560 section {* Context Parser (TBD) *} |
560 section {* Context Parser (TBD) *} |
561 |
561 |
562 text {* |
562 text {* |
563 Used for example in \isacommand{attribute\_setup} and \isacommand{method\_setup}. |
563 Used for example in \isacommand{attribute\_setup} and \isacommand{method\_setup}. |
564 *} |
564 *} |
|
565 |
|
566 section {* Argument and Attribute Parsers (TBD) *} |
565 |
567 |
566 section {* Parsing Inner Syntax *} |
568 section {* Parsing Inner Syntax *} |
567 |
569 |
568 text {* |
570 text {* |
569 There is usually no need to write your own parser for parsing inner syntax, that is |
571 There is usually no need to write your own parser for parsing inner syntax, that is |
720 \end{readmore} |
722 \end{readmore} |
721 *} |
723 *} |
722 |
724 |
723 text_raw {* |
725 text_raw {* |
724 \begin{exercise} |
726 \begin{exercise} |
725 If you look closely how @{ML SpecParse.where_alt_specs} is implemented |
727 Have a look at how the parser @{ML SpecParse.where_alt_specs} is implemented |
726 in file @{ML_file "Pure/Isar/spec_parse.ML"} and compare it to our @{ML "spec_parser"}, |
728 in file @{ML_file "Pure/Isar/spec_parse.ML"}. This parser corresponds |
727 you can notice an additional ``tail'' (Lines 8 to 10): |
729 to the ``where-part'' of the introduction rules given above. Below |
|
730 we paraphrase the code of @{ML SpecParse.where_alt_specs} adapted to our |
|
731 purposes. |
728 \begin{isabelle} |
732 \begin{isabelle} |
729 *} |
733 *} |
730 ML %linenosgray{*val spec_parser' = |
734 ML %linenosgray{*val spec_parser' = |
731 OuterParse.fixes -- |
735 OuterParse.fixes -- |
732 Scan.optional |
736 Scan.optional |
737 Scan.option (Scan.ahead (OuterParse.name || |
741 Scan.option (Scan.ahead (OuterParse.name || |
738 OuterParse.$$$ "[") -- |
742 OuterParse.$$$ "[") -- |
739 OuterParse.!!! (OuterParse.$$$ "|"))))) [] *} |
743 OuterParse.!!! (OuterParse.$$$ "|"))))) [] *} |
740 text_raw {* |
744 text_raw {* |
741 \end{isabelle} |
745 \end{isabelle} |
742 What is the purpose of this additional ``tail''? |
746 Both parsers accept the same input, but if you look closely, you can notice |
|
747 an additional ``tail'' (Lines 8 to 10) in @{ML spec_parser'}. What is the purpose of |
|
748 this additional ``tail''? |
743 \end{exercise} |
749 \end{exercise} |
744 *} |
750 *} |
745 |
751 |
746 section {* New Commands and Keyword Files\label{sec:newcommand} *} |
752 section {* New Commands and Keyword Files\label{sec:newcommand} *} |
747 |
753 |
748 text {* |
754 text {* |
749 (FIXME: update to the right command setup) |
755 (FIXME: update to the right command setup --- is this still needed) |
750 |
756 |
751 Often new commands, for example for providing new definitional principles, |
757 Often new commands, for example for providing new definitional principles, |
752 need to be implemented. While this is not difficult on the ML-level, |
758 need to be implemented. While this is not difficult on the ML-level, |
753 new commands, in order to be useful, need to be recognised by |
759 new commands, in order to be useful, need to be recognised by |
754 ProofGeneral. This results in some subtle configuration issues, which we |
760 ProofGeneral. This results in some subtle configuration issues, which we |
1003 *} |
1009 *} |
1004 |
1010 |
1005 section {* Methods *} |
1011 section {* Methods *} |
1006 |
1012 |
1007 text {* |
1013 text {* |
1008 Methods are a central concept in Isabelle. They are the ones you use for example |
1014 (FIXME: maybe move to after the tactic section) |
|
1015 |
|
1016 Methods are a central to Isabelle. They are the ones you use for example |
1009 in \isacommand{apply}. To print out all currently known methods you can use the |
1017 in \isacommand{apply}. To print out all currently known methods you can use the |
1010 Isabelle command: |
1018 Isabelle command: |
1011 *} |
1019 |
1012 |
1020 \begin{isabelle} |
1013 print_methods |
1021 \isacommand{print\_methods}\\ |
1014 |
1022 @{text "> methods:"}\\ |
1015 text {* |
1023 @{text "> -: do nothing (insert current facts only)"}\\ |
|
1024 @{text "> HOL.default: apply some intro/elim rule (potentially classical)"}\\ |
|
1025 @{text "> ..."} |
|
1026 \end{isabelle} |
|
1027 |
1016 An example of a very simple method is: |
1028 An example of a very simple method is: |
1017 *} |
1029 *} |
1018 |
1030 |
1019 method_setup %gray foobar_meth = |
1031 method_setup %gray foobar_meth = |
1020 {* Scan.succeed |
1032 {* Scan.succeed |
1021 (K (SIMPLE_METHOD ((etac @{thm conjE} THEN' rtac @{thm conjI}) 1))) *} |
1033 (K (SIMPLE_METHOD ((etac @{thm conjE} THEN' rtac @{thm conjI}) 1))) *} |
1022 "foobar method" |
1034 "foobar method for conjE and conjI" |
1023 |
1035 |
1024 text {* |
1036 text {* |
1025 It defines the method @{text foobar_meth}, which takes no arguments (therefore the |
1037 It defines the method @{text foobar_meth}, which takes no arguments (therefore the |
1026 parser @{ML Scan.succeed}) and |
1038 parser @{ML Scan.succeed}) and only applies a single tactic, namely the tactic which |
1027 only applies the tactic @{thm [source] conjE} and then @{thm [source] conjI}. |
1039 applies @{thm [source] conjE} and then @{thm [source] conjI}. The function @{ML SIMPLE_METHOD} |
1028 This method can be used in the following proof |
1040 turns such a tactic into a method. @{text "Foobar_meth"} can be used as follows |
1029 *} |
1041 *} |
1030 |
1042 |
1031 lemma shows "A \<and> B \<Longrightarrow> C \<and> D" |
1043 lemma shows "A \<and> B \<Longrightarrow> C \<and> D" |
1032 apply(foobar_meth) |
1044 apply(foobar_meth) |
1033 txt {* |
1045 txt {* |