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