doc-src/TutorialI/Rules/rules.tex
 changeset 10967 69937e62a28e parent 10887 7fb42b97413a child 10971 6852682eaf16
     1.1 --- a/doc-src/TutorialI/Rules/rules.tex	Tue Jan 23 18:05:53 2001 +0100
1.2 +++ b/doc-src/TutorialI/Rules/rules.tex	Tue Jan 23 18:13:00 2001 +0100
1.3 @@ -749,7 +749,6 @@
1.4  \end{isabelle}
1.5  The first step invokes the rule by applying the method \isa{rule allI}.
1.6  \begin{isabelle}
1.7 -%{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ x\isanewline
1.8  \ 1.\ \isasymAnd x.\ P\ x\ \isasymlongrightarrow\ P\ x
1.9  \end{isabelle}
1.10  Note  that the resulting proof state has a bound variable,
1.11 @@ -814,7 +813,7 @@
1.12  rules add bound variables or assumptions.
1.13
1.14  Now, to reason from the universally quantified
1.15 -assumption, we apply the elimination rule using the {\isa{drule}}
1.16 +assumption, we apply the elimination rule using the \isa{drule}
1.17  method.  This rule is called \isa{spec} because it specializes a universal formula
1.18  to a particular term.
1.19  \begin{isabelle}
1.20 @@ -841,7 +840,38 @@
1.21  be identical to the conclusion, provided the two formulas are unifiable.
1.22
1.23
1.24 -\subsection{Re-using an Assumption: the {\tt\slshape frule} Method}
1.25 +\subsection{Renaming an Assumption: {\tt\slshape rename_tac}}
1.26 +
1.27 +When you apply a rule such as \isa{allI}, the quantified variable becomes a new
1.28 +bound variable of the new subgoal.  Isabelle tries to avoid changing its name, but
1.29 +sometimes it has to choose a new name in order to avoid a clash.  Here is a
1.30 +contrived example:
1.31 +\begin{isabelle}
1.32 +\isacommand{lemma}\ "x\ <\ y\ \isasymLongrightarrow \ \isasymforall x\ y.\ P\ x\
1.33 +(f\ y)"\isanewline
1.34 +\isacommand{apply}\ intro\isanewline
1.35 +\ 1.\ \isasymAnd xa\ ya.\ x\ <\ y\ \isasymLongrightarrow \ P\ xa\ (f\ ya)
1.36 +\end{isabelle}
1.37 +%
1.38 +The names \isa{x} and \isa{y} were already in use, so the new bound variables are
1.39 +called \isa{xa} and~\isa{ya}.  You can rename them by invoking \isa{rename_tac}:
1.40 +
1.41 +\begin{isabelle}
1.42 +\isacommand{apply}\ (rename_tac\ v\ w)\isanewline
1.43 +\ 1.\ \isasymAnd v\ w.\ x\ <\ y\ \isasymLongrightarrow \ P\ v\ (f\ w)
1.44 +\end{isabelle}
1.45 +Recall that \isa{rule_tac}\index{rule_tac|and renaming} instantiates a
1.46 +theorem with specified terms.  These terms may involve the goal's bound
1.47 +variables, but beware of referring to  variables
1.48 +like~\isa{xa}.  A future change to your theories could change the set of names
1.49 +produced at top level, so that \isa{xa} changes to~\isa{xb} or reverts to~\isa{x}.
1.50 +It is safer to rename automatically-generated variables before mentioning them.
1.51 +
1.52 +If the subgoal has more bound variables than there are names given to
1.53 +\isa{rename_tac}, the rightmost ones are renamed.
1.54 +
1.55 +
1.56 +\subsection{Reusing an Assumption: {\tt\slshape frule}}
1.57
1.58  Note that \isa{drule spec} removes the universal quantifier and --- as
1.59  usual with elimination rules --- discards the original formula.  Sometimes, a
1.60 @@ -1840,8 +1870,58 @@
1.61
1.62  \section{Methods for Forward Proof}
1.63
1.64 -We have seen that forward proof works well within a backward
1.65 -proof.  Also in that spirit is the \isa{insert} method, which inserts a
1.66 +We have seen that the forward proof directives work well within a backward
1.67 +proof.  There are many ways to achieve a forward style, using our existing
1.68 +proof methods and some additional ones that we introduce below.
1.69 +
1.70 +The methods \isa{drule}, \isa{frule}, \isa{drule_tac}, etc.,
1.71 +reason forward from a subgoal.  We have seen them already, using rules such as
1.72 +\isa{mp} and
1.73 +\isa{spec} to operate on formulae.  They can also operate on terms, using rules
1.74 +such as these:
1.75 +\begin{isabelle}
1.76 +x\ =\ y\ \isasymLongrightarrow \ f\ x\ =\ f\ y%
1.77 +\rulename{arg_cong}\isanewline
1.78 +i\ \isasymle \ j\ \isasymLongrightarrow \ i\ *\ k\ \isasymle \ j\ *\ k%
1.79 +\rulename{mult_le_mono1}
1.80 +\end{isabelle}
1.81 +
1.82 +For example, let us prove a fact about divisibility in the natural numbers:
1.83 +\begin{isabelle}
1.84 +\isacommand{lemma}\ "\#2\ \isasymle \ u\ \isasymLongrightarrow \ u*m\ \isasymnoteq
1.85 +\ Suc(u*n)"\isanewline
1.86 +\isacommand{apply}\ intro\isanewline
1.87 +\ 1.\ \isasymlbrakk \#2\ \isasymle \ u;\ u\ *\ m\ =\ Suc\ (u\ *\ n)\isasymrbrakk \ \isasymLongrightarrow \ False%
1.88 +\end{isabelle}
1.89 +%
1.90 +The key step is to apply the function \ldots\isa{mod\ u} to both sides of the
1.91 +equation
1.92 +\isa{u*m\ =\ Suc(u*n)}:
1.93 +
1.94 +\begin{isabelle}
1.95 +\isacommand{apply}\ (drule_tac\ f="\isasymlambda x.\ x\ mod\ u"\ \isakeyword{in}\
1.96 +arg_cong)\isanewline
1.97 +\ 1.\ \isasymlbrakk \#2\ \isasymle \ u;\ u\ *\ m\ mod\ u\ =\ Suc\ (u\ *\ n)\ mod\
1.98 +u\isasymrbrakk \ \isasymLongrightarrow \ False
1.99 +\end{isabelle}
1.100 +%
1.101 +Simplification reduces the left side to 0 and the right side to~1, yielding the
1.103 +\begin{isabelle}
1.104 +\isacommand{apply}\ (simp\ add:\ mod_Suc)\isanewline
1.105 +\isacommand{done}
1.106 +\end{isabelle}
1.107 +
1.108 +Our proof has used a fact about remainder:
1.109 +\begin{isabelle}
1.110 +Suc\ m\ mod\ n\ =\isanewline
1.111 +(if\ Suc\ (m\ mod\ n)\ =\ n\ then\ 0\ else\ Suc\ (m\ mod\ n))
1.112 +\rulename{mod_Suc}
1.113 +\end{isabelle}
1.114 +
1.115 +\medskip
1.116 +The methods designed for supporting forward reasoning are \isa{insert} and
1.117 +\isa{subgoal_tac}.  The \isa{insert} method inserts a
1.118  given theorem as a new assumption of the current subgoal.  This already
1.119  is a forward step; moreover, we may (as always when using a theorem) apply
1.120  \isa{of}, \isa{THEN} and other directives.  The new assumption can then
1.121 @@ -1988,3 +2068,167 @@
1.122  \item {\isa{subgoal_tac}} adds a formula as a new assumption and leaves the
1.123  subgoal of proving that formula
1.124  \end{itemize}
1.125 +
1.126 +
1.127 +\section{Managing Large Proofs}
1.128 +
1.129 +Naturally you should try to divide proofs into manageable parts.  Look for lemmas
1.130 +that can be proved separately.  Sometimes you will observe that they are
1.131 +instances of much simpler facts.  On other occasions, no lemmas suggest themselves
1.132 +and you are forced to cope with a long proof involving many subgoals.
1.133 +
1.134 +\subsection{Tacticals, or Control Structures}
1.135 +
1.136 +If the proof is long, perhaps it at least has some regularity.  Then you can
1.137 +express it more concisely using \textbf{tacticals}, which provide control
1.138 +structures.  Here is a proof (it would be a one-liner using
1.139 +\isa{blast}, but forget that) that contains a series of repeated
1.140 +commands:
1.141 +%
1.142 +\begin{isabelle}
1.143 +\isacommand{lemma}\ "\isasymlbrakk P\isasymlongrightarrow Q;\
1.144 +Q\isasymlongrightarrow R;\ R\isasymlongrightarrow S;\ P\isasymrbrakk \
1.145 +\isasymLongrightarrow \ S"\isanewline
1.146 +\isacommand{apply}\ (drule\ mp,\ assumption)\isanewline
1.147 +\isacommand{apply}\ (drule\ mp,\ assumption)\isanewline
1.148 +\isacommand{apply}\ (drule\ mp,\ assumption)\isanewline
1.149 +\isacommand{apply}\ (assumption)\isanewline
1.150 +\isacommand{done}
1.151 +\end{isabelle}
1.152 +%
1.153 +Each of the three identical commands finds an implication and proves its
1.154 +antecedent by assumption.  The first one finds \isa{P\isasymlongrightarrow Q} and
1.155 +\isa{P}, concluding~\isa{Q}; the second one concludes~\isa{R} and the third one
1.156 +concludes~\isa{S}.  The final step matches the assumption \isa{S} with the goal to
1.157 +be proved.
1.158 +
1.159 +Suffixing a method with a plus sign~(\isa+)
1.160 +expresses one or more repetitions:
1.161 +\begin{isabelle}
1.162 +\isacommand{lemma}\ "\isasymlbrakk P\isasymlongrightarrow Q;\ Q\isasymlongrightarrow R;\ R\isasymlongrightarrow S;\ P\isasymrbrakk \ \isasymLongrightarrow \ S"\isanewline
1.163 +\isacommand{by}\ (drule\ mp,\ assumption)+
1.164 +\end{isabelle}
1.165 +%
1.166 +Using \isacommand{by} takes care of the final use of \isa{assumption}.  The new
1.167 +proof is more concise.  It is also more general: the repetitive method works
1.168 +for a chain of implications having any length, not just three.
1.169 +
1.170 +Choice is another control structure.  Separating two methods by a vertical
1.171 +bar~(\isa|) gives the effect of applying the first method, and if that fails,
1.172 +trying the second.  It can be combined with repetition, when the choice must be
1.173 +made over and over again.  Here is a chain of implications in which most of the
1.174 +antecedents are proved by assumption, but one is proved by arithmetic:
1.175 +\begin{isabelle}
1.176 +\isacommand{lemma}\ "\isasymlbrakk Q\isasymlongrightarrow R;\ P\isasymlongrightarrow Q;\ x<\#5\isasymlongrightarrow P;\
1.177 +Suc\ x\ <\ \#5\isasymrbrakk \ \isasymLongrightarrow \ R"\ \isanewline
1.178 +\isacommand{by}\ (drule\ mp,\ (assumption|arith))+
1.179 +\end{isabelle}
1.180 +The \isa{arith}
1.181 +method can prove $x<5$ from $x+1<5$, but it cannot duplicate the effect of
1.182 +\isa{assumption}.  Therefore, we combine these methods using the choice
1.183 +operator.
1.184 +
1.185 +A postfixed question mark~(\isa?) expresses zero or one repetitions of a method.
1.186 +It can also be viewed as the choice between executing a method and doing nothing.
1.187 +It is useless at top level but may be valuable within other control structures.
1.188 +
1.189 +
1.190 +\subsection{Subgoal Numbering}
1.191 +
1.192 +Another problem in large proofs is contending with huge
1.193 +subgoals or many subgoals.  Induction can produce a proof state that looks
1.194 +like this:
1.195 +\begin{isabelle}
1.196 +\ 1.\ bigsubgoal1\isanewline
1.197 +\ 2.\ bigsubgoal2\isanewline
1.198 +\ 3.\ bigsubgoal3\isanewline
1.199 +\ 4.\ bigsubgoal4\isanewline
1.200 +\ 5.\ bigsubgoal5\isanewline
1.201 +\ 6.\ bigsubgoal6
1.202 +\end{isabelle}
1.203 +If each \isa{bigsubgoal} is 15 lines or so, the proof state will be too big to
1.204 +scroll through.  By default, Isabelle displays at most 10 subgoals.  The
1.205 +\isacommand{pr} command lets you change this limit:
1.206 +\begin{isabelle}
1.207 +\isacommand{pr}\ 2\isanewline
1.208 +\ 1.\ bigsubgoal1\isanewline
1.209 +\ 2.\ bigsubgoal2\isanewline
1.210 +A total of 6 subgoals...
1.211 +\end{isabelle}
1.212 +
1.213 +\medskip
1.214 +All methods apply to the first subgoal.
1.215 +Sometimes, not only in a large proof, you may want to focus on some other
1.216 +subgoal.  Then you should try the commands \isacommand{defer} or \isacommand{prefer}.
1.217 +
1.218 +In the following example, the first subgoal looks hard, while the others
1.219 +look as if \isa{blast} alone could prove them:
1.220 +%\begin{isabelle}
1.221 +%\isacommand{lemma}\ "hard\ \isasymand \ (P\ \isasymor \ \isachartilde P)\ \isasymand \ (Q\isasymlongrightarrow Q)"\isanewline
1.222 +%\isacommand{apply}\ intro
1.223 +%\end{isabelle}
1.224 +\begin{isabelle}
1.225 +\ 1.\ hard\isanewline
1.226 +\ 2.\ \isasymnot \ \isasymnot \ P\ \isasymLongrightarrow \ P\isanewline
1.227 +\ 3.\ Q\ \isasymLongrightarrow \ Q%
1.228 +\end{isabelle}
1.229 +%
1.230 +The \isacommand{defer} command moves the first subgoal into the last position.
1.231 +\begin{isabelle}
1.232 +\isacommand{defer}\ 1\isanewline
1.233 +\ 1.\ \isasymnot \ \isasymnot \ P\ \isasymLongrightarrow \ P\isanewline
1.234 +\ 2.\ Q\ \isasymLongrightarrow \ Q\isanewline
1.235 +\ 3.\ hard%
1.236 +\end{isabelle}
1.237 +%
1.238 +Now we apply \isa{blast} repeatedly to the easy subgoals:
1.239 +\begin{isabelle}
1.240 +\isacommand{apply}\ blast+\isanewline
1.241 +\ 1.\ hard%
1.242 +\end{isabelle}
1.243 +Using \isacommand{defer}, we have cleared away the trivial parts of the proof so
1.244 +that we can devote attention to the difficult part.
1.245 +
1.246 +\medskip
1.247 +The \isacommand{prefer} command moves the specified subgoal into the
1.248 +first position.  For example, if you suspect that one of your subgoals is
1.249 +invalid (not a theorem), then you should investigate that subgoal first.  If it
1.250 +cannot be proved, then there is no point in proving the other subgoals.
1.251 +\begin{isabelle}
1.252 +\ 1.\ ok1\isanewline
1.253 +\ 2.\ ok2\isanewline
1.254 +\ 3.\ doubtful%
1.255 +\end{isabelle}
1.256 +%
1.257 +We decide to work on the third subgoal.
1.258 +\begin{isabelle}
1.259 +\isacommand{prefer}\ 3\isanewline
1.260 +\ 1.\ doubtful\isanewline
1.261 +\ 2.\ ok1\isanewline
1.262 +\ 3.\ ok2
1.263 +\end{isabelle}
1.264 +If we manage to prove \isa{doubtful}, then we can work on the other
1.265 +subgoals, confident that we are not wasting our time.  Finally we revise the
1.266 +proof script to remove the \isacommand{prefer} command, since we needed it only to
1.267 +focus our exploration.  The previous example is different: its use of
1.268 +\isacommand{defer} stops trivial subgoals from cluttering the rest of the
1.269 +proof.  Even there, we should consider proving \isa{hard} as a preliminary
1.270 +lemma.  Always seek ways to streamline your proofs.
1.271 +
1.272 +
1.273 +\medskip
1.274 +Summary:
1.275 +\begin{itemize}
1.276 +\item the control structures \isa+, \isa? and \isa| help express complicated proofs
1.277 +\item the \isacommand{pr} command can limit the number of subgoals to display
1.278 +\item the \isacommand{defer} and \isacommand{prefer} commands move a
1.279 +subgoal to the last or first position
1.280 +\end{itemize}
1.281 +
1.282 +\begin{exercise}
1.283 +This proof uses \isa? and \isa+ to \ldots{} can you explain?
1.284 +\begin{isabelle}
1.285 +\isacommand{lemma}\ "\isasymlbrakk P\isasymand Q\isasymlongrightarrow R;\ P\isasymlongrightarrow Q;\ P\isasymrbrakk \ \isasymLongrightarrow \ R"\isanewline
1.286 +\isacommand{by}\ (drule\ mp,\ intro?,\ assumption+)+
1.287 +\end{isabelle}
1.288 +\end{exercise}