doc-src/IsarOverview/Isar/document/Logic.tex
author wenzelm
Fri Jun 17 18:36:25 2005 +0200 (2005-06-17)
changeset 16459 7efee005e568
parent 15909 5f0c8a3f0226
child 17125 e6a82d1a1829
permissions -rw-r--r--
updated;
     1 %
     2 \begin{isabellebody}%
     3 \def\isabellecontext{Logic}%
     4 \isamarkupfalse%
     5 %
     6 \isamarkupsection{Logic \label{sec:Logic}%
     7 }
     8 \isamarkuptrue%
     9 %
    10 \isamarkupsubsection{Propositional logic%
    11 }
    12 \isamarkuptrue%
    13 %
    14 \isamarkupsubsubsection{Introduction rules%
    15 }
    16 \isamarkuptrue%
    17 %
    18 \begin{isamarkuptext}%
    19 We start with a really trivial toy proof to introduce the basic
    20 features of structured proofs.%
    21 \end{isamarkuptext}%
    22 \isamarkuptrue%
    23 \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ A{\isachardoublequote}\isanewline
    24 \isamarkupfalse%
    25 \isacommand{proof}\ {\isacharparenleft}rule\ impI{\isacharparenright}\isanewline
    26 \ \ \isamarkupfalse%
    27 \isacommand{assume}\ a{\isacharcolon}\ {\isachardoublequote}A{\isachardoublequote}\isanewline
    28 \ \ \isamarkupfalse%
    29 \isacommand{show}\ {\isachardoublequote}A{\isachardoublequote}\ \isamarkupfalse%
    30 \isacommand{by}{\isacharparenleft}rule\ a{\isacharparenright}\isanewline
    31 \isamarkupfalse%
    32 \isacommand{qed}\isamarkupfalse%
    33 %
    34 \begin{isamarkuptext}%
    35 \noindent
    36 The operational reading: the \isakeyword{assume}-\isakeyword{show}
    37 block proves \isa{A\ {\isasymLongrightarrow}\ A} (\isa{a} is a degenerate rule (no
    38 assumptions) that proves \isa{A} outright), which rule
    39 \isa{impI} (\isa{{\isacharparenleft}{\isacharquery}P\ {\isasymLongrightarrow}\ {\isacharquery}Q{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharquery}P\ {\isasymlongrightarrow}\ {\isacharquery}Q}) turns into the desired \isa{A\ {\isasymlongrightarrow}\ A}.  However, this text is much too detailed for comfort. Therefore
    40 Isar implements the following principle: \begin{quote}\em Command
    41 \isakeyword{proof} automatically tries to select an introduction rule
    42 based on the goal and a predefined list of rules.  \end{quote} Here
    43 \isa{impI} is applied automatically:%
    44 \end{isamarkuptext}%
    45 \isamarkuptrue%
    46 \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ A{\isachardoublequote}\isanewline
    47 \isamarkupfalse%
    48 \isacommand{proof}\isanewline
    49 \ \ \isamarkupfalse%
    50 \isacommand{assume}\ a{\isacharcolon}\ A\isanewline
    51 \ \ \isamarkupfalse%
    52 \isacommand{show}\ A\ \isamarkupfalse%
    53 \isacommand{by}{\isacharparenleft}rule\ a{\isacharparenright}\isanewline
    54 \isamarkupfalse%
    55 \isacommand{qed}\isamarkupfalse%
    56 %
    57 \begin{isamarkuptext}%
    58 \noindent Single-identifier formulae such as \isa{A} need not
    59 be enclosed in double quotes. However, we will continue to do so for
    60 uniformity.
    61 
    62 Trivial proofs, in particular those by assumption, should be trivial
    63 to perform. Proof ``.'' does just that (and a bit more). Thus
    64 naming of assumptions is often superfluous:%
    65 \end{isamarkuptext}%
    66 \isamarkuptrue%
    67 \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ A{\isachardoublequote}\isanewline
    68 \isamarkupfalse%
    69 \isacommand{proof}\isanewline
    70 \ \ \isamarkupfalse%
    71 \isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\isanewline
    72 \ \ \isamarkupfalse%
    73 \isacommand{show}\ {\isachardoublequote}A{\isachardoublequote}\ \isamarkupfalse%
    74 \isacommand{{\isachardot}}\isanewline
    75 \isamarkupfalse%
    76 \isacommand{qed}\isamarkupfalse%
    77 %
    78 \begin{isamarkuptext}%
    79 To hide proofs by assumption further, \isakeyword{by}\isa{{\isacharparenleft}method{\isacharparenright}}
    80 first applies \isa{method} and then tries to solve all remaining subgoals
    81 by assumption:%
    82 \end{isamarkuptext}%
    83 \isamarkuptrue%
    84 \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ A\ {\isasymand}\ A{\isachardoublequote}\isanewline
    85 \isamarkupfalse%
    86 \isacommand{proof}\isanewline
    87 \ \ \isamarkupfalse%
    88 \isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\isanewline
    89 \ \ \isamarkupfalse%
    90 \isacommand{show}\ {\isachardoublequote}A\ {\isasymand}\ A{\isachardoublequote}\ \isamarkupfalse%
    91 \isacommand{by}{\isacharparenleft}rule\ conjI{\isacharparenright}\isanewline
    92 \isamarkupfalse%
    93 \isacommand{qed}\isamarkupfalse%
    94 %
    95 \begin{isamarkuptext}%
    96 \noindent Rule \isa{conjI} is of course \isa{{\isasymlbrakk}{\isacharquery}P{\isacharsemicolon}\ {\isacharquery}Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P\ {\isasymand}\ {\isacharquery}Q}.
    97 A drawback of implicit proofs by assumption is that it
    98 is no longer obvious where an assumption is used.
    99 
   100 Proofs of the form \isakeyword{by}\isa{{\isacharparenleft}rule}~\emph{name}\isa{{\isacharparenright}}
   101 can be abbreviated to ``..''  if \emph{name} refers to one of the
   102 predefined introduction rules (or elimination rules, see below):%
   103 \end{isamarkuptext}%
   104 \isamarkuptrue%
   105 \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ A\ {\isasymand}\ A{\isachardoublequote}\isanewline
   106 \isamarkupfalse%
   107 \isacommand{proof}\isanewline
   108 \ \ \isamarkupfalse%
   109 \isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\isanewline
   110 \ \ \isamarkupfalse%
   111 \isacommand{show}\ {\isachardoublequote}A\ {\isasymand}\ A{\isachardoublequote}\ \isamarkupfalse%
   112 \isacommand{{\isachardot}{\isachardot}}\isanewline
   113 \isamarkupfalse%
   114 \isacommand{qed}\isamarkupfalse%
   115 %
   116 \begin{isamarkuptext}%
   117 \noindent
   118 This is what happens: first the matching introduction rule \isa{conjI}
   119 is applied (first ``.''), then the two subgoals are solved by assumption
   120 (second ``.'').%
   121 \end{isamarkuptext}%
   122 \isamarkuptrue%
   123 %
   124 \isamarkupsubsubsection{Elimination rules%
   125 }
   126 \isamarkuptrue%
   127 %
   128 \begin{isamarkuptext}%
   129 A typical elimination rule is \isa{conjE}, $\land$-elimination:
   130 \begin{isabelle}%
   131 \ \ \ \ \ {\isasymlbrakk}{\isacharquery}P\ {\isasymand}\ {\isacharquery}Q{\isacharsemicolon}\ {\isasymlbrakk}{\isacharquery}P{\isacharsemicolon}\ {\isacharquery}Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}R{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}R%
   132 \end{isabelle}  In the following proof it is applied
   133 by hand, after its first (\emph{major}) premise has been eliminated via
   134 \isa{{\isacharbrackleft}OF\ AB{\isacharbrackright}}:%
   135 \end{isamarkuptext}%
   136 \isamarkuptrue%
   137 \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequote}\isanewline
   138 \isamarkupfalse%
   139 \isacommand{proof}\isanewline
   140 \ \ \isamarkupfalse%
   141 \isacommand{assume}\ AB{\isacharcolon}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\isanewline
   142 \ \ \isamarkupfalse%
   143 \isacommand{show}\ {\isachardoublequote}B\ {\isasymand}\ A{\isachardoublequote}\isanewline
   144 \ \ \isamarkupfalse%
   145 \isacommand{proof}\ {\isacharparenleft}rule\ conjE{\isacharbrackleft}OF\ AB{\isacharbrackright}{\isacharparenright}\ \ %
   146 \isamarkupcmt{\isa{conjE{\isacharbrackleft}OF\ AB{\isacharbrackright}}: \isa{{\isacharparenleft}{\isasymlbrakk}A{\isacharsemicolon}\ B{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}R{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharquery}R}%
   147 }
   148 \isanewline
   149 \ \ \ \ \isamarkupfalse%
   150 \isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\ {\isachardoublequote}B{\isachardoublequote}\isanewline
   151 \ \ \ \ \isamarkupfalse%
   152 \isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
   153 \isacommand{{\isachardot}{\isachardot}}\isanewline
   154 \ \ \isamarkupfalse%
   155 \isacommand{qed}\isanewline
   156 \isamarkupfalse%
   157 \isacommand{qed}\isamarkupfalse%
   158 %
   159 \begin{isamarkuptext}%
   160 \noindent Note that the term \isa{{\isacharquery}thesis} always stands for the
   161 ``current goal'', i.e.\ the enclosing \isakeyword{show} (or
   162 \isakeyword{have}) statement.
   163 
   164 This is too much proof text. Elimination rules should be selected
   165 automatically based on their major premise, the formula or rather connective
   166 to be eliminated. In Isar they are triggered by facts being fed
   167 \emph{into} a proof. Syntax:
   168 \begin{center}
   169 \isakeyword{from} \emph{fact} \isakeyword{show} \emph{proposition} \emph{proof}
   170 \end{center}
   171 where \emph{fact} stands for the name of a previously proved
   172 proposition, e.g.\ an assumption, an intermediate result or some global
   173 theorem, which may also be modified with \isa{OF} etc.
   174 The \emph{fact} is ``piped'' into the \emph{proof}, which can deal with it
   175 how it chooses. If the \emph{proof} starts with a plain \isakeyword{proof},
   176 an elimination rule (from a predefined list) is applied
   177 whose first premise is solved by the \emph{fact}. Thus the proof above
   178 is equivalent to the following one:%
   179 \end{isamarkuptext}%
   180 \isamarkuptrue%
   181 \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequote}\isanewline
   182 \isamarkupfalse%
   183 \isacommand{proof}\isanewline
   184 \ \ \isamarkupfalse%
   185 \isacommand{assume}\ AB{\isacharcolon}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\isanewline
   186 \ \ \isamarkupfalse%
   187 \isacommand{from}\ AB\ \isamarkupfalse%
   188 \isacommand{show}\ {\isachardoublequote}B\ {\isasymand}\ A{\isachardoublequote}\isanewline
   189 \ \ \isamarkupfalse%
   190 \isacommand{proof}\isanewline
   191 \ \ \ \ \isamarkupfalse%
   192 \isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\ {\isachardoublequote}B{\isachardoublequote}\isanewline
   193 \ \ \ \ \isamarkupfalse%
   194 \isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
   195 \isacommand{{\isachardot}{\isachardot}}\isanewline
   196 \ \ \isamarkupfalse%
   197 \isacommand{qed}\isanewline
   198 \isamarkupfalse%
   199 \isacommand{qed}\isamarkupfalse%
   200 %
   201 \begin{isamarkuptext}%
   202 Now we come to a second important principle:
   203 \begin{quote}\em
   204 Try to arrange the sequence of propositions in a UNIX-like pipe,
   205 such that the proof of each proposition builds on the previous proposition.
   206 \end{quote}
   207 The previous proposition can be referred to via the fact \isa{this}.
   208 This greatly reduces the need for explicit naming of propositions:%
   209 \end{isamarkuptext}%
   210 \isamarkuptrue%
   211 \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequote}\isanewline
   212 \isamarkupfalse%
   213 \isacommand{proof}\isanewline
   214 \ \ \isamarkupfalse%
   215 \isacommand{assume}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\isanewline
   216 \ \ \isamarkupfalse%
   217 \isacommand{from}\ this\ \isamarkupfalse%
   218 \isacommand{show}\ {\isachardoublequote}B\ {\isasymand}\ A{\isachardoublequote}\isanewline
   219 \ \ \isamarkupfalse%
   220 \isacommand{proof}\isanewline
   221 \ \ \ \ \isamarkupfalse%
   222 \isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\ {\isachardoublequote}B{\isachardoublequote}\isanewline
   223 \ \ \ \ \isamarkupfalse%
   224 \isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
   225 \isacommand{{\isachardot}{\isachardot}}\isanewline
   226 \ \ \isamarkupfalse%
   227 \isacommand{qed}\isanewline
   228 \isamarkupfalse%
   229 \isacommand{qed}\isamarkupfalse%
   230 %
   231 \begin{isamarkuptext}%
   232 \noindent Because of the frequency of \isakeyword{from}~\isa{this}, Isar provides two abbreviations:
   233 \begin{center}
   234 \begin{tabular}{r@ {\quad=\quad}l}
   235 \isakeyword{then} & \isakeyword{from} \isa{this} \\
   236 \isakeyword{thus} & \isakeyword{then} \isakeyword{show}
   237 \end{tabular}
   238 \end{center}
   239 
   240 Here is an alternative proof that operates purely by forward reasoning:%
   241 \end{isamarkuptext}%
   242 \isamarkuptrue%
   243 \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequote}\isanewline
   244 \isamarkupfalse%
   245 \isacommand{proof}\isanewline
   246 \ \ \isamarkupfalse%
   247 \isacommand{assume}\ ab{\isacharcolon}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\isanewline
   248 \ \ \isamarkupfalse%
   249 \isacommand{from}\ ab\ \isamarkupfalse%
   250 \isacommand{have}\ a{\isacharcolon}\ {\isachardoublequote}A{\isachardoublequote}\ \isamarkupfalse%
   251 \isacommand{{\isachardot}{\isachardot}}\isanewline
   252 \ \ \isamarkupfalse%
   253 \isacommand{from}\ ab\ \isamarkupfalse%
   254 \isacommand{have}\ b{\isacharcolon}\ {\isachardoublequote}B{\isachardoublequote}\ \isamarkupfalse%
   255 \isacommand{{\isachardot}{\isachardot}}\isanewline
   256 \ \ \isamarkupfalse%
   257 \isacommand{from}\ b\ a\ \isamarkupfalse%
   258 \isacommand{show}\ {\isachardoublequote}B\ {\isasymand}\ A{\isachardoublequote}\ \isamarkupfalse%
   259 \isacommand{{\isachardot}{\isachardot}}\isanewline
   260 \isamarkupfalse%
   261 \isacommand{qed}\isamarkupfalse%
   262 %
   263 \begin{isamarkuptext}%
   264 \noindent It is worth examining this text in detail because it
   265 exhibits a number of new concepts.  For a start, it is the first time
   266 we have proved intermediate propositions (\isakeyword{have}) on the
   267 way to the final \isakeyword{show}. This is the norm in nontrivial
   268 proofs where one cannot bridge the gap between the assumptions and the
   269 conclusion in one step. To understand how the proof works we need to
   270 explain more Isar details.
   271 
   272 Method \isa{rule} can be given a list of rules, in which case
   273 \isa{{\isacharparenleft}rule}~\textit{rules}\isa{{\isacharparenright}} applies the first matching
   274 rule in the list \textit{rules}. Command \isakeyword{from} can be
   275 followed by any number of facts.  Given \isakeyword{from}~\isa{f}$_1$~\dots~\isa{f}$_n$, the proof step
   276 \isa{{\isacharparenleft}rule}~\textit{rules}\isa{{\isacharparenright}} following a \isakeyword{have}
   277 or \isakeyword{show} searches \textit{rules} for a rule whose first
   278 $n$ premises can be proved by \isa{f}$_1$~\dots~\isa{f}$_n$ in the
   279 given order. Finally one needs to know that ``..'' is short for
   280 \isa{by{\isacharparenleft}rule}~\textit{elim-rules intro-rules}\isa{{\isacharparenright}} (or
   281 \isa{by{\isacharparenleft}rule}~\textit{intro-rules}\isa{{\isacharparenright}} if there are no facts
   282 fed into the proof), i.e.\ elimination rules are tried before
   283 introduction rules.
   284 
   285 Thus in the above proof both \isakeyword{have}s are proved via
   286 \isa{conjE} triggered by \isakeyword{from}~\isa{ab} whereas
   287 in the \isakeyword{show} step no elimination rule is applicable and
   288 the proof succeeds with \isa{conjI}. The latter would fail had
   289 we written \isakeyword{from}~\isa{a\ b} instead of
   290 \isakeyword{from}~\isa{b\ a}.
   291 
   292 Proofs starting with a plain \isa{proof} behave the same because the
   293 latter is short for \isa{proof\ {\isacharparenleft}rule}~\textit{elim-rules
   294 intro-rules}\isa{{\isacharparenright}} (or \isa{proof\ {\isacharparenleft}rule}~\textit{intro-rules}\isa{{\isacharparenright}} if there are no facts fed into
   295 the proof).%
   296 \end{isamarkuptext}%
   297 \isamarkuptrue%
   298 %
   299 \isamarkupsubsection{More constructs%
   300 }
   301 \isamarkuptrue%
   302 %
   303 \begin{isamarkuptext}%
   304 In the previous proof of \isa{A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A} we needed to feed
   305 more than one fact into a proof step, a frequent situation. Then the
   306 UNIX-pipe model appears to break down and we need to name the different
   307 facts to refer to them. But this can be avoided:%
   308 \end{isamarkuptext}%
   309 \isamarkuptrue%
   310 \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequote}\isanewline
   311 \isamarkupfalse%
   312 \isacommand{proof}\isanewline
   313 \ \ \isamarkupfalse%
   314 \isacommand{assume}\ ab{\isacharcolon}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\isanewline
   315 \ \ \isamarkupfalse%
   316 \isacommand{from}\ ab\ \isamarkupfalse%
   317 \isacommand{have}\ {\isachardoublequote}B{\isachardoublequote}\ \isamarkupfalse%
   318 \isacommand{{\isachardot}{\isachardot}}\isanewline
   319 \ \ \isamarkupfalse%
   320 \isacommand{moreover}\isanewline
   321 \ \ \isamarkupfalse%
   322 \isacommand{from}\ ab\ \isamarkupfalse%
   323 \isacommand{have}\ {\isachardoublequote}A{\isachardoublequote}\ \isamarkupfalse%
   324 \isacommand{{\isachardot}{\isachardot}}\isanewline
   325 \ \ \isamarkupfalse%
   326 \isacommand{ultimately}\ \isamarkupfalse%
   327 \isacommand{show}\ {\isachardoublequote}B\ {\isasymand}\ A{\isachardoublequote}\ \isamarkupfalse%
   328 \isacommand{{\isachardot}{\isachardot}}\isanewline
   329 \isamarkupfalse%
   330 \isacommand{qed}\isamarkupfalse%
   331 %
   332 \begin{isamarkuptext}%
   333 \noindent You can combine any number of facts \isa{A{\isadigit{1}}} \dots\ \isa{An} into a sequence by separating their proofs with
   334 \isakeyword{moreover}. After the final fact, \isakeyword{ultimately} stands
   335 for \isakeyword{from}~\isa{A{\isadigit{1}}}~\dots~\isa{An}.  This avoids having to
   336 introduce names for all of the sequence elements.%
   337 \end{isamarkuptext}%
   338 \isamarkuptrue%
   339 %
   340 \begin{isamarkuptext}%
   341 Although we have only seen a few introduction and elimination rules so
   342 far, Isar's predefined rules include all the usual natural deduction
   343 rules. We conclude our exposition of propositional logic with an extended
   344 example --- which rules are used implicitly where?%
   345 \end{isamarkuptext}%
   346 \isamarkuptrue%
   347 \isacommand{lemma}\ {\isachardoublequote}{\isasymnot}\ {\isacharparenleft}A\ {\isasymand}\ B{\isacharparenright}\ {\isasymlongrightarrow}\ {\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ B{\isachardoublequote}\isanewline
   348 \isamarkupfalse%
   349 \isacommand{proof}\isanewline
   350 \ \ \isamarkupfalse%
   351 \isacommand{assume}\ n{\isacharcolon}\ {\isachardoublequote}{\isasymnot}\ {\isacharparenleft}A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isanewline
   352 \ \ \isamarkupfalse%
   353 \isacommand{show}\ {\isachardoublequote}{\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ B{\isachardoublequote}\isanewline
   354 \ \ \isamarkupfalse%
   355 \isacommand{proof}\ {\isacharparenleft}rule\ ccontr{\isacharparenright}\isanewline
   356 \ \ \ \ \isamarkupfalse%
   357 \isacommand{assume}\ nn{\isacharcolon}\ {\isachardoublequote}{\isasymnot}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ B{\isacharparenright}{\isachardoublequote}\isanewline
   358 \ \ \ \ \isamarkupfalse%
   359 \isacommand{have}\ {\isachardoublequote}{\isasymnot}\ A{\isachardoublequote}\isanewline
   360 \ \ \ \ \isamarkupfalse%
   361 \isacommand{proof}\isanewline
   362 \ \ \ \ \ \ \isamarkupfalse%
   363 \isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\isanewline
   364 \ \ \ \ \ \ \isamarkupfalse%
   365 \isacommand{have}\ {\isachardoublequote}{\isasymnot}\ B{\isachardoublequote}\isanewline
   366 \ \ \ \ \ \ \isamarkupfalse%
   367 \isacommand{proof}\isanewline
   368 \ \ \ \ \ \ \ \ \isamarkupfalse%
   369 \isacommand{assume}\ {\isachardoublequote}B{\isachardoublequote}\isanewline
   370 \ \ \ \ \ \ \ \ \isamarkupfalse%
   371 \isacommand{have}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\ \isamarkupfalse%
   372 \isacommand{{\isachardot}{\isachardot}}\isanewline
   373 \ \ \ \ \ \ \ \ \isamarkupfalse%
   374 \isacommand{with}\ n\ \isamarkupfalse%
   375 \isacommand{show}\ False\ \isamarkupfalse%
   376 \isacommand{{\isachardot}{\isachardot}}\isanewline
   377 \ \ \ \ \ \ \isamarkupfalse%
   378 \isacommand{qed}\isanewline
   379 \ \ \ \ \ \ \isamarkupfalse%
   380 \isacommand{hence}\ {\isachardoublequote}{\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ B{\isachardoublequote}\ \isamarkupfalse%
   381 \isacommand{{\isachardot}{\isachardot}}\isanewline
   382 \ \ \ \ \ \ \isamarkupfalse%
   383 \isacommand{with}\ nn\ \isamarkupfalse%
   384 \isacommand{show}\ False\ \isamarkupfalse%
   385 \isacommand{{\isachardot}{\isachardot}}\isanewline
   386 \ \ \ \ \isamarkupfalse%
   387 \isacommand{qed}\isanewline
   388 \ \ \ \ \isamarkupfalse%
   389 \isacommand{hence}\ {\isachardoublequote}{\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ B{\isachardoublequote}\ \isamarkupfalse%
   390 \isacommand{{\isachardot}{\isachardot}}\isanewline
   391 \ \ \ \ \isamarkupfalse%
   392 \isacommand{with}\ nn\ \isamarkupfalse%
   393 \isacommand{show}\ False\ \isamarkupfalse%
   394 \isacommand{{\isachardot}{\isachardot}}\isanewline
   395 \ \ \isamarkupfalse%
   396 \isacommand{qed}\isanewline
   397 \isamarkupfalse%
   398 \isacommand{qed}\isamarkupfalse%
   399 %
   400 \begin{isamarkuptext}%
   401 \noindent
   402 Rule \isa{ccontr} (``classical contradiction'') is
   403 \isa{{\isacharparenleft}{\isasymnot}\ P\ {\isasymLongrightarrow}\ False{\isacharparenright}\ {\isasymLongrightarrow}\ P}.
   404 Apart from demonstrating the strangeness of classical
   405 arguments by contradiction, this example also introduces two new
   406 abbreviations:
   407 \begin{center}
   408 \begin{tabular}{l@ {\quad=\quad}l}
   409 \isakeyword{hence} & \isakeyword{then} \isakeyword{have} \\
   410 \isakeyword{with}~\emph{facts} &
   411 \isakeyword{from}~\emph{facts} \isa{this}
   412 \end{tabular}
   413 \end{center}%
   414 \end{isamarkuptext}%
   415 \isamarkuptrue%
   416 %
   417 \isamarkupsubsection{Avoiding duplication%
   418 }
   419 \isamarkuptrue%
   420 %
   421 \begin{isamarkuptext}%
   422 So far our examples have been a bit unnatural: normally we want to
   423 prove rules expressed with \isa{{\isasymLongrightarrow}}, not \isa{{\isasymlongrightarrow}}. Here is an example:%
   424 \end{isamarkuptext}%
   425 \isamarkuptrue%
   426 \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymand}\ B\ {\isasymLongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequote}\isanewline
   427 \isamarkupfalse%
   428 \isacommand{proof}\isanewline
   429 \ \ \isamarkupfalse%
   430 \isacommand{assume}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\ \isamarkupfalse%
   431 \isacommand{thus}\ {\isachardoublequote}B{\isachardoublequote}\ \isamarkupfalse%
   432 \isacommand{{\isachardot}{\isachardot}}\isanewline
   433 \isamarkupfalse%
   434 \isacommand{next}\isanewline
   435 \ \ \isamarkupfalse%
   436 \isacommand{assume}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\ \isamarkupfalse%
   437 \isacommand{thus}\ {\isachardoublequote}A{\isachardoublequote}\ \isamarkupfalse%
   438 \isacommand{{\isachardot}{\isachardot}}\isanewline
   439 \isamarkupfalse%
   440 \isacommand{qed}\isamarkupfalse%
   441 %
   442 \begin{isamarkuptext}%
   443 \noindent The \isakeyword{proof} always works on the conclusion,
   444 \isa{B\ {\isasymand}\ A} in our case, thus selecting $\land$-introduction. Hence
   445 we must show \isa{B} and \isa{A}; both are proved by
   446 $\land$-elimination and the proofs are separated by \isakeyword{next}:
   447 \begin{description}
   448 \item[\isakeyword{next}] deals with multiple subgoals. For example,
   449 when showing \isa{A\ {\isasymand}\ B} we need to show both \isa{A} and \isa{B}.  Each subgoal is proved separately, in \emph{any} order. The
   450 individual proofs are separated by \isakeyword{next}.  \footnote{Each
   451 \isakeyword{show} must prove one of the pending subgoals.  If a
   452 \isakeyword{show} matches multiple subgoals, e.g.\ if the subgoals
   453 contain ?-variables, the first one is proved. Thus the order in which
   454 the subgoals are proved can matter --- see
   455 \S\ref{sec:CaseDistinction} for an example.}
   456 
   457 Strictly speaking \isakeyword{next} is only required if the subgoals
   458 are proved in different assumption contexts which need to be
   459 separated, which is not the case above. For clarity we
   460 have employed \isakeyword{next} anyway and will continue to do so.
   461 \end{description}
   462 
   463 This is all very well as long as formulae are small. Let us now look at some
   464 devices to avoid repeating (possibly large) formulae. A very general method
   465 is pattern matching:%
   466 \end{isamarkuptext}%
   467 \isamarkuptrue%
   468 \isacommand{lemma}\ {\isachardoublequote}large{\isacharunderscore}A\ {\isasymand}\ large{\isacharunderscore}B\ {\isasymLongrightarrow}\ large{\isacharunderscore}B\ {\isasymand}\ large{\isacharunderscore}A{\isachardoublequote}\isanewline
   469 \ \ \ \ \ \ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequote}{\isacharquery}AB\ {\isasymLongrightarrow}\ {\isacharquery}B\ {\isasymand}\ {\isacharquery}A{\isachardoublequote}{\isacharparenright}\isanewline
   470 \isamarkupfalse%
   471 \isacommand{proof}\isanewline
   472 \ \ \isamarkupfalse%
   473 \isacommand{assume}\ {\isachardoublequote}{\isacharquery}AB{\isachardoublequote}\ \isamarkupfalse%
   474 \isacommand{thus}\ {\isachardoublequote}{\isacharquery}B{\isachardoublequote}\ \isamarkupfalse%
   475 \isacommand{{\isachardot}{\isachardot}}\isanewline
   476 \isamarkupfalse%
   477 \isacommand{next}\isanewline
   478 \ \ \isamarkupfalse%
   479 \isacommand{assume}\ {\isachardoublequote}{\isacharquery}AB{\isachardoublequote}\ \isamarkupfalse%
   480 \isacommand{thus}\ {\isachardoublequote}{\isacharquery}A{\isachardoublequote}\ \isamarkupfalse%
   481 \isacommand{{\isachardot}{\isachardot}}\isanewline
   482 \isamarkupfalse%
   483 \isacommand{qed}\isamarkupfalse%
   484 %
   485 \begin{isamarkuptext}%
   486 \noindent Any formula may be followed by
   487 \isa{{\isacharparenleft}}\isakeyword{is}~\emph{pattern}\isa{{\isacharparenright}} which causes the pattern
   488 to be matched against the formula, instantiating the \isa{{\isacharquery}}-variables in
   489 the pattern. Subsequent uses of these variables in other terms causes
   490 them to be replaced by the terms they stand for.
   491 
   492 We can simplify things even more by stating the theorem by means of the
   493 \isakeyword{assumes} and \isakeyword{shows} elements which allow direct
   494 naming of assumptions:%
   495 \end{isamarkuptext}%
   496 \isamarkuptrue%
   497 \isacommand{lemma}\ \isakeyword{assumes}\ AB{\isacharcolon}\ {\isachardoublequote}large{\isacharunderscore}A\ {\isasymand}\ large{\isacharunderscore}B{\isachardoublequote}\isanewline
   498 \ \ \isakeyword{shows}\ {\isachardoublequote}large{\isacharunderscore}B\ {\isasymand}\ large{\isacharunderscore}A{\isachardoublequote}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequote}{\isacharquery}B\ {\isasymand}\ {\isacharquery}A{\isachardoublequote}{\isacharparenright}\isanewline
   499 \isamarkupfalse%
   500 \isacommand{proof}\isanewline
   501 \ \ \isamarkupfalse%
   502 \isacommand{from}\ AB\ \isamarkupfalse%
   503 \isacommand{show}\ {\isachardoublequote}{\isacharquery}B{\isachardoublequote}\ \isamarkupfalse%
   504 \isacommand{{\isachardot}{\isachardot}}\isanewline
   505 \isamarkupfalse%
   506 \isacommand{next}\isanewline
   507 \ \ \isamarkupfalse%
   508 \isacommand{from}\ AB\ \isamarkupfalse%
   509 \isacommand{show}\ {\isachardoublequote}{\isacharquery}A{\isachardoublequote}\ \isamarkupfalse%
   510 \isacommand{{\isachardot}{\isachardot}}\isanewline
   511 \isamarkupfalse%
   512 \isacommand{qed}\isamarkupfalse%
   513 %
   514 \begin{isamarkuptext}%
   515 \noindent Note the difference between \isa{{\isacharquery}AB}, a term, and
   516 \isa{AB}, a fact.
   517 
   518 Finally we want to start the proof with $\land$-elimination so we
   519 don't have to perform it twice, as above. Here is a slick way to
   520 achieve this:%
   521 \end{isamarkuptext}%
   522 \isamarkuptrue%
   523 \isacommand{lemma}\ \isakeyword{assumes}\ AB{\isacharcolon}\ {\isachardoublequote}large{\isacharunderscore}A\ {\isasymand}\ large{\isacharunderscore}B{\isachardoublequote}\isanewline
   524 \ \ \isakeyword{shows}\ {\isachardoublequote}large{\isacharunderscore}B\ {\isasymand}\ large{\isacharunderscore}A{\isachardoublequote}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequote}{\isacharquery}B\ {\isasymand}\ {\isacharquery}A{\isachardoublequote}{\isacharparenright}\isanewline
   525 \isamarkupfalse%
   526 \isacommand{using}\ AB\isanewline
   527 \isamarkupfalse%
   528 \isacommand{proof}\isanewline
   529 \ \ \isamarkupfalse%
   530 \isacommand{assume}\ {\isachardoublequote}{\isacharquery}A{\isachardoublequote}\ {\isachardoublequote}{\isacharquery}B{\isachardoublequote}\ \isamarkupfalse%
   531 \isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
   532 \isacommand{{\isachardot}{\isachardot}}\isanewline
   533 \isamarkupfalse%
   534 \isacommand{qed}\isamarkupfalse%
   535 %
   536 \begin{isamarkuptext}%
   537 \noindent Command \isakeyword{using} can appear before a proof
   538 and adds further facts to those piped into the proof. Here \isa{AB}
   539 is the only such fact and it triggers $\land$-elimination. Another
   540 frequent idiom is as follows:
   541 \begin{center}
   542 \isakeyword{from} \emph{major-facts}~
   543 \isakeyword{show} \emph{proposition}~
   544 \isakeyword{using} \emph{minor-facts}~
   545 \emph{proof}
   546 \end{center}
   547 
   548 Sometimes it is necessary to suppress the implicit application of rules in a
   549 \isakeyword{proof}. For example \isakeyword{show}~\isa{A\ {\isasymor}\ B} would
   550 trigger $\lor$-introduction, requiring us to prove \isa{A}. A simple
   551 ``\isa{{\isacharminus}}'' prevents this \emph{faux pas}:%
   552 \end{isamarkuptext}%
   553 \isamarkuptrue%
   554 \isacommand{lemma}\ \isakeyword{assumes}\ AB{\isacharcolon}\ {\isachardoublequote}A\ {\isasymor}\ B{\isachardoublequote}\ \isakeyword{shows}\ {\isachardoublequote}B\ {\isasymor}\ A{\isachardoublequote}\isanewline
   555 \isamarkupfalse%
   556 \isacommand{proof}\ {\isacharminus}\isanewline
   557 \ \ \isamarkupfalse%
   558 \isacommand{from}\ AB\ \isamarkupfalse%
   559 \isacommand{show}\ {\isacharquery}thesis\isanewline
   560 \ \ \isamarkupfalse%
   561 \isacommand{proof}\isanewline
   562 \ \ \ \ \isamarkupfalse%
   563 \isacommand{assume}\ A\ \isamarkupfalse%
   564 \isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
   565 \isacommand{{\isachardot}{\isachardot}}\isanewline
   566 \ \ \isamarkupfalse%
   567 \isacommand{next}\isanewline
   568 \ \ \ \ \isamarkupfalse%
   569 \isacommand{assume}\ B\ \isamarkupfalse%
   570 \isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
   571 \isacommand{{\isachardot}{\isachardot}}\isanewline
   572 \ \ \isamarkupfalse%
   573 \isacommand{qed}\isanewline
   574 \isamarkupfalse%
   575 \isacommand{qed}\isamarkupfalse%
   576 %
   577 \isamarkupsubsection{Predicate calculus%
   578 }
   579 \isamarkuptrue%
   580 %
   581 \begin{isamarkuptext}%
   582 Command \isakeyword{fix} introduces new local variables into a
   583 proof. The pair \isakeyword{fix}-\isakeyword{show} corresponds to \isa{{\isasymAnd}}
   584 (the universal quantifier at the
   585 meta-level) just like \isakeyword{assume}-\isakeyword{show} corresponds to
   586 \isa{{\isasymLongrightarrow}}. Here is a sample proof, annotated with the rules that are
   587 applied implicitly:%
   588 \end{isamarkuptext}%
   589 \isamarkuptrue%
   590 \isacommand{lemma}\ \isakeyword{assumes}\ P{\isacharcolon}\ {\isachardoublequote}{\isasymforall}x{\isachardot}\ P\ x{\isachardoublequote}\ \isakeyword{shows}\ {\isachardoublequote}{\isasymforall}x{\isachardot}\ P{\isacharparenleft}f\ x{\isacharparenright}{\isachardoublequote}\isanewline
   591 \isamarkupfalse%
   592 \isacommand{proof}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ %
   593 \isamarkupcmt{\isa{allI}: \isa{{\isacharparenleft}{\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymforall}x{\isachardot}\ {\isacharquery}P\ x}%
   594 }
   595 \isanewline
   596 \ \ \isamarkupfalse%
   597 \isacommand{fix}\ a\isanewline
   598 \ \ \isamarkupfalse%
   599 \isacommand{from}\ P\ \isamarkupfalse%
   600 \isacommand{show}\ {\isachardoublequote}P{\isacharparenleft}f\ a{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse%
   601 \isacommand{{\isachardot}{\isachardot}}\ \ %
   602 \isamarkupcmt{\isa{allE}: \isa{{\isasymlbrakk}{\isasymforall}x{\isachardot}\ {\isacharquery}P\ x{\isacharsemicolon}\ {\isacharquery}P\ {\isacharquery}x\ {\isasymLongrightarrow}\ {\isacharquery}R{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}R}%
   603 }
   604 \isanewline
   605 \isamarkupfalse%
   606 \isacommand{qed}\isamarkupfalse%
   607 %
   608 \begin{isamarkuptext}%
   609 \noindent Note that in the proof we have chosen to call the bound
   610 variable \isa{a} instead of \isa{x} merely to show that the choice of
   611 local names is irrelevant.
   612 
   613 Next we look at \isa{{\isasymexists}} which is a bit more tricky.%
   614 \end{isamarkuptext}%
   615 \isamarkuptrue%
   616 \isacommand{lemma}\ \isakeyword{assumes}\ Pf{\isacharcolon}\ {\isachardoublequote}{\isasymexists}x{\isachardot}\ P{\isacharparenleft}f\ x{\isacharparenright}{\isachardoublequote}\ \isakeyword{shows}\ {\isachardoublequote}{\isasymexists}y{\isachardot}\ P\ y{\isachardoublequote}\isanewline
   617 \isamarkupfalse%
   618 \isacommand{proof}\ {\isacharminus}\isanewline
   619 \ \ \isamarkupfalse%
   620 \isacommand{from}\ Pf\ \isamarkupfalse%
   621 \isacommand{show}\ {\isacharquery}thesis\isanewline
   622 \ \ \isamarkupfalse%
   623 \isacommand{proof}\ \ \ \ \ \ \ \ \ \ \ \ \ \ %
   624 \isamarkupcmt{\isa{exE}: \isa{{\isasymlbrakk}{\isasymexists}x{\isachardot}\ {\isacharquery}P\ x{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x\ {\isasymLongrightarrow}\ {\isacharquery}Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}Q}%
   625 }
   626 \isanewline
   627 \ \ \ \ \isamarkupfalse%
   628 \isacommand{fix}\ x\isanewline
   629 \ \ \ \ \isamarkupfalse%
   630 \isacommand{assume}\ {\isachardoublequote}P{\isacharparenleft}f\ x{\isacharparenright}{\isachardoublequote}\isanewline
   631 \ \ \ \ \isamarkupfalse%
   632 \isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
   633 \isacommand{{\isachardot}{\isachardot}}\ \ %
   634 \isamarkupcmt{\isa{exI}: \isa{{\isacharquery}P\ {\isacharquery}x\ {\isasymLongrightarrow}\ {\isasymexists}x{\isachardot}\ {\isacharquery}P\ x}%
   635 }
   636 \isanewline
   637 \ \ \isamarkupfalse%
   638 \isacommand{qed}\isanewline
   639 \isamarkupfalse%
   640 \isacommand{qed}\isamarkupfalse%
   641 %
   642 \begin{isamarkuptext}%
   643 \noindent Explicit $\exists$-elimination as seen above can become
   644 cumbersome in practice.  The derived Isar language element
   645 \isakeyword{obtain} provides a more appealing form of generalised
   646 existence reasoning:%
   647 \end{isamarkuptext}%
   648 \isamarkuptrue%
   649 \isacommand{lemma}\ \isakeyword{assumes}\ Pf{\isacharcolon}\ {\isachardoublequote}{\isasymexists}x{\isachardot}\ P{\isacharparenleft}f\ x{\isacharparenright}{\isachardoublequote}\ \isakeyword{shows}\ {\isachardoublequote}{\isasymexists}y{\isachardot}\ P\ y{\isachardoublequote}\isanewline
   650 \isamarkupfalse%
   651 \isacommand{proof}\ {\isacharminus}\isanewline
   652 \ \ \isamarkupfalse%
   653 \isacommand{from}\ Pf\ \isamarkupfalse%
   654 \isacommand{obtain}\ x\ \isakeyword{where}\ {\isachardoublequote}P{\isacharparenleft}f\ x{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse%
   655 \isacommand{{\isachardot}{\isachardot}}\isanewline
   656 \ \ \isamarkupfalse%
   657 \isacommand{thus}\ {\isachardoublequote}{\isasymexists}y{\isachardot}\ P\ y{\isachardoublequote}\ \isamarkupfalse%
   658 \isacommand{{\isachardot}{\isachardot}}\isanewline
   659 \isamarkupfalse%
   660 \isacommand{qed}\isamarkupfalse%
   661 %
   662 \begin{isamarkuptext}%
   663 \noindent Note how the proof text follows the usual mathematical style
   664 of concluding $P(x)$ from $\exists x. P(x)$, while carefully introducing $x$
   665 as a new local variable.  Technically, \isakeyword{obtain} is similar to
   666 \isakeyword{fix} and \isakeyword{assume} together with a soundness proof of
   667 the elimination involved.
   668 
   669 Here is a proof of a well known tautology.
   670 Which rule is used where?%
   671 \end{isamarkuptext}%
   672 \isamarkuptrue%
   673 \isacommand{lemma}\ \isakeyword{assumes}\ ex{\isacharcolon}\ {\isachardoublequote}{\isasymexists}x{\isachardot}\ {\isasymforall}y{\isachardot}\ P\ x\ y{\isachardoublequote}\ \isakeyword{shows}\ {\isachardoublequote}{\isasymforall}y{\isachardot}\ {\isasymexists}x{\isachardot}\ P\ x\ y{\isachardoublequote}\isanewline
   674 \isamarkupfalse%
   675 \isacommand{proof}\isanewline
   676 \ \ \isamarkupfalse%
   677 \isacommand{fix}\ y\isanewline
   678 \ \ \isamarkupfalse%
   679 \isacommand{from}\ ex\ \isamarkupfalse%
   680 \isacommand{obtain}\ x\ \isakeyword{where}\ {\isachardoublequote}{\isasymforall}y{\isachardot}\ P\ x\ y{\isachardoublequote}\ \isamarkupfalse%
   681 \isacommand{{\isachardot}{\isachardot}}\isanewline
   682 \ \ \isamarkupfalse%
   683 \isacommand{hence}\ {\isachardoublequote}P\ x\ y{\isachardoublequote}\ \isamarkupfalse%
   684 \isacommand{{\isachardot}{\isachardot}}\isanewline
   685 \ \ \isamarkupfalse%
   686 \isacommand{thus}\ {\isachardoublequote}{\isasymexists}x{\isachardot}\ P\ x\ y{\isachardoublequote}\ \isamarkupfalse%
   687 \isacommand{{\isachardot}{\isachardot}}\isanewline
   688 \isamarkupfalse%
   689 \isacommand{qed}\isamarkupfalse%
   690 %
   691 \isamarkupsubsection{Making bigger steps%
   692 }
   693 \isamarkuptrue%
   694 %
   695 \begin{isamarkuptext}%
   696 So far we have confined ourselves to single step proofs. Of course
   697 powerful automatic methods can be used just as well. Here is an example,
   698 Cantor's theorem that there is no surjective function from a set to its
   699 powerset:%
   700 \end{isamarkuptext}%
   701 \isamarkuptrue%
   702 \isacommand{theorem}\ {\isachardoublequote}{\isasymexists}S{\isachardot}\ S\ {\isasymnotin}\ range\ {\isacharparenleft}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isacharparenright}{\isachardoublequote}\isanewline
   703 \isamarkupfalse%
   704 \isacommand{proof}\isanewline
   705 \ \ \isamarkupfalse%
   706 \isacommand{let}\ {\isacharquery}S\ {\isacharequal}\ {\isachardoublequote}{\isacharbraceleft}x{\isachardot}\ x\ {\isasymnotin}\ f\ x{\isacharbraceright}{\isachardoublequote}\isanewline
   707 \ \ \isamarkupfalse%
   708 \isacommand{show}\ {\isachardoublequote}{\isacharquery}S\ {\isasymnotin}\ range\ f{\isachardoublequote}\isanewline
   709 \ \ \isamarkupfalse%
   710 \isacommand{proof}\isanewline
   711 \ \ \ \ \isamarkupfalse%
   712 \isacommand{assume}\ {\isachardoublequote}{\isacharquery}S\ {\isasymin}\ range\ f{\isachardoublequote}\isanewline
   713 \ \ \ \ \isamarkupfalse%
   714 \isacommand{then}\ \isamarkupfalse%
   715 \isacommand{obtain}\ y\ \isakeyword{where}\ fy{\isacharcolon}\ {\isachardoublequote}{\isacharquery}S\ {\isacharequal}\ f\ y{\isachardoublequote}\ \isamarkupfalse%
   716 \isacommand{{\isachardot}{\isachardot}}\isanewline
   717 \ \ \ \ \isamarkupfalse%
   718 \isacommand{show}\ False\isanewline
   719 \ \ \ \ \isamarkupfalse%
   720 \isacommand{proof}\ cases\isanewline
   721 \ \ \ \ \ \ \isamarkupfalse%
   722 \isacommand{assume}\ {\isachardoublequote}y\ {\isasymin}\ {\isacharquery}S{\isachardoublequote}\isanewline
   723 \ \ \ \ \ \ \isamarkupfalse%
   724 \isacommand{with}\ fy\ \isamarkupfalse%
   725 \isacommand{show}\ False\ \isamarkupfalse%
   726 \isacommand{by}\ blast\isanewline
   727 \ \ \ \ \isamarkupfalse%
   728 \isacommand{next}\isanewline
   729 \ \ \ \ \ \ \isamarkupfalse%
   730 \isacommand{assume}\ {\isachardoublequote}y\ {\isasymnotin}\ {\isacharquery}S{\isachardoublequote}\isanewline
   731 \ \ \ \ \ \ \isamarkupfalse%
   732 \isacommand{with}\ fy\ \isamarkupfalse%
   733 \isacommand{show}\ False\ \isamarkupfalse%
   734 \isacommand{by}\ blast\isanewline
   735 \ \ \ \ \isamarkupfalse%
   736 \isacommand{qed}\isanewline
   737 \ \ \isamarkupfalse%
   738 \isacommand{qed}\isanewline
   739 \isamarkupfalse%
   740 \isacommand{qed}\isamarkupfalse%
   741 %
   742 \begin{isamarkuptext}%
   743 \noindent
   744 For a start, the example demonstrates two new constructs:
   745 \begin{itemize}
   746 \item \isakeyword{let} introduces an abbreviation for a term, in our case
   747 the witness for the claim.
   748 \item Proof by \isa{cases} starts a proof by cases. Note that it remains
   749 implicit what the two cases are: it is merely expected that the two subproofs
   750 prove \isa{P\ {\isasymLongrightarrow}\ {\isacharquery}thesis} and \isa{{\isasymnot}P\ {\isasymLongrightarrow}\ {\isacharquery}thesis} (in that order)
   751 for some \isa{P}.
   752 \end{itemize}
   753 If you wonder how to \isakeyword{obtain} \isa{y}:
   754 via the predefined elimination rule \isa{{\isasymlbrakk}b\ {\isasymin}\ range\ f{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ b\ {\isacharequal}\ f\ x\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P}.
   755 
   756 Method \isa{blast} is used because the contradiction does not follow easily
   757 by just a single rule. If you find the proof too cryptic for human
   758 consumption, here is a more detailed version; the beginning up to
   759 \isakeyword{obtain} stays unchanged.%
   760 \end{isamarkuptext}%
   761 \isamarkuptrue%
   762 \isacommand{theorem}\ {\isachardoublequote}{\isasymexists}S{\isachardot}\ S\ {\isasymnotin}\ range\ {\isacharparenleft}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isacharparenright}{\isachardoublequote}\isanewline
   763 \isamarkupfalse%
   764 \isacommand{proof}\isanewline
   765 \ \ \isamarkupfalse%
   766 \isacommand{let}\ {\isacharquery}S\ {\isacharequal}\ {\isachardoublequote}{\isacharbraceleft}x{\isachardot}\ x\ {\isasymnotin}\ f\ x{\isacharbraceright}{\isachardoublequote}\isanewline
   767 \ \ \isamarkupfalse%
   768 \isacommand{show}\ {\isachardoublequote}{\isacharquery}S\ {\isasymnotin}\ range\ f{\isachardoublequote}\isanewline
   769 \ \ \isamarkupfalse%
   770 \isacommand{proof}\isanewline
   771 \ \ \ \ \isamarkupfalse%
   772 \isacommand{assume}\ {\isachardoublequote}{\isacharquery}S\ {\isasymin}\ range\ f{\isachardoublequote}\isanewline
   773 \ \ \ \ \isamarkupfalse%
   774 \isacommand{then}\ \isamarkupfalse%
   775 \isacommand{obtain}\ y\ \isakeyword{where}\ fy{\isacharcolon}\ {\isachardoublequote}{\isacharquery}S\ {\isacharequal}\ f\ y{\isachardoublequote}\ \isamarkupfalse%
   776 \isacommand{{\isachardot}{\isachardot}}\isanewline
   777 \ \ \ \ \isamarkupfalse%
   778 \isacommand{show}\ False\isanewline
   779 \ \ \ \ \isamarkupfalse%
   780 \isacommand{proof}\ cases\isanewline
   781 \ \ \ \ \ \ \isamarkupfalse%
   782 \isacommand{assume}\ {\isachardoublequote}y\ {\isasymin}\ {\isacharquery}S{\isachardoublequote}\isanewline
   783 \ \ \ \ \ \ \isamarkupfalse%
   784 \isacommand{hence}\ {\isachardoublequote}y\ {\isasymnotin}\ f\ y{\isachardoublequote}\ \ \ \isamarkupfalse%
   785 \isacommand{by}\ simp\isanewline
   786 \ \ \ \ \ \ \isamarkupfalse%
   787 \isacommand{hence}\ {\isachardoublequote}y\ {\isasymnotin}\ {\isacharquery}S{\isachardoublequote}\ \ \ \ \isamarkupfalse%
   788 \isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}fy{\isacharparenright}\isanewline
   789 \ \ \ \ \ \ \isamarkupfalse%
   790 \isacommand{thus}\ False\ \ \ \ \ \ \ \ \ \isamarkupfalse%
   791 \isacommand{by}\ contradiction\isanewline
   792 \ \ \ \ \isamarkupfalse%
   793 \isacommand{next}\isanewline
   794 \ \ \ \ \ \ \isamarkupfalse%
   795 \isacommand{assume}\ {\isachardoublequote}y\ {\isasymnotin}\ {\isacharquery}S{\isachardoublequote}\isanewline
   796 \ \ \ \ \ \ \isamarkupfalse%
   797 \isacommand{hence}\ {\isachardoublequote}y\ {\isasymin}\ f\ y{\isachardoublequote}\ \ \ \isamarkupfalse%
   798 \isacommand{by}\ simp\isanewline
   799 \ \ \ \ \ \ \isamarkupfalse%
   800 \isacommand{hence}\ {\isachardoublequote}y\ {\isasymin}\ {\isacharquery}S{\isachardoublequote}\ \ \ \ \isamarkupfalse%
   801 \isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}fy{\isacharparenright}\isanewline
   802 \ \ \ \ \ \ \isamarkupfalse%
   803 \isacommand{thus}\ False\ \ \ \ \ \ \ \ \ \isamarkupfalse%
   804 \isacommand{by}\ contradiction\isanewline
   805 \ \ \ \ \isamarkupfalse%
   806 \isacommand{qed}\isanewline
   807 \ \ \isamarkupfalse%
   808 \isacommand{qed}\isanewline
   809 \isamarkupfalse%
   810 \isacommand{qed}\isamarkupfalse%
   811 %
   812 \begin{isamarkuptext}%
   813 \noindent Method \isa{contradiction} succeeds if both $P$ and
   814 $\neg P$ are among the assumptions and the facts fed into that step, in any order.
   815 
   816 As it happens, Cantor's theorem can be proved automatically by best-first
   817 search. Depth-first search would diverge, but best-first search successfully
   818 navigates through the large search space:%
   819 \end{isamarkuptext}%
   820 \isamarkuptrue%
   821 \isacommand{theorem}\ {\isachardoublequote}{\isasymexists}S{\isachardot}\ S\ {\isasymnotin}\ range\ {\isacharparenleft}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isacharparenright}{\isachardoublequote}\isanewline
   822 \isamarkupfalse%
   823 \isacommand{by}\ best\isamarkupfalse%
   824 %
   825 \isamarkupsubsection{Raw proof blocks%
   826 }
   827 \isamarkuptrue%
   828 %
   829 \begin{isamarkuptext}%
   830 Although we have shown how to employ powerful automatic methods like
   831 \isa{blast} to achieve bigger proof steps, there may still be the
   832 tendency to use the default introduction and elimination rules to
   833 decompose goals and facts. This can lead to very tedious proofs:%
   834 \end{isamarkuptext}%
   835 \isamarkuptrue%
   836 \isamarkupfalse%
   837 \isacommand{lemma}\ {\isachardoublequote}{\isasymforall}x\ y{\isachardot}\ A\ x\ y\ {\isasymand}\ B\ x\ y\ {\isasymlongrightarrow}\ C\ x\ y{\isachardoublequote}\isanewline
   838 \isamarkupfalse%
   839 \isacommand{proof}\isanewline
   840 \ \ \isamarkupfalse%
   841 \isacommand{fix}\ x\ \isamarkupfalse%
   842 \isacommand{show}\ {\isachardoublequote}{\isasymforall}y{\isachardot}\ A\ x\ y\ {\isasymand}\ B\ x\ y\ {\isasymlongrightarrow}\ C\ x\ y{\isachardoublequote}\isanewline
   843 \ \ \isamarkupfalse%
   844 \isacommand{proof}\isanewline
   845 \ \ \ \ \isamarkupfalse%
   846 \isacommand{fix}\ y\ \isamarkupfalse%
   847 \isacommand{show}\ {\isachardoublequote}A\ x\ y\ {\isasymand}\ B\ x\ y\ {\isasymlongrightarrow}\ C\ x\ y{\isachardoublequote}\isanewline
   848 \ \ \ \ \isamarkupfalse%
   849 \isacommand{proof}\isanewline
   850 \ \ \ \ \ \ \isamarkupfalse%
   851 \isacommand{assume}\ {\isachardoublequote}A\ x\ y\ {\isasymand}\ B\ x\ y{\isachardoublequote}\isanewline
   852 \ \ \ \ \ \ \isamarkupfalse%
   853 \isacommand{show}\ {\isachardoublequote}C\ x\ y{\isachardoublequote}\ \isamarkupfalse%
   854 \isacommand{sorry}\isanewline
   855 \ \ \ \ \isamarkupfalse%
   856 \isacommand{qed}\isanewline
   857 \ \ \isamarkupfalse%
   858 \isacommand{qed}\isanewline
   859 \isamarkupfalse%
   860 \isacommand{qed}\isamarkupfalse%
   861 %
   862 \begin{isamarkuptext}%
   863 \noindent Since we are only interested in the decomposition and not the
   864 actual proof, the latter has been replaced by
   865 \isakeyword{sorry}. Command \isakeyword{sorry} proves anything but is
   866 only allowed in quick and dirty mode, the default interactive mode. It
   867 is very convenient for top down proof development.
   868 
   869 Luckily we can avoid this step by step decomposition very easily:%
   870 \end{isamarkuptext}%
   871 \isamarkuptrue%
   872 \isacommand{lemma}\ {\isachardoublequote}{\isasymforall}x\ y{\isachardot}\ A\ x\ y\ {\isasymand}\ B\ x\ y\ {\isasymlongrightarrow}\ C\ x\ y{\isachardoublequote}\isanewline
   873 \isamarkupfalse%
   874 \isacommand{proof}\ {\isacharminus}\isanewline
   875 \ \ \isamarkupfalse%
   876 \isacommand{have}\ {\isachardoublequote}{\isasymAnd}x\ y{\isachardot}\ {\isasymlbrakk}\ A\ x\ y{\isacharsemicolon}\ B\ x\ y\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ C\ x\ y{\isachardoublequote}\isanewline
   877 \ \ \isamarkupfalse%
   878 \isacommand{proof}\ {\isacharminus}\isanewline
   879 \ \ \ \ \isamarkupfalse%
   880 \isacommand{fix}\ x\ y\ \isamarkupfalse%
   881 \isacommand{assume}\ {\isachardoublequote}A\ x\ y{\isachardoublequote}\ {\isachardoublequote}B\ x\ y{\isachardoublequote}\isanewline
   882 \ \ \ \ \isamarkupfalse%
   883 \isacommand{show}\ {\isachardoublequote}C\ x\ y{\isachardoublequote}\ \isamarkupfalse%
   884 \isacommand{sorry}\isanewline
   885 \ \ \isamarkupfalse%
   886 \isacommand{qed}\isanewline
   887 \ \ \isamarkupfalse%
   888 \isacommand{thus}\ {\isacharquery}thesis\ \isamarkupfalse%
   889 \isacommand{by}\ blast\isanewline
   890 \isamarkupfalse%
   891 \isacommand{qed}\isamarkupfalse%
   892 %
   893 \begin{isamarkuptext}%
   894 \noindent
   895 This can be simplified further by \emph{raw proof blocks}, i.e.\
   896 proofs enclosed in braces:%
   897 \end{isamarkuptext}%
   898 \isamarkuptrue%
   899 \isacommand{lemma}\ {\isachardoublequote}{\isasymforall}x\ y{\isachardot}\ A\ x\ y\ {\isasymand}\ B\ x\ y\ {\isasymlongrightarrow}\ C\ x\ y{\isachardoublequote}\isanewline
   900 \isamarkupfalse%
   901 \isacommand{proof}\ {\isacharminus}\isanewline
   902 \ \ \isamarkupfalse%
   903 \isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
   904 \isacommand{fix}\ x\ y\ \isamarkupfalse%
   905 \isacommand{assume}\ {\isachardoublequote}A\ x\ y{\isachardoublequote}\ {\isachardoublequote}B\ x\ y{\isachardoublequote}\isanewline
   906 \ \ \ \ \isamarkupfalse%
   907 \isacommand{have}\ {\isachardoublequote}C\ x\ y{\isachardoublequote}\ \isamarkupfalse%
   908 \isacommand{sorry}\ \isamarkupfalse%
   909 \isacommand{{\isacharbraceright}}\isanewline
   910 \ \ \isamarkupfalse%
   911 \isacommand{thus}\ {\isacharquery}thesis\ \isamarkupfalse%
   912 \isacommand{by}\ blast\isanewline
   913 \isamarkupfalse%
   914 \isacommand{qed}\isamarkupfalse%
   915 %
   916 \begin{isamarkuptext}%
   917 \noindent The result of the raw proof block is the same theorem
   918 as above, namely \isa{{\isasymAnd}x\ y{\isachardot}\ {\isasymlbrakk}A\ x\ y{\isacharsemicolon}\ B\ x\ y{\isasymrbrakk}\ {\isasymLongrightarrow}\ C\ x\ y}.  Raw
   919 proof blocks are like ordinary proofs except that they do not prove
   920 some explicitly stated property but that the property emerges directly
   921 out of the \isakeyword{fixe}s, \isakeyword{assume}s and
   922 \isakeyword{have} in the block. Thus they again serve to avoid
   923 duplication. Note that the conclusion of a raw proof block is stated with
   924 \isakeyword{have} rather than \isakeyword{show} because it is not the
   925 conclusion of some pending goal but some independent claim.
   926 
   927 The general idea demonstrated in this subsection is very
   928 important in Isar and distinguishes it from tactic-style proofs:
   929 \begin{quote}\em
   930 Do not manipulate the proof state into a particular form by applying
   931 tactics but state the desired form explicitly and let the tactic verify
   932 that from this form the original goal follows.
   933 \end{quote}
   934 This yields more readable and also more robust proofs.
   935 
   936 \subsubsection{General case distinctions}
   937 
   938 As an important application of raw proof blocks we show how to deal
   939 with general case distinctions --- more specific kinds are treated in
   940 \S\ref{sec:CaseDistinction}. Imagine that you would like to prove some
   941 goal by distinguishing $n$ cases $P_1$, \dots, $P_n$. You show that
   942 the $n$ cases are exhaustive (i.e.\ $P_1 \lor \dots \lor P_n$) and
   943 that each case $P_i$ implies the goal. Taken together, this proves the
   944 goal. The corresponding Isar proof pattern (for $n = 3$) is very handy:%
   945 \end{isamarkuptext}%
   946 \isamarkuptrue%
   947 %
   948 \renewcommand{\isamarkupcmt}[1]{#1}
   949 \isamarkupfalse%
   950 \isacommand{proof}\ {\isacharminus}\isanewline
   951 \ \ \isamarkupfalse%
   952 \isacommand{have}\ {\isachardoublequote}P\isactrlisub {\isadigit{1}}\ {\isasymor}\ P\isactrlisub {\isadigit{2}}\ {\isasymor}\ P\isactrlisub {\isadigit{3}}{\isachardoublequote}\ \isamarkupfalse%
   953 \ %
   954 \isamarkupcmt{\dots%
   955 }
   956 \isanewline
   957 \ \ \isamarkupfalse%
   958 \isacommand{moreover}\isanewline
   959 \ \ \isamarkupfalse%
   960 \isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
   961 \isacommand{assume}\ P\isactrlisub {\isadigit{1}}\isanewline
   962 \ \ \ \ %
   963 \isamarkupcmt{\dots%
   964 }
   965 \isanewline
   966 \ \ \ \ \isamarkupfalse%
   967 \isacommand{have}\ {\isacharquery}thesis\ \isamarkupfalse%
   968 \ %
   969 \isamarkupcmt{\dots%
   970 }
   971 \ \isamarkupfalse%
   972 \isacommand{{\isacharbraceright}}\isanewline
   973 \ \ \isamarkupfalse%
   974 \isacommand{moreover}\isanewline
   975 \ \ \isamarkupfalse%
   976 \isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
   977 \isacommand{assume}\ P\isactrlisub {\isadigit{2}}\isanewline
   978 \ \ \ \ %
   979 \isamarkupcmt{\dots%
   980 }
   981 \isanewline
   982 \ \ \ \ \isamarkupfalse%
   983 \isacommand{have}\ {\isacharquery}thesis\ \isamarkupfalse%
   984 \ %
   985 \isamarkupcmt{\dots%
   986 }
   987 \ \isamarkupfalse%
   988 \isacommand{{\isacharbraceright}}\isanewline
   989 \ \ \isamarkupfalse%
   990 \isacommand{moreover}\isanewline
   991 \ \ \isamarkupfalse%
   992 \isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
   993 \isacommand{assume}\ P\isactrlisub {\isadigit{3}}\isanewline
   994 \ \ \ \ %
   995 \isamarkupcmt{\dots%
   996 }
   997 \isanewline
   998 \ \ \ \ \isamarkupfalse%
   999 \isacommand{have}\ {\isacharquery}thesis\ \isamarkupfalse%
  1000 \ %
  1001 \isamarkupcmt{\dots%
  1002 }
  1003 \ \isamarkupfalse%
  1004 \isacommand{{\isacharbraceright}}\isanewline
  1005 \ \ \isamarkupfalse%
  1006 \isacommand{ultimately}\ \isamarkupfalse%
  1007 \isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
  1008 \isacommand{by}\ blast\isanewline
  1009 \isamarkupfalse%
  1010 \isacommand{qed}\isamarkupfalse%
  1011 %
  1012 \renewcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
  1013 %
  1014 \isamarkupsubsection{Further refinements%
  1015 }
  1016 \isamarkuptrue%
  1017 %
  1018 \begin{isamarkuptext}%
  1019 This subsection discusses some further tricks that can make
  1020 life easier although they are not essential.%
  1021 \end{isamarkuptext}%
  1022 \isamarkuptrue%
  1023 %
  1024 \isamarkupsubsubsection{\isakeyword{and}%
  1025 }
  1026 \isamarkuptrue%
  1027 %
  1028 \begin{isamarkuptext}%
  1029 Propositions (following \isakeyword{assume} etc) may but need not be
  1030 separated by \isakeyword{and}. This is not just for readability
  1031 (\isakeyword{from} \isa{A} \isakeyword{and} \isa{B} looks nicer than
  1032 \isakeyword{from} \isa{A} \isa{B}) but for structuring lists of propositions
  1033 into possibly named blocks. In
  1034 \begin{center}
  1035 \isakeyword{assume} \isa{A:} $A_1$ $A_2$ \isakeyword{and} \isa{B:} $A_3$
  1036 \isakeyword{and} $A_4$
  1037 \end{center}
  1038 label \isa{A} refers to the list of propositions $A_1$ $A_2$ and
  1039 label \isa{B} to $A_3$.%
  1040 \end{isamarkuptext}%
  1041 \isamarkuptrue%
  1042 %
  1043 \isamarkupsubsubsection{\isakeyword{note}%
  1044 }
  1045 \isamarkuptrue%
  1046 %
  1047 \begin{isamarkuptext}%
  1048 If you want to remember intermediate fact(s) that cannot be
  1049 named directly, use \isakeyword{note}. For example the result of raw
  1050 proof block can be named by following it with
  1051 \isakeyword{note}~\isa{some{\isacharunderscore}name\ {\isacharequal}\ this}.  As a side effect,
  1052 \isa{this} is set to the list of facts on the right-hand side. You
  1053 can also say \isa{note\ some{\isacharunderscore}fact}, which simply sets \isa{this},
  1054 i.e.\ recalls \isa{some{\isacharunderscore}fact}, e.g.\ in a \isakeyword{moreover} sequence.%
  1055 \end{isamarkuptext}%
  1056 \isamarkuptrue%
  1057 %
  1058 \isamarkupsubsubsection{\isakeyword{fixes}%
  1059 }
  1060 \isamarkuptrue%
  1061 %
  1062 \begin{isamarkuptext}%
  1063 Sometimes it is necessary to decorate a proposition with type
  1064 constraints, as in Cantor's theorem above. These type constraints tend
  1065 to make the theorem less readable. The situation can be improved a
  1066 little by combining the type constraint with an outer \isa{{\isasymAnd}}:%
  1067 \end{isamarkuptext}%
  1068 \isamarkuptrue%
  1069 \isacommand{theorem}\ {\isachardoublequote}{\isasymAnd}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isachardot}\ {\isasymexists}S{\isachardot}\ S\ {\isasymnotin}\ range\ f{\isachardoublequote}\isamarkupfalse%
  1070 \isamarkupfalse%
  1071 %
  1072 \begin{isamarkuptext}%
  1073 \noindent However, now \isa{f} is bound and we need a
  1074 \isakeyword{fix}~\isa{f} in the proof before we can refer to \isa{f}.
  1075 This is avoided by \isakeyword{fixes}:%
  1076 \end{isamarkuptext}%
  1077 \isamarkuptrue%
  1078 \isacommand{theorem}\ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isachardoublequote}\ \isakeyword{shows}\ {\isachardoublequote}{\isasymexists}S{\isachardot}\ S\ {\isasymnotin}\ range\ f{\isachardoublequote}\isamarkupfalse%
  1079 \isamarkupfalse%
  1080 %
  1081 \begin{isamarkuptext}%
  1082 \noindent
  1083 Even better, \isakeyword{fixes} allows to introduce concrete syntax locally:%
  1084 \end{isamarkuptext}%
  1085 \isamarkuptrue%
  1086 \isacommand{lemma}\ comm{\isacharunderscore}mono{\isacharcolon}\isanewline
  1087 \ \ \isakeyword{fixes}\ r\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequote}\ {\isacharparenleft}\isakeyword{infix}\ {\isachardoublequote}{\isachargreater}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{and}\isanewline
  1088 \ \ \ \ \ \ \ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isacharplus}{\isacharplus}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
  1089 \ \ \isakeyword{assumes}\ comm{\isacharcolon}\ {\isachardoublequote}{\isasymAnd}x\ y{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isachardot}\ x\ {\isacharplus}{\isacharplus}\ y\ {\isacharequal}\ y\ {\isacharplus}{\isacharplus}\ x{\isachardoublequote}\ \isakeyword{and}\isanewline
  1090 \ \ \ \ \ \ \ \ \ \ mono{\isacharcolon}\ {\isachardoublequote}{\isasymAnd}x\ y\ z{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isachardot}\ x\ {\isachargreater}\ y\ {\isasymLongrightarrow}\ x\ {\isacharplus}{\isacharplus}\ z\ {\isachargreater}\ y\ {\isacharplus}{\isacharplus}\ z{\isachardoublequote}\isanewline
  1091 \ \ \isakeyword{shows}\ {\isachardoublequote}x\ {\isachargreater}\ y\ {\isasymLongrightarrow}\ z\ {\isacharplus}{\isacharplus}\ x\ {\isachargreater}\ z\ {\isacharplus}{\isacharplus}\ y{\isachardoublequote}\isanewline
  1092 \isamarkupfalse%
  1093 \isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ comm\ mono{\isacharparenright}\isamarkupfalse%
  1094 %
  1095 \begin{isamarkuptext}%
  1096 \noindent The concrete syntax is dropped at the end of the proof and the
  1097 theorem becomes \begin{isabelle}%
  1098 {\isasymlbrakk}{\isasymAnd}x\ y{\isachardot}\ {\isacharquery}f\ x\ y\ {\isacharequal}\ {\isacharquery}f\ y\ x{\isacharsemicolon}\isanewline
  1099 \isaindent{\ }{\isasymAnd}x\ y\ z{\isachardot}\ {\isacharquery}r\ x\ y\ {\isasymLongrightarrow}\ {\isacharquery}r\ {\isacharparenleft}{\isacharquery}f\ x\ z{\isacharparenright}\ {\isacharparenleft}{\isacharquery}f\ y\ z{\isacharparenright}{\isacharsemicolon}\ {\isacharquery}r\ {\isacharquery}x\ {\isacharquery}y{\isasymrbrakk}\isanewline
  1100 {\isasymLongrightarrow}\ {\isacharquery}r\ {\isacharparenleft}{\isacharquery}f\ {\isacharquery}z\ {\isacharquery}x{\isacharparenright}\ {\isacharparenleft}{\isacharquery}f\ {\isacharquery}z\ {\isacharquery}y{\isacharparenright}%
  1101 \end{isabelle}
  1102 \tweakskip%
  1103 \end{isamarkuptext}%
  1104 \isamarkuptrue%
  1105 %
  1106 \isamarkupsubsubsection{\isakeyword{obtain}%
  1107 }
  1108 \isamarkuptrue%
  1109 %
  1110 \begin{isamarkuptext}%
  1111 The \isakeyword{obtain} construct can introduce multiple
  1112 witnesses and propositions as in the following proof fragment:%
  1113 \end{isamarkuptext}%
  1114 \isamarkuptrue%
  1115 \isacommand{lemma}\ \isakeyword{assumes}\ A{\isacharcolon}\ {\isachardoublequote}{\isasymexists}x\ y{\isachardot}\ P\ x\ y\ {\isasymand}\ Q\ x\ y{\isachardoublequote}\ \isakeyword{shows}\ {\isachardoublequote}R{\isachardoublequote}\isanewline
  1116 \isamarkupfalse%
  1117 \isacommand{proof}\ {\isacharminus}\isanewline
  1118 \ \ \isamarkupfalse%
  1119 \isacommand{from}\ A\ \isamarkupfalse%
  1120 \isacommand{obtain}\ x\ y\ \isakeyword{where}\ P{\isacharcolon}\ {\isachardoublequote}P\ x\ y{\isachardoublequote}\ \isakeyword{and}\ Q{\isacharcolon}\ {\isachardoublequote}Q\ x\ y{\isachardoublequote}\ \ \isamarkupfalse%
  1121 \isacommand{by}\ blast\isamarkupfalse%
  1122 \isamarkupfalse%
  1123 %
  1124 \begin{isamarkuptext}%
  1125 Remember also that one does not even need to start with a formula
  1126 containing \isa{{\isasymexists}} as we saw in the proof of Cantor's theorem.%
  1127 \end{isamarkuptext}%
  1128 \isamarkuptrue%
  1129 %
  1130 \isamarkupsubsubsection{Combining proof styles%
  1131 }
  1132 \isamarkuptrue%
  1133 %
  1134 \begin{isamarkuptext}%
  1135 Finally, whole ``scripts'' (tactic-based proofs in the style of
  1136 \cite{LNCS2283}) may appear in the leaves of the proof tree, although this is
  1137 best avoided.  Here is a contrived example:%
  1138 \end{isamarkuptext}%
  1139 \isamarkuptrue%
  1140 \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ {\isacharparenleft}A\ {\isasymlongrightarrow}\ B{\isacharparenright}\ {\isasymlongrightarrow}\ B{\isachardoublequote}\isanewline
  1141 \isamarkupfalse%
  1142 \isacommand{proof}\isanewline
  1143 \ \ \isamarkupfalse%
  1144 \isacommand{assume}\ a{\isacharcolon}\ {\isachardoublequote}A{\isachardoublequote}\isanewline
  1145 \ \ \isamarkupfalse%
  1146 \isacommand{show}\ {\isachardoublequote}{\isacharparenleft}A\ {\isasymlongrightarrow}B{\isacharparenright}\ {\isasymlongrightarrow}\ B{\isachardoublequote}\isanewline
  1147 \ \ \ \ \isamarkupfalse%
  1148 \isacommand{apply}{\isacharparenleft}rule\ impI{\isacharparenright}\isanewline
  1149 \ \ \ \ \isamarkupfalse%
  1150 \isacommand{apply}{\isacharparenleft}erule\ impE{\isacharparenright}\isanewline
  1151 \ \ \ \ \isamarkupfalse%
  1152 \isacommand{apply}{\isacharparenleft}rule\ a{\isacharparenright}\isanewline
  1153 \ \ \ \ \isamarkupfalse%
  1154 \isacommand{apply}\ assumption\isanewline
  1155 \ \ \ \ \isamarkupfalse%
  1156 \isacommand{done}\isanewline
  1157 \isamarkupfalse%
  1158 \isacommand{qed}\isamarkupfalse%
  1159 %
  1160 \begin{isamarkuptext}%
  1161 \noindent You may need to resort to this technique if an
  1162 automatic step fails to prove the desired proposition.
  1163 
  1164 When converting a proof from tactic-style into Isar you can proceed
  1165 in a top-down manner: parts of the proof can be left in script form
  1166 while the outer structure is already expressed in Isar.%
  1167 \end{isamarkuptext}%
  1168 \isamarkuptrue%
  1169 \isamarkupfalse%
  1170 \end{isabellebody}%
  1171 %%% Local Variables:
  1172 %%% mode: latex
  1173 %%% TeX-master: "root"
  1174 %%% End: