theory Lib

lemma not_prefix_cases:
  fixes prefix
  assumes pfx: "\<not> prefix \<le> lst"
  and c1: "\<lbrakk> prefix \<noteq> []; lst = [] \<rbrakk> \<Longrightarrow> R"
  and c2: "\<And>a as x xs. \<lbrakk> prefix = a#as; lst = x#xs; x = a; \<not> as \<le> xs\<rbrakk> \<Longrightarrow> R"
  and c3: "\<And>a as x xs. \<lbrakk> prefix = a#as; lst = x#xs; x \<noteq> a\<rbrakk> \<Longrightarrow> R"
  shows "R" proof (cases prefix) case Nil then show ?thesis using pfx by simp next case (Cons a as) have c: "prefix = a#as" by fact show ?thesis proof (cases lst) case Nil then show ?thesis by (intro c1, simp add: Cons) next case (Cons x xs) show ?thesis proof (cases "x = a") case True show ?thesis proof (intro c2) show "\<not> as \<le> xs" using pfx c Cons True by simp qed fact+ next case False show ?thesis by (rule c3) fact+ qed qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. R proof (state)
goal (2 subgoals):
 1. prefix = [] \<Longrightarrow> R
 2. \<And>a list. prefix = a # list \<Longrightarrow> R proof (state)
this:
prefix = []

goal (2 subgoals):
 1. prefix = [] \<Longrightarrow> R
 2. \<And>a list. prefix = a # list \<Longrightarrow> R proof (chain)
picking this:
prefix = [] proof (prove)
using this:
prefix = []

goal (1 subgoal):
 1. R proof (prove)
using this:
prefix = []
\<not> prefix \<le> lst

goal (1 subgoal):
 1. R proof (state)
this:
R

goal (1 subgoal):
 1. \<And>a list. prefix = a # list \<Longrightarrow> R proof (state)
goal (1 subgoal):
 1. \<And>a list. prefix = a # list \<Longrightarrow> R proof (state)
this:
prefix = a # as

goal (1 subgoal):
 1. \<And>a list. prefix = a # list \<Longrightarrow> R proof (prove)
goal (1 subgoal):
 1. prefix = a # as proof (state)
this:
prefix = a # as

goal (1 subgoal):
 1. \<And>a list. prefix = a # list \<Longrightarrow> R proof (prove)
goal (1 subgoal):
 1. R proof (state)
goal (2 subgoals):
 1. lst = [] \<Longrightarrow> R
 2. \<And>a list. lst = a # list \<Longrightarrow> R proof (state)
this:
lst = []

goal (2 subgoals):
 1. lst = [] \<Longrightarrow> R
 2. \<And>a list. lst = a # list \<Longrightarrow> R proof (chain)
picking this:
lst = [] proof (prove)
using this:
lst = []

goal (1 subgoal):
 1. R proof (state)
this:
R

goal (1 subgoal):
 1. \<And>a list. lst = a # list \<Longrightarrow> R proof (state)
goal (1 subgoal):
 1. \<And>a list. lst = a # list \<Longrightarrow> R proof (state)
this:
lst = x # xs

goal (1 subgoal):
 1. \<And>a list. lst = a # list \<Longrightarrow> R proof (prove)
goal (1 subgoal):
 1. R proof (state)
goal (2 subgoals):
 1. x = a \<Longrightarrow> R
 2. x \<noteq> a \<Longrightarrow> R proof (state)
this:
x = a

goal (2 subgoals):
 1. x = a \<Longrightarrow> R
 2. x \<noteq> a \<Longrightarrow> R proof (prove)
goal (1 subgoal):
 1. R proof (state)
goal (4 subgoals):
 1. prefix = ?a # ?as
 2. lst = ?x # ?xs
 3. ?x = ?a
 4. \<not> ?as \<le> ?xs proof (prove)
goal (1 subgoal):
 1. \<not> as \<le> xs proof (prove)
using this:
\<not> prefix \<le> lst
prefix = a # as
lst = x # xs
x = a

goal (1 subgoal):
 1. \<not> as \<le> xs proof (state)
this:
\<not> as \<le> xs

goal (3 subgoals):
 1. prefix = ?a # as
 2. lst = ?x # xs
 3. ?x = ?a proof (state)
this:
R

goal (1 subgoal):
 1. x \<noteq> a \<Longrightarrow> R proof (state)
goal (1 subgoal):
 1. x \<noteq> a \<Longrightarrow> R proof (state)
this:
x \<noteq> a

goal (1 subgoal):
 1. x \<noteq> a \<Longrightarrow> R proof (prove)
goal (1 subgoal):
 1. R proof (state)
this:
R

goal:
No subgoals! proof (state)
this:
R

goal:
No subgoals! proof (state)
this:
R

goal:
No subgoals!