%

\begin{isabellebody}%

\def\isabellecontext{First{\isaliteral{5F}{\isacharunderscore}}Order{\isaliteral{5F}{\isacharunderscore}}Logic}%

%

\isamarkupheader{Example: First-Order Logic%

}

\isamarkuptrue%

%

\isadelimvisible

%

\endisadelimvisible

%

\isatagvisible

\isacommand{theory}\isamarkupfalse%

\ First{\isaliteral{5F}{\isacharunderscore}}Order{\isaliteral{5F}{\isacharunderscore}}Logic\isanewline

\isakeyword{imports}\ Base\ \ \isanewline

\isakeyword{begin}%

\endisatagvisible

{\isafoldvisible}%

%

\isadelimvisible

%

\endisadelimvisible

%

\begin{isamarkuptext}%

\noindent In order to commence a new object-logic within

  Isabelle/Pure we introduce abstract syntactic categories \isa{{\isaliteral{22}{\isachardoublequote}}i{\isaliteral{22}{\isachardoublequote}}}

  for individuals and \isa{{\isaliteral{22}{\isachardoublequote}}o{\isaliteral{22}{\isachardoublequote}}} for object-propositions.  The latter

  is embedded into the language of Pure propositions by means of a

  separate judgment.%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{typedecl}\isamarkupfalse%

\ i\isanewline

\isacommand{typedecl}\isamarkupfalse%

\ o\isanewline

\isanewline

\isacommand{judgment}\isamarkupfalse%

\isanewline

\ \ Trueprop\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}o\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ prop{\isaliteral{22}{\isachardoublequoteclose}}\ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{5}}{\isaliteral{29}{\isacharparenright}}%

\begin{isamarkuptext}%

