wneuper/isa: doc-src/IsarRef/Thy/document/Synopsis.tex@a45121ffcfcb

1 %

     2 \begin{isabellebody}%

     3 \def\isabellecontext{Synopsis}%

4 %

     5 \isadelimtheory

6 %

     7 \endisadelimtheory

8 %

     9 \isatagtheory

    10 \isacommand{theory}\isamarkupfalse%

    11 \ Synopsis\isanewline

    12 \isakeyword{imports}\ Base\ Main\isanewline

    13 \isakeyword{begin}%

    14 \endisatagtheory

    15 {\isafoldtheory}%

    16 %

    17 \isadelimtheory

    18 %

    19 \endisadelimtheory

    20 %

    21 \isamarkupchapter{Synopsis%

    22 }

    23 \isamarkuptrue%

    24 %

    25 \isamarkupsection{Notepad%

    26 }

    27 \isamarkuptrue%

    28 %

    29 \begin{isamarkuptext}%

    30 An Isar proof body serves as mathematical notepad to compose logical

    31   content, consisting of types, terms, facts.%

    32 \end{isamarkuptext}%

    33 \isamarkuptrue%

    34 %

    35 \isamarkupsubsection{Types and terms%

    36 }

    37 \isamarkuptrue%

    38 \isacommand{notepad}\isamarkupfalse%

    39 \isanewline

    40 \isakeyword{begin}%

    41 \isadelimproof

    42 %

    43 \endisadelimproof

    44 %

    45 \isatagproof

    46 %

    47 \begin{isamarkuptxt}%

    48 Locally fixed entities:%

    49 \end{isamarkuptxt}%

    50 \isamarkuptrue%

    51 \ \ \isacommand{fix}\isamarkupfalse%

    52 \ x\ \ \ %

    53 \isamarkupcmt{local constant, without any type information yet%

    54 }

    55 \isanewline

    56 \ \ \isacommand{fix}\isamarkupfalse%

    57 \ x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ \ %

    58 \isamarkupcmt{variant with explicit type-constraint for subsequent use%

    59 }

    60 \isanewline

    61 \isanewline

    62 \ \ \isacommand{fix}\isamarkupfalse%

    63 \ a\ b\isanewline

    64 \ \ \isacommand{assume}\isamarkupfalse%

    65 \ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{22}{\isachardoublequoteclose}}\ \ %

    66 \isamarkupcmt{type assignment at first occurrence in concrete term%

    67 }

    68 %

    69 \begin{isamarkuptxt}%

    70 Definitions (non-polymorphic):%

    71 \end{isamarkuptxt}%

    72 \isamarkuptrue%

    73 \ \ \isacommand{def}\isamarkupfalse%

    74 \ x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{22}{\isachardoublequoteopen}}t{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequoteclose}}%

    75 \begin{isamarkuptxt}%

    76 Abbreviations (polymorphic):%

    77 \end{isamarkuptxt}%

    78 \isamarkuptrue%

    79 \ \ \isacommand{let}\isamarkupfalse%

    80 \ {\isaliteral{3F}{\isacharquery}}f\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{22}{\isachardoublequoteclose}}%

    81 \endisatagproof

    82 {\isafoldproof}%

    83 %

    84 \isadelimproof

    85 %

    86 \endisadelimproof

    87 \isanewline

    88 \ \ \isacommand{term}\isamarkupfalse%

    89 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}f\ {\isaliteral{3F}{\isacharquery}}f{\isaliteral{22}{\isachardoublequoteclose}}%

    90 \isadelimproof

    91 %

    92 \endisadelimproof

    93 %

    94 \isatagproof

    95 %

    96 \begin{isamarkuptxt}%

    97 Notation:%

    98 \end{isamarkuptxt}%

    99 \isamarkuptrue%

   100 \ \ \isacommand{write}\isamarkupfalse%

   101 \ x\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}%

   102 \endisatagproof

   103 {\isafoldproof}%

   104 %

   105 \isadelimproof

   106 %

   107 \endisadelimproof

   108 \isanewline

   109 \isacommand{end}\isamarkupfalse%

   110 %

   111 \isamarkupsubsection{Facts%

   112 }

   113 \isamarkuptrue%

   114 %

   115 \begin{isamarkuptext}%

   116 A fact is a simultaneous list of theorems.%

   117 \end{isamarkuptext}%

   118 \isamarkuptrue%

   119 %

   120 \isamarkupsubsubsection{Producing facts%

   121 }

   122 \isamarkuptrue%

   123 \isacommand{notepad}\isamarkupfalse%

   124 \isanewline

   125 \isakeyword{begin}%

   126 \isadelimproof

   127 %

   128 \endisadelimproof

   129 %

   130 \isatagproof

   131 %

   132 \begin{isamarkuptxt}%

   133 Via assumption (``lambda''):%

   134 \end{isamarkuptxt}%

   135 \isamarkuptrue%

   136 \ \ \isacommand{assume}\isamarkupfalse%

   137 \ a{\isaliteral{3A}{\isacharcolon}}\ A%

   138 \begin{isamarkuptxt}%

   139 Via proof (``let''):%

   140 \end{isamarkuptxt}%

   141 \isamarkuptrue%

   142 \ \ \isacommand{have}\isamarkupfalse%

   143 \ b{\isaliteral{3A}{\isacharcolon}}\ B\ \isacommand{sorry}\isamarkupfalse%

   144 %

   145 \begin{isamarkuptxt}%

   146 Via abbreviation (``let''):%

   147 \end{isamarkuptxt}%

   148 \isamarkuptrue%

   149 \ \ \isacommand{note}\isamarkupfalse%

   150 \ c\ {\isaliteral{3D}{\isacharequal}}\ a\ b%

   151 \endisatagproof

   152 {\isafoldproof}%

   153 %

   154 \isadelimproof

   155 %

   156 \endisadelimproof

   157 \isanewline

   158 \isanewline

   159 \isacommand{end}\isamarkupfalse%

   160 %

   161 \isamarkupsubsubsection{Referencing facts%

   162 }

   163 \isamarkuptrue%

   164 \isacommand{notepad}\isamarkupfalse%

   165 \isanewline

   166 \isakeyword{begin}%

   167 \isadelimproof

   168 %

   169 \endisadelimproof

   170 %

   171 \isatagproof

   172 %

   173 \begin{isamarkuptxt}%

   174 Via explicit name:%

   175 \end{isamarkuptxt}%

   176 \isamarkuptrue%

   177 \ \ \isacommand{assume}\isamarkupfalse%

   178 \ a{\isaliteral{3A}{\isacharcolon}}\ A\isanewline

   179 \ \ \isacommand{note}\isamarkupfalse%

   180 \ a%

   181 \begin{isamarkuptxt}%

   182 Via implicit name:%

   183 \end{isamarkuptxt}%

   184 \isamarkuptrue%

   185 \ \ \isacommand{assume}\isamarkupfalse%

   186 \ A\isanewline

   187 \ \ \isacommand{note}\isamarkupfalse%

   188 \ this%

   189 \begin{isamarkuptxt}%

   190 Via literal proposition (unification with results from the proof text):%

   191 \end{isamarkuptxt}%

   192 \isamarkuptrue%

   193 \ \ \isacommand{assume}\isamarkupfalse%

   194 \ A\isanewline

   195 \ \ \isacommand{note}\isamarkupfalse%

   196 \ {\isaliteral{60}{\isacharbackquoteopen}}A{\isaliteral{60}{\isacharbackquoteclose}}\isanewline

   197 \isanewline

   198 \ \ \isacommand{assume}\isamarkupfalse%

   199 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ B\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

   200 \ \ \isacommand{note}\isamarkupfalse%

   201 \ {\isaliteral{60}{\isacharbackquoteopen}}B\ a{\isaliteral{60}{\isacharbackquoteclose}}\isanewline

   202 \ \ \isacommand{note}\isamarkupfalse%

   203 \ {\isaliteral{60}{\isacharbackquoteopen}}B\ b{\isaliteral{60}{\isacharbackquoteclose}}%

   204 \endisatagproof

   205 {\isafoldproof}%

   206 %

   207 \isadelimproof

   208 %

   209 \endisadelimproof

   210 \isanewline

   211 \isacommand{end}\isamarkupfalse%

   212 %

   213 \isamarkupsubsubsection{Manipulating facts%

   214 }

   215 \isamarkuptrue%

   216 \isacommand{notepad}\isamarkupfalse%

   217 \isanewline

   218 \isakeyword{begin}%

   219 \isadelimproof

   220 %

   221 \endisadelimproof

   222 %

   223 \isatagproof

   224 %

   225 \begin{isamarkuptxt}%

   226 Instantiation:%

   227 \end{isamarkuptxt}%

   228 \isamarkuptrue%

   229 \ \ \isacommand{assume}\isamarkupfalse%

   230 \ a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ B\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

   231 \ \ \isacommand{note}\isamarkupfalse%

   232 \ a\isanewline

   233 \ \ \isacommand{note}\isamarkupfalse%

   234 \ a\ {\isaliteral{5B}{\isacharbrackleft}}of\ b{\isaliteral{5D}{\isacharbrackright}}\isanewline

   235 \ \ \isacommand{note}\isamarkupfalse%

   236 \ a\ {\isaliteral{5B}{\isacharbrackleft}}\isakeyword{where}\ x\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{5D}{\isacharbrackright}}%

   237 \begin{isamarkuptxt}%

   238 Backchaining:%

   239 \end{isamarkuptxt}%

   240 \isamarkuptrue%

   241 \ \ \isacommand{assume}\isamarkupfalse%

   242 \ {\isadigit{1}}{\isaliteral{3A}{\isacharcolon}}\ A\isanewline

   243 \ \ \isacommand{assume}\isamarkupfalse%

   244 \ {\isadigit{2}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

   245 \ \ \isacommand{note}\isamarkupfalse%

   246 \ {\isadigit{2}}\ {\isaliteral{5B}{\isacharbrackleft}}OF\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}\isanewline

   247 \ \ \isacommand{note}\isamarkupfalse%

   248 \ {\isadigit{1}}\ {\isaliteral{5B}{\isacharbrackleft}}THEN\ {\isadigit{2}}{\isaliteral{5D}{\isacharbrackright}}%

   249 \begin{isamarkuptxt}%

   250 Symmetric results:%

   251 \end{isamarkuptxt}%

   252 \isamarkuptrue%

   253 \ \ \isacommand{assume}\isamarkupfalse%

   254 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

   255 \ \ \isacommand{note}\isamarkupfalse%

   256 \ this\ {\isaliteral{5B}{\isacharbrackleft}}symmetric{\isaliteral{5D}{\isacharbrackright}}\isanewline

   257 \isanewline

   258 \ \ \isacommand{assume}\isamarkupfalse%

   259 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

   260 \ \ \isacommand{note}\isamarkupfalse%

   261 \ this\ {\isaliteral{5B}{\isacharbrackleft}}symmetric{\isaliteral{5D}{\isacharbrackright}}%

   262 \begin{isamarkuptxt}%

   263 Adhoc-simplification (take care!):%

   264 \end{isamarkuptxt}%

   265 \isamarkuptrue%

   266 \ \ \isacommand{assume}\isamarkupfalse%

   267 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{40}{\isacharat}}\ xs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

   268 \ \ \isacommand{note}\isamarkupfalse%

   269 \ this\ {\isaliteral{5B}{\isacharbrackleft}}simplified{\isaliteral{5D}{\isacharbrackright}}%

   270 \endisatagproof

   271 {\isafoldproof}%

   272 %

   273 \isadelimproof

   274 %

   275 \endisadelimproof

   276 \isanewline

   277 \isacommand{end}\isamarkupfalse%

   278 %

   279 \isamarkupsubsubsection{Projections%

   280 }

   281 \isamarkuptrue%

   282 %

   283 \begin{isamarkuptext}%

   284 Isar facts consist of multiple theorems.  There is notation to project

   285   interval ranges.%

   286 \end{isamarkuptext}%

   287 \isamarkuptrue%

   288 \isacommand{notepad}\isamarkupfalse%

   289 \isanewline

   290 \isakeyword{begin}\isanewline

   291 %

   292 \isadelimproof

   293 \ \ %

   294 \endisadelimproof

   295 %

   296 \isatagproof

   297 \isacommand{assume}\isamarkupfalse%

   298 \ stuff{\isaliteral{3A}{\isacharcolon}}\ A\ B\ C\ D\isanewline

   299 \ \ \isacommand{note}\isamarkupfalse%

   300 \ stuff{\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\isanewline

   301 \ \ \isacommand{note}\isamarkupfalse%

   302 \ stuff{\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}{\isaliteral{2D}{\isacharminus}}{\isadigit{3}}{\isaliteral{29}{\isacharparenright}}\isanewline

   303 \ \ \isacommand{note}\isamarkupfalse%

   304 \ stuff{\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{29}{\isacharparenright}}%

   305 \endisatagproof

   306 {\isafoldproof}%

   307 %

   308 \isadelimproof

   309 \isanewline

   310 %

   311 \endisadelimproof

   312 \isacommand{end}\isamarkupfalse%

   313 %

   314 \isamarkupsubsubsection{Naming conventions%

   315 }

   316 \isamarkuptrue%

   317 %

   318 \begin{isamarkuptext}%

   319 \begin{itemize}

   321   \item Lower-case identifiers are usually preferred.

   323   \item Facts can be named after the main term within the proposition.

   325   \item Facts should \emph{not} be named after the command that

   326   introduced them (\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}, \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}).  This is

   327   misleading and hard to maintain.

   329   \item Natural numbers can be used as ``meaningless'' names (more

   330   appropriate than \isa{{\isaliteral{22}{\isachardoublequote}}a{\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}a{\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}} etc.)

   332   \item Symbolic identifiers are supported (e.g. \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}).

   334   \end{itemize}%

   335 \end{isamarkuptext}%

   336 \isamarkuptrue%

   337 %

   338 \isamarkupsubsection{Block structure%

   339 }

   340 \isamarkuptrue%

   341 %

   342 \begin{isamarkuptext}%

   343 The formal notepad is block structured.  The fact produced by the last

   344   entry of a block is exported into the outer context.%

   345 \end{isamarkuptext}%

   346 \isamarkuptrue%

   347 \isacommand{notepad}\isamarkupfalse%

   348 \isanewline

   349 \isakeyword{begin}\isanewline

   350 %

   351 \isadelimproof

   352 \ \ %

   353 \endisadelimproof

   354 %

   355 \isatagproof

   356 \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%

   357 \isanewline

   358 \ \ \ \ \isacommand{have}\isamarkupfalse%

   359 \ a{\isaliteral{3A}{\isacharcolon}}\ A\ \isacommand{sorry}\isamarkupfalse%

   360 \isanewline

   361 \ \ \ \ \isacommand{have}\isamarkupfalse%

   362 \ b{\isaliteral{3A}{\isacharcolon}}\ B\ \isacommand{sorry}\isamarkupfalse%

   363 \isanewline

   364 \ \ \ \ \isacommand{note}\isamarkupfalse%

   365 \ a\ b\isanewline

   366 \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%

   367 \isanewline

   368 \ \ \isacommand{note}\isamarkupfalse%

   369 \ this\isanewline

   370 \ \ \isacommand{note}\isamarkupfalse%

   371 \ {\isaliteral{60}{\isacharbackquoteopen}}A{\isaliteral{60}{\isacharbackquoteclose}}\isanewline

   372 \ \ \isacommand{note}\isamarkupfalse%

   373 \ {\isaliteral{60}{\isacharbackquoteopen}}B{\isaliteral{60}{\isacharbackquoteclose}}%

   374 \endisatagproof

   375 {\isafoldproof}%

   376 %

   377 \isadelimproof

   378 \isanewline

   379 %

   380 \endisadelimproof

   381 \isacommand{end}\isamarkupfalse%

   382 %

   383 \begin{isamarkuptext}%

   384 Explicit blocks as well as implicit blocks of nested goal

   385   statements (e.g.\ \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}) automatically introduce one extra

   386   pair of parentheses in reserve.  The \hyperlink{command.next}{\mbox{\isa{\isacommand{next}}}} command allows

   387   to ``jump'' between these sub-blocks.%

   388 \end{isamarkuptext}%

   389 \isamarkuptrue%

   390 \isacommand{notepad}\isamarkupfalse%

   391 \isanewline

   392 \isakeyword{begin}\isanewline

   393 %

   394 \isadelimproof

   395 \isanewline

   396 \ \ %

   397 \endisadelimproof

   398 %

   399 \isatagproof

   400 \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%

   401 \isanewline

   402 \ \ \ \ \isacommand{have}\isamarkupfalse%

   403 \ a{\isaliteral{3A}{\isacharcolon}}\ A\ \isacommand{sorry}\isamarkupfalse%

   404 \isanewline

   405 \ \ \isacommand{next}\isamarkupfalse%

   406 \isanewline

   407 \ \ \ \ \isacommand{have}\isamarkupfalse%

   408 \ b{\isaliteral{3A}{\isacharcolon}}\ B\isanewline

   409 \ \ \ \ \isacommand{proof}\isamarkupfalse%

   410 \ {\isaliteral{2D}{\isacharminus}}\isanewline

   411 \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%

   412 \ B\ \isacommand{sorry}\isamarkupfalse%

   413 \isanewline

   414 \ \ \ \ \isacommand{next}\isamarkupfalse%

   415 \isanewline

   416 \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%

   417 \ c{\isaliteral{3A}{\isacharcolon}}\ C\ \isacommand{sorry}\isamarkupfalse%

   418 \isanewline

   419 \ \ \ \ \isacommand{next}\isamarkupfalse%

   420 \isanewline

   421 \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%

   422 \ d{\isaliteral{3A}{\isacharcolon}}\ D\ \isacommand{sorry}\isamarkupfalse%

   423 \isanewline

   424 \ \ \ \ \isacommand{qed}\isamarkupfalse%

   425 \isanewline

   426 \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%

   427 %

   428 \begin{isamarkuptxt}%

   429 Alternative version with explicit parentheses everywhere:%

   430 \end{isamarkuptxt}%

   431 \isamarkuptrue%

   432 \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%

   433 \isanewline

   434 \ \ \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%

   435 \isanewline

   436 \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%

   437 \ a{\isaliteral{3A}{\isacharcolon}}\ A\ \isacommand{sorry}\isamarkupfalse%

   438 \isanewline

   439 \ \ \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%

   440 \isanewline

   441 \ \ \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%

   442 \isanewline

   443 \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%

   444 \ b{\isaliteral{3A}{\isacharcolon}}\ B\isanewline

   445 \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%

   446 \ {\isaliteral{2D}{\isacharminus}}\isanewline

   447 \ \ \ \ \ \ \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%

   448 \isanewline

   449 \ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%

   450 \ B\ \isacommand{sorry}\isamarkupfalse%

   451 \isanewline

   452 \ \ \ \ \ \ \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%

   453 \isanewline

   454 \ \ \ \ \ \ \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%

   455 \isanewline

   456 \ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%

   457 \ c{\isaliteral{3A}{\isacharcolon}}\ C\ \isacommand{sorry}\isamarkupfalse%

   458 \isanewline

   459 \ \ \ \ \ \ \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%

   460 \isanewline

   461 \ \ \ \ \ \ \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%

   462 \isanewline

   463 \ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%

   464 \ d{\isaliteral{3A}{\isacharcolon}}\ D\ \isacommand{sorry}\isamarkupfalse%

   465 \isanewline

   466 \ \ \ \ \ \ \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%

   467 \isanewline

   468 \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%

   469 \isanewline

   470 \ \ \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%

   471 \isanewline

   472 \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%

   473 %

   474 \endisatagproof

   475 {\isafoldproof}%

   476 %

   477 \isadelimproof

   478 \isanewline

   479 %

   480 \endisadelimproof

   481 \isanewline

   482 \isacommand{end}\isamarkupfalse%

   483 %

   484 \isamarkupsection{Calculational reasoning \label{sec:calculations-synopsis}%

   485 }

   486 \isamarkuptrue%

   487 %

   488 \begin{isamarkuptext}%

   489 For example, see \verb|~~/src/HOL/Isar_Examples/Group.thy|.%

   490 \end{isamarkuptext}%

   491 \isamarkuptrue%

   492 %

   493 \isamarkupsubsection{Special names in Isar proofs%

   494 }

   495 \isamarkuptrue%

   496 %

   497 \begin{isamarkuptext}%

   498 \begin{itemize}

   500   \item term \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}thesis{\isaliteral{22}{\isachardoublequote}}} --- the main conclusion of the

   501   innermost pending claim

   503   \item term \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} --- the argument of the last explicitly

   504     stated result (for infix application this is the right-hand side)

   506   \item fact \isa{{\isaliteral{22}{\isachardoublequote}}this{\isaliteral{22}{\isachardoublequote}}} --- the last result produced in the text

   508   \end{itemize}%

   509 \end{isamarkuptext}%

   510 \isamarkuptrue%

   511 \isacommand{notepad}\isamarkupfalse%

   512 \isanewline

   513 \isakeyword{begin}\isanewline

   514 %

   515 \isadelimproof

   516 \ \ %

   517 \endisadelimproof

   518 %

   519 \isatagproof

   520 \isacommand{have}\isamarkupfalse%

   521 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

   522 \ \ \isacommand{proof}\isamarkupfalse%

   523 \ {\isaliteral{2D}{\isacharminus}}%

   524 \endisatagproof

   525 {\isafoldproof}%

   526 %

   527 \isadelimproof

   528 \isanewline

   529 %

   530 \endisadelimproof

   531 \ \ \ \ \isacommand{term}\isamarkupfalse%

   532 \ {\isaliteral{3F}{\isacharquery}}thesis\isanewline

   533 %

   534 \isadelimproof

   535 \ \ \ \ %

   536 \endisadelimproof

   537 %

   538 \isatagproof

   539 \isacommand{show}\isamarkupfalse%

   540 \ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{sorry}\isamarkupfalse%

   541 %

   542 \endisatagproof

   543 {\isafoldproof}%

   544 %

   545 \isadelimproof

   546 \isanewline

   547 %

   548 \endisadelimproof

   549 \ \ \ \ \isacommand{term}\isamarkupfalse%

   550 \ {\isaliteral{3F}{\isacharquery}}thesis\ \ %

   551 \isamarkupcmt{static!%

   552 }

   553 \isanewline

   554 %

   555 \isadelimproof

   556 \ \ %

   557 \endisadelimproof

   558 %

   559 \isatagproof

   560 \isacommand{qed}\isamarkupfalse%

   561 %

   562 \endisatagproof

   563 {\isafoldproof}%

   564 %

   565 \isadelimproof

   566 \isanewline

   567 %

   568 \endisadelimproof

   569 \ \ \isacommand{term}\isamarkupfalse%

   570 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

   571 \ \ \isacommand{thm}\isamarkupfalse%

   572 \ this\isanewline

   573 \isacommand{end}\isamarkupfalse%

   574 %

   575 \begin{isamarkuptext}%

   576 Calculational reasoning maintains the special fact called

   577   ``\isa{calculation}'' in the background.  Certain language

   578   elements combine primary \isa{this} with secondary \isa{calculation}.%

   579 \end{isamarkuptext}%

   580 \isamarkuptrue%

   581 %

   582 \isamarkupsubsection{Transitive chains%

   583 }

   584 \isamarkuptrue%

   585 %

   586 \begin{isamarkuptext}%

   587 The Idea is to combine \isa{this} and \isa{calculation}

   588   via typical \isa{trans} rules (see also \hyperlink{command.print-trans-rules}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}trans{\isaliteral{5F}{\isacharunderscore}}rules}}}}):%

   589 \end{isamarkuptext}%

   590 \isamarkuptrue%

   591 \isacommand{thm}\isamarkupfalse%

   592 \ trans\isanewline

   593 \isacommand{thm}\isamarkupfalse%

   594 \ less{\isaliteral{5F}{\isacharunderscore}}trans\isanewline

   595 \isacommand{thm}\isamarkupfalse%

   596 \ less{\isaliteral{5F}{\isacharunderscore}}le{\isaliteral{5F}{\isacharunderscore}}trans\isanewline

   597 \isanewline

   598 \isacommand{notepad}\isamarkupfalse%

   599 \isanewline

   600 \isakeyword{begin}%

   601 \isadelimproof

   602 %

   603 \endisadelimproof

   604 %

   605 \isatagproof

   606 %

   607 \begin{isamarkuptxt}%

   608 Plain bottom-up calculation:%

   609 \end{isamarkuptxt}%

   610 \isamarkuptrue%

   611 \ \ \isacommand{have}\isamarkupfalse%

   612 \ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

   613 \isanewline

   614 \ \ \isacommand{also}\isamarkupfalse%

   615 \isanewline

   616 \ \ \isacommand{have}\isamarkupfalse%

   617 \ {\isaliteral{22}{\isachardoublequoteopen}}b\ {\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

   618 \isanewline

   619 \ \ \isacommand{also}\isamarkupfalse%

   620 \isanewline

   621 \ \ \isacommand{have}\isamarkupfalse%

   622 \ {\isaliteral{22}{\isachardoublequoteopen}}c\ {\isaliteral{3D}{\isacharequal}}\ d{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

   623 \isanewline

   624 \ \ \isacommand{finally}\isamarkupfalse%

   625 \isanewline

   626 \ \ \isacommand{have}\isamarkupfalse%

   627 \ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3D}{\isacharequal}}\ d{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

   628 %

   629 \begin{isamarkuptxt}%

   630 Variant using the \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} abbreviation:%

   631 \end{isamarkuptxt}%

   632 \isamarkuptrue%

   633 \ \ \isacommand{have}\isamarkupfalse%

   634 \ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

   635 \isanewline

   636 \ \ \isacommand{also}\isamarkupfalse%

   637 \isanewline

   638 \ \ \isacommand{have}\isamarkupfalse%

   639 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

   640 \isanewline

   641 \ \ \isacommand{also}\isamarkupfalse%

   642 \isanewline

   643 \ \ \isacommand{have}\isamarkupfalse%

   644 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ d{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

   645 \isanewline

   646 \ \ \isacommand{finally}\isamarkupfalse%

   647 \isanewline

   648 \ \ \isacommand{have}\isamarkupfalse%

   649 \ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3D}{\isacharequal}}\ d{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

   650 %

   651 \begin{isamarkuptxt}%

   652 Top-down version with explicit claim at the head:%

   653 \end{isamarkuptxt}%

   654 \isamarkuptrue%

   655 \ \ \isacommand{have}\isamarkupfalse%

   656 \ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3D}{\isacharequal}}\ d{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

   657 \ \ \isacommand{proof}\isamarkupfalse%

   658 \ {\isaliteral{2D}{\isacharminus}}\isanewline

   659 \ \ \ \ \isacommand{have}\isamarkupfalse%

   660 \ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

   661 \isanewline

   662 \ \ \ \ \isacommand{also}\isamarkupfalse%

   663 \isanewline

   664 \ \ \ \ \isacommand{have}\isamarkupfalse%

   665 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

   666 \isanewline

   667 \ \ \ \ \isacommand{also}\isamarkupfalse%

   668 \isanewline

   669 \ \ \ \ \isacommand{have}\isamarkupfalse%

   670 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ d{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

   671 \isanewline

   672 \ \ \ \ \isacommand{finally}\isamarkupfalse%

   673 \isanewline

   674 \ \ \ \ \isacommand{show}\isamarkupfalse%

   675 \ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

   676 \isanewline

   677 \ \ \isacommand{qed}\isamarkupfalse%

   678 \isanewline

   679 \isacommand{next}\isamarkupfalse%

   680 %

   681 \begin{isamarkuptxt}%

   682 Mixed inequalities (require suitable base type):%

   683 \end{isamarkuptxt}%

   684 \isamarkuptrue%

   685 \ \ \isacommand{fix}\isamarkupfalse%

   686 \ a\ b\ c\ d\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\isanewline

   687 \isanewline

   688 \ \ \isacommand{have}\isamarkupfalse%

   689 \ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3C}{\isacharless}}\ b{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

   690 \isanewline

   691 \ \ \isacommand{also}\isamarkupfalse%

   692 \isanewline

   693 \ \ \isacommand{have}\isamarkupfalse%

   694 \ {\isaliteral{22}{\isachardoublequoteopen}}b{\isaliteral{5C3C6C653E}{\isasymle}}\ c{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

   695 \isanewline

   696 \ \ \isacommand{also}\isamarkupfalse%

   697 \isanewline

   698 \ \ \isacommand{have}\isamarkupfalse%

   699 \ {\isaliteral{22}{\isachardoublequoteopen}}c\ {\isaliteral{3D}{\isacharequal}}\ d{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

   700 \isanewline

   701 \ \ \isacommand{finally}\isamarkupfalse%

   702 \isanewline

   703 \ \ \isacommand{have}\isamarkupfalse%

   704 \ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3C}{\isacharless}}\ d{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

   705 %

   706 \endisatagproof

   707 {\isafoldproof}%

   708 %

   709 \isadelimproof

   710 %

   711 \endisadelimproof

   712 \isanewline

   713 \isacommand{end}\isamarkupfalse%

   714 %

   715 \isamarkupsubsubsection{Notes%

   716 }

   717 \isamarkuptrue%

   718 %

   719 \begin{isamarkuptext}%

   720 \begin{itemize}

   722   \item The notion of \isa{trans} rule is very general due to the

   723   flexibility of Isabelle/Pure rule composition.

   725   \item User applications may declare there own rules, with some care

   726   about the operational details of higher-order unification.

   728   \end{itemize}%

   729 \end{isamarkuptext}%

   730 \isamarkuptrue%

   731 %

   732 \isamarkupsubsection{Degenerate calculations and bigstep reasoning%

   733 }

   734 \isamarkuptrue%

   735 %

   736 \begin{isamarkuptext}%

   737 The Idea is to append \isa{this} to \isa{calculation},

   738   without rule composition.%

   739 \end{isamarkuptext}%

   740 \isamarkuptrue%

   741 \isacommand{notepad}\isamarkupfalse%

   742 \isanewline

   743 \isakeyword{begin}%

   744 \isadelimproof

   745 %

   746 \endisadelimproof

   747 %

   748 \isatagproof

   749 %

   750 \begin{isamarkuptxt}%

   751 A vacuous proof:%

   752 \end{isamarkuptxt}%

   753 \isamarkuptrue%

   754 \ \ \isacommand{have}\isamarkupfalse%

   755 \ A\ \isacommand{sorry}\isamarkupfalse%

   756 \isanewline

   757 \ \ \isacommand{moreover}\isamarkupfalse%

   758 \isanewline

   759 \ \ \isacommand{have}\isamarkupfalse%

   760 \ B\ \isacommand{sorry}\isamarkupfalse%

   761 \isanewline

   762 \ \ \isacommand{moreover}\isamarkupfalse%

   763 \isanewline

   764 \ \ \isacommand{have}\isamarkupfalse%

   765 \ C\ \isacommand{sorry}\isamarkupfalse%

   766 \isanewline

   767 \ \ \isacommand{ultimately}\isamarkupfalse%

   768 \isanewline

   769 \ \ \isacommand{have}\isamarkupfalse%

   770 \ A\ \isakeyword{and}\ B\ \isakeyword{and}\ C\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

   771 \isanewline

   772 \isacommand{next}\isamarkupfalse%

   773 %

   774 \begin{isamarkuptxt}%

   775 Slightly more content (trivial bigstep reasoning):%

   776 \end{isamarkuptxt}%

   777 \isamarkuptrue%

   778 \ \ \isacommand{have}\isamarkupfalse%

   779 \ A\ \isacommand{sorry}\isamarkupfalse%

   780 \isanewline

   781 \ \ \isacommand{moreover}\isamarkupfalse%

   782 \isanewline

   783 \ \ \isacommand{have}\isamarkupfalse%

   784 \ B\ \isacommand{sorry}\isamarkupfalse%

   785 \isanewline

   786 \ \ \isacommand{moreover}\isamarkupfalse%

   787 \isanewline

   788 \ \ \isacommand{have}\isamarkupfalse%

   789 \ C\ \isacommand{sorry}\isamarkupfalse%

   790 \isanewline

   791 \ \ \isacommand{ultimately}\isamarkupfalse%

   792 \isanewline

   793 \ \ \isacommand{have}\isamarkupfalse%

   794 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ C{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%

   795 \ blast\isanewline

   796 \isacommand{next}\isamarkupfalse%

   797 %

   798 \begin{isamarkuptxt}%

   799 More ambitious bigstep reasoning involving structured results:%

   800 \end{isamarkuptxt}%

   801 \isamarkuptrue%

   802 \ \ \isacommand{have}\isamarkupfalse%

   803 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B\ {\isaliteral{5C3C6F723E}{\isasymor}}\ C{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

   804 \isanewline

   805 \ \ \isacommand{moreover}\isamarkupfalse%

   806 \isanewline

   807 \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%

   808 \ \isacommand{assume}\isamarkupfalse%

   809 \ A\ \isacommand{have}\isamarkupfalse%

   810 \ R\ \isacommand{sorry}\isamarkupfalse%

   811 \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%

   812 \isanewline

   813 \ \ \isacommand{moreover}\isamarkupfalse%

   814 \isanewline

   815 \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%

   816 \ \isacommand{assume}\isamarkupfalse%

   817 \ B\ \isacommand{have}\isamarkupfalse%

   818 \ R\ \isacommand{sorry}\isamarkupfalse%

   819 \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%

   820 \isanewline

   821 \ \ \isacommand{moreover}\isamarkupfalse%

   822 \isanewline

   823 \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%

   824 \ \isacommand{assume}\isamarkupfalse%

   825 \ C\ \isacommand{have}\isamarkupfalse%

   826 \ R\ \isacommand{sorry}\isamarkupfalse%

   827 \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%

   828 \isanewline

   829 \ \ \isacommand{ultimately}\isamarkupfalse%

   830 \isanewline

   831 \ \ \isacommand{have}\isamarkupfalse%

   832 \ R\ \isacommand{by}\isamarkupfalse%

   833 \ blast\ \ %

   834 \isamarkupcmt{``big-bang integration'' of proof blocks (occasionally fragile)%

   835 }

   836 %

   837 \endisatagproof

   838 {\isafoldproof}%

   839 %

   840 \isadelimproof

   841 %

   842 \endisadelimproof

   843 \isanewline

   844 \isacommand{end}\isamarkupfalse%

   845 %

   846 \isamarkupsection{Induction%

   847 }

   848 \isamarkuptrue%

   849 %

   850 \isamarkupsubsection{Induction as Natural Deduction%

   851 }

   852 \isamarkuptrue%

   853 %

   854 \begin{isamarkuptext}%

   855 In principle, induction is just a special case of Natural

   856   Deduction (see also \secref{sec:natural-deduction-synopsis}).  For

   857   example:%

   858 \end{isamarkuptext}%

   859 \isamarkuptrue%

   860 \isacommand{thm}\isamarkupfalse%

   861 \ nat{\isaliteral{2E}{\isachardot}}induct\isanewline

   862 \isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}\isamarkupfalse%

   863 \ nat{\isaliteral{2E}{\isachardot}}induct\isanewline

   864 \isanewline

   865 \isacommand{notepad}\isamarkupfalse%

   866 \isanewline

   867 \isakeyword{begin}\isanewline

   868 %

   869 \isadelimproof

   870 \ \ %

   871 \endisadelimproof

   872 %

   873 \isatagproof

   874 \isacommand{fix}\isamarkupfalse%

   875 \ n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\isanewline

   876 \ \ \isacommand{have}\isamarkupfalse%

   877 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

   878 \ \ \isacommand{proof}\isamarkupfalse%

   879 \ {\isaliteral{28}{\isacharparenleft}}rule\ nat{\isaliteral{2E}{\isachardot}}induct{\isaliteral{29}{\isacharparenright}}\ \ %

   880 \isamarkupcmt{fragile rule application!%

   881 }

   882 \isanewline

   883 \ \ \ \ \isacommand{show}\isamarkupfalse%

   884 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

   885 \isanewline

   886 \ \ \isacommand{next}\isamarkupfalse%

   887 \isanewline

   888 \ \ \ \ \isacommand{fix}\isamarkupfalse%

   889 \ n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\isanewline

   890 \ \ \ \ \isacommand{assume}\isamarkupfalse%

   891 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

   892 \ \ \ \ \isacommand{show}\isamarkupfalse%

   893 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

   894 \isanewline

   895 \ \ \isacommand{qed}\isamarkupfalse%

   896 %

   897 \endisatagproof

   898 {\isafoldproof}%

   899 %

   900 \isadelimproof

   901 \isanewline

   902 %

   903 \endisadelimproof

   904 \isacommand{end}\isamarkupfalse%

   905 %

   906 \begin{isamarkuptext}%

   907 In practice, much more proof infrastructure is required.

   909   The proof method \hyperlink{method.induct}{\mbox{\isa{induct}}} provides:

   910   \begin{itemize}

   912   \item implicit rule selection and robust instantiation

   914   \item context elements via symbolic case names

   916   \item support for rule-structured induction statements, with local

   917     parameters, premises, etc.

   919   \end{itemize}%

   920 \end{isamarkuptext}%

   921 \isamarkuptrue%

   922 \isacommand{notepad}\isamarkupfalse%

   923 \isanewline

   924 \isakeyword{begin}\isanewline

   925 %

   926 \isadelimproof

   927 \ \ %

   928 \endisadelimproof

   929 %

   930 \isatagproof

   931 \isacommand{fix}\isamarkupfalse%

   932 \ n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\isanewline

   933 \ \ \isacommand{have}\isamarkupfalse%

   934 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

   935 \ \ \isacommand{proof}\isamarkupfalse%

   936 \ {\isaliteral{28}{\isacharparenleft}}induct\ n{\isaliteral{29}{\isacharparenright}}\isanewline

   937 \ \ \ \ \isacommand{case}\isamarkupfalse%

   938 \ {\isadigit{0}}\isanewline

   939 \ \ \ \ \isacommand{show}\isamarkupfalse%

   940 \ {\isaliteral{3F}{\isacharquery}}case\ \isacommand{sorry}\isamarkupfalse%

   941 \isanewline

   942 \ \ \isacommand{next}\isamarkupfalse%

   943 \isanewline

   944 \ \ \ \ \isacommand{case}\isamarkupfalse%

   945 \ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\isanewline

   946 \ \ \ \ \isacommand{from}\isamarkupfalse%

   947 \ Suc{\isaliteral{2E}{\isachardot}}hyps\ \isacommand{show}\isamarkupfalse%

   948 \ {\isaliteral{3F}{\isacharquery}}case\ \isacommand{sorry}\isamarkupfalse%

   949 \isanewline

   950 \ \ \isacommand{qed}\isamarkupfalse%

   951 %

   952 \endisatagproof

   953 {\isafoldproof}%

   954 %

   955 \isadelimproof

   956 \isanewline

   957 %

   958 \endisadelimproof

   959 \isacommand{end}\isamarkupfalse%

   960 %

   961 \isamarkupsubsubsection{Example%

   962 }

   963 \isamarkuptrue%

   964 %

   965 \begin{isamarkuptext}%

   966 The subsequent example combines the following proof patterns:

   967   \begin{itemize}

   969   \item outermost induction (over the datatype structure of natural

   970   numbers), to decompose the proof problem in top-down manner

   972   \item calculational reasoning (\secref{sec:calculations-synopsis})

   973   to compose the result in each case

   975   \item solving local claims within the calculation by simplification

   977   \end{itemize}%

   978 \end{isamarkuptext}%

   979 \isamarkuptrue%

   980 \isacommand{lemma}\isamarkupfalse%

   981 \isanewline

   982 \ \ \isakeyword{fixes}\ n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\isanewline

   983 \ \ \isakeyword{shows}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C53756D3E}{\isasymSum}}i{\isaliteral{3D}{\isacharequal}}{\isadigit{0}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}n{\isaliteral{2E}{\isachardot}}\ i{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ n\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ div\ {\isadigit{2}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

   984 %

   985 \isadelimproof

   986 %

   987 \endisadelimproof

   988 %

   989 \isatagproof

   990 \isacommand{proof}\isamarkupfalse%

   991 \ {\isaliteral{28}{\isacharparenleft}}induct\ n{\isaliteral{29}{\isacharparenright}}\isanewline

   992 \ \ \isacommand{case}\isamarkupfalse%

   993 \ {\isadigit{0}}\isanewline

   994 \ \ \isacommand{have}\isamarkupfalse%

   995 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C53756D3E}{\isasymSum}}i{\isaliteral{3D}{\isacharequal}}{\isadigit{0}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isadigit{0}}{\isaliteral{2E}{\isachardot}}\ i{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%

   996 \ simp\isanewline

   997 \ \ \isacommand{also}\isamarkupfalse%

   998 \ \isacommand{have}\isamarkupfalse%

   999 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ div\ {\isadigit{2}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%

  1000 \ simp\isanewline

  1001 \ \ \isacommand{finally}\isamarkupfalse%

  1002 \ \isacommand{show}\isamarkupfalse%

  1003 \ {\isaliteral{3F}{\isacharquery}}case\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

  1004 \isanewline

  1005 \isacommand{next}\isamarkupfalse%

  1006 \isanewline

  1007 \ \ \isacommand{case}\isamarkupfalse%

  1008 \ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\isanewline

  1009 \ \ \isacommand{have}\isamarkupfalse%

  1010 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C53756D3E}{\isasymSum}}i{\isaliteral{3D}{\isacharequal}}{\isadigit{0}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}Suc\ n{\isaliteral{2E}{\isachardot}}\ i{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C53756D3E}{\isasymSum}}i{\isaliteral{3D}{\isacharequal}}{\isadigit{0}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}n{\isaliteral{2E}{\isachardot}}\ i{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%

  1011 \ simp\isanewline

  1012 \ \ \isacommand{also}\isamarkupfalse%

  1013 \ \isacommand{have}\isamarkupfalse%

  1014 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ n\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ div\ {\isadigit{2}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%

  1015 \ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ Suc{\isaliteral{2E}{\isachardot}}hyps{\isaliteral{29}{\isacharparenright}}\isanewline

  1016 \ \ \isacommand{also}\isamarkupfalse%

  1017 \ \isacommand{have}\isamarkupfalse%

  1018 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{2}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ div\ {\isadigit{2}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%

  1019 \ simp\isanewline

  1020 \ \ \isacommand{also}\isamarkupfalse%

  1021 \ \isacommand{have}\isamarkupfalse%

  1022 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}Suc\ n\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}Suc\ n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ div\ {\isadigit{2}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%

  1023 \ simp\isanewline

  1024 \ \ \isacommand{finally}\isamarkupfalse%

  1025 \ \isacommand{show}\isamarkupfalse%

  1026 \ {\isaliteral{3F}{\isacharquery}}case\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

  1027 \isanewline

  1028 \isacommand{qed}\isamarkupfalse%

  1029 %

  1030 \endisatagproof

  1031 {\isafoldproof}%

  1032 %

  1033 \isadelimproof

  1034 %

  1035 \endisadelimproof

  1036 %

  1037 \begin{isamarkuptext}%

  1038 This demonstrates how induction proofs can be done without

  1039   having to consider the raw Natural Deduction structure.%

  1040 \end{isamarkuptext}%

  1041 \isamarkuptrue%

  1042 %

  1043 \isamarkupsubsection{Induction with local parameters and premises%

  1044 }

  1045 \isamarkuptrue%

  1046 %

  1047 \begin{isamarkuptext}%

  1048 Idea: Pure rule statements are passed through the induction

  1049   rule.  This achieves convenient proof patterns, thanks to some

  1050   internal trickery in the \hyperlink{method.induct}{\mbox{\isa{induct}}} method.

  1052   Important: Using compact HOL formulae with \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}{\isaliteral{22}{\isachardoublequote}}} is a

  1053   well-known anti-pattern! It would produce useless formal noise.%

  1054 \end{isamarkuptext}%

  1055 \isamarkuptrue%

  1056 \isacommand{notepad}\isamarkupfalse%

  1057 \isanewline

  1058 \isakeyword{begin}\isanewline

  1059 %

  1060 \isadelimproof

  1061 \ \ %

  1062 \endisadelimproof

  1063 %

  1064 \isatagproof

  1065 \isacommand{fix}\isamarkupfalse%

  1066 \ n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\isanewline

  1067 \ \ \isacommand{fix}\isamarkupfalse%

  1068 \ P\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  1069 \ \ \isacommand{fix}\isamarkupfalse%

  1070 \ Q\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  1071 \isanewline

  1072 \ \ \isacommand{have}\isamarkupfalse%

  1073 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  1074 \ \ \isacommand{proof}\isamarkupfalse%

  1075 \ {\isaliteral{28}{\isacharparenleft}}induct\ n{\isaliteral{29}{\isacharparenright}}\isanewline

  1076 \ \ \ \ \isacommand{case}\isamarkupfalse%

  1077 \ {\isadigit{0}}\isanewline

  1078 \ \ \ \ \isacommand{show}\isamarkupfalse%

  1079 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

  1080 \isanewline

  1081 \ \ \isacommand{next}\isamarkupfalse%

  1082 \isanewline

  1083 \ \ \ \ \isacommand{case}\isamarkupfalse%

  1084 \ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\isanewline

  1085 \ \ \ \ \isacommand{from}\isamarkupfalse%

  1086 \ {\isaliteral{60}{\isacharbackquoteopen}}P\ n{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse%

  1087 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

  1088 \isanewline

  1089 \ \ \isacommand{qed}\isamarkupfalse%

  1090 \isanewline

  1091 \isanewline

  1092 \ \ \isacommand{have}\isamarkupfalse%

  1093 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  1094 \ \ \isacommand{proof}\isamarkupfalse%

  1095 \ {\isaliteral{28}{\isacharparenleft}}induct\ n{\isaliteral{29}{\isacharparenright}}\isanewline

  1096 \ \ \ \ \isacommand{case}\isamarkupfalse%

  1097 \ {\isadigit{0}}\isanewline

  1098 \ \ \ \ \isacommand{from}\isamarkupfalse%

  1099 \ {\isaliteral{60}{\isacharbackquoteopen}}A\ {\isadigit{0}}{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse%

  1100 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

  1101 \isanewline

  1102 \ \ \isacommand{next}\isamarkupfalse%

  1103 \isanewline

  1104 \ \ \ \ \isacommand{case}\isamarkupfalse%

  1105 \ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\isanewline

  1106 \ \ \ \ \isacommand{from}\isamarkupfalse%

  1107 \ {\isaliteral{60}{\isacharbackquoteopen}}A\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ n{\isaliteral{60}{\isacharbackquoteclose}}\isanewline

  1108 \ \ \ \ \ \ \isakeyword{and}\ {\isaliteral{60}{\isacharbackquoteopen}}A\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse%

  1109 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

  1110 \isanewline

  1111 \ \ \isacommand{qed}\isamarkupfalse%

  1112 \isanewline

  1113 \isanewline

  1114 \ \ \isacommand{have}\isamarkupfalse%

  1115 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ Q\ x\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  1116 \ \ \isacommand{proof}\isamarkupfalse%

  1117 \ {\isaliteral{28}{\isacharparenleft}}induct\ n{\isaliteral{29}{\isacharparenright}}\isanewline

  1118 \ \ \ \ \isacommand{case}\isamarkupfalse%

  1119 \ {\isadigit{0}}\isanewline

  1120 \ \ \ \ \isacommand{show}\isamarkupfalse%

  1121 \ {\isaliteral{22}{\isachardoublequoteopen}}Q\ x\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

  1122 \isanewline

  1123 \ \ \isacommand{next}\isamarkupfalse%

  1124 \isanewline

  1125 \ \ \ \ \isacommand{case}\isamarkupfalse%

  1126 \ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\isanewline

  1127 \ \ \ \ \isacommand{from}\isamarkupfalse%

  1128 \ {\isaliteral{60}{\isacharbackquoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ Q\ x\ n{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse%

  1129 \ {\isaliteral{22}{\isachardoublequoteopen}}Q\ x\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

  1130 %

  1131 \begin{isamarkuptxt}%

  1132 Local quantification admits arbitrary instances:%

  1133 \end{isamarkuptxt}%

  1134 \isamarkuptrue%

  1135 \ \ \ \ \isacommand{note}\isamarkupfalse%

  1136 \ {\isaliteral{60}{\isacharbackquoteopen}}Q\ a\ n{\isaliteral{60}{\isacharbackquoteclose}}\ \isakeyword{and}\ {\isaliteral{60}{\isacharbackquoteopen}}Q\ b\ n{\isaliteral{60}{\isacharbackquoteclose}}\isanewline

  1137 \ \ \isacommand{qed}\isamarkupfalse%

  1138 %

  1139 \endisatagproof

  1140 {\isafoldproof}%

  1141 %

  1142 \isadelimproof

  1143 \isanewline

  1144 %

  1145 \endisadelimproof

  1146 \isacommand{end}\isamarkupfalse%

  1147 %

  1148 \isamarkupsubsection{Implicit induction context%

  1149 }

  1150 \isamarkuptrue%

  1151 %

  1152 \begin{isamarkuptext}%

  1153 The \hyperlink{method.induct}{\mbox{\isa{induct}}} method can isolate local parameters and

  1154   premises directly from the given statement.  This is convenient in

  1155   practical applications, but requires some understanding of what is

  1156   going on internally (as explained above).%

  1157 \end{isamarkuptext}%

  1158 \isamarkuptrue%

  1159 \isacommand{notepad}\isamarkupfalse%

  1160 \isanewline

  1161 \isakeyword{begin}\isanewline

  1162 %

  1163 \isadelimproof

  1164 \ \ %

  1165 \endisadelimproof

  1166 %

  1167 \isatagproof

  1168 \isacommand{fix}\isamarkupfalse%

  1169 \ n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\isanewline

  1170 \ \ \isacommand{fix}\isamarkupfalse%

  1171 \ Q\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  1172 \isanewline

  1173 \ \ \isacommand{fix}\isamarkupfalse%

  1174 \ x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\isanewline

  1175 \ \ \isacommand{assume}\isamarkupfalse%

  1176 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ x\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  1177 \ \ \isacommand{then}\isamarkupfalse%

  1178 \ \isacommand{have}\isamarkupfalse%

  1179 \ {\isaliteral{22}{\isachardoublequoteopen}}Q\ x\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  1180 \ \ \isacommand{proof}\isamarkupfalse%

  1181 \ {\isaliteral{28}{\isacharparenleft}}induct\ n\ arbitrary{\isaliteral{3A}{\isacharcolon}}\ x{\isaliteral{29}{\isacharparenright}}\isanewline

  1182 \ \ \ \ \isacommand{case}\isamarkupfalse%

  1183 \ {\isadigit{0}}\isanewline

  1184 \ \ \ \ \isacommand{from}\isamarkupfalse%

  1185 \ {\isaliteral{60}{\isacharbackquoteopen}}A\ x\ {\isadigit{0}}{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse%

  1186 \ {\isaliteral{22}{\isachardoublequoteopen}}Q\ x\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

  1187 \isanewline

  1188 \ \ \isacommand{next}\isamarkupfalse%

  1189 \isanewline

  1190 \ \ \ \ \isacommand{case}\isamarkupfalse%

  1191 \ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\isanewline

  1192 \ \ \ \ \isacommand{from}\isamarkupfalse%

  1193 \ {\isaliteral{60}{\isacharbackquoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ A\ x\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q\ x\ n{\isaliteral{60}{\isacharbackquoteclose}}\ \ %

  1194 \isamarkupcmt{arbitrary instances can be produced here%

  1195 }

  1196 \isanewline

  1197 \ \ \ \ \ \ \isakeyword{and}\ {\isaliteral{60}{\isacharbackquoteopen}}A\ x\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse%

  1198 \ {\isaliteral{22}{\isachardoublequoteopen}}Q\ x\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

  1199 \isanewline

  1200 \ \ \isacommand{qed}\isamarkupfalse%

  1201 %

  1202 \endisatagproof

  1203 {\isafoldproof}%

  1204 %

  1205 \isadelimproof

  1206 \isanewline

  1207 %

  1208 \endisadelimproof

  1209 \isacommand{end}\isamarkupfalse%

  1210 %

  1211 \isamarkupsubsection{Advanced induction with term definitions%

  1212 }

  1213 \isamarkuptrue%

  1214 %

  1215 \begin{isamarkuptext}%

  1216 Induction over subexpressions of a certain shape are delicate

  1217   to formalize.  The Isar \hyperlink{method.induct}{\mbox{\isa{induct}}} method provides

  1218   infrastructure for this.

  1220   Idea: sub-expressions of the problem are turned into a defined

  1221   induction variable; often accompanied with fixing of auxiliary

  1222   parameters in the original expression.%

  1223 \end{isamarkuptext}%

  1224 \isamarkuptrue%

  1225 \isacommand{notepad}\isamarkupfalse%

  1226 \isanewline

  1227 \isakeyword{begin}\isanewline

  1228 %

  1229 \isadelimproof

  1230 \ \ %

  1231 \endisadelimproof

  1232 %

  1233 \isatagproof

  1234 \isacommand{fix}\isamarkupfalse%

  1235 \ a\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  1236 \ \ \isacommand{fix}\isamarkupfalse%

  1237 \ A\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  1238 \isanewline

  1239 \ \ \isacommand{assume}\isamarkupfalse%

  1240 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{28}{\isacharparenleft}}a\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  1241 \ \ \isacommand{then}\isamarkupfalse%

  1242 \ \isacommand{have}\isamarkupfalse%

  1243 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{28}{\isacharparenleft}}a\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  1244 \ \ \isacommand{proof}\isamarkupfalse%

  1245 \ {\isaliteral{28}{\isacharparenleft}}induct\ {\isaliteral{22}{\isachardoublequoteopen}}a\ x{\isaliteral{22}{\isachardoublequoteclose}}\ arbitrary{\isaliteral{3A}{\isacharcolon}}\ x{\isaliteral{29}{\isacharparenright}}\isanewline

  1246 \ \ \ \ \isacommand{case}\isamarkupfalse%

  1247 \ {\isadigit{0}}\isanewline

  1248 \ \ \ \ \isacommand{note}\isamarkupfalse%

  1249 \ prem\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{60}{\isacharbackquoteopen}}A\ {\isaliteral{28}{\isacharparenleft}}a\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{60}{\isacharbackquoteclose}}\isanewline

  1250 \ \ \ \ \ \ \isakeyword{and}\ defn\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{60}{\isacharbackquoteopen}}{\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ a\ x{\isaliteral{60}{\isacharbackquoteclose}}\isanewline

  1251 \ \ \ \ \isacommand{show}\isamarkupfalse%

  1252 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{28}{\isacharparenleft}}a\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

  1253 \isanewline

  1254 \ \ \isacommand{next}\isamarkupfalse%

  1255 \isanewline

  1256 \ \ \ \ \isacommand{case}\isamarkupfalse%

  1257 \ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\isanewline

  1258 \ \ \ \ \isacommand{note}\isamarkupfalse%

  1259 \ hyp\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{60}{\isacharbackquoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ n\ {\isaliteral{3D}{\isacharequal}}\ a\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A\ {\isaliteral{28}{\isacharparenleft}}a\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{28}{\isacharparenleft}}a\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{60}{\isacharbackquoteclose}}\isanewline

  1260 \ \ \ \ \ \ \isakeyword{and}\ prem\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{60}{\isacharbackquoteopen}}A\ {\isaliteral{28}{\isacharparenleft}}a\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{60}{\isacharbackquoteclose}}\isanewline

  1261 \ \ \ \ \ \ \isakeyword{and}\ defn\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{60}{\isacharbackquoteopen}}Suc\ n\ {\isaliteral{3D}{\isacharequal}}\ a\ x{\isaliteral{60}{\isacharbackquoteclose}}\isanewline

  1262 \ \ \ \ \isacommand{show}\isamarkupfalse%

  1263 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{28}{\isacharparenleft}}a\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

  1264 \isanewline

  1265 \ \ \isacommand{qed}\isamarkupfalse%

  1266 %

  1267 \endisatagproof

  1268 {\isafoldproof}%

  1269 %

  1270 \isadelimproof

  1271 \isanewline

  1272 %

  1273 \endisadelimproof

  1274 \isacommand{end}\isamarkupfalse%

  1275 %

  1276 \isamarkupsection{Natural Deduction \label{sec:natural-deduction-synopsis}%

  1277 }

  1278 \isamarkuptrue%

  1279 %

  1280 \isamarkupsubsection{Rule statements%

  1281 }

  1282 \isamarkuptrue%

  1283 %

  1284 \begin{isamarkuptext}%

  1285 Isabelle/Pure ``theorems'' are always natural deduction rules,

  1286   which sometimes happen to consist of a conclusion only.

  1288   The framework connectives \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{22}{\isachardoublequote}}} indicate the

  1289   rule structure declaratively.  For example:%

  1290 \end{isamarkuptext}%

  1291 \isamarkuptrue%

  1292 \isacommand{thm}\isamarkupfalse%

  1293 \ conjI\isanewline

  1294 \isacommand{thm}\isamarkupfalse%

  1295 \ impI\isanewline

  1296 \isacommand{thm}\isamarkupfalse%

  1297 \ nat{\isaliteral{2E}{\isachardot}}induct%

  1298 \begin{isamarkuptext}%

  1299 The object-logic is embedded into the Pure framework via an implicit

  1300   derivability judgment \isa{{\isaliteral{22}{\isachardoublequote}}Trueprop\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ bool\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ prop{\isaliteral{22}{\isachardoublequote}}}.

  1302   Thus any HOL formulae appears atomic to the Pure framework, while

  1303   the rule structure outlines the corresponding proof pattern.

  1305   This can be made explicit as follows:%

  1306 \end{isamarkuptext}%

  1307 \isamarkuptrue%

  1308 \isacommand{notepad}\isamarkupfalse%

  1309 \isanewline

  1310 \isakeyword{begin}\isanewline

  1311 %

  1312 \isadelimproof

  1313 \ \ %

  1314 \endisadelimproof

  1315 %

  1316 \isatagproof

  1317 \isacommand{write}\isamarkupfalse%

  1318 \ Trueprop\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}Tr{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}%

  1319 \endisatagproof

  1320 {\isafoldproof}%

  1321 %

  1322 \isadelimproof

  1323 \isanewline

  1324 %

  1325 \endisadelimproof

  1326 \isanewline

  1327 \ \ \isacommand{thm}\isamarkupfalse%

  1328 \ conjI\isanewline

  1329 \ \ \isacommand{thm}\isamarkupfalse%

  1330 \ impI\isanewline

  1331 \ \ \isacommand{thm}\isamarkupfalse%

  1332 \ nat{\isaliteral{2E}{\isachardot}}induct\isanewline

  1333 \isacommand{end}\isamarkupfalse%

  1334 %

  1335 \begin{isamarkuptext}%

  1336 Isar provides first-class notation for rule statements as follows.%

  1337 \end{isamarkuptext}%

  1338 \isamarkuptrue%

  1339 \isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}\isamarkupfalse%

  1340 \ conjI\isanewline

  1341 \isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}\isamarkupfalse%

  1342 \ impI\isanewline

  1343 \isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}\isamarkupfalse%

  1344 \ nat{\isaliteral{2E}{\isachardot}}induct%

  1345 \isamarkupsubsubsection{Examples%

  1346 }

  1347 \isamarkuptrue%

  1348 %

  1349 \begin{isamarkuptext}%

  1350 Introductions and eliminations of some standard connectives of

  1351   the object-logic can be written as rule statements as follows.  (The

  1352   proof ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\hyperlink{method.blast}{\mbox{\isa{blast}}}'' serves as sanity check.)%

  1353 \end{isamarkuptext}%

  1354 \isamarkuptrue%

  1355 \isacommand{lemma}\isamarkupfalse%

  1356 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ False{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P{\isaliteral{22}{\isachardoublequoteclose}}%

  1357 \isadelimproof

  1358 \ %

  1359 \endisadelimproof

  1360 %

  1361 \isatagproof

  1362 \isacommand{by}\isamarkupfalse%

  1363 \ blast%

  1364 \endisatagproof

  1365 {\isafoldproof}%

  1366 %

  1367 \isadelimproof

  1368 %

  1369 \endisadelimproof

  1370 \isanewline

  1371 \isacommand{lemma}\isamarkupfalse%

  1372 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q{\isaliteral{22}{\isachardoublequoteclose}}%

  1373 \isadelimproof

  1374 \ %

  1375 \endisadelimproof

  1376 %

  1377 \isatagproof

  1378 \isacommand{by}\isamarkupfalse%

  1379 \ blast%

  1380 \endisatagproof

  1381 {\isafoldproof}%

  1382 %

  1383 \isadelimproof

  1384 %

  1385 \endisadelimproof

  1386 \isanewline

  1387 \isanewline

  1388 \isacommand{lemma}\isamarkupfalse%

  1389 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q{\isaliteral{22}{\isachardoublequoteclose}}%

  1390 \isadelimproof

  1391 \ %

  1392 \endisadelimproof

  1393 %

  1394 \isatagproof

  1395 \isacommand{by}\isamarkupfalse%

  1396 \ blast%

  1397 \endisatagproof

  1398 {\isafoldproof}%

  1399 %

  1400 \isadelimproof

  1401 %

  1402 \endisadelimproof

  1403 \isanewline

  1404 \isacommand{lemma}\isamarkupfalse%

  1405 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{22}{\isachardoublequoteclose}}%

  1406 \isadelimproof

  1407 \ %

  1408 \endisadelimproof

  1409 %

  1410 \isatagproof

  1411 \isacommand{by}\isamarkupfalse%

  1412 \ blast%

  1413 \endisatagproof

  1414 {\isafoldproof}%

  1415 %

  1416 \isadelimproof

  1417 %

  1418 \endisadelimproof

  1419 \isanewline

  1420 \isanewline

  1421 \isacommand{lemma}\isamarkupfalse%

  1422 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q{\isaliteral{22}{\isachardoublequoteclose}}%

  1423 \isadelimproof

  1424 \ %

  1425 \endisadelimproof

  1426 %

  1427 \isatagproof

  1428 \isacommand{by}\isamarkupfalse%

  1429 \ blast%

  1430 \endisatagproof

  1431 {\isafoldproof}%

  1432 %

  1433 \isadelimproof

  1434 %

  1435 \endisadelimproof

  1436 \isanewline

  1437 \isacommand{lemma}\isamarkupfalse%

  1438 \ {\isaliteral{22}{\isachardoublequoteopen}}Q\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q{\isaliteral{22}{\isachardoublequoteclose}}%

  1439 \isadelimproof

  1440 \ %

  1441 \endisadelimproof

  1442 %

  1443 \isatagproof

  1444 \isacommand{by}\isamarkupfalse%

  1445 \ blast%

  1446 \endisatagproof

  1447 {\isafoldproof}%

  1448 %

  1449 \isadelimproof

  1450 %

  1451 \endisadelimproof

  1452 \isanewline

  1453 \isacommand{lemma}\isamarkupfalse%

  1454 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}Q\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{22}{\isachardoublequoteclose}}%

  1455 \isadelimproof

  1456 \ %

  1457 \endisadelimproof

  1458 %

  1459 \isatagproof

  1460 \isacommand{by}\isamarkupfalse%

  1461 \ blast%

  1462 \endisatagproof

  1463 {\isafoldproof}%

  1464 %

  1465 \isadelimproof

  1466 %

  1467 \endisadelimproof

  1468 \isanewline

  1469 \isanewline

  1470 \isacommand{lemma}\isamarkupfalse%

  1471 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%

  1472 \isadelimproof

  1473 \ %

  1474 \endisadelimproof

  1475 %

  1476 \isatagproof

  1477 \isacommand{by}\isamarkupfalse%

  1478 \ blast%

  1479 \endisatagproof

  1480 {\isafoldproof}%

  1481 %

  1482 \isadelimproof

  1483 %

  1484 \endisadelimproof

  1485 \isanewline

  1486 \isacommand{lemma}\isamarkupfalse%

  1487 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ x{\isaliteral{22}{\isachardoublequoteclose}}%

  1488 \isadelimproof

  1489 \ %

  1490 \endisadelimproof

  1491 %

  1492 \isatagproof

  1493 \isacommand{by}\isamarkupfalse%

  1494 \ blast%

  1495 \endisatagproof

  1496 {\isafoldproof}%

  1497 %

  1498 \isadelimproof

  1499 %

  1500 \endisadelimproof

  1501 \isanewline

  1502 \isanewline

  1503 \isacommand{lemma}\isamarkupfalse%

  1504 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%

  1505 \isadelimproof

  1506 \ %

  1507 \endisadelimproof

  1508 %

  1509 \isatagproof

  1510 \isacommand{by}\isamarkupfalse%

  1511 \ blast%

  1512 \endisatagproof

  1513 {\isafoldproof}%

  1514 %

  1515 \isadelimproof

  1516 %

  1517 \endisadelimproof

  1518 \isanewline

  1519 \isacommand{lemma}\isamarkupfalse%

  1520 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ P\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{22}{\isachardoublequoteclose}}%

  1521 \isadelimproof

  1522 \ %

  1523 \endisadelimproof

  1524 %

  1525 \isatagproof

  1526 \isacommand{by}\isamarkupfalse%

  1527 \ blast%

  1528 \endisatagproof

  1529 {\isafoldproof}%

  1530 %

  1531 \isadelimproof

  1532 %

  1533 \endisadelimproof

  1534 \isanewline

  1535 \isanewline

  1536 \isacommand{lemma}\isamarkupfalse%

  1537 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ B{\isaliteral{22}{\isachardoublequoteclose}}%

  1538 \isadelimproof

  1539 \ %

  1540 \endisadelimproof

  1541 %

  1542 \isatagproof

  1543 \isacommand{by}\isamarkupfalse%

  1544 \ blast%

  1545 \endisatagproof

  1546 {\isafoldproof}%

  1547 %

  1548 \isadelimproof

  1549 %

  1550 \endisadelimproof

  1551 \isanewline

  1552 \isacommand{lemma}\isamarkupfalse%

  1553 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{22}{\isachardoublequoteclose}}%

  1554 \isadelimproof

  1555 \ %

  1556 \endisadelimproof

  1557 %

  1558 \isatagproof

  1559 \isacommand{by}\isamarkupfalse%

  1560 \ blast%

  1561 \endisatagproof

  1562 {\isafoldproof}%

  1563 %

  1564 \isadelimproof

  1565 %

  1566 \endisadelimproof

  1567 \isanewline

  1568 \isanewline

  1569 \isacommand{lemma}\isamarkupfalse%

  1570 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ B{\isaliteral{22}{\isachardoublequoteclose}}%

  1571 \isadelimproof

  1572 \ %

  1573 \endisadelimproof

  1574 %

  1575 \isatagproof

  1576 \isacommand{by}\isamarkupfalse%

  1577 \ blast%

  1578 \endisatagproof

  1579 {\isafoldproof}%

  1580 %

  1581 \isadelimproof

  1582 %

  1583 \endisadelimproof

  1584 \isanewline

  1585 \isacommand{lemma}\isamarkupfalse%

  1586 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ B{\isaliteral{22}{\isachardoublequoteclose}}%

  1587 \isadelimproof

  1588 \ %

  1589 \endisadelimproof

  1590 %

  1591 \isatagproof

  1592 \isacommand{by}\isamarkupfalse%

  1593 \ blast%

  1594 \endisatagproof

  1595 {\isafoldproof}%

  1596 %

  1597 \isadelimproof

  1598 %

  1599 \endisadelimproof

  1600 \isanewline

  1601 \isacommand{lemma}\isamarkupfalse%

  1602 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{22}{\isachardoublequoteclose}}%

  1603 \isadelimproof

  1604 \ %

  1605 \endisadelimproof

  1606 %

  1607 \isatagproof

  1608 \isacommand{by}\isamarkupfalse%

  1609 \ blast%

  1610 \endisatagproof

  1611 {\isafoldproof}%

  1612 %

  1613 \isadelimproof

  1614 %

  1615 \endisadelimproof

  1616 %

  1617 \isamarkupsubsection{Isar context elements%

  1618 }

  1619 \isamarkuptrue%

  1620 %

  1621 \begin{isamarkuptext}%

  1622 We derive some results out of the blue, using Isar context

  1623   elements and some explicit blocks.  This illustrates their meaning

  1624   wrt.\ Pure connectives, without goal states getting in the way.%

  1625 \end{isamarkuptext}%

  1626 \isamarkuptrue%

  1627 \isacommand{notepad}\isamarkupfalse%

  1628 \isanewline

  1629 \isakeyword{begin}\isanewline

  1630 %

  1631 \isadelimproof

  1632 \ \ %

  1633 \endisadelimproof

  1634 %

  1635 \isatagproof

  1636 \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%

  1637 \isanewline

  1638 \ \ \ \ \isacommand{fix}\isamarkupfalse%

  1639 \ x\isanewline

  1640 \ \ \ \ \isacommand{have}\isamarkupfalse%

  1641 \ {\isaliteral{22}{\isachardoublequoteopen}}B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

  1642 \isanewline

  1643 \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%

  1644 \isanewline

  1645 \ \ \isacommand{have}\isamarkupfalse%

  1646 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%

  1647 \ fact\isanewline

  1648 \isanewline

  1649 \isacommand{next}\isamarkupfalse%

  1650 \isanewline

  1651 \isanewline

  1652 \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%

  1653 \isanewline

  1654 \ \ \ \ \isacommand{assume}\isamarkupfalse%

  1655 \ A\isanewline

  1656 \ \ \ \ \isacommand{have}\isamarkupfalse%

  1657 \ B\ \isacommand{sorry}\isamarkupfalse%

  1658 \isanewline

  1659 \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%

  1660 \isanewline

  1661 \ \ \isacommand{have}\isamarkupfalse%

  1662 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%

  1663 \ fact\isanewline

  1664 \isanewline

  1665 \isacommand{next}\isamarkupfalse%

  1666 \isanewline

  1667 \isanewline

  1668 \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%

  1669 \isanewline

  1670 \ \ \ \ \isacommand{def}\isamarkupfalse%

  1671 \ x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t\isanewline

  1672 \ \ \ \ \isacommand{have}\isamarkupfalse%

  1673 \ {\isaliteral{22}{\isachardoublequoteopen}}B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

  1674 \isanewline

  1675 \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%

  1676 \isanewline

  1677 \ \ \isacommand{have}\isamarkupfalse%

  1678 \ {\isaliteral{22}{\isachardoublequoteopen}}B\ t{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%

  1679 \ fact\isanewline

  1680 \isanewline

  1681 \isacommand{next}\isamarkupfalse%

  1682 \isanewline

  1683 \isanewline

  1684 \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%

  1685 \isanewline

  1686 \ \ \ \ \isacommand{obtain}\isamarkupfalse%

  1687 \ x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

  1688 \isanewline

  1689 \ \ \ \ \isacommand{have}\isamarkupfalse%

  1690 \ C\ \isacommand{sorry}\isamarkupfalse%

  1691 \isanewline

  1692 \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%

  1693 \isanewline

  1694 \ \ \isacommand{have}\isamarkupfalse%

  1695 \ C\ \isacommand{by}\isamarkupfalse%

  1696 \ fact%

  1697 \endisatagproof

  1698 {\isafoldproof}%

  1699 %

  1700 \isadelimproof

  1701 \isanewline

  1702 %

  1703 \endisadelimproof

  1704 \isanewline

  1705 \isacommand{end}\isamarkupfalse%

  1706 %

  1707 \isamarkupsubsection{Pure rule composition%

  1708 }

  1709 \isamarkuptrue%

  1710 %

  1711 \begin{isamarkuptext}%

  1712 The Pure framework provides means for:

  1714   \begin{itemize}

  1716     \item backward-chaining of rules by \hyperlink{inference.resolution}{\mbox{\isa{resolution}}}

  1718     \item closing of branches by \hyperlink{inference.assumption}{\mbox{\isa{assumption}}}

  1720   \end{itemize}

  1722   Both principles involve higher-order unification of \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}}-terms

  1723   modulo \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C626574613E}{\isasymbeta}}{\isaliteral{5C3C6574613E}{\isasymeta}}{\isaliteral{22}{\isachardoublequote}}}-equivalence (cf.\ Huet and Miller).%

  1724 \end{isamarkuptext}%

  1725 \isamarkuptrue%

  1726 \isacommand{notepad}\isamarkupfalse%

  1727 \isanewline

  1728 \isakeyword{begin}\isanewline

  1729 %

  1730 \isadelimproof

  1731 \ \ %

  1732 \endisadelimproof

  1733 %

  1734 \isatagproof

  1735 \isacommand{assume}\isamarkupfalse%

  1736 \ a{\isaliteral{3A}{\isacharcolon}}\ A\ \isakeyword{and}\ b{\isaliteral{3A}{\isacharcolon}}\ B%

  1737 \endisatagproof

  1738 {\isafoldproof}%

  1739 %

  1740 \isadelimproof

  1741 \isanewline

  1742 %

  1743 \endisadelimproof

  1744 \ \ \isacommand{thm}\isamarkupfalse%

  1745 \ conjI\isanewline

  1746 \ \ \isacommand{thm}\isamarkupfalse%

  1747 \ conjI\ {\isaliteral{5B}{\isacharbrackleft}}of\ A\ B{\isaliteral{5D}{\isacharbrackright}}\ \ %

  1748 \isamarkupcmt{instantiation%

  1749 }

  1750 \isanewline

  1751 \ \ \isacommand{thm}\isamarkupfalse%

  1752 \ conjI\ {\isaliteral{5B}{\isacharbrackleft}}of\ A\ B{\isaliteral{2C}{\isacharcomma}}\ OF\ a\ b{\isaliteral{5D}{\isacharbrackright}}\ \ %

  1753 \isamarkupcmt{instantiation and composition%

  1754 }

  1755 \isanewline

  1756 \ \ \isacommand{thm}\isamarkupfalse%

  1757 \ conjI\ {\isaliteral{5B}{\isacharbrackleft}}OF\ a\ b{\isaliteral{5D}{\isacharbrackright}}\ \ %

  1758 \isamarkupcmt{composition via unification (trivial)%

  1759 }

  1760 \isanewline

  1761 \ \ \isacommand{thm}\isamarkupfalse%

  1762 \ conjI\ {\isaliteral{5B}{\isacharbrackleft}}OF\ {\isaliteral{60}{\isacharbackquoteopen}}A{\isaliteral{60}{\isacharbackquoteclose}}\ {\isaliteral{60}{\isacharbackquoteopen}}B{\isaliteral{60}{\isacharbackquoteclose}}{\isaliteral{5D}{\isacharbrackright}}\isanewline

  1763 \isanewline

  1764 \ \ \isacommand{thm}\isamarkupfalse%

  1765 \ conjI\ {\isaliteral{5B}{\isacharbrackleft}}OF\ disjI{\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}\isanewline

  1766 \isacommand{end}\isamarkupfalse%

  1767 %

  1768 \begin{isamarkuptext}%

  1769 Note: Low-level rule composition is tedious and leads to

  1770   unreadable~/ unmaintainable expressions in the text.%

  1771 \end{isamarkuptext}%

  1772 \isamarkuptrue%

  1773 %

  1774 \isamarkupsubsection{Structured backward reasoning%

  1775 }

  1776 \isamarkuptrue%

  1777 %

  1778 \begin{isamarkuptext}%

  1779 Idea: Canonical proof decomposition via \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~/

  1780   \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~/ \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}, where the body produces a

  1781   natural deduction rule to refine some goal.%

  1782 \end{isamarkuptext}%

  1783 \isamarkuptrue%

  1784 \isacommand{notepad}\isamarkupfalse%

  1785 \isanewline

  1786 \isakeyword{begin}\isanewline

  1787 %

  1788 \isadelimproof

  1789 \ \ %

  1790 \endisadelimproof

  1791 %

  1792 \isatagproof

  1793 \isacommand{fix}\isamarkupfalse%

  1794 \ A\ B\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  1795 \isanewline

  1796 \ \ \isacommand{have}\isamarkupfalse%

  1797 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ A\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  1798 \ \ \isacommand{proof}\isamarkupfalse%

  1799 \ {\isaliteral{2D}{\isacharminus}}\isanewline

  1800 \ \ \ \ \isacommand{fix}\isamarkupfalse%

  1801 \ x\isanewline

  1802 \ \ \ \ \isacommand{assume}\isamarkupfalse%

  1803 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  1804 \ \ \ \ \isacommand{show}\isamarkupfalse%

  1805 \ {\isaliteral{22}{\isachardoublequoteopen}}B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

  1806 \isanewline

  1807 \ \ \isacommand{qed}\isamarkupfalse%

  1808 \isanewline

  1809 \isanewline

  1810 \ \ \isacommand{have}\isamarkupfalse%

  1811 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ A\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  1812 \ \ \isacommand{proof}\isamarkupfalse%

  1813 \ {\isaliteral{2D}{\isacharminus}}\isanewline

  1814 \ \ \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%

  1815 \isanewline

  1816 \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%

  1817 \ x\isanewline

  1818 \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%

  1819 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  1820 \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%

  1821 \ {\isaliteral{22}{\isachardoublequoteopen}}B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

  1822 \isanewline

  1823 \ \ \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%

  1824 \ %

  1825 \isamarkupcmt{implicit block structure made explicit%

  1826 }

  1827 \isanewline

  1828 \ \ \ \ \isacommand{note}\isamarkupfalse%

  1829 \ {\isaliteral{60}{\isacharbackquoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ A\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ x{\isaliteral{60}{\isacharbackquoteclose}}\isanewline

  1830 \ \ \ \ \ \ %

  1831 \isamarkupcmt{side exit for the resulting rule%

  1832 }

  1833 \isanewline

  1834 \ \ \isacommand{qed}\isamarkupfalse%

  1835 %

  1836 \endisatagproof

  1837 {\isafoldproof}%

  1838 %

  1839 \isadelimproof

  1840 \isanewline

  1841 %

  1842 \endisadelimproof

  1843 \isacommand{end}\isamarkupfalse%

  1844 %

  1845 \isamarkupsubsection{Structured rule application%

  1846 }

  1847 \isamarkuptrue%

  1848 %

  1849 \begin{isamarkuptext}%

  1850 Idea: Previous facts and new claims are composed with a rule from

  1851   the context (or background library).%

  1852 \end{isamarkuptext}%

  1853 \isamarkuptrue%

  1854 \isacommand{notepad}\isamarkupfalse%

  1855 \isanewline

  1856 \isakeyword{begin}\isanewline

  1857 %

  1858 \isadelimproof

  1859 \ \ %

  1860 \endisadelimproof

  1861 %

  1862 \isatagproof

  1863 \isacommand{assume}\isamarkupfalse%

  1864 \ r{\isadigit{1}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isaliteral{22}{\isachardoublequoteclose}}\ \ %

  1865 \isamarkupcmt{simple rule (Horn clause)%

  1866 }

  1867 \isanewline

  1868 \isanewline

  1869 \ \ \isacommand{have}\isamarkupfalse%

  1870 \ A\ \isacommand{sorry}\isamarkupfalse%

  1871 \ \ %

  1872 \isamarkupcmt{prefix of facts via outer sub-proof%

  1873 }

  1874 \isanewline

  1875 \ \ \isacommand{then}\isamarkupfalse%

  1876 \ \isacommand{have}\isamarkupfalse%

  1877 \ C\isanewline

  1878 \ \ \isacommand{proof}\isamarkupfalse%

  1879 \ {\isaliteral{28}{\isacharparenleft}}rule\ r{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\isanewline

  1880 \ \ \ \ \isacommand{show}\isamarkupfalse%

  1881 \ B\ \isacommand{sorry}\isamarkupfalse%

  1882 \ \ %

  1883 \isamarkupcmt{remaining rule premises via inner sub-proof%

  1884 }

  1885 \isanewline

  1886 \ \ \isacommand{qed}\isamarkupfalse%

  1887 \isanewline

  1888 \isanewline

  1889 \ \ \isacommand{have}\isamarkupfalse%

  1890 \ C\isanewline

  1891 \ \ \isacommand{proof}\isamarkupfalse%

  1892 \ {\isaliteral{28}{\isacharparenleft}}rule\ r{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\isanewline

  1893 \ \ \ \ \isacommand{show}\isamarkupfalse%

  1894 \ A\ \isacommand{sorry}\isamarkupfalse%

  1895 \isanewline

  1896 \ \ \ \ \isacommand{show}\isamarkupfalse%

  1897 \ B\ \isacommand{sorry}\isamarkupfalse%

  1898 \isanewline

  1899 \ \ \isacommand{qed}\isamarkupfalse%

  1900 \isanewline

  1901 \isanewline

  1902 \ \ \isacommand{have}\isamarkupfalse%

  1903 \ A\ \isakeyword{and}\ B\ \isacommand{sorry}\isamarkupfalse%

  1904 \isanewline

  1905 \ \ \isacommand{then}\isamarkupfalse%

  1906 \ \isacommand{have}\isamarkupfalse%

  1907 \ C\isanewline

  1908 \ \ \isacommand{proof}\isamarkupfalse%

  1909 \ {\isaliteral{28}{\isacharparenleft}}rule\ r{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\isanewline

  1910 \ \ \isacommand{qed}\isamarkupfalse%

  1911 \isanewline

  1912 \isanewline

  1913 \ \ \isacommand{have}\isamarkupfalse%

  1914 \ A\ \isakeyword{and}\ B\ \isacommand{sorry}\isamarkupfalse%

  1915 \isanewline

  1916 \ \ \isacommand{then}\isamarkupfalse%

  1917 \ \isacommand{have}\isamarkupfalse%

  1918 \ C\ \isacommand{by}\isamarkupfalse%

  1919 \ {\isaliteral{28}{\isacharparenleft}}rule\ r{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\isanewline

  1920 \isanewline

  1921 \isacommand{next}\isamarkupfalse%

  1922 \isanewline

  1923 \isanewline

  1924 \ \ \isacommand{assume}\isamarkupfalse%

  1925 \ r{\isadigit{2}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ B{\isadigit{1}}\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isadigit{2}}\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isaliteral{22}{\isachardoublequoteclose}}\ \ %

  1926 \isamarkupcmt{nested rule%

  1927 }

  1928 \isanewline

  1929 \isanewline

  1930 \ \ \isacommand{have}\isamarkupfalse%

  1931 \ A\ \isacommand{sorry}\isamarkupfalse%

  1932 \isanewline

  1933 \ \ \isacommand{then}\isamarkupfalse%

  1934 \ \isacommand{have}\isamarkupfalse%

  1935 \ C\isanewline

  1936 \ \ \isacommand{proof}\isamarkupfalse%

  1937 \ {\isaliteral{28}{\isacharparenleft}}rule\ r{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\isanewline

  1938 \ \ \ \ \isacommand{fix}\isamarkupfalse%

  1939 \ x\isanewline

  1940 \ \ \ \ \isacommand{assume}\isamarkupfalse%

  1941 \ {\isaliteral{22}{\isachardoublequoteopen}}B{\isadigit{1}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  1942 \ \ \ \ \isacommand{show}\isamarkupfalse%

  1943 \ {\isaliteral{22}{\isachardoublequoteopen}}B{\isadigit{2}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

  1944 \isanewline

  1945 \ \ \isacommand{qed}\isamarkupfalse%

  1946 %

  1947 \begin{isamarkuptxt}%

  1948 The compound rule premise \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ B{\isadigit{1}}\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isadigit{2}}\ x{\isaliteral{22}{\isachardoublequote}}} is better

  1949     addressed via \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~/ \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~/ \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}

  1950     in the nested proof body.%

  1951 \end{isamarkuptxt}%

  1952 \isamarkuptrue%

  1953 %

  1954 \endisatagproof

  1955 {\isafoldproof}%

  1956 %

  1957 \isadelimproof

  1958 %

  1959 \endisadelimproof

  1960 \isacommand{end}\isamarkupfalse%

  1961 %

  1962 \isamarkupsubsection{Example: predicate logic%

  1963 }

  1964 \isamarkuptrue%

  1965 %

  1966 \begin{isamarkuptext}%

  1967 Using the above principles, standard introduction and elimination proofs

  1968   of predicate logic connectives of HOL work as follows.%

  1969 \end{isamarkuptext}%

  1970 \isamarkuptrue%

  1971 \isacommand{notepad}\isamarkupfalse%

  1972 \isanewline

  1973 \isakeyword{begin}\isanewline

  1974 %

  1975 \isadelimproof

  1976 \ \ %

  1977 \endisadelimproof

  1978 %

  1979 \isatagproof

  1980 \isacommand{have}\isamarkupfalse%

  1981 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ A\ \isacommand{sorry}\isamarkupfalse%

  1982 \isanewline

  1983 \ \ \isacommand{then}\isamarkupfalse%

  1984 \ \isacommand{have}\isamarkupfalse%

  1985 \ B\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

  1986 \isanewline

  1987 \isanewline

  1988 \ \ \isacommand{have}\isamarkupfalse%

  1989 \ A\ \isacommand{sorry}\isamarkupfalse%

  1990 \isanewline

  1991 \ \ \isacommand{then}\isamarkupfalse%

  1992 \ \isacommand{have}\isamarkupfalse%

  1993 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

  1994 \isanewline

  1995 \isanewline

  1996 \ \ \isacommand{have}\isamarkupfalse%

  1997 \ B\ \isacommand{sorry}\isamarkupfalse%

  1998 \isanewline

  1999 \ \ \isacommand{then}\isamarkupfalse%

  2000 \ \isacommand{have}\isamarkupfalse%

  2001 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

  2002 \isanewline

  2003 \isanewline

  2004 \ \ \isacommand{have}\isamarkupfalse%

  2005 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

  2006 \isanewline

  2007 \ \ \isacommand{then}\isamarkupfalse%

  2008 \ \isacommand{have}\isamarkupfalse%

  2009 \ C\isanewline

  2010 \ \ \isacommand{proof}\isamarkupfalse%

  2011 \isanewline

  2012 \ \ \ \ \isacommand{assume}\isamarkupfalse%

  2013 \ A\isanewline

  2014 \ \ \ \ \isacommand{then}\isamarkupfalse%

  2015 \ \isacommand{show}\isamarkupfalse%

  2016 \ C\ \isacommand{sorry}\isamarkupfalse%

  2017 \isanewline

  2018 \ \ \isacommand{next}\isamarkupfalse%

  2019 \isanewline

  2020 \ \ \ \ \isacommand{assume}\isamarkupfalse%

  2021 \ B\isanewline

  2022 \ \ \ \ \isacommand{then}\isamarkupfalse%

  2023 \ \isacommand{show}\isamarkupfalse%

  2024 \ C\ \isacommand{sorry}\isamarkupfalse%

  2025 \isanewline

  2026 \ \ \isacommand{qed}\isamarkupfalse%

  2027 \isanewline

  2028 \isanewline

  2029 \ \ \isacommand{have}\isamarkupfalse%

  2030 \ A\ \isakeyword{and}\ B\ \isacommand{sorry}\isamarkupfalse%

  2031 \isanewline

  2032 \ \ \isacommand{then}\isamarkupfalse%

  2033 \ \isacommand{have}\isamarkupfalse%

  2034 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

  2035 \isanewline

  2036 \isanewline

  2037 \ \ \isacommand{have}\isamarkupfalse%

  2038 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

  2039 \isanewline

  2040 \ \ \isacommand{then}\isamarkupfalse%

  2041 \ \isacommand{have}\isamarkupfalse%

  2042 \ A\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

  2043 \isanewline

  2044 \isanewline

  2045 \ \ \isacommand{have}\isamarkupfalse%

  2046 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

  2047 \isanewline

  2048 \ \ \isacommand{then}\isamarkupfalse%

  2049 \ \isacommand{have}\isamarkupfalse%

  2050 \ B\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

  2051 \isanewline

  2052 \isanewline

  2053 \ \ \isacommand{have}\isamarkupfalse%

  2054 \ False\ \isacommand{sorry}\isamarkupfalse%

  2055 \isanewline

  2056 \ \ \isacommand{then}\isamarkupfalse%

  2057 \ \isacommand{have}\isamarkupfalse%

  2058 \ A\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

  2059 \isanewline

  2060 \isanewline

  2061 \ \ \isacommand{have}\isamarkupfalse%

  2062 \ True\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

  2063 \isanewline

  2064 \isanewline

  2065 \ \ \isacommand{have}\isamarkupfalse%

  2066 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  2067 \ \ \isacommand{proof}\isamarkupfalse%

  2068 \isanewline

  2069 \ \ \ \ \isacommand{assume}\isamarkupfalse%

  2070 \ A\isanewline

  2071 \ \ \ \ \isacommand{then}\isamarkupfalse%

  2072 \ \isacommand{show}\isamarkupfalse%

  2073 \ False\ \isacommand{sorry}\isamarkupfalse%

  2074 \isanewline

  2075 \ \ \isacommand{qed}\isamarkupfalse%

  2076 \isanewline

  2077 \isanewline

  2078 \ \ \isacommand{have}\isamarkupfalse%

  2079 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ A\ \isacommand{sorry}\isamarkupfalse%

  2080 \isanewline

  2081 \ \ \isacommand{then}\isamarkupfalse%

  2082 \ \isacommand{have}\isamarkupfalse%

  2083 \ B\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

  2084 \isanewline

  2085 \isanewline

  2086 \ \ \isacommand{have}\isamarkupfalse%

  2087 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  2088 \ \ \isacommand{proof}\isamarkupfalse%

  2089 \isanewline

  2090 \ \ \ \ \isacommand{fix}\isamarkupfalse%

  2091 \ x\isanewline

  2092 \ \ \ \ \isacommand{show}\isamarkupfalse%

  2093 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

  2094 \isanewline

  2095 \ \ \isacommand{qed}\isamarkupfalse%

  2096 \isanewline

  2097 \isanewline

  2098 \ \ \isacommand{have}\isamarkupfalse%

  2099 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

  2100 \isanewline

  2101 \ \ \isacommand{then}\isamarkupfalse%

  2102 \ \isacommand{have}\isamarkupfalse%

  2103 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ a{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

  2104 \isanewline

  2105 \isanewline

  2106 \ \ \isacommand{have}\isamarkupfalse%

  2107 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  2108 \ \ \isacommand{proof}\isamarkupfalse%

  2109 \isanewline

  2110 \ \ \ \ \isacommand{show}\isamarkupfalse%

  2111 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ a{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

  2112 \isanewline

  2113 \ \ \isacommand{qed}\isamarkupfalse%

  2114 \isanewline

  2115 \isanewline

  2116 \ \ \isacommand{have}\isamarkupfalse%

  2117 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

  2118 \isanewline

  2119 \ \ \isacommand{then}\isamarkupfalse%

  2120 \ \isacommand{have}\isamarkupfalse%

  2121 \ C\isanewline

  2122 \ \ \isacommand{proof}\isamarkupfalse%

  2123 \isanewline

  2124 \ \ \ \ \isacommand{fix}\isamarkupfalse%

  2125 \ a\isanewline

  2126 \ \ \ \ \isacommand{assume}\isamarkupfalse%

  2127 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ a{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  2128 \ \ \ \ \isacommand{show}\isamarkupfalse%

  2129 \ C\ \isacommand{sorry}\isamarkupfalse%

  2130 \isanewline

  2131 \ \ \isacommand{qed}\isamarkupfalse%

  2132 %

  2133 \begin{isamarkuptxt}%

  2134 Less awkward version using \hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}}:%

  2135 \end{isamarkuptxt}%

  2136 \isamarkuptrue%

  2137 \ \ \isacommand{have}\isamarkupfalse%

  2138 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

  2139 \isanewline

  2140 \ \ \isacommand{then}\isamarkupfalse%

  2141 \ \isacommand{obtain}\isamarkupfalse%

  2142 \ a\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}P\ a{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

  2143 %

  2144 \endisatagproof

  2145 {\isafoldproof}%

  2146 %

  2147 \isadelimproof

  2148 \isanewline

  2149 %

  2150 \endisadelimproof

  2151 \isacommand{end}\isamarkupfalse%

  2152 %

  2153 \begin{isamarkuptext}%

  2154 Further variations to illustrate Isar sub-proofs involving

  2155   \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}:%

  2156 \end{isamarkuptext}%

  2157 \isamarkuptrue%

  2158 \isacommand{notepad}\isamarkupfalse%

  2159 \isanewline

  2160 \isakeyword{begin}\isanewline

  2161 %

  2162 \isadelimproof

  2163 \ \ %

  2164 \endisadelimproof

  2165 %

  2166 \isatagproof

  2167 \isacommand{have}\isamarkupfalse%

  2168 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  2169 \ \ \isacommand{proof}\isamarkupfalse%

  2170 \ \ %

  2171 \isamarkupcmt{two strictly isolated subproofs%

  2172 }

  2173 \isanewline

  2174 \ \ \ \ \isacommand{show}\isamarkupfalse%

  2175 \ A\ \isacommand{sorry}\isamarkupfalse%

  2176 \isanewline

  2177 \ \ \isacommand{next}\isamarkupfalse%

  2178 \isanewline

  2179 \ \ \ \ \isacommand{show}\isamarkupfalse%

  2180 \ B\ \isacommand{sorry}\isamarkupfalse%

  2181 \isanewline

  2182 \ \ \isacommand{qed}\isamarkupfalse%

  2183 \isanewline

  2184 \isanewline

  2185 \ \ \isacommand{have}\isamarkupfalse%

  2186 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  2187 \ \ \isacommand{proof}\isamarkupfalse%

  2188 \ \ %

  2189 \isamarkupcmt{one simultaneous sub-proof%

  2190 }

  2191 \isanewline

  2192 \ \ \ \ \isacommand{show}\isamarkupfalse%

  2193 \ A\ \isakeyword{and}\ B\ \isacommand{sorry}\isamarkupfalse%

  2194 \isanewline

  2195 \ \ \isacommand{qed}\isamarkupfalse%

  2196 \isanewline

  2197 \isanewline

  2198 \ \ \isacommand{have}\isamarkupfalse%

  2199 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  2200 \ \ \isacommand{proof}\isamarkupfalse%

  2201 \ \ %

  2202 \isamarkupcmt{two subproofs in the same context%

  2203 }

  2204 \isanewline

  2205 \ \ \ \ \isacommand{show}\isamarkupfalse%

  2206 \ A\ \isacommand{sorry}\isamarkupfalse%

  2207 \isanewline

  2208 \ \ \ \ \isacommand{show}\isamarkupfalse%

  2209 \ B\ \isacommand{sorry}\isamarkupfalse%

  2210 \isanewline

  2211 \ \ \isacommand{qed}\isamarkupfalse%

  2212 \isanewline

  2213 \isanewline

  2214 \ \ \isacommand{have}\isamarkupfalse%

  2215 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  2216 \ \ \isacommand{proof}\isamarkupfalse%

  2217 \ \ %

  2218 \isamarkupcmt{swapped order%

  2219 }

  2220 \isanewline

  2221 \ \ \ \ \isacommand{show}\isamarkupfalse%

  2222 \ B\ \isacommand{sorry}\isamarkupfalse%

  2223 \isanewline

  2224 \ \ \ \ \isacommand{show}\isamarkupfalse%

  2225 \ A\ \isacommand{sorry}\isamarkupfalse%

  2226 \isanewline

  2227 \ \ \isacommand{qed}\isamarkupfalse%

  2228 \isanewline

  2229 \isanewline

  2230 \ \ \isacommand{have}\isamarkupfalse%

  2231 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  2232 \ \ \isacommand{proof}\isamarkupfalse%

  2233 \ \ %

  2234 \isamarkupcmt{sequential subproofs%

  2235 }

  2236 \isanewline

  2237 \ \ \ \ \isacommand{show}\isamarkupfalse%

  2238 \ A\ \isacommand{sorry}\isamarkupfalse%

  2239 \isanewline

  2240 \ \ \ \ \isacommand{show}\isamarkupfalse%

  2241 \ B\ \isacommand{using}\isamarkupfalse%

  2242 \ {\isaliteral{60}{\isacharbackquoteopen}}A{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{sorry}\isamarkupfalse%

  2243 \isanewline

  2244 \ \ \isacommand{qed}\isamarkupfalse%

  2245 %

  2246 \endisatagproof

  2247 {\isafoldproof}%

  2248 %

  2249 \isadelimproof

  2250 \isanewline

  2251 %

  2252 \endisadelimproof

  2253 \isacommand{end}\isamarkupfalse%

  2254 %

  2255 \isamarkupsubsubsection{Example: set-theoretic operators%

  2256 }

  2257 \isamarkuptrue%

  2258 %

  2259 \begin{isamarkuptext}%

  2260 There is nothing special about logical connectives (\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616E643E}{\isasymand}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6F723E}{\isasymor}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}{\isaliteral{22}{\isachardoublequote}}} etc.).  Operators from

  2261   set-theory or lattice-theory work analogously.  It is only a matter

  2262   of rule declarations in the library; rules can be also specified

  2263   explicitly.%

  2264 \end{isamarkuptext}%

  2265 \isamarkuptrue%

  2266 \isacommand{notepad}\isamarkupfalse%

  2267 \isanewline

  2268 \isakeyword{begin}\isanewline

  2269 %

  2270 \isadelimproof

  2271 \ \ %

  2272 \endisadelimproof

  2273 %

  2274 \isatagproof

  2275 \isacommand{have}\isamarkupfalse%

  2276 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

  2277 \isanewline

  2278 \ \ \isacommand{then}\isamarkupfalse%

  2279 \ \isacommand{have}\isamarkupfalse%

  2280 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

  2281 \isanewline

  2282 \isanewline

  2283 \ \ \isacommand{have}\isamarkupfalse%

  2284 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

  2285 \isanewline

  2286 \ \ \isacommand{then}\isamarkupfalse%

  2287 \ \isacommand{have}\isamarkupfalse%

  2288 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

  2289 \isanewline

  2290 \isanewline

  2291 \ \ \isacommand{have}\isamarkupfalse%

  2292 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

  2293 \isanewline

  2294 \ \ \isacommand{then}\isamarkupfalse%

  2295 \ \isacommand{have}\isamarkupfalse%

  2296 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

  2297 \isanewline

  2298 \isanewline

  2299 \ \ \isacommand{have}\isamarkupfalse%

  2300 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

  2301 \isanewline

  2302 \ \ \isacommand{then}\isamarkupfalse%

  2303 \ \isacommand{have}\isamarkupfalse%

  2304 \ C\isanewline

  2305 \ \ \isacommand{proof}\isamarkupfalse%

  2306 \isanewline

  2307 \ \ \ \ \isacommand{assume}\isamarkupfalse%

  2308 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  2309 \ \ \ \ \isacommand{then}\isamarkupfalse%

  2310 \ \isacommand{show}\isamarkupfalse%

  2311 \ C\ \isacommand{sorry}\isamarkupfalse%

  2312 \isanewline

  2313 \ \ \isacommand{next}\isamarkupfalse%

  2314 \isanewline

  2315 \ \ \ \ \isacommand{assume}\isamarkupfalse%

  2316 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  2317 \ \ \ \ \isacommand{then}\isamarkupfalse%

  2318 \ \isacommand{show}\isamarkupfalse%

  2319 \ C\ \isacommand{sorry}\isamarkupfalse%

  2320 \isanewline

  2321 \ \ \isacommand{qed}\isamarkupfalse%

  2322 \isanewline

  2323 \isanewline

  2324 \isacommand{next}\isamarkupfalse%

  2325 \isanewline

  2326 \ \ \isacommand{have}\isamarkupfalse%

  2327 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{5C3C496E7465723E}{\isasymInter}}A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  2328 \ \ \isacommand{proof}\isamarkupfalse%

  2329 \isanewline

  2330 \ \ \ \ \isacommand{fix}\isamarkupfalse%

  2331 \ a\isanewline

  2332 \ \ \ \ \isacommand{assume}\isamarkupfalse%

  2333 \ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  2334 \ \ \ \ \isacommand{show}\isamarkupfalse%

  2335 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ a{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

  2336 \isanewline

  2337 \ \ \isacommand{qed}\isamarkupfalse%

  2338 \isanewline

  2339 \isanewline

  2340 \ \ \isacommand{have}\isamarkupfalse%

  2341 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{5C3C496E7465723E}{\isasymInter}}A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

  2342 \isanewline

  2343 \ \ \isacommand{then}\isamarkupfalse%

  2344 \ \isacommand{have}\isamarkupfalse%

  2345 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ a{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  2346 \ \ \isacommand{proof}\isamarkupfalse%

  2347 \isanewline

  2348 \ \ \ \ \isacommand{show}\isamarkupfalse%

  2349 \ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

  2350 \isanewline

  2351 \ \ \isacommand{qed}\isamarkupfalse%

  2352 \isanewline

  2353 \isanewline

  2354 \ \ \isacommand{have}\isamarkupfalse%

  2355 \ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ a{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

  2356 \isanewline

  2357 \ \ \isacommand{then}\isamarkupfalse%

  2358 \ \isacommand{have}\isamarkupfalse%

  2359 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{5C3C556E696F6E3E}{\isasymUnion}}A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

  2360 \isanewline

  2361 \isanewline

  2362 \ \ \isacommand{have}\isamarkupfalse%

  2363 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{5C3C556E696F6E3E}{\isasymUnion}}A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

  2364 \isanewline

  2365 \ \ \isacommand{then}\isamarkupfalse%

  2366 \ \isacommand{obtain}\isamarkupfalse%

  2367 \ a\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ a{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

  2368 %

  2369 \endisatagproof

  2370 {\isafoldproof}%

  2371 %

  2372 \isadelimproof

  2373 \isanewline

  2374 %

  2375 \endisadelimproof

  2376 \isacommand{end}\isamarkupfalse%

  2377 %

  2378 \isamarkupsection{Generalized elimination and cases%

  2379 }

  2380 \isamarkuptrue%

  2381 %

  2382 \isamarkupsubsection{General elimination rules%

  2383 }

  2384 \isamarkuptrue%

  2385 %

  2386 \begin{isamarkuptext}%

  2387 The general format of elimination rules is illustrated by the

  2388   following typical representatives:%

  2389 \end{isamarkuptext}%

  2390 \isamarkuptrue%

  2391 \isacommand{thm}\isamarkupfalse%

  2392 \ exE\ \ \ \ \ %

  2393 \isamarkupcmt{local parameter%

  2394 }

  2395 \isanewline

  2396 \isacommand{thm}\isamarkupfalse%

  2397 \ conjE\ \ \ %

  2398 \isamarkupcmt{local premises%

  2399 }

  2400 \isanewline

  2401 \isacommand{thm}\isamarkupfalse%

  2402 \ disjE\ \ \ %

  2403 \isamarkupcmt{split into cases%

  2404 }

  2405 %

  2406 \begin{isamarkuptext}%

  2407 Combining these characteristics leads to the following general scheme

  2408   for elimination rules with cases:

  2410   \begin{itemize}

  2412   \item prefix of assumptions (or ``major premises'')

  2414   \item one or more cases that enable to establish the main conclusion

  2415     in an augmented context

  2417   \end{itemize}%

  2418 \end{isamarkuptext}%

  2419 \isamarkuptrue%

  2420 \isacommand{notepad}\isamarkupfalse%

  2421 \isanewline

  2422 \isakeyword{begin}\isanewline

  2423 %

  2424 \isadelimproof

  2425 \ \ %

  2426 \endisadelimproof

  2427 %

  2428 \isatagproof

  2429 \isacommand{assume}\isamarkupfalse%

  2430 \ r{\isaliteral{3A}{\isacharcolon}}\isanewline

  2431 \ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}A{\isadigit{1}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A{\isadigit{2}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\ assumptions\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline

  2432 \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x\ y{\isaliteral{2E}{\isachardot}}\ B{\isadigit{1}}\ x\ y\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isadigit{1}}\ x\ y\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\ case\ {\isadigit{1}}\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline

  2433 \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x\ y{\isaliteral{2E}{\isachardot}}\ B{\isadigit{2}}\ x\ y\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isadigit{2}}\ x\ y\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\ case\ {\isadigit{2}}\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline

  2434 \ \ \ \ \ \ R\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\ main\ conclusion\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  2435 \isanewline

  2436 \ \ \isacommand{have}\isamarkupfalse%

  2437 \ A{\isadigit{1}}\ \isakeyword{and}\ A{\isadigit{2}}\ \isacommand{sorry}\isamarkupfalse%

  2438 \isanewline

  2439 \ \ \isacommand{then}\isamarkupfalse%

  2440 \ \isacommand{have}\isamarkupfalse%

  2441 \ R\isanewline

  2442 \ \ \isacommand{proof}\isamarkupfalse%

  2443 \ {\isaliteral{28}{\isacharparenleft}}rule\ r{\isaliteral{29}{\isacharparenright}}\isanewline

  2444 \ \ \ \ \isacommand{fix}\isamarkupfalse%

  2445 \ x\ y\isanewline

  2446 \ \ \ \ \isacommand{assume}\isamarkupfalse%

  2447 \ {\isaliteral{22}{\isachardoublequoteopen}}B{\isadigit{1}}\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ {\isaliteral{22}{\isachardoublequoteopen}}C{\isadigit{1}}\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  2448 \ \ \ \ \isacommand{show}\isamarkupfalse%

  2449 \ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{sorry}\isamarkupfalse%

  2450 \isanewline

  2451 \ \ \isacommand{next}\isamarkupfalse%

  2452 \isanewline

  2453 \ \ \ \ \isacommand{fix}\isamarkupfalse%

  2454 \ x\ y\isanewline

  2455 \ \ \ \ \isacommand{assume}\isamarkupfalse%

  2456 \ {\isaliteral{22}{\isachardoublequoteopen}}B{\isadigit{2}}\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ {\isaliteral{22}{\isachardoublequoteopen}}C{\isadigit{2}}\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  2457 \ \ \ \ \isacommand{show}\isamarkupfalse%

  2458 \ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{sorry}\isamarkupfalse%

  2459 \isanewline

  2460 \ \ \isacommand{qed}\isamarkupfalse%

  2461 %

  2462 \endisatagproof

  2463 {\isafoldproof}%

  2464 %

  2465 \isadelimproof

  2466 \isanewline

  2467 %

  2468 \endisadelimproof

  2469 \isacommand{end}\isamarkupfalse%

  2470 %

  2471 \begin{isamarkuptext}%

  2472 Here \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}thesis{\isaliteral{22}{\isachardoublequote}}} is used to refer to the unchanged goal

  2473   statement.%

  2474 \end{isamarkuptext}%

  2475 \isamarkuptrue%

  2476 %

  2477 \isamarkupsubsection{Rules with cases%

  2478 }

  2479 \isamarkuptrue%

  2480 %

  2481 \begin{isamarkuptext}%

  2482 Applying an elimination rule to some goal, leaves that unchanged

  2483   but allows to augment the context in the sub-proof of each case.

  2485   Isar provides some infrastructure to support this:

  2487   \begin{itemize}

  2489   \item native language elements to state eliminations

  2491   \item symbolic case names

  2493   \item method \hyperlink{method.cases}{\mbox{\isa{cases}}} to recover this structure in a

  2494   sub-proof

  2496   \end{itemize}%

  2497 \end{isamarkuptext}%

  2498 \isamarkuptrue%

  2499 \isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}\isamarkupfalse%

  2500 \ exE\isanewline

  2501 \isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}\isamarkupfalse%

  2502 \ conjE\isanewline

  2503 \isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}\isamarkupfalse%

  2504 \ disjE\isanewline

  2505 \isanewline

  2506 \isacommand{lemma}\isamarkupfalse%

  2507 \isanewline

  2508 \ \ \isakeyword{assumes}\ A{\isadigit{1}}\ \isakeyword{and}\ A{\isadigit{2}}\ \ %

  2509 \isamarkupcmt{assumptions%

  2510 }

  2511 \isanewline

  2512 \ \ \isakeyword{obtains}\isanewline

  2513 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}case{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ \ x\ y\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}B{\isadigit{1}}\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ {\isaliteral{22}{\isachardoublequoteopen}}C{\isadigit{1}}\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  2514 \ \ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{28}{\isacharparenleft}}case{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ \ x\ y\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}B{\isadigit{2}}\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ {\isaliteral{22}{\isachardoublequoteopen}}C{\isadigit{2}}\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  2515 %

  2516 \isadelimproof

  2517 \ \ %

  2518 \endisadelimproof

  2519 %

  2520 \isatagproof

  2521 \isacommand{sorry}\isamarkupfalse%

  2522 %

  2523 \endisatagproof

  2524 {\isafoldproof}%

  2525 %

  2526 \isadelimproof

  2527 %

  2528 \endisadelimproof

  2529 %

  2530 \isamarkupsubsubsection{Example%

  2531 }

  2532 \isamarkuptrue%

  2533 \isacommand{lemma}\isamarkupfalse%

  2534 \ tertium{\isaliteral{5F}{\isacharunderscore}}non{\isaliteral{5F}{\isacharunderscore}}datur{\isaliteral{3A}{\isacharcolon}}\isanewline

  2535 \ \ \isakeyword{obtains}\isanewline

  2536 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}T{\isaliteral{29}{\isacharparenright}}\ \ A\isanewline

  2537 \ \ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{28}{\isacharparenleft}}F{\isaliteral{29}{\isacharparenright}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  2538 %

  2539 \isadelimproof

  2540 \ \ %

  2541 \endisadelimproof

  2542 %

  2543 \isatagproof

  2544 \isacommand{by}\isamarkupfalse%

  2545 \ blast%

  2546 \endisatagproof

  2547 {\isafoldproof}%

  2548 %

  2549 \isadelimproof

  2550 \isanewline

  2551 %

  2552 \endisadelimproof

  2553 \isanewline

  2554 \isacommand{notepad}\isamarkupfalse%

  2555 \isanewline

  2556 \isakeyword{begin}\isanewline

  2557 %

  2558 \isadelimproof

  2559 \ \ %

  2560 \endisadelimproof

  2561 %

  2562 \isatagproof

  2563 \isacommand{fix}\isamarkupfalse%

  2564 \ x\ y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\isanewline

  2565 \ \ \isacommand{have}\isamarkupfalse%

  2566 \ C\isanewline

  2567 \ \ \isacommand{proof}\isamarkupfalse%

  2568 \ {\isaliteral{28}{\isacharparenleft}}cases\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{22}{\isachardoublequoteclose}}\ rule{\isaliteral{3A}{\isacharcolon}}\ tertium{\isaliteral{5F}{\isacharunderscore}}non{\isaliteral{5F}{\isacharunderscore}}datur{\isaliteral{29}{\isacharparenright}}\isanewline

  2569 \ \ \ \ \isacommand{case}\isamarkupfalse%

  2570 \ T\isanewline

  2571 \ \ \ \ \isacommand{from}\isamarkupfalse%

  2572 \ {\isaliteral{60}{\isacharbackquoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse%

  2573 \ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{sorry}\isamarkupfalse%

  2574 \isanewline

  2575 \ \ \isacommand{next}\isamarkupfalse%

  2576 \isanewline

  2577 \ \ \ \ \isacommand{case}\isamarkupfalse%

  2578 \ F\isanewline

  2579 \ \ \ \ \isacommand{from}\isamarkupfalse%

  2580 \ {\isaliteral{60}{\isacharbackquoteopen}}x\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ y{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse%

  2581 \ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{sorry}\isamarkupfalse%

  2582 \isanewline

  2583 \ \ \isacommand{qed}\isamarkupfalse%

  2584 %

  2585 \endisatagproof

  2586 {\isafoldproof}%

  2587 %

  2588 \isadelimproof

  2589 \isanewline

  2590 %

  2591 \endisadelimproof

  2592 \isacommand{end}\isamarkupfalse%

  2593 %

  2594 \isamarkupsubsubsection{Example%

  2595 }

  2596 \isamarkuptrue%

  2597 %

  2598 \begin{isamarkuptext}%

  2599 Isabelle/HOL specification mechanisms (datatype, inductive, etc.)

  2600   provide suitable derived cases rules.%

  2601 \end{isamarkuptext}%

  2602 \isamarkuptrue%

  2603 \isacommand{datatype}\isamarkupfalse%

  2604 \ foo\ {\isaliteral{3D}{\isacharequal}}\ Foo\ {\isaliteral{7C}{\isacharbar}}\ Bar\ foo\isanewline

  2605 \isanewline

  2606 \isacommand{notepad}\isamarkupfalse%

  2607 \isanewline

  2608 \isakeyword{begin}\isanewline

  2609 %

  2610 \isadelimproof

  2611 \ \ %

  2612 \endisadelimproof

  2613 %

  2614 \isatagproof

  2615 \isacommand{fix}\isamarkupfalse%

  2616 \ x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ foo\isanewline

  2617 \ \ \isacommand{have}\isamarkupfalse%

  2618 \ C\isanewline

  2619 \ \ \isacommand{proof}\isamarkupfalse%

  2620 \ {\isaliteral{28}{\isacharparenleft}}cases\ x{\isaliteral{29}{\isacharparenright}}\isanewline

  2621 \ \ \ \ \isacommand{case}\isamarkupfalse%

  2622 \ Foo\isanewline

  2623 \ \ \ \ \isacommand{from}\isamarkupfalse%

  2624 \ {\isaliteral{60}{\isacharbackquoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ Foo{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse%

  2625 \ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{sorry}\isamarkupfalse%

  2626 \isanewline

  2627 \ \ \isacommand{next}\isamarkupfalse%

  2628 \isanewline

  2629 \ \ \ \ \isacommand{case}\isamarkupfalse%

  2630 \ {\isaliteral{28}{\isacharparenleft}}Bar\ a{\isaliteral{29}{\isacharparenright}}\isanewline

  2631 \ \ \ \ \isacommand{from}\isamarkupfalse%

  2632 \ {\isaliteral{60}{\isacharbackquoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ Bar\ a{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse%

  2633 \ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{sorry}\isamarkupfalse%

  2634 \isanewline

  2635 \ \ \isacommand{qed}\isamarkupfalse%

  2636 %

  2637 \endisatagproof

  2638 {\isafoldproof}%

  2639 %

  2640 \isadelimproof

  2641 \isanewline

  2642 %

  2643 \endisadelimproof

  2644 \isacommand{end}\isamarkupfalse%

  2645 %

  2646 \isamarkupsubsection{Obtaining local contexts%

  2647 }

  2648 \isamarkuptrue%

  2649 %

  2650 \begin{isamarkuptext}%

  2651 A single ``case'' branch may be inlined into Isar proof text

  2652   via \hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}}.  This proves \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ B\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ thesis{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ thesis{\isaliteral{22}{\isachardoublequote}}} on the spot, and augments the context afterwards.%

  2653 \end{isamarkuptext}%

  2654 \isamarkuptrue%

  2655 \isacommand{notepad}\isamarkupfalse%

  2656 \isanewline

  2657 \isakeyword{begin}\isanewline

  2658 %

  2659 \isadelimproof

  2660 \ \ %

  2661 \endisadelimproof

  2662 %

  2663 \isatagproof

  2664 \isacommand{fix}\isamarkupfalse%

  2665 \ B\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  2666 \isanewline

  2667 \ \ \isacommand{obtain}\isamarkupfalse%

  2668 \ x\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

  2669 \isanewline

  2670 \ \ \isacommand{note}\isamarkupfalse%

  2671 \ {\isaliteral{60}{\isacharbackquoteopen}}B\ x{\isaliteral{60}{\isacharbackquoteclose}}%

  2672 \begin{isamarkuptxt}%

  2673 Conclusions from this context may not mention \isa{x} again!%

  2674 \end{isamarkuptxt}%

  2675 \isamarkuptrue%

  2676 \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%

  2677 \isanewline

  2678 \ \ \ \ \isacommand{obtain}\isamarkupfalse%

  2679 \ x\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%

  2680 \isanewline

  2681 \ \ \ \ \isacommand{from}\isamarkupfalse%

  2682 \ {\isaliteral{60}{\isacharbackquoteopen}}B\ x{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{have}\isamarkupfalse%

  2683 \ C\ \isacommand{sorry}\isamarkupfalse%

  2684 \isanewline

  2685 \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%

  2686 \isanewline

  2687 \ \ \isacommand{note}\isamarkupfalse%

  2688 \ {\isaliteral{60}{\isacharbackquoteopen}}C{\isaliteral{60}{\isacharbackquoteclose}}%

  2689 \endisatagproof

  2690 {\isafoldproof}%

  2691 %

  2692 \isadelimproof

  2693 \isanewline

  2694 %

  2695 \endisadelimproof

  2696 \isacommand{end}\isamarkupfalse%

  2697 \isanewline

  2698 %

  2699 \isadelimtheory

  2700 \isanewline

  2701 %

  2702 \endisadelimtheory

  2703 %

  2704 \isatagtheory

  2705 \isacommand{end}\isamarkupfalse%

  2706 %

  2707 \endisatagtheory

  2708 {\isafoldtheory}%

  2709 %

  2710 \isadelimtheory

  2711 \isanewline

  2712 %

  2713 \endisadelimtheory

  2714 \end{isabellebody}%

  2715 %%% Local Variables:

  2716 %%% mode: latex

  2717 %%% TeX-master: "root"

  2718 %%% End:

author	wenzelm
	Mon, 03 Oct 2011 11:14:19 +0200
changeset 45988	a45121ffcfcb
parent 44127	3ba51a3acff0
child 46691	1fe2dd6d5086
permissions	-rw-r--r--