# HG changeset patch # User berghofe # Date 835352330 -7200 # Node ID e381e1c51689b62fe94eff4044b95cd03fa19e3c # Parent 245721624c8dbeb06eef0c577f158ed09c4b0697 Classical tactics now use default claset. diff -r 245721624c8d -r e381e1c51689 src/HOL/ex/Acc.ML --- 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"; diff -r 245721624c8d -r e381e1c51689 src/HOL/ex/Comb.ML --- 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^*"; diff -r 245721624c8d -r e381e1c51689 src/HOL/ex/InSort.ML --- 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)"; diff -r 245721624c8d -r e381e1c51689 src/HOL/ex/LList.ML --- 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 diff -r 245721624c8d -r e381e1c51689 src/HOL/ex/LexProd.ML --- 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"; diff -r 245721624c8d -r e381e1c51689 src/HOL/ex/MT.ML --- 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"; diff -r 245721624c8d -r e381e1c51689 src/HOL/ex/Mutil.ML --- 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); \ diff -r 245721624c8d -r e381e1c51689 src/HOL/ex/Perm.ML --- 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(); diff -r 245721624c8d -r e381e1c51689 src/HOL/ex/PropLog.ML --- 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."; diff -r 245721624c8d -r e381e1c51689 src/HOL/ex/Puzzle.ML --- 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 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(); diff -r 245721624c8d -r e381e1c51689 src/HOL/ex/Qsort.ML --- 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(); diff -r 245721624c8d -r e381e1c51689 src/HOL/ex/SList.ML --- 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"; diff -r 245721624c8d -r e381e1c51689 src/HOL/ex/Simult.ML --- 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); diff -r 245721624c8d -r e381e1c51689 src/HOL/ex/Term.ML --- 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 *) diff -r 245721624c8d -r e381e1c51689 src/HOL/ex/cla.ML --- 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(); diff -r 245721624c8d -r e381e1c51689 src/HOL/ex/meson.ML --- 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)); diff -r 245721624c8d -r e381e1c51689 src/HOL/ex/rel.ML --- 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"; diff -r 245721624c8d -r e381e1c51689 src/HOL/ex/set.ML --- 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))";