# HG changeset patch # User paulson # Date 947781090 -3600 # Node ID a71686059be0e529b8ed7c9ae18ad5108cece610 # Parent b43ad07660b970e0e1388ec5d96fbd783892c8c8 a bit of tidying diff -r b43ad07660b9 -r a71686059be0 src/ZF/AC/AC16_WO4.ML --- a/src/ZF/AC/AC16_WO4.ML Thu Jan 13 17:30:23 2000 +0100 +++ b/src/ZF/AC/AC16_WO4.ML Thu Jan 13 17:31:30 2000 +0100 @@ -44,8 +44,9 @@ Goal "EX y R. well_ord(y,R) & x Int y = 0 & ~y lepoll z & ~Finite(y)"; by (res_inst_tac [("x","{{a,x}. a:nat Un Hartog(z)}")] exI 1); -by (resolve_tac [transfer thy Ord_nat RS well_ord_Memrel RS (Ord_Hartog RS - well_ord_Memrel RSN (2, well_ord_Un)) RS exE] 1); +by (resolve_tac [transfer thy Ord_nat RS well_ord_Memrel RS + (Ord_Hartog RS + well_ord_Memrel RSN (2, well_ord_Un)) RS exE] 1); by (fast_tac (claset() addSIs [Ord_Hartog, well_ord_Memrel, well_ord_paired, HartogI RSN (2, lepoll_trans1), @@ -55,9 +56,8 @@ lepoll_paired RS lepoll_Finite]) 1); val lemma2 = result(); -val [prem] = goal thy "~Finite(B) ==> ~Finite(A Un B)"; -by (fast_tac (claset() - addSIs [subset_imp_lepoll RS (prem RSN (2, lepoll_infinite))]) 1); +Goal "~Finite(B) ==> ~Finite(A Un B)"; +by (blast_tac (claset() addIs [subset_Finite]) 1); qed "infinite_Un"; (* ********************************************************************** *) @@ -613,7 +613,8 @@ by (REPEAT (eresolve_tac [exE, conjE] 1)); by (eres_inst_tac [("x","A Un y")] allE 1); by (ftac infinite_Un 1 THEN (mp_tac 1)); -by (etac zero_lt_natE 1); by (assume_tac 1); +by (etac zero_lt_natE 1); +by (assume_tac 1); by (Clarify_tac 1); by (DEPTH_SOLVE (ares_tac [export conclusion] 1)); qed "AC16_WO4"; diff -r b43ad07660b9 -r a71686059be0 src/ZF/AC/AC_Equiv.ML --- a/src/ZF/AC/AC_Equiv.ML Thu Jan 13 17:30:23 2000 +0100 +++ b/src/ZF/AC/AC_Equiv.ML Thu Jan 13 17:31:30 2000 +0100 @@ -4,9 +4,6 @@ *) - -open AC_Equiv; - val WO_defs = [WO1_def, WO2_def, WO3_def, WO4_def, WO5_def, WO6_def, WO8_def]; val AC_defs = [AC0_def, AC1_def, AC2_def, AC3_def, AC4_def, AC5_def, @@ -99,10 +96,6 @@ addSIs [major RS CollectD1 RS Pi_type, major RS CollectD2]) 1); qed "inj_strengthen_type"; -Goalw [Finite_def] "n:nat ==> Finite(n)"; -by (fast_tac (claset() addSIs [eqpoll_refl]) 1); -qed "nat_into_Finite"; - Goalw [Finite_def] "~Finite(nat)"; by (fast_tac (claset() addSDs [eqpoll_imp_lepoll] addIs [Ord_nat RSN (2, ltI) RS lt_not_lepoll RS notE]) 1); diff -r b43ad07660b9 -r a71686059be0 src/ZF/AC/AC_Equiv.thy --- a/src/ZF/AC/AC_Equiv.thy Thu Jan 13 17:30:23 2000 +0100 +++ b/src/ZF/AC/AC_Equiv.thy Thu Jan 13 17:31:30 2000 +0100 @@ -12,7 +12,10 @@ but slightly changed. *) -AC_Equiv = CardinalArith + Univ + + +AC_Equiv = CardinalArith + Univ + + (*NOT "Main" because that theory includes AC!!!*) + consts diff -r b43ad07660b9 -r a71686059be0 src/ZF/AC/Cardinal_aux.ML --- a/src/ZF/AC/Cardinal_aux.ML Thu Jan 13 17:30:23 2000 +0100 +++ b/src/ZF/AC/Cardinal_aux.ML Thu Jan 13 17:31:30 2000 +0100 @@ -11,17 +11,16 @@ (* ********************************************************************** *) (* j=|A| *) -goal Cardinal.thy - "!!A. [| A lepoll i; Ord(i) |] ==> EX j. j le i & A eqpoll j"; -by (fast_tac (claset() addIs [lepoll_cardinal_le, well_ord_Memrel, - well_ord_cardinal_eqpoll RS eqpoll_sym] - addDs [lepoll_well_ord]) 1); +Goal "[| A lepoll i; Ord(i) |] ==> EX j. j le i & A eqpoll j"; +by (blast_tac (claset() addSIs [lepoll_cardinal_le, well_ord_Memrel, + well_ord_cardinal_eqpoll RS eqpoll_sym] + addDs [lepoll_well_ord]) 1); qed "lepoll_imp_ex_le_eqpoll"; (* j=|A| *) -goalw Cardinal.thy [lesspoll_def] - "!!A a. [| A lesspoll i; Ord(i) |] ==> EX j. j EX j. j InfCard(|i|)"; @@ -161,7 +160,7 @@ qed "UN_eq_UN_Diffs"; Goalw [lepoll_def, eqpoll_def] - "a lepoll X ==> EX Y. Y<=X & a eqpoll Y"; + "a lepoll X ==> EX Y. Y<=X & a eqpoll Y"; by (etac exE 1); by (forward_tac [subset_refl RSN (2, restrict_bij)] 1); by (res_inst_tac [("x","f``a")] exI 1); @@ -176,9 +175,9 @@ \ A-B lesspoll a |] ==> P"; by (REPEAT (eresolve_tac [lesspoll_imp_ex_lt_eqpoll RS exE, Card_is_Ord, conjE] 1)); -by (forw_inst_tac [("j","xa")] (lt_Ord RS (lt_Ord RSN (2, Un_upper1_le))) 1 +by (forw_inst_tac [("j","xa")] ([lt_Ord, lt_Ord] MRS Un_upper1_le) 1 THEN (assume_tac 1)); -by (forw_inst_tac [("j","xa")] (lt_Ord RS (lt_Ord RSN (2, Un_upper2_le))) 1 +by (forw_inst_tac [("j","xa")] ([lt_Ord, lt_Ord] MRS Un_upper2_le) 1 THEN (assume_tac 1)); by (dtac Un_least_lt 1 THEN (assume_tac 1)); by (dresolve_tac [le_imp_lepoll RSN diff -r b43ad07660b9 -r a71686059be0 src/ZF/AC/DC.ML --- a/src/ZF/AC/DC.ML Thu Jan 13 17:30:23 2000 +0100 +++ b/src/ZF/AC/DC.ML Thu Jan 13 17:31:30 2000 +0100 @@ -200,8 +200,7 @@ Goalw [lesspoll_def, Finite_def] "A lesspoll nat ==> Finite(A)"; -by (fast_tac (claset() addSDs [ltD, lepoll_imp_ex_le_eqpoll] - addSIs [Ord_nat]) 1); +by (fast_tac (claset() addSDs [ltD, lepoll_imp_ex_le_eqpoll]) 1); qed "lesspoll_nat_is_Finite"; Goal "n:nat ==> ALL A. (A eqpoll n & A <= X) --> A : Fin(X)"; diff -r b43ad07660b9 -r a71686059be0 src/ZF/AC/DC_lemmas.ML --- a/src/ZF/AC/DC_lemmas.ML Thu Jan 13 17:30:23 2000 +0100 +++ b/src/ZF/AC/DC_lemmas.ML Thu Jan 13 17:31:30 2000 +0100 @@ -85,9 +85,7 @@ Goal "[| Ord(k); i:k |] ==> succ(i) : succ(k)"; by (resolve_tac [Ord_linear RS disjE] 1 THEN (assume_tac 3)); -by (REPEAT (fast_tac (claset() addSIs [Ord_succ] - addEs [Ord_in_Ord, mem_irrefl, mem_asym] - addSDs [succ_inject]) 1)); +by (REPEAT (fast_tac (claset() addEs [Ord_in_Ord, mem_irrefl, mem_asym]) 1)); qed "succ_in_succ"; Goalw [restrict_def] diff -r b43ad07660b9 -r a71686059be0 src/ZF/AC/WO2_AC16.ML --- a/src/ZF/AC/WO2_AC16.ML Thu Jan 13 17:30:23 2000 +0100 +++ b/src/ZF/AC/WO2_AC16.ML Thu Jan 13 17:31:30 2000 +0100 @@ -38,8 +38,8 @@ \ ALL i j. i le j --> F(i) <= F(j); i V = W"; -by (res_inst_tac [("j","j")] (lt_Ord RS (lt_Ord RSN (2, Ord_linear_le))) 1 - THEN (REPEAT (assume_tac 1))); +by (res_inst_tac [("j","j")] ([lt_Ord, lt_Ord] MRS Ord_linear_le) 1 + THEN (REPEAT (assume_tac 1))); by (eresolve_tac [lemma3_1 RS sym] 1 THEN (REPEAT (assume_tac 1))); by (etac lemma3_1 1 THEN (REPEAT (assume_tac 1))); val lemma3 = result(); @@ -118,7 +118,7 @@ Goalw [lesspoll_def] - "!!X. [| Finite(X); ~Finite(a); Ord(a) |] ==> X lesspoll a"; + "[| Finite(X); ~Finite(a); Ord(a) |] ==> X lesspoll a"; by (rtac conjI 1); by (dresolve_tac [nat_le_infinite_Ord RS le_imp_lepoll] 1 THEN (assume_tac 1)); @@ -129,48 +129,13 @@ subset_imp_lepoll RSN (2, eqpoll_imp_lepoll RS lepoll_trans)]) 1); qed "Finite_lesspoll_infinite_Ord"; - -Goal "x:X ==> Union(X) = Union(X-{x}) Un x"; -by (Fast_tac 1); -qed "Union_eq_Un_Diff"; - - -Goal "n:nat ==> ALL X. X eqpoll n --> (ALL x:X. Finite(x)) \ -\ --> Finite(Union(X))"; -by (induct_tac "n" 1); -by (fast_tac (claset() addSDs [eqpoll_imp_lepoll RS lepoll_0_is_0] - addSIs [nat_0I RS nat_into_Finite] addss (simpset())) 1); -by (REPEAT (resolve_tac [allI, impI] 1)); -by (resolve_tac [eqpoll_succ_imp_not_empty RS not_emptyE] 1 THEN (assume_tac 1)); -by (res_inst_tac [("P","%z. Finite(z)")] (Union_eq_Un_Diff RS ssubst) 1 - THEN (assume_tac 1)); -by (rtac Finite_Un 1); -by (Fast_tac 2); -by (fast_tac (claset() addSIs [Diff_sing_eqpoll]) 1); -qed "Finite_Union_lemma"; - - -Goal "[| ALL x:X. Finite(x); Finite(X) |] ==> Finite(Union(X))"; -by (eresolve_tac [Finite_def RS def_imp_iff RS iffD1 RS bexE] 1); -by (dtac Finite_Union_lemma 1); -by (Fast_tac 1); -qed "Finite_Union"; - - -Goalw [Finite_def] "[| x lepoll n; n:nat |] ==> Finite(x)"; -by (fast_tac (claset() - addEs [nat_into_Ord RSN (2, lepoll_imp_ex_le_eqpoll) RS exE, - Ord_nat RSN (2, ltI) RSN (2, lt_trans1) RS ltD]) 1); -qed "lepoll_nat_num_imp_Finite"; - - Goal "[| ALL x:X. x lepoll n & x <= T; well_ord(T, R); X lepoll b; \ \ b Union(X) lesspoll a"; by (excluded_middle_tac "Finite(X)" 1); by (resolve_tac [Card_is_Ord RSN (3, Finite_lesspoll_infinite_Ord)] 2 THEN (REPEAT (assume_tac 3))); -by (fast_tac (claset() addSEs [lepoll_nat_num_imp_Finite] +by (fast_tac (claset() addSEs [lepoll_nat_imp_Finite] addSIs [Finite_Union]) 2); by (dresolve_tac [lt_Ord RSN (2, lepoll_imp_ex_le_eqpoll)] 1 THEN (assume_tac 1)); by (REPEAT (eresolve_tac [exE, conjE] 1)); @@ -311,8 +276,9 @@ by (rtac dbl_Diff_eqpoll_Card 1 THEN (TRYALL assume_tac)); by (rtac Union_recfunAC16_lesspoll 1 THEN (REPEAT (assume_tac 1))); by (eresolve_tac [add_type RS nat_succI] 1 THEN (assume_tac 1)); -by (resolve_tac [nat_succI RSN (2, bexI RS (Finite_def RS def_imp_iff RS - iffD2)) RS (Card_is_Ord RSN (3, Finite_lesspoll_infinite_Ord))] 1 +by (resolve_tac [nat_succI RSN + (2, bexI RS (Finite_def RS def_imp_iff RS iffD2)) RS + (Card_is_Ord RSN (3, Finite_lesspoll_infinite_Ord))] 1 THEN (TRYALL assume_tac)); by (eresolve_tac [ltD RSN (2, bij_is_fun RS apply_type) RS CollectE] 1 THEN (TRYALL assume_tac)); @@ -320,17 +286,16 @@ (* back to the proof *) -val disj_Un_eqpoll_nat_sum = disj_Un_eqpoll_sum RS ( - sum_eqpoll_cong RSN (2, - nat_sum_eqpoll_sum RSN (3, - eqpoll_trans RS eqpoll_trans))) |> standard; +val disj_Un_eqpoll_nat_sum = + [disj_Un_eqpoll_sum, sum_eqpoll_cong, nat_sum_eqpoll_sum] MRS + (eqpoll_trans RS eqpoll_trans) |> standard; Goal "[| x : Pow(A - B - fa`i); x eqpoll m; \ \ fa : bij(a, {x: Pow(A) . x eqpoll k}); i fa ` i Un x : {x: Pow(A) . x eqpoll k #+ m}"; by (rtac CollectI 1); -by (fast_tac (claset() addSIs [PowD RS (PowD RSN (2, Un_least RS PowI))] +by (fast_tac (claset() addSEs [ltD RSN (2, bij_is_fun RS apply_type RS CollectE)]) 1); by (rtac disj_Un_eqpoll_nat_sum 1 THEN (TRYALL assume_tac)); diff -r b43ad07660b9 -r a71686059be0 src/ZF/AC/WO6_WO1.ML --- a/src/ZF/AC/WO6_WO1.ML Thu Jan 13 17:30:23 2000 +0100 +++ b/src/ZF/AC/WO6_WO1.ML Thu Jan 13 17:31:30 2000 +0100 @@ -57,10 +57,10 @@ (* Two cases for lemma ii *) (* ********************************************************************** *) Goalw [lesspoll_def] - "!! a f u. ALL b \ -\ (ALL b (EX g \ + "ALL b (ALL b \ +\ (EX g \ \ u(f,b,g,d) eqpoll m))"; by (Asm_simp_tac 1); by (blast_tac (claset() delrules [equalityI]) 1);