Converted proofs to use default clasets.

--- a/src/HOL/IMP/Denotation.ML	Tue Sep 10 11:37:52 1996 +0200
+++ b/src/HOL/IMP/Denotation.ML	Tue Sep 10 20:10:29 1996 +0200
@@ -6,20 +6,12 @@
 
 open Denotation;
 
-val denotation_cs =  comp_cs addss (!simpset addsimps evalc.intrs);
-
-
-(**** Rewrite Rules for C ****)
-
-val C_simps = map (fn t => t RS eq_reflection)
-  [C_skip,C_assign,C_comp,C_if,C_while]; 
-
 
 (**** mono (Gamma(b,c)) ****)
 
 qed_goalw "Gamma_mono" Denotation.thy [mono_def,Gamma_def]
         "mono (Gamma b c)"
-     (fn _ => [(best_tac comp_cs 1)]);
+     (fn _ => [Fast_tac 1]);
 
 
 goal Denotation.thy "C(WHILE b DO c) = C(IF b THEN c;WHILE b DO c ELSE SKIP)";
@@ -37,38 +29,29 @@
 
 (* start with rule induction *)
 by (etac evalc.induct 1);
-by (rewrite_tac (Gamma_def::C_simps));
-  (* simplification with HOL_ss too agressive *)
-(* skip *)
-by (fast_tac denotation_cs 1);
-(* assign *)
-by (fast_tac denotation_cs 1);
-(* comp *)
-by (fast_tac denotation_cs 1);
-(* if *)
-by (fast_tac denotation_cs 1);
-by (fast_tac denotation_cs 1);
+auto();
 (* while *)
+by(rewtac Gamma_def);
 by (rtac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski RS ssubst)) 1);
-by (fast_tac denotation_cs 1);
+by (Fast_tac 1);
 by (rtac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski RS ssubst)) 1);
-by (fast_tac denotation_cs 1);
+by (Fast_tac 1);
 
 qed "com1";
 
-
 (* Denotational Semantics implies Operational Semantics *)
 
 goal Denotation.thy "!s t. (s,t):C(c) --> <c,s> -c-> t";
 by (com.induct_tac "c" 1);
-by (rewrite_tac C_simps);
-by (ALLGOALS (TRY o fast_tac denotation_cs));
+
+by(ALLGOALS Full_simp_tac);
+by(ALLGOALS (TRY o Fast_tac));
 
 (* while *)
 by (strip_tac 1);
 by (etac (Gamma_mono RSN (2,induct)) 1);
 by (rewtac Gamma_def);  
-by (fast_tac denotation_cs 1);
+by (Fast_tac 1);
 
 qed_spec_mp "com2";
 
@@ -76,5 +59,5 @@
 (**** Proof of Equivalence ****)
 
 goal Denotation.thy "(s,t) : C(c)  =  (<c,s> -c-> t)";
-by (fast_tac (set_cs addEs [com2] addDs [com1]) 1);
+by (fast_tac (!claset addEs [com2] addDs [com1]) 1);
 qed "denotational_is_natural";

--- a/src/HOL/IMP/Expr.ML	Tue Sep 10 11:37:52 1996 +0200
+++ b/src/HOL/IMP/Expr.ML	Tue Sep 10 20:10:29 1996 +0200
@@ -35,7 +35,7 @@
 goal Expr.thy "!n. ((a,s) -a-> n) = (n = A a s)";
 by (aexp.induct_tac "a" 1);                               (* struct. ind. *)
 by (ALLGOALS Simp_tac);                                   (* rewr. Den.   *)
