--- a/src/ZF/AC.ML Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/AC.ML Wed Jan 08 15:04:27 1997 +0100
@@ -14,7 +14,7 @@
by (excluded_middle_tac "A=0" 1);
by (asm_simp_tac (!simpset addsimps [Pi_empty1]) 2 THEN Fast_tac 2);
(*The non-trivial case*)
-by (fast_tac (eq_cs addIs [AC, nonempty]) 1);
+by (fast_tac (!claset addIs [AC, nonempty]) 1);
qed "AC_Pi";
(*Using dtac, this has the advantage of DELETING the universal quantifier*)
@@ -27,7 +27,7 @@
goal AC.thy "EX f. f: (PROD X: Pow(C)-{0}. X)";
by (res_inst_tac [("B1", "%x.x")] (AC_Pi RS exE) 1);
by (etac exI 2);
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "AC_Pi_Pow";
val [nonempty] = goal AC.thy
@@ -40,7 +40,7 @@
goal ZF.thy "!!x A. [| 0 ~: A; x: A |] ==> EX y. y:x";
by (subgoal_tac "x ~= 0" 1);
-by (ALLGOALS (fast_tac eq_cs));
+by (ALLGOALS (Fast_tac));
qed "non_empty_family";
goal AC.thy "!!A. 0 ~: A ==> EX f: A->Union(A). ALL x:A. f`x : x";
--- a/src/ZF/AC/Cardinal_aux.ML Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/AC/Cardinal_aux.ML Wed Jan 08 15:04:27 1997 +0100
@@ -69,7 +69,7 @@
setloop (split_tac [expand_if] ORELSE' etac UnE);
goal upair.thy "{x, y} - {y} = {x} - {y}";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
val double_Diff_sing = result();
goal upair.thy "if({y,z}-{z}=0, z, THE w. {y,z}-{z}={w}) = y";
--- a/src/ZF/AC/DC.ML Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/AC/DC.ML Wed Jan 08 15:04:27 1997 +0100
@@ -51,7 +51,7 @@
by (rtac CollectI 1);
by (rtac SigmaI 1);
by (fast_tac (!claset addSIs [nat_0I RS UN_I, empty_fun]) 1);
-br (nat_1I RS UN_I) 1;
+by (rtac (nat_1I RS UN_I) 1);
by (fast_tac (!claset addSIs [singleton_fun RS Pi_type]
addss (!simpset addsimps [singleton_0 RS sym])) 1);
by (asm_full_simp_tac (!simpset addsimps [domain_0, domain_cons,
@@ -115,9 +115,9 @@
by (Step_tac 1);
by (rtac bexI 1 THEN (assume_tac 2));
by (best_tac (!claset addIs [ltD]
- addSEs [nat_0_le RS leE]
+ addSEs [nat_0_le RS leE]
addEs [sym RS trans RS succ_neq_0, domain_of_fun]
- addss (!simpset)) 1);
+ addss (!simpset)) 1);
(** LEVEL 7 **)
by (dresolve_tac [nat_succI RSN (2, bspec)] 1 THEN (assume_tac 1));
by (subgoal_tac "f ` succ(succ(x)) : succ(k)->X" 1);
@@ -276,7 +276,7 @@
goal thy "!!x. x: X \
\ ==> {<0,x>}: (UN n:nat. {f:succ(n)->X. ALL k:n. <f`k, f`succ(k)> : R})";
-br (nat_0I RS UN_I) 1;
+by (rtac (nat_0I RS UN_I) 1);
by (fast_tac (!claset addSIs [singleton_fun RS Pi_type]
addss (!simpset addsimps [singleton_0 RS sym])) 1);
val singleton_in_funs = result();
@@ -303,7 +303,7 @@
by (step_tac (!claset delrules [domainE]) 1);
by (swap_res_tac [bexI] 1 THEN etac singleton_in_funs 2);
by (asm_full_simp_tac (!simpset addsimps [nat_0I RSN (2, bexI),
- cons_fun_type2, empty_fun]) 1);
+ cons_fun_type2, empty_fun]) 1);
val lemma1 = result();
goal thy "!!f. [| f:nat->X; n:nat |] ==> \
@@ -392,8 +392,8 @@
by (etac nat_induct 1);
by (dresolve_tac [[nat_0I, Ord_nat] MRS ltI RSN (2, ospec)] 1);
by (fast_tac (FOL_cs addss
- (!simpset addsimps [image_0, singleton_fun RS domain_of_fun,
- singleton_0, singleton_in_funs])) 1);
+ (!simpset addsimps [image_0, singleton_fun RS domain_of_fun,
+ singleton_0, singleton_in_funs])) 1);
(*induction step*) (** LEVEL 5 **)
by (Full_simp_tac 1);
by (dresolve_tac [[nat_succI, Ord_nat] MRS ltI RSN (2, ospec)] 1
@@ -411,10 +411,10 @@
by (etac domainE 1);
by (forward_tac [f_n_type] 1 THEN REPEAT (assume_tac 1));
-br bexI 1;
+by (rtac bexI 1);
by (etac nat_succI 2);
by (res_inst_tac [("x","cons(<succ(xa), ya>, f`xa)")] bexI 1);
-br conjI 1;
+by (rtac conjI 1);
by (fast_tac (FOL_cs
addEs [subst_context RSN (2, trans) RS domain_cons_eq_succ,
subst_context, all_in_image_restrict_eq, trans, equalityD1]) 2);
--- a/src/ZF/AC/HH.ML Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/AC/HH.ML Wed Jan 08 15:04:27 1997 +0100
@@ -149,7 +149,7 @@
by (asm_full_simp_tac (!simpset addsimps [lam_type, Diff_eq_0_iff]) 1);
by (Step_tac 1);
by (set_mp_tac 1);
-by (deepen_tac (eq_cs addSIs [bexI] addSEs [equalityE]) 4 1);
+by (deepen_tac (!claset addSIs [bexI] addSEs [equalityE]) 4 1);
val lam_surj_sing = result();
goal thy "!!x. y:Pow(x)-{0} ==> x ~= 0";
@@ -188,30 +188,32 @@
addSDs [singleton_subsetD]) 1);
val HH_subset_imp_eq = result();
-goal thy "!!f. [| f : (PROD X:Pow(x)-{0}. {{z}. z:x}); \
+goal thy "!!f. [| f : (Pow(x)-{0}) -> {{z}. z:x}; \
\ a:(LEAST i. HH(f,x,i)={x}) |] ==> EX z:x. HH(f,x,a) = {z}";
by (dtac less_Least_subset_x 1);
by (forward_tac [HH_subset_imp_eq] 1);
by (dtac apply_type 1);
by (resolve_tac [Diff_subset RS PowI RS DiffI] 1);
-by (fast_tac (!claset addSDs [HH_subset_x_imp_subset_Diff_UN RS not_emptyI2]) 1);
-by (fast_tac (!claset addSEs [RepFunE] addEs [ssubst]) 1);
+by (fast_tac
+ (!claset addSDs [HH_subset_x_imp_subset_Diff_UN RS not_emptyI2]) 1);
+by (fast_tac (!claset addss (!simpset)) 1);
val f_sing_imp_HH_sing = result();
goalw thy [bij_def]
"!!f. [| x - (UN j: (LEAST i. HH(f,x,i)={x}). HH(f,x,j)) = 0; \
-\ f : (PROD X:Pow(x)-{0}. {{z}. z:x}) |] \
+\ f : (Pow(x)-{0}) -> {{z}. z:x} |] \
\ ==> (lam a:(LEAST i. HH(f,x,i)={x}). HH(f,x,a)) \
\ : bij(LEAST i. HH(f,x,i)={x}, {{y}. y:x})";
by (fast_tac (!claset addSIs [lam_Least_HH_inj, lam_surj_sing,
- f_sing_imp_HH_sing]) 1);
+ f_sing_imp_HH_sing]) 1);
val f_sing_lam_bij = result();
goal thy "!!f. f: (PROD X: Pow(x)-{0}. F(X)) \
\ ==> (lam X:Pow(x)-{0}. {f`X}) : (PROD X: Pow(x)-{0}. {{z}. z:F(X)})";
by (fast_tac (FOL_cs addSIs [lam_type, RepFun_eqI, singleton_eq_iff RS iffD2]
- addDs [apply_type]) 1);
+ addDs [apply_type]) 1);
val lam_singI = result();
-val bij_Least_HH_x = standard (lam_singI RSN (2,
- [f_sing_lam_bij, lam_sing_bij RS bij_converse_bij] MRS comp_bij));
+val bij_Least_HH_x =
+ (lam_singI RSN (2, [f_sing_lam_bij, lam_sing_bij RS bij_converse_bij]
+ MRS comp_bij)) |> standard;
--- a/src/ZF/AC/WO1_WO8.ML Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/AC/WO1_WO8.ML Wed Jan 08 15:04:27 1997 +0100
@@ -24,7 +24,6 @@
by (fast_tac (!claset addSEs [lam_sing_bij RS bij_is_inj RS
well_ord_rvimage]) 2);
by (res_inst_tac [("x","lam a:{{x}. x:A}. THE x. a={x}")] exI 1);
-by (fast_tac (!claset addSEs [singleton_eq_iff RS iffD1 RS sym]
- addSIs [lam_type]
- addIs [the_equality RS ssubst]) 1);
+by (fast_tac (!claset addSIs [lam_type]
+ addss (!simpset addsimps [singleton_eq_iff, the_equality])) 1);
qed "WO8_WO1";
--- a/src/ZF/AC/WO2_AC16.ML Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/AC/WO2_AC16.ML Wed Jan 08 15:04:27 1997 +0100
@@ -124,7 +124,7 @@
val Finite_lesspoll_infinite_Ord = result();
goal thy "!!x. x:X ==> Union(X) = Union(X-{x}) Un x";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
val Union_eq_Un_Diff = result();
goal thy "!!n. n:nat ==> ALL X. X eqpoll n --> (ALL x:X. Finite(x)) \
@@ -182,7 +182,7 @@
(* ********************************************************************** *)
goal thy "A Un {a} = cons(a, A)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
val Un_sing_eq_cons = result();
goal thy "!!A. A lepoll B ==> A Un {a} lepoll succ(B)";
@@ -361,7 +361,7 @@
(* ********************************************************************** *)
goal thy "!!A. [| A <= B; a : A; A - {a} = B - {a} |] ==> A = B";
-by (fast_tac (eq_cs addSEs [equalityE]) 1);
+by (fast_tac (!claset addSEs [equalityE]) 1);
val Diffs_eq_imp_eq = result();
goal thy "!!A. m:nat ==> ALL A B. A <= B & m lepoll A & B lepoll m --> A=B";
@@ -538,27 +538,32 @@
by (etac OUN_E 1);
by (dtac prem1 1);
by (Fast_tac 1);
+(** LEVEL 5 **)
by (rtac ballI 1);
by (etac imageE 1);
by (dresolve_tac [prem3 RS Limit_is_Ord RSN (2, ltI) RS
(prem3 RS Limit_has_succ)] 1);
by (forward_tac [prem1] 1);
by (etac conjE 1);
+(** LEVEL 10 **)
by (dresolve_tac [leI RS succ_leE RSN (2, ospec)] 1 THEN (assume_tac 1));
by (etac impE 1);
by (fast_tac (!claset addSEs [leI RS succ_leE RS lt_Ord RS le_refl]) 1);
by (dresolve_tac [prem2 RSN (2, apply_equality)] 1);
by (REPEAT (eresolve_tac [conjE, ex1E] 1));
+(** LEVEL 15 **)
by (rtac ex1I 1);
by (fast_tac (!claset addSIs [OUN_I]) 1);
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 2);
+(** LEVEL 20 **)
+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));
by (etac conjE 1);
+(** LEVEL 25 **)
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 (etac ex1_two_eq 1);
@@ -573,7 +578,8 @@
"!!n k. [| WO2; 0<m; k:nat; m:nat |] ==> AC16(k #+ m,k)";
by (rtac allI 1);
by (rtac impI 1);
-by (forward_tac [WO2_infinite_subsets_eqpoll_X] 1 THEN (REPEAT (assume_tac 1)));
+by (forward_tac [WO2_infinite_subsets_eqpoll_X] 1
+ THEN (REPEAT (assume_tac 1)));
by (forw_inst_tac [("n","k #+ m")] (WO2_infinite_subsets_eqpoll_X) 1
THEN (REPEAT (ares_tac [add_type] 1)));
by (forward_tac [WO2_imp_ex_Card] 1);
--- a/src/ZF/AC/WO6_WO1.ML Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/AC/WO6_WO1.ML Wed Jan 08 15:04:27 1997 +0100
@@ -65,7 +65,7 @@
\ (EX b<a. f`b ~= 0 & (ALL g<a. ALL d<a. u(f,b,g,d) ~= 0 --> \
\ u(f,b,g,d) eqpoll m))";
by (Asm_simp_tac 1);
-by (Fast_tac 1);
+by (fast_tac (!claset delrules [equalityI]) 1);
val cases = result();
(* ********************************************************************** *)
@@ -233,7 +233,7 @@
\ |] ==> vv2(f,b,g,s) <= f`g";
by (split_tac [expand_if] 1);
by (Step_tac 1);
-be (uu_Least_is_fun RS apply_type) 1;
+by (etac (uu_Least_is_fun RS apply_type) 1);
by (REPEAT_SOME (fast_tac (!claset addSIs [not_emptyI, singleton_subsetI])));
val vv2_subset = result();
@@ -354,7 +354,7 @@
goal thy "EX y. x Un y*y <= y";
by (res_inst_tac [("x","UN n:nat. rec(n, x, %k r. r Un r*r)")] exI 1);
by (safe_tac (!claset));
-br (nat_0I RS UN_I) 1;
+by (rtac (nat_0I RS UN_I) 1);
by (Asm_simp_tac 1);
by (res_inst_tac [("a","succ(n Un na)")] UN_I 1);
by (eresolve_tac [Un_nat_type RS nat_succI] 1 THEN (assume_tac 1));
--- a/src/ZF/AC/rel_is_fun.ML Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/AC/rel_is_fun.ML Wed Jan 08 15:04:27 1997 +0100
@@ -20,8 +20,8 @@
by (etac domainE 1);
by (forward_tac [inj_is_fun RS apply_type] 1 THEN (atac 1));
by (rtac LeastI2 1);
-by (REPEAT (fast_tac (!claset addIs [fst_conv, left_inverse RS ssubst]
- addSEs [nat_into_Ord RS Ord_in_Ord]) 1));
+by (REPEAT (fast_tac (!claset addSEs [nat_into_Ord RS Ord_in_Ord]
+ addss (!simpset addsimps [left_inverse])) 1));
val lepoll_m_imp_domain_lepoll_m = result();
goalw Cardinal.thy [function_def]
--- a/src/ZF/Arith.ML Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/Arith.ML Wed Jan 08 15:04:27 1997 +0100
@@ -335,7 +335,7 @@
nat_into_Ord, not_lt_iff_le RS iffD1];
val div_ss = (!simpset) addsimps [nat_into_Ord, div_termination RS ltD,
- not_lt_iff_le RS iffD2];
+ not_lt_iff_le RS iffD2];
(*Type checking depends upon termination!*)
goalw Arith.thy [mod_def] "!!m n. [| 0<n; m:nat; n:nat |] ==> m mod n : nat";
@@ -585,7 +585,7 @@
(*Thanks to Sten Agerholm*)
goal Arith.thy (* add_le_elim1 *)
"!!m n k. [|m#+n le m#+k; m:nat; n:nat; k:nat|] ==> n le k";
-be rev_mp 1;
+by (etac rev_mp 1);
by (eres_inst_tac[("n","n")]nat_induct 1);
by (Asm_simp_tac 1);
by (Step_tac 1);
--- a/src/ZF/Bool.ML Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/Bool.ML Wed Jan 08 15:04:27 1997 +0100
@@ -11,7 +11,7 @@
val bool_defs = [bool_def,cond_def];
goalw Bool.thy [succ_def] "{0} = 1";
-br refl 1;
+by (rtac refl 1);
qed "singleton_0";
(* Introduction rules *)
--- a/src/ZF/Cardinal.ML Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/Cardinal.ML Wed Jan 08 15:04:27 1997 +0100
@@ -110,7 +110,7 @@
qed "eqpoll_iff";
goalw Cardinal.thy [lepoll_def, inj_def] "!!A. A lepoll 0 ==> A = 0";
-by (fast_tac (eq_cs addDs [apply_type]) 1);
+by (fast_tac (!claset addDs [apply_type]) 1);
qed "lepoll_0_is_0";
(*0 lepoll Y*)
@@ -163,7 +163,7 @@
addEs [apply_funtype RS succE]) 1);
(*Proving it's injective*)
by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
-by (Fast_tac 1);
+by (fast_tac (!claset delrules [equalityI]) 1);
qed "inj_not_surj_succ";
(** Variations on transitivity **)
@@ -671,7 +671,7 @@
by (forward_tac [Diff_sing_lepoll] 1);
by (assume_tac 1);
by (dtac lepoll_0_is_0 1);
-by (fast_tac (eq_cs addEs [equalityE]) 1);
+by (fast_tac (!claset addEs [equalityE]) 1);
qed "lepoll_1_is_sing";
goalw Cardinal.thy [lepoll_def] "A Un B lepoll A+B";
--- a/src/ZF/CardinalArith.ML Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/CardinalArith.ML Wed Jan 08 15:04:27 1997 +0100
@@ -421,7 +421,7 @@
by (REPEAT (eresolve_tac [asm_rl, lt_trans] 2));
by (REPEAT (etac ltE 1));
by (asm_simp_tac (!simpset addsimps [rvimage_iff, rmult_iff, Memrel_iff,
- Un_absorb, Un_least_mem_iff, ltD]) 1);
+ Un_absorb, Un_least_mem_iff, ltD]) 1);
qed "csquare_ltI";
(*Part of the traditional proof. UNUSED since it's harder to prove & apply *)
@@ -758,7 +758,7 @@
by (subgoal_tac "cons(x,cons(xa,y)) = cons(xa,cons(x,y))" 1);
by (Asm_simp_tac 1);
by (fast_tac (!claset addSDs [cons_lepoll_consD]) 1);
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Fin_imp_not_cons_lepoll";
goal CardinalArith.thy
--- a/src/ZF/Cardinal_AC.ML Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/Cardinal_AC.ML Wed Jan 08 15:04:27 1997 +0100
@@ -190,7 +190,7 @@
Card_is_Ord, Ord_0_lt_csucc]) 2);
by (asm_full_simp_tac
(!simpset addsimps [InfCard_is_Card, le_Card_iff, lepoll_def]) 1);
-by (safe_tac eq_cs);
+by (safe_tac (!claset addSIs [equalityI]));
by (swap_res_tac [[inj_UN_subset, cardinal_UN_Ord_lt_csucc]
MRS lt_subset_trans] 1);
by (REPEAT (assume_tac 1));
--- a/src/ZF/Coind/MT.ML Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/Coind/MT.ML Wed Jan 08 15:04:27 1997 +0100
@@ -36,7 +36,7 @@
AddDs [te_owrE,(ElabRel.dom_subset RS subsetD)];
Addsimps [ve_dom_owr, te_dom_owr, ve_app_owr1, ve_app_owr2,
- te_app_owr1, te_app_owr2];
+ te_app_owr1, te_app_owr2];
val clean_tac =
REPEAT_FIRST (fn i =>
@@ -129,7 +129,7 @@
by (etac htr_closE 1);
by (etac elab_fnE 1);
by (rewrite_tac Ty.con_defs);
-by (safe_tac sum_cs);
+by (safe_tac (!claset));
by (dtac (spec RS spec RS mp RS mp) 1);
by (assume_tac 3);
by (assume_tac 2);
--- a/src/ZF/Coind/Map.ML Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/Coind/Map.ML Wed Jan 08 15:04:27 1997 +0100
@@ -11,19 +11,19 @@
(* ############################################################ *)
goal Map.thy "!!A. a:A ==> Sigma(A,B)``{a} = B(a)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "qbeta";
goal Map.thy "!!A. a~:A ==> Sigma(A,B)``{a} = 0";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "qbeta_emp";
goal Map.thy "!!A.a ~: A ==> Sigma(A,B)``{a}=0";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "image_Sigma1";
goal Map.thy "0``A = 0";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "image_02";
(* ############################################################ *)
@@ -107,7 +107,7 @@
goalw Map.thy [TMap_def,map_app_def,domain_def]
"!!m.[| m:TMap(A,B); a:domain(m) |] ==> map_app(m,a):B";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "tmap_appI";
goalw Map.thy [PMap_def]
@@ -123,12 +123,12 @@
goalw Map.thy [TMap_def]
"!!m.[| m:TMap(A,B); a:domain(m) |] ==> a:A";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "tmap_domainD";
goalw Map.thy [PMap_def,TMap_def]
"!!m.[| m:PMap(A,B); a:domain(m) |] ==> a:A";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "pmap_domainD";
(* ############################################################ *)
@@ -140,33 +140,33 @@
(* Lemmas *)
goal Map.thy "domain(UN x:A.B(x)) = (UN x:A.domain(B(x)))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "domain_UN";
goal Map.thy "domain(Sigma(A,B)) = {x:A.EX y.y:B(x)}";
by (simp_tac (!simpset addsimps [domain_UN,domain_0,domain_cons]) 1);
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "domain_Sigma";
(* Theorems *)
goalw Map.thy [map_emp_def] "domain(map_emp) = 0";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "map_domain_emp";
goalw Map.thy [map_owr_def]
"!!a.b ~= 0 ==> domain(map_owr(f,a,b)) = {a} Un domain(f)";
by (simp_tac (!simpset addsimps [domain_Sigma]) 1);
by (rtac equalityI 1);
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
by (rtac subsetI 1);
by (rtac CollectI 1);
by (assume_tac 1);
by (etac UnE' 1);
by (etac singletonE 1);
by (Asm_simp_tac 1);
-by (fast_tac eq_cs 1);
-by (fast_tac (eq_cs addss (!simpset)) 1);
+by (Fast_tac 1);
+by (fast_tac (!claset addss (!simpset)) 1);
qed "map_domain_owr";
(** Application **)
@@ -183,7 +183,7 @@
by (rtac (excluded_middle RS disjE) 1);
by (stac qbeta_emp 1);
by (assume_tac 1);
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
by (etac (qbeta RS ssubst) 1);
by (Asm_simp_tac 1);
qed "map_app_owr2";
--- a/src/ZF/Epsilon.ML Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/Epsilon.ML Wed Jan 08 15:04:27 1997 +0100
@@ -112,7 +112,7 @@
goalw Epsilon.thy [Transset_def]
"!!i j. [| Transset(i); j:i |] ==> Memrel(i)-``{j} = j";
-by (fast_tac (eq_cs addSIs [MemrelI] addSEs [MemrelE]) 1);
+by (fast_tac (!claset addSIs [MemrelI] addSEs [MemrelE]) 1);
qed "under_Memrel";
(* j : eclose(A) ==> Memrel(eclose(A)) -`` j = j *)
--- a/src/ZF/EquivClass.ML Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/EquivClass.ML Wed Jan 08 15:04:27 1997 +0100
@@ -110,7 +110,7 @@
goalw EquivClass.thy [equiv_def,refl_def,quotient_def]
"!!A r. equiv(A,r) ==> Union(A/r) = A";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Union_quotient";
goalw EquivClass.thy [quotient_def]
@@ -181,7 +181,7 @@
by (rtac (equivA RS equiv_type RS subsetD RS SigmaE2) 1);
by (assume_tac 1);
by (asm_simp_tac (!simpset addsimps [equivA RS UN_equiv_class,
- congruent2_implies_congruent]) 1);
+ congruent2_implies_congruent]) 1);
by (rewrite_goals_tac [congruent2_def,equiv_def,refl_def]);
by (Fast_tac 1);
qed "congruent2_implies_congruent_UN";
@@ -191,8 +191,8 @@
\ ==> (UN x1:r``{a1}. UN x2:r``{a2}. b(x1,x2)) = b(a1,a2)";
by (cut_facts_tac prems 1);
by (asm_simp_tac (!simpset addsimps [equivA RS UN_equiv_class,
- congruent2_implies_congruent,
- congruent2_implies_congruent_UN]) 1);
+ congruent2_implies_congruent,
+ congruent2_implies_congruent_UN]) 1);
qed "UN_equiv_class2";
(*type checking*)
@@ -249,6 +249,6 @@
by (rtac (equivA RS equiv_type RS subsetD RS SigmaE2) 1);
by (assume_tac 1);
by (asm_simp_tac (!simpset addsimps [commute,
- [equivA, congt] MRS UN_equiv_class]) 1);
+ [equivA, congt] MRS UN_equiv_class]) 1);
by (REPEAT (ares_tac [congt' RS spec RS spec RS mp] 1));
qed "congruent_commuteI";
--- a/src/ZF/List.ML Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/List.ML Wed Jan 08 15:04:27 1997 +0100
@@ -28,7 +28,7 @@
goal List.thy "list(A) = {0} + (A * list(A))";
let open list; val rew = rewrite_rule con_defs in
-by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs)
+by (fast_tac (!claset addSIs (equalityI :: map rew intrs)
addEs [rew elim]) 1)
end;
qed "list_unfold";
@@ -113,7 +113,7 @@
goalw List.thy [drop_def]
"!!i. i:nat ==> drop(succ(i), Cons(a,l)) = drop(i,l)";
-br sym 1;
+by (rtac sym 1);
by (etac nat_induct 1);
by (Simp_tac 1);
by (Asm_simp_tac 1);
--- a/src/ZF/Order.ML Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/Order.ML Wed Jan 08 15:04:27 1997 +0100
@@ -82,13 +82,13 @@
goalw Order.thy [pred_def]
"pred(pred(A,x,r), y, r) = pred(A,x,r) Int pred(A,y,r)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "pred_pred_eq";
goalw Order.thy [trans_on_def, pred_def]
"!!r. [| trans[A](r); <y,x>:r; x:A; y:A \
\ |] ==> pred(pred(A,x,r), y, r) = pred(A,y,r)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "trans_pred_pred_eq";
@@ -171,7 +171,7 @@
qed "tot_ord_0";
goalw Order.thy [wf_on_def, wf_def] "wf[0](r)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "wf_on_0";
goalw Order.thy [well_ord_def] "well_ord(0,r)";
@@ -300,7 +300,7 @@
goalw Order.thy [part_ord_def, irrefl_def, trans_on_def, ord_iso_def]
"!!A B r. [| part_ord(B,s); f: ord_iso(A,r,B,s) |] ==> part_ord(A,r)";
by (Asm_simp_tac 1);
-by (fast_tac (ZF_cs addIs [bij_is_fun RS apply_type]) 1);
+by (fast_tac (!claset addIs [bij_is_fun RS apply_type]) 1);
qed "part_ord_ord_iso";
goalw Order.thy [linear_def, ord_iso_def]
@@ -319,11 +319,10 @@
by (asm_full_simp_tac (!simpset addcongs [conj_cong2]) 1);
by (safe_tac (!claset));
by (dres_inst_tac [("x", "{f`z. z:Z Int A}")] spec 1);
-by (safe_tac eq_cs);
+by (safe_tac (!claset addSIs [equalityI]));
by (dtac equalityD1 1);
by (fast_tac (!claset addSIs [bexI]) 1);
-by (fast_tac (!claset addSIs [bexI]
- addIs [bij_is_fun RS apply_type]) 1);
+by (fast_tac (!claset addSIs [bexI] addIs [bij_is_fun RS apply_type]) 1);
qed "wf_on_ord_iso";
goalw Order.thy [well_ord_def, tot_ord_def]
@@ -382,7 +381,8 @@
by (etac CollectE 1);
by (asm_simp_tac
(!simpset addsimps [[bij_is_fun, Collect_subset] MRS image_fun]) 1);
-by (safe_tac (eq_cs addSEs [bij_is_fun RS apply_type]));
+by (rtac equalityI 1);
+by (safe_tac (!claset addSEs [bij_is_fun RS apply_type]));
by (rtac RepFun_eqI 1);
by (fast_tac (!claset addSIs [right_inverse_bij RS sym]) 1);
by (asm_simp_tac bij_inverse_ss 1);
@@ -472,7 +472,7 @@
goalw Order.thy [ord_iso_map_def]
"converse(ord_iso_map(A,r,B,s)) = ord_iso_map(B,s,A,r)";
-by (fast_tac (eq_cs addIs [ord_iso_sym]) 1);
+by (fast_tac (!claset addIs [ord_iso_sym]) 1);
qed "converse_ord_iso_map";
goalw Order.thy [ord_iso_map_def, function_def]
--- a/src/ZF/OrderArith.ML Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/OrderArith.ML Wed Jan 08 15:04:27 1997 +0100
@@ -15,22 +15,22 @@
goalw OrderArith.thy [radd_def]
"<Inl(a), Inr(b)> : radd(A,r,B,s) <-> a:A & b:B";
-by (fast_tac sum_cs 1);
+by (Fast_tac 1);
qed "radd_Inl_Inr_iff";
goalw OrderArith.thy [radd_def]
"<Inl(a'), Inl(a)> : radd(A,r,B,s) <-> a':A & a:A & <a',a>:r";
-by (fast_tac sum_cs 1);
+by (Fast_tac 1);
qed "radd_Inl_iff";
goalw OrderArith.thy [radd_def]
"<Inr(b'), Inr(b)> : radd(A,r,B,s) <-> b':B & b:B & <b',b>:s";
-by (fast_tac sum_cs 1);
+by (Fast_tac 1);
qed "radd_Inr_iff";
goalw OrderArith.thy [radd_def]
"<Inr(b), Inl(a)> : radd(A,r,B,s) <-> False";
-by (fast_tac sum_cs 1);
+by (Fast_tac 1);
qed "radd_Inr_Inl_iff";
(** Elimination Rule **)
@@ -48,7 +48,7 @@
(*Apply each premise to correct subgoal; can't just use fast_tac
because hyp_subst_tac would delete equalities too quickly*)
by (EVERY (map (fn prem =>
- EVERY1 [rtac prem, assume_tac, REPEAT o fast_tac sum_cs])
+ EVERY1 [rtac prem, assume_tac, REPEAT o Fast_tac])
prems));
qed "raddE";
@@ -63,7 +63,7 @@
(** Linearity **)
Addsimps [radd_Inl_iff, radd_Inr_iff,
- radd_Inl_Inr_iff, radd_Inr_Inl_iff];
+ radd_Inl_Inr_iff, radd_Inr_Inl_iff];
goalw OrderArith.thy [linear_def]
"!!r s. [| linear(A,r); linear(B,s) |] ==> linear(A+B,radd(A,r,B,s))";
@@ -83,15 +83,15 @@
by (rtac ballI 2);
by (eres_inst_tac [("r","r"),("a","x")] wf_on_induct 2 THEN assume_tac 2);
by (etac (bspec RS mp) 2);
-by (fast_tac sum_cs 2);
-by (best_tac (sum_cs addSEs [raddE]) 2);
+by (Fast_tac 2);
+by (best_tac (!claset addSEs [raddE]) 2);
(*Returning to main part of proof*)
by (REPEAT_FIRST (eresolve_tac [sumE, ssubst]));
-by (best_tac sum_cs 1);
+by (Best_tac 1);
by (eres_inst_tac [("r","s"),("a","ya")] wf_on_induct 1 THEN assume_tac 1);
by (etac (bspec RS mp) 1);
-by (fast_tac sum_cs 1);
-by (best_tac (sum_cs addSEs [raddE]) 1);
+by (Fast_tac 1);
+by (best_tac (!claset addSEs [raddE]) 1);
qed "wf_on_radd";
goal OrderArith.thy
@@ -129,7 +129,7 @@
by (safe_tac (!claset addSIs [sum_bij]));
(*Do the beta-reductions now*)
by (ALLGOALS (Asm_full_simp_tac));
-by (safe_tac sum_cs);
+by (safe_tac (!claset));
(*8 subgoals!*)
by (ALLGOALS
(asm_full_simp_tac
@@ -143,9 +143,9 @@
\ (lam z:A+B. case(%x.x, %y.y, z)) : bij(A+B, A Un B)";
by (res_inst_tac [("d", "%z. if(z:A, Inl(z), Inr(z))")]
lam_bijective 1);
-by (fast_tac (sum_cs addSIs [if_type]) 2);
+by (fast_tac (!claset addSIs [if_type]) 2);
by (DEPTH_SOLVE_1 (eresolve_tac [case_type, UnI1, UnI2] 1));
-by (safe_tac sum_cs);
+by (safe_tac (!claset));
by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if])));
by (fast_tac (!claset addEs [equalityE]) 1);
qed "sum_disjoint_bij";
@@ -295,10 +295,10 @@
by (resolve_tac [id_bij RS sum_bij RS comp_bij] 1);
by (rtac singleton_prod_bij 1);
by (rtac sum_disjoint_bij 1);
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
by (asm_simp_tac (!simpset addcongs [case_cong] addsimps [id_conv]) 1);
by (resolve_tac [comp_lam RS trans RS sym] 1);
-by (fast_tac (sum_cs addSEs [case_type]) 1);
+by (fast_tac (!claset addSEs [case_type]) 1);
by (asm_simp_tac (!simpset addsimps [case_case]) 1);
qed "prod_sum_singleton_bij";
@@ -374,7 +374,7 @@
goalw OrderArith.thy [rvimage_def]
"rvimage(A,f, converse(r)) = converse(rvimage(A,f,r))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "rvimage_converse";
@@ -441,5 +441,5 @@
goalw OrderArith.thy [ord_iso_def, rvimage_def]
"!!A B. f: ord_iso(A,r, B,s) ==> rvimage(A,f,s) = r Int A*A";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "ord_iso_rvimage_eq";
--- a/src/ZF/OrderType.ML Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/OrderType.ML Wed Jan 08 15:04:27 1997 +0100
@@ -32,12 +32,12 @@
goalw OrderType.thy [pred_def, lt_def]
"!!i j. j<i ==> pred(i, j, Memrel(i)) = j";
by (asm_simp_tac (!simpset addsimps [Memrel_iff]) 1);
-by (fast_tac (eq_cs addEs [Ord_trans]) 1);
+by (fast_tac (!claset addEs [Ord_trans]) 1);
qed "lt_pred_Memrel";
goalw OrderType.thy [pred_def,Memrel_def]
"!!A x. x:A ==> pred(A, x, Memrel(A)) = A Int x";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "pred_Memrel";
goal OrderType.thy
@@ -241,7 +241,7 @@
by (asm_full_simp_tac (!simpset addsimps [pred_def]) 1);
by (rtac (refl RSN (2,RepFun_cong)) 1);
by (dtac well_ord_is_trans_on 1);
-by (fast_tac (eq_cs addSEs [trans_onD]) 1);
+by (fast_tac (!claset addSEs [trans_onD]) 1);
qed "ordermap_pred_eq_ordermap";
goalw OrderType.thy [ordertype_def]
@@ -275,7 +275,8 @@
goal OrderType.thy
"!!A r. well_ord(A,r) ==> \
\ ordertype(A,r) = {ordertype(pred(A,x,r),r). x:A}";
-by (safe_tac (eq_cs addSIs [ordertype_pred_lt RS ltD]));
+by (rtac equalityI 1);
+by (safe_tac (!claset addSIs [ordertype_pred_lt RS ltD]));
by (fast_tac
(!claset addss
(!simpset addsimps [ordertype_def,
@@ -294,7 +295,7 @@
by (rtac conjI 1);
by (etac well_ord_Memrel 1);
by (rewrite_goals_tac [Ord_def, Transset_def, pred_def, Memrel_def]);
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Ord_is_Ord_alt";
(*proof by lcp*)
@@ -319,7 +320,7 @@
goal OrderType.thy "(lam z:A+0. case(%x.x, %y.y, z)) : bij(A+0, A)";
by (res_inst_tac [("d", "Inl")] lam_bijective 1);
-by (safe_tac sum_cs);
+by (safe_tac (!claset));
by (ALLGOALS (Asm_simp_tac));
qed "bij_sum_0";
@@ -327,12 +328,12 @@
"!!A r. well_ord(A,r) ==> ordertype(A+0, radd(A,r,0,s)) = ordertype(A,r)";
by (resolve_tac [bij_sum_0 RS ord_isoI RS ordertype_eq] 1);
by (assume_tac 2);
-by (fast_tac (sum_cs addss (!simpset addsimps [radd_Inl_iff, Memrel_iff])) 1);
+by (fast_tac (!claset addss (!simpset addsimps [radd_Inl_iff, Memrel_iff])) 1);
qed "ordertype_sum_0_eq";
goal OrderType.thy "(lam z:0+A. case(%x.x, %y.y, z)) : bij(0+A, A)";
by (res_inst_tac [("d", "Inr")] lam_bijective 1);
-by (safe_tac sum_cs);
+by (safe_tac (!claset));
by (ALLGOALS (Asm_simp_tac));
qed "bij_0_sum";
@@ -340,7 +341,7 @@
"!!A r. well_ord(A,r) ==> ordertype(0+A, radd(0,s,A,r)) = ordertype(A,r)";
by (resolve_tac [bij_0_sum RS ord_isoI RS ordertype_eq] 1);
by (assume_tac 2);
-by (fast_tac (sum_cs addss (!simpset addsimps [radd_Inr_iff, Memrel_iff])) 1);
+by (fast_tac (!claset addss (!simpset addsimps [radd_Inr_iff, Memrel_iff])) 1);
qed "ordertype_0_sum_eq";
(** Initial segments of radd. Statements by Grabczewski **)
@@ -351,7 +352,7 @@
\ (lam x:pred(A,a,r). Inl(x)) \
\ : bij(pred(A,a,r), pred(A+B, Inl(a), radd(A,r,B,s)))";
by (res_inst_tac [("d", "case(%x.x, %y.y)")] lam_bijective 1);
-by (safe_tac sum_cs);
+by (safe_tac (!claset));
by (ALLGOALS
(asm_full_simp_tac
(!simpset addsimps [radd_Inl_iff, radd_Inr_Inl_iff])));
@@ -371,7 +372,7 @@
\ id(A+pred(B,b,s)) \
\ : bij(A+pred(B,b,s), pred(A+B, Inr(b), radd(A,r,B,s)))";
by (res_inst_tac [("d", "%z.z")] lam_bijective 1);
-by (safe_tac sum_cs);
+by (safe_tac (!claset));
by (ALLGOALS (Asm_full_simp_tac));
qed "pred_Inr_bij";
@@ -380,7 +381,7 @@
\ ordertype(pred(A+B, Inr(b), radd(A,r,B,s)), radd(A,r,B,s)) = \
\ ordertype(A+pred(B,b,s), radd(A,r,pred(B,b,s),s))";
by (resolve_tac [pred_Inr_bij RS ord_isoI RS ord_iso_sym RS ordertype_eq] 1);
-by (fast_tac (sum_cs addss (!simpset addsimps [pred_def, id_def])) 2);
+by (fast_tac (!claset addss (!simpset addsimps [pred_def, id_def])) 2);
by (REPEAT_FIRST (ares_tac [well_ord_radd, pred_subset, well_ord_subset]));
qed "ordertype_pred_Inr_eq";
@@ -414,9 +415,9 @@
by (REPEAT (ares_tac [Ord_ordertype, well_ord_radd, well_ord_Memrel] 2));
by (asm_simp_tac
(!simpset addsimps [ordertype_pred_unfold,
- well_ord_radd, well_ord_Memrel,
- ordertype_pred_Inl_eq,
- lt_pred_Memrel, leI RS le_ordertype_Memrel]
+ well_ord_radd, well_ord_Memrel,
+ ordertype_pred_Inl_eq,
+ lt_pred_Memrel, leI RS le_ordertype_Memrel]
setloop rtac (InlI RSN (2,bexI))) 1);
qed "lt_oadd1";
@@ -487,7 +488,7 @@
(!simpset addsimps [ordertype_pred_unfold, well_ord_radd,
well_ord_Memrel]) 1);
by (eresolve_tac [ltD RS RepFunE] 1);
-by (fast_tac (sum_cs addss
+by (fast_tac (!claset addss
(!simpset addsimps [ordertype_pred_Inl_eq, well_ord_Memrel,
ltI, lt_pred_Memrel, le_ordertype_Memrel, leI,
ordertype_pred_Inr_eq,
@@ -522,12 +523,12 @@
goal OrderType.thy "!!i. Ord(i) ==> i++1 = succ(i)";
by (asm_simp_tac (!simpset addsimps [oadd_unfold, Ord_1, oadd_0]) 1);
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "oadd_1";
goal OrderType.thy
"!!i. [| Ord(i); Ord(j) |] ==> i++succ(j) = succ(i++j)";
- (*ZF_ss prevents looping*)
+ (*ZF_ss prevents looping*)
by (asm_simp_tac (ZF_ss addsimps [Ord_oadd, oadd_1 RS sym]) 1);
by (asm_simp_tac (!simpset addsimps [oadd_1, oadd_assoc, Ord_1]) 1);
qed "oadd_succ";
@@ -538,7 +539,7 @@
val prems = goal OrderType.thy
"[| Ord(i); !!x. x:A ==> Ord(j(x)); a:A |] ==> \
\ i ++ (UN x:A. j(x)) = (UN x:A. i++j(x))";
-by (fast_tac (eq_cs addIs (prems @ [ltI, Ord_UN, Ord_oadd,
+by (fast_tac (!claset addIs (prems @ [ltI, Ord_UN, Ord_oadd,
lt_oadd1 RS ltD, oadd_lt_mono2 RS ltD])
addSEs [ltE, ltI RS lt_oadd_disj RS disjE]) 1);
qed "oadd_UN";
@@ -562,7 +563,7 @@
by (rtac le_implies_UN_le_UN 2);
by (Fast_tac 2);
by (asm_simp_tac (!simpset addsimps [Union_eq_UN RS sym, Limit_Union_eq,
- le_refl, Limit_is_Ord]) 1);
+ le_refl, Limit_is_Ord]) 1);
qed "oadd_le_self2";
goal OrderType.thy "!!i j k. [| k le j; Ord(i) |] ==> k++i le j++i";
@@ -600,7 +601,7 @@
goal OrderType.thy
"!!A B. A<=B ==> (lam y:B. if(y:A, Inl(y), Inr(y))) : bij(B, A+(B-A))";
by (res_inst_tac [("d", "case(%x.x, %y.y)")] lam_bijective 1);
-by (fast_tac (sum_cs addSIs [if_type]) 1);
+by (fast_tac (!claset addSIs [if_type]) 1);
by (fast_tac (!claset addSIs [case_type]) 1);
by (etac sumE 2);
by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if])));
@@ -677,7 +678,8 @@
"!!A B. [| a:A; b:B |] ==> \
\ pred(A*B, <a,b>, rmult(A,r,B,s)) = \
\ pred(A,a,r)*B Un ({a} * pred(B,b,s))";
-by (safe_tac eq_cs);
+by (rtac equalityI 1);
+by (safe_tac (!claset));
by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [rmult_iff])));
by (ALLGOALS (Fast_tac));
qed "pred_Pair_eq";
@@ -730,7 +732,7 @@
by (rtac ltI 1);
by (asm_simp_tac
(!simpset addsimps [Ord_ordertype, well_ord_rmult, well_ord_Memrel,
- lt_Ord2]) 2);
+ lt_Ord2]) 2);
by (asm_simp_tac
(!simpset addsimps [ordertype_pred_unfold,
well_ord_rmult, well_ord_Memrel, lt_Ord2]) 1);
@@ -738,7 +740,7 @@
by (fast_tac (!claset addSEs [ltE]) 2);
by (asm_simp_tac
(!simpset addsimps [ordertype_pred_Pair_lemma, ltI,
- symmetric omult_def]) 1);
+ symmetric omult_def]) 1);
qed "omult_oadd_lt";
goal OrderType.thy
@@ -802,7 +804,7 @@
qed "oadd_omult_distrib";
goal OrderType.thy "!!i. [| Ord(i); Ord(j) |] ==> i**succ(j) = (i**j)++i";
- (*ZF_ss prevents looping*)
+ (*ZF_ss prevents looping*)
by (asm_simp_tac (ZF_ss addsimps [oadd_1 RS sym]) 1);
by (asm_simp_tac
(!simpset addsimps [omult_1, oadd_omult_distrib, Ord_1]) 1);
@@ -830,7 +832,7 @@
"[| Ord(i); !!x. x:A ==> Ord(j(x)) |] ==> \
\ i ** (UN x:A. j(x)) = (UN x:A. i**j(x))";
by (asm_simp_tac (!simpset addsimps (prems@[Ord_UN, omult_unfold])) 1);
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "omult_UN";
goal OrderType.thy
@@ -909,7 +911,7 @@
by (rtac le_implies_UN_le_UN 2);
by (Fast_tac 2);
by (asm_simp_tac (!simpset addsimps [Union_eq_UN RS sym, Limit_Union_eq,
- Limit_is_Ord RS le_refl]) 1);
+ Limit_is_Ord RS le_refl]) 1);
qed "omult_le_self2";
--- a/src/ZF/Ordinal.ML Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/Ordinal.ML Wed Jan 08 15:04:27 1997 +0100
@@ -17,7 +17,7 @@
qed "Transset_iff_Pow";
goalw Ordinal.thy [Transset_def] "Transset(A) <-> Union(succ(A)) = A";
-by (fast_tac (eq_cs addSEs [equalityE]) 1);
+by (fast_tac (!claset addSEs [equalityE]) 1);
qed "Transset_iff_Union_succ";
(** Consequences of downwards closure **)
@@ -314,11 +314,11 @@
qed "Memrel_mono";
goalw Ordinal.thy [Memrel_def] "Memrel(0) = 0";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Memrel_0";
goalw Ordinal.thy [Memrel_def] "Memrel(1) = 0";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Memrel_1";
Addsimps [Memrel_0, Memrel_1];
@@ -396,7 +396,7 @@
by (trans_ind_tac "i" prems 1);
by (rtac (impI RS allI) 1);
by (trans_ind_tac "j" [] 1);
-by (DEPTH_SOLVE (step_tac eq_cs 1 ORELSE Ord_trans_tac 1));
+by (DEPTH_SOLVE (Step_tac 1 ORELSE Ord_trans_tac 1));
qed "Ord_linear_lemma";
(*"[| Ord(i); Ord(x) |] ==> i:x | i=x | x:i"*)
@@ -623,7 +623,7 @@
qed "le_implies_UN_le_UN";
goal Ordinal.thy "!!i. Ord(i) ==> (UN y:i. succ(y)) = i";
-by (fast_tac (eq_cs addEs [Ord_trans]) 1);
+by (fast_tac (!claset addEs [Ord_trans]) 1);
qed "Ord_equality";
(*Holds for all transitive sets, not just ordinals*)
@@ -635,7 +635,7 @@
(*** Limit ordinals -- general properties ***)
goalw Ordinal.thy [Limit_def] "!!i. Limit(i) ==> Union(i) = i";
-by (fast_tac (eq_cs addSIs [ltI] addSEs [ltE] addEs [Ord_trans]) 1);
+by (fast_tac (!claset addSIs [ltI] addSEs [ltE] addEs [Ord_trans]) 1);
qed "Limit_Union_eq";
goalw Ordinal.thy [Limit_def] "!!i. Limit(i) ==> Ord(i)";
@@ -673,7 +673,7 @@
goal Ordinal.thy "!!i. Ord(i) ==> i=0 | (EX j. Ord(j) & i=succ(j)) | Limit(i)";
by (fast_tac (!claset addSIs [non_succ_LimitI, Ord_0_lt]
- addSDs [Ord_succD]) 1);
+ addSDs [Ord_succD]) 1);
qed "Ord_cases_disj";
val major::prems = goal Ordinal.thy
--- a/src/ZF/Perm.ML Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/Perm.ML Wed Jan 08 15:04:27 1997 +0100
@@ -23,7 +23,7 @@
qed "fun_is_surj";
goalw Perm.thy [surj_def] "!!f A B. f: surj(A,B) ==> range(f)=B";
-by (best_tac (!claset addIs [equalityI,apply_Pair] addEs [range_type]) 1);
+by (best_tac (!claset addIs [apply_Pair] addEs [range_type]) 1);
qed "surj_range";
(** A function with a right inverse is a surjection **)
@@ -269,7 +269,7 @@
qed "domain_comp_eq";
goal Perm.thy "(r O s)``A = r``(s``A)";
-by (fast_tac (!claset addIs [equalityI]) 1);
+by (Fast_tac 1);
qed "image_comp";
@@ -286,21 +286,21 @@
(*associative law for composition*)
goal Perm.thy "(r O s) O t = r O (s O t)";
-by (fast_tac (!claset addIs [equalityI]) 1);
+by (Fast_tac 1);
qed "comp_assoc";
(*left identity of composition; provable inclusions are
id(A) O r <= r
and [| r<=A*B; B<=C |] ==> r <= id(C) O r *)
goal Perm.thy "!!r A B. r<=A*B ==> id(B) O r = r";
-by (fast_tac (!claset addIs [equalityI]) 1);
+by (Fast_tac 1);
qed "left_comp_id";
(*right identity of composition; provable inclusions are
r O id(A) <= r
and [| r<=A*B; A<=C |] ==> r <= r O id(C) *)
goal Perm.thy "!!r A B. r<=A*B ==> r O id(A) = r";
-by (fast_tac (!claset addIs [equalityI]) 1);
+by (Fast_tac 1);
qed "right_comp_id";
@@ -404,7 +404,7 @@
(*left inverse of composition; one inclusion is
f: A->B ==> id(A) <= converse(f) O f *)
goalw Perm.thy [inj_def] "!!f. f: inj(A,B) ==> converse(f) O f = id(A)";
-by (fast_tac (!claset addIs [equalityI, apply_Pair]
+by (fast_tac (!claset addIs [apply_Pair]
addEs [domain_type]
addss (!simpset addsimps [apply_iff])) 1);
qed "left_comp_inverse";
--- a/src/ZF/QPair.ML Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/QPair.ML Wed Jan 08 15:04:27 1997 +0100
@@ -88,10 +88,10 @@
(fn prems=> [ (simp_tac (!simpset addsimps prems) 1) ]);
qed_goal "QSigma_empty1" thy "QSigma(0,B) = 0"
- (fn _ => [ (fast_tac (!claset addIs [equalityI]) 1) ]);
+ (fn _ => [ (Fast_tac 1) ]);
qed_goal "QSigma_empty2" thy "A <*> 0 = 0"
- (fn _ => [ (fast_tac (!claset addIs [equalityI]) 1) ]);
+ (fn _ => [ (Fast_tac 1) ]);
Addsimps [QSigma_empty1, QSigma_empty2];
@@ -192,17 +192,17 @@
qed_goal "qconverse_qconverse" thy
"!!A B r. r<=QSigma(A,B) ==> qconverse(qconverse(r)) = r"
- (fn _ => [ (fast_tac (!claset addSIs [equalityI]) 1) ]);
+ (fn _ => [ (Fast_tac 1) ]);
qed_goal "qconverse_type" thy
"!!A B r. r <= A <*> B ==> qconverse(r) <= B <*> A"
(fn _ => [ (Fast_tac 1) ]);
qed_goal "qconverse_prod" thy "qconverse(A <*> B) = B <*> A"
- (fn _ => [ (fast_tac (!claset addSIs [equalityI]) 1) ]);
+ (fn _ => [ (Fast_tac 1) ]);
qed_goal "qconverse_empty" thy "qconverse(0) = 0"
- (fn _ => [ (fast_tac (!claset addSIs [equalityI]) 1) ]);
+ (fn _ => [ (Fast_tac 1) ]);
(**** The Quine-inspired notion of disjoint sum ****)
@@ -315,17 +315,17 @@
(** Rules for the Part primitive **)
goal thy "Part(A <+> B,QInl) = {QInl(x). x: A}";
-by (fast_tac (!claset addIs [equalityI]) 1);
+by (Fast_tac 1);
qed "Part_QInl";
goal thy "Part(A <+> B,QInr) = {QInr(y). y: B}";
-by (fast_tac (!claset addIs [equalityI]) 1);
+by (Fast_tac 1);
qed "Part_QInr";
goal thy "Part(A <+> B, %x.QInr(h(x))) = {QInr(y). y: Part(B,h)}";
-by (fast_tac (!claset addIs [equalityI]) 1);
+by (Fast_tac 1);
qed "Part_QInr2";
goal thy "!!A B C. C <= A <+> B ==> Part(C,QInl) Un Part(C,QInr) = C";
-by (fast_tac (!claset addIs [equalityI]) 1);
+by (Fast_tac 1);
qed "Part_qsum_equality";
--- a/src/ZF/Resid/Cube.ML Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/Resid/Cube.ML Wed Jan 08 15:04:27 1997 +0100
@@ -74,10 +74,10 @@
goal Cube.thy
"!!u.[|w~u; w~v; regular(u); regular(v)|]==> \
-\ EX uv.EX vu. (w|>u) |> vu = (w|>v) |> uv & (w|>u)~vu &\
+\ EX uv vu. (w|>u) |> vu = (w|>v) |> uv & (w|>u)~vu &\
\ regular(vu) & (w|>v)~uv & regular(uv) ";
by (forw_inst_tac [("x1","v")] (comp_sym RS comp_trans) 1);
-by (REPEAT(Step_tac 1));
+by (step_tac (!claset addSIs [exI]) 1);
by (rtac cube 1);
by (asm_simp_tac (prism_ss addsimps [comp_sym_iff]) 1);
by (asm_simp_tac (prism_ss addsimps [comp_sym_iff]) 1);
--- a/src/ZF/Sum.ML Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/Sum.ML Wed Jan 08 15:04:27 1997 +0100
@@ -43,7 +43,7 @@
val sum_defs = [sum_def,Inl_def,Inr_def,case_def];
goalw Sum.thy (bool_def::sum_defs) "Sigma(bool,C) = C(0) + C(1)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Sigma_bool";
(** Introduction rules for the injections **)
@@ -103,8 +103,6 @@
Addsimps [InlI, InrI, Inl_iff, Inr_iff, Inl_Inr_iff, Inr_Inl_iff, sum_empty];
-val sum_cs = !claset;
-
goal Sum.thy "!!A B. Inl(a): A+B ==> a: A";
by (Fast_tac 1);
qed "InlD";
@@ -127,7 +125,7 @@
qed "sum_equal_iff";
goalw Sum.thy [sum_def] "A+A = 2*A";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "sum_eq_2_times";
@@ -143,8 +141,6 @@
Addsimps [case_Inl, case_Inr];
-val sum_ss = !simpset;
-
val major::prems = goal Sum.thy
"[| u: A+B; \
\ !!x. x: A ==> c(x): C(Inl(x)); \
@@ -187,17 +183,17 @@
qed "Part_mono";
goal Sum.thy "Part(Collect(A,P), h) = Collect(Part(A,h), P)";
-by (fast_tac (!claset addSIs [equalityI]) 1);
+by (Fast_tac 1);
qed "Part_Collect";
bind_thm ("Part_CollectE", Part_Collect RS equalityD1 RS subsetD RS CollectE);
goal Sum.thy "Part(A+B,Inl) = {Inl(x). x: A}";
-by (fast_tac (!claset addIs [equalityI]) 1);
+by (Fast_tac 1);
qed "Part_Inl";
goal Sum.thy "Part(A+B,Inr) = {Inr(y). y: B}";
-by (fast_tac (!claset addIs [equalityI]) 1);
+by (Fast_tac 1);
qed "Part_Inr";
goalw Sum.thy [Part_def] "!!a. a : Part(A,h) ==> a : A";
@@ -205,13 +201,13 @@
qed "PartD1";
goal Sum.thy "Part(A,%x.x) = A";
-by (fast_tac (!claset addIs [equalityI]) 1);
+by (Fast_tac 1);
qed "Part_id";
goal Sum.thy "Part(A+B, %x.Inr(h(x))) = {Inr(y). y: Part(B,h)}";
-by (fast_tac (!claset addIs [equalityI]) 1);
+by (Fast_tac 1);
qed "Part_Inr2";
goal Sum.thy "!!A B C. C <= A+B ==> Part(C,Inl) Un Part(C,Inr) = C";
-by (fast_tac (!claset addIs [equalityI]) 1);
+by (Fast_tac 1);
qed "Part_sum_equality";
--- a/src/ZF/Trancl.ML Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/Trancl.ML Wed Jan 08 15:04:27 1997 +0100
@@ -55,7 +55,7 @@
qed "r_subset_rtrancl";
goal Trancl.thy "field(r^*) = field(r)";
-by (fast_tac (eq_cs addIs [r_into_rtrancl]
+by (fast_tac (!claset addIs [r_into_rtrancl]
addSDs [rtrancl_type RS subsetD]) 1);
qed "rtrancl_field";
--- a/src/ZF/Univ.ML Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/Univ.ML Wed Jan 08 15:04:27 1997 +0100
@@ -122,7 +122,7 @@
goal Univ.thy "Vfrom(A,0) = A";
by (stac Vfrom 1);
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Vfrom_0";
goal Univ.thy "!!i. Ord(i) ==> Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))";
@@ -258,7 +258,7 @@
qed "Inr_in_VLimit";
goal Univ.thy "!!i. Limit(i) ==> Vfrom(C,i)+Vfrom(C,i) <= Vfrom(C,i)";
-by (fast_tac (sum_cs addSIs [Inl_in_VLimit, Inr_in_VLimit]) 1);
+by (fast_tac (!claset addSIs [Inl_in_VLimit, Inr_in_VLimit]) 1);
qed "sum_VLimit";
bind_thm ("sum_subset_VLimit", [sum_mono, sum_VLimit] MRS subset_trans);
@@ -284,7 +284,7 @@
goalw Ordinal.thy [Pair_def,Transset_def]
"!!C. [| <a,b> <= C; Transset(C) |] ==> a: C & b: C";
-by (Fast_tac 1);
+by (Best_tac 1);
qed "Transset_Pair_subset";
goal Univ.thy
@@ -387,7 +387,7 @@
goal Univ.thy "Vset(i) = (UN j:i. Pow(Vset(j)))";
by (stac Vfrom 1);
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Vset";
val Vset_succ = Transset_0 RS Transset_Vfrom_succ;
--- a/src/ZF/ZF.ML Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/ZF.ML Wed Jan 08 15:04:27 1997 +0100
@@ -152,6 +152,8 @@
qed_goal "equalityI" ZF.thy "[| A <= B; B <= A |] ==> A = B"
(fn prems=> [ (REPEAT (resolve_tac (prems@[conjI, extension RS iffD2]) 1)) ]);
+AddIs [equalityI];
+
qed_goal "equality_iffI" ZF.thy "(!!x. x:A <-> x:B) ==> A = B"
(fn [prem] =>
[ (rtac equalityI 1),
@@ -268,7 +270,7 @@
(fn _ => [Fast_tac 1]);
goal ZF.thy "{x.x:A} = A";
-by (fast_tac (!claset addSIs [equalityI]) 1);
+by (fast_tac (!claset) 1);
qed "triv_RepFun";
Addsimps [RepFun_iff, triv_RepFun];
@@ -438,7 +440,7 @@
AddSIs [empty_subsetI];
qed_goal "equals0I" ZF.thy "[| !!y. y:A ==> False |] ==> A=0"
- (fn prems=> [ fast_tac (!claset addIs [equalityI] addDs prems) 1 ]);
+ (fn prems=> [ fast_tac (!claset addDs prems) 1 ]);
qed_goal "equals0D" ZF.thy "!!P. [| A=0; a:A |] ==> P"
(fn _=> [ Full_simp_tac 1, Fast_tac 1 ]);
--- a/src/ZF/Zorn.ML Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/Zorn.ML Wed Jan 08 15:04:27 1997 +0100
@@ -281,7 +281,7 @@
by (subgoal_tac "cons(z,c): super(S,c)" 1);
by (fast_tac (!claset addEs [equalityE]) 1);
by (rewtac super_def);
-by (safe_tac eq_cs);
+by (safe_tac (!claset));
by (fast_tac (!claset addEs [chain_extend]) 1);
by (best_tac (!claset addEs [equalityE]) 1);
qed "Zorn";
@@ -301,7 +301,7 @@
by (REPEAT_SOME (eresolve_tac [asm_rl,subsetD]));
by (subgoal_tac "x = Inter(Z)" 1);
by (Fast_tac 1);
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "TFin_well_lemma5";
(*Well-ordering of TFin(S,next)*)
@@ -334,7 +334,7 @@
by (rtac wf_onI 1);
by (forward_tac [well_ord_TFin_lemma] 1 THEN assume_tac 1);
by (dres_inst_tac [("x","Inter(Z)")] bspec 1 THEN assume_tac 1);
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "well_ord_TFin";
(** Defining the "next" operation for Zermelo's Theorem **)
@@ -343,7 +343,7 @@
"!!S. [| ch : (PROD X:Pow(S) - {0}. X); X<=S; X~=S \
\ |] ==> ch ` (S-X) : S-X";
by (etac apply_type 1);
-by (fast_tac (eq_cs addEs [equalityE]) 1);
+by (fast_tac (!claset addEs [equalityE]) 1);
qed "choice_Diff";
(*This justifies Definition 6.1*)
@@ -392,7 +392,7 @@
\ Union({y: TFin(S,next). x~: y})" 1);
by (asm_simp_tac
(!simpset delsimps [Union_iff]
- addsimps [Collect_subset RS TFin_UnionI RS TFin_is_subset,
+ addsimps [Collect_subset RS TFin_UnionI RS TFin_is_subset,
Pow_iff, cons_subset_iff, subset_refl,
choice_Diff RS DiffD2]
setloop split_tac [expand_if]) 2);
--- a/src/ZF/domrange.ML Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/domrange.ML Wed Jan 08 15:04:27 1997 +0100
@@ -36,16 +36,16 @@
qed_goal "converse_converse" thy
"!!A B r. r<=Sigma(A,B) ==> converse(converse(r)) = r"
- (fn _ => [ (fast_tac (!claset addSIs [equalityI]) 1) ]);
+ (fn _ => [ (Fast_tac 1) ]);
qed_goal "converse_type" thy "!!A B r. r<=A*B ==> converse(r)<=B*A"
(fn _ => [ (Fast_tac 1) ]);
qed_goal "converse_prod" thy "converse(A*B) = B*A"
- (fn _ => [ (fast_tac (!claset addSIs [equalityI]) 1) ]);
+ (fn _ => [ (Fast_tac 1) ]);
qed_goal "converse_empty" thy "converse(0) = 0"
- (fn _ => [ (fast_tac (!claset addSIs [equalityI]) 1) ]);
+ (fn _ => [ (Fast_tac 1) ]);
Addsimps [converse_prod, converse_empty];
@@ -191,9 +191,7 @@
AddIs [vimageI];
AddSEs [vimageE];
-val ZF_cs = !claset;
-
-val eq_cs = ZF_cs addSIs [equalityI];
+val ZF_cs = !claset delrules [equalityI];
(** The Union of a set of relations is a relation -- Lemma for fun_Union **)
goal thy "!!S. (ALL x:S. EX A B. x <= A*B) ==> \
@@ -208,10 +206,10 @@
goal thy "!!r. [| <a,c> : r; c~=b |] ==> domain(r-{<a,b>}) = domain(r)";
-by (deepen_tac eq_cs 0 1);
+by (Deepen_tac 0 1);
qed "domain_Diff_eq";
goal thy "!!r. [| <c,b> : r; c~=a |] ==> range(r-{<a,b>}) = range(r)";
-by (deepen_tac eq_cs 0 1);
+by (Deepen_tac 0 1);
qed "range_Diff_eq";
--- a/src/ZF/equalities.ML Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/equalities.ML Wed Jan 08 15:04:27 1997 +0100
@@ -11,23 +11,23 @@
(* cons_def refers to Upair; reversing the equality LOOPS in rewriting!*)
goal thy "{a} Un B = cons(a,B)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "cons_eq";
goal thy "cons(a, cons(b, C)) = cons(b, cons(a, C))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "cons_commute";
goal thy "!!B. a: B ==> cons(a,B) = B";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "cons_absorb";
goal thy "!!B. a: B ==> cons(a, B-{a}) = B";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "cons_Diff";
goal thy "!!C. [| a: C; ALL y:C. y=b |] ==> C = {b}";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "equal_singleton_lemma";
val equal_singleton = ballI RSN (2,equal_singleton_lemma);
@@ -36,101 +36,101 @@
(*NOT an equality, but it seems to belong here...*)
goal thy "cons(a,B) Int C <= cons(a, B Int C)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Int_cons";
goal thy "A Int A = A";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Int_absorb";
goal thy "A Int B = B Int A";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Int_commute";
goal thy "(A Int B) Int C = A Int (B Int C)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Int_assoc";
goal thy "(A Un B) Int C = (A Int C) Un (B Int C)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Int_Un_distrib";
goal thy "A<=B <-> A Int B = A";
-by (fast_tac (eq_cs addSEs [equalityE]) 1);
+by (fast_tac (!claset addSEs [equalityE]) 1);
qed "subset_Int_iff";
goal thy "A<=B <-> B Int A = A";
-by (fast_tac (eq_cs addSEs [equalityE]) 1);
+by (fast_tac (!claset addSEs [equalityE]) 1);
qed "subset_Int_iff2";
goal thy "!!A B C. C<=A ==> (A-B) Int C = C-B";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Int_Diff_eq";
(** Binary Union **)
goal thy "cons(a,B) Un C = cons(a, B Un C)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Un_cons";
goal thy "A Un A = A";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Un_absorb";
goal thy "A Un B = B Un A";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Un_commute";
goal thy "(A Un B) Un C = A Un (B Un C)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Un_assoc";
goal thy "(A Int B) Un C = (A Un C) Int (B Un C)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Un_Int_distrib";
goal thy "A<=B <-> A Un B = B";
-by (fast_tac (eq_cs addSEs [equalityE]) 1);
+by (fast_tac (!claset addSEs [equalityE]) 1);
qed "subset_Un_iff";
goal thy "A<=B <-> B Un A = B";
-by (fast_tac (eq_cs addSEs [equalityE]) 1);
+by (fast_tac (!claset addSEs [equalityE]) 1);
qed "subset_Un_iff2";
(** Simple properties of Diff -- set difference **)
goal thy "A-A = 0";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Diff_cancel";
goal thy "0-A = 0";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "empty_Diff";
goal thy "A-0 = A";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Diff_0";
goal thy "A-B=0 <-> A<=B";
-by (fast_tac (eq_cs addEs [equalityE]) 1);
+by (fast_tac (!claset addEs [equalityE]) 1);
qed "Diff_eq_0_iff";
(*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*)
goal thy "A - cons(a,B) = A - B - {a}";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Diff_cons";
(*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*)
goal thy "A - cons(a,B) = A - {a} - B";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Diff_cons2";
goal thy "A Int (B-A) = 0";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Diff_disjoint";
goal thy "!!A B. A<=B ==> A Un (B-A) = B";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Diff_partition";
goal thy "A <= B Un (A - B)";
@@ -138,40 +138,40 @@
qed "subset_Un_Diff";
goal thy "!!A B. [| A<=B; B<=C |] ==> B-(C-A) = A";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "double_complement";
goal thy "(A Un B) - (B-A) = A";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "double_complement_Un";
goal thy
"(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Un_Int_crazy";
goal thy "A - (B Un C) = (A-B) Int (A-C)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Diff_Un";
goal thy "A - (B Int C) = (A-B) Un (A-C)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Diff_Int";
(*Halmos, Naive Set Theory, page 16.*)
goal thy "(A Int B) Un C = A Int (B Un C) <-> C<=A";
-by (fast_tac (eq_cs addSEs [equalityE]) 1);
+by (fast_tac (!claset addSEs [equalityE]) 1);
qed "Un_Int_assoc_iff";
(** Big Union and Intersection **)
goal thy "Union(cons(a,B)) = a Un Union(B)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Union_cons";
goal thy "Union(A Un B) = Union(A) Un Union(B)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Union_Un_distrib";
goal thy "Union(A Int B) <= Union(A) Int Union(B)";
@@ -179,11 +179,11 @@
qed "Union_Int_subset";
goal thy "Union(C) Int A = 0 <-> (ALL B:C. B Int A = 0)";
-by (fast_tac (eq_cs addSEs [equalityE]) 1);
+by (fast_tac (!claset addSEs [equalityE]) 1);
qed "Union_disjoint";
goalw thy [Inter_def] "Inter(0) = 0";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Inter_0";
goal thy "!!A B. [| z:A; z:B |] ==> Inter(A) Un Inter(B) <= Inter(A Int B)";
@@ -192,70 +192,70 @@
(* A good challenge: Inter is ill-behaved on the empty set *)
goal thy "!!A B. [| a:A; b:B |] ==> Inter(A Un B) = Inter(A) Int Inter(B)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Inter_Un_distrib";
goal thy "Union({b}) = b";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Union_singleton";
goal thy "Inter({b}) = b";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Inter_singleton";
(** Unions and Intersections of Families **)
goal thy "Union(A) = (UN x:A. x)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Union_eq_UN";
goalw thy [Inter_def] "Inter(A) = (INT x:A. x)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Inter_eq_INT";
goal thy "(UN i:0. A(i)) = 0";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "UN_0";
(*Halmos, Naive Set Theory, page 35.*)
goal thy "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Int_UN_distrib";
goal thy "!!A B. i:I ==> B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Un_INT_distrib";
goal thy
"(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Int_UN_distrib2";
goal thy
"!!I J. [| i:I; j:J |] ==> \
\ (INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Un_INT_distrib2";
goal thy "!!A. a: A ==> (UN y:A. c) = c";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "UN_constant";
goal thy "!!A. a: A ==> (INT y:A. c) = c";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "INT_constant";
(** Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5:
Union of a family of unions **)
goal thy "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i)) Un (UN i:I. B(i))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "UN_Un_distrib";
goal thy
"!!A B. i:I ==> \
\ (INT i:I. A(i) Int B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "INT_Int_distrib";
goal thy "(UN z:I Int J. A(z)) <= (UN z:I. A(z)) Int (UN z:J. A(z))";
@@ -265,47 +265,47 @@
(** Devlin, page 12, exercise 5: Complements **)
goal thy "!!A B. i:I ==> B - (UN i:I. A(i)) = (INT i:I. B - A(i))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Diff_UN";
goal thy "!!A B. i:I ==> B - (INT i:I. A(i)) = (UN i:I. B - A(i))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Diff_INT";
(** Unions and Intersections with General Sum **)
(*Not suitable for rewriting: LOOPS!*)
goal thy "Sigma(cons(a,B), C) = ({a}*C(a)) Un Sigma(B,C)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Sigma_cons1";
(*Not suitable for rewriting: LOOPS!*)
goal thy "A * cons(b,B) = A*{b} Un A*B";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Sigma_cons2";
goal thy "Sigma(succ(A), B) = ({A}*B(A)) Un Sigma(A,B)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Sigma_succ1";
goal thy "A * succ(B) = A*{B} Un A*B";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Sigma_succ2";
goal thy "(SUM x:(UN y:A. C(y)). B(x)) = (UN y:A. SUM x:C(y). B(x))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "SUM_UN_distrib1";
goal thy "(SUM i:I. UN j:J. C(i,j)) = (UN j:J. SUM i:I. C(i,j))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "SUM_UN_distrib2";
goal thy "(SUM i:I Un J. C(i)) = (SUM i:I. C(i)) Un (SUM j:J. C(j))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "SUM_Un_distrib1";
goal thy "(SUM i:I. A(i) Un B(i)) = (SUM i:I. A(i)) Un (SUM i:I. B(i))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "SUM_Un_distrib2";
(*First-order version of the above, for rewriting*)
@@ -314,12 +314,12 @@
qed "prod_Un_distrib2";
goal thy "(SUM i:I Int J. C(i)) = (SUM i:I. C(i)) Int (SUM j:J. C(j))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "SUM_Int_distrib1";
goal thy
"(SUM i:I. A(i) Int B(i)) = (SUM i:I. A(i)) Int (SUM i:I. B(i))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "SUM_Int_distrib2";
(*First-order version of the above, for rewriting*)
@@ -329,35 +329,35 @@
(*Cf Aczel, Non-Well-Founded Sets, page 115*)
goal thy "(SUM i:I. A(i)) = (UN i:I. {i} * A(i))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "SUM_eq_UN";
(** Domain **)
qed_goal "domain_of_prod" thy "!!A B. b:B ==> domain(A*B) = A"
- (fn _ => [ fast_tac eq_cs 1 ]);
+ (fn _ => [ Fast_tac 1 ]);
qed_goal "domain_0" thy "domain(0) = 0"
- (fn _ => [ fast_tac eq_cs 1 ]);
+ (fn _ => [ Fast_tac 1 ]);
qed_goal "domain_cons" thy
"domain(cons(<a,b>,r)) = cons(a, domain(r))"
- (fn _ => [ fast_tac eq_cs 1 ]);
+ (fn _ => [ Fast_tac 1 ]);
goal thy "domain(A Un B) = domain(A) Un domain(B)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "domain_Un_eq";
goal thy "domain(A Int B) <= domain(A) Int domain(B)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "domain_Int_subset";
goal thy "domain(A) - domain(B) <= domain(A - B)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "domain_Diff_subset";
goal thy "domain(converse(r)) = range(r)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "domain_converse";
Addsimps [domain_0, domain_cons, domain_Un_eq, domain_converse];
@@ -367,17 +367,17 @@
qed_goal "range_of_prod" thy
"!!a A B. a:A ==> range(A*B) = B"
- (fn _ => [ fast_tac eq_cs 1 ]);
+ (fn _ => [ Fast_tac 1 ]);
qed_goal "range_0" thy "range(0) = 0"
- (fn _ => [ fast_tac eq_cs 1 ]);
+ (fn _ => [ Fast_tac 1 ]);
qed_goal "range_cons" thy
"range(cons(<a,b>,r)) = cons(b, range(r))"
- (fn _ => [ fast_tac eq_cs 1 ]);
+ (fn _ => [ Fast_tac 1 ]);
goal thy "range(A Un B) = range(A) Un range(B)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "range_Un_eq";
goal thy "range(A Int B) <= range(A) Int range(B)";
@@ -385,11 +385,11 @@
qed "range_Int_subset";
goal thy "range(A) - range(B) <= range(A - B)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "range_Diff_subset";
goal thy "range(converse(r)) = domain(r)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "range_converse";
Addsimps [range_0, range_cons, range_Un_eq, range_converse];
@@ -398,29 +398,29 @@
(** Field **)
qed_goal "field_of_prod" thy "field(A*A) = A"
- (fn _ => [ fast_tac eq_cs 1 ]);
+ (fn _ => [ Fast_tac 1 ]);
qed_goal "field_0" thy "field(0) = 0"
- (fn _ => [ fast_tac eq_cs 1 ]);
+ (fn _ => [ Fast_tac 1 ]);
qed_goal "field_cons" thy
"field(cons(<a,b>,r)) = cons(a, cons(b, field(r)))"
(fn _ => [ rtac equalityI 1, ALLGOALS (Fast_tac) ]);
goal thy "field(A Un B) = field(A) Un field(B)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "field_Un_eq";
goal thy "field(A Int B) <= field(A) Int field(B)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "field_Int_subset";
goal thy "field(A) - field(B) <= field(A - B)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "field_Diff_subset";
goal thy "field(converse(r)) = field(r)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "field_converse";
Addsimps [field_0, field_cons, field_Un_eq, field_converse];
@@ -429,11 +429,11 @@
(** Image **)
goal thy "r``0 = 0";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "image_0";
goal thy "r``(A Un B) = (r``A) Un (r``B)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "image_Un";
goal thy "r``(A Int B) <= (r``A) Int (r``B)";
@@ -445,7 +445,7 @@
qed "image_Int_square_subset";
goal thy "!!r. B<=A ==> (r Int A*A)``B = (r``B) Int A";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "image_Int_square";
Addsimps [image_0, image_Un];
@@ -454,11 +454,11 @@
(** Inverse Image **)
goal thy "r-``0 = 0";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "vimage_0";
goal thy "r-``(A Un B) = (r-``A) Un (r-``B)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "vimage_Un";
goal thy "r-``(A Int B) <= (r-``A) Int (r-``B)";
@@ -470,7 +470,7 @@
qed "vimage_Int_square_subset";
goal thy "!!r. B<=A ==> (r Int A*A)-``B = (r-``B) Int A";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "vimage_Int_square";
Addsimps [vimage_0, vimage_Un];
@@ -479,24 +479,24 @@
(** Converse **)
goal thy "converse(A Un B) = converse(A) Un converse(B)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "converse_Un";
goal thy "converse(A Int B) = converse(A) Int converse(B)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "converse_Int";
goal thy "converse(A - B) = converse(A) - converse(B)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "converse_Diff";
goal thy "converse(UN x:A. B(x)) = (UN x:A. converse(B(x)))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "converse_UN";
(*Unfolding Inter avoids using excluded middle on A=0*)
goalw thy [Inter_def] "converse(INT x:A. B(x)) = (INT x:A. converse(B(x)))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "converse_INT";
Addsimps [converse_Un, converse_Int, converse_Diff, converse_UN, converse_INT];
@@ -516,15 +516,15 @@
qed "subset_Pow_Union";
goal thy "Union(Pow(A)) = A";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Union_Pow_eq";
goal thy "Pow(A Int B) = Pow(A) Int Pow(B)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Int_Pow_eq";
goal thy "!!x A. x:A ==> (INT x:A. Pow(B(x))) = Pow(INT x:A. B(x))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "INT_Pow_subset";
Addsimps [Union_Pow_eq, Int_Pow_eq];
@@ -532,25 +532,25 @@
(** RepFun **)
goal thy "{f(x).x:A}=0 <-> A=0";
-by (fast_tac (eq_cs addSEs [equalityE]) 1);
+by (fast_tac (!claset addSEs [equalityE]) 1);
qed "RepFun_eq_0_iff";
(** Collect **)
goal thy "Collect(A Un B, P) = Collect(A,P) Un Collect(B,P)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Collect_Un";
goal thy "Collect(A Int B, P) = Collect(A,P) Int Collect(B,P)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Collect_Int";
goal thy "Collect(A - B, P) = Collect(A,P) - Collect(B,P)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Collect_Diff";
goal thy "{x:cons(a,B). P(x)} = if(P(a), cons(a, {x:B. P(x)}), {x:B. P(x)})";
by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Collect_cons";
--- a/src/ZF/ex/Brouwer.ML Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/ex/Brouwer.ML Wed Jan 08 15:04:27 1997 +0100
@@ -14,7 +14,7 @@
goal Brouwer.thy "brouwer = {0} + brouwer + (nat -> brouwer)";
let open brouwer; val rew = rewrite_rule con_defs in
-by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs)
+by (fast_tac (!claset addSIs (equalityI :: map rew intrs)
addEs [rew elim]) 1)
end;
qed "brouwer_unfold";
@@ -38,7 +38,7 @@
goal Brouwer.thy "Well(A,B) = (SUM x:A. B(x) -> Well(A,B))";
let open Well; val rew = rewrite_rule con_defs in
-by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs)
+by (fast_tac (!claset addSIs (equalityI :: map rew intrs)
addEs [rew elim]) 1)
end;
qed "Well_unfold";
--- a/src/ZF/ex/Data.ML Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/ex/Data.ML Wed Jan 08 15:04:27 1997 +0100
@@ -11,7 +11,7 @@
goal Data.thy "data(A,B) = ({0} + A) + (A*B + A*B*data(A,B))";
let open data; val rew = rewrite_rule con_defs in
-by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs)
+by (fast_tac (!claset addSIs (equalityI :: map rew intrs)
addEs [rew elim]) 1)
end;
qed "data_unfold";
--- a/src/ZF/ex/Mutil.ML Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/ex/Mutil.ML Wed Jan 08 15:04:27 1997 +0100
@@ -12,7 +12,7 @@
(** Basic properties of evnodd **)
goalw thy [evnodd_def] "<i,j>: evnodd(A,b) <-> <i,j>: A & (i#+j) mod 2 = b";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "evnodd_iff";
goalw thy [evnodd_def] "evnodd(A, b) <= A";
@@ -103,16 +103,16 @@
by (assume_tac 2);
by (subgoal_tac (*seems the easiest way of turning one to the other*)
"{i}*{succ(n1#+n1)} Un {i}*{n1#+n1} = {<i,n1#+n1>, <i,succ(n1#+n1)>}" 1);
-by (fast_tac eq_cs 2);
+by (Fast_tac 2);
by (asm_simp_tac (!simpset addsimps [domino.horiz]) 1);
-by (fast_tac (eq_cs addEs [mem_irrefl, mem_asym]) 1);
+by (fast_tac (!claset addEs [mem_irrefl, mem_asym]) 1);
qed "dominoes_tile_row";
goal thy "!!m n. [| m: nat; n: nat |] ==> m * (n #+ n) : tiling(domino)";
by (nat_ind_tac "m" [] 1);
by (simp_tac (!simpset addsimps tiling.intrs) 1);
by (asm_simp_tac (!simpset addsimps [Sigma_succ1]) 1);
-by (fast_tac (eq_cs addIs [tiling_UnI, dominoes_tile_row]
+by (fast_tac (!claset addIs [tiling_UnI, dominoes_tile_row]
addEs [mem_irrefl]) 1);
qed "dominoes_tile_matrix";
--- a/src/ZF/ex/Ntree.ML Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/ex/Ntree.ML Wed Jan 08 15:04:27 1997 +0100
@@ -15,7 +15,7 @@
goal Ntree.thy "ntree(A) = A * (UN n: nat. n -> ntree(A))";
let open ntree; val rew = rewrite_rule con_defs in
-by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs)
+by (fast_tac (!claset addSIs (equalityI :: map rew intrs)
addEs [rew elim]) 1)
end;
qed "ntree_unfold";
@@ -70,7 +70,7 @@
goal Ntree.thy "maptree(A) = A * (maptree(A) -||> maptree(A))";
let open maptree; val rew = rewrite_rule con_defs in
-by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs)
+by (fast_tac (!claset addSIs (equalityI :: map rew intrs)
addEs [rew elim]) 1)
end;
qed "maptree_unfold";
@@ -95,7 +95,7 @@
goal Ntree.thy "maptree2(A,B) = A * (B -||> maptree2(A,B))";
let open maptree2; val rew = rewrite_rule con_defs in
-by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs)
+by (fast_tac (!claset addSIs (equalityI :: map rew intrs)
addEs [rew elim]) 1)
end;
qed "maptree2_unfold";
--- a/src/ZF/ex/TF.ML Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/ex/TF.ML Wed Jan 08 15:04:27 1997 +0100
@@ -38,7 +38,7 @@
"tree_forest(A) = (A*forest(A)) + ({0} + tree(A)*forest(A))";
let open tree_forest;
val rew = rewrite_rule (con_defs @ tl defs) in
-by (fast_tac (sum_cs addSIs (equalityI :: (map rew intrs RL [PartD1]))
+by (fast_tac (!claset addSIs (equalityI :: (map rew intrs RL [PartD1]))
addEs [rew elim]) 1)
end;
qed "tree_forest_unfold";
--- a/src/ZF/ex/Term.ML Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/ex/Term.ML Wed Jan 08 15:04:27 1997 +0100
@@ -11,7 +11,7 @@
goal Term.thy "term(A) = A * list(term(A))";
let open term; val rew = rewrite_rule con_defs in
-by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs)
+by (fast_tac (!claset addSIs (equalityI :: map rew intrs)
addEs [rew elim]) 1)
end;
qed "term_unfold";
--- a/src/ZF/func.ML Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/func.ML Wed Jan 08 15:04:27 1997 +0100
@@ -53,11 +53,11 @@
(*Empty function spaces*)
goalw thy [Pi_def, function_def] "Pi(0,A) = {0}";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Pi_empty1";
goalw thy [Pi_def] "!!A a. a:A ==> A->0 = 0";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Pi_empty2";
(*The empty function*)
@@ -67,7 +67,7 @@
(*The singleton function*)
goalw thy [Pi_def, function_def] "{<a,b>} : {a} -> {b}";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "singleton_fun";
Addsimps [empty_fun, singleton_fun];
@@ -245,7 +245,7 @@
(** Images of functions **)
goalw thy [lam_def] "!!C A. C <= A ==> (lam x:A.b(x)) `` C = {b(x). x:C}";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "image_lam";
goal thy "!!C A. [| f : Pi(A,B); C <= A |] ==> f``C = {f`x. x:C}";
@@ -291,7 +291,7 @@
qed "restrict_eqI";
goalw thy [restrict_def, lam_def] "domain(restrict(f,C)) = C";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "domain_restrict";
val [prem] = goalw thy [restrict_def]
@@ -360,7 +360,7 @@
(** Domain and range of a function/relation **)
goalw thy [Pi_def] "!!f. f : Pi(A,B) ==> domain(f)=A";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "domain_of_fun";
goal thy "!!f. [| f : Pi(A,B); a: A |] ==> f`a : range(f)";
@@ -379,7 +379,7 @@
"!!f A B. [| f: A->B; c~:A |] ==> cons(<c,b>,f) : cons(c,A) -> cons(b,B)";
by (forward_tac [singleton_fun RS fun_disjoint_Un] 1);
by (asm_full_simp_tac (FOL_ss addsimps [cons_eq]) 2);
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "fun_extend";
goal thy
@@ -417,6 +417,6 @@
by (etac consE 1);
by (ALLGOALS
(asm_simp_tac (!simpset addsimps [restrict, fun_extend_apply1,
- fun_extend_apply2])));
+ fun_extend_apply2])));
qed "cons_fun_eq";
--- a/src/ZF/pair.ML Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/pair.ML Wed Jan 08 15:04:27 1997 +0100
@@ -99,10 +99,10 @@
AddSEs [SigmaE2, SigmaE];
qed_goal "Sigma_empty1" thy "Sigma(0,B) = 0"
- (fn _ => [ (fast_tac (!claset addIs [equalityI]) 1) ]);
+ (fn _ => [ (Fast_tac 1) ]);
qed_goal "Sigma_empty2" thy "A*0 = 0"
- (fn _ => [ (fast_tac (!claset addIs [equalityI]) 1) ]);
+ (fn _ => [ (Fast_tac 1) ]);
Addsimps [Sigma_empty1, Sigma_empty2];
--- a/src/ZF/subset.ML Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/subset.ML Wed Jan 08 15:04:27 1997 +0100
@@ -23,7 +23,7 @@
bind_thm ("cons_subsetE", cons_subset_iff RS iffD1 RS conjE);
qed_goal "subset_empty_iff" thy "A<=0 <-> A=0"
- (fn _=> [ (fast_tac (!claset addIs [equalityI]) 1) ]);
+ (fn _=> [ (Fast_tac 1) ]);
qed_goal "subset_cons_iff" thy
"C<=cons(a,B) <-> C<=B | (a:C & C-{a} <= B)"
@@ -73,7 +73,7 @@
(*** Union of a family of sets ***)
goal thy "A <= (UN i:I. B(i)) <-> A = (UN i:I. A Int B(i))";
-by (fast_tac (!claset addSIs [equalityI] addSEs [equalityE]) 1);
+by (fast_tac (!claset addSEs [equalityE]) 1);
qed "subset_UN_iff_eq";
qed_goal "UN_subset_iff" thy
--- a/src/ZF/upair.ML Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/upair.ML Wed Jan 08 15:04:27 1997 +0100
@@ -198,8 +198,7 @@
qed_goalw "the_equality" thy [the_def]
"[| P(a); !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a"
(fn [pa,eq] =>
- [ (fast_tac (!claset addSIs [pa] addIs [equalityI]
- addEs [eq RS subst]) 1) ]);
+ [ (fast_tac (!claset addSIs [pa] addEs [eq RS subst]) 1) ]);
(* Only use this if you already know EX!x. P(x) *)
qed_goal "the_equality2" thy
@@ -226,7 +225,7 @@
(*If it's "undefined", it's zero!*)
qed_goalw "the_0" thy [the_def]
"!!P. ~ (EX! x. P(x)) ==> (THE x. P(x))=0"
- (fn _ => [ (fast_tac (!claset addIs [equalityI] addSEs [ReplaceE]) 1) ]);
+ (fn _ => [ (fast_tac (!claset addSEs [ReplaceE]) 1) ]);
(*** if -- a conditional expression for formulae ***)