src/ZF/Cardinal.thy
 author wenzelm Mon Dec 04 22:54:31 2017 +0100 (20 months ago) changeset 67131 85d10959c2e4 parent 61798 27f3c10b0b50 child 67443 3abf6a722518 permissions -rw-r--r--
tuned signature;
 clasohm@1478 ` 1` ```(* Title: ZF/Cardinal.thy ``` clasohm@1478 ` 2` ``` Author: Lawrence C Paulson, Cambridge University Computer Laboratory ``` lcp@435 ` 3` ``` Copyright 1994 University of Cambridge ``` paulson@13328 ` 4` ```*) ``` paulson@13221 ` 5` wenzelm@60770 ` 6` ```section\Cardinal Numbers Without the Axiom of Choice\ ``` lcp@435 ` 7` krauss@26056 ` 8` ```theory Cardinal imports OrderType Finite Nat_ZF Sum begin ``` paulson@13221 ` 9` wenzelm@24893 ` 10` ```definition ``` lcp@435 ` 11` ``` (*least ordinal operator*) ``` wenzelm@61394 ` 12` ``` Least :: "(i=>o) => i" (binder "\ " 10) where ``` paulson@46820 ` 13` ``` "Least(P) == THE i. Ord(i) & P(i) & (\j. j ~P(j))" ``` lcp@435 ` 14` wenzelm@24893 ` 15` ```definition ``` wenzelm@61394 ` 16` ``` eqpoll :: "[i,i] => o" (infixl "\" 50) where ``` wenzelm@61394 ` 17` ``` "A \ B == \f. f \ bij(A,B)" ``` lcp@435 ` 18` wenzelm@24893 ` 19` ```definition ``` wenzelm@61394 ` 20` ``` lepoll :: "[i,i] => o" (infixl "\" 50) where ``` wenzelm@61394 ` 21` ``` "A \ B == \f. f \ inj(A,B)" ``` lcp@435 ` 22` wenzelm@24893 ` 23` ```definition ``` wenzelm@61394 ` 24` ``` lesspoll :: "[i,i] => o" (infixl "\" 50) where ``` wenzelm@61394 ` 25` ``` "A \ B == A \ B & ~(A \ B)" ``` lcp@832 ` 26` wenzelm@24893 ` 27` ```definition ``` wenzelm@24893 ` 28` ``` cardinal :: "i=>i" ("|_|") where ``` wenzelm@61394 ` 29` ``` "|A| == (\ i. i \ A)" ``` lcp@435 ` 30` wenzelm@24893 ` 31` ```definition ``` wenzelm@24893 ` 32` ``` Finite :: "i=>o" where ``` wenzelm@61394 ` 33` ``` "Finite(A) == \n\nat. A \ n" ``` lcp@435 ` 34` wenzelm@24893 ` 35` ```definition ``` wenzelm@24893 ` 36` ``` Card :: "i=>o" where ``` paulson@13221 ` 37` ``` "Card(i) == (i = |i|)" ``` lcp@435 ` 38` kleing@14565 ` 39` wenzelm@60770 ` 40` ```subsection\The Schroeder-Bernstein Theorem\ ``` wenzelm@60770 ` 41` ```text\See Davey and Priestly, page 106\ ``` paulson@13221 ` 42` paulson@13221 ` 43` ```(** Lemma: Banach's Decomposition Theorem **) ``` paulson@13221 ` 44` paulson@13221 ` 45` ```lemma decomp_bnd_mono: "bnd_mono(X, %W. X - g``(Y - f``W))" ``` paulson@13221 ` 46` ```by (rule bnd_monoI, blast+) ``` paulson@13221 ` 47` paulson@13221 ` 48` ```lemma Banach_last_equation: ``` paulson@46953 ` 49` ``` "g \ Y->X ``` paulson@46820 ` 50` ``` ==> g``(Y - f`` lfp(X, %W. X - g``(Y - f``W))) = ``` paulson@46820 ` 51` ``` X - lfp(X, %W. X - g``(Y - f``W))" ``` wenzelm@59788 ` 52` ```apply (rule_tac P = "%u. v = X-u" for v ``` paulson@13221 ` 53` ``` in decomp_bnd_mono [THEN lfp_unfold, THEN ssubst]) ``` paulson@13221 ` 54` ```apply (simp add: double_complement fun_is_rel [THEN image_subset]) ``` paulson@13221 ` 55` ```done ``` paulson@13221 ` 56` paulson@13221 ` 57` ```lemma decomposition: ``` paulson@46953 ` 58` ``` "[| f \ X->Y; g \ Y->X |] ==> ``` paulson@46820 ` 59` ``` \XA XB YA YB. (XA \ XB = 0) & (XA \ XB = X) & ``` paulson@46820 ` 60` ``` (YA \ YB = 0) & (YA \ YB = Y) & ``` paulson@13221 ` 61` ``` f``XA=YA & g``YB=XB" ``` paulson@13221 ` 62` ```apply (intro exI conjI) ``` paulson@13221 ` 63` ```apply (rule_tac [6] Banach_last_equation) ``` paulson@13221 ` 64` ```apply (rule_tac [5] refl) ``` paulson@46820 ` 65` ```apply (assumption | ``` paulson@13221 ` 66` ``` rule Diff_disjoint Diff_partition fun_is_rel image_subset lfp_subset)+ ``` paulson@13221 ` 67` ```done ``` paulson@13221 ` 68` paulson@13221 ` 69` ```lemma schroeder_bernstein: ``` paulson@46953 ` 70` ``` "[| f \ inj(X,Y); g \ inj(Y,X) |] ==> \h. h \ bij(X,Y)" ``` paulson@46820 ` 71` ```apply (insert decomposition [of f X Y g]) ``` paulson@13221 ` 72` ```apply (simp add: inj_is_fun) ``` paulson@13221 ` 73` ```apply (blast intro!: restrict_bij bij_disjoint_Un intro: bij_converse_bij) ``` paulson@46820 ` 74` ```(* The instantiation of exI to @{term"restrict(f,XA) \ converse(restrict(g,YB))"} ``` paulson@13221 ` 75` ``` is forced by the context!! *) ``` paulson@13221 ` 76` ```done ``` paulson@13221 ` 77` paulson@13221 ` 78` paulson@13221 ` 79` ```(** Equipollence is an equivalence relation **) ``` paulson@13221 ` 80` paulson@46953 ` 81` ```lemma bij_imp_eqpoll: "f \ bij(A,B) ==> A \ B" ``` paulson@13221 ` 82` ```apply (unfold eqpoll_def) ``` paulson@13221 ` 83` ```apply (erule exI) ``` paulson@13221 ` 84` ```done ``` paulson@13221 ` 85` wenzelm@61394 ` 86` ```(*A \ A*) ``` wenzelm@45602 ` 87` ```lemmas eqpoll_refl = id_bij [THEN bij_imp_eqpoll, simp] ``` paulson@13221 ` 88` paulson@13221 ` 89` ```lemma eqpoll_sym: "X \ Y ==> Y \ X" ``` paulson@13221 ` 90` ```apply (unfold eqpoll_def) ``` paulson@13221 ` 91` ```apply (blast intro: bij_converse_bij) ``` paulson@13221 ` 92` ```done ``` paulson@13221 ` 93` paulson@46841 ` 94` ```lemma eqpoll_trans [trans]: ``` paulson@13221 ` 95` ``` "[| X \ Y; Y \ Z |] ==> X \ Z" ``` paulson@13221 ` 96` ```apply (unfold eqpoll_def) ``` paulson@13221 ` 97` ```apply (blast intro: comp_bij) ``` paulson@13221 ` 98` ```done ``` paulson@13221 ` 99` paulson@13221 ` 100` ```(** Le-pollence is a partial ordering **) ``` paulson@13221 ` 101` paulson@13221 ` 102` ```lemma subset_imp_lepoll: "X<=Y ==> X \ Y" ``` paulson@13221 ` 103` ```apply (unfold lepoll_def) ``` paulson@13221 ` 104` ```apply (rule exI) ``` paulson@13221 ` 105` ```apply (erule id_subset_inj) ``` paulson@13221 ` 106` ```done ``` paulson@13221 ` 107` wenzelm@45602 ` 108` ```lemmas lepoll_refl = subset_refl [THEN subset_imp_lepoll, simp] ``` paulson@13221 ` 109` wenzelm@45602 ` 110` ```lemmas le_imp_lepoll = le_imp_subset [THEN subset_imp_lepoll] ``` paulson@13221 ` 111` paulson@13221 ` 112` ```lemma eqpoll_imp_lepoll: "X \ Y ==> X \ Y" ``` paulson@13221 ` 113` ```by (unfold eqpoll_def bij_def lepoll_def, blast) ``` paulson@13221 ` 114` paulson@46841 ` 115` ```lemma lepoll_trans [trans]: "[| X \ Y; Y \ Z |] ==> X \ Z" ``` paulson@13221 ` 116` ```apply (unfold lepoll_def) ``` paulson@13221 ` 117` ```apply (blast intro: comp_inj) ``` paulson@13221 ` 118` ```done ``` paulson@13221 ` 119` paulson@46841 ` 120` ```lemma eq_lepoll_trans [trans]: "[| X \ Y; Y \ Z |] ==> X \ Z" ``` paulson@46953 ` 121` ``` by (blast intro: eqpoll_imp_lepoll lepoll_trans) ``` paulson@46841 ` 122` paulson@46841 ` 123` ```lemma lepoll_eq_trans [trans]: "[| X \ Y; Y \ Z |] ==> X \ Z" ``` paulson@46953 ` 124` ``` by (blast intro: eqpoll_imp_lepoll lepoll_trans) ``` paulson@46841 ` 125` paulson@13221 ` 126` ```(*Asymmetry law*) ``` paulson@13221 ` 127` ```lemma eqpollI: "[| X \ Y; Y \ X |] ==> X \ Y" ``` paulson@13221 ` 128` ```apply (unfold lepoll_def eqpoll_def) ``` paulson@13221 ` 129` ```apply (elim exE) ``` paulson@13221 ` 130` ```apply (rule schroeder_bernstein, assumption+) ``` paulson@13221 ` 131` ```done ``` paulson@13221 ` 132` paulson@13221 ` 133` ```lemma eqpollE: ``` paulson@13221 ` 134` ``` "[| X \ Y; [| X \ Y; Y \ X |] ==> P |] ==> P" ``` paulson@46820 ` 135` ```by (blast intro: eqpoll_imp_lepoll eqpoll_sym) ``` paulson@13221 ` 136` paulson@46821 ` 137` ```lemma eqpoll_iff: "X \ Y \ X \ Y & Y \ X" ``` paulson@13221 ` 138` ```by (blast intro: eqpollI elim!: eqpollE) ``` paulson@13221 ` 139` paulson@13221 ` 140` ```lemma lepoll_0_is_0: "A \ 0 ==> A = 0" ``` paulson@13221 ` 141` ```apply (unfold lepoll_def inj_def) ``` paulson@13221 ` 142` ```apply (blast dest: apply_type) ``` paulson@13221 ` 143` ```done ``` paulson@13221 ` 144` paulson@46820 ` 145` ```(*@{term"0 \ Y"}*) ``` wenzelm@45602 ` 146` ```lemmas empty_lepollI = empty_subsetI [THEN subset_imp_lepoll] ``` paulson@13221 ` 147` paulson@46821 ` 148` ```lemma lepoll_0_iff: "A \ 0 \ A=0" ``` paulson@13221 ` 149` ```by (blast intro: lepoll_0_is_0 lepoll_refl) ``` paulson@13221 ` 150` paulson@46820 ` 151` ```lemma Un_lepoll_Un: ``` paulson@46820 ` 152` ``` "[| A \ B; C \ D; B \ D = 0 |] ==> A \ C \ B \ D" ``` paulson@13221 ` 153` ```apply (unfold lepoll_def) ``` paulson@13221 ` 154` ```apply (blast intro: inj_disjoint_Un) ``` paulson@13221 ` 155` ```done ``` paulson@13221 ` 156` wenzelm@61394 ` 157` ```(*A \ 0 ==> A=0*) ``` wenzelm@45602 ` 158` ```lemmas eqpoll_0_is_0 = eqpoll_imp_lepoll [THEN lepoll_0_is_0] ``` paulson@13221 ` 159` paulson@46821 ` 160` ```lemma eqpoll_0_iff: "A \ 0 \ A=0" ``` paulson@13221 ` 161` ```by (blast intro: eqpoll_0_is_0 eqpoll_refl) ``` paulson@13221 ` 162` paulson@46820 ` 163` ```lemma eqpoll_disjoint_Un: ``` paulson@46820 ` 164` ``` "[| A \ B; C \ D; A \ C = 0; B \ D = 0 |] ``` paulson@46820 ` 165` ``` ==> A \ C \ B \ D" ``` paulson@13221 ` 166` ```apply (unfold eqpoll_def) ``` paulson@13221 ` 167` ```apply (blast intro: bij_disjoint_Un) ``` paulson@13221 ` 168` ```done ``` paulson@13221 ` 169` paulson@13221 ` 170` wenzelm@60770 ` 171` ```subsection\lesspoll: contributions by Krzysztof Grabczewski\ ``` paulson@13221 ` 172` paulson@13221 ` 173` ```lemma lesspoll_not_refl: "~ (i \ i)" ``` paulson@46820 ` 174` ```by (simp add: lesspoll_def) ``` paulson@13221 ` 175` paulson@13221 ` 176` ```lemma lesspoll_irrefl [elim!]: "i \ i ==> P" ``` paulson@46820 ` 177` ```by (simp add: lesspoll_def) ``` paulson@13221 ` 178` paulson@13221 ` 179` ```lemma lesspoll_imp_lepoll: "A \ B ==> A \ B" ``` paulson@13221 ` 180` ```by (unfold lesspoll_def, blast) ``` paulson@13221 ` 181` paulson@46820 ` 182` ```lemma lepoll_well_ord: "[| A \ B; well_ord(B,r) |] ==> \s. well_ord(A,s)" ``` paulson@13221 ` 183` ```apply (unfold lepoll_def) ``` paulson@13221 ` 184` ```apply (blast intro: well_ord_rvimage) ``` paulson@13221 ` 185` ```done ``` paulson@13221 ` 186` paulson@46821 ` 187` ```lemma lepoll_iff_leqpoll: "A \ B \ A \ B | A \ B" ``` paulson@13221 ` 188` ```apply (unfold lesspoll_def) ``` paulson@13221 ` 189` ```apply (blast intro!: eqpollI elim!: eqpollE) ``` paulson@13221 ` 190` ```done ``` paulson@13221 ` 191` paulson@46820 ` 192` ```lemma inj_not_surj_succ: ``` paulson@47042 ` 193` ``` assumes fi: "f \ inj(A, succ(m))" and fns: "f \ surj(A, succ(m))" ``` paulson@47042 ` 194` ``` shows "\f. f \ inj(A,m)" ``` paulson@47042 ` 195` ```proof - ``` paulson@47042 ` 196` ``` from fi [THEN inj_is_fun] fns ``` paulson@47042 ` 197` ``` obtain y where y: "y \ succ(m)" "\x. x\A \ f ` x \ y" ``` paulson@47042 ` 198` ``` by (auto simp add: surj_def) ``` paulson@47042 ` 199` ``` show ?thesis ``` paulson@47042 ` 200` ``` proof ``` paulson@47042 ` 201` ``` show "(\z\A. if f`z = m then y else f`z) \ inj(A, m)" using y fi ``` paulson@47042 ` 202` ``` by (simp add: inj_def) ``` paulson@47042 ` 203` ``` (auto intro!: if_type [THEN lam_type] intro: Pi_type dest: apply_funtype) ``` paulson@47042 ` 204` ``` qed ``` paulson@47042 ` 205` ```qed ``` paulson@13221 ` 206` paulson@13221 ` 207` ```(** Variations on transitivity **) ``` paulson@13221 ` 208` paulson@46841 ` 209` ```lemma lesspoll_trans [trans]: ``` paulson@13221 ` 210` ``` "[| X \ Y; Y \ Z |] ==> X \ Z" ``` paulson@13221 ` 211` ```apply (unfold lesspoll_def) ``` paulson@13221 ` 212` ```apply (blast elim!: eqpollE intro: eqpollI lepoll_trans) ``` paulson@13221 ` 213` ```done ``` paulson@13221 ` 214` paulson@46841 ` 215` ```lemma lesspoll_trans1 [trans]: ``` paulson@13221 ` 216` ``` "[| X \ Y; Y \ Z |] ==> X \ Z" ``` paulson@13221 ` 217` ```apply (unfold lesspoll_def) ``` paulson@13221 ` 218` ```apply (blast elim!: eqpollE intro: eqpollI lepoll_trans) ``` paulson@13221 ` 219` ```done ``` paulson@13221 ` 220` paulson@46841 ` 221` ```lemma lesspoll_trans2 [trans]: ``` paulson@13221 ` 222` ``` "[| X \ Y; Y \ Z |] ==> X \ Z" ``` paulson@13221 ` 223` ```apply (unfold lesspoll_def) ``` paulson@13221 ` 224` ```apply (blast elim!: eqpollE intro: eqpollI lepoll_trans) ``` paulson@13221 ` 225` ```done ``` paulson@13221 ` 226` paulson@46841 ` 227` ```lemma eq_lesspoll_trans [trans]: ``` paulson@46841 ` 228` ``` "[| X \ Y; Y \ Z |] ==> X \ Z" ``` paulson@46953 ` 229` ``` by (blast intro: eqpoll_imp_lepoll lesspoll_trans1) ``` paulson@46841 ` 230` paulson@46841 ` 231` ```lemma lesspoll_eq_trans [trans]: ``` paulson@46841 ` 232` ``` "[| X \ Y; Y \ Z |] ==> X \ Z" ``` paulson@46953 ` 233` ``` by (blast intro: eqpoll_imp_lepoll lesspoll_trans2) ``` paulson@46841 ` 234` paulson@13221 ` 235` wenzelm@61394 ` 236` ```(** \ -- the least number operator [from HOL/Univ.ML] **) ``` paulson@13221 ` 237` paulson@46820 ` 238` ```lemma Least_equality: ``` paulson@46847 ` 239` ``` "[| P(i); Ord(i); !!x. x ~P(x) |] ==> (\ x. P(x)) = i" ``` paulson@46820 ` 240` ```apply (unfold Least_def) ``` paulson@13221 ` 241` ```apply (rule the_equality, blast) ``` paulson@13221 ` 242` ```apply (elim conjE) ``` paulson@13221 ` 243` ```apply (erule Ord_linear_lt, assumption, blast+) ``` paulson@13221 ` 244` ```done ``` paulson@13221 ` 245` paulson@47016 ` 246` ```lemma LeastI: ``` paulson@47016 ` 247` ``` assumes P: "P(i)" and i: "Ord(i)" shows "P(\ x. P(x))" ``` paulson@47016 ` 248` ```proof - ``` paulson@47016 ` 249` ``` { from i have "P(i) \ P(\ x. P(x))" ``` paulson@47016 ` 250` ``` proof (induct i rule: trans_induct) ``` paulson@47016 ` 251` ``` case (step i) ``` paulson@47016 ` 252` ``` show ?case ``` paulson@47016 ` 253` ``` proof (cases "P(\ a. P(a))") ``` paulson@47016 ` 254` ``` case True thus ?thesis . ``` paulson@47016 ` 255` ``` next ``` paulson@47016 ` 256` ``` case False ``` paulson@47016 ` 257` ``` hence "\x. x \ i \ ~P(x)" using step ``` paulson@47016 ` 258` ``` by blast ``` paulson@47018 ` 259` ``` hence "(\ a. P(a)) = i" using step ``` paulson@47018 ` 260` ``` by (blast intro: Least_equality ltD) ``` paulson@47018 ` 261` ``` thus ?thesis using step.prems ``` paulson@47016 ` 262` ``` by simp ``` paulson@47016 ` 263` ``` qed ``` paulson@47016 ` 264` ``` qed ``` paulson@47016 ` 265` ``` } ``` paulson@47016 ` 266` ``` thus ?thesis using P . ``` paulson@47016 ` 267` ```qed ``` paulson@13221 ` 268` wenzelm@60770 ` 269` ```text\The proof is almost identical to the one above!\ ``` paulson@47018 ` 270` ```lemma Least_le: ``` paulson@47018 ` 271` ``` assumes P: "P(i)" and i: "Ord(i)" shows "(\ x. P(x)) \ i" ``` paulson@47018 ` 272` ```proof - ``` paulson@47018 ` 273` ``` { from i have "P(i) \ (\ x. P(x)) \ i" ``` paulson@47018 ` 274` ``` proof (induct i rule: trans_induct) ``` paulson@47018 ` 275` ``` case (step i) ``` paulson@47018 ` 276` ``` show ?case ``` paulson@47018 ` 277` ``` proof (cases "(\ a. P(a)) \ i") ``` paulson@47018 ` 278` ``` case True thus ?thesis . ``` paulson@47018 ` 279` ``` next ``` paulson@47018 ` 280` ``` case False ``` paulson@47018 ` 281` ``` hence "\x. x \ i \ ~ (\ a. P(a)) \ i" using step ``` paulson@47018 ` 282` ``` by blast ``` paulson@47018 ` 283` ``` hence "(\ a. P(a)) = i" using step ``` paulson@47018 ` 284` ``` by (blast elim: ltE intro: ltI Least_equality lt_trans1) ``` paulson@47018 ` 285` ``` thus ?thesis using step ``` paulson@47018 ` 286` ``` by simp ``` paulson@47018 ` 287` ``` qed ``` paulson@47018 ` 288` ``` qed ``` paulson@47018 ` 289` ``` } ``` paulson@47018 ` 290` ``` thus ?thesis using P . ``` paulson@47018 ` 291` ```qed ``` paulson@13221 ` 292` wenzelm@61394 ` 293` ```(*\ really is the smallest*) ``` paulson@46847 ` 294` ```lemma less_LeastE: "[| P(i); i < (\ x. P(x)) |] ==> Q" ``` paulson@13221 ` 295` ```apply (rule Least_le [THEN [2] lt_trans2, THEN lt_irrefl], assumption+) ``` paulson@46820 ` 296` ```apply (simp add: lt_Ord) ``` paulson@13221 ` 297` ```done ``` paulson@13221 ` 298` paulson@13221 ` 299` ```(*Easier to apply than LeastI: conclusion has only one occurrence of P*) ``` paulson@13221 ` 300` ```lemma LeastI2: ``` paulson@46847 ` 301` ``` "[| P(i); Ord(i); !!j. P(j) ==> Q(j) |] ==> Q(\ j. P(j))" ``` paulson@46820 ` 302` ```by (blast intro: LeastI ) ``` paulson@13221 ` 303` wenzelm@61394 ` 304` ```(*If there is no such P then \ is vacuously 0*) ``` paulson@46820 ` 305` ```lemma Least_0: ``` paulson@46847 ` 306` ``` "[| ~ (\i. Ord(i) & P(i)) |] ==> (\ x. P(x)) = 0" ``` paulson@13221 ` 307` ```apply (unfold Least_def) ``` paulson@13221 ` 308` ```apply (rule the_0, blast) ``` paulson@13221 ` 309` ```done ``` paulson@13221 ` 310` paulson@46847 ` 311` ```lemma Ord_Least [intro,simp,TC]: "Ord(\ x. P(x))" ``` paulson@47042 ` 312` ```proof (cases "\i. Ord(i) & P(i)") ``` paulson@47042 ` 313` ``` case True ``` paulson@47042 ` 314` ``` then obtain i where "P(i)" "Ord(i)" by auto ``` paulson@47042 ` 315` ``` hence " (\ x. P(x)) \ i" by (rule Least_le) ``` paulson@47042 ` 316` ``` thus ?thesis ``` paulson@47042 ` 317` ``` by (elim ltE) ``` paulson@47042 ` 318` ```next ``` paulson@47042 ` 319` ``` case False ``` paulson@47042 ` 320` ``` hence "(\ x. P(x)) = 0" by (rule Least_0) ``` paulson@47042 ` 321` ``` thus ?thesis ``` paulson@47042 ` 322` ``` by auto ``` paulson@47042 ` 323` ```qed ``` paulson@13221 ` 324` paulson@13221 ` 325` wenzelm@60770 ` 326` ```subsection\Basic Properties of Cardinals\ ``` paulson@13221 ` 327` paulson@13221 ` 328` ```(*Not needed for simplification, but helpful below*) ``` paulson@46847 ` 329` ```lemma Least_cong: "(!!y. P(y) \ Q(y)) ==> (\ x. P(x)) = (\ x. Q(x))" ``` paulson@13221 ` 330` ```by simp ``` paulson@13221 ` 331` paulson@46820 ` 332` ```(*Need AC to get @{term"X \ Y ==> |X| \ |Y|"}; see well_ord_lepoll_imp_Card_le ``` paulson@13221 ` 333` ``` Converse also requires AC, but see well_ord_cardinal_eqE*) ``` paulson@13221 ` 334` ```lemma cardinal_cong: "X \ Y ==> |X| = |Y|" ``` paulson@13221 ` 335` ```apply (unfold eqpoll_def cardinal_def) ``` paulson@13221 ` 336` ```apply (rule Least_cong) ``` paulson@13221 ` 337` ```apply (blast intro: comp_bij bij_converse_bij) ``` paulson@13221 ` 338` ```done ``` paulson@13221 ` 339` paulson@13221 ` 340` ```(*Under AC, the premise becomes trivial; one consequence is ||A|| = |A|*) ``` paulson@46820 ` 341` ```lemma well_ord_cardinal_eqpoll: ``` paulson@47018 ` 342` ``` assumes r: "well_ord(A,r)" shows "|A| \ A" ``` paulson@47018 ` 343` ```proof (unfold cardinal_def) ``` paulson@47018 ` 344` ``` show "(\ i. i \ A) \ A" ``` paulson@47018 ` 345` ``` by (best intro: LeastI Ord_ordertype ordermap_bij bij_converse_bij bij_imp_eqpoll r) ``` paulson@47018 ` 346` ```qed ``` paulson@13221 ` 347` paulson@46820 ` 348` ```(* @{term"Ord(A) ==> |A| \ A"} *) ``` paulson@13221 ` 349` ```lemmas Ord_cardinal_eqpoll = well_ord_Memrel [THEN well_ord_cardinal_eqpoll] ``` paulson@13221 ` 350` paulson@46841 ` 351` ```lemma Ord_cardinal_idem: "Ord(A) \ ||A|| = |A|" ``` paulson@46841 ` 352` ``` by (rule Ord_cardinal_eqpoll [THEN cardinal_cong]) ``` paulson@46841 ` 353` paulson@13221 ` 354` ```lemma well_ord_cardinal_eqE: ``` paulson@46953 ` 355` ``` assumes woX: "well_ord(X,r)" and woY: "well_ord(Y,s)" and eq: "|X| = |Y|" ``` paulson@46847 ` 356` ```shows "X \ Y" ``` paulson@46847 ` 357` ```proof - ``` paulson@46953 ` 358` ``` have "X \ |X|" by (blast intro: well_ord_cardinal_eqpoll [OF woX] eqpoll_sym) ``` paulson@46847 ` 359` ``` also have "... = |Y|" by (rule eq) ``` paulson@46953 ` 360` ``` also have "... \ Y" by (rule well_ord_cardinal_eqpoll [OF woY]) ``` paulson@46847 ` 361` ``` finally show ?thesis . ``` paulson@46847 ` 362` ```qed ``` paulson@13221 ` 363` paulson@13221 ` 364` ```lemma well_ord_cardinal_eqpoll_iff: ``` paulson@46821 ` 365` ``` "[| well_ord(X,r); well_ord(Y,s) |] ==> |X| = |Y| \ X \ Y" ``` paulson@13221 ` 366` ```by (blast intro: cardinal_cong well_ord_cardinal_eqE) ``` paulson@13221 ` 367` paulson@13221 ` 368` paulson@13221 ` 369` ```(** Observations from Kunen, page 28 **) ``` paulson@13221 ` 370` paulson@46820 ` 371` ```lemma Ord_cardinal_le: "Ord(i) ==> |i| \ i" ``` paulson@13221 ` 372` ```apply (unfold cardinal_def) ``` paulson@13221 ` 373` ```apply (erule eqpoll_refl [THEN Least_le]) ``` paulson@13221 ` 374` ```done ``` paulson@13221 ` 375` paulson@13221 ` 376` ```lemma Card_cardinal_eq: "Card(K) ==> |K| = K" ``` paulson@13221 ` 377` ```apply (unfold Card_def) ``` paulson@13221 ` 378` ```apply (erule sym) ``` paulson@13221 ` 379` ```done ``` paulson@13221 ` 380` paulson@46841 ` 381` ```(* Could replace the @{term"~(j \ i)"} by @{term"~(i \ j)"}. *) ``` paulson@13221 ` 382` ```lemma CardI: "[| Ord(i); !!j. j ~(j \ i) |] ==> Card(i)" ``` paulson@46820 ` 383` ```apply (unfold Card_def cardinal_def) ``` paulson@13221 ` 384` ```apply (subst Least_equality) ``` paulson@47018 ` 385` ```apply (blast intro: eqpoll_refl)+ ``` paulson@13221 ` 386` ```done ``` paulson@13221 ` 387` paulson@13221 ` 388` ```lemma Card_is_Ord: "Card(i) ==> Ord(i)" ``` paulson@13221 ` 389` ```apply (unfold Card_def cardinal_def) ``` paulson@13221 ` 390` ```apply (erule ssubst) ``` paulson@13221 ` 391` ```apply (rule Ord_Least) ``` paulson@13221 ` 392` ```done ``` paulson@13221 ` 393` paulson@46820 ` 394` ```lemma Card_cardinal_le: "Card(K) ==> K \ |K|" ``` paulson@13221 ` 395` ```apply (simp (no_asm_simp) add: Card_is_Ord Card_cardinal_eq) ``` paulson@13221 ` 396` ```done ``` paulson@13221 ` 397` paulson@13221 ` 398` ```lemma Ord_cardinal [simp,intro!]: "Ord(|A|)" ``` paulson@13221 ` 399` ```apply (unfold cardinal_def) ``` paulson@13221 ` 400` ```apply (rule Ord_Least) ``` paulson@13221 ` 401` ```done ``` paulson@13221 ` 402` wenzelm@60770 ` 403` ```text\The cardinals are the initial ordinals.\ ``` paulson@46821 ` 404` ```lemma Card_iff_initial: "Card(K) \ Ord(K) & (\j. j ~ j \ K)" ``` paulson@47018 ` 405` ```proof - ``` paulson@47018 ` 406` ``` { fix j ``` paulson@47018 ` 407` ``` assume K: "Card(K)" "j \ K" ``` paulson@47018 ` 408` ``` assume "j < K" ``` paulson@47018 ` 409` ``` also have "... = (\ i. i \ K)" using K ``` paulson@47018 ` 410` ``` by (simp add: Card_def cardinal_def) ``` paulson@47018 ` 411` ``` finally have "j < (\ i. i \ K)" . ``` paulson@47018 ` 412` ``` hence "False" using K ``` paulson@47018 ` 413` ``` by (best dest: less_LeastE) ``` paulson@47018 ` 414` ``` } ``` paulson@47018 ` 415` ``` then show ?thesis ``` paulson@47042 ` 416` ``` by (blast intro: CardI Card_is_Ord) ``` paulson@47018 ` 417` ```qed ``` paulson@13221 ` 418` paulson@13221 ` 419` ```lemma lt_Card_imp_lesspoll: "[| Card(a); i i \ a" ``` paulson@13221 ` 420` ```apply (unfold lesspoll_def) ``` paulson@13221 ` 421` ```apply (drule Card_iff_initial [THEN iffD1]) ``` paulson@13221 ` 422` ```apply (blast intro!: leI [THEN le_imp_lepoll]) ``` paulson@13221 ` 423` ```done ``` paulson@13221 ` 424` paulson@13221 ` 425` ```lemma Card_0: "Card(0)" ``` paulson@13221 ` 426` ```apply (rule Ord_0 [THEN CardI]) ``` paulson@13221 ` 427` ```apply (blast elim!: ltE) ``` paulson@13221 ` 428` ```done ``` paulson@13221 ` 429` paulson@46820 ` 430` ```lemma Card_Un: "[| Card(K); Card(L) |] ==> Card(K \ L)" ``` paulson@13221 ` 431` ```apply (rule Ord_linear_le [of K L]) ``` paulson@13221 ` 432` ```apply (simp_all add: subset_Un_iff [THEN iffD1] Card_is_Ord le_imp_subset ``` paulson@13221 ` 433` ``` subset_Un_iff2 [THEN iffD1]) ``` paulson@13221 ` 434` ```done ``` paulson@13221 ` 435` paulson@13221 ` 436` ```(*Infinite unions of cardinals? See Devlin, Lemma 6.7, page 98*) ``` paulson@13221 ` 437` paulson@47101 ` 438` ```lemma Card_cardinal [iff]: "Card(|A|)" ``` paulson@46847 ` 439` ```proof (unfold cardinal_def) ``` paulson@46847 ` 440` ``` show "Card(\ i. i \ A)" ``` paulson@46847 ` 441` ``` proof (cases "\i. Ord (i) & i \ A") ``` wenzelm@61798 ` 442` ``` case False thus ?thesis \\degenerate case\ ``` paulson@46847 ` 443` ``` by (simp add: Least_0 Card_0) ``` paulson@46847 ` 444` ``` next ``` wenzelm@61798 ` 445` ``` case True \\real case: @{term A} is isomorphic to some ordinal\ ``` paulson@46847 ` 446` ``` then obtain i where i: "Ord(i)" "i \ A" by blast ``` paulson@46953 ` 447` ``` show ?thesis ``` paulson@46847 ` 448` ``` proof (rule CardI [OF Ord_Least], rule notI) ``` paulson@46847 ` 449` ``` fix j ``` paulson@46953 ` 450` ``` assume j: "j < (\ i. i \ A)" ``` paulson@46847 ` 451` ``` assume "j \ (\ i. i \ A)" ``` paulson@46847 ` 452` ``` also have "... \ A" using i by (auto intro: LeastI) ``` paulson@46847 ` 453` ``` finally have "j \ A" . ``` paulson@46953 ` 454` ``` thus False ``` paulson@46847 ` 455` ``` by (rule less_LeastE [OF _ j]) ``` paulson@46847 ` 456` ``` qed ``` paulson@46847 ` 457` ``` qed ``` paulson@46847 ` 458` ```qed ``` paulson@13221 ` 459` paulson@13221 ` 460` ```(*Kunen's Lemma 10.5*) ``` paulson@46953 ` 461` ```lemma cardinal_eq_lemma: ``` paulson@46841 ` 462` ``` assumes i:"|i| \ j" and j: "j \ i" shows "|j| = |i|" ``` paulson@46841 ` 463` ```proof (rule eqpollI [THEN cardinal_cong]) ``` paulson@46841 ` 464` ``` show "j \ i" by (rule le_imp_lepoll [OF j]) ``` paulson@46841 ` 465` ```next ``` paulson@46841 ` 466` ``` have Oi: "Ord(i)" using j by (rule le_Ord2) ``` paulson@46953 ` 467` ``` hence "i \ |i|" ``` paulson@46953 ` 468` ``` by (blast intro: Ord_cardinal_eqpoll eqpoll_sym) ``` paulson@46953 ` 469` ``` also have "... \ j" ``` paulson@46953 ` 470` ``` by (blast intro: le_imp_lepoll i) ``` paulson@46841 ` 471` ``` finally show "i \ j" . ``` paulson@46841 ` 472` ```qed ``` paulson@13221 ` 473` paulson@46953 ` 474` ```lemma cardinal_mono: ``` paulson@46877 ` 475` ``` assumes ij: "i \ j" shows "|i| \ |j|" ``` paulson@47016 ` 476` ```using Ord_cardinal [of i] Ord_cardinal [of j] ``` paulson@47016 ` 477` ```proof (cases rule: Ord_linear_le) ``` paulson@47016 ` 478` ``` case le thus ?thesis . ``` paulson@46877 ` 479` ```next ``` paulson@47016 ` 480` ``` case ge ``` paulson@46877 ` 481` ``` have i: "Ord(i)" using ij ``` paulson@46953 ` 482` ``` by (simp add: lt_Ord) ``` paulson@46953 ` 483` ``` have ci: "|i| \ j" ``` paulson@46953 ` 484` ``` by (blast intro: Ord_cardinal_le ij le_trans i) ``` paulson@46953 ` 485` ``` have "|i| = ||i||" ``` paulson@46953 ` 486` ``` by (auto simp add: Ord_cardinal_idem i) ``` paulson@46877 ` 487` ``` also have "... = |j|" ``` paulson@47016 ` 488` ``` by (rule cardinal_eq_lemma [OF ge ci]) ``` paulson@46877 ` 489` ``` finally have "|i| = |j|" . ``` paulson@46877 ` 490` ``` thus ?thesis by simp ``` paulson@46877 ` 491` ```qed ``` paulson@13221 ` 492` wenzelm@61798 ` 493` ```text\Since we have @{term"|succ(nat)| \ |nat|"}, the converse of \cardinal_mono\ fails!\ ``` paulson@13221 ` 494` ```lemma cardinal_lt_imp_lt: "[| |i| < |j|; Ord(i); Ord(j) |] ==> i < j" ``` paulson@13221 ` 495` ```apply (rule Ord_linear2 [of i j], assumption+) ``` paulson@13221 ` 496` ```apply (erule lt_trans2 [THEN lt_irrefl]) ``` paulson@13221 ` 497` ```apply (erule cardinal_mono) ``` paulson@13221 ` 498` ```done ``` paulson@13221 ` 499` paulson@13221 ` 500` ```lemma Card_lt_imp_lt: "[| |i| < K; Ord(i); Card(K) |] ==> i < K" ``` paulson@46877 ` 501` ``` by (simp (no_asm_simp) add: cardinal_lt_imp_lt Card_is_Ord Card_cardinal_eq) ``` paulson@13221 ` 502` paulson@46821 ` 503` ```lemma Card_lt_iff: "[| Ord(i); Card(K) |] ==> (|i| < K) \ (i < K)" ``` paulson@13221 ` 504` ```by (blast intro: Card_lt_imp_lt Ord_cardinal_le [THEN lt_trans1]) ``` paulson@13221 ` 505` paulson@46821 ` 506` ```lemma Card_le_iff: "[| Ord(i); Card(K) |] ==> (K \ |i|) \ (K \ i)" ``` paulson@13269 ` 507` ```by (simp add: Card_lt_iff Card_is_Ord Ord_cardinal not_lt_iff_le [THEN iff_sym]) ``` paulson@13221 ` 508` paulson@13221 ` 509` ```(*Can use AC or finiteness to discharge first premise*) ``` paulson@13221 ` 510` ```lemma well_ord_lepoll_imp_Card_le: ``` paulson@46841 ` 511` ``` assumes wB: "well_ord(B,r)" and AB: "A \ B" ``` paulson@46841 ` 512` ``` shows "|A| \ |B|" ``` paulson@47016 ` 513` ```using Ord_cardinal [of A] Ord_cardinal [of B] ``` paulson@47016 ` 514` ```proof (cases rule: Ord_linear_le) ``` paulson@47016 ` 515` ``` case le thus ?thesis . ``` paulson@47016 ` 516` ```next ``` paulson@47016 ` 517` ``` case ge ``` paulson@46841 ` 518` ``` from lepoll_well_ord [OF AB wB] ``` paulson@46841 ` 519` ``` obtain s where s: "well_ord(A, s)" by blast ``` paulson@46953 ` 520` ``` have "B \ |B|" by (blast intro: wB eqpoll_sym well_ord_cardinal_eqpoll) ``` paulson@47016 ` 521` ``` also have "... \ |A|" by (rule le_imp_lepoll [OF ge]) ``` paulson@46841 ` 522` ``` also have "... \ A" by (rule well_ord_cardinal_eqpoll [OF s]) ``` paulson@46841 ` 523` ``` finally have "B \ A" . ``` paulson@46953 ` 524` ``` hence "A \ B" by (blast intro: eqpollI AB) ``` paulson@46841 ` 525` ``` hence "|A| = |B|" by (rule cardinal_cong) ``` paulson@46841 ` 526` ``` thus ?thesis by simp ``` paulson@46841 ` 527` ```qed ``` paulson@13221 ` 528` paulson@46820 ` 529` ```lemma lepoll_cardinal_le: "[| A \ i; Ord(i) |] ==> |A| \ i" ``` paulson@13221 ` 530` ```apply (rule le_trans) ``` paulson@13221 ` 531` ```apply (erule well_ord_Memrel [THEN well_ord_lepoll_imp_Card_le], assumption) ``` paulson@13221 ` 532` ```apply (erule Ord_cardinal_le) ``` paulson@13221 ` 533` ```done ``` paulson@13221 ` 534` paulson@13221 ` 535` ```lemma lepoll_Ord_imp_eqpoll: "[| A \ i; Ord(i) |] ==> |A| \ A" ``` paulson@13221 ` 536` ```by (blast intro: lepoll_cardinal_le well_ord_Memrel well_ord_cardinal_eqpoll dest!: lepoll_well_ord) ``` paulson@13221 ` 537` paulson@14046 ` 538` ```lemma lesspoll_imp_eqpoll: "[| A \ i; Ord(i) |] ==> |A| \ A" ``` paulson@13221 ` 539` ```apply (unfold lesspoll_def) ``` paulson@13221 ` 540` ```apply (blast intro: lepoll_Ord_imp_eqpoll) ``` paulson@13221 ` 541` ```done ``` paulson@13221 ` 542` paulson@46820 ` 543` ```lemma cardinal_subset_Ord: "[|A<=i; Ord(i)|] ==> |A| \ i" ``` paulson@14046 ` 544` ```apply (drule subset_imp_lepoll [THEN lepoll_cardinal_le]) ``` paulson@14046 ` 545` ```apply (auto simp add: lt_def) ``` paulson@14046 ` 546` ```apply (blast intro: Ord_trans) ``` paulson@14046 ` 547` ```done ``` paulson@13221 ` 548` wenzelm@60770 ` 549` ```subsection\The finite cardinals\ ``` paulson@13221 ` 550` paulson@46820 ` 551` ```lemma cons_lepoll_consD: ``` paulson@46820 ` 552` ``` "[| cons(u,A) \ cons(v,B); u\A; v\B |] ==> A \ B" ``` paulson@13221 ` 553` ```apply (unfold lepoll_def inj_def, safe) ``` paulson@46820 ` 554` ```apply (rule_tac x = "\x\A. if f`x=v then f`u else f`x" in exI) ``` paulson@13221 ` 555` ```apply (rule CollectI) ``` paulson@13221 ` 556` ```(*Proving it's in the function space A->B*) ``` paulson@13221 ` 557` ```apply (rule if_type [THEN lam_type]) ``` paulson@13221 ` 558` ```apply (blast dest: apply_funtype) ``` paulson@13221 ` 559` ```apply (blast elim!: mem_irrefl dest: apply_funtype) ``` paulson@13221 ` 560` ```(*Proving it's injective*) ``` paulson@13221 ` 561` ```apply (simp (no_asm_simp)) ``` paulson@13221 ` 562` ```apply blast ``` paulson@13221 ` 563` ```done ``` paulson@13221 ` 564` paulson@46820 ` 565` ```lemma cons_eqpoll_consD: "[| cons(u,A) \ cons(v,B); u\A; v\B |] ==> A \ B" ``` paulson@13221 ` 566` ```apply (simp add: eqpoll_iff) ``` paulson@13221 ` 567` ```apply (blast intro: cons_lepoll_consD) ``` paulson@13221 ` 568` ```done ``` paulson@13221 ` 569` paulson@13221 ` 570` ```(*Lemma suggested by Mike Fourman*) ``` paulson@13221 ` 571` ```lemma succ_lepoll_succD: "succ(m) \ succ(n) ==> m \ n" ``` paulson@13221 ` 572` ```apply (unfold succ_def) ``` paulson@13221 ` 573` ```apply (erule cons_lepoll_consD) ``` paulson@13221 ` 574` ```apply (rule mem_not_refl)+ ``` paulson@13221 ` 575` ```done ``` paulson@13221 ` 576` paulson@46877 ` 577` paulson@46935 ` 578` ```lemma nat_lepoll_imp_le: ``` paulson@46935 ` 579` ``` "m \ nat ==> n \ nat \ m \ n \ m \ n" ``` paulson@46935 ` 580` ```proof (induct m arbitrary: n rule: nat_induct) ``` paulson@46935 ` 581` ``` case 0 thus ?case by (blast intro!: nat_0_le) ``` paulson@46935 ` 582` ```next ``` paulson@46935 ` 583` ``` case (succ m) ``` wenzelm@60770 ` 584` ``` show ?case using \n \ nat\ ``` paulson@46935 ` 585` ``` proof (cases rule: natE) ``` paulson@46935 ` 586` ``` case 0 thus ?thesis using succ ``` paulson@46935 ` 587` ``` by (simp add: lepoll_def inj_def) ``` paulson@46935 ` 588` ``` next ``` wenzelm@60770 ` 589` ``` case (succ n') thus ?thesis using succ.hyps \ succ(m) \ n\ ``` paulson@46935 ` 590` ``` by (blast intro!: succ_leI dest!: succ_lepoll_succD) ``` paulson@46935 ` 591` ``` qed ``` paulson@46935 ` 592` ```qed ``` paulson@13221 ` 593` paulson@46953 ` 594` ```lemma nat_eqpoll_iff: "[| m \ nat; n \ nat |] ==> m \ n \ m = n" ``` paulson@13221 ` 595` ```apply (rule iffI) ``` paulson@13221 ` 596` ```apply (blast intro: nat_lepoll_imp_le le_anti_sym elim!: eqpollE) ``` paulson@13221 ` 597` ```apply (simp add: eqpoll_refl) ``` paulson@13221 ` 598` ```done ``` paulson@13221 ` 599` paulson@13221 ` 600` ```(*The object of all this work: every natural number is a (finite) cardinal*) ``` paulson@46820 ` 601` ```lemma nat_into_Card: ``` paulson@47042 ` 602` ``` assumes n: "n \ nat" shows "Card(n)" ``` paulson@47042 ` 603` ```proof (unfold Card_def cardinal_def, rule sym) ``` paulson@47042 ` 604` ``` have "Ord(n)" using n by auto ``` paulson@47042 ` 605` ``` moreover ``` paulson@47042 ` 606` ``` { fix i ``` paulson@47042 ` 607` ``` assume "i < n" "i \ n" ``` paulson@47042 ` 608` ``` hence False using n ``` paulson@47042 ` 609` ``` by (auto simp add: lt_nat_in_nat [THEN nat_eqpoll_iff]) ``` paulson@47042 ` 610` ``` } ``` paulson@47042 ` 611` ``` ultimately show "(\ i. i \ n) = n" by (auto intro!: Least_equality) ``` paulson@47042 ` 612` ```qed ``` paulson@13221 ` 613` paulson@13221 ` 614` ```lemmas cardinal_0 = nat_0I [THEN nat_into_Card, THEN Card_cardinal_eq, iff] ``` paulson@13221 ` 615` ```lemmas cardinal_1 = nat_1I [THEN nat_into_Card, THEN Card_cardinal_eq, iff] ``` paulson@13221 ` 616` paulson@13221 ` 617` paulson@13221 ` 618` ```(*Part of Kunen's Lemma 10.6*) ``` paulson@46877 ` 619` ```lemma succ_lepoll_natE: "[| succ(n) \ n; n \ nat |] ==> P" ``` paulson@13221 ` 620` ```by (rule nat_lepoll_imp_le [THEN lt_irrefl], auto) ``` paulson@13221 ` 621` paulson@46820 ` 622` ```lemma nat_lepoll_imp_ex_eqpoll_n: ``` paulson@13221 ` 623` ``` "[| n \ nat; nat \ X |] ==> \Y. Y \ X & n \ Y" ``` paulson@13221 ` 624` ```apply (unfold lepoll_def eqpoll_def) ``` paulson@13221 ` 625` ```apply (fast del: subsetI subsetCE ``` paulson@13221 ` 626` ``` intro!: subset_SIs ``` paulson@13221 ` 627` ``` dest!: Ord_nat [THEN [2] OrdmemD, THEN [2] restrict_inj] ``` paulson@46820 ` 628` ``` elim!: restrict_bij ``` paulson@13221 ` 629` ``` inj_is_fun [THEN fun_is_rel, THEN image_subset]) ``` paulson@13221 ` 630` ```done ``` paulson@13221 ` 631` paulson@13221 ` 632` wenzelm@61394 ` 633` ```(** \, \ and natural numbers **) ``` paulson@13221 ` 634` paulson@46877 ` 635` ```lemma lepoll_succ: "i \ succ(i)" ``` paulson@46877 ` 636` ``` by (blast intro: subset_imp_lepoll) ``` paulson@46877 ` 637` paulson@46820 ` 638` ```lemma lepoll_imp_lesspoll_succ: ``` paulson@46877 ` 639` ``` assumes A: "A \ m" and m: "m \ nat" ``` paulson@46877 ` 640` ``` shows "A \ succ(m)" ``` paulson@46877 ` 641` ```proof - ``` paulson@46953 ` 642` ``` { assume "A \ succ(m)" ``` paulson@46877 ` 643` ``` hence "succ(m) \ A" by (rule eqpoll_sym) ``` paulson@46877 ` 644` ``` also have "... \ m" by (rule A) ``` paulson@46877 ` 645` ``` finally have "succ(m) \ m" . ``` paulson@46877 ` 646` ``` hence False by (rule succ_lepoll_natE) (rule m) } ``` paulson@46877 ` 647` ``` moreover have "A \ succ(m)" by (blast intro: lepoll_trans A lepoll_succ) ``` paulson@46953 ` 648` ``` ultimately show ?thesis by (auto simp add: lesspoll_def) ``` paulson@46877 ` 649` ```qed ``` paulson@46877 ` 650` paulson@46877 ` 651` ```lemma lesspoll_succ_imp_lepoll: ``` paulson@46877 ` 652` ``` "[| A \ succ(m); m \ nat |] ==> A \ m" ``` paulson@46877 ` 653` ```apply (unfold lesspoll_def lepoll_def eqpoll_def bij_def) ``` paulson@46877 ` 654` ```apply (auto dest: inj_not_surj_succ) ``` paulson@13221 ` 655` ```done ``` paulson@13221 ` 656` paulson@46877 ` 657` ```lemma lesspoll_succ_iff: "m \ nat ==> A \ succ(m) \ A \ m" ``` paulson@13221 ` 658` ```by (blast intro!: lepoll_imp_lesspoll_succ lesspoll_succ_imp_lepoll) ``` paulson@13221 ` 659` paulson@46877 ` 660` ```lemma lepoll_succ_disj: "[| A \ succ(m); m \ nat |] ==> A \ m | A \ succ(m)" ``` paulson@13221 ` 661` ```apply (rule disjCI) ``` paulson@13221 ` 662` ```apply (rule lesspoll_succ_imp_lepoll) ``` paulson@13221 ` 663` ```prefer 2 apply assumption ``` paulson@13221 ` 664` ```apply (simp (no_asm_simp) add: lesspoll_def) ``` paulson@13221 ` 665` ```done ``` paulson@13221 ` 666` paulson@13221 ` 667` ```lemma lesspoll_cardinal_lt: "[| A \ i; Ord(i) |] ==> |A| < i" ``` paulson@13221 ` 668` ```apply (unfold lesspoll_def, clarify) ``` paulson@13221 ` 669` ```apply (frule lepoll_cardinal_le, assumption) ``` paulson@13221 ` 670` ```apply (blast intro: well_ord_Memrel well_ord_cardinal_eqpoll [THEN eqpoll_sym] ``` paulson@13221 ` 671` ``` dest: lepoll_well_ord elim!: leE) ``` paulson@13221 ` 672` ```done ``` paulson@13221 ` 673` paulson@13221 ` 674` wenzelm@60770 ` 675` ```subsection\The first infinite cardinal: Omega, or nat\ ``` paulson@13221 ` 676` paulson@13221 ` 677` ```(*This implies Kunen's Lemma 10.6*) ``` paulson@46877 ` 678` ```lemma lt_not_lepoll: ``` paulson@46877 ` 679` ``` assumes n: "n nat" shows "~ i \ n" ``` paulson@46877 ` 680` ```proof - ``` paulson@46877 ` 681` ``` { assume i: "i \ n" ``` paulson@46877 ` 682` ``` have "succ(n) \ i" using n ``` paulson@46953 ` 683` ``` by (elim ltE, blast intro: Ord_succ_subsetI [THEN subset_imp_lepoll]) ``` paulson@46877 ` 684` ``` also have "... \ n" by (rule i) ``` paulson@46877 ` 685` ``` finally have "succ(n) \ n" . ``` paulson@46877 ` 686` ``` hence False by (rule succ_lepoll_natE) (rule n) } ``` paulson@46877 ` 687` ``` thus ?thesis by auto ``` paulson@46877 ` 688` ```qed ``` paulson@13221 ` 689` wenzelm@61798 ` 690` ```text\A slightly weaker version of \nat_eqpoll_iff\\ ``` paulson@46877 ` 691` ```lemma Ord_nat_eqpoll_iff: ``` paulson@46877 ` 692` ``` assumes i: "Ord(i)" and n: "n \ nat" shows "i \ n \ i=n" ``` paulson@47016 ` 693` ```using i nat_into_Ord [OF n] ``` paulson@47016 ` 694` ```proof (cases rule: Ord_linear_lt) ``` paulson@47016 ` 695` ``` case lt ``` paulson@46877 ` 696` ``` hence "i \ nat" by (rule lt_nat_in_nat) (rule n) ``` paulson@46953 ` 697` ``` thus ?thesis by (simp add: nat_eqpoll_iff n) ``` paulson@46877 ` 698` ```next ``` paulson@47016 ` 699` ``` case eq ``` paulson@46953 ` 700` ``` thus ?thesis by (simp add: eqpoll_refl) ``` paulson@46877 ` 701` ```next ``` paulson@47016 ` 702` ``` case gt ``` paulson@46953 ` 703` ``` hence "~ i \ n" using n by (rule lt_not_lepoll) ``` paulson@46877 ` 704` ``` hence "~ i \ n" using n by (blast intro: eqpoll_imp_lepoll) ``` wenzelm@60770 ` 705` ``` moreover have "i \ n" using \n by auto ``` paulson@46877 ` 706` ``` ultimately show ?thesis by blast ``` paulson@46877 ` 707` ```qed ``` paulson@13221 ` 708` paulson@13221 ` 709` ```lemma Card_nat: "Card(nat)" ``` paulson@46877 ` 710` ```proof - ``` paulson@46877 ` 711` ``` { fix i ``` paulson@46953 ` 712` ``` assume i: "i < nat" "i \ nat" ``` paulson@46953 ` 713` ``` hence "~ nat \ i" ``` paulson@46953 ` 714` ``` by (simp add: lt_def lt_not_lepoll) ``` paulson@46953 ` 715` ``` hence False using i ``` paulson@46877 ` 716` ``` by (simp add: eqpoll_iff) ``` paulson@46877 ` 717` ``` } ``` paulson@46953 ` 718` ``` hence "(\ i. i \ nat) = nat" by (blast intro: Least_equality eqpoll_refl) ``` paulson@46877 ` 719` ``` thus ?thesis ``` paulson@46953 ` 720` ``` by (auto simp add: Card_def cardinal_def) ``` paulson@46877 ` 721` ```qed ``` paulson@13221 ` 722` paulson@13221 ` 723` ```(*Allows showing that |i| is a limit cardinal*) ``` paulson@46820 ` 724` ```lemma nat_le_cardinal: "nat \ i ==> nat \ |i|" ``` paulson@13221 ` 725` ```apply (rule Card_nat [THEN Card_cardinal_eq, THEN subst]) ``` paulson@13221 ` 726` ```apply (erule cardinal_mono) ``` paulson@13221 ` 727` ```done ``` paulson@13221 ` 728` paulson@46841 ` 729` ```lemma n_lesspoll_nat: "n \ nat ==> n \ nat" ``` paulson@46841 ` 730` ``` by (blast intro: Ord_nat Card_nat ltI lt_Card_imp_lesspoll) ``` paulson@46841 ` 731` paulson@13221 ` 732` wenzelm@60770 ` 733` ```subsection\Towards Cardinal Arithmetic\ ``` paulson@13221 ` 734` ```(** Congruence laws for successor, cardinal addition and multiplication **) ``` paulson@13221 ` 735` paulson@13221 ` 736` ```(*Congruence law for cons under equipollence*) ``` paulson@46820 ` 737` ```lemma cons_lepoll_cong: ``` paulson@46820 ` 738` ``` "[| A \ B; b \ B |] ==> cons(a,A) \ cons(b,B)" ``` paulson@13221 ` 739` ```apply (unfold lepoll_def, safe) ``` paulson@46820 ` 740` ```apply (rule_tac x = "\y\cons (a,A) . if y=a then b else f`y" in exI) ``` paulson@46953 ` 741` ```apply (rule_tac d = "%z. if z \ B then converse (f) `z else a" in lam_injective) ``` paulson@46820 ` 742` ```apply (safe elim!: consE') ``` paulson@13221 ` 743` ``` apply simp_all ``` paulson@46820 ` 744` ```apply (blast intro: inj_is_fun [THEN apply_type])+ ``` paulson@13221 ` 745` ```done ``` paulson@13221 ` 746` paulson@13221 ` 747` ```lemma cons_eqpoll_cong: ``` paulson@46820 ` 748` ``` "[| A \ B; a \ A; b \ B |] ==> cons(a,A) \ cons(b,B)" ``` paulson@13221 ` 749` ```by (simp add: eqpoll_iff cons_lepoll_cong) ``` paulson@13221 ` 750` paulson@13221 ` 751` ```lemma cons_lepoll_cons_iff: ``` paulson@46821 ` 752` ``` "[| a \ A; b \ B |] ==> cons(a,A) \ cons(b,B) \ A \ B" ``` paulson@13221 ` 753` ```by (blast intro: cons_lepoll_cong cons_lepoll_consD) ``` paulson@13221 ` 754` paulson@13221 ` 755` ```lemma cons_eqpoll_cons_iff: ``` paulson@46821 ` 756` ``` "[| a \ A; b \ B |] ==> cons(a,A) \ cons(b,B) \ A \ B" ``` paulson@13221 ` 757` ```by (blast intro: cons_eqpoll_cong cons_eqpoll_consD) ``` paulson@13221 ` 758` paulson@13221 ` 759` ```lemma singleton_eqpoll_1: "{a} \ 1" ``` paulson@13221 ` 760` ```apply (unfold succ_def) ``` paulson@13221 ` 761` ```apply (blast intro!: eqpoll_refl [THEN cons_eqpoll_cong]) ``` paulson@13221 ` 762` ```done ``` paulson@13221 ` 763` paulson@13221 ` 764` ```lemma cardinal_singleton: "|{a}| = 1" ``` paulson@13221 ` 765` ```apply (rule singleton_eqpoll_1 [THEN cardinal_cong, THEN trans]) ``` paulson@13221 ` 766` ```apply (simp (no_asm) add: nat_into_Card [THEN Card_cardinal_eq]) ``` paulson@13221 ` 767` ```done ``` paulson@13221 ` 768` paulson@46820 ` 769` ```lemma not_0_is_lepoll_1: "A \ 0 ==> 1 \ A" ``` paulson@13221 ` 770` ```apply (erule not_emptyE) ``` paulson@13221 ` 771` ```apply (rule_tac a = "cons (x, A-{x}) " in subst) ``` paulson@13221 ` 772` ```apply (rule_tac [2] a = "cons(0,0)" and P= "%y. y \ cons (x, A-{x})" in subst) ``` paulson@13221 ` 773` ```prefer 3 apply (blast intro: cons_lepoll_cong subset_imp_lepoll, auto) ``` paulson@13221 ` 774` ```done ``` paulson@13221 ` 775` paulson@13221 ` 776` ```(*Congruence law for succ under equipollence*) ``` paulson@13221 ` 777` ```lemma succ_eqpoll_cong: "A \ B ==> succ(A) \ succ(B)" ``` paulson@13221 ` 778` ```apply (unfold succ_def) ``` paulson@13221 ` 779` ```apply (simp add: cons_eqpoll_cong mem_not_refl) ``` paulson@13221 ` 780` ```done ``` paulson@13221 ` 781` paulson@13221 ` 782` ```(*Congruence law for + under equipollence*) ``` paulson@13221 ` 783` ```lemma sum_eqpoll_cong: "[| A \ C; B \ D |] ==> A+B \ C+D" ``` paulson@13221 ` 784` ```apply (unfold eqpoll_def) ``` paulson@13221 ` 785` ```apply (blast intro!: sum_bij) ``` paulson@13221 ` 786` ```done ``` paulson@13221 ` 787` paulson@13221 ` 788` ```(*Congruence law for * under equipollence*) ``` paulson@46820 ` 789` ```lemma prod_eqpoll_cong: ``` paulson@13221 ` 790` ``` "[| A \ C; B \ D |] ==> A*B \ C*D" ``` paulson@13221 ` 791` ```apply (unfold eqpoll_def) ``` paulson@13221 ` 792` ```apply (blast intro!: prod_bij) ``` paulson@13221 ` 793` ```done ``` paulson@13221 ` 794` paulson@46820 ` 795` ```lemma inj_disjoint_eqpoll: ``` paulson@46953 ` 796` ``` "[| f \ inj(A,B); A \ B = 0 |] ==> A \ (B - range(f)) \ B" ``` paulson@13221 ` 797` ```apply (unfold eqpoll_def) ``` paulson@13221 ` 798` ```apply (rule exI) ``` paulson@46953 ` 799` ```apply (rule_tac c = "%x. if x \ A then f`x else x" ``` paulson@46953 ` 800` ``` and d = "%y. if y \ range (f) then converse (f) `y else y" ``` paulson@13221 ` 801` ``` in lam_bijective) ``` paulson@13221 ` 802` ```apply (blast intro!: if_type inj_is_fun [THEN apply_type]) ``` paulson@13221 ` 803` ```apply (simp (no_asm_simp) add: inj_converse_fun [THEN apply_funtype]) ``` paulson@46820 ` 804` ```apply (safe elim!: UnE') ``` paulson@13221 ` 805` ``` apply (simp_all add: inj_is_fun [THEN apply_rangeI]) ``` paulson@46820 ` 806` ```apply (blast intro: inj_converse_fun [THEN apply_type])+ ``` paulson@13221 ` 807` ```done ``` paulson@13221 ` 808` paulson@13221 ` 809` wenzelm@60770 ` 810` ```subsection\Lemmas by Krzysztof Grabczewski\ ``` paulson@13356 ` 811` paulson@13356 ` 812` ```(*New proofs using cons_lepoll_cons. Could generalise from succ to cons.*) ``` paulson@13221 ` 813` wenzelm@60770 ` 814` ```text\If @{term A} has at most @{term"n+1"} elements and @{term"a \ A"} ``` wenzelm@60770 ` 815` ``` then @{term"A-{a}"} has at most @{term n}.\ ``` paulson@46820 ` 816` ```lemma Diff_sing_lepoll: ``` paulson@46877 ` 817` ``` "[| a \ A; A \ succ(n) |] ==> A - {a} \ n" ``` paulson@13221 ` 818` ```apply (unfold succ_def) ``` paulson@13221 ` 819` ```apply (rule cons_lepoll_consD) ``` paulson@13221 ` 820` ```apply (rule_tac [3] mem_not_refl) ``` paulson@13221 ` 821` ```apply (erule cons_Diff [THEN ssubst], safe) ``` paulson@13221 ` 822` ```done ``` paulson@13221 ` 823` wenzelm@60770 ` 824` ```text\If @{term A} has at least @{term"n+1"} elements then @{term"A-{a}"} has at least @{term n}.\ ``` paulson@46820 ` 825` ```lemma lepoll_Diff_sing: ``` paulson@46877 ` 826` ``` assumes A: "succ(n) \ A" shows "n \ A - {a}" ``` paulson@46877 ` 827` ```proof - ``` paulson@46877 ` 828` ``` have "cons(n,n) \ A" using A ``` paulson@46877 ` 829` ``` by (unfold succ_def) ``` paulson@46953 ` 830` ``` also have "... \ cons(a, A-{a})" ``` paulson@46877 ` 831` ``` by (blast intro: subset_imp_lepoll) ``` paulson@46877 ` 832` ``` finally have "cons(n,n) \ cons(a, A-{a})" . ``` paulson@46877 ` 833` ``` thus ?thesis ``` paulson@46953 ` 834` ``` by (blast intro: cons_lepoll_consD mem_irrefl) ``` paulson@46877 ` 835` ```qed ``` paulson@13221 ` 836` paulson@46877 ` 837` ```lemma Diff_sing_eqpoll: "[| a \ A; A \ succ(n) |] ==> A - {a} \ n" ``` paulson@46820 ` 838` ```by (blast intro!: eqpollI ``` paulson@46820 ` 839` ``` elim!: eqpollE ``` paulson@13221 ` 840` ``` intro: Diff_sing_lepoll lepoll_Diff_sing) ``` paulson@13221 ` 841` paulson@46877 ` 842` ```lemma lepoll_1_is_sing: "[| A \ 1; a \ A |] ==> A = {a}" ``` paulson@13221 ` 843` ```apply (frule Diff_sing_lepoll, assumption) ``` paulson@13221 ` 844` ```apply (drule lepoll_0_is_0) ``` paulson@13221 ` 845` ```apply (blast elim: equalityE) ``` paulson@13221 ` 846` ```done ``` paulson@13221 ` 847` paulson@46820 ` 848` ```lemma Un_lepoll_sum: "A \ B \ A+B" ``` paulson@13221 ` 849` ```apply (unfold lepoll_def) ``` paulson@46877 ` 850` ```apply (rule_tac x = "\x\A \ B. if x\A then Inl (x) else Inr (x)" in exI) ``` paulson@46877 ` 851` ```apply (rule_tac d = "%z. snd (z)" in lam_injective) ``` paulson@46820 ` 852` ```apply force ``` paulson@13221 ` 853` ```apply (simp add: Inl_def Inr_def) ``` paulson@13221 ` 854` ```done ``` paulson@13221 ` 855` paulson@13221 ` 856` ```lemma well_ord_Un: ``` paulson@46820 ` 857` ``` "[| well_ord(X,R); well_ord(Y,S) |] ==> \T. well_ord(X \ Y, T)" ``` paulson@46820 ` 858` ```by (erule well_ord_radd [THEN Un_lepoll_sum [THEN lepoll_well_ord]], ``` paulson@13221 ` 859` ``` assumption) ``` paulson@13221 ` 860` paulson@13221 ` 861` ```(*Krzysztof Grabczewski*) ``` paulson@46820 ` 862` ```lemma disj_Un_eqpoll_sum: "A \ B = 0 ==> A \ B \ A + B" ``` paulson@13221 ` 863` ```apply (unfold eqpoll_def) ``` paulson@46877 ` 864` ```apply (rule_tac x = "\a\A \ B. if a \ A then Inl (a) else Inr (a)" in exI) ``` paulson@46877 ` 865` ```apply (rule_tac d = "%z. case (%x. x, %x. x, z)" in lam_bijective) ``` paulson@13221 ` 866` ```apply auto ``` paulson@13221 ` 867` ```done ``` paulson@13221 ` 868` paulson@13221 ` 869` wenzelm@60770 ` 870` ```subsection \Finite and infinite sets\ ``` paulson@13221 ` 871` paulson@47018 ` 872` ```lemma eqpoll_imp_Finite_iff: "A \ B ==> Finite(A) \ Finite(B)" ``` paulson@47018 ` 873` ```apply (unfold Finite_def) ``` paulson@47018 ` 874` ```apply (blast intro: eqpoll_trans eqpoll_sym) ``` paulson@47018 ` 875` ```done ``` paulson@47018 ` 876` paulson@13244 ` 877` ```lemma Finite_0 [simp]: "Finite(0)" ``` paulson@13221 ` 878` ```apply (unfold Finite_def) ``` paulson@13221 ` 879` ```apply (blast intro!: eqpoll_refl nat_0I) ``` paulson@13221 ` 880` ```done ``` paulson@13221 ` 881` paulson@47018 ` 882` ```lemma Finite_cons: "Finite(x) ==> Finite(cons(y,x))" ``` paulson@13221 ` 883` ```apply (unfold Finite_def) ``` paulson@47018 ` 884` ```apply (case_tac "y \ x") ``` paulson@47018 ` 885` ```apply (simp add: cons_absorb) ``` paulson@47018 ` 886` ```apply (erule bexE) ``` paulson@47018 ` 887` ```apply (rule bexI) ``` paulson@47018 ` 888` ```apply (erule_tac [2] nat_succI) ``` paulson@47018 ` 889` ```apply (simp (no_asm_simp) add: succ_def cons_eqpoll_cong mem_not_refl) ``` paulson@47018 ` 890` ```done ``` paulson@47018 ` 891` paulson@47018 ` 892` ```lemma Finite_succ: "Finite(x) ==> Finite(succ(x))" ``` paulson@47018 ` 893` ```apply (unfold succ_def) ``` paulson@47018 ` 894` ```apply (erule Finite_cons) ``` paulson@13221 ` 895` ```done ``` paulson@13221 ` 896` paulson@47018 ` 897` ```lemma lepoll_nat_imp_Finite: ``` paulson@47018 ` 898` ``` assumes A: "A \ n" and n: "n \ nat" shows "Finite(A)" ``` paulson@47018 ` 899` ```proof - ``` paulson@47018 ` 900` ``` have "A \ n \ Finite(A)" using n ``` paulson@47018 ` 901` ``` proof (induct n) ``` paulson@47018 ` 902` ``` case 0 ``` paulson@47018 ` 903` ``` hence "A = 0" by (rule lepoll_0_is_0) ``` paulson@47018 ` 904` ``` thus ?case by simp ``` paulson@47018 ` 905` ``` next ``` paulson@47018 ` 906` ``` case (succ n) ``` paulson@47018 ` 907` ``` hence "A \ n \ A \ succ(n)" by (blast dest: lepoll_succ_disj) ``` paulson@47018 ` 908` ``` thus ?case using succ by (auto simp add: Finite_def) ``` paulson@47018 ` 909` ``` qed ``` paulson@47018 ` 910` ``` thus ?thesis using A . ``` paulson@47018 ` 911` ```qed ``` paulson@47018 ` 912` paulson@46820 ` 913` ```lemma lesspoll_nat_is_Finite: ``` paulson@13221 ` 914` ``` "A \ nat ==> Finite(A)" ``` paulson@13221 ` 915` ```apply (unfold Finite_def) ``` paulson@46820 ` 916` ```apply (blast dest: ltD lesspoll_cardinal_lt ``` paulson@13221 ` 917` ``` lesspoll_imp_eqpoll [THEN eqpoll_sym]) ``` paulson@13221 ` 918` ```done ``` paulson@13221 ` 919` paulson@46820 ` 920` ```lemma lepoll_Finite: ``` paulson@46877 ` 921` ``` assumes Y: "Y \ X" and X: "Finite(X)" shows "Finite(Y)" ``` paulson@46877 ` 922` ```proof - ``` paulson@46953 ` 923` ``` obtain n where n: "n \ nat" "X \ n" using X ``` paulson@46953 ` 924` ``` by (auto simp add: Finite_def) ``` paulson@46877 ` 925` ``` have "Y \ X" by (rule Y) ``` paulson@46877 ` 926` ``` also have "... \ n" by (rule n) ``` paulson@46877 ` 927` ``` finally have "Y \ n" . ``` paulson@46877 ` 928` ``` thus ?thesis using n by (simp add: lepoll_nat_imp_Finite) ``` paulson@46877 ` 929` ```qed ``` paulson@13221 ` 930` wenzelm@45602 ` 931` ```lemmas subset_Finite = subset_imp_lepoll [THEN lepoll_Finite] ``` paulson@13221 ` 932` paulson@46821 ` 933` ```lemma Finite_cons_iff [iff]: "Finite(cons(y,x)) \ Finite(x)" ``` paulson@13244 ` 934` ```by (blast intro: Finite_cons subset_Finite) ``` paulson@13244 ` 935` paulson@46821 ` 936` ```lemma Finite_succ_iff [iff]: "Finite(succ(x)) \ Finite(x)" ``` paulson@13244 ` 937` ```by (simp add: succ_def) ``` paulson@13244 ` 938` paulson@47018 ` 939` ```lemma Finite_Int: "Finite(A) | Finite(B) ==> Finite(A \ B)" ``` paulson@47018 ` 940` ```by (blast intro: subset_Finite) ``` paulson@47018 ` 941` paulson@47018 ` 942` ```lemmas Finite_Diff = Diff_subset [THEN subset_Finite] ``` paulson@47018 ` 943` paulson@46820 ` 944` ```lemma nat_le_infinite_Ord: ``` paulson@46820 ` 945` ``` "[| Ord(i); ~ Finite(i) |] ==> nat \ i" ``` paulson@13221 ` 946` ```apply (unfold Finite_def) ``` paulson@13221 ` 947` ```apply (erule Ord_nat [THEN [2] Ord_linear2]) ``` paulson@13221 ` 948` ```prefer 2 apply assumption ``` paulson@13221 ` 949` ```apply (blast intro!: eqpoll_refl elim!: ltE) ``` paulson@13221 ` 950` ```done ``` paulson@13221 ` 951` paulson@46820 ` 952` ```lemma Finite_imp_well_ord: ``` paulson@46820 ` 953` ``` "Finite(A) ==> \r. well_ord(A,r)" ``` paulson@13221 ` 954` ```apply (unfold Finite_def eqpoll_def) ``` paulson@13221 ` 955` ```apply (blast intro: well_ord_rvimage bij_is_inj well_ord_Memrel nat_into_Ord) ``` paulson@13221 ` 956` ```done ``` paulson@13221 ` 957` paulson@13244 ` 958` ```lemma succ_lepoll_imp_not_empty: "succ(x) \ y ==> y \ 0" ``` paulson@13244 ` 959` ```by (fast dest!: lepoll_0_is_0) ``` paulson@13244 ` 960` paulson@13244 ` 961` ```lemma eqpoll_succ_imp_not_empty: "x \ succ(n) ==> x \ 0" ``` paulson@13244 ` 962` ```by (fast elim!: eqpoll_sym [THEN eqpoll_0_is_0, THEN succ_neq_0]) ``` paulson@13244 ` 963` paulson@13244 ` 964` ```lemma Finite_Fin_lemma [rule_format]: ``` paulson@46820 ` 965` ``` "n \ nat ==> \A. (A\n & A \ X) \ A \ Fin(X)" ``` paulson@13244 ` 966` ```apply (induct_tac n) ``` paulson@13244 ` 967` ```apply (rule allI) ``` paulson@13244 ` 968` ```apply (fast intro!: Fin.emptyI dest!: eqpoll_imp_lepoll [THEN lepoll_0_is_0]) ``` paulson@13244 ` 969` ```apply (rule allI) ``` paulson@13244 ` 970` ```apply (rule impI) ``` paulson@13244 ` 971` ```apply (erule conjE) ``` paulson@13244 ` 972` ```apply (rule eqpoll_succ_imp_not_empty [THEN not_emptyE], assumption) ``` paulson@13244 ` 973` ```apply (frule Diff_sing_eqpoll, assumption) ``` paulson@13244 ` 974` ```apply (erule allE) ``` paulson@13244 ` 975` ```apply (erule impE, fast) ``` paulson@13244 ` 976` ```apply (drule subsetD, assumption) ``` paulson@13244 ` 977` ```apply (drule Fin.consI, assumption) ``` paulson@13244 ` 978` ```apply (simp add: cons_Diff) ``` paulson@13244 ` 979` ```done ``` paulson@13244 ` 980` paulson@13244 ` 981` ```lemma Finite_Fin: "[| Finite(A); A \ X |] ==> A \ Fin(X)" ``` paulson@46820 ` 982` ```by (unfold Finite_def, blast intro: Finite_Fin_lemma) ``` paulson@13244 ` 983` paulson@46953 ` 984` ```lemma Fin_lemma [rule_format]: "n \ nat ==> \A. A \ n \ A \ Fin(A)" ``` paulson@13244 ` 985` ```apply (induct_tac n) ``` paulson@13244 ` 986` ```apply (simp add: eqpoll_0_iff, clarify) ``` paulson@46953 ` 987` ```apply (subgoal_tac "\u. u \ A") ``` paulson@13244 ` 988` ```apply (erule exE) ``` wenzelm@46471 ` 989` ```apply (rule Diff_sing_eqpoll [elim_format]) ``` paulson@13244 ` 990` ```prefer 2 apply assumption ``` paulson@13244 ` 991` ```apply assumption ``` paulson@13784 ` 992` ```apply (rule_tac b = A in cons_Diff [THEN subst], assumption) ``` paulson@13244 ` 993` ```apply (rule Fin.consI, blast) ``` paulson@13244 ` 994` ```apply (blast intro: subset_consI [THEN Fin_mono, THEN subsetD]) ``` paulson@13244 ` 995` ```(*Now for the lemma assumed above*) ``` paulson@13244 ` 996` ```apply (unfold eqpoll_def) ``` paulson@13244 ` 997` ```apply (blast intro: bij_converse_bij [THEN bij_is_fun, THEN apply_type]) ``` paulson@13244 ` 998` ```done ``` paulson@13244 ` 999` paulson@46820 ` 1000` ```lemma Finite_into_Fin: "Finite(A) ==> A \ Fin(A)" ``` paulson@13244 ` 1001` ```apply (unfold Finite_def) ``` paulson@13244 ` 1002` ```apply (blast intro: Fin_lemma) ``` paulson@13244 ` 1003` ```done ``` paulson@13244 ` 1004` paulson@46820 ` 1005` ```lemma Fin_into_Finite: "A \ Fin(U) ==> Finite(A)" ``` paulson@13244 ` 1006` ```by (fast intro!: Finite_0 Finite_cons elim: Fin_induct) ``` paulson@13244 ` 1007` paulson@46821 ` 1008` ```lemma Finite_Fin_iff: "Finite(A) \ A \ Fin(A)" ``` paulson@13244 ` 1009` ```by (blast intro: Finite_into_Fin Fin_into_Finite) ``` paulson@13244 ` 1010` paulson@46820 ` 1011` ```lemma Finite_Un: "[| Finite(A); Finite(B) |] ==> Finite(A \ B)" ``` paulson@46820 ` 1012` ```by (blast intro!: Fin_into_Finite Fin_UnI ``` paulson@13244 ` 1013` ``` dest!: Finite_into_Fin ``` paulson@46820 ` 1014` ``` intro: Un_upper1 [THEN Fin_mono, THEN subsetD] ``` paulson@13244 ` 1015` ``` Un_upper2 [THEN Fin_mono, THEN subsetD]) ``` paulson@13244 ` 1016` paulson@46821 ` 1017` ```lemma Finite_Un_iff [simp]: "Finite(A \ B) \ (Finite(A) & Finite(B))" ``` paulson@46820 ` 1018` ```by (blast intro: subset_Finite Finite_Un) ``` paulson@14883 ` 1019` wenzelm@60770 ` 1020` ```text\The converse must hold too.\ ``` paulson@46820 ` 1021` ```lemma Finite_Union: "[| \y\X. Finite(y); Finite(X) |] ==> Finite(\(X))" ``` paulson@13244 ` 1022` ```apply (simp add: Finite_Fin_iff) ``` paulson@13244 ` 1023` ```apply (rule Fin_UnionI) ``` paulson@13244 ` 1024` ```apply (erule Fin_induct, simp) ``` paulson@13244 ` 1025` ```apply (blast intro: Fin.consI Fin_mono [THEN [2] rev_subsetD]) ``` paulson@13244 ` 1026` ```done ``` paulson@13244 ` 1027` paulson@13244 ` 1028` ```(* Induction principle for Finite(A), by Sidi Ehmety *) ``` wenzelm@13524 ` 1029` ```lemma Finite_induct [case_names 0 cons, induct set: Finite]: ``` paulson@13244 ` 1030` ```"[| Finite(A); P(0); ``` paulson@46820 ` 1031` ``` !! x B. [| Finite(B); x \ B; P(B) |] ==> P(cons(x, B)) |] ``` paulson@13244 ` 1032` ``` ==> P(A)" ``` paulson@46820 ` 1033` ```apply (erule Finite_into_Fin [THEN Fin_induct]) ``` paulson@13244 ` 1034` ```apply (blast intro: Fin_into_Finite)+ ``` paulson@13244 ` 1035` ```done ``` paulson@13244 ` 1036` paulson@13244 ` 1037` ```(*Sidi Ehmety. The contrapositive says ~Finite(A) ==> ~Finite(A-{a}) *) ``` paulson@13244 ` 1038` ```lemma Diff_sing_Finite: "Finite(A - {a}) ==> Finite(A)" ``` paulson@13244 ` 1039` ```apply (unfold Finite_def) ``` paulson@46877 ` 1040` ```apply (case_tac "a \ A") ``` paulson@13244 ` 1041` ```apply (subgoal_tac [2] "A-{a}=A", auto) ``` paulson@13244 ` 1042` ```apply (rule_tac x = "succ (n) " in bexI) ``` paulson@13244 ` 1043` ```apply (subgoal_tac "cons (a, A - {a}) = A & cons (n, n) = succ (n) ") ``` paulson@13784 ` 1044` ```apply (drule_tac a = a and b = n in cons_eqpoll_cong) ``` paulson@13244 ` 1045` ```apply (auto dest: mem_irrefl) ``` paulson@13244 ` 1046` ```done ``` paulson@13244 ` 1047` paulson@13244 ` 1048` ```(*Sidi Ehmety. And the contrapositive of this says ``` paulson@13244 ` 1049` ``` [| ~Finite(A); Finite(B) |] ==> ~Finite(A-B) *) ``` paulson@46820 ` 1050` ```lemma Diff_Finite [rule_format]: "Finite(B) ==> Finite(A-B) \ Finite(A)" ``` paulson@13244 ` 1051` ```apply (erule Finite_induct, auto) ``` paulson@46953 ` 1052` ```apply (case_tac "x \ A") ``` paulson@13244 ` 1053` ``` apply (subgoal_tac [2] "A-cons (x, B) = A - B") ``` paulson@13615 ` 1054` ```apply (subgoal_tac "A - cons (x, B) = (A - B) - {x}", simp) ``` paulson@13244 ` 1055` ```apply (drule Diff_sing_Finite, auto) ``` paulson@13244 ` 1056` ```done ``` paulson@13244 ` 1057` paulson@13244 ` 1058` ```lemma Finite_RepFun: "Finite(A) ==> Finite(RepFun(A,f))" ``` paulson@13244 ` 1059` ```by (erule Finite_induct, simp_all) ``` paulson@13244 ` 1060` paulson@13244 ` 1061` ```lemma Finite_RepFun_iff_lemma [rule_format]: ``` paulson@46820 ` 1062` ``` "[|Finite(x); !!x y. f(x)=f(y) ==> x=y|] ``` paulson@46820 ` 1063` ``` ==> \A. x = RepFun(A,f) \ Finite(A)" ``` paulson@13244 ` 1064` ```apply (erule Finite_induct) ``` paulson@46820 ` 1065` ``` apply clarify ``` paulson@13244 ` 1066` ``` apply (case_tac "A=0", simp) ``` paulson@46820 ` 1067` ``` apply (blast del: allE, clarify) ``` paulson@46820 ` 1068` ```apply (subgoal_tac "\z\A. x = f(z)") ``` paulson@46820 ` 1069` ``` prefer 2 apply (blast del: allE elim: equalityE, clarify) ``` paulson@13244 ` 1070` ```apply (subgoal_tac "B = {f(u) . u \ A - {z}}") ``` paulson@46820 ` 1071` ``` apply (blast intro: Diff_sing_Finite) ``` wenzelm@59788 ` 1072` ```apply (thin_tac "\A. P(A) \ Finite(A)" for P) ``` paulson@46820 ` 1073` ```apply (rule equalityI) ``` paulson@46820 ` 1074` ``` apply (blast intro: elim: equalityE) ``` paulson@46820 ` 1075` ```apply (blast intro: elim: equalityCE) ``` paulson@13244 ` 1076` ```done ``` paulson@13244 ` 1077` wenzelm@60770 ` 1078` ```text\I don't know why, but if the premise is expressed using meta-connectives ``` wenzelm@60770 ` 1079` ```then the simplifier cannot prove it automatically in conditional rewriting.\ ``` paulson@13244 ` 1080` ```lemma Finite_RepFun_iff: ``` paulson@46821 ` 1081` ``` "(\x y. f(x)=f(y) \ x=y) ==> Finite(RepFun(A,f)) \ Finite(A)" ``` paulson@46820 ` 1082` ```by (blast intro: Finite_RepFun Finite_RepFun_iff_lemma [of _ f]) ``` paulson@13244 ` 1083` paulson@13244 ` 1084` ```lemma Finite_Pow: "Finite(A) ==> Finite(Pow(A))" ``` paulson@46820 ` 1085` ```apply (erule Finite_induct) ``` paulson@46820 ` 1086` ```apply (simp_all add: Pow_insert Finite_Un Finite_RepFun) ``` paulson@13244 ` 1087` ```done ``` paulson@13244 ` 1088` paulson@13244 ` 1089` ```lemma Finite_Pow_imp_Finite: "Finite(Pow(A)) ==> Finite(A)" ``` paulson@13244 ` 1090` ```apply (subgoal_tac "Finite({{x} . x \ A})") ``` paulson@46820 ` 1091` ``` apply (simp add: Finite_RepFun_iff ) ``` paulson@46820 ` 1092` ```apply (blast intro: subset_Finite) ``` paulson@13244 ` 1093` ```done ``` paulson@13244 ` 1094` paulson@46821 ` 1095` ```lemma Finite_Pow_iff [iff]: "Finite(Pow(A)) \ Finite(A)" ``` paulson@13244 ` 1096` ```by (blast intro: Finite_Pow Finite_Pow_imp_Finite) ``` paulson@13244 ` 1097` paulson@47101 ` 1098` ```lemma Finite_cardinal_iff: ``` paulson@47101 ` 1099` ``` assumes i: "Ord(i)" shows "Finite(|i|) \ Finite(i)" ``` paulson@47101 ` 1100` ``` by (auto simp add: Finite_def) (blast intro: eqpoll_trans eqpoll_sym Ord_cardinal_eqpoll [OF i])+ ``` paulson@13244 ` 1101` paulson@13221 ` 1102` paulson@13221 ` 1103` ```(*Krzysztof Grabczewski's proof that the converse of a finite, well-ordered ``` paulson@13221 ` 1104` ``` set is well-ordered. Proofs simplified by lcp. *) ``` paulson@13221 ` 1105` paulson@46877 ` 1106` ```lemma nat_wf_on_converse_Memrel: "n \ nat ==> wf[n](converse(Memrel(n)))" ``` paulson@47018 ` 1107` ```proof (induct n rule: nat_induct) ``` paulson@47018 ` 1108` ``` case 0 thus ?case by (blast intro: wf_onI) ``` paulson@47018 ` 1109` ```next ``` paulson@47018 ` 1110` ``` case (succ x) ``` paulson@47018 ` 1111` ``` hence wfx: "\Z. Z = 0 \ (\z\Z. \y. z \ y \ z \ x \ y \ x \ z \ x \ y \ Z)" ``` wenzelm@61798 ` 1112` ``` by (simp add: wf_on_def wf_def) \\not easy to erase the duplicate @{term"z \ x"}!\ ``` paulson@47018 ` 1113` ``` show ?case ``` paulson@47018 ` 1114` ``` proof (rule wf_onI) ``` paulson@47018 ` 1115` ``` fix Z u ``` paulson@47018 ` 1116` ``` assume Z: "u \ Z" "\z\Z. \y\Z. \y, z\ \ converse(Memrel(succ(x)))" ``` paulson@47018 ` 1117` ``` show False ``` paulson@47018 ` 1118` ``` proof (cases "x \ Z") ``` paulson@47018 ` 1119` ``` case True thus False using Z ``` paulson@47018 ` 1120` ``` by (blast elim: mem_irrefl mem_asym) ``` paulson@47018 ` 1121` ``` next ``` paulson@47018 ` 1122` ``` case False thus False using wfx [of Z] Z ``` paulson@47018 ` 1123` ``` by blast ``` paulson@47018 ` 1124` ``` qed ``` paulson@47018 ` 1125` ``` qed ``` paulson@47018 ` 1126` ```qed ``` paulson@13221 ` 1127` paulson@46877 ` 1128` ```lemma nat_well_ord_converse_Memrel: "n \ nat ==> well_ord(n,converse(Memrel(n)))" ``` paulson@13221 ` 1129` ```apply (frule Ord_nat [THEN Ord_in_Ord, THEN well_ord_Memrel]) ``` paulson@47018 ` 1130` ```apply (simp add: well_ord_def tot_ord_converse nat_wf_on_converse_Memrel) ``` paulson@13221 ` 1131` ```done ``` paulson@13221 ` 1132` paulson@13221 ` 1133` ```lemma well_ord_converse: ``` paulson@46820 ` 1134` ``` "[|well_ord(A,r); ``` paulson@13221 ` 1135` ``` well_ord(ordertype(A,r), converse(Memrel(ordertype(A, r)))) |] ``` paulson@13221 ` 1136` ``` ==> well_ord(A,converse(r))" ``` paulson@13221 ` 1137` ```apply (rule well_ord_Int_iff [THEN iffD1]) ``` paulson@13221 ` 1138` ```apply (frule ordermap_bij [THEN bij_is_inj, THEN well_ord_rvimage], assumption) ``` paulson@13221 ` 1139` ```apply (simp add: rvimage_converse converse_Int converse_prod ``` paulson@13221 ` 1140` ``` ordertype_ord_iso [THEN ord_iso_rvimage_eq]) ``` paulson@13221 ` 1141` ```done ``` paulson@13221 ` 1142` paulson@13221 ` 1143` ```lemma ordertype_eq_n: ``` paulson@46953 ` 1144` ``` assumes r: "well_ord(A,r)" and A: "A \ n" and n: "n \ nat" ``` paulson@46877 ` 1145` ``` shows "ordertype(A,r) = n" ``` paulson@46877 ` 1146` ```proof - ``` paulson@46953 ` 1147` ``` have "ordertype(A,r) \ A" ``` paulson@46953 ` 1148` ``` by (blast intro: bij_imp_eqpoll bij_converse_bij ordermap_bij r) ``` paulson@46877 ` 1149` ``` also have "... \ n" by (rule A) ``` paulson@46877 ` 1150` ``` finally have "ordertype(A,r) \ n" . ``` paulson@46877 ` 1151` ``` thus ?thesis ``` paulson@46953 ` 1152` ``` by (simp add: Ord_nat_eqpoll_iff Ord_ordertype n r) ``` paulson@46877 ` 1153` ```qed ``` paulson@13221 ` 1154` paulson@46820 ` 1155` ```lemma Finite_well_ord_converse: ``` paulson@13221 ` 1156` ``` "[| Finite(A); well_ord(A,r) |] ==> well_ord(A,converse(r))" ``` paulson@13221 ` 1157` ```apply (unfold Finite_def) ``` paulson@13221 ` 1158` ```apply (rule well_ord_converse, assumption) ``` paulson@13221 ` 1159` ```apply (blast dest: ordertype_eq_n intro!: nat_well_ord_converse_Memrel) ``` paulson@13221 ` 1160` ```done ``` paulson@13221 ` 1161` paulson@46877 ` 1162` ```lemma nat_into_Finite: "n \ nat ==> Finite(n)" ``` paulson@47018 ` 1163` ``` by (auto simp add: Finite_def intro: eqpoll_refl) ``` paulson@13221 ` 1164` paulson@46877 ` 1165` ```lemma nat_not_Finite: "~ Finite(nat)" ``` paulson@46877 ` 1166` ```proof - ``` paulson@46877 ` 1167` ``` { fix n ``` paulson@46877 ` 1168` ``` assume n: "n \ nat" "nat \ n" ``` paulson@46953 ` 1169` ``` have "n \ nat" by (rule n) ``` paulson@46877 ` 1170` ``` also have "... = n" using n ``` paulson@46953 ` 1171` ``` by (simp add: Ord_nat_eqpoll_iff Ord_nat) ``` paulson@46877 ` 1172` ``` finally have "n \ n" . ``` paulson@46953 ` 1173` ``` hence False ``` paulson@46953 ` 1174` ``` by (blast elim: mem_irrefl) ``` paulson@46877 ` 1175` ``` } ``` paulson@46877 ` 1176` ``` thus ?thesis ``` paulson@46953 ` 1177` ``` by (auto simp add: Finite_def) ``` paulson@46877 ` 1178` ```qed ``` paulson@14076 ` 1179` lcp@435 ` 1180` ```end ```