equal
deleted
inserted
replaced
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 |