3 \def\isabellecontext{Synopsis}%
10 \isacommand{theory}\isamarkupfalse%
12 \isakeyword{imports}\ Base\ Main\isanewline
21 \isamarkupchapter{Synopsis%
25 \isamarkupsection{Notepad%
29 \begin{isamarkuptext}%
30 An Isar proof body serves as mathematical notepad to compose logical
31 content, consisting of types, terms, facts.%
35 \isamarkupsubsection{Types and terms%
38 \isacommand{notepad}\isamarkupfalse%
48 Locally fixed entities:%
51 \ \ \isacommand{fix}\isamarkupfalse%
53 \isamarkupcmt{local constant, without any type information yet%
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%
62 \ \ \isacommand{fix}\isamarkupfalse%
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%
70 Definitions (non-polymorphic):%
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}}%
76 Abbreviations (polymorphic):%
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}}%
88 \ \ \isacommand{term}\isamarkupfalse%
89 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}f\ {\isaliteral{3F}{\isacharquery}}f{\isaliteral{22}{\isachardoublequoteclose}}%
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}}%
109 \isacommand{end}\isamarkupfalse%
111 \isamarkupsubsection{Facts%
115 \begin{isamarkuptext}%
116 A fact is a simultaneous list of theorems.%
120 \isamarkupsubsubsection{Producing facts%
123 \isacommand{notepad}\isamarkupfalse%
132 \begin{isamarkuptxt}%
133 Via assumption (``lambda''):%
136 \ \ \isacommand{assume}\isamarkupfalse%
137 \ a{\isaliteral{3A}{\isacharcolon}}\ A%
138 \begin{isamarkuptxt}%
139 Via proof (``let''):%
142 \ \ \isacommand{have}\isamarkupfalse%
143 \ b{\isaliteral{3A}{\isacharcolon}}\ B\ \isacommand{sorry}\isamarkupfalse%
145 \begin{isamarkuptxt}%
146 Via abbreviation (``let''):%
149 \ \ \isacommand{note}\isamarkupfalse%
150 \ c\ {\isaliteral{3D}{\isacharequal}}\ a\ b%
159 \isacommand{end}\isamarkupfalse%
161 \isamarkupsubsubsection{Referencing facts%
164 \isacommand{notepad}\isamarkupfalse%
173 \begin{isamarkuptxt}%
177 \ \ \isacommand{assume}\isamarkupfalse%
178 \ a{\isaliteral{3A}{\isacharcolon}}\ A\isanewline
179 \ \ \isacommand{note}\isamarkupfalse%
181 \begin{isamarkuptxt}%
185 \ \ \isacommand{assume}\isamarkupfalse%
187 \ \ \isacommand{note}\isamarkupfalse%
189 \begin{isamarkuptxt}%
190 Via literal proposition (unification with results from the proof text):%
193 \ \ \isacommand{assume}\isamarkupfalse%
195 \ \ \isacommand{note}\isamarkupfalse%
196 \ {\isaliteral{60}{\isacharbackquoteopen}}A{\isaliteral{60}{\isacharbackquoteclose}}\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}}%
211 \isacommand{end}\isamarkupfalse%
213 \isamarkupsubsubsection{Manipulating facts%
216 \isacommand{notepad}\isamarkupfalse%
225 \begin{isamarkuptxt}%
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%
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}%
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}%
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
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!):%
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}}%
277 \isacommand{end}\isamarkupfalse%
279 \isamarkupsubsubsection{Projections%
283 \begin{isamarkuptext}%
284 Isar facts consist of multiple theorems. There is notation to project
288 \isacommand{notepad}\isamarkupfalse%
290 \isakeyword{begin}\isanewline
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}}%
312 \isacommand{end}\isamarkupfalse%
314 \isamarkupsubsubsection{Naming conventions%
318 \begin{isamarkuptext}%
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}}}).
338 \isamarkupsubsection{Block structure%
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.%
347 \isacommand{notepad}\isamarkupfalse%
349 \isakeyword{begin}\isanewline
356 \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
358 \ \ \ \ \isacommand{have}\isamarkupfalse%
359 \ a{\isaliteral{3A}{\isacharcolon}}\ A\ \isacommand{sorry}\isamarkupfalse%
361 \ \ \ \ \isacommand{have}\isamarkupfalse%
362 \ b{\isaliteral{3A}{\isacharcolon}}\ B\ \isacommand{sorry}\isamarkupfalse%
364 \ \ \ \ \isacommand{note}\isamarkupfalse%
366 \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
368 \ \ \isacommand{note}\isamarkupfalse%
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}}%
381 \isacommand{end}\isamarkupfalse%
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.%
390 \isacommand{notepad}\isamarkupfalse%
392 \isakeyword{begin}\isanewline
400 \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
402 \ \ \ \ \isacommand{have}\isamarkupfalse%
403 \ a{\isaliteral{3A}{\isacharcolon}}\ A\ \isacommand{sorry}\isamarkupfalse%
405 \ \ \isacommand{next}\isamarkupfalse%
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%
414 \ \ \ \ \isacommand{next}\isamarkupfalse%
416 \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
417 \ c{\isaliteral{3A}{\isacharcolon}}\ C\ \isacommand{sorry}\isamarkupfalse%
419 \ \ \ \ \isacommand{next}\isamarkupfalse%
421 \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
422 \ d{\isaliteral{3A}{\isacharcolon}}\ D\ \isacommand{sorry}\isamarkupfalse%
424 \ \ \ \ \isacommand{qed}\isamarkupfalse%
426 \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
428 \begin{isamarkuptxt}%
429 Alternative version with explicit parentheses everywhere:%
432 \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
434 \ \ \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
436 \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
437 \ a{\isaliteral{3A}{\isacharcolon}}\ A\ \isacommand{sorry}\isamarkupfalse%
439 \ \ \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
441 \ \ \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
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%
449 \ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
450 \ B\ \isacommand{sorry}\isamarkupfalse%
452 \ \ \ \ \ \ \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
454 \ \ \ \ \ \ \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
456 \ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
457 \ c{\isaliteral{3A}{\isacharcolon}}\ C\ \isacommand{sorry}\isamarkupfalse%
459 \ \ \ \ \ \ \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
461 \ \ \ \ \ \ \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
463 \ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
464 \ d{\isaliteral{3A}{\isacharcolon}}\ D\ \isacommand{sorry}\isamarkupfalse%
466 \ \ \ \ \ \ \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
468 \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
470 \ \ \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
472 \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
482 \isacommand{end}\isamarkupfalse%
484 \isamarkupsection{Calculational reasoning \label{sec:calculations-synopsis}%
488 \begin{isamarkuptext}%
489 For example, see \verb|~~/src/HOL/Isar_Examples/Group.thy|.%
493 \isamarkupsubsection{Special names in Isar proofs%
497 \begin{isamarkuptext}%
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
511 \isacommand{notepad}\isamarkupfalse%
513 \isakeyword{begin}\isanewline
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}}%
531 \ \ \ \ \isacommand{term}\isamarkupfalse%
532 \ {\isaliteral{3F}{\isacharquery}}thesis\isanewline
539 \isacommand{show}\isamarkupfalse%
540 \ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{sorry}\isamarkupfalse%
549 \ \ \ \ \isacommand{term}\isamarkupfalse%
550 \ {\isaliteral{3F}{\isacharquery}}thesis\ \ %
551 \isamarkupcmt{static!%
560 \isacommand{qed}\isamarkupfalse%
569 \ \ \isacommand{term}\isamarkupfalse%
570 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
571 \ \ \isacommand{thm}\isamarkupfalse%
573 \isacommand{end}\isamarkupfalse%
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}.%
582 \isamarkupsubsection{Transitive chains%
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}}}}):%
591 \isacommand{thm}\isamarkupfalse%
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
598 \isacommand{notepad}\isamarkupfalse%
607 \begin{isamarkuptxt}%
608 Plain bottom-up calculation:%
611 \ \ \isacommand{have}\isamarkupfalse%
612 \ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
614 \ \ \isacommand{also}\isamarkupfalse%
616 \ \ \isacommand{have}\isamarkupfalse%
617 \ {\isaliteral{22}{\isachardoublequoteopen}}b\ {\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
619 \ \ \isacommand{also}\isamarkupfalse%
621 \ \ \isacommand{have}\isamarkupfalse%
622 \ {\isaliteral{22}{\isachardoublequoteopen}}c\ {\isaliteral{3D}{\isacharequal}}\ d{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
624 \ \ \isacommand{finally}\isamarkupfalse%
626 \ \ \isacommand{have}\isamarkupfalse%
627 \ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3D}{\isacharequal}}\ d{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
629 \begin{isamarkuptxt}%
630 Variant using the \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} abbreviation:%
633 \ \ \isacommand{have}\isamarkupfalse%
634 \ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
636 \ \ \isacommand{also}\isamarkupfalse%
638 \ \ \isacommand{have}\isamarkupfalse%
639 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
641 \ \ \isacommand{also}\isamarkupfalse%
643 \ \ \isacommand{have}\isamarkupfalse%
644 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ d{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
646 \ \ \isacommand{finally}\isamarkupfalse%
648 \ \ \isacommand{have}\isamarkupfalse%
649 \ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3D}{\isacharequal}}\ d{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
651 \begin{isamarkuptxt}%
652 Top-down version with explicit claim at the head:%
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%
662 \ \ \ \ \isacommand{also}\isamarkupfalse%
664 \ \ \ \ \isacommand{have}\isamarkupfalse%
665 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
667 \ \ \ \ \isacommand{also}\isamarkupfalse%
669 \ \ \ \ \isacommand{have}\isamarkupfalse%
670 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ d{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
672 \ \ \ \ \isacommand{finally}\isamarkupfalse%
674 \ \ \ \ \isacommand{show}\isamarkupfalse%
675 \ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
677 \ \ \isacommand{qed}\isamarkupfalse%
679 \isacommand{next}\isamarkupfalse%
681 \begin{isamarkuptxt}%
682 Mixed inequalities (require suitable base type):%
685 \ \ \isacommand{fix}\isamarkupfalse%
686 \ a\ b\ c\ d\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\isanewline
688 \ \ \isacommand{have}\isamarkupfalse%
689 \ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3C}{\isacharless}}\ b{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
691 \ \ \isacommand{also}\isamarkupfalse%
693 \ \ \isacommand{have}\isamarkupfalse%
694 \ {\isaliteral{22}{\isachardoublequoteopen}}b{\isaliteral{5C3C6C653E}{\isasymle}}\ c{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
696 \ \ \isacommand{also}\isamarkupfalse%
698 \ \ \isacommand{have}\isamarkupfalse%
699 \ {\isaliteral{22}{\isachardoublequoteopen}}c\ {\isaliteral{3D}{\isacharequal}}\ d{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
701 \ \ \isacommand{finally}\isamarkupfalse%
703 \ \ \isacommand{have}\isamarkupfalse%
704 \ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3C}{\isacharless}}\ d{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
713 \isacommand{end}\isamarkupfalse%
715 \isamarkupsubsubsection{Notes%
719 \begin{isamarkuptext}%
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.
732 \isamarkupsubsection{Degenerate calculations and bigstep reasoning%
736 \begin{isamarkuptext}%
737 The Idea is to append \isa{this} to \isa{calculation},
738 without rule composition.%
741 \isacommand{notepad}\isamarkupfalse%
750 \begin{isamarkuptxt}%
754 \ \ \isacommand{have}\isamarkupfalse%
755 \ A\ \isacommand{sorry}\isamarkupfalse%
757 \ \ \isacommand{moreover}\isamarkupfalse%
759 \ \ \isacommand{have}\isamarkupfalse%
760 \ B\ \isacommand{sorry}\isamarkupfalse%
762 \ \ \isacommand{moreover}\isamarkupfalse%
764 \ \ \isacommand{have}\isamarkupfalse%
765 \ C\ \isacommand{sorry}\isamarkupfalse%
767 \ \ \isacommand{ultimately}\isamarkupfalse%
769 \ \ \isacommand{have}\isamarkupfalse%
770 \ A\ \isakeyword{and}\ B\ \isakeyword{and}\ C\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
772 \isacommand{next}\isamarkupfalse%
774 \begin{isamarkuptxt}%
775 Slightly more content (trivial bigstep reasoning):%
778 \ \ \isacommand{have}\isamarkupfalse%
779 \ A\ \isacommand{sorry}\isamarkupfalse%
781 \ \ \isacommand{moreover}\isamarkupfalse%
783 \ \ \isacommand{have}\isamarkupfalse%
784 \ B\ \isacommand{sorry}\isamarkupfalse%
786 \ \ \isacommand{moreover}\isamarkupfalse%
788 \ \ \isacommand{have}\isamarkupfalse%
789 \ C\ \isacommand{sorry}\isamarkupfalse%
791 \ \ \isacommand{ultimately}\isamarkupfalse%
793 \ \ \isacommand{have}\isamarkupfalse%
794 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ C{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
796 \isacommand{next}\isamarkupfalse%
798 \begin{isamarkuptxt}%
799 More ambitious bigstep reasoning involving structured results:%
802 \ \ \isacommand{have}\isamarkupfalse%
803 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B\ {\isaliteral{5C3C6F723E}{\isasymor}}\ C{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
805 \ \ \isacommand{moreover}\isamarkupfalse%
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%
813 \ \ \isacommand{moreover}\isamarkupfalse%
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%
821 \ \ \isacommand{moreover}\isamarkupfalse%
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%
829 \ \ \isacommand{ultimately}\isamarkupfalse%
831 \ \ \isacommand{have}\isamarkupfalse%
832 \ R\ \isacommand{by}\isamarkupfalse%
834 \isamarkupcmt{``big-bang integration'' of proof blocks (occasionally fragile)%
844 \isacommand{end}\isamarkupfalse%
846 \isamarkupsection{Induction%
850 \isamarkupsubsection{Induction as Natural Deduction%
854 \begin{isamarkuptext}%
855 In principle, induction is just a special case of Natural
856 Deduction (see also \secref{sec:natural-deduction-synopsis}). For
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
865 \isacommand{notepad}\isamarkupfalse%
867 \isakeyword{begin}\isanewline
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!%
883 \ \ \ \ \isacommand{show}\isamarkupfalse%
884 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
886 \ \ \isacommand{next}\isamarkupfalse%
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%
895 \ \ \isacommand{qed}\isamarkupfalse%
904 \isacommand{end}\isamarkupfalse%
906 \begin{isamarkuptext}%
907 In practice, much more proof infrastructure is required.
909 The proof method \hyperlink{method.induct}{\mbox{\isa{induct}}} provides:
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.
922 \isacommand{notepad}\isamarkupfalse%
924 \isakeyword{begin}\isanewline
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%
942 \ \ \isacommand{next}\isamarkupfalse%
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%
950 \ \ \isacommand{qed}\isamarkupfalse%
959 \isacommand{end}\isamarkupfalse%
961 \isamarkupsubsubsection{Example%
965 \begin{isamarkuptext}%
966 The subsequent example combines the following proof patterns:
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
980 \isacommand{lemma}\isamarkupfalse%
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
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%
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%
1001 \ \ \isacommand{finally}\isamarkupfalse%
1002 \ \isacommand{show}\isamarkupfalse%
1003 \ {\isaliteral{3F}{\isacharquery}}case\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
1005 \isacommand{next}\isamarkupfalse%
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%
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%
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%
1024 \ \ \isacommand{finally}\isamarkupfalse%
1025 \ \isacommand{show}\isamarkupfalse%
1026 \ {\isaliteral{3F}{\isacharquery}}case\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
1028 \isacommand{qed}\isamarkupfalse%
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}%
1043 \isamarkupsubsection{Induction with local parameters and premises%
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}%
1056 \isacommand{notepad}\isamarkupfalse%
1058 \isakeyword{begin}\isanewline
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
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%
1081 \ \ \isacommand{next}\isamarkupfalse%
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%
1089 \ \ \isacommand{qed}\isamarkupfalse%
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%
1102 \ \ \isacommand{next}\isamarkupfalse%
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%
1111 \ \ \isacommand{qed}\isamarkupfalse%
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%
1123 \ \ \isacommand{next}\isamarkupfalse%
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%
1131 \begin{isamarkuptxt}%
1132 Local quantification admits arbitrary instances:%
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%
1146 \isacommand{end}\isamarkupfalse%
1148 \isamarkupsubsection{Implicit induction context%
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}%
1159 \isacommand{notepad}\isamarkupfalse%
1161 \isakeyword{begin}\isanewline
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
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%
1188 \ \ \isacommand{next}\isamarkupfalse%
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%
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%
1200 \ \ \isacommand{qed}\isamarkupfalse%
1209 \isacommand{end}\isamarkupfalse%
1211 \isamarkupsubsection{Advanced induction with term definitions%
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}%
1225 \isacommand{notepad}\isamarkupfalse%
1227 \isakeyword{begin}\isanewline
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
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%
1254 \ \ \isacommand{next}\isamarkupfalse%
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%
1265 \ \ \isacommand{qed}\isamarkupfalse%
1274 \isacommand{end}\isamarkupfalse%
1276 \isamarkupsection{Natural Deduction \label{sec:natural-deduction-synopsis}%
1280 \isamarkupsubsection{Rule statements%
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}%
1292 \isacommand{thm}\isamarkupfalse%
1294 \isacommand{thm}\isamarkupfalse%
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}%
1308 \isacommand{notepad}\isamarkupfalse%
1310 \isakeyword{begin}\isanewline
1317 \isacommand{write}\isamarkupfalse%
1318 \ Trueprop\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}Tr{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}%
1327 \ \ \isacommand{thm}\isamarkupfalse%
1329 \ \ \isacommand{thm}\isamarkupfalse%
1331 \ \ \isacommand{thm}\isamarkupfalse%
1332 \ nat{\isaliteral{2E}{\isachardot}}induct\isanewline
1333 \isacommand{end}\isamarkupfalse%
1335 \begin{isamarkuptext}%
1336 Isar provides first-class notation for rule statements as follows.%
1337 \end{isamarkuptext}%
1339 \isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}\isamarkupfalse%
1341 \isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}\isamarkupfalse%
1343 \isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}\isamarkupfalse%
1344 \ nat{\isaliteral{2E}{\isachardot}}induct%
1345 \isamarkupsubsubsection{Examples%
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}%
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}}%
1362 \isacommand{by}\isamarkupfalse%
1371 \isacommand{lemma}\isamarkupfalse%
1372 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q{\isaliteral{22}{\isachardoublequoteclose}}%
1378 \isacommand{by}\isamarkupfalse%
1388 \isacommand{lemma}\isamarkupfalse%
1389 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q{\isaliteral{22}{\isachardoublequoteclose}}%
1395 \isacommand{by}\isamarkupfalse%
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}}%
1411 \isacommand{by}\isamarkupfalse%
1421 \isacommand{lemma}\isamarkupfalse%
1422 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q{\isaliteral{22}{\isachardoublequoteclose}}%
1428 \isacommand{by}\isamarkupfalse%
1437 \isacommand{lemma}\isamarkupfalse%
1438 \ {\isaliteral{22}{\isachardoublequoteopen}}Q\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q{\isaliteral{22}{\isachardoublequoteclose}}%
1444 \isacommand{by}\isamarkupfalse%
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}}%
1460 \isacommand{by}\isamarkupfalse%
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}}%
1477 \isacommand{by}\isamarkupfalse%
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}}%
1493 \isacommand{by}\isamarkupfalse%
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}}%
1510 \isacommand{by}\isamarkupfalse%
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}}%
1526 \isacommand{by}\isamarkupfalse%
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}}%
1543 \isacommand{by}\isamarkupfalse%
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}}%
1559 \isacommand{by}\isamarkupfalse%
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}}%
1576 \isacommand{by}\isamarkupfalse%
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}}%
1592 \isacommand{by}\isamarkupfalse%
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}}%
1608 \isacommand{by}\isamarkupfalse%
1617 \isamarkupsubsection{Isar context elements%
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}%
1627 \isacommand{notepad}\isamarkupfalse%
1629 \isakeyword{begin}\isanewline
1636 \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
1638 \ \ \ \ \isacommand{fix}\isamarkupfalse%
1640 \ \ \ \ \isacommand{have}\isamarkupfalse%
1641 \ {\isaliteral{22}{\isachardoublequoteopen}}B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
1643 \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
1645 \ \ \isacommand{have}\isamarkupfalse%
1646 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
1649 \isacommand{next}\isamarkupfalse%
1652 \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
1654 \ \ \ \ \isacommand{assume}\isamarkupfalse%
1656 \ \ \ \ \isacommand{have}\isamarkupfalse%
1657 \ B\ \isacommand{sorry}\isamarkupfalse%
1659 \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
1661 \ \ \isacommand{have}\isamarkupfalse%
1662 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
1665 \isacommand{next}\isamarkupfalse%
1668 \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
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%
1675 \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
1677 \ \ \isacommand{have}\isamarkupfalse%
1678 \ {\isaliteral{22}{\isachardoublequoteopen}}B\ t{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
1681 \isacommand{next}\isamarkupfalse%
1684 \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
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%
1689 \ \ \ \ \isacommand{have}\isamarkupfalse%
1690 \ C\ \isacommand{sorry}\isamarkupfalse%
1692 \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
1694 \ \ \isacommand{have}\isamarkupfalse%
1695 \ C\ \isacommand{by}\isamarkupfalse%
1705 \isacommand{end}\isamarkupfalse%
1707 \isamarkupsubsection{Pure rule composition%
1711 \begin{isamarkuptext}%
1712 The Pure framework provides means for:
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}}}
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}%
1726 \isacommand{notepad}\isamarkupfalse%
1728 \isakeyword{begin}\isanewline
1735 \isacommand{assume}\isamarkupfalse%
1736 \ a{\isaliteral{3A}{\isacharcolon}}\ A\ \isakeyword{and}\ b{\isaliteral{3A}{\isacharcolon}}\ B%
1744 \ \ \isacommand{thm}\isamarkupfalse%
1746 \ \ \isacommand{thm}\isamarkupfalse%
1747 \ conjI\ {\isaliteral{5B}{\isacharbrackleft}}of\ A\ B{\isaliteral{5D}{\isacharbrackright}}\ \ %
1748 \isamarkupcmt{instantiation%
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%
1756 \ \ \isacommand{thm}\isamarkupfalse%
1757 \ conjI\ {\isaliteral{5B}{\isacharbrackleft}}OF\ a\ b{\isaliteral{5D}{\isacharbrackright}}\ \ %
1758 \isamarkupcmt{composition via unification (trivial)%
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
1764 \ \ \isacommand{thm}\isamarkupfalse%
1765 \ conjI\ {\isaliteral{5B}{\isacharbrackleft}}OF\ disjI{\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}\isanewline
1766 \isacommand{end}\isamarkupfalse%
1768 \begin{isamarkuptext}%
1769 Note: Low-level rule composition is tedious and leads to
1770 unreadable~/ unmaintainable expressions in the text.%
1771 \end{isamarkuptext}%
1774 \isamarkupsubsection{Structured backward reasoning%
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}%
1784 \isacommand{notepad}\isamarkupfalse%
1786 \isakeyword{begin}\isanewline
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
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%
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%
1807 \ \ \isacommand{qed}\isamarkupfalse%
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%
1816 \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
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%
1823 \ \ \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
1825 \isamarkupcmt{implicit block structure made explicit%
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
1831 \isamarkupcmt{side exit for the resulting rule%
1834 \ \ \isacommand{qed}\isamarkupfalse%
1843 \isacommand{end}\isamarkupfalse%
1845 \isamarkupsubsection{Structured rule application%
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}%
1854 \isacommand{notepad}\isamarkupfalse%
1856 \isakeyword{begin}\isanewline
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)%
1869 \ \ \isacommand{have}\isamarkupfalse%
1870 \ A\ \isacommand{sorry}\isamarkupfalse%
1872 \isamarkupcmt{prefix of facts via outer sub-proof%
1875 \ \ \isacommand{then}\isamarkupfalse%
1876 \ \isacommand{have}\isamarkupfalse%
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%
1883 \isamarkupcmt{remaining rule premises via inner sub-proof%
1886 \ \ \isacommand{qed}\isamarkupfalse%
1889 \ \ \isacommand{have}\isamarkupfalse%
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%
1896 \ \ \ \ \isacommand{show}\isamarkupfalse%
1897 \ B\ \isacommand{sorry}\isamarkupfalse%
1899 \ \ \isacommand{qed}\isamarkupfalse%
1902 \ \ \isacommand{have}\isamarkupfalse%
1903 \ A\ \isakeyword{and}\ B\ \isacommand{sorry}\isamarkupfalse%
1905 \ \ \isacommand{then}\isamarkupfalse%
1906 \ \isacommand{have}\isamarkupfalse%
1908 \ \ \isacommand{proof}\isamarkupfalse%
1909 \ {\isaliteral{28}{\isacharparenleft}}rule\ r{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\isanewline
1910 \ \ \isacommand{qed}\isamarkupfalse%
1913 \ \ \isacommand{have}\isamarkupfalse%
1914 \ A\ \isakeyword{and}\ B\ \isacommand{sorry}\isamarkupfalse%
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
1921 \isacommand{next}\isamarkupfalse%
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%
1930 \ \ \isacommand{have}\isamarkupfalse%
1931 \ A\ \isacommand{sorry}\isamarkupfalse%
1933 \ \ \isacommand{then}\isamarkupfalse%
1934 \ \isacommand{have}\isamarkupfalse%
1936 \ \ \isacommand{proof}\isamarkupfalse%
1937 \ {\isaliteral{28}{\isacharparenleft}}rule\ r{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\isanewline
1938 \ \ \ \ \isacommand{fix}\isamarkupfalse%
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%
1945 \ \ \isacommand{qed}\isamarkupfalse%
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.%
1960 \isacommand{end}\isamarkupfalse%
1962 \isamarkupsubsection{Example: predicate logic%
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}%
1971 \isacommand{notepad}\isamarkupfalse%
1973 \isakeyword{begin}\isanewline
1980 \isacommand{have}\isamarkupfalse%
1981 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ A\ \isacommand{sorry}\isamarkupfalse%
1983 \ \ \isacommand{then}\isamarkupfalse%
1984 \ \isacommand{have}\isamarkupfalse%
1985 \ B\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
1988 \ \ \isacommand{have}\isamarkupfalse%
1989 \ A\ \isacommand{sorry}\isamarkupfalse%
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%
1996 \ \ \isacommand{have}\isamarkupfalse%
1997 \ B\ \isacommand{sorry}\isamarkupfalse%
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%
2004 \ \ \isacommand{have}\isamarkupfalse%
2005 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
2007 \ \ \isacommand{then}\isamarkupfalse%
2008 \ \isacommand{have}\isamarkupfalse%
2010 \ \ \isacommand{proof}\isamarkupfalse%
2012 \ \ \ \ \isacommand{assume}\isamarkupfalse%
2014 \ \ \ \ \isacommand{then}\isamarkupfalse%
2015 \ \isacommand{show}\isamarkupfalse%
2016 \ C\ \isacommand{sorry}\isamarkupfalse%
2018 \ \ \isacommand{next}\isamarkupfalse%
2020 \ \ \ \ \isacommand{assume}\isamarkupfalse%
2022 \ \ \ \ \isacommand{then}\isamarkupfalse%
2023 \ \isacommand{show}\isamarkupfalse%
2024 \ C\ \isacommand{sorry}\isamarkupfalse%
2026 \ \ \isacommand{qed}\isamarkupfalse%
2029 \ \ \isacommand{have}\isamarkupfalse%
2030 \ A\ \isakeyword{and}\ B\ \isacommand{sorry}\isamarkupfalse%
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%
2037 \ \ \isacommand{have}\isamarkupfalse%
2038 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
2040 \ \ \isacommand{then}\isamarkupfalse%
2041 \ \isacommand{have}\isamarkupfalse%
2042 \ A\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
2045 \ \ \isacommand{have}\isamarkupfalse%
2046 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
2048 \ \ \isacommand{then}\isamarkupfalse%
2049 \ \isacommand{have}\isamarkupfalse%
2050 \ B\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
2053 \ \ \isacommand{have}\isamarkupfalse%
2054 \ False\ \isacommand{sorry}\isamarkupfalse%
2056 \ \ \isacommand{then}\isamarkupfalse%
2057 \ \isacommand{have}\isamarkupfalse%
2058 \ A\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
2061 \ \ \isacommand{have}\isamarkupfalse%
2062 \ True\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
2065 \ \ \isacommand{have}\isamarkupfalse%
2066 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
2067 \ \ \isacommand{proof}\isamarkupfalse%
2069 \ \ \ \ \isacommand{assume}\isamarkupfalse%
2071 \ \ \ \ \isacommand{then}\isamarkupfalse%
2072 \ \isacommand{show}\isamarkupfalse%
2073 \ False\ \isacommand{sorry}\isamarkupfalse%
2075 \ \ \isacommand{qed}\isamarkupfalse%
2078 \ \ \isacommand{have}\isamarkupfalse%
2079 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ A\ \isacommand{sorry}\isamarkupfalse%
2081 \ \ \isacommand{then}\isamarkupfalse%
2082 \ \isacommand{have}\isamarkupfalse%
2083 \ B\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
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%
2090 \ \ \ \ \isacommand{fix}\isamarkupfalse%
2092 \ \ \ \ \isacommand{show}\isamarkupfalse%
2093 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
2095 \ \ \isacommand{qed}\isamarkupfalse%
2098 \ \ \isacommand{have}\isamarkupfalse%
2099 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
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%
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%
2110 \ \ \ \ \isacommand{show}\isamarkupfalse%
2111 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ a{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
2113 \ \ \isacommand{qed}\isamarkupfalse%
2116 \ \ \isacommand{have}\isamarkupfalse%
2117 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
2119 \ \ \isacommand{then}\isamarkupfalse%
2120 \ \isacommand{have}\isamarkupfalse%
2122 \ \ \isacommand{proof}\isamarkupfalse%
2124 \ \ \ \ \isacommand{fix}\isamarkupfalse%
2126 \ \ \ \ \isacommand{assume}\isamarkupfalse%
2127 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ a{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
2128 \ \ \ \ \isacommand{show}\isamarkupfalse%
2129 \ C\ \isacommand{sorry}\isamarkupfalse%
2131 \ \ \isacommand{qed}\isamarkupfalse%
2133 \begin{isamarkuptxt}%
2134 Less awkward version using \hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}}:%
2137 \ \ \isacommand{have}\isamarkupfalse%
2138 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
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%
2151 \isacommand{end}\isamarkupfalse%
2153 \begin{isamarkuptext}%
2154 Further variations to illustrate Isar sub-proofs involving
2155 \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}:%
2156 \end{isamarkuptext}%
2158 \isacommand{notepad}\isamarkupfalse%
2160 \isakeyword{begin}\isanewline
2167 \isacommand{have}\isamarkupfalse%
2168 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
2169 \ \ \isacommand{proof}\isamarkupfalse%
2171 \isamarkupcmt{two strictly isolated subproofs%
2174 \ \ \ \ \isacommand{show}\isamarkupfalse%
2175 \ A\ \isacommand{sorry}\isamarkupfalse%
2177 \ \ \isacommand{next}\isamarkupfalse%
2179 \ \ \ \ \isacommand{show}\isamarkupfalse%
2180 \ B\ \isacommand{sorry}\isamarkupfalse%
2182 \ \ \isacommand{qed}\isamarkupfalse%
2185 \ \ \isacommand{have}\isamarkupfalse%
2186 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
2187 \ \ \isacommand{proof}\isamarkupfalse%
2189 \isamarkupcmt{one simultaneous sub-proof%
2192 \ \ \ \ \isacommand{show}\isamarkupfalse%
2193 \ A\ \isakeyword{and}\ B\ \isacommand{sorry}\isamarkupfalse%
2195 \ \ \isacommand{qed}\isamarkupfalse%
2198 \ \ \isacommand{have}\isamarkupfalse%
2199 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
2200 \ \ \isacommand{proof}\isamarkupfalse%
2202 \isamarkupcmt{two subproofs in the same context%
2205 \ \ \ \ \isacommand{show}\isamarkupfalse%
2206 \ A\ \isacommand{sorry}\isamarkupfalse%
2208 \ \ \ \ \isacommand{show}\isamarkupfalse%
2209 \ B\ \isacommand{sorry}\isamarkupfalse%
2211 \ \ \isacommand{qed}\isamarkupfalse%
2214 \ \ \isacommand{have}\isamarkupfalse%
2215 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
2216 \ \ \isacommand{proof}\isamarkupfalse%
2218 \isamarkupcmt{swapped order%
2221 \ \ \ \ \isacommand{show}\isamarkupfalse%
2222 \ B\ \isacommand{sorry}\isamarkupfalse%
2224 \ \ \ \ \isacommand{show}\isamarkupfalse%
2225 \ A\ \isacommand{sorry}\isamarkupfalse%
2227 \ \ \isacommand{qed}\isamarkupfalse%
2230 \ \ \isacommand{have}\isamarkupfalse%
2231 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
2232 \ \ \isacommand{proof}\isamarkupfalse%
2234 \isamarkupcmt{sequential subproofs%
2237 \ \ \ \ \isacommand{show}\isamarkupfalse%
2238 \ A\ \isacommand{sorry}\isamarkupfalse%
2240 \ \ \ \ \isacommand{show}\isamarkupfalse%
2241 \ B\ \isacommand{using}\isamarkupfalse%
2242 \ {\isaliteral{60}{\isacharbackquoteopen}}A{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{sorry}\isamarkupfalse%
2244 \ \ \isacommand{qed}\isamarkupfalse%
2253 \isacommand{end}\isamarkupfalse%
2255 \isamarkupsubsubsection{Example: set-theoretic operators%
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 for analogously. It is only a matter
2262 of rule declarations in the library; rules can be also specified
2264 \end{isamarkuptext}%
2266 \isacommand{notepad}\isamarkupfalse%
2268 \isakeyword{begin}\isanewline
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%
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%
2283 \ \ \isacommand{have}\isamarkupfalse%
2284 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
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%
2291 \ \ \isacommand{have}\isamarkupfalse%
2292 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
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%
2299 \ \ \isacommand{have}\isamarkupfalse%
2300 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
2302 \ \ \isacommand{then}\isamarkupfalse%
2303 \ \isacommand{have}\isamarkupfalse%
2305 \ \ \isacommand{proof}\isamarkupfalse%
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%
2313 \ \ \isacommand{next}\isamarkupfalse%
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%
2321 \ \ \isacommand{qed}\isamarkupfalse%
2324 \isacommand{next}\isamarkupfalse%
2326 \ \ \isacommand{have}\isamarkupfalse%
2327 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{5C3C496E7465723E}{\isasymInter}}A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
2328 \ \ \isacommand{proof}\isamarkupfalse%
2330 \ \ \ \ \isacommand{fix}\isamarkupfalse%
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%
2337 \ \ \isacommand{qed}\isamarkupfalse%
2340 \ \ \isacommand{have}\isamarkupfalse%
2341 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{5C3C496E7465723E}{\isasymInter}}A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
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%
2348 \ \ \ \ \isacommand{show}\isamarkupfalse%
2349 \ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
2351 \ \ \isacommand{qed}\isamarkupfalse%
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%
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%
2362 \ \ \isacommand{have}\isamarkupfalse%
2363 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{5C3C556E696F6E3E}{\isasymUnion}}A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
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%
2376 \isacommand{end}\isamarkupfalse%
2378 \isamarkupsection{Generalized elimination and cases%
2382 \isamarkupsubsection{General elimination rules%
2386 \begin{isamarkuptext}%
2387 The general format of elimination rules is illustrated by the
2388 following typical representatives:%
2389 \end{isamarkuptext}%
2391 \isacommand{thm}\isamarkupfalse%
2393 \isamarkupcmt{local parameter%
2396 \isacommand{thm}\isamarkupfalse%
2398 \isamarkupcmt{local premises%
2401 \isacommand{thm}\isamarkupfalse%
2403 \isamarkupcmt{split into cases%
2406 \begin{isamarkuptext}%
2407 Combining these characteristics leads to the following general scheme
2408 for elimination rules with cases:
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
2418 \end{isamarkuptext}%
2420 \isacommand{notepad}\isamarkupfalse%
2422 \isakeyword{begin}\isanewline
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
2436 \ \ \isacommand{have}\isamarkupfalse%
2437 \ A{\isadigit{1}}\ \isakeyword{and}\ A{\isadigit{2}}\ \isacommand{sorry}\isamarkupfalse%
2439 \ \ \isacommand{then}\isamarkupfalse%
2440 \ \isacommand{have}\isamarkupfalse%
2442 \ \ \isacommand{proof}\isamarkupfalse%
2443 \ {\isaliteral{28}{\isacharparenleft}}rule\ r{\isaliteral{29}{\isacharparenright}}\isanewline
2444 \ \ \ \ \isacommand{fix}\isamarkupfalse%
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%
2451 \ \ \isacommand{next}\isamarkupfalse%
2453 \ \ \ \ \isacommand{fix}\isamarkupfalse%
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%
2460 \ \ \isacommand{qed}\isamarkupfalse%
2469 \isacommand{end}\isamarkupfalse%
2471 \begin{isamarkuptext}%
2472 Here \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}thesis{\isaliteral{22}{\isachardoublequote}}} is used to refer to the unchanged goal
2474 \end{isamarkuptext}%
2477 \isamarkupsubsection{Rules with cases%
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:
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
2497 \end{isamarkuptext}%
2499 \isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}\isamarkupfalse%
2501 \isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}\isamarkupfalse%
2503 \isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}\isamarkupfalse%
2506 \isacommand{lemma}\isamarkupfalse%
2508 \ \ \isakeyword{assumes}\ A{\isadigit{1}}\ \isakeyword{and}\ A{\isadigit{2}}\ \ %
2509 \isamarkupcmt{assumptions%
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
2521 \isacommand{sorry}\isamarkupfalse%
2530 \isamarkupsubsubsection{Example%
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
2544 \isacommand{by}\isamarkupfalse%
2554 \isacommand{notepad}\isamarkupfalse%
2556 \isakeyword{begin}\isanewline
2563 \isacommand{fix}\isamarkupfalse%
2564 \ x\ y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\isanewline
2565 \ \ \isacommand{have}\isamarkupfalse%
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%
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%
2575 \ \ \isacommand{next}\isamarkupfalse%
2577 \ \ \ \ \isacommand{case}\isamarkupfalse%
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%
2583 \ \ \isacommand{qed}\isamarkupfalse%
2592 \isacommand{end}\isamarkupfalse%
2594 \isamarkupsubsubsection{Example%
2598 \begin{isamarkuptext}%
2599 Isabelle/HOL specification mechanisms (datatype, inductive, etc.)
2600 provide suitable derived cases rules.%
2601 \end{isamarkuptext}%
2603 \isacommand{datatype}\isamarkupfalse%
2604 \ foo\ {\isaliteral{3D}{\isacharequal}}\ Foo\ {\isaliteral{7C}{\isacharbar}}\ Bar\ foo\isanewline
2606 \isacommand{notepad}\isamarkupfalse%
2608 \isakeyword{begin}\isanewline
2615 \isacommand{fix}\isamarkupfalse%
2616 \ x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ foo\isanewline
2617 \ \ \isacommand{have}\isamarkupfalse%
2619 \ \ \isacommand{proof}\isamarkupfalse%
2620 \ {\isaliteral{28}{\isacharparenleft}}cases\ x{\isaliteral{29}{\isacharparenright}}\isanewline
2621 \ \ \ \ \isacommand{case}\isamarkupfalse%
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%
2627 \ \ \isacommand{next}\isamarkupfalse%
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%
2635 \ \ \isacommand{qed}\isamarkupfalse%
2644 \isacommand{end}\isamarkupfalse%
2646 \isamarkupsubsection{Obtaining local contexts%
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}%
2655 \isacommand{notepad}\isamarkupfalse%
2657 \isakeyword{begin}\isanewline
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
2667 \ \ \isacommand{obtain}\isamarkupfalse%
2668 \ x\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
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!%
2676 \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
2678 \ \ \ \ \isacommand{obtain}\isamarkupfalse%
2679 \ x\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
2681 \ \ \ \ \isacommand{from}\isamarkupfalse%
2682 \ {\isaliteral{60}{\isacharbackquoteopen}}B\ x{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{have}\isamarkupfalse%
2683 \ C\ \isacommand{sorry}\isamarkupfalse%
2685 \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
2687 \ \ \isacommand{note}\isamarkupfalse%
2688 \ {\isaliteral{60}{\isacharbackquoteopen}}C{\isaliteral{60}{\isacharbackquoteclose}}%
2696 \isacommand{end}\isamarkupfalse%
2705 \isacommand{end}\isamarkupfalse%
2714 %%% Local Variables:
2716 %%% TeX-master: "root"