# HG changeset patch
# User paulson
# Date 985951756 -7200
# Node ID 6902638af59e72edf8a4c02875f39ac5c193a838
# Parent  34c81a796ee3d1d5ffae35c94e894a6df449221c
quantifier instantiation

diff -r 34c81a796ee3 -r 6902638af59e doc-src/TutorialI/Rules/Basic.thy
--- a/doc-src/TutorialI/Rules/Basic.thy	Fri Mar 30 12:31:10 2001 +0200
+++ b/doc-src/TutorialI/Rules/Basic.thy	Fri Mar 30 13:29:16 2001 +0200
@@ -223,10 +223,50 @@
 	--{* @{subgoals[display,indent=0,margin=65]} *}
 by (drule mp)
 
-
 lemma "\<lbrakk>\<forall>x. P x \<longrightarrow> P (f x); P a\<rbrakk> \<Longrightarrow> P(f (f a))"
 by blast
 
+
+text{*
+the existential quantifier*}
+
+text {*
+@{thm[display]"exI"}
+\rulename{exI}
+
+@{thm[display]"exE"}
+\rulename{exE}
+*};
+
+
+text{*
+instantiating quantifiers explicitly by rule_tac and erule_tac*}
+
+lemma "\<lbrakk>\<forall>x. P x \<longrightarrow> P (h x); P a\<rbrakk> \<Longrightarrow> P(h (h a))"
+apply (frule spec)
+	--{* @{subgoals[display,indent=0,margin=65]} *}
+apply (drule mp, assumption)
+	--{* @{subgoals[display,indent=0,margin=65]} *}
+apply (drule_tac x = "h a" in spec)
+	--{* @{subgoals[display,indent=0,margin=65]} *}
+by (drule mp)
+
+text {*
+@{thm[display]"dvd_def"}
+\rulename{dvd_def}
+*};
+
+lemma mult_dvd_mono: "\<lbrakk>i dvd m; j dvd n\<rbrakk> \<Longrightarrow> i*j dvd (m*n :: nat)"
+apply (simp add: dvd_def)
+	--{* @{subgoals[display,indent=0,margin=65]} *}
+apply (erule exE) 
+	--{* @{subgoals[display,indent=0,margin=65]} *}
+apply (erule exE) 
+	--{* @{subgoals[display,indent=0,margin=65]} *}
+apply (rule_tac x="k*ka" in exI) 
+apply simp
+done
+
 text{*
 Hilbert-epsilon theorems*}
 
diff -r 34c81a796ee3 -r 6902638af59e doc-src/TutorialI/Rules/Primes.thy
--- a/doc-src/TutorialI/Rules/Primes.thy	Fri Mar 30 12:31:10 2001 +0200
+++ b/doc-src/TutorialI/Rules/Primes.thy	Fri Mar 30 13:29:16 2001 +0200
@@ -15,11 +15,9 @@
 ML "IsarOutput.indent := 5"  (*that is, Doc/TutorialI/settings.ML*)
 
 
-text {*
-\begin{quote}
+text {*Now in Basic.thy!
 @{thm[display]"dvd_def"}
 \rulename{dvd_def}
-\end{quote}
 *};
 
 
diff -r 34c81a796ee3 -r 6902638af59e doc-src/TutorialI/Rules/rules.tex
--- a/doc-src/TutorialI/Rules/rules.tex	Fri Mar 30 12:31:10 2001 +0200
+++ b/doc-src/TutorialI/Rules/rules.tex	Fri Mar 30 13:29:16 2001 +0200
@@ -1008,13 +1008,53 @@
 \index{quantifiers!universal|)}  
 
 
+\subsection{The Existential Quantifier}
+
+\index{quantifiers!existential|(}%
+The concepts just presented also apply
+to the existential quantifier, whose introduction rule looks like this in
+Isabelle: 
+\begin{isabelle}
+?P\ ?x\ \isasymLongrightarrow\ {\isasymexists}x.\ ?P\ x\rulename{exI}
+\end{isabelle}
+If we can exhibit some $x$ such that $P(x)$ is true, then $\exists x.
+P(x)$ is also true.  It is a dual of the universal elimination rule, and
+logic texts present it using the same notation for substitution.
+
+The existential
+elimination rule looks like this
+in a logic text: 
+\[ \infer{Q}{\exists x.\,P & \infer*{Q}{[P]}} \]
+%
+It looks like this in Isabelle: 
+\begin{isabelle}
+\isasymlbrakk{\isasymexists}x.\ ?P\ x;\ \isasymAnd x.\ ?P\ x\ \isasymLongrightarrow\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?Q\rulename{exE}
+\end{isabelle}
+%
+Given an existentially quantified theorem and some
+formula $Q$ to prove, it creates a new assumption by removing the quantifier.  As with
+the universal introduction  rule, the textbook version imposes a proviso on the
+quantified variable, which Isabelle expresses using its meta-logic.  Note that it is
+enough to have a universal quantifier in the meta-logic; we do not need an existential
+quantifier to be built in as well.
+ 
+
+\begin{exercise}
+Prove the lemma
+\[ \exists x.\, P\conj Q(x)\Imp P\conj(\exists x.\, Q(x)). \]
+\emph{Hint}: the proof is similar 
+to the one just above for the universal quantifier. 
+\end{exercise}
+\index{quantifiers|)}\index{quantifiers!existential|)}
+
+
 \subsection{Renaming an Assumption: {\tt\slshape rename_tac}}
 
 \index{assumptions!renaming|(}\index{*rename_tac|(}%
 When you apply a rule such as \isa{allI}, the quantified variable
 becomes a new bound variable of the new subgoal.  Isabelle tries to avoid
 changing its name, but sometimes it has to choose a new name in order to
-avoid a clash.  Here is a contrived example:
+avoid a clash.  The result may not be ideal:
 \begin{isabelle}
 \isacommand{lemma}\ "x\ <\ y\ \isasymLongrightarrow \ \isasymforall x\ y.\ P\ x\
 (f\ y)"\isanewline
@@ -1097,48 +1137,107 @@
 of the desired assumption, \isa{P(h(h~a))}.  The \isacommand{by}
 command forces Isabelle to backtrack until it finds the correct one.
 Alternatively, we could have used the \isacommand{apply} command and bundled the
-\isa{drule mp} with \emph{two} calls of \isa{assumption}.%
+\isa{drule mp} with \emph{two} calls of \isa{assumption}.  Or, of course,
+we could have given the entire proof to \isa{auto}.%
 \index{assumptions!reusing|)}\index{*frule|)}
 
 
-\subsection{The Existential Quantifier}
+
+\subsection{Instantiating a Quantifier Explicitly}
+\index{quantifiers!instantiating}
 
-\index{quantifiers!existential|(}%
-The concepts just presented also apply
-to the existential quantifier, whose introduction rule looks like this in
-Isabelle: 
+We can prove a theorem of the form $\exists x.\,P\, x$ by exhibiting a
+suitable term~$t$ such that $P\,t$ is true.  Dually, we can use an
+assumption of the form $\forall x.\,P\, x$ by exhibiting a
+suitable term~$t$ such that $P\,t$ is false, or (more generally)
+that contributes in some way to the proof at hand.  In many cases, 
+Isabelle makes the correct choice automatically, constructing the term by
+unification.  In other cases, the required term is not obvious and we must
+specify it ourselves.  Suitable methods are \isa{rule_tac}, \isa{drule_tac}
+and \isa{erule_tac}.
+
+We have just seen a proof of this lemma:
 \begin{isabelle}
-?P\ ?x\ \isasymLongrightarrow\ {\isasymexists}x.\ ?P\ x\rulename{exI}
+\isacommand{lemma}\ "\isasymlbrakk \isasymforall x.\ P\ x\
+\isasymlongrightarrow \ P\ (h\ x);\ P\ a\isasymrbrakk \
+\isasymLongrightarrow \ P(h\ (h\ a))"
 \end{isabelle}
-If we can exhibit some $x$ such that $P(x)$ is true, then $\exists x.
-P(x)$ is also true.  It is a dual of the universal elimination rule, and
-logic texts present it using the same notation for substitution.
-
-The existential
-elimination rule looks like this
-in a logic text: 
-\[ \infer{Q}{\exists x.\,P & \infer*{Q}{[P]}} \]
-%
-It looks like this in Isabelle: 
+We had reached this subgoal:
 \begin{isabelle}
-\isasymlbrakk{\isasymexists}x.\ ?P\ x;\ \isasymAnd x.\ ?P\ x\ \isasymLongrightarrow\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?Q\rulename{exE}
+\ 1.\ \isasymlbrakk{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ (h\
+x);\ P\ a;\ P\ (h\ a)\isasymrbrakk\ \isasymLongrightarrow\ P\ (h\ (h\ a))
 \end{isabelle}
 %
-Given an existentially quantified theorem and some
-formula $Q$ to prove, it creates a new assumption by removing the quantifier.  As with
-the universal introduction  rule, the textbook version imposes a proviso on the
-quantified variable, which Isabelle expresses using its meta-logic.  Note that it is
-enough to have a universal quantifier in the meta-logic; we do not need an existential
-quantifier to be built in as well.
- 
+The proof requires instantiating the quantified assumption with the
+term~\isa{h~a}.
+\begin{isabelle}
+\isacommand{apply}\ (drule_tac\ x\ =\ "h\ a"\ \isakeyword{in}\
+spec)\isanewline
+\ 1.\ \isasymlbrakk P\ a;\ P\ (h\ a);\ P\ (h\ a)\ \isasymlongrightarrow \
+P\ (h\ (h\ a))\isasymrbrakk \ \isasymLongrightarrow \ P\ (h\ (h\ a))
+\end{isabelle}
+We have forced the desired instantiation.
+
+\medskip
+Existential formulas can be instantiated too.  The next example uses the 
+\emph{divides} relation of number theory: 
+\begin{isabelle}
+?m\ dvd\ ?n\ \isasymequiv\ {\isasymexists}k.\ ?n\ =\ ?m\ *\ k
+\rulename{dvd_def}
+\end{isabelle}
 
-\begin{exercise}
-Prove the lemma
-\[ \exists x.\, P\conj Q(x)\Imp P\conj(\exists x.\, Q(x)). \]
-\emph{Hint}: the proof is similar 
-to the one just above for the universal quantifier. 
-\end{exercise}
-\index{quantifiers|)}\index{quantifiers!existential|)}
+Let us prove that multiplication of natural numbers is monotone with
+respect to the divides relation:
+\begin{isabelle}
+\isacommand{lemma}\ mult_dvd_mono:\ "{\isasymlbrakk}i\ dvd\ m;\ j\ dvd\
+n\isasymrbrakk\ \isasymLongrightarrow\ i*j\ dvd\ (m*n\ ::\ nat)"\isanewline
+\isacommand{apply}\ (simp\ add:\ dvd_def)
+\end{isabelle}
+%
+Opening the definition of divides leaves this subgoal:
+\begin{isabelle}
+\ 1.\ \isasymlbrakk \isasymexists k.\ m\ =\ i\ *\ k;\ \isasymexists k.\ n\
+=\ j\ *\ k\isasymrbrakk \ \isasymLongrightarrow \ \isasymexists k.\ m\ *\
+n\ =\ i\ *\ j\ *\ k%
+\isanewline
+\isacommand{apply}\ (erule\ exE)\isanewline
+\ 1.\ \isasymAnd k.\ \isasymlbrakk \isasymexists k.\ n\ =\ j\ *\ k;\ m\ =\
+i\ *\ k\isasymrbrakk \ \isasymLongrightarrow \ \isasymexists k.\ m\ *\ n\
+=\ i\ *\ j\ *\ k%
+\isanewline
+\isacommand{apply}\ (erule\ exE)
+\end{isabelle}
+%
+Eliminating the two existential quantifiers in the assumptions leaves this
+subgoal:
+\begin{isabelle}
+\ 1.\ \isasymAnd k\ ka.\ \isasymlbrakk m\ =\ i\ *\ k;\ n\ =\ j\ *\
+ka\isasymrbrakk \ \isasymLongrightarrow \ \isasymexists k.\ m\ *\ n\ =\ i\
+*\ j\ *\ k
+\end{isabelle}
+%
+The term needed to instantiate the remaining quantifier is~\isa{k*ka}:
+\begin{isabelle}
+\isacommand{apply}\ (rule_tac\ x="k*ka"\ \isakeyword{in}\ exI)\ \isanewline
+\ 1.\ \isasymAnd k\ ka.\ \isasymlbrakk m\ =\ i\ *\ k;\ n\ =\ j\ *\
+ka\isasymrbrakk \ \isasymLongrightarrow \ m\ *\ n\ =\ i\
+*\ j\ *\ (k\ *\ ka)
+\end{isabelle}
+%
+The rest is automatic, by arithmetic.
+\begin{isabelle}
+\isacommand{apply}\ simp\isanewline
+\isacommand{done}\isanewline
+\end{isabelle}
+
+\begin{warn}
+References to automatically-generated names like~\isa{ka} can make a proof
+brittle, especially if the proof is long.  Small changes to your theory can
+cause these names to change.  Robust proofs replace
+automatically-generated names by ones chosen using
+\isa{rename_tac} before giving them to \isa{rule_tac}.
+\end{warn}
+
 
 
 \section{Hilbert's Epsilon-Operator}
@@ -1824,8 +1923,8 @@
 rule by specifying values for its variables.  Analogous is \isa{OF}, which
 generates an instance of a rule by specifying facts for its premises.  
 
-Below we shall need the 
-\emph{divides} relation of number theory: 
+We again need the 
+\emph{divides} relation of number theory, which as we recall is defined by 
 \begin{isabelle}
 ?m\ dvd\ ?n\ \isasymequiv\ {\isasymexists}k.\ ?n\ =\ ?m\ *\ k
 \rulename{dvd_def}