--- a/src/ZF/Cardinal.ML Tue Jun 18 18:45:07 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,848 +0,0 @@
-(* Title: ZF/Cardinal.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1994 University of Cambridge
-
-Cardinals in Zermelo-Fraenkel Set Theory
-
-This theory does NOT assume the Axiom of Choice
-*)
-
-(*** The Schroeder-Bernstein Theorem -- see Davey & Priestly, page 106 ***)
-
-(** Lemma: Banach's Decomposition Theorem **)
-
-Goal "bnd_mono(X, %W. X - g``(Y - f``W))";
-by (rtac bnd_monoI 1);
-by (REPEAT (ares_tac [Diff_subset, subset_refl, Diff_mono, image_mono] 1));
-qed "decomp_bnd_mono";
-
-val [gfun] = goal (the_context ())
- "g: Y->X ==> \
-\ g``(Y - f`` lfp(X, %W. X - g``(Y - f``W))) = \
-\ X - lfp(X, %W. X - g``(Y - f``W)) ";
-by (res_inst_tac [("P", "%u. ?v = X-u")]
- (decomp_bnd_mono RS lfp_unfold RS ssubst) 1);
-by (simp_tac (simpset() addsimps [subset_refl, double_complement,
- gfun RS fun_is_rel RS image_subset]) 1);
-qed "Banach_last_equation";
-
-Goal "[| f: X->Y; g: Y->X |] ==> \
-\ EX XA XB YA YB. (XA Int XB = 0) & (XA Un XB = X) & \
-\ (YA Int YB = 0) & (YA Un YB = Y) & \
-\ f``XA=YA & g``YB=XB";
-by (REPEAT
- (FIRSTGOAL
- (resolve_tac [refl, exI, conjI, Diff_disjoint, Diff_partition])));
-by (rtac Banach_last_equation 3);
-by (REPEAT (ares_tac [fun_is_rel, image_subset, lfp_subset] 1));
-qed "decomposition";
-
-val prems = goal (the_context ())
- "[| f: inj(X,Y); g: inj(Y,X) |] ==> EX h. h: bij(X,Y)";
-by (cut_facts_tac prems 1);
-by (cut_facts_tac [(prems RL [inj_is_fun]) MRS decomposition] 1);
-by (blast_tac (claset() addSIs [restrict_bij,bij_disjoint_Un]
- addIs [bij_converse_bij]) 1);
-(* The instantiation of exI to "restrict(f,XA) Un converse(restrict(g,YB))"
- is forced by the context!! *)
-qed "schroeder_bernstein";
-
-
-(** Equipollence is an equivalence relation **)
-
-Goalw [eqpoll_def] "f: bij(A,B) ==> A eqpoll B";
-by (etac exI 1);
-qed "bij_imp_eqpoll";
-
-(*A eqpoll A*)
-bind_thm ("eqpoll_refl", id_bij RS bij_imp_eqpoll);
-Addsimps [eqpoll_refl];
-
-Goalw [eqpoll_def] "X eqpoll Y ==> Y eqpoll X";
-by (blast_tac (claset() addIs [bij_converse_bij]) 1);
-qed "eqpoll_sym";
-
-Goalw [eqpoll_def]
- "[| X eqpoll Y; Y eqpoll Z |] ==> X eqpoll Z";
-by (blast_tac (claset() addIs [comp_bij]) 1);
-qed "eqpoll_trans";
-
-(** Le-pollence is a partial ordering **)
-
-Goalw [lepoll_def] "X<=Y ==> X lepoll Y";
-by (rtac exI 1);
-by (etac id_subset_inj 1);
-qed "subset_imp_lepoll";
-
-bind_thm ("lepoll_refl", subset_refl RS subset_imp_lepoll);
-Addsimps [lepoll_refl];
-
-bind_thm ("le_imp_lepoll", le_imp_subset RS subset_imp_lepoll);
-
-Goalw [eqpoll_def, bij_def, lepoll_def]
- "X eqpoll Y ==> X lepoll Y";
-by (Blast_tac 1);
-qed "eqpoll_imp_lepoll";
-
-Goalw [lepoll_def]
- "[| X lepoll Y; Y lepoll Z |] ==> X lepoll Z";
-by (blast_tac (claset() addIs [comp_inj]) 1);
-qed "lepoll_trans";
-
-(*Asymmetry law*)
-Goalw [lepoll_def,eqpoll_def]
- "[| X lepoll Y; Y lepoll X |] ==> X eqpoll Y";
-by (REPEAT (etac exE 1));
-by (rtac schroeder_bernstein 1);
-by (REPEAT (assume_tac 1));
-qed "eqpollI";
-
-val [major,minor] = Goal
- "[| X eqpoll Y; [| X lepoll Y; Y lepoll X |] ==> P |] ==> P";
-by (rtac minor 1);
-by (REPEAT (resolve_tac [major, eqpoll_imp_lepoll, eqpoll_sym] 1));
-qed "eqpollE";
-
-Goal "X eqpoll Y <-> X lepoll Y & Y lepoll X";
-by (blast_tac (claset() addIs [eqpollI] addSEs [eqpollE]) 1);
-qed "eqpoll_iff";
-
-Goalw [lepoll_def, inj_def] "A lepoll 0 ==> A = 0";
-by (blast_tac (claset() addDs [apply_type]) 1);
-qed "lepoll_0_is_0";
-
-(*0 lepoll Y*)
-bind_thm ("empty_lepollI", empty_subsetI RS subset_imp_lepoll);
-
-Goal "A lepoll 0 <-> A=0";
-by (blast_tac (claset() addIs [lepoll_0_is_0, lepoll_refl]) 1);
-qed "lepoll_0_iff";
-
-Goalw [lepoll_def]
- "[| A lepoll B; C lepoll D; B Int D = 0 |] ==> A Un C lepoll B Un D";
-by (blast_tac (claset() addIs [inj_disjoint_Un]) 1);
-qed "Un_lepoll_Un";
-
-(*A eqpoll 0 ==> A=0*)
-bind_thm ("eqpoll_0_is_0", eqpoll_imp_lepoll RS lepoll_0_is_0);
-
-Goal "A eqpoll 0 <-> A=0";
-by (blast_tac (claset() addIs [eqpoll_0_is_0, eqpoll_refl]) 1);
-qed "eqpoll_0_iff";
-
-Goalw [eqpoll_def]
- "[| A eqpoll B; C eqpoll D; A Int C = 0; B Int D = 0 |] \
-\ ==> A Un C eqpoll B Un D";
-by (blast_tac (claset() addIs [bij_disjoint_Un]) 1);
-qed "eqpoll_disjoint_Un";
-
-
-(*** lesspoll: contributions by Krzysztof Grabczewski ***)
-
-Goalw [lesspoll_def] "A lesspoll B ==> A lepoll B";
-by (Blast_tac 1);
-qed "lesspoll_imp_lepoll";
-
-Goalw [lepoll_def] "[| A lepoll B; well_ord(B,r) |] ==> EX s. well_ord(A,s)";
-by (blast_tac (claset() addIs [well_ord_rvimage]) 1);
-qed "lepoll_well_ord";
-
-Goalw [lesspoll_def] "A lepoll B <-> A lesspoll B | A eqpoll B";
-by (blast_tac (claset() addSIs [eqpollI] addSEs [eqpollE]) 1);
-qed "lepoll_iff_leqpoll";
-
-Goalw [inj_def, surj_def]
- "[| f : inj(A, succ(m)); f ~: surj(A, succ(m)) |] ==> EX f. f:inj(A,m)";
-by (safe_tac (claset_of ZF.thy));
-by (swap_res_tac [exI] 1);
-by (res_inst_tac [("a", "lam z:A. if f`z=m then y else f`z")] CollectI 1);
-by (best_tac (claset() addSIs [if_type RS lam_type]
- addEs [apply_funtype RS succE]) 1);
-(*Proving it's injective*)
-by (Asm_simp_tac 1);
-by (blast_tac (claset() delrules [equalityI]) 1);
-qed "inj_not_surj_succ";
-
-(** Variations on transitivity **)
-
-Goalw [lesspoll_def]
- "[| X lesspoll Y; Y lesspoll Z |] ==> X lesspoll Z";
-by (blast_tac (claset() addSEs [eqpollE] addIs [eqpollI, lepoll_trans]) 1);
-qed "lesspoll_trans";
-
-Goalw [lesspoll_def]
- "[| X lepoll Y; Y lesspoll Z |] ==> X lesspoll Z";
-by (blast_tac (claset() addSEs [eqpollE] addIs [eqpollI, lepoll_trans]) 1);
-qed "lesspoll_trans1";
-
-Goalw [lesspoll_def]
- "[| X lesspoll Y; Y lepoll Z |] ==> X lesspoll Z";
-by (blast_tac (claset() addSEs [eqpollE] addIs [eqpollI, lepoll_trans]) 1);
-qed "lesspoll_trans2";
-
-
-(** LEAST -- the least number operator [from HOL/Univ.ML] **)
-
-val [premP,premOrd,premNot] = Goalw [Least_def]
- "[| P(i); Ord(i); !!x. x<i ==> ~P(x) |] ==> (LEAST x. P(x)) = i";
-by (rtac the_equality 1);
-by (blast_tac (claset() addSIs [premP,premOrd,premNot]) 1);
-by (REPEAT (etac conjE 1));
-by (etac (premOrd RS Ord_linear_lt) 1);
-by (ALLGOALS (blast_tac (claset() addSIs [premP] addSDs [premNot])));
-qed "Least_equality";
-
-(*Perform induction on i, then prove the Ord(i) subgoal using prems. *)
-fun trans_ind_tac a prems i =
- EVERY [res_inst_tac [("i",a)] trans_induct i,
- rename_last_tac a ["1"] (i+1),
- ares_tac prems i];
-
-Goal "[| P(i); Ord(i) |] ==> P(LEAST x. P(x))";
-by (etac rev_mp 1);
-by (trans_ind_tac "i" [] 1);
-by (rtac impI 1);
-by (rtac classical 1);
-by (EVERY1 [stac Least_equality, assume_tac, assume_tac]);
-by (assume_tac 2);
-by (blast_tac (claset() addSEs [ltE]) 1);
-qed "LeastI";
-
-(*Proof is almost identical to the one above!*)
-Goal "[| P(i); Ord(i) |] ==> (LEAST x. P(x)) le i";
-by (etac rev_mp 1);
-by (trans_ind_tac "i" [] 1);
-by (rtac impI 1);
-by (rtac classical 1);
-by (EVERY1 [stac Least_equality, assume_tac, assume_tac]);
-by (etac le_refl 2);
-by (blast_tac (claset() addEs [ltE] addIs [leI, ltI, lt_trans1]) 1);
-qed "Least_le";
-
-(*LEAST really is the smallest*)
-Goal "[| P(i); i < (LEAST x. P(x)) |] ==> Q";
-by (rtac (Least_le RSN (2,lt_trans2) RS lt_irrefl) 1);
-by (REPEAT (eresolve_tac [asm_rl, ltE] 1));
-qed "less_LeastE";
-
-(*Easier to apply than LeastI: conclusion has only one occurrence of P*)
-val prems = goal (the_context ())
- "[| P(i); Ord(i); !!j. P(j) ==> Q(j) |] ==> Q(LEAST j. P(j))";
-by (resolve_tac prems 1);
-by (rtac LeastI 1);
-by (resolve_tac prems 1);
-by (resolve_tac prems 1) ;
-qed "LeastI2";
-
-(*If there is no such P then LEAST is vacuously 0*)
-Goalw [Least_def]
- "[| ~ (EX i. Ord(i) & P(i)) |] ==> (LEAST x. P(x)) = 0";
-by (rtac the_0 1);
-by (Blast_tac 1);
-qed "Least_0";
-
-Goal "Ord(LEAST x. P(x))";
-by (excluded_middle_tac "EX i. Ord(i) & P(i)" 1);
-by Safe_tac;
-by (rtac (Least_le RS ltE) 2);
-by (REPEAT_SOME assume_tac);
-by (etac (Least_0 RS ssubst) 1);
-by (rtac Ord_0 1);
-qed "Ord_Least";
-
-
-(** Basic properties of cardinals **)
-
-(*Not needed for simplification, but helpful below*)
-val prems = Goal "(!!y. P(y) <-> Q(y)) ==> (LEAST x. P(x)) = (LEAST x. Q(x))";
-by (simp_tac (simpset() addsimps prems) 1);
-qed "Least_cong";
-
-(*Need AC to get X lepoll Y ==> |X| le |Y|; see well_ord_lepoll_imp_Card_le
- Converse also requires AC, but see well_ord_cardinal_eqE*)
-Goalw [eqpoll_def,cardinal_def] "X eqpoll Y ==> |X| = |Y|";
-by (rtac Least_cong 1);
-by (blast_tac (claset() addIs [comp_bij, bij_converse_bij]) 1);
-qed "cardinal_cong";
-
-(*Under AC, the premise becomes trivial; one consequence is ||A|| = |A|*)
-Goalw [cardinal_def]
- "well_ord(A,r) ==> |A| eqpoll A";
-by (rtac LeastI 1);
-by (etac Ord_ordertype 2);
-by (etac (ordermap_bij RS bij_converse_bij RS bij_imp_eqpoll) 1);
-qed "well_ord_cardinal_eqpoll";
-
-(* Ord(A) ==> |A| eqpoll A *)
-bind_thm ("Ord_cardinal_eqpoll", well_ord_Memrel RS well_ord_cardinal_eqpoll);
-
-Goal "[| well_ord(X,r); well_ord(Y,s); |X| = |Y| |] ==> X eqpoll Y";
-by (rtac (eqpoll_sym RS eqpoll_trans) 1);
-by (etac well_ord_cardinal_eqpoll 1);
-by (asm_simp_tac (simpset() addsimps [well_ord_cardinal_eqpoll]) 1);
-qed "well_ord_cardinal_eqE";
-
-Goal "[| well_ord(X,r); well_ord(Y,s) |] ==> |X| = |Y| <-> X eqpoll Y";
-by (blast_tac (claset() addIs [cardinal_cong, well_ord_cardinal_eqE]) 1);
-qed "well_ord_cardinal_eqpoll_iff";
-
-
-(** Observations from Kunen, page 28 **)
-
-Goalw [cardinal_def] "Ord(i) ==> |i| le i";
-by (etac (eqpoll_refl RS Least_le) 1);
-qed "Ord_cardinal_le";
-
-Goalw [Card_def] "Card(K) ==> |K| = K";
-by (etac sym 1);
-qed "Card_cardinal_eq";
-
-(* Could replace the ~(j eqpoll i) by ~(i lepoll j) *)
-val prems = Goalw [Card_def,cardinal_def]
- "[| Ord(i); !!j. j<i ==> ~(j eqpoll i) |] ==> Card(i)";
-by (stac Least_equality 1);
-by (REPEAT (ares_tac ([refl,eqpoll_refl]@prems) 1));
-qed "CardI";
-
-Goalw [Card_def, cardinal_def] "Card(i) ==> Ord(i)";
-by (etac ssubst 1);
-by (rtac Ord_Least 1);
-qed "Card_is_Ord";
-
-Goal "Card(K) ==> K le |K|";
-by (asm_simp_tac (simpset() addsimps [Card_is_Ord, Card_cardinal_eq]) 1);
-qed "Card_cardinal_le";
-
-Goalw [cardinal_def] "Ord(|A|)";
-by (rtac Ord_Least 1);
-qed "Ord_cardinal";
-
-Addsimps [Ord_cardinal];
-AddSIs [Ord_cardinal];
-
-(*The cardinals are the initial ordinals*)
-Goal "Card(K) <-> Ord(K) & (ALL j. j<K --> ~ j eqpoll K)";
-by (safe_tac (claset() addSIs [CardI, Card_is_Ord]));
-by (Blast_tac 2);
-by (rewrite_goals_tac [Card_def, cardinal_def]);
-by (rtac less_LeastE 1);
-by (etac subst 2);
-by (ALLGOALS assume_tac);
-qed "Card_iff_initial";
-
-Goalw [lesspoll_def] "[| Card(a); i<a |] ==> i lesspoll a";
-by (dresolve_tac [Card_iff_initial RS iffD1] 1);
-by (blast_tac (claset() addSIs [leI RS le_imp_lepoll]) 1);
-qed "lt_Card_imp_lesspoll";
-
-Goal "Card(0)";
-by (rtac (Ord_0 RS CardI) 1);
-by (blast_tac (claset() addSEs [ltE]) 1);
-qed "Card_0";
-
-val [premK,premL] = goal (the_context ())
- "[| Card(K); Card(L) |] ==> Card(K Un L)";
-by (rtac ([premK RS Card_is_Ord, premL RS Card_is_Ord] MRS Ord_linear_le) 1);
-by (asm_simp_tac
- (simpset() addsimps [premL, le_imp_subset, subset_Un_iff RS iffD1]) 1);
-by (asm_simp_tac
- (simpset() addsimps [premK, le_imp_subset, subset_Un_iff2 RS iffD1]) 1);
-qed "Card_Un";
-
-(*Infinite unions of cardinals? See Devlin, Lemma 6.7, page 98*)
-
-Goalw [cardinal_def] "Card(|A|)";
-by (excluded_middle_tac "EX i. Ord(i) & i eqpoll A" 1);
-by (etac (Least_0 RS ssubst) 1 THEN rtac Card_0 1);
-by (rtac (Ord_Least RS CardI) 1);
-by Safe_tac;
-by (rtac less_LeastE 1);
-by (assume_tac 2);
-by (etac eqpoll_trans 1);
-by (REPEAT (ares_tac [LeastI] 1));
-qed "Card_cardinal";
-
-(*Kunen's Lemma 10.5*)
-Goal "[| |i| le j; j le i |] ==> |j| = |i|";
-by (rtac (eqpollI RS cardinal_cong) 1);
-by (etac le_imp_lepoll 1);
-by (rtac lepoll_trans 1);
-by (etac le_imp_lepoll 2);
-by (rtac (eqpoll_sym RS eqpoll_imp_lepoll) 1);
-by (rtac Ord_cardinal_eqpoll 1);
-by (REPEAT (eresolve_tac [ltE, Ord_succD] 1));
-qed "cardinal_eq_lemma";
-
-Goal "i le j ==> |i| le |j|";
-by (res_inst_tac [("i","|i|"),("j","|j|")] Ord_linear_le 1);
-by (REPEAT_FIRST (ares_tac [Ord_cardinal, le_eqI]));
-by (rtac cardinal_eq_lemma 1);
-by (assume_tac 2);
-by (etac le_trans 1);
-by (etac ltE 1);
-by (etac Ord_cardinal_le 1);
-qed "cardinal_mono";
-
-(*Since we have |succ(nat)| le |nat|, the converse of cardinal_mono fails!*)
-Goal "[| |i| < |j|; Ord(i); Ord(j) |] ==> i < j";
-by (rtac Ord_linear2 1);
-by (REPEAT_SOME assume_tac);
-by (etac (lt_trans2 RS lt_irrefl) 1);
-by (etac cardinal_mono 1);
-qed "cardinal_lt_imp_lt";
-
-Goal "[| |i| < K; Ord(i); Card(K) |] ==> i < K";
-by (asm_simp_tac (simpset() addsimps
- [cardinal_lt_imp_lt, Card_is_Ord, Card_cardinal_eq]) 1);
-qed "Card_lt_imp_lt";
-
-Goal "[| Ord(i); Card(K) |] ==> (|i| < K) <-> (i < K)";
-by (blast_tac (claset() addIs [Card_lt_imp_lt, Ord_cardinal_le RS lt_trans1]) 1);
-qed "Card_lt_iff";
-
-Goal "[| Ord(i); Card(K) |] ==> (K le |i|) <-> (K le i)";
-by (asm_simp_tac (simpset() addsimps
- [Card_lt_iff, Card_is_Ord, Ord_cardinal,
- not_lt_iff_le RS iff_sym]) 1);
-qed "Card_le_iff";
-
-(*Can use AC or finiteness to discharge first premise*)
-Goal "[| well_ord(B,r); A lepoll B |] ==> |A| le |B|";
-by (res_inst_tac [("i","|A|"),("j","|B|")] Ord_linear_le 1);
-by (REPEAT_FIRST (ares_tac [Ord_cardinal, le_eqI]));
-by (rtac (eqpollI RS cardinal_cong) 1 THEN assume_tac 1);
-by (rtac lepoll_trans 1);
-by (rtac (well_ord_cardinal_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll) 1);
-by (assume_tac 1);
-by (etac (le_imp_lepoll RS lepoll_trans) 1);
-by (rtac eqpoll_imp_lepoll 1);
-by (rewtac lepoll_def);
-by (etac exE 1);
-by (rtac well_ord_cardinal_eqpoll 1);
-by (etac well_ord_rvimage 1);
-by (assume_tac 1);
-qed "well_ord_lepoll_imp_Card_le";
-
-
-Goal "[| A lepoll i; Ord(i) |] ==> |A| le i";
-by (rtac le_trans 1);
-by (etac (well_ord_Memrel RS well_ord_lepoll_imp_Card_le) 1);
-by (assume_tac 1);
-by (etac Ord_cardinal_le 1);
-qed "lepoll_cardinal_le";
-
-Goal "[| A lepoll i; Ord(i) |] ==> |A| eqpoll A";
-by (blast_tac (claset() addIs [lepoll_cardinal_le, well_ord_Memrel,
- well_ord_cardinal_eqpoll]
- addSDs [lepoll_well_ord]) 1);
-qed "lepoll_Ord_imp_eqpoll";
-
-Goalw [lesspoll_def]
- "[| A lesspoll i; Ord(i) |] ==> |A| eqpoll A";
-by (blast_tac (claset() addIs [lepoll_Ord_imp_eqpoll]) 1);
-qed "lesspoll_imp_eqpoll";
-
-
-(*** The finite cardinals ***)
-
-Goalw [lepoll_def, inj_def]
- "[| cons(u,A) lepoll cons(v,B); u~:A; v~:B |] ==> A lepoll B";
-by Safe_tac;
-by (res_inst_tac [("x", "lam x:A. if f`x=v then f`u else f`x")] exI 1);
-by (rtac CollectI 1);
-(*Proving it's in the function space A->B*)
-by (rtac (if_type RS lam_type) 1);
-by (blast_tac (claset() addDs [apply_funtype]) 1);
-by (blast_tac (claset() addSEs [mem_irrefl] addDs [apply_funtype]) 1);
-(*Proving it's injective*)
-by (Asm_simp_tac 1);
-by (Blast_tac 1);
-qed "cons_lepoll_consD";
-
-Goal "[| cons(u,A) eqpoll cons(v,B); u~:A; v~:B |] ==> A eqpoll B";
-by (asm_full_simp_tac (simpset() addsimps [eqpoll_iff]) 1);
-by (blast_tac (claset() addIs [cons_lepoll_consD]) 1);
-qed "cons_eqpoll_consD";
-
-(*Lemma suggested by Mike Fourman*)
-Goalw [succ_def] "succ(m) lepoll succ(n) ==> m lepoll n";
-by (etac cons_lepoll_consD 1);
-by (REPEAT (rtac mem_not_refl 1));
-qed "succ_lepoll_succD";
-
-Goal "m:nat ==> ALL n: nat. m lepoll n --> m le n";
-by (etac nat_induct 1); (*induct_tac isn't available yet*)
-by (blast_tac (claset() addSIs [nat_0_le]) 1);
-by (rtac ballI 1);
-by (eres_inst_tac [("n","n")] natE 1);
-by (asm_simp_tac (simpset() addsimps [lepoll_def, inj_def]) 1);
-by (blast_tac (claset() addSIs [succ_leI] addSDs [succ_lepoll_succD]) 1);
-qed_spec_mp "nat_lepoll_imp_le";
-
-Goal "[| m:nat; n: nat |] ==> m eqpoll n <-> m = n";
-by (rtac iffI 1);
-by (asm_simp_tac (simpset() addsimps [eqpoll_refl]) 2);
-by (blast_tac (claset() addIs [nat_lepoll_imp_le, le_anti_sym]
- addSEs [eqpollE]) 1);
-qed "nat_eqpoll_iff";
-
-(*The object of all this work: every natural number is a (finite) cardinal*)
-Goalw [Card_def,cardinal_def]
- "n: nat ==> Card(n)";
-by (stac Least_equality 1);
-by (REPEAT_FIRST (ares_tac [eqpoll_refl, nat_into_Ord, refl]));
-by (asm_simp_tac (simpset() addsimps [lt_nat_in_nat RS nat_eqpoll_iff]) 1);
-by (blast_tac (claset() addSEs [lt_irrefl]) 1);
-qed "nat_into_Card";
-
-bind_thm ("cardinal_0", nat_0I RS nat_into_Card RS Card_cardinal_eq);
-bind_thm ("cardinal_1", nat_1I RS nat_into_Card RS Card_cardinal_eq);
-AddIffs [cardinal_0, cardinal_1];
-
-(*Part of Kunen's Lemma 10.6*)
-Goal "[| succ(n) lepoll n; n:nat |] ==> P";
-by (rtac (nat_lepoll_imp_le RS lt_irrefl) 1);
-by (REPEAT (ares_tac [nat_succI] 1));
-qed "succ_lepoll_natE";
-
-Goalw [lesspoll_def] "n \\<in> nat ==> n lesspoll nat";
-by (fast_tac (claset() addSEs [Ord_nat RSN (2, ltI) RS leI RS le_imp_lepoll,
- eqpoll_sym RS eqpoll_imp_lepoll]
- addIs [Ord_nat RSN (2, nat_succI RS ltI) RS leI
- RS le_imp_lepoll RS lepoll_trans RS succ_lepoll_natE]) 1);
-qed "n_lesspoll_nat";
-
-Goalw [lepoll_def, eqpoll_def]
- "[| n \\<in> nat; nat lepoll X |] ==> \\<exists>Y. Y \\<subseteq> X & n eqpoll Y";
-by (fast_tac (subset_cs addSDs [Ord_nat RSN (2, OrdmemD) RSN (2, restrict_inj)]
- addSEs [restrict_bij, inj_is_fun RS fun_is_rel RS image_subset]) 1);
-qed "nat_lepoll_imp_ex_eqpoll_n";
-
-
-(** lepoll, lesspoll and natural numbers **)
-
-Goalw [lesspoll_def]
- "[| A lepoll m; m:nat |] ==> A lesspoll succ(m)";
-by (rtac conjI 1);
-by (blast_tac (claset() addIs [subset_imp_lepoll RSN (2,lepoll_trans)]) 1);
-by (rtac notI 1);
-by (dresolve_tac [eqpoll_sym RS eqpoll_imp_lepoll] 1);
-by (dtac lepoll_trans 1 THEN assume_tac 1);
-by (etac succ_lepoll_natE 1 THEN assume_tac 1);
-qed "lepoll_imp_lesspoll_succ";
-
-Goalw [lesspoll_def, lepoll_def, eqpoll_def, bij_def]
- "[| A lesspoll succ(m); m:nat |] ==> A lepoll m";
-by (Clarify_tac 1);
-by (blast_tac (claset() addSIs [inj_not_surj_succ]) 1);
-qed "lesspoll_succ_imp_lepoll";
-
-Goal "m:nat ==> A lesspoll succ(m) <-> A lepoll m";
-by (blast_tac (claset() addSIs [lepoll_imp_lesspoll_succ,
- lesspoll_succ_imp_lepoll]) 1);
-qed "lesspoll_succ_iff";
-
-Goal "[| A lepoll succ(m); m:nat |] ==> A lepoll m | A eqpoll succ(m)";
-by (rtac disjCI 1);
-by (rtac lesspoll_succ_imp_lepoll 1);
-by (assume_tac 2);
-by (asm_simp_tac (simpset() addsimps [lesspoll_def]) 1);
-qed "lepoll_succ_disj";
-
-Goalw [lesspoll_def] "[| A lesspoll i; Ord(i) |] ==> |A| < i";
-by (Clarify_tac 1);
-by (ftac lepoll_cardinal_le 1);
-by (assume_tac 1);
-by (blast_tac (claset() addIs [well_ord_Memrel,
- well_ord_cardinal_eqpoll RS eqpoll_sym]
- addDs [lepoll_well_ord]
- addSEs [leE]) 1);
-qed "lesspoll_cardinal_lt";
-
-
-(*** The first infinite cardinal: Omega, or nat ***)
-
-(*This implies Kunen's Lemma 10.6*)
-Goal "[| n<i; n:nat |] ==> ~ i lepoll n";
-by (rtac notI 1);
-by (rtac succ_lepoll_natE 1 THEN assume_tac 2);
-by (rtac lepoll_trans 1 THEN assume_tac 2);
-by (etac ltE 1);
-by (REPEAT (ares_tac [Ord_succ_subsetI RS subset_imp_lepoll] 1));
-qed "lt_not_lepoll";
-
-Goal "[| Ord(i); n:nat |] ==> i eqpoll n <-> i=n";
-by (rtac iffI 1);
-by (asm_simp_tac (simpset() addsimps [eqpoll_refl]) 2);
-by (rtac Ord_linear_lt 1);
-by (REPEAT_SOME (eresolve_tac [asm_rl, nat_into_Ord]));
-by (etac (lt_nat_in_nat RS nat_eqpoll_iff RS iffD1) 1 THEN
- REPEAT (assume_tac 1));
-by (rtac (lt_not_lepoll RS notE) 1 THEN (REPEAT (assume_tac 1)));
-by (etac eqpoll_imp_lepoll 1);
-qed "Ord_nat_eqpoll_iff";
-
-Goalw [Card_def,cardinal_def] "Card(nat)";
-by (stac Least_equality 1);
-by (REPEAT_FIRST (ares_tac [eqpoll_refl, Ord_nat, refl]));
-by (etac ltE 1);
-by (asm_simp_tac (simpset() addsimps [eqpoll_iff, lt_not_lepoll, ltI]) 1);
-qed "Card_nat";
-
-(*Allows showing that |i| is a limit cardinal*)
-Goal "nat le i ==> nat le |i|";
-by (rtac (Card_nat RS Card_cardinal_eq RS subst) 1);
-by (etac cardinal_mono 1);
-qed "nat_le_cardinal";
-
-
-(*** Towards Cardinal Arithmetic ***)
-(** Congruence laws for successor, cardinal addition and multiplication **)
-
-(*Congruence law for cons under equipollence*)
-Goalw [lepoll_def]
- "[| A lepoll B; b ~: B |] ==> cons(a,A) lepoll cons(b,B)";
-by Safe_tac;
-by (res_inst_tac [("x", "lam y: cons(a,A). if y=a then b else f`y")] exI 1);
-by (res_inst_tac [("d","%z. if z:B then converse(f)`z else a")]
- lam_injective 1);
-by (asm_simp_tac (simpset() addsimps [inj_is_fun RS apply_type, cons_iff]
- setloop etac consE') 1);
-by (asm_simp_tac (simpset() addsimps [inj_is_fun RS apply_type]
- setloop etac consE') 1);
-qed "cons_lepoll_cong";
-
-Goal "[| A eqpoll B; a ~: A; b ~: B |] ==> cons(a,A) eqpoll cons(b,B)";
-by (asm_full_simp_tac (simpset() addsimps [eqpoll_iff, cons_lepoll_cong]) 1);
-qed "cons_eqpoll_cong";
-
-Goal "[| a ~: A; b ~: B |] ==> \
-\ cons(a,A) lepoll cons(b,B) <-> A lepoll B";
-by (blast_tac (claset() addIs [cons_lepoll_cong, cons_lepoll_consD]) 1);
-qed "cons_lepoll_cons_iff";
-
-Goal "[| a ~: A; b ~: B |] ==> \
-\ cons(a,A) eqpoll cons(b,B) <-> A eqpoll B";
-by (blast_tac (claset() addIs [cons_eqpoll_cong, cons_eqpoll_consD]) 1);
-qed "cons_eqpoll_cons_iff";
-
-Goalw [succ_def] "{a} eqpoll 1";
-by (blast_tac (claset() addSIs [eqpoll_refl RS cons_eqpoll_cong]) 1);
-qed "singleton_eqpoll_1";
-
-Goal "|{a}| = 1";
-by (resolve_tac [singleton_eqpoll_1 RS cardinal_cong RS trans] 1);
-by (simp_tac (simpset() addsimps [nat_into_Card RS Card_cardinal_eq]) 1);
-qed "cardinal_singleton";
-
-Goal "A ~= 0 ==> 1 lepoll A";
-by (etac not_emptyE 1);
-by (res_inst_tac [("a", "cons(x, A-{x})")] subst 1);
-by (res_inst_tac [("a", "cons(0,0)"),
- ("P", "%y. y lepoll cons(x, A-{x})")] subst 2);
-by (blast_tac (claset() addIs [cons_lepoll_cong, subset_imp_lepoll]) 3);
-by Auto_tac;
-qed "not_0_is_lepoll_1";
-
-(*Congruence law for succ under equipollence*)
-Goalw [succ_def]
- "A eqpoll B ==> succ(A) eqpoll succ(B)";
-by (REPEAT (ares_tac [cons_eqpoll_cong, mem_not_refl] 1));
-qed "succ_eqpoll_cong";
-
-(*Congruence law for + under equipollence*)
-Goalw [eqpoll_def]
- "[| A eqpoll C; B eqpoll D |] ==> A+B eqpoll C+D";
-by (blast_tac (claset() addSIs [sum_bij]) 1);
-qed "sum_eqpoll_cong";
-
-(*Congruence law for * under equipollence*)
-Goalw [eqpoll_def]
- "[| A eqpoll C; B eqpoll D |] ==> A*B eqpoll C*D";
-by (blast_tac (claset() addSIs [prod_bij]) 1);
-qed "prod_eqpoll_cong";
-
-Goalw [eqpoll_def]
- "[| f: inj(A,B); A Int B = 0 |] ==> A Un (B - range(f)) eqpoll B";
-by (rtac exI 1);
-by (res_inst_tac [("c", "%x. if x:A then f`x else x"),
- ("d", "%y. if y: range(f) then converse(f)`y else y")]
- lam_bijective 1);
-by (blast_tac (claset() addSIs [if_type, inj_is_fun RS apply_type]) 1);
-by (asm_simp_tac
- (simpset() addsimps [inj_converse_fun RS apply_funtype]) 1);
-by (asm_simp_tac (simpset() addsimps [inj_is_fun RS apply_rangeI]
- setloop etac UnE') 1);
-by (asm_simp_tac (simpset() addsimps [inj_converse_fun RS apply_funtype]) 1);
-by (Blast_tac 1);
-qed "inj_disjoint_eqpoll";
-
-
-(*** Lemmas by Krzysztof Grabczewski. New proofs using cons_lepoll_cons.
- Could easily generalise from succ to cons. ***)
-
-(*If A has at most n+1 elements and a:A then A-{a} has at most n.*)
-Goalw [succ_def]
- "[| a:A; A lepoll succ(n) |] ==> A - {a} lepoll n";
-by (rtac cons_lepoll_consD 1);
-by (rtac mem_not_refl 3);
-by (eresolve_tac [cons_Diff RS ssubst] 1);
-by Safe_tac;
-qed "Diff_sing_lepoll";
-
-(*If A has at least n+1 elements then A-{a} has at least n.*)
-Goalw [succ_def]
- "[| succ(n) lepoll A |] ==> n lepoll A - {a}";
-by (rtac cons_lepoll_consD 1);
-by (rtac mem_not_refl 2);
-by (Blast_tac 2);
-by (blast_tac (claset() addIs [subset_imp_lepoll RSN (2, lepoll_trans)]) 1);
-qed "lepoll_Diff_sing";
-
-Goal "[| a:A; A eqpoll succ(n) |] ==> A - {a} eqpoll n";
-by (blast_tac (claset() addSIs [eqpollI] addSEs [eqpollE]
- addIs [Diff_sing_lepoll,lepoll_Diff_sing]) 1);
-qed "Diff_sing_eqpoll";
-
-Goal "[| A lepoll 1; a:A |] ==> A = {a}";
-by (ftac Diff_sing_lepoll 1);
-by (assume_tac 1);
-by (dtac lepoll_0_is_0 1);
-by (blast_tac (claset() addEs [equalityE]) 1);
-qed "lepoll_1_is_sing";
-
-Goalw [lepoll_def] "A Un B lepoll A+B";
-by (res_inst_tac [("x",
- "lam x: A Un B. if x:A then Inl(x) else Inr(x)")] exI 1);
-by (res_inst_tac [("d","%z. snd(z)")] lam_injective 1);
-by (asm_full_simp_tac (simpset() addsimps [Inl_def, Inr_def]) 2);
-by Auto_tac;
-qed "Un_lepoll_sum";
-
-Goal "[| well_ord(X,R); well_ord(Y,S) |] ==> EX T. well_ord(X Un Y, T)";
-by (eresolve_tac [well_ord_radd RS (Un_lepoll_sum RS lepoll_well_ord)] 1);
-by (assume_tac 1);
-qed "well_ord_Un";
-
-(*Krzysztof Grabczewski*)
-Goalw [eqpoll_def] "A Int B = 0 ==> A Un B eqpoll A + B";
-by (res_inst_tac [("x","lam a:A Un B. if a:A then Inl(a) else Inr(a)")] exI 1);
-by (res_inst_tac [("d","%z. case(%x. x, %x. x, z)")] lam_bijective 1);
-by Auto_tac;
-qed "disj_Un_eqpoll_sum";
-
-
-(*** Finite and infinite sets ***)
-
-Goalw [Finite_def] "Finite(0)";
-by (blast_tac (claset() addSIs [eqpoll_refl, nat_0I]) 1);
-qed "Finite_0";
-
-Goalw [Finite_def]
- "[| A lepoll n; n:nat |] ==> Finite(A)";
-by (etac rev_mp 1);
-by (etac nat_induct 1);
-by (blast_tac (claset() addSDs [lepoll_0_is_0] addSIs [eqpoll_refl,nat_0I]) 1);
-by (blast_tac (claset() addSDs [lepoll_succ_disj]) 1);
-qed "lepoll_nat_imp_Finite";
-
-Goalw [Finite_def]
- "A lesspoll nat ==> Finite(A)";
-by (blast_tac (claset() addDs [ltD, lesspoll_cardinal_lt,
- lesspoll_imp_eqpoll RS eqpoll_sym]) 1);;
-qed "lesspoll_nat_is_Finite";
-
-Goalw [Finite_def]
- "[| Y lepoll X; Finite(X) |] ==> Finite(Y)";
-by (blast_tac
- (claset() addSEs [eqpollE]
- addIs [lepoll_trans RS
- rewrite_rule [Finite_def] lepoll_nat_imp_Finite]) 1);
-qed "lepoll_Finite";
-
-bind_thm ("subset_Finite", subset_imp_lepoll RS lepoll_Finite);
-
-bind_thm ("Finite_Diff", Diff_subset RS subset_Finite);
-
-Goalw [Finite_def] "Finite(x) ==> Finite(cons(y,x))";
-by (excluded_middle_tac "y:x" 1);
-by (asm_simp_tac (simpset() addsimps [cons_absorb]) 2);
-by (etac bexE 1);
-by (rtac bexI 1);
-by (etac nat_succI 2);
-by (asm_simp_tac
- (simpset() addsimps [succ_def, cons_eqpoll_cong, mem_not_refl]) 1);
-qed "Finite_cons";
-
-Goalw [succ_def] "Finite(x) ==> Finite(succ(x))";
-by (etac Finite_cons 1);
-qed "Finite_succ";
-
-Goalw [Finite_def]
- "[| Ord(i); ~ Finite(i) |] ==> nat le i";
-by (eresolve_tac [Ord_nat RSN (2,Ord_linear2)] 1);
-by (assume_tac 2);
-by (blast_tac (claset() addSIs [eqpoll_refl] addSEs [ltE]) 1);
-qed "nat_le_infinite_Ord";
-
-Goalw [Finite_def, eqpoll_def]
- "Finite(A) ==> EX r. well_ord(A,r)";
-by (blast_tac (claset() addIs [well_ord_rvimage, bij_is_inj, well_ord_Memrel,
- nat_into_Ord]) 1);
-qed "Finite_imp_well_ord";
-
-
-(*Krzysztof Grabczewski's proof that the converse of a finite, well-ordered
- set is well-ordered. Proofs simplified by lcp. *)
-
-Goal "n:nat ==> wf[n](converse(Memrel(n)))";
-by (etac nat_induct 1);
-by (blast_tac (claset() addIs [wf_onI]) 1);
-by (rtac wf_onI 1);
-by (asm_full_simp_tac (simpset() addsimps [wf_on_def, wf_def]) 1);
-by (excluded_middle_tac "x:Z" 1);
-by (dres_inst_tac [("x", "x")] bspec 2 THEN assume_tac 2);
-by (blast_tac (claset() addEs [mem_irrefl, mem_asym]) 2);
-by (dres_inst_tac [("x", "Z")] spec 1);
-by (Blast.depth_tac (claset()) 4 1);
-qed "nat_wf_on_converse_Memrel";
-
-Goal "n:nat ==> well_ord(n,converse(Memrel(n)))";
-by (forward_tac [transfer (the_context ()) Ord_nat RS Ord_in_Ord RS well_ord_Memrel] 1);
-by (rewtac well_ord_def);
-by (blast_tac (claset() addSIs [tot_ord_converse,
- nat_wf_on_converse_Memrel]) 1);
-qed "nat_well_ord_converse_Memrel";
-
-Goal "[| well_ord(A,r); \
-\ well_ord(ordertype(A,r), converse(Memrel(ordertype(A, r)))) \
-\ |] ==> well_ord(A,converse(r))";
-by (resolve_tac [well_ord_Int_iff RS iffD1] 1);
-by (forward_tac [ordermap_bij RS bij_is_inj RS well_ord_rvimage] 1);
-by (assume_tac 1);
-by (asm_full_simp_tac
- (simpset() addsimps [rvimage_converse, converse_Int, converse_prod,
- ordertype_ord_iso RS ord_iso_rvimage_eq]) 1);
-qed "well_ord_converse";
-
-Goal "[| well_ord(A,r); A eqpoll n; n:nat |] ==> ordertype(A,r)=n";
-by (rtac (Ord_ordertype RS Ord_nat_eqpoll_iff RS iffD1) 1 THEN
- REPEAT (assume_tac 1));
-by (rtac eqpoll_trans 1 THEN assume_tac 2);
-by (rewtac eqpoll_def);
-by (blast_tac (claset() addSIs [ordermap_bij RS bij_converse_bij]) 1);
-qed "ordertype_eq_n";
-
-Goalw [Finite_def]
- "[| Finite(A); well_ord(A,r) |] ==> well_ord(A,converse(r))";
-by (rtac well_ord_converse 1 THEN assume_tac 1);
-by (blast_tac (claset() addDs [ordertype_eq_n]
- addSIs [nat_well_ord_converse_Memrel]) 1);
-qed "Finite_well_ord_converse";
-
-Goalw [Finite_def] "n:nat ==> Finite(n)";
-by (fast_tac (claset() addSIs [eqpoll_refl]) 1);
-qed "nat_into_Finite";
-
-
--- a/src/ZF/Cardinal.thy Tue Jun 18 18:45:07 2002 +0200
+++ b/src/ZF/Cardinal.thy Wed Jun 19 09:03:34 2002 +0200
@@ -4,37 +4,1004 @@
Copyright 1994 University of Cambridge
Cardinals in Zermelo-Fraenkel Set Theory
+
+This theory does NOT assume the Axiom of Choice
*)
-Cardinal = OrderType + Fixedpt + Nat + Sum +
-consts
- Least :: (i=>o) => i (binder "LEAST " 10)
- eqpoll, lepoll,
- lesspoll :: [i,i] => o (infixl 50)
- cardinal :: i=>i ("|_|")
- Finite, Card :: i=>o
+theory Cardinal = OrderType + Fixedpt + Nat + Sum:
+
+(*** The following really belong in upair ***)
-defs
+lemma eq_imp_not_mem: "a=A ==> a ~: A"
+by (blast intro: elim: mem_irrefl)
+
+constdefs
(*least ordinal operator*)
- Least_def "Least(P) == THE i. Ord(i) & P(i) & (ALL j. j<i --> ~P(j))"
+ Least :: "(i=>o) => i" (binder "LEAST " 10)
+ "Least(P) == THE i. Ord(i) & P(i) & (ALL j. j<i --> ~P(j))"
- eqpoll_def "A eqpoll B == EX f. f: bij(A,B)"
+ eqpoll :: "[i,i] => o" (infixl "eqpoll" 50)
+ "A eqpoll B == EX f. f: bij(A,B)"
- lepoll_def "A lepoll B == EX f. f: inj(A,B)"
+ lepoll :: "[i,i] => o" (infixl "lepoll" 50)
+ "A lepoll B == EX f. f: inj(A,B)"
- lesspoll_def "A lesspoll B == A lepoll B & ~(A eqpoll B)"
+ lesspoll :: "[i,i] => o" (infixl "lesspoll" 50)
+ "A lesspoll B == A lepoll B & ~(A eqpoll B)"
- Finite_def "Finite(A) == EX n:nat. A eqpoll n"
+ cardinal :: "i=>i" ("|_|")
+ "|A| == LEAST i. i eqpoll A"
- cardinal_def "|A| == LEAST i. i eqpoll A"
+ Finite :: "i=>o"
+ "Finite(A) == EX n:nat. A eqpoll n"
- Card_def "Card(i) == (i = |i|)"
+ Card :: "i=>o"
+ "Card(i) == (i = |i|)"
syntax (xsymbols)
- "op eqpoll" :: [i,i] => o (infixl "\\<approx>" 50)
- "op lepoll" :: [i,i] => o (infixl "\\<lesssim>" 50)
- "op lesspoll" :: [i,i] => o (infixl "\\<prec>" 50)
- "LEAST " :: [pttrn, o] => i ("(3\\<mu>_./ _)" [0, 10] 10)
+ "eqpoll" :: "[i,i] => o" (infixl "\<approx>" 50)
+ "lepoll" :: "[i,i] => o" (infixl "\<lesssim>" 50)
+ "lesspoll" :: "[i,i] => o" (infixl "\<prec>" 50)
+ "LEAST " :: "[pttrn, o] => i" ("(3\<mu>_./ _)" [0, 10] 10)
+
+(*** The Schroeder-Bernstein Theorem -- see Davey & Priestly, page 106 ***)
+
+(** Lemma: Banach's Decomposition Theorem **)
+
+lemma decomp_bnd_mono: "bnd_mono(X, %W. X - g``(Y - f``W))"
+by (rule bnd_monoI, blast+)
+
+lemma Banach_last_equation:
+ "g: Y->X
+ ==> g``(Y - f`` lfp(X, %W. X - g``(Y - f``W))) =
+ X - lfp(X, %W. X - g``(Y - f``W))"
+apply (rule_tac P = "%u. ?v = X-u"
+ in decomp_bnd_mono [THEN lfp_unfold, THEN ssubst])
+apply (simp add: double_complement fun_is_rel [THEN image_subset])
+done
+
+lemma decomposition:
+ "[| f: X->Y; g: Y->X |] ==>
+ EX XA XB YA YB. (XA Int XB = 0) & (XA Un XB = X) &
+ (YA Int YB = 0) & (YA Un YB = Y) &
+ f``XA=YA & g``YB=XB"
+apply (intro exI conjI)
+apply (rule_tac [6] Banach_last_equation)
+apply (rule_tac [5] refl)
+apply (assumption |
+ rule Diff_disjoint Diff_partition fun_is_rel image_subset lfp_subset)+
+done
+
+lemma schroeder_bernstein:
+ "[| f: inj(X,Y); g: inj(Y,X) |] ==> EX h. h: bij(X,Y)"
+apply (insert decomposition [of f X Y g])
+apply (simp add: inj_is_fun)
+apply (blast intro!: restrict_bij bij_disjoint_Un intro: bij_converse_bij)
+(* The instantiation of exI to "restrict(f,XA) Un converse(restrict(g,YB))"
+ is forced by the context!! *)
+done
+
+
+(** Equipollence is an equivalence relation **)
+
+lemma bij_imp_eqpoll: "f: bij(A,B) ==> A \<approx> B"
+apply (unfold eqpoll_def)
+apply (erule exI)
+done
+
+(*A eqpoll A*)
+lemmas eqpoll_refl = id_bij [THEN bij_imp_eqpoll, standard, simp]
+
+lemma eqpoll_sym: "X \<approx> Y ==> Y \<approx> X"
+apply (unfold eqpoll_def)
+apply (blast intro: bij_converse_bij)
+done
+
+lemma eqpoll_trans:
+ "[| X \<approx> Y; Y \<approx> Z |] ==> X \<approx> Z"
+apply (unfold eqpoll_def)
+apply (blast intro: comp_bij)
+done
+
+(** Le-pollence is a partial ordering **)
+
+lemma subset_imp_lepoll: "X<=Y ==> X \<lesssim> Y"
+apply (unfold lepoll_def)
+apply (rule exI)
+apply (erule id_subset_inj)
+done
+
+lemmas lepoll_refl = subset_refl [THEN subset_imp_lepoll, standard, simp]
+
+lemmas le_imp_lepoll = le_imp_subset [THEN subset_imp_lepoll, standard]
+
+lemma eqpoll_imp_lepoll: "X \<approx> Y ==> X \<lesssim> Y"
+by (unfold eqpoll_def bij_def lepoll_def, blast)
+
+lemma lepoll_trans: "[| X \<lesssim> Y; Y \<lesssim> Z |] ==> X \<lesssim> Z"
+apply (unfold lepoll_def)
+apply (blast intro: comp_inj)
+done
+
+(*Asymmetry law*)
+lemma eqpollI: "[| X \<lesssim> Y; Y \<lesssim> X |] ==> X \<approx> Y"
+apply (unfold lepoll_def eqpoll_def)
+apply (elim exE)
+apply (rule schroeder_bernstein, assumption+)
+done
+
+lemma eqpollE:
+ "[| X \<approx> Y; [| X \<lesssim> Y; Y \<lesssim> X |] ==> P |] ==> P"
+by (blast intro: eqpoll_imp_lepoll eqpoll_sym)
+
+lemma eqpoll_iff: "X \<approx> Y <-> X \<lesssim> Y & Y \<lesssim> X"
+by (blast intro: eqpollI elim!: eqpollE)
+
+lemma lepoll_0_is_0: "A \<lesssim> 0 ==> A = 0"
+apply (unfold lepoll_def inj_def)
+apply (blast dest: apply_type)
+done
+
+(*0 \<lesssim> Y*)
+lemmas empty_lepollI = empty_subsetI [THEN subset_imp_lepoll, standard]
+
+lemma lepoll_0_iff: "A \<lesssim> 0 <-> A=0"
+by (blast intro: lepoll_0_is_0 lepoll_refl)
+
+lemma Un_lepoll_Un:
+ "[| A \<lesssim> B; C \<lesssim> D; B Int D = 0 |] ==> A Un C \<lesssim> B Un D"
+apply (unfold lepoll_def)
+apply (blast intro: inj_disjoint_Un)
+done
+
+(*A eqpoll 0 ==> A=0*)
+lemmas eqpoll_0_is_0 = eqpoll_imp_lepoll [THEN lepoll_0_is_0, standard]
+
+lemma eqpoll_0_iff: "A \<approx> 0 <-> A=0"
+by (blast intro: eqpoll_0_is_0 eqpoll_refl)
+
+lemma eqpoll_disjoint_Un:
+ "[| A \<approx> B; C \<approx> D; A Int C = 0; B Int D = 0 |]
+ ==> A Un C \<approx> B Un D"
+apply (unfold eqpoll_def)
+apply (blast intro: bij_disjoint_Un)
+done
+
+
+(*** lesspoll: contributions by Krzysztof Grabczewski ***)
+
+lemma lesspoll_not_refl: "~ (i \<prec> i)"
+by (simp add: lesspoll_def)
+
+lemma lesspoll_irrefl [elim!]: "i \<prec> i ==> P"
+by (simp add: lesspoll_def)
+
+lemma lesspoll_imp_lepoll: "A \<prec> B ==> A \<lesssim> B"
+by (unfold lesspoll_def, blast)
+
+lemma lepoll_well_ord: "[| A \<lesssim> B; well_ord(B,r) |] ==> EX s. well_ord(A,s)"
+apply (unfold lepoll_def)
+apply (blast intro: well_ord_rvimage)
+done
+
+lemma lepoll_iff_leqpoll: "A \<lesssim> B <-> A \<prec> B | A \<approx> B"
+apply (unfold lesspoll_def)
+apply (blast intro!: eqpollI elim!: eqpollE)
+done
+
+lemma inj_not_surj_succ:
+ "[| f : inj(A, succ(m)); f ~: surj(A, succ(m)) |] ==> EX f. f:inj(A,m)"
+apply (unfold inj_def surj_def)
+apply (safe del: succE)
+apply (erule swap, rule exI)
+apply (rule_tac a = "lam z:A. if f`z=m then y else f`z" in CollectI)
+txt{*the typing condition*}
+ apply (best intro!: if_type [THEN lam_type] elim: apply_funtype [THEN succE])
+txt{*Proving it's injective*}
+apply simp
+apply blast
+done
+
+(** Variations on transitivity **)
+
+lemma lesspoll_trans:
+ "[| X \<prec> Y; Y \<prec> Z |] ==> X \<prec> Z"
+apply (unfold lesspoll_def)
+apply (blast elim!: eqpollE intro: eqpollI lepoll_trans)
+done
+
+lemma lesspoll_trans1:
+ "[| X \<lesssim> Y; Y \<prec> Z |] ==> X \<prec> Z"
+apply (unfold lesspoll_def)
+apply (blast elim!: eqpollE intro: eqpollI lepoll_trans)
+done
+
+lemma lesspoll_trans2:
+ "[| X \<prec> Y; Y \<lesssim> Z |] ==> X \<prec> Z"
+apply (unfold lesspoll_def)
+apply (blast elim!: eqpollE intro: eqpollI lepoll_trans)
+done
+
+
+(** LEAST -- the least number operator [from HOL/Univ.ML] **)
+
+lemma Least_equality:
+ "[| P(i); Ord(i); !!x. x<i ==> ~P(x) |] ==> (LEAST x. P(x)) = i"
+apply (unfold Least_def)
+apply (rule the_equality, blast)
+apply (elim conjE)
+apply (erule Ord_linear_lt, assumption, blast+)
+done
+
+lemma LeastI: "[| P(i); Ord(i) |] ==> P(LEAST x. P(x))"
+apply (erule rev_mp)
+apply (erule_tac i=i in trans_induct)
+apply (rule impI)
+apply (rule classical)
+apply (blast intro: Least_equality [THEN ssubst] elim!: ltE)
+done
+
+(*Proof is almost identical to the one above!*)
+lemma Least_le: "[| P(i); Ord(i) |] ==> (LEAST x. P(x)) le i"
+apply (erule rev_mp)
+apply (erule_tac i=i in trans_induct)
+apply (rule impI)
+apply (rule classical)
+apply (subst Least_equality, assumption+)
+apply (erule_tac [2] le_refl)
+apply (blast elim: ltE intro: leI ltI lt_trans1)
+done
+
+(*LEAST really is the smallest*)
+lemma less_LeastE: "[| P(i); i < (LEAST x. P(x)) |] ==> Q"
+apply (rule Least_le [THEN [2] lt_trans2, THEN lt_irrefl], assumption+)
+apply (simp add: lt_Ord)
+done
+
+(*Easier to apply than LeastI: conclusion has only one occurrence of P*)
+lemma LeastI2:
+ "[| P(i); Ord(i); !!j. P(j) ==> Q(j) |] ==> Q(LEAST j. P(j))"
+by (blast intro: LeastI )
+
+(*If there is no such P then LEAST is vacuously 0*)
+lemma Least_0:
+ "[| ~ (EX i. Ord(i) & P(i)) |] ==> (LEAST x. P(x)) = 0"
+apply (unfold Least_def)
+apply (rule the_0, blast)
+done
+
+lemma Ord_Least: "Ord(LEAST x. P(x))"
+apply (rule_tac P = "EX i. Ord(i) & P(i)" in case_split_thm)
+ (*case_tac method not available yet; needs "inductive"*)
+apply safe
+apply (rule Least_le [THEN ltE])
+prefer 3 apply assumption+
+apply (erule Least_0 [THEN ssubst])
+apply (rule Ord_0)
+done
+
+
+(** Basic properties of cardinals **)
+
+(*Not needed for simplification, but helpful below*)
+lemma Least_cong:
+ "(!!y. P(y) <-> Q(y)) ==> (LEAST x. P(x)) = (LEAST x. Q(x))"
+by simp
+
+(*Need AC to get X \<lesssim> Y ==> |X| le |Y|; see well_ord_lepoll_imp_Card_le
+ Converse also requires AC, but see well_ord_cardinal_eqE*)
+lemma cardinal_cong: "X \<approx> Y ==> |X| = |Y|"
+apply (unfold eqpoll_def cardinal_def)
+apply (rule Least_cong)
+apply (blast intro: comp_bij bij_converse_bij)
+done
+
+(*Under AC, the premise becomes trivial; one consequence is ||A|| = |A|*)
+lemma well_ord_cardinal_eqpoll:
+ "well_ord(A,r) ==> |A| \<approx> A"
+apply (unfold cardinal_def)
+apply (rule LeastI)
+apply (erule_tac [2] Ord_ordertype)
+apply (erule ordermap_bij [THEN bij_converse_bij, THEN bij_imp_eqpoll])
+done
+
+(* Ord(A) ==> |A| \<approx> A *)
+lemmas Ord_cardinal_eqpoll = well_ord_Memrel [THEN well_ord_cardinal_eqpoll]
+
+lemma well_ord_cardinal_eqE:
+ "[| well_ord(X,r); well_ord(Y,s); |X| = |Y| |] ==> X \<approx> Y"
+apply (rule eqpoll_sym [THEN eqpoll_trans])
+apply (erule well_ord_cardinal_eqpoll)
+apply (simp (no_asm_simp) add: well_ord_cardinal_eqpoll)
+done
+
+lemma well_ord_cardinal_eqpoll_iff:
+ "[| well_ord(X,r); well_ord(Y,s) |] ==> |X| = |Y| <-> X \<approx> Y"
+by (blast intro: cardinal_cong well_ord_cardinal_eqE)
+
+
+(** Observations from Kunen, page 28 **)
+
+lemma Ord_cardinal_le: "Ord(i) ==> |i| le i"
+apply (unfold cardinal_def)
+apply (erule eqpoll_refl [THEN Least_le])
+done
+
+lemma Card_cardinal_eq: "Card(K) ==> |K| = K"
+apply (unfold Card_def)
+apply (erule sym)
+done
+
+(* Could replace the ~(j \<approx> i) by ~(i \<lesssim> j) *)
+lemma CardI: "[| Ord(i); !!j. j<i ==> ~(j \<approx> i) |] ==> Card(i)"
+apply (unfold Card_def cardinal_def)
+apply (subst Least_equality)
+apply (blast intro: eqpoll_refl )+
+done
+
+lemma Card_is_Ord: "Card(i) ==> Ord(i)"
+apply (unfold Card_def cardinal_def)
+apply (erule ssubst)
+apply (rule Ord_Least)
+done
+
+lemma Card_cardinal_le: "Card(K) ==> K le |K|"
+apply (simp (no_asm_simp) add: Card_is_Ord Card_cardinal_eq)
+done
+
+lemma Ord_cardinal [simp,intro!]: "Ord(|A|)"
+apply (unfold cardinal_def)
+apply (rule Ord_Least)
+done
+
+(*The cardinals are the initial ordinals*)
+lemma Card_iff_initial: "Card(K) <-> Ord(K) & (ALL j. j<K --> ~ j \<approx> K)"
+apply (safe intro!: CardI Card_is_Ord)
+ prefer 2 apply blast
+apply (unfold Card_def cardinal_def)
+apply (rule less_LeastE)
+apply (erule_tac [2] subst, assumption+)
+done
+
+lemma lt_Card_imp_lesspoll: "[| Card(a); i<a |] ==> i \<prec> a"
+apply (unfold lesspoll_def)
+apply (drule Card_iff_initial [THEN iffD1])
+apply (blast intro!: leI [THEN le_imp_lepoll])
+done
+
+lemma Card_0: "Card(0)"
+apply (rule Ord_0 [THEN CardI])
+apply (blast elim!: ltE)
+done
+
+lemma Card_Un: "[| Card(K); Card(L) |] ==> Card(K Un L)"
+apply (rule Ord_linear_le [of K L])
+apply (simp_all add: subset_Un_iff [THEN iffD1] Card_is_Ord le_imp_subset
+ subset_Un_iff2 [THEN iffD1])
+done
+
+(*Infinite unions of cardinals? See Devlin, Lemma 6.7, page 98*)
+
+lemma Card_cardinal: "Card(|A|)"
+apply (unfold cardinal_def)
+apply (rule_tac P = "EX i. Ord (i) & i \<approx> A" in case_split_thm)
+ txt{*degenerate case*}
+ prefer 2 apply (erule Least_0 [THEN ssubst], rule Card_0)
+txt{*real case: A is isomorphic to some ordinal*}
+apply (rule Ord_Least [THEN CardI], safe)
+apply (rule less_LeastE)
+prefer 2 apply assumption
+apply (erule eqpoll_trans)
+apply (best intro: LeastI )
+done
+
+(*Kunen's Lemma 10.5*)
+lemma cardinal_eq_lemma: "[| |i| le j; j le i |] ==> |j| = |i|"
+apply (rule eqpollI [THEN cardinal_cong])
+apply (erule le_imp_lepoll)
+apply (rule lepoll_trans)
+apply (erule_tac [2] le_imp_lepoll)
+apply (rule eqpoll_sym [THEN eqpoll_imp_lepoll])
+apply (rule Ord_cardinal_eqpoll)
+apply (elim ltE Ord_succD)
+done
+
+lemma cardinal_mono: "i le j ==> |i| le |j|"
+apply (rule_tac i = "|i|" and j = "|j|" in Ord_linear_le)
+apply (safe intro!: Ord_cardinal le_eqI)
+apply (rule cardinal_eq_lemma)
+prefer 2 apply assumption
+apply (erule le_trans)
+apply (erule ltE)
+apply (erule Ord_cardinal_le)
+done
+
+(*Since we have |succ(nat)| le |nat|, the converse of cardinal_mono fails!*)
+lemma cardinal_lt_imp_lt: "[| |i| < |j|; Ord(i); Ord(j) |] ==> i < j"
+apply (rule Ord_linear2 [of i j], assumption+)
+apply (erule lt_trans2 [THEN lt_irrefl])
+apply (erule cardinal_mono)
+done
+
+lemma Card_lt_imp_lt: "[| |i| < K; Ord(i); Card(K) |] ==> i < K"
+apply (simp (no_asm_simp) add: cardinal_lt_imp_lt Card_is_Ord Card_cardinal_eq)
+done
+
+lemma Card_lt_iff: "[| Ord(i); Card(K) |] ==> (|i| < K) <-> (i < K)"
+by (blast intro: Card_lt_imp_lt Ord_cardinal_le [THEN lt_trans1])
+
+lemma Card_le_iff: "[| Ord(i); Card(K) |] ==> (K le |i|) <-> (K le i)"
+apply (simp add: Card_lt_iff Card_is_Ord Ord_cardinal not_lt_iff_le [THEN iff_sym])
+done
+
+(*Can use AC or finiteness to discharge first premise*)
+lemma well_ord_lepoll_imp_Card_le:
+ "[| well_ord(B,r); A \<lesssim> B |] ==> |A| le |B|"
+apply (rule_tac i = "|A|" and j = "|B|" in Ord_linear_le)
+apply (safe intro!: Ord_cardinal le_eqI)
+apply (rule eqpollI [THEN cardinal_cong], assumption)
+apply (rule lepoll_trans)
+apply (rule well_ord_cardinal_eqpoll [THEN eqpoll_sym, THEN eqpoll_imp_lepoll], assumption)
+apply (erule le_imp_lepoll [THEN lepoll_trans])
+apply (rule eqpoll_imp_lepoll)
+apply (unfold lepoll_def)
+apply (erule exE)
+apply (rule well_ord_cardinal_eqpoll)
+apply (erule well_ord_rvimage, assumption)
+done
+
+
+lemma lepoll_cardinal_le: "[| A \<lesssim> i; Ord(i) |] ==> |A| le i"
+apply (rule le_trans)
+apply (erule well_ord_Memrel [THEN well_ord_lepoll_imp_Card_le], assumption)
+apply (erule Ord_cardinal_le)
+done
+
+lemma lepoll_Ord_imp_eqpoll: "[| A \<lesssim> i; Ord(i) |] ==> |A| \<approx> A"
+by (blast intro: lepoll_cardinal_le well_ord_Memrel well_ord_cardinal_eqpoll dest!: lepoll_well_ord)
+
+lemma lesspoll_imp_eqpoll:
+ "[| A \<prec> i; Ord(i) |] ==> |A| \<approx> A"
+apply (unfold lesspoll_def)
+apply (blast intro: lepoll_Ord_imp_eqpoll)
+done
+
+
+(*** The finite cardinals ***)
+
+lemma cons_lepoll_consD:
+ "[| cons(u,A) \<lesssim> cons(v,B); u~:A; v~:B |] ==> A \<lesssim> B"
+apply (unfold lepoll_def inj_def, safe)
+apply (rule_tac x = "lam x:A. if f`x=v then f`u else f`x" in exI)
+apply (rule CollectI)
+(*Proving it's in the function space A->B*)
+apply (rule if_type [THEN lam_type])
+apply (blast dest: apply_funtype)
+apply (blast elim!: mem_irrefl dest: apply_funtype)
+(*Proving it's injective*)
+apply (simp (no_asm_simp))
+apply blast
+done
+
+lemma cons_eqpoll_consD: "[| cons(u,A) \<approx> cons(v,B); u~:A; v~:B |] ==> A \<approx> B"
+apply (simp add: eqpoll_iff)
+apply (blast intro: cons_lepoll_consD)
+done
+
+(*Lemma suggested by Mike Fourman*)
+lemma succ_lepoll_succD: "succ(m) \<lesssim> succ(n) ==> m \<lesssim> n"
+apply (unfold succ_def)
+apply (erule cons_lepoll_consD)
+apply (rule mem_not_refl)+
+done
+
+lemma nat_lepoll_imp_le [rule_format]:
+ "m:nat ==> ALL n: nat. m \<lesssim> n --> m le n"
+apply (erule nat_induct) (*induct_tac isn't available yet*)
+apply (blast intro!: nat_0_le)
+apply (rule ballI)
+apply (erule_tac n = "n" in natE)
+apply (simp (no_asm_simp) add: lepoll_def inj_def)
+apply (blast intro!: succ_leI dest!: succ_lepoll_succD)
+done
+
+lemma nat_eqpoll_iff: "[| m:nat; n: nat |] ==> m \<approx> n <-> m = n"
+apply (rule iffI)
+apply (blast intro: nat_lepoll_imp_le le_anti_sym elim!: eqpollE)
+apply (simp add: eqpoll_refl)
+done
+
+(*The object of all this work: every natural number is a (finite) cardinal*)
+lemma nat_into_Card:
+ "n: nat ==> Card(n)"
+apply (unfold Card_def cardinal_def)
+apply (subst Least_equality)
+apply (rule eqpoll_refl)
+apply (erule nat_into_Ord)
+apply (simp (no_asm_simp) add: lt_nat_in_nat [THEN nat_eqpoll_iff])
+apply (blast elim!: lt_irrefl)+
+done
+
+lemmas cardinal_0 = nat_0I [THEN nat_into_Card, THEN Card_cardinal_eq, iff]
+lemmas cardinal_1 = nat_1I [THEN nat_into_Card, THEN Card_cardinal_eq, iff]
+
+
+(*Part of Kunen's Lemma 10.6*)
+lemma succ_lepoll_natE: "[| succ(n) \<lesssim> n; n:nat |] ==> P"
+by (rule nat_lepoll_imp_le [THEN lt_irrefl], auto)
+
+lemma n_lesspoll_nat: "n \<in> nat ==> n \<prec> nat"
+apply (unfold lesspoll_def)
+apply (fast elim!: Ord_nat [THEN [2] ltI [THEN leI, THEN le_imp_lepoll]]
+ eqpoll_sym [THEN eqpoll_imp_lepoll]
+ intro: Ord_nat [THEN [2] nat_succI [THEN ltI], THEN leI,
+ THEN le_imp_lepoll, THEN lepoll_trans, THEN succ_lepoll_natE])
+done
+
+lemma nat_lepoll_imp_ex_eqpoll_n:
+ "[| n \<in> nat; nat \<lesssim> X |] ==> \<exists>Y. Y \<subseteq> X & n \<approx> Y"
+apply (unfold lepoll_def eqpoll_def)
+apply (fast del: subsetI subsetCE
+ intro!: subset_SIs
+ dest!: Ord_nat [THEN [2] OrdmemD, THEN [2] restrict_inj]
+ elim!: restrict_bij
+ inj_is_fun [THEN fun_is_rel, THEN image_subset])
+done
+
+
+(** lepoll, \<prec> and natural numbers **)
+
+lemma lepoll_imp_lesspoll_succ:
+ "[| A \<lesssim> m; m:nat |] ==> A \<prec> succ(m)"
+apply (unfold lesspoll_def)
+apply (rule conjI)
+apply (blast intro: subset_imp_lepoll [THEN [2] lepoll_trans])
+apply (rule notI)
+apply (drule eqpoll_sym [THEN eqpoll_imp_lepoll])
+apply (drule lepoll_trans, assumption)
+apply (erule succ_lepoll_natE, assumption)
+done
+
+lemma lesspoll_succ_imp_lepoll:
+ "[| A \<prec> succ(m); m:nat |] ==> A \<lesssim> m"
+apply (unfold lesspoll_def lepoll_def eqpoll_def bij_def, clarify)
+apply (blast intro!: inj_not_surj_succ)
+done
+
+lemma lesspoll_succ_iff: "m:nat ==> A \<prec> succ(m) <-> A \<lesssim> m"
+by (blast intro!: lepoll_imp_lesspoll_succ lesspoll_succ_imp_lepoll)
+
+lemma lepoll_succ_disj: "[| A \<lesssim> succ(m); m:nat |] ==> A \<lesssim> m | A \<approx> succ(m)"
+apply (rule disjCI)
+apply (rule lesspoll_succ_imp_lepoll)
+prefer 2 apply assumption
+apply (simp (no_asm_simp) add: lesspoll_def)
+done
+
+lemma lesspoll_cardinal_lt: "[| A \<prec> i; Ord(i) |] ==> |A| < i"
+apply (unfold lesspoll_def, clarify)
+apply (frule lepoll_cardinal_le, assumption)
+apply (blast intro: well_ord_Memrel well_ord_cardinal_eqpoll [THEN eqpoll_sym]
+ dest: lepoll_well_ord elim!: leE)
+done
+
+
+(*** The first infinite cardinal: Omega, or nat ***)
+
+(*This implies Kunen's Lemma 10.6*)
+lemma lt_not_lepoll: "[| n<i; n:nat |] ==> ~ i \<lesssim> n"
+apply (rule notI)
+apply (rule succ_lepoll_natE [of n])
+apply (rule lepoll_trans [of _ i])
+apply (erule ltE)
+apply (rule Ord_succ_subsetI [THEN subset_imp_lepoll], assumption+)
+done
+
+lemma Ord_nat_eqpoll_iff: "[| Ord(i); n:nat |] ==> i \<approx> n <-> i=n"
+apply (rule iffI)
+ prefer 2 apply (simp add: eqpoll_refl)
+apply (rule Ord_linear_lt [of i n])
+apply (simp_all add: nat_into_Ord)
+apply (erule lt_nat_in_nat [THEN nat_eqpoll_iff, THEN iffD1], assumption+)
+apply (rule lt_not_lepoll [THEN notE], assumption+)
+apply (erule eqpoll_imp_lepoll)
+done
+
+lemma Card_nat: "Card(nat)"
+apply (unfold Card_def cardinal_def)
+apply (subst Least_equality)
+apply (rule eqpoll_refl)
+apply (rule Ord_nat)
+apply (erule ltE)
+apply (simp_all add: eqpoll_iff lt_not_lepoll ltI)
+done
+
+(*Allows showing that |i| is a limit cardinal*)
+lemma nat_le_cardinal: "nat le i ==> nat le |i|"
+apply (rule Card_nat [THEN Card_cardinal_eq, THEN subst])
+apply (erule cardinal_mono)
+done
+
+
+(*** Towards Cardinal Arithmetic ***)
+(** Congruence laws for successor, cardinal addition and multiplication **)
+
+(*Congruence law for cons under equipollence*)
+lemma cons_lepoll_cong:
+ "[| A \<lesssim> B; b ~: B |] ==> cons(a,A) \<lesssim> cons(b,B)"
+apply (unfold lepoll_def, safe)
+apply (rule_tac x = "lam y: cons (a,A) . if y=a then b else f`y" in exI)
+apply (rule_tac d = "%z. if z:B then converse (f) `z else a" in lam_injective)
+apply (safe elim!: consE')
+ apply simp_all
+apply (blast intro: inj_is_fun [THEN apply_type])+
+done
+
+lemma cons_eqpoll_cong:
+ "[| A \<approx> B; a ~: A; b ~: B |] ==> cons(a,A) \<approx> cons(b,B)"
+by (simp add: eqpoll_iff cons_lepoll_cong)
+
+lemma cons_lepoll_cons_iff:
+ "[| a ~: A; b ~: B |] ==> cons(a,A) \<lesssim> cons(b,B) <-> A \<lesssim> B"
+by (blast intro: cons_lepoll_cong cons_lepoll_consD)
+
+lemma cons_eqpoll_cons_iff:
+ "[| a ~: A; b ~: B |] ==> cons(a,A) \<approx> cons(b,B) <-> A \<approx> B"
+by (blast intro: cons_eqpoll_cong cons_eqpoll_consD)
+
+lemma singleton_eqpoll_1: "{a} \<approx> 1"
+apply (unfold succ_def)
+apply (blast intro!: eqpoll_refl [THEN cons_eqpoll_cong])
+done
+
+lemma cardinal_singleton: "|{a}| = 1"
+apply (rule singleton_eqpoll_1 [THEN cardinal_cong, THEN trans])
+apply (simp (no_asm) add: nat_into_Card [THEN Card_cardinal_eq])
+done
+
+lemma not_0_is_lepoll_1: "A ~= 0 ==> 1 \<lesssim> A"
+apply (erule not_emptyE)
+apply (rule_tac a = "cons (x, A-{x}) " in subst)
+apply (rule_tac [2] a = "cons(0,0)" and P= "%y. y \<lesssim> cons (x, A-{x})" in subst)
+prefer 3 apply (blast intro: cons_lepoll_cong subset_imp_lepoll, auto)
+done
+
+(*Congruence law for succ under equipollence*)
+lemma succ_eqpoll_cong: "A \<approx> B ==> succ(A) \<approx> succ(B)"
+apply (unfold succ_def)
+apply (simp add: cons_eqpoll_cong mem_not_refl)
+done
+
+(*Congruence law for + under equipollence*)
+lemma sum_eqpoll_cong: "[| A \<approx> C; B \<approx> D |] ==> A+B \<approx> C+D"
+apply (unfold eqpoll_def)
+apply (blast intro!: sum_bij)
+done
+
+(*Congruence law for * under equipollence*)
+lemma prod_eqpoll_cong:
+ "[| A \<approx> C; B \<approx> D |] ==> A*B \<approx> C*D"
+apply (unfold eqpoll_def)
+apply (blast intro!: prod_bij)
+done
+
+lemma inj_disjoint_eqpoll:
+ "[| f: inj(A,B); A Int B = 0 |] ==> A Un (B - range(f)) \<approx> B"
+apply (unfold eqpoll_def)
+apply (rule exI)
+apply (rule_tac c = "%x. if x:A then f`x else x"
+ and d = "%y. if y: range (f) then converse (f) `y else y"
+ in lam_bijective)
+apply (blast intro!: if_type inj_is_fun [THEN apply_type])
+apply (simp (no_asm_simp) add: inj_converse_fun [THEN apply_funtype])
+apply (safe elim!: UnE')
+ apply (simp_all add: inj_is_fun [THEN apply_rangeI])
+apply (blast intro: inj_converse_fun [THEN apply_type])+
+done
+
+
+(*** Lemmas by Krzysztof Grabczewski. New proofs using cons_lepoll_cons.
+ Could easily generalise from succ to cons. ***)
+
+(*If A has at most n+1 elements and a:A then A-{a} has at most n.*)
+lemma Diff_sing_lepoll:
+ "[| a:A; A \<lesssim> succ(n) |] ==> A - {a} \<lesssim> n"
+apply (unfold succ_def)
+apply (rule cons_lepoll_consD)
+apply (rule_tac [3] mem_not_refl)
+apply (erule cons_Diff [THEN ssubst], safe)
+done
+
+(*If A has at least n+1 elements then A-{a} has at least n.*)
+lemma lepoll_Diff_sing:
+ "[| succ(n) \<lesssim> A |] ==> n \<lesssim> A - {a}"
+apply (unfold succ_def)
+apply (rule cons_lepoll_consD)
+apply (rule_tac [2] mem_not_refl)
+prefer 2 apply blast
+apply (blast intro: subset_imp_lepoll [THEN [2] lepoll_trans])
+done
+
+lemma Diff_sing_eqpoll: "[| a:A; A \<approx> succ(n) |] ==> A - {a} \<approx> n"
+by (blast intro!: eqpollI
+ elim!: eqpollE
+ intro: Diff_sing_lepoll lepoll_Diff_sing)
+
+lemma lepoll_1_is_sing: "[| A \<lesssim> 1; a:A |] ==> A = {a}"
+apply (frule Diff_sing_lepoll, assumption)
+apply (drule lepoll_0_is_0)
+apply (blast elim: equalityE)
+done
+
+lemma Un_lepoll_sum: "A Un B \<lesssim> A+B"
+apply (unfold lepoll_def)
+apply (rule_tac x = "lam x: A Un B. if x:A then Inl (x) else Inr (x) " in exI)
+apply (rule_tac d = "%z. snd (z) " in lam_injective)
+apply force
+apply (simp add: Inl_def Inr_def)
+done
+
+lemma well_ord_Un:
+ "[| well_ord(X,R); well_ord(Y,S) |] ==> EX T. well_ord(X Un Y, T)"
+by (erule well_ord_radd [THEN Un_lepoll_sum [THEN lepoll_well_ord]],
+ assumption)
+
+(*Krzysztof Grabczewski*)
+lemma disj_Un_eqpoll_sum: "A Int B = 0 ==> A Un B \<approx> A + B"
+apply (unfold eqpoll_def)
+apply (rule_tac x = "lam a:A Un B. if a:A then Inl (a) else Inr (a) " in exI)
+apply (rule_tac d = "%z. case (%x. x, %x. x, z) " in lam_bijective)
+apply auto
+done
+
+
+(*** Finite and infinite sets ***)
+
+lemma Finite_0: "Finite(0)"
+apply (unfold Finite_def)
+apply (blast intro!: eqpoll_refl nat_0I)
+done
+
+lemma lepoll_nat_imp_Finite: "[| A \<lesssim> n; n:nat |] ==> Finite(A)"
+apply (unfold Finite_def)
+apply (erule rev_mp)
+apply (erule nat_induct)
+apply (blast dest!: lepoll_0_is_0 intro!: eqpoll_refl nat_0I)
+apply (blast dest!: lepoll_succ_disj)
+done
+
+lemma lesspoll_nat_is_Finite:
+ "A \<prec> nat ==> Finite(A)"
+apply (unfold Finite_def)
+apply (blast dest: ltD lesspoll_cardinal_lt
+ lesspoll_imp_eqpoll [THEN eqpoll_sym])
+done
+
+lemma lepoll_Finite:
+ "[| Y \<lesssim> X; Finite(X) |] ==> Finite(Y)"
+apply (unfold Finite_def)
+apply (blast elim!: eqpollE
+ intro: lepoll_trans [THEN lepoll_nat_imp_Finite
+ [unfolded Finite_def]])
+done
+
+lemmas subset_Finite = subset_imp_lepoll [THEN lepoll_Finite, standard]
+
+lemmas Finite_Diff = Diff_subset [THEN subset_Finite, standard]
+
+lemma Finite_cons: "Finite(x) ==> Finite(cons(y,x))"
+apply (unfold Finite_def)
+apply (rule_tac P = "y:x" in case_split_thm)
+apply (simp add: cons_absorb)
+apply (erule bexE)
+apply (rule bexI)
+apply (erule_tac [2] nat_succI)
+apply (simp (no_asm_simp) add: succ_def cons_eqpoll_cong mem_not_refl)
+done
+
+lemma Finite_succ: "Finite(x) ==> Finite(succ(x))"
+apply (unfold succ_def)
+apply (erule Finite_cons)
+done
+
+lemma nat_le_infinite_Ord:
+ "[| Ord(i); ~ Finite(i) |] ==> nat le i"
+apply (unfold Finite_def)
+apply (erule Ord_nat [THEN [2] Ord_linear2])
+prefer 2 apply assumption
+apply (blast intro!: eqpoll_refl elim!: ltE)
+done
+
+lemma Finite_imp_well_ord:
+ "Finite(A) ==> EX r. well_ord(A,r)"
+apply (unfold Finite_def eqpoll_def)
+apply (blast intro: well_ord_rvimage bij_is_inj well_ord_Memrel nat_into_Ord)
+done
+
+
+(*Krzysztof Grabczewski's proof that the converse of a finite, well-ordered
+ set is well-ordered. Proofs simplified by lcp. *)
+
+lemma nat_wf_on_converse_Memrel: "n:nat ==> wf[n](converse(Memrel(n)))"
+apply (erule nat_induct)
+apply (blast intro: wf_onI)
+apply (rule wf_onI)
+apply (simp add: wf_on_def wf_def)
+apply (rule_tac P = "x:Z" in case_split_thm)
+ txt{*x:Z case*}
+ apply (drule_tac x = x in bspec, assumption)
+ apply (blast elim: mem_irrefl mem_asym)
+txt{*other case*}
+apply (drule_tac x = "Z" in spec, blast)
+done
+
+lemma nat_well_ord_converse_Memrel: "n:nat ==> well_ord(n,converse(Memrel(n)))"
+apply (frule Ord_nat [THEN Ord_in_Ord, THEN well_ord_Memrel])
+apply (unfold well_ord_def)
+apply (blast intro!: tot_ord_converse nat_wf_on_converse_Memrel)
+done
+
+lemma well_ord_converse:
+ "[|well_ord(A,r);
+ well_ord(ordertype(A,r), converse(Memrel(ordertype(A, r)))) |]
+ ==> well_ord(A,converse(r))"
+apply (rule well_ord_Int_iff [THEN iffD1])
+apply (frule ordermap_bij [THEN bij_is_inj, THEN well_ord_rvimage], assumption)
+apply (simp add: rvimage_converse converse_Int converse_prod
+ ordertype_ord_iso [THEN ord_iso_rvimage_eq])
+done
+
+lemma ordertype_eq_n:
+ "[| well_ord(A,r); A \<approx> n; n:nat |] ==> ordertype(A,r)=n"
+apply (rule Ord_ordertype [THEN Ord_nat_eqpoll_iff, THEN iffD1], assumption+)
+apply (rule eqpoll_trans)
+ prefer 2 apply assumption
+apply (unfold eqpoll_def)
+apply (blast intro!: ordermap_bij [THEN bij_converse_bij])
+done
+
+lemma Finite_well_ord_converse:
+ "[| Finite(A); well_ord(A,r) |] ==> well_ord(A,converse(r))"
+apply (unfold Finite_def)
+apply (rule well_ord_converse, assumption)
+apply (blast dest: ordertype_eq_n intro!: nat_well_ord_converse_Memrel)
+done
+
+lemma nat_into_Finite: "n:nat ==> Finite(n)"
+apply (unfold Finite_def)
+apply (fast intro!: eqpoll_refl)
+done
+
+ML
+{*
+val Least_def = thm "Least_def";
+val eqpoll_def = thm "eqpoll_def";
+val lepoll_def = thm "lepoll_def";
+val lesspoll_def = thm "lesspoll_def";
+val cardinal_def = thm "cardinal_def";
+val Finite_def = thm "Finite_def";
+val Card_def = thm "Card_def";
+val eq_imp_not_mem = thm "eq_imp_not_mem";
+val decomp_bnd_mono = thm "decomp_bnd_mono";
+val Banach_last_equation = thm "Banach_last_equation";
+val decomposition = thm "decomposition";
+val schroeder_bernstein = thm "schroeder_bernstein";
+val bij_imp_eqpoll = thm "bij_imp_eqpoll";
+val eqpoll_refl = thm "eqpoll_refl";
+val eqpoll_sym = thm "eqpoll_sym";
+val eqpoll_trans = thm "eqpoll_trans";
+val subset_imp_lepoll = thm "subset_imp_lepoll";
+val lepoll_refl = thm "lepoll_refl";
+val le_imp_lepoll = thm "le_imp_lepoll";
+val eqpoll_imp_lepoll = thm "eqpoll_imp_lepoll";
+val lepoll_trans = thm "lepoll_trans";
+val eqpollI = thm "eqpollI";
+val eqpollE = thm "eqpollE";
+val eqpoll_iff = thm "eqpoll_iff";
+val lepoll_0_is_0 = thm "lepoll_0_is_0";
+val empty_lepollI = thm "empty_lepollI";
+val lepoll_0_iff = thm "lepoll_0_iff";
+val Un_lepoll_Un = thm "Un_lepoll_Un";
+val eqpoll_0_is_0 = thm "eqpoll_0_is_0";
+val eqpoll_0_iff = thm "eqpoll_0_iff";
+val eqpoll_disjoint_Un = thm "eqpoll_disjoint_Un";
+val lesspoll_not_refl = thm "lesspoll_not_refl";
+val lesspoll_irrefl = thm "lesspoll_irrefl";
+val lesspoll_imp_lepoll = thm "lesspoll_imp_lepoll";
+val lepoll_well_ord = thm "lepoll_well_ord";
+val lepoll_iff_leqpoll = thm "lepoll_iff_leqpoll";
+val inj_not_surj_succ = thm "inj_not_surj_succ";
+val lesspoll_trans = thm "lesspoll_trans";
+val lesspoll_trans1 = thm "lesspoll_trans1";
+val lesspoll_trans2 = thm "lesspoll_trans2";
+val Least_equality = thm "Least_equality";
+val LeastI = thm "LeastI";
+val Least_le = thm "Least_le";
+val less_LeastE = thm "less_LeastE";
+val LeastI2 = thm "LeastI2";
+val Least_0 = thm "Least_0";
+val Ord_Least = thm "Ord_Least";
+val Least_cong = thm "Least_cong";
+val cardinal_cong = thm "cardinal_cong";
+val well_ord_cardinal_eqpoll = thm "well_ord_cardinal_eqpoll";
+val Ord_cardinal_eqpoll = thm "Ord_cardinal_eqpoll";
+val well_ord_cardinal_eqE = thm "well_ord_cardinal_eqE";
+val well_ord_cardinal_eqpoll_iff = thm "well_ord_cardinal_eqpoll_iff";
+val Ord_cardinal_le = thm "Ord_cardinal_le";
+val Card_cardinal_eq = thm "Card_cardinal_eq";
+val CardI = thm "CardI";
+val Card_is_Ord = thm "Card_is_Ord";
+val Card_cardinal_le = thm "Card_cardinal_le";
+val Ord_cardinal = thm "Ord_cardinal";
+val Card_iff_initial = thm "Card_iff_initial";
+val lt_Card_imp_lesspoll = thm "lt_Card_imp_lesspoll";
+val Card_0 = thm "Card_0";
+val Card_Un = thm "Card_Un";
+val Card_cardinal = thm "Card_cardinal";
+val cardinal_mono = thm "cardinal_mono";
+val cardinal_lt_imp_lt = thm "cardinal_lt_imp_lt";
+val Card_lt_imp_lt = thm "Card_lt_imp_lt";
+val Card_lt_iff = thm "Card_lt_iff";
+val Card_le_iff = thm "Card_le_iff";
+val well_ord_lepoll_imp_Card_le = thm "well_ord_lepoll_imp_Card_le";
+val lepoll_cardinal_le = thm "lepoll_cardinal_le";
+val lepoll_Ord_imp_eqpoll = thm "lepoll_Ord_imp_eqpoll";
+val lesspoll_imp_eqpoll = thm "lesspoll_imp_eqpoll";
+val cons_lepoll_consD = thm "cons_lepoll_consD";
+val cons_eqpoll_consD = thm "cons_eqpoll_consD";
+val succ_lepoll_succD = thm "succ_lepoll_succD";
+val nat_lepoll_imp_le = thm "nat_lepoll_imp_le";
+val nat_eqpoll_iff = thm "nat_eqpoll_iff";
+val nat_into_Card = thm "nat_into_Card";
+val cardinal_0 = thm "cardinal_0";
+val cardinal_1 = thm "cardinal_1";
+val succ_lepoll_natE = thm "succ_lepoll_natE";
+val n_lesspoll_nat = thm "n_lesspoll_nat";
+val nat_lepoll_imp_ex_eqpoll_n = thm "nat_lepoll_imp_ex_eqpoll_n";
+val lepoll_imp_lesspoll_succ = thm "lepoll_imp_lesspoll_succ";
+val lesspoll_succ_imp_lepoll = thm "lesspoll_succ_imp_lepoll";
+val lesspoll_succ_iff = thm "lesspoll_succ_iff";
+val lepoll_succ_disj = thm "lepoll_succ_disj";
+val lesspoll_cardinal_lt = thm "lesspoll_cardinal_lt";
+val lt_not_lepoll = thm "lt_not_lepoll";
+val Ord_nat_eqpoll_iff = thm "Ord_nat_eqpoll_iff";
+val Card_nat = thm "Card_nat";
+val nat_le_cardinal = thm "nat_le_cardinal";
+val cons_lepoll_cong = thm "cons_lepoll_cong";
+val cons_eqpoll_cong = thm "cons_eqpoll_cong";
+val cons_lepoll_cons_iff = thm "cons_lepoll_cons_iff";
+val cons_eqpoll_cons_iff = thm "cons_eqpoll_cons_iff";
+val singleton_eqpoll_1 = thm "singleton_eqpoll_1";
+val cardinal_singleton = thm "cardinal_singleton";
+val not_0_is_lepoll_1 = thm "not_0_is_lepoll_1";
+val succ_eqpoll_cong = thm "succ_eqpoll_cong";
+val sum_eqpoll_cong = thm "sum_eqpoll_cong";
+val prod_eqpoll_cong = thm "prod_eqpoll_cong";
+val inj_disjoint_eqpoll = thm "inj_disjoint_eqpoll";
+val Diff_sing_lepoll = thm "Diff_sing_lepoll";
+val lepoll_Diff_sing = thm "lepoll_Diff_sing";
+val Diff_sing_eqpoll = thm "Diff_sing_eqpoll";
+val lepoll_1_is_sing = thm "lepoll_1_is_sing";
+val Un_lepoll_sum = thm "Un_lepoll_sum";
+val well_ord_Un = thm "well_ord_Un";
+val disj_Un_eqpoll_sum = thm "disj_Un_eqpoll_sum";
+val Finite_0 = thm "Finite_0";
+val lepoll_nat_imp_Finite = thm "lepoll_nat_imp_Finite";
+val lesspoll_nat_is_Finite = thm "lesspoll_nat_is_Finite";
+val lepoll_Finite = thm "lepoll_Finite";
+val subset_Finite = thm "subset_Finite";
+val Finite_Diff = thm "Finite_Diff";
+val Finite_cons = thm "Finite_cons";
+val Finite_succ = thm "Finite_succ";
+val nat_le_infinite_Ord = thm "nat_le_infinite_Ord";
+val Finite_imp_well_ord = thm "Finite_imp_well_ord";
+val nat_wf_on_converse_Memrel = thm "nat_wf_on_converse_Memrel";
+val nat_well_ord_converse_Memrel = thm "nat_well_ord_converse_Memrel";
+val well_ord_converse = thm "well_ord_converse";
+val ordertype_eq_n = thm "ordertype_eq_n";
+val Finite_well_ord_converse = thm "Finite_well_ord_converse";
+val nat_into_Finite = thm "nat_into_Finite";
+*}
end
--- a/src/ZF/CardinalArith.thy Tue Jun 18 18:45:07 2002 +0200
+++ b/src/ZF/CardinalArith.thy Wed Jun 19 09:03:34 2002 +0200
@@ -45,81 +45,6 @@
"op |*|" :: "[i,i] => i" (infixl "\<otimes>" 70)
-(*** The following really belong early in the development ***)
-
-lemma relation_converse_converse [simp]:
- "relation(r) ==> converse(converse(r)) = r"
-by (simp add: relation_def, blast)
-
-lemma relation_restrict [simp]: "relation(restrict(r,A))"
-by (simp add: restrict_def relation_def, blast)
-
-(*** The following really belong in Order ***)
-
-lemma subset_ord_iso_Memrel:
- "[| f: ord_iso(A,Memrel(B),C,r); A<=B |] ==> f: ord_iso(A,Memrel(A),C,r)"
-apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN fun_is_rel])
-apply (frule ord_iso_trans [OF id_ord_iso_Memrel], assumption)
-apply (simp add: right_comp_id)
-done
-
-lemma restrict_ord_iso:
- "[| f \<in> ord_iso(i, Memrel(i), Order.pred(A,a,r), r); a \<in> A; j < i;
- trans[A](r) |]
- ==> restrict(f,j) \<in> ord_iso(j, Memrel(j), Order.pred(A,f`j,r), r)"
-apply (frule ltD)
-apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type], assumption)
-apply (frule ord_iso_restrict_pred, assumption)
-apply (simp add: pred_iff trans_pred_pred_eq lt_pred_Memrel)
-apply (blast intro!: subset_ord_iso_Memrel le_imp_subset [OF leI])
-done
-
-lemma restrict_ord_iso2:
- "[| f \<in> ord_iso(Order.pred(A,a,r), r, i, Memrel(i)); a \<in> A;
- j < i; trans[A](r) |]
- ==> converse(restrict(converse(f), j))
- \<in> ord_iso(Order.pred(A, converse(f)`j, r), r, j, Memrel(j))"
-by (blast intro: restrict_ord_iso ord_iso_sym ltI)
-
-(*** The following really belong in OrderType ***)
-
-lemma oadd_eq_0_iff: "[| Ord(i); Ord(j) |] ==> (i ++ j) = 0 <-> i=0 & j=0"
-apply (erule trans_induct3 [of j])
-apply (simp_all add: oadd_Limit)
-apply (simp add: Union_empty_iff Limit_def lt_def, blast)
-done
-
-lemma oadd_eq_lt_iff: "[| Ord(i); Ord(j) |] ==> 0 < (i ++ j) <-> 0<i | 0<j"
-by (simp add: Ord_0_lt_iff [symmetric] oadd_eq_0_iff)
-
-lemma oadd_lt_self: "[| Ord(i); 0<j |] ==> i < i++j"
-apply (rule lt_trans2)
-apply (erule le_refl)
-apply (simp only: lt_Ord2 oadd_1 [of i, symmetric])
-apply (blast intro: succ_leI oadd_le_mono)
-done
-
-lemma oadd_LimitI: "[| Ord(i); Limit(j) |] ==> Limit(i ++ j)"
-apply (simp add: oadd_Limit)
-apply (frule Limit_has_1 [THEN ltD])
-apply (rule increasing_LimitI)
- apply (rule Ord_0_lt)
- apply (blast intro: Ord_in_Ord [OF Limit_is_Ord])
- apply (force simp add: Union_empty_iff oadd_eq_0_iff
- Limit_is_Ord [of j, THEN Ord_in_Ord], auto)
-apply (rule_tac x="succ(x)" in bexI)
- apply (simp add: ltI Limit_is_Ord [of j, THEN Ord_in_Ord])
-apply (simp add: Limit_def lt_def)
-done
-
-(*** The following really belong in Cardinal ***)
-
-lemma lesspoll_not_refl: "~ (i lesspoll i)"
-by (simp add: lesspoll_def)
-
-lemma lesspoll_irrefl [elim!]: "i lesspoll i ==> P"
-by (simp add: lesspoll_def)
-
lemma Card_Union [simp,intro,TC]: "(ALL x:A. Card(x)) ==> Card(Union(A))"
apply (rule CardI)
apply (simp add: Card_is_Ord)
@@ -230,11 +155,11 @@
apply (rule cardinal_cong)
apply (rule eqpoll_trans)
apply (rule sum_eqpoll_cong [OF well_ord_cardinal_eqpoll eqpoll_refl])
- apply (blast intro: well_ord_radd elim:)
+ apply (blast intro: well_ord_radd )
apply (rule sum_assoc_eqpoll [THEN eqpoll_trans])
apply (rule eqpoll_sym)
apply (rule sum_eqpoll_cong [OF eqpoll_refl well_ord_cardinal_eqpoll])
-apply (blast intro: well_ord_radd elim:)
+apply (blast intro: well_ord_radd )
done
(** 0 is the identity for addition **)
@@ -255,7 +180,7 @@
lemma sum_lepoll_self: "A \<lesssim> A+B"
apply (unfold lepoll_def inj_def)
apply (rule_tac x = "lam x:A. Inl (x) " in exI)
-apply (simp (no_asm_simp))
+apply simp
done
(*Could probably weaken the premises to well_ord(K,r), or removing using AC*)
@@ -263,8 +188,8 @@
lemma cadd_le_self:
"[| Card(K); Ord(L) |] ==> K le (K |+| L)"
apply (unfold cadd_def)
-apply (rule le_trans [OF Card_cardinal_le well_ord_lepoll_imp_Card_le])
-apply assumption;
+apply (rule le_trans [OF Card_cardinal_le well_ord_lepoll_imp_Card_le],
+ assumption)
apply (rule_tac [2] sum_lepoll_self)
apply (blast intro: well_ord_radd well_ord_Memrel Card_is_Ord)
done
@@ -272,14 +197,13 @@
(** Monotonicity of addition **)
lemma sum_lepoll_mono:
- "[| A \<lesssim> C; B \<lesssim> D |] ==> A + B \<lesssim> C + D"
+ "[| A \<lesssim> C; B \<lesssim> D |] ==> A + B \<lesssim> C + D"
apply (unfold lepoll_def)
-apply (elim exE);
+apply (elim exE)
apply (rule_tac x = "lam z:A+B. case (%w. Inl(f`w), %y. Inr(fa`y), z)" in exI)
-apply (rule_tac d = "case (%w. Inl(converse(f) `w), %y. Inr(converse(fa) `y))"
+apply (rule_tac d = "case (%w. Inl(converse(f) `w), %y. Inr(converse(fa) ` y))"
in lam_injective)
-apply (typecheck add: inj_is_fun)
-apply auto
+apply (typecheck add: inj_is_fun, auto)
done
lemma cadd_le_mono:
@@ -293,17 +217,12 @@
(** Addition of finite cardinals is "ordinary" addition **)
-(*????????????????upair.ML*)
-lemma eq_imp_not_mem: "a=A ==> a ~: A"
-apply (blast intro: elim: mem_irrefl);
-done
-
lemma sum_succ_eqpoll: "succ(A)+B \<approx> succ(A+B)"
apply (unfold eqpoll_def)
apply (rule exI)
apply (rule_tac c = "%z. if z=Inl (A) then A+B else z"
and d = "%z. if z=A+B then Inl (A) else z" in lam_bijective)
- apply (simp_all)
+ apply simp_all
apply (blast dest: sym [THEN eq_imp_not_mem] elim: mem_irrefl)+
done
@@ -333,8 +252,8 @@
lemma prod_commute_eqpoll: "A*B \<approx> B*A"
apply (unfold eqpoll_def)
apply (rule exI)
-apply (rule_tac c = "%<x,y>.<y,x>" and d = "%<x,y>.<y,x>" in lam_bijective)
-apply (auto );
+apply (rule_tac c = "%<x,y>.<y,x>" and d = "%<x,y>.<y,x>" in lam_bijective,
+ auto)
done
lemma cmult_commute: "i |*| j = j |*| i"
@@ -356,11 +275,11 @@
==> (i |*| j) |*| k = i |*| (j |*| k)"
apply (unfold cmult_def)
apply (rule cardinal_cong)
-apply (rule eqpoll_trans);
+apply (rule eqpoll_trans)
apply (rule prod_eqpoll_cong [OF well_ord_cardinal_eqpoll eqpoll_refl])
apply (blast intro: well_ord_rmult)
apply (rule prod_assoc_eqpoll [THEN eqpoll_trans])
-apply (rule eqpoll_sym);
+apply (rule eqpoll_sym)
apply (rule prod_eqpoll_cong [OF eqpoll_refl well_ord_cardinal_eqpoll])
apply (blast intro: well_ord_rmult)
done
@@ -378,11 +297,11 @@
==> (i |+| j) |*| k = (i |*| k) |+| (j |*| k)"
apply (unfold cadd_def cmult_def)
apply (rule cardinal_cong)
-apply (rule eqpoll_trans);
+apply (rule eqpoll_trans)
apply (rule prod_eqpoll_cong [OF well_ord_cardinal_eqpoll eqpoll_refl])
apply (blast intro: well_ord_radd)
apply (rule sum_prod_distrib_eqpoll [THEN eqpoll_trans])
-apply (rule eqpoll_sym);
+apply (rule eqpoll_sym)
apply (rule sum_eqpoll_cong [OF well_ord_cardinal_eqpoll
well_ord_cardinal_eqpoll])
apply (blast intro: well_ord_rmult)+
@@ -393,13 +312,11 @@
lemma prod_0_eqpoll: "0*A \<approx> 0"
apply (unfold eqpoll_def)
apply (rule exI)
-apply (rule lam_bijective)
-apply safe
+apply (rule lam_bijective, safe)
done
lemma cmult_0 [simp]: "0 |*| i = 0"
-apply (simp add: cmult_def prod_0_eqpoll [THEN cardinal_cong])
-done
+by (simp add: cmult_def prod_0_eqpoll [THEN cardinal_cong])
(** 1 is the identity for multiplication **)
@@ -418,8 +335,7 @@
lemma prod_square_lepoll: "A \<lesssim> A*A"
apply (unfold lepoll_def inj_def)
-apply (rule_tac x = "lam x:A. <x,x>" in exI)
-apply (simp (no_asm))
+apply (rule_tac x = "lam x:A. <x,x>" in exI, simp)
done
(*Could probably weaken the premise to well_ord(K,r), or remove using AC*)
@@ -428,16 +344,15 @@
apply (rule le_trans)
apply (rule_tac [2] well_ord_lepoll_imp_Card_le)
apply (rule_tac [3] prod_square_lepoll)
-apply (simp (no_asm_simp) add: le_refl Card_is_Ord Card_cardinal_eq)
-apply (blast intro: well_ord_rmult well_ord_Memrel Card_is_Ord);
+apply (simp add: le_refl Card_is_Ord Card_cardinal_eq)
+apply (blast intro: well_ord_rmult well_ord_Memrel Card_is_Ord)
done
(** Multiplication by a non-zero cardinal **)
lemma prod_lepoll_self: "b: B ==> A \<lesssim> A*B"
apply (unfold lepoll_def inj_def)
-apply (rule_tac x = "lam x:A. <x,b>" in exI)
-apply (simp (no_asm_simp))
+apply (rule_tac x = "lam x:A. <x,b>" in exI, simp)
done
(*Could probably weaken the premises to well_ord(K,r), or removing using AC*)
@@ -445,7 +360,7 @@
"[| Card(K); Ord(L); 0<L |] ==> K le (K |*| L)"
apply (unfold cmult_def)
apply (rule le_trans [OF Card_cardinal_le well_ord_lepoll_imp_Card_le])
- apply assumption;
+ apply assumption
apply (blast intro: well_ord_rmult well_ord_Memrel Card_is_Ord)
apply (blast intro: prod_lepoll_self ltD)
done
@@ -455,12 +370,11 @@
lemma prod_lepoll_mono:
"[| A \<lesssim> C; B \<lesssim> D |] ==> A * B \<lesssim> C * D"
apply (unfold lepoll_def)
-apply (elim exE);
+apply (elim exE)
apply (rule_tac x = "lam <w,y>:A*B. <f`w, fa`y>" in exI)
apply (rule_tac d = "%<w,y>. <converse (f) `w, converse (fa) `y>"
in lam_injective)
-apply (typecheck add: inj_is_fun)
-apply auto
+apply (typecheck add: inj_is_fun, auto)
done
lemma cmult_le_mono:
@@ -476,7 +390,7 @@
lemma prod_succ_eqpoll: "succ(A)*B \<approx> B + A*B"
apply (unfold eqpoll_def)
-apply (rule exI);
+apply (rule exI)
apply (rule_tac c = "%<x,y>. if x=A then Inl (y) else Inr (<x,y>)"
and d = "case (%y. <A,y>, %z. z)" in lam_bijective)
apply safe
@@ -495,24 +409,21 @@
lemma nat_cmult_eq_mult: "[| m: nat; n: nat |] ==> m |*| n = m#*n"
apply (induct_tac "m")
-apply (simp (no_asm_simp))
-apply (simp (no_asm_simp) add: cmult_succ_lemma nat_cadd_eq_add)
+apply (simp_all add: cmult_succ_lemma nat_cadd_eq_add)
done
lemma cmult_2: "Card(n) ==> 2 |*| n = n |+| n"
-apply (simp add: cmult_succ_lemma Card_is_Ord cadd_commute [of _ 0])
-done
+by (simp add: cmult_succ_lemma Card_is_Ord cadd_commute [of _ 0])
lemma sum_lepoll_prod: "2 \<lesssim> C ==> B+B \<lesssim> C*B"
-apply (rule lepoll_trans);
+apply (rule lepoll_trans)
apply (rule sum_eq_2_times [THEN equalityD1, THEN subset_imp_lepoll])
apply (erule prod_lepoll_mono)
-apply (rule lepoll_refl);
+apply (rule lepoll_refl)
done
lemma lepoll_imp_sum_lepoll_prod: "[| A \<lesssim> B; 2 \<lesssim> A |] ==> A+B \<lesssim> A*B"
-apply (blast intro: sum_lepoll_mono sum_lepoll_prod lepoll_trans lepoll_refl)
-done
+by (blast intro: sum_lepoll_mono sum_lepoll_prod lepoll_trans lepoll_refl)
(*** Infinite Cardinals are Limit Ordinals ***)
@@ -578,8 +489,7 @@
apply (drule trans)
apply (erule le_imp_subset [THEN nat_succ_eqpoll, THEN cardinal_cong])
apply (erule Ord_cardinal_le [THEN lt_trans2, THEN lt_irrefl])
-apply (rule le_eqI)
-apply assumption;
+apply (rule le_eqI, assumption)
apply (rule Ord_cardinal)
done
@@ -591,8 +501,9 @@
"[| well_ord(A,r); x:A |] ==> ordermap(A,r)`x \<approx> pred(A,x,r)"
apply (unfold eqpoll_def)
apply (rule exI)
-apply (simp (no_asm_simp) add: ordermap_eq_image well_ord_is_wf)
-apply (erule ordermap_bij [THEN bij_is_inj, THEN restrict_bij, THEN bij_converse_bij])
+apply (simp add: ordermap_eq_image well_ord_is_wf)
+apply (erule ordermap_bij [THEN bij_is_inj, THEN restrict_bij,
+ THEN bij_converse_bij])
apply (rule pred_subset)
done
@@ -606,8 +517,7 @@
lemma well_ord_csquare: "Ord(K) ==> well_ord(K*K, csquare_rel(K))"
apply (unfold csquare_rel_def)
-apply (rule csquare_lam_inj [THEN well_ord_rvimage])
-apply assumption;
+apply (rule csquare_lam_inj [THEN well_ord_rvimage], assumption)
apply (blast intro: well_ord_rmult well_ord_Memrel)
done
@@ -618,9 +528,9 @@
apply (unfold csquare_rel_def)
apply (erule rev_mp)
apply (elim ltE)
-apply (simp (no_asm_simp) add: rvimage_iff Un_absorb Un_least_mem_iff ltD)
+apply (simp add: rvimage_iff Un_absorb Un_least_mem_iff ltD)
apply (safe elim!: mem_irrefl intro!: Un_upper1_le Un_upper2_le)
-apply (simp_all (no_asm_simp) add: lt_def succI2)
+apply (simp_all add: lt_def succI2)
done
lemma pred_csquare_subset:
@@ -628,8 +538,7 @@
apply (unfold Order.pred_def)
apply (safe del: SigmaI succCI)
apply (erule csquareD [THEN conjE])
-apply (unfold lt_def)
-apply (auto );
+apply (unfold lt_def, auto)
done
lemma csquare_ltI:
@@ -638,7 +547,7 @@
apply (subgoal_tac "x<K & y<K")
prefer 2 apply (blast intro: lt_trans)
apply (elim ltE)
-apply (simp (no_asm_simp) add: rvimage_iff Un_absorb Un_least_mem_iff ltD)
+apply (simp add: rvimage_iff Un_absorb Un_least_mem_iff ltD)
done
(*Part of the traditional proof. UNUSED since it's harder to prove & apply *)
@@ -648,9 +557,10 @@
apply (subgoal_tac "x<K & y<K")
prefer 2 apply (blast intro: lt_trans1)
apply (elim ltE)
-apply (simp (no_asm_simp) add: rvimage_iff Un_absorb Un_least_mem_iff ltD)
+apply (simp add: rvimage_iff Un_absorb Un_least_mem_iff ltD)
apply (elim succE)
-apply (simp_all (no_asm_simp) add: subset_Un_iff [THEN iff_sym] subset_Un_iff2 [THEN iff_sym] OrdmemD)
+apply (simp_all add: subset_Un_iff [THEN iff_sym]
+ subset_Un_iff2 [THEN iff_sym] OrdmemD)
done
(** The cardinality of initial segments **)
@@ -661,8 +571,7 @@
ordermap(K*K, csquare_rel(K)) ` <z,z>"
apply (subgoal_tac "z<K & well_ord (K*K, csquare_rel (K))")
prefer 2 apply (blast intro!: Un_least_lt Limit_has_succ
- Limit_is_Ord [THEN well_ord_csquare])
-apply (clarify );
+ Limit_is_Ord [THEN well_ord_csquare], clarify)
apply (rule csquare_ltI [THEN ordermap_mono, THEN ltI])
apply (erule_tac [4] well_ord_is_wf)
apply (blast intro!: Un_upper1_le Un_upper2_le Ord_ordermap elim!: ltE)+
@@ -670,15 +579,15 @@
(*Kunen: "each <x,y>: K*K has no more than z*z predecessors..." (page 29) *)
lemma ordermap_csquare_le:
- "[| Limit(K); x<K; y<K; z=succ(x Un y) |] ==>
- | ordermap(K*K, csquare_rel(K)) ` <x,y> | le |succ(z)| |*| |succ(z)|"
+ "[| Limit(K); x<K; y<K; z=succ(x Un y) |]
+ ==> | ordermap(K*K, csquare_rel(K)) ` <x,y> | le |succ(z)| |*| |succ(z)|"
apply (unfold cmult_def)
apply (rule well_ord_rmult [THEN well_ord_lepoll_imp_Card_le])
apply (rule Ord_cardinal [THEN well_ord_Memrel])+
apply (subgoal_tac "z<K")
prefer 2 apply (blast intro!: Un_least_lt Limit_has_succ)
-apply (rule ordermap_z_lt [THEN leI, THEN le_imp_lepoll, THEN lepoll_trans])
-apply assumption +
+apply (rule ordermap_z_lt [THEN leI, THEN le_imp_lepoll, THEN lepoll_trans],
+ assumption+)
apply (rule ordermap_eqpoll_pred [THEN eqpoll_imp_lepoll, THEN lepoll_trans])
apply (erule Limit_is_Ord [THEN well_ord_csquare])
apply (blast intro: ltD)
@@ -694,8 +603,7 @@
"[| InfCard(K); ALL y:K. InfCard(y) --> y |*| y = y |]
==> ordertype(K*K, csquare_rel(K)) le K"
apply (frule InfCard_is_Card [THEN Card_is_Ord])
-apply (rule all_lt_imp_le)
-apply assumption
+apply (rule all_lt_imp_le, assumption)
apply (erule well_ord_csquare [THEN Ord_ordertype])
apply (rule Card_lt_imp_lt)
apply (erule_tac [3] InfCard_is_Card)
@@ -703,8 +611,7 @@
apply (simp add: ordertype_unfold)
apply (safe elim!: ltE)
apply (subgoal_tac "Ord (xa) & Ord (ya)")
- prefer 2 apply (blast intro: Ord_in_Ord)
-apply (clarify );
+ prefer 2 apply (blast intro: Ord_in_Ord, clarify)
(*??WHAT A MESS!*)
apply (rule InfCard_is_Limit [THEN ordermap_csquare_le, THEN lt_trans1],
(assumption | rule refl | erule ltI)+)
@@ -730,9 +637,10 @@
apply (rule le_anti_sym)
apply (erule_tac [2] InfCard_is_Card [THEN cmult_square_le])
apply (rule ordertype_csquare_le [THEN [2] le_trans])
-prefer 2 apply (assumption)
-prefer 2 apply (assumption)
-apply (simp (no_asm_simp) add: cmult_def Ord_cardinal_le well_ord_csquare [THEN ordermap_bij, THEN bij_imp_eqpoll, THEN cardinal_cong] well_ord_csquare [THEN Ord_ordertype])
+apply (simp add: cmult_def Ord_cardinal_le
+ well_ord_csquare [THEN Ord_ordertype]
+ well_ord_csquare [THEN ordermap_bij, THEN bij_imp_eqpoll,
+ THEN cardinal_cong], assumption+)
done
(*Corollary for arbitrary well-ordered sets (all sets, assuming AC)*)
@@ -741,9 +649,8 @@
apply (rule prod_eqpoll_cong [THEN eqpoll_trans])
apply (erule well_ord_cardinal_eqpoll [THEN eqpoll_sym])+
apply (rule well_ord_cardinal_eqE)
-apply (blast intro: Ord_cardinal well_ord_rmult well_ord_Memrel)
-apply assumption;
-apply (simp (no_asm_simp) add: cmult_def [symmetric] InfCard_csquare_eq)
+apply (blast intro: Ord_cardinal well_ord_rmult well_ord_Memrel, assumption)
+apply (simp add: cmult_def [symmetric] InfCard_csquare_eq)
done
(** Toward's Kunen's Corollary 10.13 (1) **)
@@ -763,12 +670,13 @@
apply (typecheck add: InfCard_is_Card Card_is_Ord)
apply (rule cmult_commute [THEN ssubst])
apply (rule Un_commute [THEN ssubst])
-apply (simp_all (no_asm_simp) add: InfCard_is_Limit [THEN Limit_has_0] InfCard_le_cmult_eq subset_Un_iff2 [THEN iffD1] le_imp_subset)
+apply (simp_all add: InfCard_is_Limit [THEN Limit_has_0] InfCard_le_cmult_eq
+ subset_Un_iff2 [THEN iffD1] le_imp_subset)
done
lemma InfCard_cdouble_eq: "InfCard(K) ==> K |+| K = K"
-apply (simp (no_asm_simp) add: cmult_2 [symmetric] InfCard_is_Card cmult_commute)
-apply (simp (no_asm_simp) add: InfCard_le_cmult_eq InfCard_is_Limit Limit_has_0 Limit_has_succ)
+apply (simp add: cmult_2 [symmetric] InfCard_is_Card cmult_commute)
+apply (simp add: InfCard_le_cmult_eq InfCard_is_Limit Limit_has_0 Limit_has_succ)
done
(*Corollary 10.13 (1), for cardinal addition*)
@@ -786,7 +694,7 @@
apply (typecheck add: InfCard_is_Card Card_is_Ord)
apply (rule cadd_commute [THEN ssubst])
apply (rule Un_commute [THEN ssubst])
-apply (simp_all (no_asm_simp) add: InfCard_le_cadd_eq subset_Un_iff2 [THEN iffD1] le_imp_subset)
+apply (simp_all add: InfCard_le_cadd_eq subset_Un_iff2 [THEN iffD1] le_imp_subset)
done
(*The other part, Corollary 10.13 (2), refers to the cardinality of the set
@@ -803,8 +711,7 @@
prefer 2 apply (blast intro!: Ord_ordertype)
apply (unfold Transset_def)
apply (safe del: subsetI)
-apply (simp add: ordertype_pred_unfold)
-apply safe
+apply (simp add: ordertype_pred_unfold, safe)
apply (rule UN_I)
apply (rule_tac [2] ReplaceI)
prefer 4 apply (blast intro: well_ord_subset elim!: predE)+
@@ -838,8 +745,7 @@
prefer 2 apply (blast intro: comp_bij ordermap_bij)
apply (rule jump_cardinal_iff [THEN iffD2])
apply (intro exI conjI)
-apply (rule subset_trans [OF rvimage_type Sigma_mono])
-apply assumption+
+apply (rule subset_trans [OF rvimage_type Sigma_mono], assumption+)
apply (erule bij_is_inj [THEN well_ord_rvimage])
apply (rule Ord_jump_cardinal [THEN well_ord_Memrel])
apply (simp add: well_ord_Memrel [THEN [2] bij_ordertype_vimage]
@@ -867,8 +773,7 @@
lemmas lt_csucc = csucc_basic [THEN conjunct2, standard]
lemma Ord_0_lt_csucc: "Ord(K) ==> 0 < csucc(K)"
-apply (blast intro: Ord_0_le lt_csucc lt_trans1)
-done
+by (blast intro: Ord_0_le lt_csucc lt_trans1)
lemma csucc_le: "[| Card(L); K<L |] ==> csucc(K) le L"
apply (unfold csucc_def)
@@ -882,15 +787,14 @@
apply (erule_tac [2] lt_trans1)
apply (simp_all add: lt_csucc Card_csucc Card_is_Ord)
apply (rule notI [THEN not_lt_imp_le])
-apply (rule Card_cardinal [THEN csucc_le, THEN lt_trans1, THEN lt_irrefl])
-apply assumption
+apply (rule Card_cardinal [THEN csucc_le, THEN lt_trans1, THEN lt_irrefl], assumption)
apply (rule Ord_cardinal_le [THEN lt_trans1])
apply (simp_all add: Ord_cardinal Card_is_Ord)
done
lemma Card_lt_csucc_iff:
"[| Card(K'); Card(K) |] ==> K' < csucc(K) <-> K' le K"
-by (simp (no_asm_simp) add: lt_csucc_iff Card_cardinal_eq Card_is_Ord)
+by (simp add: lt_csucc_iff Card_cardinal_eq Card_is_Ord)
lemma InfCard_csucc: "InfCard(K) ==> InfCard(csucc(K))"
by (simp add: InfCard_def Card_csucc Card_is_Ord
@@ -901,17 +805,14 @@
lemma Fin_lemma [rule_format]: "n: nat ==> ALL A. A \<approx> n --> A : Fin(A)"
apply (induct_tac "n")
-apply (simp (no_asm) add: eqpoll_0_iff)
-apply clarify
+apply (simp add: eqpoll_0_iff, clarify)
apply (subgoal_tac "EX u. u:A")
apply (erule exE)
apply (rule Diff_sing_eqpoll [THEN revcut_rl])
-prefer 2 apply (assumption)
+prefer 2 apply assumption
apply assumption
-apply (rule_tac b = "A" in cons_Diff [THEN subst])
-apply assumption
-apply (rule Fin.consI)
-apply blast
+apply (rule_tac b = "A" in cons_Diff [THEN subst], assumption)
+apply (rule Fin.consI, blast)
apply (blast intro: subset_consI [THEN Fin_mono, THEN subsetD])
(*Now for the lemma assumed above*)
apply (unfold eqpoll_def)
@@ -924,12 +825,10 @@
done
lemma Fin_into_Finite: "A : Fin(U) ==> Finite(A)"
-apply (fast intro!: Finite_0 Finite_cons elim: Fin_induct)
-done
+by (fast intro!: Finite_0 Finite_cons elim: Fin_induct)
lemma Finite_Fin_iff: "Finite(A) <-> A : Fin(A)"
-apply (blast intro: Finite_into_Fin Fin_into_Finite)
-done
+by (blast intro: Finite_into_Fin Fin_into_Finite)
lemma Finite_Un: "[| Finite(A); Finite(B) |] ==> Finite(A Un B)"
by (blast intro!: Fin_into_Finite Fin_UnI
@@ -940,8 +839,7 @@
lemma Finite_Union: "[| ALL y:X. Finite(y); Finite(X) |] ==> Finite(Union(X))"
apply (simp add: Finite_Fin_iff)
apply (rule Fin_UnionI)
-apply (erule Fin_induct)
-apply (simp (no_asm))
+apply (erule Fin_induct, simp)
apply (blast intro: Fin.consI Fin_mono [THEN [2] rev_subsetD])
done
@@ -959,25 +857,24 @@
lemma Fin_imp_not_cons_lepoll: "A: Fin(U) ==> x~:A --> ~ cons(x,A) \<lesssim> A"
apply (erule Fin_induct)
-apply (simp (no_asm) add: lepoll_0_iff)
+apply (simp add: lepoll_0_iff)
apply (subgoal_tac "cons (x,cons (xa,y)) = cons (xa,cons (x,y))")
-apply (simp (no_asm_simp))
-apply (blast dest!: cons_lepoll_consD)
-apply blast
+apply simp
+apply (blast dest!: cons_lepoll_consD, blast)
done
-lemma Finite_imp_cardinal_cons: "[| Finite(A); a~:A |] ==> |cons(a,A)| = succ(|A|)"
+lemma Finite_imp_cardinal_cons:
+ "[| Finite(A); a~:A |] ==> |cons(a,A)| = succ(|A|)"
apply (unfold cardinal_def)
apply (rule Least_equality)
apply (fold cardinal_def)
-apply (simp (no_asm) add: succ_def)
+apply (simp add: succ_def)
apply (blast intro: cons_eqpoll_cong well_ord_cardinal_eqpoll
elim!: mem_irrefl dest!: Finite_imp_well_ord)
apply (blast intro: Card_cardinal Card_is_Ord)
apply (rule notI)
-apply (rule Finite_into_Fin [THEN Fin_imp_not_cons_lepoll, THEN mp, THEN notE])
-apply assumption
-apply assumption
+apply (rule Finite_into_Fin [THEN Fin_imp_not_cons_lepoll, THEN mp, THEN notE],
+ assumption, assumption)
apply (erule eqpoll_sym [THEN eqpoll_imp_lepoll, THEN lepoll_trans])
apply (erule le_imp_lepoll [THEN lepoll_trans])
apply (blast intro: well_ord_cardinal_eqpoll [THEN eqpoll_imp_lepoll]
@@ -985,16 +882,16 @@
done
-lemma Finite_imp_succ_cardinal_Diff: "[| Finite(A); a:A |] ==> succ(|A-{a}|) = |A|"
-apply (rule_tac b = "A" in cons_Diff [THEN subst])
-apply assumption
-apply (simp (no_asm_simp) add: Finite_imp_cardinal_cons Diff_subset [THEN subset_Finite])
-apply (simp (no_asm_simp) add: cons_Diff)
+lemma Finite_imp_succ_cardinal_Diff:
+ "[| Finite(A); a:A |] ==> succ(|A-{a}|) = |A|"
+apply (rule_tac b = "A" in cons_Diff [THEN subst], assumption)
+apply (simp add: Finite_imp_cardinal_cons Diff_subset [THEN subset_Finite])
+apply (simp add: cons_Diff)
done
lemma Finite_imp_cardinal_Diff: "[| Finite(A); a:A |] ==> |A-{a}| < |A|"
apply (rule succ_leE)
-apply (simp (no_asm_simp) add: Finite_imp_succ_cardinal_Diff)
+apply (simp add: Finite_imp_succ_cardinal_Diff)
done
@@ -1006,7 +903,7 @@
apply (rule eqpoll_trans)
apply (rule well_ord_radd [THEN well_ord_cardinal_eqpoll, THEN eqpoll_sym])
apply (erule nat_implies_well_ord)+
-apply (simp (no_asm_simp) add: nat_cadd_eq_add [symmetric] cadd_def eqpoll_refl)
+apply (simp add: nat_cadd_eq_add [symmetric] cadd_def eqpoll_refl)
done
@@ -1016,8 +913,7 @@
lemma Diff_sing_Finite: "Finite(A - {a}) ==> Finite(A)"
apply (unfold Finite_def)
apply (case_tac "a:A")
-apply (subgoal_tac [2] "A-{a}=A")
-apply auto
+apply (subgoal_tac [2] "A-{a}=A", auto)
apply (rule_tac x = "succ (n) " in bexI)
apply (subgoal_tac "cons (a, A - {a}) = A & cons (n, n) = succ (n) ")
apply (drule_tac a = "a" and b = "n" in cons_eqpoll_cong)
@@ -1026,27 +922,22 @@
(*And the contrapositive of this says
[| ~Finite(A); Finite(B) |] ==> ~Finite(A-B) *)
-lemma Diff_Finite [rule_format (no_asm)]: "Finite(B) ==> Finite(A-B) --> Finite(A)"
-apply (erule Finite_induct)
-apply auto
+lemma Diff_Finite [rule_format]: "Finite(B) ==> Finite(A-B) --> Finite(A)"
+apply (erule Finite_induct, auto)
apply (case_tac "x:A")
apply (subgoal_tac [2] "A-cons (x, B) = A - B")
apply (subgoal_tac "A - cons (x, B) = (A - B) - {x}")
-apply (rotate_tac -1)
-apply simp
-apply (drule Diff_sing_Finite)
-apply auto
+apply (rotate_tac -1, simp)
+apply (drule Diff_sing_Finite, auto)
done
-lemma Ord_subset_natD [rule_format (no_asm)]: "Ord(i) ==> i <= nat --> i : nat | i=nat"
-apply (erule trans_induct3)
-apply auto
+lemma Ord_subset_natD [rule_format]: "Ord(i) ==> i <= nat --> i : nat | i=nat"
+apply (erule trans_induct3, auto)
apply (blast dest!: nat_le_Limit [THEN le_imp_subset])
done
lemma Ord_nat_subset_into_Card: "[| Ord(i); i <= nat |] ==> Card(i)"
-apply (blast dest: Ord_subset_natD intro: Card_nat nat_into_Card)
-done
+by (blast dest: Ord_subset_natD intro: Card_nat nat_into_Card)
lemma Finite_cardinal_in_nat [simp]: "Finite(A) ==> |A| : nat"
apply (erule Finite_induct)
@@ -1056,11 +947,10 @@
lemma Finite_Diff_sing_eq_diff_1: "[| Finite(A); x:A |] ==> |A-{x}| = |A| #- 1"
apply (rule succ_inject)
apply (rule_tac b = "|A|" in trans)
-apply (simp (no_asm_simp) add: Finite_imp_succ_cardinal_Diff)
+apply (simp add: Finite_imp_succ_cardinal_Diff)
apply (subgoal_tac "1 \<lesssim> A")
-prefer 2 apply (blast intro: not_0_is_lepoll_1)
-apply (frule Finite_imp_well_ord)
-apply clarify
+ prefer 2 apply (blast intro: not_0_is_lepoll_1)
+apply (frule Finite_imp_well_ord, clarify)
apply (rotate_tac -1)
apply (drule well_ord_lepoll_imp_Card_le)
apply (auto simp add: cardinal_1)
@@ -1069,21 +959,21 @@
apply (auto simp add: Finite_cardinal_in_nat)
done
-lemma cardinal_lt_imp_Diff_not_0 [rule_format (no_asm)]: "Finite(B) ==> ALL A. |B|<|A| --> A - B ~= 0"
-apply (erule Finite_induct)
-apply auto
+lemma cardinal_lt_imp_Diff_not_0 [rule_format]:
+ "Finite(B) ==> ALL A. |B|<|A| --> A - B ~= 0"
+apply (erule Finite_induct, auto)
apply (simp_all add: Finite_imp_cardinal_cons)
-apply (case_tac "Finite (A) ")
-apply (subgoal_tac [2] "Finite (cons (x, B))")
-apply (drule_tac [2] B = "cons (x, B) " in Diff_Finite)
-apply (auto simp add: Finite_0 Finite_cons)
+apply (case_tac "Finite (A)")
+ apply (subgoal_tac [2] "Finite (cons (x, B))")
+ apply (drule_tac [2] B = "cons (x, B) " in Diff_Finite)
+ apply (auto simp add: Finite_0 Finite_cons)
apply (subgoal_tac "|B|<|A|")
-prefer 2 apply (blast intro: lt_trans Ord_cardinal)
+ prefer 2 apply (blast intro: lt_trans Ord_cardinal)
apply (case_tac "x:A")
-apply (subgoal_tac [2] "A - cons (x, B) = A - B")
-apply auto
+ apply (subgoal_tac [2] "A - cons (x, B) = A - B")
+ apply auto
apply (subgoal_tac "|A| le |cons (x, B) |")
-prefer 2
+ prefer 2
apply (blast dest: Finite_cons [THEN Finite_imp_well_ord]
intro: well_ord_lepoll_imp_Card_le subset_imp_lepoll)
apply (auto simp add: Finite_imp_cardinal_cons)
--- a/src/ZF/OrderType.thy Tue Jun 18 18:45:07 2002 +0200
+++ b/src/ZF/OrderType.thy Wed Jun 19 09:03:34 2002 +0200
@@ -12,6 +12,7 @@
*)
theory OrderType = OrderArith + OrdQuant:
+
constdefs
ordermap :: "[i,i]=>i"
@@ -469,7 +470,7 @@
apply (auto simp add: Ord_oadd lt_oadd1)
done
-(** A couple of strange but necessary results! **)
+(** Various other results **)
lemma id_ord_iso_Memrel: "A<=B ==> id(A) : ord_iso(A, Memrel(A), A, Memrel(B))"
apply (rule id_bij [THEN ord_isoI])
@@ -477,6 +478,31 @@
apply blast
done
+lemma subset_ord_iso_Memrel:
+ "[| f: ord_iso(A,Memrel(B),C,r); A<=B |] ==> f: ord_iso(A,Memrel(A),C,r)"
+apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN fun_is_rel])
+apply (frule ord_iso_trans [OF id_ord_iso_Memrel], assumption)
+apply (simp add: right_comp_id)
+done
+
+lemma restrict_ord_iso:
+ "[| f \<in> ord_iso(i, Memrel(i), Order.pred(A,a,r), r); a \<in> A; j < i;
+ trans[A](r) |]
+ ==> restrict(f,j) \<in> ord_iso(j, Memrel(j), Order.pred(A,f`j,r), r)"
+apply (frule ltD)
+apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type], assumption)
+apply (frule ord_iso_restrict_pred, assumption)
+apply (simp add: pred_iff trans_pred_pred_eq lt_pred_Memrel)
+apply (blast intro!: subset_ord_iso_Memrel le_imp_subset [OF leI])
+done
+
+lemma restrict_ord_iso2:
+ "[| f \<in> ord_iso(Order.pred(A,a,r), r, i, Memrel(i)); a \<in> A;
+ j < i; trans[A](r) |]
+ ==> converse(restrict(converse(f), j))
+ \<in> ord_iso(Order.pred(A, converse(f)`j, r), r, j, Memrel(j))"
+by (blast intro: restrict_ord_iso ord_iso_sym ltI)
+
lemma ordertype_sum_Memrel:
"[| well_ord(A,r); k<j |]
==> ordertype(A+k, radd(A, r, k, Memrel(j))) =
@@ -582,6 +608,28 @@
apply (simp (no_asm_simp) add: Limit_is_Ord [THEN Ord_in_Ord] oadd_UN [symmetric] Union_eq_UN [symmetric] Limit_Union_eq)
done
+lemma oadd_eq_0_iff: "[| Ord(i); Ord(j) |] ==> (i ++ j) = 0 <-> i=0 & j=0"
+apply (erule trans_induct3 [of j])
+apply (simp_all add: oadd_Limit)
+apply (simp add: Union_empty_iff Limit_def lt_def, blast)
+done
+
+lemma oadd_eq_lt_iff: "[| Ord(i); Ord(j) |] ==> 0 < (i ++ j) <-> 0<i | 0<j"
+by (simp add: Ord_0_lt_iff [symmetric] oadd_eq_0_iff)
+
+lemma oadd_LimitI: "[| Ord(i); Limit(j) |] ==> Limit(i ++ j)"
+apply (simp add: oadd_Limit)
+apply (frule Limit_has_1 [THEN ltD])
+apply (rule increasing_LimitI)
+ apply (rule Ord_0_lt)
+ apply (blast intro: Ord_in_Ord [OF Limit_is_Ord])
+ apply (force simp add: Union_empty_iff oadd_eq_0_iff
+ Limit_is_Ord [of j, THEN Ord_in_Ord], auto)
+apply (rule_tac x="succ(x)" in bexI)
+ apply (simp add: ltI Limit_is_Ord [of j, THEN Ord_in_Ord])
+apply (simp add: Limit_def lt_def)
+done
+
(** Order/monotonicity properties of ordinal addition **)
lemma oadd_le_self2: "Ord(i) ==> i le j++i"
@@ -617,6 +665,13 @@
lemma oadd_le_iff2: "[| Ord(j); Ord(k) |] ==> i++j le i++k <-> j le k"
by (simp del: oadd_succ add: oadd_lt_iff2 oadd_succ [symmetric] Ord_succ)
+lemma oadd_lt_self: "[| Ord(i); 0<j |] ==> i < i++j"
+apply (rule lt_trans2)
+apply (erule le_refl)
+apply (simp only: lt_Ord2 oadd_1 [of i, symmetric])
+apply (blast intro: succ_leI oadd_le_mono)
+done
+
(** Ordinal subtraction; the difference is ordertype(j-i, Memrel(j)).
Probably simpler to define the difference recursively!
--- a/src/ZF/func.thy Tue Jun 18 18:45:07 2002 +0200
+++ b/src/ZF/func.thy Wed Jun 19 09:03:34 2002 +0200
@@ -8,6 +8,13 @@
theory func = equalities:
+lemma relation_converse_converse [simp]:
+ "relation(r) ==> converse(converse(r)) = r"
+by (simp add: relation_def, blast)
+
+lemma relation_restrict [simp]: "relation(restrict(r,A))"
+by (simp add: restrict_def relation_def, blast)
+
(*** The Pi operator -- dependent function space ***)
lemma Pi_iff: