doc-src/TutorialI/Misc/AdvancedInd.thy
 author nipkow Mon Aug 28 09:32:51 2000 +0200 (2000-08-28) changeset 9689 751fde5307e4 parent 9645 20ae97cd2a16 child 9723 a977245dfc8a permissions -rw-r--r--
*** empty log message ***
 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@9645  24 (where \isa{hd} and \isa{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@9645  31 \begin{isabellepar}%  nipkow@9645  32 \ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ (rev\ [])\ =\ last\ []  nipkow@9645  33 \end{isabellepar}%  nipkow@9645  34 which, after simplification, becomes  nipkow@9645  35 \begin{isabellepar}%  nipkow@9645  36 \ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ []\ =\ last\ []  nipkow@9645  37 \end{isabellepar}%  nipkow@9645  38 We cannot prove this equality because we do not know what \isa{hd} and  nipkow@9645  39 \isa{last} return when applied to \isa{[]}.  nipkow@9645  40 nipkow@9645  41 The point is that we have violated the above warning. Because the induction  nipkow@9645  42 formula is only the conclusion, the occurrence of \isa{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@9645  47 using \isa{\isasymlongrightarrow}.}  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@9645  59 \begin{isabellepar}%  nipkow@9645  60 \ 1.\ []\ {\isasymnoteq}\ []\ {\isasymlongrightarrow}\ hd\ (rev\ [])\ =\ last\ []  nipkow@9645  61 \end{isabellepar}%  nipkow@9645  62 which is trivial, and \isa{auto} finishes the whole proof.  nipkow@9645  63 nipkow@9689  64 If \isa{hd\_rev} is meant to be a simplification rule, you are done. But if you  nipkow@9645  65 really need the \isa{\isasymLongrightarrow}-version of \isa{hd\_rev}, for  nipkow@9645  66 example because you want to apply it as an introduction rule, you need to  nipkow@9645  67 derive it separately, by combining it with 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@9645  81 Here is a simple example (which is proved by \isa{blast}):  nipkow@9689  82 *};  nipkow@9645  83 nipkow@9689  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@9645  89 application of modus ponens and \isa{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@9645  95 or the wholesale stripping of \isa{\isasymforall} and  nipkow@9645  96 \isa{\isasymlongrightarrow} in the conclusion via \isa{rulify}  nipkow@9689  97 *};  nipkow@9645  98 nipkow@9689  99 lemmas myrule = simple[rulify];  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 nipkow@9689  107 lemma myrule[rulify]: "\\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@9645  117 general, when inducting on some term $t$ you must rephrase the conclusion as  nipkow@9645  118 $\forall y@1 \dots y@n.~ x = t \longrightarrow C$ where $y@1 \dots y@n$  nipkow@9645  119 are the free variables in $t$ and $x$ is new, and perform induction on $x$  nipkow@9645  120 afterwards. An example appears below.  nipkow@9689  121 *};  nipkow@9645  122 nipkow@9689  123 subsection{*Beyond structural and recursion induction*};  nipkow@9645  124 nipkow@9645  125 text{*  nipkow@9645  126 So far, inductive proofs where by structural induction for  nipkow@9645  127 primitive recursive functions and recursion induction for total recursive  nipkow@9645  128 functions. But sometimes structural induction is awkward and there is no  nipkow@9645  129 recursive function in sight either that could furnish a more appropriate  nipkow@9645  130 induction schema. In such cases some existing standard induction schema can  nipkow@9645  131 be helpful. We show how to apply such induction schemas by an example.  nipkow@9645  132 nipkow@9645  133 Structural induction on \isa{nat} is  nipkow@9645  134 usually known as mathematical induction''. There is also complete  nipkow@9645  135 induction'', where you must prove $P(n)$ under the assumption that $P(m)$  nipkow@9645  136 holds for all \$m nat";  nipkow@9689  144 axioms f_ax: "f(f(n)) < f(Suc(n))";  nipkow@9645  145 nipkow@9645  146 text{*\noindent  nipkow@9645  147 From the above axiom\footnote{In general, the use of axioms is strongly  nipkow@9645  148 discouraged, because of the danger of inconsistencies. The above axiom does  nipkow@9645  149 not introduce an inconsistency because, for example, the identity function  nipkow@9645  150 satisfies it.}  nipkow@9645  151 for \isa{f} it follows that @{term"n <= f n"}, which can  nipkow@9645  152 be proved by induction on @{term"f n"}. Following the recipy outlined  nipkow@9645  153 above, we have to phrase the proposition as follows to allow induction:  nipkow@9689  154 *};  nipkow@9645  155 nipkow@9689  156 lemma f_incr_lem: "\\i. k = f i \\ i \\ f i";  nipkow@9645  157 nipkow@9645  158 txt{*\noindent  nipkow@9645  159 To perform induction on \isa{k} using \isa{less\_induct}, we use the same  nipkow@9645  160 general induction method as for recursion induction (see  nipkow@9645  161 \S\ref{sec:recdef-induction}):  nipkow@9689  162 *};  nipkow@9645  163 nipkow@9689  164 apply(induct_tac k rule:less_induct);  nipkow@9645  165 (*<*)  nipkow@9689  166 apply(rule allI);  nipkow@9645  167 apply(case_tac i);  nipkow@9645  168  apply(simp);  nipkow@9645  169 (*>*)  nipkow@9645  170 txt{*\noindent  nipkow@9645  171 which leaves us with the following proof state:  nipkow@9645  172 \begin{isabellepar}%  nipkow@9645  173 \ 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  174 \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymforall}\mbox{i}.\ \mbox{n}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i}  nipkow@9645  175 \end{isabellepar}%  nipkow@9645  176 After stripping the \isa{\isasymforall i}, the proof continues with a case  nipkow@9645  177 distinction on \isa{i}. The case \isa{i = 0} is trivial and we focus on the  nipkow@9645  178 other case:  nipkow@9645  179 \begin{isabellepar}%  nipkow@9645  180 \ 1.\ {\isasymAnd}\mbox{n}\ \mbox{i}\ \mbox{nat}.\isanewline  nipkow@9645  181 \ \ \ \ \ \ \ {\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  182 \ \ \ \ \ \ \ {\isasymLongrightarrow}\ \mbox{n}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i}  nipkow@9645  183 \end{isabellepar}%  nipkow@9689  184 *};  nipkow@9645  185 nipkow@9645  186 by(blast intro!: f_ax Suc_leI intro:le_less_trans);  nipkow@9645  187 nipkow@9645  188 text{*\noindent  nipkow@9645  189 It is not surprising if you find the last step puzzling.  nipkow@9645  190 The proof goes like this (writing \isa{j} instead of \isa{nat}).  nipkow@9645  191 Since @{term"i = Suc j"} it suffices to show  nipkow@9689  192 @{term"j < f(Suc j)"} (by \isa{Suc\_leI}: @{thm"Suc_leI"[no_vars]}). This is  nipkow@9645  193 proved as follows. From \isa{f\_ax} we have @{term"f (f j) < f (Suc j)"}  nipkow@9645  194 (1) which implies @{term"f j <= f (f j)"} (by the induction hypothesis).  nipkow@9645  195 Using (1) once more we obtain @{term"f j < f(Suc j)"} (2) by transitivity  nipkow@9689  196 (\isa{le_less_trans}: @{thm"le_less_trans"[no_vars]}).  nipkow@9645  197 Using the induction hypothesis once more we obtain @{term"j <= f j"}  nipkow@9645  198 which, together with (2) yields @{term"j < f (Suc j)"} (again by  nipkow@9645  199 \isa{le_less_trans}).  nipkow@9645  200 nipkow@9645  201 This last step shows both the power and the danger of automatic proofs: they  nipkow@9645  202 will usually not tell you how the proof goes, because it can be very hard to  nipkow@9645  203 translate the internal proof into a human-readable format. Therefore  nipkow@9645  204 \S\ref{sec:part2?} introduces a language for writing readable yet concise  nipkow@9645  205 proofs.  nipkow@9645  206 nipkow@9645  207 We can now derive the desired @{term"i <= f i"} from \isa{f\_incr}:  nipkow@9689  208 *};  nipkow@9645  209 nipkow@9645  210 lemmas f_incr = f_incr_lem[rulify, OF refl];  nipkow@9645  211 nipkow@9689  212 text{*\noindent  nipkow@9645  213 The final \isa{refl} gets rid of the premise \isa{?k = f ?i}. Again, we could  nipkow@9645  214 have included this derivation in the original statement of the lemma:  nipkow@9689  215 *};  nipkow@9645  216 nipkow@9689  217 lemma f_incr[rulify, OF refl]: "\\i. k = f i \\ i \\ f i";  nipkow@9689  218 (*<*)oops;(*>*)  nipkow@9645  219 nipkow@9645  220 text{*  nipkow@9645  221 \begin{exercise}  nipkow@9645  222 From the above axiom and lemma for \isa{f} show that \isa{f} is the identity.  nipkow@9645  223 \end{exercise}  nipkow@9645  224 nipkow@9645  225 In general, \isa{induct\_tac} can be applied with any rule \isa{r}  nipkow@9645  226 whose conclusion is of the form \isa{?P ?x1 \dots ?xn}, in which case the  nipkow@9645  227 format is  nipkow@9645  228 \begin{ttbox}  nipkow@9645  229 apply(induct_tac y1 ... yn rule: r)  nipkow@9645  230 \end{ttbox}\index{*induct_tac}%  nipkow@9645  231 where \isa{y1}, \dots, \isa{yn} are variables in the first subgoal.  nipkow@9645  232 In fact, \isa{induct\_tac} even allows the conclusion of  nipkow@9645  233 \isa{r} to be an (iterated) conjunction of formulae of the above form, in  nipkow@9645  234 which case the application is  nipkow@9645  235 \begin{ttbox}  nipkow@9645  236 apply(induct_tac y1 ... yn and ... and z1 ... zm rule: r)  nipkow@9645  237 \end{ttbox}  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@9689  245 of \isa{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@9689  250 lemma induct_lem: "(\\n::nat. \\m P n) ==> \\mn::nat. \\m P n) ==> P n";  nipkow@9689  281 by(insert induct_lem, blast);  nipkow@9689  282 nipkow@9689  283 text{*\noindent  nipkow@9645  284 Finally we should mention that HOL already provides the mother of all  nipkow@9645  285 inductions, \emph{wellfounded induction} (\isa{wf\_induct}):  nipkow@9645  286 \begin{quote}  nipkow@9689  287 @{thm[display]"wf_induct"[no_vars]}  nipkow@9645  288 \end{quote}  nipkow@9689  289 where @{term"wf r"} means that the relation \isa{r} is wellfounded.  nipkow@9689  290 For example \isa{less\_induct} is the special case where \isa{r} is \isa{<} on @{typ"nat"}.  nipkow@9645  291 For details see the library.  nipkow@9689  292 *};  nipkow@9645  293 nipkow@9645  294 (*<*)  nipkow@9645  295 end  nipkow@9645  296 (*>*)