
diff -r 3f153aa4f231 -r 72a53b07d264 ProgTutorial/General.thy
--- a/ProgTutorial/General.thy	Tue Nov 10 06:24:00 2009 +0100
+++ b/ProgTutorial/General.thy	Tue Nov 10 12:17:08 2009 +0100
@@ -674,7 +674,7 @@
   \end{exercise}
 *}
 
-section {* Unification and Matching (TBD) *}
+section {* Unification and Matching *}
 
 text {* 
   Isabelle's terms and types may contain schematic term variables
@@ -690,8 +690,8 @@
   schematic variables.
 
   Let us begin with describing the unification and matching function for
-  types.  Both return type environments, ML-type @{ML_type "Type.tyenv"},
-  which map schematic type variables to types (and sorts). Below we use the
+  types.  Both return type environments (ML-type @{ML_type "Type.tyenv"})
+  which map 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 * ?'b"} and @{text "?'b list *
   nat"}. This will produce the mapping, or type environment, @{text "[?'a :=
@@ -706,13 +706,13 @@
 end*}
 
 text {* 
-  The environment @{ML_ind "Vartab.empty"} in line 5 stands for the 
-  empty type environment, which is needed for starting the unification 
-  without any (pre)instantiations.  In case of a failure 
-  @{ML typ_unify in Sign} will throw the exception @{text TUNIFY}.
-  We can print out the resulting type environment @{ML tyenv_unif} 
-  with the built-in function @{ML_ind dest in Vartab} from the structure
-  @{ML_struct Vartab}.
+  The environment @{ML_ind "Vartab.empty"} in line 5 stands for the empty type
+  environment, which is needed for starting the unification without any
+  (pre)instantiations. The @{text 0} is an integer index that we will explain
+  below. In case of failure @{ML typ_unify in Sign} will throw the exception
+  @{text TUNIFY}.  We can print out the resulting type environment @{ML
+  tyenv_unif} with the built-in function @{ML_ind dest in Vartab} from the
+  structure @{ML_struct Vartab}.
 
   @{ML_response_fake [display,gray]
   "Vartab.dest tyenv_unif"
@@ -749,49 +749,57 @@
 
 text {*
   The first components in this list stand for the schematic type variables and
-  the second are the associated sorts and types. In this example the sort
-  is the default sort @{text "HOL.type"}. We will use in what follows
-  the pretty-printing function from Figure~\ref{fig:prettyenv} for 
-  @{ML_type "Type.tyenv"}s. For the type environment in the example 
-  this function prints out the more legible: 
+  the second are the associated sorts and types. In this example the sort is
+  the default sort @{text "HOL.type"}. We will use in what follows the
+  pretty-printing function from Figure~\ref{fig:prettyenv} for @{ML_type
+  "Type.tyenv"}s. For the type environment in the example this function prints
+  out the more legible:
 
   @{ML_response_fake [display, gray]
   "pretty_tyenv @{context} tyenv_unif"
   "[?'a := ?'b list, ?'b := nat]"}
 
-  The index @{text 0} in Line 5 in the example above is the maximal index of
-  the schematic type variables occuring in @{text ty1} and @{text ty2}. This
-  index will be increased whenever a new schematic type variable is introduced
-  during unification.  This is for example the case when two schematic type
-  variables have different, incomparable sorts. Then a new schematic type
-  variable is introduced with the combined sorts. To show this let us assume two
-  sorts, say @{text "s1"} and @{text "s2"}, which we attach to the schematic type
-  variables @{text "?'a"} and @{text "?'b"}. Since we do not make any assumption
-  about the sors, they are incomparable, leading to the type environment:
+  The way the unification function @{ML typ_unify in Sign} is implemented 
+  using an initial type environment and initial index makes it easy to
+  unify more than two terms. For example 
+*}
+
+ML %linenosgray{*val (tyenvs, _) = let
+  val tys1 = (@{typ_pat "?'a"}, @{typ_pat "?'b list"})
+  val tys2 = (@{typ_pat "?'b"}, @{typ_pat "nat"})
+in
+  fold (Sign.typ_unify @{theory}) [tys1, tys2] (Vartab.empty, 0) 
+end*}
+
+text {*
+  The index @{text 0} in Line 5 is the maximal index of the schematic type
+  variables occurring in @{text ty1} and @{text ty2}. This index will be
+  increased whenever a new schematic type variable is introduced during
+  unification.  This is for example the case when two schematic type variables
+  have different, incomparable sorts. Then a new schematic type variable is
+  introduced with the combined sorts. To show this let us assume two sorts,
+  say @{text "s1"} and @{text "s2"}, which we attach to the schematic type
+  variables @{text "?'a"} and @{text "?'b"}. Since we do not make any
+  assumption about the sorts, they are incomparable.
 *}
 
 ML{*val (tyenv, index) = let
-  val ty2 = @{typ_pat "?'a::s1"}
-  val ty1 = @{typ_pat "?'b::s2"}
+  val ty1 = @{typ_pat "?'a::s1"}
+  val ty2 = @{typ_pat "?'b::s2"}
 in
   Sign.typ_unify @{theory} (ty1, ty2) (Vartab.empty, 0) 
 end*}
 
 text {*
-  To print out this type environment we switch on the printing of sort 
-  information.
-*}
-
-ML{*show_sorts := true*}
-
-text {*
-  Now we can see
+  To print out the result type environment we switch on the printing 
+  of sort information by setting @{ML_ind show_sorts in Syntax} to 
+  true. This allows us to inspect the typing environment.
 
   @{ML_response_fake [display,gray]
   "pretty_tyenv @{context} tyenv"
   "[?'a::s1 := ?'a1::{s1,s2}, ?'b::s2 := ?'a1::{s1,s2}]"}
 
-  the type variables @{text "?'a"} and @{text "?'b"} are instantiated
+  As can be seen, the type variables @{text "?'a"} and @{text "?'b"} are instantiated
   with a new type variable @{text "?'a1"} with sort @{text "{s1,s2}"}. Since a new
   type variable has been introduced the @{ML index}, originally being @{text 0}, 
   has been increased by @{text 1}.
@@ -799,24 +807,10 @@
   @{ML_response [display,gray]
   "index"
   "1"}
-*}(*<*)ML %linenos{*show_sorts := false*}(*>*)
-
-text {*
-  The way the unification function @{ML typ_unify in Sign} is implemented 
-  using an initial type environment and initial index makes it easy to
-  unify more than two terms. For example 
-*}
-
-ML{*val (tyenvs, _) = let
-  val tys1 = (@{typ_pat "?'a"}, @{typ_pat "?'b list"})
-  val tys2 = (@{typ_pat "?'b"}, @{typ_pat "nat"})
-in
-  fold (Sign.typ_unify @{theory}) [tys1, tys2] (Vartab.empty, 0) 
-end*}
-
-text {*
-  Let us now return again to the unifier from the first example in this
-  section.
+
+  Let us now return again to the unification problem @{text "?'a * ?'b"} and 
+  @{text "?'b list * nat"} from the beginning of the section, and the 
+  calculated type environment @{ML tyenv_unif}:
 
   @{ML_response_fake [display, gray]
   "pretty_tyenv @{context} tyenv_unif"
@@ -839,8 +833,8 @@
   correctly instantiated.
 
   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} and might raise the exception @{text TYPE_MATCH} in case
+  also from the structure @{ML_struct Sign}. This function returns a @{ML_type
+  Type.tyenv} as well, but might raise the exception @{text TYPE_MATCH} in case
   of failure. For example
 *}
 
@@ -858,7 +852,7 @@
   "pretty_tyenv @{context} tyenv_match"
   "[?'a := bool list, ?'b := nat]"}
   
-  Unlike the unification, which uses the function @{ML norm_type in Envir}, 
+  Unlike unification, which uses the function @{ML norm_type in Envir}, 
   applying the matcher to a type needs to be done with the function
   @{ML_ind subst_type in Envir}.
 
@@ -881,23 +875,23 @@
 
 text {*
   Now @{ML tyenv_unif} is equal to @{ML tyenv_match'}. If we apply 
-  @{ML norm_type in Envir} to the matcher we obtain
+  @{ML norm_type in Envir} to the type @{text "?'a * ?'b"} 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 unifyier we obtain
+  which does not solve the matching problem, and if
+  we apply @{ML subst_type in Envir} to the same type we obtain
 
   @{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.
+  which does not solve the unification problem.
 
   \begin{readmore}
-  Unification and matching of types is implemented
+  Unification and matching for 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"}.
@@ -909,9 +903,9 @@
 
 text {*
   Unification and matching of terms is substantially more complicated than the
-  type-case. The reason is that terms have abstractions and unification
-  or matching modulo plain equality is often not meaningful in this
-  context. Nevertheless, Isabelle implements the function @{ML_ind
+  type-case. The reason is that terms have abstractions and, in this context,  
+  unification or matching modulo plain equality is often not meaningful. 
+  Nevertheless, Isabelle implements the function @{ML_ind
   first_order_match in Pattern} for terms.  This matching function returns a
   type environment and a term environment.  To pretty print the latter we use
   the function @{text "pretty_env"}:
@@ -944,7 +938,7 @@
 text {*
   In this example we annotated explicitly types because then 
   the type environment is empty and can be ignored. The 
-  resulting term environment is:
+  resulting term environment is
 
   @{ML_response_fake [display, gray]
   "pretty_env @{context} fo_env"
@@ -952,8 +946,8 @@
 
   The matcher can be applied to a term using the function @{ML_ind subst_term
   in Envir} (remember the same convention for types applies to terms: @{ML
-  subst_term in Envir} is for matchers and @{ML norm_term in Envir} is for
-  unifyiers). The function @{ML subst_term in Envir} expects a type environment,
+  subst_term in Envir} is for matchers and @{ML norm_term in Envir} for
+  unifiers). The function @{ML subst_term in Envir} expects a type environment,
   which is set to empty in the example below, and a term environment.
 
   @{ML_response_fake [display, gray]
@@ -969,7 +963,7 @@
   First-order matching is useful for matching against applications and
   variables. It can deal also with abstractions and a limited form of
   alpha-equivalence, but this kind of matching should be used with care, since
-  it is not clear whether the result is meaningful. A working example is
+  it is not clear whether the result is meaningful. A meaningful example is
   matching @{text "\<lambda>x. P x"} against the pattern @{text "\<lambda>y. ?X y"}. In this
   case first-order matching produces @{text "[?X := P]"}.
 
@@ -987,18 +981,17 @@
 *}
 
 text {*
-  In the context of unifying abstractions, more thouroughly studied is
-  higher-order pattern unification and higher-order pattern matching.  A
+  Unification of abstractions is more thoroughly studied in the context
+  of higher-order pattern unification and higher-order pattern matching.  A
   \emph{\index*{pattern}} is a lambda term whose ``head symbol'' (that is the
   first symbol under abstractions) is either a constant, or a schematic or a free
   variable. If it is a schematic variable then it can be only applied by
   distinct bound variables. This excludes that a schematic variable is an
-  argument of a schematic variable and that a schematic variable is applied
-  twice to the same bound variable. The function @{ML_ind pattern in Pattern}
+  argument of another one and that a schematic variable is applied
+  twice with the same bound variable. The function @{ML_ind pattern in Pattern}
   in the structure @{ML_struct Pattern} tests whether a term satisfies these
   restrictions.
 
-
   @{ML_response [display, gray]
   "let
   val trm_list = 
@@ -1011,20 +1004,62 @@
 end"
   "[true, true, true, true, true, false, false, false]"}
 
-  The point of restricting unification and matching to patterns is that
-  it is decidable and produces most general unifiers. In this way 
-  matching and unify can be implemented so that they produce a type
-  and term environment (the latter actually produces only a term 
-  environment).
+  The point of the restriction to patterns is that unification and matching 
+  are decidable and produce most general unifiers, respectively matchers. 
+  In this way, matching and unification can be implemented as functions that 
+  produce a type and term environment (unification actually returns a 
+  record of type @{ML_type Envir.env} containing a maxind, a type environment 
+  and a term environment). The former function is @{ML_ind match in Pattern},
+  the latter @{ML_ind unify in Pattern} both implemented in the structure
+  @{ML_struct Pattern}. An example for higher-order pattern unification is
+
+  \ldots
 *}
 
+ML{*let
+  val pat = @{term_pat "?X"}
+  val trm = @{term "a"}
+  val init = (Vartab.empty, Vartab.empty)
+in
+  Pattern.match @{theory} (pat, trm) init
+end *}
 
 text {*
+  An assumption of this function is that the terms to be unified have 
+  already the same type. In case of failure, the exceptions that are raised
+  are either @{text Pattern}, @{text MATCH} or @{text Unif}.
+
+  As mentioned before, ``full'' higher-order unification, respectively, matching 
+  problems are in general undecidable and might in general not posses a single
+  most general solution. Therefore Isabelle implements Huet's pre-unification
+  algorithm which does not return a single result, rather a lazy list of potentially
+  infinite unifiers. The corresponding function is called @{ML_ind unifiers in Unify}.
+  An example is as follows
+
+  \ldots
+
+  In case of failure this function does not raise an exception, rather returns
+  the empty sequence. In order to find a reasonable solution for a unification 
+  problem, Isabelle also tries first to solve the problem by higher-order 
+  pattern unification.
+
+  \ldots
+  
+  For higher-order matching the function is called @{ML_ind matchers in Unify}.
+  Also this function might potentially return sequences with more than one
+  element.
+
+
+  Like @{ML unifiers in Unify}, this function does not raise an exception
+  in case of failure. It also tries out first whether the matching problem
+  can be solved by first-order matching.
+
   \begin{readmore}
-  For term, unification and matching of higher-order patterns is implemented in 
+  Unification and matching of higher-order patterns is implemented in 
   @{ML_file "Pure/pattern.ML"}. This file also contains a first-order matcher
   for terms. Full higher-order unification is implemented
-  in @{ML_file "Pure/unify.ML"}. 
+  in @{ML_file "Pure/unify.ML"}. It uses lazy sequences which are implemented
+  in @{ML_file "Pure/General/seq.ML"}.
   \end{readmore}
 *}
 




