equal
deleted
inserted
replaced
375 \emph{not} replaced with code that will look up the current theory in |
375 \emph{not} replaced with code that will look up the current theory in |
376 some data structure and return it. Instead, it is literally |
376 some data structure and return it. Instead, it is literally |
377 replaced with the value representing the theory name. |
377 replaced with the value representing the theory name. |
378 |
378 |
379 In a similar way you can use antiquotations to refer to proved theorems: |
379 In a similar way you can use antiquotations to refer to proved theorems: |
380 for a single theorem |
380 @{text "@{thm \<dots>}"} for a single theorem |
381 |
381 |
382 @{ML_response_fake [display,gray] "@{thm allI}" "(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x"} |
382 @{ML_response_fake [display,gray] "@{thm allI}" "(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x"} |
383 |
383 |
384 and for more than one |
384 and @{text "@{thms \<dots>}"} for more than one |
385 |
385 |
386 @{ML_response_fake [display,gray] "@{thms conj_ac}" |
386 @{ML_response_fake [display,gray] "@{thms conj_ac}" |
387 "(?P \<and> ?Q) = (?Q \<and> ?P) |
387 "(?P \<and> ?Q) = (?Q \<and> ?P) |
388 (?P \<and> ?Q \<and> ?R) = (?Q \<and> ?P \<and> ?R) |
388 (?P \<and> ?Q \<and> ?R) = (?Q \<and> ?P \<and> ?R) |
389 ((?P \<and> ?Q) \<and> ?R) = (?P \<and> ?Q \<and> ?R)"} |
389 ((?P \<and> ?Q) \<and> ?R) = (?P \<and> ?Q \<and> ?R)"} |
883 \end{readmore} |
883 \end{readmore} |
884 |
884 |
885 (FIXME: how to add case-names to goal states - maybe in the next section) |
885 (FIXME: how to add case-names to goal states - maybe in the next section) |
886 *} |
886 *} |
887 |
887 |
888 |
|
889 section {* Theorem Attributes *} |
888 section {* Theorem Attributes *} |
890 |
889 |
891 text {* |
890 text {* |
892 |
891 Theorem attributes are @{text "[simp]"}, @{text "[OF \<dots>]"}, @{text |
|
892 "[symmetric]"} and so on. Such attributes are \emph{neither} tags \emph{or} flags |
|
893 annotated to theorems, but functions that do further processing once the |
|
894 theorems are proven. In particular, it is not possible to find out |
|
895 what are all theorems that have an given attribute in common, unless of course |
|
896 the function behind the attribute stores the theorems in a retrivable |
|
897 datastructure. This can be easily done by the recipe described in |
|
898 \ref{rec:named}. |
893 |
899 |
894 If you want to print out all currently known attributes a theorem |
900 If you want to print out all currently known attributes a theorem |
895 can have, you can use the function: |
901 can have, you can use the function: |
896 |
902 |
897 @{ML_response_fake [display,gray] "Attrib.print_attributes @{theory}" |
903 @{ML_response_fake [display,gray] "Attrib.print_attributes @{theory}" |
900 HOL.elim: declaration of Classical elimination rule |
906 HOL.elim: declaration of Classical elimination rule |
901 \<dots>"} |
907 \<dots>"} |
902 |
908 |
903 *} |
909 *} |
904 |
910 |
|
911 ML{*val my_symmetric = Thm.rule_attribute (fn _ => fn thm => thm RS @{thm sym})*} |
|
912 |
|
913 text {* |
|
914 the setup |
|
915 *} |
|
916 |
|
917 setup {* |
|
918 Attrib.add_attributes |
|
919 [("my_sym", Attrib.no_args my_symmetric, "applying the sym rule")] |
|
920 *} |
|
921 |
|
922 lemma test: "1 = Suc 0" by simp |
|
923 |
|
924 text {* |
|
925 @{thm test[my_sym]} |
|
926 *} |
|
927 |
|
928 text {* |
|
929 What are: |
|
930 |
|
931 @{text "rule_attribute"} |
|
932 |
|
933 @{text "declaration_attribute"} |
|
934 |
|
935 @{text "theory_attributes"} |
|
936 |
|
937 @{text "proof_attributes"} |
|
938 |
|
939 |
|
940 \begin{readmore} |
|
941 FIXME: @{ML_file "Pure/more_thm.ML"} @{ML_file "Pure/Isar/attrib.ML"} |
|
942 \end{readmore} |
|
943 |
|
944 |
|
945 *} |
|
946 |
905 |
947 |
906 section {* Theories and Local Theories *} |
948 section {* Theories and Local Theories *} |
907 |
949 |
908 text {* |
950 text {* |
909 (FIXME: expand) |
951 (FIXME: expand) |
|
952 |
|
953 (FIXME: explain \isacommand{setup}) |
910 |
954 |
911 There are theories, proof contexts and local theories (in this order, if you |
955 There are theories, proof contexts and local theories (in this order, if you |
912 want to order them). |
956 want to order them). |
913 |
957 |
914 In contrast to an ordinary theory, which simply consists of a type |
958 In contrast to an ordinary theory, which simply consists of a type |