(* Title: ZF/Cardinal_AC.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
These results help justify infinite-branching datatypes
*)
section‹Cardinal Arithmetic
Using AC
›
theory Cardinal_AC
imports CardinalArith Zorn
begin
subsection‹Strengthened Forms of Existing
Theorems on Cardinals
›
lemma cardinal_eqpoll:
"|A| \ A"
apply (rule AC_well_ord [
THEN exE])
apply (erule well_ord_cardinal_eqpoll)
done
text‹The
theorem 🍋‹||A|| = |A|
››
lemmas cardinal_idem = cardinal_eqpoll [
THEN cardinal_cong, simp]
lemma cardinal_eqE:
"|X| = |Y| \ X \ Y"
apply (rule AC_well_ord [
THEN exE])
apply (rule AC_well_ord [
THEN exE])
apply (rule well_ord_cardinal_eqE, assumption+)
done
lemma cardinal_eqpoll_iff:
"|X| = |Y| \ X \ Y"
by (blast intro: cardinal_cong cardinal_eqE)
lemma cardinal_disjoint_Un:
"\|A|=|B|; |C|=|D|; A \ C = 0; B \ D = 0\
==> |A
∪ C| = |B
∪ D|
"
by (simp add: cardinal_eqpoll_iff eqpoll_disjoint_Un)
lemma lepoll_imp_cardinal_le:
"A \ B \ |A| \ |B|"
apply (rule AC_well_ord [
THEN exE])
apply (erule well_ord_lepoll_imp_cardinal_le, assumption)
done
lemma cadd_assoc:
"(i \ j) \ k = i \ (j \ k)"
apply (rule AC_well_ord [
THEN exE])
apply (rule AC_well_ord [
THEN exE])
apply (rule AC_well_ord [
THEN exE])
apply (rule well_ord_cadd_assoc, assumption+)
done
lemma cmult_assoc:
"(i \ j) \ k = i \ (j \ k)"
apply (rule AC_well_ord [
THEN exE])
apply (rule AC_well_ord [
THEN exE])
apply (rule AC_well_ord [
THEN exE])
apply (rule well_ord_cmult_assoc, assumption+)
done
lemma cadd_cmult_distrib:
"(i \ j) \ k = (i \ k) \ (j \ k)"
apply (rule AC_well_ord [
THEN exE])
apply (rule AC_well_ord [
THEN exE])
apply (rule AC_well_ord [
THEN exE])
apply (rule well_ord_cadd_cmult_distrib, assumption+)
done
lemma InfCard_square_eq:
"InfCard(|A|) \ A*A \ A"
apply (rule AC_well_ord [
THEN exE])
apply (erule well_ord_InfCard_square_eq, assumption)
done
subsection ‹The relationship between cardinality
and le-pollence
›
lemma Card_le_imp_lepoll:
assumes "|A| \ |B|" shows "A \ B"
proof -
have "A \ |A|"
by (rule cardinal_eqpoll [
THEN eqpoll_sym])
also have "... \ |B|"
by (rule le_imp_subset [
THEN subset_imp_lepoll]) (rule assms)
also have "... \ B"
by (rule cardinal_eqpoll)
finally show ?thesis .
qed
lemma le_Card_iff:
"Card(K) \ |A| \ K \ A \ K"
apply (erule Card_cardinal_eq [
THEN subst], rule iffI,
erule Card_le_imp_lepoll)
apply (erule lepoll_imp_cardinal_le)
done
lemma cardinal_0_iff_0 [simp]:
"|A| = 0 \ A = 0"
apply auto
apply (drule cardinal_0 [
THEN ssubst])
apply (blast intro: eqpoll_0_iff [
THEN iffD1] cardinal_eqpoll_iff [
THEN iffD1])
done
lemma cardinal_lt_iff_lesspoll:
assumes i:
"Ord(i)" shows "i < |A| \ i \ A"
proof
assume "i < |A|"
hence "i \ |A|"
by (blast intro: lt_Card_imp_lesspoll Card_cardinal)
also have "... \ A"
by (rule cardinal_eqpoll)
finally show "i \ A" .
next
assume "i \ A"
also have "... \ |A|"
by (blast intro: cardinal_eqpoll eqpoll_sym)
finally have "i \ |A|" .
thus "i < |A|" using i
by (force intro: cardinal_lt_imp_lt lesspoll_cardinal_lt)
qed
lemma cardinal_le_imp_lepoll:
" i \ |A| \ i \ A"
by (blast intro: lt_Ord Card_le_imp_lepoll Ord_cardinal_le le_trans)
subsection‹Other Applications of AC
›
lemma surj_implies_inj:
assumes f:
"f \ surj(X,Y)" shows "\g. g \ inj(Y,X)"
proof -
from f AC_Pi [of Y
"\y. f-``{y}"]
obtain z
where z:
"z \ (\y\Y. f -`` {y})"
by (auto simp add: surj_def) (fast dest: apply_Pair)
show ?thesis
proof
show "z \ inj(Y, X)" using z surj_is_fun [OF f]
by (blast dest: apply_type Pi_memberD
intro: apply_equality Pi_type f_imp_injective)
qed
qed
text‹Kunen
's Lemma 10.20\
lemma surj_implies_cardinal_le:
assumes f:
"f \ surj(X,Y)" shows "|Y| \ |X|"
proof (rule lepoll_imp_cardinal_le)
from f [
THEN surj_implies_inj]
obtain g
where "g \ inj(Y,X)" ..
thus "Y \ X"
by (auto simp add: lepoll_def)
qed
text‹Kunen
's Lemma 10.21\
lemma cardinal_UN_le:
assumes K:
"InfCard(K)"
shows "(\i. i\K \ |X(i)| \ K) \ |\i\K. X(i)| \ K"
proof (simp add: K InfCard_is_Card le_Card_iff)
have [intro]:
"Ord(K)" by (blast intro: InfCard_is_Card Card_is_Ord K)
assume "\i. i\K \ X(i) \ K"
hence "\i. i\K \ \f. f \ inj(X(i), K)" by (simp add: lepoll_def)
with AC_Pi
obtain f
where f:
"f \ (\i\K. inj(X(i), K))"
by force
{
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)) \ K \ K"
proof (unfold lepoll_def)
show "\f. f \ inj(\RepFun(K, X), K \ K)"
apply (rule exI)
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)+
done
qed
also have "... \ K"
by (simp add: K InfCard_square_eq InfCard_is_Card Card_cardinal_eq)
finally show "(\i\K. X(i)) \ K" .
qed
text‹The same again,
using 🍋‹csucc
››
lemma cardinal_UN_lt_csucc:
"\InfCard(K); \i. i\K \ |X(i)| < csucc(K)\
==> |
∪i
∈K. X(i)| < csucc(K)
"
by (simp add: Card_lt_csucc_iff cardinal_UN_le InfCard_is_Card Card_cardinal)
text‹The same again,
for a union of ordinals.
In use, j(i)
is a bit like rank(i),
the least ordinal j such that i:Vfrom(A,j).
›
lemma cardinal_UN_Ord_lt_csucc:
"\InfCard(K); \i. i\K \ j(i) < csucc(K)\
==> (
∪i
∈K. j(i)) < csucc(K)
"
apply (rule cardinal_UN_lt_csucc [
THEN Card_lt_imp_lt], assumption)
apply (blast intro: Ord_cardinal_le [
THEN lt_trans1] elim: ltE)
apply (blast intro!: Ord_UN elim: ltE)
apply (erule InfCard_is_Card [
THEN Card_is_Ord,
THEN Card_csucc])
done
subsection‹The Main Result
for Infinite-Branching Datatypes
›
text‹As above, but the index set need not be a cardinal. Work
backwards along the injection
from 🍋‹W
› into
🍋‹K
›, given
that
🍋‹W
≠0
›.
›
lemma inj_UN_subset:
assumes f:
"f \ inj(A,B)" and a:
"a \ A"
shows "(\x\A. C(x)) \ (\y\B. C(if y \ range(f) then converse(f)`y else a))"
proof (rule UN_least)
fix x
assume x:
"x \ A"
hence fx:
"f ` x \ B" by (blast intro: f inj_is_fun [
THEN apply_type])
have "C(x) \ C(if f ` x \ range(f) then converse(f) ` (f ` x) else a)"
using f x
by (simp add: inj_is_fun [
THEN apply_rangeI])
also have "... \ (\y\B. C(if y \ range(f) then converse(f) ` y else a))"
by (rule UN_upper [OF fx])
finally show "C(x) \ (\y\B. C(if y \ range(f) then converse(f)`y else a))" .
qed
theorem le_UN_Ord_lt_csucc:
assumes IK:
"InfCard(K)" and WK:
"|W| \ K" and j:
"\w. w\W \ j(w) < csucc(K)"
shows "(\w\W. j(w)) < csucc(K)"
proof -
have CK:
"Card(K)"
by (simp add: InfCard_is_Card IK)
then obtain f
where f:
"f \ inj(W, K)" using WK
by(auto simp add: le_Card_iff lepoll_def)
have OU:
"Ord(\w\W. j(w))" using j
by (blast elim: ltE)
note lt_subset_trans [OF _ _ OU, trans]
show ?thesis
proof (cases
"W=0")
case True
🍋 ‹solve the easy 0
case›
thus ?thesis
by (simp add: CK Card_is_Ord Card_csucc Ord_0_lt_csucc)
next
case False
then obtain x
where x:
"x \ W" by blast
have "(\x\W. j(x)) \ (\k\K. j(if k \ range(f) then converse(f) ` k else x))"
by (rule inj_UN_subset [OF f x])
also have "... < csucc(K)" using IK
proof (rule cardinal_UN_Ord_lt_csucc)
fix k
assume "k \ K"
thus "j(if k \ range(f) then converse(f) ` k else x) < csucc(K)" using f x j
by (simp add: inj_converse_fun [
THEN apply_type])
qed
finally show ?thesis .
qed
qed
end
