doc-src/TutorialI/Misc/document/AdvancedInd.tex
author wenzelm
Tue Oct 16 17:07:40 2007 +0200 (2007-10-16)
changeset 25056 743f3603ba8b
parent 19654 2c02a8054616
child 25258 22d16596c306
permissions -rw-r--r--
updated;
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
\begin{equation}\label{eqn:ind-over-term}
nipkow@16069
   121
\forall y@1 \dots y@n.~ x = t \longrightarrow C.
nipkow@16069
   122
\end{equation}
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<n$. In Isabelle, this is the theorem \tdx{nat_less_induct}:
nipkow@9670
   181
\begin{isabelle}%
wenzelm@19654
   182
\ \ \ \ \ {\isacharparenleft}{\isasymAnd}n{\isachardot}\ {\isasymforall}m{\isacharless}n{\isachardot}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n%
wenzelm@9924
   183
\end{isabelle}
paulson@11494
   184
As an application, we prove a property of the following
nipkow@11278
   185
function:%
nipkow@9670
   186
\end{isamarkuptext}%
wenzelm@17175
   187
\isamarkuptrue%
wenzelm@17175
   188
\isacommand{consts}\isamarkupfalse%
wenzelm@17175
   189
\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline
wenzelm@17175
   190
\isacommand{axioms}\isamarkupfalse%
wenzelm@17175
   191
\ f{\isacharunderscore}ax{\isacharcolon}\ {\isachardoublequoteopen}f{\isacharparenleft}f{\isacharparenleft}n{\isacharparenright}{\isacharparenright}\ {\isacharless}\ f{\isacharparenleft}Suc{\isacharparenleft}n{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
nipkow@9670
   192
\begin{isamarkuptext}%
nipkow@11256
   193
\begin{warn}
nipkow@11256
   194
We discourage the use of axioms because of the danger of
nipkow@11256
   195
inconsistencies.  Axiom \isa{f{\isacharunderscore}ax} does
nipkow@11256
   196
not introduce an inconsistency because, for example, the identity function
nipkow@11256
   197
satisfies it.  Axioms can be useful in exploratory developments, say when 
nipkow@11256
   198
you assume some well-known theorems so that you can quickly demonstrate some
nipkow@11256
   199
point about methodology.  If your example turns into a substantial proof
nipkow@11256
   200
development, you should replace axioms by theorems.
nipkow@11256
   201
\end{warn}\noindent
paulson@10878
   202
The axiom for \isa{f} implies \isa{n\ {\isasymle}\ f\ n}, which can
nipkow@11196
   203
be proved by induction on \mbox{\isa{f\ n}}. Following the recipe outlined
nipkow@9670
   204
above, we have to phrase the proposition as follows to allow induction:%
nipkow@9670
   205
\end{isamarkuptext}%
wenzelm@17175
   206
\isamarkuptrue%
wenzelm@17175
   207
\isacommand{lemma}\isamarkupfalse%
wenzelm@17175
   208
\ f{\isacharunderscore}incr{\isacharunderscore}lem{\isacharcolon}\ {\isachardoublequoteopen}{\isasymforall}i{\isachardot}\ k\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isachardoublequoteclose}%
wenzelm@17056
   209
\isadelimproof
wenzelm@17056
   210
%
wenzelm@17056
   211
\endisadelimproof
wenzelm@17056
   212
%
wenzelm@17056
   213
\isatagproof
nipkow@16069
   214
%
nipkow@16069
   215
\begin{isamarkuptxt}%
nipkow@16069
   216
\noindent
nipkow@16069
   217
To perform induction on \isa{k} using \isa{nat{\isacharunderscore}less{\isacharunderscore}induct}, we use
nipkow@16069
   218
the same general induction method as for recursion induction (see
nipkow@16069
   219
\S\ref{sec:recdef-induction}):%
nipkow@16069
   220
\end{isamarkuptxt}%
wenzelm@17175
   221
\isamarkuptrue%
wenzelm@17175
   222
\isacommand{apply}\isamarkupfalse%
wenzelm@17175
   223
{\isacharparenleft}induct{\isacharunderscore}tac\ k\ rule{\isacharcolon}\ nat{\isacharunderscore}less{\isacharunderscore}induct{\isacharparenright}%
nipkow@16069
   224
\begin{isamarkuptxt}%
nipkow@16069
   225
\noindent
nipkow@16069
   226
We get the following proof state:
nipkow@16069
   227
\begin{isabelle}%
wenzelm@19654
   228
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymforall}m{\isacharless}n{\isachardot}\ {\isasymforall}i{\isachardot}\ m\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i\ {\isasymLongrightarrow}\ {\isasymforall}i{\isachardot}\ n\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i%
nipkow@16069
   229
\end{isabelle}
nipkow@16069
   230
After stripping the \isa{{\isasymforall}i}, the proof continues with a case
nipkow@16069
   231
distinction on \isa{i}. The case \isa{i\ {\isacharequal}\ {\isadigit{0}}} is trivial and we focus on
nipkow@16069
   232
the other case:%
nipkow@16069
   233
\end{isamarkuptxt}%
wenzelm@17175
   234
\isamarkuptrue%
wenzelm@17175
   235
\isacommand{apply}\isamarkupfalse%
wenzelm@17175
   236
{\isacharparenleft}rule\ allI{\isacharparenright}\isanewline
wenzelm@17175
   237
\isacommand{apply}\isamarkupfalse%
wenzelm@17175
   238
{\isacharparenleft}case{\isacharunderscore}tac\ i{\isacharparenright}\isanewline
wenzelm@17175
   239
\ \isacommand{apply}\isamarkupfalse%
wenzelm@17175
   240
{\isacharparenleft}simp{\isacharparenright}%
nipkow@16069
   241
\begin{isamarkuptxt}%
nipkow@16069
   242
\begin{isabelle}%
nipkow@16069
   243
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n\ i\ nat{\isachardot}\isanewline
wenzelm@19654
   244
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}{\isasymforall}m{\isacharless}n{\isachardot}\ {\isasymforall}i{\isachardot}\ m\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isacharsemicolon}\ i\ {\isacharequal}\ Suc\ nat{\isasymrbrakk}\ {\isasymLongrightarrow}\ n\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i%
nipkow@16069
   245
\end{isabelle}%
nipkow@16069
   246
\end{isamarkuptxt}%
wenzelm@17175
   247
\isamarkuptrue%
wenzelm@17175
   248
\isacommand{by}\isamarkupfalse%
wenzelm@17175
   249
{\isacharparenleft}blast\ intro{\isacharbang}{\isacharcolon}\ f{\isacharunderscore}ax\ Suc{\isacharunderscore}leI\ intro{\isacharcolon}\ le{\isacharunderscore}less{\isacharunderscore}trans{\isacharparenright}%
wenzelm@17056
   250
\endisatagproof
wenzelm@17056
   251
{\isafoldproof}%
wenzelm@17056
   252
%
wenzelm@17056
   253
\isadelimproof
wenzelm@17056
   254
%
wenzelm@17056
   255
\endisadelimproof
wenzelm@11866
   256
%
nipkow@9670
   257
\begin{isamarkuptext}%
nipkow@9670
   258
\noindent
nipkow@11196
   259
If you find the last step puzzling, here are the two lemmas it employs:
paulson@10878
   260
\begin{isabelle}
paulson@10878
   261
\isa{m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ Suc\ m\ {\isasymle}\ n}
paulson@10878
   262
\rulename{Suc_leI}\isanewline
wenzelm@25056
   263
\isa{{\isasymlbrakk}x\ {\isasymle}\ y{\isacharsemicolon}\ y\ {\isacharless}\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharless}\ z}
paulson@10878
   264
\rulename{le_less_trans}
paulson@10878
   265
\end{isabelle}
paulson@10878
   266
%
nipkow@9670
   267
The proof goes like this (writing \isa{j} instead of \isa{nat}).
nipkow@9792
   268
Since \isa{i\ {\isacharequal}\ Suc\ j} it suffices to show
paulson@10878
   269
\hbox{\isa{j\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}}},
paulson@10878
   270
by \isa{Suc{\isacharunderscore}leI}\@.  This is
nipkow@9792
   271
proved as follows. From \isa{f{\isacharunderscore}ax} we have \isa{f\ {\isacharparenleft}f\ j{\isacharparenright}\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}}
paulson@10878
   272
