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