872 end" |
872 end" |
873 "True |
873 "True |
874 (\<lambda>x. x) = (\<lambda>x. x)"} |
874 (\<lambda>x. x) = (\<lambda>x. x)"} |
875 |
875 |
876 Other function produce terms that can be pattern-matched. |
876 Other function produce terms that can be pattern-matched. |
877 Suppose the following theorem. |
877 Suppose the following two theorems. |
878 *} |
878 *} |
879 |
879 |
880 lemma foo_test: |
880 lemma |
881 shows "A \<Longrightarrow> B \<Longrightarrow> C" sorry |
881 shows foo_test1: "A \<Longrightarrow> B \<Longrightarrow> C" |
882 |
882 and foo_test2: "A \<longrightarrow> B \<longrightarrow> C" sorry |
883 text {* |
883 |
884 We can deconstruct it into premises and conclusion. |
884 text {* |
|
885 We can deconstruct them into premises and conclusions as follows. |
885 |
886 |
886 @{ML_response_fake [display,gray] |
887 @{ML_response_fake [display,gray] |
887 "let |
888 "let |
888 val thm = @{thm foo_test} |
889 val ctxt = @{context} |
889 in |
890 fun prems_and_concl thm = |
890 (Thm.prems_of thm, [Thm.concl_of thm]) |
891 [\"Premises: \" ^ |
891 |> pairself (tracing o string_of_terms @{context}) |
892 (string_of_terms ctxt (Thm.prems_of thm))] @ |
892 end" |
893 [\"Conclusion: \" ^ |
893 "?A, ?B |
894 (string_of_term ctxt (Thm.concl_of thm))] |
894 ?C"} |
895 |> cat_lines |
|
896 |> tracing |
|
897 in |
|
898 prems_and_concl @{thm foo_test1}; |
|
899 prems_and_concl @{thm foo_test2} |
|
900 end" |
|
901 "Premises: ?A, ?B |
|
902 Conclusion: ?C |
|
903 Premises: |
|
904 Conclusion: ?A \<longrightarrow> ?B \<longrightarrow> ?C"} |
|
905 |
|
906 Note that in the second case, there is no premise. |
895 |
907 |
896 \begin{readmore} |
908 \begin{readmore} |
897 For the functions @{text "assume"}, @{text "forall_elim"} etc |
909 For the functions @{text "assume"}, @{text "forall_elim"} etc |
898 see \isccite{sec:thms}. The basic functions for theorems are defined in |
910 see \isccite{sec:thms}. The basic functions for theorems are defined in |
899 @{ML_file "Pure/thm.ML"}, @{ML_file "Pure/more_thm.ML"} and @{ML_file "Pure/drule.ML"}. |
911 @{ML_file "Pure/thm.ML"}, @{ML_file "Pure/more_thm.ML"} and @{ML_file "Pure/drule.ML"}. |
900 \end{readmore} |
912 \end{readmore} |
901 |
913 |
|
914 |
|
915 Often it is necessary to transform theorems to and from the object |
|
916 logic. For example, the function @{ML_ind rulify in ObjectLogic} |
|
917 replaces all @{text "\<longrightarrow>"} and @{text "\<forall>"} into the equivalents of the |
|
918 meta logic. For example |
|
919 |
|
920 @{ML_response_fake [display, gray] |
|
921 "ObjectLogic.rulify @{thm foo_test2}" |
|
922 "\<lbrakk>?A; ?B\<rbrakk> \<Longrightarrow> ?C"} |
|
923 |
|
924 The transformation in the other direction can be achieved with function |
|
925 @{ML_ind atomize in ObjectLogic} and the following code. |
|
926 |
|
927 @{ML_response_fake [display,gray] |
|
928 "let |
|
929 val thm = @{thm foo_test1} |
|
930 val meta_eq = ObjectLogic.atomize (cprop_of thm) |
|
931 in |
|
932 MetaSimplifier.rewrite_rule [meta_eq] thm |
|
933 end" |
|
934 "?A \<longrightarrow> ?B \<longrightarrow> ?C"} |
|
935 |
|
936 In this code the function @{ML atomize in ObjectLogic} produces |
|
937 a meta-equation between the given theorem and the theorem transformed |
|
938 into the object logic. The function @{ML_ind rewrite_rule in MetaSimplifier} |
|
939 unfolds this meta-equation in the given theorem. The result is |
|
940 the theorem with object logic connectives. |
|
941 x |
|
942 Theorems can also be produced from terms by giving an explicit proof. |
|
943 One way to achive this is by using the function @{ML_ind prove in Goal}. |
|
944 For example |
|
945 |
|
946 @{ML_response_fake [display,gray] |
|
947 "let |
|
948 val trm = @{term \"P \<Longrightarrow> P::bool\"} |
|
949 val tac = K (atac 1) |
|
950 in |
|
951 Goal.prove @{context} [\"P\"] [] trm tac |
|
952 end" |
|
953 "?P \<Longrightarrow> ?P"} |
|
954 |
|
955 This function takes as second argument a list of strings. This list specifies |
|
956 which variables should be turned into meta-variables once the term is proved. |
|
957 The proof is given in form of a tactic. We explain tactics in |
|
958 Chapter~\ref{chp:tactical}. |
|
959 |
|
960 Theorems also contain auxiliary data, such their names and kind, but also |
|
961 names for cases etc. This data is stored in a string-string list and can |
|
962 be retrieved with the function @{ML_ind get_tags in Thm}. Assume the |
|
963 following lemma. |
|
964 *} |
|
965 |
|
966 lemma foo_data: "P \<Longrightarrow> P" by assumption |
|
967 |
|
968 text {* |
|
969 The auxiliary data of this lemma is as follows. |
|
970 |
|
971 @{ML_response_fake [display,gray] |
|
972 "Thm.get_tags @{thm foo_data}" |
|
973 " [(\"name\", \"FirstSteps.foo_data\"), (\"kind\", \"lemma\")]"} |
|
974 *} |
|
975 |
|
976 |
|
977 local_setup {* |
|
978 LocalTheory.note Thm.theoremK |
|
979 ((@{binding "rr2"}, []), [(RuleCases.name ["a"] @{thm foo_data})]) #> snd *} |
|
980 |
|
981 ML {* Thm.get_tags @{thm rr2} *} |
|
982 |
|
983 lemma |
|
984 "Q \<Longrightarrow> Q" |
|
985 proof (induct rule: rr2) |
|
986 oops |
|
987 |
|
988 text {* |
902 TBD below. |
989 TBD below. |
903 |
990 |
904 (FIXME: handy functions working on theorems, like @{ML_ind rulify in ObjectLogic} and so on) |
|
905 |
|
906 (FIXME: @{ML_ind prove in Goal}) |
|
907 |
991 |
908 (FIXME: how to add case-names to goal states - maybe in the |
992 (FIXME: how to add case-names to goal states - maybe in the |
909 next section) |
993 next section) |
910 |
994 |
911 (FIXME: example for how to add theorem styles) |
995 (FIXME: example for how to add theorem styles) |