arg_cong, tacticals, pr, defer, prefer
authorpaulson
Tue Jan 23 18:13:00 2001 +0100 (2001-01-23)
changeset 1096769937e62a28e
parent 10966 8f2c27041a8e
child 10968 4882d65cc716
arg_cong, tacticals, pr, defer, prefer
doc-src/TutorialI/Rules/rules.tex
     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.102 +required contradiction.
   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}