diff -r 272ba2cceeb2 -r 8d160d79b48c ProgTutorial/General.thy
--- a/ProgTutorial/General.thy	Sat Nov 07 10:08:09 2009 +0100
+++ b/ProgTutorial/General.thy	Mon Nov 09 09:25:51 2009 +0100
@@ -674,26 +674,166 @@
   \end{exercise}
 *}
 
-section {* Matching and Unification (TBD) *}
+section {* Unification and Matching (TBD) *}
 
 text {* 
-  Using the antiquotation from Section~\ref{sec:antiquote}.
+  Isabelle's terms and types contain schematic term variables
+  (term-constructor @{ML Var}) and schematic type variables (term-constructor
+  @{ML TVar}). Both are printed out as variables with a leading question
+  mark. They stand for unknown terms and types, which can be made more concrete
+  by instantiations. Such instantiations can be calculated by unification or
+  matching. While in case of types, unification and matching is relatively
+  straightforward, in case of terms the algorithms are substantially more
+  complicated, because terms need higher-order versions of the unification and
+  matching algorithms. Below we shall use the antiquotation @{text "@{typ_pat \<dots>}"} and
+  @{text "@{term_pat \<dots>}"} from Section~\ref{sec:antiquote} in order to
+  construct examples involving schematic variables.
+
+  Let us begin with describing unification and matching of types.  Both
+  matching and unification of types return a type environment, ML-type
+  @{ML_type "Type.tyenv"}, which maps schematic type variables to types (and
+  sorts). Below we use the function @{ML_ind typ_unify in Sign} from the 
+  structure @{ML_struct Sign} for unifying
+  the types @{text "?'a * nat"} and @{text "?'b list * ?'b"}. This will
+  produce the mapping @{text "[?'a := ?'b list, ?'b := nat]"}.
+*}
+
+ML{*val (tyenv_unif, _) = let
+  val ty1 = @{typ_pat "?'a * nat"}
+  val ty2 = @{typ_pat "?'b list * ?'b"}
+in
+  Sign.typ_unify @{theory} (ty1, ty2) (Vartab.empty, 0) 
+end*}
+
+text {* 
+  The value @{ML_ind empty in Vartab} stands for the empty type environment, 
+  which is the value for starting the unification without any 
+  instantiations.\footnote{\bf FIXME: what is 0?} 
+  We can print out the resulting 
+  type environment with the built-in function @{ML_ind dest in Vartab}.
+
+  @{ML_response_fake [display,gray]
+  "Vartab.dest tyenv_unif"
+  "[((\"'a\", 0), ([\"HOL.type\"], \"?'b List.list\")), 
+ ((\"'b\", 0), ([\"HOL.type\"], \"nat\"))]"}
+
+  For what follows we will use the following pretty-printing function
+  for @{ML_type "Type.tyenv"}s
 *}
 
-ML{*val (env, _) = 
-  Sign.typ_unify @{theory} (@{typ_pat "?'b * ?'c"}, @{typ_pat "?'a * ?'b"}) (Vartab.empty, 0) *}
+ML{*fun pretty_tyenv ctxt tyenv =
+let
+  fun aux (v, (s, T)) =
+        Syntax.string_of_typ ctxt (TVar (v, s)) 
+        ^ " := " ^ Syntax.string_of_typ ctxt T
+in
+  tyenv |> Vartab.dest
+        |> map aux 
+        |> commas
+        |> enclose "[" "]"
+        |> tracing
+end*}
 
-ML{*Vartab.dest env  *}
+text {*
+  which prints for the type environment above
+
+  @{ML_response_fake [display, gray]
+  "pretty_tyenv @{context} tyenv_unif"
+  "[?'a := ?'b list, ?'b := nat]"}
 
-ML{*Envir.norm_type env @{typ_pat "?'a"}*}
+  Observe that the type environment that the function @{ML typ_unify in
+  Sign} returns is in \emph{not} an instantiation in fully solved form: while @{text
+  "?'b"} is instantiated to @{typ nat}, this is not propagated to the
+  instantiation for @{text "?'a"}.  In unification theory, this is often
+  called an instantiation in \emph{triangular form}. These instantiations
+  are used because of performance reasons.
+
+
+  To apply a type environment in triangular form to a type, say @{text "?'a *
+  ?'b"}, you should use the function @{ML_ind norm_type in Envir}:
 
-ML{*val env = 
-  Sign.typ_match @{theory} (@{typ_pat "?'b * ?'c"}, @{typ_pat "?'a * ?'b"}) Vartab.empty *}
+  @{ML_response_fake [display, gray]
+  "Envir.norm_type tyenv_unif @{typ_pat \"?'a * ?'b\"}"
+  "nat list * nat"}
+*}
 
-ML{*Envir.subst_type env  @{typ_pat "?'a"} *}
+text {* 
+  Matching of types can be done with the function @{ML_ind typ_match in Sign}
+  from the structure @{ML_struct Sign}. It also returns a @{ML_type
+  Type.tyenv}. For example
+*}
+
+ML{*val tyenv_match = let
+  val pat = @{typ_pat "?'a * ?'b"}
+  and ty  = @{typ_pat "bool list * nat"}
+in
+  Sign.typ_match @{theory} (pat, ty) Vartab.empty 
+end*}
 
 text {*
-  Note the difference. Norm for unify; Subst for match.
+  Printing out the calculated matcher gives
+
+  @{ML_response_fake [display,gray]
+  "pretty_tyenv @{context} tyenv_match"
+  "[?'a := bool list, ?'b := nat]"}
+  
+  Applying the matcher to a type needs to be done with the function
+  @{ML_ind subst_type in Envir}.
+
+  @{ML_response_fake [display, gray]
+  "Envir.subst_type tyenv_match @{typ_pat \"?'a * ?'b\"}"
+  "bool list * nat"}
+
+  Be careful to observe the difference: use @{ML subst_type in Envir} 
+  for matchers and @{ML norm_type in Envir} for unifiers. To show the 
+  difference let us calculate the following matcher.
+*}
+
+ML{*val tyenv_match' = let
+  val pat = @{typ_pat "?'a * ?'b"}
+  and ty  = @{typ_pat "?'b list * nat"}
+in
+  Sign.typ_match @{theory} (pat, ty) Vartab.empty 
+end*}
+
+text {*
+  Now @{ML tyenv_unif} is equal to @{ML tyenv_match'}. Consider
+  again the type @{text "?'a * ?'b"}. If we apply 
+  @{ML norm_type in Envir} to the matcher we obtain
+
+  @{ML_response_fake [display, gray]
+  "Envir.norm_type tyenv_match' @{typ_pat \"?'a * ?'b\"}"
+  "nat list * nat"}
+
+  which is not a matcher for the second matching problem, and if
+  we apply @{ML subst_type in Envir} to the unifier
+
+  @{ML_response_fake [display, gray]
+  "Envir.subst_type tyenv_unif @{typ_pat \"?'a * ?'b\"}"
+  "?'b list * nat"}
+  
+  which is not the correct unifier for the unification problem.
+
+  \begin{readmore}
+  Unification and matching of types is implemented
+  in @{ML_file "Pure/type.ML"}. The ``interface'' functions for them
+  are in @{ML_file "Pure/sign.ML"}. Matching and unification produce type environments
+  as results. These are implemented in @{ML_file "Pure/envir.ML"}.
+  This file also includes the substitution and normalisation functions. 
+  Environments are lookup tables that are implemented in 
+  @{ML_file "Pure/term_ord.ML"}.
+  \end{readmore}
+*}
+
+text {*
+  TBD below
+
+
+  \begin{readmore}
+  For term, unification and matching of higher-order patterns is implemented in 
+  @{ML_file "Pure/pattern.ML"}. Full higher-order unification is implemented
+  in @{ML_file "Pure/unify.ML"}. 
+  \end{readmore}
 *}
 
 section {* Type-Checking\label{sec:typechecking} *}