doc-src/IsarRef/Thy/document/Framework.tex
author wenzelm
Fri Oct 29 11:49:56 2010 +0200 (2010-10-29)
changeset 40255 9ffbc25e1606
parent 36357 641a521bfc19
child 40406 313a24b66a8d
permissions -rw-r--r--
eliminated obsolete \_ escapes in rail environments;
     1 %
     2 \begin{isabellebody}%
     3 \def\isabellecontext{Framework}%
     4 %
     5 \isadelimtheory
     6 %
     7 \endisadelimtheory
     8 %
     9 \isatagtheory
    10 \isacommand{theory}\isamarkupfalse%
    11 \ Framework\isanewline
    12 \isakeyword{imports}\ Main\isanewline
    13 \isakeyword{begin}%
    14 \endisatagtheory
    15 {\isafoldtheory}%
    16 %
    17 \isadelimtheory
    18 %
    19 \endisadelimtheory
    20 %
    21 \isamarkupchapter{The Isabelle/Isar Framework \label{ch:isar-framework}%
    22 }
    23 \isamarkuptrue%
    24 %
    25 \begin{isamarkuptext}%
    26 Isabelle/Isar
    27   \cite{Wenzel:1999:TPHOL,Wenzel-PhD,Nipkow-TYPES02,Wenzel-Paulson:2006,Wenzel:2006:Festschrift}
    28   is intended as a generic framework for developing formal
    29   mathematical documents with full proof checking.  Definitions and
    30   proofs are organized as theories.  An assembly of theory sources may
    31   be presented as a printed document; see also
    32   \chref{ch:document-prep}.
    33 
    34   The main objective of Isar is the design of a human-readable
    35   structured proof language, which is called the ``primary proof
    36   format'' in Isar terminology.  Such a primary proof language is
    37   somewhere in the middle between the extremes of primitive proof
    38   objects and actual natural language.  In this respect, Isar is a bit
    39   more formalistic than Mizar
    40   \cite{Trybulec:1993:MizarFeatures,Rudnicki:1992:MizarOverview,Wiedijk:1999:Mizar},
    41   using logical symbols for certain reasoning schemes where Mizar
    42   would prefer English words; see \cite{Wenzel-Wiedijk:2002} for
    43   further comparisons of these systems.
    44 
    45   So Isar challenges the traditional way of recording informal proofs
    46   in mathematical prose, as well as the common tendency to see fully
    47   formal proofs directly as objects of some logical calculus (e.g.\
    48   \isa{{\isachardoublequote}{\isasymlambda}{\isachardoublequote}}-terms in a version of type theory).  In fact, Isar is
    49   better understood as an interpreter of a simple block-structured
    50   language for describing the data flow of local facts and goals,
    51   interspersed with occasional invocations of proof methods.
    52   Everything is reduced to logical inferences internally, but these
    53   steps are somewhat marginal compared to the overall bookkeeping of
    54   the interpretation process.  Thanks to careful design of the syntax
    55   and semantics of Isar language elements, a formal record of Isar
    56   instructions may later appear as an intelligible text to the
    57   attentive reader.
    58 
    59   The Isar proof language has emerged from careful analysis of some
    60   inherent virtues of the existing logical framework of Isabelle/Pure
    61   \cite{paulson-found,paulson700}, notably composition of higher-order
    62   natural deduction rules, which is a generalization of Gentzen's
    63   original calculus \cite{Gentzen:1935}.  The approach of generic
    64   inference systems in Pure is continued by Isar towards actual proof
    65   texts.
    66 
    67   Concrete applications require another intermediate layer: an
    68   object-logic.  Isabelle/HOL \cite{isa-tutorial} (simply-typed
    69   set-theory) is being used most of the time; Isabelle/ZF
    70   \cite{isabelle-ZF} is less extensively developed, although it would
    71   probably fit better for classical mathematics.
    72 
    73   \medskip In order to illustrate natural deduction in Isar, we shall
    74   refer to the background theory and library of Isabelle/HOL.  This
    75   includes common notions of predicate logic, naive set-theory etc.\
    76   using fairly standard mathematical notation.  From the perspective
    77   of generic natural deduction there is nothing special about the
    78   logical connectives of HOL (\isa{{\isachardoublequote}{\isasymand}{\isachardoublequote}}, \isa{{\isachardoublequote}{\isasymor}{\isachardoublequote}}, \isa{{\isachardoublequote}{\isasymforall}{\isachardoublequote}},
    79   \isa{{\isachardoublequote}{\isasymexists}{\isachardoublequote}}, etc.), only the resulting reasoning principles are
    80   relevant to the user.  There are similar rules available for
    81   set-theory operators (\isa{{\isachardoublequote}{\isasyminter}{\isachardoublequote}}, \isa{{\isachardoublequote}{\isasymunion}{\isachardoublequote}}, \isa{{\isachardoublequote}{\isasymInter}{\isachardoublequote}}, \isa{{\isachardoublequote}{\isasymUnion}{\isachardoublequote}}, etc.), or any other theory developed in the library (lattice
    82   theory, topology etc.).
    83 
    84   Subsequently we briefly review fragments of Isar proof texts
    85   corresponding directly to such general deduction schemes.  The
    86   examples shall refer to set-theory, to minimize the danger of
    87   understanding connectives of predicate logic as something special.
    88 
    89   \medskip The following deduction performs \isa{{\isachardoublequote}{\isasyminter}{\isachardoublequote}}-introduction,
    90   working forwards from assumptions towards the conclusion.  We give
    91   both the Isar text, and depict the primitive rule involved, as
    92   determined by unification of the problem against rules that are
    93   declared in the library context.%
    94 \end{isamarkuptext}%
    95 \isamarkuptrue%
    96 %
    97 \medskip\begin{minipage}{0.6\textwidth}
    98 %
    99 \isadelimproof
   100 \ \ \ \ %
   101 \endisadelimproof
   102 %
   103 \isatagproof
   104 \isacommand{assume}\isamarkupfalse%
   105 \ {\isachardoublequoteopen}x\ {\isasymin}\ A{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}x\ {\isasymin}\ B{\isachardoublequoteclose}\isanewline
   106 \ \ \ \ \isacommand{then}\isamarkupfalse%
   107 \ \isacommand{have}\isamarkupfalse%
   108 \ {\isachardoublequoteopen}x\ {\isasymin}\ A\ {\isasyminter}\ B{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
   109 %
   110 \endisatagproof
   111 {\isafoldproof}%
   112 %
   113 \isadelimproof
   114 %
   115 \endisadelimproof
   116 %
   117 \end{minipage}\begin{minipage}{0.4\textwidth}
   118 %
   119 \begin{isamarkuptext}%
   120 \infer{\isa{{\isachardoublequote}x\ {\isasymin}\ A\ {\isasyminter}\ B{\isachardoublequote}}}{\isa{{\isachardoublequote}x\ {\isasymin}\ A{\isachardoublequote}} & \isa{{\isachardoublequote}x\ {\isasymin}\ B{\isachardoublequote}}}%
   121 \end{isamarkuptext}%
   122 \isamarkuptrue%
   123 %
   124 \end{minipage}
   125 %
   126 \begin{isamarkuptext}%
   127 \medskip\noindent Note that \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}} augments the proof
   128   context, \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}} indicates that the current fact shall be
   129   used in the next step, and \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}} states an intermediate
   130   goal.  The two dots ``\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}}'' refer to a complete proof of
   131   this claim, using the indicated facts and a canonical rule from the
   132   context.  We could have been more explicit here by spelling out the
   133   final proof step via the \hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}} command:%
   134 \end{isamarkuptext}%
   135 \isamarkuptrue%
   136 %
   137 \isadelimproof
   138 \ \ \ \ %
   139 \endisadelimproof
   140 %
   141 \isatagproof
   142 \isacommand{assume}\isamarkupfalse%
   143 \ {\isachardoublequoteopen}x\ {\isasymin}\ A{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}x\ {\isasymin}\ B{\isachardoublequoteclose}\isanewline
   144 \ \ \ \ \isacommand{then}\isamarkupfalse%
   145 \ \isacommand{have}\isamarkupfalse%
   146 \ {\isachardoublequoteopen}x\ {\isasymin}\ A\ {\isasyminter}\ B{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
   147 \ {\isacharparenleft}rule\ IntI{\isacharparenright}%
   148 \endisatagproof
   149 {\isafoldproof}%
   150 %
   151 \isadelimproof
   152 %
   153 \endisadelimproof
   154 %
   155 \begin{isamarkuptext}%
   156 \noindent The format of the \isa{{\isachardoublequote}{\isasyminter}{\isachardoublequote}}-introduction rule represents
   157   the most basic inference, which proceeds from given premises to a
   158   conclusion, without any nested proof context involved.
   159 
   160   The next example performs backwards introduction on \isa{{\isachardoublequote}{\isasymInter}{\isasymA}{\isachardoublequote}},
   161   the intersection of all sets within a given set.  This requires a
   162   nested proof of set membership within a local context, where \isa{A} is an arbitrary-but-fixed member of the collection:%
   163 \end{isamarkuptext}%
   164 \isamarkuptrue%
   165 %
   166 \medskip\begin{minipage}{0.6\textwidth}
   167 %
   168 \isadelimproof
   169 \ \ \ \ %
   170 \endisadelimproof
   171 %
   172 \isatagproof
   173 \isacommand{have}\isamarkupfalse%
   174 \ {\isachardoublequoteopen}x\ {\isasymin}\ {\isasymInter}{\isasymA}{\isachardoublequoteclose}\isanewline
   175 \ \ \ \ \isacommand{proof}\isamarkupfalse%
   176 \isanewline
   177 \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
   178 \ A\isanewline
   179 \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
   180 \ {\isachardoublequoteopen}A\ {\isasymin}\ {\isasymA}{\isachardoublequoteclose}\isanewline
   181 \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
   182 \ {\isachardoublequoteopen}x\ {\isasymin}\ A{\isachardoublequoteclose}%
   183 \endisatagproof
   184 {\isafoldproof}%
   185 %
   186 \isadelimproof
   187 %
   188 \endisadelimproof
   189 %
   190 \isadelimnoproof
   191 \ %
   192 \endisadelimnoproof
   193 %
   194 \isatagnoproof
   195 \isacommand{sorry}\isamarkupfalse%
   196 %
   197 \endisatagnoproof
   198 {\isafoldnoproof}%
   199 %
   200 \isadelimnoproof
   201 %
   202 \endisadelimnoproof
   203 \isanewline
   204 %
   205 \isadelimproof
   206 \ \ \ \ %
   207 \endisadelimproof
   208 %
   209 \isatagproof
   210 \isacommand{qed}\isamarkupfalse%
   211 %
   212 \endisatagproof
   213 {\isafoldproof}%
   214 %
   215 \isadelimproof
   216 %
   217 \endisadelimproof
   218 %
   219 \end{minipage}\begin{minipage}{0.4\textwidth}
   220 %
   221 \begin{isamarkuptext}%
   222 \infer{\isa{{\isachardoublequote}x\ {\isasymin}\ {\isasymInter}{\isasymA}{\isachardoublequote}}}{\infer*{\isa{{\isachardoublequote}x\ {\isasymin}\ A{\isachardoublequote}}}{\isa{{\isachardoublequote}{\isacharbrackleft}A{\isacharbrackright}{\isacharbrackleft}A\ {\isasymin}\ {\isasymA}{\isacharbrackright}{\isachardoublequote}}}}%
   223 \end{isamarkuptext}%
   224 \isamarkuptrue%
   225 %
   226 \end{minipage}
   227 %
   228 \begin{isamarkuptext}%
   229 \medskip\noindent This Isar reasoning pattern again refers to the
   230   primitive rule depicted above.  The system determines it in the
   231   ``\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}'' step, which could have been spelt out more
   232   explicitly as ``\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isachardoublequote}{\isacharparenleft}rule\ InterI{\isacharparenright}{\isachardoublequote}}''.  Note
   233   that the rule involves both a local parameter \isa{{\isachardoublequote}A{\isachardoublequote}} and an
   234   assumption \isa{{\isachardoublequote}A\ {\isasymin}\ {\isasymA}{\isachardoublequote}} in the nested reasoning.  This kind of
   235   compound rule typically demands a genuine sub-proof in Isar, working
   236   backwards rather than forwards as seen before.  In the proof body we
   237   encounter the \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}-\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}-\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}
   238   outline of nested sub-proofs that is typical for Isar.  The final
   239   \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}} is like \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}} followed by an additional
   240   refinement of the enclosing claim, using the rule derived from the
   241   proof body.
   242 
   243   \medskip The next example involves \isa{{\isachardoublequote}{\isasymUnion}{\isasymA}{\isachardoublequote}}, which can be
   244   characterized as the set of all \isa{{\isachardoublequote}x{\isachardoublequote}} such that \isa{{\isachardoublequote}{\isasymexists}A{\isachardot}\ x\ {\isasymin}\ A\ {\isasymand}\ A\ {\isasymin}\ {\isasymA}{\isachardoublequote}}.  The elimination rule for \isa{{\isachardoublequote}x\ {\isasymin}\ {\isasymUnion}{\isasymA}{\isachardoublequote}} does
   245   not mention \isa{{\isachardoublequote}{\isasymexists}{\isachardoublequote}} and \isa{{\isachardoublequote}{\isasymand}{\isachardoublequote}} at all, but admits to obtain
   246   directly a local \isa{{\isachardoublequote}A{\isachardoublequote}} such that \isa{{\isachardoublequote}x\ {\isasymin}\ A{\isachardoublequote}} and \isa{{\isachardoublequote}A\ {\isasymin}\ {\isasymA}{\isachardoublequote}} hold.  This corresponds to the following Isar proof and
   247   inference rule, respectively:%
   248 \end{isamarkuptext}%
   249 \isamarkuptrue%
   250 %
   251 \medskip\begin{minipage}{0.6\textwidth}
   252 %
   253 \isadelimproof
   254 \ \ \ \ %
   255 \endisadelimproof
   256 %
   257 \isatagproof
   258 \isacommand{assume}\isamarkupfalse%
   259 \ {\isachardoublequoteopen}x\ {\isasymin}\ {\isasymUnion}{\isasymA}{\isachardoublequoteclose}\isanewline
   260 \ \ \ \ \isacommand{then}\isamarkupfalse%
   261 \ \isacommand{have}\isamarkupfalse%
   262 \ C\isanewline
   263 \ \ \ \ \isacommand{proof}\isamarkupfalse%
   264 \isanewline
   265 \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
   266 \ A\isanewline
   267 \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
   268 \ {\isachardoublequoteopen}x\ {\isasymin}\ A{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}A\ {\isasymin}\ {\isasymA}{\isachardoublequoteclose}\isanewline
   269 \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
   270 \ C%
   271 \endisatagproof
   272 {\isafoldproof}%
   273 %
   274 \isadelimproof
   275 %
   276 \endisadelimproof
   277 %
   278 \isadelimnoproof
   279 \ %
   280 \endisadelimnoproof
   281 %
   282 \isatagnoproof
   283 \isacommand{sorry}\isamarkupfalse%
   284 %
   285 \endisatagnoproof
   286 {\isafoldnoproof}%
   287 %
   288 \isadelimnoproof
   289 %
   290 \endisadelimnoproof
   291 \isanewline
   292 %
   293 \isadelimproof
   294 \ \ \ \ %
   295 \endisadelimproof
   296 %
   297 \isatagproof
   298 \isacommand{qed}\isamarkupfalse%
   299 %
   300 \endisatagproof
   301 {\isafoldproof}%
   302 %
   303 \isadelimproof
   304 %
   305 \endisadelimproof
   306 %
   307 \end{minipage}\begin{minipage}{0.4\textwidth}
   308 %
   309 \begin{isamarkuptext}%
   310 \infer{\isa{{\isachardoublequote}C{\isachardoublequote}}}{\isa{{\isachardoublequote}x\ {\isasymin}\ {\isasymUnion}{\isasymA}{\isachardoublequote}} & \infer*{\isa{{\isachardoublequote}C{\isachardoublequote}}~}{\isa{{\isachardoublequote}{\isacharbrackleft}A{\isacharbrackright}{\isacharbrackleft}x\ {\isasymin}\ A{\isacharcomma}\ A\ {\isasymin}\ {\isasymA}{\isacharbrackright}{\isachardoublequote}}}}%
   311 \end{isamarkuptext}%
   312 \isamarkuptrue%
   313 %
   314 \end{minipage}
   315 %
   316 \begin{isamarkuptext}%
   317 \medskip\noindent Although the Isar proof follows the natural
   318   deduction rule closely, the text reads not as natural as
   319   anticipated.  There is a double occurrence of an arbitrary
   320   conclusion \isa{{\isachardoublequote}C{\isachardoublequote}}, which represents the final result, but is
   321   irrelevant for now.  This issue arises for any elimination rule
   322   involving local parameters.  Isar provides the derived language
   323   element \hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}}, which is able to perform the same
   324   elimination proof more conveniently:%
   325 \end{isamarkuptext}%
   326 \isamarkuptrue%
   327 %
   328 \isadelimproof
   329 \ \ \ \ %
   330 \endisadelimproof
   331 %
   332 \isatagproof
   333 \isacommand{assume}\isamarkupfalse%
   334 \ {\isachardoublequoteopen}x\ {\isasymin}\ {\isasymUnion}{\isasymA}{\isachardoublequoteclose}\isanewline
   335 \ \ \ \ \isacommand{then}\isamarkupfalse%
   336 \ \isacommand{obtain}\isamarkupfalse%
   337 \ A\ \isakeyword{where}\ {\isachardoublequoteopen}x\ {\isasymin}\ A{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}A\ {\isasymin}\ {\isasymA}{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
   338 %
   339 \endisatagproof
   340 {\isafoldproof}%
   341 %
   342 \isadelimproof
   343 %
   344 \endisadelimproof
   345 %
   346 \begin{isamarkuptext}%
   347 \noindent Here we avoid to mention the final conclusion \isa{{\isachardoublequote}C{\isachardoublequote}}
   348   and return to plain forward reasoning.  The rule involved in the
   349   ``\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}}'' proof is the same as before.%
   350 \end{isamarkuptext}%
   351 \isamarkuptrue%
   352 %
   353 \isamarkupsection{The Pure framework \label{sec:framework-pure}%
   354 }
   355 \isamarkuptrue%
   356 %
   357 \begin{isamarkuptext}%
   358 The Pure logic \cite{paulson-found,paulson700} is an intuitionistic
   359   fragment of higher-order logic \cite{church40}.  In type-theoretic
   360   parlance, there are three levels of \isa{{\isachardoublequote}{\isasymlambda}{\isachardoublequote}}-calculus with
   361   corresponding arrows \isa{{\isachardoublequote}{\isasymRightarrow}{\isachardoublequote}}/\isa{{\isachardoublequote}{\isasymAnd}{\isachardoublequote}}/\isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}}:
   362 
   363   \medskip
   364   \begin{tabular}{ll}
   365   \isa{{\isachardoublequote}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymbeta}{\isachardoublequote}} & syntactic function space (terms depending on terms) \\
   366   \isa{{\isachardoublequote}{\isasymAnd}x{\isachardot}\ B{\isacharparenleft}x{\isacharparenright}{\isachardoublequote}} & universal quantification (proofs depending on terms) \\
   367   \isa{{\isachardoublequote}A\ {\isasymLongrightarrow}\ B{\isachardoublequote}} & implication (proofs depending on proofs) \\
   368   \end{tabular}
   369   \medskip
   370 
   371   \noindent Here only the types of syntactic terms, and the
   372   propositions of proof terms have been shown.  The \isa{{\isachardoublequote}{\isasymlambda}{\isachardoublequote}}-structure of proofs can be recorded as an optional feature of
   373   the Pure inference kernel \cite{Berghofer-Nipkow:2000:TPHOL}, but
   374   the formal system can never depend on them due to \emph{proof
   375   irrelevance}.
   376 
   377   On top of this most primitive layer of proofs, Pure implements a
   378   generic calculus for nested natural deduction rules, similar to
   379   \cite{Schroeder-Heister:1984}.  Here object-logic inferences are
   380   internalized as formulae over \isa{{\isachardoublequote}{\isasymAnd}{\isachardoublequote}} and \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}}.
   381   Combining such rule statements may involve higher-order unification
   382   \cite{paulson-natural}.%
   383 \end{isamarkuptext}%
   384 \isamarkuptrue%
   385 %
   386 \isamarkupsubsection{Primitive inferences%
   387 }
   388 \isamarkuptrue%
   389 %
   390 \begin{isamarkuptext}%
   391 Term syntax provides explicit notation for abstraction \isa{{\isachardoublequote}{\isasymlambda}x\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}{\isachardot}\ b{\isacharparenleft}x{\isacharparenright}{\isachardoublequote}} and application \isa{{\isachardoublequote}b\ a{\isachardoublequote}}, while types are usually
   392   implicit thanks to type-inference; terms of type \isa{{\isachardoublequote}prop{\isachardoublequote}} are
   393   called propositions.  Logical statements are composed via \isa{{\isachardoublequote}{\isasymAnd}x\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}{\isachardot}\ B{\isacharparenleft}x{\isacharparenright}{\isachardoublequote}} and \isa{{\isachardoublequote}A\ {\isasymLongrightarrow}\ B{\isachardoublequote}}.  Primitive reasoning operates on
   394   judgments of the form \isa{{\isachardoublequote}{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}{\isachardoublequote}}, with standard introduction
   395   and elimination rules for \isa{{\isachardoublequote}{\isasymAnd}{\isachardoublequote}} and \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}} that refer to
   396   fixed parameters \isa{{\isachardoublequote}x\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlisub m{\isachardoublequote}} and hypotheses
   397   \isa{{\isachardoublequote}A\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ A\isactrlisub n{\isachardoublequote}} from the context \isa{{\isachardoublequote}{\isasymGamma}{\isachardoublequote}};
   398   the corresponding proof terms are left implicit.  The subsequent
   399   inference rules define \isa{{\isachardoublequote}{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}{\isachardoublequote}} inductively, relative to a
   400   collection of axioms:
   401 
   402   \[
   403   \infer{\isa{{\isachardoublequote}{\isasymturnstile}\ A{\isachardoublequote}}}{(\isa{{\isachardoublequote}A{\isachardoublequote}} \text{~axiom})}
   404   \qquad
   405   \infer{\isa{{\isachardoublequote}A\ {\isasymturnstile}\ A{\isachardoublequote}}}{}
   406   \]
   407 
   408   \[
   409   \infer{\isa{{\isachardoublequote}{\isasymGamma}\ {\isasymturnstile}\ {\isasymAnd}x{\isachardot}\ B{\isacharparenleft}x{\isacharparenright}{\isachardoublequote}}}{\isa{{\isachardoublequote}{\isasymGamma}\ {\isasymturnstile}\ B{\isacharparenleft}x{\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}x\ {\isasymnotin}\ {\isasymGamma}{\isachardoublequote}}}
   410   \qquad
   411   \infer{\isa{{\isachardoublequote}{\isasymGamma}\ {\isasymturnstile}\ B{\isacharparenleft}a{\isacharparenright}{\isachardoublequote}}}{\isa{{\isachardoublequote}{\isasymGamma}\ {\isasymturnstile}\ {\isasymAnd}x{\isachardot}\ B{\isacharparenleft}x{\isacharparenright}{\isachardoublequote}}}
   412   \]
   413 
   414   \[
   415   \infer{\isa{{\isachardoublequote}{\isasymGamma}\ {\isacharminus}\ A\ {\isasymturnstile}\ A\ {\isasymLongrightarrow}\ B{\isachardoublequote}}}{\isa{{\isachardoublequote}{\isasymGamma}\ {\isasymturnstile}\ B{\isachardoublequote}}}
   416   \qquad
   417   \infer{\isa{{\isachardoublequote}{\isasymGamma}\isactrlsub {\isadigit{1}}\ {\isasymunion}\ {\isasymGamma}\isactrlsub {\isadigit{2}}\ {\isasymturnstile}\ B{\isachardoublequote}}}{\isa{{\isachardoublequote}{\isasymGamma}\isactrlsub {\isadigit{1}}\ {\isasymturnstile}\ A\ {\isasymLongrightarrow}\ B{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymGamma}\isactrlsub {\isadigit{2}}\ {\isasymturnstile}\ A{\isachardoublequote}}}
   418   \]
   419 
   420   Furthermore, Pure provides a built-in equality \isa{{\isachardoublequote}{\isasymequiv}\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ prop{\isachardoublequote}} with axioms for reflexivity, substitution, extensionality,
   421   and \isa{{\isachardoublequote}{\isasymalpha}{\isasymbeta}{\isasymeta}{\isachardoublequote}}-conversion on \isa{{\isachardoublequote}{\isasymlambda}{\isachardoublequote}}-terms.
   422 
   423   \medskip An object-logic introduces another layer on top of Pure,
   424   e.g.\ with types \isa{{\isachardoublequote}i{\isachardoublequote}} for individuals and \isa{{\isachardoublequote}o{\isachardoublequote}} for
   425   propositions, term constants \isa{{\isachardoublequote}Trueprop\ {\isacharcolon}{\isacharcolon}\ o\ {\isasymRightarrow}\ prop{\isachardoublequote}} as
   426   (implicit) derivability judgment and connectives like \isa{{\isachardoublequote}{\isasymand}\ {\isacharcolon}{\isacharcolon}\ o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ o{\isachardoublequote}} or \isa{{\isachardoublequote}{\isasymforall}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}i\ {\isasymRightarrow}\ o{\isacharparenright}\ {\isasymRightarrow}\ o{\isachardoublequote}}, and axioms for object-level
   427   rules such as \isa{{\isachardoublequote}conjI{\isacharcolon}\ A\ {\isasymLongrightarrow}\ B\ {\isasymLongrightarrow}\ A\ {\isasymand}\ B{\isachardoublequote}} or \isa{{\isachardoublequote}allI{\isacharcolon}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ B\ x{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymforall}x{\isachardot}\ B\ x{\isachardoublequote}}.  Derived object rules are represented as theorems of
   428   Pure.  After the initial object-logic setup, further axiomatizations
   429   are usually avoided; plain definitions and derived principles are
   430   used exclusively.%
   431 \end{isamarkuptext}%
   432 \isamarkuptrue%
   433 %
   434 \isamarkupsubsection{Reasoning with rules \label{sec:framework-resolution}%
   435 }
   436 \isamarkuptrue%
   437 %
   438 \begin{isamarkuptext}%
   439 Primitive inferences mostly serve foundational purposes.  The main
   440   reasoning mechanisms of Pure operate on nested natural deduction
   441   rules expressed as formulae, using \isa{{\isachardoublequote}{\isasymAnd}{\isachardoublequote}} to bind local
   442   parameters and \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}} to express entailment.  Multiple
   443   parameters and premises are represented by repeating these
   444   connectives in a right-associative manner.
   445 
   446   Since \isa{{\isachardoublequote}{\isasymAnd}{\isachardoublequote}} and \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}} commute thanks to the theorem
   447   \isa{{\isachardoublequote}{\isacharparenleft}A\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ B\ x{\isacharparenright}{\isacharparenright}\ {\isasymequiv}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ A\ {\isasymLongrightarrow}\ B\ x{\isacharparenright}{\isachardoublequote}}, we may assume w.l.o.g.\
   448   that rule statements always observe the normal form where
   449   quantifiers are pulled in front of implications at each level of
   450   nesting.  This means that any Pure proposition may be presented as a
   451   \emph{Hereditary Harrop Formula} \cite{Miller:1991} which is of the
   452   form \isa{{\isachardoublequote}{\isasymAnd}x\isactrlisub {\isadigit{1}}\ {\isasymdots}\ x\isactrlisub m{\isachardot}\ H\isactrlisub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ H\isactrlisub n\ {\isasymLongrightarrow}\ A{\isachardoublequote}} for \isa{{\isachardoublequote}m{\isacharcomma}\ n\ {\isasymge}\ {\isadigit{0}}{\isachardoublequote}}, and \isa{{\isachardoublequote}A{\isachardoublequote}} atomic, and \isa{{\isachardoublequote}H\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ H\isactrlisub n{\isachardoublequote}} being recursively of the same format.
   453   Following the convention that outermost quantifiers are implicit,
   454   Horn clauses \isa{{\isachardoublequote}A\isactrlisub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ A\isactrlisub n\ {\isasymLongrightarrow}\ A{\isachardoublequote}} are a special
   455   case of this.
   456 
   457   For example, \isa{{\isachardoublequote}{\isasyminter}{\isachardoublequote}}-introduction rule encountered before is
   458   represented as a Pure theorem as follows:
   459   \[
   460   \isa{{\isachardoublequote}IntI{\isacharcolon}{\isachardoublequote}}~\isa{{\isachardoublequote}x\ {\isasymin}\ A\ {\isasymLongrightarrow}\ x\ {\isasymin}\ B\ {\isasymLongrightarrow}\ x\ {\isasymin}\ A\ {\isasyminter}\ B{\isachardoublequote}}
   461   \]
   462 
   463   \noindent This is a plain Horn clause, since no further nesting on
   464   the left is involved.  The general \isa{{\isachardoublequote}{\isasymInter}{\isachardoublequote}}-introduction
   465   corresponds to a Hereditary Harrop Formula with one additional level
   466   of nesting:
   467   \[
   468   \isa{{\isachardoublequote}InterI{\isacharcolon}{\isachardoublequote}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymAnd}A{\isachardot}\ A\ {\isasymin}\ {\isasymA}\ {\isasymLongrightarrow}\ x\ {\isasymin}\ A{\isacharparenright}\ {\isasymLongrightarrow}\ x\ {\isasymin}\ {\isasymInter}{\isasymA}{\isachardoublequote}}
   469   \]
   470 
   471   \medskip Goals are also represented as rules: \isa{{\isachardoublequote}A\isactrlisub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ A\isactrlisub n\ {\isasymLongrightarrow}\ C{\isachardoublequote}} states that the sub-goals \isa{{\isachardoublequote}A\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ A\isactrlisub n{\isachardoublequote}} entail the result \isa{{\isachardoublequote}C{\isachardoublequote}}; for \isa{{\isachardoublequote}n\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequote}} the
   472   goal is finished.  To allow \isa{{\isachardoublequote}C{\isachardoublequote}} being a rule statement
   473   itself, we introduce the protective marker \isa{{\isachardoublequote}{\isacharhash}\ {\isacharcolon}{\isacharcolon}\ prop\ {\isasymRightarrow}\ prop{\isachardoublequote}}, which is defined as identity and hidden from the user.  We
   474   initialize and finish goal states as follows:
   475 
   476   \[
   477   \begin{array}{c@ {\qquad}c}
   478   \infer[(\indexdef{}{inference}{init}\hypertarget{inference.init}{\hyperlink{inference.init}{\mbox{\isa{init}}}})]{\isa{{\isachardoublequote}C\ {\isasymLongrightarrow}\ {\isacharhash}C{\isachardoublequote}}}{} &
   479   \infer[(\indexdef{}{inference}{finish}\hypertarget{inference.finish}{\hyperlink{inference.finish}{\mbox{\isa{finish}}}})]{\isa{C}}{\isa{{\isachardoublequote}{\isacharhash}C{\isachardoublequote}}}
   480   \end{array}
   481   \]
   482 
   483   \noindent Goal states are refined in intermediate proof steps until
   484   a finished form is achieved.  Here the two main reasoning principles
   485   are \hyperlink{inference.resolution}{\mbox{\isa{resolution}}}, for back-chaining a rule against a
   486   sub-goal (replacing it by zero or more sub-goals), and \hyperlink{inference.assumption}{\mbox{\isa{assumption}}}, for solving a sub-goal (finding a short-circuit with
   487   local assumptions).  Below \isa{{\isachardoublequote}\isactrlvec x{\isachardoublequote}} stands for \isa{{\isachardoublequote}x\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlisub n{\isachardoublequote}} (\isa{{\isachardoublequote}n\ {\isasymge}\ {\isadigit{0}}{\isachardoublequote}}).
   488 
   489   \[
   490   \infer[(\indexdef{}{inference}{resolution}\hypertarget{inference.resolution}{\hyperlink{inference.resolution}{\mbox{\isa{resolution}}}})]
   491   {\isa{{\isachardoublequote}{\isacharparenleft}{\isasymAnd}\isactrlvec x{\isachardot}\ \isactrlvec H\ \isactrlvec x\ {\isasymLongrightarrow}\ \isactrlvec A\ {\isacharparenleft}\isactrlvec a\ \isactrlvec x{\isacharparenright}{\isacharparenright}{\isasymvartheta}\ {\isasymLongrightarrow}\ C{\isasymvartheta}{\isachardoublequote}}}
   492   {\begin{tabular}{rl}
   493     \isa{{\isachardoublequote}rule{\isacharcolon}{\isachardoublequote}} &
   494     \isa{{\isachardoublequote}\isactrlvec A\ \isactrlvec a\ {\isasymLongrightarrow}\ B\ \isactrlvec a{\isachardoublequote}} \\
   495     \isa{{\isachardoublequote}goal{\isacharcolon}{\isachardoublequote}} &
   496     \isa{{\isachardoublequote}{\isacharparenleft}{\isasymAnd}\isactrlvec x{\isachardot}\ \isactrlvec H\ \isactrlvec x\ {\isasymLongrightarrow}\ B{\isacharprime}\ \isactrlvec x{\isacharparenright}\ {\isasymLongrightarrow}\ C{\isachardoublequote}} \\
   497     \isa{{\isachardoublequote}goal\ unifier{\isacharcolon}{\isachardoublequote}} &
   498     \isa{{\isachardoublequote}{\isacharparenleft}{\isasymlambda}\isactrlvec x{\isachardot}\ B\ {\isacharparenleft}\isactrlvec a\ \isactrlvec x{\isacharparenright}{\isacharparenright}{\isasymvartheta}\ {\isacharequal}\ B{\isacharprime}{\isasymvartheta}{\isachardoublequote}} \\
   499    \end{tabular}}
   500   \]
   501 
   502   \medskip
   503 
   504   \[
   505   \infer[(\indexdef{}{inference}{assumption}\hypertarget{inference.assumption}{\hyperlink{inference.assumption}{\mbox{\isa{assumption}}}})]{\isa{{\isachardoublequote}C{\isasymvartheta}{\isachardoublequote}}}
   506   {\begin{tabular}{rl}
   507     \isa{{\isachardoublequote}goal{\isacharcolon}{\isachardoublequote}} &
   508     \isa{{\isachardoublequote}{\isacharparenleft}{\isasymAnd}\isactrlvec x{\isachardot}\ \isactrlvec H\ \isactrlvec x\ {\isasymLongrightarrow}\ A\ \isactrlvec x{\isacharparenright}\ {\isasymLongrightarrow}\ C{\isachardoublequote}} \\
   509     \isa{{\isachardoublequote}assm\ unifier{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}A{\isasymvartheta}\ {\isacharequal}\ H\isactrlsub i{\isasymvartheta}{\isachardoublequote}}~~\text{(for some~\isa{{\isachardoublequote}H\isactrlsub i{\isachardoublequote}})} \\
   510    \end{tabular}}
   511   \]
   512 
   513   The following trace illustrates goal-oriented reasoning in
   514   Isabelle/Pure:
   515 
   516   {\footnotesize
   517   \medskip
   518   \begin{tabular}{r@ {\quad}l}
   519   \isa{{\isachardoublequote}{\isacharparenleft}A\ {\isasymand}\ B\ {\isasymLongrightarrow}\ B\ {\isasymand}\ A{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharhash}{\isacharparenleft}A\ {\isasymand}\ B\ {\isasymLongrightarrow}\ B\ {\isasymand}\ A{\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}init{\isacharparenright}{\isachardoublequote}} \\
   520   \isa{{\isachardoublequote}{\isacharparenleft}A\ {\isasymand}\ B\ {\isasymLongrightarrow}\ B{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}A\ {\isasymand}\ B\ {\isasymLongrightarrow}\ A{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharhash}{\isasymdots}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}resolution\ B\ {\isasymLongrightarrow}\ A\ {\isasymLongrightarrow}\ B\ {\isasymand}\ A{\isacharparenright}{\isachardoublequote}} \\
   521   \isa{{\isachardoublequote}{\isacharparenleft}A\ {\isasymand}\ B\ {\isasymLongrightarrow}\ A\ {\isasymand}\ B{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}A\ {\isasymand}\ B\ {\isasymLongrightarrow}\ A{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharhash}{\isasymdots}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}resolution\ A\ {\isasymand}\ B\ {\isasymLongrightarrow}\ B{\isacharparenright}{\isachardoublequote}} \\
   522   \isa{{\isachardoublequote}{\isacharparenleft}A\ {\isasymand}\ B\ {\isasymLongrightarrow}\ A{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharhash}{\isasymdots}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}assumption{\isacharparenright}{\isachardoublequote}} \\
   523   \isa{{\isachardoublequote}{\isacharparenleft}A\ {\isasymand}\ B\ {\isasymLongrightarrow}\ B\ {\isasymand}\ A{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharhash}{\isasymdots}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}resolution\ A\ {\isasymand}\ B\ {\isasymLongrightarrow}\ A{\isacharparenright}{\isachardoublequote}} \\
   524   \isa{{\isachardoublequote}{\isacharhash}{\isasymdots}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}assumption{\isacharparenright}{\isachardoublequote}} \\
   525   \isa{{\isachardoublequote}A\ {\isasymand}\ B\ {\isasymLongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}finish{\isacharparenright}{\isachardoublequote}} \\
   526   \end{tabular}
   527   \medskip
   528   }
   529 
   530   Compositions of \hyperlink{inference.assumption}{\mbox{\isa{assumption}}} after \hyperlink{inference.resolution}{\mbox{\isa{resolution}}} occurs quite often, typically in elimination steps.
   531   Traditional Isabelle tactics accommodate this by a combined
   532   \indexdef{}{inference}{elim\_resolution}\hypertarget{inference.elim-resolution}{\hyperlink{inference.elim-resolution}{\mbox{\isa{elim{\isacharunderscore}resolution}}}} principle.  In contrast, Isar uses
   533   a slightly more refined combination, where the assumptions to be
   534   closed are marked explicitly, using again the protective marker
   535   \isa{{\isachardoublequote}{\isacharhash}{\isachardoublequote}}:
   536 
   537   \[
   538   \infer[(\hyperlink{inference.refinement}{\mbox{\isa{refinement}}})]
   539   {\isa{{\isachardoublequote}{\isacharparenleft}{\isasymAnd}\isactrlvec x{\isachardot}\ \isactrlvec H\ \isactrlvec x\ {\isasymLongrightarrow}\ \isactrlvec G{\isacharprime}\ {\isacharparenleft}\isactrlvec a\ \isactrlvec x{\isacharparenright}{\isacharparenright}{\isasymvartheta}\ {\isasymLongrightarrow}\ C{\isasymvartheta}{\isachardoublequote}}}
   540   {\begin{tabular}{rl}
   541     \isa{{\isachardoublequote}sub{\isasymdash}proof{\isacharcolon}{\isachardoublequote}} &
   542     \isa{{\isachardoublequote}\isactrlvec G\ \isactrlvec a\ {\isasymLongrightarrow}\ B\ \isactrlvec a{\isachardoublequote}} \\
   543     \isa{{\isachardoublequote}goal{\isacharcolon}{\isachardoublequote}} &
   544     \isa{{\isachardoublequote}{\isacharparenleft}{\isasymAnd}\isactrlvec x{\isachardot}\ \isactrlvec H\ \isactrlvec x\ {\isasymLongrightarrow}\ B{\isacharprime}\ \isactrlvec x{\isacharparenright}\ {\isasymLongrightarrow}\ C{\isachardoublequote}} \\
   545     \isa{{\isachardoublequote}goal\ unifier{\isacharcolon}{\isachardoublequote}} &
   546     \isa{{\isachardoublequote}{\isacharparenleft}{\isasymlambda}\isactrlvec x{\isachardot}\ B\ {\isacharparenleft}\isactrlvec a\ \isactrlvec x{\isacharparenright}{\isacharparenright}{\isasymvartheta}\ {\isacharequal}\ B{\isacharprime}{\isasymvartheta}{\isachardoublequote}} \\
   547     \isa{{\isachardoublequote}assm\ unifiers{\isacharcolon}{\isachardoublequote}} &
   548     \isa{{\isachardoublequote}{\isacharparenleft}{\isasymlambda}\isactrlvec x{\isachardot}\ G\isactrlsub j\ {\isacharparenleft}\isactrlvec a\ \isactrlvec x{\isacharparenright}{\isacharparenright}{\isasymvartheta}\ {\isacharequal}\ {\isacharhash}H\isactrlsub i{\isasymvartheta}{\isachardoublequote}} \\
   549     & \quad (for each marked \isa{{\isachardoublequote}G\isactrlsub j{\isachardoublequote}} some \isa{{\isachardoublequote}{\isacharhash}H\isactrlsub i{\isachardoublequote}}) \\
   550    \end{tabular}}
   551   \]
   552 
   553   \noindent Here the \isa{{\isachardoublequote}sub{\isasymdash}proof{\isachardoublequote}} rule stems from the
   554   main \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}-\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}-\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}} outline of
   555   Isar (cf.\ \secref{sec:framework-subproof}): each assumption
   556   indicated in the text results in a marked premise \isa{{\isachardoublequote}G{\isachardoublequote}} above.
   557   The marking enforces resolution against one of the sub-goal's
   558   premises.  Consequently, \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}-\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}-\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}} enables to fit the result of a sub-proof quite robustly into a
   559   pending sub-goal, while maintaining a good measure of flexibility.%
   560 \end{isamarkuptext}%
   561 \isamarkuptrue%
   562 %
   563 \isamarkupsection{The Isar proof language \label{sec:framework-isar}%
   564 }
   565 \isamarkuptrue%
   566 %
   567 \begin{isamarkuptext}%
   568 Structured proofs are presented as high-level expressions for
   569   composing entities of Pure (propositions, facts, and goals).  The
   570   Isar proof language allows to organize reasoning within the
   571   underlying rule calculus of Pure, but Isar is not another logical
   572   calculus!
   573 
   574   Isar is an exercise in sound minimalism.  Approximately half of the
   575   language is introduced as primitive, the rest defined as derived
   576   concepts.  The following grammar describes the core language
   577   (category \isa{{\isachardoublequote}proof{\isachardoublequote}}), which is embedded into theory
   578   specification elements such as \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}; see also
   579   \secref{sec:framework-stmt} for the separate category \isa{{\isachardoublequote}statement{\isachardoublequote}}.
   580 
   581   \medskip
   582   \begin{tabular}{rcl}
   583     \isa{{\isachardoublequote}theory{\isasymdash}stmt{\isachardoublequote}} & = & \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}~\isa{{\isachardoublequote}statement\ proof\ \ {\isacharbar}{\isachardoublequote}}~~\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}~\isa{{\isachardoublequote}{\isasymdots}\ \ {\isacharbar}\ \ {\isasymdots}{\isachardoublequote}} \\[1ex]
   584 
   585     \isa{{\isachardoublequote}proof{\isachardoublequote}} & = & \isa{{\isachardoublequote}prfx\isactrlsup {\isacharasterisk}{\isachardoublequote}}~\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isachardoublequote}method\isactrlsup {\isacharquery}\ stmt\isactrlsup {\isacharasterisk}{\isachardoublequote}}~\hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}~\isa{{\isachardoublequote}method\isactrlsup {\isacharquery}{\isachardoublequote}} \\[1ex]
   586 
   587     \isa{prfx} & = & \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}~\isa{{\isachardoublequote}facts{\isachardoublequote}} \\
   588     & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \hyperlink{command.unfolding}{\mbox{\isa{\isacommand{unfolding}}}}~\isa{{\isachardoublequote}facts{\isachardoublequote}} \\
   589 
   590     \isa{stmt} & = & \hyperlink{command.braceleft}{\mbox{\isa{\isacommand{{\isacharbraceleft}}}}}~\isa{{\isachardoublequote}stmt\isactrlsup {\isacharasterisk}{\isachardoublequote}}~\hyperlink{command.braceright}{\mbox{\isa{\isacommand{{\isacharbraceright}}}}} \\
   591     & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \hyperlink{command.next}{\mbox{\isa{\isacommand{next}}}} \\
   592     & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}~\isa{{\isachardoublequote}name\ {\isacharequal}\ facts{\isachardoublequote}} \\
   593     & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \hyperlink{command.let}{\mbox{\isa{\isacommand{let}}}}~\isa{{\isachardoublequote}term\ {\isacharequal}\ term{\isachardoublequote}} \\
   594     & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{{\isachardoublequote}var\isactrlsup {\isacharplus}{\isachardoublequote}} \\
   595     & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isachardoublequote}{\isasymguillemotleft}inference{\isasymguillemotright}\ name{\isacharcolon}\ props{\isachardoublequote}} \\
   596     & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharquery}{\isachardoublequote}}~\isa{goal} \\
   597     \isa{goal} & = & \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}~\isa{{\isachardoublequote}name{\isacharcolon}\ props\ proof{\isachardoublequote}} \\
   598     & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}~\isa{{\isachardoublequote}name{\isacharcolon}\ props\ proof{\isachardoublequote}} \\
   599   \end{tabular}
   600 
   601   \medskip Simultaneous propositions or facts may be separated by the
   602   \hyperlink{keyword.and}{\mbox{\isa{\isakeyword{and}}}} keyword.
   603 
   604   \medskip The syntax for terms and propositions is inherited from
   605   Pure (and the object-logic).  A \isa{{\isachardoublequote}pattern{\isachardoublequote}} is a \isa{{\isachardoublequote}term{\isachardoublequote}} with schematic variables, to be bound by higher-order
   606   matching.
   607 
   608   \medskip Facts may be referenced by name or proposition.  For
   609   example, the result of ``\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ A\ {\isasymlangle}proof{\isasymrangle}{\isachardoublequote}}''
   610   becomes available both as \isa{{\isachardoublequote}a{\isachardoublequote}} and
   611   \isacharbackquoteopen\isa{{\isachardoublequote}A{\isachardoublequote}}\isacharbackquoteclose.  Moreover,
   612   fact expressions may involve attributes that modify either the
   613   theorem or the background context.  For example, the expression
   614   ``\isa{{\isachardoublequote}a\ {\isacharbrackleft}OF\ b{\isacharbrackright}{\isachardoublequote}}'' refers to the composition of two facts
   615   according to the \hyperlink{inference.resolution}{\mbox{\isa{resolution}}} inference of
   616   \secref{sec:framework-resolution}, while ``\isa{{\isachardoublequote}a\ {\isacharbrackleft}intro{\isacharbrackright}{\isachardoublequote}}''
   617   declares a fact as introduction rule in the context.
   618 
   619   The special fact called ``\hyperlink{fact.this}{\mbox{\isa{this}}}'' always refers to the last
   620   result, as produced by \hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}, \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}, \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}, or \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}.  Since \hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}} occurs
   621   frequently together with \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}} we provide some
   622   abbreviations:
   623 
   624   \medskip
   625   \begin{tabular}{rcl}
   626     \hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{a} & \isa{{\isachardoublequote}{\isasymequiv}{\isachardoublequote}} & \hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}~\isa{a}~\hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}} \\
   627     \hyperlink{command.with}{\mbox{\isa{\isacommand{with}}}}~\isa{a} & \isa{{\isachardoublequote}{\isasymequiv}{\isachardoublequote}} & \hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{{\isachardoublequote}a\ {\isasymAND}\ this{\isachardoublequote}} \\
   628   \end{tabular}
   629   \medskip
   630 
   631   The \isa{{\isachardoublequote}method{\isachardoublequote}} category is essentially a parameter and may be
   632   populated later.  Methods use the facts indicated by \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}} or \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}, and then operate on the goal state.
   633   Some basic methods are predefined: ``\hyperlink{method.-}{\mbox{\isa{{\isacharminus}}}}'' leaves the goal
   634   unchanged, ``\hyperlink{method.this}{\mbox{\isa{this}}}'' applies the facts as rules to the
   635   goal, ``\hyperlink{method.rule}{\mbox{\isa{rule}}}'' applies the facts to another rule and the
   636   result to the goal (both ``\hyperlink{method.this}{\mbox{\isa{this}}}'' and ``\hyperlink{method.rule}{\mbox{\isa{rule}}}''
   637   refer to \hyperlink{inference.resolution}{\mbox{\isa{resolution}}} of
   638   \secref{sec:framework-resolution}).  The secondary arguments to
   639   ``\hyperlink{method.rule}{\mbox{\isa{rule}}}'' may be specified explicitly as in ``\isa{{\isachardoublequote}{\isacharparenleft}rule\ a{\isacharparenright}{\isachardoublequote}}'', or picked from the context.  In the latter case, the system
   640   first tries rules declared as \hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}} or
   641   \hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}}, followed by those declared as \hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}}.
   642 
   643   The default method for \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}} is ``\hyperlink{method.rule}{\mbox{\isa{rule}}}''
   644   (arguments picked from the context), for \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}} it is
   645   ``\hyperlink{method.-}{\mbox{\isa{{\isacharminus}}}}''.  Further abbreviations for terminal proof steps
   646   are ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isachardoublequote}method\isactrlsub {\isadigit{1}}\ method\isactrlsub {\isadigit{2}}{\isachardoublequote}}'' for
   647   ``\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isachardoublequote}method\isactrlsub {\isadigit{1}}{\isachardoublequote}}~\hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}~\isa{{\isachardoublequote}method\isactrlsub {\isadigit{2}}{\isachardoublequote}}'', and ``\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}}'' for ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\hyperlink{method.rule}{\mbox{\isa{rule}}}, and ``\hyperlink{command.dot}{\mbox{\isa{\isacommand{{\isachardot}}}}}'' for ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\hyperlink{method.this}{\mbox{\isa{this}}}''.  The \hyperlink{command.unfolding}{\mbox{\isa{\isacommand{unfolding}}}} element operates
   648   directly on the current facts and goal by applying equalities.
   649 
   650   \medskip Block structure can be indicated explicitly by ``\hyperlink{command.braceleft}{\mbox{\isa{\isacommand{{\isacharbraceleft}}}}}~\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}~\hyperlink{command.braceright}{\mbox{\isa{\isacommand{{\isacharbraceright}}}}}'', although the body of a sub-proof
   651   already involves implicit nesting.  In any case, \hyperlink{command.next}{\mbox{\isa{\isacommand{next}}}}
   652   jumps into the next section of a block, i.e.\ it acts like closing
   653   an implicit block scope and opening another one; there is no direct
   654   correspondence to subgoals here.
   655 
   656   The remaining elements \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}} and \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}} build up
   657   a local context (see \secref{sec:framework-context}), while
   658   \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}} refines a pending sub-goal by the rule resulting
   659   from a nested sub-proof (see \secref{sec:framework-subproof}).
   660   Further derived concepts will support calculational reasoning (see
   661   \secref{sec:framework-calc}).%
   662 \end{isamarkuptext}%
   663 \isamarkuptrue%
   664 %
   665 \isamarkupsubsection{Context elements \label{sec:framework-context}%
   666 }
   667 \isamarkuptrue%
   668 %
   669 \begin{isamarkuptext}%
   670 In judgments \isa{{\isachardoublequote}{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}{\isachardoublequote}} of the primitive framework, \isa{{\isachardoublequote}{\isasymGamma}{\isachardoublequote}}
   671   essentially acts like a proof context.  Isar elaborates this idea
   672   towards a higher-level notion, with additional information for
   673   type-inference, term abbreviations, local facts, hypotheses etc.
   674 
   675   The element \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}{\isachardoublequote}} declares a local
   676   parameter, i.e.\ an arbitrary-but-fixed entity of a given type; in
   677   results exported from the context, \isa{{\isachardoublequote}x{\isachardoublequote}} may become anything.
   678   The \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isachardoublequote}{\isasymguillemotleft}inference{\isasymguillemotright}{\isachardoublequote}} element provides a
   679   general interface to hypotheses: ``\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isachardoublequote}{\isasymguillemotleft}inference{\isasymguillemotright}\ A{\isachardoublequote}}'' produces \isa{{\isachardoublequote}A\ {\isasymturnstile}\ A{\isachardoublequote}} locally, while the
   680   included inference tells how to discharge \isa{A} from results
   681   \isa{{\isachardoublequote}A\ {\isasymturnstile}\ B{\isachardoublequote}} later on.  There is no user-syntax for \isa{{\isachardoublequote}{\isasymguillemotleft}inference{\isasymguillemotright}{\isachardoublequote}}, i.e.\ it may only occur internally when derived
   682   commands are defined in ML.
   683 
   684   At the user-level, the default inference for \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}} is
   685   \hyperlink{inference.discharge}{\mbox{\isa{discharge}}} as given below.  The additional variants
   686   \hyperlink{command.presume}{\mbox{\isa{\isacommand{presume}}}} and \hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}} are defined as follows:
   687 
   688   \medskip
   689   \begin{tabular}{rcl}
   690     \hyperlink{command.presume}{\mbox{\isa{\isacommand{presume}}}}~\isa{A} & \isa{{\isachardoublequote}{\isasymequiv}{\isachardoublequote}} & \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isachardoublequote}{\isasymguillemotleft}weak{\isasymdash}discharge{\isasymguillemotright}\ A{\isachardoublequote}} \\
   691     \hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}}~\isa{{\isachardoublequote}x\ {\isasymequiv}\ a{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymequiv}{\isachardoublequote}} & \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{x}~\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isachardoublequote}{\isasymguillemotleft}expansion{\isasymguillemotright}\ x\ {\isasymequiv}\ a{\isachardoublequote}} \\
   692   \end{tabular}
   693   \medskip
   694 
   695   \[
   696   \infer[(\indexdef{}{inference}{discharge}\hypertarget{inference.discharge}{\hyperlink{inference.discharge}{\mbox{\isa{discharge}}}})]{\isa{{\isachardoublequote}{\isasymstrut}{\isasymGamma}\ {\isacharminus}\ A\ {\isasymturnstile}\ {\isacharhash}A\ {\isasymLongrightarrow}\ B{\isachardoublequote}}}{\isa{{\isachardoublequote}{\isasymstrut}{\isasymGamma}\ {\isasymturnstile}\ B{\isachardoublequote}}}
   697   \]
   698   \[
   699   \infer[(\indexdef{}{inference}{weak-discharge}\hypertarget{inference.weak-discharge}{\hyperlink{inference.weak-discharge}{\mbox{\isa{weak{\isasymdash}discharge}}}})]{\isa{{\isachardoublequote}{\isasymstrut}{\isasymGamma}\ {\isacharminus}\ A\ {\isasymturnstile}\ A\ {\isasymLongrightarrow}\ B{\isachardoublequote}}}{\isa{{\isachardoublequote}{\isasymstrut}{\isasymGamma}\ {\isasymturnstile}\ B{\isachardoublequote}}}
   700   \]
   701   \[
   702   \infer[(\indexdef{}{inference}{expansion}\hypertarget{inference.expansion}{\hyperlink{inference.expansion}{\mbox{\isa{expansion}}}})]{\isa{{\isachardoublequote}{\isasymstrut}{\isasymGamma}\ {\isacharminus}\ {\isacharparenleft}x\ {\isasymequiv}\ a{\isacharparenright}\ {\isasymturnstile}\ B\ a{\isachardoublequote}}}{\isa{{\isachardoublequote}{\isasymstrut}{\isasymGamma}\ {\isasymturnstile}\ B\ x{\isachardoublequote}}}
   703   \]
   704 
   705   \medskip Note that \hyperlink{inference.discharge}{\mbox{\isa{discharge}}} and \hyperlink{inference.weak-discharge}{\mbox{\isa{weak{\isasymdash}discharge}}} differ in the marker for \isa{A}, which is
   706   relevant when the result of a \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}-\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}-\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}} outline is composed with a pending goal,
   707   cf.\ \secref{sec:framework-subproof}.
   708 
   709   The most interesting derived context element in Isar is \hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}} \cite[\S5.3]{Wenzel-PhD}, which supports generalized
   710   elimination steps in a purely forward manner.  The \hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}}
   711   command takes a specification of parameters \isa{{\isachardoublequote}\isactrlvec x{\isachardoublequote}} and
   712   assumptions \isa{{\isachardoublequote}\isactrlvec A{\isachardoublequote}} to be added to the context, together
   713   with a proof of a case rule stating that this extension is
   714   conservative (i.e.\ may be removed from closed results later on):
   715 
   716   \medskip
   717   \begin{tabular}{l}
   718   \isa{{\isachardoublequote}{\isasymlangle}facts{\isasymrangle}{\isachardoublequote}}~~\hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}}~\isa{{\isachardoublequote}\isactrlvec x\ {\isasymWHERE}\ \isactrlvec A\ \isactrlvec x\ \ {\isasymlangle}proof{\isasymrangle}\ {\isasymequiv}{\isachardoublequote}} \\[0.5ex]
   719   \quad \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}~\isa{{\isachardoublequote}case{\isacharcolon}\ {\isasymAnd}thesis{\isachardot}\ {\isacharparenleft}{\isasymAnd}\isactrlvec x{\isachardot}\ \isactrlvec A\ \isactrlvec x\ {\isasymLongrightarrow}\ thesis{\isacharparenright}\ {\isasymLongrightarrow}\ thesis{\isasymrangle}{\isachardoublequote}} \\
   720   \quad \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\hyperlink{method.-}{\mbox{\isa{{\isacharminus}}}} \\
   721   \qquad \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{thesis} \\
   722   \qquad \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isachardoublequote}{\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\ {\isasymAnd}\isactrlvec x{\isachardot}\ \isactrlvec A\ \isactrlvec x\ {\isasymLongrightarrow}\ thesis{\isachardoublequote}} \\
   723   \qquad \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}~\isa{thesis}~\hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}~\isa{{\isachardoublequote}{\isasymlangle}facts{\isasymrangle}\ {\isasymlangle}proof{\isasymrangle}{\isachardoublequote}} \\
   724   \quad \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}} \\
   725   \quad \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{{\isachardoublequote}\isactrlvec x{\isachardoublequote}}~\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isachardoublequote}{\isasymguillemotleft}elimination\ case{\isasymguillemotright}\ \isactrlvec A\ \isactrlvec x{\isachardoublequote}} \\
   726   \end{tabular}
   727   \medskip
   728 
   729   \[
   730   \infer[(\hyperlink{inference.elimination}{\mbox{\isa{elimination}}})]{\isa{{\isachardoublequote}{\isasymGamma}\ {\isasymturnstile}\ B{\isachardoublequote}}}{
   731     \begin{tabular}{rl}
   732     \isa{{\isachardoublequote}case{\isacharcolon}{\isachardoublequote}} &
   733     \isa{{\isachardoublequote}{\isasymGamma}\ {\isasymturnstile}\ {\isasymAnd}thesis{\isachardot}\ {\isacharparenleft}{\isasymAnd}\isactrlvec x{\isachardot}\ \isactrlvec A\ \isactrlvec x\ {\isasymLongrightarrow}\ thesis{\isacharparenright}\ {\isasymLongrightarrow}\ thesis{\isachardoublequote}} \\[0.2ex]
   734     \isa{{\isachardoublequote}result{\isacharcolon}{\isachardoublequote}} &
   735     \isa{{\isachardoublequote}{\isasymGamma}\ {\isasymunion}\ \isactrlvec A\ \isactrlvec y\ {\isasymturnstile}\ B{\isachardoublequote}} \\[0.2ex]
   736     \end{tabular}}
   737   \]
   738 
   739   \noindent Here the name ``\isa{thesis}'' is a specific convention
   740   for an arbitrary-but-fixed proposition; in the primitive natural
   741   deduction rules shown before we have occasionally used \isa{C}.
   742   The whole statement of ``\hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}}~\isa{x}~\hyperlink{keyword.where}{\mbox{\isa{\isakeyword{where}}}}~\isa{{\isachardoublequote}A\ x{\isachardoublequote}}'' may be read as a claim that \isa{{\isachardoublequote}A\ x{\isachardoublequote}}
   743   may be assumed for some arbitrary-but-fixed \isa{{\isachardoublequote}x{\isachardoublequote}}.  Also note
   744   that ``\hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}}~\isa{{\isachardoublequote}A\ {\isasymAND}\ B{\isachardoublequote}}'' without parameters
   745   is similar to ``\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}~\isa{{\isachardoublequote}A\ {\isasymAND}\ B{\isachardoublequote}}'', but the
   746   latter involves multiple sub-goals.
   747 
   748   \medskip The subsequent Isar proof texts explain all context
   749   elements introduced above using the formal proof language itself.
   750   After finishing a local proof within a block, we indicate the
   751   exported result via \hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}.%
   752 \end{isamarkuptext}%
   753 \isamarkuptrue%
   754 %
   755 \isadelimproof
   756 %
   757 \endisadelimproof
   758 %
   759 \isatagproof
   760 %
   761 \begin{minipage}[t]{0.4\textwidth}
   762 \ \ \isacommand{{\isacharbraceleft}}\isamarkupfalse%
   763 \isanewline
   764 \ \ \ \ \isacommand{fix}\isamarkupfalse%
   765 \ x\isanewline
   766 \ \ \ \ \isacommand{have}\isamarkupfalse%
   767 \ {\isachardoublequoteopen}B\ x{\isachardoublequoteclose}%
   768 \endisatagproof
   769 {\isafoldproof}%
   770 %
   771 \isadelimproof
   772 %
   773 \endisadelimproof
   774 %
   775 \isadelimnoproof
   776 \ %
   777 \endisadelimnoproof
   778 %
   779 \isatagnoproof
   780 \isacommand{sorry}\isamarkupfalse%
   781 %
   782 \endisatagnoproof
   783 {\isafoldnoproof}%
   784 %
   785 \isadelimnoproof
   786 \isanewline
   787 %
   788 \endisadelimnoproof
   789 %
   790 \isadelimproof
   791 \ \ %
   792 \endisadelimproof
   793 %
   794 \isatagproof
   795 \isacommand{{\isacharbraceright}}\isamarkupfalse%
   796 \isanewline
   797 \ \ \isacommand{note}\isamarkupfalse%
   798 \ {\isacharbackquoteopen}{\isasymAnd}x{\isachardot}\ B\ x{\isacharbackquoteclose}%
   799 \end{minipage}\quad\begin{minipage}[t]{0.4\textwidth}
   800 \ \ \isacommand{{\isacharbraceleft}}\isamarkupfalse%
   801 \isanewline
   802 \ \ \ \ \isacommand{assume}\isamarkupfalse%
   803 \ A\isanewline
   804 \ \ \ \ \isacommand{have}\isamarkupfalse%
   805 \ B%
   806 \endisatagproof
   807 {\isafoldproof}%
   808 %
   809 \isadelimproof
   810 %
   811 \endisadelimproof
   812 %
   813 \isadelimnoproof
   814 \ %
   815 \endisadelimnoproof
   816 %
   817 \isatagnoproof
   818 \isacommand{sorry}\isamarkupfalse%
   819 %
   820 \endisatagnoproof
   821 {\isafoldnoproof}%
   822 %
   823 \isadelimnoproof
   824 \isanewline
   825 %
   826 \endisadelimnoproof
   827 %
   828 \isadelimproof
   829 \ \ %
   830 \endisadelimproof
   831 %
   832 \isatagproof
   833 \isacommand{{\isacharbraceright}}\isamarkupfalse%
   834 \isanewline
   835 \ \ \isacommand{note}\isamarkupfalse%
   836 \ {\isacharbackquoteopen}A\ {\isasymLongrightarrow}\ B{\isacharbackquoteclose}%
   837 \end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}
   838 \ \ \isacommand{{\isacharbraceleft}}\isamarkupfalse%
   839 \isanewline
   840 \ \ \ \ \isacommand{def}\isamarkupfalse%
   841 \ x\ {\isasymequiv}\ a\isanewline
   842 \ \ \ \ \isacommand{have}\isamarkupfalse%
   843 \ {\isachardoublequoteopen}B\ x{\isachardoublequoteclose}%
   844 \endisatagproof
   845 {\isafoldproof}%
   846 %
   847 \isadelimproof
   848 %
   849 \endisadelimproof
   850 %
   851 \isadelimnoproof
   852 \ %
   853 \endisadelimnoproof
   854 %
   855 \isatagnoproof
   856 \isacommand{sorry}\isamarkupfalse%
   857 %
   858 \endisatagnoproof
   859 {\isafoldnoproof}%
   860 %
   861 \isadelimnoproof
   862 \isanewline
   863 %
   864 \endisadelimnoproof
   865 %
   866 \isadelimproof
   867 \ \ %
   868 \endisadelimproof
   869 %
   870 \isatagproof
   871 \isacommand{{\isacharbraceright}}\isamarkupfalse%
   872 \isanewline
   873 \ \ \isacommand{note}\isamarkupfalse%
   874 \ {\isacharbackquoteopen}B\ a{\isacharbackquoteclose}%
   875 \end{minipage}\quad\begin{minipage}[t]{0.4\textwidth}
   876 \ \ \isacommand{{\isacharbraceleft}}\isamarkupfalse%
   877 \isanewline
   878 \ \ \ \ \isacommand{obtain}\isamarkupfalse%
   879 \ x\ \isakeyword{where}\ {\isachardoublequoteopen}A\ x{\isachardoublequoteclose}%
   880 \endisatagproof
   881 {\isafoldproof}%
   882 %
   883 \isadelimproof
   884 %
   885 \endisadelimproof
   886 %
   887 \isadelimnoproof
   888 \ %
   889 \endisadelimnoproof
   890 %
   891 \isatagnoproof
   892 \isacommand{sorry}\isamarkupfalse%
   893 %
   894 \endisatagnoproof
   895 {\isafoldnoproof}%
   896 %
   897 \isadelimnoproof
   898 \isanewline
   899 %
   900 \endisadelimnoproof
   901 %
   902 \isadelimproof
   903 \ \ \ \ %
   904 \endisadelimproof
   905 %
   906 \isatagproof
   907 \isacommand{have}\isamarkupfalse%
   908 \ B%
   909 \endisatagproof
   910 {\isafoldproof}%
   911 %
   912 \isadelimproof
   913 %
   914 \endisadelimproof
   915 %
   916 \isadelimnoproof
   917 \ %
   918 \endisadelimnoproof
   919 %
   920 \isatagnoproof
   921 \isacommand{sorry}\isamarkupfalse%
   922 %
   923 \endisatagnoproof
   924 {\isafoldnoproof}%
   925 %
   926 \isadelimnoproof
   927 \isanewline
   928 %
   929 \endisadelimnoproof
   930 %
   931 \isadelimproof
   932 \ \ %
   933 \endisadelimproof
   934 %
   935 \isatagproof
   936 \isacommand{{\isacharbraceright}}\isamarkupfalse%
   937 \isanewline
   938 \ \ \isacommand{note}\isamarkupfalse%
   939 \ {\isacharbackquoteopen}B{\isacharbackquoteclose}%
   940 \end{minipage}
   941 %
   942 \endisatagproof
   943 {\isafoldproof}%
   944 %
   945 \isadelimproof
   946 %
   947 \endisadelimproof
   948 %
   949 \begin{isamarkuptext}%
   950 \bigskip\noindent This illustrates the meaning of Isar context
   951   elements without goals getting in between.%
   952 \end{isamarkuptext}%
   953 \isamarkuptrue%
   954 %
   955 \isamarkupsubsection{Structured statements \label{sec:framework-stmt}%
   956 }
   957 \isamarkuptrue%
   958 %
   959 \begin{isamarkuptext}%
   960 The category \isa{{\isachardoublequote}statement{\isachardoublequote}} of top-level theorem specifications
   961   is defined as follows:
   962 
   963   \medskip
   964   \begin{tabular}{rcl}
   965   \isa{{\isachardoublequote}statement{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymequiv}{\isachardoublequote}} & \isa{{\isachardoublequote}name{\isacharcolon}\ props\ {\isasymAND}\ {\isasymdots}{\isachardoublequote}} \\
   966   & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}context\isactrlsup {\isacharasterisk}\ conclusion{\isachardoublequote}} \\[0.5ex]
   967 
   968   \isa{{\isachardoublequote}context{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymequiv}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymFIXES}\ vars\ {\isasymAND}\ {\isasymdots}{\isachardoublequote}} \\
   969   & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymASSUMES}\ name{\isacharcolon}\ props\ {\isasymAND}\ {\isasymdots}{\isachardoublequote}} \\
   970 
   971   \isa{{\isachardoublequote}conclusion{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymequiv}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymSHOWS}\ name{\isacharcolon}\ props\ {\isasymAND}\ {\isasymdots}{\isachardoublequote}} \\
   972   & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymOBTAINS}\ vars\ {\isasymAND}\ {\isasymdots}\ {\isasymWHERE}\ name{\isacharcolon}\ props\ {\isasymAND}\ {\isasymdots}{\isachardoublequote}} \\
   973   & & \quad \isa{{\isachardoublequote}{\isasymBBAR}\ {\isasymdots}{\isachardoublequote}} \\
   974   \end{tabular}
   975 
   976   \medskip\noindent A simple \isa{{\isachardoublequote}statement{\isachardoublequote}} consists of named
   977   propositions.  The full form admits local context elements followed
   978   by the actual conclusions, such as ``\hyperlink{keyword.fixes}{\mbox{\isa{\isakeyword{fixes}}}}~\isa{x}~\hyperlink{keyword.assumes}{\mbox{\isa{\isakeyword{assumes}}}}~\isa{{\isachardoublequote}A\ x{\isachardoublequote}}~\hyperlink{keyword.shows}{\mbox{\isa{\isakeyword{shows}}}}~\isa{{\isachardoublequote}B\ x{\isachardoublequote}}''.  The final result emerges as a Pure rule after discharging
   979   the context: \isa{{\isachardoublequote}{\isasymAnd}x{\isachardot}\ A\ x\ {\isasymLongrightarrow}\ B\ x{\isachardoublequote}}.
   980 
   981   The \hyperlink{keyword.obtains}{\mbox{\isa{\isakeyword{obtains}}}} variant is another abbreviation defined
   982   below; unlike \hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}} (cf.\
   983   \secref{sec:framework-context}) there may be several ``cases''
   984   separated by ``\isa{{\isachardoublequote}{\isasymBBAR}{\isachardoublequote}}'', each consisting of several
   985   parameters (\isa{{\isachardoublequote}vars{\isachardoublequote}}) and several premises (\isa{{\isachardoublequote}props{\isachardoublequote}}).
   986   This specifies multi-branch elimination rules.
   987 
   988   \medskip
   989   \begin{tabular}{l}
   990   \isa{{\isachardoublequote}{\isasymOBTAINS}\ \isactrlvec x\ {\isasymWHERE}\ \isactrlvec A\ \isactrlvec x\ \ \ {\isasymBBAR}\ \ \ {\isasymdots}\ \ \ {\isasymequiv}{\isachardoublequote}} \\[0.5ex]
   991   \quad \isa{{\isachardoublequote}{\isasymFIXES}\ thesis{\isachardoublequote}} \\
   992   \quad \isa{{\isachardoublequote}{\isasymASSUMES}\ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\ {\isasymAnd}\isactrlvec x{\isachardot}\ \isactrlvec A\ \isactrlvec x\ {\isasymLongrightarrow}\ thesis\ \ {\isasymAND}\ \ {\isasymdots}{\isachardoublequote}} \\
   993   \quad \isa{{\isachardoublequote}{\isasymSHOWS}\ thesis{\isachardoublequote}} \\
   994   \end{tabular}
   995   \medskip
   996 
   997   Presenting structured statements in such an ``open'' format usually
   998   simplifies the subsequent proof, because the outer structure of the
   999   problem is already laid out directly.  E.g.\ consider the following
  1000   canonical patterns for \isa{{\isachardoublequote}{\isasymSHOWS}{\isachardoublequote}} and \isa{{\isachardoublequote}{\isasymOBTAINS}{\isachardoublequote}},
  1001   respectively:%
  1002 \end{isamarkuptext}%
  1003 \isamarkuptrue%
  1004 %
  1005 \begin{minipage}{0.5\textwidth}
  1006 \isacommand{theorem}\isamarkupfalse%
  1007 \isanewline
  1008 \ \ \isakeyword{fixes}\ x\ \isakeyword{and}\ y\isanewline
  1009 \ \ \isakeyword{assumes}\ {\isachardoublequoteopen}A\ x{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}B\ y{\isachardoublequoteclose}\isanewline
  1010 \ \ \isakeyword{shows}\ {\isachardoublequoteopen}C\ x\ y{\isachardoublequoteclose}\isanewline
  1011 %
  1012 \isadelimproof
  1013 %
  1014 \endisadelimproof
  1015 %
  1016 \isatagproof
  1017 \isacommand{proof}\isamarkupfalse%
  1018 \ {\isacharminus}\isanewline
  1019 \ \ \isacommand{from}\isamarkupfalse%
  1020 \ {\isacharbackquoteopen}A\ x{\isacharbackquoteclose}\ \isakeyword{and}\ {\isacharbackquoteopen}B\ y{\isacharbackquoteclose}\isanewline
  1021 \ \ \isacommand{show}\isamarkupfalse%
  1022 \ {\isachardoublequoteopen}C\ x\ y{\isachardoublequoteclose}%
  1023 \endisatagproof
  1024 {\isafoldproof}%
  1025 %
  1026 \isadelimproof
  1027 %
  1028 \endisadelimproof
  1029 %
  1030 \isadelimnoproof
  1031 \ %
  1032 \endisadelimnoproof
  1033 %
  1034 \isatagnoproof
  1035 \isacommand{sorry}\isamarkupfalse%
  1036 %
  1037 \endisatagnoproof
  1038 {\isafoldnoproof}%
  1039 %
  1040 \isadelimnoproof
  1041 \isanewline
  1042 %
  1043 \endisadelimnoproof
  1044 %
  1045 \isadelimproof
  1046 %
  1047 \endisadelimproof
  1048 %
  1049 \isatagproof
  1050 \isacommand{qed}\isamarkupfalse%
  1051 %
  1052 \endisatagproof
  1053 {\isafoldproof}%
  1054 %
  1055 \isadelimproof
  1056 %
  1057 \endisadelimproof
  1058 %
  1059 \end{minipage}\begin{minipage}{0.5\textwidth}
  1060 \isacommand{theorem}\isamarkupfalse%
  1061 \isanewline
  1062 \ \ \isakeyword{obtains}\ x\ \isakeyword{and}\ y\isanewline
  1063 \ \ \isakeyword{where}\ {\isachardoublequoteopen}A\ x{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}B\ y{\isachardoublequoteclose}\isanewline
  1064 %
  1065 \isadelimproof
  1066 %
  1067 \endisadelimproof
  1068 %
  1069 \isatagproof
  1070 \isacommand{proof}\isamarkupfalse%
  1071 \ {\isacharminus}\isanewline
  1072 \ \ \isacommand{have}\isamarkupfalse%
  1073 \ {\isachardoublequoteopen}A\ a{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}B\ b{\isachardoublequoteclose}%
  1074 \endisatagproof
  1075 {\isafoldproof}%
  1076 %
  1077 \isadelimproof
  1078 %
  1079 \endisadelimproof
  1080 %
  1081 \isadelimnoproof
  1082 \ %
  1083 \endisadelimnoproof
  1084 %
  1085 \isatagnoproof
  1086 \isacommand{sorry}\isamarkupfalse%
  1087 %
  1088 \endisatagnoproof
  1089 {\isafoldnoproof}%
  1090 %
  1091 \isadelimnoproof
  1092 \isanewline
  1093 %
  1094 \endisadelimnoproof
  1095 %
  1096 \isadelimproof
  1097 \ \ %
  1098 \endisadelimproof
  1099 %
  1100 \isatagproof
  1101 \isacommand{then}\isamarkupfalse%
  1102 \ \isacommand{show}\isamarkupfalse%
  1103 \ thesis\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
  1104 \isanewline
  1105 \isacommand{qed}\isamarkupfalse%
  1106 %
  1107 \endisatagproof
  1108 {\isafoldproof}%
  1109 %
  1110 \isadelimproof
  1111 %
  1112 \endisadelimproof
  1113 %
  1114 \end{minipage}
  1115 %
  1116 \begin{isamarkuptext}%
  1117 \medskip\noindent Here local facts \isacharbackquoteopen\isa{{\isachardoublequote}A\ x{\isachardoublequote}}\isacharbackquoteclose\ and \isacharbackquoteopen\isa{{\isachardoublequote}B\ y{\isachardoublequote}}\isacharbackquoteclose\ are referenced immediately; there is no
  1118   need to decompose the logical rule structure again.  In the second
  1119   proof the final ``\hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}}~\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}~\isa{thesis}~\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}}''  involves the local rule case \isa{{\isachardoublequote}{\isasymAnd}x\ y{\isachardot}\ A\ x\ {\isasymLongrightarrow}\ B\ y\ {\isasymLongrightarrow}\ thesis{\isachardoublequote}} for the particular instance of terms \isa{{\isachardoublequote}a{\isachardoublequote}} and \isa{{\isachardoublequote}b{\isachardoublequote}} produced in the body.%
  1120 \end{isamarkuptext}%
  1121 \isamarkuptrue%
  1122 %
  1123 \isamarkupsubsection{Structured proof refinement \label{sec:framework-subproof}%
  1124 }
  1125 \isamarkuptrue%
  1126 %
  1127 \begin{isamarkuptext}%
  1128 By breaking up the grammar for the Isar proof language, we may
  1129   understand a proof text as a linear sequence of individual proof
  1130   commands.  These are interpreted as transitions of the Isar virtual
  1131   machine (Isar/VM), which operates on a block-structured
  1132   configuration in single steps.  This allows users to write proof
  1133   texts in an incremental manner, and inspect intermediate
  1134   configurations for debugging.
  1135 
  1136   The basic idea is analogous to evaluating algebraic expressions on a
  1137   stack machine: \isa{{\isachardoublequote}{\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ {\isasymcdot}\ c{\isachardoublequote}} then corresponds to a sequence
  1138   of single transitions for each symbol \isa{{\isachardoublequote}{\isacharparenleft}{\isacharcomma}\ a{\isacharcomma}\ {\isacharplus}{\isacharcomma}\ b{\isacharcomma}\ {\isacharparenright}{\isacharcomma}\ {\isasymcdot}{\isacharcomma}\ c{\isachardoublequote}}.
  1139   In Isar the algebraic values are facts or goals, and the operations
  1140   are inferences.
  1141 
  1142   \medskip The Isar/VM state maintains a stack of nodes, each node
  1143   contains the local proof context, the linguistic mode, and a pending
  1144   goal (optional).  The mode determines the type of transition that
  1145   may be performed next, it essentially alternates between forward and
  1146   backward reasoning, with an intermediate stage for chained facts
  1147   (see \figref{fig:isar-vm}).
  1148 
  1149   \begin{figure}[htb]
  1150   \begin{center}
  1151   \includegraphics[width=0.8\textwidth]{Thy/document/isar-vm}
  1152   \end{center}
  1153   \caption{Isar/VM modes}\label{fig:isar-vm}
  1154   \end{figure}
  1155 
  1156   For example, in \isa{{\isachardoublequote}state{\isachardoublequote}} mode Isar acts like a mathematical
  1157   scratch-pad, accepting declarations like \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}, \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}, and claims like \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}, \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}.  A goal
  1158   statement changes the mode to \isa{{\isachardoublequote}prove{\isachardoublequote}}, which means that we
  1159   may now refine the problem via \hyperlink{command.unfolding}{\mbox{\isa{\isacommand{unfolding}}}} or \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}.  Then we are again in \isa{{\isachardoublequote}state{\isachardoublequote}} mode of a proof body,
  1160   which may issue \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}} statements to solve pending
  1161   sub-goals.  A concluding \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}} will return to the original
  1162   \isa{{\isachardoublequote}state{\isachardoublequote}} mode one level upwards.  The subsequent Isar/VM
  1163   trace indicates block structure, linguistic mode, goal state, and
  1164   inferences:%
  1165 \end{isamarkuptext}%
  1166 \isamarkuptrue%
  1167 %
  1168 \begingroup\footnotesize
  1169 %
  1170 \isadelimproof
  1171 %
  1172 \endisadelimproof
  1173 %
  1174 \isatagproof
  1175 %
  1176 \begin{minipage}[t]{0.18\textwidth}
  1177 \ \ \isacommand{have}\isamarkupfalse%
  1178 \ {\isachardoublequoteopen}A\ {\isasymlongrightarrow}\ B{\isachardoublequoteclose}\isanewline
  1179 \ \ \isacommand{proof}\isamarkupfalse%
  1180 \isanewline
  1181 \ \ \ \ \isacommand{assume}\isamarkupfalse%
  1182 \ A\isanewline
  1183 \ \ \ \ \isacommand{show}\isamarkupfalse%
  1184 \ B%
  1185 \endisatagproof
  1186 {\isafoldproof}%
  1187 %
  1188 \isadelimproof
  1189 %
  1190 \endisadelimproof
  1191 \isanewline
  1192 %
  1193 \isadelimnoproof
  1194 \ \ \ \ \ \ %
  1195 \endisadelimnoproof
  1196 %
  1197 \isatagnoproof
  1198 \isacommand{sorry}\isamarkupfalse%
  1199 %
  1200 \endisatagnoproof
  1201 {\isafoldnoproof}%
  1202 %
  1203 \isadelimnoproof
  1204 %
  1205 \endisadelimnoproof
  1206 \isanewline
  1207 %
  1208 \isadelimproof
  1209 \ \ %
  1210 \endisadelimproof
  1211 %
  1212 \isatagproof
  1213 \isacommand{qed}\isamarkupfalse%
  1214 %
  1215 \end{minipage}\quad
  1216 \begin{minipage}[t]{0.06\textwidth}
  1217 \isa{{\isachardoublequote}begin{\isachardoublequote}} \\
  1218 \\
  1219 \\
  1220 \isa{{\isachardoublequote}begin{\isachardoublequote}} \\
  1221 \isa{{\isachardoublequote}end{\isachardoublequote}} \\
  1222 \isa{{\isachardoublequote}end{\isachardoublequote}} \\
  1223 \end{minipage}
  1224 \begin{minipage}[t]{0.08\textwidth}
  1225 \isa{{\isachardoublequote}prove{\isachardoublequote}} \\
  1226 \isa{{\isachardoublequote}state{\isachardoublequote}} \\
  1227 \isa{{\isachardoublequote}state{\isachardoublequote}} \\
  1228 \isa{{\isachardoublequote}prove{\isachardoublequote}} \\
  1229 \isa{{\isachardoublequote}state{\isachardoublequote}} \\
  1230 \isa{{\isachardoublequote}state{\isachardoublequote}} \\
  1231 \end{minipage}\begin{minipage}[t]{0.35\textwidth}
  1232 \isa{{\isachardoublequote}{\isacharparenleft}A\ {\isasymlongrightarrow}\ B{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharhash}{\isacharparenleft}A\ {\isasymlongrightarrow}\ B{\isacharparenright}{\isachardoublequote}} \\
  1233 \isa{{\isachardoublequote}{\isacharparenleft}A\ {\isasymLongrightarrow}\ B{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharhash}{\isacharparenleft}A\ {\isasymlongrightarrow}\ B{\isacharparenright}{\isachardoublequote}} \\
  1234 \\
  1235 \\
  1236 \isa{{\isachardoublequote}{\isacharhash}{\isacharparenleft}A\ {\isasymlongrightarrow}\ B{\isacharparenright}{\isachardoublequote}} \\
  1237 \isa{{\isachardoublequote}A\ {\isasymlongrightarrow}\ B{\isachardoublequote}} \\
  1238 \end{minipage}\begin{minipage}[t]{0.4\textwidth}
  1239 \isa{{\isachardoublequote}{\isacharparenleft}init{\isacharparenright}{\isachardoublequote}} \\
  1240 \isa{{\isachardoublequote}{\isacharparenleft}resolution\ impI{\isacharparenright}{\isachardoublequote}} \\
  1241 \\
  1242 \\
  1243 \isa{{\isachardoublequote}{\isacharparenleft}refinement\ {\isacharhash}A\ {\isasymLongrightarrow}\ B{\isacharparenright}{\isachardoublequote}} \\
  1244 \isa{{\isachardoublequote}{\isacharparenleft}finish{\isacharparenright}{\isachardoublequote}} \\
  1245 \end{minipage}
  1246 %
  1247 \endisatagproof
  1248 {\isafoldproof}%
  1249 %
  1250 \isadelimproof
  1251 %
  1252 \endisadelimproof
  1253 %
  1254 \endgroup
  1255 %
  1256 \begin{isamarkuptext}%
  1257 \noindent Here the \hyperlink{inference.refinement}{\mbox{\isa{refinement}}} inference from
  1258   \secref{sec:framework-resolution} mediates composition of Isar
  1259   sub-proofs nicely.  Observe that this principle incorporates some
  1260   degree of freedom in proof composition.  In particular, the proof
  1261   body allows parameters and assumptions to be re-ordered, or commuted
  1262   according to Hereditary Harrop Form.  Moreover, context elements
  1263   that are not used in a sub-proof may be omitted altogether.  For
  1264   example:%
  1265 \end{isamarkuptext}%
  1266 \isamarkuptrue%
  1267 %
  1268 \begin{minipage}{0.5\textwidth}
  1269 %
  1270 \isadelimproof
  1271 \ \ %
  1272 \endisadelimproof
  1273 %
  1274 \isatagproof
  1275 \isacommand{have}\isamarkupfalse%
  1276 \ {\isachardoublequoteopen}{\isasymAnd}x\ y{\isachardot}\ A\ x\ {\isasymLongrightarrow}\ B\ y\ {\isasymLongrightarrow}\ C\ x\ y{\isachardoublequoteclose}\isanewline
  1277 \ \ \isacommand{proof}\isamarkupfalse%
  1278 \ {\isacharminus}\isanewline
  1279 \ \ \ \ \isacommand{fix}\isamarkupfalse%
  1280 \ x\ \isakeyword{and}\ y\isanewline
  1281 \ \ \ \ \isacommand{assume}\isamarkupfalse%
  1282 \ {\isachardoublequoteopen}A\ x{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}B\ y{\isachardoublequoteclose}\isanewline
  1283 \ \ \ \ \isacommand{show}\isamarkupfalse%
  1284 \ {\isachardoublequoteopen}C\ x\ y{\isachardoublequoteclose}%
  1285 \endisatagproof
  1286 {\isafoldproof}%
  1287 %
  1288 \isadelimproof
  1289 %
  1290 \endisadelimproof
  1291 %
  1292 \isadelimnoproof
  1293 \ %
  1294 \endisadelimnoproof
  1295 %
  1296 \isatagnoproof
  1297 \isacommand{sorry}\isamarkupfalse%
  1298 %
  1299 \endisatagnoproof
  1300 {\isafoldnoproof}%
  1301 %
  1302 \isadelimnoproof
  1303 %
  1304 \endisadelimnoproof
  1305 \isanewline
  1306 %
  1307 \isadelimproof
  1308 \ \ %
  1309 \endisadelimproof
  1310 %
  1311 \isatagproof
  1312 \isacommand{qed}\isamarkupfalse%
  1313 %
  1314 \end{minipage}\begin{minipage}{0.5\textwidth}
  1315 \ \ \isacommand{have}\isamarkupfalse%
  1316 \ {\isachardoublequoteopen}{\isasymAnd}x\ y{\isachardot}\ A\ x\ {\isasymLongrightarrow}\ B\ y\ {\isasymLongrightarrow}\ C\ x\ y{\isachardoublequoteclose}\isanewline
  1317 \ \ \isacommand{proof}\isamarkupfalse%
  1318 \ {\isacharminus}\isanewline
  1319 \ \ \ \ \isacommand{fix}\isamarkupfalse%
  1320 \ x\ \isacommand{assume}\isamarkupfalse%
  1321 \ {\isachardoublequoteopen}A\ x{\isachardoublequoteclose}\isanewline
  1322 \ \ \ \ \isacommand{fix}\isamarkupfalse%
  1323 \ y\ \isacommand{assume}\isamarkupfalse%
  1324 \ {\isachardoublequoteopen}B\ y{\isachardoublequoteclose}\isanewline
  1325 \ \ \ \ \isacommand{show}\isamarkupfalse%
  1326 \ {\isachardoublequoteopen}C\ x\ y{\isachardoublequoteclose}%
  1327 \endisatagproof
  1328 {\isafoldproof}%
  1329 %
  1330 \isadelimproof
  1331 %
  1332 \endisadelimproof
  1333 %
  1334 \isadelimnoproof
  1335 \ %
  1336 \endisadelimnoproof
  1337 %
  1338 \isatagnoproof
  1339 \isacommand{sorry}\isamarkupfalse%
  1340 %
  1341 \endisatagnoproof
  1342 {\isafoldnoproof}%
  1343 %
  1344 \isadelimnoproof
  1345 %
  1346 \endisadelimnoproof
  1347 \isanewline
  1348 %
  1349 \isadelimproof
  1350 \ \ %
  1351 \endisadelimproof
  1352 %
  1353 \isatagproof
  1354 \isacommand{qed}\isamarkupfalse%
  1355 %
  1356 \end{minipage}\\[3ex]\begin{minipage}{0.5\textwidth}
  1357 \ \ \isacommand{have}\isamarkupfalse%
  1358 \ {\isachardoublequoteopen}{\isasymAnd}x\ y{\isachardot}\ A\ x\ {\isasymLongrightarrow}\ B\ y\ {\isasymLongrightarrow}\ C\ x\ y{\isachardoublequoteclose}\isanewline
  1359 \ \ \isacommand{proof}\isamarkupfalse%
  1360 \ {\isacharminus}\isanewline
  1361 \ \ \ \ \isacommand{fix}\isamarkupfalse%
  1362 \ y\ \isacommand{assume}\isamarkupfalse%
  1363 \ {\isachardoublequoteopen}B\ y{\isachardoublequoteclose}\isanewline
  1364 \ \ \ \ \isacommand{fix}\isamarkupfalse%
  1365 \ x\ \isacommand{assume}\isamarkupfalse%
  1366 \ {\isachardoublequoteopen}A\ x{\isachardoublequoteclose}\isanewline
  1367 \ \ \ \ \isacommand{show}\isamarkupfalse%
  1368 \ {\isachardoublequoteopen}C\ x\ y{\isachardoublequoteclose}\ \isacommand{sorry}\isamarkupfalse%
  1369 \isanewline
  1370 \ \ \isacommand{qed}\isamarkupfalse%
  1371 %
  1372 \end{minipage}\begin{minipage}{0.5\textwidth}
  1373 \ \ \isacommand{have}\isamarkupfalse%
  1374 \ {\isachardoublequoteopen}{\isasymAnd}x\ y{\isachardot}\ A\ x\ {\isasymLongrightarrow}\ B\ y\ {\isasymLongrightarrow}\ C\ x\ y{\isachardoublequoteclose}\isanewline
  1375 \ \ \isacommand{proof}\isamarkupfalse%
  1376 \ {\isacharminus}\isanewline
  1377 \ \ \ \ \isacommand{fix}\isamarkupfalse%
  1378 \ y\ \isacommand{assume}\isamarkupfalse%
  1379 \ {\isachardoublequoteopen}B\ y{\isachardoublequoteclose}\isanewline
  1380 \ \ \ \ \isacommand{fix}\isamarkupfalse%
  1381 \ x\isanewline
  1382 \ \ \ \ \isacommand{show}\isamarkupfalse%
  1383 \ {\isachardoublequoteopen}C\ x\ y{\isachardoublequoteclose}\ \isacommand{sorry}\isamarkupfalse%
  1384 \isanewline
  1385 \ \ \isacommand{qed}\isamarkupfalse%
  1386 %
  1387 \endisatagproof
  1388 {\isafoldproof}%
  1389 %
  1390 \isadelimproof
  1391 %
  1392 \endisadelimproof
  1393 %
  1394 \end{minipage}
  1395 %
  1396 \begin{isamarkuptext}%
  1397 \medskip\noindent Such ``peephole optimizations'' of Isar texts are
  1398   practically important to improve readability, by rearranging
  1399   contexts elements according to the natural flow of reasoning in the
  1400   body, while still observing the overall scoping rules.
  1401 
  1402   \medskip This illustrates the basic idea of structured proof
  1403   processing in Isar.  The main mechanisms are based on natural
  1404   deduction rule composition within the Pure framework.  In
  1405   particular, there are no direct operations on goal states within the
  1406   proof body.  Moreover, there is no hidden automated reasoning
  1407   involved, just plain unification.%
  1408 \end{isamarkuptext}%
  1409 \isamarkuptrue%
  1410 %
  1411 \isamarkupsubsection{Calculational reasoning \label{sec:framework-calc}%
  1412 }
  1413 \isamarkuptrue%
  1414 %
  1415 \begin{isamarkuptext}%
  1416 The existing Isar infrastructure is sufficiently flexible to support
  1417   calculational reasoning (chains of transitivity steps) as derived
  1418   concept.  The generic proof elements introduced below depend on
  1419   rules declared as \hyperlink{attribute.trans}{\mbox{\isa{trans}}} in the context.  It is left to
  1420   the object-logic to provide a suitable rule collection for mixed
  1421   relations of \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}}, \isa{{\isachardoublequote}{\isacharless}{\isachardoublequote}}, \isa{{\isachardoublequote}{\isasymle}{\isachardoublequote}}, \isa{{\isachardoublequote}{\isasymsubset}{\isachardoublequote}},
  1422   \isa{{\isachardoublequote}{\isasymsubseteq}{\isachardoublequote}} etc.  Due to the flexibility of rule composition
  1423   (\secref{sec:framework-resolution}), substitution of equals by
  1424   equals is covered as well, even substitution of inequalities
  1425   involving monotonicity conditions; see also \cite[\S6]{Wenzel-PhD}
  1426   and \cite{Bauer-Wenzel:2001}.
  1427 
  1428   The generic calculational mechanism is based on the observation that
  1429   rules such as \isa{{\isachardoublequote}trans{\isacharcolon}{\isachardoublequote}}~\isa{{\isachardoublequote}x\ {\isacharequal}\ y\ {\isasymLongrightarrow}\ y\ {\isacharequal}\ z\ {\isasymLongrightarrow}\ x\ {\isacharequal}\ z{\isachardoublequote}}
  1430   proceed from the premises towards the conclusion in a deterministic
  1431   fashion.  Thus we may reason in forward mode, feeding intermediate
  1432   results into rules selected from the context.  The course of
  1433   reasoning is organized by maintaining a secondary fact called
  1434   ``\hyperlink{fact.calculation}{\mbox{\isa{calculation}}}'', apart from the primary ``\hyperlink{fact.this}{\mbox{\isa{this}}}''
  1435   already provided by the Isar primitives.  In the definitions below,
  1436   \hyperlink{attribute.OF}{\mbox{\isa{OF}}} refers to \hyperlink{inference.resolution}{\mbox{\isa{resolution}}}
  1437   (\secref{sec:framework-resolution}) with multiple rule arguments,
  1438   and \isa{{\isachardoublequote}trans{\isachardoublequote}} represents to a suitable rule from the context:
  1439 
  1440   \begin{matharray}{rcl}
  1441     \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}}\isa{{\isachardoublequote}\isactrlsub {\isadigit{0}}{\isachardoublequote}} & \equiv & \hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}~\isa{{\isachardoublequote}calculation\ {\isacharequal}\ this{\isachardoublequote}} \\
  1442     \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}}\isa{{\isachardoublequote}\isactrlsub n\isactrlsub {\isacharplus}\isactrlsub {\isadigit{1}}{\isachardoublequote}} & \equiv & \hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}}~\isa{{\isachardoublequote}calculation\ {\isacharequal}\ trans\ {\isacharbrackleft}OF\ calculation\ this{\isacharbrackright}{\isachardoublequote}} \\[0.5ex]
  1443     \hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}} & \equiv & \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}}~\hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{calculation} \\
  1444   \end{matharray}
  1445 
  1446   \noindent The start of a calculation is determined implicitly in the
  1447   text: here \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}} sets \hyperlink{fact.calculation}{\mbox{\isa{calculation}}} to the current
  1448   result; any subsequent occurrence will update \hyperlink{fact.calculation}{\mbox{\isa{calculation}}} by
  1449   combination with the next result and a transitivity rule.  The
  1450   calculational sequence is concluded via \hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}}, where
  1451   the final result is exposed for use in a concluding claim.
  1452 
  1453   Here is a canonical proof pattern, using \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}} to
  1454   establish the intermediate results:%
  1455 \end{isamarkuptext}%
  1456 \isamarkuptrue%
  1457 %
  1458 \isadelimproof
  1459 \ \ %
  1460 \endisadelimproof
  1461 %
  1462 \isatagproof
  1463 \isacommand{have}\isamarkupfalse%
  1464 \ {\isachardoublequoteopen}a\ {\isacharequal}\ b{\isachardoublequoteclose}\ \isacommand{sorry}\isamarkupfalse%
  1465 \isanewline
  1466 \ \ \isacommand{also}\isamarkupfalse%
  1467 \ \isacommand{have}\isamarkupfalse%
  1468 \ {\isachardoublequoteopen}{\isasymdots}\ {\isacharequal}\ c{\isachardoublequoteclose}\ \isacommand{sorry}\isamarkupfalse%
  1469 \isanewline
  1470 \ \ \isacommand{also}\isamarkupfalse%
  1471 \ \isacommand{have}\isamarkupfalse%
  1472 \ {\isachardoublequoteopen}{\isasymdots}\ {\isacharequal}\ d{\isachardoublequoteclose}\ \isacommand{sorry}\isamarkupfalse%
  1473 \isanewline
  1474 \ \ \isacommand{finally}\isamarkupfalse%
  1475 \ \isacommand{have}\isamarkupfalse%
  1476 \ {\isachardoublequoteopen}a\ {\isacharequal}\ d{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
  1477 %
  1478 \endisatagproof
  1479 {\isafoldproof}%
  1480 %
  1481 \isadelimproof
  1482 %
  1483 \endisadelimproof
  1484 %
  1485 \begin{isamarkuptext}%
  1486 \noindent The term ``\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}'' above is a special abbreviation
  1487   provided by the Isabelle/Isar syntax layer: it statically refers to
  1488   the right-hand side argument of the previous statement given in the
  1489   text.  Thus it happens to coincide with relevant sub-expressions in
  1490   the calculational chain, but the exact correspondence is dependent
  1491   on the transitivity rules being involved.
  1492 
  1493   \medskip Symmetry rules such as \isa{{\isachardoublequote}x\ {\isacharequal}\ y\ {\isasymLongrightarrow}\ y\ {\isacharequal}\ x{\isachardoublequote}} are like
  1494   transitivities with only one premise.  Isar maintains a separate
  1495   rule collection declared via the \hyperlink{attribute.sym}{\mbox{\isa{sym}}} attribute, to be
  1496   used in fact expressions ``\isa{{\isachardoublequote}a\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isachardoublequote}}'', or single-step
  1497   proofs ``\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isachardoublequote}x\ {\isacharequal}\ y{\isachardoublequote}}~\hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}}~\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}~\isa{{\isachardoublequote}y\ {\isacharequal}\ x{\isachardoublequote}}~\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}}''.%
  1498 \end{isamarkuptext}%
  1499 \isamarkuptrue%
  1500 %
  1501 \isadelimtheory
  1502 %
  1503 \endisadelimtheory
  1504 %
  1505 \isatagtheory
  1506 \isacommand{end}\isamarkupfalse%
  1507 %
  1508 \endisatagtheory
  1509 {\isafoldtheory}%
  1510 %
  1511 \isadelimtheory
  1512 %
  1513 \endisadelimtheory
  1514 \end{isabellebody}%
  1515 %%% Local Variables:
  1516 %%% mode: latex
  1517 %%% TeX-master: "root"
  1518 %%% End: