Theory Cardinal
section‹Cardinal Numbers Without the Axiom of Choice›
theory Cardinal imports OrderType Finite Nat Sum begin
definition
Least :: "(i⇒o) ⇒ i" (binder ‹μ › 10) where
"Least(P) ≡ THE i. Ord(i) ∧ P(i) ∧ (∀j. j<i ⟶ ¬P(j))"
definition
eqpoll :: "[i,i] ⇒ o" (infixl ‹≈› 50) where
"A ≈ B ≡ ∃f. f ∈ bij(A,B)"
definition
lepoll :: "[i,i] ⇒ o" (infixl ‹≲› 50) where
"A ≲ B ≡ ∃f. f ∈ inj(A,B)"
definition
lesspoll :: "[i,i] ⇒ o" (infixl ‹≺› 50) where
"A ≺ B ≡ A ≲ B ∧ ¬(A ≈ B)"
definition
cardinal :: "i⇒i" (‹|_|›) where
"|A| ≡ (μ i. i ≈ A)"
definition
Finite :: "i⇒o" where
"Finite(A) ≡ ∃n∈nat. A ≈ n"
definition
Card :: "i⇒o" where
"Card(i) ≡ (i = |i|)"
subsection‹The Schroeder-Bernstein Theorem›
text‹See Davey and Priestly, page 106›
lemma decomp_bnd_mono: "bnd_mono(X, λW. X - g``(Y - f``W))"
by (rule bnd_monoI, blast+)
lemma Banach_last_equation:
"g ∈ Y->X
⟹ g``(Y - f`` lfp(X, λW. X - g``(Y - f``W))) =
X - lfp(X, λW. X - g``(Y - f``W))"
apply (rule_tac P = "λu. v = X-u" for v
in decomp_bnd_mono [THEN lfp_unfold, THEN ssubst])
apply (simp add: double_complement fun_is_rel [THEN image_subset])
done
lemma decomposition:
"⟦f ∈ X->Y; g ∈ Y->X⟧ ⟹
∃XA XB YA YB. (XA ∩ XB = 0) ∧ (XA ∪ XB = X) ∧
(YA ∩ YB = 0) ∧ (YA ∪ YB = Y) ∧
f``XA=YA ∧ g``YB=XB"
apply (intro exI conjI)
apply (rule_tac [6] Banach_last_equation)
apply (rule_tac [5] refl)
apply (assumption |
rule Diff_disjoint Diff_partition fun_is_rel image_subset lfp_subset)+
done
lemma schroeder_bernstein:
"⟦f ∈ inj(X,Y); g ∈ inj(Y,X)⟧ ⟹ ∃h. h ∈ bij(X,Y)"
apply (insert decomposition [of f X Y g])
apply (simp add: inj_is_fun)
apply (blast intro!: restrict_bij bij_disjoint_Un intro: bij_converse_bij)
done
lemma bij_imp_eqpoll: "f ∈ bij(A,B) ⟹ A ≈ B"
unfolding eqpoll_def
apply (erule exI)
done
lemmas eqpoll_refl = id_bij [THEN bij_imp_eqpoll, simp]
lemma eqpoll_sym: "X ≈ Y ⟹ Y ≈ X"
unfolding eqpoll_def
apply (blast intro: bij_converse_bij)
done
lemma eqpoll_trans [trans]:
"⟦X ≈ Y; Y ≈ Z⟧ ⟹ X ≈ Z"
unfolding eqpoll_def
apply (blast intro: comp_bij)
done
lemma subset_imp_lepoll: "X<=Y ⟹ X ≲ Y"
unfolding lepoll_def
apply (rule exI)
apply (erule id_subset_inj)
done
lemmas lepoll_refl = subset_refl [THEN subset_imp_lepoll, simp]
lemmas le_imp_lepoll = le_imp_subset [THEN subset_imp_lepoll]
lemma eqpoll_imp_lepoll: "X ≈ Y ⟹ X ≲ Y"
by (unfold eqpoll_def bij_def lepoll_def, blast)
lemma lepoll_trans [trans]: "⟦X ≲ Y; Y ≲ Z⟧ ⟹ X ≲ Z"
unfolding lepoll_def
apply (blast intro: comp_inj)
done
lemma eq_lepoll_trans [trans]: "⟦X ≈ Y; Y ≲ Z⟧ ⟹ X ≲ Z"
by (blast intro: eqpoll_imp_lepoll lepoll_trans)
lemma lepoll_eq_trans [trans]: "⟦X ≲ Y; Y ≈ Z⟧ ⟹ X ≲ Z"
by (blast intro: eqpoll_imp_lepoll lepoll_trans)
lemma eqpollI: "⟦X ≲ Y; Y ≲ X⟧ ⟹ X ≈ Y"
unfolding lepoll_def eqpoll_def
apply (elim exE)
apply (rule schroeder_bernstein, assumption+)
done
lemma eqpollE:
"⟦X ≈ Y; ⟦X ≲ Y; Y ≲ X⟧ ⟹ P⟧ ⟹ P"
by (blast intro: eqpoll_imp_lepoll eqpoll_sym)
lemma eqpoll_iff: "X ≈ Y ⟷ X ≲ Y ∧ Y ≲ X"
by (blast intro: eqpollI elim!: eqpollE)
lemma lepoll_0_is_0: "A ≲ 0 ⟹ A = 0"
unfolding lepoll_def inj_def
apply (blast dest: apply_type)
done
lemmas empty_lepollI = empty_subsetI [THEN subset_imp_lepoll]
lemma lepoll_0_iff: "A ≲ 0 ⟷ A=0"
by (blast intro: lepoll_0_is_0 lepoll_refl)
lemma Un_lepoll_Un:
"⟦A ≲ B; C ≲ D; B ∩ D = 0⟧ ⟹ A ∪ C ≲ B ∪ D"
unfolding lepoll_def
apply (blast intro: inj_disjoint_Un)
done
lemmas eqpoll_0_is_0 = eqpoll_imp_lepoll [THEN lepoll_0_is_0]
lemma eqpoll_0_iff: "A ≈ 0 ⟷ A=0"
by (blast intro: eqpoll_0_is_0 eqpoll_refl)
lemma eqpoll_disjoint_Un:
"⟦A ≈ B; C ≈ D; A ∩ C = 0; B ∩ D = 0⟧
⟹ A ∪ C ≈ B ∪ D"
unfolding eqpoll_def
apply (blast intro: bij_disjoint_Un)
done
subsection‹lesspoll: contributions by Krzysztof Grabczewski›
lemma lesspoll_not_refl: "¬ (i ≺ i)"
by (simp add: lesspoll_def)
lemma lesspoll_irrefl [elim!]: "i ≺ i ⟹ P"
by (simp add: lesspoll_def)
lemma lesspoll_imp_lepoll: "A ≺ B ⟹ A ≲ B"
by (unfold lesspoll_def, blast)
lemma lepoll_well_ord: "⟦A ≲ B; well_ord(B,r)⟧ ⟹ ∃s. well_ord(A,s)"
unfolding lepoll_def
apply (blast intro: well_ord_rvimage)
done
lemma lepoll_iff_leqpoll: "A ≲ B ⟷ A ≺ B | A ≈ B"
unfolding lesspoll_def
apply (blast intro!: eqpollI elim!: eqpollE)
done
lemma inj_not_surj_succ:
assumes fi: "f ∈ inj(A, succ(m))" and fns: "f ∉ surj(A, succ(m))"
shows "∃f. f ∈ inj(A,m)"
proof -
from fi [THEN inj_is_fun] fns
obtain y where y: "y ∈ succ(m)" "⋀x. x∈A ⟹ f ` x ≠ y"
by (auto simp add: surj_def)
show ?thesis
proof
show "(λz∈A. if f`z = m then y else f`z) ∈ inj(A, m)" using y fi
by (simp add: inj_def)
(auto intro!: if_type [THEN lam_type] intro: Pi_type dest: apply_funtype)
qed
qed
lemma lesspoll_trans [trans]:
"⟦X ≺ Y; Y ≺ Z⟧ ⟹ X ≺ Z"
unfolding lesspoll_def
apply (blast elim!: eqpollE intro: eqpollI lepoll_trans)
done
lemma lesspoll_trans1 [trans]:
"⟦X ≲ Y; Y ≺ Z⟧ ⟹ X ≺ Z"
unfolding lesspoll_def
apply (blast elim!: eqpollE intro: eqpollI lepoll_trans)
done
lemma lesspoll_trans2 [trans]:
"⟦X ≺ Y; Y ≲ Z⟧ ⟹ X ≺ Z"
unfolding lesspoll_def
apply (blast elim!: eqpollE intro: eqpollI lepoll_trans)
done
lemma eq_lesspoll_trans [trans]:
"⟦X ≈ Y; Y ≺ Z⟧ ⟹ X ≺ Z"
by (blast intro: eqpoll_imp_lepoll lesspoll_trans1)
lemma lesspoll_eq_trans [trans]:
"⟦X ≺ Y; Y ≈ Z⟧ ⟹ X ≺ Z"
by (blast intro: eqpoll_imp_lepoll lesspoll_trans2)
lemma Least_equality:
"⟦P(i); Ord(i); ⋀x. x<i ⟹ ¬P(x)⟧ ⟹ (μ x. P(x)) = i"
unfolding Least_def
apply (rule the_equality, blast)
apply (elim conjE)
apply (erule Ord_linear_lt, assumption, blast+)
done
lemma LeastI:
assumes P: "P(i)" and i: "Ord(i)" shows "P(μ x. P(x))"
proof -
{ from i have "P(i) ⟹ P(μ x. P(x))"
proof (induct i rule: trans_induct)
case (step i)
show ?case
proof (cases "P(μ a. P(a))")
case True thus ?thesis .
next
case False
hence "⋀x. x ∈ i ⟹ ¬P(x)" using step
by blast
hence "(μ a. P(a)) = i" using step
by (blast intro: Least_equality ltD)
thus ?thesis using step.prems
by simp
qed
qed
}
thus ?thesis using P .
qed
text‹The proof is almost identical to the one above!›
lemma Least_le:
assumes P: "P(i)" and i: "Ord(i)" shows "(μ x. P(x)) ≤ i"
proof -
{ from i have "P(i) ⟹ (μ x. P(x)) ≤ i"
proof (induct i rule: trans_induct)
case (step i)
show ?case
proof (cases "(μ a. P(a)) ≤ i")
case True thus ?thesis .
next
case False
hence "⋀x. x ∈ i ⟹ ¬ (μ a. P(a)) ≤ i" using step
by blast
hence "(μ a. P(a)) = i" using step
by (blast elim: ltE intro: ltI Least_equality lt_trans1)
thus ?thesis using step
by simp
qed
qed
}
thus ?thesis using P .
qed
lemma less_LeastE: "⟦P(i); i < (μ x. P(x))⟧ ⟹ Q"
apply (rule Least_le [THEN [2] lt_trans2, THEN lt_irrefl], assumption+)
apply (simp add: lt_Ord)
done
lemma LeastI2:
"⟦P(i); Ord(i); ⋀j. P(j) ⟹ Q(j)⟧ ⟹ Q(μ j. P(j))"
by (blast intro: LeastI )
lemma Least_0:
"⟦¬ (∃i. Ord(i) ∧ P(i))⟧ ⟹ (μ x. P(x)) = 0"
unfolding Least_def
apply (rule the_0, blast)
done
lemma Ord_Least [intro,simp,TC]: "Ord(μ x. P(x))"
proof (cases "∃i. Ord(i) ∧ P(i)")
case True
then obtain i where "P(i)" "Ord(i)" by auto
hence " (μ x. P(x)) ≤ i" by (rule Least_le)
thus ?thesis
by (elim ltE)
next
case False
hence "(μ x. P(x)) = 0" by (rule Least_0)
thus ?thesis
by auto
qed
subsection‹Basic Properties of Cardinals›
lemma Least_cong: "(⋀y. P(y) ⟷ Q(y)) ⟹ (μ x. P(x)) = (μ x. Q(x))"
by simp
lemma cardinal_cong: "X ≈ Y ⟹ |X| = |Y|"
unfolding eqpoll_def cardinal_def
apply (rule Least_cong)
apply (blast intro: comp_bij bij_converse_bij)
done
lemma well_ord_cardinal_eqpoll:
assumes r: "well_ord(A,r)" shows "|A| ≈ A"
proof (unfold cardinal_def)
show "(μ i. i ≈ A) ≈ A"
by (best intro: LeastI Ord_ordertype ordermap_bij bij_converse_bij bij_imp_eqpoll r)
qed
lemmas Ord_cardinal_eqpoll = well_ord_Memrel [THEN well_ord_cardinal_eqpoll]
lemma Ord_cardinal_idem: "Ord(A) ⟹ ||A|| = |A|"
by (rule Ord_cardinal_eqpoll [THEN cardinal_cong])
lemma well_ord_cardinal_eqE:
assumes woX: "well_ord(X,r)" and woY: "well_ord(Y,s)" and eq: "|X| = |Y|"
shows "X ≈ Y"
proof -
have "X ≈ |X|" by (blast intro: well_ord_cardinal_eqpoll [OF woX] eqpoll_sym)
also have "... = |Y|" by (rule eq)
also have "... ≈ Y" by (rule well_ord_cardinal_eqpoll [OF woY])
finally show ?thesis .
qed
lemma well_ord_cardinal_eqpoll_iff:
"⟦well_ord(X,r); well_ord(Y,s)⟧ ⟹ |X| = |Y| ⟷ X ≈ Y"
by (blast intro: cardinal_cong well_ord_cardinal_eqE)
lemma Ord_cardinal_le: "Ord(i) ⟹ |i| ≤ i"
unfolding cardinal_def
apply (erule eqpoll_refl [THEN Least_le])
done
lemma Card_cardinal_eq: "Card(K) ⟹ |K| = K"
unfolding Card_def
apply (erule sym)
done
lemma CardI: "⟦Ord(i); ⋀j. j<i ⟹ ¬(j ≈ i)⟧ ⟹ Card(i)"
unfolding Card_def cardinal_def
apply (subst Least_equality)
apply (blast intro: eqpoll_refl)+
done
lemma Card_is_Ord: "Card(i) ⟹ Ord(i)"
unfolding Card_def cardinal_def
apply (erule ssubst)
apply (rule Ord_Least)
done
lemma Card_cardinal_le: "Card(K) ⟹ K ≤ |K|"
apply (simp (no_asm_simp) add: Card_is_Ord Card_cardinal_eq)
done
lemma Ord_cardinal [simp,intro!]: "Ord(|A|)"
unfolding cardinal_def
apply (rule Ord_Least)
done
text‹The cardinals are the initial ordinals.›
lemma Card_iff_initial: "Card(K) ⟷ Ord(K) ∧ (∀j. j<K ⟶ ¬ j ≈ K)"
proof -
{ fix j
assume K: "Card(K)" "j ≈ K"
assume "j < K"
also have "... = (μ i. i ≈ K)" using K
by (simp add: Card_def cardinal_def)
finally have "j < (μ i. i ≈ K)" .
hence "False" using K
by (best dest: less_LeastE)
}
then show ?thesis
by (blast intro: CardI Card_is_Ord)
qed
lemma lt_Card_imp_lesspoll: "⟦Card(a); i<a⟧ ⟹ i ≺ a"
unfolding lesspoll_def
apply (drule Card_iff_initial [THEN iffD1])
apply (blast intro!: leI [THEN le_imp_lepoll])
done
lemma Card_0: "Card(0)"
apply (rule Ord_0 [THEN CardI])
apply (blast elim!: ltE)
done
lemma Card_Un: "⟦Card(K); Card(L)⟧ ⟹ Card(K ∪ L)"
apply (rule Ord_linear_le [of K L])
apply (simp_all add: subset_Un_iff [THEN iffD1] Card_is_Ord le_imp_subset
subset_Un_iff2 [THEN iffD1])
done
lemma Card_cardinal [iff]: "Card(|A|)"
proof (unfold cardinal_def)
show "Card(μ i. i ≈ A)"
proof (cases "∃i. Ord (i) ∧ i ≈ A")
case False thus ?thesis
by (simp add: Least_0 Card_0)
next
case True
then obtain i where i: "Ord(i)" "i ≈ A" by blast
show ?thesis
proof (rule CardI [OF Ord_Least], rule notI)
fix j
assume j: "j < (μ i. i ≈ A)"
assume "j ≈ (μ i. i ≈ A)"
also have "... ≈ A" using i by (auto intro: LeastI)
finally have "j ≈ A" .
thus False
by (rule less_LeastE [OF _ j])
qed
qed
qed
lemma cardinal_eq_lemma:
assumes i:"|i| ≤ j" and j: "j ≤ i" shows "|j| = |i|"
proof (rule eqpollI [THEN cardinal_cong])
show "j ≲ i" by (rule le_imp_lepoll [OF j])
next
have Oi: "Ord(i)" using j by (rule le_Ord2)
hence "i ≈ |i|"
by (blast intro: Ord_cardinal_eqpoll eqpoll_sym)
also have "... ≲ j"
by (blast intro: le_imp_lepoll i)
finally show "i ≲ j" .
qed
lemma cardinal_mono:
assumes ij: "i ≤ j" shows "|i| ≤ |j|"
using Ord_cardinal [of i] Ord_cardinal [of j]
proof (cases rule: Ord_linear_le)
case le thus ?thesis .
next
case ge
have i: "Ord(i)" using ij
by (simp add: lt_Ord)
have ci: "|i| ≤ j"
by (blast intro: Ord_cardinal_le ij le_trans i)
have "|i| = ||i||"
by (auto simp add: Ord_cardinal_idem i)
also have "... = |j|"
by (rule cardinal_eq_lemma [OF ge ci])
finally have "|i| = |j|" .
thus ?thesis by simp
qed
text‹Since we have \<^term>‹|succ(nat)| ≤ |nat|›, the converse of ‹cardinal_mono› fails!›
lemma cardinal_lt_imp_lt: "⟦|i| < |j|; Ord(i); Ord(j)⟧ ⟹ i < j"
apply (rule Ord_linear2 [of i j], assumption+)
apply (erule lt_trans2 [THEN lt_irrefl])
apply (erule cardinal_mono)
done
lemma Card_lt_imp_lt: "⟦|i| < K; Ord(i); Card(K)⟧ ⟹ i < K"
by (simp (no_asm_simp) add: cardinal_lt_imp_lt Card_is_Ord Card_cardinal_eq)
lemma Card_lt_iff: "⟦Ord(i); Card(K)⟧ ⟹ (|i| < K) ⟷ (i < K)"
by (blast intro: Card_lt_imp_lt Ord_cardinal_le [THEN lt_trans1])
lemma Card_le_iff: "⟦Ord(i); Card(K)⟧ ⟹ (K ≤ |i|) ⟷ (K ≤ i)"
by (simp add: Card_lt_iff Card_is_Ord Ord_cardinal not_lt_iff_le [THEN iff_sym])
lemma well_ord_lepoll_imp_cardinal_le:
assumes wB: "well_ord(B,r)" and AB: "A ≲ B"
shows "|A| ≤ |B|"
using Ord_cardinal [of A] Ord_cardinal [of B]
proof (cases rule: Ord_linear_le)
case le thus ?thesis .
next
case ge
from lepoll_well_ord [OF AB wB]
obtain s where s: "well_ord(A, s)" by blast
have "B ≈ |B|" by (blast intro: wB eqpoll_sym well_ord_cardinal_eqpoll)
also have "... ≲ |A|" by (rule le_imp_lepoll [OF ge])
also have "... ≈ A" by (rule well_ord_cardinal_eqpoll [OF s])
finally have "B ≲ A" .
hence "A ≈ B" by (blast intro: eqpollI AB)
hence "|A| = |B|" by (rule cardinal_cong)
thus ?thesis by simp
qed
lemma lepoll_cardinal_le: "⟦A ≲ i; Ord(i)⟧ ⟹ |A| ≤ i"
apply (rule le_trans)
apply (erule well_ord_Memrel [THEN well_ord_lepoll_imp_cardinal_le], assumption)
apply (erule Ord_cardinal_le)
done
lemma lepoll_Ord_imp_eqpoll: "⟦A ≲ i; Ord(i)⟧ ⟹ |A| ≈ A"
by (blast intro: lepoll_cardinal_le well_ord_Memrel well_ord_cardinal_eqpoll dest!: lepoll_well_ord)
lemma lesspoll_imp_eqpoll: "⟦A ≺ i; Ord(i)⟧ ⟹ |A| ≈ A"
unfolding lesspoll_def
apply (blast intro: lepoll_Ord_imp_eqpoll)
done
lemma cardinal_subset_Ord: "⟦A<=i; Ord(i)⟧ ⟹ |A| ⊆ i"
apply (drule subset_imp_lepoll [THEN lepoll_cardinal_le])
apply (auto simp add: lt_def)
apply (blast intro: Ord_trans)
done
subsection‹The finite cardinals›
lemma cons_lepoll_consD:
"⟦cons(u,A) ≲ cons(v,B); u∉A; v∉B⟧ ⟹ A ≲ B"
apply (unfold lepoll_def inj_def, safe)
apply (rule_tac x = "λx∈A. if f`x=v then f`u else f`x" in exI)
apply (rule CollectI)
apply (rule if_type [THEN lam_type])
apply (blast dest: apply_funtype)
apply (blast elim!: mem_irrefl dest: apply_funtype)
apply (simp (no_asm_simp))
apply blast
done
lemma cons_eqpoll_consD: "⟦cons(u,A) ≈ cons(v,B); u∉A; v∉B⟧ ⟹ A ≈ B"
apply (simp add: eqpoll_iff)
apply (blast intro: cons_lepoll_consD)
done
lemma succ_lepoll_succD: "succ(m) ≲ succ(n) ⟹ m ≲ n"
unfolding succ_def
apply (erule cons_lepoll_consD)
apply (rule mem_not_refl)+
done
lemma nat_lepoll_imp_le:
"m ∈ nat ⟹ n ∈ nat ⟹ m ≲ n ⟹ m ≤ n"
proof (induct m arbitrary: n rule: nat_induct)
case 0 thus ?case by (blast intro!: nat_0_le)
next
case (succ m)
show ?case using ‹n ∈ nat›
proof (cases rule: natE)
case 0 thus ?thesis using succ
by (simp add: lepoll_def inj_def)
next
case (succ n') thus ?thesis using succ.hyps ‹ succ(m) ≲ n›
by (blast intro!: succ_leI dest!: succ_lepoll_succD)
qed
qed
lemma nat_eqpoll_iff: "⟦m ∈ nat; n ∈ nat⟧ ⟹ m ≈ n ⟷ m = n"
apply (rule iffI)
apply (blast intro: nat_lepoll_imp_le le_anti_sym elim!: eqpollE)
apply (simp add: eqpoll_refl)
done
lemma nat_into_Card:
assumes n: "n ∈ nat" shows "Card(n)"
proof (unfold Card_def cardinal_def, rule sym)
have "Ord(n)" using n by auto
moreover
{ fix i
assume "i < n" "i ≈ n"
hence False using n
by (auto simp add: lt_nat_in_nat [THEN nat_eqpoll_iff])
}
ultimately show "(μ i. i ≈ n) = n" by (auto intro!: Least_equality)
qed
lemmas cardinal_0 = nat_0I [THEN nat_into_Card, THEN Card_cardinal_eq, iff]
lemmas cardinal_1 = nat_1I [THEN nat_into_Card, THEN Card_cardinal_eq, iff]
lemma succ_lepoll_natE: "⟦succ(n) ≲ n; n ∈ nat⟧ ⟹ P"
by (rule nat_lepoll_imp_le [THEN lt_irrefl], auto)
lemma nat_lepoll_imp_ex_eqpoll_n:
"⟦n ∈ nat; nat ≲ X⟧ ⟹ ∃Y. Y ⊆ X ∧ n ≈ Y"
unfolding lepoll_def eqpoll_def
apply (fast del: subsetI subsetCE
intro!: subset_SIs
dest!: Ord_nat [THEN [2] OrdmemD, THEN [2] restrict_inj]
elim!: restrict_bij
inj_is_fun [THEN fun_is_rel, THEN image_subset])
done
lemma lepoll_succ: "i ≲ succ(i)"
by (blast intro: subset_imp_lepoll)
lemma lepoll_imp_lesspoll_succ:
assumes A: "A ≲ m" and m: "m ∈ nat"
shows "A ≺ succ(m)"
proof -
{ assume "A ≈ succ(m)"
hence "succ(m) ≈ A" by (rule eqpoll_sym)
also have "... ≲ m" by (rule A)
finally have "succ(m) ≲ m" .
hence False by (rule succ_lepoll_natE) (rule m) }
moreover have "A ≲ succ(m)" by (blast intro: lepoll_trans A lepoll_succ)
ultimately show ?thesis by (auto simp add: lesspoll_def)
qed
lemma lesspoll_succ_imp_lepoll:
"⟦A ≺ succ(m); m ∈ nat⟧ ⟹ A ≲ m"
unfolding lesspoll_def lepoll_def eqpoll_def bij_def
apply (auto dest: inj_not_surj_succ)
done
lemma lesspoll_succ_iff: "m ∈ nat ⟹ A ≺ succ(m) ⟷ A ≲ m"
by (blast intro!: lepoll_imp_lesspoll_succ lesspoll_succ_imp_lepoll)
lemma lepoll_succ_disj: "⟦A ≲ succ(m); m ∈ nat⟧ ⟹ A ≲ m | A ≈ succ(m)"
apply (rule disjCI)
apply (rule lesspoll_succ_imp_lepoll)
prefer 2 apply assumption
apply (simp (no_asm_simp) add: lesspoll_def)
done
lemma lesspoll_cardinal_lt: "⟦A ≺ i; Ord(i)⟧ ⟹ |A| < i"
apply (unfold lesspoll_def, clarify)
apply (frule lepoll_cardinal_le, assumption)
apply (blast intro: well_ord_Memrel well_ord_cardinal_eqpoll [THEN eqpoll_sym]
dest: lepoll_well_ord elim!: leE)
done
subsection‹The first infinite cardinal: Omega, or nat›
lemma lt_not_lepoll:
assumes n: "n<i" "n ∈ nat" shows "¬ i ≲ n"
proof -
{ assume i: "i ≲ n"
have "succ(n) ≲ i" using n
by (elim ltE, blast intro: Ord_succ_subsetI [THEN subset_imp_lepoll])
also have "... ≲ n" by (rule i)
finally have "succ(n) ≲ n" .
hence False by (rule succ_lepoll_natE) (rule n) }
thus ?thesis by auto
qed
text‹A slightly weaker version of ‹nat_eqpoll_iff››
lemma Ord_nat_eqpoll_iff:
assumes i: "Ord(i)" and n: "n ∈ nat" shows "i ≈ n ⟷ i=n"
using i nat_into_Ord [OF n]
proof (cases rule: Ord_linear_lt)
case lt
hence "i ∈ nat" by (rule lt_nat_in_nat) (rule n)
thus ?thesis by (simp add: nat_eqpoll_iff n)
next
case eq
thus ?thesis by (simp add: eqpoll_refl)
next
case gt
hence "¬ i ≲ n" using n by (rule lt_not_lepoll)
hence "¬ i ≈ n" using n by (blast intro: eqpoll_imp_lepoll)
moreover have "i ≠ n" using ‹n<i› by auto
ultimately show ?thesis by blast
qed
lemma Card_nat: "Card(nat)"
proof -
{ fix i
assume i: "i < nat" "i ≈ nat"
hence "¬ nat ≲ i"
by (simp add: lt_def lt_not_lepoll)
hence False using i
by (simp add: eqpoll_iff)
}
hence "(μ i. i ≈ nat) = nat" by (blast intro: Least_equality eqpoll_refl)
thus ?thesis
by (auto simp add: Card_def cardinal_def)
qed
lemma nat_le_cardinal: "nat ≤ i ⟹ nat ≤ |i|"
apply (rule Card_nat [THEN Card_cardinal_eq, THEN subst])
apply (erule cardinal_mono)
done
lemma n_lesspoll_nat: "n ∈ nat ⟹ n ≺ nat"
by (blast intro: Ord_nat Card_nat ltI lt_Card_imp_lesspoll)
subsection‹Towards Cardinal Arithmetic›
lemma cons_lepoll_cong:
"⟦A ≲ B; b ∉ B⟧ ⟹ cons(a,A) ≲ cons(b,B)"
apply (unfold lepoll_def, safe)
apply (rule_tac x = "λy∈cons (a,A) . if y=a then b else f`y" in exI)
apply (rule_tac d = "λz. if z ∈ B then converse (f) `z else a" in lam_injective)
apply (safe elim!: consE')
apply simp_all
apply (blast intro: inj_is_fun [THEN apply_type])+
done
lemma cons_eqpoll_cong:
"⟦A ≈ B; a ∉ A; b ∉ B⟧ ⟹ cons(a,A) ≈ cons(b,B)"
by (simp add: eqpoll_iff cons_lepoll_cong)
lemma cons_lepoll_cons_iff:
"⟦a ∉ A; b ∉ B⟧ ⟹ cons(a,A) ≲ cons(b,B) ⟷ A ≲ B"
by (blast intro: cons_lepoll_cong cons_lepoll_consD)
lemma cons_eqpoll_cons_iff:
"⟦a ∉ A; b ∉ B⟧ ⟹ cons(a,A) ≈ cons(b,B) ⟷ A ≈ B"
by (blast intro: cons_eqpoll_cong cons_eqpoll_consD)
lemma singleton_eqpoll_1: "{a} ≈ 1"
unfolding succ_def
apply (blast intro!: eqpoll_refl [THEN cons_eqpoll_cong])
done
lemma cardinal_singleton: "|{a}| = 1"
apply (rule singleton_eqpoll_1 [THEN cardinal_cong, THEN trans])
apply (simp (no_asm) add: nat_into_Card [THEN Card_cardinal_eq])
done
lemma not_0_is_lepoll_1: "A ≠ 0 ⟹ 1 ≲ A"
apply (erule not_emptyE)
apply (rule_tac a = "cons (x, A-{x}) " in subst)
apply (rule_tac [2] a = "cons(0,0)" and P= "λy. y ≲ cons (x, A-{x})" in subst)
prefer 3 apply (blast intro: cons_lepoll_cong subset_imp_lepoll, auto)
done
lemma succ_eqpoll_cong: "A ≈ B ⟹ succ(A) ≈ succ(B)"
unfolding succ_def
apply (simp add: cons_eqpoll_cong mem_not_refl)
done
lemma sum_eqpoll_cong: "⟦A ≈ C; B ≈ D⟧ ⟹ A+B ≈ C+D"
unfolding eqpoll_def
apply (blast intro!: sum_bij)
done
lemma prod_eqpoll_cong:
"⟦A ≈ C; B ≈ D⟧ ⟹ A*B ≈ C*D"
unfolding eqpoll_def
apply (blast intro!: prod_bij)
done
lemma inj_disjoint_eqpoll:
"⟦f ∈ inj(A,B); A ∩ B = 0⟧ ⟹ A ∪ (B - range(f)) ≈ B"
unfolding eqpoll_def
apply (rule exI)
apply (rule_tac c = "λx. if x ∈ A then f`x else x"
and d = "λy. if y ∈ range (f) then converse (f) `y else y"
in lam_bijective)
apply (blast intro!: if_type inj_is_fun [THEN apply_type])
apply (simp (no_asm_simp) add: inj_converse_fun [THEN apply_funtype])
apply (safe elim!: UnE')
apply (simp_all add: inj_is_fun [THEN apply_rangeI])
apply (blast intro: inj_converse_fun [THEN apply_type])+
done
subsection‹Lemmas by Krzysztof Grabczewski›
text‹If \<^term>‹A› has at most \<^term>‹n+1› elements and \<^term>‹a ∈ A›
then \<^term>‹A-{a}› has at most \<^term>‹n›.›
lemma Diff_sing_lepoll:
"⟦a ∈ A; A ≲ succ(n)⟧ ⟹ A - {a} ≲ n"
unfolding succ_def
apply (rule cons_lepoll_consD)
apply (rule_tac [3] mem_not_refl)
apply (erule cons_Diff [THEN ssubst], safe)
done
text‹If \<^term>‹A› has at least \<^term>‹n+1› elements then \<^term>‹A-{a}› has at least \<^term>‹n›.›
lemma lepoll_Diff_sing:
assumes A: "succ(n) ≲ A" shows "n ≲ A - {a}"
proof -
have "cons(n,n) ≲ A" using A
by (unfold succ_def)
also have "... ≲ cons(a, A-{a})"
by (blast intro: subset_imp_lepoll)
finally have "cons(n,n) ≲ cons(a, A-{a})" .
thus ?thesis
by (blast intro: cons_lepoll_consD mem_irrefl)
qed
lemma Diff_sing_eqpoll: "⟦a ∈ A; A ≈ succ(n)⟧ ⟹ A - {a} ≈ n"
by (blast intro!: eqpollI
elim!: eqpollE
intro: Diff_sing_lepoll lepoll_Diff_sing)
lemma lepoll_1_is_sing: "⟦A ≲ 1; a ∈ A⟧ ⟹ A = {a}"
apply (frule Diff_sing_lepoll, assumption)
apply (drule lepoll_0_is_0)
apply (blast elim: equalityE)
done
lemma Un_lepoll_sum: "A ∪ B ≲ A+B"
unfolding lepoll_def
apply (rule_tac x = "λx∈A ∪ B. if x∈A then Inl (x) else Inr (x)" in exI)
apply (rule_tac d = "λz. snd (z)" in lam_injective)
apply force
apply (simp add: Inl_def Inr_def)
done
lemma well_ord_Un:
"⟦well_ord(X,R); well_ord(Y,S)⟧ ⟹ ∃T. well_ord(X ∪ Y, T)"
by (erule well_ord_radd [THEN Un_lepoll_sum [THEN lepoll_well_ord]],
assumption)
lemma disj_Un_eqpoll_sum: "A ∩ B = 0 ⟹ A ∪ B ≈ A + B"
unfolding eqpoll_def
apply (rule_tac x = "λa∈A ∪ B. if a ∈ A then Inl (a) else Inr (a)" in exI)
apply (rule_tac d = "λz. case (λx. x, λx. x, z)" in lam_bijective)
apply auto
done
subsection ‹Finite and infinite sets›
lemma eqpoll_imp_Finite_iff: "A ≈ B ⟹ Finite(A) ⟷ Finite(B)"
unfolding Finite_def
apply (blast intro: eqpoll_trans eqpoll_sym)
done
lemma Finite_0 [simp]: "Finite(0)"
unfolding Finite_def
apply (blast intro!: eqpoll_refl nat_0I)
done
lemma Finite_cons: "Finite(x) ⟹ Finite(cons(y,x))"
unfolding Finite_def
apply (case_tac "y ∈ x")
apply (simp add: cons_absorb)
apply (erule bexE)
apply (rule bexI)
apply (erule_tac [2] nat_succI)
apply (simp (no_asm_simp) add: succ_def cons_eqpoll_cong mem_not_refl)
done
lemma Finite_succ: "Finite(x) ⟹ Finite(succ(x))"
unfolding succ_def
apply (erule Finite_cons)
done
lemma lepoll_nat_imp_Finite:
assumes A: "A ≲ n" and n: "n ∈ nat" shows "Finite(A)"
proof -
have "A ≲ n ⟹ Finite(A)" using n
proof (induct n)
case 0
hence "A = 0" by (rule lepoll_0_is_0)
thus ?case by simp
next
case (succ n)
hence "A ≲ n ∨ A ≈ succ(n)" by (blast dest: lepoll_succ_disj)
thus ?case using succ by (auto simp add: Finite_def)
qed
thus ?thesis using A .
qed
lemma lesspoll_nat_is_Finite:
"A ≺ nat ⟹ Finite(A)"
unfolding Finite_def
apply (blast dest: ltD lesspoll_cardinal_lt
lesspoll_imp_eqpoll [THEN eqpoll_sym])
done
lemma lepoll_Finite:
assumes Y: "Y ≲ X" and X: "Finite(X)" shows "Finite(Y)"
proof -
obtain n where n: "n ∈ nat" "X ≈ n" using X
by (auto simp add: Finite_def)
have "Y ≲ X" by (rule Y)
also have "... ≈ n" by (rule n)
finally have "Y ≲ n" .
thus ?thesis using n by (simp add: lepoll_nat_imp_Finite)
qed
lemmas subset_Finite = subset_imp_lepoll [THEN lepoll_Finite]
lemma Finite_cons_iff [iff]: "Finite(cons(y,x)) ⟷ Finite(x)"
by (blast intro: Finite_cons subset_Finite)
lemma Finite_succ_iff [iff]: "Finite(succ(x)) ⟷ Finite(x)"
by (simp add: succ_def)
lemma Finite_Int: "Finite(A) | Finite(B) ⟹ Finite(A ∩ B)"
by (blast intro: subset_Finite)
lemmas Finite_Diff = Diff_subset [THEN subset_Finite]
lemma nat_le_infinite_Ord:
"⟦Ord(i); ¬ Finite(i)⟧ ⟹ nat ≤ i"
unfolding Finite_def
apply (erule Ord_nat [THEN [2] Ord_linear2])
prefer 2 apply assumption
apply (blast intro!: eqpoll_refl elim!: ltE)
done
lemma Finite_imp_well_ord:
"Finite(A) ⟹ ∃r. well_ord(A,r)"
unfolding Finite_def eqpoll_def
apply (blast intro: well_ord_rvimage bij_is_inj well_ord_Memrel nat_into_Ord)
done
lemma succ_lepoll_imp_not_empty: "succ(x) ≲ y ⟹ y ≠ 0"
by (fast dest!: lepoll_0_is_0)
lemma eqpoll_succ_imp_not_empty: "x ≈ succ(n) ⟹ x ≠ 0"
by (fast elim!: eqpoll_sym [THEN eqpoll_0_is_0, THEN succ_neq_0])
lemma Finite_Fin_lemma [rule_format]:
"n ∈ nat ⟹ ∀A. (A≈n ∧ A ⊆ X) ⟶ A ∈ Fin(X)"
apply (induct_tac n)
apply (rule allI)
apply (fast intro!: Fin.emptyI dest!: eqpoll_imp_lepoll [THEN lepoll_0_is_0])
apply (rule allI)
apply (rule impI)
apply (erule conjE)
apply (rule eqpoll_succ_imp_not_empty [THEN not_emptyE], assumption)
apply (frule Diff_sing_eqpoll, assumption)
apply (erule allE)
apply (erule impE, fast)
apply (drule subsetD, assumption)
apply (drule Fin.consI, assumption)
apply (simp add: cons_Diff)
done
lemma Finite_Fin: "⟦Finite(A); A ⊆ X⟧ ⟹ A ∈ Fin(X)"
by (unfold Finite_def, blast intro: Finite_Fin_lemma)
lemma Fin_lemma [rule_format]: "n ∈ nat ⟹ ∀A. A ≈ n ⟶ A ∈ Fin(A)"
apply (induct_tac n)
apply (simp add: eqpoll_0_iff, clarify)
apply (subgoal_tac "∃u. u ∈ A")
apply (erule exE)
apply (rule Diff_sing_eqpoll [elim_format])
prefer 2 apply assumption
apply assumption
apply (rule_tac b = A in cons_Diff [THEN subst], assumption)
apply (rule Fin.consI, blast)
apply (blast intro: subset_consI [THEN Fin_mono, THEN subsetD])
unfolding eqpoll_def
apply (blast intro: bij_converse_bij [THEN bij_is_fun, THEN apply_type])
done
lemma Finite_into_Fin: "Finite(A) ⟹ A ∈ Fin(A)"
unfolding Finite_def
apply (blast intro: Fin_lemma)
done
lemma Fin_into_Finite: "A ∈ Fin(U) ⟹ Finite(A)"
by (fast intro!: Finite_0 Finite_cons elim: Fin_induct)
lemma Finite_Fin_iff: "Finite(A) ⟷ A ∈ Fin(A)"
by (blast intro: Finite_into_Fin Fin_into_Finite)
lemma Finite_Un: "⟦Finite(A); Finite(B)⟧ ⟹ Finite(A ∪ B)"
by (blast intro!: Fin_into_Finite Fin_UnI
dest!: Finite_into_Fin
intro: Un_upper1 [THEN Fin_mono, THEN subsetD]
Un_upper2 [THEN Fin_mono, THEN subsetD])
lemma Finite_Un_iff [simp]: "Finite(A ∪ B) ⟷ (Finite(A) ∧ Finite(B))"
by (blast intro: subset_Finite Finite_Un)
text‹The converse must hold too.›
lemma Finite_Union: "⟦∀y∈X. Finite(y); Finite(X)⟧ ⟹ Finite(⋃(X))"
apply (simp add: Finite_Fin_iff)
apply (rule Fin_UnionI)
apply (erule Fin_induct, simp)
apply (blast intro: Fin.consI Fin_mono [THEN [2] rev_subsetD])
done
lemma Finite_induct [case_names 0 cons, induct set: Finite]:
"⟦Finite(A); P(0);
⋀x B. ⟦Finite(B); x ∉ B; P(B)⟧ ⟹ P(cons(x, B))⟧
⟹ P(A)"
apply (erule Finite_into_Fin [THEN Fin_induct])
apply (blast intro: Fin_into_Finite)+
done
lemma Diff_sing_Finite: "Finite(A - {a}) ⟹ Finite(A)"
unfolding Finite_def
apply (case_tac "a ∈ A")
apply (subgoal_tac [2] "A-{a}=A", auto)
apply (rule_tac x = "succ (n) " in bexI)
apply (subgoal_tac "cons (a, A - {a}) = A ∧ cons (n, n) = succ (n) ")
apply (drule_tac a = a and b = n in cons_eqpoll_cong)
apply (auto dest: mem_irrefl)
done
lemma Diff_Finite [rule_format]: "Finite(B) ⟹ Finite(A-B) ⟶ Finite(A)"
apply (erule Finite_induct, auto)
apply (case_tac "x ∈ A")
apply (subgoal_tac [2] "A-cons (x, B) = A - B")
apply (subgoal_tac "A - cons (x, B) = (A - B) - {x}", simp)
apply (drule Diff_sing_Finite, auto)
done
lemma Finite_RepFun: "Finite(A) ⟹ Finite(RepFun(A,f))"
by (erule Finite_induct, simp_all)
lemma Finite_RepFun_iff_lemma [rule_format]:
"⟦Finite(x); ⋀x y. f(x)=f(y) ⟹ x=y⟧
⟹ ∀A. x = RepFun(A,f) ⟶ Finite(A)"
apply (erule Finite_induct)
apply clarify
apply (case_tac "A=0", simp)
apply (blast del: allE, clarify)
apply (subgoal_tac "∃z∈A. x = f(z)")
prefer 2 apply (blast del: allE elim: equalityE, clarify)
apply (subgoal_tac "B = {f(u) . u ∈ A - {z}}")
apply (blast intro: Diff_sing_Finite)
apply (thin_tac "∀A. P(A) ⟶ Finite(A)" for P)
apply (rule equalityI)
apply (blast intro: elim: equalityE)
apply (blast intro: elim: equalityCE)
done
text‹I don't know why, but if the premise is expressed using meta-connectives
then the simplifier cannot prove it automatically in conditional rewriting.›
lemma Finite_RepFun_iff:
"(∀x y. f(x)=f(y) ⟶ x=y) ⟹ Finite(RepFun(A,f)) ⟷ Finite(A)"
by (blast intro: Finite_RepFun Finite_RepFun_iff_lemma [of _ f])
lemma Finite_Pow: "Finite(A) ⟹ Finite(Pow(A))"
apply (erule Finite_induct)
apply (simp_all add: Pow_insert Finite_Un Finite_RepFun)
done
lemma Finite_Pow_imp_Finite: "Finite(Pow(A)) ⟹ Finite(A)"
apply (subgoal_tac "Finite({{x} . x ∈ A})")
apply (simp add: Finite_RepFun_iff )
apply (blast intro: subset_Finite)
done
lemma Finite_Pow_iff [iff]: "Finite(Pow(A)) ⟷ Finite(A)"
by (blast intro: Finite_Pow Finite_Pow_imp_Finite)
lemma Finite_cardinal_iff:
assumes i: "Ord(i)" shows "Finite(|i|) ⟷ Finite(i)"
by (auto simp add: Finite_def) (blast intro: eqpoll_trans eqpoll_sym Ord_cardinal_eqpoll [OF i])+
lemma nat_wf_on_converse_Memrel: "n ∈ nat ⟹ wf[n](converse(Memrel(n)))"
proof (induct n rule: nat_induct)
case 0 thus ?case by (blast intro: wf_onI)
next
case (succ x)
hence wfx: "⋀Z. Z = 0 ∨ (∃z∈Z. ∀y. z ∈ y ∧ z ∈ x ∧ y ∈ x ∧ z ∈ x ⟶ y ∉ Z)"
by (simp add: wf_on_def wf_def)
show ?case
proof (rule wf_onI)
fix Z u
assume Z: "u ∈ Z" "∀z∈Z. ∃y∈Z. ⟨y, z⟩ ∈ converse(Memrel(succ(x)))"
show False
proof (cases "x ∈ Z")
case True thus False using Z
by (blast elim: mem_irrefl mem_asym)
next
case False thus False using wfx [of Z] Z
by blast
qed
qed
qed
lemma nat_well_ord_converse_Memrel: "n ∈ nat ⟹ well_ord(n,converse(Memrel(n)))"
apply (frule Ord_nat [THEN Ord_in_Ord, THEN well_ord_Memrel])
apply (simp add: well_ord_def tot_ord_converse nat_wf_on_converse_Memrel)
done
lemma well_ord_converse:
"⟦well_ord(A,r);
well_ord(ordertype(A,r), converse(Memrel(ordertype(A, r))))⟧
⟹ well_ord(A,converse(r))"
apply (rule well_ord_Int_iff [THEN iffD1])
apply (frule ordermap_bij [THEN bij_is_inj, THEN well_ord_rvimage], assumption)
apply (simp add: rvimage_converse converse_Int converse_prod
ordertype_ord_iso [THEN ord_iso_rvimage_eq])
done
lemma ordertype_eq_n:
assumes r: "well_ord(A,r)" and A: "A ≈ n" and n: "n ∈ nat"
shows "ordertype(A,r) = n"
proof -
have "ordertype(A,r) ≈ A"
by (blast intro: bij_imp_eqpoll bij_converse_bij ordermap_bij r)
also have "... ≈ n" by (rule A)
finally have "ordertype(A,r) ≈ n" .
thus ?thesis
by (simp add: Ord_nat_eqpoll_iff Ord_ordertype n r)
qed
lemma Finite_well_ord_converse:
"⟦Finite(A); well_ord(A,r)⟧ ⟹ well_ord(A,converse(r))"
unfolding Finite_def
apply (rule well_ord_converse, assumption)
apply (blast dest: ordertype_eq_n intro!: nat_well_ord_converse_Memrel)
done
lemma nat_into_Finite: "n ∈ nat ⟹ Finite(n)"
by (auto simp add: Finite_def intro: eqpoll_refl)
lemma nat_not_Finite: "¬ Finite(nat)"
proof -
{ fix n
assume n: "n ∈ nat" "nat ≈ n"
have "n ∈ nat" by (rule n)
also have "... = n" using n
by (simp add: Ord_nat_eqpoll_iff Ord_nat)
finally have "n ∈ n" .
hence False
by (blast elim: mem_irrefl)
}
thus ?thesis
by (auto simp add: Finite_def)
qed
end