isabelle-cookbook: comparison ProgTutorial/General.thy

equal deleted inserted replaced

-:5f7ca76f94e3
+:5dcee4d751ad
 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
+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
 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
 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}]"}
+"[?'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"
 "1"}
 @{text "?X ?Y"}.
 *}
 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"}
+val trm_a = @{term "P::(nat\<Rightarrow>nat\<Rightarrow>nat)\<Rightarrow>bool"}
-$ @{term "\<lambda>a b. (Q::nat\<Rightarrow>nat\<Rightarrow>nat) b a"}
+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 {*
 In this example we annotated explicitly types because then
 the type environment is empty and can be ignored. The
 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 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
 val fo_pat = @{term_pat \"\<lambda>y. (?X::nat\<Rightarrow>bool) y\"}
 val trm = @{term \"\<lambda>x. (P::nat\<Rightarrow>bool) x\"}
 *}
 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
+distinct bound variables. This excludes terms where a schematic variable is an
-argument of another one and that a schematic variable is applied
+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.
 @{ML_response [display, gray]
 in
 pretty_env @{context} (Envir.term_env env)
 end"
 "[?X := \<lambda>y x. x, ?Y := \<lambda>x. x]"}
+The function @{ML_ind "Envir.empty"} generates a record with a specified
-An assumption of this function is that the terms to be unified have
+max-index for the schematic variables (in the example the index is @{text
-already the same type. In case of failure, the exceptions that are raised
+0}) and empty type and term environments. The function @{ML_ind
-are either @{text Pattern}, @{text MATCH} or @{text Unif}.
+"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
-As mentioned before, ``full'' higher-order unification, respectively
+this function is that the terms to be unified have already the same type. In
-higher-order matching problems, are in general undecidable and might also not posses a
+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
+ML{*val uni_seq =
-In case of failure this function does not raise an exception, rather returns
+let
-the empty sequence. In order to find a reasonable solution for a unification
+val trm1 = @{term_pat "?X ?Y"}
-problem, Isabelle also tries first to solve the problem by higher-order
+val trm2 = @{term "f a"}
-pattern unification. For higher-order matching the function is called
+val init = Envir.empty 0
-@{ML_ind matchers in Unify}. Also this function might potentially return
+in
-sequences with more than one matcher.
+Unify.unifiers (@{theory}, init, [(trm1, trm2)])
+end *}
-\ldots
+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
+in case of failure, but returns an empty sequence. It also first tries
-can be solved by first-order matching.
+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
 for terms. Full higher-order unification is implemented
 section {* Managing Name Spaces (TBD) *}
 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 {*
 \begin{conventions}
 \begin{itemize}

changeset 387	5dcee4d751ad
parent 386	5f7ca76f94e3
child 388	0b337dedc306