src/Doc/Isar_Ref/Framework.thy

 
 chapter \<open>The Isabelle/Isar Framework \label{ch:isar-framework}\<close>
 
 text \<open>
   Isabelle/Isar @{cite "Wenzel:1999:TPHOL" and "Wenzel-PhD" and
-  "Nipkow-TYPES02" and "Wenzel-Paulson:2006" and "Wenzel:2006:Festschrift"}
-  is intended as a generic framework for developing formal
-  mathematical documents with full proof checking.  Definitions and
-  proofs are organized as theories.  An assembly of theory sources may
-  be presented as a printed document; see also
-  \chref{ch:document-prep}.
-
-  The main objective of Isar is the design of a human-readable
-  structured proof language, which is called the ``primary proof
-  format'' in Isar terminology.  Such a primary proof language is
-  somewhere in the middle between the extremes of primitive proof
-  objects and actual natural language.  In this respect, Isar is a bit
-  more formalistic than Mizar @{cite "Trybulec:1993:MizarFeatures" and
-  "Rudnicki:1992:MizarOverview" and "Wiedijk:1999:Mizar"},
-  using logical symbols for certain reasoning schemes where Mizar
-  would prefer English words; see @{cite "Wenzel-Wiedijk:2002"} for
-  further comparisons of these systems.
-
-  So Isar challenges the traditional way of recording informal proofs
-  in mathematical prose, as well as the common tendency to see fully
-  formal proofs directly as objects of some logical calculus (e.g.\
-  \<open>\<lambda>\<close>-terms in a version of type theory).  In fact, Isar is
-  better understood as an interpreter of a simple block-structured
-  language for describing the data flow of local facts and goals,
-  interspersed with occasional invocations of proof methods.
-  Everything is reduced to logical inferences internally, but these
-  steps are somewhat marginal compared to the overall bookkeeping of
-  the interpretation process.  Thanks to careful design of the syntax
-  and semantics of Isar language elements, a formal record of Isar
-  instructions may later appear as an intelligible text to the
-  attentive reader.
-
-  The Isar proof language has emerged from careful analysis of some
-  inherent virtues of the existing logical framework of Isabelle/Pure
-  @{cite "paulson-found" and "paulson700"}, notably composition of higher-order
-  natural deduction rules, which is a generalization of Gentzen's
-  original calculus @{cite "Gentzen:1935"}.  The approach of generic
-  inference systems in Pure is continued by Isar towards actual proof
-  texts.
-
-  Concrete applications require another intermediate layer: an
-  object-logic.  Isabelle/HOL @{cite "isa-tutorial"} (simply-typed
-  set-theory) is being used most of the time; Isabelle/ZF
-  @{cite "isabelle-ZF"} is less extensively developed, although it would
-  probably fit better for classical mathematics.
-
-  \<^medskip>
-  In order to illustrate natural deduction in Isar, we shall
-  refer to the background theory and library of Isabelle/HOL.  This
-  includes common notions of predicate logic, naive set-theory etc.\
-  using fairly standard mathematical notation.  From the perspective
-  of generic natural deduction there is nothing special about the
-  logical connectives of HOL (\<open>\<and>\<close>, \<open>\<or>\<close>, \<open>\<forall>\<close>,
-  \<open>\<exists>\<close>, etc.), only the resulting reasoning principles are
-  relevant to the user.  There are similar rules available for
-  set-theory operators (\<open>\<inter>\<close>, \<open>\<union>\<close>, \<open>\<Inter>\<close>, \<open>\<Union>\<close>, etc.), or any other theory developed in the library (lattice
+  "Nipkow-TYPES02" and "Wenzel-Paulson:2006" and "Wenzel:2006:Festschrift"} is
+  intended as a generic framework for developing formal mathematical documents
+  with full proof checking. Definitions and proofs are organized as theories.
+  An assembly of theory sources may be presented as a printed document; see
+  also \chref{ch:document-prep}.
+
+  The main objective of Isar is the design of a human-readable structured
+  proof language, which is called the ``primary proof format'' in Isar
+  terminology. Such a primary proof language is somewhere in the middle
+  between the extremes of primitive proof objects and actual natural language.
+  In this respect, Isar is a bit more formalistic than Mizar @{cite
+  "Trybulec:1993:MizarFeatures" and "Rudnicki:1992:MizarOverview" and
+  "Wiedijk:1999:Mizar"}, using logical symbols for certain reasoning schemes
+  where Mizar would prefer English words; see @{cite "Wenzel-Wiedijk:2002"}
+  for further comparisons of these systems.
+
+  So Isar challenges the traditional way of recording informal proofs in
+  mathematical prose, as well as the common tendency to see fully formal
+  proofs directly as objects of some logical calculus (e.g.\ \<open>\<lambda>\<close>-terms in a
+  version of type theory). In fact, Isar is better understood as an
+  interpreter of a simple block-structured language for describing the data
+  flow of local facts and goals, interspersed with occasional invocations of
+  proof methods. Everything is reduced to logical inferences internally, but
+  these steps are somewhat marginal compared to the overall bookkeeping of the
+  interpretation process. Thanks to careful design of the syntax and semantics
+  of Isar language elements, a formal record of Isar instructions may later
+  appear as an intelligible text to the attentive reader.
+
+  The Isar proof language has emerged from careful analysis of some inherent
+  virtues of the existing logical framework of Isabelle/Pure @{cite
+  "paulson-found" and "paulson700"}, notably composition of higher-order
+  natural deduction rules, which is a generalization of Gentzen's original
+  calculus @{cite "Gentzen:1935"}. The approach of generic inference systems
+  in Pure is continued by Isar towards actual proof texts.
+
+  Concrete applications require another intermediate layer: an object-logic.
+  Isabelle/HOL @{cite "isa-tutorial"} (simply-typed set-theory) is being used
+  most of the time; Isabelle/ZF @{cite "isabelle-ZF"} is less extensively
+  developed, although it would probably fit better for classical mathematics.
+
+  \<^medskip>
+  In order to illustrate natural deduction in Isar, we shall refer to the
+  background theory and library of Isabelle/HOL. This includes common notions
+  of predicate logic, naive set-theory etc.\ using fairly standard
+  mathematical notation. From the perspective of generic natural deduction
+  there is nothing special about the logical connectives of HOL (\<open>\<and>\<close>, \<open>\<or>\<close>,
+  \<open>\<forall>\<close>, \<open>\<exists>\<close>, etc.), only the resulting reasoning principles are relevant to the
+  user. There are similar rules available for set-theory operators (\<open>\<inter>\<close>, \<open>\<union>\<close>,
+  \<open>\<Inter>\<close>, \<open>\<Union>\<close>, etc.), or any other theory developed in the library (lattice
   theory, topology etc.).
 
-  Subsequently we briefly review fragments of Isar proof texts
-  corresponding directly to such general deduction schemes.  The
-  examples shall refer to set-theory, to minimize the danger of
-  understanding connectives of predicate logic as something special.
-
-  \<^medskip>
-  The following deduction performs \<open>\<inter>\<close>-introduction,
-  working forwards from assumptions towards the conclusion.  We give
-  both the Isar text, and depict the primitive rule involved, as
-  determined by unification of the problem against rules that are
-  declared in the library context.
+  Subsequently we briefly review fragments of Isar proof texts corresponding
+  directly to such general deduction schemes. The examples shall refer to
+  set-theory, to minimize the danger of understanding connectives of predicate
+  logic as something special.
+
+  \<^medskip>
+  The following deduction performs \<open>\<inter>\<close>-introduction, working forwards from
+  assumptions towards the conclusion. We give both the Isar text, and depict
+  the primitive rule involved, as determined by unification of the problem
+  against rules that are declared in the library context.
 \<close>
 
 text_raw \<open>\medskip\begin{minipage}{0.6\textwidth}\<close>
 
 (*<*)

 
 text_raw \<open>\end{minipage}\<close>
 
 text \<open>
   \<^medskip>
-  Note that @{command assume} augments the proof
-  context, @{command then} indicates that the current fact shall be
-  used in the next step, and @{command have} states an intermediate
-  goal.  The two dots ``@{command ".."}'' refer to a complete proof of
-  this claim, using the indicated facts and a canonical rule from the
-  context.  We could have been more explicit here by spelling out the
-  final proof step via the @{command "by"} command:
+  Note that @{command assume} augments the proof context, @{command then}
+  indicates that the current fact shall be used in the next step, and
+  @{command have} states an intermediate goal. The two dots ``@{command
+  ".."}'' refer to a complete proof of this claim, using the indicated facts
+  and a canonical rule from the context. We could have been more explicit here
+  by spelling out the final proof step via the @{command "by"} command:
 \<close>
 
 (*<*)
 notepad
 begin

 (*<*)
 end
 (*>*)
 
 text \<open>
-  The format of the \<open>\<inter>\<close>-introduction rule represents
-  the most basic inference, which proceeds from given premises to a
-  conclusion, without any nested proof context involved.
-
-  The next example performs backwards introduction on @{term "\<Inter>\<A>"},
-  the intersection of all sets within a given set.  This requires a
-  nested proof of set membership within a local context, where @{term
-  A} is an arbitrary-but-fixed member of the collection:
+  The format of the \<open>\<inter>\<close>-introduction rule represents the most basic inference,
+  which proceeds from given premises to a conclusion, without any nested proof
+  context involved.
+
+  The next example performs backwards introduction on @{term "\<Inter>\<A>"}, the
+  intersection of all sets within a given set. This requires a nested proof of
+  set membership within a local context, where @{term A} is an
+  arbitrary-but-fixed member of the collection:
 \<close>
 
 text_raw \<open>\medskip\begin{minipage}{0.6\textwidth}\<close>
 
 (*<*)

 
 text_raw \<open>\end{minipage}\<close>
 
 text \<open>
   \<^medskip>
-  This Isar reasoning pattern again refers to the
-  primitive rule depicted above.  The system determines it in the
-  ``@{command proof}'' step, which could have been spelled out more
-  explicitly as ``@{command proof}~\<open>(rule InterI)\<close>''.  Note
-  that the rule involves both a local parameter @{term "A"} and an
-  assumption @{prop "A \<in> \<A>"} in the nested reasoning.  This kind of
+  This Isar reasoning pattern again refers to the primitive rule depicted
+  above. The system determines it in the ``@{command proof}'' step, which
+  could have been spelled out more explicitly as ``@{command proof}~\<open>(rule
+  InterI)\<close>''. Note that the rule involves both a local parameter @{term "A"}
+  and an assumption @{prop "A \<in> \<A>"} in the nested reasoning. This kind of
   compound rule typically demands a genuine sub-proof in Isar, working
