[STATEMENT]
lemma lapp_fin_fin_lemma:
  assumes rsA: "r @@ s \<in> A\<^sup>\<star>"
  shows "r \<in> A\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<in> A\<^sup>\<star>
[PROOF STEP]
using rsA
[PROOF STATE]
proof (prove)
using this:
r @@ s \<in> A\<^sup>\<star>

goal (1 subgoal):
 1. r \<in> A\<^sup>\<star>
[PROOF STEP]
proof(induct l\<equiv>"r@@s" arbitrary: r)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>r. r @@ s = LNil \<Longrightarrow> r \<in> A\<^sup>\<star>
 2. \<And>a l r. \<lbrakk>l \<in> A\<^sup>\<star>; \<And>r. l = r @@ s \<Longrightarrow> r \<in> A\<^sup>\<star>; a \<in> A; a ## l = r @@ s\<rbrakk> \<Longrightarrow> r \<in> A\<^sup>\<star>
[PROOF STEP]
case LNil_fin
[PROOF STATE]
proof (state)
this:
r @@ s = LNil

goal (2 subgoals):
 1. \<And>r. r @@ s = LNil \<Longrightarrow> r \<in> A\<^sup>\<star>
 2. \<And>a l r. \<lbrakk>l \<in> A\<^sup>\<star>; \<And>r. l = r @@ s \<Longrightarrow> r \<in> A\<^sup>\<star>; a \<in> A; a ## l = r @@ s\<rbrakk> \<Longrightarrow> r \<in> A\<^sup>\<star>
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
r @@ s = LNil

goal (1 subgoal):
 1. r \<in> A\<^sup>\<star>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r \<in> A\<^sup>\<star>

goal (1 subgoal):
 1. \<And>a l r. \<lbrakk>l \<in> A\<^sup>\<star>; \<And>r. l = r @@ s \<Longrightarrow> r \<in> A\<^sup>\<star>; a \<in> A; a ## l = r @@ s\<rbrakk> \<Longrightarrow> r \<in> A\<^sup>\<star>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a l r. \<lbrakk>l \<in> A\<^sup>\<star>; \<And>r. l = r @@ s \<Longrightarrow> r \<in> A\<^sup>\<star>; a \<in> A; a ## l = r @@ s\<rbrakk> \<Longrightarrow> r \<in> A\<^sup>\<star>
[PROOF STEP]
case (LCons_fin a l')
[PROOF STATE]
proof (state)
this:
l' \<in> A\<^sup>\<star>
l' = ?r @@ s \<Longrightarrow> ?r \<in> A\<^sup>\<star>
a \<in> A
a ## l' = r @@ s

goal (1 subgoal):
 1. \<And>a l r. \<lbrakk>l \<in> A\<^sup>\<star>; \<And>r. l = r @@ s \<Longrightarrow> r \<in> A\<^sup>\<star>; a \<in> A; a ## l = r @@ s\<rbrakk> \<Longrightarrow> r \<in> A\<^sup>\<star>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<in> A\<^sup>\<star>
[PROOF STEP]
proof (cases "r")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. r = LNil \<Longrightarrow> r \<in> A\<^sup>\<star>
 2. \<And>x21 x22. r = x21 ## x22 \<Longrightarrow> r \<in> A\<^sup>\<star>
[PROOF STEP]
case LNil
[PROOF STATE]
proof (state)
this:
r = LNil

goal (2 subgoals):
 1. r = LNil \<Longrightarrow> r \<in> A\<^sup>\<star>
 2. \<And>x21 x22. r = x21 ## x22 \<Longrightarrow> r \<in> A\<^sup>\<star>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
r = LNil

goal (1 subgoal):
 1. r \<in> A\<^sup>\<star>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r \<in> A\<^sup>\<star>

goal (1 subgoal):
 1. \<And>x21 x22. r = x21 ## x22 \<Longrightarrow> r \<in> A\<^sup>\<star>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x21 x22. r = x21 ## x22 \<Longrightarrow> r \<in> A\<^sup>\<star>
[PROOF STEP]
case (LCons x xs)
[PROOF STATE]
proof (state)
this:
r = x ## xs

goal (1 subgoal):
 1. \<And>x21 x22. r = x21 ## x22 \<Longrightarrow> r \<in> A\<^sup>\<star>
[PROOF STEP]
with \<open>a##l' = r @@ s\<close>
[PROOF STATE]
proof (chain)
picking this:
a ## l' = r @@ s
r = x ## xs
[PROOF STEP]
have "a = x" and "l' = xs @@ s"
[PROOF STATE]
proof (prove)
using this:
a ## l' = r @@ s
r = x ## xs

goal (1 subgoal):
 1. a = x &&& l' = xs @@ s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a = x
l' = xs @@ s

goal (1 subgoal):
 1. \<And>x21 x22. r = x21 ## x22 \<Longrightarrow> r \<in> A\<^sup>\<star>
[PROOF STEP]
with LCons_fin LCons
[PROOF STATE]
proof (chain)
picking this:
l' \<in> A\<^sup>\<star>
l' = ?r @@ s \<Longrightarrow> ?r \<in> A\<^sup>\<star>
a \<in> A
a ## l' = r @@ s
r = x ## xs
a = x
l' = xs @@ s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
l' \<in> A\<^sup>\<star>
l' = ?r @@ s \<Longrightarrow> ?r \<in> A\<^sup>\<star>
a \<in> A
a ## l' = r @@ s
r = x ## xs
a = x
l' = xs @@ s

goal (1 subgoal):
 1. r \<in> A\<^sup>\<star>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r \<in> A\<^sup>\<star>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
r \<in> A\<^sup>\<star>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lapp_fin_fin_iff [iff]: "(r @@ s \<in> A\<^sup>\<star>) = (r \<in> A\<^sup>\<star> \<and> s \<in> A\<^sup>\<star>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r @@ s \<in> A\<^sup>\<star>) = (r \<in> A\<^sup>\<star> \<and> s \<in> A\<^sup>\<star>)
[PROOF STEP]
proof (auto intro: lappfin_finT lapp_fin_fin_lemma)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r @@ s \<in> A\<^sup>\<star> \<Longrightarrow> s \<in> A\<^sup>\<star>
[PROOF STEP]
assume rsA: "r @@ s \<in> A\<^sup>\<star>"
[PROOF STATE]
proof (state)
this:
r @@ s \<in> A\<^sup>\<star>

goal (1 subgoal):
 1. r @@ s \<in> A\<^sup>\<star> \<Longrightarrow> s \<in> A\<^sup>\<star>
[PROOF STEP]
hence "r \<in> A\<^sup>\<star>"
[PROOF STATE]
proof (prove)
using this:
r @@ s \<in> A\<^sup>\<star>

goal (1 subgoal):
 1. r \<in> A\<^sup>\<star>
[PROOF STEP]
by (rule lapp_fin_fin_lemma)
[PROOF STATE]
proof (state)
this:
r \<in> A\<^sup>\<star>

goal (1 subgoal):
 1. r @@ s \<in> A\<^sup>\<star> \<Longrightarrow> s \<in> A\<^sup>\<star>
[PROOF STEP]
hence "r @@ s \<in> A\<^sup>\<star> \<longrightarrow> s \<in> A\<^sup>\<star>"
[PROOF STATE]
proof (prove)
using this:
r \<in> A\<^sup>\<star>

goal (1 subgoal):
 1. r @@ s \<in> A\<^sup>\<star> \<longrightarrow> s \<in> A\<^sup>\<star>
[PROOF STEP]
by (induct "r", simp) (auto elim: finlsts.cases)
[PROOF STATE]
proof (state)
this:
r @@ s \<in> A\<^sup>\<star> \<longrightarrow> s \<in> A\<^sup>\<star>

goal (1 subgoal):
 1. r @@ s \<in> A\<^sup>\<star> \<Longrightarrow> s \<in> A\<^sup>\<star>
[PROOF STEP]
with rsA
[PROOF STATE]
proof (chain)
picking this:
r @@ s \<in> A\<^sup>\<star>
r @@ s \<in> A\<^sup>\<star> \<longrightarrow> s \<in> A\<^sup>\<star>
[PROOF STEP]
show "s \<in> A\<^sup>\<star>"
[PROOF STATE]
proof (prove)
using this:
r @@ s \<in> A\<^sup>\<star>
r @@ s \<in> A\<^sup>\<star> \<longrightarrow> s \<in> A\<^sup>\<star>

goal (1 subgoal):
 1. s \<in> A\<^sup>\<star>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s \<in> A\<^sup>\<star>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lapp_all_invT:
assumes rs: "r@@s \<in> A\<^sup>\<infinity>"
  shows "r \<in> A\<^sup>\<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<in> A\<^sup>\<infinity>
[PROOF STEP]
proof (cases "r \<in> UNIV\<^sup>\<star>")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. r \<in> UNIV\<^sup>\<star> \<Longrightarrow> r \<in> A\<^sup>\<infinity>
 2. r \<notin> UNIV\<^sup>\<star> \<Longrightarrow> r \<in> A\<^sup>\<infinity>
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
r \<notin> UNIV\<^sup>\<star>

goal (2 subgoals):
 1. r \<in> UNIV\<^sup>\<star> \<Longrightarrow> r \<in> A\<^sup>\<infinity>
 2. r \<notin> UNIV\<^sup>\<star> \<Longrightarrow> r \<in> A\<^sup>\<infinity>
[PROOF STEP]
with rs
[PROOF STATE]
proof (chain)
picking this:
r @@ s \<in> A\<^sup>\<infinity>
r \<notin> UNIV\<^sup>\<star>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
r @@ s \<in> A\<^sup>\<infinity>
r \<notin> UNIV\<^sup>\<star>

goal (1 subgoal):
 1. r \<in> A\<^sup>\<infinity>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
r \<in> A\<^sup>\<infinity>

goal (1 subgoal):
 1. r \<in> UNIV\<^sup>\<star> \<Longrightarrow> r \<in> A\<^sup>\<infinity>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r \<in> UNIV\<^sup>\<star> \<Longrightarrow> r \<in> A\<^sup>\<infinity>
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
r \<in> UNIV\<^sup>\<star>

goal (1 subgoal):
 1. r \<in> UNIV\<^sup>\<star> \<Longrightarrow> r \<in> A\<^sup>\<infinity>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
r \<in> UNIV\<^sup>\<star>

goal (1 subgoal):
 1. r \<in> A\<^sup>\<infinity>
[PROOF STEP]
using rs
[PROOF STATE]
proof (prove)
using this:
r \<in> UNIV\<^sup>\<star>
r @@ s \<in> A\<^sup>\<infinity>

goal (1 subgoal):
 1. r \<in> A\<^sup>\<infinity>
[PROOF STEP]
by (induct "r") auto
[PROOF STATE]
proof (state)
this:
r \<in> A\<^sup>\<infinity>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lapp_fin_infT: "\<lbrakk>s \<in> A\<^sup>\<star>; t \<in> A\<^sup>\<omega>\<rbrakk> \<Longrightarrow> s @@ t \<in> A\<^sup>\<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<in> A\<^sup>\<star>; t \<in> A\<^sup>\<omega>\<rbrakk> \<Longrightarrow> s @@ t \<in> A\<^sup>\<omega>
[PROOF STEP]
by (induct rule: finlsts.induct)
     (auto intro: inflstsI2)


[STATEMENT]
lemma app_invT:
  assumes "r \<in> A\<^sup>\<star>" shows "r @@ s \<in> A\<^sup>\<omega> \<Longrightarrow> s \<in> A\<^sup>\<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r @@ s \<in> A\<^sup>\<omega> \<Longrightarrow> s \<in> A\<^sup>\<omega>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
r \<in> A\<^sup>\<star>

goal (1 subgoal):
 1. r @@ s \<in> A\<^sup>\<omega> \<Longrightarrow> s \<in> A\<^sup>\<omega>
[PROOF STEP]
proof (induct arbitrary: s)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>l s. \<lbrakk>l = LNil; l @@ s \<in> A\<^sup>\<omega>\<rbrakk> \<Longrightarrow> s \<in> A\<^sup>\<omega>
 2. \<And>a l s. \<lbrakk>l \<in> A\<^sup>\<star>; \<And>s. l @@ s \<in> A\<^sup>\<omega> \<Longrightarrow> s \<in> A\<^sup>\<omega>; a \<in> A; (a ## l) @@ s \<in> A\<^sup>\<omega>\<rbrakk> \<Longrightarrow> s \<in> A\<^sup>\<omega>
[PROOF STEP]
case LNil_fin
[PROOF STATE]
proof (state)
this:
l_ = LNil
l_ @@ s \<in> A\<^sup>\<omega>

goal (2 subgoals):
 1. \<And>l s. \<lbrakk>l = LNil; l @@ s \<in> A\<^sup>\<omega>\<rbrakk> \<Longrightarrow> s \<in> A\<^sup>\<omega>
 2. \<And>a l s. \<lbrakk>l \<in> A\<^sup>\<star>; \<And>s. l @@ s \<in> A\<^sup>\<omega> \<Longrightarrow> s \<in> A\<^sup>\<omega>; a \<in> A; (a ## l) @@ s \<in> A\<^sup>\<omega>\<rbrakk> \<Longrightarrow> s \<in> A\<^sup>\<omega>
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
l_ = LNil
l_ @@ s \<in> A\<^sup>\<omega>

goal (1 subgoal):
 1. s \<in> A\<^sup>\<omega>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
s \<in> A\<^sup>\<omega>

goal (1 subgoal):
 1. \<And>a l s. \<lbrakk>l \<in> A\<^sup>\<star>; \<And>s. l @@ s \<in> A\<^sup>\<omega> \<Longrightarrow> s \<in> A\<^sup>\<omega>; a \<in> A; (a ## l) @@ s \<in> A\<^sup>\<omega>\<rbrakk> \<Longrightarrow> s \<in> A\<^sup>\<omega>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a l s. \<lbrakk>l \<in> A\<^sup>\<star>; \<And>s. l @@ s \<in> A\<^sup>\<omega> \<Longrightarrow> s \<in> A\<^sup>\<omega>; a \<in> A; (a ## l) @@ s \<in> A\<^sup>\<omega>\<rbrakk> \<Longrightarrow> s \<in> A\<^sup>\<omega>
[PROOF STEP]
case (LCons_fin a l)
[PROOF STATE]
proof (state)
this:
l \<in> A\<^sup>\<star>
l @@ ?s \<in> A\<^sup>\<omega> \<Longrightarrow> ?s \<in> A\<^sup>\<omega>
a \<in> A
(a ## l) @@ s \<in> A\<^sup>\<omega>

goal (1 subgoal):
 1. \<And>a l s. \<lbrakk>l \<in> A\<^sup>\<star>; \<And>s. l @@ s \<in> A\<^sup>\<omega> \<Longrightarrow> s \<in> A\<^sup>\<omega>; a \<in> A; (a ## l) @@ s \<in> A\<^sup>\<omega>\<rbrakk> \<Longrightarrow> s \<in> A\<^sup>\<omega>
[PROOF STEP]
from \<open>(a ## l) @@ s \<in> A\<^sup>\<omega>\<close>
[PROOF STATE]
proof (chain)
picking this:
(a ## l) @@ s \<in> A\<^sup>\<omega>
[PROOF STEP]
have "a ## (l @@ s) \<in> A\<^sup>\<omega>"
[PROOF STATE]
proof (prove)
using this:
(a ## l) @@ s \<in> A\<^sup>\<omega>

goal (1 subgoal):
 1. a ## l @@ s \<in> A\<^sup>\<omega>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a ## l @@ s \<in> A\<^sup>\<omega>

goal (1 subgoal):
 1. \<And>a l s. \<lbrakk>l \<in> A\<^sup>\<star>; \<And>s. l @@ s \<in> A\<^sup>\<omega> \<Longrightarrow> s \<in> A\<^sup>\<omega>; a \<in> A; (a ## l) @@ s \<in> A\<^sup>\<omega>\<rbrakk> \<Longrightarrow> s \<in> A\<^sup>\<omega>
[PROOF STEP]
hence "l @@ s \<in> A\<^sup>\<omega>"
[PROOF STATE]
proof (prove)
using this:
a ## l @@ s \<in> A\<^sup>\<omega>

goal (1 subgoal):
 1. l @@ s \<in> A\<^sup>\<omega>
[PROOF STEP]
by (auto elim: inflsts_cases)
[PROOF STATE]
proof (state)
this:
l @@ s \<in> A\<^sup>\<omega>

goal (1 subgoal):
 1. \<And>a l s. \<lbrakk>l \<in> A\<^sup>\<star>; \<And>s. l @@ s \<in> A\<^sup>\<omega> \<Longrightarrow> s \<in> A\<^sup>\<omega>; a \<in> A; (a ## l) @@ s \<in> A\<^sup>\<omega>\<rbrakk> \<Longrightarrow> s \<in> A\<^sup>\<omega>
[PROOF STEP]
with LCons_fin
[PROOF STATE]
proof (chain)
picking this:
l \<in> A\<^sup>\<star>
l @@ ?s \<in> A\<^sup>\<omega> \<Longrightarrow> ?s \<in> A\<^sup>\<omega>
a \<in> A
(a ## l) @@ s \<in> A\<^sup>\<omega>
l @@ s \<in> A\<^sup>\<omega>
[PROOF STEP]
show "s \<in> A\<^sup>\<omega>"
[PROOF STATE]
proof (prove)
using this:
l \<in> A\<^sup>\<star>
l @@ ?s \<in> A\<^sup>\<omega> \<Longrightarrow> ?s \<in> A\<^sup>\<omega>
a \<in> A
(a ## l) @@ s \<in> A\<^sup>\<omega>
l @@ s \<in> A\<^sup>\<omega>

goal (1 subgoal):
 1. s \<in> A\<^sup>\<omega>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
s \<in> A\<^sup>\<omega>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lapp_inv2T:
  assumes rsinf: "r @@ s \<in> A\<^sup>\<omega>"
  shows "r \<in> A\<^sup>\<star> \<and> s \<in> A\<^sup>\<omega> \<or> r \<in> A\<^sup>\<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<in> A\<^sup>\<star> \<and> s \<in> A\<^sup>\<omega> \<or> r \<in> A\<^sup>\<omega>
[PROOF STEP]
proof (rule disjCI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r \<notin> A\<^sup>\<omega> \<Longrightarrow> r \<in> A\<^sup>\<star> \<and> s \<in> A\<^sup>\<omega>
[PROOF STEP]
assume rnotinf: "r \<notin> A\<^sup>\<omega>"
[PROOF STATE]
proof (state)
this:
r \<notin> A\<^sup>\<omega>

goal (1 subgoal):
 1. r \<notin> A\<^sup>\<omega> \<Longrightarrow> r \<in> A\<^sup>\<star> \<and> s \<in> A\<^sup>\<omega>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
r \<notin> A\<^sup>\<omega>

goal (1 subgoal):
 1. r \<notin> A\<^sup>\<omega> \<Longrightarrow> r \<in> A\<^sup>\<star> \<and> s \<in> A\<^sup>\<omega>
[PROOF STEP]
from rsinf
[PROOF STATE]
proof (chain)
picking this:
r @@ s \<in> A\<^sup>\<omega>
[PROOF STEP]
have rsall: "r@@s \<in> A\<^sup>\<infinity>"
[PROOF STATE]
proof (prove)
using this:
r @@ s \<in> A\<^sup>\<omega>

goal (1 subgoal):
 1. r @@ s \<in> A\<^sup>\<infinity>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r @@ s \<in> A\<^sup>\<infinity>

goal (1 subgoal):
 1. r \<notin> A\<^sup>\<omega> \<Longrightarrow> r \<in> A\<^sup>\<star> \<and> s \<in> A\<^sup>\<omega>
[PROOF STEP]
hence "r \<in> A\<^sup>\<infinity>"
[PROOF STATE]
proof (prove)
using this:
r @@ s \<in> A\<^sup>\<infinity>

goal (1 subgoal):
 1. r \<in> A\<^sup>\<infinity>
[PROOF STEP]
by (rule lapp_all_invT)
[PROOF STATE]
proof (state)
this:
r \<in> A\<^sup>\<infinity>

goal (1 subgoal):
 1. r \<notin> A\<^sup>\<omega> \<Longrightarrow> r \<in> A\<^sup>\<star> \<and> s \<in> A\<^sup>\<omega>
[PROOF STEP]
hence "r \<in> A\<^sup>\<star>"
[PROOF STATE]
proof (prove)
using this:
r \<in> A\<^sup>\<infinity>

goal (1 subgoal):
 1. r \<in> A\<^sup>\<star>
[PROOF STEP]
using rnotinf
[PROOF STATE]
proof (prove)
using this:
r \<in> A\<^sup>\<infinity>
r \<notin> A\<^sup>\<omega>

goal (1 subgoal):
 1. r \<in> A\<^sup>\<star>
[PROOF STEP]
by (auto elim: alllstsE)
[PROOF STATE]
proof (state)
this:
r \<in> A\<^sup>\<star>

goal (1 subgoal):
 1. r \<notin> A\<^sup>\<omega> \<Longrightarrow> r \<in> A\<^sup>\<star> \<and> s \<in> A\<^sup>\<omega>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
r \<notin> A\<^sup>\<omega>
r \<in> A\<^sup>\<star>
[PROOF STEP]
show "r \<in> A\<^sup>\<star> \<and> s \<in> A\<^sup>\<omega>"
[PROOF STATE]
proof (prove)
using this:
r \<notin> A\<^sup>\<omega>
r \<in> A\<^sup>\<star>

goal (1 subgoal):
 1. r \<in> A\<^sup>\<star> \<and> s \<in> A\<^sup>\<omega>
[PROOF STEP]
using rsinf
[PROOF STATE]
proof (prove)
using this:
r \<notin> A\<^sup>\<omega>
r \<in> A\<^sup>\<star>
r @@ s \<in> A\<^sup>\<omega>

goal (1 subgoal):
 1. r \<in> A\<^sup>\<star> \<and> s \<in> A\<^sup>\<omega>
[PROOF STEP]
by (auto  intro: app_invT)
[PROOF STATE]
proof (state)
this:
r \<in> A\<^sup>\<star> \<and> s \<in> A\<^sup>\<omega>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lapp_infT:
  "(r @@ s \<in> A\<^sup>\<omega>) = (r \<in> A\<^sup>\<star> \<and> s \<in> A\<^sup>\<omega> \<or> r \<in> A\<^sup>\<omega>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r @@ s \<in> A\<^sup>\<omega>) = (r \<in> A\<^sup>\<star> \<and> s \<in> A\<^sup>\<omega> \<or> r \<in> A\<^sup>\<omega>)
[PROOF STEP]
by (auto dest: lapp_inv2T intro: lapp_fin_infT)


[STATEMENT]
lemma lapp_allT_iff:
  "(r @@ s \<in> A\<^sup>\<infinity>) = (r \<in> A\<^sup>\<star> \<and> s \<in> A\<^sup>\<infinity> \<or> r \<in> A\<^sup>\<omega>)"
  (is "?L = ?R")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r @@ s \<in> A\<^sup>\<infinity>) = (r \<in> A\<^sup>\<star> \<and> s \<in> A\<^sup>\<infinity> \<or> r \<in> A\<^sup>\<omega>)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. r @@ s \<in> A\<^sup>\<infinity> \<Longrightarrow> r \<in> A\<^sup>\<star> \<and> s \<in> A\<^sup>\<infinity> \<or> r \<in> A\<^sup>\<omega>
 2. r \<in> A\<^sup>\<star> \<and> s \<in> A\<^sup>\<infinity> \<or> r \<in> A\<^sup>\<omega> \<Longrightarrow> r @@ s \<in> A\<^sup>\<infinity>
[PROOF STEP]
assume ?L
[PROOF STATE]
proof (state)
this:
r @@ s \<in> A\<^sup>\<infinity>

goal (2 subgoals):
 1. r @@ s \<in> A\<^sup>\<infinity> \<Longrightarrow> r \<in> A\<^sup>\<star> \<and> s \<in> A\<^sup>\<infinity> \<or> r \<in> A\<^sup>\<omega>
 2. r \<in> A\<^sup>\<star> \<and> s \<in> A\<^sup>\<infinity> \<or> r \<in> A\<^sup>\<omega> \<Longrightarrow> r @@ s \<in> A\<^sup>\<infinity>
[PROOF STEP]
thus ?R
[PROOF STATE]
proof (prove)
using this:
r @@ s \<in> A\<^sup>\<infinity>

goal (1 subgoal):
 1. r \<in> A\<^sup>\<star> \<and> s \<in> A\<^sup>\<infinity> \<or> r \<in> A\<^sup>\<omega>
[PROOF STEP]
by (cases rule: alllstsE) (auto simp: lapp_infT intro: finsubsetall)
[PROOF STATE]
proof (state)
this:
r \<in> A\<^sup>\<star> \<and> s \<in> A\<^sup>\<infinity> \<or> r \<in> A\<^sup>\<omega>

goal (1 subgoal):
 1. r \<in> A\<^sup>\<star> \<and> s \<in> A\<^sup>\<infinity> \<or> r \<in> A\<^sup>\<omega> \<Longrightarrow> r @@ s \<in> A\<^sup>\<infinity>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r \<in> A\<^sup>\<star> \<and> s \<in> A\<^sup>\<infinity> \<or> r \<in> A\<^sup>\<omega> \<Longrightarrow> r @@ s \<in> A\<^sup>\<infinity>
[PROOF STEP]
assume ?R
[PROOF STATE]
proof (state)
this:
r \<in> A\<^sup>\<star> \<and> s \<in> A\<^sup>\<infinity> \<or> r \<in> A\<^sup>\<omega>

goal (1 subgoal):
 1. r \<in> A\<^sup>\<star> \<and> s \<in> A\<^sup>\<infinity> \<or> r \<in> A\<^sup>\<omega> \<Longrightarrow> r @@ s \<in> A\<^sup>\<infinity>
[PROOF STEP]
thus ?L
[PROOF STATE]
proof (prove)
using this:
r \<in> A\<^sup>\<star> \<and> s \<in> A\<^sup>\<infinity> \<or> r \<in> A\<^sup>\<omega>

goal (1 subgoal):
 1. r @@ s \<in> A\<^sup>\<infinity>
[PROOF STEP]
by (auto dest: finsubsetall intro: lappT)
[PROOF STATE]
proof (state)
this:
r @@ s \<in> A\<^sup>\<infinity>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lrevT [simp, intro!]:
  "xs \<in> A\<^sup>\<star> \<Longrightarrow> lrev xs \<in> A\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<in> A\<^sup>\<star> \<Longrightarrow> lrev xs \<in> A\<^sup>\<star>
[PROOF STEP]
by (induct rule: finlsts.induct) auto


[STATEMENT]
lemma lrev_lappend [simp]:
  assumes fin: "xs \<in> UNIV\<^sup>\<star>" "ys \<in> UNIV\<^sup>\<star>"
  shows "lrev (xs @@ ys) = (lrev ys) @@ (lrev xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lrev (xs @@ ys) = lrev ys @@ lrev xs
[PROOF STEP]
using fin
[PROOF STATE]
proof (prove)
using this:
xs \<in> UNIV\<^sup>\<star>
ys \<in> UNIV\<^sup>\<star>

goal (1 subgoal):
 1. lrev (xs @@ ys) = lrev ys @@ lrev xs
[PROOF STEP]
by induct (auto simp: lrev_LCons [of _ UNIV] lappend_assoc)


[STATEMENT]
lemma lrev_lrev_ident [simp]:
  assumes fin: "xs \<in> UNIV\<^sup>\<star>"
  shows "lrev (lrev xs) = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lrev (lrev xs) = xs
[PROOF STEP]
using fin
[PROOF STATE]
proof (prove)
using this:
xs \<in> UNIV\<^sup>\<star>

goal (1 subgoal):
 1. lrev (lrev xs) = xs
[PROOF STEP]
proof (induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>l. l = LNil \<Longrightarrow> lrev (lrev l) = l
 2. \<And>a l. \<lbrakk>l \<in> UNIV\<^sup>\<star>; lrev (lrev l) = l; a \<in> UNIV\<rbrakk> \<Longrightarrow> lrev (lrev (a ## l)) = a ## l
[PROOF STEP]
case (LCons_fin a l)
[PROOF STATE]
proof (state)
this:
l \<in> UNIV\<^sup>\<star>
lrev (lrev l) = l
a \<in> UNIV

goal (2 subgoals):
 1. \<And>l. l = LNil \<Longrightarrow> lrev (lrev l) = l
 2. \<And>a l. \<lbrakk>l \<in> UNIV\<^sup>\<star>; lrev (lrev l) = l; a \<in> UNIV\<rbrakk> \<Longrightarrow> lrev (lrev (a ## l)) = a ## l
[PROOF STEP]
have "a ## LNil \<in> UNIV\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a ## LNil \<in> UNIV\<^sup>\<star>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a ## LNil \<in> UNIV\<^sup>\<star>

goal (2 subgoals):
 1. \<And>l. l = LNil \<Longrightarrow> lrev (lrev l) = l
 2. \<And>a l. \<lbrakk>l \<in> UNIV\<^sup>\<star>; lrev (lrev l) = l; a \<in> UNIV\<rbrakk> \<Longrightarrow> lrev (lrev (a ## l)) = a ## l
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
a ## LNil \<in> UNIV\<^sup>\<star>

goal (1 subgoal):
 1. lrev (lrev (a ## l)) = a ## l
[PROOF STEP]
using LCons_fin
[PROOF STATE]
proof (prove)
using this:
a ## LNil \<in> UNIV\<^sup>\<star>
l \<in> UNIV\<^sup>\<star>
lrev (lrev l) = l
a \<in> UNIV

goal (1 subgoal):
 1. lrev (lrev (a ## l)) = a ## l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lrev (lrev (a ## l)) = a ## l

goal (1 subgoal):
 1. \<And>l. l = LNil \<Longrightarrow> lrev (lrev l) = l
[PROOF STEP]
qed simp


[STATEMENT]
lemma LNil_is_lrev_conv [iff]:
"xs \<in> UNIV\<^sup>\<star> \<Longrightarrow> (LNil = lrev xs) = (xs = LNil)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<in> UNIV\<^sup>\<star> \<Longrightarrow> (LNil = lrev xs) = (xs = LNil)
[PROOF STEP]
by (induct rule: finlsts.induct) auto


[STATEMENT]
lemma lrev_is_lrev_conv [iff]:
assumes fin: "xs \<in> UNIV\<^sup>\<star>" "ys \<in> UNIV\<^sup>\<star>"
  shows "(lrev xs = lrev ys) = (xs = ys)"
  (is "?L = ?R")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (lrev xs = lrev ys) = (xs = ys)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. lrev xs = lrev ys \<Longrightarrow> xs = ys
 2. xs = ys \<Longrightarrow> lrev xs = lrev ys
[PROOF STEP]
assume L: ?L
[PROOF STATE]
proof (state)
this:
lrev xs = lrev ys

goal (2 subgoals):
 1. lrev xs = lrev ys \<Longrightarrow> xs = ys
 2. xs = ys \<Longrightarrow> lrev xs = lrev ys
[PROOF STEP]
hence "lrev (lrev xs) = lrev (lrev ys)"
[PROOF STATE]
proof (prove)
using this:
lrev xs = lrev ys

goal (1 subgoal):
 1. lrev (lrev xs) = lrev (lrev ys)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lrev (lrev xs) = lrev (lrev ys)

goal (2 subgoals):
 1. lrev xs = lrev ys \<Longrightarrow> xs = ys
 2. xs = ys \<Longrightarrow> lrev xs = lrev ys
[PROOF STEP]
thus ?R
[PROOF STATE]
proof (prove)
using this:
lrev (lrev xs) = lrev (lrev ys)

goal (1 subgoal):
 1. xs = ys
[PROOF STEP]
using fin
[PROOF STATE]
proof (prove)
using this:
lrev (lrev xs) = lrev (lrev ys)
xs \<in> UNIV\<^sup>\<star>
ys \<in> UNIV\<^sup>\<star>

goal (1 subgoal):
 1. xs = ys
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
xs = ys

goal (1 subgoal):
 1. xs = ys \<Longrightarrow> lrev xs = lrev ys
[PROOF STEP]
qed simp


[STATEMENT]
lemma lrev_induct [case_names LNil snocl, consumes 1]:
  assumes fin: "xs \<in> A\<^sup>\<star>"
  and init: "P LNil"
  and step: "\<And>x xs. \<lbrakk> xs \<in> A\<^sup>\<star>; P xs; x \<in> A \<rbrakk> \<Longrightarrow> P (xs @@ x##LNil)"
  shows "P xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P xs
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P xs
[PROOF STEP]
define l where "l = lrev xs"
[PROOF STATE]
proof (state)
this:
l = lrev xs

goal (1 subgoal):
 1. P xs
[PROOF STEP]
with fin
[PROOF STATE]
proof (chain)
picking this:
xs \<in> A\<^sup>\<star>
l = lrev xs
[PROOF STEP]
have "l \<in> A\<^sup>\<star>"
[PROOF STATE]
proof (prove)
using this:
xs \<in> A\<^sup>\<star>
l = lrev xs

goal (1 subgoal):
 1. l \<in> A\<^sup>\<star>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
l \<in> A\<^sup>\<star>

goal (1 subgoal):
 1. P xs
[PROOF STEP]
hence "P (lrev l)"
[PROOF STATE]
proof (prove)
using this:
l \<in> A\<^sup>\<star>

goal (1 subgoal):
 1. P (lrev l)
[PROOF STEP]
proof (induct l)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>l. l = LNil \<Longrightarrow> P (lrev l)
 2. \<And>a l. \<lbrakk>l \<in> A\<^sup>\<star>; P (lrev l); a \<in> A\<rbrakk> \<Longrightarrow> P (lrev (a ## l))
[PROOF STEP]
case LNil_fin
[PROOF STATE]
proof (state)
this:
l_ = LNil

goal (2 subgoals):
 1. \<And>l. l = LNil \<Longrightarrow> P (lrev l)
 2. \<And>a l. \<lbrakk>l \<in> A\<^sup>\<star>; P (lrev l); a \<in> A\<rbrakk> \<Longrightarrow> P (lrev (a ## l))
[PROOF STEP]
with init
[PROOF STATE]
proof (chain)
picking this:
P LNil
l_ = LNil
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
P LNil
l_ = LNil

goal (1 subgoal):
 1. P (lrev l_)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P (lrev l_)

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>l \<in> A\<^sup>\<star>; P (lrev l); a \<in> A\<rbrakk> \<Longrightarrow> P (lrev (a ## l))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a l. \<lbrakk>l \<in> A\<^sup>\<star>; P (lrev l); a \<in> A\<rbrakk> \<Longrightarrow> P (lrev (a ## l))
[PROOF STEP]
case (LCons_fin a l)
[PROOF STATE]
proof (state)
this:
l \<in> A\<^sup>\<star>
P (lrev l)
a \<in> A

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>l \<in> A\<^sup>\<star>; P (lrev l); a \<in> A\<rbrakk> \<Longrightarrow> P (lrev (a ## l))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
l \<in> A\<^sup>\<star>
P (lrev l)
a \<in> A

goal (1 subgoal):
 1. P (lrev (a ## l))
[PROOF STEP]
by (auto intro: step)
[PROOF STATE]
proof (state)
this:
P (lrev (a ## l))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P (lrev l)

goal (1 subgoal):
 1. P xs
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
P (lrev l)

goal (1 subgoal):
 1. P xs
[PROOF STEP]
using fin l_def
[PROOF STATE]
proof (prove)
using this:
P (lrev l)
xs \<in> A\<^sup>\<star>
l = lrev xs

goal (1 subgoal):
 1. P xs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P xs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finlsts_rev_cases:
  assumes tfin: "t \<in> A\<^sup>\<star>"
  obtains (LNil) "t = LNil"
    |    (snocl) a l where "l \<in> A\<^sup>\<star>" "a \<in> A" "t = l @@ a ## LNil"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t = LNil \<Longrightarrow> thesis; \<And>l a. \<lbrakk>l \<in> A\<^sup>\<star>; a \<in> A; t = l @@ a ## LNil\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
t \<in> A\<^sup>\<star>

goal (1 subgoal):
 1. \<lbrakk>t = LNil \<Longrightarrow> thesis; \<And>l a. \<lbrakk>l \<in> A\<^sup>\<star>; a \<in> A; t = l @@ a ## LNil\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (induct rule: lrev_induct) auto


[STATEMENT]
lemma ll2f_LNil [simp]: "LNil!!x = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LNil !! x = None
[PROOF STEP]
by (cases "x") auto


[STATEMENT]
lemma None_lfinite: "t!!i = None \<Longrightarrow> t \<in> UNIV\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t !! i = None \<Longrightarrow> t \<in> UNIV\<^sup>\<star>
[PROOF STEP]
proof (induct "i" arbitrary: t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>t. t !! 0 = None \<Longrightarrow> t \<in> UNIV\<^sup>\<star>
 2. \<And>i t. \<lbrakk>\<And>t. t !! i = None \<Longrightarrow> t \<in> UNIV\<^sup>\<star>; t !! Suc i = None\<rbrakk> \<Longrightarrow> t \<in> UNIV\<^sup>\<star>
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
t !! 0 = None

goal (2 subgoals):
 1. \<And>t. t !! 0 = None \<Longrightarrow> t \<in> UNIV\<^sup>\<star>
 2. \<And>i t. \<lbrakk>\<And>t. t !! i = None \<Longrightarrow> t \<in> UNIV\<^sup>\<star>; t !! Suc i = None\<rbrakk> \<Longrightarrow> t \<in> UNIV\<^sup>\<star>
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
t !! 0 = None

goal (1 subgoal):
 1. t \<in> UNIV\<^sup>\<star>
[PROOF STEP]
by(cases t) auto
[PROOF STATE]
proof (state)
this:
t \<in> UNIV\<^sup>\<star>

goal (1 subgoal):
 1. \<And>i t. \<lbrakk>\<And>t. t !! i = None \<Longrightarrow> t \<in> UNIV\<^sup>\<star>; t !! Suc i = None\<rbrakk> \<Longrightarrow> t \<in> UNIV\<^sup>\<star>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i t. \<lbrakk>\<And>t. t !! i = None \<Longrightarrow> t \<in> UNIV\<^sup>\<star>; t !! Suc i = None\<rbrakk> \<Longrightarrow> t \<in> UNIV\<^sup>\<star>
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
?t !! n = None \<Longrightarrow> ?t \<in> UNIV\<^sup>\<star>
t !! Suc n = None

goal (1 subgoal):
 1. \<And>i t. \<lbrakk>\<And>t. t !! i = None \<Longrightarrow> t \<in> UNIV\<^sup>\<star>; t !! Suc i = None\<rbrakk> \<Longrightarrow> t \<in> UNIV\<^sup>\<star>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> UNIV\<^sup>\<star>
[PROOF STEP]
proof(cases t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. t = LNil \<Longrightarrow> t \<in> UNIV\<^sup>\<star>
 2. \<And>x21 x22. t = x21 ## x22 \<Longrightarrow> t \<in> UNIV\<^sup>\<star>
[PROOF STEP]
case LNil
[PROOF STATE]
proof (state)
this:
t = LNil

goal (2 subgoals):
 1. t = LNil \<Longrightarrow> t \<in> UNIV\<^sup>\<star>
 2. \<And>x21 x22. t = x21 ## x22 \<Longrightarrow> t \<in> UNIV\<^sup>\<star>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
t = LNil

goal (1 subgoal):
 1. t \<in> UNIV\<^sup>\<star>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t \<in> UNIV\<^sup>\<star>

goal (1 subgoal):
 1. \<And>x21 x22. t = x21 ## x22 \<Longrightarrow> t \<in> UNIV\<^sup>\<star>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x21 x22. t = x21 ## x22 \<Longrightarrow> t \<in> UNIV\<^sup>\<star>
[PROOF STEP]
case (LCons x l')
[PROOF STATE]
proof (state)
this:
t = x ## l'

goal (1 subgoal):
 1. \<And>x21 x22. t = x21 ## x22 \<Longrightarrow> t \<in> UNIV\<^sup>\<star>
[PROOF STEP]
with \<open>l' !! n = None \<Longrightarrow> l' \<in> UNIV\<^sup>\<star>\<close> \<open>t !! Suc n = None\<close>
[PROOF STATE]
proof (chain)
picking this:
l' !! n = None \<Longrightarrow> l' \<in> UNIV\<^sup>\<star>
t !! Suc n = None
t = x ## l'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
l' !! n = None \<Longrightarrow> l' \<in> UNIV\<^sup>\<star>
t !! Suc n = None
t = x ## l'

goal (1 subgoal):
 1. t \<in> UNIV\<^sup>\<star>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t \<in> UNIV\<^sup>\<star>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
t \<in> UNIV\<^sup>\<star>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma infinite_Some: "t \<in> A\<^sup>\<omega> \<Longrightarrow> \<exists>a. t!!i = Some a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> A\<^sup>\<omega> \<Longrightarrow> \<exists>a. t !! i = Some a
[PROOF STEP]
by (rule ccontr) (auto dest: None_lfinite)


[STATEMENT]
lemma Least_True [simp]:
  "(LEAST (n::nat). True) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST n. True) = 0
[PROOF STEP]
by (auto simp: Least_def)


[STATEMENT]
lemma  ll2f_llength [simp]: "r \<in> A\<^sup>\<star> \<Longrightarrow> r!!(llength r) = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<in> A\<^sup>\<star> \<Longrightarrow> r !! LList2.llength r = None
[PROOF STEP]
by (erule finlsts.induct) auto


[STATEMENT]
lemma llength_least_None:
  assumes rA: "r \<in> A\<^sup>\<star>"
  shows "llength r = (LEAST i. r!!i = None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LList2.llength r = (LEAST i. r !! i = None)
[PROOF STEP]
using rA
[PROOF STATE]
proof (prove)
using this:
r \<in> A\<^sup>\<star>

goal (1 subgoal):
 1. LList2.llength r = (LEAST i. r !! i = None)
[PROOF STEP]
proof induct
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>l. l = LNil \<Longrightarrow> LList2.llength l = (LEAST i. l !! i = None)
 2. \<And>a l. \<lbrakk>l \<in> A\<^sup>\<star>; LList2.llength l = (LEAST i. l !! i = None); a \<in> A\<rbrakk> \<Longrightarrow> LList2.llength (a ## l) = (LEAST i. (a ## l) !! i = None)
[PROOF STEP]
case LNil_fin
[PROOF STATE]
proof (state)
this:
l_ = LNil

goal (2 subgoals):
 1. \<And>l. l = LNil \<Longrightarrow> LList2.llength l = (LEAST i. l !! i = None)
 2. \<And>a l. \<lbrakk>l \<in> A\<^sup>\<star>; LList2.llength l = (LEAST i. l !! i = None); a \<in> A\<rbrakk> \<Longrightarrow> LList2.llength (a ## l) = (LEAST i. (a ## l) !! i = None)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
l_ = LNil

goal (1 subgoal):
 1. LList2.llength l_ = (LEAST i. l_ !! i = None)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
LList2.llength l_ = (LEAST i. l_ !! i = None)

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>l \<in> A\<^sup>\<star>; LList2.llength l = (LEAST i. l !! i = None); a \<in> A\<rbrakk> \<Longrightarrow> LList2.llength (a ## l) = (LEAST i. (a ## l) !! i = None)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a l. \<lbrakk>l \<in> A\<^sup>\<star>; LList2.llength l = (LEAST i. l !! i = None); a \<in> A\<rbrakk> \<Longrightarrow> LList2.llength (a ## l) = (LEAST i. (a ## l) !! i = None)
[PROOF STEP]
case (LCons_fin a l)
[PROOF STATE]
proof (state)
this:
l \<in> A\<^sup>\<star>
LList2.llength l = (LEAST i. l !! i = None)
a \<in> A

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>l \<in> A\<^sup>\<star>; LList2.llength l = (LEAST i. l !! i = None); a \<in> A\<rbrakk> \<Longrightarrow> LList2.llength (a ## l) = (LEAST i. (a ## l) !! i = None)
[PROOF STEP]
hence "(LEAST i. (a ## l) !! i = None) = llength (a ## l)"
[PROOF STATE]
proof (prove)
using this:
l \<in> A\<^sup>\<star>
LList2.llength l = (LEAST i. l !! i = None)
a \<in> A

goal (1 subgoal):
 1. (LEAST i. (a ## l) !! i = None) = LList2.llength (a ## l)
[PROOF STEP]
by (auto intro!: ll2f_llength Least_Suc2)
[PROOF STATE]
proof (state)
this:
(LEAST i. (a ## l) !! i = None) = LList2.llength (a ## l)

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>l \<in> A\<^sup>\<star>; LList2.llength l = (LEAST i. l !! i = None); a \<in> A\<rbrakk> \<Longrightarrow> LList2.llength (a ## l) = (LEAST i. (a ## l) !! i = None)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(LEAST i. (a ## l) !! i = None) = LList2.llength (a ## l)

goal (1 subgoal):
 1. LList2.llength (a ## l) = (LEAST i. (a ## l) !! i = None)
[PROOF STEP]
by rule
[PROOF STATE]
proof (state)
this:
LList2.llength (a ## l) = (LEAST i. (a ## l) !! i = None)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ll2f_lem1:
 "t !! (Suc i) = Some x \<Longrightarrow> \<exists> y. t !! i = Some y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t !! Suc i = Some x \<Longrightarrow> \<exists>y. t !! i = Some y
[PROOF STEP]
proof (induct i arbitrary: x t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x t. t !! Suc 0 = Some x \<Longrightarrow> \<exists>y. t !! 0 = Some y
 2. \<And>i x t. \<lbrakk>\<And>x t. t !! Suc i = Some x \<Longrightarrow> \<exists>y. t !! i = Some y; t !! Suc (Suc i) = Some x\<rbrakk> \<Longrightarrow> \<exists>y. t !! Suc i = Some y
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
t !! Suc 0 = Some x

goal (2 subgoals):
 1. \<And>x t. t !! Suc 0 = Some x \<Longrightarrow> \<exists>y. t !! 0 = Some y
 2. \<And>i x t. \<lbrakk>\<And>x t. t !! Suc i = Some x \<Longrightarrow> \<exists>y. t !! i = Some y; t !! Suc (Suc i) = Some x\<rbrakk> \<Longrightarrow> \<exists>y. t !! Suc i = Some y
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
t !! Suc 0 = Some x

goal (1 subgoal):
 1. \<exists>y. t !! 0 = Some y
[PROOF STEP]
by (auto split: llist.splits)
[PROOF STATE]
proof (state)
this:
\<exists>y. t !! 0 = Some y

goal (1 subgoal):
 1. \<And>i x t. \<lbrakk>\<And>x t. t !! Suc i = Some x \<Longrightarrow> \<exists>y. t !! i = Some y; t !! Suc (Suc i) = Some x\<rbrakk> \<Longrightarrow> \<exists>y. t !! Suc i = Some y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i x t. \<lbrakk>\<And>x t. t !! Suc i = Some x \<Longrightarrow> \<exists>y. t !! i = Some y; t !! Suc (Suc i) = Some x\<rbrakk> \<Longrightarrow> \<exists>y. t !! Suc i = Some y
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
?t !! Suc k = Some ?x \<Longrightarrow> \<exists>y. ?t !! k = Some y
t !! Suc (Suc k) = Some x

goal (1 subgoal):
 1. \<And>i x t. \<lbrakk>\<And>x t. t !! Suc i = Some x \<Longrightarrow> \<exists>y. t !! i = Some y; t !! Suc (Suc i) = Some x\<rbrakk> \<Longrightarrow> \<exists>y. t !! Suc i = Some y
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
?t !! Suc k = Some ?x \<Longrightarrow> \<exists>y. ?t !! k = Some y
t !! Suc (Suc k) = Some x

goal (1 subgoal):
 1. \<exists>y. t !! Suc k = Some y
[PROOF STEP]
by (cases t) auto
[PROOF STATE]
proof (state)
this:
\<exists>y. t !! Suc k = Some y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ll2f_None_Suc: "t !! i = None \<Longrightarrow> t !! Suc i = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t !! i = None \<Longrightarrow> t !! Suc i = None
[PROOF STEP]
proof (induct i arbitrary: t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>t. t !! 0 = None \<Longrightarrow> t !! Suc 0 = None
 2. \<And>i t. \<lbrakk>\<And>t. t !! i = None \<Longrightarrow> t !! Suc i = None; t !! Suc i = None\<rbrakk> \<Longrightarrow> t !! Suc (Suc i) = None
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
t !! 0 = None

goal (2 subgoals):
 1. \<And>t. t !! 0 = None \<Longrightarrow> t !! Suc 0 = None
 2. \<And>i t. \<lbrakk>\<And>t. t !! i = None \<Longrightarrow> t !! Suc i = None; t !! Suc i = None\<rbrakk> \<Longrightarrow> t !! Suc (Suc i) = None
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
t !! 0 = None

goal (1 subgoal):
 1. t !! Suc 0 = None
[PROOF STEP]
by (auto split: llist.split)
[PROOF STATE]
proof (state)
this:
t !! Suc 0 = None

goal (1 subgoal):
 1. \<And>i t. \<lbrakk>\<And>t. t !! i = None \<Longrightarrow> t !! Suc i = None; t !! Suc i = None\<rbrakk> \<Longrightarrow> t !! Suc (Suc i) = None
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i t. \<lbrakk>\<And>t. t !! i = None \<Longrightarrow> t !! Suc i = None; t !! Suc i = None\<rbrakk> \<Longrightarrow> t !! Suc (Suc i) = None
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
?t !! k = None \<Longrightarrow> ?t !! Suc k = None
t !! Suc k = None

goal (1 subgoal):
 1. \<And>i t. \<lbrakk>\<And>t. t !! i = None \<Longrightarrow> t !! Suc i = None; t !! Suc i = None\<rbrakk> \<Longrightarrow> t !! Suc (Suc i) = None
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
?t !! k = None \<Longrightarrow> ?t !! Suc k = None
t !! Suc k = None

goal (1 subgoal):
 1. t !! Suc (Suc k) = None
[PROOF STEP]
by (cases t) auto
[PROOF STATE]
proof (state)
this:
t !! Suc (Suc k) = None

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ll2f_None_le:
  "\<lbrakk> t!!j = None; j \<le> i \<rbrakk> \<Longrightarrow> t!!i = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t !! j = None; j \<le> i\<rbrakk> \<Longrightarrow> t !! i = None
[PROOF STEP]
proof (induct i arbitrary: t j)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>t j. \<lbrakk>t !! j = None; j \<le> 0\<rbrakk> \<Longrightarrow> t !! 0 = None
 2. \<And>i t j. \<lbrakk>\<And>t j. \<lbrakk>t !! j = None; j \<le> i\<rbrakk> \<Longrightarrow> t !! i = None; t !! j = None; j \<le> Suc i\<rbrakk> \<Longrightarrow> t !! Suc i = None
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
t !! j = None
j \<le> 0

goal (2 subgoals):
 1. \<And>t j. \<lbrakk>t !! j = None; j \<le> 0\<rbrakk> \<Longrightarrow> t !! 0 = None
 2. \<And>i t j. \<lbrakk>\<And>t j. \<lbrakk>t !! j = None; j \<le> i\<rbrakk> \<Longrightarrow> t !! i = None; t !! j = None; j \<le> Suc i\<rbrakk> \<Longrightarrow> t !! Suc i = None
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
t !! j = None
j \<le> 0

goal (1 subgoal):
 1. t !! 0 = None
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
t !! 0 = None

goal (1 subgoal):
 1. \<And>i t j. \<lbrakk>\<And>t j. \<lbrakk>t !! j = None; j \<le> i\<rbrakk> \<Longrightarrow> t !! i = None; t !! j = None; j \<le> Suc i\<rbrakk> \<Longrightarrow> t !! Suc i = None
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i t j. \<lbrakk>\<And>t j. \<lbrakk>t !! j = None; j \<le> i\<rbrakk> \<Longrightarrow> t !! i = None; t !! j = None; j \<le> Suc i\<rbrakk> \<Longrightarrow> t !! Suc i = None
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?t !! ?j = None; ?j \<le> k\<rbrakk> \<Longrightarrow> ?t !! k = None
t !! j = None
j \<le> Suc k

goal (1 subgoal):
 1. \<And>i t j. \<lbrakk>\<And>t j. \<lbrakk>t !! j = None; j \<le> i\<rbrakk> \<Longrightarrow> t !! i = None; t !! j = None; j \<le> Suc i\<rbrakk> \<Longrightarrow> t !! Suc i = None
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?t !! ?j = None; ?j \<le> k\<rbrakk> \<Longrightarrow> ?t !! k = None
t !! j = None
j \<le> Suc k

goal (1 subgoal):
 1. t !! Suc k = None
[PROOF STEP]
by (cases j) (auto split: llist.split)
[PROOF STATE]
proof (state)
this:
t !! Suc k = None

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ll2f_Some_le:
  assumes jlei: "j \<le> i"
  and tisome: "t !! i = Some x"
  and H: "\<And> y. t !! j = Some y \<Longrightarrow> Q"
  shows "Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Q
[PROOF STEP]
have  "\<exists> y. t !! j = Some y" (is "?R")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y. t !! j = Some y
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>y. t !! j = Some y \<Longrightarrow> False
[PROOF STEP]
assume "\<not> ?R"
[PROOF STATE]
proof (state)
this:
\<nexists>y. t !! j = Some y

goal (1 subgoal):
 1. \<nexists>y. t !! j = Some y \<Longrightarrow> False
[PROOF STEP]
hence "t !! j = None"
[PROOF STATE]
proof (prove)
using this:
\<nexists>y. t !! j = Some y

goal (1 subgoal):
 1. t !! j = None
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t !! j = None

goal (1 subgoal):
 1. \<nexists>y. t !! j = Some y \<Longrightarrow> False
[PROOF STEP]
with tisome jlei
[PROOF STATE]
proof (chain)
picking this:
t !! i = Some x
j \<le> i
t !! j = None
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
t !! i = Some x
j \<le> i
t !! j = None

goal (1 subgoal):
 1. False
[PROOF STEP]
by (auto dest:  ll2f_None_le)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>y. t !! j = Some y

goal (1 subgoal):
 1. Q
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>y. t !! j = Some y

goal (1 subgoal):
 1. Q
[PROOF STEP]
using H
[PROOF STATE]
proof (prove)
using this:
\<exists>y. t !! j = Some y
t !! j = Some ?y \<Longrightarrow> Q

goal (1 subgoal):
 1. Q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ltake_LNil [simp]: "LNil \<down> i = LNil"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LNil \<down> i = LNil
[PROOF STEP]
by (cases "i") auto


[STATEMENT]
lemma ltake_LCons_Suc: "(a ## l) \<down> (Suc i) = a ## l \<down> i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a ## l) \<down> Suc i = a ## l \<down> i
[PROOF STEP]
by simp


[STATEMENT]
lemma take_fin [iff]: "t \<in> A\<^sup>\<infinity> \<Longrightarrow> t\<down>i \<in> A\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> A\<^sup>\<infinity> \<Longrightarrow> t \<down> i \<in> A\<^sup>\<star>
[PROOF STEP]
proof (induct i arbitrary: t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>t. t \<in> A\<^sup>\<infinity> \<Longrightarrow> t \<down> 0 \<in> A\<^sup>\<star>
 2. \<And>i t. \<lbrakk>\<And>t. t \<in> A\<^sup>\<infinity> \<Longrightarrow> t \<down> i \<in> A\<^sup>\<star>; t \<in> A\<^sup>\<infinity>\<rbrakk> \<Longrightarrow> t \<down> Suc i \<in> A\<^sup>\<star>
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
t \<in> A\<^sup>\<infinity>

goal (2 subgoals):
 1. \<And>t. t \<in> A\<^sup>\<infinity> \<Longrightarrow> t \<down> 0 \<in> A\<^sup>\<star>
 2. \<And>i t. \<lbrakk>\<And>t. t \<in> A\<^sup>\<infinity> \<Longrightarrow> t \<down> i \<in> A\<^sup>\<star>; t \<in> A\<^sup>\<infinity>\<rbrakk> \<Longrightarrow> t \<down> Suc i \<in> A\<^sup>\<star>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<down> 0 \<in> A\<^sup>\<star>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t \<down> 0 \<in> A\<^sup>\<star>

goal (1 subgoal):
 1. \<And>i t. \<lbrakk>\<And>t. t \<in> A\<^sup>\<infinity> \<Longrightarrow> t \<down> i \<in> A\<^sup>\<star>; t \<in> A\<^sup>\<infinity>\<rbrakk> \<Longrightarrow> t \<down> Suc i \<in> A\<^sup>\<star>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i t. \<lbrakk>\<And>t. t \<in> A\<^sup>\<infinity> \<Longrightarrow> t \<down> i \<in> A\<^sup>\<star>; t \<in> A\<^sup>\<infinity>\<rbrakk> \<Longrightarrow> t \<down> Suc i \<in> A\<^sup>\<star>
[PROOF STEP]
case (Suc j)
[PROOF STATE]
proof (state)
this:
?t \<in> A\<^sup>\<infinity> \<Longrightarrow> ?t \<down> j \<in> A\<^sup>\<star>
t \<in> A\<^sup>\<infinity>

goal (1 subgoal):
 1. \<And>i t. \<lbrakk>\<And>t. t \<in> A\<^sup>\<infinity> \<Longrightarrow> t \<down> i \<in> A\<^sup>\<star>; t \<in> A\<^sup>\<infinity>\<rbrakk> \<Longrightarrow> t \<down> Suc i \<in> A\<^sup>\<star>
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
?t \<in> A\<^sup>\<infinity> \<Longrightarrow> ?t \<down> j \<in> A\<^sup>\<star>
t \<in> A\<^sup>\<infinity>

goal (1 subgoal):
 1. t \<down> Suc j \<in> A\<^sup>\<star>
[PROOF STEP]
by (cases "t") auto
[PROOF STATE]
proof (state)
this:
t \<down> Suc j \<in> A\<^sup>\<star>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ltake_fin [iff]:
  "r \<down> i \<in> UNIV\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<down> i \<in> UNIV\<^sup>\<star>
[PROOF STEP]
by simp


[STATEMENT]
lemma llength_take [simp]: "t \<in> A\<^sup>\<omega> \<Longrightarrow> llength (t\<down>i) = i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> A\<^sup>\<omega> \<Longrightarrow> LList2.llength (t \<down> i) = i
[PROOF STEP]
proof (induct "i" arbitrary: t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>t. t \<in> A\<^sup>\<omega> \<Longrightarrow> LList2.llength (t \<down> 0) = 0
 2. \<And>i t. \<lbrakk>\<And>t. t \<in> A\<^sup>\<omega> \<Longrightarrow> LList2.llength (t \<down> i) = i; t \<in> A\<^sup>\<omega>\<rbrakk> \<Longrightarrow> LList2.llength (t \<down> Suc i) = Suc i
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
t \<in> A\<^sup>\<omega>

goal (2 subgoals):
 1. \<And>t. t \<in> A\<^sup>\<omega> \<Longrightarrow> LList2.llength (t \<down> 0) = 0
 2. \<And>i t. \<lbrakk>\<And>t. t \<in> A\<^sup>\<omega> \<Longrightarrow> LList2.llength (t \<down> i) = i; t \<in> A\<^sup>\<omega>\<rbrakk> \<Longrightarrow> LList2.llength (t \<down> Suc i) = Suc i
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
t \<in> A\<^sup>\<omega>

goal (1 subgoal):
 1. LList2.llength (t \<down> 0) = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
LList2.llength (t \<down> 0) = 0

goal (1 subgoal):
 1. \<And>i t. \<lbrakk>\<And>t. t \<in> A\<^sup>\<omega> \<Longrightarrow> LList2.llength (t \<down> i) = i; t \<in> A\<^sup>\<omega>\<rbrakk> \<Longrightarrow> LList2.llength (t \<down> Suc i) = Suc i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i t. \<lbrakk>\<And>t. t \<in> A\<^sup>\<omega> \<Longrightarrow> LList2.llength (t \<down> i) = i; t \<in> A\<^sup>\<omega>\<rbrakk> \<Longrightarrow> LList2.llength (t \<down> Suc i) = Suc i
[PROOF STEP]
case (Suc j)
[PROOF STATE]
proof (state)
this:
?t \<in> A\<^sup>\<omega> \<Longrightarrow> LList2.llength (?t \<down> j) = j
t \<in> A\<^sup>\<omega>

goal (1 subgoal):
 1. \<And>i t. \<lbrakk>\<And>t. t \<in> A\<^sup>\<omega> \<Longrightarrow> LList2.llength (t \<down> i) = i; t \<in> A\<^sup>\<omega>\<rbrakk> \<Longrightarrow> LList2.llength (t \<down> Suc i) = Suc i
[PROOF STEP]
from \<open>t \<in> A\<^sup>\<omega>\<close> \<open>\<And>t. t \<in> A\<^sup>\<omega> \<Longrightarrow> llength (t \<down> j) = j\<close>
[PROOF STATE]
proof (chain)
picking this:
t \<in> A\<^sup>\<omega>
?t \<in> A\<^sup>\<omega> \<Longrightarrow> LList2.llength (?t \<down> j) = j
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
t \<in> A\<^sup>\<omega>
?t \<in> A\<^sup>\<omega> \<Longrightarrow> LList2.llength (?t \<down> j) = j

goal (1 subgoal):
 1. LList2.llength (t \<down> Suc j) = Suc j
[PROOF STEP]
by(cases) (auto simp: llength_LCons [of _ UNIV])
[PROOF STATE]
proof (state)
this:
LList2.llength (t \<down> Suc j) = Suc j

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ltake_ldrop_id: "(x \<down> i) @@ (x \<up> i) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<down> i @@ x \<up> i = x
[PROOF STEP]
proof (induct "i" arbitrary: x)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<down> 0 @@ x \<up> 0 = x
 2. \<And>i x. (\<And>x. x \<down> i @@ x \<up> i = x) \<Longrightarrow> x \<down> Suc i @@ x \<up> Suc i = x
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>x. x \<down> 0 @@ x \<up> 0 = x
 2. \<And>i x. (\<And>x. x \<down> i @@ x \<up> i = x) \<Longrightarrow> x \<down> Suc i @@ x \<up> Suc i = x
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<down> 0 @@ x \<up> 0 = x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<down> 0 @@ x \<up> 0 = x

goal (1 subgoal):
 1. \<And>i x. (\<And>x. x \<down> i @@ x \<up> i = x) \<Longrightarrow> x \<down> Suc i @@ x \<up> Suc i = x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i x. (\<And>x. x \<down> i @@ x \<up> i = x) \<Longrightarrow> x \<down> Suc i @@ x \<up> Suc i = x
[PROOF STEP]
case (Suc j)
[PROOF STATE]
proof (state)
this:
?x \<down> j @@ ?x \<up> j = ?x

goal (1 subgoal):
 1. \<And>i x. (\<And>x. x \<down> i @@ x \<up> i = x) \<Longrightarrow> x \<down> Suc i @@ x \<up> Suc i = x
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
?x \<down> j @@ ?x \<up> j = ?x

goal (1 subgoal):
 1. x \<down> Suc j @@ x \<up> Suc j = x
[PROOF STEP]
by (cases x) auto
[PROOF STATE]
proof (state)
this:
x \<down> Suc j @@ x \<up> Suc j = x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ltake_ldrop:
  "(xs \<up> m) \<down> n =(xs \<down> (n + m)) \<up> m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<up> m \<down> n = xs \<down> (n + m) \<up> m
[PROOF STEP]
proof (induct "m" arbitrary: xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xs. xs \<up> 0 \<down> n = xs \<down> (n + 0) \<up> 0
 2. \<And>m xs. (\<And>xs. xs \<up> m \<down> n = xs \<down> (n + m) \<up> m) \<Longrightarrow> xs \<up> Suc m \<down> n = xs \<down> (n + Suc m) \<up> Suc m
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>xs. xs \<up> 0 \<down> n = xs \<down> (n + 0) \<up> 0
 2. \<And>m xs. (\<And>xs. xs \<up> m \<down> n = xs \<down> (n + m) \<up> m) \<Longrightarrow> xs \<up> Suc m \<down> n = xs \<down> (n + Suc m) \<up> Suc m
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<up> 0 \<down> n = xs \<down> (n + 0) \<up> 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
xs \<up> 0 \<down> n = xs \<down> (n + 0) \<up> 0

goal (1 subgoal):
 1. \<And>m xs. (\<And>xs. xs \<up> m \<down> n = xs \<down> (n + m) \<up> m) \<Longrightarrow> xs \<up> Suc m \<down> n = xs \<down> (n + Suc m) \<up> Suc m
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m xs. (\<And>xs. xs \<up> m \<down> n = xs \<down> (n + m) \<up> m) \<Longrightarrow> xs \<up> Suc m \<down> n = xs \<down> (n + Suc m) \<up> Suc m
[PROOF STEP]
case (Suc l)
[PROOF STATE]
proof (state)
this:
?xs \<up> l \<down> n = ?xs \<down> (n + l) \<up> l

goal (1 subgoal):
 1. \<And>m xs. (\<And>xs. xs \<up> m \<down> n = xs \<down> (n + m) \<up> m) \<Longrightarrow> xs \<up> Suc m \<down> n = xs \<down> (n + Suc m) \<up> Suc m
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
?xs \<up> l \<down> n = ?xs \<down> (n + l) \<up> l

goal (1 subgoal):
 1. xs \<up> Suc l \<down> n = xs \<down> (n + Suc l) \<up> Suc l
[PROOF STEP]
by (cases "xs") auto
[PROOF STATE]
proof (state)
this:
xs \<up> Suc l \<down> n = xs \<down> (n + Suc l) \<up> Suc l

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ldrop_LNil [simp]: "LNil \<up> i = LNil"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LNil \<up> i = LNil
[PROOF STEP]
by (cases "i") auto


[STATEMENT]
lemma ldrop_add: "t \<up> (i + k) = t \<up> i \<up> k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<up> (i + k) = t \<up> i \<up> k
[PROOF STEP]
proof (induct "i" arbitrary: t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>t. t \<up> (0 + k) = t \<up> 0 \<up> k
 2. \<And>i t. (\<And>t. t \<up> (i + k) = t \<up> i \<up> k) \<Longrightarrow> t \<up> (Suc i + k) = t \<up> Suc i \<up> k
[PROOF STEP]
case (Suc j)
[PROOF STATE]
proof (state)
this:
?t \<up> (j + k) = ?t \<up> j \<up> k

goal (2 subgoals):
 1. \<And>t. t \<up> (0 + k) = t \<up> 0 \<up> k
 2. \<And>i t. (\<And>t. t \<up> (i + k) = t \<up> i \<up> k) \<Longrightarrow> t \<up> (Suc i + k) = t \<up> Suc i \<up> k
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
?t \<up> (j + k) = ?t \<up> j \<up> k

goal (1 subgoal):
 1. t \<up> (Suc j + k) = t \<up> Suc j \<up> k
[PROOF STEP]
by (cases "t") auto
[PROOF STATE]
proof (state)
this:
t \<up> (Suc j + k) = t \<up> Suc j \<up> k

goal (1 subgoal):
 1. \<And>t. t \<up> (0 + k) = t \<up> 0 \<up> k
[PROOF STEP]
qed simp


[STATEMENT]
lemma ldrop_fun: "t \<up> i !! j = t!!(i + j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<up> i !! j = t !! (i + j)
[PROOF STEP]
proof (induct i arbitrary: t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>t. t \<up> 0 !! j = t !! (0 + j)
 2. \<And>i t. (\<And>t. t \<up> i !! j = t !! (i + j)) \<Longrightarrow> t \<up> Suc i !! j = t !! (Suc i + j)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>t. t \<up> 0 !! j = t !! (0 + j)
 2. \<And>i t. (\<And>t. t \<up> i !! j = t !! (i + j)) \<Longrightarrow> t \<up> Suc i !! j = t !! (Suc i + j)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<up> 0 !! j = t !! (0 + j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
t \<up> 0 !! j = t !! (0 + j)

goal (1 subgoal):
 1. \<And>i t. (\<And>t. t \<up> i !! j = t !! (i + j)) \<Longrightarrow> t \<up> Suc i !! j = t !! (Suc i + j)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i t. (\<And>t. t \<up> i !! j = t !! (i + j)) \<Longrightarrow> t \<up> Suc i !! j = t !! (Suc i + j)
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
?t \<up> k !! j = ?t !! (k + j)

goal (1 subgoal):
 1. \<And>i t. (\<And>t. t \<up> i !! j = t !! (i + j)) \<Longrightarrow> t \<up> Suc i !! j = t !! (Suc i + j)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?t \<up> k !! j = ?t !! (k + j)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?t \<up> k !! j = ?t !! (k + j)

goal (1 subgoal):
 1. t \<up> Suc k !! j = t !! (Suc k + j)
[PROOF STEP]
by (cases "t") auto
[PROOF STATE]
proof (state)
this:
t \<up> Suc k !! j = t !! (Suc k + j)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ldropT[simp]: "t \<in> A\<^sup>\<infinity> \<Longrightarrow> t \<up> i \<in> A\<^sup>\<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> A\<^sup>\<infinity> \<Longrightarrow> t \<up> i \<in> A\<^sup>\<infinity>
[PROOF STEP]
proof (induct i arbitrary: t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>t. t \<in> A\<^sup>\<infinity> \<Longrightarrow> t \<up> 0 \<in> A\<^sup>\<infinity>
 2. \<And>i t. \<lbrakk>\<And>t. t \<in> A\<^sup>\<infinity> \<Longrightarrow> t \<up> i \<in> A\<^sup>\<infinity>; t \<in> A\<^sup>\<infinity>\<rbrakk> \<Longrightarrow> t \<up> Suc i \<in> A\<^sup>\<infinity>
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
t \<in> A\<^sup>\<infinity>

goal (2 subgoals):
 1. \<And>t. t \<in> A\<^sup>\<infinity> \<Longrightarrow> t \<up> 0 \<in> A\<^sup>\<infinity>
 2. \<And>i t. \<lbrakk>\<And>t. t \<in> A\<^sup>\<infinity> \<Longrightarrow> t \<up> i \<in> A\<^sup>\<infinity>; t \<in> A\<^sup>\<infinity>\<rbrakk> \<Longrightarrow> t \<up> Suc i \<in> A\<^sup>\<infinity>
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
t \<in> A\<^sup>\<infinity>

goal (1 subgoal):
 1. t \<up> 0 \<in> A\<^sup>\<infinity>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
t \<up> 0 \<in> A\<^sup>\<infinity>

goal (1 subgoal):
 1. \<And>i t. \<lbrakk>\<And>t. t \<in> A\<^sup>\<infinity> \<Longrightarrow> t \<up> i \<in> A\<^sup>\<infinity>; t \<in> A\<^sup>\<infinity>\<rbrakk> \<Longrightarrow> t \<up> Suc i \<in> A\<^sup>\<infinity>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i t. \<lbrakk>\<And>t. t \<in> A\<^sup>\<infinity> \<Longrightarrow> t \<up> i \<in> A\<^sup>\<infinity>; t \<in> A\<^sup>\<infinity>\<rbrakk> \<Longrightarrow> t \<up> Suc i \<in> A\<^sup>\<infinity>
[PROOF STEP]
case (Suc j)
[PROOF STATE]
proof (state)
this:
?t \<in> A\<^sup>\<infinity> \<Longrightarrow> ?t \<up> j \<in> A\<^sup>\<infinity>
t \<in> A\<^sup>\<infinity>

goal (1 subgoal):
 1. \<And>i t. \<lbrakk>\<And>t. t \<in> A\<^sup>\<infinity> \<Longrightarrow> t \<up> i \<in> A\<^sup>\<infinity>; t \<in> A\<^sup>\<infinity>\<rbrakk> \<Longrightarrow> t \<up> Suc i \<in> A\<^sup>\<infinity>
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
?t \<in> A\<^sup>\<infinity> \<Longrightarrow> ?t \<up> j \<in> A\<^sup>\<infinity>
t \<in> A\<^sup>\<infinity>

goal (1 subgoal):
 1. t \<up> Suc j \<in> A\<^sup>\<infinity>
[PROOF STEP]
by (cases "t") auto
[PROOF STATE]
proof (state)
this:
t \<up> Suc j \<in> A\<^sup>\<infinity>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ldrop_finT[simp]: "t \<in> A\<^sup>\<star> \<Longrightarrow> t \<up> i \<in> A\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> A\<^sup>\<star> \<Longrightarrow> t \<up> i \<in> A\<^sup>\<star>
[PROOF STEP]
proof (induct i arbitrary: t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>t. t \<in> A\<^sup>\<star> \<Longrightarrow> t \<up> 0 \<in> A\<^sup>\<star>
 2. \<And>i t. \<lbrakk>\<And>t. t \<in> A\<^sup>\<star> \<Longrightarrow> t \<up> i \<in> A\<^sup>\<star>; t \<in> A\<^sup>\<star>\<rbrakk> \<Longrightarrow> t \<up> Suc i \<in> A\<^sup>\<star>
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
t \<in> A\<^sup>\<star>

goal (2 subgoals):
 1. \<And>t. t \<in> A\<^sup>\<star> \<Longrightarrow> t \<up> 0 \<in> A\<^sup>\<star>
 2. \<And>i t. \<lbrakk>\<And>t. t \<in> A\<^sup>\<star> \<Longrightarrow> t \<up> i \<in> A\<^sup>\<star>; t \<in> A\<^sup>\<star>\<rbrakk> \<Longrightarrow> t \<up> Suc i \<in> A\<^sup>\<star>
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
t \<in> A\<^sup>\<star>

goal (1 subgoal):
 1. t \<up> 0 \<in> A\<^sup>\<star>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
t \<up> 0 \<in> A\<^sup>\<star>

goal (1 subgoal):
 1. \<And>i t. \<lbrakk>\<And>t. t \<in> A\<^sup>\<star> \<Longrightarrow> t \<up> i \<in> A\<^sup>\<star>; t \<in> A\<^sup>\<star>\<rbrakk> \<Longrightarrow> t \<up> Suc i \<in> A\<^sup>\<star>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i t. \<lbrakk>\<And>t. t \<in> A\<^sup>\<star> \<Longrightarrow> t \<up> i \<in> A\<^sup>\<star>; t \<in> A\<^sup>\<star>\<rbrakk> \<Longrightarrow> t \<up> Suc i \<in> A\<^sup>\<star>
[PROOF STEP]
fix n t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i t. \<lbrakk>\<And>t. t \<in> A\<^sup>\<star> \<Longrightarrow> t \<up> i \<in> A\<^sup>\<star>; t \<in> A\<^sup>\<star>\<rbrakk> \<Longrightarrow> t \<up> Suc i \<in> A\<^sup>\<star>
[PROOF STEP]
assume "t \<in> A\<^sup>\<star>" and
    "\<And>t::'a llist. t \<in> A\<^sup>\<star> \<Longrightarrow> t \<up> n \<in> A\<^sup>\<star>"
[PROOF STATE]
proof (state)
this:
t \<in> A\<^sup>\<star>
?t \<in> A\<^sup>\<star> \<Longrightarrow> ?t \<up> n \<in> A\<^sup>\<star>

goal (1 subgoal):
 1. \<And>i t. \<lbrakk>\<And>t. t \<in> A\<^sup>\<star> \<Longrightarrow> t \<up> i \<in> A\<^sup>\<star>; t \<in> A\<^sup>\<star>\<rbrakk> \<Longrightarrow> t \<up> Suc i \<in> A\<^sup>\<star>
[PROOF STEP]
thus "t \<up> Suc n \<in> A\<^sup>\<star>"
[PROOF STATE]
proof (prove)
using this:
t \<in> A\<^sup>\<star>
?t \<in> A\<^sup>\<star> \<Longrightarrow> ?t \<up> n \<in> A\<^sup>\<star>

goal (1 subgoal):
 1. t \<up> Suc n \<in> A\<^sup>\<star>
[PROOF STEP]
by (cases "t") auto
[PROOF STATE]
proof (state)
this:
t \<up> Suc n \<in> A\<^sup>\<star>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ldrop_infT[simp]: "t \<in> A\<^sup>\<omega> \<Longrightarrow> t \<up> i \<in> A\<^sup>\<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> A\<^sup>\<omega> \<Longrightarrow> t \<up> i \<in> A\<^sup>\<omega>
[PROOF STEP]
proof (induct i arbitrary: t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>t. t \<in> A\<^sup>\<omega> \<Longrightarrow> t \<up> 0 \<in> A\<^sup>\<omega>
 2. \<And>i t. \<lbrakk>\<And>t. t \<in> A\<^sup>\<omega> \<Longrightarrow> t \<up> i \<in> A\<^sup>\<omega>; t \<in> A\<^sup>\<omega>\<rbrakk> \<Longrightarrow> t \<up> Suc i \<in> A\<^sup>\<omega>
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
t \<in> A\<^sup>\<omega>

goal (2 subgoals):
 1. \<And>t. t \<in> A\<^sup>\<omega> \<Longrightarrow> t \<up> 0 \<in> A\<^sup>\<omega>
 2. \<And>i t. \<lbrakk>\<And>t. t \<in> A\<^sup>\<omega> \<Longrightarrow> t \<up> i \<in> A\<^sup>\<omega>; t \<in> A\<^sup>\<omega>\<rbrakk> \<Longrightarrow> t \<up> Suc i \<in> A\<^sup>\<omega>
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
t \<in> A\<^sup>\<omega>

goal (1 subgoal):
 1. t \<up> 0 \<in> A\<^sup>\<omega>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
t \<up> 0 \<in> A\<^sup>\<omega>

goal (1 subgoal):
 1. \<And>i t. \<lbrakk>\<And>t. t \<in> A\<^sup>\<omega> \<Longrightarrow> t \<up> i \<in> A\<^sup>\<omega>; t \<in> A\<^sup>\<omega>\<rbrakk> \<Longrightarrow> t \<up> Suc i \<in> A\<^sup>\<omega>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i t. \<lbrakk>\<And>t. t \<in> A\<^sup>\<omega> \<Longrightarrow> t \<up> i \<in> A\<^sup>\<omega>; t \<in> A\<^sup>\<omega>\<rbrakk> \<Longrightarrow> t \<up> Suc i \<in> A\<^sup>\<omega>
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
?t \<in> A\<^sup>\<omega> \<Longrightarrow> ?t \<up> n \<in> A\<^sup>\<omega>
t \<in> A\<^sup>\<omega>

goal (1 subgoal):
 1. \<And>i t. \<lbrakk>\<And>t. t \<in> A\<^sup>\<omega> \<Longrightarrow> t \<up> i \<in> A\<^sup>\<omega>; t \<in> A\<^sup>\<omega>\<rbrakk> \<Longrightarrow> t \<up> Suc i \<in> A\<^sup>\<omega>
[PROOF STEP]
from \<open>t \<in> A\<^sup>\<omega>\<close> \<open>\<And>t. t \<in> A\<^sup>\<omega> \<Longrightarrow> t \<up> n \<in> A\<^sup>\<omega>\<close>
[PROOF STATE]
proof (chain)
picking this:
t \<in> A\<^sup>\<omega>
?t \<in> A\<^sup>\<omega> \<Longrightarrow> ?t \<up> n \<in> A\<^sup>\<omega>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
t \<in> A\<^sup>\<omega>
?t \<in> A\<^sup>\<omega> \<Longrightarrow> ?t \<up> n \<in> A\<^sup>\<omega>

goal (1 subgoal):
 1. t \<up> Suc n \<in> A\<^sup>\<omega>
[PROOF STEP]
by (cases "t") auto
[PROOF STATE]
proof (state)
this:
t \<up> Suc n \<in> A\<^sup>\<omega>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lapp_suff_llength: "r \<in> A\<^sup>\<star> \<Longrightarrow> (r@@s) \<up> llength r = s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<in> A\<^sup>\<star> \<Longrightarrow> (r @@ s) \<up> LList2.llength r = s
[PROOF STEP]
by (induct rule: finlsts.induct) auto


[STATEMENT]
lemma ltake_lappend_llength [simp]:
  "r \<in> A\<^sup>\<star> \<Longrightarrow> (r @@ s) \<down> llength r = r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<in> A\<^sup>\<star> \<Longrightarrow> (r @@ s) \<down> LList2.llength r = r
[PROOF STEP]
by (induct rule: finlsts.induct) auto


[STATEMENT]
lemma ldrop_LNil_less:
  "\<lbrakk>j \<le> i; t \<up> j = LNil\<rbrakk> \<Longrightarrow> t \<up> i = LNil"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>j \<le> i; t \<up> j = LNil\<rbrakk> \<Longrightarrow> t \<up> i = LNil
[PROOF STEP]
proof (induct i arbitrary: j t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>j t. \<lbrakk>j \<le> 0; t \<up> j = LNil\<rbrakk> \<Longrightarrow> t \<up> 0 = LNil
 2. \<And>i j t. \<lbrakk>\<And>j t. \<lbrakk>j \<le> i; t \<up> j = LNil\<rbrakk> \<Longrightarrow> t \<up> i = LNil; j \<le> Suc i; t \<up> j = LNil\<rbrakk> \<Longrightarrow> t \<up> Suc i = LNil
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
j \<le> 0
t \<up> j = LNil

goal (2 subgoals):
 1. \<And>j t. \<lbrakk>j \<le> 0; t \<up> j = LNil\<rbrakk> \<Longrightarrow> t \<up> 0 = LNil
 2. \<And>i j t. \<lbrakk>\<And>j t. \<lbrakk>j \<le> i; t \<up> j = LNil\<rbrakk> \<Longrightarrow> t \<up> i = LNil; j \<le> Suc i; t \<up> j = LNil\<rbrakk> \<Longrightarrow> t \<up> Suc i = LNil
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
j \<le> 0
t \<up> j = LNil

goal (1 subgoal):
 1. t \<up> 0 = LNil
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t \<up> 0 = LNil

goal (1 subgoal):
 1. \<And>i j t. \<lbrakk>\<And>j t. \<lbrakk>j \<le> i; t \<up> j = LNil\<rbrakk> \<Longrightarrow> t \<up> i = LNil; j \<le> Suc i; t \<up> j = LNil\<rbrakk> \<Longrightarrow> t \<up> Suc i = LNil
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j t. \<lbrakk>\<And>j t. \<lbrakk>j \<le> i; t \<up> j = LNil\<rbrakk> \<Longrightarrow> t \<up> i = LNil; j \<le> Suc i; t \<up> j = LNil\<rbrakk> \<Longrightarrow> t \<up> Suc i = LNil
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?j \<le> n; ?t \<up> ?j = LNil\<rbrakk> \<Longrightarrow> ?t \<up> n = LNil
j \<le> Suc n
t \<up> j = LNil

goal (1 subgoal):
 1. \<And>i j t. \<lbrakk>\<And>j t. \<lbrakk>j \<le> i; t \<up> j = LNil\<rbrakk> \<Longrightarrow> t \<up> i = LNil; j \<le> Suc i; t \<up> j = LNil\<rbrakk> \<Longrightarrow> t \<up> Suc i = LNil
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?j \<le> n; ?t \<up> ?j = LNil\<rbrakk> \<Longrightarrow> ?t \<up> n = LNil
j \<le> Suc n
t \<up> j = LNil

goal (1 subgoal):
 1. t \<up> Suc n = LNil
[PROOF STEP]
by (cases j, simp) (cases t, simp_all)
[PROOF STATE]
proof (state)
this:
t \<up> Suc n = LNil

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ldrop_inf_iffT [iff]: "(t \<up> i \<in> UNIV\<^sup>\<omega>)  =  (t \<in> UNIV\<^sup>\<omega>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (t \<up> i \<in> UNIV\<^sup>\<omega>) = (t \<in> UNIV\<^sup>\<omega>)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. t \<up> i \<in> UNIV\<^sup>\<omega> \<Longrightarrow> t \<in> UNIV\<^sup>\<omega>
 2. t \<in> UNIV\<^sup>\<omega> \<Longrightarrow> t \<up> i \<in> UNIV\<^sup>\<omega>
[PROOF STEP]
show "t\<up>i \<in> UNIV\<^sup>\<omega> \<Longrightarrow> t \<in> UNIV\<^sup>\<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<up> i \<in> UNIV\<^sup>\<omega> \<Longrightarrow> t \<in> UNIV\<^sup>\<omega>
[PROOF STEP]
by (rule ccontr) (auto dest: ldrop_finT)
[PROOF STATE]
proof (state)
this:
t \<up> i \<in> UNIV\<^sup>\<omega> \<Longrightarrow> t \<in> UNIV\<^sup>\<omega>

goal (1 subgoal):
 1. t \<in> UNIV\<^sup>\<omega> \<Longrightarrow> t \<up> i \<in> UNIV\<^sup>\<omega>
[PROOF STEP]
qed auto


[STATEMENT]
lemma ldrop_fin_iffT [iff]: "(t \<up> i \<in> UNIV\<^sup>\<star>) = (t \<in> UNIV\<^sup>\<star>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (t \<up> i \<in> UNIV\<^sup>\<star>) = (t \<in> UNIV\<^sup>\<star>)
[PROOF STEP]
by auto


[STATEMENT]
lemma drop_nonLNil: "t\<up>i \<noteq> LNil \<Longrightarrow> t \<noteq> LNil"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<up> i \<noteq> LNil \<Longrightarrow> t \<noteq> LNil
[PROOF STEP]
by (auto)


[STATEMENT]
lemma llength_drop_take:
  "t\<up>i \<noteq> LNil \<Longrightarrow> llength (t\<down>i) = i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<up> i \<noteq> LNil \<Longrightarrow> LList2.llength (t \<down> i) = i
[PROOF STEP]
proof (induct i arbitrary: t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>t. t \<up> 0 \<noteq> LNil \<Longrightarrow> LList2.llength (t \<down> 0) = 0
 2. \<And>i t. \<lbrakk>\<And>t. t \<up> i \<noteq> LNil \<Longrightarrow> LList2.llength (t \<down> i) = i; t \<up> Suc i \<noteq> LNil\<rbrakk> \<Longrightarrow> LList2.llength (t \<down> Suc i) = Suc i
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
t \<up> 0 \<noteq> LNil

goal (2 subgoals):
 1. \<And>t. t \<up> 0 \<noteq> LNil \<Longrightarrow> LList2.llength (t \<down> 0) = 0
 2. \<And>i t. \<lbrakk>\<And>t. t \<up> i \<noteq> LNil \<Longrightarrow> LList2.llength (t \<down> i) = i; t \<up> Suc i \<noteq> LNil\<rbrakk> \<Longrightarrow> LList2.llength (t \<down> Suc i) = Suc i
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LList2.llength (t \<down> 0) = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
LList2.llength (t \<down> 0) = 0

goal (1 subgoal):
 1. \<And>i t. \<lbrakk>\<And>t. t \<up> i \<noteq> LNil \<Longrightarrow> LList2.llength (t \<down> i) = i; t \<up> Suc i \<noteq> LNil\<rbrakk> \<Longrightarrow> LList2.llength (t \<down> Suc i) = Suc i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i t. \<lbrakk>\<And>t. t \<up> i \<noteq> LNil \<Longrightarrow> LList2.llength (t \<down> i) = i; t \<up> Suc i \<noteq> LNil\<rbrakk> \<Longrightarrow> LList2.llength (t \<down> Suc i) = Suc i
[PROOF STEP]
case (Suc j)
[PROOF STATE]
proof (state)
this:
?t \<up> j \<noteq> LNil \<Longrightarrow> LList2.llength (?t \<down> j) = j
t \<up> Suc j \<noteq> LNil

goal (1 subgoal):
 1. \<And>i t. \<lbrakk>\<And>t. t \<up> i \<noteq> LNil \<Longrightarrow> LList2.llength (t \<down> i) = i; t \<up> Suc i \<noteq> LNil\<rbrakk> \<Longrightarrow> LList2.llength (t \<down> Suc i) = Suc i
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
?t \<up> j \<noteq> LNil \<Longrightarrow> LList2.llength (?t \<down> j) = j
t \<up> Suc j \<noteq> LNil

goal (1 subgoal):
 1. LList2.llength (t \<down> Suc j) = Suc j
[PROOF STEP]
by (cases t) (auto simp: llength_LCons [of _ UNIV])
[PROOF STATE]
proof (state)
this:
LList2.llength (t \<down> Suc j) = Suc j

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fps_induct [case_names LNil LCons, induct set: fpslsts, consumes 1]:
  assumes fps: "l \<in> A\<^sup>\<clubsuit>"
  and    init: "\<And>a. a \<in> A \<Longrightarrow> P (a##LNil)"
  and    step: "\<And>a l. \<lbrakk> l \<in> A\<^sup>\<clubsuit>; P l; a \<in> A \<rbrakk> \<Longrightarrow> P (a ## l)"
  shows "P l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P l
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P l
[PROOF STEP]
from fps
[PROOF STATE]
proof (chain)
picking this:
l \<in> A\<^sup>\<clubsuit>
[PROOF STEP]
have "l \<in> A\<^sup>\<star>" and "l \<noteq> LNil"
[PROOF STATE]
proof (prove)
using this:
l \<in> A\<^sup>\<clubsuit>

goal (1 subgoal):
 1. l \<in> A\<^sup>\<star> &&& l \<noteq> LNil
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l \<in> A\<^sup>\<star>
l \<noteq> LNil

goal (1 subgoal):
 1. P l
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
l \<in> A\<^sup>\<star>
l \<noteq> LNil

goal (1 subgoal):
 1. P l
[PROOF STEP]
by (induct, simp) (cases, auto intro: init step)
[PROOF STATE]
proof (state)
this:
P l

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lbutlast_lapp_llast:
assumes "l \<in> A\<^sup>\<clubsuit>"
  shows "l = lbutlast l @@ (llast l ## LNil)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l = lbutlast l @@ LList2.llast l ## LNil
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
l \<in> A\<^sup>\<clubsuit>

goal (1 subgoal):
 1. l = lbutlast l @@ LList2.llast l ## LNil
[PROOF STEP]
by induct auto


[STATEMENT]
lemma llast_snoc [simp]:
  assumes fin: "xs \<in> A\<^sup>\<star>"
  shows "llast (xs @@ x ## LNil) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LList2.llast (xs @@ x ## LNil) = x
[PROOF STEP]
using fin
[PROOF STATE]
proof (prove)
using this:
xs \<in> A\<^sup>\<star>

goal (1 subgoal):
 1. LList2.llast (xs @@ x ## LNil) = x
[PROOF STEP]
proof induct
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>l. l = LNil \<Longrightarrow> LList2.llast (l @@ x ## LNil) = x
 2. \<And>a l. \<lbrakk>l \<in> A\<^sup>\<star>; LList2.llast (l @@ x ## LNil) = x; a \<in> A\<rbrakk> \<Longrightarrow> LList2.llast ((a ## l) @@ x ## LNil) = x
[PROOF STEP]
case LNil_fin
[PROOF STATE]
proof (state)
this:
l_ = LNil

goal (2 subgoals):
 1. \<And>l. l = LNil \<Longrightarrow> LList2.llast (l @@ x ## LNil) = x
 2. \<And>a l. \<lbrakk>l \<in> A\<^sup>\<star>; LList2.llast (l @@ x ## LNil) = x; a \<in> A\<rbrakk> \<Longrightarrow> LList2.llast ((a ## l) @@ x ## LNil) = x
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
l_ = LNil

goal (1 subgoal):
 1. LList2.llast (l_ @@ x ## LNil) = x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
LList2.llast (l_ @@ x ## LNil) = x

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>l \<in> A\<^sup>\<star>; LList2.llast (l @@ x ## LNil) = x; a \<in> A\<rbrakk> \<Longrightarrow> LList2.llast ((a ## l) @@ x ## LNil) = x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a l. \<lbrakk>l \<in> A\<^sup>\<star>; LList2.llast (l @@ x ## LNil) = x; a \<in> A\<rbrakk> \<Longrightarrow> LList2.llast ((a ## l) @@ x ## LNil) = x
[PROOF STEP]
case (LCons_fin a l)
[PROOF STATE]
proof (state)
this:
l \<in> A\<^sup>\<star>
LList2.llast (l @@ x ## LNil) = x
a \<in> A

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>l \<in> A\<^sup>\<star>; LList2.llast (l @@ x ## LNil) = x; a \<in> A\<rbrakk> \<Longrightarrow> LList2.llast ((a ## l) @@ x ## LNil) = x
[PROOF STEP]
have "x ## LNil \<in> UNIV\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x ## LNil \<in> UNIV\<^sup>\<star>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x ## LNil \<in> UNIV\<^sup>\<star>

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>l \<in> A\<^sup>\<star>; LList2.llast (l @@ x ## LNil) = x; a \<in> A\<rbrakk> \<Longrightarrow> LList2.llast ((a ## l) @@ x ## LNil) = x
[PROOF STEP]
with LCons_fin
[PROOF STATE]
proof (chain)
picking this:
l \<in> A\<^sup>\<star>
LList2.llast (l @@ x ## LNil) = x
a \<in> A
x ## LNil \<in> UNIV\<^sup>\<star>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
l \<in> A\<^sup>\<star>
LList2.llast (l @@ x ## LNil) = x
a \<in> A
x ## LNil \<in> UNIV\<^sup>\<star>

goal (1 subgoal):
 1. LList2.llast ((a ## l) @@ x ## LNil) = x
[PROOF STEP]
by (auto simp: llast_LCons [of _ UNIV])
[PROOF STATE]
proof (state)
this:
LList2.llast ((a ## l) @@ x ## LNil) = x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lbutlast_snoc [simp]:
  assumes fin: "xs \<in> A\<^sup>\<star>"
  shows "lbutlast (xs @@ x ## LNil) = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lbutlast (xs @@ x ## LNil) = xs
[PROOF STEP]
using fin
[PROOF STATE]
proof (prove)
using this:
xs \<in> A\<^sup>\<star>

goal (1 subgoal):
 1. lbutlast (xs @@ x ## LNil) = xs
[PROOF STEP]
proof induct
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>l. l = LNil \<Longrightarrow> lbutlast (l @@ x ## LNil) = l
 2. \<And>a l. \<lbrakk>l \<in> A\<^sup>\<star>; lbutlast (l @@ x ## LNil) = l; a \<in> A\<rbrakk> \<Longrightarrow> lbutlast ((a ## l) @@ x ## LNil) = a ## l
[PROOF STEP]
case LNil_fin
[PROOF STATE]
proof (state)
this:
l_ = LNil

goal (2 subgoals):
 1. \<And>l. l = LNil \<Longrightarrow> lbutlast (l @@ x ## LNil) = l
 2. \<And>a l. \<lbrakk>l \<in> A\<^sup>\<star>; lbutlast (l @@ x ## LNil) = l; a \<in> A\<rbrakk> \<Longrightarrow> lbutlast ((a ## l) @@ x ## LNil) = a ## l
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
l_ = LNil

goal (1 subgoal):
 1. lbutlast (l_ @@ x ## LNil) = l_
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lbutlast (l_ @@ x ## LNil) = l_

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>l \<in> A\<^sup>\<star>; lbutlast (l @@ x ## LNil) = l; a \<in> A\<rbrakk> \<Longrightarrow> lbutlast ((a ## l) @@ x ## LNil) = a ## l
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a l. \<lbrakk>l \<in> A\<^sup>\<star>; lbutlast (l @@ x ## LNil) = l; a \<in> A\<rbrakk> \<Longrightarrow> lbutlast ((a ## l) @@ x ## LNil) = a ## l
[PROOF STEP]
case (LCons_fin a l)
[PROOF STATE]
proof (state)
this:
l \<in> A\<^sup>\<star>
lbutlast (l @@ x ## LNil) = l
a \<in> A

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>l \<in> A\<^sup>\<star>; lbutlast (l @@ x ## LNil) = l; a \<in> A\<rbrakk> \<Longrightarrow> lbutlast ((a ## l) @@ x ## LNil) = a ## l
[PROOF STEP]
have "x ## LNil \<in> UNIV\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x ## LNil \<in> UNIV\<^sup>\<star>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x ## LNil \<in> UNIV\<^sup>\<star>

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>l \<in> A\<^sup>\<star>; lbutlast (l @@ x ## LNil) = l; a \<in> A\<rbrakk> \<Longrightarrow> lbutlast ((a ## l) @@ x ## LNil) = a ## l
[PROOF STEP]
with LCons_fin
[PROOF STATE]
proof (chain)
picking this:
l \<in> A\<^sup>\<star>
lbutlast (l @@ x ## LNil) = l
a \<in> A
x ## LNil \<in> UNIV\<^sup>\<star>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
l \<in> A\<^sup>\<star>
lbutlast (l @@ x ## LNil) = l
a \<in> A
x ## LNil \<in> UNIV\<^sup>\<star>

goal (1 subgoal):
 1. lbutlast ((a ## l) @@ x ## LNil) = a ## l
[PROOF STEP]
by (auto simp: lbutlast_LCons [of _ UNIV])
[PROOF STATE]
proof (state)
this:
lbutlast ((a ## l) @@ x ## LNil) = a ## l

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma llast_lappend [simp]:
"\<lbrakk> x \<in> UNIV\<^sup>\<star>; y \<in> UNIV\<^sup>\<star> \<rbrakk> \<Longrightarrow> llast (x @@ a ## y) = llast (a ## y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> UNIV\<^sup>\<star>; y \<in> UNIV\<^sup>\<star>\<rbrakk> \<Longrightarrow> LList2.llast (x @@ a ## y) = LList2.llast (a ## y)
[PROOF STEP]
proof (induct rule: finlsts.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. y \<in> UNIV\<^sup>\<star> \<Longrightarrow> LList2.llast (LNil @@ a ## y) = LList2.llast (a ## y)
 2. \<And>l aa. \<lbrakk>l \<in> UNIV\<^sup>\<star>; y \<in> UNIV\<^sup>\<star> \<Longrightarrow> LList2.llast (l @@ a ## y) = LList2.llast (a ## y); aa \<in> UNIV; y \<in> UNIV\<^sup>\<star>\<rbrakk> \<Longrightarrow> LList2.llast ((aa ## l) @@ a ## y) = LList2.llast (a ## y)
[PROOF STEP]
case LNil_fin
[PROOF STATE]
proof (state)
this:
y \<in> UNIV\<^sup>\<star>

goal (2 subgoals):
 1. y \<in> UNIV\<^sup>\<star> \<Longrightarrow> LList2.llast (LNil @@ a ## y) = LList2.llast (a ## y)
 2. \<And>l aa. \<lbrakk>l \<in> UNIV\<^sup>\<star>; y \<in> UNIV\<^sup>\<star> \<Longrightarrow> LList2.llast (l @@ a ## y) = LList2.llast (a ## y); aa \<in> UNIV; y \<in> UNIV\<^sup>\<star>\<rbrakk> \<Longrightarrow> LList2.llast ((aa ## l) @@ a ## y) = LList2.llast (a ## y)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
y \<in> UNIV\<^sup>\<star>

goal (1 subgoal):
 1. LList2.llast (LNil @@ a ## y) = LList2.llast (a ## y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
LList2.llast (LNil @@ a ## y) = LList2.llast (a ## y)

goal (1 subgoal):
 1. \<And>l aa. \<lbrakk>l \<in> UNIV\<^sup>\<star>; y \<in> UNIV\<^sup>\<star> \<Longrightarrow> LList2.llast (l @@ a ## y) = LList2.llast (a ## y); aa \<in> UNIV; y \<in> UNIV\<^sup>\<star>\<rbrakk> \<Longrightarrow> LList2.llast ((aa ## l) @@ a ## y) = LList2.llast (a ## y)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>l aa. \<lbrakk>l \<in> UNIV\<^sup>\<star>; y \<in> UNIV\<^sup>\<star> \<Longrightarrow> LList2.llast (l @@ a ## y) = LList2.llast (a ## y); aa \<in> UNIV; y \<in> UNIV\<^sup>\<star>\<rbrakk> \<Longrightarrow> LList2.llast ((aa ## l) @@ a ## y) = LList2.llast (a ## y)
[PROOF STEP]
case (LCons_fin l b)
[PROOF STATE]
proof (state)
this:
l \<in> UNIV\<^sup>\<star>
y \<in> UNIV\<^sup>\<star> \<Longrightarrow> LList2.llast (l @@ a ## y) = LList2.llast (a ## y)
b \<in> UNIV
y \<in> UNIV\<^sup>\<star>

goal (1 subgoal):
 1. \<And>l aa. \<lbrakk>l \<in> UNIV\<^sup>\<star>; y \<in> UNIV\<^sup>\<star> \<Longrightarrow> LList2.llast (l @@ a ## y) = LList2.llast (a ## y); aa \<in> UNIV; y \<in> UNIV\<^sup>\<star>\<rbrakk> \<Longrightarrow> LList2.llast ((aa ## l) @@ a ## y) = LList2.llast (a ## y)
[PROOF STEP]
hence "l @@ a ## y \<in> UNIV\<^sup>\<star>"
[PROOF STATE]
proof (prove)
using this:
l \<in> UNIV\<^sup>\<star>
y \<in> UNIV\<^sup>\<star> \<Longrightarrow> LList2.llast (l @@ a ## y) = LList2.llast (a ## y)
b \<in> UNIV
y \<in> UNIV\<^sup>\<star>

goal (1 subgoal):
 1. l @@ a ## y \<in> UNIV\<^sup>\<star>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l @@ a ## y \<in> UNIV\<^sup>\<star>

goal (1 subgoal):
 1. \<And>l aa. \<lbrakk>l \<in> UNIV\<^sup>\<star>; y \<in> UNIV\<^sup>\<star> \<Longrightarrow> LList2.llast (l @@ a ## y) = LList2.llast (a ## y); aa \<in> UNIV; y \<in> UNIV\<^sup>\<star>\<rbrakk> \<Longrightarrow> LList2.llast ((aa ## l) @@ a ## y) = LList2.llast (a ## y)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
l @@ a ## y \<in> UNIV\<^sup>\<star>

goal (1 subgoal):
 1. LList2.llast ((b ## l) @@ a ## y) = LList2.llast (a ## y)
[PROOF STEP]
using LCons_fin
[PROOF STATE]
proof (prove)
using this:
l @@ a ## y \<in> UNIV\<^sup>\<star>
l \<in> UNIV\<^sup>\<star>
y \<in> UNIV\<^sup>\<star> \<Longrightarrow> LList2.llast (l @@ a ## y) = LList2.llast (a ## y)
b \<in> UNIV
y \<in> UNIV\<^sup>\<star>

goal (1 subgoal):
 1. LList2.llast ((b ## l) @@ a ## y) = LList2.llast (a ## y)
[PROOF STEP]
by (auto simp: llast_LCons [of _ UNIV])
[PROOF STATE]
proof (state)
this:
LList2.llast ((b ## l) @@ a ## y) = LList2.llast (a ## y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma llast_llength:
  assumes tfin: "t \<in> UNIV\<^sup>\<star>"
  shows "t \<noteq> LNil \<Longrightarrow> t !! (llength t - (Suc 0)) = Some (llast t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<noteq> LNil \<Longrightarrow> t !! (LList2.llength t - Suc 0) = Some (LList2.llast t)
[PROOF STEP]
using tfin
[PROOF STATE]
proof (prove)
using this:
t \<in> UNIV\<^sup>\<star>

goal (1 subgoal):
 1. t \<noteq> LNil \<Longrightarrow> t !! (LList2.llength t - Suc 0) = Some (LList2.llast t)
[PROOF STEP]
proof induct
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>l. \<lbrakk>l = LNil; l \<noteq> LNil\<rbrakk> \<Longrightarrow> l !! (LList2.llength l - Suc 0) = Some (LList2.llast l)
 2. \<And>a l. \<lbrakk>l \<in> UNIV\<^sup>\<star>; l \<noteq> LNil \<Longrightarrow> l !! (LList2.llength l - Suc 0) = Some (LList2.llast l); a \<in> UNIV; a ## l \<noteq> LNil\<rbrakk> \<Longrightarrow> (a ## l) !! (LList2.llength (a ## l) - Suc 0) = Some (LList2.llast (a ## l))
[PROOF STEP]
case (LNil_fin l)
[PROOF STATE]
proof (state)
this:
l = LNil
l \<noteq> LNil

goal (2 subgoals):
 1. \<And>l. \<lbrakk>l = LNil; l \<noteq> LNil\<rbrakk> \<Longrightarrow> l !! (LList2.llength l - Suc 0) = Some (LList2.llast l)
 2. \<And>a l. \<lbrakk>l \<in> UNIV\<^sup>\<star>; l \<noteq> LNil \<Longrightarrow> l !! (LList2.llength l - Suc 0) = Some (LList2.llast l); a \<in> UNIV; a ## l \<noteq> LNil\<rbrakk> \<Longrightarrow> (a ## l) !! (LList2.llength (a ## l) - Suc 0) = Some (LList2.llast (a ## l))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
l = LNil
l \<noteq> LNil

goal (1 subgoal):
 1. l !! (LList2.llength l - Suc 0) = Some (LList2.llast l)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l !! (LList2.llength l - Suc 0) = Some (LList2.llast l)

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>l \<in> UNIV\<^sup>\<star>; l \<noteq> LNil \<Longrightarrow> l !! (LList2.llength l - Suc 0) = Some (LList2.llast l); a \<in> UNIV; a ## l \<noteq> LNil\<rbrakk> \<Longrightarrow> (a ## l) !! (LList2.llength (a ## l) - Suc 0) = Some (LList2.llast (a ## l))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a l. \<lbrakk>l \<in> UNIV\<^sup>\<star>; l \<noteq> LNil \<Longrightarrow> l !! (LList2.llength l - Suc 0) = Some (LList2.llast l); a \<in> UNIV; a ## l \<noteq> LNil\<rbrakk> \<Longrightarrow> (a ## l) !! (LList2.llength (a ## l) - Suc 0) = Some (LList2.llast (a ## l))
[PROOF STEP]
case (LCons_fin a l)
[PROOF STATE]
proof (state)
this:
l \<in> UNIV\<^sup>\<star>
l \<noteq> LNil \<Longrightarrow> l !! (LList2.llength l - Suc 0) = Some (LList2.llast l)
a \<in> UNIV
a ## l \<noteq> LNil

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>l \<in> UNIV\<^sup>\<star>; l \<noteq> LNil \<Longrightarrow> l !! (LList2.llength l - Suc 0) = Some (LList2.llast l); a \<in> UNIV; a ## l \<noteq> LNil\<rbrakk> \<Longrightarrow> (a ## l) !! (LList2.llength (a ## l) - Suc 0) = Some (LList2.llast (a ## l))
[PROOF STEP]
note consal = this
[PROOF STATE]
proof (state)
this:
l \<in> UNIV\<^sup>\<star>
l \<noteq> LNil \<Longrightarrow> l !! (LList2.llength l - Suc 0) = Some (LList2.llast l)
a \<in> UNIV
a ## l \<noteq> LNil

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>l \<in> UNIV\<^sup>\<star>; l \<noteq> LNil \<Longrightarrow> l !! (LList2.llength l - Suc 0) = Some (LList2.llast l); a \<in> UNIV; a ## l \<noteq> LNil\<rbrakk> \<Longrightarrow> (a ## l) !! (LList2.llength (a ## l) - Suc 0) = Some (LList2.llast (a ## l))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
l \<in> UNIV\<^sup>\<star>
l \<noteq> LNil \<Longrightarrow> l !! (LList2.llength l - Suc 0) = Some (LList2.llast l)
a \<in> UNIV
a ## l \<noteq> LNil

goal (1 subgoal):
 1. (a ## l) !! (LList2.llength (a ## l) - Suc 0) = Some (LList2.llast (a ## l))
[PROOF STEP]
proof (cases l)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>l \<noteq> LNil \<Longrightarrow> l !! (LList2.llength l - Suc 0) = Some (LList2.llast l); a \<in> UNIV; a ## l \<noteq> LNil; l = LNil\<rbrakk> \<Longrightarrow> (a ## l) !! (LList2.llength (a ## l) - Suc 0) = Some (LList2.llast (a ## l))
 2. \<And>la aa. \<lbrakk>l \<noteq> LNil \<Longrightarrow> l !! (LList2.llength l - Suc 0) = Some (LList2.llast l); a \<in> UNIV; a ## l \<noteq> LNil; l = aa ## la; la \<in> UNIV\<^sup>\<star>; aa \<in> UNIV\<rbrakk> \<Longrightarrow> (a ## l) !! (LList2.llength (a ## l) - Suc 0) = Some (LList2.llast (a ## l))
[PROOF STEP]
case LNil_fin
[PROOF STATE]
proof (state)
this:
l = LNil

goal (2 subgoals):
 1. \<lbrakk>l \<noteq> LNil \<Longrightarrow> l !! (LList2.llength l - Suc 0) = Some (LList2.llast l); a \<in> UNIV; a ## l \<noteq> LNil; l = LNil\<rbrakk> \<Longrightarrow> (a ## l) !! (LList2.llength (a ## l) - Suc 0) = Some (LList2.llast (a ## l))
 2. \<And>la aa. \<lbrakk>l \<noteq> LNil \<Longrightarrow> l !! (LList2.llength l - Suc 0) = Some (LList2.llast l); a \<in> UNIV; a ## l \<noteq> LNil; l = aa ## la; la \<in> UNIV\<^sup>\<star>; aa \<in> UNIV\<rbrakk> \<Longrightarrow> (a ## l) !! (LList2.llength (a ## l) - Suc 0) = Some (LList2.llast (a ## l))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
l = LNil

goal (1 subgoal):
 1. (a ## l) !! (LList2.llength (a ## l) - Suc 0) = Some (LList2.llast (a ## l))
[PROOF STEP]
using consal
[PROOF STATE]
proof (prove)
using this:
l = LNil
l \<in> UNIV\<^sup>\<star>
l \<noteq> LNil \<Longrightarrow> l !! (LList2.llength l - Suc 0) = Some (LList2.llast l)
a \<in> UNIV
a ## l \<noteq> LNil

goal (1 subgoal):
 1. (a ## l) !! (LList2.llength (a ## l) - Suc 0) = Some (LList2.llast (a ## l))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(a ## l) !! (LList2.llength (a ## l) - Suc 0) = Some (LList2.llast (a ## l))

goal (1 subgoal):
 1. \<And>la aa. \<lbrakk>l \<noteq> LNil \<Longrightarrow> l !! (LList2.llength l - Suc 0) = Some (LList2.llast l); a \<in> UNIV; a ## l \<noteq> LNil; l = aa ## la; la \<in> UNIV\<^sup>\<star>; aa \<in> UNIV\<rbrakk> \<Longrightarrow> (a ## l) !! (LList2.llength (a ## l) - Suc 0) = Some (LList2.llast (a ## l))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>la aa. \<lbrakk>l \<noteq> LNil \<Longrightarrow> l !! (LList2.llength l - Suc 0) = Some (LList2.llast l); a \<in> UNIV; a ## l \<noteq> LNil; l = aa ## la; la \<in> UNIV\<^sup>\<star>; aa \<in> UNIV\<rbrakk> \<Longrightarrow> (a ## l) !! (LList2.llength (a ## l) - Suc 0) = Some (LList2.llast (a ## l))
[PROOF STEP]
case (LCons_fin aa la)
[PROOF STATE]
proof (state)
this:
l = la ## aa
aa \<in> UNIV\<^sup>\<star>
la \<in> UNIV

goal (1 subgoal):
 1. \<And>la aa. \<lbrakk>l \<noteq> LNil \<Longrightarrow> l !! (LList2.llength l - Suc 0) = Some (LList2.llast l); a \<in> UNIV; a ## l \<noteq> LNil; l = aa ## la; la \<in> UNIV\<^sup>\<star>; aa \<in> UNIV\<rbrakk> \<Longrightarrow> (a ## l) !! (LList2.llength (a ## l) - Suc 0) = Some (LList2.llast (a ## l))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
l = la ## aa
aa \<in> UNIV\<^sup>\<star>
la \<in> UNIV

goal (1 subgoal):
 1. (a ## l) !! (LList2.llength (a ## l) - Suc 0) = Some (LList2.llast (a ## l))
[PROOF STEP]
using consal
[PROOF STATE]
proof (prove)
using this:
l = la ## aa
aa \<in> UNIV\<^sup>\<star>
la \<in> UNIV
l \<in> UNIV\<^sup>\<star>
l \<noteq> LNil \<Longrightarrow> l !! (LList2.llength l - Suc 0) = Some (LList2.llast l)
a \<in> UNIV
a ## l \<noteq> LNil

goal (1 subgoal):
 1. (a ## l) !! (LList2.llength (a ## l) - Suc 0) = Some (LList2.llast (a ## l))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(a ## l) !! (LList2.llength (a ## l) - Suc 0) = Some (LList2.llast (a ## l))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(a ## l) !! (LList2.llength (a ## l) - Suc 0) = Some (LList2.llast (a ## l))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lconst_unfold: "lconst a = a ## lconst a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lconst a = a ## lconst a
[PROOF STEP]
by (auto simp: lconst_def intro: iterates)


[STATEMENT]
lemma lconst_LNil [iff]: "lconst a \<noteq> LNil"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lconst a \<noteq> LNil
[PROOF STEP]
by (clarify,frule subst [OF lconst_unfold]) simp


[STATEMENT]
lemma lconstT:
  assumes aA: "a \<in> A"
  shows "lconst a \<in> A\<^sup>\<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lconst a \<in> A\<^sup>\<omega>
[PROOF STEP]
proof (rule inflstsI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. lconst a \<in> A\<^sup>\<infinity>
 2. lconst a \<in> UNIV\<^sup>\<star> \<Longrightarrow> False
[PROOF STEP]
show "lconst a \<in> A\<^sup>\<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lconst a \<in> A\<^sup>\<infinity>
[PROOF STEP]
proof (rule alllsts.coinduct [of "\<lambda>x. x = lconst a"], simp_all)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>l aa. lconst a = aa ## l \<and> (l = lconst a \<or> l \<in> A\<^sup>\<infinity>) \<and> aa \<in> A
[PROOF STEP]
have "lconst a = a ## lconst a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lconst a = a ## lconst a
[PROOF STEP]
by (rule lconst_unfold)
[PROOF STATE]
proof (state)
this:
lconst a = a ## lconst a

goal (1 subgoal):
 1. \<exists>l aa. lconst a = aa ## l \<and> (l = lconst a \<or> l \<in> A\<^sup>\<infinity>) \<and> aa \<in> A
[PROOF STEP]
with aA
[PROOF STATE]
proof (chain)
picking this:
a \<in> A
lconst a = a ## lconst a
[PROOF STEP]
show "\<exists>l aa. lconst a = aa ## l \<and> (l = lconst a \<or> l \<in> A\<^sup>\<infinity>) \<and> aa \<in> A"
[PROOF STATE]
proof (prove)
using this:
a \<in> A
lconst a = a ## lconst a

goal (1 subgoal):
 1. \<exists>l aa. lconst a = aa ## l \<and> (l = lconst a \<or> l \<in> A\<^sup>\<infinity>) \<and> aa \<in> A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>l aa. lconst a = aa ## l \<and> (l = lconst a \<or> l \<in> A\<^sup>\<infinity>) \<and> aa \<in> A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
lconst a \<in> A\<^sup>\<infinity>

goal (1 subgoal):
 1. lconst a \<in> UNIV\<^sup>\<star> \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lconst a \<in> UNIV\<^sup>\<star> \<Longrightarrow> False
[PROOF STEP]
assume lconst: "lconst a \<in> UNIV\<^sup>\<star>"
[PROOF STATE]
proof (state)
this:
lconst a \<in> UNIV\<^sup>\<star>

goal (1 subgoal):
 1. lconst a \<in> UNIV\<^sup>\<star> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
lconst a \<in> UNIV\<^sup>\<star>

goal (1 subgoal):
 1. lconst a \<in> UNIV\<^sup>\<star> \<Longrightarrow> False
[PROOF STEP]
have "\<And>l. l \<in> UNIV\<^sup>\<star> \<Longrightarrow> lconst a \<noteq> l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. l \<in> UNIV\<^sup>\<star> \<Longrightarrow> lconst a \<noteq> l
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>l. l \<in> UNIV\<^sup>\<star> \<Longrightarrow> lconst a \<noteq> l
[PROOF STEP]
fix l::"'a llist"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>l. l \<in> UNIV\<^sup>\<star> \<Longrightarrow> lconst a \<noteq> l
[PROOF STEP]
assume "l\<in>UNIV\<^sup>\<star>"
[PROOF STATE]
proof (state)
this:
l \<in> UNIV\<^sup>\<star>

goal (1 subgoal):
 1. \<And>l. l \<in> UNIV\<^sup>\<star> \<Longrightarrow> lconst a \<noteq> l
[PROOF STEP]
thus "lconst a \<noteq> l"
[PROOF STATE]
proof (prove)
using this:
l \<in> UNIV\<^sup>\<star>

goal (1 subgoal):
 1. lconst a \<noteq> l
[PROOF STEP]
proof (rule finlsts_induct, simp_all)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa la. \<lbrakk>la \<in> UNIV\<^sup>\<star>; lconst a \<noteq> la; l \<in> UNIV\<^sup>\<star>\<rbrakk> \<Longrightarrow> lconst a \<noteq> aa ## la
[PROOF STEP]
fix a' l'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa la. \<lbrakk>la \<in> UNIV\<^sup>\<star>; lconst a \<noteq> la; l \<in> UNIV\<^sup>\<star>\<rbrakk> \<Longrightarrow> lconst a \<noteq> aa ## la
[PROOF STEP]
assume
        al': "lconst a \<noteq> l'" and
        l'A: "l' \<in> UNIV\<^sup>\<star>"
[PROOF STATE]
proof (state)
this:
lconst a \<noteq> l'
l' \<in> UNIV\<^sup>\<star>

goal (1 subgoal):
 1. \<And>aa la. \<lbrakk>la \<in> UNIV\<^sup>\<star>; lconst a \<noteq> la; l \<in> UNIV\<^sup>\<star>\<rbrakk> \<Longrightarrow> lconst a \<noteq> aa ## la
[PROOF STEP]
from al'
[PROOF STATE]
proof (chain)
picking this:
lconst a \<noteq> l'
[PROOF STEP]
show  "lconst a \<noteq> a' ## l'"
[PROOF STATE]
proof (prove)
using this:
lconst a \<noteq> l'

goal (1 subgoal):
 1. lconst a \<noteq> a' ## l'
[PROOF STEP]
proof (rule contrapos_np)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> lconst a \<noteq> a' ## l' \<Longrightarrow> lconst a = l'
[PROOF STEP]
assume notal: "\<not> lconst a \<noteq> a' ## l'"
[PROOF STATE]
proof (state)
this:
\<not> lconst a \<noteq> a' ## l'

goal (1 subgoal):
 1. \<not> lconst a \<noteq> a' ## l' \<Longrightarrow> lconst a = l'
[PROOF STEP]
hence "lconst a = a' ## l'"
[PROOF STATE]
proof (prove)
using this:
\<not> lconst a \<noteq> a' ## l'

goal (1 subgoal):
 1. lconst a = a' ## l'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lconst a = a' ## l'

goal (1 subgoal):
 1. \<not> lconst a \<noteq> a' ## l' \<Longrightarrow> lconst a = l'
[PROOF STEP]
hence "a ## lconst a = a' ## l'"
[PROOF STATE]
proof (prove)
using this:
lconst a = a' ## l'

goal (1 subgoal):
 1. a ## lconst a = a' ## l'
[PROOF STEP]
by (rule subst [OF lconst_unfold])
[PROOF STATE]
proof (state)
this:
a ## lconst a = a' ## l'

goal (1 subgoal):
 1. \<not> lconst a \<noteq> a' ## l' \<Longrightarrow> lconst a = l'
[PROOF STEP]
thus "lconst a = l'"
[PROOF STATE]
proof (prove)
using this:
a ## lconst a = a' ## l'

goal (1 subgoal):
 1. lconst a = l'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lconst a = l'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
lconst a \<noteq> a' ## l'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
lconst a \<noteq> l

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?l \<in> UNIV\<^sup>\<star> \<Longrightarrow> lconst a \<noteq> ?l

goal (1 subgoal):
 1. lconst a \<in> UNIV\<^sup>\<star> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
lconst a \<in> UNIV\<^sup>\<star>
?l \<in> UNIV\<^sup>\<star> \<Longrightarrow> lconst a \<noteq> ?l
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
lconst a \<in> UNIV\<^sup>\<star>
?l \<in> UNIV\<^sup>\<star> \<Longrightarrow> lconst a \<noteq> ?l

goal (1 subgoal):
 1. False
[PROOF STEP]
using aA
[PROOF STATE]
proof (prove)
using this:
lconst a \<in> UNIV\<^sup>\<star>
?l \<in> UNIV\<^sup>\<star> \<Longrightarrow> lconst a \<noteq> ?l
a \<in> A

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma not_LCons_le_LNil [iff]:
  "\<not> (a##l) \<le> LNil"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> a ## l \<le> LNil
[PROOF STEP]
by (unfold llist_le_def) auto


[STATEMENT]
lemma LNil_le [iff]:"LNil \<le> s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LNil \<le> s
[PROOF STEP]
by (auto simp: llist_le_def)


[STATEMENT]
lemma le_LNil [iff]: "(s \<le> LNil) = (s = LNil)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s \<le> LNil) = (s = LNil)
[PROOF STEP]
by (auto simp: llist_le_def)


[STATEMENT]
lemma llist_inf_le:
  "s \<in> A\<^sup>\<omega>  \<Longrightarrow> (s\<le>t) = (s=t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<in> A\<^sup>\<omega> \<Longrightarrow> (s \<le> t) = (s = t)
[PROOF STEP]
by (unfold llist_le_def) auto


[STATEMENT]
lemma le_LCons [iff]: "(x ## xs \<le> y ## ys) = (x = y \<and> xs \<le> ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x ## xs \<le> y ## ys) = (x = y \<and> xs \<le> ys)
[PROOF STEP]
by (unfold llist_le_def) auto


[STATEMENT]
lemma llist_le_refl [iff]:
  "(s:: 'a llist) \<le> s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<le> s
[PROOF STEP]
by (unfold llist_le_def) (rule exI [of _ "LNil"], simp)


[STATEMENT]
lemma llist_le_trans [trans]:
  fixes r:: "'a llist"
  shows "r \<le> s \<Longrightarrow> s \<le> t \<Longrightarrow> r \<le> t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r \<le> s; s \<le> t\<rbrakk> \<Longrightarrow> r \<le> t
[PROOF STEP]
by (auto simp: llist_le_def lappend_assoc)