best_tac, deepen_tac and safe_tac now also use default claset.
authorberghofe
Mon Jun 03 17:10:56 1996 +0200 (1996-06-03)
changeset 17868a31d85d27b8
parent 1785 0a2414dd696b
child 1787 9246e236a57f
best_tac, deepen_tac and safe_tac now also use default claset.
src/HOL/Arith.ML
src/HOL/Finite.ML
src/HOL/Nat.ML
src/HOL/Relation.ML
src/HOL/Trancl.ML
src/HOL/Univ.ML
src/HOL/WF.ML
src/HOL/equalities.ML
     1.1 --- a/src/HOL/Arith.ML	Mon Jun 03 11:44:44 1996 +0200
     1.2 +++ b/src/HOL/Arith.ML	Mon Jun 03 17:10:56 1996 +0200
     1.3 @@ -384,7 +384,7 @@
     1.4  goal thy "Suc(Suc(m)) mod 2 = m mod 2";
     1.5  by (subgoal_tac "m mod 2 < 2" 1);
     1.6  by (asm_simp_tac (!simpset addsimps [mod_less_divisor]) 2);
     1.7 -by (safe_tac less_cs);
     1.8 +by (safe_tac (!claset));
     1.9  by (ALLGOALS (asm_simp_tac (!simpset addsimps [mod_Suc])));
    1.10  qed "mod2_Suc_Suc";
    1.11  Addsimps [mod2_Suc_Suc];
    1.12 @@ -406,7 +406,7 @@
    1.13  by (REPEAT_FIRST (ares_tac [conjI, impI]));
    1.14  by (res_inst_tac [("x","0")] exI 2);
    1.15  by (Simp_tac 2);
    1.16 -by (safe_tac HOL_cs);
    1.17 +by (safe_tac (claset_of "HOL"));
    1.18  by (res_inst_tac [("x","Suc(k)")] exI 1);
    1.19  by (Simp_tac 1);
    1.20  qed_spec_mp "less_eq_Suc_add";
    1.21 @@ -462,7 +462,7 @@
    1.22  qed_spec_mp "add_leD1";
    1.23  
    1.24  goal Arith.thy "!!k l::nat. [| k<l; m+l = k+n |] ==> m<n";
    1.25 -by (safe_tac (HOL_cs addSDs [less_eq_Suc_add]));
    1.26 +by (safe_tac (!claset addSDs [less_eq_Suc_add]));
    1.27  by (asm_full_simp_tac
    1.28      (!simpset delsimps [add_Suc_right]
    1.29                  addsimps ([add_Suc_right RS sym, add_left_cancel] @add_ac)) 1);
    1.30 @@ -523,7 +523,7 @@
    1.31  goal Arith.thy "!!i::nat. [| i<=j; k<=l |] ==> i*k<=j*l";
    1.32  by (rtac le_trans 1);
    1.33  by (ALLGOALS 
    1.34 -    (deepen_tac (HOL_cs addIs [mult_commute RS ssubst, mult_le_mono1]) 0));
    1.35 +    (deepen_tac (!claset addIs [mult_commute RS ssubst, mult_le_mono1]) 0));
    1.36  qed "mult_le_mono";
    1.37  
    1.38  (*strict, in 1st argument; proof is by induction on k>0*)
     2.1 --- a/src/HOL/Finite.ML	Mon Jun 03 11:44:44 1996 +0200
     2.2 +++ b/src/HOL/Finite.ML	Mon Jun 03 17:10:56 1996 +0200
     2.3 @@ -49,7 +49,7 @@
     2.4              rtac subs]);
     2.5  by (rtac (fin RS Fin_induct) 1);
     2.6  by (simp_tac (!simpset addsimps [subset_Un_eq]) 1);
     2.7 -by (safe_tac (set_cs addSDs [subset_insert_iff RS iffD1]));
     2.8 +by (safe_tac (!claset addSDs [subset_insert_iff RS iffD1]));
     2.9  by (eres_inst_tac [("t","C")] (insert_Diff RS subst) 2);
    2.10  by (ALLGOALS Asm_simp_tac);
    2.11  qed "Fin_subset";
    2.12 @@ -205,47 +205,47 @@
    2.13  by (etac equalityE 1);
    2.14  by (asm_full_simp_tac
    2.15       (!simpset addsimps [subset_insert,Collect_conv_insert, less_Suc_eq]) 1);
    2.16 -by (SELECT_GOAL(safe_tac eq_cs)1);
    2.17 +by (SELECT_GOAL(safe_tac (!claset))1);
    2.18    by (Asm_full_simp_tac 1);
    2.19    by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
    2.20 -  by (SELECT_GOAL(safe_tac eq_cs)1);
    2.21 +  by (SELECT_GOAL(safe_tac (!claset))1);
    2.22     by (subgoal_tac "x ~= f m" 1);
    2.23      by (Fast_tac 2);
    2.24     by (subgoal_tac "? k. f k = x & k<m" 1);
    2.25 -    by (best_tac set_cs 2);
    2.26 -   by (SELECT_GOAL(safe_tac HOL_cs)1);
    2.27 +    by (best_tac (!claset) 2);
    2.28 +   by (SELECT_GOAL(safe_tac (!claset))1);
    2.29     by (res_inst_tac [("x","k")] exI 1);
    2.30     by (Asm_simp_tac 1);
    2.31    by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
    2.32 -  by (best_tac set_cs 1);
    2.33 +  by (best_tac (!claset) 1);
    2.34   bd sym 1;
    2.35   by (rotate_tac ~1 1);
    2.36   by (Asm_full_simp_tac 1);
    2.37   by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
    2.38 - by (SELECT_GOAL(safe_tac eq_cs)1);
    2.39 + by (SELECT_GOAL(safe_tac (!claset))1);
    2.40    by (subgoal_tac "x ~= f m" 1);
    2.41     by (Fast_tac 2);
    2.42    by (subgoal_tac "? k. f k = x & k<m" 1);
    2.43 -   by (best_tac set_cs 2);
    2.44 -  by (SELECT_GOAL(safe_tac HOL_cs)1);
    2.45 +   by (best_tac (!claset) 2);
    2.46 +  by (SELECT_GOAL(safe_tac (!claset))1);
    2.47    by (res_inst_tac [("x","k")] exI 1);
    2.48    by (Asm_simp_tac 1);
    2.49   by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
    2.50 - by (best_tac set_cs 1);
    2.51 + by (best_tac (!claset) 1);
    2.52  by (res_inst_tac [("x","%j. if f j = f i then f m else f j")] exI 1);
    2.53 -by (SELECT_GOAL(safe_tac eq_cs)1);
    2.54 +by (SELECT_GOAL(safe_tac (!claset))1);
    2.55   by (subgoal_tac "x ~= f i" 1);
    2.56    by (Fast_tac 2);
    2.57   by (case_tac "x = f m" 1);
    2.58    by (res_inst_tac [("x","i")] exI 1);
    2.59    by (Asm_simp_tac 1);
    2.60   by (subgoal_tac "? k. f k = x & k<m" 1);
    2.61 -  by (best_tac set_cs 2);
    2.62 - by (SELECT_GOAL(safe_tac HOL_cs)1);
    2.63 +  by (best_tac (!claset) 2);
    2.64 + by (SELECT_GOAL(safe_tac (!claset))1);
    2.65   by (res_inst_tac [("x","k")] exI 1);
    2.66   by (Asm_simp_tac 1);
    2.67  by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
    2.68 -by (best_tac set_cs 1);
    2.69 +by (best_tac (!claset) 1);
    2.70  val lemma = result();
    2.71  
    2.72  goal Finite.thy "!!A. [| finite A; x ~: A |] ==> \
    2.73 @@ -316,7 +316,7 @@
    2.74  by (strip_tac 1);
    2.75  by (case_tac "x:B" 1);
    2.76   by (dtac mk_disjoint_insert 1);
    2.77 - by (SELECT_GOAL(safe_tac HOL_cs)1);
    2.78 + by (SELECT_GOAL(safe_tac (!claset))1);
    2.79   by (rotate_tac ~1 1);
    2.80   by (asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1);
    2.81  by (rotate_tac ~1 1);
     3.1 --- a/src/HOL/Nat.ML	Mon Jun 03 11:44:44 1996 +0200
     3.2 +++ b/src/HOL/Nat.ML	Mon Jun 03 17:10:56 1996 +0200
     3.3 @@ -557,7 +557,7 @@
     3.4  	cut_facts_tac prems 1,
     3.5  	rtac select_equality 1,
     3.6  	fold_goals_tac [Least_def],
     3.7 -	safe_tac (HOL_cs addSEs [LeastI]),
     3.8 +	safe_tac (!claset addSEs [LeastI]),
     3.9  	res_inst_tac [("n","j")] natE 1,
    3.10  	Fast_tac 1,
    3.11  	fast_tac (!claset addDs [Suc_less_SucD] addDs [not_less_Least]) 1,	
    3.12 @@ -566,11 +566,11 @@
    3.13  	hyp_subst_tac 1,
    3.14  	rewtac Least_def,
    3.15  	rtac (select_equality RS arg_cong RS sym) 1,
    3.16 -	safe_tac HOL_cs,
    3.17 +	safe_tac (!claset),
    3.18  	dtac Suc_mono 1,
    3.19  	Fast_tac 1,
    3.20  	cut_facts_tac [less_linear] 1,
    3.21 -	safe_tac HOL_cs,
    3.22 +	safe_tac (!claset),
    3.23  	atac 2,
    3.24  	Fast_tac 2,
    3.25  	dtac Suc_mono 1,
     4.1 --- a/src/HOL/Relation.ML	Mon Jun 03 11:44:44 1996 +0200
     4.2 +++ b/src/HOL/Relation.ML	Mon Jun 03 17:10:56 1996 +0200
     4.3 @@ -162,7 +162,7 @@
     4.4      "[| b: r^^A;  !!x.[| (x,b): r;  x:A |] ==> P |] ==> P"
     4.5   (fn major::prems=>
     4.6    [ (rtac (major RS CollectE) 1),
     4.7 -    (safe_tac set_cs),
     4.8 +    (safe_tac (!claset)),
     4.9      (etac RangeE 1),
    4.10      (rtac (hd prems) 1),
    4.11      (REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ]);
     5.1 --- a/src/HOL/Trancl.ML	Mon Jun 03 11:44:44 1996 +0200
     5.2 +++ b/src/HOL/Trancl.ML	Mon Jun 03 17:10:56 1996 +0200
     5.3 @@ -75,7 +75,7 @@
     5.4  
     5.5  (*transitivity of transitive closure!! -- by induction.*)
     5.6  goalw Trancl.thy [trans_def] "trans(r^*)";
     5.7 -by (safe_tac HOL_cs);
     5.8 +by (safe_tac (!claset));
     5.9  by (eres_inst_tac [("b","z")] rtrancl_induct 1);
    5.10  by (ALLGOALS(fast_tac (!claset addIs [rtrancl_into_rtrancl])));
    5.11  qed "trans_rtrancl";
    5.12 @@ -150,7 +150,7 @@
    5.13  qed "rtrancl_converseI";
    5.14  
    5.15  goal Trancl.thy "(converse r)^* = converse(r^*)";
    5.16 -by (safe_tac (rel_eq_cs addSIs [rtrancl_converseI]));
    5.17 +by (safe_tac (!claset addSIs [rtrancl_converseI]));
    5.18  by (res_inst_tac [("p","x")] PairE 1);
    5.19  by (hyp_subst_tac 1);
    5.20  by (etac rtrancl_converseD 1);
     6.1 --- a/src/HOL/Univ.ML	Mon Jun 03 11:44:44 1996 +0200
     6.2 +++ b/src/HOL/Univ.ML	Mon Jun 03 17:10:56 1996 +0200
     6.3 @@ -131,7 +131,7 @@
     6.4  by (etac (Push_inject1 RS sym) 1);
     6.5  by (rtac (inj_Rep_Node RS injD) 1);
     6.6  by (etac trans 1);
     6.7 -by (safe_tac (HOL_cs addSEs [Pair_inject,Push_inject,sym]));
     6.8 +by (safe_tac (!claset addSEs [Pair_inject,Push_inject,sym]));
     6.9  qed "Push_Node_inject";
    6.10  
    6.11  
    6.12 @@ -230,7 +230,7 @@
    6.13      "ndepth (Push_Node i n) = Suc(ndepth(n))";
    6.14  by (stac (Rep_Node RS Node_Push_I RS Abs_Node_inverse) 1);
    6.15  by (cut_facts_tac [rewrite_rule [Node_def] Rep_Node] 1);
    6.16 -by (safe_tac set_cs);
    6.17 +by (safe_tac (!claset));
    6.18  by (etac ssubst 1);  (*instantiates type variables!*)
    6.19  by (Simp_tac 1);
    6.20  by (rtac Least_equality 1);
    6.21 @@ -244,11 +244,11 @@
    6.22  (*** ntrunc applied to the various node sets ***)
    6.23  
    6.24  goalw Univ.thy [ntrunc_def] "ntrunc 0 M = {}";
    6.25 -by (safe_tac (set_cs addSIs [equalityI] addSEs [less_zeroE]));
    6.26 +by (safe_tac (!claset addSIs [equalityI] addSEs [less_zeroE]));
    6.27  qed "ntrunc_0";
    6.28  
    6.29  goalw Univ.thy [Atom_def,ntrunc_def] "ntrunc (Suc k) (Atom a) = Atom(a)";
    6.30 -by (safe_tac (set_cs addSIs [equalityI]));
    6.31 +by (safe_tac (!claset addSIs [equalityI]));
    6.32  by (stac ndepth_K0 1);
    6.33  by (rtac zero_less_Suc 1);
    6.34  qed "ntrunc_Atom";
    6.35 @@ -263,7 +263,7 @@
    6.36  
    6.37  goalw Univ.thy [Scons_def,ntrunc_def]
    6.38      "ntrunc (Suc k) (M$N) = ntrunc k M $ ntrunc k N";
    6.39 -by (safe_tac (set_cs addSIs [equalityI,imageI]));
    6.40 +by (safe_tac ((claset_of "Fun") addSIs [equalityI,imageI]));
    6.41  by (REPEAT (stac ndepth_Push_Node 3 THEN etac Suc_mono 3));
    6.42  by (REPEAT (rtac Suc_less_SucD 1 THEN 
    6.43              rtac (ndepth_Push_Node RS subst) 1 THEN 
    6.44 @@ -275,7 +275,7 @@
    6.45  goalw Univ.thy [In0_def] "ntrunc (Suc 0) (In0 M) = {}";
    6.46  by (simp_tac (!simpset addsimps [ntrunc_Scons,ntrunc_0]) 1);
    6.47  by (rewtac Scons_def);
    6.48 -by (safe_tac (set_cs addSIs [equalityI]));
    6.49 +by (safe_tac (!claset addSIs [equalityI]));
    6.50  qed "ntrunc_one_In0";
    6.51  
    6.52  goalw Univ.thy [In0_def]
    6.53 @@ -286,7 +286,7 @@
    6.54  goalw Univ.thy [In1_def] "ntrunc (Suc 0) (In1 M) = {}";
    6.55  by (simp_tac (!simpset addsimps [ntrunc_Scons,ntrunc_0]) 1);
    6.56  by (rewtac Scons_def);
    6.57 -by (safe_tac (set_cs addSIs [equalityI]));
    6.58 +by (safe_tac (!claset addSIs [equalityI]));
    6.59  qed "ntrunc_one_In1";
    6.60  
    6.61  goalw Univ.thy [In1_def]
    6.62 @@ -541,7 +541,7 @@
    6.63  (*Dependent version*)
    6.64  goal Univ.thy
    6.65      "(Sigma A B <**> Sigma C D) <= Sigma (A<*>C) (Split(%x y. B(x)<*>D(y)))";
    6.66 -by (safe_tac univ_cs);
    6.67 +by (safe_tac (!claset));
    6.68  by (stac Split 1);
    6.69  by (Fast_tac 1);
    6.70  qed "dprod_subset_Sigma2";
     7.1 --- a/src/HOL/WF.ML	Mon Jun 03 11:44:44 1996 +0200
     7.2 +++ b/src/HOL/WF.ML	Mon Jun 03 17:10:56 1996 +0200
     7.3 @@ -19,7 +19,7 @@
     7.4  by (strip_tac 1);
     7.5  by (rtac allE 1);
     7.6  by (assume_tac 1);
     7.7 -by (best_tac (HOL_cs addSEs [prem1 RS subsetD RS SigmaE2] addIs [prem2]) 1);
     7.8 +by (best_tac (!claset addSEs [prem1 RS subsetD RS SigmaE2] addIs [prem2]) 1);
     7.9  qed "wfI";
    7.10  
    7.11  val major::prems = goalw WF.thy [wf_def]
     8.1 --- a/src/HOL/equalities.ML	Mon Jun 03 11:44:44 1996 +0200
     8.2 +++ b/src/HOL/equalities.ML	Mon Jun 03 17:10:56 1996 +0200
     8.3 @@ -310,7 +310,7 @@
     8.4  qed "Inter_Un_subset";
     8.5  
     8.6  goal Set.thy "Inter(A Un B) = Inter(A) Int Inter(B)";
     8.7 -by (best_tac eq_cs 1);
     8.8 +by (best_tac (!claset) 1);
     8.9  qed "Inter_Un_distrib";
    8.10  
    8.11  section "UN and INT";
    8.12 @@ -412,7 +412,7 @@
    8.13  qed "Un_Inter";
    8.14  
    8.15  goal Set.thy "(INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)";
    8.16 -by (best_tac eq_cs 1);
    8.17 +by (best_tac (!claset) 1);
    8.18  qed "Int_Inter_image";
    8.19  
    8.20  (*Equivalent version*)