[STATEMENT]
lemma weak_action_modality_not_tau:
    assumes "\<alpha> \<noteq> \<tau>"
    shows "(\<langle>\<langle>\<alpha>\<rangle>\<rangle>x) = weak_tau_modality (Act \<alpha> (weak_tau_modality x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>\<langle>\<alpha>\<rangle>\<rangle>x = weak_tau_modality (Act \<alpha> (weak_tau_modality x))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<alpha> \<noteq> \<tau>

goal (1 subgoal):
 1. \<langle>\<langle>\<alpha>\<rangle>\<rangle>x = weak_tau_modality (Act \<alpha> (weak_tau_modality x))
[PROOF STEP]
unfolding weak_action_modality_def
[PROOF STATE]
proof (prove)
using this:
\<alpha> \<noteq> \<tau>

goal (1 subgoal):
 1. (if \<alpha> = \<tau> then weak_tau_modality x else weak_tau_modality (Act \<alpha> (weak_tau_modality x))) = weak_tau_modality (Act \<alpha> (weak_tau_modality x))
[PROOF STEP]
by simp


[STATEMENT]
lemma weak_action_modality_eq:
    assumes "Act \<alpha>1 x1 = Act \<alpha>2 x2"
    shows "(\<langle>\<langle>\<alpha>1\<rangle>\<rangle>x1) = (\<langle>\<langle>\<alpha>2\<rangle>\<rangle>x2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>\<langle>\<alpha>1\<rangle>\<rangle>x1 = \<langle>\<langle>\<alpha>2\<rangle>\<rangle>x2
[PROOF STEP]
proof (cases "\<alpha>1 = \<tau>")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<alpha>1 = \<tau> \<Longrightarrow> \<langle>\<langle>\<alpha>1\<rangle>\<rangle>x1 = \<langle>\<langle>\<alpha>2\<rangle>\<rangle>x2
 2. \<alpha>1 \<noteq> \<tau> \<Longrightarrow> \<langle>\<langle>\<alpha>1\<rangle>\<rangle>x1 = \<langle>\<langle>\<alpha>2\<rangle>\<rangle>x2
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<alpha>1 = \<tau>

goal (2 subgoals):
 1. \<alpha>1 = \<tau> \<Longrightarrow> \<langle>\<langle>\<alpha>1\<rangle>\<rangle>x1 = \<langle>\<langle>\<alpha>2\<rangle>\<rangle>x2
 2. \<alpha>1 \<noteq> \<tau> \<Longrightarrow> \<langle>\<langle>\<alpha>1\<rangle>\<rangle>x1 = \<langle>\<langle>\<alpha>2\<rangle>\<rangle>x2
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
Act \<alpha>1 x1 = Act \<alpha>2 x2
\<alpha>1 = \<tau>
[PROOF STEP]
have "\<alpha>2 = \<alpha>1 \<and> x2 = x1"
[PROOF STATE]
proof (prove)
using this:
Act \<alpha>1 x1 = Act \<alpha>2 x2
\<alpha>1 = \<tau>

goal (1 subgoal):
 1. \<alpha>2 = \<alpha>1 \<and> x2 = x1
[PROOF STEP]
by (metis Act_tau_eq_iff)
[PROOF STATE]
proof (state)
this:
\<alpha>2 = \<alpha>1 \<and> x2 = x1

goal (2 subgoals):
 1. \<alpha>1 = \<tau> \<Longrightarrow> \<langle>\<langle>\<alpha>1\<rangle>\<rangle>x1 = \<langle>\<langle>\<alpha>2\<rangle>\<rangle>x2
 2. \<alpha>1 \<noteq> \<tau> \<Longrightarrow> \<langle>\<langle>\<alpha>1\<rangle>\<rangle>x1 = \<langle>\<langle>\<alpha>2\<rangle>\<rangle>x2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<alpha>2 = \<alpha>1 \<and> x2 = x1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<alpha>2 = \<alpha>1 \<and> x2 = x1

goal (1 subgoal):
 1. \<langle>\<langle>\<alpha>1\<rangle>\<rangle>x1 = \<langle>\<langle>\<alpha>2\<rangle>\<rangle>x2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<langle>\<langle>\<alpha>1\<rangle>\<rangle>x1 = \<langle>\<langle>\<alpha>2\<rangle>\<rangle>x2

goal (1 subgoal):
 1. \<alpha>1 \<noteq> \<tau> \<Longrightarrow> \<langle>\<langle>\<alpha>1\<rangle>\<rangle>x1 = \<langle>\<langle>\<alpha>2\<rangle>\<rangle>x2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<alpha>1 \<noteq> \<tau> \<Longrightarrow> \<langle>\<langle>\<alpha>1\<rangle>\<rangle>x1 = \<langle>\<langle>\<alpha>2\<rangle>\<rangle>x2
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<alpha>1 \<noteq> \<tau>

goal (1 subgoal):
 1. \<alpha>1 \<noteq> \<tau> \<Longrightarrow> \<langle>\<langle>\<alpha>1\<rangle>\<rangle>x1 = \<langle>\<langle>\<alpha>2\<rangle>\<rangle>x2
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Act \<alpha>1 x1 = Act \<alpha>2 x2
[PROOF STEP]
obtain p where 1: "supp x1 - bn \<alpha>1 = supp x2 - bn \<alpha>2" and 2: "(supp x1 - bn \<alpha>1) \<sharp>* p"
      and 3: "p \<bullet> x1 = x2" and 4: "supp \<alpha>1 - bn \<alpha>1 = supp \<alpha>2 - bn \<alpha>2" and 5: "(supp \<alpha>1 - bn \<alpha>1) \<sharp>* p"
      and 6: "p \<bullet> \<alpha>1 = \<alpha>2"
[PROOF STATE]
proof (prove)
using this:
Act \<alpha>1 x1 = Act \<alpha>2 x2

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>supp x1 - bn \<alpha>1 = supp x2 - bn \<alpha>2; (supp x1 - bn \<alpha>1) \<sharp>* p; p \<bullet> x1 = x2; supp \<alpha>1 - bn \<alpha>1 = supp \<alpha>2 - bn \<alpha>2; (supp \<alpha>1 - bn \<alpha>1) \<sharp>* p; p \<bullet> \<alpha>1 = \<alpha>2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis Act_eq_iff_perm)
[PROOF STATE]
proof (state)
this:
supp x1 - bn \<alpha>1 = supp x2 - bn \<alpha>2
(supp x1 - bn \<alpha>1) \<sharp>* p
p \<bullet> x1 = x2
supp \<alpha>1 - bn \<alpha>1 = supp \<alpha>2 - bn \<alpha>2
(supp \<alpha>1 - bn \<alpha>1) \<sharp>* p
p \<bullet> \<alpha>1 = \<alpha>2

goal (1 subgoal):
 1. \<alpha>1 \<noteq> \<tau> \<Longrightarrow> \<langle>\<langle>\<alpha>1\<rangle>\<rangle>x1 = \<langle>\<langle>\<alpha>2\<rangle>\<rangle>x2
[PROOF STEP]
from 1
[PROOF STATE]
proof (chain)
picking this:
supp x1 - bn \<alpha>1 = supp x2 - bn \<alpha>2
[PROOF STEP]
have "supp (weak_tau_modality x1) - bn \<alpha>1 = supp (weak_tau_modality x2) - bn \<alpha>2"
[PROOF STATE]
proof (prove)
using this:
supp x1 - bn \<alpha>1 = supp x2 - bn \<alpha>2

goal (1 subgoal):
 1. supp (weak_tau_modality x1) - bn \<alpha>1 = supp (weak_tau_modality x2) - bn \<alpha>2
[PROOF STEP]
by (metis supp_weak_tau_modality)
[PROOF STATE]
proof (state)
this:
supp (weak_tau_modality x1) - bn \<alpha>1 = supp (weak_tau_modality x2) - bn \<alpha>2

goal (1 subgoal):
 1. \<alpha>1 \<noteq> \<tau> \<Longrightarrow> \<langle>\<langle>\<alpha>1\<rangle>\<rangle>x1 = \<langle>\<langle>\<alpha>2\<rangle>\<rangle>x2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
supp (weak_tau_modality x1) - bn \<alpha>1 = supp (weak_tau_modality x2) - bn \<alpha>2

goal (1 subgoal):
 1. \<alpha>1 \<noteq> \<tau> \<Longrightarrow> \<langle>\<langle>\<alpha>1\<rangle>\<rangle>x1 = \<langle>\<langle>\<alpha>2\<rangle>\<rangle>x2
[PROOF STEP]
from 2
[PROOF STATE]
proof (chain)
picking this:
(supp x1 - bn \<alpha>1) \<sharp>* p
[PROOF STEP]
have "(supp (weak_tau_modality x1) - bn \<alpha>1) \<sharp>* p"
[PROOF STATE]
proof (prove)
using this:
(supp x1 - bn \<alpha>1) \<sharp>* p

goal (1 subgoal):
 1. (supp (weak_tau_modality x1) - bn \<alpha>1) \<sharp>* p
[PROOF STEP]
by (metis supp_weak_tau_modality)
[PROOF STATE]
proof (state)
this:
(supp (weak_tau_modality x1) - bn \<alpha>1) \<sharp>* p

goal (1 subgoal):
 1. \<alpha>1 \<noteq> \<tau> \<Longrightarrow> \<langle>\<langle>\<alpha>1\<rangle>\<rangle>x1 = \<langle>\<langle>\<alpha>2\<rangle>\<rangle>x2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(supp (weak_tau_modality x1) - bn \<alpha>1) \<sharp>* p

goal (1 subgoal):
 1. \<alpha>1 \<noteq> \<tau> \<Longrightarrow> \<langle>\<langle>\<alpha>1\<rangle>\<rangle>x1 = \<langle>\<langle>\<alpha>2\<rangle>\<rangle>x2
[PROOF STEP]
from 3
[PROOF STATE]
proof (chain)
picking this:
p \<bullet> x1 = x2
[PROOF STEP]
have "p \<bullet> weak_tau_modality x1 = weak_tau_modality x2"
[PROOF STATE]
proof (prove)
using this:
p \<bullet> x1 = x2

goal (1 subgoal):
 1. p \<bullet> weak_tau_modality x1 = weak_tau_modality x2
[PROOF STEP]
by (metis weak_tau_modality_eqvt)
[PROOF STATE]
proof (state)
this:
p \<bullet> weak_tau_modality x1 = weak_tau_modality x2

goal (1 subgoal):
 1. \<alpha>1 \<noteq> \<tau> \<Longrightarrow> \<langle>\<langle>\<alpha>1\<rangle>\<rangle>x1 = \<langle>\<langle>\<alpha>2\<rangle>\<rangle>x2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
supp (weak_tau_modality x1) - bn \<alpha>1 = supp (weak_tau_modality x2) - bn \<alpha>2
(supp (weak_tau_modality x1) - bn \<alpha>1) \<sharp>* p
p \<bullet> weak_tau_modality x1 = weak_tau_modality x2
[PROOF STEP]
have "Act \<alpha>1 (weak_tau_modality x1) = Act \<alpha>2 (weak_tau_modality x2)"
[PROOF STATE]
proof (prove)
using this:
supp (weak_tau_modality x1) - bn \<alpha>1 = supp (weak_tau_modality x2) - bn \<alpha>2
(supp (weak_tau_modality x1) - bn \<alpha>1) \<sharp>* p
p \<bullet> weak_tau_modality x1 = weak_tau_modality x2

goal (1 subgoal):
 1. Act \<alpha>1 (weak_tau_modality x1) = Act \<alpha>2 (weak_tau_modality x2)
[PROOF STEP]
using 4 and 5 and 6 and Act_eq_iff_perm
[PROOF STATE]
proof (prove)
using this:
supp (weak_tau_modality x1) - bn \<alpha>1 = supp (weak_tau_modality x2) - bn \<alpha>2
(supp (weak_tau_modality x1) - bn \<alpha>1) \<sharp>* p
p \<bullet> weak_tau_modality x1 = weak_tau_modality x2
supp \<alpha>1 - bn \<alpha>1 = supp \<alpha>2 - bn \<alpha>2
(supp \<alpha>1 - bn \<alpha>1) \<sharp>* p
p \<bullet> \<alpha>1 = \<alpha>2
(Act ?\<alpha>1.0 ?x1.0 = Act ?\<alpha>2.0 ?x2.0) = (\<exists>p. supp ?x1.0 - bn ?\<alpha>1.0 = supp ?x2.0 - bn ?\<alpha>2.0 \<and> (supp ?x1.0 - bn ?\<alpha>1.0) \<sharp>* p \<and> p \<bullet> ?x1.0 = ?x2.0 \<and> supp ?\<alpha>1.0 - bn ?\<alpha>1.0 = supp ?\<alpha>2.0 - bn ?\<alpha>2.0 \<and> (supp ?\<alpha>1.0 - bn ?\<alpha>1.0) \<sharp>* p \<and> p \<bullet> ?\<alpha>1.0 = ?\<alpha>2.0)

goal (1 subgoal):
 1. Act \<alpha>1 (weak_tau_modality x1) = Act \<alpha>2 (weak_tau_modality x2)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Act \<alpha>1 (weak_tau_modality x1) = Act \<alpha>2 (weak_tau_modality x2)

goal (1 subgoal):
 1. \<alpha>1 \<noteq> \<tau> \<Longrightarrow> \<langle>\<langle>\<alpha>1\<rangle>\<rangle>x1 = \<langle>\<langle>\<alpha>2\<rangle>\<rangle>x2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Act \<alpha>1 (weak_tau_modality x1) = Act \<alpha>2 (weak_tau_modality x2)

goal (1 subgoal):
 1. \<alpha>1 \<noteq> \<tau> \<Longrightarrow> \<langle>\<langle>\<alpha>1\<rangle>\<rangle>x1 = \<langle>\<langle>\<alpha>2\<rangle>\<rangle>x2
[PROOF STEP]
from \<open>\<alpha>1 \<noteq> \<tau>\<close> and assms
[PROOF STATE]
proof (chain)
picking this:
\<alpha>1 \<noteq> \<tau>
Act \<alpha>1 x1 = Act \<alpha>2 x2
[PROOF STEP]
have "\<alpha>2 \<noteq> \<tau>"
[PROOF STATE]
proof (prove)
using this:
\<alpha>1 \<noteq> \<tau>
Act \<alpha>1 x1 = Act \<alpha>2 x2

goal (1 subgoal):
 1. \<alpha>2 \<noteq> \<tau>
[PROOF STEP]
by (metis Act_tau_eq_iff)
[PROOF STATE]
proof (state)
this:
\<alpha>2 \<noteq> \<tau>

goal (1 subgoal):
 1. \<alpha>1 \<noteq> \<tau> \<Longrightarrow> \<langle>\<langle>\<alpha>1\<rangle>\<rangle>x1 = \<langle>\<langle>\<alpha>2\<rangle>\<rangle>x2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Act \<alpha>1 (weak_tau_modality x1) = Act \<alpha>2 (weak_tau_modality x2)
\<alpha>2 \<noteq> \<tau>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Act \<alpha>1 (weak_tau_modality x1) = Act \<alpha>2 (weak_tau_modality x2)
\<alpha>2 \<noteq> \<tau>

goal (1 subgoal):
 1. \<langle>\<langle>\<alpha>1\<rangle>\<rangle>x1 = \<langle>\<langle>\<alpha>2\<rangle>\<rangle>x2
[PROOF STEP]
using \<open>\<alpha>1 \<noteq> \<tau>\<close>
[PROOF STATE]
proof (prove)
using this:
Act \<alpha>1 (weak_tau_modality x1) = Act \<alpha>2 (weak_tau_modality x2)
\<alpha>2 \<noteq> \<tau>
\<alpha>1 \<noteq> \<tau>

goal (1 subgoal):
 1. \<langle>\<langle>\<alpha>1\<rangle>\<rangle>x1 = \<langle>\<langle>\<alpha>2\<rangle>\<rangle>x2
[PROOF STEP]
by (simp add: weak_action_modality_not_tau)
[PROOF STATE]
proof (state)
this:
\<langle>\<langle>\<alpha>1\<rangle>\<rangle>x1 = \<langle>\<langle>\<alpha>2\<rangle>\<rangle>x2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finite_supp_wf_Pred [simp]: "finite (supp (binsert (Pred \<phi>) (bsingleton x)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (supp (binsert (Pred \<phi>) (bsingleton x)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite (supp (binsert (Pred \<phi>) (bsingleton x)))
[PROOF STEP]
have "supp (bsingleton x) \<subseteq> supp x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. supp (bsingleton x) \<subseteq> supp x
[PROOF STEP]
by (simp add: eqvtI supp_fun_app_eqvt)
[PROOF STATE]
proof (state)
this:
supp (bsingleton x) \<subseteq> supp x

goal (1 subgoal):
 1. finite (supp (binsert (Pred \<phi>) (bsingleton x)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
supp (bsingleton x) \<subseteq> supp x

goal (1 subgoal):
 1. finite (supp (binsert (Pred \<phi>) (bsingleton x)))
[PROOF STEP]
have "eqvt binsert"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqvt binsert
[PROOF STEP]
by (simp add: eqvtI)
[PROOF STATE]
proof (state)
this:
eqvt binsert

goal (1 subgoal):
 1. finite (supp (binsert (Pred \<phi>) (bsingleton x)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
supp (bsingleton x) \<subseteq> supp x
eqvt binsert
[PROOF STEP]
have "supp (binsert (Pred \<phi>) (bsingleton x)) \<subseteq> supp \<phi> \<union> supp x"
[PROOF STATE]
proof (prove)
using this:
supp (bsingleton x) \<subseteq> supp x
eqvt binsert

goal (1 subgoal):
 1. supp (binsert (Pred \<phi>) (bsingleton x)) \<subseteq> supp \<phi> \<union> supp x
[PROOF STEP]
using supp_fun_app supp_fun_app_eqvt
[PROOF STATE]
proof (prove)
using this:
supp (bsingleton x) \<subseteq> supp x
eqvt binsert
supp (?f ?x) \<subseteq> supp ?f \<union> supp ?x
eqvt ?f \<Longrightarrow> supp (?f ?x) \<subseteq> supp ?x

goal (1 subgoal):
 1. supp (binsert (Pred \<phi>) (bsingleton x)) \<subseteq> supp \<phi> \<union> supp x
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
supp (binsert (Pred \<phi>) (bsingleton x)) \<subseteq> supp \<phi> \<union> supp x

goal (1 subgoal):
 1. finite (supp (binsert (Pred \<phi>) (bsingleton x)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
supp (binsert (Pred \<phi>) (bsingleton x)) \<subseteq> supp \<phi> \<union> supp x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
supp (binsert (Pred \<phi>) (bsingleton x)) \<subseteq> supp \<phi> \<union> supp x

goal (1 subgoal):
 1. finite (supp (binsert (Pred \<phi>) (bsingleton x)))
[PROOF STEP]
by (metis finite_UnI finite_supp rev_finite_subset)
[PROOF STATE]
proof (state)
this:
finite (supp (binsert (Pred \<phi>) (bsingleton x)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weak_formula_eqvt (*[eqvt]*) [simp]: "weak_formula x \<Longrightarrow> weak_formula (p \<bullet> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weak_formula x \<Longrightarrow> weak_formula (p \<bullet> x)
[PROOF STEP]
proof (induct rule: weak_formula.induct)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>xset. \<lbrakk>finite (supp xset); \<And>x. x \<in> set_bset xset \<Longrightarrow> weak_formula x; \<And>x. x \<in> set_bset xset \<Longrightarrow> weak_formula (p \<bullet> x)\<rbrakk> \<Longrightarrow> weak_formula (p \<bullet> Conj xset)
 2. \<And>x. \<lbrakk>weak_formula x; weak_formula (p \<bullet> x)\<rbrakk> \<Longrightarrow> weak_formula (p \<bullet> Formula.Not x)
 3. \<And>x \<alpha>. \<lbrakk>weak_formula x; weak_formula (p \<bullet> x)\<rbrakk> \<Longrightarrow> weak_formula (p \<bullet> \<langle>\<langle>\<alpha>\<rangle>\<rangle>x)
 4. \<And>x \<phi>. \<lbrakk>weak_formula x; weak_formula (p \<bullet> x)\<rbrakk> \<Longrightarrow> weak_formula (p \<bullet> \<langle>\<langle>\<tau>\<rangle>\<rangle>Conj (binsert (Pred \<phi>) (bsingleton x)))
[PROOF STEP]
case (wf_Conj xset)
[PROOF STATE]
proof (state)
this:
finite (supp xset)
?x7 \<in> set_bset xset \<Longrightarrow> weak_formula ?x7
?x7 \<in> set_bset xset \<Longrightarrow> weak_formula (p \<bullet> ?x7)

goal (4 subgoals):
 1. \<And>xset. \<lbrakk>finite (supp xset); \<And>x. x \<in> set_bset xset \<Longrightarrow> weak_formula x; \<And>x. x \<in> set_bset xset \<Longrightarrow> weak_formula (p \<bullet> x)\<rbrakk> \<Longrightarrow> weak_formula (p \<bullet> Conj xset)
 2. \<And>x. \<lbrakk>weak_formula x; weak_formula (p \<bullet> x)\<rbrakk> \<Longrightarrow> weak_formula (p \<bullet> Formula.Not x)
 3. \<And>x \<alpha>. \<lbrakk>weak_formula x; weak_formula (p \<bullet> x)\<rbrakk> \<Longrightarrow> weak_formula (p \<bullet> \<langle>\<langle>\<alpha>\<rangle>\<rangle>x)
 4. \<And>x \<phi>. \<lbrakk>weak_formula x; weak_formula (p \<bullet> x)\<rbrakk> \<Longrightarrow> weak_formula (p \<bullet> \<langle>\<langle>\<tau>\<rangle>\<rangle>Conj (binsert (Pred \<phi>) (bsingleton x)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite (supp xset)
?x7 \<in> set_bset xset \<Longrightarrow> weak_formula ?x7
?x7 \<in> set_bset xset \<Longrightarrow> weak_formula (p \<bullet> ?x7)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
finite (supp xset)
?x7 \<in> set_bset xset \<Longrightarrow> weak_formula ?x7
?x7 \<in> set_bset xset \<Longrightarrow> weak_formula (p \<bullet> ?x7)

goal (1 subgoal):
 1. weak_formula (p \<bullet> Conj xset)
[PROOF STEP]
by simp (metis (no_types, lifting) imageE permute_finite permute_set_eq_image set_bset_eqvt supp_eqvt weak_formula.wf_Conj)
[PROOF STATE]
proof (state)
this:
weak_formula (p \<bullet> Conj xset)

goal (3 subgoals):
 1. \<And>x. \<lbrakk>weak_formula x; weak_formula (p \<bullet> x)\<rbrakk> \<Longrightarrow> weak_formula (p \<bullet> Formula.Not x)
 2. \<And>x \<alpha>. \<lbrakk>weak_formula x; weak_formula (p \<bullet> x)\<rbrakk> \<Longrightarrow> weak_formula (p \<bullet> \<langle>\<langle>\<alpha>\<rangle>\<rangle>x)
 3. \<And>x \<phi>. \<lbrakk>weak_formula x; weak_formula (p \<bullet> x)\<rbrakk> \<Longrightarrow> weak_formula (p \<bullet> \<langle>\<langle>\<tau>\<rangle>\<rangle>Conj (binsert (Pred \<phi>) (bsingleton x)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>weak_formula x; weak_formula (p \<bullet> x)\<rbrakk> \<Longrightarrow> weak_formula (p \<bullet> Formula.Not x)
 2. \<And>x \<alpha>. \<lbrakk>weak_formula x; weak_formula (p \<bullet> x)\<rbrakk> \<Longrightarrow> weak_formula (p \<bullet> \<langle>\<langle>\<alpha>\<rangle>\<rangle>x)
 3. \<And>x \<phi>. \<lbrakk>weak_formula x; weak_formula (p \<bullet> x)\<rbrakk> \<Longrightarrow> weak_formula (p \<bullet> \<langle>\<langle>\<tau>\<rangle>\<rangle>Conj (binsert (Pred \<phi>) (bsingleton x)))
[PROOF STEP]
case (wf_Not x)
[PROOF STATE]
proof (state)
this:
weak_formula x
weak_formula (p \<bullet> x)

goal (3 subgoals):
 1. \<And>x. \<lbrakk>weak_formula x; weak_formula (p \<bullet> x)\<rbrakk> \<Longrightarrow> weak_formula (p \<bullet> Formula.Not x)
 2. \<And>x \<alpha>. \<lbrakk>weak_formula x; weak_formula (p \<bullet> x)\<rbrakk> \<Longrightarrow> weak_formula (p \<bullet> \<langle>\<langle>\<alpha>\<rangle>\<rangle>x)
 3. \<And>x \<phi>. \<lbrakk>weak_formula x; weak_formula (p \<bullet> x)\<rbrakk> \<Longrightarrow> weak_formula (p \<bullet> \<langle>\<langle>\<tau>\<rangle>\<rangle>Conj (binsert (Pred \<phi>) (bsingleton x)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
weak_formula x
weak_formula (p \<bullet> x)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
weak_formula x
weak_formula (p \<bullet> x)

goal (1 subgoal):
 1. weak_formula (p \<bullet> Formula.Not x)
[PROOF STEP]
by (simp add: weak_formula.wf_Not)
[PROOF STATE]
proof (state)
this:
weak_formula (p \<bullet> Formula.Not x)

goal (2 subgoals):
 1. \<And>x \<alpha>. \<lbrakk>weak_formula x; weak_formula (p \<bullet> x)\<rbrakk> \<Longrightarrow> weak_formula (p \<bullet> \<langle>\<langle>\<alpha>\<rangle>\<rangle>x)
 2. \<And>x \<phi>. \<lbrakk>weak_formula x; weak_formula (p \<bullet> x)\<rbrakk> \<Longrightarrow> weak_formula (p \<bullet> \<langle>\<langle>\<tau>\<rangle>\<rangle>Conj (binsert (Pred \<phi>) (bsingleton x)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x \<alpha>. \<lbrakk>weak_formula x; weak_formula (p \<bullet> x)\<rbrakk> \<Longrightarrow> weak_formula (p \<bullet> \<langle>\<langle>\<alpha>\<rangle>\<rangle>x)
 2. \<And>x \<phi>. \<lbrakk>weak_formula x; weak_formula (p \<bullet> x)\<rbrakk> \<Longrightarrow> weak_formula (p \<bullet> \<langle>\<langle>\<tau>\<rangle>\<rangle>Conj (binsert (Pred \<phi>) (bsingleton x)))
[PROOF STEP]
case (wf_Act x \<alpha>)
[PROOF STATE]
proof (state)
this:
weak_formula x
weak_formula (p \<bullet> x)

goal (2 subgoals):
 1. \<And>x \<alpha>. \<lbrakk>weak_formula x; weak_formula (p \<bullet> x)\<rbrakk> \<Longrightarrow> weak_formula (p \<bullet> \<langle>\<langle>\<alpha>\<rangle>\<rangle>x)
 2. \<And>x \<phi>. \<lbrakk>weak_formula x; weak_formula (p \<bullet> x)\<rbrakk> \<Longrightarrow> weak_formula (p \<bullet> \<langle>\<langle>\<tau>\<rangle>\<rangle>Conj (binsert (Pred \<phi>) (bsingleton x)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
weak_formula x
weak_formula (p \<bullet> x)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
weak_formula x
weak_formula (p \<bullet> x)

goal (1 subgoal):
 1. weak_formula (p \<bullet> \<langle>\<langle>\<alpha>\<rangle>\<rangle>x)
[PROOF STEP]
by (simp add: weak_formula.wf_Act)
[PROOF STATE]
proof (state)
this:
weak_formula (p \<bullet> \<langle>\<langle>\<alpha>\<rangle>\<rangle>x)

goal (1 subgoal):
 1. \<And>x \<phi>. \<lbrakk>weak_formula x; weak_formula (p \<bullet> x)\<rbrakk> \<Longrightarrow> weak_formula (p \<bullet> \<langle>\<langle>\<tau>\<rangle>\<rangle>Conj (binsert (Pred \<phi>) (bsingleton x)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x \<phi>. \<lbrakk>weak_formula x; weak_formula (p \<bullet> x)\<rbrakk> \<Longrightarrow> weak_formula (p \<bullet> \<langle>\<langle>\<tau>\<rangle>\<rangle>Conj (binsert (Pred \<phi>) (bsingleton x)))
[PROOF STEP]
case (wf_Pred x \<phi>)
[PROOF STATE]
proof (state)
this:
weak_formula x
weak_formula (p \<bullet> x)

goal (1 subgoal):
 1. \<And>x \<phi>. \<lbrakk>weak_formula x; weak_formula (p \<bullet> x)\<rbrakk> \<Longrightarrow> weak_formula (p \<bullet> \<langle>\<langle>\<tau>\<rangle>\<rangle>Conj (binsert (Pred \<phi>) (bsingleton x)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
weak_formula x
weak_formula (p \<bullet> x)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
weak_formula x
weak_formula (p \<bullet> x)

goal (1 subgoal):
 1. weak_formula (p \<bullet> \<langle>\<langle>\<tau>\<rangle>\<rangle>Conj (binsert (Pred \<phi>) (bsingleton x)))
[PROOF STEP]
by (simp add: tau_eqvt weak_formula.wf_Pred)
[PROOF STATE]
proof (state)
this:
weak_formula (p \<bullet> \<langle>\<langle>\<tau>\<rangle>\<rangle>Conj (binsert (Pred \<phi>) (bsingleton x)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma set_not_emptyI[intro 0]: "x \<in> S \<Longrightarrow> S \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> S \<Longrightarrow> S \<noteq> {}
[PROOF STEP]
by auto


[STATEMENT]
lemma sets_empty_iffI[intro 0]:
    assumes "\<And> a. a \<in> A \<Longrightarrow> \<exists> b. b \<in> B"
    assumes "\<And> b. b \<in> B \<Longrightarrow> \<exists> a. a \<in> A"
    shows "A = {} \<longleftrightarrow> B = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A = {}) = (B = {})
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?a \<in> A \<Longrightarrow> \<exists>b. b \<in> B
?b \<in> B \<Longrightarrow> \<exists>a. a \<in> A

goal (1 subgoal):
 1. (A = {}) = (B = {})
[PROOF STEP]
by auto


[STATEMENT]
lemma disjointI[intro 0]:
    assumes "\<And> x. x \<in> A \<Longrightarrow> x \<in> B \<Longrightarrow> False"
    shows "A \<inter> B = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<inter> B = {}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> A; ?x \<in> B\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. A \<inter> B = {}
[PROOF STEP]
by auto


[STATEMENT]
lemma range_subsetI[intro 0]:
    assumes "\<And> x. f x \<in> S"
    shows "range f \<subseteq> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. range f \<subseteq> S
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f ?x \<in> S

goal (1 subgoal):
 1. range f \<subseteq> S
[PROOF STEP]
by blast


[STATEMENT]
lemma finite_imageI_range:
    assumes "finite (range f)"
    shows "finite (f ` A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (f ` A)
[PROOF STEP]
using finite_subset image_mono subset_UNIV assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite ?A
?A \<subseteq> ?B \<Longrightarrow> ?f ` ?A \<subseteq> ?f ` ?B
?A \<subseteq> UNIV
finite (range f)

goal (1 subgoal):
 1. finite (f ` A)
[PROOF STEP]
by metis


[STATEMENT]
lemma inf_img_fin_domE':
    assumes "infinite A"
    assumes "finite (f ` A)"
    obtains y
    where "y \<in> f ` A" "infinite (A \<inter> f -` {y})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> f ` A; infinite (A \<inter> f -` {y})\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>y. \<lbrakk>y \<in> f ` A; infinite (A \<inter> f -` {y})\<rbrakk> \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume 1: "\<not> thesis"
[PROOF STATE]
proof (state)
this:
\<not> thesis

goal (1 subgoal):
 1. \<lbrakk>\<And>y. \<lbrakk>y \<in> f ` A; infinite (A \<inter> f -` {y})\<rbrakk> \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have 2: "finite (\<Union> y \<in> f ` A. A \<inter> f -` {y})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (\<Union>y\<in>f ` A. A \<inter> f -` {y})
[PROOF STEP]
proof (rule finite_UN_I)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite (f ` A)
 2. \<And>y. y \<in> f ` A \<Longrightarrow> finite (A \<inter> f -` {y})
[PROOF STEP]
show "finite (f ` A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (f ` A)
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
finite (f ` A)

goal (1 subgoal):
 1. finite (f ` A)
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
finite (f ` A)

goal (1 subgoal):
 1. \<And>y. y \<in> f ` A \<Longrightarrow> finite (A \<inter> f -` {y})
[PROOF STEP]
show "\<And> y. y \<in> f ` A \<Longrightarrow> finite (A \<inter> f -` {y})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. y \<in> f ` A \<Longrightarrow> finite (A \<inter> f -` {y})
[PROOF STEP]
using that 1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?y \<in> f ` A; infinite (A \<inter> f -` {?y})\<rbrakk> \<Longrightarrow> thesis
\<not> thesis

goal (1 subgoal):
 1. \<And>y. y \<in> f ` A \<Longrightarrow> finite (A \<inter> f -` {y})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?y \<in> f ` A \<Longrightarrow> finite (A \<inter> f -` {?y})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite (\<Union>y\<in>f ` A. A \<inter> f -` {y})

goal (1 subgoal):
 1. \<lbrakk>\<And>y. \<lbrakk>y \<in> f ` A; infinite (A \<inter> f -` {y})\<rbrakk> \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have 3: "A \<subseteq> (\<Union> y \<in> f ` A. A \<inter> f -` {y})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> (\<Union>y\<in>f ` A. A \<inter> f -` {y})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
A \<subseteq> (\<Union>y\<in>f ` A. A \<inter> f -` {y})

goal (1 subgoal):
 1. \<lbrakk>\<And>y. \<lbrakk>y \<in> f ` A; infinite (A \<inter> f -` {y})\<rbrakk> \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
using assms(1) 2 3
[PROOF STATE]
proof (prove)
using this:
infinite A
finite (\<Union>y\<in>f ` A. A \<inter> f -` {y})
A \<subseteq> (\<Union>y\<in>f ` A. A \<inter> f -` {y})

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vimage_singleton[simp]: "f -` {y} = {x. f x = y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f -` {y} = {x. f x = y}
[PROOF STEP]
unfolding vimage_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x. f x \<in> {y}} = {x. f x = y}
[PROOF STEP]
by simp


[STATEMENT]
lemma these_alt_def: "Option.these S = Some -` S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Option.these S = Some -` S
[PROOF STEP]
unfolding Option.these_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the ` {x \<in> S. x \<noteq> None} = Some -` S
[PROOF STEP]
by force


[STATEMENT]
lemma the_vimage_subset: "the -` {a} \<subseteq> {None, Some a}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the -` {a} \<subseteq> {None, Some a}
[PROOF STEP]
by auto


[STATEMENT]
lemma finite_induct_reverse[consumes 1, case_names remove]:
    assumes "finite S"
    assumes "\<And> S. finite S \<Longrightarrow> (\<And> x. x \<in> S \<Longrightarrow> P (S - {x})) \<Longrightarrow> P S"
    shows "P S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P S
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
finite S

goal (1 subgoal):
 1. P S
[PROOF STEP]
proof (induct rule: finite_psubset_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>A. \<lbrakk>finite A; \<And>B. B \<subset> A \<Longrightarrow> P B\<rbrakk> \<Longrightarrow> P A
[PROOF STEP]
case (psubset S)
[PROOF STATE]
proof (state)
this:
finite S
?B \<subset> S \<Longrightarrow> P ?B

goal (1 subgoal):
 1. \<And>A. \<lbrakk>finite A; \<And>B. B \<subset> A \<Longrightarrow> P B\<rbrakk> \<Longrightarrow> P A
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P S
[PROOF STEP]
proof (rule assms(2))
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite S
 2. \<And>x. x \<in> S \<Longrightarrow> P (S - {x})
[PROOF STEP]
show "finite S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite S
[PROOF STEP]
using psubset(1)
[PROOF STATE]
proof (prove)
using this:
finite S

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

goal (1 subgoal):
 1. \<And>x. x \<in> S \<Longrightarrow> P (S - {x})
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> S \<Longrightarrow> P (S - {x})
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> S \<Longrightarrow> P (S - {x})
[PROOF STEP]
assume 0: "x \<in> S"
[PROOF STATE]
proof (state)
this:
x \<in> S

goal (1 subgoal):
 1. \<And>x. x \<in> S \<Longrightarrow> P (S - {x})
[PROOF STEP]
show "P (S - {x})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (S - {x})
[PROOF STEP]
proof (rule psubset(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. S - {x} \<subset> S
[PROOF STEP]
show "S - {x} \<subset> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S - {x} \<subset> S
[PROOF STEP]
using 0
[PROOF STATE]
proof (prove)
using this:
x \<in> S

goal (1 subgoal):
 1. S - {x} \<subset> S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
S - {x} \<subset> S

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P (S - {x})

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma zero_not_in_Suc_image[simp]: "0 \<notin> Suc ` A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<notin> Suc ` A
[PROOF STEP]
by auto


[STATEMENT]
lemma Collect_split_Suc:
    "\<not> P 0 \<Longrightarrow> {i. P i} = Suc ` {i. P (Suc i)}"
    "P 0 \<Longrightarrow> {i. P i} = {0} \<union> Suc ` {i. P (Suc i)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> P 0 \<Longrightarrow> {i. P i} = Suc ` {i. P (Suc i)}) &&& (P 0 \<Longrightarrow> {i. P i} = {0} \<union> Suc ` {i. P (Suc i)})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<not> P 0 \<Longrightarrow> {i. P i} = Suc ` {i. P (Suc i)}
 2. P 0 \<Longrightarrow> {i. P i} = {0} \<union> Suc ` {i. P (Suc i)}
[PROOF STEP]
assume "\<not> P 0"
[PROOF STATE]
proof (state)
this:
\<not> P 0

goal (2 subgoals):
 1. \<not> P 0 \<Longrightarrow> {i. P i} = Suc ` {i. P (Suc i)}
 2. P 0 \<Longrightarrow> {i. P i} = {0} \<union> Suc ` {i. P (Suc i)}
[PROOF STEP]
thus "{i. P i} = Suc ` {i. P (Suc i)}"
[PROOF STATE]
proof (prove)
using this:
\<not> P 0

goal (1 subgoal):
 1. {i. P i} = Suc ` {i. P (Suc i)}
[PROOF STEP]
by (auto, metis image_eqI mem_Collect_eq nat.exhaust)
[PROOF STATE]
proof (state)
this:
{i. P i} = Suc ` {i. P (Suc i)}

goal (1 subgoal):
 1. P 0 \<Longrightarrow> {i. P i} = {0} \<union> Suc ` {i. P (Suc i)}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P 0 \<Longrightarrow> {i. P i} = {0} \<union> Suc ` {i. P (Suc i)}
[PROOF STEP]
assume "P 0"
[PROOF STATE]
proof (state)
this:
P 0

goal (1 subgoal):
 1. P 0 \<Longrightarrow> {i. P i} = {0} \<union> Suc ` {i. P (Suc i)}
[PROOF STEP]
thus "{i. P i} = {0} \<union> Suc ` {i. P (Suc i)}"
[PROOF STATE]
proof (prove)
using this:
P 0

goal (1 subgoal):
 1. {i. P i} = {0} \<union> Suc ` {i. P (Suc i)}
[PROOF STEP]
by (auto, metis imageI mem_Collect_eq not0_implies_Suc)
[PROOF STATE]
proof (state)
this:
{i. P i} = {0} \<union> Suc ` {i. P (Suc i)}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Collect_subsume[simp]:
    assumes "\<And> x. x \<in> A \<Longrightarrow> P x"
    shows "{x \<in> A. P x} = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x \<in> A. P x} = A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?x \<in> A \<Longrightarrow> P ?x

goal (1 subgoal):
 1. {x \<in> A. P x} = A
[PROOF STEP]
unfolding simp_implies_def
[PROOF STATE]
proof (prove)
using this:
?x \<in> A \<Longrightarrow> P ?x

goal (1 subgoal):
 1. {x \<in> A. P x} = A
[PROOF STEP]
by auto


[STATEMENT]
lemma Max_ge':
    assumes "finite A" "A \<noteq> {}"
    assumes "b \<in> A" "a \<le> b"
    shows "a \<le> Max A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> Max A
[PROOF STEP]
using assms Max_ge_iff
[PROOF STATE]
proof (prove)
using this:
finite A
A \<noteq> {}
b \<in> A
a \<le> b
\<lbrakk>finite ?A; ?A \<noteq> {}\<rbrakk> \<Longrightarrow> (?x \<le> Max ?A) = (\<exists>a\<in>?A. ?x \<le> a)

goal (1 subgoal):
 1. a \<le> Max A
[PROOF STEP]
by auto


[STATEMENT]
lemma least_contains[intro?, simp]:
    fixes A :: "'a :: wellorder set"
    assumes "k \<in> A"
    shows "least A \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. least A \<in> A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
k \<in> A

goal (1 subgoal):
 1. least A \<in> A
[PROOF STEP]
by (metis LeastI)


[STATEMENT]
lemma least_contains'[intro?, simp]:
    fixes A :: "'a :: wellorder set"
    assumes "A \<noteq> {}"
    shows "least A \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. least A \<in> A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A \<noteq> {}

goal (1 subgoal):
 1. least A \<in> A
[PROOF STEP]
by (metis LeastI equals0I)


[STATEMENT]
lemma least_least[intro?, simp]:
    fixes A :: "'a :: wellorder set"
    assumes "k \<in> A"
    shows "least A \<le> k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. least A \<le> k
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
k \<in> A

goal (1 subgoal):
 1. least A \<le> k
[PROOF STEP]
by (metis Least_le)


[STATEMENT]
lemma least_unique:
    fixes A :: "'a :: wellorder set"
    assumes "k \<in> A" "k \<le> least A"
    shows "k = least A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k = least A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
k \<in> A
k \<le> least A

goal (1 subgoal):
 1. k = least A
[PROOF STEP]
by (metis Least_le antisym)


[STATEMENT]
lemma least_not_less:
    fixes A :: "'a :: wellorder set"
    assumes "k < least A"
    shows "k \<notin> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<notin> A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
k < least A

goal (1 subgoal):
 1. k \<notin> A
[PROOF STEP]
by (metis not_less_Least)


[STATEMENT]
lemma leastI2_order[simp]:
    fixes A :: "'a :: wellorder set"
    assumes "A \<noteq> {}" "\<And> k. k \<in> A \<Longrightarrow> (\<And> l. l \<in> A \<Longrightarrow> k \<le> l) \<Longrightarrow> P k"
    shows "P (least A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (least A)
[PROOF STEP]
proof (rule LeastI2_order)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. ?x \<in> A
 2. \<And>y. y \<in> A \<Longrightarrow> ?x \<le> y
 3. \<And>x. \<lbrakk>x \<in> A; \<forall>y. y \<in> A \<longrightarrow> x \<le> y\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
show "least A \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. least A \<in> A
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
A \<noteq> {}

goal (1 subgoal):
 1. least A \<in> A
[PROOF STEP]
by rule
[PROOF STATE]
proof (state)
this:
least A \<in> A

goal (2 subgoals):
 1. \<And>y. y \<in> A \<Longrightarrow> least A \<le> y
 2. \<And>x. \<lbrakk>x \<in> A; \<forall>y. y \<in> A \<longrightarrow> x \<le> y\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>y. y \<in> A \<Longrightarrow> least A \<le> y
 2. \<And>x. \<lbrakk>x \<in> A; \<forall>y. y \<in> A \<longrightarrow> x \<le> y\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>y. y \<in> A \<Longrightarrow> least A \<le> y
 2. \<And>x. \<lbrakk>x \<in> A; \<forall>y. y \<in> A \<longrightarrow> x \<le> y\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
assume 1: "k \<in> A"
[PROOF STATE]
proof (state)
this:
k \<in> A

goal (2 subgoals):
 1. \<And>y. y \<in> A \<Longrightarrow> least A \<le> y
 2. \<And>x. \<lbrakk>x \<in> A; \<forall>y. y \<in> A \<longrightarrow> x \<le> y\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
show "least A \<le> k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. least A \<le> k
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
k \<in> A

goal (1 subgoal):
 1. least A \<le> k
[PROOF STEP]
by rule
[PROOF STATE]
proof (state)
this:
least A \<le> k

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> A; \<forall>y. y \<in> A \<longrightarrow> x \<le> y\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> A; \<forall>y. y \<in> A \<longrightarrow> x \<le> y\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> A; \<forall>y. y \<in> A \<longrightarrow> x \<le> y\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
assume 1: "k \<in> A" "\<forall> l. l \<in> A \<longrightarrow> k \<le> l"
[PROOF STATE]
proof (state)
this:
k \<in> A
\<forall>l. l \<in> A \<longrightarrow> k \<le> l

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> A; \<forall>y. y \<in> A \<longrightarrow> x \<le> y\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
show "P k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P k
[PROOF STEP]
using assms(2) 1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?k \<in> A; \<And>l. l \<in> A \<Longrightarrow> ?k \<le> l\<rbrakk> \<Longrightarrow> P ?k
k \<in> A
\<forall>l. l \<in> A \<longrightarrow> k \<le> l

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma least_singleton[simp]:
    fixes a :: "'a :: wellorder"
    shows "least {a} = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. least {a} = a
[PROOF STEP]
by (metis insert_not_empty least_contains' singletonD)


[STATEMENT]
lemma least_image[simp]:
    fixes f :: "'a :: wellorder \<Rightarrow> 'b :: wellorder"
    assumes "A \<noteq> {}" "\<And> k l. k \<in> A \<Longrightarrow> l \<in> A \<Longrightarrow> k \<le> l \<Longrightarrow> f k \<le> f l"
    shows "least (f ` A) = f (least A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. least (f ` A) = f (least A)
[PROOF STEP]
proof (rule leastI2_order)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A \<noteq> {}
 2. \<And>k. \<lbrakk>k \<in> A; \<And>l. l \<in> A \<Longrightarrow> k \<le> l\<rbrakk> \<Longrightarrow> least (f ` A) = f k
[PROOF STEP]
show "A \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<noteq> {}
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
A \<noteq> {}

goal (1 subgoal):
 1. A \<noteq> {}
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
A \<noteq> {}

goal (1 subgoal):
 1. \<And>k. \<lbrakk>k \<in> A; \<And>l. l \<in> A \<Longrightarrow> k \<le> l\<rbrakk> \<Longrightarrow> least (f ` A) = f k
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>k \<in> A; \<And>l. l \<in> A \<Longrightarrow> k \<le> l\<rbrakk> \<Longrightarrow> least (f ` A) = f k
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>k \<in> A; \<And>l. l \<in> A \<Longrightarrow> k \<le> l\<rbrakk> \<Longrightarrow> least (f ` A) = f k
[PROOF STEP]
assume 1: "k \<in> A" "\<And> i. i \<in> A \<Longrightarrow> k \<le> i"
[PROOF STATE]
proof (state)
this:
k \<in> A
?i \<in> A \<Longrightarrow> k \<le> ?i

goal (1 subgoal):
 1. \<And>k. \<lbrakk>k \<in> A; \<And>l. l \<in> A \<Longrightarrow> k \<le> l\<rbrakk> \<Longrightarrow> least (f ` A) = f k
[PROOF STEP]
show "least (f ` A) = f k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. least (f ` A) = f k
[PROOF STEP]
proof (rule leastI2_order)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f ` A \<noteq> {}
 2. \<And>ka. \<lbrakk>ka \<in> f ` A; \<And>l. l \<in> f ` A \<Longrightarrow> ka \<le> l\<rbrakk> \<Longrightarrow> ka = f k
[PROOF STEP]
show "f ` A \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` A \<noteq> {}
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
A \<noteq> {}

goal (1 subgoal):
 1. f ` A \<noteq> {}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f ` A \<noteq> {}

goal (1 subgoal):
 1. \<And>ka. \<lbrakk>ka \<in> f ` A; \<And>l. l \<in> f ` A \<Longrightarrow> ka \<le> l\<rbrakk> \<Longrightarrow> ka = f k
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ka. \<lbrakk>ka \<in> f ` A; \<And>l. l \<in> f ` A \<Longrightarrow> ka \<le> l\<rbrakk> \<Longrightarrow> ka = f k
[PROOF STEP]
fix l
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ka. \<lbrakk>ka \<in> f ` A; \<And>l. l \<in> f ` A \<Longrightarrow> ka \<le> l\<rbrakk> \<Longrightarrow> ka = f k
[PROOF STEP]
assume 2: "l \<in> f ` A" "\<And> i. i \<in> f ` A \<Longrightarrow> l \<le> i"
[PROOF STATE]
proof (state)
this:
l \<in> f ` A
?i \<in> f ` A \<Longrightarrow> l \<le> ?i

goal (1 subgoal):
 1. \<And>ka. \<lbrakk>ka \<in> f ` A; \<And>l. l \<in> f ` A \<Longrightarrow> ka \<le> l\<rbrakk> \<Longrightarrow> ka = f k
[PROOF STEP]
show "l = f k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l = f k
[PROOF STEP]
using assms(2) 1 2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?k \<in> A; ?l \<in> A; ?k \<le> ?l\<rbrakk> \<Longrightarrow> f ?k \<le> f ?l
k \<in> A
?i \<in> A \<Longrightarrow> k \<le> ?i
l \<in> f ` A
?i \<in> f ` A \<Longrightarrow> l \<le> ?i

goal (1 subgoal):
 1. l = f k
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
l = f k

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
least (f ` A) = f k

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma least_le:
    fixes A B :: "'a :: wellorder set"
    assumes "B \<noteq> {}"
    assumes "\<And> i. i \<le> least A \<Longrightarrow> i \<le> least B \<Longrightarrow> i \<in> B \<Longrightarrow> i \<in> A"
    shows "least A \<le> least B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. least A \<le> least B
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> least A \<le> least B \<Longrightarrow> False
[PROOF STEP]
assume 1: "\<not> least A \<le> least B"
[PROOF STATE]
proof (state)
this:
\<not> least A \<le> least B

goal (1 subgoal):
 1. \<not> least A \<le> least B \<Longrightarrow> False
[PROOF STEP]
have 2: "least B \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. least B \<in> A
[PROOF STEP]
using assms(1, 2) 1
[PROOF STATE]
proof (prove)
using this:
B \<noteq> {}
\<lbrakk>?i \<le> least A; ?i \<le> least B; ?i \<in> B\<rbrakk> \<Longrightarrow> ?i \<in> A
\<not> least A \<le> least B

goal (1 subgoal):
 1. least B \<in> A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
least B \<in> A

goal (1 subgoal):
 1. \<not> least A \<le> least B \<Longrightarrow> False
[PROOF STEP]
have 3: "least A \<le> least B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. least A \<le> least B
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
least B \<in> A

goal (1 subgoal):
 1. least A \<le> least B
[PROOF STEP]
by rule
[PROOF STATE]
proof (state)
this:
least A \<le> least B

goal (1 subgoal):
 1. \<not> least A \<le> least B \<Longrightarrow> False
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
using 1 3
[PROOF STATE]
proof (prove)
using this:
\<not> least A \<le> least B
least A \<le> least B

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma least_eq:
    fixes A B :: "'a :: wellorder set"
    assumes "A \<noteq> {}" "B \<noteq> {}"
    assumes "\<And> i. i \<le> least A \<Longrightarrow> i \<le> least B \<Longrightarrow> i \<in> A \<longleftrightarrow> i \<in> B"
    shows "least A = least B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. least A = least B
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A \<noteq> {}
B \<noteq> {}
\<lbrakk>?i \<le> least A; ?i \<le> least B\<rbrakk> \<Longrightarrow> (?i \<in> A) = (?i \<in> B)

goal (1 subgoal):
 1. least A = least B
[PROOF STEP]
by (auto intro: antisym least_le)


[STATEMENT]
lemma least_Suc[simp]:
    assumes "A \<noteq> {}"
    shows "least (Suc ` A) = Suc (least A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. least (Suc ` A) = Suc (least A)
[PROOF STEP]
proof (rule antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. least (Suc ` A) \<le> Suc (least A)
 2. Suc (least A) \<le> least (Suc ` A)
[PROOF STEP]
obtain k where 10: "k \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k. k \<in> A \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A \<noteq> {}

goal (1 subgoal):
 1. (\<And>k. k \<in> A \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
k \<in> A

goal (2 subgoals):
 1. least (Suc ` A) \<le> Suc (least A)
 2. Suc (least A) \<le> least (Suc ` A)
[PROOF STEP]
have 11: "Suc k \<in> Suc ` A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc k \<in> Suc ` A
[PROOF STEP]
using 10
[PROOF STATE]
proof (prove)
using this:
k \<in> A

goal (1 subgoal):
 1. Suc k \<in> Suc ` A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc k \<in> Suc ` A

goal (2 subgoals):
 1. least (Suc ` A) \<le> Suc (least A)
 2. Suc (least A) \<le> least (Suc ` A)
[PROOF STEP]
have 20: "least A \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. least A \<in> A
[PROOF STEP]
using 10 LeastI
[PROOF STATE]
proof (prove)
using this:
k \<in> A
?P ?k \<Longrightarrow> ?P (LEAST x. ?P x)

goal (1 subgoal):
 1. least A \<in> A
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
least A \<in> A

goal (2 subgoals):
 1. least (Suc ` A) \<le> Suc (least A)
 2. Suc (least A) \<le> least (Suc ` A)
[PROOF STEP]
have 21: "least (Suc ` A) \<in> Suc ` A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. least (Suc ` A) \<in> Suc ` A
[PROOF STEP]
using 11 LeastI
[PROOF STATE]
proof (prove)
using this:
Suc k \<in> Suc ` A
?P ?k \<Longrightarrow> ?P (LEAST x. ?P x)

goal (1 subgoal):
 1. least (Suc ` A) \<in> Suc ` A
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
least (Suc ` A) \<in> Suc ` A

goal (2 subgoals):
 1. least (Suc ` A) \<le> Suc (least A)
 2. Suc (least A) \<le> least (Suc ` A)
[PROOF STEP]
have 30: "\<And> l. l \<in> A \<Longrightarrow> least A \<le> l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. l \<in> A \<Longrightarrow> least A \<le> l
[PROOF STEP]
using 10 Least_le
[PROOF STATE]
proof (prove)
using this:
k \<in> A
?P ?k \<Longrightarrow> (LEAST x. ?P x) \<le> ?k

goal (1 subgoal):
 1. \<And>l. l \<in> A \<Longrightarrow> least A \<le> l
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
?l \<in> A \<Longrightarrow> least A \<le> ?l

goal (2 subgoals):
 1. least (Suc ` A) \<le> Suc (least A)
 2. Suc (least A) \<le> least (Suc ` A)
[PROOF STEP]
have 31: "\<And> l. l \<in> Suc ` A \<Longrightarrow> least (Suc ` A) \<le> l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. l \<in> Suc ` A \<Longrightarrow> least (Suc ` A) \<le> l
[PROOF STEP]
using 11 Least_le
[PROOF STATE]
proof (prove)
using this:
Suc k \<in> Suc ` A
?P ?k \<Longrightarrow> (LEAST x. ?P x) \<le> ?k

goal (1 subgoal):
 1. \<And>l. l \<in> Suc ` A \<Longrightarrow> least (Suc ` A) \<le> l
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
?l \<in> Suc ` A \<Longrightarrow> least (Suc ` A) \<le> ?l

goal (2 subgoals):
 1. least (Suc ` A) \<le> Suc (least A)
 2. Suc (least A) \<le> least (Suc ` A)
[PROOF STEP]
show "least (Suc ` A) \<le> Suc (least A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. least (Suc ` A) \<le> Suc (least A)
[PROOF STEP]
using 20 31
[PROOF STATE]
proof (prove)
using this:
least A \<in> A
?l \<in> Suc ` A \<Longrightarrow> least (Suc ` A) \<le> ?l

goal (1 subgoal):
 1. least (Suc ` A) \<le> Suc (least A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
least (Suc ` A) \<le> Suc (least A)

goal (1 subgoal):
 1. Suc (least A) \<le> least (Suc ` A)
[PROOF STEP]
show "Suc (least A) \<le> least (Suc ` A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (least A) \<le> least (Suc ` A)
[PROOF STEP]
using 21 30
[PROOF STATE]
proof (prove)
using this:
least (Suc ` A) \<in> Suc ` A
?l \<in> A \<Longrightarrow> least A \<le> ?l

goal (1 subgoal):
 1. Suc (least A) \<le> least (Suc ` A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc (least A) \<le> least (Suc ` A)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma least_Suc_diff[simp]: "Suc ` A - {least (Suc ` A)} = Suc ` (A - {least A})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc ` A - {least (Suc ` A)} = Suc ` (A - {least A})
[PROOF STEP]
proof (cases "A = {}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A = {} \<Longrightarrow> Suc ` A - {least (Suc ` A)} = Suc ` (A - {least A})
 2. A \<noteq> {} \<Longrightarrow> Suc ` A - {least (Suc ` A)} = Suc ` (A - {least A})
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
A = {}

goal (2 subgoals):
 1. A = {} \<Longrightarrow> Suc ` A - {least (Suc ` A)} = Suc ` (A - {least A})
 2. A \<noteq> {} \<Longrightarrow> Suc ` A - {least (Suc ` A)} = Suc ` (A - {least A})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc ` A - {least (Suc ` A)} = Suc ` (A - {least A})
[PROOF STEP]
unfolding True
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc ` {} - {least (Suc ` {})} = Suc ` ({} - {least {}})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Suc ` A - {least (Suc ` A)} = Suc ` (A - {least A})

goal (1 subgoal):
 1. A \<noteq> {} \<Longrightarrow> Suc ` A - {least (Suc ` A)} = Suc ` (A - {least A})
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A \<noteq> {} \<Longrightarrow> Suc ` A - {least (Suc ` A)} = Suc ` (A - {least A})
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
A \<noteq> {}

goal (1 subgoal):
 1. A \<noteq> {} \<Longrightarrow> Suc ` A - {least (Suc ` A)} = Suc ` (A - {least A})
[PROOF STEP]
have "Suc ` A - {least (Suc ` A)} = Suc ` A - {Suc (least A)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc ` A - {least (Suc ` A)} = Suc ` A - {Suc (least A)}
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
A \<noteq> {}

goal (1 subgoal):
 1. Suc ` A - {least (Suc ` A)} = Suc ` A - {Suc (least A)}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Suc ` A - {least (Suc ` A)} = Suc ` A - {Suc (least A)}

goal (1 subgoal):
 1. A \<noteq> {} \<Longrightarrow> Suc ` A - {least (Suc ` A)} = Suc ` (A - {least A})
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Suc ` A - {least (Suc ` A)} = Suc ` A - {Suc (least A)}

goal (1 subgoal):
 1. A \<noteq> {} \<Longrightarrow> Suc ` A - {least (Suc ` A)} = Suc ` (A - {least A})
[PROOF STEP]
have "\<dots> = Suc ` A - Suc ` {least A}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc ` A - {Suc (least A)} = Suc ` A - Suc ` {least A}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Suc ` A - {Suc (least A)} = Suc ` A - Suc ` {least A}

goal (1 subgoal):
 1. A \<noteq> {} \<Longrightarrow> Suc ` A - {least (Suc ` A)} = Suc ` (A - {least A})
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Suc ` A - {Suc (least A)} = Suc ` A - Suc ` {least A}

goal (1 subgoal):
 1. A \<noteq> {} \<Longrightarrow> Suc ` A - {least (Suc ` A)} = Suc ` (A - {least A})
[PROOF STEP]
have "\<dots> = Suc ` (A - {least A})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc ` A - Suc ` {least A} = Suc ` (A - {least A})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Suc ` A - Suc ` {least A} = Suc ` (A - {least A})

goal (1 subgoal):
 1. A \<noteq> {} \<Longrightarrow> Suc ` A - {least (Suc ` A)} = Suc ` (A - {least A})
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Suc ` A - {least (Suc ` A)} = Suc ` (A - {least A})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Suc ` A - {least (Suc ` A)} = Suc ` (A - {least A})

goal (1 subgoal):
 1. Suc ` A - {least (Suc ` A)} = Suc ` (A - {least A})
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
Suc ` A - {least (Suc ` A)} = Suc ` (A - {least A})

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Max_diff_least[simp]:
    fixes A :: "'a :: wellorder set"
    assumes "finite A" "A - {least A} \<noteq> {}"
    shows "Max (A - {least A}) = Max A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Max (A - {least A}) = Max A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Max (A - {least A}) = Max A
[PROOF STEP]
have 1: "least A \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. least A \<in> A
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
A - {least A} \<noteq> {}

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

goal (1 subgoal):
 1. Max (A - {least A}) = Max A
[PROOF STEP]
obtain a where 2: "a \<in> A - {least A}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a. a \<in> A - {least A} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
A - {least A} \<noteq> {}

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

goal (1 subgoal):
 1. Max (A - {least A}) = Max A
[PROOF STEP]
have "Max A = Max (insert (least A) (A - {least A}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Max A = Max (insert (least A) (A - {least A}))
[PROOF STEP]
using insert_absorb 1
[PROOF STATE]
proof (prove)
using this:
?a \<in> ?A \<Longrightarrow> insert ?a ?A = ?A
least A \<in> A

goal (1 subgoal):
 1. Max A = Max (insert (least A) (A - {least A}))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
Max A = Max (insert (least A) (A - {least A}))

goal (1 subgoal):
 1. Max (A - {least A}) = Max A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Max A = Max (insert (least A) (A - {least A}))

goal (1 subgoal):
 1. Max (A - {least A}) = Max A
[PROOF STEP]
have "\<dots> = max (least A) (Max (A - {least A}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Max (insert (least A) (A - {least A})) = max (least A) (Max (A - {least A}))
[PROOF STEP]
proof (rule Max_insert)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite (A - {least A})
 2. A - {least A} \<noteq> {}
[PROOF STEP]
show "finite (A - {least A})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (A - {least A})
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
finite A

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

goal (1 subgoal):
 1. A - {least A} \<noteq> {}
[PROOF STEP]
show "A - {least A} \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A - {least A} \<noteq> {}
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
A - {least A} \<noteq> {}

goal (1 subgoal):
 1. A - {least A} \<noteq> {}
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
A - {least A} \<noteq> {}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Max (insert (least A) (A - {least A})) = max (least A) (Max (A - {least A}))

goal (1 subgoal):
 1. Max (A - {least A}) = Max A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Max (insert (least A) (A - {least A})) = max (least A) (Max (A - {least A}))

goal (1 subgoal):
 1. Max (A - {least A}) = Max A
[PROOF STEP]
have "\<dots> = Max (A - {least A})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max (least A) (Max (A - {least A})) = Max (A - {least A})
[PROOF STEP]
proof (rule max_absorb2, rule Max_ge')
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. finite (A - {least A})
 2. A - {least A} \<noteq> {}
 3. ?b2 \<in> A - {least A}
 4. least A \<le> ?b2
[PROOF STEP]
show "finite (A - {least A})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (A - {least A})
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
finite A

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

goal (3 subgoals):
 1. A - {least A} \<noteq> {}
 2. ?b2 \<in> A - {least A}
 3. least A \<le> ?b2
[PROOF STEP]
show "A - {least A} \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A - {least A} \<noteq> {}
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
A - {least A} \<noteq> {}

goal (1 subgoal):
 1. A - {least A} \<noteq> {}
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
A - {least A} \<noteq> {}

goal (2 subgoals):
 1. ?b2 \<in> A - {least A}
 2. least A \<le> ?b2
[PROOF STEP]
show "a \<in> A - {least A}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> A - {least A}
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
a \<in> A - {least A}

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

goal (1 subgoal):
 1. least A \<le> a
[PROOF STEP]
show "least A \<le> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. least A \<le> a
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
a \<in> A - {least A}

goal (1 subgoal):
 1. least A \<le> a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
least A \<le> a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
max (least A) (Max (A - {least A})) = Max (A - {least A})

goal (1 subgoal):
 1. Max (A - {least A}) = Max A
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Max A = Max (A - {least A})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Max A = Max (A - {least A})

goal (1 subgoal):
 1. Max (A - {least A}) = Max A
[PROOF STEP]
by rule
[PROOF STATE]
proof (state)
this:
Max (A - {least A}) = Max A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nat_set_card_equality_less:
    fixes A :: "nat set"
    assumes "x \<in> A" "y \<in> A" "card {z \<in> A. z < x} = card {z \<in> A. z < y}"
    shows "x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
proof (cases x y rule: linorder_cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. x < y \<Longrightarrow> x = y
 2. x = y \<Longrightarrow> x = y
 3. y < x \<Longrightarrow> x = y
[PROOF STEP]
case less
[PROOF STATE]
proof (state)
this:
x < y

goal (3 subgoals):
 1. x < y \<Longrightarrow> x = y
 2. x = y \<Longrightarrow> x = y
 3. y < x \<Longrightarrow> x = y
[PROOF STEP]
have 0: "finite {z \<in> A. z < y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {z \<in> A. z < y}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite {z \<in> A. z < y}

goal (3 subgoals):
 1. x < y \<Longrightarrow> x = y
 2. x = y \<Longrightarrow> x = y
 3. y < x \<Longrightarrow> x = y
[PROOF STEP]
have 1: "{z \<in> A. z < x} \<subset> {z \<in> A. z < y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {z \<in> A. z < x} \<subset> {z \<in> A. z < y}
[PROOF STEP]
using assms(1, 2) less
[PROOF STATE]
proof (prove)
using this:
x \<in> A
y \<in> A
x < y

goal (1 subgoal):
 1. {z \<in> A. z < x} \<subset> {z \<in> A. z < y}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
{z \<in> A. z < x} \<subset> {z \<in> A. z < y}

goal (3 subgoals):
 1. x < y \<Longrightarrow> x = y
 2. x = y \<Longrightarrow> x = y
 3. y < x \<Longrightarrow> x = y
[PROOF STEP]
have 2: "card {z \<in> A. z < x} < card {z \<in> A. z < y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {z \<in> A. z < x} < card {z \<in> A. z < y}
[PROOF STEP]
using psubset_card_mono 0 1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?B; ?A \<subset> ?B\<rbrakk> \<Longrightarrow> card ?A < card ?B
finite {z \<in> A. z < y}
{z \<in> A. z < x} \<subset> {z \<in> A. z < y}

goal (1 subgoal):
 1. card {z \<in> A. z < x} < card {z \<in> A. z < y}
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
card {z \<in> A. z < x} < card {z \<in> A. z < y}

goal (3 subgoals):
 1. x < y \<Longrightarrow> x = y
 2. x = y \<Longrightarrow> x = y
 3. y < x \<Longrightarrow> x = y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
using assms(3) 2
[PROOF STATE]
proof (prove)
using this:
card {z \<in> A. z < x} = card {z \<in> A. z < y}
card {z \<in> A. z < x} < card {z \<in> A. z < y}

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

goal (2 subgoals):
 1. x = y \<Longrightarrow> x = y
 2. y < x \<Longrightarrow> x = y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = y \<Longrightarrow> x = y
 2. y < x \<Longrightarrow> x = y
[PROOF STEP]
case equal
[PROOF STATE]
proof (state)
this:
x = y

goal (2 subgoals):
 1. x = y \<Longrightarrow> x = y
 2. y < x \<Longrightarrow> x = y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
using equal
[PROOF STATE]
proof (prove)
using this:
x = y

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

goal (1 subgoal):
 1. y < x \<Longrightarrow> x = y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y < x \<Longrightarrow> x = y
[PROOF STEP]
case greater
[PROOF STATE]
proof (state)
this:
y < x

goal (1 subgoal):
 1. y < x \<Longrightarrow> x = y
[PROOF STEP]
have 0: "finite {z \<in> A. z < x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {z \<in> A. z < x}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite {z \<in> A. z < x}

goal (1 subgoal):
 1. y < x \<Longrightarrow> x = y
[PROOF STEP]
have 1: "{z \<in> A. z < y} \<subset> {z \<in> A. z < x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {z \<in> A. z < y} \<subset> {z \<in> A. z < x}
[PROOF STEP]
using assms(1, 2) greater
[PROOF STATE]
proof (prove)
using this:
x \<in> A
y \<in> A
y < x

goal (1 subgoal):
 1. {z \<in> A. z < y} \<subset> {z \<in> A. z < x}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
{z \<in> A. z < y} \<subset> {z \<in> A. z < x}

goal (1 subgoal):
 1. y < x \<Longrightarrow> x = y
[PROOF STEP]
have 2: "card {z \<in> A. z < y} < card {z \<in> A. z < x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {z \<in> A. z < y} < card {z \<in> A. z < x}
[PROOF STEP]
using psubset_card_mono 0 1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?B; ?A \<subset> ?B\<rbrakk> \<Longrightarrow> card ?A < card ?B
finite {z \<in> A. z < x}
{z \<in> A. z < y} \<subset> {z \<in> A. z < x}

goal (1 subgoal):
 1. card {z \<in> A. z < y} < card {z \<in> A. z < x}
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
card {z \<in> A. z < y} < card {z \<in> A. z < x}

goal (1 subgoal):
 1. y < x \<Longrightarrow> x = y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
using assms(3) 2
[PROOF STATE]
proof (prove)
using this:
card {z \<in> A. z < x} = card {z \<in> A. z < y}
card {z \<in> A. z < y} < card {z \<in> A. z < x}

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nat_set_card_equality_le:
    fixes A :: "nat set"
    assumes "x \<in> A" "y \<in> A" "card {z \<in> A. z \<le> x} = card {z \<in> A. z \<le> y}"
    shows "x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
proof (cases x y rule: linorder_cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. x < y \<Longrightarrow> x = y
 2. x = y \<Longrightarrow> x = y
 3. y < x \<Longrightarrow> x = y
[PROOF STEP]
case less
[PROOF STATE]
proof (state)
this:
x < y

goal (3 subgoals):
 1. x < y \<Longrightarrow> x = y
 2. x = y \<Longrightarrow> x = y
 3. y < x \<Longrightarrow> x = y
[PROOF STEP]
have 0: "finite {z \<in> A. z \<le> y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {z \<in> A. z \<le> y}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite {z \<in> A. z \<le> y}

goal (3 subgoals):
 1. x < y \<Longrightarrow> x = y
 2. x = y \<Longrightarrow> x = y
 3. y < x \<Longrightarrow> x = y
[PROOF STEP]
have 1: "{z \<in> A. z \<le> x} \<subset> {z \<in> A. z \<le> y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {z \<in> A. z \<le> x} \<subset> {z \<in> A. z \<le> y}
[PROOF STEP]
using assms(1, 2) less
[PROOF STATE]
proof (prove)
using this:
x \<in> A
y \<in> A
x < y

goal (1 subgoal):
 1. {z \<in> A. z \<le> x} \<subset> {z \<in> A. z \<le> y}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
{z \<in> A. z \<le> x} \<subset> {z \<in> A. z \<le> y}

goal (3 subgoals):
 1. x < y \<Longrightarrow> x = y
 2. x = y \<Longrightarrow> x = y
 3. y < x \<Longrightarrow> x = y
[PROOF STEP]
have 2: "card {z \<in> A. z \<le> x} < card {z \<in> A. z \<le> y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {z \<in> A. z \<le> x} < card {z \<in> A. z \<le> y}
[PROOF STEP]
using psubset_card_mono 0 1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?B; ?A \<subset> ?B\<rbrakk> \<Longrightarrow> card ?A < card ?B
finite {z \<in> A. z \<le> y}
{z \<in> A. z \<le> x} \<subset> {z \<in> A. z \<le> y}

goal (1 subgoal):
 1. card {z \<in> A. z \<le> x} < card {z \<in> A. z \<le> y}
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
card {z \<in> A. z \<le> x} < card {z \<in> A. z \<le> y}

goal (3 subgoals):
 1. x < y \<Longrightarrow> x = y
 2. x = y \<Longrightarrow> x = y
 3. y < x \<Longrightarrow> x = y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
using assms(3) 2
[PROOF STATE]
proof (prove)
using this:
card {z \<in> A. z \<le> x} = card {z \<in> A. z \<le> y}
card {z \<in> A. z \<le> x} < card {z \<in> A. z \<le> y}

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

goal (2 subgoals):
 1. x = y \<Longrightarrow> x = y
 2. y < x \<Longrightarrow> x = y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = y \<Longrightarrow> x = y
 2. y < x \<Longrightarrow> x = y
[PROOF STEP]
case equal
[PROOF STATE]
proof (state)
this:
x = y

goal (2 subgoals):
 1. x = y \<Longrightarrow> x = y
 2. y < x \<Longrightarrow> x = y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
using equal
[PROOF STATE]
proof (prove)
using this:
x = y

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

goal (1 subgoal):
 1. y < x \<Longrightarrow> x = y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y < x \<Longrightarrow> x = y
[PROOF STEP]
case greater
[PROOF STATE]
proof (state)
this:
y < x

goal (1 subgoal):
 1. y < x \<Longrightarrow> x = y
[PROOF STEP]
have 0: "finite {z \<in> A. z \<le> x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {z \<in> A. z \<le> x}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite {z \<in> A. z \<le> x}

goal (1 subgoal):
 1. y < x \<Longrightarrow> x = y
[PROOF STEP]
have 1: "{z \<in> A. z \<le> y} \<subset> {z \<in> A. z \<le> x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {z \<in> A. z \<le> y} \<subset> {z \<in> A. z \<le> x}
[PROOF STEP]
using assms(1, 2) greater
[PROOF STATE]
proof (prove)
using this:
x \<in> A
y \<in> A
y < x

goal (1 subgoal):
 1. {z \<in> A. z \<le> y} \<subset> {z \<in> A. z \<le> x}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
{z \<in> A. z \<le> y} \<subset> {z \<in> A. z \<le> x}

goal (1 subgoal):
 1. y < x \<Longrightarrow> x = y
[PROOF STEP]
have 2: "card {z \<in> A. z \<le> y} < card {z \<in> A. z \<le> x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {z \<in> A. z \<le> y} < card {z \<in> A. z \<le> x}
[PROOF STEP]
using psubset_card_mono 0 1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?B; ?A \<subset> ?B\<rbrakk> \<Longrightarrow> card ?A < card ?B
finite {z \<in> A. z \<le> x}
{z \<in> A. z \<le> y} \<subset> {z \<in> A. z \<le> x}

goal (1 subgoal):
 1. card {z \<in> A. z \<le> y} < card {z \<in> A. z \<le> x}
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
card {z \<in> A. z \<le> y} < card {z \<in> A. z \<le> x}

goal (1 subgoal):
 1. y < x \<Longrightarrow> x = y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
using assms(3) 2
[PROOF STATE]
proof (prove)
using this:
card {z \<in> A. z \<le> x} = card {z \<in> A. z \<le> y}
card {z \<in> A. z \<le> y} < card {z \<in> A. z \<le> x}

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nat_set_card_mono[simp]:
    fixes A :: "nat set"
    assumes "x \<in> A"
    shows "card {z \<in> A. z < x} < card {z \<in> A. z < y} \<longleftrightarrow> x < y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (card {z \<in> A. z < x} < card {z \<in> A. z < y}) = (x < y)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. card {z \<in> A. z < x} < card {z \<in> A. z < y} \<Longrightarrow> x < y
 2. x < y \<Longrightarrow> card {z \<in> A. z < x} < card {z \<in> A. z < y}
[PROOF STEP]
assume 1: "card {z \<in> A. z < x} < card {z \<in> A. z < y}"
[PROOF STATE]
proof (state)
this:
card {z \<in> A. z < x} < card {z \<in> A. z < y}

goal (2 subgoals):
 1. card {z \<in> A. z < x} < card {z \<in> A. z < y} \<Longrightarrow> x < y
 2. x < y \<Longrightarrow> card {z \<in> A. z < x} < card {z \<in> A. z < y}
[PROOF STEP]
show "x < y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < y
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> x < y \<Longrightarrow> False
[PROOF STEP]
assume 2: "\<not> x < y"
[PROOF STATE]
proof (state)
this:
\<not> x < y

goal (1 subgoal):
 1. \<not> x < y \<Longrightarrow> False
[PROOF STEP]
have 3: "card {z \<in> A. z < y} \<le> card {z \<in> A. z < x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {z \<in> A. z < y} \<le> card {z \<in> A. z < x}
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
\<not> x < y

goal (1 subgoal):
 1. card {z \<in> A. z < y} \<le> card {z \<in> A. z < x}
[PROOF STEP]
by (auto intro: card_mono)
[PROOF STATE]
proof (state)
this:
card {z \<in> A. z < y} \<le> card {z \<in> A. z < x}

goal (1 subgoal):
 1. \<not> x < y \<Longrightarrow> False
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
using 1 3
[PROOF STATE]
proof (prove)
using this:
card {z \<in> A. z < x} < card {z \<in> A. z < y}
card {z \<in> A. z < y} \<le> card {z \<in> A. z < x}

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x < y

goal (1 subgoal):
 1. x < y \<Longrightarrow> card {z \<in> A. z < x} < card {z \<in> A. z < y}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x < y \<Longrightarrow> card {z \<in> A. z < x} < card {z \<in> A. z < y}
[PROOF STEP]
assume 1: "x < y"
[PROOF STATE]
proof (state)
this:
x < y

goal (1 subgoal):
 1. x < y \<Longrightarrow> card {z \<in> A. z < x} < card {z \<in> A. z < y}
[PROOF STEP]
show "card {z \<in> A. z < x} < card {z \<in> A. z < y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {z \<in> A. z < x} < card {z \<in> A. z < y}
[PROOF STEP]
proof (intro psubset_card_mono psubsetI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. finite {z \<in> A. z < y}
 2. {z \<in> A. z < x} \<subseteq> {z \<in> A. z < y}
 3. {z \<in> A. z < x} \<noteq> {z \<in> A. z < y}
[PROOF STEP]
show "finite {z \<in> A. z < y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {z \<in> A. z < y}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite {z \<in> A. z < y}

goal (2 subgoals):
 1. {z \<in> A. z < x} \<subseteq> {z \<in> A. z < y}
 2. {z \<in> A. z < x} \<noteq> {z \<in> A. z < y}
[PROOF STEP]
show "{z \<in> A. z < x} \<subseteq> {z \<in> A. z < y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {z \<in> A. z < x} \<subseteq> {z \<in> A. z < y}
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
x < y

goal (1 subgoal):
 1. {z \<in> A. z < x} \<subseteq> {z \<in> A. z < y}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{z \<in> A. z < x} \<subseteq> {z \<in> A. z < y}

goal (1 subgoal):
 1. {z \<in> A. z < x} \<noteq> {z \<in> A. z < y}
[PROOF STEP]
show "{z \<in> A. z < x} \<noteq> {z \<in> A. z < y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {z \<in> A. z < x} \<noteq> {z \<in> A. z < y}
[PROOF STEP]
using assms 1
[PROOF STATE]
proof (prove)
using this:
x \<in> A
x < y

goal (1 subgoal):
 1. {z \<in> A. z < x} \<noteq> {z \<in> A. z < y}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{z \<in> A. z < x} \<noteq> {z \<in> A. z < y}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card {z \<in> A. z < x} < card {z \<in> A. z < y}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma card_one[elim]:
    assumes "card A = 1"
    obtains a
    where "A = {a}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a. A = {a} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
card A = 1

goal (1 subgoal):
 1. (\<And>a. A = {a} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis One_nat_def card_Suc_eq)


[STATEMENT]
lemma image_alt_def: "f ` A = {f x |x. x \<in> A}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` A = {f x |x. x \<in> A}
[PROOF STEP]
by auto


[STATEMENT]
lemma supset_mono_inductive[mono]:
    assumes "\<And> x. x \<in> B \<longrightarrow> x \<in> C"
    shows "A \<subseteq> B \<longrightarrow> A \<subseteq> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> B \<longrightarrow> A \<subseteq> C
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?x \<in> B \<longrightarrow> ?x \<in> C

goal (1 subgoal):
 1. A \<subseteq> B \<longrightarrow> A \<subseteq> C
[PROOF STEP]
by auto


[STATEMENT]
lemma Collect_mono_inductive[mono]:
    assumes "\<And> x. P x \<longrightarrow> Q x"
    shows "x \<in> {x. P x} \<longrightarrow> x \<in> {x. Q x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> {x. P x} \<longrightarrow> x \<in> {x. Q x}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P ?x \<longrightarrow> Q ?x

goal (1 subgoal):
 1. x \<in> {x. P x} \<longrightarrow> x \<in> {x. Q x}
[PROOF STEP]
by auto


[STATEMENT]
lemma image_union_split:
    assumes "f ` (A \<union> B) = g ` C"
    obtains D E
    where "f ` A = g ` D" "f ` B = g ` E" "D \<subseteq> C" "E \<subseteq> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>D E. \<lbrakk>f ` A = g ` D; f ` B = g ` E; D \<subseteq> C; E \<subseteq> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f ` (A \<union> B) = g ` C

goal (1 subgoal):
 1. (\<And>D E. \<lbrakk>f ` A = g ` D; f ` B = g ` E; D \<subseteq> C; E \<subseteq> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding image_Un
[PROOF STATE]
proof (prove)
using this:
f ` A \<union> f ` B = g ` C

goal (1 subgoal):
 1. (\<And>D E. \<lbrakk>f ` A = g ` D; f ` B = g ` E; D \<subseteq> C; E \<subseteq> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis (erased, lifting) inf_sup_ord(3) inf_sup_ord(4) subset_imageE)


[STATEMENT]
lemma image_insert_split:
    assumes "inj g" "f ` insert a B = g ` C"
    obtains d E
    where "f a = g d" "f ` B = g ` E" "d \<in> C" "E \<subseteq> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>d E. \<lbrakk>f a = g d; f ` B = g ` E; d \<in> C; E \<subseteq> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>d E. \<lbrakk>f a = g d; f ` B = g ` E; d \<in> C; E \<subseteq> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have 1: "f ` ({a} \<union> B) = g ` C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` ({a} \<union> B) = g ` C
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
f ` insert a B = g ` C

goal (1 subgoal):
 1. f ` ({a} \<union> B) = g ` C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f ` ({a} \<union> B) = g ` C

goal (1 subgoal):
 1. (\<And>d E. \<lbrakk>f a = g d; f ` B = g ` E; d \<in> C; E \<subseteq> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain D E where 2: "f ` {a} = g ` D" "f ` B = g ` E" "D \<subseteq> C" "E \<subseteq> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>D E. \<lbrakk>f ` {a} = g ` D; f ` B = g ` E; D \<subseteq> C; E \<subseteq> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using image_union_split 1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?f ` (?A \<union> ?B) = ?g ` ?C; \<And>D E. \<lbrakk>?f ` ?A = ?g ` D; ?f ` ?B = ?g ` E; D \<subseteq> ?C; E \<subseteq> ?C\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
f ` ({a} \<union> B) = g ` C

goal (1 subgoal):
 1. (\<And>D E. \<lbrakk>f ` {a} = g ` D; f ` B = g ` E; D \<subseteq> C; E \<subseteq> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
f ` {a} = g ` D
f ` B = g ` E
D \<subseteq> C
E \<subseteq> C

goal (1 subgoal):
 1. (\<And>d E. \<lbrakk>f a = g d; f ` B = g ` E; d \<in> C; E \<subseteq> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain d where 3: "D = {d}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>d. D = {d} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(1) 2(1)
[PROOF STATE]
proof (prove)
using this:
inj g
f ` {a} = g ` D

goal (1 subgoal):
 1. (\<And>d. D = {d} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto, metis (erased, opaque_lifting) imageE
      image_empty image_insert inj_image_eq_iff singletonI)
[PROOF STATE]
proof (state)
this:
D = {d}

goal (1 subgoal):
 1. (\<And>d E. \<lbrakk>f a = g d; f ` B = g ` E; d \<in> C; E \<subseteq> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that 2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>f a = g ?d; f ` B = g ` ?E; ?d \<in> C; ?E \<subseteq> C\<rbrakk> \<Longrightarrow> thesis
f ` {a} = g ` D
f ` B = g ` E
D \<subseteq> C
E \<subseteq> C

goal (1 subgoal):
 1. thesis
[PROOF STEP]
unfolding 3
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>f a = g ?d; f ` B = g ` ?E; ?d \<in> C; ?E \<subseteq> C\<rbrakk> \<Longrightarrow> thesis
f ` {a} = g ` {d}
f ` B = g ` E
{d} \<subseteq> C
E \<subseteq> C

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

goal:
No subgoals!
[PROOF STEP]
qed