
diff -r 5f7ca76f94e3 -r 5dcee4d751ad ProgTutorial/General.thy
--- a/ProgTutorial/General.thy	Thu Nov 12 10:06:26 2009 +0100
+++ b/ProgTutorial/General.thy	Thu Nov 12 20:35:14 2009 +0100
@@ -774,7 +774,7 @@
 
 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
+  variables occurring in @{text tys1} and @{text tys2}. 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
@@ -798,12 +798,12 @@
 
   @{ML_response_fake [display,gray]
   "pretty_tyenv @{context} tyenv"
-  "[?'a::s1 := ?'a1::{s1,s2}, ?'b::s2 := ?'a1::{s1,s2}]"}
+  "[?'a::s1 := ?'a1::{s1, s2}, ?'b::s2 := ?'a1::{s1, s2}]"}
 
   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
+  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}.
+  has been increased to @{text 1}.
 
   @{ML_response [display,gray]
   "index"
@@ -926,11 +926,11 @@
 
 ML{*val (_, fo_env) = let
   val fo_pat = @{term_pat "(?X::(nat\<Rightarrow>nat\<Rightarrow>nat)\<Rightarrow>bool) ?Y"}
-  val trm = @{term "P::(nat\<Rightarrow>nat\<Rightarrow>nat)\<Rightarrow>bool"} 
-              $ @{term "\<lambda>a b. (Q::nat\<Rightarrow>nat\<Rightarrow>nat) b a"}
+  val trm_a = @{term "P::(nat\<Rightarrow>nat\<Rightarrow>nat)\<Rightarrow>bool"} 
+  val trm_b = @{term "\<lambda>a b. (Q::nat\<Rightarrow>nat\<Rightarrow>nat) b a"}
   val init = (Vartab.empty, Vartab.empty) 
 in
-  Pattern.first_order_match @{theory} (fo_pat, trm) init
+  Pattern.first_order_match @{theory} (fo_pat, trm_a $ trm_b) init
 end *}
 
 text {*
@@ -963,7 +963,7 @@
   alpha-equivalence, but this kind of matching should be used with care, since
   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]"}.
+  case, first-order matching produces @{text "[?X := P]"}.
 
   @{ML_response_fake [display, gray]
   "let
@@ -981,11 +981,11 @@
 text {*
   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
+  \emph{\index*{pattern}} is an abstraction term whose ``head symbol'' (that is the
   first symbol under an abstraction) is either a constant, a schematic or a free
   variable. If it is a schematic variable then it can be only applied with
-  distinct bound variables. This excludes that a schematic variable is an
-  argument of another one and that a schematic variable is applied
+  distinct bound variables. This excludes terms where a schematic variable is an
+  argument of another one and where 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.
@@ -1022,31 +1022,81 @@
 end"
   "[?X := \<lambda>y x. x, ?Y := \<lambda>x. x]"}
 
-
-  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
-  higher-order matching problems, are in general undecidable and might also not posses a
+  The function @{ML_ind "Envir.empty"} generates a record with a specified
+  max-index for the schematic variables (in the example the index is @{text
+  0}) and empty type and term environments. The function @{ML_ind
+  "Envir.term_env"} pulls out the term environment from the result record. The
+  function for type environment is @{ML_ind "Envir.type_env"}. 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, unrestricted higher-order unification, respectively
+  higher-order matching, is in general undecidable and might also not posses a
   single most general solution. Therefore Isabelle implements the unification
   function @{ML_ind unifiers in Unify} so that it returns a lazy list of
   potentially infinite unifiers.  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. For higher-order matching the function is called 
-  @{ML_ind matchers in Unify}. Also this function might potentially return 
-  sequences with more than one matcher.
-
-  \ldots
-
+*}
+
+ML{*val uni_seq =
+let 
+  val trm1 = @{term_pat "?X ?Y"}
+  val trm2 = @{term "f a"}
+  val init = Envir.empty 0
+in
+  Unify.unifiers (@{theory}, init, [(trm1, trm2)])
+end *}
+
+text {*
+  The unifiers can be extracted from the lazy sequence using the 
+  function @{ML_ind "Seq.pull"}. In the example we obtain three 
+  unifiers @{text "un1\<dots>un3"}.
+*}
+
+ML{*val SOME ((un1, _), next1) = Seq.pull uni_seq;
+val SOME ((un2, _), next2) = Seq.pull next1;
+val SOME ((un3, _), next3) = Seq.pull next2;
+val NONE = Seq.pull next3 *}
+
+text {*
+  \footnote{\bf FIXME: what is the list of term pairs in the unifier: flex-flex pairs?}
+
+  We can print them out as follows.
+
+  @{ML_response_fake [display, gray]
+  "pretty_env @{context} (Envir.term_env un1);
+pretty_env @{context} (Envir.term_env un2);
+pretty_env @{context} (Envir.term_env un3)"
+  "[?X := \<lambda>a. a, ?Y := f a]
+[?X := f, ?Y := a]
+[?X := \<lambda>b. f a]"}
+
+
+  In case of failure the function @{ML_ind unifiers in Unify} does not raise
+  an exception, rather returns the empty sequence. For example
+
+  @{ML_response [display, gray]
+"let 
+  val trm1 = @{term \"a\"}
+  val trm2 = @{term \"b\"}
+  val init = Envir.empty 0
+in
+  Unify.unifiers (@{theory}, init, [(trm1, trm2)])
+  |> Seq.pull
+end"
+"NONE"}
+
+  In order to find a
+  reasonable solution for a unification problem, Isabelle also tries first to
+  solve the problem by higher-order pattern unification. 
+
+  For higher-order
+  matching the function is called @{ML_ind matchers in Unify} implemented
+  in the structure @{ML_struct Unify}. Also this
+  function returns sequences with possibly more than one matcher.
   Like @{ML unifiers in Unify}, this function does not raise an exception
-  in case of failure. It also first tries out whether the matching problem
-  can be solved by first-order matching.
+  in case of failure, but returns an empty sequence. It also first tries 
+  out whether the matching problem can be solved by first-order matching.
 
   \begin{readmore}
   Unification and matching of higher-order patterns is implemented in 
@@ -2425,6 +2475,14 @@
 ML {* Sign.intern_type @{theory} "list" *}
 ML {* Sign.intern_const @{theory} "prod_fun" *}
 
+
+text {* 
+  @{ML_ind "Binding.str_of"} returns the string with markup;
+  @{ML_ind "Binding.name_of"} returns the string without markup
+*}
+
+
+
 section {* Summary *}
 
 text {*




