# HG changeset patch # User Christian Urban # Date 1250902568 -7200 # Node ID e450fa467e3fb46efb969e95fd4b6ab77f3a9dda # Parent 1859210215519920e789ab806894baff14d35a8c polished the commands section diff -r 185921021551 -r e450fa467e3f ProgTutorial/Helper/Command/Command.thy --- a/ProgTutorial/Helper/Command/Command.thy Fri Aug 21 16:23:51 2009 +0200 +++ b/ProgTutorial/Helper/Command/Command.thy Sat Aug 22 02:56:08 2009 +0200 @@ -1,10 +1,11 @@ theory Command imports Main begin + ML {* let val do_nothing = Scan.succeed (LocalTheory.theory I) - val kind = OuterKeyword.thy_goal + val kind = OuterKeyword.thy_decl in OuterSyntax.local_theory "foobar" "description of foobar" kind do_nothing end @@ -12,11 +13,61 @@ ML {* let + fun trace_prop str = + LocalTheory.theory (fn lthy => (tracing str; lthy)) + 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 +end +*} + +ML {* +let + fun prove_prop str lthy = + let + val prop = Syntax.read_prop lthy str + in + Proof.theorem_i NONE (K I) [[(prop,[])]] lthy + 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" + kind prove_prop_parser +end +*} + +ML {* +val r = ref (NONE:(unit -> term) option) +*} +ML {* +let + fun setup_proof (txt, pos) lthy = + let + val trm = ML_Context.evaluate lthy true ("r", r) txt + in + Proof.theorem_i NONE (K I) [[(trm,[])]] lthy + end; + + val setup_proof_parser = OuterParse.ML_source >> setup_proof + + val kind = OuterKeyword.thy_goal +in + OuterSyntax.local_theory_to_proof "foobar_prove" "proving a proposition" + kind setup_proof_parser +end +*} + +(* +ML {* +let val do_nothing = Scan.succeed (LocalTheory.theory I) val kind = OuterKeyword.thy_decl in - OuterSyntax.local_theory "simple_induct" "description of foobar" kind do_nothing + OuterSyntax.local_theory "simple_inductive" "description of foobar" kind do_nothing end -*} +*}*) end diff -r 185921021551 -r e450fa467e3f ProgTutorial/Helper/IsaMakefile --- a/ProgTutorial/Helper/IsaMakefile Fri Aug 21 16:23:51 2009 +0200 +++ b/ProgTutorial/Helper/IsaMakefile Sat Aug 22 02:56:08 2009 +0200 @@ -21,7 +21,7 @@ Command: $(LOG)/HOL-Command.gz -$(LOG)/HOL-Command.gz: ## Command/ROOT.ML Command/document/root.tex Command/*.thy +$(LOG)/HOL-Command.gz: Command/ROOT.ML Command/*.thy @$(USEDIR) HOL Command diff -r 185921021551 -r e450fa467e3f ProgTutorial/Helper/isar-keywords-command.el --- a/ProgTutorial/Helper/isar-keywords-command.el Fri Aug 21 16:23:51 2009 +0200 +++ b/ProgTutorial/Helper/isar-keywords-command.el Sat Aug 22 02:56:08 2009 +0200 @@ -1,6 +1,6 @@ ;; ;; Keyword classification tables for Isabelle/Isar. -;; Generated from Pure + HOL + Pure-ProofGeneral + HOL-Command. +;; Generated from Pure + Pure-ProofGeneral + HOL + HOL-Command. ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT *** ;; @@ -97,6 +97,9 @@ "find_theorems" "fix" "foobar" + "foobar_goal" + "foobar_prove" + "foobar_trace" "from" "full_prf" "fun" @@ -197,7 +200,7 @@ "section" "setup" "show" - "simple_induct" + "simple_inductive" "simproc_setup" "sledgehammer" "sorry" @@ -433,6 +436,8 @@ "extract" "extract_type" "finalconsts" + "foobar" + "foobar_trace" "fun" "global" "hide" @@ -464,7 +469,7 @@ "record" "refute_params" "setup" - "simple_induct" + "simple_inductive" "simproc_setup" "syntax" "text" @@ -484,7 +489,8 @@ '("ax_specification" "code_pred" "corollary" - "foobar" + "foobar_goal" + "foobar_prove" "function" "instance" "interpretation" diff -r 185921021551 -r e450fa467e3f ProgTutorial/Parsing.thy --- a/ProgTutorial/Parsing.thy Fri Aug 21 16:23:51 2009 +0200 +++ b/ProgTutorial/Parsing.thy Sat Aug 22 02:56:08 2009 +0200 @@ -1,22 +1,22 @@ theory Parsing -imports Base "Package/Simple_Inductive_Package" +imports Base "Helper/Command/Command" "Package/Simple_Inductive_Package" uses "Parsing.ML" begin chapter {* Parsing *} text {* - - Isabelle distinguishes between \emph{outer} and \emph{inner} syntax. - Commands, such as \isacommand{definition}, \isacommand{inductive} and so - on, belong to the outer syntax, whereas terms, types and so on belong to the - inner syntax. For parsing inner syntax, - Isabelle uses a rather general and sophisticated algorithm, which - is driven by priority grammars. Parsers for outer syntax are built up by functional - parsing combinators. These combinators are a well-established technique for parsing, - which has, for example, been described in Paulson's classic ML-book \cite{paulson-ml2}. - Isabelle developers are usually concerned with writing these outer syntax parsers, - either for new definitional packages or for calling methods with specific arguments. + Isabelle distinguishes between \emph{outer} and \emph{inner} + syntax. Commands, such as \isacommand{definition}, \isacommand{inductive} + and so on, belong to the outer syntax, whereas terms, types and so on belong + to the inner syntax. For parsing inner syntax, Isabelle uses a rather + general and sophisticated algorithm, which is driven by priority + grammars. Parsers for outer syntax are built up by functional parsing + combinators. These combinators are a well-established technique for parsing, + which has, for example, been described in Paulson's classic ML-book + \cite{paulson-ml2}. Isabelle developers are usually concerned with writing + these outer syntax parsers, either for new definitional packages or for + calling methods with specific arguments. \begin{readmore} The library for writing parser combinators is split up, roughly, into two @@ -25,9 +25,9 @@ "Pure/General/scan.ML"}. The second part of the library consists of combinators for dealing with specific token types, which are defined in the structure @{ML_struct OuterParse} in the file @{ML_file - "Pure/Isar/outer_parse.ML"}. Specific parsers for packages are defined - in @{ML_file "Pure/Isar/spec_parse.ML"}. Parsers for method arguments - are defined in @{ML_file "Pure/Isar/args.ML"}. + "Pure/Isar/outer_parse.ML"}. Specific parsers for packages are defined in + @{ML_file "Pure/Isar/spec_parse.ML"}. Parsers for method arguments are + defined in @{ML_file "Pure/Isar/args.ML"}. \end{readmore} *} @@ -136,9 +136,9 @@ end" "((\"h\", [\"e\", \"l\", \"l\", \"o\"]), (\"w\", [\"o\", \"r\", \"l\", \"d\"]))"} - The functions @{ML_ind "|--"} and @{ML_ind "--|"} work like the sequencing function - for parsers, except that they discard the item being parsed by the first (respectively second) - parser. For example: + The functions @{ML_ind "|--"} and @{ML_ind "--|"} work like the sequencing + function for parsers, except that they discard the item being parsed by the + first (respectively second) parser. For example: @{ML_response [display,gray] "let @@ -944,29 +944,34 @@ $ISABELLE_LOGS/{Pure.gz,HOL.gz,Pure-ProofGeneral.gz,HOL-FoobarCommand.gz}"} The result is the file @{text "isar-keywords-foobar.el"}. It should contain - the string @{text "foobar"} twice.\footnote{To see whether things are fine, check - that @{text "grep foobar"} on this file returns something - non-empty.} This keyword file needs to - be copied into the directory @{text "~/.isabelle/etc"}. To make ProofGeneral - aware of this keyword file, you have to start Isabelle with the option @{text - "-k foobar"}, that is: + the string @{text "foobar"} twice.\footnote{To see whether things are fine, + check that @{text "grep foobar"} on this file returns something non-empty.} + This keyword file needs to be copied into the directory @{text + "~/.isabelle/etc"}. To make ProofGeneral aware of it, you have to start + Isabelle with the option @{text "-k foobar"}, that is: @{text [display] "$ isabelle emacs -k foobar a_theory_file"} If you now build a theory on top of @{text "Command.thy"}, - then the command \isacommand{foobar} can be used. - Similarly with any other new command, and also any new keyword that is - introduced with + then the command \isacommand{foobar} can be used. You can just write +*} + +foobar + +text {* + but you will not see any action as we chose to implement this command to do + nothing. A similarly procedure has to be done with any other new command, and + also any new keyword that is introduced with @{ML_ind OuterKeyword.keyword}. + *} ML{*val _ = OuterKeyword.keyword "blink" *} text {* - At the moment the command \isacommand{foobar} is not very useful. Let us refine - it a bit - next by letting it take a proposition as argument and printing this proposition - inside the tracing buffer. + At the moment the command \isacommand{foobar} is not very useful. Let us + refine it a bit next by letting it take a proposition as argument and + printing this proposition inside the tracing buffer. The crucial part of a command is the function that determines the behaviour of the command. In the code above we used a ``do-nothing''-function, which @@ -985,21 +990,18 @@ val trace_prop_parser = OuterParse.prop >> trace_prop val kind = OuterKeyword.thy_decl in - OuterSyntax.local_theory "foobar" "traces a proposition" + OuterSyntax.local_theory "foobar_trace" "traces a proposition" kind trace_prop_parser end *} +text {* + The command is now \isacommand{foobar\_trace} and can be used to + see the proposition in the tracing buffer. +*} + +foobar_trace "True \ False" text {* - Now you can type - - \begin{isabelle} - \isacommand{foobar}~@{text [quotes] "True \ False"}\\ - @{text "> \"True \ False\""} - \end{isabelle} - - and see the proposition in the tracing buffer. - Note that so far we used @{ML_ind thy_decl in OuterKeyword} as the kind indicator for the command. This means that the command finishes as soon as the arguments are processed. Examples of this kind of commands are @@ -1014,7 +1016,7 @@ OuterKeyword} to @{ML thy_goal in OuterKeyword} then the keyword file needs to be re-created! - Below we change \isacommand{foobar} so that it takes a proposition as + Below we change \isacommand{foobar\_trace} so that it takes a proposition as argument and then starts a proof in order to prove it. Therefore in Line 13, we set the kind indicator to @{ML thy_goal in OuterKeyword}. *} @@ -1030,7 +1032,7 @@ val prove_prop_parser = OuterParse.prop >> prove_prop val kind = OuterKeyword.thy_goal in - OuterSyntax.local_theory_to_proof "foobar" "proving a proposition" + OuterSyntax.local_theory_to_proof "foobar_goal" "proving a proposition" kind prove_prop_parser end *} @@ -1044,28 +1046,49 @@ should be done with the theorem once it is proved (we chose to just forget about it). Line 9 contains the parser for the proposition. - If you now type \isacommand{foobar}~@{text [quotes] "True \ True"}, you obtain the following - proof state - - \begin{isabelle} - \isacommand{foobar}~@{text [quotes] "True \ True"}\\ - @{text "goal (1 subgoal):"}\\ - @{text "1. True \ True"} - \end{isabelle} + If you now type \isacommand{foobar\_goal}~@{text [quotes] "True \ True"}, + you obtain the following proof state +*} - and you can build the following proof +foobar_goal "True \ True" +txt {* + \begin{minipage}{\textwidth} + @{subgoals [display]} + \end{minipage}\medskip - \begin{isabelle} - \isacommand{foobar}~@{text [quotes] "True \ True"}\\ - \isacommand{apply}@{text "(rule conjI)"}\\ - \isacommand{apply}@{text "(rule TrueI)+"}\\ - \isacommand{done} - \end{isabelle} + and can prove the proposition as follows. +*} +apply(rule conjI) +apply(rule TrueI)+ +done + +text {* (FIXME: read a name and show how to store theorems; see @{ML_ind note in LocalTheory}) *} +ML_val{*val r = ref (NONE:(unit -> term) option)*} +ML{*let + fun setup_proof (txt, pos) lthy = + let + val trm = ML_Context.evaluate lthy true ("r", r) txt + in + Proof.theorem_i NONE (K I) [[(trm,[])]] lthy + end; + + val setup_proof_parser = OuterParse.ML_source >> setup_proof + + val kind = OuterKeyword.thy_goal +in + OuterSyntax.local_theory_to_proof "foobar_prove" "proving a proposition" + kind setup_proof_parser +end*} + +foobar_prove {* @{prop "True"} *} +apply(rule TrueI) +done + diff -r 185921021551 -r e450fa467e3f progtutorial.pdf Binary file progtutorial.pdf has changed