author | paulson |

Tue Jan 23 18:13:00 2001 +0100 (2001-01-23) | |

changeset 10967 | 69937e62a28e |

parent 10966 | 8f2c27041a8e |

child 10968 | 4882d65cc716 |

arg_cong, tacticals, pr, defer, prefer

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}