src/ZF/Cardinal_AC.thy
 author paulson Tue Mar 06 15:15:49 2012 +0000 (2012-03-06) changeset 46820 c656222c4dc1 parent 46751 6b94c39b7366 child 46821 ff6b0c1087f2 permissions -rw-r--r--
 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@13134 ` 14` ```lemma cardinal_eqpoll: "|A| eqpoll 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@13134 ` 22` ```lemma cardinal_eqE: "|X| = |Y| ==> X eqpoll 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@13134 ` 28` ```lemma cardinal_eqpoll_iff: "|X| = |Y| <-> X eqpoll 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@46820 ` 36` ```lemma lepoll_imp_Card_le: "A lepoll 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@13134 ` 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@13134 ` 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@13134 ` 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@13134 ` 62` ```lemma InfCard_square_eq: "InfCard(|A|) ==> A*A eqpoll 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@46820 ` 70` ```lemma Card_le_imp_lepoll: "|A| \ |B| ==> A lepoll B" ``` paulson@13134 ` 71` ```apply (rule cardinal_eqpoll ``` paulson@13134 ` 72` ``` [THEN eqpoll_sym, THEN eqpoll_imp_lepoll, THEN lepoll_trans]) ``` paulson@13134 ` 73` ```apply (erule le_imp_subset [THEN subset_imp_lepoll, THEN lepoll_trans]) ``` paulson@13134 ` 74` ```apply (rule cardinal_eqpoll [THEN eqpoll_imp_lepoll]) ``` paulson@13134 ` 75` ```done ``` paulson@13134 ` 76` paulson@46820 ` 77` ```lemma le_Card_iff: "Card(K) ==> |A| \ K <-> A lepoll K" ``` paulson@46820 ` 78` ```apply (erule Card_cardinal_eq [THEN subst], rule iffI, ``` paulson@13269 ` 79` ``` erule Card_le_imp_lepoll) ``` paulson@46820 ` 80` ```apply (erule lepoll_imp_Card_le) ``` paulson@13134 ` 81` ```done ``` paulson@13134 ` 82` paulson@14046 ` 83` ```lemma cardinal_0_iff_0 [simp]: "|A| = 0 <-> A = 0"; ``` paulson@46820 ` 84` ```apply auto ``` paulson@14046 ` 85` ```apply (drule cardinal_0 [THEN ssubst]) ``` paulson@14046 ` 86` ```apply (blast intro: eqpoll_0_iff [THEN iffD1] cardinal_eqpoll_iff [THEN iffD1]) ``` paulson@14046 ` 87` ```done ``` paulson@14046 ` 88` paulson@14046 ` 89` ```lemma cardinal_lt_iff_lesspoll: "Ord(i) ==> i < |A| <-> i lesspoll A" ``` paulson@14046 ` 90` ```apply (cut_tac A = "A" in cardinal_eqpoll) ``` paulson@14046 ` 91` ```apply (auto simp add: eqpoll_iff) ``` paulson@14046 ` 92` ```apply (blast intro: lesspoll_trans2 lt_Card_imp_lesspoll Card_cardinal) ``` paulson@46820 ` 93` ```apply (force intro: cardinal_lt_imp_lt lesspoll_cardinal_lt lesspoll_trans2 ``` paulson@14046 ` 94` ``` simp add: cardinal_idem) ``` paulson@14046 ` 95` ```done ``` paulson@14046 ` 96` paulson@14046 ` 97` ```lemma cardinal_le_imp_lepoll: " i \ |A| ==> i \ A" ``` paulson@14046 ` 98` ```apply (blast intro: lt_Ord Card_le_imp_lepoll Ord_cardinal_le le_trans) ``` paulson@14046 ` 99` ```done ``` paulson@14046 ` 100` paulson@14046 ` 101` paulson@14046 ` 102` ```subsection{*Other Applications of AC*} ``` paulson@14046 ` 103` paulson@46820 ` 104` ```lemma surj_implies_inj: "f: surj(X,Y) ==> \g. g: inj(Y,X)" ``` paulson@13134 ` 105` ```apply (unfold surj_def) ``` paulson@13134 ` 106` ```apply (erule CollectE) ``` paulson@13784 ` 107` ```apply (rule_tac A1 = Y and B1 = "%y. f-``{y}" in AC_Pi [THEN exE]) ``` paulson@13134 ` 108` ```apply (fast elim!: apply_Pair) ``` paulson@46820 ` 109` ```apply (blast dest: apply_type Pi_memberD ``` paulson@13615 ` 110` ``` intro: apply_equality Pi_type f_imp_injective) ``` paulson@13134 ` 111` ```done ``` paulson@13134 ` 112` paulson@13134 ` 113` ```(*Kunen's Lemma 10.20*) ``` paulson@46820 ` 114` ```lemma surj_implies_cardinal_le: "f: surj(X,Y) ==> |Y| \ |X|" ``` paulson@13134 ` 115` ```apply (rule lepoll_imp_Card_le) ``` paulson@13134 ` 116` ```apply (erule surj_implies_inj [THEN exE]) ``` paulson@13134 ` 117` ```apply (unfold lepoll_def) ``` paulson@13134 ` 118` ```apply (erule exI) ``` paulson@13134 ` 119` ```done ``` paulson@13134 ` 120` paulson@13134 ` 121` ```(*Kunen's Lemma 10.21*) ``` paulson@13615 ` 122` ```lemma cardinal_UN_le: ``` paulson@46820 ` 123` ``` "[| InfCard(K); \i\K. |X(i)| \ K |] ==> |\i\K. X(i)| \ K" ``` paulson@13134 ` 124` ```apply (simp add: InfCard_is_Card le_Card_iff) ``` paulson@13134 ` 125` ```apply (rule lepoll_trans) ``` paulson@13134 ` 126` ``` prefer 2 ``` paulson@13134 ` 127` ``` apply (rule InfCard_square_eq [THEN eqpoll_imp_lepoll]) ``` paulson@13134 ` 128` ``` apply (simp add: InfCard_is_Card Card_cardinal_eq) ``` paulson@13134 ` 129` ```apply (unfold lepoll_def) ``` paulson@13134 ` 130` ```apply (frule InfCard_is_Card [THEN Card_is_Ord]) ``` paulson@13134 ` 131` ```apply (erule AC_ball_Pi [THEN exE]) ``` paulson@13134 ` 132` ```apply (rule exI) ``` paulson@13134 ` 133` ```(*Lemma needed in both subgoals, for a fixed z*) ``` paulson@46820 ` 134` ```apply (subgoal_tac "\z\(\i\K. X (i)). z: X (LEAST i. z:X (i)) & ``` paulson@46820 ` 135` ``` (LEAST i. z:X (i)) \ K") ``` paulson@13134 ` 136` ``` prefer 2 ``` paulson@13134 ` 137` ``` apply (fast intro!: Least_le [THEN lt_trans1, THEN ltD] ltI ``` paulson@13134 ` 138` ``` elim!: LeastI Ord_in_Ord) ``` paulson@46820 ` 139` ```apply (rule_tac c = "%z. " ``` paulson@13134 ` 140` ``` and d = "%. converse (f`i) ` j" in lam_injective) ``` paulson@13134 ` 141` ```(*Instantiate the lemma proved above*) ``` paulson@13269 ` 142` ```by (blast intro: inj_is_fun [THEN apply_type] dest: apply_type, force) ``` paulson@13134 ` 143` paulson@13134 ` 144` paulson@13134 ` 145` ```(*The same again, using csucc*) ``` paulson@13134 ` 146` ```lemma cardinal_UN_lt_csucc: ``` paulson@46820 ` 147` ``` "[| InfCard(K); \i\K. |X(i)| < csucc(K) |] ``` paulson@13615 ` 148` ``` ==> |\i\K. X(i)| < csucc(K)" ``` paulson@13615 ` 149` ```by (simp add: Card_lt_csucc_iff cardinal_UN_le InfCard_is_Card Card_cardinal) ``` paulson@13134 ` 150` paulson@13134 ` 151` ```(*The same again, for a union of ordinals. In use, j(i) is a bit like rank(i), ``` paulson@13134 ` 152` ``` the least ordinal j such that i:Vfrom(A,j). *) ``` paulson@13134 ` 153` ```lemma cardinal_UN_Ord_lt_csucc: ``` paulson@46820 ` 154` ``` "[| InfCard(K); \i\K. j(i) < csucc(K) |] ``` paulson@13615 ` 155` ``` ==> (\i\K. j(i)) < csucc(K)" ``` paulson@13269 ` 156` ```apply (rule cardinal_UN_lt_csucc [THEN Card_lt_imp_lt], assumption) ``` paulson@13134 ` 157` ```apply (blast intro: Ord_cardinal_le [THEN lt_trans1] elim: ltE) ``` paulson@13134 ` 158` ```apply (blast intro!: Ord_UN elim: ltE) ``` paulson@13134 ` 159` ```apply (erule InfCard_is_Card [THEN Card_is_Ord, THEN Card_csucc]) ``` paulson@13134 ` 160` ```done ``` paulson@13134 ` 161` paulson@13134 ` 162` paulson@13134 ` 163` ```(** Main result for infinite-branching datatypes. As above, but the index ``` paulson@13134 ` 164` ``` set need not be a cardinal. Surprisingly complicated proof! ``` paulson@13134 ` 165` ```**) ``` paulson@13134 ` 166` paulson@46820 ` 167` ```(*Work backwards along the injection from W into K, given that @{term"W\0"}.*) ``` paulson@13134 ` 168` ```lemma inj_UN_subset: ``` paulson@46820 ` 169` ``` "[| f: inj(A,B); a:A |] ==> ``` paulson@46820 ` 170` ``` (\x\A. C(x)) \ (\y\B. C(if y: range(f) then converse(f)`y else a))" ``` paulson@13134 ` 171` ```apply (rule UN_least) ``` paulson@13134 ` 172` ```apply (rule_tac x1= "f`x" in subset_trans [OF _ UN_upper]) ``` paulson@13134 ` 173` ``` apply (simp add: inj_is_fun [THEN apply_rangeI]) ``` paulson@13134 ` 174` ```apply (blast intro: inj_is_fun [THEN apply_type]) ``` paulson@13134 ` 175` ```done ``` paulson@13134 ` 176` paulson@13134 ` 177` ```(*Simpler to require |W|=K; we'd have a bijection; but the theorem would ``` paulson@13134 ` 178` ``` be weaker.*) ``` paulson@13134 ` 179` ```lemma le_UN_Ord_lt_csucc: ``` paulson@46820 ` 180` ``` "[| InfCard(K); |W| \ K; \w\W. j(w) < csucc(K) |] ``` paulson@13615 ` 181` ``` ==> (\w\W. j(w)) < csucc(K)" ``` paulson@13134 ` 182` ```apply (case_tac "W=0") ``` paulson@13134 ` 183` ```(*solve the easy 0 case*) ``` paulson@46820 ` 184` ``` apply (simp add: InfCard_is_Card Card_is_Ord [THEN Card_csucc] ``` paulson@13134 ` 185` ``` Card_is_Ord Ord_0_lt_csucc) ``` paulson@13134 ` 186` ```apply (simp add: InfCard_is_Card le_Card_iff lepoll_def) ``` paulson@13134 ` 187` ```apply (safe intro!: equalityI) ``` paulson@46820 ` 188` ```apply (erule swap) ``` paulson@13269 ` 189` ```apply (rule lt_subset_trans [OF inj_UN_subset cardinal_UN_Ord_lt_csucc], assumption+) ``` paulson@13134 ` 190` ``` apply (simp add: inj_converse_fun [THEN apply_type]) ``` paulson@13134 ` 191` ```apply (blast intro!: Ord_UN elim: ltE) ``` paulson@13134 ` 192` ```done ``` paulson@13134 ` 193` paulson@13134 ` 194` ```end ```