src/ZF/Cardinal.ML
 author lcp Fri, 23 Dec 1994 16:33:37 +0100 changeset 833 ba386650df2c parent 803 4c8333ab3eae child 845 825e96b87ef7 permissions -rw-r--r--
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, succ_eqpoll_succD, cons_lepoll_cons_iff, cons_eqpoll_cons_iff. Deleted inj_succ_succD. Streamlined proof of nat_lepoll_imp_le_lemma. Added Krzysztof's theorems diff_sing_lepoll, lepoll_diff_sing, diff_sing_eqpoll, lepoll_1_is_sing, inj_not_surj_succ, lesspoll_trans, lesspoll_lepoll_lesspoll, lepoll_lesspoll_lesspoll, lepoll_imp_lesspoll_succ, lesspoll_succ_imp_lepoll, lepoll_succ_disj, lepoll_nat_imp_Finite, lepoll_Finite, Finite_imp_cons_Finite, Finite_imp_succ_Finite, nat_le_infinite_Ord, nat_wf_on_converse_Memrel, nat_well_ord_converse_Memrel, well_ord_converse, ordertype_eq_n, Finite_well_ord_converse
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 1` ```(* Title: ZF/Cardinal.ML ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 2` ``` ID: \$Id\$ ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 3` ``` Author: Lawrence C Paulson, Cambridge University Computer Laboratory ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 4` ``` Copyright 1994 University of Cambridge ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 5` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 6` ```Cardinals in Zermelo-Fraenkel Set Theory ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 7` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 8` ```This theory does NOT assume the Axiom of Choice ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 9` ```*) ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 10` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 11` ```open Cardinal; ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 12` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 13` ```(*** The Schroeder-Bernstein Theorem -- see Davey & Priestly, page 106 ***) ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 14` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 15` ```(** Lemma: Banach's Decomposition Theorem **) ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 16` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 17` ```goal Cardinal.thy "bnd_mono(X, %W. X - g``(Y - f``W))"; ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 18` ```by (rtac bnd_monoI 1); ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 19` ```by (REPEAT (ares_tac [Diff_subset, subset_refl, Diff_mono, image_mono] 1)); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 20` ```qed "decomp_bnd_mono"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 21` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 22` ```val [gfun] = goal Cardinal.thy ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 23` ``` "g: Y->X ==> \ ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 24` ```\ g``(Y - f`` lfp(X, %W. X - g``(Y - f``W))) = \ ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 25` ```\ X - lfp(X, %W. X - g``(Y - f``W)) "; ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 26` ```by (res_inst_tac [("P", "%u. ?v = X-u")] ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 27` ``` (decomp_bnd_mono RS lfp_Tarski RS ssubst) 1); ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 28` ```by (simp_tac (ZF_ss addsimps [subset_refl, double_complement, ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 29` ``` gfun RS fun_is_rel RS image_subset]) 1); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 30` ```qed "Banach_last_equation"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 31` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 32` ```val prems = goal Cardinal.thy ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 33` ``` "[| f: X->Y; g: Y->X |] ==> \ ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 34` ```\ EX XA XB YA YB. (XA Int XB = 0) & (XA Un XB = X) & \ ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 35` ```\ (YA Int YB = 0) & (YA Un YB = Y) & \ ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 36` ```\ f``XA=YA & g``YB=XB"; ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 37` ```by (REPEAT ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 38` ``` (FIRSTGOAL ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 39` ``` (resolve_tac [refl, exI, conjI, Diff_disjoint, Diff_partition]))); ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 40` ```by (rtac Banach_last_equation 3); ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 41` ```by (REPEAT (resolve_tac (prems@[fun_is_rel, image_subset, lfp_subset]) 1)); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 42` ```qed "decomposition"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 43` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 44` ```val prems = goal Cardinal.thy ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 45` ``` "[| f: inj(X,Y); g: inj(Y,X) |] ==> EX h. h: bij(X,Y)"; ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 46` ```by (cut_facts_tac prems 1); ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 47` ```by (cut_facts_tac [(prems RL [inj_is_fun]) MRS decomposition] 1); ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 48` ```by (fast_tac (ZF_cs addSIs [restrict_bij,bij_disjoint_Un] ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 49` ``` addIs [bij_converse_bij]) 1); ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 50` ```(* The instantiation of exI to "restrict(f,XA) Un converse(restrict(g,YB))" ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 51` ``` is forced by the context!! *) ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 52` ```qed "schroeder_bernstein"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 53` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 54` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 55` ```(** Equipollence is an equivalence relation **) ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 56` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 57` ```goalw Cardinal.thy [eqpoll_def] "X eqpoll X"; ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 58` ```by (rtac exI 1); ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 59` ```by (rtac id_bij 1); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 60` ```qed "eqpoll_refl"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 61` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 62` ```goalw Cardinal.thy [eqpoll_def] "!!X Y. X eqpoll Y ==> Y eqpoll X"; ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 63` ```by (fast_tac (ZF_cs addIs [bij_converse_bij]) 1); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 64` ```qed "eqpoll_sym"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 65` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 66` ```goalw Cardinal.thy [eqpoll_def] ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 67` ``` "!!X Y. [| X eqpoll Y; Y eqpoll Z |] ==> X eqpoll Z"; ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 68` ```by (fast_tac (ZF_cs addIs [comp_bij]) 1); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 69` ```qed "eqpoll_trans"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 70` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 71` ```(** Le-pollence is a partial ordering **) ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 72` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 73` ```goalw Cardinal.thy [lepoll_def] "!!X Y. X<=Y ==> X lepoll Y"; ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 74` ```by (rtac exI 1); ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 75` ```by (etac id_subset_inj 1); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 76` ```qed "subset_imp_lepoll"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 77` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 78` ```val lepoll_refl = subset_refl RS subset_imp_lepoll; ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 79` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 80` ```goalw Cardinal.thy [eqpoll_def, bij_def, lepoll_def] ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 81` ``` "!!X Y. X eqpoll Y ==> X lepoll Y"; ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 82` ```by (fast_tac ZF_cs 1); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 83` ```qed "eqpoll_imp_lepoll"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 84` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 85` ```goalw Cardinal.thy [lepoll_def] ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 86` ``` "!!X Y. [| X lepoll Y; Y lepoll Z |] ==> X lepoll Z"; ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 87` ```by (fast_tac (ZF_cs addIs [comp_inj]) 1); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 88` ```qed "lepoll_trans"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 89` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 90` ```(*Asymmetry law*) ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 91` ```goalw Cardinal.thy [lepoll_def,eqpoll_def] ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 92` ``` "!!X Y. [| X lepoll Y; Y lepoll X |] ==> X eqpoll Y"; ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 93` ```by (REPEAT (etac exE 1)); ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 94` ```by (rtac schroeder_bernstein 1); ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 95` ```by (REPEAT (assume_tac 1)); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 96` ```qed "eqpollI"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 97` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 98` ```val [major,minor] = goal Cardinal.thy ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 99` ``` "[| X eqpoll Y; [| X lepoll Y; Y lepoll X |] ==> P |] ==> P"; ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 100` ```by (rtac minor 1); ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 101` ```by (REPEAT (resolve_tac [major, eqpoll_imp_lepoll, eqpoll_sym] 1)); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 102` ```qed "eqpollE"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 103` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 104` ```goal Cardinal.thy "X eqpoll Y <-> X lepoll Y & Y lepoll X"; ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 105` ```by (fast_tac (ZF_cs addIs [eqpollI] addSEs [eqpollE]) 1); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 106` ```qed "eqpoll_iff"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 107` 833 ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 108` ```goalw Cardinal.thy [lepoll_def, inj_def] "!!A. A lepoll 0 ==> A = 0"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 109` ```by (fast_tac (eq_cs addDs [apply_type]) 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 110` ```qed "lepoll_0_is_0"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 111` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 112` ```(*0 lepoll Y*) ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 113` ```bind_thm ("empty_lepollI", empty_subsetI RS subset_imp_lepoll); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 114` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 115` ```(*A eqpoll 0 ==> A=0*) ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 116` ```bind_thm ("eqpoll_0_is_0", eqpoll_imp_lepoll RS lepoll_0_is_0); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 117` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 118` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 119` ```(*** lesspoll: contributions by Krzysztof Grabczewski ***) ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 120` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 121` ```goalw Cardinal.thy [inj_def, surj_def] ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 122` ``` "!!f. [| f : inj(A, succ(m)); f ~: surj(A, succ(m)) |] ==> EX f. f:inj(A,m)"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 123` ```by (safe_tac lemmas_cs); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 124` ```by (swap_res_tac [exI] 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 125` ```by (res_inst_tac [("a", "lam z:A. if(f`z=m, y, f`z)")] CollectI 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 126` ```by (fast_tac (ZF_cs addSIs [if_type RS lam_type] ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 127` ``` addEs [apply_funtype RS succE]) 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 128` ```(*Proving it's injective*) ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 129` ```by (asm_simp_tac (ZF_ss setloop split_tac [expand_if]) 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 130` ```by (fast_tac ZF_cs 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 131` ```qed "inj_not_surj_succ"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 132` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 133` ```(** Variations on transitivity **) ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 134` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 135` ```goalw Cardinal.thy [lesspoll_def] ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 136` ``` "!!X. [| X lesspoll Y; Y lesspoll Z |] ==> X lesspoll Z"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 137` ```by (fast_tac (ZF_cs addSIs [eqpollI] addSEs [eqpollE] addIs [lepoll_trans]) 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 138` ```qed "lesspoll_trans"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 139` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 140` ```goalw Cardinal.thy [lesspoll_def] ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 141` ``` "!!X. [| X lesspoll Y; Y lepoll Z |] ==> X lesspoll Z"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 142` ```by (fast_tac (ZF_cs addSIs [eqpollI] addSEs [eqpollE] addIs [lepoll_trans]) 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 143` ```qed "lesspoll_lepoll_lesspoll"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 144` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 145` ```goalw Cardinal.thy [lesspoll_def] ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 146` ``` "!!X. [| X lesspoll Y; Z lepoll X |] ==> Z lesspoll Y"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 147` ```by (fast_tac (ZF_cs addSIs [eqpollI] addSEs [eqpollE] addIs [lepoll_trans]) 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 148` ```qed "lepoll_lesspoll_lesspoll"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 149` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 150` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 151` ```(** LEAST -- the least number operator [from HOL/Univ.ML] **) ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 152` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 153` ```val [premP,premOrd,premNot] = goalw Cardinal.thy [Least_def] ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 154` ``` "[| P(i); Ord(i); !!x. x ~P(x) |] ==> (LEAST x.P(x)) = i"; ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 155` ```by (rtac the_equality 1); ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 156` ```by (fast_tac (ZF_cs addSIs [premP,premOrd,premNot]) 1); ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 157` ```by (REPEAT (etac conjE 1)); ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 158` ```by (etac (premOrd RS Ord_linear_lt) 1); ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 159` ```by (ALLGOALS (fast_tac (ZF_cs addSIs [premP] addSDs [premNot]))); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 160` ```qed "Least_equality"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 161` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 162` ```goal Cardinal.thy "!!i. [| P(i); Ord(i) |] ==> P(LEAST x.P(x))"; ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 163` ```by (etac rev_mp 1); ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 164` ```by (trans_ind_tac "i" [] 1); ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 165` ```by (rtac impI 1); ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 166` ```by (rtac classical 1); ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 167` ```by (EVERY1 [rtac (Least_equality RS ssubst), assume_tac, assume_tac]); ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 168` ```by (assume_tac 2); ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 169` ```by (fast_tac (ZF_cs addSEs [ltE]) 1); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 170` ```qed "LeastI"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 171` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 172` ```(*Proof is almost identical to the one above!*) ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 173` ```goal Cardinal.thy "!!i. [| P(i); Ord(i) |] ==> (LEAST x.P(x)) le i"; ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 174` ```by (etac rev_mp 1); ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 175` ```by (trans_ind_tac "i" [] 1); ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 176` ```by (rtac impI 1); ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 177` ```by (rtac classical 1); ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 178` ```by (EVERY1 [rtac (Least_equality RS ssubst), assume_tac, assume_tac]); ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 179` ```by (etac le_refl 2); ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 180` ```by (fast_tac (ZF_cs addEs [ltE, lt_trans1] addIs [leI, ltI]) 1); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 181` ```qed "Least_le"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 182` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 183` ```(*LEAST really is the smallest*) ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 184` ```goal Cardinal.thy "!!i. [| P(i); i < (LEAST x.P(x)) |] ==> Q"; ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 185` ```by (rtac (Least_le RSN (2,lt_trans2) RS lt_irrefl) 1); ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 186` ```by (REPEAT (eresolve_tac [asm_rl, ltE] 1)); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 187` ```qed "less_LeastE"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 188` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 189` ```(*If there is no such P then LEAST is vacuously 0*) ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 190` ```goalw Cardinal.thy [Least_def] ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 191` ``` "!!P. [| ~ (EX i. Ord(i) & P(i)) |] ==> (LEAST x.P(x)) = 0"; ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 192` ```by (rtac the_0 1); ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 193` ```by (fast_tac ZF_cs 1); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 194` ```qed "Least_0"; ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 195` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 196` ```goal Cardinal.thy "Ord(LEAST x.P(x))"; ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 197` ```by (excluded_middle_tac "EX i. Ord(i) & P(i)" 1); ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 198` ```by (safe_tac ZF_cs); ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 199` ```by (rtac (Least_le RS ltE) 2); ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 200` ```by (REPEAT_SOME assume_tac); ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 201` ```by (etac (Least_0 RS ssubst) 1); ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 202` ```by (rtac Ord_0 1); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 203` ```qed "Ord_Least"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 204` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 205` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 206` ```(** Basic properties of cardinals **) ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 207` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 208` ```(*Not needed for simplification, but helpful below*) ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 209` ```val prems = goal Cardinal.thy ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 210` ``` "[| !!y. P(y) <-> Q(y) |] ==> (LEAST x.P(x)) = (LEAST x.Q(x))"; ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 211` ```by (simp_tac (FOL_ss addsimps prems) 1); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 212` ```qed "Least_cong"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 213` 765 06a484afc603 Card_cardinal_le: new lcp parents: 760 diff changeset ` 214` ```(*Need AC to prove X lepoll Y ==> |X| le |Y| ; ``` 06a484afc603 Card_cardinal_le: new lcp parents: 760 diff changeset ` 215` ``` see well_ord_lepoll_imp_Card_le *) ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 216` ```goalw Cardinal.thy [eqpoll_def,cardinal_def] "!!X Y. X eqpoll Y ==> |X| = |Y|"; ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 217` ```by (rtac Least_cong 1); ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 218` ```by (fast_tac (ZF_cs addEs [comp_bij,bij_converse_bij]) 1); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 219` ```qed "cardinal_cong"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 220` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 221` ```(*Under AC, the premise becomes trivial; one consequence is ||A|| = |A|*) ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 222` ```goalw Cardinal.thy [eqpoll_def, cardinal_def] ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 223` ``` "!!A. well_ord(A,r) ==> |A| eqpoll A"; ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 224` ```by (rtac LeastI 1); ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 225` ```by (etac Ord_ordertype 2); ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 226` ```by (rtac exI 1); ``` 467 92868dab2939 new cardinal arithmetic developments lcp parents: 437 diff changeset ` 227` ```by (etac (ordermap_bij RS bij_converse_bij) 1); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 228` ```qed "well_ord_cardinal_eqpoll"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 229` 803 4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result", lcp parents: 792 diff changeset ` 230` ```bind_thm ("Ord_cardinal_eqpoll", well_ord_Memrel RS well_ord_cardinal_eqpoll); ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 231` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 232` ```goal Cardinal.thy ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 233` ``` "!!X Y. [| well_ord(X,r); well_ord(Y,s); |X| = |Y| |] ==> X eqpoll Y"; ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 234` ```by (rtac (eqpoll_sym RS eqpoll_trans) 1); ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 235` ```by (etac well_ord_cardinal_eqpoll 1); ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 236` ```by (asm_simp_tac (ZF_ss addsimps [well_ord_cardinal_eqpoll]) 1); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 237` ```qed "well_ord_cardinal_eqE"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 238` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 239` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 240` ```(** Observations from Kunen, page 28 **) ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 241` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 242` ```goalw Cardinal.thy [cardinal_def] "!!i. Ord(i) ==> |i| le i"; ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 243` ```by (etac (eqpoll_refl RS Least_le) 1); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 244` ```qed "Ord_cardinal_le"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 245` 484 70b789956bd3 Axiom of choice, cardinality results, etc. lcp parents: 467 diff changeset ` 246` ```goalw Cardinal.thy [Card_def] "!!K. Card(K) ==> |K| = K"; ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 247` ```by (etac sym 1); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 248` ```qed "Card_cardinal_eq"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 249` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 250` ```val prems = goalw Cardinal.thy [Card_def,cardinal_def] ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 251` ``` "[| Ord(i); !!j. j ~(j eqpoll i) |] ==> Card(i)"; ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 252` ```by (rtac (Least_equality RS ssubst) 1); ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 253` ```by (REPEAT (ares_tac ([refl,eqpoll_refl]@prems) 1)); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 254` ```qed "CardI"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 255` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 256` ```goalw Cardinal.thy [Card_def, cardinal_def] "!!i. Card(i) ==> Ord(i)"; ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 257` ```by (etac ssubst 1); ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 258` ```by (rtac Ord_Least 1); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 259` ```qed "Card_is_Ord"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 260` 765 06a484afc603 Card_cardinal_le: new lcp parents: 760 diff changeset ` 261` ```goal Cardinal.thy "!!K. Card(K) ==> K le |K|"; ``` 06a484afc603 Card_cardinal_le: new lcp parents: 760 diff changeset ` 262` ```by (asm_simp_tac (ZF_ss addsimps [le_refl, Card_is_Ord, Card_cardinal_eq]) 1); ``` 782 200a16083201 added bind_thm for theorems defined by "standard ..." clasohm parents: 765 diff changeset ` 263` ```qed "Card_cardinal_le"; ``` 765 06a484afc603 Card_cardinal_le: new lcp parents: 760 diff changeset ` 264` 484 70b789956bd3 Axiom of choice, cardinality results, etc. lcp parents: 467 diff changeset ` 265` ```goalw Cardinal.thy [cardinal_def] "Ord(|A|)"; ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 266` ```by (rtac Ord_Least 1); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 267` ```qed "Ord_cardinal"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 268` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 269` ```goal Cardinal.thy "Card(0)"; ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 270` ```by (rtac (Ord_0 RS CardI) 1); ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 271` ```by (fast_tac (ZF_cs addSEs [ltE]) 1); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 272` ```qed "Card_0"; ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 273` 522 e1de521e012a ZF/Cardinal/Card_Un: new lcp parents: 484 diff changeset ` 274` ```val [premK,premL] = goal Cardinal.thy ``` e1de521e012a ZF/Cardinal/Card_Un: new lcp parents: 484 diff changeset ` 275` ``` "[| Card(K); Card(L) |] ==> Card(K Un L)"; ``` e1de521e012a ZF/Cardinal/Card_Un: new lcp parents: 484 diff changeset ` 276` ```by (rtac ([premK RS Card_is_Ord, premL RS Card_is_Ord] MRS Ord_linear_le) 1); ``` e1de521e012a ZF/Cardinal/Card_Un: new lcp parents: 484 diff changeset ` 277` ```by (asm_simp_tac ``` e1de521e012a ZF/Cardinal/Card_Un: new lcp parents: 484 diff changeset ` 278` ``` (ZF_ss addsimps [premL, le_imp_subset, subset_Un_iff RS iffD1]) 1); ``` e1de521e012a ZF/Cardinal/Card_Un: new lcp parents: 484 diff changeset ` 279` ```by (asm_simp_tac ``` e1de521e012a ZF/Cardinal/Card_Un: new lcp parents: 484 diff changeset ` 280` ``` (ZF_ss addsimps [premK, le_imp_subset, subset_Un_iff2 RS iffD1]) 1); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 281` ```qed "Card_Un"; ``` 522 e1de521e012a ZF/Cardinal/Card_Un: new lcp parents: 484 diff changeset ` 282` e1de521e012a ZF/Cardinal/Card_Un: new lcp parents: 484 diff changeset ` 283` ```(*Infinite unions of cardinals? See Devlin, Lemma 6.7, page 98*) ``` e1de521e012a ZF/Cardinal/Card_Un: new lcp parents: 484 diff changeset ` 284` 484 70b789956bd3 Axiom of choice, cardinality results, etc. lcp parents: 467 diff changeset ` 285` ```goalw Cardinal.thy [cardinal_def] "Card(|A|)"; ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 286` ```by (excluded_middle_tac "EX i. Ord(i) & i eqpoll A" 1); ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 287` ```by (etac (Least_0 RS ssubst) 1 THEN rtac Card_0 1); ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 288` ```by (rtac (Ord_Least RS CardI) 1); ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 289` ```by (safe_tac ZF_cs); ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 290` ```by (rtac less_LeastE 1); ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 291` ```by (assume_tac 2); ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 292` ```by (etac eqpoll_trans 1); ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 293` ```by (REPEAT (ares_tac [LeastI] 1)); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 294` ```qed "Card_cardinal"; ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 295` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 296` ```(*Kunen's Lemma 10.5*) ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 297` ```goal Cardinal.thy "!!i j. [| |i| le j; j le i |] ==> |j| = |i|"; ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 298` ```by (rtac (eqpollI RS cardinal_cong) 1); ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 299` ```by (etac (le_imp_subset RS subset_imp_lepoll) 1); ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 300` ```by (rtac lepoll_trans 1); ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 301` ```by (etac (le_imp_subset RS subset_imp_lepoll) 2); ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 302` ```by (rtac (eqpoll_sym RS eqpoll_imp_lepoll) 1); ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 303` ```by (rtac Ord_cardinal_eqpoll 1); ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 304` ```by (REPEAT (eresolve_tac [ltE, Ord_succD] 1)); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 305` ```qed "cardinal_eq_lemma"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 306` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 307` ```goal Cardinal.thy "!!i j. i le j ==> |i| le |j|"; ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 308` ```by (res_inst_tac [("i","|i|"),("j","|j|")] Ord_linear_le 1); ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 309` ```by (REPEAT_FIRST (ares_tac [Ord_cardinal, le_eqI])); ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 310` ```by (rtac cardinal_eq_lemma 1); ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 311` ```by (assume_tac 2); ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 312` ```by (etac le_trans 1); ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 313` ```by (etac ltE 1); ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 314` ```by (etac Ord_cardinal_le 1); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 315` ```qed "cardinal_mono"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 316` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 317` ```(*Since we have |succ(nat)| le |nat|, the converse of cardinal_mono fails!*) ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 318` ```goal Cardinal.thy "!!i j. [| |i| < |j|; Ord(i); Ord(j) |] ==> i < j"; ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 319` ```by (rtac Ord_linear2 1); ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 320` ```by (REPEAT_SOME assume_tac); ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 321` ```by (etac (lt_trans2 RS lt_irrefl) 1); ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 322` ```by (etac cardinal_mono 1); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 323` ```qed "cardinal_lt_imp_lt"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 324` 484 70b789956bd3 Axiom of choice, cardinality results, etc. lcp parents: 467 diff changeset ` 325` ```goal Cardinal.thy "!!i j. [| |i| < K; Ord(i); Card(K) |] ==> i < K"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 326` ```by (asm_simp_tac (ZF_ss addsimps ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 327` ``` [cardinal_lt_imp_lt, Card_is_Ord, Card_cardinal_eq]) 1); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 328` ```qed "Card_lt_imp_lt"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 329` 484 70b789956bd3 Axiom of choice, cardinality results, etc. lcp parents: 467 diff changeset ` 330` ```goal Cardinal.thy "!!i j. [| Ord(i); Card(K) |] ==> (|i| < K) <-> (i < K)"; ``` 70b789956bd3 Axiom of choice, cardinality results, etc. lcp parents: 467 diff changeset ` 331` ```by (fast_tac (ZF_cs addEs [Card_lt_imp_lt, Ord_cardinal_le RS lt_trans1]) 1); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 332` ```qed "Card_lt_iff"; ``` 484 70b789956bd3 Axiom of choice, cardinality results, etc. lcp parents: 467 diff changeset ` 333` 70b789956bd3 Axiom of choice, cardinality results, etc. lcp parents: 467 diff changeset ` 334` ```goal Cardinal.thy "!!i j. [| Ord(i); Card(K) |] ==> (K le |i|) <-> (K le i)"; ``` 70b789956bd3 Axiom of choice, cardinality results, etc. lcp parents: 467 diff changeset ` 335` ```by (asm_simp_tac (ZF_ss addsimps ``` 70b789956bd3 Axiom of choice, cardinality results, etc. lcp parents: 467 diff changeset ` 336` ``` [Card_lt_iff, Card_is_Ord, Ord_cardinal, ``` 70b789956bd3 Axiom of choice, cardinality results, etc. lcp parents: 467 diff changeset ` 337` ``` not_lt_iff_le RS iff_sym]) 1); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 338` ```qed "Card_le_iff"; ``` 484 70b789956bd3 Axiom of choice, cardinality results, etc. lcp parents: 467 diff changeset ` 339` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 340` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 341` ```(*** The finite cardinals ***) ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 342` 833 ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 343` ```goalw Cardinal.thy [lepoll_def, inj_def] ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 344` ``` "!!A B. [| cons(u,A) lepoll cons(v,B); u~:A; v~:B |] ==> A lepoll B"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 345` ```by (safe_tac ZF_cs); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 346` ```by (res_inst_tac [("x", "lam x:A. if(f`x=v, f`u, f`x)")] exI 1); ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 347` ```by (rtac CollectI 1); ``` 833 ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 348` ```(*Proving it's in the function space A->B*) ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 349` ```by (rtac (if_type RS lam_type) 1); ``` 833 ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 350` ```by (fast_tac (ZF_cs addEs [apply_funtype RS consE]) 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 351` ```by (fast_tac (ZF_cs addSEs [mem_irrefl] addEs [apply_funtype RS consE]) 1); ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 352` ```(*Proving it's injective*) ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 353` ```by (asm_simp_tac (ZF_ss setloop split_tac [expand_if]) 1); ``` 833 ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 354` ```by (fast_tac ZF_cs 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 355` ```qed "cons_lepoll_consD"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 356` 833 ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 357` ```goal Cardinal.thy ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 358` ``` "!!A B. [| cons(u,A) eqpoll cons(v,B); u~:A; v~:B |] ==> A eqpoll B"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 359` ```by (asm_full_simp_tac (ZF_ss addsimps [eqpoll_iff]) 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 360` ```by (fast_tac (ZF_cs addIs [cons_lepoll_consD]) 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 361` ```qed "cons_eqpoll_consD"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 362` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 363` ```(*Lemma suggested by Mike Fourman*) ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 364` ```goalw Cardinal.thy [succ_def] "!!m n. succ(m) lepoll succ(n) ==> m lepoll n"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 365` ```by (etac cons_lepoll_consD 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 366` ```by (REPEAT (rtac mem_not_refl 1)); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 367` ```qed "succ_lepoll_succD"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 368` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 369` ```val [prem] = goal Cardinal.thy ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 370` ``` "m:nat ==> ALL n: nat. m lepoll n --> m le n"; ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 371` ```by (nat_ind_tac "m" [prem] 1); ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 372` ```by (fast_tac (ZF_cs addSIs [nat_0_le]) 1); ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 373` ```by (rtac ballI 1); ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 374` ```by (eres_inst_tac [("n","n")] natE 1); ``` 833 ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 375` ```by (asm_simp_tac (ZF_ss addsimps [lepoll_def, inj_def, ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 376` ``` succI1 RS Pi_empty2]) 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 377` ```by (fast_tac (ZF_cs addSIs [succ_leI] addSDs [succ_lepoll_succD]) 1); ``` 803 4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result", lcp parents: 792 diff changeset ` 378` ```val nat_lepoll_imp_le_lemma = result(); ``` 4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result", lcp parents: 792 diff changeset ` 379` 4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result", lcp parents: 792 diff changeset ` 380` ```bind_thm ("nat_lepoll_imp_le", nat_lepoll_imp_le_lemma RS bspec RS mp); ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 381` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 382` ```goal Cardinal.thy ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 383` ``` "!!m n. [| m:nat; n: nat |] ==> m eqpoll n <-> m = n"; ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 384` ```by (rtac iffI 1); ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 385` ```by (asm_simp_tac (ZF_ss addsimps [eqpoll_refl]) 2); ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 386` ```by (fast_tac (ZF_cs addIs [nat_lepoll_imp_le, le_anti_sym] ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 387` ``` addSEs [eqpollE]) 1); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 388` ```qed "nat_eqpoll_iff"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 389` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 390` ```goalw Cardinal.thy [Card_def,cardinal_def] ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 391` ``` "!!n. n: nat ==> Card(n)"; ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 392` ```by (rtac (Least_equality RS ssubst) 1); ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 393` ```by (REPEAT_FIRST (ares_tac [eqpoll_refl, nat_into_Ord, refl])); ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 394` ```by (asm_simp_tac (ZF_ss addsimps [lt_nat_in_nat RS nat_eqpoll_iff]) 1); ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 395` ```by (fast_tac (ZF_cs addSEs [lt_irrefl]) 1); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 396` ```qed "nat_into_Card"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 397` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 398` ```(*Part of Kunen's Lemma 10.6*) ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 399` ```goal Cardinal.thy "!!n. [| succ(n) lepoll n; n:nat |] ==> P"; ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 400` ```by (rtac (nat_lepoll_imp_le RS lt_irrefl) 1); ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 401` ```by (REPEAT (ares_tac [nat_succI] 1)); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 402` ```qed "succ_lepoll_natE"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 403` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 404` 833 ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 405` ```(** lepoll, lesspoll and natural numbers **) ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 406` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 407` ```goalw Cardinal.thy [lesspoll_def] ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 408` ``` "!!m. [| A lepoll m; m:nat |] ==> A lesspoll succ(m)"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 409` ```by (rtac conjI 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 410` ```by (fast_tac (ZF_cs addIs [subset_imp_lepoll RSN (2,lepoll_trans)]) 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 411` ```by (rtac notI 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 412` ```by (dresolve_tac [eqpoll_sym RS eqpoll_imp_lepoll] 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 413` ```by (dtac lepoll_trans 1 THEN assume_tac 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 414` ```by (etac succ_lepoll_natE 1 THEN assume_tac 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 415` ```qed "lepoll_imp_lesspoll_succ"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 416` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 417` ```goalw Cardinal.thy [lesspoll_def, lepoll_def, eqpoll_def, bij_def] ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 418` ``` "!!m. [| A lesspoll succ(m); m:nat |] ==> A lepoll m"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 419` ```by (step_tac ZF_cs 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 420` ```by (fast_tac (ZF_cs addSIs [inj_not_surj_succ]) 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 421` ```qed "lesspoll_succ_imp_lepoll"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 422` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 423` ```goal Cardinal.thy "!!A m. [| A lepoll succ(m); m:nat |] ==> \ ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 424` ```\ A lepoll m | A eqpoll succ(m)"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 425` ```by (rtac disjCI 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 426` ```by (rtac lesspoll_succ_imp_lepoll 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 427` ```by (assume_tac 2); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 428` ```by (asm_simp_tac (ZF_ss addsimps [lesspoll_def]) 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 429` ```qed "lepoll_succ_disj"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 430` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 431` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 432` ```(*** The first infinite cardinal: Omega, or nat ***) ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 433` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 434` ```(*This implies Kunen's Lemma 10.6*) ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 435` ```goal Cardinal.thy "!!n. [| n ~ i lepoll n"; ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 436` ```by (rtac notI 1); ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 437` ```by (rtac succ_lepoll_natE 1 THEN assume_tac 2); ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 438` ```by (rtac lepoll_trans 1 THEN assume_tac 2); ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 439` ```by (etac ltE 1); ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 440` ```by (REPEAT (ares_tac [Ord_succ_subsetI RS subset_imp_lepoll] 1)); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 441` ```qed "lt_not_lepoll"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 442` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 443` ```goal Cardinal.thy "!!i n. [| Ord(i); n:nat |] ==> i eqpoll n <-> i=n"; ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 444` ```by (rtac iffI 1); ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 445` ```by (asm_simp_tac (ZF_ss addsimps [eqpoll_refl]) 2); ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 446` ```by (rtac Ord_linear_lt 1); ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 447` ```by (REPEAT_SOME (eresolve_tac [asm_rl, nat_into_Ord])); ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 448` ```by (etac (lt_nat_in_nat RS nat_eqpoll_iff RS iffD1) 1 THEN ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 449` ``` REPEAT (assume_tac 1)); ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 450` ```by (rtac (lt_not_lepoll RS notE) 1 THEN (REPEAT (assume_tac 1))); ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 451` ```by (etac eqpoll_imp_lepoll 1); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 452` ```qed "Ord_nat_eqpoll_iff"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 453` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 454` ```goalw Cardinal.thy [Card_def,cardinal_def] "Card(nat)"; ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 455` ```by (rtac (Least_equality RS ssubst) 1); ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 456` ```by (REPEAT_FIRST (ares_tac [eqpoll_refl, Ord_nat, refl])); ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 457` ```by (etac ltE 1); ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 458` ```by (asm_simp_tac (ZF_ss addsimps [eqpoll_iff, lt_not_lepoll, ltI]) 1); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 459` ```qed "Card_nat"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 460` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 461` ```(*Allows showing that |i| is a limit cardinal*) ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 462` ```goal Cardinal.thy "!!i. nat le i ==> nat le |i|"; ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 463` ```by (rtac (Card_nat RS Card_cardinal_eq RS subst) 1); ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 464` ```by (etac cardinal_mono 1); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 465` ```qed "nat_le_cardinal"; ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 466` 571 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 467` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 468` ```(*** Towards Cardinal Arithmetic ***) ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 469` ```(** Congruence laws for successor, cardinal addition and multiplication **) ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 470` 792 5d2a7634da46 case_ss: now built upon ZF/Order/bij_inverse_ss. Deleted lcp parents: 782 diff changeset ` 471` ```val case_ss = ``` 5d2a7634da46 case_ss: now built upon ZF/Order/bij_inverse_ss. Deleted lcp parents: 782 diff changeset ` 472` ``` bij_inverse_ss addsimps [Inl_iff, Inl_Inr_iff, Inr_iff, Inr_Inl_iff, ``` 5d2a7634da46 case_ss: now built upon ZF/Order/bij_inverse_ss. Deleted lcp parents: 782 diff changeset ` 473` ``` case_Inl, case_Inr, InlI, InrI]; ``` 571 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 474` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 475` ```(*Congruence law for cons under equipollence*) ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 476` ```goalw Cardinal.thy [lepoll_def] ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 477` ``` "!!A B. [| A lepoll B; b ~: B |] ==> cons(a,A) lepoll cons(b,B)"; ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 478` ```by (safe_tac ZF_cs); ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 479` ```by (res_inst_tac [("x", "lam y: cons(a,A).if(y=a, b, f`y)")] exI 1); ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 480` ```by (res_inst_tac [("d","%z.if(z:B, converse(f)`z, a)")] ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 481` ``` lam_injective 1); ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 482` ```by (asm_simp_tac (ZF_ss addsimps [inj_is_fun RS apply_type, cons_iff] ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 483` ``` setloop etac consE') 1); ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 484` ```by (asm_simp_tac (ZF_ss addsimps [inj_is_fun RS apply_type, left_inverse] ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 485` ``` setloop etac consE') 1); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 486` ```qed "cons_lepoll_cong"; ``` 571 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 487` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 488` ```goal Cardinal.thy ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 489` ``` "!!A B. [| A eqpoll B; a ~: A; b ~: B |] ==> cons(a,A) eqpoll cons(b,B)"; ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 490` ```by (asm_full_simp_tac (ZF_ss addsimps [eqpoll_iff, cons_lepoll_cong]) 1); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 491` ```qed "cons_eqpoll_cong"; ``` 571 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 492` 833 ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 493` ```goal Cardinal.thy ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 494` ``` "!!A B. [| a ~: A; b ~: B |] ==> \ ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 495` ```\ cons(a,A) lepoll cons(b,B) <-> A lepoll B"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 496` ```by (fast_tac (ZF_cs addIs [cons_lepoll_cong, cons_lepoll_consD]) 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 497` ```qed "cons_lepoll_cons_iff"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 498` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 499` ```goal Cardinal.thy ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 500` ``` "!!A B. [| a ~: A; b ~: B |] ==> \ ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 501` ```\ cons(a,A) eqpoll cons(b,B) <-> A eqpoll B"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 502` ```by (fast_tac (ZF_cs addIs [cons_eqpoll_cong, cons_eqpoll_consD]) 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 503` ```qed "cons_eqpoll_cons_iff"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 504` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 505` ```goalw Cardinal.thy [succ_def] "{a} eqpoll 1"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 506` ```by (fast_tac (ZF_cs addSIs [eqpoll_refl RS cons_eqpoll_cong]) 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 507` ```qed "singleton_eqpoll_1"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 508` 571 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 509` ```(*Congruence law for succ under equipollence*) ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 510` ```goalw Cardinal.thy [succ_def] ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 511` ``` "!!A B. A eqpoll B ==> succ(A) eqpoll succ(B)"; ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 512` ```by (REPEAT (ares_tac [cons_eqpoll_cong, mem_not_refl] 1)); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 513` ```qed "succ_eqpoll_cong"; ``` 571 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 514` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 515` ```(*Congruence law for + under equipollence*) ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 516` ```goalw Cardinal.thy [eqpoll_def] ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 517` ``` "!!A B C D. [| A eqpoll C; B eqpoll D |] ==> A+B eqpoll C+D"; ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 518` ```by (safe_tac ZF_cs); ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 519` ```by (rtac exI 1); ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 520` ```by (res_inst_tac [("c", "case(%x. Inl(f`x), %y. Inr(fa`y))"), ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 521` ``` ("d", "case(%x. Inl(converse(f)`x), %y. Inr(converse(fa)`y))")] ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 522` ``` lam_bijective 1); ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 523` ```by (safe_tac (ZF_cs addSEs [sumE])); ``` 792 5d2a7634da46 case_ss: now built upon ZF/Order/bij_inverse_ss. Deleted lcp parents: 782 diff changeset ` 524` ```by (ALLGOALS (asm_simp_tac case_ss)); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 525` ```qed "sum_eqpoll_cong"; ``` 571 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 526` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 527` ```(*Congruence law for * under equipollence*) ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 528` ```goalw Cardinal.thy [eqpoll_def] ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 529` ``` "!!A B C D. [| A eqpoll C; B eqpoll D |] ==> A*B eqpoll C*D"; ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 530` ```by (safe_tac ZF_cs); ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 531` ```by (rtac exI 1); ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 532` ```by (res_inst_tac [("c", "split(%x y. )"), ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 533` ``` ("d", "split(%x y. )")] ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 534` ``` lam_bijective 1); ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 535` ```by (safe_tac ZF_cs); ``` 792 5d2a7634da46 case_ss: now built upon ZF/Order/bij_inverse_ss. Deleted lcp parents: 782 diff changeset ` 536` ```by (ALLGOALS (asm_simp_tac case_ss)); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 537` ```qed "prod_eqpoll_cong"; ``` 571 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 538` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 539` ```goalw Cardinal.thy [eqpoll_def] ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 540` ``` "!!f. [| f: inj(A,B); A Int B = 0 |] ==> A Un (B - range(f)) eqpoll B"; ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 541` ```by (rtac exI 1); ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 542` ```by (res_inst_tac [("c", "%x. if(x:A, f`x, x)"), ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 543` ``` ("d", "%y. if(y: range(f), converse(f)`y, y)")] ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 544` ``` lam_bijective 1); ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 545` ```by (fast_tac (ZF_cs addSIs [if_type, apply_type] addIs [inj_is_fun]) 1); ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 546` ```by (asm_simp_tac ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 547` ``` (ZF_ss addsimps [inj_converse_fun RS apply_funtype] ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 548` ``` setloop split_tac [expand_if]) 1); ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 549` ```by (asm_simp_tac (ZF_ss addsimps [inj_is_fun RS apply_rangeI, left_inverse] ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 550` ``` setloop etac UnE') 1); ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 551` ```by (asm_simp_tac ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 552` ``` (ZF_ss addsimps [inj_converse_fun RS apply_funtype, right_inverse] ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 553` ``` setloop split_tac [expand_if]) 1); ``` 0b03ce5b62f7 ZF/Cardinal: some results moved here from CardinalArith lcp parents: 522 diff changeset ` 554` ```by (fast_tac (ZF_cs addEs [equals0D]) 1); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 571 diff changeset ` 555` ```qed "inj_disjoint_eqpoll"; ``` 833 ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 556` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 557` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 558` ```(*** Lemmas by Krzysztof Grabczewski. New proofs using cons_lepoll_cons. ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 559` ``` Could easily generalise from succ to cons. ***) ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 560` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 561` ```goalw Cardinal.thy [succ_def] ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 562` ``` "!!A a n. [| a:A; A lepoll succ(n) |] ==> A - {a} lepoll n"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 563` ```by (rtac cons_lepoll_consD 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 564` ```by (rtac mem_not_refl 3); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 565` ```by (eresolve_tac [cons_Diff RS ssubst] 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 566` ```by (safe_tac ZF_cs); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 567` ```qed "diff_sing_lepoll"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 568` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 569` ```goalw Cardinal.thy [succ_def] ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 570` ``` "!!A a n. [| a:A; succ(n) lepoll A |] ==> n lepoll A - {a}"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 571` ```by (rtac cons_lepoll_consD 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 572` ```by (rtac mem_not_refl 2); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 573` ```by (eresolve_tac [cons_Diff RS ssubst] 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 574` ```by (safe_tac ZF_cs); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 575` ```qed "lepoll_diff_sing"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 576` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 577` ```goal Cardinal.thy "!!A a n. [| a:A; A eqpoll succ(n) |] ==> A - {a} eqpoll n"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 578` ```by (fast_tac (ZF_cs addSIs [eqpollI] addSEs [eqpollE] ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 579` ``` addIs [diff_sing_lepoll,lepoll_diff_sing]) 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 580` ```qed "diff_sing_eqpoll"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 581` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 582` ```goal Cardinal.thy "!!A. [| A lepoll 1; a:A |] ==> A = {a}"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 583` ```by (forward_tac [diff_sing_lepoll] 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 584` ```by (assume_tac 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 585` ```by (dtac lepoll_0_is_0 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 586` ```by (fast_tac (eq_cs addEs [equalityE]) 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 587` ```qed "lepoll_1_is_sing"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 588` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 589` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 590` ```(*** Finite and infinite sets ***) ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 591` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 592` ```goalw Cardinal.thy [Finite_def] ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 593` ``` "!!A. [| A lepoll n; n:nat |] ==> Finite(A)"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 594` ```by (etac rev_mp 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 595` ```by (etac nat_induct 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 596` ```by (fast_tac (ZF_cs addSDs [lepoll_0_is_0] addSIs [eqpoll_refl,nat_0I]) 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 597` ```by (fast_tac (ZF_cs addSDs [lepoll_succ_disj] addSIs [nat_succI]) 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 598` ```qed "lepoll_nat_imp_Finite"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 599` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 600` ```goalw Cardinal.thy [Finite_def] ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 601` ``` "!!X. [| Y lepoll X; Finite(X) |] ==> Finite(Y)"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 602` ```by (fast_tac (ZF_cs addSEs [eqpollE] ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 603` ``` addEs [lepoll_trans RS ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 604` ``` rewrite_rule [Finite_def] lepoll_nat_imp_Finite]) 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 605` ```qed "lepoll_Finite"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 606` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 607` ```goalw Cardinal.thy [Finite_def] "!!x. Finite(x) ==> Finite(cons(y,x))"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 608` ```by (excluded_middle_tac "y:x" 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 609` ```by (asm_simp_tac (ZF_ss addsimps [cons_absorb]) 2); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 610` ```by (etac bexE 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 611` ```by (rtac bexI 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 612` ```by (etac nat_succI 2); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 613` ```by (asm_simp_tac ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 614` ``` (ZF_ss addsimps [succ_def, cons_eqpoll_cong, mem_not_refl]) 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 615` ```qed "Finite_imp_cons_Finite"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 616` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 617` ```goalw Cardinal.thy [succ_def] "!!x. Finite(x) ==> Finite(succ(x))"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 618` ```by (etac Finite_imp_cons_Finite 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 619` ```qed "Finite_imp_succ_Finite"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 620` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 621` ```goalw Cardinal.thy [Finite_def] ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 622` ``` "!!i. [| Ord(i); ~ Finite(i) |] ==> nat le i"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 623` ```by (eresolve_tac [Ord_nat RSN (2,Ord_linear2)] 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 624` ```by (assume_tac 2); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 625` ```by (fast_tac (ZF_cs addSIs [eqpoll_refl] addSEs [ltE]) 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 626` ```qed "nat_le_infinite_Ord"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 627` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 628` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 629` ```(*Krzysztof Grabczewski's proof that the converse of a finite, well-ordered ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 630` ``` set is well-ordered. Proofs simplified by lcp. *) ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 631` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 632` ```goal Nat.thy "!!n. n:nat ==> wf[n](converse(Memrel(n)))"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 633` ```by (etac nat_induct 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 634` ```by (fast_tac (ZF_cs addIs [wf_onI]) 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 635` ```by (rtac wf_onI 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 636` ```by (asm_full_simp_tac ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 637` ``` (ZF_ss addsimps [wf_on_def, wf_def, converse_iff, Memrel_iff]) 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 638` ```by (excluded_middle_tac "x:Z" 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 639` ```by (dres_inst_tac [("x", "x")] bspec 2 THEN assume_tac 2); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 640` ```by (fast_tac (ZF_cs addSEs [mem_irrefl] addEs [mem_asym]) 2); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 641` ```by (dres_inst_tac [("x", "Z")] spec 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 642` ```by (safe_tac ZF_cs); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 643` ```by (dres_inst_tac [("x", "xa")] bspec 1 THEN assume_tac 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 644` ```by (fast_tac ZF_cs 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 645` ```qed "nat_wf_on_converse_Memrel"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 646` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 647` ```goal Cardinal.thy "!!n. n:nat ==> well_ord(n,converse(Memrel(n)))"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 648` ```by (forward_tac [Ord_nat RS Ord_in_Ord RS well_ord_Memrel] 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 649` ```by (rewtac well_ord_def); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 650` ```by (fast_tac (ZF_cs addSIs [tot_ord_converse, nat_wf_on_converse_Memrel]) 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 651` ```qed "nat_well_ord_converse_Memrel"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 652` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 653` ```goal Cardinal.thy ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 654` ``` "!!A. [| well_ord(A,r); \ ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 655` ```\ well_ord(ordertype(A,r), converse(Memrel(ordertype(A, r)))) \ ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 656` ```\ |] ==> well_ord(A,converse(r))"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 657` ```by (resolve_tac [well_ord_Int_iff RS iffD1] 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 658` ```by (forward_tac [ordermap_bij RS bij_is_inj RS well_ord_rvimage] 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 659` ```by (assume_tac 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 660` ```by (asm_full_simp_tac ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 661` ``` (ZF_ss addsimps [rvimage_converse, converse_Int, converse_prod, ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 662` ``` ordertype_ord_iso RS ord_iso_rvimage_eq]) 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 663` ```qed "well_ord_converse"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 664` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 665` ```goal Cardinal.thy ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 666` ``` "!!A. [| well_ord(A,r); A eqpoll n; n:nat |] ==> ordertype(A,r)=n"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 667` ```by (rtac (Ord_ordertype RS Ord_nat_eqpoll_iff RS iffD1) 1 THEN ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 668` ``` REPEAT (assume_tac 1)); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 669` ```by (rtac eqpoll_trans 1 THEN assume_tac 2); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 670` ```by (rewtac eqpoll_def); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 671` ```by (fast_tac (ZF_cs addSIs [ordermap_bij RS bij_converse_bij]) 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 672` ```qed "ordertype_eq_n"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 673` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 674` ```goalw Cardinal.thy [Finite_def] ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 675` ``` "!!A. [| Finite(A); well_ord(A,r) |] ==> well_ord(A,converse(r))"; ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 676` ```by (rtac well_ord_converse 1 THEN assume_tac 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 677` ```by (fast_tac (ZF_cs addDs [ordertype_eq_n] ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 678` ``` addSIs [nat_well_ord_converse_Memrel]) 1); ``` ba386650df2c Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, lcp parents: 803 diff changeset ` 679` ```qed "Finite_well_ord_converse"; ```