doc-src/TutorialI/Misc/document/AdvancedInd.tex
author nipkow
Thu Sep 14 17:46:00 2000 +0200 (2000-09-14)
changeset 9958 67f2920862c7
parent 9933 9feb1e0c4cb3
child 10186 499637e8f2c6
permissions -rw-r--r--
*** empty log message ***
     1 %
     2 \begin{isabellebody}%
     3 \def\isabellecontext{AdvancedInd}%
     4 %
     5 \begin{isamarkuptext}%
     6 \noindent
     7 Now that we have learned about rules and logic, we take another look at the
     8 finer points of induction. The two questions we answer are: what to do if the
     9 proposition to be proved is not directly amenable to induction, and how to
    10 utilize and even derive new induction schemas.%
    11 \end{isamarkuptext}%
    12 %
    13 \isamarkupsubsection{Massaging the proposition\label{sec:ind-var-in-prems}}
    14 %
    15 \begin{isamarkuptext}%
    16 \noindent
    17 So far we have assumed that the theorem we want to prove is already in a form
    18 that is amenable to induction, but this is not always the case:%
    19 \end{isamarkuptext}%
    20 \isacommand{lemma}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ last\ xs{\isachardoublequote}\isanewline
    21 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}%
    22 \begin{isamarkuptxt}%
    23 \noindent
    24 (where \isa{hd} and \isa{last} return the first and last element of a
    25 non-empty list)
    26 produces the warning
    27 \begin{quote}\tt
    28 Induction variable occurs also among premises!
    29 \end{quote}
    30 and leads to the base case
    31 \begin{isabelle}
    32 \ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ (rev\ [])\ =\ last\ []
    33 \end{isabelle}
    34 which, after simplification, becomes
    35 \begin{isabelle}
    36 \ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ []\ =\ last\ []
    37 \end{isabelle}
    38 We cannot prove this equality because we do not know what \isa{hd} and
    39 \isa{last} return when applied to \isa{{\isacharbrackleft}{\isacharbrackright}}.
    40 
    41 The point is that we have violated the above warning. Because the induction
    42 formula is only the conclusion, the occurrence of \isa{xs} in the premises is
    43 not modified by induction. Thus the case that should have been trivial
    44 becomes unprovable. Fortunately, the solution is easy:
    45 \begin{quote}
    46 \emph{Pull all occurrences of the induction variable into the conclusion
    47 using \isa{{\isasymlongrightarrow}}.}
    48 \end{quote}
    49 This means we should prove%
    50 \end{isamarkuptxt}%
    51 \isacommand{lemma}\ hd{\isacharunderscore}rev{\isacharcolon}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ last\ xs{\isachardoublequote}%
    52 \begin{isamarkuptext}%
    53 \noindent
    54 This time, induction leaves us with the following base case
    55 \begin{isabelle}
    56 \ 1.\ []\ {\isasymnoteq}\ []\ {\isasymlongrightarrow}\ hd\ (rev\ [])\ =\ last\ []
    57 \end{isabelle}
    58 which is trivial, and \isa{auto} finishes the whole proof.
    59 
    60 If \isa{hd{\isacharunderscore}rev} is meant to be a simplification rule, you are
    61 done. But if you really need the \isa{{\isasymLongrightarrow}}-version of
    62 \isa{hd{\isacharunderscore}rev}, for example because you want to apply it as an
    63 introduction rule, you need to derive it separately, by combining it with
    64 modus ponens:%
    65 \end{isamarkuptext}%
    66 \isacommand{lemmas}\ hd{\isacharunderscore}revI\ {\isacharequal}\ hd{\isacharunderscore}rev{\isacharbrackleft}THEN\ mp{\isacharbrackright}%
    67 \begin{isamarkuptext}%
    68 \noindent
    69 which yields the lemma we originally set out to prove.
    70 
    71 In case there are multiple premises $A@1$, \dots, $A@n$ containing the
    72 induction variable, you should turn the conclusion $C$ into
    73 \[ A@1 \longrightarrow \cdots A@n \longrightarrow C \]
    74 (see the remark?? in \S\ref{??}).
    75 Additionally, you may also have to universally quantify some other variables,
    76 which can yield a fairly complex conclusion.
    77 Here is a simple example (which is proved by \isa{blast}):%
    78 \end{isamarkuptext}%
    79 \isacommand{lemma}\ simple{\isacharcolon}\ {\isachardoublequote}{\isasymforall}y{\isachardot}\ A\ y\ {\isasymlongrightarrow}\ B\ y\ {\isasymlongrightarrow}\ B\ y\ {\isacharampersand}\ A\ y{\isachardoublequote}%
    80 \begin{isamarkuptext}%
    81 \noindent
    82 You can get the desired lemma by explicit
    83 application of modus ponens and \isa{spec}:%
    84 \end{isamarkuptext}%
    85 \isacommand{lemmas}\ myrule\ {\isacharequal}\ simple{\isacharbrackleft}THEN\ spec{\isacharcomma}\ THEN\ mp{\isacharcomma}\ THEN\ mp{\isacharbrackright}%
    86 \begin{isamarkuptext}%
    87 \noindent
    88 or the wholesale stripping of \isa{{\isasymforall}} and
    89 \isa{{\isasymlongrightarrow}} in the conclusion via \isa{rule{\isacharunderscore}format}%
    90 \end{isamarkuptext}%
    91 \isacommand{lemmas}\ myrule\ {\isacharequal}\ simple{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}%
    92 \begin{isamarkuptext}%
    93 \noindent
    94 yielding \isa{{\isasymlbrakk}A\ y{\isacharsemicolon}\ B\ y{\isasymrbrakk}\ {\isasymLongrightarrow}\ B\ y\ {\isasymand}\ A\ y}.
    95 You can go one step further and include these derivations already in the
    96 statement of your original lemma, thus avoiding the intermediate step:%
    97 \end{isamarkuptext}%
    98 \isacommand{lemma}\ myrule{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\ \ {\isachardoublequote}{\isasymforall}y{\isachardot}\ A\ y\ {\isasymlongrightarrow}\ B\ y\ {\isasymlongrightarrow}\ B\ y\ {\isacharampersand}\ A\ y{\isachardoublequote}%
    99 \begin{isamarkuptext}%
   100 \bigskip
   101 
   102 A second reason why your proposition may not be amenable to induction is that
   103 you want to induct on a whole term, rather than an individual variable. In
   104 general, when inducting on some term $t$ you must rephrase the conclusion as
   105 \[ \forall y@1 \dots y@n.~ x = t \longrightarrow C \] where $y@1 \dots y@n$
   106 are the free variables in $t$ and $x$ is new, and perform induction on $x$
   107 afterwards. An example appears below.%
   108 \end{isamarkuptext}%
   109 %
   110 \isamarkupsubsection{Beyond structural and recursion induction}
   111 %
   112 \begin{isamarkuptext}%
   113 So far, inductive proofs where by structural induction for
   114 primitive recursive functions and recursion induction for total recursive
   115 functions. But sometimes structural induction is awkward and there is no
   116 recursive function in sight either that could furnish a more appropriate
   117 induction schema. In such cases some existing standard induction schema can
   118 be helpful. We show how to apply such induction schemas by an example.
   119 
   120 Structural induction on \isa{nat} is
   121 usually known as ``mathematical induction''. There is also ``complete
   122 induction'', where you must prove $P(n)$ under the assumption that $P(m)$
   123 holds for all $m<n$. In Isabelle, this is the theorem \isa{nat{\isacharunderscore}less{\isacharunderscore}induct}:
   124 \begin{isabelle}%
   125 \ \ \ \ \ {\isacharparenleft}{\isasymAnd}n{\isachardot}\ {\isasymforall}m{\isachardot}\ m\ {\isacharless}\ n\ {\isasymlongrightarrow}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n%
   126 \end{isabelle}
   127 Here is an example of its application.%
   128 \end{isamarkuptext}%
   129 \isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isacharequal}{\isachargreater}\ nat{\isachardoublequote}\isanewline
   130 \isacommand{axioms}\ f{\isacharunderscore}ax{\isacharcolon}\ {\isachardoublequote}f{\isacharparenleft}f{\isacharparenleft}n{\isacharparenright}{\isacharparenright}\ {\isacharless}\ f{\isacharparenleft}Suc{\isacharparenleft}n{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
   131 \begin{isamarkuptext}%
   132 \noindent
   133 From the above axiom\footnote{In general, the use of axioms is strongly
   134 discouraged, because of the danger of inconsistencies. The above axiom does
   135 not introduce an inconsistency because, for example, the identity function
   136 satisfies it.}
   137 for \isa{f} it follows that \isa{n\ {\isasymle}\ f\ n}, which can
   138 be proved by induction on \isa{f\ n}. Following the recipy outlined
   139 above, we have to phrase the proposition as follows to allow induction:%
   140 \end{isamarkuptext}%
   141 \isacommand{lemma}\ f{\isacharunderscore}incr{\isacharunderscore}lem{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i{\isachardot}\ k\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isachardoublequote}%
   142 \begin{isamarkuptxt}%
   143 \noindent
   144 To perform induction on \isa{k} using \isa{nat{\isacharunderscore}less{\isacharunderscore}induct}, we use the same
   145 general induction method as for recursion induction (see
   146 \S\ref{sec:recdef-induction}):%
   147 \end{isamarkuptxt}%
   148 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ k\ rule{\isacharcolon}\ nat{\isacharunderscore}less{\isacharunderscore}induct{\isacharparenright}%
   149 \begin{isamarkuptxt}%
   150 \noindent
   151 which leaves us with the following proof state:
   152 \begin{isabelle}
   153 \ 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
   154 \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymforall}\mbox{i}.\ \mbox{n}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i}
   155 \end{isabelle}
   156 After stripping the \isa{{\isasymforall}i}, the proof continues with a case
   157 distinction on \isa{i}. The case \isa{i\ {\isacharequal}\ \isadigit{0}} is trivial and we focus on
   158 the other case:
   159 \begin{isabelle}
   160 \ 1.\ {\isasymAnd}\mbox{n}\ \mbox{i}\ \mbox{nat}.\isanewline
   161 \ \ \ \ \ \ \ {\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
   162 \ \ \ \ \ \ \ {\isasymLongrightarrow}\ \mbox{n}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i}
   163 \end{isabelle}%
   164 \end{isamarkuptxt}%
   165 \isacommand{by}{\isacharparenleft}blast\ intro{\isacharbang}{\isacharcolon}\ f{\isacharunderscore}ax\ Suc{\isacharunderscore}leI\ intro{\isacharcolon}\ le{\isacharunderscore}less{\isacharunderscore}trans{\isacharparenright}%
   166 \begin{isamarkuptext}%
   167 \noindent
   168 It is not surprising if you find the last step puzzling.
   169 The proof goes like this (writing \isa{j} instead of \isa{nat}).
   170 Since \isa{i\ {\isacharequal}\ Suc\ j} it suffices to show
   171 \isa{j\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}} (by \isa{Suc{\isacharunderscore}leI}: \isa{m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ Suc\ m\ {\isasymle}\ n}). This is
   172 proved as follows. From \isa{f{\isacharunderscore}ax} we have \isa{f\ {\isacharparenleft}f\ j{\isacharparenright}\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}}
   173 (1) which implies \isa{f\ j\ {\isasymle}\ f\ {\isacharparenleft}f\ j{\isacharparenright}} (by the induction hypothesis).
   174 Using (1) once more we obtain \isa{f\ j\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}} (2) by transitivity
   175 (\isa{le{\isacharunderscore}less{\isacharunderscore}trans}: \isa{{\isasymlbrakk}i\ {\isasymle}\ j{\isacharsemicolon}\ j\ {\isacharless}\ k{\isasymrbrakk}\ {\isasymLongrightarrow}\ i\ {\isacharless}\ k}).
   176 Using the induction hypothesis once more we obtain \isa{j\ {\isasymle}\ f\ j}
   177 which, together with (2) yields \isa{j\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}} (again by
   178 \isa{le{\isacharunderscore}less{\isacharunderscore}trans}).
   179 
   180 This last step shows both the power and the danger of automatic proofs: they
   181 will usually not tell you how the proof goes, because it can be very hard to
   182 translate the internal proof into a human-readable format. Therefore
   183 \S\ref{sec:part2?} introduces a language for writing readable yet concise
   184 proofs.
   185 
   186 We can now derive the desired \isa{i\ {\isasymle}\ f\ i} from \isa{f{\isacharunderscore}incr}:%
   187 \end{isamarkuptext}%
   188 \isacommand{lemmas}\ f{\isacharunderscore}incr\ {\isacharequal}\ f{\isacharunderscore}incr{\isacharunderscore}lem{\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ OF\ refl{\isacharbrackright}%
   189 \begin{isamarkuptext}%
   190 \noindent
   191 The final \isa{refl} gets rid of the premise \isa{{\isacharquery}k\ {\isacharequal}\ f\ {\isacharquery}i}. Again,
   192 we could have included this derivation in the original statement of the lemma:%
   193 \end{isamarkuptext}%
   194 \isacommand{lemma}\ f{\isacharunderscore}incr{\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ OF\ refl{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i{\isachardot}\ k\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isachardoublequote}%
   195 \begin{isamarkuptext}%
   196 \begin{exercise}
   197 From the above axiom and lemma for \isa{f} show that \isa{f} is the
   198 identity.
   199 \end{exercise}
   200 
   201 In general, \isa{induct{\isacharunderscore}tac} can be applied with any rule $r$
   202 whose conclusion is of the form ${?}P~?x@1 \dots ?x@n$, in which case the
   203 format is
   204 \begin{quote}
   205 \isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $y@1 \dots y@n$ \isa{rule{\isacharcolon}} $r$\isa{{\isacharparenright}}
   206 \end{quote}\index{*induct_tac}%
   207 where $y@1, \dots, y@n$ are variables in the first subgoal.
   208 In fact, \isa{induct{\isacharunderscore}tac} even allows the conclusion of
   209 $r$ to be an (iterated) conjunction of formulae of the above form, in
   210 which case the application is
   211 \begin{quote}
   212 \isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $y@1 \dots y@n$ \isa{and} \dots\ \isa{and} $z@1 \dots z@m$ \isa{rule{\isacharcolon}} $r$\isa{{\isacharparenright}}
   213 \end{quote}%
   214 \end{isamarkuptext}%
   215 %
   216 \isamarkupsubsection{Derivation of new induction schemas}
   217 %
   218 \begin{isamarkuptext}%
   219 \label{sec:derive-ind}
   220 Induction schemas are ordinary theorems and you can derive new ones
   221 whenever you wish.  This section shows you how to, using the example
   222 of \isa{nat{\isacharunderscore}less{\isacharunderscore}induct}. Assume we only have structural induction
   223 available for \isa{nat} and want to derive complete induction. This
   224 requires us to generalize the statement first:%
   225 \end{isamarkuptext}%
   226 \isacommand{lemma}\ induct{\isacharunderscore}lem{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isasymAnd}n{\isacharcolon}{\isacharcolon}nat{\isachardot}\ {\isasymforall}m{\isacharless}n{\isachardot}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymforall}m{\isacharless}n{\isachardot}\ P\ m{\isachardoublequote}\isanewline
   227 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ n{\isacharparenright}%
   228 \begin{isamarkuptxt}%
   229 \noindent
   230 The base case is trivially true. For the induction step (\isa{m\ {\isacharless}\ Suc\ n}) we distinguish two cases: case \isa{m\ {\isacharless}\ n} is true by induction
   231 hypothesis and case \isa{m\ {\isacharequal}\ n} follows from the assumption, again using
   232 the induction hypothesis:%
   233 \end{isamarkuptxt}%
   234 \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
   235 \isacommand{by}{\isacharparenleft}blast\ elim{\isacharcolon}less{\isacharunderscore}SucE{\isacharparenright}%
   236 \begin{isamarkuptext}%
   237 \noindent
   238 The elimination rule \isa{less{\isacharunderscore}SucE} expresses the case distinction:
   239 \begin{isabelle}%
   240 \ \ \ \ \ {\isasymlbrakk}m\ {\isacharless}\ Suc\ n{\isacharsemicolon}\ m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ m\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P%
   241 \end{isabelle}
   242 
   243 Now it is straightforward to derive the original version of
   244 \isa{nat{\isacharunderscore}less{\isacharunderscore}induct} by manipulting the conclusion of the above lemma:
   245 instantiate \isa{n} by \isa{Suc\ n} and \isa{m} by \isa{n} and
   246 remove the trivial condition \isa{n\ {\isacharless}\ Sc\ n}. Fortunately, this
   247 happens automatically when we add the lemma as a new premise to the
   248 desired goal:%
   249 \end{isamarkuptext}%
   250 \isacommand{theorem}\ nat{\isacharunderscore}less{\isacharunderscore}induct{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isasymAnd}n{\isacharcolon}{\isacharcolon}nat{\isachardot}\ {\isasymforall}m{\isacharless}n{\isachardot}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n{\isachardoublequote}\isanewline
   251 \isacommand{by}{\isacharparenleft}insert\ induct{\isacharunderscore}lem{\isacharcomma}\ blast{\isacharparenright}%
   252 \begin{isamarkuptext}%
   253 Finally we should mention that HOL already provides the mother of all
   254 inductions, \emph{wellfounded induction} (\isa{wf{\isacharunderscore}induct}):
   255 \begin{isabelle}%
   256 \ \ \ \ \ {\isasymlbrakk}wf\ r{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isasymforall}y{\isachardot}\ {\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ r\ {\isasymlongrightarrow}\ P\ y\ {\isasymLongrightarrow}\ P\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ a%
   257 \end{isabelle}
   258 where \isa{wf\ r} means that the relation \isa{r} is wellfounded.
   259 For example, theorem \isa{nat{\isacharunderscore}less{\isacharunderscore}induct} can be viewed (and
   260 derived) as a special case of \isa{wf{\isacharunderscore}induct} where 
   261 \isa{r} is \isa{{\isacharless}} on \isa{nat}. For details see the library.%
   262 \end{isamarkuptext}%
   263 \end{isabellebody}%
   264 %%% Local Variables:
   265 %%% mode: latex
   266 %%% TeX-master: "root"
   267 %%% End: