src/Doc/Isar_Ref/Framework.thy
author wenzelm
Mon Oct 09 21:12:22 2017 +0200 (23 months ago)
changeset 66822 4642cf4a7ebb
parent 64510 488cb71eeb83
child 67399 eab6ce8368fa
permissions -rw-r--r--
tuned signature;
     1 (*:maxLineLen=78:*)
     2 
     3 theory Framework
     4   imports Main Base
     5 begin
     6 
     7 chapter \<open>The Isabelle/Isar Framework \label{ch:isar-framework}\<close>
     8 
     9 text \<open>
    10   Isabelle/Isar @{cite "Wenzel:1999:TPHOL" and "Wenzel-PhD" and
    11   "Nipkow-TYPES02" and "Wiedijk:1999:Mizar" and "Wenzel-Paulson:2006" and
    12   "Wenzel:2006:Festschrift"} is a generic framework for developing formal
    13   mathematical documents with full proof checking. Definitions, statements and
    14   proofs are organized as theories. A collection of theories sources may be
    15   presented as a printed document; see also \chref{ch:document-prep}.
    16 
    17   The main concern of Isar is the design of a human-readable structured proof
    18   language, which is called the ``primary proof format'' in Isar terminology.
    19   Such a primary proof language is somewhere in the middle between the
    20   extremes of primitive proof objects and actual natural language.
    21 
    22   Thus Isar challenges the traditional way of recording informal proofs in
    23   mathematical prose, as well as the common tendency to see fully formal
    24   proofs directly as objects of some logical calculus (e.g.\ \<open>\<lambda>\<close>-terms in a
    25   version of type theory). Technically, Isar is an interpreter of a simple
    26   block-structured language for describing the data flow of local facts and
    27   goals, interspersed with occasional invocations of proof methods. Everything
    28   is reduced to logical inferences internally, but these steps are somewhat
    29   marginal compared to the overall bookkeeping of the interpretation process.
    30   Thanks to careful design of the syntax and semantics of Isar language
    31   elements, a formal record of Isar commands may later appear as an
    32   intelligible text to the human reader.
    33 
    34   The Isar proof language has emerged from careful analysis of some inherent
    35   virtues of the logical framework Isabelle/Pure @{cite "paulson-found" and
    36   "paulson700"}, notably composition of higher-order natural deduction rules,
    37   which is a generalization of Gentzen's original calculus @{cite
    38   "Gentzen:1935"}. The approach of generic inference systems in Pure is
    39   continued by Isar towards actual proof texts. See also
    40   \figref{fig:natural-deduction}
    41 
    42   \begin{figure}[htb]
    43 
    44   \begin{center}
    45   \begin{minipage}[t]{0.9\textwidth}
    46 
    47   \textbf{Inferences:}
    48   \begin{center}
    49   \begin{tabular}{l@ {\qquad}l}
    50   \infer{\<open>B\<close>}{\<open>A \<longrightarrow> B\<close> & \<open>A\<close>} &
    51   \infer{\<open>A \<longrightarrow> B\<close>}{\infer*{\<open>B\<close>}{\<open>[A]\<close>}} \\
    52   \end{tabular}
    53   \end{center}
    54 
    55   \textbf{Isabelle/Pure:}
    56   \begin{center}
    57   \begin{tabular}{l@ {\qquad}l}
    58   \<open>(A \<longrightarrow> B) \<Longrightarrow> A \<Longrightarrow> B\<close> &
    59   \<open>(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B\<close>
    60   \end{tabular}
    61   \end{center}
    62 
    63   \textbf{Isabelle/Isar:}
    64   \begin{center}
    65   \begin{minipage}[t]{0.4\textwidth}
    66   @{theory_text [display, indent = 2]
    67     \<open>have "A \<longrightarrow> B" \<proof>
    68 also have A \<proof>
    69 finally have B .\<close>}
    70   \end{minipage}
    71   \begin{minipage}[t]{0.4\textwidth}
    72   @{theory_text [display, indent = 2]
    73     \<open>have "A \<longrightarrow> B"
    74 proof
    75   assume A
    76   then show B \<proof>
    77 qed\<close>}
    78   \end{minipage}
    79   \end{center}
    80 
    81   \end{minipage}
    82   \end{center}
    83 
    84   \caption{Natural Deduction via inferences according to Gentzen, rules in
    85   Isabelle/Pure, and proofs in Isabelle/Isar}\label{fig:natural-deduction}
    86 
    87   \end{figure}
    88 
    89   \<^medskip>
    90   Concrete applications require another intermediate layer: an object-logic.
    91   Isabelle/HOL @{cite "isa-tutorial"} (simply-typed set-theory) is most
    92   commonly used; elementary examples are given in the directory
    93   \<^dir>\<open>~~/src/HOL/Isar_Examples\<close>. Some examples demonstrate how to start a fresh
    94   object-logic from Isabelle/Pure, and use Isar proofs from the very start,
    95   despite the lack of advanced proof tools at such an early stage (e.g.\ see
    96   \<^file>\<open>~~/src/HOL/Isar_Examples/Higher_Order_Logic.thy\<close>). Isabelle/FOL @{cite
    97   "isabelle-logics"} and Isabelle/ZF @{cite "isabelle-ZF"} also work, but are
    98   much less developed.
    99 
   100   In order to illustrate natural deduction in Isar, we shall subsequently
   101   refer to the background theory and library of Isabelle/HOL. This includes
   102   common notions of predicate logic, naive set-theory etc.\ using fairly
   103   standard mathematical notation. From the perspective of generic natural
   104   deduction there is nothing special about the logical connectives of HOL
   105   (\<open>\<and>\<close>, \<open>\<or>\<close>, \<open>\<forall>\<close>, \<open>\<exists>\<close>, etc.), only the resulting reasoning principles are
   106   relevant to the user. There are similar rules available for set-theory
   107   operators (\<open>\<inter>\<close>, \<open>\<union>\<close>, \<open>\<Inter>\<close>, \<open>\<Union>\<close>, etc.), or any other theory developed in the
   108   library (lattice theory, topology etc.).
   109 
   110   Subsequently we briefly review fragments of Isar proof texts corresponding
   111   directly to such general deduction schemes. The examples shall refer to
   112   set-theory, to minimize the danger of understanding connectives of predicate
   113   logic as something special.
   114 
   115   \<^medskip>
   116   The following deduction performs \<open>\<inter>\<close>-introduction, working forwards from
   117   assumptions towards the conclusion. We give both the Isar text, and depict
   118   the primitive rule involved, as determined by unification of fact and goal
   119   statements against rules that are declared in the library context.
   120 \<close>
   121 
   122 text_raw \<open>\medskip\begin{minipage}{0.6\textwidth}\<close>
   123 
   124 (*<*)
   125 notepad
   126 begin
   127     fix x :: 'a and A B
   128 (*>*)
   129     assume "x \<in> A" and "x \<in> B"
   130     then have "x \<in> A \<inter> B" ..
   131 (*<*)
   132 end
   133 (*>*)
   134 
   135 text_raw \<open>\end{minipage}\begin{minipage}{0.4\textwidth}\<close>
   136 
   137 text \<open>
   138   \infer{\<open>x \<in> A \<inter> B\<close>}{\<open>x \<in> A\<close> & \<open>x \<in> B\<close>}
   139 \<close>
   140 
   141 text_raw \<open>\end{minipage}\<close>
   142 
   143 text \<open>
   144   \<^medskip>
   145   Note that \<^theory_text>\<open>assume\<close> augments the proof context, \<^theory_text>\<open>then\<close> indicates that the
   146   current fact shall be used in the next step, and \<^theory_text>\<open>have\<close> states an
   147   intermediate goal. The two dots ``\<^theory_text>\<open>..\<close>'' refer to a complete proof of this
   148   claim, using the indicated facts and a canonical rule from the context. We
   149   could have been more explicit here by spelling out the final proof step via
   150   the \<^theory_text>\<open>by\<close> command:
   151 \<close>
   152 
   153 (*<*)
   154 notepad
   155 begin
   156     fix x :: 'a and A B
   157 (*>*)
   158     assume "x \<in> A" and "x \<in> B"
   159     then have "x \<in> A \<inter> B" by (rule IntI)
   160 (*<*)
   161 end
   162 (*>*)
   163 
   164 text \<open>
   165   The format of the \<open>\<inter>\<close>-introduction rule represents the most basic inference,
   166   which proceeds from given premises to a conclusion, without any nested proof
   167   context involved.
   168 
   169   The next example performs backwards introduction of \<open>\<Inter>\<A>\<close>, the intersection
   170   of all sets within a given set. This requires a nested proof of set
   171   membership within a local context, where \<open>A\<close> is an arbitrary-but-fixed
   172   member of the collection:
   173 \<close>
   174 
   175 text_raw \<open>\medskip\begin{minipage}{0.6\textwidth}\<close>
   176 
   177 (*<*)
   178 notepad
   179 begin
   180     fix x :: 'a and \<A>
   181 (*>*)
   182     have "x \<in> \<Inter>\<A>"
   183     proof
   184       fix A
   185       assume "A \<in> \<A>"
   186       show "x \<in> A" \<proof>
   187     qed
   188 (*<*)
   189 end
   190 (*>*)
   191 
   192 text_raw \<open>\end{minipage}\begin{minipage}{0.4\textwidth}\<close>
   193 
   194 text \<open>
   195   \infer{\<open>x \<in> \<Inter>\<A>\<close>}{\infer*{\<open>x \<in> A\<close>}{\<open>[A][A \<in> \<A>]\<close>}}
   196 \<close>
   197 
   198 text_raw \<open>\end{minipage}\<close>
   199 
   200 text \<open>
   201   \<^medskip>
   202   This Isar reasoning pattern again refers to the primitive rule depicted
   203   above. The system determines it in the ``\<^theory_text>\<open>proof\<close>'' step, which could have
   204   been spelled out more explicitly as ``\<^theory_text>\<open>proof (rule InterI)\<close>''. Note that
   205   the rule involves both a local parameter \<open>A\<close> and an assumption \<open>A \<in> \<A>\<close> in
   206   the nested reasoning. Such compound rules typically demands a genuine
   207   subproof in Isar, working backwards rather than forwards as seen before. In
   208   the proof body we encounter the \<^theory_text>\<open>fix\<close>-\<^theory_text>\<open>assume\<close>-\<^theory_text>\<open>show\<close> outline of nested
   209   subproofs that is typical for Isar. The final \<^theory_text>\<open>show\<close> is like \<^theory_text>\<open>have\<close>
   210   followed by an additional refinement of the enclosing claim, using the rule
   211   derived from the proof body.
   212 
   213   \<^medskip>
   214   The next example involves \<open>\<Union>\<A>\<close>, which can be characterized as the set of
   215   all \<open>x\<close> such that \<open>\<exists>A. x \<in> A \<and> A \<in> \<A>\<close>. The elimination rule for \<open>x \<in> \<Union>\<A>\<close>
   216   does not mention \<open>\<exists>\<close> and \<open>\<and>\<close> at all, but admits to obtain directly a local
   217   \<open>A\<close> such that \<open>x \<in> A\<close> and \<open>A \<in> \<A>\<close> hold. This corresponds to the following
   218   Isar proof and inference rule, respectively:
   219 \<close>
   220 
   221 text_raw \<open>\medskip\begin{minipage}{0.6\textwidth}\<close>
   222 
   223 (*<*)
   224 notepad
   225 begin
   226     fix x :: 'a and \<A> C
   227 (*>*)
   228     assume "x \<in> \<Union>\<A>"
   229     then have C
   230     proof
   231       fix A
   232       assume "x \<in> A" and "A \<in> \<A>"
   233       show C \<proof>
   234     qed
   235 (*<*)
   236 end
   237 (*>*)
   238 
   239 text_raw \<open>\end{minipage}\begin{minipage}{0.4\textwidth}\<close>
   240 
   241 text \<open>
   242   \infer{\<open>C\<close>}{\<open>x \<in> \<Union>\<A>\<close> & \infer*{\<open>C\<close>~}{\<open>[A][x \<in> A, A \<in> \<A>]\<close>}}
   243 \<close>
   244 
   245 text_raw \<open>\end{minipage}\<close>
   246 
   247 text \<open>
   248   \<^medskip>
   249   Although the Isar proof follows the natural deduction rule closely, the text
   250   reads not as natural as anticipated. There is a double occurrence of an
   251   arbitrary conclusion \<open>C\<close>, which represents the final result, but is
   252   irrelevant for now. This issue arises for any elimination rule involving
   253   local parameters. Isar provides the derived language element \<^theory_text>\<open>obtain\<close>,
   254   which is able to perform the same elimination proof more conveniently:
   255 \<close>
   256 
   257 (*<*)
   258 notepad
   259 begin
   260     fix x :: 'a and \<A>
   261 (*>*)
   262     assume "x \<in> \<Union>\<A>"
   263     then obtain A where "x \<in> A" and "A \<in> \<A>" ..
   264 (*<*)
   265 end
   266 (*>*)
   267 
   268 text \<open>
   269   Here we avoid to mention the final conclusion \<open>C\<close> and return to plain
   270   forward reasoning. The rule involved in the ``\<^theory_text>\<open>..\<close>'' proof is the same as
   271   before.
   272 \<close>
   273 
   274 
   275 section \<open>The Pure framework \label{sec:framework-pure}\<close>
   276 
   277 text \<open>
   278   The Pure logic @{cite "paulson-found" and "paulson700"} is an intuitionistic
   279   fragment of higher-order logic @{cite "church40"}. In type-theoretic
   280   parlance, there are three levels of \<open>\<lambda>\<close>-calculus with corresponding arrows
   281   \<open>\<Rightarrow>\<close>/\<open>\<And>\<close>/\<open>\<Longrightarrow>\<close>:
   282 
   283   \<^medskip>
   284   \begin{tabular}{ll}
   285   \<open>\<alpha> \<Rightarrow> \<beta>\<close> & syntactic function space (terms depending on terms) \\
   286   \<open>\<And>x. B(x)\<close> & universal quantification (proofs depending on terms) \\
   287   \<open>A \<Longrightarrow> B\<close> & implication (proofs depending on proofs) \\
   288   \end{tabular}
   289   \<^medskip>
   290 
   291   Here only the types of syntactic terms, and the propositions of proof terms
   292   have been shown. The \<open>\<lambda>\<close>-structure of proofs can be recorded as an optional
   293   feature of the Pure inference kernel @{cite "Berghofer-Nipkow:2000:TPHOL"},
   294   but the formal system can never depend on them due to \<^emph>\<open>proof irrelevance\<close>.
   295 
   296   On top of this most primitive layer of proofs, Pure implements a generic
   297   calculus for nested natural deduction rules, similar to @{cite
   298   "Schroeder-Heister:1984"}. Here object-logic inferences are internalized as
   299   formulae over \<open>\<And>\<close> and \<open>\<Longrightarrow>\<close>. Combining such rule statements may involve
   300   higher-order unification @{cite "paulson-natural"}.
   301 \<close>
   302 
   303 
   304 subsection \<open>Primitive inferences\<close>
   305 
   306 text \<open>
   307   Term syntax provides explicit notation for abstraction \<open>\<lambda>x :: \<alpha>. b(x)\<close> and
   308   application \<open>b a\<close>, while types are usually implicit thanks to
   309   type-inference; terms of type \<open>prop\<close> are called propositions. Logical
   310   statements are composed via \<open>\<And>x :: \<alpha>. B(x)\<close> and \<open>A \<Longrightarrow> B\<close>. Primitive reasoning
   311   operates on judgments of the form \<open>\<Gamma> \<turnstile> \<phi>\<close>, with standard introduction and
   312   elimination rules for \<open>\<And>\<close> and \<open>\<Longrightarrow>\<close> that refer to fixed parameters \<open>x\<^sub>1, \<dots>,
   313   x\<^sub>m\<close> and hypotheses \<open>A\<^sub>1, \<dots>, A\<^sub>n\<close> from the context \<open>\<Gamma>\<close>; the corresponding
   314   proof terms are left implicit. The subsequent inference rules define \<open>\<Gamma> \<turnstile> \<phi>\<close>
   315   inductively, relative to a collection of axioms from the implicit background
   316   theory:
   317 
   318   \[
   319   \infer{\<open>\<turnstile> A\<close>}{\<open>A\<close> \mbox{~is axiom}}
   320   \qquad
   321   \infer{\<open>A \<turnstile> A\<close>}{}
   322   \]
   323 
   324   \[
   325   \infer{\<open>\<Gamma> \<turnstile> \<And>x. B(x)\<close>}{\<open>\<Gamma> \<turnstile> B(x)\<close> & \<open>x \<notin> \<Gamma>\<close>}
   326   \qquad
   327   \infer{\<open>\<Gamma> \<turnstile> B(a)\<close>}{\<open>\<Gamma> \<turnstile> \<And>x. B(x)\<close>}
   328   \]
   329 
   330   \[
   331   \infer{\<open>\<Gamma> - A \<turnstile> A \<Longrightarrow> B\<close>}{\<open>\<Gamma> \<turnstile> B\<close>}
   332   \qquad
   333   \infer{\<open>\<Gamma>\<^sub>1 \<union> \<Gamma>\<^sub>2 \<turnstile> B\<close>}{\<open>\<Gamma>\<^sub>1 \<turnstile> A \<Longrightarrow> B\<close> & \<open>\<Gamma>\<^sub>2 \<turnstile> A\<close>}
   334   \]
   335 
   336   Furthermore, Pure provides a built-in equality \<open>\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop\<close> with
   337   axioms for reflexivity, substitution, extensionality, and \<open>\<alpha>\<beta>\<eta>\<close>-conversion
   338   on \<open>\<lambda>\<close>-terms.
   339 
   340   \<^medskip>
   341 
   342   An object-logic introduces another layer on top of Pure, e.g.\ with types
   343   \<open>i\<close> for individuals and \<open>o\<close> for propositions, term constants \<open>Trueprop :: o
   344   \<Rightarrow> prop\<close> as (implicit) derivability judgment and connectives like \<open>\<and> :: o \<Rightarrow> o
   345   \<Rightarrow> o\<close> or \<open>\<forall> :: (i \<Rightarrow> o) \<Rightarrow> o\<close>, and axioms for object-level rules such as
   346   \<open>conjI: A \<Longrightarrow> B \<Longrightarrow> A \<and> B\<close> or \<open>allI: (\<And>x. B x) \<Longrightarrow> \<forall>x. B x\<close>. Derived object rules
   347   are represented as theorems of Pure. After the initial object-logic setup,
   348   further axiomatizations are usually avoided: definitional principles are
   349   used instead (e.g.\ \<^theory_text>\<open>definition\<close>, \<^theory_text>\<open>inductive\<close>, \<^theory_text>\<open>fun\<close>, \<^theory_text>\<open>function\<close>).
   350 \<close>
   351 
   352 
   353 subsection \<open>Reasoning with rules \label{sec:framework-resolution}\<close>
   354 
   355 text \<open>
   356   Primitive inferences mostly serve foundational purposes. The main reasoning
   357   mechanisms of Pure operate on nested natural deduction rules expressed as
   358   formulae, using \<open>\<And>\<close> to bind local parameters and \<open>\<Longrightarrow>\<close> to express entailment.
   359   Multiple parameters and premises are represented by repeating these
   360   connectives in a right-associative manner.
   361 
   362   Thanks to the Pure theorem @{prop "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"} the
   363   connectives \<open>\<And>\<close> and \<open>\<Longrightarrow>\<close> commute. So we may assume w.l.o.g.\ that rule
   364   statements always observe the normal form where quantifiers are pulled in
   365   front of implications at each level of nesting. This means that any Pure
   366   proposition may be presented as a \<^emph>\<open>Hereditary Harrop Formula\<close> @{cite
   367   "Miller:1991"} which is of the form \<open>\<And>x\<^sub>1 \<dots> x\<^sub>m. H\<^sub>1 \<Longrightarrow> \<dots> H\<^sub>n \<Longrightarrow> A\<close> for \<open>m, n
   368   \<ge> 0\<close>, and \<open>A\<close> atomic, and \<open>H\<^sub>1, \<dots>, H\<^sub>n\<close> being recursively of the same
   369   format. Following the convention that outermost quantifiers are implicit,
   370   Horn clauses \<open>A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> A\<close> are a special case of this.
   371 
   372   For example, the \<open>\<inter>\<close>-introduction rule encountered before is represented as
   373   a Pure theorem as follows:
   374   \[
   375   \<open>IntI:\<close>~@{prop "x \<in> A \<Longrightarrow> x \<in> B \<Longrightarrow> x \<in> A \<inter> B"}
   376   \]
   377 
   378   This is a plain Horn clause, since no further nesting on the left is
   379   involved. The general \<open>\<Inter>\<close>-introduction corresponds to a Hereditary Harrop
   380   Formula with one additional level of nesting:
   381   \[
   382   \<open>InterI:\<close>~@{prop "(\<And>A. A \<in> \<A> \<Longrightarrow> x \<in> A) \<Longrightarrow> x \<in> \<Inter>\<A>"}
   383   \]
   384 
   385   \<^medskip>
   386   Goals are also represented as rules: \<open>A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C\<close> states that the
   387   subgoals \<open>A\<^sub>1, \<dots>, A\<^sub>n\<close> entail the result \<open>C\<close>; for \<open>n = 0\<close> the goal is
   388   finished. To allow \<open>C\<close> being a rule statement itself, there is an internal
   389   protective marker \<open># :: prop \<Rightarrow> prop\<close>, which is defined as identity and
   390   hidden from the user. We initialize and finish goal states as follows:
   391 
   392   \[
   393   \begin{array}{c@ {\qquad}c}
   394   \infer[(@{inference_def init})]{\<open>C \<Longrightarrow> #C\<close>}{} &
   395   \infer[(@{inference_def finish})]{\<open>C\<close>}{\<open>#C\<close>}
   396   \end{array}
   397   \]
   398 
   399   Goal states are refined in intermediate proof steps until a finished form is
   400   achieved. Here the two main reasoning principles are @{inference
   401   resolution}, for back-chaining a rule against a subgoal (replacing it by
   402   zero or more subgoals), and @{inference assumption}, for solving a subgoal
   403   (finding a short-circuit with local assumptions). Below \<open>\<^vec>x\<close> stands
   404   for \<open>x\<^sub>1, \<dots>, x\<^sub>n\<close> (for \<open>n \<ge> 0\<close>).
   405 
   406   \[
   407   \infer[(@{inference_def resolution})]
   408   {\<open>(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> \<^vec>A (\<^vec>a \<^vec>x))\<vartheta> \<Longrightarrow> C\<vartheta>\<close>}
   409   {\begin{tabular}{rl}
   410     \<open>rule:\<close> &
   411     \<open>\<^vec>A \<^vec>a \<Longrightarrow> B \<^vec>a\<close> \\
   412     \<open>goal:\<close> &
   413     \<open>(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> B' \<^vec>x) \<Longrightarrow> C\<close> \\
   414     \<open>goal unifier:\<close> &
   415     \<open>(\<lambda>\<^vec>x. B (\<^vec>a \<^vec>x))\<vartheta> = B'\<vartheta>\<close> \\
   416    \end{tabular}}
   417   \]
   418 
   419   \<^medskip>
   420 
   421   \[
   422   \infer[(@{inference_def assumption})]{\<open>C\<vartheta>\<close>}
   423   {\begin{tabular}{rl}
   424     \<open>goal:\<close> &
   425     \<open>(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> A \<^vec>x) \<Longrightarrow> C\<close> \\
   426     \<open>assm unifier:\<close> & \<open>A\<vartheta> = H\<^sub>i\<vartheta>\<close>~~\mbox{for some~\<open>H\<^sub>i\<close>} \\
   427    \end{tabular}}
   428   \]
   429 
   430   The following trace illustrates goal-oriented reasoning in
   431   Isabelle/Pure:
   432 
   433   {\footnotesize
   434   \<^medskip>
   435   \begin{tabular}{r@ {\quad}l}
   436   \<open>(A \<and> B \<Longrightarrow> B \<and> A) \<Longrightarrow> #(A \<and> B \<Longrightarrow> B \<and> A)\<close> & \<open>(init)\<close> \\
   437   \<open>(A \<and> B \<Longrightarrow> B) \<Longrightarrow> (A \<and> B \<Longrightarrow> A) \<Longrightarrow> #\<dots>\<close> & \<open>(resolution B \<Longrightarrow> A \<Longrightarrow> B \<and> A)\<close> \\
   438   \<open>(A \<and> B \<Longrightarrow> A \<and> B) \<Longrightarrow> (A \<and> B \<Longrightarrow> A) \<Longrightarrow> #\<dots>\<close> & \<open>(resolution A \<and> B \<Longrightarrow> B)\<close> \\
   439   \<open>(A \<and> B \<Longrightarrow> A) \<Longrightarrow> #\<dots>\<close> & \<open>(assumption)\<close> \\
   440   \<open>(A \<and> B \<Longrightarrow> A \<and> B) \<Longrightarrow> #\<dots>\<close> & \<open>(resolution A \<and> B \<Longrightarrow> A)\<close> \\
   441   \<open>#\<dots>\<close> & \<open>(assumption)\<close> \\
   442   \<open>A \<and> B \<Longrightarrow> B \<and> A\<close> & \<open>(finish)\<close> \\
   443   \end{tabular}
   444   \<^medskip>
   445   }
   446 
   447   Compositions of @{inference assumption} after @{inference resolution} occurs
   448   quite often, typically in elimination steps. Traditional Isabelle tactics
   449   accommodate this by a combined @{inference_def elim_resolution} principle.
   450   In contrast, Isar uses a combined refinement rule as follows:\footnote{For
   451   simplicity and clarity, the presentation ignores \<^emph>\<open>weak premises\<close> as
   452   introduced via \<^theory_text>\<open>presume\<close> or \<^theory_text>\<open>show \<dots> when\<close>.}
   453 
   454   {\small
   455   \[
   456   \infer[(@{inference refinement})]
   457   {\<open>C\<vartheta>\<close>}
   458   {\begin{tabular}{rl}
   459     \<open>subgoal:\<close> &
   460     \<open>(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> B' \<^vec>x) \<Longrightarrow> C\<close> \\
   461     \<open>subproof:\<close> &
   462     \<open>\<^vec>G \<^vec>a \<Longrightarrow> B \<^vec>a\<close> \quad for schematic \<open>\<^vec>a\<close> \\
   463     \<open>concl unifier:\<close> &
   464     \<open>(\<lambda>\<^vec>x. B (\<^vec>a \<^vec>x))\<vartheta> = B'\<vartheta>\<close> \\
   465     \<open>assm unifiers:\<close> &
   466     \<open>(\<lambda>\<^vec>x. G\<^sub>j (\<^vec>a \<^vec>x))\<vartheta> = H\<^sub>i\<vartheta>\<close> \quad for each \<open>G\<^sub>j\<close> some \<open>H\<^sub>i\<close> \\
   467    \end{tabular}}
   468   \]}
   469 
   470   Here the \<open>subproof\<close> rule stems from the main \<^theory_text>\<open>fix\<close>-\<^theory_text>\<open>assume\<close>-\<^theory_text>\<open>show\<close>
   471   outline of Isar (cf.\ \secref{sec:framework-subproof}): each assumption
   472   indicated in the text results in a marked premise \<open>G\<close> above. Consequently,
   473   \<^theory_text>\<open>fix\<close>-\<^theory_text>\<open>assume\<close>-\<^theory_text>\<open>show\<close> enables to fit the result of a subproof quite
   474   robustly into a pending subgoal, while maintaining a good measure of
   475   flexibility: the subproof only needs to fit modulo unification, and its
   476   assumptions may be a proper subset of the subgoal premises (see
   477   \secref{sec:framework-subproof}).
   478 \<close>
   479 
   480 
   481 section \<open>The Isar proof language \label{sec:framework-isar}\<close>
   482 
   483 text \<open>
   484   Structured proofs are presented as high-level expressions for composing
   485   entities of Pure (propositions, facts, and goals). The Isar proof language
   486   allows to organize reasoning within the underlying rule calculus of Pure,
   487   but Isar is not another logical calculus. Isar merely imposes certain
   488   structure and policies on Pure inferences. The main grammar of the Isar
   489   proof language is given in \figref{fig:isar-syntax}.
   490 
   491   \begin{figure}[htb]
   492   \begin{center}
   493   \begin{tabular}{rcl}
   494     \<open>main\<close> & \<open>=\<close> & \<^theory_text>\<open>notepad begin "statement\<^sup>*" end\<close> \\
   495     & \<open>|\<close> & \<^theory_text>\<open>theorem name: props if name: props for vars\<close> \\
   496     & \<open>|\<close> & \<^theory_text>\<open>theorem name:\<close> \\
   497     & & \quad\<^theory_text>\<open>fixes vars\<close> \\
   498     & & \quad\<^theory_text>\<open>assumes name: props\<close> \\
   499     & & \quad\<^theory_text>\<open>shows name: props "proof"\<close> \\
   500     & \<open>|\<close> & \<^theory_text>\<open>theorem name:\<close> \\
   501     & & \quad\<^theory_text>\<open>fixes vars\<close> \\
   502     & & \quad\<^theory_text>\<open>assumes name: props\<close> \\
   503     & & \quad\<^theory_text>\<open>obtains (name) clause "\<^bold>|" \<dots> "proof"\<close> \\
   504     \<open>proof\<close> & \<open>=\<close> & \<^theory_text>\<open>"refinement\<^sup>* proper_proof"\<close> \\
   505     \<open>refinement\<close> & \<open>=\<close> &  \<^theory_text>\<open>apply method\<close> \\
   506     & \<open>|\<close> & \<^theory_text>\<open>supply name = thms\<close> \\
   507     & \<open>|\<close> & \<^theory_text>\<open>subgoal premises name for vars "proof"\<close> \\
   508     & \<open>|\<close> & \<^theory_text>\<open>using thms\<close> \\
   509     & \<open>|\<close> & \<^theory_text>\<open>unfolding thms\<close> \\
   510     \<open>proper_proof\<close> & \<open>=\<close> & \<^theory_text>\<open>proof "method\<^sup>?" "statement\<^sup>*" qed "method\<^sup>?"\<close> \\
   511     & \<open>|\<close> & \<^theory_text>\<open>by method method\<close>~~~\<open>|\<close>~~~\<^theory_text>\<open>..\<close>~~~\<open>|\<close>~~~\<^theory_text>\<open>.\<close>~~~\<open>|\<close>~~~\<^theory_text>\<open>sorry\<close>~~~\<open>|\<close>~~~\<^theory_text>\<open>done\<close> \\
   512     \<open>statement\<close> & \<open>=\<close> & \<^theory_text>\<open>{ "statement\<^sup>*" }\<close>~~~\<open>|\<close>~~~\<^theory_text>\<open>next\<close> \\
   513     & \<open>|\<close> & \<^theory_text>\<open>note name = thms\<close> \\
   514     & \<open>|\<close> & \<^theory_text>\<open>let "term" = "term"\<close> \\
   515     & \<open>|\<close> & \<^theory_text>\<open>write name  (mixfix)\<close> \\
   516     & \<open>|\<close> & \<^theory_text>\<open>fix vars\<close> \\
   517     & \<open>|\<close> & \<^theory_text>\<open>assume name: props if props for vars\<close> \\
   518     & \<open>|\<close> & \<^theory_text>\<open>presume name: props if props for vars\<close> \\
   519     & \<open>|\<close> & \<^theory_text>\<open>define clause\<close> \\
   520     & \<open>|\<close> & \<^theory_text>\<open>case name: "case"\<close> \\
   521     & \<open>|\<close> & \<^theory_text>\<open>then"\<^sup>?" goal\<close> \\
   522     & \<open>|\<close> & \<^theory_text>\<open>from thms goal\<close> \\
   523     & \<open>|\<close> & \<^theory_text>\<open>with thms goal\<close> \\
   524     & \<open>|\<close> & \<^theory_text>\<open>also\<close>~~~\<open>|\<close>~~~\<^theory_text>\<open>finally goal\<close> \\
   525     & \<open>|\<close> & \<^theory_text>\<open>moreover\<close>~~~\<open>|\<close>~~~\<^theory_text>\<open>ultimately goal\<close> \\
   526     \<open>goal\<close> & \<open>=\<close> & \<^theory_text>\<open>have name: props if name: props for vars "proof"\<close> \\
   527     & \<open>|\<close> & \<^theory_text>\<open>show name: props if name: props for vars "proof"\<close> \\
   528     & \<open>|\<close> & \<^theory_text>\<open>show name: props when name: props for vars "proof"\<close> \\
   529     & \<open>|\<close> & \<^theory_text>\<open>consider (name) clause "\<^bold>|" \<dots> "proof"\<close> \\
   530     & \<open>|\<close> & \<^theory_text>\<open>obtain (name) clause "proof"\<close> \\
   531     \<open>clause\<close> & \<open>=\<close> & \<^theory_text>\<open>vars where name: props if props for vars\<close> \\
   532   \end{tabular}
   533   \end{center}
   534   \caption{Main grammar of the Isar proof language}\label{fig:isar-syntax}
   535   \end{figure}
   536 
   537   The construction of the Isar proof language proceeds in a bottom-up fashion,
   538   as an exercise in purity and minimalism. The grammar in
   539   \appref{ap:main-grammar} describes the primitive parts of the core language
   540   (category \<open>proof\<close>), which is embedded into the main outer theory syntax via
   541   elements that require a proof (e.g.\ \<^theory_text>\<open>theorem\<close>, \<^theory_text>\<open>lemma\<close>, \<^theory_text>\<open>function\<close>,
   542   \<^theory_text>\<open>termination\<close>).
   543 
   544   The syntax for terms and propositions is inherited from Pure (and the
   545   object-logic). A \<open>pattern\<close> is a \<open>term\<close> with schematic variables, to be bound
   546   by higher-order matching. Simultaneous propositions or facts may be
   547   separated by the \<^theory_text>\<open>and\<close> keyword.
   548 
   549   \<^medskip>
   550   Facts may be referenced by name or proposition. For example, the result of
   551   ``\<^theory_text>\<open>have a: A \<proof>\<close>'' becomes accessible both via the name \<open>a\<close> and the
   552   literal proposition \<open>\<open>A\<close>\<close>. Moreover, fact expressions may involve attributes
   553   that modify either the theorem or the background context. For example, the
   554   expression ``\<open>a [OF b]\<close>'' refers to the composition of two facts according
   555   to the @{inference resolution} inference of
   556   \secref{sec:framework-resolution}, while ``\<open>a [intro]\<close>'' declares a fact as
   557   introduction rule in the context.
   558 
   559   The special fact called ``@{fact this}'' always refers to the last result,
   560   as produced by \<^theory_text>\<open>note\<close>, \<^theory_text>\<open>assume\<close>, \<^theory_text>\<open>have\<close>, or \<^theory_text>\<open>show\<close>. Since \<^theory_text>\<open>note\<close> occurs
   561   frequently together with \<^theory_text>\<open>then\<close>, there are some abbreviations:
   562 
   563   \<^medskip>
   564   \begin{tabular}{rcl}
   565     \<^theory_text>\<open>from a\<close> & \<open>\<equiv>\<close> & \<^theory_text>\<open>note a then\<close> \\
   566     \<^theory_text>\<open>with a\<close> & \<open>\<equiv>\<close> & \<^theory_text>\<open>from a and this\<close> \\
   567   \end{tabular}
   568   \<^medskip>
   569 
   570   The \<open>method\<close> category is essentially a parameter of the Isar language and
   571   may be populated later. The command \<^theory_text>\<open>method_setup\<close> allows to define proof
   572   methods semantically in Isabelle/ML. The Eisbach language allows to define
   573   proof methods symbolically, as recursive expressions over existing methods
   574   @{cite "Matichuk-et-al:2014"}; see also \<^dir>\<open>~~/src/HOL/Eisbach\<close>.
   575 
   576   Methods use the facts indicated by \<^theory_text>\<open>then\<close> or \<^theory_text>\<open>using\<close>, and then operate on
   577   the goal state. Some basic methods are predefined in Pure: ``@{method "-"}''
   578   leaves the goal unchanged, ``@{method this}'' applies the facts as rules to
   579   the goal, ``@{method (Pure) "rule"}'' applies the facts to another rule and
   580   the result to the goal (both ``@{method this}'' and ``@{method (Pure)
   581   rule}'' refer to @{inference resolution} of
   582   \secref{sec:framework-resolution}). The secondary arguments to ``@{method
   583   (Pure) rule}'' may be specified explicitly as in ``\<open>(rule a)\<close>'', or picked
   584   from the context. In the latter case, the system first tries rules declared
   585   as @{attribute (Pure) elim} or @{attribute (Pure) dest}, followed by those
   586   declared as @{attribute (Pure) intro}.
   587 
   588   The default method for \<^theory_text>\<open>proof\<close> is ``@{method standard}'' (which subsumes
   589   @{method rule} with arguments picked from the context), for \<^theory_text>\<open>qed\<close> it is
   590   ``@{method "succeed"}''. Further abbreviations for terminal proof steps are
   591   ``\<^theory_text>\<open>by method\<^sub>1 method\<^sub>2\<close>'' for ``\<^theory_text>\<open>proof method\<^sub>1 qed method\<^sub>2\<close>'', and
   592   ``\<^theory_text>\<open>..\<close>'' for ``\<^theory_text>\<open>by standard\<close>, and ``\<^theory_text>\<open>.\<close>'' for ``\<^theory_text>\<open>by this\<close>''. The command
   593   ``\<^theory_text>\<open>unfolding facts\<close>'' operates directly on the goal by applying equalities.
   594 
   595   \<^medskip>
   596   Block structure can be indicated explicitly by ``\<^theory_text>\<open>{ \<dots> }\<close>'', although the
   597   body of a subproof ``\<^theory_text>\<open>proof \<dots> qed\<close>'' already provides implicit nesting. In
   598   both situations, \<^theory_text>\<open>next\<close> jumps into the next section of a block, i.e.\ it
   599   acts like closing an implicit block scope and opening another one. There is
   600   no direct connection to subgoals here!
   601 
   602   The commands \<^theory_text>\<open>fix\<close> and \<^theory_text>\<open>assume\<close> build up a local context (see
   603   \secref{sec:framework-context}), while \<^theory_text>\<open>show\<close> refines a pending subgoal by
   604   the rule resulting from a nested subproof (see
   605   \secref{sec:framework-subproof}). Further derived concepts will support
   606   calculational reasoning (see \secref{sec:framework-calc}).
   607 \<close>
   608 
   609 
   610 subsection \<open>Context elements \label{sec:framework-context}\<close>
   611 
   612 text \<open>
   613   In judgments \<open>\<Gamma> \<turnstile> \<phi>\<close> of the primitive framework, \<open>\<Gamma>\<close> essentially acts like a
   614   proof context. Isar elaborates this idea towards a more advanced concept,
   615   with additional information for type-inference, term abbreviations, local
   616   facts, hypotheses etc.
   617 
   618   The element \<^theory_text>\<open>fix x :: \<alpha>\<close> declares a local parameter, i.e.\ an
   619   arbitrary-but-fixed entity of a given type; in results exported from the
   620   context, \<open>x\<close> may become anything. The \<^theory_text>\<open>assume \<guillemotleft>inference\<guillemotright>\<close> element provides
   621   a general interface to hypotheses: \<^theory_text>\<open>assume \<guillemotleft>inference\<guillemotright> A\<close> produces \<open>A \<turnstile> A\<close>
   622   locally, while the included inference tells how to discharge \<open>A\<close> from
   623   results \<open>A \<turnstile> B\<close> later on. There is no surface syntax for \<open>\<guillemotleft>inference\<guillemotright>\<close>,
   624   i.e.\ it may only occur internally when derived commands are defined in ML.
   625 
   626   The default inference for \<^theory_text>\<open>assume\<close> is @{inference export} as given below.
   627   The derived element \<^theory_text>\<open>define x where "x \<equiv> a"\<close> is defined as \<^theory_text>\<open>fix x assume
   628   \<guillemotleft>expand\<guillemotright> x \<equiv> a\<close>, with the subsequent inference @{inference expand}.
   629 
   630   \[
   631   \infer[(@{inference_def export})]{\<open>\<strut>\<Gamma> - A \<turnstile> A \<Longrightarrow> B\<close>}{\<open>\<strut>\<Gamma> \<turnstile> B\<close>}
   632   \qquad
   633   \infer[(@{inference_def expand})]{\<open>\<strut>\<Gamma> - (x \<equiv> a) \<turnstile> B a\<close>}{\<open>\<strut>\<Gamma> \<turnstile> B x\<close>}
   634   \]
   635 
   636   \<^medskip>
   637   The most interesting derived context element in Isar is \<^theory_text>\<open>obtain\<close> @{cite
   638   \<open>\S5.3\<close> "Wenzel-PhD"}, which supports generalized elimination steps in a
   639   purely forward manner. The \<^theory_text>\<open>obtain\<close> command takes a specification of
   640   parameters \<open>\<^vec>x\<close> and assumptions \<open>\<^vec>A\<close> to be added to the context,
   641   together with a proof of a case rule stating that this extension is
   642   conservative (i.e.\ may be removed from closed results later on):
   643 
   644   \<^medskip>
   645   \begin{tabular}{l}
   646   \<^theory_text>\<open>\<langle>facts\<rangle> obtain "\<^vec>x" where "\<^vec>A" "\<^vec>x" \<proof> \<equiv>\<close> \\[0.5ex]
   647   \quad \<^theory_text>\<open>have "case": "\<And>thesis. (\<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis) \<Longrightarrow> thesis"\<close> \\
   648   \quad \<^theory_text>\<open>proof -\<close> \\
   649   \qquad \<^theory_text>\<open>fix thesis\<close> \\
   650   \qquad \<^theory_text>\<open>assume [intro]: "\<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis"\<close> \\
   651   \qquad \<^theory_text>\<open>show thesis using \<langle>facts\<rangle> \<proof>\<close> \\
   652   \quad \<^theory_text>\<open>qed\<close> \\
   653   \quad \<^theory_text>\<open>fix "\<^vec>x" assume \<guillemotleft>elimination "case"\<guillemotright> "\<^vec>A \<^vec>x"\<close> \\
   654   \end{tabular}
   655   \<^medskip>
   656 
   657   \[
   658   \infer[(@{inference elimination})]{\<open>\<Gamma> \<turnstile> B\<close>}{
   659     \begin{tabular}{rl}
   660     \<open>case:\<close> &
   661     \<open>\<Gamma> \<turnstile> \<And>thesis. (\<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis) \<Longrightarrow> thesis\<close> \\[0.2ex]
   662     \<open>result:\<close> &
   663     \<open>\<Gamma> \<union> \<^vec>A \<^vec>y \<turnstile> B\<close> \\[0.2ex]
   664     \end{tabular}}
   665   \]
   666 
   667   Here the name ``\<open>thesis\<close>'' is a specific convention for an
   668   arbitrary-but-fixed proposition; in the primitive natural deduction rules
   669   shown before we have occasionally used \<open>C\<close>. The whole statement of
   670   ``\<^theory_text>\<open>obtain x where A x\<close>'' can be read as a claim that \<open>A x\<close> may be assumed
   671   for some arbitrary-but-fixed \<open>x\<close>. Also note that ``\<^theory_text>\<open>obtain A and B\<close>''
   672   without parameters is similar to ``\<^theory_text>\<open>have A and B\<close>'', but the latter
   673   involves multiple subgoals that need to be proven separately.
   674 
   675   \<^medskip>
   676   The subsequent Isar proof texts explain all context elements introduced
   677   above using the formal proof language itself. After finishing a local proof
   678   within a block, the exported result is indicated via \<^theory_text>\<open>note\<close>.
   679 \<close>
   680 
   681 (*<*)
   682 theorem True
   683 proof
   684 (*>*)
   685   text_raw \<open>\begin{minipage}[t]{0.45\textwidth}\<close>
   686   {
   687     fix x
   688     have "B x" \<proof>
   689   }
   690   note \<open>\<And>x. B x\<close>
   691   text_raw \<open>\end{minipage}\quad\begin{minipage}[t]{0.45\textwidth}\<close>(*<*)next(*>*)
   692   {
   693     assume A
   694     have B \<proof>
   695   }
   696   note \<open>A \<Longrightarrow> B\<close>
   697   text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.45\textwidth}\<close>(*<*)next(*>*)
   698   {
   699     define x where "x \<equiv> a"
   700     have "B x" \<proof>
   701   }
   702   note \<open>B a\<close>
   703   text_raw \<open>\end{minipage}\quad\begin{minipage}[t]{0.45\textwidth}\<close>(*<*)next(*>*)
   704   {
   705     obtain x where "A x" \<proof>
   706     have B \<proof>
   707   }
   708   note \<open>B\<close>
   709   text_raw \<open>\end{minipage}\<close>
   710 (*<*)
   711 qed
   712 (*>*)
   713 
   714 text \<open>
   715   \<^bigskip>
   716   This explains the meaning of Isar context elements without, without goal
   717   states getting in the way.
   718 \<close>
   719 
   720 
   721 subsection \<open>Structured statements \label{sec:framework-stmt}\<close>
   722 
   723 text \<open>
   724   The syntax of top-level theorem statements is defined as follows:
   725 
   726   \<^medskip>
   727   \begin{tabular}{rcl}
   728   \<open>statement\<close> & \<open>\<equiv>\<close> & \<^theory_text>\<open>name: props and \<dots>\<close> \\
   729   & \<open>|\<close> & \<open>context\<^sup>* conclusion\<close> \\[0.5ex]
   730 
   731   \<open>context\<close> & \<open>\<equiv>\<close> & \<^theory_text>\<open>fixes vars and \<dots>\<close> \\
   732   & \<open>|\<close> & \<^theory_text>\<open>assumes name: props and \<dots>\<close> \\
   733 
   734   \<open>conclusion\<close> & \<open>\<equiv>\<close> & \<^theory_text>\<open>shows name: props and \<dots>\<close> \\
   735   & \<open>|\<close> & \<^theory_text>\<open>obtains vars and \<dots> where name: props and \<dots>\<close> \\
   736   & & \quad \<open>\<BBAR> \<dots>\<close> \\
   737   \end{tabular}
   738 
   739   \<^medskip>
   740   A simple statement consists of named propositions. The full form admits
   741   local context elements followed by the actual conclusions, such as ``\<^theory_text>\<open>fixes
   742   x assumes A x shows B x\<close>''. The final result emerges as a Pure rule after
   743   discharging the context: @{prop "\<And>x. A x \<Longrightarrow> B x"}.
   744 
   745   The \<^theory_text>\<open>obtains\<close> variant is another abbreviation defined below; unlike
   746   \<^theory_text>\<open>obtain\<close> (cf.\ \secref{sec:framework-context}) there may be several
   747   ``cases'' separated by ``\<open>\<BBAR>\<close>'', each consisting of several parameters
   748   (\<open>vars\<close>) and several premises (\<open>props\<close>). This specifies multi-branch
   749   elimination rules.
   750 
   751   \<^medskip>
   752   \begin{tabular}{l}
   753   \<^theory_text>\<open>obtains "\<^vec>x" where "\<^vec>A" "\<^vec>x"  "\<BBAR>"  \<dots>  \<equiv>\<close> \\[0.5ex]
   754   \quad \<^theory_text>\<open>fixes thesis\<close> \\
   755   \quad \<^theory_text>\<open>assumes [intro]: "\<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis"  and  \<dots>\<close> \\
   756   \quad \<^theory_text>\<open>shows thesis\<close> \\
   757   \end{tabular}
   758   \<^medskip>
   759 
   760   Presenting structured statements in such an ``open'' format usually
   761   simplifies the subsequent proof, because the outer structure of the problem
   762   is already laid out directly. E.g.\ consider the following canonical
   763   patterns for \<^theory_text>\<open>shows\<close> and \<^theory_text>\<open>obtains\<close>, respectively:
   764 \<close>
   765 
   766 text_raw \<open>\begin{minipage}{0.5\textwidth}\<close>
   767 
   768   theorem
   769     fixes x and y
   770     assumes "A x" and "B y"
   771     shows "C x y"
   772   proof -
   773     from \<open>A x\<close> and \<open>B y\<close>
   774     show "C x y" \<proof>
   775   qed
   776 
   777 text_raw \<open>\end{minipage}\begin{minipage}{0.5\textwidth}\<close>
   778 
   779   theorem
   780     obtains x and y
   781     where "A x" and "B y"
   782   proof -
   783     have "A a" and "B b" \<proof>
   784     then show thesis ..
   785   qed
   786 
   787 text_raw \<open>\end{minipage}\<close>
   788 
   789 text \<open>
   790   \<^medskip>
   791   Here local facts \<open>\<open>A x\<close>\<close> and \<open>\<open>B y\<close>\<close> are referenced immediately; there is no
   792   need to decompose the logical rule structure again. In the second proof the
   793   final ``\<^theory_text>\<open>then show thesis ..\<close>'' involves the local rule case \<open>\<And>x y. A x \<Longrightarrow> B
   794   y \<Longrightarrow> thesis\<close> for the particular instance of terms \<open>a\<close> and \<open>b\<close> produced in the
   795   body.
   796 \<close>
   797 
   798 
   799 subsection \<open>Structured proof refinement \label{sec:framework-subproof}\<close>
   800 
   801 text \<open>
   802   By breaking up the grammar for the Isar proof language, we may understand a
   803   proof text as a linear sequence of individual proof commands. These are
   804   interpreted as transitions of the Isar virtual machine (Isar/VM), which
   805   operates on a block-structured configuration in single steps. This allows
   806   users to write proof texts in an incremental manner, and inspect
   807   intermediate configurations for debugging.
   808 
   809   The basic idea is analogous to evaluating algebraic expressions on a stack
   810   machine: \<open>(a + b) \<cdot> c\<close> then corresponds to a sequence of single transitions
   811   for each symbol \<open>(, a, +, b, ), \<cdot>, c\<close>. In Isar the algebraic values are
   812   facts or goals, and the operations are inferences.
   813 
   814   \<^medskip>
   815   The Isar/VM state maintains a stack of nodes, each node contains the local
   816   proof context, the linguistic mode, and a pending goal (optional). The mode
   817   determines the type of transition that may be performed next, it essentially
   818   alternates between forward and backward reasoning, with an intermediate
   819   stage for chained facts (see \figref{fig:isar-vm}).
   820 
   821   \begin{figure}[htb]
   822   \begin{center}
   823   \includegraphics[width=0.8\textwidth]{isar-vm}
   824   \end{center}
   825   \caption{Isar/VM modes}\label{fig:isar-vm}
   826   \end{figure}
   827 
   828   For example, in \<open>state\<close> mode Isar acts like a mathematical scratch-pad,
   829   accepting declarations like \<^theory_text>\<open>fix\<close>, \<^theory_text>\<open>assume\<close>, and claims like \<^theory_text>\<open>have\<close>,
   830   \<^theory_text>\<open>show\<close>. A goal statement changes the mode to \<open>prove\<close>, which means that we
   831   may now refine the problem via \<^theory_text>\<open>unfolding\<close> or \<^theory_text>\<open>proof\<close>. Then we are again
   832   in \<open>state\<close> mode of a proof body, which may issue \<^theory_text>\<open>show\<close> statements to solve
   833   pending subgoals. A concluding \<^theory_text>\<open>qed\<close> will return to the original \<open>state\<close>
   834   mode one level upwards. The subsequent Isar/VM trace indicates block
   835   structure, linguistic mode, goal state, and inferences:
   836 \<close>
   837 
   838 text_raw \<open>\begingroup\footnotesize\<close>
   839 (*<*)notepad begin
   840 (*>*)
   841   text_raw \<open>\begin{minipage}[t]{0.18\textwidth}\<close>
   842   have "A \<longrightarrow> B"
   843   proof
   844     assume A
   845     show B
   846       \<proof>
   847   qed
   848   text_raw \<open>\end{minipage}\quad
   849 \begin{minipage}[t]{0.06\textwidth}
   850 \<open>begin\<close> \\
   851 \\
   852 \\
   853 \<open>begin\<close> \\
   854 \<open>end\<close> \\
   855 \<open>end\<close> \\
   856 \end{minipage}
   857 \begin{minipage}[t]{0.08\textwidth}
   858 \<open>prove\<close> \\
   859 \<open>state\<close> \\
   860 \<open>state\<close> \\
   861 \<open>prove\<close> \\
   862 \<open>state\<close> \\
   863 \<open>state\<close> \\
   864 \end{minipage}\begin{minipage}[t]{0.35\textwidth}
   865 \<open>(A \<longrightarrow> B) \<Longrightarrow> #(A \<longrightarrow> B)\<close> \\
   866 \<open>(A \<Longrightarrow> B) \<Longrightarrow> #(A \<longrightarrow> B)\<close> \\
   867 \\
   868 \\
   869 \<open>#(A \<longrightarrow> B)\<close> \\
   870 \<open>A \<longrightarrow> B\<close> \\
   871 \end{minipage}\begin{minipage}[t]{0.4\textwidth}
   872 \<open>(init)\<close> \\
   873 \<open>(resolution impI)\<close> \\
   874 \\
   875 \\
   876 \<open>(refinement #A \<Longrightarrow> B)\<close> \\
   877 \<open>(finish)\<close> \\
   878 \end{minipage}\<close>
   879 (*<*)
   880 end
   881 (*>*)
   882 text_raw \<open>\endgroup\<close>
   883 
   884 text \<open>
   885   Here the @{inference refinement} inference from
   886   \secref{sec:framework-resolution} mediates composition of Isar subproofs
   887   nicely. Observe that this principle incorporates some degree of freedom in
   888   proof composition. In particular, the proof body allows parameters and
   889   assumptions to be re-ordered, or commuted according to Hereditary Harrop
   890   Form. Moreover, context elements that are not used in a subproof may be
   891   omitted altogether. For example:
   892 \<close>
   893 
   894 text_raw \<open>\begin{minipage}{0.5\textwidth}\<close>
   895 
   896 (*<*)
   897 notepad
   898 begin
   899 (*>*)
   900   have "\<And>x y. A x \<Longrightarrow> B y \<Longrightarrow> C x y"
   901   proof -
   902     fix x and y
   903     assume "A x" and "B y"
   904     show "C x y" \<proof>
   905   qed
   906 
   907 text_raw \<open>\end{minipage}\begin{minipage}{0.5\textwidth}\<close>
   908 
   909 (*<*)
   910 next
   911 (*>*)
   912   have "\<And>x y. A x \<Longrightarrow> B y \<Longrightarrow> C x y"
   913   proof -
   914     fix x assume "A x"
   915     fix y assume "B y"
   916     show "C x y" \<proof>
   917   qed
   918 
   919 text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}{0.5\textwidth}\<close>
   920 
   921 (*<*)
   922 next
   923 (*>*)
   924   have "\<And>x y. A x \<Longrightarrow> B y \<Longrightarrow> C x y"
   925   proof -
   926     fix y assume "B y"
   927     fix x assume "A x"
   928     show "C x y" \<proof>
   929   qed
   930 
   931 text_raw \<open>\end{minipage}\begin{minipage}{0.5\textwidth}\<close>
   932 (*<*)
   933 next
   934 (*>*)
   935   have "\<And>x y. A x \<Longrightarrow> B y \<Longrightarrow> C x y"
   936   proof -
   937     fix y assume "B y"
   938     fix x
   939     show "C x y" \<proof>
   940   qed
   941 (*<*)
   942 end
   943 (*>*)
   944 
   945 text_raw \<open>\end{minipage}\<close>
   946 
   947 text \<open>
   948   \<^medskip>
   949   Such fine-tuning of Isar text is practically important to improve
   950   readability. Contexts elements are rearranged according to the natural flow
   951   of reasoning in the body, while still observing the overall scoping rules.
   952 
   953   \<^medskip>
   954   This illustrates the basic idea of structured proof processing in Isar. The
   955   main mechanisms are based on natural deduction rule composition within the
   956   Pure framework. In particular, there are no direct operations on goal states
   957   within the proof body. Moreover, there is no hidden automated reasoning
   958   involved, just plain unification.
   959 \<close>
   960 
   961 
   962 subsection \<open>Calculational reasoning \label{sec:framework-calc}\<close>
   963 
   964 text \<open>
   965   The existing Isar infrastructure is sufficiently flexible to support
   966   calculational reasoning (chains of transitivity steps) as derived concept.
   967   The generic proof elements introduced below depend on rules declared as
   968   @{attribute trans} in the context. It is left to the object-logic to provide
   969   a suitable rule collection for mixed relations of \<open>=\<close>, \<open><\<close>, \<open>\<le>\<close>, \<open>\<subset>\<close>, \<open>\<subseteq>\<close>
   970   etc. Due to the flexibility of rule composition
   971   (\secref{sec:framework-resolution}), substitution of equals by equals is
   972   covered as well, even substitution of inequalities involving monotonicity
   973   conditions; see also @{cite \<open>\S6\<close> "Wenzel-PhD"} and @{cite
   974   "Bauer-Wenzel:2001"}.
   975 
   976   The generic calculational mechanism is based on the observation that rules
   977   such as \<open>trans:\<close>~@{prop "x = y \<Longrightarrow> y = z \<Longrightarrow> x = z"} proceed from the premises
   978   towards the conclusion in a deterministic fashion. Thus we may reason in
   979   forward mode, feeding intermediate results into rules selected from the
   980   context. The course of reasoning is organized by maintaining a secondary
   981   fact called ``@{fact calculation}'', apart from the primary ``@{fact this}''
   982   already provided by the Isar primitives. In the definitions below,
   983   @{attribute OF} refers to @{inference resolution}
   984   (\secref{sec:framework-resolution}) with multiple rule arguments, and
   985   \<open>trans\<close> represents to a suitable rule from the context:
   986 
   987   \begin{matharray}{rcl}
   988     \<^theory_text>\<open>also"\<^sub>0"\<close> & \equiv & \<^theory_text>\<open>note calculation = this\<close> \\
   989     \<^theory_text>\<open>also"\<^sub>n\<^sub>+\<^sub>1"\<close> & \equiv & \<^theory_text>\<open>note calculation = trans [OF calculation this]\<close> \\[0.5ex]
   990     \<^theory_text>\<open>finally\<close> & \equiv & \<^theory_text>\<open>also from calculation\<close> \\
   991   \end{matharray}
   992 
   993   The start of a calculation is determined implicitly in the text: here
   994   \<^theory_text>\<open>also\<close> sets @{fact calculation} to the current result; any subsequent
   995   occurrence will update @{fact calculation} by combination with the next
   996   result and a transitivity rule. The calculational sequence is concluded via
   997   \<^theory_text>\<open>finally\<close>, where the final result is exposed for use in a concluding claim.
   998 
   999   Here is a canonical proof pattern, using \<^theory_text>\<open>have\<close> to establish the
  1000   intermediate results:
  1001 \<close>
  1002 
  1003 (*<*)
  1004 notepad
  1005 begin
  1006   fix a b c d :: 'a
  1007 (*>*)
  1008   have "a = b" \<proof>
  1009   also have "\<dots> = c" \<proof>
  1010   also have "\<dots> = d" \<proof>
  1011   finally have "a = d" .
  1012 (*<*)
  1013 end
  1014 (*>*)
  1015 
  1016 text \<open>
  1017   The term ``\<open>\<dots>\<close>'' (literal ellipsis) is a special abbreviation provided by
  1018   the Isabelle/Isar term syntax: it statically refers to the right-hand side
  1019   argument of the previous statement given in the text. Thus it happens to
  1020   coincide with relevant sub-expressions in the calculational chain, but the
  1021   exact correspondence is dependent on the transitivity rules being involved.
  1022 
  1023   \<^medskip>
  1024   Symmetry rules such as @{prop "x = y \<Longrightarrow> y = x"} are like transitivities with
  1025   only one premise. Isar maintains a separate rule collection declared via the
  1026   @{attribute sym} attribute, to be used in fact expressions ``\<open>a
  1027   [symmetric]\<close>'', or single-step proofs ``\<^theory_text>\<open>assume "x = y" then have "y = x"
  1028   ..\<close>''.
  1029 \<close>
  1030 
  1031 end