888 |
888 |
889 section {* Theorem Attributes *} |
889 section {* Theorem Attributes *} |
890 |
890 |
891 text {* |
891 text {* |
892 Theorem attributes are @{text "[simp]"}, @{text "[OF \<dots>]"}, @{text |
892 Theorem attributes are @{text "[simp]"}, @{text "[OF \<dots>]"}, @{text |
893 "[symmetric]"} and so on. Such attributes are \emph{neither} tags \emph{or} flags |
893 "[symmetric]"} and so on. Such attributes are \emph{neither} tags \emph{nor} flags |
894 annotated to theorems, but functions that do further processing once the |
894 annotated to theorems, but functions that do further processing once a |
895 theorems are proven. In particular, it is not possible to find out |
895 theorem is proven. In particular, it is not possible to find out |
896 what are all theorems that have an given attribute in common, unless of course |
896 what are all theorems that have a given attribute in common, unless of course |
897 the function behind the attribute stores the theorems in a retrivable |
897 the function behind the attribute stores the theorems in a retrivable |
898 datastructure. This can be easily done by the recipe described in |
898 datastructure. This can be easily done by the recipe described in |
899 \ref{rec:named}. |
899 \ref{rec:named}. |
900 |
900 |
901 If you want to print out all currently known attributes a theorem |
901 If you want to print out all currently known attributes a theorem |
905 "COMP: direct composition with rules (no lifting) |
905 "COMP: direct composition with rules (no lifting) |
906 HOL.dest: declaration of Classical destruction rule |
906 HOL.dest: declaration of Classical destruction rule |
907 HOL.elim: declaration of Classical elimination rule |
907 HOL.elim: declaration of Classical elimination rule |
908 \<dots>"} |
908 \<dots>"} |
909 |
909 |
|
910 To explain how to write your own attribute, let us start with an extremely simple |
|
911 version of the attribute @{text "[symmetric]"}. The purpose of this attribute is |
|
912 to produce the ``symmetric'' version of an equation. The main function behind |
|
913 this attribute is |
910 *} |
914 *} |
911 |
915 |
912 ML{*val my_symmetric = Thm.rule_attribute (fn _ => fn thm => thm RS @{thm sym})*} |
916 ML{*val my_symmetric = Thm.rule_attribute (fn _ => fn thm => thm RS @{thm sym})*} |
913 |
917 |
914 text {* |
918 text {* |
915 the setup |
919 where the function @{ML "Thm.rule_attribute"} expects a function taking a |
|
920 context (we ignore it in the code above) and a theorem (@{text thm}) and |
|
921 returns another theorem (namely @{text thm} resolved with the rule |
|
922 @{thm sym[no_vars]}). The function @{ML "Thm.rule_attribute"} then returns |
|
923 an attribute (of type @{ML_type "attribute"}). |
|
924 |
|
925 Before we can use the attribute, we need to set it up. This can be done |
|
926 using the function @{ML Attrib.add_attributes} as follows. |
916 *} |
927 *} |
917 |
928 |
918 setup {* |
929 setup {* |
919 Attrib.add_attributes |
930 Attrib.add_attributes |
920 [("my_sym", Attrib.no_args my_symmetric, "applying the sym rule")] |
931 [("my_sym", Attrib.no_args my_symmetric, "applying the sym rule")] |
921 *} |
932 *} |
922 |
933 |
923 lemma test: "1 = Suc 0" by simp |
934 text {* |
924 |
935 The attribute does not expect any further arguments (like @{text "[OF \<dots>]"} that |
925 text {* |
936 can take a list of theorems as argument). Therefore we use the function |
926 @{thm test[my_sym]} |
937 @{ML Attrib.no_args}. Later on we will also consider attributes taking further |
|
938 arguments. An example for the attribute @{text "[my_sym]"} is the proof |
|
939 *} |
|
940 |
|
941 lemma test[my_sym]: "2 = Suc (Suc 0)" by simp |
|
942 |
|
943 text {* |
|
944 which stores the theorem @{thm test} under the name @{thm [source] test}. We |
|
945 can also use the attribute when referring to this theorem. |
|
946 |
|
947 \begin{isabelle} |
|
948 \isacommand{thm}~@{text "test[my_sym]"}\\ |
|
949 @{text "> "}~@{thm test[my_sym]} |
|
950 \end{isabelle} |
|
951 |
927 *} |
952 *} |
928 |
953 |
929 text {* |
954 text {* |
930 What are: |
955 What are: |
931 |
956 |
932 @{text "rule_attribute"} |
|
933 |
957 |
934 @{text "declaration_attribute"} |
958 @{text "declaration_attribute"} |
935 |
959 |
936 @{text "theory_attributes"} |
960 @{text "theory_attributes"} |
937 |
961 |