# HG changeset patch
# User Manuel Eberl <eberlm@in.tum.de>
# Date 1589380536 -7200
# Node ID db120661dded6c70353251cc30a14d2dbe422227
# Parent  f4626b1f1b9689e1bd9531be7fd45587c10473bf
new HOL simproc: eliminate_false_implies

diff -r f4626b1f1b96 -r db120661dded src/HOL/Analysis/Abstract_Topology_2.thy
--- a/src/HOL/Analysis/Abstract_Topology_2.thy	Thu May 14 23:44:01 2020 +0200
+++ b/src/HOL/Analysis/Abstract_Topology_2.thy	Wed May 13 16:35:36 2020 +0200
@@ -1400,7 +1400,7 @@
    "\<lbrakk>connected_component_of X x y; connected_component_of X y z\<rbrakk>
         \<Longrightarrow> connected_component_of X x z"
   unfolding connected_component_of_def
-  using connectedin_Un by fastforce
+  using connectedin_Un by blast
 
 lemma connected_component_of_mono:
    "\<lbrakk>connected_component_of (subtopology X S) x y; S \<subseteq> T\<rbrakk>
diff -r f4626b1f1b96 -r db120661dded src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu May 14 23:44:01 2020 +0200
+++ b/src/HOL/HOL.thy	Wed May 13 16:35:36 2020 +0200
@@ -1294,13 +1294,32 @@
 lemma False_implies_equals: "(False \<Longrightarrow> P) \<equiv> Trueprop True"
   by standard simp_all
 
-(* This is not made a simp rule because it does not improve any proofs
-   but slows some AFP entries down by 5% (cpu time). May 2015 *)
+(* It seems that making this a simp rule is slower than using the simproc below *)
 lemma implies_False_swap:
-  "NO_MATCH (Trueprop False) P \<Longrightarrow>
-    (False \<Longrightarrow> PROP P \<Longrightarrow> PROP Q) \<equiv> (PROP P \<Longrightarrow> False \<Longrightarrow> PROP Q)"
+  "(False \<Longrightarrow> PROP P \<Longrightarrow> PROP Q) \<equiv> (PROP P \<Longrightarrow> False \<Longrightarrow> PROP Q)"
   by (rule swap_prems_eq)
 
+ML \<open>
+fun eliminate_false_implies ct =
+  let
+    val (prems, concl) = Logic.strip_horn (Thm.term_of ct)
+    fun go n =
+      if n > 1 then
+        Conv.rewr_conv @{thm Pure.swap_prems_eq}
+        then_conv Conv.arg_conv (go (n - 1))
+        then_conv Conv.rewr_conv @{thm HOL.implies_True_equals}
+      else
+        Conv.rewr_conv @{thm HOL.False_implies_equals}
+  in
+    case concl of
+      Const (@{const_name HOL.Trueprop}, _) $ _ => SOME (go (length prems) ct)
+    | _ => NONE
+  end
+\<close>
+
+simproc_setup eliminate_false_implies ("False \<Longrightarrow> PROP P") = \<open>K (K eliminate_false_implies)\<close>
+
+
 lemma ex_simps:
   "\<And>P Q. (\<exists>x. P x \<and> Q)   = ((\<exists>x. P x) \<and> Q)"
   "\<And>P Q. (\<exists>x. P \<and> Q x)   = (P \<and> (\<exists>x. Q x))"