--- a/ProgTutorial/FirstSteps.thy Mon Mar 23 18:28:41 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy Mon Mar 23 18:35:58 2009 +0100
@@ -89,7 +89,7 @@
@{ML_response_fake [display,gray] "warning (makestring 1)" "\"1\""}
- However @{ML makestring} only works if the type of what is converted is monomorphic
+ However, @{ML makestring} only works if the type of what is converted is monomorphic
and not a function.
The function @{ML "warning"} should only be used for testing purposes, because any
@@ -101,7 +101,7 @@
@{ML_response_fake [display,gray] "tracing \"foo\"" "\"foo\""}
It is also possible to redirect the ``channel'' where the string @{text "foo"} is
- printed to a separate file, e.g.~to prevent ProofGeneral from choking on massive
+ printed to a separate file, e.g., to prevent ProofGeneral from choking on massive
amounts of trace output. This redirection can be achieved with the code:
*}
@@ -260,7 +260,7 @@
|> (fn x => x + 4)*}
text {*
- which increments its argument @{text x} by 5. It does this by first incrementing
+ which increments its argument @{text x} by 5. It proceeds 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
@@ -361,9 +361,9 @@
cannot be merged back into the ``main waterfall''. To do this, you can use
the next combinator.
- The combinator @{ML "`"} 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
+ The combinator @{ML "`"} (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
*}
ML{*fun inc_as_pair x =
@@ -405,7 +405,8 @@
|-> (fn x => fn y => x + y)*}
text {*
- Recall that @{ML "|>"} is the reverse function applications. Recall also that the related
+ Recall that @{ML "|>"} is the reverse function application. Recall also that
+ the related
reverse function composition is @{ML "#>"}. In fact all the combinators @{ML "|->"},
@{ML "|>>"} and @{ML "||>"} described above have related combinators for function
composition, namely @{ML "#->"}, @{ML "#>>"} and @{ML "##>"}. Using @{ML "#->"},
@@ -421,7 +422,8 @@
(FIXME: find a good exercise for combinators)
\begin{readmore}
- The most frequently used combinator are defined in the files @{ML_file "Pure/library.ML"}
+ The most frequently used combinators are defined in the files @{ML_file
+ "Pure/library.ML"}
and @{ML_file "Pure/General/basics.ML"}. Also \isccite{sec:ML-linear-trans}
contains further information about combinators.
\end{readmore}
@@ -495,11 +497,11 @@
"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
+ Again, this way of referencing simpsets makes you independent from additions
of lemmas to the simpset by the user that potentially cause loops.
On the ML-level of Isabelle, you often have to work with qualified names;
- these are strings with some additional information, such positional information
+ these are strings with some additional information, such as positional information
and qualifiers. Such bindings can be generated with the antiquotation
@{text "@{binding \<dots>}"}.
@@ -507,8 +509,9 @@
"@{binding \"name\"}"
"name"}
- An example where a binding is needed is the function @{ML define in LocalTheory}.
- Below this function defines the constant @{term "TrueConj"} as the conjunction
+ An example where a binding is needed is the function @{ML define in
+ LocalTheory}. Below, this function is used to define the constant @{term
+ "TrueConj"} as the conjunction
@{term "True \<and> True"}.
*}
@@ -517,6 +520,7 @@
((@{binding "TrueConj"}, NoSyn),
(Attrib.empty_binding, @{term "True \<and> True"})) *}
+<<<<<<< local
text {*
Now querying the definition you obtain:
@@ -528,27 +532,27 @@
(FIXME give a better example why bindings are important; maybe
give a pointer to \isacommand{local\_setup})
- While antiquotations have many applications, they were originally introduced in order
- to avoid explicit bindings for theorems such as:
+ While antiquotations have many applications, they were originally introduced
+ in order to avoid explicit bindings of theorems such as:
*}
ML{*val allI = thm "allI" *}
text {*
- These bindings are difficult to maintain and also can be accidentally
- overwritten by the user. This often broke Isabelle
+ Such bindings are difficult to maintain and can be overwritten by the
+ user accidentally. 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
- course of this chapter you will learn more about these antiquotations:
+ usefulness in cases where data needs to be built up dynamically. In the
+ course of this chapter you will learn more about antiquotations:
they can simplify Isabelle programming since one can directly access all
- kinds of logical elements from th ML-level.
+ kinds of logical elements from the ML-level.
*}
section {* Terms and Types *}
text {*
- One way to construct terms of Isabelle is by using the antiquotation
+ One way to construct Isabelle terms, is by using the antiquotation
\mbox{@{text "@{term \<dots>}"}}. For example:
@{ML_response [display,gray]
@@ -556,16 +560,16 @@
"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
- datatype @{ML_type "term"}.
+ will show the term @{term "(a::nat) + b = c"}, but printed using an internal
+ representation corresponding to the data type @{ML_type "term"}.
- The internal representation of terms uses the usual de Bruijn index mechanism where bound
- variables are represented by the constructor @{ML Bound}. The index in @{ML Bound} refers to
- the number of Abstractions (@{ML Abs}) we have to skip until we hit the @{ML Abs} that
- binds the corresponding variable. However, in Isabelle the names of bound variables are
- kept at abstractions for printing purposes, and so should be treated only as ``comments''.
- Application in Isabelle is realised with the term-constructor @{ML $}.
+ This internal representation uses the usual de Bruijn index mechanism---where
+ bound variables are represented by the constructor @{ML Bound}. The index in
+ @{ML Bound} refers to the number of Abstractions (@{ML Abs}) we have to skip
+ until we hit the @{ML Abs} that binds the corresponding variable. Note that
+ the names of bound variables are kept at abstractions for printing purposes,
+ and so should be treated only as ``comments''. Application in Isabelle is
+ realised with the term-constructor @{ML $}.
\begin{readmore}
Terms are described in detail in \isccite{sec:terms}. Their
@@ -679,8 +683,8 @@
(Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"}
There are a number of handy functions that are frequently used for
- constructing terms. One is the function @{ML list_comb}, which takes
- a term and a list of terms as arguments, and produces as output the term
+ constructing terms. One is the function @{ML list_comb}, which takes a term
+ and a list of terms as arguments, and produces as output the term
list applied to the term. For example
@{ML_response_fake [display,gray]
@@ -746,7 +750,7 @@
\begin{exercise}\label{fun:makesum}
Write a function which takes two terms representing natural numbers
- in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produce the
+ in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produces the
number representing their sum.
\end{exercise}
@@ -808,7 +812,7 @@
@{ML_response [display,gray] "@{term \"Nil\"}" "Const (\"List.list.Nil\", \<dots>)"}
the name of the constant @{text "Nil"} depends on the theory in which the
- term constructor is defined (@{text "List"}) and also in which datatype
+ term constructor is defined (@{text "List"}) and also in which data type
(@{text "list"}). Even worse, some constants have a name involving
type-classes. Consider for example the constants for @{term "zero"} and
\mbox{@{text "(op *)"}}:
@@ -820,10 +824,10 @@
While you could use the complete name, for example
@{ML "Const (\"List.list.Nil\", some_type)" for some_type}, for referring to or
matching against @{text "Nil"}, this would make the code rather brittle.
- The reason is that the theory and the name of the datatype can easily change.
+ The reason is that the theory and the name of the data type can easily change.
To make the code more robust, it is better to use the antiquotation
@{text "@{const_name \<dots>}"}. With this antiquotation you can harness the
- variable parts of the constant's name. Therefore a functions for
+ variable parts of the constant's name. Therefore a function for
matching against constants that have a polymorphic type should
be written as follows.
*}
@@ -833,7 +837,7 @@
| is_nil_or_all _ = false *}
text {*
- Occasional you have to calculate what the ``base'' name of a given
+ Occasionally you have to calculate what the ``base'' name of a given
constant is. For this you can use the function @{ML Sign.extern_const} or
@{ML Long_Name.base_name}. For example:
@@ -874,7 +878,7 @@
| _ => t)*}
text {*
- An example as follows:
+ Here is an example:
@{ML_response_fake [display,gray]
"map_types nat_to_int @{term \"a = (1::nat)\"}"
@@ -943,7 +947,7 @@
result that type-checks.
\end{exercise}
- Remember Isabelle follows the Church-style typing for terms, i.e.~a term contains
+ Remember Isabelle follows the Church-style typing for terms, i.e., a term contains
enough typing information (constants, free variables and abstractions all have typing
information) so that it is always clear what the type of a term is.
Given a well-typed term, the function @{ML type_of} returns the
@@ -993,12 +997,12 @@
Const (\"HOL.one_class.one\", \"nat\") $ Free (\"x\", \"nat\")"}
Instead of giving explicitly the type for the constant @{text "plus"} and the free
- variable @{text "x"}, the type-inference fills in the missing information.
+ variable @{text "x"}, type-inference fills in the missing information.
\begin{readmore}
See @{ML_file "Pure/Syntax/syntax.ML"} where more functions about reading,
- checking and pretty-printing of terms are defined. Functions related to the
- type inference are implemented in @{ML_file "Pure/type.ML"} and
+ checking and pretty-printing of terms are defined. Functions related to
+ type-inference are implemented in @{ML_file "Pure/type.ML"} and
@{ML_file "Pure/type_infer.ML"}.
\end{readmore}
@@ -1010,7 +1014,7 @@
text {*
Just like @{ML_type cterm}s, theorems are abstract objects of type @{ML_type thm}
- that can only be build by going through interfaces. As a consequence, every proof
+ that can only be built by going through interfaces. As a consequence, every proof
in Isabelle is correct by construction. This follows the tradition of the LCF approach
\cite{GordonMilnerWadsworth79}.
@@ -1081,7 +1085,7 @@
theorem is proved. In particular, it is not possible to find out
what are all theorems that have a given attribute in common, unless of course
the function behind the attribute stores the theorems in a retrievable
- datastructure.
+ data structure.
If you want to print out all currently known attributes a theorem can have,
you can use the Isabelle command
@@ -1439,7 +1443,7 @@
text {*
In the previous section we used \isacommand{setup} in order to make
a theorem attribute known to Isabelle. What happens behind the scenes
- is that \isacommand{setup} expects a functions of type
+ is that \isacommand{setup} expects a function of type
@{ML_type "theory -> theory"}: the input theory is the current theory and the
output the theory where the theory attribute has been stored.
@@ -1495,7 +1499,7 @@
In contrast to an ordinary theory, which simply consists of a type
signature, as well as tables for constants, axioms and theorems, a local
- theory also contains additional context information, such as locally fixed
+ theory contains additional context information, such as locally fixed
variables and local assumptions that may be used by the package. The type
@{ML_type local_theory} is identical to the type of \emph{proof contexts}
@{ML_type "Proof.context"}, although not every proof context constitutes a
@@ -1549,4 +1553,4 @@
ML {*DatatypePackage.get_datatype @{theory} "List.list"*}
-end
\ No newline at end of file
+end