-by (TRYALL (fast_tac (set_cs addSIs (evala.intrs@prems)
+by (TRYALL (fast_tac (!claset addSIs (evala.intrs@prems)
                              addSEs evala_elim_cases)));
 qed_spec_mp "aexp_iff";
 

--- a/src/HOL/IMP/Hoare.ML	Tue Sep 10 11:37:52 1996 +0200
+++ b/src/HOL/IMP/Hoare.ML	Tue Sep 10 20:10:29 1996 +0200
@@ -12,19 +12,15 @@
 goalw Hoare.thy [hoare_valid_def] "!!P c Q. |- {P}c{Q} ==> |= {P}c{Q}";
 by (etac hoare.induct 1);
     by(ALLGOALS Asm_simp_tac);
-  by(fast_tac rel_cs 1);
+  by (Fast_tac 1);
  by (Fast_tac 1);
 by (rtac allI 1);
 by (rtac allI 1);
 by (rtac impI 1);
 by (etac induct2 1);
  br Gamma_mono 1;
-by(prune_params_tac);
-by(rename_tac "s t" 1);
 by (rewtac Gamma_def);  
-by(eres_inst_tac [("x","s")] allE 1);
-by (Step_tac 1);
-  by(ALLGOALS Asm_full_simp_tac);
+by (Fast_tac 1);
 qed "hoare_sound";
 
 goalw Hoare.thy [swp_def] "swp SKIP Q = Q";

--- a/src/HOL/IMP/Natural.ML	Tue Sep 10 11:37:52 1996 +0200
+++ b/src/HOL/IMP/Natural.ML	Tue Sep 10 20:10:29 1996 +0200
@@ -6,18 +6,19 @@
 
 open Natural;
 
+AddIs evalc.intrs;
+
 val evalc_elim_cases = map (evalc.mk_cases com.simps)
    ["<SKIP,s> -c-> t", "<x:=a,s> -c-> t", "<c1;c2, s> -c-> t",
     "<IF b THEN c1 ELSE c2, s> -c-> t"];
 
 val evalc_WHILE_case = evalc.mk_cases com.simps "<WHILE b DO c,s> -c-> t";
 
-val evalc_cs = set_cs addSEs evalc_elim_cases
-                      addEs  [evalc_WHILE_case];
+AddSEs evalc_elim_cases;
 
 (* evaluation of com is deterministic *)
 goal Natural.thy "!!c s t. <c,s> -c-> t ==> (!u. <c,s> -c-> u --> u=t)";
 by (etac evalc.induct 1);
 by (thin_tac "<?c,s2> -c-> s1" 7);
-by (ALLGOALS (deepen_tac evalc_cs 4));
+by (ALLGOALS (deepen_tac (!claset addEs [evalc_WHILE_case]) 4));
 qed_spec_mp "com_det";

--- a/src/HOL/IMP/Transition.ML	Tue Sep 10 11:37:52 1996 +0200
+++ b/src/HOL/IMP/Transition.ML	Tue Sep 10 20:10:29 1996 +0200
@@ -10,23 +10,23 @@
 
 section "Winskel's Proof";
 
-val relpow_cs = rel_cs addSEs [rel_pow_0_E];
-
-val evalc1_elim_cases = map (evalc1.mk_cases com.simps)
-   ["(SKIP,s) -1-> t", "(x:=a,s) -1-> t", "(c1;c2, s) -1-> t",
-    "(IF b THEN c1 ELSE c2, s) -1-> t", "(WHILE b DO c,s) -1-> t"];
+AddSEs [rel_pow_0_E];
 
-val evalc1_cs = relpow_cs addIs ([e-mail]);
+val evalc1_SEs = map (evalc1.mk_cases com.simps)
+   ["(SKIP,s) -1-> t", "(x:=a,s) -1-> t","(c1;c2, s) -1-> t", 
+    "(IF b THEN c1 ELSE c2, s) -1-> t"];
+val evalc1_Es = map (evalc1.mk_cases com.simps)
+   ["(WHILE b DO c,s) -1-> t"];
 
-goal Transition.thy "!!c. (c,s) -0-> (SKIP,u) ==> c = SKIP & s = u";
-by(fast_tac evalc1_cs 1);
-val hlemma1 = result();
+AddSEs evalc1_SEs;
+
+AddIs evalc1.intrs;
 
 goal Transition.thy "!!s. (SKIP,s) -m-> (SKIP,t) ==> s = t & m = 0";
 be rel_pow_E2 1;
 by (Asm_full_simp_tac 1);
-by (eresolve_tac evalc1_elim_cases 1);
-val hlemma2 = result();
+by(Fast_tac 1);
+val hlemma = result();
 
 
 goal Transition.thy
@@ -34,11 +34,11 @@
 \              (c;d, s) -*-> (SKIP, u)";
 by(nat_ind_tac "n" 1);
  (* case n = 0 *)
- by(fast_tac (evalc1_cs addIs [rtrancl_into_rtrancl2])1);
+ by(fast_tac (!claset addIs [rtrancl_into_rtrancl2])1);
 (* induction step *)
-by (safe_tac (HOL_cs addSDs [rel_pow_Suc_D2]));
+by (safe_tac (!claset addSDs [rel_pow_Suc_D2]));
 by(split_all_tac 1);
-by(fast_tac (evalc1_cs addIs [rtrancl_into_rtrancl2]) 1);
+by(fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1);
 qed_spec_mp "lemma1";
 
 
@@ -49,18 +49,18 @@
 br rtrancl_refl 1;
 
 (* ASSIGN *)
-by (fast_tac (evalc1_cs addSIs [r_into_rtrancl]) 1);
+by (fast_tac (!claset addSIs [r_into_rtrancl]) 1);
 
 (* SEMI *)
-by (fast_tac (set_cs addDs [rtrancl_imp_UN_rel_pow] addIs [lemma1]) 1);
+by (fast_tac (!claset addDs [rtrancl_imp_UN_rel_pow] addIs [lemma1]) 1);
 
 (* IF *)
-by (fast_tac (evalc1_cs addIs [rtrancl_into_rtrancl2]) 1);
-by (fast_tac (evalc1_cs addIs [rtrancl_into_rtrancl2]) 1);
+by (fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1);
+by (fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1);
 
 (* WHILE *)
-by (fast_tac (evalc1_cs addSIs [r_into_rtrancl]) 1);
-by (fast_tac (evalc1_cs addDs [rtrancl_imp_UN_rel_pow]
+by (fast_tac (!claset addSIs [r_into_rtrancl]) 1);
+by (fast_tac (!claset addDs [rtrancl_imp_UN_rel_pow]
                         addIs [rtrancl_into_rtrancl2,lemma1]) 1);
 
 qed "evalc_impl_evalc1";
@@ -71,33 +71,31 @@
 \            (? t m. (c,s) -*-> (SKIP,t) & (d,t) -m-> (SKIP,u) & m <= n)";
 by(nat_ind_tac "n" 1);
  (* case n = 0 *)
- by (fast_tac (HOL_cs addSDs [hlemma1] addss !simpset) 1);
+ by (fast_tac (!claset addss !simpset) 1);
 (* induction step *)
-by (fast_tac (HOL_cs addSIs [rtrancl_refl,le_SucI,le_refl]
+by (fast_tac (!claset addSIs [le_SucI,le_refl]
                      addSDs [rel_pow_Suc_D2]
-                     addSEs (evalc1_elim_cases@
-                             [rel_pow_imp_rtrancl,rtrancl_into_rtrancl2])) 1);
+                     addSEs [rel_pow_imp_rtrancl,rtrancl_into_rtrancl2]) 1);
 qed_spec_mp "lemma2";
 
 goal Transition.thy "!s t. (c,s) -*-> (SKIP,t) --> <c,s> -c-> t";
 by (com.induct_tac "c" 1);
-by (safe_tac (evalc1_cs addSDs [rtrancl_imp_UN_rel_pow]));
+by (safe_tac (!claset addSDs [rtrancl_imp_UN_rel_pow]));
 
 (* SKIP *)
-by (fast_tac (evalc1_cs addSEs rel_pow_E2::evalc1_elim_cases) 1);
+by (fast_tac (!claset addSEs [rel_pow_E2]) 1);
 
 (* ASSIGN *)
-by (fast_tac (evalc1_cs addSDs [hlemma2]
-                        addSEs rel_pow_E2::evalc1_elim_cases
-                        addss !simpset) 1);
+by (fast_tac (!claset addSDs [hlemma]  addSEs [rel_pow_E2]
+                      addss !simpset) 1);
 
 (* SEMI *)
-by (fast_tac (evalc1_cs addSDs [lemma2,rel_pow_imp_rtrancl]) 1);
+by (fast_tac (!claset addSDs [lemma2,rel_pow_imp_rtrancl]) 1);
 
 (* IF *)
 be rel_pow_E2 1;
 by (Asm_full_simp_tac 1);
-by (fast_tac (evalc1_cs addSDs[rel_pow_imp_rtrancl]addEs evalc1_elim_cases) 1);
+by (fast_tac (!claset addSDs [rel_pow_imp_rtrancl]) 1);
 
 (* WHILE, induction on the length of the computation *)
 by(rotate_tac 1 1);
@@ -107,13 +105,13 @@
 by (strip_tac 1);
 be rel_pow_E2 1;
  by (Asm_full_simp_tac 1);
-by (eresolve_tac evalc1_elim_cases 1);
+by (eresolve_tac evalc1_Es 1);
 
 (* WhileFalse *)
- by (fast_tac (evalc1_cs addSDs [hlemma2]) 1);
+ by (fast_tac (!claset addSDs [hlemma]) 1);
 
 (* WhileTrue *)
-by(fast_tac(evalc1_cs addSDs[lemma2,le_imp_less_or_eq,less_Suc_eq RS iffD2])1);
+by(fast_tac(!claset addSDs[lemma2,le_imp_less_or_eq,less_Suc_eq RS iffD2])1);
 
 qed_spec_mp "evalc1_impl_evalc";
 
@@ -131,8 +129,8 @@
  "!!c1. (c1,s1) -*-> (SKIP,s2) ==> \
 \ (c2,s2) -*-> cs3 --> (c1;c2,s1) -*-> cs3";
 be converse_rtrancl_induct2 1;
-by(fast_tac (evalc1_cs addIs [rtrancl_into_rtrancl2]) 1);
-by(fast_tac (evalc1_cs addIs [rtrancl_into_rtrancl2]) 1);
+by(fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1);
+by(fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1);
 qed_spec_mp "my_lemma1";
 
 
@@ -143,18 +141,18 @@
 br rtrancl_refl 1;
 
 (* ASSIGN *)
-by (fast_tac (evalc1_cs addSIs [r_into_rtrancl]) 1);
+by (fast_tac (!claset addSIs [r_into_rtrancl]) 1);
 
 (* SEMI *)
-by (fast_tac (HOL_cs addIs [my_lemma1]) 1);
+by (fast_tac (!claset addIs [my_lemma1]) 1);
 
 (* IF *)
-by (fast_tac (evalc1_cs addIs [rtrancl_into_rtrancl2]) 1);
-by (fast_tac (evalc1_cs addIs [rtrancl_into_rtrancl2]) 1);
+by (fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1);
+by (fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1);
 
 (* WHILE *)
-by (fast_tac (evalc1_cs addSIs [r_into_rtrancl]) 1);
-by (fast_tac (evalc1_cs addIs [rtrancl_into_rtrancl2,my_lemma1]) 1);
+by (fast_tac (!claset addSIs [r_into_rtrancl]) 1);
+by (fast_tac (!claset addIs [rtrancl_into_rtrancl2,my_lemma1]) 1);
 
 qed "evalc_impl_evalc1";
 
@@ -196,17 +194,16 @@
 goal Transition.thy 
   "!!c s. ((c,s) -1-> (c',s')) ==> (!t. <c',s'> -c-> t --> <c,s> -c-> t)";
 be evalc1.induct 1;
-by(ALLGOALS(fast_tac (evalc1_cs addEs (evalc_elim_cases@evalc1_elim_cases)
-                                addss !simpset)));
+auto();
 qed_spec_mp "FB_lemma3";
 
 val [major] = goal Transition.thy
   "(c,s) -*-> (c',s') ==> <c',s'> -c-> t --> <c,s> -c-> t";
 br (major RS rtrancl_induct2) 1;
-by(fast_tac prod_cs 1);
-by(fast_tac (prod_cs addIs [FB_lemma3] addbefore (split_all_tac 1)) 1);
+by(Fast_tac 1);
+by(fast_tac (!claset addIs [FB_lemma3] addbefore (split_all_tac 1)) 1);
 qed_spec_mp "FB_lemma2";
 
 goal Transition.thy "!!c. (c,s) -*-> (SKIP,t) ==> <c,s> -c-> t";
-by (fast_tac (evalc1_cs addEs [FB_lemma2]) 1);
+by (fast_tac (!claset addEs [FB_lemma2]) 1);
 qed "evalc1_impl_evalc";

--- a/src/HOL/IMP/VC.ML	Tue Sep 10 11:37:52 1996 +0200
+++ b/src/HOL/IMP/VC.ML	Tue Sep 10 20:10:29 1996 +0200
@@ -8,34 +8,25 @@
 
 open VC;
 
-val lemma = prove_goal HOL.thy "!s.P s --> P s" (K[fast_tac HOL_cs 1]);
+AddIs hoare.intrs;
+
+val lemma = prove_goal HOL.thy "!s.P s --> P s" (K[Fast_tac 1]);
 
 goal VC.thy "!Q. (!s. vc c Q s) --> |- {wp c Q} astrip c {Q}";
 by(acom.induct_tac "c" 1);
     by(ALLGOALS Simp_tac);
-    by(fast_tac (HOL_cs addIs hoare.intrs) 1);
-   by(fast_tac (HOL_cs addIs hoare.intrs) 1);
-  by(fast_tac (HOL_cs addIs hoare.intrs) 1);
+    by(Fast_tac 1);
+   by(Fast_tac 1);
+  by(Fast_tac 1);
  (* if *)
- br allI 1;
- br impI 1;
- brs hoare.intrs 1;
-  brs hoare.intrs 1;
-    by(fast_tac HOL_cs 2);
-   by(fast_tac HOL_cs 1);
-  by(fast_tac HOL_cs 1);
- brs hoare.intrs 1;
-   by(fast_tac HOL_cs 2);
-  by(fast_tac HOL_cs 1);
- by(fast_tac HOL_cs 1);
+ by(Deepen_tac 4 1);
 (* while *)
 by(safe_tac HOL_cs);
 by (resolve_tac hoare.intrs 1);
   br lemma 1;
  brs hoare.intrs 1;
  brs hoare.intrs 1;
-   by(fast_tac HOL_cs 2);
-  by(ALLGOALS(fast_tac HOL_cs));
+   by(ALLGOALS(fast_tac HOL_cs));
 qed "vc_sound";
 
 goal VC.thy "!P Q. (!s. P s --> Q s) --> (!s. wp c P s --> wp c Q s)";