# HG changeset patch
# User nipkow
# Date 1394690827 -3600
# Node ID 29e308b56d23a4e56517b97936cd4bce6d50be10
# Parent  31e427387ab5c551518367291ac2df655ecea43c
enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions

diff -r 31e427387ab5 -r 29e308b56d23 NEWS
--- a/NEWS	Wed Mar 12 22:57:50 2014 +0100
+++ b/NEWS	Thu Mar 13 07:07:07 2014 +0100
@@ -98,6 +98,12 @@
 
 *** HOL ***
 
+* Simplifier: Enhanced solver of preconditions of rewrite rules
+  can now deal with conjunctions.
+  For help with converting proofs, the old behaviour of the simplifier
+  can be restored like this:  declare/using [[simp_legacy_precond]]
+  This configuration option will disappear again in the future.
+
 * HOL-Word:
   * Abandoned fact collection "word_arith_alts", which is a
   duplicate of "word_arith_wis".
diff -r 31e427387ab5 -r 29e308b56d23 src/HOL/Auth/Guard/Guard_Yahalom.thy
--- a/src/HOL/Auth/Guard/Guard_Yahalom.thy	Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/Auth/Guard/Guard_Yahalom.thy	Thu Mar 13 07:07:07 2014 +0100
@@ -218,12 +218,12 @@
 apply (rule Guard_extand, simp, blast)
 apply (case_tac "NAa=NB", clarify)
 apply (frule Says_imp_spies)
-apply (frule in_Guard_kparts_Crypt, simp+, blast, simp+)
+apply (frule in_Guard_kparts_Crypt, simp+)
 apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Ba in ya3_shrK, simp)
 apply (drule ya2'_imp_ya1'_parts, simp, blast, blast)
 apply (case_tac "NBa=NB", clarify)
 apply (frule Says_imp_spies)
-apply (frule in_Guard_kparts_Crypt, simp+, blast, simp+)
+apply (frule in_Guard_kparts_Crypt, simp+)
 apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Ba in ya3_shrK, simp)
 apply (drule NB_is_uniq_in_ya2', simp+, blast, simp+)
 apply (simp add: No_Nonce, blast)
@@ -239,7 +239,7 @@
 apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Aa in ya3_shrK, simp)
 apply (frule ya3'_imp_ya2', simp+, blast, clarify)
 apply (frule_tac A=B' in Says_imp_spies)
-apply (rotate_tac -1, frule in_Guard_kparts_Crypt, simp+, blast, simp+)
+apply (rotate_tac -1, frule in_Guard_kparts_Crypt, simp+)
 apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Ba in ya3_shrK, simp)
 apply (drule NB_is_uniq_in_ya2', simp+, blast, clarify)
 apply (drule ya3'_imp_ya3, simp+)
diff -r 31e427387ab5 -r 29e308b56d23 src/HOL/Auth/Public.thy
--- a/src/HOL/Auth/Public.thy	Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/Auth/Public.thy	Thu Mar 13 07:07:07 2014 +0100
@@ -414,7 +414,7 @@
 (*Tactic for possibility theorems*)
 fun possibility_tac ctxt =
     REPEAT (*omit used_Says so that Nonces start from different traces!*)
-    (ALLGOALS (simp_tac (ctxt delsimps [@{thm used_Says}]))
+    (ALLGOALS (simp_tac (ctxt setSolver safe_solver delsimps [@{thm used_Says}]))
      THEN
      REPEAT_FIRST (eq_assume_tac ORELSE' 
                    resolve_tac [refl, conjI, @{thm Nonce_supply}]))
diff -r 31e427387ab5 -r 29e308b56d23 src/HOL/Auth/ZhouGollmann.thy
--- a/src/HOL/Auth/ZhouGollmann.thy	Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/Auth/ZhouGollmann.thy	Thu Mar 13 07:07:07 2014 +0100
@@ -101,7 +101,7 @@
                      THEN zg.ZG2, THEN zg.Reception [of _ B A],
                      THEN zg.ZG3, THEN zg.Reception [of _ A TTP], 
                      THEN zg.ZG4])
-apply (possibility, auto)
+apply (basic_possibility, auto)
 done
 
 subsection {*Basic Lemmas*}
diff -r 31e427387ab5 -r 29e308b56d23 src/HOL/Bali/Example.thy
--- a/src/HOL/Bali/Example.thy	Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/Bali/Example.thy	Thu Mar 13 07:07:07 2014 +0100
@@ -1280,8 +1280,6 @@
 apply   (rule conjI)
 apply    (rule eval_Is (* Init Object *))
 apply    (simp)
-apply    (rule conjI, rule HOL.refl)+
-apply    (rule HOL.refl)
 apply   (simp)
 apply   (rule conjI, rule_tac [2] HOL.refl)
 apply   (rule eval_Is (* Expr *))
diff -r 31e427387ab5 -r 29e308b56d23 src/HOL/Bali/Trans.thy
--- a/src/HOL/Bali/Trans.thy	Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/Bali/Trans.thy	Thu Mar 13 07:07:07 2014 +0100
@@ -23,12 +23,7 @@
     | (FVar) accC statDeclC stat a fn where "v={accC,statDeclC,stat}(Lit a)..fn"
     | (AVar) a i where "v=(Lit a).[Lit i]"
   using ground LVar FVar AVar
-  apply (cases v)
-  apply (simp add: groundVar_def)
-  apply (simp add: groundVar_def,blast)
-  apply (simp add: groundVar_def,blast)
-  apply (simp add: groundVar_def)
-  done
+  by (cases v) (auto simp add: groundVar_def)
 
 definition
   groundExprs :: "expr list \<Rightarrow> bool"
diff -r 31e427387ab5 -r 29e308b56d23 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy	Thu Mar 13 07:07:07 2014 +0100
@@ -2613,7 +2613,7 @@
     and inequality: "u \<le> lx \<and> ux \<le> l'"
     by (cases "approx prec x vs", auto,
       cases "approx prec a vs", auto,
-      cases "approx prec b vs", auto, blast)
+      cases "approx prec b vs", auto)
   from inequality approx[OF AtLeastAtMost.prems(2) l_eq] approx[OF AtLeastAtMost.prems(2) u_eq] approx[OF AtLeastAtMost.prems(2) x_eq]
   show ?case by auto
 qed
