new ==> simp rule
authornipkow
Sat Apr 25 17:38:22 2015 +0200 (2015-04-25)
changeset 601476d7b7a037e8d
parent 60146 bcb680bbcd00
child 60148 f0fc2378a479
new ==> simp rule
src/HOL/Extraction.thy
src/HOL/HOL.thy
     1.1 --- a/src/HOL/Extraction.thy	Wed Apr 22 20:07:00 2015 +0200
     1.2 +++ b/src/HOL/Extraction.thy	Sat Apr 25 17:38:22 2015 +0200
     1.3 @@ -32,7 +32,7 @@
     1.4    induct_atomize induct_atomize' induct_rulify induct_rulify'
     1.5    induct_rulify_fallback induct_trueI
     1.6    True_implies_equals implies_True_equals TrueE
     1.7 -  False_implies_equals
     1.8 +  False_implies_equals implies_False_swap
     1.9  
    1.10  lemmas [extraction_expand_def] =
    1.11    HOL.induct_forall_def HOL.induct_implies_def HOL.induct_equal_def HOL.induct_conj_def
     2.1 --- a/src/HOL/HOL.thy	Wed Apr 22 20:07:00 2015 +0200
     2.2 +++ b/src/HOL/HOL.thy	Sat Apr 25 17:38:22 2015 +0200
     2.3 @@ -1270,6 +1270,10 @@
     2.4  lemma False_implies_equals: "(False \<Longrightarrow> P) \<equiv> Trueprop True"
     2.5  by default simp_all
     2.6  
     2.7 +lemma implies_False_swap:
     2.8 +  "(False \<Longrightarrow> PROP P \<Longrightarrow> PROP Q) \<equiv> (PROP P \<Longrightarrow> False \<Longrightarrow> PROP Q)"
     2.9 +by(rule swap_prems_eq)
    2.10 +
    2.11  lemma ex_simps:
    2.12    "!!P Q. (EX x. P x & Q)   = ((EX x. P x) & Q)"
    2.13    "!!P Q. (EX x. P & Q x)   = (P & (EX x. Q x))"
    2.14 @@ -1293,7 +1297,7 @@
    2.15  lemmas [simp] =
    2.16    triv_forall_equality (*prunes params*)
    2.17    True_implies_equals implies_True_equals (*prune True in asms*)
    2.18 -  False_implies_equals (*prune False in asms*)
    2.19 +  False_implies_equals implies_False_swap (*prune False in asms*)
    2.20    if_True
    2.21    if_False
    2.22    if_cancel