644 \"| evenS[intro]: \\\"odd n \<Longrightarrow> even (Suc n)\\\" \" ^ |
643 \"| evenS[intro]: \\\"odd n \<Longrightarrow> even (Suc n)\\\" \" ^ |
645 \"| oddS[intro]: \\\"even n \<Longrightarrow> odd (Suc n)\\\"\") |
644 \"| oddS[intro]: \\\"even n \<Longrightarrow> odd (Suc n)\\\"\") |
646 in |
645 in |
647 parse spec_parser input |
646 parse spec_parser input |
648 end" |
647 end" |
649 "(((NONE, [(even, NONE, NoSyn), (odd, NONE, NoSyn)]), |
648 "(([(even, NONE, NoSyn), (odd, NONE, NoSyn)], |
650 [((even0,\<dots>), \"\\^E\\^Ftoken\\^Eeven 0\\^E\\^F\\^E\"), |
649 [((even0,\<dots>), \"\\^E\\^Ftoken\\^Eeven 0\\^E\\^F\\^E\"), |
651 ((evenS,\<dots>), \"\\^E\\^Ftoken\\^Eodd n \<Longrightarrow> even (Suc n)\\^E\\^F\\^E\"), |
650 ((evenS,\<dots>), \"\\^E\\^Ftoken\\^Eodd n \<Longrightarrow> even (Suc n)\\^E\\^F\\^E\"), |
652 ((oddS,\<dots>), \"\\^E\\^Ftoken\\^Eeven n \<Longrightarrow> odd (Suc n)\\^E\\^F\\^E\")]), [])"} |
651 ((oddS,\<dots>), \"\\^E\\^Ftoken\\^Eeven n \<Longrightarrow> odd (Suc n)\\^E\\^F\\^E\")]), [])"} |
653 |
652 |
654 As you see, the result is a ``nested'' four-tuple consisting of an optional |
653 As you see, the result is a pair consisting of a list of |
655 locale (in this case @{ML NONE}); a list of variables with optional |
654 variables with optional type-annotation and syntax-annotation, and a list of |
656 type-annotation and syntax-annotation; and a list of rules where every rule |
655 rules where every rule has optionally a name and an attribute. |
657 has optionally a name and an attribute. |
656 |
658 |
657 The function @{ML OuterParse.fixes} in Line 2 of the parser reads an |
659 |
658 \isacommand{and}-separated |
660 In Line 2 of the parser, the function @{ML OuterParse.opt_target} reads a target |
|
661 in order to indicate a locale in which the specification is made. For example |
|
662 |
|
663 @{ML_response [display,gray] |
|
664 "parse OuterParse.opt_target (filtered_input \"(in test)\")" "(SOME \"test\",[])"} |
|
665 |
|
666 returns the locale @{text [quotes] "test"}; if no target is given, like in the |
|
667 case of @{text "even"} and @{text "odd"}, the function returns @{ML NONE}. |
|
668 |
|
669 The function @{ML OuterParse.fixes} in Line 3 reads an \isacommand{and}-separated |
|
670 list of variables that can include optional type annotations and syntax translations. |
659 list of variables that can include optional type annotations and syntax translations. |
671 For example:\footnote{Note that in the code we need to write |
660 For example:\footnote{Note that in the code we need to write |
672 @{text "\\\"int \<Rightarrow> bool\\\""} in order to properly escape the double quotes |
661 @{text "\\\"int \<Rightarrow> bool\\\""} in order to properly escape the double quotes |
673 in the compound type.} |
662 in the compound type.} |
674 |
663 |
694 |
683 |
695 \begin{readmore} |
684 \begin{readmore} |
696 The datastructre for sytax annotations is defined in @{ML_file "Pure/Syntax/mixfix.ML"}. |
685 The datastructre for sytax annotations is defined in @{ML_file "Pure/Syntax/mixfix.ML"}. |
697 \end{readmore} |
686 \end{readmore} |
698 |
687 |
699 Lines 4 to 8 in the function @{ML spec_parser} implement the parser for a |
688 Lines 3 to 7 in the function @{ML spec_parser} implement the parser for a |
700 list of introduction rules, that is propositions with theorem |
689 list of introduction rules, that is propositions with theorem |
701 annotations. The introduction rules are propositions parsed by @{ML |
690 annotations. The introduction rules are propositions parsed by @{ML |
702 OuterParse.prop}. However, they can include an optional theorem name plus |
691 OuterParse.prop}. However, they can include an optional theorem name plus |
703 some attributes. For example |
692 some attributes. For example |
704 |
693 |
710 end" "(foo_lemma, [((\"intro\", []), \<dots>), ((\"dest\", [\<dots>]), \<dots>)])"} |
699 end" "(foo_lemma, [((\"intro\", []), \<dots>), ((\"dest\", [\<dots>]), \<dots>)])"} |
711 |
700 |
712 The function @{ML opt_thm_name in SpecParse} is the ``optional'' variant of |
701 The function @{ML opt_thm_name in SpecParse} is the ``optional'' variant of |
713 @{ML thm_name in SpecParse}. Theorem names can contain attributes. The name |
702 @{ML thm_name in SpecParse}. Theorem names can contain attributes. The name |
714 has to end with @{text [quotes] ":"}---see the argument of |
703 has to end with @{text [quotes] ":"}---see the argument of |
715 the function @{ML SpecParse.opt_thm_name} in Line 8. |
704 the function @{ML SpecParse.opt_thm_name} in Line 7. |
716 |
705 |
717 \begin{readmore} |
706 \begin{readmore} |
718 Attributes and arguments are implemented in the files @{ML_file "Pure/Isar/attrib.ML"} |
707 Attributes and arguments are implemented in the files @{ML_file "Pure/Isar/attrib.ML"} |
719 and @{ML_file "Pure/Isar/args.ML"}. |
708 and @{ML_file "Pure/Isar/args.ML"}. |
720 \end{readmore} |
709 \end{readmore} |
914 and then ``open up'' a proof in order to prove the proposition (for example |
903 and then ``open up'' a proof in order to prove the proposition (for example |
915 \isacommand{lemma}) or prove some other properties (for example |
904 \isacommand{lemma}) or prove some other properties (for example |
916 \isacommand{function}). To achieve this kind of behaviour, you have to use the kind |
905 \isacommand{function}). To achieve this kind of behaviour, you have to use the kind |
917 indicator @{ML thy_goal in OuterKeyword}. Note, however, once you change the |
906 indicator @{ML thy_goal in OuterKeyword}. Note, however, once you change the |
918 ``kind'' of a command from @{ML thy_decl in OuterKeyword} to @{ML thy_goal in OuterKeyword} |
907 ``kind'' of a command from @{ML thy_decl in OuterKeyword} to @{ML thy_goal in OuterKeyword} |
919 then the keyword file needs to be re-created. |
908 then the keyword file needs to be re-created! |
920 |
909 |
921 Below we change \isacommand{foobar} so that it takes a proposition as |
910 Below we change \isacommand{foobar} so that it takes a proposition as |
922 argument and then starts a proof in order to prove it. Therefore in Line 13, |
911 argument and then starts a proof in order to prove it. Therefore in Line 13, |
923 we set the kind indicator to @{ML thy_goal in OuterKeyword}. |
912 we set the kind indicator to @{ML thy_goal in OuterKeyword}. |
924 *} |
913 *} |
996 {* Scan.succeed |
985 {* Scan.succeed |
997 (K (SIMPLE_METHOD ((etac @{thm conjE} THEN' rtac @{thm conjI}) 1))) *} |
986 (K (SIMPLE_METHOD ((etac @{thm conjE} THEN' rtac @{thm conjI}) 1))) *} |
998 "foobar method" |
987 "foobar method" |
999 |
988 |
1000 text {* |
989 text {* |
1001 It defines the method @{text foobar_meth} which takes no arguments and |
990 It defines the method @{text foobar_meth}, which takes no arguments (therefore the |
|
991 parser @{ML Scan.succeed}) and |
1002 only applies the tactic @{thm [source] conjE} and then @{thm [source] conjI}. |
992 only applies the tactic @{thm [source] conjE} and then @{thm [source] conjI}. |
1003 It can be applied in the following proof |
993 This method can be used in the following proof |
1004 *} |
994 *} |
1005 |
995 |
1006 lemma shows "A \<and> B \<Longrightarrow> C \<and> D" |
996 lemma shows "A \<and> B \<Longrightarrow> C \<and> D" |
1007 apply(foobar_meth) |
997 apply(foobar_meth) |
1008 txt {* |
998 txt {* |