@@ -2902,7 +2902,7 @@
                (Mult (Inverse (Num (Float (int k) 0)))
                      (Mult (Add (Var (Suc (Suc 0))) (Minus (Num c)))
                            (Var (Suc 0))))) [Some (l1, u1), Some (l2, u2), vs!x]"
-      by (auto elim!: lift_bin) blast
+      by (auto elim!: lift_bin)
 
     from bnd_c `x < length xs`
     have bnd: "bounded_by (xs[x:=c]) (vs[x:= Some (c,c)])"
diff -r 31e427387ab5 -r 29e308b56d23 src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Thu Mar 13 07:07:07 2014 +0100
@@ -473,7 +473,6 @@
       then have ?case using 4
         apply (cases "p +\<^sub>p p' = 0\<^sub>p")
         apply (auto simp add: Let_def)
-        apply blast
         done
     }
     ultimately have ?case by blast
diff -r 31e427387ab5 -r 29e308b56d23 src/HOL/HOLCF/IOA/meta_theory/Seq.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/Seq.thy	Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Seq.thy	Thu Mar 13 07:07:07 2014 +0100
@@ -5,7 +5,7 @@
 header {* Partial, Finite and Infinite Sequences (lazy lists), modeled as domain *}
 
 theory Seq
-imports HOLCF
+imports "../../HOLCF"
 begin
 
 default_sort pcpo
diff -r 31e427387ab5 -r 29e308b56d23 src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy	Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy	Thu Mar 13 07:07:07 2014 +0100
@@ -99,7 +99,6 @@
 apply (erule conjE)
 apply (simp add: Let_def)
 apply (rule_tac x = "ex" in someI)
-apply (erule conjE)
 apply assumption
 done
 
diff -r 31e427387ab5 -r 29e308b56d23 src/HOL/HOLCF/IOA/meta_theory/TLS.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/TLS.thy	Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/TLS.thy	Thu Mar 13 07:07:07 2014 +0100
@@ -196,10 +196,7 @@
 apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
 apply (tactic {* pair_tac @{context} "a" 1 *})
 apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
-apply blast
-apply fastforce
 apply (tactic {* pair_tac @{context} "a" 1 *})
- apply fastforce
 done
 
 end
diff -r 31e427387ab5 -r 29e308b56d23 src/HOL/HOLCF/Universal.thy
--- a/src/HOL/HOLCF/Universal.thy	Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/HOLCF/Universal.thy	Thu Mar 13 07:07:07 2014 +0100
@@ -111,12 +111,11 @@
   "ubasis_until P 0 = 0"
 | "finite S \<Longrightarrow> ubasis_until P (node i a S) =
     (if P (node i a S) then node i a S else ubasis_until P a)"
-    apply clarify
-    apply (rule_tac x=b in node_cases)
-     apply simp
+   apply clarify
+   apply (rule_tac x=b in node_cases)
     apply simp
-    apply fast
    apply simp
+   apply fast
   apply simp
  apply simp
 done
diff -r 31e427387ab5 -r 29e308b56d23 src/HOL/Hoare_Parallel/RG_Tran.thy
--- a/src/HOL/Hoare_Parallel/RG_Tran.thy	Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/Hoare_Parallel/RG_Tran.thy	Thu Mar 13 07:07:07 2014 +0100
@@ -196,7 +196,6 @@
 apply(erule_tac x="Some P2" in allE)
 apply(erule allE,erule impE, assumption)
 apply(drule div_seq,simp)
-apply force
 apply clarify
 apply(erule disjE)
  apply clarify
diff -r 31e427387ab5 -r 29e308b56d23 src/HOL/Imperative_HOL/ex/Linked_Lists.thy
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Thu Mar 13 07:07:07 2014 +0100
@@ -918,7 +918,7 @@
   from 3(7)[OF no_inter2] obtain rs where rs_def: "refs_of' h1 r1 rs" by (rule list_of'_refs_of')
   from refs_of'_merge[OF refs_of'_pn qrs_def 3(6) no_inter this] p_in have p_rs: "p \<notin> set rs" by auto
   with 3(7)[OF no_inter2] 3(1-5) 3(8) p_rs rs_def p_stays
