832 LocalTheory.note Thm.theoremK |
832 LocalTheory.note Thm.theoremK |
833 ((@{binding "my_thm"}, []), [my_thm]) #> snd *} |
833 ((@{binding "my_thm"}, []), [my_thm]) #> snd *} |
834 |
834 |
835 text {* |
835 text {* |
836 The fourth argument of @{ML note in LocalTheory} is the list of theorems we |
836 The fourth argument of @{ML note in LocalTheory} is the list of theorems we |
837 want to store under a name. The first argument @{ML_ind theoremK in Thm} is |
837 want to store under a name. We can store more than one under a single name. |
|
838 The first argument @{ML_ind theoremK in Thm} is |
838 a kind indicator, which classifies the theorem. There are several such kind |
839 a kind indicator, which classifies the theorem. There are several such kind |
839 indicators: for a theorem arising from a definition you should use @{ML_ind |
840 indicators: for a theorem arising from a definition you should use @{ML_ind |
840 definitionK in Thm}, for an axiom @{ML_ind axiomK in Thm}, and for |
841 definitionK in Thm}, for an axiom @{ML_ind axiomK in Thm}, and for |
841 ``normal'' theorems the kinds @{ML_ind theoremK in Thm} or @{ML_ind lemmaK |
842 ``normal'' theorems the kinds @{ML_ind theoremK in Thm} or @{ML_ind lemmaK |
842 in Thm}. The second argument of @{ML note in LocalTheory} is the name under |
843 in Thm}. The second argument of @{ML note in LocalTheory} is the name under |
843 which we store the theorem or theorems. The third argument can contain a |
844 which we store the theorem or theorems. The third argument can contain a |
844 list of theorem attributes, which we will explain in detail in |
845 list of theorem attributes, which we will explain in detail in |
845 Section~\ref{sec:attributes}. Below we just use one such attribute in order |
846 Section~\ref{sec:attributes}. Below we just use one such attribute for |
846 add the theorem to the simpset: |
847 adding the theorem to the simpset: |
847 *} |
848 *} |
848 |
849 |
849 local_setup %gray {* |
850 local_setup %gray {* |
850 LocalTheory.note Thm.theoremK |
851 LocalTheory.note Thm.theoremK |
851 ((@{binding "my_thm_simp"}, |
852 ((@{binding "my_thm_simp"}, |
877 \begin{isabelle} |
878 \begin{isabelle} |
878 \isacommand{thm}~@{text "my_thm"}\isanewline |
879 \isacommand{thm}~@{text "my_thm"}\isanewline |
879 @{text ">"}~@{prop "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"} |
880 @{text ">"}~@{prop "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"} |
880 \end{isabelle} |
881 \end{isabelle} |
881 |
882 |
882 or with the @{text "@{thm \<dots>}"}-antiquotation on the ML-level. As can be seen, |
883 or with the @{text "@{thm \<dots>}"}-antiquotation on the ML-level. Otherwise the |
883 the theorem does not have any meta-variables that would be present if we proved |
884 user has no access to these theorems. |
884 this theorem on the user-level. We will see later on that we have to |
885 |
885 construct meta-variables in theorems explicitly. |
886 Recall that Isabelle does not let you call @{ML note in LocalTheory} twice |
886 |
887 with the same theorem name. In effect, once a theorem is stored under a name, |
887 \footnote{\bf FIXME say something about @{ML_ind add_thms_dynamic in PureThy}} |
888 this association will be fixed. While this is a ``safety-net'' to make sure a |
888 *} |
889 theorem name refers to a particular theorem or collection of theorems, it is |
889 |
890 also a bit too restrictive in cases where a theorem name should refer to a |
890 text {* |
891 dynamically expanding list of theorems (like a simpset). Therefore Isabelle |
|
892 also implements a mechanism where a theorem name can refer to a custom theorem |
|
893 list. For this you can use the function @{ML_ind add_thms_dynamic in PureThy}. |
|
894 To see how it works let us assume we defined our own theorem list maintained |
|
895 in the data storage @{text MyThmList}. |
|
896 *} |
|
897 |
|
898 ML{*structure MyThmList = GenericDataFun |
|
899 (type T = thm list |
|
900 val empty = [] |
|
901 val extend = I |
|
902 val merge = K (op @) |
|
903 ) |
|
904 |
|
905 fun update thm = Context.theory_map (MyThmList.map (fn thms => thm::thms))*} |
|
906 |
|
907 text {* |
|
908 The function @{ML update} allows us to update the theorem list, for example |
|
909 by adding the theorem @{thm [source] TrueI}. |
|
910 *} |
|
911 |
|
912 setup %gray {* update @{thm TrueI} *} |
|
913 |
|
914 text {* |
|
915 We can now install the theorem list so that it is visible to the user and |
|
916 can be refered to by a theorem name. For this need to call |
|
917 @{ML_ind add_thms_dynamic in PureThy} |
|
918 *} |
|
919 |
|
920 setup %gray {* |
|
921 PureThy.add_thms_dynamic (@{binding "mythmlist"}, MyThmList.get) |
|
922 *} |
|
923 |
|
924 text {* |
|
925 with a name and a function that accesses the theorem list. Now if the |
|
926 user issues the command |
|
927 |
|
928 \begin{isabelle} |
|
929 \isacommand{thm}~@{text "mythmlist"}\\ |
|
930 @{text "> True"} |
|
931 \end{isabelle} |
|
932 |
|
933 the current content of the theorem list is displayed. If more theorems are stored in |
|
934 the list, say |
|
935 *} |
|
936 |
|
937 setup %gray {* update @{thm FalseE} *} |
|
938 |
|
939 text {* |
|
940 then the same command produces |
|
941 |
|
942 \begin{isabelle} |
|
943 \isacommand{thm}~@{text "mythmlist"}\\ |
|
944 @{text "> False \<Longrightarrow> ?P"}\\ |
|
945 @{text "> True"} |
|
946 \end{isabelle} |
|
947 |
891 There is a multitude of functions that manage or manipulate theorems in the |
948 There is a multitude of functions that manage or manipulate theorems in the |
892 structures @{ML_struct Thm} and @{ML_struct Drule}. For example |
949 structures @{ML_struct Thm} and @{ML_struct Drule}. For example |
893 we can test theorems for alpha equality. Suppose you proved the following three |
950 we can test theorems for alpha equality. Suppose you proved the following three |
894 theorems. |
951 theorems. |
895 *} |
952 *} |
1081 "Thm.get_tags @{thm foo_data'}" |
1138 "Thm.get_tags @{thm foo_data'}" |
1082 "[(\"name\", \"General.foo_data'\"), (\"kind\", \"lemma\"), |
1139 "[(\"name\", \"General.foo_data'\"), (\"kind\", \"lemma\"), |
1083 (\"case_names\", \"foo_case_one;foo_case_two\")]"} |
1140 (\"case_names\", \"foo_case_one;foo_case_two\")]"} |
1084 |
1141 |
1085 You can observe the case names of this lemma on the user level when using |
1142 You can observe the case names of this lemma on the user level when using |
1086 the proof methods @{ML_text cases} and @{ML_text induct}. In the proof below |
1143 the proof methods @{text cases} and @{text induct}. In the proof below |
1087 *} |
1144 *} |
1088 |
1145 |
1089 lemma |
1146 lemma |
1090 shows "Q \<Longrightarrow> Q \<Longrightarrow> Q" |
1147 shows "Q \<Longrightarrow> Q \<Longrightarrow> Q" |
1091 proof (cases rule: foo_data') |
1148 proof (cases rule: foo_data') |
1204 in |
1261 in |
1205 Term_Style.setup "my_strip_allq2" (parser >> action) |
1262 Term_Style.setup "my_strip_allq2" (parser >> action) |
1206 end *} |
1263 end *} |
1207 |
1264 |
1208 text {* |
1265 text {* |
1209 The parser reads a list of names. In the function @{ML_text action} we first |
1266 The parser reads a list of names. In the function @{text action} we first |
1210 call @{ML rename_allq} with the parsed list, then we call @{ML strip_allq} |
1267 call @{ML rename_allq} with the parsed list, then we call @{ML strip_allq} |
1211 on the resulting term. We can now suggest, for example, two variables for |
1268 on the resulting term. We can now suggest, for example, two variables for |
1212 stripping off the first two @{text \<forall>}-quantifiers. |
1269 stripping off the first two @{text \<forall>}-quantifiers. |
1213 |
1270 |
1214 |
1271 |