wneuper/isa: doc-src/IsarRef/Thy/document/First_Order

1 %

     2 \begin{isabellebody}%

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

4 %

     5 \isamarkupheader{Example: First-Order Logic%

6 }

     7 \isamarkuptrue%

8 %

     9 \isadelimvisible

    10 %

    11 \endisadelimvisible

    12 %

    13 \isatagvisible

    14 \isacommand{theory}\isamarkupfalse%

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

    16 \isakeyword{imports}\ Base\ \ \isanewline

    17 \isakeyword{begin}%

    18 \endisatagvisible

    19 {\isafoldvisible}%

    20 %

    21 \isadelimvisible

    22 %

    23 \endisadelimvisible

    24 %

    25 \begin{isamarkuptext}%

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

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

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

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

    30   separate judgment.%

    31 \end{isamarkuptext}%

    32 \isamarkuptrue%

    33 \isacommand{typedecl}\isamarkupfalse%

    34 \ i\isanewline

    35 \isacommand{typedecl}\isamarkupfalse%

    36 \ o\isanewline

    37 \isanewline

    38 \isacommand{judgment}\isamarkupfalse%

    39 \isanewline

    40 \ \ 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}}%

    41 \begin{isamarkuptext}%

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

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

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

    45   object-logic''.%

    46 \end{isamarkuptext}%

    47 \isamarkuptrue%

    48 %

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

    50 }

    51 \isamarkuptrue%

    52 %

    53 \begin{isamarkuptext}%

    54 Equality is axiomatized as a binary predicate on individuals, with

    55   reflexivity as introduction, and substitution as elimination

    56   principle.  Note that the latter is particularly convenient in a

    57   framework like Isabelle, because syntactic congruences are

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

    59   expressions containing occurrences of \isa{x}.%

    60 \end{isamarkuptext}%

    61 \isamarkuptrue%

    62 \isacommand{axiomatization}\isamarkupfalse%

    63 \isanewline

    64 \ \ 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

    65 \isakeyword{where}\isanewline

    66 \ \ 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

    67 \ \ 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}}%

    68 \begin{isamarkuptext}%

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

    70   full generality.  We derive some common symmetry~/ transitivity

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

    72 \end{isamarkuptext}%

    73 \isamarkuptrue%

    74 \isacommand{theorem}\isamarkupfalse%

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

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

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

    78 %

    79 \isadelimproof

    80 %

    81 \endisadelimproof

    82 %

    83 \isatagproof

    84 \isacommand{proof}\isamarkupfalse%

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

    86 \ \ \isacommand{have}\isamarkupfalse%

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

    88 \isanewline

    89 \ \ \isacommand{with}\isamarkupfalse%

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

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

    92 \isanewline

    93 \isacommand{qed}\isamarkupfalse%

    94 %

    95 \endisatagproof

    96 {\isafoldproof}%

    97 %

    98 \isadelimproof

    99 \isanewline

   100 %

   101 \endisadelimproof

   102 \isanewline

   103 \isacommand{theorem}\isamarkupfalse%

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

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

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

   107 %

   108 \isadelimproof

   109 %

   110 \endisadelimproof

   111 %

   112 \isatagproof

   113 \isacommand{proof}\isamarkupfalse%

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

   115 \ \ \isacommand{from}\isamarkupfalse%

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

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

   118 \isanewline

   119 \ \ \isacommand{from}\isamarkupfalse%

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

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

   122 \isanewline

   123 \isacommand{qed}\isamarkupfalse%

   124 %

   125 \endisatagproof

   126 {\isafoldproof}%

   127 %

   128 \isadelimproof

   129 \isanewline

   130 %

   131 \endisadelimproof

   132 \isanewline

   133 \isacommand{theorem}\isamarkupfalse%

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

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

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

   137 %

   138 \isadelimproof

   139 %

   140 \endisadelimproof

   141 %

   142 \isatagproof

   143 \isacommand{proof}\isamarkupfalse%

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

   145 \ \ \isacommand{from}\isamarkupfalse%

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

   147 \ \ \isacommand{show}\isamarkupfalse%

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

   149 \isanewline

   150 \isacommand{qed}\isamarkupfalse%

   151 %

   152 \endisatagproof

   153 {\isafoldproof}%

   154 %

   155 \isadelimproof

   156 \isanewline

   157 %

   158 \endisadelimproof

   159 \isanewline

   160 \isacommand{theorem}\isamarkupfalse%

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

   162 \ \ \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

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

   164 %

   165 \isadelimproof

   166 %

   167 \endisadelimproof

   168 %

   169 \isatagproof

   170 \isacommand{proof}\isamarkupfalse%

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

   172 \ \ \isacommand{from}\isamarkupfalse%

   173 \ {\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

   174 \ \ \isacommand{show}\isamarkupfalse%

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

   176 \isanewline

   177 \isacommand{qed}\isamarkupfalse%

   178 %

   179 \endisatagproof

   180 {\isafoldproof}%

   181 %

   182 \isadelimproof

   183 %

   184 \endisadelimproof

   185 %

   186 \isamarkupsubsection{Basic group theory%

   187 }

   188 \isamarkuptrue%

   189 %

   190 \begin{isamarkuptext}%

   191 As an example for equational reasoning we consider some bits of

   192   group theory.  The subsequent locale definition postulates group

   193   operations and axioms; we also derive some consequences of this

   194   specification.%

   195 \end{isamarkuptext}%

   196 \isamarkuptrue%

   197 \isacommand{locale}\isamarkupfalse%

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

   199 \ \ \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

   200 \ \ \ \ \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

   201 \ \ \ \ \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

   202 \ \ \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

   203 \ \ \ \ \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

   204 \ \ \ \ \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

   205 \isakeyword{begin}\isanewline

   206 \isanewline

   207 \isacommand{theorem}\isamarkupfalse%

   208 \ 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

   209 %

   210 \isadelimproof

   211 %

   212 \endisadelimproof

   213 %

   214 \isatagproof

   215 \isacommand{proof}\isamarkupfalse%

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

   217 \ \ \isacommand{have}\isamarkupfalse%

   218 \ {\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%

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

   220 \ \ \isacommand{also}\isamarkupfalse%

   221 \ \isacommand{have}\isamarkupfalse%

   222 \ {\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%

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

   224 \ \ \isacommand{also}\isamarkupfalse%

   225 \ \isacommand{have}\isamarkupfalse%

   226 \ {\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%

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

   228 \ \ \isacommand{also}\isamarkupfalse%

   229 \ \isacommand{have}\isamarkupfalse%

   230 \ {\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%

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

   232 \ \ \isacommand{also}\isamarkupfalse%

   233 \ \isacommand{have}\isamarkupfalse%

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

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

   236 \ \ \isacommand{also}\isamarkupfalse%

   237 \ \isacommand{have}\isamarkupfalse%

   238 \ {\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%

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

   240 \ \ \isacommand{also}\isamarkupfalse%

   241 \ \isacommand{have}\isamarkupfalse%

   242 \ {\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%

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

   244 \ \ \isacommand{also}\isamarkupfalse%

   245 \ \isacommand{have}\isamarkupfalse%

   246 \ {\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%

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

   248 \ \ \isacommand{finally}\isamarkupfalse%

   249 \ \isacommand{show}\isamarkupfalse%

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

   251 \isanewline

   252 \isacommand{qed}\isamarkupfalse%

   253 %

   254 \endisatagproof

   255 {\isafoldproof}%

   256 %

   257 \isadelimproof

   258 \isanewline

   259 %

   260 \endisadelimproof

   261 \isanewline

   262 \isacommand{theorem}\isamarkupfalse%

   263 \ 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

   264 %

   265 \isadelimproof

   266 %

   267 \endisadelimproof

   268 %

   269 \isatagproof

   270 \isacommand{proof}\isamarkupfalse%

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

   272 \ \ \isacommand{have}\isamarkupfalse%

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

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

   275 \ \ \isacommand{also}\isamarkupfalse%

   276 \ \isacommand{have}\isamarkupfalse%

   277 \ {\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%

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

   279 \ \ \isacommand{also}\isamarkupfalse%

   280 \ \isacommand{have}\isamarkupfalse%

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

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

   283 \ \ \isacommand{also}\isamarkupfalse%

   284 \ \isacommand{have}\isamarkupfalse%

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

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

   287 \ \ \isacommand{finally}\isamarkupfalse%

   288 \ \isacommand{show}\isamarkupfalse%

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

   290 \isanewline

   291 \isacommand{qed}\isamarkupfalse%

   292 %

   293 \endisatagproof

   294 {\isafoldproof}%

   295 %

   296 \isadelimproof

   297 %

   298 \endisadelimproof

   299 %

   300 \begin{isamarkuptext}%

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

   302   work by producing various instances of the given rules (potentially

   303   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

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

   305   involve any of the transitivity rules declared in

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

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

   308   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.

   310   Occasional substitutions in calculations are adequate, but should

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

   312   plain transitivity only, with replacements occurring always in

   313   topmost position. For example:%

   314 \end{isamarkuptext}%

   315 \isamarkuptrue%

   316 %

   317 \isadelimproof

   318 %

   319 \endisadelimproof

   320 %

   321 \isatagproof

   322 \ \ \isacommand{have}\isamarkupfalse%

   323 \ {\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%

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

   325 \isanewline

   326 \ \ \isacommand{also}\isamarkupfalse%

   327 \ \isacommand{have}\isamarkupfalse%

   328 \ {\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%

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

   330 \isanewline

   331 \ \ \isacommand{also}\isamarkupfalse%

   332 \ \isacommand{have}\isamarkupfalse%

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

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

   335 \isanewline

   336 \ \ \isacommand{also}\isamarkupfalse%

   337 \ \isacommand{have}\isamarkupfalse%

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

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

   340 \isanewline

   341 \ \ \isacommand{finally}\isamarkupfalse%

   342 \ \isacommand{have}\isamarkupfalse%

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

   344 %

   345 \endisatagproof

   346 {\isafoldproof}%

   347 %

   348 \isadelimproof

   349 %

   350 \endisadelimproof

   351 %

   352 \begin{isamarkuptext}%

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

   354   definitions in order to normalize each equational problem.  A more

   355   realistic object-logic would include proper setup for the Simplifier

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

   357   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.%

   358 \end{isamarkuptext}%

   359 \isamarkuptrue%

   360 \isacommand{end}\isamarkupfalse%

   361 %

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

   363 }

   364 \isamarkuptrue%

   365 %

   366 \begin{isamarkuptext}%

   367 We axiomatize basic connectives of propositional logic: implication,

   368   disjunction, and conjunction.  The associated rules are modeled

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

   370 \end{isamarkuptext}%

   371 \isamarkuptrue%

   372 \isacommand{axiomatization}\isamarkupfalse%

   373 \isanewline

   374 \ \ 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

   375 \ \ 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

   376 \ \ 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

   377 \isanewline

   378 \isacommand{axiomatization}\isamarkupfalse%

   379 \isanewline

   380 \ \ 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

   381 \ \ 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

   382 \ \ 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

   383 \ \ 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

   384 \isanewline

   385 \isacommand{axiomatization}\isamarkupfalse%

   386 \isanewline

   387 \ \ 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

   388 \ \ 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

   389 \ \ 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

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

   391 \begin{isamarkuptext}%

   392 \noindent The conjunctive destructions have the disadvantage that

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

   394   component should be projected.  The more convenient simultaneous

   395   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

   396   follows:%

   397 \end{isamarkuptext}%

   398 \isamarkuptrue%

   399 \isacommand{theorem}\isamarkupfalse%

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

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

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

   403 %

   404 \isadelimproof

   405 %

   406 \endisadelimproof

   407 %

   408 \isatagproof

   409 \isacommand{proof}\isamarkupfalse%

   410 \isanewline

   411 \ \ \isacommand{from}\isamarkupfalse%

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

   413 \ A\ \isacommand{by}\isamarkupfalse%

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

   415 \ \ \isacommand{from}\isamarkupfalse%

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

   417 \ B\ \isacommand{by}\isamarkupfalse%

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

   419 \isacommand{qed}\isamarkupfalse%

   420 %

   421 \endisatagproof

   422 {\isafoldproof}%

   423 %

   424 \isadelimproof

   425 %

   426 \endisadelimproof

   427 %

   428 \begin{isamarkuptext}%

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

   430   intermediate elimination step:%

   431 \end{isamarkuptext}%

   432 \isamarkuptrue%

   433 %

   434 \isadelimproof

   435 %

   436 \endisadelimproof

   437 %

   438 \isatagproof

   439 \ \ \isacommand{assume}\isamarkupfalse%

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

   441 \ \ \isacommand{then}\isamarkupfalse%

   442 \ \isacommand{obtain}\isamarkupfalse%

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

   444 \isanewline

   445 \ \ \isacommand{then}\isamarkupfalse%

   446 \ \isacommand{have}\isamarkupfalse%

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

   448 %

   449 \endisatagproof

   450 {\isafoldproof}%

   451 %

   452 \isadelimproof

   453 %

   454 \endisadelimproof

   455 %

   456 \begin{isamarkuptext}%

   457 \noindent Note that the analogous elimination rule for disjunction

   458   ``\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

   459   the original axiomatization of \isa{disjE}.

   461   \medskip We continue propositional logic by introducing absurdity

   462   with its characteristic elimination.  Plain truth may then be

   463   defined as a proposition that is trivially true.%

   464 \end{isamarkuptext}%

   465 \isamarkuptrue%

   466 \isacommand{axiomatization}\isamarkupfalse%

   467 \isanewline

   468 \ \ 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

   469 \ \ 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

   470 \isanewline

   471 \isacommand{definition}\isamarkupfalse%

   472 \isanewline

   473 \ \ 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

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

   475 \isanewline

   476 \isacommand{theorem}\isamarkupfalse%

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

   478 %

   479 \isadelimproof

   480 \ \ %

   481 \endisadelimproof

   482 %

   483 \isatagproof

   484 \isacommand{unfolding}\isamarkupfalse%

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

   486 %

   487 \endisatagproof

   488 {\isafoldproof}%

   489 %

   490 \isadelimproof

   491 %

   492 \endisadelimproof

   493 %

   494 \begin{isamarkuptext}%

   495 \medskip\noindent Now negation represents an implication towards

   496   absurdity:%

   497 \end{isamarkuptext}%

   498 \isamarkuptrue%

   499 \isacommand{definition}\isamarkupfalse%

   500 \isanewline

   501 \ \ 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

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

   503 \isanewline

   504 \isacommand{theorem}\isamarkupfalse%

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

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

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

   508 %

   509 \isadelimproof

   510 %

   511 \endisadelimproof

   512 %

   513 \isatagproof

   514 \isacommand{unfolding}\isamarkupfalse%

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

   516 \isacommand{proof}\isamarkupfalse%

   517 \isanewline

   518 \ \ \isacommand{assume}\isamarkupfalse%

   519 \ A\isanewline

   520 \ \ \isacommand{then}\isamarkupfalse%

   521 \ \isacommand{show}\isamarkupfalse%

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

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

   524 \isacommand{qed}\isamarkupfalse%

   525 %

   526 \endisatagproof

   527 {\isafoldproof}%

   528 %

   529 \isadelimproof

   530 \isanewline

   531 %

   532 \endisadelimproof

   533 \isanewline

   534 \isacommand{theorem}\isamarkupfalse%

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

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

   537 \ \ \isakeyword{shows}\ B\isanewline

   538 %

   539 \isadelimproof

   540 %

   541 \endisadelimproof

   542 %

   543 \isatagproof

   544 \isacommand{proof}\isamarkupfalse%

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

   546 \ \ \isacommand{from}\isamarkupfalse%

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

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

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

   550 \isanewline

   551 \ \ \isacommand{from}\isamarkupfalse%

   552 \ {\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%

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

   554 \isanewline

   555 \ \ \isacommand{then}\isamarkupfalse%

   556 \ \isacommand{show}\isamarkupfalse%

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

   558 \isanewline

   559 \isacommand{qed}\isamarkupfalse%

   560 %

   561 \endisatagproof

   562 {\isafoldproof}%

   563 %

   564 \isadelimproof

   565 %

   566 \endisadelimproof

   567 %

   568 \isamarkupsubsection{Classical logic%

   569 }

   570 \isamarkuptrue%

   571 %

   572 \begin{isamarkuptext}%

   573 Subsequently we state the principle of classical contradiction as a

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

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

   576   well-known consequences of the classical principle.%

   577 \end{isamarkuptext}%

   578 \isamarkuptrue%

   579 \isacommand{locale}\isamarkupfalse%

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

   581 \ \ \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

   582 \isakeyword{begin}\isanewline

   583 \isanewline

   584 \isacommand{theorem}\isamarkupfalse%

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

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

   587 \ \ \isakeyword{shows}\ C\isanewline

   588 %

   589 \isadelimproof

   590 %

   591 \endisadelimproof

   592 %

   593 \isatagproof

   594 \isacommand{proof}\isamarkupfalse%

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

   596 \ \ \isacommand{assume}\isamarkupfalse%

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

   598 \ \ \isacommand{with}\isamarkupfalse%

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

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

   601 \isanewline

   602 \isacommand{qed}\isamarkupfalse%

   603 %

   604 \endisatagproof

   605 {\isafoldproof}%

   606 %

   607 \isadelimproof

   608 \isanewline

   609 %

   610 \endisadelimproof

   611 \isanewline

   612 \isacommand{theorem}\isamarkupfalse%

   613 \ 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

   614 %

   615 \isadelimproof

   616 %

   617 \endisadelimproof

   618 %

   619 \isatagproof

   620 \isacommand{proof}\isamarkupfalse%

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

   622 \ \ \isacommand{show}\isamarkupfalse%

   623 \ {\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

   624 \ \ \isacommand{proof}\isamarkupfalse%

   625 \isanewline

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

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

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

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

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

   631 \isanewline

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

   633 \ C\ \isacommand{then}\isamarkupfalse%

   634 \ \isacommand{have}\isamarkupfalse%

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

   636 \isanewline

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

   638 \ {\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%

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

   640 \isanewline

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

   642 \isanewline

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

   644 \ \isacommand{have}\isamarkupfalse%

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

   646 \isanewline

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

   648 \ {\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%

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

   650 \isanewline

   651 \ \ \isacommand{qed}\isamarkupfalse%

   652 \isanewline

   653 \isacommand{qed}\isamarkupfalse%

   654 %

   655 \endisatagproof

   656 {\isafoldproof}%

   657 %

   658 \isadelimproof

   659 %

   660 \endisadelimproof

   661 %

   662 \begin{isamarkuptext}%

   663 \noindent These examples illustrate both classical reasoning and

   664   non-trivial propositional proofs in general.  All three rules

   665   characterize classical logic independently, but the original rule is

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

   667   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

   668   format for eliminations, despite the additional twist that the

   669   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}}}''.

   670   This also explains nicely how classical reasoning really works:

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

   672   negation!%

   673 \end{isamarkuptext}%

   674 \isamarkuptrue%

   675 \isacommand{end}\isamarkupfalse%

   676 %

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

   678 }

   679 \isamarkuptrue%

   680 %

   681 \begin{isamarkuptext}%

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

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

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

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

   686   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.%

   687 \end{isamarkuptext}%

   688 \isamarkuptrue%

   689 \isacommand{axiomatization}\isamarkupfalse%

   690 \isanewline

   691 \ \ 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

   692 \ \ 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

   693 \ \ 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

   694 \isanewline

   695 \isacommand{axiomatization}\isamarkupfalse%

   696 \isanewline

   697 \ \ 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

   698 \ \ 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

   699 \ \ 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}}%

   700 \begin{isamarkuptext}%

   701 \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

   702   subsequent example we illustrate quantifier reasoning involving all

   703   four rules:%

   704 \end{isamarkuptext}%

   705 \isamarkuptrue%

   706 \isacommand{theorem}\isamarkupfalse%

   707 \isanewline

   708 \ \ \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

   709 \ \ \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

   710 %

   711 \isadelimproof

   712 %

   713 \endisadelimproof

   714 %

   715 \isatagproof

   716 \isacommand{proof}\isamarkupfalse%

   717 \ \ \ \ %

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

   719 }

   720 \isanewline

   721 \ \ \isacommand{obtain}\isamarkupfalse%

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

   723 \ {\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%

   724 \ \ \ \ %

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

   726 }

   727 \isanewline

   728 \ \ \isacommand{fix}\isamarkupfalse%

   729 \ y\ \isacommand{have}\isamarkupfalse%

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

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

   732 \ \ \ \ %

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

   734 }

   735 \isanewline

   736 \ \ \isacommand{then}\isamarkupfalse%

   737 \ \isacommand{show}\isamarkupfalse%

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

   739 \ \ \ \ %

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

   741 }

   742 \isanewline

   743 \isacommand{qed}\isamarkupfalse%

   744 %

   745 \endisatagproof

   746 {\isafoldproof}%

   747 %

   748 \isadelimproof

   749 %

   750 \endisadelimproof

   751 %

   752 \isamarkupsubsection{Canonical reasoning patterns%

   753 }

   754 \isamarkuptrue%

   755 %

   756 \begin{isamarkuptext}%

   757 The main rules of first-order predicate logic from

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

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

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

   762   \medskip

   763   \begin{tabular}{l}

   764   \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}}} \\

   765   \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]

   767   \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}}} \\

   768   \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}}} \\

   769   \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]

   771   \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}}} \\

   772   \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]

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

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

   777   \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}}} \\

   778   \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]

   780   \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}}} \\

   781   \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]

   783   \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}}} \\

   784   \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}}}

   785   \end{tabular}

   786   \medskip

   788   \noindent This essentially provides a declarative reading of Pure

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

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

   791   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

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

   793   follows:%

   794 \end{isamarkuptext}%

   795 \isamarkuptrue%

   796 %

   797 \isadelimproof

   798 %

   799 \endisadelimproof

   800 %

   801 \isatagproof

   802 %

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

   804 \isanewline

   805 \ \ \isacommand{have}\isamarkupfalse%

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

   807 \ \ \isacommand{proof}\isamarkupfalse%

   808 \isanewline

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

   810 \ A\isanewline

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

   812 \ B%

   813 \endisatagproof

   814 {\isafoldproof}%

   815 %

   816 \isadelimproof

   817 %

   818 \endisadelimproof

   819 %

   820 \isadelimnoproof

   821 \ %

   822 \endisadelimnoproof

   823 %

   824 \isatagnoproof

   825 \isacommand{sorry}\isamarkupfalse%

   826 %

   827 \endisatagnoproof

   828 {\isafoldnoproof}%

   829 %

   830 \isadelimnoproof

   831 \isanewline

   832 %

   833 \endisadelimnoproof

   834 %

   835 \isadelimproof

   836 \ \ %

   837 \endisadelimproof

   838 %

   839 \isatagproof

   840 \isacommand{qed}\isamarkupfalse%

   841 %

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

   843 \isanewline

   844 \ \ \isacommand{have}\isamarkupfalse%

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

   846 \endisatagproof

   847 {\isafoldproof}%

   848 %

   849 \isadelimproof

   850 %

   851 \endisadelimproof

   852 %

   853 \isadelimnoproof

   854 \ %

   855 \endisadelimnoproof

   856 %

   857 \isatagnoproof

   858 \isacommand{sorry}\isamarkupfalse%

   859 %

   860 \endisatagnoproof

   861 {\isafoldnoproof}%

   862 %

   863 \isadelimnoproof

   864 \isanewline

   865 %

   866 \endisadelimnoproof

   867 %

   868 \isadelimproof

   869 \ \ %

   870 \endisadelimproof

   871 %

   872 \isatagproof

   873 \isacommand{then}\isamarkupfalse%

   874 \ \isacommand{have}\isamarkupfalse%

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

   876 %

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

   878 \isanewline

   879 \ \ \isacommand{have}\isamarkupfalse%

   880 \ A%

   881 \endisatagproof

   882 {\isafoldproof}%

   883 %

   884 \isadelimproof

   885 %

   886 \endisadelimproof

   887 %

   888 \isadelimnoproof

   889 \ %

   890 \endisadelimnoproof

   891 %

   892 \isatagnoproof

   893 \isacommand{sorry}\isamarkupfalse%

   894 %

   895 \endisatagnoproof

   896 {\isafoldnoproof}%

   897 %

   898 \isadelimnoproof

   899 \isanewline

   900 %

   901 \endisadelimnoproof

   902 %

   903 \isadelimproof

   904 \ \ %

   905 \endisadelimproof

   906 %

   907 \isatagproof

   908 \isacommand{then}\isamarkupfalse%

   909 \ \isacommand{have}\isamarkupfalse%

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

   911 \isanewline

   912 \isanewline

   913 \ \ \isacommand{have}\isamarkupfalse%

   914 \ B%

   915 \endisatagproof

   916 {\isafoldproof}%

   917 %

   918 \isadelimproof

   919 %

   920 \endisadelimproof

   921 %

   922 \isadelimnoproof

   923 \ %

   924 \endisadelimnoproof

   925 %

   926 \isatagnoproof

   927 \isacommand{sorry}\isamarkupfalse%

   928 %

   929 \endisatagnoproof

   930 {\isafoldnoproof}%

   931 %

   932 \isadelimnoproof

   933 \isanewline

   934 %

   935 \endisadelimnoproof

   936 %

   937 \isadelimproof

   938 \ \ %

   939 \endisadelimproof

   940 %

   941 \isatagproof

   942 \isacommand{then}\isamarkupfalse%

   943 \ \isacommand{have}\isamarkupfalse%

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

   945 %

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

   947 \isanewline

   948 \ \ \isacommand{have}\isamarkupfalse%

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

   950 \endisatagproof

   951 {\isafoldproof}%

   952 %

   953 \isadelimproof

   954 %

   955 \endisadelimproof

   956 %

   957 \isadelimnoproof

   958 \ %

   959 \endisadelimnoproof

   960 %

   961 \isatagnoproof

   962 \isacommand{sorry}\isamarkupfalse%

   963 %

   964 \endisatagnoproof

   965 {\isafoldnoproof}%

   966 %

   967 \isadelimnoproof

   968 \isanewline

   969 %

   970 \endisadelimnoproof

   971 %

   972 \isadelimproof

   973 \ \ %

   974 \endisadelimproof

   975 %

   976 \isatagproof

   977 \isacommand{then}\isamarkupfalse%

   978 \ \isacommand{have}\isamarkupfalse%

   979 \ C\isanewline

   980 \ \ \isacommand{proof}\isamarkupfalse%

   981 \isanewline

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

   983 \ A\isanewline

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

   985 \ \isacommand{show}\isamarkupfalse%

   986 \ C%

   987 \endisatagproof

   988 {\isafoldproof}%

   989 %

   990 \isadelimproof

   991 %

   992 \endisadelimproof

   993 %

   994 \isadelimnoproof

   995 \ %

   996 \endisadelimnoproof

   997 %

   998 \isatagnoproof

   999 \isacommand{sorry}\isamarkupfalse%

  1000 %

  1001 \endisatagnoproof

  1002 {\isafoldnoproof}%

  1003 %

  1004 \isadelimnoproof

  1005 \isanewline

  1006 %

  1007 \endisadelimnoproof

  1008 %

  1009 \isadelimproof

  1010 \ \ %

  1011 \endisadelimproof

  1012 %

  1013 \isatagproof

  1014 \isacommand{next}\isamarkupfalse%

  1015 \isanewline

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

  1017 \ B\isanewline

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

  1019 \ \isacommand{show}\isamarkupfalse%

  1020 \ C%

  1021 \endisatagproof

  1022 {\isafoldproof}%

  1023 %

  1024 \isadelimproof

  1025 %

  1026 \endisadelimproof

  1027 %

  1028 \isadelimnoproof

  1029 \ %

  1030 \endisadelimnoproof

  1031 %

  1032 \isatagnoproof

  1033 \isacommand{sorry}\isamarkupfalse%

  1034 %

  1035 \endisatagnoproof

  1036 {\isafoldnoproof}%

  1037 %

  1038 \isadelimnoproof

  1039 \isanewline

  1040 %

  1041 \endisadelimnoproof

  1042 %

  1043 \isadelimproof

  1044 \ \ %

  1045 \endisadelimproof

  1046 %

  1047 \isatagproof

  1048 \isacommand{qed}\isamarkupfalse%

  1049 %

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

  1051 \isanewline

  1052 \ \ \isacommand{have}\isamarkupfalse%

  1053 \ A\ \isakeyword{and}\ B%

  1054 \endisatagproof

  1055 {\isafoldproof}%

  1056 %

  1057 \isadelimproof

  1058 %

  1059 \endisadelimproof

  1060 %

  1061 \isadelimnoproof

  1062 \ %

  1063 \endisadelimnoproof

  1064 %

  1065 \isatagnoproof

  1066 \isacommand{sorry}\isamarkupfalse%

  1067 %

  1068 \endisatagnoproof

  1069 {\isafoldnoproof}%

  1070 %

  1071 \isadelimnoproof

  1072 \isanewline

  1073 %

  1074 \endisadelimnoproof

  1075 %

  1076 \isadelimproof

  1077 \ \ %

  1078 \endisadelimproof

  1079 %

  1080 \isatagproof

  1081 \isacommand{then}\isamarkupfalse%

  1082 \ \isacommand{have}\isamarkupfalse%

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

  1084 %

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

  1086 \isanewline

  1087 \ \ \isacommand{have}\isamarkupfalse%

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

  1089 \endisatagproof

  1090 {\isafoldproof}%

  1091 %

  1092 \isadelimproof

  1093 %

  1094 \endisadelimproof

  1095 %

  1096 \isadelimnoproof

  1097 \ %

  1098 \endisadelimnoproof

  1099 %

  1100 \isatagnoproof

  1101 \isacommand{sorry}\isamarkupfalse%

  1102 %

  1103 \endisatagnoproof

  1104 {\isafoldnoproof}%

  1105 %

  1106 \isadelimnoproof

  1107 \isanewline

  1108 %

  1109 \endisadelimnoproof

  1110 %

  1111 \isadelimproof

  1112 \ \ %

  1113 \endisadelimproof

  1114 %

  1115 \isatagproof

  1116 \isacommand{then}\isamarkupfalse%

  1117 \ \isacommand{obtain}\isamarkupfalse%

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

  1119 %

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

  1121 \isanewline

  1122 \ \ \isacommand{have}\isamarkupfalse%

  1123 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C626F74746F6D3E}{\isasymbottom}}{\isaliteral{22}{\isachardoublequoteclose}}%

  1124 \endisatagproof

  1125 {\isafoldproof}%

  1126 %

  1127 \isadelimproof

  1128 %

  1129 \endisadelimproof

  1130 %

  1131 \isadelimnoproof

  1132 \ %

  1133 \endisadelimnoproof

  1134 %

  1135 \isatagnoproof

  1136 \isacommand{sorry}\isamarkupfalse%

  1137 %

  1138 \endisatagnoproof

  1139 {\isafoldnoproof}%

  1140 %

  1141 \isadelimnoproof

  1142 \isanewline

  1143 %

  1144 \endisadelimnoproof

  1145 %

  1146 \isadelimproof

  1147 \ \ %

  1148 \endisadelimproof

  1149 %

  1150 \isatagproof

  1151 \isacommand{then}\isamarkupfalse%

  1152 \ \isacommand{have}\isamarkupfalse%

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

  1154 %

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

  1156 \isanewline

  1157 \ \ \isacommand{have}\isamarkupfalse%

  1158 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C746F703E}{\isasymtop}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%

  1159 %

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

  1161 \isanewline

  1162 \ \ \isacommand{have}\isamarkupfalse%

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

  1164 \ \ \isacommand{proof}\isamarkupfalse%

  1165 \isanewline

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

  1167 \ A\isanewline

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

  1169 \ \isacommand{show}\isamarkupfalse%

  1170 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C626F74746F6D3E}{\isasymbottom}}{\isaliteral{22}{\isachardoublequoteclose}}%

  1171 \endisatagproof

  1172 {\isafoldproof}%

  1173 %

  1174 \isadelimproof

  1175 %

  1176 \endisadelimproof

  1177 %

  1178 \isadelimnoproof

  1179 \ %

  1180 \endisadelimnoproof

  1181 %

  1182 \isatagnoproof

  1183 \isacommand{sorry}\isamarkupfalse%

  1184 %

  1185 \endisatagnoproof

  1186 {\isafoldnoproof}%

  1187 %

  1188 \isadelimnoproof

  1189 \isanewline

  1190 %

  1191 \endisadelimnoproof

  1192 %

  1193 \isadelimproof

  1194 \ \ %

  1195 \endisadelimproof

  1196 %

  1197 \isatagproof

  1198 \isacommand{qed}\isamarkupfalse%

  1199 %

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

  1201 \isanewline

  1202 \ \ \isacommand{have}\isamarkupfalse%

  1203 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ A%

  1204 \endisatagproof

  1205 {\isafoldproof}%

  1206 %

  1207 \isadelimproof

  1208 %

  1209 \endisadelimproof

  1210 %

  1211 \isadelimnoproof

  1212 \ %

  1213 \endisadelimnoproof

  1214 %

  1215 \isatagnoproof

  1216 \isacommand{sorry}\isamarkupfalse%

  1217 %

  1218 \endisatagnoproof

  1219 {\isafoldnoproof}%

  1220 %

  1221 \isadelimnoproof

  1222 \isanewline

  1223 %

  1224 \endisadelimnoproof

  1225 %

  1226 \isadelimproof

  1227 \ \ %

  1228 \endisadelimproof

  1229 %

  1230 \isatagproof

  1231 \isacommand{then}\isamarkupfalse%

  1232 \ \isacommand{have}\isamarkupfalse%

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

  1234 %

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

  1236 \isanewline

  1237 \ \ \isacommand{have}\isamarkupfalse%

  1238 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ B\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  1239 \ \ \isacommand{proof}\isamarkupfalse%

  1240 \isanewline

  1241 \ \ \ \ \isacommand{fix}\isamarkupfalse%

  1242 \ x\isanewline

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

  1244 \ {\isaliteral{22}{\isachardoublequoteopen}}B\ x{\isaliteral{22}{\isachardoublequoteclose}}%

  1245 \endisatagproof

  1246 {\isafoldproof}%

  1247 %

  1248 \isadelimproof

  1249 %

  1250 \endisadelimproof

  1251 %

  1252 \isadelimnoproof

  1253 \ %

  1254 \endisadelimnoproof

  1255 %

  1256 \isatagnoproof

  1257 \isacommand{sorry}\isamarkupfalse%

  1258 %

  1259 \endisatagnoproof

  1260 {\isafoldnoproof}%

  1261 %

  1262 \isadelimnoproof

  1263 \isanewline

  1264 %

  1265 \endisadelimnoproof

  1266 %

  1267 \isadelimproof

  1268 \ \ %

  1269 \endisadelimproof

  1270 %

  1271 \isatagproof

  1272 \isacommand{qed}\isamarkupfalse%

  1273 %

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

  1275 \isanewline

  1276 \ \ \isacommand{have}\isamarkupfalse%

  1277 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ B\ x{\isaliteral{22}{\isachardoublequoteclose}}%

  1278 \endisatagproof

  1279 {\isafoldproof}%

  1280 %

  1281 \isadelimproof

  1282 %

  1283 \endisadelimproof

  1284 %

  1285 \isadelimnoproof

  1286 \ %

  1287 \endisadelimnoproof

  1288 %

  1289 \isatagnoproof

  1290 \isacommand{sorry}\isamarkupfalse%

  1291 %

  1292 \endisatagnoproof

  1293 {\isafoldnoproof}%

  1294 %

  1295 \isadelimnoproof

  1296 \isanewline

  1297 %

  1298 \endisadelimnoproof

  1299 %

  1300 \isadelimproof

  1301 \ \ %

  1302 \endisadelimproof

  1303 %

  1304 \isatagproof

  1305 \isacommand{then}\isamarkupfalse%

  1306 \ \isacommand{have}\isamarkupfalse%

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

  1308 %

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

  1310 \isanewline

  1311 \ \ \isacommand{have}\isamarkupfalse%

  1312 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ B\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  1313 \ \ \isacommand{proof}\isamarkupfalse%

  1314 \isanewline

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

  1316 \ {\isaliteral{22}{\isachardoublequoteopen}}B\ a{\isaliteral{22}{\isachardoublequoteclose}}%

  1317 \endisatagproof

  1318 {\isafoldproof}%

  1319 %

  1320 \isadelimproof

  1321 %

  1322 \endisadelimproof

  1323 %

  1324 \isadelimnoproof

  1325 \ %

  1326 \endisadelimnoproof

  1327 %

  1328 \isatagnoproof

  1329 \isacommand{sorry}\isamarkupfalse%

  1330 %

  1331 \endisatagnoproof

  1332 {\isafoldnoproof}%

  1333 %

  1334 \isadelimnoproof

  1335 \isanewline

  1336 %

  1337 \endisadelimnoproof

  1338 %

  1339 \isadelimproof

  1340 \ \ %

  1341 \endisadelimproof

  1342 %

  1343 \isatagproof

  1344 \isacommand{qed}\isamarkupfalse%

  1345 %

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

  1347 \isanewline

  1348 \ \ \isacommand{have}\isamarkupfalse%

  1349 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ B\ x{\isaliteral{22}{\isachardoublequoteclose}}%

  1350 \endisatagproof

  1351 {\isafoldproof}%

  1352 %

  1353 \isadelimproof

  1354 %

  1355 \endisadelimproof

  1356 %

  1357 \isadelimnoproof

  1358 \ %

  1359 \endisadelimnoproof

  1360 %

  1361 \isatagnoproof

  1362 \isacommand{sorry}\isamarkupfalse%

  1363 %

  1364 \endisatagnoproof

  1365 {\isafoldnoproof}%

  1366 %

  1367 \isadelimnoproof

  1368 \isanewline

  1369 %

  1370 \endisadelimnoproof

  1371 %

  1372 \isadelimproof

  1373 \ \ %

  1374 \endisadelimproof

  1375 %

  1376 \isatagproof

  1377 \isacommand{then}\isamarkupfalse%

  1378 \ \isacommand{obtain}\isamarkupfalse%

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

  1380 %

  1381 \end{minipage}

  1382 %

  1383 \endisatagproof

  1384 {\isafoldproof}%

  1385 %

  1386 \isadelimproof

  1387 %

  1388 \endisadelimproof

  1389 %

  1390 \begin{isamarkuptext}%

  1391 \bigskip\noindent Of course, these proofs are merely examples.  As

  1392   sketched in \secref{sec:framework-subproof}, there is a fair amount

  1393   of flexibility in expressing Pure deductions in Isar.  Here the user

  1394   is asked to express himself adequately, aiming at proof texts of

  1395   literary quality.%

  1396 \end{isamarkuptext}%

  1397 \isamarkuptrue%

  1398 %

  1399 \isadelimvisible

  1400 %

  1401 \endisadelimvisible

  1402 %

  1403 \isatagvisible

  1404 \isacommand{end}\isamarkupfalse%

  1405 %

  1406 \endisatagvisible

  1407 {\isafoldvisible}%

  1408 %

  1409 \isadelimvisible

  1410 %

  1411 \endisadelimvisible

  1412 \isanewline

  1413 \end{isabellebody}%

  1414 %%% Local Variables:

  1415 %%% mode: latex

  1416 %%% TeX-master: "root"

  1417 %%% End:

author	wenzelm
	Mon, 03 Oct 2011 11:14:19 +0200
changeset 45988	a45121ffcfcb
parent 43522	e3fdb7c96be5
permissions	-rw-r--r--