Theory CardinalArith_Relative
section‹Relative, Choice-less Cardinal Arithmetic›
theory CardinalArith_Relative
imports
Cardinal_Relative
begin
relativize functional "rvimage" "rvimage_rel" external
relationalize "rvimage_rel" "is_rvimage"
definition
csquare_lam :: "i⇒i" where
"csquare_lam(K) ≡ λ⟨x,y⟩∈K×K. ⟨x ∪ y, x, y⟩"
relativize_tm "⟨fst(x) ∪ snd(x), fst(x), snd(x)⟩" "is_csquare_lam_body"
definition
is_csquare_lam :: "[i⇒o,i,i]⇒o" where
"is_csquare_lam(M,K,l) ≡ ∃K2[M]. cartprod(M,K,K,K2) ∧
is_lambda(M,K2,is_csquare_lam_body(M),l)"
definition jump_cardinal_body :: "[i,i] ⇒ i" where
"jump_cardinal_body(U,X) ≡
{z . r ∈ U, well_ord(X, r) ∧ z = ordertype(X, r)}"
lemma jump_cardinal_body_char :
"jump_cardinal_body(U,X) = {ordertype(X, r) . r ∈ {r∈U . well_ord(X, r)}}"
unfolding jump_cardinal_body_def
by auto
definition jump_cardinal_body' where
"jump_cardinal_body'(x) ≡ jump_cardinal_body(Pow(x×x),x)"
lemma (in M_cardinals) csquare_lam_closed[intro,simp]: "M(K) ⟹ M(csquare_lam(K))"
using csquare_lam_replacement unfolding csquare_lam_def
by (rule lam_closed) (auto dest:transM)
locale M_pre_cardinal_arith = M_cardinals +
assumes
wfrec_pred_replacement:"M(A) ⟹ M(r) ⟹
wfrec_replacement(M, λx f z. z = f `` Order.pred(A, x, r), r)"
relativize_tm "∃x' y' x y. z = ⟨⟨x', y'⟩, x, y⟩ ∧ (⟨x', x⟩ ∈ r ∨ x' = x ∧ ⟨y', y⟩ ∈ s)"
"is_rmultP"
relativize functional "rmult" "rmult_rel" external
relationalize "rmult_rel" "is_rmult"
lemma (in M_trivial) rmultP_abs [absolut]: "⟦ M(r); M(s); M(z) ⟧ ⟹ is_rmultP(M,s,r,z) ⟷
(∃x' y' x y. z = ⟨⟨x', y'⟩, x, y⟩ ∧ (⟨x', x⟩ ∈ r ∨ x' = x ∧ ⟨y', y⟩ ∈ s))"
unfolding is_rmultP_def by (auto dest:transM)
definition
is_csquare_rel :: "[i⇒o,i,i]⇒o" where
"is_csquare_rel(M,K,cs) ≡ ∃K2[M]. ∃la[M]. ∃memK[M].
∃rmKK[M]. ∃rmKK2[M].
cartprod(M,K,K,K2) ∧ is_csquare_lam(M,K,la) ∧
membership(M,K,memK) ∧ is_rmult(M,K,memK,K,memK,rmKK) ∧
is_rmult(M,K,memK,K2,rmKK,rmKK2) ∧ is_rvimage(M,K2,la,rmKK2,cs)"
context M_basic
begin
lemma rvimage_abs[absolut]:
assumes "M(A)" "M(f)" "M(r)" "M(z)"
shows "is_rvimage(M,A,f,r,z) ⟷ z = rvimage(A,f,r)"
using assms transM[OF _ ‹M(A)›]
unfolding is_rvimage_def rvimage_def
by auto
lemma rmult_abs [absolut]: "⟦ M(A); M(r); M(B); M(s); M(z) ⟧ ⟹
is_rmult(M,A,r,B,s,z) ⟷ z=rmult(A,r,B,s)"
using rmultP_abs transM[of _ "(A × B) × A × B"]
unfolding is_rmultP_def is_rmult_def rmult_def
by (auto del: iffI)
lemma csquare_lam_body_abs[absolut]: "M(x) ⟹ M(z) ⟹
is_csquare_lam_body(M,x,z) ⟷ z = <fst(x) ∪ snd(x), fst(x), snd(x)>"
unfolding is_csquare_lam_body_def by (simp add:absolut)
lemma csquare_lam_abs[absolut]: "M(K) ⟹ M(l) ⟹
is_csquare_lam(M,K,l) ⟷ l = (λx∈K×K. ⟨fst(x) ∪ snd(x), fst(x), snd(x)⟩)"
unfolding is_csquare_lam_def
using lambda_abs2[of "K×K" "is_csquare_lam_body(M)"
"λx. ⟨fst(x) ∪ snd(x), fst(x), snd(x)⟩"]
unfolding Relation1_def by (simp add:absolut)
lemma csquare_lam_eq_lam:"csquare_lam(K) = (λz∈K×K. <fst(z) ∪ snd(z), fst(z), snd(z)>)"
proof -
have "(λ⟨x,y⟩∈K × K. ⟨x ∪ y, x, y⟩)`z =
(λz∈K×K. <fst(z) ∪ snd(z), fst(z), snd(z)>)`z" if "z∈K×K" for z
using that by auto
then
show ?thesis
unfolding csquare_lam_def
by simp
qed
end
context M_pre_cardinal_arith
begin
lemma csquare_rel_closed[intro,simp]: "M(K) ⟹ M(csquare_rel(K))"
using csquare_lam_replacement unfolding csquare_rel_def
by (intro rvimage_closed lam_closed) (auto dest:transM)
lemma csquare_rel_abs[absolut]: "⟦ M(K); M(cs)⟧ ⟹
is_csquare_rel(M,K,cs) ⟷ cs = csquare_rel(K)"
using csquare_lam_closed[unfolded csquare_lam_eq_lam]
unfolding is_csquare_rel_def csquare_rel_def
by (simp add:absolut csquare_lam_eq_lam[unfolded csquare_lam_def])
end
subsection‹Discipline for \<^term>‹csucc››
relativize functional "csucc" "csucc_rel" external
relationalize "csucc_rel" "is_csucc"
synthesize "is_csucc" from_definition assuming "nonempty"
arity_theorem for "is_csucc_fm"
abbreviation
csucc_r :: "[i,i⇒o] ⇒ i" (‹'(_⇧+')⇗_⇖›) where
"csucc_r(x,M) ≡ csucc_rel(M,x)"
abbreviation
csucc_r_set :: "[i,i] ⇒ i" (‹'(_⇧+')⇗_⇖›) where
"csucc_r_set(x,M) ≡ csucc_rel(##M,x)"
context M_Perm
begin
rel_closed for "csucc"
using Least_closed'[of "λ L. M(L) ∧ Card⇗M⇖(L) ∧ K < L"]
unfolding csucc_rel_def
by simp
is_iff_rel for "csucc"
using least_abs'[of "λ L. M(L) ∧ Card⇗M⇖(L) ∧ K < L" res]
is_Card_iff
unfolding is_csucc_def csucc_rel_def
by (simp add:absolut)
end
notation csucc_rel (‹csucc⇗_⇖'(_')›)
context M_cardinals
begin
lemma Card_rel_Union [simp,intro,TC]:
assumes A: "⋀x. x∈A ⟹ Card⇗M⇖(x)" and
types:"M(A)"
shows "Card⇗M⇖(⋃(A))"
proof (rule Card_relI)
show "Ord(⋃A)" using A
by (simp add: Card_rel_is_Ord types transM)
next
fix j
assume j: "j < ⋃A"
moreover from this
have "M(j)" unfolding lt_def by (auto simp add:types dest:transM)
from j
have "∃c∈A. j ∈ c ∧ Card⇗M⇖(c)" using A types
unfolding lt_def
by (simp)
then
obtain c where c: "c∈A" "j < c" "Card⇗M⇖(c)" "M(c)"
using Card_rel_is_Ord types unfolding lt_def
by (auto dest:transM)
with ‹M(j)›
have jls: "j ≺⇗M⇖ c"
by (simp add: lt_Card_rel_imp_lesspoll_rel types)
{ assume eqp: "j ≈⇗M⇖ ⋃A"
have "c ≲⇗M⇖ ⋃A" using c
by (blast intro: subset_imp_lepoll_rel types)
also from types ‹M(j)›
have "... ≈⇗M⇖ j" by (rule_tac eqpoll_rel_sym [OF eqp]) (simp_all add:types)
also have "... ≺⇗M⇖ c" by (rule jls)
finally have "c ≺⇗M⇖ c" by (simp_all add:‹M(c)› ‹M(j)› types)
with ‹M(c)›
have False
by (auto dest:lesspoll_rel_irrefl)
} thus "¬ j ≈⇗M⇖ ⋃A" by blast
qed (simp_all add:types)
text‹We are not relativizing directly the results involving unions of
(ordinal) indexed families (namely, @{thm [source] Card_UN} and
@{thm [source] Card_OUN}, respectively) because of their higher order nature.›
lemma in_Card_imp_lesspoll: "[| Card⇗M⇖(K); b ∈ K; M(K); M(b) |] ==> b ≺⇗M⇖ K"
apply (unfold lesspoll_rel_def)
apply (simp add: Card_rel_iff_initial)
apply (fast intro!: le_imp_lepoll_rel ltI leI)
done
subsection‹Cardinal addition›
text‹Note (Paulson): Could omit proving the algebraic laws for cardinal addition and
multiplication. On finite cardinals these operations coincide with
addition and multiplication of natural numbers; on infinite cardinals they
coincide with union (maximum). Either way we get most laws for free.›
subsubsection‹Cardinal addition is commutative›
lemma sum_commute_eqpoll_rel: "M(A) ⟹ M(B) ⟹ A+B ≈⇗M⇖ B+A"
proof (simp add: def_eqpoll_rel, rule rexI)
show "(λz∈A+B. case(Inr,Inl,z)) ∈ bij(A+B, B+A)"
by (auto intro: lam_bijective [where d = "case(Inr,Inl)"])
assume "M(A)" "M(B)"
then
show "M(λz∈A + B. case(Inr, Inl, z))"
using case_replacement1
by (rule_tac lam_closed) (auto dest:transM)
qed
lemma cadd_rel_commute: "M(i) ⟹ M(j) ⟹ i ⊕⇗M⇖ j = j ⊕⇗M⇖ i"
apply (unfold cadd_rel_def)
apply (auto intro: sum_commute_eqpoll_rel [THEN cardinal_rel_cong])
done
subsubsection‹Cardinal addition is associative›
lemma sum_assoc_eqpoll_rel: "M(A) ⟹ M(B) ⟹ M(C) ⟹ (A+B)+C ≈⇗M⇖ A+(B+C)"
apply (simp add: def_eqpoll_rel)
apply (rule rexI)
apply (rule sum_assoc_bij)
using case_replacement2
by (rule_tac lam_closed) (auto dest:transM)
text‹Unconditional version requires AC›
lemma well_ord_cadd_rel_assoc:
assumes i: "well_ord(i,ri)" and j: "well_ord(j,rj)" and k: "well_ord(k,rk)"
and
types: "M(i)" "M(ri)" "M(j)" "M(rj)" "M(k)" "M(rk)"
shows "(i ⊕⇗M⇖ j) ⊕⇗M⇖ k = i ⊕⇗M⇖ (j ⊕⇗M⇖ k)"
proof (simp add: assms cadd_rel_def, rule cardinal_rel_cong)
from types
have "|i + j|⇗M⇖ + k ≈⇗M⇖ (i + j) + k"
by (auto intro!: sum_eqpoll_rel_cong well_ord_cardinal_rel_eqpoll_rel eqpoll_rel_refl well_ord_radd i j)
also have "... ≈⇗M⇖ i + (j + k)"
by (rule sum_assoc_eqpoll_rel) (simp_all add:types)
also
have "... ≈⇗M⇖ i + |j + k|⇗M⇖"
proof (auto intro!: sum_eqpoll_rel_cong intro:eqpoll_rel_refl simp add:types)
from types
have "|j + k|⇗M⇖ ≈⇗M⇖ j + k"
using well_ord_cardinal_rel_eqpoll_rel[OF well_ord_radd, OF j k]
by (simp)
with types
show "j + k ≈⇗M⇖ |j + k|⇗M⇖"
using eqpoll_rel_sym by simp
qed
finally show "|i + j|⇗M⇖ + k ≈⇗M⇖ i + |j + k|⇗M⇖" by (simp_all add:types)
qed (simp_all add:types)
subsubsection‹0 is the identity for addition›
lemma case_id_eq: "x∈sum(A,B) ⟹ case(λz . z, λz. z ,x) = snd(x)"
unfolding case_def cond_def by (auto simp:Inl_def Inr_def)
lemma lam_case_id: "(λz∈0 + A. case(λx. x, λy. y, z)) = (λz∈0 + A . snd(z))"
using case_id_eq by simp
lemma sum_0_eqpoll_rel: "M(A) ⟹ 0+A ≈⇗M⇖ A"
apply (simp add:def_eqpoll_rel)
apply (rule rexI)
apply (rule bij_0_sum,subst lam_case_id)
using lam_replacement_snd[unfolded lam_replacement_def]
by (rule lam_closed)
(auto simp add:case_def cond_def Inr_def dest:transM)
lemma cadd_rel_0 [simp]: "Card⇗M⇖(K) ⟹ M(K) ⟹ 0 ⊕⇗M⇖ K = K"
apply (simp add: cadd_rel_def)
apply (simp add: sum_0_eqpoll_rel [THEN cardinal_rel_cong] Card_rel_cardinal_rel_eq)
done
subsubsection‹Addition by another cardinal›
lemma sum_lepoll_rel_self: "M(A) ⟹ M(B) ⟹ A ≲⇗M⇖ A+B"
proof (simp add: def_lepoll_rel, rule rexI)
show "(λx∈A. Inl (x)) ∈ inj(A, A + B)"
by (simp add: inj_def)
assume "M(A)" "M(B)"
then
show "M(λx∈A. Inl(x))"
using Inl_replacement1 transM[OF _ ‹M(A)›]
by (rule_tac lam_closed) (auto simp add: Inl_def)
qed
lemma cadd_rel_le_self:
assumes K: "Card⇗M⇖(K)" and L: "Ord(L)" and
types:"M(K)" "M(L)"
shows "K ≤ (K ⊕⇗M⇖ L)"
proof (simp add:types cadd_rel_def)
have "K ≤ |K|⇗M⇖"
by (rule Card_rel_cardinal_rel_le [OF K]) (simp add:types)
moreover have "|K|⇗M⇖ ≤ |K + L|⇗M⇖" using K L
by (blast intro: well_ord_lepoll_rel_imp_cardinal_rel_le sum_lepoll_rel_self
well_ord_radd well_ord_Memrel Card_rel_is_Ord types)
ultimately show "K ≤ |K + L|⇗M⇖"
by (blast intro: le_trans)
qed
subsubsection‹Monotonicity of addition›
lemma sum_lepoll_rel_mono:
"[| A ≲⇗M⇖ C; B ≲⇗M⇖ D; M(A); M(B); M(C); M(D) |] ==> A + B ≲⇗M⇖ C + D"
apply (simp add: def_lepoll_rel)
apply (elim rexE)
apply (rule_tac x = "λz∈A+B. case (%w. Inl(f`w), %y. Inr(fa`y), z)" in rexI)
apply (rule_tac d = "case (%w. Inl(converse(f) `w), %y. Inr(converse(fa) ` y))"
in lam_injective)
apply (typecheck add: inj_is_fun, auto)
apply (rule_tac lam_closed, auto dest:transM intro:case_replacement4)
done
lemma cadd_rel_le_mono:
"[| K' ≤ K; L' ≤ L;M(K');M(K);M(L');M(L) |] ==> (K' ⊕⇗M⇖ L') ≤ (K ⊕⇗M⇖ L)"
apply (unfold cadd_rel_def)
apply (safe dest!: le_subset_iff [THEN iffD1])
apply (rule well_ord_lepoll_rel_imp_cardinal_rel_le)
apply (blast intro: well_ord_radd well_ord_Memrel)
apply (auto intro: sum_lepoll_rel_mono subset_imp_lepoll_rel)
done
subsubsection‹Addition of finite cardinals is "ordinary" addition›
lemma sum_succ_eqpoll_rel: "M(A) ⟹ M(B) ⟹ succ(A)+B ≈⇗M⇖ succ(A+B)"
apply (simp add:def_eqpoll_rel)
apply (rule rexI)
apply (rule_tac c = "%z. if z=Inl (A) then A+B else z"
and d = "%z. if z=A+B then Inl (A) else z" in lam_bijective)
apply simp_all
apply (blast dest: sym [THEN eq_imp_not_mem] elim: mem_irrefl)+
apply(rule_tac lam_closed, auto dest:transM intro:if_then_range_replacement2)
done
lemma cadd_succ_lemma:
assumes "Ord(m)" "Ord(n)" and
types: "M(m)" "M(n)"
shows "succ(m) ⊕⇗M⇖ n = |succ(m ⊕⇗M⇖ n)|⇗M⇖"
using types
proof (simp add: cadd_rel_def)
have [intro]: "m + n ≈⇗M⇖ |m + n|⇗M⇖" using assms
by (blast intro: eqpoll_rel_sym well_ord_cardinal_rel_eqpoll_rel well_ord_radd well_ord_Memrel)
have "|succ(m) + n|⇗M⇖ = |succ(m + n)|⇗M⇖"
by (rule sum_succ_eqpoll_rel [THEN cardinal_rel_cong]) (simp_all add:types)
also have "... = |succ(|m + n|⇗M⇖)|⇗M⇖"
by (blast intro: succ_eqpoll_rel_cong cardinal_rel_cong types)
finally show "|succ(m) + n|⇗M⇖ = |succ(|m + n|⇗M⇖)|⇗M⇖" .
qed
lemma nat_cadd_rel_eq_add:
assumes m: "m ∈ nat" and [simp]: "n ∈ nat" shows"m ⊕⇗M⇖ n = m +⇩ω n"
using m
proof (induct m)
case 0 thus ?case
using transM[OF _ M_nat]
by (auto simp add: nat_into_Card_rel)
next
case (succ m) thus ?case
using transM[OF _ M_nat]
by (simp add: cadd_succ_lemma nat_into_Card_rel Card_rel_cardinal_rel_eq)
qed
subsection‹Cardinal multiplication›
subsubsection‹Cardinal multiplication is commutative›
lemma prod_commute_eqpoll_rel: "M(A) ⟹ M(B) ⟹ A*B ≈⇗M⇖ B*A"
apply (simp add: def_eqpoll_rel)
apply (rule rexI)
apply (rule_tac c = "%<x,y>.<y,x>" and d = "%<x,y>.<y,x>" in lam_bijective,
auto)
apply(rule_tac lam_closed, auto intro:swap_replacement dest:transM)
done
lemma cmult_rel_commute: "M(i) ⟹ M(j) ⟹ i ⊗⇗M⇖ j = j ⊗⇗M⇖ i"
apply (unfold cmult_rel_def)
apply (rule prod_commute_eqpoll_rel [THEN cardinal_rel_cong], simp_all)
done
subsubsection‹Cardinal multiplication is associative›
lemma prod_assoc_eqpoll_rel: "M(A) ⟹ M(B) ⟹ M(C) ⟹ (A*B)*C ≈⇗M⇖ A*(B*C)"
apply (simp add: def_eqpoll_rel)
apply (rule rexI)
apply (rule prod_assoc_bij)
apply(rule_tac lam_closed, auto intro:assoc_replacement dest:transM)
done
text‹Unconditional version requires AC›
lemma well_ord_cmult_rel_assoc:
assumes i: "well_ord(i,ri)" and j: "well_ord(j,rj)" and k: "well_ord(k,rk)"
and
types: "M(i)" "M(ri)" "M(j)" "M(rj)" "M(k)" "M(rk)"
shows "(i ⊗⇗M⇖ j) ⊗⇗M⇖ k = i ⊗⇗M⇖ (j ⊗⇗M⇖ k)"
proof (simp add: assms cmult_rel_def, rule cardinal_rel_cong)
have "|i * j|⇗M⇖ * k ≈⇗M⇖ (i * j) * k"
by (auto intro!: prod_eqpoll_rel_cong
well_ord_cardinal_rel_eqpoll_rel eqpoll_rel_refl
well_ord_rmult i j simp add:types)
also have "... ≈⇗M⇖ i * (j * k)"
by (rule prod_assoc_eqpoll_rel, simp_all add:types)
also have "... ≈⇗M⇖ i * |j * k|⇗M⇖"
by (blast intro: prod_eqpoll_rel_cong well_ord_cardinal_rel_eqpoll_rel
eqpoll_rel_refl well_ord_rmult j k eqpoll_rel_sym types)
finally show "|i * j|⇗M⇖ * k ≈⇗M⇖ i * |j * k|⇗M⇖" by (simp add:types)
qed (simp_all add:types)
subsubsection‹Cardinal multiplication distributes over addition›
lemma sum_prod_distrib_eqpoll_rel: "M(A) ⟹ M(B) ⟹ M(C) ⟹ (A+B)*C ≈⇗M⇖ (A*C)+(B*C)"
apply (simp add: def_eqpoll_rel)
apply (rule rexI)
apply (rule sum_prod_distrib_bij)
apply(rule_tac lam_closed, auto intro:case_replacement5 dest:transM)
done
lemma well_ord_cadd_cmult_distrib:
assumes i: "well_ord(i,ri)" and j: "well_ord(j,rj)" and k: "well_ord(k,rk)"
and
types: "M(i)" "M(ri)" "M(j)" "M(rj)" "M(k)" "M(rk)"
shows "(i ⊕⇗M⇖ j) ⊗⇗M⇖ k = (i ⊗⇗M⇖ k) ⊕⇗M⇖ (j ⊗⇗M⇖ k)"
proof (simp add: assms cadd_rel_def cmult_rel_def, rule cardinal_rel_cong)
have "|i + j|⇗M⇖ * k ≈⇗M⇖ (i + j) * k"
by (blast intro: prod_eqpoll_rel_cong well_ord_cardinal_rel_eqpoll_rel
eqpoll_rel_refl well_ord_radd i j types)
also have "... ≈⇗M⇖ i * k + j * k"
by (rule sum_prod_distrib_eqpoll_rel) (simp_all add:types)
also have "... ≈⇗M⇖ |i * k|⇗M⇖ + |j * k|⇗M⇖"
by (blast intro: sum_eqpoll_rel_cong well_ord_cardinal_rel_eqpoll_rel
well_ord_rmult i j k eqpoll_rel_sym types)
finally show "|i + j|⇗M⇖ * k ≈⇗M⇖ |i * k|⇗M⇖ + |j * k|⇗M⇖" by (simp add:types)
qed (simp_all add:types)
subsubsection‹Multiplication by 0 yields 0›
lemma prod_0_eqpoll_rel: "M(A) ⟹ 0*A ≈⇗M⇖ 0"
apply (simp add: def_eqpoll_rel)
apply (rule rexI)
apply (rule lam_bijective, auto)
done
lemma cmult_rel_0 [simp]: "M(i) ⟹ 0 ⊗⇗M⇖ i = 0"
by (simp add: cmult_rel_def prod_0_eqpoll_rel [THEN cardinal_rel_cong])
subsubsection‹1 is the identity for multiplication›
lemma prod_singleton_eqpoll_rel: "M(x) ⟹ M(A) ⟹ {x}*A ≈⇗M⇖ A"
apply (simp add: def_eqpoll_rel)
apply (rule rexI)
apply (rule singleton_prod_bij [THEN bij_converse_bij])
apply (rule converse_closed)
apply(rule_tac lam_closed, auto intro:prepend_replacement dest:transM)
done
lemma cmult_rel_1 [simp]: "Card⇗M⇖(K) ⟹ M(K) ⟹ 1 ⊗⇗M⇖ K = K"
apply (simp add: cmult_rel_def succ_def)
apply (simp add: prod_singleton_eqpoll_rel[THEN cardinal_rel_cong] Card_rel_cardinal_rel_eq)
done
subsection‹Some inequalities for multiplication›
lemma prod_square_lepoll_rel: "M(A) ⟹ A ≲⇗M⇖ A*A"
apply (simp add:def_lepoll_rel inj_def)
apply (rule_tac x = "λx∈A. <x,x>" in rexI, simp)
apply(rule_tac lam_closed, auto intro:id_replacement dest:transM)
done
lemma cmult_rel_square_le: "Card⇗M⇖(K) ⟹ M(K) ⟹ K ≤ K ⊗⇗M⇖ K"
apply (unfold cmult_rel_def)
apply (rule le_trans)
apply (rule_tac [2] well_ord_lepoll_rel_imp_cardinal_rel_le)
apply (rule_tac [3] prod_square_lepoll_rel)
apply (simp add: le_refl Card_rel_is_Ord Card_rel_cardinal_rel_eq)
apply (blast intro: well_ord_rmult well_ord_Memrel Card_rel_is_Ord)
apply simp_all
done
subsubsection‹Multiplication by a non-zero cardinal›
lemma prod_lepoll_rel_self: "b ∈ B ⟹ M(b) ⟹ M(B) ⟹ M(A) ⟹ A ≲⇗M⇖ A*B"
apply (simp add: def_lepoll_rel inj_def)
apply (rule_tac x = "λx∈A. <x,b>" in rexI, simp)
apply(rule_tac lam_closed, auto intro:pospend_replacement dest:transM)
done
lemma cmult_rel_le_self:
"[| Card⇗M⇖(K); Ord(L); 0<L; M(K);M(L) |] ==> K ≤ (K ⊗⇗M⇖ L)"
apply (unfold cmult_rel_def)
apply (rule le_trans [OF Card_rel_cardinal_rel_le well_ord_lepoll_rel_imp_cardinal_rel_le])
apply assumption apply simp
apply (blast intro: well_ord_rmult well_ord_Memrel Card_rel_is_Ord)
apply (auto intro: prod_lepoll_rel_self ltD)
done
subsubsection‹Monotonicity of multiplication›
lemma prod_lepoll_rel_mono:
"[| A ≲⇗M⇖ C; B ≲⇗M⇖ D; M(A); M(B); M(C); M(D)|] ==> A * B ≲⇗M⇖ C * D"
apply (simp add:def_lepoll_rel)
apply (elim rexE)
apply (rule_tac x = "lam <w,y>:A*B. <f`w, fa`y>" in rexI)
apply (rule_tac d = "%<w,y>. <converse (f) `w, converse (fa) `y>"
in lam_injective)
apply (typecheck add: inj_is_fun, auto)
apply(rule_tac lam_closed, auto intro:prod_fun_replacement dest:transM)
done
lemma cmult_rel_le_mono:
"[| K' ≤ K; L' ≤ L;M(K');M(K);M(L');M(L) |] ==> (K' ⊗⇗M⇖ L') ≤ (K ⊗⇗M⇖ L)"
apply (unfold cmult_rel_def)
apply (safe dest!: le_subset_iff [THEN iffD1])
apply (rule well_ord_lepoll_rel_imp_cardinal_rel_le)
apply (blast intro: well_ord_rmult well_ord_Memrel)
apply (auto intro: prod_lepoll_rel_mono subset_imp_lepoll_rel)
done
subsection‹Multiplication of finite cardinals is "ordinary" multiplication›
lemma prod_succ_eqpoll_rel: "M(A) ⟹ M(B) ⟹ succ(A)*B ≈⇗M⇖ B + A*B"
apply (simp add: def_eqpoll_rel)
apply (rule rexI)
apply (rule_tac c = "λp. if fst(p)=A then Inl (snd(p)) else Inr (p)"
and d = "case (%y. <A,y>, %z. z)" in lam_bijective)
apply safe
apply (simp_all add: succI2 if_type mem_imp_not_eq)
apply(rule_tac lam_closed, auto intro:Inl_replacement2 dest:transM)
done
lemma cmult_rel_succ_lemma:
"[| Ord(m); Ord(n) ; M(m); M(n) |] ==> succ(m) ⊗⇗M⇖ n = n ⊕⇗M⇖ (m ⊗⇗M⇖ n)"
apply (simp add: cmult_rel_def cadd_rel_def)
apply (rule prod_succ_eqpoll_rel [THEN cardinal_rel_cong, THEN trans], simp_all)
apply (rule cardinal_rel_cong [symmetric], simp_all)
apply (rule sum_eqpoll_rel_cong [OF eqpoll_rel_refl well_ord_cardinal_rel_eqpoll_rel], assumption)
apply (blast intro: well_ord_rmult well_ord_Memrel)
apply simp_all
done
lemma nat_cmult_rel_eq_mult: "[| m ∈ nat; n ∈ nat |] ==> m ⊗⇗M⇖ n = m#*n"
using transM[OF _ M_nat]
apply (induct_tac m)
apply (simp_all add: cmult_rel_succ_lemma nat_cadd_rel_eq_add)
done
lemma cmult_rel_2: "Card⇗M⇖(n) ⟹ M(n) ⟹ 2 ⊗⇗M⇖ n = n ⊕⇗M⇖ n"
by (simp add: cmult_rel_succ_lemma Card_rel_is_Ord cadd_rel_commute [of _ 0])
lemma sum_lepoll_rel_prod:
assumes C: "2 ≲⇗M⇖ C" and
types:"M(C)" "M(B)"
shows "B+B ≲⇗M⇖ C*B"
proof -
have "B+B ≲⇗M⇖ 2*B"
by (simp add: sum_eq_2_times types)
also have "... ≲⇗M⇖ C*B"
by (blast intro: prod_lepoll_rel_mono lepoll_rel_refl C types)
finally show "B+B ≲⇗M⇖ C*B" by (simp_all add:types)
qed
lemma lepoll_imp_sum_lepoll_prod: "[| A ≲⇗M⇖ B; 2 ≲⇗M⇖ A; M(A) ;M(B) |] ==> A+B ≲⇗M⇖ A*B"
by (blast intro: sum_lepoll_rel_mono sum_lepoll_rel_prod lepoll_rel_trans lepoll_rel_refl)
end
subsection‹Infinite Cardinals are Limit Ordinals›
context M_pre_cardinal_arith
begin
lemma nat_cons_lepoll_rel: "nat ≲⇗M⇖ A ⟹ M(A) ⟹ M(u) ==> cons(u,A) ≲⇗M⇖ A"
apply (simp add: def_lepoll_rel)
apply (erule rexE)
apply (rule_tac x =
"λz∈cons (u,A).
if z=u then f`0
else if z ∈ range (f) then f`succ (converse (f) `z) else z"
in rexI)
apply (rule_tac d =
"%y. if y ∈ range(f) then nat_case (u, %z. f`z, converse(f) `y)
else y"
in lam_injective)
apply (fast intro!: if_type apply_type intro: inj_is_fun inj_converse_fun)
apply (simp add: inj_is_fun [THEN apply_rangeI]
inj_converse_fun [THEN apply_rangeI]
inj_converse_fun [THEN apply_funtype])
proof -
fix f
assume "M(A)" "M(f)" "M(u)"
then
show "M(λz∈cons(u, A). if z = u then f ` 0 else if z ∈ range(f) then f ` succ(converse(f) ` z) else z)"
using if_then_range_replacement transM[OF _ ‹M(A)›]
by (rule_tac lam_closed, auto)
qed
lemma nat_cons_eqpoll_rel: "nat ≲⇗M⇖ A ==> M(A) ⟹ M(u) ⟹ cons(u,A) ≈⇗M⇖ A"
apply (erule nat_cons_lepoll_rel [THEN eqpoll_relI], assumption+)
apply (rule subset_consI [THEN subset_imp_lepoll_rel], simp_all)
done
lemma nat_succ_eqpoll_rel: "nat ⊆ A ==> M(A) ⟹ succ(A) ≈⇗M⇖ A"
apply (unfold succ_def)
apply (erule subset_imp_lepoll_rel [THEN nat_cons_eqpoll_rel], simp_all)
done
lemma InfCard_rel_nat: "InfCard⇗M⇖(nat)"
apply (simp add: InfCard_rel_def)
apply (blast intro: Card_rel_nat Card_rel_is_Ord)
done
lemma InfCard_rel_is_Card_rel: "M(K) ⟹ InfCard⇗M⇖(K) ⟹ Card⇗M⇖(K)"
apply (simp add: InfCard_rel_def)
done
lemma InfCard_rel_Un:
"[| InfCard⇗M⇖(K); Card⇗M⇖(L); M(K); M(L) |] ==> InfCard⇗M⇖(K ∪ L)"
apply (simp add: InfCard_rel_def)
apply (simp add: Card_rel_Un Un_upper1_le [THEN [2] le_trans] Card_rel_is_Ord)
done
lemma InfCard_rel_is_Limit: "InfCard⇗M⇖(K) ==> M(K) ⟹ Limit(K)"
apply (simp add: InfCard_rel_def)
apply (erule conjE)
apply (frule Card_rel_is_Ord, assumption)
apply (rule ltI [THEN non_succ_LimitI])
apply (erule le_imp_subset [THEN subsetD])
apply (safe dest!: Limit_nat [THEN Limit_le_succD])
apply (unfold Card_rel_def)
apply (drule trans)
apply (erule le_imp_subset [THEN nat_succ_eqpoll_rel, THEN cardinal_rel_cong], simp_all)
apply (erule Ord_cardinal_rel_le [THEN lt_trans2, THEN lt_irrefl], assumption)
apply (rule le_eqI) prefer 2
apply (rule Ord_cardinal_rel, assumption+)
done
end
lemma (in M_ordertype) ordertype_abs[absolut]:
assumes "wellordered(M,A,r)" "M(A)" "M(r)" "M(i)"
shows "otype(M,A,r,i) ⟷ i = ordertype(A,r)"
proof -
have eq:"j = k" if
"g ∈ ⟨A, r⟩ ≅ ⟨j, Memrel(j)⟩" "Ord(j)"
"h ∈ ⟨A, r⟩ ≅ ⟨k, Memrel(k)⟩" "Ord(k)"
for j k g h
proof -
from that
have "h O converse(g) ∈ ⟨j, Memrel(j)⟩ ≅ ⟨k, Memrel(k)⟩"
using ord_iso_sym ord_iso_trans by blast
with ‹Ord(j)› ‹Ord(k)›
show "j=k"
using Ord_iso_implies_eq[of j k "h O converse(g)"]
by simp
qed
have otypeE: "∃ h . h ∈ ⟨A, r⟩ ≅ ⟨k, Memrel(k)⟩" if "otype(M, A, r, k)" "M(k)" for k
proof -
note that assms
moreover from this
obtain h where "omap(M, A, r, h)" "M(h)"
using that omap_exists[of A r] by auto
moreover from calculation
have "h ∈ ⟨A, r⟩ ≅ ⟨k, Memrel(k)⟩"
using that omap_ord_iso obase_equals by simp
then
show ?thesis ..
qed
show ?thesis
proof(intro iffI)
note assms
moreover
assume "otype(M, A, r, i)"
moreover from calculation
obtain f j where "M(f)" "Ord(j)" "f ∈ ⟨A, r⟩ ≅ ⟨j, Memrel(j)⟩"
using ordertype_exists[of A r] by auto
ultimately
show "i = ordertype(A, r)"
using Ord_otype[OF _ well_ord_is_trans_on] eq[of f j _ i] ordertypes_are_absolute
otypeE[of i]
by auto
next
note assms
moreover
assume "i = ordertype(A, r)"
moreover from calculation
obtain j where "otype(M,A,r,j)" "M(j)"
using otype_exists by auto
ultimately
show "otype(M, A, r, i)"
using Ord_ordertype eq[of _ i _ j] Ord_otype[OF _ well_ord_is_trans_on]
otypeE[of j] ordertype_ord_iso[of A r]
by auto
qed
qed
lemma (in M_ordertype) ordertype_closed[intro,simp]: "⟦ wellordered(M,A,r);M(A);M(r)⟧ ⟹ M(ordertype(A,r))"
using ordertype_exists ordertypes_are_absolute by blast
relationalize "transitive_rel" "is_transitive" external
synthesize "is_transitive" from_definition assuming "nonempty"
arity_theorem for "is_transitive_fm"
lemma (in M_trivial) is_transitive_iff_transitive_rel:
"M(A)⟹ M(r) ⟹ transitive_rel(M, A, r) ⟷ is_transitive(M,A, r)"
unfolding transitive_rel_def is_transitive_def by simp
relationalize "linear_rel" "is_linear" external
synthesize "is_linear" from_definition assuming "nonempty"
arity_theorem for "is_linear_fm"
reldb_add relational "transitive_on" "transitive_rel"
reldb_add relational "linear_on" "linear_rel"
reldb_add functional "transitive_on" "transitive_rel"
reldb_add functional "linear_on" "linear_rel"
lemma (in M_trivial) is_linear_iff_linear_rel:
"M(A)⟹ M(r) ⟹ is_linear(M,A, r) ⟷ linear_rel(M, A, r)"
unfolding linear_rel_def is_linear_def by simp
relationalize "wellfounded_on" "is_wellfounded_on" external
synthesize "is_wellfounded_on" from_definition assuming "nonempty"
arity_theorem for "is_wellfounded_on_fm"
lemma (in M_trivial) is_wellfounded_on_iff_wellfounded_on:
"M(A)⟹ M(r) ⟹ is_wellfounded_on(M,A, r) ⟷ wellfounded_on(M, A, r)"
unfolding wellfounded_on_def is_wellfounded_on_def by simp
definition
is_well_ord :: "[i=>o,i,i]=>o" where
"is_well_ord(M,A,r) ==
is_transitive(M,A,r) ∧ is_linear(M,A,r) ∧ is_wellfounded_on(M,A,r)"
lemma (in M_trivial) is_well_ord_iff_wellordered:
"M(A)⟹ M(r) ⟹ is_well_ord(M,A, r) ⟷ wellordered(M, A, r)"
using is_wellfounded_on_iff_wellfounded_on is_linear_iff_linear_rel
is_transitive_iff_transitive_rel
unfolding wellordered_def is_well_ord_def by simp
synthesize "is_well_ord" from_definition assuming "nonempty"
arity_theorem for "is_well_ord_fm"
reldb_add relational "well_ord" "is_well_ord"
reldb_add functional "well_ord" "well_ord"
reldb_add relational "Order.pred" "pred_set"
reldb_add functional "Order.pred" "Order.pred"
relativize functional "ord_iso" "ord_iso_rel" external
relationalize "ord_iso_rel" "is_ord_iso"
context M_pre_cardinal_arith
begin
is_iff_rel for "ord_iso"
using bij_rel_iff
unfolding is_ord_iso_def ord_iso_rel_def
by simp
rel_closed for "ord_iso"
using ord_iso_separation unfolding ord_iso_rel_def
by simp
end
synthesize "is_ord_iso" from_definition assuming "nonempty"
lemma trans_on_iff_trans: "trans[A](r) ⟷ trans(r ∩ A×A)"
unfolding trans_on_def trans_def by auto
lemma trans_on_subset: "trans[A](r) ⟹ B ⊆ A ⟹ trans[B](r)"
unfolding trans_on_def
by auto
lemma relation_Int: "relation(r ∩ B×B)"
unfolding relation_def
by auto
text‹Discipline for \<^term>‹ordermap››
relativize functional "ordermap" "ordermap_rel" external
relationalize "ordermap_rel" "is_ordermap"
lemma wfrec_on_pred_eq:
assumes "r ∈ Pow(A×A)"
shows "wfrec[A](r, x, λx f. f `` Order.pred(A, x, r)) = wfrec(r, x, λx f. f `` Order.pred(A, x, r))"
proof -
from ‹r ∈ Pow(A×A)›
have "r ∩ A×A = r" by auto
then
show ?thesis
unfolding wfrec_on_def by simp
qed
context M_pre_cardinal_arith
begin
lemma wfrec_on_pred_closed:
assumes "wf[A](r)" "trans[A](r)" "r ∈ Pow⇗M⇖(A×A)" "M(A)" "x ∈ A"
shows "M(wfrec(r, x, λx f. f `` Order.pred(A, x, r)))"
proof -
note assms
moreover from this
have "M(r)" "M(x)"
using transM[of _ "Pow⇗M⇖(A×A)"] transM[of _ A]
by simp_all
moreover from calculation
have "wfrec[A](r, x, λx f. f `` Order.pred(A, x, r)) = wfrec(r, x, λx f. f `` Order.pred(A, x, r))"
using wfrec_on_pred_eq Pow_rel_char
by simp
moreover from calculation
have "M(wfrec(r, x, λx f. f `` Order.pred(A, x, r)))"
using wfrec_pred_replacement wf_on_imp_wf trans_on_imp_trans subset_Sigma_imp_relation
Pow_rel_char
by (rule_tac MH="λx f b. ∃a[M]. image(M, f, a, b) ∧ pred_set(M, A, x, r, a)" in trans_wfrec_closed)
(auto dest:transM simp:relation2_def)
ultimately
show ?thesis
by simp
qed
lemma wfrec_on_pred_closed':
assumes "wf[A](r)" "trans[A](r)" "r ∈ Pow⇗M⇖(A×A)" "M(A)" "x ∈ A"
shows "M(wfrec[A](r, x, λx f. f `` Order.pred(A, x, r)))"
using assms wfrec_on_pred_closed wfrec_on_pred_eq Pow_rel_char
by simp
lemma ordermap_rel_closed[intro,simp]:
assumes "wf[A](r)" "trans[A](r)" "r ∈ Pow⇗M⇖(A×A)" "M(A)"
shows "M(ordermap_rel(M, A, r))"
proof -
from assms
have "r ∩ A×A = r" "r∈Pow(A×A)" "M(r)"
using Pow_rel_char
by auto
with assms
have "wf(r)" "trans(r)" "relation(r)"
unfolding wf_on_def
using trans_on_iff_trans relation_def by auto
with ‹M(A)› ‹M(r)›
have 1:"
(∃y[M]. pair(M, x, y, z) ∧ is_wfrec(M, λx f z. z = f `` Order.pred(A, x, r), r, x, y))
⟷
z = ⟨x,wfrec(r,x,λx f. f `` Order.pred(A, x, r))⟩" if "M(x)" "M(z)" for x z
using that trans_wfrec_abs[of r,where
H="λx f. f `` Order.pred(A, x, r)" and
MH="λx f z . z= f `` Order.pred(A, x, r)",simplified]
wfrec_pred_replacement
unfolding relation2_def
by auto
with ‹M(A)› ‹M(r)›
have "strong_replacement(M,λx z. z = ⟨x,wfrec(r,x,λx f. f `` Order.pred(A, x, r))⟩)"
using strong_replacement_cong[of M,OF 1,THEN iffD1,OF _ _
wfrec_pred_replacement[unfolded wfrec_replacement_def]]
by simp
with ‹M(A)› ‹M(r)› ‹r ∈ Pow(A×A)› assms
show ?thesis
unfolding ordermap_rel_def
using lam_cong[OF refl wfrec_on_pred_eq] wfrec_on_pred_closed lam_closed
by auto
qed
lemma is_ordermap_iff:
assumes "r ∈ Pow⇗M⇖(A×A)" "wf[A](r)" "trans[A](r)"
"M(A)" "M(res)"
shows "is_ordermap(M, A, r, res) ⟷ res = ordermap_rel(M, A, r)"
proof -
from ‹r ∈ _› ‹M(A)›
have "r ∩ A×A = r" "M(r)" "r ∈ Pow(A×A)" "⋀ x y . ⟨x,y⟩∈r ⟹ x∈A"
using Pow_rel_char
by auto
with assms
have "wf(r)" "trans(r)" "relation(r)"
unfolding wf_on_def
using trans_on_iff_trans relation_def by auto
with ‹r∈Pow(A×A)›
show ?thesis
using ordermap_rel_closed[of r A] assms wfrec_on_pred_closed wfrec_pred_replacement
unfolding is_ordermap_def ordermap_rel_def
apply (rule_tac lambda_abs2,simp_all add:Relation1_def,clarify)
apply (rule trans_wfrec_on_abs)
apply (auto dest:transM simp add: relation_Int relation2_def)
by(rule_tac wfrec_on_pred_closed'[of A r],auto)
qed
end
text‹Discipline for \<^term>‹ordertype››
relativize functional "ordertype" "ordertype_rel" external
relationalize "ordertype_rel" "is_ordertype"
definition is_order_body
where "is_order_body(M,p,z) ≡ ∃X[M].∃r[M].∃A[M]. is_fst(M,p,X) ∧ is_snd(M,p,r) ∧
cartprod(M,X,X,A) ∧ subset(M,r,A) ∧ M(z) ∧ M(r) ∧ is_well_ord(M,X,r) ∧ is_ordertype(M,X,r,z)"
context M_pre_cardinal_arith
begin
lemma is_ordertype_iff:
assumes "r ∈ Pow⇗M⇖(A×A)" "well_ord(A,r)"
shows "M(A) ⟹ M(res) ⟹ is_ordertype(M, A, r, res) ⟷ res = ordertype_rel(M, A, r)"
using assms is_ordermap_iff[of r A] trans_on_iff_trans
ordermap_rel_closed[of A r]
unfolding is_ordertype_def ordertype_rel_def wf_on_def well_ord_def part_ord_def tot_ord_def
by simp
lemma ordertype_rel_abs:
assumes "wellordered(M,X,r)" "M(X)" "M(r)"
shows "ordertype_rel(M,X,r) = ordertype(X,r)"
using assms ordertypes_are_absolute[of X r]
unfolding ordertype_def ordertype_rel_def ordermap_rel_def ordermap_def
by simp
lemma (in M_pre_cardinal_arith) is_order_body_abs :
"M(Xr) ⟹ M(z) ⟹ is_order_body(M, Xr, z) ⟷
snd(Xr)∈Pow⇗M⇖(fst(Xr)×fst(Xr)) ∧ well_ord(fst(Xr), snd(Xr)) ∧ z = ordertype(fst(Xr), snd(Xr))"
using is_ordertype_iff ordertype_rel_abs well_ord_is_linear Pow_rel_char
is_well_ord_iff_wellordered snd_abs fst_abs
unfolding is_order_body_def
by simp
lemma well_ord_restr: "well_ord(X, r) ⟹ well_ord(X, r ∩ X×X)"
proof -
have "r ∩ X×X ∩ X×X = r ∩ X×X" by auto
moreover
assume "well_ord(X, r)"
ultimately
show ?thesis
unfolding well_ord_def tot_ord_def part_ord_def linear_def
irrefl_def wf_on_def
by simp_all (simp only: trans_on_def, blast)
qed
lemma ordertype_restr_eq :
assumes "well_ord(X,r)"
shows "ordertype(X, r) = ordertype(X, r ∩ X×X)"
using ordermap_restr_eq assms unfolding ordertype_def
by simp
lemma ordertype_rel_closed[intro,simp]:
assumes "well_ord(A,r)" "r ∈ Pow⇗M⇖(A×A)" "M(A)"
shows "M(ordertype_rel(M,A,r))"
using assms Pow_rel_char
unfolding well_ord_def tot_ord_def part_ord_def ordertype_rel_def
by simp
end
relativize functional "jump_cardinal_body" "jump_cardinal_body_rel"
relationalize "jump_cardinal_body_rel" "is_jump_cardinal_body_rel"
relativize functional "jump_cardinal_body'" "jump_cardinal_body'_rel"
relationalize "jump_cardinal_body'_rel" "is_jump_cardinal_body'_rel"
text‹Notice that this is not quite the same as \<^term>‹jump_cardinal›:
observe \<^term>‹Pow(X*X)›.›
definition
jump_cardinal' :: "i⇒i" where
"jump_cardinal'(K) ≡
⋃X∈Pow(K). {z. r ∈ Pow(X*X), z = jump_cardinal_body(Pow(X*X),X)}"
relativize functional "jump_cardinal" "jump_cardinal_rel" external
relativize functional "trans_on" "transitivie_rel" external
relationalize "jump_cardinal_rel" "is_jump_cardinal"
lemma (in M_ordertype) ordermap_closed[intro,simp]:
assumes "wellordered(M,A,r)" and types:"M(A)" "M(r)"
shows "M(ordermap(A,r))"
proof -
note assms
moreover from this
obtain i f where "Ord(i)" "f ∈ ord_iso(A, r, i, Memrel(i))"
"M(i)" "M(f)" using ordertype_exists by blast
moreover from calculation
have "i = ordertype(A,r)" using ordertypes_are_absolute by force
moreover from calculation
have "ordermap(A,r) ∈ ord_iso(A, r, i, Memrel(i))"
using ordertype_ord_iso by simp
ultimately
have "f = ordermap(A,r)" using well_ord_iso_unique by fastforce
with ‹M(f)›
show ?thesis by simp
qed
context M_pre_cardinal_arith
begin
lemma def_jump_cardinal_body:
"M(X) ⟹ M(U) ⟹
jump_cardinal_body(U,X) = {z . r ∈ U, M(z) ∧ well_ord(X, r) ∧ z = ordertype(X, r)}"
unfolding jump_cardinal_body_def
using ordertype_closed
by(rule_tac Replace_cong,auto dest:transM)
lemma jump_cardinal_body_abs:
shows "M(A) ⟹ jump_cardinal_body_rel(M,Pow⇗M⇖(A×A),A) = jump_cardinal_body(Pow⇗M⇖(A×A),A)"
unfolding jump_cardinal_body_rel_def
using def_jump_cardinal_body ordertype_rel_abs transM[of _ "Pow⇗M⇖(A×A)"]
by simp
end
locale M_cardinal_arith = M_pre_cardinal_arith +
assumes
is_ordertype_replacement :
"strong_replacement(M,λ x z . ∃y[M]. is_order_body(M,x,y) ∧ z=⟨x,y⟩)"
and
pow_rel_separation : "∀A[M]. separation(M, λy. ∃x[M]. x ∈ A ∧ y = ⟨x, Pow⇗M⇖(x)⟩)"
and
separation_is_well_ord : "separation(M, λx . is_well_ord(M,fst(x),snd(x)))"
begin
lemmas Pow_rel_replacement = lam_replacement_Pow_rel[OF pow_rel_separation]
lemma ordtype_replacement :
"strong_replacement(M , λx z . (snd(x) ∈ Pow⇗M⇖(fst(x)×fst(x)) ∧ well_ord(fst(x),snd(x))) ∧
z =⟨x, ordertype(fst(x),snd(x))⟩)"
using strong_replacement_cong[THEN iffD1,OF _ is_ordertype_replacement] is_order_body_abs
by simp
lemma separation_well_ord : "separation(M, λx . well_ord(fst(x),snd(x)))"
using separation_cong[THEN iffD1] separation_is_well_ord is_well_ord_iff_wellordered well_ord_abs
by simp
lemma jump_cardinal_body_lam_replacement :
shows "lam_replacement(M, λX .jump_cardinal_body(Pow⇗M⇖(X × X),X))" and
"M(X) ⟹ M(jump_cardinal_body(Pow⇗M⇖(X × X), X))"
proof -
define WO where "WO ≡ λX . {r∈Pow⇗M⇖(X×X) . well_ord(X,r)}"
define lam_jump_cardinal_body where
"lam_jump_cardinal_body ≡ λX . λr∈WO(X) . ordertype(X,r)"
have "lam_jump_cardinal_body(X) = {⟨r,ordertype(X,r)⟩ . r ∈ WO(X)}" for X
unfolding lam_jump_cardinal_body_def WO_def lam_def
by simp
then
have "jump_cardinal_body(Pow⇗M⇖(X × X),X) = {snd(p) . p ∈ lam_jump_cardinal_body(X)}" if "M(X)" for X
unfolding jump_cardinal_body_def WO_def lam_def
by force
moreover
have "lam_replacement(M, λx. {y . r ∈ Pow⇗M⇖(x × x), (r ∈ Pow⇗M⇖(x × x) ∧ well_ord(x, r)) ∧ y = ordertype(x, r)})"
(is "lam_replacement(M,?q)")
using Pow_rel_replacement[THEN [2] lam_replacement_hcomp]
lam_replacement_CartProd lam_replacement_identity lam_replacement_fst lam_replacement_snd
fst_closed[OF transM] snd_closed[OF transM]
separation_well_ord separation_in separation_conj transM[of _ "Pow⇗M⇖(_×_)"]
strong_lam_replacement_imp_lam_replacement_RepFun[OF ordtype_replacement, where g="λX. Pow⇗M⇖(X × X)"]
by force
moreover
have "M(?q(x))" if "M(x)" for x
using that Pow_rel_replacement[THEN [2] lam_replacement_hcomp]
lam_replacement_CartProd lam_replacement_identity
ordertype_closed transM[of _ "Pow⇗M⇖(_×_)"]
fst_closed[OF transM] snd_closed[OF transM]
by(rule_tac strong_lam_replacement_imp_strong_replacement[OF ordtype_replacement,THEN strong_replacement_closed],
auto)
moreover
have "?q(x)={snd(p) . p ∈ (λr∈WO(x). ordertype(x, r))}" if "M(x)" for x
using that
unfolding lam_def WO_def
by force
moreover from calculation
have "?q(X) = jump_cardinal_body(Pow⇗M⇖(X × X), X)" if "M(X)" for X
using that
unfolding lam_jump_cardinal_body_def
by simp
moreover from calculation
have "M(jump_cardinal_body(Pow⇗M⇖(X × X), X))" if "M(X)" for X
using that by simp
moreover from calculation
have 1:"lam_replacement(M, λx . {snd(p) . p ∈ lam_jump_cardinal_body(x)})"
using lam_replacement_cong
by auto
ultimately
show "lam_replacement(M, λX .jump_cardinal_body(Pow⇗M⇖(X × X),X))" and
"M(X) ⟹ M(jump_cardinal_body(Pow⇗M⇖(X × X), X))"
using lam_replacement_imp_strong_replacement[OF lam_replacement_snd]
lam_replacement_cong[OF 1,unfolded lam_jump_cardinal_body_def]
by simp_all
qed
lemmas jump_cardinal_body_closed = jump_cardinal_body_lam_replacement(2)
lemma jump_cardinal_closed:
assumes "M(K)"
shows "M({jump_cardinal_body(Pow⇗M⇖(X × X),X) . X ∈ Pow⇗M⇖(K)})"
using assms jump_cardinal_body_lam_replacement lam_replacement_imp_strong_replacement
transM[of _ "Pow⇗M⇖(K)"] RepFun_closed
by auto
end
context M_pre_cardinal_arith
begin
lemma ordermap_eqpoll_pred:
"[| well_ord(A,r); x ∈ A ; M(A);M(r);M(x)|] ==> ordermap(A,r)`x ≈⇗M⇖ Order.pred(A,x,r)"
apply (simp add: def_eqpoll_rel)
apply (rule rexI)
apply (simp add: ordermap_eq_image well_ord_is_wf)
apply (erule ordermap_bij [THEN bij_is_inj, THEN restrict_bij,
THEN bij_converse_bij])
apply (rule pred_subset, simp)
done
text‹Kunen: "each \<^term>‹⟨x,y⟩ ∈ K × K› has no more than \<^term>‹z × z› predecessors..." (page 29)›
lemma ordermap_csquare_le:
assumes K: "Limit(K)" and x: "x<K" and y: " y<K"
and types: "M(K)" "M(x)" "M(y)"
shows "|ordermap(K × K, csquare_rel(K)) ` ⟨x,y⟩|⇗M⇖ ≤ |succ(succ(x ∪ y))|⇗M⇖ ⊗⇗M⇖ |succ(succ(x ∪ y))|⇗M⇖"
using types
proof (simp add: cmult_rel_def, rule_tac well_ord_lepoll_rel_imp_cardinal_rel_le)
let ?z="succ(x ∪ y)"
show "well_ord(|succ(?z)|⇗M⇖ × |succ(?z)|⇗M⇖,
rmult(|succ(?z)|⇗M⇖, Memrel(|succ(?z)|⇗M⇖), |succ(?z)|⇗M⇖, Memrel(|succ(?z)|⇗M⇖)))"
by (blast intro: well_ord_Memrel well_ord_rmult types)
next
let ?z="succ(x ∪ y)"
have zK: "?z<K" using x y K
by (blast intro: Un_least_lt Limit_has_succ)
hence oz: "Ord(?z)" by (elim ltE)
from assms
have Mom:"M(ordermap(K × K, csquare_rel(K)))"
using well_ord_csquare Limit_is_Ord by fastforce
then
have "ordermap(K × K, csquare_rel(K)) ` ⟨x,y⟩ ≲⇗M⇖ ordermap(K × K, csquare_rel(K)) ` ⟨?z,?z⟩"
by (blast intro: ordermap_z_lt leI le_imp_lepoll_rel K x y types)
also have "... ≈⇗M⇖ Order.pred(K × K, ⟨?z,?z⟩, csquare_rel(K))"
proof (rule ordermap_eqpoll_pred)
show "well_ord(K × K, csquare_rel(K))" using K
by (rule Limit_is_Ord [THEN well_ord_csquare])
next
show "⟨?z, ?z⟩ ∈ K × K" using zK
by (blast intro: ltD)
qed (simp_all add:types)
also have "... ≲⇗M⇖ succ(?z) × succ(?z)" using zK
by (rule_tac pred_csquare_subset [THEN subset_imp_lepoll_rel]) (simp_all add:types)
also have "... ≈⇗M⇖ |succ(?z)|⇗M⇖ × |succ(?z)|⇗M⇖" using oz
by (blast intro: prod_eqpoll_rel_cong Ord_cardinal_rel_eqpoll_rel eqpoll_rel_sym types)
finally show "ordermap(K × K, csquare_rel(K)) ` ⟨x,y⟩ ≲⇗M⇖ |succ(?z)|⇗M⇖ × |succ(?z)|⇗M⇖"
by (simp_all add:types Mom)
from Mom
show "M(ordermap(K × K, csquare_rel(K)) ` ⟨x, y⟩)" by (simp_all add:types)
qed (simp_all add:types)
text‹Kunen: "... so the order type is ‹≤› K"›
lemma ordertype_csquare_le_M:
assumes IK: "InfCard⇗M⇖(K)" and eq: "⋀y. y∈K ⟹ InfCard⇗M⇖(y) ⟹ M(y) ⟹ y ⊗⇗M⇖ y = y"
and types: "M(K)"
shows "ordertype(K*K, csquare_rel(K)) ≤ K"
proof -
have CK: "Card⇗M⇖(K)" using IK by (rule_tac InfCard_rel_is_Card_rel) (simp_all add:types)
hence OK: "Ord(K)" by (rule Card_rel_is_Ord) (simp_all add:types)
moreover have "Ord(ordertype(K × K, csquare_rel(K)))" using OK
by (rule well_ord_csquare [THEN Ord_ordertype])
ultimately show ?thesis
proof (rule all_lt_imp_le)
fix i
assume i:"i < ordertype(K × K, csquare_rel(K))"
hence Oi: "Ord(i)" by (elim ltE)
obtain x y where x: "x ∈ K" and y: "y ∈ K"
and ieq: "i = ordermap(K × K, csquare_rel(K)) ` ⟨x,y⟩"
using i by (auto simp add: ordertype_unfold elim: ltE)
hence xy: "Ord(x)" "Ord(y)" "x < K" "y < K" using OK
by (blast intro: Ord_in_Ord ltI)+
hence ou: "Ord(x ∪ y)"
by (simp)
from OK types
have "M(ordertype(K × K, csquare_rel(K)))"
using well_ord_csquare by fastforce
with i x y types
have types': "M(K)" "M(i)" "M(x)" "M(y)"
using types by (auto dest:transM ltD)
show "i < K"
proof (rule Card_rel_lt_imp_lt [OF _ Oi CK])
have "|i|⇗M⇖ ≤ |succ(succ(x ∪ y))|⇗M⇖ ⊗⇗M⇖ |succ(succ(x ∪ y))|⇗M⇖" using IK xy
by (auto simp add: ieq types intro: InfCard_rel_is_Limit [THEN ordermap_csquare_le] types')
moreover have "|succ(succ(x ∪ y))|⇗M⇖ ⊗⇗M⇖ |succ(succ(x ∪ y))|⇗M⇖ < K"
proof (cases rule: Ord_linear2 [OF ou Ord_nat])
assume "x ∪ y < nat"
hence "|succ(succ(x ∪ y))|⇗M⇖ ⊗⇗M⇖ |succ(succ(x ∪ y))|⇗M⇖ ∈ nat"
by (simp add: lt_def nat_cmult_rel_eq_mult nat_succI
nat_into_Card_rel [THEN Card_rel_cardinal_rel_eq] types')
also have "... ⊆ K" using IK
by (simp add: InfCard_rel_def le_imp_subset types)
finally show "|succ(succ(x ∪ y))|⇗M⇖ ⊗⇗M⇖ |succ(succ(x ∪ y))|⇗M⇖ < K"
by (simp add: ltI OK)
next
assume natxy: "nat ≤ x ∪ y"
hence seq: "|succ(succ(x ∪ y))|⇗M⇖ = |x ∪ y|⇗M⇖" using xy
by (simp add: le_imp_subset nat_succ_eqpoll_rel [THEN cardinal_rel_cong] le_succ_iff types')
also have "... < K" using xy
by (simp add: Un_least_lt Ord_cardinal_rel_le [THEN lt_trans1] types')
finally have "|succ(succ(x ∪ y))|⇗M⇖ < K" .
moreover have "InfCard⇗M⇖(|succ(succ(x ∪ y))|⇗M⇖)" using xy natxy
by (simp add: seq InfCard_rel_def nat_le_cardinal_rel types')
ultimately show ?thesis by (simp add: eq ltD types')
qed
ultimately show "|i|⇗M⇖ < K" by (blast intro: lt_trans1)
qed (simp_all add:types')
qed
qed
lemma InfCard_rel_csquare_eq:
assumes IK: "InfCard⇗M⇖(K)" and
types: "M(K)"
shows "K ⊗⇗M⇖ K = K"
proof -
have OK: "Ord(K)" using IK by (simp add: Card_rel_is_Ord InfCard_rel_is_Card_rel types)
from OK assms
show "K ⊗⇗M⇖ K = K"
proof (induct rule: trans_induct)
case (step i)
note types = ‹M(K)› ‹M(i)›
show "i ⊗⇗M⇖ i = i"
proof (rule le_anti_sym)
from step types
have Mot:"M(ordertype(i × i, csquare_rel(i)))" "M(ordermap(i × i, csquare_rel(i)))"
using well_ord_csquare Limit_is_Ord by simp_all
then
have "|i × i|⇗M⇖ = |ordertype(i × i, csquare_rel(i))|⇗M⇖"
by (rule_tac cardinal_rel_cong,
simp_all add: step.hyps well_ord_csquare [THEN ordermap_bij, THEN bij_imp_eqpoll_rel] types)
with Mot
have "i ⊗⇗M⇖ i ≤ ordertype(i × i, csquare_rel(i))"
by (simp add: step.hyps cmult_rel_def Ord_cardinal_rel_le well_ord_csquare [THEN Ord_ordertype] types)
moreover
have "ordertype(i × i, csquare_rel(i)) ≤ i" using step
by (rule_tac ordertype_csquare_le_M) (simp add: types)
ultimately show "i ⊗⇗M⇖ i ≤ i" by (rule le_trans)
next
show "i ≤ i ⊗⇗M⇖ i" using step
by (blast intro: cmult_rel_square_le InfCard_rel_is_Card_rel)
qed
qed
qed
lemma well_ord_InfCard_rel_square_eq:
assumes r: "well_ord(A,r)" and I: "InfCard⇗M⇖(|A|⇗M⇖)" and
types: "M(A)" "M(r)"
shows "A × A ≈⇗M⇖ A"
proof -
have "A × A ≈⇗M⇖ |A|⇗M⇖ × |A|⇗M⇖"
by (blast intro: prod_eqpoll_rel_cong well_ord_cardinal_rel_eqpoll_rel eqpoll_rel_sym r types)
also have "... ≈⇗M⇖ A"
proof (rule well_ord_cardinal_rel_eqE [OF _ r])
show "well_ord(|A|⇗M⇖ × |A|⇗M⇖, rmult(|A|⇗M⇖, Memrel(|A|⇗M⇖), |A|⇗M⇖, Memrel(|A|⇗M⇖)))"
by (blast intro: well_ord_rmult well_ord_Memrel r types)
next
show "||A|⇗M⇖ × |A|⇗M⇖|⇗M⇖ = |A|⇗M⇖" using InfCard_rel_csquare_eq I
by (simp add: cmult_rel_def types)
qed (simp_all add:types)
finally show ?thesis by (simp_all add:types)
qed
lemma InfCard_rel_square_eqpoll:
assumes "InfCard⇗M⇖(K)" and types:"M(K)" shows "K × K ≈⇗M⇖ K"
using assms
apply (rule_tac well_ord_InfCard_rel_square_eq)
apply (erule InfCard_rel_is_Card_rel [THEN Card_rel_is_Ord, THEN well_ord_Memrel])
apply (simp_all add: InfCard_rel_is_Card_rel [THEN Card_rel_cardinal_rel_eq] types)
done
lemma Inf_Card_rel_is_InfCard_rel: "[| Card⇗M⇖(i); ~ Finite_rel(M,i) ; M(i) |] ==> InfCard⇗M⇖(i)"
by (simp add: InfCard_rel_def Card_rel_is_Ord [THEN nat_le_infinite_Ord])
subsubsection‹Toward's Kunen's Corollary 10.13 (1)›
lemma InfCard_rel_le_cmult_rel_eq: "[| InfCard⇗M⇖(K); L ≤ K; 0<L; M(K) ; M(L) |] ==> K ⊗⇗M⇖ L = K"
apply (rule le_anti_sym)
prefer 2
apply (erule ltE, blast intro: cmult_rel_le_self InfCard_rel_is_Card_rel)
apply (frule InfCard_rel_is_Card_rel [THEN Card_rel_is_Ord, THEN le_refl]) prefer 3
apply (rule cmult_rel_le_mono [THEN le_trans], assumption+)
apply (simp_all add: InfCard_rel_csquare_eq)
done
lemma InfCard_rel_cmult_rel_eq: "[| InfCard⇗M⇖(K); InfCard⇗M⇖(L); M(K) ; M(L) |] ==> K ⊗⇗M⇖ L = K ∪ L"
apply (rule_tac i = K and j = L in Ord_linear_le)
apply (typecheck add: InfCard_rel_is_Card_rel Card_rel_is_Ord)
apply (rule cmult_rel_commute [THEN ssubst]) prefer 3
apply (rule Un_commute [THEN ssubst])
apply (simp_all add: InfCard_rel_is_Limit [THEN Limit_has_0] InfCard_rel_le_cmult_rel_eq
subset_Un_iff2 [THEN iffD1] le_imp_subset)
done
lemma InfCard_rel_cdouble_eq: "InfCard⇗M⇖(K) ⟹ M(K) ⟹ K ⊕⇗M⇖ K = K"
apply (simp add: cmult_rel_2 [symmetric] InfCard_rel_is_Card_rel cmult_rel_commute)
apply (simp add: InfCard_rel_le_cmult_rel_eq InfCard_rel_is_Limit Limit_has_0 Limit_has_succ)
done
lemma InfCard_rel_le_cadd_rel_eq: "[| InfCard⇗M⇖(K); L ≤ K ; M(K) ; M(L)|] ==> K ⊕⇗M⇖ L = K"
apply (rule le_anti_sym)
prefer 2
apply (erule ltE, blast intro: cadd_rel_le_self InfCard_rel_is_Card_rel)
apply (frule InfCard_rel_is_Card_rel [THEN Card_rel_is_Ord, THEN le_refl]) prefer 3
apply (rule cadd_rel_le_mono [THEN le_trans], assumption+)
apply (simp_all add: InfCard_rel_cdouble_eq)
done
lemma InfCard_rel_cadd_rel_eq: "[| InfCard⇗M⇖(K); InfCard⇗M⇖(L); M(K) ; M(L) |] ==> K ⊕⇗M⇖ L = K ∪ L"
apply (rule_tac i = K and j = L in Ord_linear_le)
apply (typecheck add: InfCard_rel_is_Card_rel Card_rel_is_Ord)
apply (rule cadd_rel_commute [THEN ssubst]) prefer 3
apply (rule Un_commute [THEN ssubst])
apply (simp_all add: InfCard_rel_le_cadd_rel_eq subset_Un_iff2 [THEN iffD1] le_imp_subset)
done
end
subsection‹For Every Cardinal Number There Exists A Greater One›
text‹This result is Kunen's Theorem 10.16, which would be trivial using AC›
locale M_cardinal_arith_jump = M_cardinal_arith + M_ordertype
begin
lemma def_jump_cardinal_rel_aux:
"X ∈ Pow⇗M⇖(K) ⟹ M(K) ⟹
{z . r ∈ Pow⇗M⇖(X × X), M(z) ∧ well_ord(X, r) ∧ z = ordertype(X, r)} =
{z . r ∈ Pow⇗M⇖(K × K), M(z) ∧ well_ord(X, r) ∧ z = ordertype(X, r)}"
proof(rule,auto simp:Pow_rel_char dest:transM)
let ?L="{z . r ∈ Pow⇗M⇖(X × X), M(z) ∧ well_ord(X, r) ∧ z = ordertype(X, r)}"
let ?R="{z . r ∈ Pow⇗M⇖(K × K), M(z) ∧ well_ord(X, r) ∧ z = ordertype(X, r)}"
show "ordertype(X, r) ∈ {y . x ∈ {x ∈ Pow(X × X) . M(x)}, M(y) ∧ well_ord(X, x) ∧ y = ordertype(X, x)}"
if "M(K)" "M(r)" "r⊆K×K" "X⊆K" "M(X)" "well_ord(X,r)" for r
proof -
from that
have "ordertype(X,r) = ordertype(X,r∩X×X)" "(r∩X×X)⊆X×X" "M(r∩X×X)"
"well_ord(X,r∩X×X)" "wellordered(M,X,r∩X×X)"
using well_ord_restr ordertype_restr_eq by auto
moreover from this
have "ordertype(X,r∩X×X) ∈ ?L"
using that Pow_rel_char
ReplaceI[of "λ z r . M(z) ∧ well_ord(X, r) ∧ z = ordertype(X, r)" "ordertype(X,r∩X×X)"]
by auto
ultimately
show ?thesis
using Pow_rel_char by auto
qed
qed
lemma def_jump_cardinal_rel_aux2:
assumes "X ∈ Pow⇗M⇖(K)" "M(K)"
shows "jump_cardinal_body(Pow⇗M⇖(K×K),X) = jump_cardinal_body(Pow⇗M⇖(X×X),X)"
proof -
from assms
have "jump_cardinal_body(Pow⇗M⇖(K×K),X) = {z . r ∈Pow⇗M⇖(K×K), M(z) ∧ well_ord(X, r) ∧ z = ordertype(X, r)}"
using def_jump_cardinal_body transM[of _ "Pow⇗M⇖(K)"]
by simp
also from assms
have "... = {z . r ∈Pow⇗M⇖(X×X), M(z) ∧ well_ord(X, r) ∧ z = ordertype(X, r)}"
using def_jump_cardinal_rel_aux transM[of _ "Pow⇗M⇖(K)"]
by simp
also from assms
have "... = jump_cardinal_body(Pow⇗M⇖(X×X),X)"
using def_jump_cardinal_body transM[of _ "Pow⇗M⇖(K)"] by auto
finally
show ?thesis .
qed
lemma def_jump_cardinal_rel:
assumes "M(K)"
shows "jump_cardinal_rel(M,K) =
(⋃{jump_cardinal_body(Pow⇗M⇖(K*K),X) . X∈ Pow⇗M⇖(K)})"
proof -
have "jump_cardinal_body(Pow⇗M⇖(X × X),X) = {z . r ∈ Pow⇗M⇖(X × X), M(z) ∧ well_ord(X, r) ∧ z=ordertype(X, r)}"
if "M(X)" for X
using that ordertype_closed transM[of _ "Pow⇗M⇖(X×X)"]
unfolding jump_cardinal_body_def
by(intro equalityI subsetI,auto)
then
have "M({z . r ∈ Pow⇗M⇖(X × X), M(z) ∧ well_ord(X, r) ∧ z = ordertype(X, r)})"
if "M(Y)" "X ∈ Pow⇗M⇖(Y)" for Y X
using jump_cardinal_body_closed[of X] that transM[of _ "Pow⇗M⇖(Y)"]
ordertype_closed transM[of _ "Pow⇗M⇖(X×X)"]
unfolding jump_cardinal_body_def
by auto
moreover from ‹M(K)›
have "R ∈ Pow⇗M⇖(X × X) ⟹ X ∈ Pow⇗M⇖(K) ⟹ R ∈ Pow⇗M⇖(K × K)" for X R
using mem_Pow_rel_abs transM[OF _ Pow_rel_closed, of R "X×X"]
transM[OF _ Pow_rel_closed, of X K] by auto
ultimately
show ?thesis
using assms is_ordertype_iff
ordertype_rel_abs transM[of _ "Pow⇗M⇖(K)"] transM[of _ "Pow⇗M⇖(K×K)"]
def_jump_cardinal_rel_aux jump_cardinal_body_closed ordertype_closed
unfolding jump_cardinal_rel_def jump_cardinal_body_def
apply(intro equalityI subsetI,auto dest:transM[of _ "Pow⇗M⇖(K)"],rename_tac y r)
by(rule_tac x="{z . xa ∈ Pow⇗M⇖(K × K), M(z) ∧ well_ord(y, xa) ∧ z = ordertype(y, xa)}" in bexI,auto)
qed
lemma Ord_jump_cardinal_rel: "M(K) ⟹ Ord(jump_cardinal_rel(M,K))"
apply (unfold def_jump_cardinal_rel jump_cardinal_body_def )
apply (rule Ord_is_Transset [THEN [2] OrdI])
prefer 2 apply (blast intro!: Ord_ordertype)
apply (unfold Transset_def)
apply (safe del: subsetI)
apply (subst ordertype_pred_unfold, simp, safe)
apply (rule UN_I)
apply (rule_tac [2] ReplaceI)
prefer 4 apply (blast intro: well_ord_subset elim!: predE, simp_all)
prefer 2 apply (blast intro: well_ord_subset elim!: predE)
proof -
fix X r xb
assume "M(K)" "X ∈ Pow⇗M⇖(K)" "r ∈ Pow⇗M⇖(K × K)" "well_ord(X, r)" "xb ∈ X"
moreover from this
have "M(X)" "M(r)"
using cartprod_closed trans_Pow_rel_closed by auto
moreover from this
have "M(xb)" using transM[OF ‹xb∈X›] by simp
ultimately
show "Order.pred(X, xb, r) ∈ Pow⇗M⇖(K)"
using def_Pow_rel by (auto dest:predE)
qed
declare conj_cong [cong del]
lemma jump_cardinal_rel_iff_old:
"M(i) ⟹ M(K) ⟹ i ∈ jump_cardinal_rel(M,K) ⟷
(∃r[M]. ∃X[M]. r ⊆ K*K & X ⊆ K & well_ord(X,r) & i = ordertype(X,r))"
apply (unfold def_jump_cardinal_rel jump_cardinal_body_def)
apply (auto del: subsetI)
apply (rename_tac y r)
apply (rule_tac x=r in rexI, intro conjI) prefer 2
apply (rule_tac x=y in rexI, intro conjI)
apply (auto dest:mem_Pow_rel transM)
apply (rule_tac A=r in rev_subsetD, assumption)
defer
apply (rename_tac r y)
apply (rule_tac x=y in bexI)
apply (rule_tac x=r in ReplaceI, auto)
using def_Pow_rel
apply (force+)[2]
apply (rule_tac A=r in rev_subsetD, assumption)
using mem_Pow_rel[THEN conjunct1]
apply auto
done
lemma K_lt_jump_cardinal_rel: "Ord(K) ==> M(K) ⟹ K < jump_cardinal_rel(M,K)"
apply (rule Ord_jump_cardinal_rel [THEN [2] ltI])
apply (rule jump_cardinal_rel_iff_old [THEN iffD2], assumption+)
apply (rule_tac x="Memrel(K)" in rexI)
apply (rule_tac x=K in rexI)
apply (simp add: ordertype_Memrel well_ord_Memrel)
using Memrel_closed
apply (simp_all add: Memrel_def subset_iff)
done
lemma def_jump_cardinal_rel':
assumes "M(K)"
shows "jump_cardinal_rel(M,K) =
(⋃X∈Pow⇗M⇖(K). {z. r ∈ Pow⇗M⇖(X×X), well_ord(X,r) ∧ z = ordertype(X,r)})"
proof -
from assms
have "jump_cardinal_rel(M, K) = (⋃X∈Pow⇗M⇖(K). jump_cardinal_body(Pow⇗M⇖(K × K), X))"
using def_jump_cardinal_rel
by simp
also from ‹M(K)›
have " ... = (⋃X∈Pow⇗M⇖(K). jump_cardinal_body(Pow⇗M⇖(X × X), X))"
using def_jump_cardinal_rel_aux2
by simp
finally
show ?thesis
unfolding jump_cardinal_body_def by simp
qed
rel_closed for "jump_cardinal"
proof -
fix K
assume "M(K)"
moreover from this
have "jump_cardinal_rel(M, K) =
⋃{jump_cardinal_body(Pow⇗M⇖(X × X), X) . X∈Pow⇗M⇖(K)}"
using def_jump_cardinal_rel'
unfolding jump_cardinal_body_def[symmetric]
by simp
moreover from calculation
have "M((⋃{jump_cardinal_body(Pow⇗M⇖(X × X), X) . X∈Pow⇗M⇖(K)}))"
using def_jump_cardinal_rel_aux jump_cardinal_closed
by simp
ultimately
show "M(jump_cardinal_rel(M,K))"
by simp
qed
lemma Card_rel_jump_cardinal_rel_lemma:
"[| well_ord(X,r); r ⊆ K * K; X ⊆ K;
f ∈ bij(ordertype(X,r), jump_cardinal_rel(M,K));
M(X); M(r); M(K); M(f) |]
==> jump_cardinal_rel(M,K) ∈ jump_cardinal_rel(M,K)"
apply (subgoal_tac "f O ordermap (X,r) ∈ bij (X, jump_cardinal_rel (M,K))")
prefer 2 apply (blast intro: comp_bij ordermap_bij)
apply (rule jump_cardinal_rel_iff_old [THEN iffD2],simp+)
apply (intro rexI conjI)
apply (rule subset_trans [OF rvimage_type Sigma_mono], assumption+)
apply (erule bij_is_inj [THEN well_ord_rvimage])
apply (rule Ord_jump_cardinal_rel [THEN well_ord_Memrel])
apply (simp_all add: well_ord_Memrel [THEN [2] bij_ordertype_vimage]
ordertype_Memrel Ord_jump_cardinal_rel)
done
lemma Card_rel_jump_cardinal_rel: "M(K) ⟹ Card_rel(M,jump_cardinal_rel(M,K))"
apply (rule Ord_jump_cardinal_rel [THEN Card_relI])
apply (simp_all add: def_eqpoll_rel)
apply (drule_tac i1=j in jump_cardinal_rel_iff_old [THEN iffD1, OF _ _ ltD, of _ K], safe)
apply (blast intro: Card_rel_jump_cardinal_rel_lemma [THEN mem_irrefl])
done
subsection‹Basic Properties of Successor Cardinals›
lemma csucc_rel_basic: "Ord(K) ==> M(K) ⟹ Card_rel(M,csucc_rel(M,K)) & K < csucc_rel(M,K)"
apply (unfold csucc_rel_def)
apply (rule LeastI[of "λi. M(i) ∧ Card_rel(M,i) ∧ K < i", THEN conjunct2])
apply (blast intro: Card_rel_jump_cardinal_rel K_lt_jump_cardinal_rel Ord_jump_cardinal_rel)+
done
lemmas Card_rel_csucc_rel = csucc_rel_basic [THEN conjunct1]
lemmas lt_csucc_rel = csucc_rel_basic [THEN conjunct2]
lemma Ord_0_lt_csucc_rel: "Ord(K) ==> M(K) ⟹ 0 < csucc_rel(M,K)"
by (blast intro: Ord_0_le lt_csucc_rel lt_trans1)
lemma csucc_rel_le: "[| Card_rel(M,L); K<L; M(K); M(L) |] ==> csucc_rel(M,K) ≤ L"
apply (unfold csucc_rel_def)
apply (rule Least_le)
apply (blast intro: Card_rel_is_Ord)+
done
lemma lt_csucc_rel_iff: "[| Ord(i); Card_rel(M,K); M(K); M(i)|] ==> i < csucc_rel(M,K) ⟷ |i|⇗M⇖ ≤ K"
apply (rule iffI)
apply (rule_tac [2] Card_rel_lt_imp_lt)
apply (erule_tac [2] lt_trans1)
apply (simp_all add: lt_csucc_rel Card_rel_csucc_rel Card_rel_is_Ord)
apply (rule notI [THEN not_lt_imp_le])
apply (rule Card_rel_cardinal_rel [THEN csucc_rel_le, THEN lt_trans1, THEN lt_irrefl], simp_all+)
apply (rule Ord_cardinal_rel_le [THEN lt_trans1])
apply (simp_all add: Card_rel_is_Ord)
done
lemma Card_rel_lt_csucc_rel_iff:
"[| Card_rel(M,K'); Card_rel(M,K); M(K'); M(K) |] ==> K' < csucc_rel(M,K) ⟷ K' ≤ K"
by (simp add: lt_csucc_rel_iff Card_rel_cardinal_rel_eq Card_rel_is_Ord)
lemma InfCard_rel_csucc_rel: "InfCard_rel(M,K) ⟹ M(K) ==> InfCard_rel(M,csucc_rel(M,K))"
by (simp add: InfCard_rel_def Card_rel_csucc_rel Card_rel_is_Ord
lt_csucc_rel [THEN leI, THEN [2] le_trans])
subsubsection‹Theorems by Krzysztof Grabczewski, proofs by lcp›
lemma nat_sum_eqpoll_rel_sum:
assumes m: "m ∈ nat" and n: "n ∈ nat" shows "m + n ≈⇗M⇖ m +⇩ω n"
proof -
have "m + n ≈⇗M⇖ |m+n|⇗M⇖" using m n
by (blast intro: nat_implies_well_ord well_ord_radd well_ord_cardinal_rel_eqpoll_rel eqpoll_rel_sym)
also have "... = m +⇩ω n" using m n
by (simp add: nat_cadd_rel_eq_add [symmetric] cadd_rel_def transM[OF _ M_nat])
finally show ?thesis .
qed
lemma Ord_nat_subset_into_Card_rel: "[| Ord(i); i ⊆ nat |] ==> Card⇗M⇖(i)"
by (blast dest: Ord_subset_natD intro: Card_rel_nat nat_into_Card_rel)
end
end