# HG changeset patch # User lcp # Date 806772923 -7200 # Node ID d4551b1a6da750da3d7aac176588381c376563e2 # Parent c8e58352b1a5ebcb2aeb5210b2c1fd791bc199a7 Many small changes to make proofs run faster diff -r c8e58352b1a5 -r d4551b1a6da7 src/ZF/AC/AC10_AC15.ML --- a/src/ZF/AC/AC10_AC15.ML Wed Jul 26 16:23:42 1995 +0200 +++ b/src/ZF/AC/AC10_AC15.ML Wed Jul 26 17:35:23 1995 +0200 @@ -110,9 +110,9 @@ \ sets_of_size_between(f`B, 2, succ(n)) & \ \ Union(f`B)=B; n:nat |] \ \ ==> EX f. ALL B:A. f`B ~= 0 & f`B <= B & f`B lepoll n"; -by (fast_tac (empty_cs addSDs [lemma3, bspec, theI] +by (fast_tac (empty_cs addSDs [lemma3, theI] addDs [bspec] addSEs [exE, conjE] - addSIs [exI, ballI, lemma5]) 1); + addIs [exI, ballI, lemma5]) 1); val ex_fun_AC13_AC15 = result(); (* ********************************************************************** *) @@ -170,7 +170,7 @@ by (safe_tac ZF_cs); by (fast_tac (empty_cs addSEs [allE, cons_times_nat_not_Finite RSN (2, impE), ex_fun_AC13_AC15]) 1); -val AC10_imp_AC13 = result(); +qed "AC10_AC13"; (* ********************************************************************** *) (* The proofs needed in the second case, not in the first *) @@ -246,12 +246,12 @@ goalw thy AC_defs "!!Z. AC13(1) ==> AC1"; by (fast_tac (AC_cs addSEs [lemma]) 1); -qed "AC13(1)_AC1"; +qed "AC13_AC1"; (* ********************************************************************** *) (* AC11 ==> AC14 *) (* ********************************************************************** *) goalw thy [AC11_def, AC14_def] "!!Z. AC11 ==> AC14"; -by (fast_tac (ZF_cs addSIs [AC10_imp_AC13]) 1); +by (fast_tac (ZF_cs addSIs [AC10_AC13]) 1); qed "AC11_AC14"; diff -r c8e58352b1a5 -r d4551b1a6da7 src/ZF/AC/AC16_WO4.ML --- a/src/ZF/AC/AC16_WO4.ML Wed Jul 26 16:23:42 1995 +0200 +++ b/src/ZF/AC/AC16_WO4.ML Wed Jul 26 17:35:23 1995 +0200 @@ -1,3 +1,9 @@ +(* Title: ZF/AC/AC16_WO4.ML + ID: $Id$ + Author: Krzysztof Gr`abczewski + + The proof of AC16(n, k) ==> WO4(n-k) +*) open AC16_WO4; @@ -447,7 +453,7 @@ goal thy "!!n. n:nat ==> {z:Pow(y). z lepoll succ(n)} = \ \ {z:Pow(y). z lepoll n} Un {z:Pow(y). z eqpoll succ(n)}"; -by (fast_tac (ZF_cs addSIs [le_refl, leI, +by (fast_tac (ZF_cs addIs [le_refl, leI, le_imp_lepoll, equalityI] addSDs [lepoll_succ_disj] addSEs [nat_into_Ord, lepoll_trans, eqpoll_imp_lepoll]) 1); diff -r c8e58352b1a5 -r d4551b1a6da7 src/ZF/AC/AC_Equiv.ML --- a/src/ZF/AC/AC_Equiv.ML Wed Jul 26 16:23:42 1995 +0200 +++ b/src/ZF/AC/AC_Equiv.ML Wed Jul 26 17:35:23 1995 +0200 @@ -21,6 +21,8 @@ (* ******************************************** *) +val nat_implies_well_ord = nat_into_Ord RS well_ord_Memrel; + (* Theorems analogous to ones presented in "ZF/Ordinal.ML" *) (* lemma for nat_le_imp_lepoll *) diff -r c8e58352b1a5 -r d4551b1a6da7 src/ZF/AC/Cardinal_aux.ML --- a/src/ZF/AC/Cardinal_aux.ML Wed Jul 26 16:23:42 1995 +0200 +++ b/src/ZF/AC/Cardinal_aux.ML Wed Jul 26 17:35:23 1995 +0200 @@ -94,14 +94,14 @@ by (fast_tac (AC_cs addSEs [left_inverse]) 1); val Un_lepoll_Un = result(); -goal thy "{x, y} - {y} = {x} - {y}"; +goal ZF.thy "{x, y} - {y} = {x} - {y}"; by (fast_tac eq_cs 1); val double_Diff_sing = result(); -goal thy "if({y,z}-{z}=0, z, THE w. {y,z}-{z}={w}) = y"; +goal ZF.thy "if({y,z}-{z}=0, z, THE w. {y,z}-{z}={w}) = y"; by (split_tac [expand_if] 1); -by (asm_full_simp_tac (AC_ss addsimps [double_Diff_sing, Diff_eq_0_iff]) 1); -by (fast_tac (AC_cs addSIs [the_equality, equalityI, equals0I] +by (asm_full_simp_tac (ZF_ss addsimps [double_Diff_sing, Diff_eq_0_iff]) 1); +by (fast_tac (ZF_cs addSIs [the_equality, equalityI, equals0I] addEs [equalityE] addSEs [singletonE]) 1); val paired_bij_lemma = result(); @@ -236,8 +236,8 @@ goal thy "!!m n. [| m:nat; n:nat |] ==> m + n eqpoll m #+ n"; by (resolve_tac [eqpoll_trans] 1); -by (eresolve_tac [nat_into_Ord RS well_ord_Memrel RS ( - nat_into_Ord RS well_ord_Memrel RSN (2, +by (eresolve_tac [nat_implies_well_ord RS ( + nat_implies_well_ord RSN (2, well_ord_radd RS well_ord_cardinal_eqpoll)) RS eqpoll_sym] 1 THEN (assume_tac 1)); by (eresolve_tac [nat_cadd_eq_add RS subst] 1 THEN (assume_tac 1)); diff -r c8e58352b1a5 -r d4551b1a6da7 src/ZF/AC/Cardinal_aux.thy --- a/src/ZF/AC/Cardinal_aux.thy Wed Jul 26 16:23:42 1995 +0200 +++ b/src/ZF/AC/Cardinal_aux.thy Wed Jul 26 17:35:23 1995 +0200 @@ -1,3 +1,3 @@ (*Dummy theory to document dependencies *) -Cardinal_aux = Cardinal + OrderType + CardinalArith + first \ No newline at end of file +Cardinal_aux = AC_Equiv + first diff -r c8e58352b1a5 -r d4551b1a6da7 src/ZF/AC/DC.ML --- a/src/ZF/AC/DC.ML Wed Jul 26 16:23:42 1995 +0200 +++ b/src/ZF/AC/DC.ML Wed Jul 26 17:35:23 1995 +0200 @@ -192,7 +192,7 @@ by (fast_tac (AC_cs addSEs [nat_succI]) 1); by (dresolve_tac [nat_succI RSN (4, lemma2)] 1 THEN REPEAT (assume_tac 1)); -by (fast_tac (AC_cs addSEs [image_fun RS sym, +by (fast_tac (AC_cs addSEs [conjE, image_fun RS sym, nat_into_Ord RSN (2, OrdmemD)]) 1); val lemma3 = result(); @@ -400,21 +400,16 @@ by (dresolve_tac [ltD] 1); by (eresolve_tac [nat_induct] 1); by (dresolve_tac [[nat_0I, Ord_nat] MRS ltI RSN (2, ospec)] 1); -by (REPEAT (eresolve_tac [CollectE, conjE, disjE] 1)); -by (asm_full_simp_tac (AC_ss - addsimps [image_0, singleton_fun RS domain_of_fun, - [lepoll_refl, succI1] MRS lepoll_1_is_sing]) 1); -by (asm_full_simp_tac (AC_ss - addsimps [image_0, singleton_fun RS domain_of_fun, - [lepoll_refl, succI1] MRS lepoll_1_is_sing, singleton_in_funs]) 1); +by (fast_tac (FOL_cs addss + (ZF_ss addsimps [image_0, singleton_fun RS domain_of_fun, + [lepoll_refl, succI1] MRS lepoll_1_is_sing, singleton_in_funs])) 1); by (dresolve_tac [[nat_succI, Ord_nat] MRS ltI RSN (2, ospec)] 1 THEN (assume_tac 1)); by (REPEAT (eresolve_tac [conjE, CollectE, disjE] 1)); -by (fast_tac (AC_cs addSEs [trans, subst_context] +by (fast_tac (FOL_cs addSEs [trans, subst_context] addSIs [UN_image_succ_eq_succ] addss AC_ss) 1); by (eresolve_tac [conjE] 1); by (eresolve_tac [notE] 1); -by (hyp_subst_tac 1); by (asm_full_simp_tac (AC_ss addsimps [UN_image_succ_eq_succ]) 1); by (eresolve_tac [conjE] 1); by (dresolve_tac [apply_UN_type] 1 THEN REPEAT (assume_tac 1)); @@ -428,7 +423,8 @@ by (resolve_tac [UN_I] 1); by (eresolve_tac [nat_succI] 1); by (resolve_tac [CollectI] 1); -by (fast_tac (AC_cs addSEs [cons_fun_type2]) 1); +by (eresolve_tac [rangeI RSN (2, subsetD) RSN (2, cons_fun_type2)] 1 + THEN REPEAT (assume_tac 1)); by (resolve_tac [ballI] 1); by (eresolve_tac [succE] 1); by (asm_full_simp_tac (AC_ss addsimps [cons_val_n, cons_val_k]) 1); @@ -455,8 +451,8 @@ by (resolve_tac [conjI] 1); by (fast_tac (AC_cs addSEs [trans RS domain_eq_imp_fun_type, subst_context]) 1); -by (fast_tac (AC_cs addSEs [nat_succI, succI2, f_n_pairs_in_R RS bspec, - subst_context, trans]) 1); +by (fast_tac (FOL_cs + addSEs [conjE, f_n_pairs_in_R, trans, subst_context]) 1); val lemma2 = result(); goal thy "!!n. [| XX = (UN n:nat. \ @@ -576,8 +572,8 @@ goal thy "!!Z. [| ALL Y:Pow(X). Y lesspoll a --> (EX x:X. : R); \ \ b:a; Z:Pow(X); Z lesspoll a |] \ \ ==> {x:X. : R} ~= 0"; -by (dresolve_tac [bspec] 1 THEN (assume_tac 1)); -by (fast_tac (AC_cs addSIs [not_emptyI]) 1); +by (fast_tac (FOL_cs addEs [bexE, equals0D] + addSDs [bspec] addIs [CollectI]) 1); val lemma_ = result(); goal thy "!!K. [| Card(K); well_ord(X,Q); \ diff -r c8e58352b1a5 -r d4551b1a6da7 src/ZF/AC/HH.ML --- a/src/ZF/AC/HH.ML Wed Jul 26 16:23:42 1995 +0200 +++ b/src/ZF/AC/HH.ML Wed Jul 26 17:35:23 1995 +0200 @@ -18,13 +18,13 @@ \ (let z = x - (UN b:a. HH(f,x,b)) \ \ in if(f`z:Pow(z)-{0}, f`z, {x}))"; by (resolve_tac [HH_def RS def_transrec RS trans] 1); -by (asm_full_simp_tac ZF_ss 1); +by (simp_tac ZF_ss 1); val HH_def_satisfies_eq = result(); goal thy "HH(f,x,a) : Pow(x)-{0} | HH(f,x,a)={x}"; by (resolve_tac [HH_def_satisfies_eq RS ssubst] 1); -by (asm_full_simp_tac (ZF_ss addsimps [Let_def, Diff_subset RS PowI]) 1); -by (split_tac [expand_if] 1); +by (simp_tac (ZF_ss addsimps [Let_def, Diff_subset RS PowI] + setloop split_tac [expand_if]) 1); by (fast_tac ZF_cs 1); val HH_values = result(); @@ -78,8 +78,8 @@ by (resolve_tac [HH_def_satisfies_eq RS ssubst] 1); by (asm_full_simp_tac (AC_ss addsimps [Let_def, Diff_subset RS PowI]) 1); by (dresolve_tac [expand_if RS iffD1] 1); -by (split_tac [expand_if] 1); -by (fast_tac (AC_cs addSEs [mem_irrefl]) 1); +by (simp_tac (ZF_ss setloop split_tac [expand_if] ) 1); +by (fast_tac (subset_cs addSEs [mem_irrefl]) 1); val HH_subset_x_imp_subset_Diff_UN = result(); goal thy "!!x. [| HH(f,x,v)=HH(f,x,w); HH(f,x,v): Pow(x)-{0}; v:w |] ==> P"; @@ -190,12 +190,12 @@ goal thy "HH(f,x,i)=f`(x - (UN j:i. HH(f,x,j))) | HH(f,x,i)={x}"; by (resolve_tac [HH_def_satisfies_eq RS ssubst] 1); -by (asm_full_simp_tac (ZF_ss addsimps [Let_def, Diff_subset RS PowI]) 1); -by (split_tac [expand_if] 1); -by (fast_tac ZF_cs 1); +by (simp_tac (ZF_ss addsimps [Let_def, Diff_subset RS PowI] + setloop split_tac [expand_if]) 1); val HH_values2 = result(); -goal thy "!!f. HH(f,x,i): Pow(x)-{0} ==> HH(f,x,i)=f`(x - (UN j:i. HH(f,x,j)))"; +goal thy + "!!f. HH(f,x,i): Pow(x)-{0} ==> HH(f,x,i)=f`(x - (UN j:i. HH(f,x,j)))"; by (resolve_tac [HH_values2 RS disjE] 1 THEN (assume_tac 1)); by (fast_tac (AC_cs addSEs [equalityE, mem_irrefl] addSDs [singleton_subsetD]) 1); diff -r c8e58352b1a5 -r d4551b1a6da7 src/ZF/AC/Hartog.ML --- a/src/ZF/AC/Hartog.ML Wed Jul 26 16:23:42 1995 +0200 +++ b/src/ZF/AC/Hartog.ML Wed Jul 26 17:35:23 1995 +0200 @@ -9,7 +9,7 @@ goal thy "!!X. ALL a. Ord(a) --> a:X ==> P"; by (res_inst_tac [("X1","{y:X. Ord(y)}")] (ON_class RS revcut_rl) 1); -by (fast_tac AC_cs 1); +by (fast_tac ZF_cs 1); val Ords_in_set = result(); goalw thy [lepoll_def] "!!X. [| Ord(a); a lepoll X |] ==> \ @@ -31,10 +31,10 @@ goal thy "!!X. [| Ord(a); a lepoll X |] ==> \ \ EX Y. Y<=X & (EX R. R<=X*X & ordertype(Y,R)=a)"; by (dresolve_tac [Ord_lepoll_imp_ex_well_ord] 1 THEN (assume_tac 1)); -by (step_tac AC_cs 1); +by (step_tac ZF_cs 1); by (REPEAT (ares_tac [exI, conjI] 1)); by (eresolve_tac [ordertype_Int] 2); -by (fast_tac AC_cs 1); +by (fast_tac ZF_cs 1); val Ord_lepoll_imp_eq_ordertype = result(); goal thy "!!X. ALL a. Ord(a) --> a lepoll X ==> \ @@ -44,7 +44,7 @@ by (REPEAT (eresolve_tac [allE, impE] 1)); by (assume_tac 1); by (dresolve_tac [Ord_lepoll_imp_eq_ordertype] 1 THEN (assume_tac 1)); -by (fast_tac (AC_cs addSIs [ReplaceI] addEs [sym]) 1); +by (fast_tac (ZF_cs addSIs [ReplaceI] addEs [sym]) 1); val Ords_lepoll_set_lemma = result(); goal thy "!!X. ALL a. Ord(a) --> a lepoll X ==> P"; @@ -53,15 +53,15 @@ goal thy "EX a. Ord(a) & ~a lepoll X"; by (resolve_tac [swap] 1); -by (fast_tac AC_cs 1); +by (fast_tac ZF_cs 1); by (resolve_tac [Ords_lepoll_set] 1); -by (fast_tac AC_cs 1); +by (fast_tac ZF_cs 1); val ex_Ord_not_lepoll = result(); goalw thy [Hartog_def] "~ Hartog(A) lepoll A"; by (resolve_tac [ex_Ord_not_lepoll RS exE] 1); by (resolve_tac [LeastI] 1); -by (REPEAT (fast_tac AC_cs 1)); +by (REPEAT (fast_tac ZF_cs 1)); val HartogI = result(); val HartogE = HartogI RS notE; @@ -71,14 +71,14 @@ val Ord_Hartog = result(); goalw thy [Hartog_def] "!!i. [| i < Hartog(A); ~ i lepoll A |] ==> P"; -by (fast_tac (AC_cs addEs [less_LeastE]) 1); +by (fast_tac (ZF_cs addEs [less_LeastE]) 1); val less_HartogE1 = result(); goal thy "!!i. [| i < Hartog(A); i eqpoll Hartog(A) |] ==> P"; -by (fast_tac (AC_cs addEs [less_HartogE1, eqpoll_sym RS eqpoll_imp_lepoll +by (fast_tac (ZF_cs addEs [less_HartogE1, eqpoll_sym RS eqpoll_imp_lepoll RS lepoll_trans RS HartogE]) 1); val less_HartogE = result(); goal thy "Card(Hartog(A))"; -by (fast_tac (AC_cs addSIs [CardI, Ord_Hartog] addEs [less_HartogE]) 1); +by (fast_tac (ZF_cs addSIs [CardI, Ord_Hartog] addEs [less_HartogE]) 1); val Card_Hartog = result(); diff -r c8e58352b1a5 -r d4551b1a6da7 src/ZF/AC/WO1_WO7.ML --- a/src/ZF/AC/WO1_WO7.ML Wed Jul 26 16:23:42 1995 +0200 +++ b/src/ZF/AC/WO1_WO7.ML Wed Jul 26 17:35:23 1995 +0200 @@ -26,8 +26,8 @@ by (excluded_middle_tac "Finite(A)" 1); by (fast_tac AC_cs 1); by (rewrite_goals_tac [Finite_def, eqpoll_def]); -by (fast_tac (AC_cs addSIs [nat_into_Ord RS well_ord_Memrel RSN (2, - bij_is_inj RS well_ord_rvimage)]) 1); +by (fast_tac (ZF_cs addSIs [[bij_is_inj, nat_implies_well_ord] MRS + well_ord_rvimage]) 1); val LEMMA_imp_WO1 = result(); (* ********************************************************************** *) diff -r c8e58352b1a5 -r d4551b1a6da7 src/ZF/AC/WO2_AC16.ML --- a/src/ZF/AC/WO2_AC16.ML Wed Jul 26 16:23:42 1995 +0200 +++ b/src/ZF/AC/WO2_AC16.ML Wed Jul 26 17:35:23 1995 +0200 @@ -531,7 +531,7 @@ (* ********************************************************************** *) (* Lemma to simplify the inductive proof *) -(* - the disired property is a consequence of the inductive assumption *) +(* - the desired property is a consequence of the inductive assumption *) (* ********************************************************************** *) val [prem1, prem2, prem3, prem4] = goal thy @@ -561,7 +561,7 @@ by (REPEAT (eresolve_tac [conjE, OUN_E] 1)); by (eresolve_tac [lt_Ord RSN (2, lt_Ord RS Ord_linear_le)] 1 THEN (assume_tac 1)); by (dresolve_tac [prem4 RS subsetD] 2 THEN (assume_tac 2)); -by (fast_tac AC_cs 2); +by (fast_tac FOL_cs 2); by (forward_tac [prem1] 1); by (forward_tac [succ_leE] 1); by (dresolve_tac [prem4 RS subsetD] 1 THEN (assume_tac 1)); @@ -569,7 +569,7 @@ by (dresolve_tac [lt_trans RSN (2, ospec)] 1 THEN (TRYALL assume_tac)); by (dresolve_tac [disjI1 RSN (2, mp)] 1 THEN (assume_tac 1)); by (eresolve_tac [ex1_two_eq] 1); -by (REPEAT (fast_tac AC_cs 1)); +by (REPEAT (fast_tac FOL_cs 1)); val lemma_simp_induct = result(); (* ********************************************************************** *) diff -r c8e58352b1a5 -r d4551b1a6da7 src/ZF/AC/first.thy --- a/src/ZF/AC/first.thy Wed Jul 26 16:23:42 1995 +0200 +++ b/src/ZF/AC/first.thy Wed Jul 26 17:35:23 1995 +0200 @@ -15,5 +15,4 @@ first_def "first(u, X, R) == u:X & (ALL v:X. v~=u --> : R)" - -end \ No newline at end of file +end