doc-src/IsarRef/Thy/document/First_Order_Logic.tex
author wenzelm
Fri Oct 29 11:49:56 2010 +0200 (2010-10-29)
changeset 40255 9ffbc25e1606
parent 29740 6f8f94ccaaaf
child 40406 313a24b66a8d
permissions -rw-r--r--
eliminated obsolete \_ escapes in rail environments;
wenzelm@29731
     1
%
wenzelm@29731
     2
\begin{isabellebody}%
wenzelm@29731
     3
\def\isabellecontext{First{\isacharunderscore}Order{\isacharunderscore}Logic}%
wenzelm@29731
     4
%
wenzelm@29731
     5
\isamarkupheader{Example: First-Order Logic%
wenzelm@29731
     6
}
wenzelm@29731
     7
\isamarkuptrue%
wenzelm@29731
     8
%
wenzelm@29731
     9
\isadelimvisible
wenzelm@29731
    10
%
wenzelm@29731
    11
\endisadelimvisible
wenzelm@29731
    12
%
wenzelm@29731
    13
\isatagvisible
wenzelm@29731
    14
\isacommand{theory}\isamarkupfalse%
wenzelm@29731
    15
\ First{\isacharunderscore}Order{\isacharunderscore}Logic\isanewline
wenzelm@29731
    16
\isakeyword{imports}\ Pure\isanewline
wenzelm@29731
    17
\isakeyword{begin}%
wenzelm@29731
    18
\endisatagvisible
wenzelm@29731
    19
{\isafoldvisible}%
wenzelm@29731
    20
%
wenzelm@29731
    21
\isadelimvisible
wenzelm@29731
    22
%
wenzelm@29731
    23
\endisadelimvisible
wenzelm@29731
    24
%
wenzelm@29731
    25
\begin{isamarkuptext}%
wenzelm@29740
    26
\noindent In order to commence a new object-logic within
wenzelm@29740
    27
  Isabelle/Pure we introduce abstract syntactic categories \isa{{\isachardoublequote}i{\isachardoublequote}}
wenzelm@29740
    28
  for individuals and \isa{{\isachardoublequote}o{\isachardoublequote}} for object-propositions.  The latter
wenzelm@29740
    29
  is embedded into the language of Pure propositions by means of a
wenzelm@29740
    30
  separate judgment.%
wenzelm@29731
    31
\end{isamarkuptext}%
wenzelm@29731
    32
\isamarkuptrue%
wenzelm@29731
    33
\isacommand{typedecl}\isamarkupfalse%
wenzelm@29731
    34
\ i\isanewline
wenzelm@29731
    35
\isacommand{typedecl}\isamarkupfalse%
wenzelm@29731
    36
\ o\isanewline
wenzelm@29731
    37
\isanewline
wenzelm@29731
    38
\isacommand{judgment}\isamarkupfalse%
wenzelm@29731
    39
\isanewline
wenzelm@29731
    40
\ \ Trueprop\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}o\ {\isasymRightarrow}\ prop{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharunderscore}{\isachardoublequoteclose}\ {\isadigit{5}}{\isacharparenright}%
wenzelm@29731
    41
\begin{isamarkuptext}%
wenzelm@29731
    42
\noindent Note that the object-logic judgement is implicit in the
wenzelm@29731
    43
  syntax: writing \isa{A} produces \isa{{\isachardoublequote}Trueprop\ A{\isachardoublequote}} internally.
wenzelm@29731
    44
  From the Pure perspective this means ``\isa{A} is derivable in the
wenzelm@29731
    45
  object-logic''.%
wenzelm@29731
    46
\end{isamarkuptext}%
wenzelm@29731
    47
\isamarkuptrue%
wenzelm@29731
    48
%
wenzelm@29731
    49
\isamarkupsubsection{Equational reasoning \label{sec:framework-ex-equal}%
wenzelm@29731
    50
}
wenzelm@29731
    51
\isamarkuptrue%
wenzelm@29731
    52
%
wenzelm@29731
    53
\begin{isamarkuptext}%
wenzelm@29731
    54
Equality is axiomatized as a binary predicate on individuals, with
wenzelm@29731
    55
  reflexivity as introduction, and substitution as elimination
wenzelm@29731
    56
  principle.  Note that the latter is particularly convenient in a
wenzelm@29731
    57
  framework like Isabelle, because syntactic congruences are
wenzelm@29731
    58
  implicitly produced by unification of \isa{{\isachardoublequote}B\ x{\isachardoublequote}} against
wenzelm@29731
    59
  expressions containing occurrences of \isa{x}.%
wenzelm@29731
    60
\end{isamarkuptext}%
wenzelm@29731
    61
\isamarkuptrue%
wenzelm@29731
    62
\isacommand{axiomatization}\isamarkupfalse%
wenzelm@29731
    63
\isanewline
wenzelm@29731
    64
\ \ equal\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ o{\isachardoublequoteclose}\ \ {\isacharparenleft}\isakeyword{infix}\ {\isachardoublequoteopen}{\isacharequal}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\isanewline
wenzelm@29731
    65
\isakeyword{where}\isanewline
wenzelm@29731
    66
\ \ refl\ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
wenzelm@29731
    67
\ \ subst\ {\isacharbrackleft}elim{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isacharequal}\ y\ {\isasymLongrightarrow}\ B\ x\ {\isasymLongrightarrow}\ B\ y{\isachardoublequoteclose}%
wenzelm@29731
    68
\begin{isamarkuptext}%
wenzelm@29731
    69
\noindent Substitution is very powerful, but also hard to control in
wenzelm@29731
    70
  full generality.  We derive some common symmetry~/ transitivity
wenzelm@29731
    71
  schemes of as particular consequences.%
wenzelm@29731
    72
\end{isamarkuptext}%
wenzelm@29731
    73
\isamarkuptrue%
wenzelm@29731
    74
\isacommand{theorem}\isamarkupfalse%
wenzelm@29731
    75
\ sym\ {\isacharbrackleft}sym{\isacharbrackright}{\isacharcolon}\isanewline
wenzelm@29731
    76
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}x\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline
wenzelm@29731
    77
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}y\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
wenzelm@29731
    78
%
wenzelm@29731
    79
\isadelimproof
wenzelm@29731
    80
%
wenzelm@29731
    81
\endisadelimproof
wenzelm@29731
    82
%
wenzelm@29731
    83
\isatagproof
wenzelm@29731
    84
\isacommand{proof}\isamarkupfalse%
wenzelm@29731
    85
\ {\isacharminus}\isanewline
wenzelm@29731
    86
\ \ \isacommand{have}\isamarkupfalse%
wenzelm@29731
    87
\ {\isachardoublequoteopen}x\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
wenzelm@29731
    88
\isanewline
wenzelm@29731
    89
\ \ \isacommand{with}\isamarkupfalse%
wenzelm@29731
    90
\ {\isacharbackquoteopen}x\ {\isacharequal}\ y{\isacharbackquoteclose}\ \isacommand{show}\isamarkupfalse%
wenzelm@29731
    91
\ {\isachardoublequoteopen}y\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
wenzelm@29731
    92
\isanewline
wenzelm@29731
    93
\isacommand{qed}\isamarkupfalse%
wenzelm@29731
    94
%
wenzelm@29731
    95
\endisatagproof
wenzelm@29731
    96
{\isafoldproof}%
wenzelm@29731
    97
%
wenzelm@29731
    98
\isadelimproof
wenzelm@29731
    99
\isanewline
wenzelm@29731
   100
%
wenzelm@29731
   101
\endisadelimproof
wenzelm@29731
   102
\isanewline
wenzelm@29731
   103
\isacommand{theorem}\isamarkupfalse%
wenzelm@29731
   104
\ forw{\isacharunderscore}subst\ {\isacharbrackleft}trans{\isacharbrackright}{\isacharcolon}\isanewline
wenzelm@29731
   105
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}y\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}B\ x{\isachardoublequoteclose}\isanewline
wenzelm@29731
   106
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}B\ y{\isachardoublequoteclose}\isanewline
wenzelm@29731
   107
%
wenzelm@29731
   108
\isadelimproof
wenzelm@29731
   109
%
wenzelm@29731
   110
\endisadelimproof
wenzelm@29731
   111
%
wenzelm@29731
   112
\isatagproof
wenzelm@29731
   113
\isacommand{proof}\isamarkupfalse%
wenzelm@29731
   114
\ {\isacharminus}\isanewline
wenzelm@29731
   115
\ \ \isacommand{from}\isamarkupfalse%
wenzelm@29731
   116
\ {\isacharbackquoteopen}y\ {\isacharequal}\ x{\isacharbackquoteclose}\ \isacommand{have}\isamarkupfalse%
wenzelm@29731
   117
\ {\isachardoublequoteopen}x\ {\isacharequal}\ y{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
wenzelm@29731
   118
\isanewline
wenzelm@29731
   119
\ \ \isacommand{from}\isamarkupfalse%
wenzelm@29731
   120
\ this\ \isakeyword{and}\ {\isacharbackquoteopen}B\ x{\isacharbackquoteclose}\ \isacommand{show}\isamarkupfalse%
wenzelm@29731
   121
\ {\isachardoublequoteopen}B\ y{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
wenzelm@29731
   122
\isanewline
wenzelm@29731
   123
\isacommand{qed}\isamarkupfalse%
wenzelm@29731
   124
%
wenzelm@29731
   125
\endisatagproof
wenzelm@29731
   126
{\isafoldproof}%
wenzelm@29731
   127
%
wenzelm@29731
   128
\isadelimproof
wenzelm@29731
   129
\isanewline
wenzelm@29731
   130
%
wenzelm@29731
   131
\endisadelimproof
wenzelm@29731
   132
\isanewline
wenzelm@29731
   133
\isacommand{theorem}\isamarkupfalse%
wenzelm@29731
   134
\ back{\isacharunderscore}subst\ {\isacharbrackleft}trans{\isacharbrackright}{\isacharcolon}\isanewline
wenzelm@29731
   135
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}B\ x{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}x\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline
wenzelm@29731
   136
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}B\ y{\isachardoublequoteclose}\isanewline
wenzelm@29731
   137
%
wenzelm@29731
   138
\isadelimproof
wenzelm@29731
   139
%
wenzelm@29731
   140
\endisadelimproof
wenzelm@29731
   141
%
wenzelm@29731
   142
\isatagproof
wenzelm@29731
   143
\isacommand{proof}\isamarkupfalse%
wenzelm@29731
   144
\ {\isacharminus}\isanewline
wenzelm@29731
   145
\ \ \isacommand{from}\isamarkupfalse%
wenzelm@29731
   146
\ {\isacharbackquoteopen}x\ {\isacharequal}\ y{\isacharbackquoteclose}\ \isakeyword{and}\ {\isacharbackquoteopen}B\ x{\isacharbackquoteclose}\isanewline
wenzelm@29731
   147
\ \ \isacommand{show}\isamarkupfalse%
wenzelm@29731
   148
\ {\isachardoublequoteopen}B\ y{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
wenzelm@29731
   149
\isanewline
wenzelm@29731
   150
\isacommand{qed}\isamarkupfalse%
wenzelm@29731
   151
%
wenzelm@29731
   152
\endisatagproof
wenzelm@29731
   153
{\isafoldproof}%
wenzelm@29731
   154
%
wenzelm@29731
   155
\isadelimproof
wenzelm@29731
   156
\isanewline
wenzelm@29731
   157
%
wenzelm@29731
   158
\endisadelimproof
wenzelm@29731
   159
\isanewline
wenzelm@29731
   160
\isacommand{theorem}\isamarkupfalse%
wenzelm@29731
   161
\ trans\ {\isacharbrackleft}trans{\isacharbrackright}{\isacharcolon}\isanewline
wenzelm@29731
   162
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}x\ {\isacharequal}\ y{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline
wenzelm@29731
   163
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}x\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline
wenzelm@29731
   164
%
wenzelm@29731
   165
\isadelimproof
wenzelm@29731
   166
%
wenzelm@29731
   167
\endisadelimproof
wenzelm@29731
   168
%
wenzelm@29731
   169
\isatagproof
wenzelm@29731
   170
\isacommand{proof}\isamarkupfalse%
wenzelm@29731
   171
\ {\isacharminus}\isanewline
wenzelm@29731
   172
\ \ \isacommand{from}\isamarkupfalse%
wenzelm@29731
   173
\ {\isacharbackquoteopen}y\ {\isacharequal}\ z{\isacharbackquoteclose}\ \isakeyword{and}\ {\isacharbackquoteopen}x\ {\isacharequal}\ y{\isacharbackquoteclose}\isanewline
wenzelm@29731
   174
\ \ \isacommand{show}\isamarkupfalse%
wenzelm@29731
   175
\ {\isachardoublequoteopen}x\ {\isacharequal}\ z{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
wenzelm@29731
   176
\isanewline
wenzelm@29731
   177
\isacommand{qed}\isamarkupfalse%
wenzelm@29731
   178
%
wenzelm@29731
   179
\endisatagproof
wenzelm@29731
   180
{\isafoldproof}%
wenzelm@29731
   181
%
wenzelm@29731
   182
\isadelimproof
wenzelm@29731
   183
%
wenzelm@29731
   184
\endisadelimproof
wenzelm@29731
   185
%
wenzelm@29731
   186
\isamarkupsubsection{Basic group theory%
wenzelm@29731
   187
}
wenzelm@29731
   188
\isamarkuptrue%
wenzelm@29731
   189
%
wenzelm@29731
   190
\begin{isamarkuptext}%
wenzelm@29731
   191
As an example for equational reasoning we consider some bits of
wenzelm@29731
   192
  group theory.  The subsequent locale definition postulates group
wenzelm@29731
   193
  operations and axioms; we also derive some consequences of this
wenzelm@29731
   194
  specification.%
wenzelm@29731
   195
\end{isamarkuptext}%
wenzelm@29731
   196
\isamarkuptrue%
wenzelm@29731
   197
\isacommand{locale}\isamarkupfalse%
wenzelm@29731
   198
\ group\ {\isacharequal}\isanewline
wenzelm@29731
   199
\ \ \isakeyword{fixes}\ prod\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ i{\isachardoublequoteclose}\ \ {\isacharparenleft}\isakeyword{infix}\ {\isachardoublequoteopen}{\isasymcirc}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
wenzelm@29731
   200
\ \ \ \ \isakeyword{and}\ inv\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}i\ {\isasymRightarrow}\ i{\isachardoublequoteclose}\ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharparenleft}{\isacharunderscore}{\isasyminverse}{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline
wenzelm@29731
   201
\ \ \ \ \isakeyword{and}\ unit\ {\isacharcolon}{\isacharcolon}\ i\ \ {\isacharparenleft}{\isachardoublequoteopen}{\isadigit{1}}{\isachardoublequoteclose}{\isacharparenright}\isanewline
wenzelm@29731
   202
\ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymcirc}\ y{\isacharparenright}\ {\isasymcirc}\ z\ {\isacharequal}\ x\ {\isasymcirc}\ {\isacharparenleft}y\ {\isasymcirc}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline
wenzelm@29731
   203
\ \ \ \ \isakeyword{and}\ left{\isacharunderscore}unit{\isacharcolon}\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isasymcirc}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
wenzelm@29731
   204
\ \ \ \ \isakeyword{and}\ left{\isacharunderscore}inv{\isacharcolon}\ {\isachardoublequoteopen}x{\isasyminverse}\ {\isasymcirc}\ x\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
wenzelm@29731
   205
\isakeyword{begin}\isanewline
wenzelm@29731
   206
\isanewline
wenzelm@29731
   207
\isacommand{theorem}\isamarkupfalse%
wenzelm@29731
   208
\ right{\isacharunderscore}inv{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymcirc}\ x{\isasyminverse}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
wenzelm@29731
   209
%
wenzelm@29731
   210
\isadelimproof
wenzelm@29731
   211
%
wenzelm@29731
   212
\endisadelimproof
wenzelm@29731
   213
%
wenzelm@29731
   214
\isatagproof
wenzelm@29731
   215
\isacommand{proof}\isamarkupfalse%
wenzelm@29731
   216
\ {\isacharminus}\isanewline
wenzelm@29731
   217
\ \ \isacommand{have}\isamarkupfalse%
wenzelm@29731
   218
\ {\isachardoublequoteopen}x\ {\isasymcirc}\ x{\isasyminverse}\ {\isacharequal}\ {\isadigit{1}}\ {\isasymcirc}\ {\isacharparenleft}x\ {\isasymcirc}\ x{\isasyminverse}{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
wenzelm@29731
   219
\ {\isacharparenleft}rule\ left{\isacharunderscore}unit\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isacharparenright}\isanewline
wenzelm@29731
   220
\ \ \isacommand{also}\isamarkupfalse%
wenzelm@29731
   221
\ \isacommand{have}\isamarkupfalse%
wenzelm@29731
   222
\ {\isachardoublequoteopen}{\isasymdots}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{1}}\ {\isasymcirc}\ x{\isacharparenright}\ {\isasymcirc}\ x{\isasyminverse}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
wenzelm@29731
   223
\ {\isacharparenleft}rule\ assoc\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isacharparenright}\isanewline
wenzelm@29731
   224
\ \ \isacommand{also}\isamarkupfalse%
wenzelm@29731
   225
\ \isacommand{have}\isamarkupfalse%
wenzelm@29731
   226
\ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminverse}{\isacharparenright}{\isasyminverse}\ {\isasymcirc}\ x{\isasyminverse}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
wenzelm@29731
   227
\ {\isacharparenleft}rule\ left{\isacharunderscore}inv\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isacharparenright}\isanewline
wenzelm@29731
   228
\ \ \isacommand{also}\isamarkupfalse%
wenzelm@29731
   229
\ \isacommand{have}\isamarkupfalse%
wenzelm@29731
   230
\ {\isachardoublequoteopen}{\isasymdots}\ {\isasymcirc}\ x\ {\isacharequal}\ {\isacharparenleft}x{\isasyminverse}{\isacharparenright}{\isasyminverse}\ {\isasymcirc}\ {\isacharparenleft}x{\isasyminverse}\ {\isasymcirc}\ x{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
wenzelm@29731
   231
\ {\isacharparenleft}rule\ assoc{\isacharparenright}\isanewline
wenzelm@29731
   232
\ \ \isacommand{also}\isamarkupfalse%
wenzelm@29731
   233
\ \isacommand{have}\isamarkupfalse%
wenzelm@29731
   234
\ {\isachardoublequoteopen}x{\isasyminverse}\ {\isasymcirc}\ x\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
wenzelm@29731
   235
\ {\isacharparenleft}rule\ left{\isacharunderscore}inv{\isacharparenright}\isanewline
wenzelm@29731
   236
\ \ \isacommand{also}\isamarkupfalse%
wenzelm@29731
   237
\ \isacommand{have}\isamarkupfalse%
wenzelm@29731
   238
\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharparenleft}x{\isasyminverse}{\isacharparenright}{\isasyminverse}\ {\isasymcirc}\ {\isasymdots}{\isacharparenright}\ {\isasymcirc}\ x{\isasyminverse}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminverse}{\isacharparenright}{\isasyminverse}\ {\isasymcirc}\ {\isacharparenleft}{\isadigit{1}}\ {\isasymcirc}\ x{\isasyminverse}{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
wenzelm@29731
   239
\ {\isacharparenleft}rule\ assoc{\isacharparenright}\isanewline
wenzelm@29731
   240
\ \ \isacommand{also}\isamarkupfalse%
wenzelm@29731
   241
\ \isacommand{have}\isamarkupfalse%
wenzelm@29731
   242
\ {\isachardoublequoteopen}{\isadigit{1}}\ {\isasymcirc}\ x{\isasyminverse}\ {\isacharequal}\ x{\isasyminverse}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
wenzelm@29731
   243
\ {\isacharparenleft}rule\ left{\isacharunderscore}unit{\isacharparenright}\isanewline
wenzelm@29731
   244
\ \ \isacommand{also}\isamarkupfalse%
wenzelm@29731
   245
\ \isacommand{have}\isamarkupfalse%
wenzelm@29731
   246
\ {\isachardoublequoteopen}{\isacharparenleft}x{\isasyminverse}{\isacharparenright}{\isasyminverse}\ {\isasymcirc}\ {\isasymdots}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
wenzelm@29731
   247
\ {\isacharparenleft}rule\ left{\isacharunderscore}inv{\isacharparenright}\isanewline
wenzelm@29731
   248
\ \ \isacommand{finally}\isamarkupfalse%
wenzelm@29731
   249
\ \isacommand{show}\isamarkupfalse%
wenzelm@29731
   250
\ {\isachardoublequoteopen}x\ {\isasymcirc}\ x{\isasyminverse}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
wenzelm@29731
   251
\isanewline
wenzelm@29731
   252
\isacommand{qed}\isamarkupfalse%
wenzelm@29731
   253
%
wenzelm@29731
   254
\endisatagproof
wenzelm@29731
   255
{\isafoldproof}%
wenzelm@29731
   256
%
wenzelm@29731
   257
\isadelimproof
wenzelm@29731
   258
\isanewline
wenzelm@29731
   259
%
wenzelm@29731
   260
\endisadelimproof
wenzelm@29731
   261
\isanewline
wenzelm@29731
   262
\isacommand{theorem}\isamarkupfalse%
wenzelm@29731
   263
\ right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymcirc}\ {\isadigit{1}}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
wenzelm@29731
   264
%
wenzelm@29731
   265
\isadelimproof
wenzelm@29731
   266
%
wenzelm@29731
   267
\endisadelimproof
wenzelm@29731
   268
%
wenzelm@29731
   269
\isatagproof
wenzelm@29731
   270
\isacommand{proof}\isamarkupfalse%
wenzelm@29731
   271
\ {\isacharminus}\isanewline
wenzelm@29731
   272
\ \ \isacommand{have}\isamarkupfalse%
wenzelm@29731
   273
\ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ x{\isasyminverse}\ {\isasymcirc}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
wenzelm@29731
   274
\ {\isacharparenleft}rule\ left{\isacharunderscore}inv\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isacharparenright}\isanewline
wenzelm@29731
   275
\ \ \isacommand{also}\isamarkupfalse%
wenzelm@29731
   276
\ \isacommand{have}\isamarkupfalse%
wenzelm@29731
   277
\ {\isachardoublequoteopen}x\ {\isasymcirc}\ {\isasymdots}\ {\isacharequal}\ {\isacharparenleft}x\ {\isasymcirc}\ x{\isasyminverse}{\isacharparenright}\ {\isasymcirc}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
wenzelm@29731
   278
\ {\isacharparenleft}rule\ assoc\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isacharparenright}\isanewline
wenzelm@29731
   279
\ \ \isacommand{also}\isamarkupfalse%
wenzelm@29731
   280
\ \isacommand{have}\isamarkupfalse%
wenzelm@29731
   281
\ {\isachardoublequoteopen}x\ {\isasymcirc}\ x{\isasyminverse}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
wenzelm@29731
   282
\ {\isacharparenleft}rule\ right{\isacharunderscore}inv{\isacharparenright}\isanewline
wenzelm@29731
   283
\ \ \isacommand{also}\isamarkupfalse%
wenzelm@29731
   284
\ \isacommand{have}\isamarkupfalse%
wenzelm@29731
   285
\ {\isachardoublequoteopen}{\isasymdots}\ {\isasymcirc}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
wenzelm@29731
   286
\ {\isacharparenleft}rule\ left{\isacharunderscore}unit{\isacharparenright}\isanewline
wenzelm@29731
   287
\ \ \isacommand{finally}\isamarkupfalse%
wenzelm@29731
   288
\ \isacommand{show}\isamarkupfalse%
wenzelm@29731
   289
\ {\isachardoublequoteopen}x\ {\isasymcirc}\ {\isadigit{1}}\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
wenzelm@29731
   290
\isanewline
wenzelm@29731
   291
\isacommand{qed}\isamarkupfalse%
wenzelm@29731
   292
%
wenzelm@29731
   293
\endisatagproof
wenzelm@29731
   294
{\isafoldproof}%
wenzelm@29731
   295
%
wenzelm@29731
   296
\isadelimproof
wenzelm@29731
   297
%
wenzelm@29731
   298
\endisadelimproof
wenzelm@29731
   299
%
wenzelm@29731
   300
\begin{isamarkuptext}%
wenzelm@29740
   301
\noindent Reasoning from basic axioms is often tedious.  Our proofs
wenzelm@29740
   302
  work by producing various instances of the given rules (potentially
wenzelm@29740
   303
  the symmetric form) using the pattern ``\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}~\isa{eq}~\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isachardoublequote}{\isacharparenleft}rule\ r{\isacharparenright}{\isachardoublequote}}'' and composing the chain of
wenzelm@29731
   304
  results via \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}}/\hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}}.  These steps may
wenzelm@29731
   305
  involve any of the transitivity rules declared in
wenzelm@29731
   306
  \secref{sec:framework-ex-equal}, namely \isa{trans} in combining
wenzelm@29731
   307
  the first two results in \isa{right{\isacharunderscore}inv} and in the final steps of
wenzelm@29731
   308
  both proofs, \isa{forw{\isacharunderscore}subst} in the first combination of \isa{right{\isacharunderscore}unit}, and \isa{back{\isacharunderscore}subst} in all other calculational steps.
wenzelm@29731
   309
wenzelm@29731
   310
  Occasional substitutions in calculations are adequate, but should
wenzelm@29731
   311
  not be over-emphasized.  The other extreme is to compose a chain by
wenzelm@29731
   312
  plain transitivity only, with replacements occurring always in
wenzelm@29731
   313
  topmost position. For example:%
wenzelm@29731
   314
\end{isamarkuptext}%
wenzelm@29731
   315
\isamarkuptrue%
wenzelm@29731
   316
%
wenzelm@29731
   317
\isadelimproof
wenzelm@29731
   318
%
wenzelm@29731
   319
\endisadelimproof
wenzelm@29731
   320
%
wenzelm@29731
   321
\isatagproof
wenzelm@29731
   322
\ \ \isacommand{have}\isamarkupfalse%
wenzelm@29731
   323
\ {\isachardoublequoteopen}x\ {\isasymcirc}\ {\isadigit{1}}\ {\isacharequal}\ x\ {\isasymcirc}\ {\isacharparenleft}x{\isasyminverse}\ {\isasymcirc}\ x{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
wenzelm@29731
   324
\ left{\isacharunderscore}inv\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
wenzelm@29731
   325
\isanewline
wenzelm@29731
   326
\ \ \isacommand{also}\isamarkupfalse%
wenzelm@29731
   327
\ \isacommand{have}\isamarkupfalse%
wenzelm@29731
   328
\ {\isachardoublequoteopen}{\isasymdots}\ {\isacharequal}\ {\isacharparenleft}x\ {\isasymcirc}\ x{\isasyminverse}{\isacharparenright}\ {\isasymcirc}\ x{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
wenzelm@29731
   329
\ assoc\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
wenzelm@29731
   330
\isanewline
wenzelm@29731
   331
\ \ \isacommand{also}\isamarkupfalse%
wenzelm@29731
   332
\ \isacommand{have}\isamarkupfalse%
wenzelm@29731
   333
\ {\isachardoublequoteopen}{\isasymdots}\ {\isacharequal}\ {\isadigit{1}}\ {\isasymcirc}\ x{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
wenzelm@29731
   334
\ right{\isacharunderscore}inv\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
wenzelm@29731
   335
\isanewline
wenzelm@29731
   336
\ \ \isacommand{also}\isamarkupfalse%
wenzelm@29731
   337
\ \isacommand{have}\isamarkupfalse%
wenzelm@29731
   338
\ {\isachardoublequoteopen}{\isasymdots}\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
wenzelm@29731
   339
\ left{\isacharunderscore}unit\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
wenzelm@29731
   340
\isanewline
wenzelm@29731
   341
\ \ \isacommand{finally}\isamarkupfalse%
wenzelm@29731
   342
\ \isacommand{have}\isamarkupfalse%
wenzelm@29731
   343
\ {\isachardoublequoteopen}x\ {\isasymcirc}\ {\isadigit{1}}\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
wenzelm@29731
   344
%
wenzelm@29731
   345
\endisatagproof
wenzelm@29731
   346
{\isafoldproof}%
wenzelm@29731
   347
%
wenzelm@29731
   348
\isadelimproof
wenzelm@29731
   349
%
wenzelm@29731
   350
\endisadelimproof
wenzelm@29731
   351
%
wenzelm@29731
   352
\begin{isamarkuptext}%
wenzelm@29731
   353
\noindent Here we have re-used the built-in mechanism for unfolding
wenzelm@29731
   354
  definitions in order to normalize each equational problem.  A more
wenzelm@29731
   355
  realistic object-logic would include proper setup for the Simplifier
wenzelm@29731
   356
  (\secref{sec:simplifier}), the main automated tool for equational
wenzelm@29740
   357
  reasoning in Isabelle.  Then ``\hyperlink{command.unfolding}{\mbox{\isa{\isacommand{unfolding}}}}~\isa{left{\isacharunderscore}inv}~\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}}'' would become ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isachardoublequote}{\isacharparenleft}simp\ only{\isacharcolon}\ left{\isacharunderscore}inv{\isacharparenright}{\isachardoublequote}}'' etc.%
wenzelm@29731
   358
\end{isamarkuptext}%
wenzelm@29731
   359
\isamarkuptrue%
wenzelm@29731
   360
\isacommand{end}\isamarkupfalse%
wenzelm@29731
   361
%
wenzelm@29740
   362
\isamarkupsubsection{Propositional logic \label{sec:framework-ex-prop}%
wenzelm@29731
   363
}
wenzelm@29731
   364
\isamarkuptrue%
wenzelm@29731
   365
%
wenzelm@29731
   366
\begin{isamarkuptext}%
wenzelm@29731
   367
We axiomatize basic connectives of propositional logic: implication,
wenzelm@29731
   368
  disjunction, and conjunction.  The associated rules are modeled
wenzelm@29740
   369
  after Gentzen's system of Natural Deduction \cite{Gentzen:1935}.%
wenzelm@29731
   370
\end{isamarkuptext}%
wenzelm@29731
   371
\isamarkuptrue%
wenzelm@29731
   372
\isacommand{axiomatization}\isamarkupfalse%
wenzelm@29731
   373
\isanewline
wenzelm@29731
   374
\ \ imp\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ o{\isachardoublequoteclose}\ \ {\isacharparenleft}\isakeyword{infixr}\ {\isachardoublequoteopen}{\isasymlongrightarrow}{\isachardoublequoteclose}\ {\isadigit{2}}{\isadigit{5}}{\isacharparenright}\ \isakeyword{where}\isanewline
wenzelm@29731
   375
\ \ impI\ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}A\ {\isasymLongrightarrow}\ B{\isacharparenright}\ {\isasymLongrightarrow}\ A\ {\isasymlongrightarrow}\ B{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
wenzelm@29731
   376
\ \ impD\ {\isacharbrackleft}dest{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}A\ {\isasymlongrightarrow}\ B{\isacharparenright}\ {\isasymLongrightarrow}\ A\ {\isasymLongrightarrow}\ B{\isachardoublequoteclose}\isanewline
wenzelm@29731
   377
\isanewline
wenzelm@29731
   378
\isacommand{axiomatization}\isamarkupfalse%
wenzelm@29731
   379
\isanewline
wenzelm@29731
   380
\ \ disj\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ o{\isachardoublequoteclose}\ \ {\isacharparenleft}\isakeyword{infixr}\ {\isachardoublequoteopen}{\isasymor}{\isachardoublequoteclose}\ {\isadigit{3}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\isanewline
wenzelm@29731
   381
\ \ disjI\isactrlisub {\isadigit{1}}\ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}A\ {\isasymLongrightarrow}\ A\ {\isasymor}\ B{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
wenzelm@29740
   382
\ \ disjI\isactrlisub {\isadigit{2}}\ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}B\ {\isasymLongrightarrow}\ A\ {\isasymor}\ B{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
wenzelm@29740
   383
\ \ disjE\ {\isacharbrackleft}elim{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}A\ {\isasymor}\ B\ {\isasymLongrightarrow}\ {\isacharparenleft}A\ {\isasymLongrightarrow}\ C{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}B\ {\isasymLongrightarrow}\ C{\isacharparenright}\ {\isasymLongrightarrow}\ C{\isachardoublequoteclose}\isanewline
wenzelm@29731
   384
\isanewline
wenzelm@29731
   385
\isacommand{axiomatization}\isamarkupfalse%
wenzelm@29731
   386
\isanewline
wenzelm@29731
   387
\ \ conj\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ o{\isachardoublequoteclose}\ \ {\isacharparenleft}\isakeyword{infixr}\ {\isachardoublequoteopen}{\isasymand}{\isachardoublequoteclose}\ {\isadigit{3}}{\isadigit{5}}{\isacharparenright}\ \isakeyword{where}\isanewline
wenzelm@29731
   388
\ \ conjI\ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}A\ {\isasymLongrightarrow}\ B\ {\isasymLongrightarrow}\ A\ {\isasymand}\ B{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
wenzelm@29740
   389
\ \ conjD\isactrlisub {\isadigit{1}}{\isacharcolon}\ {\isachardoublequoteopen}A\ {\isasymand}\ B\ {\isasymLongrightarrow}\ A{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
wenzelm@29740
   390
\ \ conjD\isactrlisub {\isadigit{2}}{\isacharcolon}\ {\isachardoublequoteopen}A\ {\isasymand}\ B\ {\isasymLongrightarrow}\ B{\isachardoublequoteclose}%
wenzelm@29731
   391
\begin{isamarkuptext}%
wenzelm@29731
   392
\noindent The conjunctive destructions have the disadvantage that
wenzelm@29731
   393
  decomposing \isa{{\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}} involves an immediate decision which
wenzelm@29731
   394
  component should be projected.  The more convenient simultaneous
wenzelm@29731
   395
  elimination \isa{{\isachardoublequote}A\ {\isasymand}\ B\ {\isasymLongrightarrow}\ {\isacharparenleft}A\ {\isasymLongrightarrow}\ B\ {\isasymLongrightarrow}\ C{\isacharparenright}\ {\isasymLongrightarrow}\ C{\isachardoublequote}} can be derived as
wenzelm@29731
   396
  follows:%
wenzelm@29731
   397
\end{isamarkuptext}%
wenzelm@29731
   398
\isamarkuptrue%
wenzelm@29731
   399
\isacommand{theorem}\isamarkupfalse%
wenzelm@29731
   400
\ conjE\ {\isacharbrackleft}elim{\isacharbrackright}{\isacharcolon}\isanewline
wenzelm@29731
   401
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}A\ {\isasymand}\ B{\isachardoublequoteclose}\isanewline
wenzelm@29731
   402
\ \ \isakeyword{obtains}\ A\ \isakeyword{and}\ B\isanewline
wenzelm@29731
   403
%
wenzelm@29731
   404
\isadelimproof
wenzelm@29731
   405
%
wenzelm@29731
   406
\endisadelimproof
wenzelm@29731
   407
%
wenzelm@29731
   408
\isatagproof
wenzelm@29731
   409
\isacommand{proof}\isamarkupfalse%
wenzelm@29731
   410
\isanewline
wenzelm@29731
   411
\ \ \isacommand{from}\isamarkupfalse%
wenzelm@29731
   412
\ {\isacharbackquoteopen}A\ {\isasymand}\ B{\isacharbackquoteclose}\ \isacommand{show}\isamarkupfalse%
wenzelm@29740
   413
\ A\ \isacommand{by}\isamarkupfalse%
wenzelm@29740
   414
\ {\isacharparenleft}rule\ conjD\isactrlisub {\isadigit{1}}{\isacharparenright}\isanewline
wenzelm@29731
   415
\ \ \isacommand{from}\isamarkupfalse%
wenzelm@29731
   416
\ {\isacharbackquoteopen}A\ {\isasymand}\ B{\isacharbackquoteclose}\ \isacommand{show}\isamarkupfalse%
wenzelm@29740
   417
\ B\ \isacommand{by}\isamarkupfalse%
wenzelm@29740
   418
\ {\isacharparenleft}rule\ conjD\isactrlisub {\isadigit{2}}{\isacharparenright}\isanewline
wenzelm@29731
   419
\isacommand{qed}\isamarkupfalse%
wenzelm@29731
   420
%
wenzelm@29731
   421
\endisatagproof
wenzelm@29731
   422
{\isafoldproof}%
wenzelm@29731
   423
%
wenzelm@29731
   424
\isadelimproof
wenzelm@29731
   425
%
wenzelm@29731
   426
\endisadelimproof
wenzelm@29731
   427
%
wenzelm@29731
   428
\begin{isamarkuptext}%
wenzelm@29731
   429
\noindent Here is an example of swapping conjuncts with a single
wenzelm@29731
   430
  intermediate elimination step:%
wenzelm@29731
   431
\end{isamarkuptext}%
wenzelm@29731
   432
\isamarkuptrue%
wenzelm@29731
   433
%
wenzelm@29731
   434
\isadelimproof
wenzelm@29731
   435
%
wenzelm@29731
   436
\endisadelimproof
wenzelm@29731
   437
%
wenzelm@29731
   438
\isatagproof
wenzelm@29731
   439
\ \ \isacommand{assume}\isamarkupfalse%
wenzelm@29731
   440
\ {\isachardoublequoteopen}A\ {\isasymand}\ B{\isachardoublequoteclose}\isanewline
wenzelm@29731
   441
\ \ \isacommand{then}\isamarkupfalse%
wenzelm@29731
   442
\ \isacommand{obtain}\isamarkupfalse%
wenzelm@29731
   443
\ B\ \isakeyword{and}\ A\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
wenzelm@29731
   444
\isanewline
wenzelm@29731
   445
\ \ \isacommand{then}\isamarkupfalse%
wenzelm@29731
   446
\ \isacommand{have}\isamarkupfalse%
wenzelm@29731
   447
\ {\isachardoublequoteopen}B\ {\isasymand}\ A{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
wenzelm@29731
   448
%
wenzelm@29731
   449
\endisatagproof
wenzelm@29731
   450
{\isafoldproof}%
wenzelm@29731
   451
%
wenzelm@29731
   452
\isadelimproof
wenzelm@29731
   453
%
wenzelm@29731
   454
\endisadelimproof
wenzelm@29731
   455
%
wenzelm@29731
   456
\begin{isamarkuptext}%
wenzelm@29740
   457
\noindent Note that the analogous elimination rule for disjunction
wenzelm@29740
   458
  ``\isa{{\isachardoublequote}{\isasymASSUMES}\ A\ {\isasymor}\ B\ {\isasymOBTAINS}\ A\ {\isasymBBAR}\ B{\isachardoublequote}}'' coincides with
wenzelm@29740
   459
  the original axiomatization of \isa{disjE}.
wenzelm@29731
   460
wenzelm@29731
   461
  \medskip We continue propositional logic by introducing absurdity
wenzelm@29731
   462
  with its characteristic elimination.  Plain truth may then be
wenzelm@29731
   463
  defined as a proposition that is trivially true.%
wenzelm@29731
   464
\end{isamarkuptext}%
wenzelm@29731
   465
\isamarkuptrue%
wenzelm@29731
   466
\isacommand{axiomatization}\isamarkupfalse%
wenzelm@29731
   467
\isanewline
wenzelm@29731
   468
\ \ false\ {\isacharcolon}{\isacharcolon}\ o\ \ {\isacharparenleft}{\isachardoublequoteopen}{\isasymbottom}{\isachardoublequoteclose}{\isacharparenright}\ \isakeyword{where}\isanewline
wenzelm@29731
   469
\ \ falseE\ {\isacharbrackleft}elim{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymbottom}\ {\isasymLongrightarrow}\ A{\isachardoublequoteclose}\isanewline
wenzelm@29731
   470
\isanewline
wenzelm@29731
   471
\isacommand{definition}\isamarkupfalse%
wenzelm@29731
   472
\isanewline
wenzelm@29731
   473
\ \ true\ {\isacharcolon}{\isacharcolon}\ o\ \ {\isacharparenleft}{\isachardoublequoteopen}{\isasymtop}{\isachardoublequoteclose}{\isacharparenright}\ \isakeyword{where}\isanewline
wenzelm@29731
   474
\ \ {\isachardoublequoteopen}{\isasymtop}\ {\isasymequiv}\ {\isasymbottom}\ {\isasymlongrightarrow}\ {\isasymbottom}{\isachardoublequoteclose}\isanewline
wenzelm@29731
   475
\isanewline
wenzelm@29731
   476
\isacommand{theorem}\isamarkupfalse%
wenzelm@29731
   477
\ trueI\ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\ {\isasymtop}\isanewline
wenzelm@29731
   478
%
wenzelm@29731
   479
\isadelimproof
wenzelm@29731
   480
\ \ %
wenzelm@29731
   481
\endisadelimproof
wenzelm@29731
   482
%
wenzelm@29731
   483
\isatagproof
wenzelm@29731
   484
\isacommand{unfolding}\isamarkupfalse%
wenzelm@29731
   485
\ true{\isacharunderscore}def\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
wenzelm@29731
   486
%
wenzelm@29731
   487
\endisatagproof
wenzelm@29731
   488
{\isafoldproof}%
wenzelm@29731
   489
%
wenzelm@29731
   490
\isadelimproof
wenzelm@29731
   491
%
wenzelm@29731
   492
\endisadelimproof
wenzelm@29731
   493
%
wenzelm@29731
   494
\begin{isamarkuptext}%
wenzelm@29740
   495
\medskip\noindent Now negation represents an implication towards
wenzelm@29740
   496
  absurdity:%
wenzelm@29731
   497
\end{isamarkuptext}%
wenzelm@29731
   498
\isamarkuptrue%
wenzelm@29731
   499
\isacommand{definition}\isamarkupfalse%
wenzelm@29731
   500
\isanewline
wenzelm@29731
   501
\ \ not\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}o\ {\isasymRightarrow}\ o{\isachardoublequoteclose}\ \ {\isacharparenleft}{\isachardoublequoteopen}{\isasymnot}\ {\isacharunderscore}{\isachardoublequoteclose}\ {\isacharbrackleft}{\isadigit{4}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{4}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\isanewline
wenzelm@29731
   502
\ \ {\isachardoublequoteopen}{\isasymnot}\ A\ {\isasymequiv}\ A\ {\isasymlongrightarrow}\ {\isasymbottom}{\isachardoublequoteclose}\isanewline
wenzelm@29731
   503
\isanewline
wenzelm@29731
   504
\isacommand{theorem}\isamarkupfalse%
wenzelm@29731
   505
\ notI\ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\isanewline
wenzelm@29731
   506
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}A\ {\isasymLongrightarrow}\ {\isasymbottom}{\isachardoublequoteclose}\isanewline
wenzelm@29731
   507
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymnot}\ A{\isachardoublequoteclose}\isanewline
wenzelm@29731
   508
%
wenzelm@29731
   509
\isadelimproof
wenzelm@29731
   510
%
wenzelm@29731
   511
\endisadelimproof
wenzelm@29731
   512
%
wenzelm@29731
   513
\isatagproof
wenzelm@29731
   514
\isacommand{unfolding}\isamarkupfalse%
wenzelm@29731
   515
\ not{\isacharunderscore}def\isanewline
wenzelm@29731
   516
\isacommand{proof}\isamarkupfalse%
wenzelm@29731
   517
\isanewline
wenzelm@29731
   518
\ \ \isacommand{assume}\isamarkupfalse%
wenzelm@29731
   519
\ A\isanewline
wenzelm@29731
   520
\ \ \isacommand{then}\isamarkupfalse%
wenzelm@29731
   521
\ \isacommand{show}\isamarkupfalse%
wenzelm@29731
   522
\ {\isasymbottom}\ \isacommand{by}\isamarkupfalse%
wenzelm@29731
   523
\ {\isacharparenleft}rule\ {\isacharbackquoteopen}A\ {\isasymLongrightarrow}\ {\isasymbottom}{\isacharbackquoteclose}{\isacharparenright}\isanewline
wenzelm@29731
   524
\isacommand{qed}\isamarkupfalse%
wenzelm@29731
   525
%
wenzelm@29731
   526
\endisatagproof
wenzelm@29731
   527
{\isafoldproof}%
wenzelm@29731
   528
%
wenzelm@29731
   529
\isadelimproof
wenzelm@29731
   530
\isanewline
wenzelm@29731
   531
%
wenzelm@29731
   532
\endisadelimproof
wenzelm@29731
   533
\isanewline
wenzelm@29731
   534
\isacommand{theorem}\isamarkupfalse%
wenzelm@29731
   535
\ notE\ {\isacharbrackleft}elim{\isacharbrackright}{\isacharcolon}\isanewline
wenzelm@29731
   536
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymnot}\ A{\isachardoublequoteclose}\ \isakeyword{and}\ A\isanewline
wenzelm@29731
   537
\ \ \isakeyword{shows}\ B\isanewline
wenzelm@29731
   538
%
wenzelm@29731
   539
\isadelimproof
wenzelm@29731
   540
%
wenzelm@29731
   541
\endisadelimproof
wenzelm@29731
   542
%
wenzelm@29731
   543
\isatagproof
wenzelm@29731
   544
\isacommand{proof}\isamarkupfalse%
wenzelm@29731
   545
\ {\isacharminus}\isanewline
wenzelm@29731
   546
\ \ \isacommand{from}\isamarkupfalse%
wenzelm@29731
   547
\ {\isacharbackquoteopen}{\isasymnot}\ A{\isacharbackquoteclose}\ \isacommand{have}\isamarkupfalse%
wenzelm@29731
   548
\ {\isachardoublequoteopen}A\ {\isasymlongrightarrow}\ {\isasymbottom}{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%
wenzelm@29731
   549
\ not{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse%
wenzelm@29731
   550
\isanewline
wenzelm@29731
   551
\ \ \isacommand{from}\isamarkupfalse%
wenzelm@29731
   552
\ {\isacharbackquoteopen}A\ {\isasymlongrightarrow}\ {\isasymbottom}{\isacharbackquoteclose}\ \isakeyword{and}\ {\isacharbackquoteopen}A{\isacharbackquoteclose}\ \isacommand{have}\isamarkupfalse%
wenzelm@29731
   553
\ {\isasymbottom}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
wenzelm@29731
   554
\isanewline
wenzelm@29731
   555
\ \ \isacommand{then}\isamarkupfalse%
wenzelm@29731
   556
\ \isacommand{show}\isamarkupfalse%
wenzelm@29731
   557
\ B\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
wenzelm@29731
   558
\isanewline
wenzelm@29731
   559
\isacommand{qed}\isamarkupfalse%
wenzelm@29731
   560
%
wenzelm@29731
   561
\endisatagproof
wenzelm@29731
   562
{\isafoldproof}%
wenzelm@29731
   563
%
wenzelm@29731
   564
\isadelimproof
wenzelm@29731
   565
%
wenzelm@29731
   566
\endisadelimproof
wenzelm@29731
   567
%
wenzelm@29731
   568
\isamarkupsubsection{Classical logic%
wenzelm@29731
   569
}
wenzelm@29731
   570
\isamarkuptrue%
wenzelm@29731
   571
%
wenzelm@29731
   572
\begin{isamarkuptext}%
wenzelm@29731
   573
Subsequently we state the principle of classical contradiction as a
wenzelm@29731
   574
  local assumption.  Thus we refrain from forcing the object-logic
wenzelm@29731
   575
  into the classical perspective.  Within that context, we may derive
wenzelm@29731
   576
  well-known consequences of the classical principle.%
wenzelm@29731
   577
\end{isamarkuptext}%
wenzelm@29731
   578
\isamarkuptrue%
wenzelm@29731
   579
\isacommand{locale}\isamarkupfalse%
wenzelm@29731
   580
\ classical\ {\isacharequal}\isanewline
wenzelm@29731
   581
\ \ \isakeyword{assumes}\ classical{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymnot}\ C\ {\isasymLongrightarrow}\ C{\isacharparenright}\ {\isasymLongrightarrow}\ C{\isachardoublequoteclose}\isanewline
wenzelm@29731
   582
\isakeyword{begin}\isanewline
wenzelm@29731
   583
\isanewline
wenzelm@29731
   584
\isacommand{theorem}\isamarkupfalse%
wenzelm@29731
   585
\ double{\isacharunderscore}negation{\isacharcolon}\isanewline
wenzelm@29731
   586
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymnot}\ {\isasymnot}\ C{\isachardoublequoteclose}\isanewline
wenzelm@29731
   587
\ \ \isakeyword{shows}\ C\isanewline
wenzelm@29731
   588
%
wenzelm@29731
   589
\isadelimproof
wenzelm@29731
   590
%
wenzelm@29731
   591
\endisadelimproof
wenzelm@29731
   592
%
wenzelm@29731
   593
\isatagproof
wenzelm@29731
   594
\isacommand{proof}\isamarkupfalse%
wenzelm@29731
   595
\ {\isacharparenleft}rule\ classical{\isacharparenright}\isanewline
wenzelm@29731
   596
\ \ \isacommand{assume}\isamarkupfalse%
wenzelm@29731
   597
\ {\isachardoublequoteopen}{\isasymnot}\ C{\isachardoublequoteclose}\isanewline
wenzelm@29731
   598
\ \ \isacommand{with}\isamarkupfalse%
wenzelm@29731
   599
\ {\isacharbackquoteopen}{\isasymnot}\ {\isasymnot}\ C{\isacharbackquoteclose}\ \isacommand{show}\isamarkupfalse%
wenzelm@29731
   600
\ C\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
wenzelm@29731
   601
\isanewline
wenzelm@29731
   602
\isacommand{qed}\isamarkupfalse%
wenzelm@29731
   603
%
wenzelm@29731
   604
\endisatagproof
wenzelm@29731
   605
{\isafoldproof}%
wenzelm@29731
   606
%
wenzelm@29731
   607
\isadelimproof
wenzelm@29731
   608
\isanewline
wenzelm@29731
   609
%
wenzelm@29731
   610
\endisadelimproof
wenzelm@29731
   611
\isanewline
wenzelm@29731
   612
\isacommand{theorem}\isamarkupfalse%
wenzelm@29731
   613
\ tertium{\isacharunderscore}non{\isacharunderscore}datur{\isacharcolon}\ {\isachardoublequoteopen}C\ {\isasymor}\ {\isasymnot}\ C{\isachardoublequoteclose}\isanewline
wenzelm@29731
   614
%
wenzelm@29731
   615
\isadelimproof
wenzelm@29731
   616
%
wenzelm@29731
   617
\endisadelimproof
wenzelm@29731
   618
%
wenzelm@29731
   619
\isatagproof
wenzelm@29731
   620
\isacommand{proof}\isamarkupfalse%
wenzelm@29731
   621
\ {\isacharparenleft}rule\ double{\isacharunderscore}negation{\isacharparenright}\isanewline
wenzelm@29731
   622
\ \ \isacommand{show}\isamarkupfalse%
wenzelm@29731
   623
\ {\isachardoublequoteopen}{\isasymnot}\ {\isasymnot}\ {\isacharparenleft}C\ {\isasymor}\ {\isasymnot}\ C{\isacharparenright}{\isachardoublequoteclose}\isanewline
wenzelm@29731
   624
\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@29731
   625
\isanewline
wenzelm@29731
   626
\ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@29731
   627
\ {\isachardoublequoteopen}{\isasymnot}\ {\isacharparenleft}C\ {\isasymor}\ {\isasymnot}\ C{\isacharparenright}{\isachardoublequoteclose}\isanewline
wenzelm@29731
   628
\ \ \ \ \isacommand{have}\isamarkupfalse%
wenzelm@29731
   629
\ {\isachardoublequoteopen}{\isasymnot}\ C{\isachardoublequoteclose}\isanewline
wenzelm@29731
   630
\ \ \ \ \isacommand{proof}\isamarkupfalse%
wenzelm@29731
   631
\isanewline
wenzelm@29731
   632
\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@29731
   633
\ C\ \isacommand{then}\isamarkupfalse%
wenzelm@29731
   634
\ \isacommand{have}\isamarkupfalse%
wenzelm@29731
   635
\ {\isachardoublequoteopen}C\ {\isasymor}\ {\isasymnot}\ C{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
wenzelm@29731
   636
\isanewline
wenzelm@29731
   637
\ \ \ \ \ \ \isacommand{with}\isamarkupfalse%
wenzelm@29731
   638
\ {\isacharbackquoteopen}{\isasymnot}\ {\isacharparenleft}C\ {\isasymor}\ {\isasymnot}\ C{\isacharparenright}{\isacharbackquoteclose}\ \isacommand{show}\isamarkupfalse%
wenzelm@29731
   639
\ {\isasymbottom}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
wenzelm@29731
   640
\isanewline
wenzelm@29731
   641
\ \ \ \ \isacommand{qed}\isamarkupfalse%
wenzelm@29731
   642
\isanewline
wenzelm@29731
   643
\ \ \ \ \isacommand{then}\isamarkupfalse%
wenzelm@29731
   644
\ \isacommand{have}\isamarkupfalse%
wenzelm@29731
   645
\ {\isachardoublequoteopen}C\ {\isasymor}\ {\isasymnot}\ C{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
wenzelm@29731
   646
\isanewline
wenzelm@29731
   647
\ \ \ \ \isacommand{with}\isamarkupfalse%
wenzelm@29731
   648
\ {\isacharbackquoteopen}{\isasymnot}\ {\isacharparenleft}C\ {\isasymor}\ {\isasymnot}\ C{\isacharparenright}{\isacharbackquoteclose}\ \isacommand{show}\isamarkupfalse%
wenzelm@29731
   649
\ {\isasymbottom}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
wenzelm@29731
   650
\isanewline
wenzelm@29731
   651
\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@29731
   652
\isanewline
wenzelm@29731
   653
\isacommand{qed}\isamarkupfalse%
wenzelm@29731
   654
%
wenzelm@29731
   655
\endisatagproof
wenzelm@29731
   656
{\isafoldproof}%
wenzelm@29731
   657
%
wenzelm@29731
   658
\isadelimproof
wenzelm@29731
   659
%
wenzelm@29731
   660
\endisadelimproof
wenzelm@29731
   661
%
wenzelm@29731
   662
\begin{isamarkuptext}%
wenzelm@29740
   663
\noindent These examples illustrate both classical reasoning and
wenzelm@29740
   664
  non-trivial propositional proofs in general.  All three rules
wenzelm@29740
   665
  characterize classical logic independently, but the original rule is
wenzelm@29740
   666
  already the most convenient to use, because it leaves the conclusion
wenzelm@29740
   667
  unchanged.  Note that \isa{{\isachardoublequote}{\isacharparenleft}{\isasymnot}\ C\ {\isasymLongrightarrow}\ C{\isacharparenright}\ {\isasymLongrightarrow}\ C{\isachardoublequote}} fits again into our
wenzelm@29740
   668
  format for eliminations, despite the additional twist that the
wenzelm@29740
   669
  context refers to the main conclusion.  So we may write \isa{classical} as the Isar statement ``\isa{{\isachardoublequote}{\isasymOBTAINS}\ {\isasymnot}\ thesis{\isachardoublequote}}''.
wenzelm@29740
   670
  This also explains nicely how classical reasoning really works:
wenzelm@29740
   671
  whatever the main \isa{thesis} might be, we may always assume its
wenzelm@29740
   672
  negation!%
wenzelm@29731
   673
\end{isamarkuptext}%
wenzelm@29731
   674
\isamarkuptrue%
wenzelm@29731
   675
\isacommand{end}\isamarkupfalse%
wenzelm@29731
   676
%
wenzelm@29740
   677
\isamarkupsubsection{Quantifiers \label{sec:framework-ex-quant}%
wenzelm@29731
   678
}
wenzelm@29731
   679
\isamarkuptrue%
wenzelm@29731
   680
%
wenzelm@29731
   681
\begin{isamarkuptext}%
wenzelm@29731
   682
Representing quantifiers is easy, thanks to the higher-order nature
wenzelm@29731
   683
  of the underlying framework.  According to the well-known technique
wenzelm@29731
   684
  introduced by Church \cite{church40}, quantifiers are operators on
wenzelm@29731
   685
  predicates, which are syntactically represented as \isa{{\isachardoublequote}{\isasymlambda}{\isachardoublequote}}-terms
wenzelm@29740
   686
  of type \isa{{\isachardoublequote}i\ {\isasymRightarrow}\ o{\isachardoublequote}}.  Binder notation turns \isa{{\isachardoublequote}All\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ B\ x{\isacharparenright}{\isachardoublequote}} into \isa{{\isachardoublequote}{\isasymforall}x{\isachardot}\ B\ x{\isachardoublequote}} etc.%
wenzelm@29731
   687
\end{isamarkuptext}%
wenzelm@29731
   688
\isamarkuptrue%
wenzelm@29731
   689
\isacommand{axiomatization}\isamarkupfalse%
wenzelm@29731
   690
\isanewline
wenzelm@29731
   691
\ \ All\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isasymRightarrow}\ o{\isacharparenright}\ {\isasymRightarrow}\ o{\isachardoublequoteclose}\ \ {\isacharparenleft}\isakeyword{binder}\ {\isachardoublequoteopen}{\isasymforall}{\isachardoublequoteclose}\ {\isadigit{1}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\isanewline
wenzelm@29731
   692
\ \ allI\ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymAnd}x{\isachardot}\ B\ x{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymforall}x{\isachardot}\ B\ x{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
wenzelm@29731
   693
\ \ allD\ {\isacharbrackleft}dest{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymforall}x{\isachardot}\ B\ x{\isacharparenright}\ {\isasymLongrightarrow}\ B\ a{\isachardoublequoteclose}\isanewline
wenzelm@29731
   694
\isanewline
wenzelm@29731
   695
\isacommand{axiomatization}\isamarkupfalse%
wenzelm@29731
   696
\isanewline
wenzelm@29731
   697
\ \ Ex\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isasymRightarrow}\ o{\isacharparenright}\ {\isasymRightarrow}\ o{\isachardoublequoteclose}\ \ {\isacharparenleft}\isakeyword{binder}\ {\isachardoublequoteopen}{\isasymexists}{\isachardoublequoteclose}\ {\isadigit{1}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\isanewline
wenzelm@29731
   698
\ \ exI\ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}B\ a\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymexists}x{\isachardot}\ B\ x{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
wenzelm@29731
   699
\ \ exE\ {\isacharbrackleft}elim{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymexists}x{\isachardot}\ B\ x{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ B\ x\ {\isasymLongrightarrow}\ C{\isacharparenright}\ {\isasymLongrightarrow}\ C{\isachardoublequoteclose}%
wenzelm@29731
   700
\begin{isamarkuptext}%
wenzelm@29740
   701
\noindent The statement of \isa{exE} corresponds to ``\isa{{\isachardoublequote}{\isasymASSUMES}\ {\isasymexists}x{\isachardot}\ B\ x\ {\isasymOBTAINS}\ x\ {\isasymWHERE}\ B\ x{\isachardoublequote}}'' in Isar.  In the
wenzelm@29740
   702
  subsequent example we illustrate quantifier reasoning involving all
wenzelm@29740
   703
  four rules:%
wenzelm@29731
   704
\end{isamarkuptext}%
wenzelm@29731
   705
\isamarkuptrue%
wenzelm@29731
   706
\isacommand{theorem}\isamarkupfalse%
wenzelm@29731
   707
\isanewline
wenzelm@29731
   708
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymexists}x{\isachardot}\ {\isasymforall}y{\isachardot}\ R\ x\ y{\isachardoublequoteclose}\isanewline
wenzelm@29731
   709
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymforall}y{\isachardot}\ {\isasymexists}x{\isachardot}\ R\ x\ y{\isachardoublequoteclose}\isanewline
wenzelm@29731
   710
%
wenzelm@29731
   711
\isadelimproof
wenzelm@29731
   712
%
wenzelm@29731
   713
\endisadelimproof
wenzelm@29731
   714
%
wenzelm@29731
   715
\isatagproof
wenzelm@29731
   716
\isacommand{proof}\isamarkupfalse%
wenzelm@29731
   717
\ \ \ \ %
wenzelm@29731
   718
\isamarkupcmt{\isa{{\isachardoublequote}{\isasymforall}{\isachardoublequote}} introduction%
wenzelm@29731
   719
}
wenzelm@29731
   720
\isanewline
wenzelm@29731
   721
\ \ \isacommand{obtain}\isamarkupfalse%
wenzelm@29731
   722
\ x\ \isakeyword{where}\ {\isachardoublequoteopen}{\isasymforall}y{\isachardot}\ R\ x\ y{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse%
wenzelm@29731
   723
\ {\isacharbackquoteopen}{\isasymexists}x{\isachardot}\ {\isasymforall}y{\isachardot}\ R\ x\ y{\isacharbackquoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
wenzelm@29731
   724
\ \ \ \ %
wenzelm@29731
   725
\isamarkupcmt{\isa{{\isachardoublequote}{\isasymexists}{\isachardoublequote}} elimination%
wenzelm@29731
   726
}
wenzelm@29731
   727
\isanewline
wenzelm@29731
   728
\ \ \isacommand{fix}\isamarkupfalse%
wenzelm@29731
   729
\ y\ \isacommand{have}\isamarkupfalse%
wenzelm@29731
   730
\ {\isachardoublequoteopen}R\ x\ y{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse%
wenzelm@29731
   731
\ {\isacharbackquoteopen}{\isasymforall}y{\isachardot}\ R\ x\ y{\isacharbackquoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
wenzelm@29731
   732
\ \ \ \ %
wenzelm@29731
   733
\isamarkupcmt{\isa{{\isachardoublequote}{\isasymforall}{\isachardoublequote}} destruction%
wenzelm@29731
   734
}
wenzelm@29731
   735
\isanewline
wenzelm@29731
   736
\ \ \isacommand{then}\isamarkupfalse%
wenzelm@29731
   737
\ \isacommand{show}\isamarkupfalse%
wenzelm@29731
   738
\ {\isachardoublequoteopen}{\isasymexists}x{\isachardot}\ R\ x\ y{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
wenzelm@29731
   739
\ \ \ \ %
wenzelm@29731
   740
\isamarkupcmt{\isa{{\isachardoublequote}{\isasymexists}{\isachardoublequote}} introduction%
wenzelm@29731
   741
}
wenzelm@29731
   742
\isanewline
wenzelm@29731
   743
\isacommand{qed}\isamarkupfalse%
wenzelm@29731
   744
%
wenzelm@29731
   745
\endisatagproof
wenzelm@29731
   746
{\isafoldproof}%
wenzelm@29731
   747
%
wenzelm@29731
   748
\isadelimproof
wenzelm@29740
   749
%
wenzelm@29740
   750
\endisadelimproof
wenzelm@29740
   751
%
wenzelm@29740
   752
\isamarkupsubsection{Canonical reasoning patterns%
wenzelm@29740
   753
}
wenzelm@29740
   754
\isamarkuptrue%
wenzelm@29740
   755
%
wenzelm@29740
   756
\begin{isamarkuptext}%
wenzelm@29740
   757
The main rules of first-order predicate logic from
wenzelm@29740
   758
  \secref{sec:framework-ex-prop} and \secref{sec:framework-ex-quant}
wenzelm@29740
   759
  can now be summarized as follows, using the native Isar statement
wenzelm@29740
   760
  format of \secref{sec:framework-stmt}.
wenzelm@29740
   761
wenzelm@29740
   762
  \medskip
wenzelm@29740
   763
  \begin{tabular}{l}
wenzelm@29740
   764
  \isa{{\isachardoublequote}impI{\isacharcolon}\ {\isasymASSUMES}\ A\ {\isasymLongrightarrow}\ B\ {\isasymSHOWS}\ A\ {\isasymlongrightarrow}\ B{\isachardoublequote}} \\
wenzelm@29740
   765
  \isa{{\isachardoublequote}impD{\isacharcolon}\ {\isasymASSUMES}\ A\ {\isasymlongrightarrow}\ B\ {\isasymAND}\ A\ {\isasymSHOWS}\ B{\isachardoublequote}} \\[1ex]
wenzelm@29740
   766
wenzelm@29740
   767
  \isa{{\isachardoublequote}disjI\isactrlisub {\isadigit{1}}{\isacharcolon}\ {\isasymASSUMES}\ A\ {\isasymSHOWS}\ A\ {\isasymor}\ B{\isachardoublequote}} \\
wenzelm@29740
   768
  \isa{{\isachardoublequote}disjI\isactrlisub {\isadigit{2}}{\isacharcolon}\ {\isasymASSUMES}\ B\ {\isasymSHOWS}\ A\ {\isasymor}\ B{\isachardoublequote}} \\
wenzelm@29740
   769
  \isa{{\isachardoublequote}disjE{\isacharcolon}\ {\isasymASSUMES}\ A\ {\isasymor}\ B\ {\isasymOBTAINS}\ A\ {\isasymBBAR}\ B{\isachardoublequote}} \\[1ex]
wenzelm@29740
   770
wenzelm@29740
   771
  \isa{{\isachardoublequote}conjI{\isacharcolon}\ {\isasymASSUMES}\ A\ {\isasymAND}\ B\ {\isasymSHOWS}\ A\ {\isasymand}\ B{\isachardoublequote}} \\
wenzelm@29740
   772
  \isa{{\isachardoublequote}conjE{\isacharcolon}\ {\isasymASSUMES}\ A\ {\isasymand}\ B\ {\isasymOBTAINS}\ A\ {\isasymAND}\ B{\isachardoublequote}} \\[1ex]
wenzelm@29740
   773
wenzelm@29740
   774
  \isa{{\isachardoublequote}falseE{\isacharcolon}\ {\isasymASSUMES}\ {\isasymbottom}\ {\isasymSHOWS}\ A{\isachardoublequote}} \\
wenzelm@29740
   775
  \isa{{\isachardoublequote}trueI{\isacharcolon}\ {\isasymSHOWS}\ {\isasymtop}{\isachardoublequote}} \\[1ex]
wenzelm@29740
   776
wenzelm@29740
   777
  \isa{{\isachardoublequote}notI{\isacharcolon}\ {\isasymASSUMES}\ A\ {\isasymLongrightarrow}\ {\isasymbottom}\ {\isasymSHOWS}\ {\isasymnot}\ A{\isachardoublequote}} \\
wenzelm@29740
   778
  \isa{{\isachardoublequote}notE{\isacharcolon}\ {\isasymASSUMES}\ {\isasymnot}\ A\ {\isasymAND}\ A\ {\isasymSHOWS}\ B{\isachardoublequote}} \\[1ex]
wenzelm@29740
   779
wenzelm@29740
   780
  \isa{{\isachardoublequote}allI{\isacharcolon}\ {\isasymASSUMES}\ {\isasymAnd}x{\isachardot}\ B\ x\ {\isasymSHOWS}\ {\isasymforall}x{\isachardot}\ B\ x{\isachardoublequote}} \\
wenzelm@29740
   781
  \isa{{\isachardoublequote}allE{\isacharcolon}\ {\isasymASSUMES}\ {\isasymforall}x{\isachardot}\ B\ x\ {\isasymSHOWS}\ B\ a{\isachardoublequote}} \\[1ex]
wenzelm@29740
   782
wenzelm@29740
   783
  \isa{{\isachardoublequote}exI{\isacharcolon}\ {\isasymASSUMES}\ B\ a\ {\isasymSHOWS}\ {\isasymexists}x{\isachardot}\ B\ x{\isachardoublequote}} \\
wenzelm@29740
   784
  \isa{{\isachardoublequote}exE{\isacharcolon}\ {\isasymASSUMES}\ {\isasymexists}x{\isachardot}\ B\ x\ {\isasymOBTAINS}\ a\ {\isasymWHERE}\ B\ a{\isachardoublequote}}
wenzelm@29740
   785
  \end{tabular}
wenzelm@29740
   786
  \medskip
wenzelm@29740
   787
wenzelm@29740
   788
  \noindent This essentially provides a declarative reading of Pure
wenzelm@29740
   789
  rules as Isar reasoning patterns: the rule statements tells how a
wenzelm@29740
   790
  canonical proof outline shall look like.  Since the above rules have
wenzelm@29740
   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
wenzelm@29740
   792
  particular shape --- we can immediately write Isar proof texts as
wenzelm@29740
   793
  follows:%
wenzelm@29740
   794
\end{isamarkuptext}%
wenzelm@29740
   795
\isamarkuptrue%
wenzelm@29740
   796
%
wenzelm@29740
   797
\isadelimproof
wenzelm@29740
   798
%
wenzelm@29740
   799
\endisadelimproof
wenzelm@29740
   800
%
wenzelm@29740
   801
\isatagproof
wenzelm@29740
   802
%
wenzelm@29740
   803
\begin{minipage}[t]{0.4\textwidth}
wenzelm@29731
   804
\isanewline
wenzelm@29740
   805
\ \ \isacommand{have}\isamarkupfalse%
wenzelm@29740
   806
\ {\isachardoublequoteopen}A\ {\isasymlongrightarrow}\ B{\isachardoublequoteclose}\isanewline
wenzelm@29740
   807
\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@29740
   808
\isanewline
wenzelm@29740
   809
\ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@29740
   810
\ A\isanewline
wenzelm@29740
   811
\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@29740
   812
\ B%
wenzelm@29740
   813
\endisatagproof
wenzelm@29740
   814
{\isafoldproof}%
wenzelm@29740
   815
%
wenzelm@29740
   816
\isadelimproof
wenzelm@29740
   817
%
wenzelm@29740
   818
\endisadelimproof
wenzelm@29740
   819
%
wenzelm@29740
   820
\isadelimnoproof
wenzelm@29740
   821
\ %
wenzelm@29740
   822
\endisadelimnoproof
wenzelm@29740
   823
%
wenzelm@29740
   824
\isatagnoproof
wenzelm@29740
   825
\isacommand{sorry}\isamarkupfalse%
wenzelm@29740
   826
%
wenzelm@29740
   827
\endisatagnoproof
wenzelm@29740
   828
{\isafoldnoproof}%
wenzelm@29740
   829
%
wenzelm@29740
   830
\isadelimnoproof
wenzelm@29740
   831
\isanewline
wenzelm@29740
   832
%
wenzelm@29740
   833
\endisadelimnoproof
wenzelm@29740
   834
%
wenzelm@29740
   835
\isadelimproof
wenzelm@29740
   836
\ \ %
wenzelm@29740
   837
\endisadelimproof
wenzelm@29740
   838
%
wenzelm@29740
   839
\isatagproof
wenzelm@29740
   840
\isacommand{qed}\isamarkupfalse%
wenzelm@29740
   841
%
wenzelm@29740
   842
\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}
wenzelm@29740
   843
\isanewline
wenzelm@29740
   844
\ \ \isacommand{have}\isamarkupfalse%
wenzelm@29740
   845
\ {\isachardoublequoteopen}A\ {\isasymlongrightarrow}\ B{\isachardoublequoteclose}\ \isakeyword{and}\ A%
wenzelm@29740
   846
\endisatagproof
wenzelm@29740
   847
{\isafoldproof}%
wenzelm@29740
   848
%
wenzelm@29740
   849
\isadelimproof
wenzelm@29740
   850
%
wenzelm@29740
   851
\endisadelimproof
wenzelm@29740
   852
%
wenzelm@29740
   853
\isadelimnoproof
wenzelm@29740
   854
\ %
wenzelm@29740
   855
\endisadelimnoproof
wenzelm@29740
   856
%
wenzelm@29740
   857
\isatagnoproof
wenzelm@29740
   858
\isacommand{sorry}\isamarkupfalse%
wenzelm@29740
   859
%
wenzelm@29740
   860
\endisatagnoproof
wenzelm@29740
   861
{\isafoldnoproof}%
wenzelm@29740
   862
%
wenzelm@29740
   863
\isadelimnoproof
wenzelm@29740
   864
\isanewline
wenzelm@29740
   865
%
wenzelm@29740
   866
\endisadelimnoproof
wenzelm@29740
   867
%
wenzelm@29740
   868
\isadelimproof
wenzelm@29740
   869
\ \ %
wenzelm@29740
   870
\endisadelimproof
wenzelm@29740
   871
%
wenzelm@29740
   872
\isatagproof
wenzelm@29740
   873
\isacommand{then}\isamarkupfalse%
wenzelm@29740
   874
\ \isacommand{have}\isamarkupfalse%
wenzelm@29740
   875
\ B\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
wenzelm@29740
   876
%
wenzelm@29740
   877
\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}
wenzelm@29740
   878
\isanewline
wenzelm@29740
   879
\ \ \isacommand{have}\isamarkupfalse%
wenzelm@29740
   880
\ A%
wenzelm@29740
   881
\endisatagproof
wenzelm@29740
   882
{\isafoldproof}%
wenzelm@29740
   883
%
wenzelm@29740
   884
\isadelimproof
wenzelm@29740
   885
%
wenzelm@29740
   886
\endisadelimproof
wenzelm@29740
   887
%
wenzelm@29740
   888
\isadelimnoproof
wenzelm@29740
   889
\ %
wenzelm@29740
   890
\endisadelimnoproof
wenzelm@29740
   891
%
wenzelm@29740
   892
\isatagnoproof
wenzelm@29740
   893
\isacommand{sorry}\isamarkupfalse%
wenzelm@29740
   894
%
wenzelm@29740
   895
\endisatagnoproof
wenzelm@29740
   896
{\isafoldnoproof}%
wenzelm@29740
   897
%
wenzelm@29740
   898
\isadelimnoproof
wenzelm@29740
   899
\isanewline
wenzelm@29740
   900
%
wenzelm@29740
   901
\endisadelimnoproof
wenzelm@29740
   902
%
wenzelm@29740
   903
\isadelimproof
wenzelm@29740
   904
\ \ %
wenzelm@29740
   905
\endisadelimproof
wenzelm@29740
   906
%
wenzelm@29740
   907
\isatagproof
wenzelm@29740
   908
\isacommand{then}\isamarkupfalse%
wenzelm@29740
   909
\ \isacommand{have}\isamarkupfalse%
wenzelm@29740
   910
\ {\isachardoublequoteopen}A\ {\isasymor}\ B{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
wenzelm@29740
   911
\isanewline
wenzelm@29740
   912
\isanewline
wenzelm@29740
   913
\ \ \isacommand{have}\isamarkupfalse%
wenzelm@29740
   914
\ B%
wenzelm@29740
   915
\endisatagproof
wenzelm@29740
   916
{\isafoldproof}%
wenzelm@29740
   917
%
wenzelm@29740
   918
\isadelimproof
wenzelm@29740
   919
%
wenzelm@29740
   920
\endisadelimproof
wenzelm@29740
   921
%
wenzelm@29740
   922
\isadelimnoproof
wenzelm@29740
   923
\ %
wenzelm@29740
   924
\endisadelimnoproof
wenzelm@29740
   925
%
wenzelm@29740
   926
\isatagnoproof
wenzelm@29740
   927
\isacommand{sorry}\isamarkupfalse%
wenzelm@29740
   928
%
wenzelm@29740
   929
\endisatagnoproof
wenzelm@29740
   930
{\isafoldnoproof}%
wenzelm@29740
   931
%
wenzelm@29740
   932
\isadelimnoproof
wenzelm@29740
   933
\isanewline
wenzelm@29740
   934
%
wenzelm@29740
   935
\endisadelimnoproof
wenzelm@29740
   936
%
wenzelm@29740
   937
\isadelimproof
wenzelm@29740
   938
\ \ %
wenzelm@29740
   939
\endisadelimproof
wenzelm@29740
   940
%
wenzelm@29740
   941
\isatagproof
wenzelm@29740
   942
\isacommand{then}\isamarkupfalse%
wenzelm@29740
   943
\ \isacommand{have}\isamarkupfalse%
wenzelm@29740
   944
\ {\isachardoublequoteopen}A\ {\isasymor}\ B{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
wenzelm@29740
   945
%
wenzelm@29740
   946
\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}
wenzelm@29740
   947
\isanewline
wenzelm@29740
   948
\ \ \isacommand{have}\isamarkupfalse%
wenzelm@29740
   949
\ {\isachardoublequoteopen}A\ {\isasymor}\ B{\isachardoublequoteclose}%
wenzelm@29740
   950
\endisatagproof
wenzelm@29740
   951
{\isafoldproof}%
wenzelm@29740
   952
%
wenzelm@29740
   953
\isadelimproof
wenzelm@29740
   954
%
wenzelm@29740
   955
\endisadelimproof
wenzelm@29740
   956
%
wenzelm@29740
   957
\isadelimnoproof
wenzelm@29740
   958
\ %
wenzelm@29740
   959
\endisadelimnoproof
wenzelm@29740
   960
%
wenzelm@29740
   961
\isatagnoproof
wenzelm@29740
   962
\isacommand{sorry}\isamarkupfalse%
wenzelm@29740
   963
%
wenzelm@29740
   964
\endisatagnoproof
wenzelm@29740
   965
{\isafoldnoproof}%
wenzelm@29740
   966
%
wenzelm@29740
   967
\isadelimnoproof
wenzelm@29740
   968
\isanewline
wenzelm@29740
   969
%
wenzelm@29740
   970
\endisadelimnoproof
wenzelm@29740
   971
%
wenzelm@29740
   972
\isadelimproof
wenzelm@29740
   973
\ \ %
wenzelm@29740
   974
\endisadelimproof
wenzelm@29740
   975
%
wenzelm@29740
   976
\isatagproof
wenzelm@29740
   977
\isacommand{then}\isamarkupfalse%
wenzelm@29740
   978
\ \isacommand{have}\isamarkupfalse%
wenzelm@29740
   979
\ C\isanewline
wenzelm@29740
   980
\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@29740
   981
\isanewline
wenzelm@29740
   982
\ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@29740
   983
\ A\isanewline
wenzelm@29740
   984
\ \ \ \ \isacommand{then}\isamarkupfalse%
wenzelm@29740
   985
\ \isacommand{show}\isamarkupfalse%
wenzelm@29740
   986
\ C%
wenzelm@29740
   987
\endisatagproof
wenzelm@29740
   988
{\isafoldproof}%
wenzelm@29740
   989
%
wenzelm@29740
   990
\isadelimproof
wenzelm@29740
   991
%
wenzelm@29740
   992
\endisadelimproof
wenzelm@29740
   993
%
wenzelm@29740
   994
\isadelimnoproof
wenzelm@29740
   995
\ %
wenzelm@29740
   996
\endisadelimnoproof
wenzelm@29740
   997
%
wenzelm@29740
   998
\isatagnoproof
wenzelm@29740
   999
\isacommand{sorry}\isamarkupfalse%
wenzelm@29740
  1000
%
wenzelm@29740
  1001
\endisatagnoproof
wenzelm@29740
  1002
{\isafoldnoproof}%
wenzelm@29740
  1003
%
wenzelm@29740
  1004
\isadelimnoproof
wenzelm@29740
  1005
\isanewline
wenzelm@29740
  1006
%
wenzelm@29740
  1007
\endisadelimnoproof
wenzelm@29740
  1008
%
wenzelm@29740
  1009
\isadelimproof
wenzelm@29740
  1010
\ \ %
wenzelm@29740
  1011
\endisadelimproof
wenzelm@29740
  1012
%
wenzelm@29740
  1013
\isatagproof
wenzelm@29740
  1014
\isacommand{next}\isamarkupfalse%
wenzelm@29740
  1015
\isanewline
wenzelm@29740
  1016
\ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@29740
  1017
\ B\isanewline
wenzelm@29740
  1018
\ \ \ \ \isacommand{then}\isamarkupfalse%
wenzelm@29740
  1019
\ \isacommand{show}\isamarkupfalse%
wenzelm@29740
  1020
\ C%
wenzelm@29740
  1021
\endisatagproof
wenzelm@29740
  1022
{\isafoldproof}%
wenzelm@29740
  1023
%
wenzelm@29740
  1024
\isadelimproof
wenzelm@29740
  1025
%
wenzelm@29740
  1026
\endisadelimproof
wenzelm@29740
  1027
%
wenzelm@29740
  1028
\isadelimnoproof
wenzelm@29740
  1029
\ %
wenzelm@29740
  1030
\endisadelimnoproof
wenzelm@29740
  1031
%
wenzelm@29740
  1032
\isatagnoproof
wenzelm@29740
  1033
\isacommand{sorry}\isamarkupfalse%
wenzelm@29740
  1034
%
wenzelm@29740
  1035
\endisatagnoproof
wenzelm@29740
  1036
{\isafoldnoproof}%
wenzelm@29740
  1037
%
wenzelm@29740
  1038
\isadelimnoproof
wenzelm@29740
  1039
\isanewline
wenzelm@29740
  1040
%
wenzelm@29740
  1041
\endisadelimnoproof
wenzelm@29740
  1042
%
wenzelm@29740
  1043
\isadelimproof
wenzelm@29740
  1044
\ \ %
wenzelm@29740
  1045
\endisadelimproof
wenzelm@29740
  1046
%
wenzelm@29740
  1047
\isatagproof
wenzelm@29740
  1048
\isacommand{qed}\isamarkupfalse%
wenzelm@29740
  1049
%
wenzelm@29740
  1050
\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}
wenzelm@29740
  1051
\isanewline
wenzelm@29740
  1052
\ \ \isacommand{have}\isamarkupfalse%
wenzelm@29740
  1053
\ A\ \isakeyword{and}\ B%
wenzelm@29740
  1054
\endisatagproof
wenzelm@29740
  1055
{\isafoldproof}%
wenzelm@29740
  1056
%
wenzelm@29740
  1057
\isadelimproof
wenzelm@29731
  1058
%
wenzelm@29731
  1059
\endisadelimproof
wenzelm@29731
  1060
%
wenzelm@29740
  1061
\isadelimnoproof
wenzelm@29740
  1062
\ %
wenzelm@29740
  1063
\endisadelimnoproof
wenzelm@29740
  1064
%
wenzelm@29740
  1065
\isatagnoproof
wenzelm@29740
  1066
\isacommand{sorry}\isamarkupfalse%
wenzelm@29740
  1067
%
wenzelm@29740
  1068
\endisatagnoproof
wenzelm@29740
  1069
{\isafoldnoproof}%
wenzelm@29740
  1070
%
wenzelm@29740
  1071
\isadelimnoproof
wenzelm@29740
  1072
\isanewline
wenzelm@29740
  1073
%
wenzelm@29740
  1074
\endisadelimnoproof
wenzelm@29740
  1075
%
wenzelm@29740
  1076
\isadelimproof
wenzelm@29740
  1077
\ \ %
wenzelm@29740
  1078
\endisadelimproof
wenzelm@29740
  1079
%
wenzelm@29740
  1080
\isatagproof
wenzelm@29740
  1081
\isacommand{then}\isamarkupfalse%
wenzelm@29740
  1082
\ \isacommand{have}\isamarkupfalse%
wenzelm@29740
  1083
\ {\isachardoublequoteopen}A\ {\isasymand}\ B{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
wenzelm@29740
  1084
%
wenzelm@29740
  1085
\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}
wenzelm@29740
  1086
\isanewline
wenzelm@29740
  1087
\ \ \isacommand{have}\isamarkupfalse%
wenzelm@29740
  1088
\ {\isachardoublequoteopen}A\ {\isasymand}\ B{\isachardoublequoteclose}%
wenzelm@29740
  1089
\endisatagproof
wenzelm@29740
  1090
{\isafoldproof}%
wenzelm@29740
  1091
%
wenzelm@29740
  1092
\isadelimproof
wenzelm@29740
  1093
%
wenzelm@29740
  1094
\endisadelimproof
wenzelm@29740
  1095
%
wenzelm@29740
  1096
\isadelimnoproof
wenzelm@29740
  1097
\ %
wenzelm@29740
  1098
\endisadelimnoproof
wenzelm@29740
  1099
%
wenzelm@29740
  1100
\isatagnoproof
wenzelm@29740
  1101
\isacommand{sorry}\isamarkupfalse%
wenzelm@29740
  1102
%
wenzelm@29740
  1103
\endisatagnoproof
wenzelm@29740
  1104
{\isafoldnoproof}%
wenzelm@29740
  1105
%
wenzelm@29740
  1106
\isadelimnoproof
wenzelm@29740
  1107
\isanewline
wenzelm@29740
  1108
%
wenzelm@29740
  1109
\endisadelimnoproof
wenzelm@29740
  1110
%
wenzelm@29740
  1111
\isadelimproof
wenzelm@29740
  1112
\ \ %
wenzelm@29740
  1113
\endisadelimproof
wenzelm@29740
  1114
%
wenzelm@29740
  1115
\isatagproof
wenzelm@29740
  1116
\isacommand{then}\isamarkupfalse%
wenzelm@29740
  1117
\ \isacommand{obtain}\isamarkupfalse%
wenzelm@29740
  1118
\ A\ \isakeyword{and}\ B\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
wenzelm@29740
  1119
%
wenzelm@29740
  1120
\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}
wenzelm@29740
  1121
\isanewline
wenzelm@29740
  1122
\ \ \isacommand{have}\isamarkupfalse%
wenzelm@29740
  1123
\ {\isachardoublequoteopen}{\isasymbottom}{\isachardoublequoteclose}%
wenzelm@29740
  1124
\endisatagproof
wenzelm@29740
  1125
{\isafoldproof}%
wenzelm@29740
  1126
%
wenzelm@29740
  1127
\isadelimproof
wenzelm@29740
  1128
%
wenzelm@29740
  1129
\endisadelimproof
wenzelm@29740
  1130
%
wenzelm@29740
  1131
\isadelimnoproof
wenzelm@29740
  1132
\ %
wenzelm@29740
  1133
\endisadelimnoproof
wenzelm@29740
  1134
%
wenzelm@29740
  1135
\isatagnoproof
wenzelm@29740
  1136
\isacommand{sorry}\isamarkupfalse%
wenzelm@29740
  1137
%
wenzelm@29740
  1138
\endisatagnoproof
wenzelm@29740
  1139
{\isafoldnoproof}%
wenzelm@29740
  1140
%
wenzelm@29740
  1141
\isadelimnoproof
wenzelm@29740
  1142
\isanewline
wenzelm@29740
  1143
%
wenzelm@29740
  1144
\endisadelimnoproof
wenzelm@29740
  1145
%
wenzelm@29740
  1146
\isadelimproof
wenzelm@29740
  1147
\ \ %
wenzelm@29740
  1148
\endisadelimproof
wenzelm@29740
  1149
%
wenzelm@29740
  1150
\isatagproof
wenzelm@29740
  1151
\isacommand{then}\isamarkupfalse%
wenzelm@29740
  1152
\ \isacommand{have}\isamarkupfalse%
wenzelm@29740
  1153
\ A\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
wenzelm@29740
  1154
%
wenzelm@29740
  1155
\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}
wenzelm@29740
  1156
\isanewline
wenzelm@29740
  1157
\ \ \isacommand{have}\isamarkupfalse%
wenzelm@29740
  1158
\ {\isachardoublequoteopen}{\isasymtop}{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
wenzelm@29740
  1159
%
wenzelm@29740
  1160
\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}
wenzelm@29740
  1161
\isanewline
wenzelm@29740
  1162
\ \ \isacommand{have}\isamarkupfalse%
wenzelm@29740
  1163
\ {\isachardoublequoteopen}{\isasymnot}\ A{\isachardoublequoteclose}\isanewline
wenzelm@29740
  1164
\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@29740
  1165
\isanewline
wenzelm@29740
  1166
\ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@29740
  1167
\ A\isanewline
wenzelm@29740
  1168
\ \ \ \ \isacommand{then}\isamarkupfalse%
wenzelm@29740
  1169
\ \isacommand{show}\isamarkupfalse%
wenzelm@29740
  1170
\ {\isachardoublequoteopen}{\isasymbottom}{\isachardoublequoteclose}%
wenzelm@29740
  1171
\endisatagproof
wenzelm@29740
  1172
{\isafoldproof}%
wenzelm@29740
  1173
%
wenzelm@29740
  1174
\isadelimproof
wenzelm@29740
  1175
%
wenzelm@29740
  1176
\endisadelimproof
wenzelm@29740
  1177
%
wenzelm@29740
  1178
\isadelimnoproof
wenzelm@29740
  1179
\ %
wenzelm@29740
  1180
\endisadelimnoproof
wenzelm@29740
  1181
%
wenzelm@29740
  1182
\isatagnoproof
wenzelm@29740
  1183
\isacommand{sorry}\isamarkupfalse%
wenzelm@29740
  1184
%
wenzelm@29740
  1185
\endisatagnoproof
wenzelm@29740
  1186
{\isafoldnoproof}%
wenzelm@29740
  1187
%
wenzelm@29740
  1188
\isadelimnoproof
wenzelm@29740
  1189
\isanewline
wenzelm@29740
  1190
%
wenzelm@29740
  1191
\endisadelimnoproof
wenzelm@29740
  1192
%
wenzelm@29740
  1193
\isadelimproof
wenzelm@29740
  1194
\ \ %
wenzelm@29740
  1195
\endisadelimproof
wenzelm@29740
  1196
%
wenzelm@29740
  1197
\isatagproof
wenzelm@29740
  1198
\isacommand{qed}\isamarkupfalse%
wenzelm@29740
  1199
%
wenzelm@29740
  1200
\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}
wenzelm@29740
  1201
\isanewline
wenzelm@29740
  1202
\ \ \isacommand{have}\isamarkupfalse%
wenzelm@29740
  1203
\ {\isachardoublequoteopen}{\isasymnot}\ A{\isachardoublequoteclose}\ \isakeyword{and}\ A%
wenzelm@29740
  1204
\endisatagproof
wenzelm@29740
  1205
{\isafoldproof}%
wenzelm@29740
  1206
%
wenzelm@29740
  1207
\isadelimproof
wenzelm@29740
  1208
%
wenzelm@29740
  1209
\endisadelimproof
wenzelm@29740
  1210
%
wenzelm@29740
  1211
\isadelimnoproof
wenzelm@29740
  1212
\ %
wenzelm@29740
  1213
\endisadelimnoproof
wenzelm@29740
  1214
%
wenzelm@29740
  1215
\isatagnoproof
wenzelm@29740
  1216
\isacommand{sorry}\isamarkupfalse%
wenzelm@29740
  1217
%
wenzelm@29740
  1218
\endisatagnoproof
wenzelm@29740
  1219
{\isafoldnoproof}%
wenzelm@29740
  1220
%
wenzelm@29740
  1221
\isadelimnoproof
wenzelm@29740
  1222
\isanewline
wenzelm@29740
  1223
%
wenzelm@29740
  1224
\endisadelimnoproof
wenzelm@29740
  1225
%
wenzelm@29740
  1226
\isadelimproof
wenzelm@29740
  1227
\ \ %
wenzelm@29740
  1228
\endisadelimproof
wenzelm@29740
  1229
%
wenzelm@29740
  1230
\isatagproof
wenzelm@29740
  1231
\isacommand{then}\isamarkupfalse%
wenzelm@29740
  1232
\ \isacommand{have}\isamarkupfalse%
wenzelm@29740
  1233
\ B\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
wenzelm@29740
  1234
%
wenzelm@29740
  1235
\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}
wenzelm@29740
  1236
\isanewline
wenzelm@29740
  1237
\ \ \isacommand{have}\isamarkupfalse%
wenzelm@29740
  1238
\ {\isachardoublequoteopen}{\isasymforall}x{\isachardot}\ B\ x{\isachardoublequoteclose}\isanewline
wenzelm@29740
  1239
\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@29740
  1240
\isanewline
wenzelm@29740
  1241
\ \ \ \ \isacommand{fix}\isamarkupfalse%
wenzelm@29740
  1242
\ x\isanewline
wenzelm@29740
  1243
\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@29740
  1244
\ {\isachardoublequoteopen}B\ x{\isachardoublequoteclose}%
wenzelm@29740
  1245
\endisatagproof
wenzelm@29740
  1246
{\isafoldproof}%
wenzelm@29740
  1247
%
wenzelm@29740
  1248
\isadelimproof
wenzelm@29740
  1249
%
wenzelm@29740
  1250
\endisadelimproof
wenzelm@29740
  1251
%
wenzelm@29740
  1252
\isadelimnoproof
wenzelm@29740
  1253
\ %
wenzelm@29740
  1254
\endisadelimnoproof
wenzelm@29740
  1255
%
wenzelm@29740
  1256
\isatagnoproof
wenzelm@29740
  1257
\isacommand{sorry}\isamarkupfalse%
wenzelm@29740
  1258
%
wenzelm@29740
  1259
\endisatagnoproof
wenzelm@29740
  1260
{\isafoldnoproof}%
wenzelm@29740
  1261
%
wenzelm@29740
  1262
\isadelimnoproof
wenzelm@29740
  1263
\isanewline
wenzelm@29740
  1264
%
wenzelm@29740
  1265
\endisadelimnoproof
wenzelm@29740
  1266
%
wenzelm@29740
  1267
\isadelimproof
wenzelm@29740
  1268
\ \ %
wenzelm@29740
  1269
\endisadelimproof
wenzelm@29740
  1270
%
wenzelm@29740
  1271
\isatagproof
wenzelm@29740
  1272
\isacommand{qed}\isamarkupfalse%
wenzelm@29740
  1273
%
wenzelm@29740
  1274
\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}
wenzelm@29740
  1275
\isanewline
wenzelm@29740
  1276
\ \ \isacommand{have}\isamarkupfalse%
wenzelm@29740
  1277
\ {\isachardoublequoteopen}{\isasymforall}x{\isachardot}\ B\ x{\isachardoublequoteclose}%
wenzelm@29740
  1278
\endisatagproof
wenzelm@29740
  1279
{\isafoldproof}%
wenzelm@29740
  1280
%
wenzelm@29740
  1281
\isadelimproof
wenzelm@29740
  1282
%
wenzelm@29740
  1283
\endisadelimproof
wenzelm@29740
  1284
%
wenzelm@29740
  1285
\isadelimnoproof
wenzelm@29740
  1286
\ %
wenzelm@29740
  1287
\endisadelimnoproof
wenzelm@29740
  1288
%
wenzelm@29740
  1289
\isatagnoproof
wenzelm@29740
  1290
\isacommand{sorry}\isamarkupfalse%
wenzelm@29740
  1291
%
wenzelm@29740
  1292
\endisatagnoproof
wenzelm@29740
  1293
{\isafoldnoproof}%
wenzelm@29740
  1294
%
wenzelm@29740
  1295
\isadelimnoproof
wenzelm@29740
  1296
\isanewline
wenzelm@29740
  1297
%
wenzelm@29740
  1298
\endisadelimnoproof
wenzelm@29740
  1299
%
wenzelm@29740
  1300
\isadelimproof
wenzelm@29740
  1301
\ \ %
wenzelm@29740
  1302
\endisadelimproof
wenzelm@29740
  1303
%
wenzelm@29740
  1304
\isatagproof
wenzelm@29740
  1305
\isacommand{then}\isamarkupfalse%
wenzelm@29740
  1306
