doc-src/IsarOverview/Isar/document/Induction.tex
author wenzelm
Tue Oct 16 17:07:40 2007 +0200 (2007-10-16)
changeset 25056 743f3603ba8b
parent 17187 45bee2f6e61f
child 25403 359b179fc963
permissions -rw-r--r--
updated;
kleing@13999
     1
%
kleing@13999
     2
\begin{isabellebody}%
kleing@13999
     3
\def\isabellecontext{Induction}%
wenzelm@17125
     4
%
wenzelm@17125
     5
\isadelimtheory
wenzelm@17125
     6
%
wenzelm@17125
     7
\endisadelimtheory
wenzelm@17125
     8
%
wenzelm@17125
     9
\isatagtheory
wenzelm@17125
    10
%
wenzelm@17125
    11
\endisatagtheory
wenzelm@17125
    12
{\isafoldtheory}%
wenzelm@17125
    13
%
wenzelm@17125
    14
\isadelimtheory
wenzelm@17125
    15
%
wenzelm@17125
    16
\endisadelimtheory
kleing@13999
    17
%
kleing@13999
    18
\isamarkupsection{Case distinction and induction \label{sec:Induct}%
kleing@13999
    19
}
kleing@13999
    20
\isamarkuptrue%
kleing@13999
    21
%
kleing@13999
    22
\begin{isamarkuptext}%
kleing@13999
    23
Computer science applications abound with inductively defined
kleing@13999
    24
structures, which is why we treat them in more detail. HOL already
kleing@13999
    25
comes with a datatype of lists with the two constructors \isa{Nil}
kleing@13999
    26
and \isa{Cons}. \isa{Nil} is written \isa{{\isacharbrackleft}{\isacharbrackright}} and \isa{Cons\ x\ xs} is written \isa{x\ {\isacharhash}\ xs}.%
kleing@13999
    27
\end{isamarkuptext}%
kleing@13999
    28
\isamarkuptrue%
kleing@13999
    29
%
kleing@13999
    30
\isamarkupsubsection{Case distinction\label{sec:CaseDistinction}%
kleing@13999
    31
}
kleing@13999
    32
\isamarkuptrue%
kleing@13999
    33
%
kleing@13999
    34
\begin{isamarkuptext}%
kleing@13999
    35
We have already met the \isa{cases} method for performing
kleing@13999
    36
binary case splits. Here is another example:%
kleing@13999
    37
\end{isamarkuptext}%
wenzelm@17175
    38
\isamarkuptrue%
wenzelm@17175
    39
\isacommand{lemma}\isamarkupfalse%
wenzelm@17175
    40
\ {\isachardoublequoteopen}{\isasymnot}\ A\ {\isasymor}\ A{\isachardoublequoteclose}\isanewline
wenzelm@17125
    41
%
wenzelm@17125
    42
\isadelimproof
wenzelm@17125
    43
%
wenzelm@17125
    44
\endisadelimproof
wenzelm@17125
    45
%
wenzelm@17125
    46
\isatagproof
wenzelm@17175
    47
\isacommand{proof}\isamarkupfalse%
wenzelm@17175
    48
\ cases\isanewline
wenzelm@17175
    49
\ \ \isacommand{assume}\isamarkupfalse%
wenzelm@17175
    50
\ {\isachardoublequoteopen}A{\isachardoublequoteclose}\ \isacommand{thus}\isamarkupfalse%
wenzelm@17175
    51
\ {\isacharquery}thesis\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
wenzelm@17175
    52
\isanewline
wenzelm@17175
    53
\isacommand{next}\isamarkupfalse%
wenzelm@17175
    54
\isanewline
wenzelm@17175
    55
\ \ \isacommand{assume}\isamarkupfalse%
wenzelm@17175
    56
\ {\isachardoublequoteopen}{\isasymnot}\ A{\isachardoublequoteclose}\ \isacommand{thus}\isamarkupfalse%
wenzelm@17175
    57
\ {\isacharquery}thesis\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
wenzelm@17175
    58
\isanewline
wenzelm@17175
    59
\isacommand{qed}\isamarkupfalse%
wenzelm@17175
    60
%
wenzelm@17125
    61
\endisatagproof
wenzelm@17125
    62
{\isafoldproof}%
wenzelm@17125
    63
%
wenzelm@17125
    64
\isadelimproof
wenzelm@17125
    65
%
wenzelm@17125
    66
\endisadelimproof
kleing@13999
    67
%
kleing@13999
    68
\begin{isamarkuptext}%
kleing@13999
    69
\noindent The two cases must come in this order because \isa{cases} merely abbreviates \isa{{\isacharparenleft}rule\ case{\isacharunderscore}split{\isacharunderscore}thm{\isacharparenright}} where
kleing@13999
    70
\isa{case{\isacharunderscore}split{\isacharunderscore}thm} is \isa{{\isasymlbrakk}{\isacharquery}P\ {\isasymLongrightarrow}\ {\isacharquery}Q{\isacharsemicolon}\ {\isasymnot}\ {\isacharquery}P\ {\isasymLongrightarrow}\ {\isacharquery}Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}Q}. If we reverse
kleing@13999
    71
the order of the two cases in the proof, the first case would prove
kleing@13999
    72
\isa{{\isasymnot}\ A\ {\isasymLongrightarrow}\ {\isasymnot}\ A\ {\isasymor}\ A} which would solve the first premise of
kleing@13999
    73
\isa{case{\isacharunderscore}split{\isacharunderscore}thm}, instantiating \isa{{\isacharquery}P} with \isa{{\isasymnot}\ A}, thus making the second premise \isa{{\isasymnot}\ {\isasymnot}\ A\ {\isasymLongrightarrow}\ {\isasymnot}\ A\ {\isasymor}\ A}.
kleing@13999
    74
Therefore the order of subgoals is not always completely arbitrary.
kleing@13999
    75
kleing@13999
    76
The above proof is appropriate if \isa{A} is textually small.
kleing@13999
    77
However, if \isa{A} is large, we do not want to repeat it. This can
kleing@13999
    78
be avoided by the following idiom%
kleing@13999
    79
\end{isamarkuptext}%
wenzelm@17175
    80
\isamarkuptrue%
wenzelm@17175
    81
\isacommand{lemma}\isamarkupfalse%
wenzelm@17175
    82
\ {\isachardoublequoteopen}{\isasymnot}\ A\ {\isasymor}\ A{\isachardoublequoteclose}\isanewline
wenzelm@17125
    83
