1.1 --- a/doc-src/TutorialI/Rules/rules.tex Thu Feb 22 18:03:11 2001 +0100
1.2 +++ b/doc-src/TutorialI/Rules/rules.tex Thu Feb 22 18:13:23 2001 +0100
1.3 @@ -475,8 +475,8 @@
1.4 %
1.5 There are two negated assumptions and we need to exchange the conclusion with the
1.6 second one. The method \isa{erule contrapos_np} would select the first assumption,
1.7 -which we do not want. So we specify the desired assumption explicitly, using
1.8 -\isa{erule_tac}. This is the resulting subgoal:
1.9 +which we do not want. So we specify the desired assumption explicitly
1.10 +using a new method, \isa{erule_tac}. This is the resulting subgoal:
1.11 \begin{isabelle}
1.12 \ 1.\ \isasymlbrakk{\isasymnot}\ (P\ \isasymlongrightarrow\ Q);\ \isasymnot\
1.13 R\isasymrbrakk\ \isasymLongrightarrow\ R\ \isasymlongrightarrow\ Q%
1.14 @@ -562,6 +562,64 @@
1.15 \index{negation|)}
1.16
1.17
1.18 +\section{Interlude: the Basic Methods for Rules}
1.19 +
1.20 +We have seen examples of many tactics that operate on individual rules. It
1.21 +may be helpful to review how they work given an arbitrary rule such as this:
1.22 +\[ \infer{Q}{P@1 & \ldots & P@n} \]
1.23 +Below, we refer to $P@1$ as the \textbf{major premise}. This concept
1.24 +applies only to elimination and destruction rules. These rules act upon an
1.25 +instance of their major premise, typically to replace it by other
1.26 +assumptions.
1.27 +
1.28 +Suppose that the rule above is called~\isa{R}\@. Here are the basic rule
1.29 +methods, most of which we have already seen:
1.30 +\begin{itemize}
1.31 +\item
1.32 +Method \isa{rule\ R} unifies~$Q$ with the current subgoal, which it
1.33 +replaces by $n$ new subgoals, to prove instances of $P@1$, \ldots,~$P@n$.
1.34 +This is backward reasoning and is appropriate for introduction rules.
1.35 +\item
1.36 +Method \isa{erule\ R} unifies~$Q$ with the current subgoal and
1.37 +simultaneously unifies $P@1$ with some assumption. The subgoal is
1.38 +replaced by the $n-1$ new subgoals of proving
1.39 +instances of $P@2$,
1.40 +\ldots,~$P@n$, with the matching assumption deleted. It is appropriate for
1.41 +elimination rules. The method
1.42 +\isa{(rule\ R,\ assumption)} is similar, but it does not delete an
1.43 +assumption.
1.44 +\item
1.45 +Method \isa{drule\ R} unifies $P@1$ with some assumption, which is
1.46 +then deleted. The subgoal is
1.47 +replaced by the $n-1$ new subgoals of proving $P@2$, \ldots,~$P@n$; an
1.48 +$n$th subgoal is like the original one but has an additional assumption: an
1.49 +instance of~$Q$. It is appropriate for destruction rules.
1.50 +\item
1.51 +Method \isa{frule\ R} is like \isa{drule\ R} except that the matching
1.52 +assumption is not deleted. (See \S\ref{sec:frule} below.)
1.53 +\end{itemize}
1.54 +
1.55 +When applying a rule, we can constrain some of its
1.56 +variables:
1.57 +\begin{isabelle}
1.58 +\ \ \ \ \ rule_tac\ $v@1$ = $t@1$ \isakeyword{and} \ldots \isakeyword{and}
1.59 +$v@k$ =
1.60 +$t@k$ \isakeyword{in} R
1.61 +\end{isabelle}
1.62 +This method behaves like \isa{rule R}, while instantiating the variables
1.63 +$v@1$, \ldots,
1.64 +$v@k$ as specified. We similarly have \isa{erule_tac}, \isa{drule_tac} and
1.65 +\isa{frule_tac}. These methods also let us specify which subgoal to
1.66 +operate on. By default it is the first subgoal, as with nearly all
1.67 +methods, but we can specify that rule \isa{R} should be applied to subgoal
1.68 +number~$i$:
1.69 +\begin{isabelle}
1.70 +\ \ \ \ \ rule_tac\ [$i$] R
1.71 +\end{isabelle}
1.72 +
1.73 +
1.74 +
1.75 +
1.76 \section{Unification and Substitution}\label{sec:unification}
1.77
1.78 \index{unification|(}%
1.79 @@ -570,7 +628,7 @@
1.80 placeholders for terms. \emph{Unification} refers to the process of
1.81 making two terms identical, possibly by replacing their schematic variables by
1.82 terms. The simplest case is when the two terms are already the same. Next
1.83 -simplest is when the variables in only one of the terms
1.84 +simplest is when the variables in only one of the term
1.85 are replaced; this is called pattern-matching. The
1.86 \isa{rule} method typically matches the rule's conclusion
1.87 against the current subgoal. In the most complex case, variables in both
1.88 @@ -612,7 +670,8 @@
1.89 \end{warn}
1.90
1.91
1.92 -\subsection{Substitution}
1.93 +\subsection{Substitution and the {\tt\slshape subst} Method}
1.94 +\label{sec:subst}
1.95
1.96 \index{substitution|(}%
1.97 Isabelle also uses function variables to express \emph{substitution}.
1.98 @@ -638,11 +697,44 @@
1.99 in which $s$ will be replaced by~$t$. The proof above requires
1.100 \isa{{\isasymlambda}x.~x=s}.
1.101
1.102 -The \isa{simp} method replaces equals by equals, but using the substitution
1.103 -rule gives us more control. Consider this proof:
1.104 +The \isa{simp} method replaces equals by equals, but the substitution
1.105 +rule gives us more control. The \isa{subst} method is the easiest way to
1.106 +use the substitution rule. Suppose a
1.107 +proof has reached this point:
1.108 +\begin{isabelle}
1.109 +\ 1.\ \isasymlbrakk P\ x\ y\ z;\ Suc\ x\ <\ y\isasymrbrakk \ \isasymLongrightarrow \ f\ z\ =\ x\ *\ y%
1.110 +\end{isabelle}
1.111 +Now we wish to apply a commutative law:
1.112 +\begin{isabelle}
1.113 +?m\ *\ ?n\ =\ ?n\ *\ ?m%
1.114 +\rulename{mult_commute}
1.115 +\end{isabelle}
1.116 +Isabelle rejects our first attempt:
1.117 +\begin{isabelle}
1.118 +apply (simp add: mult_commute)
1.119 +\end{isabelle}
1.120 +The simplifier notices the danger of looping and refuses to apply the
1.121 +rule.%
1.122 +\footnote{More precisely, it only applies such a rule if the new term is
1.123 +smaller under a specified ordering; here, \isa{x\ *\ y}
1.124 +is already smaller than
1.125 +\isa{y\ *\ x}.}
1.126 +%
1.127 +The \isa{subst} method applies \isa{mult_commute} exactly once.
1.128 +\begin{isabelle}
1.129 +\isacommand{apply}\ (subst\ mult_commute)\isanewline
1.130 +\ 1.\ \isasymlbrakk P\ x\ y\ z;\ Suc\ x\ <\ y\isasymrbrakk \
1.131 +\isasymLongrightarrow \ f\ z\ =\ y\ *\ x%
1.132 +\end{isabelle}
1.133 +As we wanted, \isa{x\ *\ y} has become \isa{y\ *\ x}.
1.134 +
1.135 +\medskip
1.136 +The \isa{subst} method is convenient, but to see how it works, let us
1.137 +examine an explicit use of the rule \isa{ssubst}.
1.138 +Consider this proof:
1.139 \begin{isabelle}
1.140 \isacommand{lemma}\
1.141 -"\isasymlbrakk \ x\ =\ f\ x;\ odd(f\ x)\ \isasymrbrakk\ \isasymLongrightarrow\
1.142 +"\isasymlbrakk x\ =\ f\ x;\ odd(f\ x)\isasymrbrakk\ \isasymLongrightarrow\
1.143 odd\ x"\isanewline
1.144 \isacommand{by}\ (erule\ ssubst)
1.145 \end{isabelle}
1.146 @@ -655,7 +747,7 @@
1.147 resulting subgoal is trivial by assumption, so the \isacommand{by} command
1.148 proves it implicitly.
1.149
1.150 -We are using the \isa{erule} method in a novel way. Hitherto,
1.151 +We are using the \isa{erule} method it in a novel way. Hitherto,
1.152 the conclusion of the rule was just a variable such as~\isa{?R}, but it may
1.153 be any term. The conclusion is unified with the subgoal just as
1.154 it would be with the \isa{rule} method. At the same time \isa{erule} looks
1.155 @@ -669,9 +761,8 @@
1.156 Higher-order unification can be tricky. Here is an example, which you may
1.157 want to skip on your first reading:
1.158 \begin{isabelle}
1.159 -\isacommand{lemma}\ "\isasymlbrakk \ x\ =\
1.160 -f\ x;\ triple\ (f\ x)\
1.161 -(f\ x)\ x\ \isasymrbrakk\
1.162 +\isacommand{lemma}\ "\isasymlbrakk x\ =\
1.163 +f\ x;\ triple\ (f\ x)\ (f\ x)\ x\isasymrbrakk\
1.164 \isasymLongrightarrow\ triple\ x\ x\ x"\isanewline
1.165 \isacommand{apply}\ (erule\ ssubst)\isanewline
1.166 \isacommand{back}\isanewline
1.167 @@ -729,8 +820,7 @@
1.168 This process continues until the first method produces an output that the
1.169 second method can use. We get a one-line proof of our example:
1.170 \begin{isabelle}
1.171 -\isacommand{lemma}\ "\isasymlbrakk \ x\ =\ f\ x;\ triple\ (f\ x)\ (f\ x)\ x\
1.172 -\isasymrbrakk\
1.173 +\isacommand{lemma}\ "\isasymlbrakk x\ =\ f\ x;\ triple\ (f\ x)\ (f\ x)\ x\isasymrbrakk\
1.174 \isasymLongrightarrow\ triple\ x\ x\ x"\isanewline
1.175 \isacommand{apply}\ (erule\ ssubst,\ assumption)\isanewline
1.176 \isacommand{done}
1.177 @@ -740,8 +830,7 @@
1.178 The \isacommand{by} command works too, since it backtracks when
1.179 proving subgoals by assumption:
1.180 \begin{isabelle}
1.181 -\isacommand{lemma}\ "\isasymlbrakk \ x\ =\ f\ x;\ triple\ (f\ x)\ (f\ x)\ x\
1.182 -\isasymrbrakk\
1.183 +\isacommand{lemma}\ "\isasymlbrakk x\ =\ f\ x;\ triple\ (f\ x)\ (f\ x)\ x\isasymrbrakk\
1.184 \isasymLongrightarrow\ triple\ x\ x\ x"\isanewline
1.185 \isacommand{by}\ (erule\ ssubst)
1.186 \end{isabelle}
1.187 @@ -754,8 +843,8 @@
1.188 Also available are {\isa{drule_tac}} and \isa{erule_tac}. Here we need
1.189 \isa{erule_tac} since above we used \isa{erule}.
1.190 \begin{isabelle}
1.191 -\isacommand{lemma}\ "\isasymlbrakk \ x\ =\ f\ x;\ triple\ (f\ x)\ (f\ x)\ x\ \isasymrbrakk\ \isasymLongrightarrow\ triple\ x\ x\ x"\isanewline
1.192 -\isacommand{by}\ (erule_tac\ P = "\isasymlambda u.\ P\ u\ u\ x"\
1.193 +\isacommand{lemma}\ "\isasymlbrakk x\ =\ f\ x;\ triple\ (f\ x)\ (f\ x)\ x\isasymrbrakk\ \isasymLongrightarrow\ triple\ x\ x\ x"\isanewline
1.194 +\isacommand{by}\ (erule_tac\ P = "\isasymlambda u.\ triple\ u\ u\ x"\
1.195 \isakeyword{in}\ ssubst)
1.196 \end{isabelle}
1.197 %
1.198 @@ -953,6 +1042,7 @@
1.199
1.200
1.201 \subsection{Reusing an Assumption: {\tt\slshape frule}}
1.202 +\label{sec:frule}
1.203
1.204 \index{assumptions!reusing|(}\index{*frule|(}%
1.205 Note that \isa{drule spec} removes the universal quantifier and --- as
1.206 @@ -1085,15 +1175,16 @@
1.207 A more challenging example illustrates how Isabelle/HOL defines the least-number
1.208 operator, which denotes the least \isa{x} satisfying~\isa{P}:
1.209 \begin{isabelle}
1.210 -(LEAST\ x.\ P\ x)\ = \ SOME\ x.\ P\ x\ \isasymand \ (\isasymforall y.\
1.211 -P\ y\ \isasymlongrightarrow \ x\ \isasymle \ y)
1.212 +(LEAST\ x.\ P\ x)\ = (SOME\ x.\ P\ x\ \isasymand \ (\isasymforall y.\
1.213 +P\ y\ \isasymlongrightarrow \ x\ \isasymle \ y))
1.214 \end{isabelle}
1.215 -
1.216 -Let us prove the counterpart of \isa{some_equality} for this operator.
1.217 -The first step merely unfolds the definitions:
1.218 +%
1.219 +Let us prove the counterpart of \isa{some_equality} for \isa{LEAST}\@.
1.220 +The first step merely unfolds the definitions (\isa{LeastM} is a
1.221 +auxiliary operator):
1.222 \begin{isabelle}
1.223 \isacommand{theorem}\ Least_equality:\isanewline
1.224 -\ \ \ \ \ "\isasymlbrakk \ P\ (k::nat);\ \ \isasymforall x.\ P\ x\ \isasymlongrightarrow \ k\ \isasymle \ x\ \isasymrbrakk \ \isasymLongrightarrow \ (LEAST\ x.\ P\ x)\ =\ k"\isanewline
1.225 +\ \ \ \ \ "\isasymlbrakk P\ (k::nat);\ \ \isasymforall x.\ P\ x\ \isasymlongrightarrow \ k\ \isasymle \ x\isasymrbrakk \ \isasymLongrightarrow \ (LEAST\ x.\ P\ x)\ =\ k"\isanewline
1.226 \isacommand{apply}\ (simp\ add:\ Least_def\ LeastM_def)\isanewline
1.227 %\ 1.\ \isasymlbrakk P\ k;\ \isasymforall x.\ P\ x\ \isasymlongrightarrow \ k\
1.228 %\isasymle \ x\isasymrbrakk \isanewline
1.229 @@ -1507,7 +1598,7 @@
1.230 Most important among these are \isa{fast} and \isa{best}. While \isa{blast}
1.231 searches for proofs using a built-in first-order reasoner, these
1.232 earlier methods search for proofs using standard Isabelle inference.
1.233 -That makes them slower but enables them to work correctly in the
1.234 +That makes them slower but enables them to work in the
1.235 presence of the more unusual features of Isabelle rules, such
1.236 as type classes and function unknowns. For example, recall the introduction rule
1.237 for Hilbert's $\varepsilon$-operator:
1.238 @@ -1719,6 +1810,12 @@
1.239 \isacommand{by}\ (rule\ gcd_mult\ [of\ k\ 1,\ simplified])
1.240 \end{isabelle}
1.241
1.242 +\begin{exercise}
1.243 +In \S\ref{sec:subst} the method \isa{subst\ mult_commute} was applied. How
1.244 +can we achieve the same effect using \isa{THEN} with the rule \isa{ssubst}?
1.245 +% answer rule (mult_commute [THEN ssubst])
1.246 +
1.247 +\end{exercise}
1.248
1.249 \subsection{The {\tt\slshape OF} Directive}
1.250
1.251 @@ -1880,8 +1977,7 @@
1.252 \begin{isabelle}
1.253 \isacommand{lemma}\
1.254 relprime_dvd_mult:\isanewline
1.255 -\ \ \ \ \ \ \ "\isasymlbrakk \ gcd(k,n){=}1;\ k\ dvd\ m*n\
1.256 -\isasymrbrakk\
1.257 +\ \ \ \ \ \ \ "\isasymlbrakk gcd(k,n){=}1;\ k\ dvd\ m*n\isasymrbrakk\
1.258 \isasymLongrightarrow\ k\ dvd\
1.259 m"\isanewline
1.260 \isacommand{apply}\ (insert\ gcd_mult_distrib2\ [of\ m\ k\