# HG changeset patch
# User paulson
# Date 1039794548 -3600
# Node ID ac6a9c2f9fb27a4c8184951f767a7780cf81b28f
# Parent  b5cd10cb106b6dfbe89efc76136c1decd59ac031
trace_unify_fail

diff -r b5cd10cb106b -r ac6a9c2f9fb2 doc-src/TutorialI/Rules/rules.tex
--- 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.
-
+bound.  Unfortunately, even if \isa{trace_unify_fail} is set, Isabelle displays no information about this type of failure.
 
 \begin{warn}
 Higher-order unification sometimes must invent