%
wenzelm@17125
    84
\isadelimproof
wenzelm@17125
    85
%
wenzelm@17125
    86
\endisadelimproof
wenzelm@17125
    87
%
wenzelm@17125
    88
\isatagproof
wenzelm@17175
    89
\isacommand{proof}\isamarkupfalse%
wenzelm@17175
    90
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}A{\isachardoublequoteclose}{\isacharparenright}\isanewline
wenzelm@17175
    91
\ \ \isacommand{case}\isamarkupfalse%
wenzelm@17175
    92
\ True\ \isacommand{thus}\isamarkupfalse%
wenzelm@17175
    93
\ {\isacharquery}thesis\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
wenzelm@17175
    94
\isanewline
wenzelm@17175
    95
\isacommand{next}\isamarkupfalse%
wenzelm@17175
    96
\isanewline
wenzelm@17175
    97
\ \ \isacommand{case}\isamarkupfalse%
wenzelm@17175
    98
\ False\ \isacommand{thus}\isamarkupfalse%
wenzelm@17175
    99
\ {\isacharquery}thesis\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
wenzelm@17175
   100
\isanewline
wenzelm@17175
   101
\isacommand{qed}\isamarkupfalse%
wenzelm@17175
   102
%
wenzelm@17125
   103
\endisatagproof
wenzelm@17125
   104
{\isafoldproof}%
wenzelm@17125
   105
%
wenzelm@17125
   106
\isadelimproof
wenzelm@17125
   107
%
wenzelm@17125
   108
\endisadelimproof
kleing@13999
   109
%
kleing@13999
   110
\begin{isamarkuptext}%
kleing@13999
   111
\noindent which is like the previous proof but instantiates
kleing@13999
   112
\isa{{\isacharquery}P} right away with \isa{A}. Thus we could prove the two
kleing@13999
   113
cases in any order. The phrase `\isakeyword{case}~\isa{True}'
kleing@13999
   114
abbreviates `\isakeyword{assume}~\isa{True{\isacharcolon}\ A}' and analogously for
kleing@13999
   115
\isa{False} and \isa{{\isasymnot}\ A}.
kleing@13999
   116
kleing@13999
   117
The same game can be played with other datatypes, for example lists,
kleing@13999
   118
where \isa{tl} is the tail of a list, and \isa{length} returns a
kleing@13999
   119
natural number (remember: $0-1=0$):%
kleing@13999
   120
\end{isamarkuptext}%
wenzelm@17175
   121
\isamarkuptrue%
wenzelm@17175
   122
\isacommand{lemma}\isamarkupfalse%
wenzelm@17175
   123
\ {\isachardoublequoteopen}length{\isacharparenleft}tl\ xs{\isacharparenright}\ {\isacharequal}\ length\ xs\ {\isacharminus}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
wenzelm@17125
   124
%
wenzelm@17125
   125
\isadelimproof
wenzelm@17125
   126
%
wenzelm@17125
   127
\endisadelimproof
wenzelm@17125
   128
%
wenzelm@17125
   129
\isatagproof
wenzelm@17175
   130
\isacommand{proof}\isamarkupfalse%
wenzelm@17175
   131
\ {\isacharparenleft}cases\ xs{\isacharparenright}\isanewline
wenzelm@17175
   132
\ \ \isacommand{case}\isamarkupfalse%
wenzelm@17175
   133
\ Nil\ \isacommand{thus}\isamarkupfalse%
wenzelm@17175
   134
\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse%
wenzelm@17175
   135
\ simp\isanewline
wenzelm@17175
   136
\isacommand{next}\isamarkupfalse%
wenzelm@17175
   137
\isanewline
wenzelm@17175
   138
\ \ \isacommand{case}\isamarkupfalse%
wenzelm@17175
   139
\ Cons\ \isacommand{thus}\isamarkupfalse%
wenzelm@17175
   140
\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse%
wenzelm@17175
   141
\ simp\isanewline
wenzelm@17175
   142
\isacommand{qed}\isamarkupfalse%
wenzelm@17175
   143
%
wenzelm@17125
   144
\endisatagproof
wenzelm@17125
   145
{\isafoldproof}%
wenzelm@17125
   146
%
wenzelm@17125
   147
\isadelimproof
wenzelm@17125
   148
%
wenzelm@17125
   149
\endisadelimproof
kleing@13999
   150
%
kleing@13999
   151
\begin{isamarkuptext}%
kleing@13999
   152
\noindent Here `\isakeyword{case}~\isa{Nil}' abbreviates
kleing@13999
   153
`\isakeyword{assume}~\isa{Nil{\isacharcolon}}~\isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}}' and
kleing@13999
   154
`\isakeyword{case}~\isa{Cons}'
kleing@13999
   155
abbreviates `\isakeyword{fix}~\isa{{\isacharquery}\ {\isacharquery}{\isacharquery}}
kleing@13999
   156
\isakeyword{assume}~\isa{Cons{\isacharcolon}}~\isa{xs\ {\isacharequal}\ {\isacharquery}\ {\isacharhash}\ {\isacharquery}{\isacharquery}}'
kleing@13999
   157
where \isa{{\isacharquery}} and \isa{{\isacharquery}{\isacharquery}}
kleing@13999
   158
stand for variable names that have been chosen by the system.
kleing@13999
   159
Therefore we cannot refer to them.
kleing@13999
   160
Luckily, this proof is simple enough we do not need to refer to them.
kleing@13999
   161
However, sometimes one may have to. Hence Isar offers a simple scheme for
kleing@13999
   162
naming those variables: replace the anonymous \isa{Cons} by
kleing@13999
   163
\isa{{\isacharparenleft}Cons\ y\ ys{\isacharparenright}}, which abbreviates `\isakeyword{fix}~\isa{y\ ys}
kleing@13999
   164
\isakeyword{assume}~\isa{Cons{\isacharcolon}}~\isa{xs\ {\isacharequal}\ y\ {\isacharhash}\ ys}'.
kleing@13999
   165
In each \isakeyword{case} the assumption can be
kleing@13999
   166
referred to inside the proof by the name of the constructor. In
kleing@13999
   167
Section~\ref{sec:full-Ind} below we will come across an example
kleing@13999
   168
of this.%
kleing@13999
   169
\end{isamarkuptext}%
kleing@13999
   170
\isamarkuptrue%
kleing@13999
   171
%
kleing@13999
   172
\isamarkupsubsection{Structural induction%
kleing@13999
   173
}
kleing@13999
   174
\isamarkuptrue%
kleing@13999
   175
%
kleing@13999
   176
\begin{isamarkuptext}%
kleing@13999
   177
We start with an inductive proof where both cases are proved automatically:%
kleing@13999
   178
\end{isamarkuptext}%
wenzelm@17175
   179
\isamarkuptrue%
wenzelm@17175
   180
\isacommand{lemma}\isamarkupfalse%
wenzelm@17175
   181
\ {\isachardoublequoteopen}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharcolon}{\isacharcolon}nat{\isasymle}n{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
wenzelm@17125
   182
%
wenzelm@17125
   183
\isadelimproof
wenzelm@17125
   184
%
wenzelm@17125
   185
\endisadelimproof
wenzelm@17125
   186
%
wenzelm@17125
   187
\isatagproof
wenzelm@17175
   188
\isacommand{by}\isamarkupfalse%
wenzelm@17175
   189
\ {\isacharparenleft}induct\ n{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
wenzelm@17125
   190
\endisatagproof
wenzelm@17125
   191
{\isafoldproof}%
wenzelm@17125
   192
%
wenzelm@17125
   193
\isadelimproof
wenzelm@17125
   194
%
wenzelm@17125
   195
\endisadelimproof
kleing@13999
   196
%
kleing@13999
   197
\begin{isamarkuptext}%
nipkow@15909
   198
\noindent The constraint \isa{{\isacharcolon}{\isacharcolon}nat} is needed because all of
nipkow@15909
   199
the operations involved are overloaded.
nipkow@15909
   200
nipkow@15909
   201
If we want to expose more of the structure of the
kleing@13999
   202
proof, we can use pattern matching to avoid having to repeat the goal
kleing@13999
   203
statement:%
kleing@13999
   204
\end{isamarkuptext}%
wenzelm@17175
   205
\isamarkuptrue%
wenzelm@17175
   206
\isacommand{lemma}\isamarkupfalse%
wenzelm@17175
   207
\ {\isachardoublequoteopen}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharcolon}{\isacharcolon}nat{\isasymle}n{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequoteopen}{\isacharquery}P\ n{\isachardoublequoteclose}{\isacharparenright}\isanewline
wenzelm@17125
   208
%
wenzelm@17125
   209
\isadelimproof
wenzelm@17125
   210
%
wenzelm@17125
   211
\endisadelimproof
wenzelm@17125
   212
%
wenzelm@17125
   213
\isatagproof
wenzelm@17175
   214
\isacommand{proof}\isamarkupfalse%
wenzelm@17175
   215
\ {\isacharparenleft}induct\ n{\isacharparenright}\isanewline
wenzelm@17175
   216
\ \ \isacommand{show}\isamarkupfalse%
wenzelm@17175
   217
\ {\isachardoublequoteopen}{\isacharquery}P\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
wenzelm@17175
   218
\ simp\isanewline
wenzelm@17175
   219
\isacommand{next}\isamarkupfalse%
wenzelm@17175
   220
\isanewline
wenzelm@17175
   221
\ \ \isacommand{fix}\isamarkupfalse%
wenzelm@17175
   222
\ n\ \isacommand{assume}\isamarkupfalse%
wenzelm@17175
   223
\ {\isachardoublequoteopen}{\isacharquery}P\ n{\isachardoublequoteclose}\isanewline
wenzelm@17175
   224
\ \ \isacommand{thus}\isamarkupfalse%
wenzelm@17175
   225
\ {\isachardoublequoteopen}{\isacharquery}P{\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
wenzelm@17175
   226
\ simp\isanewline
wenzelm@17175
   227
\isacommand{qed}\isamarkupfalse%
wenzelm@17175
   228
%
wenzelm@17125
   229
\endisatagproof
wenzelm@17125
   230
{\isafoldproof}%
wenzelm@17125
   231
%
wenzelm@17125
   232
\isadelimproof
wenzelm@17125
   233
%
wenzelm@17125
   234
\endisadelimproof
kleing@13999
   235
%
kleing@13999
   236
\begin{isamarkuptext}%
kleing@13999
   237
\noindent We could refine this further to show more of the equational
kleing@13999
   238
proof. Instead we explore the same avenue as for case distinctions:
kleing@13999
   239
introducing context via the \isakeyword{case} command:%
kleing@13999
   240
\end{isamarkuptext}%
wenzelm@17175
   241
\isamarkuptrue%
wenzelm@17175
   242
\isacommand{lemma}\isamarkupfalse%
wenzelm@17175
   243
\ {\isachardoublequoteopen}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharcolon}{\isacharcolon}nat\ {\isasymle}\ n{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
wenzelm@17125
   244
%
wenzelm@17125
   245
\isadelimproof
wenzelm@17125
   246
%
wenzelm@17125
   247
\endisadelimproof
wenzelm@17125
   248
%
wenzelm@17125
   249
\isatagproof
wenzelm@17175
   250
\isacommand{proof}\isamarkupfalse%
wenzelm@17175
   251
\ {\isacharparenleft}induct\ n{\isacharparenright}\isanewline
wenzelm@17175
   252
\ \ \isacommand{case}\isamarkupfalse%
wenzelm@17175
   253
\ {\isadigit{0}}\ \isacommand{show}\isamarkupfalse%
wenzelm@17175
   254
\ {\isacharquery}case\ \isacommand{by}\isamarkupfalse%
wenzelm@17175
   255
\ simp\isanewline
wenzelm@17175
   256
\isacommand{next}\isamarkupfalse%
wenzelm@17175
   257
\isanewline
wenzelm@17175
   258
\ \ \isacommand{case}\isamarkupfalse%
wenzelm@17175
   259
\ Suc\ \isacommand{thus}\isamarkupfalse%
wenzelm@17175
   260
\ {\isacharquery}case\ \isacommand{by}\isamarkupfalse%
wenzelm@17175
   261
\ simp\isanewline
wenzelm@17175
   262
\isacommand{qed}\isamarkupfalse%
wenzelm@17175
   263
%
wenzelm@17125
   264
\endisatagproof
wenzelm@17125
   265
{\isafoldproof}%
wenzelm@17125
   266
%
wenzelm@17125
   267
\isadelimproof
wenzelm@17125
   268
%
wenzelm@17125
   269
\endisadelimproof
kleing@13999
   270
%
kleing@13999
   271
\begin{isamarkuptext}%
kleing@13999
   272
\noindent The implicitly defined \isa{{\isacharquery}case} refers to the
kleing@13999
   273
corresponding case to be proved, i.e.\ \isa{{\isacharquery}P\ {\isadigit{0}}} in the first case and
kleing@13999
   274
\isa{{\isacharquery}P{\isacharparenleft}Suc\ n{\isacharparenright}} in the second case. Context \isakeyword{case}~\isa{{\isadigit{0}}} is
kleing@13999
   275
empty whereas \isakeyword{case}~\isa{Suc} assumes \isa{{\isacharquery}P\ n}. Again we
kleing@13999
   276
have the same problem as with case distinctions: we cannot refer to an anonymous \isa{n}
kleing@13999
   277
in the induction step because it has not been introduced via \isakeyword{fix}
kleing@13999
   278
(in contrast to the previous proof). The solution is the one outlined for
kleing@13999
   279
\isa{Cons} above: replace \isa{Suc} by \isa{{\isacharparenleft}Suc\ i{\isacharparenright}}:%
kleing@13999
   280
\end{isamarkuptext}%
wenzelm@17175
   281
\isamarkuptrue%
wenzelm@17175
   282
\isacommand{lemma}\isamarkupfalse%
wenzelm@17175
   283
\ \isakeyword{fixes}\ n{\isacharcolon}{\isacharcolon}nat\ \isakeyword{shows}\ {\isachardoublequoteopen}n\ {\isacharless}\ n{\isacharasterisk}n\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
wenzelm@17125
   284
%
wenzelm@17125
   285
\isadelimproof
wenzelm@17125
   286
%
wenzelm@17125
   287
\endisadelimproof
wenzelm@17125
   288
%
wenzelm@17125
   289
\isatagproof
wenzelm@17175
   290
\isacommand{proof}\isamarkupfalse%
wenzelm@17175
   291
\ {\isacharparenleft}induct\ n{\isacharparenright}\isanewline
wenzelm@17175
   292
\ \ \isacommand{case}\isamarkupfalse%
wenzelm@17175
   293
\ {\isadigit{0}}\ \isacommand{show}\isamarkupfalse%
wenzelm@17175
   294
\ {\isacharquery}case\ \isacommand{by}\isamarkupfalse%
wenzelm@17175
   295
\ simp\isanewline
wenzelm@17175
   296
\isacommand{next}\isamarkupfalse%
wenzelm@17175
   297
\isanewline
wenzelm@17175
   298
\ \ \isacommand{case}\isamarkupfalse%
wenzelm@17175
   299
\ {\isacharparenleft}Suc\ i{\isacharparenright}\ \isacommand{thus}\isamarkupfalse%
wenzelm@17175
   300
\ {\isachardoublequoteopen}Suc\ i\ {\isacharless}\ Suc\ i\ {\isacharasterisk}\ Suc\ i\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
wenzelm@17175
   301
\ simp\isanewline
wenzelm@17175
   302
\isacommand{qed}\isamarkupfalse%
wenzelm@17175
   303
%
wenzelm@17125
   304
\endisatagproof
wenzelm@17125
   305
{\isafoldproof}%
wenzelm@17125
   306
%
wenzelm@17125
   307
\isadelimproof
wenzelm@17125
   308
%
wenzelm@17125
   309
\endisadelimproof
kleing@13999
   310
%
kleing@13999
   311
\begin{isamarkuptext}%
kleing@13999
   312
\noindent Of course we could again have written
kleing@13999
   313
\isakeyword{thus}~\isa{{\isacharquery}case} instead of giving the term explicitly
kleing@13999
   314
but we wanted to use \isa{i} somewhere.%
kleing@13999
   315
\end{isamarkuptext}%
kleing@13999
   316
\isamarkuptrue%
kleing@13999
   317
%
kleing@13999
   318
\isamarkupsubsection{Induction formulae involving \isa{{\isasymAnd}} or \isa{{\isasymLongrightarrow}}\label{sec:full-Ind}%
kleing@13999
   319
}
kleing@13999
   320
\isamarkuptrue%
kleing@13999
   321
%
kleing@13999
   322
\begin{isamarkuptext}%
kleing@13999
   323
Let us now consider the situation where the goal to be proved contains
kleing@13999
   324
\isa{{\isasymAnd}} or \isa{{\isasymLongrightarrow}}, say \isa{{\isasymAnd}x{\isachardot}\ P\ x\ {\isasymLongrightarrow}\ Q\ x} --- motivation and a
kleing@13999
   325
real example follow shortly.  This means that in each case of the induction,
kleing@13999
   326
\isa{{\isacharquery}case} would be of the form \isa{{\isasymAnd}x{\isachardot}\ P{\isacharprime}\ x\ {\isasymLongrightarrow}\ Q{\isacharprime}\ x}.  Thus the
kleing@13999
   327
first proof steps will be the canonical ones, fixing \isa{x} and assuming
kleing@13999
   328
\isa{P{\isacharprime}\ x}. To avoid this tedium, induction performs these steps
kleing@13999
   329
automatically: for example in case \isa{{\isacharparenleft}Suc\ n{\isacharparenright}}, \isa{{\isacharquery}case} is only
kleing@13999
   330
\isa{Q{\isacharprime}\ x} whereas the assumptions (named \isa{Suc}!) contain both the
kleing@13999
   331
usual induction hypothesis \emph{and} \isa{P{\isacharprime}\ x}.
kleing@13999
   332
It should be clear how this generalises to more complex formulae.
kleing@13999
   333
kleing@13999
   334
As an example we will now prove complete induction via
kleing@13999
   335
structural induction.%
kleing@13999
   336
\end{isamarkuptext}%
wenzelm@17175
   337
\isamarkuptrue%
wenzelm@17175
   338
\isacommand{lemma}\isamarkupfalse%
wenzelm@17175
   339
\ \isakeyword{assumes}\ A{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymAnd}n{\isachardot}\ {\isacharparenleft}{\isasymAnd}m{\isachardot}\ m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P\ m{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
wenzelm@17175
   340
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}P{\isacharparenleft}n{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
wenzelm@17125
   341
%
wenzelm@17125
   342
\isadelimproof
wenzelm@17125
   343
%
wenzelm@17125
   344
\endisadelimproof
wenzelm@17125
   345
%
wenzelm@17125
   346
\isatagproof
wenzelm@17175
   347
\isacommand{proof}\isamarkupfalse%
wenzelm@17175
   348
\ {\isacharparenleft}rule\ A{\isacharparenright}\isanewline
wenzelm@17175
   349
\ \ \isacommand{show}\isamarkupfalse%
wenzelm@17175
   350
\ {\isachardoublequoteopen}{\isasymAnd}m{\isachardot}\ m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P\ m{\isachardoublequoteclose}\isanewline
wenzelm@17175
   351
\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@17175
   352
\ {\isacharparenleft}induct\ n{\isacharparenright}\isanewline
wenzelm@17175
   353
\ \ \ \ \isacommand{case}\isamarkupfalse%
wenzelm@17175
   354
\ {\isadigit{0}}\ \isacommand{thus}\isamarkupfalse%
wenzelm@17175
   355
\ {\isacharquery}case\ \isacommand{by}\isamarkupfalse%
wenzelm@17175
   356
\ simp\isanewline
wenzelm@17175
   357
\ \ \isacommand{next}\isamarkupfalse%
wenzelm@17175
   358
\isanewline
wenzelm@17175
   359
\ \ \ \ \isacommand{case}\isamarkupfalse%
wenzelm@17175
   360
\ {\isacharparenleft}Suc\ n{\isacharparenright}\ \ \ %
wenzelm@16459
   361
\isamarkupcmt{\isakeyword{fix} \isa{m} \isakeyword{assume} \isa{Suc}: \isa{{\isachardoublequote}{\isacharquery}m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P\ {\isacharquery}m{\isachardoublequote}} \isa{{\isachardoublequote}m\ {\isacharless}\ Suc\ n{\isachardoublequote}}%
wenzelm@16459
   362
}
wenzelm@16459
   363
\isanewline
wenzelm@17175
   364
\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@17175
   365
\ {\isacharquery}case\ \ \ \ %
wenzelm@16459
   366
\isamarkupcmt{\isa{P\ m}%
wenzelm@16459
   367
}
wenzelm@16459
   368
\isanewline
wenzelm@17175
   369
\ \ \ \ \isacommand{proof}\isamarkupfalse%
wenzelm@17175
   370
\ cases\isanewline
wenzelm@17175
   371
\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@17175
   372
\ eq{\isacharcolon}\ {\isachardoublequoteopen}m\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
wenzelm@17175
   373
\ \ \ \ \ \ \isacommand{from}\isamarkupfalse%
wenzelm@17175
   374
\ Suc\ \isakeyword{and}\ A\ \isacommand{have}\isamarkupfalse%
wenzelm@17175
   375
\ {\isachardoublequoteopen}P\ n{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
wenzelm@17175
   376
\ blast\isanewline
wenzelm@17175
   377
\ \ \ \ \ \ \isacommand{with}\isamarkupfalse%
wenzelm@17175
   378
\ eq\ \isacommand{show}\isamarkupfalse%
wenzelm@17175
   379
\ {\isachardoublequoteopen}P\ m{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
wenzelm@17175
   380
\ simp\isanewline
wenzelm@17175
   381
\ \ \ \ \isacommand{next}\isamarkupfalse%
wenzelm@17175
   382
\isanewline
wenzelm@17175
   383
\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@17175
   384
\ {\isachardoublequoteopen}m\ {\isasymnoteq}\ n{\isachardoublequoteclose}\isanewline
wenzelm@17175
   385
\ \ \ \ \ \ \isacommand{with}\isamarkupfalse%
wenzelm@17175
   386
\ Suc\ \isacommand{have}\isamarkupfalse%
wenzelm@17175
   387
\ {\isachardoublequoteopen}m\ {\isacharless}\ n{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
wenzelm@17175
   388
\ arith\isanewline
wenzelm@17175
   389
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
wenzelm@17175
   390
\ {\isachardoublequoteopen}P\ m{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
wenzelm@17175
   391
{\isacharparenleft}rule\ Suc{\isacharparenright}\isanewline
wenzelm@17175
   392
\ \ \ \ \isacommand{qed}\isamarkupfalse%
wenzelm@17175
   393
\isanewline
wenzelm@17175
   394
\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@17175
   395
\isanewline
wenzelm@17175
   396
\isacommand{qed}\isamarkupfalse%
wenzelm@17175
   397
%
wenzelm@17125
   398
\endisatagproof
wenzelm@17125
   399
{\isafoldproof}%
wenzelm@17125
   400
%
wenzelm@17125
   401
\isadelimproof
wenzelm@17125
   402
%
wenzelm@17125
   403
\endisadelimproof
kleing@13999
   404
%
kleing@13999
   405
\begin{isamarkuptext}%
kleing@13999
   406
\noindent Given the explanations above and the comments in the
kleing@13999
   407
proof text (only necessary for novices), the proof should be quite
kleing@13999
   408
readable.
kleing@13999
   409
kleing@13999
   410
The statement of the lemma is interesting because it deviates from the style in
kleing@13999
   411
the Tutorial~\cite{LNCS2283}, which suggests to introduce \isa{{\isasymforall}} or
kleing@13999
   412
\isa{{\isasymlongrightarrow}} into a theorem to strengthen it for induction. In Isar
kleing@13999
   413
proofs we can use \isa{{\isasymAnd}} and \isa{{\isasymLongrightarrow}} instead. This simplifies the
kleing@13999
   414
proof and means we do not have to convert between the two kinds of
kleing@13999
   415
connectives.
kleing@13999
   416
kleing@13999
   417
Note that in a nested induction over the same data type, the inner
kleing@13999
   418
case labels hide the outer ones of the same name. If you want to refer
kleing@13999
   419
to the outer ones inside, you need to name them on the outside, e.g.\
kleing@13999
   420
\isakeyword{note}~\isa{outer{\isacharunderscore}IH\ {\isacharequal}\ Suc}.%
kleing@13999
   421
\end{isamarkuptext}%
kleing@13999
   422
\isamarkuptrue%
kleing@13999
   423
%
kleing@13999
   424
\isamarkupsubsection{Rule induction%
kleing@13999
   425
}
kleing@13999
   426
\isamarkuptrue%
kleing@13999
   427
%
kleing@13999
   428
\begin{isamarkuptext}%
kleing@13999
   429
HOL also supports inductively defined sets. See \cite{LNCS2283}
kleing@13999
   430
for details. As an example we define our own version of the reflexive
kleing@13999
   431
transitive closure of a relation --- HOL provides a predefined one as well.%
kleing@13999
   432
\end{isamarkuptext}%
wenzelm@17175
   433
\isamarkuptrue%
wenzelm@25056
   434
\isacommand{inductive{\isacharunderscore}set}\isamarkupfalse%
wenzelm@25056
   435
\isanewline
wenzelm@25056
   436
\ \ rtc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequoteclose}\ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharunderscore}{\isacharasterisk}{\isachardoublequoteclose}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline
wenzelm@25056
   437
\ \ \isakeyword{for}\ r\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequoteclose}\isanewline
wenzelm@25056
   438
\isakeyword{where}\isanewline
wenzelm@25056
   439
\ \ refl{\isacharcolon}\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\isanewline
wenzelm@25056
   440
{\isacharbar}\ step{\isacharcolon}\ \ {\isachardoublequoteopen}{\isasymlbrakk}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}%
kleing@13999
   441
\begin{isamarkuptext}%
kleing@13999
   442
\noindent
kleing@13999
   443
First the constant is declared as a function on binary
kleing@13999
   444
relations (with concrete syntax \isa{r{\isacharasterisk}} instead of \isa{rtc\ r}), then the defining clauses are given. We will now prove that
kleing@13999
   445
\isa{r{\isacharasterisk}} is indeed transitive:%
kleing@13999
   446
\end{isamarkuptext}%
wenzelm@17175
   447
\isamarkuptrue%
wenzelm@17175
   448
\isacommand{lemma}\isamarkupfalse%
wenzelm@17175
   449
\ \isakeyword{assumes}\ A{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\isanewline
wenzelm@17125
   450
%
wenzelm@17125
   451
\isadelimproof
wenzelm@17125
   452
%
wenzelm@17125
   453
\endisadelimproof
wenzelm@17125
   454
%
wenzelm@17125
   455
\isatagproof
wenzelm@17175
   456
\isacommand{using}\isamarkupfalse%
wenzelm@17175
   457
\ A\isanewline
wenzelm@17175
   458
\isacommand{proof}\isamarkupfalse%
wenzelm@17175
   459
\ induct\isanewline
wenzelm@17175
   460
\ \ \isacommand{case}\isamarkupfalse%
wenzelm@17175
   461
\ refl\ \isacommand{thus}\isamarkupfalse%
wenzelm@17175
   462
\ {\isacharquery}case\ \isacommand{{\isachardot}}\isamarkupfalse%
wenzelm@17175
   463
\isanewline
wenzelm@17175
   464
\isacommand{next}\isamarkupfalse%
wenzelm@17175
   465
\isanewline
wenzelm@17175
   466
\ \ \isacommand{case}\isamarkupfalse%
wenzelm@17175
   467
\ step\ \isacommand{thus}\isamarkupfalse%
wenzelm@17175
   468
\ {\isacharquery}case\ \isacommand{by}\isamarkupfalse%
wenzelm@17175
   469
{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isachardot}step{\isacharparenright}\isanewline
wenzelm@17175
   470
\isacommand{qed}\isamarkupfalse%
wenzelm@17175
   471
%
wenzelm@17125
   472
\endisatagproof
wenzelm@17125
   473
{\isafoldproof}%
wenzelm@17125
   474
%
wenzelm@17125
   475
\isadelimproof
wenzelm@17125
   476
%
wenzelm@17125
   477
\endisadelimproof
kleing@13999
   478
%
kleing@13999
   479
\begin{isamarkuptext}%
kleing@13999
   480
\noindent Rule induction is triggered by a fact $(x_1,\dots,x_n)
kleing@13999
   481
\in R$ piped into the proof, here \isakeyword{using}~\isa{A}. The
kleing@13999
   482
proof itself follows the inductive definition very
kleing@13999
   483
closely: there is one case for each rule, and it has the same name as
kleing@13999
   484
the rule, analogous to structural induction.
kleing@13999
   485
kleing@13999
   486
However, this proof is rather terse. Here is a more readable version:%
kleing@13999
   487
\end{isamarkuptext}%
wenzelm@17175
   488
\isamarkuptrue%
wenzelm@17175
   489
\isacommand{lemma}\isamarkupfalse%
wenzelm@17175
   490
\ \isakeyword{assumes}\ A{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\ \isakeyword{and}\ B{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\isanewline
wenzelm@17175
   491
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\isanewline
wenzelm@17125
   492
%
wenzelm@17125
   493
\isadelimproof
wenzelm@17125
   494
%
wenzelm@17125
   495
\endisadelimproof
wenzelm@17125
   496
%
wenzelm@17125
   497
\isatagproof
wenzelm@17175
   498
\isacommand{proof}\isamarkupfalse%
wenzelm@17175
   499
\ {\isacharminus}\isanewline
wenzelm@17175
   500
\ \ \isacommand{from}\isamarkupfalse%
wenzelm@17175
   501
\ A\ B\ \isacommand{show}\isamarkupfalse%
wenzelm@17175
   502
\ {\isacharquery}thesis\isanewline
wenzelm@17175
   503
\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@17175
   504
\ induct\isanewline
wenzelm@17175
   505
\ \ \ \ \isacommand{fix}\isamarkupfalse%
wenzelm@17175
   506
\ x\ \isacommand{assume}\isamarkupfalse%
wenzelm@17175
   507
\ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\ \ %
wenzelm@16459
   508
\isamarkupcmt{\isa{B}[\isa{y} := \isa{x}]%
wenzelm@16459
   509
}
wenzelm@16459
   510
\isanewline
wenzelm@17175
   511
\ \ \ \ \isacommand{thus}\isamarkupfalse%
wenzelm@17175
   512
\ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
wenzelm@17175
   513
\isanewline
wenzelm@17175
   514
\ \ \isacommand{next}\isamarkupfalse%
wenzelm@17175
   515
\isanewline
wenzelm@17175
   516
\ \ \ \ \isacommand{fix}\isamarkupfalse%
wenzelm@17175
   517
\ x{\isacharprime}\ x\ y\isanewline
wenzelm@17175
   518
\ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@17175
   519
\ {\isadigit{1}}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharprime}{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ r{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
wenzelm@17175
   520
\ \ \ \ \ \ \ \ \ \ \ IH{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
wenzelm@17175
   521
\ \ \ \ \ \ \ \ \ \ \ B{\isacharcolon}\ \ {\isachardoublequoteopen}{\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\isanewline
wenzelm@17175
   522
\ \ \ \ \isacommand{from}\isamarkupfalse%
wenzelm@17175
   523
\ {\isadigit{1}}\ IH{\isacharbrackleft}OF\ B{\isacharbrackright}\ \isacommand{show}\isamarkupfalse%
wenzelm@17175
   524
\ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharprime}{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
wenzelm@17175
   525
{\isacharparenleft}rule\ rtc{\isachardot}step{\isacharparenright}\isanewline
wenzelm@17175
   526
\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@17175
   527
\isanewline
wenzelm@17175
   528
\isacommand{qed}\isamarkupfalse%
wenzelm@17175
   529
%
wenzelm@17125
   530
\endisatagproof
wenzelm@17125
   531
{\isafoldproof}%
wenzelm@17125
   532
%
wenzelm@17125
   533
\isadelimproof
wenzelm@17125
   534
%
wenzelm@17125
   535
\endisadelimproof
kleing@13999
   536
%
kleing@13999
   537
\begin{isamarkuptext}%
kleing@13999
   538
\noindent We start the proof with \isakeyword{from}~\isa{A\ B}. Only \isa{A} is ``consumed'' by the induction step.
kleing@13999
   539
Since \isa{B} is left over we don't just prove \isa{{\isacharquery}thesis} but \isa{B\ {\isasymLongrightarrow}\ {\isacharquery}thesis}, just as in the previous proof. The
kleing@13999
   540
base case is trivial. In the assumptions for the induction step we can
kleing@13999
   541
see very clearly how things fit together and permit ourselves the
kleing@13999
   542
obvious forward step \isa{IH{\isacharbrackleft}OF\ B{\isacharbrackright}}.
kleing@13999
   543
kleing@13999
   544
The notation `\isakeyword{case}~\isa{(}\emph{constructor} \emph{vars}\isa{)}'
kleing@13999
   545
is also supported for inductive definitions. The \emph{constructor} is (the
kleing@13999
   546
name of) the rule and the \emph{vars} fix the free variables in the
kleing@13999
   547
rule; the order of the \emph{vars} must correspond to the
kleing@13999
   548
\emph{alphabetical order} of the variables as they appear in the rule.
kleing@13999
   549
For example, we could start the above detailed proof of the induction
kleing@13999
   550
with \isakeyword{case}~\isa{(step x' x y)}. However, we can then only
kleing@13999
   551
refer to the assumptions named \isa{step} collectively and not
kleing@13999
   552
individually, as the above proof requires.%
kleing@13999
   553
\end{isamarkuptext}%
kleing@13999
   554
\isamarkuptrue%
kleing@13999
   555
%
kleing@13999
   556
\isamarkupsubsection{More induction%
kleing@13999
   557
}
kleing@13999
   558
\isamarkuptrue%
kleing@13999
   559
%
kleing@13999
   560
\begin{isamarkuptext}%
kleing@13999
   561
We close the section by demonstrating how arbitrary induction
kleing@13999
   562
rules are applied. As a simple example we have chosen recursion
kleing@13999
   563
induction, i.e.\ induction based on a recursive function
kleing@13999
   564
definition. However, most of what we show works for induction in
kleing@13999
   565
general.
kleing@13999
   566
kleing@13999
   567
The example is an unusual definition of rotation:%
kleing@13999
   568
\end{isamarkuptext}%
wenzelm@17175
   569
\isamarkuptrue%
wenzelm@17175
   570
\isacommand{consts}\isamarkupfalse%
wenzelm@17175
   571
\ rot\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\isanewline
wenzelm@17175
   572
\isacommand{recdef}\isamarkupfalse%
wenzelm@17175
   573
\ rot\ {\isachardoublequoteopen}measure\ length{\isachardoublequoteclose}\ \ %
kleing@13999
   574
\isamarkupcmt{for the internal termination proof%
kleing@13999
   575
}
kleing@13999
   576
\isanewline
wenzelm@17175
   577
{\isachardoublequoteopen}rot\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
wenzelm@17175
   578
{\isachardoublequoteopen}rot\ {\isacharbrackleft}x{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}x{\isacharbrackright}{\isachardoublequoteclose}\isanewline
wenzelm@17175
   579
{\isachardoublequoteopen}rot\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ y\ {\isacharhash}\ rot{\isacharparenleft}x{\isacharhash}zs{\isacharparenright}{\isachardoublequoteclose}%
kleing@13999
   580
\begin{isamarkuptext}%
kleing@13999
   581
\noindent This yields, among other things, the induction rule
kleing@13999
   582
\isa{rot{\isachardot}induct}: \begin{isabelle}%
kleing@13999
   583
{\isasymlbrakk}P\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ P\ {\isacharbrackleft}x{\isacharbrackright}{\isacharsemicolon}\ {\isasymAnd}x\ y\ zs{\isachardot}\ P\ {\isacharparenleft}x\ {\isacharhash}\ zs{\isacharparenright}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}x\ {\isacharhash}\ y\ {\isacharhash}\ zs{\isacharparenright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ x%
kleing@13999
   584
\end{isabelle}
kleing@13999
   585
In the following proof we rely on a default naming scheme for cases: they are
kleing@13999
   586
called 1, 2, etc, unless they have been named explicitly. The latter happens
kleing@13999
   587
only with datatypes and inductively defined sets, but not with recursive
kleing@13999
   588
functions.%
kleing@13999
   589
\end{isamarkuptext}%
wenzelm@17175
   590
\isamarkuptrue%
wenzelm@17175
   591
\isacommand{lemma}\isamarkupfalse%
wenzelm@17175
   592
\ {\isachardoublequoteopen}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ rot\ xs\ {\isacharequal}\ tl\ xs\ {\isacharat}\ {\isacharbrackleft}hd\ xs{\isacharbrackright}{\isachardoublequoteclose}\isanewline
wenzelm@17125
   593
%
wenzelm@17125
   594
\isadelimproof
wenzelm@17125
   595
%
wenzelm@17125
   596
\endisadelimproof
wenzelm@17125
   597
%
wenzelm@17125
   598
\isatagproof
wenzelm@17175
   599
\isacommand{proof}\isamarkupfalse%
wenzelm@17175
   600
\ {\isacharparenleft}induct\ xs\ rule{\isacharcolon}\ rot{\isachardot}induct{\isacharparenright}\isanewline
wenzelm@17175
   601
\ \ \isacommand{case}\isamarkupfalse%
wenzelm@17175
   602
\ {\isadigit{1}}\ \isacommand{thus}\isamarkupfalse%
wenzelm@17175
   603
\ {\isacharquery}case\ \isacommand{by}\isamarkupfalse%
wenzelm@17175
   604
\ simp\isanewline
wenzelm@17175
   605
\isacommand{next}\isamarkupfalse%
wenzelm@17175
   606
\isanewline
wenzelm@17175
   607
\ \ \isacommand{case}\isamarkupfalse%
wenzelm@17175
   608
\ {\isadigit{2}}\ \isacommand{show}\isamarkupfalse%
wenzelm@17175
   609
\ {\isacharquery}case\ \isacommand{by}\isamarkupfalse%
wenzelm@17175
   610
\ simp\isanewline
wenzelm@17175
   611
\isacommand{next}\isamarkupfalse%
wenzelm@17175
   612
\isanewline
wenzelm@17175
   613
\ \ \isacommand{case}\isamarkupfalse%
wenzelm@17175
   614
\ {\isacharparenleft}{\isadigit{3}}\ a\ b\ cs{\isacharparenright}\isanewline
wenzelm@17175
   615
\ \ \isacommand{have}\isamarkupfalse%
wenzelm@17175
   616
\ {\isachardoublequoteopen}rot\ {\isacharparenleft}a\ {\isacharhash}\ b\ {\isacharhash}\ cs{\isacharparenright}\ {\isacharequal}\ b\ {\isacharhash}\ rot{\isacharparenleft}a\ {\isacharhash}\ cs{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
wenzelm@17175
   617
\ simp\isanewline
wenzelm@17175
   618
\ \ \isacommand{also}\isamarkupfalse%
wenzelm@17175
   619
\ \isacommand{have}\isamarkupfalse%
wenzelm@17175
   620
\ {\isachardoublequoteopen}{\isasymdots}\ {\isacharequal}\ b\ {\isacharhash}\ tl{\isacharparenleft}a\ {\isacharhash}\ cs{\isacharparenright}\ {\isacharat}\ {\isacharbrackleft}hd{\isacharparenleft}a\ {\isacharhash}\ cs{\isacharparenright}{\isacharbrackright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
wenzelm@17175
   621
{\isacharparenleft}simp\ add{\isacharcolon}{\isadigit{3}}{\isacharparenright}\isanewline
wenzelm@17175
   622
\ \ \isacommand{also}\isamarkupfalse%
wenzelm@17175
   623
\ \isacommand{have}\isamarkupfalse%
wenzelm@17175
   624
\ {\isachardoublequoteopen}{\isasymdots}\ {\isacharequal}\ tl\ {\isacharparenleft}a\ {\isacharhash}\ b\ {\isacharhash}\ cs{\isacharparenright}\ {\isacharat}\ {\isacharbrackleft}hd\ {\isacharparenleft}a\ {\isacharhash}\ b\ {\isacharhash}\ cs{\isacharparenright}{\isacharbrackright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
wenzelm@17175
   625
\ simp\isanewline
wenzelm@17175
   626
\ \ \isacommand{finally}\isamarkupfalse%
wenzelm@17175
   627
\ \isacommand{show}\isamarkupfalse%
wenzelm@17175
   628
\ {\isacharquery}case\ \isacommand{{\isachardot}}\isamarkupfalse%
wenzelm@17175
   629
\isanewline
wenzelm@17175
   630
\isacommand{qed}\isamarkupfalse%
wenzelm@17175
   631
%
wenzelm@17125
   632
\endisatagproof
wenzelm@17125
   633
{\isafoldproof}%
wenzelm@17125
   634
%
wenzelm@17125
   635
\isadelimproof
wenzelm@17125
   636
%
wenzelm@17125
   637
\endisadelimproof
kleing@13999
   638
%
kleing@13999
   639
\begin{isamarkuptext}%
kleing@13999
   640
\noindent
kleing@13999
   641
The third case is only shown in gory detail (see \cite{BauerW-TPHOLs01}
kleing@13999
   642
for how to reason with chains of equations) to demonstrate that the
kleing@13999
   643
`\isakeyword{case}~\isa{(}\emph{constructor} \emph{vars}\isa{)}' notation also
kleing@13999
   644
works for arbitrary induction theorems with numbered cases. The order
kleing@13999
   645
of the \emph{vars} corresponds to the order of the
kleing@13999
   646
\isa{{\isasymAnd}}-quantified variables in each case of the induction
kleing@13999
   647
theorem. For induction theorems produced by \isakeyword{recdef} it is
kleing@13999
   648
the order in which the variables appear on the left-hand side of the
kleing@13999
   649
equation.
kleing@13999
   650
kleing@13999
   651
The proof is so simple that it can be condensed to%
kleing@13999
   652
\end{isamarkuptext}%
wenzelm@17175
   653
\isamarkuptrue%
wenzelm@17125
   654
%
wenzelm@17125
   655
\isadelimproof
wenzelm@17125
   656
%
wenzelm@17125
   657
\endisadelimproof
wenzelm@17125
   658
%
wenzelm@17125
   659
\isatagproof
wenzelm@17175
   660
\isacommand{by}\isamarkupfalse%
wenzelm@17175
   661
\ {\isacharparenleft}induct\ xs\ rule{\isacharcolon}\ rot{\isachardot}induct{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline
wenzelm@17125
   662
%
wenzelm@17125
   663
\endisatagproof
wenzelm@17125
   664
{\isafoldproof}%
wenzelm@17125
   665
%
wenzelm@17125
   666
\isadelimproof
wenzelm@17125
   667
%
wenzelm@17125
   668
\endisadelimproof
wenzelm@17125
   669
%
wenzelm@17125
   670
\isadelimtheory
wenzelm@17125
   671
%
wenzelm@17125
   672
\endisadelimtheory
wenzelm@17125
   673
%
wenzelm@17125
   674
\isatagtheory
wenzelm@17125
   675
%
wenzelm@17125
   676
\endisatagtheory
wenzelm@17125
   677
{\isafoldtheory}%
wenzelm@17125
   678
%
wenzelm@17125
   679
\isadelimtheory
wenzelm@17125
   680
%
wenzelm@17125
   681
\endisadelimtheory
kleing@13999
   682
\end{isabellebody}%
kleing@13999
   683
%%% Local Variables:
kleing@13999
   684
%%% mode: latex
kleing@13999
   685
%%% TeX-master: "root"
kleing@13999
   686
%%% End: