765 text {* |
766 text {* |
766 If we print out the value of @{ML my_thm} then we see only the |
767 If we print out the value of @{ML my_thm} then we see only the |
767 final statement of the theorem. |
768 final statement of the theorem. |
768 |
769 |
769 @{ML_response_fake [display, gray] |
770 @{ML_response_fake [display, gray] |
770 "string_of_thm @{context} my_thm |
771 "string_of_thm @{context} my_thm |> tracing" |
771 |> tracing" |
|
772 "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"} |
772 "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"} |
773 |
773 |
774 However, internally the code-snippet constructs the following |
774 However, internally the code-snippet constructs the following |
775 proof. |
775 proof. |
776 |
776 |
785 } |
785 } |
786 } |
786 } |
787 } |
787 } |
788 \] |
788 \] |
789 |
789 |
790 While we obtained a theorem as result, this theorem is not |
790 While we obtained a theorem as the result, this theorem is not |
791 yet stored in Isabelle's theorem database. So it cannot be referenced later |
791 yet stored in Isabelle's theorem database. Consequently, it cannot be |
792 on. One way to store it is |
792 referenced later on. One way to store it in the theorem database is |
793 *} |
793 by using the function @{ML_ind note in LocalTheory}. |
794 |
794 *} |
795 local_setup %gray{* |
795 |
|
796 local_setup %gray {* |
796 LocalTheory.note Thm.theoremK |
797 LocalTheory.note Thm.theoremK |
797 ((@{binding "my_thm"}, []), [my_thm]) #> snd *} |
798 ((@{binding "my_thm"}, []), [my_thm]) #> snd *} |
798 |
799 |
799 text {* |
800 text {* |
800 Now it can be referenced with the \isacommand{thm}-command on the user-level |
801 Now it can be referenced with the \isacommand{thm}-command on the user-level |
804 \isacommand{thm}~@{text "my_thm"}\isanewline |
805 \isacommand{thm}~@{text "my_thm"}\isanewline |
805 @{text ">"}~@{prop "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"} |
806 @{text ">"}~@{prop "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"} |
806 \end{isabelle} |
807 \end{isabelle} |
807 |
808 |
808 or with the @{text "@{thm \<dots>}"}-antiquotation on the ML-level. Note that the |
809 or with the @{text "@{thm \<dots>}"}-antiquotation on the ML-level. Note that the |
809 theorem does not have the meta-variables that would be present if we stated |
810 theorem does not have any meta-variables that would be present if we proved |
810 this theorem on the user-level. |
811 this theorem on the user-level. As we shall see later on, we have to provide |
811 |
812 this information explicitly. |
|
813 |
|
814 There is a multitude of functions that manage or manipulate theorems. For example |
|
815 we can test theorems for (alpha) equality. Suppose you proved the following three |
|
816 facts. |
|
817 *} |
|
818 |
|
819 lemma |
|
820 shows thm1: "\<forall>x. P x" |
|
821 and thm2: "\<forall>y. P y" |
|
822 and thm3: "\<forall>y. Q y" sorry |
|
823 |
|
824 text {* |
|
825 Testing for equality using the function @{ML_ind eq_thm in Thm} produces: |
|
826 |
|
827 @{ML_response [display,gray] |
|
828 "(Thm.eq_thm (@{thm thm1}, @{thm thm2}), |
|
829 Thm.eq_thm (@{thm thm2}, @{thm thm3}))" |
|
830 "(true, false)"} |
|
831 |
|
832 Many functions destruct a theorem into a @{ML_type cterm}. For example |
|
833 @{ML_ind lhs_of in Thm} and @{ML_ind rhs_of in Thm} return the left and |
|
834 righ-hand side, respectively, of a meta-equality. |
|
835 |
|
836 @{ML_response_fake [display,gray] |
|
837 "let |
|
838 val eq = @{thm True_def} |
|
839 in |
|
840 (Thm.lhs_of eq, Thm.rhs_of eq) |
|
841 |> pairself (tracing o string_of_cterm @{context}) |
|
842 end" |
|
843 "True |
|
844 (\<lambda>x. x) = (\<lambda>x. x)"} |
|
845 |
|
846 Other function produce immediately a term that can be pattern-matched. |
|
847 Suppose the following theorem. |
|
848 *} |
|
849 |
|
850 lemma foo_test: |
|
851 shows "A \<Longrightarrow> B \<Longrightarrow> C" sorry |
|
852 |
|
853 text {* |
|
854 @{ML_response_fake [display,gray] |
|
855 "let |
|
856 val thm = @{thm foo_test} |
|
857 in |
|
858 (Thm.prems_of thm, [Thm.concl_of thm]) |
|
859 |> pairself (tracing o string_of_terms @{context}) |
|
860 end" |
|
861 "?A, ?B |
|
862 ?C"} |
812 |
863 |
813 \begin{readmore} |
864 \begin{readmore} |
814 For the functions @{text "assume"}, @{text "forall_elim"} etc |
865 For the functions @{text "assume"}, @{text "forall_elim"} etc |
815 see \isccite{sec:thms}. The basic functions for theorems are defined in |
866 see \isccite{sec:thms}. The basic functions for theorems are defined in |
816 @{ML_file "Pure/thm.ML"}, @{ML_file "Pure/more_thm.ML"} and @{ML_file "Pure/drule.ML"}. |
867 @{ML_file "Pure/thm.ML"}, @{ML_file "Pure/more_thm.ML"} and @{ML_file "Pure/drule.ML"}. |