1767 this, we build the theorem @{term "True \<equiv> True"} (Line 1) and then |
1767 this, we build the theorem @{term "True \<equiv> True"} (Line 1) and then |
1768 unfold the constant @{term "True"} according to its definition (Line 2). |
1768 unfold the constant @{term "True"} according to its definition (Line 2). |
1769 |
1769 |
1770 @{ML_response_fake [display,gray,linenos] |
1770 @{ML_response_fake [display,gray,linenos] |
1771 "Thm.reflexive @{cterm \"True\"} |
1771 "Thm.reflexive @{cterm \"True\"} |
1772 |> Simplifier.rewrite_rule [@{thm True_def}] |
1772 |> Simplifier.rewrite_rule @{context} [@{thm True_def}] |
1773 |> pretty_thm @{context} |
1773 |> pretty_thm @{context} |
1774 |> pwriteln" |
1774 |> pwriteln" |
1775 "(\<lambda>x. x) = (\<lambda>x. x) \<equiv> (\<lambda>x. x) = (\<lambda>x. x)"} |
1775 "(\<lambda>x. x) = (\<lambda>x. x) \<equiv> (\<lambda>x. x) = (\<lambda>x. x)"} |
1776 |
1776 |
1777 Often it is necessary to transform theorems to and from the object |
1777 Often it is necessary to transform theorems to and from the object |
1783 some build in functions which help with these transformations. The function |
1783 some build in functions which help with these transformations. The function |
1784 @{ML_ind rulify in Object_Logic} |
1784 @{ML_ind rulify in Object_Logic} |
1785 replaces all object connectives by equivalents in the meta logic. For example |
1785 replaces all object connectives by equivalents in the meta logic. For example |
1786 |
1786 |
1787 @{ML_response_fake [display, gray] |
1787 @{ML_response_fake [display, gray] |
1788 "Object_Logic.rulify @{thm foo_test2}" |
1788 "Object_Logic.rulify @{context} @{thm foo_test2}" |
1789 "\<lbrakk>?A; ?B\<rbrakk> \<Longrightarrow> ?C"} |
1789 "\<lbrakk>?A; ?B\<rbrakk> \<Longrightarrow> ?C"} |
1790 |
1790 |
1791 The transformation in the other direction can be achieved with function |
1791 The transformation in the other direction can be achieved with function |
1792 @{ML_ind atomize in Object_Logic} and the following code. |
1792 @{ML_ind atomize in Object_Logic} and the following code. |
1793 |
1793 |
1794 @{ML_response_fake [display,gray] |
1794 @{ML_response_fake [display,gray] |
1795 "let |
1795 "let |
1796 val thm = @{thm foo_test1} |
1796 val thm = @{thm foo_test1} |
1797 val meta_eq = Object_Logic.atomize (cprop_of thm) |
1797 val meta_eq = Object_Logic.atomize @{context} (cprop_of thm) |
1798 in |
1798 in |
1799 Raw_Simplifier.rewrite_rule [meta_eq] thm |
1799 Raw_Simplifier.rewrite_rule @{context} [meta_eq] thm |
1800 end" |
1800 end" |
1801 "?A \<longrightarrow> ?B \<longrightarrow> ?C"} |
1801 "?A \<longrightarrow> ?B \<longrightarrow> ?C"} |
1802 |
1802 |
1803 In this code the function @{ML atomize in Object_Logic} produces |
1803 In this code the function @{ML atomize in Object_Logic} produces |
1804 a meta-equation between the given theorem and the theorem transformed |
1804 a meta-equation between the given theorem and the theorem transformed |
1813 @{text "?list"}. For this we can use the function |
1813 @{text "?list"}. For this we can use the function |
1814 @{ML_ind forall_intr_vars in Drule}. This allows us to implement the |
1814 @{ML_ind forall_intr_vars in Drule}. This allows us to implement the |
1815 following function for atomizing a theorem. |
1815 following function for atomizing a theorem. |
1816 *} |
1816 *} |
1817 |
1817 |
1818 ML %grayML{*fun atomize_thm thm = |
1818 ML %grayML{*fun atomize_thm ctxt thm = |
1819 let |
1819 let |
1820 val thm' = forall_intr_vars thm |
1820 val thm' = forall_intr_vars thm |
1821 val thm'' = Object_Logic.atomize (cprop_of thm') |
1821 val thm'' = Object_Logic.atomize ctxt (cprop_of thm') |
1822 in |
1822 in |
1823 Raw_Simplifier.rewrite_rule [thm''] thm' |
1823 Raw_Simplifier.rewrite_rule ctxt [thm''] thm' |
1824 end*} |
1824 end*} |
1825 |
1825 |
1826 text {* |
1826 text {* |
1827 This function produces for the theorem @{thm [source] list.induct} |
1827 This function produces for the theorem @{thm [source] list.induct} |
1828 |
1828 |
1829 @{ML_response_fake [display, gray] |
1829 @{ML_response_fake [display, gray] |
1830 "atomize_thm @{thm list.induct}" |
1830 "atomize_thm @{context} @{thm list.induct}" |
1831 "\<forall>P list. P [] \<longrightarrow> (\<forall>a list. P list \<longrightarrow> P (a # list)) \<longrightarrow> P list"} |
1831 "\<forall>P list. P [] \<longrightarrow> (\<forall>a list. P list \<longrightarrow> P (a # list)) \<longrightarrow> P list"} |
1832 |
1832 |
1833 Theorems can also be produced from terms by giving an explicit proof. |
1833 Theorems can also be produced from terms by giving an explicit proof. |
1834 One way to achieve this is by using the function @{ML_ind prove in Goal} |
1834 One way to achieve this is by using the function @{ML_ind prove in Goal} |
1835 in the structure @{ML_struct Goal}. For example below we use this function |
1835 in the structure @{ML_struct Goal}. For example below we use this function |