(1) which implies \isa{f\ j\ {\isasymle}\ f\ {\isacharparenleft}f\ j{\isacharparenright}} by the induction hypothesis.
paulson@10878
   273
Using (1) once more we obtain \isa{f\ j\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}} (2) by the transitivity
paulson@10878
   274
rule \isa{le{\isacharunderscore}less{\isacharunderscore}trans}.
nipkow@9792
   275
Using the induction hypothesis once more we obtain \isa{j\ {\isasymle}\ f\ j}
nipkow@9792
   276
which, together with (2) yields \isa{j\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}} (again by
nipkow@9792
   277
\isa{le{\isacharunderscore}less{\isacharunderscore}trans}).
nipkow@9670
   278
paulson@11494
   279
This last step shows both the power and the danger of automatic proofs.  They
paulson@11494
   280
will usually not tell you how the proof goes, because it can be hard to
paulson@11494
   281
translate the internal proof into a human-readable format.  Automatic
paulson@11494
   282
proofs are easy to write but hard to read and understand.
nipkow@9670
   283
paulson@11494
   284
The desired result, \isa{i\ {\isasymle}\ f\ i}, follows from \isa{f{\isacharunderscore}incr{\isacharunderscore}lem}:%
nipkow@9670
   285
\end{isamarkuptext}%
wenzelm@17175
   286
\isamarkuptrue%
wenzelm@17175
   287
\isacommand{lemmas}\isamarkupfalse%
wenzelm@17175
   288
\ f{\isacharunderscore}incr\ {\isacharequal}\ f{\isacharunderscore}incr{\isacharunderscore}lem{\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ OF\ refl{\isacharbrackright}%
nipkow@9670
   289
\begin{isamarkuptext}%
wenzelm@9698
   290
\noindent
paulson@10878
   291
The final \isa{refl} gets rid of the premise \isa{{\isacharquery}k\ {\isacharequal}\ f\ {\isacharquery}i}. 
paulson@10878
   292
We could have included this derivation in the original statement of the lemma:%
nipkow@9670
   293
\end{isamarkuptext}%
wenzelm@17175
   294
\isamarkuptrue%
wenzelm@17175
   295
\isacommand{lemma}\isamarkupfalse%
wenzelm@17175
   296
\ f{\isacharunderscore}incr{\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ OF\ refl{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymforall}i{\isachardot}\ k\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isachardoublequoteclose}%
wenzelm@17056
   297
\isadelimproof
wenzelm@17056
   298
%
wenzelm@17056
   299
\endisadelimproof
wenzelm@17056
   300
%
wenzelm@17056
   301
\isatagproof
wenzelm@17056
   302
%
wenzelm@17056
   303
\endisatagproof
wenzelm@17056
   304
{\isafoldproof}%
wenzelm@17056
   305
%
wenzelm@17056
   306
\isadelimproof
wenzelm@17056
   307
%
wenzelm@17056
   308
\endisadelimproof
wenzelm@11866
   309
%
nipkow@9670
   310
\begin{isamarkuptext}%
nipkow@11256
   311
\begin{exercise}
nipkow@11256
   312
From the axiom and lemma for \isa{f}, show that \isa{f} is the
nipkow@11256
   313
identity function.
nipkow@11256
   314
\end{exercise}
nipkow@9670
   315
paulson@11428
   316
Method \methdx{induct_tac} can be applied with any rule $r$
nipkow@9792
   317
whose conclusion is of the form ${?}P~?x@1 \dots ?x@n$, in which case the
nipkow@9670
   318
format is
nipkow@9792
   319
\begin{quote}
nipkow@9792
   320
\isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $y@1 \dots y@n$ \isa{rule{\isacharcolon}} $r$\isa{{\isacharparenright}}
paulson@11428
   321
\end{quote}
nipkow@9792
   322
where $y@1, \dots, y@n$ are variables in the first subgoal.
nipkow@11256
   323
The conclusion of $r$ can even be an (iterated) conjunction of formulae of
nipkow@11256
   324
the above form in which case the application is
nipkow@9792
   325
\begin{quote}
nipkow@9792
   326
\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}}
paulson@10878
   327
\end{quote}
paulson@10878
   328
nipkow@11256
   329
A further useful induction rule is \isa{length{\isacharunderscore}induct},
nipkow@11256
   330
