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