--- 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}
--- a/ProgTutorial/General.thy Wed Oct 14 14:56:19 2009 +0200
+++ b/ProgTutorial/General.thy Sun Oct 18 08:44:39 2009 +0200
@@ -17,16 +17,16 @@
Isabelle is build around a few central ideas. One central idea is the
LCF-approach to theorem proving where there is a small trusted core and
everything else is build on top of this trusted core. The fundamental data
- structures involved in this core are certified terms and types, as well as
- theorems.
+ structures involved in this core are certified terms and certified types,
+ as well as theorems.
*}
section {* Terms and Types *}
text {*
- There are certified terms and uncertified terms (respectively types).
- Uncertified terms are just called terms. One way to construct them is by
+ In Isabelle, there are certified terms and uncertified terms (respectively types).
+ Uncertified terms are often just called terms. One way to construct them is by
using the antiquotation \mbox{@{text "@{term \<dots>}"}}. For example
@{ML_response [display,gray]
@@ -34,8 +34,9 @@
"Const (\"op =\", \<dots>) $
(Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
- constructs the term @{term "(a::nat) + b = c"}, but it printed using the internal
- representation corresponding to the datatype @{ML_type_ind "term"} defined as follows:
+ constructs the term @{term "(a::nat) + b = c"}. The resulting term is printed using
+ the internal representation corresponding to the datatype @{ML_type_ind "term"},
+ which is defined as follows:
*}
ML_val %linenosgray{*datatype term =
@@ -48,7 +49,7 @@
text {*
This datatype implements Church-style lambda-terms, where types are
- explicitly recorded in the variables, constants and abstractions. As can be
+ explicitly recorded in variables, constants and abstractions. As can be
seen in Line 5, terms use the usual de Bruijn index mechanism for
representing bound variables. For example in
@@ -153,7 +154,7 @@
where it is not (since it is already constructed by a meta-implication).
The purpose of the @{text "Trueprop"}-coercion is to embed formulae of
- an object logic, for example HOL, into the meta-logic of Isabelle. It
+ an object logic, for example HOL, into the meta-logic of Isabelle. The coercion
is needed whenever a term is constructed that will be proved as a theorem.
As already seen above, types can be constructed using the antiquotation
@@ -171,7 +172,7 @@
text {*
Like with terms, there is the distinction between free type
- variables (term-constructor @{ML "TFree"} and schematic
+ variables (term-constructor @{ML "TFree"}) and schematic
type variables (term-constructor @{ML "TVar"}). A type constant,
like @{typ "int"} or @{typ bool}, are types with an empty list
of argument types. However, it is a bit difficult to show an
@@ -236,7 +237,7 @@
There are a number of handy functions that are frequently used for
constructing terms. One is the function @{ML_ind list_comb in Term}, which
- takes a term and a list of terms as arguments, and produces as output the
+ takes as argument a term and a list of terms, and produces as output the
term list applied to the term. For example
@@ -262,7 +263,7 @@
"Abs (\"x\", \"nat\", Free (\"P\", \"bool \<Rightarrow> bool\") $ Bound 0)"}
In this example, @{ML lambda} produces a de Bruijn index (i.e.~@{ML "Bound 0"}),
- and an abstraction. It also records the type of the abstracted
+ and an abstraction, where it also records the type of the abstracted
variable and for printing purposes also its name. Note that because of the
typing annotation on @{text "P"}, the variable @{text "x"} in @{text "P x"}
is of the same type as the abstracted variable. If it is of different type,
@@ -320,7 +321,7 @@
text {*
The function returns a pair consisting of the stripped off variables and
- the body of the universal quantifications. For example
+ the body of the universal quantification. For example
@{ML_response_fake [display, gray]
"strip_alls @{term \"\<forall>x y. x = (y::bool)\"}"
@@ -346,7 +347,8 @@
takes is the replacement for @{ML "Bound 0"}, the next element for @{ML "Bound 1"}
and so on.
- There are many convenient functions that construct specific HOL-terms. For
+ There are also many convenient functions that construct specific HOL-terms
+ in the structure @{ML_struct HOLogic}. For
example @{ML_ind mk_eq in HOLogic} constructs an equality out of two terms.
The types needed in this equality are calculated from the type of the
arguments. For example
@@ -545,14 +547,13 @@
\end{exercise}
\begin{exercise}\label{fun:makesum}
- Write a function which takes two terms representing natural numbers
+ Write a function that takes two terms representing natural numbers
in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produces the
number representing their sum.
\end{exercise}
\begin{exercise}\label{ex:debruijn}
- Implement the function, which we below name deBruijn\footnote{According to
- personal communication of de Bruijn to Dyckhoff.}, that depends on a natural
+ Implement the function, which we below name deBruijn, that depends on a natural
number n$>$0 and constructs terms of the form:
\begin{center}
@@ -575,7 +576,8 @@
\end{center}
Make sure you use the functions defined in @{ML_file "HOL/Tools/hologic.ML"}
- for constructing the terms for the logical connectives.
+ for constructing the terms for the logical connectives.\footnote{Thanks to Roy
+ Dyckhoff for this exercise.}
\end{exercise}
*}
@@ -1382,7 +1384,7 @@
the current simpset.
*}
-section {* Theories (TBD) *}
+section {* Theories\label{sec:theories} (TBD) *}
text {*
There are theories, proof contexts and local theories (in this order, if you