\ \isacommand{have}\isamarkupfalse%
wenzelm@29740
  1307
\ {\isachardoublequoteopen}B\ a{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
wenzelm@29740
  1308
%
wenzelm@29740
  1309
\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}
wenzelm@29740
  1310
\isanewline
wenzelm@29740
  1311
\ \ \isacommand{have}\isamarkupfalse%
wenzelm@29740
  1312
\ {\isachardoublequoteopen}{\isasymexists}x{\isachardot}\ B\ x{\isachardoublequoteclose}\isanewline
wenzelm@29740
  1313
\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@29740
  1314
\isanewline
wenzelm@29740
  1315
\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@29740
  1316
\ {\isachardoublequoteopen}B\ a{\isachardoublequoteclose}%
wenzelm@29740
  1317
\endisatagproof
wenzelm@29740
  1318
{\isafoldproof}%
wenzelm@29740
  1319
%
wenzelm@29740
  1320
\isadelimproof
wenzelm@29740
  1321
%
wenzelm@29740
  1322
\endisadelimproof
wenzelm@29740
  1323
%
wenzelm@29740
  1324
\isadelimnoproof
wenzelm@29740
  1325
\ %
wenzelm@29740
  1326
\endisadelimnoproof
wenzelm@29740
  1327
%
wenzelm@29740
  1328
\isatagnoproof
wenzelm@29740
  1329
\isacommand{sorry}\isamarkupfalse%
wenzelm@29740
  1330
%
wenzelm@29740
  1331
\endisatagnoproof
wenzelm@29740
  1332
{\isafoldnoproof}%
wenzelm@29740
  1333
%
wenzelm@29740
  1334
\isadelimnoproof
wenzelm@29740
  1335
\isanewline
wenzelm@29740
  1336
%
wenzelm@29740
  1337
\endisadelimnoproof
wenzelm@29740
  1338
%
wenzelm@29740
  1339
\isadelimproof
wenzelm@29740
  1340
\ \ %
wenzelm@29740
  1341
\endisadelimproof
wenzelm@29740
  1342
%
wenzelm@29740
  1343
\isatagproof
wenzelm@29740
  1344
\isacommand{qed}\isamarkupfalse%
wenzelm@29740
  1345
%
wenzelm@29740
  1346
\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}
wenzelm@29740
  1347
\isanewline
wenzelm@29740
  1348
\ \ \isacommand{have}\isamarkupfalse%
wenzelm@29740
  1349
\ {\isachardoublequoteopen}{\isasymexists}x{\isachardot}\ B\ x{\isachardoublequoteclose}%
wenzelm@29740
  1350
\endisatagproof
wenzelm@29740
  1351
{\isafoldproof}%
wenzelm@29740
  1352
%
wenzelm@29740
  1353
\isadelimproof
wenzelm@29740
  1354
%
wenzelm@29740
  1355
\endisadelimproof
wenzelm@29740
  1356
%
wenzelm@29740
  1357
\isadelimnoproof
wenzelm@29740
  1358
\ %
wenzelm@29740
  1359
\endisadelimnoproof
wenzelm@29740
  1360
%
wenzelm@29740
  1361
\isatagnoproof
wenzelm@29740
  1362
\isacommand{sorry}\isamarkupfalse%
wenzelm@29740
  1363
%
wenzelm@29740
  1364
\endisatagnoproof
wenzelm@29740
  1365
{\isafoldnoproof}%
wenzelm@29740
  1366
%
wenzelm@29740
  1367
\isadelimnoproof
wenzelm@29740
  1368
\isanewline
wenzelm@29740
  1369
%
wenzelm@29740
  1370
\endisadelimnoproof
wenzelm@29740
  1371
%
wenzelm@29740
  1372
\isadelimproof
wenzelm@29740
  1373
\ \ %
wenzelm@29740
  1374
\endisadelimproof
wenzelm@29740
  1375
%
wenzelm@29740
  1376
\isatagproof
wenzelm@29740
  1377
\isacommand{then}\isamarkupfalse%
wenzelm@29740
  1378
\ \isacommand{obtain}\isamarkupfalse%
wenzelm@29740
  1379
\ a\ \isakeyword{where}\ {\isachardoublequoteopen}B\ a{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
wenzelm@29740
  1380
%
wenzelm@29740
  1381
\end{minipage}
wenzelm@29740
  1382
%
wenzelm@29740
  1383
\endisatagproof
wenzelm@29740
  1384
{\isafoldproof}%
wenzelm@29740
  1385
%
wenzelm@29740
  1386
\isadelimproof
wenzelm@29740
  1387
%
wenzelm@29740
  1388
\endisadelimproof
wenzelm@29740
  1389
%
wenzelm@29740
  1390
\begin{isamarkuptext}%
wenzelm@29740
  1391
\bigskip\noindent Of course, these proofs are merely examples.  As
wenzelm@29740
  1392
  sketched in \secref{sec:framework-subproof}, there is a fair amount
wenzelm@29740
  1393
  of flexibility in expressing Pure deductions in Isar.  Here the user
wenzelm@29740
  1394
  is asked to express himself adequately, aiming at proof texts of
wenzelm@29740
  1395
  literary quality.%
wenzelm@29740
  1396
\end{isamarkuptext}%
wenzelm@29740
  1397
\isamarkuptrue%
wenzelm@29740
  1398
%
wenzelm@29731
  1399
\isadelimvisible
wenzelm@29731
  1400
%
wenzelm@29731
  1401
\endisadelimvisible
wenzelm@29731
  1402
%
wenzelm@29731
  1403
\isatagvisible
wenzelm@29731
  1404
\isacommand{end}\isamarkupfalse%
wenzelm@29731
  1405
%
wenzelm@29731
  1406
\endisatagvisible
wenzelm@29731
  1407
{\isafoldvisible}%
wenzelm@29731
  1408
%
wenzelm@29731
  1409
\isadelimvisible
wenzelm@29731
  1410
%
wenzelm@29731
  1411
\endisadelimvisible
wenzelm@29740
  1412
\isanewline
wenzelm@29731
  1413
\end{isabellebody}%
wenzelm@29731
  1414
%%% Local Variables:
wenzelm@29731
  1415
%%% mode: latex
wenzelm@29731
  1416
%%% TeX-master: "root"
wenzelm@29731
  1417
%%% End: