isabelle-cookbook: comparison ProgTutorial/General.thy

equal deleted inserted replaced

-:78c91a629602
+:5f7ca76f94e3
 *}
 section {* Unification and Matching *}
 text {*
-Isabelle's terms and types may contain schematic term variables
+As seen earlier, Isabelle's terms and types may contain schematic term variables
 (term-constructor @{ML Var}) and schematic type variables (term-constructor
 @{ML TVar}). These variables stand for unknown entities, which can be made
 more concrete by instantiations. Such instantiations might be a result of
 unification or matching. While in case of types, unification and matching is
 relatively straightforward, in case of terms the algorithms are
 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. The @{text 0} is an integer index that we will explain
+(pre)instantiations. The @{text 0} is an integer index that will be explained
 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
+@{text TUNIFY}.  We can print out the resulting type environment bound to
-tyenv_unif} with the built-in function @{ML_ind dest in Vartab} from the
+@{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"
 "[((\"'a\", 0), ([\"HOL.type\"], \"?'b List.list\")),
 *}
 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
+the default sort @{text "HOL.type"}. Instead of @{ML "Vartab.dest"}, we will
-pretty-printing function from Figure~\ref{fig:prettyenv} for @{ML_type
+use in what follows our own pretty-printing function from
-"Type.tyenv"}s. For the type environment in the example this function prints
+Figure~\ref{fig:prettyenv} for @{ML_type "Type.tyenv"}s. For the type
-out the more legible:
+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]"}
 @{ML_response [display,gray]
 "index"
 "1"}
-Let us now return again to the unification problem @{text "?'a * ?'b"} and
+Let us now return to the unification problem @{text "?'a * ?'b"} and
-@{text "?'b list * nat"} from the beginning of the section, and the
+@{text "?'b list * nat"} from the beginning of this section, and the
 calculated type environment @{ML tyenv_unif}:
 @{ML_response_fake [display, gray]
 "pretty_tyenv @{context} tyenv_unif"
 "[?'a := ?'b list, ?'b := nat]"}
 Observe that the type environment which 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 not fully solved
+called an instantiation in \emph{triangular form}. These triangular
-instantiations are used because of performance reasons.
+instantiations, or triangular type environments, are used because of
-To apply a type environment in triangular form to a type, say @{text "?'a *
+performance reasons. To apply such a type environment to a type, say @{text "?'a *
 ?'b"}, you should use the function @{ML_ind norm_type in Envir}:
 @{ML_response_fake [display, gray]
 "Envir.norm_type tyenv_unif @{typ_pat \"?'a * ?'b\"}"
 "nat list * nat"}
-With this function the type variables @{text "?'a"} and @{text "?'b"} are
-correctly instantiated.
 Matching of types can be done with the function @{ML_ind typ_match in Sign}
 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
 "pretty_tyenv @{context} tyenv_match"
 "[?'a := bool list, ?'b := nat]"}
 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}.
+@{ML_ind subst_type in Envir}. For example
 @{ML_response_fake [display, gray]
 "Envir.subst_type tyenv_match @{typ_pat \"?'a * ?'b\"}"
 "bool list * nat"}
 Be careful to observe the difference: use always
 @{ML subst_type in Envir} for matchers and @{ML norm_type in Envir}
-for unifiers. To make the difference explicit, let us calculate the
+for unifiers. To show the difference, let us calculate the
 following matcher:
 *}
 ML{*val tyenv_match' = let
 val pat = @{typ_pat "?'a * ?'b"}
 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"}.
 This file also includes the substitution and normalisation functions,
-that apply a type environment to a type. Type environments are lookup
+which apply a type environment to a type. Type environments are lookup
 tables which are implemented in @{ML_file "Pure/term_ord.ML"}.
 \end{readmore}
 *}
 text {*
 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
-first symbol under abstractions) is either a constant, or a schematic or a free
+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 by
+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
 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.
 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},
+and a term environment). The corresponding functions are @{ML_ind match in Pattern},
-the latter @{ML_ind unify in Pattern} both implemented in the structure
+and @{ML_ind unify in Pattern} both implemented in the structure
 @{ML_struct Pattern}. An example for higher-order pattern unification is
 @{ML_response_fake [display, gray]
 "let
 val trm1 = @{term_pat \"\<lambda>x y. g (?X y x) (f (?Y 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, matching
+As mentioned before, ``full'' higher-order unification, respectively
-problems are in general undecidable and might in general not posses a single
+higher-order matching problems, are in general undecidable and might also not posses a
-most general solution. Therefore Isabelle implements Huet's pre-unification
+single most general solution. Therefore Isabelle implements the unification
-algorithm which does not return a single result, rather a lazy list of potentially
+function @{ML_ind unifiers in Unify} so that it returns a lazy list of
-infinite unifiers. The corresponding function is called @{ML_ind unifiers in Unify}.
+potentially infinite unifiers.  An example is as follows
-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.
+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
-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
+in case of failure. 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
 @{ML_file "Pure/pattern.ML"}. This file also contains a first-order matcher

changeset 386	5f7ca76f94e3
parent 385	78c91a629602
child 387	5dcee4d751ad