repaired critical proofs depending on the order inside non-confluent SimpSets

--- a/src/HOL/IOA/ABP/Correctness.ML	Tue Apr 23 16:58:21 1996 +0200
+++ b/src/HOL/IOA/ABP/Correctness.ML	Tue Apr 23 16:58:57 1996 +0200
@@ -227,6 +227,9 @@
 goal Correctness.thy 
       "is_weak_pmap (%id.id) sender_ioa sender_ioa";
 by (simp_tac (!simpset addsimps [Solve.is_weak_pmap_def]) 1);
+by (rtac conjI 1);
+(* start states *)
+by (fast_tac set_cs 1);
 (* main-part *)
 by (REPEAT (rtac allI 1));
 by (rtac imp_conj_lemma 1);
@@ -239,6 +242,9 @@
 goal Correctness.thy 
       "is_weak_pmap (%id.id) receiver_ioa receiver_ioa";
 by (simp_tac (!simpset addsimps [Solve.is_weak_pmap_def]) 1);
+by (rtac conjI 1);
+ (* start states *)
+by (fast_tac set_cs 1);
 (* main-part *)
 by (REPEAT (rtac allI 1));
 by (rtac imp_conj_lemma 1);
@@ -250,6 +256,9 @@
 goal Correctness.thy 
       "is_weak_pmap (%id.id) env_ioa env_ioa";
 by (simp_tac (!simpset addsimps [Solve.is_weak_pmap_def]) 1);
+by (rtac conjI 1);
+(* start states *)
+by (fast_tac set_cs 1);
 (* main-part *)
 by (REPEAT (rtac allI 1));
 by (rtac imp_conj_lemma 1);

--- a/src/HOL/IOA/NTP/Lemmas.ML	Tue Apr 23 16:58:21 1996 +0200
+++ b/src/HOL/IOA/NTP/Lemmas.ML	Tue Apr 23 16:58:57 1996 +0200
@@ -164,7 +164,7 @@
 
 goal Arith.thy "x < Suc(y) --> x<=y";
   by (nat_ind_tac "n" 1);
-  by (Asm_simp_tac 1);
+  by (asm_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
   by (safe_tac HOL_cs);
   by (etac less_imp_le 1);
 qed "less_suc_imp_leq";

--- a/src/HOL/IOA/meta_theory/IOA.ML	Tue Apr 23 16:58:21 1996 +0200
+++ b/src/HOL/IOA/meta_theory/IOA.ML	Tue Apr 23 16:58:57 1996 +0200
@@ -59,16 +59,16 @@
 \                         %i.if i<Suc n then snd ex i else t)")] bexI 1);
   by(res_inst_tac [("x","Suc(n)")] exI 1);
   by(Simp_tac 1);
-  by(asm_simp_tac (!simpset delsimps [less_Suc_eq]) 1);
+  by(asm_simp_tac (!simpset (*delsimps [less_Suc_eq]*)) 1);
   by(REPEAT(rtac allI 1));
   by(res_inst_tac [("m","na"),("n","n")] (make_elim less_linear) 1);
   be disjE 1;
-  by(Asm_simp_tac 1);
+  by(asm_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
   be disjE 1;
   by(Asm_simp_tac 1);
   by(fast_tac HOL_cs 1);
   by(forward_tac [less_not_sym] 1);
-  by(asm_simp_tac (!simpset addsimps [less_not_refl2]) 1);
+  by(asm_simp_tac (!simpset addsimps [less_not_refl2,less_Suc_eq]) 1);
 qed "reachable_n";
 
 val [p1,p2] = goalw IOA.thy [invariant_def]

--- a/src/HOL/Lambda/Eta.ML	Tue Apr 23 16:58:21 1996 +0200
+++ b/src/HOL/Lambda/Eta.ML	Tue Apr 23 16:58:57 1996 +0200
@@ -32,14 +32,14 @@
 
 goal Arith.thy "i < j --> pred i < j";
 by(nat_ind_tac "j" 1);
-by(ALLGOALS(asm_simp_tac(simpset_of "Arith")));
+by(ALLGOALS(asm_simp_tac(simpset_of "Arith" addsimps [less_Suc_eq])));
 by(nat_ind_tac "j1" 1);
 by(ALLGOALS(asm_simp_tac(simpset_of "Arith")));
 qed_spec_mp "less_imp_pred_less";
 
 goal Arith.thy "i<j --> ~ pred j < i";
 by(nat_ind_tac "j" 1);
-by(ALLGOALS(asm_simp_tac(simpset_of "Arith")));
+by(ALLGOALS(asm_simp_tac(simpset_of "Arith" addsimps [less_Suc_eq])));
 by(fast_tac (HOL_cs addDs [less_imp_pred_less]) 1);
 qed_spec_mp "less_imp_not_pred_less";
 Addsimps [less_imp_not_pred_less];
@@ -47,6 +47,7 @@
 goal Nat.thy "i < j --> j < Suc(Suc i) --> j = Suc i";
 by(nat_ind_tac "j" 1);
 by(ALLGOALS(simp_tac(simpset_of "Nat")));
+by(simp_tac(simpset_of "Nat" addsimps [less_Suc_eq])1);
 by(fast_tac (HOL_cs addDs [less_not_sym]) 1);
 qed_spec_mp "less_interval1";
 
@@ -179,8 +180,7 @@
 
 goal Eta.thy "!i. ~free t (Suc i) --> decr t i = decr t (Suc i)";
 by(db.induct_tac "t" 1);
-by(ALLGOALS(asm_simp_tac (addsplit (!simpset) addsimps [le_def])));
-by(fast_tac (HOL_cs addDs [less_interval1]) 1);
+by(ALLGOALS(asm_simp_tac (addsplit (!simpset) addsimps [le_def, less_Suc_eq])));
 by(fast_tac HOL_cs 1);
 qed "decr_not_free";
 Addsimps [decr_not_free];

--- a/src/HOL/Lambda/Lambda.ML	Tue Apr 23 16:58:21 1996 +0200
+++ b/src/HOL/Lambda/Lambda.ML	Tue Apr 23 16:58:57 1996 +0200
@@ -14,13 +14,13 @@
 goal Nat.thy "!!i. [| i < Suc j; j < k |] ==> i < k";
 by (rtac le_less_trans 1);
 by (assume_tac 2);
-by(asm_full_simp_tac (!simpset addsimps [le_def]) 1);
+by(asm_full_simp_tac (!simpset addsimps [le_def, less_Suc_eq]) 1);
 by(fast_tac (HOL_cs addEs [less_asym,less_irrefl]) 1);
 qed "lt_trans1";
 
 goal Nat.thy "!!i. [| i < j; j < Suc(k) |] ==> i < k";
 by (etac less_le_trans 1);
-by(asm_full_simp_tac (!simpset addsimps [le_def]) 1);
+by(asm_full_simp_tac (!simpset addsimps [le_def, less_Suc_eq]) 1);
 by(fast_tac (HOL_cs addEs [less_asym,less_irrefl]) 1);
 qed "lt_trans2";
 
@@ -47,7 +47,7 @@
 
 open Lambda;
 
-Delsimps [less_Suc_eq, subst_Var];
+Delsimps [(*less_Suc_eq, *)subst_Var];
 Addsimps ([if_not_P, not_less_eq] @ beta.intrs);
 
 (* don't add r_into_rtrancl! *)

--- a/src/HOL/Lex/AutoChopper.ML	Tue Apr 23 16:58:21 1996 +0200
+++ b/src/HOL/Lex/AutoChopper.ML	Tue Apr 23 16:58:57 1996 +0200
@@ -150,7 +150,8 @@
   by (fast_tac HOL_cs 2);
  by (Simp_tac 2);
 by (subgoal_tac "flat(yss) @ zs = list" 1);
- by (Asm_simp_tac 1);
+ by(hyp_subst_tac 1);
+ by(atac 1);
 by (case_tac "yss = []" 1);
  by (Asm_simp_tac 1);
  by (hyp_subst_tac 1);

--- a/src/HOL/MiniML/I.ML	Tue Apr 23 16:58:21 1996 +0200
+++ b/src/HOL/MiniML/I.ML	Tue Apr 23 16:58:57 1996 +0200
@@ -1,5 +1,8 @@
 open I;
 
+Unify.trace_bound := 45;
+Unify.search_bound := 50;
+
 goal thy
   "! a m s s' t n.  \
 \    (new_tv m a & new_tv m s) --> I e a m s = Ok(s',t,n) -->   \

--- a/src/HOL/Subst/Unifier.ML	Tue Apr 23 16:58:21 1996 +0200
+++ b/src/HOL/Subst/Unifier.ML	Tue Apr 23 16:58:57 1996 +0200
@@ -79,7 +79,8 @@
 
 goal Unifier.thy "Idem(s) = (sdom(s) Int srange(s) = {})";
 by (simp_tac (subst_ss addsimps [raw_Idem_iff,subst_eq_iff,subst_comp,
-                                invariance,dom_range_disjoint])1);
+                                invariance,dom_range_disjoint]
+		       delsimps (empty_iff::mem_simps)) 1);
 qed "Idem_iff";
 
 goal Unifier.thy "Idem([])";

--- a/src/HOL/ex/LList.ML	Tue Apr 23 16:58:21 1996 +0200
+++ b/src/HOL/ex/LList.ML	Tue Apr 23 16:58:57 1996 +0200
@@ -163,7 +163,7 @@
 by (rename_tac "n'" 1);
 by (res_inst_tac [("n", "n'")] natE 1);
 by (asm_simp_tac (!simpset addsimps [CONS_def, ntrunc_one_In1]) 1);
-by (asm_simp_tac (!simpset addsimps [CONS_def, ntrunc_In1, ntrunc_Scons]) 1);
+by (asm_simp_tac (!simpset addsimps [CONS_def, ntrunc_In1, ntrunc_Scons, less_Suc_eq]) 1);
 qed "LListD_implies_ntrunc_equality";
 
 (*The domain of the LListD relation*)
@@ -307,7 +307,7 @@
 by (res_inst_tac [("n", "n")] natE 1);
 by (res_inst_tac [("n", "xb")] natE 2);
 by (ALLGOALS(asm_simp_tac(!simpset addsimps
-            [ntrunc_0,ntrunc_one_CONS,ntrunc_CONS])));
+            [ntrunc_0,ntrunc_one_CONS,ntrunc_CONS, less_Suc_eq])));
 result();
 
 

--- a/src/HOL/ex/Mutil.ML	Tue Apr 23 16:58:21 1996 +0200
+++ b/src/HOL/ex/Mutil.ML	Tue Apr 23 16:58:57 1996 +0200
@@ -108,7 +108,7 @@
 by (res_inst_tac [("x", "i")] spec 1);
 by (nat_ind_tac "k" 1);
 by (Simp_tac 1);
-by (asm_simp_tac (!simpset addsimps [below_Suc]) 1);
+by (asm_simp_tac (!simpset addsimps [below_Suc, less_Suc_eq]) 1);
 by (fast_tac set_cs 1);
 qed "below_less_iff";
 

--- a/src/HOL/ex/Puzzle.ML	Tue Apr 23 16:58:21 1996 +0200
+++ b/src/HOL/ex/Puzzle.ML	Tue Apr 23 16:58:57 1996 +0200
@@ -36,7 +36,7 @@
 val prems = goal Puzzle.thy "(!!n.f(n) <= f(Suc(n))) ==> m<n --> f(m) <= f(n)";
 by (res_inst_tac[("n","n")]nat_induct 1);
 by (Simp_tac 1);
-by (Simp_tac 1);
+by (simp_tac (!simpset addsimps [less_Suc_eq]) 1);
 by (fast_tac (HOL_cs addIs (le_trans::prems)) 1);
 bind_thm("mono_lemma1", result() RS mp);
 

--- a/src/HOL/ex/Qsort.ML	Tue Apr 23 16:58:21 1996 +0200
+++ b/src/HOL/ex/Qsort.ML	Tue Apr 23 16:58:57 1996 +0200
@@ -23,33 +23,41 @@
  "((Alls x:xs.P(x)) & (Alls x:xs.Q(x))) = (Alls x:xs. P(x)&Q(x))";
 by(list.induct_tac "xs" 1);
 by(ALLGOALS Asm_simp_tac);
-Addsimps [result()];
+val alls_lemma=result();
+Addsimps [alls_lemma];
 
-goal HOL.thy "((~P --> Q) & (P --> Q)) = Q";
+goal HOL.thy "((P --> Q) & (~P --> Q)) = Q";
 by(fast_tac HOL_cs 1);
 val lemma = result();
 
 goal Qsort.thy "(Alls x:qsort le xs.P(x))  =  (Alls x:xs.P(x))";
 by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
-by(ALLGOALS(asm_simp_tac (!simpset addsimps [lemma])));
+by(Asm_simp_tac 1);
+by(asm_simp_tac (!simpset delsimps [alls_lemma, list_all_Cons])1);
+by(asm_simp_tac (!simpset addsimps [lemma]) 1);
 Addsimps [result()];
 
 goal Qsort.thy
  "sorted le (xs@ys) = (sorted le xs & sorted le ys & \
 \                     (Alls x:xs. Alls y:ys. le x y))";
 by(list.induct_tac "xs" 1);
-by(ALLGOALS Asm_simp_tac);
+by(Asm_simp_tac 1);
+by(asm_simp_tac (!simpset delsimps [alls_lemma]) 1);
 Addsimps [result()];
 
+
+
+
 goal Qsort.thy 
  "!!le. [| total(le); transf(le) |] ==>  sorted le (qsort le xs)";
 by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
-by(ALLGOALS(asm_full_simp_tac (!simpset addsimps [list_all_mem_conv]) ));
+by(Asm_simp_tac 1);
+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);
 result();
 
-
 (* A verification based on predicate calculus rather than combinators *)
 
 val sorted_Cons =
@@ -68,7 +76,10 @@
  "sorted le (xs@ys) = (sorted le xs & sorted le ys & \
 \                     (!x. x mem xs --> (!y. y mem ys --> le x y)))";
 by(list.induct_tac "xs" 1);
-by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
+by(Asm_simp_tac 1);
+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);
 Addsimps [result()];
 
@@ -76,7 +87,11 @@
   "!!xs. [| total(le); transf(le) |] ==>  sorted le (qsort le xs)";
 by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
 by(Simp_tac 1);
-by(asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by(asm_simp_tac (!simpset setloop (split_tac [expand_if])
+			  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);
 result();
+
+