--- a/CookBook/FirstSteps.thy Fri Jan 16 14:57:36 2009 +0000
+++ b/CookBook/FirstSteps.thy Fri Jan 23 17:50:35 2009 +0000
@@ -2,7 +2,6 @@
imports Base
begin
-
chapter {* First Steps *}
text {*
@@ -29,19 +28,22 @@
The easiest and quickest way to include code in a theory is
by using the \isacommand{ML}-command. For example\smallskip
+\begin{isabelle}
+\begin{graybox}
\isa{\isacommand{ML}
\isacharverbatimopen\isanewline
\hspace{5mm}@{ML "3 + 4"}\isanewline
\isacharverbatimclose\isanewline
@{text "> 7"}\smallskip}
+\end{graybox}
+\end{isabelle}
- The @{text [quotes] "> 7"} indicates the response Isabelle prints out when the
- \isacommand{ML}-command is evaluated. Like ``normal'' Isabelle proof scripts,
+ Like ``normal'' Isabelle proof scripts,
\isacommand{ML}-commands can be evaluated by using the advance and undo buttons of
your Isabelle environment. The code inside the \isacommand{ML}-command
can also contain value and function bindings, and even those can be
- undone when the proof script is retracted. For better readability, we will in what
- follows drop the \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose}
+ undone when the proof script is retracted. As mentioned earlier, we will
+ drop the \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose}
whenever we show code and its response.
Once a portion of code is relatively stable, one usually wants to
@@ -73,7 +75,7 @@
will print out @{text [quotes] "any string"} inside the response buffer
of Isabelle. This function expects a string as argument. If you develop under PolyML,
then there is a convenient, though again ``quick-and-dirty'', method for
- converting values into strings, namely @{ML makestring}:
+ converting values into strings, namely using the function @{ML makestring}:
@{ML_response_fake [display,gray] "warning (makestring 1)" "\"1\""}
@@ -109,9 +111,16 @@
text {*
Calling @{ML "redirect_tracing"} with @{ML "(TextIO.openOut \"foo.bar\")"}
will cause that all tracing information is printed into the file @{text "foo.bar"}.
+
+ Error messages can be printed using the function @{ML error} as in
+
+ @{ML_response_fake [display,gray] "if 0=1 then 1 else (error \"foo\")" "\"foo\""}
+
*}
+
+
section {* Antiquotations *}
text {*
@@ -145,9 +154,12 @@
some data structure and return it. Instead, it is literally
replaced with the value representing the theory name.
- In a similar way you can use antiquotations to refer to theorems or simpsets:
+ In a similar way you can use antiquotations to refer to theorems:
@{ML_response_fake [display,gray] "@{thm allI}" "(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x"}
+
+ or simpsets:
+
@{ML_response_fake [display,gray]
"let
val ({rules,...},_) = MetaSimplifier.rep_ss @{simpset}
@@ -155,24 +167,31 @@
map #name (Net.entries rules)
end" "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}
- The second example extracts the theorem names that are stored in a simpset.
- For this the function @{ML rep_ss in MetaSimplifier} returns a record
- containing information about the simpset. The rules of a simpset are stored
+ The code above extracts the theorem names that are stored in a simpset.
+ We refer to the current simpset with the antiquotation @{text "@{simpset}"}.
+ The function @{ML rep_ss in MetaSimplifier} returns a record
+ containing all information about the simpset. The rules of a simpset are stored
in a discrimination net (a datastructure for fast indexing). From this net
we can extract the entries using the function @{ML Net.entries}.
- While antiquotations have many applications, they were originally introduced to
- avoid explicit bindings for theorems such as
+ \begin{readmore}
+ The infrastructure for simpsets is implemented in @{ML_file "Pure/meta_simplifier.ML"}
+ and @{ML_file "Pure/simplifier.ML"}.
+ \end{readmore}
+
+ While antiquotations have many applications, they were originally introduced in order
+ to avoid explicit bindings for theorems such as
*}
ML{*val allI = thm "allI" *}
text {*
- These bindings were difficult to maintain and also could accidentally
- be overwritten by the user. This usually broke definitional
+ These bindings were difficult to maintain and also could be accidentally
+ overwritten by the user. This usually broke definitional
packages. Antiquotations solve this problem, since they are ``linked''
- statically at compile-time. However, that also sometimes limits their
- usefulness. In the course of this introduction, we will learn more about
+ statically at compile-time. However, this static linkage also limits their
+ usefulness in cases where data needs to be build up dynamically. In the course of
+ this introduction, we will learn more about
these antiquotations: they greatly simplify Isabelle programming since one
can directly access all kinds of logical elements from ML.
@@ -185,8 +204,9 @@
\mbox{@{text "@{term \<dots>}"}}. For example
@{ML_response [display,gray]
- "@{term \"(a::nat) + b = c\"}"
- "Const (\"op =\", \<dots>) $ (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
+"@{term \"(a::nat) + b = c\"}"
+"Const (\"op =\", \<dots>) $
+ (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
This will show the term @{term "(a::nat) + b = c"}, but printed using the internal
representation of this term. This internal representation corresponds to the
@@ -222,7 +242,7 @@
can use the following ML function to set the limit to a value high
enough:
- @{ML [display] "print_depth 50"}
+ @{ML [display,gray] "print_depth 50"}
\end{exercise}
The antiquotation @{text "@{prop \<dots>}"} constructs terms of propositional type,
@@ -265,7 +285,8 @@
ML{*fun make_imp P Q tau =
let
val x = Free ("x",tau)
- in Logic.all x (Logic.mk_implies (P $ x, Q $ x))
+ in
+ Logic.all x (Logic.mk_implies (P $ x, Q $ x))
end *}
text {*
@@ -278,7 +299,7 @@
text {*
To see this apply @{text "@{term S}"}, @{text "@{term T}"} and @{text "@{typ nat}"}
- to both functions. With @{ML make_imp} we obtain the correct term involving
+ to both functions. With @{ML make_imp} we obtain the intended term involving
@{term "S"}, @{text "T"} and @{text "@{typ nat}"}
@{ML_response [display,gray] "make_imp @{term S} @{term T} @{typ nat}"
@@ -287,7 +308,7 @@
Const \<dots> $ (Free (\"S\",\<dots>) $ \<dots>) $
(Free (\"T\",\<dots>) $ \<dots>))"}
- With @{ML make_wrong_imp} we obtain an incorrect term involving the @{term "P"}
+ With @{ML make_wrong_imp} we obtain a term involving the @{term "P"}
and @{text "Q"} from the antiquotation.
@{ML_response [display,gray] "make_wrong_imp @{term S} @{term T} @{typ nat}"
@@ -316,15 +337,14 @@
(FIXME: Is it useful to explain @{text "@{const_syntax}"}?)
- Similarly, types can be constructed manually, for example as follows:
+ Similarly, types can be constructed manually. For example a function type
+ can be constructed as follows:
*}
ML{*fun make_fun_type tau1 tau2 = Type ("fun",[tau1,tau2]) *}
-text {*
- which can be equally written as
-*}
+text {* This can be equally written as *}
ML{*fun make_fun_type tau1 tau2 = tau1 --> tau2 *}
@@ -351,7 +371,7 @@
\begin{exercise}\label{fun:makesum}
Write a function which takes two terms representing natural numbers
- in unary (like @{term "Suc (Suc (Suc 0))"}), and produce the unary
+ in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produce the
number representing their sum.
\end{exercise}
@@ -393,8 +413,7 @@
val zero = @{term \"0::nat\"}
in
cterm_of @{theory}
- (Const (@{const_name plus}, natT --> natT --> natT)
- $ zero $ zero)
+ (Const (@{const_name plus}, natT --> natT --> natT) $ zero $ zero)
end" "0 + 0"}
\begin{exercise}
@@ -408,8 +427,8 @@
text {*
Just like @{ML_type cterm}s, theorems are abstract objects of type @{ML_type thm}
- that can only be built by going through interfaces. In effect all proofs
- are checked.
+ that can only be built by going through interfaces. As a consequence of this is that
+ every proof is correct by construction (FIXME reference LCF-philosophy)
To see theorems in ``action'', let us give a proof for the following statement
*}
@@ -421,8 +440,7 @@
text {*
on the ML-level:\footnote{Note that @{text "|>"} is reverse
- application. This combinator, and several variants are defined in
- @{ML_file "Pure/General/basics.ML"}.}
+ application. See Section~\ref{sec:combinators}.}
@{ML_response_fake [display,gray]
"let
@@ -467,121 +485,26 @@
*}
-
-section {* Tactical Reasoning *}
-
-text {*
- The goal-oriented tactical style reasoning of the ML level is similar
- to the @{text apply}-style at the user level, i.e.~the reasoning is centred
- around a \emph{goal}, which is modified in a sequence of proof steps
- until it is solved.
-
- A goal (or goal state) is a special @{ML_type thm}, which by
- convention is an implication of the form:
-
- @{text[display] "A\<^isub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^isub>n \<Longrightarrow> #(C)"}
-
- where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are the open
- subgoals.
- Since the goal @{term C} can potentially be an implication, there is a
- @{text "#"} wrapped around it, which prevents that premises are
- misinterpreted as open subgoals. The wrapper @{text "# :: prop \<Rightarrow>
- prop"} is just the identity function and used as a syntactic marker.
-
- \begin{readmore}
- For more on goals see \isccite{sec:tactical-goals}. (FIXME: in which
- file is most code for dealing with goals?)
- \end{readmore}
-
- Tactics are functions that map a goal state to a (lazy)
- sequence of successor states, hence the type of a tactic is
-
- @{ML_type[display] "thm -> thm Seq.seq"}
-
- \begin{readmore}
- See @{ML_file "Pure/General/seq.ML"} for the implementation of lazy
- sequences. However in day-to-day Isabelle programming, one rarely
- constructs sequences explicitly, but uses the predefined tactic
- combinators (tacticals) instead. See @{ML_file "Pure/tctical.ML"}
- for the code; see Chapters 3 and 4 in the old Isabelle Reference Manual.
- \end{readmore}
-
- While tactics can operate on the subgoals (the @{text "A\<^isub>i"} above), they
- are expected to leave the conclusion @{term C} intact, with the
- exception of possibly instantiating schematic variables.
-
- To see how tactics work, let us transcribe a simple @{text apply}-style
- proof into ML:
-*}
-
-lemma disj_swap: "P \<or> Q \<Longrightarrow> Q \<or> P"
-apply (erule disjE)
- apply (rule disjI2)
- apply assumption
-apply (rule disjI1)
-apply assumption
-done
-
-text {*
- To start the proof, the function @{ML "Goal.prove"}~@{text "ctxt xs As C tac"} sets
- up a goal state for proving the goal @{text C} under the assumptions @{text As}
- (empty in the proof at hand)
- with the variables @{text xs} that will be generalised once the
- goal is proved. The @{text "tac"} is the tactic which proves the goal and which
- can make use of the local assumptions (there are none in this example).
-
-@{ML_response_fake [display,gray]
-"let
- val ctxt = @{context}
- val goal = @{prop \"P \<or> Q \<Longrightarrow> Q \<or> P\"}
-in
- Goal.prove ctxt [\"P\", \"Q\"] [] goal (fn _ =>
- eresolve_tac [disjE] 1
- THEN resolve_tac [disjI2] 1
- THEN assume_tac 1
- THEN resolve_tac [disjI1] 1
- THEN assume_tac 1)
-end" "?P \<or> ?Q \<Longrightarrow> ?Q \<or> ?P"}
-
- \begin{readmore}
- To learn more about the function @{ML Goal.prove} see \isccite{sec:results} and
- the file @{ML_file "Pure/goal.ML"}.
- \end{readmore}
-
-
- An alternative way to transcribe this proof is as follows
-
-@{ML_response_fake [display,gray]
-"let
- val ctxt = @{context}
- val goal = @{prop \"P \<or> Q \<Longrightarrow> Q \<or> P\"}
-in
- Goal.prove ctxt [\"P\", \"Q\"] [] goal (fn _ =>
- (eresolve_tac [disjE]
- THEN' resolve_tac [disjI2]
- THEN' assume_tac
- THEN' resolve_tac [disjI1]
- THEN' assume_tac) 1)
-end" "?P \<or> ?Q \<Longrightarrow> ?Q \<or> ?P"}
-
- (FIXME: are there any advantages/disadvantages about this way?)
-*}
-
section {* Storing Theorems *}
section {* Theorem Attributes *}
-
-section {* Combinators *}
+section {* Operations on Constants (Names) *}
text {*
- Perhaps one of the most puzzling aspects for a beginner when looking at
+ (FIXME how can I extract the constant name without the theory name etc)
+*}
+
+section {* Combinators\label{sec:combinators} *}
+
+text {*
+ Perhaps one of the most puzzling aspects for a beginner when reading at
existing Isabelle code is the liberal use of combinators. At first they
- seem to obstruct reading the code, but after getting familiar with them
- they actually ease the reading and also the programming.
+ seem to obstruct the comprehension of the code, but after getting familiar
+ with them they actually ease the reading and also the programming.
\begin{readmore}
- The most frequently used combinator are defined in @{ML_file "Pure/library.ML"}
+ The most frequently used combinator are defined in the files @{ML_file "Pure/library.ML"}
and @{ML_file "Pure/General/basics.ML"}.
\end{readmore}
@@ -590,10 +513,17 @@
ML{*fun I x = x*}
+text {* Another frequently used combinator is @{ML K} *}
+
+ML{*fun K x = fn _ => x*}
+
text {*
- Another frequently used combinator is @{ML K}
+ which ``wraps'' a function around the argument @{text "x"}. This function
+ ignores its argument.
-
+ @{ML "(op |>)"}
*}
+ML{*fun x |> f = f x*}
+
end
\ No newline at end of file
--- a/CookBook/Intro.thy Fri Jan 16 14:57:36 2009 +0000
+++ b/CookBook/Intro.thy Fri Jan 23 17:50:35 2009 +0000
@@ -1,5 +1,5 @@
theory Intro
-imports Main
+imports Base
begin
@@ -8,24 +8,24 @@
text {*
The purpose of this Cookbook is to guide the reader through the first steps
- of Isabelle programming, and to explain some tricks of the trade. The code
+ of Isabelle programming, and to explain tricks of the trade. The code
provided in the Cookbook is as far as possible checked against recent
versions of Isabelle. If something does not work, then please let us
know. If you have comments or like to add to the Cookbook, you are very
- welcome.
+ welcome! The Cookbook will {\bf only} remain to be helpful, if it gets constantly
+ updated.
*}
section {* Intended Audience and Prior Knowledge *}
text {*
- This Cookbook targets readers who already know how to use Isabelle
- for writing theories and proofs. We also assume that readers are
- familiar with the functional programming language ML, the language in
- which most of Isabelle is implemented. If you are unfamiliar with either of
- these two subjects, you should first work through the Isabelle/HOL
- tutorial \cite{isa-tutorial} or Paulson's book on ML
- \cite{paulson-ml2}.
+ This Cookbook targets readers who already know how to use Isabelle for
+ writing theories and proofs. We also assume that readers are familiar with
+ the functional programming language ML, the language in which most of
+ Isabelle is implemented. If you are unfamiliar with either of these two
+ subjects, you should first work through the Isabelle/HOL tutorial
+ \cite{isa-tutorial} or Paulson's book on ML \cite{paulson-ml2}.
*}
@@ -67,8 +67,42 @@
section {* Conventions *}
text {*
- We use @{text "$"} to indicate a command needs to be run on the Unix-command
- line.
+
+ All ML-code in this Cookbook is shown in highlighed displays, such as:
+
+ \begin{isabelle}
+ \begin{graybox}
+ \isa{\isacommand{ML}
+ \isacharverbatimopen\isanewline
+ \hspace{5mm}@{ML "3 + 4"}\isanewline
+ \isacharverbatimclose}
+ \end{graybox}
+ \end{isabelle}
+
+ This corresponds to how code can be processed inside the interactive
+ environment of Isabelle. However, for better readability we will drop
+ the enclosing \isacommand{ML} \isa{\isacharverbatimopen \ldots
+ \isacharverbatimclose} and just show
+
+ @{ML [display,gray] "3 + 4"}
+
+ for the code above. Whenever appropriate we show the response of the code
+ when evaluated. The response is prefixed with a @{text [quotes] ">"}", like
+
+ @{ML_response [display,gray] "3 + 4" "7"}
+
+ Isabelle commands are written in bold. For example \isacommand{lemma},
+ \isacommand{foobar} and so on. We use @{text "$"} to indicate a command
+ needs to be run on the Unix-command line, like
+
+ @{text [display] "$ ls -la"}
+
+ Pointers to further information and files are indicated as follows:
+
+ \begin{readmore}
+ Further information.
+ \end{readmore}
+
*}
--- a/CookBook/Parsing.thy Fri Jan 16 14:57:36 2009 +0000
+++ b/CookBook/Parsing.thy Fri Jan 23 17:50:35 2009 +0000
@@ -189,7 +189,7 @@
"Exception ABORT raised"}
then the parsing aborts and the error message @{text "foo"} is printed out. In order to
- see the error message properly, we need to prefix the parser with the function
+ see the error message, we need to prefix the parser with the function
@{ML "Scan.error"}. For example
@{ML_response_fake [display,gray] "Scan.error (!! (fn _ => \"foo\") ($$ \"h\"))"
@@ -353,17 +353,17 @@
The definition for tokens is in the file @{ML_file "Pure/Isar/outer_lex.ML"}.
\end{readmore}
- The structure @{ML_struct OuterLex} defines several kinds of token (for example
+ The structure @{ML_struct OuterLex} defines several kinds of tokens (for example
@{ML "Ident" in OuterLex} for identifiers, @{ML "Keyword" in OuterLex} for keywords and
@{ML "Command" in OuterLex} for commands). Some token parsers take into account the
- kind of token.
+ kind of tokens.
*}
text {*
For the examples below, we can generate a token list out of a string using
the function @{ML "OuterSyntax.scan"}, which we give below @{ML
"Position.none"} as argument since, at the moment, we are not interested in
- generating precise error messages. The following
+ generating precise error messages. The following code
@{ML_response_fake [display,gray] "OuterSyntax.scan Position.none \"hello world\""
@@ -375,7 +375,7 @@
@{text [quotes] "hello"} and @{text [quotes] "world"} do not match any
other syntactic category.\footnote{Note that because of a possible a bug in
the PolyML runtime system the result is printed as @{text "?"}, instead of
- the token.} The second indicates a space.
+ the tokens.} The second indicates a space.
Many parsing functions later on will require spaces, comments and the like
to have already been filtered out. So from now on we are going to use the
@@ -409,7 +409,7 @@
we obtain a list consisting of only a command and two keyword tokens.
If you want to see which keywords and commands are currently known, type in
- the following (you might have to adjust the @{ML print_depth} in order to
+ the following code (you might have to adjust the @{ML print_depth} in order to
see the complete list):
@{ML_response_fake [display,gray]
@@ -454,7 +454,7 @@
"([\"in\",\"in\",\"in\"],[\<dots>])"}
@{ML "OuterParse.enum1"} works similarly, except that the parsed list must
- be non-empty. Note that we had to add an @{text [quotes] "foo"} at the end
+ be non-empty. Note that we had to add a string @{text [quotes] "foo"} at the end
of the parsed string, otherwise the parser would have consumed all tokens
and then failed with the exception @{text "MORE"}. Like in the previous
section, we can avoid this exception using the wrapper @{ML
@@ -470,7 +470,7 @@
end"
"([\"in\",\"in\",\"in\"],[])"}
- The following function will help us later to run examples
+ The following function will help to run examples.
*}
@@ -585,7 +585,7 @@
The option @{text "-k foobar"} indicates which postfix the name of the keyword file
will be assigned. In the case above the generated file will be named @{text
- "isar-keywords-foobar.el"}. As indicated, this command requires log files to be
+ "isar-keywords-foobar.el"}. As can be seen, this command requires log files to be
present (in order to extract the keywords from them). To generate these log
files, we first package the code above into a separate theory file named
@{text "Command.thy"}, say---see Figure~\ref{fig:commandtheory} for the
@@ -608,21 +608,21 @@
end"}\\
\isa{\isacharverbatimclose}\\
\isacommand{end}
- \end{graybox}
- \caption{The file @{text "Command.thy"} is necessary for generating a log
+ \end{graybox}\\[-4mm]
+ \caption{\small The file @{text "Command.thy"} is necessary for generating a log
file. This log file enables Isabelle to generate a keyword file containing
the command \isacommand{foobar}.\label{fig:commandtheory}}
\end{figure}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- For our purposes it is sufficient to use the log files for the theories
+ For our purposes it is sufficient to use the log files of the theories
@{text "Pure"}, @{text "HOL"} and @{text "Pure-ProofGeneral"}, as well as
- the theory @{text "Command.thy"} containing the new
- \isacommand{foobar}-command. If you target another logics besides HOL, such
+ the log file for the theory @{text "Command.thy"}, which contains the new
+ \isacommand{foobar}-command. If you target other logics besides HOL, such
as Nominal or ZF, then you need to adapt the log files appropriately.
@{text Pure} and @{text HOL} are usually compiled during the installation of
Isabelle. So log files for them should be already available. If not, then
- they can be conveniently compiled using build-script from the Isabelle
+ they can be conveniently compiled with the help of the build-script from the Isabelle
distribution
@@ -675,8 +675,8 @@
Pure-ProofGeneral.gz
HOL-FoobarCommand.gz"}
- They are the ones we need for creating the keyword files. Assuming the name
- of the directory is in @{text "ISABELLE_LOGS"},
+ From them we create the keyword files. Assuming the name
+ of the directory is in @{text "$ISABELLE_LOGS"},
then the Unix command for creating the keyword file is:
@{text [display]
@@ -687,53 +687,48 @@
string @{text "foobar"} twice (check for example that @{text "grep foobar
isar-keywords-foobar.el"} returns something non-empty). This keyword file
needs to be copied into the directory @{text "~/.isabelle/etc"}. To make
- Isabelle aware of this keyword file, we have to start it with the option @{text
+ Isabelle aware of this keyword file, we have to start Isabelle with the option @{text
"-k foobar"}, i.e.
@{text [display] "$ isabelle -k foobar a_theory_file"}
- If we now run the original code
-*}
-
-ML{*let
- val do_nothing = Scan.succeed (Toplevel.theory I)
- val kind = OuterKeyword.thy_decl
-in
- OuterSyntax.command "foobar" "description of foobar" kind do_nothing
-end *}
-
-text {*
- then we can make use of \isacommand{foobar} in a theory that builds on @{text "Command.thy"}!
+ If we now build a theory on top of @{text "Command.thy"},
+ then we can make use of the command \isacommand{foobar}.
Similarly with any other new command.
- At the moment \isacommand{foobar} is not very useful. Let us next refine it a bit
- by taking a proposition as argument and printing this proposition inside
+ At the moment \isacommand{foobar} is not very useful. Let us refine it a bit
+ next by taking 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 because of @{ML Scan.succeed} does not parse
- any argument, but immediately returns the simple toplevel function
- @{ML "Toplevel.theory I"}. We can replace this code by a function that first
- parses a proposition (using the parser @{ML OuterParse.prop}), then prints out
- the tracing information and finally does nothing. For this we can write
+ 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
+ because of @{ML Scan.succeed} does not parse any argument, but immediately
+ returns the simple toplevel function @{ML "Toplevel.theory I"}. We can
+ replace this code by a function that first parses a proposition (using the
+ parser @{ML OuterParse.prop}), then prints out the tracing
+ information (using a new top-level function @{text trace_top_lvl}) and
+ finally does nothing. For this we can write
+
*}
ML{*let
- val trace_prop =
- OuterParse.prop >> (fn str => (tracing str; (Toplevel.theory I)))
+ fun trace_top_lvl str =
+ Toplevel.theory (fn thy => (tracing str; thy))
+
+ val trace_prop = OuterParse.prop >> trace_top_lvl
+
val kind = OuterKeyword.thy_decl
in
OuterSyntax.command "foobar" "traces a proposition" kind trace_prop
end *}
text {*
- Now we can type for example
+ Now we can type
\begin{isabelle}
\isacommand{foobar}~@{text [quotes] "True \<and> False"}\\
- @{text "> True \<and> False"}
+ @{text "> \"True \<and> False\""}
\end{isabelle}
and see the proposition in the tracing buffer.
@@ -741,14 +736,14 @@
Note that so far we used @{ML 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
- \isacommand{definition} and \isacommand{declare}. In other cases
+ \isacommand{definition} and \isacommand{declare}. In other cases,
commands are expected to parse some arguments, for example a proposition,
- and then ``open up'' a proof in order to prove the proposition (think of
+ and then ``open up'' a proof in order to prove the proposition (for example
\isacommand{lemma}) or prove some other properties (for example in
- \isacommand{function}). To achieve this behaviour, we have to use the kind
+ \isacommand{function}). To achieve this kind of behaviour, we have to use the kind
indicator @{ML thy_goal in OuterKeyword}.
- Below we change \isacommand{foobar} so that it expects a proposition as
+ Below we change \isacommand{foobar} so that it takes a proposition as
argument and then starts a proof in order to prove it. Therefore in Line 13
below, we set the kind indicator to @{ML thy_goal in OuterKeyword}.
*}
@@ -758,7 +753,7 @@
let
val prop = Syntax.read_prop ctxt str
in
- Proof.theorem_i NONE (K I) [[(Syntax.read_prop ctxt str,[])]] ctxt
+ Proof.theorem_i NONE (K I) [[(prop,[])]] ctxt
end;
val prove_prop = OuterParse.prop >>
@@ -774,8 +769,11 @@
The function @{text set_up_thm} takes a string (the proposition to be
proved) and a context. The context is necessary in order to be able to use
@{ML Syntax.read_prop}, which converts a string into a proper proposition.
- In Line 6 the function @{ML Proof.theorem_i} starts the proof for the
- proposition. In Lines 9 to 11 contain the parser for the proposition.
+ In Line 6 the function @{ML Proof.theorem_i} 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
+ should be done with the theorem once it is proved (we chose to just forget
+ about it). In Lines 9 to 11 contain the parser for the proposition.
If we now type \isacommand{foobar}~@{text [quotes] "True \<and> True"}, we obtain the following
proof state:
@@ -796,12 +794,16 @@
\end{isabelle}
- (FIXME What does @{text "Toplevel.theory"}?)
+ (FIXME What does @{text "Toplevel.theory"} @{text "Toplevel.print"}?)
(FIXME Explain @{text "OuterKeyword.thy_decl"} and parser)
+ (FIXME read a name and show how to store theorems)
+
+ (FIXME possibly also read a locale)
*}
+(*<*)
chapter {* Parsing *}
text {*
@@ -852,9 +854,9 @@
\begin{verbatim}
open StringCvt ;
type ('res, 'src) ex_reader = 'src -> 'res * 'src
- (* ex_reader : ('res, 'src) reader -> ('res, 'src) ex_reader *)
+ ex_reader : ('res, 'src) reader -> ('res, 'src) ex_reader
fun ex_reader rdr src = Option.valOf (rdr src) ;
- (* reader : ('res, 'src) ex_reader -> ('res, 'src) reader *)
+ reader : ('res, 'src) ex_reader -> ('res, 'src) reader
fun reader exrdr src = SOME (exrdr src) handle _ => NONE ;
\end{verbatim}
@@ -1469,7 +1471,6 @@
*}
-
+(*>*)
-
-end
\ No newline at end of file
+end
\ No newline at end of file
--- a/CookBook/ROOT.ML Fri Jan 16 14:57:36 2009 +0000
+++ b/CookBook/ROOT.ML Fri Jan 23 17:50:35 2009 +0000
@@ -5,6 +5,7 @@
use_thy "Intro";
use_thy "FirstSteps";
use_thy "Parsing";
+use_thy "Tactical";
no_document use_thy "Package/Simple_Inductive_Package";
use_thy "Package/Ind_Intro";
Binary file cookbook.pdf has changed