nipkow@9645  1 (*<*)  wenzelm@58860  2 theory AdvancedInd imports Main begin  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  paulson@11494  7 finer points of induction. We consider two questions: 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}).  wenzelm@58860  12 *}  nipkow@9645  13 wenzelm@58860  14 subsection{*Massaging the Proposition*}  nipkow@9645  15 nipkow@10217  16 text{*\label{sec:ind-var-in-prems}  paulson@11494  17 Often we have assumed that the theorem to be proved is already in a form  paulson@10885  18 that is amenable to induction, but sometimes it isn't.  paulson@10885  19 Here is an example.  paulson@10885  20 Since @{term"hd"} and @{term"last"} return the first and last element of a  paulson@10885  21 non-empty list, this lemma looks easy to prove:  wenzelm@58860  22 *}  nipkow@9645  23 paulson@10885  24 lemma "xs \ [] \ hd(rev xs) = last xs"  paulson@10885  25 apply(induct_tac xs)  nipkow@9645  26 nipkow@9645  27 txt{*\noindent  paulson@10885  28 But induction produces the warning  nipkow@9645  29 \begin{quote}\tt  nipkow@9645  30 Induction variable occurs also among premises!  nipkow@9645  31 \end{quote}  nipkow@9645  32 and leads to the base case  nipkow@10363  33 @{subgoals[display,indent=0,goals_limit=1]}  paulson@11494  34 Simplification reduces the base case to this:  nipkow@9723  35 \begin{isabelle}  nipkow@9645  36 \ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ []\ =\ last\ []  nipkow@9723  37 \end{isabelle}  nipkow@10242  38 We cannot prove this equality because we do not know what @{term hd} and  nipkow@10242  39 @{term last} return when applied to @{term"[]"}.  nipkow@9645  40 paulson@10885  41 We should not have ignored the warning. Because the induction  paulson@10885  42 formula is only the conclusion, induction does not affect the occurrence of @{term xs} in the premises.  paulson@10885  43 Thus the case that should have been trivial  paulson@11494  44 becomes unprovable. Fortunately, the solution is easy:\footnote{A similar  nipkow@10242  45 heuristic applies to rule inductions; see \S\ref{sec:rtc}.}  nipkow@9645  46 \begin{quote}  nipkow@9645  47 \emph{Pull all occurrences of the induction variable into the conclusion  nipkow@9792  48 using @{text"\"}.}  nipkow@9645  49 \end{quote}  paulson@10885  50 Thus we should state the lemma as an ordinary  paulson@10885  51 implication~(@{text"\"}), letting  paulson@11494  52 \attrdx{rule_format} (\S\ref{sec:forward}) convert the  paulson@10885  53 result to the usual @{text"\"} form:  wenzelm@58860  54 *}  wenzelm@58860  55 (*<*)oops(*>*)  wenzelm@58860  56 lemma hd_rev [rule_format]: "xs \ [] \ hd(rev xs) = last xs"  nipkow@9645  57 (*<*)  wenzelm@58860  58 apply(induct_tac xs)  nipkow@9645  59 (*>*)  nipkow@9645  60 nipkow@10420  61 txt{*\noindent  paulson@10885  62 This time, induction leaves us with a trivial base case:  nipkow@10420  63 @{subgoals[display,indent=0,goals_limit=1]}  paulson@10885  64 And @{text"auto"} completes the proof.  nipkow@9645  65 paulson@10885  66 If there are multiple premises $A@1$, \dots, $A@n$ containing the  nipkow@9645  67 induction variable, you should turn the conclusion $C$ into  paulson@11494  68 $A@1 \longrightarrow \cdots A@n \longrightarrow C.$  nipkow@9645  69 Additionally, you may also have to universally quantify some other variables,  nipkow@11196  70 which can yield a fairly complex conclusion. However, @{text rule_format}  paulson@10885  71 can remove any number of occurrences of @{text"\"} and  paulson@10885  72 @{text"\"}.  nipkow@9645  73 paulson@11494  74 \index{induction!on a term}%  nipkow@9645  75 A second reason why your proposition may not be amenable to induction is that  paulson@11494  76 you want to induct on a complex term, rather than a variable. In  paulson@11494  77 general, induction on a term~$t$ requires rephrasing the conclusion~$C$  nipkow@10217  78 as  nipkow@11277  79 \label{eqn:ind-over-term}  paulson@11494  80 \forall y@1 \dots y@n.~ x = t \longrightarrow C.  nipkow@11277  81   paulson@11494  82 where $y@1 \dots y@n$ are the free variables in $t$ and $x$ is a new variable.  wenzelm@12815  83 Now you can perform induction on~$x$. An example appears in  nipkow@10217  84 \S\ref{sec:complete-ind} below.  nipkow@10217  85 nipkow@10217  86 The very same problem may occur in connection with rule induction. Remember  nipkow@10217  87 that it requires a premise of the form $(x@1,\dots,x@k) \in R$, where $R$ is  nipkow@10217  88 some inductively defined set and the $x@i$ are variables. If instead we have  nipkow@10217  89 a premise $t \in R$, where $t$ is not just an $n$-tuple of variables, we  nipkow@10217  90 replace it with $(x@1,\dots,x@k) \in R$, and rephrase the conclusion $C$ as  paulson@11494  91 $\forall y@1 \dots y@n.~ (x@1,\dots,x@k) = t \longrightarrow C.$  nipkow@10217  92 For an example see \S\ref{sec:CTL-revisited} below.  nipkow@10281  93 nipkow@10281  94 Of course, all premises that share free variables with $t$ need to be pulled into  nipkow@10281  95 the conclusion as well, under the @{text"\"}, again using @{text"\"} as shown above.  nipkow@11277  96 nipkow@11277  97 Readers who are puzzled by the form of statement  nipkow@11277  98 (\ref{eqn:ind-over-term}) above should remember that the  nipkow@11277  99 transformation is only performed to permit induction. Once induction  nipkow@11277  100 has been applied, the statement can be transformed back into something quite  nipkow@11277  101 intuitive. For example, applying wellfounded induction on $x$ (w.r.t.\  nipkow@11277  102 $\prec$) to (\ref{eqn:ind-over-term}) and transforming the result a  nipkow@11277  103 little leads to the goal  nipkow@11278  104 $\bigwedge\overline{y}.\  nipkow@11278  105  \forall \overline{z}.\ t\,\overline{z} \prec t\,\overline{y}\ \longrightarrow\ C\,\overline{z}  nipkow@11278  106  \ \Longrightarrow\ C\,\overline{y}$  nipkow@11278  107 where $\overline{y}$ stands for $y@1 \dots y@n$ and the dependence of $t$ and  nipkow@11278  108 $C$ on the free variables of $t$ has been made explicit.  nipkow@11278  109 Unfortunately, this induction schema cannot be expressed as a  nipkow@11278  110 single theorem because it depends on the number of free variables in $t$ ---  nipkow@11278  111 the notation $\overline{y}$ is merely an informal device.  nipkow@11277  112 *}  nipkow@12492  113 (*<*)by auto(*>*)  nipkow@9645  114 wenzelm@58860  115 subsection{*Beyond Structural and Recursion Induction*}  nipkow@9645  116 nipkow@10217  117 text{*\label{sec:complete-ind}  paulson@10885  118 So far, inductive proofs were by structural induction for  nipkow@9645  119 primitive recursive functions and recursion induction for total recursive  nipkow@9645  120 functions. But sometimes structural induction is awkward and there is no  paulson@10885  121 recursive function that could furnish a more appropriate  paulson@10885  122 induction schema. In such cases a general-purpose induction schema can  nipkow@9645  123 be helpful. We show how to apply such induction schemas by an example.  nipkow@9645  124 nipkow@9792  125 Structural induction on @{typ"nat"} is  paulson@11494  126 usually known as mathematical induction. There is also \textbf{complete}  paulson@11494  127 \index{induction!complete}%  paulson@11494  128 induction, where you prove $P(n)$ under the assumption that $P(m)$  paulson@11494  129 holds for all $m nat"  wenzelm@48994  136  where f_ax: "f(f(n)) < f(Suc(n))"  nipkow@9645  137 nipkow@11256  138 text{*  nipkow@11256  139 \begin{warn}  nipkow@11256  140 We discourage the use of axioms because of the danger of  nipkow@11256  141 inconsistencies. Axiom @{text f_ax} does  nipkow@11256  142 not introduce an inconsistency because, for example, the identity function  nipkow@11256  143 satisfies it. Axioms can be useful in exploratory developments, say when  nipkow@11256  144 you assume some well-known theorems so that you can quickly demonstrate some  nipkow@11256  145 point about methodology. If your example turns into a substantial proof  nipkow@11256  146 development, you should replace axioms by theorems.  nipkow@11256  147 \end{warn}\noindent  paulson@10885  148 The axiom for @{term"f"} implies @{prop"n <= f n"}, which can  nipkow@11196  149 be proved by induction on \mbox{@{term"f n"}}. Following the recipe outlined  nipkow@9645  150 above, we have to phrase the proposition as follows to allow induction:  wenzelm@58860  151 *}  nipkow@9645  152 wenzelm@58860  153 lemma f_incr_lem: "\i. k = f i \ i \ f i"  nipkow@9645  154 nipkow@9645  155 txt{*\noindent  nipkow@10363  156 To perform induction on @{term k} using @{thm[source]nat_less_induct}, we use  nipkow@10363  157 the same general induction method as for recursion induction (see  nipkow@25258  158 \S\ref{sec:fun-induction}):  wenzelm@58860  159 *}  nipkow@9645  160 wenzelm@58860  161 apply(induct_tac k rule: nat_less_induct)  nipkow@10363  162 nipkow@10363  163 txt{*\noindent  paulson@11494  164 We get the following proof state:  nipkow@10363  165 @{subgoals[display,indent=0,margin=65]}  nipkow@10363  166 After stripping the @{text"\i"}, the proof continues with a case  nipkow@12699  167 distinction on @{term"i"}. The case @{prop"i = (0::nat)"} is trivial and we focus on  nipkow@10363  168 the other case:  nipkow@10363  169 *}  nipkow@10363  170 nipkow@11196  171 apply(rule allI)  nipkow@11196  172 apply(case_tac i)  nipkow@11196  173  apply(simp)  nipkow@10363  174 txt{*  nipkow@10363  175 @{subgoals[display,indent=0]}  nipkow@11196  176 *}  nipkow@11196  177 by(blast intro!: f_ax Suc_leI intro: le_less_trans)  nipkow@9645  178 nipkow@9645  179 text{*\noindent  nipkow@11196  180 If you find the last step puzzling, here are the two lemmas it employs:  paulson@10885  181 \begin{isabelle}  paulson@10885  182 @{thm Suc_leI[no_vars]}  paulson@10885  183 \rulename{Suc_leI}\isanewline  paulson@10885  184 @{thm le_less_trans[no_vars]}  paulson@10885  185 \rulename{le_less_trans}  paulson@10885  186 \end{isabelle}  paulson@10885  187 %  nipkow@9792  188 The proof goes like this (writing @{term"j"} instead of @{typ"nat"}).  nipkow@9792  189 Since @{prop"i = Suc j"} it suffices to show  paulson@10885  190 \hbox{@{prop"j < f(Suc j)"}},  paulson@10885  191 by @{thm[source]Suc_leI}\@. This is  nipkow@9792  192 proved as follows. From @{thm[source]f_ax} we have @{prop"f (f j) < f (Suc j)"}  paulson@10885  193 (1) which implies @{prop"f j <= f (f j)"} by the induction hypothesis.  paulson@10885  194 Using (1) once more we obtain @{prop"f j < f(Suc j)"} (2) by the transitivity  paulson@10885  195 rule @{thm[source]le_less_trans}.  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 paulson@11494  200 This last step shows both the power and the danger of automatic proofs. They  paulson@11494  201 will usually not tell you how the proof goes, because it can be hard to  paulson@11494  202 translate the internal proof into a human-readable format. Automatic  paulson@11494  203 proofs are easy to write but hard to read and understand.  nipkow@9645  204 paulson@11494  205 The desired result, @{prop"i <= f i"}, follows from @{thm[source]f_incr_lem}:  wenzelm@58860  206 *}  nipkow@9645  207 wenzelm@58860  208 lemmas f_incr = f_incr_lem[rule_format, OF refl]  nipkow@9645  209 nipkow@9689  210 text{*\noindent  paulson@10885  211 The final @{thm[source]refl} gets rid of the premise @{text"?k = f ?i"}.  paulson@10885  212 We could have included this derivation in the original statement of the lemma:  wenzelm@58860  213 *}  nipkow@9645  214 wenzelm@58860  215 lemma f_incr[rule_format, OF refl]: "\i. k = f i \ i \ f i"  wenzelm@58860  216 (*<*)oops(*>*)  nipkow@9645  217 nipkow@9645  218 text{*  nipkow@11256  219 \begin{exercise}  nipkow@11256  220 From the axiom and lemma for @{term"f"}, show that @{term"f"} is the  nipkow@11256  221 identity function.  nipkow@11256  222 \end{exercise}  nipkow@9645  223 paulson@11428  224 Method \methdx{induct_tac} can be applied with any rule$r$ nipkow@9792  225 whose conclusion is of the form${?}P~?x@1 \dots ?x@n$, in which case the  nipkow@9645  226 format is  nipkow@9792  227 \begin{quote}  nipkow@9792  228 \isacommand{apply}@{text"(induct_tac"}$y@1 \dots y@n$@{text"rule:"}$r$@{text")"}  paulson@11428  229 \end{quote}  wenzelm@27320  230 where$y@1, \dots, y@n\$ are variables in the conclusion of the first subgoal.  paulson@10885  231 nipkow@11256  232 A further useful induction rule is @{thm[source]length_induct},  nipkow@11256  233 induction on the length of a list\indexbold{*length_induct}  nipkow@11256  234 @{thm[display]length_induct[no_vars]}  nipkow@11256  235 which is a special case of @{thm[source]measure_induct}  nipkow@11256  236 @{thm[display]measure_induct[no_vars]}  nipkow@11256  237 where @{term f} may be any function into type @{typ nat}.  nipkow@11256  238 *}  nipkow@9645  239 wenzelm@58860  240 subsection{*Derivation of New Induction Schemas*}  nipkow@9689  241 nipkow@9689  242 text{*\label{sec:derive-ind}  paulson@11494  243 \index{induction!deriving new schemas}%  nipkow@9689  244 Induction schemas are ordinary theorems and you can derive new ones  paulson@11494  245 whenever you wish. This section shows you how, using the example  nipkow@9933  246 of @{thm[source]nat_less_induct}. Assume we only have structural induction  paulson@11494  247 available for @{typ"nat"} and want to derive complete induction. We  paulson@11494  248 must generalize the statement as shown:  wenzelm@58860  249 *}  nipkow@9689  250 wenzelm@58860  251 lemma induct_lem: "(\n::nat. \m P n) \ \mn::nat. \m P n) \ P n"  wenzelm@58860  276 by(insert induct_lem, blast)  nipkow@9689  277 nipkow@9933  278 text{*  paulson@11494  279 HOL already provides the mother of  nipkow@10396  280 all inductions, well-founded induction (see \S\ref{sec:Well-founded}). For  paulson@10885  281 example theorem @{thm[source]nat_less_induct} is  nipkow@10396  282 a special case of @{thm[source]wf_induct} where @{term r} is @{text"<"} on  paulson@10885  283 @{typ nat}. The details can be found in theory \isa{Wellfounded_Recursion}.  nipkow@10654  284 *}  nipkow@10654  285 (*<*)end(*>*)