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: