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⇒o,i] ⇒ i" where
"jump_cardinal_body(M,X) ≡
{z . r ∈ Pow⇗M⇖(X × X), M(z) ∧ M(r) ∧ well_ord(X, r) ∧ z = ordertype(X, r)} "
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
ord_iso_separation: "M(A) ⟹ M(r) ⟹ M(s) ⟹
separation(M, λf. ∀x∈A. ∀y∈A. ⟨x, y⟩ ∈ r ⟷ ⟨f ` x, f ` y⟩ ∈ s)"
and
wfrec_pred_replacement:"M(A) ⟹ M(r) ⟹
wfrec_replacement(M, λx f z. z = f `` Order.pred(A, x, r), r)"
locale M_cardinal_arith= M_pre_cardinal_arith +
assumes
ordertype_replacement :
"M(X) ⟹ strong_replacement(M,λ x z . M(z) ∧ M(x) ∧ x∈Pow_rel(M,X×X) ∧ well_ord(X, x) ∧ z=ordertype(X,x))"
and
strong_replacement_jc_body :
"strong_replacement(M,λ x z . M(z) ∧ M(x) ∧ z = jump_cardinal_body(M,x))"
and
surj_imp_inj_replacement:
"M(f) ⟹ M(x) ⟹ strong_replacement(M, λy z. y ∈ f -`` {x} ∧ z = {⟨x, y⟩})"
"M(f) ⟹ strong_replacement(M, λx z. z = Sigfun(x, λy. f -`` {y}))"
"M(f) ⟹ strong_replacement(M, λx y. y = f -`` {x})"
"M(f) ⟹ M(r) ⟹ strong_replacement(M, λx y. y = ⟨x, minimum(r, f -`` {x})⟩)"
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)"
unfolding is_csquare_rel_def csquare_rel_def
using csquare_lam_closed[unfolded csquare_lam_eq_lam]
by (simp add:absolut csquare_lam_eq_lam[unfolded csquare_lam_def])
end
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)
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]:
"[| wellordered(M,A,r); M(A); M(r); M(i)|] ==>
otype(M,A,r,i) ⟷ i = ordertype(A,r)"
proof (intro iffI)
assume "wellordered(M, A, r)" "M(A)" "M(r)" "M(i)" "otype(M, A, r, i)"
moreover from this
obtain f j where "M(f)" "M(j)" "Ord(j)" "f ∈ ⟨A, r⟩ ≅ ⟨j, Memrel(j)⟩"
using ordertype_exists[of A r] by auto
moreover from calculation
have "∃f[M]. f ∈ ⟨A, r⟩ ≅ ⟨j, Memrel(j)⟩" by auto
moreover
have "∃f[M]. f ∈ ⟨A, r⟩ ≅ ⟨i, Memrel(i)⟩"
proof -
note calculation
moreover from this
obtain h where "omap(M, A, r, h)" "M(h)"
using omap_exists by auto
moreover from calculation
have "h ∈ ⟨A, r⟩ ≅ ⟨i, Memrel(i)⟩"
using omap_ord_iso obase_equals by simp
moreover from calculation
have "h O converse(f) ∈ ⟨j, Memrel(j)⟩ ≅ ⟨i, Memrel(i)⟩"
using ord_iso_sym ord_iso_trans by blast
moreover from calculation
have "i=j"
using Ord_iso_implies_eq[of j i "h O converse(f)"]
Ord_otype[OF _ well_ord_is_trans_on] by simp
ultimately
show ?thesis by simp
qed
ultimately
show "i = ordertype(A, r)"
by (force intro:ordertypes_are_absolute[of A r _ i]
simp add:Ord_otype[OF _ well_ord_is_trans_on])
next
assume "wellordered(M,A, r)" "i = ordertype(A, r)"
"M(i)" "M(A)" "M(r)"
moreover from this
obtain h where "omap(M, A, r, h)" "M(h)"
using omap_exists by auto
moreover from calculation
obtain j where "otype(M,A,r,j)" "M(j)"
using otype_exists by auto
moreover from calculation
have "h ∈ ⟨A, r⟩ ≅ ⟨j, Memrel(j)⟩"
using omap_ord_iso_otype by simp
moreover from calculation
obtain f where "f ∈ ⟨A, r⟩ ≅ ⟨i, Memrel(i)⟩"
using ordertype_ord_iso by auto
moreover
have "j=i"
proof -
note calculation
moreover from this
have "h O converse(f) ∈ ⟨i, Memrel(i)⟩ ≅ ⟨j, Memrel(j)⟩"
using ord_iso_sym ord_iso_trans by blast
moreover from calculation
have "Ord(i)" using Ord_ordertype by simp
ultimately
show "j=i"
using Ord_iso_implies_eq[of i j "h O converse(f)"]
Ord_otype[OF _ well_ord_is_trans_on] by simp
qed
ultimately
show "otype(M, A, r, i)" by simp
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"
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"
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"
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
reldb_add relational "well_ord" "is_well_ord"
reldb_add functional "well_ord" "well_ord"
synthesize "is_well_ord" from_definition assuming "nonempty"
reldb_add relational "Order.pred" "pred_set"
reldb_add functional "Order.pred" "Order.pred"
reldb_add functional "Ord" "Ord"
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 is_lambda_iff_sats [iff_sats]:
assumes is_F_iff_sats:
"!!a0 a1 a2.
[|a0∈Aa; a1∈Aa; a2∈Aa|]
==> is_F(a1, a0) ⟷ sats(Aa, is_F_fm, Cons(a0,Cons(a1,Cons(a2,env))))"
shows
"nth(A, env) = Ab ⟹
nth(r, env) = ra ⟹
A ∈ nat ⟹
r ∈ nat ⟹
env ∈ list(Aa) ⟹
is_lambda(##Aa, Ab, is_F, ra) ⟷ Aa, env ⊨ lambda_fm(is_F_fm,A, r)"
using sats_lambda_fm[OF assms, of A r] by simp
lemma sats_is_wfrec_fm' :
assumes MH_iff_sats:
"!!a0 a1 a2 a3 a4.
[|a0∈A; a1∈A; a2∈A; a3∈A; a4∈A|]
==> MH(a2, a1, a0) ⟷ sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,Cons(a4,env))))))"
shows
"[|x ∈ nat; y ∈ nat; z ∈ nat; env ∈ list(A); 0 ∈ A|]
==> sats(A, is_wfrec_fm(p,x,y,z), env) ⟷
is_wfrec(##A, MH, nth(x,env), nth(y,env), nth(z,env))"
using MH_iff_sats [THEN iff_sym] nth_closed sats_is_recfun_fm
by (simp add: is_wfrec_fm_def is_wfrec_def) blast
lemma is_wfrec_iff_sats' [iff_sats]:
assumes MH_iff_sats:
"!!a0 a1 a2 a3 a4.
[|a0∈Aa; a1∈Aa; a2∈Aa; a3∈Aa; a4∈Aa|]
==> MH(a2, a1, a0) ⟷ sats(Aa, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,Cons(a4,env))))))"
"x ∈ nat" "y ∈ nat" "z ∈ nat" "env ∈ list(Aa)" "0 ∈ Aa"
"nth(x, env) = xx" "nth(y, env) = yy" "nth(z, env) = zz"
shows
"is_wfrec(##Aa, MH, xx, yy, zz) ⟷ Aa, env ⊨ is_wfrec_fm(p,x,y,z)"
using assms(7-9) sats_is_wfrec_fm'[OF assms(1-6)] by simp
lemma is_wfrec_on_iff_sats [iff_sats]:
assumes MH_iff_sats:
"!!a0 a1 a2 a3 a4.
[|a0∈Aa; a1∈Aa; a2∈Aa; a3∈Aa; a4∈Aa|]
==> MH(a2, a1, a0) ⟷ sats(Aa, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,Cons(a4,env))))))"
shows
"nth(x, env) = xx ⟹
nth(y, env) = yy ⟹
nth(z, env) = zz ⟹
x ∈ nat ⟹
y ∈ nat ⟹
z ∈ nat ⟹
env ∈ list(Aa) ⟹
0 ∈ Aa ⟹ is_wfrec_on(##Aa, MH, aa,xx, yy, zz) ⟷ Aa, env ⊨ is_wfrec_fm(p,x,y,z)"
using assms sats_is_wfrec_fm'[OF assms] unfolding is_wfrec_on_def by simp
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"
context M_pre_cardinal_arith
begin
lemma wfrec_on_pred_eq :
assumes "r ∈ Pow(A×A)" "M(A)" "M(r)"
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
moreover from this
show ?thesis
unfolding wfrec_on_def by simp
qed
lemma wfrec_on_pred_closed :
assumes "wf[A](r)" "trans[A](r)" "r ∈ Pow(A×A)" "M(A)" "M(r)" "x ∈ A"
shows "M(wfrec(r, x, λx f. f `` Order.pred(A, x, r)))"
proof -
from assms
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 by simp
moreover from assms
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
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(A×A)" "M(A)" "M(r)" "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 by simp
lemma ordermap_rel_closed' :
assumes "wf[A](r)" "trans[A](r)" "r ∈ Pow(A×A)" "M(A)" "M(r)"
shows "M(ordermap_rel(M, A, r))"
proof -
from assms
have "r ∩ A×A = r" by auto
with assms have "wf(r)" "trans(r)" "relation(r)"
unfolding wf_on_def using trans_on_iff_trans relation_def by auto
then
have 1:"⋀ x z . M(x) ⟹ M(z) ⟹
(∃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))>"
using 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] assms
wfrec_pred_replacement unfolding relation2_def
by auto
then
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]] assms by simp
then show ?thesis
using Pow_iff assms
unfolding ordermap_rel_def
apply(subst lam_cong[OF refl wfrec_on_pred_eq],simp_all)
using wfrec_on_pred_closed lam_closed
by simp
qed
lemma ordermap_rel_closed [intro,simp]:
assumes "wf[A](r)" "trans[A](r)" "r ∈ Pow(A×A)"
shows "M(A) ⟹ M(r) ⟹ M(ordermap_rel(M, A, r))"
using ordermap_rel_closed' assms by simp
lemma is_ordermap_iff :
assumes "r ∈ Pow(A×A)" "wf[A](r)" "trans[A](r)"
"M(A)" "M(r)" "M(res)"
shows "is_ordermap(M, A, r, res) ⟷ res = ordermap_rel(M, A, r)"
proof -
from ‹r ∈ Pow(A×A)›
have "r ∩ A×A = r" by auto
with assms have 1:"wf(r)" "trans(r)" "relation(r)"
unfolding wf_on_def using trans_on_iff_trans relation_def by auto
from assms
have "r ∩ A×A = r" "r ⊆ A×A" "<x,y> ∈ r ⟹ x∈A ∧ y∈A" for x y by auto
then
show ?thesis
using ordermap_rel_closed[of r A] assms wfrec_on_pred_closed wfrec_pred_replacement 1
unfolding is_ordermap_def ordermap_rel_def
apply (rule_tac lambda_abs2)
apply (simp_all add:Relation1_def)
apply 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
synthesize "is_ordermap" from_definition assuming "nonempty"
text‹Discipline for \<^term>‹ordertype››
relativize functional "ordertype" "ordertype_rel" external
relationalize "ordertype_rel" "is_ordertype"
context M_pre_cardinal_arith
begin
lemma is_ordertype_iff :
assumes "r ∈ Pow(A×A)" "wf[A](r)" "trans[A](r)"
shows "M(A) ⟹ M(r) ⟹ 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 by simp
lemma is_ordertype_iff' :
assumes "r ∈ Pow_rel(M,A×A)" "well_ord(A,r)"
shows "M(A) ⟹ M(r) ⟹ M(res) ⟹ is_ordertype(M, A, r, res) ⟷ res = ordertype_rel(M, A, r)"
using assms is_ordertype_iff Pow_rel_char
unfolding well_ord_def part_ord_def tot_ord_def by simp
lemma is_ordertype_iff'' :
assumes "well_ord(A,r)" "r⊆A×A"
shows "M(A) ⟹ M(r) ⟹ M(res) ⟹ is_ordertype(M, A, r, res) ⟷ res = ordertype_rel(M, A, r)"
using assms is_ordertype_iff
unfolding well_ord_def part_ord_def tot_ord_def by simp
end
synthesize "is_ordertype" from_definition assuming "nonempty"
definition
jump_cardinal' :: "i⇒i" where
"jump_cardinal'(K) ≡
⋃X∈Pow(K). {z. r ∈ Pow(X*X), well_ord(X,r) & z = ordertype(X,r)}"
relativize functional "jump_cardinal'" "jump_cardinal'_rel" external
relationalize "jump_cardinal'_rel" "is_jump_cardinal'"
synthesize "is_jump_cardinal'" from_definition assuming "nonempty"
arity_theorem for "is_jump_cardinal'_fm"
definition jump_cardinal_body' where
"jump_cardinal_body'(X) ≡ {z . r ∈ Pow(X × X), well_ord(X, r) ∧ z = ordertype(X, r)}"
relativize functional "jump_cardinal_body'" "jump_cardinal_body'_rel" external
relationalize "jump_cardinal_body'_rel" "is_jump_cardinal_body'"
synthesize "is_jump_cardinal_body'" from_definition assuming "nonempty"
arity_theorem for "is_jump_cardinal_body'_fm"
context M_pre_cardinal_arith
begin
lemma ordertype_rel_closed' :
assumes "wf[A](r)" "trans[A](r)" "r ∈ Pow(A×A)" "M(r)" "M(A)"
shows "M(ordertype_rel(M,A,r))"
unfolding ordertype_rel_def
using ordermap_rel_closed image_closed assms by simp
lemma ordertype_rel_closed [intro,simp]:
assumes "well_ord(A,r)" "r ∈ Pow_rel(M,A×A)" "M(A)"
shows "M(ordertype_rel(M,A,r))"
using assms Pow_rel_char ordertype_rel_closed'
unfolding well_ord_def tot_ord_def part_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 univalent_aux1 : "M(X) ⟹ univalent(M,Pow_rel(M,X×X),
λr z. M(z) ∧ M(r) ∧ r∈Pow_rel(M,X×X) ∧ is_well_ord(M, X, r) ∧ is_ordertype(M, X, r, z))"
using is_well_ord_iff_wellordered
is_ordertype_iff[of _ X]
trans_on_subset[OF well_ord_is_trans_on]
well_ord_is_wf[THEN wf_on_subset_A] mem_Pow_rel_abs
unfolding univalent_def
by (simp)
lemma jump_cardinal_body_eq :
"M(X) ⟹ jump_cardinal_body(M,X) = jump_cardinal_body'_rel(M,X)"
unfolding jump_cardinal_body_def jump_cardinal_body'_rel_def
using ordertype_rel_abs
by auto
end
context M_cardinal_arith
begin
lemma jump_cardinal_closed_aux1 :
assumes "M(X)"
shows
"M(jump_cardinal_body(M,X))"
unfolding jump_cardinal_body_def
using ‹M(X)› ordertype_rel_abs
ordertype_replacement[OF ‹M(X)›] univalent_aux1[OF ‹M(X)›]
strong_replacement_closed[where A="Pow⇗M⇖(X × X)" and
P="λ r z . M(z) ∧ M(r) ∧ r ∈ Pow⇗M⇖(X × X) ∧ well_ord(X, r) ∧ z = ordertype(X, r)"]
by auto
lemma univalent_jc_body : "M(X) ⟹ univalent(M,X,λ x z . M(z) ∧ M(x) ∧ z = jump_cardinal_body(M,x))"
using transM[of _ X] jump_cardinal_closed_aux1 by auto
lemma jump_cardinal_body_closed :
assumes "M(K)"
shows "M({a . X ∈ Pow⇗M⇖(K), M(a) ∧ M(X) ∧ a = jump_cardinal_body(M,X)})"
using assms univalent_jc_body jump_cardinal_closed_aux1 strong_replacement_jc_body
by simp
rel_closed for "jump_cardinal'"
using jump_cardinal_body_closed ordertype_rel_abs
unfolding jump_cardinal_body_def jump_cardinal'_rel_def
by simp
is_iff_rel for "jump_cardinal'"
proof -
assume types: "M(K)" "M(res)"
have "is_Replace(M, Pow_rel(M,X×X), λr z. M(z) ∧ M(r) ∧ is_well_ord(M, X, r) ∧ is_ordertype(M, X, r, z),
a) ⟷ a = {z . r ∈ Pow_rel(M,X×X), M(z) ∧ M(r) ∧ is_well_ord(M,X,r) ∧ is_ordertype(M, X, r, z)}"
if "M(X)" "M(a)" for X a
using that univalent_aux1
by (rule_tac Replace_abs) (simp_all)
then
have "is_Replace(M, Pow_rel(M,X×X), λr z. M(z) ∧ M(r) ∧ is_well_ord(M, X, r) ∧ is_ordertype(M, X, r, z),
a) ⟷ a = {z . r ∈ Pow_rel(M,X×X), M(z) ∧ M(r) ∧ well_ord(X, r) ∧ z = ordertype_rel(M, X, r)}"
if "M(X)" "M(a)" for X a
using that univalent_aux1 is_ordertype_iff' is_well_ord_iff_wellordered well_ord_abs by auto
moreover
have "is_Replace(M, d, λX a. M(a) ∧ M(X) ∧
a = {z . r ∈ Pow⇗M⇖(X × X), M(z) ∧ M(r) ∧ well_ord(X, r) ∧ z = ordertype(X, r)}, e)
⟷
e ={a . X ∈ d, M(a) ∧ M(X) ∧ a = jump_cardinal_body(M,X)}"
if "M(d)" "M(e)" for d e
using jump_cardinal_closed_aux1 that
unfolding jump_cardinal_body_def
by (rule_tac Replace_abs) simp_all
ultimately
show ?thesis
using Pow_rel_iff jump_cardinal_body_closed[of K] ordertype_rel_abs
unfolding is_jump_cardinal'_def jump_cardinal'_rel_def jump_cardinal_body_def
by (simp add: types)
qed
end
locale M_jump_cardinal= M_ordertype
context M_cardinal_arith
begin
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
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_jump_cardinal
begin
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 def_jump_cardinal_rel_aux :
"X ∈ Pow⇗M⇖(K) ⟹ well_ord(X, w) ⟹ 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 :
assumes "M(K)"
shows "jump_cardinal'_rel(M,K) =
(⋃X∈Pow_rel(M,K). {z. r ∈ Pow_rel(M,K*K), well_ord(X,r) & z = ordertype(X,r)})"
proof -
have "M({z . r ∈ Pow⇗M⇖(X × X), M(z) ∧ well_ord(X, r) ∧ z = ordertype(X, r)})"
(is "M(Replace(_,?P))")
if "M(X)" for X
using that jump_cardinal_closed_aux1[of X] ordertype_rel_abs[of X]
jump_cardinal_body_def
by (subst Replace_cong[where P="?P"
and Q="λr z. M(z) ∧ M(r) ∧ well_ord(X, r) ∧ z = ordertype_rel(M,X,r)",
OF refl, of "Pow⇗M⇖(X × X)"]) (auto dest:transM)
then
have "M({z . r ∈ Pow⇗M⇖(Y × Y), M(z) ∧ well_ord(X, r) ∧ z = ordertype(X, r)})"
if "M(Y)" "M(X)" "X ∈ Pow⇗M⇖(Y)" "well_ord(X,r)" for Y X r
using that def_jump_cardinal_rel_aux[of X Y r, symmetric] by simp
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 is_well_ord_iff_wellordered
ordertype_rel_abs transM[of _ "Pow⇗M⇖(K)"] transM[of _ "Pow⇗M⇖(K×K)"]
def_jump_cardinal_rel_aux
unfolding jump_cardinal'_rel_def
apply (intro equalityI)
apply (auto dest:transM)
apply (rename_tac X R)
apply (rule_tac x=X in bexI)
apply (rule_tac x=R in ReplaceI)
apply auto
apply (rule_tac x="{y . xa ∈ Pow⇗M⇖(K × K), M(y) ∧ M(xa) ∧ well_ord(X, xa) ∧ y = ordertype(X, xa)}" in bexI)
apply auto
by (rule_tac x=X in ReplaceI) auto
qed
notation jump_cardinal'_rel (‹jump'_cardinal'_rel›)
lemma Ord_jump_cardinal_rel : "M(K) ⟹ Ord(jump_cardinal_rel(M,K))"
apply (unfold def_jump_cardinal_rel)
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)
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 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