# HG changeset patch
# User berghofe
# Date 1033397295 -7200
# Node ID 55d32e76ef4e136f79cc51cdb036c250780ea9d8
# Parent  2edf034c902a461709967f1b09971baacaaf0df7
Adapted to new simplifier.

diff -r 2edf034c902a -r 55d32e76ef4e src/HOL/IMP/Machines.thy
--- a/src/HOL/IMP/Machines.thy	Mon Sep 30 16:47:03 2002 +0200
+++ b/src/HOL/IMP/Machines.thy	Mon Sep 30 16:48:15 2002 +0200
@@ -193,7 +193,7 @@
   apply simp
   apply(rule rev_revD)
   apply simp
- apply(clarsimp simp add: neq_Nil_conv append_eq_conv_conj)
+ apply(simp (no_asm_use) add: neq_Nil_conv append_eq_conv_conj, clarify)+
  apply(drule sym)
  apply simp
  apply(rule rev_revD)
diff -r 2edf034c902a -r 55d32e76ef4e src/HOL/IMPP/Hoare.ML
--- a/src/HOL/IMPP/Hoare.ML	Mon Sep 30 16:47:03 2002 +0200
+++ b/src/HOL/IMPP/Hoare.ML	Mon Sep 30 16:48:15 2002 +0200
@@ -179,7 +179,7 @@
 by         (Blast_tac 1); (* cut *)
 by        (Blast_tac 1); (* weaken *)
 by       (ALLGOALS (EVERY'[REPEAT o thin_tac "?x : hoare_derivs", 
-	                   Clarsimp_tac, REPEAT o smp_tac 1]));
+	                   Simp_tac, Clarify_tac, REPEAT o smp_tac 1]));
 by       (ALLGOALS (full_simp_tac (simpset() addsimps [triple_valid_def2])));
 by       (EVERY'[strip_tac, smp_tac 2, Blast_tac] 1); (* conseq *)
 by      (ALLGOALS Clarsimp_tac); (* Skip, Ass, Local *)
@@ -273,10 +273,9 @@
 by  (resolve_tac (premises()(*hoare_derivs.asm*)) 1);
 by  (Fast_tac 1);
 by (resolve_tac (tl(premises())(*MGT_BodyN*)) 1);
-byev[dtac spec 1, etac impE 1, etac impE 2, etac impE 3, dtac spec 4,etac mp 4];
-by   (eresolve_tac (tl(tl(tl(premises())))) 4);
+byev[dtac spec 1, etac impE 1, etac impE 2, dtac spec 3,etac mp 3];
+by   (eresolve_tac (tl(tl(tl(premises())))) 3);
 by   (Fast_tac 1);
-by (etac Suc_leD 1);
 by (dtac finite_subset 1);
 by (etac finite_imageI 1);
 by (Asm_simp_tac 1); 
diff -r 2edf034c902a -r 55d32e76ef4e src/HOL/Induct/LFilter.thy
--- a/src/HOL/Induct/LFilter.thy	Mon Sep 30 16:47:03 2002 +0200
+++ b/src/HOL/Induct/LFilter.thy	Mon Sep 30 16:48:15 2002 +0200
@@ -125,7 +125,6 @@
 
 lemma lfilter_eq_LNil: "lfilter p l = LNil ==> l ~: Domain(findRel p)" 
 apply (auto iff: Domain_findRel_iff)
-apply (rotate_tac 1, simp) 
 done
 
 lemma lfilter_eq_LCons [rule_format]:
diff -r 2edf034c902a -r 55d32e76ef4e src/HOL/Induct/SList.thy
--- a/src/HOL/Induct/SList.thy	Mon Sep 30 16:47:03 2002 +0200
+++ b/src/HOL/Induct/SList.thy	Mon Sep 30 16:48:15 2002 +0200
@@ -875,7 +875,8 @@
 apply (erule all_dupE) 
 apply (rule trans) 
 prefer 2 apply assumption
-apply (simp add: assoc [THEN spec, THEN spec, THEN spec, THEN sym])
+apply (simp (no_asm_use) add: assoc [THEN spec, THEN spec, THEN spec, THEN sym])
+apply simp
 done
 
 lemma foldl_append_sym: 
diff -r 2edf034c902a -r 55d32e76ef4e src/ZF/IMP/Equiv.thy
--- a/src/ZF/IMP/Equiv.thy	Mon Sep 30 16:47:03 2002 +0200
+++ b/src/ZF/IMP/Equiv.thy	Mon Sep 30 16:48:15 2002 +0200
@@ -38,7 +38,7 @@
 
 lemma com1: "<c,sigma> -c-> sigma' ==> <sigma,sigma'> \<in> C(c)"
   apply (erule evalc.induct)
-        apply simp_all
+        apply (simp_all (no_asm_simp))
       txt {* @{text skip} *}
       apply fast
      txt {* @{text assign} *}
diff -r 2edf034c902a -r 55d32e76ef4e src/ZF/Induct/Multiset.ML
--- a/src/ZF/Induct/Multiset.ML	Mon Sep 30 16:47:03 2002 +0200
+++ b/src/ZF/Induct/Multiset.ML	Mon Sep 30 16:48:15 2002 +0200
@@ -51,13 +51,6 @@
 Addsimps [domain_of_fun];
 Delrules [domainE];
 
-(* The following tactic moves the condition `simp_cond' to the begining
-   of the list of hypotheses and then makes simplifications accordingly *)
-
-fun rotate_simp_tac simp_cond i =
-(dres_inst_tac [("psi", simp_cond)] asm_rl i THEN rotate_tac ~1 i
- THEN Asm_full_simp_tac i);
-
 (* A useful simplification rule *)
 
 Goal "(f:A -> nat-{0}) <-> f:A->nat&(ALL a:A. f`a:nat & 0 < f`a)";
@@ -73,7 +66,7 @@
  "[| multiset(M); mset_of(M)<=A |] ==> M:Mult(A)";
 by (auto_tac (claset(), simpset()
              addsimps [multiset_fun_iff, mset_of_def]));
-by (rotate_simp_tac "M:?u" 1);
+by (Asm_full_simp_tac 1);
 by (res_inst_tac [("B1","nat-{0}")] (FiniteFun_mono RS subsetD) 1);
 by (ALLGOALS(Asm_simp_tac));
 by (rtac (Finite_into_Fin RSN (2, Fin_mono RS subsetD) RS fun_FiniteFunI) 1);
@@ -157,7 +150,7 @@
 by (rewtac mset_of_def);
 by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [multiset_fun_iff])));
 by (ALLGOALS(Clarify_tac));
-by (ALLGOALS(rotate_simp_tac "M:?u"));
+by (ALLGOALS Asm_full_simp_tac);
 by Auto_tac;
 qed "mset_of_diff";
 Addsimps [mset_of_diff];
@@ -341,7 +334,7 @@
  "[| multiset(M); a:mset_of(M) |] ==> 0 < mcount(M, a)";
 by (Clarify_tac 1);
 by (rewrite_goals_tac [mcount_def, mset_of_def]);
-by (rotate_simp_tac "M:?u" 1);
+by (Asm_full_simp_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [multiset_fun_iff]) 1); 
 qed "mcount_elem";
 
@@ -441,8 +434,6 @@
 by (rtac sym 1 THEN rtac equalityI 1);
 by (rewrite_goals_tac [mcount_def, mset_of_def]);
 by (auto_tac (claset(), simpset() addsimps [multiset_fun_iff]));
-by (ALLGOALS(rotate_simp_tac "M:?u"));
-by (ALLGOALS(rotate_simp_tac "N:?u"));
 by (ALLGOALS(dres_inst_tac [("x", "x")] spec));
 by (case_tac "x:Aa" 2 THEN case_tac "x:A" 1);
 by Auto_tac;
@@ -455,8 +446,6 @@
 by (blast_tac (claset() addIs [equality_lemma]) 2);
 by (rewrite_goals_tac [multiset_def, mset_of_def]);
 by (auto_tac (claset(), simpset() addsimps [multiset_fun_iff]));
-by (rotate_simp_tac "M:?u" 1);
-by (rotate_simp_tac "N:?u" 1);
 by (rtac fun_extension 1);
 by (Blast_tac 1 THEN Blast_tac 1);
 by (dres_inst_tac [("x", "x")] spec 1);
@@ -535,7 +524,6 @@
 by (rewrite_goals_tac [mset_of_def, mcount_def]);
 by (case_tac "x:A" 1);
 by Auto_tac;
-by (rotate_simp_tac "M:?u" 2);
 by (subgoal_tac "$# M ` x $+ #-1 = $# M ` x $- $# 1" 1);
 by (etac ssubst 1);
 by (rtac int_of_diff 1);
@@ -592,9 +580,6 @@
 by (auto_tac (claset(), 
               simpset() addsimps [mset_of_def, multiset_def,  
                                   multiset_fun_iff, msize_def]@prems));
-by (rotate_simp_tac "M:?u" 1);
-by (rotate_simp_tac "M:?u" 2);
-by (rotate_simp_tac "ALL a:A. ?u(a)" 1);
 by (subgoal_tac "setsum(%x. $# mcount(M, x), A)=$# succ(x)" 1);
 by (dtac setsum_succD 1 THEN Auto_tac);
 by (case_tac "1 <M`a" 1);
@@ -631,9 +616,7 @@
 by (Asm_simp_tac 1);
 by (subgoal_tac "cons(a, A)= A" 1);
 by (Blast_tac 2);
-by (rotate_simp_tac "cons(a, A) = A" 1);
-by (rotate_simp_tac "ALL x:A. ?u(x)" 1);
-by (rotate_simp_tac "ALL x:A. ?u(x)" 2);
+by (Asm_full_simp_tac 1);
 by (subgoal_tac "M=cons(<a, M`a>, funrestrict(M, A-{a}))" 1);
 by (rtac  fun_cons_funrestrict_eq 2);
 by (subgoal_tac "cons(a, A-{a}) = A" 2);
@@ -660,7 +643,7 @@
 by (Blast_tac 1);
 by (asm_simp_tac (simpset() addsimps [mset_of_def]) 1);
 by (dres_inst_tac [("b", "if ?u then ?v else ?w")] sym 1);
-by (ALLGOALS(rotate_simp_tac "ALL x:A. ?u(x)"));
+by (ALLGOALS Asm_full_simp_tac);
 by (subgoal_tac "{x:A - {a} . 0 < funrestrict(M, A - {x}) ` x} = A - {a}" 1);
 by (auto_tac (claset() addSIs [setsum_cong], 
               simpset() addsimps [zdiff_eq_iff, 
@@ -692,7 +675,7 @@
  "[| multiset(M); a ~:mset_of(M) |] ==> M +# {#a#} = cons(<a, 1>, M)";
 by (auto_tac (claset(), simpset() addsimps [munion_def]));
 by (rewtac mset_of_def);
-by (rotate_simp_tac "M:?u" 1);
+by (Asm_full_simp_tac 1);
 by (rtac fun_extension 1 THEN rtac lam_type 1);
 by (ALLGOALS(Asm_full_simp_tac));
 by (auto_tac (claset(), simpset()  
@@ -707,7 +690,7 @@
 by (auto_tac (claset(),  simpset() 
      addsimps [munion_def, multiset_fun_iff, msingle_def]));
 by (rewtac mset_of_def);
-by (rotate_simp_tac "M:?u" 1);
+by (Asm_full_simp_tac 1);
 by (subgoal_tac "A Un {a} = A" 1);
 by (rtac fun_extension 1);
 by (auto_tac (claset() addDs [domain_type] 
@@ -767,7 +750,6 @@
 Goalw [multiset_def, mset_of_def]
  "[| multiset(M); a:mset_of(M) |] ==> natify(M`a) = M`a";
 by (auto_tac (claset(), simpset() addsimps [multiset_fun_iff]));
-by (rotate_simp_tac "M:?u" 1);
 qed "natify_elem_is_self";
 Addsimps [natify_elem_is_self];
 
@@ -1024,8 +1006,6 @@
 by (case_tac "a ~: mset_of(I)" 1);
 by (auto_tac (claset(), simpset() addsimps 
              [mcount_def, mset_of_def, multiset_def, multiset_fun_iff]));
-by (rotate_simp_tac "I:?u" 1);
-by (rotate_simp_tac "J:?u" 1);
 by (auto_tac (claset() addDs [domain_type], simpset() addsimps [lemma]));
 qed "mdiff_union_single_conv";
 
@@ -1141,7 +1121,6 @@
 by (asm_full_simp_tac (simpset() addsimps [multirel1_iff, Mult_iff_multiset]) 1);
 by (Force_tac 1);
 (*Now we know J' ~=  0*)
-by (rotate_simp_tac "multiset(J')" 1);
 by (dtac sym 1 THEN rotate_tac ~1 1);
 by (Asm_full_simp_tac 1);
 by (thin_tac "$# x = msize(J')" 1);
@@ -1215,7 +1194,6 @@
 by (forw_inst_tac [("B", "mset_of(K)")] part_ord_subset 1);
 by (ALLGOALS(Asm_full_simp_tac));
 by (auto_tac (claset(), simpset() addsimps [multiset_def, mset_of_def]));
-by (rotate_simp_tac "K:?u" 1);
 qed "irrefl_on_multirel";
 
 Goalw [multirel_def, trans_on_def] "trans[Mult(A)](multirel(A, r))";
diff -r 2edf034c902a -r 55d32e76ef4e src/ZF/Integ/Bin.thy
--- a/src/ZF/Integ/Bin.thy	Mon Sep 30 16:47:03 2002 +0200
+++ b/src/ZF/Integ/Bin.thy	Mon Sep 30 16:48:15 2002 +0200
@@ -365,12 +365,9 @@
 apply (subgoal_tac "integ_of (w) : int")
 apply typecheck
 apply (drule int_cases)
-apply (auto elim!: boolE simp add: int_of_add [symmetric])
-apply (simp_all add: zcompare_rls zminus_zadd_distrib [symmetric]
+apply (safe elim!: boolE)
+apply (simp_all (asm_lr) add: zcompare_rls zminus_zadd_distrib [symmetric]
                      int_of_add [symmetric])
-apply (subgoal_tac "znegative ($- $# succ (n)) <-> znegative ($# succ (n))")
- apply (simp (no_asm_use))
-apply simp 
 done
 
 lemma iszero_integ_of_0:
diff -r 2edf034c902a -r 55d32e76ef4e src/ZF/Integ/Int.thy
--- a/src/ZF/Integ/Int.thy	Mon Sep 30 16:47:03 2002 +0200
+++ b/src/ZF/Integ/Int.thy	Mon Sep 30 16:48:15 2002 +0200
@@ -678,7 +678,6 @@
 
 lemma zless_not_refl [iff]: "~ (z$<z)"
 apply (auto simp add: zless_def znegative_def int_of_def zdiff_def)
-apply (rotate_tac 2, auto)
 done
 
 lemma neq_iff_zless: "[| x: int; y: int |] ==> (x ~= y) <-> (x $< y | y $< x)"
diff -r 2edf034c902a -r 55d32e76ef4e src/ZF/Integ/IntDiv.thy
--- a/src/ZF/Integ/IntDiv.thy	Mon Sep 30 16:47:03 2002 +0200
+++ b/src/ZF/Integ/IntDiv.thy	Mon Sep 30 16:48:15 2002 +0200
@@ -229,7 +229,6 @@
  apply (erule natE)
 apply (simp_all add: zadd_zmult_distrib zadd_zless_mono zle_def)
 apply (frule nat_0_le)
-apply (erule (1) notE impE)
 apply (subgoal_tac "i $+ (i $+ $# xa $* i) $< j $+ (j $+ $# xa $* j) ")
 apply (simp (no_asm_use))
 apply (rule zadd_zless_mono)
@@ -392,7 +391,6 @@
 apply (subgoal_tac "q = q'")
  prefer 2 apply (blast intro: unique_quotient)
 apply (simp add: quorem_def)
-apply auto
 done
 
 
diff -r 2edf034c902a -r 55d32e76ef4e src/ZF/Resid/Redex.thy
--- a/src/ZF/Resid/Redex.thy	Mon Sep 30 16:47:03 2002 +0200
+++ b/src/ZF/Resid/Redex.thy	Mon Sep 30 16:48:15 2002 +0200
@@ -178,11 +178,7 @@
 
 lemma union_preserve_regular [rule_format]:
      "u ~ v ==> regular(u)-->regular(v)-->regular(u un v)"
-apply (erule Scomp.induct, auto)
-(*select the given assumption for simplification*)
-apply (erule_tac P = "regular (Fun (?u) un ?v) " in rev_mp)
-apply simp
-done
+  by (erule Scomp.induct, auto)
 
 end
 
diff -r 2edf034c902a -r 55d32e76ef4e src/ZF/Resid/Reduction.thy
--- a/src/ZF/Resid/Reduction.thy	Mon Sep 30 16:47:03 2002 +0200
+++ b/src/ZF/Resid/Reduction.thy	Mon Sep 30 16:48:15 2002 +0200
@@ -236,8 +236,6 @@
      "u~v ==> regular(v) --> unmark(u) =1=> unmark(u|>v)"
 apply (erule Scomp.induct)
 apply (auto simp add: unmmark_subst_rec)
-apply (drule_tac psi = "Fun (?u) =1=> ?w" in asm_rl)
-apply auto
 done
 
 lemma completeness: "[|u \<in> lambda; u~v; regular(v)|] ==> u =1=> unmark(u|>v)"
diff -r 2edf034c902a -r 55d32e76ef4e src/ZF/Resid/Residuals.thy
--- a/src/ZF/Resid/Residuals.thy	Mon Sep 30 16:47:03 2002 +0200
+++ b/src/ZF/Resid/Residuals.thy	Mon Sep 30 16:48:15 2002 +0200
@@ -118,10 +118,7 @@
 
 lemma resfunc_type [simp]:
      "[|s~t; regular(t)|]==> regular(t) --> s |> t \<in> redexes"
-apply (erule Scomp.induct, auto)
-apply (drule_tac psi = "Fun (?u) |> ?v \<in> redexes" in asm_rl)
-apply auto
-done
+  by (erule Scomp.induct, auto)
 
 (* ------------------------------------------------------------------------- *)
 (*     Commutation theorem                                                   *)
@@ -138,7 +135,6 @@
          lift_rec(u,n) |> lift_rec(v,n) = lift_rec(u |> v,n))"
 apply (erule Scomp.induct, safe)
 apply (simp_all add: lift_rec_Var subst_Var lift_subst)
-apply (rotate_tac -2, simp)
 done
 
 lemma residuals_subst_rec:
@@ -169,7 +165,6 @@
 lemma residuals_preserve_reg [rule_format, simp]:
      "u~v ==> regular(u) --> regular(v) --> regular(u|>v)"
 apply (erule Scomp.induct, auto)
-apply (drule_tac psi = "regular (Fun (?u) |> ?v)" in asm_rl, force)+
 done
 
 (* ------------------------------------------------------------------------- *)
diff -r 2edf034c902a -r 55d32e76ef4e src/ZF/UNITY/UNITY.ML
--- a/src/ZF/UNITY/UNITY.ML	Mon Sep 30 16:47:03 2002 +0200
+++ b/src/ZF/UNITY/UNITY.ML	Mon Sep 30 16:48:15 2002 +0200
@@ -609,7 +609,7 @@
 "[| F : stable(C); F : A co (C Un A') |] ==> F : (C Un A) co (C Un A')";
 by (cut_inst_tac [("F", "F")] Acts_type 1);
 by Auto_tac;
-by (Force_tac 1);
+by (Blast.depth_tac (claset()) 10 1);
 qed "stable_constrains_Un";
 
 Goalw [stable_def, constrains_def, st_set_def]
diff -r 2edf034c902a -r 55d32e76ef4e src/ZF/UNITY/Union.ML
--- a/src/ZF/UNITY/Union.ML	Mon Sep 30 16:47:03 2002 +0200
+++ b/src/ZF/UNITY/Union.ML	Mon Sep 30 16:48:15 2002 +0200
@@ -592,8 +592,7 @@
 (*For safety_prop to hold, the property must be satisfiable!*)
 Goal "safety_prop(A co B) <-> (A <= B & st_set(A))";
 by (simp_tac (simpset() addsimps [safety_prop_def, constrains_def, st_set_def]) 1);
-by (auto_tac (claset() addDs [Acts_type RS subsetD], simpset()));
-by (REPEAT(Blast_tac 1));
+by (Blast_tac 1);
 qed "safety_prop_constrains";
 AddIffs [safety_prop_constrains];
 
diff -r 2edf034c902a -r 55d32e76ef4e src/ZF/UNITY/WFair.ML
--- a/src/ZF/UNITY/WFair.ML	Mon Sep 30 16:47:03 2002 +0200
+++ b/src/ZF/UNITY/WFair.ML	Mon Sep 30 16:48:15 2002 +0200
@@ -21,8 +21,8 @@
 
 Goalw [stable_def, constrains_def, transient_def]
     "[| F : stable(A); F : transient(A) |] ==> A = 0";
-by Auto_tac;
-by (Blast_tac 1);
+by (Asm_full_simp_tac 1);
+by (Blast.depth_tac (claset()) 10 1);
 qed "stable_transient_empty";
 
 Goalw [transient_def, st_set_def] 
diff -r 2edf034c902a -r 55d32e76ef4e src/ZF/ex/Limit.thy
--- a/src/ZF/ex/Limit.thy	Mon Sep 30 16:47:03 2002 +0200
+++ b/src/ZF/ex/Limit.thy	Mon Sep 30 16:48:15 2002 +0200
@@ -1620,7 +1620,7 @@
         m \<in> nat |]==>R"
 apply (rule le_exists, assumption)
 prefer 2 apply (simp add: lt_nat_in_nat)
-apply (rule le_trans [THEN le_exists], assumption+, auto)
+apply (rule le_trans [THEN le_exists], assumption+, force+)
 done
 
 lemma eps_split_left_le: