isabelle-cookbook: comparison ProgTutorial/General.thy

equal deleted inserted replaced

-:3f153aa4f231
+:72a53b07d264
 for constructing the terms for the logical connectives.\footnote{Thanks to Roy
 Dyckhoff for suggesting this exercise and working out the details.}
 \end{exercise}
 *}
-section {* Unification and Matching (TBD) *}
+section {* Unification and Matching *}
 text {*
 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
 antiquotations @{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 the unification and matching function for
-types.  Both return type environments, ML-type @{ML_type "Type.tyenv"},
+types.  Both return type environments (ML-type @{ML_type "Type.tyenv"})
-which map schematic type variables to types (and sorts). Below we use the
+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 :=
 ?'b list, ?'b := nat]"}.
 *}
 in
 Sign.typ_unify @{theory} (ty1, ty2) (Vartab.empty, 0)
 end*}
 text {*
-The environment @{ML_ind "Vartab.empty"} in line 5 stands for the
+The environment @{ML_ind "Vartab.empty"} in line 5 stands for the empty type
-empty type environment, which is needed for starting the unification
+environment, which is needed for starting the unification without any
-without any (pre)instantiations.  In case of a failure
+(pre)instantiations. The @{text 0} is an integer index that we will explain
-@{ML typ_unify in Sign} will throw the exception @{text TUNIFY}.
+below. In case of failure @{ML typ_unify in Sign} will throw the exception
-We can print out the resulting type environment @{ML tyenv_unif}
+@{text TUNIFY}.  We can print out the resulting type environment @{ML
-with the built-in function @{ML_ind dest in Vartab} from the structure
+tyenv_unif} with the built-in function @{ML_ind dest in Vartab} from the
-@{ML_struct Vartab}.
+structure @{ML_struct Vartab}.
 @{ML_response_fake [display,gray]
 "Vartab.dest tyenv_unif"
 "[((\"'a\", 0), ([\"HOL.type\"], \"?'b List.list\")),
 ((\"'b\", 0), ([\"HOL.type\"], \"nat\"))]"}
 \end{figure}
 *}
 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
+the second are the associated sorts and types. In this example the sort is
-is the default sort @{text "HOL.type"}. We will use in what follows
+the default sort @{text "HOL.type"}. We will use in what follows the
-the pretty-printing function from Figure~\ref{fig:prettyenv} for
+pretty-printing function from Figure~\ref{fig:prettyenv} for @{ML_type
-@{ML_type "Type.tyenv"}s. For the type environment in the example
+"Type.tyenv"}s. For the type environment in the example this function prints
-this function prints out the more legible:
+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 way the unification function @{ML typ_unify in Sign} is implemented
-the schematic type variables occuring in @{text ty1} and @{text ty2}. This
+using an initial type environment and initial index makes it easy to
-index will be increased whenever a new schematic type variable is introduced
+unify more than two terms. For example
-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
+ML %linenosgray{*val (tyenvs, _) = let
-sorts, say @{text "s1"} and @{text "s2"}, which we attach to the schematic type
+val tys1 = (@{typ_pat "?'a"}, @{typ_pat "?'b list"})
-variables @{text "?'a"} and @{text "?'b"}. Since we do not make any assumption
+val tys2 = (@{typ_pat "?'b"}, @{typ_pat "nat"})
-about the sors, they are incomparable, leading to the type environment:
+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 "?'a::s1"}
-val ty1 = @{typ_pat "?'b::s2"}
+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
+To print out the result type environment we switch on the printing
-information.
+of sort information by setting @{ML_ind show_sorts in Syntax} to
-*}
+true. This allows us to inspect the typing environment.
-ML{*show_sorts := true*}
-text {*
-Now we can see
 @{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}.
 @{ML_response [display,gray]
 "index"
 "1"}
-*}(*<*)ML %linenos{*show_sorts := false*}(*>*)
+Let us now return again to the unification problem @{text "?'a * ?'b"} and
-text {*
+@{text "?'b list * nat"} from the beginning of the section, and the
-The way the unification function @{ML typ_unify in Sign} is implemented
+calculated type environment @{ML tyenv_unif}:
-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.
 @{ML_response_fake [display, gray]
 "pretty_tyenv @{context} tyenv_unif"
 "[?'a := ?'b list, ?'b := 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}
-from the structure @{ML_struct Sign}. It also returns a @{ML_type
+also from the structure @{ML_struct Sign}. This function returns a @{ML_type
-Type.tyenv} and might raise the exception @{text TYPE_MATCH} in case
+Type.tyenv} as well, but might raise the exception @{text TYPE_MATCH} in case
 of failure. For example
 *}
 ML{*val tyenv_match = let
 val pat = @{typ_pat "?'a * ?'b"}
 @{ML_response_fake [display,gray]
 "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}.
 @{ML_response_fake [display, gray]
 "Envir.subst_type tyenv_match @{typ_pat \"?'a * ?'b\"}"
 Sign.typ_match @{theory} (pat, ty) Vartab.empty
 end*}
 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
+which does not solve the matching problem, and if
-we apply @{ML subst_type in Envir} to the unifyier we obtain
+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"}.
 This file also includes the substitution and normalisation functions,
 that apply a type environment to a type. Type environments are lookup
 \end{readmore}
 *}
 text {*
 Unification and matching of terms is substantially more complicated than the
-type-case. The reason is that terms have abstractions and unification
+type-case. The reason is that terms have abstractions and, in this context,
-or matching modulo plain equality is often not meaningful in this
+unification or matching modulo plain equality is often not meaningful.
-context. Nevertheless, Isabelle implements the function @{ML_ind
+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"}:
 *}
 end *}
 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"
 "[?X := P, ?Y := \<lambda>a b. Q b a]"}
 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
+subst_term in Envir} is for matchers and @{ML norm_term in Envir} for
-unifyiers). The function @{ML subst_term in Envir} expects a type environment,
+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]
 "let
 val trm = @{term_pat \"(?X::(nat\<Rightarrow>nat\<Rightarrow>nat)\<Rightarrow>bool) ?Y\"}
 "P (\<lambda>a b. Q b a)"}
 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]"}.
 @{ML_response_fake [display, gray]
 "let
 end"
 "[?X := P]"}
 *}
 text {*
-In the context of unifying abstractions, more thouroughly studied is
+Unification of abstractions is more thoroughly studied in the context
-higher-order pattern unification and higher-order pattern matching.  A
+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
+argument of another one and that a schematic variable is applied
-twice to the same bound variable. The function @{ML_ind pattern in Pattern}
+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 =
 [@{term_pat \"?X\"},              @{term_pat \"a\"},
 in
 map Pattern.pattern trm_list
 end"
 "[true, true, true, true, true, false, false, false]"}
-The point of restricting unification and matching to patterns is that
+The point of the restriction to patterns is that unification and matching
-it is decidable and produces most general unifiers. In this way
+are decidable and produce most general unifiers, respectively matchers.
-matching and unify can be implemented so that they produce a type
+In this way, matching and unification can be implemented as functions that
-and term environment (the latter actually produces only a term
+produce a type and term environment (unification actually returns a
-environment).
+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
-text {*
+\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}
 *}

changeset 383	72a53b07d264
parent 382	3f153aa4f231
child 384	0b24a016f6dd