2 theory AdvancedInd imports Main begin;
6 Now that we have learned about rules and logic, we take another look at the
7 finer points of induction. We consider two questions: what to do if the
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}).
14 subsection{*Massaging the Proposition*};
16 text{*\label{sec:ind-var-in-prems}
17 Often we have assumed that the theorem to be proved is already in a form
18 that is amenable to induction, but sometimes it isn't.
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:
24 lemma "xs \<noteq> [] \<Longrightarrow> hd(rev xs) = last xs"
28 But induction produces the warning
30 Induction variable occurs also among premises!
32 and leads to the base case
33 @{subgoals[display,indent=0,goals_limit=1]}
34 Simplification reduces the base case to this:
36 \ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ []\ =\ last\ []
38 We cannot prove this equality because we do not know what @{term hd} and
39 @{term last} return when applied to @{term"[]"}.
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
44 becomes unprovable. Fortunately, the solution is easy:\footnote{A similar
45 heuristic applies to rule inductions; see \S\ref{sec:rtc}.}
47 \emph{Pull all occurrences of the induction variable into the conclusion
48 using @{text"\<longrightarrow>"}.}
50 Thus we should state the lemma as an ordinary
51 implication~(@{text"\<longrightarrow>"}), letting
52 \attrdx{rule_format} (\S\ref{sec:forward}) convert the
53 result to the usual @{text"\<Longrightarrow>"} form:
56 lemma hd_rev [rule_format]: "xs \<noteq> [] \<longrightarrow> hd(rev xs) = last xs";
62 This time, induction leaves us with a trivial base case:
63 @{subgoals[display,indent=0,goals_limit=1]}
64 And @{text"auto"} completes the proof.
66 If there are multiple premises $A@1$, \dots, $A@n$ containing the
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,
70 which can yield a fairly complex conclusion. However, @{text rule_format}
71 can remove any number of occurrences of @{text"\<forall>"} and
72 @{text"\<longrightarrow>"}.
74 \index{induction!on a term}%
75 A second reason why your proposition may not be amenable to induction is that
76 you want to induct on a complex term, rather than a variable. In
77 general, induction on a term~$t$ requires rephrasing the conclusion~$C$
79 \begin{equation}\label{eqn:ind-over-term}
80 \forall y@1 \dots y@n.~ x = t \longrightarrow C.
82 where $y@1 \dots y@n$ are the free variables in $t$ and $x$ is a new variable.
83 Now you can perform induction on~$x$. An example appears in
84 \S\ref{sec:complete-ind} below.
86 The very same problem may occur in connection with rule induction. Remember
87 that it requires a premise of the form $(x@1,\dots,x@k) \in R$, where $R$ is
88 some inductively defined set and the $x@i$ are variables. If instead we have
89 a premise $t \in R$, where $t$ is not just an $n$-tuple of variables, we
90 replace it with $(x@1,\dots,x@k) \in R$, and rephrase the conclusion $C$ as
91 \[ \forall y@1 \dots y@n.~ (x@1,\dots,x@k) = t \longrightarrow C. \]
92 For an example see \S\ref{sec:CTL-revisited} below.
94 Of course, all premises that share free variables with $t$ need to be pulled into
95 the conclusion as well, under the @{text"\<forall>"}, again using @{text"\<longrightarrow>"} as shown above.
97 Readers who are puzzled by the form of statement
98 (\ref{eqn:ind-over-term}) above should remember that the
99 transformation is only performed to permit induction. Once induction
100 has been applied, the statement can be transformed back into something quite
101 intuitive. For example, applying wellfounded induction on $x$ (w.r.t.\
102 $\prec$) to (\ref{eqn:ind-over-term}) and transforming the result a
103 little leads to the goal
104 \[ \bigwedge\overline{y}.\
105 \forall \overline{z}.\ t\,\overline{z} \prec t\,\overline{y}\ \longrightarrow\ C\,\overline{z}
106 \ \Longrightarrow\ C\,\overline{y} \]
107 where $\overline{y}$ stands for $y@1 \dots y@n$ and the dependence of $t$ and
108 $C$ on the free variables of $t$ has been made explicit.
109 Unfortunately, this induction schema cannot be expressed as a
110 single theorem because it depends on the number of free variables in $t$ ---
111 the notation $\overline{y}$ is merely an informal device.
115 subsection{*Beyond Structural and Recursion Induction*};
117 text{*\label{sec:complete-ind}
118 So far, inductive proofs were by structural induction for
119 primitive recursive functions and recursion induction for total recursive
120 functions. But sometimes structural induction is awkward and there is no
121 recursive function that could furnish a more appropriate
122 induction schema. In such cases a general-purpose induction schema can
123 be helpful. We show how to apply such induction schemas by an example.
125 Structural induction on @{typ"nat"} is
126 usually known as mathematical induction. There is also \textbf{complete}
127 \index{induction!complete}%
128 induction, where you prove $P(n)$ under the assumption that $P(m)$
129 holds for all $m<n$. In Isabelle, this is the theorem \tdx{nat_less_induct}:
130 @{thm[display]"nat_less_induct"[no_vars]}
131 As an application, we prove a property of the following
135 consts f :: "nat \<Rightarrow> nat";
136 axioms f_ax: "f(f(n)) < f(Suc(n))";
140 We discourage the use of axioms because of the danger of
141 inconsistencies. Axiom @{text f_ax} does
142 not introduce an inconsistency because, for example, the identity function
143 satisfies it. Axioms can be useful in exploratory developments, say when
144 you assume some well-known theorems so that you can quickly demonstrate some
145 point about methodology. If your example turns into a substantial proof
146 development, you should replace axioms by theorems.
148 The axiom for @{term"f"} implies @{prop"n <= f n"}, which can
149 be proved by induction on \mbox{@{term"f n"}}. Following the recipe outlined
150 above, we have to phrase the proposition as follows to allow induction:
153 lemma f_incr_lem: "\<forall>i. k = f i \<longrightarrow> i \<le> f i";
156 To perform induction on @{term k} using @{thm[source]nat_less_induct}, we use
157 the same general induction method as for recursion induction (see
158 \S\ref{sec:fun-induction}):
161 apply(induct_tac k rule: nat_less_induct);
164 We get the following proof state:
165 @{subgoals[display,indent=0,margin=65]}
166 After stripping the @{text"\<forall>i"}, the proof continues with a case
167 distinction on @{term"i"}. The case @{prop"i = (0::nat)"} is trivial and we focus on
175 @{subgoals[display,indent=0]}
177 by(blast intro!: f_ax Suc_leI intro: le_less_trans)
180 If you find the last step puzzling, here are the two lemmas it employs:
182 @{thm Suc_leI[no_vars]}
183 \rulename{Suc_leI}\isanewline
184 @{thm le_less_trans[no_vars]}
185 \rulename{le_less_trans}
188 The proof goes like this (writing @{term"j"} instead of @{typ"nat"}).
189 Since @{prop"i = Suc j"} it suffices to show
190 \hbox{@{prop"j < f(Suc j)"}},
191 by @{thm[source]Suc_leI}\@. This is
192 proved as follows. From @{thm[source]f_ax} we have @{prop"f (f j) < f (Suc j)"}
193 (1) which implies @{prop"f j <= f (f j)"} by the induction hypothesis.
194 Using (1) once more we obtain @{prop"f j < f(Suc j)"} (2) by the transitivity
195 rule @{thm[source]le_less_trans}.
196 Using the induction hypothesis once more we obtain @{prop"j <= f j"}
197 which, together with (2) yields @{prop"j < f (Suc j)"} (again by
198 @{thm[source]le_less_trans}).
200 This last step shows both the power and the danger of automatic proofs. They
201 will usually not tell you how the proof goes, because it can be hard to
202 translate the internal proof into a human-readable format. Automatic
203 proofs are easy to write but hard to read and understand.
205 The desired result, @{prop"i <= f i"}, follows from @{thm[source]f_incr_lem}:
208 lemmas f_incr = f_incr_lem[rule_format, OF refl];
211 The final @{thm[source]refl} gets rid of the premise @{text"?k = f ?i"}.
212 We could have included this derivation in the original statement of the lemma:
215 lemma f_incr[rule_format, OF refl]: "\<forall>i. k = f i \<longrightarrow> i \<le> f i";
220 From the axiom and lemma for @{term"f"}, show that @{term"f"} is the
224 Method \methdx{induct_tac} can be applied with any rule $r$
225 whose conclusion is of the form ${?}P~?x@1 \dots ?x@n$, in which case the
228 \isacommand{apply}@{text"(induct_tac"} $y@1 \dots y@n$ @{text"rule:"} $r$@{text")"}
230 where $y@1, \dots, y@n$ are variables in the conclusion of the first subgoal.
232 A further useful induction rule is @{thm[source]length_induct},
233 induction on the length of a list\indexbold{*length_induct}
234 @{thm[display]length_induct[no_vars]}
235 which is a special case of @{thm[source]measure_induct}
236 @{thm[display]measure_induct[no_vars]}
237 where @{term f} may be any function into type @{typ nat}.
240 subsection{*Derivation of New Induction Schemas*};
242 text{*\label{sec:derive-ind}
243 \index{induction!deriving new schemas}%
244 Induction schemas are ordinary theorems and you can derive new ones
245 whenever you wish. This section shows you how, using the example
246 of @{thm[source]nat_less_induct}. Assume we only have structural induction
247 available for @{typ"nat"} and want to derive complete induction. We
248 must generalize the statement as shown:
251 lemma induct_lem: "(\<And>n::nat. \<forall>m<n. P m \<Longrightarrow> P n) \<Longrightarrow> \<forall>m<n. P m";
255 The base case is vacuously true. For the induction step (@{prop"m <
256 Suc n"}) we distinguish two cases: case @{prop"m < n"} is true by induction
257 hypothesis and case @{prop"m = n"} follows from the assumption, again using
258 the induction hypothesis:
261 by(blast elim: less_SucE)
264 The elimination rule @{thm[source]less_SucE} expresses the case distinction:
265 @{thm[display]"less_SucE"[no_vars]}
267 Now it is straightforward to derive the original version of
268 @{thm[source]nat_less_induct} by manipulating the conclusion of the above
269 lemma: instantiate @{term"n"} by @{term"Suc n"} and @{term"m"} by @{term"n"}
270 and remove the trivial condition @{prop"n < Suc n"}. Fortunately, this
271 happens automatically when we add the lemma as a new premise to the
275 theorem nat_less_induct: "(\<And>n::nat. \<forall>m<n. P m \<Longrightarrow> P n) \<Longrightarrow> P n";
276 by(insert induct_lem, blast);
279 HOL already provides the mother of
280 all inductions, well-founded induction (see \S\ref{sec:Well-founded}). For
281 example theorem @{thm[source]nat_less_induct} is
282 a special case of @{thm[source]wf_induct} where @{term r} is @{text"<"} on
283 @{typ nat}. The details can be found in theory \isa{Wellfounded_Recursion}.