undid 6d7b7a037e8d because it does not help but slows simplification down by up to 5% (AODV)
authornipkow
Sat May 09 12:19:24 2015 +0200 (2015-05-09)
changeset 601834cd4c204578c
parent 60182 e1ea5a6379c9
child 60184 7541f29492c3
undid 6d7b7a037e8d because it does not help but slows simplification down by up to 5% (AODV)
src/HOL/HOL.thy
src/HOL/Hoare_Parallel/OG_Examples.thy
     1.1 --- a/src/HOL/HOL.thy	Thu May 07 15:34:28 2015 +0200
     1.2 +++ b/src/HOL/HOL.thy	Sat May 09 12:19:24 2015 +0200
     1.3 @@ -1270,6 +1270,8 @@
     1.4  lemma False_implies_equals: "(False \<Longrightarrow> P) \<equiv> Trueprop True"
     1.5  by default simp_all
     1.6  
     1.7 +(* This is not made a simp rule because it does not improve any proofs
     1.8 +   but slows some AFP entries down by 5% (cpu time). May 2015 *)
     1.9  lemma implies_False_swap: "NO_MATCH (Trueprop False) P \<Longrightarrow>
    1.10    (False \<Longrightarrow> PROP P \<Longrightarrow> PROP Q) \<equiv> (PROP P \<Longrightarrow> False \<Longrightarrow> PROP Q)"
    1.11  by(rule swap_prems_eq)
    1.12 @@ -1297,7 +1299,7 @@
    1.13  lemmas [simp] =
    1.14    triv_forall_equality (*prunes params*)
    1.15    True_implies_equals implies_True_equals (*prune True in asms*)
    1.16 -  False_implies_equals implies_False_swap (*prune False in asms*)
    1.17 +  False_implies_equals (*prune False in asms*)
    1.18    if_True
    1.19    if_False
    1.20    if_cancel
     2.1 --- a/src/HOL/Hoare_Parallel/OG_Examples.thy	Thu May 07 15:34:28 2015 +0200
     2.2 +++ b/src/HOL/Hoare_Parallel/OG_Examples.thy	Sat May 09 12:19:24 2015 +0200
     2.3 @@ -169,7 +169,7 @@
     2.4  apply oghoare
     2.5  --\<open>35 vc\<close>
     2.6  apply simp_all
     2.7 ---\<open>21 vc\<close>
     2.8 +--\<open>16 vc\<close>
     2.9  apply(tactic \<open>ALLGOALS (clarify_tac @{context})\<close>)
    2.10  --\<open>11 vc\<close>
    2.11  apply simp_all
    2.12 @@ -433,14 +433,14 @@
    2.13  apply(tactic \<open>ALLGOALS (clarify_tac @{context})\<close>)
    2.14  --\<open>112 subgoals left\<close>
    2.15  apply(simp_all (no_asm))
    2.16 ---\<open>97 subgoals left\<close>
    2.17 +--\<open>43 subgoals left\<close>
    2.18  apply(tactic \<open>ALLGOALS (conjI_Tac (K all_tac))\<close>)
    2.19 ---\<open>930 subgoals left\<close>
    2.20 +--\<open>419 subgoals left\<close>
    2.21  apply(tactic \<open>ALLGOALS (clarify_tac @{context})\<close>)
    2.22  --\<open>99 subgoals left\<close>
    2.23 -apply(simp_all (*asm_lr*) only:length_0_conv [THEN sym])
    2.24 +apply(simp_all only:length_0_conv [THEN sym])
    2.25  --\<open>20 subgoals left\<close>
    2.26 -apply (simp_all (*asm_lr*) del:length_0_conv length_greater_0_conv add: nth_list_update mod_lemma)
    2.27 +apply (simp_all del:length_0_conv length_greater_0_conv add: nth_list_update mod_lemma)
    2.28  --\<open>9 subgoals left\<close>
    2.29  apply (force simp add:less_Suc_eq)
    2.30  apply(hypsubst_thin, drule sym)