Classical tactics now use default claset.
--- a/src/HOL/ex/Acc.ML Fri Jun 21 11:57:00 1996 +0200
+++ b/src/HOL/ex/Acc.ML Fri Jun 21 12:18:50 1996 +0200
@@ -14,14 +14,14 @@
(*The intended introduction rule*)
val prems = goal Acc.thy
"[| !!b. (b,a):r ==> b: acc(r) |] ==> a: acc(r)";
-by (fast_tac (set_cs addIs (prems @
+by (fast_tac (!claset addIs (prems @
map (rewrite_rule [pred_def]) acc.intrs)) 1);
qed "accI";
goal Acc.thy "!!a b r. [| b: acc(r); (a,b): r |] ==> a: acc(r)";
by (etac acc.elim 1);
by (rewtac pred_def);
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
qed "acc_downward";
val [major,indhyp] = goal Acc.thy
@@ -32,7 +32,7 @@
by (rtac indhyp 1);
by (resolve_tac acc.intrs 1);
by (rewtac pred_def);
-by (fast_tac set_cs 2);
+by (Fast_tac 2);
by (etac (Int_lower1 RS Pow_mono RS subsetD) 1);
qed "acc_induct";
@@ -41,20 +41,20 @@
by (rtac (major RS wfI) 1);
by (etac acc.induct 1);
by (rewtac pred_def);
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
qed "acc_wfI";
val [major] = goal Acc.thy "wf(r) ==> ALL x. (x,y): r | (y,x):r --> y: acc(r)";
by (rtac (major RS wf_induct) 1);
by (rtac (impI RS allI) 1);
by (rtac accI 1);
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
qed "acc_wfD_lemma";
val [major] = goal Acc.thy "wf(r) ==> r <= (acc r) Times (acc r)";
by (rtac subsetI 1);
by (res_inst_tac [("p", "x")] PairE 1);
-by (fast_tac (set_cs addSIs [SigmaI,
+by (fast_tac (!claset addSIs [SigmaI,
major RS acc_wfD_lemma RS spec RS mp]) 1);
qed "acc_wfD";
--- a/src/HOL/ex/Comb.ML Fri Jun 21 11:57:00 1996 +0200
+++ b/src/HOL/ex/Comb.ML Fri Jun 21 12:18:50 1996 +0200
@@ -29,8 +29,8 @@
"!!r. [| diamond(r); (x,y):r^* |] ==> \
\ ALL y'. (x,y'):r --> (EX z. (y',z): r^* & (y,z): r)";
by (etac rtrancl_induct 1);
-by (fast_tac (HOL_cs addIs [rtrancl_refl]) 1);
-by (slow_best_tac (set_cs addIs [r_into_rtrancl RSN (2, rtrancl_trans)]
+by (fast_tac (!claset addIs [rtrancl_refl]) 1);
+by (slow_best_tac (!claset addIs [r_into_rtrancl RSN (2, rtrancl_trans)]
addSDs [spec_mp]) 1);
val diamond_strip_lemmaE = result() RS spec RS mp RS exE;
@@ -38,9 +38,9 @@
by (rewtac diamond_def); (*unfold only in goal, not in premise!*)
by (rtac (impI RS allI RS allI) 1);
by (etac rtrancl_induct 1);
-by (fast_tac (set_cs addIs [rtrancl_refl]) 1);
+by (fast_tac (!claset addIs [rtrancl_refl]) 1);
by (ALLGOALS
- (slow_best_tac (set_cs addIs [r_into_rtrancl, rtrancl_trans]
+ (slow_best_tac ((claset_of "Fun") addIs [r_into_rtrancl, rtrancl_trans]
addEs [major RS diamond_strip_lemmaE])));
qed "diamond_rtrancl";
@@ -54,30 +54,29 @@
val S_contractE = contract.mk_cases comb.simps "S -1-> z";
val Ap_contractE = contract.mk_cases comb.simps "x#y -1-> z";
-val contract_cs =
- HOL_cs addIs contract.intrs
- addSEs [K_contractE, S_contractE, Ap_contractE]
- addss (HOL_ss addsimps comb.simps);
+AddIs contract.intrs;
+AddSEs [K_contractE, S_contractE, Ap_contractE];
+Addss (HOL_ss addsimps comb.simps);
goalw Comb.thy [I_def] "!!z. I -1-> z ==> P";
-by (fast_tac contract_cs 1);
+by (Fast_tac 1);
qed "I_contract_E";
(*Unused*)
goal Comb.thy "!!x z. K#x -1-> z ==> (EX y. z = K#y & x -1-> y)";
-by (fast_tac contract_cs 1);
+by (Fast_tac 1);
qed "K1_contractD";
goal Comb.thy "!!x z. x ---> y ==> x#z ---> y#z";
by (etac rtrancl_induct 1);
by (rtac rtrancl_refl 1);
-by (fast_tac (contract_cs addIs [r_into_rtrancl, rtrancl_trans]) 1);
+by (fast_tac (!claset addIs [r_into_rtrancl, rtrancl_trans]) 1);
qed "Ap_reduce1";
goal Comb.thy "!!x z. x ---> y ==> z#x ---> z#y";
by (etac rtrancl_induct 1);
by (rtac rtrancl_refl 1);
-by (fast_tac (contract_cs addIs [r_into_rtrancl, rtrancl_trans]) 1);
+by (fast_tac (!claset addIs [r_into_rtrancl, rtrancl_trans]) 1);
qed "Ap_reduce2";
(** Counterexample to the diamond property for -1-> **)
@@ -87,15 +86,15 @@
qed "KIII_contract1";
goalw Comb.thy [I_def] "K#I#(I#I) -1-> K#I#((K#I)#(K#I))";
-by (fast_tac contract_cs 1);
+by (Fast_tac 1);
qed "KIII_contract2";
goal Comb.thy "K#I#((K#I)#(K#I)) -1-> I";
-by (fast_tac contract_cs 1);
+by (Fast_tac 1);
qed "KIII_contract3";
goalw Comb.thy [diamond_def] "~ diamond(contract)";
-by (fast_tac (HOL_cs addIs [KIII_contract1,KIII_contract2,KIII_contract3]
+by (fast_tac (!claset addIs [KIII_contract1,KIII_contract2,KIII_contract3]
addSEs [I_contract_E]) 1);
qed "not_diamond_contract";
@@ -108,25 +107,23 @@
val S_parcontractE = parcontract.mk_cases comb.simps "S =1=> z";
val Ap_parcontractE = parcontract.mk_cases comb.simps "x#y =1=> z";
-val parcontract_cs =
- HOL_cs addIs parcontract.intrs
- addSEs [K_parcontractE, S_parcontractE,
- Ap_parcontractE]
- addss (HOL_ss addsimps comb.simps);
+AddIs parcontract.intrs;
+AddSEs [K_parcontractE, S_parcontractE,Ap_parcontractE];
+Addss (HOL_ss addsimps comb.simps);
(*** Basic properties of parallel contraction ***)
goal Comb.thy "!!x z. K#x =1=> z ==> (EX x'. z = K#x' & x =1=> x')";
-by (fast_tac parcontract_cs 1);
+by (Fast_tac 1);
qed "K1_parcontractD";
goal Comb.thy "!!x z. S#x =1=> z ==> (EX x'. z = S#x' & x =1=> x')";
-by (fast_tac parcontract_cs 1);
+by (Fast_tac 1);
qed "S1_parcontractD";
goal Comb.thy
"!!x y z. S#x#y =1=> z ==> (EX x' y'. z = S#x'#y' & x =1=> x' & y =1=> y')";
-by (fast_tac (parcontract_cs addSDs [S1_parcontractD]) 1);
+by (fast_tac (!claset addSDs [S1_parcontractD]) 1);
(*the extra rule makes the proof more than twice as fast*)
qed "S2_parcontractD";
@@ -135,7 +132,7 @@
by (rtac (impI RS allI RS allI) 1);
by (etac parcontract.induct 1 THEN prune_params_tac);
by (ALLGOALS
- (fast_tac (parcontract_cs addSDs [K1_parcontractD,S2_parcontractD])));
+ (fast_tac (!claset addSDs [K1_parcontractD,S2_parcontractD])));
qed "diamond_parcontract";
@@ -145,26 +142,26 @@
by (rtac subsetI 1);
by (split_all_tac 1);
by (etac contract.induct 1);
-by (ALLGOALS (fast_tac (parcontract_cs)));
+by (ALLGOALS (Fast_tac));
qed "contract_subset_parcontract";
(*Reductions: simply throw together reflexivity, transitivity and
the one-step reductions*)
-val reduce_cs = contract_cs
- addIs [rtrancl_refl, r_into_rtrancl,
+
+AddIs [rtrancl_refl, r_into_rtrancl,
contract.K, contract.S, Ap_reduce1, Ap_reduce2,
rtrancl_trans];
(*Example only: not used*)
goalw Comb.thy [I_def] "I#x ---> x";
-by (best_tac reduce_cs 1);
+by (best_tac (!claset) 1);
qed "reduce_I";
goal Comb.thy "parcontract <= contract^*";
by (rtac subsetI 1);
by (split_all_tac 1);
by (etac parcontract.induct 1 THEN prune_params_tac);
-by (ALLGOALS (deepen_tac reduce_cs 0));
+by (ALLGOALS (deepen_tac (!claset) 0));
qed "parcontract_subset_reduce";
goal Comb.thy "contract^* = parcontract^*";
--- a/src/HOL/ex/InSort.ML Fri Jun 21 11:57:00 1996 +0200
+++ b/src/HOL/ex/InSort.ML Fri Jun 21 12:18:50 1996 +0200
@@ -8,19 +8,19 @@
goalw InSort.thy [Sorting.total_def]
"!!f. [| total(f); ~f x y |] ==> f y x";
-by(fast_tac HOL_cs 1);
+by(Fast_tac 1);
qed "totalD";
goalw InSort.thy [Sorting.transf_def]
"!!f. [| transf(f); f b a |] ==> !x. f a x --> f b x";
-by(fast_tac HOL_cs 1);
+by(Fast_tac 1);
qed "transfD";
goal InSort.thy "list_all p (ins f x xs) = (list_all p xs & p(x))";
by(list.induct_tac "xs" 1);
by(Asm_simp_tac 1);
by(asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
-by(fast_tac HOL_cs 1);
+by(Fast_tac 1);
Addsimps [result()];
goal InSort.thy "(!x. p(x) --> q(x)) --> list_all p xs --> list_all q xs";
@@ -34,7 +34,7 @@
by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
by(cut_facts_tac prems 1);
by(cut_inst_tac [("p","f(a)"),("q","f(x)")] list_all_imp 1);
-by(fast_tac (HOL_cs addDs [totalD,transfD]) 1);
+by(fast_tac (!claset addDs [totalD,transfD]) 1);
Addsimps [result()];
goal InSort.thy "!!f. [| total(f); transf(f) |] ==> sorted f (insort f xs)";
--- a/src/HOL/ex/LList.ML Fri Jun 21 11:57:00 1996 +0200
+++ b/src/HOL/ex/LList.ML Fri Jun 21 12:18:50 1996 +0200
@@ -27,7 +27,7 @@
goal LList.thy "llist(A) = {Numb(0)} <+> (A <*> llist(A))";
let val rew = rewrite_rule [NIL_def, CONS_def] in
-by (fast_tac (univ_cs addSIs (equalityI :: map rew llist.intrs)
+by (fast_tac (!claset addSIs (equalityI :: map rew llist.intrs)
addEs [rew llist.elim]) 1)
end;
qed "llist_unfold";
@@ -45,12 +45,12 @@
qed "llist_coinduct";
goalw LList.thy [list_Fun_def, NIL_def] "NIL: list_Fun A X";
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
qed "list_Fun_NIL_I";
goalw LList.thy [list_Fun_def,CONS_def]
"!!M N. [| M: A; N: X |] ==> CONS M N : list_Fun A X";
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
qed "list_Fun_CONS_I";
(*Utilise the "strong" part, i.e. gfp(f)*)
@@ -99,7 +99,7 @@
"sum_case (%u.NIL) (split(%z w. CONS z (LList_corec w f))) (f a) <= \
\ LList_corec a f";
by (simp_tac (!simpset addsimps [CONS_UN1]) 1);
-by (safe_tac set_cs);
+by (safe_tac (!claset));
by (ALLGOALS (res_inst_tac [("x","Suc(?k)")] UN1_I THEN' Asm_simp_tac));
qed "LList_corec_subset2";
@@ -124,7 +124,7 @@
goal LList.thy "LList_corec a f : llist({u.True})";
by (res_inst_tac [("X", "range(%x.LList_corec x ?g)")] llist_coinduct 1);
by (rtac rangeI 1);
-by (safe_tac set_cs);
+by (safe_tac (!claset));
by (stac LList_corec 1);
by (simp_tac (!simpset addsimps [list_Fun_NIL_I, list_Fun_CONS_I, CollectI]
|> add_eqI) 1);
@@ -136,10 +136,10 @@
\ llist(range Leaf)";
by (res_inst_tac [("X", "range(%x.LList_corec x ?g)")] llist_coinduct 1);
by (rtac rangeI 1);
-by (safe_tac set_cs);
+by (safe_tac (!claset));
by (stac LList_corec 1);
by (asm_simp_tac (!simpset addsimps [list_Fun_NIL_I]) 1);
-by (fast_tac (set_cs addSIs [list_Fun_CONS_I]) 1);
+by (fast_tac (!claset addSIs [list_Fun_CONS_I]) 1);
qed "LList_corec_type2";
@@ -148,16 +148,16 @@
(*This theorem is actually used, unlike the many similar ones in ZF*)
goal LList.thy "LListD(r) = diag({Numb(0)}) <++> (r <**> LListD(r))";
let val rew = rewrite_rule [NIL_def, CONS_def] in
-by (fast_tac (univ_cs addSIs (equalityI :: map rew LListD.intrs)
+by (fast_tac (!claset addSIs (equalityI :: map rew LListD.intrs)
addEs [rew LListD.elim]) 1)
end;
qed "LListD_unfold";
goal LList.thy "!M N. (M,N) : LListD(diag(A)) --> ntrunc k M = ntrunc k N";
by (res_inst_tac [("n", "k")] less_induct 1);
-by (safe_tac set_cs);
+by (safe_tac ((claset_of "Fun") delrules [equalityI]));
by (etac LListD.elim 1);
-by (safe_tac (prod_cs addSEs [diagE]));
+by (safe_tac (((claset_of "Prod") delrules [equalityI]) addSEs [diagE]));
by (res_inst_tac [("n", "n")] natE 1);
by (asm_simp_tac (!simpset addsimps [ntrunc_0]) 1);
by (rename_tac "n'" 1);
@@ -173,14 +173,14 @@
(*avoids unfolding LListD on the rhs*)
by (res_inst_tac [("P", "%x. fst``x <= ?B")] (LListD_unfold RS ssubst) 1);
by (Simp_tac 1);
-by (fast_tac univ_cs 1);
+by (Fast_tac 1);
qed "fst_image_LListD";
(*This inclusion justifies the use of coinduction to show M=N*)
goal LList.thy "LListD(diag(A)) <= diag(llist(A))";
by (rtac subsetI 1);
by (res_inst_tac [("p","x")] PairE 1);
-by (safe_tac HOL_cs);
+by (safe_tac (!claset));
by (rtac diag_eqI 1);
by (rtac (LListD_implies_ntrunc_equality RS spec RS spec RS mp RS
ntrunc_equality) 1);
@@ -200,12 +200,12 @@
qed "LListD_coinduct";
goalw LList.thy [LListD_Fun_def,NIL_def] "(NIL,NIL) : LListD_Fun r s";
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
qed "LListD_Fun_NIL_I";
goalw LList.thy [LListD_Fun_def,CONS_def]
"!!x. [| x:A; (M,N):s |] ==> (CONS x M, CONS x N) : LListD_Fun (diag A) s";
-by (fast_tac univ_cs 1);
+by (Fast_tac 1);
qed "LListD_Fun_CONS_I";
(*Utilise the "strong" part, i.e. gfp(f)*)
@@ -250,7 +250,7 @@
by (rtac (LListD_subset_diag RS subsetD RS diagE) 1);
by (etac LListD_coinduct 1);
by (asm_simp_tac (!simpset addsimps [LListD_eq_diag]) 1);
-by (safe_tac prod_cs);
+by (safe_tac (!claset));
qed "LList_equalityI";
@@ -266,7 +266,7 @@
by (res_inst_tac [("A", "{u.True}"),
("r", "range(%u. (h1(u),h2(u)))")] LList_equalityI 1);
by (rtac rangeI 1);
-by (safe_tac set_cs);
+by (safe_tac (!claset));
by (stac prem1 1);
by (stac prem2 1);
by (simp_tac (!simpset addsimps [LListD_Fun_NIL_I,
@@ -324,7 +324,7 @@
The containing set is simply the singleton {Lconst(M)}. *)
goal LList.thy "!!M A. M:A ==> Lconst(M): llist(A)";
by (rtac (singletonI RS llist_coinduct) 1);
-by (safe_tac set_cs);
+by (safe_tac (!claset));
by (res_inst_tac [("P", "%u. u: ?A")] (Lconst RS ssubst) 1);
by (REPEAT (ares_tac [list_Fun_CONS_I, singletonI, UnI1] 1));
qed "Lconst_type";
@@ -383,27 +383,28 @@
(** Injectiveness of CONS and LCons **)
goalw LList.thy [CONS_def] "(CONS M N=CONS M' N') = (M=M' & N=N')";
-by (fast_tac (HOL_cs addSEs [Scons_inject, make_elim In1_inject]) 1);
+by (fast_tac (!claset addSEs [Scons_inject, make_elim In1_inject]) 1);
qed "CONS_CONS_eq2";
bind_thm ("CONS_inject", (CONS_CONS_eq RS iffD1 RS conjE));
(*For reasoning about abstract llist constructors*)
-val llist_cs = set_cs addIs [Rep_llist]@llist.intrs
- addSEs [CONS_neq_NIL,NIL_neq_CONS,CONS_inject]
- addSDs [inj_onto_Abs_llist RS inj_ontoD,
+
+AddIs ([Rep_llist]@llist.intrs);
+AddSEs [CONS_neq_NIL,NIL_neq_CONS,CONS_inject];
+AddSDs [inj_onto_Abs_llist RS inj_ontoD,
inj_Rep_llist RS injD, Leaf_inject];
goalw LList.thy [LCons_def] "(LCons x xs=LCons y ys) = (x=y & xs=ys)";
-by (fast_tac llist_cs 1);
+by (Fast_tac 1);
qed "LCons_LCons_eq";
bind_thm ("LCons_inject", (LCons_LCons_eq RS iffD1 RS conjE));
val [major] = goal LList.thy "CONS M N: llist(A) ==> M: A & N: llist(A)";
by (rtac (major RS llist.elim) 1);
by (etac CONS_neq_NIL 1);
-by (fast_tac llist_cs 1);
+by (Fast_tac 1);
qed "CONS_D2";
@@ -450,7 +451,7 @@
val [major,minor] = goal LList.thy
"[| M: llist(A); !!x. x:A ==> f(x):B |] ==> Lmap f M: llist(B)";
by (rtac (major RS imageI RS llist_coinduct) 1);
-by (safe_tac set_cs);
+by (safe_tac (!claset));
by (etac llist.elim 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [Lmap_NIL,Lmap_CONS])));
by (REPEAT (ares_tac [list_Fun_NIL_I, list_Fun_CONS_I,
@@ -468,7 +469,7 @@
val [prem] = goalw LList.thy [o_def]
"M: llist(A) ==> Lmap (f o g) M = Lmap f (Lmap g M)";
by (rtac (prem RS imageI RS LList_equalityI) 1);
-by (safe_tac set_cs);
+by (safe_tac (!claset));
by (etac llist.elim 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [Lmap_NIL,Lmap_CONS])));
by (REPEAT (ares_tac [LListD_Fun_NIL_I, imageI, UnI1,
@@ -477,7 +478,7 @@
val [prem] = goal LList.thy "M: llist(A) ==> Lmap (%x.x) M = M";
by (rtac (prem RS imageI RS LList_equalityI) 1);
-by (safe_tac set_cs);
+by (safe_tac (!claset));
by (etac llist.elim 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [Lmap_NIL,Lmap_CONS])));
by (REPEAT (ares_tac [LListD_Fun_NIL_I, imageI RS UnI1,
@@ -525,13 +526,13 @@
"!!M N. [| M: llist(A); N: llist(A) |] ==> Lappend M N: llist(A)";
by (res_inst_tac
[("X", "UN u:llist(A). UN v: llist(A). {Lappend u v}")] llist_coinduct 1);
-by (fast_tac set_cs 1);
-by (safe_tac set_cs);
+by (Fast_tac 1);
+by (safe_tac (!claset));
by (eres_inst_tac [("a", "u")] llist.elim 1);
by (eres_inst_tac [("a", "v")] llist.elim 1);
by (ALLGOALS
(Asm_simp_tac THEN'
- fast_tac (set_cs addSIs [llist.NIL_I, list_Fun_NIL_I, list_Fun_CONS_I])));
+ fast_tac (!claset addSIs [llist.NIL_I, list_Fun_NIL_I, list_Fun_CONS_I])));
qed "Lappend_type";
(*strong co-induction: bisimulation and case analysis on one variable*)
@@ -544,7 +545,7 @@
by (eres_inst_tac [("a", "u")] llist.elim 1);
by (asm_simp_tac (!simpset addsimps [Lappend_NIL, list_Fun_llist_I]) 1);
by (Asm_simp_tac 1);
-by (fast_tac (set_cs addSIs [list_Fun_CONS_I]) 1);
+by (fast_tac (!claset addSIs [list_Fun_CONS_I]) 1);
qed "Lappend_type";
(**** Lazy lists as the type 'a llist -- strongly typed versions of above ****)
@@ -609,19 +610,19 @@
\ LListD_Fun (diag A) r <= (llist A) Times (llist A)";
by (stac llist_unfold 1);
by (simp_tac (!simpset addsimps [NIL_def, CONS_def]) 1);
-by (fast_tac univ_cs 1);
+by (Fast_tac 1);
qed "LListD_Fun_subset_Sigma_llist";
goal LList.thy
"prod_fun Rep_llist Rep_llist `` r <= \
\ (llist(range Leaf)) Times (llist(range Leaf))";
-by (fast_tac (prod_cs addIs [Rep_llist]) 1);
+by (fast_tac (!claset addIs [Rep_llist]) 1);
qed "subset_Sigma_llist";
val [prem] = goal LList.thy
"r <= (llist(range Leaf)) Times (llist(range Leaf)) ==> \
\ prod_fun (Rep_llist o Abs_llist) (Rep_llist o Abs_llist) `` r <= r";
-by (safe_tac prod_cs);
+by (safe_tac (!claset));
by (rtac (prem RS subsetD RS SigmaE2) 1);
by (assume_tac 1);
by (asm_simp_tac (!simpset addsimps [o_def,prod_fun,Abs_llist_inverse]) 1);
@@ -631,8 +632,8 @@
"prod_fun Rep_llist Rep_llist `` range(%x. (x, x)) = \
\ diag(llist(range Leaf))";
by (rtac equalityI 1);
-by (fast_tac (univ_cs addIs [Rep_llist]) 1);
-by (fast_tac (univ_cs addSEs [Abs_llist_inverse RS subst]) 1);
+by (fast_tac (!claset addIs [Rep_llist]) 1);
+by (fast_tac (!claset addSEs [Abs_llist_inverse RS subst]) 1);
qed "prod_fun_range_eq_diag";
(** To show two llists are equal, exhibit a bisimulation!
@@ -736,7 +737,7 @@
by (res_inst_tac [("r", "range(%u.(lmap f (iterates f u),iterates f (f u)))")]
llist_equalityI 1);
by (rtac rangeI 1);
-by (safe_tac set_cs);
+by (safe_tac (!claset));
by (res_inst_tac [("x1", "f(u)")] (iterates RS ssubst) 1);
by (res_inst_tac [("x1", "u")] (iterates RS ssubst) 1);
by (simp_tac (!simpset addsimps [lmap_LCons]) 1);
@@ -776,7 +777,7 @@
\ nat_rec n (iterates f u) (%m y.lmap f y)))")]
llist_equalityI 1);
by (REPEAT (resolve_tac [UN1_I, range_eqI, Pair_cong, nat_rec_0 RS sym] 1));
-by (safe_tac set_cs);
+by (safe_tac (!claset));
by (stac iterates 1);
by (stac prem 1);
by (stac fun_power_lmap 1);
@@ -826,7 +827,7 @@
by (res_inst_tac [("r", "range(%u.(lappend (iterates f u) N,iterates f u))")]
llist_equalityI 1);
by (rtac rangeI 1);
-by (safe_tac set_cs);
+by (safe_tac (!claset));
by (stac iterates 1);
by (simp_tac (!simpset addsimps [lappend_LCons]) 1);
qed "lappend_iterates";
@@ -841,7 +842,7 @@
llist_equalityI 1);
by (rtac UN1_I 1);
by (rtac rangeI 1);
-by (safe_tac set_cs);
+by (safe_tac (!claset));
by (res_inst_tac [("l", "l")] llistE 1);
by (res_inst_tac [("l", "n")] llistE 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps
--- a/src/HOL/ex/LexProd.ML Fri Jun 21 11:57:00 1996 +0200
+++ b/src/HOL/ex/LexProd.ML Fri Jun 21 12:18:50 1996 +0200
@@ -11,7 +11,7 @@
by (cut_facts_tac prems 1);
by (rtac allI 1);
by (rtac (surjective_pairing RS ssubst) 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
qed "split_all_pair";
val [wfa,wfb] = goalw LexProd.thy [wf_def,LexProd.lex_prod_def]
@@ -20,5 +20,5 @@
by (rtac (wfa RS spec RS mp) 1);
by (EVERY1 [rtac allI,rtac impI]);
by (rtac (wfb RS spec RS mp) 1);
-by (fast_tac (set_cs addSEs [Pair_inject]) 1);
+by (fast_tac (!claset addSEs [Pair_inject]) 1);
qed "wf_lex_prod";
--- a/src/HOL/ex/MT.ML Fri Jun 21 11:57:00 1996 +0200
+++ b/src/HOL/ex/MT.ML Fri Jun 21 12:18:50 1996 +0200
@@ -35,11 +35,11 @@
(* ############################################################ *)
val infsys_mono_tac =
- (rewtac subset_def) THEN (safe_tac HOL_cs) THEN (rtac ballI 1) THEN
+ (rewtac subset_def) THEN (safe_tac (claset_of "HOL")) THEN (rtac ballI 1) THEN
(rtac CollectI 1) THEN (dtac CollectD 1) THEN
REPEAT
( (TRY ((etac disjE 1) THEN (rtac disjI2 2) THEN (rtac disjI1 1))) THEN
- (REPEAT (etac exE 1)) THEN (REPEAT (rtac exI 1)) THEN (fast_tac set_cs 1)
+ (REPEAT (etac exE 1)) THEN (REPEAT (rtac exI 1)) THEN (fast_tac ((claset_of "Fun")delrules [equalityI]) 1)
);
val prems = goal MT.thy "P a b ==> P (fst (a,b)) (snd (a,b))";
@@ -102,7 +102,7 @@
by (rtac (monoh RS monoD) 1);
by (rtac (UnE RS subsetI) 1);
by (assume_tac 1);
-by (fast_tac (set_cs addSIs [cih]) 1);
+by (fast_tac (!claset addSIs [cih]) 1);
by (rtac (monoh RS monoD RS subsetD) 1);
by (rtac Un_upper2 1);
by (etac (monoh RS gfp_lemma2 RS subsetD) 1);
@@ -169,7 +169,7 @@
by (rtac lfp_intro2 1);
by (rtac eval_fun_mono 1);
by (rewtac eval_fun_def);
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
qed "eval_const";
val prems = goalw MT.thy [eval_def, eval_rel_def]
@@ -178,7 +178,7 @@
by (rtac lfp_intro2 1);
by (rtac eval_fun_mono 1);
by (rewtac eval_fun_def);
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
qed "eval_var2";
val prems = goalw MT.thy [eval_def, eval_rel_def]
@@ -187,7 +187,7 @@
by (rtac lfp_intro2 1);
by (rtac eval_fun_mono 1);
by (rewtac eval_fun_def);
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
qed "eval_fn";
val prems = goalw MT.thy [eval_def, eval_rel_def]
@@ -197,7 +197,7 @@
by (rtac lfp_intro2 1);
by (rtac eval_fun_mono 1);
by (rewtac eval_fun_def);
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
qed "eval_fix";
val prems = goalw MT.thy [eval_def, eval_rel_def]
@@ -207,7 +207,7 @@
by (rtac lfp_intro2 1);
by (rtac eval_fun_mono 1);
by (rewtac eval_fun_def);
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
qed "eval_app1";
val prems = goalw MT.thy [eval_def, eval_rel_def]
@@ -220,7 +220,7 @@
by (rtac lfp_intro2 1);
by (rtac eval_fun_mono 1);
by (rewtac eval_fun_def);
-by (fast_tac (set_cs addSIs [disjI2]) 1);
+by (fast_tac (!claset addSIs [disjI2]) 1);
qed "eval_app2";
(* Strong elimination, induction on evaluations *)
@@ -248,9 +248,9 @@
by (rtac eval_fun_mono 1);
by (rewtac eval_fun_def);
by (dtac CollectD 1);
-by (safe_tac HOL_cs);
+by (safe_tac (!claset));
by (ALLGOALS (resolve_tac prems));
-by (ALLGOALS (fast_tac set_cs));
+by (ALLGOALS (Fast_tac));
qed "eval_ind0";
val prems = goal MT.thy
@@ -293,7 +293,7 @@
by (rtac lfp_intro2 1);
by (rtac elab_fun_mono 1);
by (rewtac elab_fun_def);
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
qed "elab_const";
val prems = goalw MT.thy [elab_def, elab_rel_def]
@@ -302,7 +302,7 @@
by (rtac lfp_intro2 1);
by (rtac elab_fun_mono 1);
by (rewtac elab_fun_def);
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
qed "elab_var";
val prems = goalw MT.thy [elab_def, elab_rel_def]
@@ -311,7 +311,7 @@
by (rtac lfp_intro2 1);
by (rtac elab_fun_mono 1);
by (rewtac elab_fun_def);
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
qed "elab_fn";
val prems = goalw MT.thy [elab_def, elab_rel_def]
@@ -321,7 +321,7 @@
by (rtac lfp_intro2 1);
by (rtac elab_fun_mono 1);
by (rewtac elab_fun_def);
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
qed "elab_fix";
val prems = goalw MT.thy [elab_def, elab_rel_def]
@@ -331,7 +331,7 @@
by (rtac lfp_intro2 1);
by (rtac elab_fun_mono 1);
by (rewtac elab_fun_def);
-by (fast_tac (set_cs addSIs [disjI2]) 1);
+by (fast_tac (!claset addSIs [disjI2]) 1);
qed "elab_app";
(* Strong elimination, induction on elaborations *)
@@ -359,9 +359,9 @@
by (rtac elab_fun_mono 1);
by (rewtac elab_fun_def);
by (dtac CollectD 1);
-by (safe_tac HOL_cs);
+by (safe_tac (!claset));
by (ALLGOALS (resolve_tac prems));
-by (ALLGOALS (fast_tac set_cs));
+by (ALLGOALS (Fast_tac));
qed "elab_ind0";
val prems = goal MT.thy
@@ -410,9 +410,9 @@
by (rtac elab_fun_mono 1);
by (rewtac elab_fun_def);
by (dtac CollectD 1);
-by (safe_tac HOL_cs);
+by (safe_tac (!claset));
by (ALLGOALS (resolve_tac prems));
-by (ALLGOALS (fast_tac set_cs));
+by (ALLGOALS (Fast_tac));
qed "elab_elim0";
val prems = goal MT.thy
@@ -441,7 +441,7 @@
fun elab_e_elim_tac p =
( (rtac elab_elim 1) THEN
(resolve_tac p 1) THEN
- (REPEAT (fast_tac (e_ext_cs HOL_cs) 1))
+ (REPEAT (fast_tac (e_ext_cs (claset_of "HOL")) 1))
);
val prems = goal MT.thy "te |- e ===> t ==> (e = e_const(c) --> c isof t)";
@@ -451,7 +451,7 @@
val prems = goal MT.thy "te |- e_const(c) ===> t ==> c isof t";
by (cut_facts_tac prems 1);
by (dtac elab_const_elim_lem 1);
-by (fast_tac prop_cs 1);
+by (Fast_tac 1);
qed "elab_const_elim";
val prems = goal MT.thy
@@ -463,7 +463,7 @@
"te |- e_var(ev) ===> t ==> t=te_app te ev & ev : te_dom(te)";
by (cut_facts_tac prems 1);
by (dtac elab_var_elim_lem 1);
-by (fast_tac prop_cs 1);
+by (Fast_tac 1);
qed "elab_var_elim";
val prems = goal MT.thy
@@ -479,7 +479,7 @@
\ (? t1 t2. t=t1->t2 & te + {x1 |=> t1} |- e1 ===> t2)";
by (cut_facts_tac prems 1);
by (dtac elab_fn_elim_lem 1);
-by (fast_tac prop_cs 1);
+by (Fast_tac 1);
qed "elab_fn_elim";
val prems = goal MT.thy
@@ -494,7 +494,7 @@
\ (? t1 t2. t=t1->t2 & te + {ev1 |=> t1->t2} + {ev2 |=> t1} |- e1 ===> t2)";
by (cut_facts_tac prems 1);
by (dtac elab_fix_elim_lem 1);
-by (fast_tac prop_cs 1);
+by (Fast_tac 1);
qed "elab_fix_elim";
val prems = goal MT.thy
@@ -507,7 +507,7 @@
"te |- e1 @ e2 ===> t2 ==> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1)";
by (cut_facts_tac prems 1);
by (dtac elab_app_elim_lem 1);
-by (fast_tac prop_cs 1);
+by (Fast_tac 1);
qed "elab_app_elim";
(* ############################################################ *)
@@ -534,7 +534,7 @@
by (rewtac MT.hasty_fun_def);
by (rtac CollectI 1);
by (rtac disjI1 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
by (rtac mono_hasty_fun 1);
qed "hasty_rel_const_coind";
@@ -553,7 +553,7 @@
by (rewtac hasty_fun_def);
by (rtac CollectI 1);
by (rtac disjI2 1);
-by (fast_tac HOL_cs 1);
+by (fast_tac (claset_of "HOL") 1);
by (rtac mono_hasty_fun 1);
qed "hasty_rel_clos_coind";
@@ -574,9 +574,9 @@
by (rewtac hasty_fun_def);
by (dtac CollectD 1);
by (fold_goals_tac [hasty_fun_def]);
-by (safe_tac HOL_cs);
+by (safe_tac (!claset));
by (ALLGOALS (resolve_tac prems));
-by (ALLGOALS (fast_tac set_cs));
+by (ALLGOALS (Fast_tac));
qed "hasty_rel_elim0";
val prems = goal MT.thy
@@ -605,7 +605,7 @@
"te |- fn ev => e ===> t & ve hastyenv te ==> v_clos(<|ev,e,ve|>) hasty t";
by (cut_facts_tac prems 1);
by (rtac hasty_rel_clos_coind 1);
-by (ALLGOALS (fast_tac set_cs));
+by (ALLGOALS (Fast_tac));
qed "hasty_clos";
(* Elimination on constants for hasty *)
@@ -614,12 +614,12 @@
"v hasty t ==> (!c.(v = v_const(c) --> c isof t))";
by (cut_facts_tac prems 1);
by (rtac hasty_rel_elim 1);
-by (ALLGOALS (fast_tac (v_ext_cs HOL_cs)));
+by (ALLGOALS (fast_tac (v_ext_cs (claset_of "HOL"))));
qed "hasty_elim_const_lem";
val prems = goal MT.thy "v_const(c) hasty t ==> c isof t";
by (cut_facts_tac (prems RL [hasty_elim_const_lem]) 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
qed "hasty_elim_const";
(* Elimination on closures for hasty *)
@@ -630,14 +630,14 @@
\ v=v_clos(<|x,e,ve|>) --> (? te.te |- fn x => e ===> t & ve hastyenv te)";
by (cut_facts_tac prems 1);
by (rtac hasty_rel_elim 1);
-by (ALLGOALS (fast_tac (v_ext_cs HOL_cs)));
+by (ALLGOALS (fast_tac (v_ext_cs (claset_of "HOL"))));
qed "hasty_elim_clos_lem";
val prems = goal MT.thy
"v_clos(<|ev,e,ve|>) hasty t ==> ? te.te |- fn ev => e ===>\
\t & ve hastyenv te ";
by (cut_facts_tac (prems RL [hasty_elim_clos_lem]) 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
qed "hasty_elim_clos";
(* ############################################################ *)
@@ -650,10 +650,10 @@
by (rewtac hasty_env_def);
by (asm_full_simp_tac (!simpset delsimps mem_simps
addsimps [ve_dom_owr, te_dom_owr]) 1);
-by (safe_tac HOL_cs);
+by (safe_tac (claset_of "HOL"));
by (excluded_middle_tac "ev=x" 1);
by (asm_full_simp_tac (!simpset addsimps [ve_app_owr2, te_app_owr2]) 1);
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
by (asm_simp_tac (!simpset addsimps [ve_app_owr1, te_app_owr1]) 1);
qed "hasty_env1";
@@ -673,7 +673,7 @@
\ ve_app ve ev hasty t";
by (cut_facts_tac prems 1);
by (dtac elab_var_elim 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
qed "consistency_var";
val prems = goal MT.thy
@@ -681,7 +681,7 @@
\ v_clos(<| ev, e, ve |>) hasty t";
by (cut_facts_tac prems 1);
by (rtac hasty_clos 1);
-by (fast_tac prop_cs 1);
+by (Fast_tac 1);
qed "consistency_fn";
val prems = goalw MT.thy [hasty_env_def,hasty_def]
@@ -692,7 +692,7 @@
\ v_clos(cl) hasty t";
by (cut_facts_tac prems 1);
by (dtac elab_fix_elim 1);
-by (safe_tac HOL_cs);
+by (safe_tac (claset_of "HOL"));
(*Do a single unfolding of cl*)
by ((forward_tac [ssubst] 1) THEN (assume_tac 2));
by (rtac hasty_rel_clos_coind 1);
@@ -700,16 +700,16 @@
by (asm_simp_tac (!simpset addsimps [ve_dom_owr, te_dom_owr]) 1);
by (asm_simp_tac (!simpset delsimps mem_simps addsimps [ve_dom_owr]) 1);
-by (safe_tac HOL_cs);
+by (safe_tac (claset_of "HOL"));
by (excluded_middle_tac "ev2=ev1a" 1);
by (asm_full_simp_tac (!simpset addsimps [ve_app_owr2, te_app_owr2]) 1);
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
by (asm_simp_tac (!simpset delsimps mem_simps
addsimps [ve_app_owr1, te_app_owr1]) 1);
by (hyp_subst_tac 1);
by (etac subst 1);
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
qed "consistency_fix";
val prems = goal MT.thy
@@ -720,13 +720,13 @@
\ v_const(c_app c1 c2) hasty t";
by (cut_facts_tac prems 1);
by (dtac elab_app_elim 1);
-by (safe_tac HOL_cs);
+by (safe_tac (!claset));
by (rtac hasty_const 1);
by (rtac isof_app 1);
by (rtac hasty_elim_const 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
by (rtac hasty_elim_const 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
qed "consistency_app1";
val prems = goal MT.thy
@@ -742,7 +742,7 @@
\ v hasty t";
by (cut_facts_tac prems 1);
by (dtac elab_app_elim 1);
-by (safe_tac HOL_cs);
+by (safe_tac (!claset));
by ((etac allE 1) THEN (etac allE 1) THEN (etac impE 1));
by (assume_tac 1);
by (etac impE 1);
@@ -752,12 +752,12 @@
by (etac impE 1);
by (assume_tac 1);
by (dtac hasty_elim_clos 1);
-by (safe_tac HOL_cs);
+by (safe_tac (!claset));
by (dtac elab_fn_elim 1);
-by (safe_tac HOL_cs);
+by (safe_tac (!claset));
by (dtac t_fun_inj 1);
-by (safe_tac prop_cs);
-by ((dtac hasty_env1 1) THEN (assume_tac 1) THEN (fast_tac HOL_cs 1));
+by (safe_tac (!claset));
+by ((dtac hasty_env1 1) THEN (assume_tac 1) THEN (Fast_tac 1));
qed "consistency_app2";
val [major] = goal MT.thy
@@ -767,7 +767,7 @@
(* Proof by induction on the structure of evaluations *)
by (rtac (major RS eval_ind) 1);
-by (safe_tac HOL_cs);
+by (safe_tac (!claset));
by (DEPTH_SOLVE
(ares_tac [consistency_const, consistency_var, consistency_fn,
consistency_fix, consistency_app1, consistency_app2] 1));
@@ -780,7 +780,7 @@
val prems = goalw MT.thy [isof_env_def,hasty_env_def]
"ve isofenv te ==> ve hastyenv te";
by (cut_facts_tac prems 1);
-by (safe_tac HOL_cs);
+by (safe_tac (!claset));
by (etac allE 1);
by (etac impE 1);
by (assume_tac 1);
@@ -795,7 +795,7 @@
by (cut_facts_tac prems 1);
by (rtac hasty_elim_const 1);
by (dtac consistency 1);
-by (fast_tac (HOL_cs addSIs [basic_consistency_lem]) 1);
+by (fast_tac (!claset addSIs [basic_consistency_lem]) 1);
qed "basic_consistency";
--- a/src/HOL/ex/Mutil.ML Fri Jun 21 11:57:00 1996 +0200
+++ b/src/HOL/ex/Mutil.ML Fri Jun 21 12:18:50 1996 +0200
@@ -16,7 +16,7 @@
\ u: tiling A --> t Int u = {} --> t Un u : tiling A";
by (etac tiling.induct 1);
by (Simp_tac 1);
-by (fast_tac (set_cs addIs tiling.intrs
+by (fast_tac (!claset addIs tiling.intrs
addss (HOL_ss addsimps [Un_assoc,
subset_empty_iff RS sym])) 1);
bind_thm ("tiling_UnI", result() RS mp RS mp);
@@ -32,17 +32,17 @@
by (res_inst_tac [("x", "i")] spec 1);
by (nat_ind_tac "k" 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [below_Suc, less_Suc_eq])));
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
qed "below_less_iff";
goal thy "below(Suc n) Times B = ({n} Times B) Un ((below n) Times B)";
by (simp_tac (!simpset addsimps [below_Suc]) 1);
-by (fast_tac (prod_cs addIs [equalityI]) 1);
+by (fast_tac (!claset addIs [equalityI]) 1);
qed "Sigma_Suc1";
goal thy "A Times below(Suc n) = (A Times {n}) Un (A Times (below n))";
by (simp_tac (!simpset addsimps [below_Suc]) 1);
-by (fast_tac (prod_cs addIs [equalityI]) 1);
+by (fast_tac (!claset addIs [equalityI]) 1);
qed "Sigma_Suc2";
goal thy "{i} Times below(n + n) : tiling domino";
@@ -53,16 +53,16 @@
by (subgoal_tac (*seems the easiest way of turning one to the other*)
"({i} Times {Suc(n1+n1)}) Un ({i} Times {n1+n1}) = \
\ {(i, n1+n1), (i, Suc(n1+n1))}" 1);
-by (fast_tac (prod_cs addIs [equalityI]) 2);
+by (fast_tac (!claset addIs [equalityI]) 2);
by (asm_simp_tac (!simpset addsimps [domino.horiz]) 1);
-by (fast_tac (prod_cs addIs [equalityI, lessI] addEs [less_irrefl, less_asym]
+by (fast_tac (!claset addIs [equalityI, lessI] addEs [less_irrefl, less_asym]
addDs [below_less_iff RS iffD1]) 1);
qed "dominoes_tile_row";
goal thy "(below m) Times below(n + n) : tiling domino";
by (nat_ind_tac "m" 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [Sigma_Suc1])));
-by (fast_tac (prod_cs addIs [equalityI, tiling_UnI, dominoes_tile_row]
+by (fast_tac (!claset addIs [equalityI, tiling_UnI, dominoes_tile_row]
addEs [below_less_iff RS iffD1 RS less_irrefl]) 1);
qed "dominoes_tile_matrix";
@@ -81,11 +81,11 @@
bind_thm("finite_evnodd", evnodd_subset RS finite_subset);
goalw thy [evnodd_def] "evnodd (A Un B) b = evnodd A b Un evnodd B b";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "evnodd_Un";
goalw thy [evnodd_def] "evnodd (A - B) b = evnodd A b - evnodd B b";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "evnodd_Diff";
goalw thy [evnodd_def] "evnodd {} b = {}";
@@ -96,7 +96,7 @@
"evnodd (insert (i,j) C) b = \
\ (if (i+j) mod 2 = b then insert (i,j) (evnodd C b) else evnodd C b)";
by (asm_full_simp_tac (!simpset addsimps [evnodd_def]
- setloop (split_tac [expand_if] THEN' step_tac eq_cs)) 1);
+ setloop (split_tac [expand_if] THEN' step_tac (!claset))) 1);
qed "evnodd_insert";
@@ -111,11 +111,11 @@
by (REPEAT (asm_simp_tac (!simpset addsimps
[evnodd_insert, evnodd_empty, mod_Suc]
setloop split_tac [expand_if]) 1
- THEN fast_tac less_cs 1));
+ THEN Fast_tac 1));
qed "domino_singleton";
goal thy "!!d. d:domino ==> finite d";
-by (fast_tac (set_cs addSIs [finite_insertI, finite_emptyI]
+by (fast_tac (!claset addSIs [finite_insertI, finite_emptyI]
addEs [domino.elim]) 1);
qed "domino_finite";
@@ -125,7 +125,7 @@
goal thy "!!t. t:tiling domino ==> finite t";
by (eresolve_tac [tiling.induct] 1);
by (rtac finite_emptyI 1);
-by (fast_tac (set_cs addIs [domino_finite, finite_UnI]) 1);
+by (fast_tac (!claset addIs [domino_finite, finite_UnI]) 1);
qed "tiling_domino_finite";
goal thy "!!t. t: tiling domino ==> card(evnodd t 0) = card(evnodd t 1)";
@@ -135,13 +135,13 @@
by (Simp_tac 2 THEN assume_tac 1);
by (res_inst_tac [("b1","1")] (domino_singleton RS exE) 1);
by (Simp_tac 2 THEN assume_tac 1);
-by (step_tac HOL_cs 1);
+by (step_tac (!claset) 1);
by (subgoal_tac "ALL p b. p : evnodd a b --> p ~: evnodd ta b" 1);
by (asm_simp_tac (!simpset addsimps [evnodd_Un, Un_insert_left,
tiling_domino_finite,
evnodd_subset RS finite_subset,
card_insert_disjoint]) 1);
-by (fast_tac (set_cs addSDs [evnodd_subset RS subsetD] addEs [equalityE]) 1);
+by (fast_tac (!claset addSDs [evnodd_subset RS subsetD] addEs [equalityE]) 1);
qed "tiling_domino_0_1";
goal thy "!!m n. [| t = below(Suc m + Suc m) Times below(Suc n + Suc n); \
--- a/src/HOL/ex/Perm.ML Fri Jun 21 11:57:00 1996 +0200
+++ b/src/HOL/ex/Perm.ML Fri Jun 21 12:18:50 1996 +0200
@@ -40,7 +40,7 @@
goal Perm.thy "!!xs. [| xs <~~> ys |] ==> x mem xs --> x mem ys";
by (etac perm.induct 1);
-by (fast_tac HOL_cs 4);
+by (Fast_tac 4);
by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if])));
val perm_mem_lemma = result();
--- a/src/HOL/ex/PropLog.ML Fri Jun 21 11:57:00 1996 +0200
+++ b/src/HOL/ex/PropLog.ML Fri Jun 21 12:18:50 1996 +0200
@@ -18,7 +18,7 @@
(*Rule is called I for Identity Combinator, not for Introduction*)
goal PropLog.thy "H |- p->p";
-by(best_tac (HOL_cs addIs [thms.K,thms.S,thms.MP]) 1);
+by(best_tac (!claset addIs [thms.K,thms.S,thms.MP]) 1);
qed "thms_I";
(** Weakening, left and right **)
@@ -35,14 +35,14 @@
val weaken_left_Un2 = Un_upper2 RS weaken_left;
goal PropLog.thy "!!H. H |- q ==> H |- p->q";
-by(fast_tac (HOL_cs addIs [thms.K,thms.MP]) 1);
+by(fast_tac (!claset addIs [thms.K,thms.MP]) 1);
qed "weaken_right";
(*The deduction theorem*)
goal PropLog.thy "!!H. insert p H |- q ==> H |- p->q";
by (etac thms.induct 1);
by (ALLGOALS
- (fast_tac (set_cs addIs [thms_I, thms.H, thms.K, thms.S, thms.DN,
+ (fast_tac (!claset addIs [thms_I, thms.H, thms.K, thms.S, thms.DN,
thms.S RS thms.MP RS thms.MP, weaken_right])));
qed "deduction";
@@ -77,7 +77,7 @@
(*Soundness of the rules wrt truth-table semantics*)
goalw PropLog.thy [sat_def] "!!H. H |- p ==> H |= p";
by (etac thms.induct 1);
-by (fast_tac (set_cs addSDs [eval_imp RS iffD1 RS mp]) 5);
+by (fast_tac (!claset addSDs [eval_imp RS iffD1 RS mp]) 5);
by (ALLGOALS Asm_simp_tac);
qed "soundness";
@@ -104,7 +104,7 @@
by (rtac (expand_if RS iffD2) 1);
by(PropLog.pl.induct_tac "p" 1);
by (ALLGOALS (simp_tac (!simpset addsimps [thms_I, thms.H])));
-by (fast_tac (set_cs addIs [weaken_left_Un1, weaken_left_Un2,
+by (fast_tac (!claset addIs [weaken_left_Un1, weaken_left_Un2,
weaken_right, imp_false]
addSEs [false_imp]) 1);
qed "hyps_thms_if";
@@ -113,18 +113,19 @@
val [sat] = goalw PropLog.thy [sat_def] "{} |= p ==> hyps p tt |- p";
by (rtac (sat RS spec RS mp RS if_P RS subst) 1 THEN
rtac hyps_thms_if 2);
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
qed "sat_thms_p";
(*For proving certain theorems in our new propositional logic*)
-val thms_cs =
- set_cs addSIs [deduction] addIs [thms.H, thms.H RS thms.MP];
+
+AddSIs [deduction];
+AddIs [thms.H, thms.H RS thms.MP];
(*The excluded middle in the form of an elimination rule*)
goal PropLog.thy "H |- (p->q) -> ((p->false)->q) -> q";
by (rtac (deduction RS deduction) 1);
by (rtac (thms.DN RS thms.MP) 1);
-by (ALLGOALS (best_tac (thms_cs addSIs prems)));
+by (ALLGOALS (best_tac (!claset addSIs prems)));
qed "thms_excluded_middle";
(*Hard to prove directly because it requires cuts*)
@@ -143,7 +144,7 @@
by (Simp_tac 1);
by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
by (Simp_tac 1);
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
qed "hyps_Diff";
(*For the case hyps(p,t)-insert(#v -> false,Y) |- p;
@@ -153,17 +154,17 @@
by (Simp_tac 1);
by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
by (Simp_tac 1);
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
qed "hyps_insert";
(** Two lemmas for use with weaken_left **)
goal Set.thy "B-C <= insert a (B-insert a C)";
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
qed "insert_Diff_same";
goal Set.thy "insert a (B-{c}) - D <= insert a (B-insert c D)";
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
qed "insert_Diff_subset2";
(*The set hyps(p,t) is finite, and elements have the form #v or #v->false;
@@ -171,7 +172,7 @@
goal PropLog.thy "hyps p t : Fin(UN v:{x.True}. {#v, #v->false})";
by (PropLog.pl.induct_tac "p" 1);
by (ALLGOALS (simp_tac (!simpset setloop (split_tac [expand_if]))));
-by (ALLGOALS (fast_tac (set_cs addSIs Fin.intrs@[Fin_UnI])));
+by (ALLGOALS (fast_tac (!claset addSIs Fin.intrs@[Fin_UnI])));
qed "hyps_finite";
val Diff_weaken_left = subset_refl RSN (2, Diff_mono) RS weaken_left;
@@ -182,7 +183,7 @@
"{} |= p ==> !t. hyps p t - hyps p t0 |- p";
by (rtac (hyps_finite RS Fin_induct) 1);
by (simp_tac (!simpset addsimps [sat RS sat_thms_p]) 1);
-by (safe_tac set_cs);
+by (safe_tac (!claset));
(*Case hyps(p,t)-insert(#v,Y) |- p *)
by (rtac thms_excluded_middle_rule 1);
by (rtac (insert_Diff_same RS weaken_left) 1);
@@ -213,16 +214,16 @@
val [finite] = goal PropLog.thy "H: Fin({p.True}) ==> !p. H |= p --> H |- p";
by (rtac (finite RS Fin_induct) 1);
-by (safe_tac (set_cs addSIs [completeness_0]));
+by (safe_tac ((claset_of "Fun") addSIs [completeness_0]));
by (rtac (weaken_left_insert RS thms.MP) 1);
-by (fast_tac (set_cs addSIs [sat_imp]) 1);
-by (fast_tac thms_cs 1);
+by (fast_tac ((claset_of "Fun") addSIs [sat_imp]) 1);
+by (Fast_tac 1);
qed "completeness_lemma";
val completeness = completeness_lemma RS spec RS mp;
val [finite] = goal PropLog.thy "H: Fin({p.True}) ==> (H |- p) = (H |= p)";
-by (fast_tac (set_cs addSEs [soundness, finite RS completeness]) 1);
+by (fast_tac (!claset addSEs [soundness, finite RS completeness]) 1);
qed "thms_iff";
writeln"Reached end of file.";
--- a/src/HOL/ex/Puzzle.ML Fri Jun 21 11:57:00 1996 +0200
+++ b/src/HOL/ex/Puzzle.ML Fri Jun 21 12:18:50 1996 +0200
@@ -21,38 +21,38 @@
by (rtac classical 1);
by (dtac not_leE 1);
by (subgoal_tac "f(na) <= f(f(na))" 1);
-by (best_tac (HOL_cs addIs [lessD,Puzzle.f_ax,le_less_trans,le_trans]) 1);
-by (fast_tac (HOL_cs addIs [Puzzle.f_ax]) 1);
+by (best_tac (!claset addIs [lessD,Puzzle.f_ax,le_less_trans,le_trans]) 1);
+by (fast_tac (!claset addIs [Puzzle.f_ax]) 1);
val lemma = result() RS spec RS mp;
goal Puzzle.thy "n <= f(n)";
-by (fast_tac (HOL_cs addIs [lemma]) 1);
+by (fast_tac (!claset addIs [lemma]) 1);
qed "lemma1";
goal Puzzle.thy "f(n) < f(Suc(n))";
-by (fast_tac (HOL_cs addIs [Puzzle.f_ax,le_less_trans,lemma1]) 1);
+by (fast_tac (!claset addIs [Puzzle.f_ax,le_less_trans,lemma1]) 1);
qed "lemma2";
val prems = goal Puzzle.thy "(!!n.f(n) <= f(Suc(n))) ==> m<n --> f(m) <= f(n)";
by (res_inst_tac[("n","n")]nat_induct 1);
by (Simp_tac 1);
by (simp_tac (!simpset addsimps [less_Suc_eq]) 1);
-by (fast_tac (HOL_cs addIs (le_trans::prems)) 1);
+by (fast_tac (!claset addIs (le_trans::prems)) 1);
bind_thm("mono_lemma1", result() RS mp);
val [p1,p2] = goal Puzzle.thy
"[| !! n. f(n)<=f(Suc(n)); m<=n |] ==> f(m) <= f(n)";
by (rtac (p2 RS le_imp_less_or_eq RS disjE) 1);
by (etac (p1 RS mono_lemma1) 1);
-by (fast_tac (HOL_cs addIs [le_refl]) 1);
+by (fast_tac (!claset addIs [le_refl]) 1);
qed "mono_lemma";
val prems = goal Puzzle.thy "m <= n ==> f(m) <= f(n)";
-by (fast_tac (HOL_cs addIs ([mono_lemma,less_imp_le,lemma2]@prems)) 1);
+by (fast_tac (!claset addIs ([mono_lemma,less_imp_le,lemma2]@prems)) 1);
qed "f_mono";
goal Puzzle.thy "f(n) = n";
by (rtac le_anti_sym 1);
by (rtac lemma1 2);
-by (fast_tac (HOL_cs addIs [Puzzle.f_ax,leI] addDs [leD,f_mono,lessD]) 1);
+by (fast_tac (!claset addIs [Puzzle.f_ax,leI] addDs [leD,f_mono,lessD]) 1);
result();
--- a/src/HOL/ex/Qsort.ML Fri Jun 21 11:57:00 1996 +0200
+++ b/src/HOL/ex/Qsort.ML Fri Jun 21 12:18:50 1996 +0200
@@ -27,7 +27,7 @@
Addsimps [alls_lemma];
goal HOL.thy "((P --> Q) & (~P --> Q)) = Q";
-by(fast_tac HOL_cs 1);
+by(Fast_tac 1);
val lemma = result();
goal Qsort.thy "(Alls x:qsort le xs.P(x)) = (Alls x:xs.P(x))";
@@ -55,7 +55,7 @@
by(asm_full_simp_tac (!simpset addsimps []) 1);
by(asm_full_simp_tac (!simpset addsimps [list_all_mem_conv]) 1);
by(rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]);
-by(fast_tac HOL_cs 1);
+by(Fast_tac 1);
result();
(* A verification based on predicate calculus rather than combinators *)
@@ -69,7 +69,7 @@
goal Qsort.thy "x mem qsort le xs = x mem xs";
by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
-by(fast_tac HOL_cs 1);
+by(Fast_tac 1);
Addsimps [result()];
goal Qsort.thy
@@ -80,7 +80,7 @@
by(asm_simp_tac (!simpset setloop (split_tac [expand_if])
delsimps [list_all_conj]
addsimps [list_all_mem_conv]) 1);
-by(fast_tac HOL_cs 1);
+by(Fast_tac 1);
Addsimps [result()];
goal Qsort.thy
@@ -91,7 +91,7 @@
delsimps [list_all_conj]
addsimps [list_all_mem_conv]) 1);
by(rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]);
-by(fast_tac HOL_cs 1);
+by(Fast_tac 1);
result();
--- a/src/HOL/ex/SList.ML Fri Jun 21 11:57:00 1996 +0200
+++ b/src/HOL/ex/SList.ML Fri Jun 21 12:18:50 1996 +0200
@@ -12,7 +12,7 @@
goal SList.thy "list(A) = {Numb(0)} <+> (A <*> list(A))";
let val rew = rewrite_rule list_con_defs in
-by (fast_tac (univ_cs addSIs (equalityI :: map rew list.intrs)
+by (fast_tac (!claset addSIs (equalityI :: map rew list.intrs)
addEs [rew list.elim]) 1)
end;
qed "list_unfold";
@@ -26,7 +26,7 @@
(*Type checking -- list creates well-founded sets*)
goalw SList.thy (list_con_defs @ list.defs) "list(sexp) <= sexp";
by (rtac lfp_lowerbound 1);
-by (fast_tac (univ_cs addIs sexp.intrs@[sexp_In0I,sexp_In1I]) 1);
+by (fast_tac (!claset addIs sexp.intrs@[sexp_In0I,sexp_In1I]) 1);
qed "list_sexp";
(* A <= sexp ==> list(A) <= sexp *)
@@ -82,32 +82,32 @@
(** Injectiveness of CONS and Cons **)
goalw SList.thy [CONS_def] "(CONS K M=CONS L N) = (K=L & M=N)";
-by (fast_tac (HOL_cs addSEs [Scons_inject, make_elim In1_inject]) 1);
+by (fast_tac (!claset addSEs [Scons_inject, make_elim In1_inject]) 1);
qed "CONS_CONS_eq";
bind_thm ("CONS_inject", (CONS_CONS_eq RS iffD1 RS conjE));
(*For reasoning about abstract list constructors*)
-val list_cs = set_cs addIs [Rep_list] @ list.intrs
- addSEs [CONS_neq_NIL,NIL_neq_CONS,CONS_inject]
- addSDs [inj_onto_Abs_list RS inj_ontoD,
- inj_Rep_list RS injD, Leaf_inject];
+AddIs ([Rep_list] @ list.intrs);
+AddSEs [CONS_neq_NIL,NIL_neq_CONS,CONS_inject];
+AddSDs [inj_onto_Abs_list RS inj_ontoD,
+ inj_Rep_list RS injD, Leaf_inject];
goalw SList.thy [Cons_def] "(x#xs=y#ys) = (x=y & xs=ys)";
-by (fast_tac list_cs 1);
+by (Fast_tac 1);
qed "Cons_Cons_eq";
bind_thm ("Cons_inject2", (Cons_Cons_eq RS iffD1 RS conjE));
val [major] = goal SList.thy "CONS M N: list(A) ==> M: A & N: list(A)";
by (rtac (major RS setup_induction) 1);
by (etac list.induct 1);
-by (ALLGOALS (fast_tac list_cs));
+by (ALLGOALS (Fast_tac));
qed "CONS_D";
val prems = goalw SList.thy [CONS_def,In1_def]
"CONS M N: sexp ==> M: sexp & N: sexp";
by (cut_facts_tac prems 1);
-by (fast_tac (set_cs addSDs [Scons_D]) 1);
+by (fast_tac (!claset addSDs [Scons_D]) 1);
qed "sexp_CONS_D";
@@ -343,7 +343,7 @@
\ (!y ys. xs=y#ys --> P(f y ys)))";
by(list_ind_tac "xs" 1);
by(ALLGOALS Asm_simp_tac);
-by(fast_tac HOL_cs 1);
+by(Fast_tac 1);
qed "expand_list_case2";
--- a/src/HOL/ex/Simult.ML Fri Jun 21 11:57:00 1996 +0200
+++ b/src/HOL/ex/Simult.ML Fri Jun 21 12:18:50 1996 +0200
@@ -29,7 +29,7 @@
goalw Simult.thy [TF_def] "TF(sexp) <= sexp";
by (rtac lfp_lowerbound 1);
-by (fast_tac (univ_cs addIs sexp.intrs@[sexp_In0I, sexp_In1I]
+by (fast_tac (!claset addIs sexp.intrs@[sexp_In0I, sexp_In1I]
addSEs [PartE]) 1);
qed "TF_sexp";
@@ -50,7 +50,7 @@
\ |] ==> R(FCONS M N) \
\ |] ==> R(i)";
by (rtac ([TF_def, TF_fun_mono, major] MRS def_induct) 1);
-by (fast_tac (set_cs addIs (prems@[PartI])
+by (fast_tac (!claset addIs (prems@[PartI])
addEs [usumE, uprodE, PartE]) 1);
qed "TF_induct";
@@ -61,9 +61,9 @@
by (cfast_tac prems 1);
qed "TF_induct_lemma";
-val uplus_cs = set_cs addSIs [PartI]
- addSDs [In0_inject, In1_inject]
- addSEs [In0_neq_In1, In1_neq_In0, PartE];
+AddSIs [PartI];
+AddSDs [In0_inject, In1_inject];
+AddSEs [In0_neq_In1, In1_neq_In0, PartE];
(*Could prove ~ TCONS M N : Part (TF A) In1 etc. *)
@@ -77,7 +77,7 @@
by (rtac (ballI RS TF_induct_lemma) 1);
by (etac TF_induct 1);
by (rewrite_goals_tac TF_Rep_defs);
-by (ALLGOALS (fast_tac (uplus_cs addIs prems)));
+by (ALLGOALS (fast_tac (!claset addIs prems)));
(*29 secs??*)
qed "Tree_Forest_induct";
@@ -91,11 +91,11 @@
("Q1","%z.Q(Abs_Forest(z))")]
(Tree_Forest_induct RS conjE) 1);
(*Instantiates ?A1 to range(Leaf). *)
-by (fast_tac (set_cs addSEs [Rep_Tree_inverse RS subst,
+by (fast_tac (!claset addSEs [Rep_Tree_inverse RS subst,
Rep_Forest_inverse RS subst]
addSIs [Rep_Tree,Rep_Forest]) 4);
(*Cannot use simplifier: the rewrites work in the wrong direction!*)
-by (ALLGOALS (fast_tac (set_cs addSEs [Abs_Tree_inverse RS subst,
+by (ALLGOALS (fast_tac (!claset addSEs [Abs_Tree_inverse RS subst,
Abs_Forest_inverse RS subst]
addSIs prems)));
qed "tree_forest_induct";
@@ -131,41 +131,41 @@
val TF_I = TF_unfold RS equalityD2 RS subsetD;
(*For reasoning about the representation*)
-val TF_Rep_cs = uplus_cs addIs [TF_I, uprodI, usum_In0I, usum_In1I]
- addSEs [Scons_inject];
+AddIs [TF_I, uprodI, usum_In0I, usum_In1I];
+AddSEs [Scons_inject];
val prems = goalw Simult.thy TF_Rep_defs
"[| a: A; M: Part (TF A) In1 |] ==> TCONS a M : Part (TF A) In0";
-by (fast_tac (TF_Rep_cs addIs prems) 1);
+by (fast_tac (!claset addIs prems) 1);
qed "TCONS_I";
(* FNIL is a TF(A) -- this also justifies the type definition*)
goalw Simult.thy TF_Rep_defs "FNIL: Part (TF A) In1";
-by (fast_tac TF_Rep_cs 1);
+by (Fast_tac 1);
qed "FNIL_I";
val prems = goalw Simult.thy TF_Rep_defs
"[| M: Part (TF A) In0; N: Part (TF A) In1 |] ==> \
\ FCONS M N : Part (TF A) In1";
-by (fast_tac (TF_Rep_cs addIs prems) 1);
+by (fast_tac (!claset addIs prems) 1);
qed "FCONS_I";
(** Injectiveness of TCONS and FCONS **)
goalw Simult.thy TF_Rep_defs "(TCONS K M=TCONS L N) = (K=L & M=N)";
-by (fast_tac TF_Rep_cs 1);
+by (Fast_tac 1);
qed "TCONS_TCONS_eq";
bind_thm ("TCONS_inject", (TCONS_TCONS_eq RS iffD1 RS conjE));
goalw Simult.thy TF_Rep_defs "(FCONS K M=FCONS L N) = (K=L & M=N)";
-by (fast_tac TF_Rep_cs 1);
+by (Fast_tac 1);
qed "FCONS_FCONS_eq";
bind_thm ("FCONS_inject", (FCONS_FCONS_eq RS iffD1 RS conjE));
(** Distinctness of TCONS, FNIL and FCONS **)
goalw Simult.thy TF_Rep_defs "TCONS M N ~= FNIL";
-by (fast_tac TF_Rep_cs 1);
+by (Fast_tac 1);
qed "TCONS_not_FNIL";
bind_thm ("FNIL_not_TCONS", (TCONS_not_FNIL RS not_sym));
@@ -173,7 +173,7 @@
val FNIL_neq_TCONS = sym RS TCONS_neq_FNIL;
goalw Simult.thy TF_Rep_defs "FCONS M N ~= FNIL";
-by (fast_tac TF_Rep_cs 1);
+by (Fast_tac 1);
qed "FCONS_not_FNIL";
bind_thm ("FNIL_not_FCONS", (FCONS_not_FNIL RS not_sym));
@@ -181,7 +181,7 @@
val FNIL_neq_FCONS = sym RS FCONS_neq_FNIL;
goalw Simult.thy TF_Rep_defs "TCONS M N ~= FCONS K L";
-by (fast_tac TF_Rep_cs 1);
+by (Fast_tac 1);
qed "TCONS_not_FCONS";
bind_thm ("FCONS_not_TCONS", (TCONS_not_FCONS RS not_sym));
@@ -194,23 +194,23 @@
(** Injectiveness of Tcons and Fcons **)
(*For reasoning about abstract constructors*)
-val TF_cs = set_cs addSIs [Rep_Tree, Rep_Forest, TCONS_I, FNIL_I, FCONS_I]
- addSEs [TCONS_inject, FCONS_inject,
+AddSIs [Rep_Tree, Rep_Forest, TCONS_I, FNIL_I, FCONS_I];
+AddSEs [TCONS_inject, FCONS_inject,
TCONS_neq_FNIL, FNIL_neq_TCONS,
FCONS_neq_FNIL, FNIL_neq_FCONS,
- TCONS_neq_FCONS, FCONS_neq_TCONS]
- addSDs [inj_onto_Abs_Tree RS inj_ontoD,
+ TCONS_neq_FCONS, FCONS_neq_TCONS];
+AddSDs [inj_onto_Abs_Tree RS inj_ontoD,
inj_onto_Abs_Forest RS inj_ontoD,
inj_Rep_Tree RS injD, inj_Rep_Forest RS injD,
Leaf_inject];
goalw Simult.thy [Tcons_def] "(Tcons x xs=Tcons y ys) = (x=y & xs=ys)";
-by (fast_tac TF_cs 1);
+by (Fast_tac 1);
qed "Tcons_Tcons_eq";
bind_thm ("Tcons_inject", (Tcons_Tcons_eq RS iffD1 RS conjE));
goalw Simult.thy [Fcons_def,Fnil_def] "Fcons x xs ~= Fnil";
-by (fast_tac TF_cs 1);
+by (Fast_tac 1);
qed "Fcons_not_Fnil";
bind_thm ("Fcons_neq_Fnil", Fcons_not_Fnil RS notE);
@@ -220,7 +220,7 @@
(** Injectiveness of Fcons **)
goalw Simult.thy [Fcons_def] "(Fcons x xs=Fcons y ys) = (x=y & xs=ys)";
-by (fast_tac TF_cs 1);
+by (Fast_tac 1);
qed "Fcons_Fcons_eq";
bind_thm ("Fcons_inject", Fcons_Fcons_eq RS iffD1 RS conjE);
--- a/src/HOL/ex/Term.ML Fri Jun 21 11:57:00 1996 +0200
+++ b/src/HOL/ex/Term.ML Fri Jun 21 12:18:50 1996 +0200
@@ -12,7 +12,7 @@
(*** Monotonicity and unfolding of the function ***)
goal Term.thy "term(A) = A <*> list(term(A))";
-by (fast_tac (univ_cs addSIs (equalityI :: term.intrs)
+by (fast_tac (!claset addSIs (equalityI :: term.intrs)
addEs [term.elim]) 1);
qed "term_unfold";
@@ -25,7 +25,7 @@
goalw Term.thy term.defs "term(sexp) <= sexp";
by (rtac lfp_lowerbound 1);
-by (fast_tac (univ_cs addIs [sexp.SconsI, list_sexp RS subsetD]) 1);
+by (fast_tac (!claset addIs [sexp.SconsI, list_sexp RS subsetD]) 1);
qed "term_sexp";
(* A <= sexp ==> term(A) <= sexp *)
--- a/src/HOL/ex/cla.ML Fri Jun 21 11:57:00 1996 +0200
+++ b/src/HOL/ex/cla.ML Fri Jun 21 12:18:50 1996 +0200
@@ -11,17 +11,17 @@
writeln"File HOL/ex/cla.";
goal HOL.thy "(P --> Q | R) --> (P-->Q) | (P-->R)";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
(*If and only if*)
goal HOL.thy "(P=Q) = (Q=P::bool)";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
goal HOL.thy "~ (P = (~P))";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
@@ -38,112 +38,112 @@
writeln"Pelletier's examples";
(*1*)
goal HOL.thy "(P-->Q) = (~Q --> ~P)";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
(*2*)
goal HOL.thy "(~ ~ P) = P";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
(*3*)
goal HOL.thy "~(P-->Q) --> (Q-->P)";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
(*4*)
goal HOL.thy "(~P-->Q) = (~Q --> P)";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
(*5*)
goal HOL.thy "((P|Q)-->(P|R)) --> (P|(Q-->R))";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
(*6*)
goal HOL.thy "P | ~ P";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
(*7*)
goal HOL.thy "P | ~ ~ ~ P";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
(*8. Peirce's law*)
goal HOL.thy "((P-->Q) --> P) --> P";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
(*9*)
goal HOL.thy "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
(*10*)
goal HOL.thy "(Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P=Q)";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
(*11. Proved in each direction (incorrectly, says Pelletier!!) *)
goal HOL.thy "P=P::bool";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
(*12. "Dijkstra's law"*)
goal HOL.thy "((P = Q) = R) = (P = (Q = R))";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
(*13. Distributive law*)
goal HOL.thy "(P | (Q & R)) = ((P | Q) & (P | R))";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
(*14*)
goal HOL.thy "(P = Q) = ((Q | ~P) & (~Q|P))";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
(*15*)
goal HOL.thy "(P --> Q) = (~P | Q)";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
(*16*)
goal HOL.thy "(P-->Q) | (Q-->P)";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
(*17*)
goal HOL.thy "((P & (Q-->R))-->S) = ((~P | Q | S) & (~P | ~R | S))";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
writeln"Classical Logic: examples with quantifiers";
goal HOL.thy "(! x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
goal HOL.thy "(? x. P-->Q(x)) = (P --> (? x.Q(x)))";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
goal HOL.thy "(? x.P(x)-->Q) = ((! x.P(x)) --> Q)";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
goal HOL.thy "((! x.P(x)) | Q) = (! x. P(x) | Q)";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
(*From Wishnu Prasetya*)
goal HOL.thy
"(!s. q(s) --> r(s)) & ~r(s) & (!s. ~r(s) & ~q(s) --> p(t) | q(t)) \
\ --> p(t) | r(t)";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
@@ -151,60 +151,60 @@
(*Needs multiple instantiation of the quantifier.*)
goal HOL.thy "(! x. P(x)-->P(f(x))) & P(d)-->P(f(f(f(d))))";
-by (deepen_tac HOL_cs 1 1);
+by (deepen_tac (!claset) 1 1);
result();
(*Needs double instantiation of the quantifier*)
goal HOL.thy "? x. P(x) --> P(a) & P(b)";
-by (deepen_tac HOL_cs 1 1);
+by (deepen_tac (!claset) 1 1);
result();
goal HOL.thy "? z. P(z) --> (! x. P(x))";
-by (deepen_tac HOL_cs 1 1);
+by (deepen_tac (!claset) 1 1);
result();
goal HOL.thy "? x. (? y. P(y)) --> P(x)";
-by (deepen_tac HOL_cs 1 1);
+by (deepen_tac (!claset) 1 1);
result();
writeln"Hard examples with quantifiers";
writeln"Problem 18";
goal HOL.thy "? y. ! x. P(y)-->P(x)";
-by (deepen_tac HOL_cs 1 1);
+by (deepen_tac (!claset) 1 1);
result();
writeln"Problem 19";
goal HOL.thy "? x. ! y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))";
-by (deepen_tac HOL_cs 1 1);
+by (deepen_tac (!claset) 1 1);
result();
writeln"Problem 20";
goal HOL.thy "(! x y. ? z. ! w. (P(x)&Q(y)-->R(z)&S(w))) \
\ --> (? x y. P(x) & Q(y)) --> (? z. R(z))";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
writeln"Problem 21";
goal HOL.thy "(? x. P-->Q(x)) & (? x. Q(x)-->P) --> (? x. P=Q(x))";
-by (deepen_tac HOL_cs 1 1);
+by (deepen_tac (!claset) 1 1);
result();
writeln"Problem 22";
goal HOL.thy "(! x. P = Q(x)) --> (P = (! x. Q(x)))";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
writeln"Problem 23";
goal HOL.thy "(! x. P | Q(x)) = (P | (! x. Q(x)))";
-by (best_tac HOL_cs 1);
+by (best_tac (!claset) 1);
result();
writeln"Problem 24";
goal HOL.thy "~(? x. S(x)&Q(x)) & (! x. P(x) --> Q(x)|R(x)) & \
\ ~(? x.P(x)) --> (? x.Q(x)) & (! x. Q(x)|R(x) --> S(x)) \
\ --> (? x. P(x)&R(x))";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
writeln"Problem 25";
@@ -213,14 +213,14 @@
\ (! x. P(x) --> (M(x) & L(x))) & \
\ ((! x. P(x)-->Q(x)) | (? x. P(x)&R(x))) \
\ --> (? x. Q(x)&P(x))";
-by (best_tac HOL_cs 1);
+by (best_tac (!claset) 1);
result();
writeln"Problem 26";
goal HOL.thy "((? x. p(x)) = (? x. q(x))) & \
\ (! x. ! y. p(x) & q(y) --> (r(x) = s(y))) \
\ --> ((! x. p(x)-->r(x)) = (! x. q(x)-->s(x)))";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
writeln"Problem 27";
@@ -229,7 +229,7 @@
\ (! x. M(x) & L(x) --> P(x)) & \
\ ((? x. R(x) & ~ Q(x)) --> (! x. L(x) --> ~ R(x))) \
\ --> (! x. M(x) --> ~L(x))";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
writeln"Problem 28. AMENDED";
@@ -237,21 +237,21 @@
\ ((! x. Q(x)|R(x)) --> (? x. Q(x)&S(x))) & \
\ ((? x.S(x)) --> (! x. L(x) --> M(x))) \
\ --> (! x. P(x) & L(x) --> M(x))";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
writeln"Problem 29. Essentially the same as Principia Mathematica *11.71";
goal HOL.thy "(? x. F(x)) & (? y. G(y)) \
\ --> ( ((! x. F(x)-->H(x)) & (! y. G(y)-->J(y))) = \
\ (! x y. F(x) & G(y) --> H(x) & J(y)))";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
writeln"Problem 30";
goal HOL.thy "(! x. P(x) | Q(x) --> ~ R(x)) & \
\ (! x. (Q(x) --> ~ S(x)) --> P(x) & R(x)) \
\ --> (! x. S(x))";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
writeln"Problem 31";
@@ -259,7 +259,7 @@
\ (? x. L(x) & P(x)) & \
\ (! x. ~ R(x) --> M(x)) \
\ --> (? x. L(x) & M(x))";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
writeln"Problem 32";
@@ -267,13 +267,13 @@
\ (! x. S(x) & R(x) --> L(x)) & \
\ (! x. M(x) --> R(x)) \
\ --> (! x. P(x) & M(x) --> L(x))";
-by (best_tac HOL_cs 1);
+by (best_tac (!claset) 1);
result();
writeln"Problem 33";
goal HOL.thy "(! x. P(a) & (P(x)-->P(b))-->P(c)) = \
\ (! x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))";
-by (best_tac HOL_cs 1);
+by (best_tac (!claset) 1);
result();
writeln"Problem 34 AMENDED (TWICE!!)";
@@ -282,13 +282,13 @@
\ ((? x. q(x)) = (! y. p(y)))) = \
\ ((? x. ! y. q(x) = q(y)) = \
\ ((? x. p(x)) = (! y. q(y))))";
-by (deepen_tac HOL_cs 3 1);
+by (deepen_tac (!claset) 3 1);
(*slower with smaller bounds*)
result();
writeln"Problem 35";
goal HOL.thy "? x y. P x y --> (! u v. P u v)";
-by (deepen_tac HOL_cs 1 1);
+by (deepen_tac (!claset) 1 1);
result();
writeln"Problem 36";
@@ -297,7 +297,7 @@
\ (! x y. J x y | G x y --> \
\ (! z. J y z | G y z --> H x z)) \
\ --> (! x. ? y. H x y)";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
writeln"Problem 37";
@@ -306,7 +306,7 @@
\ (! x z. ~(P x z) --> (? y. Q y z)) & \
\ ((? x y. Q x y) --> (! x. R x x)) \
\ --> (! x. ? y. R x y)";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
writeln"Problem 38";
@@ -316,29 +316,29 @@
\ (! x. (~p(a) | p(x) | (? z. ? w. p(z) & r x w & r w z)) & \
\ (~p(a) | ~(? y. p(y) & r x y) | \
\ (? z. ? w. p(z) & r x w & r w z)))";
-by (deepen_tac HOL_cs 0 1); (*beats fast_tac!*)
+by (deepen_tac (!claset) 0 1); (*beats fast_tac!*)
result();
writeln"Problem 39";
goal HOL.thy "~ (? x. ! y. F y x = (~ F y y))";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
writeln"Problem 40. AMENDED";
goal HOL.thy "(? y. ! x. F x y = F x x) \
\ --> ~ (! x. ? y. ! z. F z y = (~ F z x))";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
writeln"Problem 41";
goal HOL.thy "(! z. ? y. ! x. f x y = (f x z & ~ f x x)) \
\ --> ~ (? z. ! x. f x z)";
-by (best_tac HOL_cs 1);
+by (best_tac (!claset) 1);
result();
writeln"Problem 42";
goal HOL.thy "~ (? y. ! x. p x y = (~ (? z. p x z & p z x)))";
-by (deepen_tac HOL_cs 3 1);
+by (deepen_tac (!claset) 3 1);
result();
writeln"Problem 43 NOT PROVED AUTOMATICALLY";
@@ -352,7 +352,7 @@
\ (? y. g(y) & h x y & (? y. g(y) & ~ h x y))) & \
\ (? x. j(x) & (! y. g(y) --> h x y)) \
\ --> (? x. j(x) & ~f(x))";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
writeln"Problem 45";
@@ -363,7 +363,7 @@
\ (? x. f(x) & (! y. h x y --> l(y)) \
\ & (! y. g(y) & h x y --> j x y)) \
\ --> (? x. f(x) & ~ (? y. g(y) & h x y))";
-by (best_tac HOL_cs 1);
+by (best_tac (!claset) 1);
result();
@@ -371,7 +371,7 @@
writeln"Problem 48";
goal HOL.thy "(a=b | c=d) & (a=c | b=d) --> a=d | b=c";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
writeln"Problem 49 NOT PROVED AUTOMATICALLY";
@@ -379,25 +379,25 @@
the type constraint ensures that x,y,z have the same type as a,b,u. *)
goal HOL.thy "(? x y::'a. ! z. z=x | z=y) & P(a) & P(b) & (~a=b) \
\ --> (! u::'a.P(u))";
-by (Classical.safe_tac HOL_cs);
+by (Classical.safe_tac (!claset));
by (res_inst_tac [("x","a")] allE 1);
by (assume_tac 1);
by (res_inst_tac [("x","b")] allE 1);
by (assume_tac 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
writeln"Problem 50";
(*What has this to do with equality?*)
goal HOL.thy "(! x. P a x | (! y.P x y)) --> (? x. ! y.P x y)";
-by (deepen_tac HOL_cs 1 1);
+by (deepen_tac (!claset) 1 1);
result();
writeln"Problem 51";
goal HOL.thy
"(? z w. ! x y. P x y = (x=z & y=w)) --> \
\ (? z. ! x. ? w. (! y. P x y = (y=w)) = (x=z))";
-by (best_tac HOL_cs 1);
+by (best_tac (!claset) 1);
result();
writeln"Problem 52";
@@ -405,7 +405,7 @@
goal HOL.thy
"(? z w. ! x y. P x y = (x=z & y=w)) --> \
\ (? w. ! y. ? z. (! x. P x y = (x=z)) = (y=w))";
-by (best_tac HOL_cs 1);
+by (best_tac (!claset) 1);
result();
writeln"Problem 55";
@@ -421,37 +421,37 @@
\ (!x. hates agatha x --> hates butler x) & \
\ (!x. ~hates x agatha | ~hates x butler | ~hates x charles) --> \
\ killed ?who agatha";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
writeln"Problem 56";
goal HOL.thy
"(! x. (? y. P(y) & x=f(y)) --> P(x)) = (! x. P(x) --> P(f(x)))";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
writeln"Problem 57";
goal HOL.thy
"P (f a b) (f b c) & P (f b c) (f a c) & \
\ (! x y z. P x y & P y z --> P x z) --> P (f a b) (f a c)";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
writeln"Problem 58 NOT PROVED AUTOMATICALLY";
goal HOL.thy "(! x y. f(x)=g(y)) --> (! x y. f(f(x))=f(g(y)))";
val f_cong = read_instantiate [("f","f")] arg_cong;
-by (fast_tac (HOL_cs addIs [f_cong]) 1);
+by (fast_tac (!claset addIs [f_cong]) 1);
result();
writeln"Problem 59";
goal HOL.thy "(! x. P(x) = (~P(f(x)))) --> (? x. P(x) & ~P(f(x)))";
-by (deepen_tac HOL_cs 1 1);
+by (deepen_tac (!claset) 1 1);
result();
writeln"Problem 60";
goal HOL.thy
"! x. P x (f x) = (? y. (! z. P z y --> P z (f x)) & P x y)";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
writeln"Problem 62 as corrected in AAR newletter #31";
@@ -459,7 +459,7 @@
"(ALL x. p a & (p x --> p(f x)) --> p(f(f x))) = \
\ (ALL x. (~ p a | p x | p(f(f x))) & \
\ (~ p a | ~ p(f x) | p(f(f x))))";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
(*From Rudnicki, Obvious Inferences, JAR 3 (1987), 383-393.
@@ -468,14 +468,14 @@
"(ALL x. F(x) & ~G(x) --> (EX y. H(x,y) & J(y))) & \
\ (EX x. K(x) & F(x) & (ALL y. H(x,y) --> K(y))) & \
\ (ALL x. K(x) --> ~G(x)) --> (EX x. K(x) --> ~G(x))";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
goal Prod.thy
"(ALL x y. R(x,y) | R(y,x)) & \
\ (ALL x y. S(x,y) & S(y,x) --> x=y) & \
\ (ALL x y. R(x,y) --> S(x,y)) --> (ALL x y. S(x,y) --> R(x,y))";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
result();
--- a/src/HOL/ex/meson.ML Fri Jun 21 11:57:00 1996 +0200
+++ b/src/HOL/ex/meson.ML Fri Jun 21 12:18:50 1996 +0200
@@ -16,7 +16,7 @@
(*Prove theorems using fast_tac*)
fun prove_fun s =
prove_goal HOL.thy s
- (fn prems => [ cut_facts_tac prems 1, fast_tac HOL_cs 1 ]);
+ (fn prems => [ cut_facts_tac prems 1, Fast_tac 1 ]);
(**** Negation Normal Form ****)
@@ -63,7 +63,7 @@
val [major] = goal HOL.thy
"! x. ? y. Q x y ==> ? f. ! x. Q x (f x)";
by (cut_facts_tac [major] 1);
-by (fast_tac (HOL_cs addEs [selectI]) 1);
+by (fast_tac (!claset addEs [selectI]) 1);
qed "choice";
@@ -430,7 +430,7 @@
(*First, breaks the goal into independent units*)
val safe_best_meson_tac =
- SELECT_GOAL (TRY (safe_tac HOL_cs) THEN
+ SELECT_GOAL (TRY (safe_tac (!claset)) THEN
TRYALL (best_meson_tac size_of_subgoals));
(** Depth-first search version **)
@@ -464,7 +464,7 @@
(prolog_step_tac' (make_horns cls))));
val safe_meson_tac =
- SELECT_GOAL (TRY (safe_tac HOL_cs) THEN
+ SELECT_GOAL (TRY (safe_tac (!claset)) THEN
TRYALL (iter_deepen_meson_tac));
--- a/src/HOL/ex/rel.ML Fri Jun 21 11:57:00 1996 +0200
+++ b/src/HOL/ex/rel.ML Fri Jun 21 12:18:50 1996 +0200
@@ -34,7 +34,7 @@
(*** domain ***)
val [prem] = goalw Rel.thy [domain_def,Pair_def] "(a,b): r ==> a : domain(r)";
-by (fast_tac (set_cs addIs [prem]) 1);
+by (fast_tac (!claset addIs [prem]) 1);
qed "domainI";
val major::prems = goalw Rel.thy [domain_def]
@@ -48,7 +48,7 @@
(*** range2 ***)
val [prem] = goalw Rel.thy [range2_def,Pair_def] "(a,b): r ==> b : range2(r)";
-by (fast_tac (set_cs addIs [prem]) 1);
+by (fast_tac (!claset addIs [prem]) 1);
qed "range2I";
val major::prems = goalw Rel.thy [range2_def]
@@ -102,8 +102,8 @@
\ ==> wf(r)";
by (rtac (prem1 RS wfI) 1);
by (res_inst_tac [ ("B", "A-Z") ] (prem2 RS subsetCE) 1);
-by (fast_tac ZF_cs 3);
-by (fast_tac ZF_cs 2);
-by (fast_tac ZF_cs 1);
+by (Fast_tac 3);
+by (Fast_tac 2);
+by (Fast_tac 1);
qed "wfI2";
--- a/src/HOL/ex/set.ML Fri Jun 21 11:57:00 1996 +0200
+++ b/src/HOL/ex/set.ML Fri Jun 21 12:18:50 1996 +0200
@@ -20,12 +20,12 @@
goal Set.thy "~ (? f:: 'a=>'a set. ! S. ? x. f(x) = S)";
(*requires best-first search because it is undirectional*)
-by (best_tac (set_cs addSEs [equalityCE]) 1);
+by (best_tac (!claset addSEs [equalityCE]) 1);
qed "cantor1";
(*This form displays the diagonal term*)
goal Set.thy "! f:: 'a=>'a set. ! x. f(x) ~= ?S(f)";
-by (best_tac (set_cs addSEs [equalityCE]) 1);
+by (best_tac (!claset addSEs [equalityCE]) 1);
uresult();
(*This form exploits the set constructs*)
@@ -39,15 +39,15 @@
by (assume_tac 1);
choplev 0;
-by (best_tac (set_cs addSEs [equalityCE]) 1);
+by (best_tac (!claset addSEs [equalityCE]) 1);
(*** The Schroder-Berstein Theorem ***)
val prems = goalw Lfp.thy [image_def] "inj(f) ==> Inv(f)``(f``X) = X";
by (cut_facts_tac prems 1);
by (rtac equalityI 1);
-by (fast_tac (set_cs addEs [Inv_f_f RS ssubst]) 1);
-by (fast_tac (set_cs addEs [Inv_f_f RS ssubst]) 1);
+by (fast_tac (!claset addEs [Inv_f_f RS ssubst]) 1);
+by (fast_tac (!claset addEs [Inv_f_f RS ssubst]) 1);
qed "inv_image_comp";
val prems = goal Set.thy "f(a) ~: (f``X) ==> a~:X";
@@ -55,7 +55,7 @@
qed "contra_imageI";
goal Lfp.thy "(a ~: Compl(X)) = (a:X)";
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
qed "not_Compl";
(*Lots of backtracking in this proof...*)
@@ -69,22 +69,22 @@
goal Lfp.thy "range(%z. if z:X then f(z) else g(z)) = f``X Un g``Compl(X)";
by (rtac equalityI 1);
by (rewtac range_def);
-by (fast_tac (set_cs addIs [if_P RS sym, if_not_P RS sym]) 2);
+by (fast_tac (!claset addIs [if_P RS sym, if_not_P RS sym]) 2);
by (rtac subsetI 1);
by (etac CollectE 1);
by (etac exE 1);
by (etac ssubst 1);
by (rtac (excluded_middle RS disjE) 1);
-by (EVERY' [rtac (if_P RS ssubst), atac, fast_tac set_cs] 2);
-by (EVERY' [rtac (if_not_P RS ssubst), atac, fast_tac set_cs] 1);
+by (EVERY' [rtac (if_P RS ssubst), atac, Fast_tac] 2);
+by (EVERY' [rtac (if_not_P RS ssubst), atac, Fast_tac] 1);
qed "range_if_then_else";
goal Lfp.thy "a : X Un Compl(X)";
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
qed "X_Un_Compl";
goalw Lfp.thy [surj_def] "surj(f) = (!a. a : range(f))";
-by (fast_tac (set_cs addEs [ssubst]) 1);
+by (fast_tac (!claset addEs [ssubst]) 1);
qed "surj_iff_full_range";
val [compl] = goal Lfp.thy
@@ -105,9 +105,9 @@
by (rewtac inj_def);
by (cut_facts_tac [injf,injg] 1);
by (EVERY1 [rtac allI, rtac allI, stac expand_if, rtac conjI, stac expand_if]);
-by (fast_tac (set_cs addEs [inj_ontoD, sym RS f_eq_gE]) 1);
+by (fast_tac (!claset addEs [inj_ontoD, sym RS f_eq_gE]) 1);
by (stac expand_if 1);
-by (fast_tac (set_cs addEs [inj_ontoD, f_eq_gE]) 1);
+by (fast_tac (!claset addEs [inj_ontoD, f_eq_gE]) 1);
qed "bij_if_then_else";
goal Lfp.thy "? X. X = Compl(g``Compl((f:: 'a=>'b)``X))";