-  backwards rather than forwards as seen before.  In the proof body we
-  encounter the @{command fix}-@{command assume}-@{command show}
-  outline of nested sub-proofs that is typical for Isar.  The final
-  @{command show} is like @{command have} followed by an additional
-  refinement of the enclosing claim, using the rule derived from the
-  proof body.
-
-  \<^medskip>
-  The next example involves @{term "\<Union>\<A>"}, which can be
-  characterized as the set of all @{term "x"} such that @{prop "\<exists>A. x
-  \<in> A \<and> A \<in> \<A>"}.  The elimination rule for @{prop "x \<in> \<Union>\<A>"} does
-  not mention \<open>\<exists>\<close> and \<open>\<and>\<close> at all, but admits to obtain
-  directly a local @{term "A"} such that @{prop "x \<in> A"} and @{prop "A
-  \<in> \<A>"} hold.  This corresponds to the following Isar proof and
+  backwards rather than forwards as seen before. In the proof body we
+  encounter the @{command fix}-@{command assume}-@{command show} outline of
+  nested sub-proofs that is typical for Isar. The final @{command show} is
+  like @{command have} followed by an additional refinement of the enclosing
+  claim, using the rule derived from the proof body.
+
+  \<^medskip>
+  The next example involves @{term "\<Union>\<A>"}, which can be characterized as the
+  set of all @{term "x"} such that @{prop "\<exists>A. x \<in> A \<and> A \<in> \<A>"}. The
+  elimination rule for @{prop "x \<in> \<Union>\<A>"} does not mention \<open>\<exists>\<close> and \<open>\<and>\<close> at all,
+  but admits to obtain directly a local @{term "A"} such that @{prop "x \<in> A"}
+  and @{prop "A \<in> \<A>"} hold. This corresponds to the following Isar proof and
   inference rule, respectively:
 \<close>
 
 text_raw \<open>\medskip\begin{minipage}{0.6\textwidth}\<close>
 

 
 text_raw \<open>\end{minipage}\<close>
 
 text \<open>
   \<^medskip>
-  Although the Isar proof follows the natural
-  deduction rule closely, the text reads not as natural as
-  anticipated.  There is a double occurrence of an arbitrary
-  conclusion @{prop "C"}, which represents the final result, but is
-  irrelevant for now.  This issue arises for any elimination rule
-  involving local parameters.  Isar provides the derived language
-  element @{command obtain}, which is able to perform the same
-  elimination proof more conveniently:
+  Although the Isar proof follows the natural deduction rule closely, the text
+  reads not as natural as anticipated. There is a double occurrence of an
+  arbitrary conclusion @{prop "C"}, which represents the final result, but is
+  irrelevant for now. This issue arises for any elimination rule involving
+  local parameters. Isar provides the derived language element @{command
+  obtain}, which is able to perform the same elimination proof more
+  conveniently:
 \<close>
 
 (*<*)
 notepad
 begin

 (*<*)
 end
 (*>*)
 
 text \<open>
-  Here we avoid to mention the final conclusion @{prop "C"}
-  and return to plain forward reasoning.  The rule involved in the
-  ``@{command ".."}'' proof is the same as before.
+  Here we avoid to mention the final conclusion @{prop "C"} and return to
+  plain forward reasoning. The rule involved in the ``@{command ".."}'' proof
+  is the same as before.
 \<close>
 
 
 section \<open>The Pure framework \label{sec:framework-pure}\<close>
 
 text \<open>
   The Pure logic @{cite "paulson-found" and "paulson700"} is an intuitionistic
-  fragment of higher-order logic @{cite "church40"}.  In type-theoretic
-  parlance, there are three levels of \<open>\<lambda>\<close>-calculus with
-  corresponding arrows \<open>\<Rightarrow>\<close>/\<open>\<And>\<close>/\<open>\<Longrightarrow>\<close>:
+  fragment of higher-order logic @{cite "church40"}. In type-theoretic
+  parlance, there are three levels of \<open>\<lambda>\<close>-calculus with corresponding arrows
+  \<open>\<Rightarrow>\<close>/\<open>\<And>\<close>/\<open>\<Longrightarrow>\<close>:
 
   \<^medskip>
   \begin{tabular}{ll}
   \<open>\<alpha> \<Rightarrow> \<beta>\<close> & syntactic function space (terms depending on terms) \\
   \<open>\<And>x. B(x)\<close> & universal quantification (proofs depending on terms) \\
   \<open>A \<Longrightarrow> B\<close> & implication (proofs depending on proofs) \\
   \end{tabular}
   \<^medskip>
 
-  Here only the types of syntactic terms, and the
-  propositions of proof terms have been shown.  The \<open>\<lambda>\<close>-structure of proofs can be recorded as an optional feature of
-  the Pure inference kernel @{cite "Berghofer-Nipkow:2000:TPHOL"}, but
-  the formal system can never depend on them due to \<^emph>\<open>proof
-  irrelevance\<close>.
-
-  On top of this most primitive layer of proofs, Pure implements a
-  generic calculus for nested natural deduction rules, similar to
-  @{cite "Schroeder-Heister:1984"}.  Here object-logic inferences are
-  internalized as formulae over \<open>\<And>\<close> and \<open>\<Longrightarrow>\<close>.
-  Combining such rule statements may involve higher-order unification
-  @{cite "paulson-natural"}.
+  Here only the types of syntactic terms, and the propositions of proof terms
+  have been shown. The \<open>\<lambda>\<close>-structure of proofs can be recorded as an optional
+  feature of the Pure inference kernel @{cite "Berghofer-Nipkow:2000:TPHOL"},
+  but the formal system can never depend on them due to \<^emph>\<open>proof irrelevance\<close>.
+
+  On top of this most primitive layer of proofs, Pure implements a generic
+  calculus for nested natural deduction rules, similar to @{cite
+  "Schroeder-Heister:1984"}. Here object-logic inferences are internalized as
+  formulae over \<open>\<And>\<close> and \<open>\<Longrightarrow>\<close>. Combining such rule statements may involve
+  higher-order unification @{cite "paulson-natural"}.
 \<close>
 
 
 subsection \<open>Primitive inferences\<close>
 
 text \<open>
-  Term syntax provides explicit notation for abstraction \<open>\<lambda>x ::
-  \<alpha>. b(x)\<close> and application \<open>b a\<close>, while types are usually
-  implicit thanks to type-inference; terms of type \<open>prop\<close> are
-  called propositions.  Logical statements are composed via \<open>\<And>x
-  :: \<alpha>. B(x)\<close> and \<open>A \<Longrightarrow> B\<close>.  Primitive reasoning operates on
-  judgments of the form \<open>\<Gamma> \<turnstile> \<phi>\<close>, with standard introduction
-  and elimination rules for \<open>\<And>\<close> and \<open>\<Longrightarrow>\<close> that refer to
-  fixed parameters \<open>x\<^sub>1, \<dots>, x\<^sub>m\<close> and hypotheses
-  \<open>A\<^sub>1, \<dots>, A\<^sub>n\<close> from the context \<open>\<Gamma>\<close>;
-  the corresponding proof terms are left implicit.  The subsequent
-  inference rules define \<open>\<Gamma> \<turnstile> \<phi>\<close> inductively, relative to a
-  collection of axioms:
+  Term syntax provides explicit notation for abstraction \<open>\<lambda>x :: \<alpha>. b(x)\<close> and
+  application \<open>b a\<close>, while types are usually implicit thanks to
+  type-inference; terms of type \<open>prop\<close> are called propositions. Logical
+  statements are composed via \<open>\<And>x :: \<alpha>. B(x)\<close> and \<open>A \<Longrightarrow> B\<close>. Primitive reasoning
+  operates on judgments of the form \<open>\<Gamma> \<turnstile> \<phi>\<close>, with standard introduction and
+  elimination rules for \<open>\<And>\<close> and \<open>\<Longrightarrow>\<close> that refer to fixed parameters \<open>x\<^sub>1, \<dots>,
+  x\<^sub>m\<close> and hypotheses \<open>A\<^sub>1, \<dots>, A\<^sub>n\<close> from the context \<open>\<Gamma>\<close>; the corresponding
+  proof terms are left implicit. The subsequent inference rules define \<open>\<Gamma> \<turnstile> \<phi>\<close>
+  inductively, relative to a collection of axioms:
 
   \[
   \infer{\<open>\<turnstile> A\<close>}{(\<open>A\<close> \mbox{~axiom})}
   \qquad
   \infer{\<open>A \<turnstile> A\<close>}{}

   \infer{\<open>\<Gamma> - A \<turnstile> A \<Longrightarrow> B\<close>}{\<open>\<Gamma> \<turnstile> B\<close>}
   \qquad
   \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>}
   \]
 
-  Furthermore, Pure provides a built-in equality \<open>\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow>
-  prop\<close> with axioms for reflexivity, substitution, extensionality,
-  and \<open>\<alpha>\<beta>\<eta>\<close>-conversion on \<open>\<lambda>\<close>-terms.
-
-  \<^medskip>
-  An object-logic introduces another layer on top of Pure,
-  e.g.\ with types \<open>i\<close> for individuals and \<open>o\<close> for
-  propositions, term constants \<open>Trueprop :: o \<Rightarrow> prop\<close> as
-  (implicit) derivability judgment and connectives like \<open>\<and> :: o
-  \<Rightarrow> o \<Rightarrow> o\<close> or \<open>\<forall> :: (i \<Rightarrow> o) \<Rightarrow> o\<close>, and axioms for object-level
-  rules such as \<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 are represented as theorems of
-  Pure.  After the initial object-logic setup, further axiomatizations
-  are usually avoided; plain definitions and derived principles are
-  used exclusively.
+  Furthermore, Pure provides a built-in equality \<open>\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop\<close> with
+  axioms for reflexivity, substitution, extensionality, and \<open>\<alpha>\<beta>\<eta>\<close>-conversion
+  on \<open>\<lambda>\<close>-terms.
+
+  \<^medskip>
+  An object-logic introduces another layer on top of Pure, e.g.\ with types
+  \<open>i\<close> for individuals and \<open>o\<close> for propositions, term constants \<open>Trueprop :: o
+  \<Rightarrow> prop\<close> as (implicit) derivability judgment and connectives like \<open>\<and> :: o \<Rightarrow> o
+  \<Rightarrow> o\<close> or \<open>\<forall> :: (i \<Rightarrow> o) \<Rightarrow> o\<close>, and axioms for object-level rules such as
+  \<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
+  are represented as theorems of Pure. After the initial object-logic setup,
+  further axiomatizations are usually avoided; plain definitions and derived
+  principles are used exclusively.
 \<close>
 
 
 subsection \<open>Reasoning with rules \label{sec:framework-resolution}\<close>
 
 text \<open>
-  Primitive inferences mostly serve foundational purposes.  The main
-  reasoning mechanisms of Pure operate on nested natural deduction
-  rules expressed as formulae, using \<open>\<And>\<close> to bind local
-  parameters and \<open>\<Longrightarrow>\<close> to express entailment.  Multiple
-  parameters and premises are represented by repeating these
+  Primitive inferences mostly serve foundational purposes. The main reasoning
+  mechanisms of Pure operate on nested natural deduction rules expressed as
+  formulae, using \<open>\<And>\<close> to bind local parameters and \<open>\<Longrightarrow>\<close> to express entailment.
+  Multiple parameters and premises are represented by repeating these
   connectives in a right-associative manner.
 
-  Since \<open>\<And>\<close> and \<open>\<Longrightarrow>\<close> commute thanks to the theorem
-  @{prop "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}, we may assume w.l.o.g.\
-  that rule statements always observe the normal form where
-  quantifiers are pulled in front of implications at each level of
-  nesting.  This means that any Pure proposition may be presented as a
-  \<^emph>\<open>Hereditary Harrop Formula\<close> @{cite "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 \<ge> 0\<close>, and \<open>A\<close> atomic, and \<open>H\<^sub>1, \<dots>, H\<^sub>n\<close> being recursively of the same format.
-  Following the convention that outermost quantifiers are implicit,
-  Horn clauses \<open>A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> A\<close> are a special
-  case of this.
-
-  For example, \<open>\<inter>\<close>-introduction rule encountered before is
-  represented as a Pure theorem as follows:
+  Since \<open>\<And>\<close> and \<open>\<Longrightarrow>\<close> commute thanks to the theorem @{prop "(A \<Longrightarrow> (\<And>x. B x)) \<equiv>
+  (\<And>x. A \<Longrightarrow> B x)"}, we may assume w.l.o.g.\ that rule statements always observe
+  the normal form where quantifiers are pulled in front of implications at
+  each level of nesting. This means that any Pure proposition may be presented
+  as a \<^emph>\<open>Hereditary Harrop Formula\<close> @{cite "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 \<ge> 0\<close>, and \<open>A\<close> atomic, and \<open>H\<^sub>1, \<dots>,
+  H\<^sub>n\<close> being recursively of the same format. Following the convention that
+  outermost quantifiers are implicit, Horn clauses \<open>A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> A\<close> are a
+  special case of this.
+
+  For example, \<open>\<inter>\<close>-introduction rule encountered before is represented as a
+  Pure theorem as follows:
   \[
   \<open>IntI:\<close>~@{prop "x \<in> A \<Longrightarrow> x \<in> B \<Longrightarrow> x \<in> A \<inter> B"}
   \]
 
-  This is a plain Horn clause, since no further nesting on
-  the left is involved.  The general \<open>\<Inter>\<close>-introduction
-  corresponds to a Hereditary Harrop Formula with one additional level
-  of nesting:
+  This is a plain Horn clause, since no further nesting on the left is
+  involved. The general \<open>\<Inter>\<close>-introduction corresponds to a Hereditary Harrop
+  Formula with one additional level of nesting:
   \[
   \<open>InterI:\<close>~@{prop "(\<And>A. A \<in> \<A> \<Longrightarrow> x \<in> A) \<Longrightarrow> x \<in> \<Inter>\<A>"}
   \]
 
   \<^medskip>
-  Goals are also represented as rules: \<open>A\<^sub>1 \<Longrightarrow>
-  \<dots> A\<^sub>n \<Longrightarrow> C\<close> states that the sub-goals \<open>A\<^sub>1, \<dots>,
-  A\<^sub>n\<close> entail the result \<open>C\<close>; for \<open>n = 0\<close> the
-  goal is finished.  To allow \<open>C\<close> being a rule statement
-  itself, we introduce the protective marker \<open># :: prop \<Rightarrow>
-  prop\<close>, which is defined as identity and hidden from the user.  We
-  initialize and finish goal states as follows:
+  Goals are also represented as rules: \<open>A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C\<close> states that the
+  sub-goals \<open>A\<^sub>1, \<dots>, A\<^sub>n\<close> entail the result \<open>C\<close>; for \<open>n = 0\<close> the goal is
+  finished. To allow \<open>C\<close> being a rule statement itself, we introduce the
+  protective marker \<open># :: prop \<Rightarrow> prop\<close>, which is defined as identity and
+  hidden from the user. We initialize and finish goal states as follows:
 
   \[
   \begin{array}{c@ {\qquad}c}
   \infer[(@{inference_def init})]{\<open>C \<Longrightarrow> #C\<close>}{} &
   \infer[(@{inference_def finish})]{\<open>C\<close>}{\<open>#C\<close>}
   \end{array}
   \]
 
-  Goal states are refined in intermediate proof steps until
-  a finished form is achieved.  Here the two main reasoning principles
-  are @{inference resolution}, for back-chaining a rule against a
-  sub-goal (replacing it by zero or more sub-goals), and @{inference
-  assumption}, for solving a sub-goal (finding a short-circuit with
-  local assumptions).  Below \<open>\<^vec>x\<close> stands for \<open>x\<^sub>1, \<dots>, x\<^sub>n\<close> (\<open>n \<ge> 0\<close>).
+  Goal states are refined in intermediate proof steps until a finished form is
+  achieved. Here the two main reasoning principles are @{inference
+  resolution}, for back-chaining a rule against a sub-goal (replacing it by
+  zero or more sub-goals), and @{inference assumption}, for solving a sub-goal
+  (finding a short-circuit with local assumptions). Below \<open>\<^vec>x\<close> stands
+  for \<open>x\<^sub>1, \<dots>, x\<^sub>n\<close> (\<open>n \<ge> 0\<close>).
 
   \[
   \infer[(@{inference_def resolution})]
   {\<open>(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> \<^vec>A (\<^vec>a \<^vec>x))\<vartheta> \<Longrightarrow> C\<vartheta>\<close>}
   {\begin{tabular}{rl}

   \<open>A \<and> B \<Longrightarrow> B \<and> A\<close> & \<open>(finish)\<close> \\
   \end{tabular}
   \<^medskip>
   }
 
-  Compositions of @{inference assumption} after @{inference
-  resolution} occurs quite often, typically in elimination steps.
-  Traditional Isabelle tactics accommodate this by a combined
-  @{inference_def elim_resolution} principle.  In contrast, Isar uses
-  a slightly more refined combination, where the assumptions to be
-  closed are marked explicitly, using again the protective marker
-  \<open>#\<close>:
+  Compositions of @{inference assumption} after @{inference resolution} occurs
+  quite often, typically in elimination steps. Traditional Isabelle tactics
+  accommodate this by a combined @{inference_def elim_resolution} principle.
+  In contrast, Isar uses a slightly more refined combination, where the
+  assumptions to be closed are marked explicitly, using again the protective
+  marker \<open>#\<close>:
 
   \[
   \infer[(@{inference refinement})]
   {\<open>(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> \<^vec>G' (\<^vec>a \<^vec>x))\<vartheta> \<Longrightarrow> C\<vartheta>\<close>}
   {\begin{tabular}{rl}

     \<open>(\<lambda>\<^vec>x. G\<^sub>j (\<^vec>a \<^vec>x))\<vartheta> = #H\<^sub>i\<vartheta>\<close> \\
     & \quad (for each marked \<open>G\<^sub>j\<close> some \<open>#H\<^sub>i\<close>) \\
    \end{tabular}}
   \]
 
-  Here the \<open>sub\<hyphen>proof\<close> rule stems from the
-  main @{command fix}-@{command assume}-@{command show} outline of
-  Isar (cf.\ \secref{sec:framework-subproof}): each assumption
-  indicated in the text results in a marked premise \<open>G\<close> above.
-  The marking enforces resolution against one of the sub-goal's
-  premises.  Consequently, @{command fix}-@{command assume}-@{command
-  show} enables to fit the result of a sub-proof quite robustly into a
-  pending sub-goal, while maintaining a good measure of flexibility.
+  Here the \<open>sub\<hyphen>proof\<close> rule stems from the main @{command fix}-@{command
+  assume}-@{command show} outline of Isar (cf.\
+  \secref{sec:framework-subproof}): each assumption indicated in the text
+  results in a marked premise \<open>G\<close> above. The marking enforces resolution
+  against one of the sub-goal's premises. Consequently, @{command
+  fix}-@{command assume}-@{command show} enables to fit the result of a
+  sub-proof quite robustly into a pending sub-goal, while maintaining a good
+  measure of flexibility.
 \<close>
 
 
 section \<open>The Isar proof language \label{sec:framework-isar}\<close>
 
 text \<open>
-  Structured proofs are presented as high-level expressions for
-  composing entities of Pure (propositions, facts, and goals).  The
-  Isar proof language allows to organize reasoning within the
-  underlying rule calculus of Pure, but Isar is not another logical
-  calculus!
-
-  Isar is an exercise in sound minimalism.  Approximately half of the
-  language is introduced as primitive, the rest defined as derived
-  concepts.  The following grammar describes the core language
-  (category \<open>proof\<close>), which is embedded into theory
-  specification elements such as @{command theorem}; see also
-  \secref{sec:framework-stmt} for the separate category \<open>statement\<close>.
+  Structured proofs are presented as high-level expressions for composing
+  entities of Pure (propositions, facts, and goals). The Isar proof language
+  allows to organize reasoning within the underlying rule calculus of Pure,
+  but Isar is not another logical calculus!
+
+  Isar is an exercise in sound minimalism. Approximately half of the language
+  is introduced as primitive, the rest defined as derived concepts. The
+  following grammar describes the core language (category \<open>proof\<close>), which is
+  embedded into theory specification elements such as @{command theorem}; see
+  also \secref{sec:framework-stmt} for the separate category \<open>statement\<close>.
 
   \<^medskip>
   \begin{tabular}{rcl}
     \<open>theory\<hyphen>stmt\<close> & = & @{command "theorem"}~\<open>statement proof  |\<close>~~@{command "definition"}~\<open>\<dots>  |  \<dots>\<close> \\[1ex]
 

     \<open>goal\<close> & = & @{command "have"}~\<open>name: props proof\<close> \\
     & \<open>|\<close> & @{command "show"}~\<open>name: props proof\<close> \\
   \end{tabular}
 
   \<^medskip>
-  Simultaneous propositions or facts may be separated by the
-  @{keyword "and"} keyword.
-
-  \<^medskip>
-  The syntax for terms and propositions is inherited from
-  Pure (and the object-logic).  A \<open>pattern\<close> is a \<open>term\<close> with schematic variables, to be bound by higher-order
-  matching.
-
-  \<^medskip>
-  Facts may be referenced by name or proposition.  For
-  example, the result of ``@{command have}~\<open>a: A \<langle>proof\<rangle>\<close>''
-  becomes available both as \<open>a\<close> and
-  \isacharbackquoteopen\<open>A\<close>\isacharbackquoteclose.  Moreover,
-  fact expressions may involve attributes that modify either the
-  theorem or the background context.  For example, the expression
-  ``\<open>a [OF b]\<close>'' refers to the composition of two facts
-  according to the @{inference resolution} inference of
-  \secref{sec:framework-resolution}, while ``\<open>a [intro]\<close>''
-  declares a fact as introduction rule in the context.
-
-  The special fact called ``@{fact this}'' always refers to the last
-  result, as produced by @{command note}, @{command assume}, @{command
-  have}, or @{command show}.  Since @{command note} occurs
-  frequently together with @{command then} we provide some
-  abbreviations:
+  Simultaneous propositions or facts may be separated by the @{keyword "and"}
+  keyword.
+
+  \<^medskip>
+  The syntax for terms and propositions is inherited from Pure (and the
+  object-logic). A \<open>pattern\<close> is a \<open>term\<close> with schematic variables, to be bound
+  by higher-order matching.
+
+  \<^medskip>
+  Facts may be referenced by name or proposition. For example, the result of
+  ``@{command have}~\<open>a: A \<langle>proof\<rangle>\<close>'' becomes available both as \<open>a\<close> and
+  \isacharbackquoteopen\<open>A\<close>\isacharbackquoteclose. Moreover, fact expressions
+  may involve attributes that modify either the theorem or the background
+  context. For example, the expression ``\<open>a [OF b]\<close>'' refers to the
+  composition of two facts according to the @{inference resolution} inference
+  of \secref{sec:framework-resolution}, while ``\<open>a [intro]\<close>'' declares a fact
+  as introduction rule in the context.
+
+  The special fact called ``@{fact this}'' always refers to the last result,
+  as produced by @{command note}, @{command assume}, @{command have}, or
+  @{command show}. Since @{command note} occurs frequently together with
+  @{command then} we provide some abbreviations:
 
   \<^medskip>
   \begin{tabular}{rcl}
     @{command from}~\<open>a\<close> & \<open>\<equiv>\<close> & @{command note}~\<open>a\<close>~@{command then} \\
     @{command with}~\<open>a\<close> & \<open>\<equiv>\<close> & @{command from}~\<open>a \<AND> this\<close> \\
   \end{tabular}
   \<^medskip>
 
-  The \<open>method\<close> category is essentially a parameter and may be
-  populated later.  Methods use the facts indicated by @{command
-  "then"} or @{command using}, and then operate on the goal state.
-  Some basic methods are predefined: ``@{method "-"}'' leaves the goal
-  unchanged, ``@{method this}'' applies the facts as rules to the
-  goal, ``@{method (Pure) "rule"}'' applies the facts to another rule and the
-  result to the goal (both ``@{method this}'' and ``@{method (Pure) rule}''
-  refer to @{inference resolution} of
-  \secref{sec:framework-resolution}).  The secondary arguments to
-  ``@{method (Pure) rule}'' may be specified explicitly as in ``\<open>(rule
-  a)\<close>'', or picked from the context.  In the latter case, the system
-  first tries rules declared as @{attribute (Pure) elim} or
-  @{attribute (Pure) dest}, followed by those declared as @{attribute
-  (Pure) intro}.
-
-  The default method for @{command proof} is ``@{method standard}''
-  (arguments picked from the context), for @{command qed} it is
-  ``@{method "succeed"}''.  Further abbreviations for terminal proof steps
-  are ``@{command "by"}~\<open>method\<^sub>1 method\<^sub>2\<close>'' for
-  ``@{command proof}~\<open>method\<^sub>1\<close>~@{command qed}~\<open>method\<^sub>2\<close>'', and ``@{command ".."}'' for ``@{command
-  "by"}~@{method standard}, and ``@{command "."}'' for ``@{command
-  "by"}~@{method this}''.  The @{command unfolding} element operates
-  directly on the current facts and goal by applying equalities.
+  The \<open>method\<close> category is essentially a parameter and may be populated later.
+  Methods use the facts indicated by @{command "then"} or @{command using},
+  and then operate on the goal state. Some basic methods are predefined:
+  ``@{method "-"}'' leaves the goal unchanged, ``@{method this}'' applies the
+  facts as rules to the goal, ``@{method (Pure) "rule"}'' applies the facts to
+  another rule and the result to the goal (both ``@{method this}'' and
+  ``@{method (Pure) rule}'' refer to @{inference resolution} of
+  \secref{sec:framework-resolution}). The secondary arguments to ``@{method
+  (Pure) rule}'' may be specified explicitly as in ``\<open>(rule a)\<close>'', or picked
+  from the context. In the latter case, the system first tries rules declared
+  as @{attribute (Pure) elim} or @{attribute (Pure) dest}, followed by those
+  declared as @{attribute (Pure) intro}.
+
+  The default method for @{command proof} is ``@{method standard}'' (arguments
+  picked from the context), for @{command qed} it is ``@{method "succeed"}''.
+  Further abbreviations for terminal proof steps are ``@{command
+  "by"}~\<open>method\<^sub>1 method\<^sub>2\<close>'' for ``@{command proof}~\<open>method\<^sub>1\<close>~@{command
+  qed}~\<open>method\<^sub>2\<close>'', and ``@{command ".."}'' for ``@{command "by"}~@{method
+  standard}, and ``@{command "."}'' for ``@{command "by"}~@{method this}''.
+  The @{command unfolding} element operates directly on the current facts and
+  goal by applying equalities.
 
   \<^medskip>
   Block structure can be indicated explicitly by ``@{command
-  "{"}~\<open>\<dots>\<close>~@{command "}"}'', although the body of a sub-proof
-  already involves implicit nesting.  In any case, @{command next}
-  jumps into the next section of a block, i.e.\ it acts like closing
-  an implicit block scope and opening another one; there is no direct
-  correspondence to subgoals here.
-
-  The remaining elements @{command fix} and @{command assume} build up
-  a local context (see \secref{sec:framework-context}), while
-  @{command show} refines a pending sub-goal by the rule resulting
-  from a nested sub-proof (see \secref{sec:framework-subproof}).
-  Further derived concepts will support calculational reasoning (see
-  \secref{sec:framework-calc}).
+  "{"}~\<open>\<dots>\<close>~@{command "}"}'', although the body of a sub-proof already involves
+  implicit nesting. In any case, @{command next} jumps into the next section
+  of a block, i.e.\ it acts like closing an implicit block scope and opening
+  another one; there is no direct correspondence to subgoals here.
+
+  The remaining elements @{command fix} and @{command assume} build up a local
+  context (see \secref{sec:framework-context}), while @{command show} refines
+  a pending sub-goal by the rule resulting from a nested sub-proof (see
+  \secref{sec:framework-subproof}). Further derived concepts will support
+  calculational reasoning (see \secref{sec:framework-calc}).
 \<close>
 
 
 subsection \<open>Context elements \label{sec:framework-context}\<close>
 
 text \<open>
-  In judgments \<open>\<Gamma> \<turnstile> \<phi>\<close> of the primitive framework, \<open>\<Gamma>\<close>
-  essentially acts like a proof context.  Isar elaborates this idea
-  towards a higher-level notion, with additional information for
-  type-inference, term abbreviations, local facts, hypotheses etc.
-
-  The element @{command fix}~\<open>x :: \<alpha>\<close> declares a local
-  parameter, i.e.\ an arbitrary-but-fixed entity of a given type; in
-  results exported from the context, \<open>x\<close> may become anything.
-  The @{command assume}~\<open>\<guillemotleft>inference\<guillemotright>\<close> element provides a
-  general interface to hypotheses: ``@{command assume}~\<open>\<guillemotleft>inference\<guillemotright> A\<close>'' produces \<open>A \<turnstile> A\<close> locally, while the
-  included inference tells how to discharge \<open>A\<close> from results
-  \<open>A \<turnstile> B\<close> later on.  There is no user-syntax for \<open>\<guillemotleft>inference\<guillemotright>\<close>, i.e.\ it may only occur internally when derived
-  commands are defined in ML.
+  In judgments \<open>\<Gamma> \<turnstile> \<phi>\<close> of the primitive framework, \<open>\<Gamma>\<close> essentially acts like a
+  proof context. Isar elaborates this idea towards a higher-level notion, with
+  additional information for type-inference, term abbreviations, local facts,
+  hypotheses etc.
+
+  The element @{command fix}~\<open>x :: \<alpha>\<close> declares a local parameter, i.e.\ an
+  arbitrary-but-fixed entity of a given type; in results exported from the
+  context, \<open>x\<close> may become anything. The @{command assume}~\<open>\<guillemotleft>inference\<guillemotright>\<close>
+  element provides a general interface to hypotheses: ``@{command
+  assume}~\<open>\<guillemotleft>inference\<guillemotright> A\<close>'' produces \<open>A \<turnstile> A\<close> locally, while the included
+  inference tells how to discharge \<open>A\<close> from results \<open>A \<turnstile> B\<close> later on. There is
+  no user-syntax for \<open>\<guillemotleft>inference\<guillemotright>\<close>, i.e.\ it may only occur internally when
+  derived commands are defined in ML.
 
   At the user-level, the default inference for @{command assume} is
-  @{inference discharge} as given below.  The additional variants
-  @{command presume} and @{command def} are defined as follows:
+  @{inference discharge} as given below. The additional variants @{command
+  presume} and @{command def} are defined as follows:
 
   \<^medskip>
   \begin{tabular}{rcl}
     @{command presume}~\<open>A\<close> & \<open>\<equiv>\<close> & @{command assume}~\<open>\<guillemotleft>weak\<hyphen>discharge\<guillemotright> A\<close> \\
     @{command def}~\<open>x \<equiv> a\<close> & \<open>\<equiv>\<close> & @{command fix}~\<open>x\<close>~@{command assume}~\<open>\<guillemotleft>expansion\<guillemotright> x \<equiv> a\<close> \\

   \[
   \infer[(@{inference_def expansion})]{\<open>\<strut>\<Gamma> - (x \<equiv> a) \<turnstile> B a\<close>}{\<open>\<strut>\<Gamma> \<turnstile> B x\<close>}
   \]
 
   \<^medskip>
-  Note that @{inference discharge} and @{inference
-  "weak\<hyphen>discharge"} differ in the marker for @{prop A}, which is
-  relevant when the result of a @{command fix}-@{command
-  assume}-@{command show} outline is composed with a pending goal,
-  cf.\ \secref{sec:framework-subproof}.
-
-  The most interesting derived context element in Isar is @{command
-  obtain} @{cite \<open>\S5.3\<close> "Wenzel-PhD"}, which supports generalized
-  elimination steps in a purely forward manner.  The @{command obtain}
-  command takes a specification of parameters \<open>\<^vec>x\<close> and
-  assumptions \<open>\<^vec>A\<close> to be added to the context, together
-  with a proof of a case rule stating that this extension is
-  conservative (i.e.\ may be removed from closed results later on):
+  Note that @{inference discharge} and @{inference "weak\<hyphen>discharge"} differ in
+  the marker for @{prop A}, which is relevant when the result of a @{command
+  fix}-@{command assume}-@{command show} outline is composed with a pending
+  goal, cf.\ \secref{sec:framework-subproof}.
+
+  The most interesting derived context element in Isar is @{command obtain}
+  @{cite \<open>\S5.3\<close> "Wenzel-PhD"}, which supports generalized elimination steps
+  in a purely forward manner. The @{command obtain} command takes a
+  specification of parameters \<open>\<^vec>x\<close> and assumptions \<open>\<^vec>A\<close> to be
+  added to the context, together with a proof of a case rule stating that this
+  extension is conservative (i.e.\ may be removed from closed results later
+  on):
 
   \<^medskip>
   \begin{tabular}{l}
   \<open>\<langle>facts\<rangle>\<close>~~@{command obtain}~\<open>\<^vec>x \<WHERE> \<^vec>A \<^vec>x  \<langle>proof\<rangle> \<equiv>\<close> \\[0.5ex]
   \quad @{command have}~\<open>case: \<And>thesis. (\<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis) \<Longrightarrow> thesis\<rangle>\<close> \\

     \<open>result:\<close> &
     \<open>\<Gamma> \<union> \<^vec>A \<^vec>y \<turnstile> B\<close> \\[0.2ex]
     \end{tabular}}
   \]
 
-  Here the name ``\<open>thesis\<close>'' is a specific convention
-  for an arbitrary-but-fixed proposition; in the primitive natural
-  deduction rules shown before we have occasionally used \<open>C\<close>.
-  The whole statement of ``@{command obtain}~\<open>x\<close>~@{keyword
-  "where"}~\<open>A x\<close>'' may be read as a claim that \<open>A x\<close>
-  may be assumed for some arbitrary-but-fixed \<open>x\<close>.  Also note
-  that ``@{command obtain}~\<open>A \<AND> B\<close>'' without parameters
-  is similar to ``@{command have}~\<open>A \<AND> B\<close>'', but the
-  latter involves multiple sub-goals.
-
-  \<^medskip>
-  The subsequent Isar proof texts explain all context
-  elements introduced above using the formal proof language itself.
-  After finishing a local proof within a block, we indicate the
-  exported result via @{command note}.
+  Here the name ``\<open>thesis\<close>'' is a specific convention for an
+  arbitrary-but-fixed proposition; in the primitive natural deduction rules
+  shown before we have occasionally used \<open>C\<close>. The whole statement of
+  ``@{command obtain}~\<open>x\<close>~@{keyword "where"}~\<open>A x\<close>'' may be read as a claim
+  that \<open>A x\<close> may be assumed for some arbitrary-but-fixed \<open>x\<close>. Also note that
+  ``@{command obtain}~\<open>A \<AND> B\<close>'' without parameters is similar to
+  ``@{command have}~\<open>A \<AND> B\<close>'', but the latter involves multiple
+  sub-goals.
+
+  \<^medskip>
+  The subsequent Isar proof texts explain all context elements introduced
+  above using the formal proof language itself. After finishing a local proof
+  within a block, we indicate the exported result via @{command note}.
 \<close>
 
 (*<*)
 theorem True
 proof

 qed
 (*>*)
 
 text \<open>
   \<^bigskip>
-  This illustrates the meaning of Isar context
-  elements without goals getting in between.
+  This illustrates the meaning of Isar context elements without goals getting
+  in between.
 \<close>
 
 
 subsection \<open>Structured statements \label{sec:framework-stmt}\<close>
 

   & \<open>|\<close> & \<open>\<OBTAINS> vars \<AND> \<dots> \<WHERE> name: props \<AND> \<dots>\<close> \\
   & & \quad \<open>\<BBAR> \<dots>\<close> \\
   \end{tabular}
 
   \<^medskip>
-  A simple \<open>statement\<close> consists of named
-  propositions.  The full form admits local context elements followed
-  by the actual conclusions, such as ``@{keyword "fixes"}~\<open>x\<close>~@{keyword "assumes"}~\<open>A x\<close>~@{keyword "shows"}~\<open>B
-  x\<close>''.  The final result emerges as a Pure rule after discharging
-  the context: @{prop "\<And>x. A x \<Longrightarrow> B x"}.
-
-  The @{keyword "obtains"} variant is another abbreviation defined
-  below; unlike @{command obtain} (cf.\
-  \secref{sec:framework-context}) there may be several ``cases''
-  separated by ``\<open>\<BBAR>\<close>'', each consisting of several
-  parameters (\<open>vars\<close>) and several premises (\<open>props\<close>).
-  This specifies multi-branch elimination rules.
+  A simple \<open>statement\<close> consists of named propositions. The full form admits
+  local context elements followed by the actual conclusions, such as
+  ``@{keyword "fixes"}~\<open>x\<close>~@{keyword "assumes"}~\<open>A x\<close>~@{keyword "shows"}~\<open>B
+  x\<close>''. The final result emerges as a Pure rule after discharging the context:
+  @{prop "\<And>x. A x \<Longrightarrow> B x"}.
+
+  The @{keyword "obtains"} variant is another abbreviation defined below;
+  unlike @{command obtain} (cf.\ \secref{sec:framework-context}) there may be
+  several ``cases'' separated by ``\<open>\<BBAR>\<close>'', each consisting of several
+  parameters (\<open>vars\<close>) and several premises (\<open>props\<close>). This specifies
+  multi-branch elimination rules.
 
   \<^medskip>
   \begin{tabular}{l}
   \<open>\<OBTAINS> \<^vec>x \<WHERE> \<^vec>A \<^vec>x   \<BBAR>   \<dots>   \<equiv>\<close> \\[0.5ex]
   \quad \<open>\<FIXES> thesis\<close> \\

   \quad \<open>\<SHOWS> thesis\<close> \\
   \end{tabular}
   \<^medskip>
 
   Presenting structured statements in such an ``open'' format usually
-  simplifies the subsequent proof, because the outer structure of the
-  problem is already laid out directly.  E.g.\ consider the following
-  canonical patterns for \<open>\<SHOWS>\<close> and \<open>\<OBTAINS>\<close>,
-  respectively:
+  simplifies the subsequent proof, because the outer structure of the problem
+  is already laid out directly. E.g.\ consider the following canonical
+  patterns for \<open>\<SHOWS>\<close> and \<open>\<OBTAINS>\<close>, respectively:
 \<close>
 
 text_raw \<open>\begin{minipage}{0.5\textwidth}\<close>
 
 theorem

 
 text_raw \<open>\end{minipage}\<close>
 
 text \<open>
   \<^medskip>
-  Here local facts \isacharbackquoteopen\<open>A
-  x\<close>\isacharbackquoteclose\ and \isacharbackquoteopen\<open>B
-  y\<close>\isacharbackquoteclose\ are referenced immediately; there is no
-  need to decompose the logical rule structure again.  In the second
-  proof the final ``@{command then}~@{command show}~\<open>thesis\<close>~@{command ".."}''  involves the local rule case \<open>\<And>x
-  y. A x \<Longrightarrow> B y \<Longrightarrow> thesis\<close> for the particular instance of terms \<open>a\<close> and \<open>b\<close> produced in the body.
-\<close>
+  Here local facts \isacharbackquoteopen\<open>A x\<close>\isacharbackquoteclose\ and
+  \isacharbackquoteopen\<open>B y\<close>\isacharbackquoteclose\ are referenced
+  immediately; there is no need to decompose the logical rule structure again.
+  In the second proof the final ``@{command then}~@{command
+  show}~\<open>thesis\<close>~@{command ".."}'' involves the local rule case \<open>\<And>x y. A x \<Longrightarrow> B
+  y \<Longrightarrow> thesis\<close> for the particular instance of terms \<open>a\<close> and \<open>b\<close> produced in the
+  body. \<close>
 
 
 subsection \<open>Structured proof refinement \label{sec:framework-subproof}\<close>
 
 text \<open>
-  By breaking up the grammar for the Isar proof language, we may
-  understand a proof text as a linear sequence of individual proof
-  commands.  These are interpreted as transitions of the Isar virtual
-  machine (Isar/VM), which operates on a block-structured
-  configuration in single steps.  This allows users to write proof
-  texts in an incremental manner, and inspect intermediate
-  configurations for debugging.
-
-  The basic idea is analogous to evaluating algebraic expressions on a
-  stack machine: \<open>(a + b) \<cdot> c\<close> then corresponds to a sequence
-  of single transitions for each symbol \<open>(, a, +, b, ), \<cdot>, c\<close>.
-  In Isar the algebraic values are facts or goals, and the operations
-  are inferences.
-
-  \<^medskip>
-  The Isar/VM state maintains a stack of nodes, each node
-  contains the local proof context, the linguistic mode, and a pending
-  goal (optional).  The mode determines the type of transition that
-  may be performed next, it essentially alternates between forward and
-  backward reasoning, with an intermediate stage for chained facts
-  (see \figref{fig:isar-vm}).
+  By breaking up the grammar for the Isar proof language, we may understand a
+  proof text as a linear sequence of individual proof commands. These are
+  interpreted as transitions of the Isar virtual machine (Isar/VM), which
+  operates on a block-structured configuration in single steps. This allows
+  users to write proof texts in an incremental manner, and inspect
+  intermediate configurations for debugging.
+
+  The basic idea is analogous to evaluating algebraic expressions on a stack
+  machine: \<open>(a + b) \<cdot> c\<close> then corresponds to a sequence of single transitions
+  for each symbol \<open>(, a, +, b, ), \<cdot>, c\<close>. In Isar the algebraic values are
+  facts or goals, and the operations are inferences.
+
+  \<^medskip>
+  The Isar/VM state maintains a stack of nodes, each node contains the local
+  proof context, the linguistic mode, and a pending goal (optional). The mode
+  determines the type of transition that may be performed next, it essentially
+  alternates between forward and backward reasoning, with an intermediate
+  stage for chained facts (see \figref{fig:isar-vm}).
 
   \begin{figure}[htb]
   \begin{center}
   \includegraphics[width=0.8\textwidth]{isar-vm}
   \end{center}
   \caption{Isar/VM modes}\label{fig:isar-vm}
   \end{figure}
 
-  For example, in \<open>state\<close> mode Isar acts like a mathematical
-  scratch-pad, accepting declarations like @{command fix}, @{command
-  assume}, and claims like @{command have}, @{command show}.  A goal
-  statement changes the mode to \<open>prove\<close>, which means that we
-  may now refine the problem via @{command unfolding} or @{command
-  proof}.  Then we are again in \<open>state\<close> mode of a proof body,
-  which may issue @{command show} statements to solve pending
-  sub-goals.  A concluding @{command qed} will return to the original
-  \<open>state\<close> mode one level upwards.  The subsequent Isar/VM
-  trace indicates block structure, linguistic mode, goal state, and
-  inferences:
+  For example, in \<open>state\<close> mode Isar acts like a mathematical scratch-pad,
+  accepting declarations like @{command fix}, @{command assume}, and claims
+  like @{command have}, @{command show}. A goal statement changes the mode to
+  \<open>prove\<close>, which means that we may now refine the problem via @{command
+  unfolding} or @{command proof}. Then we are again in \<open>state\<close> mode of a proof
+  body, which may issue @{command show} statements to solve pending sub-goals.
+  A concluding @{command qed} will return to the original \<open>state\<close> mode one
+  level upwards. The subsequent Isar/VM trace indicates block structure,
+  linguistic mode, goal state, and inferences:
 \<close>
 
 text_raw \<open>\begingroup\footnotesize\<close>
 (*<*)notepad begin
 (*>*)

 (*>*)
 text_raw \<open>\endgroup\<close>
 
 text \<open>
   Here the @{inference refinement} inference from
-  \secref{sec:framework-resolution} mediates composition of Isar
-  sub-proofs nicely.  Observe that this principle incorporates some
-  degree of freedom in proof composition.  In particular, the proof
-  body allows parameters and assumptions to be re-ordered, or commuted
-  according to Hereditary Harrop Form.  Moreover, context elements
-  that are not used in a sub-proof may be omitted altogether.  For
-  example:
+  \secref{sec:framework-resolution} mediates composition of Isar sub-proofs
+  nicely. Observe that this principle incorporates some degree of freedom in
+  proof composition. In particular, the proof body allows parameters and
+  assumptions to be re-ordered, or commuted according to Hereditary Harrop
+  Form. Moreover, context elements that are not used in a sub-proof may be
+  omitted altogether. For example:
 \<close>
 
 text_raw \<open>\begin{minipage}{0.5\textwidth}\<close>
 
 (*<*)

 
 text_raw \<open>\end{minipage}\<close>
 
 text \<open>
   \<^medskip>
-  Such ``peephole optimizations'' of Isar texts are
-  practically important to improve readability, by rearranging
-  contexts elements according to the natural flow of reasoning in the
-  body, while still observing the overall scoping rules.
-
-  \<^medskip>
-  This illustrates the basic idea of structured proof
-  processing in Isar.  The main mechanisms are based on natural
-  deduction rule composition within the Pure framework.  In
-  particular, there are no direct operations on goal states within the
-  proof body.  Moreover, there is no hidden automated reasoning
+  Such ``peephole optimizations'' of Isar texts are practically important to
+  improve readability, by rearranging contexts elements according to the
+  natural flow of reasoning in the body, while still observing the overall
+  scoping rules.
+
+  \<^medskip>
+  This illustrates the basic idea of structured proof processing in Isar. The
+  main mechanisms are based on natural deduction rule composition within the
+  Pure framework. In particular, there are no direct operations on goal states
+  within the proof body. Moreover, there is no hidden automated reasoning
   involved, just plain unification.
 \<close>
 
 
 subsection \<open>Calculational reasoning \label{sec:framework-calc}\<close>
 
 text \<open>
   The existing Isar infrastructure is sufficiently flexible to support
-  calculational reasoning (chains of transitivity steps) as derived
-  concept.  The generic proof elements introduced below depend on
-  rules declared as @{attribute trans} in the context.  It is left to
-  the object-logic to provide a suitable rule collection for mixed
-  relations of \<open>=\<close>, \<open><\<close>, \<open>\<le>\<close>, \<open>\<subset>\<close>,
-  \<open>\<subseteq>\<close> etc.  Due to the flexibility of rule composition
-  (\secref{sec:framework-resolution}), substitution of equals by
-  equals is covered as well, even substitution of inequalities
-  involving monotonicity conditions; see also @{cite \<open>\S6\<close> "Wenzel-PhD"}
-  and @{cite "Bauer-Wenzel:2001"}.
-
-  The generic calculational mechanism is based on the observation that
-  rules such as \<open>trans:\<close>~@{prop "x = y \<Longrightarrow> y = z \<Longrightarrow> x = z"}
-  proceed from the premises towards the conclusion in a deterministic
-  fashion.  Thus we may reason in forward mode, feeding intermediate
-  results into rules selected from the context.  The course of
-  reasoning is organized by maintaining a secondary fact called
-  ``@{fact calculation}'', apart from the primary ``@{fact this}''
-  already provided by the Isar primitives.  In the definitions below,
+  calculational reasoning (chains of transitivity steps) as derived concept.
+  The generic proof elements introduced below depend on rules declared as
+  @{attribute trans} in the context. It is left to the object-logic to provide
+  a suitable rule collection for mixed relations of \<open>=\<close>, \<open><\<close>, \<open>\<le>\<close>, \<open>\<subset>\<close>, \<open>\<subseteq>\<close>
+  etc. Due to the flexibility of rule composition
+  (\secref{sec:framework-resolution}), substitution of equals by equals is
+  covered as well, even substitution of inequalities involving monotonicity
+  conditions; see also @{cite \<open>\S6\<close> "Wenzel-PhD"} and @{cite
+  "Bauer-Wenzel:2001"}.
+
+  The generic calculational mechanism is based on the observation that rules
+  such as \<open>trans:\<close>~@{prop "x = y \<Longrightarrow> y = z \<Longrightarrow> x = z"} proceed from the premises
+  towards the conclusion in a deterministic fashion. Thus we may reason in
+  forward mode, feeding intermediate results into rules selected from the
+  context. The course of reasoning is organized by maintaining a secondary
+  fact called ``@{fact calculation}'', apart from the primary ``@{fact this}''
+  already provided by the Isar primitives. In the definitions below,
   @{attribute OF} refers to @{inference resolution}
-  (\secref{sec:framework-resolution}) with multiple rule arguments,
-  and \<open>trans\<close> represents to a suitable rule from the context:
+  (\secref{sec:framework-resolution}) with multiple rule arguments, and
+  \<open>trans\<close> represents to a suitable rule from the context:
 
   \begin{matharray}{rcl}
     @{command "also"}\<open>\<^sub>0\<close> & \equiv & @{command "note"}~\<open>calculation = this\<close> \\
     @{command "also"}\<open>\<^sub>n\<^sub>+\<^sub>1\<close> & \equiv & @{command "note"}~\<open>calculation = trans [OF calculation this]\<close> \\[0.5ex]
     @{command "finally"} & \equiv & @{command "also"}~@{command "from"}~\<open>calculation\<close> \\
   \end{matharray}
 
-  The start of a calculation is determined implicitly in the
-  text: here @{command also} sets @{fact calculation} to the current
-  result; any subsequent occurrence will update @{fact calculation} by
-  combination with the next result and a transitivity rule.  The
-  calculational sequence is concluded via @{command finally}, where
-  the final result is exposed for use in a concluding claim.
-
-  Here is a canonical proof pattern, using @{command have} to
-  establish the intermediate results:
+  The start of a calculation is determined implicitly in the text: here
+  @{command also} sets @{fact calculation} to the current result; any
+  subsequent occurrence will update @{fact calculation} by combination with
+  the next result and a transitivity rule. The calculational sequence is
+  concluded via @{command finally}, where the final result is exposed for use
+  in a concluding claim.
+
+  Here is a canonical proof pattern, using @{command have} to establish the
+  intermediate results:
 \<close>
 
 (*<*)
 notepad
 begin

 (*<*)
 end
 (*>*)
 
 text \<open>
-  The term ``\<open>\<dots>\<close>'' above is a special abbreviation
-  provided by the Isabelle/Isar syntax layer: it statically refers to
-  the right-hand side argument of the previous statement given in the
-  text.  Thus it happens to coincide with relevant sub-expressions in
-  the calculational chain, but the exact correspondence is dependent
-  on the transitivity rules being involved.
-
-  \<^medskip>
-  Symmetry rules such as @{prop "x = y \<Longrightarrow> y = x"} are like
-  transitivities with only one premise.  Isar maintains a separate
-  rule collection declared via the @{attribute sym} attribute, to be
-  used in fact expressions ``\<open>a [symmetric]\<close>'', or single-step
-  proofs ``@{command assume}~\<open>x = y\<close>~@{command then}~@{command
-  have}~\<open>y = x\<close>~@{command ".."}''.
+  The term ``\<open>\<dots>\<close>'' above is a special abbreviation provided by the
+  Isabelle/Isar syntax layer: it statically refers to the right-hand side
+  argument of the previous statement given in the text. Thus it happens to
+  coincide with relevant sub-expressions in the calculational chain, but the
+  exact correspondence is dependent on the transitivity rules being involved.
+
+  \<^medskip>
+  Symmetry rules such as @{prop "x = y \<Longrightarrow> y = x"} are like transitivities with
+  only one premise. Isar maintains a separate rule collection declared via the
+  @{attribute sym} attribute, to be used in fact expressions ``\<open>a
+  [symmetric]\<close>'', or single-step proofs ``@{command assume}~\<open>x = y\<close>~@{command
+  then}~@{command have}~\<open>y = x\<close>~@{command ".."}''.
 \<close>
 
 end