-  show ?case by auto
+  show ?case by (auto simp: list_of'_set_ref)
 next
   case (4 x xs' y ys' p q pn qn h1 r1 h')
   from 4(1) obtain prs where prs_def: "refs_of' h p prs" by (rule list_of'_refs_of')
@@ -935,7 +935,7 @@
   from 4(7)[OF no_inter2] obtain rs where rs_def: "refs_of' h1 r1 rs" by (rule list_of'_refs_of')
   from refs_of'_merge[OF prs_def refs_of'_qn 4(6) no_inter this] q_in have q_rs: "q \<notin> set rs" by auto
   with 4(7)[OF no_inter2] 4(1-5) 4(8) q_rs rs_def q_stays
-  show ?case by auto
+  show ?case by (auto simp: list_of'_set_ref)
 qed
 
 section {* Code generation *}
diff -r 31e427387ab5 -r 29e308b56d23 src/HOL/Isar_Examples/Hoare_Ex.thy
--- a/src/HOL/Isar_Examples/Hoare_Ex.thy	Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/Isar_Examples/Hoare_Ex.thy	Thu Mar 13 07:07:07 2014 +0100
@@ -59,7 +59,7 @@
   by hoare
 
 lemma "\<turnstile> \<lbrace>True\<rbrace> \<acute>M := a; \<acute>N := b \<lbrace>\<acute>M = a \<and> \<acute>N = b\<rbrace>"
-  by hoare simp
+  by hoare
 
 lemma
   "\<turnstile> \<lbrace>\<acute>M = a \<and> \<acute>N = b\<rbrace>
diff -r 31e427387ab5 -r 29e308b56d23 src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Thu Mar 13 07:07:07 2014 +0100
@@ -204,7 +204,6 @@
     apply auto
     apply (case_tac xc)
     apply auto
-    apply fastforce
     done
 qed
 
diff -r 31e427387ab5 -r 29e308b56d23 src/HOL/MicroJava/BV/BVNoTypeError.thy
--- a/src/HOL/MicroJava/BV/BVNoTypeError.thy	Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/MicroJava/BV/BVNoTypeError.thy	Thu Mar 13 07:07:07 2014 +0100
@@ -236,7 +236,7 @@
     then obtain stk loc C sig pc frs' where
       xcp [simp]: "xcp = None" and
       frs [simp]: "frs = (stk,loc,C,sig,pc)#frs'" 
-      by (clarsimp simp add: neq_Nil_conv) fast
+      by (clarsimp simp add: neq_Nil_conv)
 
     from conforms obtain  ST LT rT maxs maxl ins et where
       hconf:  "G \<turnstile>h hp \<surd>" and
@@ -245,7 +245,7 @@
       phi:    "Phi C sig ! pc = Some (ST,LT)" and
       frame:  "correct_frame G hp (ST,LT) maxl ins (stk,loc,C,sig,pc)" and
       frames: "correct_frames G hp Phi rT sig frs'"
-      by (auto simp add: correct_state_def) (rule that)
+      by (auto simp add: correct_state_def)
 
     from frame obtain
       stk: "approx_stk G hp stk ST" and
@@ -354,7 +354,7 @@
         obtain D fs where
           hp: "hp (the_Addr x) = Some (D,fs)" and
           D:  "G \<turnstile> D \<preceq>C C"
-          by - (drule non_npD, assumption, clarsimp, blast)
+          by - (drule non_npD, assumption, clarsimp)
         hence "hp (the_Addr x) \<noteq> None" (is ?P1) by simp
         moreover
         from wf mth hp D
diff -r 31e427387ab5 -r 29e308b56d23 src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Thu Mar 13 07:07:07 2014 +0100
@@ -889,7 +889,7 @@
     loc:    "hp ref = Some obj" and
     obj_ty: "obj_ty obj = Class D" and
     D:      "G \<turnstile> Class D \<preceq> X"
-    by (auto simp add: conf_def) blast
+    by (auto simp add: conf_def)
   
   with X_Ref obtain X' where X': "X = Class X'"
     by (blast dest: widen_Class)
@@ -1052,7 +1052,7 @@
       meth'': "method (G, D) sig = Some (D'', rT'', body)" and
       ST0':   "ST' = rev apTs @ Class D # ST0'" and
       len':   "length apTs = length pt" 
-      by clarsimp blast    
+      by clarsimp
 
     from f frame'
     obtain
@@ -1074,7 +1074,7 @@
       methD':  "method (G, D') sig = Some (mD, rT0, body')" and
       lessD':  "G \<turnstile> X \<preceq> Class D'" and
       suc_pc': "Suc pc' < length ins'"
-      by (clarsimp simp add: wt_instr_def eff_def norm_eff_def) blast
+      by (clarsimp simp add: wt_instr_def eff_def norm_eff_def)
 
     from len len' ST0 ST0'
     have "X = Class D" by simp
diff -r 31e427387ab5 -r 29e308b56d23 src/HOL/MicroJava/BV/EffectMono.thy
--- a/src/HOL/MicroJava/BV/EffectMono.thy	Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/MicroJava/BV/EffectMono.thy	Thu Mar 13 07:07:07 2014 +0100
@@ -161,7 +161,7 @@
         where s2:  "s2 = (vT' # oT' # ST', LT')" and
               oT': "G\<turnstile> oT' \<preceq> oT" and
               vT': "G\<turnstile> vT' \<preceq> vT"
-        by - (cases s2, simp add: sup_state_Cons2, elim exE conjE, simp, rule that)
+        by - (cases s2, simp add: sup_state_Cons2, elim exE conjE, simp)
       moreover
       from vT' vT
       have "G \<turnstile> vT' \<preceq> b" by (rule widen_trans)
diff -r 31e427387ab5 -r 29e308b56d23 src/HOL/MicroJava/BV/JVMType.thy
--- a/src/HOL/MicroJava/BV/JVMType.thy	Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/MicroJava/BV/JVMType.thy	Thu Mar 13 07:07:07 2014 +0100
@@ -258,7 +258,7 @@
     assume l: "length (l#ls) = length b"
     
     then obtain b' bs where b: "b = b'#bs"
-      by (cases b) (simp, simp add: neq_Nil_conv, rule that)
+      by (cases b) (simp, simp add: neq_Nil_conv)
 
     with f
     have "\<forall>n. n < length ls \<longrightarrow> (G \<turnstile> (ls!n) <=o (bs!n))"
diff -r 31e427387ab5 -r 29e308b56d23 src/HOL/MicroJava/Comp/CorrComp.thy
--- a/src/HOL/MicroJava/Comp/CorrComp.thy	Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/MicroJava/Comp/CorrComp.thy	Thu Mar 13 07:07:07 2014 +0100
@@ -523,7 +523,6 @@
 apply (rule_tac ?instrs0.0 = "[load_default_val b]" in progression_transitive, simp)
 apply (rule progression_one_step)
 apply (simp (no_asm_simp) add: load_default_val_def)
-apply (rule conjI, simp)+ apply (rule HOL.refl)
 
 apply (rule progression_one_step)
 apply (simp (no_asm_simp))
@@ -816,7 +815,7 @@
 apply (rule_tac ?instrs0.0 = "[Dup]" in progression_transitive, simp)
 apply (rule progression_one_step)
 apply (simp add: gh_def)
-apply (rule conjI, simp)+ apply simp
+apply simp
 apply (rule progression_one_step)
 apply (simp add: gh_def)
 (* the following falls out of the general scheme *)
@@ -865,8 +864,6 @@
    (* Dup_x1 *)
    apply (rule progression_one_step)
    apply (simp add: gh_def)
-   apply (rule conjI, simp)+ apply simp
-
 
    (* Putfield \<longrightarrow> still looks nasty*)
    apply (rule progression_one_step)
@@ -948,7 +945,6 @@
 apply simp
 apply (rule_tac ?instrs0.0 = "[LitPush (Bool False)]" in progression_transitive, simp (no_asm_simp))
 apply (rule progression_one_step,  simp)
-apply (rule conjI, rule HOL.refl)+ apply (rule HOL.refl)
 
 apply (rule_tac ?instrs0.0 = "compExpr (gmb G CL S) e" in progression_transitive, rule HOL.refl)
 apply fast
@@ -958,18 +954,17 @@
 apply simp
 apply (rule_tac ?instrs0.0 = "[Ifcmpeq (2 + int (length (compStmt (gmb G CL S) c1)))]" in progression_transitive, simp)
 apply (rule progression_one_step) apply simp
-apply (rule conjI, rule HOL.refl)+ apply (rule HOL.refl)
 apply (rule_tac ?instrs0.0 = "(compStmt (gmb G CL S) c1)" in progression_transitive, simp)
 apply fast
 apply (rule_tac ?instrs1.0 = "[]" in jump_fwd_progression)
-apply (simp, rule conjI, (rule HOL.refl)+)
+apply (simp)
 apply simp apply (rule conjI, simp) apply (simp add: nat_add_distrib)
 apply (rule progression_refl)
 
  (* case b= False *)
 apply simp
 apply (rule_tac ?instrs1.0 = "compStmt (gmb G CL S) c2" in jump_fwd_progression)
-apply (simp, rule conjI, (rule HOL.refl)+)
+apply (simp)
 apply (simp, rule conjI, rule HOL.refl, simp add: nat_add_distrib)
 apply fast
 
@@ -992,12 +987,11 @@
 apply (rule_tac ?instrs0.0 = "[LitPush (Bool False)]" in progression_transitive, simp (no_asm_simp))
 apply (rule progression_one_step)
    apply simp 
-   apply (rule conjI, rule HOL.refl)+ apply (rule HOL.refl)
 
 apply (rule_tac ?instrs0.0 = "compExpr (gmb G CL S) e" in progression_transitive, rule HOL.refl)
 apply fast
 apply (rule_tac ?instrs1.0 = "[]" in jump_fwd_progression)
-apply (simp, rule conjI, rule HOL.refl, rule HOL.refl)
+apply (simp)
 apply (simp, rule conjI, rule HOL.refl, simp add: nat_add_distrib)
 apply (rule progression_refl)
 
@@ -1022,12 +1016,10 @@
 apply simp
 apply (rule jump_bwd_progression) 
 apply simp
-apply (rule conjI, (rule HOL.refl)+)
 
 apply (rule_tac ?instrs0.0 = "[LitPush (Bool False)]" in progression_transitive, simp (no_asm_simp))
 apply (rule progression_one_step)
    apply simp 
-   apply (rule conjI, simp)+ apply simp
 
 apply (rule_tac ?instrs0.0 = "compExpr (gmb G CL S) e" in progression_transitive, rule HOL.refl)
 apply fast
@@ -1038,7 +1030,6 @@
 
 apply (rule_tac ?instrs0.0 = "[Ifcmpeq (2 + int (length (compStmt (gmb G CL S) c)))]" in progression_transitive, simp)
 apply (rule progression_one_step) apply simp
-apply (rule conjI, rule HOL.refl)+ apply (rule HOL.refl)
 apply fast
 
  (* case b= False \<longrightarrow> contradiction*)
@@ -1126,7 +1117,6 @@
 apply (simp (no_asm_use) only: exec_instr.simps)
 apply (erule thin_rl, erule thin_rl, erule thin_rl)
 apply (simp add: compMethod_def raise_system_xcpt_def)
-apply (rule conjI, simp)+ apply (rule HOL.refl)
 
      (* get instructions of invoked method *)
 apply (simp (no_asm_simp) add: gis_def gmb_def compMethod_def)
@@ -1177,7 +1167,6 @@
 apply (frule non_npD) apply assumption
 apply (erule exE)+ apply simp
 apply (rule conf_obj_AddrI) apply simp 
-apply (rule conjI, (rule HOL.refl)+)
 apply (rule widen_Class_Class [THEN iffD1], rule widen.refl)
 
 
diff -r 31e427387ab5 -r 29e308b56d23 src/HOL/MicroJava/Comp/CorrCompTp.thy
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Thu Mar 13 07:07:07 2014 +0100
@@ -1268,7 +1268,6 @@
   apply (frule max_spec2mheads, (erule exE)+, (erule conjE)+)
   apply (rule exI)+
   apply (simp add: wf_prog_ws_prog [THEN comp_method])
-  apply auto
   done
 
 
@@ -2517,16 +2516,13 @@
                               (start_ST, start_LT C pTs (length lvars))))
                 = (start_ST, inited_LT C pTs lvars)") 
    prefer 2 apply (rule compTpInitLvars_LT_ST) apply (rule HOL.refl) apply assumption
