author | paulson |
Tue, 17 Jul 2001 13:46:21 +0200 | |
changeset 11428 | 332347b9b942 |
parent 11278 | 9710486b886b |
child 11494 | 23a118849801 |
permissions | -rw-r--r-- |
9645 | 1 |
(*<*) |
2 |
theory AdvancedInd = Main:; |
|
3 |
(*>*) |
|
4 |
||
5 |
text{*\noindent |
|
6 |
Now that we have learned about rules and logic, we take another look at the |
|
7 |
finer points of induction. The two questions we answer are: what to do if the |
|
10396 | 8 |
proposition to be proved is not directly amenable to induction |
9 |
(\S\ref{sec:ind-var-in-prems}), and how to utilize (\S\ref{sec:complete-ind}) |
|
10 |
and even derive (\S\ref{sec:derive-ind}) new induction schemas. We conclude |
|
11 |
with an extended example of induction (\S\ref{sec:CTL-revisited}). |
|
9689 | 12 |
*}; |
9645 | 13 |
|
10885 | 14 |
subsection{*Massaging the Proposition*}; |
9645 | 15 |
|
10217 | 16 |
text{*\label{sec:ind-var-in-prems} |
10885 | 17 |
Often we have assumed that the theorem we want to prove is already in a form |
18 |
that is amenable to induction, but sometimes it isn't. |
|
19 |
Here is an example. |
|
20 |
Since @{term"hd"} and @{term"last"} return the first and last element of a |
|
21 |
non-empty list, this lemma looks easy to prove: |
|
9689 | 22 |
*}; |
9645 | 23 |
|
10885 | 24 |
lemma "xs \<noteq> [] \<Longrightarrow> hd(rev xs) = last xs" |
25 |
apply(induct_tac xs) |
|
9645 | 26 |
|
27 |
txt{*\noindent |
|
10885 | 28 |
But induction produces the warning |
9645 | 29 |
\begin{quote}\tt |
30 |
Induction variable occurs also among premises! |
|
31 |
\end{quote} |
|
32 |
and leads to the base case |
|
10363 | 33 |
@{subgoals[display,indent=0,goals_limit=1]} |
10885 | 34 |
After simplification, it becomes |
9723 | 35 |
\begin{isabelle} |
9645 | 36 |
\ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ []\ =\ last\ [] |
9723 | 37 |
\end{isabelle} |
10242 | 38 |
We cannot prove this equality because we do not know what @{term hd} and |
39 |
@{term last} return when applied to @{term"[]"}. |
|
9645 | 40 |
|
10885 | 41 |
We should not have ignored the warning. Because the induction |
42 |
formula is only the conclusion, induction does not affect the occurrence of @{term xs} in the premises. |
|
43 |
Thus the case that should have been trivial |
|
10242 | 44 |
becomes unprovable. Fortunately, the solution is easy:\footnote{A very similar |
45 |
heuristic applies to rule inductions; see \S\ref{sec:rtc}.} |
|
9645 | 46 |
\begin{quote} |
47 |
\emph{Pull all occurrences of the induction variable into the conclusion |
|
9792 | 48 |
using @{text"\<longrightarrow>"}.} |
9645 | 49 |
\end{quote} |
10885 | 50 |
Thus we should state the lemma as an ordinary |
51 |
implication~(@{text"\<longrightarrow>"}), letting |
|
52 |
@{text rule_format} (\S\ref{sec:forward}) convert the |
|
53 |
result to the usual @{text"\<Longrightarrow>"} form: |
|
9689 | 54 |
*}; |
55 |
(*<*)oops;(*>*) |
|
10885 | 56 |
lemma hd_rev [rule_format]: "xs \<noteq> [] \<longrightarrow> hd(rev xs) = last xs"; |
9645 | 57 |
(*<*) |
10420 | 58 |
apply(induct_tac xs); |
9645 | 59 |
(*>*) |
60 |
||
10420 | 61 |
txt{*\noindent |
10885 | 62 |
This time, induction leaves us with a trivial base case: |
10420 | 63 |
@{subgoals[display,indent=0,goals_limit=1]} |
10885 | 64 |
And @{text"auto"} completes the proof. |
9645 | 65 |
|
10885 | 66 |
If there are multiple premises $A@1$, \dots, $A@n$ containing the |
9645 | 67 |
induction variable, you should turn the conclusion $C$ into |
68 |
\[ A@1 \longrightarrow \cdots A@n \longrightarrow C \] |
|
69 |
Additionally, you may also have to universally quantify some other variables, |
|
11196 | 70 |
which can yield a fairly complex conclusion. However, @{text rule_format} |
10885 | 71 |
can remove any number of occurrences of @{text"\<forall>"} and |
72 |
@{text"\<longrightarrow>"}. |
|
11196 | 73 |
*} |
9645 | 74 |
|
11196 | 75 |
(*<*) |
76 |
by auto; |
|
77 |
(*>*) |
|
78 |
(* |
|
79 |
Here is a simple example (which is proved by @{text"blast"}): |
|
10885 | 80 |
lemma simple[rule_format]: "\<forall>y. A y \<longrightarrow> B y \<longrightarrow> B y \<and> A y"; |
9689 | 81 |
by blast; |
11196 | 82 |
*) |
9645 | 83 |
|
84 |
text{* |
|
85 |
A second reason why your proposition may not be amenable to induction is that |
|
86 |
you want to induct on a whole term, rather than an individual variable. In |
|
10217 | 87 |
general, when inducting on some term $t$ you must rephrase the conclusion $C$ |
88 |
as |
|
11277 | 89 |
\begin{equation}\label{eqn:ind-over-term} |
90 |
\forall y@1 \dots y@n.~ x = t \longrightarrow C |
|
91 |
\end{equation} |
|
10217 | 92 |
where $y@1 \dots y@n$ are the free variables in $t$ and $x$ is new, and |
93 |
perform induction on $x$ afterwards. An example appears in |
|
94 |
\S\ref{sec:complete-ind} below. |
|
95 |
||
96 |
The very same problem may occur in connection with rule induction. Remember |
|
97 |
that it requires a premise of the form $(x@1,\dots,x@k) \in R$, where $R$ is |
|
98 |
some inductively defined set and the $x@i$ are variables. If instead we have |
|
99 |
a premise $t \in R$, where $t$ is not just an $n$-tuple of variables, we |
|
100 |
replace it with $(x@1,\dots,x@k) \in R$, and rephrase the conclusion $C$ as |
|
101 |
\[ \forall y@1 \dots y@n.~ (x@1,\dots,x@k) = t \longrightarrow C \] |
|
102 |
For an example see \S\ref{sec:CTL-revisited} below. |
|
10281 | 103 |
|
104 |
Of course, all premises that share free variables with $t$ need to be pulled into |
|
105 |
the conclusion as well, under the @{text"\<forall>"}, again using @{text"\<longrightarrow>"} as shown above. |
|
11277 | 106 |
|
107 |
Readers who are puzzled by the form of statement |
|
108 |
(\ref{eqn:ind-over-term}) above should remember that the |
|
109 |
transformation is only performed to permit induction. Once induction |
|
110 |
has been applied, the statement can be transformed back into something quite |
|
111 |
intuitive. For example, applying wellfounded induction on $x$ (w.r.t.\ |
|
112 |
$\prec$) to (\ref{eqn:ind-over-term}) and transforming the result a |
|
113 |
little leads to the goal |
|
11278 | 114 |
\[ \bigwedge\overline{y}.\ |
115 |
\forall \overline{z}.\ t\,\overline{z} \prec t\,\overline{y}\ \longrightarrow\ C\,\overline{z} |
|
116 |
\ \Longrightarrow\ C\,\overline{y} \] |
|
117 |
where $\overline{y}$ stands for $y@1 \dots y@n$ and the dependence of $t$ and |
|
118 |
$C$ on the free variables of $t$ has been made explicit. |
|
119 |
Unfortunately, this induction schema cannot be expressed as a |
|
120 |
single theorem because it depends on the number of free variables in $t$ --- |
|
121 |
the notation $\overline{y}$ is merely an informal device. |
|
11277 | 122 |
*} |
9645 | 123 |
|
10885 | 124 |
subsection{*Beyond Structural and Recursion Induction*}; |
9645 | 125 |
|
10217 | 126 |
text{*\label{sec:complete-ind} |
10885 | 127 |
So far, inductive proofs were by structural induction for |
9645 | 128 |
primitive recursive functions and recursion induction for total recursive |
129 |
functions. But sometimes structural induction is awkward and there is no |
|
10885 | 130 |
recursive function that could furnish a more appropriate |
131 |
induction schema. In such cases a general-purpose induction schema can |
|
9645 | 132 |
be helpful. We show how to apply such induction schemas by an example. |
133 |
||
9792 | 134 |
Structural induction on @{typ"nat"} is |
10885 | 135 |
usually known as mathematical induction. There is also \emph{complete} |
136 |
induction, where you must prove $P(n)$ under the assumption that $P(m)$ |
|
9933 | 137 |
holds for all $m<n$. In Isabelle, this is the theorem @{thm[source]nat_less_induct}: |
138 |
@{thm[display]"nat_less_induct"[no_vars]} |
|
11278 | 139 |
As an example of its application we prove a property of the following |
140 |
function: |
|
9689 | 141 |
*}; |
9645 | 142 |
|
10281 | 143 |
consts f :: "nat \<Rightarrow> nat"; |
9689 | 144 |
axioms f_ax: "f(f(n)) < f(Suc(n))"; |
9645 | 145 |
|
11256 | 146 |
text{* |
147 |
\begin{warn} |
|
148 |
We discourage the use of axioms because of the danger of |
|
149 |
inconsistencies. Axiom @{text f_ax} does |
|
150 |
not introduce an inconsistency because, for example, the identity function |
|
151 |
satisfies it. Axioms can be useful in exploratory developments, say when |
|
152 |
you assume some well-known theorems so that you can quickly demonstrate some |
|
153 |
point about methodology. If your example turns into a substantial proof |
|
154 |
development, you should replace axioms by theorems. |
|
155 |
\end{warn}\noindent |
|
10885 | 156 |
The axiom for @{term"f"} implies @{prop"n <= f n"}, which can |
11196 | 157 |
be proved by induction on \mbox{@{term"f n"}}. Following the recipe outlined |
9645 | 158 |
above, we have to phrase the proposition as follows to allow induction: |
9689 | 159 |
*}; |
9645 | 160 |
|
9933 | 161 |
lemma f_incr_lem: "\<forall>i. k = f i \<longrightarrow> i \<le> f i"; |
9645 | 162 |
|
163 |
txt{*\noindent |
|
10363 | 164 |
To perform induction on @{term k} using @{thm[source]nat_less_induct}, we use |
165 |
the same general induction method as for recursion induction (see |
|
9645 | 166 |
\S\ref{sec:recdef-induction}): |
9689 | 167 |
*}; |
9645 | 168 |
|
9923 | 169 |
apply(induct_tac k rule: nat_less_induct); |
10363 | 170 |
|
171 |
txt{*\noindent |
|
172 |
which leaves us with the following proof state: |
|
173 |
@{subgoals[display,indent=0,margin=65]} |
|
174 |
After stripping the @{text"\<forall>i"}, the proof continues with a case |
|
175 |
distinction on @{term"i"}. The case @{prop"i = 0"} is trivial and we focus on |
|
176 |
the other case: |
|
177 |
*} |
|
178 |
||
11196 | 179 |
apply(rule allI) |
180 |
apply(case_tac i) |
|
181 |
apply(simp) |
|
10363 | 182 |
txt{* |
183 |
@{subgoals[display,indent=0]} |
|
11196 | 184 |
*} |
185 |
by(blast intro!: f_ax Suc_leI intro: le_less_trans) |
|
9645 | 186 |
|
187 |
text{*\noindent |
|
11196 | 188 |
If you find the last step puzzling, here are the two lemmas it employs: |
10885 | 189 |
\begin{isabelle} |
190 |
@{thm Suc_leI[no_vars]} |
|
191 |
\rulename{Suc_leI}\isanewline |
|
192 |
@{thm le_less_trans[no_vars]} |
|
193 |
\rulename{le_less_trans} |
|
194 |
\end{isabelle} |
|
195 |
% |
|
9792 | 196 |
The proof goes like this (writing @{term"j"} instead of @{typ"nat"}). |
197 |
Since @{prop"i = Suc j"} it suffices to show |
|
10885 | 198 |
\hbox{@{prop"j < f(Suc j)"}}, |
199 |
by @{thm[source]Suc_leI}\@. This is |
|
9792 | 200 |
proved as follows. From @{thm[source]f_ax} we have @{prop"f (f j) < f (Suc j)"} |
10885 | 201 |
(1) which implies @{prop"f j <= f (f j)"} by the induction hypothesis. |
202 |
Using (1) once more we obtain @{prop"f j < f(Suc j)"} (2) by the transitivity |
|
203 |
rule @{thm[source]le_less_trans}. |
|
9792 | 204 |
Using the induction hypothesis once more we obtain @{prop"j <= f j"} |
205 |
which, together with (2) yields @{prop"j < f (Suc j)"} (again by |
|
206 |
@{thm[source]le_less_trans}). |
|
9645 | 207 |
|
208 |
This last step shows both the power and the danger of automatic proofs: they |
|
209 |
will usually not tell you how the proof goes, because it can be very hard to |
|
210 |
translate the internal proof into a human-readable format. Therefore |
|
10885 | 211 |
Chapter~\ref{sec:part2?} introduces a language for writing readable |
9645 | 212 |
proofs. |
213 |
||
11196 | 214 |
We can now derive the desired @{prop"i <= f i"} from @{thm[source]f_incr_lem}: |
9689 | 215 |
*}; |
9645 | 216 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9933
diff
changeset
|
217 |
lemmas f_incr = f_incr_lem[rule_format, OF refl]; |
9645 | 218 |
|
9689 | 219 |
text{*\noindent |
10885 | 220 |
The final @{thm[source]refl} gets rid of the premise @{text"?k = f ?i"}. |
221 |
We could have included this derivation in the original statement of the lemma: |
|
9689 | 222 |
*}; |
9645 | 223 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9933
diff
changeset
|
224 |
lemma f_incr[rule_format, OF refl]: "\<forall>i. k = f i \<longrightarrow> i \<le> f i"; |
9689 | 225 |
(*<*)oops;(*>*) |
9645 | 226 |
|
227 |
text{* |
|
11256 | 228 |
\begin{exercise} |
229 |
From the axiom and lemma for @{term"f"}, show that @{term"f"} is the |
|
230 |
identity function. |
|
231 |
\end{exercise} |
|
9645 | 232 |
|
11428 | 233 |
Method \methdx{induct_tac} can be applied with any rule $r$ |
9792 | 234 |
whose conclusion is of the form ${?}P~?x@1 \dots ?x@n$, in which case the |
9645 | 235 |
format is |
9792 | 236 |
\begin{quote} |
237 |
\isacommand{apply}@{text"(induct_tac"} $y@1 \dots y@n$ @{text"rule:"} $r$@{text")"} |
|
11428 | 238 |
\end{quote} |
9792 | 239 |
where $y@1, \dots, y@n$ are variables in the first subgoal. |
11256 | 240 |
The conclusion of $r$ can even be an (iterated) conjunction of formulae of |
241 |
the above form in which case the application is |
|
9792 | 242 |
\begin{quote} |
243 |
\isacommand{apply}@{text"(induct_tac"} $y@1 \dots y@n$ @{text"and"} \dots\ @{text"and"} $z@1 \dots z@m$ @{text"rule:"} $r$@{text")"} |
|
244 |
\end{quote} |
|
10885 | 245 |
|
11256 | 246 |
A further useful induction rule is @{thm[source]length_induct}, |
247 |
induction on the length of a list\indexbold{*length_induct} |
|
248 |
@{thm[display]length_induct[no_vars]} |
|
249 |
which is a special case of @{thm[source]measure_induct} |
|
250 |
@{thm[display]measure_induct[no_vars]} |
|
251 |
where @{term f} may be any function into type @{typ nat}. |
|
252 |
*} |
|
9645 | 253 |
|
10885 | 254 |
subsection{*Derivation of New Induction Schemas*}; |
9689 | 255 |
|
256 |
text{*\label{sec:derive-ind} |
|
257 |
Induction schemas are ordinary theorems and you can derive new ones |
|
258 |
whenever you wish. This section shows you how to, using the example |
|
9933 | 259 |
of @{thm[source]nat_less_induct}. Assume we only have structural induction |
9689 | 260 |
available for @{typ"nat"} and want to derive complete induction. This |
261 |
requires us to generalize the statement first: |
|
262 |
*}; |
|
263 |
||
9933 | 264 |
lemma induct_lem: "(\<And>n::nat. \<forall>m<n. P m \<Longrightarrow> P n) \<Longrightarrow> \<forall>m<n. P m"; |
9689 | 265 |
apply(induct_tac n); |
266 |
||
267 |
txt{*\noindent |
|
11196 | 268 |
The base case is vacuously true. For the induction step (@{prop"m < |
9933 | 269 |
Suc n"}) we distinguish two cases: case @{prop"m < n"} is true by induction |
270 |
hypothesis and case @{prop"m = n"} follows from the assumption, again using |
|
9689 | 271 |
the induction hypothesis: |
272 |
*}; |
|
11196 | 273 |
apply(blast); |
9933 | 274 |
by(blast elim:less_SucE) |
9689 | 275 |
|
276 |
text{*\noindent |
|
11196 | 277 |
The elimination rule @{thm[source]less_SucE} expresses the case distinction: |
9689 | 278 |
@{thm[display]"less_SucE"[no_vars]} |
279 |
||
280 |
Now it is straightforward to derive the original version of |
|
11256 | 281 |
@{thm[source]nat_less_induct} by manipulating the conclusion of the above |
282 |
lemma: instantiate @{term"n"} by @{term"Suc n"} and @{term"m"} by @{term"n"} |
|
283 |
and remove the trivial condition @{prop"n < Suc n"}. Fortunately, this |
|
9689 | 284 |
happens automatically when we add the lemma as a new premise to the |
285 |
desired goal: |
|
286 |
*}; |
|
287 |
||
9933 | 288 |
theorem nat_less_induct: "(\<And>n::nat. \<forall>m<n. P m \<Longrightarrow> P n) \<Longrightarrow> P n"; |
9689 | 289 |
by(insert induct_lem, blast); |
290 |
||
9933 | 291 |
text{* |
10396 | 292 |
Finally we should remind the reader that HOL already provides the mother of |
293 |
all inductions, well-founded induction (see \S\ref{sec:Well-founded}). For |
|
10885 | 294 |
example theorem @{thm[source]nat_less_induct} is |
10396 | 295 |
a special case of @{thm[source]wf_induct} where @{term r} is @{text"<"} on |
10885 | 296 |
@{typ nat}. The details can be found in theory \isa{Wellfounded_Recursion}. |
10654 | 297 |
*} |
298 |
(*<*)end(*>*) |