--- a/ProgTutorial/FirstSteps.thy Wed Oct 14 14:56:19 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy Sun Oct 18 08:44:39 2009 +0200
@@ -20,7 +20,7 @@
more meticulous the paint job, the longer the tower shall endure.''} \\[1ex]
Gustave Eiffel, In his book {\em The 300-Meter Tower}.\footnote{The Eiffel Tower has been
re-painted 18 times since its initial construction, an average of once every
- seven years. It takes more than a year for a team of 25 painters to paint the tower
+ seven years. It takes more than one year for a team of 25 painters to paint the tower
from top to bottom.}
\end{flushright}
@@ -220,7 +220,7 @@
them (see Section \ref{sec:pretty}), but for quick-and-dirty solutions they
are a bit unwieldy. One way to transform a term into a string is to use the
function @{ML_ind string_of_term in Syntax} in the structure @{ML_struct
- Syntax}, which we bind for more convenience to the toplevel.
+ Syntax}. For more convenience, we bind this function to the toplevel.
*}
ML{*val string_of_term = Syntax.string_of_term*}
@@ -232,7 +232,7 @@
"string_of_term @{context} @{term \"1::nat\"}"
"\"\\^E\\^Fterm\\^E\\^E\\^Fconst\\^Fname=HOL.one_class.one\\^E1\\^E\\^F\\^E\\^E\\^F\\^E\""}
- This produces a string corrsponding to the term @{term [show_types] "1::nat"} with some
+ We obtain a string corrsponding to the term @{term [show_types] "1::nat"} with some
additional information encoded in it. The string can be properly printed by
using either the function @{ML_ind writeln} or @{ML_ind tracing}:
@@ -278,7 +278,7 @@
string_of_term ctxt (prop_of thm)*}
text {*
- Theorems also include schematic variables, such as @{text "?P"},
+ Theorems include schematic variables, such as @{text "?P"},
@{text "?Q"} and so on. They are needed in Isabelle in order to able to
instantiate theorems when they are applied. For example the theorem
@{thm [source] conjI} shown below can be used for any (typable)
@@ -321,9 +321,9 @@
commas (map (string_of_thm_no_vars ctxt) thms) *}
text {*
- Note, that when printing out several parcels of information that
- semantically belong together, like a warning message consisting for example
- of a term and a type, you should try to keep this information together in a
+ Note that when printing out several ``parcels'' of information that
+ semantically belong together, like a warning message consisting of
+ a term and its type, you should try to keep this information together in a
single string. Therefore do \emph{not} print out information as
@{ML_response_fake [display,gray]
@@ -349,6 +349,12 @@
Section \ref{sec:pretty} will also explain the infrastructure of Isabelle
that helps with more elaborate pretty printing.
+
+ \begin{readmore}
+ Most of the basic string functions of Isabelle are defined in
+ @{ML_file "Pure/library.ML"}.
+ \end{readmore}
+
*}
@@ -373,9 +379,8 @@
ML{*fun K x = fn _ => x*}
text {*
- @{ML K} ``wraps'' a function around the argument @{text "x"}. However, this
- function ignores its argument. As a result, @{ML K} defines a constant function
- always returning @{text x}.
+ @{ML K} ``wraps'' a function around @{text "x"} that ignores its argument. As a
+ result, @{ML K} defines a constant function always returning @{text x}.
The next combinator is reverse application, @{ML_ind "|>" in Basics}, defined as:
*}
@@ -393,7 +398,7 @@
|> (fn x => x + 4)*}
text {*
- which increments its argument @{text x} by 5. It proceeds by first incrementing
+ which increments its argument @{text x} by 5. It does this by first incrementing
the argument by 1 (Line 2); then storing the result in a pair (Line 3); taking
the first component of the pair (Line 4) and finally incrementing the first
component by 4 (Line 5). This kind of cascading manipulations of values is quite
@@ -425,7 +430,7 @@
avoided: it is more than easy to get the intermediate values wrong, not to
mention the nightmares the maintenance of this code causes!
- In Isabelle, a ``real world'' example for a function written in
+ In Isabelle a ``real world'' example for a function written in
the waterfall fashion might be the following code:
*}
@@ -496,7 +501,7 @@
increment-by-two, followed by increment-by-three. Again, the reverse function
composition allows you to read the code top-down.
- The remaining combinators described in this section add convenience for the
+ The remaining combinators we describe in this section add convenience for the
``waterfall method'' of writing functions. The combinator @{ML_ind tap in
Basics} allows you to get hold of an intermediate result (to do some
side-calculations for instance). The function
@@ -510,14 +515,19 @@
text {*
increments the argument first by @{text "1"} and then by @{text "2"}. In the
middle (Line 3), however, it uses @{ML tap} for printing the ``plus-one''
- intermediate result inside the tracing buffer. The function @{ML tap} can
- only be used for side-calculations, because any value that is computed
- cannot be merged back into the ``main waterfall''. To do this, you can use
- the next combinator.
+ intermediate result. The function @{ML tap} can only be used for
+ side-calculations, because any value that is computed cannot be merged back
+ into the ``main waterfall''. To do this, you can use the next combinator.
The combinator @{ML_ind "`" in Basics} (a backtick) is similar to @{ML tap},
but applies a function to the value and returns the result together with the
- value (as a pair). For example the function
+ value (as a pair). It is defined as
+*}
+
+ML{*fun `f = fn x => (f x, x)*}
+
+text {*
+ An example for this combinator is the function
*}
ML{*fun inc_as_pair x =
@@ -525,7 +535,7 @@
|> (fn (x, y) => (x, y + 1))*}
text {*
- takes @{text x} as argument, and then increments @{text x}, but also keeps
+ which takes @{text x} as argument, and then increments @{text x}, but also keeps
@{text x}. The intermediate result is therefore the pair @{ML "(x + 1, x)"
for x}. After that, the function increments the right-hand component of the
pair. So finally the result will be @{ML "(x + 1, x + 1)" for x}.
@@ -561,7 +571,7 @@
end*}
text {*
- where however the return value of the recursive call is bound explicitly to
+ where the return value of the recursive call is bound explicitly to
the pair @{ML "(los, grs)" for los grs}. You can implement this function
more concisely as
*}
@@ -645,11 +655,11 @@
sometimes necessary to do some ``plumbing'' in order to fit functions
together. We have already seen such plumbing in the function @{ML
apply_fresh_args}, where @{ML curry} is needed for making the function @{ML
- list_comb} that works over pairs to fit with the combinator @{ML "|>"}. Such
+ list_comb}, which works over pairs to fit with the combinator @{ML "|>"}. Such
plumbing is also needed in situations where a function operate over lists,
but one calculates only with a single element. An example is the function
- @{ML_ind check_terms in Syntax}, whose purpose is to type-check a list
- of terms. Consider the code:
+ @{ML_ind check_terms in Syntax}, whose purpose is to simultaneously type-check
+ a list of terms. Consider the code:
@{ML_response_fake [display, gray]
"let
@@ -712,7 +722,7 @@
therefore we are not interested in them in this Tutorial, except in Appendix
\ref{rec:docantiquotations} where we show how to implement your own document
antiquotations.} For example, one can print out the name of the current
- theory by typing
+ theory with the code
@{ML_response [display,gray] "Context.theory_name @{theory}" "\"FirstSteps\""}
@@ -777,7 +787,7 @@
"[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}
Again, this way of referencing simpsets makes you independent from additions
- of lemmas to the simpset by the user that can potentially cause loops in your
+ of lemmas to the simpset by the user, which can potentially cause loops in your
code.
On the ML-level of Isabelle, you often have to work with qualified names.
@@ -820,13 +830,13 @@
It is also possible to define your own antiquotations. But you should
exercise care when introducing new ones, as they can also make your code
- also difficult to read. In the next chapter we will see how the (build in)
- antiquotation @{text "@{term \<dots>}"} can be used to construct terms. A
+ also difficult to read. In the next chapter we describe how the (build in)
+ antiquotation @{text "@{term \<dots>}"} for constructing terms. A
restriction of this antiquotation is that it does not allow you to use
- schematic variables. If you want to have an antiquotation that does not have
+ schematic variables in terms. If you want to have an antiquotation that does not have
this restriction, you can implement your own using the function @{ML_ind
- inline in ML_Antiquote}. The code for the antiquotation @{text "term_pat"} is
- as follows.
+ inline in ML_Antiquote} in the structure @{ML_struct ML_Antiquote}. The code
+ for the antiquotation @{text "term_pat"} is as follows.
*}
ML %linenosgray{*let
@@ -844,19 +854,13 @@
The parser in Line 2 provides us with a context and a string; this string is
transformed into a term using the function @{ML_ind read_term_pattern in
ProofContext} (Line 5); the next two lines transform the term into a string
- so that the ML-system can understand it. An example for the usage
- of this antiquotation is:
+ so that the ML-system can understand it. An example for this antiquotation is:
@{ML_response_fake [display,gray]
"@{term_pat \"Suc (?x::nat)\"}"
"Const (\"Suc\", \"nat \<Rightarrow> nat\") $ Var ((\"x\", 0), \"nat\")"}
which shows the internal representation of the term @{text "Suc ?x"}.
- This is different from the build-in @{text "@{term \<dots>}"}-antiquotation.
-
- @{ML_response_fake [display,gray]
- "@{term \"Suc (x::nat)\"}"
- "Const (\"Suc\", \"nat \<Rightarrow> nat\") $ Free (\"x\", \"nat\")"}
\begin{readmore}
The file @{ML_file "Pure/ML/ml_antiquote.ML"} contains the the definitions
@@ -870,12 +874,12 @@
text {*
Isabelle provides mechanisms for storing (and retrieving) arbitrary
data. Before we delve into the details, let us digress a bit. Conventional
- wisdom has it that the type-system of ML ensures that for example an
- @{ML_type "'a list"} can only hold elements of the same type, namely
+ wisdom has it that the type-system of ML ensures that an
+ @{ML_type "'a list"}, say, can only hold elements of the same type, namely
@{ML_type "'a"}. Despite this wisdom, however, it is possible to implement a
universal type in ML, although by some arguably accidental features of ML.
This universal type can be used to store data of different type into a single list.
- It allows one to inject and to project data of \emph{arbitrary} type. This is
+ In fact, it allows one to inject and to project data of \emph{arbitrary} type. This is
in contrast to datatypes, which only allow injection and projection of data for
some fixed collection of types. In light of the conventional wisdom cited
above it is important to keep in mind that the universal type does not
@@ -890,7 +894,7 @@
We will show the usage of the universal type by storing an integer and
a boolean into a single list. Let us first define injection and projection
- functions for booleans and integers into and from @{ML_type Universal.universal}.
+ functions for booleans and integers into and from the type @{ML_type Universal.universal}.
*}
ML{*local
@@ -937,22 +941,22 @@
Now, Isabelle heavily uses this mechanism for storing all sorts of
data: theorem lists, simpsets, facts etc. Roughly speaking, there are two
- places where data can be stored: in \emph{theories} and in \emph{proof
- contexts}. Again roughly speaking, data such as simpsets need to be stored
+ places where data can be stored in Isabelle: in \emph{theories} and in \emph{proof
+ contexts}. Data such as simpsets need to be stored
in a theory, since they need to be maintained across proofs and even across
theories. On the other hand, data such as facts change inside a proof and
are only relevant to the proof at hand. Therefore such data needs to be
- maintained inside a proof context.\footnote{\bf TODO: explain more about
- this in a separate section.}
+ maintained inside a proof context.
For theories and proof contexts there are, respectively, the functors
@{ML_funct_ind TheoryDataFun} and @{ML_funct_ind ProofDataFun} that help
with the data storage. Below we show how to implement a table in which we
can store theorems and look them up according to a string key. The
- intention is to be able to look up introduction rules for logical
+ intention in this example is to be able to look up introduction rules for logical
connectives. Such a table might be useful in an automatic proof procedure
- and therefore it makes sense to store this data inside a theory. The code
- for the table is:
+ and therefore it makes sense to store this data inside a theory.
+ Therefore we use the functor @{ML_funct TheoryDataFun}.
+ The code for the table is:
*}
ML %linenosgray{*structure Data = TheoryDataFun
@@ -964,17 +968,19 @@
text {*
In order to store data in a theory, we have to specify the type of the data
- (Line 2). In this case we specify the type @{ML_type "thm Symtab.table"}, which
- stands for tables in which @{ML_type string}s can be looked up producing an associated
- @{ML_type thm}. We also have to specify four functions: how to initialise
- the data storage (Line 3), how to copy it (Line 4), how to extend it (Line
- 5) and how two tables should be merged (Line 6). These functions correspond
- roughly to the operations performed on theories.\footnote{\bf FIXME: Say more
- about the assumptions of these operations.} The result structure @{ML_text Data}
+ (Line 2). In this case we specify the type @{ML_type "thm Symtab.table"},
+ which stands for a table in which @{ML_type string}s can be looked up
+ producing an associated @{ML_type thm}. We also have to specify four
+ functions to use this functor: namely how to initialise the data storage
+ (Line 3), how to copy it (Line 4), how to extend it (Line 5) and how two
+ tables should be merged (Line 6). These functions correspond roughly to the
+ operations performed on theories and we just give some sensible
+ defaults\footnote{\bf FIXME: Say more about the
+ assumptions of these operations.} The result structure @{ML_text Data}
contains functions for accessing the table (@{ML Data.get}) and for updating
- it (@{ML Data.map}). There are also two more functions (@{ML Data.init} and
- @{ML Data.put}), which however we ignore here. Below we define two auxiliary
- functions, which help us with accessing the table.
+ it (@{ML Data.map}). There are also two more functions (@{ML Data.init} and
+ @{ML Data.put}), which however are not relevant here. Below we define two
+ auxiliary functions, which help us with accessing the table.
*}
ML{*val lookup = Symtab.lookup o Data.get
@@ -993,8 +999,8 @@
text {*
The use of the command \isacommand{setup} makes sure the table in the
- \emph{current} theory is updated. The lookup can now be performed as
- follows.
+ \emph{current} theory is updated (this is explained further in
+ section~\ref{sec:theories}). The lookup can now be performed as follows.
@{ML_response_fake [display, gray]
"lookup @{theory} \"op &\""
@@ -1008,16 +1014,16 @@
setup %gray {* update "op &" @{thm TrueI} *}
text {*
- and @{ML lookup} now produces the introduction rule for @{term "True"}
+ and accordingly, @{ML lookup} now produces the introduction rule for @{term "True"}
@{ML_response_fake [display, gray]
"lookup @{theory} \"op &\""
"SOME \"True\""}
there are no references involved. This is one of the most fundamental
- coding conventions for programming in Isabelle. References would
+ coding conventions for programming in Isabelle. References
interfere with the multithreaded execution model of Isabelle and also
- defeat its undo-mechanism in proof scripts. For this consider the
+ defeat its undo-mechanism. To see the latter, consider the
following data container where we maintain a reference to a list of
integers.
*}
@@ -1045,7 +1051,7 @@
text {*
which takes an integer and adds it to the content of the reference.
- As done above, we update the reference with the command
+ As before, we update the reference with the command
\isacommand{setup}.
*}
@@ -1060,7 +1066,7 @@
"ref [1]"}
So far everything is as expected. But, the trouble starts if we attempt to
- backtrack to the point ``before'' the \isacommand{setup}-command. There, we
+ backtrack to the ``point'' before the \isacommand{setup}-command. There, we
would expect that the list is empty again. But since it is stored in a
reference, Isabelle has no control over it. So it is not empty, but still
@{ML "ref [1]" in Unsynchronized}. Adding to the trouble, if we execute the
@@ -1084,9 +1090,9 @@
tables and symtables in @{ML_file "Pure/General/table.ML"}.
\end{readmore}
- Storing data in a proof context is done in a similar fashion. The
- corresponding functor is @{ML_funct_ind ProofDataFun}. With the
- following code we can store a list of terms in a proof context.
+ Storing data in a proof context is done in a similar fashion. As mentioned
+ before, the corresponding functor is @{ML_funct_ind ProofDataFun}. With the
+ following code we can store a list of terms in a proof context.
*}
ML{*structure Data = ProofDataFun
@@ -1095,7 +1101,7 @@
text {*
The function we have to specify has to produce a list once a context
- is initialised (taking the theory into account from which the
+ is initialised (possibly taking the theory into account from which the
context is derived). We choose to just return the empty list. Next
we define two auxiliary functions for updating the list with a given
term and printing the list.
@@ -1140,8 +1146,8 @@
theories, and therefore one can access the data potentially
indefinitely.
- For convenience there is an abstract layer, the type @{ML_type Context.generic},
- for theories and proof contexts. This type is defined as follows
+ For convenience there is an abstract layer, namely the type @{ML_type Context.generic},
+ for treating theories and proof contexts more uniformly. This type is defined as follows
*}
ML_val{*datatype generic =
@@ -1149,13 +1155,12 @@
| Proof of proof*}
text {*
- For this type a number of operations are defined which allow the
- uniform treatment of theories and proof contexts.
+ \footnote{\bf FIXME: say more about generic contexts.}
There are two special instances of the data storage mechanism described
- above. The first instance are named theorem lists. Since storing theorems in a list
- is such a common task, there is the special functor @{ML_funct_ind Named_Thms}.
- To obtain a named theorem list, you just declare
+ above. The first instance implements named theorem lists using the functor
+ @{ML_funct_ind Named_Thms}. This is because storing theorems in a list
+ is such a common task. To obtain a named theorem list, you just declare
*}
ML{*structure FooRules = Named_Thms
@@ -1173,10 +1178,9 @@
an attribute @{text foo} (with the @{text add} and @{text del} options
for adding and deleting theorems) and an internal ML-interface to retrieve and
modify the theorems.
-
- Furthermore, the facts are made available on the user-level under the dynamic
- fact name @{text foo}. For example you can declare three lemmas to be of the kind
- @{text foo} by:
+ Furthermore, the theorems are made available on the user-level under the name
+ @{text foo}. For example you can declare three lemmas to be a member of the
+ theorem list @{text foo} by:
*}
lemma rule1[foo]: "A" sorry
@@ -1187,7 +1191,7 @@
declare rule1[foo del]
-text {* and query the remaining ones with:
+text {* You can query the remaining ones with:
\begin{isabelle}
\isacommand{thm}~@{text "foo"}\\
@@ -1209,8 +1213,8 @@
"[\"True\", \"?C\",\"?B\"]"}
Note that this function takes a proof context as argument. This might be
- confusing, since the theorem list is stored as theory data. The proof context
- however conatains the information about the current theory and so the function
+ confusing, since the theorem list is stored as theory data. It becomes clear by knowing
+ that the proof context contains the information about the current theory and so the function
can access the theorem list in the theory via the context.
\begin{readmore}
@@ -1272,7 +1276,9 @@
val ctxt' = Config.put sval \"foo\" ctxt
val ctxt'' = Config.put sval \"bar\" ctxt'
in
- (Config.get ctxt sval, Config.get ctxt' sval, Config.get ctxt'' sval)
+ (Config.get ctxt sval,
+ Config.get ctxt' sval,
+ Config.get ctxt'' sval)
end"
"(\"some string\", \"foo\", \"bar\")"}
@@ -1296,7 +1302,7 @@
\begin{conventions}
\begin{itemize}
\item Print messages that belong together as a single string.
- \item Do not use references in any Isabelle code.
+ \item Do not use references in Isabelle code.
\end{itemize}
\end{conventions}