# HG changeset patch # User paulson # Date 1024470214 -7200 # Node ID e29378f347e423323f26d009c92b2169469e0492 # Parent 62c899c771513e92b005922371b28d9f3cc586c9 conversion of Cardinal, CardinalArith diff -r 62c899c77151 -r e29378f347e4 src/ZF/Cardinal.ML --- 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 ~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 ~(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 ~ 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 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 \\ 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 \\ nat; nat lepoll X |] ==> \\Y. Y \\ 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 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"; - - diff -r 62c899c77151 -r e29378f347e4 src/ZF/Cardinal.thy --- 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 ~P(j))" + Least :: "(i=>o) => i" (binder "LEAST " 10) + "Least(P) == THE i. Ord(i) & P(i) & (ALL j. j ~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 "\\" 50) - "op lepoll" :: [i,i] => o (infixl "\\" 50) - "op lesspoll" :: [i,i] => o (infixl "\\" 50) - "LEAST " :: [pttrn, o] => i ("(3\\_./ _)" [0, 10] 10) + "eqpoll" :: "[i,i] => o" (infixl "\" 50) + "lepoll" :: "[i,i] => o" (infixl "\" 50) + "lesspoll" :: "[i,i] => o" (infixl "\" 50) + "LEAST " :: "[pttrn, o] => i" ("(3\_./ _)" [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 \ 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 \ Y ==> Y \ X" +apply (unfold eqpoll_def) +apply (blast intro: bij_converse_bij) +done + +lemma eqpoll_trans: + "[| X \ Y; Y \ Z |] ==> X \ Z" +apply (unfold eqpoll_def) +apply (blast intro: comp_bij) +done + +(** Le-pollence is a partial ordering **) + +lemma subset_imp_lepoll: "X<=Y ==> X \ 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 \ Y ==> X \ Y" +by (unfold eqpoll_def bij_def lepoll_def, blast) + +lemma lepoll_trans: "[| X \ Y; Y \ Z |] ==> X \ Z" +apply (unfold lepoll_def) +apply (blast intro: comp_inj) +done + +(*Asymmetry law*) +lemma eqpollI: "[| X \ Y; Y \ X |] ==> X \ Y" +apply (unfold lepoll_def eqpoll_def) +apply (elim exE) +apply (rule schroeder_bernstein, assumption+) +done + +lemma eqpollE: + "[| X \ Y; [| X \ Y; Y \ X |] ==> P |] ==> P" +by (blast intro: eqpoll_imp_lepoll eqpoll_sym) + +lemma eqpoll_iff: "X \ Y <-> X \ Y & Y \ X" +by (blast intro: eqpollI elim!: eqpollE) + +lemma lepoll_0_is_0: "A \ 0 ==> A = 0" +apply (unfold lepoll_def inj_def) +apply (blast dest: apply_type) +done + +(*0 \ Y*) +lemmas empty_lepollI = empty_subsetI [THEN subset_imp_lepoll, standard] + +lemma lepoll_0_iff: "A \ 0 <-> A=0" +by (blast intro: lepoll_0_is_0 lepoll_refl) + +lemma Un_lepoll_Un: + "[| A \ B; C \ D; B Int D = 0 |] ==> A Un C \ 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 \ 0 <-> A=0" +by (blast intro: eqpoll_0_is_0 eqpoll_refl) + +lemma eqpoll_disjoint_Un: + "[| A \ B; C \ D; A Int C = 0; B Int D = 0 |] + ==> A Un C \ B Un D" +apply (unfold eqpoll_def) +apply (blast intro: bij_disjoint_Un) +done + + +(*** lesspoll: contributions by Krzysztof Grabczewski ***) + +lemma lesspoll_not_refl: "~ (i \ i)" +by (simp add: lesspoll_def) + +lemma lesspoll_irrefl [elim!]: "i \ i ==> P" +by (simp add: lesspoll_def) + +lemma lesspoll_imp_lepoll: "A \ B ==> A \ B" +by (unfold lesspoll_def, blast) + +lemma lepoll_well_ord: "[| A \ 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 \ B <-> A \ B | A \ 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 \ Y; Y \ Z |] ==> X \ Z" +apply (unfold lesspoll_def) +apply (blast elim!: eqpollE intro: eqpollI lepoll_trans) +done + +lemma lesspoll_trans1: + "[| X \ Y; Y \ Z |] ==> X \ Z" +apply (unfold lesspoll_def) +apply (blast elim!: eqpollE intro: eqpollI lepoll_trans) +done + +lemma lesspoll_trans2: + "[| X \ Y; Y \ Z |] ==> X \ 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 ~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 \ 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 \ 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| \ 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| \ 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 \ 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 \ 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 \ i) by ~(i \ j) *) +lemma CardI: "[| Ord(i); !!j. j ~(j \ 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 ~ j \ 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 i \ 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 \ 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 \ 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 \ 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 \ i; Ord(i) |] ==> |A| \ A" +by (blast intro: lepoll_cardinal_le well_ord_Memrel well_ord_cardinal_eqpoll dest!: lepoll_well_ord) + +lemma lesspoll_imp_eqpoll: + "[| A \ i; Ord(i) |] ==> |A| \ A" +apply (unfold lesspoll_def) +apply (blast intro: lepoll_Ord_imp_eqpoll) +done + + +(*** The finite cardinals ***) + +lemma cons_lepoll_consD: + "[| cons(u,A) \ cons(v,B); u~:A; v~:B |] ==> A \ 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) \ cons(v,B); u~:A; v~:B |] ==> A \ B" +apply (simp add: eqpoll_iff) +apply (blast intro: cons_lepoll_consD) +done + +(*Lemma suggested by Mike Fourman*) +lemma succ_lepoll_succD: "succ(m) \ succ(n) ==> m \ 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 \ 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 \ 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) \ n; n:nat |] ==> P" +by (rule nat_lepoll_imp_le [THEN lt_irrefl], auto) + +lemma n_lesspoll_nat: "n \ nat ==> n \ 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 \ nat; nat \ X |] ==> \Y. Y \ X & n \ 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, \ and natural numbers **) + +lemma lepoll_imp_lesspoll_succ: + "[| A \ m; m:nat |] ==> A \ 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 \ succ(m); m:nat |] ==> A \ 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 \ succ(m) <-> A \ m" +by (blast intro!: lepoll_imp_lesspoll_succ lesspoll_succ_imp_lepoll) + +lemma lepoll_succ_disj: "[| A \ succ(m); m:nat |] ==> A \ m | A \ 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 \ 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" +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 \ 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 \ B; b ~: B |] ==> cons(a,A) \ 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 \ B; a ~: A; b ~: B |] ==> cons(a,A) \ cons(b,B)" +by (simp add: eqpoll_iff cons_lepoll_cong) + +lemma cons_lepoll_cons_iff: + "[| a ~: A; b ~: B |] ==> cons(a,A) \ cons(b,B) <-> A \ B" +by (blast intro: cons_lepoll_cong cons_lepoll_consD) + +lemma cons_eqpoll_cons_iff: + "[| a ~: A; b ~: B |] ==> cons(a,A) \ cons(b,B) <-> A \ B" +by (blast intro: cons_eqpoll_cong cons_eqpoll_consD) + +lemma singleton_eqpoll_1: "{a} \ 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 \ 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 \ 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 \ B ==> succ(A) \ 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 \ C; B \ D |] ==> A+B \ C+D" +apply (unfold eqpoll_def) +apply (blast intro!: sum_bij) +done + +(*Congruence law for * under equipollence*) +lemma prod_eqpoll_cong: + "[| A \ C; B \ D |] ==> A*B \ 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)) \ 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 \ succ(n) |] ==> A - {a} \ 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) \ A |] ==> n \ 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 \ succ(n) |] ==> A - {a} \ n" +by (blast intro!: eqpollI + elim!: eqpollE + intro: Diff_sing_lepoll lepoll_Diff_sing) + +lemma lepoll_1_is_sing: "[| A \ 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 \ 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 \ 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 \ 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 \ 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 \ 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 \ 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 diff -r 62c899c77151 -r e29378f347e4 src/ZF/CardinalArith.thy --- 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 "\" 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 \ ord_iso(i, Memrel(i), Order.pred(A,a,r), r); a \ A; j < i; - trans[A](r) |] - ==> restrict(f,j) \ 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 \ ord_iso(Order.pred(A,a,r), r, i, Memrel(i)); a \ A; - j < i; trans[A](r) |] - ==> converse(restrict(converse(f), j)) - \ 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 < 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 \ 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 \ C; B \ D |] ==> A + B \ C + D" + "[| A \ C; B \ D |] ==> A + B \ 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 \ 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 \ B*A" apply (unfold eqpoll_def) apply (rule exI) -apply (rule_tac c = "%." and d = "%." in lam_bijective) -apply (auto ); +apply (rule_tac c = "%." and d = "%." 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 \ 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 \ A*A" apply (unfold lepoll_def inj_def) -apply (rule_tac x = "lam x:A. " in exI) -apply (simp (no_asm)) +apply (rule_tac x = "lam x:A. " 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 \ A*B" apply (unfold lepoll_def inj_def) -apply (rule_tac x = "lam x:A. " in exI) -apply (simp (no_asm_simp)) +apply (rule_tac x = "lam x:A. " 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 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 \ C; B \ D |] ==> A * B \ C * D" apply (unfold lepoll_def) -apply (elim exE); +apply (elim exE) apply (rule_tac x = "lam :A*B. " in exI) apply (rule_tac d = "%. " 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 \ B + A*B" apply (unfold eqpoll_def) -apply (rule exI); +apply (rule exI) apply (rule_tac c = "%. if x=A then Inl (y) else Inr ()" and d = "case (%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 \ C ==> B+B \ 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 \ B; 2 \ A |] ==> A+B \ 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 \ 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" apply (subgoal_tac "z: K*K has no more than z*z predecessors..." (page 29) *) lemma ordermap_csquare_le: - "[| Limit(K); x - | ordermap(K*K, csquare_rel(K)) ` | le |succ(z)| |*| |succ(z)|" + "[| Limit(K); x | ordermap(K*K, csquare_rel(K)) ` | 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 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 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 \ 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) \ 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 \ 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) diff -r 62c899c77151 -r e29378f347e4 src/ZF/OrderType.thy --- 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 \ ord_iso(i, Memrel(i), Order.pred(A,a,r), r); a \ A; j < i; + trans[A](r) |] + ==> restrict(f,j) \ 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 \ ord_iso(Order.pred(A,a,r), r, i, Memrel(i)); a \ A; + j < i; trans[A](r) |] + ==> converse(restrict(converse(f), j)) + \ 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 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 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 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! diff -r 62c899c77151 -r e29378f347e4 src/ZF/func.thy --- 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: