isabelle-cookbook: comparison ProgTutorial/Parsing.thy

equal deleted inserted replaced

-:f76135c6c527
+:ce754ad78bc9
 even and odd
 where
 even0: "even 0"
 | evenS: "odd n \<Longrightarrow> even (Suc n)"
 | oddS: "even n \<Longrightarrow> odd (Suc n)"
 text {*
 For this we are going to use the parser:
 *}
 foobar
 text {*
 but you will not see any action as we chose to implement this command to do
-nothing. The point of this command is to only show the procedure of how
+nothing. The point of this command is only to show the procedure of how
 to interact with ProofGeneral. A similar procedure has to be done with any
 other new command, and also any new keyword that is introduced with
-@{ML_ind OuterKeyword.keyword}.
+the function @{ML_ind keyword in OuterKeyword}. For example:
 *}
 ML{*val _ = OuterKeyword.keyword "blink" *}
 text {*
 finally does nothing. For this you can write:
 *}
 ML{*let
 fun trace_prop str =
-LocalTheory.theory (fn lthy => (tracing str; lthy))
+LocalTheory.theory (fn ctxt => (tracing str; ctxt))
-val trace_prop_parser = OuterParse.prop >> trace_prop
 val kind = OuterKeyword.thy_decl
 in
 OuterSyntax.local_theory "foobar_trace" "traces a proposition"
-kind trace_prop_parser
+kind (OuterParse.prop >> trace_prop)
 end *}
 text {*
 The command is now \isacommand{foobar\_trace} and can be used to
 see the proposition in the tracing buffer.
 "local_theory_to_proof" in OuterSyntax} to set up the command.  Note,
 however, once you change the ``kind'' of a command from @{ML thy_decl in
 OuterKeyword} to @{ML thy_goal in OuterKeyword} then the keyword file needs
 to be re-created!
-Below we change \isacommand{foobar\_trace} so that it takes a proposition as
+Below we show the command \isacommand{foobar\_goal} which takes a
-argument and then starts a proof in order to prove it. Therefore in Line 13,
+proposition as argument and then starts a proof in order to prove
-we set the kind indicator to @{ML thy_goal in OuterKeyword}.
+it. Therefore in Line 9, we set the kind indicator to @{ML thy_goal in
+OuterKeyword}.
 *}
 ML%linenosgray{*let
-fun prove_prop str lthy =
+fun goal_prop str lthy =
 let
 val prop = Syntax.read_prop lthy str
 in
 Proof.theorem_i NONE (K I) [[(prop,[])]] lthy
-end;
+end
-val prove_prop_parser = OuterParse.prop >> prove_prop
 val kind = OuterKeyword.thy_goal
 in
-OuterSyntax.local_theory_to_proof "foobar_goal" "proving a proposition"
+OuterSyntax.local_theory_to_proof "foobar_goal" "proves a proposition"
-kind prove_prop_parser
+kind (OuterParse.prop >> goal_prop)
 end *}
 text {*
-The function @{text prove_prop} in Lines 2 to 7 takes a string (the proposition to be
+The function @{text goal_prop} in Lines 2 to 7 takes a string (the proposition to be
 proved) and a context as argument.  The context is necessary in order to be able to use
 @{ML_ind  read_prop in Syntax}, which converts a string into a proper proposition.
 In Line 6 the function @{ML_ind  theorem_i in Proof} starts the proof for the
 proposition. Its argument @{ML NONE} stands for a locale (which we chose to
 omit); the argument @{ML "(K I)"} stands for a function that determines what
 apply(rule conjI)
 apply(rule TrueI)+
 done
 text {*
+{\bf TBD below}
 (FIXME: read a name and show how to store theorems; see @{ML_ind  note in LocalTheory})
 *}

changeset 327	ce754ad78bc9
parent 326	f76135c6c527
child 328	c0cae24b9d46