src/ZF/Cardinal_AC.thy
 author wenzelm Tue Sep 25 22:36:06 2012 +0200 (2012-09-25 ago) changeset 49566 66cbf8bb4693 parent 47071 2884ee1ffbf0 child 58871 c399ae4b836f permissions -rw-r--r--
basic integration of graphview into document model;
 clasohm@1478 ` 1` ```(* Title: ZF/Cardinal_AC.thy ``` clasohm@1478 ` 2` ``` Author: Lawrence C Paulson, Cambridge University Computer Laboratory ``` lcp@484 ` 3` ``` Copyright 1994 University of Cambridge ``` lcp@484 ` 4` paulson@13134 ` 5` ```These results help justify infinite-branching datatypes ``` lcp@484 ` 6` ```*) ``` lcp@484 ` 7` paulson@13328 ` 8` ```header{*Cardinal Arithmetic Using AC*} ``` paulson@13328 ` 9` haftmann@16417 ` 10` ```theory Cardinal_AC imports CardinalArith Zorn begin ``` paulson@13134 ` 11` paulson@13356 ` 12` ```subsection{*Strengthened Forms of Existing Theorems on Cardinals*} ``` paulson@13134 ` 13` paulson@46954 ` 14` ```lemma cardinal_eqpoll: "|A| \ A" ``` paulson@13134 ` 15` ```apply (rule AC_well_ord [THEN exE]) ``` paulson@13134 ` 16` ```apply (erule well_ord_cardinal_eqpoll) ``` paulson@13134 ` 17` ```done ``` paulson@13134 ` 18` paulson@14046 ` 19` ```text{*The theorem @{term "||A|| = |A|"} *} ``` wenzelm@45602 ` 20` ```lemmas cardinal_idem = cardinal_eqpoll [THEN cardinal_cong, simp] ``` paulson@13134 ` 21` paulson@46954 ` 22` ```lemma cardinal_eqE: "|X| = |Y| ==> X \ Y" ``` paulson@13134 ` 23` ```apply (rule AC_well_ord [THEN exE]) ``` paulson@13134 ` 24` ```apply (rule AC_well_ord [THEN exE]) ``` paulson@13269 ` 25` ```apply (rule well_ord_cardinal_eqE, assumption+) ``` paulson@13134 ` 26` ```done ``` paulson@13134 ` 27` paulson@46954 ` 28` ```lemma cardinal_eqpoll_iff: "|X| = |Y| \ X \ Y" ``` paulson@13269 ` 29` ```by (blast intro: cardinal_cong cardinal_eqE) ``` paulson@13134 ` 30` paulson@13615 ` 31` ```lemma cardinal_disjoint_Un: ``` paulson@46820 ` 32` ``` "[| |A|=|B|; |C|=|D|; A \ C = 0; B \ D = 0 |] ``` paulson@46820 ` 33` ``` ==> |A \ C| = |B \ D|" ``` paulson@13615 ` 34` ```by (simp add: cardinal_eqpoll_iff eqpoll_disjoint_Un) ``` paulson@13134 ` 35` paulson@46954 ` 36` ```lemma lepoll_imp_Card_le: "A \ B ==> |A| \ |B|" ``` paulson@13134 ` 37` ```apply (rule AC_well_ord [THEN exE]) ``` paulson@13269 ` 38` ```apply (erule well_ord_lepoll_imp_Card_le, assumption) ``` paulson@13134 ` 39` ```done ``` paulson@13134 ` 40` paulson@46821 ` 41` ```lemma cadd_assoc: "(i \ j) \ k = i \ (j \ k)" ``` paulson@13134 ` 42` ```apply (rule AC_well_ord [THEN exE]) ``` paulson@13134 ` 43` ```apply (rule AC_well_ord [THEN exE]) ``` paulson@13134 ` 44` ```apply (rule AC_well_ord [THEN exE]) ``` paulson@13269 ` 45` ```apply (rule well_ord_cadd_assoc, assumption+) ``` paulson@13134 ` 46` ```done ``` paulson@13134 ` 47` paulson@46821 ` 48` ```lemma cmult_assoc: "(i \ j) \ k = i \ (j \ k)" ``` paulson@13134 ` 49` ```apply (rule AC_well_ord [THEN exE]) ``` paulson@13134 ` 50` ```apply (rule AC_well_ord [THEN exE]) ``` paulson@13134 ` 51` ```apply (rule AC_well_ord [THEN exE]) ``` paulson@13269 ` 52` ```apply (rule well_ord_cmult_assoc, assumption+) ``` paulson@13134 ` 53` ```done ``` paulson@13134 ` 54` paulson@46821 ` 55` ```lemma cadd_cmult_distrib: "(i \ j) \ k = (i \ k) \ (j \ k)" ``` paulson@13134 ` 56` ```apply (rule AC_well_ord [THEN exE]) ``` paulson@13134 ` 57` ```apply (rule AC_well_ord [THEN exE]) ``` paulson@13134 ` 58` ```apply (rule AC_well_ord [THEN exE]) ``` paulson@13269 ` 59` ```apply (rule well_ord_cadd_cmult_distrib, assumption+) ``` paulson@13134 ` 60` ```done ``` paulson@13134 ` 61` paulson@46954 ` 62` ```lemma InfCard_square_eq: "InfCard(|A|) ==> A*A \ A" ``` paulson@13134 ` 63` ```apply (rule AC_well_ord [THEN exE]) ``` paulson@13269 ` 64` ```apply (erule well_ord_InfCard_square_eq, assumption) ``` paulson@13134 ` 65` ```done ``` paulson@13134 ` 66` paulson@13134 ` 67` paulson@14046 ` 68` ```subsection {*The relationship between cardinality and le-pollence*} ``` paulson@13134 ` 69` paulson@46954 ` 70` ```lemma Card_le_imp_lepoll: ``` paulson@46954 ` 71` ``` assumes "|A| \ |B|" shows "A \ B" ``` paulson@46954 ` 72` ```proof - ``` paulson@46954 ` 73` ``` have "A \ |A|" ``` paulson@46954 ` 74` ``` by (rule cardinal_eqpoll [THEN eqpoll_sym]) ``` paulson@46954 ` 75` ``` also have "... \ |B|" ``` paulson@46954 ` 76` ``` by (rule le_imp_subset [THEN subset_imp_lepoll]) (rule assms) ``` paulson@46954 ` 77` ``` also have "... \ B" ``` paulson@46954 ` 78` ``` by (rule cardinal_eqpoll) ``` paulson@46954 ` 79` ``` finally show ?thesis . ``` paulson@46954 ` 80` ```qed ``` paulson@13134 ` 81` paulson@46954 ` 82` ```lemma le_Card_iff: "Card(K) ==> |A| \ K \ A \ K" ``` paulson@46820 ` 83` ```apply (erule Card_cardinal_eq [THEN subst], rule iffI, ``` paulson@13269 ` 84` ``` erule Card_le_imp_lepoll) ``` paulson@46820 ` 85` ```apply (erule lepoll_imp_Card_le) ``` paulson@13134 ` 86` ```done ``` paulson@13134 ` 87` paulson@46954 ` 88` ```lemma cardinal_0_iff_0 [simp]: "|A| = 0 \ A = 0" ``` paulson@46820 ` 89` ```apply auto ``` paulson@14046 ` 90` ```apply (drule cardinal_0 [THEN ssubst]) ``` paulson@14046 ` 91` ```apply (blast intro: eqpoll_0_iff [THEN iffD1] cardinal_eqpoll_iff [THEN iffD1]) ``` paulson@14046 ` 92` ```done ``` paulson@14046 ` 93` paulson@46954 ` 94` ```lemma cardinal_lt_iff_lesspoll: ``` paulson@46954 ` 95` ``` assumes i: "Ord(i)" shows "i < |A| \ i \ A" ``` paulson@46954 ` 96` ```proof ``` paulson@46954 ` 97` ``` assume "i < |A|" ``` paulson@46954 ` 98` ``` hence "i \ |A|" ``` paulson@46954 ` 99` ``` by (blast intro: lt_Card_imp_lesspoll Card_cardinal) ``` paulson@46954 ` 100` ``` also have "... \ A" ``` paulson@46954 ` 101` ``` by (rule cardinal_eqpoll) ``` paulson@46954 ` 102` ``` finally show "i \ A" . ``` paulson@46954 ` 103` ```next ``` paulson@46954 ` 104` ``` assume "i \ A" ``` paulson@46954 ` 105` ``` also have "... \ |A|" ``` paulson@46954 ` 106` ``` by (blast intro: cardinal_eqpoll eqpoll_sym) ``` paulson@46954 ` 107` ``` finally have "i \ |A|" . ``` paulson@46954 ` 108` ``` thus "i < |A|" using i ``` paulson@46954 ` 109` ``` by (force intro: cardinal_lt_imp_lt lesspoll_cardinal_lt) ``` paulson@46954 ` 110` ```qed ``` paulson@14046 ` 111` paulson@14046 ` 112` ```lemma cardinal_le_imp_lepoll: " i \ |A| ==> i \ A" ``` paulson@46954 ` 113` ``` by (blast intro: lt_Ord Card_le_imp_lepoll Ord_cardinal_le le_trans) ``` paulson@14046 ` 114` paulson@14046 ` 115` paulson@14046 ` 116` ```subsection{*Other Applications of AC*} ``` paulson@14046 ` 117` paulson@47052 ` 118` ```lemma surj_implies_inj: ``` paulson@47052 ` 119` ``` assumes f: "f \ surj(X,Y)" shows "\g. g \ inj(Y,X)" ``` paulson@47052 ` 120` ```proof - ``` paulson@47052 ` 121` ``` from f AC_Pi [of Y "%y. f-``{y}"] ``` paulson@47052 ` 122` ``` obtain z where z: "z \ (\ y\Y. f -`` {y})" ``` paulson@47052 ` 123` ``` by (auto simp add: surj_def) (fast dest: apply_Pair) ``` paulson@47052 ` 124` ``` show ?thesis ``` paulson@47052 ` 125` ``` proof ``` paulson@47052 ` 126` ``` show "z \ inj(Y, X)" using z surj_is_fun [OF f] ``` paulson@47052 ` 127` ``` by (blast dest: apply_type Pi_memberD ``` paulson@47052 ` 128` ``` intro: apply_equality Pi_type f_imp_injective) ``` paulson@47052 ` 129` ``` qed ``` paulson@47052 ` 130` ```qed ``` paulson@13134 ` 131` paulson@47052 ` 132` ```text{*Kunen's Lemma 10.20*} ``` paulson@47052 ` 133` ```lemma surj_implies_cardinal_le: ``` paulson@47052 ` 134` ``` assumes f: "f \ surj(X,Y)" shows "|Y| \ |X|" ``` paulson@47052 ` 135` ```proof (rule lepoll_imp_Card_le) ``` paulson@47052 ` 136` ``` from f [THEN surj_implies_inj] obtain g where "g \ inj(Y,X)" .. ``` paulson@47052 ` 137` ``` thus "Y \ X" ``` paulson@47052 ` 138` ``` by (auto simp add: lepoll_def) ``` paulson@47052 ` 139` ```qed ``` paulson@13134 ` 140` paulson@47052 ` 141` ```text{*Kunen's Lemma 10.21*} ``` paulson@13615 ` 142` ```lemma cardinal_UN_le: ``` paulson@46963 ` 143` ``` assumes K: "InfCard(K)" ``` paulson@46963 ` 144` ``` shows "(!!i. i\K ==> |X(i)| \ K) ==> |\i\K. X(i)| \ K" ``` paulson@46963 ` 145` ```proof (simp add: K InfCard_is_Card le_Card_iff) ``` paulson@46963 ` 146` ``` have [intro]: "Ord(K)" by (blast intro: InfCard_is_Card Card_is_Ord K) ``` paulson@46963 ` 147` ``` assume "!!i. i\K ==> X(i) \ K" ``` paulson@46963 ` 148` ``` hence "!!i. i\K ==> \f. f \ inj(X(i), K)" by (simp add: lepoll_def) ``` paulson@46963 ` 149` ``` with AC_Pi obtain f where f: "f \ (\ i\K. inj(X(i), K))" ``` paulson@47052 ` 150` ``` by force ``` paulson@46963 ` 151` ``` { fix z ``` paulson@46963 ` 152` ``` assume z: "z \ (\i\K. X(i))" ``` paulson@46963 ` 153` ``` then obtain i where i: "i \ K" "Ord(i)" "z \ X(i)" ``` paulson@46963 ` 154` ``` by (blast intro: Ord_in_Ord [of K]) ``` paulson@46963 ` 155` ``` hence "(LEAST i. z \ X(i)) \ i" by (fast intro: Least_le) ``` paulson@46963 ` 156` ``` hence "(LEAST i. z \ X(i)) < K" by (best intro: lt_trans1 ltI i) ``` paulson@46963 ` 157` ``` hence "(LEAST i. z \ X(i)) \ K" and "z \ X(LEAST i. z \ X(i))" ``` paulson@46963 ` 158` ``` by (auto intro: LeastI ltD i) ``` paulson@46963 ` 159` ``` } note mems = this ``` paulson@46963 ` 160` ``` have "(\i\K. X(i)) \ K \ K" ``` paulson@46963 ` 161` ``` proof (unfold lepoll_def) ``` paulson@46963 ` 162` ``` show "\f. f \ inj(\RepFun(K, X), K \ K)" ``` paulson@46963 ` 163` ``` apply (rule exI) ``` paulson@46963 ` 164` ``` apply (rule_tac c = "%z. \LEAST i. z \ X(i), f ` (LEAST i. z \ X(i)) ` z\" ``` paulson@46963 ` 165` ``` and d = "%\i,j\. converse (f`i) ` j" in lam_injective) ``` paulson@46963 ` 166` ``` apply (force intro: f inj_is_fun mems apply_type Perm.left_inverse)+ ``` paulson@46963 ` 167` ``` done ``` paulson@46963 ` 168` ``` qed ``` paulson@46963 ` 169` ``` also have "... \ K" ``` paulson@46963 ` 170` ``` by (simp add: K InfCard_square_eq InfCard_is_Card Card_cardinal_eq) ``` paulson@46963 ` 171` ``` finally show "(\i\K. X(i)) \ K" . ``` paulson@46963 ` 172` ```qed ``` paulson@13134 ` 173` paulson@46963 ` 174` ```text{*The same again, using @{term csucc}*} ``` paulson@13134 ` 175` ```lemma cardinal_UN_lt_csucc: ``` paulson@47071 ` 176` ``` "[| InfCard(K); \i. i\K \ |X(i)| < csucc(K) |] ``` paulson@13615 ` 177` ``` ==> |\i\K. X(i)| < csucc(K)" ``` paulson@13615 ` 178` ```by (simp add: Card_lt_csucc_iff cardinal_UN_le InfCard_is_Card Card_cardinal) ``` paulson@13134 ` 179` paulson@47052 ` 180` ```text{*The same again, for a union of ordinals. In use, j(i) is a bit like rank(i), ``` paulson@47052 ` 181` ``` the least ordinal j such that i:Vfrom(A,j). *} ``` paulson@13134 ` 182` ```lemma cardinal_UN_Ord_lt_csucc: ``` paulson@47071 ` 183` ``` "[| InfCard(K); \i. i\K \ j(i) < csucc(K) |] ``` paulson@13615 ` 184` ``` ==> (\i\K. j(i)) < csucc(K)" ``` paulson@13269 ` 185` ```apply (rule cardinal_UN_lt_csucc [THEN Card_lt_imp_lt], assumption) ``` paulson@13134 ` 186` ```apply (blast intro: Ord_cardinal_le [THEN lt_trans1] elim: ltE) ``` paulson@13134 ` 187` ```apply (blast intro!: Ord_UN elim: ltE) ``` paulson@13134 ` 188` ```apply (erule InfCard_is_Card [THEN Card_is_Ord, THEN Card_csucc]) ``` paulson@13134 ` 189` ```done ``` paulson@13134 ` 190` paulson@13134 ` 191` paulson@47071 ` 192` ```subsection{*The Main Result for Infinite-Branching Datatypes*} ``` paulson@13134 ` 193` paulson@47071 ` 194` ```text{*As above, but the index set need not be a cardinal. Work ``` paulson@47071 ` 195` ```backwards along the injection from @{term W} into @{term K}, given ``` paulson@47071 ` 196` ```that @{term"W\0"}.*} ``` paulson@46954 ` 197` paulson@13134 ` 198` ```lemma inj_UN_subset: ``` paulson@46954 ` 199` ``` assumes f: "f \ inj(A,B)" and a: "a \ A" ``` paulson@46954 ` 200` ``` shows "(\x\A. C(x)) \ (\y\B. C(if y \ range(f) then converse(f)`y else a))" ``` paulson@46954 ` 201` ```proof (rule UN_least) ``` paulson@46954 ` 202` ``` fix x ``` paulson@46954 ` 203` ``` assume x: "x \ A" ``` paulson@46954 ` 204` ``` hence fx: "f ` x \ B" by (blast intro: f inj_is_fun [THEN apply_type]) ``` paulson@46954 ` 205` ``` have "C(x) \ C(if f ` x \ range(f) then converse(f) ` (f ` x) else a)" ``` paulson@46954 ` 206` ``` using f x by (simp add: inj_is_fun [THEN apply_rangeI]) ``` paulson@46954 ` 207` ``` also have "... \ (\y\B. C(if y \ range(f) then converse(f) ` y else a))" ``` paulson@46954 ` 208` ``` by (rule UN_upper [OF fx]) ``` paulson@46954 ` 209` ``` finally show "C(x) \ (\y\B. C(if y \ range(f) then converse(f)`y else a))" . ``` paulson@46954 ` 210` ```qed ``` paulson@13134 ` 211` paulson@47071 ` 212` ```theorem le_UN_Ord_lt_csucc: ``` paulson@47071 ` 213` ``` assumes IK: "InfCard(K)" and WK: "|W| \ K" and j: "\w. w\W \ j(w) < csucc(K)" ``` paulson@47071 ` 214` ``` shows "(\w\W. j(w)) < csucc(K)" ``` paulson@47071 ` 215` ```proof - ``` paulson@47071 ` 216` ``` have CK: "Card(K)" ``` paulson@47071 ` 217` ``` by (simp add: InfCard_is_Card IK) ``` paulson@47071 ` 218` ``` then obtain f where f: "f \ inj(W, K)" using WK ``` paulson@47071 ` 219` ``` by(auto simp add: le_Card_iff lepoll_def) ``` paulson@47071 ` 220` ``` have OU: "Ord(\w\W. j(w))" using j ``` paulson@47071 ` 221` ``` by (blast elim: ltE) ``` paulson@47071 ` 222` ``` note lt_subset_trans [OF _ _ OU, trans] ``` paulson@47071 ` 223` ``` show ?thesis ``` paulson@47071 ` 224` ``` proof (cases "W=0") ``` paulson@47071 ` 225` ``` case True --{*solve the easy 0 case*} ``` paulson@47071 ` 226` ``` thus ?thesis by (simp add: CK Card_is_Ord Card_csucc Ord_0_lt_csucc) ``` paulson@47071 ` 227` ``` next ``` paulson@47071 ` 228` ``` case False ``` paulson@47071 ` 229` ``` then obtain x where x: "x \ W" by blast ``` paulson@47071 ` 230` ``` have "(\x\W. j(x)) \ (\k\K. j(if k \ range(f) then converse(f) ` k else x))" ``` paulson@47071 ` 231` ``` by (rule inj_UN_subset [OF f x]) ``` paulson@47071 ` 232` ``` also have "... < csucc(K)" using IK ``` paulson@47071 ` 233` ``` proof (rule cardinal_UN_Ord_lt_csucc) ``` paulson@47071 ` 234` ``` fix k ``` paulson@47071 ` 235` ``` assume "k \ K" ``` paulson@47071 ` 236` ``` thus "j(if k \ range(f) then converse(f) ` k else x) < csucc(K)" using f x j ``` paulson@47071 ` 237` ``` by (simp add: inj_converse_fun [THEN apply_type]) ``` paulson@47071 ` 238` ``` qed ``` paulson@47071 ` 239` ``` finally show ?thesis . ``` paulson@47071 ` 240` ``` qed ``` paulson@47071 ` 241` ```qed ``` paulson@13134 ` 242` paulson@13134 ` 243` ```end ```