wenzelm@29716: theory Framework
wenzelm@42651: imports Base Main
wenzelm@29716: begin
wenzelm@29716: 
wenzelm@58618: chapter \<open>The Isabelle/Isar Framework \label{ch:isar-framework}\<close>
wenzelm@29716: 
wenzelm@58618: text \<open>
wenzelm@58552:   Isabelle/Isar @{cite "Wenzel:1999:TPHOL" and "Wenzel-PhD" and
wenzelm@58552:   "Nipkow-TYPES02" and "Wenzel-Paulson:2006" and "Wenzel:2006:Festschrift"}
wenzelm@29716:   is intended as a generic framework for developing formal
wenzelm@29716:   mathematical documents with full proof checking.  Definitions and
wenzelm@29735:   proofs are organized as theories.  An assembly of theory sources may
wenzelm@29716:   be presented as a printed document; see also
wenzelm@29716:   \chref{ch:document-prep}.
wenzelm@29716: 
wenzelm@29716:   The main objective of Isar is the design of a human-readable
wenzelm@29716:   structured proof language, which is called the ``primary proof
wenzelm@29716:   format'' in Isar terminology.  Such a primary proof language is
wenzelm@29716:   somewhere in the middle between the extremes of primitive proof
wenzelm@29716:   objects and actual natural language.  In this respect, Isar is a bit
wenzelm@58552:   more formalistic than Mizar @{cite "Trybulec:1993:MizarFeatures" and
wenzelm@58552:   "Rudnicki:1992:MizarOverview" and "Wiedijk:1999:Mizar"},
wenzelm@29716:   using logical symbols for certain reasoning schemes where Mizar
wenzelm@58552:   would prefer English words; see @{cite "Wenzel-Wiedijk:2002"} for
wenzelm@29716:   further comparisons of these systems.
wenzelm@29716: 
wenzelm@29716:   So Isar challenges the traditional way of recording informal proofs
wenzelm@29716:   in mathematical prose, as well as the common tendency to see fully
wenzelm@29716:   formal proofs directly as objects of some logical calculus (e.g.\
wenzelm@29716:   @{text "\<lambda>"}-terms in a version of type theory).  In fact, Isar is
wenzelm@29716:   better understood as an interpreter of a simple block-structured
wenzelm@29735:   language for describing the data flow of local facts and goals,
wenzelm@29716:   interspersed with occasional invocations of proof methods.
wenzelm@29716:   Everything is reduced to logical inferences internally, but these
wenzelm@29716:   steps are somewhat marginal compared to the overall bookkeeping of
wenzelm@29716:   the interpretation process.  Thanks to careful design of the syntax
wenzelm@29716:   and semantics of Isar language elements, a formal record of Isar
wenzelm@29716:   instructions may later appear as an intelligible text to the
wenzelm@29716:   attentive reader.
wenzelm@29716: 
wenzelm@29716:   The Isar proof language has emerged from careful analysis of some
wenzelm@29716:   inherent virtues of the existing logical framework of Isabelle/Pure
wenzelm@58552:   @{cite "paulson-found" and "paulson700"}, notably composition of higher-order
wenzelm@29716:   natural deduction rules, which is a generalization of Gentzen's
wenzelm@58552:   original calculus @{cite "Gentzen:1935"}.  The approach of generic
wenzelm@29716:   inference systems in Pure is continued by Isar towards actual proof
wenzelm@29716:   texts.
wenzelm@29716: 
wenzelm@29716:   Concrete applications require another intermediate layer: an
wenzelm@58552:   object-logic.  Isabelle/HOL @{cite "isa-tutorial"} (simply-typed
wenzelm@29716:   set-theory) is being used most of the time; Isabelle/ZF
wenzelm@58552:   @{cite "isabelle-ZF"} is less extensively developed, although it would
wenzelm@29716:   probably fit better for classical mathematics.
wenzelm@29721: 
wenzelm@29735:   \medskip In order to illustrate natural deduction in Isar, we shall
wenzelm@29735:   refer to the background theory and library of Isabelle/HOL.  This
wenzelm@29735:   includes common notions of predicate logic, naive set-theory etc.\
wenzelm@29735:   using fairly standard mathematical notation.  From the perspective
wenzelm@29735:   of generic natural deduction there is nothing special about the
wenzelm@29735:   logical connectives of HOL (@{text "\<and>"}, @{text "\<or>"}, @{text "\<forall>"},
wenzelm@29735:   @{text "\<exists>"}, etc.), only the resulting reasoning principles are
wenzelm@29735:   relevant to the user.  There are similar rules available for
wenzelm@29735:   set-theory operators (@{text "\<inter>"}, @{text "\<union>"}, @{text "\<Inter>"}, @{text
wenzelm@29735:   "\<Union>"}, etc.), or any other theory developed in the library (lattice
wenzelm@29735:   theory, topology etc.).
wenzelm@29721: 
wenzelm@29721:   Subsequently we briefly review fragments of Isar proof texts
wenzelm@29735:   corresponding directly to such general deduction schemes.  The
wenzelm@29735:   examples shall refer to set-theory, to minimize the danger of
wenzelm@29721:   understanding connectives of predicate logic as something special.
wenzelm@29721: 
wenzelm@29721:   \medskip The following deduction performs @{text "\<inter>"}-introduction,
wenzelm@29721:   working forwards from assumptions towards the conclusion.  We give
wenzelm@29721:   both the Isar text, and depict the primitive rule involved, as
wenzelm@29735:   determined by unification of the problem against rules that are
wenzelm@29735:   declared in the library context.
wenzelm@58618: \<close>
wenzelm@29721: 
wenzelm@58618: text_raw \<open>\medskip\begin{minipage}{0.6\textwidth}\<close>
wenzelm@29721: 
wenzelm@29721: (*<*)
wenzelm@40964: notepad
wenzelm@40964: begin
wenzelm@29721: (*>*)
wenzelm@29721:     assume "x \<in> A" and "x \<in> B"
wenzelm@29721:     then have "x \<in> A \<inter> B" ..
wenzelm@29721: (*<*)
wenzelm@40964: end
wenzelm@29721: (*>*)
wenzelm@29721: 
wenzelm@58618: text_raw \<open>\end{minipage}\begin{minipage}{0.4\textwidth}\<close>
wenzelm@29721: 
wenzelm@58618: text \<open>
wenzelm@29721:   \infer{@{prop "x \<in> A \<inter> B"}}{@{prop "x \<in> A"} & @{prop "x \<in> B"}}
wenzelm@58618: \<close>
wenzelm@29721: 
wenzelm@58618: text_raw \<open>\end{minipage}\<close>
wenzelm@29721: 
wenzelm@58618: text \<open>
wenzelm@29737:   \medskip\noindent Note that @{command assume} augments the proof
wenzelm@29737:   context, @{command then} indicates that the current fact shall be
wenzelm@29737:   used in the next step, and @{command have} states an intermediate
wenzelm@29735:   goal.  The two dots ``@{command ".."}'' refer to a complete proof of
wenzelm@29735:   this claim, using the indicated facts and a canonical rule from the
wenzelm@29721:   context.  We could have been more explicit here by spelling out the
wenzelm@29721:   final proof step via the @{command "by"} command:
wenzelm@58618: \<close>
wenzelm@29721: 
wenzelm@29721: (*<*)
wenzelm@40964: notepad
wenzelm@40964: begin
wenzelm@29721: (*>*)
wenzelm@29721:     assume "x \<in> A" and "x \<in> B"
wenzelm@29721:     then have "x \<in> A \<inter> B" by (rule IntI)
wenzelm@29721: (*<*)
wenzelm@40964: end
wenzelm@29721: (*>*)
wenzelm@29721: 
wenzelm@58618: text \<open>
wenzelm@29721:   \noindent The format of the @{text "\<inter>"}-introduction rule represents
wenzelm@29721:   the most basic inference, which proceeds from given premises to a
wenzelm@29735:   conclusion, without any nested proof context involved.
wenzelm@29721: 
wenzelm@29735:   The next example performs backwards introduction on @{term "\<Inter>\<A>"},
wenzelm@29735:   the intersection of all sets within a given set.  This requires a
wenzelm@29735:   nested proof of set membership within a local context, where @{term
wenzelm@29735:   A} is an arbitrary-but-fixed member of the collection:
wenzelm@58618: \<close>
wenzelm@29721: 
wenzelm@58618: text_raw \<open>\medskip\begin{minipage}{0.6\textwidth}\<close>
wenzelm@29721: 
wenzelm@29721: (*<*)
wenzelm@40964: notepad
wenzelm@40964: begin
wenzelm@29721: (*>*)
wenzelm@29721:     have "x \<in> \<Inter>\<A>"
wenzelm@29721:     proof
wenzelm@29721:       fix A
wenzelm@29721:       assume "A \<in> \<A>"
wenzelm@29733:       show "x \<in> A" sorry %noproof
wenzelm@29721:     qed
wenzelm@29721: (*<*)
wenzelm@40964: end
wenzelm@29721: (*>*)
wenzelm@29721: 
wenzelm@58618: text_raw \<open>\end{minipage}\begin{minipage}{0.4\textwidth}\<close>
wenzelm@29721: 
wenzelm@58618: text \<open>
wenzelm@29721:   \infer{@{prop "x \<in> \<Inter>\<A>"}}{\infer*{@{prop "x \<in> A"}}{@{text "[A][A \<in> \<A>]"}}}
wenzelm@58618: \<close>
wenzelm@29721: 
wenzelm@58618: text_raw \<open>\end{minipage}\<close>
wenzelm@29721: 
wenzelm@58618: text \<open>
wenzelm@29721:   \medskip\noindent This Isar reasoning pattern again refers to the
wenzelm@29721:   primitive rule depicted above.  The system determines it in the
wenzelm@56594:   ``@{command proof}'' step, which could have been spelled out more
wenzelm@29737:   explicitly as ``@{command proof}~@{text "(rule InterI)"}''.  Note
wenzelm@29735:   that the rule involves both a local parameter @{term "A"} and an
wenzelm@29729:   assumption @{prop "A \<in> \<A>"} in the nested reasoning.  This kind of
wenzelm@29729:   compound rule typically demands a genuine sub-proof in Isar, working
wenzelm@29729:   backwards rather than forwards as seen before.  In the proof body we
wenzelm@29737:   encounter the @{command fix}-@{command assume}-@{command show}
wenzelm@29737:   outline of nested sub-proofs that is typical for Isar.  The final
wenzelm@29737:   @{command show} is like @{command have} followed by an additional
wenzelm@29737:   refinement of the enclosing claim, using the rule derived from the
wenzelm@29737:   proof body.
wenzelm@29721: 
wenzelm@29721:   \medskip The next example involves @{term "\<Union>\<A>"}, which can be
wenzelm@29721:   characterized as the set of all @{term "x"} such that @{prop "\<exists>A. x
wenzelm@29721:   \<in> A \<and> A \<in> \<A>"}.  The elimination rule for @{prop "x \<in> \<Union>\<A>"} does
wenzelm@29721:   not mention @{text "\<exists>"} and @{text "\<and>"} at all, but admits to obtain
wenzelm@29721:   directly a local @{term "A"} such that @{prop "x \<in> A"} and @{prop "A
wenzelm@29721:   \<in> \<A>"} hold.  This corresponds to the following Isar proof and
wenzelm@29721:   inference rule, respectively:
wenzelm@58618: \<close>
wenzelm@29721: 
wenzelm@58618: text_raw \<open>\medskip\begin{minipage}{0.6\textwidth}\<close>
wenzelm@29721: 
wenzelm@29721: (*<*)
wenzelm@40964: notepad
wenzelm@40964: begin
wenzelm@29721: (*>*)
wenzelm@29721:     assume "x \<in> \<Union>\<A>"
wenzelm@29721:     then have C
wenzelm@29721:     proof
wenzelm@29721:       fix A
wenzelm@29721:       assume "x \<in> A" and "A \<in> \<A>"
wenzelm@29733:       show C sorry %noproof
wenzelm@29721:     qed
wenzelm@29721: (*<*)
wenzelm@40964: end
wenzelm@29721: (*>*)
wenzelm@29721: 
wenzelm@58618: text_raw \<open>\end{minipage}\begin{minipage}{0.4\textwidth}\<close>
wenzelm@29721: 
wenzelm@58618: text \<open>
wenzelm@29721:   \infer{@{prop "C"}}{@{prop "x \<in> \<Union>\<A>"} & \infer*{@{prop "C"}~}{@{text "[A][x \<in> A, A \<in> \<A>]"}}}
wenzelm@58618: \<close>
wenzelm@29721: 
wenzelm@58618: text_raw \<open>\end{minipage}\<close>
wenzelm@29721: 
wenzelm@58618: text \<open>
wenzelm@29721:   \medskip\noindent Although the Isar proof follows the natural
wenzelm@29721:   deduction rule closely, the text reads not as natural as
wenzelm@29721:   anticipated.  There is a double occurrence of an arbitrary
wenzelm@29721:   conclusion @{prop "C"}, which represents the final result, but is
wenzelm@29721:   irrelevant for now.  This issue arises for any elimination rule
wenzelm@29721:   involving local parameters.  Isar provides the derived language
wenzelm@29737:   element @{command obtain}, which is able to perform the same
wenzelm@29721:   elimination proof more conveniently:
wenzelm@58618: \<close>
wenzelm@29721: 
wenzelm@29721: (*<*)
wenzelm@40964: notepad
wenzelm@40964: begin
wenzelm@29721: (*>*)
wenzelm@29721:     assume "x \<in> \<Union>\<A>"
wenzelm@29721:     then obtain A where "x \<in> A" and "A \<in> \<A>" ..
wenzelm@29721: (*<*)
wenzelm@40964: end
wenzelm@29721: (*>*)
wenzelm@29721: 
wenzelm@58618: text \<open>
wenzelm@29721:   \noindent Here we avoid to mention the final conclusion @{prop "C"}
wenzelm@29721:   and return to plain forward reasoning.  The rule involved in the
wenzelm@29721:   ``@{command ".."}'' proof is the same as before.
wenzelm@58618: \<close>
wenzelm@29716: 
wenzelm@29729: 
wenzelm@58618: section \<open>The Pure framework \label{sec:framework-pure}\<close>
wenzelm@29729: 
wenzelm@58618: text \<open>
wenzelm@58552:   The Pure logic @{cite "paulson-found" and "paulson700"} is an intuitionistic
wenzelm@58552:   fragment of higher-order logic @{cite "church40"}.  In type-theoretic
wenzelm@29729:   parlance, there are three levels of @{text "\<lambda>"}-calculus with
wenzelm@29735:   corresponding arrows @{text "\<Rightarrow>"}/@{text "\<And>"}/@{text "\<Longrightarrow>"}:
wenzelm@29735: 
wenzelm@29735:   \medskip
wenzelm@29735:   \begin{tabular}{ll}
wenzelm@29735:   @{text "\<alpha> \<Rightarrow> \<beta>"} & syntactic function space (terms depending on terms) \\
wenzelm@29735:   @{text "\<And>x. B(x)"} & universal quantification (proofs depending on terms) \\
wenzelm@29735:   @{text "A \<Longrightarrow> B"} & implication (proofs depending on proofs) \\
wenzelm@29735:   \end{tabular}
wenzelm@29735:   \medskip
wenzelm@29729: 
wenzelm@29735:   \noindent Here only the types of syntactic terms, and the
wenzelm@29735:   propositions of proof terms have been shown.  The @{text
wenzelm@29735:   "\<lambda>"}-structure of proofs can be recorded as an optional feature of
wenzelm@58552:   the Pure inference kernel @{cite "Berghofer-Nipkow:2000:TPHOL"}, but
wenzelm@29735:   the formal system can never depend on them due to \emph{proof
wenzelm@29735:   irrelevance}.
wenzelm@29735: 
wenzelm@29735:   On top of this most primitive layer of proofs, Pure implements a
wenzelm@29735:   generic calculus for nested natural deduction rules, similar to
wenzelm@58552:   @{cite "Schroeder-Heister:1984"}.  Here object-logic inferences are
wenzelm@29735:   internalized as formulae over @{text "\<And>"} and @{text "\<Longrightarrow>"}.
wenzelm@29735:   Combining such rule statements may involve higher-order unification
wenzelm@58552:   @{cite "paulson-natural"}.
wenzelm@58618: \<close>
wenzelm@29729: 
wenzelm@29729: 
wenzelm@58618: subsection \<open>Primitive inferences\<close>
wenzelm@29729: 
wenzelm@58618: text \<open>
wenzelm@29729:   Term syntax provides explicit notation for abstraction @{text "\<lambda>x ::
wenzelm@29729:   \<alpha>. b(x)"} and application @{text "b a"}, while types are usually
wenzelm@29729:   implicit thanks to type-inference; terms of type @{text "prop"} are
wenzelm@29729:   called propositions.  Logical statements are composed via @{text "\<And>x
wenzelm@29729:   :: \<alpha>. B(x)"} and @{text "A \<Longrightarrow> B"}.  Primitive reasoning operates on
wenzelm@29729:   judgments of the form @{text "\<Gamma> \<turnstile> \<phi>"}, with standard introduction
wenzelm@29729:   and elimination rules for @{text "\<And>"} and @{text "\<Longrightarrow>"} that refer to
wenzelm@53015:   fixed parameters @{text "x\<^sub>1, \<dots>, x\<^sub>m"} and hypotheses
wenzelm@53015:   @{text "A\<^sub>1, \<dots>, A\<^sub>n"} from the context @{text "\<Gamma>"};
wenzelm@29729:   the corresponding proof terms are left implicit.  The subsequent
wenzelm@29729:   inference rules define @{text "\<Gamma> \<turnstile> \<phi>"} inductively, relative to a
wenzelm@29729:   collection of axioms:
wenzelm@29729: 
wenzelm@29729:   \[
wenzelm@29729:   \infer{@{text "\<turnstile> A"}}{(@{text "A"} \text{~axiom})}
wenzelm@29729:   \qquad
wenzelm@29729:   \infer{@{text "A \<turnstile> A"}}{}
wenzelm@29729:   \]
wenzelm@29729: 
wenzelm@29729:   \[
wenzelm@29729:   \infer{@{text "\<Gamma> \<turnstile> \<And>x. B(x)"}}{@{text "\<Gamma> \<turnstile> B(x)"} & @{text "x \<notin> \<Gamma>"}}
wenzelm@29729:   \qquad
wenzelm@29729:   \infer{@{text "\<Gamma> \<turnstile> B(a)"}}{@{text "\<Gamma> \<turnstile> \<And>x. B(x)"}}
wenzelm@29729:   \]
wenzelm@29729: 
wenzelm@29729:   \[
wenzelm@29729:   \infer{@{text "\<Gamma> - A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}
wenzelm@29729:   \qquad
wenzelm@29729:   \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"}}
wenzelm@29729:   \]
wenzelm@29729: 
wenzelm@29729:   Furthermore, Pure provides a built-in equality @{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow>
wenzelm@29729:   prop"} with axioms for reflexivity, substitution, extensionality,
wenzelm@29729:   and @{text "\<alpha>\<beta>\<eta>"}-conversion on @{text "\<lambda>"}-terms.
wenzelm@29729: 
wenzelm@29729:   \medskip An object-logic introduces another layer on top of Pure,
wenzelm@29729:   e.g.\ with types @{text "i"} for individuals and @{text "o"} for
wenzelm@29729:   propositions, term constants @{text "Trueprop :: o \<Rightarrow> prop"} as
wenzelm@29729:   (implicit) derivability judgment and connectives like @{text "\<and> :: o
wenzelm@29729:   \<Rightarrow> o \<Rightarrow> o"} or @{text "\<forall> :: (i \<Rightarrow> o) \<Rightarrow> o"}, and axioms for object-level
wenzelm@29729:   rules such as @{text "conjI: A \<Longrightarrow> B \<Longrightarrow> A \<and> B"} or @{text "allI: (\<And>x. B
wenzelm@29729:   x) \<Longrightarrow> \<forall>x. B x"}.  Derived object rules are represented as theorems of
wenzelm@29729:   Pure.  After the initial object-logic setup, further axiomatizations
wenzelm@29729:   are usually avoided; plain definitions and derived principles are
wenzelm@29729:   used exclusively.
wenzelm@58618: \<close>
wenzelm@29729: 
wenzelm@29729: 
wenzelm@58618: subsection \<open>Reasoning with rules \label{sec:framework-resolution}\<close>
wenzelm@29729: 
wenzelm@58618: text \<open>
wenzelm@29729:   Primitive inferences mostly serve foundational purposes.  The main
wenzelm@29729:   reasoning mechanisms of Pure operate on nested natural deduction
wenzelm@29729:   rules expressed as formulae, using @{text "\<And>"} to bind local
wenzelm@29729:   parameters and @{text "\<Longrightarrow>"} to express entailment.  Multiple
wenzelm@29729:   parameters and premises are represented by repeating these
wenzelm@29735:   connectives in a right-associative manner.
wenzelm@29729: 
wenzelm@29729:   Since @{text "\<And>"} and @{text "\<Longrightarrow>"} commute thanks to the theorem
wenzelm@29729:   @{prop "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}, we may assume w.l.o.g.\
wenzelm@29729:   that rule statements always observe the normal form where
wenzelm@29729:   quantifiers are pulled in front of implications at each level of
wenzelm@29729:   nesting.  This means that any Pure proposition may be presented as a
wenzelm@58552:   \emph{Hereditary Harrop Formula} @{cite "Miller:1991"} which is of the
wenzelm@53015:   form @{text "\<And>x\<^sub>1 \<dots> x\<^sub>m. H\<^sub>1 \<Longrightarrow> \<dots> H\<^sub>n \<Longrightarrow>
wenzelm@29735:   A"} for @{text "m, n \<ge> 0"}, and @{text "A"} atomic, and @{text
wenzelm@53015:   "H\<^sub>1, \<dots>, H\<^sub>n"} being recursively of the same format.
wenzelm@29729:   Following the convention that outermost quantifiers are implicit,
wenzelm@53015:   Horn clauses @{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> A"} are a special
wenzelm@29729:   case of this.
wenzelm@29729: 
wenzelm@29735:   For example, @{text "\<inter>"}-introduction rule encountered before is
wenzelm@29735:   represented as a Pure theorem as follows:
wenzelm@29735:   \[
wenzelm@29735:   @{text "IntI:"}~@{prop "x \<in> A \<Longrightarrow> x \<in> B \<Longrightarrow> x \<in> A \<inter> B"}
wenzelm@29735:   \]
wenzelm@29735: 
wenzelm@29735:   \noindent This is a plain Horn clause, since no further nesting on
wenzelm@29735:   the left is involved.  The general @{text "\<Inter>"}-introduction
wenzelm@29735:   corresponds to a Hereditary Harrop Formula with one additional level
wenzelm@29735:   of nesting:
wenzelm@29735:   \[
wenzelm@29735:   @{text "InterI:"}~@{prop "(\<And>A. A \<in> \<A> \<Longrightarrow> x \<in> A) \<Longrightarrow> x \<in> \<Inter>\<A>"}
wenzelm@29735:   \]
wenzelm@29735: 
wenzelm@53015:   \medskip Goals are also represented as rules: @{text "A\<^sub>1 \<Longrightarrow>
wenzelm@53015:   \<dots> A\<^sub>n \<Longrightarrow> C"} states that the sub-goals @{text "A\<^sub>1, \<dots>,
wenzelm@53015:   A\<^sub>n"} entail the result @{text "C"}; for @{text "n = 0"} the
wenzelm@29729:   goal is finished.  To allow @{text "C"} being a rule statement
wenzelm@29729:   itself, we introduce the protective marker @{text "# :: prop \<Rightarrow>
wenzelm@29729:   prop"}, which is defined as identity and hidden from the user.  We
wenzelm@29729:   initialize and finish goal states as follows:
wenzelm@29729: 
wenzelm@29729:   \[
wenzelm@29729:   \begin{array}{c@ {\qquad}c}
wenzelm@29729:   \infer[(@{inference_def init})]{@{text "C \<Longrightarrow> #C"}}{} &
wenzelm@29729:   \infer[(@{inference_def finish})]{@{text C}}{@{text "#C"}}
wenzelm@29729:   \end{array}
wenzelm@29729:   \]
wenzelm@29729: 
wenzelm@29735:   \noindent Goal states are refined in intermediate proof steps until
wenzelm@29735:   a finished form is achieved.  Here the two main reasoning principles
wenzelm@29735:   are @{inference resolution}, for back-chaining a rule against a
wenzelm@29735:   sub-goal (replacing it by zero or more sub-goals), and @{inference
wenzelm@29729:   assumption}, for solving a sub-goal (finding a short-circuit with
wenzelm@29729:   local assumptions).  Below @{text "\<^vec>x"} stands for @{text
wenzelm@53015:   "x\<^sub>1, \<dots>, x\<^sub>n"} (@{text "n \<ge> 0"}).
wenzelm@29729: 
wenzelm@29729:   \[
wenzelm@29729:   \infer[(@{inference_def resolution})]
wenzelm@29729:   {@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> \<^vec>A (\<^vec>a \<^vec>x))\<vartheta> \<Longrightarrow> C\<vartheta>"}}
wenzelm@29729:   {\begin{tabular}{rl}
wenzelm@29729:     @{text "rule:"} &
wenzelm@29729:     @{text "\<^vec>A \<^vec>a \<Longrightarrow> B \<^vec>a"} \\
wenzelm@29729:     @{text "goal:"} &
wenzelm@29729:     @{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> B' \<^vec>x) \<Longrightarrow> C"} \\
wenzelm@29729:     @{text "goal unifier:"} &
wenzelm@29729:     @{text "(\<lambda>\<^vec>x. B (\<^vec>a \<^vec>x))\<vartheta> = B'\<vartheta>"} \\
wenzelm@29729:    \end{tabular}}
wenzelm@29729:   \]
wenzelm@29729: 
wenzelm@29729:   \medskip
wenzelm@29729: 
wenzelm@29729:   \[
wenzelm@29729:   \infer[(@{inference_def assumption})]{@{text "C\<vartheta>"}}
wenzelm@29729:   {\begin{tabular}{rl}
wenzelm@29729:     @{text "goal:"} &
wenzelm@29729:     @{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> A \<^vec>x) \<Longrightarrow> C"} \\
wenzelm@29729:     @{text "assm unifier:"} & @{text "A\<vartheta> = H\<^sub>i\<vartheta>"}~~\text{(for some~@{text "H\<^sub>i"})} \\
wenzelm@29729:    \end{tabular}}
wenzelm@29729:   \]
wenzelm@29729: 
wenzelm@29729:   The following trace illustrates goal-oriented reasoning in
wenzelm@29729:   Isabelle/Pure:
wenzelm@29729: 
wenzelm@29735:   {\footnotesize
wenzelm@29729:   \medskip
wenzelm@29735:   \begin{tabular}{r@ {\quad}l}
wenzelm@29729:   @{text "(A \<and> B \<Longrightarrow> B \<and> A) \<Longrightarrow> #(A \<and> B \<Longrightarrow> B \<and> A)"} & @{text "(init)"} \\
wenzelm@29729:   @{text "(A \<and> B \<Longrightarrow> B) \<Longrightarrow> (A \<and> B \<Longrightarrow> A) \<Longrightarrow> #\<dots>"} & @{text "(resolution B \<Longrightarrow> A \<Longrightarrow> B \<and> A)"} \\
wenzelm@29729:   @{text "(A \<and> B \<Longrightarrow> A \<and> B) \<Longrightarrow> (A \<and> B \<Longrightarrow> A) \<Longrightarrow> #\<dots>"} & @{text "(resolution A \<and> B \<Longrightarrow> B)"} \\
wenzelm@29729:   @{text "(A \<and> B \<Longrightarrow> A) \<Longrightarrow> #\<dots>"} & @{text "(assumption)"} \\
wenzelm@48279:   @{text "(A \<and> B \<Longrightarrow> A \<and> B) \<Longrightarrow> #\<dots>"} & @{text "(resolution A \<and> B \<Longrightarrow> A)"} \\
wenzelm@29729:   @{text "#\<dots>"} & @{text "(assumption)"} \\
wenzelm@29729:   @{text "A \<and> B \<Longrightarrow> B \<and> A"} & @{text "(finish)"} \\
wenzelm@29729:   \end{tabular}
wenzelm@29729:   \medskip
wenzelm@29735:   }
wenzelm@29729: 
wenzelm@29729:   Compositions of @{inference assumption} after @{inference
wenzelm@29729:   resolution} occurs quite often, typically in elimination steps.
wenzelm@29729:   Traditional Isabelle tactics accommodate this by a combined
wenzelm@29729:   @{inference_def elim_resolution} principle.  In contrast, Isar uses
wenzelm@29729:   a slightly more refined combination, where the assumptions to be
wenzelm@29729:   closed are marked explicitly, using again the protective marker
wenzelm@29729:   @{text "#"}:
wenzelm@29729: 
wenzelm@29729:   \[
wenzelm@29729:   \infer[(@{inference refinement})]
wenzelm@29729:   {@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> \<^vec>G' (\<^vec>a \<^vec>x))\<vartheta> \<Longrightarrow> C\<vartheta>"}}
wenzelm@29729:   {\begin{tabular}{rl}
wenzelm@42666:     @{text "sub\<hyphen>proof:"} &
wenzelm@29729:     @{text "\<^vec>G \<^vec>a \<Longrightarrow> B \<^vec>a"} \\
wenzelm@29729:     @{text "goal:"} &
wenzelm@29729:     @{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> B' \<^vec>x) \<Longrightarrow> C"} \\
wenzelm@29729:     @{text "goal unifier:"} &
wenzelm@29729:     @{text "(\<lambda>\<^vec>x. B (\<^vec>a \<^vec>x))\<vartheta> = B'\<vartheta>"} \\
wenzelm@29729:     @{text "assm unifiers:"} &
wenzelm@29729:     @{text "(\<lambda>\<^vec>x. G\<^sub>j (\<^vec>a \<^vec>x))\<vartheta> = #H\<^sub>i\<vartheta>"} \\
wenzelm@29729:     & \quad (for each marked @{text "G\<^sub>j"} some @{text "#H\<^sub>i"}) \\
wenzelm@29729:    \end{tabular}}
wenzelm@29729:   \]
wenzelm@29729: 
wenzelm@42666:   \noindent Here the @{text "sub\<hyphen>proof"} rule stems from the
wenzelm@29737:   main @{command fix}-@{command assume}-@{command show} outline of
wenzelm@29737:   Isar (cf.\ \secref{sec:framework-subproof}): each assumption
wenzelm@29729:   indicated in the text results in a marked premise @{text "G"} above.
wenzelm@29735:   The marking enforces resolution against one of the sub-goal's
wenzelm@29737:   premises.  Consequently, @{command fix}-@{command assume}-@{command
wenzelm@29737:   show} enables to fit the result of a sub-proof quite robustly into a
wenzelm@29737:   pending sub-goal, while maintaining a good measure of flexibility.
wenzelm@58618: \<close>
wenzelm@29729: 
wenzelm@29729: 
wenzelm@58618: section \<open>The Isar proof language \label{sec:framework-isar}\<close>
wenzelm@29729: 
wenzelm@58618: text \<open>
wenzelm@29729:   Structured proofs are presented as high-level expressions for
wenzelm@29729:   composing entities of Pure (propositions, facts, and goals).  The
wenzelm@29729:   Isar proof language allows to organize reasoning within the
wenzelm@29729:   underlying rule calculus of Pure, but Isar is not another logical
wenzelm@29729:   calculus!
wenzelm@29729: 
wenzelm@29729:   Isar is an exercise in sound minimalism.  Approximately half of the
wenzelm@29729:   language is introduced as primitive, the rest defined as derived
wenzelm@29729:   concepts.  The following grammar describes the core language
wenzelm@29729:   (category @{text "proof"}), which is embedded into theory
wenzelm@29729:   specification elements such as @{command theorem}; see also
wenzelm@29729:   \secref{sec:framework-stmt} for the separate category @{text
wenzelm@29729:   "statement"}.
wenzelm@29729: 
wenzelm@29729:   \medskip
wenzelm@29729:   \begin{tabular}{rcl}
wenzelm@42666:     @{text "theory\<hyphen>stmt"} & = & @{command "theorem"}~@{text "statement proof  |"}~~@{command "definition"}~@{text "\<dots>  |  \<dots>"} \\[1ex]
wenzelm@29729: 
wenzelm@29729:     @{text "proof"} & = & @{text "prfx\<^sup>*"}~@{command "proof"}~@{text "method\<^sup>? stmt\<^sup>*"}~@{command "qed"}~@{text "method\<^sup>?"} \\[1ex]
wenzelm@29729: 
wenzelm@29729:     @{text prfx} & = & @{command "using"}~@{text "facts"} \\
wenzelm@29729:     & @{text "|"} & @{command "unfolding"}~@{text "facts"} \\
wenzelm@29729: 
wenzelm@29729:     @{text stmt} & = & @{command "{"}~@{text "stmt\<^sup>*"}~@{command "}"} \\
wenzelm@29729:     & @{text "|"} & @{command "next"} \\
wenzelm@29729:     & @{text "|"} & @{command "note"}~@{text "name = facts"} \\
wenzelm@29729:     & @{text "|"} & @{command "let"}~@{text "term = term"} \\
wenzelm@29729:     & @{text "|"} & @{command "fix"}~@{text "var\<^sup>+"} \\
wenzelm@29737:     & @{text "|"} & @{command assume}~@{text "\<guillemotleft>inference\<guillemotright> name: props"} \\
wenzelm@29729:     & @{text "|"} & @{command "then"}@{text "\<^sup>?"}~@{text goal} \\
wenzelm@29729:     @{text goal} & = & @{command "have"}~@{text "name: props proof"} \\
wenzelm@29729:     & @{text "|"} & @{command "show"}~@{text "name: props proof"} \\
wenzelm@29729:   \end{tabular}
wenzelm@29729: 
wenzelm@29729:   \medskip Simultaneous propositions or facts may be separated by the
wenzelm@29729:   @{keyword "and"} keyword.
wenzelm@29729: 
wenzelm@29729:   \medskip The syntax for terms and propositions is inherited from
wenzelm@29729:   Pure (and the object-logic).  A @{text "pattern"} is a @{text
wenzelm@29729:   "term"} with schematic variables, to be bound by higher-order
wenzelm@29729:   matching.
wenzelm@29729: 
wenzelm@29735:   \medskip Facts may be referenced by name or proposition.  For
wenzelm@29737:   example, the result of ``@{command have}~@{text "a: A \<langle>proof\<rangle>"}''
wenzelm@29735:   becomes available both as @{text "a"} and
wenzelm@29735:   \isacharbackquoteopen@{text "A"}\isacharbackquoteclose.  Moreover,
wenzelm@29735:   fact expressions may involve attributes that modify either the
wenzelm@29735:   theorem or the background context.  For example, the expression
wenzelm@29735:   ``@{text "a [OF b]"}'' refers to the composition of two facts
wenzelm@29735:   according to the @{inference resolution} inference of
wenzelm@29735:   \secref{sec:framework-resolution}, while ``@{text "a [intro]"}''
wenzelm@29735:   declares a fact as introduction rule in the context.
wenzelm@29729: 
wenzelm@29735:   The special fact called ``@{fact this}'' always refers to the last
wenzelm@29737:   result, as produced by @{command note}, @{command assume}, @{command
wenzelm@29737:   have}, or @{command show}.  Since @{command note} occurs
wenzelm@29737:   frequently together with @{command then} we provide some
wenzelm@29737:   abbreviations:
wenzelm@29729: 
wenzelm@29737:   \medskip
wenzelm@29737:   \begin{tabular}{rcl}
wenzelm@29737:     @{command from}~@{text a} & @{text "\<equiv>"} & @{command note}~@{text a}~@{command then} \\
wenzelm@29737:     @{command with}~@{text a} & @{text "\<equiv>"} & @{command from}~@{text "a \<AND> this"} \\
wenzelm@29737:   \end{tabular}
wenzelm@29737:   \medskip
wenzelm@29737: 
wenzelm@29737:   The @{text "method"} category is essentially a parameter and may be
wenzelm@29737:   populated later.  Methods use the facts indicated by @{command
wenzelm@29737:   "then"} or @{command using}, and then operate on the goal state.
wenzelm@29737:   Some basic methods are predefined: ``@{method "-"}'' leaves the goal
wenzelm@29737:   unchanged, ``@{method this}'' applies the facts as rules to the
wenzelm@42626:   goal, ``@{method (Pure) "rule"}'' applies the facts to another rule and the
wenzelm@42626:   result to the goal (both ``@{method this}'' and ``@{method (Pure) rule}''
wenzelm@29737:   refer to @{inference resolution} of
wenzelm@29729:   \secref{sec:framework-resolution}).  The secondary arguments to
wenzelm@42626:   ``@{method (Pure) rule}'' may be specified explicitly as in ``@{text "(rule
wenzelm@29729:   a)"}'', or picked from the context.  In the latter case, the system
wenzelm@29729:   first tries rules declared as @{attribute (Pure) elim} or
wenzelm@29729:   @{attribute (Pure) dest}, followed by those declared as @{attribute
wenzelm@29729:   (Pure) intro}.
wenzelm@29729: 
wenzelm@42626:   The default method for @{command proof} is ``@{method (Pure) rule}''
wenzelm@29737:   (arguments picked from the context), for @{command qed} it is
wenzelm@29729:   ``@{method "-"}''.  Further abbreviations for terminal proof steps
wenzelm@29729:   are ``@{command "by"}~@{text "method\<^sub>1 method\<^sub>2"}'' for
wenzelm@29737:   ``@{command proof}~@{text "method\<^sub>1"}~@{command qed}~@{text
wenzelm@29737:   "method\<^sub>2"}'', and ``@{command ".."}'' for ``@{command
wenzelm@42626:   "by"}~@{method (Pure) rule}, and ``@{command "."}'' for ``@{command
wenzelm@29737:   "by"}~@{method this}''.  The @{command unfolding} element operates
wenzelm@29737:   directly on the current facts and goal by applying equalities.
wenzelm@29729: 
wenzelm@29737:   \medskip Block structure can be indicated explicitly by ``@{command
wenzelm@29737:   "{"}~@{text "\<dots>"}~@{command "}"}'', although the body of a sub-proof
wenzelm@29737:   already involves implicit nesting.  In any case, @{command next}
wenzelm@29737:   jumps into the next section of a block, i.e.\ it acts like closing
wenzelm@29737:   an implicit block scope and opening another one; there is no direct
wenzelm@29737:   correspondence to subgoals here.
wenzelm@29729: 
wenzelm@29737:   The remaining elements @{command fix} and @{command assume} build up
wenzelm@29737:   a local context (see \secref{sec:framework-context}), while
wenzelm@29737:   @{command show} refines a pending sub-goal by the rule resulting
wenzelm@29729:   from a nested sub-proof (see \secref{sec:framework-subproof}).
wenzelm@29729:   Further derived concepts will support calculational reasoning (see
wenzelm@29729:   \secref{sec:framework-calc}).
wenzelm@58618: \<close>
wenzelm@29729: 
wenzelm@29729: 
wenzelm@58618: subsection \<open>Context elements \label{sec:framework-context}\<close>
wenzelm@29729: 
wenzelm@58618: text \<open>
wenzelm@29729:   In judgments @{text "\<Gamma> \<turnstile> \<phi>"} of the primitive framework, @{text "\<Gamma>"}
wenzelm@29729:   essentially acts like a proof context.  Isar elaborates this idea
wenzelm@29735:   towards a higher-level notion, with additional information for
wenzelm@29729:   type-inference, term abbreviations, local facts, hypotheses etc.
wenzelm@29729: 
wenzelm@29737:   The element @{command fix}~@{text "x :: \<alpha>"} declares a local
wenzelm@29729:   parameter, i.e.\ an arbitrary-but-fixed entity of a given type; in
wenzelm@29729:   results exported from the context, @{text "x"} may become anything.
wenzelm@29737:   The @{command assume}~@{text "\<guillemotleft>inference\<guillemotright>"} element provides a
wenzelm@29737:   general interface to hypotheses: ``@{command assume}~@{text
wenzelm@29737:   "\<guillemotleft>inference\<guillemotright> A"}'' produces @{text "A \<turnstile> A"} locally, while the
wenzelm@29737:   included inference tells how to discharge @{text A} from results
wenzelm@29737:   @{text "A \<turnstile> B"} later on.  There is no user-syntax for @{text
wenzelm@29737:   "\<guillemotleft>inference\<guillemotright>"}, i.e.\ it may only occur internally when derived
wenzelm@29737:   commands are defined in ML.
wenzelm@29737: 
wenzelm@29737:   At the user-level, the default inference for @{command assume} is
wenzelm@29737:   @{inference discharge} as given below.  The additional variants
wenzelm@29737:   @{command presume} and @{command def} are defined as follows:
wenzelm@29737: 
wenzelm@29737:   \medskip
wenzelm@29737:   \begin{tabular}{rcl}
wenzelm@42666:     @{command presume}~@{text A} & @{text "\<equiv>"} & @{command assume}~@{text "\<guillemotleft>weak\<hyphen>discharge\<guillemotright> A"} \\
wenzelm@29737:     @{command def}~@{text "x \<equiv> a"} & @{text "\<equiv>"} & @{command fix}~@{text x}~@{command assume}~@{text "\<guillemotleft>expansion\<guillemotright> x \<equiv> a"} \\
wenzelm@29737:   \end{tabular}
wenzelm@29737:   \medskip
wenzelm@29729: 
wenzelm@29729:   \[
wenzelm@29737:   \infer[(@{inference_def discharge})]{@{text "\<strut>\<Gamma> - A \<turnstile> #A \<Longrightarrow> B"}}{@{text "\<strut>\<Gamma> \<turnstile> B"}}
wenzelm@29737:   \]
wenzelm@29737:   \[
wenzelm@42666:   \infer[(@{inference_def "weak\<hyphen>discharge"})]{@{text "\<strut>\<Gamma> - A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<strut>\<Gamma> \<turnstile> B"}}
wenzelm@29737:   \]
wenzelm@29737:   \[
wenzelm@29729:   \infer[(@{inference_def expansion})]{@{text "\<strut>\<Gamma> - (x \<equiv> a) \<turnstile> B a"}}{@{text "\<strut>\<Gamma> \<turnstile> B x"}}
wenzelm@29729:   \]
wenzelm@29729: 
wenzelm@29737:   \medskip Note that @{inference discharge} and @{inference
wenzelm@42666:   "weak\<hyphen>discharge"} differ in the marker for @{prop A}, which is
wenzelm@29737:   relevant when the result of a @{command fix}-@{command
wenzelm@29737:   assume}-@{command show} outline is composed with a pending goal,
wenzelm@29737:   cf.\ \secref{sec:framework-subproof}.
wenzelm@29729: 
wenzelm@29737:   The most interesting derived context element in Isar is @{command
wenzelm@58552:   obtain} @{cite \<open>\S5.3\<close> "Wenzel-PhD"}, which supports generalized
wenzelm@29737:   elimination steps in a purely forward manner.  The @{command obtain}
wenzelm@29739:   command takes a specification of parameters @{text "\<^vec>x"} and
wenzelm@29737:   assumptions @{text "\<^vec>A"} to be added to the context, together
wenzelm@29737:   with a proof of a case rule stating that this extension is
wenzelm@29737:   conservative (i.e.\ may be removed from closed results later on):
wenzelm@29729: 
wenzelm@29729:   \medskip
wenzelm@29729:   \begin{tabular}{l}
wenzelm@29729:   @{text "\<langle>facts\<rangle>"}~~@{command obtain}~@{text "\<^vec>x \<WHERE> \<^vec>A \<^vec>x  \<langle>proof\<rangle> \<equiv>"} \\[0.5ex]
wenzelm@29729:   \quad @{command have}~@{text "case: \<And>thesis. (\<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis) \<Longrightarrow> thesis\<rangle>"} \\
wenzelm@29729:   \quad @{command proof}~@{method "-"} \\
wenzelm@29729:   \qquad @{command fix}~@{text thesis} \\
wenzelm@29729:   \qquad @{command assume}~@{text "[intro]: \<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis"} \\
wenzelm@29733:   \qquad @{command show}~@{text thesis}~@{command using}~@{text "\<langle>facts\<rangle> \<langle>proof\<rangle>"} \\
wenzelm@29729:   \quad @{command qed} \\
wenzelm@29737:   \quad @{command fix}~@{text "\<^vec>x"}~@{command assume}~@{text "\<guillemotleft>elimination case\<guillemotright> \<^vec>A \<^vec>x"} \\
wenzelm@29729:   \end{tabular}
wenzelm@29729:   \medskip
wenzelm@29729: 
wenzelm@29729:   \[
wenzelm@29729:   \infer[(@{inference elimination})]{@{text "\<Gamma> \<turnstile> B"}}{
wenzelm@29729:     \begin{tabular}{rl}
wenzelm@29729:     @{text "case:"} &
wenzelm@29729:     @{text "\<Gamma> \<turnstile> \<And>thesis. (\<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis) \<Longrightarrow> thesis"} \\[0.2ex]
wenzelm@29729:     @{text "result:"} &
wenzelm@29729:     @{text "\<Gamma> \<union> \<^vec>A \<^vec>y \<turnstile> B"} \\[0.2ex]
wenzelm@29729:     \end{tabular}}
wenzelm@29729:   \]
wenzelm@29729: 
wenzelm@29729:   \noindent Here the name ``@{text thesis}'' is a specific convention
wenzelm@29729:   for an arbitrary-but-fixed proposition; in the primitive natural
wenzelm@29729:   deduction rules shown before we have occasionally used @{text C}.
wenzelm@29737:   The whole statement of ``@{command obtain}~@{text x}~@{keyword
wenzelm@29729:   "where"}~@{text "A x"}'' may be read as a claim that @{text "A x"}
wenzelm@29729:   may be assumed for some arbitrary-but-fixed @{text "x"}.  Also note
wenzelm@29737:   that ``@{command obtain}~@{text "A \<AND> B"}'' without parameters
wenzelm@29737:   is similar to ``@{command have}~@{text "A \<AND> B"}'', but the
wenzelm@29737:   latter involves multiple sub-goals.
wenzelm@29729: 
wenzelm@29729:   \medskip The subsequent Isar proof texts explain all context
wenzelm@29729:   elements introduced above using the formal proof language itself.
wenzelm@29729:   After finishing a local proof within a block, we indicate the
wenzelm@29739:   exported result via @{command note}.
wenzelm@58618: \<close>
wenzelm@29729: 
wenzelm@29729: (*<*)
wenzelm@29729: theorem True
wenzelm@29729: proof
wenzelm@29729: (*>*)
wenzelm@58999:   text_raw \<open>\begin{minipage}[t]{0.45\textwidth}\<close>
wenzelm@29729:   {
wenzelm@29729:     fix x
wenzelm@29735:     have "B x" sorry %noproof
wenzelm@29729:   }
wenzelm@58618:   note \<open>\<And>x. B x\<close>
wenzelm@58999:   text_raw \<open>\end{minipage}\quad\begin{minipage}[t]{0.45\textwidth}\<close>(*<*)next(*>*)
wenzelm@29735:   {
wenzelm@29735:     assume A
wenzelm@29735:     have B sorry %noproof
wenzelm@29735:   }
wenzelm@58618:   note \<open>A \<Longrightarrow> B\<close>
wenzelm@58999:   text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.45\textwidth}\<close>(*<*)next(*>*)
wenzelm@29729:   {
wenzelm@29729:     def x \<equiv> a
wenzelm@29735:     have "B x" sorry %noproof
wenzelm@29729:   }
wenzelm@58618:   note \<open>B a\<close>
wenzelm@58999:   text_raw \<open>\end{minipage}\quad\begin{minipage}[t]{0.45\textwidth}\<close>(*<*)next(*>*)
wenzelm@29729:   {
wenzelm@29735:     obtain x where "A x" sorry %noproof
wenzelm@29733:     have B sorry %noproof
wenzelm@29729:   }
wenzelm@58618:   note \<open>B\<close>
wenzelm@58999:   text_raw \<open>\end{minipage}\<close>
wenzelm@29729: (*<*)
wenzelm@29729: qed
wenzelm@29729: (*>*)
wenzelm@29729: 
wenzelm@58618: text \<open>
wenzelm@29739:   \bigskip\noindent This illustrates the meaning of Isar context
wenzelm@29739:   elements without goals getting in between.
wenzelm@58618: \<close>
wenzelm@29729: 
wenzelm@58618: subsection \<open>Structured statements \label{sec:framework-stmt}\<close>
wenzelm@29729: 
wenzelm@58618: text \<open>
wenzelm@29729:   The category @{text "statement"} of top-level theorem specifications
wenzelm@29729:   is defined as follows:
wenzelm@29729: 
wenzelm@29729:   \medskip
wenzelm@29729:   \begin{tabular}{rcl}
wenzelm@29729:   @{text "statement"} & @{text "\<equiv>"} & @{text "name: props \<AND> \<dots>"} \\
wenzelm@29729:   & @{text "|"} & @{text "context\<^sup>* conclusion"} \\[0.5ex]
wenzelm@29729: 
wenzelm@29729:   @{text "context"} & @{text "\<equiv>"} & @{text "\<FIXES> vars \<AND> \<dots>"} \\
wenzelm@29729:   & @{text "|"} & @{text "\<ASSUMES> name: props \<AND> \<dots>"} \\
wenzelm@29729: 
wenzelm@29729:   @{text "conclusion"} & @{text "\<equiv>"} & @{text "\<SHOWS> name: props \<AND> \<dots>"} \\
wenzelm@29735:   & @{text "|"} & @{text "\<OBTAINS> vars \<AND> \<dots> \<WHERE> name: props \<AND> \<dots>"} \\
wenzelm@29735:   & & \quad @{text "\<BBAR> \<dots>"} \\
wenzelm@29729:   \end{tabular}
wenzelm@29729: 
wenzelm@29729:   \medskip\noindent A simple @{text "statement"} consists of named
wenzelm@29729:   propositions.  The full form admits local context elements followed
wenzelm@29729:   by the actual conclusions, such as ``@{keyword "fixes"}~@{text
wenzelm@29729:   x}~@{keyword "assumes"}~@{text "A x"}~@{keyword "shows"}~@{text "B
wenzelm@29729:   x"}''.  The final result emerges as a Pure rule after discharging
wenzelm@29729:   the context: @{prop "\<And>x. A x \<Longrightarrow> B x"}.
wenzelm@29729: 
wenzelm@29729:   The @{keyword "obtains"} variant is another abbreviation defined
wenzelm@29729:   below; unlike @{command obtain} (cf.\
wenzelm@29729:   \secref{sec:framework-context}) there may be several ``cases''
wenzelm@29729:   separated by ``@{text "\<BBAR>"}'', each consisting of several
wenzelm@29729:   parameters (@{text "vars"}) and several premises (@{text "props"}).
wenzelm@29729:   This specifies multi-branch elimination rules.
wenzelm@29729: 
wenzelm@29729:   \medskip
wenzelm@29729:   \begin{tabular}{l}
wenzelm@29729:   @{text "\<OBTAINS> \<^vec>x \<WHERE> \<^vec>A \<^vec>x   \<BBAR>   \<dots>   \<equiv>"} \\[0.5ex]
wenzelm@29729:   \quad @{text "\<FIXES> thesis"} \\
wenzelm@29729:   \quad @{text "\<ASSUMES> [intro]: \<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis  \<AND>  \<dots>"} \\
wenzelm@29729:   \quad @{text "\<SHOWS> thesis"} \\
wenzelm@29729:   \end{tabular}
wenzelm@29729:   \medskip
wenzelm@29729: 
wenzelm@29729:   Presenting structured statements in such an ``open'' format usually
wenzelm@29729:   simplifies the subsequent proof, because the outer structure of the
wenzelm@29729:   problem is already laid out directly.  E.g.\ consider the following
wenzelm@29729:   canonical patterns for @{text "\<SHOWS>"} and @{text "\<OBTAINS>"},
wenzelm@29729:   respectively:
wenzelm@58618: \<close>
wenzelm@29729: 
wenzelm@58618: text_raw \<open>\begin{minipage}{0.5\textwidth}\<close>
wenzelm@29729: 
wenzelm@29729: theorem
wenzelm@29729:   fixes x and y
wenzelm@29729:   assumes "A x" and "B y"
wenzelm@29729:   shows "C x y"
wenzelm@29729: proof -
wenzelm@58618:   from \<open>A x\<close> and \<open>B y\<close>
wenzelm@29733:   show "C x y" sorry %noproof
wenzelm@29729: qed
wenzelm@29729: 
wenzelm@58618: text_raw \<open>\end{minipage}\begin{minipage}{0.5\textwidth}\<close>
wenzelm@29729: 
wenzelm@29729: theorem
wenzelm@29729:   obtains x and y
wenzelm@29729:   where "A x" and "B y"
wenzelm@29729: proof -
wenzelm@29733:   have "A a" and "B b" sorry %noproof
wenzelm@29729:   then show thesis ..
wenzelm@29729: qed
wenzelm@29729: 
wenzelm@58618: text_raw \<open>\end{minipage}\<close>
wenzelm@29729: 
wenzelm@58618: text \<open>
wenzelm@29729:   \medskip\noindent Here local facts \isacharbackquoteopen@{text "A
wenzelm@29729:   x"}\isacharbackquoteclose\ and \isacharbackquoteopen@{text "B
wenzelm@29729:   y"}\isacharbackquoteclose\ are referenced immediately; there is no
wenzelm@29729:   need to decompose the logical rule structure again.  In the second
wenzelm@29729:   proof the final ``@{command then}~@{command show}~@{text
wenzelm@29729:   thesis}~@{command ".."}''  involves the local rule case @{text "\<And>x
wenzelm@29729:   y. A x \<Longrightarrow> B y \<Longrightarrow> thesis"} for the particular instance of terms @{text
wenzelm@29729:   "a"} and @{text "b"} produced in the body.
wenzelm@58618: \<close>
wenzelm@29729: 
wenzelm@29729: 
wenzelm@58618: subsection \<open>Structured proof refinement \label{sec:framework-subproof}\<close>
wenzelm@29729: 
wenzelm@58618: text \<open>
wenzelm@29729:   By breaking up the grammar for the Isar proof language, we may
wenzelm@29729:   understand a proof text as a linear sequence of individual proof
wenzelm@29729:   commands.  These are interpreted as transitions of the Isar virtual
wenzelm@29729:   machine (Isar/VM), which operates on a block-structured
wenzelm@29729:   configuration in single steps.  This allows users to write proof
wenzelm@29729:   texts in an incremental manner, and inspect intermediate
wenzelm@29729:   configurations for debugging.
wenzelm@29729: 
wenzelm@29729:   The basic idea is analogous to evaluating algebraic expressions on a
wenzelm@29729:   stack machine: @{text "(a + b) \<cdot> c"} then corresponds to a sequence
wenzelm@29729:   of single transitions for each symbol @{text "(, a, +, b, ), \<cdot>, c"}.
wenzelm@29729:   In Isar the algebraic values are facts or goals, and the operations
wenzelm@29729:   are inferences.
wenzelm@29729: 
wenzelm@29729:   \medskip The Isar/VM state maintains a stack of nodes, each node
wenzelm@29729:   contains the local proof context, the linguistic mode, and a pending
wenzelm@29729:   goal (optional).  The mode determines the type of transition that
wenzelm@29729:   may be performed next, it essentially alternates between forward and
wenzelm@29738:   backward reasoning, with an intermediate stage for chained facts
wenzelm@29738:   (see \figref{fig:isar-vm}).
wenzelm@29738: 
wenzelm@29738:   \begin{figure}[htb]
wenzelm@29738:   \begin{center}
wenzelm@48958:   \includegraphics[width=0.8\textwidth]{isar-vm}
wenzelm@29738:   \end{center}
wenzelm@29738:   \caption{Isar/VM modes}\label{fig:isar-vm}
wenzelm@29738:   \end{figure}
wenzelm@29738: 
wenzelm@29738:   For example, in @{text "state"} mode Isar acts like a mathematical
wenzelm@29738:   scratch-pad, accepting declarations like @{command fix}, @{command
wenzelm@29738:   assume}, and claims like @{command have}, @{command show}.  A goal
wenzelm@29738:   statement changes the mode to @{text "prove"}, which means that we
wenzelm@29738:   may now refine the problem via @{command unfolding} or @{command
wenzelm@29738:   proof}.  Then we are again in @{text "state"} mode of a proof body,
wenzelm@29738:   which may issue @{command show} statements to solve pending
wenzelm@29738:   sub-goals.  A concluding @{command qed} will return to the original
wenzelm@29738:   @{text "state"} mode one level upwards.  The subsequent Isar/VM
wenzelm@29738:   trace indicates block structure, linguistic mode, goal state, and
wenzelm@29738:   inferences:
wenzelm@58618: \<close>
wenzelm@29729: 
wenzelm@58618: text_raw \<open>\begingroup\footnotesize\<close>
wenzelm@40964: (*<*)notepad begin
wenzelm@29729: (*>*)
wenzelm@58999:   text_raw \<open>\begin{minipage}[t]{0.18\textwidth}\<close>
wenzelm@29729:   have "A \<longrightarrow> B"
wenzelm@29729:   proof
wenzelm@29729:     assume A
wenzelm@29729:     show B
wenzelm@29733:       sorry %noproof
wenzelm@29729:   qed
wenzelm@58999:   text_raw \<open>\end{minipage}\quad
wenzelm@29735: \begin{minipage}[t]{0.06\textwidth}
wenzelm@29729: @{text "begin"} \\
wenzelm@29729: \\
wenzelm@29729: \\
wenzelm@29729: @{text "begin"} \\
wenzelm@29729: @{text "end"} \\
wenzelm@29729: @{text "end"} \\
wenzelm@29729: \end{minipage}
wenzelm@29729: \begin{minipage}[t]{0.08\textwidth}
wenzelm@29729: @{text "prove"} \\
wenzelm@29729: @{text "state"} \\
wenzelm@29729: @{text "state"} \\
wenzelm@29729: @{text "prove"} \\
wenzelm@29729: @{text "state"} \\
wenzelm@29729: @{text "state"} \\
wenzelm@29735: \end{minipage}\begin{minipage}[t]{0.35\textwidth}
wenzelm@29729: @{text "(A \<longrightarrow> B) \<Longrightarrow> #(A \<longrightarrow> B)"} \\
wenzelm@29729: @{text "(A \<Longrightarrow> B) \<Longrightarrow> #(A \<longrightarrow> B)"} \\
wenzelm@29729: \\
wenzelm@29729: \\
wenzelm@29729: @{text "#(A \<longrightarrow> B)"} \\
wenzelm@29729: @{text "A \<longrightarrow> B"} \\
wenzelm@29735: \end{minipage}\begin{minipage}[t]{0.4\textwidth}
wenzelm@29729: @{text "(init)"} \\
wenzelm@29735: @{text "(resolution impI)"} \\
wenzelm@29729: \\
wenzelm@29729: \\
wenzelm@29729: @{text "(refinement #A \<Longrightarrow> B)"} \\
wenzelm@29729: @{text "(finish)"} \\
wenzelm@58618: \end{minipage}\<close>
wenzelm@29729: (*<*)
wenzelm@40964: end
wenzelm@29729: (*>*)
wenzelm@58618: text_raw \<open>\endgroup\<close>
wenzelm@29729: 
wenzelm@58618: text \<open>
wenzelm@29735:   \noindent Here the @{inference refinement} inference from
wenzelm@29729:   \secref{sec:framework-resolution} mediates composition of Isar
wenzelm@29729:   sub-proofs nicely.  Observe that this principle incorporates some
wenzelm@29729:   degree of freedom in proof composition.  In particular, the proof
wenzelm@29729:   body allows parameters and assumptions to be re-ordered, or commuted
wenzelm@29729:   according to Hereditary Harrop Form.  Moreover, context elements
wenzelm@29729:   that are not used in a sub-proof may be omitted altogether.  For
wenzelm@29729:   example:
wenzelm@58618: \<close>
wenzelm@29729: 
wenzelm@58618: text_raw \<open>\begin{minipage}{0.5\textwidth}\<close>
wenzelm@29729: 
wenzelm@29729: (*<*)
wenzelm@40964: notepad
wenzelm@40964: begin
wenzelm@29729: (*>*)
wenzelm@29729:   have "\<And>x y. A x \<Longrightarrow> B y \<Longrightarrow> C x y"
wenzelm@29729:   proof -
wenzelm@29729:     fix x and y
wenzelm@29729:     assume "A x" and "B y"
wenzelm@29733:     show "C x y" sorry %noproof
wenzelm@29729:   qed
wenzelm@29729: 
wenzelm@58999: text_raw \<open>\end{minipage}\begin{minipage}{0.5\textwidth}\<close>
wenzelm@29729: 
wenzelm@29729: (*<*)
wenzelm@29729: next
wenzelm@29729: (*>*)
wenzelm@29729:   have "\<And>x y. A x \<Longrightarrow> B y \<Longrightarrow> C x y"
wenzelm@29729:   proof -
wenzelm@29729:     fix x assume "A x"
wenzelm@29729:     fix y assume "B y"
wenzelm@29733:     show "C x y" sorry %noproof
wenzelm@29729:   qed
wenzelm@29729: 
wenzelm@58999: text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}{0.5\textwidth}\<close>
wenzelm@29729: 
wenzelm@29729: (*<*)
wenzelm@29729: next
wenzelm@29729: (*>*)
wenzelm@29729:   have "\<And>x y. A x \<Longrightarrow> B y \<Longrightarrow> C x y"
wenzelm@29729:   proof -
wenzelm@29729:     fix y assume "B y"
wenzelm@29729:     fix x assume "A x"
wenzelm@29729:     show "C x y" sorry
wenzelm@29729:   qed
wenzelm@29729: 
wenzelm@58999: text_raw \<open>\end{minipage}\begin{minipage}{0.5\textwidth}\<close>
wenzelm@29729: (*<*)
wenzelm@29729: next
wenzelm@29729: (*>*)
wenzelm@29729:   have "\<And>x y. A x \<Longrightarrow> B y \<Longrightarrow> C x y"
wenzelm@29729:   proof -
wenzelm@29729:     fix y assume "B y"
wenzelm@29729:     fix x
wenzelm@29729:     show "C x y" sorry
wenzelm@29729:   qed
wenzelm@29729: (*<*)
wenzelm@40964: end
wenzelm@29729: (*>*)
wenzelm@29729: 
wenzelm@58618: text_raw \<open>\end{minipage}\<close>
wenzelm@29729: 
wenzelm@58618: text \<open>
wenzelm@29735:   \medskip\noindent Such ``peephole optimizations'' of Isar texts are
wenzelm@29729:   practically important to improve readability, by rearranging
wenzelm@29729:   contexts elements according to the natural flow of reasoning in the
wenzelm@29729:   body, while still observing the overall scoping rules.
wenzelm@29729: 
wenzelm@29729:   \medskip This illustrates the basic idea of structured proof
wenzelm@29729:   processing in Isar.  The main mechanisms are based on natural
wenzelm@29729:   deduction rule composition within the Pure framework.  In
wenzelm@29729:   particular, there are no direct operations on goal states within the
wenzelm@29729:   proof body.  Moreover, there is no hidden automated reasoning
wenzelm@29729:   involved, just plain unification.
wenzelm@58618: \<close>
wenzelm@29729: 
wenzelm@29729: 
wenzelm@58618: subsection \<open>Calculational reasoning \label{sec:framework-calc}\<close>
wenzelm@29729: 
wenzelm@58618: text \<open>
wenzelm@29735:   The existing Isar infrastructure is sufficiently flexible to support
wenzelm@29729:   calculational reasoning (chains of transitivity steps) as derived
wenzelm@29729:   concept.  The generic proof elements introduced below depend on
wenzelm@29732:   rules declared as @{attribute trans} in the context.  It is left to
wenzelm@29729:   the object-logic to provide a suitable rule collection for mixed
wenzelm@29732:   relations of @{text "="}, @{text "<"}, @{text "\<le>"}, @{text "\<subset>"},
wenzelm@29732:   @{text "\<subseteq>"} etc.  Due to the flexibility of rule composition
wenzelm@29729:   (\secref{sec:framework-resolution}), substitution of equals by
wenzelm@29729:   equals is covered as well, even substitution of inequalities
wenzelm@58552:   involving monotonicity conditions; see also @{cite \<open>\S6\<close> "Wenzel-PhD"}
wenzelm@58552:   and @{cite "Bauer-Wenzel:2001"}.
wenzelm@29729: 
wenzelm@29729:   The generic calculational mechanism is based on the observation that
wenzelm@29735:   rules such as @{text "trans:"}~@{prop "x = y \<Longrightarrow> y = z \<Longrightarrow> x = z"}
wenzelm@29735:   proceed from the premises towards the conclusion in a deterministic
wenzelm@29735:   fashion.  Thus we may reason in forward mode, feeding intermediate
wenzelm@29735:   results into rules selected from the context.  The course of
wenzelm@29735:   reasoning is organized by maintaining a secondary fact called
wenzelm@29735:   ``@{fact calculation}'', apart from the primary ``@{fact this}''
wenzelm@29735:   already provided by the Isar primitives.  In the definitions below,
wenzelm@29735:   @{attribute OF} refers to @{inference resolution}
wenzelm@29735:   (\secref{sec:framework-resolution}) with multiple rule arguments,
wenzelm@29735:   and @{text "trans"} represents to a suitable rule from the context:
wenzelm@29729: 
wenzelm@29729:   \begin{matharray}{rcl}
wenzelm@29729:     @{command "also"}@{text "\<^sub>0"} & \equiv & @{command "note"}~@{text "calculation = this"} \\
wenzelm@29729:     @{command "also"}@{text "\<^sub>n\<^sub>+\<^sub>1"} & \equiv & @{command "note"}~@{text "calculation = trans [OF calculation this]"} \\[0.5ex]
wenzelm@29729:     @{command "finally"} & \equiv & @{command "also"}~@{command "from"}~@{text calculation} \\
wenzelm@29729:   \end{matharray}
wenzelm@29729: 
wenzelm@29729:   \noindent The start of a calculation is determined implicitly in the
wenzelm@29729:   text: here @{command also} sets @{fact calculation} to the current
wenzelm@29729:   result; any subsequent occurrence will update @{fact calculation} by
wenzelm@29729:   combination with the next result and a transitivity rule.  The
wenzelm@29729:   calculational sequence is concluded via @{command finally}, where
wenzelm@29729:   the final result is exposed for use in a concluding claim.
wenzelm@29729: 
wenzelm@29729:   Here is a canonical proof pattern, using @{command have} to
wenzelm@29729:   establish the intermediate results:
wenzelm@58618: \<close>
wenzelm@29729: 
wenzelm@29729: (*<*)
wenzelm@40964: notepad
wenzelm@40964: begin
wenzelm@29729: (*>*)
wenzelm@29729:   have "a = b" sorry
wenzelm@29729:   also have "\<dots> = c" sorry
wenzelm@29729:   also have "\<dots> = d" sorry
wenzelm@29729:   finally have "a = d" .
wenzelm@29729: (*<*)
wenzelm@40964: end
wenzelm@29729: (*>*)
wenzelm@29729: 
wenzelm@58618: text \<open>
wenzelm@29729:   \noindent The term ``@{text "\<dots>"}'' above is a special abbreviation
wenzelm@29729:   provided by the Isabelle/Isar syntax layer: it statically refers to
wenzelm@29729:   the right-hand side argument of the previous statement given in the
wenzelm@29729:   text.  Thus it happens to coincide with relevant sub-expressions in
wenzelm@29729:   the calculational chain, but the exact correspondence is dependent
wenzelm@29729:   on the transitivity rules being involved.
wenzelm@29729: 
wenzelm@29729:   \medskip Symmetry rules such as @{prop "x = y \<Longrightarrow> y = x"} are like
wenzelm@29729:   transitivities with only one premise.  Isar maintains a separate
wenzelm@29729:   rule collection declared via the @{attribute sym} attribute, to be
wenzelm@29729:   used in fact expressions ``@{text "a [symmetric]"}'', or single-step
wenzelm@29729:   proofs ``@{command assume}~@{text "x = y"}~@{command then}~@{command
wenzelm@29729:   have}~@{text "y = x"}~@{command ".."}''.
wenzelm@58618: \<close>
wenzelm@29729: 
wenzelm@29742: end