Theory ZF_Library
section‹Library of basic $\ZF$ results\label{sec:zf-lib}›
theory ZF_Library
imports
"ZF-Constructible.Normal"
begin
text‹This theory gathers basic ``combinatorial'' results that can be proved
in $\ZF$ (that is, without using the Axiom of Choice $\AC$).
›
text‹We begin by setting up math-friendly notation.›
no_notation oadd (infixl ‹++› 65)
no_notation sum (infixr ‹+› 65)
notation oadd (infixl ‹+› 65)
notation nat (‹ω›)
notation csucc (‹_⇧+› [90])
no_notation Aleph (‹ℵ_› [90] 90)
notation Aleph (‹ℵ⇘_⇙›)
syntax "_ge" :: "[i,i] ⇒ o" (infixl ‹≥› 50)
translations "x ≥ y" ⇀ "y ≤ x"
subsection‹Some minimal arithmetic/ordinal stuff›
lemma Un_leD1 : "i ∪ j ≤ k ⟹ Ord(i) ⟹ Ord(j) ⟹ Ord(k) ⟹ i ≤ k"
by (rule Un_least_lt_iff[THEN iffD1[THEN conjunct1]],simp_all)
lemma Un_leD2 : "i ∪ j ≤ k ⟹ Ord(i) ⟹ Ord(j) ⟹ Ord(k) ⟹ j ≤ k"
by (rule Un_least_lt_iff[THEN iffD1[THEN conjunct2]],simp_all)
lemma Un_memD1: "i ∪ j ∈ k ⟹ Ord(i) ⟹ Ord(j) ⟹ Ord(k) ⟹ i ≤ k"
by (drule ltI, assumption, drule leI, rule Un_least_lt_iff[THEN iffD1[THEN conjunct1]],simp_all)
lemma Un_memD2 : "i ∪ j ∈ k ⟹ Ord(i) ⟹ Ord(j) ⟹ Ord(k) ⟹ j ≤ k"
by (drule ltI, assumption, drule leI, rule Un_least_lt_iff[THEN iffD1[THEN conjunct2]],simp_all)
text‹This lemma allows to apply arithmetic simprocs to ordinal addition›
lemma nat_oadd_add[simp]:
assumes "m ∈ ω" "n ∈ ω" shows "n + m = n #+ m"
using assms
by induct simp_all
lemma Ord_has_max_imp_succ:
assumes "Ord(γ)" "β ∈ γ" "∀α∈γ. α ≤ β"
shows "γ = succ(β)"
using assms Ord_trans[of _ β γ]
unfolding lt_def
by (intro equalityI subsetI) auto
lemma Least_antitone:
assumes
"Ord(j)" "P(j)" "⋀i. P(i) ⟹ Q(i)"
shows
"(μ i. Q(i)) ≤ (μ i. P(i))"
using assms LeastI2[of P j Q] Least_le by simp
lemma Least_set_antitone:
"Ord(j) ⟹ j∈A ⟹ A ⊆ B ⟹ (μ i. i∈B) ≤ (μ i. i∈A)"
using subset_iff by (auto intro:Least_antitone)
lemma le_neq_imp_lt:
"x≤y ⟹ x≠y ⟹ x<y"
using ltD ltI[of x y] le_Ord2
unfolding succ_def by auto
text‹Strict upper bound of a set of ordinals.›
definition
str_bound :: "i⇒i" where
"str_bound(A) ≡ ⋃a∈A. succ(a)"
lemma str_bound_type [TC]: "∀a∈A. Ord(a) ⟹ Ord(str_bound(A))"
unfolding str_bound_def by auto
lemma str_bound_lt: "∀a∈A. Ord(a) ⟹ ∀a∈A. a < str_bound(A)"
unfolding str_bound_def using str_bound_type
by (blast intro:ltI)
lemma naturals_lt_nat[intro]: "n ∈ ω ⟹ n < ω"
unfolding lt_def by simp
text‹The next two lemmas are handy when one is constructing
some object recursively. The first handles injectivity (of recursively
constructed sequences of sets), while the second is helpful for
establishing a symmetry argument.›
lemma Int_eq_zero_imp_not_eq:
assumes
"⋀x y. x∈D ⟹ y ∈ D ⟹ x ≠ y ⟹ A(x) ∩ A(y) = 0"
"⋀x. x∈D ⟹ A(x) ≠ 0" "a∈D" "b∈D" "a≠b"
shows
"A(a) ≠ A(b)"
using assms by fastforce
lemma lt_neq_symmetry:
assumes
"⋀α β. α ∈ γ ⟹ β ∈ γ ⟹ α < β ⟹ Q(α,β)"
"⋀α β. Q(α,β) ⟹ Q(β,α)"
"α ∈ γ" "β ∈ γ" "α ≠ β"
"Ord(γ)"
shows
"Q(α,β)"
proof -
from assms
consider "α<β" | "β<α"
using Ord_linear_lt[of α β thesis] Ord_in_Ord[of γ]
by auto
then
show ?thesis by cases (auto simp add:assms)
qed
lemma cardinal_succ_not_0: "|A| = succ(n) ⟹ A ≠ 0"
by auto
lemma Ord_eq_Collect_lt: "i<α ⟹ {j∈α. j<i} = i"
apply (rule equalityI)
apply (blast dest: ltD)
apply (auto simp add: Ord_mem_iff_lt)
apply (rule Ord_trans ltI[OF _ lt_Ord]; auto simp add:lt_def dest:ltD)+
done
subsection‹Manipulation of function spaces›
definition
Finite_to_one :: "[i,i] ⇒ i" where
"Finite_to_one(X,Y) ≡ {f:X→Y. ∀y∈Y. Finite({x∈X . f`x = y})}"
lemma Finite_to_oneI[intro]:
assumes "f:X→Y" "⋀y. y∈Y ⟹ Finite({x∈X . f`x = y})"
shows "f ∈ Finite_to_one(X,Y)"
using assms unfolding Finite_to_one_def by simp
lemma Finite_to_oneD[dest]:
"f ∈ Finite_to_one(X,Y) ⟹ f:X→Y"
"f ∈ Finite_to_one(X,Y) ⟹ y∈Y ⟹ Finite({x∈X . f`x = y})"
unfolding Finite_to_one_def by simp_all
lemma subset_Diff_Un: "X ⊆ A ⟹ A = (A - X) ∪ X " by auto
lemma Diff_bij:
assumes "∀A∈F. X ⊆ A" shows "(λA∈F. A-X) ∈ bij(F, {A-X. A∈F})"
using assms unfolding bij_def inj_def surj_def
by (auto intro:lam_type, subst subset_Diff_Un[of X]) auto
lemma function_space_nonempty:
assumes "b∈B"
shows "(λx∈A. b) : A → B"
using assms lam_type by force
lemma vimage_lam: "(λx∈A. f(x)) -`` B = { x∈A . f(x) ∈ B }"
using lam_funtype[of A f, THEN [2] domain_type]
lam_funtype[of A f, THEN [2] apply_equality] lamI[of _ A f]
by auto blast
lemma range_fun_subset_codomain:
assumes "h:B → C"
shows "range(h) ⊆ C"
unfolding range_def domain_def converse_def using range_type[OF _ assms] by auto
lemma Pi_rangeD:
assumes "f∈Pi(A,B)" "b ∈ range(f)"
shows "∃a∈A. f`a = b"
using assms apply_equality[OF _ assms(1), of _ b]
domain_type[OF _ assms(1)] by auto
lemma Pi_range_eq: "f ∈ Pi(A,B) ⟹ range(f) = {f ` x . x ∈ A}"
using Pi_rangeD[of f A B] apply_rangeI[of f A B]
by blast
lemma Pi_vimage_subset : "f ∈ Pi(A,B) ⟹ f-``C ⊆ A"
unfolding Pi_def by auto
lemma apply_in_codomain_Ord:
assumes
"Ord(γ)" "γ≠0" "f: A → γ"
shows
"f`x∈γ"
proof (cases "x∈A")
case True
from assms ‹x∈A›
show ?thesis
using domain_of_fun apply_rangeI by simp
next
case False
from assms ‹x∉A›
show ?thesis
using apply_0 Ord_0_lt ltD domain_of_fun by auto
qed
lemma range_eq_image:
assumes "f:A→B"
shows "range(f) = f``A"
proof
show "f `` A ⊆ range(f)"
unfolding image_def by blast
{
fix x
assume "x∈range(f)"
with assms
have "x∈f``A"
using domain_of_fun[of f A "λ_. B"] by auto
}
then
show "range(f) ⊆ f `` A" ..
qed
lemma Image_sub_codomain: "f:A→B ⟹ f``C ⊆ B"
using image_subset fun_is_rel[of _ _ "λ_ . B"] by force
lemma inj_to_Image:
assumes
"f:A→B" "f ∈ inj(A,B)"
shows
"f ∈ inj(A,f``A)"
using assms inj_inj_range range_eq_image by force
lemma inj_imp_surj:
fixes f b
notes inj_is_fun[dest]
defines [simp]: "ifx(x) ≡ if x∈range(f) then converse(f)`x else b"
assumes "f ∈ inj(B,A)" "b∈B"
shows "(λx∈A. ifx(x)) ∈ surj(A,B)"
proof -
from assms
have "converse(f) ∈ surj(range(f),B)" "range(f) ⊆ A"
"converse(f) : range(f) → B"
using inj_converse_surj range_fun_subset_codomain surj_is_fun by blast+
with ‹b∈B›
show "(λx∈A. ifx(x)) ∈ surj(A,B)"
unfolding surj_def
proof (intro CollectI lam_type ballI; elim CollectE)
fix y
assume "y ∈ B" "∀y∈B. ∃x∈range(f). converse(f) ` x = y"
with ‹range(f) ⊆ A›
show "∃x∈A. (λx∈A. ifx(x)) ` x = y"
by (drule_tac bspec, auto)
qed simp
qed
lemma fun_Pi_disjoint_Un:
assumes "f ∈ Pi(A,B)" "g ∈ Pi(C,D)" "A ∩ C = 0"
shows "f ∪ g ∈ Pi(A ∪ C, λx. B(x) ∪ D(x))"
using assms
by (simp add: Pi_iff extension Un_rls) (unfold function_def, blast)
lemma Un_restrict_decomposition:
assumes "f ∈ Pi(A,B)"
shows "f = restrict(f, A ∩ C) ∪ restrict(f, A - C)"
using assms
proof (rule fun_extension)
from assms
have "restrict(f,A∩C) ∪ restrict(f,A-C) ∈ Pi(A∩C ∪ (A-C), λx. B(x)∪B(x))"
using restrict_type2[of f A B]
by (rule_tac fun_Pi_disjoint_Un) force+
moreover
have "(A ∩ C) ∪ (A - C) = A" by auto
ultimately
show "restrict(f, A ∩ C) ∪ restrict(f, A - C) ∈ Pi(A, B)" by simp
next
fix x
assume "x ∈ A"
with assms
show "f ` x = (restrict(f, A ∩ C) ∪ restrict(f, A - C)) ` x"
using restrict fun_disjoint_apply1[of _ "restrict(f,_)"]
fun_disjoint_apply2[of _ "restrict(f,_)"]
domain_restrict[of f] apply_0 domain_of_fun
by (cases "x∈C") simp_all
qed
lemma restrict_eq_imp_Un_into_Pi:
assumes "f ∈ Pi(A,B)" "g ∈ Pi(C,D)" "restrict(f, A ∩ C) = restrict(g, A ∩ C)"
shows "f ∪ g ∈ Pi(A ∪ C, λx. B(x) ∪ D(x))"
proof -
note assms
moreover from this
have "x ∉ g ⟹ x ∉ restrict(g, A ∩ C)" for x
using restrict_subset[of g "A ∩ C"] by auto
moreover from calculation
have "x ∈ f ⟹ x ∈ restrict(f, A - C) ∨ x ∈ restrict(g, A ∩ C)" for x
by (subst (asm) Un_restrict_decomposition[of f A B "C"]) auto
ultimately
have "f ∪ g = restrict(f, A - C) ∪ g"
using restrict_subset[of g "A ∩ C"]
by (subst Un_restrict_decomposition[of f A B "C"]) auto
moreover
have "A - C ∪ C = A ∪ C" by auto
moreover
note assms
ultimately
show ?thesis
using fun_Pi_disjoint_Un[OF
restrict_type2[of f A B "A-C"], of g C D]
by auto
qed
lemma restrict_eq_imp_Un_into_Pi':
assumes "f ∈ Pi(A,B)" "g ∈ Pi(C,D)"
"restrict(f, domain(f) ∩ domain(g)) = restrict(g, domain(f) ∩ domain(g))"
shows "f ∪ g ∈ Pi(A ∪ C, λx. B(x) ∪ D(x))"
using assms domain_of_fun restrict_eq_imp_Un_into_Pi by simp
lemma restrict_subset_Sigma: "f ⊆ Sigma(C,B) ⟹ restrict(f,A) ⊆ Sigma(A∩C, B)"
by (auto simp add: restrict_def)
subsection‹Finite sets›
lemma Replace_sing1:
"⟦ (∃a. P(d,a)) ∧ (∀y y'. P(d,y) ⟶ P(d,y') ⟶ y=y') ⟧ ⟹ ∃a. {y . x ∈ {d}, P(x,y)} = {a}"
by blast
lemma Replace_sing2:
assumes "∀a. ¬ P(d,a)"
shows "{y . x ∈ {d}, P(x,y)} = 0"
using assms by auto
lemma Replace_sing3:
assumes "∃c e. c ≠ e ∧ P(d,c) ∧ P(d,e)"
shows "{y . x ∈ {d}, P(x,y)} = 0"
proof -
{
fix z
{
assume "∀y. P(d, y) ⟶ y = z"
with assms
have "False" by auto
}
then
have "z ∉ {y . x ∈ {d}, P(x,y)}"
using Replace_iff by auto
}
then
show ?thesis
by (intro equalityI subsetI) simp_all
qed
lemma Replace_Un: "{b . a ∈ A ∪ B, Q(a, b)} =
{b . a ∈ A, Q(a, b)} ∪ {b . a ∈ B, Q(a, b)}"
by (intro equalityI subsetI) (auto simp add:Replace_iff)
lemma Replace_subset_sing: "∃z. {y . x ∈ {d}, P(x,y)} ⊆ {z}"
proof -
consider
(1) "(∃a. P(d,a)) ∧ (∀y y'. P(d,y) ⟶ P(d,y') ⟶ y=y')" |
(2) "∀a. ¬ P(d,a)" | (3) "∃c e. c ≠ e ∧ P(d,c) ∧ P(d,e)" by auto
then
show "∃z. {y . x ∈ {d}, P(x,y)} ⊆ {z}"
proof (cases)
case 1
then show ?thesis using Replace_sing1[of P d] by auto
next
case 2
then show ?thesis by auto
next
case 3
then show ?thesis using Replace_sing3[of P d] by auto
qed
qed
lemma Finite_Replace: "Finite(A) ⟹ Finite(Replace(A,Q))"
proof (induct rule:Finite_induct)
case 0
then
show ?case by simp
next
case (cons x B)
moreover
have "{b . a ∈ cons(x, B), Q(a, b)} =
{b . a ∈ B, Q(a, b)} ∪ {b . a ∈ {x}, Q(a, b)}"
using Replace_Un unfolding cons_def by auto
moreover
obtain d where "{b . a ∈ {x}, Q(a, b)} ⊆ {d}"
using Replace_subset_sing[of _ Q] by blast
moreover from this
have "Finite({b . a ∈ {x}, Q(a, b)})"
using subset_Finite by simp
ultimately
show ?case using subset_Finite by simp
qed
lemma Finite_domain: "Finite(A) ⟹ Finite(domain(A))"
using Finite_Replace unfolding domain_def
by auto
lemma Finite_converse: "Finite(A) ⟹ Finite(converse(A))"
using Finite_Replace unfolding converse_def
by auto
lemma Finite_range: "Finite(A) ⟹ Finite(range(A))"
using Finite_domain Finite_converse unfolding range_def
by blast
lemma Finite_Sigma: "Finite(A) ⟹ ∀x. Finite(B(x)) ⟹ Finite(Sigma(A,B))"
unfolding Sigma_def using Finite_RepFun Finite_Union
by simp
lemma Finite_Pi: "Finite(A) ⟹ ∀x. Finite(B(x)) ⟹ Finite(Pi(A,B))"
using Finite_Sigma
Finite_Pow subset_Finite[of "Pi(A,B)" "Pow(Sigma(A,B))"]
unfolding Pi_def
by auto
subsection‹Basic results on equipollence, cardinality and related concepts›
lemma lepollD[dest]: "A ≲ B ⟹ ∃f. f ∈ inj(A, B)"
unfolding lepoll_def .
lemma lepollI[intro]: "f ∈ inj(A, B) ⟹ A ≲ B"
unfolding lepoll_def by blast
lemma eqpollD[dest]: "A ≈ B ⟹ ∃f. f ∈ bij(A, B)"
unfolding eqpoll_def .
declare bij_imp_eqpoll[intro]
lemma range_of_subset_eqpoll:
assumes "f ∈ inj(X,Y)" "S ⊆ X"
shows "S ≈ f `` S"
using assms restrict_bij by blast
text‹I thank Miguel Pagano for this proof.›
lemma function_space_eqpoll_cong:
assumes
"A ≈ A'" "B ≈ B'"
shows
"A → B ≈ A' → B'"
proof -
from assms(1)[THEN eqpoll_sym] assms(2)
obtain f g where "f ∈ bij(A',A)" "g ∈ bij(B,B')"
by blast
then
have "converse(g) : B' → B" "converse(f): A → A'"
using bij_converse_bij bij_is_fun by auto
show ?thesis
unfolding eqpoll_def
proof (intro exI fg_imp_bijective, rule_tac [1-2] lam_type)
fix F
assume "F: A → B"
with ‹f ∈ bij(A',A)› ‹g ∈ bij(B,B')›
show "g O F O f : A' → B'"
using bij_is_fun comp_fun by blast
next
fix F
assume "F: A' → B'"
with ‹converse(g) : B' → B› ‹converse(f): A → A'›
show "converse(g) O F O converse(f) : A → B"
using comp_fun by blast
next
from ‹f∈_› ‹g∈_› ‹converse(f)∈_› ‹converse(g)∈_›
have "(⋀x. x ∈ A' → B' ⟹ converse(g) O x O converse(f) ∈ A → B)"
using bij_is_fun comp_fun by blast
then
have "(λx∈A → B. g O x O f) O (λx∈A' → B'. converse(g) O x O converse(f))
= (λx∈A' → B' . (g O converse(g)) O x O (converse(f) O f))"
using lam_cong comp_assoc comp_lam[of "A' → B'" ] by auto
also
have "... = (λx∈A' → B' . id(B') O x O (id(A')))"
using left_comp_inverse[OF bij_is_inj[OF ‹f∈_›]]
right_comp_inverse[OF bij_is_surj[OF ‹g∈_›]]
by auto
also
have "... = (λx∈A' → B' . x)"
using left_comp_id[OF fun_is_rel] right_comp_id[OF fun_is_rel] lam_cong by auto
also
have "... = id(A'→B')" unfolding id_def by simp
finally
show "(λx∈A -> B. g O x O f) O (λx∈A' -> B'. converse(g) O x O converse(f)) = id(A' -> B')" .
next
from ‹f∈_› ‹g∈_›
have "(⋀x. x ∈ A → B ⟹ g O x O f ∈ A' → B')"
using bij_is_fun comp_fun by blast
then
have "(λx∈A' -> B'. converse(g) O x O converse(f)) O (λx∈A -> B. g O x O f)
= (λx∈A → B . (converse(g) O g) O x O (f O converse(f)))"
using comp_lam comp_assoc by auto
also
have "... = (λx∈A → B . id(B) O x O (id(A)))"
using
right_comp_inverse[OF bij_is_surj[OF ‹f∈_›]]
left_comp_inverse[OF bij_is_inj[OF ‹g∈_›]] lam_cong
by auto
also
have "... = (λx∈A → B . x)"
using left_comp_id[OF fun_is_rel] right_comp_id[OF fun_is_rel] lam_cong by auto
also
have "... = id(A→B)" unfolding id_def by simp
finally
show "(λx∈A' → B'. converse(g) O x O converse(f)) O (λx∈A -> B. g O x O f) = id(A -> B)" .
qed
qed
lemma curry_eqpoll:
fixes d ν1 ν2 κ
shows "ν1 → ν2 → κ ≈ ν1 × ν2 → κ"
unfolding eqpoll_def
proof (intro exI, rule lam_bijective,
rule_tac [1-2] lam_type, rule_tac [2] lam_type)
fix f z
assume "f : ν1 → ν2 → κ" "z ∈ ν1 × ν2"
then
show "f`fst(z)`snd(z) ∈ κ"
by simp
next
fix f x y
assume "f : ν1 × ν2 → κ" "x∈ν1" "y∈ν2"
then
show "f`⟨x,y⟩ ∈ κ" by simp
next
fix f
assume "f : ν1 × ν2 → κ"
then
show "(λx∈ν1 × ν2. (λx∈ν1. λxa∈ν2. f ` ⟨x, xa⟩) ` fst(x) ` snd(x)) = f"
by (auto intro:fun_extension)
qed simp
lemma Pow_eqpoll_function_space:
fixes d X
notes bool_of_o_def [simp]
defines [simp]:"d(A) ≡ (λx∈X. bool_of_o(x∈A))"
shows "Pow(X) ≈ X → 2"
unfolding eqpoll_def
proof (intro exI, rule lam_bijective)
fix A
assume "A∈Pow(X)"
then
show "d(A) : X → 2"
using lam_type[of _ "λx. bool_of_o(x∈A)" "λ_. 2"]
by force
from ‹A∈Pow(X)›
show "{y∈X. d(A)`y = 1} = A"
by (auto)
next
fix f
assume "f: X→2"
then
show "d({y ∈ X . f ` y = 1}) = f"
using apply_type[OF ‹f: X→2›]
by (force intro:fun_extension)
qed blast
lemma cantor_inj: "f ∉ inj(Pow(A),A)"
using inj_imp_surj[OF _ Pow_bottom] cantor_surj by blast
definition
cexp :: "[i,i] ⇒ i" ("_⇗↑_⇖" [76,1] 75) where
"κ⇗↑ν⇖ ≡ |ν → κ|"
lemma Card_cexp: "Card(κ⇗↑ν⇖)"
unfolding cexp_def Card_cardinal by simp
lemma eq_csucc_ord:
"Ord(i) ⟹ i⇧+ = |i|⇧+"
using Card_lt_iff Least_cong unfolding csucc_def by auto
text‹I thank Miguel Pagano for this proof.›
lemma lesspoll_csucc:
assumes "Ord(κ)"
shows "d ≺ κ⇧+ ⟷ d ≲ κ"
proof
assume "d ≺ κ⇧+"
moreover
note Card_is_Ord ‹Ord(κ)›
moreover from calculation
have "κ < κ⇧+" "Card(κ⇧+)"
using Ord_cardinal_eqpoll csucc_basic by simp_all
moreover from calculation
have "d ≺ |κ|⇧+" "Card(|κ|)" "d ≈ |d|"
using eq_csucc_ord[of κ] lesspoll_imp_eqpoll eqpoll_sym by simp_all
moreover from calculation
have "|d| < |κ|⇧+"
using lesspoll_cardinal_lt csucc_basic by simp
moreover from calculation
have "|d| ≲ |κ|"
using Card_lt_csucc_iff le_imp_lepoll by simp
moreover from calculation
have "|d| ≲ κ"
using lepoll_eq_trans Ord_cardinal_eqpoll by simp
ultimately
show "d ≲ κ"
using eq_lepoll_trans by simp
next
from ‹Ord(κ)›
have "κ < κ⇧+" "Card(κ⇧+)"
using csucc_basic by simp_all
moreover
assume "d ≲ κ"
ultimately
have "d ≲ κ⇧+"
using le_imp_lepoll leI lepoll_trans by simp
moreover
from ‹d ≲ κ› ‹Ord(κ)›
have "κ⇧+ ≲ κ" if "d ≈ κ⇧+"
using eqpoll_sym[OF that] eq_lepoll_trans[OF _ ‹d≲κ›] by simp
moreover from calculation ‹Card(_)›
have "¬ d ≈ κ⇧+"
using lesspoll_irrefl lesspoll_trans1 lt_Card_imp_lesspoll[OF _ ‹κ <_›]
by auto
ultimately
show "d ≺ κ⇧+"
unfolding lesspoll_def by simp
qed
abbreviation
Infinite :: "i⇒o" where
"Infinite(X) ≡ ¬ Finite(X)"
lemma Infinite_not_empty: "Infinite(X) ⟹ X ≠ 0"
using empty_lepollI by auto
lemma Infinite_imp_nats_lepoll:
assumes "Infinite(X)" "n ∈ ω"
shows "n ≲ X"
using ‹n ∈ ω›
proof (induct)
case 0
then
show ?case using empty_lepollI by simp
next
case (succ x)
show ?case
proof -
from ‹Infinite(X)› and ‹x ∈ ω›
have "¬ (x ≈ X)"
using eqpoll_sym unfolding Finite_def by auto
with ‹x ≲ X›
obtain f where "f ∈ inj(x,X)" "f ∉ surj(x,X)"
unfolding bij_def eqpoll_def by auto
moreover from this
obtain b where "b ∈ X" "∀a∈x. f`a ≠ b"
using inj_is_fun unfolding surj_def by auto
ultimately
have "f ∈ inj(x,X-{b})"
unfolding inj_def by (auto intro:Pi_type)
then
have "cons(⟨x, b⟩, f) ∈ inj(succ(x), cons(b, X - {b}))"
using inj_extend[of f x "X-{b}" x b] unfolding succ_def
by (auto dest:mem_irrefl)
moreover from ‹b∈X›
have "cons(b, X - {b}) = X" by auto
ultimately
show "succ(x) ≲ X" by auto
qed
qed
lemma zero_lesspoll: assumes "0<κ" shows "0 ≺ κ"
using assms eqpoll_0_iff[THEN iffD1, of κ] eqpoll_sym
unfolding lesspoll_def lepoll_def
by (auto simp add:inj_def)
lemma lepoll_nat_imp_Infinite: "ω ≲ X ⟹ Infinite(X)"
proof (rule ccontr, simp)
assume "ω ≲ X" "Finite(X)"
moreover from this
obtain n where "X ≈ n" "n ∈ ω"
unfolding Finite_def by auto
moreover from calculation
have "ω ≲ n"
using lepoll_eq_trans by simp
ultimately
show "False"
using lepoll_nat_imp_Finite nat_not_Finite by simp
qed
lemma InfCard_imp_Infinite: "InfCard(κ) ⟹ Infinite(κ)"
using le_imp_lepoll[THEN lepoll_nat_imp_Infinite, of κ]
unfolding InfCard_def by simp
lemma lt_surj_empty_imp_Card:
assumes "Ord(κ)" "⋀α. α < κ ⟹ surj(α,κ) = 0"
shows "Card(κ)"
proof -
{
assume "|κ| < κ"
with assms
have "False"
using LeastI[of "λi. i ≈ κ" κ, OF eqpoll_refl]
Least_le[of "λi. i ≈ κ" "|κ|", OF Ord_cardinal_eqpoll]
unfolding Card_def cardinal_def eqpoll_def bij_def
by simp
}
with assms
show ?thesis
using Ord_cardinal_le[of κ] not_lt_imp_le[of "|κ|" κ] le_anti_sym
unfolding Card_def by auto
qed
subsection‹Morphisms of binary relations›
text‹The main case of interest is in the case of partial orders.›
lemma mono_map_mono:
assumes
"f ∈ mono_map(A,r,B,s)" "B ⊆ C"
shows
"f ∈ mono_map(A,r,C,s)"
unfolding mono_map_def
proof (intro CollectI ballI impI)
from ‹f ∈ mono_map(A,_,B,_)›
have "f: A → B"
using mono_map_is_fun by simp
with ‹B⊆C›
show "f: A → C"
using fun_weaken_type by simp
fix x y
assume "x∈A" "y∈A" "⟨x,y⟩ ∈ r"
moreover from this and ‹f: A → B›
have "f`x ∈ B" "f`y ∈ B"
using apply_type by simp_all
moreover
note ‹f ∈ mono_map(_,r,_,s)›
ultimately
show "⟨f ` x, f ` y⟩ ∈ s"
unfolding mono_map_def by blast
qed
lemma ordertype_zero_imp_zero: "ordertype(A,r) = 0 ⟹ A = 0"
using ordermap_type[of A r]
by (cases "A=0") auto
lemma mono_map_increasing:
"j∈mono_map(A,r,B,s) ⟹ a∈A ⟹ c∈A ⟹ ⟨a,c⟩∈r ⟹ ⟨j`a,j`c⟩∈s"
unfolding mono_map_def by simp
lemma linear_mono_map_reflects:
assumes
"linear(α,r)" "trans[β](s)" "irrefl(β,s)" "f∈mono_map(α,r,β,s)"
"x∈α" "y∈α" "⟨f`x,f`y⟩∈s"
shows
"⟨x,y⟩∈r"
proof -
from ‹f∈mono_map(_,_,_,_)›
have preserves:"x∈α ⟹ y∈α ⟹ ⟨x,y⟩∈r ⟹ ⟨f`x,f`y⟩∈s" for x y
unfolding mono_map_def by blast
{
assume "⟨x, y⟩ ∉ r" "x∈α" "y∈α"
moreover
note ‹⟨f`x,f`y⟩∈s› and ‹linear(α,r)›
moreover from calculation
have "y = x ∨ ⟨y,x⟩∈r"
unfolding linear_def by blast
moreover
note preserves [of y x]
ultimately
have "y = x ∨ ⟨f`y, f`x⟩∈ s" by blast
moreover from ‹f∈mono_map(_,_,β,_)› ‹x∈α› ‹y∈α›
have "f`x∈β" "f`y∈β"
using apply_type[OF mono_map_is_fun] by simp_all
moreover
note ‹⟨f`x,f`y⟩∈s› ‹trans[β](s)› ‹irrefl(β,s)›
ultimately
have "False"
using trans_onD[of β s "f`x" "f`y" "f`x"] irreflE by blast
}
with assms
show "⟨x,y⟩∈r" by blast
qed
lemma irrefl_Memrel: "irrefl(x, Memrel(x))"
unfolding irrefl_def using mem_irrefl by auto
lemmas Memrel_mono_map_reflects = linear_mono_map_reflects
[OF well_ord_is_linear[OF well_ord_Memrel] well_ord_is_trans_on[OF well_ord_Memrel]
irrefl_Memrel]
lemma mono_map_is_inj':
"⟦ linear(A,r); irrefl(B,s); f ∈ mono_map(A,r,B,s) ⟧ ⟹ f ∈ inj(A,B)"
unfolding irrefl_def mono_map_def inj_def using linearE
by (clarify, rename_tac x w)
(erule_tac x=w and y=x in linearE, assumption+, (force intro: apply_type)+)
lemma mono_map_imp_ord_iso_image:
assumes
"linear(α,r)" "trans[β](s)" "irrefl(β,s)" "f∈mono_map(α,r,β,s)"
shows
"f ∈ ord_iso(α,r,f``α,s)"
unfolding ord_iso_def
proof (intro CollectI ballI iffI)
from assms
have "f ∈ inj(α,β)"
using mono_map_is_inj' by blast
moreover from ‹f ∈ mono_map(_,_,_,_)›
have "f ∈ surj(α, f``α)"
unfolding mono_map_def using surj_image by auto
ultimately
show "f ∈ bij(α, f``α)"
unfolding bij_def using inj_is_fun inj_to_Image by simp
from ‹f∈mono_map(_,_,_,_)›
show "x∈α ⟹ y∈α ⟹ ⟨x,y⟩∈r ⟹ ⟨f`x,f`y⟩∈s" for x y
unfolding mono_map_def by blast
with assms
show "⟨f`x,f`y⟩∈s ⟹ x∈α ⟹ y∈α ⟹ ⟨x,y⟩∈r" for x y
using linear_mono_map_reflects
by blast
qed
text‹We introduce the following notation for strictly increasing maps
between ordinals.›
abbreviation
mono_map_Memrel :: "[i,i] ⇒ i" (infixr ‹→⇩<› 60) where
"α →⇩< β ≡ mono_map(α,Memrel(α),β,Memrel(β))"
lemma mono_map_imp_ord_iso_Memrel:
assumes
"Ord(α)" "Ord(β)" "f:α →⇩< β"
shows
"f ∈ ord_iso(α,Memrel(α),f``α,Memrel(β))"
using assms mono_map_imp_ord_iso_image[OF well_ord_is_linear[OF well_ord_Memrel]
well_ord_is_trans_on[OF well_ord_Memrel] irrefl_Memrel] by blast
lemma mono_map_ordertype_image':
assumes
"X⊆α" "Ord(α)" "Ord(β)" "f ∈ mono_map(X,Memrel(α),β,Memrel(β))"
shows
"ordertype(f``X,Memrel(β)) = ordertype(X,Memrel(α))"
using assms mono_map_is_fun[of f X _ β] ordertype_eq
mono_map_imp_ord_iso_image[OF well_ord_is_linear[OF well_ord_Memrel, THEN linear_subset]
well_ord_is_trans_on[OF well_ord_Memrel] irrefl_Memrel, of α X β f]
well_ord_subset[OF well_ord_Memrel] Image_sub_codomain[of f X β X] by auto
lemma mono_map_ordertype_image:
assumes
"Ord(α)" "Ord(β)" "f:α →⇩< β"
shows
"ordertype(f``α,Memrel(β)) = α"
using assms mono_map_is_fun ordertype_Memrel ordertype_eq[of f α "Memrel(α)"]
mono_map_imp_ord_iso_Memrel well_ord_subset[OF well_ord_Memrel] Image_sub_codomain[of _ α]
by auto
lemma apply_in_image: "f:A→B ⟹ a∈A ⟹ f`a ∈ f``A"
using range_eq_image apply_rangeI[of f] by simp
lemma Image_subset_Ord_imp_lt:
assumes
"Ord(α)" "h``A ⊆ α" "x∈domain(h)" "x∈A" "function(h)"
shows
"h`x < α"
using assms
unfolding domain_def using imageI ltI function_apply_equality by auto
lemma ordermap_le_arg:
assumes
"X⊆β" "x∈X" "Ord(β)"
shows
"x∈X ⟹ ordermap(X,Memrel(β))`x≤x"
proof (induct rule:Ord_induct[OF subsetD, OF assms])
case (1 x)
have "wf[X](Memrel(β))"
using wf_imp_wf_on[OF wf_Memrel] .
with 1
have "ordermap(X,Memrel(β))`x = {ordermap(X,Memrel(β))`y . y∈{y∈X . y∈x ∧ y∈β}}"
using ordermap_unfold Ord_trans[of _ x β] by auto
also from assms
have "... = {ordermap(X,Memrel(β))`y . y∈{y∈X . y∈x}}"
using Ord_trans[of _ x β] Ord_in_Ord by blast
finally
have ordm:"ordermap(X,Memrel(β))`x = {ordermap(X,Memrel(β))`y . y∈{y∈X . y∈x}}" .
from 1
have "y∈x ⟹ y∈X ⟹ ordermap(X,Memrel(β))`y ≤ y" for y by simp
with ‹x∈β› and ‹Ord(β)›
have "y∈x ⟹ y∈X ⟹ ordermap(X,Memrel(β))`y ∈ x" for y
using ltI[OF _ Ord_in_Ord[of β x]] lt_trans1 ltD by blast
with ordm
have "ordermap(X,Memrel(β))`x ⊆ x" by auto
with ‹x∈X› assms
show ?case
using subset_imp_le Ord_in_Ord[of β x] Ord_ordermap
well_ord_subset[OF well_ord_Memrel, of β] by force
qed
lemma subset_imp_ordertype_le:
assumes
"X⊆β" "Ord(β)"
shows
"ordertype(X,Memrel(β))≤β"
proof -
{
fix x
assume "x∈X"
with assms
have "ordermap(X,Memrel(β))`x ≤ x"
using ordermap_le_arg by simp
with ‹x∈X› and assms
have "ordermap(X,Memrel(β))`x ∈ β" (is "?y ∈ _")
using ltD[of ?y "succ(x)"] Ord_trans[of ?y x β] by auto
}
then
have "ordertype(X, Memrel(β)) ⊆ β"
using ordertype_unfold[of X] by auto
with assms
show ?thesis
using subset_imp_le Ord_ordertype[OF well_ord_subset, OF well_ord_Memrel] by simp
qed
lemma mono_map_imp_le:
assumes
"f∈mono_map(α, Memrel(α),β, Memrel(β))" "Ord(α)" "Ord(β)"
shows
"α≤β"
proof -
from assms
have "f ∈ ⟨α, Memrel(α)⟩ ≅ ⟨f``α, Memrel(β)⟩"
using mono_map_imp_ord_iso_Memrel by simp
then
have "converse(f) ∈ ⟨f``α, Memrel(β)⟩ ≅ ⟨α, Memrel(α)⟩"
using ord_iso_sym by simp
with ‹Ord(α)›
have "α = ordertype(f``α,Memrel(β))"
using ordertype_eq well_ord_Memrel ordertype_Memrel by auto
also from assms
have "ordertype(f``α,Memrel(β)) ≤ β"
using subset_imp_ordertype_le mono_map_is_fun[of f] Image_sub_codomain[of f] by force
finally
show ?thesis .
qed
lemmas Memrel_mono_map_is_inj = mono_map_is_inj
[OF well_ord_is_linear[OF well_ord_Memrel]
wf_imp_wf_on[OF wf_Memrel]]
lemma mono_mapI:
assumes "f: A→B" "⋀x y. x∈A ⟹ y∈A ⟹ ⟨x,y⟩∈r ⟹ ⟨f`x,f`y⟩∈s"
shows "f ∈ mono_map(A,r,B,s)"
unfolding mono_map_def using assms by simp
lemmas mono_mapD = mono_map_is_fun mono_map_increasing
bundle mono_map_rules = mono_mapI[intro!] mono_map_is_fun[dest] mono_mapD[dest]
lemma nats_le_InfCard:
assumes "n ∈ ω" "InfCard(κ)"
shows "n ≤ κ"
using assms Ord_is_Transset
le_trans[of n ω κ, OF le_subset_iff[THEN iffD2]]
unfolding InfCard_def Transset_def by simp
lemma nat_into_InfCard:
assumes "n ∈ ω" "InfCard(κ)"
shows "n ∈ κ"
using assms le_imp_subset[of ω κ]
unfolding InfCard_def by auto
subsection‹Alephs are infinite cardinals›
lemma Aleph_zero_eq_nat: "ℵ⇘0⇙ = ω"
unfolding Aleph_def by simp
lemma InfCard_Aleph:
notes Aleph_zero_eq_nat[simp]
assumes "Ord(α)"
shows "InfCard(ℵ⇘α⇙)"
proof -
have "¬ (ℵ⇘α⇙ ∈ ω)"
proof (cases "α=0")
case True
then show ?thesis using mem_irrefl by auto
next
case False
with ‹Ord(α)›
have "ω ∈ ℵ⇘α⇙" using Ord_0_lt[of α] ltD by (auto dest:Aleph_increasing)
then show ?thesis using foundation by blast
qed
with ‹Ord(α)›
have "¬ (|ℵ⇘α⇙| ∈ ω)"
using Card_cardinal_eq by auto
then
have "¬ Finite(ℵ⇘α⇙)" by auto
with ‹Ord(α)›
show ?thesis
using Inf_Card_is_InfCard by simp
qed
text‹Most properties of cardinals depend on $\AC$, even for the countable.
Here we just state the definition of this concept, and most proofs will
appear after assuming Choice.›
definition
countable :: "i⇒o" where
"countable(X) ≡ X ≲ ω"
lemma countableI[intro]: "X ≲ ω ⟹ countable(X)"
unfolding countable_def by simp
lemma countableD[dest]: "countable(X) ⟹ X ≲ ω"
unfolding countable_def by simp
text‹A ∗‹delta system› is family of sets with a common pairwise
intersection. We will work with this notion in Section~\ref{sec:dsl},
but we state the definition here in order to have it available in a
choiceless context.›
definition
delta_system :: "i ⇒ o" where
"delta_system(D) ≡ ∃r. ∀A∈D. ∀B∈D. A ≠ B ⟶ A ∩ B = r"
lemma delta_systemI[intro]:
assumes "∀A∈D. ∀B∈D. A ≠ B ⟶ A ∩ B = r"
shows "delta_system(D)"
using assms unfolding delta_system_def by simp
lemma delta_systemD[dest]:
"delta_system(D) ⟹ ∃r. ∀A∈D. ∀B∈D. A ≠ B ⟶ A ∩ B = r"
unfolding delta_system_def by simp
text‹Hence, pairwise intersections equal the intersection of the whole
family.›
lemma delta_system_root_eq_Inter:
assumes "delta_system(D)"
shows "∀A∈D. ∀B∈D. A ≠ B ⟶ A ∩ B = ⋂D"
proof (clarify, intro equalityI, auto)
fix A' B' x C
assume hyp:"A'∈D" "B'∈ D" "A'≠B'" "x∈A'" "x∈B'" "C∈D"
with assms
obtain r where delta:"∀A∈D. ∀B∈D. A ≠ B ⟶ A ∩ B = r"
by auto
show "x ∈ C"
proof (cases "C=A'")
case True
with hyp and assms
show ?thesis by simp
next
case False
moreover
note hyp
moreover from calculation and delta
have "r = C ∩ A'" "A' ∩ B' = r" "x∈r" by auto
ultimately
show ?thesis by simp
qed
qed
lemmas Limit_Aleph = InfCard_Aleph[THEN InfCard_is_Limit]
lemmas Aleph_cont = Normal_imp_cont[OF Normal_Aleph]
lemmas Aleph_sup = Normal_Union[OF _ _ Normal_Aleph]
bundle Ord_dests = Limit_is_Ord[dest] Card_is_Ord[dest]
bundle Aleph_dests = Aleph_cont[dest] Aleph_sup[dest]
bundle Aleph_intros = Aleph_increasing[intro!]
bundle Aleph_mem_dests = Aleph_increasing[OF ltI, THEN ltD, dest]
subsection‹Transfinite recursive constructions›
definition
rec_constr :: "[i,i] ⇒ i" where
"rec_constr(f,α) ≡ transrec(α,λa g. f`(g``a))"
text‹The function \<^term>‹rec_constr› allows to perform ∗‹recursive
constructions›: given a choice function on the powerset of some
set, a transfinite sequence is created by successively choosing
some new element.
The next result explains its use.›
lemma rec_constr_unfold: "rec_constr(f,α) = f`({rec_constr(f,β). β∈α})"
using def_transrec[OF rec_constr_def, of f α] image_lam by simp
lemma rec_constr_type: assumes "f:Pow(G)→ G" "Ord(α)"
shows "rec_constr(f,α) ∈ G"
using assms(2,1)
by (induct rule:trans_induct)
(subst rec_constr_unfold, rule apply_type[of f "Pow(G)" "λ_. G"], auto)
end