more rules for FOL also

--- 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;

--- 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>