--- 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";
--- 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);
--- 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 *)
--- 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));
--- 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
--- 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. <Y, x> : R); \
\ b:a; Z:Pow(X); Z lesspoll a |] \
\ ==> {x:X. <Z,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); \
--- 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);
--- 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();
--- 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();
(* ********************************************************************** *)
--- 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();
(* ********************************************************************** *)
--- 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 --> <u,v> : R)"
-
-end
\ No newline at end of file
+end