
diff -r ab9e09076462 -r cccb25ee1309 ProgTutorial/FirstSteps.thy
--- 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"}.
+
 *}
 
 




