nipkow@9645 1 (*<*) nipkow@9645 2 theory AdvancedInd = Main:; nipkow@9645 3 (*>*) nipkow@9645 4 nipkow@9645 5 text{*\noindent nipkow@9645 6 Now that we have learned about rules and logic, we take another look at the nipkow@9645 7 finer points of induction. The two questions we answer are: what to do if the nipkow@9645 8 proposition to be proved is not directly amenable to induction, and how to nipkow@9645 9 utilize and even derive new induction schemas. nipkow@9689 10 *}; nipkow@9645 11 nipkow@10217 12 subsection{*Massaging the proposition*}; nipkow@9645 13 nipkow@10217 14 text{*\label{sec:ind-var-in-prems} nipkow@9645 15 So far we have assumed that the theorem we want to prove is already in a form nipkow@9645 16 that is amenable to induction, but this is not always the case: nipkow@9689 17 *}; nipkow@9645 18 nipkow@9933 19 lemma "xs \ [] \ hd(rev xs) = last xs"; nipkow@9645 20 apply(induct_tac xs); nipkow@9645 21 nipkow@9645 22 txt{*\noindent nipkow@9792 23 (where @{term"hd"} and @{term"last"} return the first and last element of a nipkow@9645 24 non-empty list) nipkow@9645 25 produces the warning nipkow@9645 26 \begin{quote}\tt nipkow@9645 27 Induction variable occurs also among premises! nipkow@9645 28 \end{quote} nipkow@9645 29 and leads to the base case nipkow@9723 30 \begin{isabelle} nipkow@9645 31 \ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ (rev\ [])\ =\ last\ [] nipkow@9723 32 \end{isabelle} nipkow@9645 33 which, after simplification, becomes nipkow@9723 34 \begin{isabelle} nipkow@9645 35 \ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ []\ =\ last\ [] nipkow@9723 36 \end{isabelle} nipkow@9792 37 We cannot prove this equality because we do not know what @{term"hd"} and nipkow@9792 38 @{term"last"} return when applied to @{term"[]"}. nipkow@9645 39 nipkow@9645 40 The point is that we have violated the above warning. Because the induction nipkow@9792 41 formula is only the conclusion, the occurrence of @{term"xs"} in the premises is nipkow@9645 42 not modified by induction. Thus the case that should have been trivial nipkow@9645 43 becomes unprovable. Fortunately, the solution is easy: nipkow@9645 44 \begin{quote} nipkow@9645 45 \emph{Pull all occurrences of the induction variable into the conclusion nipkow@9792 46 using @{text"\"}.} nipkow@9645 47 \end{quote} nipkow@9645 48 This means we should prove nipkow@9689 49 *}; nipkow@9689 50 (*<*)oops;(*>*) nipkow@9933 51 lemma hd_rev: "xs \ [] \ hd(rev xs) = last xs"; nipkow@9645 52 (*<*) nipkow@9689 53 by(induct_tac xs, auto); nipkow@9645 54 (*>*) nipkow@9645 55 nipkow@9645 56 text{*\noindent nipkow@9645 57 This time, induction leaves us with the following base case nipkow@9723 58 \begin{isabelle} nipkow@9645 59 \ 1.\ []\ {\isasymnoteq}\ []\ {\isasymlongrightarrow}\ hd\ (rev\ [])\ =\ last\ [] nipkow@9723 60 \end{isabelle} nipkow@9792 61 which is trivial, and @{text"auto"} finishes the whole proof. nipkow@9645 62 nipkow@9792 63 If @{thm[source]hd_rev} is meant to be a simplification rule, you are nipkow@9792 64 done. But if you really need the @{text"\"}-version of nipkow@9792 65 @{thm[source]hd_rev}, for example because you want to apply it as an nipkow@9792 66 introduction rule, you need to derive it separately, by combining it with nipkow@9792 67 modus ponens: nipkow@9689 68 *}; nipkow@9645 69 nipkow@9689 70 lemmas hd_revI = hd_rev[THEN mp]; nipkow@9645 71 nipkow@9645 72 text{*\noindent nipkow@9645 73 which yields the lemma we originally set out to prove. nipkow@9645 74 nipkow@9645 75 In case there are multiple premises $A@1$, \dots, $A@n$ containing the nipkow@9645 76 induction variable, you should turn the conclusion $C$ into nipkow@9645 77 $A@1 \longrightarrow \cdots A@n \longrightarrow C$ nipkow@9645 78 (see the remark?? in \S\ref{??}). nipkow@9645 79 Additionally, you may also have to universally quantify some other variables, nipkow@9645 80 which can yield a fairly complex conclusion. nipkow@9792 81 Here is a simple example (which is proved by @{text"blast"}): nipkow@9689 82 *}; nipkow@9645 83 nipkow@9933 84 lemma simple: "\y. A y \ B y \ B y & A y"; nipkow@9689 85 (*<*)by blast;(*>*) nipkow@9645 86 nipkow@9645 87 text{*\noindent nipkow@9645 88 You can get the desired lemma by explicit nipkow@9792 89 application of modus ponens and @{thm[source]spec}: nipkow@9689 90 *}; nipkow@9645 91 nipkow@9689 92 lemmas myrule = simple[THEN spec, THEN mp, THEN mp]; nipkow@9645 93 nipkow@9645 94 text{*\noindent nipkow@9792 95 or the wholesale stripping of @{text"\"} and wenzelm@9941 96 @{text"\"} in the conclusion via @{text"rule_format"} nipkow@9689 97 *}; nipkow@9645 98 wenzelm@9941 99 lemmas myrule = simple[rule_format]; nipkow@9645 100 nipkow@9645 101 text{*\noindent nipkow@9689 102 yielding @{thm"myrule"[no_vars]}. nipkow@9645 103 You can go one step further and include these derivations already in the nipkow@9645 104 statement of your original lemma, thus avoiding the intermediate step: nipkow@9689 105 *}; nipkow@9645 106 wenzelm@9941 107 lemma myrule[rule_format]: "\y. A y \ B y \ B y & A y"; nipkow@9645 108 (*<*) nipkow@9689 109 by blast; nipkow@9645 110 (*>*) nipkow@9645 111 nipkow@9645 112 text{* nipkow@9645 113 \bigskip nipkow@9645 114 nipkow@9645 115 A second reason why your proposition may not be amenable to induction is that nipkow@9645 116 you want to induct on a whole term, rather than an individual variable. In nipkow@10217 117 general, when inducting on some term $t$ you must rephrase the conclusion $C$ nipkow@10217 118 as nipkow@10217 119 $\forall y@1 \dots y@n.~ x = t \longrightarrow C$ nipkow@10217 120 where $y@1 \dots y@n$ are the free variables in $t$ and $x$ is new, and nipkow@10217 121 perform induction on $x$ afterwards. An example appears in nipkow@10217 122 \S\ref{sec:complete-ind} below. nipkow@10217 123 nipkow@10217 124 The very same problem may occur in connection with rule induction. Remember nipkow@10217 125 that it requires a premise of the form $(x@1,\dots,x@k) \in R$, where $R$ is nipkow@10217 126 some inductively defined set and the $x@i$ are variables. If instead we have nipkow@10217 127 a premise $t \in R$, where $t$ is not just an $n$-tuple of variables, we nipkow@10217 128 replace it with $(x@1,\dots,x@k) \in R$, and rephrase the conclusion $C$ as nipkow@10217 129 $\forall y@1 \dots y@n.~ (x@1,\dots,x@k) = t \longrightarrow C$ nipkow@10217 130 For an example see \S\ref{sec:CTL-revisited} below. nipkow@9689 131 *}; nipkow@9645 132 nipkow@9689 133 subsection{*Beyond structural and recursion induction*}; nipkow@9645 134 nipkow@10217 135 text{*\label{sec:complete-ind} nipkow@9645 136 So far, inductive proofs where by structural induction for nipkow@9645 137 primitive recursive functions and recursion induction for total recursive nipkow@9645 138 functions. But sometimes structural induction is awkward and there is no nipkow@9645 139 recursive function in sight either that could furnish a more appropriate nipkow@9645 140 induction schema. In such cases some existing standard induction schema can nipkow@9645 141 be helpful. We show how to apply such induction schemas by an example. nipkow@9645 142 nipkow@9792 143 Structural induction on @{typ"nat"} is nipkow@9645 144 usually known as mathematical induction''. There is also complete nipkow@9645 145 induction'', where you must prove $P(n)$ under the assumption that $P(m)$ nipkow@9933 146 holds for all $m nat"; nipkow@9689 152 axioms f_ax: "f(f(n)) < f(Suc(n))"; nipkow@9645 153 nipkow@9645 154 text{*\noindent nipkow@9645 155 From the above axiom\footnote{In general, the use of axioms is strongly nipkow@9645 156 discouraged, because of the danger of inconsistencies. The above axiom does nipkow@9645 157 not introduce an inconsistency because, for example, the identity function nipkow@9645 158 satisfies it.} nipkow@9792 159 for @{term"f"} it follows that @{prop"n <= f n"}, which can nipkow@9645 160 be proved by induction on @{term"f n"}. Following the recipy outlined nipkow@9645 161 above, we have to phrase the proposition as follows to allow induction: nipkow@9689 162 *}; nipkow@9645 163 nipkow@9933 164 lemma f_incr_lem: "\i. k = f i \ i \ f i"; nipkow@9645 165 nipkow@9645 166 txt{*\noindent nipkow@9933 167 To perform induction on @{term"k"} using @{thm[source]nat_less_induct}, we use the same nipkow@9645 168 general induction method as for recursion induction (see nipkow@9645 169 \S\ref{sec:recdef-induction}): nipkow@9689 170 *}; nipkow@9645 171 wenzelm@9923 172 apply(induct_tac k rule: nat_less_induct); nipkow@9645 173 (*<*) nipkow@9689 174 apply(rule allI); nipkow@9645 175 apply(case_tac i); nipkow@9645 176 apply(simp); nipkow@9645 177 (*>*) nipkow@9645 178 txt{*\noindent nipkow@9645 179 which leaves us with the following proof state: nipkow@9723 180 \begin{isabelle} nipkow@9645 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 nipkow@9645 182 \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymforall}\mbox{i}.\ \mbox{n}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i} nipkow@9723 183 \end{isabelle} nipkow@9792 184 After stripping the @{text"\i"}, the proof continues with a case nipkow@9792 185 distinction on @{term"i"}. The case @{prop"i = 0"} is trivial and we focus on nipkow@9792 186 the other case: nipkow@9723 187 \begin{isabelle} nipkow@9645 188 \ 1.\ {\isasymAnd}\mbox{n}\ \mbox{i}\ \mbox{nat}.\isanewline nipkow@9645 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 nipkow@9645 190 \ \ \ \ \ \ \ {\isasymLongrightarrow}\ \mbox{n}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i} nipkow@9723 191 \end{isabelle} nipkow@9689 192 *}; nipkow@9645 193 wenzelm@9923 194 by(blast intro!: f_ax Suc_leI intro: le_less_trans); nipkow@9645 195 nipkow@9645 196 text{*\noindent nipkow@9645 197 It is not surprising if you find the last step puzzling. nipkow@9792 198 The proof goes like this (writing @{term"j"} instead of @{typ"nat"}). nipkow@9792 199 Since @{prop"i = Suc j"} it suffices to show nipkow@9792 200 @{prop"j < f(Suc j)"} (by @{thm[source]Suc_leI}: @{thm"Suc_leI"[no_vars]}). This is nipkow@9792 201 proved as follows. From @{thm[source]f_ax} we have @{prop"f (f j) < f (Suc j)"} nipkow@9792 202 (1) which implies @{prop"f j <= f (f j)"} (by the induction hypothesis). nipkow@9792 203 Using (1) once more we obtain @{prop"f j < f(Suc j)"} (2) by transitivity nipkow@9792 204 (@{thm[source]le_less_trans}: @{thm"le_less_trans"[no_vars]}). nipkow@9792 205 Using the induction hypothesis once more we obtain @{prop"j <= f j"} nipkow@9792 206 which, together with (2) yields @{prop"j < f (Suc j)"} (again by nipkow@9792 207 @{thm[source]le_less_trans}). nipkow@9645 208 nipkow@9645 209 This last step shows both the power and the danger of automatic proofs: they nipkow@9645 210 will usually not tell you how the proof goes, because it can be very hard to nipkow@9645 211 translate the internal proof into a human-readable format. Therefore nipkow@9645 212 \S\ref{sec:part2?} introduces a language for writing readable yet concise nipkow@9645 213 proofs. nipkow@9645 214 nipkow@9792 215 We can now derive the desired @{prop"i <= f i"} from @{text"f_incr"}: nipkow@9689 216 *}; nipkow@9645 217 wenzelm@9941 218 lemmas f_incr = f_incr_lem[rule_format, OF refl]; nipkow@9645 219 nipkow@9689 220 text{*\noindent nipkow@9792 221 The final @{thm[source]refl} gets rid of the premise @{text"?k = f ?i"}. Again, nipkow@9792 222 we could have included this derivation in the original statement of the lemma: nipkow@9689 223 *}; nipkow@9645 224 wenzelm@9941 225 lemma f_incr[rule_format, OF refl]: "\i. k = f i \ i \ f i"; nipkow@9689 226 (*<*)oops;(*>*) nipkow@9645 227 nipkow@9645 228 text{* nipkow@9645 229 \begin{exercise} nipkow@9792 230 From the above axiom and lemma for @{term"f"} show that @{term"f"} is the nipkow@9792 231 identity. nipkow@9645 232 \end{exercise} nipkow@9645 233 nipkow@10236 234 In general, @{text induct_tac} can be applied with any rule$r$nipkow@9792 235 whose conclusion is of the form${?}P~?x@1 \dots ?x@n$, in which case the nipkow@9645 236 format is nipkow@9792 237 \begin{quote} nipkow@9792 238 \isacommand{apply}@{text"(induct_tac"}$y@1 \dots y@n$@{text"rule:"}$r$@{text")"} nipkow@9792 239 \end{quote}\index{*induct_tac}% nipkow@9792 240 where$y@1, \dots, y@n$are variables in the first subgoal. nipkow@10236 241 A further example of a useful induction rule is @{thm[source]length_induct}, nipkow@10236 242 induction on the length of a list:\indexbold{*length_induct} nipkow@10236 243 @{thm[display]length_induct[no_vars]} nipkow@10236 244 nipkow@9792 245 In fact, @{text"induct_tac"} even allows the conclusion of nipkow@9792 246$r$to be an (iterated) conjunction of formulae of the above form, in nipkow@9645 247 which case the application is nipkow@9792 248 \begin{quote} nipkow@9792 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")"} nipkow@9792 250 \end{quote} nipkow@9689 251 *}; nipkow@9645 252 nipkow@9689 253 subsection{*Derivation of new induction schemas*}; nipkow@9689 254 nipkow@9689 255 text{*\label{sec:derive-ind} nipkow@9689 256 Induction schemas are ordinary theorems and you can derive new ones nipkow@9689 257 whenever you wish. This section shows you how to, using the example nipkow@9933 258 of @{thm[source]nat_less_induct}. Assume we only have structural induction nipkow@9689 259 available for @{typ"nat"} and want to derive complete induction. This nipkow@9689 260 requires us to generalize the statement first: nipkow@9689 261 *}; nipkow@9689 262 nipkow@9933 263 lemma induct_lem: "(\n::nat. \m P n) \ \mn::nat. \m P n) \ P n"; nipkow@9689 288 by(insert induct_lem, blast); nipkow@9689 289 nipkow@9933 290 text{* nipkow@10186 291 nipkow@9645 292 Finally we should mention that HOL already provides the mother of all nipkow@10186 293 inductions, \textbf{wellfounded nipkow@10186 294 induction}\indexbold{induction!wellfounded}\index{wellfounded nipkow@10186 295 induction|see{induction, wellfounded}} (@{thm[source]wf_induct}): nipkow@10186 296 @{thm[display]wf_induct[no_vars]} nipkow@10186 297 where @{term"wf r"} means that the relation @{term r} is wellfounded nipkow@10186 298 (see \S\ref{sec:wellfounded}). nipkow@9933 299 For example, theorem @{thm[source]nat_less_induct} can be viewed (and nipkow@9933 300 derived) as a special case of @{thm[source]wf_induct} where nipkow@10186 301 @{term r} is @{text"<"} on @{typ nat}. The details can be found in the HOL library. nipkow@10186 302 For a mathematical account of wellfounded induction see, for example, \cite{Baader-Nipkow}. nipkow@9689 303 *}; nipkow@9645 304 nipkow@9645 305 (*<*) nipkow@9645 306 end nipkow@9645 307 (*>*)