# HG changeset patch
# User paulson
# Date 1077283371 -3600
# Node ID 32d1526d32370846ca4bc91eb4811bc67d8fa4f2
# Parent  4201e19164820e38c6af810f4eb4710978b1e079
new "where" section

diff -r 4201e1916482 -r 32d1526d3237 doc-src/TutorialI/Rules/Forward.thy
--- a/doc-src/TutorialI/Rules/Forward.thy	Fri Feb 20 01:32:59 2004 +0100
+++ b/doc-src/TutorialI/Rules/Forward.thy	Fri Feb 20 14:22:51 2004 +0100
@@ -58,9 +58,22 @@
 lemmas gcd_mult_0 = gcd_mult_distrib2 [of k 1];
 lemmas gcd_mult_1 = gcd_mult_0 [simplified];
 
+lemmas where1 = gcd_mult_distrib2 [where m=1]
+
+lemmas where2 = gcd_mult_distrib2 [where m=1 and k=1]
+
+lemmas where3 = gcd_mult_distrib2 [where m=1 and k="j+k"]
+
 text {*
+example using ``of'':
 @{thm[display] gcd_mult_distrib2 [of _ 1]}
 
+example using ``where'':
+@{thm[display] gcd_mult_distrib2 [where m=1]}
+
+example using ``where'', ``and'':
+@{thm[display] gcd_mult_distrib2 [where m=1 and k="j+k"]}
+
 @{thm[display] gcd_mult_0}
 \rulename{gcd_mult_0}
 
diff -r 4201e1916482 -r 32d1526d3237 doc-src/TutorialI/Rules/rules.tex
--- a/doc-src/TutorialI/Rules/rules.tex	Fri Feb 20 01:32:59 2004 +0100
+++ b/doc-src/TutorialI/Rules/rules.tex	Fri Feb 20 14:22:51 2004 +0100
@@ -1800,7 +1800,7 @@
 Forward proof means deriving new facts from old ones.  It is  the
 most fundamental type of proof.  Backward proof, by working  from goals to
 subgoals, can help us find a difficult proof.  But it is
-not always the best way of presenting the proof so found.  Forward
+not always the best way of presenting the proof thus found.  Forward
 proof is particularly good for reasoning from the general
 to the specific.  For example, consider this distributive law for
 the greatest common divisor:
@@ -1816,7 +1816,8 @@
 Re-orientation works by applying the symmetry of equality to 
 an equation, so it too is a forward step.  
 
-\subsection{Modifying a Theorem using {\tt\slshape of} and {\tt\slshape THEN}}
+\subsection{Modifying a Theorem using {\tt\slshape of},  {\tt\slshape where}
+ and {\tt\slshape THEN}}
 
 Let us reproduce our examples in Isabelle.  Recall that in
 {\S}\ref{sec:recdef-simplification} we declared the recursive function
@@ -1852,18 +1853,31 @@
 \begin{isabelle}
 \ \ \ \ \ k\ *\ gcd\ (1,\ ?n)\ =\ gcd\ (k\ *\ 1,\ k\ *\ ?n)
 \end{isabelle}
-Something is odd: {\isa{k}} is an ordinary variable, while {\isa{?n}} 
+Something is odd: \isa{k} is an ordinary variable, while \isa{?n} 
 is schematic.  We did not specify an instantiation 
-for {\isa{?n}}.  In its present form, the theorem does not allow 
-substitution for {\isa{k}}.  One solution is to avoid giving an instantiation for
+for \isa{?n}.  In its present form, the theorem does not allow 
+substitution for \isa{k}.  One solution is to avoid giving an instantiation for
 \isa{?k}: instead of a term we can put an underscore~(\isa{_}).  For example,
 \begin{isabelle}
 \ \ \ \ \ gcd_mult_distrib2\ [of\ _\ 1]
 \end{isabelle}
 replaces \isa{?m} by~\isa{1} but leaves \isa{?k} unchanged.  
 
-The next step is to put
-the theorem \isa{gcd_mult_0} into a simplified form, performing the steps 
+An equivalent solution is to use the attribute \isa{where}. 
+\begin{isabelle}
+\ \ \ \ \ gcd\_mult\_distrib2\ [where\ m=1]
+\end{isabelle}
+While \isa{of} refers to
+variables by their position, \isa{where} refers to variables by name. Multiple
+instantiations are separated by~\isa{and}, as in this example:
+\begin{isabelle}
+\ \ \ \ \ gcd\_mult\_distrib2\ [where\ m=1\ and\ k=1]
+\end{isabelle}
+
+We now continue the present example with the version of \isa{gcd_mult_0}
+shown above, which has \isa{k} instead of \isa{?k}.
+Once we have replaced \isa{?m} by~1, we must next simplify
+the theorem \isa{gcd_mult_0}, performing the steps 
 $\gcd(1,n)=1$ and $k\times1=k$.  The \attrdx{simplified}
 attribute takes a theorem
 and returns the result of simplifying it, with respect to the default