611 where |
611 where |
612 even0: "even 0" |
612 even0: "even 0" |
613 | evenS: "odd n \<Longrightarrow> even (Suc n)" |
613 | evenS: "odd n \<Longrightarrow> even (Suc n)" |
614 | oddS: "even n \<Longrightarrow> odd (Suc n)" |
614 | oddS: "even n \<Longrightarrow> odd (Suc n)" |
615 |
615 |
616 text {* and *} |
|
617 |
|
618 simple_inductive |
|
619 trcl\<iota> for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
|
620 where |
|
621 base: "trcl\<iota> R x x" |
|
622 | step: "trcl\<iota> R x y \<Longrightarrow> R y z \<Longrightarrow> trcl\<iota> R x z" |
|
623 |
|
624 text {* |
616 text {* |
625 For this we are going to use the parser: |
617 For this we are going to use the parser: |
626 *} |
618 *} |
627 |
619 |
628 ML %linenosgray{*val spec_parser = |
620 ML %linenosgray{*val spec_parser = |
629 OuterParse.opt_target -- |
621 OuterParse.opt_target -- |
630 OuterParse.fixes -- |
622 OuterParse.fixes -- |
631 OuterParse.for_fixes -- |
|
632 Scan.optional |
623 Scan.optional |
633 (OuterParse.$$$ "where" |-- |
624 (OuterParse.$$$ "where" |-- |
634 OuterParse.!!! |
625 OuterParse.!!! |
635 (OuterParse.enum1 "|" |
626 (OuterParse.enum1 "|" |
636 (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*} |
627 (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*} |
653 \"| evenS[intro]: \\\"odd n \<Longrightarrow> even (Suc n)\\\" \" ^ |
644 \"| evenS[intro]: \\\"odd n \<Longrightarrow> even (Suc n)\\\" \" ^ |
654 \"| oddS[intro]: \\\"even n \<Longrightarrow> odd (Suc n)\\\"\") |
645 \"| oddS[intro]: \\\"even n \<Longrightarrow> odd (Suc n)\\\"\") |
655 in |
646 in |
656 parse spec_parser input |
647 parse spec_parser input |
657 end" |
648 end" |
658 "((((NONE, [(even, NONE, NoSyn), (odd, NONE, NoSyn)]), []), |
649 "(((NONE, [(even, NONE, NoSyn), (odd, NONE, NoSyn)]), |
659 [((even0,\<dots>), \"\\^E\\^Ftoken\\^Eeven 0\\^E\\^F\\^E\"), |
650 [((even0,\<dots>), \"\\^E\\^Ftoken\\^Eeven 0\\^E\\^F\\^E\"), |
660 ((evenS,\<dots>), \"\\^E\\^Ftoken\\^Eodd n \<Longrightarrow> even (Suc n)\\^E\\^F\\^E\"), |
651 ((evenS,\<dots>), \"\\^E\\^Ftoken\\^Eodd n \<Longrightarrow> even (Suc n)\\^E\\^F\\^E\"), |
661 ((oddS,\<dots>), \"\\^E\\^Ftoken\\^Eeven n \<Longrightarrow> odd (Suc n)\\^E\\^F\\^E\")]), [])"} |
652 ((oddS,\<dots>), \"\\^E\\^Ftoken\\^Eeven n \<Longrightarrow> odd (Suc n)\\^E\\^F\\^E\")]), [])"} |
662 |
653 |
663 As you see, the result is a ``nested'' four-tuple consisting of an |
654 As you see, the result is a ``nested'' four-tuple consisting of an optional |
664 optional locale (in this case @{ML NONE}); a list of variables with optional |
655 locale (in this case @{ML NONE}); a list of variables with optional |
665 type-annotation and syntax-annotation; a list of for-fixes (fixed variables; in this |
656 type-annotation and syntax-annotation; and a list of rules where every rule |
666 case there are none); and a list of rules where every rule has optionally a name and |
657 has optionally a name and an attribute. |
667 an attribute. |
658 |
668 |
659 |
669 In Line 2 of the parser, the function @{ML OuterParse.opt_target} reads a target |
660 In Line 2 of the parser, the function @{ML OuterParse.opt_target} reads a target |
670 in order to indicate a locale in which the specification is made. For example |
661 in order to indicate a locale in which the specification is made. For example |
671 |
662 |
672 @{ML_response [display,gray] |
663 @{ML_response [display,gray] |
703 |
694 |
704 \begin{readmore} |
695 \begin{readmore} |
705 The datastructre for sytax annotations is defined in @{ML_file "Pure/Syntax/mixfix.ML"}. |
696 The datastructre for sytax annotations is defined in @{ML_file "Pure/Syntax/mixfix.ML"}. |
706 \end{readmore} |
697 \end{readmore} |
707 |
698 |
708 Similarly, the function @{ML OuterParse.for_fixes} in Line 4: it reads the |
699 Lines 4 to 8 in the function @{ML spec_parser} implement the parser for a |
709 same \isacommand{and}-separated list of variables as @{ML "fixes" in OuterParse}, |
|
710 but requires that this list is prefixed by the keyword \isacommand{for}. |
|
711 |
|
712 @{ML_response [display,gray] |
|
713 "parse OuterParse.for_fixes (filtered_input \"for foo and bar and blink\")" |
|
714 "([(foo, NONE, NoSyn), (bar, NONE, NoSyn), (blink, NONE, NoSyn)],[])"} |
|
715 |
|
716 Lines 5 to 9 in the function @{ML spec_parser} implement the parser for a |
|
717 list of introduction rules, that is propositions with theorem |
700 list of introduction rules, that is propositions with theorem |
718 annotations. The introduction rules are propositions parsed by @{ML |
701 annotations. The introduction rules are propositions parsed by @{ML |
719 OuterParse.prop}. However, they can include an optional theorem name plus |
702 OuterParse.prop}. However, they can include an optional theorem name plus |
720 some attributes. For example |
703 some attributes. For example |
721 |
704 |
727 end" "(foo_lemma, [((\"intro\", []), \<dots>), ((\"dest\", [\<dots>]), \<dots>)])"} |
710 end" "(foo_lemma, [((\"intro\", []), \<dots>), ((\"dest\", [\<dots>]), \<dots>)])"} |
728 |
711 |
729 The function @{ML opt_thm_name in SpecParse} is the ``optional'' variant of |
712 The function @{ML opt_thm_name in SpecParse} is the ``optional'' variant of |
730 @{ML thm_name in SpecParse}. Theorem names can contain attributes. The name |
713 @{ML thm_name in SpecParse}. Theorem names can contain attributes. The name |
731 has to end with @{text [quotes] ":"}---see the argument of |
714 has to end with @{text [quotes] ":"}---see the argument of |
732 the function @{ML SpecParse.opt_thm_name} in Line 9. |
715 the function @{ML SpecParse.opt_thm_name} in Line 8. |
733 |
716 |
734 \begin{readmore} |
717 \begin{readmore} |
735 Attributes and arguments are implemented in the files @{ML_file "Pure/Isar/attrib.ML"} |
718 Attributes and arguments are implemented in the files @{ML_file "Pure/Isar/attrib.ML"} |
736 and @{ML_file "Pure/Isar/args.ML"}. |
719 and @{ML_file "Pure/Isar/args.ML"}. |
737 \end{readmore} |
720 \end{readmore} |