799 |
799 |
800 text {* |
800 text {* |
801 The first argument @{ML_ind theoremK in Thm} is a kind indicator, which |
801 The first argument @{ML_ind theoremK in Thm} is a kind indicator, which |
802 classifies the theorem. For a theorem arising from a definition we should |
802 classifies the theorem. For a theorem arising from a definition we should |
803 state @{ML_ind definitionK in Thm}, instead. The second argument is the |
803 state @{ML_ind definitionK in Thm}, instead. The second argument is the |
804 name under which we stroe the theorem or theorems. The third contains is |
804 name under which we store the theorem or theorems. The third can contain |
805 a list of (theorem) attributes. Above it is empty, but if we want to store |
805 a list of (theorem) attributes. Above it is empty, but if we want to store |
806 the therem and at the same time add it to the simpset we have to declare. |
806 the theorem and at the same time add it to the simpset we have to declare: |
807 *} |
807 *} |
808 |
808 |
809 local_setup %gray {* |
809 local_setup %gray {* |
810 LocalTheory.note Thm.theoremK |
810 LocalTheory.note Thm.theoremK |
811 ((@{binding "my_thm_simp"}, [Attrib.internal (K Simplifier.simp_add)]), [my_thm]) #> snd *} |
811 ((@{binding "my_thm_simp"}, |
812 |
812 [Attrib.internal (K Simplifier.simp_add)]), |
813 |
813 [my_thm]) #> snd *} |
814 |
814 |
815 text {* |
815 text {* |
816 Now @{thm [source] my_thm} can be referenced with the \isacommand{thm}-command |
816 Note that we have to use another name for the theorem, since Isabelle does |
817 on the user-level of Isabelle |
817 not allow to add another theorem under the same name. The attribute can be |
|
818 given @{ML_ind internal in Attrib}. If we use the function @{ML |
|
819 get_thm_names_from_ss} from the previous chapter, we can check whether the |
|
820 theorem has been added. |
|
821 |
|
822 @{ML_response [display,gray] |
|
823 "let |
|
824 fun pred s = match_string \"my_thm_simp\" s |
|
825 in |
|
826 exists pred (get_thm_names_from_ss @{simpset}) |
|
827 end" |
|
828 "true"} |
|
829 |
|
830 Now the theorems @{thm [source] my_thm} and @{thm [source] my_thm_simp} can |
|
831 also be referenced with the \isacommand{thm}-command on the user-level of |
|
832 Isabelle |
818 |
833 |
819 \begin{isabelle} |
834 \begin{isabelle} |
820 \isacommand{thm}~@{text "my_thm"}\isanewline |
835 \isacommand{thm}~@{text "my_thm"}\isanewline |
821 @{text ">"}~@{prop "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"} |
836 @{text ">"}~@{prop "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"} |
822 \end{isabelle} |
837 \end{isabelle} |
823 |
838 |
824 or with the @{text "@{thm \<dots>}"}-antiquotation on the ML-level. Note that the |
839 or with the @{text "@{thm \<dots>}"}-antiquotation on the ML-level. Note that the |
825 theorem does not have any meta-variables that would be present if we proved |
840 theorem does not have any meta-variables that would be present if we proved |
826 this theorem on the user-level. As we shall see later on, we have to provide |
841 this theorem on the user-level. As we shall see later on, we have to construct |
827 this information explicitly. |
842 meta-variables explicitly. |
828 |
843 |
829 There is a multitude of functions that manage or manipulate theorems. For example |
844 There is a multitude of functions that manage or manipulate theorems. For example |
830 we can test theorems for (alpha) equality. Suppose you proved the following three |
845 we can test theorems for (alpha) equality. Suppose you proved the following three |
831 facts. |
846 facts. |
832 *} |
847 *} |
842 @{ML_response [display,gray] |
857 @{ML_response [display,gray] |
843 "(Thm.eq_thm (@{thm thm1}, @{thm thm2}), |
858 "(Thm.eq_thm (@{thm thm1}, @{thm thm2}), |
844 Thm.eq_thm (@{thm thm2}, @{thm thm3}))" |
859 Thm.eq_thm (@{thm thm2}, @{thm thm3}))" |
845 "(true, false)"} |
860 "(true, false)"} |
846 |
861 |
847 Many functions destruct a theorem into a @{ML_type cterm}. For example |
862 Many functions destruct theorems into @{ML_type cterm}s. For example |
848 @{ML_ind lhs_of in Thm} and @{ML_ind rhs_of in Thm} return the left and |
863 the functions @{ML_ind lhs_of in Thm} and @{ML_ind rhs_of in Thm} return |
849 righ-hand side, respectively, of a meta-equality. |
864 the left and right-hand side, respectively, of a meta-equality. |
850 |
865 |
851 @{ML_response_fake [display,gray] |
866 @{ML_response_fake [display,gray] |
852 "let |
867 "let |
853 val eq = @{thm True_def} |
868 val eq = @{thm True_def} |
854 in |
869 in |
856 |> pairself (tracing o string_of_cterm @{context}) |
871 |> pairself (tracing o string_of_cterm @{context}) |
857 end" |
872 end" |
858 "True |
873 "True |
859 (\<lambda>x. x) = (\<lambda>x. x)"} |
874 (\<lambda>x. x) = (\<lambda>x. x)"} |
860 |
875 |
861 Other function produce immediately a term that can be pattern-matched. |
876 Other function produce terms that can be pattern-matched. |
862 Suppose the following theorem. |
877 Suppose the following theorem. |
863 *} |
878 *} |
864 |
879 |
865 lemma foo_test: |
880 lemma foo_test: |
866 shows "A \<Longrightarrow> B \<Longrightarrow> C" sorry |
881 shows "A \<Longrightarrow> B \<Longrightarrow> C" sorry |
867 |
882 |
868 text {* |
883 text {* |
|
884 We can deconstruct it into premises and conclusion. |
|
885 |
869 @{ML_response_fake [display,gray] |
886 @{ML_response_fake [display,gray] |
870 "let |
887 "let |
871 val thm = @{thm foo_test} |
888 val thm = @{thm foo_test} |
872 in |
889 in |
873 (Thm.prems_of thm, [Thm.concl_of thm]) |
890 (Thm.prems_of thm, [Thm.concl_of thm]) |
879 \begin{readmore} |
896 \begin{readmore} |
880 For the functions @{text "assume"}, @{text "forall_elim"} etc |
897 For the functions @{text "assume"}, @{text "forall_elim"} etc |
881 see \isccite{sec:thms}. The basic functions for theorems are defined in |
898 see \isccite{sec:thms}. The basic functions for theorems are defined in |
882 @{ML_file "Pure/thm.ML"}, @{ML_file "Pure/more_thm.ML"} and @{ML_file "Pure/drule.ML"}. |
899 @{ML_file "Pure/thm.ML"}, @{ML_file "Pure/more_thm.ML"} and @{ML_file "Pure/drule.ML"}. |
883 \end{readmore} |
900 \end{readmore} |
|
901 |
|
902 TBD below. |
884 |
903 |
885 (FIXME: handy functions working on theorems, like @{ML_ind rulify in ObjectLogic} and so on) |
904 (FIXME: handy functions working on theorems, like @{ML_ind rulify in ObjectLogic} and so on) |
886 |
905 |
887 (FIXME: @{ML_ind prove in Goal}) |
906 (FIXME: @{ML_ind prove in Goal}) |
888 |
907 |