nipkow@9722  1 %  nipkow@9722  2 \begin{isabellebody}%  wenzelm@9924  3 \def\isabellecontext{AdvancedInd}%  wenzelm@17056  4 %  wenzelm@17056  5 \isadelimtheory  wenzelm@17056  6 %  wenzelm@17056  7 \endisadelimtheory  wenzelm@17056  8 %  wenzelm@17056  9 \isatagtheory  wenzelm@17056  10 %  wenzelm@17056  11 \endisatagtheory  wenzelm@17056  12 {\isafoldtheory}%  wenzelm@17056  13 %  wenzelm@17056  14 \isadelimtheory  wenzelm@17056  15 %  wenzelm@17056  16 \endisadelimtheory  nipkow@9670  17 %  nipkow@9670  18 \begin{isamarkuptext}%  nipkow@9670  19 \noindent  nipkow@9670  20 Now that we have learned about rules and logic, we take another look at the  paulson@11494  21 finer points of induction. We consider two questions: what to do if the  nipkow@10396  22 proposition to be proved is not directly amenable to induction  nipkow@10396  23 (\S\ref{sec:ind-var-in-prems}), and how to utilize (\S\ref{sec:complete-ind})  nipkow@10396  24 and even derive (\S\ref{sec:derive-ind}) new induction schemas. We conclude  nipkow@10396  25 with an extended example of induction (\S\ref{sec:CTL-revisited}).%  nipkow@9670  26 \end{isamarkuptext}%  wenzelm@11866  27 \isamarkuptrue%  nipkow@9670  28 %  paulson@10878  29 \isamarkupsubsection{Massaging the Proposition%  paulson@10397  30 }  wenzelm@11866  31 \isamarkuptrue%  nipkow@9670  32 %  nipkow@9670  33 \begin{isamarkuptext}%  nipkow@10217  34 \label{sec:ind-var-in-prems}  paulson@11494  35 Often we have assumed that the theorem to be proved is already in a form  paulson@10878  36 that is amenable to induction, but sometimes it isn't.  paulson@10878  37 Here is an example.  paulson@10878  38 Since \isa{hd} and \isa{last} return the first and last element of a  paulson@10878  39 non-empty list, this lemma looks easy to prove:%  nipkow@9670  40 \end{isamarkuptext}%  wenzelm@17175  41 \isamarkuptrue%  wenzelm@17175  42 \isacommand{lemma}\isamarkupfalse%  wenzelm@17175  43 \ {\isachardoublequoteopen}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ last\ xs{\isachardoublequoteclose}\isanewline  wenzelm@17056  44 %  wenzelm@17056  45 \isadelimproof  wenzelm@17056  46 %  wenzelm@17056  47 \endisadelimproof  wenzelm@17056  48 %  wenzelm@17056  49 \isatagproof  wenzelm@17175  50 \isacommand{apply}\isamarkupfalse%  wenzelm@17175  51 {\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}%  nipkow@16069  52 \begin{isamarkuptxt}%  nipkow@16069  53 \noindent  nipkow@16069  54 But induction produces the warning  nipkow@16069  55 \begin{quote}\tt  nipkow@16069  56 Induction variable occurs also among premises!  nipkow@16069  57 \end{quote}  nipkow@16069  58 and leads to the base case  nipkow@16069  59 \begin{isabelle}%  nipkow@16069  60 \ {\isadigit{1}}{\isachardot}\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd\ {\isacharparenleft}rev\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ last\ {\isacharbrackleft}{\isacharbrackright}%  nipkow@16069  61 \end{isabelle}  nipkow@16069  62 Simplification reduces the base case to this:  nipkow@16069  63 \begin{isabelle}  nipkow@16069  64 \ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ []\ =\ last\ []  nipkow@16069  65 \end{isabelle}  nipkow@16069  66 We cannot prove this equality because we do not know what \isa{hd} and  nipkow@16069  67 \isa{last} return when applied to \isa{{\isacharbrackleft}{\isacharbrackright}}.  nipkow@16069  68 nipkow@16069  69 We should not have ignored the warning. Because the induction  nipkow@16069  70 formula is only the conclusion, induction does not affect the occurrence of \isa{xs} in the premises.  nipkow@16069  71 Thus the case that should have been trivial  nipkow@16069  72 becomes unprovable. Fortunately, the solution is easy:\footnote{A similar  nipkow@16069  73 heuristic applies to rule inductions; see \S\ref{sec:rtc}.}  nipkow@16069  74 \begin{quote}  nipkow@16069  75 \emph{Pull all occurrences of the induction variable into the conclusion  nipkow@16069  76 using \isa{{\isasymlongrightarrow}}.}  nipkow@16069  77 \end{quote}  nipkow@16069  78 Thus we should state the lemma as an ordinary  nipkow@16069  79 implication~(\isa{{\isasymlongrightarrow}}), letting  nipkow@16069  80 \attrdx{rule_format} (\S\ref{sec:forward}) convert the  nipkow@16069  81 result to the usual \isa{{\isasymLongrightarrow}} form:%  nipkow@16069  82 \end{isamarkuptxt}%  wenzelm@17175  83 \isamarkuptrue%  wenzelm@17056  84 %  wenzelm@17056  85 \endisatagproof  wenzelm@17056  86 {\isafoldproof}%  wenzelm@17056  87 %  wenzelm@17056  88 \isadelimproof  wenzelm@17056  89 %  wenzelm@17056  90 \endisadelimproof  wenzelm@17175  91 \isacommand{lemma}\isamarkupfalse%  wenzelm@17175  92 \ hd{\isacharunderscore}rev\ {\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ last\ xs{\isachardoublequoteclose}%  wenzelm@17056  93 \isadelimproof  wenzelm@17056  94 %  wenzelm@17056  95 \endisadelimproof  wenzelm@17056  96 %  wenzelm@17056  97 \isatagproof  nipkow@16069  98 %  nipkow@16069  99 \begin{isamarkuptxt}%  nipkow@16069  100 \noindent  nipkow@16069  101 This time, induction leaves us with a trivial base case:  nipkow@16069  102 \begin{isabelle}%  nipkow@16069  103 \ {\isadigit{1}}{\isachardot}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ hd\ {\isacharparenleft}rev\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ last\ {\isacharbrackleft}{\isacharbrackright}%  nipkow@16069  104 \end{isabelle}  nipkow@16069  105 And \isa{auto} completes the proof.  nipkow@16069  106 nipkow@16069  107 If there are multiple premises $A@1$, \dots, $A@n$ containing the  nipkow@16069  108 induction variable, you should turn the conclusion $C$ into  nipkow@16069  109 $A@1 \longrightarrow \cdots A@n \longrightarrow C.$  nipkow@16069  110 Additionally, you may also have to universally quantify some other variables,  nipkow@16069  111 which can yield a fairly complex conclusion. However, \isa{rule{\isacharunderscore}format}  nipkow@16069  112 can remove any number of occurrences of \isa{{\isasymforall}} and  nipkow@16069  113 \isa{{\isasymlongrightarrow}}.  nipkow@16069  114 nipkow@16069  115 \index{induction!on a term}%  nipkow@16069  116 A second reason why your proposition may not be amenable to induction is that  nipkow@16069  117 you want to induct on a complex term, rather than a variable. In  nipkow@16069  118 general, induction on a term~$t$ requires rephrasing the conclusion~$C$  nipkow@16069  119 as  nipkow@16069  120 \label{eqn:ind-over-term}  nipkow@16069  121 \forall y@1 \dots y@n.~ x = t \longrightarrow C.  nipkow@16069  122   nipkow@16069  123 where $y@1 \dots y@n$ are the free variables in $t$ and $x$ is a new variable.  nipkow@16069  124 Now you can perform induction on~$x$. An example appears in  nipkow@16069  125 \S\ref{sec:complete-ind} below.  nipkow@16069  126 nipkow@16069  127 The very same problem may occur in connection with rule induction. Remember  nipkow@16069  128 that it requires a premise of the form $(x@1,\dots,x@k) \in R$, where $R$ is  nipkow@16069  129 some inductively defined set and the $x@i$ are variables. If instead we have  nipkow@16069  130 a premise $t \in R$, where $t$ is not just an $n$-tuple of variables, we  nipkow@16069  131 replace it with $(x@1,\dots,x@k) \in R$, and rephrase the conclusion $C$ as  nipkow@16069  132 $\forall y@1 \dots y@n.~ (x@1,\dots,x@k) = t \longrightarrow C.$  nipkow@16069  133 For an example see \S\ref{sec:CTL-revisited} below.  nipkow@16069  134 nipkow@16069  135 Of course, all premises that share free variables with $t$ need to be pulled into  nipkow@16069  136 the conclusion as well, under the \isa{{\isasymforall}}, again using \isa{{\isasymlongrightarrow}} as shown above.  nipkow@16069  137 nipkow@16069  138 Readers who are puzzled by the form of statement  nipkow@16069  139 (\ref{eqn:ind-over-term}) above should remember that the  nipkow@16069  140 transformation is only performed to permit induction. Once induction  nipkow@16069  141 has been applied, the statement can be transformed back into something quite  nipkow@16069  142 intuitive. For example, applying wellfounded induction on $x$ (w.r.t.\  nipkow@16069  143 $\prec$) to (\ref{eqn:ind-over-term}) and transforming the result a  nipkow@16069  144 little leads to the goal  nipkow@16069  145 $\bigwedge\overline{y}.\  nipkow@16069  146  \forall \overline{z}.\ t\,\overline{z} \prec t\,\overline{y}\ \longrightarrow\ C\,\overline{z}  nipkow@16069  147  \ \Longrightarrow\ C\,\overline{y}$  nipkow@16069  148 where $\overline{y}$ stands for $y@1 \dots y@n$ and the dependence of $t$ and  nipkow@16069  149 $C$ on the free variables of $t$ has been made explicit.  nipkow@16069  150 Unfortunately, this induction schema cannot be expressed as a  nipkow@16069  151 single theorem because it depends on the number of free variables in $t$ ---  nipkow@16069  152 the notation $\overline{y}$ is merely an informal device.%  nipkow@16069  153 \end{isamarkuptxt}%  wenzelm@17175  154 \isamarkuptrue%  wenzelm@17056  155 %  wenzelm@17056  156 \endisatagproof  wenzelm@17056  157 {\isafoldproof}%  wenzelm@17056  158 %  wenzelm@17056  159 \isadelimproof  wenzelm@17056  160 %  wenzelm@17056  161 \endisadelimproof  nipkow@9670  162 %  paulson@10878  163 \isamarkupsubsection{Beyond Structural and Recursion Induction%  paulson@10397  164 }  wenzelm@11866  165 \isamarkuptrue%  nipkow@9670  166 %  nipkow@9670  167 \begin{isamarkuptext}%  nipkow@10217  168 \label{sec:complete-ind}  paulson@10878  169 So far, inductive proofs were by structural induction for  nipkow@9670  170 primitive recursive functions and recursion induction for total recursive  nipkow@9670  171 functions. But sometimes structural induction is awkward and there is no  paulson@10878  172 recursive function that could furnish a more appropriate  paulson@10878  173 induction schema. In such cases a general-purpose induction schema can  nipkow@9670  174 be helpful. We show how to apply such induction schemas by an example.  nipkow@9670  175 nipkow@9670  176 Structural induction on \isa{nat} is  paulson@11494  177 usually known as mathematical induction. There is also \textbf{complete}  paulson@11494  178 \index{induction!complete}%  paulson@11494  179 induction, where you prove $P(n)$ under the assumption that $P(m)$  paulson@11494  180 `holds for all \$m