summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

doc-src/TutorialI/Misc/AdvancedInd.thy

author | nipkow |

Tue Oct 17 13:28:57 2000 +0200 (2000-10-17) | |

changeset 10236 | 7626cb4e1407 |

parent 10217 | e61e7e1eacaf |

child 10241 | e0428c2778f1 |

permissions | -rw-r--r-- |

*** empty log message ***

1 (*<*)

2 theory AdvancedInd = Main:;

3 (*>*)

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

8 proposition to be proved is not directly amenable to induction, and how to

9 utilize and even derive new induction schemas.

10 *};

12 subsection{*Massaging the proposition*};

14 text{*\label{sec:ind-var-in-prems}

15 So far we have assumed that the theorem we want to prove is already in a form

16 that is amenable to induction, but this is not always the case:

17 *};

19 lemma "xs \<noteq> [] \<Longrightarrow> hd(rev xs) = last xs";

20 apply(induct_tac xs);

22 txt{*\noindent

23 (where @{term"hd"} and @{term"last"} return the first and last element of a

24 non-empty list)

25 produces the warning

26 \begin{quote}\tt

27 Induction variable occurs also among premises!

28 \end{quote}

29 and leads to the base case

30 \begin{isabelle}

31 \ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ (rev\ [])\ =\ last\ []

32 \end{isabelle}

33 which, after simplification, becomes

34 \begin{isabelle}

35 \ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ []\ =\ last\ []

36 \end{isabelle}

37 We cannot prove this equality because we do not know what @{term"hd"} and

38 @{term"last"} return when applied to @{term"[]"}.

40 The point is that we have violated the above warning. Because the induction

41 formula is only the conclusion, the occurrence of @{term"xs"} in the premises is

42 not modified by induction. Thus the case that should have been trivial

43 becomes unprovable. Fortunately, the solution is easy:

44 \begin{quote}

45 \emph{Pull all occurrences of the induction variable into the conclusion

46 using @{text"\<longrightarrow>"}.}

47 \end{quote}

48 This means we should prove

49 *};

50 (*<*)oops;(*>*)

51 lemma hd_rev: "xs \<noteq> [] \<longrightarrow> hd(rev xs) = last xs";

52 (*<*)

53 by(induct_tac xs, auto);

54 (*>*)

56 text{*\noindent

57 This time, induction leaves us with the following base case

58 \begin{isabelle}

59 \ 1.\ []\ {\isasymnoteq}\ []\ {\isasymlongrightarrow}\ hd\ (rev\ [])\ =\ last\ []

60 \end{isabelle}

61 which is trivial, and @{text"auto"} finishes the whole proof.

63 If @{thm[source]hd_rev} is meant to be a simplification rule, you are

64 done. But if you really need the @{text"\<Longrightarrow>"}-version of

65 @{thm[source]hd_rev}, for example because you want to apply it as an

66 introduction rule, you need to derive it separately, by combining it with

67 modus ponens:

68 *};

70 lemmas hd_revI = hd_rev[THEN mp];

72 text{*\noindent

73 which yields the lemma we originally set out to prove.

75 In case there are multiple premises $A@1$, \dots, $A@n$ containing the

76 induction variable, you should turn the conclusion $C$ into

77 \[ A@1 \longrightarrow \cdots A@n \longrightarrow C \]

78 (see the remark?? in \S\ref{??}).

79 Additionally, you may also have to universally quantify some other variables,

80 which can yield a fairly complex conclusion.

81 Here is a simple example (which is proved by @{text"blast"}):

82 *};

84 lemma simple: "\<forall>y. A y \<longrightarrow> B y \<longrightarrow> B y & A y";

85 (*<*)by blast;(*>*)

87 text{*\noindent

88 You can get the desired lemma by explicit

89 application of modus ponens and @{thm[source]spec}:

90 *};

92 lemmas myrule = simple[THEN spec, THEN mp, THEN mp];

94 text{*\noindent

95 or the wholesale stripping of @{text"\<forall>"} and

96 @{text"\<longrightarrow>"} in the conclusion via @{text"rule_format"}

97 *};

99 lemmas myrule = simple[rule_format];

101 text{*\noindent

102 yielding @{thm"myrule"[no_vars]}.

103 You can go one step further and include these derivations already in the

104 statement of your original lemma, thus avoiding the intermediate step:

105 *};

107 lemma myrule[rule_format]: "\<forall>y. A y \<longrightarrow> B y \<longrightarrow> B y & A y";

108 (*<*)

109 by blast;

110 (*>*)

112 text{*

113 \bigskip

115 A second reason why your proposition may not be amenable to induction is that

116 you want to induct on a whole term, rather than an individual variable. In

117 general, when inducting on some term $t$ you must rephrase the conclusion $C$

118 as

119 \[ \forall y@1 \dots y@n.~ x = t \longrightarrow C \]

120 where $y@1 \dots y@n$ are the free variables in $t$ and $x$ is new, and

121 perform induction on $x$ afterwards. An example appears in

122 \S\ref{sec:complete-ind} below.

124 The very same problem may occur in connection with rule induction. Remember

125 that it requires a premise of the form $(x@1,\dots,x@k) \in R$, where $R$ is

126 some inductively defined set and the $x@i$ are variables. If instead we have

127 a premise $t \in R$, where $t$ is not just an $n$-tuple of variables, we

128 replace it with $(x@1,\dots,x@k) \in R$, and rephrase the conclusion $C$ as

129 \[ \forall y@1 \dots y@n.~ (x@1,\dots,x@k) = t \longrightarrow C \]

130 For an example see \S\ref{sec:CTL-revisited} below.

131 *};

133 subsection{*Beyond structural and recursion induction*};

135 text{*\label{sec:complete-ind}

136 So far, inductive proofs where by structural induction for

137 primitive recursive functions and recursion induction for total recursive

138 functions. But sometimes structural induction is awkward and there is no

139 recursive function in sight either that could furnish a more appropriate

140 induction schema. In such cases some existing standard induction schema can

141 be helpful. We show how to apply such induction schemas by an example.

143 Structural induction on @{typ"nat"} is

144 usually known as ``mathematical induction''. There is also ``complete

145 induction'', where you must prove $P(n)$ under the assumption that $P(m)$

146 holds for all $m<n$. In Isabelle, this is the theorem @{thm[source]nat_less_induct}:

147 @{thm[display]"nat_less_induct"[no_vars]}

148 Here is an example of its application.

149 *};

151 consts f :: "nat => nat";

152 axioms f_ax: "f(f(n)) < f(Suc(n))";

154 text{*\noindent

155 From the above axiom\footnote{In general, the use of axioms is strongly

156 discouraged, because of the danger of inconsistencies. The above axiom does

157 not introduce an inconsistency because, for example, the identity function

158 satisfies it.}

159 for @{term"f"} it follows that @{prop"n <= f n"}, which can

160 be proved by induction on @{term"f n"}. Following the recipy outlined

161 above, we have to phrase the proposition as follows to allow induction:

162 *};

164 lemma f_incr_lem: "\<forall>i. k = f i \<longrightarrow> i \<le> f i";

166 txt{*\noindent

167 To perform induction on @{term"k"} using @{thm[source]nat_less_induct}, we use the same

168 general induction method as for recursion induction (see

169 \S\ref{sec:recdef-induction}):

170 *};

172 apply(induct_tac k rule: nat_less_induct);

173 (*<*)

174 apply(rule allI);

175 apply(case_tac i);

176 apply(simp);

177 (*>*)

178 txt{*\noindent

179 which leaves us with the following proof state:

180 \begin{isabelle}

181 \ 1.\ {\isasymAnd}\mbox{n}.\ {\isasymforall}\mbox{m}.\ \mbox{m}\ <\ \mbox{n}\ {\isasymlongrightarrow}\ ({\isasymforall}\mbox{i}.\ \mbox{m}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i})\isanewline

182 \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymforall}\mbox{i}.\ \mbox{n}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i}

183 \end{isabelle}

184 After stripping the @{text"\<forall>i"}, the proof continues with a case

185 distinction on @{term"i"}. The case @{prop"i = 0"} is trivial and we focus on

186 the other case:

187 \begin{isabelle}

188 \ 1.\ {\isasymAnd}\mbox{n}\ \mbox{i}\ \mbox{nat}.\isanewline

189 \ \ \ \ \ \ \ {\isasymlbrakk}{\isasymforall}\mbox{m}.\ \mbox{m}\ <\ \mbox{n}\ {\isasymlongrightarrow}\ ({\isasymforall}\mbox{i}.\ \mbox{m}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i});\ \mbox{i}\ =\ Suc\ \mbox{nat}{\isasymrbrakk}\isanewline

190 \ \ \ \ \ \ \ {\isasymLongrightarrow}\ \mbox{n}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i}

191 \end{isabelle}

192 *};

194 by(blast intro!: f_ax Suc_leI intro: le_less_trans);

196 text{*\noindent

197 It is not surprising if you find the last step puzzling.

198 The proof goes like this (writing @{term"j"} instead of @{typ"nat"}).

199 Since @{prop"i = Suc j"} it suffices to show

200 @{prop"j < f(Suc j)"} (by @{thm[source]Suc_leI}: @{thm"Suc_leI"[no_vars]}). This is

201 proved as follows. From @{thm[source]f_ax} we have @{prop"f (f j) < f (Suc j)"}

202 (1) which implies @{prop"f j <= f (f j)"} (by the induction hypothesis).

203 Using (1) once more we obtain @{prop"f j < f(Suc j)"} (2) by transitivity

204 (@{thm[source]le_less_trans}: @{thm"le_less_trans"[no_vars]}).

205 Using the induction hypothesis once more we obtain @{prop"j <= f j"}

206 which, together with (2) yields @{prop"j < f (Suc j)"} (again by

207 @{thm[source]le_less_trans}).

209 This last step shows both the power and the danger of automatic proofs: they

210 will usually not tell you how the proof goes, because it can be very hard to

211 translate the internal proof into a human-readable format. Therefore

212 \S\ref{sec:part2?} introduces a language for writing readable yet concise

213 proofs.

215 We can now derive the desired @{prop"i <= f i"} from @{text"f_incr"}:

216 *};

218 lemmas f_incr = f_incr_lem[rule_format, OF refl];

220 text{*\noindent

221 The final @{thm[source]refl} gets rid of the premise @{text"?k = f ?i"}. Again,

222 we could have included this derivation in the original statement of the lemma:

223 *};

225 lemma f_incr[rule_format, OF refl]: "\<forall>i. k = f i \<longrightarrow> i \<le> f i";

226 (*<*)oops;(*>*)

228 text{*

229 \begin{exercise}

230 From the above axiom and lemma for @{term"f"} show that @{term"f"} is the

231 identity.

232 \end{exercise}

234 In general, @{text induct_tac} can be applied with any rule $r$

235 whose conclusion is of the form ${?}P~?x@1 \dots ?x@n$, in which case the

236 format is

237 \begin{quote}

238 \isacommand{apply}@{text"(induct_tac"} $y@1 \dots y@n$ @{text"rule:"} $r$@{text")"}

239 \end{quote}\index{*induct_tac}%

240 where $y@1, \dots, y@n$ are variables in the first subgoal.

241 A further example of a useful induction rule is @{thm[source]length_induct},

242 induction on the length of a list:\indexbold{*length_induct}

243 @{thm[display]length_induct[no_vars]}

245 In fact, @{text"induct_tac"} even allows the conclusion of

246 $r$ to be an (iterated) conjunction of formulae of the above form, in

247 which case the application is

248 \begin{quote}

249 \isacommand{apply}@{text"(induct_tac"} $y@1 \dots y@n$ @{text"and"} \dots\ @{text"and"} $z@1 \dots z@m$ @{text"rule:"} $r$@{text")"}

250 \end{quote}

251 *};

253 subsection{*Derivation of new induction schemas*};

255 text{*\label{sec:derive-ind}

256 Induction schemas are ordinary theorems and you can derive new ones

257 whenever you wish. This section shows you how to, using the example

258 of @{thm[source]nat_less_induct}. Assume we only have structural induction

259 available for @{typ"nat"} and want to derive complete induction. This

260 requires us to generalize the statement first:

261 *};

263 lemma induct_lem: "(\<And>n::nat. \<forall>m<n. P m \<Longrightarrow> P n) \<Longrightarrow> \<forall>m<n. P m";

264 apply(induct_tac n);

266 txt{*\noindent

267 The base case is trivially true. For the induction step (@{prop"m <

268 Suc n"}) we distinguish two cases: case @{prop"m < n"} is true by induction

269 hypothesis and case @{prop"m = n"} follows from the assumption, again using

270 the induction hypothesis:

271 *};

272 apply(blast);

273 by(blast elim:less_SucE)

275 text{*\noindent

276 The elimination rule @{thm[source]less_SucE} expresses the case distinction:

277 @{thm[display]"less_SucE"[no_vars]}

279 Now it is straightforward to derive the original version of

280 @{thm[source]nat_less_induct} by manipulting the conclusion of the above lemma:

281 instantiate @{term"n"} by @{term"Suc n"} and @{term"m"} by @{term"n"} and

282 remove the trivial condition @{prop"n < Sc n"}. Fortunately, this

283 happens automatically when we add the lemma as a new premise to the

284 desired goal:

285 *};

287 theorem nat_less_induct: "(\<And>n::nat. \<forall>m<n. P m \<Longrightarrow> P n) \<Longrightarrow> P n";

288 by(insert induct_lem, blast);

290 text{*

292 Finally we should mention that HOL already provides the mother of all

293 inductions, \textbf{wellfounded

294 induction}\indexbold{induction!wellfounded}\index{wellfounded

295 induction|see{induction, wellfounded}} (@{thm[source]wf_induct}):

296 @{thm[display]wf_induct[no_vars]}

297 where @{term"wf r"} means that the relation @{term r} is wellfounded

298 (see \S\ref{sec:wellfounded}).

299 For example, theorem @{thm[source]nat_less_induct} can be viewed (and

300 derived) as a special case of @{thm[source]wf_induct} where

301 @{term r} is @{text"<"} on @{typ nat}. The details can be found in the HOL library.

302 For a mathematical account of wellfounded induction see, for example, \cite{Baader-Nipkow}.

303 *};

305 (*<*)

306 end

307 (*>*)