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:
`