# HG changeset patch # User berghofe # Date 833814656 -7200 # Node ID 8a31d85d27b8c61c61b008bc1da4225d97ff7e4f # Parent 0a2414dd696b1877bf5fe6c3b4fa03ce365b627f best_tac, deepen_tac and safe_tac now also use default claset. diff -r 0a2414dd696b -r 8a31d85d27b8 src/HOL/Arith.ML --- a/src/HOL/Arith.ML Mon Jun 03 11:44:44 1996 +0200 +++ b/src/HOL/Arith.ML Mon Jun 03 17:10:56 1996 +0200 @@ -384,7 +384,7 @@ goal thy "Suc(Suc(m)) mod 2 = m mod 2"; by (subgoal_tac "m mod 2 < 2" 1); by (asm_simp_tac (!simpset addsimps [mod_less_divisor]) 2); -by (safe_tac less_cs); +by (safe_tac (!claset)); by (ALLGOALS (asm_simp_tac (!simpset addsimps [mod_Suc]))); qed "mod2_Suc_Suc"; Addsimps [mod2_Suc_Suc]; @@ -406,7 +406,7 @@ by (REPEAT_FIRST (ares_tac [conjI, impI])); by (res_inst_tac [("x","0")] exI 2); by (Simp_tac 2); -by (safe_tac HOL_cs); +by (safe_tac (claset_of "HOL")); by (res_inst_tac [("x","Suc(k)")] exI 1); by (Simp_tac 1); qed_spec_mp "less_eq_Suc_add"; @@ -462,7 +462,7 @@ qed_spec_mp "add_leD1"; goal Arith.thy "!!k l::nat. [| k m i*k<=j*l"; by (rtac le_trans 1); by (ALLGOALS - (deepen_tac (HOL_cs addIs [mult_commute RS ssubst, mult_le_mono1]) 0)); + (deepen_tac (!claset addIs [mult_commute RS ssubst, mult_le_mono1]) 0)); qed "mult_le_mono"; (*strict, in 1st argument; proof is by induction on k>0*) diff -r 0a2414dd696b -r 8a31d85d27b8 src/HOL/Finite.ML --- a/src/HOL/Finite.ML Mon Jun 03 11:44:44 1996 +0200 +++ b/src/HOL/Finite.ML Mon Jun 03 17:10:56 1996 +0200 @@ -49,7 +49,7 @@ rtac subs]); by (rtac (fin RS Fin_induct) 1); by (simp_tac (!simpset addsimps [subset_Un_eq]) 1); -by (safe_tac (set_cs addSDs [subset_insert_iff RS iffD1])); +by (safe_tac (!claset addSDs [subset_insert_iff RS iffD1])); by (eres_inst_tac [("t","C")] (insert_Diff RS subst) 2); by (ALLGOALS Asm_simp_tac); qed "Fin_subset"; @@ -205,47 +205,47 @@ by (etac equalityE 1); by (asm_full_simp_tac (!simpset addsimps [subset_insert,Collect_conv_insert, less_Suc_eq]) 1); -by (SELECT_GOAL(safe_tac eq_cs)1); +by (SELECT_GOAL(safe_tac (!claset))1); by (Asm_full_simp_tac 1); by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1); - by (SELECT_GOAL(safe_tac eq_cs)1); + by (SELECT_GOAL(safe_tac (!claset))1); by (subgoal_tac "x ~= f m" 1); by (Fast_tac 2); by (subgoal_tac "? k. f k = x & k \ @@ -316,7 +316,7 @@ by (strip_tac 1); by (case_tac "x:B" 1); by (dtac mk_disjoint_insert 1); - by (SELECT_GOAL(safe_tac HOL_cs)1); + by (SELECT_GOAL(safe_tac (!claset))1); by (rotate_tac ~1 1); by (asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1); by (rotate_tac ~1 1); diff -r 0a2414dd696b -r 8a31d85d27b8 src/HOL/Nat.ML --- a/src/HOL/Nat.ML Mon Jun 03 11:44:44 1996 +0200 +++ b/src/HOL/Nat.ML Mon Jun 03 17:10:56 1996 +0200 @@ -557,7 +557,7 @@ cut_facts_tac prems 1, rtac select_equality 1, fold_goals_tac [Least_def], - safe_tac (HOL_cs addSEs [LeastI]), + safe_tac (!claset addSEs [LeastI]), res_inst_tac [("n","j")] natE 1, Fast_tac 1, fast_tac (!claset addDs [Suc_less_SucD] addDs [not_less_Least]) 1, @@ -566,11 +566,11 @@ hyp_subst_tac 1, rewtac Least_def, rtac (select_equality RS arg_cong RS sym) 1, - safe_tac HOL_cs, + safe_tac (!claset), dtac Suc_mono 1, Fast_tac 1, cut_facts_tac [less_linear] 1, - safe_tac HOL_cs, + safe_tac (!claset), atac 2, Fast_tac 2, dtac Suc_mono 1, diff -r 0a2414dd696b -r 8a31d85d27b8 src/HOL/Relation.ML --- a/src/HOL/Relation.ML Mon Jun 03 11:44:44 1996 +0200 +++ b/src/HOL/Relation.ML Mon Jun 03 17:10:56 1996 +0200 @@ -162,7 +162,7 @@ "[| b: r^^A; !!x.[| (x,b): r; x:A |] ==> P |] ==> P" (fn major::prems=> [ (rtac (major RS CollectE) 1), - (safe_tac set_cs), + (safe_tac (!claset)), (etac RangeE 1), (rtac (hd prems) 1), (REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ]); diff -r 0a2414dd696b -r 8a31d85d27b8 src/HOL/Trancl.ML --- a/src/HOL/Trancl.ML Mon Jun 03 11:44:44 1996 +0200 +++ b/src/HOL/Trancl.ML Mon Jun 03 17:10:56 1996 +0200 @@ -75,7 +75,7 @@ (*transitivity of transitive closure!! -- by induction.*) goalw Trancl.thy [trans_def] "trans(r^*)"; -by (safe_tac HOL_cs); +by (safe_tac (!claset)); by (eres_inst_tac [("b","z")] rtrancl_induct 1); by (ALLGOALS(fast_tac (!claset addIs [rtrancl_into_rtrancl]))); qed "trans_rtrancl"; @@ -150,7 +150,7 @@ qed "rtrancl_converseI"; goal Trancl.thy "(converse r)^* = converse(r^*)"; -by (safe_tac (rel_eq_cs addSIs [rtrancl_converseI])); +by (safe_tac (!claset addSIs [rtrancl_converseI])); by (res_inst_tac [("p","x")] PairE 1); by (hyp_subst_tac 1); by (etac rtrancl_converseD 1); diff -r 0a2414dd696b -r 8a31d85d27b8 src/HOL/Univ.ML --- a/src/HOL/Univ.ML Mon Jun 03 11:44:44 1996 +0200 +++ b/src/HOL/Univ.ML Mon Jun 03 17:10:56 1996 +0200 @@ -131,7 +131,7 @@ by (etac (Push_inject1 RS sym) 1); by (rtac (inj_Rep_Node RS injD) 1); by (etac trans 1); -by (safe_tac (HOL_cs addSEs [Pair_inject,Push_inject,sym])); +by (safe_tac (!claset addSEs [Pair_inject,Push_inject,sym])); qed "Push_Node_inject"; @@ -230,7 +230,7 @@ "ndepth (Push_Node i n) = Suc(ndepth(n))"; by (stac (Rep_Node RS Node_Push_I RS Abs_Node_inverse) 1); by (cut_facts_tac [rewrite_rule [Node_def] Rep_Node] 1); -by (safe_tac set_cs); +by (safe_tac (!claset)); by (etac ssubst 1); (*instantiates type variables!*) by (Simp_tac 1); by (rtac Least_equality 1); @@ -244,11 +244,11 @@ (*** ntrunc applied to the various node sets ***) goalw Univ.thy [ntrunc_def] "ntrunc 0 M = {}"; -by (safe_tac (set_cs addSIs [equalityI] addSEs [less_zeroE])); +by (safe_tac (!claset addSIs [equalityI] addSEs [less_zeroE])); qed "ntrunc_0"; goalw Univ.thy [Atom_def,ntrunc_def] "ntrunc (Suc k) (Atom a) = Atom(a)"; -by (safe_tac (set_cs addSIs [equalityI])); +by (safe_tac (!claset addSIs [equalityI])); by (stac ndepth_K0 1); by (rtac zero_less_Suc 1); qed "ntrunc_Atom"; @@ -263,7 +263,7 @@ goalw Univ.thy [Scons_def,ntrunc_def] "ntrunc (Suc k) (M$N) = ntrunc k M $ ntrunc k N"; -by (safe_tac (set_cs addSIs [equalityI,imageI])); +by (safe_tac ((claset_of "Fun") addSIs [equalityI,imageI])); by (REPEAT (stac ndepth_Push_Node 3 THEN etac Suc_mono 3)); by (REPEAT (rtac Suc_less_SucD 1 THEN rtac (ndepth_Push_Node RS subst) 1 THEN @@ -275,7 +275,7 @@ goalw Univ.thy [In0_def] "ntrunc (Suc 0) (In0 M) = {}"; by (simp_tac (!simpset addsimps [ntrunc_Scons,ntrunc_0]) 1); by (rewtac Scons_def); -by (safe_tac (set_cs addSIs [equalityI])); +by (safe_tac (!claset addSIs [equalityI])); qed "ntrunc_one_In0"; goalw Univ.thy [In0_def] @@ -286,7 +286,7 @@ goalw Univ.thy [In1_def] "ntrunc (Suc 0) (In1 M) = {}"; by (simp_tac (!simpset addsimps [ntrunc_Scons,ntrunc_0]) 1); by (rewtac Scons_def); -by (safe_tac (set_cs addSIs [equalityI])); +by (safe_tac (!claset addSIs [equalityI])); qed "ntrunc_one_In1"; goalw Univ.thy [In1_def] @@ -541,7 +541,7 @@ (*Dependent version*) goal Univ.thy "(Sigma A B <**> Sigma C D) <= Sigma (A<*>C) (Split(%x y. B(x)<*>D(y)))"; -by (safe_tac univ_cs); +by (safe_tac (!claset)); by (stac Split 1); by (Fast_tac 1); qed "dprod_subset_Sigma2"; diff -r 0a2414dd696b -r 8a31d85d27b8 src/HOL/WF.ML --- a/src/HOL/WF.ML Mon Jun 03 11:44:44 1996 +0200 +++ b/src/HOL/WF.ML Mon Jun 03 17:10:56 1996 +0200 @@ -19,7 +19,7 @@ by (strip_tac 1); by (rtac allE 1); by (assume_tac 1); -by (best_tac (HOL_cs addSEs [prem1 RS subsetD RS SigmaE2] addIs [prem2]) 1); +by (best_tac (!claset addSEs [prem1 RS subsetD RS SigmaE2] addIs [prem2]) 1); qed "wfI"; val major::prems = goalw WF.thy [wf_def] diff -r 0a2414dd696b -r 8a31d85d27b8 src/HOL/equalities.ML --- a/src/HOL/equalities.ML Mon Jun 03 11:44:44 1996 +0200 +++ b/src/HOL/equalities.ML Mon Jun 03 17:10:56 1996 +0200 @@ -310,7 +310,7 @@ qed "Inter_Un_subset"; goal Set.thy "Inter(A Un B) = Inter(A) Int Inter(B)"; -by (best_tac eq_cs 1); +by (best_tac (!claset) 1); qed "Inter_Un_distrib"; section "UN and INT"; @@ -412,7 +412,7 @@ qed "Un_Inter"; goal Set.thy "(INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)"; -by (best_tac eq_cs 1); +by (best_tac (!claset) 1); qed "Int_Inter_image"; (*Equivalent version*)