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: