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