theory Lib

lemma not_prefix_induct [consumes 1, case_names Nil Neq Eq]:
  fixes prefix
  assumes np: "\<not> prefix \<le> lst"
  and base:   "\<And>x xs. P (x#xs) []"
  and r1:     "\<And>x xs y ys. x \<noteq> y \<Longrightarrow> P (x#xs) (y#ys)"
  and r2:     "\<And>x xs y ys. \<lbrakk> x = y; \<not> xs \<le> ys; P xs ys \<rbrakk> \<Longrightarrow> P (x#xs) (y#ys)"
  shows "P prefix lst" using np proof (induct lst arbitrary: prefix) case Nil then show ?case by (auto simp: neq_Nil_conv elim!: not_prefix_cases intro!: base) next case (Cons y ys) have npfx: "\<not> prefix \<le> (y # ys)" by fact then obtain x xs where pv: "prefix = x # xs" by (rule not_prefix_cases) auto have ih: "\<And>prefix. \<not> prefix \<le> ys \<Longrightarrow> P prefix ys" by fact show ?case using npfx by (simp only: pv) (erule not_prefix_cases, auto intro: r1 r2 ih) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P prefix lst proof (prove)
using this:
\<not> prefix \<le> lst

goal (1 subgoal):
 1. P prefix lst proof (state)
goal (2 subgoals):
 1. \<And>prefix. \<not> prefix \<le> [] \<Longrightarrow> P prefix []
 2. \<And>a lst prefix. \<lbrakk>\<And>prefix. \<not> prefix \<le> lst \<Longrightarrow> P prefix lst; \<not> prefix \<le> a # lst\<rbrakk> \<Longrightarrow> P prefix (a # lst) proof (state)
this:
\<not> prefix \<le> []

goal (2 subgoals):
 1. \<And>prefix. \<not> prefix \<le> [] \<Longrightarrow> P prefix []
 2. \<And>a lst prefix. \<lbrakk>\<And>prefix. \<not> prefix \<le> lst \<Longrightarrow> P prefix lst; \<not> prefix \<le> a # lst\<rbrakk> \<Longrightarrow> P prefix (a # lst) proof (chain)
picking this:
\<not> prefix \<le> [] proof (prove)
using this:
\<not> prefix \<le> []

goal (1 subgoal):
 1. P prefix [] proof (state)
this:
P prefix []

goal (1 subgoal):
 1. \<And>a lst prefix. \<lbrakk>\<And>prefix. \<not> prefix \<le> lst \<Longrightarrow> P prefix lst; \<not> prefix \<le> a # lst\<rbrakk> \<Longrightarrow> P prefix (a # lst) proof (state)
goal (1 subgoal):
 1. \<And>a lst prefix. \<lbrakk>\<And>prefix. \<not> prefix \<le> lst \<Longrightarrow> P prefix lst; \<not> prefix \<le> a # lst\<rbrakk> \<Longrightarrow> P prefix (a # lst) proof (state)
this:
\<not> ?prefix \<le> ys \<Longrightarrow> P ?prefix ys
\<not> prefix \<le> y # ys

goal (1 subgoal):
 1. \<And>a lst prefix. \<lbrakk>\<And>prefix. \<not> prefix \<le> lst \<Longrightarrow> P prefix lst; \<not> prefix \<le> a # lst\<rbrakk> \<Longrightarrow> P prefix (a # lst) proof (prove)
goal (1 subgoal):
 1. \<not> prefix \<le> y # ys proof (state)
this:
\<not> prefix \<le> y # ys

goal (1 subgoal):
 1. \<And>a lst prefix. \<lbrakk>\<And>prefix. \<not> prefix \<le> lst \<Longrightarrow> P prefix lst; \<not> prefix \<le> a # lst\<rbrakk> \<Longrightarrow> P prefix (a # lst) proof (chain)
picking this:
\<not> prefix \<le> y # ys proof (prove)
using this:
\<not> prefix \<le> y # ys

goal (1 subgoal):
 1. (\<And>x xs. prefix = x # xs \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
prefix = x # xs

goal (1 subgoal):
 1. \<And>a lst prefix. \<lbrakk>\<And>prefix. \<not> prefix \<le> lst \<Longrightarrow> P prefix lst; \<not> prefix \<le> a # lst\<rbrakk> \<Longrightarrow> P prefix (a # lst) proof (prove)
goal (1 subgoal):
 1. \<And>prefix. \<not> prefix \<le> ys \<Longrightarrow> P prefix ys proof (state)
this:
\<not> ?prefix \<le> ys \<Longrightarrow> P ?prefix ys

goal (1 subgoal):
 1. \<And>a lst prefix. \<lbrakk>\<And>prefix. \<not> prefix \<le> lst \<Longrightarrow> P prefix lst; \<not> prefix \<le> a # lst\<rbrakk> \<Longrightarrow> P prefix (a # lst) proof (prove)
goal (1 subgoal):
 1. P prefix (y # ys) proof (prove)
using this:
\<not> prefix \<le> y # ys

goal (1 subgoal):
 1. P prefix (y # ys) proof (state)
this:
P prefix (y # ys)

goal:
No subgoals!