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