Theory Cardinal_AC_Relative
section‹Relative, Cardinal Arithmetic Using AC›
theory Cardinal_AC_Relative
imports
ZF_Miscellanea
Interface
CardinalArith_Relative
begin
locale M_AC=
fixes M
assumes
choice_ax: "choice_ax(M)"
locale M_cardinal_AC= M_cardinal_arith + M_AC
begin
lemma well_ord_surj_imp_lepoll_rel :
assumes "well_ord(A,r)" "h ∈ surj(A,B)" and
types:"M(A)" "M(r)" "M(h)" "M(B)"
shows "B ≲⇗M⇖ A"
proof -
note eq=vimage_fun_sing[OF surj_is_fun[OF ‹h∈_›]]
from assms
have "(λb∈B. minimum(r, {a∈A. h`a=b})) ∈ inj(B,A)" (is "?f∈_")
using well_ord_surj_imp_inj_inverse assms(1,2) by simp
with assms
have "M(?f`b)" if "b∈B" for b
using apply_type[OF inj_is_fun[OF ‹?f∈_›]] that transM[OF _ ‹M(A)›] by simp
with assms
have "M(?f)"
using lam_closed surj_imp_inj_replacement(4) eq by auto
with ‹?f∈_› assms
have "?f ∈ inj⇗M⇖(B,A)"
using mem_inj_abs by simp
with ‹M(?f)›
show ?thesis unfolding lepoll_rel_def by auto
qed
lemma surj_imp_well_ord_M :
assumes wos: "well_ord(A,r)" "h ∈ surj(A,B)"
and
types: "M(A)" "M(r)" "M(h)" "M(B)"
shows "∃s[M]. well_ord(B,s)"
using assms lepoll_rel_well_ord
well_ord_surj_imp_lepoll_rel by fast
lemma choice_ax_well_ord : "M(S) ⟹ ∃r[M]. well_ord(S,r)"
using choice_ax well_ord_Memrel[THEN surj_imp_well_ord_M]
unfolding choice_ax_def by auto
end
locale M_Pi_assumptions_choice= M_Pi_assumptions + M_cardinal_AC +
assumes
B_replacement: "strong_replacement(M, λx y. y = B(x))"
and
minimum_replacement: "M(r) ⟹ strong_replacement(M, λx y. y = ⟨x, minimum(r, B(x))⟩)"
begin
lemma AC_M :
assumes "a ∈ A" "⋀x. x ∈ A ⟹ ∃y. y ∈ B(x)"
shows "∃z[M]. z ∈ Pi⇗M⇖(A, B)"
proof -
have "M(⋃x∈A. B(x))" using assms family_union_closed Pi_assumptions B_replacement by simp
then
obtain r where "well_ord(⋃x∈A. B(x),r)" "M(r)"
using choice_ax_well_ord by blast
let ?f="λx∈A. minimum(r,B(x))"
have "M(minimum(r, B(x)))" if "x∈A" for x
proof -
from ‹well_ord(_,r)› ‹x∈A›
have "well_ord(B(x),r)" using well_ord_subset UN_upper by simp
with assms ‹x∈A› ‹M(r)›
show ?thesis using Pi_assumptions by blast
qed
with assms and ‹M(r)›
have "M(?f)"
using Pi_assumptions minimum_replacement lam_closed
by simp
moreover from assms and calculation
have "?f ∈ Pi⇗M⇖(A,B)"
using lam_type[OF minimum_in, OF ‹well_ord(⋃x∈A. B(x),r)›, of A B]
Pi_rel_char by auto
ultimately
show ?thesis by blast
qed
lemma AC_Pi_rel : assumes "⋀x. x ∈ A ⟹ ∃y. y ∈ B(x)"
shows "∃z[M]. z ∈ Pi⇗M⇖(A, B)"
proof (cases "A=0")
interpret Pi0:M_Pi_assumptions_0
using Pi_assumptions by unfold_locales auto
case True
then
show ?thesis using assms by simp
next
case False
then
obtain a where "a ∈ A" by auto
with assms
show ?thesis by (blast intro!: AC_M)
qed
end
context M_cardinal_AC
begin
subsection‹Strengthened Forms of Existing Theorems on Cardinals›
lemma cardinal_rel_eqpoll_rel : "M(A) ⟹ |A|⇗M⇖ ≈⇗M⇖ A"
apply (rule choice_ax_well_ord [THEN rexE])
apply (auto intro:well_ord_cardinal_rel_eqpoll_rel)
done
lemmas cardinal_rel_idem= cardinal_rel_eqpoll_rel [THEN cardinal_rel_cong, simp]
lemma cardinal_rel_eqE : "|X|⇗M⇖ = |Y|⇗M⇖ ==> M(X) ⟹ M(Y) ⟹ X ≈⇗M⇖ Y"
apply (rule choice_ax_well_ord [THEN rexE], assumption)
apply (rule choice_ax_well_ord [THEN rexE, of Y], assumption)
apply (rule well_ord_cardinal_rel_eqE, assumption+)
done
lemma cardinal_rel_eqpoll_rel_iff : "M(X) ⟹ M(Y) ⟹ |X|⇗M⇖ = |Y|⇗M⇖ ⟷ X ≈⇗M⇖ Y"
by (blast intro: cardinal_rel_cong cardinal_rel_eqE)
lemma cardinal_rel_disjoint_Un :
"[| |A|⇗M⇖=|B|⇗M⇖; |C|⇗M⇖=|D|⇗M⇖; A ∩ C = 0; B ∩ D = 0; M(A); M(B); M(C); M(D)|]
==> |A ∪ C|⇗M⇖ = |B ∪ D|⇗M⇖"
by (simp add: cardinal_rel_eqpoll_rel_iff eqpoll_rel_disjoint_Un)
lemma lepoll_rel_imp_cardinal_rel_le : "A ≲⇗M⇖ B ==> M(A) ⟹ M(B) ⟹ |A|⇗M⇖ ≤ |B|⇗M⇖"
apply (rule choice_ax_well_ord [THEN rexE]) prefer 2
apply (erule well_ord_lepoll_rel_imp_cardinal_rel_le, assumption+)
done
lemma cadd_rel_assoc : "⟦M(i); M(j); M(k)⟧ ⟹ (i ⊕⇗M⇖ j) ⊕⇗M⇖ k = i ⊕⇗M⇖ (j ⊕⇗M⇖ k)"
apply (rule choice_ax_well_ord [THEN rexE]) prefer 2
apply (rule choice_ax_well_ord [THEN rexE]) prefer 2
apply (rule choice_ax_well_ord [THEN rexE]) prefer 2
apply (rule well_ord_cadd_rel_assoc, assumption+)
done
lemma cmult_rel_assoc : "⟦M(i); M(j); M(k)⟧ ⟹ (i ⊗⇗M⇖ j) ⊗⇗M⇖ k = i ⊗⇗M⇖ (j ⊗⇗M⇖ k)"
apply (rule choice_ax_well_ord [THEN rexE]) prefer 2
apply (rule choice_ax_well_ord [THEN rexE]) prefer 2
apply (rule choice_ax_well_ord [THEN rexE]) prefer 2
apply (rule well_ord_cmult_rel_assoc, assumption+)
done
lemma cadd_cmult_distrib : "⟦M(i); M(j); M(k)⟧ ⟹ (i ⊕⇗M⇖ j) ⊗⇗M⇖ k = (i ⊗⇗M⇖ k) ⊕⇗M⇖ (j ⊗⇗M⇖ k)"
apply (rule choice_ax_well_ord [THEN rexE]) prefer 2
apply (rule choice_ax_well_ord [THEN rexE]) prefer 2
apply (rule choice_ax_well_ord [THEN rexE]) prefer 2
apply (rule well_ord_cadd_cmult_distrib, assumption+)
done
lemma InfCard_rel_square_eq : "InfCard⇗M⇖(|A|⇗M⇖) ⟹ M(A) ⟹ A×A ≈⇗M⇖ A"
apply (rule choice_ax_well_ord [THEN rexE]) prefer 2
apply (erule well_ord_InfCard_rel_square_eq, assumption, simp_all)
done
subsection ‹The relationship between cardinality and le-pollence›
lemma Card_rel_le_imp_lepoll_rel :
assumes "|A|⇗M⇖ ≤ |B|⇗M⇖"
and types: "M(A)" "M(B)"
shows "A ≲⇗M⇖ B"
proof -
have "A ≈⇗M⇖ |A|⇗M⇖"
by (rule cardinal_rel_eqpoll_rel [THEN eqpoll_rel_sym], simp_all add:types)
also have "... ≲⇗M⇖ |B|⇗M⇖"
by (rule le_imp_subset [THEN subset_imp_lepoll_rel]) (rule assms, simp_all add:types)
also have "... ≈⇗M⇖ B"
by (rule cardinal_rel_eqpoll_rel, simp_all add:types)
finally show ?thesis by (simp_all add:types)
qed
lemma le_Card_rel_iff : "Card⇗M⇖(K) ==> M(K) ⟹ M(A) ⟹ |A|⇗M⇖ ≤ K ⟷ A ≲⇗M⇖ K"
apply (erule Card_rel_cardinal_rel_eq [THEN subst], assumption, rule iffI,
erule Card_rel_le_imp_lepoll_rel, assumption+)
apply (erule lepoll_rel_imp_cardinal_rel_le, assumption+)
done
lemma cardinal_rel_0_iff_0 [simp]: "M(A) ⟹ |A|⇗M⇖ = 0 ⟷ A = 0"
using cardinal_rel_0 eqpoll_rel_0_iff [THEN iffD1]
cardinal_rel_eqpoll_rel_iff [THEN iffD1, OF _ nonempty]
by auto
lemma cardinal_rel_lt_iff_lesspoll_rel :
assumes i: "Ord(i)" and
types: "M(i)" "M(A)"
shows "i < |A|⇗M⇖ ⟷ i ≺⇗M⇖ A"
proof
assume "i < |A|⇗M⇖"
hence "i ≺⇗M⇖ |A|⇗M⇖"
by (blast intro: lt_Card_rel_imp_lesspoll_rel types)
also have "... ≈⇗M⇖ A"
by (rule cardinal_rel_eqpoll_rel) (simp_all add:types)
finally show "i ≺⇗M⇖ A" by (simp_all add:types)
next
assume "i ≺⇗M⇖ A"
also have "... ≈⇗M⇖ |A|⇗M⇖"
by (blast intro: cardinal_rel_eqpoll_rel eqpoll_rel_sym types)
finally have "i ≺⇗M⇖ |A|⇗M⇖" by (simp_all add:types)
thus "i < |A|⇗M⇖" using i types
by (force intro: cardinal_rel_lt_imp_lt lesspoll_rel_cardinal_rel_lt)
qed
lemma cardinal_rel_le_imp_lepoll_rel : " i ≤ |A|⇗M⇖ ==> M(i) ⟹ M(A) ⟹i ≲⇗M⇖ A"
by (blast intro: lt_Ord Card_rel_le_imp_lepoll_rel Ord_cardinal_rel_le le_trans)
subsection‹Other Applications of AC›
text‹We have an example of instantiating a locale involving higher
order variables inside a proof, by using the assumptions of the
first order, active locale.›
lemma surj_rel_implies_inj_rel :
assumes f: "f ∈ surj⇗M⇖(X,Y)" and
types: "M(f)" "M(X)" "M(Y)"
shows "∃g[M]. g ∈ inj⇗M⇖(Y,X)"
proof -
from types
interpret M_Pi_assumptions_choice _ Y "λy. f-``{y}"
by unfold_locales (auto intro:surj_imp_inj_replacement dest:transM)
from f AC_Pi_rel
obtain z where z: "z ∈ Pi⇗M⇖(Y, λy. f -`` {y})"
using surj_rel_char
by (auto simp add: surj_def types) (fast dest: apply_Pair)
show ?thesis
proof
show "z ∈ inj⇗M⇖(Y, X)" "M(z)"
using z surj_is_fun[of f X Y] f Pi_rel_char
by (auto dest: apply_type Pi_memberD
intro: apply_equality Pi_type f_imp_injective
simp add:types mem_surj_abs)
qed
qed
text‹Kunen's Lemma 10.20›
lemma surj_rel_implies_cardinal_rel_le :
assumes f: "f ∈ surj⇗M⇖(X,Y)" and
types:"M(f)" "M(X)" "M(Y)"
shows "|Y|⇗M⇖ ≤ |X|⇗M⇖"
proof (rule lepoll_rel_imp_cardinal_rel_le)
from f [THEN surj_rel_implies_inj_rel]
obtain g where "g ∈ inj⇗M⇖(Y,X)"
by (blast intro:types)
then
show "Y ≲⇗M⇖ X"
using inj_rel_char
by (auto simp add: def_lepoll_rel types)
qed (simp_all add:types)
end
text‹The set-theoretic universe.›
abbreviation
Universe :: "i⇒o" (‹𝒱›) where
"𝒱(x) ≡ True"
lemma separation_absolute : "separation(𝒱, P)"
unfolding separation_def
by (rule rallI, rule_tac x="{x∈_ . P(x)}" in rexI) auto
lemma univalent_absolute :
assumes "univalent(𝒱, A, P)" "P(x, b)" "x ∈ A"
shows "P(x, y) ⟹ y = b"
using assms
unfolding univalent_def by force
lemma replacement_absolute : "strong_replacement(𝒱, P)"
unfolding strong_replacement_def
proof (intro rallI impI)
fix A
assume "univalent(𝒱, A, P)"
then
show "∃Y[𝒱]. ∀b[𝒱]. b ∈ Y ⟷ (∃x[𝒱]. x ∈ A ∧ P(x, b))"
by (rule_tac x="{y. x∈A , P(x,y)}" in rexI)
(auto dest:univalent_absolute[of _ P])
qed
lemma Union_ax_absolute : "Union_ax(𝒱)"
unfolding Union_ax_def big_union_def
by (auto intro:rexI[of _ "⋃_"])
lemma upair_ax_absolute : "upair_ax(𝒱)"
unfolding upair_ax_def upair_def rall_def rex_def
by (auto)
lemma power_ax_absolute :"power_ax(𝒱)"
proof -
{
fix x
have "∀y[𝒱]. y ∈ Pow(x) ⟷ (∀z[𝒱]. z ∈ y ⟶ z ∈ x)"
by auto
}
then
show "power_ax(𝒱)"
unfolding power_ax_def powerset_def subset_def by blast
qed
locale M_cardinal_UN= M_Pi_assumptions_choice _ K X for K X +
assumes
X_witness_in_M: "w ∈ X(x) ⟹ M(x)"
and
lam_m_replacement:"M(f) ⟹ strong_replacement(M,
λx y. y = ⟨x, μ i. x ∈ X(i), f ` (μ i. x ∈ X(i)) ` x⟩)"
and
inj_replacement:
"M(x) ⟹ strong_replacement(M, λy z. y ∈ inj⇗M⇖(X(x), K) ∧ z = {⟨x, y⟩})"
"strong_replacement(M, λx y. y = inj⇗M⇖(X(x), K))"
"strong_replacement(M,
λx z. z = Sigfun(x, λi. inj⇗M⇖(X(i), K)))"
"M(r) ⟹ strong_replacement(M,
λx y. y = ⟨x, minimum(r, inj⇗M⇖(X(x), K))⟩)"
begin
lemma UN_closed : "M(⋃i∈K. X(i))"
using family_union_closed B_replacement Pi_assumptions by simp
text‹Kunen's Lemma 10.21›
lemma cardinal_rel_UN_le :
assumes K: "InfCard⇗M⇖(K)"
shows "(⋀i. i∈K ⟹ |X(i)|⇗M⇖ ≤ K) ⟹ |⋃i∈K. X(i)|⇗M⇖ ≤ K"
proof (simp add: K InfCard_rel_is_Card_rel le_Card_rel_iff Pi_assumptions)
have "M(f) ⟹ M(λx∈(⋃x∈K. X(x)). ⟨μ i. x ∈ X(i), f ` (μ i. x ∈ X(i)) ` x⟩)" for f
using lam_m_replacement X_witness_in_M Least_closed' Pi_assumptions UN_closed
by (rule_tac lam_closed) (auto dest:transM)
note types = this Pi_assumptions UN_closed
have [intro]: "Ord(K)" by (blast intro: InfCard_rel_is_Card_rel
Card_rel_is_Ord K types)
interpret pii:M_Pi_assumptions_choice _ K "λi. inj⇗M⇖(X(i), K)"
using inj_replacement Pi_assumptions transM[of _ K]
by unfold_locales (simp_all del:mem_inj_abs)
assume asm:"⋀i. i∈K ⟹ X(i) ≲⇗M⇖ K"
then
have "⋀i. i∈K ⟹ M(inj⇗M⇖(X(i), K))"
by (auto simp add: types)
interpret V:M_N_Perm M "𝒱"
using separation_absolute replacement_absolute Union_ax_absolute
power_ax_absolute upair_ax_absolute
by unfold_locales auto
note bad_simps[simp del] = V.N.Forall_in_M_iff V.N.Equal_in_M_iff
V.N.nonempty
have abs:"inj_rel(𝒱,x,y) = inj(x,y)" for x y
using V.N.inj_rel_char by simp
from asm
have "⋀i. i∈K ⟹ ∃f[M]. f ∈ inj⇗M⇖(X(i), K)"
by (simp add: types def_lepoll_rel)
then
obtain f where "f ∈ (∏i∈K. inj⇗M⇖(X(i), K))" "M(f)"
using pii.AC_Pi_rel pii.Pi_rel_char by auto
with abs
have f:"f ∈ (∏i∈K. inj(X(i), K))"
using Pi_weaken_type[OF _ V.inj_rel_transfer, of f K X "λ_. K"]
Pi_assumptions by simp
{ fix z
assume z: "z ∈ (⋃i∈K. X(i))"
then obtain i where i: "i ∈ K" "Ord(i)" "z ∈ X(i)"
by (blast intro: Ord_in_Ord [of K])
hence "(μ i. z ∈ X(i)) ≤ i" by (fast intro: Least_le)
hence "(μ i. z ∈ X(i)) < K" by (best intro: lt_trans1 ltI i)
hence "(μ i. z ∈ X(i)) ∈ K" and "z ∈ X(μ i. z ∈ X(i))"
by (auto intro: LeastI ltD i)
} note mems = this
have "(⋃i∈K. X(i)) ≲⇗M⇖ K × K"
proof (simp add:types def_lepoll_rel)
show "∃f[M]. f ∈ inj(⋃x∈K. X(x), K × K)"
apply (rule rexI)
apply (rule_tac c = "λz. ⟨μ i. z ∈ X(i), f ` (μ i. z ∈ X(i)) ` z⟩"
and d = "λ⟨i,j⟩. converse (f`i) ` j" in lam_injective)
apply (force intro: f inj_is_fun mems apply_type Perm.left_inverse)+
apply (simp add:types ‹M(f)›)
done
qed
also have "... ≈⇗M⇖ K"
by (simp add: K InfCard_rel_square_eq InfCard_rel_is_Card_rel
Card_rel_cardinal_rel_eq types)
finally have "(⋃i∈K. X(i)) ≲⇗M⇖ K" by (simp_all add:types)
then
show ?thesis
by (simp add: K InfCard_rel_is_Card_rel le_Card_rel_iff types)
qed
end
end