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: