--- 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
--- 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
--- 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"
--- 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 \<and> False"
text {*
- Now you can type
-
- \begin{isabelle}
- \isacommand{foobar}~@{text [quotes] "True \<and> False"}\\
- @{text "> \"True \<and> 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 \<and> True"}, you obtain the following
- proof state
-
- \begin{isabelle}
- \isacommand{foobar}~@{text [quotes] "True \<and> True"}\\
- @{text "goal (1 subgoal):"}\\
- @{text "1. True \<and> True"}
- \end{isabelle}
+ If you now type \isacommand{foobar\_goal}~@{text [quotes] "True \<and> True"},
+ you obtain the following proof state
+*}
- and you can build the following proof
+foobar_goal "True \<and> True"
+txt {*
+ \begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage}\medskip
- \begin{isabelle}
- \isacommand{foobar}~@{text [quotes] "True \<and> 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
+
Binary file progtutorial.pdf has changed