# HG changeset patch
# User nipkow
# Date 842447827 -7200
# Node ID b50f96543dec7cc23ba21facde2ab69960c767e9
# Parent  8c94c9a5be108baaa9977bafdc7ce752043e06d6
Removed refs to clasets like rel_cs etc. Used implicit claset.

diff -r 8c94c9a5be10 -r b50f96543dec src/HOL/Lambda/Commutation.ML
--- a/src/HOL/Lambda/Commutation.ML	Tue Sep 10 20:10:29 1996 +0200
+++ b/src/HOL/Lambda/Commutation.ML	Wed Sep 11 15:17:07 1996 +0200
@@ -11,53 +11,47 @@
 (*** square ***)
 
 goalw Commutation.thy [square_def] "!!R. square R S T U ==> square S R U T";
-by(fast_tac HOL_cs 1);
+by(Fast_tac 1);
 qed "square_sym";
 
 goalw Commutation.thy [square_def]
   "!!R. [| square R S T U; T <= T' |] ==> square R S T' U";
-by(fast_tac set_cs 1);
+by(Fast_tac 1);
 qed "square_subset";
 
 goalw Commutation.thy [square_def]
   "!!R. [| square R S T (R^=); S <= T |] ==> square (R^=) S T (R^=)";
-by(fast_tac rel_cs 1);
+by(Fast_tac 1);
 qed "square_reflcl";
 
 goalw Commutation.thy [square_def]
   "!!R. square R S S T ==> square (R^*) S S (T^*)";
 by(strip_tac 1);
 by (etac rtrancl_induct 1);
-by(fast_tac trancl_cs 1);
-by(fast_tac (HOL_cs addSEs [rtrancl_into_rtrancl]) 1);
+by(Fast_tac 1);
+by(best_tac (!claset addSEs [rtrancl_into_rtrancl]) 1);
 qed "square_rtrancl";
 
 goalw Commutation.thy [commute_def]
  "!!R. square R S (S^*) (R^=) ==> commute (R^*) (S^*)";
-by (dtac square_reflcl 1);
-by (rtac subsetI 1);
-by (etac r_into_rtrancl 1);
-by (dtac square_sym 1);
-by (dtac square_rtrancl 1);
-by(Asm_full_simp_tac 1);
-by (dtac square_sym 1);
-by (dtac square_rtrancl 1);
-by(Asm_full_simp_tac 1);
+by(fast_tac (!claset addDs [square_reflcl,square_sym RS square_rtrancl]
+                     addEs [r_into_rtrancl]
+                     addss !simpset) 1);
 qed "square_rtrancl_reflcl_commute";
 
 (*** commute ***)
 
 goalw Commutation.thy [commute_def] "!!R. commute R S ==> commute S R";
-by(fast_tac (HOL_cs addIs [square_sym]) 1);
+by(fast_tac (!claset addIs [square_sym]) 1);
 qed "commute_sym";
 
 goalw Commutation.thy [commute_def] "!!R. commute R S ==> commute (R^*) (S^*)";
-by(fast_tac (HOL_cs addIs [square_rtrancl,square_sym]) 1);
+by(fast_tac (!claset addIs [square_rtrancl,square_sym]) 1);
 qed "commute_rtrancl";
 
 goalw Commutation.thy [commute_def,square_def]
   "!!R. [| commute R T; commute S T |] ==> commute (R Un S) T";
-by(fast_tac set_cs 1);
+by(Fast_tac 1);
 qed "commute_Un";
 
 (*** diamond, confluence and union ***)
@@ -73,7 +67,7 @@
 
 goalw Commutation.thy [diamond_def]
   "!!R. square R R (R^=) (R^=) ==> confluent R";
-by(fast_tac (trancl_cs addIs [square_rtrancl_reflcl_commute,r_into_rtrancl]
+by(fast_tac (!claset addIs [square_rtrancl_reflcl_commute,r_into_rtrancl]
                        addEs [square_subset]) 1);
 qed "square_reflcl_confluent";
 
@@ -81,13 +75,13 @@
  "!!R. [| confluent R; confluent S; commute (R^*) (S^*) |] \
 \      ==> confluent(R Un S)";
 br (rtrancl_Un_rtrancl RS subst) 1;
-by (fast_tac (HOL_cs addDs [diamond_Un] addIs [diamond_confluent]) 1);
+by (fast_tac (!claset addDs [diamond_Un] addIs [diamond_confluent]) 1);
 qed "confluent_Un";
 
 goal Commutation.thy
   "!!R.[| diamond(R); T <= R; R <= T^* |] ==> confluent(T)";
-by(fast_tac (HOL_cs addIs [diamond_confluent]
-                    addDs [rtrancl_subset RS sym] addss HOL_ss) 1);
+by(fast_tac (!claset addIs [diamond_confluent]
+                    addDs [rtrancl_subset RS sym] addss !simpset) 1);
 qed "diamond_to_confluence";
 
 (*** Church_Rosser ***)
@@ -100,7 +94,7 @@
        rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD])1);
 by(safe_tac HOL_cs);
 by (etac rtrancl_induct 1);
- by(fast_tac trancl_cs 1);
-by(slow_tac (rel_cs addIs [r_into_rtrancl]
+ by(Fast_tac 1);
+by(slow_best_tac (!claset addIs [r_into_rtrancl]
                     addEs [rtrancl_trans,r_into_rtrancl RS rtrancl_trans]) 1);
 qed "Church_Rosser_confluent";
diff -r 8c94c9a5be10 -r b50f96543dec src/HOL/Lambda/Eta.ML
--- a/src/HOL/Lambda/Eta.ML	Tue Sep 10 20:10:29 1996 +0200
+++ b/src/HOL/Lambda/Eta.ML	Wed Sep 11 15:17:07 1996 +0200
@@ -20,8 +20,8 @@
 val beta_cases = map (beta.mk_cases db.simps)
     ["s @ t -> u","Var i -> t"];
 
-val eta_cs = lambda_cs addIs eta.intrs
-                       addSEs (beta_cases@eta_cases);
+AddIs eta.intrs;
+AddSEs (beta_cases@eta_cases);
 
 section "Arithmetic lemmas";
 
@@ -122,7 +122,7 @@
 goalw Eta.thy [square_def,id_def]  "square eta eta (eta^=) (eta^=)";
 by (rtac (impI RS allI RS allI) 1);
 by (etac eta.induct 1);
-by(ALLGOALS(fast_tac (eta_cs addSEs [eta_decr,not_free_eta] addss !simpset)));
+by(ALLGOALS(fast_tac (!claset addSEs [eta_decr,not_free_eta] addss !simpset)));
 val lemma = result();
 
 goal Eta.thy "confluent(eta)";
@@ -133,22 +133,22 @@
 
 goal Eta.thy "!!s. s -e>> s' ==> Fun s -e>> Fun s'";
 by (etac rtrancl_induct 1);
-by (ALLGOALS(fast_tac (eta_cs addIs [rtrancl_refl,rtrancl_into_rtrancl])));
+by (ALLGOALS(fast_tac (!claset addIs [rtrancl_refl,rtrancl_into_rtrancl])));
 qed "rtrancl_eta_Fun";
 
 goal Eta.thy "!!s. s -e>> s' ==> s @ t -e>> s' @ t";
 by (etac rtrancl_induct 1);
-by (ALLGOALS(fast_tac (eta_cs addIs [rtrancl_refl,rtrancl_into_rtrancl])));
+by (ALLGOALS(fast_tac (!claset addIs [rtrancl_refl,rtrancl_into_rtrancl])));
 qed "rtrancl_eta_AppL";
 
 goal Eta.thy "!!s. t -e>> t' ==> s @ t -e>> s @ t'";
 by (etac rtrancl_induct 1);
-by (ALLGOALS(fast_tac (eta_cs addIs [rtrancl_refl,rtrancl_into_rtrancl])));
+by (ALLGOALS(fast_tac (!claset addIs [rtrancl_refl,rtrancl_into_rtrancl])));
 qed "rtrancl_eta_AppR";
 
 goal Eta.thy "!!s. [| s -e>> s'; t -e>> t' |] ==> s @ t -e>> s' @ t'";
-by (fast_tac (eta_cs addSIs [rtrancl_eta_AppL,rtrancl_eta_AppR]
-                     addIs [rtrancl_trans]) 1);
+by (deepen_tac (!claset addSIs [rtrancl_eta_AppL,rtrancl_eta_AppR]
+                     addIs [rtrancl_trans]) 2 1);
 qed "rtrancl_eta_App";
 
 section "Commutation of -> and -e>";
@@ -196,9 +196,9 @@
 goal Eta.thy "!s t i. s -e> t --> u[s/i] -e>> u[t/i]";
 by(db.induct_tac "u" 1);
 by(ALLGOALS(asm_simp_tac (addsplit (!simpset))));
-by(fast_tac (eta_cs addIs [r_into_rtrancl]) 1);
-by(fast_tac (eta_cs addSIs [rtrancl_eta_App]) 1);
-by(fast_tac (eta_cs addSIs [rtrancl_eta_Fun,eta_lift]) 1);
+by(fast_tac (!claset addIs [r_into_rtrancl]) 1);
+by(fast_tac (!claset addSIs [rtrancl_eta_App]) 1);
+by(fast_tac (!claset addSIs [rtrancl_eta_Fun,eta_lift]) 1);
 qed_spec_mp "rtrancl_eta_subst";
 
 goalw Eta.thy [square_def] "square beta eta (eta^*) (beta^=)";
@@ -207,12 +207,12 @@
 by(strip_tac 1);
 by (eresolve_tac eta_cases 1);
 by (eresolve_tac eta_cases 1);
-by(fast_tac (eta_cs addss (!simpset addsimps [subst_decr])) 1);
-by(fast_tac (eta_cs addIs [r_into_rtrancl,eta_subst]) 1);
-by(fast_tac (eta_cs addIs [rtrancl_eta_subst]) 1);
-by(fast_tac (eta_cs addIs [r_into_rtrancl,rtrancl_eta_AppL]) 1);
-by(fast_tac (eta_cs addIs [r_into_rtrancl,rtrancl_eta_AppR]) 1);
-by(fast_tac (eta_cs addIs [r_into_rtrancl,rtrancl_eta_Fun,free_beta,beta_decr]
+by(fast_tac (!claset addss (!simpset addsimps [subst_decr])) 1);
+by(slow_tac (!claset addIs [r_into_rtrancl,eta_subst]) 1);
+by(slow_tac (!claset addIs [rtrancl_eta_subst]) 1);
+by(slow_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_AppL]) 1);
+by(slow_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_AppR]) 1);
+by(slow_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_Fun,free_beta,beta_decr]
                   addss (!simpset addsimps[subst_decr,symmetric decr_def])) 1);
 qed "square_beta_eta";
 
diff -r 8c94c9a5be10 -r b50f96543dec src/HOL/Lambda/Lambda.ML
--- a/src/HOL/Lambda/Lambda.ML	Tue Sep 10 20:10:29 1996 +0200
+++ b/src/HOL/Lambda/Lambda.ML	Wed Sep 11 15:17:07 1996 +0200
@@ -47,11 +47,11 @@
 
 open Lambda;
 
-Delsimps [(*less_Suc_eq, *)subst_Var];
+Delsimps [subst_Var];
 Addsimps ([if_not_P, not_less_eq] @ beta.intrs);
 
 (* don't add r_into_rtrancl! *)
-val lambda_cs = trancl_cs addSIs beta.intrs;
+AddSIs beta.intrs;
 
 val db_case_distinction =
   rule_by_tactic(EVERY[etac thin_rl 2,etac thin_rl 2,etac thin_rl 3])db.induct;
@@ -60,23 +60,25 @@
 
 goal Lambda.thy "!!s. s ->> s' ==> Fun s ->> Fun s'";
 by (etac rtrancl_induct 1);
-by (ALLGOALS(fast_tac (lambda_cs addIs [rtrancl_refl,rtrancl_into_rtrancl])));
+by (ALLGOALS(fast_tac (!claset addIs [rtrancl_into_rtrancl])));
 qed "rtrancl_beta_Fun";
+AddSIs [rtrancl_beta_Fun];
 
 goal Lambda.thy "!!s. s ->> s' ==> s @ t ->> s' @ t";
 by (etac rtrancl_induct 1);
-by (ALLGOALS(fast_tac (lambda_cs addIs [rtrancl_refl,rtrancl_into_rtrancl])));
+by (ALLGOALS(fast_tac (!claset addIs [rtrancl_into_rtrancl])));
 qed "rtrancl_beta_AppL";
 
 goal Lambda.thy "!!s. t ->> t' ==> s @ t ->> s @ t'";
 by (etac rtrancl_induct 1);
-by (ALLGOALS(fast_tac (lambda_cs addIs [rtrancl_refl,rtrancl_into_rtrancl])));
+by (ALLGOALS(fast_tac (!claset addIs [rtrancl_into_rtrancl])));
 qed "rtrancl_beta_AppR";
 
 goal Lambda.thy "!!s. [| s ->> s'; t ->> t' |] ==> s @ t ->> s' @ t'";
-by (fast_tac (lambda_cs addSIs [rtrancl_beta_AppL,rtrancl_beta_AppR]
-                        addIs  [rtrancl_trans]) 1);
+by (deepen_tac (!claset addSIs [rtrancl_beta_AppL,rtrancl_beta_AppR]
+                        addIs  [rtrancl_trans]) 3 1);
 qed "rtrancl_beta_App";
+AddIs [rtrancl_beta_App];
 
 (*** subst and lift ***)
 
diff -r 8c94c9a5be10 -r b50f96543dec src/HOL/Lambda/Lambda.thy
--- a/src/HOL/Lambda/Lambda.thy	Tue Sep 10 20:10:29 1996 +0200
+++ b/src/HOL/Lambda/Lambda.thy	Wed Sep 11 15:17:07 1996 +0200
@@ -36,7 +36,7 @@
 
 primrec substn db
   "substn (Var i) s k = (if k < i then Var(pred i)
-                                    else if i = k then liftn k s 0 else Var i)"
+                         else if i = k then liftn k s 0 else Var i)"
   "substn (t @ u) s k = (substn t s k) @ (substn u s k)"
   "substn (Fun t) s k = Fun (substn t s (Suc k))"
 
diff -r 8c94c9a5be10 -r b50f96543dec src/HOL/Lambda/ParRed.ML
--- a/src/HOL/Lambda/ParRed.ML	Tue Sep 10 20:10:29 1996 +0200
+++ b/src/HOL/Lambda/ParRed.ML	Wed Sep 11 15:17:07 1996 +0200
@@ -15,12 +15,13 @@
     ["Var n => t", "Fun s => Fun t",
      "(Fun s) @ t => u", "s @ t => u", "Fun s => t"];
 
-val parred_cs = lambda_cs addSIs par_beta.intrs addSEs par_beta_cases;
+AddSIs par_beta.intrs;
+AddSEs par_beta_cases;
 
 (*** beta <= par_beta <= beta^* ***)
 
 goal ParRed.thy "(Var n => t) = (t = Var n)";
-by(fast_tac parred_cs 1);
+by(Fast_tac 1);
 qed "par_beta_varL";
 Addsimps [par_beta_varL];
 
@@ -29,30 +30,28 @@
 by(ALLGOALS Asm_simp_tac);
 qed"par_beta_refl";
 Addsimps [par_beta_refl];
+(* AddSIs [par_beta_refl]; causes search to blow up *)
 
 goal ParRed.thy "beta <= par_beta";
 by (rtac subsetI 1);
 by (split_all_tac 1);
 by (etac beta.induct 1);
-by (ALLGOALS(fast_tac (parred_cs addSIs [par_beta_refl])));
+by (ALLGOALS(fast_tac (!claset addSIs [par_beta_refl])));
 qed "beta_subset_par_beta";
 
 goal ParRed.thy "par_beta <= beta^*";
 by (rtac subsetI 1);
 by (split_all_tac 1);
 by (etac par_beta.induct 1);
-by (ALLGOALS
-    (fast_tac (parred_cs addIs
-	                  [rtrancl_beta_Fun,rtrancl_beta_App,rtrancl_refl,
-			   rtrancl_into_rtrancl] 
-                         addEs [rtrancl_trans])));
+by (ALLGOALS (slow_best_tac (!claset addIs [rtrancl_into_rtrancl] 
+                                     addEs [rtrancl_trans])));
 qed "par_beta_subset_beta";
 
 (*** => ***)
 
 goal ParRed.thy "!t' n. t => t' --> lift t n => lift t' n";
 by(db.induct_tac "t" 1);
-by(ALLGOALS(fast_tac (parred_cs addss (!simpset))));
+by(ALLGOALS(fast_tac (!claset addss (!simpset))));
 qed_spec_mp "par_beta_lift";
 Addsimps [par_beta_lift];
 
@@ -64,8 +63,8 @@
  bes par_beta_cases 1;
   by(Asm_simp_tac 1);
  by(asm_simp_tac (!simpset addsimps [subst_subst RS sym]) 1);
- by(fast_tac (parred_cs addSIs [par_beta_lift] addss (!simpset)) 1);
-by(fast_tac (parred_cs addss (!simpset)) 1);
+ by(fast_tac (!claset addSIs [par_beta_lift] addss (!simpset)) 1);
+by(fast_tac (!claset addss (!simpset)) 1);
 qed_spec_mp "par_beta_subst";
 
 (*** Confluence (directly) ***)
@@ -73,7 +72,7 @@
 goalw ParRed.thy [diamond_def,commute_def,square_def] "diamond(par_beta)";
 by (rtac (impI RS allI RS allI) 1);
 by (etac par_beta.induct 1);
-by(ALLGOALS(fast_tac (parred_cs addSIs [par_beta_subst])));
+by(ALLGOALS(fast_tac (!claset addSIs [par_beta_subst])));
 qed "diamond_par_beta";
 
 
@@ -84,7 +83,7 @@
   by(Simp_tac 1);
  be rev_mp 1;
  by(db.induct_tac "db1" 1);
- by(ALLGOALS(fast_tac (parred_cs addSIs [par_beta_subst] addss (!simpset))));
+ by(ALLGOALS(fast_tac (!claset addSIs [par_beta_subst] addss !simpset)));
 qed_spec_mp "par_beta_cd";
 
 (*** Confluence (via cd) ***)