
diff -r 2565c87f8db7 -r 8057d65607eb ProgTutorial/FirstSteps.thy
--- a/ProgTutorial/FirstSteps.thy	Fri Jul 31 19:10:39 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Sat Aug 01 08:59:41 2009 +0200
@@ -349,7 +349,8 @@
 text {*
   This function takes a term and a context as argument. If the term is of function
   type, then @{ML "apply_fresh_args"} returns the term with distinct variables 
-  applied to it. For example:
+  applied to it. For example below variables are applied to the term 
+  @{term [show_types] "P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool"}:
 
   @{ML_response_fake [display,gray]
 "let
@@ -364,17 +365,17 @@
 
   You can read off this behaviour from how @{ML apply_fresh_args} is
   coded: in Line 2, the function @{ML [index] fastype_of} calculates the type of the
-  function; @{ML [index] binder_types} in the next line produces the list of argument
+  term; @{ML [index] binder_types} in the next line produces the list of argument
   types (in the case above the list @{text "[nat, int, unit]"}); Line 4 
   pairs up each type with the string  @{text "z"}; the
   function @{ML [index] variant_frees in Variable} generates for each @{text "z"} a
   unique name avoiding the given @{text f}; the list of name-type pairs is turned
   into a list of variable terms in Line 6, which in the last line is applied
-  by the function @{ML [index] list_comb} to the function. In this last step we have to 
+  by the function @{ML [index] list_comb} to the term. In this last step we have to 
   use the function @{ML [index] curry}, because @{ML [index] list_comb} expects the 
   function and the variables list as a pair. This kind of functions is often needed when
-  constructing terms and the infrastructure helps tremendously to avoid
-  any name clashes. Consider for example: 
+  constructing terms with fresh variables. The infrastructure helps tremendously 
+  to avoid any name clashes. Consider for example: 
 
    @{ML_response_fake [display,gray]
 "let
@@ -496,7 +497,7 @@
   "acc_incs 1 ||>> (fn x => (x, x + 2))"
   "(((((\"\", 1), 2), 3), 4), 6)"}
 
-  (FIXME: maybe give a ``real world'' example)
+  (FIXME: maybe give a ``real world'' example for this combinator)
 *}
 
 text {*
@@ -535,7 +536,8 @@
   The main advantage of embedding all code in a theory is that the code can
   contain references to entities defined on the logical level of Isabelle. By
   this we mean definitions, theorems, terms and so on. This kind of reference is
-  realised with antiquotations.  For example, one can print out the name of the current
+  realised with antiquotations, sometimes also referred to as ML-antiquotations.  
+  For example, one can print out the name of the current
   theory by typing
 
   
@@ -637,13 +639,13 @@
   why @{ML snd} is needed)
 
   It is also possible to define your own antiquotations. But you should
-  exercise care when introducing new one, as they can also make your
-  code unreadable. In the next section we will see how the (build in) 
+  exercise care when introducing new ones, as they can also make your
+  code also difficult to read. In the next section we will see how the (build in) 
   antiquotation @{text "@{term \<dots>}"} can be used to construct terms.
   A restriction of this antiquotation is that it does not allow you to
-  use schematic variables. If you want a antiquotation that does not
+  use schematic variables. If you want an antiquotation that does not
   have this restriction, you can implement your own using the 
-  function @{ML [index] ML_Antiquote.inline}. 
+  function @{ML [index] ML_Antiquote.inline}. The code is as follows.
 *}
 
 ML %linenosgray{*ML_Antiquote.inline "term_pat"
@@ -654,9 +656,9 @@
          |> ML_Syntax.atomic))*}
 
 text {*
-  We call the antiquotation @{text "term_pat"} (Line 1); the parser in Line
+  We call the new antiquotation @{text "term_pat"} (Line 1); the parser in Line
   2 provides us with a context and a string; this string is transformed into a 
-  term using the function @{ML read_term_pattern in ProofContext} (Line 4);
+  term using the function @{ML [index] read_term_pattern in ProofContext} (Line 4);
   the next two lines print the term so that the ML-system can understand 
   them. An example of this antiquotation is as follows.
 
@@ -664,24 +666,27 @@
   "@{term_pat \"Suc (?x::nat)\"}"
   "Const (\"Suc\", \"nat \<Rightarrow> nat\") $ Var ((\"x\", 0), \"nat\")"}
 
+  which is the internal representation of the term @{text "Suc ?x"}.
+
   \begin{readmore}
   The file @{ML_file "Pure/ML/ml_antiquote.ML"} contains the the definitions
   for most antiquotations. 
   \end{readmore}
 
-  Note also that in Isabelle there are two kinds of antiquotations, which have
-  very different infrastructures. The first kind, described in this section,
-  is sometimes called \emph{ML-antiquotations}. They are used to refer to
-  entities (like terms, types etc) from Isabelle's logic layer inside ML-code. 
-  They are ``linked'' statically at compile-time, which  limits sometimes 
-  their usefulness in  cases where, for example, terms needs to be built up 
-  dynamically.  
-
-  The other kind of antiquotations are called \emph{document antiquotations}. 
-  They are used only in the text parts of Isabelle and help with printing logical 
-  entities inside \LaTeX-documents. In this Tutorial we are not interested
-  in these antiquotations, except in Appendix \ref{rec:docantiquotations} where
-  we show how to implement your own document antiquotations. 
+  Note one source of possible confusion about antiquotations. There are two kinds 
+  of them in Isabelle, which have very different purpose and infrastructures. The 
+  first kind, described in this section, are \emph{ML-antiquotations}. They are 
+  used to refer to entities (like terms, types etc) from Isabelle's logic layer 
+  inside ML-code. They are ``linked'' statically at compile-time, which  limits 
+  sometimes their usefulness in  cases where, for example, terms needs to be 
+  built up dynamically.  
+
+  The other kind of antiquotations are \emph{document} antiquotations. 
+  They are used only in the text parts of Isabelle and their purpose is to print 
+  logical entities inside \LaTeX-documents. They are part of the user level and
+  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. 
 *}
 
 section {* Terms and Types *}
@@ -708,6 +713,7 @@
 | $ of term * term *}
 
 text {*
+  This datatype implements lambda-terms typed in Church-style.
   As can be seen in Line 5, terms use the usual de Bruijn index mechanism
   for representing bound variables.  For
   example in
@@ -716,11 +722,15 @@
   "@{term \"\<lambda>x y. x y\"}"
   "Abs (\"x\", \"'a \<Rightarrow> 'b\", Abs (\"y\", \"'a\", Bound 1 $ Bound 0))"}
 
-  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
-  realised with the term-constructor @{ML $}. 
+  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. Constructing 
+  a term with dangling de Bruijn indices is possible, but will be flagged as
+  ill-formed when you try to typecheck or certify it (see
+  Section~\ref{sec:typechecking}). 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 $}.
+
 
   Isabelle makes a distinction between \emph{free} variables (term-constructor @{ML Free})
   and variables (term-constructor @{ML Var}). The latter correspond to the schematic 
@@ -731,20 +741,17 @@
 "let
   val v1 = Var ((\"x\", 3), @{typ bool})
   val v2 = Var ((\"x1\", 3), @{typ bool})
+  val v3 = Free (\"x\", @{typ bool})
 in
   writeln (Syntax.string_of_term @{context} v1);
-  writeln (Syntax.string_of_term @{context} v2)
+  writeln (Syntax.string_of_term @{context} v2);
+  writeln (Syntax.string_of_term @{context} v3)
 end"
 "?x3
-?x1.3"}
-
-  This is different from a free variable
-
-  @{ML_response_fake [display, gray]
-  "writeln (Syntax.string_of_term @{context} (Free (\"x\", @{typ bool})))"
-  "x"}
-
-  When constructing terms, you are usually concerned with free variables (for example
+?x1.3
+x"}
+
+  When constructing terms, you are usually concerned with free variables (as mentioned earlier,
   you cannot construct schematic variables using the antiquotation @{text "@{term \<dots>}"}). 
   If you deal with theorems, you have to, however, observe the distinction. A similar
   distinction holds for types (see below).
@@ -817,7 +824,7 @@
 
   @{ML_response_fake [display,gray] "@{typ \"bool \<Rightarrow> nat\"}" "bool \<Rightarrow> nat"}
 
-  Their definition is
+  The corresponding datatype is
 *}
   
 ML_val{*datatype typ =
@@ -830,8 +837,13 @@
   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.
-  
+  of argument types. However, it is a bit difficult to show an
+  example, because Isabelle always pretty-prints types (unlike terms).
+  Here is a contrived example:
+
+  @{ML_response [display, gray]
+  "if Type (\"bool\", []) = @{typ \"bool\"} then true else false"
+  "true"}
 
   \begin{readmore}
   Types are described in detail in \isccite{sec:types}. Their
@@ -891,7 +903,12 @@
   list applied to the term. For example
 
 @{ML_response_fake [display,gray]
-"list_comb (@{term \"P::nat\"}, [@{term \"True\"}, @{term \"False\"}])"
+"let
+  val t = @{term \"P::nat\"}
+  val args = [@{term \"True\"}, @{term \"False\"}]
+in
+  list_comb (t, args)
+end"
 "Free (\"P\", \"nat\") $ Const (\"True\", \"bool\") $ Const (\"False\", \"bool\")"}
 
   Another handy function is @{ML [index] lambda}, which abstracts a variable 
@@ -901,7 +918,7 @@
   "lambda @{term \"x::nat\"} @{term \"(P::nat \<Rightarrow> bool) x\"}"
   "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"}), 
+  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
   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"}
@@ -1159,7 +1176,7 @@
 *}
 
 
-section {* Type-Checking *}
+section {* Type-Checking\label{sec:typechecking} *}
 
 text {* 
   




