
wenzelm@44121: %
wenzelm@44121: \begin{isabellebody}%
wenzelm@44121: \def\isabellecontext{Synopsis}%
wenzelm@44121: %
wenzelm@44121: \isadelimtheory
wenzelm@44121: %
wenzelm@44121: \endisadelimtheory
wenzelm@44121: %
wenzelm@44121: \isatagtheory
wenzelm@44121: \isacommand{theory}\isamarkupfalse%
wenzelm@44121: \ Synopsis\isanewline
wenzelm@44121: \isakeyword{imports}\ Base\ Main\isanewline
wenzelm@44121: \isakeyword{begin}%
wenzelm@44121: \endisatagtheory
wenzelm@44121: {\isafoldtheory}%
wenzelm@44121: %
wenzelm@44121: \isadelimtheory
wenzelm@44121: %
wenzelm@44121: \endisadelimtheory
wenzelm@44121: %
wenzelm@44121: \isamarkupchapter{Synopsis%
wenzelm@44121: }
wenzelm@44121: \isamarkuptrue%
wenzelm@44121: %
wenzelm@44121: \isamarkupsection{Notepad%
wenzelm@44121: }
wenzelm@44121: \isamarkuptrue%
wenzelm@44121: %
wenzelm@44121: \begin{isamarkuptext}%
wenzelm@44121: An Isar proof body serves as mathematical notepad to compose logical
wenzelm@44122:   content, consisting of types, terms, facts.%
wenzelm@44121: \end{isamarkuptext}%
wenzelm@44121: \isamarkuptrue%
wenzelm@44121: %
wenzelm@44122: \isamarkupsubsection{Types and terms%
wenzelm@44122: }
wenzelm@44122: \isamarkuptrue%
wenzelm@44122: \isacommand{notepad}\isamarkupfalse%
wenzelm@44122: \isanewline
wenzelm@44122: \isakeyword{begin}%
wenzelm@44122: \isadelimproof
wenzelm@44122: %
wenzelm@44122: \endisadelimproof
wenzelm@44122: %
wenzelm@44122: \isatagproof
wenzelm@44122: %
wenzelm@44122: \begin{isamarkuptxt}%
wenzelm@44122: Locally fixed entities:%
wenzelm@44122: \end{isamarkuptxt}%
wenzelm@44122: \isamarkuptrue%
wenzelm@44122: \ \ \isacommand{fix}\isamarkupfalse%
wenzelm@44122: \ x\ \ \ %
wenzelm@44122: \isamarkupcmt{local constant, without any type information yet%
wenzelm@44122: }
wenzelm@44122: \isanewline
wenzelm@44122: \ \ \isacommand{fix}\isamarkupfalse%
wenzelm@44122: \ x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ \ %
wenzelm@44122: \isamarkupcmt{variant with explicit type-constraint for subsequent use%
wenzelm@44122: }
wenzelm@44122: \isanewline
wenzelm@44122: \isanewline
wenzelm@44122: \ \ \isacommand{fix}\isamarkupfalse%
wenzelm@44122: \ a\ b\isanewline
wenzelm@44122: \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44122: \ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{22}{\isachardoublequoteclose}}\ \ %
wenzelm@44122: \isamarkupcmt{type assignment at first occurrence in concrete term%
wenzelm@44122: }
wenzelm@44122: %
wenzelm@44122: \begin{isamarkuptxt}%
wenzelm@44122: Definitions (non-polymorphic):%
wenzelm@44122: \end{isamarkuptxt}%
wenzelm@44122: \isamarkuptrue%
wenzelm@44122: \ \ \isacommand{def}\isamarkupfalse%
wenzelm@44122: \ x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{22}{\isachardoublequoteopen}}t{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequoteclose}}%
wenzelm@44122: \begin{isamarkuptxt}%
wenzelm@44122: Abbreviations (polymorphic):%
wenzelm@44122: \end{isamarkuptxt}%
wenzelm@44122: \isamarkuptrue%
wenzelm@44122: \ \ \isacommand{let}\isamarkupfalse%
wenzelm@44122: \ {\isaliteral{3F}{\isacharquery}}f\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{22}{\isachardoublequoteclose}}%
wenzelm@44122: \endisatagproof
wenzelm@44122: {\isafoldproof}%
wenzelm@44122: %
wenzelm@44122: \isadelimproof
wenzelm@44122: %
wenzelm@44122: \endisadelimproof
wenzelm@44122: \isanewline
wenzelm@44122: \ \ \isacommand{term}\isamarkupfalse%
wenzelm@44122: \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}f\ {\isaliteral{3F}{\isacharquery}}f{\isaliteral{22}{\isachardoublequoteclose}}%
wenzelm@44122: \isadelimproof
wenzelm@44122: %
wenzelm@44122: \endisadelimproof
wenzelm@44122: %
wenzelm@44122: \isatagproof
wenzelm@44122: %
wenzelm@44122: \begin{isamarkuptxt}%
wenzelm@44122: Notation:%
wenzelm@44122: \end{isamarkuptxt}%
wenzelm@44122: \isamarkuptrue%
wenzelm@44122: \ \ \isacommand{write}\isamarkupfalse%
wenzelm@44122: \ x\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}%
wenzelm@44122: \endisatagproof
wenzelm@44122: {\isafoldproof}%
wenzelm@44122: %
wenzelm@44122: \isadelimproof
wenzelm@44122: %
wenzelm@44122: \endisadelimproof
wenzelm@44122: \isanewline
wenzelm@44122: \isacommand{end}\isamarkupfalse%
wenzelm@44122: %
wenzelm@44121: \isamarkupsubsection{Facts%
wenzelm@44121: }
wenzelm@44121: \isamarkuptrue%
wenzelm@44121: %
wenzelm@44121: \begin{isamarkuptext}%
wenzelm@44121: A fact is a simultaneous list of theorems.%
wenzelm@44121: \end{isamarkuptext}%
wenzelm@44121: \isamarkuptrue%
wenzelm@44121: %
wenzelm@44121: \isamarkupsubsubsection{Producing facts%
wenzelm@44121: }
wenzelm@44121: \isamarkuptrue%
wenzelm@44121: \isacommand{notepad}\isamarkupfalse%
wenzelm@44121: \isanewline
wenzelm@44121: \isakeyword{begin}%
wenzelm@44121: \isadelimproof
wenzelm@44121: %
wenzelm@44121: \endisadelimproof
wenzelm@44121: %
wenzelm@44121: \isatagproof
wenzelm@44121: %
wenzelm@44121: \begin{isamarkuptxt}%
wenzelm@44121: Via assumption (``lambda''):%
wenzelm@44121: \end{isamarkuptxt}%
wenzelm@44121: \isamarkuptrue%
wenzelm@44121: \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44121: \ a{\isaliteral{3A}{\isacharcolon}}\ A%
wenzelm@44121: \begin{isamarkuptxt}%
wenzelm@44121: Via proof (``let''):%
wenzelm@44121: \end{isamarkuptxt}%
wenzelm@44121: \isamarkuptrue%
wenzelm@44121: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44121: \ b{\isaliteral{3A}{\isacharcolon}}\ B\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44121: %
wenzelm@44121: \begin{isamarkuptxt}%
wenzelm@44121: Via abbreviation (``let''):%
wenzelm@44121: \end{isamarkuptxt}%
wenzelm@44121: \isamarkuptrue%
wenzelm@44121: \ \ \isacommand{note}\isamarkupfalse%
wenzelm@44121: \ c\ {\isaliteral{3D}{\isacharequal}}\ a\ b%
wenzelm@44121: \endisatagproof
wenzelm@44121: {\isafoldproof}%
wenzelm@44121: %
wenzelm@44121: \isadelimproof
wenzelm@44121: %
wenzelm@44121: \endisadelimproof
wenzelm@44121: \isanewline
wenzelm@44121: \isanewline
wenzelm@44121: \isacommand{end}\isamarkupfalse%
wenzelm@44121: %
wenzelm@44121: \isamarkupsubsubsection{Referencing facts%
wenzelm@44121: }
wenzelm@44121: \isamarkuptrue%
wenzelm@44121: \isacommand{notepad}\isamarkupfalse%
wenzelm@44121: \isanewline
wenzelm@44121: \isakeyword{begin}%
wenzelm@44121: \isadelimproof
wenzelm@44121: %
wenzelm@44121: \endisadelimproof
wenzelm@44121: %
wenzelm@44121: \isatagproof
wenzelm@44121: %
wenzelm@44121: \begin{isamarkuptxt}%
wenzelm@44121: Via explicit name:%
wenzelm@44121: \end{isamarkuptxt}%
wenzelm@44121: \isamarkuptrue%
wenzelm@44121: \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44121: \ a{\isaliteral{3A}{\isacharcolon}}\ A\isanewline
wenzelm@44121: \ \ \isacommand{note}\isamarkupfalse%
wenzelm@44121: \ a%
wenzelm@44121: \begin{isamarkuptxt}%
wenzelm@44121: Via implicit name:%
wenzelm@44121: \end{isamarkuptxt}%
wenzelm@44121: \isamarkuptrue%
wenzelm@44121: \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44121: \ A\isanewline
wenzelm@44121: \ \ \isacommand{note}\isamarkupfalse%
wenzelm@44121: \ this%
wenzelm@44121: \begin{isamarkuptxt}%
wenzelm@44121: Via literal proposition (unification with results from the proof text):%
wenzelm@44121: \end{isamarkuptxt}%
wenzelm@44121: \isamarkuptrue%
wenzelm@44121: \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44121: \ A\isanewline
wenzelm@44121: \ \ \isacommand{note}\isamarkupfalse%
wenzelm@44121: \ {\isaliteral{60}{\isacharbackquoteopen}}A{\isaliteral{60}{\isacharbackquoteclose}}\isanewline
wenzelm@44121: \isanewline
wenzelm@44121: \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44121: \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ B\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44121: \ \ \isacommand{note}\isamarkupfalse%
wenzelm@44121: \ {\isaliteral{60}{\isacharbackquoteopen}}B\ a{\isaliteral{60}{\isacharbackquoteclose}}\isanewline
wenzelm@44121: \ \ \isacommand{note}\isamarkupfalse%
wenzelm@44121: \ {\isaliteral{60}{\isacharbackquoteopen}}B\ b{\isaliteral{60}{\isacharbackquoteclose}}%
wenzelm@44121: \endisatagproof
wenzelm@44121: {\isafoldproof}%
wenzelm@44121: %
wenzelm@44121: \isadelimproof
wenzelm@44121: %
wenzelm@44121: \endisadelimproof
wenzelm@44121: \isanewline
wenzelm@44121: \isacommand{end}\isamarkupfalse%
wenzelm@44121: %
wenzelm@44121: \isamarkupsubsubsection{Manipulating facts%
wenzelm@44121: }
wenzelm@44121: \isamarkuptrue%
wenzelm@44121: \isacommand{notepad}\isamarkupfalse%
wenzelm@44121: \isanewline
wenzelm@44121: \isakeyword{begin}%
wenzelm@44121: \isadelimproof
wenzelm@44121: %
wenzelm@44121: \endisadelimproof
wenzelm@44121: %
wenzelm@44121: \isatagproof
wenzelm@44121: %
wenzelm@44121: \begin{isamarkuptxt}%
wenzelm@44121: Instantiation:%
wenzelm@44121: \end{isamarkuptxt}%
wenzelm@44121: \isamarkuptrue%
wenzelm@44121: \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44121: \ a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ B\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44121: \ \ \isacommand{note}\isamarkupfalse%
wenzelm@44121: \ a\isanewline
wenzelm@44121: \ \ \isacommand{note}\isamarkupfalse%
wenzelm@44121: \ a\ {\isaliteral{5B}{\isacharbrackleft}}of\ b{\isaliteral{5D}{\isacharbrackright}}\isanewline
wenzelm@44121: \ \ \isacommand{note}\isamarkupfalse%
wenzelm@44121: \ a\ {\isaliteral{5B}{\isacharbrackleft}}\isakeyword{where}\ x\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{5D}{\isacharbrackright}}%
wenzelm@44121: \begin{isamarkuptxt}%
wenzelm@44121: Backchaining:%
wenzelm@44121: \end{isamarkuptxt}%
wenzelm@44121: \isamarkuptrue%
wenzelm@44121: \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44121: \ {\isadigit{1}}{\isaliteral{3A}{\isacharcolon}}\ A\isanewline
wenzelm@44121: \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44121: \ {\isadigit{2}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44121: \ \ \isacommand{note}\isamarkupfalse%
wenzelm@44121: \ {\isadigit{2}}\ {\isaliteral{5B}{\isacharbrackleft}}OF\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}\isanewline
wenzelm@44121: \ \ \isacommand{note}\isamarkupfalse%
wenzelm@44121: \ {\isadigit{1}}\ {\isaliteral{5B}{\isacharbrackleft}}THEN\ {\isadigit{2}}{\isaliteral{5D}{\isacharbrackright}}%
wenzelm@44121: \begin{isamarkuptxt}%
wenzelm@44121: Symmetric results:%
wenzelm@44121: \end{isamarkuptxt}%
wenzelm@44121: \isamarkuptrue%
wenzelm@44121: \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44121: \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44121: \ \ \isacommand{note}\isamarkupfalse%
wenzelm@44121: \ this\ {\isaliteral{5B}{\isacharbrackleft}}symmetric{\isaliteral{5D}{\isacharbrackright}}\isanewline
wenzelm@44121: \isanewline
wenzelm@44121: \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44121: \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44121: \ \ \isacommand{note}\isamarkupfalse%
wenzelm@44121: \ this\ {\isaliteral{5B}{\isacharbrackleft}}symmetric{\isaliteral{5D}{\isacharbrackright}}%
wenzelm@44121: \begin{isamarkuptxt}%
wenzelm@44126: Adhoc-simplification (take care!):%
wenzelm@44121: \end{isamarkuptxt}%
wenzelm@44121: \isamarkuptrue%
wenzelm@44121: \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44121: \ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{40}{\isacharat}}\ xs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44121: \ \ \isacommand{note}\isamarkupfalse%
wenzelm@44121: \ this\ {\isaliteral{5B}{\isacharbrackleft}}simplified{\isaliteral{5D}{\isacharbrackright}}%
wenzelm@44121: \endisatagproof
wenzelm@44121: {\isafoldproof}%
wenzelm@44121: %
wenzelm@44121: \isadelimproof
wenzelm@44121: %
wenzelm@44121: \endisadelimproof
wenzelm@44121: \isanewline
wenzelm@44121: \isacommand{end}\isamarkupfalse%
wenzelm@44121: %
wenzelm@44121: \isamarkupsubsubsection{Projections%
wenzelm@44121: }
wenzelm@44121: \isamarkuptrue%
wenzelm@44121: %
wenzelm@44121: \begin{isamarkuptext}%
wenzelm@44121: Isar facts consist of multiple theorems.  There is notation to project
wenzelm@44121:   interval ranges.%
wenzelm@44121: \end{isamarkuptext}%
wenzelm@44121: \isamarkuptrue%
wenzelm@44121: \isacommand{notepad}\isamarkupfalse%
wenzelm@44121: \isanewline
wenzelm@44121: \isakeyword{begin}\isanewline
wenzelm@44121: %
wenzelm@44121: \isadelimproof
wenzelm@44121: \ \ %
wenzelm@44121: \endisadelimproof
wenzelm@44121: %
wenzelm@44121: \isatagproof
wenzelm@44121: \isacommand{assume}\isamarkupfalse%
wenzelm@44121: \ stuff{\isaliteral{3A}{\isacharcolon}}\ A\ B\ C\ D\isanewline
wenzelm@44121: \ \ \isacommand{note}\isamarkupfalse%
wenzelm@44121: \ stuff{\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44121: \ \ \isacommand{note}\isamarkupfalse%
wenzelm@44121: \ stuff{\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}{\isaliteral{2D}{\isacharminus}}{\isadigit{3}}{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44121: \ \ \isacommand{note}\isamarkupfalse%
wenzelm@44121: \ stuff{\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{29}{\isacharparenright}}%
wenzelm@44121: \endisatagproof
wenzelm@44121: {\isafoldproof}%
wenzelm@44121: %
wenzelm@44121: \isadelimproof
wenzelm@44121: \isanewline
wenzelm@44121: %
wenzelm@44121: \endisadelimproof
wenzelm@44121: \isacommand{end}\isamarkupfalse%
wenzelm@44121: %
wenzelm@44121: \isamarkupsubsubsection{Naming conventions%
wenzelm@44121: }
wenzelm@44121: \isamarkuptrue%
wenzelm@44121: %
wenzelm@44121: \begin{isamarkuptext}%
wenzelm@44121: \begin{itemize}
wenzelm@44121: 
wenzelm@44121:   \item Lower-case identifiers are usually preferred.
wenzelm@44121: 
wenzelm@44121:   \item Facts can be named after the main term within the proposition.
wenzelm@44121: 
wenzelm@44121:   \item Facts should \emph{not} be named after the command that
wenzelm@44121:   introduced them (\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}, \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}).  This is
wenzelm@44121:   misleading and hard to maintain.
wenzelm@44121: 
wenzelm@44121:   \item Natural numbers can be used as ``meaningless'' names (more
wenzelm@44121:   appropriate than \isa{{\isaliteral{22}{\isachardoublequote}}a{\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}a{\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}} etc.)
wenzelm@44121: 
wenzelm@44121:   \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}}}).
wenzelm@44121: 
wenzelm@44121:   \end{itemize}%
wenzelm@44121: \end{isamarkuptext}%
wenzelm@44121: \isamarkuptrue%
wenzelm@44121: %
wenzelm@44121: \isamarkupsubsection{Block structure%
wenzelm@44121: }
wenzelm@44121: \isamarkuptrue%
wenzelm@44121: %
wenzelm@44121: \begin{isamarkuptext}%
wenzelm@44121: The formal notepad is block structured.  The fact produced by the last
wenzelm@44121:   entry of a block is exported into the outer context.%
wenzelm@44121: \end{isamarkuptext}%
wenzelm@44121: \isamarkuptrue%
wenzelm@44121: \isacommand{notepad}\isamarkupfalse%
wenzelm@44121: \isanewline
wenzelm@44121: \isakeyword{begin}\isanewline
wenzelm@44121: %
wenzelm@44121: \isadelimproof
wenzelm@44121: \ \ %
wenzelm@44121: \endisadelimproof
wenzelm@44121: %
wenzelm@44121: \isatagproof
wenzelm@44121: \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
wenzelm@44121: \isanewline
wenzelm@44121: \ \ \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44121: \ a{\isaliteral{3A}{\isacharcolon}}\ A\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44121: \isanewline
wenzelm@44121: \ \ \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44121: \ b{\isaliteral{3A}{\isacharcolon}}\ B\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44121: \isanewline
wenzelm@44121: \ \ \ \ \isacommand{note}\isamarkupfalse%
wenzelm@44121: \ a\ b\isanewline
wenzelm@44121: \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
wenzelm@44121: \isanewline
wenzelm@44121: \ \ \isacommand{note}\isamarkupfalse%
wenzelm@44121: \ this\isanewline
wenzelm@44121: \ \ \isacommand{note}\isamarkupfalse%
wenzelm@44121: \ {\isaliteral{60}{\isacharbackquoteopen}}A{\isaliteral{60}{\isacharbackquoteclose}}\isanewline
wenzelm@44121: \ \ \isacommand{note}\isamarkupfalse%
wenzelm@44121: \ {\isaliteral{60}{\isacharbackquoteopen}}B{\isaliteral{60}{\isacharbackquoteclose}}%
wenzelm@44121: \endisatagproof
wenzelm@44121: {\isafoldproof}%
wenzelm@44121: %
wenzelm@44121: \isadelimproof
wenzelm@44121: \isanewline
wenzelm@44121: %
wenzelm@44121: \endisadelimproof
wenzelm@44121: \isacommand{end}\isamarkupfalse%
wenzelm@44121: %
wenzelm@44121: \begin{isamarkuptext}%
wenzelm@44121: Explicit blocks as well as implicit blocks of nested goal
wenzelm@44121:   statements (e.g.\ \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}) automatically introduce one extra
wenzelm@44121:   pair of parentheses in reserve.  The \hyperlink{command.next}{\mbox{\isa{\isacommand{next}}}} command allows
wenzelm@44122:   to ``jump'' between these sub-blocks.%
wenzelm@44121: \end{isamarkuptext}%
wenzelm@44121: \isamarkuptrue%
wenzelm@44121: \isacommand{notepad}\isamarkupfalse%
wenzelm@44121: \isanewline
wenzelm@44121: \isakeyword{begin}\isanewline
wenzelm@44121: %
wenzelm@44121: \isadelimproof
wenzelm@44121: \isanewline
wenzelm@44121: \ \ %
wenzelm@44121: \endisadelimproof
wenzelm@44121: %
wenzelm@44121: \isatagproof
wenzelm@44121: \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
wenzelm@44121: \isanewline
wenzelm@44121: \ \ \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44121: \ a{\isaliteral{3A}{\isacharcolon}}\ A\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44121: \isanewline
wenzelm@44121: \ \ \isacommand{next}\isamarkupfalse%
wenzelm@44121: \isanewline
wenzelm@44121: \ \ \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44121: \ b{\isaliteral{3A}{\isacharcolon}}\ B\isanewline
wenzelm@44121: \ \ \ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44121: \ {\isaliteral{2D}{\isacharminus}}\isanewline
wenzelm@44121: \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44121: \ B\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44121: \isanewline
wenzelm@44121: \ \ \ \ \isacommand{next}\isamarkupfalse%
wenzelm@44121: \isanewline
wenzelm@44121: \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44121: \ c{\isaliteral{3A}{\isacharcolon}}\ C\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44121: \isanewline
wenzelm@44121: \ \ \ \ \isacommand{next}\isamarkupfalse%
wenzelm@44121: \isanewline
wenzelm@44121: \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44121: \ d{\isaliteral{3A}{\isacharcolon}}\ D\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44121: \isanewline
wenzelm@44121: \ \ \ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44121: \isanewline
wenzelm@44121: \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
wenzelm@44121: %
wenzelm@44121: \begin{isamarkuptxt}%
wenzelm@44121: Alternative version with explicit parentheses everywhere:%
wenzelm@44121: \end{isamarkuptxt}%
wenzelm@44121: \isamarkuptrue%
wenzelm@44121: \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
wenzelm@44121: \isanewline
wenzelm@44121: \ \ \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
wenzelm@44121: \isanewline
wenzelm@44121: \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44121: \ a{\isaliteral{3A}{\isacharcolon}}\ A\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44121: \isanewline
wenzelm@44121: \ \ \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
wenzelm@44121: \isanewline
wenzelm@44121: \ \ \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
wenzelm@44121: \isanewline
wenzelm@44121: \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44121: \ b{\isaliteral{3A}{\isacharcolon}}\ B\isanewline
wenzelm@44121: \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44121: \ {\isaliteral{2D}{\isacharminus}}\isanewline
wenzelm@44121: \ \ \ \ \ \ \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
wenzelm@44121: \isanewline
wenzelm@44121: \ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44121: \ B\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44121: \isanewline
wenzelm@44121: \ \ \ \ \ \ \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
wenzelm@44121: \isanewline
wenzelm@44121: \ \ \ \ \ \ \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
wenzelm@44121: \isanewline
wenzelm@44121: \ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44121: \ c{\isaliteral{3A}{\isacharcolon}}\ C\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44121: \isanewline
wenzelm@44121: \ \ \ \ \ \ \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
wenzelm@44121: \isanewline
wenzelm@44121: \ \ \ \ \ \ \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
wenzelm@44121: \isanewline
wenzelm@44121: \ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44121: \ d{\isaliteral{3A}{\isacharcolon}}\ D\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44121: \isanewline
wenzelm@44121: \ \ \ \ \ \ \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
wenzelm@44121: \isanewline
wenzelm@44121: \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44121: \isanewline
wenzelm@44121: \ \ \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
wenzelm@44121: \isanewline
wenzelm@44121: \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
wenzelm@44121: %
wenzelm@44121: \endisatagproof
wenzelm@44121: {\isafoldproof}%
wenzelm@44121: %
wenzelm@44121: \isadelimproof
wenzelm@44121: \isanewline
wenzelm@44121: %
wenzelm@44121: \endisadelimproof
wenzelm@44121: \isanewline
wenzelm@44121: \isacommand{end}\isamarkupfalse%
wenzelm@44123: %
wenzelm@44125: \isamarkupsection{Calculational reasoning \label{sec:calculations-synopsis}%
wenzelm@44123: }
wenzelm@44123: \isamarkuptrue%
wenzelm@44123: %
wenzelm@44123: \begin{isamarkuptext}%
wenzelm@44123: For example, see \verb|~~/src/HOL/Isar_Examples/Group.thy|.%
wenzelm@44123: \end{isamarkuptext}%
wenzelm@44123: \isamarkuptrue%
wenzelm@44123: %
wenzelm@44123: \isamarkupsubsection{Special names in Isar proofs%
wenzelm@44123: }
wenzelm@44123: \isamarkuptrue%
wenzelm@44123: %
wenzelm@44123: \begin{isamarkuptext}%
wenzelm@44123: \begin{itemize}
wenzelm@44123: 
wenzelm@44123:   \item term \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}thesis{\isaliteral{22}{\isachardoublequote}}} --- the main conclusion of the
wenzelm@44123:   innermost pending claim
wenzelm@44123: 
wenzelm@44123:   \item term \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} --- the argument of the last explicitly
wenzelm@44123:     stated result (for infix application this is the right-hand side)
wenzelm@44123: 
wenzelm@44123:   \item fact \isa{{\isaliteral{22}{\isachardoublequote}}this{\isaliteral{22}{\isachardoublequote}}} --- the last result produced in the text
wenzelm@44123: 
wenzelm@44123:   \end{itemize}%
wenzelm@44123: \end{isamarkuptext}%
wenzelm@44123: \isamarkuptrue%
wenzelm@44123: \isacommand{notepad}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \isakeyword{begin}\isanewline
wenzelm@44123: %
wenzelm@44123: \isadelimproof
wenzelm@44123: \ \ %
wenzelm@44123: \endisadelimproof
wenzelm@44123: %
wenzelm@44123: \isatagproof
wenzelm@44123: \isacommand{have}\isamarkupfalse%
wenzelm@44123: \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44123: \ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44123: \ {\isaliteral{2D}{\isacharminus}}%
wenzelm@44123: \endisatagproof
wenzelm@44123: {\isafoldproof}%
wenzelm@44123: %
wenzelm@44123: \isadelimproof
wenzelm@44123: \isanewline
wenzelm@44123: %
wenzelm@44123: \endisadelimproof
wenzelm@44123: \ \ \ \ \isacommand{term}\isamarkupfalse%
wenzelm@44123: \ {\isaliteral{3F}{\isacharquery}}thesis\isanewline
wenzelm@44123: %
wenzelm@44123: \isadelimproof
wenzelm@44123: \ \ \ \ %
wenzelm@44123: \endisadelimproof
wenzelm@44123: %
wenzelm@44123: \isatagproof
wenzelm@44123: \isacommand{show}\isamarkupfalse%
wenzelm@44123: \ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44123: %
wenzelm@44123: \endisatagproof
wenzelm@44123: {\isafoldproof}%
wenzelm@44123: %
wenzelm@44123: \isadelimproof
wenzelm@44123: \isanewline
wenzelm@44123: %
wenzelm@44123: \endisadelimproof
wenzelm@44123: \ \ \ \ \isacommand{term}\isamarkupfalse%
wenzelm@44123: \ {\isaliteral{3F}{\isacharquery}}thesis\ \ %
wenzelm@44123: \isamarkupcmt{static!%
wenzelm@44123: }
wenzelm@44123: \isanewline
wenzelm@44123: %
wenzelm@44123: \isadelimproof
wenzelm@44123: \ \ %
wenzelm@44123: \endisadelimproof
wenzelm@44123: %
wenzelm@44123: \isatagproof
wenzelm@44123: \isacommand{qed}\isamarkupfalse%
wenzelm@44123: %
wenzelm@44123: \endisatagproof
wenzelm@44123: {\isafoldproof}%
wenzelm@44123: %
wenzelm@44123: \isadelimproof
wenzelm@44123: \isanewline
wenzelm@44123: %
wenzelm@44123: \endisadelimproof
wenzelm@44123: \ \ \isacommand{term}\isamarkupfalse%
wenzelm@44123: \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44123: \ \ \isacommand{thm}\isamarkupfalse%
wenzelm@44123: \ this\isanewline
wenzelm@44123: \isacommand{end}\isamarkupfalse%
wenzelm@44123: %
wenzelm@44123: \begin{isamarkuptext}%
wenzelm@44123: Calculational reasoning maintains the special fact called
wenzelm@44123:   ``\isa{calculation}'' in the background.  Certain language
wenzelm@44123:   elements combine primary \isa{this} with secondary \isa{calculation}.%
wenzelm@44123: \end{isamarkuptext}%
wenzelm@44123: \isamarkuptrue%
wenzelm@44123: %
wenzelm@44123: \isamarkupsubsection{Transitive chains%
wenzelm@44123: }
wenzelm@44123: \isamarkuptrue%
wenzelm@44123: %
wenzelm@44123: \begin{isamarkuptext}%
wenzelm@44123: The Idea is to combine \isa{this} and \isa{calculation}
wenzelm@44123:   via typical \isa{trans} rules (see also \hyperlink{command.print-trans-rules}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}trans{\isaliteral{5F}{\isacharunderscore}}rules}}}}):%
wenzelm@44123: \end{isamarkuptext}%
wenzelm@44123: \isamarkuptrue%
wenzelm@44123: \isacommand{thm}\isamarkupfalse%
wenzelm@44123: \ trans\isanewline
wenzelm@44123: \isacommand{thm}\isamarkupfalse%
wenzelm@44123: \ less{\isaliteral{5F}{\isacharunderscore}}trans\isanewline
wenzelm@44123: \isacommand{thm}\isamarkupfalse%
wenzelm@44123: \ less{\isaliteral{5F}{\isacharunderscore}}le{\isaliteral{5F}{\isacharunderscore}}trans\isanewline
wenzelm@44123: \isanewline
wenzelm@44123: \isacommand{notepad}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \isakeyword{begin}%
wenzelm@44123: \isadelimproof
wenzelm@44123: %
wenzelm@44123: \endisadelimproof
wenzelm@44123: %
wenzelm@44123: \isatagproof
wenzelm@44123: %
wenzelm@44123: \begin{isamarkuptxt}%
wenzelm@44123: Plain bottom-up calculation:%
wenzelm@44123: \end{isamarkuptxt}%
wenzelm@44123: \isamarkuptrue%
wenzelm@44123: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123: \ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \ \ \isacommand{also}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123: \ {\isaliteral{22}{\isachardoublequoteopen}}b\ {\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \ \ \isacommand{also}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123: \ {\isaliteral{22}{\isachardoublequoteopen}}c\ {\isaliteral{3D}{\isacharequal}}\ d{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \ \ \isacommand{finally}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123: \ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3D}{\isacharequal}}\ d{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44123: %
wenzelm@44123: \begin{isamarkuptxt}%
wenzelm@44123: Variant using the \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} abbreviation:%
wenzelm@44123: \end{isamarkuptxt}%
wenzelm@44123: \isamarkuptrue%
wenzelm@44123: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123: \ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \ \ \isacommand{also}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123: \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \ \ \isacommand{also}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123: \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ d{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \ \ \isacommand{finally}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123: \ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3D}{\isacharequal}}\ d{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44123: %
wenzelm@44123: \begin{isamarkuptxt}%
wenzelm@44123: Top-down version with explicit claim at the head:%
wenzelm@44123: \end{isamarkuptxt}%
wenzelm@44123: \isamarkuptrue%
wenzelm@44123: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123: \ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3D}{\isacharequal}}\ d{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44123: \ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44123: \ {\isaliteral{2D}{\isacharminus}}\isanewline
wenzelm@44123: \ \ \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123: \ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \ \ \ \ \isacommand{also}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \ \ \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123: \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \ \ \ \ \isacommand{also}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \ \ \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123: \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ d{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \ \ \ \ \isacommand{finally}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44123: \ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \isacommand{next}\isamarkupfalse%
wenzelm@44123: %
wenzelm@44123: \begin{isamarkuptxt}%
wenzelm@44123: Mixed inequalities (require suitable base type):%
wenzelm@44123: \end{isamarkuptxt}%
wenzelm@44123: \isamarkuptrue%
wenzelm@44123: \ \ \isacommand{fix}\isamarkupfalse%
wenzelm@44123: \ a\ b\ c\ d\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\isanewline
wenzelm@44123: \isanewline
wenzelm@44123: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123: \ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3C}{\isacharless}}\ b{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \ \ \isacommand{also}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123: \ {\isaliteral{22}{\isachardoublequoteopen}}b{\isaliteral{5C3C6C653E}{\isasymle}}\ c{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \ \ \isacommand{also}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123: \ {\isaliteral{22}{\isachardoublequoteopen}}c\ {\isaliteral{3D}{\isacharequal}}\ d{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \ \ \isacommand{finally}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123: \ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3C}{\isacharless}}\ d{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44123: %
wenzelm@44123: \endisatagproof
wenzelm@44123: {\isafoldproof}%
wenzelm@44123: %
wenzelm@44123: \isadelimproof
wenzelm@44123: %
wenzelm@44123: \endisadelimproof
wenzelm@44123: \isanewline
wenzelm@44123: \isacommand{end}\isamarkupfalse%
wenzelm@44123: %
wenzelm@44123: \isamarkupsubsubsection{Notes%
wenzelm@44123: }
wenzelm@44123: \isamarkuptrue%
wenzelm@44123: %
wenzelm@44123: \begin{isamarkuptext}%
wenzelm@44123: \begin{itemize}
wenzelm@44123: 
wenzelm@44123:   \item The notion of \isa{trans} rule is very general due to the
wenzelm@44123:   flexibility of Isabelle/Pure rule composition.
wenzelm@44123: 
wenzelm@44123:   \item User applications may declare there own rules, with some care
wenzelm@44123:   about the operational details of higher-order unification.
wenzelm@44123: 
wenzelm@44123:   \end{itemize}%
wenzelm@44123: \end{isamarkuptext}%
wenzelm@44123: \isamarkuptrue%
wenzelm@44123: %
wenzelm@44123: \isamarkupsubsection{Degenerate calculations and bigstep reasoning%
wenzelm@44123: }
wenzelm@44123: \isamarkuptrue%
wenzelm@44123: %
wenzelm@44123: \begin{isamarkuptext}%
wenzelm@44123: The Idea is to append \isa{this} to \isa{calculation},
wenzelm@44123:   without rule composition.%
wenzelm@44123: \end{isamarkuptext}%
wenzelm@44123: \isamarkuptrue%
wenzelm@44123: \isacommand{notepad}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \isakeyword{begin}%
wenzelm@44123: \isadelimproof
wenzelm@44123: %
wenzelm@44123: \endisadelimproof
wenzelm@44123: %
wenzelm@44123: \isatagproof
wenzelm@44123: %
wenzelm@44123: \begin{isamarkuptxt}%
wenzelm@44124: A vacuous proof:%
wenzelm@44123: \end{isamarkuptxt}%
wenzelm@44123: \isamarkuptrue%
wenzelm@44123: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123: \ A\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \ \ \isacommand{moreover}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123: \ B\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \ \ \isacommand{moreover}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123: \ C\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \ \ \isacommand{ultimately}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123: \ A\ \isakeyword{and}\ B\ \isakeyword{and}\ C\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \isacommand{next}\isamarkupfalse%
wenzelm@44123: %
wenzelm@44123: \begin{isamarkuptxt}%
wenzelm@44123: Slightly more content (trivial bigstep reasoning):%
wenzelm@44123: \end{isamarkuptxt}%
wenzelm@44123: \isamarkuptrue%
wenzelm@44123: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123: \ A\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \ \ \isacommand{moreover}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123: \ B\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \ \ \isacommand{moreover}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123: \ C\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \ \ \isacommand{ultimately}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123: \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ C{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
wenzelm@44123: \ blast\isanewline
wenzelm@44123: \isacommand{next}\isamarkupfalse%
wenzelm@44123: %
wenzelm@44123: \begin{isamarkuptxt}%
wenzelm@44124: More ambitious bigstep reasoning involving structured results:%
wenzelm@44123: \end{isamarkuptxt}%
wenzelm@44123: \isamarkuptrue%
wenzelm@44123: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123: \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B\ {\isaliteral{5C3C6F723E}{\isasymor}}\ C{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \ \ \isacommand{moreover}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
wenzelm@44123: \ \isacommand{assume}\isamarkupfalse%
wenzelm@44123: \ A\ \isacommand{have}\isamarkupfalse%
wenzelm@44123: \ R\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44123: \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \ \ \isacommand{moreover}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
wenzelm@44123: \ \isacommand{assume}\isamarkupfalse%
wenzelm@44123: \ B\ \isacommand{have}\isamarkupfalse%
wenzelm@44123: \ R\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44123: \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \ \ \isacommand{moreover}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
wenzelm@44123: \ \isacommand{assume}\isamarkupfalse%
wenzelm@44123: \ C\ \isacommand{have}\isamarkupfalse%
wenzelm@44123: \ R\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44123: \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \ \ \isacommand{ultimately}\isamarkupfalse%
wenzelm@44123: \isanewline
wenzelm@44123: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123: \ R\ \isacommand{by}\isamarkupfalse%
wenzelm@44123: \ blast\ \ %
wenzelm@44123: \isamarkupcmt{``big-bang integration'' of proof blocks (occasionally fragile)%
wenzelm@44123: }
wenzelm@44123: %
wenzelm@44123: \endisatagproof
wenzelm@44123: {\isafoldproof}%
wenzelm@44123: %
wenzelm@44123: \isadelimproof
wenzelm@44123: %
wenzelm@44123: \endisadelimproof
wenzelm@44123: \isanewline
wenzelm@44123: \isacommand{end}\isamarkupfalse%
wenzelm@44124: %
wenzelm@44127: \isamarkupsection{Induction%
wenzelm@44125: }
wenzelm@44125: \isamarkuptrue%
wenzelm@44125: %
wenzelm@44125: \isamarkupsubsection{Induction as Natural Deduction%
wenzelm@44125: }
wenzelm@44125: \isamarkuptrue%
wenzelm@44125: %
wenzelm@44125: \begin{isamarkuptext}%
wenzelm@44125: In principle, induction is just a special case of Natural
wenzelm@44125:   Deduction (see also \secref{sec:natural-deduction-synopsis}).  For
wenzelm@44125:   example:%
wenzelm@44125: \end{isamarkuptext}%
wenzelm@44125: \isamarkuptrue%
wenzelm@44125: \isacommand{thm}\isamarkupfalse%
wenzelm@44125: \ nat{\isaliteral{2E}{\isachardot}}induct\isanewline
wenzelm@44125: \isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}\isamarkupfalse%
wenzelm@44125: \ nat{\isaliteral{2E}{\isachardot}}induct\isanewline
wenzelm@44125: \isanewline
wenzelm@44125: \isacommand{notepad}\isamarkupfalse%
wenzelm@44125: \isanewline
wenzelm@44125: \isakeyword{begin}\isanewline
wenzelm@44125: %
wenzelm@44125: \isadelimproof
wenzelm@44125: \ \ %
wenzelm@44125: \endisadelimproof
wenzelm@44125: %
wenzelm@44125: \isatagproof
wenzelm@44125: \isacommand{fix}\isamarkupfalse%
wenzelm@44125: \ n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\isanewline
wenzelm@44125: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{22}{\isachardoublequoteopen}}P\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44125: \ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{28}{\isacharparenleft}}rule\ nat{\isaliteral{2E}{\isachardot}}induct{\isaliteral{29}{\isacharparenright}}\ \ %
wenzelm@44125: \isamarkupcmt{fragile rule application!%
wenzelm@44125: }
wenzelm@44125: \isanewline
wenzelm@44125: \ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44125: \isanewline
wenzelm@44125: \ \ \isacommand{next}\isamarkupfalse%
wenzelm@44125: \isanewline
wenzelm@44125: \ \ \ \ \isacommand{fix}\isamarkupfalse%
wenzelm@44125: \ n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\isanewline
wenzelm@44125: \ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{22}{\isachardoublequoteopen}}P\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44125: \ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44125: \isanewline
wenzelm@44125: \ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44125: %
wenzelm@44125: \endisatagproof
wenzelm@44125: {\isafoldproof}%
wenzelm@44125: %
wenzelm@44125: \isadelimproof
wenzelm@44125: \isanewline
wenzelm@44125: %
wenzelm@44125: \endisadelimproof
wenzelm@44125: \isacommand{end}\isamarkupfalse%
wenzelm@44125: %
wenzelm@44125: \begin{isamarkuptext}%
wenzelm@44125: In practice, much more proof infrastructure is required.
wenzelm@44125: 
wenzelm@44125:   The proof method \hyperlink{method.induct}{\mbox{\isa{induct}}} provides:
wenzelm@44125:   \begin{itemize}
wenzelm@44125: 
wenzelm@44125:   \item implicit rule selection and robust instantiation
wenzelm@44125: 
wenzelm@44125:   \item context elements via symbolic case names
wenzelm@44125: 
wenzelm@44125:   \item support for rule-structured induction statements, with local
wenzelm@44125:     parameters, premises, etc.
wenzelm@44125: 
wenzelm@44125:   \end{itemize}%
wenzelm@44125: \end{isamarkuptext}%
wenzelm@44125: \isamarkuptrue%
wenzelm@44125: \isacommand{notepad}\isamarkupfalse%
wenzelm@44125: \isanewline
wenzelm@44125: \isakeyword{begin}\isanewline
wenzelm@44125: %
wenzelm@44125: \isadelimproof
wenzelm@44125: \ \ %
wenzelm@44125: \endisadelimproof
wenzelm@44125: %
wenzelm@44125: \isatagproof
wenzelm@44125: \isacommand{fix}\isamarkupfalse%
wenzelm@44125: \ n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\isanewline
wenzelm@44125: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{22}{\isachardoublequoteopen}}P\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44125: \ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{28}{\isacharparenleft}}induct\ n{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44125: \ \ \ \ \isacommand{case}\isamarkupfalse%
wenzelm@44125: \ {\isadigit{0}}\isanewline
wenzelm@44125: \ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{3F}{\isacharquery}}case\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44125: \isanewline
wenzelm@44125: \ \ \isacommand{next}\isamarkupfalse%
wenzelm@44125: \isanewline
wenzelm@44125: \ \ \ \ \isacommand{case}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44125: \ \ \ \ \isacommand{from}\isamarkupfalse%
wenzelm@44125: \ Suc{\isaliteral{2E}{\isachardot}}hyps\ \isacommand{show}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{3F}{\isacharquery}}case\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44125: \isanewline
wenzelm@44125: \ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44125: %
wenzelm@44125: \endisatagproof
wenzelm@44125: {\isafoldproof}%
wenzelm@44125: %
wenzelm@44125: \isadelimproof
wenzelm@44125: \isanewline
wenzelm@44125: %
wenzelm@44125: \endisadelimproof
wenzelm@44125: \isacommand{end}\isamarkupfalse%
wenzelm@44125: %
wenzelm@44125: \isamarkupsubsubsection{Example%
wenzelm@44125: }
wenzelm@44125: \isamarkuptrue%
wenzelm@44125: %
wenzelm@44125: \begin{isamarkuptext}%
wenzelm@44125: The subsequent example combines the following proof patterns:
wenzelm@44125:   \begin{itemize}
wenzelm@44125: 
wenzelm@44125:   \item outermost induction (over the datatype structure of natural
wenzelm@44125:   numbers), to decompose the proof problem in top-down manner
wenzelm@44125: 
wenzelm@44125:   \item calculational reasoning (\secref{sec:calculations-synopsis})
wenzelm@44125:   to compose the result in each case
wenzelm@44125: 
wenzelm@44125:   \item solving local claims within the calculation by simplification
wenzelm@44125: 
wenzelm@44125:   \end{itemize}%
wenzelm@44125: \end{isamarkuptext}%
wenzelm@44125: \isamarkuptrue%
wenzelm@44125: \isacommand{lemma}\isamarkupfalse%
wenzelm@44125: \isanewline
wenzelm@44125: \ \ \isakeyword{fixes}\ n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\isanewline
wenzelm@44125: \ \ \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
wenzelm@44125: %
wenzelm@44125: \isadelimproof
wenzelm@44125: %
wenzelm@44125: \endisadelimproof
wenzelm@44125: %
wenzelm@44125: \isatagproof
wenzelm@44125: \isacommand{proof}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{28}{\isacharparenleft}}induct\ n{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44125: \ \ \isacommand{case}\isamarkupfalse%
wenzelm@44125: \ {\isadigit{0}}\isanewline
wenzelm@44125: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44125: \ {\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%
wenzelm@44125: \ simp\isanewline
wenzelm@44125: \ \ \isacommand{also}\isamarkupfalse%
wenzelm@44125: \ \isacommand{have}\isamarkupfalse%
wenzelm@44125: \ {\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%
wenzelm@44125: \ simp\isanewline
wenzelm@44125: \ \ \isacommand{finally}\isamarkupfalse%
wenzelm@44125: \ \isacommand{show}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{3F}{\isacharquery}}case\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44125: \isanewline
wenzelm@44125: \isacommand{next}\isamarkupfalse%
wenzelm@44125: \isanewline
wenzelm@44125: \ \ \isacommand{case}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44125: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44125: \ {\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%
wenzelm@44125: \ simp\isanewline
wenzelm@44125: \ \ \isacommand{also}\isamarkupfalse%
wenzelm@44125: \ \isacommand{have}\isamarkupfalse%
wenzelm@44125: \ {\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%
wenzelm@44125: \ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ Suc{\isaliteral{2E}{\isachardot}}hyps{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44125: \ \ \isacommand{also}\isamarkupfalse%
wenzelm@44125: \ \isacommand{have}\isamarkupfalse%
wenzelm@44125: \ {\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%
wenzelm@44125: \ simp\isanewline
wenzelm@44125: \ \ \isacommand{also}\isamarkupfalse%
wenzelm@44125: \ \isacommand{have}\isamarkupfalse%
wenzelm@44125: \ {\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%
wenzelm@44125: \ simp\isanewline
wenzelm@44125: \ \ \isacommand{finally}\isamarkupfalse%
wenzelm@44125: \ \isacommand{show}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{3F}{\isacharquery}}case\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44125: \isanewline
wenzelm@44125: \isacommand{qed}\isamarkupfalse%
wenzelm@44125: %
wenzelm@44125: \endisatagproof
wenzelm@44125: {\isafoldproof}%
wenzelm@44125: %
wenzelm@44125: \isadelimproof
wenzelm@44125: %
wenzelm@44125: \endisadelimproof
wenzelm@44125: %
wenzelm@44125: \begin{isamarkuptext}%
wenzelm@44125: This demonstrates how induction proofs can be done without
wenzelm@44125:   having to consider the raw Natural Deduction structure.%
wenzelm@44125: \end{isamarkuptext}%
wenzelm@44125: \isamarkuptrue%
wenzelm@44125: %
wenzelm@44125: \isamarkupsubsection{Induction with local parameters and premises%
wenzelm@44125: }
wenzelm@44125: \isamarkuptrue%
wenzelm@44125: %
wenzelm@44125: \begin{isamarkuptext}%
wenzelm@44125: Idea: Pure rule statements are passed through the induction
wenzelm@44125:   rule.  This achieves convenient proof patterns, thanks to some
wenzelm@44125:   internal trickery in the \hyperlink{method.induct}{\mbox{\isa{induct}}} method.
wenzelm@44125: 
wenzelm@44125:   Important: Using compact HOL formulae with \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}{\isaliteral{22}{\isachardoublequote}}} is a
wenzelm@44125:   well-known anti-pattern! It would produce useless formal noise.%
wenzelm@44125: \end{isamarkuptext}%
wenzelm@44125: \isamarkuptrue%
wenzelm@44125: \isacommand{notepad}\isamarkupfalse%
wenzelm@44125: \isanewline
wenzelm@44125: \isakeyword{begin}\isanewline
wenzelm@44125: %
wenzelm@44125: \isadelimproof
wenzelm@44125: \ \ %
wenzelm@44125: \endisadelimproof
wenzelm@44125: %
wenzelm@44125: \isatagproof
wenzelm@44125: \isacommand{fix}\isamarkupfalse%
wenzelm@44125: \ n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\isanewline
wenzelm@44125: \ \ \isacommand{fix}\isamarkupfalse%
wenzelm@44125: \ P\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44125: \ \ \isacommand{fix}\isamarkupfalse%
wenzelm@44125: \ 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
wenzelm@44125: \isanewline
wenzelm@44125: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{22}{\isachardoublequoteopen}}P\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44125: \ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{28}{\isacharparenleft}}induct\ n{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44125: \ \ \ \ \isacommand{case}\isamarkupfalse%
wenzelm@44125: \ {\isadigit{0}}\isanewline
wenzelm@44125: \ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44125: \isanewline
wenzelm@44125: \ \ \isacommand{next}\isamarkupfalse%
wenzelm@44125: \isanewline
wenzelm@44125: \ \ \ \ \isacommand{case}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44125: \ \ \ \ \isacommand{from}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{60}{\isacharbackquoteopen}}P\ n{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44125: \isanewline
wenzelm@44125: \ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44125: \isanewline
wenzelm@44125: \isanewline
wenzelm@44125: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{22}{\isachardoublequoteopen}}A\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44125: \ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{28}{\isacharparenleft}}induct\ n{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44125: \ \ \ \ \isacommand{case}\isamarkupfalse%
wenzelm@44125: \ {\isadigit{0}}\isanewline
wenzelm@44125: \ \ \ \ \isacommand{from}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{60}{\isacharbackquoteopen}}A\ {\isadigit{0}}{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44125: \isanewline
wenzelm@44125: \ \ \isacommand{next}\isamarkupfalse%
wenzelm@44125: \isanewline
wenzelm@44125: \ \ \ \ \isacommand{case}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44125: \ \ \ \ \isacommand{from}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{60}{\isacharbackquoteopen}}A\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ n{\isaliteral{60}{\isacharbackquoteclose}}\isanewline
wenzelm@44125: \ \ \ \ \ \ \isakeyword{and}\ {\isaliteral{60}{\isacharbackquoteopen}}A\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44125: \isanewline
wenzelm@44125: \ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44125: \isanewline
wenzelm@44125: \isanewline
wenzelm@44125: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ Q\ x\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44125: \ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{28}{\isacharparenleft}}induct\ n{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44125: \ \ \ \ \isacommand{case}\isamarkupfalse%
wenzelm@44125: \ {\isadigit{0}}\isanewline
wenzelm@44125: \ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{22}{\isachardoublequoteopen}}Q\ x\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44125: \isanewline
wenzelm@44125: \ \ \isacommand{next}\isamarkupfalse%
wenzelm@44125: \isanewline
wenzelm@44125: \ \ \ \ \isacommand{case}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44125: \ \ \ \ \isacommand{from}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{60}{\isacharbackquoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ Q\ x\ n{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{22}{\isachardoublequoteopen}}Q\ x\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44125: %
wenzelm@44125: \begin{isamarkuptxt}%
wenzelm@44125: Local quantification admits arbitrary instances:%
wenzelm@44125: \end{isamarkuptxt}%
wenzelm@44125: \isamarkuptrue%
wenzelm@44125: \ \ \ \ \isacommand{note}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{60}{\isacharbackquoteopen}}Q\ a\ n{\isaliteral{60}{\isacharbackquoteclose}}\ \isakeyword{and}\ {\isaliteral{60}{\isacharbackquoteopen}}Q\ b\ n{\isaliteral{60}{\isacharbackquoteclose}}\isanewline
wenzelm@44125: \ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44125: %
wenzelm@44125: \endisatagproof
wenzelm@44125: {\isafoldproof}%
wenzelm@44125: %
wenzelm@44125: \isadelimproof
wenzelm@44125: \isanewline
wenzelm@44125: %
wenzelm@44125: \endisadelimproof
wenzelm@44125: \isacommand{end}\isamarkupfalse%
wenzelm@44125: %
wenzelm@44125: \isamarkupsubsection{Implicit induction context%
wenzelm@44125: }
wenzelm@44125: \isamarkuptrue%
wenzelm@44125: %
wenzelm@44125: \begin{isamarkuptext}%
wenzelm@44125: The \hyperlink{method.induct}{\mbox{\isa{induct}}} method can isolate local parameters and
wenzelm@44125:   premises directly from the given statement.  This is convenient in
wenzelm@44125:   practical applications, but requires some understanding of what is
wenzelm@44125:   going on internally (as explained above).%
wenzelm@44125: \end{isamarkuptext}%
wenzelm@44125: \isamarkuptrue%
wenzelm@44125: \isacommand{notepad}\isamarkupfalse%
wenzelm@44125: \isanewline
wenzelm@44125: \isakeyword{begin}\isanewline
wenzelm@44125: %
wenzelm@44125: \isadelimproof
wenzelm@44125: \ \ %
wenzelm@44125: \endisadelimproof
wenzelm@44125: %
wenzelm@44125: \isatagproof
wenzelm@44125: \isacommand{fix}\isamarkupfalse%
wenzelm@44125: \ n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\isanewline
wenzelm@44125: \ \ \isacommand{fix}\isamarkupfalse%
wenzelm@44125: \ 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
wenzelm@44125: \isanewline
wenzelm@44125: \ \ \isacommand{fix}\isamarkupfalse%
wenzelm@44125: \ x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\isanewline
wenzelm@44125: \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{22}{\isachardoublequoteopen}}A\ x\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44125: \ \ \isacommand{then}\isamarkupfalse%
wenzelm@44125: \ \isacommand{have}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{22}{\isachardoublequoteopen}}Q\ x\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44125: \ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{28}{\isacharparenleft}}induct\ n\ arbitrary{\isaliteral{3A}{\isacharcolon}}\ x{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44125: \ \ \ \ \isacommand{case}\isamarkupfalse%
wenzelm@44125: \ {\isadigit{0}}\isanewline
wenzelm@44125: \ \ \ \ \isacommand{from}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{60}{\isacharbackquoteopen}}A\ x\ {\isadigit{0}}{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{22}{\isachardoublequoteopen}}Q\ x\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44125: \isanewline
wenzelm@44125: \ \ \isacommand{next}\isamarkupfalse%
wenzelm@44125: \isanewline
wenzelm@44125: \ \ \ \ \isacommand{case}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44125: \ \ \ \ \isacommand{from}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{60}{\isacharbackquoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ A\ x\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q\ x\ n{\isaliteral{60}{\isacharbackquoteclose}}\ \ %
wenzelm@44125: \isamarkupcmt{arbitrary instances can be produced here%
wenzelm@44125: }
wenzelm@44125: \isanewline
wenzelm@44125: \ \ \ \ \ \ \isakeyword{and}\ {\isaliteral{60}{\isacharbackquoteopen}}A\ x\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{22}{\isachardoublequoteopen}}Q\ x\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44125: \isanewline
wenzelm@44125: \ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44125: %
wenzelm@44125: \endisatagproof
wenzelm@44125: {\isafoldproof}%
wenzelm@44125: %
wenzelm@44125: \isadelimproof
wenzelm@44125: \isanewline
wenzelm@44125: %
wenzelm@44125: \endisadelimproof
wenzelm@44125: \isacommand{end}\isamarkupfalse%
wenzelm@44125: %
wenzelm@44125: \isamarkupsubsection{Advanced induction with term definitions%
wenzelm@44125: }
wenzelm@44125: \isamarkuptrue%
wenzelm@44125: %
wenzelm@44125: \begin{isamarkuptext}%
wenzelm@44125: Induction over subexpressions of a certain shape are delicate
wenzelm@44125:   to formalize.  The Isar \hyperlink{method.induct}{\mbox{\isa{induct}}} method provides
wenzelm@44125:   infrastructure for this.
wenzelm@44125: 
wenzelm@44125:   Idea: sub-expressions of the problem are turned into a defined
wenzelm@44125:   induction variable; often accompanied with fixing of auxiliary
wenzelm@44125:   parameters in the original expression.%
wenzelm@44125: \end{isamarkuptext}%
wenzelm@44125: \isamarkuptrue%
wenzelm@44125: \isacommand{notepad}\isamarkupfalse%
wenzelm@44125: \isanewline
wenzelm@44125: \isakeyword{begin}\isanewline
wenzelm@44125: %
wenzelm@44125: \isadelimproof
wenzelm@44125: \ \ %
wenzelm@44125: \endisadelimproof
wenzelm@44125: %
wenzelm@44125: \isatagproof
wenzelm@44125: \isacommand{fix}\isamarkupfalse%
wenzelm@44125: \ a\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44125: \ \ \isacommand{fix}\isamarkupfalse%
wenzelm@44125: \ A\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44125: \isanewline
wenzelm@44125: \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{28}{\isacharparenleft}}a\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44125: \ \ \isacommand{then}\isamarkupfalse%
wenzelm@44125: \ \isacommand{have}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{28}{\isacharparenleft}}a\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44125: \ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{28}{\isacharparenleft}}induct\ {\isaliteral{22}{\isachardoublequoteopen}}a\ x{\isaliteral{22}{\isachardoublequoteclose}}\ arbitrary{\isaliteral{3A}{\isacharcolon}}\ x{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44125: \ \ \ \ \isacommand{case}\isamarkupfalse%
wenzelm@44125: \ {\isadigit{0}}\isanewline
wenzelm@44125: \ \ \ \ \isacommand{note}\isamarkupfalse%
wenzelm@44125: \ prem\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{60}{\isacharbackquoteopen}}A\ {\isaliteral{28}{\isacharparenleft}}a\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{60}{\isacharbackquoteclose}}\isanewline
wenzelm@44125: \ \ \ \ \ \ \isakeyword{and}\ defn\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{60}{\isacharbackquoteopen}}{\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ a\ x{\isaliteral{60}{\isacharbackquoteclose}}\isanewline
wenzelm@44125: \ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{28}{\isacharparenleft}}a\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44125: \isanewline
wenzelm@44125: \ \ \isacommand{next}\isamarkupfalse%
wenzelm@44125: \isanewline
wenzelm@44125: \ \ \ \ \isacommand{case}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44125: \ \ \ \ \isacommand{note}\isamarkupfalse%
wenzelm@44125: \ 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
wenzelm@44125: \ \ \ \ \ \ \isakeyword{and}\ prem\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{60}{\isacharbackquoteopen}}A\ {\isaliteral{28}{\isacharparenleft}}a\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{60}{\isacharbackquoteclose}}\isanewline
wenzelm@44125: \ \ \ \ \ \ \isakeyword{and}\ defn\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{60}{\isacharbackquoteopen}}Suc\ n\ {\isaliteral{3D}{\isacharequal}}\ a\ x{\isaliteral{60}{\isacharbackquoteclose}}\isanewline
wenzelm@44125: \ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44125: \ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{28}{\isacharparenleft}}a\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44125: \isanewline
wenzelm@44125: \ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44125: %
wenzelm@44125: \endisatagproof
wenzelm@44125: {\isafoldproof}%
wenzelm@44125: %
wenzelm@44125: \isadelimproof
wenzelm@44125: \isanewline
wenzelm@44125: %
wenzelm@44125: \endisadelimproof
wenzelm@44125: \isacommand{end}\isamarkupfalse%
wenzelm@44125: %
wenzelm@44127: \isamarkupsection{Natural Deduction \label{sec:natural-deduction-synopsis}%
wenzelm@44124: }
wenzelm@44124: \isamarkuptrue%
wenzelm@44124: %
wenzelm@44124: \isamarkupsubsection{Rule statements%
wenzelm@44124: }
wenzelm@44124: \isamarkuptrue%
wenzelm@44124: %
wenzelm@44124: \begin{isamarkuptext}%
wenzelm@44124: Isabelle/Pure ``theorems'' are always natural deduction rules,
wenzelm@44124:   which sometimes happen to consist of a conclusion only.
wenzelm@44124: 
wenzelm@44124:   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
wenzelm@44124:   rule structure declaratively.  For example:%
wenzelm@44124: \end{isamarkuptext}%
wenzelm@44124: \isamarkuptrue%
wenzelm@44124: \isacommand{thm}\isamarkupfalse%
wenzelm@44124: \ conjI\isanewline
wenzelm@44124: \isacommand{thm}\isamarkupfalse%
wenzelm@44124: \ impI\isanewline
wenzelm@44124: \isacommand{thm}\isamarkupfalse%
wenzelm@44124: \ nat{\isaliteral{2E}{\isachardot}}induct%
wenzelm@44124: \begin{isamarkuptext}%
wenzelm@44124: The object-logic is embedded into the Pure framework via an implicit
wenzelm@44124:   derivability judgment \isa{{\isaliteral{22}{\isachardoublequote}}Trueprop\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ bool\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ prop{\isaliteral{22}{\isachardoublequote}}}.
wenzelm@44124: 
wenzelm@44124:   Thus any HOL formulae appears atomic to the Pure framework, while
wenzelm@44124:   the rule structure outlines the corresponding proof pattern.
wenzelm@44124: 
wenzelm@44124:   This can be made explicit as follows:%
wenzelm@44124: \end{isamarkuptext}%
wenzelm@44124: \isamarkuptrue%
wenzelm@44124: \isacommand{notepad}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \isakeyword{begin}\isanewline
wenzelm@44124: %
wenzelm@44124: \isadelimproof
wenzelm@44124: \ \ %
wenzelm@44124: \endisadelimproof
wenzelm@44124: %
wenzelm@44124: \isatagproof
wenzelm@44124: \isacommand{write}\isamarkupfalse%
wenzelm@44124: \ Trueprop\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}Tr{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}%
wenzelm@44124: \endisatagproof
wenzelm@44124: {\isafoldproof}%
wenzelm@44124: %
wenzelm@44124: \isadelimproof
wenzelm@44124: \isanewline
wenzelm@44124: %
wenzelm@44124: \endisadelimproof
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{thm}\isamarkupfalse%
wenzelm@44124: \ conjI\isanewline
wenzelm@44124: \ \ \isacommand{thm}\isamarkupfalse%
wenzelm@44124: \ impI\isanewline
wenzelm@44124: \ \ \isacommand{thm}\isamarkupfalse%
wenzelm@44124: \ nat{\isaliteral{2E}{\isachardot}}induct\isanewline
wenzelm@44124: \isacommand{end}\isamarkupfalse%
wenzelm@44124: %
wenzelm@44124: \begin{isamarkuptext}%
wenzelm@44124: Isar provides first-class notation for rule statements as follows.%
wenzelm@44124: \end{isamarkuptext}%
wenzelm@44124: \isamarkuptrue%
wenzelm@44124: \isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}\isamarkupfalse%
wenzelm@44124: \ conjI\isanewline
wenzelm@44124: \isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}\isamarkupfalse%
wenzelm@44124: \ impI\isanewline
wenzelm@44124: \isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}\isamarkupfalse%
wenzelm@44124: \ nat{\isaliteral{2E}{\isachardot}}induct%
wenzelm@44124: \isamarkupsubsubsection{Examples%
wenzelm@44124: }
wenzelm@44124: \isamarkuptrue%
wenzelm@44124: %
wenzelm@44124: \begin{isamarkuptext}%
wenzelm@44124: Introductions and eliminations of some standard connectives of
wenzelm@44124:   the object-logic can be written as rule statements as follows.  (The
wenzelm@44124:   proof ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\hyperlink{method.blast}{\mbox{\isa{blast}}}'' serves as sanity check.)%
wenzelm@44124: \end{isamarkuptext}%
wenzelm@44124: \isamarkuptrue%
wenzelm@44124: \isacommand{lemma}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ False{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P{\isaliteral{22}{\isachardoublequoteclose}}%
wenzelm@44124: \isadelimproof
wenzelm@44124: \ %
wenzelm@44124: \endisadelimproof
wenzelm@44124: %
wenzelm@44124: \isatagproof
wenzelm@44124: \isacommand{by}\isamarkupfalse%
wenzelm@44124: \ blast%
wenzelm@44124: \endisatagproof
wenzelm@44124: {\isafoldproof}%
wenzelm@44124: %
wenzelm@44124: \isadelimproof
wenzelm@44124: %
wenzelm@44124: \endisadelimproof
wenzelm@44124: \isanewline
wenzelm@44124: \isacommand{lemma}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q{\isaliteral{22}{\isachardoublequoteclose}}%
wenzelm@44124: \isadelimproof
wenzelm@44124: \ %
wenzelm@44124: \endisadelimproof
wenzelm@44124: %
wenzelm@44124: \isatagproof
wenzelm@44124: \isacommand{by}\isamarkupfalse%
wenzelm@44124: \ blast%
wenzelm@44124: \endisatagproof
wenzelm@44124: {\isafoldproof}%
wenzelm@44124: %
wenzelm@44124: \isadelimproof
wenzelm@44124: %
wenzelm@44124: \endisadelimproof
wenzelm@44124: \isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \isacommand{lemma}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q{\isaliteral{22}{\isachardoublequoteclose}}%
wenzelm@44124: \isadelimproof
wenzelm@44124: \ %
wenzelm@44124: \endisadelimproof
wenzelm@44124: %
wenzelm@44124: \isatagproof
wenzelm@44124: \isacommand{by}\isamarkupfalse%
wenzelm@44124: \ blast%
wenzelm@44124: \endisatagproof
wenzelm@44124: {\isafoldproof}%
wenzelm@44124: %
wenzelm@44124: \isadelimproof
wenzelm@44124: %
wenzelm@44124: \endisadelimproof
wenzelm@44124: \isanewline
wenzelm@44124: \isacommand{lemma}\isamarkupfalse%
wenzelm@44124: \ {\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}}%
wenzelm@44124: \isadelimproof
wenzelm@44124: \ %
wenzelm@44124: \endisadelimproof
wenzelm@44124: %
wenzelm@44124: \isatagproof
wenzelm@44124: \isacommand{by}\isamarkupfalse%
wenzelm@44124: \ blast%
wenzelm@44124: \endisatagproof
wenzelm@44124: {\isafoldproof}%
wenzelm@44124: %
wenzelm@44124: \isadelimproof
wenzelm@44124: %
wenzelm@44124: \endisadelimproof
wenzelm@44124: \isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \isacommand{lemma}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q{\isaliteral{22}{\isachardoublequoteclose}}%
wenzelm@44124: \isadelimproof
wenzelm@44124: \ %
wenzelm@44124: \endisadelimproof
wenzelm@44124: %
wenzelm@44124: \isatagproof
wenzelm@44124: \isacommand{by}\isamarkupfalse%
wenzelm@44124: \ blast%
wenzelm@44124: \endisatagproof
wenzelm@44124: {\isafoldproof}%
wenzelm@44124: %
wenzelm@44124: \isadelimproof
wenzelm@44124: %
wenzelm@44124: \endisadelimproof
wenzelm@44124: \isanewline
wenzelm@44124: \isacommand{lemma}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}Q\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q{\isaliteral{22}{\isachardoublequoteclose}}%
wenzelm@44124: \isadelimproof
wenzelm@44124: \ %
wenzelm@44124: \endisadelimproof
wenzelm@44124: %
wenzelm@44124: \isatagproof
wenzelm@44124: \isacommand{by}\isamarkupfalse%
wenzelm@44124: \ blast%
wenzelm@44124: \endisatagproof
wenzelm@44124: {\isafoldproof}%
wenzelm@44124: %
wenzelm@44124: \isadelimproof
wenzelm@44124: %
wenzelm@44124: \endisadelimproof
wenzelm@44124: \isanewline
wenzelm@44124: \isacommand{lemma}\isamarkupfalse%
wenzelm@44124: \ {\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}}%
wenzelm@44124: \isadelimproof
wenzelm@44124: \ %
wenzelm@44124: \endisadelimproof
wenzelm@44124: %
wenzelm@44124: \isatagproof
wenzelm@44124: \isacommand{by}\isamarkupfalse%
wenzelm@44124: \ blast%
wenzelm@44124: \endisatagproof
wenzelm@44124: {\isafoldproof}%
wenzelm@44124: %
wenzelm@44124: \isadelimproof
wenzelm@44124: %
wenzelm@44124: \endisadelimproof
wenzelm@44124: \isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \isacommand{lemma}\isamarkupfalse%
wenzelm@44124: \ {\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}}%
wenzelm@44124: \isadelimproof
wenzelm@44124: \ %
wenzelm@44124: \endisadelimproof
wenzelm@44124: %
wenzelm@44124: \isatagproof
wenzelm@44124: \isacommand{by}\isamarkupfalse%
wenzelm@44124: \ blast%
wenzelm@44124: \endisatagproof
wenzelm@44124: {\isafoldproof}%
wenzelm@44124: %
wenzelm@44124: \isadelimproof
wenzelm@44124: %
wenzelm@44124: \endisadelimproof
wenzelm@44124: \isanewline
wenzelm@44124: \isacommand{lemma}\isamarkupfalse%
wenzelm@44124: \ {\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}}%
wenzelm@44124: \isadelimproof
wenzelm@44124: \ %
wenzelm@44124: \endisadelimproof
wenzelm@44124: %
wenzelm@44124: \isatagproof
wenzelm@44124: \isacommand{by}\isamarkupfalse%
wenzelm@44124: \ blast%
wenzelm@44124: \endisatagproof
wenzelm@44124: {\isafoldproof}%
wenzelm@44124: %
wenzelm@44124: \isadelimproof
wenzelm@44124: %
wenzelm@44124: \endisadelimproof
wenzelm@44124: \isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \isacommand{lemma}\isamarkupfalse%
wenzelm@44124: \ {\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}}%
wenzelm@44124: \isadelimproof
wenzelm@44124: \ %
wenzelm@44124: \endisadelimproof
wenzelm@44124: %
wenzelm@44124: \isatagproof
wenzelm@44124: \isacommand{by}\isamarkupfalse%
wenzelm@44124: \ blast%
wenzelm@44124: \endisatagproof
wenzelm@44124: {\isafoldproof}%
wenzelm@44124: %
wenzelm@44124: \isadelimproof
wenzelm@44124: %
wenzelm@44124: \endisadelimproof
wenzelm@44124: \isanewline
wenzelm@44124: \isacommand{lemma}\isamarkupfalse%
wenzelm@44124: \ {\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}}%
wenzelm@44124: \isadelimproof
wenzelm@44124: \ %
wenzelm@44124: \endisadelimproof
wenzelm@44124: %
wenzelm@44124: \isatagproof
wenzelm@44124: \isacommand{by}\isamarkupfalse%
wenzelm@44124: \ blast%
wenzelm@44124: \endisatagproof
wenzelm@44124: {\isafoldproof}%
wenzelm@44124: %
wenzelm@44124: \isadelimproof
wenzelm@44124: %
wenzelm@44124: \endisadelimproof
wenzelm@44124: \isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \isacommand{lemma}\isamarkupfalse%
wenzelm@44124: \ {\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}}%
wenzelm@44124: \isadelimproof
wenzelm@44124: \ %
wenzelm@44124: \endisadelimproof
wenzelm@44124: %
wenzelm@44124: \isatagproof
wenzelm@44124: \isacommand{by}\isamarkupfalse%
wenzelm@44124: \ blast%
wenzelm@44124: \endisatagproof
wenzelm@44124: {\isafoldproof}%
wenzelm@44124: %
wenzelm@44124: \isadelimproof
wenzelm@44124: %
wenzelm@44124: \endisadelimproof
wenzelm@44124: \isanewline
wenzelm@44124: \isacommand{lemma}\isamarkupfalse%
wenzelm@44124: \ {\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}}%
wenzelm@44124: \isadelimproof
wenzelm@44124: \ %
wenzelm@44124: \endisadelimproof
wenzelm@44124: %
wenzelm@44124: \isatagproof
wenzelm@44124: \isacommand{by}\isamarkupfalse%
wenzelm@44124: \ blast%
wenzelm@44124: \endisatagproof
wenzelm@44124: {\isafoldproof}%
wenzelm@44124: %
wenzelm@44124: \isadelimproof
wenzelm@44124: %
wenzelm@44124: \endisadelimproof
wenzelm@44124: \isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \isacommand{lemma}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ B{\isaliteral{22}{\isachardoublequoteclose}}%
wenzelm@44124: \isadelimproof
wenzelm@44124: \ %
wenzelm@44124: \endisadelimproof
wenzelm@44124: %
wenzelm@44124: \isatagproof
wenzelm@44124: \isacommand{by}\isamarkupfalse%
wenzelm@44124: \ blast%
wenzelm@44124: \endisatagproof
wenzelm@44124: {\isafoldproof}%
wenzelm@44124: %
wenzelm@44124: \isadelimproof
wenzelm@44124: %
wenzelm@44124: \endisadelimproof
wenzelm@44124: \isanewline
wenzelm@44124: \isacommand{lemma}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ B{\isaliteral{22}{\isachardoublequoteclose}}%
wenzelm@44124: \isadelimproof
wenzelm@44124: \ %
wenzelm@44124: \endisadelimproof
wenzelm@44124: %
wenzelm@44124: \isatagproof
wenzelm@44124: \isacommand{by}\isamarkupfalse%
wenzelm@44124: \ blast%
wenzelm@44124: \endisatagproof
wenzelm@44124: {\isafoldproof}%
wenzelm@44124: %
wenzelm@44124: \isadelimproof
wenzelm@44124: %
wenzelm@44124: \endisadelimproof
wenzelm@44124: \isanewline
wenzelm@44124: \isacommand{lemma}\isamarkupfalse%
wenzelm@44124: \ {\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}}%
wenzelm@44124: \isadelimproof
wenzelm@44124: \ %
wenzelm@44124: \endisadelimproof
wenzelm@44124: %
wenzelm@44124: \isatagproof
wenzelm@44124: \isacommand{by}\isamarkupfalse%
wenzelm@44124: \ blast%
wenzelm@44124: \endisatagproof
wenzelm@44124: {\isafoldproof}%
wenzelm@44124: %
wenzelm@44124: \isadelimproof
wenzelm@44124: %
wenzelm@44124: \endisadelimproof
wenzelm@44124: %
wenzelm@44124: \isamarkupsubsection{Isar context elements%
wenzelm@44124: }
wenzelm@44124: \isamarkuptrue%
wenzelm@44124: %
wenzelm@44124: \begin{isamarkuptext}%
wenzelm@44124: We derive some results out of the blue, using Isar context
wenzelm@44124:   elements and some explicit blocks.  This illustrates their meaning
wenzelm@44124:   wrt.\ Pure connectives, without goal states getting in the way.%
wenzelm@44124: \end{isamarkuptext}%
wenzelm@44124: \isamarkuptrue%
wenzelm@44124: \isacommand{notepad}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \isakeyword{begin}\isanewline
wenzelm@44124: %
wenzelm@44124: \isadelimproof
wenzelm@44124: \ \ %
wenzelm@44124: \endisadelimproof
wenzelm@44124: %
wenzelm@44124: \isatagproof
wenzelm@44124: \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \ \ \isacommand{fix}\isamarkupfalse%
wenzelm@44124: \ x\isanewline
wenzelm@44124: \ \ \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
wenzelm@44124: \ fact\isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \isacommand{next}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44124: \ A\isanewline
wenzelm@44124: \ \ \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ B\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
wenzelm@44124: \ fact\isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \isacommand{next}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \ \ \isacommand{def}\isamarkupfalse%
wenzelm@44124: \ x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t\isanewline
wenzelm@44124: \ \ \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}B\ t{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
wenzelm@44124: \ fact\isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \isacommand{next}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \ \ \isacommand{obtain}\isamarkupfalse%
wenzelm@44124: \ x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ C\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ C\ \isacommand{by}\isamarkupfalse%
wenzelm@44124: \ fact%
wenzelm@44124: \endisatagproof
wenzelm@44124: {\isafoldproof}%
wenzelm@44124: %
wenzelm@44124: \isadelimproof
wenzelm@44124: \isanewline
wenzelm@44124: %
wenzelm@44124: \endisadelimproof
wenzelm@44124: \isanewline
wenzelm@44124: \isacommand{end}\isamarkupfalse%
wenzelm@44124: %
wenzelm@44124: \isamarkupsubsection{Pure rule composition%
wenzelm@44124: }
wenzelm@44124: \isamarkuptrue%
wenzelm@44124: %
wenzelm@44124: \begin{isamarkuptext}%
wenzelm@44124: The Pure framework provides means for:
wenzelm@44124: 
wenzelm@44124:   \begin{itemize}
wenzelm@44124: 
wenzelm@44124:     \item backward-chaining of rules by \hyperlink{inference.resolution}{\mbox{\isa{resolution}}}
wenzelm@44124: 
wenzelm@44124:     \item closing of branches by \hyperlink{inference.assumption}{\mbox{\isa{assumption}}}
wenzelm@44124: 
wenzelm@44124:   \end{itemize}
wenzelm@44124: 
wenzelm@44124:   Both principles involve higher-order unification of \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}}-terms
wenzelm@44124:   modulo \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C626574613E}{\isasymbeta}}{\isaliteral{5C3C6574613E}{\isasymeta}}{\isaliteral{22}{\isachardoublequote}}}-equivalence (cf.\ Huet and Miller).%
wenzelm@44124: \end{isamarkuptext}%
wenzelm@44124: \isamarkuptrue%
wenzelm@44124: \isacommand{notepad}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \isakeyword{begin}\isanewline
wenzelm@44124: %
wenzelm@44124: \isadelimproof
wenzelm@44124: \ \ %
wenzelm@44124: \endisadelimproof
wenzelm@44124: %
wenzelm@44124: \isatagproof
wenzelm@44124: \isacommand{assume}\isamarkupfalse%
wenzelm@44124: \ a{\isaliteral{3A}{\isacharcolon}}\ A\ \isakeyword{and}\ b{\isaliteral{3A}{\isacharcolon}}\ B%
wenzelm@44124: \endisatagproof
wenzelm@44124: {\isafoldproof}%
wenzelm@44124: %
wenzelm@44124: \isadelimproof
wenzelm@44124: \isanewline
wenzelm@44124: %
wenzelm@44124: \endisadelimproof
wenzelm@44124: \ \ \isacommand{thm}\isamarkupfalse%
wenzelm@44124: \ conjI\isanewline
wenzelm@44124: \ \ \isacommand{thm}\isamarkupfalse%
wenzelm@44124: \ conjI\ {\isaliteral{5B}{\isacharbrackleft}}of\ A\ B{\isaliteral{5D}{\isacharbrackright}}\ \ %
wenzelm@44124: \isamarkupcmt{instantiation%
wenzelm@44124: }
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{thm}\isamarkupfalse%
wenzelm@44124: \ conjI\ {\isaliteral{5B}{\isacharbrackleft}}of\ A\ B{\isaliteral{2C}{\isacharcomma}}\ OF\ a\ b{\isaliteral{5D}{\isacharbrackright}}\ \ %
wenzelm@44124: \isamarkupcmt{instantiation and composition%
wenzelm@44124: }
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{thm}\isamarkupfalse%
wenzelm@44124: \ conjI\ {\isaliteral{5B}{\isacharbrackleft}}OF\ a\ b{\isaliteral{5D}{\isacharbrackright}}\ \ %
wenzelm@44124: \isamarkupcmt{composition via unification (trivial)%
wenzelm@44124: }
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{thm}\isamarkupfalse%
wenzelm@44124: \ conjI\ {\isaliteral{5B}{\isacharbrackleft}}OF\ {\isaliteral{60}{\isacharbackquoteopen}}A{\isaliteral{60}{\isacharbackquoteclose}}\ {\isaliteral{60}{\isacharbackquoteopen}}B{\isaliteral{60}{\isacharbackquoteclose}}{\isaliteral{5D}{\isacharbrackright}}\isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{thm}\isamarkupfalse%
wenzelm@44124: \ conjI\ {\isaliteral{5B}{\isacharbrackleft}}OF\ disjI{\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}\isanewline
wenzelm@44124: \isacommand{end}\isamarkupfalse%
wenzelm@44124: %
wenzelm@44124: \begin{isamarkuptext}%
wenzelm@44124: Note: Low-level rule composition is tedious and leads to
wenzelm@44124:   unreadable~/ unmaintainable expressions in the text.%
wenzelm@44124: \end{isamarkuptext}%
wenzelm@44124: \isamarkuptrue%
wenzelm@44124: %
wenzelm@44124: \isamarkupsubsection{Structured backward reasoning%
wenzelm@44124: }
wenzelm@44124: \isamarkuptrue%
wenzelm@44124: %
wenzelm@44124: \begin{isamarkuptext}%
wenzelm@44124: Idea: Canonical proof decomposition via \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~/
wenzelm@44124:   \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~/ \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}, where the body produces a
wenzelm@44124:   natural deduction rule to refine some goal.%
wenzelm@44124: \end{isamarkuptext}%
wenzelm@44124: \isamarkuptrue%
wenzelm@44124: \isacommand{notepad}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \isakeyword{begin}\isanewline
wenzelm@44124: %
wenzelm@44124: \isadelimproof
wenzelm@44124: \ \ %
wenzelm@44124: \endisadelimproof
wenzelm@44124: %
wenzelm@44124: \isatagproof
wenzelm@44124: \isacommand{fix}\isamarkupfalse%
wenzelm@44124: \ A\ B\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ A\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124: \ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{2D}{\isacharminus}}\isanewline
wenzelm@44124: \ \ \ \ \isacommand{fix}\isamarkupfalse%
wenzelm@44124: \ x\isanewline
wenzelm@44124: \ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}A\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124: \ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ A\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124: \ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{2D}{\isacharminus}}\isanewline
wenzelm@44124: \ \ \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
wenzelm@44124: \ x\isanewline
wenzelm@44124: \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}A\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124: \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
wenzelm@44124: \ %
wenzelm@44124: \isamarkupcmt{implicit block structure made explicit%
wenzelm@44124: }
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \ \ \isacommand{note}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{60}{\isacharbackquoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ A\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ x{\isaliteral{60}{\isacharbackquoteclose}}\isanewline
wenzelm@44124: \ \ \ \ \ \ %
wenzelm@44124: \isamarkupcmt{side exit for the resulting rule%
wenzelm@44124: }
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124: %
wenzelm@44124: \endisatagproof
wenzelm@44124: {\isafoldproof}%
wenzelm@44124: %
wenzelm@44124: \isadelimproof
wenzelm@44124: \isanewline
wenzelm@44124: %
wenzelm@44124: \endisadelimproof
wenzelm@44124: \isacommand{end}\isamarkupfalse%
wenzelm@44124: %
wenzelm@44124: \isamarkupsubsection{Structured rule application%
wenzelm@44124: }
wenzelm@44124: \isamarkuptrue%
wenzelm@44124: %
wenzelm@44124: \begin{isamarkuptext}%
wenzelm@44124: Idea: Previous facts and new claims are composed with a rule from
wenzelm@44124:   the context (or background library).%
wenzelm@44124: \end{isamarkuptext}%
wenzelm@44124: \isamarkuptrue%
wenzelm@44124: \isacommand{notepad}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \isakeyword{begin}\isanewline
wenzelm@44124: %
wenzelm@44124: \isadelimproof
wenzelm@44124: \ \ %
wenzelm@44124: \endisadelimproof
wenzelm@44124: %
wenzelm@44124: \isatagproof
wenzelm@44124: \isacommand{assume}\isamarkupfalse%
wenzelm@44124: \ r{\isadigit{1}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isaliteral{22}{\isachardoublequoteclose}}\ \ %
wenzelm@44124: \isamarkupcmt{simple rule (Horn clause)%
wenzelm@44124: }
wenzelm@44124: \isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ A\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \ \ %
wenzelm@44124: \isamarkupcmt{prefix of facts via outer sub-proof%
wenzelm@44124: }
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124: \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ C\isanewline
wenzelm@44124: \ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{28}{\isacharparenleft}}rule\ r{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44124: \ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124: \ B\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \ \ %
wenzelm@44124: \isamarkupcmt{remaining rule premises via inner sub-proof%
wenzelm@44124: }
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ C\isanewline
wenzelm@44124: \ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{28}{\isacharparenleft}}rule\ r{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44124: \ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124: \ A\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124: \ B\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ A\ \isakeyword{and}\ B\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124: \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ C\isanewline
wenzelm@44124: \ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{28}{\isacharparenleft}}rule\ r{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44124: \ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ A\ \isakeyword{and}\ B\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124: \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ C\ \isacommand{by}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{28}{\isacharparenleft}}rule\ r{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \isacommand{next}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44124: \ 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}}\ \ %
wenzelm@44124: \isamarkupcmt{nested rule%
wenzelm@44124: }
wenzelm@44124: \isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ A\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124: \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ C\isanewline
wenzelm@44124: \ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{28}{\isacharparenleft}}rule\ r{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44124: \ \ \ \ \isacommand{fix}\isamarkupfalse%
wenzelm@44124: \ x\isanewline
wenzelm@44124: \ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}B{\isadigit{1}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124: \ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}B{\isadigit{2}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124: %
wenzelm@44124: \begin{isamarkuptxt}%
wenzelm@44124: 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
wenzelm@44124:     addressed via \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~/ \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~/ \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}
wenzelm@44124:     in the nested proof body.%
wenzelm@44124: \end{isamarkuptxt}%
wenzelm@44124: \isamarkuptrue%
wenzelm@44124: %
wenzelm@44124: \endisatagproof
wenzelm@44124: {\isafoldproof}%
wenzelm@44124: %
wenzelm@44124: \isadelimproof
wenzelm@44124: %
wenzelm@44124: \endisadelimproof
wenzelm@44124: \isacommand{end}\isamarkupfalse%
wenzelm@44124: %
wenzelm@44124: \isamarkupsubsection{Example: predicate logic%
wenzelm@44124: }
wenzelm@44124: \isamarkuptrue%
wenzelm@44124: %
wenzelm@44124: \begin{isamarkuptext}%
wenzelm@44124: Using the above principles, standard introduction and elimination proofs
wenzelm@44124:   of predicate logic connectives of HOL work as follows.%
wenzelm@44124: \end{isamarkuptext}%
wenzelm@44124: \isamarkuptrue%
wenzelm@44124: \isacommand{notepad}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \isakeyword{begin}\isanewline
wenzelm@44124: %
wenzelm@44124: \isadelimproof
wenzelm@44124: \ \ %
wenzelm@44124: \endisadelimproof
wenzelm@44124: %
wenzelm@44124: \isatagproof
wenzelm@44124: \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ A\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124: \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ B\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ A\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124: \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ B\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124: \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124: \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ C\isanewline
wenzelm@44124: \ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44124: \ A\isanewline
wenzelm@44124: \ \ \ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124: \ \isacommand{show}\isamarkupfalse%
wenzelm@44124: \ C\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{next}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44124: \ B\isanewline
wenzelm@44124: \ \ \ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124: \ \isacommand{show}\isamarkupfalse%
wenzelm@44124: \ C\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ A\ \isakeyword{and}\ B\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124: \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124: \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ A\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124: \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ B\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ False\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124: \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ A\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ True\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124: \ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44124: \ A\isanewline
wenzelm@44124: \ \ \ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124: \ \isacommand{show}\isamarkupfalse%
wenzelm@44124: \ False\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ A\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124: \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ B\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124: \ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \ \ \isacommand{fix}\isamarkupfalse%
wenzelm@44124: \ x\isanewline
wenzelm@44124: \ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}P\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124: \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}P\ a{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124: \ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}P\ a{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124: \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ C\isanewline
wenzelm@44124: \ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \ \ \isacommand{fix}\isamarkupfalse%
wenzelm@44124: \ a\isanewline
wenzelm@44124: \ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}P\ a{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124: \ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124: \ C\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124: %
wenzelm@44124: \begin{isamarkuptxt}%
wenzelm@44124: Less awkward version using \hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}}:%
wenzelm@44124: \end{isamarkuptxt}%
wenzelm@44124: \isamarkuptrue%
wenzelm@44124: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124: \ \isacommand{obtain}\isamarkupfalse%
wenzelm@44124: \ a\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}P\ a{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44124: %
wenzelm@44124: \endisatagproof
wenzelm@44124: {\isafoldproof}%
wenzelm@44124: %
wenzelm@44124: \isadelimproof
wenzelm@44124: \isanewline
wenzelm@44124: %
wenzelm@44124: \endisadelimproof
wenzelm@44124: \isacommand{end}\isamarkupfalse%
wenzelm@44124: %
wenzelm@44124: \begin{isamarkuptext}%
wenzelm@44124: Further variations to illustrate Isar sub-proofs involving
wenzelm@44124:   \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}:%
wenzelm@44124: \end{isamarkuptext}%
wenzelm@44124: \isamarkuptrue%
wenzelm@44124: \isacommand{notepad}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \isakeyword{begin}\isanewline
wenzelm@44124: %
wenzelm@44124: \isadelimproof
wenzelm@44124: \ \ %
wenzelm@44124: \endisadelimproof
wenzelm@44124: %
wenzelm@44124: \isatagproof
wenzelm@44124: \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124: \ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124: \ \ %
wenzelm@44124: \isamarkupcmt{two strictly isolated subproofs%
wenzelm@44124: }
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124: \ A\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{next}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124: \ B\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124: \ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124: \ \ %
wenzelm@44124: \isamarkupcmt{one simultaneous sub-proof%
wenzelm@44124: }
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124: \ A\ \isakeyword{and}\ B\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124: \ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124: \ \ %
wenzelm@44124: \isamarkupcmt{two subproofs in the same context%
wenzelm@44124: }
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124: \ A\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124: \ B\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124: \ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124: \ \ %
wenzelm@44124: \isamarkupcmt{swapped order%
wenzelm@44124: }
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124: \ B\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124: \ A\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124: \ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124: \ \ %
wenzelm@44124: \isamarkupcmt{sequential subproofs%
wenzelm@44124: }
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124: \ A\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124: \ B\ \isacommand{using}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{60}{\isacharbackquoteopen}}A{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124: %
wenzelm@44124: \endisatagproof
wenzelm@44124: {\isafoldproof}%
wenzelm@44124: %
wenzelm@44124: \isadelimproof
wenzelm@44124: \isanewline
wenzelm@44124: %
wenzelm@44124: \endisadelimproof
wenzelm@44124: \isacommand{end}\isamarkupfalse%
wenzelm@44124: %
wenzelm@44124: \isamarkupsubsubsection{Example: set-theoretic operators%
wenzelm@44124: }
wenzelm@44124: \isamarkuptrue%
wenzelm@44124: %
wenzelm@44124: \begin{isamarkuptext}%
wenzelm@44124: 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
wenzelm@45988:   set-theory or lattice-theory work analogously.  It is only a matter
wenzelm@44124:   of rule declarations in the library; rules can be also specified
wenzelm@44124:   explicitly.%
wenzelm@44124: \end{isamarkuptext}%
wenzelm@44124: \isamarkuptrue%
wenzelm@44124: \isacommand{notepad}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \isakeyword{begin}\isanewline
wenzelm@44124: %
wenzelm@44124: \isadelimproof
wenzelm@44124: \ \ %
wenzelm@44124: \endisadelimproof
wenzelm@44124: %
wenzelm@44124: \isatagproof
wenzelm@44124: \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ {\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%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124: \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124: \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124: \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124: \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ C\isanewline
wenzelm@44124: \ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124: \ \ \ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124: \ \isacommand{show}\isamarkupfalse%
wenzelm@44124: \ C\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{next}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124: \ \ \ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124: \ \isacommand{show}\isamarkupfalse%
wenzelm@44124: \ C\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \isacommand{next}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{5C3C496E7465723E}{\isasymInter}}A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124: \ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \ \ \isacommand{fix}\isamarkupfalse%
wenzelm@44124: \ a\isanewline
wenzelm@44124: \ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124: \ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ a{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{5C3C496E7465723E}{\isasymInter}}A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124: \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ a{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124: \ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ {\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%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124: \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{5C3C556E696F6E3E}{\isasymUnion}}A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124: \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{5C3C556E696F6E3E}{\isasymUnion}}A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124: \isanewline
wenzelm@44124: \ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124: \ \isacommand{obtain}\isamarkupfalse%
wenzelm@44124: \ 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%
wenzelm@44124: %
wenzelm@44124: \endisatagproof
wenzelm@44124: {\isafoldproof}%
wenzelm@44124: %
wenzelm@44124: \isadelimproof
wenzelm@44124: \isanewline
wenzelm@44124: %
wenzelm@44124: \endisadelimproof
wenzelm@44124: \isacommand{end}\isamarkupfalse%
wenzelm@44126: %
wenzelm@44126: \isamarkupsection{Generalized elimination and cases%
wenzelm@44126: }
wenzelm@44126: \isamarkuptrue%
wenzelm@44126: %
wenzelm@44126: \isamarkupsubsection{General elimination rules%
wenzelm@44126: }
wenzelm@44126: \isamarkuptrue%
wenzelm@44126: %
wenzelm@44126: \begin{isamarkuptext}%
wenzelm@44126: The general format of elimination rules is illustrated by the
wenzelm@44126:   following typical representatives:%
wenzelm@44126: \end{isamarkuptext}%
wenzelm@44126: \isamarkuptrue%
wenzelm@44126: \isacommand{thm}\isamarkupfalse%
wenzelm@44126: \ exE\ \ \ \ \ %
wenzelm@44126: \isamarkupcmt{local parameter%
wenzelm@44126: }
wenzelm@44126: \isanewline
wenzelm@44126: \isacommand{thm}\isamarkupfalse%
wenzelm@44126: \ conjE\ \ \ %
wenzelm@44126: \isamarkupcmt{local premises%
wenzelm@44126: }
wenzelm@44126: \isanewline
wenzelm@44126: \isacommand{thm}\isamarkupfalse%
wenzelm@44126: \ disjE\ \ \ %
wenzelm@44126: \isamarkupcmt{split into cases%
wenzelm@44126: }
wenzelm@44126: %
wenzelm@44126: \begin{isamarkuptext}%
wenzelm@44126: Combining these characteristics leads to the following general scheme
wenzelm@44126:   for elimination rules with cases:
wenzelm@44126: 
wenzelm@44126:   \begin{itemize}
wenzelm@44126: 
wenzelm@44126:   \item prefix of assumptions (or ``major premises'')
wenzelm@44126: 
wenzelm@44126:   \item one or more cases that enable to establish the main conclusion
wenzelm@44126:     in an augmented context
wenzelm@44126: 
wenzelm@44126:   \end{itemize}%
wenzelm@44126: \end{isamarkuptext}%
wenzelm@44126: \isamarkuptrue%
wenzelm@44126: \isacommand{notepad}\isamarkupfalse%
wenzelm@44126: \isanewline
wenzelm@44126: \isakeyword{begin}\isanewline
wenzelm@44126: %
wenzelm@44126: \isadelimproof
wenzelm@44126: \ \ %
wenzelm@44126: \endisadelimproof
wenzelm@44126: %
wenzelm@44126: \isatagproof
wenzelm@44126: \isacommand{assume}\isamarkupfalse%
wenzelm@44126: \ r{\isaliteral{3A}{\isacharcolon}}\isanewline
wenzelm@44126: \ \ \ \ {\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
wenzelm@44126: \ \ \ \ \ \ {\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
wenzelm@44126: \ \ \ \ \ \ {\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
wenzelm@44126: \ \ \ \ \ \ R\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\ main\ conclusion\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44126: \isanewline
wenzelm@44126: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44126: \ A{\isadigit{1}}\ \isakeyword{and}\ A{\isadigit{2}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44126: \isanewline
wenzelm@44126: \ \ \isacommand{then}\isamarkupfalse%
wenzelm@44126: \ \isacommand{have}\isamarkupfalse%
wenzelm@44126: \ R\isanewline
wenzelm@44126: \ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44126: \ {\isaliteral{28}{\isacharparenleft}}rule\ r{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44126: \ \ \ \ \isacommand{fix}\isamarkupfalse%
wenzelm@44126: \ x\ y\isanewline
wenzelm@44126: \ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44126: \ {\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
wenzelm@44126: \ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44126: \ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44126: \isanewline
wenzelm@44126: \ \ \isacommand{next}\isamarkupfalse%
wenzelm@44126: \isanewline
wenzelm@44126: \ \ \ \ \isacommand{fix}\isamarkupfalse%
wenzelm@44126: \ x\ y\isanewline
wenzelm@44126: \ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44126: \ {\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
wenzelm@44126: \ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44126: \ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44126: \isanewline
wenzelm@44126: \ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44126: %
wenzelm@44126: \endisatagproof
wenzelm@44126: {\isafoldproof}%
wenzelm@44126: %
wenzelm@44126: \isadelimproof
wenzelm@44126: \isanewline
wenzelm@44126: %
wenzelm@44126: \endisadelimproof
wenzelm@44126: \isacommand{end}\isamarkupfalse%
wenzelm@44126: %
wenzelm@44126: \begin{isamarkuptext}%
wenzelm@44126: Here \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}thesis{\isaliteral{22}{\isachardoublequote}}} is used to refer to the unchanged goal
wenzelm@44126:   statement.%
wenzelm@44126: \end{isamarkuptext}%
wenzelm@44126: \isamarkuptrue%
wenzelm@44126: %
wenzelm@44126: \isamarkupsubsection{Rules with cases%
wenzelm@44126: }
wenzelm@44126: \isamarkuptrue%
wenzelm@44126: %
wenzelm@44126: \begin{isamarkuptext}%
wenzelm@44126: Applying an elimination rule to some goal, leaves that unchanged
wenzelm@44126:   but allows to augment the context in the sub-proof of each case.
wenzelm@44126: 
wenzelm@44126:   Isar provides some infrastructure to support this:
wenzelm@44126: 
wenzelm@44126:   \begin{itemize}
wenzelm@44126: 
wenzelm@44126:   \item native language elements to state eliminations
wenzelm@44126: 
wenzelm@44126:   \item symbolic case names
wenzelm@44126: 
wenzelm@44126:   \item method \hyperlink{method.cases}{\mbox{\isa{cases}}} to recover this structure in a
wenzelm@44126:   sub-proof
wenzelm@44126: 
wenzelm@44126:   \end{itemize}%
wenzelm@44126: \end{isamarkuptext}%
wenzelm@44126: \isamarkuptrue%
wenzelm@44126: \isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}\isamarkupfalse%
wenzelm@44126: \ exE\isanewline
wenzelm@44126: \isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}\isamarkupfalse%
wenzelm@44126: \ conjE\isanewline
wenzelm@44126: \isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}\isamarkupfalse%
wenzelm@44126: \ disjE\isanewline
wenzelm@44126: \isanewline
wenzelm@44126: \isacommand{lemma}\isamarkupfalse%
wenzelm@44126: \isanewline
wenzelm@44126: \ \ \isakeyword{assumes}\ A{\isadigit{1}}\ \isakeyword{and}\ A{\isadigit{2}}\ \ %
wenzelm@44126: \isamarkupcmt{assumptions%
wenzelm@44126: }
wenzelm@44126: \isanewline
wenzelm@44126: \ \ \isakeyword{obtains}\isanewline
wenzelm@44126: \ \ \ \ {\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
wenzelm@44126: \ \ {\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
wenzelm@44126: %
wenzelm@44126: \isadelimproof
wenzelm@44126: \ \ %
wenzelm@44126: \endisadelimproof
wenzelm@44126: %
wenzelm@44126: \isatagproof
wenzelm@44126: \isacommand{sorry}\isamarkupfalse%
wenzelm@44126: %
wenzelm@44126: \endisatagproof
wenzelm@44126: {\isafoldproof}%
wenzelm@44126: %
wenzelm@44126: \isadelimproof
wenzelm@44126: %
wenzelm@44126: \endisadelimproof
wenzelm@44126: %
wenzelm@44126: \isamarkupsubsubsection{Example%
wenzelm@44126: }
wenzelm@44126: \isamarkuptrue%
wenzelm@44126: \isacommand{lemma}\isamarkupfalse%
wenzelm@44126: \ tertium{\isaliteral{5F}{\isacharunderscore}}non{\isaliteral{5F}{\isacharunderscore}}datur{\isaliteral{3A}{\isacharcolon}}\isanewline
wenzelm@44126: \ \ \isakeyword{obtains}\isanewline
wenzelm@44126: \ \ \ \ {\isaliteral{28}{\isacharparenleft}}T{\isaliteral{29}{\isacharparenright}}\ \ A\isanewline
wenzelm@44126: \ \ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{28}{\isacharparenleft}}F{\isaliteral{29}{\isacharparenright}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44126: %
wenzelm@44126: \isadelimproof
wenzelm@44126: \ \ %
wenzelm@44126: \endisadelimproof
wenzelm@44126: %
wenzelm@44126: \isatagproof
wenzelm@44126: \isacommand{by}\isamarkupfalse%
wenzelm@44126: \ blast%
wenzelm@44126: \endisatagproof
wenzelm@44126: {\isafoldproof}%
wenzelm@44126: %
wenzelm@44126: \isadelimproof
wenzelm@44126: \isanewline
wenzelm@44126: %
wenzelm@44126: \endisadelimproof
wenzelm@44126: \isanewline
wenzelm@44126: \isacommand{notepad}\isamarkupfalse%
wenzelm@44126: \isanewline
wenzelm@44126: \isakeyword{begin}\isanewline
wenzelm@44126: %
wenzelm@44126: \isadelimproof
wenzelm@44126: \ \ %
wenzelm@44126: \endisadelimproof
wenzelm@44126: %
wenzelm@44126: \isatagproof
wenzelm@44126: \isacommand{fix}\isamarkupfalse%
wenzelm@44126: \ x\ y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\isanewline
wenzelm@44126: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44126: \ C\isanewline
wenzelm@44126: \ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44126: \ {\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
wenzelm@44126: \ \ \ \ \isacommand{case}\isamarkupfalse%
wenzelm@44126: \ T\isanewline
wenzelm@44126: \ \ \ \ \isacommand{from}\isamarkupfalse%
wenzelm@44126: \ {\isaliteral{60}{\isacharbackquoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse%
wenzelm@44126: \ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44126: \isanewline
wenzelm@44126: \ \ \isacommand{next}\isamarkupfalse%
wenzelm@44126: \isanewline
wenzelm@44126: \ \ \ \ \isacommand{case}\isamarkupfalse%
wenzelm@44126: \ F\isanewline
wenzelm@44126: \ \ \ \ \isacommand{from}\isamarkupfalse%
wenzelm@44126: \ {\isaliteral{60}{\isacharbackquoteopen}}x\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ y{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse%
wenzelm@44126: \ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44126: \isanewline
wenzelm@44126: \ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44126: %
wenzelm@44126: \endisatagproof
wenzelm@44126: {\isafoldproof}%
wenzelm@44126: %
wenzelm@44126: \isadelimproof
wenzelm@44126: \isanewline
wenzelm@44126: %
wenzelm@44126: \endisadelimproof
wenzelm@44126: \isacommand{end}\isamarkupfalse%
wenzelm@44126: %
wenzelm@44126: \isamarkupsubsubsection{Example%
wenzelm@44126: }
wenzelm@44126: \isamarkuptrue%
wenzelm@44126: %
wenzelm@44126: \begin{isamarkuptext}%
wenzelm@44126: Isabelle/HOL specification mechanisms (datatype, inductive, etc.)
wenzelm@44126:   provide suitable derived cases rules.%
wenzelm@44126: \end{isamarkuptext}%
wenzelm@44126: \isamarkuptrue%
wenzelm@44126: \isacommand{datatype}\isamarkupfalse%
wenzelm@44126: \ foo\ {\isaliteral{3D}{\isacharequal}}\ Foo\ {\isaliteral{7C}{\isacharbar}}\ Bar\ foo\isanewline
wenzelm@44126: \isanewline
wenzelm@44126: \isacommand{notepad}\isamarkupfalse%
wenzelm@44126: \isanewline
wenzelm@44126: \isakeyword{begin}\isanewline
wenzelm@44126: %
wenzelm@44126: \isadelimproof
wenzelm@44126: \ \ %
wenzelm@44126: \endisadelimproof
wenzelm@44126: %
wenzelm@44126: \isatagproof
wenzelm@44126: \isacommand{fix}\isamarkupfalse%
wenzelm@44126: \ x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ foo\isanewline
wenzelm@44126: \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44126: \ C\isanewline
wenzelm@44126: \ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44126: \ {\isaliteral{28}{\isacharparenleft}}cases\ x{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44126: \ \ \ \ \isacommand{case}\isamarkupfalse%
wenzelm@44126: \ Foo\isanewline
wenzelm@44126: \ \ \ \ \isacommand{from}\isamarkupfalse%
wenzelm@44126: \ {\isaliteral{60}{\isacharbackquoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ Foo{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse%
wenzelm@44126: \ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44126: \isanewline
wenzelm@44126: \ \ \isacommand{next}\isamarkupfalse%
wenzelm@44126: \isanewline
wenzelm@44126: \ \ \ \ \isacommand{case}\isamarkupfalse%
wenzelm@44126: \ {\isaliteral{28}{\isacharparenleft}}Bar\ a{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44126: \ \ \ \ \isacommand{from}\isamarkupfalse%
wenzelm@44126: \ {\isaliteral{60}{\isacharbackquoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ Bar\ a{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse%
wenzelm@44126: \ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44126: \isanewline
wenzelm@44126: \ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44126: %
wenzelm@44126: \endisatagproof
wenzelm@44126: {\isafoldproof}%
wenzelm@44126: %
wenzelm@44126: \isadelimproof
wenzelm@44126: \isanewline
wenzelm@44126: %
wenzelm@44126: \endisadelimproof
wenzelm@44126: \isacommand{end}\isamarkupfalse%
wenzelm@44126: %
wenzelm@44126: \isamarkupsubsection{Obtaining local contexts%
wenzelm@44126: }
wenzelm@44126: \isamarkuptrue%
wenzelm@44126: %
wenzelm@44126: \begin{isamarkuptext}%
wenzelm@44126: A single ``case'' branch may be inlined into Isar proof text
wenzelm@44126:   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.%
wenzelm@44126: \end{isamarkuptext}%
wenzelm@44126: \isamarkuptrue%
wenzelm@44126: \isacommand{notepad}\isamarkupfalse%
wenzelm@44126: \isanewline
wenzelm@44126: \isakeyword{begin}\isanewline
wenzelm@44126: %
wenzelm@44126: \isadelimproof
wenzelm@44126: \ \ %
wenzelm@44126: \endisadelimproof
wenzelm@44126: %
wenzelm@44126: \isatagproof
wenzelm@44126: \isacommand{fix}\isamarkupfalse%
wenzelm@44126: \ B\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44126: \isanewline
wenzelm@44126: \ \ \isacommand{obtain}\isamarkupfalse%
wenzelm@44126: \ x\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44126: \isanewline
wenzelm@44126: \ \ \isacommand{note}\isamarkupfalse%
wenzelm@44126: \ {\isaliteral{60}{\isacharbackquoteopen}}B\ x{\isaliteral{60}{\isacharbackquoteclose}}%
wenzelm@44126: \begin{isamarkuptxt}%
wenzelm@44126: Conclusions from this context may not mention \isa{x} again!%
wenzelm@44126: \end{isamarkuptxt}%
wenzelm@44126: \isamarkuptrue%
wenzelm@44126: \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
wenzelm@44126: \isanewline
wenzelm@44126: \ \ \ \ \isacommand{obtain}\isamarkupfalse%
wenzelm@44126: \ x\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44126: \isanewline
wenzelm@44126: \ \ \ \ \isacommand{from}\isamarkupfalse%
wenzelm@44126: \ {\isaliteral{60}{\isacharbackquoteopen}}B\ x{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{have}\isamarkupfalse%
wenzelm@44126: \ C\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44126: \isanewline
wenzelm@44126: \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
wenzelm@44126: \isanewline
wenzelm@44126: \ \ \isacommand{note}\isamarkupfalse%
wenzelm@44126: \ {\isaliteral{60}{\isacharbackquoteopen}}C{\isaliteral{60}{\isacharbackquoteclose}}%
wenzelm@44126: \endisatagproof
wenzelm@44126: {\isafoldproof}%
wenzelm@44126: %
wenzelm@44126: \isadelimproof
wenzelm@44126: \isanewline
wenzelm@44126: %
wenzelm@44126: \endisadelimproof
wenzelm@44126: \isacommand{end}\isamarkupfalse%
wenzelm@44121: \isanewline
wenzelm@44121: %
wenzelm@44121: \isadelimtheory
wenzelm@44121: \isanewline
wenzelm@44121: %
wenzelm@44121: \endisadelimtheory
wenzelm@44121: %
wenzelm@44121: \isatagtheory
wenzelm@44121: \isacommand{end}\isamarkupfalse%
wenzelm@44121: %
wenzelm@44121: \endisatagtheory
wenzelm@44121: {\isafoldtheory}%
wenzelm@44121: %
wenzelm@44121: \isadelimtheory
wenzelm@45988: \isanewline
wenzelm@44121: %
wenzelm@44121: \endisadelimtheory
wenzelm@44121: \end{isabellebody}%
wenzelm@44121: %%% Local Variables:
wenzelm@44121: %%% mode: latex
wenzelm@44121: %%% TeX-master: "root"
wenzelm@44121: %%% End:




