author nipkow Tue Oct 17 13:28:57 2000 +0200 (2000-10-17) changeset 10236 7626cb4e1407 parent 10217 e61e7e1eacaf child 10242 028f54cd2cc9 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:

    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 $C$

   105 as

   106 $\forall y@1 \dots y@n.~ x = t \longrightarrow C$

   107 where $y@1 \dots y@n$ are the free variables in $t$ and $x$ is new, and

   108 perform induction on $x$ afterwards. An example appears in

   109 \S\ref{sec:complete-ind} below.

   110

   111 The very same problem may occur in connection with rule induction. Remember

   112 that it requires a premise of the form $(x@1,\dots,x@k) \in R$, where $R$ is

   113 some inductively defined set and the $x@i$ are variables.  If instead we have

   114 a premise $t \in R$, where $t$ is not just an $n$-tuple of variables, we

   115 replace it with $(x@1,\dots,x@k) \in R$, and rephrase the conclusion $C$ as

   116 $\forall y@1 \dots y@n.~ (x@1,\dots,x@k) = t \longrightarrow C$

   117 For an example see \S\ref{sec:CTL-revisited} below.%

   118 \end{isamarkuptext}%

   119 %

   120 \isamarkupsubsection{Beyond structural and recursion induction}

   121 %

   122 \begin{isamarkuptext}%

   123 \label{sec:complete-ind}

   124 So far, inductive proofs where by structural induction for

   125 primitive recursive functions and recursion induction for total recursive

   126 functions. But sometimes structural induction is awkward and there is no

   127 recursive function in sight either that could furnish a more appropriate

   128 induction schema. In such cases some existing standard induction schema can

   129 be helpful. We show how to apply such induction schemas by an example.

   130

   131 Structural induction on \isa{nat} is

   132 usually known as mathematical induction''. There is also complete

   133 induction'', where you must prove $P(n)$ under the assumption that $P(m)$

   134 holds for all $m<n$. In Isabelle, this is the theorem \isa{nat{\isacharunderscore}less{\isacharunderscore}induct}:

   135 \begin{isabelle}%

   136 \ \ \ \ \ {\isacharparenleft}{\isasymAnd}n{\isachardot}\ {\isasymforall}m{\isachardot}\ m\ {\isacharless}\ n\ {\isasymlongrightarrow}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n%

   137 \end{isabelle}

   138 Here is an example of its application.%

   139 \end{isamarkuptext}%

   140 \isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isacharequal}{\isachargreater}\ nat{\isachardoublequote}\isanewline

   141 \isacommand{axioms}\ f{\isacharunderscore}ax{\isacharcolon}\ {\isachardoublequote}f{\isacharparenleft}f{\isacharparenleft}n{\isacharparenright}{\isacharparenright}\ {\isacharless}\ f{\isacharparenleft}Suc{\isacharparenleft}n{\isacharparenright}{\isacharparenright}{\isachardoublequote}%

   142 \begin{isamarkuptext}%

   143 \noindent

   144 From the above axiom\footnote{In general, the use of axioms is strongly

   145 discouraged, because of the danger of inconsistencies. The above axiom does

   146 not introduce an inconsistency because, for example, the identity function

   147 satisfies it.}

   148 for \isa{f} it follows that \isa{n\ {\isasymle}\ f\ n}, which can

   149 be proved by induction on \isa{f\ n}. Following the recipy outlined

   150 above, we have to phrase the proposition as follows to allow induction:%

   151 \end{isamarkuptext}%

   152 \isacommand{lemma}\ f{\isacharunderscore}incr{\isacharunderscore}lem{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i{\isachardot}\ k\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isachardoublequote}%

   153 \begin{isamarkuptxt}%

   154 \noindent

   155 To perform induction on \isa{k} using \isa{nat{\isacharunderscore}less{\isacharunderscore}induct}, we use the same

   156 general induction method as for recursion induction (see

   157 \S\ref{sec:recdef-induction}):%

   158 \end{isamarkuptxt}%

   159 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ k\ rule{\isacharcolon}\ nat{\isacharunderscore}less{\isacharunderscore}induct{\isacharparenright}%

   160 \begin{isamarkuptxt}%

   161 \noindent

   162 which leaves us with the following proof state:

   163 \begin{isabelle}

   164 \ 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

   165 \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymforall}\mbox{i}.\ \mbox{n}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i}

   166 \end{isabelle}

   167 After stripping the \isa{{\isasymforall}i}, the proof continues with a case

   168 distinction on \isa{i}. The case \isa{i\ {\isacharequal}\ {\isadigit{0}}} is trivial and we focus on

   169 the other case:

   170 \begin{isabelle}

   171 \ 1.\ {\isasymAnd}\mbox{n}\ \mbox{i}\ \mbox{nat}.\isanewline

   172 \ \ \ \ \ \ \ {\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

   173 \ \ \ \ \ \ \ {\isasymLongrightarrow}\ \mbox{n}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i}

   174 \end{isabelle}%

   175 \end{isamarkuptxt}%

   176 \isacommand{by}{\isacharparenleft}blast\ intro{\isacharbang}{\isacharcolon}\ f{\isacharunderscore}ax\ Suc{\isacharunderscore}leI\ intro{\isacharcolon}\ le{\isacharunderscore}less{\isacharunderscore}trans{\isacharparenright}%

   177 \begin{isamarkuptext}%

   178 \noindent

   179 It is not surprising if you find the last step puzzling.

   180 The proof goes like this (writing \isa{j} instead of \isa{nat}).

   181 Since \isa{i\ {\isacharequal}\ Suc\ j} it suffices to show

   182 \isa{j\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}} (by \isa{Suc{\isacharunderscore}leI}: \isa{m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ Suc\ m\ {\isasymle}\ n}). This is

   183 proved as follows. From \isa{f{\isacharunderscore}ax} we have \isa{f\ {\isacharparenleft}f\ j{\isacharparenright}\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}}

   184 (1) which implies \isa{f\ j\ {\isasymle}\ f\ {\isacharparenleft}f\ j{\isacharparenright}} (by the induction hypothesis).

   185 Using (1) once more we obtain \isa{f\ j\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}} (2) by transitivity

   186 (\isa{le{\isacharunderscore}less{\isacharunderscore}trans}: \isa{{\isasymlbrakk}i\ {\isasymle}\ j{\isacharsemicolon}\ j\ {\isacharless}\ k{\isasymrbrakk}\ {\isasymLongrightarrow}\ i\ {\isacharless}\ k}).

   187 Using the induction hypothesis once more we obtain \isa{j\ {\isasymle}\ f\ j}

   188 which, together with (2) yields \isa{j\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}} (again by

   189 \isa{le{\isacharunderscore}less{\isacharunderscore}trans}).

   190

   191 This last step shows both the power and the danger of automatic proofs: they

   192 will usually not tell you how the proof goes, because it can be very hard to

   193 translate the internal proof into a human-readable format. Therefore

   194 \S\ref{sec:part2?} introduces a language for writing readable yet concise

   195 proofs.

   196

   197 We can now derive the desired \isa{i\ {\isasymle}\ f\ i} from \isa{f{\isacharunderscore}incr}:%

   198 \end{isamarkuptext}%

   199 \isacommand{lemmas}\ f{\isacharunderscore}incr\ {\isacharequal}\ f{\isacharunderscore}incr{\isacharunderscore}lem{\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ OF\ refl{\isacharbrackright}%

   200 \begin{isamarkuptext}%

   201 \noindent

   202 The final \isa{refl} gets rid of the premise \isa{{\isacharquery}k\ {\isacharequal}\ f\ {\isacharquery}i}. Again,

   203 we could have included this derivation in the original statement of the lemma:%

   204 \end{isamarkuptext}%

   205 \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}%

   206 \begin{isamarkuptext}%

   207 \begin{exercise}

   208 From the above axiom and lemma for \isa{f} show that \isa{f} is the

   209 identity.

   210 \end{exercise}

   211

   212 In general, \isa{induct{\isacharunderscore}tac} can be applied with any rule $r$

   213 whose conclusion is of the form ${?}P~?x@1 \dots ?x@n$, in which case the

   214 format is

   215 \begin{quote}

   216 \isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $y@1 \dots y@n$ \isa{rule{\isacharcolon}} $r$\isa{{\isacharparenright}}

   217 \end{quote}\index{*induct_tac}%

   218 where $y@1, \dots, y@n$ are variables in the first subgoal.

   219 A further example of a useful induction rule is \isa{length{\isacharunderscore}induct},

   220 induction on the length of a list:\indexbold{*length_induct}

   221 \begin{isabelle}%

   222 \ \ \ \ \ {\isacharparenleft}{\isasymAnd}xs{\isachardot}\ {\isasymforall}ys{\isachardot}\ length\ ys\ {\isacharless}\ length\ xs\ {\isasymlongrightarrow}\ P\ ys\ {\isasymLongrightarrow}\ P\ xs{\isacharparenright}\ {\isasymLongrightarrow}\ P\ xs%

   223 \end{isabelle}

   224

   225 In fact, \isa{induct{\isacharunderscore}tac} even allows the conclusion of

   226 $r$ to be an (iterated) conjunction of formulae of the above form, in

   227 which case the application is

   228 \begin{quote}

   229 \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}}

   230 \end{quote}%

   231 \end{isamarkuptext}%

   232 %

   233 \isamarkupsubsection{Derivation of new induction schemas}

   234 %

   235 \begin{isamarkuptext}%

   236 \label{sec:derive-ind}

   237 Induction schemas are ordinary theorems and you can derive new ones

   238 whenever you wish.  This section shows you how to, using the example

   239 of \isa{nat{\isacharunderscore}less{\isacharunderscore}induct}. Assume we only have structural induction

   240 available for \isa{nat} and want to derive complete induction. This

   241 requires us to generalize the statement first:%

   242 \end{isamarkuptext}%

   243 \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

   244 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ n{\isacharparenright}%

   245 \begin{isamarkuptxt}%

   246 \noindent

   247 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

   248 hypothesis and case \isa{m\ {\isacharequal}\ n} follows from the assumption, again using

   249 the induction hypothesis:%

   250 \end{isamarkuptxt}%

   251 \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline

   252 \isacommand{by}{\isacharparenleft}blast\ elim{\isacharcolon}less{\isacharunderscore}SucE{\isacharparenright}%

   253 \begin{isamarkuptext}%

   254 \noindent

   255 The elimination rule \isa{less{\isacharunderscore}SucE} expresses the case distinction:

   256 \begin{isabelle}%

   257 \ \ \ \ \ {\isasymlbrakk}m\ {\isacharless}\ Suc\ n{\isacharsemicolon}\ m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ m\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P%

   258 \end{isabelle}

   259

   260 Now it is straightforward to derive the original version of

   261 \isa{nat{\isacharunderscore}less{\isacharunderscore}induct} by manipulting the conclusion of the above lemma:

   262 instantiate \isa{n} by \isa{Suc\ n} and \isa{m} by \isa{n} and

   263 remove the trivial condition \isa{n\ {\isacharless}\ Sc\ n}. Fortunately, this

   264 happens automatically when we add the lemma as a new premise to the

   265 desired goal:%

   266 \end{isamarkuptext}%

   267 \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

   268 \isacommand{by}{\isacharparenleft}insert\ induct{\isacharunderscore}lem{\isacharcomma}\ blast{\isacharparenright}%

   269 \begin{isamarkuptext}%

   270 Finally we should mention that HOL already provides the mother of all

   271 inductions, \textbf{wellfounded

   272 induction}\indexbold{induction!wellfounded}\index{wellfounded

   273 induction|see{induction, wellfounded}} (\isa{wf{\isacharunderscore}induct}):

   274 \begin{isabelle}%

   275 \ \ \ \ \ {\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%

   276 \end{isabelle}

   277 where \isa{wf\ r} means that the relation \isa{r} is wellfounded

   278 (see \S\ref{sec:wellfounded}).

   279 For example, theorem \isa{nat{\isacharunderscore}less{\isacharunderscore}induct} can be viewed (and

   280 derived) as a special case of \isa{wf{\isacharunderscore}induct} where

   281 \isa{r} is \isa{{\isacharless}} on \isa{nat}. The details can be found in the HOL library.

   282 For a mathematical account of wellfounded induction see, for example, \cite{Baader-Nipkow}.%

   283 \end{isamarkuptext}%

   284 \end{isabellebody}%

   285 %%% Local Variables:

   286 %%% mode: latex

   287 %%% TeX-master: "root"

   288 %%% End: