src/HOL/HOL.thy
changeset 60183 4cd4c204578c
parent 60169 5ef8ed685965
child 60758 d8d85a8172b5
equal deleted inserted replaced
60182:e1ea5a6379c9 60183:4cd4c204578c
  1268 by default (intro TrueI)
  1268 by default (intro TrueI)
  1269 
  1269 
  1270 lemma False_implies_equals: "(False \<Longrightarrow> P) \<equiv> Trueprop True"
  1270 lemma False_implies_equals: "(False \<Longrightarrow> P) \<equiv> Trueprop True"
  1271 by default simp_all
  1271 by default simp_all
  1272 
  1272 
       
  1273 (* This is not made a simp rule because it does not improve any proofs
       
  1274    but slows some AFP entries down by 5% (cpu time). May 2015 *)
  1273 lemma implies_False_swap: "NO_MATCH (Trueprop False) P \<Longrightarrow>
  1275 lemma implies_False_swap: "NO_MATCH (Trueprop False) P \<Longrightarrow>
  1274   (False \<Longrightarrow> PROP P \<Longrightarrow> PROP Q) \<equiv> (PROP P \<Longrightarrow> False \<Longrightarrow> PROP Q)"
  1276   (False \<Longrightarrow> PROP P \<Longrightarrow> PROP Q) \<equiv> (PROP P \<Longrightarrow> False \<Longrightarrow> PROP Q)"
  1275 by(rule swap_prems_eq)
  1277 by(rule swap_prems_eq)
  1276 
  1278 
  1277 lemma ex_simps:
  1279 lemma ex_simps:
  1295   by (iprover | blast)+
  1297   by (iprover | blast)+
  1296 
  1298 
  1297 lemmas [simp] =
  1299 lemmas [simp] =
  1298   triv_forall_equality (*prunes params*)
  1300   triv_forall_equality (*prunes params*)
  1299   True_implies_equals implies_True_equals (*prune True in asms*)
  1301   True_implies_equals implies_True_equals (*prune True in asms*)
  1300   False_implies_equals implies_False_swap (*prune False in asms*)
  1302   False_implies_equals (*prune False in asms*)
  1301   if_True
  1303   if_True
  1302   if_False
  1304   if_False
  1303   if_cancel
  1305   if_cancel
  1304   if_eq_cancel
  1306   if_eq_cancel
  1305   imp_disjL
  1307   imp_disjL