author paulson Fri, 13 Dec 2002 16:49:08 +0100 changeset 13751 ac6a9c2f9fb2 parent 13750 b5cd10cb106b child 13752 a1290b92b1b0
trace_unify_fail
--- a/doc-src/TutorialI/Rules/rules.tex	Fri Dec 13 16:48:20 2002 +0100
+++ b/doc-src/TutorialI/Rules/rules.tex	Fri Dec 13 16:49:08 2002 +0100
@@ -618,14 +618,15 @@
\index{unification|(}%
As we have seen, Isabelle rules involve schematic variables, which begin with
a question mark and act as
-placeholders for terms.  \textbf{Unification} refers to  the process of
-making two terms identical, possibly by replacing their schematic variables by
+placeholders for terms.  \textbf{Unification} --- well known to Prolog programmers --- is the act of
+making two terms identical, possibly replacing their schematic variables by
terms.  The simplest case is when the two terms are already the same. Next
simplest is \textbf{pattern-matching}, which replaces variables in only one of the
terms.  The
\isa{rule} method typically  matches the rule's conclusion
-against the current subgoal.  In the most complex case,  variables in both
-terms are replaced; the \isa{rule} method can do this if the goal
+against the current subgoal.  The
+\isa{assumption} method matches the current subgoal's conclusion
+against each of its assumptions.   Unification can instantiate variables in both terms; the \isa{rule} method can do this if the goal
itself contains schematic variables.  Other occurrences of the variables in
the rule or proof state are updated at the same time.

@@ -633,18 +634,33 @@
as $\exists x.\,P$, they let us proceed with a proof.  They can be
filled in later, sometimes in stages and often automatically.

-Unification is well known to Prolog programmers. Isabelle uses
+If unification fails when you think it should succeed, try setting the flag \index{flags}\isa{trace_unify_fail}\index{* trace_unify_fail (flag)},
+which makes Isabelle show the cause of unification failures.  For example, suppose we are trying to prove this subgoal by assumption:
+\begin{isabelle}
+\ 1.\ P\ (a,\ f\ (b,\ g\ (e,\ a),\ b),\ a)\ \isasymLongrightarrow \ P\ (a,\ f\ (b,\ g\ (c,\ a),\ b),\ a)
+\end{isabelle}
+The \isa{assumption} method having failed, we try again with the flag set:
+\begin{isabelle}
+\isacommand{ML}\ "set\ trace\_unify\_fail"\isanewline
+\isacommand{apply} assumption
+\end{isabelle}
+Even in this trivial case, the output is unexpectedly verbose, but it yields the necessary information:
+\begin{isabelle}
+Clash: e =/= c\isanewline
+Clash: == =/= Trueprop
+\end{isabelle}
+
+Isabelle uses
\textbf{higher-order} unification, which works in the
-typed $\lambda$-calculus.  The general case is
-undecidable, but for our purposes, the differences from ordinary
-unification are straightforward.  It handles bound  variables
-correctly, avoiding capture.  The two terms \isa{{\isasymlambda}x.\ ?P} and
+typed $\lambda$-calculus.  The procedure requires search and is potentially
+undecidable.  For our purposes, however, the differences from ordinary
+unification are straightforward.  It handles bound variables
+correctly, avoiding capture.  The two terms
+\isa{{\isasymlambda}x.\ f(x,z)} and \isa{{\isasymlambda}y.\ f(y,z)} are
+trivially unifiable because they differ only by a bound variable renaming.  The two terms \isa{{\isasymlambda}x.\ ?P} and
\isa{{\isasymlambda}x.\ t x}  are not unifiable; replacing \isa{?P} by
\isa{t x} is forbidden because the free occurrence of~\isa{x} would become
-bound.  The two terms
-\isa{{\isasymlambda}x.\ f(x,z)} and \isa{{\isasymlambda}y.\ f(y,z)} are
-trivially unifiable because they differ only by a bound variable renaming.
-
Higher-order unification sometimes must invent