enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions
authornipkow
Thu Mar 13 07:07:07 2014 +0100 (2014-03-13)
changeset 5607329e308b56d23
parent 56072 31e427387ab5
child 56074 30a60277aa6e
enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions
NEWS
src/HOL/Auth/Guard/Guard_Yahalom.thy
src/HOL/Auth/Public.thy
src/HOL/Auth/ZhouGollmann.thy
src/HOL/Bali/Example.thy
src/HOL/Bali/Trans.thy
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
src/HOL/HOLCF/IOA/meta_theory/Seq.thy
src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy
src/HOL/HOLCF/IOA/meta_theory/TLS.thy
src/HOL/HOLCF/Universal.thy
src/HOL/Hoare_Parallel/RG_Tran.thy
src/HOL/Imperative_HOL/ex/Linked_Lists.thy
src/HOL/Isar_Examples/Hoare_Ex.thy
src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
src/HOL/MicroJava/BV/BVNoTypeError.thy
src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
src/HOL/MicroJava/BV/EffectMono.thy
src/HOL/MicroJava/BV/JVMType.thy
src/HOL/MicroJava/Comp/CorrComp.thy
src/HOL/MicroJava/Comp/CorrCompTp.thy
src/HOL/MicroJava/J/Eval.thy
src/HOL/MicroJava/J/WellForm.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Nominal/Examples/Class1.thy
src/HOL/Nominal/Examples/Class2.thy
src/HOL/Old_Number_Theory/Pocklington.thy
src/HOL/Proofs/Lambda/LambdaType.thy
src/HOL/Proofs/Lambda/WeakNorm.thy
src/HOL/Quotient.thy
src/HOL/Tools/simpdata.ML
src/HOL/Word/Bool_List_Representation.thy
src/HOL/ZF/HOLZF.thy
     1.1 --- a/NEWS	Wed Mar 12 22:57:50 2014 +0100
     1.2 +++ b/NEWS	Thu Mar 13 07:07:07 2014 +0100
     1.3 @@ -98,6 +98,12 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Simplifier: Enhanced solver of preconditions of rewrite rules
     1.8 +  can now deal with conjunctions.
     1.9 +  For help with converting proofs, the old behaviour of the simplifier
    1.10 +  can be restored like this:  declare/using [[simp_legacy_precond]]
    1.11 +  This configuration option will disappear again in the future.
    1.12 +
    1.13  * HOL-Word:
    1.14    * Abandoned fact collection "word_arith_alts", which is a
    1.15    duplicate of "word_arith_wis".
     2.1 --- a/src/HOL/Auth/Guard/Guard_Yahalom.thy	Wed Mar 12 22:57:50 2014 +0100
     2.2 +++ b/src/HOL/Auth/Guard/Guard_Yahalom.thy	Thu Mar 13 07:07:07 2014 +0100
     2.3 @@ -218,12 +218,12 @@
     2.4  apply (rule Guard_extand, simp, blast)
     2.5  apply (case_tac "NAa=NB", clarify)
     2.6  apply (frule Says_imp_spies)
     2.7 -apply (frule in_Guard_kparts_Crypt, simp+, blast, simp+)
     2.8 +apply (frule in_Guard_kparts_Crypt, simp+)
     2.9  apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Ba in ya3_shrK, simp)
    2.10  apply (drule ya2'_imp_ya1'_parts, simp, blast, blast)
    2.11  apply (case_tac "NBa=NB", clarify)
    2.12  apply (frule Says_imp_spies)
    2.13 -apply (frule in_Guard_kparts_Crypt, simp+, blast, simp+)
    2.14 +apply (frule in_Guard_kparts_Crypt, simp+)
    2.15  apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Ba in ya3_shrK, simp)
    2.16  apply (drule NB_is_uniq_in_ya2', simp+, blast, simp+)
    2.17  apply (simp add: No_Nonce, blast)
    2.18 @@ -239,7 +239,7 @@
    2.19  apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Aa in ya3_shrK, simp)
    2.20  apply (frule ya3'_imp_ya2', simp+, blast, clarify)
    2.21  apply (frule_tac A=B' in Says_imp_spies)
    2.22 -apply (rotate_tac -1, frule in_Guard_kparts_Crypt, simp+, blast, simp+)
    2.23 +apply (rotate_tac -1, frule in_Guard_kparts_Crypt, simp+)
    2.24  apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Ba in ya3_shrK, simp)
    2.25  apply (drule NB_is_uniq_in_ya2', simp+, blast, clarify)
    2.26  apply (drule ya3'_imp_ya3, simp+)
     3.1 --- a/src/HOL/Auth/Public.thy	Wed Mar 12 22:57:50 2014 +0100
     3.2 +++ b/src/HOL/Auth/Public.thy	Thu Mar 13 07:07:07 2014 +0100
     3.3 @@ -414,7 +414,7 @@
     3.4  (*Tactic for possibility theorems*)
     3.5  fun possibility_tac ctxt =
     3.6      REPEAT (*omit used_Says so that Nonces start from different traces!*)
     3.7 -    (ALLGOALS (simp_tac (ctxt delsimps [@{thm used_Says}]))
     3.8 +    (ALLGOALS (simp_tac (ctxt setSolver safe_solver delsimps [@{thm used_Says}]))
     3.9       THEN
    3.10       REPEAT_FIRST (eq_assume_tac ORELSE' 
    3.11                     resolve_tac [refl, conjI, @{thm Nonce_supply}]))
     4.1 --- a/src/HOL/Auth/ZhouGollmann.thy	Wed Mar 12 22:57:50 2014 +0100
     4.2 +++ b/src/HOL/Auth/ZhouGollmann.thy	Thu Mar 13 07:07:07 2014 +0100
     4.3 @@ -101,7 +101,7 @@
     4.4                       THEN zg.ZG2, THEN zg.Reception [of _ B A],
     4.5                       THEN zg.ZG3, THEN zg.Reception [of _ A TTP], 
     4.6                       THEN zg.ZG4])
     4.7 -apply (possibility, auto)
     4.8 +apply (basic_possibility, auto)
     4.9  done
    4.10  
    4.11  subsection {*Basic Lemmas*}
     5.1 --- a/src/HOL/Bali/Example.thy	Wed Mar 12 22:57:50 2014 +0100
     5.2 +++ b/src/HOL/Bali/Example.thy	Thu Mar 13 07:07:07 2014 +0100
     5.3 @@ -1280,8 +1280,6 @@
     5.4  apply   (rule conjI)
     5.5  apply    (rule eval_Is (* Init Object *))
     5.6  apply    (simp)
     5.7 -apply    (rule conjI, rule HOL.refl)+
     5.8 -apply    (rule HOL.refl)
     5.9  apply   (simp)
    5.10  apply   (rule conjI, rule_tac [2] HOL.refl)
    5.11  apply   (rule eval_Is (* Expr *))
     6.1 --- a/src/HOL/Bali/Trans.thy	Wed Mar 12 22:57:50 2014 +0100
     6.2 +++ b/src/HOL/Bali/Trans.thy	Thu Mar 13 07:07:07 2014 +0100
     6.3 @@ -23,12 +23,7 @@
     6.4      | (FVar) accC statDeclC stat a fn where "v={accC,statDeclC,stat}(Lit a)..fn"
     6.5      | (AVar) a i where "v=(Lit a).[Lit i]"
     6.6    using ground LVar FVar AVar
     6.7 -  apply (cases v)
     6.8 -  apply (simp add: groundVar_def)
     6.9 -  apply (simp add: groundVar_def,blast)
    6.10 -  apply (simp add: groundVar_def,blast)
    6.11 -  apply (simp add: groundVar_def)
    6.12 -  done
    6.13 +  by (cases v) (auto simp add: groundVar_def)
    6.14  
    6.15  definition
    6.16    groundExprs :: "expr list \<Rightarrow> bool"
     7.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Wed Mar 12 22:57:50 2014 +0100
     7.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Thu Mar 13 07:07:07 2014 +0100
     7.3 @@ -2613,7 +2613,7 @@
     7.4      and inequality: "u \<le> lx \<and> ux \<le> l'"
     7.5      by (cases "approx prec x vs", auto,
     7.6        cases "approx prec a vs", auto,
     7.7 -      cases "approx prec b vs", auto, blast)
     7.8 +      cases "approx prec b vs", auto)
     7.9    from inequality approx[OF AtLeastAtMost.prems(2) l_eq] approx[OF AtLeastAtMost.prems(2) u_eq] approx[OF AtLeastAtMost.prems(2) x_eq]
    7.10    show ?case by auto
    7.11  qed
    7.12 @@ -2902,7 +2902,7 @@
    7.13                 (Mult (Inverse (Num (Float (int k) 0)))
    7.14                       (Mult (Add (Var (Suc (Suc 0))) (Minus (Num c)))
    7.15                             (Var (Suc 0))))) [Some (l1, u1), Some (l2, u2), vs!x]"
    7.16 -      by (auto elim!: lift_bin) blast
    7.17 +      by (auto elim!: lift_bin)
    7.18  
    7.19      from bnd_c `x < length xs`
    7.20      have bnd: "bounded_by (xs[x:=c]) (vs[x:= Some (c,c)])"
     8.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Wed Mar 12 22:57:50 2014 +0100
     8.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Thu Mar 13 07:07:07 2014 +0100
     8.3 @@ -473,7 +473,6 @@
     8.4        then have ?case using 4
     8.5          apply (cases "p +\<^sub>p p' = 0\<^sub>p")
     8.6          apply (auto simp add: Let_def)
     8.7 -        apply blast
     8.8          done
     8.9      }
    8.10      ultimately have ?case by blast
     9.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Seq.thy	Wed Mar 12 22:57:50 2014 +0100
     9.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Seq.thy	Thu Mar 13 07:07:07 2014 +0100
     9.3 @@ -5,7 +5,7 @@
     9.4  header {* Partial, Finite and Infinite Sequences (lazy lists), modeled as domain *}
     9.5  
     9.6  theory Seq
     9.7 -imports HOLCF
     9.8 +imports "../../HOLCF"
     9.9  begin
    9.10  
    9.11  default_sort pcpo
    10.1 --- a/src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy	Wed Mar 12 22:57:50 2014 +0100
    10.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy	Thu Mar 13 07:07:07 2014 +0100
    10.3 @@ -99,7 +99,6 @@
    10.4  apply (erule conjE)
    10.5  apply (simp add: Let_def)
    10.6  apply (rule_tac x = "ex" in someI)
    10.7 -apply (erule conjE)
    10.8  apply assumption
    10.9  done
   10.10  
    11.1 --- a/src/HOL/HOLCF/IOA/meta_theory/TLS.thy	Wed Mar 12 22:57:50 2014 +0100
    11.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/TLS.thy	Thu Mar 13 07:07:07 2014 +0100
    11.3 @@ -196,10 +196,7 @@
    11.4  apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
    11.5  apply (tactic {* pair_tac @{context} "a" 1 *})
    11.6  apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
    11.7 -apply blast
    11.8 -apply fastforce
    11.9  apply (tactic {* pair_tac @{context} "a" 1 *})
   11.10 - apply fastforce
   11.11  done
   11.12  
   11.13  end
    12.1 --- a/src/HOL/HOLCF/Universal.thy	Wed Mar 12 22:57:50 2014 +0100
    12.2 +++ b/src/HOL/HOLCF/Universal.thy	Thu Mar 13 07:07:07 2014 +0100
    12.3 @@ -111,12 +111,11 @@
    12.4    "ubasis_until P 0 = 0"
    12.5  | "finite S \<Longrightarrow> ubasis_until P (node i a S) =
    12.6      (if P (node i a S) then node i a S else ubasis_until P a)"
    12.7 -    apply clarify
    12.8 -    apply (rule_tac x=b in node_cases)
    12.9 -     apply simp
   12.10 +   apply clarify
   12.11 +   apply (rule_tac x=b in node_cases)
   12.12      apply simp
   12.13 -    apply fast
   12.14     apply simp
   12.15 +   apply fast
   12.16    apply simp
   12.17   apply simp
   12.18  done
    13.1 --- a/src/HOL/Hoare_Parallel/RG_Tran.thy	Wed Mar 12 22:57:50 2014 +0100
    13.2 +++ b/src/HOL/Hoare_Parallel/RG_Tran.thy	Thu Mar 13 07:07:07 2014 +0100
    13.3 @@ -196,7 +196,6 @@
    13.4  apply(erule_tac x="Some P2" in allE)
    13.5  apply(erule allE,erule impE, assumption)
    13.6  apply(drule div_seq,simp)
    13.7 -apply force
    13.8  apply clarify
    13.9  apply(erule disjE)
   13.10   apply clarify
    14.1 --- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Wed Mar 12 22:57:50 2014 +0100
    14.2 +++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Thu Mar 13 07:07:07 2014 +0100
    14.3 @@ -918,7 +918,7 @@
    14.4    from 3(7)[OF no_inter2] obtain rs where rs_def: "refs_of' h1 r1 rs" by (rule list_of'_refs_of')
    14.5    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
    14.6    with 3(7)[OF no_inter2] 3(1-5) 3(8) p_rs rs_def p_stays
    14.7 -  show ?case by auto
    14.8 +  show ?case by (auto simp: list_of'_set_ref)
    14.9  next
   14.10    case (4 x xs' y ys' p q pn qn h1 r1 h')
   14.11    from 4(1) obtain prs where prs_def: "refs_of' h p prs" by (rule list_of'_refs_of')
   14.12 @@ -935,7 +935,7 @@
   14.13    from 4(7)[OF no_inter2] obtain rs where rs_def: "refs_of' h1 r1 rs" by (rule list_of'_refs_of')
   14.14    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
   14.15    with 4(7)[OF no_inter2] 4(1-5) 4(8) q_rs rs_def q_stays
   14.16 -  show ?case by auto
   14.17 +  show ?case by (auto simp: list_of'_set_ref)
   14.18  qed
   14.19  
   14.20  section {* Code generation *}
    15.1 --- a/src/HOL/Isar_Examples/Hoare_Ex.thy	Wed Mar 12 22:57:50 2014 +0100
    15.2 +++ b/src/HOL/Isar_Examples/Hoare_Ex.thy	Thu Mar 13 07:07:07 2014 +0100
    15.3 @@ -59,7 +59,7 @@
    15.4    by hoare
    15.5  
    15.6  lemma "\<turnstile> \<lbrace>True\<rbrace> \<acute>M := a; \<acute>N := b \<lbrace>\<acute>M = a \<and> \<acute>N = b\<rbrace>"
    15.7 -  by hoare simp
    15.8 +  by hoare
    15.9  
   15.10  lemma
   15.11    "\<turnstile> \<lbrace>\<acute>M = a \<and> \<acute>N = b\<rbrace>
    16.1 --- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Wed Mar 12 22:57:50 2014 +0100
    16.2 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Thu Mar 13 07:07:07 2014 +0100
    16.3 @@ -204,7 +204,6 @@
    16.4      apply auto
    16.5      apply (case_tac xc)
    16.6      apply auto
    16.7 -    apply fastforce
    16.8      done
    16.9  qed
   16.10  
    17.1 --- a/src/HOL/MicroJava/BV/BVNoTypeError.thy	Wed Mar 12 22:57:50 2014 +0100
    17.2 +++ b/src/HOL/MicroJava/BV/BVNoTypeError.thy	Thu Mar 13 07:07:07 2014 +0100
    17.3 @@ -236,7 +236,7 @@
    17.4      then obtain stk loc C sig pc frs' where
    17.5        xcp [simp]: "xcp = None" and
    17.6        frs [simp]: "frs = (stk,loc,C,sig,pc)#frs'" 
    17.7 -      by (clarsimp simp add: neq_Nil_conv) fast
    17.8 +      by (clarsimp simp add: neq_Nil_conv)
    17.9  
   17.10      from conforms obtain  ST LT rT maxs maxl ins et where
   17.11        hconf:  "G \<turnstile>h hp \<surd>" and
   17.12 @@ -245,7 +245,7 @@
   17.13        phi:    "Phi C sig ! pc = Some (ST,LT)" and
   17.14        frame:  "correct_frame G hp (ST,LT) maxl ins (stk,loc,C,sig,pc)" and
   17.15        frames: "correct_frames G hp Phi rT sig frs'"
   17.16 -      by (auto simp add: correct_state_def) (rule that)
   17.17 +      by (auto simp add: correct_state_def)
   17.18  
   17.19      from frame obtain
   17.20        stk: "approx_stk G hp stk ST" and
   17.21 @@ -354,7 +354,7 @@
   17.22          obtain D fs where
   17.23            hp: "hp (the_Addr x) = Some (D,fs)" and
   17.24            D:  "G \<turnstile> D \<preceq>C C"
   17.25 -          by - (drule non_npD, assumption, clarsimp, blast)
   17.26 +          by - (drule non_npD, assumption, clarsimp)
   17.27          hence "hp (the_Addr x) \<noteq> None" (is ?P1) by simp
   17.28          moreover
   17.29          from wf mth hp D
    18.1 --- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Wed Mar 12 22:57:50 2014 +0100
    18.2 +++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Thu Mar 13 07:07:07 2014 +0100
    18.3 @@ -889,7 +889,7 @@
    18.4      loc:    "hp ref = Some obj" and
    18.5      obj_ty: "obj_ty obj = Class D" and
    18.6      D:      "G \<turnstile> Class D \<preceq> X"
    18.7 -    by (auto simp add: conf_def) blast
    18.8 +    by (auto simp add: conf_def)
    18.9    
   18.10    with X_Ref obtain X' where X': "X = Class X'"
   18.11      by (blast dest: widen_Class)
   18.12 @@ -1052,7 +1052,7 @@
   18.13        meth'': "method (G, D) sig = Some (D'', rT'', body)" and
   18.14        ST0':   "ST' = rev apTs @ Class D # ST0'" and
   18.15        len':   "length apTs = length pt" 
   18.16 -      by clarsimp blast    
   18.17 +      by clarsimp
   18.18  
   18.19      from f frame'
   18.20      obtain
   18.21 @@ -1074,7 +1074,7 @@
   18.22        methD':  "method (G, D') sig = Some (mD, rT0, body')" and
   18.23        lessD':  "G \<turnstile> X \<preceq> Class D'" and
   18.24        suc_pc': "Suc pc' < length ins'"
   18.25 -      by (clarsimp simp add: wt_instr_def eff_def norm_eff_def) blast
   18.26 +      by (clarsimp simp add: wt_instr_def eff_def norm_eff_def)
   18.27  
   18.28      from len len' ST0 ST0'
   18.29      have "X = Class D" by simp
    19.1 --- a/src/HOL/MicroJava/BV/EffectMono.thy	Wed Mar 12 22:57:50 2014 +0100
    19.2 +++ b/src/HOL/MicroJava/BV/EffectMono.thy	Thu Mar 13 07:07:07 2014 +0100
    19.3 @@ -161,7 +161,7 @@
    19.4          where s2:  "s2 = (vT' # oT' # ST', LT')" and
    19.5                oT': "G\<turnstile> oT' \<preceq> oT" and
    19.6                vT': "G\<turnstile> vT' \<preceq> vT"
    19.7 -        by - (cases s2, simp add: sup_state_Cons2, elim exE conjE, simp, rule that)
    19.8 +        by - (cases s2, simp add: sup_state_Cons2, elim exE conjE, simp)
    19.9        moreover
   19.10        from vT' vT
   19.11        have "G \<turnstile> vT' \<preceq> b" by (rule widen_trans)
    20.1 --- a/src/HOL/MicroJava/BV/JVMType.thy	Wed Mar 12 22:57:50 2014 +0100
    20.2 +++ b/src/HOL/MicroJava/BV/JVMType.thy	Thu Mar 13 07:07:07 2014 +0100
    20.3 @@ -258,7 +258,7 @@
    20.4      assume l: "length (l#ls) = length b"
    20.5      
    20.6      then obtain b' bs where b: "b = b'#bs"
    20.7 -      by (cases b) (simp, simp add: neq_Nil_conv, rule that)
    20.8 +      by (cases b) (simp, simp add: neq_Nil_conv)
    20.9  
   20.10      with f
   20.11      have "\<forall>n. n < length ls \<longrightarrow> (G \<turnstile> (ls!n) <=o (bs!n))"
    21.1 --- a/src/HOL/MicroJava/Comp/CorrComp.thy	Wed Mar 12 22:57:50 2014 +0100
    21.2 +++ b/src/HOL/MicroJava/Comp/CorrComp.thy	Thu Mar 13 07:07:07 2014 +0100
    21.3 @@ -523,7 +523,6 @@
    21.4  apply (rule_tac ?instrs0.0 = "[load_default_val b]" in progression_transitive, simp)
    21.5  apply (rule progression_one_step)
    21.6  apply (simp (no_asm_simp) add: load_default_val_def)
    21.7 -apply (rule conjI, simp)+ apply (rule HOL.refl)
    21.8  
    21.9  apply (rule progression_one_step)
   21.10  apply (simp (no_asm_simp))
   21.11 @@ -816,7 +815,7 @@
   21.12  apply (rule_tac ?instrs0.0 = "[Dup]" in progression_transitive, simp)
   21.13  apply (rule progression_one_step)
   21.14  apply (simp add: gh_def)
   21.15 -apply (rule conjI, simp)+ apply simp
   21.16 +apply simp
   21.17  apply (rule progression_one_step)
   21.18  apply (simp add: gh_def)
   21.19  (* the following falls out of the general scheme *)
   21.20 @@ -865,8 +864,6 @@
   21.21     (* Dup_x1 *)
   21.22     apply (rule progression_one_step)
   21.23     apply (simp add: gh_def)
   21.24 -   apply (rule conjI, simp)+ apply simp
   21.25 -
   21.26  
   21.27     (* Putfield \<longrightarrow> still looks nasty*)
   21.28     apply (rule progression_one_step)
   21.29 @@ -948,7 +945,6 @@
   21.30  apply simp
   21.31  apply (rule_tac ?instrs0.0 = "[LitPush (Bool False)]" in progression_transitive, simp (no_asm_simp))
   21.32  apply (rule progression_one_step,  simp)
   21.33 -apply (rule conjI, rule HOL.refl)+ apply (rule HOL.refl)
   21.34  
   21.35  apply (rule_tac ?instrs0.0 = "compExpr (gmb G CL S) e" in progression_transitive, rule HOL.refl)
   21.36  apply fast
   21.37 @@ -958,18 +954,17 @@
   21.38  apply simp
   21.39  apply (rule_tac ?instrs0.0 = "[Ifcmpeq (2 + int (length (compStmt (gmb G CL S) c1)))]" in progression_transitive, simp)
   21.40  apply (rule progression_one_step) apply simp
   21.41 -apply (rule conjI, rule HOL.refl)+ apply (rule HOL.refl)
   21.42  apply (rule_tac ?instrs0.0 = "(compStmt (gmb G CL S) c1)" in progression_transitive, simp)
   21.43  apply fast
   21.44  apply (rule_tac ?instrs1.0 = "[]" in jump_fwd_progression)
   21.45 -apply (simp, rule conjI, (rule HOL.refl)+)
   21.46 +apply (simp)
   21.47  apply simp apply (rule conjI, simp) apply (simp add: nat_add_distrib)
   21.48  apply (rule progression_refl)
   21.49  
   21.50   (* case b= False *)
   21.51  apply simp
   21.52  apply (rule_tac ?instrs1.0 = "compStmt (gmb G CL S) c2" in jump_fwd_progression)
   21.53 -apply (simp, rule conjI, (rule HOL.refl)+)
   21.54 +apply (simp)
   21.55  apply (simp, rule conjI, rule HOL.refl, simp add: nat_add_distrib)
   21.56  apply fast
   21.57  
   21.58 @@ -992,12 +987,11 @@
   21.59  apply (rule_tac ?instrs0.0 = "[LitPush (Bool False)]" in progression_transitive, simp (no_asm_simp))
   21.60  apply (rule progression_one_step)
   21.61     apply simp 
   21.62 -   apply (rule conjI, rule HOL.refl)+ apply (rule HOL.refl)
   21.63  
   21.64  apply (rule_tac ?instrs0.0 = "compExpr (gmb G CL S) e" in progression_transitive, rule HOL.refl)
   21.65  apply fast
   21.66  apply (rule_tac ?instrs1.0 = "[]" in jump_fwd_progression)
   21.67 -apply (simp, rule conjI, rule HOL.refl, rule HOL.refl)
   21.68 +apply (simp)
   21.69  apply (simp, rule conjI, rule HOL.refl, simp add: nat_add_distrib)
   21.70  apply (rule progression_refl)
   21.71  
   21.72 @@ -1022,12 +1016,10 @@
   21.73  apply simp
   21.74  apply (rule jump_bwd_progression) 
   21.75  apply simp
   21.76 -apply (rule conjI, (rule HOL.refl)+)
   21.77  
   21.78  apply (rule_tac ?instrs0.0 = "[LitPush (Bool False)]" in progression_transitive, simp (no_asm_simp))
   21.79  apply (rule progression_one_step)
   21.80     apply simp 
   21.81 -   apply (rule conjI, simp)+ apply simp
   21.82  
   21.83  apply (rule_tac ?instrs0.0 = "compExpr (gmb G CL S) e" in progression_transitive, rule HOL.refl)
   21.84  apply fast
   21.85 @@ -1038,7 +1030,6 @@
   21.86  
   21.87  apply (rule_tac ?instrs0.0 = "[Ifcmpeq (2 + int (length (compStmt (gmb G CL S) c)))]" in progression_transitive, simp)
   21.88  apply (rule progression_one_step) apply simp
   21.89 -apply (rule conjI, rule HOL.refl)+ apply (rule HOL.refl)
   21.90  apply fast
   21.91  
   21.92   (* case b= False \<longrightarrow> contradiction*)
   21.93 @@ -1126,7 +1117,6 @@
   21.94  apply (simp (no_asm_use) only: exec_instr.simps)
   21.95  apply (erule thin_rl, erule thin_rl, erule thin_rl)
   21.96  apply (simp add: compMethod_def raise_system_xcpt_def)
   21.97 -apply (rule conjI, simp)+ apply (rule HOL.refl)
   21.98  
   21.99       (* get instructions of invoked method *)
  21.100  apply (simp (no_asm_simp) add: gis_def gmb_def compMethod_def)
  21.101 @@ -1177,7 +1167,6 @@
  21.102  apply (frule non_npD) apply assumption
  21.103  apply (erule exE)+ apply simp
  21.104  apply (rule conf_obj_AddrI) apply simp 
  21.105 -apply (rule conjI, (rule HOL.refl)+)
  21.106  apply (rule widen_Class_Class [THEN iffD1], rule widen.refl)
  21.107  
  21.108  
    22.1 --- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Wed Mar 12 22:57:50 2014 +0100
    22.2 +++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Thu Mar 13 07:07:07 2014 +0100
    22.3 @@ -1268,7 +1268,6 @@
    22.4    apply (frule max_spec2mheads, (erule exE)+, (erule conjE)+)
    22.5    apply (rule exI)+
    22.6    apply (simp add: wf_prog_ws_prog [THEN comp_method])
    22.7 -  apply auto
    22.8    done
    22.9  
   22.10  
   22.11 @@ -2517,16 +2516,13 @@
   22.12                                (start_ST, start_LT C pTs (length lvars))))
   22.13                  = (start_ST, inited_LT C pTs lvars)") 
   22.14     prefer 2 apply (rule compTpInitLvars_LT_ST) apply (rule HOL.refl) apply assumption
   22.15 -apply (simp only:)
   22.16  apply (subgoal_tac "(snd (compTpStmt (pns, lvars, blk, res) G blk
   22.17                         (start_ST, inited_LT C pTs lvars))) 
   22.18                  = (start_ST, inited_LT C pTs lvars)") 
   22.19     prefer 2 apply (erule conjE)+
   22.20     apply (rule compTpStmt_LT_ST) apply (rule HOL.refl) apply assumption+
   22.21     apply (simp only:)+ apply (simp (no_asm_simp) add: is_inited_LT_def)
   22.22 -apply (simp only:)
   22.23 -apply (rule compTpExpr_LT_ST) apply (rule HOL.refl) apply assumption+
   22.24 -   apply (simp only:)+ apply (simp (no_asm_simp) add: is_inited_LT_def)
   22.25 +   apply (simp (no_asm_simp) add: is_inited_LT_def)
   22.26  
   22.27  
   22.28     (* Return *)
    23.1 --- a/src/HOL/MicroJava/J/Eval.thy	Wed Mar 12 22:57:50 2014 +0100
    23.2 +++ b/src/HOL/MicroJava/J/Eval.thy	Thu Mar 13 07:07:07 2014 +0100
    23.3 @@ -226,7 +226,7 @@
    23.4    next
    23.5      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)
    23.6      with Call_code show ?thesis
    23.7 -      by(cases "s4")(simp, (erule meta_allE meta_impE|rule conjI refl| assumption)+)
    23.8 +      by(cases "s4") auto
    23.9    qed(erule (3) that[OF refl]|assumption)+
   23.10  next
   23.11    case evals
    24.1 --- a/src/HOL/MicroJava/J/WellForm.thy	Wed Mar 12 22:57:50 2014 +0100
    24.2 +++ b/src/HOL/MicroJava/J/WellForm.thy	Thu Mar 13 07:07:07 2014 +0100
    24.3 @@ -565,7 +565,7 @@
    24.4  apply clarify
    24.5  apply (frule wf_prog_ws_prog)
    24.6  apply (frule fields_Object, assumption+)
    24.7 -apply (simp only: is_class_Object) apply simp
    24.8 +apply (simp only: is_class_Object)
    24.9  
   24.10  apply clarify
   24.11  apply (frule fields_rec)
    25.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Mar 12 22:57:50 2014 +0100
    25.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Mar 13 07:07:07 2014 +0100
    25.3 @@ -2958,10 +2958,10 @@
    25.4    fix f
    25.5    assume *: "Ball f open" "s \<union> t \<subseteq> \<Union>f"
    25.6    from * `compact s` obtain s' where "s' \<subseteq> f \<and> finite s' \<and> s \<subseteq> \<Union>s'"
    25.7 -    unfolding compact_eq_heine_borel by (auto elim!: allE[of _ f]) metis
    25.8 +    unfolding compact_eq_heine_borel by (auto elim!: allE[of _ f])
    25.9    moreover
   25.10    from * `compact t` obtain t' where "t' \<subseteq> f \<and> finite t' \<and> t \<subseteq> \<Union>t'"
   25.11 -    unfolding compact_eq_heine_borel by (auto elim!: allE[of _ f]) metis
   25.12 +    unfolding compact_eq_heine_borel by (auto elim!: allE[of _ f])
   25.13    ultimately show "\<exists>f'\<subseteq>f. finite f' \<and> s \<union> t \<subseteq> \<Union>f'"
   25.14      by (auto intro!: exI[of _ "s' \<union> t'"])
   25.15  qed
    26.1 --- a/src/HOL/Nominal/Examples/Class1.thy	Wed Mar 12 22:57:50 2014 +0100
    26.2 +++ b/src/HOL/Nominal/Examples/Class1.thy	Thu Mar 13 07:07:07 2014 +0100
    26.3 @@ -1702,32 +1702,13 @@
    26.4  next
    26.5    case (NotR y M d)
    26.6    then show ?case 
    26.7 -    apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
    26.8 -    apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(N,M{d:=(x).N},([(c,d)]\<bullet>M){c:=(x).N})")
    26.9 -    apply(erule exE, simp add: fresh_prod)
   26.10 -    apply(erule conjE)+
   26.11 -    apply(simp add: fresh_fun_simp_NotR)
   26.12 -    apply(simp add: trm.inject alpha)
   26.13 -    apply(rule exists_fresh'(2)[OF fs_coname1])
   26.14 -    done
   26.15 +    by(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
   26.16  next
   26.17    case (AndR c1 M c2 M' c3)
   26.18    then show ?case
   26.19 -    apply(simp)
   26.20 -    apply(auto)
   26.21 -    apply(simp add: fresh_prod calc_atm fresh_atm abs_fresh)
   26.22 -    apply(simp add: fresh_prod calc_atm fresh_atm abs_fresh fresh_left)
   26.23 -    apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(N,M{c3:=(x).N},
   26.24 -                  M'{c3:=(x).N},c1,c2,c3,([(c,c3)]\<bullet>M){c:=(x).N},([(c,c3)]\<bullet>M'){c:=(x).N})")
   26.25 -    apply(erule exE, simp add: fresh_prod)
   26.26 -    apply(erule conjE)+
   26.27 -    apply(simp add: fresh_fun_simp_AndR)
   26.28 -    apply (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh subst_fresh)
   26.29 -    apply(rule exists_fresh'(2)[OF fs_coname1])
   26.30 -    apply(simp add: fresh_prod calc_atm fresh_atm abs_fresh fresh_left)
   26.31 -    apply(simp add: fresh_prod calc_atm fresh_atm abs_fresh fresh_left)
   26.32 -    apply(auto simp add: trm.inject alpha)
   26.33 -    done
   26.34 +    apply(auto simp add: fresh_prod calc_atm fresh_atm abs_fresh fresh_left)
   26.35 +    apply (metis (erased, hide_lams))
   26.36 +    by metis
   26.37  next
   26.38    case AndL1
   26.39    then show ?case by (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
   26.40 @@ -1737,25 +1718,11 @@
   26.41  next
   26.42    case (OrR1 d M e)
   26.43    then show ?case 
   26.44 -    apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
   26.45 -    apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(N,M{e:=(x).N},([(c,e)]\<bullet>M){c:=(x).N},d,e)")
   26.46 -    apply(erule exE, simp add: fresh_prod)
   26.47 -    apply(erule conjE)+
   26.48 -    apply(simp add: fresh_fun_simp_OrR1)
   26.49 -    apply(simp add: trm.inject alpha)
   26.50 -    apply(rule exists_fresh'(2)[OF fs_coname1])
   26.51 -    done
   26.52 +    by(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
   26.53  next
   26.54    case (OrR2 d M e)
   26.55    then show ?case 
   26.56 -    apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
   26.57 -    apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(N,M{e:=(x).N},([(c,e)]\<bullet>M){c:=(x).N},d,e)")
   26.58 -    apply(erule exE, simp add: fresh_prod)
   26.59 -    apply(erule conjE)+
   26.60 -    apply(simp add: fresh_fun_simp_OrR2)
   26.61 -    apply(simp add: trm.inject alpha)
   26.62 -    apply(rule exists_fresh'(2)[OF fs_coname1])
   26.63 -    done
   26.64 +    by(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
   26.65  next
   26.66    case (OrL x1 M x2 M' x3)
   26.67    then show ?case
   26.68 @@ -1764,24 +1731,16 @@
   26.69    case ImpL
   26.70    then show ?case
   26.71      by (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
   26.72 +       metis
   26.73  next
   26.74    case (ImpR y d M e)
   26.75    then show ?case
   26.76 -    apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
   26.77 -    apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(N,M{e:=(x).N},([(c,e)]\<bullet>M){c:=(x).N},d,e)")
   26.78 -    apply(erule exE, simp add: fresh_prod)
   26.79 -    apply(erule conjE)+
   26.80 -    apply(simp add: fresh_fun_simp_ImpR)
   26.81 -    apply(simp add: trm.inject alpha)
   26.82 -    apply(rule exists_fresh'(2)[OF fs_coname1])
   26.83 -    done
   26.84 +    by(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
   26.85  next
   26.86    case (Cut d M y M')
   26.87    then show ?case
   26.88 -    apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
   26.89 -    apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])
   26.90 -    apply(simp add: calc_atm)
   26.91 -    done
   26.92 +    by(simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
   26.93 +      (metis crename.simps(1) crename_id crename_rename)
   26.94  qed
   26.95  
   26.96  lemma substc_rename2:
   26.97 @@ -1885,14 +1844,7 @@
   26.98  next
   26.99    case (NotL d M z)
  26.100    then show ?case 
  26.101 -    apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
  26.102 -    apply(subgoal_tac "\<exists>a'::name. a'\<sharp>(N,M{x:=<a>.N},([(y,x)]\<bullet>M){y:=<a>.N})")
  26.103 -    apply(erule exE, simp add: fresh_prod)
  26.104 -    apply(erule conjE)+
  26.105 -    apply(simp add: fresh_fun_simp_NotL)
  26.106 -    apply(simp add: trm.inject alpha)
  26.107 -    apply(rule exists_fresh'(1)[OF fs_name1])
  26.108 -    done
  26.109 +    by(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
  26.110  next
  26.111    case (AndR c1 M c2 M' c3)
  26.112    then show ?case
  26.113 @@ -1906,37 +1858,16 @@
  26.114  next
  26.115    case (AndL1 u M v)
  26.116    then show ?case 
  26.117 -    apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
  26.118 -    apply(subgoal_tac "\<exists>a'::name. a'\<sharp>(N,M{x:=<a>.N},([(y,x)]\<bullet>M){y:=<a>.N},u,v)")
  26.119 -    apply(erule exE, simp add: fresh_prod)
  26.120 -    apply(erule conjE)+
  26.121 -    apply(simp add: fresh_fun_simp_AndL1)
  26.122 -    apply(simp add: trm.inject alpha)
  26.123 -    apply(rule exists_fresh'(1)[OF fs_name1])
  26.124 -    done
  26.125 +    by(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
  26.126  next
  26.127    case (AndL2 u M v)
  26.128    then show ?case 
  26.129 -    apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
  26.130 -    apply(subgoal_tac "\<exists>a'::name. a'\<sharp>(N,M{x:=<a>.N},([(y,x)]\<bullet>M){y:=<a>.N},u,v)")
  26.131 -    apply(erule exE, simp add: fresh_prod)
  26.132 -    apply(erule conjE)+
  26.133 -    apply(simp add: fresh_fun_simp_AndL2)
  26.134 -    apply(simp add: trm.inject alpha)
  26.135 -    apply(rule exists_fresh'(1)[OF fs_name1])
  26.136 -    done
  26.137 +    by(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
  26.138  next
  26.139    case (OrL x1 M x2 M' x3)
  26.140    then show ?case
  26.141 -    apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
  26.142 -    apply(subgoal_tac 
  26.143 -    "\<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)")
  26.144 -    apply(erule exE, simp add: fresh_prod)
  26.145 -    apply(erule conjE)+
  26.146 -    apply(simp add: fresh_fun_simp_OrL)
  26.147 -    apply(simp add: trm.inject alpha)
  26.148 -    apply(rule exists_fresh'(1)[OF fs_name1])
  26.149 -    done
  26.150 +    by(simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
  26.151 +      (metis (poly_guards_query))
  26.152  next 
  26.153    case ImpR
  26.154    then show ?case
  26.155 @@ -1944,21 +1875,15 @@
  26.156  next
  26.157    case (ImpL d M v M' u)
  26.158    then show ?case
  26.159 -    apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
  26.160 -    apply(subgoal_tac 
  26.161 -    "\<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)")
  26.162 -    apply(erule exE, simp add: fresh_prod)
  26.163 -    apply(erule conjE)+
  26.164 -    apply(simp add: fresh_fun_simp_ImpL)
  26.165 -    apply(simp add: trm.inject alpha)
  26.166 -    apply(rule exists_fresh'(1)[OF fs_name1])
  26.167 -    done
  26.168 +    by(simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
  26.169 +       (metis (poly_guards_query))
  26.170  next
  26.171    case (Cut d M y M')
  26.172    then show ?case
  26.173      apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
  26.174      apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst])
  26.175      apply(simp add: calc_atm)
  26.176 +    apply metis
  26.177      done
  26.178  qed
  26.179  
    27.1 --- a/src/HOL/Nominal/Examples/Class2.thy	Wed Mar 12 22:57:50 2014 +0100
    27.2 +++ b/src/HOL/Nominal/Examples/Class2.thy	Thu Mar 13 07:07:07 2014 +0100
    27.3 @@ -2869,15 +2869,9 @@
    27.4  apply(rotate_tac 10)
    27.5  apply(drule_tac x="a" in meta_spec)
    27.6  apply(auto simp add: ty.inject)
    27.7 -apply(blast)
    27.8 -apply(blast)
    27.9 -apply(blast)
   27.10  apply(rotate_tac 10)
   27.11  apply(drule_tac x="a" in meta_spec)
   27.12  apply(auto simp add: ty.inject)
   27.13 -apply(blast)
   27.14 -apply(blast)
   27.15 -apply(blast)
   27.16  done
   27.17  
   27.18  termination
    28.1 --- a/src/HOL/Old_Number_Theory/Pocklington.thy	Wed Mar 12 22:57:50 2014 +0100
    28.2 +++ b/src/HOL/Old_Number_Theory/Pocklington.thy	Thu Mar 13 07:07:07 2014 +0100
    28.3 @@ -615,7 +615,7 @@
    28.4              from x(3)[rule_format, of z] z(2,3) have "z=x"
    28.5                unfolding modeq_def mod_less[OF y(2)] by simp}
    28.6            with xm x(1,2) have "\<exists>!x. x \<in> ?S \<and> (?h \<circ> op * a) x = y"
    28.7 -            unfolding modeq_def mod_less[OF y(2)] by auto }
    28.8 +            unfolding modeq_def mod_less[OF y(2)] by safe auto }
    28.9          thus "\<forall>y\<in>{m. coprime m n \<and> m < n}.
   28.10         \<exists>!x. x \<in> {m. coprime m n \<and> m < n} \<and> ((\<lambda>m. m mod n) \<circ> op * a) x = y" by blast
   28.11        next
    29.1 --- a/src/HOL/Proofs/Lambda/LambdaType.thy	Wed Mar 12 22:57:50 2014 +0100
    29.2 +++ b/src/HOL/Proofs/Lambda/LambdaType.thy	Thu Mar 13 07:07:07 2014 +0100
    29.3 @@ -130,10 +130,6 @@
    29.4    apply (case_tac ys)
    29.5    apply simp
    29.6    apply simp
    29.7 -  apply atomize
    29.8 -  apply (erule allE)+
    29.9 -  apply (erule mp, rule conjI)
   29.10 -  apply (rule refl)+
   29.11    done
   29.12  
   29.13  lemma types_snocE: "e \<tturnstile> ts @ [t] : Ts \<Longrightarrow>
   29.14 @@ -142,7 +138,6 @@
   29.15    apply simp
   29.16    apply (case_tac "ts @ [t]")
   29.17    apply (simp add: types_snoc_eq)+
   29.18 -  apply iprover
   29.19    done
   29.20  
   29.21  
    30.1 --- a/src/HOL/Proofs/Lambda/WeakNorm.thy	Wed Mar 12 22:57:50 2014 +0100
    30.2 +++ b/src/HOL/Proofs/Lambda/WeakNorm.thy	Thu Mar 13 07:07:07 2014 +0100
    30.3 @@ -93,7 +93,7 @@
    30.4          next
    30.5            case (Cons a as)
    30.6            with argsT obtain T'' Ts where Us: "Us = T'' # Ts"
    30.7 -            by (cases Us) (rule FalseE, simp+, erule that)
    30.8 +            by (cases Us) (rule FalseE, simp)
    30.9            from varT and Us have varT: "e\<langle>i:T\<rangle> \<turnstile> Var x : T'' \<Rightarrow> Ts \<Rrightarrow> T'"
   30.10              by simp
   30.11            from varT eq have T: "T = T'' \<Rightarrow> Ts \<Rrightarrow> T'" by cases auto
    31.1 --- a/src/HOL/Quotient.thy	Wed Mar 12 22:57:50 2014 +0100
    31.2 +++ b/src/HOL/Quotient.thy	Thu Mar 13 07:07:07 2014 +0100
    31.3 @@ -487,15 +487,7 @@
    31.4  
    31.5  lemma bex1_bexeq_reg:
    31.6    shows "(\<exists>!x\<in>Respects R. P x) \<longrightarrow> (Bex1_rel R (\<lambda>x. P x))"
    31.7 -  apply (simp add: Ex1_def Bex1_rel_def in_respects)
    31.8 -  apply clarify
    31.9 -  apply auto
   31.10 -  apply (rule bexI)
   31.11 -  apply assumption
   31.12 -  apply (simp add: in_respects)
   31.13 -  apply (simp add: in_respects)
   31.14 -  apply auto
   31.15 -  done
   31.16 +  by (auto simp add: Ex1_def Bex1_rel_def Bex_def Ball_def in_respects)
   31.17  
   31.18  lemma bex1_bexeq_reg_eqv:
   31.19    assumes a: "equivp R"
    32.1 --- a/src/HOL/Tools/simpdata.ML	Wed Mar 12 22:57:50 2014 +0100
    32.2 +++ b/src/HOL/Tools/simpdata.ML	Thu Mar 13 07:07:07 2014 +0100
    32.3 @@ -109,10 +109,21 @@
    32.4  fun mksimps pairs (_: Proof.context) =
    32.5    map_filter (try mk_eq) o mk_atomize pairs o gen_all;
    32.6  
    32.7 +val simp_legacy_precond =
    32.8 +  Attrib.setup_config_bool @{binding "simp_legacy_precond"} (K false)
    32.9 +
   32.10  fun unsafe_solver_tac ctxt =
   32.11 -  (fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN'
   32.12 -  FIRST' [resolve_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ctxt),
   32.13 -    atac, etac @{thm FalseE}];
   32.14 +  let
   32.15 +    val intros =
   32.16 +      if Config.get ctxt simp_legacy_precond then [] else [@{thm conjI}]
   32.17 +    val sol_thms =
   32.18 +      reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ctxt;
   32.19 +    fun sol_tac i =
   32.20 +      FIRST [resolve_tac sol_thms i, atac i , etac @{thm FalseE} i] ORELSE
   32.21 +      (match_tac intros THEN_ALL_NEW sol_tac) i
   32.22 +  in
   32.23 +    (fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN' sol_tac
   32.24 +  end;
   32.25  
   32.26  val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac;
   32.27  
    33.1 --- a/src/HOL/Word/Bool_List_Representation.thy	Wed Mar 12 22:57:50 2014 +0100
    33.2 +++ b/src/HOL/Word/Bool_List_Representation.thy	Thu Mar 13 07:07:07 2014 +0100
    33.3 @@ -941,7 +941,6 @@
    33.4    apply (subst bin_rsplit_aux.simps)
    33.5    apply (subst bin_rsplit_aux.simps)
    33.6    apply (clarsimp split: prod.split)
    33.7 -  apply auto
    33.8    done
    33.9  
   33.10  lemma bin_rsplitl_aux_append:
   33.11 @@ -950,7 +949,6 @@
   33.12    apply (subst bin_rsplitl_aux.simps)
   33.13    apply (subst bin_rsplitl_aux.simps)
   33.14    apply (clarsimp split: prod.split)
   33.15 -  apply auto
   33.16    done
   33.17  
   33.18  lemmas rsplit_aux_apps [where bs = "[]"] =
    34.1 --- a/src/HOL/ZF/HOLZF.thy	Wed Mar 12 22:57:50 2014 +0100
    34.2 +++ b/src/HOL/ZF/HOLZF.thy	Thu Mar 13 07:07:07 2014 +0100
    34.3 @@ -261,7 +261,7 @@
    34.4    apply (frule Elem_Elem_PFun[where p=y], simp)
    34.5    apply (subgoal_tac "isFun F")
    34.6    apply (simp add: isFun_def isOpair_def)  
    34.7 -  apply (auto simp add: Fst Snd, blast)
    34.8 +  apply (auto simp add: Fst Snd)
    34.9    apply (auto simp add: PFun_def Sep)
   34.10    done
   34.11