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@9933  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@9933  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@9933  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  wenzelm@9923  97 @{text"\"} in the conclusion via @{text"rulified"}  nipkow@9689  98 *};  nipkow@9645  99 wenzelm@9923  100 lemmas myrule = simple[rulified];  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@9933  108 lemma myrule[rulified]: "\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@9933  137 holds for all $m nat";  nipkow@9689  143 axioms f_ax: "f(f(n)) < f(Suc(n))";  nipkow@9645  144 nipkow@9645  145 text{*\noindent  nipkow@9645  146 From the above axiom\footnote{In general, the use of axioms is strongly  nipkow@9645  147 discouraged, because of the danger of inconsistencies. The above axiom does  nipkow@9645  148 not introduce an inconsistency because, for example, the identity function  nipkow@9645  149 satisfies it.}  nipkow@9792  150 for @{term"f"} it follows that @{prop"n <= f n"}, which can  nipkow@9645  151 be proved by induction on @{term"f n"}. Following the recipy outlined  nipkow@9645  152 above, we have to phrase the proposition as follows to allow induction:  nipkow@9689  153 *};  nipkow@9645  154 nipkow@9933  155 lemma f_incr_lem: "\i. k = f i \ i \ f i";  nipkow@9645  156 nipkow@9645  157 txt{*\noindent  nipkow@9933  158 To perform induction on @{term"k"} using @{thm[source]nat_less_induct}, we use the same  nipkow@9645  159 general induction method as for recursion induction (see  nipkow@9645  160 \S\ref{sec:recdef-induction}):  nipkow@9689  161 *};  nipkow@9645  162 wenzelm@9923  163 apply(induct_tac k rule: nat_less_induct);  nipkow@9645  164 (*<*)  nipkow@9689  165 apply(rule allI);  nipkow@9645  166 apply(case_tac i);  nipkow@9645  167  apply(simp);  nipkow@9645  168 (*>*)  nipkow@9645  169 txt{*\noindent  nipkow@9645  170 which leaves us with the following proof state:  nipkow@9723  171 \begin{isabelle}  nipkow@9645  172 \ 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  173 \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymforall}\mbox{i}.\ \mbox{n}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i}  nipkow@9723  174 \end{isabelle}  nipkow@9792  175 After stripping the @{text"\i"}, the proof continues with a case  nipkow@9792  176 distinction on @{term"i"}. The case @{prop"i = 0"} is trivial and we focus on  nipkow@9792  177 the other case:  nipkow@9723  178 \begin{isabelle}  nipkow@9645  179 \ 1.\ {\isasymAnd}\mbox{n}\ \mbox{i}\ \mbox{nat}.\isanewline  nipkow@9645  180 \ \ \ \ \ \ \ {\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  181 \ \ \ \ \ \ \ {\isasymLongrightarrow}\ \mbox{n}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i}  nipkow@9723  182 \end{isabelle}  nipkow@9689  183 *};  nipkow@9645  184 wenzelm@9923  185 by(blast intro!: f_ax Suc_leI intro: le_less_trans);  nipkow@9645  186 nipkow@9645  187 text{*\noindent  nipkow@9645  188 It is not surprising if you find the last step puzzling.  nipkow@9792  189 The proof goes like this (writing @{term"j"} instead of @{typ"nat"}).  nipkow@9792  190 Since @{prop"i = Suc j"} it suffices to show  nipkow@9792  191 @{prop"j < f(Suc j)"} (by @{thm[source]Suc_leI}: @{thm"Suc_leI"[no_vars]}). This is  nipkow@9792  192 proved as follows. From @{thm[source]f_ax} we have @{prop"f (f j) < f (Suc j)"}  nipkow@9792  193 (1) which implies @{prop"f j <= f (f j)"} (by the induction hypothesis).  nipkow@9792  194 Using (1) once more we obtain @{prop"f j < f(Suc j)"} (2) by transitivity  nipkow@9792  195 (@{thm[source]le_less_trans}: @{thm"le_less_trans"[no_vars]}).  nipkow@9792  196 Using the induction hypothesis once more we obtain @{prop"j <= f j"}  nipkow@9792  197 which, together with (2) yields @{prop"j < f (Suc j)"} (again by  nipkow@9792  198 @{thm[source]le_less_trans}).  nipkow@9645  199 nipkow@9645  200 This last step shows both the power and the danger of automatic proofs: they  nipkow@9645  201 will usually not tell you how the proof goes, because it can be very hard to  nipkow@9645  202 translate the internal proof into a human-readable format. Therefore  nipkow@9645  203 \S\ref{sec:part2?} introduces a language for writing readable yet concise  nipkow@9645  204 proofs.  nipkow@9645  205 nipkow@9792  206 We can now derive the desired @{prop"i <= f i"} from @{text"f_incr"}:  nipkow@9689  207 *};  nipkow@9645  208 wenzelm@9923  209 lemmas f_incr = f_incr_lem[rulified, OF refl];  nipkow@9645  210 nipkow@9689  211 text{*\noindent  nipkow@9792  212 The final @{thm[source]refl} gets rid of the premise @{text"?k = f ?i"}. Again,  nipkow@9792  213 we could have included this derivation in the original statement of the lemma:  nipkow@9689  214 *};  nipkow@9645  215 nipkow@9933  216 lemma f_incr[rulified, OF refl]: "\i. k = f i \ i \ f i";  nipkow@9689  217 (*<*)oops;(*>*)  nipkow@9645  218 nipkow@9645  219 text{*  nipkow@9645  220 \begin{exercise}  nipkow@9792  221 From the above axiom and lemma for @{term"f"} show that @{term"f"} is the  nipkow@9792  222 identity.  nipkow@9645  223 \end{exercise}  nipkow@9645  224 nipkow@9792  225 In general, @{text"induct_tac"} can be applied with any rule$r$ nipkow@9792  226 whose conclusion is of the form${?}P~?x@1 \dots ?x@n$, in which case the  nipkow@9645  227 format is  nipkow@9792  228 \begin{quote}  nipkow@9792  229 \isacommand{apply}@{text"(induct_tac"}$y@1 \dots y@n$@{text"rule:"}$r$@{text")"}  nipkow@9792  230 \end{quote}\index{*induct_tac}%  nipkow@9792  231 where$y@1, \dots, y@n$are variables in the first subgoal.  nipkow@9792  232 In fact, @{text"induct_tac"} even allows the conclusion of  nipkow@9792  233 $r$to be an (iterated) conjunction of formulae of the above form, in  nipkow@9645  234 which case the application is  nipkow@9792  235 \begin{quote}  nipkow@9792  236 \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  237 \end{quote}  nipkow@9689  238 *};  nipkow@9645  239 nipkow@9689  240 subsection{*Derivation of new induction schemas*};  nipkow@9689  241 nipkow@9689  242 text{*\label{sec:derive-ind}  nipkow@9689  243 Induction schemas are ordinary theorems and you can derive new ones  nipkow@9689  244 whenever you wish. This section shows you how to, using the example  nipkow@9933  245 of @{thm[source]nat_less_induct}. Assume we only have structural induction  nipkow@9689  246 available for @{typ"nat"} and want to derive complete induction. This  nipkow@9689  247 requires us to generalize the statement first:  nipkow@9689  248 *};  nipkow@9689  249 nipkow@9933  250 lemma induct_lem: "(\n::nat. \m P n) \ \mn::nat. \m P n) \ P n";  nipkow@9689  275 by(insert induct_lem, blast);  nipkow@9689  276 nipkow@9933  277 text{*  nipkow@9645  278 Finally we should mention that HOL already provides the mother of all  nipkow@9792  279 inductions, \emph{wellfounded induction} (@{thm[source]wf_induct}):  nipkow@9689  280 @{thm[display]"wf_induct"[no_vars]}  nipkow@9792  281 where @{term"wf r"} means that the relation @{term"r"} is wellfounded.  nipkow@9933  282 For example, theorem @{thm[source]nat_less_induct} can be viewed (and  nipkow@9933  283 derived) as a special case of @{thm[source]wf_induct} where  nipkow@9933  284 @{term"r"} is @{text"<"} on @{typ"nat"}. For details see the library.  nipkow@9689  285 *};  nipkow@9645  286 nipkow@9645  287 (*<*)  nipkow@9645  288 end  nipkow@9645  289 (*>*)