827 \<open>(P \<or> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> R) \<and> (Q \<longrightarrow> R)\<close> |
827 \<open>(P \<or> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> R) \<and> (Q \<longrightarrow> R)\<close> |
828 by iprover+ |
828 by iprover+ |
829 |
829 |
830 lemma subst_all: |
830 lemma subst_all: |
831 \<open>(\<And>x. x = a \<Longrightarrow> PROP P(x)) \<equiv> PROP P(a)\<close> |
831 \<open>(\<And>x. x = a \<Longrightarrow> PROP P(x)) \<equiv> PROP P(a)\<close> |
832 proof (rule equal_intr_rule) |
|
833 assume *: \<open>\<And>x. x = a \<Longrightarrow> PROP P(x)\<close> |
|
834 show \<open>PROP P(a)\<close> |
|
835 by (rule *) (rule refl) |
|
836 next |
|
837 fix x |
|
838 assume \<open>PROP P(a)\<close> and \<open>x = a\<close> |
|
839 from \<open>x = a\<close> have \<open>x \<equiv> a\<close> |
|
840 by (rule eq_reflection) |
|
841 with \<open>PROP P(a)\<close> show \<open>PROP P(x)\<close> |
|
842 by simp |
|
843 qed |
|
844 |
|
845 lemma subst_all': |
|
846 \<open>(\<And>x. a = x \<Longrightarrow> PROP P(x)) \<equiv> PROP P(a)\<close> |
832 \<open>(\<And>x. a = x \<Longrightarrow> PROP P(x)) \<equiv> PROP P(a)\<close> |
847 proof (rule equal_intr_rule) |
833 proof - |
848 assume *: \<open>\<And>x. a = x \<Longrightarrow> PROP P(x)\<close> |
834 show \<open>(\<And>x. x = a \<Longrightarrow> PROP P(x)) \<equiv> PROP P(a)\<close> |
849 show \<open>PROP P(a)\<close> |
835 proof (rule equal_intr_rule) |
850 by (rule *) (rule refl) |
836 assume *: \<open>\<And>x. x = a \<Longrightarrow> PROP P(x)\<close> |
851 next |
837 show \<open>PROP P(a)\<close> |
852 fix x |
838 by (rule *) (rule refl) |
853 assume \<open>PROP P(a)\<close> and \<open>a = x\<close> |
839 next |
854 from \<open>a = x\<close> have \<open>a \<equiv> x\<close> |
840 fix x |
855 by (rule eq_reflection) |
841 assume \<open>PROP P(a)\<close> and \<open>x = a\<close> |
856 with \<open>PROP P(a)\<close> show \<open>PROP P(x)\<close> |
842 from \<open>x = a\<close> have \<open>x \<equiv> a\<close> |
857 by simp |
843 by (rule eq_reflection) |
|
844 with \<open>PROP P(a)\<close> show \<open>PROP P(x)\<close> |
|
845 by simp |
|
846 qed |
|
847 show \<open>(\<And>x. a = x \<Longrightarrow> PROP P(x)) \<equiv> PROP P(a)\<close> |
|
848 proof (rule equal_intr_rule) |
|
849 assume *: \<open>\<And>x. a = x \<Longrightarrow> PROP P(x)\<close> |
|
850 show \<open>PROP P(a)\<close> |
|
851 by (rule *) (rule refl) |
|
852 next |
|
853 fix x |
|
854 assume \<open>PROP P(a)\<close> and \<open>a = x\<close> |
|
855 from \<open>a = x\<close> have \<open>a \<equiv> x\<close> |
|
856 by (rule eq_reflection) |
|
857 with \<open>PROP P(a)\<close> show \<open>PROP P(x)\<close> |
|
858 by simp |
|
859 qed |
858 qed |
860 qed |
859 |
861 |
860 |
862 |
861 subsubsection \<open>Conversion into rewrite rules\<close> |
863 subsubsection \<open>Conversion into rewrite rules\<close> |
862 |
864 |