induction on the length of a list\indexbold{*length_induct}
nipkow@11256
   331
\begin{isabelle}%
nipkow@11256
   332
\ \ \ \ \ {\isacharparenleft}{\isasymAnd}xs{\isachardot}\ {\isasymforall}ys{\isachardot}\ length\ ys\ {\isacharless}\ length\ xs\ {\isasymlongrightarrow}\ P\ ys\ {\isasymLongrightarrow}\ P\ xs{\isacharparenright}\ {\isasymLongrightarrow}\ P\ xs%
nipkow@11256
   333
\end{isabelle}
nipkow@11256
   334
which is a special case of \isa{measure{\isacharunderscore}induct}
nipkow@11256
   335
\begin{isabelle}%
nipkow@11256
   336
\ \ \ \ \ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ {\isasymforall}y{\isachardot}\ f\ y\ {\isacharless}\ f\ x\ {\isasymlongrightarrow}\ P\ y\ {\isasymLongrightarrow}\ P\ x{\isacharparenright}\ {\isasymLongrightarrow}\ P\ a%
nipkow@11256
   337
\end{isabelle}
nipkow@11256
   338
where \isa{f} may be any function into type \isa{nat}.%
wenzelm@9698
   339
\end{isamarkuptext}%
wenzelm@11866
   340
\isamarkuptrue%
wenzelm@9698
   341
%
paulson@10878
   342
\isamarkupsubsection{Derivation of New Induction Schemas%
paulson@10397
   343
}
wenzelm@11866
   344
\isamarkuptrue%
wenzelm@9698
   345
%
wenzelm@9698
   346
\begin{isamarkuptext}%
wenzelm@9698
   347
\label{sec:derive-ind}
paulson@11494
   348
\index{induction!deriving new schemas}%
wenzelm@9698
   349
Induction schemas are ordinary theorems and you can derive new ones
paulson@11494
   350
whenever you wish.  This section shows you how, using the example
wenzelm@9924
   351
of \isa{nat{\isacharunderscore}less{\isacharunderscore}induct}. Assume we only have structural induction
paulson@11494
   352
available for \isa{nat} and want to derive complete induction.  We
paulson@11494
   353
must generalize the statement as shown:%
wenzelm@9698
   354
\end{isamarkuptext}%
wenzelm@17175
   355
\isamarkuptrue%
wenzelm@17175
   356
\isacommand{lemma}\isamarkupfalse%
wenzelm@17175
   357
\ induct{\isacharunderscore}lem{\isacharcolon}\ {\isachardoublequoteopen}{\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{\isachardoublequoteclose}\isanewline
wenzelm@17056
   358
%
wenzelm@17056
   359
\isadelimproof
wenzelm@17056
   360
%
wenzelm@17056
   361
\endisadelimproof
wenzelm@17056
   362
%
wenzelm@17056
   363
\isatagproof
wenzelm@17175
   364
\isacommand{apply}\isamarkupfalse%
wenzelm@17175
   365
{\isacharparenleft}induct{\isacharunderscore}tac\ n{\isacharparenright}%
nipkow@16069
   366
\begin{isamarkuptxt}%
nipkow@16069
   367
\noindent
nipkow@16069
   368
The base case is vacuously true. For the induction step (\isa{m\ {\isacharless}\ Suc\ n}) we distinguish two cases: case \isa{m\ {\isacharless}\ n} is true by induction
nipkow@16069
   369
hypothesis and case \isa{m\ {\isacharequal}\ n} follows from the assumption, again using
nipkow@16069
   370
the induction hypothesis:%
nipkow@16069
   371
\end{isamarkuptxt}%
wenzelm@17175
   372
\isamarkuptrue%
wenzelm@17175
   373
\ \isacommand{apply}\isamarkupfalse%
wenzelm@17175
   374
{\isacharparenleft}blast{\isacharparenright}\isanewline
wenzelm@17175
   375
\isacommand{by}\isamarkupfalse%
wenzelm@17175
   376
{\isacharparenleft}blast\ elim{\isacharcolon}\ less{\isacharunderscore}SucE{\isacharparenright}%
wenzelm@17056
   377
\endisatagproof
wenzelm@17056
   378
{\isafoldproof}%
wenzelm@17056
   379
%
wenzelm@17056
   380
\isadelimproof
wenzelm@17056
   381
%
wenzelm@17056
   382
\endisadelimproof
wenzelm@11866
   383
%
wenzelm@9698
   384
\begin{isamarkuptext}%
wenzelm@9698
   385
\noindent
nipkow@11196
   386
The elimination rule \isa{less{\isacharunderscore}SucE} expresses the case distinction:
wenzelm@9698
   387
\begin{isabelle}%
nipkow@10696
   388
\ \ \ \ \ {\isasymlbrakk}m\ {\isacharless}\ Suc\ n{\isacharsemicolon}\ m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ m\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P%
wenzelm@9924
   389
\end{isabelle}
wenzelm@9698
   390
wenzelm@9698
   391
Now it is straightforward to derive the original version of
nipkow@11256
   392
\isa{nat{\isacharunderscore}less{\isacharunderscore}induct} by manipulating the conclusion of the above
nipkow@11256
   393
lemma: instantiate \isa{n} by \isa{Suc\ n} and \isa{m} by \isa{n}
nipkow@11256
   394
and remove the trivial condition \isa{n\ {\isacharless}\ Suc\ n}. Fortunately, this
wenzelm@9698
   395
happens automatically when we add the lemma as a new premise to the
wenzelm@9698
   396
desired goal:%
wenzelm@9698
   397
\end{isamarkuptext}%
wenzelm@17175
   398
\isamarkuptrue%
wenzelm@17175
   399
\isacommand{theorem}\isamarkupfalse%
wenzelm@17175
   400
\ nat{\isacharunderscore}less{\isacharunderscore}induct{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymAnd}n{\isacharcolon}{\isacharcolon}nat{\isachardot}\ {\isasymforall}m{\isacharless}n{\isachardot}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n{\isachardoublequoteclose}\isanewline
wenzelm@17056
   401
%
wenzelm@17056
   402
\isadelimproof
wenzelm@17056
   403
%
wenzelm@17056
   404
\endisadelimproof
wenzelm@17056
   405
%
wenzelm@17056
   406
\isatagproof
wenzelm@17175
   407
\isacommand{by}\isamarkupfalse%
wenzelm@17175
   408
{\isacharparenleft}insert\ induct{\isacharunderscore}lem{\isacharcomma}\ blast{\isacharparenright}%
wenzelm@17056
   409
\endisatagproof
wenzelm@17056
   410
{\isafoldproof}%
wenzelm@17056
   411
%
wenzelm@17056
   412
\isadelimproof
wenzelm@17056
   413
%
wenzelm@17056
   414
\endisadelimproof
wenzelm@11866
   415
%
wenzelm@9698
   416
\begin{isamarkuptext}%
paulson@11494
   417
HOL already provides the mother of
nipkow@10396
   418
all inductions, well-founded induction (see \S\ref{sec:Well-founded}).  For
paulson@10878
   419
example theorem \isa{nat{\isacharunderscore}less{\isacharunderscore}induct} is
nipkow@10396
   420
a special case of \isa{wf{\isacharunderscore}induct} where \isa{r} is \isa{{\isacharless}} on
paulson@10878
   421
\isa{nat}. The details can be found in theory \isa{Wellfounded_Recursion}.%
nipkow@9670
   422
\end{isamarkuptext}%
wenzelm@17175
   423
\isamarkuptrue%
wenzelm@17056
   424
%
wenzelm@17056
   425
\isadelimtheory
wenzelm@17056
   426
%
wenzelm@17056
   427
\endisadelimtheory
wenzelm@17056
   428
%
wenzelm@17056
   429
\isatagtheory
wenzelm@17056
   430
%
wenzelm@17056
   431
\endisatagtheory
wenzelm@17056
   432
{\isafoldtheory}%
wenzelm@17056
   433
%
wenzelm@17056
   434
\isadelimtheory
wenzelm@17056
   435
%
wenzelm@17056
   436
\endisadelimtheory
nipkow@9722
   437
\end{isabellebody}%
nipkow@9670
   438
%%% Local Variables:
nipkow@9670
   439
%%% mode: latex
nipkow@9670
   440
%%% TeX-master: "root"
nipkow@9670
   441
%%% End: