[STATEMENT]
lemma sorted_list_of_set_append: assumes \<open>finite xs\<close> \<open>finite ys\<close> \<open>\<forall> x \<in> xs. \<forall> y \<in> ys. x < y\<close> shows \<open>sorted_list_of_set (xs \<union> ys) = sorted_list_of_set xs @ (sorted_list_of_set ys)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted_list_of_set (xs \<union> ys) = sorted_list_of_set xs @ sorted_list_of_set ys
[PROOF STEP]
using assms(1,3)
[PROOF STATE]
proof (prove)
using this:
finite xs
\<forall>x\<in>xs. \<forall>y\<in>ys. x < y

goal (1 subgoal):
 1. sorted_list_of_set (xs \<union> ys) = sorted_list_of_set xs @ sorted_list_of_set ys
[PROOF STEP]
proof (induction \<open>xs\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>x\<in>{}. Ball ys ((<) x) \<Longrightarrow> sorted_list_of_set ({} \<union> ys) = sorted_list_of_set {} @ sorted_list_of_set ys
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<forall>x\<in>F. Ball ys ((<) x) \<Longrightarrow> sorted_list_of_set (F \<union> ys) = sorted_list_of_set F @ sorted_list_of_set ys; \<forall>x\<in>insert x F. Ball ys ((<) x)\<rbrakk> \<Longrightarrow> sorted_list_of_set (insert x F \<union> ys) = sorted_list_of_set (insert x F) @ sorted_list_of_set ys
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>{}. \<forall>a\<in>ys. x < a

goal (2 subgoals):
 1. \<forall>x\<in>{}. Ball ys ((<) x) \<Longrightarrow> sorted_list_of_set ({} \<union> ys) = sorted_list_of_set {} @ sorted_list_of_set ys
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<forall>x\<in>F. Ball ys ((<) x) \<Longrightarrow> sorted_list_of_set (F \<union> ys) = sorted_list_of_set F @ sorted_list_of_set ys; \<forall>x\<in>insert x F. Ball ys ((<) x)\<rbrakk> \<Longrightarrow> sorted_list_of_set (insert x F \<union> ys) = sorted_list_of_set (insert x F) @ sorted_list_of_set ys
[PROOF STEP]
thus \<open>?case\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>{}. \<forall>a\<in>ys. x < a

goal (1 subgoal):
 1. sorted_list_of_set ({} \<union> ys) = sorted_list_of_set {} @ sorted_list_of_set ys
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sorted_list_of_set ({} \<union> ys) = sorted_list_of_set {} @ sorted_list_of_set ys

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<forall>x\<in>F. Ball ys ((<) x) \<Longrightarrow> sorted_list_of_set (F \<union> ys) = sorted_list_of_set F @ sorted_list_of_set ys; \<forall>x\<in>insert x F. Ball ys ((<) x)\<rbrakk> \<Longrightarrow> sorted_list_of_set (insert x F \<union> ys) = sorted_list_of_set (insert x F) @ sorted_list_of_set ys
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<forall>x\<in>F. Ball ys ((<) x) \<Longrightarrow> sorted_list_of_set (F \<union> ys) = sorted_list_of_set F @ sorted_list_of_set ys; \<forall>x\<in>insert x F. Ball ys ((<) x)\<rbrakk> \<Longrightarrow> sorted_list_of_set (insert x F \<union> ys) = sorted_list_of_set (insert x F) @ sorted_list_of_set ys
[PROOF STEP]
case (insert x xs)
[PROOF STATE]
proof (state)
this:
finite xs
x \<notin> xs
\<forall>x\<in>xs. \<forall>a\<in>ys. x < a \<Longrightarrow> sorted_list_of_set (xs \<union> ys) = sorted_list_of_set xs @ sorted_list_of_set ys
\<forall>x\<in>insert x xs. \<forall>a\<in>ys. x < a

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<forall>x\<in>F. Ball ys ((<) x) \<Longrightarrow> sorted_list_of_set (F \<union> ys) = sorted_list_of_set F @ sorted_list_of_set ys; \<forall>x\<in>insert x F. Ball ys ((<) x)\<rbrakk> \<Longrightarrow> sorted_list_of_set (insert x F \<union> ys) = sorted_list_of_set (insert x F) @ sorted_list_of_set ys
[PROOF STEP]
hence iv: \<open>sorted_list_of_set (xs \<union> ys) = sorted_list_of_set xs @ sorted_list_of_set ys\<close>
[PROOF STATE]
proof (prove)
using this:
finite xs
x \<notin> xs
\<forall>x\<in>xs. \<forall>a\<in>ys. x < a \<Longrightarrow> sorted_list_of_set (xs \<union> ys) = sorted_list_of_set xs @ sorted_list_of_set ys
\<forall>x\<in>insert x xs. \<forall>a\<in>ys. x < a

goal (1 subgoal):
 1. sorted_list_of_set (xs \<union> ys) = sorted_list_of_set xs @ sorted_list_of_set ys
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
sorted_list_of_set (xs \<union> ys) = sorted_list_of_set xs @ sorted_list_of_set ys

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<forall>x\<in>F. Ball ys ((<) x) \<Longrightarrow> sorted_list_of_set (F \<union> ys) = sorted_list_of_set F @ sorted_list_of_set ys; \<forall>x\<in>insert x F. Ball ys ((<) x)\<rbrakk> \<Longrightarrow> sorted_list_of_set (insert x F \<union> ys) = sorted_list_of_set (insert x F) @ sorted_list_of_set ys
[PROOF STEP]
have le: \<open>\<forall> y \<in> set (sorted_list_of_set ys). x < y\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>y\<in>set (sorted_list_of_set ys). x < y
[PROOF STEP]
using insert(4) assms(2) sorted_list_of_set
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>insert x xs. \<forall>a\<in>ys. x < a
finite ys
finite ?A \<Longrightarrow> set (sorted_list_of_set ?A) = ?A
sorted (sorted_list_of_set ?A)
distinct (sorted_list_of_set ?A)

goal (1 subgoal):
 1. \<forall>y\<in>set (sorted_list_of_set ys). x < y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>y\<in>set (sorted_list_of_set ys). x < y

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<forall>x\<in>F. Ball ys ((<) x) \<Longrightarrow> sorted_list_of_set (F \<union> ys) = sorted_list_of_set F @ sorted_list_of_set ys; \<forall>x\<in>insert x F. Ball ys ((<) x)\<rbrakk> \<Longrightarrow> sorted_list_of_set (insert x F \<union> ys) = sorted_list_of_set (insert x F) @ sorted_list_of_set ys
[PROOF STEP]
have \<open>sorted_list_of_set (insert x xs \<union> ys) = sorted_list_of_set (insert x (xs \<union> ys))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted_list_of_set (insert x xs \<union> ys) = sorted_list_of_set (insert x (xs \<union> ys))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sorted_list_of_set (insert x xs \<union> ys) = sorted_list_of_set (insert x (xs \<union> ys))

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<forall>x\<in>F. Ball ys ((<) x) \<Longrightarrow> sorted_list_of_set (F \<union> ys) = sorted_list_of_set F @ sorted_list_of_set ys; \<forall>x\<in>insert x F. Ball ys ((<) x)\<rbrakk> \<Longrightarrow> sorted_list_of_set (insert x F \<union> ys) = sorted_list_of_set (insert x F) @ sorted_list_of_set ys
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sorted_list_of_set (insert x xs \<union> ys) = sorted_list_of_set (insert x (xs \<union> ys))

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<forall>x\<in>F. Ball ys ((<) x) \<Longrightarrow> sorted_list_of_set (F \<union> ys) = sorted_list_of_set F @ sorted_list_of_set ys; \<forall>x\<in>insert x F. Ball ys ((<) x)\<rbrakk> \<Longrightarrow> sorted_list_of_set (insert x F \<union> ys) = sorted_list_of_set (insert x F) @ sorted_list_of_set ys
[PROOF STEP]
have \<open>\<dots> = insort x (sorted_list_of_set (xs \<union> ys))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted_list_of_set (insert x (xs \<union> ys)) = insort x (sorted_list_of_set (xs \<union> ys))
[PROOF STEP]
by (metis Un_iff assms(2) finite_Un insert.hyps(1) insert.hyps(2) insert.prems insertI1 less_irrefl sorted_list_of_set_insert)
[PROOF STATE]
proof (state)
this:
sorted_list_of_set (insert x (xs \<union> ys)) = insort x (sorted_list_of_set (xs \<union> ys))

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<forall>x\<in>F. Ball ys ((<) x) \<Longrightarrow> sorted_list_of_set (F \<union> ys) = sorted_list_of_set F @ sorted_list_of_set ys; \<forall>x\<in>insert x F. Ball ys ((<) x)\<rbrakk> \<Longrightarrow> sorted_list_of_set (insert x F \<union> ys) = sorted_list_of_set (insert x F) @ sorted_list_of_set ys
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sorted_list_of_set (insert x (xs \<union> ys)) = insort x (sorted_list_of_set (xs \<union> ys))

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<forall>x\<in>F. Ball ys ((<) x) \<Longrightarrow> sorted_list_of_set (F \<union> ys) = sorted_list_of_set F @ sorted_list_of_set ys; \<forall>x\<in>insert x F. Ball ys ((<) x)\<rbrakk> \<Longrightarrow> sorted_list_of_set (insert x F \<union> ys) = sorted_list_of_set (insert x F) @ sorted_list_of_set ys
[PROOF STEP]
have \<open>\<dots> = insort x (sorted_list_of_set xs @ sorted_list_of_set ys)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insort x (sorted_list_of_set (xs \<union> ys)) = insort x (sorted_list_of_set xs @ sorted_list_of_set ys)
[PROOF STEP]
using iv
[PROOF STATE]
proof (prove)
using this:
sorted_list_of_set (xs \<union> ys) = sorted_list_of_set xs @ sorted_list_of_set ys

goal (1 subgoal):
 1. insort x (sorted_list_of_set (xs \<union> ys)) = insort x (sorted_list_of_set xs @ sorted_list_of_set ys)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
insort x (sorted_list_of_set (xs \<union> ys)) = insort x (sorted_list_of_set xs @ sorted_list_of_set ys)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<forall>x\<in>F. Ball ys ((<) x) \<Longrightarrow> sorted_list_of_set (F \<union> ys) = sorted_list_of_set F @ sorted_list_of_set ys; \<forall>x\<in>insert x F. Ball ys ((<) x)\<rbrakk> \<Longrightarrow> sorted_list_of_set (insert x F \<union> ys) = sorted_list_of_set (insert x F) @ sorted_list_of_set ys
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
insort x (sorted_list_of_set (xs \<union> ys)) = insort x (sorted_list_of_set xs @ sorted_list_of_set ys)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<forall>x\<in>F. Ball ys ((<) x) \<Longrightarrow> sorted_list_of_set (F \<union> ys) = sorted_list_of_set F @ sorted_list_of_set ys; \<forall>x\<in>insert x F. Ball ys ((<) x)\<rbrakk> \<Longrightarrow> sorted_list_of_set (insert x F \<union> ys) = sorted_list_of_set (insert x F) @ sorted_list_of_set ys
[PROOF STEP]
have \<open>\<dots> = insort x (sorted_list_of_set xs) @ sorted_list_of_set ys\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insort x (sorted_list_of_set xs @ sorted_list_of_set ys) = insort x (sorted_list_of_set xs) @ sorted_list_of_set ys
[PROOF STEP]
by (metis le insort_append_first less_le_not_le)
[PROOF STATE]
proof (state)
this:
insort x (sorted_list_of_set xs @ sorted_list_of_set ys) = insort x (sorted_list_of_set xs) @ sorted_list_of_set ys

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<forall>x\<in>F. Ball ys ((<) x) \<Longrightarrow> sorted_list_of_set (F \<union> ys) = sorted_list_of_set F @ sorted_list_of_set ys; \<forall>x\<in>insert x F. Ball ys ((<) x)\<rbrakk> \<Longrightarrow> sorted_list_of_set (insert x F \<union> ys) = sorted_list_of_set (insert x F) @ sorted_list_of_set ys
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
insort x (sorted_list_of_set xs @ sorted_list_of_set ys) = insort x (sorted_list_of_set xs) @ sorted_list_of_set ys

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<forall>x\<in>F. Ball ys ((<) x) \<Longrightarrow> sorted_list_of_set (F \<union> ys) = sorted_list_of_set F @ sorted_list_of_set ys; \<forall>x\<in>insert x F. Ball ys ((<) x)\<rbrakk> \<Longrightarrow> sorted_list_of_set (insert x F \<union> ys) = sorted_list_of_set (insert x F) @ sorted_list_of_set ys
[PROOF STEP]
have \<open>\<dots> = sorted_list_of_set (insert x xs) @ sorted_list_of_set ys\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insort x (sorted_list_of_set xs) @ sorted_list_of_set ys = sorted_list_of_set (insert x xs) @ sorted_list_of_set ys
[PROOF STEP]
using sorted_list_of_set_insert[OF insert(1),of \<open>x\<close>] insert(2)
[PROOF STATE]
proof (prove)
using this:
x \<notin> xs \<Longrightarrow> sorted_list_of_set (insert x xs) = insort x (sorted_list_of_set xs)
x \<notin> xs

goal (1 subgoal):
 1. insort x (sorted_list_of_set xs) @ sorted_list_of_set ys = sorted_list_of_set (insert x xs) @ sorted_list_of_set ys
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insort x (sorted_list_of_set xs) @ sorted_list_of_set ys = sorted_list_of_set (insert x xs) @ sorted_list_of_set ys

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<forall>x\<in>F. Ball ys ((<) x) \<Longrightarrow> sorted_list_of_set (F \<union> ys) = sorted_list_of_set F @ sorted_list_of_set ys; \<forall>x\<in>insert x F. Ball ys ((<) x)\<rbrakk> \<Longrightarrow> sorted_list_of_set (insert x F \<union> ys) = sorted_list_of_set (insert x F) @ sorted_list_of_set ys
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sorted_list_of_set (insert x xs \<union> ys) = sorted_list_of_set (insert x xs) @ sorted_list_of_set ys
[PROOF STEP]
show \<open>?case\<close>
[PROOF STATE]
proof (prove)
using this:
sorted_list_of_set (insert x xs \<union> ys) = sorted_list_of_set (insert x xs) @ sorted_list_of_set ys

goal (1 subgoal):
 1. sorted_list_of_set (insert x xs \<union> ys) = sorted_list_of_set (insert x xs) @ sorted_list_of_set ys
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
sorted_list_of_set (insert x xs \<union> ys) = sorted_list_of_set (insert x xs) @ sorted_list_of_set ys

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma filter_insort: \<open>sorted xs \<Longrightarrow> filter P (insort x xs) = (if P x then insort x (filter P xs) else filter P xs)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted xs \<Longrightarrow> filter P (insort x xs) = (if P x then insort x (filter P xs) else filter P xs)
[PROOF STEP]
by (induction \<open>xs\<close>, simp) (metis filter_insort filter_insort_triv map_ident)


[STATEMENT]
lemma filter_sorted_list_of_set: assumes \<open>finite xs\<close> shows \<open>filter P (sorted_list_of_set xs) = sorted_list_of_set {x \<in> xs. P x}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter P (sorted_list_of_set xs) = sorted_list_of_set {x \<in> xs. P x}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite xs

goal (1 subgoal):
 1. filter P (sorted_list_of_set xs) = sorted_list_of_set {x \<in> xs. P x}
[PROOF STEP]
proof(induction \<open>xs\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. filter P (sorted_list_of_set {}) = sorted_list_of_set {x \<in> {}. P x}
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; filter P (sorted_list_of_set F) = sorted_list_of_set {x \<in> F. P x}\<rbrakk> \<Longrightarrow> filter P (sorted_list_of_set (insert x F)) = sorted_list_of_set {xa \<in> insert x F. P xa}
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. filter P (sorted_list_of_set {}) = sorted_list_of_set {x \<in> {}. P x}
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; filter P (sorted_list_of_set F) = sorted_list_of_set {x \<in> F. P x}\<rbrakk> \<Longrightarrow> filter P (sorted_list_of_set (insert x F)) = sorted_list_of_set {xa \<in> insert x F. P xa}
[PROOF STEP]
thus \<open>?case\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter P (sorted_list_of_set {}) = sorted_list_of_set {x \<in> {}. P x}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
filter P (sorted_list_of_set {}) = sorted_list_of_set {x \<in> {}. P x}

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; filter P (sorted_list_of_set F) = sorted_list_of_set {x \<in> F. P x}\<rbrakk> \<Longrightarrow> filter P (sorted_list_of_set (insert x F)) = sorted_list_of_set {xa \<in> insert x F. P xa}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; filter P (sorted_list_of_set F) = sorted_list_of_set {x \<in> F. P x}\<rbrakk> \<Longrightarrow> filter P (sorted_list_of_set (insert x F)) = sorted_list_of_set {xa \<in> insert x F. P xa}
[PROOF STEP]
case (insert x xs)
[PROOF STATE]
proof (state)
this:
finite xs
x \<notin> xs
filter P (sorted_list_of_set xs) = sorted_list_of_set {x \<in> xs. P x}

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; filter P (sorted_list_of_set F) = sorted_list_of_set {x \<in> F. P x}\<rbrakk> \<Longrightarrow> filter P (sorted_list_of_set (insert x F)) = sorted_list_of_set {xa \<in> insert x F. P xa}
[PROOF STEP]
have *: \<open>set (sorted_list_of_set xs) = xs\<close> \<open>sorted (sorted_list_of_set xs)\<close> \<open>distinct (sorted_list_of_set xs)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (sorted_list_of_set xs) = xs &&& sorted (sorted_list_of_set xs) &&& distinct (sorted_list_of_set xs)
[PROOF STEP]
by (auto simp add: insert.hyps(1))
[PROOF STATE]
proof (state)
this:
set (sorted_list_of_set xs) = xs
sorted (sorted_list_of_set xs)
distinct (sorted_list_of_set xs)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; filter P (sorted_list_of_set F) = sorted_list_of_set {x \<in> F. P x}\<rbrakk> \<Longrightarrow> filter P (sorted_list_of_set (insert x F)) = sorted_list_of_set {xa \<in> insert x F. P xa}
[PROOF STEP]
have **: \<open>P x \<Longrightarrow> {y \<in> insert x xs. P y} = insert x {y \<in> xs. P y}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P x \<Longrightarrow> {y \<in> insert x xs. P y} = insert x {y \<in> xs. P y}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P x \<Longrightarrow> {y \<in> insert x xs. P y} = insert x {y \<in> xs. P y}

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; filter P (sorted_list_of_set F) = sorted_list_of_set {x \<in> F. P x}\<rbrakk> \<Longrightarrow> filter P (sorted_list_of_set (insert x F)) = sorted_list_of_set {xa \<in> insert x F. P xa}
[PROOF STEP]
have ***: \<open>\<not> P x \<Longrightarrow> {y \<in> insert x xs. P y} = {y \<in> xs. P y}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> P x \<Longrightarrow> {y \<in> insert x xs. P y} = {y \<in> xs. P y}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> P x \<Longrightarrow> {y \<in> insert x xs. P y} = {y \<in> xs. P y}

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; filter P (sorted_list_of_set F) = sorted_list_of_set {x \<in> F. P x}\<rbrakk> \<Longrightarrow> filter P (sorted_list_of_set (insert x F)) = sorted_list_of_set {xa \<in> insert x F. P xa}
[PROOF STEP]
note filter_insort[OF *(2),of \<open>P\<close> \<open>x\<close>] sorted_list_of_set_insert[OF insert(1), of \<open>x\<close>] insert(2,3) ** ***
[PROOF STATE]
proof (state)
this:
filter P (insort x (sorted_list_of_set xs)) = (if P x then insort x (filter P (sorted_list_of_set xs)) else filter P (sorted_list_of_set xs))
x \<notin> xs \<Longrightarrow> sorted_list_of_set (insert x xs) = insort x (sorted_list_of_set xs)
x \<notin> xs
filter P (sorted_list_of_set xs) = sorted_list_of_set {x \<in> xs. P x}
P x \<Longrightarrow> {y \<in> insert x xs. P y} = insert x {y \<in> xs. P y}
\<not> P x \<Longrightarrow> {y \<in> insert x xs. P y} = {y \<in> xs. P y}

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; filter P (sorted_list_of_set F) = sorted_list_of_set {x \<in> F. P x}\<rbrakk> \<Longrightarrow> filter P (sorted_list_of_set (insert x F)) = sorted_list_of_set {xa \<in> insert x F. P xa}
[PROOF STEP]
thus \<open>?case\<close>
[PROOF STATE]
proof (prove)
using this:
filter P (insort x (sorted_list_of_set xs)) = (if P x then insort x (filter P (sorted_list_of_set xs)) else filter P (sorted_list_of_set xs))
x \<notin> xs \<Longrightarrow> sorted_list_of_set (insert x xs) = insort x (sorted_list_of_set xs)
x \<notin> xs
filter P (sorted_list_of_set xs) = sorted_list_of_set {x \<in> xs. P x}
P x \<Longrightarrow> {y \<in> insert x xs. P y} = insert x {y \<in> xs. P y}
\<not> P x \<Longrightarrow> {y \<in> insert x xs. P y} = {y \<in> xs. P y}

goal (1 subgoal):
 1. filter P (sorted_list_of_set (insert x xs)) = sorted_list_of_set {xa \<in> insert x xs. P xa}
[PROOF STEP]
by (metis (mono_tags) "*"(1) List.finite_set distinct_filter distinct_insort distinct_sorted_list_of_set set_filter sorted_list_of_set_insert)
[PROOF STATE]
proof (state)
this:
filter P (sorted_list_of_set (insert x xs)) = sorted_list_of_set {xa \<in> insert x xs. P xa}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma unbounded_nat_set_infinite: assumes \<open>\<forall> (i::nat). \<exists> j\<ge>i. j \<in> A\<close> shows \<open>\<not> finite A\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<exists>j\<ge>i. j \<in> A

goal (1 subgoal):
 1. infinite A
[PROOF STEP]
by (metis finite_nat_set_iff_bounded_le not_less_eq_eq)


[STATEMENT]
lemma infinite_ascending: assumes nf: \<open>\<not> finite (A::nat set)\<close> obtains f where \<open>range f = A\<close> \<open>\<forall> i. f i < f (Suc i)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> range ?f2 = A
 2. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> \<forall>i. ?f2 i < ?f2 (Suc i)
[PROOF STEP]
let \<open>?f\<close> = \<open>\<lambda> i. (LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i)\<close>
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> range ?f2 = A
 2. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> \<forall>i. ?f2 i < ?f2 (Suc i)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> range ?f2 = A
 2. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> \<forall>i. ?f2 i < ?f2 (Suc i)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> range ?f2 = A
 2. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> \<forall>i. ?f2 i < ?f2 (Suc i)
[PROOF STEP]
obtain a where \<open>a \<in> A\<close> \<open>card (A \<inter> {..<a}) = i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof (induction \<open>i\<close> arbitrary: \<open>thesis\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>thesis. (\<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
 2. \<And>i thesis. \<lbrakk>\<And>thesis. (\<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis; \<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = Suc i\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a \<in> A; card (A \<inter> {..<?a}) = 0\<rbrakk> \<Longrightarrow> thesis

goal (2 subgoals):
 1. \<And>thesis. (\<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
 2. \<And>i thesis. \<lbrakk>\<And>thesis. (\<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis; \<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = Suc i\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
let \<open>?a0\<close> = \<open>(LEAST a. a \<in> A)\<close>
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>thesis. (\<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
 2. \<And>i thesis. \<lbrakk>\<And>thesis. (\<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis; \<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = Suc i\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have \<open>?a0 \<in> A\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST a. a \<in> A) \<in> A
[PROOF STEP]
by (metis LeastI empty_iff finite.emptyI nf set_eq_iff)
[PROOF STATE]
proof (state)
this:
(LEAST a. a \<in> A) \<in> A

goal (2 subgoals):
 1. \<And>thesis. (\<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
 2. \<And>i thesis. \<lbrakk>\<And>thesis. (\<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis; \<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = Suc i\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(LEAST a. a \<in> A) \<in> A

goal (2 subgoals):
 1. \<And>thesis. (\<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
 2. \<And>i thesis. \<lbrakk>\<And>thesis. (\<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis; \<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = Suc i\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have \<open>\<And>b. b \<in> A \<Longrightarrow> ?a0 \<le> b\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. b \<in> A \<Longrightarrow> (LEAST a. a \<in> A) \<le> b
[PROOF STEP]
by (metis Least_le)
[PROOF STATE]
proof (state)
this:
?b \<in> A \<Longrightarrow> (LEAST a. a \<in> A) \<le> ?b

goal (2 subgoals):
 1. \<And>thesis. (\<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
 2. \<And>i thesis. \<lbrakk>\<And>thesis. (\<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis; \<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = Suc i\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
hence \<open>card (A \<inter> {..<?a}) = 0\<close>
[PROOF STATE]
proof (prove)
using this:
?b \<in> A \<Longrightarrow> (LEAST a. a \<in> A) \<le> ?b

goal (1 subgoal):
 1. card (A \<inter> {..<LEAST a. a \<in> A}) = 0
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
card (A \<inter> {..<LEAST a. a \<in> A}) = 0

goal (2 subgoals):
 1. \<And>thesis. (\<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
 2. \<And>i thesis. \<lbrakk>\<And>thesis. (\<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis; \<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = Suc i\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(LEAST a. a \<in> A) \<in> A
card (A \<inter> {..<LEAST a. a \<in> A}) = 0
[PROOF STEP]
show \<open>?case\<close>
[PROOF STATE]
proof (prove)
using this:
(LEAST a. a \<in> A) \<in> A
card (A \<inter> {..<LEAST a. a \<in> A}) = 0

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using 0
[PROOF STATE]
proof (prove)
using this:
(LEAST a. a \<in> A) \<in> A
card (A \<inter> {..<LEAST a. a \<in> A}) = 0
\<lbrakk>?a \<in> A; card (A \<inter> {..<?a}) = 0\<rbrakk> \<Longrightarrow> thesis

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

goal (1 subgoal):
 1. \<And>i thesis. \<lbrakk>\<And>thesis. (\<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis; \<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = Suc i\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i thesis. \<lbrakk>\<And>thesis. (\<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis; \<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = Suc i\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case (Suc i)
[PROOF STATE]
proof (state)
this:
(\<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = i\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
\<lbrakk>?a \<in> A; card (A \<inter> {..<?a}) = Suc i\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. \<And>i thesis. \<lbrakk>\<And>thesis. (\<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis; \<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = Suc i\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
obtain a where aa: \<open>a \<in> A\<close> and card: \<open>card (A \<inter> {..<a}) = i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Suc.IH
[PROOF STATE]
proof (prove)
using this:
(\<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = i\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
a \<in> A
card (A \<inter> {..<a}) = i

goal (1 subgoal):
 1. \<And>i thesis. \<lbrakk>\<And>thesis. (\<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis; \<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = Suc i\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have nf': \<open>~ finite (A - {..a})\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite (A - {..a})
[PROOF STEP]
using nf
[PROOF STATE]
proof (prove)
using this:
infinite A

goal (1 subgoal):
 1. infinite (A - {..a})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
infinite (A - {..a})

goal (1 subgoal):
 1. \<And>i thesis. \<lbrakk>\<And>thesis. (\<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis; \<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = Suc i\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
let \<open>?b\<close> = \<open>LEAST b. b \<in> A - {..a}\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i thesis. \<lbrakk>\<And>thesis. (\<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis; \<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = Suc i\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have bin: \<open>?b \<in> A-{..a}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST b. b \<in> A - {..a}) \<in> A - {..a}
[PROOF STEP]
by (metis LeastI empty_iff finite.emptyI nf' set_eq_iff)
[PROOF STATE]
proof (state)
this:
(LEAST b. b \<in> A - {..a}) \<in> A - {..a}

goal (1 subgoal):
 1. \<And>i thesis. \<lbrakk>\<And>thesis. (\<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis; \<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = Suc i\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have le: \<open>\<And>c. c \<in> A-{..a} \<Longrightarrow> ?b \<le> c\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c. c \<in> A - {..a} \<Longrightarrow> (LEAST b. b \<in> A - {..a}) \<le> c
[PROOF STEP]
by (metis Least_le)
[PROOF STATE]
proof (state)
this:
?c \<in> A - {..a} \<Longrightarrow> (LEAST b. b \<in> A - {..a}) \<le> ?c

goal (1 subgoal):
 1. \<And>i thesis. \<lbrakk>\<And>thesis. (\<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis; \<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = Suc i\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have ab: \<open>a < ?b\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a < (LEAST b. b \<in> A - {..a})
[PROOF STEP]
using bin
[PROOF STATE]
proof (prove)
using this:
(LEAST b. b \<in> A - {..a}) \<in> A - {..a}

goal (1 subgoal):
 1. a < (LEAST b. b \<in> A - {..a})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a < (LEAST b. b \<in> A - {..a})

goal (1 subgoal):
 1. \<And>i thesis. \<lbrakk>\<And>thesis. (\<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis; \<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = Suc i\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have \<open>\<And> c. c \<in> A \<Longrightarrow> c < ?b \<Longrightarrow> c \<le> a\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>c \<in> A; c < (LEAST b. b \<in> A - {..a})\<rbrakk> \<Longrightarrow> c \<le> a
[PROOF STEP]
using le
[PROOF STATE]
proof (prove)
using this:
?c \<in> A - {..a} \<Longrightarrow> (LEAST b. b \<in> A - {..a}) \<le> ?c

goal (1 subgoal):
 1. \<And>c. \<lbrakk>c \<in> A; c < (LEAST b. b \<in> A - {..a})\<rbrakk> \<Longrightarrow> c \<le> a
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<lbrakk>?c \<in> A; ?c < (LEAST b. b \<in> A - {..a})\<rbrakk> \<Longrightarrow> ?c \<le> a

goal (1 subgoal):
 1. \<And>i thesis. \<lbrakk>\<And>thesis. (\<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis; \<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = Suc i\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
hence \<open>A \<inter> {..<?b} = insert a (A \<inter> {..<a})\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?c \<in> A; ?c < (LEAST b. b \<in> A - {..a})\<rbrakk> \<Longrightarrow> ?c \<le> a

goal (1 subgoal):
 1. A \<inter> {..<LEAST b. b \<in> A - {..a}} = insert a (A \<inter> {..<a})
[PROOF STEP]
using bin ab aa
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?c \<in> A; ?c < (LEAST b. b \<in> A - {..a})\<rbrakk> \<Longrightarrow> ?c \<le> a
(LEAST b. b \<in> A - {..a}) \<in> A - {..a}
a < (LEAST b. b \<in> A - {..a})
a \<in> A

goal (1 subgoal):
 1. A \<inter> {..<LEAST b. b \<in> A - {..a}} = insert a (A \<inter> {..<a})
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
A \<inter> {..<LEAST b. b \<in> A - {..a}} = insert a (A \<inter> {..<a})

goal (1 subgoal):
 1. \<And>i thesis. \<lbrakk>\<And>thesis. (\<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis; \<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = Suc i\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
hence \<open>card (A \<inter>{..<?b}) = Suc i\<close>
[PROOF STATE]
proof (prove)
using this:
A \<inter> {..<LEAST b. b \<in> A - {..a}} = insert a (A \<inter> {..<a})

goal (1 subgoal):
 1. card (A \<inter> {..<LEAST b. b \<in> A - {..a}}) = Suc i
[PROOF STEP]
using card
[PROOF STATE]
proof (prove)
using this:
A \<inter> {..<LEAST b. b \<in> A - {..a}} = insert a (A \<inter> {..<a})
card (A \<inter> {..<a}) = i

goal (1 subgoal):
 1. card (A \<inter> {..<LEAST b. b \<in> A - {..a}}) = Suc i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (A \<inter> {..<LEAST b. b \<in> A - {..a}}) = Suc i

goal (1 subgoal):
 1. \<And>i thesis. \<lbrakk>\<And>thesis. (\<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis; \<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = Suc i\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
thus \<open>?case\<close>
[PROOF STATE]
proof (prove)
using this:
card (A \<inter> {..<LEAST b. b \<in> A - {..a}}) = Suc i

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using Suc.prems bin
[PROOF STATE]
proof (prove)
using this:
card (A \<inter> {..<LEAST b. b \<in> A - {..a}}) = Suc i
\<lbrakk>?a \<in> A; card (A \<inter> {..<?a}) = Suc i\<rbrakk> \<Longrightarrow> thesis
(LEAST b. b \<in> A - {..a}) \<in> A - {..a}

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
a \<in> A
card (A \<inter> {..<a}) = i

goal (2 subgoals):
 1. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> range ?f2 = A
 2. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> \<forall>i. ?f2 i < ?f2 (Suc i)
[PROOF STEP]
note \<open>\<And> thesis. ((\<And>a. a \<in> A \<Longrightarrow> card (A \<inter> {..<a}) = i \<Longrightarrow> thesis) \<Longrightarrow> thesis)\<close>
[PROOF STATE]
proof (state)
this:
(\<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = i\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (2 subgoals):
 1. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> range ?f2 = A
 2. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> \<forall>i. ?f2 i < ?f2 (Suc i)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(\<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = ?i8\<rbrakk> \<Longrightarrow> ?thesisb5) \<Longrightarrow> ?thesisb5

goal (2 subgoals):
 1. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> range ?f2 = A
 2. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> \<forall>i. ?f2 i < ?f2 (Suc i)
[PROOF STEP]
note ex = this
[PROOF STATE]
proof (state)
this:
(\<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = ?i8\<rbrakk> \<Longrightarrow> ?thesisb5) \<Longrightarrow> ?thesisb5

goal (2 subgoals):
 1. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> range ?f2 = A
 2. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> \<forall>i. ?f2 i < ?f2 (Suc i)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(\<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = ?i8\<rbrakk> \<Longrightarrow> ?thesisb5) \<Longrightarrow> ?thesisb5

goal (2 subgoals):
 1. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> range ?f2 = A
 2. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> \<forall>i. ?f2 i < ?f2 (Suc i)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> range ?f2 = A
 2. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> \<forall>i. ?f2 i < ?f2 (Suc i)
[PROOF STEP]
obtain a where a: \<open>a \<in> A \<and> card (A \<inter>{..<a}) = i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a. a \<in> A \<and> card (A \<inter> {..<a}) = i \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ex
[PROOF STATE]
proof (prove)
using this:
(\<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = ?i8\<rbrakk> \<Longrightarrow> ?thesisb5) \<Longrightarrow> ?thesisb5

goal (1 subgoal):
 1. (\<And>a. a \<in> A \<and> card (A \<inter> {..<a}) = i \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a \<in> A \<and> card (A \<inter> {..<a}) = i

goal (2 subgoals):
 1. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> range ?f2 = A
 2. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> \<forall>i. ?f2 i < ?f2 (Suc i)
[PROOF STEP]
have ina: \<open>?f i \<in> A\<close> and card: \<open>card (A \<inter>{..<?f i}) = i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i) \<in> A &&& card (A \<inter> {..<LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i}) = i
[PROOF STEP]
using LeastI[of \<open>\<lambda> a. a \<in> A \<and> card (A \<inter>{..<a}) = i\<close> \<open>a\<close>, OF a]
[PROOF STATE]
proof (prove)
using this:
(LEAST x. x \<in> A \<and> card (A \<inter> {..<x}) = i) \<in> A \<and> card (A \<inter> {..<LEAST x. x \<in> A \<and> card (A \<inter> {..<x}) = i}) = i

goal (1 subgoal):
 1. (LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i) \<in> A &&& card (A \<inter> {..<LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i}) = i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i) \<in> A
card (A \<inter> {..<LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i}) = i

goal (2 subgoals):
 1. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> range ?f2 = A
 2. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> \<forall>i. ?f2 i < ?f2 (Suc i)
[PROOF STEP]
obtain b where b: \<open>b \<in> A \<and> card (A \<inter>{..<b}) = Suc i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>b. b \<in> A \<and> card (A \<inter> {..<b}) = Suc i \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ex
[PROOF STATE]
proof (prove)
using this:
(\<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = ?i8\<rbrakk> \<Longrightarrow> ?thesisb5) \<Longrightarrow> ?thesisb5

goal (1 subgoal):
 1. (\<And>b. b \<in> A \<and> card (A \<inter> {..<b}) = Suc i \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
b \<in> A \<and> card (A \<inter> {..<b}) = Suc i

goal (2 subgoals):
 1. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> range ?f2 = A
 2. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> \<forall>i. ?f2 i < ?f2 (Suc i)
[PROOF STEP]
have inab: \<open>?f (Suc i) \<in> A\<close> and cardb: \<open>card (A \<inter>{..<?f (Suc i)}) = Suc i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = Suc i) \<in> A &&& card (A \<inter> {..<LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = Suc i}) = Suc i
[PROOF STEP]
using LeastI[of \<open>\<lambda> a. a \<in> A \<and> card (A \<inter>{..<a}) = Suc i\<close> \<open>b\<close>, OF b]
[PROOF STATE]
proof (prove)
using this:
(LEAST x. x \<in> A \<and> card (A \<inter> {..<x}) = Suc i) \<in> A \<and> card (A \<inter> {..<LEAST x. x \<in> A \<and> card (A \<inter> {..<x}) = Suc i}) = Suc i

goal (1 subgoal):
 1. (LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = Suc i) \<in> A &&& card (A \<inter> {..<LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = Suc i}) = Suc i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = Suc i) \<in> A
card (A \<inter> {..<LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = Suc i}) = Suc i

goal (2 subgoals):
 1. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> range ?f2 = A
 2. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> \<forall>i. ?f2 i < ?f2 (Suc i)
[PROOF STEP]
have \<open>?f i < ?f (Suc i)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i) < (LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = Suc i)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i) < (LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = Suc i) \<Longrightarrow> False
[PROOF STEP]
assume \<open>\<not> ?f i < ?f (Suc i)\<close>
[PROOF STATE]
proof (state)
this:
\<not> (LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i) < (LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = Suc i)

goal (1 subgoal):
 1. \<not> (LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i) < (LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = Suc i) \<Longrightarrow> False
[PROOF STEP]
hence \<open>A \<inter>{..<?f (Suc i)} \<subseteq> A \<inter>{..<?f i}\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> (LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i) < (LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = Suc i)

goal (1 subgoal):
 1. A \<inter> {..<LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = Suc i} \<subseteq> A \<inter> {..<LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<inter> {..<LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = Suc i} \<subseteq> A \<inter> {..<LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i}

goal (1 subgoal):
 1. \<not> (LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i) < (LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = Suc i) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
A \<inter> {..<LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = Suc i} \<subseteq> A \<inter> {..<LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i}

goal (1 subgoal):
 1. \<not> (LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i) < (LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = Suc i) \<Longrightarrow> False
[PROOF STEP]
have \<open>finite (A \<inter>{..<?f i})\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (A \<inter> {..<LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (A \<inter> {..<LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i})

goal (1 subgoal):
 1. \<not> (LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i) < (LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = Suc i) \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
A \<inter> {..<LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = Suc i} \<subseteq> A \<inter> {..<LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i}
finite (A \<inter> {..<LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i})
[PROOF STEP]
have \<open>card(A \<inter>{..<?f (Suc i)}) \<le> card (A \<inter>{..<?f i})\<close>
[PROOF STATE]
proof (prove)
using this:
A \<inter> {..<LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = Suc i} \<subseteq> A \<inter> {..<LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i}
finite (A \<inter> {..<LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i})

goal (1 subgoal):
 1. card (A \<inter> {..<LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = Suc i}) \<le> card (A \<inter> {..<LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i})
[PROOF STEP]
by (metis (erased, lifting) card_mono)
[PROOF STATE]
proof (state)
this:
card (A \<inter> {..<LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = Suc i}) \<le> card (A \<inter> {..<LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i})

goal (1 subgoal):
 1. \<not> (LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i) < (LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = Suc i) \<Longrightarrow> False
[PROOF STEP]
thus \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
card (A \<inter> {..<LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = Suc i}) \<le> card (A \<inter> {..<LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i})

goal (1 subgoal):
 1. False
[PROOF STEP]
using card cardb
[PROOF STATE]
proof (prove)
using this:
card (A \<inter> {..<LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = Suc i}) \<le> card (A \<inter> {..<LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i})
card (A \<inter> {..<LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i}) = i
card (A \<inter> {..<LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = Suc i}) = Suc i

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i) < (LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = Suc i)

goal (2 subgoals):
 1. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> range ?f2 = A
 2. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> \<forall>i. ?f2 i < ?f2 (Suc i)
[PROOF STEP]
note this ina
[PROOF STATE]
proof (state)
this:
(LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i) < (LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = Suc i)
(LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i) \<in> A

goal (2 subgoals):
 1. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> range ?f2 = A
 2. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> \<forall>i. ?f2 i < ?f2 (Suc i)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = ?i2) < (LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = Suc ?i2)
(LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = ?i2) \<in> A

goal (2 subgoals):
 1. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> range ?f2 = A
 2. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> \<forall>i. ?f2 i < ?f2 (Suc i)
[PROOF STEP]
note b = this
[PROOF STATE]
proof (state)
this:
(LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = ?i2) < (LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = Suc ?i2)
(LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = ?i2) \<in> A

goal (2 subgoals):
 1. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> range ?f2 = A
 2. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> \<forall>i. ?f2 i < ?f2 (Suc i)
[PROOF STEP]
thus \<open>\<forall> i. ?f i < ?f (Suc i)\<close>
[PROOF STATE]
proof (prove)
using this:
(LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = ?i2) < (LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = Suc ?i2)
(LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = ?i2) \<in> A

goal (1 subgoal):
 1. \<forall>i. (LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i) < (LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = Suc i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i. (LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i) < (LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = Suc i)

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> range (\<lambda>i. LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i) = A
[PROOF STEP]
have *: \<open>range ?f \<subseteq> A\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. range (\<lambda>i. LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i) \<subseteq> A
[PROOF STEP]
using b
[PROOF STATE]
proof (prove)
using this:
(LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = ?i2) < (LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = Suc ?i2)
(LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = ?i2) \<in> A

goal (1 subgoal):
 1. range (\<lambda>i. LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i) \<subseteq> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
range (\<lambda>i. LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i) \<subseteq> A

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> range (\<lambda>i. LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i) = A
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
range (\<lambda>i. LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i) \<subseteq> A

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> range (\<lambda>i. LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i) = A
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
range (\<lambda>i. LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i) \<subseteq> A

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> range (\<lambda>i. LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i) = A
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> range (\<lambda>i. LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i) = A
[PROOF STEP]
assume ina: \<open>a \<in> A\<close>
[PROOF STATE]
proof (state)
this:
a \<in> A

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> range (\<lambda>i. LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i) = A
[PROOF STEP]
let \<open>?i\<close> = \<open>card (A \<inter> {..<a})\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> range (\<lambda>i. LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i) = A
[PROOF STEP]
obtain b where b: \<open>b \<in> A \<and> card (A \<inter>{..<b}) = ?i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>b. b \<in> A \<and> card (A \<inter> {..<b}) = card (A \<inter> {..<a}) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ex
[PROOF STATE]
proof (prove)
using this:
(\<And>a. \<lbrakk>a \<in> A; card (A \<inter> {..<a}) = ?i8\<rbrakk> \<Longrightarrow> ?thesisb5) \<Longrightarrow> ?thesisb5

goal (1 subgoal):
 1. (\<And>b. b \<in> A \<and> card (A \<inter> {..<b}) = card (A \<inter> {..<a}) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
b \<in> A \<and> card (A \<inter> {..<b}) = card (A \<inter> {..<a})

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> range (\<lambda>i. LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i) = A
[PROOF STEP]
have inab: \<open>?f ?i \<in> A\<close> and cardb: \<open>card (A \<inter>{..<?f ?i}) = ?i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a})) \<in> A &&& card (A \<inter> {..<LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a})}) = card (A \<inter> {..<a})
[PROOF STEP]
using LeastI[of \<open>\<lambda> a. a \<in> A \<and> card (A \<inter>{..<a}) = ?i\<close> \<open>b\<close>, OF b]
[PROOF STATE]
proof (prove)
using this:
(LEAST x. x \<in> A \<and> card (A \<inter> {..<x}) = card (A \<inter> {..<a})) \<in> A \<and> card (A \<inter> {..<LEAST x. x \<in> A \<and> card (A \<inter> {..<x}) = card (A \<inter> {..<a})}) = card (A \<inter> {..<a})

goal (1 subgoal):
 1. (LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a})) \<in> A &&& card (A \<inter> {..<LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a})}) = card (A \<inter> {..<a})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a})) \<in> A
card (A \<inter> {..<LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a})}) = card (A \<inter> {..<a})

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> range (\<lambda>i. LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i) = A
[PROOF STEP]
have le: \<open>?f ?i \<le> a\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a})) \<le> a
[PROOF STEP]
using Least_le[of \<open>\<lambda> a. a \<in> A \<and> card (A \<inter>{..<a}) = ?i\<close> \<open>a\<close>] ina
[PROOF STATE]
proof (prove)
using this:
a \<in> A \<and> card (A \<inter> {..<a}) = card (A \<inter> {..<a}) \<Longrightarrow> (LEAST x. x \<in> A \<and> card (A \<inter> {..<x}) = card (A \<inter> {..<a})) \<le> a
a \<in> A

goal (1 subgoal):
 1. (LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a})) \<le> a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a})) \<le> a

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> range (\<lambda>i. LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i) = A
[PROOF STEP]
have \<open>a = ?f ?i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = (LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a}))
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<noteq> (LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a})) \<Longrightarrow> False
[PROOF STEP]
have fin: \<open>finite (A \<inter> {..<a})\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (A \<inter> {..<a})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (A \<inter> {..<a})

goal (1 subgoal):
 1. a \<noteq> (LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a})) \<Longrightarrow> False
[PROOF STEP]
assume \<open>a \<noteq> ?f ?i\<close>
[PROOF STATE]
proof (state)
this:
a \<noteq> (LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a}))

goal (1 subgoal):
 1. a \<noteq> (LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a})) \<Longrightarrow> False
[PROOF STEP]
hence \<open>?f ?i < a\<close>
[PROOF STATE]
proof (prove)
using this:
a \<noteq> (LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a}))

goal (1 subgoal):
 1. (LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a})) < a
[PROOF STEP]
using le
[PROOF STATE]
proof (prove)
using this:
a \<noteq> (LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a}))
(LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a})) \<le> a

goal (1 subgoal):
 1. (LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a})) < a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a})) < a

goal (1 subgoal):
 1. a \<noteq> (LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a})) \<Longrightarrow> False
[PROOF STEP]
hence \<open>?f ?i \<in> A \<inter> {..<a}\<close>
[PROOF STATE]
proof (prove)
using this:
(LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a})) < a

goal (1 subgoal):
 1. (LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a})) \<in> A \<inter> {..<a}
[PROOF STEP]
using inab
[PROOF STATE]
proof (prove)
using this:
(LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a})) < a
(LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a})) \<in> A

goal (1 subgoal):
 1. (LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a})) \<in> A \<inter> {..<a}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a})) \<in> A \<inter> {..<a}

goal (1 subgoal):
 1. a \<noteq> (LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a})) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a})) \<in> A \<inter> {..<a}

goal (1 subgoal):
 1. a \<noteq> (LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a})) \<Longrightarrow> False
[PROOF STEP]
have \<open>A \<inter> {..<?f ?i} \<subseteq> A \<inter> {..<a}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<inter> {..<LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a})} \<subseteq> A \<inter> {..<a}
[PROOF STEP]
using le
[PROOF STATE]
proof (prove)
using this:
(LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a})) \<le> a

goal (1 subgoal):
 1. A \<inter> {..<LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a})} \<subseteq> A \<inter> {..<a}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<inter> {..<LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a})} \<subseteq> A \<inter> {..<a}

goal (1 subgoal):
 1. a \<noteq> (LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a})) \<Longrightarrow> False
[PROOF STEP]
hence \<open>A \<inter> {..<?f ?i} = A \<inter> {..<a}\<close>
[PROOF STATE]
proof (prove)
using this:
A \<inter> {..<LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a})} \<subseteq> A \<inter> {..<a}

goal (1 subgoal):
 1. A \<inter> {..<LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a})} = A \<inter> {..<a}
[PROOF STEP]
using cardb card_subset_eq[OF fin]
[PROOF STATE]
proof (prove)
using this:
A \<inter> {..<LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a})} \<subseteq> A \<inter> {..<a}
card (A \<inter> {..<LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a})}) = card (A \<inter> {..<a})
\<lbrakk>?A \<subseteq> A \<inter> {..<a}; card ?A = card (A \<inter> {..<a})\<rbrakk> \<Longrightarrow> ?A = A \<inter> {..<a}

goal (1 subgoal):
 1. A \<inter> {..<LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a})} = A \<inter> {..<a}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<inter> {..<LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a})} = A \<inter> {..<a}

goal (1 subgoal):
 1. a \<noteq> (LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a})) \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a})) \<in> A \<inter> {..<a}
A \<inter> {..<LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a})} = A \<inter> {..<a}
[PROOF STEP]
show \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
(LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a})) \<in> A \<inter> {..<a}
A \<inter> {..<LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a})} = A \<inter> {..<a}

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
a = (LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a}))

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> range (\<lambda>i. LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i) = A
[PROOF STEP]
hence \<open>a \<in> range ?f\<close>
[PROOF STATE]
proof (prove)
using this:
a = (LEAST aa. aa \<in> A \<and> card (A \<inter> {..<aa}) = card (A \<inter> {..<a}))

goal (1 subgoal):
 1. a \<in> range (\<lambda>i. LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<in> range (\<lambda>i. LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i)

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> range (\<lambda>i. LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i) = A
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?a2 \<in> A \<Longrightarrow> ?a2 \<in> range (\<lambda>i. LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i)

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> range (\<lambda>i. LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i) = A
[PROOF STEP]
hence \<open>A \<subseteq> range ?f\<close>
[PROOF STATE]
proof (prove)
using this:
?a2 \<in> A \<Longrightarrow> ?a2 \<in> range (\<lambda>i. LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i)

goal (1 subgoal):
 1. A \<subseteq> range (\<lambda>i. LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<subseteq> range (\<lambda>i. LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i)

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>range f = A; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> range (\<lambda>i. LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i) = A
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
range (\<lambda>i. LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i) \<subseteq> A
A \<subseteq> range (\<lambda>i. LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i)
[PROOF STEP]
show \<open>range ?f = A\<close>
[PROOF STATE]
proof (prove)
using this:
range (\<lambda>i. LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i) \<subseteq> A
A \<subseteq> range (\<lambda>i. LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i)

goal (1 subgoal):
 1. range (\<lambda>i. LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i) = A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
range (\<lambda>i. LEAST a. a \<in> A \<and> card (A \<inter> {..<a}) = i) = A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mono_ge_id: \<open>\<forall> i. f i < f (Suc i) \<Longrightarrow> i \<le> f i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. f i < f (Suc i) \<Longrightarrow> i \<le> f i
[PROOF STEP]
apply (induction \<open>i\<close>,auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>i \<le> f i; \<forall>i. f i < f (Suc i)\<rbrakk> \<Longrightarrow> Suc i \<le> f (Suc i)
[PROOF STEP]
by (metis not_le not_less_eq_eq order_trans)


[STATEMENT]
lemma insort_map_mono: assumes mono: \<open>\<forall> n m. n < m \<longrightarrow> f n < f m\<close> shows \<open>map f (insort n ns) = insort (f n) (map f ns)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map f (insort n ns) = insort (f n) (map f ns)
[PROOF STEP]
apply (induction \<open>ns\<close>)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. map f (insort n []) = insort (f n) (map f [])
 2. \<And>a ns. map f (insort n ns) = insort (f n) (map f ns) \<Longrightarrow> map f (insort n (a # ns)) = insort (f n) (map f (a # ns))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a ns. \<lbrakk>map f (insort n ns) = insort (f n) (map f ns); n \<le> a; \<not> f n \<le> f a\<rbrakk> \<Longrightarrow> f n = f a
 2. \<And>a ns. \<lbrakk>map f (insort n ns) = insort (f n) (map f ns); n \<le> a; \<not> f n \<le> f a\<rbrakk> \<Longrightarrow> f a # map f ns = insort (f n) (map f ns)
 3. \<And>a ns. \<lbrakk>map f (insort n ns) = insort (f n) (map f ns); \<not> n \<le> a; f n \<le> f a\<rbrakk> \<Longrightarrow> f a = f n
 4. \<And>a ns. \<lbrakk>map f (insort n ns) = insort (f n) (map f ns); \<not> n \<le> a; f n \<le> f a\<rbrakk> \<Longrightarrow> insort (f n) (map f ns) = f a # map f ns
[PROOF STEP]
apply (metis not_less not_less_iff_gr_or_eq mono)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a ns. \<lbrakk>map f (insort n ns) = insort (f n) (map f ns); n \<le> a; \<not> f n \<le> f a\<rbrakk> \<Longrightarrow> f a # map f ns = insort (f n) (map f ns)
 2. \<And>a ns. \<lbrakk>map f (insort n ns) = insort (f n) (map f ns); \<not> n \<le> a; f n \<le> f a\<rbrakk> \<Longrightarrow> f a = f n
 3. \<And>a ns. \<lbrakk>map f (insort n ns) = insort (f n) (map f ns); \<not> n \<le> a; f n \<le> f a\<rbrakk> \<Longrightarrow> insort (f n) (map f ns) = f a # map f ns
[PROOF STEP]
apply (metis antisym_conv1 less_imp_le mono)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a ns. \<lbrakk>map f (insort n ns) = insort (f n) (map f ns); \<not> n \<le> a; f n \<le> f a\<rbrakk> \<Longrightarrow> f a = f n
 2. \<And>a ns. \<lbrakk>map f (insort n ns) = insort (f n) (map f ns); \<not> n \<le> a; f n \<le> f a\<rbrakk> \<Longrightarrow> insort (f n) (map f ns) = f a # map f ns
[PROOF STEP]
apply (metis mono not_less)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a ns. \<lbrakk>map f (insort n ns) = insort (f n) (map f ns); \<not> n \<le> a; f n \<le> f a\<rbrakk> \<Longrightarrow> insort (f n) (map f ns) = f a # map f ns
[PROOF STEP]
by (metis mono not_less)


[STATEMENT]
lemma sorted_list_of_set_map_mono: assumes mono: \<open>\<forall> n m. n < m \<longrightarrow> f n < f m\<close> and fin: \<open>finite A\<close>
shows \<open>map f (sorted_list_of_set A) = sorted_list_of_set (f`A)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map f (sorted_list_of_set A) = sorted_list_of_set (f ` A)
[PROOF STEP]
using fin
[PROOF STATE]
proof (prove)
using this:
finite A

goal (1 subgoal):
 1. map f (sorted_list_of_set A) = sorted_list_of_set (f ` A)
[PROOF STEP]
proof (induction)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. map f (sorted_list_of_set {}) = sorted_list_of_set (f ` {})
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; map f (sorted_list_of_set F) = sorted_list_of_set (f ` F)\<rbrakk> \<Longrightarrow> map f (sorted_list_of_set (insert x F)) = sorted_list_of_set (f ` insert x F)
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. map f (sorted_list_of_set {}) = sorted_list_of_set (f ` {})
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; map f (sorted_list_of_set F) = sorted_list_of_set (f ` F)\<rbrakk> \<Longrightarrow> map f (sorted_list_of_set (insert x F)) = sorted_list_of_set (f ` insert x F)
[PROOF STEP]
thus \<open>?case\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map f (sorted_list_of_set {}) = sorted_list_of_set (f ` {})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map f (sorted_list_of_set {}) = sorted_list_of_set (f ` {})

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; map f (sorted_list_of_set F) = sorted_list_of_set (f ` F)\<rbrakk> \<Longrightarrow> map f (sorted_list_of_set (insert x F)) = sorted_list_of_set (f ` insert x F)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; map f (sorted_list_of_set F) = sorted_list_of_set (f ` F)\<rbrakk> \<Longrightarrow> map f (sorted_list_of_set (insert x F)) = sorted_list_of_set (f ` insert x F)
[PROOF STEP]
case (insert x A)
[PROOF STATE]
proof (state)
this:
finite A
x \<notin> A
map f (sorted_list_of_set A) = sorted_list_of_set (f ` A)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; map f (sorted_list_of_set F) = sorted_list_of_set (f ` F)\<rbrakk> \<Longrightarrow> map f (sorted_list_of_set (insert x F)) = sorted_list_of_set (f ` insert x F)
[PROOF STEP]
have [simp]:\<open>sorted_list_of_set (insert x A) = insort x (sorted_list_of_set A)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted_list_of_set (insert x A) = insort x (sorted_list_of_set A)
[PROOF STEP]
using insert sorted_list_of_set_insert
[PROOF STATE]
proof (prove)
using this:
finite A
x \<notin> A
map f (sorted_list_of_set A) = sorted_list_of_set (f ` A)
\<lbrakk>finite ?A; ?x \<notin> ?A\<rbrakk> \<Longrightarrow> sorted_list_of_set (insert ?x ?A) = insort ?x (sorted_list_of_set ?A)

goal (1 subgoal):
 1. sorted_list_of_set (insert x A) = insort x (sorted_list_of_set A)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sorted_list_of_set (insert x A) = insort x (sorted_list_of_set A)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; map f (sorted_list_of_set F) = sorted_list_of_set (f ` F)\<rbrakk> \<Longrightarrow> map f (sorted_list_of_set (insert x F)) = sorted_list_of_set (f ` insert x F)
[PROOF STEP]
have \<open>f ` insert x A = insert (f x) (f ` A)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` insert x A = insert (f x) (f ` A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f ` insert x A = insert (f x) (f ` A)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; map f (sorted_list_of_set F) = sorted_list_of_set (f ` F)\<rbrakk> \<Longrightarrow> map f (sorted_list_of_set (insert x F)) = sorted_list_of_set (f ` insert x F)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f ` insert x A = insert (f x) (f ` A)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; map f (sorted_list_of_set F) = sorted_list_of_set (f ` F)\<rbrakk> \<Longrightarrow> map f (sorted_list_of_set (insert x F)) = sorted_list_of_set (f ` insert x F)
[PROOF STEP]
have \<open>f x \<notin> f`A\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f x \<notin> f ` A
[PROOF STEP]
apply (rule ccontr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> f x \<notin> f ` A \<Longrightarrow> False
[PROOF STEP]
using insert(2) mono
[PROOF STATE]
proof (prove)
using this:
x \<notin> A
\<forall>n m. n < m \<longrightarrow> f n < f m

goal (1 subgoal):
 1. \<not> f x \<notin> f ` A \<Longrightarrow> False
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<notin> A; \<forall>n m. n < m \<longrightarrow> f n < f m; f x = f xa; xa \<in> A\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (metis insert.hyps(2) mono neq_iff)
[PROOF STATE]
proof (state)
this:
f x \<notin> f ` A

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; map f (sorted_list_of_set F) = sorted_list_of_set (f ` F)\<rbrakk> \<Longrightarrow> map f (sorted_list_of_set (insert x F)) = sorted_list_of_set (f ` insert x F)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f ` insert x A = insert (f x) (f ` A)
f x \<notin> f ` A
[PROOF STEP]
have \<open>sorted_list_of_set (f ` insert x A) = insort (f x) (sorted_list_of_set (f`A))\<close>
[PROOF STATE]
proof (prove)
using this:
f ` insert x A = insert (f x) (f ` A)
f x \<notin> f ` A

goal (1 subgoal):
 1. sorted_list_of_set (f ` insert x A) = insort (f x) (sorted_list_of_set (f ` A))
[PROOF STEP]
using insert(1) sorted_list_of_set_insert
[PROOF STATE]
proof (prove)
using this:
f ` insert x A = insert (f x) (f ` A)
f x \<notin> f ` A
finite A
\<lbrakk>finite ?A; ?x \<notin> ?A\<rbrakk> \<Longrightarrow> sorted_list_of_set (insert ?x ?A) = insort ?x (sorted_list_of_set ?A)

goal (1 subgoal):
 1. sorted_list_of_set (f ` insert x A) = insort (f x) (sorted_list_of_set (f ` A))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sorted_list_of_set (f ` insert x A) = insort (f x) (sorted_list_of_set (f ` A))

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; map f (sorted_list_of_set F) = sorted_list_of_set (f ` F)\<rbrakk> \<Longrightarrow> map f (sorted_list_of_set (insert x F)) = sorted_list_of_set (f ` insert x F)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sorted_list_of_set (f ` insert x A) = insort (f x) (sorted_list_of_set (f ` A))

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; map f (sorted_list_of_set F) = sorted_list_of_set (f ` F)\<rbrakk> \<Longrightarrow> map f (sorted_list_of_set (insert x F)) = sorted_list_of_set (f ` insert x F)
[PROOF STEP]
have \<open>\<dots> = insort (f x) (map f (sorted_list_of_set A))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insort (f x) (sorted_list_of_set (f ` A)) = insort (f x) (map f (sorted_list_of_set A))
[PROOF STEP]
using insert.IH
[PROOF STATE]
proof (prove)
using this:
map f (sorted_list_of_set A) = sorted_list_of_set (f ` A)

goal (1 subgoal):
 1. insort (f x) (sorted_list_of_set (f ` A)) = insort (f x) (map f (sorted_list_of_set A))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insort (f x) (sorted_list_of_set (f ` A)) = insort (f x) (map f (sorted_list_of_set A))

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; map f (sorted_list_of_set F) = sorted_list_of_set (f ` F)\<rbrakk> \<Longrightarrow> map f (sorted_list_of_set (insert x F)) = sorted_list_of_set (f ` insert x F)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
insort (f x) (sorted_list_of_set (f ` A)) = insort (f x) (map f (sorted_list_of_set A))

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; map f (sorted_list_of_set F) = sorted_list_of_set (f ` F)\<rbrakk> \<Longrightarrow> map f (sorted_list_of_set (insert x F)) = sorted_list_of_set (f ` insert x F)
[PROOF STEP]
have \<open>\<dots> = map f (insort x (sorted_list_of_set A))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insort (f x) (map f (sorted_list_of_set A)) = map f (insort x (sorted_list_of_set A))
[PROOF STEP]
using insort_map_mono[OF mono]
[PROOF STATE]
proof (prove)
using this:
map f (insort ?n ?ns) = insort (f ?n) (map f ?ns)

goal (1 subgoal):
 1. insort (f x) (map f (sorted_list_of_set A)) = map f (insort x (sorted_list_of_set A))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insort (f x) (map f (sorted_list_of_set A)) = map f (insort x (sorted_list_of_set A))

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; map f (sorted_list_of_set F) = sorted_list_of_set (f ` F)\<rbrakk> \<Longrightarrow> map f (sorted_list_of_set (insert x F)) = sorted_list_of_set (f ` insert x F)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sorted_list_of_set (f ` insert x A) = map f (insort x (sorted_list_of_set A))
[PROOF STEP]
show \<open>map f (sorted_list_of_set (insert x A)) = sorted_list_of_set (f ` insert x A)\<close>
[PROOF STATE]
proof (prove)
using this:
sorted_list_of_set (f ` insert x A) = map f (insort x (sorted_list_of_set A))

goal (1 subgoal):
 1. map f (sorted_list_of_set (insert x A)) = sorted_list_of_set (f ` insert x A)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map f (sorted_list_of_set (insert x A)) = sorted_list_of_set (f ` insert x A)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma GreatestIB:
fixes n :: \<open>nat\<close> and P
assumes a:\<open>\<exists>k\<le>n. P k\<close>
shows GreatestBI: \<open>P (GREATEST k. k\<le>n \<and> P k)\<close> and GreatestB: \<open>(GREATEST k. k\<le>n \<and> P k) \<le> n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (GREATEST k. k \<le> n \<and> P k) &&& (GREATEST k. k \<le> n \<and> P k) \<le> n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P (GREATEST k. k \<le> n \<and> P k)
 2. (GREATEST k. k \<le> n \<and> P k) \<le> n
[PROOF STEP]
show \<open>P (GREATEST k. k\<le>n \<and> P k)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (GREATEST k. k \<le> n \<and> P k)
[PROOF STEP]
using GreatestI_ex_nat[OF assms]
[PROOF STATE]
proof (prove)
using this:
(\<And>y. y \<le> n \<and> P y \<Longrightarrow> y \<le> ?b) \<Longrightarrow> (GREATEST k. k \<le> n \<and> P k) \<le> n \<and> P (GREATEST k. k \<le> n \<and> P k)

goal (1 subgoal):
 1. P (GREATEST k. k \<le> n \<and> P k)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P (GREATEST k. k \<le> n \<and> P k)

goal (1 subgoal):
 1. (GREATEST k. k \<le> n \<and> P k) \<le> n
[PROOF STEP]
show \<open>(GREATEST k. k\<le>n \<and> P k) \<le> n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (GREATEST k. k \<le> n \<and> P k) \<le> n
[PROOF STEP]
using GreatestI_ex_nat[OF assms]
[PROOF STATE]
proof (prove)
using this:
(\<And>y. y \<le> n \<and> P y \<Longrightarrow> y \<le> ?b) \<Longrightarrow> (GREATEST k. k \<le> n \<and> P k) \<le> n \<and> P (GREATEST k. k \<le> n \<and> P k)

goal (1 subgoal):
 1. (GREATEST k. k \<le> n \<and> P k) \<le> n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(GREATEST k. k \<le> n \<and> P k) \<le> n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma GreatestB_le:
fixes n :: \<open>nat\<close>
assumes \<open>x\<le>n\<close> and \<open>P x\<close>
shows \<open>x \<le> (GREATEST k. k\<le>n \<and> P k)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> (GREATEST k. k \<le> n \<and> P k)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<le> (GREATEST k. k \<le> n \<and> P k)
[PROOF STEP]
have *: \<open>\<forall> y. y\<le>n \<and> P y \<longrightarrow> y<Suc n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>y. y \<le> n \<and> P y \<longrightarrow> y < Suc n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>y. y \<le> n \<and> P y \<longrightarrow> y < Suc n

goal (1 subgoal):
 1. x \<le> (GREATEST k. k \<le> n \<and> P k)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>y. y \<le> n \<and> P y \<longrightarrow> y < Suc n
[PROOF STEP]
show \<open>x \<le> (GREATEST k. k\<le>n \<and> P k)\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>y. y \<le> n \<and> P y \<longrightarrow> y < Suc n

goal (1 subgoal):
 1. x \<le> (GREATEST k. k \<le> n \<and> P k)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>y. y \<le> n \<and> P y \<longrightarrow> y < Suc n
x \<le> n
P x

goal (1 subgoal):
 1. x \<le> (GREATEST k. k \<le> n \<and> P k)
[PROOF STEP]
by (blast intro: Greatest_le_nat)
[PROOF STATE]
proof (state)
this:
x \<le> (GREATEST k. k \<le> n \<and> P k)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma LeastBI_ex: assumes \<open>\<exists>k \<le> n. P k\<close> shows \<open>P (LEAST k::'c::wellorder. P k)\<close> and \<open>(LEAST k. P k) \<le> n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (LEAST k. P k) &&& (LEAST k. P k) \<le> n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P (LEAST k. P k)
 2. (LEAST k. P k) \<le> n
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<exists>k\<le>n. P k
[PROOF STEP]
obtain k where k: "k \<le> n" "P k"
[PROOF STATE]
proof (prove)
using this:
\<exists>k\<le>n. P k

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>k \<le> n; P k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
k \<le> n
P k

goal (2 subgoals):
 1. P (LEAST k. P k)
 2. (LEAST k. P k) \<le> n
[PROOF STEP]
thus \<open>P (LEAST k. P k)\<close>
[PROOF STATE]
proof (prove)
using this:
k \<le> n
P k

goal (1 subgoal):
 1. P (LEAST k. P k)
[PROOF STEP]
using LeastI[of \<open>P\<close> \<open>k\<close>]
[PROOF STATE]
proof (prove)
using this:
k \<le> n
P k
P k \<Longrightarrow> P (LEAST x. P x)

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

goal (1 subgoal):
 1. (LEAST k. P k) \<le> n
[PROOF STEP]
show \<open>(LEAST k. P k) \<le> n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST k. P k) \<le> n
[PROOF STEP]
using Least_le[of \<open>P\<close> \<open>k\<close>] k
[PROOF STATE]
proof (prove)
using this:
P k \<Longrightarrow> (LEAST x. P x) \<le> k
k \<le> n
P k

goal (1 subgoal):
 1. (LEAST k. P k) \<le> n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(LEAST k. P k) \<le> n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma allB_atLeastLessThan_lower:  assumes \<open>(i::nat) \<le> j\<close> \<open>\<forall> x\<in>{i..<n}. P x\<close> shows \<open>\<forall> x\<in>{j..<n}. P x\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>{j..<n}. P x
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {j..<n} \<Longrightarrow> P x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {j..<n} \<Longrightarrow> P x
[PROOF STEP]
assume \<open>x\<in>{j..<n}\<close>
[PROOF STATE]
proof (state)
this:
x \<in> {j..<n}

goal (1 subgoal):
 1. \<And>x. x \<in> {j..<n} \<Longrightarrow> P x
[PROOF STEP]
hence \<open>x\<in>{i..<n}\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> {j..<n}

goal (1 subgoal):
 1. x \<in> {i..<n}
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
x \<in> {j..<n}
i \<le> j

goal (1 subgoal):
 1. x \<in> {i..<n}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<in> {i..<n}

goal (1 subgoal):
 1. \<And>x. x \<in> {j..<n} \<Longrightarrow> P x
[PROOF STEP]
thus \<open>P x\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> {i..<n}

goal (1 subgoal):
 1. P x
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
x \<in> {i..<n}
\<forall>x\<in>{i..<n}. P x

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma path0: \<open>path \<sigma> 0 = entry\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path \<sigma> 0 = local.entry
[PROOF STEP]
unfolding path_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst ((local.step ^^ 0) (local.entry, \<sigma>)) = local.entry
[PROOF STEP]
by auto


[STATEMENT]
lemma path_in_nodes[intro]: \<open>path \<sigma> k \<in> nodes\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path \<sigma> k \<in> local.nodes
[PROOF STEP]
proof (induction \<open>k\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. path \<sigma> 0 \<in> local.nodes
 2. \<And>k. path \<sigma> k \<in> local.nodes \<Longrightarrow> path \<sigma> (Suc k) \<in> local.nodes
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
path \<sigma> k \<in> local.nodes

goal (2 subgoals):
 1. path \<sigma> 0 \<in> local.nodes
 2. \<And>k. path \<sigma> k \<in> local.nodes \<Longrightarrow> path \<sigma> (Suc k) \<in> local.nodes
[PROOF STEP]
hence \<open>\<And> \<sigma>'. (path \<sigma> k, suc (path \<sigma> k) \<sigma>') \<in> edges\<close>
[PROOF STATE]
proof (prove)
using this:
path \<sigma> k \<in> local.nodes

goal (1 subgoal):
 1. \<And>\<sigma>'. (path \<sigma> k, suc (path \<sigma> k) \<sigma>') \<in> local.edges
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(path \<sigma> k, suc (path \<sigma> k) ?\<sigma>'1) \<in> local.edges

goal (2 subgoals):
 1. path \<sigma> 0 \<in> local.nodes
 2. \<And>k. path \<sigma> k \<in> local.nodes \<Longrightarrow> path \<sigma> (Suc k) \<in> local.nodes
[PROOF STEP]
hence \<open>(path \<sigma> k, path \<sigma> (Suc k)) \<in> edges\<close>
[PROOF STATE]
proof (prove)
using this:
(path \<sigma> k, suc (path \<sigma> k) ?\<sigma>'1) \<in> local.edges

goal (1 subgoal):
 1. (path \<sigma> k, path \<sigma> (Suc k)) \<in> local.edges
[PROOF STEP]
unfolding path_def
[PROOF STATE]
proof (prove)
using this:
(fst ((local.step ^^ k) (local.entry, \<sigma>)), suc (fst ((local.step ^^ k) (local.entry, \<sigma>))) ?\<sigma>'1) \<in> local.edges

goal (1 subgoal):
 1. (fst ((local.step ^^ k) (local.entry, \<sigma>)), fst ((local.step ^^ Suc k) (local.entry, \<sigma>))) \<in> local.edges
[PROOF STEP]
by (metis suc_def comp_apply funpow.simps(2) prod.collapse)
[PROOF STATE]
proof (state)
this:
(path \<sigma> k, path \<sigma> (Suc k)) \<in> local.edges

goal (2 subgoals):
 1. path \<sigma> 0 \<in> local.nodes
 2. \<And>k. path \<sigma> k \<in> local.nodes \<Longrightarrow> path \<sigma> (Suc k) \<in> local.nodes
[PROOF STEP]
thus \<open>?case\<close>
[PROOF STATE]
proof (prove)
using this:
(path \<sigma> k, path \<sigma> (Suc k)) \<in> local.edges

goal (1 subgoal):
 1. path \<sigma> (Suc k) \<in> local.nodes
[PROOF STEP]
using edges_nodes
[PROOF STATE]
proof (prove)
using this:
(path \<sigma> k, path \<sigma> (Suc k)) \<in> local.edges
local.edges \<subseteq> local.nodes \<times> local.nodes

goal (1 subgoal):
 1. path \<sigma> (Suc k) \<in> local.nodes
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
path \<sigma> (Suc k) \<in> local.nodes

goal (1 subgoal):
 1. path \<sigma> 0 \<in> local.nodes
[PROOF STEP]
qed (auto simp add: path_def)


[STATEMENT]
lemma path_is_path[simp]: \<open>is_path (path \<sigma>)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_path (path \<sigma>)
[PROOF STEP]
unfolding is_path_def path_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. (fst ((local.step ^^ n) (local.entry, \<sigma>)), fst ((local.step ^^ Suc n) (local.entry, \<sigma>))) \<in> local.edges
[PROOF STEP]
using step_suc_sem
[PROOF STATE]
proof (prove)
using this:
local.step (?n, ?\<sigma>) = (suc ?n ?\<sigma>, sem ?n ?\<sigma>)

goal (1 subgoal):
 1. \<forall>n. (fst ((local.step ^^ n) (local.entry, \<sigma>)), fst ((local.step ^^ Suc n) (local.entry, \<sigma>))) \<in> local.edges
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. (\<And>n \<sigma>. local.step (n, \<sigma>) = (suc n \<sigma>, sem n \<sigma>)) \<Longrightarrow> (fst ((local.step ^^ n) (local.entry, \<sigma>)), fst (local.step ((local.step ^^ n) (local.entry, \<sigma>)))) \<in> local.edges
[PROOF STEP]
by (metis path_def suc_def edges_complete path_in_nodes prod.collapse)


[STATEMENT]
lemma term_path_stable: assumes \<open>is_path \<pi>\<close> \<open>\<pi> i = return\<close> and le: \<open>i \<le> j\<close> shows \<open>\<pi> j = return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> j = local.return
[PROOF STEP]
using le
[PROOF STATE]
proof (prove)
using this:
i \<le> j

goal (1 subgoal):
 1. \<pi> j = local.return
[PROOF STEP]
proof (induction \<open>j\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i \<le> 0 \<Longrightarrow> \<pi> 0 = local.return
 2. \<And>j. \<lbrakk>i \<le> j \<Longrightarrow> \<pi> j = local.return; i \<le> Suc j\<rbrakk> \<Longrightarrow> \<pi> (Suc j) = local.return
[PROOF STEP]
case (Suc j)
[PROOF STATE]
proof (state)
this:
i \<le> j \<Longrightarrow> \<pi> j = local.return
i \<le> Suc j

goal (2 subgoals):
 1. i \<le> 0 \<Longrightarrow> \<pi> 0 = local.return
 2. \<And>j. \<lbrakk>i \<le> j \<Longrightarrow> \<pi> j = local.return; i \<le> Suc j\<rbrakk> \<Longrightarrow> \<pi> (Suc j) = local.return
[PROOF STEP]
show \<open>?case\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> (Suc j) = local.return
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> \<pi> (Suc j) = local.return
 2. \<not> ?P \<Longrightarrow> \<pi> (Suc j) = local.return
[PROOF STEP]
assume \<open>i\<le>j\<close>
[PROOF STATE]
proof (state)
this:
i \<le> j

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<pi> (Suc j) = local.return
 2. \<not> ?P \<Longrightarrow> \<pi> (Suc j) = local.return
[PROOF STEP]
hence \<open>\<pi> j = return\<close>
[PROOF STATE]
proof (prove)
using this:
i \<le> j

goal (1 subgoal):
 1. \<pi> j = local.return
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
i \<le> j
i \<le> j \<Longrightarrow> \<pi> j = local.return
i \<le> Suc j

goal (1 subgoal):
 1. \<pi> j = local.return
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<pi> j = local.return

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<pi> (Suc j) = local.return
 2. \<not> ?P \<Longrightarrow> \<pi> (Suc j) = local.return
[PROOF STEP]
hence \<open>(return, \<pi> (Suc j)) \<in> edges\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi> j = local.return

goal (1 subgoal):
 1. (local.return, \<pi> (Suc j)) \<in> local.edges
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
\<pi> j = local.return
is_path \<pi>

goal (1 subgoal):
 1. (local.return, \<pi> (Suc j)) \<in> local.edges
[PROOF STEP]
unfolding is_path_def
[PROOF STATE]
proof (prove)
using this:
\<pi> j = local.return
\<forall>n. (\<pi> n, \<pi> (Suc n)) \<in> local.edges

goal (1 subgoal):
 1. (local.return, \<pi> (Suc j)) \<in> local.edges
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(local.return, \<pi> (Suc j)) \<in> local.edges

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<pi> (Suc j) = local.return
 2. \<not> ?P \<Longrightarrow> \<pi> (Suc j) = local.return
[PROOF STEP]
thus \<open>\<pi> (Suc j) = return\<close>
[PROOF STATE]
proof (prove)
using this:
(local.return, \<pi> (Suc j)) \<in> local.edges

goal (1 subgoal):
 1. \<pi> (Suc j) = local.return
[PROOF STEP]
using edges_return
[PROOF STATE]
proof (prove)
using this:
(local.return, \<pi> (Suc j)) \<in> local.edges
(local.return, ?x) \<in> local.edges \<Longrightarrow> ?x = local.return

goal (1 subgoal):
 1. \<pi> (Suc j) = local.return
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi> (Suc j) = local.return

goal (1 subgoal):
 1. \<not> i \<le> j \<Longrightarrow> \<pi> (Suc j) = local.return
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> i \<le> j \<Longrightarrow> \<pi> (Suc j) = local.return
[PROOF STEP]
assume \<open>\<not> i \<le> j\<close>
[PROOF STATE]
proof (state)
this:
\<not> i \<le> j

goal (1 subgoal):
 1. \<not> i \<le> j \<Longrightarrow> \<pi> (Suc j) = local.return
[PROOF STEP]
hence \<open>Suc j = i\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> i \<le> j

goal (1 subgoal):
 1. Suc j = i
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
\<not> i \<le> j
i \<le> j \<Longrightarrow> \<pi> j = local.return
i \<le> Suc j

goal (1 subgoal):
 1. Suc j = i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc j = i

goal (1 subgoal):
 1. \<not> i \<le> j \<Longrightarrow> \<pi> (Suc j) = local.return
[PROOF STEP]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
Suc j = i

goal (1 subgoal):
 1. \<pi> (Suc j) = local.return
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
Suc j = i
\<pi> i = local.return

goal (1 subgoal):
 1. \<pi> (Suc j) = local.return
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi> (Suc j) = local.return

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<pi> (Suc j) = local.return

goal (1 subgoal):
 1. i \<le> 0 \<Longrightarrow> \<pi> 0 = local.return
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<le> 0 \<Longrightarrow> \<pi> 0 = local.return
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
i \<le> 0

goal (1 subgoal):
 1. i \<le> 0 \<Longrightarrow> \<pi> 0 = local.return
[PROOF STEP]
thus \<open>?case\<close>
[PROOF STATE]
proof (prove)
using this:
i \<le> 0

goal (1 subgoal):
 1. \<pi> 0 = local.return
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i \<le> 0
is_path \<pi>
\<pi> i = local.return
i \<le> j

goal (1 subgoal):
 1. \<pi> 0 = local.return
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<pi> 0 = local.return

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma path_path_shift: assumes \<open>is_path \<pi>\<close> shows \<open>is_path (\<pi>\<guillemotleft>m)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_path (\<pi> \<guillemotleft> m)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>

goal (1 subgoal):
 1. is_path (\<pi> \<guillemotleft> m)
[PROOF STEP]
unfolding is_path_def
[PROOF STATE]
proof (prove)
using this:
\<forall>n. (\<pi> n, \<pi> (Suc n)) \<in> local.edges

goal (1 subgoal):
 1. \<forall>n. ((\<pi> \<guillemotleft> m) n, (\<pi> \<guillemotleft> m) (Suc n)) \<in> local.edges
[PROOF STEP]
by simp