--- a/ProgTutorial/FirstSteps.thy Sun May 17 16:22:27 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy Mon May 18 05:21:40 2009 +0200
@@ -144,7 +144,7 @@
"Exception- ERROR \"foo\" raised
At command \"ML\"."}
- (FIXME @{ML Toplevel.debug} @{ML Toplevel.profiling})
+ (FIXME Mention how to work with @{ML Toplevel.debug} and @{ML Toplevel.profiling}.)
*}
(*
@@ -163,7 +163,8 @@
text {*
Most often you want to inspect data of type @{ML_type term}, @{ML_type cterm}
- or @{ML_type thm}. Isabelle contains elaborate pretty-printing functions for printing them,
+ or @{ML_type thm}. Isabelle contains elaborate pretty-printing functions for printing
+ them (see Section \ref{sec:pretty}),
but for quick-and-dirty solutions they are far too unwieldy. A simple way to transform
a term into a string is to use the function @{ML Syntax.string_of_term}.
@@ -479,7 +480,7 @@
contains further information about combinators.
\end{readmore}
- (FIXME: say something abou calling conventions)
+ (FIXME: say something about calling conventions)
*}
@@ -552,8 +553,8 @@
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 as positional information
+ On the ML-level of Isabelle, you often have to work with qualified names.
+ These are strings with some additional information, such as positional information
and qualifiers. Such qualified names can be generated with the antiquotation
@{text "@{binding \<dots>}"}.
@@ -562,7 +563,7 @@
"name"}
An example where a binding is needed is the function @{ML define in
- LocalTheory}. Below, this function is used to define the constant @{term
+ LocalTheory}. This function is below used to define the constant @{term
"TrueConj"} as the conjunction
@{term "True \<and> True"}.
*}
@@ -613,16 +614,10 @@
(Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
will show the term @{term "(a::nat) + b = c"}, but printed using the internal
- representation corresponding to the datatype @{ML_type "term"}. Since Isabelle
- uses Church-style terms, the datatype @{ML_type term} must be defined in
- conjunction with types, that is the datatype @{ML_type typ}:
+ representation corresponding to the datatype @{ML_type "term"} defined as follows:
*}
-ML_val{*datatype typ =
- Type of string * typ list
-| TFree of string * sort
-| TVar of indexname * sort
-datatype term =
+ML_val{*datatype term =
Const of string * typ
| Free of string * typ
| Var of indexname * typ
@@ -631,15 +626,15 @@
| $ of term * term *}
text {*
- The datatype for terms uses the usual de Bruijn index mechanism---where
- bound variables are represented by the constructor @{ML Bound}.
+ Terms use the usual de Bruijn index mechanism---where
+ bound variables are represented by the constructor @{ML Bound}. For
+ example in
@{ML_response_fake [display, gray]
"@{term \"\<lambda>x y. x y\"}"
"Abs (\"x\", \"'a \<Rightarrow> 'b\", Abs (\"y\", \"'a\", Bound 1 $ Bound 0))"}
- The index in
- @{ML Bound} refers to the number of Abstractions (@{ML Abs}) we have to skip
+ the indices refer to the number of Abstractions (@{ML Abs}) that we need 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
@@ -647,13 +642,13 @@
Isabelle makes a distinction between \emph{free} variables (term-constructor @{ML Free})
and variables (term-constructor @{ML Var}). The latter correspond to the schematic
- variables that show up with a question mark in front of them. Consider the following
- two examples
+ variables that when printed show up with a question mark in front of them. Consider
+ the following two examples
@{ML_response_fake [display, gray]
"let
val v1 = Var ((\"x\", 3), @{typ bool})
- val v2 = Var ((\"x1\",3), @{typ bool})
+ val v2 = Var ((\"x1\", 3), @{typ bool})
in
writeln (Syntax.string_of_term @{context} v1);
writeln (Syntax.string_of_term @{context} v2)
@@ -664,13 +659,13 @@
This is different from a free variable
@{ML_response_fake [display, gray]
- "@{term \"x\"}"
+ "writeln (Syntax.string_of_term @{context} (Free (\"x\", @{typ bool})))"
"x"}
When constructing terms, you are usually concerned with free variables (for example
you cannot construct schematic variables using the antiquotation @{text "@{term \<dots>}"}).
- If you deal with theorems, you have to observe the distinction. The same holds
- for types.
+ If you deal with theorems, you have to observe the distinction. A similar
+ distinction holds for types (see below).
\begin{readmore}
Terms and types are described in detail in \isccite{sec:terms}. Their
@@ -685,8 +680,14 @@
"Type unification failed: Occurs check!"}
raises a typing error, while it perfectly ok to construct the term
-
- @{ML [display,gray] "Free (\"x\", @{typ nat}) $ Free (\"x\", @{typ nat})"}
+
+ @{ML_response_fake [display,gray]
+"let
+ val omega = Free (\"x\", @{typ nat}) $ Free (\"x\", @{typ nat})
+in
+ writeln (Syntax.string_of_term @{context} omega)
+end"
+ "x x"}
with the raw ML-constructors.
Sometimes the internal representation of terms can be surprisingly different
@@ -731,6 +732,22 @@
@{ML_response_fake [display,gray] "@{typ \"bool \<Rightarrow> nat\"}" "bool \<Rightarrow> nat"}
+ Their definition is
+*}
+
+ML_val{*datatype typ =
+ Type of string * typ list
+| TFree of string * sort
+| TVar of indexname * sort *}
+
+text {*
+ Like with terms, there is the distinction between free type
+ 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.
+
+
\begin{readmore}
Types are described in detail in \isccite{sec:types}. Their
definition and many useful operations are implemented
@@ -944,6 +961,8 @@
@{ML_response [display,gray]
"@{type_name \"list\"}" "\"List.list\""}
+ (FIXME: Explain the following better.)
+
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:
@@ -992,9 +1011,25 @@
"Const (\"op =\", \"int \<Rightarrow> int \<Rightarrow> bool\")
$ Free (\"a\", \"int\") $ Const (\"HOL.one_class.one\", \"int\")"}
- (FIXME: a readmore about types)
+ If you want to obtain the list of free type-variables of a term, you
+ can use the function @{ML Term.add_tfrees} (similarly @{ML Term.add_tvars}
+ for the schematic type-variables). One would expect that such functions
+ take a term as input and return a list of types. But their type is actually
+
+ @{text[display] "Term.term -> (string * Term.sort) list -> (string * Term.sort) list"}
- (Explain @{ML Term.add_tvarsT} and @{ML Term.add_tfreesT})
+ that is they take, besides a term, also a list of type-variables as input.
+ So in order to obtain the list of type-variables of a term you have to
+ call them as follows
+
+ @{ML_response [gray,display]
+ "Term.add_tfrees @{term \"(a,b)\"} []"
+ "[(\"'b\", [\"HOL.type\"]), (\"'a\", [\"HOL.type\"])]"}
+
+ The reason for this definition is that @{ML Term.add_tfrees} can
+ be easily folded over a list of terms. Similarly for all functions
+ named @{text "add_"}some\_name in @{ML_file "Pure/term.ML"}.
+
*}