3 \def\isabellecontext{AdvancedInd}%
8 Now that we have learned about rules and logic, we take another look at the
9 finer points of induction. We consider two questions: what to do if the
10 proposition to be proved is not directly amenable to induction
11 (\S\ref{sec:ind-var-in-prems}), and how to utilize (\S\ref{sec:complete-ind})
12 and even derive (\S\ref{sec:derive-ind}) new induction schemas. We conclude
13 with an extended example of induction (\S\ref{sec:CTL-revisited}).%
17 \isamarkupsubsection{Massaging the Proposition%
21 \begin{isamarkuptext}%
22 \label{sec:ind-var-in-prems}
23 Often we have assumed that the theorem to be proved is already in a form
24 that is amenable to induction, but sometimes it isn't.
26 Since \isa{hd} and \isa{last} return the first and last element of a
27 non-empty list, this lemma looks easy to prove:%
30 \isacommand{lemma}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ last\ xs{\isachardoublequote}\isanewline
32 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isamarkupfalse%
36 But induction produces the warning
38 Induction variable occurs also among premises!
40 and leads to the base case
42 \ {\isadigit{1}}{\isachardot}\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd\ {\isacharparenleft}rev\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ last\ {\isacharbrackleft}{\isacharbrackright}%
44 Simplification reduces the base case to this:
46 \ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ []\ =\ last\ []
48 We cannot prove this equality because we do not know what \isa{hd} and
49 \isa{last} return when applied to \isa{{\isacharbrackleft}{\isacharbrackright}}.
51 We should not have ignored the warning. Because the induction
52 formula is only the conclusion, induction does not affect the occurrence of \isa{xs} in the premises.
53 Thus the case that should have been trivial
54 becomes unprovable. Fortunately, the solution is easy:\footnote{A similar
55 heuristic applies to rule inductions; see \S\ref{sec:rtc}.}
57 \emph{Pull all occurrences of the induction variable into the conclusion
58 using \isa{{\isasymlongrightarrow}}.}
60 Thus we should state the lemma as an ordinary
61 implication~(\isa{{\isasymlongrightarrow}}), letting
62 \attrdx{rule_format} (\S\ref{sec:forward}) convert the
63 result to the usual \isa{{\isasymLongrightarrow}} form:%
67 \isacommand{lemma}\ hd{\isacharunderscore}rev\ {\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ last\ xs{\isachardoublequote}\isamarkupfalse%
72 This time, induction leaves us with a trivial base case:
74 \ {\isadigit{1}}{\isachardot}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ hd\ {\isacharparenleft}rev\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ last\ {\isacharbrackleft}{\isacharbrackright}%
76 And \isa{auto} completes the proof.
78 If there are multiple premises $A@1$, \dots, $A@n$ containing the
79 induction variable, you should turn the conclusion $C$ into
80 \[ A@1 \longrightarrow \cdots A@n \longrightarrow C. \]
81 Additionally, you may also have to universally quantify some other variables,
82 which can yield a fairly complex conclusion. However, \isa{rule{\isacharunderscore}format}
83 can remove any number of occurrences of \isa{{\isasymforall}} and
84 \isa{{\isasymlongrightarrow}}.
86 \index{induction!on a term}%
87 A second reason why your proposition may not be amenable to induction is that
88 you want to induct on a complex term, rather than a variable. In
89 general, induction on a term~$t$ requires rephrasing the conclusion~$C$
91 \begin{equation}\label{eqn:ind-over-term}
92 \forall y@1 \dots y@n.~ x = t \longrightarrow C.
94 where $y@1 \dots y@n$ are the free variables in $t$ and $x$ is a new variable.
95 Now you can perform induction on~$x$. An example appears in
96 \S\ref{sec:complete-ind} below.
98 The very same problem may occur in connection with rule induction. Remember
99 that it requires a premise of the form $(x@1,\dots,x@k) \in R$, where $R$ is
100 some inductively defined set and the $x@i$ are variables. If instead we have
101 a premise $t \in R$, where $t$ is not just an $n$-tuple of variables, we
102 replace it with $(x@1,\dots,x@k) \in R$, and rephrase the conclusion $C$ as
103 \[ \forall y@1 \dots y@n.~ (x@1,\dots,x@k) = t \longrightarrow C. \]
104 For an example see \S\ref{sec:CTL-revisited} below.
106 Of course, all premises that share free variables with $t$ need to be pulled into
107 the conclusion as well, under the \isa{{\isasymforall}}, again using \isa{{\isasymlongrightarrow}} as shown above.
109 Readers who are puzzled by the form of statement
110 (\ref{eqn:ind-over-term}) above should remember that the
111 transformation is only performed to permit induction. Once induction
112 has been applied, the statement can be transformed back into something quite
113 intuitive. For example, applying wellfounded induction on $x$ (w.r.t.\
114 $\prec$) to (\ref{eqn:ind-over-term}) and transforming the result a
115 little leads to the goal
116 \[ \bigwedge\overline{y}.\
117 \forall \overline{z}.\ t\,\overline{z} \prec t\,\overline{y}\ \longrightarrow\ C\,\overline{z}
118 \ \Longrightarrow\ C\,\overline{y} \]
119 where $\overline{y}$ stands for $y@1 \dots y@n$ and the dependence of $t$ and
120 $C$ on the free variables of $t$ has been made explicit.
121 Unfortunately, this induction schema cannot be expressed as a
122 single theorem because it depends on the number of free variables in $t$ ---
123 the notation $\overline{y}$ is merely an informal device.%
128 \isamarkupsubsection{Beyond Structural and Recursion Induction%
132 \begin{isamarkuptext}%
133 \label{sec:complete-ind}
134 So far, inductive proofs were by structural induction for
135 primitive recursive functions and recursion induction for total recursive
136 functions. But sometimes structural induction is awkward and there is no
137 recursive function that could furnish a more appropriate
138 induction schema. In such cases a general-purpose induction schema can
139 be helpful. We show how to apply such induction schemas by an example.
141 Structural induction on \isa{nat} is
142 usually known as mathematical induction. There is also \textbf{complete}
143 \index{induction!complete}%
144 induction, where you prove $P(n)$ under the assumption that $P(m)$
145 holds for all $m<n$. In Isabelle, this is the theorem \tdx{nat_less_induct}:
147 \ \ \ \ \ {\isacharparenleft}{\isasymAnd}n{\isachardot}\ {\isasymforall}m{\isacharless}n{\isachardot}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n%
149 As an application, we prove a property of the following
153 \isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
155 \isacommand{axioms}\ f{\isacharunderscore}ax{\isacharcolon}\ {\isachardoublequote}f{\isacharparenleft}f{\isacharparenleft}n{\isacharparenright}{\isacharparenright}\ {\isacharless}\ f{\isacharparenleft}Suc{\isacharparenleft}n{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
157 \begin{isamarkuptext}%
159 We discourage the use of axioms because of the danger of
160 inconsistencies. Axiom \isa{f{\isacharunderscore}ax} does
161 not introduce an inconsistency because, for example, the identity function
162 satisfies it. Axioms can be useful in exploratory developments, say when
163 you assume some well-known theorems so that you can quickly demonstrate some
164 point about methodology. If your example turns into a substantial proof
165 development, you should replace axioms by theorems.
167 The axiom for \isa{f} implies \isa{n\ {\isasymle}\ f\ n}, which can
168 be proved by induction on \mbox{\isa{f\ n}}. Following the recipe outlined
169 above, we have to phrase the proposition as follows to allow induction:%
172 \isacommand{lemma}\ f{\isacharunderscore}incr{\isacharunderscore}lem{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i{\isachardot}\ k\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isachardoublequote}\isamarkupfalse%
174 \begin{isamarkuptxt}%
176 To perform induction on \isa{k} using \isa{nat{\isacharunderscore}less{\isacharunderscore}induct}, we use
177 the same general induction method as for recursion induction (see
178 \S\ref{sec:recdef-induction}):%
181 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ k\ rule{\isacharcolon}\ nat{\isacharunderscore}less{\isacharunderscore}induct{\isacharparenright}\isamarkupfalse%
183 \begin{isamarkuptxt}%
185 We get the following proof state:
187 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymforall}m{\isacharless}n{\isachardot}\ {\isasymforall}i{\isachardot}\ m\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i\ {\isasymLongrightarrow}\ {\isasymforall}i{\isachardot}\ n\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i%
189 After stripping the \isa{{\isasymforall}i}, the proof continues with a case
190 distinction on \isa{i}. The case \isa{i\ {\isacharequal}\ {\isadigit{0}}} is trivial and we focus on
194 \isacommand{apply}{\isacharparenleft}rule\ allI{\isacharparenright}\isanewline
196 \isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ i{\isacharparenright}\isanewline
198 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isamarkupfalse%
200 \begin{isamarkuptxt}%
202 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n\ i\ nat{\isachardot}\isanewline
203 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}{\isasymforall}m{\isacharless}n{\isachardot}\ {\isasymforall}i{\isachardot}\ m\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isacharsemicolon}\ i\ {\isacharequal}\ Suc\ nat{\isasymrbrakk}\ {\isasymLongrightarrow}\ n\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i%
207 \isacommand{by}{\isacharparenleft}blast\ intro{\isacharbang}{\isacharcolon}\ f{\isacharunderscore}ax\ Suc{\isacharunderscore}leI\ intro{\isacharcolon}\ le{\isacharunderscore}less{\isacharunderscore}trans{\isacharparenright}\isamarkupfalse%
209 \begin{isamarkuptext}%
211 If you find the last step puzzling, here are the two lemmas it employs:
213 \isa{m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ Suc\ m\ {\isasymle}\ n}
214 \rulename{Suc_leI}\isanewline
215 \isa{{\isasymlbrakk}i\ {\isasymle}\ j{\isacharsemicolon}\ j\ {\isacharless}\ k{\isasymrbrakk}\ {\isasymLongrightarrow}\ i\ {\isacharless}\ k}
216 \rulename{le_less_trans}
219 The proof goes like this (writing \isa{j} instead of \isa{nat}).
220 Since \isa{i\ {\isacharequal}\ Suc\ j} it suffices to show
221 \hbox{\isa{j\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}}},
222 by \isa{Suc{\isacharunderscore}leI}\@. This is
223 proved as follows. From \isa{f{\isacharunderscore}ax} we have \isa{f\ {\isacharparenleft}f\ j{\isacharparenright}\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}}
224 (1) which implies \isa{f\ j\ {\isasymle}\ f\ {\isacharparenleft}f\ j{\isacharparenright}} by the induction hypothesis.
225 Using (1) once more we obtain \isa{f\ j\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}} (2) by the transitivity
226 rule \isa{le{\isacharunderscore}less{\isacharunderscore}trans}.
227 Using the induction hypothesis once more we obtain \isa{j\ {\isasymle}\ f\ j}
228 which, together with (2) yields \isa{j\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}} (again by
229 \isa{le{\isacharunderscore}less{\isacharunderscore}trans}).
231 This last step shows both the power and the danger of automatic proofs. They
232 will usually not tell you how the proof goes, because it can be hard to
233 translate the internal proof into a human-readable format. Automatic
234 proofs are easy to write but hard to read and understand.
236 The desired result, \isa{i\ {\isasymle}\ f\ i}, follows from \isa{f{\isacharunderscore}incr{\isacharunderscore}lem}:%
239 \isacommand{lemmas}\ f{\isacharunderscore}incr\ {\isacharequal}\ f{\isacharunderscore}incr{\isacharunderscore}lem{\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ OF\ refl{\isacharbrackright}\isamarkupfalse%
241 \begin{isamarkuptext}%
243 The final \isa{refl} gets rid of the premise \isa{{\isacharquery}k\ {\isacharequal}\ f\ {\isacharquery}i}.
244 We could have included this derivation in the original statement of the lemma:%
247 \isacommand{lemma}\ f{\isacharunderscore}incr{\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ OF\ refl{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i{\isachardot}\ k\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isachardoublequote}\isamarkupfalse%
250 \begin{isamarkuptext}%
252 From the axiom and lemma for \isa{f}, show that \isa{f} is the
256 Method \methdx{induct_tac} can be applied with any rule $r$
257 whose conclusion is of the form ${?}P~?x@1 \dots ?x@n$, in which case the
260 \isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $y@1 \dots y@n$ \isa{rule{\isacharcolon}} $r$\isa{{\isacharparenright}}
262 where $y@1, \dots, y@n$ are variables in the first subgoal.
263 The conclusion of $r$ can even be an (iterated) conjunction of formulae of
264 the above form in which case the application is
266 \isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $y@1 \dots y@n$ \isa{and} \dots\ \isa{and} $z@1 \dots z@m$ \isa{rule{\isacharcolon}} $r$\isa{{\isacharparenright}}
269 A further useful induction rule is \isa{length{\isacharunderscore}induct},
270 induction on the length of a list\indexbold{*length_induct}
272 \ \ \ \ \ {\isacharparenleft}{\isasymAnd}xs{\isachardot}\ {\isasymforall}ys{\isachardot}\ length\ ys\ {\isacharless}\ length\ xs\ {\isasymlongrightarrow}\ P\ ys\ {\isasymLongrightarrow}\ P\ xs{\isacharparenright}\ {\isasymLongrightarrow}\ P\ xs%
274 which is a special case of \isa{measure{\isacharunderscore}induct}
276 \ \ \ \ \ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ {\isasymforall}y{\isachardot}\ f\ y\ {\isacharless}\ f\ x\ {\isasymlongrightarrow}\ P\ y\ {\isasymLongrightarrow}\ P\ x{\isacharparenright}\ {\isasymLongrightarrow}\ P\ a%
278 where \isa{f} may be any function into type \isa{nat}.%
282 \isamarkupsubsection{Derivation of New Induction Schemas%
286 \begin{isamarkuptext}%
287 \label{sec:derive-ind}
288 \index{induction!deriving new schemas}%
289 Induction schemas are ordinary theorems and you can derive new ones
290 whenever you wish. This section shows you how, using the example
291 of \isa{nat{\isacharunderscore}less{\isacharunderscore}induct}. Assume we only have structural induction
292 available for \isa{nat} and want to derive complete induction. We
293 must generalize the statement as shown:%
296 \isacommand{lemma}\ induct{\isacharunderscore}lem{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isasymAnd}n{\isacharcolon}{\isacharcolon}nat{\isachardot}\ {\isasymforall}m{\isacharless}n{\isachardot}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymforall}m{\isacharless}n{\isachardot}\ P\ m{\isachardoublequote}\isanewline
298 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ n{\isacharparenright}\isamarkupfalse%
300 \begin{isamarkuptxt}%
302 The base case is vacuously true. For the induction step (\isa{m\ {\isacharless}\ Suc\ n}) we distinguish two cases: case \isa{m\ {\isacharless}\ n} is true by induction
303 hypothesis and case \isa{m\ {\isacharequal}\ n} follows from the assumption, again using
304 the induction hypothesis:%
307 \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
309 \isacommand{by}{\isacharparenleft}blast\ elim{\isacharcolon}\ less{\isacharunderscore}SucE{\isacharparenright}\isamarkupfalse%
311 \begin{isamarkuptext}%
313 The elimination rule \isa{less{\isacharunderscore}SucE} expresses the case distinction:
315 \ \ \ \ \ {\isasymlbrakk}m\ {\isacharless}\ Suc\ n{\isacharsemicolon}\ m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ m\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P%
318 Now it is straightforward to derive the original version of
319 \isa{nat{\isacharunderscore}less{\isacharunderscore}induct} by manipulating the conclusion of the above
320 lemma: instantiate \isa{n} by \isa{Suc\ n} and \isa{m} by \isa{n}
321 and remove the trivial condition \isa{n\ {\isacharless}\ Suc\ n}. Fortunately, this
322 happens automatically when we add the lemma as a new premise to the
326 \isacommand{theorem}\ nat{\isacharunderscore}less{\isacharunderscore}induct{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isasymAnd}n{\isacharcolon}{\isacharcolon}nat{\isachardot}\ {\isasymforall}m{\isacharless}n{\isachardot}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n{\isachardoublequote}\isanewline
328 \isacommand{by}{\isacharparenleft}insert\ induct{\isacharunderscore}lem{\isacharcomma}\ blast{\isacharparenright}\isamarkupfalse%
330 \begin{isamarkuptext}%
331 HOL already provides the mother of
332 all inductions, well-founded induction (see \S\ref{sec:Well-founded}). For
333 example theorem \isa{nat{\isacharunderscore}less{\isacharunderscore}induct} is
334 a special case of \isa{wf{\isacharunderscore}induct} where \isa{r} is \isa{{\isacharless}} on
335 \isa{nat}. The details can be found in theory \isa{Wellfounded_Recursion}.%
342 %%% TeX-master: "root"