[STATEMENT]
lemma BuildSeq_insf:
  assumes b: "BuildSeq B C s k z"
      and m: "m \<^bold>\<in> succ k"
      and n: "n \<^bold>\<in> succ k"
      and y: "B y \<or> C y (app s m) (app s n)"
shows "BuildSeq B C (insf s (succ k) y) (succ k) y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. BuildSeq B C (insf s (succ k) y) (succ k) y
[PROOF STEP]
proof (rule BuildSeqI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. LstSeq (insf s (succ k) y) (succ k) y
 2. \<And>l. l \<^bold>\<in> succ (succ k) \<Longrightarrow> Builds B C (insf s (succ k) y) l
[PROOF STEP]
show "LstSeq (insf s (succ k) y) (succ k) y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LstSeq (insf s (succ k) y) (succ k) y
[PROOF STEP]
by (metis BuildSeq_imp_LstSeq LstSeq_insf b)
[PROOF STATE]
proof (state)
this:
LstSeq (insf s (succ k) y) (succ k) y

goal (1 subgoal):
 1. \<And>l. l \<^bold>\<in> succ (succ k) \<Longrightarrow> Builds B C (insf s (succ k) y) l
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>l. l \<^bold>\<in> succ (succ k) \<Longrightarrow> Builds B C (insf s (succ k) y) l
[PROOF STEP]
fix l
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>l. l \<^bold>\<in> succ (succ k) \<Longrightarrow> Builds B C (insf s (succ k) y) l
[PROOF STEP]
assume l: "l \<^bold>\<in> succ (succ k)"
[PROOF STATE]
proof (state)
this:
l \<^bold>\<in> succ (succ k)

goal (1 subgoal):
 1. \<And>l. l \<^bold>\<in> succ (succ k) \<Longrightarrow> Builds B C (insf s (succ k) y) l
[PROOF STEP]
thus "Builds B C (insf s (succ k) y) l"
[PROOF STATE]
proof (prove)
using this:
l \<^bold>\<in> succ (succ k)

goal (1 subgoal):
 1. Builds B C (insf s (succ k) y) l
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. l = succ k \<Longrightarrow> Builds B C (insf s (succ k) y) l
 2. l \<^bold>\<in> succ k \<Longrightarrow> Builds B C (insf s (succ k) y) l
[PROOF STEP]
assume l: "l = succ k"
[PROOF STATE]
proof (state)
this:
l = succ k

goal (2 subgoals):
 1. l = succ k \<Longrightarrow> Builds B C (insf s (succ k) y) l
 2. l \<^bold>\<in> succ k \<Longrightarrow> Builds B C (insf s (succ k) y) l
[PROOF STEP]
have "B (app (insf s l y) l) \<or> C (app (insf s l y) l) (app (insf s l y) m) (app (insf s l y) n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B (app (insf s l y) l) \<or> C (app (insf s l y) l) (app (insf s l y) m) (app (insf s l y) n)
[PROOF STEP]
by (metis BuildSeq_imp_Seq app_insf_Seq_if b hmem_not_refl l m n y)
[PROOF STATE]
proof (state)
this:
B (app (insf s l y) l) \<or> C (app (insf s l y) l) (app (insf s l y) m) (app (insf s l y) n)

goal (2 subgoals):
 1. l = succ k \<Longrightarrow> Builds B C (insf s (succ k) y) l
 2. l \<^bold>\<in> succ k \<Longrightarrow> Builds B C (insf s (succ k) y) l
[PROOF STEP]
thus "Builds B C (insf s (succ k) y) l"
[PROOF STATE]
proof (prove)
using this:
B (app (insf s l y) l) \<or> C (app (insf s l y) l) (app (insf s l y) m) (app (insf s l y) n)

goal (1 subgoal):
 1. Builds B C (insf s (succ k) y) l
[PROOF STEP]
using m n
[PROOF STATE]
proof (prove)
using this:
B (app (insf s l y) l) \<or> C (app (insf s l y) l) (app (insf s l y) m) (app (insf s l y) n)
m \<^bold>\<in> succ k
n \<^bold>\<in> succ k

goal (1 subgoal):
 1. Builds B C (insf s (succ k) y) l
[PROOF STEP]
by (auto simp: Builds_def l)
[PROOF STATE]
proof (state)
this:
Builds B C (insf s (succ k) y) l

goal (1 subgoal):
 1. l \<^bold>\<in> succ k \<Longrightarrow> Builds B C (insf s (succ k) y) l
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l \<^bold>\<in> succ k \<Longrightarrow> Builds B C (insf s (succ k) y) l
[PROOF STEP]
assume l: "l \<^bold>\<in> succ k"
[PROOF STATE]
proof (state)
this:
l \<^bold>\<in> succ k

goal (1 subgoal):
 1. l \<^bold>\<in> succ k \<Longrightarrow> Builds B C (insf s (succ k) y) l
[PROOF STEP]
have  "LstSeq s k z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LstSeq s k z
[PROOF STEP]
by (metis BuildSeq_imp_LstSeq b)
[PROOF STATE]
proof (state)
this:
LstSeq s k z

goal (1 subgoal):
 1. l \<^bold>\<in> succ k \<Longrightarrow> Builds B C (insf s (succ k) y) l
[PROOF STEP]
thus "Builds B C (insf s (succ k) y) l"
[PROOF STATE]
proof (prove)
using this:
LstSeq s k z

goal (1 subgoal):
 1. Builds B C (insf s (succ k) y) l
[PROOF STEP]
using b l
[PROOF STATE]
proof (prove)
using this:
LstSeq s k z
BuildSeq B C s k z
l \<^bold>\<in> succ k

goal (1 subgoal):
 1. Builds B C (insf s (succ k) y) l
[PROOF STEP]
by (metis hballE Builds_insf BuildSeq_def)
[PROOF STATE]
proof (state)
this:
Builds B C (insf s (succ k) y) l

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Builds B C (insf s (succ k) y) l

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma BuildSeq_insf1:
  assumes b: "BuildSeq B C s k z"
      and y: "B y"
  shows "BuildSeq B C (insf s (succ k) y) (succ k) y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. BuildSeq B C (insf s (succ k) y) (succ k) y
[PROOF STEP]
by (metis BuildSeq_insf b succ_iff y)


[STATEMENT]
lemma BuildSeq_insf2:
  assumes b: "BuildSeq B C s k z"
      and m: "m \<^bold>\<in> k"
      and n: "n \<^bold>\<in> k"
      and y: "C y (app s m) (app s n)"
  shows "BuildSeq B C (insf s (succ k) y) (succ k) y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. BuildSeq B C (insf s (succ k) y) (succ k) y
[PROOF STEP]
by (metis BuildSeq_insf b m n succ_iff y)


[STATEMENT]
lemma BuildSeq_append:
  assumes s1: "BuildSeq B C s1 k1 y1" and s2: "BuildSeq B C s2 k2 y2"
  shows "BuildSeq B C (seq_append (succ k1) s1 s2) (succ (k1 @+ k2)) y2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. BuildSeq B C (seq_append (succ k1) s1 s2) (succ (k1 @+ k2)) y2
[PROOF STEP]
proof (rule BuildSeqI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. LstSeq (seq_append (succ k1) s1 s2) (succ (k1 @+ k2)) y2
 2. \<And>l. l \<^bold>\<in> succ (succ (k1 @+ k2)) \<Longrightarrow> Builds B C (seq_append (succ k1) s1 s2) l
[PROOF STEP]
show "LstSeq (seq_append (succ k1) s1 s2) (succ (k1 @+ k2)) y2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LstSeq (seq_append (succ k1) s1 s2) (succ (k1 @+ k2)) y2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
BuildSeq B C s1 k1 y1
BuildSeq B C s2 k2 y2

goal (1 subgoal):
 1. LstSeq (seq_append (succ k1) s1 s2) (succ (k1 @+ k2)) y2
[PROOF STEP]
by (metis BuildSeq_imp_LstSeq LstSeq_append)
[PROOF STATE]
proof (state)
this:
LstSeq (seq_append (succ k1) s1 s2) (succ (k1 @+ k2)) y2

goal (1 subgoal):
 1. \<And>l. l \<^bold>\<in> succ (succ (k1 @+ k2)) \<Longrightarrow> Builds B C (seq_append (succ k1) s1 s2) l
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>l. l \<^bold>\<in> succ (succ (k1 @+ k2)) \<Longrightarrow> Builds B C (seq_append (succ k1) s1 s2) l
[PROOF STEP]
fix l
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>l. l \<^bold>\<in> succ (succ (k1 @+ k2)) \<Longrightarrow> Builds B C (seq_append (succ k1) s1 s2) l
[PROOF STEP]
have s1L: "LstSeq s1 k1 y1"
   and s1BC: "\<And>l. l \<^bold>\<in> succ k1 \<Longrightarrow> Builds B C s1 l"
   and s2L: "LstSeq s2 k2 y2"
   and s2BC: "\<And>l. l \<^bold>\<in> succ k2 \<Longrightarrow> Builds B C s2 l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LstSeq s1 k1 y1 &&& (\<And>l. l \<^bold>\<in> succ k1 \<Longrightarrow> Builds B C s1 l)) &&& LstSeq s2 k2 y2 &&& (\<And>l. l \<^bold>\<in> succ k2 \<Longrightarrow> Builds B C s2 l)
[PROOF STEP]
using s1 s2
[PROOF STATE]
proof (prove)
using this:
BuildSeq B C s1 k1 y1
BuildSeq B C s2 k2 y2

goal (1 subgoal):
 1. (LstSeq s1 k1 y1 &&& (\<And>l. l \<^bold>\<in> succ k1 \<Longrightarrow> Builds B C s1 l)) &&& LstSeq s2 k2 y2 &&& (\<And>l. l \<^bold>\<in> succ k2 \<Longrightarrow> Builds B C s2 l)
[PROOF STEP]
by (auto simp: BuildSeq_def)
[PROOF STATE]
proof (state)
this:
LstSeq s1 k1 y1
?l \<^bold>\<in> succ k1 \<Longrightarrow> Builds B C s1 ?l
LstSeq s2 k2 y2
?l \<^bold>\<in> succ k2 \<Longrightarrow> Builds B C s2 ?l

goal (1 subgoal):
 1. \<And>l. l \<^bold>\<in> succ (succ (k1 @+ k2)) \<Longrightarrow> Builds B C (seq_append (succ k1) s1 s2) l
[PROOF STEP]
assume l: "l \<^bold>\<in> succ (succ (k1 @+ k2))"
[PROOF STATE]
proof (state)
this:
l \<^bold>\<in> succ (succ (k1 @+ k2))

goal (1 subgoal):
 1. \<And>l. l \<^bold>\<in> succ (succ (k1 @+ k2)) \<Longrightarrow> Builds B C (seq_append (succ k1) s1 s2) l
[PROOF STEP]
hence  "l \<^bold>\<in> succ k1 @+ succ k2"
[PROOF STATE]
proof (prove)
using this:
l \<^bold>\<in> succ (succ (k1 @+ k2))

goal (1 subgoal):
 1. l \<^bold>\<in> succ k1 @+ succ k2
[PROOF STEP]
by (metis LstSeq_imp_Ord hadd_succ_left hadd_succ_right s2L)
[PROOF STATE]
proof (state)
this:
l \<^bold>\<in> succ k1 @+ succ k2

goal (1 subgoal):
 1. \<And>l. l \<^bold>\<in> succ (succ (k1 @+ k2)) \<Longrightarrow> Builds B C (seq_append (succ k1) s1 s2) l
[PROOF STEP]
thus "Builds B C (seq_append (succ k1) s1 s2) l"
[PROOF STATE]
proof (prove)
using this:
l \<^bold>\<in> succ k1 @+ succ k2

goal (1 subgoal):
 1. Builds B C (seq_append (succ k1) s1 s2) l
[PROOF STEP]
proof (rule hmem_hadd_E)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. l \<^bold>\<in> succ k1 \<Longrightarrow> Builds B C (seq_append (succ k1) s1 s2) l
 2. \<And>z. \<lbrakk>z \<^bold>\<in> succ k2; l = succ k1 @+ z\<rbrakk> \<Longrightarrow> Builds B C (seq_append (succ k1) s1 s2) l
[PROOF STEP]
assume l1: "l \<^bold>\<in> succ k1"
[PROOF STATE]
proof (state)
this:
l \<^bold>\<in> succ k1

goal (2 subgoals):
 1. l \<^bold>\<in> succ k1 \<Longrightarrow> Builds B C (seq_append (succ k1) s1 s2) l
 2. \<And>z. \<lbrakk>z \<^bold>\<in> succ k2; l = succ k1 @+ z\<rbrakk> \<Longrightarrow> Builds B C (seq_append (succ k1) s1 s2) l
[PROOF STEP]
hence "B (app s1 l) \<or> (\<exists>m\<^bold>\<in>l. \<exists>n\<^bold>\<in>l. C (app s1 l) (app s1 m) (app s1 n))"
[PROOF STATE]
proof (prove)
using this:
l \<^bold>\<in> succ k1

goal (1 subgoal):
 1. B (app s1 l) \<or> (\<exists>m\<^bold>\<in>l. \<exists>n\<^bold>\<in>l. C (app s1 l) (app s1 m) (app s1 n))
[PROOF STEP]
using s1BC
[PROOF STATE]
proof (prove)
using this:
l \<^bold>\<in> succ k1
?l \<^bold>\<in> succ k1 \<Longrightarrow> Builds B C s1 ?l

goal (1 subgoal):
 1. B (app s1 l) \<or> (\<exists>m\<^bold>\<in>l. \<exists>n\<^bold>\<in>l. C (app s1 l) (app s1 m) (app s1 n))
[PROOF STEP]
by (simp add: Builds_def)
[PROOF STATE]
proof (state)
this:
B (app s1 l) \<or> (\<exists>m\<^bold>\<in>l. \<exists>n\<^bold>\<in>l. C (app s1 l) (app s1 m) (app s1 n))

goal (2 subgoals):
 1. l \<^bold>\<in> succ k1 \<Longrightarrow> Builds B C (seq_append (succ k1) s1 s2) l
 2. \<And>z. \<lbrakk>z \<^bold>\<in> succ k2; l = succ k1 @+ z\<rbrakk> \<Longrightarrow> Builds B C (seq_append (succ k1) s1 s2) l
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
B (app s1 l) \<or> (\<exists>m\<^bold>\<in>l. \<exists>n\<^bold>\<in>l. C (app s1 l) (app s1 m) (app s1 n))

goal (1 subgoal):
 1. Builds B C (seq_append (succ k1) s1 s2) l
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. B (app s1 l) \<Longrightarrow> Builds B C (seq_append (succ k1) s1 s2) l
 2. \<exists>m\<^bold>\<in>l. \<exists>n\<^bold>\<in>l. C (app s1 l) (app s1 m) (app s1 n) \<Longrightarrow> Builds B C (seq_append (succ k1) s1 s2) l
[PROOF STEP]
assume "B (app s1 l)"
[PROOF STATE]
proof (state)
this:
B (app s1 l)

goal (2 subgoals):
 1. B (app s1 l) \<Longrightarrow> Builds B C (seq_append (succ k1) s1 s2) l
 2. \<exists>m\<^bold>\<in>l. \<exists>n\<^bold>\<in>l. C (app s1 l) (app s1 m) (app s1 n) \<Longrightarrow> Builds B C (seq_append (succ k1) s1 s2) l
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
B (app s1 l)

goal (1 subgoal):
 1. Builds B C (seq_append (succ k1) s1 s2) l
[PROOF STEP]
by (metis Builds_def LstSeq_append_app1 l1 s1L)
[PROOF STATE]
proof (state)
this:
Builds B C (seq_append (succ k1) s1 s2) l

goal (1 subgoal):
 1. \<exists>m\<^bold>\<in>l. \<exists>n\<^bold>\<in>l. C (app s1 l) (app s1 m) (app s1 n) \<Longrightarrow> Builds B C (seq_append (succ k1) s1 s2) l
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>m\<^bold>\<in>l. \<exists>n\<^bold>\<in>l. C (app s1 l) (app s1 m) (app s1 n) \<Longrightarrow> Builds B C (seq_append (succ k1) s1 s2) l
[PROOF STEP]
assume "\<exists>m\<^bold>\<in>l. \<exists>n\<^bold>\<in>l. C (app s1 l) (app s1 m) (app s1 n)"
[PROOF STATE]
proof (state)
this:
\<exists>m\<^bold>\<in>l. \<exists>n\<^bold>\<in>l. C (app s1 l) (app s1 m) (app s1 n)

goal (1 subgoal):
 1. \<exists>m\<^bold>\<in>l. \<exists>n\<^bold>\<in>l. C (app s1 l) (app s1 m) (app s1 n) \<Longrightarrow> Builds B C (seq_append (succ k1) s1 s2) l
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>m\<^bold>\<in>l. \<exists>n\<^bold>\<in>l. C (app s1 l) (app s1 m) (app s1 n)
[PROOF STEP]
obtain m n where mn: "m \<^bold>\<in> l" "n \<^bold>\<in> l" and C: "C (app s1 l) (app s1 m) (app s1 n)"
[PROOF STATE]
proof (prove)
using this:
\<exists>m\<^bold>\<in>l. \<exists>n\<^bold>\<in>l. C (app s1 l) (app s1 m) (app s1 n)

goal (1 subgoal):
 1. (\<And>m n. \<lbrakk>m \<^bold>\<in> l; n \<^bold>\<in> l; C (app s1 l) (app s1 m) (app s1 n)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
m \<^bold>\<in> l
n \<^bold>\<in> l
C (app s1 l) (app s1 m) (app s1 n)

goal (1 subgoal):
 1. \<exists>m\<^bold>\<in>l. \<exists>n\<^bold>\<in>l. C (app s1 l) (app s1 m) (app s1 n) \<Longrightarrow> Builds B C (seq_append (succ k1) s1 s2) l
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
m \<^bold>\<in> l
n \<^bold>\<in> l
C (app s1 l) (app s1 m) (app s1 n)

goal (1 subgoal):
 1. \<exists>m\<^bold>\<in>l. \<exists>n\<^bold>\<in>l. C (app s1 l) (app s1 m) (app s1 n) \<Longrightarrow> Builds B C (seq_append (succ k1) s1 s2) l
[PROOF STEP]
have "m \<^bold>\<in> succ k1" "n \<^bold>\<in> succ k1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<^bold>\<in> succ k1 &&& n \<^bold>\<in> succ k1
[PROOF STEP]
by (metis LstSeq_def Ord_trans l1 mn s1L succ_iff)+
[PROOF STATE]
proof (state)
this:
m \<^bold>\<in> succ k1
n \<^bold>\<in> succ k1

goal (1 subgoal):
 1. \<exists>m\<^bold>\<in>l. \<exists>n\<^bold>\<in>l. C (app s1 l) (app s1 m) (app s1 n) \<Longrightarrow> Builds B C (seq_append (succ k1) s1 s2) l
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
m \<^bold>\<in> l
n \<^bold>\<in> l
C (app s1 l) (app s1 m) (app s1 n)
m \<^bold>\<in> succ k1
n \<^bold>\<in> succ k1
[PROOF STEP]
have "C (app (seq_append (succ k1) s1 s2) l)
                         (app (seq_append (succ k1) s1 s2) m)
                         (app (seq_append (succ k1) s1 s2) n)"
[PROOF STATE]
proof (prove)
using this:
m \<^bold>\<in> l
n \<^bold>\<in> l
C (app s1 l) (app s1 m) (app s1 n)
m \<^bold>\<in> succ k1
n \<^bold>\<in> succ k1

goal (1 subgoal):
 1. C (app (seq_append (succ k1) s1 s2) l) (app (seq_append (succ k1) s1 s2) m) (app (seq_append (succ k1) s1 s2) n)
[PROOF STEP]
using s1L l1
[PROOF STATE]
proof (prove)
using this:
m \<^bold>\<in> l
n \<^bold>\<in> l
C (app s1 l) (app s1 m) (app s1 n)
m \<^bold>\<in> succ k1
n \<^bold>\<in> succ k1
LstSeq s1 k1 y1
l \<^bold>\<in> succ k1

goal (1 subgoal):
 1. C (app (seq_append (succ k1) s1 s2) l) (app (seq_append (succ k1) s1 s2) m) (app (seq_append (succ k1) s1 s2) n)
[PROOF STEP]
by (simp add: LstSeq_append_app1)
[PROOF STATE]
proof (state)
this:
C (app (seq_append (succ k1) s1 s2) l) (app (seq_append (succ k1) s1 s2) m) (app (seq_append (succ k1) s1 s2) n)

goal (1 subgoal):
 1. \<exists>m\<^bold>\<in>l. \<exists>n\<^bold>\<in>l. C (app s1 l) (app s1 m) (app s1 n) \<Longrightarrow> Builds B C (seq_append (succ k1) s1 s2) l
[PROOF STEP]
thus "Builds B C (seq_append (succ k1) s1 s2) l"
[PROOF STATE]
proof (prove)
using this:
C (app (seq_append (succ k1) s1 s2) l) (app (seq_append (succ k1) s1 s2) m) (app (seq_append (succ k1) s1 s2) n)

goal (1 subgoal):
 1. Builds B C (seq_append (succ k1) s1 s2) l
[PROOF STEP]
using mn
[PROOF STATE]
proof (prove)
using this:
C (app (seq_append (succ k1) s1 s2) l) (app (seq_append (succ k1) s1 s2) m) (app (seq_append (succ k1) s1 s2) n)
m \<^bold>\<in> l
n \<^bold>\<in> l

goal (1 subgoal):
 1. Builds B C (seq_append (succ k1) s1 s2) l
[PROOF STEP]
by (auto simp: Builds_def)
[PROOF STATE]
proof (state)
this:
Builds B C (seq_append (succ k1) s1 s2) l

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Builds B C (seq_append (succ k1) s1 s2) l

goal (1 subgoal):
 1. \<And>z. \<lbrakk>z \<^bold>\<in> succ k2; l = succ k1 @+ z\<rbrakk> \<Longrightarrow> Builds B C (seq_append (succ k1) s1 s2) l
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>z \<^bold>\<in> succ k2; l = succ k1 @+ z\<rbrakk> \<Longrightarrow> Builds B C (seq_append (succ k1) s1 s2) l
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>z \<^bold>\<in> succ k2; l = succ k1 @+ z\<rbrakk> \<Longrightarrow> Builds B C (seq_append (succ k1) s1 s2) l
[PROOF STEP]
assume z: "z \<^bold>\<in> succ k2" and l2: "l = succ k1 @+ z"
[PROOF STATE]
proof (state)
this:
z \<^bold>\<in> succ k2
l = succ k1 @+ z

goal (1 subgoal):
 1. \<And>z. \<lbrakk>z \<^bold>\<in> succ k2; l = succ k1 @+ z\<rbrakk> \<Longrightarrow> Builds B C (seq_append (succ k1) s1 s2) l
[PROOF STEP]
hence "B (app s2 z) \<or> (\<exists>m\<^bold>\<in>z. \<exists>n\<^bold>\<in>z. C (app s2 z) (app s2 m) (app s2 n))"
[PROOF STATE]
proof (prove)
using this:
z \<^bold>\<in> succ k2
l = succ k1 @+ z

goal (1 subgoal):
 1. B (app s2 z) \<or> (\<exists>m\<^bold>\<in>z. \<exists>n\<^bold>\<in>z. C (app s2 z) (app s2 m) (app s2 n))
[PROOF STEP]
using s2BC
[PROOF STATE]
proof (prove)
using this:
z \<^bold>\<in> succ k2
l = succ k1 @+ z
?l \<^bold>\<in> succ k2 \<Longrightarrow> Builds B C s2 ?l

goal (1 subgoal):
 1. B (app s2 z) \<or> (\<exists>m\<^bold>\<in>z. \<exists>n\<^bold>\<in>z. C (app s2 z) (app s2 m) (app s2 n))
[PROOF STEP]
by (simp add: Builds_def)
[PROOF STATE]
proof (state)
this:
B (app s2 z) \<or> (\<exists>m\<^bold>\<in>z. \<exists>n\<^bold>\<in>z. C (app s2 z) (app s2 m) (app s2 n))

goal (1 subgoal):
 1. \<And>z. \<lbrakk>z \<^bold>\<in> succ k2; l = succ k1 @+ z\<rbrakk> \<Longrightarrow> Builds B C (seq_append (succ k1) s1 s2) l
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
B (app s2 z) \<or> (\<exists>m\<^bold>\<in>z. \<exists>n\<^bold>\<in>z. C (app s2 z) (app s2 m) (app s2 n))

goal (1 subgoal):
 1. Builds B C (seq_append (succ k1) s1 s2) l
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. B (app s2 z) \<Longrightarrow> Builds B C (seq_append (succ k1) s1 s2) l
 2. \<exists>m\<^bold>\<in>z. \<exists>n\<^bold>\<in>z. C (app s2 z) (app s2 m) (app s2 n) \<Longrightarrow> Builds B C (seq_append (succ k1) s1 s2) l
[PROOF STEP]
assume "B (app s2 z)"
[PROOF STATE]
proof (state)
this:
B (app s2 z)

goal (2 subgoals):
 1. B (app s2 z) \<Longrightarrow> Builds B C (seq_append (succ k1) s1 s2) l
 2. \<exists>m\<^bold>\<in>z. \<exists>n\<^bold>\<in>z. C (app s2 z) (app s2 m) (app s2 n) \<Longrightarrow> Builds B C (seq_append (succ k1) s1 s2) l
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
B (app s2 z)

goal (1 subgoal):
 1. Builds B C (seq_append (succ k1) s1 s2) l
[PROOF STEP]
by (metis Builds_def LstSeq_append_app2 l2 s1L s2L)
[PROOF STATE]
proof (state)
this:
Builds B C (seq_append (succ k1) s1 s2) l

goal (1 subgoal):
 1. \<exists>m\<^bold>\<in>z. \<exists>n\<^bold>\<in>z. C (app s2 z) (app s2 m) (app s2 n) \<Longrightarrow> Builds B C (seq_append (succ k1) s1 s2) l
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>m\<^bold>\<in>z. \<exists>n\<^bold>\<in>z. C (app s2 z) (app s2 m) (app s2 n) \<Longrightarrow> Builds B C (seq_append (succ k1) s1 s2) l
[PROOF STEP]
assume "\<exists>m\<^bold>\<in>z. \<exists>n\<^bold>\<in>z. C (app s2 z) (app s2 m) (app s2 n)"
[PROOF STATE]
proof (state)
this:
\<exists>m\<^bold>\<in>z. \<exists>n\<^bold>\<in>z. C (app s2 z) (app s2 m) (app s2 n)

goal (1 subgoal):
 1. \<exists>m\<^bold>\<in>z. \<exists>n\<^bold>\<in>z. C (app s2 z) (app s2 m) (app s2 n) \<Longrightarrow> Builds B C (seq_append (succ k1) s1 s2) l
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>m\<^bold>\<in>z. \<exists>n\<^bold>\<in>z. C (app s2 z) (app s2 m) (app s2 n)
[PROOF STEP]
obtain m n where mn: "m \<^bold>\<in> z" "n \<^bold>\<in> z" and C: "C (app s2 z) (app s2 m) (app s2 n)"
[PROOF STATE]
proof (prove)
using this:
\<exists>m\<^bold>\<in>z. \<exists>n\<^bold>\<in>z. C (app s2 z) (app s2 m) (app s2 n)

goal (1 subgoal):
 1. (\<And>m n. \<lbrakk>m \<^bold>\<in> z; n \<^bold>\<in> z; C (app s2 z) (app s2 m) (app s2 n)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
m \<^bold>\<in> z
n \<^bold>\<in> z
C (app s2 z) (app s2 m) (app s2 n)

goal (1 subgoal):
 1. \<exists>m\<^bold>\<in>z. \<exists>n\<^bold>\<in>z. C (app s2 z) (app s2 m) (app s2 n) \<Longrightarrow> Builds B C (seq_append (succ k1) s1 s2) l
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
m \<^bold>\<in> z
n \<^bold>\<in> z
C (app s2 z) (app s2 m) (app s2 n)

goal (1 subgoal):
 1. \<exists>m\<^bold>\<in>z. \<exists>n\<^bold>\<in>z. C (app s2 z) (app s2 m) (app s2 n) \<Longrightarrow> Builds B C (seq_append (succ k1) s1 s2) l
[PROOF STEP]
have "m \<^bold>\<in> succ k2" "n \<^bold>\<in> succ k2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<^bold>\<in> succ k2 &&& n \<^bold>\<in> succ k2
[PROOF STEP]
using mn
[PROOF STATE]
proof (prove)
using this:
m \<^bold>\<in> z
n \<^bold>\<in> z

goal (1 subgoal):
 1. m \<^bold>\<in> succ k2 &&& n \<^bold>\<in> succ k2
[PROOF STEP]
by (metis LstSeq_def Ord_trans z s2L succ_iff)+
[PROOF STATE]
proof (state)
this:
m \<^bold>\<in> succ k2
n \<^bold>\<in> succ k2

goal (1 subgoal):
 1. \<exists>m\<^bold>\<in>z. \<exists>n\<^bold>\<in>z. C (app s2 z) (app s2 m) (app s2 n) \<Longrightarrow> Builds B C (seq_append (succ k1) s1 s2) l
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
m \<^bold>\<in> z
n \<^bold>\<in> z
C (app s2 z) (app s2 m) (app s2 n)
m \<^bold>\<in> succ k2
n \<^bold>\<in> succ k2
[PROOF STEP]
have "C (app (seq_append (succ k1) s1 s2) l)
                         (app (seq_append (succ k1) s1 s2) (succ k1 @+ m))
                         (app (seq_append (succ k1) s1 s2) (succ k1 @+ n))"
[PROOF STATE]
proof (prove)
using this:
m \<^bold>\<in> z
n \<^bold>\<in> z
C (app s2 z) (app s2 m) (app s2 n)
m \<^bold>\<in> succ k2
n \<^bold>\<in> succ k2

goal (1 subgoal):
 1. C (app (seq_append (succ k1) s1 s2) l) (app (seq_append (succ k1) s1 s2) (succ k1 @+ m)) (app (seq_append (succ k1) s1 s2) (succ k1 @+ n))
[PROOF STEP]
using s1L s2L l2 z
[PROOF STATE]
proof (prove)
using this:
m \<^bold>\<in> z
n \<^bold>\<in> z
C (app s2 z) (app s2 m) (app s2 n)
m \<^bold>\<in> succ k2
n \<^bold>\<in> succ k2
LstSeq s1 k1 y1
LstSeq s2 k2 y2
l = succ k1 @+ z
z \<^bold>\<in> succ k2

goal (1 subgoal):
 1. C (app (seq_append (succ k1) s1 s2) l) (app (seq_append (succ k1) s1 s2) (succ k1 @+ m)) (app (seq_append (succ k1) s1 s2) (succ k1 @+ n))
[PROOF STEP]
by (simp add: LstSeq_append_app2)
[PROOF STATE]
proof (state)
this:
C (app (seq_append (succ k1) s1 s2) l) (app (seq_append (succ k1) s1 s2) (succ k1 @+ m)) (app (seq_append (succ k1) s1 s2) (succ k1 @+ n))

goal (1 subgoal):
 1. \<exists>m\<^bold>\<in>z. \<exists>n\<^bold>\<in>z. C (app s2 z) (app s2 m) (app s2 n) \<Longrightarrow> Builds B C (seq_append (succ k1) s1 s2) l
[PROOF STEP]
thus "Builds B C (seq_append (succ k1) s1 s2) l"
[PROOF STATE]
proof (prove)
using this:
C (app (seq_append (succ k1) s1 s2) l) (app (seq_append (succ k1) s1 s2) (succ k1 @+ m)) (app (seq_append (succ k1) s1 s2) (succ k1 @+ n))

goal (1 subgoal):
 1. Builds B C (seq_append (succ k1) s1 s2) l
[PROOF STEP]
using mn l2
[PROOF STATE]
proof (prove)
using this:
C (app (seq_append (succ k1) s1 s2) l) (app (seq_append (succ k1) s1 s2) (succ k1 @+ m)) (app (seq_append (succ k1) s1 s2) (succ k1 @+ n))
m \<^bold>\<in> z
n \<^bold>\<in> z
l = succ k1 @+ z

goal (1 subgoal):
 1. Builds B C (seq_append (succ k1) s1 s2) l
[PROOF STEP]
by (auto simp: Builds_def HBall_def)
[PROOF STATE]
proof (state)
this:
Builds B C (seq_append (succ k1) s1 s2) l

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Builds B C (seq_append (succ k1) s1 s2) l

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Builds B C (seq_append (succ k1) s1 s2) l

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma BuildSeq_combine:
  assumes b1: "BuildSeq B C s1 k1 y1" and b2: "BuildSeq B C s2 k2 y2"
      and y: "C y y1 y2"
  shows "BuildSeq B C (insf (seq_append (succ k1) s1 s2) (succ (succ (k1 @+ k2))) y) (succ (succ (k1 @+ k2))) y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. BuildSeq B C (insf (seq_append (succ k1) s1 s2) (succ (succ (k1 @+ k2))) y) (succ (succ (k1 @+ k2))) y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. BuildSeq B C (insf (seq_append (succ k1) s1 s2) (succ (succ (k1 @+ k2))) y) (succ (succ (k1 @+ k2))) y
[PROOF STEP]
have k2: "Ord k2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ord k2
[PROOF STEP]
using b2
[PROOF STATE]
proof (prove)
using this:
BuildSeq B C s2 k2 y2

goal (1 subgoal):
 1. Ord k2
[PROOF STEP]
by (auto simp: BuildSeq_def LstSeq_def)
[PROOF STATE]
proof (state)
this:
Ord k2

goal (1 subgoal):
 1. BuildSeq B C (insf (seq_append (succ k1) s1 s2) (succ (succ (k1 @+ k2))) y) (succ (succ (k1 @+ k2))) y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. BuildSeq B C (insf (seq_append (succ k1) s1 s2) (succ (succ (k1 @+ k2))) y) (succ (succ (k1 @+ k2))) y
[PROOF STEP]
proof (rule BuildSeq_insf [where m=k1 and n="succ(k1@+k2)"])
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. BuildSeq B C (seq_append (succ k1) s1 s2) (succ (k1 @+ k2)) ?z
 2. k1 \<^bold>\<in> succ (succ (k1 @+ k2))
 3. succ (k1 @+ k2) \<^bold>\<in> succ (succ (k1 @+ k2))
 4. B y \<or> C y (app (seq_append (succ k1) s1 s2) k1) (app (seq_append (succ k1) s1 s2) (succ (k1 @+ k2)))
[PROOF STEP]
show "BuildSeq B C (seq_append (succ k1) s1 s2) (succ (k1 @+ k2)) y2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. BuildSeq B C (seq_append (succ k1) s1 s2) (succ (k1 @+ k2)) y2
[PROOF STEP]
by (rule BuildSeq_append [OF b1 b2])
[PROOF STATE]
proof (state)
this:
BuildSeq B C (seq_append (succ k1) s1 s2) (succ (k1 @+ k2)) y2

goal (3 subgoals):
 1. k1 \<^bold>\<in> succ (succ (k1 @+ k2))
 2. succ (k1 @+ k2) \<^bold>\<in> succ (succ (k1 @+ k2))
 3. B y \<or> C y (app (seq_append (succ k1) s1 s2) k1) (app (seq_append (succ k1) s1 s2) (succ (k1 @+ k2)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. k1 \<^bold>\<in> succ (succ (k1 @+ k2))
 2. succ (k1 @+ k2) \<^bold>\<in> succ (succ (k1 @+ k2))
 3. B y \<or> C y (app (seq_append (succ k1) s1 s2) k1) (app (seq_append (succ k1) s1 s2) (succ (k1 @+ k2)))
[PROOF STEP]
show "k1 \<^bold>\<in> succ (succ (k1 @+ k2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k1 \<^bold>\<in> succ (succ (k1 @+ k2))
[PROOF STEP]
using k2
[PROOF STATE]
proof (prove)
using this:
Ord k2

goal (1 subgoal):
 1. k1 \<^bold>\<in> succ (succ (k1 @+ k2))
[PROOF STEP]
by (metis hadd_0_right hmem_0_Ord hmem_self_hadd succ_iff)
[PROOF STATE]
proof (state)
this:
k1 \<^bold>\<in> succ (succ (k1 @+ k2))

goal (2 subgoals):
 1. succ (k1 @+ k2) \<^bold>\<in> succ (succ (k1 @+ k2))
 2. B y \<or> C y (app (seq_append (succ k1) s1 s2) k1) (app (seq_append (succ k1) s1 s2) (succ (k1 @+ k2)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. succ (k1 @+ k2) \<^bold>\<in> succ (succ (k1 @+ k2))
 2. B y \<or> C y (app (seq_append (succ k1) s1 s2) k1) (app (seq_append (succ k1) s1 s2) (succ (k1 @+ k2)))
[PROOF STEP]
show "succ (k1 @+ k2) \<^bold>\<in> succ (succ (k1 @+ k2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. succ (k1 @+ k2) \<^bold>\<in> succ (succ (k1 @+ k2))
[PROOF STEP]
by (metis succ_iff)
[PROOF STATE]
proof (state)
this:
succ (k1 @+ k2) \<^bold>\<in> succ (succ (k1 @+ k2))

goal (1 subgoal):
 1. B y \<or> C y (app (seq_append (succ k1) s1 s2) k1) (app (seq_append (succ k1) s1 s2) (succ (k1 @+ k2)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. B y \<or> C y (app (seq_append (succ k1) s1 s2) k1) (app (seq_append (succ k1) s1 s2) (succ (k1 @+ k2)))
[PROOF STEP]
have [simp]: "app (seq_append (succ k1) s1 s2) k1 = y1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. app (seq_append (succ k1) s1 s2) k1 = y1
[PROOF STEP]
by (metis b1 BuildSeq_imp_LstSeq LstSeq_app LstSeq_append_app1 succ_iff)
[PROOF STATE]
proof (state)
this:
app (seq_append (succ k1) s1 s2) k1 = y1

goal (1 subgoal):
 1. B y \<or> C y (app (seq_append (succ k1) s1 s2) k1) (app (seq_append (succ k1) s1 s2) (succ (k1 @+ k2)))
[PROOF STEP]
have [simp]: "app (seq_append (succ k1) s1 s2) (succ (k1 @+ k2)) = y2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. app (seq_append (succ k1) s1 s2) (succ (k1 @+ k2)) = y2
[PROOF STEP]
by (metis b1 b2 k2 BuildSeq_imp_LstSeq LstSeq_app LstSeq_append_app2 hadd_succ_left)
[PROOF STATE]
proof (state)
this:
app (seq_append (succ k1) s1 s2) (succ (k1 @+ k2)) = y2

goal (1 subgoal):
 1. B y \<or> C y (app (seq_append (succ k1) s1 s2) k1) (app (seq_append (succ k1) s1 s2) (succ (k1 @+ k2)))
[PROOF STEP]
show "B y \<or>
          C y (app (seq_append (succ k1) s1 s2) k1)
              (app (seq_append (succ k1) s1 s2) (succ (k1 @+ k2)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B y \<or> C y (app (seq_append (succ k1) s1 s2) k1) (app (seq_append (succ k1) s1 s2) (succ (k1 @+ k2)))
[PROOF STEP]
using y
[PROOF STATE]
proof (prove)
using this:
C y y1 y2

goal (1 subgoal):
 1. B y \<or> C y (app (seq_append (succ k1) s1 s2) k1) (app (seq_append (succ k1) s1 s2) (succ (k1 @+ k2)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
B y \<or> C y (app (seq_append (succ k1) s1 s2) k1) (app (seq_append (succ k1) s1 s2) (succ (k1 @+ k2)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
BuildSeq B C (insf (seq_append (succ k1) s1 s2) (succ (succ (k1 @+ k2))) y) (succ (succ (k1 @+ k2))) y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma LstSeq_1: "LstSeq \<lbrace>\<langle>0, y\<rangle>\<rbrace> 0 y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LstSeq \<lbrace>\<langle>0, y\<rangle>\<rbrace> 0 y
[PROOF STEP]
by (auto simp: LstSeq_def One_hf_eq_succ Seq_ins OrdDom_def)


[STATEMENT]
lemma BuildSeq_1: "B y \<Longrightarrow> BuildSeq B C \<lbrace>\<langle>0, y\<rangle>\<rbrace> 0 y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B y \<Longrightarrow> BuildSeq B C \<lbrace>\<langle>0, y\<rangle>\<rbrace> 0 y
[PROOF STEP]
by (auto simp: BuildSeq_def Builds_def LstSeq_1)


[STATEMENT]
lemma BuildSeq_exI: "B t \<Longrightarrow> \<exists>s k. BuildSeq B C s k t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B t \<Longrightarrow> \<exists>s k. BuildSeq B C s k t
[PROOF STEP]
by (metis BuildSeq_1)


[STATEMENT]
lemma BuildSeq_succ_E:
    assumes s: "BuildSeq B C s k y"
      obtains "B y" |  m n where "m \<^bold>\<in> k" "n \<^bold>\<in> k" "C y (app s m) (app s n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>B y \<Longrightarrow> thesis; \<And>m n. \<lbrakk>m \<^bold>\<in> k; n \<^bold>\<in> k; C y (app s m) (app s n)\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>B y \<Longrightarrow> thesis; \<And>m n. \<lbrakk>m \<^bold>\<in> k; n \<^bold>\<in> k; C y (app s m) (app s n)\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have Bs: "Builds B C s k" and apps: "app s k = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Builds B C s k &&& app s k = y
[PROOF STEP]
using s
[PROOF STATE]
proof (prove)
using this:
BuildSeq B C s k y

goal (1 subgoal):
 1. Builds B C s k &&& app s k = y
[PROOF STEP]
by (auto simp: BuildSeq_def)
[PROOF STATE]
proof (state)
this:
Builds B C s k
app s k = y

goal (1 subgoal):
 1. \<lbrakk>B y \<Longrightarrow> thesis; \<And>m n. \<lbrakk>m \<^bold>\<in> k; n \<^bold>\<in> k; C y (app s m) (app s n)\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
hence "B y \<or> (\<exists>m \<^bold>\<in> k. \<exists>n \<^bold>\<in> k. C y (app s m) (app s n))"
[PROOF STATE]
proof (prove)
using this:
Builds B C s k
app s k = y

goal (1 subgoal):
 1. B y \<or> (\<exists>m\<^bold>\<in>k. \<exists>n\<^bold>\<in>k. C y (app s m) (app s n))
[PROOF STEP]
by (metis Builds_def apps Bs)
[PROOF STATE]
proof (state)
this:
B y \<or> (\<exists>m\<^bold>\<in>k. \<exists>n\<^bold>\<in>k. C y (app s m) (app s n))

goal (1 subgoal):
 1. \<lbrakk>B y \<Longrightarrow> thesis; \<And>m n. \<lbrakk>m \<^bold>\<in> k; n \<^bold>\<in> k; C y (app s m) (app s n)\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
B y \<or> (\<exists>m\<^bold>\<in>k. \<exists>n\<^bold>\<in>k. C y (app s m) (app s n))

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
B y \<or> (\<exists>m\<^bold>\<in>k. \<exists>n\<^bold>\<in>k. C y (app s m) (app s n))
B y \<Longrightarrow> thesis
\<lbrakk>?m \<^bold>\<in> k; ?n \<^bold>\<in> k; C y (app s ?m) (app s ?n)\<rbrakk> \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma BuildSeq_induct [consumes 1, case_names B C]:
  assumes major: "BuildSeq B C s k a"
      and B: "\<And>x. B x \<Longrightarrow> P x"
      and C: "\<And>x y z. C x y z \<Longrightarrow> P y \<Longrightarrow> P z \<Longrightarrow> P x"
  shows "P a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P a
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P a
[PROOF STEP]
have "Ord k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ord k
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
BuildSeq B C s k a
B ?x \<Longrightarrow> P ?x
\<lbrakk>C ?x ?y ?z; P ?y; P ?z\<rbrakk> \<Longrightarrow> P ?x

goal (1 subgoal):
 1. Ord k
[PROOF STEP]
by (auto simp: BuildSeq_def LstSeq_def)
[PROOF STATE]
proof (state)
this:
Ord k

goal (1 subgoal):
 1. P a
[PROOF STEP]
hence "\<And>a s. BuildSeq B C s k a \<Longrightarrow> P a"
[PROOF STATE]
proof (prove)
using this:
Ord k

goal (1 subgoal):
 1. \<And>a s. BuildSeq B C s k a \<Longrightarrow> P a
[PROOF STEP]
by (induction k rule: Ord_induct) (metis BuildSeq_trunc BuildSeq_succ_E B C)
[PROOF STATE]
proof (state)
this:
BuildSeq B C ?s k ?a \<Longrightarrow> P ?a

goal (1 subgoal):
 1. P a
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
BuildSeq B C ?s k ?a \<Longrightarrow> P ?a

goal (1 subgoal):
 1. P a
[PROOF STEP]
by (metis major)
[PROOF STATE]
proof (state)
this:
P a

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma BuildSeq2_combine:
  assumes b1: "BuildSeq2 B C s1 k1 y1 y1'" and b2: "BuildSeq2 B C s2 k2 y2 y2'"
      and y: "C y y' y1 y1' y2 y2'"
  shows "BuildSeq2 B C (insf (seq_append (succ k1) s1 s2) (succ (succ (k1 @+ k2))) \<langle>y, y'\<rangle>)
                       (succ (succ (k1 @+ k2))) y y'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. BuildSeq2 B C (insf (seq_append (succ k1) s1 s2) (succ (succ (k1 @+ k2))) \<langle>y, y'\<rangle>) (succ (succ (k1 @+ k2))) y y'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
BuildSeq2 B C s1 k1 y1 y1'
BuildSeq2 B C s2 k2 y2 y2'
C y y' y1 y1' y2 y2'

goal (1 subgoal):
 1. BuildSeq2 B C (insf (seq_append (succ k1) s1 s2) (succ (succ (k1 @+ k2))) \<langle>y, y'\<rangle>) (succ (succ (k1 @+ k2))) y y'
[PROOF STEP]
apply (unfold BuildSeq2_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>BuildSeq (\<lambda>p. \<exists>x x'. p = \<langle>x, x'\<rangle> \<and> B x x') (\<lambda>p q r. \<exists>x x' y y' z z'. p = \<langle>x, x'\<rangle> \<and> q = \<langle>y, y'\<rangle> \<and> r = \<langle>z, z'\<rangle> \<and> C x x' y y' z z') s1 k1 \<langle>y1, y1'\<rangle>; BuildSeq (\<lambda>p. \<exists>x x'. p = \<langle>x, x'\<rangle> \<and> B x x') (\<lambda>p q r. \<exists>x x' y y' z z'. p = \<langle>x, x'\<rangle> \<and> q = \<langle>y, y'\<rangle> \<and> r = \<langle>z, z'\<rangle> \<and> C x x' y y' z z') s2 k2 \<langle>y2, y2'\<rangle>; C y y' y1 y1' y2 y2'\<rbrakk> \<Longrightarrow> BuildSeq (\<lambda>p. \<exists>x x'. p = \<langle>x, x'\<rangle> \<and> B x x') (\<lambda>p q r. \<exists>x x' y y' z z'. p = \<langle>x, x'\<rangle> \<and> q = \<langle>y, y'\<rangle> \<and> r = \<langle>z, z'\<rangle> \<and> C x x' y y' z z') (insf (seq_append (succ k1) s1 s2) (succ (succ (k1 @+ k2))) \<langle>y, y'\<rangle>) (succ (succ (k1 @+ k2))) \<langle>y, y'\<rangle>
[PROOF STEP]
apply (blast intro: BuildSeq_combine)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma BuildSeq2_1: "B y y' \<Longrightarrow> BuildSeq2 B C \<lbrace>\<langle>0, y, y'\<rangle>\<rbrace> 0 y y'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B y y' \<Longrightarrow> BuildSeq2 B C \<lbrace>\<langle>0, y, y'\<rangle>\<rbrace> 0 y y'
[PROOF STEP]
by (auto simp: BuildSeq2_def BuildSeq_1)


[STATEMENT]
lemma BuildSeq2_induct [consumes 1, case_names B C]:
  assumes "BuildSeq2 B C s k a a'"
      and B: "\<And>x x'. B x x' \<Longrightarrow> P x x'"
      and C: "\<And>x x' y y' z z'. C x x' y y' z z' \<Longrightarrow> P y y' \<Longrightarrow> P z z' \<Longrightarrow> P x x'"
  shows "P a a'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P a a'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
BuildSeq2 B C s k a a'
B ?x ?x' \<Longrightarrow> P ?x ?x'
\<lbrakk>C ?x ?x' ?y ?y' ?z ?z'; P ?y ?y'; P ?z ?z'\<rbrakk> \<Longrightarrow> P ?x ?x'

goal (1 subgoal):
 1. P a a'
[PROOF STEP]
apply (simp add: BuildSeq2_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>BuildSeq (\<lambda>p. \<exists>x x'. p = \<langle>x, x'\<rangle> \<and> B x x') (\<lambda>p q r. \<exists>x x'. p = \<langle>x, x'\<rangle> \<and> (\<exists>y y'. q = \<langle>y, y'\<rangle> \<and> (\<exists>z z'. r = \<langle>z, z'\<rangle> \<and> C x x' y y' z z'))) s k \<langle>a, a'\<rangle>; \<And>x x'. B x x' \<Longrightarrow> P x x'; \<And>x x' y y' z z'. \<lbrakk>C x x' y y' z z'; P y y'; P z z'\<rbrakk> \<Longrightarrow> P x x'\<rbrakk> \<Longrightarrow> P a a'
[PROOF STEP]
apply (drule BuildSeq_induct [where P = "\<lambda>\<langle>x,x'\<rangle>. P x x'"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>\<And>x x'. B x x' \<Longrightarrow> P x x'; \<And>x x' y y' z z'. \<lbrakk>C x x' y y' z z'; P y y'; P z z'\<rbrakk> \<Longrightarrow> P x x'; \<exists>xa x'. x = \<langle>xa, x'\<rangle> \<and> B xa x'\<rbrakk> \<Longrightarrow> hsplit P x
 2. \<And>x y z. \<lbrakk>\<And>x x'. B x x' \<Longrightarrow> P x x'; \<And>x x' y y' z z'. \<lbrakk>C x x' y y' z z'; P y y'; P z z'\<rbrakk> \<Longrightarrow> P x x'; \<exists>xa x'. x = \<langle>xa, x'\<rangle> \<and> (\<exists>ya y'. y = \<langle>ya, y'\<rangle> \<and> (\<exists>za z'. z = \<langle>za, z'\<rangle> \<and> C xa x' ya y' za z')); hsplit P y; hsplit P z\<rbrakk> \<Longrightarrow> hsplit P x
 3. \<lbrakk>\<And>x x'. B x x' \<Longrightarrow> P x x'; \<And>x x' y y' z z'. \<lbrakk>C x x' y y' z z'; P y y'; P z z'\<rbrakk> \<Longrightarrow> P x x'; hsplit P \<langle>a, a'\<rangle>\<rbrakk> \<Longrightarrow> P a a'
[PROOF STEP]
apply (auto intro: B C)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma BuildSeq3_combine:
  assumes b1: "BuildSeq3 B C s1 k1 y1 y1' y1''" and b2: "BuildSeq3 B C s2 k2 y2 y2' y2''"
      and y: "C y y' y'' y1 y1' y1'' y2 y2' y2''"
  shows "BuildSeq3 B C (insf (seq_append (succ k1) s1 s2) (succ (succ (k1 @+ k2))) \<langle>y, y', y''\<rangle>)
                       (succ (succ (k1 @+ k2))) y y' y''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. BuildSeq3 B C (insf (seq_append (succ k1) s1 s2) (succ (succ (k1 @+ k2))) \<langle>y, y', y''\<rangle>) (succ (succ (k1 @+ k2))) y y' y''
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
BuildSeq3 B C s1 k1 y1 y1' y1''
BuildSeq3 B C s2 k2 y2 y2' y2''
C y y' y'' y1 y1' y1'' y2 y2' y2''

goal (1 subgoal):
 1. BuildSeq3 B C (insf (seq_append (succ k1) s1 s2) (succ (succ (k1 @+ k2))) \<langle>y, y', y''\<rangle>) (succ (succ (k1 @+ k2))) y y' y''
[PROOF STEP]
apply (unfold BuildSeq3_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>BuildSeq (\<lambda>p. \<exists>x x' x''. p = \<langle>x, x', x''\<rangle> \<and> B x x' x'') (\<lambda>p q r. \<exists>x x' x'' y y' y'' z z' z''. p = \<langle>x, x', x''\<rangle> \<and> q = \<langle>y, y', y''\<rangle> \<and> r = \<langle>z, z', z''\<rangle> \<and> C x x' x'' y y' y'' z z' z'') s1 k1 \<langle>y1, y1', y1''\<rangle>; BuildSeq (\<lambda>p. \<exists>x x' x''. p = \<langle>x, x', x''\<rangle> \<and> B x x' x'') (\<lambda>p q r. \<exists>x x' x'' y y' y'' z z' z''. p = \<langle>x, x', x''\<rangle> \<and> q = \<langle>y, y', y''\<rangle> \<and> r = \<langle>z, z', z''\<rangle> \<and> C x x' x'' y y' y'' z z' z'') s2 k2 \<langle>y2, y2', y2''\<rangle>; C y y' y'' y1 y1' y1'' y2 y2' y2''\<rbrakk> \<Longrightarrow> BuildSeq (\<lambda>p. \<exists>x x' x''. p = \<langle>x, x', x''\<rangle> \<and> B x x' x'') (\<lambda>p q r. \<exists>x x' x'' y y' y'' z z' z''. p = \<langle>x, x', x''\<rangle> \<and> q = \<langle>y, y', y''\<rangle> \<and> r = \<langle>z, z', z''\<rangle> \<and> C x x' x'' y y' y'' z z' z'') (insf (seq_append (succ k1) s1 s2) (succ (succ (k1 @+ k2))) \<langle>y, y', y''\<rangle>) (succ (succ (k1 @+ k2))) \<langle>y, y', y''\<rangle>
[PROOF STEP]
apply (blast intro: BuildSeq_combine)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma BuildSeq3_1: "B y y' y'' \<Longrightarrow> BuildSeq3 B C \<lbrace>\<langle>0, y, y', y''\<rangle>\<rbrace> 0 y y' y''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B y y' y'' \<Longrightarrow> BuildSeq3 B C \<lbrace>\<langle>0, y, y', y''\<rangle>\<rbrace> 0 y y' y''
[PROOF STEP]
by (auto simp: BuildSeq3_def BuildSeq_1)


[STATEMENT]
lemma BuildSeq3_exI: "B t t' t'' \<Longrightarrow> \<exists>s k. BuildSeq3 B C s k t t' t''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B t t' t'' \<Longrightarrow> \<exists>s k. BuildSeq3 B C s k t t' t''
[PROOF STEP]
by (metis BuildSeq3_1)


[STATEMENT]
lemma BuildSeq3_induct [consumes 1, case_names B C]:
  assumes "BuildSeq3 B C s k a a' a''"
      and B: "\<And>x x' x''. B x x' x'' \<Longrightarrow> P x x' x''"
      and C: "\<And>x x' x'' y y' y'' z z' z''. C x x' x'' y y' y'' z z' z'' \<Longrightarrow> P y y' y'' \<Longrightarrow> P z z' z'' \<Longrightarrow> P x x' x''"
  shows "P a a' a''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P a a' a''
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
BuildSeq3 B C s k a a' a''
B ?x ?x' ?x'' \<Longrightarrow> P ?x ?x' ?x''
\<lbrakk>C ?x ?x' ?x'' ?y ?y' ?y'' ?z ?z' ?z''; P ?y ?y' ?y''; P ?z ?z' ?z''\<rbrakk> \<Longrightarrow> P ?x ?x' ?x''

goal (1 subgoal):
 1. P a a' a''
[PROOF STEP]
apply (simp add: BuildSeq3_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>BuildSeq (\<lambda>p. \<exists>x x' x''. p = \<langle>x, x', x''\<rangle> \<and> B x x' x'') (\<lambda>p q r. \<exists>x x' x''. p = \<langle>x, x', x''\<rangle> \<and> (\<exists>y y' y''. q = \<langle>y, y', y''\<rangle> \<and> (\<exists>z z' z''. r = \<langle>z, z', z''\<rangle> \<and> C x x' x'' y y' y'' z z' z''))) s k \<langle>a, a', a''\<rangle>; \<And>x x' x''. B x x' x'' \<Longrightarrow> P x x' x''; \<And>x x' x'' y y' y'' z z' z''. \<lbrakk>C x x' x'' y y' y'' z z' z''; P y y' y''; P z z' z''\<rbrakk> \<Longrightarrow> P x x' x''\<rbrakk> \<Longrightarrow> P a a' a''
[PROOF STEP]
apply (drule BuildSeq_induct [where P = "\<lambda>\<langle>x,x',x''\<rangle>. P x x' x''"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>\<And>x x' x''. B x x' x'' \<Longrightarrow> P x x' x''; \<And>x x' x'' y y' y'' z z' z''. \<lbrakk>C x x' x'' y y' y'' z z' z''; P y y' y''; P z z' z''\<rbrakk> \<Longrightarrow> P x x' x''; \<exists>xa x' x''. x = \<langle>xa, x', x''\<rangle> \<and> B xa x' x''\<rbrakk> \<Longrightarrow> hsplit (\<lambda>x. hsplit (P x)) x
 2. \<And>x y z. \<lbrakk>\<And>x x' x''. B x x' x'' \<Longrightarrow> P x x' x''; \<And>x x' x'' y y' y'' z z' z''. \<lbrakk>C x x' x'' y y' y'' z z' z''; P y y' y''; P z z' z''\<rbrakk> \<Longrightarrow> P x x' x''; \<exists>xa x' x''. x = \<langle>xa, x', x''\<rangle> \<and> (\<exists>ya y' y''. y = \<langle>ya, y', y''\<rangle> \<and> (\<exists>za z' z''. z = \<langle>za, z', z''\<rangle> \<and> C xa x' x'' ya y' y'' za z' z'')); hsplit (\<lambda>x. hsplit (P x)) y; hsplit (\<lambda>x. hsplit (P x)) z\<rbrakk> \<Longrightarrow> hsplit (\<lambda>x. hsplit (P x)) x
 3. \<lbrakk>\<And>x x' x''. B x x' x'' \<Longrightarrow> P x x' x''; \<And>x x' x'' y y' y'' z z' z''. \<lbrakk>C x x' x'' y y' y'' z z' z''; P y y' y''; P z z' z''\<rbrakk> \<Longrightarrow> P x x' x''; hsplit (\<lambda>x. hsplit (P x)) \<langle>a, a', a''\<rangle>\<rbrakk> \<Longrightarrow> P a a' a''
[PROOF STEP]
apply (auto intro: B C)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Rep_hf_0 [simp]: "Rep_hf 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_hf 0 = 0
[PROOF STEP]
by (metis Abs_hf_inverse HF.HF_def UNIV_I Zero_hf_def image_empty set_encode_empty)


[STATEMENT]
lemma hmem_imp_less: "x \<^bold>\<in> y \<Longrightarrow> Rep_hf x < Rep_hf y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<^bold>\<in> y \<Longrightarrow> Rep_hf x < Rep_hf y
[PROOF STEP]
apply (auto simp: hmem_def hfset_def set_decode_def Abs_hf_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x = Abs_hf xa; odd (Rep_hf y div 2 ^ xa)\<rbrakk> \<Longrightarrow> xa < Rep_hf y
[PROOF STEP]
apply (metis div_less even_zero le_less_trans less_two_power not_less)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hsubset_imp_le: "x \<le> y \<Longrightarrow> Rep_hf x \<le> Rep_hf y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> Rep_hf x \<le> Rep_hf y
[PROOF STEP]
apply (auto simp: less_eq_hf_def hmem_def hfset_def Abs_hf_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>xa. xa \<in> Abs_hf ` set_decode (Rep_hf x) \<longrightarrow> xa \<in> Abs_hf ` set_decode (Rep_hf y) \<Longrightarrow> Rep_hf x \<le> Rep_hf y
[PROOF STEP]
apply (cases x rule: Abs_hf_cases)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ya. \<lbrakk>\<forall>xa. xa \<in> Abs_hf ` set_decode (Rep_hf x) \<longrightarrow> xa \<in> Abs_hf ` set_decode (Rep_hf y); x = Abs_hf ya; ya \<in> UNIV\<rbrakk> \<Longrightarrow> Rep_hf x \<le> Rep_hf y
[PROOF STEP]
apply (cases y rule: Abs_hf_cases, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ya yaa. \<lbrakk>\<forall>x. x \<in> Abs_hf ` set_decode (Rep_hf (Abs_hf ya)) \<longrightarrow> x \<in> Abs_hf ` set_decode (Rep_hf (Abs_hf yaa)); x = Abs_hf ya; y = Abs_hf yaa\<rbrakk> \<Longrightarrow> Rep_hf (Abs_hf ya) \<le> Rep_hf (Abs_hf yaa)
[PROOF STEP]
apply (rule subset_decode_imp_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ya yaa. \<lbrakk>\<forall>x. x \<in> Abs_hf ` set_decode (Rep_hf (Abs_hf ya)) \<longrightarrow> x \<in> Abs_hf ` set_decode (Rep_hf (Abs_hf yaa)); x = Abs_hf ya; y = Abs_hf yaa\<rbrakk> \<Longrightarrow> set_decode (Rep_hf (Abs_hf ya)) \<subseteq> set_decode (Rep_hf (Abs_hf yaa))
[PROOF STEP]
apply (auto simp: Abs_hf_inverse [OF UNIV_I])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ya yaa xa. \<lbrakk>\<forall>x. x \<in> Abs_hf ` set_decode ya \<longrightarrow> x \<in> Abs_hf ` set_decode yaa; x = Abs_hf ya; y = Abs_hf yaa; xa \<in> set_decode ya\<rbrakk> \<Longrightarrow> xa \<in> set_decode yaa
[PROOF STEP]
apply (metis Abs_hf_inverse UNIV_I imageE imageI)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma least_equality:
  assumes "x \<^bold>\<in> a" and "\<And>y. y \<^bold>\<in> a \<Longrightarrow> Rep_hf x \<le> Rep_hf y"
  shows "least a = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. least a = x
[PROOF STEP]
unfolding least_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (THE x. x \<^bold>\<in> a \<and> (\<forall>y. y \<^bold>\<in> a \<longrightarrow> Rep_hf x \<le> Rep_hf y)) = x
[PROOF STEP]
apply (rule the_equality)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. x \<^bold>\<in> a \<and> (\<forall>y. y \<^bold>\<in> a \<longrightarrow> Rep_hf x \<le> Rep_hf y)
 2. \<And>xa. xa \<^bold>\<in> a \<and> (\<forall>y. y \<^bold>\<in> a \<longrightarrow> Rep_hf xa \<le> Rep_hf y) \<Longrightarrow> xa = x
[PROOF STEP]
apply (metis assms)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. xa \<^bold>\<in> a \<and> (\<forall>y. y \<^bold>\<in> a \<longrightarrow> Rep_hf xa \<le> Rep_hf y) \<Longrightarrow> xa = x
[PROOF STEP]
apply (metis Rep_hf_inverse assms eq_iff)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma leastI2_order:
  assumes "x \<^bold>\<in> a"
    and "\<And>y. y \<^bold>\<in> a \<Longrightarrow> Rep_hf x \<le> Rep_hf y"
    and "\<And>z. z \<^bold>\<in> a \<Longrightarrow> \<forall>y. y \<^bold>\<in> a \<longrightarrow> Rep_hf z \<le> Rep_hf y \<Longrightarrow> Q z"
  shows "Q (least a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q (least a)
[PROOF STEP]
by (metis assms least_equality)


[STATEMENT]
lemma nonempty_imp_ex_least: "a \<noteq> 0 \<Longrightarrow> \<exists>x. x \<^bold>\<in> a \<and> (\<forall>y. y \<^bold>\<in> a \<longrightarrow> Rep_hf x \<le> Rep_hf y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<noteq> 0 \<Longrightarrow> \<exists>x. x \<^bold>\<in> a \<and> (\<forall>y. y \<^bold>\<in> a \<longrightarrow> Rep_hf x \<le> Rep_hf y)
[PROOF STEP]
proof (induction a rule: hf_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 \<noteq> 0 \<Longrightarrow> \<exists>x. x \<^bold>\<in> 0 \<and> (\<forall>y. y \<^bold>\<in> 0 \<longrightarrow> Rep_hf x \<le> Rep_hf y)
 2. \<And>x y. \<lbrakk>x \<noteq> 0 \<Longrightarrow> \<exists>xa. xa \<^bold>\<in> x \<and> (\<forall>y. y \<^bold>\<in> x \<longrightarrow> Rep_hf xa \<le> Rep_hf y); y \<noteq> 0 \<Longrightarrow> \<exists>x. x \<^bold>\<in> y \<and> (\<forall>ya. ya \<^bold>\<in> y \<longrightarrow> Rep_hf x \<le> Rep_hf ya); x \<^bold>\<notin> y; y \<triangleleft> x \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>xa. xa \<^bold>\<in> y \<triangleleft> x \<and> (\<forall>ya. ya \<^bold>\<in> y \<triangleleft> x \<longrightarrow> Rep_hf xa \<le> Rep_hf ya)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
0 \<noteq> 0

goal (2 subgoals):
 1. 0 \<noteq> 0 \<Longrightarrow> \<exists>x. x \<^bold>\<in> 0 \<and> (\<forall>y. y \<^bold>\<in> 0 \<longrightarrow> Rep_hf x \<le> Rep_hf y)
 2. \<And>x y. \<lbrakk>x \<noteq> 0 \<Longrightarrow> \<exists>xa. xa \<^bold>\<in> x \<and> (\<forall>y. y \<^bold>\<in> x \<longrightarrow> Rep_hf xa \<le> Rep_hf y); y \<noteq> 0 \<Longrightarrow> \<exists>x. x \<^bold>\<in> y \<and> (\<forall>ya. ya \<^bold>\<in> y \<longrightarrow> Rep_hf x \<le> Rep_hf ya); x \<^bold>\<notin> y; y \<triangleleft> x \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>xa. xa \<^bold>\<in> y \<triangleleft> x \<and> (\<forall>ya. ya \<^bold>\<in> y \<triangleleft> x \<longrightarrow> Rep_hf xa \<le> Rep_hf ya)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
0 \<noteq> 0

goal (1 subgoal):
 1. \<exists>x. x \<^bold>\<in> 0 \<and> (\<forall>y. y \<^bold>\<in> 0 \<longrightarrow> Rep_hf x \<le> Rep_hf y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>x. x \<^bold>\<in> 0 \<and> (\<forall>y. y \<^bold>\<in> 0 \<longrightarrow> Rep_hf x \<le> Rep_hf y)

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<noteq> 0 \<Longrightarrow> \<exists>xa. xa \<^bold>\<in> x \<and> (\<forall>y. y \<^bold>\<in> x \<longrightarrow> Rep_hf xa \<le> Rep_hf y); y \<noteq> 0 \<Longrightarrow> \<exists>x. x \<^bold>\<in> y \<and> (\<forall>ya. ya \<^bold>\<in> y \<longrightarrow> Rep_hf x \<le> Rep_hf ya); x \<^bold>\<notin> y; y \<triangleleft> x \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>xa. xa \<^bold>\<in> y \<triangleleft> x \<and> (\<forall>ya. ya \<^bold>\<in> y \<triangleleft> x \<longrightarrow> Rep_hf xa \<le> Rep_hf ya)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<noteq> 0 \<Longrightarrow> \<exists>xa. xa \<^bold>\<in> x \<and> (\<forall>y. y \<^bold>\<in> x \<longrightarrow> Rep_hf xa \<le> Rep_hf y); y \<noteq> 0 \<Longrightarrow> \<exists>x. x \<^bold>\<in> y \<and> (\<forall>ya. ya \<^bold>\<in> y \<longrightarrow> Rep_hf x \<le> Rep_hf ya); x \<^bold>\<notin> y; y \<triangleleft> x \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>xa. xa \<^bold>\<in> y \<triangleleft> x \<and> (\<forall>ya. ya \<^bold>\<in> y \<triangleleft> x \<longrightarrow> Rep_hf xa \<le> Rep_hf ya)
[PROOF STEP]
case (hinsert u v)
[PROOF STATE]
proof (state)
this:
u \<noteq> 0 \<Longrightarrow> \<exists>x. x \<^bold>\<in> u \<and> (\<forall>y. y \<^bold>\<in> u \<longrightarrow> Rep_hf x \<le> Rep_hf y)
v \<noteq> 0 \<Longrightarrow> \<exists>x. x \<^bold>\<in> v \<and> (\<forall>y. y \<^bold>\<in> v \<longrightarrow> Rep_hf x \<le> Rep_hf y)
u \<^bold>\<notin> v
v \<triangleleft> u \<noteq> 0

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<noteq> 0 \<Longrightarrow> \<exists>xa. xa \<^bold>\<in> x \<and> (\<forall>y. y \<^bold>\<in> x \<longrightarrow> Rep_hf xa \<le> Rep_hf y); y \<noteq> 0 \<Longrightarrow> \<exists>x. x \<^bold>\<in> y \<and> (\<forall>ya. ya \<^bold>\<in> y \<longrightarrow> Rep_hf x \<le> Rep_hf ya); x \<^bold>\<notin> y; y \<triangleleft> x \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>xa. xa \<^bold>\<in> y \<triangleleft> x \<and> (\<forall>ya. ya \<^bold>\<in> y \<triangleleft> x \<longrightarrow> Rep_hf xa \<le> Rep_hf ya)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. x \<^bold>\<in> v \<triangleleft> u \<and> (\<forall>y. y \<^bold>\<in> v \<triangleleft> u \<longrightarrow> Rep_hf x \<le> Rep_hf y)
[PROOF STEP]
proof (cases "v=0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. v = 0 \<Longrightarrow> \<exists>x. x \<^bold>\<in> v \<triangleleft> u \<and> (\<forall>y. y \<^bold>\<in> v \<triangleleft> u \<longrightarrow> Rep_hf x \<le> Rep_hf y)
 2. v \<noteq> 0 \<Longrightarrow> \<exists>x. x \<^bold>\<in> v \<triangleleft> u \<and> (\<forall>y. y \<^bold>\<in> v \<triangleleft> u \<longrightarrow> Rep_hf x \<le> Rep_hf y)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
v = 0

goal (2 subgoals):
 1. v = 0 \<Longrightarrow> \<exists>x. x \<^bold>\<in> v \<triangleleft> u \<and> (\<forall>y. y \<^bold>\<in> v \<triangleleft> u \<longrightarrow> Rep_hf x \<le> Rep_hf y)
 2. v \<noteq> 0 \<Longrightarrow> \<exists>x. x \<^bold>\<in> v \<triangleleft> u \<and> (\<forall>y. y \<^bold>\<in> v \<triangleleft> u \<longrightarrow> Rep_hf x \<le> Rep_hf y)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
v = 0

goal (1 subgoal):
 1. \<exists>x. x \<^bold>\<in> v \<triangleleft> u \<and> (\<forall>y. y \<^bold>\<in> v \<triangleleft> u \<longrightarrow> Rep_hf x \<le> Rep_hf y)
[PROOF STEP]
by (rule_tac x=u in exI, simp)
[PROOF STATE]
proof (state)
this:
\<exists>x. x \<^bold>\<in> v \<triangleleft> u \<and> (\<forall>y. y \<^bold>\<in> v \<triangleleft> u \<longrightarrow> Rep_hf x \<le> Rep_hf y)

goal (1 subgoal):
 1. v \<noteq> 0 \<Longrightarrow> \<exists>x. x \<^bold>\<in> v \<triangleleft> u \<and> (\<forall>y. y \<^bold>\<in> v \<triangleleft> u \<longrightarrow> Rep_hf x \<le> Rep_hf y)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v \<noteq> 0 \<Longrightarrow> \<exists>x. x \<^bold>\<in> v \<triangleleft> u \<and> (\<forall>y. y \<^bold>\<in> v \<triangleleft> u \<longrightarrow> Rep_hf x \<le> Rep_hf y)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
v \<noteq> 0

goal (1 subgoal):
 1. v \<noteq> 0 \<Longrightarrow> \<exists>x. x \<^bold>\<in> v \<triangleleft> u \<and> (\<forall>y. y \<^bold>\<in> v \<triangleleft> u \<longrightarrow> Rep_hf x \<le> Rep_hf y)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
v \<noteq> 0

goal (1 subgoal):
 1. \<exists>x. x \<^bold>\<in> v \<triangleleft> u \<and> (\<forall>y. y \<^bold>\<in> v \<triangleleft> u \<longrightarrow> Rep_hf x \<le> Rep_hf y)
[PROOF STEP]
by (metis dual_order.trans eq_iff hinsert.IH(2) hmem_hinsert
                  less_eq_insert1_iff linear)
[PROOF STATE]
proof (state)
this:
\<exists>x. x \<^bold>\<in> v \<triangleleft> u \<and> (\<forall>y. y \<^bold>\<in> v \<triangleleft> u \<longrightarrow> Rep_hf x \<le> Rep_hf y)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>x. x \<^bold>\<in> v \<triangleleft> u \<and> (\<forall>y. y \<^bold>\<in> v \<triangleleft> u \<longrightarrow> Rep_hf x \<le> Rep_hf y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma least_hmem: "a \<noteq> 0 \<Longrightarrow> least a \<^bold>\<in> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<noteq> 0 \<Longrightarrow> least a \<^bold>\<in> a
[PROOF STEP]
apply (frule nonempty_imp_ex_least, clarify)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>a \<noteq> 0; x \<^bold>\<in> a; \<forall>y. y \<^bold>\<in> a \<longrightarrow> Rep_hf x \<le> Rep_hf y\<rbrakk> \<Longrightarrow> least a \<^bold>\<in> a
[PROOF STEP]
apply (rule leastI2_order, auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ufa_invarD:
  "\<lbrakk>ufa_invar l; i<length l\<rbrakk> \<Longrightarrow> rep_of_dom (l,i)"
  "\<lbrakk>ufa_invar l; i<length l\<rbrakk> \<Longrightarrow> l!i<length l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>ufa_invar l; i < length l\<rbrakk> \<Longrightarrow> rep_of_dom (l, i)) &&& (\<lbrakk>ufa_invar l; i < length l\<rbrakk> \<Longrightarrow> l ! i < length l)
[PROOF STEP]
unfolding ufa_invar_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>\<forall>i<length l. rep_of_dom (l, i) \<and> l ! i < length l; i < length l\<rbrakk> \<Longrightarrow> rep_of_dom (l, i)) &&& (\<lbrakk>\<forall>i<length l. rep_of_dom (l, i) \<and> l ! i < length l; i < length l\<rbrakk> \<Longrightarrow> l ! i < length l)
[PROOF STEP]
by auto


[STATEMENT]
lemma rep_of_refl: "l!i=i \<Longrightarrow> rep_of l i = i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l ! i = i \<Longrightarrow> rep_of l i = i
[PROOF STEP]
apply (subst rep_of.psimps)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. l ! i = i \<Longrightarrow> rep_of_dom (l, i)
 2. l ! i = i \<Longrightarrow> (if l ! i = i then i else rep_of l (l ! i)) = i
[PROOF STEP]
apply (rule rep_of.domintros)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>l ! i = i; l ! i \<noteq> i\<rbrakk> \<Longrightarrow> rep_of_dom (l, l ! i)
 2. l ! i = i \<Longrightarrow> (if l ! i = i then i else rep_of l (l ! i)) = i
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma rep_of_step:
  "\<lbrakk>ufa_invar l; i<length l; l!i\<noteq>i\<rbrakk> \<Longrightarrow> rep_of l i = rep_of l (l!i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; i < length l; l ! i \<noteq> i\<rbrakk> \<Longrightarrow> rep_of l i = rep_of l (l ! i)
[PROOF STEP]
apply (subst rep_of.psimps)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ufa_invar l; i < length l; l ! i \<noteq> i\<rbrakk> \<Longrightarrow> rep_of_dom (l, i)
 2. \<lbrakk>ufa_invar l; i < length l; l ! i \<noteq> i\<rbrakk> \<Longrightarrow> (if l ! i = i then i else rep_of l (l ! i)) = rep_of l (l ! i)
[PROOF STEP]
apply (auto dest: ufa_invarD)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma rep_of_iff: "\<lbrakk>ufa_invar l; i<length l\<rbrakk>
  \<Longrightarrow> rep_of l i = (if l!i=i then i else rep_of l (l!i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; i < length l\<rbrakk> \<Longrightarrow> rep_of l i = (if l ! i = i then i else rep_of l (l ! i))
[PROOF STEP]
by (simp add: rep_of_simps)


[STATEMENT]
lemma rep_of_induct[case_names base step, consumes 2]:
  assumes I: "ufa_invar l"
  assumes L: "i<length l"
  assumes BASE: "\<And>i. \<lbrakk> ufa_invar l; i<length l; l!i=i \<rbrakk> \<Longrightarrow> P l i"
  assumes STEP: "\<And>i. \<lbrakk> ufa_invar l; i<length l; l!i\<noteq>i; P l (l!i) \<rbrakk>
    \<Longrightarrow> P l i"
  shows "P l i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P l i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P l i
[PROOF STEP]
from ufa_invarD[OF I L]
[PROOF STATE]
proof (chain)
picking this:
rep_of_dom (l, i)
l ! i < length l
[PROOF STEP]
have "ufa_invar l \<and> i<length l \<longrightarrow> P l i"
[PROOF STATE]
proof (prove)
using this:
rep_of_dom (l, i)
l ! i < length l

goal (1 subgoal):
 1. ufa_invar l \<and> i < length l \<longrightarrow> P l i
[PROOF STEP]
apply (induct l\<equiv>l i rule: rep_of.pinduct)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>rep_of_dom (l, i); \<lbrakk>l ! i \<noteq> i; l ! (l ! i) < length l\<rbrakk> \<Longrightarrow> ufa_invar l \<and> l ! i < length l \<longrightarrow> P l (l ! i); l ! i < length l\<rbrakk> \<Longrightarrow> ufa_invar l \<and> i < length l \<longrightarrow> P l i
[PROOF STEP]
apply (auto intro: STEP BASE dest: ufa_invarD)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
ufa_invar l \<and> i < length l \<longrightarrow> P l i

goal (1 subgoal):
 1. P l i
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
ufa_invar l \<and> i < length l \<longrightarrow> P l i

goal (1 subgoal):
 1. P l i
[PROOF STEP]
using I L
[PROOF STATE]
proof (prove)
using this:
ufa_invar l \<and> i < length l \<longrightarrow> P l i
ufa_invar l
i < length l

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rep_of_min:
  "\<lbrakk> ufa_invar l; i<length l \<rbrakk> \<Longrightarrow> l!(rep_of l i) = rep_of l i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; i < length l\<rbrakk> \<Longrightarrow> l ! rep_of l i = rep_of l i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; i < length l\<rbrakk> \<Longrightarrow> l ! rep_of l i = rep_of l i
[PROOF STEP]
have "\<lbrakk>rep_of_dom (l,i) \<rbrakk> \<Longrightarrow> l!(rep_of l i) = rep_of l i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rep_of_dom (l, i) \<Longrightarrow> l ! rep_of l i = rep_of l i
[PROOF STEP]
apply (induct arbitrary:  rule: rep_of.pinduct)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l i. \<lbrakk>rep_of_dom (l, i); l ! i \<noteq> i \<Longrightarrow> l ! rep_of l (l ! i) = rep_of l (l ! i)\<rbrakk> \<Longrightarrow> l ! rep_of l i = rep_of l i
[PROOF STEP]
apply (subst rep_of.psimps, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l i. \<lbrakk>rep_of_dom (l, i); l ! i \<noteq> i \<Longrightarrow> l ! rep_of l (l ! i) = rep_of l (l ! i)\<rbrakk> \<Longrightarrow> l ! (if l ! i = i then i else rep_of l (l ! i)) = rep_of l i
[PROOF STEP]
apply (subst (2) rep_of.psimps, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l i. \<lbrakk>rep_of_dom (l, i); l ! i \<noteq> i \<Longrightarrow> l ! rep_of l (l ! i) = rep_of l (l ! i)\<rbrakk> \<Longrightarrow> l ! (if l ! i = i then i else rep_of l (l ! i)) = (if l ! i = i then i else rep_of l (l ! i))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
rep_of_dom (l, i) \<Longrightarrow> l ! rep_of l i = rep_of l i

goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; i < length l\<rbrakk> \<Longrightarrow> l ! rep_of l i = rep_of l i
[PROOF STEP]
thus "\<lbrakk> ufa_invar l; i<length l \<rbrakk> \<Longrightarrow> l!(rep_of l i) = rep_of l i"
[PROOF STATE]
proof (prove)
using this:
rep_of_dom (l, i) \<Longrightarrow> l ! rep_of l i = rep_of l i

goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; i < length l\<rbrakk> \<Longrightarrow> l ! rep_of l i = rep_of l i
[PROOF STEP]
by (metis ufa_invarD(1))
[PROOF STATE]
proof (state)
this:
\<lbrakk>ufa_invar l; i < length l\<rbrakk> \<Longrightarrow> l ! rep_of l i = rep_of l i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rep_of_bound:
  "\<lbrakk> ufa_invar l; i<length l \<rbrakk> \<Longrightarrow> rep_of l i < length l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; i < length l\<rbrakk> \<Longrightarrow> rep_of l i < length l
[PROOF STEP]
apply (induct rule: rep_of_induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i = i\<rbrakk> \<Longrightarrow> rep_of l i < length l
 2. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i \<noteq> i; rep_of l (l ! i) < length l\<rbrakk> \<Longrightarrow> rep_of l i < length l
[PROOF STEP]
apply (auto simp: rep_of_iff)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma rep_of_idem:
  "\<lbrakk> ufa_invar l; i<length l \<rbrakk> \<Longrightarrow> rep_of l (rep_of l i) = rep_of l i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; i < length l\<rbrakk> \<Longrightarrow> rep_of l (rep_of l i) = rep_of l i
[PROOF STEP]
by (auto simp: rep_of_min rep_of_refl)


[STATEMENT]
lemma rep_of_min_upd: "\<lbrakk> ufa_invar l; x<length l; i<length l \<rbrakk> \<Longrightarrow>
  rep_of (l[rep_of l x := rep_of l x]) i = rep_of l i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; x < length l; i < length l\<rbrakk> \<Longrightarrow> rep_of (l[rep_of l x := rep_of l x]) i = rep_of l i
[PROOF STEP]
by (metis list_update_id rep_of_min)


[STATEMENT]
lemma rep_of_idx:
  "\<lbrakk>ufa_invar l; i<length l\<rbrakk> \<Longrightarrow> rep_of l (l!i) = rep_of l i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; i < length l\<rbrakk> \<Longrightarrow> rep_of l (l ! i) = rep_of l i
[PROOF STEP]
by (metis rep_of_step)


[STATEMENT]
lemma ufa_\<alpha>_equiv[simp, intro!]: "part_equiv (ufa_\<alpha> l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. part_equiv (ufa_\<alpha> l)
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. sym (ufa_\<alpha> l)
 2. trans (ufa_\<alpha> l)
[PROOF STEP]
unfolding ufa_\<alpha>_def
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. sym {(x, y). x < length l \<and> y < length l \<and> rep_of l x = rep_of l y}
 2. trans {(x, y). x < length l \<and> y < length l \<and> rep_of l x = rep_of l y}
[PROOF STEP]
apply (rule symI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. (a, b) \<in> {(x, y). x < length l \<and> y < length l \<and> rep_of l x = rep_of l y} \<Longrightarrow> (b, a) \<in> {(x, y). x < length l \<and> y < length l \<and> rep_of l x = rep_of l y}
 2. trans {(x, y). x < length l \<and> y < length l \<and> rep_of l x = rep_of l y}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trans {(x, y). x < length l \<and> y < length l \<and> rep_of l x = rep_of l y}
[PROOF STEP]
apply (rule transI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>(x, y) \<in> {(x, y). x < length l \<and> y < length l \<and> rep_of l x = rep_of l y}; (y, z) \<in> {(x, y). x < length l \<and> y < length l \<and> rep_of l x = rep_of l y}\<rbrakk> \<Longrightarrow> (x, z) \<in> {(x, y). x < length l \<and> y < length l \<and> rep_of l x = rep_of l y}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ufa_\<alpha>_lenD:
  "(x,y)\<in>ufa_\<alpha> l \<Longrightarrow> x<length l"
  "(x,y)\<in>ufa_\<alpha> l \<Longrightarrow> y<length l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((x, y) \<in> ufa_\<alpha> l \<Longrightarrow> x < length l) &&& ((x, y) \<in> ufa_\<alpha> l \<Longrightarrow> y < length l)
[PROOF STEP]
unfolding ufa_\<alpha>_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((x, y) \<in> {(x, y). x < length l \<and> y < length l \<and> rep_of l x = rep_of l y} \<Longrightarrow> x < length l) &&& ((x, y) \<in> {(x, y). x < length l \<and> y < length l \<and> rep_of l x = rep_of l y} \<Longrightarrow> y < length l)
[PROOF STEP]
by auto


[STATEMENT]
lemma ufa_\<alpha>_dom[simp]: "Domain (ufa_\<alpha> l) = {0..<length l}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Domain (ufa_\<alpha> l) = {0..<length l}
[PROOF STEP]
unfolding ufa_\<alpha>_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Domain {(x, y). x < length l \<and> y < length l \<and> rep_of l x = rep_of l y} = {0..<length l}
[PROOF STEP]
by auto


[STATEMENT]
lemma ufa_\<alpha>_refl[simp]: "(i,i)\<in>ufa_\<alpha> l \<longleftrightarrow> i<length l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((i, i) \<in> ufa_\<alpha> l) = (i < length l)
[PROOF STEP]
unfolding ufa_\<alpha>_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((i, i) \<in> {(x, y). x < length l \<and> y < length l \<and> rep_of l x = rep_of l y}) = (i < length l)
[PROOF STEP]
by simp


[STATEMENT]
lemma ufa_\<alpha>_len_eq:
  assumes "ufa_\<alpha> l = ufa_\<alpha> l'"
  shows "length l = length l'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length l = length l'
[PROOF STEP]
by (metis assms le_antisym less_not_refl linorder_le_less_linear ufa_\<alpha>_refl)


[STATEMENT]
lemma ufa_init_invar: "ufa_invar [0..<n]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ufa_invar [0..<n]
[PROOF STEP]
unfolding ufa_invar_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i<length [0..<n]. rep_of_dom ([0..<n], i) \<and> [0..<n] ! i < length [0..<n]
[PROOF STEP]
by (auto intro: rep_of.domintros)


[STATEMENT]
lemma ufa_init_correct: "ufa_\<alpha> [0..<n] = {(x,x) | x. x<n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ufa_\<alpha> [0..<n] = {(x, x) |x. x < n}
[PROOF STEP]
unfolding ufa_\<alpha>_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(x, y). x < length [0..<n] \<and> y < length [0..<n] \<and> rep_of [0..<n] x = rep_of [0..<n] y} = {(x, x) |x. x < n}
[PROOF STEP]
using ufa_init_invar[of n]
[PROOF STATE]
proof (prove)
using this:
ufa_invar [0..<n]

goal (1 subgoal):
 1. {(x, y). x < length [0..<n] \<and> y < length [0..<n] \<and> rep_of [0..<n] x = rep_of [0..<n] y} = {(x, x) |x. x < n}
[PROOF STEP]
apply (auto simp: rep_of_refl)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ufa_find_correct: "\<lbrakk>ufa_invar l; x<length l; y<length l\<rbrakk>
  \<Longrightarrow> rep_of l x = rep_of l y \<longleftrightarrow> (x,y)\<in>ufa_\<alpha> l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; x < length l; y < length l\<rbrakk> \<Longrightarrow> (rep_of l x = rep_of l y) = ((x, y) \<in> ufa_\<alpha> l)
[PROOF STEP]
unfolding ufa_\<alpha>_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; x < length l; y < length l\<rbrakk> \<Longrightarrow> (rep_of l x = rep_of l y) = ((x, y) \<in> {(x, y). x < length l \<and> y < length l \<and> rep_of l x = rep_of l y})
[PROOF STEP]
by auto


[STATEMENT]
lemma ufa_union_invar:
  assumes I: "ufa_invar l"
  assumes L: "x<length l" "y<length l"
  shows "ufa_invar (ufa_union l x y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ufa_invar (ufa_union l x y)
[PROOF STEP]
unfolding ufa_invar_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i<length (ufa_union l x y). rep_of_dom (ufa_union l x y, i) \<and> ufa_union l x y ! i < length (ufa_union l x y)
[PROOF STEP]
proof (intro allI impI, simp only: length_list_update)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < length l \<Longrightarrow> rep_of_dom (ufa_union l x y, i) \<and> ufa_union l x y ! i < length l
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < length l \<Longrightarrow> rep_of_dom (ufa_union l x y, i) \<and> ufa_union l x y ! i < length l
[PROOF STEP]
assume A: "i<length l"
[PROOF STATE]
proof (state)
this:
i < length l

goal (1 subgoal):
 1. \<And>i. i < length l \<Longrightarrow> rep_of_dom (ufa_union l x y, i) \<and> ufa_union l x y ! i < length l
[PROOF STEP]
with I
[PROOF STATE]
proof (chain)
picking this:
ufa_invar l
i < length l
[PROOF STEP]
have "rep_of_dom (l,i)"
[PROOF STATE]
proof (prove)
using this:
ufa_invar l
i < length l

goal (1 subgoal):
 1. rep_of_dom (l, i)
[PROOF STEP]
by (auto dest: ufa_invarD)
[PROOF STATE]
proof (state)
this:
rep_of_dom (l, i)

goal (1 subgoal):
 1. \<And>i. i < length l \<Longrightarrow> rep_of_dom (ufa_union l x y, i) \<and> ufa_union l x y ! i < length l
[PROOF STEP]
have "ufa_union l x y ! i < length l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ufa_union l x y ! i < length l
[PROOF STEP]
using I L A
[PROOF STATE]
proof (prove)
using this:
ufa_invar l
x < length l
y < length l
i < length l

goal (1 subgoal):
 1. ufa_union l x y ! i < length l
[PROOF STEP]
apply (cases "i=rep_of l x")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ufa_invar l; x < length l; y < length l; i < length l; i = rep_of l x\<rbrakk> \<Longrightarrow> ufa_union l x y ! i < length l
 2. \<lbrakk>ufa_invar l; x < length l; y < length l; i < length l; i \<noteq> rep_of l x\<rbrakk> \<Longrightarrow> ufa_union l x y ! i < length l
[PROOF STEP]
apply (auto simp: rep_of_bound dest: ufa_invarD)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
ufa_union l x y ! i < length l

goal (1 subgoal):
 1. \<And>i. i < length l \<Longrightarrow> rep_of_dom (ufa_union l x y, i) \<and> ufa_union l x y ! i < length l
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ufa_union l x y ! i < length l

goal (1 subgoal):
 1. \<And>i. i < length l \<Longrightarrow> rep_of_dom (ufa_union l x y, i) \<and> ufa_union l x y ! i < length l
[PROOF STEP]
have "rep_of_dom (ufa_union l x y, i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rep_of_dom (ufa_union l x y, i)
[PROOF STEP]
using I A L
[PROOF STATE]
proof (prove)
using this:
ufa_invar l
i < length l
x < length l
y < length l

goal (1 subgoal):
 1. rep_of_dom (ufa_union l x y, i)
[PROOF STEP]
proof (induct rule: rep_of_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i = i; x < length l; y < length l\<rbrakk> \<Longrightarrow> rep_of_dom (ufa_union l x y, i)
 2. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i \<noteq> i; \<lbrakk>x < length l; y < length l\<rbrakk> \<Longrightarrow> rep_of_dom (ufa_union l x y, l ! i); x < length l; y < length l\<rbrakk> \<Longrightarrow> rep_of_dom (ufa_union l x y, i)
[PROOF STEP]
case (base i)
[PROOF STATE]
proof (state)
this:
ufa_invar l
i < length l
l ! i = i
x < length l
y < length l

goal (2 subgoals):
 1. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i = i; x < length l; y < length l\<rbrakk> \<Longrightarrow> rep_of_dom (ufa_union l x y, i)
 2. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i \<noteq> i; \<lbrakk>x < length l; y < length l\<rbrakk> \<Longrightarrow> rep_of_dom (ufa_union l x y, l ! i); x < length l; y < length l\<rbrakk> \<Longrightarrow> rep_of_dom (ufa_union l x y, i)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
ufa_invar l
i < length l
l ! i = i
x < length l
y < length l

goal (1 subgoal):
 1. rep_of_dom (ufa_union l x y, i)
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; i < length l; l ! i = i; x < length l; y < length l\<rbrakk> \<Longrightarrow> rep_of_dom (ufa_union l x y, i)
[PROOF STEP]
apply (rule rep_of.domintros)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; i < length l; l ! i = i; x < length l; y < length l; ufa_union l x y ! i \<noteq> i\<rbrakk> \<Longrightarrow> rep_of_dom (ufa_union l x y, ufa_union l x y ! i)
[PROOF STEP]
apply (cases "i=rep_of l x")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ufa_invar l; i < length l; l ! i = i; x < length l; y < length l; ufa_union l x y ! i \<noteq> i; i = rep_of l x\<rbrakk> \<Longrightarrow> rep_of_dom (ufa_union l x y, ufa_union l x y ! i)
 2. \<lbrakk>ufa_invar l; i < length l; l ! i = i; x < length l; y < length l; ufa_union l x y ! i \<noteq> i; i \<noteq> rep_of l x\<rbrakk> \<Longrightarrow> rep_of_dom (ufa_union l x y, ufa_union l x y ! i)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; rep_of l x < length l; l ! rep_of l x = rep_of l x; x < length l; y < length l; rep_of l y \<noteq> rep_of l x; i = rep_of l x\<rbrakk> \<Longrightarrow> rep_of_dom (ufa_union l x y, rep_of l y)
[PROOF STEP]
apply (rule rep_of.domintros)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; rep_of l x < length l; l ! rep_of l x = rep_of l x; x < length l; y < length l; rep_of l y \<noteq> rep_of l x; i = rep_of l x; ufa_union l x y ! rep_of l y \<noteq> rep_of l y\<rbrakk> \<Longrightarrow> rep_of_dom (ufa_union l x y, ufa_union l x y ! rep_of l y)
[PROOF STEP]
apply (auto simp: rep_of_min)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
rep_of_dom (ufa_union l x y, i)

goal (1 subgoal):
 1. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i \<noteq> i; \<lbrakk>x < length l; y < length l\<rbrakk> \<Longrightarrow> rep_of_dom (ufa_union l x y, l ! i); x < length l; y < length l\<rbrakk> \<Longrightarrow> rep_of_dom (ufa_union l x y, i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i \<noteq> i; \<lbrakk>x < length l; y < length l\<rbrakk> \<Longrightarrow> rep_of_dom (ufa_union l x y, l ! i); x < length l; y < length l\<rbrakk> \<Longrightarrow> rep_of_dom (ufa_union l x y, i)
[PROOF STEP]
case (step i)
[PROOF STATE]
proof (state)
this:
ufa_invar l
i < length l
l ! i \<noteq> i
\<lbrakk>x < length l; y < length l\<rbrakk> \<Longrightarrow> rep_of_dom (ufa_union l x y, l ! i)
x < length l
y < length l

goal (1 subgoal):
 1. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i \<noteq> i; \<lbrakk>x < length l; y < length l\<rbrakk> \<Longrightarrow> rep_of_dom (ufa_union l x y, l ! i); x < length l; y < length l\<rbrakk> \<Longrightarrow> rep_of_dom (ufa_union l x y, i)
[PROOF STEP]
from step.prems \<open>ufa_invar l\<close> \<open>i<length l\<close> \<open>l!i\<noteq>i\<close>
[PROOF STATE]
proof (chain)
picking this:
x < length l
y < length l
ufa_invar l
i < length l
l ! i \<noteq> i
[PROOF STEP]
have [simp]: "ufa_union l x y ! i = l!i"
[PROOF STATE]
proof (prove)
using this:
x < length l
y < length l
ufa_invar l
i < length l
l ! i \<noteq> i

goal (1 subgoal):
 1. ufa_union l x y ! i = l ! i
[PROOF STEP]
apply (auto simp: rep_of_min rep_of_bound nth_list_update)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
ufa_union l x y ! i = l ! i

goal (1 subgoal):
 1. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i \<noteq> i; \<lbrakk>x < length l; y < length l\<rbrakk> \<Longrightarrow> rep_of_dom (ufa_union l x y, l ! i); x < length l; y < length l\<rbrakk> \<Longrightarrow> rep_of_dom (ufa_union l x y, i)
[PROOF STEP]
from step
[PROOF STATE]
proof (chain)
picking this:
ufa_invar l
i < length l
l ! i \<noteq> i
\<lbrakk>x < length l; y < length l\<rbrakk> \<Longrightarrow> rep_of_dom (ufa_union l x y, l ! i)
x < length l
y < length l
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ufa_invar l
i < length l
l ! i \<noteq> i
\<lbrakk>x < length l; y < length l\<rbrakk> \<Longrightarrow> rep_of_dom (ufa_union l x y, l ! i)
x < length l
y < length l

goal (1 subgoal):
 1. rep_of_dom (ufa_union l x y, i)
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; i < length l; l ! i \<noteq> i; \<lbrakk>x < length l; y < length l\<rbrakk> \<Longrightarrow> rep_of_dom (ufa_union l x y, l ! i); x < length l; y < length l\<rbrakk> \<Longrightarrow> rep_of_dom (ufa_union l x y, i)
[PROOF STEP]
apply (rule rep_of.domintros)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; i < length l; l ! i \<noteq> i; \<lbrakk>x < length l; y < length l\<rbrakk> \<Longrightarrow> rep_of_dom (ufa_union l x y, l ! i); x < length l; y < length l; ufa_union l x y ! i \<noteq> i\<rbrakk> \<Longrightarrow> rep_of_dom (ufa_union l x y, ufa_union l x y ! i)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
rep_of_dom (ufa_union l x y, i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rep_of_dom (ufa_union l x y, i)

goal (1 subgoal):
 1. \<And>i. i < length l \<Longrightarrow> rep_of_dom (ufa_union l x y, i) \<and> ufa_union l x y ! i < length l
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ufa_union l x y ! i < length l
rep_of_dom (ufa_union l x y, i)
[PROOF STEP]
show
    "rep_of_dom (ufa_union l x y, i) \<and> ufa_union l x y ! i < length l"
[PROOF STATE]
proof (prove)
using this:
ufa_union l x y ! i < length l
rep_of_dom (ufa_union l x y, i)

goal (1 subgoal):
 1. rep_of_dom (ufa_union l x y, i) \<and> ufa_union l x y ! i < length l
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
rep_of_dom (ufa_union l x y, i) \<and> ufa_union l x y ! i < length l

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ufa_union_aux:
  assumes I: "ufa_invar l"
  assumes L: "x<length l" "y<length l"
  assumes IL: "i<length l"
  shows "rep_of (ufa_union l x y) i =
    (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
[PROOF STEP]
using I IL
[PROOF STATE]
proof (prove)
using this:
ufa_invar l
i < length l

goal (1 subgoal):
 1. rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
[PROOF STEP]
proof (induct rule: rep_of_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i = i\<rbrakk> \<Longrightarrow> rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
 2. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i \<noteq> i; rep_of (ufa_union l x y) (l ! i) = (if rep_of l (l ! i) = rep_of l x then rep_of l y else rep_of l (l ! i))\<rbrakk> \<Longrightarrow> rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
[PROOF STEP]
case (base i)
[PROOF STATE]
proof (state)
this:
ufa_invar l
i < length l
l ! i = i

goal (2 subgoals):
 1. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i = i\<rbrakk> \<Longrightarrow> rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
 2. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i \<noteq> i; rep_of (ufa_union l x y) (l ! i) = (if rep_of l (l ! i) = rep_of l x then rep_of l y else rep_of l (l ! i))\<rbrakk> \<Longrightarrow> rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
[PROOF STEP]
have [simp]: "rep_of l i = i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rep_of l i = i
[PROOF STEP]
using \<open>l!i=i\<close>
[PROOF STATE]
proof (prove)
using this:
l ! i = i

goal (1 subgoal):
 1. rep_of l i = i
[PROOF STEP]
by (simp add: rep_of_refl)
[PROOF STATE]
proof (state)
this:
rep_of l i = i

goal (2 subgoals):
 1. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i = i\<rbrakk> \<Longrightarrow> rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
 2. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i \<noteq> i; rep_of (ufa_union l x y) (l ! i) = (if rep_of l (l ! i) = rep_of l x then rep_of l y else rep_of l (l ! i))\<rbrakk> \<Longrightarrow> rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
[PROOF STEP]
note [simp] = \<open>ufa_invar l\<close> \<open>i<length l\<close>
[PROOF STATE]
proof (state)
this:
ufa_invar l
i < length l

goal (2 subgoals):
 1. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i = i\<rbrakk> \<Longrightarrow> rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
 2. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i \<noteq> i; rep_of (ufa_union l x y) (l ! i) = (if rep_of l (l ! i) = rep_of l x then rep_of l y else rep_of l (l ! i))\<rbrakk> \<Longrightarrow> rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
 2. \<not> ?P \<Longrightarrow> rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
[PROOF STEP]
assume A[simp]: "rep_of l x = i"
[PROOF STATE]
proof (state)
this:
rep_of l x = i

goal (2 subgoals):
 1. ?P \<Longrightarrow> rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
 2. \<not> ?P \<Longrightarrow> rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
[PROOF STEP]
have [simp]: "l[i := rep_of l y] ! i = rep_of l y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l[i := rep_of l y] ! i = rep_of l y
[PROOF STEP]
by (auto simp: rep_of_bound)
[PROOF STATE]
proof (state)
this:
l[i := rep_of l y] ! i = rep_of l y

goal (2 subgoals):
 1. ?P \<Longrightarrow> rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
 2. \<not> ?P \<Longrightarrow> rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
 2. \<not> ?P \<Longrightarrow> rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
[PROOF STEP]
assume [simp]: "rep_of l y = i"
[PROOF STATE]
proof (state)
this:
rep_of l y = i

goal (2 subgoals):
 1. ?P \<Longrightarrow> rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
 2. \<not> ?P \<Longrightarrow> rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
[PROOF STEP]
by (simp add: rep_of_refl)
[PROOF STATE]
proof (state)
this:
rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)

goal (1 subgoal):
 1. rep_of l y \<noteq> i \<Longrightarrow> rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rep_of l y \<noteq> i \<Longrightarrow> rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
[PROOF STEP]
assume A: "rep_of l y \<noteq> i"
[PROOF STATE]
proof (state)
this:
rep_of l y \<noteq> i

goal (1 subgoal):
 1. rep_of l y \<noteq> i \<Longrightarrow> rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
[PROOF STEP]
have [simp]: "rep_of (l[i := rep_of l y]) i = rep_of l y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rep_of (l[i := rep_of l y]) i = rep_of l y
[PROOF STEP]
apply (subst rep_of_step[OF ufa_union_invar[OF I L], simplified])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. i < length l
 2. l[i := rep_of l y] ! i \<noteq> i
 3. rep_of (l[i := rep_of l y]) (l[i := rep_of l y] ! i) = rep_of l y
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
rep_of l y \<noteq> i

goal (3 subgoals):
 1. i < length l
 2. l[i := rep_of l y] ! i \<noteq> i
 3. rep_of (l[i := rep_of l y]) (l[i := rep_of l y] ! i) = rep_of l y
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rep_of l y \<noteq> i \<Longrightarrow> rep_of (l[i := rep_of l y]) (rep_of l y) = rep_of l y
[PROOF STEP]
apply (subst rep_of_refl[where i="rep_of l y"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. rep_of l y \<noteq> i \<Longrightarrow> l[i := rep_of l y] ! rep_of l y = rep_of l y
 2. rep_of l y \<noteq> i \<Longrightarrow> rep_of l y = rep_of l y
[PROOF STEP]
using I L
[PROOF STATE]
proof (prove)
using this:
ufa_invar l
x < length l
y < length l

goal (2 subgoals):
 1. rep_of l y \<noteq> i \<Longrightarrow> l[i := rep_of l y] ! rep_of l y = rep_of l y
 2. rep_of l y \<noteq> i \<Longrightarrow> rep_of l y = rep_of l y
[PROOF STEP]
apply (simp_all add: rep_of_min)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
rep_of (l[i := rep_of l y]) i = rep_of l y

goal (1 subgoal):
 1. rep_of l y \<noteq> i \<Longrightarrow> rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
[PROOF STEP]
by (simp add: rep_of_refl)
[PROOF STATE]
proof (state)
this:
rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)

goal (1 subgoal):
 1. rep_of l x \<noteq> i \<Longrightarrow> rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rep_of l x \<noteq> i \<Longrightarrow> rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
[PROOF STEP]
assume A: "rep_of l x \<noteq> i"
[PROOF STATE]
proof (state)
this:
rep_of l x \<noteq> i

goal (1 subgoal):
 1. rep_of l x \<noteq> i \<Longrightarrow> rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
[PROOF STEP]
hence "ufa_union l x y ! i = l!i"
[PROOF STATE]
proof (prove)
using this:
rep_of l x \<noteq> i

goal (1 subgoal):
 1. ufa_union l x y ! i = l ! i
[PROOF STEP]
by (auto)
[PROOF STATE]
proof (state)
this:
ufa_union l x y ! i = l ! i

goal (1 subgoal):
 1. rep_of l x \<noteq> i \<Longrightarrow> rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ufa_union l x y ! i = l ! i

goal (1 subgoal):
 1. rep_of l x \<noteq> i \<Longrightarrow> rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
[PROOF STEP]
note \<open>l!i=i\<close>
[PROOF STATE]
proof (state)
this:
l ! i = i

goal (1 subgoal):
 1. rep_of l x \<noteq> i \<Longrightarrow> rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ufa_union l x y ! i = i
[PROOF STEP]
have "rep_of (ufa_union l x y) i = i"
[PROOF STATE]
proof (prove)
using this:
ufa_union l x y ! i = i

goal (1 subgoal):
 1. rep_of (ufa_union l x y) i = i
[PROOF STEP]
by (simp add: rep_of_refl)
[PROOF STATE]
proof (state)
this:
rep_of (ufa_union l x y) i = i

goal (1 subgoal):
 1. rep_of l x \<noteq> i \<Longrightarrow> rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
rep_of (ufa_union l x y) i = i

goal (1 subgoal):
 1. rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
rep_of (ufa_union l x y) i = i
rep_of l x \<noteq> i

goal (1 subgoal):
 1. rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)

goal (1 subgoal):
 1. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i \<noteq> i; rep_of (ufa_union l x y) (l ! i) = (if rep_of l (l ! i) = rep_of l x then rep_of l y else rep_of l (l ! i))\<rbrakk> \<Longrightarrow> rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i \<noteq> i; rep_of (ufa_union l x y) (l ! i) = (if rep_of l (l ! i) = rep_of l x then rep_of l y else rep_of l (l ! i))\<rbrakk> \<Longrightarrow> rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
[PROOF STEP]
case (step i)
[PROOF STATE]
proof (state)
this:
ufa_invar l
i < length l
l ! i \<noteq> i
rep_of (ufa_union l x y) (l ! i) = (if rep_of l (l ! i) = rep_of l x then rep_of l y else rep_of l (l ! i))

goal (1 subgoal):
 1. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i \<noteq> i; rep_of (ufa_union l x y) (l ! i) = (if rep_of l (l ! i) = rep_of l x then rep_of l y else rep_of l (l ! i))\<rbrakk> \<Longrightarrow> rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
[PROOF STEP]
note [simp] = I L \<open>i<length l\<close>
[PROOF STATE]
proof (state)
this:
ufa_invar l
x < length l
y < length l
i < length l

goal (1 subgoal):
 1. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i \<noteq> i; rep_of (ufa_union l x y) (l ! i) = (if rep_of l (l ! i) = rep_of l x then rep_of l y else rep_of l (l ! i))\<rbrakk> \<Longrightarrow> rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
[PROOF STEP]
have "rep_of l x \<noteq> i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rep_of l x \<noteq> i
[PROOF STEP]
by (metis I L(1) rep_of_min \<open>l!i\<noteq>i\<close>)
[PROOF STATE]
proof (state)
this:
rep_of l x \<noteq> i

goal (1 subgoal):
 1. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i \<noteq> i; rep_of (ufa_union l x y) (l ! i) = (if rep_of l (l ! i) = rep_of l x then rep_of l y else rep_of l (l ! i))\<rbrakk> \<Longrightarrow> rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
[PROOF STEP]
hence [simp]: "ufa_union l x y ! i = l!i"
[PROOF STATE]
proof (prove)
using this:
rep_of l x \<noteq> i

goal (1 subgoal):
 1. ufa_union l x y ! i = l ! i
[PROOF STEP]
by (auto simp add: nth_list_update rep_of_bound \<open>l!i\<noteq>i\<close>) []
[PROOF STATE]
proof (state)
this:
ufa_union l x y ! i = l ! i

goal (1 subgoal):
 1. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i \<noteq> i; rep_of (ufa_union l x y) (l ! i) = (if rep_of l (l ! i) = rep_of l x then rep_of l y else rep_of l (l ! i))\<rbrakk> \<Longrightarrow> rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
[PROOF STEP]
have "rep_of (ufa_union l x y) i = rep_of (ufa_union l x y) (l!i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rep_of (ufa_union l x y) i = rep_of (ufa_union l x y) (l ! i)
[PROOF STEP]
by (auto simp add: rep_of_iff[OF ufa_union_invar[OF I L]])
[PROOF STATE]
proof (state)
this:
rep_of (ufa_union l x y) i = rep_of (ufa_union l x y) (l ! i)

goal (1 subgoal):
 1. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i \<noteq> i; rep_of (ufa_union l x y) (l ! i) = (if rep_of l (l ! i) = rep_of l x then rep_of l y else rep_of l (l ! i))\<rbrakk> \<Longrightarrow> rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
rep_of (ufa_union l x y) i = rep_of (ufa_union l x y) (l ! i)

goal (1 subgoal):
 1. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i \<noteq> i; rep_of (ufa_union l x y) (l ! i) = (if rep_of l (l ! i) = rep_of l x then rep_of l y else rep_of l (l ! i))\<rbrakk> \<Longrightarrow> rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
[PROOF STEP]
note step.hyps(4)
[PROOF STATE]
proof (state)
this:
rep_of (ufa_union l x y) (l ! i) = (if rep_of l (l ! i) = rep_of l x then rep_of l y else rep_of l (l ! i))

goal (1 subgoal):
 1. \<And>i. \<lbrakk>ufa_invar l; i < length l; l ! i \<noteq> i; rep_of (ufa_union l x y) (l ! i) = (if rep_of l (l ! i) = rep_of l x then rep_of l y else rep_of l (l ! i))\<rbrakk> \<Longrightarrow> rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
rep_of (ufa_union l x y) i = (if rep_of l (l ! i) = rep_of l x then rep_of l y else rep_of l (l ! i))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
rep_of (ufa_union l x y) i = (if rep_of l (l ! i) = rep_of l x then rep_of l y else rep_of l (l ! i))

goal (1 subgoal):
 1. rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
[PROOF STEP]
by (auto simp: rep_of_idx)
[PROOF STATE]
proof (state)
this:
rep_of (ufa_union l x y) i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ufa_union_correct: "\<lbrakk> ufa_invar l; x<length l; y<length l \<rbrakk>
  \<Longrightarrow> ufa_\<alpha> (ufa_union l x y) = per_union (ufa_\<alpha> l) x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; x < length l; y < length l\<rbrakk> \<Longrightarrow> ufa_\<alpha> (ufa_union l x y) = per_union (ufa_\<alpha> l) x y
[PROOF STEP]
unfolding ufa_\<alpha>_def per_union_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; x < length l; y < length l\<rbrakk> \<Longrightarrow> {(xa, ya). xa < length (ufa_union l x y) \<and> ya < length (ufa_union l x y) \<and> rep_of (ufa_union l x y) xa = rep_of (ufa_union l x y) ya} = {(x, y). x < length l \<and> y < length l \<and> rep_of l x = rep_of l y} \<union> {(xa, ya). (xa, x) \<in> {(x, y). x < length l \<and> y < length l \<and> rep_of l x = rep_of l y} \<and> (ya, y) \<in> {(x, y). x < length l \<and> y < length l \<and> rep_of l x = rep_of l y}} \<union> {(ya, xa). (xa, x) \<in> {(x, y). x < length l \<and> y < length l \<and> rep_of l x = rep_of l y} \<and> (ya, y) \<in> {(x, y). x < length l \<and> y < length l \<and> rep_of l x = rep_of l y}}
[PROOF STEP]
by (auto simp: ufa_union_aux
    split: if_split_asm
  )