# HG changeset patch
# User haftmann
# Date 1591284622 0
# Node ID 2e7df6774373015ced80571b5faee7b0ad67f2e5
# Parent  4e0a58818edc72b7cb6444e182d8ba31ca1b0329
more rules for FOL also

diff -r 4e0a58818edc -r 2e7df6774373 src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Thu Jun 04 15:30:22 2020 +0000
+++ b/src/FOL/FOL.thy	Thu Jun 04 15:30:22 2020 +0000
@@ -344,7 +344,7 @@
 (*intuitionistic simprules only*)
 val IFOL_ss =
   put_simpset FOL_basic_ss \<^context>
-  addsimps @{thms meta_simps IFOL_simps int_ex_simps int_all_simps}
+  addsimps @{thms meta_simps IFOL_simps int_ex_simps int_all_simps subst_all subst_all'}
   addsimprocs [\<^simproc>\<open>defined_All\<close>, \<^simproc>\<open>defined_Ex\<close>]
   |> Simplifier.add_cong @{thm imp_cong}
   |> simpset_of;
diff -r 4e0a58818edc -r 2e7df6774373 src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Thu Jun 04 15:30:22 2020 +0000
+++ b/src/FOL/IFOL.thy	Thu Jun 04 15:30:22 2020 +0000
@@ -827,6 +827,36 @@
   \<open>(P \<or> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> R) \<and> (Q \<longrightarrow> R)\<close>
   by iprover+
 
+lemma subst_all:
+  \<open>(\<And>x. x = a \<Longrightarrow> PROP P(x)) \<equiv> PROP P(a)\<close>
+proof (rule equal_intr_rule)
+  assume *: \<open>\<And>x. x = a \<Longrightarrow> PROP P(x)\<close>
+  show \<open>PROP P(a)\<close>
+    by (rule *) (rule refl)
+next
+  fix x
+  assume \<open>PROP P(a)\<close> and \<open>x = a\<close>
+  from \<open>x = a\<close> have \<open>x \<equiv> a\<close>
+    by (rule eq_reflection)
+  with \<open>PROP P(a)\<close> show \<open>PROP P(x)\<close>
+    by simp
+qed
+
+lemma subst_all':
+  \<open>(\<And>x. a = x \<Longrightarrow> PROP P(x)) \<equiv> PROP P(a)\<close>
+proof (rule equal_intr_rule)
+  assume *: \<open>\<And>x. a = x \<Longrightarrow> PROP P(x)\<close>
+  show \<open>PROP P(a)\<close>
+    by (rule *) (rule refl)
+next
+  fix x
+  assume \<open>PROP P(a)\<close> and \<open>a = x\<close>
+  from \<open>a = x\<close> have \<open>a \<equiv> x\<close>
+    by (rule eq_reflection)
+  with \<open>PROP P(a)\<close> show \<open>PROP P(x)\<close>
+    by simp
+qed
+
 
 subsubsection \<open>Conversion into rewrite rules\<close>