--- a/CookBook/FirstSteps.thy Mon Mar 02 10:06:06 2009 +0000
+++ b/CookBook/FirstSteps.thy Tue Mar 03 13:00:55 2009 +0000
@@ -406,13 +406,16 @@
\emph{discrimination net} (a data structure for fast indexing). From this
net you can extract the entries using the function @{ML Net.entries}.
You can now use @{ML get_thm_names_from_ss} to obtain all names of theorems stored
- in the current simpset---this simpset can be referred to using the antiquotation
+ in the current simpset. This simpset can be referred to using the antiquotation
@{text "@{simpset}"}.
@{ML_response_fake [display,gray]
"get_thm_names_from_ss @{simpset}"
"[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}
+ Again, this way or referencing simpsets makes you independent from additions
+ of lemmas to the simpset by the user that potentially cause loops.
+
\begin{readmore}
The infrastructure for simpsets is implemented in @{ML_file "Pure/meta_simplifier.ML"}
and @{ML_file "Pure/simplifier.ML"}. Discrimination nets are implemented
@@ -427,7 +430,7 @@
text {*
These bindings are difficult to maintain and also can be accidentally
- overwritten by the user. This often breakes Isabelle
+ overwritten by the user. This often broke Isabelle
packages. Antiquotations solve this problem, since they are ``linked''
statically at compile-time. However, this static linkage also limits their
usefulness in cases where data needs to be build up dynamically. In the
@@ -513,7 +516,7 @@
*}
-section {* Constructing Terms and Types Manually *}
+section {* Constructing Terms and Types Manually\label{sec:terms_types_manually} *}
text {*
While antiquotations are very convenient for constructing terms, they can
@@ -568,13 +571,13 @@
ML{*fun make_fun_type tau1 tau2 = Type ("fun",[tau1,tau2]) *}
-text {* This can be equally written as: *}
+text {* This can be equally written with the combinator @{ML "-->"} as: *}
ML{*fun make_fun_type tau1 tau2 = tau1 --> tau2 *}
text {*
A handy function for manipulating terms is @{ML map_types}: it takes a
- function and applies it to every type in the term. You can, for example,
+ function and applies it to every type in a term. You can, for example,
change every @{typ nat} in a term into an @{typ int} using the function:
*}
@@ -918,7 +921,7 @@
context (which we ignore in the code above) and a theorem (@{text thm}), and
returns another theorem (namely @{text thm} resolved with the lemma
@{thm [source] sym}: @{thm sym[no_vars]}). The function @{ML "Thm.rule_attribute"} then returns
- an attribute (of type @{ML_type "attribute"}).
+ an attribute.
Before we can use the attribute, we need to set it up. This can be done
using the function @{ML Attrib.add_attributes} as follows.
@@ -974,7 +977,7 @@
text {*
These functions take a theorem and a context and, for what we are explaining
- here it is sufficient to just return the context unchanged. They change
+ here it is sufficient that they just return the context unchanged. They change
however the reference @{ML my_thms}, whereby the function @{ML Thm.add_thm}
adds a theorem if it is not already included in the list, and @{ML
Thm.del_thm} deletes one. Both functions use the predicate @{ML
@@ -982,7 +985,7 @@
propositions (modulo alpha-equivalence).
- We can turn both functions into attributes using
+ You can turn both functions into attributes using
*}
ML{*val my_add = Thm.declaration_attribute my_thms_add
@@ -1009,7 +1012,7 @@
@{ML_response_fake [display,gray]
"!my_thms" "[\"True\"]"}
- We can also add theorems using the command \isacommand{declare}
+ You can also add theorems using the command \isacommand{declare}
*}
declare test[my_thms] trueI_2[my_thms add]
@@ -1030,7 +1033,7 @@
declare test[my_thms del]
-text {* After this, the theorem list is:
+text {* After this, the theorem list is again:
@{ML_response_fake [display,gray]
"!my_thms"
@@ -1040,7 +1043,7 @@
but there can be any number of them. We just have to change the parser for reading
the arguments accordingly.
- However, as said at the beginning using references for storing theorems is
+ However, as said at the beginning of this example, using references for storing theorems is
\emph{not} the received way of doing such things. The received way is to
start a ``data slot'' in a context by using the functor @{text GenericDataFun}:
*}
@@ -1052,7 +1055,7 @@
fun merge _ = Thm.merge_thms) *}
text {*
- To use this data slot, we only have to change the functions @{ML my_thms_add} and
+ To use this data slot, you only have to change @{ML my_thms_add} and
@{ML my_thms_del} to:
*}
@@ -1083,7 +1086,7 @@
modify the theorems.
Furthermore, the facts are made available on the user level under the dynamic
- fact name @{text foo}. For example we can declare three lemmas to be of the kind
+ fact name @{text foo}. For example you can declare three lemmas to be of the kind
@{text foo} by:
*}
@@ -1103,7 +1106,7 @@
@{text "> ?B"}
\end{isabelle}
- On the ML-level the rules marked with @{text "foo"} an be retrieved
+ On the ML-level the rules marked with @{text "foo"} can be retrieved
using the function @{ML FooRules.get}:
@{ML_response_fake [display,gray] "FooRules.get @{context}" "[\"?C\",\"?B\"]"}
@@ -1114,10 +1117,7 @@
data.
\end{readmore}
- (FIXME What are:
-
- @{text "theory_attributes"}
- @{text "proof_attributes"})
+ (FIXME What are: @{text "theory_attributes"}, @{text "proof_attributes"}?)
\begin{readmore}
--- a/CookBook/Intro.thy Mon Mar 02 10:06:06 2009 +0000
+++ b/CookBook/Intro.thy Tue Mar 03 13:00:55 2009 +0000
@@ -50,7 +50,7 @@
\item[The Isar Reference Manual] provides specification material (like grammars,
examples and so on) about Isar and its implementation. It is currently in
- the process of being updated. .
+ the process of being updated.
\end{description}
Then of course there is:
@@ -60,7 +60,7 @@
things really work. Therefore you should not hesitate to look at the
way things are actually implemented. More importantly, it is often
good to look at code that does similar things as you want to do and
- to learn from other people's code.
+ to learn from that code.
\end{description}
*}
@@ -108,6 +108,10 @@
Further information or pointers to files.
\end{readmore}
+ A few exercises a scattered around the text. Their solutions are given
+ in Appendix~\ref{ch:solutions}. Of course, you learn most, if you first try
+ to solve the exercises on your own.
+
*}
section {* Acknowledgements *}
@@ -115,7 +119,7 @@
text {*
Financial support for this tutorial was provided by the German
Research Council (DFG) under grant number URB 165/5-1. The following
- people contributed:
+ people contributed to the text:
\begin{itemize}
\item {\bf Stefan Berghofer} wrote nearly all of the ML-code of the
--- a/CookBook/Parsing.thy Mon Mar 02 10:06:06 2009 +0000
+++ b/CookBook/Parsing.thy Tue Mar 03 13:00:55 2009 +0000
@@ -11,7 +11,7 @@
Theory commands, such as \isacommand{definition}, \isacommand{inductive} and so
on, belong to the outer syntax, whereas items inside double quotation marks, such
as terms, types and so on, belong to the inner syntax. For parsing inner syntax,
- Isabelle uses a rather general and sophisticated algorithm due to Earley, which
+ 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}.
@@ -348,7 +348,7 @@
text {*
Most of the time, however, Isabelle developers have to deal with parsing
- tokens, not strings. These token parsers will have the type:
+ tokens, not strings. These token parsers have the type:
*}
ML{*type 'a parser = OuterLex.token list -> 'a * OuterLex.token list*}
@@ -601,7 +601,7 @@
text {*
There are a number of special purpose parsers that help with parsing
- specifications of functions, inductive definitions and so on. In
+ specifications of function definitions, inductive predicates and so on. In
Capter~\ref{chp:package}, for example, we will need to parse specifications
for inductive predicates of the form:
*}
@@ -613,6 +613,8 @@
| evenS: "odd n \<Longrightarrow> even (Suc n)"
| oddS: "even n \<Longrightarrow> odd (Suc n)"
+text {* and *}
+
simple_inductive
trcl\<iota> for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
where
@@ -692,8 +694,8 @@
*}
text {*
- Whenever types are given, they are stored in the @{ML SOME}s. They types are
- not yet given to the variable: this must be done by type inference later
+ Whenever types are given, they are stored in the @{ML SOME}s. The types are
+ not yet used to type the variables: this must be done by type-inference later
on. Since types are part of the inner syntax they are strings with some
encoded information (see previous section). If a syntax translation is
present for a variable, then it is stored in the @{ML Mixfix} datastructure;
@@ -853,7 +855,7 @@
@{text [display] "$ ISABELLE_LOGS=\"$(isabelle getenv -b ISABELLE_OUTPUT)\"/log"}
- on the Unix prompt. If you now also type @{text "ls $ISABELLE_LOGS"}, then the
+ on the Unix prompt. If you now type @{text "ls $ISABELLE_LOGS"}, then the
directory should include the files:
@{text [display]
--- a/CookBook/Solutions.thy Mon Mar 02 10:06:06 2009 +0000
+++ b/CookBook/Solutions.thy Tue Mar 03 13:00:55 2009 +0000
@@ -3,7 +3,7 @@
uses "infix_conv.ML"
begin
-chapter {* Solutions to Most Exercises *}
+chapter {* Solutions to Most Exercises\label{ch:solutions} *}
text {* \solution{fun:revsum} *}
--- a/CookBook/Tactical.thy Mon Mar 02 10:06:06 2009 +0000
+++ b/CookBook/Tactical.thy Tue Mar 03 13:00:55 2009 +0000
@@ -289,8 +289,8 @@
printed by the Isabelle system and by @{ML my_print_tac}. The latter shows
the goal state as represented internally (highlighted boxes). This
illustrates that every goal state in Isabelle is represented by a theorem:
- when we start the proof of \mbox{@{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}} the theorem is
- @{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}; when we finish the proof the
+ when you start the proof of \mbox{@{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}} the theorem is
+ @{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}; when you finish the proof the
theorem is @{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}.\label{fig:goalstates}}
\end{figure}
*}
@@ -328,8 +328,9 @@
text {*
Let us start with the tactic @{ML print_tac}, which is quite useful for low-level
- debugging of tactics. It just prints out a message and the current goal state.
- Processing the proof
+ debugging of tactics. It just prints out a message and the current goal state
+ (unlike @{ML my_print_tac} it prints the goal state as the user would see it).
+ For example, processing the proof
*}
lemma shows "False \<Longrightarrow> True"
@@ -386,7 +387,7 @@
text {*
Note the number in each tactic call. Also as mentioned in the previous section, most
- basic tactics take such an argument; it addresses the subgoal they are analysing.
+ basic tactics take such a number as argument; it addresses the subgoal they are analysing.
In the proof below, we first split up the conjunction in the second subgoal by
focusing on this subgoal first.
*}
@@ -692,10 +693,12 @@
construct the patterns, the pattern in Line 8 cannot be constructed in this
way. The reason is that an antiquotation would fix the type of the
quantified variable. So you really have to construct the pattern using the
- basic term-constructors. This is not necessary in other cases, because their type
- is always fixed to function types involving only the type @{typ bool}. For the
- final pattern, we chose to just return @{ML all_tac}. Consequently,
- @{ML select_tac} never fails.
+ basic term-constructors. This is not necessary in other cases, because their
+ type is always fixed to function types involving only the type @{typ
+ bool}. (See Section \ref{sec:terms_types_manually} about constructing terms
+ manually.) For the catch-all pattern, we chose to just return @{ML all_tac}.
+ Consequently, @{ML select_tac} never fails.
+
Let us now see how to apply this tactic. Consider the four goals:
*}
@@ -924,7 +927,7 @@
@{ML REPEAT1} is similar, but runs the tactic at least once (failing if
this is not possible).
- If you are after the ``primed'' version of @{ML repeat_xmp} then you
+ If you are after the ``primed'' version of @{ML repeat_xmp}, then you
need to implement it as
*}
Binary file cookbook.pdf has changed