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