\noindent Note that the object-logic judgement is implicit in the

  syntax: writing \isa{A} produces \isa{{\isaliteral{22}{\isachardoublequote}}Trueprop\ A{\isaliteral{22}{\isachardoublequote}}} internally.

  From the Pure perspective this means ``\isa{A} is derivable in the

  object-logic''.%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isamarkupsubsection{Equational reasoning \label{sec:framework-ex-equal}%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

Equality is axiomatized as a binary predicate on individuals, with

  reflexivity as introduction, and substitution as elimination

  principle.  Note that the latter is particularly convenient in a

  framework like Isabelle, because syntactic congruences are

  implicitly produced by unification of \isa{{\isaliteral{22}{\isachardoublequote}}B\ x{\isaliteral{22}{\isachardoublequote}}} against

  expressions containing occurrences of \isa{x}.%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{axiomatization}\isamarkupfalse%

\isanewline

\ \ equal\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ o{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infix}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{5}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline

\isakeyword{where}\isanewline

\ \ refl\ {\isaliteral{5B}{\isacharbrackleft}}intro{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline

\ \ subst\ {\isaliteral{5B}{\isacharbrackleft}}elim{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ y\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ y{\isaliteral{22}{\isachardoublequoteclose}}%

\begin{isamarkuptext}%

\noindent Substitution is very powerful, but also hard to control in

  full generality.  We derive some common symmetry~/ transitivity

  schemes of \isa{equal} as particular consequences.%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{theorem}\isamarkupfalse%

\ sym\ {\isaliteral{5B}{\isacharbrackleft}}sym{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline

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

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

%

\isadelimproof

%

\endisadelimproof

%

\isatagproof

\isacommand{proof}\isamarkupfalse%

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

\ \ \isacommand{have}\isamarkupfalse%

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

\isanewline

\ \ \isacommand{with}\isamarkupfalse%

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

\ {\isaliteral{22}{\isachardoublequoteopen}}y\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

\isanewline

\isacommand{qed}\isamarkupfalse%

%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

\isanewline

%

\endisadelimproof

\isanewline

\isacommand{theorem}\isamarkupfalse%

\ forw{\isaliteral{5F}{\isacharunderscore}}subst\ {\isaliteral{5B}{\isacharbrackleft}}trans{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline

\ \ \isakeyword{assumes}\ {\isaliteral{22}{\isachardoublequoteopen}}y\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ {\isaliteral{22}{\isachardoublequoteopen}}B\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

\ \ \isakeyword{shows}\ {\isaliteral{22}{\isachardoublequoteopen}}B\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

%

\isadelimproof

%

\endisadelimproof

%

\isatagproof

\isacommand{proof}\isamarkupfalse%

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

\ \ \isacommand{from}\isamarkupfalse%

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

\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

\isanewline

\ \ \isacommand{from}\isamarkupfalse%

\ this\ \isakeyword{and}\ {\isaliteral{60}{\isacharbackquoteopen}}B\ x{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse%

\ {\isaliteral{22}{\isachardoublequoteopen}}B\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

\isanewline

\isacommand{qed}\isamarkupfalse%

%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

\isanewline

%

\endisadelimproof

\isanewline

\isacommand{theorem}\isamarkupfalse%

\ back{\isaliteral{5F}{\isacharunderscore}}subst\ {\isaliteral{5B}{\isacharbrackleft}}trans{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline

\ \ \isakeyword{assumes}\ {\isaliteral{22}{\isachardoublequoteopen}}B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

\ \ \isakeyword{shows}\ {\isaliteral{22}{\isachardoublequoteopen}}B\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

%

\isadelimproof

%

\endisadelimproof

%

\isatagproof

\isacommand{proof}\isamarkupfalse%

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

\ \ \isacommand{from}\isamarkupfalse%

\ {\isaliteral{60}{\isacharbackquoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{60}{\isacharbackquoteclose}}\ \isakeyword{and}\ {\isaliteral{60}{\isacharbackquoteopen}}B\ x{\isaliteral{60}{\isacharbackquoteclose}}\isanewline

\ \ \isacommand{show}\isamarkupfalse%

\ {\isaliteral{22}{\isachardoublequoteopen}}B\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

\isanewline

\isacommand{qed}\isamarkupfalse%

%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

\isanewline

%

\endisadelimproof

\isanewline

\isacommand{theorem}\isamarkupfalse%

\ trans\ {\isaliteral{5B}{\isacharbrackleft}}trans{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline

\ \ \isakeyword{assumes}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ {\isaliteral{22}{\isachardoublequoteopen}}y\ {\isaliteral{3D}{\isacharequal}}\ z{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

\ \ \isakeyword{shows}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ z{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

%

\isadelimproof

%

\endisadelimproof

%

\isatagproof

\isacommand{proof}\isamarkupfalse%

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

\ \ \isacommand{from}\isamarkupfalse%

\ {\isaliteral{60}{\isacharbackquoteopen}}y\ {\isaliteral{3D}{\isacharequal}}\ z{\isaliteral{60}{\isacharbackquoteclose}}\ \isakeyword{and}\ {\isaliteral{60}{\isacharbackquoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{60}{\isacharbackquoteclose}}\isanewline

\ \ \isacommand{show}\isamarkupfalse%

\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ z{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

\isanewline

\isacommand{qed}\isamarkupfalse%

%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

%

\endisadelimproof

%

\isamarkupsubsection{Basic group theory%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

As an example for equational reasoning we consider some bits of

  group theory.  The subsequent locale definition postulates group

  operations and axioms; we also derive some consequences of this

  specification.%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{locale}\isamarkupfalse%

\ group\ {\isaliteral{3D}{\isacharequal}}\isanewline

\ \ \isakeyword{fixes}\ prod\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ i{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infix}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C636972633E}{\isasymcirc}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{7}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline

\ \ \ \ \isakeyword{and}\ inv\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ i{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isaliteral{5D}{\isacharbrackright}}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isaliteral{29}{\isacharparenright}}\isanewline

\ \ \ \ \isakeyword{and}\ unit\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ i\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isadigit{1}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\isanewline

\ \ \isakeyword{assumes}\ assoc{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ z\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ {\isaliteral{28}{\isacharparenleft}}y\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ z{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

\ \ \ \ \isakeyword{and}\ left{\isaliteral{5F}{\isacharunderscore}}unit{\isaliteral{3A}{\isacharcolon}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isadigit{1}}\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ x\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

\ \ \ \ \isakeyword{and}\ left{\isaliteral{5F}{\isacharunderscore}}inv{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}x{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ x\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

\isakeyword{begin}\isanewline

\isanewline

\isacommand{theorem}\isamarkupfalse%

\ right{\isaliteral{5F}{\isacharunderscore}}inv{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ x{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

%

\isadelimproof

%

\endisadelimproof

%

\isatagproof

\isacommand{proof}\isamarkupfalse%

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

\ \ \isacommand{have}\isamarkupfalse%

\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ x{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ x{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%

\ {\isaliteral{28}{\isacharparenleft}}rule\ left{\isaliteral{5F}{\isacharunderscore}}unit\ {\isaliteral{5B}{\isacharbrackleft}}symmetric{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\isanewline

\ \ \isacommand{also}\isamarkupfalse%

\ \isacommand{have}\isamarkupfalse%

\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ x{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%

\ {\isaliteral{28}{\isacharparenleft}}rule\ assoc\ {\isaliteral{5B}{\isacharbrackleft}}symmetric{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\isanewline

\ \ \isacommand{also}\isamarkupfalse%

\ \isacommand{have}\isamarkupfalse%

\ {\isaliteral{22}{\isachardoublequoteopen}}{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ x{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%

\ {\isaliteral{28}{\isacharparenleft}}rule\ left{\isaliteral{5F}{\isacharunderscore}}inv\ {\isaliteral{5B}{\isacharbrackleft}}symmetric{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\isanewline

\ \ \isacommand{also}\isamarkupfalse%

\ \isacommand{have}\isamarkupfalse%

\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ x\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%

\ {\isaliteral{28}{\isacharparenleft}}rule\ assoc{\isaliteral{29}{\isacharparenright}}\isanewline

\ \ \isacommand{also}\isamarkupfalse%

\ \isacommand{have}\isamarkupfalse%

\ {\isaliteral{22}{\isachardoublequoteopen}}x{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ x\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%

\ {\isaliteral{28}{\isacharparenleft}}rule\ left{\isaliteral{5F}{\isacharunderscore}}inv{\isaliteral{29}{\isacharparenright}}\isanewline

\ \ \isacommand{also}\isamarkupfalse%

\ \isacommand{have}\isamarkupfalse%

\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ x{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ x{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%

\ {\isaliteral{28}{\isacharparenleft}}rule\ assoc{\isaliteral{29}{\isacharparenright}}\isanewline

\ \ \isacommand{also}\isamarkupfalse%

\ \isacommand{have}\isamarkupfalse%

\ {\isaliteral{22}{\isachardoublequoteopen}}{\isadigit{1}}\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ x{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%

\ {\isaliteral{28}{\isacharparenleft}}rule\ left{\isaliteral{5F}{\isacharunderscore}}unit{\isaliteral{29}{\isacharparenright}}\isanewline

\ \ \isacommand{also}\isamarkupfalse%

\ \isacommand{have}\isamarkupfalse%

\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%

\ {\isaliteral{28}{\isacharparenleft}}rule\ left{\isaliteral{5F}{\isacharunderscore}}inv{\isaliteral{29}{\isacharparenright}}\isanewline

\ \ \isacommand{finally}\isamarkupfalse%

\ \isacommand{show}\isamarkupfalse%

\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ x{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

\isanewline

\isacommand{qed}\isamarkupfalse%

%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

\isanewline

%

\endisadelimproof

\isanewline

\isacommand{theorem}\isamarkupfalse%

\ right{\isaliteral{5F}{\isacharunderscore}}unit{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ {\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

%

\isadelimproof

%

\endisadelimproof

%

\isatagproof

\isacommand{proof}\isamarkupfalse%

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

\ \ \isacommand{have}\isamarkupfalse%

\ {\isaliteral{22}{\isachardoublequoteopen}}{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%

\ {\isaliteral{28}{\isacharparenleft}}rule\ left{\isaliteral{5F}{\isacharunderscore}}inv\ {\isaliteral{5B}{\isacharbrackleft}}symmetric{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\isanewline

\ \ \isacommand{also}\isamarkupfalse%

\ \isacommand{have}\isamarkupfalse%

\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ x{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%

\ {\isaliteral{28}{\isacharparenleft}}rule\ assoc\ {\isaliteral{5B}{\isacharbrackleft}}symmetric{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\isanewline

\ \ \isacommand{also}\isamarkupfalse%

\ \isacommand{have}\isamarkupfalse%

\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ x{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%

\ {\isaliteral{28}{\isacharparenleft}}rule\ right{\isaliteral{5F}{\isacharunderscore}}inv{\isaliteral{29}{\isacharparenright}}\isanewline

\ \ \isacommand{also}\isamarkupfalse%

\ \isacommand{have}\isamarkupfalse%

\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ x\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%

\ {\isaliteral{28}{\isacharparenleft}}rule\ left{\isaliteral{5F}{\isacharunderscore}}unit{\isaliteral{29}{\isacharparenright}}\isanewline

\ \ \isacommand{finally}\isamarkupfalse%

\ \isacommand{show}\isamarkupfalse%

\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ {\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

\isanewline

\isacommand{qed}\isamarkupfalse%

%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

%

\endisadelimproof

%

\begin{isamarkuptext}%

\noindent Reasoning from basic axioms is often tedious.  Our proofs

  work by producing various instances of the given rules (potentially

  the symmetric form) using the pattern ``\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}~\isa{eq}~\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}rule\ r{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'' and composing the chain of

  results via \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}}/\hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}}.  These steps may

  involve any of the transitivity rules declared in

  \secref{sec:framework-ex-equal}, namely \isa{trans} in combining

  the first two results in \isa{right{\isaliteral{5F}{\isacharunderscore}}inv} and in the final steps of

  both proofs, \isa{forw{\isaliteral{5F}{\isacharunderscore}}subst} in the first combination of \isa{right{\isaliteral{5F}{\isacharunderscore}}unit}, and \isa{back{\isaliteral{5F}{\isacharunderscore}}subst} in all other calculational steps.

  Occasional substitutions in calculations are adequate, but should

  not be over-emphasized.  The other extreme is to compose a chain by

  plain transitivity only, with replacements occurring always in

  topmost position. For example:%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimproof

%

\endisadelimproof

%

\isatagproof

\ \ \isacommand{have}\isamarkupfalse%

\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ {\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{unfolding}\isamarkupfalse%

\ left{\isaliteral{5F}{\isacharunderscore}}inv\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

\isanewline

\ \ \isacommand{also}\isamarkupfalse%

\ \isacommand{have}\isamarkupfalse%

\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ x{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{unfolding}\isamarkupfalse%

\ assoc\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

\isanewline

\ \ \isacommand{also}\isamarkupfalse%

\ \isacommand{have}\isamarkupfalse%

\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{unfolding}\isamarkupfalse%

\ right{\isaliteral{5F}{\isacharunderscore}}inv\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

\isanewline

\ \ \isacommand{also}\isamarkupfalse%

\ \isacommand{have}\isamarkupfalse%

\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{unfolding}\isamarkupfalse%

\ left{\isaliteral{5F}{\isacharunderscore}}unit\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

\isanewline

\ \ \isacommand{finally}\isamarkupfalse%

\ \isacommand{have}\isamarkupfalse%

\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ {\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

%

\endisadelimproof

%

\begin{isamarkuptext}%

\noindent Here we have re-used the built-in mechanism for unfolding

  definitions in order to normalize each equational problem.  A more

  realistic object-logic would include proper setup for the Simplifier

  (\secref{sec:simplifier}), the main automated tool for equational

  reasoning in Isabelle.  Then ``\hyperlink{command.unfolding}{\mbox{\isa{\isacommand{unfolding}}}}~\isa{left{\isaliteral{5F}{\isacharunderscore}}inv}~\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}}}}'' would become ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}simp\ only{\isaliteral{3A}{\isacharcolon}}\ left{\isaliteral{5F}{\isacharunderscore}}inv{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'' etc.%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{end}\isamarkupfalse%

%

\isamarkupsubsection{Propositional logic \label{sec:framework-ex-prop}%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

We axiomatize basic connectives of propositional logic: implication,

  disjunction, and conjunction.  The associated rules are modeled

  after Gentzen's system of Natural Deduction \cite{Gentzen:1935}.%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{axiomatization}\isamarkupfalse%

\isanewline

\ \ imp\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}o\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ o\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ o{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infixr}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{2}}{\isadigit{5}}{\isaliteral{29}{\isacharparenright}}\ \isakeyword{where}\isanewline

\ \ impI\ {\isaliteral{5B}{\isacharbrackleft}}intro{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline

\ \ impD\ {\isaliteral{5B}{\isacharbrackleft}}dest{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

\isanewline

\isacommand{axiomatization}\isamarkupfalse%

\isanewline

\ \ disj\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}o\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ o\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ o{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infixr}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6F723E}{\isasymor}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{3}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ \isakeyword{where}\isanewline

\ \ disjI\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5B}{\isacharbrackleft}}intro{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline

\ \ disjI\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}\ {\isaliteral{5B}{\isacharbrackleft}}intro{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline

\ \ disjE\ {\isaliteral{5B}{\isacharbrackleft}}elim{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

\isanewline

\isacommand{axiomatization}\isamarkupfalse%

\isanewline

\ \ conj\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}o\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ o\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ o{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infixr}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C616E643E}{\isasymand}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{3}}{\isadigit{5}}{\isaliteral{29}{\isacharparenright}}\ \isakeyword{where}\isanewline

\ \ conjI\ {\isaliteral{5B}{\isacharbrackleft}}intro{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline

\ \ conjD\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline

\ \ conjD\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isaliteral{22}{\isachardoublequoteclose}}%

\begin{isamarkuptext}%

\noindent The conjunctive destructions have the disadvantage that

  decomposing \isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequote}}} involves an immediate decision which

  component should be projected.  The more convenient simultaneous

  elimination \isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isaliteral{22}{\isachardoublequote}}} can be derived as

  follows:%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{theorem}\isamarkupfalse%

\ conjE\ {\isaliteral{5B}{\isacharbrackleft}}elim{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline

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

\ \ \isakeyword{obtains}\ A\ \isakeyword{and}\ B\isanewline

%

\isadelimproof

%

\endisadelimproof

%

\isatagproof

\isacommand{proof}\isamarkupfalse%

\isanewline

\ \ \isacommand{from}\isamarkupfalse%

\ {\isaliteral{60}{\isacharbackquoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse%

\ A\ \isacommand{by}\isamarkupfalse%

\ {\isaliteral{28}{\isacharparenleft}}rule\ conjD\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\isanewline

\ \ \isacommand{from}\isamarkupfalse%

\ {\isaliteral{60}{\isacharbackquoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse%

\ B\ \isacommand{by}\isamarkupfalse%

\ {\isaliteral{28}{\isacharparenleft}}rule\ conjD\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\isanewline

\isacommand{qed}\isamarkupfalse%

%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

%

\endisadelimproof

%

\begin{isamarkuptext}%

\noindent Here is an example of swapping conjuncts with a single

  intermediate elimination step:%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimproof

%

\endisadelimproof

%

\isatagproof

\ \ \isacommand{assume}\isamarkupfalse%

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

\ \ \isacommand{then}\isamarkupfalse%

\ \isacommand{obtain}\isamarkupfalse%

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

\isanewline

\ \ \isacommand{then}\isamarkupfalse%

\ \isacommand{have}\isamarkupfalse%

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

%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

%

\endisadelimproof

%

\begin{isamarkuptext}%

\noindent Note that the analogous elimination rule for disjunction

  ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C415353554D45533E}{\isasymASSUMES}}\ A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B\ {\isaliteral{5C3C4F425441494E533E}{\isasymOBTAINS}}\ A\ {\isaliteral{5C3C424241523E}{\isasymBBAR}}\ B{\isaliteral{22}{\isachardoublequote}}}'' coincides with

  the original axiomatization of \isa{disjE}.

  \medskip We continue propositional logic by introducing absurdity

  with its characteristic elimination.  Plain truth may then be

  defined as a proposition that is trivially true.%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{axiomatization}\isamarkupfalse%

\isanewline

\ \ false\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ o\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C626F74746F6D3E}{\isasymbottom}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\ \isakeyword{where}\isanewline

\ \ falseE\ {\isaliteral{5B}{\isacharbrackleft}}elim{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C626F74746F6D3E}{\isasymbottom}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

\isanewline

\isacommand{definition}\isamarkupfalse%

\isanewline

\ \ true\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ o\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C746F703E}{\isasymtop}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\ \isakeyword{where}\isanewline

\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C746F703E}{\isasymtop}}\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{5C3C626F74746F6D3E}{\isasymbottom}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ {\isaliteral{5C3C626F74746F6D3E}{\isasymbottom}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

\isanewline

\isacommand{theorem}\isamarkupfalse%

\ trueI\ {\isaliteral{5B}{\isacharbrackleft}}intro{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C746F703E}{\isasymtop}}\isanewline

%

\isadelimproof

\ \ %

\endisadelimproof

%

\isatagproof

\isacommand{unfolding}\isamarkupfalse%

\ true{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

%

\endisadelimproof

%

\begin{isamarkuptext}%

\medskip\noindent Now negation represents an implication towards

  absurdity:%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{definition}\isamarkupfalse%

\isanewline

\ \ not\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}o\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ o{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isadigit{4}}{\isadigit{0}}{\isaliteral{5D}{\isacharbrackright}}\ {\isadigit{4}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ \isakeyword{where}\isanewline

\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ {\isaliteral{5C3C626F74746F6D3E}{\isasymbottom}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

\isanewline

\isacommand{theorem}\isamarkupfalse%

\ notI\ {\isaliteral{5B}{\isacharbrackleft}}intro{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline

\ \ \isakeyword{assumes}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C626F74746F6D3E}{\isasymbottom}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

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

%

\isadelimproof

%

\endisadelimproof

%

\isatagproof

\isacommand{unfolding}\isamarkupfalse%

\ not{\isaliteral{5F}{\isacharunderscore}}def\isanewline

\isacommand{proof}\isamarkupfalse%

\isanewline

\ \ \isacommand{assume}\isamarkupfalse%

\ A\isanewline

\ \ \isacommand{then}\isamarkupfalse%

\ \isacommand{show}\isamarkupfalse%

\ {\isaliteral{5C3C626F74746F6D3E}{\isasymbottom}}\ \isacommand{by}\isamarkupfalse%

\ {\isaliteral{28}{\isacharparenleft}}rule\ {\isaliteral{60}{\isacharbackquoteopen}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C626F74746F6D3E}{\isasymbottom}}{\isaliteral{60}{\isacharbackquoteclose}}{\isaliteral{29}{\isacharparenright}}\isanewline

\isacommand{qed}\isamarkupfalse%

%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

\isanewline

%

\endisadelimproof

\isanewline

\isacommand{theorem}\isamarkupfalse%

\ notE\ {\isaliteral{5B}{\isacharbrackleft}}elim{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline

\ \ \isakeyword{assumes}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ A\isanewline

\ \ \isakeyword{shows}\ B\isanewline

%

\isadelimproof

%

\endisadelimproof

%

\isatagproof

\isacommand{proof}\isamarkupfalse%

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

\ \ \isacommand{from}\isamarkupfalse%

\ {\isaliteral{60}{\isacharbackquoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{have}\isamarkupfalse%

\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ {\isaliteral{5C3C626F74746F6D3E}{\isasymbottom}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{unfolding}\isamarkupfalse%

\ not{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

\isanewline

\ \ \isacommand{from}\isamarkupfalse%

\ {\isaliteral{60}{\isacharbackquoteopen}}A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ {\isaliteral{5C3C626F74746F6D3E}{\isasymbottom}}{\isaliteral{60}{\isacharbackquoteclose}}\ \isakeyword{and}\ {\isaliteral{60}{\isacharbackquoteopen}}A{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{have}\isamarkupfalse%

\ {\isaliteral{5C3C626F74746F6D3E}{\isasymbottom}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

\isanewline

\ \ \isacommand{then}\isamarkupfalse%

\ \isacommand{show}\isamarkupfalse%

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

\isanewline

\isacommand{qed}\isamarkupfalse%

%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

%

\endisadelimproof

%

\isamarkupsubsection{Classical logic%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

Subsequently we state the principle of classical contradiction as a

  local assumption.  Thus we refrain from forcing the object-logic

  into the classical perspective.  Within that context, we may derive

  well-known consequences of the classical principle.%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{locale}\isamarkupfalse%

\ classical\ {\isaliteral{3D}{\isacharequal}}\isanewline

\ \ \isakeyword{assumes}\ classical{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ C\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

\isakeyword{begin}\isanewline

\isanewline

\isacommand{theorem}\isamarkupfalse%

\ double{\isaliteral{5F}{\isacharunderscore}}negation{\isaliteral{3A}{\isacharcolon}}\isanewline

\ \ \isakeyword{assumes}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ C{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

\ \ \isakeyword{shows}\ C\isanewline

%

\isadelimproof

%

\endisadelimproof

%

\isatagproof

\isacommand{proof}\isamarkupfalse%

\ {\isaliteral{28}{\isacharparenleft}}rule\ classical{\isaliteral{29}{\isacharparenright}}\isanewline

\ \ \isacommand{assume}\isamarkupfalse%

\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ C{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

\ \ \isacommand{with}\isamarkupfalse%

\ {\isaliteral{60}{\isacharbackquoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ C{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse%

\ C\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

\isanewline

\isacommand{qed}\isamarkupfalse%

%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

\isanewline

%

\endisadelimproof

\isanewline

\isacommand{theorem}\isamarkupfalse%

\ tertium{\isaliteral{5F}{\isacharunderscore}}non{\isaliteral{5F}{\isacharunderscore}}datur{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}C\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ C{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

%

\isadelimproof

%

\endisadelimproof

%

\isatagproof

\isacommand{proof}\isamarkupfalse%

\ {\isaliteral{28}{\isacharparenleft}}rule\ double{\isaliteral{5F}{\isacharunderscore}}negation{\isaliteral{29}{\isacharparenright}}\isanewline

\ \ \isacommand{show}\isamarkupfalse%

\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ {\isaliteral{28}{\isacharparenleft}}C\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ C{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

\ \ \isacommand{proof}\isamarkupfalse%

\isanewline

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

\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ {\isaliteral{28}{\isacharparenleft}}C\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ C{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

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

\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ C{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

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

\isanewline

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

\ C\ \isacommand{then}\isamarkupfalse%

\ \isacommand{have}\isamarkupfalse%

\ {\isaliteral{22}{\isachardoublequoteopen}}C\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ C{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

\isanewline

\ \ \ \ \ \ \isacommand{with}\isamarkupfalse%

\ {\isaliteral{60}{\isacharbackquoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ {\isaliteral{28}{\isacharparenleft}}C\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ C{\isaliteral{29}{\isacharparenright}}{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse%

\ {\isaliteral{5C3C626F74746F6D3E}{\isasymbottom}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

\isanewline

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

\isanewline

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

\ \isacommand{have}\isamarkupfalse%

\ {\isaliteral{22}{\isachardoublequoteopen}}C\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ C{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

\isanewline

\ \ \ \ \isacommand{with}\isamarkupfalse%

\ {\isaliteral{60}{\isacharbackquoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ {\isaliteral{28}{\isacharparenleft}}C\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ C{\isaliteral{29}{\isacharparenright}}{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse%

\ {\isaliteral{5C3C626F74746F6D3E}{\isasymbottom}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

\isanewline

\ \ \isacommand{qed}\isamarkupfalse%

\isanewline

\isacommand{qed}\isamarkupfalse%

%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

%

\endisadelimproof

%

\begin{isamarkuptext}%

\noindent These examples illustrate both classical reasoning and

  non-trivial propositional proofs in general.  All three rules

  characterize classical logic independently, but the original rule is

  already the most convenient to use, because it leaves the conclusion

  unchanged.  Note that \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ C\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isaliteral{22}{\isachardoublequote}}} fits again into our

  format for eliminations, despite the additional twist that the

  context refers to the main conclusion.  So we may write \isa{classical} as the Isar statement ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C4F425441494E533E}{\isasymOBTAINS}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ thesis{\isaliteral{22}{\isachardoublequote}}}''.

  This also explains nicely how classical reasoning really works:

  whatever the main \isa{thesis} might be, we may always assume its

  negation!%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{end}\isamarkupfalse%

%

\isamarkupsubsection{Quantifiers \label{sec:framework-ex-quant}%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

Representing quantifiers is easy, thanks to the higher-order nature

  of the underlying framework.  According to the well-known technique

  introduced by Church \cite{church40}, quantifiers are operators on

  predicates, which are syntactically represented as \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}{\isaliteral{22}{\isachardoublequote}}}-terms

  of type \isa{{\isaliteral{22}{\isachardoublequote}}i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ o{\isaliteral{22}{\isachardoublequote}}}.  Binder notation turns \isa{{\isaliteral{22}{\isachardoublequote}}All\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ B\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} into \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ B\ x{\isaliteral{22}{\isachardoublequote}}} etc.%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{axiomatization}\isamarkupfalse%

\isanewline

\ \ All\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ o{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ o{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{28}{\isacharparenleft}}\isakeyword{binder}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{1}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ \isakeyword{where}\isanewline

\ \ allI\ {\isaliteral{5B}{\isacharbrackleft}}intro{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ B\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline

\ \ allD\ {\isaliteral{5B}{\isacharbrackleft}}dest{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ B\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ a{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

\isanewline

\isacommand{axiomatization}\isamarkupfalse%

\isanewline

\ \ Ex\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ o{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ o{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{28}{\isacharparenleft}}\isakeyword{binder}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{1}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ \isakeyword{where}\isanewline

\ \ exI\ {\isaliteral{5B}{\isacharbrackleft}}intro{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}B\ a\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ B\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline

\ \ exE\ {\isaliteral{5B}{\isacharbrackleft}}elim{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ B\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ B\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isaliteral{22}{\isachardoublequoteclose}}%

\begin{isamarkuptext}%

\noindent The statement of \isa{exE} corresponds to ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C415353554D45533E}{\isasymASSUMES}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ B\ x\ {\isaliteral{5C3C4F425441494E533E}{\isasymOBTAINS}}\ x\ {\isaliteral{5C3C57484552453E}{\isasymWHERE}}\ B\ x{\isaliteral{22}{\isachardoublequote}}}'' in Isar.  In the

  subsequent example we illustrate quantifier reasoning involving all

  four rules:%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{theorem}\isamarkupfalse%

\isanewline

\ \ \isakeyword{assumes}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}y{\isaliteral{2E}{\isachardot}}\ R\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

\ \ \isakeyword{shows}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}y{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ R\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

%

\isadelimproof

%

\endisadelimproof

%

\isatagproof

\isacommand{proof}\isamarkupfalse%

\ \ \ \ %

\isamarkupcmt{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}{\isaliteral{22}{\isachardoublequote}}} introduction%

}

\isanewline

\ \ \isacommand{obtain}\isamarkupfalse%

\ x\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}y{\isaliteral{2E}{\isachardot}}\ R\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{using}\isamarkupfalse%

\ {\isaliteral{60}{\isacharbackquoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}y{\isaliteral{2E}{\isachardot}}\ R\ x\ y{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

\ \ \ \ %

\isamarkupcmt{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}{\isaliteral{22}{\isachardoublequote}}} elimination%

}

\isanewline

\ \ \isacommand{fix}\isamarkupfalse%

\ y\ \isacommand{have}\isamarkupfalse%

\ {\isaliteral{22}{\isachardoublequoteopen}}R\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{using}\isamarkupfalse%

\ {\isaliteral{60}{\isacharbackquoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}y{\isaliteral{2E}{\isachardot}}\ R\ x\ y{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

\ \ \ \ %

\isamarkupcmt{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}{\isaliteral{22}{\isachardoublequote}}} destruction%

}

\isanewline

\ \ \isacommand{then}\isamarkupfalse%

\ \isacommand{show}\isamarkupfalse%

\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ R\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

\ \ \ \ %

\isamarkupcmt{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}{\isaliteral{22}{\isachardoublequote}}} introduction%

}

\isanewline

\isacommand{qed}\isamarkupfalse%

%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

%

\endisadelimproof

%

\isamarkupsubsection{Canonical reasoning patterns%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

The main rules of first-order predicate logic from

  \secref{sec:framework-ex-prop} and \secref{sec:framework-ex-quant}

  can now be summarized as follows, using the native Isar statement

  format of \secref{sec:framework-stmt}.

  \medskip

  \begin{tabular}{l}

  \isa{{\isaliteral{22}{\isachardoublequote}}impI{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C415353554D45533E}{\isasymASSUMES}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ {\isaliteral{5C3C53484F57533E}{\isasymSHOWS}}\ A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ B{\isaliteral{22}{\isachardoublequote}}} \\

  \isa{{\isaliteral{22}{\isachardoublequote}}impD{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C415353554D45533E}{\isasymASSUMES}}\ A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ B\ {\isaliteral{5C3C414E443E}{\isasymAND}}\ A\ {\isaliteral{5C3C53484F57533E}{\isasymSHOWS}}\ B{\isaliteral{22}{\isachardoublequote}}} \\[1ex]

  \isa{{\isaliteral{22}{\isachardoublequote}}disjI\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C415353554D45533E}{\isasymASSUMES}}\ A\ {\isaliteral{5C3C53484F57533E}{\isasymSHOWS}}\ A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B{\isaliteral{22}{\isachardoublequote}}} \\

  \isa{{\isaliteral{22}{\isachardoublequote}}disjI\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C415353554D45533E}{\isasymASSUMES}}\ B\ {\isaliteral{5C3C53484F57533E}{\isasymSHOWS}}\ A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B{\isaliteral{22}{\isachardoublequote}}} \\

  \isa{{\isaliteral{22}{\isachardoublequote}}disjE{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C415353554D45533E}{\isasymASSUMES}}\ A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B\ {\isaliteral{5C3C4F425441494E533E}{\isasymOBTAINS}}\ A\ {\isaliteral{5C3C424241523E}{\isasymBBAR}}\ B{\isaliteral{22}{\isachardoublequote}}} \\[1ex]

  \isa{{\isaliteral{22}{\isachardoublequote}}conjI{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C415353554D45533E}{\isasymASSUMES}}\ A\ {\isaliteral{5C3C414E443E}{\isasymAND}}\ B\ {\isaliteral{5C3C53484F57533E}{\isasymSHOWS}}\ A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequote}}} \\

  \isa{{\isaliteral{22}{\isachardoublequote}}conjE{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C415353554D45533E}{\isasymASSUMES}}\ A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B\ {\isaliteral{5C3C4F425441494E533E}{\isasymOBTAINS}}\ A\ {\isaliteral{5C3C414E443E}{\isasymAND}}\ B{\isaliteral{22}{\isachardoublequote}}} \\[1ex]

  \isa{{\isaliteral{22}{\isachardoublequote}}falseE{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C415353554D45533E}{\isasymASSUMES}}\ {\isaliteral{5C3C626F74746F6D3E}{\isasymbottom}}\ {\isaliteral{5C3C53484F57533E}{\isasymSHOWS}}\ A{\isaliteral{22}{\isachardoublequote}}} \\

  \isa{{\isaliteral{22}{\isachardoublequote}}trueI{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C53484F57533E}{\isasymSHOWS}}\ {\isaliteral{5C3C746F703E}{\isasymtop}}{\isaliteral{22}{\isachardoublequote}}} \\[1ex]

  \isa{{\isaliteral{22}{\isachardoublequote}}notI{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C415353554D45533E}{\isasymASSUMES}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C626F74746F6D3E}{\isasymbottom}}\ {\isaliteral{5C3C53484F57533E}{\isasymSHOWS}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A{\isaliteral{22}{\isachardoublequote}}} \\

  \isa{{\isaliteral{22}{\isachardoublequote}}notE{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C415353554D45533E}{\isasymASSUMES}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A\ {\isaliteral{5C3C414E443E}{\isasymAND}}\ A\ {\isaliteral{5C3C53484F57533E}{\isasymSHOWS}}\ B{\isaliteral{22}{\isachardoublequote}}} \\[1ex]

  \isa{{\isaliteral{22}{\isachardoublequote}}allI{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C415353554D45533E}{\isasymASSUMES}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ B\ x\ {\isaliteral{5C3C53484F57533E}{\isasymSHOWS}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ B\ x{\isaliteral{22}{\isachardoublequote}}} \\

  \isa{{\isaliteral{22}{\isachardoublequote}}allE{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C415353554D45533E}{\isasymASSUMES}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ B\ x\ {\isaliteral{5C3C53484F57533E}{\isasymSHOWS}}\ B\ a{\isaliteral{22}{\isachardoublequote}}} \\[1ex]

  \isa{{\isaliteral{22}{\isachardoublequote}}exI{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C415353554D45533E}{\isasymASSUMES}}\ B\ a\ {\isaliteral{5C3C53484F57533E}{\isasymSHOWS}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ B\ x{\isaliteral{22}{\isachardoublequote}}} \\

  \isa{{\isaliteral{22}{\isachardoublequote}}exE{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C415353554D45533E}{\isasymASSUMES}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ B\ x\ {\isaliteral{5C3C4F425441494E533E}{\isasymOBTAINS}}\ a\ {\isaliteral{5C3C57484552453E}{\isasymWHERE}}\ B\ a{\isaliteral{22}{\isachardoublequote}}}

  \end{tabular}

  \medskip

  \noindent This essentially provides a declarative reading of Pure

  rules as Isar reasoning patterns: the rule statements tells how a

  canonical proof outline shall look like.  Since the above rules have

  already been declared as \hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}}, \hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}, \hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}} --- each according to its

  particular shape --- we can immediately write Isar proof texts as

  follows:%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimproof

%

\endisadelimproof

%

\isatagproof

%

\begin{minipage}[t]{0.4\textwidth}

\isanewline

\ \ \isacommand{have}\isamarkupfalse%

\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

\ \ \isacommand{proof}\isamarkupfalse%

\isanewline

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

\ A\isanewline

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

\ B%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

%

\endisadelimproof

%

\isadelimnoproof

\ %

\endisadelimnoproof

%

\isatagnoproof

\isacommand{sorry}\isamarkupfalse%

%

\endisatagnoproof

{\isafoldnoproof}%

%

\isadelimnoproof

\isanewline

%

\endisadelimnoproof

%

\isadelimproof

\ \ %

\endisadelimproof

%

\isatagproof

\isacommand{qed}\isamarkupfalse%

%

\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}

\isanewline

\ \ \isacommand{have}\isamarkupfalse%

\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ A%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

%

\endisadelimproof

%

\isadelimnoproof

\ %

\endisadelimnoproof

%

\isatagnoproof

\isacommand{sorry}\isamarkupfalse%

%

\endisatagnoproof

{\isafoldnoproof}%

%

\isadelimnoproof

\isanewline

%

\endisadelimnoproof

%

\isadelimproof

\ \ %

\endisadelimproof

%

\isatagproof

\isacommand{then}\isamarkupfalse%

\ \isacommand{have}\isamarkupfalse%

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

%

\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}

\isanewline

\ \ \isacommand{have}\isamarkupfalse%

\ A%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

%

\endisadelimproof

%

\isadelimnoproof

\ %

\endisadelimnoproof

%

\isatagnoproof

\isacommand{sorry}\isamarkupfalse%

%

\endisatagnoproof

{\isafoldnoproof}%

%

\isadelimnoproof

\isanewline

%

\endisadelimnoproof

%

\isadelimproof

\ \ %

\endisadelimproof

%

\isatagproof

\isacommand{then}\isamarkupfalse%

\ \isacommand{have}\isamarkupfalse%

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

\isanewline

\isanewline

\ \ \isacommand{have}\isamarkupfalse%

\ B%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

%

\endisadelimproof

%

\isadelimnoproof

\ %

\endisadelimnoproof

%

\isatagnoproof

\isacommand{sorry}\isamarkupfalse%

%

\endisatagnoproof

{\isafoldnoproof}%

%

\isadelimnoproof

\isanewline

%

\endisadelimnoproof

%

\isadelimproof

\ \ %

\endisadelimproof

%

\isatagproof

\isacommand{then}\isamarkupfalse%

\ \isacommand{have}\isamarkupfalse%

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

%

\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}

\isanewline

\ \ \isacommand{have}\isamarkupfalse%

\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B{\isaliteral{22}{\isachardoublequoteclose}}%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

%

\endisadelimproof

%

\isadelimnoproof

\ %

\endisadelimnoproof

%

\isatagnoproof

\isacommand{sorry}\isamarkupfalse%

%

\endisatagnoproof

{\isafoldnoproof}%

%

\isadelimnoproof

\isanewline

%

\endisadelimnoproof

%

\isadelimproof

\ \ %

\endisadelimproof

%

\isatagproof

\isacommand{then}\isamarkupfalse%

\ \isacommand{have}\isamarkupfalse%

\ C\isanewline

\ \ \isacommand{proof}\isamarkupfalse%

\isanewline

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

\ A\isanewline

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

\ \isacommand{show}\isamarkupfalse%

\ C%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

%

\endisadelimproof

%