-apply (simp only:)
 apply (subgoal_tac "(snd (compTpStmt (pns, lvars, blk, res) G blk
                        (start_ST, inited_LT C pTs lvars))) 
                 = (start_ST, inited_LT C pTs lvars)") 
    prefer 2 apply (erule conjE)+
    apply (rule compTpStmt_LT_ST) apply (rule HOL.refl) apply assumption+
    apply (simp only:)+ apply (simp (no_asm_simp) add: is_inited_LT_def)
-apply (simp only:)
-apply (rule compTpExpr_LT_ST) apply (rule HOL.refl) apply assumption+
-   apply (simp only:)+ apply (simp (no_asm_simp) add: is_inited_LT_def)
+   apply (simp (no_asm_simp) add: is_inited_LT_def)
 
 
    (* Return *)
diff -r 31e427387ab5 -r 29e308b56d23 src/HOL/MicroJava/J/Eval.thy
--- a/src/HOL/MicroJava/J/Eval.thy	Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/MicroJava/J/Eval.thy	Thu Mar 13 07:07:07 2014 +0100
@@ -226,7 +226,7 @@
   next
     case (Call a b c d e f g h i j k l m n o p q r s t u v s4)
     with Call_code show ?thesis
-      by(cases "s4")(simp, (erule meta_allE meta_impE|rule conjI refl| assumption)+)
+      by(cases "s4") auto
   qed(erule (3) that[OF refl]|assumption)+
 next
   case evals
diff -r 31e427387ab5 -r 29e308b56d23 src/HOL/MicroJava/J/WellForm.thy
--- a/src/HOL/MicroJava/J/WellForm.thy	Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/MicroJava/J/WellForm.thy	Thu Mar 13 07:07:07 2014 +0100
@@ -565,7 +565,7 @@
 apply clarify
 apply (frule wf_prog_ws_prog)
 apply (frule fields_Object, assumption+)
-apply (simp only: is_class_Object) apply simp
+apply (simp only: is_class_Object)
 
 apply clarify
 apply (frule fields_rec)
diff -r 31e427387ab5 -r 29e308b56d23 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Mar 13 07:07:07 2014 +0100
@@ -2958,10 +2958,10 @@
   fix f
   assume *: "Ball f open" "s \<union> t \<subseteq> \<Union>f"
   from * `compact s` obtain s' where "s' \<subseteq> f \<and> finite s' \<and> s \<subseteq> \<Union>s'"
-    unfolding compact_eq_heine_borel by (auto elim!: allE[of _ f]) metis
+    unfolding compact_eq_heine_borel by (auto elim!: allE[of _ f])
   moreover
   from * `compact t` obtain t' where "t' \<subseteq> f \<and> finite t' \<and> t \<subseteq> \<Union>t'"
-    unfolding compact_eq_heine_borel by (auto elim!: allE[of _ f]) metis
+    unfolding compact_eq_heine_borel by (auto elim!: allE[of _ f])
   ultimately show "\<exists>f'\<subseteq>f. finite f' \<and> s \<union> t \<subseteq> \<Union>f'"
     by (auto intro!: exI[of _ "s' \<union> t'"])
 qed
diff -r 31e427387ab5 -r 29e308b56d23 src/HOL/Nominal/Examples/Class1.thy
--- a/src/HOL/Nominal/Examples/Class1.thy	Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/Nominal/Examples/Class1.thy	Thu Mar 13 07:07:07 2014 +0100
@@ -1702,32 +1702,13 @@
 next
   case (NotR y M d)
   then show ?case 
-    apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
-    apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(N,M{d:=(x).N},([(c,d)]\<bullet>M){c:=(x).N})")
-    apply(erule exE, simp add: fresh_prod)
-    apply(erule conjE)+
-    apply(simp add: fresh_fun_simp_NotR)
-    apply(simp add: trm.inject alpha)
-    apply(rule exists_fresh'(2)[OF fs_coname1])
-    done
+    by(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
 next
   case (AndR c1 M c2 M' c3)
   then show ?case
-    apply(simp)
-    apply(auto)
-    apply(simp add: fresh_prod calc_atm fresh_atm abs_fresh)
-    apply(simp add: fresh_prod calc_atm fresh_atm abs_fresh fresh_left)
-    apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(N,M{c3:=(x).N},
-                  M'{c3:=(x).N},c1,c2,c3,([(c,c3)]\<bullet>M){c:=(x).N},([(c,c3)]\<bullet>M'){c:=(x).N})")
-    apply(erule exE, simp add: fresh_prod)
-    apply(erule conjE)+
-    apply(simp add: fresh_fun_simp_AndR)
-    apply (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh subst_fresh)
-    apply(rule exists_fresh'(2)[OF fs_coname1])
-    apply(simp add: fresh_prod calc_atm fresh_atm abs_fresh fresh_left)
-    apply(simp add: fresh_prod calc_atm fresh_atm abs_fresh fresh_left)
-    apply(auto simp add: trm.inject alpha)
-    done
+    apply(auto simp add: fresh_prod calc_atm fresh_atm abs_fresh fresh_left)
+    apply (metis (erased, hide_lams))
+    by metis
 next
   case AndL1
   then show ?case by (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
@@ -1737,25 +1718,11 @@
 next
   case (OrR1 d M e)
   then show ?case 
-    apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
-    apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(N,M{e:=(x).N},([(c,e)]\<bullet>M){c:=(x).N},d,e)")
-    apply(erule exE, simp add: fresh_prod)
-    apply(erule conjE)+
-    apply(simp add: fresh_fun_simp_OrR1)
-    apply(simp add: trm.inject alpha)
-    apply(rule exists_fresh'(2)[OF fs_coname1])
-    done
+    by(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
 next
   case (OrR2 d M e)
   then show ?case 
-    apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
-    apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(N,M{e:=(x).N},([(c,e)]\<bullet>M){c:=(x).N},d,e)")
-    apply(erule exE, simp add: fresh_prod)
-    apply(erule conjE)+
-    apply(simp add: fresh_fun_simp_OrR2)
-    apply(simp add: trm.inject alpha)
-    apply(rule exists_fresh'(2)[OF fs_coname1])
-    done
+    by(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
 next
   case (OrL x1 M x2 M' x3)
   then show ?case
@@ -1764,24 +1731,16 @@
   case ImpL
   then show ?case
     by (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
+       metis
 next
   case (ImpR y d M e)
   then show ?case
-    apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
-    apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(N,M{e:=(x).N},([(c,e)]\<bullet>M){c:=(x).N},d,e)")
-    apply(erule exE, simp add: fresh_prod)
-    apply(erule conjE)+
-    apply(simp add: fresh_fun_simp_ImpR)
-    apply(simp add: trm.inject alpha)
-    apply(rule exists_fresh'(2)[OF fs_coname1])
-    done
+    by(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
 next
   case (Cut d M y M')
   then show ?case
-    apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
-    apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])
-    apply(simp add: calc_atm)
-    done
+    by(simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
+      (metis crename.simps(1) crename_id crename_rename)
 qed
 
 lemma substc_rename2:
@@ -1885,14 +1844,7 @@
 next
   case (NotL d M z)
   then show ?case 
-    apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
-    apply(subgoal_tac "\<exists>a'::name. a'\<sharp>(N,M{x:=<a>.N},([(y,x)]\<bullet>M){y:=<a>.N})")
-    apply(erule exE, simp add: fresh_prod)
-    apply(erule conjE)+
-    apply(simp add: fresh_fun_simp_NotL)
-    apply(simp add: trm.inject alpha)
-    apply(rule exists_fresh'(1)[OF fs_name1])
-    done
+    by(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
 next
   case (AndR c1 M c2 M' c3)
   then show ?case
@@ -1906,37 +1858,16 @@
 next
   case (AndL1 u M v)
   then show ?case 
-    apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
-    apply(subgoal_tac "\<exists>a'::name. a'\<sharp>(N,M{x:=<a>.N},([(y,x)]\<bullet>M){y:=<a>.N},u,v)")
-    apply(erule exE, simp add: fresh_prod)
-    apply(erule conjE)+
-    apply(simp add: fresh_fun_simp_AndL1)
-    apply(simp add: trm.inject alpha)
-    apply(rule exists_fresh'(1)[OF fs_name1])
-    done
+    by(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
 next
   case (AndL2 u M v)
   then show ?case 
-    apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
-    apply(subgoal_tac "\<exists>a'::name. a'\<sharp>(N,M{x:=<a>.N},([(y,x)]\<bullet>M){y:=<a>.N},u,v)")
-    apply(erule exE, simp add: fresh_prod)
-    apply(erule conjE)+
-    apply(simp add: fresh_fun_simp_AndL2)
-    apply(simp add: trm.inject alpha)
-    apply(rule exists_fresh'(1)[OF fs_name1])
-    done
+    by(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
 next
   case (OrL x1 M x2 M' x3)
   then show ?case
-    apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
-    apply(subgoal_tac 
-    "\<exists>a'::name. a'\<sharp>(N,M{x:=<a>.N},M'{x:=<a>.N},([(y,x)]\<bullet>M){y:=<a>.N},([(y,x)]\<bullet>M'){y:=<a>.N},x1,x2)")
-    apply(erule exE, simp add: fresh_prod)
-    apply(erule conjE)+
-    apply(simp add: fresh_fun_simp_OrL)
-    apply(simp add: trm.inject alpha)
-    apply(rule exists_fresh'(1)[OF fs_name1])
-    done
+    by(simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
+      (metis (poly_guards_query))
 next 
   case ImpR
   then show ?case
@@ -1944,21 +1875,15 @@
 next
   case (ImpL d M v M' u)
   then show ?case
-    apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
-    apply(subgoal_tac 
-    "\<exists>a'::name. a'\<sharp>(N,M{u:=<a>.N},M'{u:=<a>.N},([(y,u)]\<bullet>M){y:=<a>.N},([(y,u)]\<bullet>M'){y:=<a>.N},d,v)")
-    apply(erule exE, simp add: fresh_prod)
-    apply(erule conjE)+
-    apply(simp add: fresh_fun_simp_ImpL)
-    apply(simp add: trm.inject alpha)
-    apply(rule exists_fresh'(1)[OF fs_name1])
-    done
+    by(simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
+       (metis (poly_guards_query))
 next
   case (Cut d M y M')
   then show ?case
     apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
     apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst])
     apply(simp add: calc_atm)
+    apply metis
     done
 qed
 
diff -r 31e427387ab5 -r 29e308b56d23 src/HOL/Nominal/Examples/Class2.thy
--- a/src/HOL/Nominal/Examples/Class2.thy	Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/Nominal/Examples/Class2.thy	Thu Mar 13 07:07:07 2014 +0100
@@ -2869,15 +2869,9 @@
 apply(rotate_tac 10)
 apply(drule_tac x="a" in meta_spec)
 apply(auto simp add: ty.inject)
-apply(blast)
-apply(blast)
-apply(blast)
 apply(rotate_tac 10)
 apply(drule_tac x="a" in meta_spec)
 apply(auto simp add: ty.inject)
-apply(blast)
-apply(blast)
-apply(blast)
 done
 
 termination
diff -r 31e427387ab5 -r 29e308b56d23 src/HOL/Old_Number_Theory/Pocklington.thy
--- a/src/HOL/Old_Number_Theory/Pocklington.thy	Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/Old_Number_Theory/Pocklington.thy	Thu Mar 13 07:07:07 2014 +0100
@@ -615,7 +615,7 @@
             from x(3)[rule_format, of z] z(2,3) have "z=x"
               unfolding modeq_def mod_less[OF y(2)] by simp}
           with xm x(1,2) have "\<exists>!x. x \<in> ?S \<and> (?h \<circ> op * a) x = y"
-            unfolding modeq_def mod_less[OF y(2)] by auto }
+            unfolding modeq_def mod_less[OF y(2)] by safe auto }
         thus "\<forall>y\<in>{m. coprime m n \<and> m < n}.
        \<exists>!x. x \<in> {m. coprime m n \<and> m < n} \<and> ((\<lambda>m. m mod n) \<circ> op * a) x = y" by blast
       next
diff -r 31e427387ab5 -r 29e308b56d23 src/HOL/Proofs/Lambda/LambdaType.thy
--- a/src/HOL/Proofs/Lambda/LambdaType.thy	Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/Proofs/Lambda/LambdaType.thy	Thu Mar 13 07:07:07 2014 +0100
@@ -130,10 +130,6 @@
   apply (case_tac ys)
   apply simp
   apply simp
-  apply atomize
-  apply (erule allE)+
-  apply (erule mp, rule conjI)
-  apply (rule refl)+
   done
 
 lemma types_snocE: "e \<tturnstile> ts @ [t] : Ts \<Longrightarrow>
@@ -142,7 +138,6 @@
   apply simp
   apply (case_tac "ts @ [t]")
   apply (simp add: types_snoc_eq)+
-  apply iprover
   done
 
 
diff -r 31e427387ab5 -r 29e308b56d23 src/HOL/Proofs/Lambda/WeakNorm.thy
--- a/src/HOL/Proofs/Lambda/WeakNorm.thy	Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/Proofs/Lambda/WeakNorm.thy	Thu Mar 13 07:07:07 2014 +0100
@@ -93,7 +93,7 @@
         next
           case (Cons a as)
           with argsT obtain T'' Ts where Us: "Us = T'' # Ts"
-            by (cases Us) (rule FalseE, simp+, erule that)
+            by (cases Us) (rule FalseE, simp)
           from varT and Us have varT: "e\<langle>i:T\<rangle> \<turnstile> Var x : T'' \<Rightarrow> Ts \<Rrightarrow> T'"
             by simp
           from varT eq have T: "T = T'' \<Rightarrow> Ts \<Rrightarrow> T'" by cases auto
diff -r 31e427387ab5 -r 29e308b56d23 src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/Quotient.thy	Thu Mar 13 07:07:07 2014 +0100
@@ -487,15 +487,7 @@
 
 lemma bex1_bexeq_reg:
   shows "(\<exists>!x\<in>Respects R. P x) \<longrightarrow> (Bex1_rel R (\<lambda>x. P x))"
-  apply (simp add: Ex1_def Bex1_rel_def in_respects)
-  apply clarify
-  apply auto
-  apply (rule bexI)
-  apply assumption
-  apply (simp add: in_respects)
-  apply (simp add: in_respects)
-  apply auto
-  done
+  by (auto simp add: Ex1_def Bex1_rel_def Bex_def Ball_def in_respects)
 
 lemma bex1_bexeq_reg_eqv:
   assumes a: "equivp R"
diff -r 31e427387ab5 -r 29e308b56d23 src/HOL/Tools/simpdata.ML
--- a/src/HOL/Tools/simpdata.ML	Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/Tools/simpdata.ML	Thu Mar 13 07:07:07 2014 +0100
@@ -109,10 +109,21 @@
 fun mksimps pairs (_: Proof.context) =
   map_filter (try mk_eq) o mk_atomize pairs o gen_all;
 
+val simp_legacy_precond =
+  Attrib.setup_config_bool @{binding "simp_legacy_precond"} (K false)
+
 fun unsafe_solver_tac ctxt =
-  (fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN'
-  FIRST' [resolve_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ctxt),
-    atac, etac @{thm FalseE}];
+  let
+    val intros =
+      if Config.get ctxt simp_legacy_precond then [] else [@{thm conjI}]
+    val sol_thms =
+      reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ctxt;
+    fun sol_tac i =
+      FIRST [resolve_tac sol_thms i, atac i , etac @{thm FalseE} i] ORELSE
+      (match_tac intros THEN_ALL_NEW sol_tac) i
+  in
+    (fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN' sol_tac
+  end;
 
 val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac;
 
diff -r 31e427387ab5 -r 29e308b56d23 src/HOL/Word/Bool_List_Representation.thy
--- a/src/HOL/Word/Bool_List_Representation.thy	Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/Word/Bool_List_Representation.thy	Thu Mar 13 07:07:07 2014 +0100
@@ -941,7 +941,6 @@
   apply (subst bin_rsplit_aux.simps)
   apply (subst bin_rsplit_aux.simps)
   apply (clarsimp split: prod.split)
-  apply auto
   done
 
 lemma bin_rsplitl_aux_append:
@@ -950,7 +949,6 @@
   apply (subst bin_rsplitl_aux.simps)
   apply (subst bin_rsplitl_aux.simps)
   apply (clarsimp split: prod.split)
-  apply auto
   done
 
 lemmas rsplit_aux_apps [where bs = "[]"] =
diff -r 31e427387ab5 -r 29e308b56d23 src/HOL/ZF/HOLZF.thy
--- a/src/HOL/ZF/HOLZF.thy	Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/ZF/HOLZF.thy	Thu Mar 13 07:07:07 2014 +0100
@@ -261,7 +261,7 @@
   apply (frule Elem_Elem_PFun[where p=y], simp)
   apply (subgoal_tac "isFun F")
   apply (simp add: isFun_def isOpair_def)  
-  apply (auto simp add: Fst Snd, blast)
+  apply (auto simp add: Fst Snd)
   apply (auto simp add: PFun_def Sep)
   done