[STATEMENT]
lemma vcard_Sup_le_cmult:
  assumes "small U" and \<kappa>: "\<And>x. x \<in> U \<Longrightarrow> vcard x \<le> \<kappa>"
  shows "vcard (\<Squnion>U) \<le> vcard (set U) \<otimes> \<kappa>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard (\<Squnion> U) \<le> vcard (set U) \<otimes> \<kappa>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vcard (\<Squnion> U) \<le> vcard (set U) \<otimes> \<kappa>
[PROOF STEP]
have "\<exists>f. f \<in> elts x \<rightarrow> elts \<kappa> \<and> inj_on f (elts x)" if "x \<in> U" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f. f \<in> elts x \<rightarrow> elts \<kappa> \<and> inj_on f (elts x)
[PROOF STEP]
using \<kappa> [OF that]
[PROOF STATE]
proof (prove)
using this:
vcard x \<le> \<kappa>

goal (1 subgoal):
 1. \<exists>f. f \<in> elts x \<rightarrow> elts \<kappa> \<and> inj_on f (elts x)
[PROOF STEP]
by (metis cardinal_le_lepoll image_subset_iff_funcset lepoll_def)
[PROOF STATE]
proof (state)
this:
?x \<in> U \<Longrightarrow> \<exists>f. f \<in> elts ?x \<rightarrow> elts \<kappa> \<and> inj_on f (elts ?x)

goal (1 subgoal):
 1. vcard (\<Squnion> U) \<le> vcard (set U) \<otimes> \<kappa>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x \<in> U \<Longrightarrow> \<exists>f. f \<in> elts ?x \<rightarrow> elts \<kappa> \<and> inj_on f (elts ?x)
[PROOF STEP]
obtain \<phi> where \<phi>: "\<And>x. x \<in> U \<Longrightarrow> (\<phi> x) \<in> elts x \<rightarrow> elts \<kappa> \<and> inj_on (\<phi> x) (elts x)"
[PROOF STATE]
proof (prove)
using this:
?x \<in> U \<Longrightarrow> \<exists>f. f \<in> elts ?x \<rightarrow> elts \<kappa> \<and> inj_on f (elts ?x)

goal (1 subgoal):
 1. (\<And>\<phi>. (\<And>x. x \<in> U \<Longrightarrow> \<phi> x \<in> elts x \<rightarrow> elts \<kappa> \<and> inj_on (\<phi> x) (elts x)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
?x \<in> U \<Longrightarrow> \<phi> ?x \<in> elts ?x \<rightarrow> elts \<kappa> \<and> inj_on (\<phi> ?x) (elts ?x)

goal (1 subgoal):
 1. vcard (\<Squnion> U) \<le> vcard (set U) \<otimes> \<kappa>
[PROOF STEP]
define u where "u \<equiv> \<lambda>y. @x. x \<in> U \<and> y \<in> elts x"
[PROOF STATE]
proof (state)
this:
u \<equiv> \<lambda>y. SOME x. x \<in> U \<and> y \<in> elts x

goal (1 subgoal):
 1. vcard (\<Squnion> U) \<le> vcard (set U) \<otimes> \<kappa>
[PROOF STEP]
have u: "u y \<in> U \<and> y \<in> elts (u y)" if "y \<in> \<Union>(elts ` U)" for y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u y \<in> U \<and> y \<in> elts (u y)
[PROOF STEP]
unfolding u_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SOME x. x \<in> U \<and> y \<in> elts x) \<in> U \<and> y \<in> elts (SOME x. x \<in> U \<and> y \<in> elts x)
[PROOF STEP]
by (metis (mono_tags, lifting)that someI2_ex UN_iff)
[PROOF STATE]
proof (state)
this:
?y \<in> \<Union> (elts ` U) \<Longrightarrow> u ?y \<in> U \<and> ?y \<in> elts (u ?y)

goal (1 subgoal):
 1. vcard (\<Squnion> U) \<le> vcard (set U) \<otimes> \<kappa>
[PROOF STEP]
define \<psi> where "\<psi> \<equiv> \<lambda>y. (u y, \<phi> (u y) y)"
[PROOF STATE]
proof (state)
this:
\<psi> \<equiv> \<lambda>y. (u y, \<phi> (u y) y)

goal (1 subgoal):
 1. vcard (\<Squnion> U) \<le> vcard (set U) \<otimes> \<kappa>
[PROOF STEP]
have U: "elts (vcard (set U)) \<approx> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts (vcard (set U)) \<approx> U
[PROOF STEP]
by (metis \<open>small U\<close> cardinal_eqpoll elts_of_set)
[PROOF STATE]
proof (state)
this:
elts (vcard (set U)) \<approx> U

goal (1 subgoal):
 1. vcard (\<Squnion> U) \<le> vcard (set U) \<otimes> \<kappa>
[PROOF STEP]
have "elts (\<Squnion>U) = \<Union>(elts ` U)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts (\<Squnion> U) = \<Union> (elts ` U)
[PROOF STEP]
using \<open>small U\<close>
[PROOF STATE]
proof (prove)
using this:
small U

goal (1 subgoal):
 1. elts (\<Squnion> U) = \<Union> (elts ` U)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
elts (\<Squnion> U) = \<Union> (elts ` U)

goal (1 subgoal):
 1. vcard (\<Squnion> U) \<le> vcard (set U) \<otimes> \<kappa>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
elts (\<Squnion> U) = \<Union> (elts ` U)

goal (1 subgoal):
 1. vcard (\<Squnion> U) \<le> vcard (set U) \<otimes> \<kappa>
[PROOF STEP]
have "\<dots> \<lesssim> U \<times> elts \<kappa>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (elts ` U) \<lesssim> U \<times> elts \<kappa>
[PROOF STEP]
unfolding lepoll_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f. inj_on f (\<Union> (elts ` U)) \<and> f ` \<Union> (elts ` U) \<subseteq> U \<times> elts \<kappa>
[PROOF STEP]
proof (intro exI conjI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. inj_on ?f (\<Union> (elts ` U))
 2. ?f ` \<Union> (elts ` U) \<subseteq> U \<times> elts \<kappa>
[PROOF STEP]
show "inj_on \<psi> (\<Union> (elts ` U))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on \<psi> (\<Union> (elts ` U))
[PROOF STEP]
using \<phi> u
[PROOF STATE]
proof (prove)
using this:
?x \<in> U \<Longrightarrow> \<phi> ?x \<in> elts ?x \<rightarrow> elts \<kappa> \<and> inj_on (\<phi> ?x) (elts ?x)
?y \<in> \<Union> (elts ` U) \<Longrightarrow> u ?y \<in> U \<and> ?y \<in> elts (u ?y)

goal (1 subgoal):
 1. inj_on \<psi> (\<Union> (elts ` U))
[PROOF STEP]
by (smt (verit) \<psi>_def inj_on_def prod.inject)
[PROOF STATE]
proof (state)
this:
inj_on \<psi> (\<Union> (elts ` U))

goal (1 subgoal):
 1. \<psi> ` \<Union> (elts ` U) \<subseteq> U \<times> elts \<kappa>
[PROOF STEP]
show "\<psi> ` \<Union> (elts ` U) \<subseteq> U \<times> elts \<kappa>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<psi> ` \<Union> (elts ` U) \<subseteq> U \<times> elts \<kappa>
[PROOF STEP]
using \<phi> u
[PROOF STATE]
proof (prove)
using this:
?x \<in> U \<Longrightarrow> \<phi> ?x \<in> elts ?x \<rightarrow> elts \<kappa> \<and> inj_on (\<phi> ?x) (elts ?x)
?y \<in> \<Union> (elts ` U) \<Longrightarrow> u ?y \<in> U \<and> ?y \<in> elts (u ?y)

goal (1 subgoal):
 1. \<psi> ` \<Union> (elts ` U) \<subseteq> U \<times> elts \<kappa>
[PROOF STEP]
by (auto simp: \<psi>_def)
[PROOF STATE]
proof (state)
this:
\<psi> ` \<Union> (elts ` U) \<subseteq> U \<times> elts \<kappa>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Union> (elts ` U) \<lesssim> U \<times> elts \<kappa>

goal (1 subgoal):
 1. vcard (\<Squnion> U) \<le> vcard (set U) \<otimes> \<kappa>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Union> (elts ` U) \<lesssim> U \<times> elts \<kappa>

goal (1 subgoal):
 1. vcard (\<Squnion> U) \<le> vcard (set U) \<otimes> \<kappa>
[PROOF STEP]
have "\<dots>  \<approx> elts (vcard (set U) \<otimes> \<kappa>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. U \<times> elts \<kappa> \<approx> elts (vcard (set U) \<otimes> \<kappa>)
[PROOF STEP]
using U elts_cmult eqpoll_sym eqpoll_trans times_eqpoll_cong
[PROOF STATE]
proof (prove)
using this:
elts (vcard (set U)) \<approx> U
elts (?\<kappa>' \<otimes> ?\<kappa>) \<approx> elts ?\<kappa>' \<times> elts ?\<kappa>
?A \<approx> ?B \<Longrightarrow> ?B \<approx> ?A
\<lbrakk>?A \<approx> ?B; ?B \<approx> ?C\<rbrakk> \<Longrightarrow> ?A \<approx> ?C
\<lbrakk>?A \<approx> ?C; ?B \<approx> ?D\<rbrakk> \<Longrightarrow> ?A \<times> ?B \<approx> ?C \<times> ?D

goal (1 subgoal):
 1. U \<times> elts \<kappa> \<approx> elts (vcard (set U) \<otimes> \<kappa>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
U \<times> elts \<kappa> \<approx> elts (vcard (set U) \<otimes> \<kappa>)

goal (1 subgoal):
 1. vcard (\<Squnion> U) \<le> vcard (set U) \<otimes> \<kappa>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
elts (\<Squnion> U) \<lesssim> elts (vcard (set U) \<otimes> \<kappa>)
[PROOF STEP]
have "elts (\<Squnion> U) \<lesssim> elts (vcard (set U) \<otimes> \<kappa>)"
[PROOF STATE]
proof (prove)
using this:
elts (\<Squnion> U) \<lesssim> elts (vcard (set U) \<otimes> \<kappa>)

goal (1 subgoal):
 1. elts (\<Squnion> U) \<lesssim> elts (vcard (set U) \<otimes> \<kappa>)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
elts (\<Squnion> U) \<lesssim> elts (vcard (set U) \<otimes> \<kappa>)

goal (1 subgoal):
 1. vcard (\<Squnion> U) \<le> vcard (set U) \<otimes> \<kappa>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
elts (\<Squnion> U) \<lesssim> elts (vcard (set U) \<otimes> \<kappa>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
elts (\<Squnion> U) \<lesssim> elts (vcard (set U) \<otimes> \<kappa>)

goal (1 subgoal):
 1. vcard (\<Squnion> U) \<le> vcard (set U) \<otimes> \<kappa>
[PROOF STEP]
by (simp add: cmult_def lepoll_cardinal_le)
[PROOF STATE]
proof (state)
this:
vcard (\<Squnion> U) \<le> vcard (set U) \<otimes> \<kappa>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma succ_lepoll_succD: "elts (succ(m)) \<lesssim> elts (succ(n)) \<Longrightarrow> elts m \<lesssim> elts n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts (ZFC_in_HOL.succ m) \<lesssim> elts (ZFC_in_HOL.succ n) \<Longrightarrow> elts m \<lesssim> elts n
[PROOF STEP]
by (simp add: insert_lepoll_insertD)


[STATEMENT]
lemma succ_eqpoll_cong: "elts a \<approx> elts b \<Longrightarrow> elts (succ(a)) \<approx> elts (succ(b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts a \<approx> elts b \<Longrightarrow> elts (ZFC_in_HOL.succ a) \<approx> elts (ZFC_in_HOL.succ b)
[PROOF STEP]
by (simp add: succ_def insert_eqpoll_cong)


[STATEMENT]
lemma sum_succ_eqpoll: "elts (succ a \<Uplus> b) \<approx> elts (succ(a\<Uplus>b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts (ZFC_in_HOL.succ a \<Uplus> b) \<approx> elts (ZFC_in_HOL.succ (a \<Uplus> b))
[PROOF STEP]
unfolding eqpoll_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f. bij_betw f (elts (ZFC_in_HOL.succ a \<Uplus> b)) (elts (ZFC_in_HOL.succ (a \<Uplus> b)))
[PROOF STEP]
proof (rule exI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bij_betw ?f (elts (ZFC_in_HOL.succ a \<Uplus> b)) (elts (ZFC_in_HOL.succ (a \<Uplus> b)))
[PROOF STEP]
let ?f = "\<lambda>z. if z=Inl a then a\<Uplus>b else z"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bij_betw ?f (elts (ZFC_in_HOL.succ a \<Uplus> b)) (elts (ZFC_in_HOL.succ (a \<Uplus> b)))
[PROOF STEP]
let ?g = "\<lambda>z. if z=a\<Uplus>b then Inl a else z"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bij_betw ?f (elts (ZFC_in_HOL.succ a \<Uplus> b)) (elts (ZFC_in_HOL.succ (a \<Uplus> b)))
[PROOF STEP]
show "bij_betw ?f (elts (succ a \<Uplus> b)) (elts (succ (a \<Uplus> b)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (\<lambda>z. if z = ZFC_Cardinals.Inl a then a \<Uplus> b else z) (elts (ZFC_in_HOL.succ a \<Uplus> b)) (elts (ZFC_in_HOL.succ (a \<Uplus> b)))
[PROOF STEP]
apply (rule bij_betw_byWitness [where f' = ?g], auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>a \<Uplus> b = ZFC_Cardinals.Inl x; x \<in> elts a\<rbrakk> \<Longrightarrow> x = a
 2. \<And>y. \<lbrakk>y \<in> elts b; a \<Uplus> b = ZFC_Cardinals.Inr y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis Inl_in_sum_iff mem_not_refl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>y \<in> elts b; a \<Uplus> b = ZFC_Cardinals.Inr y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (metis Inr_in_sum_iff mem_not_refl)
[PROOF STATE]
proof (state)
this:
bij_betw (\<lambda>z. if z = ZFC_Cardinals.Inl a then a \<Uplus> b else z) (elts (ZFC_in_HOL.succ a \<Uplus> b)) (elts (ZFC_in_HOL.succ (a \<Uplus> b)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cadd_succ: "succ m \<oplus> n = vcard (succ(m \<oplus> n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ZFC_in_HOL.succ m \<oplus> n = vcard (ZFC_in_HOL.succ (m \<oplus> n))
[PROOF STEP]
proof (unfold cadd_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vcard (ZFC_in_HOL.succ m \<Uplus> n) = vcard (ZFC_in_HOL.succ (vcard (m \<Uplus> n)))
[PROOF STEP]
have [intro]: "elts (m \<Uplus> n) \<approx> elts (vcard (m \<Uplus> n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts (m \<Uplus> n) \<approx> elts (vcard (m \<Uplus> n))
[PROOF STEP]
using cardinal_eqpoll eqpoll_sym
[PROOF STATE]
proof (prove)
using this:
elts (vcard ?a) \<approx> elts ?a
?A \<approx> ?B \<Longrightarrow> ?B \<approx> ?A

goal (1 subgoal):
 1. elts (m \<Uplus> n) \<approx> elts (vcard (m \<Uplus> n))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
elts (m \<Uplus> n) \<approx> elts (vcard (m \<Uplus> n))

goal (1 subgoal):
 1. vcard (ZFC_in_HOL.succ m \<Uplus> n) = vcard (ZFC_in_HOL.succ (vcard (m \<Uplus> n)))
[PROOF STEP]
have "vcard (succ m \<Uplus> n) = vcard (succ(m \<Uplus> n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard (ZFC_in_HOL.succ m \<Uplus> n) = vcard (ZFC_in_HOL.succ (m \<Uplus> n))
[PROOF STEP]
by (rule sum_succ_eqpoll [THEN cardinal_cong])
[PROOF STATE]
proof (state)
this:
vcard (ZFC_in_HOL.succ m \<Uplus> n) = vcard (ZFC_in_HOL.succ (m \<Uplus> n))

goal (1 subgoal):
 1. vcard (ZFC_in_HOL.succ m \<Uplus> n) = vcard (ZFC_in_HOL.succ (vcard (m \<Uplus> n)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
vcard (ZFC_in_HOL.succ m \<Uplus> n) = vcard (ZFC_in_HOL.succ (m \<Uplus> n))

goal (1 subgoal):
 1. vcard (ZFC_in_HOL.succ m \<Uplus> n) = vcard (ZFC_in_HOL.succ (vcard (m \<Uplus> n)))
[PROOF STEP]
have "\<dots> = vcard (succ(vcard (m \<Uplus> n)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard (ZFC_in_HOL.succ (m \<Uplus> n)) = vcard (ZFC_in_HOL.succ (vcard (m \<Uplus> n)))
[PROOF STEP]
by (blast intro: succ_eqpoll_cong cardinal_cong)
[PROOF STATE]
proof (state)
this:
vcard (ZFC_in_HOL.succ (m \<Uplus> n)) = vcard (ZFC_in_HOL.succ (vcard (m \<Uplus> n)))

goal (1 subgoal):
 1. vcard (ZFC_in_HOL.succ m \<Uplus> n) = vcard (ZFC_in_HOL.succ (vcard (m \<Uplus> n)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
vcard (ZFC_in_HOL.succ m \<Uplus> n) = vcard (ZFC_in_HOL.succ (vcard (m \<Uplus> n)))
[PROOF STEP]
show "vcard (succ m \<Uplus> n) = vcard (succ(vcard (m \<Uplus> n)))"
[PROOF STATE]
proof (prove)
using this:
vcard (ZFC_in_HOL.succ m \<Uplus> n) = vcard (ZFC_in_HOL.succ (vcard (m \<Uplus> n)))

goal (1 subgoal):
 1. vcard (ZFC_in_HOL.succ m \<Uplus> n) = vcard (ZFC_in_HOL.succ (vcard (m \<Uplus> n)))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
vcard (ZFC_in_HOL.succ m \<Uplus> n) = vcard (ZFC_in_HOL.succ (vcard (m \<Uplus> n)))

goal:
No subgoals!
[PROOF STEP]
qed


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

goal (2 subgoals):
 1. ord_of_nat 0 \<oplus> ord_of_nat n = ord_of_nat (0 + n)
 2. \<And>m. ord_of_nat m \<oplus> ord_of_nat n = ord_of_nat (m + n) \<Longrightarrow> ord_of_nat (Suc m) \<oplus> ord_of_nat n = ord_of_nat (Suc m + n)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
ord_of_nat m \<oplus> ord_of_nat n = ord_of_nat (m + n)

goal (1 subgoal):
 1. ord_of_nat (Suc m) \<oplus> ord_of_nat n = ord_of_nat (Suc m + n)
[PROOF STEP]
by (metis Card_def Card_ord_of_nat add_Suc cadd_succ ord_of_nat.simps(2))
[PROOF STATE]
proof (state)
this:
ord_of_nat (Suc m) \<oplus> ord_of_nat n = ord_of_nat (Suc m + n)

goal (1 subgoal):
 1. ord_of_nat 0 \<oplus> ord_of_nat n = ord_of_nat (0 + n)
[PROOF STEP]
qed auto


[STATEMENT]
lemma vcard_disjoint_sup:
  assumes "x \<sqinter> y = 0" shows "vcard (x \<squnion> y) = vcard x \<oplus> vcard y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard (x \<squnion> y) = vcard x \<oplus> vcard y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vcard (x \<squnion> y) = vcard x \<oplus> vcard y
[PROOF STEP]
have "elts (x \<squnion> y) \<approx> elts (x \<Uplus> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts (x \<squnion> y) \<approx> elts (x \<Uplus> y)
[PROOF STEP]
unfolding eqpoll_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f. bij_betw f (elts (x \<squnion> y)) (elts (x \<Uplus> y))
[PROOF STEP]
proof (rule exI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bij_betw ?f (elts (x \<squnion> y)) (elts (x \<Uplus> y))
[PROOF STEP]
let ?f = "\<lambda>z. if z \<in> elts x then Inl z else Inr z"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bij_betw ?f (elts (x \<squnion> y)) (elts (x \<Uplus> y))
[PROOF STEP]
let ?g = "sum_case id id"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bij_betw ?f (elts (x \<squnion> y)) (elts (x \<Uplus> y))
[PROOF STEP]
show "bij_betw ?f (elts (x \<squnion> y)) (elts (x \<Uplus> y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (\<lambda>z. if z \<in> elts x then ZFC_Cardinals.Inl z else ZFC_Cardinals.Inr z) (elts (x \<squnion> y)) (elts (x \<Uplus> y))
[PROOF STEP]
by (rule bij_betw_byWitness [where f' = ?g]) (use assms V_disjoint_iff in auto)
[PROOF STATE]
proof (state)
this:
bij_betw (\<lambda>z. if z \<in> elts x then ZFC_Cardinals.Inl z else ZFC_Cardinals.Inr z) (elts (x \<squnion> y)) (elts (x \<Uplus> y))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
elts (x \<squnion> y) \<approx> elts (x \<Uplus> y)

goal (1 subgoal):
 1. vcard (x \<squnion> y) = vcard x \<oplus> vcard y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
elts (x \<squnion> y) \<approx> elts (x \<Uplus> y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
elts (x \<squnion> y) \<approx> elts (x \<Uplus> y)

goal (1 subgoal):
 1. vcard (x \<squnion> y) = vcard x \<oplus> vcard y
[PROOF STEP]
by (metis cadd_commute cadd_def cardinal_cong cardinal_idem vsum_0_eqpoll cadd_assoc)
[PROOF STATE]
proof (state)
this:
vcard (x \<squnion> y) = vcard x \<oplus> vcard y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vcard_sup: "vcard (x \<squnion> y) \<le> vcard x \<oplus> vcard y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard (x \<squnion> y) \<le> vcard x \<oplus> vcard y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vcard (x \<squnion> y) \<le> vcard x \<oplus> vcard y
[PROOF STEP]
have "elts (x \<squnion> y) \<lesssim> elts (x \<Uplus> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts (x \<squnion> y) \<lesssim> elts (x \<Uplus> y)
[PROOF STEP]
unfolding lepoll_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f. inj_on f (elts (x \<squnion> y)) \<and> f ` elts (x \<squnion> y) \<subseteq> elts (x \<Uplus> y)
[PROOF STEP]
proof (intro exI conjI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. inj_on ?f (elts (x \<squnion> y))
 2. ?f ` elts (x \<squnion> y) \<subseteq> elts (x \<Uplus> y)
[PROOF STEP]
let ?f = "\<lambda>z. if z \<in> elts x then Inl z else Inr z"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. inj_on ?f (elts (x \<squnion> y))
 2. ?f ` elts (x \<squnion> y) \<subseteq> elts (x \<Uplus> y)
[PROOF STEP]
show "inj_on ?f (elts (x \<squnion> y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (\<lambda>z. if z \<in> elts x then ZFC_Cardinals.Inl z else ZFC_Cardinals.Inr z) (elts (x \<squnion> y))
[PROOF STEP]
by (simp add: inj_on_def)
[PROOF STATE]
proof (state)
this:
inj_on (\<lambda>z. if z \<in> elts x then ZFC_Cardinals.Inl z else ZFC_Cardinals.Inr z) (elts (x \<squnion> y))

goal (1 subgoal):
 1. (\<lambda>z. if z \<in> elts x then ZFC_Cardinals.Inl z else ZFC_Cardinals.Inr z) ` elts (x \<squnion> y) \<subseteq> elts (x \<Uplus> y)
[PROOF STEP]
show "?f ` elts (x \<squnion> y) \<subseteq> elts (x \<Uplus> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>z. if z \<in> elts x then ZFC_Cardinals.Inl z else ZFC_Cardinals.Inr z) ` elts (x \<squnion> y) \<subseteq> elts (x \<Uplus> y)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(\<lambda>z. if z \<in> elts x then ZFC_Cardinals.Inl z else ZFC_Cardinals.Inr z) ` elts (x \<squnion> y) \<subseteq> elts (x \<Uplus> y)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
elts (x \<squnion> y) \<lesssim> elts (x \<Uplus> y)

goal (1 subgoal):
 1. vcard (x \<squnion> y) \<le> vcard x \<oplus> vcard y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
elts (x \<squnion> y) \<lesssim> elts (x \<Uplus> y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
elts (x \<squnion> y) \<lesssim> elts (x \<Uplus> y)

goal (1 subgoal):
 1. vcard (x \<squnion> y) \<le> vcard x \<oplus> vcard y
[PROOF STEP]
using cadd_ac
[PROOF STATE]
proof (prove)
using this:
elts (x \<squnion> y) \<lesssim> elts (x \<Uplus> y)
?i \<oplus> ?j \<oplus> ?k = ?i \<oplus> (?j \<oplus> ?k)
?i \<oplus> ?j = ?j \<oplus> ?i
?j \<oplus> (?i \<oplus> ?k) = ?i \<oplus> (?j \<oplus> ?k)

goal (1 subgoal):
 1. vcard (x \<squnion> y) \<le> vcard x \<oplus> vcard y
[PROOF STEP]
by (metis cadd_def cardinal_cong cardinal_idem lepoll_imp_Card_le vsum_0_eqpoll)
[PROOF STATE]
proof (state)
this:
vcard (x \<squnion> y) \<le> vcard x \<oplus> vcard y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma InfCard_iff: "InfCard \<kappa> \<longleftrightarrow> Card \<kappa> \<and> infinite (elts \<kappa>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InfCard \<kappa> = (Card \<kappa> \<and> infinite (elts \<kappa>))
[PROOF STEP]
proof (cases "\<omega> \<le> \<kappa>")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<omega> \<le> \<kappa> \<Longrightarrow> InfCard \<kappa> = (Card \<kappa> \<and> infinite (elts \<kappa>))
 2. \<not> \<omega> \<le> \<kappa> \<Longrightarrow> InfCard \<kappa> = (Card \<kappa> \<and> infinite (elts \<kappa>))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<omega> \<le> \<kappa>

goal (2 subgoals):
 1. \<omega> \<le> \<kappa> \<Longrightarrow> InfCard \<kappa> = (Card \<kappa> \<and> infinite (elts \<kappa>))
 2. \<not> \<omega> \<le> \<kappa> \<Longrightarrow> InfCard \<kappa> = (Card \<kappa> \<and> infinite (elts \<kappa>))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<omega> \<le> \<kappa>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<omega> \<le> \<kappa>

goal (1 subgoal):
 1. InfCard \<kappa> = (Card \<kappa> \<and> infinite (elts \<kappa>))
[PROOF STEP]
using inj_ord_of_nat lepoll_def less_eq_V_def
[PROOF STATE]
proof (prove)
using this:
\<omega> \<le> \<kappa>
inj ord_of_nat
?A \<lesssim> ?B \<equiv> \<exists>f. inj_on f ?A \<and> f ` ?A \<subseteq> ?B
?x \<le> ?y \<equiv> elts ?x \<subseteq> elts ?y

goal (1 subgoal):
 1. InfCard \<kappa> = (Card \<kappa> \<and> infinite (elts \<kappa>))
[PROOF STEP]
by (auto simp: InfCard_def \<omega>_def infinite_le_lepoll)
[PROOF STATE]
proof (state)
this:
InfCard \<kappa> = (Card \<kappa> \<and> infinite (elts \<kappa>))

goal (1 subgoal):
 1. \<not> \<omega> \<le> \<kappa> \<Longrightarrow> InfCard \<kappa> = (Card \<kappa> \<and> infinite (elts \<kappa>))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> \<omega> \<le> \<kappa> \<Longrightarrow> InfCard \<kappa> = (Card \<kappa> \<and> infinite (elts \<kappa>))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> \<omega> \<le> \<kappa>

goal (1 subgoal):
 1. \<not> \<omega> \<le> \<kappa> \<Longrightarrow> InfCard \<kappa> = (Card \<kappa> \<and> infinite (elts \<kappa>))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> \<omega> \<le> \<kappa>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> \<omega> \<le> \<kappa>

goal (1 subgoal):
 1. InfCard \<kappa> = (Card \<kappa> \<and> infinite (elts \<kappa>))
[PROOF STEP]
using Card_iff_initial InfCard_def infinite_Ord_omega
[PROOF STATE]
proof (prove)
using this:
\<not> \<omega> \<le> \<kappa>
Card ?\<kappa> = (Ord ?\<kappa> \<and> (\<forall>\<alpha>. Ord \<alpha> \<and> \<alpha> < ?\<kappa> \<longrightarrow> \<not> elts \<alpha> \<approx> elts ?\<kappa>))
InfCard ?\<kappa> \<equiv> Card ?\<kappa> \<and> \<omega> \<le> ?\<kappa>
\<lbrakk>Ord ?\<alpha>; infinite (elts ?\<alpha>)\<rbrakk> \<Longrightarrow> \<omega> \<le> ?\<alpha>

goal (1 subgoal):
 1. InfCard \<kappa> = (Card \<kappa> \<and> infinite (elts \<kappa>))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
InfCard \<kappa> = (Card \<kappa> \<and> infinite (elts \<kappa>))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma InfCard_ge_ord_of_nat:
  assumes "InfCard \<kappa>" shows "ord_of_nat n \<le> \<kappa>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ord_of_nat n \<le> \<kappa>
[PROOF STEP]
using InfCard_def assms ord_of_nat_le_omega
[PROOF STATE]
proof (prove)
using this:
InfCard ?\<kappa> \<equiv> Card ?\<kappa> \<and> \<omega> \<le> ?\<kappa>
InfCard \<kappa>
ord_of_nat ?n \<le> \<omega>

goal (1 subgoal):
 1. ord_of_nat n \<le> \<kappa>
[PROOF STEP]
by blast


[STATEMENT]
lemma InfCard_not_0[iff]: "\<not> InfCard 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> InfCard 0
[PROOF STEP]
by (simp add: InfCard_iff)


[STATEMENT]
lemma less_vcard_VPow: "vcard A < vcard (VPow A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard A < vcard (VPow A)
[PROOF STEP]
proof (rule lesspoll_imp_Card_less)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. elts A \<prec> elts (VPow A)
[PROOF STEP]
show "elts A \<prec> elts (VPow A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts A \<prec> elts (VPow A)
[PROOF STEP]
by (simp add: elts_VPow down inj_on_def lesspoll_Pow_self)
[PROOF STATE]
proof (state)
this:
elts A \<prec> elts (VPow A)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma greater_Card:
  assumes "Card \<kappa>" shows "\<kappa> < vcard (VPow \<kappa>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<kappa> < vcard (VPow \<kappa>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<kappa> < vcard (VPow \<kappa>)
[PROOF STEP]
have "\<kappa> = vcard \<kappa>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<kappa> = vcard \<kappa>
[PROOF STEP]
using Card_def assms
[PROOF STATE]
proof (prove)
using this:
Card ?i \<equiv> ?i = vcard ?i
Card \<kappa>

goal (1 subgoal):
 1. \<kappa> = vcard \<kappa>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<kappa> = vcard \<kappa>

goal (1 subgoal):
 1. \<kappa> < vcard (VPow \<kappa>)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<kappa> = vcard \<kappa>

goal (1 subgoal):
 1. \<kappa> < vcard (VPow \<kappa>)
[PROOF STEP]
have "\<dots> < vcard (VPow \<kappa>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard \<kappa> < vcard (VPow \<kappa>)
[PROOF STEP]
proof (rule lesspoll_imp_Card_less)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. elts \<kappa> \<prec> elts (VPow \<kappa>)
[PROOF STEP]
show "elts \<kappa> \<prec> elts (VPow \<kappa>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts \<kappa> \<prec> elts (VPow \<kappa>)
[PROOF STEP]
by (simp add: elts_VPow down inj_on_def lesspoll_Pow_self)
[PROOF STATE]
proof (state)
this:
elts \<kappa> \<prec> elts (VPow \<kappa>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
vcard \<kappa> < vcard (VPow \<kappa>)

goal (1 subgoal):
 1. \<kappa> < vcard (VPow \<kappa>)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<kappa> < vcard (VPow \<kappa>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<kappa> < vcard (VPow \<kappa>)

goal (1 subgoal):
 1. \<kappa> < vcard (VPow \<kappa>)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<kappa> < vcard (VPow \<kappa>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma le_csucc:
  assumes "Card \<kappa>" shows "\<kappa> \<le> csucc \<kappa>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<kappa> \<le> csucc \<kappa>
[PROOF STEP]
by (simp add: assms less_csucc less_imp_le)


[STATEMENT]
lemma csucc_le: "\<lbrakk>Card \<mu>; \<kappa> \<in> elts \<mu>\<rbrakk> \<Longrightarrow> csucc \<kappa> \<le> \<mu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Card \<mu>; \<kappa> \<in> elts \<mu>\<rbrakk> \<Longrightarrow> csucc \<kappa> \<le> \<mu>
[PROOF STEP]
unfolding csucc_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Card \<mu>; \<kappa> \<in> elts \<mu>\<rbrakk> \<Longrightarrow> (LEAST \<kappa>'. Ord \<kappa>' \<and> Card \<kappa>' \<and> \<kappa> < \<kappa>') \<le> \<mu>
[PROOF STEP]
by (simp add: Card_is_Ord Ord_Least_le OrdmemD)


[STATEMENT]
lemma finite_csucc: "a \<in> elts \<omega> \<Longrightarrow> csucc a = succ a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> elts \<omega> \<Longrightarrow> csucc a = ZFC_in_HOL.succ a
[PROOF STEP]
unfolding csucc_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> elts \<omega> \<Longrightarrow> (LEAST \<kappa>'. Ord \<kappa>' \<and> Card \<kappa>' \<and> a < \<kappa>') = ZFC_in_HOL.succ a
[PROOF STEP]
proof (rule Least_equality)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a \<in> elts \<omega> \<Longrightarrow> Ord (ZFC_in_HOL.succ a) \<and> Card (ZFC_in_HOL.succ a) \<and> a < ZFC_in_HOL.succ a
 2. \<And>y. \<lbrakk>a \<in> elts \<omega>; Ord y \<and> Card y \<and> a < y\<rbrakk> \<Longrightarrow> ZFC_in_HOL.succ a \<le> y
[PROOF STEP]
show "Ord (ZFC_in_HOL.succ a) \<and> Card (ZFC_in_HOL.succ a) \<and> a < ZFC_in_HOL.succ a"
    if "a \<in> elts \<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ord (ZFC_in_HOL.succ a) \<and> Card (ZFC_in_HOL.succ a) \<and> a < ZFC_in_HOL.succ a
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
a \<in> elts \<omega>

goal (1 subgoal):
 1. Ord (ZFC_in_HOL.succ a) \<and> Card (ZFC_in_HOL.succ a) \<and> a < ZFC_in_HOL.succ a
[PROOF STEP]
by (auto simp: less_V_def less_eq_V_def nat_into_Card)
[PROOF STATE]
proof (state)
this:
a \<in> elts \<omega> \<Longrightarrow> Ord (ZFC_in_HOL.succ a) \<and> Card (ZFC_in_HOL.succ a) \<and> a < ZFC_in_HOL.succ a

goal (1 subgoal):
 1. \<And>y. \<lbrakk>a \<in> elts \<omega>; Ord y \<and> Card y \<and> a < y\<rbrakk> \<Longrightarrow> ZFC_in_HOL.succ a \<le> y
[PROOF STEP]
show "ZFC_in_HOL.succ a \<le> y"
    if "a \<in> elts \<omega>"
      and "Ord y \<and> Card y \<and> a < y"
    for y :: V
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ZFC_in_HOL.succ a \<le> y
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
a \<in> elts \<omega>
Ord y \<and> Card y \<and> a < y

goal (1 subgoal):
 1. ZFC_in_HOL.succ a \<le> y
[PROOF STEP]
using Ord_mem_iff_lt dual_order.strict_implies_order
[PROOF STATE]
proof (prove)
using this:
a \<in> elts \<omega>
Ord y \<and> Card y \<and> a < y
\<lbrakk>Ord ?k; Ord ?l\<rbrakk> \<Longrightarrow> (?k \<in> elts ?l) = (?k < ?l)
?b < ?a \<Longrightarrow> ?b \<le> ?a

goal (1 subgoal):
 1. ZFC_in_HOL.succ a \<le> y
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<lbrakk>a \<in> elts \<omega>; Ord ?y \<and> Card ?y \<and> a < ?y\<rbrakk> \<Longrightarrow> ZFC_in_HOL.succ a \<le> ?y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Finite_imp_cardinal_cons [simp]:
  assumes FA: "finite A" and a: "a \<notin> A"
  shows "vcard (set (insert a A)) = csucc(vcard (set A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard (set (insert a A)) = csucc (vcard (set A))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vcard (set (insert a A)) = csucc (vcard (set A))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard (set (insert a A)) = csucc (vcard (set A))
[PROOF STEP]
unfolding csucc_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard (set (insert a A)) = (LEAST \<kappa>'. Ord \<kappa>' \<and> Card \<kappa>' \<and> vcard (set A) < \<kappa>')
[PROOF STEP]
proof (rule Least_equality [THEN sym])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Ord (vcard (set (insert a A))) \<and> Card (vcard (set (insert a A))) \<and> vcard (set A) < vcard (set (insert a A))
 2. \<And>y. Ord y \<and> Card y \<and> vcard (set A) < y \<Longrightarrow> vcard (set (insert a A)) \<le> y
[PROOF STEP]
have "small A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. small A
[PROOF STEP]
by (simp add: FA Finite_V)
[PROOF STATE]
proof (state)
this:
small A

goal (2 subgoals):
 1. Ord (vcard (set (insert a A))) \<and> Card (vcard (set (insert a A))) \<and> vcard (set A) < vcard (set (insert a A))
 2. \<And>y. Ord y \<and> Card y \<and> vcard (set A) < y \<Longrightarrow> vcard (set (insert a A)) \<le> y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
small A
[PROOF STEP]
have "\<not> elts (set A) \<approx> elts (set (insert a A))"
[PROOF STATE]
proof (prove)
using this:
small A

goal (1 subgoal):
 1. \<not> elts (set A) \<approx> elts (set (insert a A))
[PROOF STEP]
using FA a eqpoll_imp_lepoll eqpoll_sym finite_insert_lepoll
[PROOF STATE]
proof (prove)
using this:
small A
finite A
a \<notin> A
?A \<approx> ?B \<Longrightarrow> ?A \<lesssim> ?B
?A \<approx> ?B \<Longrightarrow> ?B \<approx> ?A
finite ?A \<Longrightarrow> (insert ?a ?A \<lesssim> ?A) = (?a \<in> ?A)

goal (1 subgoal):
 1. \<not> elts (set A) \<approx> elts (set (insert a A))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<not> elts (set A) \<approx> elts (set (insert a A))

goal (2 subgoals):
 1. Ord (vcard (set (insert a A))) \<and> Card (vcard (set (insert a A))) \<and> vcard (set A) < vcard (set (insert a A))
 2. \<And>y. Ord y \<and> Card y \<and> vcard (set A) < y \<Longrightarrow> vcard (set (insert a A)) \<le> y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> elts (set A) \<approx> elts (set (insert a A))
[PROOF STEP]
show "Ord (vcard (set (insert a A))) \<and> Card (vcard (set (insert a A))) \<and> vcard (set A) < vcard (set (insert a A))"
[PROOF STATE]
proof (prove)
using this:
\<not> elts (set A) \<approx> elts (set (insert a A))

goal (1 subgoal):
 1. Ord (vcard (set (insert a A))) \<and> Card (vcard (set (insert a A))) \<and> vcard (set A) < vcard (set (insert a A))
[PROOF STEP]
by (simp add: Card_def lesspoll_imp_Card_less lesspoll_def subset_imp_lepoll subset_insertI)
[PROOF STATE]
proof (state)
this:
Ord (vcard (set (insert a A))) \<and> Card (vcard (set (insert a A))) \<and> vcard (set A) < vcard (set (insert a A))

goal (1 subgoal):
 1. \<And>y. Ord y \<and> Card y \<and> vcard (set A) < y \<Longrightarrow> vcard (set (insert a A)) \<le> y
[PROOF STEP]
show "vcard (set (insert a A)) \<le> i"
      if "Ord i \<and> Card i \<and> vcard (set A) < i" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard (set (insert a A)) \<le> i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vcard (set (insert a A)) \<le> i
[PROOF STEP]
have "elts (vcard (set A)) \<approx> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts (vcard (set A)) \<approx> A
[PROOF STEP]
by (metis FA finite_imp_small cardinal_eqpoll elts_of_set)
[PROOF STATE]
proof (state)
this:
elts (vcard (set A)) \<approx> A

goal (1 subgoal):
 1. vcard (set (insert a A)) \<le> i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
elts (vcard (set A)) \<approx> A
[PROOF STEP]
have less: "A \<prec> elts i"
[PROOF STATE]
proof (prove)
using this:
elts (vcard (set A)) \<approx> A

goal (1 subgoal):
 1. A \<prec> elts i
[PROOF STEP]
using eq_lesspoll_trans eqpoll_sym lt_Card_imp_lesspoll that
[PROOF STATE]
proof (prove)
using this:
elts (vcard (set A)) \<approx> A
\<lbrakk>?X \<approx> ?Y; ?Y \<prec> ?Z\<rbrakk> \<Longrightarrow> ?X \<prec> ?Z
?A \<approx> ?B \<Longrightarrow> ?B \<approx> ?A
\<lbrakk>?i < ?a; Card ?a; Ord ?i\<rbrakk> \<Longrightarrow> elts ?i \<prec> elts ?a
Ord i \<and> Card i \<and> vcard (set A) < i

goal (1 subgoal):
 1. A \<prec> elts i
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
A \<prec> elts i

goal (1 subgoal):
 1. vcard (set (insert a A)) \<le> i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard (set (insert a A)) \<le> i
[PROOF STEP]
using that less
[PROOF STATE]
proof (prove)
using this:
Ord i \<and> Card i \<and> vcard (set A) < i
A \<prec> elts i

goal (1 subgoal):
 1. vcard (set (insert a A)) \<le> i
[PROOF STEP]
by (auto simp: less_imp_insert_lepoll lepoll_cardinal_le)
[PROOF STATE]
proof (state)
this:
vcard (set (insert a A)) \<le> i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Ord ?i \<and> Card ?i \<and> vcard (set A) < ?i \<Longrightarrow> vcard (set (insert a A)) \<le> ?i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
vcard (set (insert a A)) = csucc (vcard (set A))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vcard_finite_set: "finite A \<Longrightarrow> vcard (set A) = ord_of_nat (card A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite A \<Longrightarrow> vcard (set A) = ord_of_nat (card A)
[PROOF STEP]
by (induction A rule: finite_induct) (auto simp: set_empty \<omega>_def finite_csucc)


[STATEMENT]
lemma lt_csucc_iff:
  assumes "Ord \<alpha>" "Card \<kappa>"
  shows "\<alpha> < csucc \<kappa> \<longleftrightarrow> vcard \<alpha> \<le> \<kappa>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<alpha> < csucc \<kappa>) = (vcard \<alpha> \<le> \<kappa>)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<alpha> < csucc \<kappa> \<Longrightarrow> vcard \<alpha> \<le> \<kappa>
 2. vcard \<alpha> \<le> \<kappa> \<Longrightarrow> \<alpha> < csucc \<kappa>
[PROOF STEP]
show "vcard \<alpha> \<le> \<kappa>" if "\<alpha> < csucc \<kappa>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard \<alpha> \<le> \<kappa>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vcard \<alpha> \<le> \<kappa>
[PROOF STEP]
have "vcard \<alpha> \<le> csucc \<kappa>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard \<alpha> \<le> csucc \<kappa>
[PROOF STEP]
by (meson \<open>Ord \<alpha>\<close> dual_order.trans lepoll_cardinal_le lepoll_refl less_le_not_le that)
[PROOF STATE]
proof (state)
this:
vcard \<alpha> \<le> csucc \<kappa>

goal (1 subgoal):
 1. vcard \<alpha> \<le> \<kappa>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vcard \<alpha> \<le> csucc \<kappa>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
vcard \<alpha> \<le> csucc \<kappa>

goal (1 subgoal):
 1. vcard \<alpha> \<le> \<kappa>
[PROOF STEP]
by (metis (no_types) Card_def Card_iff_initial Ord_linear2 Ord_mem_iff_lt assms cardinal_eqpoll cardinal_idem csucc_le eq_iff eqpoll_sym that)
[PROOF STATE]
proof (state)
this:
vcard \<alpha> \<le> \<kappa>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<alpha> < csucc \<kappa> \<Longrightarrow> vcard \<alpha> \<le> \<kappa>

goal (1 subgoal):
 1. vcard \<alpha> \<le> \<kappa> \<Longrightarrow> \<alpha> < csucc \<kappa>
[PROOF STEP]
show "\<alpha> < csucc \<kappa>" if "vcard \<alpha> \<le> \<kappa>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> < csucc \<kappa>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<alpha> < csucc \<kappa>
[PROOF STEP]
have "\<not> csucc \<kappa> \<le> \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> csucc \<kappa> \<le> \<alpha>
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
vcard \<alpha> \<le> \<kappa>

goal (1 subgoal):
 1. \<not> csucc \<kappa> \<le> \<alpha>
[PROOF STEP]
by (metis Card_csucc Card_def assms(2) le_less_trans lepoll_imp_Card_le less_csucc less_eq_V_def less_le_not_le subset_imp_lepoll)
[PROOF STATE]
proof (state)
this:
\<not> csucc \<kappa> \<le> \<alpha>

goal (1 subgoal):
 1. \<alpha> < csucc \<kappa>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> csucc \<kappa> \<le> \<alpha>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> csucc \<kappa> \<le> \<alpha>

goal (1 subgoal):
 1. \<alpha> < csucc \<kappa>
[PROOF STEP]
by (meson Card_csucc Card_is_Ord Ord_linear2 assms)
[PROOF STATE]
proof (state)
this:
\<alpha> < csucc \<kappa>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
vcard \<alpha> \<le> \<kappa> \<Longrightarrow> \<alpha> < csucc \<kappa>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Card_lt_csucc_iff: "\<lbrakk>Card \<kappa>'; Card \<kappa>\<rbrakk> \<Longrightarrow> (\<kappa>' < csucc \<kappa>) = (\<kappa>' \<le> \<kappa>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Card \<kappa>'; Card \<kappa>\<rbrakk> \<Longrightarrow> (\<kappa>' < csucc \<kappa>) = (\<kappa>' \<le> \<kappa>)
[PROOF STEP]
by (simp add: lt_csucc_iff Card_cardinal_eq Card_is_Ord)


[STATEMENT]
lemma csucc_lt_csucc_iff: "\<lbrakk>Card \<kappa>'; Card \<kappa>\<rbrakk> \<Longrightarrow> (csucc \<kappa>' < csucc \<kappa>) = (\<kappa>' < \<kappa>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Card \<kappa>'; Card \<kappa>\<rbrakk> \<Longrightarrow> (csucc \<kappa>' < csucc \<kappa>) = (\<kappa>' < \<kappa>)
[PROOF STEP]
by (metis Card_csucc Card_is_Ord Card_lt_csucc_iff Ord_not_less)


[STATEMENT]
lemma csucc_le_csucc_iff: "\<lbrakk>Card \<kappa>'; Card \<kappa>\<rbrakk> \<Longrightarrow> (csucc \<kappa>' \<le> csucc \<kappa>) = (\<kappa>' \<le> \<kappa>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Card \<kappa>'; Card \<kappa>\<rbrakk> \<Longrightarrow> (csucc \<kappa>' \<le> csucc \<kappa>) = (\<kappa>' \<le> \<kappa>)
[PROOF STEP]
by (metis Card_csucc Card_is_Ord Card_lt_csucc_iff Ord_not_less)


[STATEMENT]
lemma csucc_0 [simp]: "csucc 0 = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. csucc 0 = 1
[PROOF STEP]
by (simp add: finite_csucc one_V_def)


[STATEMENT]
lemma Card_Un [simp,intro]:
  assumes "Card x" "Card y" shows "Card(x \<squnion> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Card (x \<squnion> y)
[PROOF STEP]
by (metis Card_is_Ord Ord_linear_le assms sup.absorb2 sup.orderE)


[STATEMENT]
lemma InfCard_csucc: "InfCard \<kappa> \<Longrightarrow> InfCard (csucc \<kappa>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InfCard \<kappa> \<Longrightarrow> InfCard (csucc \<kappa>)
[PROOF STEP]
using InfCard_def le_csucc
[PROOF STATE]
proof (prove)
using this:
InfCard ?\<kappa> \<equiv> Card ?\<kappa> \<and> \<omega> \<le> ?\<kappa>
Card ?\<kappa> \<Longrightarrow> ?\<kappa> \<le> csucc ?\<kappa>

goal (1 subgoal):
 1. InfCard \<kappa> \<Longrightarrow> InfCard (csucc \<kappa>)
[PROOF STEP]
by auto


[STATEMENT]
lemma InfCard_is_Limit:
  assumes "InfCard \<kappa>" shows "Limit \<kappa>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Limit \<kappa>
[PROOF STEP]
proof (rule non_succ_LimitI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<kappa> \<noteq> 0
 2. Ord \<kappa>
 3. \<And>y. ZFC_in_HOL.succ y \<noteq> \<kappa>
[PROOF STEP]
show "\<kappa> \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<kappa> \<noteq> 0
[PROOF STEP]
using InfCard_def assms mem_not_refl
[PROOF STATE]
proof (prove)
using this:
InfCard ?\<kappa> \<equiv> Card ?\<kappa> \<and> \<omega> \<le> ?\<kappa>
InfCard \<kappa>
?i \<notin> elts ?i

goal (1 subgoal):
 1. \<kappa> \<noteq> 0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<kappa> \<noteq> 0

goal (2 subgoals):
 1. Ord \<kappa>
 2. \<And>y. ZFC_in_HOL.succ y \<noteq> \<kappa>
[PROOF STEP]
show "Ord \<kappa>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ord \<kappa>
[PROOF STEP]
using Card_is_Ord InfCard_def assms
[PROOF STATE]
proof (prove)
using this:
Card ?\<kappa> \<Longrightarrow> Ord ?\<kappa>
InfCard ?\<kappa> \<equiv> Card ?\<kappa> \<and> \<omega> \<le> ?\<kappa>
InfCard \<kappa>

goal (1 subgoal):
 1. Ord \<kappa>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Ord \<kappa>

goal (1 subgoal):
 1. \<And>y. ZFC_in_HOL.succ y \<noteq> \<kappa>
[PROOF STEP]
show "ZFC_in_HOL.succ y \<noteq> \<kappa>" for y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ZFC_in_HOL.succ y \<noteq> \<kappa>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ZFC_in_HOL.succ y = \<kappa> \<Longrightarrow> False
[PROOF STEP]
assume "succ y = \<kappa>"
[PROOF STATE]
proof (state)
this:
ZFC_in_HOL.succ y = \<kappa>

goal (1 subgoal):
 1. ZFC_in_HOL.succ y = \<kappa> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ZFC_in_HOL.succ y = \<kappa>
[PROOF STEP]
have "Card (succ y)"
[PROOF STATE]
proof (prove)
using this:
ZFC_in_HOL.succ y = \<kappa>

goal (1 subgoal):
 1. Card (ZFC_in_HOL.succ y)
[PROOF STEP]
using InfCard_def assms
[PROOF STATE]
proof (prove)
using this:
ZFC_in_HOL.succ y = \<kappa>
InfCard ?\<kappa> \<equiv> Card ?\<kappa> \<and> \<omega> \<le> ?\<kappa>
InfCard \<kappa>

goal (1 subgoal):
 1. Card (ZFC_in_HOL.succ y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Card (ZFC_in_HOL.succ y)

goal (1 subgoal):
 1. ZFC_in_HOL.succ y = \<kappa> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Card (ZFC_in_HOL.succ y)

goal (1 subgoal):
 1. ZFC_in_HOL.succ y = \<kappa> \<Longrightarrow> False
[PROOF STEP]
have "\<omega> \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<omega> \<le> y
[PROOF STEP]
by (metis InfCard_iff Ord_in_Ord \<open>Ord \<kappa>\<close> \<open>ZFC_in_HOL.succ y = \<kappa>\<close> assms elts_succ finite_insert infinite_Ord_omega insertI1)
[PROOF STATE]
proof (state)
this:
\<omega> \<le> y

goal (1 subgoal):
 1. ZFC_in_HOL.succ y = \<kappa> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<omega> \<le> y

goal (1 subgoal):
 1. ZFC_in_HOL.succ y = \<kappa> \<Longrightarrow> False
[PROOF STEP]
have "elts y \<approx> elts (succ y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts y \<approx> elts (ZFC_in_HOL.succ y)
[PROOF STEP]
using InfCard_iff \<open>ZFC_in_HOL.succ y = \<kappa>\<close> assms eqpoll_sym infinite_insert_eqpoll
[PROOF STATE]
proof (prove)
using this:
InfCard ?\<kappa> = (Card ?\<kappa> \<and> infinite (elts ?\<kappa>))
ZFC_in_HOL.succ y = \<kappa>
InfCard \<kappa>
?A \<approx> ?B \<Longrightarrow> ?B \<approx> ?A
infinite ?A \<Longrightarrow> insert ?a ?A \<approx> ?A

goal (1 subgoal):
 1. elts y \<approx> elts (ZFC_in_HOL.succ y)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
elts y \<approx> elts (ZFC_in_HOL.succ y)

goal (1 subgoal):
 1. ZFC_in_HOL.succ y = \<kappa> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Card (ZFC_in_HOL.succ y)
\<omega> \<le> y
elts y \<approx> elts (ZFC_in_HOL.succ y)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
Card (ZFC_in_HOL.succ y)
\<omega> \<le> y
elts y \<approx> elts (ZFC_in_HOL.succ y)

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis Card_iff_initial Ord_in_Ord OrdmemD elts_succ insertI1)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ZFC_in_HOL.succ ?y \<noteq> \<kappa>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma InfCard_csquare_eq:
  assumes "InfCard(\<kappa>)" shows "\<kappa> \<otimes> \<kappa> = \<kappa>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<kappa> \<otimes> \<kappa> = \<kappa>
[PROOF STEP]
using infinite_times_eqpoll_self [of "elts \<kappa>"] assms
[PROOF STATE]
proof (prove)
using this:
infinite (elts \<kappa>) \<Longrightarrow> elts \<kappa> \<times> elts \<kappa> \<approx> elts \<kappa>
InfCard \<kappa>

goal (1 subgoal):
 1. \<kappa> \<otimes> \<kappa> = \<kappa>
[PROOF STEP]
unfolding InfCard_iff Card_def
[PROOF STATE]
proof (prove)
using this:
infinite (elts \<kappa>) \<Longrightarrow> elts \<kappa> \<times> elts \<kappa> \<approx> elts \<kappa>
\<kappa> = vcard \<kappa> \<and> infinite (elts \<kappa>)

goal (1 subgoal):
 1. \<kappa> \<otimes> \<kappa> = \<kappa>
[PROOF STEP]
by (metis cardinal_cong cardinal_eqpoll cmult_def elts_vcard_VSigma_eqpoll eqpoll_trans)


[STATEMENT]
lemma InfCard_le_cmult_eq:
  assumes "InfCard \<kappa>" "\<mu> \<le> \<kappa>" "\<mu> \<noteq> 0"
  shows "\<kappa> \<otimes> \<mu> = \<kappa>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<kappa> \<otimes> \<mu> = \<kappa>
[PROOF STEP]
proof (rule order_antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<kappa> \<otimes> \<mu> \<le> \<kappa>
 2. \<kappa> \<le> \<kappa> \<otimes> \<mu>
[PROOF STEP]
have "\<kappa> \<otimes> \<mu> \<le> \<kappa> \<otimes> \<kappa>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<kappa> \<otimes> \<mu> \<le> \<kappa> \<otimes> \<kappa>
[PROOF STEP]
by (simp add: assms(2) cmult_le_mono)
[PROOF STATE]
proof (state)
this:
\<kappa> \<otimes> \<mu> \<le> \<kappa> \<otimes> \<kappa>

goal (2 subgoals):
 1. \<kappa> \<otimes> \<mu> \<le> \<kappa>
 2. \<kappa> \<le> \<kappa> \<otimes> \<mu>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<kappa> \<otimes> \<mu> \<le> \<kappa> \<otimes> \<kappa>

goal (2 subgoals):
 1. \<kappa> \<otimes> \<mu> \<le> \<kappa>
 2. \<kappa> \<le> \<kappa> \<otimes> \<mu>
[PROOF STEP]
have "\<dots> \<le> \<kappa>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<kappa> \<otimes> \<kappa> \<le> \<kappa>
[PROOF STEP]
by (simp add: InfCard_csquare_eq assms(1))
[PROOF STATE]
proof (state)
this:
\<kappa> \<otimes> \<kappa> \<le> \<kappa>

goal (2 subgoals):
 1. \<kappa> \<otimes> \<mu> \<le> \<kappa>
 2. \<kappa> \<le> \<kappa> \<otimes> \<mu>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<kappa> \<otimes> \<mu> \<le> \<kappa>
[PROOF STEP]
show "\<kappa> \<otimes> \<mu> \<le> \<kappa>"
[PROOF STATE]
proof (prove)
using this:
\<kappa> \<otimes> \<mu> \<le> \<kappa>

goal (1 subgoal):
 1. \<kappa> \<otimes> \<mu> \<le> \<kappa>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<kappa> \<otimes> \<mu> \<le> \<kappa>

goal (1 subgoal):
 1. \<kappa> \<le> \<kappa> \<otimes> \<mu>
[PROOF STEP]
show "\<kappa> \<le> \<kappa> \<otimes> \<mu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<kappa> \<le> \<kappa> \<otimes> \<mu>
[PROOF STEP]
using InfCard_def assms(1) assms(3) cmult_le_self
[PROOF STATE]
proof (prove)
using this:
InfCard ?\<kappa> \<equiv> Card ?\<kappa> \<and> \<omega> \<le> ?\<kappa>
InfCard \<kappa>
\<mu> \<noteq> 0
\<lbrakk>Card ?\<kappa>; ?\<alpha> \<noteq> 0\<rbrakk> \<Longrightarrow> ?\<kappa> \<le> ?\<kappa> \<otimes> ?\<alpha>

goal (1 subgoal):
 1. \<kappa> \<le> \<kappa> \<otimes> \<mu>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<kappa> \<le> \<kappa> \<otimes> \<mu>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma InfCard_cmult_eq: "\<lbrakk>InfCard \<kappa>; InfCard \<mu>\<rbrakk> \<Longrightarrow> \<kappa> \<otimes> \<mu> = \<kappa> \<squnion> \<mu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>InfCard \<kappa>; InfCard \<mu>\<rbrakk> \<Longrightarrow> \<kappa> \<otimes> \<mu> = \<kappa> \<squnion> \<mu>
[PROOF STEP]
by (metis Card_is_Ord InfCard_def InfCard_le_cmult_eq Ord_linear_le cmult_commute inf_sup_aci(5) mem_not_refl sup.orderE sup_V_0_right zero_in_omega)


[STATEMENT]
lemma cmult_succ:
  "succ(m) \<otimes> n = n \<oplus> (m \<otimes> n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ZFC_in_HOL.succ m \<otimes> n = n \<oplus> m \<otimes> n
[PROOF STEP]
unfolding cmult_def cadd_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard (vtimes (ZFC_in_HOL.succ m) n) = vcard (n \<Uplus> vcard (vtimes m n))
[PROOF STEP]
proof (rule cardinal_cong)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. elts (vtimes (ZFC_in_HOL.succ m) n) \<approx> elts (n \<Uplus> vcard (vtimes m n))
[PROOF STEP]
have "elts (vtimes (ZFC_in_HOL.succ m) n) \<approx> elts n <+> elts m \<times> elts n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts (vtimes (ZFC_in_HOL.succ m) n) \<approx> elts n <+> elts m \<times> elts n
[PROOF STEP]
by (simp add: elts_VSigma prod_insert_eqpoll)
[PROOF STATE]
proof (state)
this:
elts (vtimes (ZFC_in_HOL.succ m) n) \<approx> elts n <+> elts m \<times> elts n

goal (1 subgoal):
 1. elts (vtimes (ZFC_in_HOL.succ m) n) \<approx> elts (n \<Uplus> vcard (vtimes m n))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
elts (vtimes (ZFC_in_HOL.succ m) n) \<approx> elts n <+> elts m \<times> elts n

goal (1 subgoal):
 1. elts (vtimes (ZFC_in_HOL.succ m) n) \<approx> elts (n \<Uplus> vcard (vtimes m n))
[PROOF STEP]
have "\<dots> \<approx> elts (n \<Uplus> vcard (vtimes m n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts n <+> elts m \<times> elts n \<approx> elts (n \<Uplus> vcard (vtimes m n))
[PROOF STEP]
unfolding elts_VSigma elts_vsum Plus_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sum_Type.Inl ` elts n \<union> Sum_Type.Inr ` (elts m \<times> elts n) \<approx> ZFC_Cardinals.Inl ` elts n \<union> ZFC_Cardinals.Inr ` elts (vcard (vtimes m n))
[PROOF STEP]
proof (rule Un_eqpoll_cong)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. Sum_Type.Inl ` elts n \<approx> ZFC_Cardinals.Inl ` elts n
 2. Sum_Type.Inr ` (elts m \<times> elts n) \<approx> ZFC_Cardinals.Inr ` elts (vcard (vtimes m n))
 3. disjnt (Sum_Type.Inl ` elts n) (Sum_Type.Inr ` (elts m \<times> elts n))
 4. disjnt (ZFC_Cardinals.Inl ` elts n) (ZFC_Cardinals.Inr ` elts (vcard (vtimes m n)))
[PROOF STEP]
show "(Sum_Type.Inr ` (elts m \<times> elts n)::(V + V \<times> V) set) \<approx> Inr ` elts (vcard (vtimes m n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sum_Type.Inr ` (elts m \<times> elts n) \<approx> ZFC_Cardinals.Inr ` elts (vcard (vtimes m n))
[PROOF STEP]
by (simp add: elts_vcard_VSigma_eqpoll eqpoll_sym)
[PROOF STATE]
proof (state)
this:
Sum_Type.Inr ` (elts m \<times> elts n) \<approx> ZFC_Cardinals.Inr ` elts (vcard (vtimes m n))

goal (3 subgoals):
 1. Sum_Type.Inl ` elts n \<approx> ZFC_Cardinals.Inl ` elts n
 2. disjnt (Sum_Type.Inl ` elts n) (Sum_Type.Inr ` (elts m \<times> elts n))
 3. disjnt (ZFC_Cardinals.Inl ` elts n) (ZFC_Cardinals.Inr ` elts (vcard (vtimes m n)))
[PROOF STEP]
qed (auto simp: disjnt_def)
[PROOF STATE]
proof (state)
this:
elts n <+> elts m \<times> elts n \<approx> elts (n \<Uplus> vcard (vtimes m n))

goal (1 subgoal):
 1. elts (vtimes (ZFC_in_HOL.succ m) n) \<approx> elts (n \<Uplus> vcard (vtimes m n))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
elts (vtimes (ZFC_in_HOL.succ m) n) \<approx> elts (n \<Uplus> vcard (vtimes m n))
[PROOF STEP]
show "elts (vtimes (ZFC_in_HOL.succ m) n) \<approx> elts (n \<Uplus> vcard (vtimes m n))"
[PROOF STATE]
proof (prove)
using this:
elts (vtimes (ZFC_in_HOL.succ m) n) \<approx> elts (n \<Uplus> vcard (vtimes m n))

goal (1 subgoal):
 1. elts (vtimes (ZFC_in_HOL.succ m) n) \<approx> elts (n \<Uplus> vcard (vtimes m n))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
elts (vtimes (ZFC_in_HOL.succ m) n) \<approx> elts (n \<Uplus> vcard (vtimes m n))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cmult_2:
  assumes "Card n" shows "ord_of_nat 2 \<otimes> n = n \<oplus> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ord_of_nat 2 \<otimes> n = n \<oplus> n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ord_of_nat 2 \<otimes> n = n \<oplus> n
[PROOF STEP]
have "ord_of_nat 2 = succ (succ 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ord_of_nat 2 = ZFC_in_HOL.succ (ZFC_in_HOL.succ 0)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
ord_of_nat 2 = ZFC_in_HOL.succ (ZFC_in_HOL.succ 0)

goal (1 subgoal):
 1. ord_of_nat 2 \<otimes> n = n \<oplus> n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ord_of_nat 2 = ZFC_in_HOL.succ (ZFC_in_HOL.succ 0)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ord_of_nat 2 = ZFC_in_HOL.succ (ZFC_in_HOL.succ 0)

goal (1 subgoal):
 1. ord_of_nat 2 \<otimes> n = n \<oplus> n
[PROOF STEP]
by (simp add: cmult_succ assms)
[PROOF STATE]
proof (state)
this:
ord_of_nat 2 \<otimes> n = n \<oplus> n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma InfCard_cdouble_eq:
  assumes "InfCard \<kappa>" shows "\<kappa> \<oplus> \<kappa> = \<kappa>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<kappa> \<oplus> \<kappa> = \<kappa>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<kappa> \<oplus> \<kappa> = \<kappa>
[PROOF STEP]
have "\<kappa> \<oplus> \<kappa> = \<kappa> \<otimes> ord_of_nat 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<kappa> \<oplus> \<kappa> = \<kappa> \<otimes> ord_of_nat 2
[PROOF STEP]
using InfCard_def assms cmult_2 cmult_commute
[PROOF STATE]
proof (prove)
using this:
InfCard ?\<kappa> \<equiv> Card ?\<kappa> \<and> \<omega> \<le> ?\<kappa>
InfCard \<kappa>
Card ?n \<Longrightarrow> ord_of_nat 2 \<otimes> ?n = ?n \<oplus> ?n
?i \<otimes> ?j = ?j \<otimes> ?i

goal (1 subgoal):
 1. \<kappa> \<oplus> \<kappa> = \<kappa> \<otimes> ord_of_nat 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<kappa> \<oplus> \<kappa> = \<kappa> \<otimes> ord_of_nat 2

goal (1 subgoal):
 1. \<kappa> \<oplus> \<kappa> = \<kappa>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<kappa> \<oplus> \<kappa> = \<kappa> \<otimes> ord_of_nat 2

goal (1 subgoal):
 1. \<kappa> \<oplus> \<kappa> = \<kappa>
[PROOF STEP]
have "\<dots> = \<kappa>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<kappa> \<otimes> ord_of_nat 2 = \<kappa>
[PROOF STEP]
by (simp add: InfCard_le_cmult_eq InfCard_ge_ord_of_nat assms)
[PROOF STATE]
proof (state)
this:
\<kappa> \<otimes> ord_of_nat 2 = \<kappa>

goal (1 subgoal):
 1. \<kappa> \<oplus> \<kappa> = \<kappa>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<kappa> \<oplus> \<kappa> = \<kappa>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<kappa> \<oplus> \<kappa> = \<kappa>

goal (1 subgoal):
 1. \<kappa> \<oplus> \<kappa> = \<kappa>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<kappa> \<oplus> \<kappa> = \<kappa>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma InfCard_le_cadd_eq: "\<lbrakk>InfCard \<kappa>; \<mu> \<le> \<kappa>\<rbrakk> \<Longrightarrow> \<kappa> \<oplus> \<mu> = \<kappa>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>InfCard \<kappa>; \<mu> \<le> \<kappa>\<rbrakk> \<Longrightarrow> \<kappa> \<oplus> \<mu> = \<kappa>
[PROOF STEP]
by (metis InfCard_cdouble_eq InfCard_def antisym cadd_le_mono cadd_le_self)


[STATEMENT]
lemma InfCard_cadd_eq: "\<lbrakk>InfCard \<kappa>; InfCard \<mu>\<rbrakk> \<Longrightarrow> \<kappa> \<oplus> \<mu> = \<kappa> \<squnion> \<mu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>InfCard \<kappa>; InfCard \<mu>\<rbrakk> \<Longrightarrow> \<kappa> \<oplus> \<mu> = \<kappa> \<squnion> \<mu>
[PROOF STEP]
by (metis Card_iff_initial InfCard_def InfCard_le_cadd_eq Ord_linear_le cadd_commute sup.absorb2 sup.orderE)


[STATEMENT]
lemma csucc_le_Card_iff: "\<lbrakk>Card \<kappa>'; Card \<kappa>\<rbrakk> \<Longrightarrow> csucc \<kappa>' \<le> \<kappa> \<longleftrightarrow> \<kappa>' < \<kappa>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Card \<kappa>'; Card \<kappa>\<rbrakk> \<Longrightarrow> (csucc \<kappa>' \<le> \<kappa>) = (\<kappa>' < \<kappa>)
[PROOF STEP]
by (metis Card_csucc Card_is_Ord Card_lt_csucc_iff Ord_not_le)


[STATEMENT]
lemma cadd_InfCard_le:
  assumes "\<alpha> \<le> \<kappa>" "\<beta> \<le> \<kappa>" "InfCard \<kappa>"
  shows "\<alpha> \<oplus> \<beta> \<le> \<kappa>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> \<oplus> \<beta> \<le> \<kappa>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<alpha> \<le> \<kappa>
\<beta> \<le> \<kappa>
InfCard \<kappa>

goal (1 subgoal):
 1. \<alpha> \<oplus> \<beta> \<le> \<kappa>
[PROOF STEP]
by (metis InfCard_cdouble_eq cadd_le_mono)


[STATEMENT]
lemma cmult_InfCard_le:
  assumes "\<alpha> \<le> \<kappa>" "\<beta> \<le> \<kappa>" "InfCard \<kappa>"
  shows "\<alpha> \<otimes> \<beta> \<le> \<kappa>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> \<otimes> \<beta> \<le> \<kappa>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<alpha> \<le> \<kappa>
\<beta> \<le> \<kappa>
InfCard \<kappa>

goal (1 subgoal):
 1. \<alpha> \<otimes> \<beta> \<le> \<kappa>
[PROOF STEP]
by (metis InfCard_csquare_eq cmult_le_mono)


[STATEMENT]
lemma Aleph: "Aleph \<alpha> = \<omega> \<squnion> (\<Squnion>y\<in>elts \<alpha>. csucc (Aleph y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<aleph>\<alpha> = \<omega> \<squnion> (\<Squnion>y\<in>elts \<alpha>. csucc (\<aleph>y))
[PROOF STEP]
by (simp add: Aleph_def transrec[of _ \<alpha>])


[STATEMENT]
lemma InfCard_Aleph [simp, intro]: "InfCard(Aleph x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InfCard (\<aleph>x)
[PROOF STEP]
proof (induction x rule: eps_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (\<And>y. y \<in> elts x \<Longrightarrow> InfCard (\<aleph>y)) \<Longrightarrow> InfCard (\<aleph>x)
[PROOF STEP]
case (step x)
[PROOF STATE]
proof (state)
this:
?y \<in> elts x \<Longrightarrow> InfCard (\<aleph>?y)

goal (1 subgoal):
 1. \<And>x. (\<And>y. y \<in> elts x \<Longrightarrow> InfCard (\<aleph>y)) \<Longrightarrow> InfCard (\<aleph>x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?y \<in> elts x \<Longrightarrow> InfCard (\<aleph>?y)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?y \<in> elts x \<Longrightarrow> InfCard (\<aleph>?y)

goal (1 subgoal):
 1. InfCard (\<aleph>x)
[PROOF STEP]
by (simp add: Aleph [of x] InfCard_def Card_UN step)
[PROOF STATE]
proof (state)
this:
InfCard (\<aleph>x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Card_Aleph [simp, intro]: "Card(Aleph x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Card (\<aleph>x)
[PROOF STEP]
using InfCard_def
[PROOF STATE]
proof (prove)
using this:
InfCard ?\<kappa> \<equiv> Card ?\<kappa> \<and> \<omega> \<le> ?\<kappa>

goal (1 subgoal):
 1. Card (\<aleph>x)
[PROOF STEP]
by auto


[STATEMENT]
lemma Aleph_0 [simp]: "\<aleph>0 = \<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<aleph>0 = \<omega>
[PROOF STEP]
by (simp add: Aleph [of 0])


[STATEMENT]
lemma mem_Aleph_succ: "\<aleph>\<alpha> \<in> elts (Aleph (succ \<alpha>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<aleph>\<alpha> \<in> elts (\<aleph>ZFC_in_HOL.succ \<alpha>)
[PROOF STEP]
apply (simp add: Aleph [of "succ \<alpha>"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<aleph>\<alpha> \<in> elts \<omega> \<or> \<aleph>\<alpha> \<in> elts (csucc (\<aleph>\<alpha>)) \<or> (\<exists>x\<in>elts \<alpha>. \<aleph>\<alpha> \<in> elts (csucc (\<aleph>x)))
[PROOF STEP]
by (meson InfCard_Aleph Card_csucc Card_is_Ord InfCard_def Ord_mem_iff_lt less_csucc)


[STATEMENT]
lemma Aleph_lt_succD [simp]: "\<aleph>\<alpha> < Aleph (succ \<alpha>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<aleph>\<alpha> < \<aleph>ZFC_in_HOL.succ \<alpha>
[PROOF STEP]
by (simp add: InfCard_is_Limit Limit_is_Ord OrdmemD mem_Aleph_succ)


[STATEMENT]
lemma Aleph_succ [simp]: "Aleph (succ x) = csucc (Aleph x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<aleph>ZFC_in_HOL.succ x = csucc (\<aleph>x)
[PROOF STEP]
proof (rule antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<aleph>ZFC_in_HOL.succ x \<le> csucc (\<aleph>x)
 2. csucc (\<aleph>x) \<le> \<aleph>ZFC_in_HOL.succ x
[PROOF STEP]
show "Aleph (ZFC_in_HOL.succ x) \<le> csucc (Aleph x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<aleph>ZFC_in_HOL.succ x \<le> csucc (\<aleph>x)
[PROOF STEP]
apply (simp add: Aleph [of "succ x"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<omega> \<le> csucc (\<aleph>x) \<and> \<Squnion> insert (csucc (\<aleph>x)) ((\<lambda>x. csucc (\<aleph>x)) ` elts x) \<le> csucc (\<aleph>x)
[PROOF STEP]
by (metis Aleph InfCard_Aleph InfCard_def Sup_V_insert le_csucc le_sup_iff order_refl
         replacement small_elts)
[PROOF STATE]
proof (state)
this:
\<aleph>ZFC_in_HOL.succ x \<le> csucc (\<aleph>x)

goal (1 subgoal):
 1. csucc (\<aleph>x) \<le> \<aleph>ZFC_in_HOL.succ x
[PROOF STEP]
show "csucc (Aleph x) \<le> Aleph (ZFC_in_HOL.succ x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. csucc (\<aleph>x) \<le> \<aleph>ZFC_in_HOL.succ x
[PROOF STEP]
by (force simp add: Aleph [of "succ x"])
[PROOF STATE]
proof (state)
this:
csucc (\<aleph>x) \<le> \<aleph>ZFC_in_HOL.succ x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma csucc_Aleph_le_Aleph: "\<alpha> \<in> elts \<beta> \<Longrightarrow> csucc (\<aleph>\<alpha>) \<le> \<aleph>\<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> \<in> elts \<beta> \<Longrightarrow> csucc (\<aleph>\<alpha>) \<le> \<aleph>\<beta>
[PROOF STEP]
by (metis Aleph ZFC_in_HOL.SUP_le_iff replacement small_elts sup_ge2)


[STATEMENT]
lemma Aleph_in_Aleph: "\<alpha> \<in> elts \<beta> \<Longrightarrow> \<aleph>\<alpha> \<in> elts (\<aleph>\<beta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> \<in> elts \<beta> \<Longrightarrow> \<aleph>\<alpha> \<in> elts (\<aleph>\<beta>)
[PROOF STEP]
using csucc_Aleph_le_Aleph mem_Aleph_succ
[PROOF STATE]
proof (prove)
using this:
?\<alpha> \<in> elts ?\<beta> \<Longrightarrow> csucc (\<aleph>?\<alpha>) \<le> \<aleph>?\<beta>
\<aleph>?\<alpha> \<in> elts (\<aleph>ZFC_in_HOL.succ ?\<alpha>)

goal (1 subgoal):
 1. \<alpha> \<in> elts \<beta> \<Longrightarrow> \<aleph>\<alpha> \<in> elts (\<aleph>\<beta>)
[PROOF STEP]
by auto


[STATEMENT]
lemma Aleph_Limit:
  assumes "Limit \<gamma>"
  shows "Aleph \<gamma> = \<Squnion> (Aleph ` elts \<gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<aleph>\<gamma> = \<Squnion> (Aleph ` elts \<gamma>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<aleph>\<gamma> = \<Squnion> (Aleph ` elts \<gamma>)
[PROOF STEP]
have [simp]: "\<gamma> \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<gamma> \<noteq> 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Limit \<gamma>

goal (1 subgoal):
 1. \<gamma> \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<gamma> \<noteq> 0

goal (1 subgoal):
 1. \<aleph>\<gamma> = \<Squnion> (Aleph ` elts \<gamma>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<aleph>\<gamma> = \<Squnion> (Aleph ` elts \<gamma>)
[PROOF STEP]
proof (rule antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<aleph>\<gamma> \<le> \<Squnion> (Aleph ` elts \<gamma>)
 2. \<Squnion> (Aleph ` elts \<gamma>) \<le> \<aleph>\<gamma>
[PROOF STEP]
show "Aleph \<gamma> \<le> \<Squnion> (Aleph ` elts \<gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<aleph>\<gamma> \<le> \<Squnion> (Aleph ` elts \<gamma>)
[PROOF STEP]
apply (simp add: Aleph [of \<gamma>])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<omega> \<le> \<Squnion> (Aleph ` elts \<gamma>) \<and> (\<Squnion>y\<in>elts \<gamma>. csucc (\<aleph>y)) \<le> \<Squnion> (Aleph ` elts \<gamma>)
[PROOF STEP]
by (metis (mono_tags, lifting) Aleph_0 Aleph_succ Limit_def ZFC_in_HOL.SUP_le_iff
           ZFC_in_HOL.Sup_upper assms imageI replacement small_elts)
[PROOF STATE]
proof (state)
this:
\<aleph>\<gamma> \<le> \<Squnion> (Aleph ` elts \<gamma>)

goal (1 subgoal):
 1. \<Squnion> (Aleph ` elts \<gamma>) \<le> \<aleph>\<gamma>
[PROOF STEP]
show "\<Squnion> (Aleph ` elts \<gamma>) \<le> Aleph \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Squnion> (Aleph ` elts \<gamma>) \<le> \<aleph>\<gamma>
[PROOF STEP]
apply (simp add: cSup_le_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>elts \<gamma>. \<aleph>x \<le> \<aleph>\<gamma>
[PROOF STEP]
by (meson InfCard_Aleph InfCard_def csucc_Aleph_le_Aleph le_csucc order_trans)
[PROOF STATE]
proof (state)
this:
\<Squnion> (Aleph ` elts \<gamma>) \<le> \<aleph>\<gamma>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<aleph>\<gamma> = \<Squnion> (Aleph ` elts \<gamma>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Aleph_increasing:
  assumes ab: "\<alpha> < \<beta>" "Ord \<alpha>" "Ord \<beta>" shows "\<aleph>\<alpha> < \<aleph>\<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<aleph>\<alpha> < \<aleph>\<beta>
[PROOF STEP]
by (meson Aleph_in_Aleph InfCard_Aleph Card_iff_initial InfCard_def Ord_mem_iff_lt assms)


[STATEMENT]
lemma countable_iff_le_Aleph0: "countable (elts A) \<longleftrightarrow> vcard A \<le> \<aleph>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. countable (elts A) = (vcard A \<le> \<aleph>0)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. countable (elts A) \<Longrightarrow> vcard A \<le> \<aleph>0
 2. vcard A \<le> \<aleph>0 \<Longrightarrow> countable (elts A)
[PROOF STEP]
show "vcard A \<le> \<aleph>0"
    if "countable (elts A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard A \<le> \<aleph>0
[PROOF STEP]
proof (cases "finite (elts A)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite (elts A) \<Longrightarrow> vcard A \<le> \<aleph>0
 2. infinite (elts A) \<Longrightarrow> vcard A \<le> \<aleph>0
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
finite (elts A)

goal (2 subgoals):
 1. finite (elts A) \<Longrightarrow> vcard A \<le> \<aleph>0
 2. infinite (elts A) \<Longrightarrow> vcard A \<le> \<aleph>0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite (elts A)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite (elts A)

goal (1 subgoal):
 1. vcard A \<le> \<aleph>0
[PROOF STEP]
using vcard_finite_set
[PROOF STATE]
proof (prove)
using this:
finite (elts A)
finite ?A \<Longrightarrow> vcard (set ?A) = ord_of_nat (card ?A)

goal (1 subgoal):
 1. vcard A \<le> \<aleph>0
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
vcard A \<le> \<aleph>0

goal (1 subgoal):
 1. infinite (elts A) \<Longrightarrow> vcard A \<le> \<aleph>0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. infinite (elts A) \<Longrightarrow> vcard A \<le> \<aleph>0
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
infinite (elts A)

goal (1 subgoal):
 1. infinite (elts A) \<Longrightarrow> vcard A \<le> \<aleph>0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
infinite (elts A)
[PROOF STEP]
have "elts \<omega> \<approx> elts A"
[PROOF STATE]
proof (prove)
using this:
infinite (elts A)

goal (1 subgoal):
 1. elts \<omega> \<approx> elts A
[PROOF STEP]
using countableE_infinite [OF that]
[PROOF STATE]
proof (prove)
using this:
infinite (elts A)
\<lbrakk>infinite (elts A); \<And>e. bij_betw e (elts A) UNIV \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. elts \<omega> \<approx> elts A
[PROOF STEP]
by (simp add: eqpoll_def \<omega>_def)
         (meson bij_betw_def bij_betw_inv bij_betw_trans inj_ord_of_nat)
[PROOF STATE]
proof (state)
this:
elts \<omega> \<approx> elts A

goal (1 subgoal):
 1. infinite (elts A) \<Longrightarrow> vcard A \<le> \<aleph>0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
elts \<omega> \<approx> elts A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
elts \<omega> \<approx> elts A

goal (1 subgoal):
 1. vcard A \<le> \<aleph>0
[PROOF STEP]
using Card_\<omega> Card_def cardinal_cong vcard_def
[PROOF STATE]
proof (prove)
using this:
elts \<omega> \<approx> elts A
Card \<omega>
Card ?i \<equiv> ?i = vcard ?i
elts ?x \<approx> elts ?y \<Longrightarrow> vcard ?x = vcard ?y
vcard ?a \<equiv> LEAST i. Ord i \<and> elts i \<approx> elts ?a

goal (1 subgoal):
 1. vcard A \<le> \<aleph>0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vcard A \<le> \<aleph>0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
countable (elts A) \<Longrightarrow> vcard A \<le> \<aleph>0

goal (1 subgoal):
 1. vcard A \<le> \<aleph>0 \<Longrightarrow> countable (elts A)
[PROOF STEP]
show "countable (elts A)"
    if "vcard A \<le> Aleph 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. countable (elts A)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. countable (elts A)
[PROOF STEP]
have "elts A \<lesssim> elts \<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts A \<lesssim> elts \<omega>
[PROOF STEP]
using cardinal_le_lepoll [OF that]
[PROOF STATE]
proof (prove)
using this:
elts A \<lesssim> elts (\<aleph>0)

goal (1 subgoal):
 1. elts A \<lesssim> elts \<omega>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
elts A \<lesssim> elts \<omega>

goal (1 subgoal):
 1. countable (elts A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
elts A \<lesssim> elts \<omega>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
elts A \<lesssim> elts \<omega>

goal (1 subgoal):
 1. countable (elts A)
[PROOF STEP]
by (simp add: countable_iff_lepoll \<omega>_def inj_ord_of_nat)
[PROOF STATE]
proof (state)
this:
countable (elts A)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
vcard A \<le> \<aleph>0 \<Longrightarrow> countable (elts A)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Aleph_csquare_eq [simp]: "\<aleph>\<alpha> \<otimes> \<aleph>\<alpha> = \<aleph>\<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<aleph>\<alpha> \<otimes> \<aleph>\<alpha> = \<aleph>\<alpha>
[PROOF STEP]
using InfCard_csquare_eq
[PROOF STATE]
proof (prove)
using this:
InfCard ?\<kappa> \<Longrightarrow> ?\<kappa> \<otimes> ?\<kappa> = ?\<kappa>

goal (1 subgoal):
 1. \<aleph>\<alpha> \<otimes> \<aleph>\<alpha> = \<aleph>\<alpha>
[PROOF STEP]
by auto


[STATEMENT]
lemma vcard_Aleph [simp]: "vcard (\<aleph>\<alpha>) = \<aleph>\<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard (\<aleph>\<alpha>) = \<aleph>\<alpha>
[PROOF STEP]
using Card_def InfCard_Aleph InfCard_def
[PROOF STATE]
proof (prove)
using this:
Card ?i \<equiv> ?i = vcard ?i
InfCard (\<aleph>?x)
InfCard ?\<kappa> \<equiv> Card ?\<kappa> \<and> \<omega> \<le> ?\<kappa>

goal (1 subgoal):
 1. vcard (\<aleph>\<alpha>) = \<aleph>\<alpha>
[PROOF STEP]
by auto


[STATEMENT]
lemma omega_le_Aleph [simp]: "\<omega> \<le> \<aleph>\<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<omega> \<le> \<aleph>\<alpha>
[PROOF STEP]
using InfCard_def
[PROOF STATE]
proof (prove)
using this:
InfCard ?\<kappa> \<equiv> Card ?\<kappa> \<and> \<omega> \<le> ?\<kappa>

goal (1 subgoal):
 1. \<omega> \<le> \<aleph>\<alpha>
[PROOF STEP]
by auto


[STATEMENT]
lemma finite_iff_less_Aleph0: "finite (elts x) \<longleftrightarrow> vcard x < \<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (elts x) = (vcard x < \<omega>)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite (elts x) \<Longrightarrow> vcard x < \<omega>
 2. vcard x < \<omega> \<Longrightarrow> finite (elts x)
[PROOF STEP]
show "finite (elts x) \<Longrightarrow> vcard x < \<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (elts x) \<Longrightarrow> vcard x < \<omega>
[PROOF STEP]
by (metis Card_\<omega> Card_def finite_lesspoll_infinite infinite_\<omega> lesspoll_imp_Card_less)
[PROOF STATE]
proof (state)
this:
finite (elts x) \<Longrightarrow> vcard x < \<omega>

goal (1 subgoal):
 1. vcard x < \<omega> \<Longrightarrow> finite (elts x)
[PROOF STEP]
show "vcard x < \<omega> \<Longrightarrow> finite (elts x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard x < \<omega> \<Longrightarrow> finite (elts x)
[PROOF STEP]
by (meson Ord_cardinal cardinal_eqpoll eqpoll_finite_iff infinite_Ord_omega less_le_not_le)
[PROOF STATE]
proof (state)
this:
vcard x < \<omega> \<Longrightarrow> finite (elts x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma countable_iff_vcard_less1: "countable (elts x) \<longleftrightarrow> vcard x < \<aleph>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. countable (elts x) = (vcard x < \<aleph>1)
[PROOF STEP]
by (simp add: countable_iff_le_Aleph0 lt_csucc_iff one_V_def)


[STATEMENT]
lemma countable_infinite_vcard: "countable (elts x) \<and> infinite (elts x) \<longleftrightarrow> vcard x = \<aleph>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (countable (elts x) \<and> infinite (elts x)) = (vcard x = \<aleph>0)
[PROOF STEP]
by (metis Aleph_0 countable_iff_le_Aleph0 dual_order.refl finite_iff_less_Aleph0 less_V_def)


[STATEMENT]
lemma Ord_\<omega>1 [simp]: "Ord \<omega>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ord \<omega>1
[PROOF STEP]
by (metis Ord_cardinal vcard_Aleph)


[STATEMENT]
lemma omega_\<omega>1 [iff]: "\<omega> \<in> elts \<omega>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<omega> \<in> elts \<omega>1
[PROOF STEP]
by (metis Aleph_0 mem_Aleph_succ one_V_def)


[STATEMENT]
lemma ord_of_nat_\<omega>1 [iff]: "ord_of_nat n \<in> elts \<omega>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ord_of_nat n \<in> elts \<omega>1
[PROOF STEP]
using Ord_\<omega>1 Ord_trans
[PROOF STATE]
proof (prove)
using this:
Ord \<omega>1
\<lbrakk>?i \<in> elts ?j; ?j \<in> elts ?k; Ord ?k\<rbrakk> \<Longrightarrow> ?i \<in> elts ?k

goal (1 subgoal):
 1. ord_of_nat n \<in> elts \<omega>1
[PROOF STEP]
by blast


[STATEMENT]
lemma countable_iff_less_\<omega>1:
  assumes "Ord \<alpha>"
  shows "countable (elts \<alpha>) \<longleftrightarrow> \<alpha> < \<omega>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. countable (elts \<alpha>) = (\<alpha> < \<omega>1)
[PROOF STEP]
by (simp add: assms countable_iff_le_Aleph0 lt_csucc_iff one_V_def)


[STATEMENT]
lemma less_\<omega>1_imp_countable:
  assumes "\<alpha> \<in> elts \<omega>1"
  shows "countable (elts \<alpha>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. countable (elts \<alpha>)
[PROOF STEP]
using Ord_\<omega>1 Ord_in_Ord OrdmemD assms countable_iff_less_\<omega>1
[PROOF STATE]
proof (prove)
using this:
Ord \<omega>1
\<lbrakk>Ord ?k; ?m \<in> elts ?k\<rbrakk> \<Longrightarrow> Ord ?m
\<lbrakk>Ord ?k; ?j \<in> elts ?k\<rbrakk> \<Longrightarrow> ?j < ?k
\<alpha> \<in> elts \<omega>1
Ord ?\<alpha> \<Longrightarrow> countable (elts ?\<alpha>) = (?\<alpha> < \<omega>1)

goal (1 subgoal):
 1. countable (elts \<alpha>)
[PROOF STEP]
by blast


[STATEMENT]
lemma \<omega>1_gt0 [simp]: "\<omega>1 > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < \<omega>1
[PROOF STEP]
using Ord_\<omega>1 Ord_trans OrdmemD
[PROOF STATE]
proof (prove)
using this:
Ord \<omega>1
\<lbrakk>?i \<in> elts ?j; ?j \<in> elts ?k; Ord ?k\<rbrakk> \<Longrightarrow> ?i \<in> elts ?k
\<lbrakk>Ord ?k; ?j \<in> elts ?k\<rbrakk> \<Longrightarrow> ?j < ?k

goal (1 subgoal):
 1. 0 < \<omega>1
[PROOF STEP]
by blast


[STATEMENT]
lemma \<omega>1_gt1 [simp]: "\<omega>1 > 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < \<omega>1
[PROOF STEP]
using Ord_\<omega>1 OrdmemD \<omega>_gt1 less_trans
[PROOF STATE]
proof (prove)
using this:
Ord \<omega>1
\<lbrakk>Ord ?k; ?j \<in> elts ?k\<rbrakk> \<Longrightarrow> ?j < ?k
1 < \<omega>
\<lbrakk>?x < ?y; ?y < ?z\<rbrakk> \<Longrightarrow> ?x < ?z

goal (1 subgoal):
 1. 1 < \<omega>1
[PROOF STEP]
by blast


[STATEMENT]
lemma Limit_\<omega>1 [simp]: "Limit \<omega>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Limit \<omega>1
[PROOF STEP]
by (simp add: InfCard_def InfCard_is_Limit le_csucc one_V_def)


[STATEMENT]
lemma sorted_list_app: "sorted_list xs \<Longrightarrow> (\<And>x. x \<in> set xs \<Longrightarrow> x \<le> y) \<Longrightarrow> sorted_list (xs @ [y])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sorted_list xs; \<And>x. x \<in> set xs \<Longrightarrow> x \<le> y\<rbrakk> \<Longrightarrow> sorted_list (xs @ [y])
[PROOF STEP]
by (induction xs rule: sorted_list.induct) auto


[STATEMENT]
lemma sorted_list_drop: "sorted_list xs \<Longrightarrow> sorted_list (drop n xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted_list xs \<Longrightarrow> sorted_list (drop n xs)
[PROOF STEP]
proof (induction xs arbitrary: n rule: sorted_list.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>n. sorted_list (drop n [])
 2. \<And>x n. sorted_list (drop n [x])
 3. \<And>x y ys n. \<lbrakk>x \<le> y; sorted_list (y # ys); \<And>n. sorted_list (drop n (y # ys))\<rbrakk> \<Longrightarrow> sorted_list (drop n (x # y # ys))
[PROOF STEP]
case (2 x n)
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. \<And>n. sorted_list (drop n [])
 2. \<And>x n. sorted_list (drop n [x])
 3. \<And>x y ys n. \<lbrakk>x \<le> y; sorted_list (y # ys); \<And>n. sorted_list (drop n (y # ys))\<rbrakk> \<Longrightarrow> sorted_list (drop n (x # y # ys))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted_list (drop n [x])
[PROOF STEP]
by (cases n) auto
[PROOF STATE]
proof (state)
this:
sorted_list (drop n [x])

goal (2 subgoals):
 1. \<And>n. sorted_list (drop n [])
 2. \<And>x y ys n. \<lbrakk>x \<le> y; sorted_list (y # ys); \<And>n. sorted_list (drop n (y # ys))\<rbrakk> \<Longrightarrow> sorted_list (drop n (x # y # ys))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n. sorted_list (drop n [])
 2. \<And>x y ys n. \<lbrakk>x \<le> y; sorted_list (y # ys); \<And>n. sorted_list (drop n (y # ys))\<rbrakk> \<Longrightarrow> sorted_list (drop n (x # y # ys))
[PROOF STEP]
case (3 x y ys n)
[PROOF STATE]
proof (state)
this:
x \<le> y
sorted_list (y # ys)
sorted_list (drop ?n (y # ys))

goal (2 subgoals):
 1. \<And>n. sorted_list (drop n [])
 2. \<And>x y ys n. \<lbrakk>x \<le> y; sorted_list (y # ys); \<And>n. sorted_list (drop n (y # ys))\<rbrakk> \<Longrightarrow> sorted_list (drop n (x # y # ys))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<le> y
sorted_list (y # ys)
sorted_list (drop ?n (y # ys))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<le> y
sorted_list (y # ys)
sorted_list (drop ?n (y # ys))

goal (1 subgoal):
 1. sorted_list (drop n (x # y # ys))
[PROOF STEP]
by (cases n) auto
[PROOF STATE]
proof (state)
this:
sorted_list (drop n (x # y # ys))

goal (1 subgoal):
 1. \<And>n. sorted_list (drop n [])
[PROOF STEP]
qed auto


[STATEMENT]
lemma sorted_list_ConsD: "sorted_list (x # xs) \<Longrightarrow> sorted_list xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted_list (x # xs) \<Longrightarrow> sorted_list xs
[PROOF STEP]
by (auto elim: sorted_list.cases)


[STATEMENT]
lemma sorted_list_Cons_nth: "sorted_list (x # xs) \<Longrightarrow> j < length xs \<Longrightarrow> x \<le> xs ! j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sorted_list (x # xs); j < length xs\<rbrakk> \<Longrightarrow> x \<le> xs ! j
[PROOF STEP]
by (induction "x # xs" arbitrary: x xs j rule: sorted_list.induct)
     (fastforce simp: nth_Cons split: nat.splits)+


[STATEMENT]
lemma sorted_list_atD: "sorted_list xs \<Longrightarrow> i \<le> j \<Longrightarrow> j < length xs \<Longrightarrow> xs ! i \<le> xs ! j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sorted_list xs; i \<le> j; j < length xs\<rbrakk> \<Longrightarrow> xs ! i \<le> xs ! j
[PROOF STEP]
proof (induction xs arbitrary: i j rule: sorted_list.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i \<le> j; j < length []\<rbrakk> \<Longrightarrow> [] ! i \<le> [] ! j
 2. \<And>x i j. \<lbrakk>i \<le> j; j < length [x]\<rbrakk> \<Longrightarrow> [x] ! i \<le> [x] ! j
 3. \<And>x y ys i j. \<lbrakk>x \<le> y; sorted_list (y # ys); \<And>i j. \<lbrakk>i \<le> j; j < length (y # ys)\<rbrakk> \<Longrightarrow> (y # ys) ! i \<le> (y # ys) ! j; i \<le> j; j < length (x # y # ys)\<rbrakk> \<Longrightarrow> (x # y # ys) ! i \<le> (x # y # ys) ! j
[PROOF STEP]
case (2 x i j)
[PROOF STATE]
proof (state)
this:
i \<le> j
j < length [x]

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i \<le> j; j < length []\<rbrakk> \<Longrightarrow> [] ! i \<le> [] ! j
 2. \<And>x i j. \<lbrakk>i \<le> j; j < length [x]\<rbrakk> \<Longrightarrow> [x] ! i \<le> [x] ! j
 3. \<And>x y ys i j. \<lbrakk>x \<le> y; sorted_list (y # ys); \<And>i j. \<lbrakk>i \<le> j; j < length (y # ys)\<rbrakk> \<Longrightarrow> (y # ys) ! i \<le> (y # ys) ! j; i \<le> j; j < length (x # y # ys)\<rbrakk> \<Longrightarrow> (x # y # ys) ! i \<le> (x # y # ys) ! j
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<le> j
j < length [x]
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
i \<le> j
j < length [x]

goal (1 subgoal):
 1. [x] ! i \<le> [x] ! j
[PROOF STEP]
by (cases i) auto
[PROOF STATE]
proof (state)
this:
[x] ! i \<le> [x] ! j

goal (2 subgoals):
 1. \<And>i j. \<lbrakk>i \<le> j; j < length []\<rbrakk> \<Longrightarrow> [] ! i \<le> [] ! j
 2. \<And>x y ys i j. \<lbrakk>x \<le> y; sorted_list (y # ys); \<And>i j. \<lbrakk>i \<le> j; j < length (y # ys)\<rbrakk> \<Longrightarrow> (y # ys) ! i \<le> (y # ys) ! j; i \<le> j; j < length (x # y # ys)\<rbrakk> \<Longrightarrow> (x # y # ys) ! i \<le> (x # y # ys) ! j
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i j. \<lbrakk>i \<le> j; j < length []\<rbrakk> \<Longrightarrow> [] ! i \<le> [] ! j
 2. \<And>x y ys i j. \<lbrakk>x \<le> y; sorted_list (y # ys); \<And>i j. \<lbrakk>i \<le> j; j < length (y # ys)\<rbrakk> \<Longrightarrow> (y # ys) ! i \<le> (y # ys) ! j; i \<le> j; j < length (x # y # ys)\<rbrakk> \<Longrightarrow> (x # y # ys) ! i \<le> (x # y # ys) ! j
[PROOF STEP]
case (3 x y ys i j)
[PROOF STATE]
proof (state)
this:
x \<le> y
sorted_list (y # ys)
\<lbrakk>?i \<le> ?j; ?j < length (y # ys)\<rbrakk> \<Longrightarrow> (y # ys) ! ?i \<le> (y # ys) ! ?j
i \<le> j
j < length (x # y # ys)

goal (2 subgoals):
 1. \<And>i j. \<lbrakk>i \<le> j; j < length []\<rbrakk> \<Longrightarrow> [] ! i \<le> [] ! j
 2. \<And>x y ys i j. \<lbrakk>x \<le> y; sorted_list (y # ys); \<And>i j. \<lbrakk>i \<le> j; j < length (y # ys)\<rbrakk> \<Longrightarrow> (y # ys) ! i \<le> (y # ys) ! j; i \<le> j; j < length (x # y # ys)\<rbrakk> \<Longrightarrow> (x # y # ys) ! i \<le> (x # y # ys) ! j
[PROOF STEP]
have "x \<le> (x # y # ys) ! j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> (x # y # ys) ! j
[PROOF STEP]
using 3(5) sorted_list_Cons_nth[OF sorted_list.intros(3)[OF 3(1,2)]]
[PROOF STATE]
proof (prove)
using this:
j < length (x # y # ys)
?j < length (y # ys) \<Longrightarrow> x \<le> (y # ys) ! ?j

goal (1 subgoal):
 1. x \<le> (x # y # ys) ! j
[PROOF STEP]
by (auto simp: nth_Cons split: nat.splits)
[PROOF STATE]
proof (state)
this:
x \<le> (x # y # ys) ! j

goal (2 subgoals):
 1. \<And>i j. \<lbrakk>i \<le> j; j < length []\<rbrakk> \<Longrightarrow> [] ! i \<le> [] ! j
 2. \<And>x y ys i j. \<lbrakk>x \<le> y; sorted_list (y # ys); \<And>i j. \<lbrakk>i \<le> j; j < length (y # ys)\<rbrakk> \<Longrightarrow> (y # ys) ! i \<le> (y # ys) ! j; i \<le> j; j < length (x # y # ys)\<rbrakk> \<Longrightarrow> (x # y # ys) ! i \<le> (x # y # ys) ! j
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<le> (x # y # ys) ! j
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<le> (x # y # ys) ! j

goal (1 subgoal):
 1. (x # y # ys) ! i \<le> (x # y # ys) ! j
[PROOF STEP]
using 3
[PROOF STATE]
proof (prove)
using this:
x \<le> (x # y # ys) ! j
x \<le> y
sorted_list (y # ys)
\<lbrakk>?i \<le> ?j; ?j < length (y # ys)\<rbrakk> \<Longrightarrow> (y # ys) ! ?i \<le> (y # ys) ! ?j
i \<le> j
j < length (x # y # ys)

goal (1 subgoal):
 1. (x # y # ys) ! i \<le> (x # y # ys) ! j
[PROOF STEP]
by (cases i) auto
[PROOF STATE]
proof (state)
this:
(x # y # ys) ! i \<le> (x # y # ys) ! j

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i \<le> j; j < length []\<rbrakk> \<Longrightarrow> [] ! i \<le> [] ! j
[PROOF STEP]
qed auto


[STATEMENT]
lemma ssorted_siterate[simp]: "(\<And>n. n \<le> f n) \<Longrightarrow> ssorted (siterate f n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n. n \<le> f n) \<Longrightarrow> ssorted (siterate f n)
[PROOF STEP]
by (coinduction arbitrary: n) auto


[STATEMENT]
lemma ssortedD: "ssorted s \<Longrightarrow> s !! i \<le> stl s !! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ssorted s \<Longrightarrow> s !! i \<le> stl s !! i
[PROOF STEP]
by (induct i arbitrary: s) (auto elim: ssorted.cases)


[STATEMENT]
lemma ssorted_sdrop: "ssorted s \<Longrightarrow> ssorted (sdrop i s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ssorted s \<Longrightarrow> ssorted (sdrop i s)
[PROOF STEP]
by (coinduction arbitrary: i s) (auto elim: ssorted.cases ssortedD)


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

goal (2 subgoals):
 1. \<And>j. \<lbrakk>0 = j - i; ssorted s; i \<le> j\<rbrakk> \<Longrightarrow> s !! i \<le> s !! j
 2. \<And>x j. \<lbrakk>\<And>j. \<lbrakk>x = j - i; ssorted s; i \<le> j\<rbrakk> \<Longrightarrow> s !! i \<le> s !! j; Suc x = j - i; ssorted s; i \<le> j\<rbrakk> \<Longrightarrow> s !! i \<le> s !! j
[PROOF STEP]
from Suc(1)[of "j - 1"] Suc(2-4) ssortedD[of s "j - 1"]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>x = j - 1 - i; ssorted s; i \<le> j - 1\<rbrakk> \<Longrightarrow> s !! i \<le> s !! (j - 1)
Suc x = j - i
ssorted s
i \<le> j
ssorted s \<Longrightarrow> s !! (j - 1) \<le> stl s !! (j - 1)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x = j - 1 - i; ssorted s; i \<le> j - 1\<rbrakk> \<Longrightarrow> s !! i \<le> s !! (j - 1)
Suc x = j - i
ssorted s
i \<le> j
ssorted s \<Longrightarrow> s !! (j - 1) \<le> stl s !! (j - 1)

goal (1 subgoal):
 1. s !! i \<le> s !! j
[PROOF STEP]
by (cases j) (auto simp: le_Suc_eq Suc_diff_le)
[PROOF STATE]
proof (state)
this:
s !! i \<le> s !! j

goal (1 subgoal):
 1. \<And>j. \<lbrakk>0 = j - i; ssorted s; i \<le> j\<rbrakk> \<Longrightarrow> s !! i \<le> s !! j
[PROOF STEP]
qed simp


[STATEMENT]
lemma sorted_stake: "ssorted s \<Longrightarrow> sorted_list (stake i s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ssorted s \<Longrightarrow> sorted_list (stake i s)
[PROOF STEP]
proof (induct i arbitrary: s)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s. ssorted s \<Longrightarrow> sorted_list (stake 0 s)
 2. \<And>i s. \<lbrakk>\<And>s. ssorted s \<Longrightarrow> sorted_list (stake i s); ssorted s\<rbrakk> \<Longrightarrow> sorted_list (stake (Suc i) s)
[PROOF STEP]
case (Suc i)
[PROOF STATE]
proof (state)
this:
ssorted ?s \<Longrightarrow> sorted_list (stake i ?s)
ssorted s

goal (2 subgoals):
 1. \<And>s. ssorted s \<Longrightarrow> sorted_list (stake 0 s)
 2. \<And>i s. \<lbrakk>\<And>s. ssorted s \<Longrightarrow> sorted_list (stake i s); ssorted s\<rbrakk> \<Longrightarrow> sorted_list (stake (Suc i) s)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ssorted ?s \<Longrightarrow> sorted_list (stake i ?s)
ssorted s
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ssorted ?s \<Longrightarrow> sorted_list (stake i ?s)
ssorted s

goal (1 subgoal):
 1. sorted_list (stake (Suc i) s)
[PROOF STEP]
by (cases i) (auto elim: ssorted.cases)
[PROOF STATE]
proof (state)
this:
sorted_list (stake (Suc i) s)

goal (1 subgoal):
 1. \<And>s. ssorted s \<Longrightarrow> sorted_list (stake 0 s)
[PROOF STEP]
qed auto


[STATEMENT]
lemma ssorted_monoI: "\<forall>i j. i \<le> j \<longrightarrow> s !! i \<le> s !! j \<Longrightarrow> ssorted s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i j. i \<le> j \<longrightarrow> s !! i \<le> s !! j \<Longrightarrow> ssorted s
[PROOF STEP]
by (coinduction arbitrary: s)
    (auto dest: spec2[of _ "Suc _" "Suc _"] spec2[of _ 0 "Suc 0"])


[STATEMENT]
lemma ssorted_iff_mono: "ssorted s \<longleftrightarrow> (\<forall>i j. i \<le> j \<longrightarrow> s !! i \<le> s !! j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ssorted s = (\<forall>i j. i \<le> j \<longrightarrow> s !! i \<le> s !! j)
[PROOF STEP]
using ssorted_monoI ssorted_monoD
[PROOF STATE]
proof (prove)
using this:
\<forall>i j. i \<le> j \<longrightarrow> ?s !! i \<le> ?s !! j \<Longrightarrow> ssorted ?s
\<lbrakk>ssorted ?s; ?i \<le> ?j\<rbrakk> \<Longrightarrow> ?s !! ?i \<le> ?s !! ?j

goal (1 subgoal):
 1. ssorted s = (\<forall>i j. i \<le> j \<longrightarrow> s !! i \<le> s !! j)
[PROOF STEP]
by metis


[STATEMENT]
lemma \<tau>_mono[simp]: "i \<le> j \<Longrightarrow> \<tau> s i \<le> \<tau> s j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<le> j \<Longrightarrow> \<tau> s i \<le> \<tau> s j
[PROOF STEP]
by transfer (auto simp: ssorted_iff_mono)


[STATEMENT]
lemma \<tau>_fin: "\<tau> \<sigma> i \<in> tfin"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau> \<sigma> i \<in> tfin
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma ex_lt_\<tau>: "x \<in> tfin \<Longrightarrow> \<exists>j. \<not>\<tau> s j \<le> \<tau> s i + x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> tfin \<Longrightarrow> \<exists>j. \<not> \<tau> s j \<le> \<tau> s i + x
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma le_\<tau>_less: "\<tau> \<sigma> i \<le> \<tau> \<sigma> j \<Longrightarrow> j < i \<Longrightarrow> \<tau> \<sigma> i = \<tau> \<sigma> j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<tau> \<sigma> i \<le> \<tau> \<sigma> j; j < i\<rbrakk> \<Longrightarrow> \<tau> \<sigma> i = \<tau> \<sigma> j
[PROOF STEP]
by (simp add: antisym)


[STATEMENT]
lemma less_\<tau>D: "\<tau> \<sigma> i < \<tau> \<sigma> j \<Longrightarrow> i < j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau> \<sigma> i < \<tau> \<sigma> j \<Longrightarrow> i < j
[PROOF STEP]
by (meson \<tau>_mono less_le_not_le not_le_imp_less)


[STATEMENT]
lemma mem_fset_from_list[simp]: "x |\<in>| fset_from_list l  \<longleftrightarrow> x \<in> set l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x |\<in>| fset_from_list l) = (x \<in> set l)
[PROOF STEP]
by transfer rule


[STATEMENT]
lemma fimage_fset_from_list[simp]: "f |`| fset_from_list l = fset_from_list (map f l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f |`| fset_from_list l = fset_from_list (map f l)
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma fset_fset_from_list[simp]: "fset (fset_from_list l) = set l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fset (fset_from_list l) = set l
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma size_fset_from_list[simp]: "distinct l \<Longrightarrow> size (fset_from_list l) = length l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct l \<Longrightarrow> size (fset_from_list l) = length l
[PROOF STEP]
by (induction l) auto


[STATEMENT]
lemma fset_from_list_of_fset[simp]: "fset_from_list (list_of_fset s) = s"
  and distinct_list_of_fset[simp]: "distinct (list_of_fset s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fset_from_list (list_of_fset s) = s &&& distinct (list_of_fset s)
[PROOF STEP]
unfolding atomize_conj list_of_fset_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fset_from_list (SOME l. fset_from_list l = s \<and> distinct l) = s \<and> distinct (SOME l. fset_from_list l = s \<and> distinct l)
[PROOF STEP]
by (transfer, rule someI_ex, rule finite_distinct_list)


[STATEMENT]
lemma length_list_of_fset[simp]: "length (list_of_fset s) = size s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (list_of_fset s) = size s
[PROOF STEP]
by (metis distinct_list_of_fset fset_from_list_of_fset size_fset_from_list)


[STATEMENT]
lemma nth_list_of_fset_mem[simp]: "i < size s \<Longrightarrow> list_of_fset s ! i |\<in>| s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < size s \<Longrightarrow> list_of_fset s ! i |\<in>| s
[PROOF STEP]
by (metis fset_from_list_of_fset length_list_of_fset mem_fset_from_list nth_mem)


[STATEMENT]
lemma indexed_fmember_is_fmember: "x |\<in>|\<^bsub>i\<^esub> s \<Longrightarrow> x |\<in>| s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x |\<in>|\<^bsub>i\<^esub> s \<Longrightarrow> x |\<in>| s
[PROOF STEP]
proof (induction rule: indexed_fmember.induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i s. i < size s \<Longrightarrow> list_of_fset s ! i |\<in>| s
[PROOF STEP]
case (1 i s)
[PROOF STATE]
proof (state)
this:
i < size s

goal (1 subgoal):
 1. \<And>i s. i < size s \<Longrightarrow> list_of_fset s ! i |\<in>| s
[PROOF STEP]
hence "i < length (list_of_fset s)"
[PROOF STATE]
proof (prove)
using this:
i < size s

goal (1 subgoal):
 1. i < length (list_of_fset s)
[PROOF STEP]
by (metis length_list_of_fset)
[PROOF STATE]
proof (state)
this:
i < length (list_of_fset s)

goal (1 subgoal):
 1. \<And>i s. i < size s \<Longrightarrow> list_of_fset s ! i |\<in>| s
[PROOF STEP]
hence "list_of_fset s ! i \<in> set (list_of_fset s)"
[PROOF STATE]
proof (prove)
using this:
i < length (list_of_fset s)

goal (1 subgoal):
 1. list_of_fset s ! i \<in> set (list_of_fset s)
[PROOF STEP]
by (rule nth_mem)
[PROOF STATE]
proof (state)
this:
list_of_fset s ! i \<in> set (list_of_fset s)

goal (1 subgoal):
 1. \<And>i s. i < size s \<Longrightarrow> list_of_fset s ! i |\<in>| s
[PROOF STEP]
thus "list_of_fset s ! i |\<in>| s"
[PROOF STATE]
proof (prove)
using this:
list_of_fset s ! i \<in> set (list_of_fset s)

goal (1 subgoal):
 1. list_of_fset s ! i |\<in>| s
[PROOF STEP]
by (metis mem_fset_from_list fset_from_list_of_fset)
[PROOF STATE]
proof (state)
this:
list_of_fset s ! i |\<in>| s

goal:
No subgoals!
[PROOF STEP]
qed