doc-src/IsarRef/Thy/Framework.thy

removed some old material (inactive since 2002/2003);

theory Framework
imports Base Main
begin

chapter {* The Isabelle/Isar Framework \label{ch:isar-framework} *}

text {*
  Isabelle/Isar
  \cite{Wenzel:1999:TPHOL,Wenzel-PhD,Nipkow-TYPES02,Wenzel-Paulson:2006,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,Rudnicki:1992:MizarOverview,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.\
  @{text "\<lambda>"}-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,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 (@{text "\<and>"}, @{text "\<or>"}, @{text "\<forall>"},
  @{text "\<exists>"}, etc.), only the resulting reasoning principles are
  relevant to the user.  There are similar rules available for
  set-theory operators (@{text "\<inter>"}, @{text "\<union>"}, @{text "\<Inter>"}, @{text
  "\<Union>"}, 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 @{text "\<inter>"}-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.
*}

text_raw {*\medskip\begin{minipage}{0.6\textwidth}*}

(*<*)
notepad
begin
(*>*)
    assume "x \<in> A" and "x \<in> B"
    then have "x \<in> A \<inter> B" ..
(*<*)
end
(*>*)

text_raw {*\end{minipage}\begin{minipage}{0.4\textwidth}*}

text {*
  \infer{@{prop "x \<in> A \<inter> B"}}{@{prop "x \<in> A"} & @{prop "x \<in> B"}}
*}

text_raw {*\end{minipage}*}

text {*
  \medskip\noindent 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:
*}

(*<*)
notepad
begin
(*>*)
    assume "x \<in> A" and "x \<in> B"
    then have "x \<in> A \<inter> B" by (rule IntI)
(*<*)
end
(*>*)

text {*
  \noindent The format of the @{text "\<inter>"}-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:
*}

text_raw {*\medskip\begin{minipage}{0.6\textwidth}*}

(*<*)
notepad
begin
(*>*)
    have "x \<in> \<Inter>\<A>"
    proof
      fix A
      assume "A \<in> \<A>"
      show "x \<in> A" sorry %noproof
    qed
(*<*)
end
(*>*)

text_raw {*\end{minipage}\begin{minipage}{0.4\textwidth}*}

text {*
  \infer{@{prop "x \<in> \<Inter>\<A>"}}{\infer*{@{prop "x \<in> A"}}{@{text "[A][A \<in> \<A>]"}}}
*}

text_raw {*\end{minipage}*}

text {*
  \medskip\noindent 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 spelt out more
  explicitly as ``@{command proof}~@{text "(rule InterI)"}''.  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 @{text "\<exists>"} and @{text "\<and>"} 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:
*}

text_raw {*\medskip\begin{minipage}{0.6\textwidth}*}

(*<*)
notepad
begin
(*>*)
    assume "x \<in> \<Union>\<A>"
    then have C
    proof
      fix A
      assume "x \<in> A" and "A \<in> \<A>"
      show C sorry %noproof
    qed
(*<*)
end
(*>*)

text_raw {*\end{minipage}\begin{minipage}{0.4\textwidth}*}

text {*
  \infer{@{prop "C"}}{@{prop "x \<in> \<Union>\<A>"} & \infer*{@{prop "C"}~}{@{text "[A][x \<in> A, A \<in> \<A>]"}}}
*}

text_raw {*\end{minipage}*}

text {*
  \medskip\noindent 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:
*}

(*<*)
notepad
begin
(*>*)
    assume "x \<in> \<Union>\<A>"
    then obtain A where "x \<in> A" and "A \<in> \<A>" ..
(*<*)
end
(*>*)

text {*
  \noindent 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.
*}


section {* The Pure framework \label{sec:framework-pure} *}

text {*
  The Pure logic \cite{paulson-found,paulson700} is an intuitionistic
  fragment of higher-order logic \cite{church40}.  In type-theoretic
  parlance, there are three levels of @{text "\<lambda>"}-calculus with
  corresponding arrows @{text "\<Rightarrow>"}/@{text "\<And>"}/@{text "\<Longrightarrow>"}:

  \medskip
  \begin{tabular}{ll}
  @{text "\<alpha> \<Rightarrow> \<beta>"} & syntactic function space (terms depending on terms) \\
  @{text "\<And>x. B(x)"} & universal quantification (proofs depending on terms) \\
  @{text "A \<Longrightarrow> B"} & implication (proofs depending on proofs) \\
  \end{tabular}
  \medskip

  \noindent Here only the types of syntactic terms, and the
  propositions of proof terms have been shown.  The @{text
  "\<lambda>"}-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{proof
  irrelevance}.

  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 @{text "\<And>"} and @{text "\<Longrightarrow>"}.
  Combining such rule statements may involve higher-order unification
  \cite{paulson-natural}.
*}


subsection {* Primitive inferences *}

text {*
  Term syntax provides explicit notation for abstraction @{text "\<lambda>x ::
  \<alpha>. b(x)"} and application @{text "b a"}, while types are usually
  implicit thanks to type-inference; terms of type @{text "prop"} are
  called propositions.  Logical statements are composed via @{text "\<And>x
  :: \<alpha>. B(x)"} and @{text "A \<Longrightarrow> B"}.  Primitive reasoning operates on
  judgments of the form @{text "\<Gamma> \<turnstile> \<phi>"}, with standard introduction
  and elimination rules for @{text "\<And>"} and @{text "\<Longrightarrow>"} that refer to
  fixed parameters @{text "x\<^isub>1, \<dots>, x\<^isub>m"} and hypotheses
  @{text "A\<^isub>1, \<dots>, A\<^isub>n"} from the context @{text "\<Gamma>"};
  the corresponding proof terms are left implicit.  The subsequent
  inference rules define @{text "\<Gamma> \<turnstile> \<phi>"} inductively, relative to a
  collection of axioms:

  \[
  \infer{@{text "\<turnstile> A"}}{(@{text "A"} \text{~axiom})}
  \qquad
  \infer{@{text "A \<turnstile> A"}}{}
  \]

  \[
  \infer{@{text "\<Gamma> \<turnstile> \<And>x. B(x)"}}{@{text "\<Gamma> \<turnstile> B(x)"} & @{text "x \<notin> \<Gamma>"}}
  \qquad
  \infer{@{text "\<Gamma> \<turnstile> B(a)"}}{@{text "\<Gamma> \<turnstile> \<And>x. B(x)"}}
  \]

  \[
  \infer{@{text "\<Gamma> - A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}
  \qquad
  \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"}}
  \]

  Furthermore, Pure provides a built-in equality @{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow>
  prop"} with axioms for reflexivity, substitution, extensionality,
  and @{text "\<alpha>\<beta>\<eta>"}-conversion on @{text "\<lambda>"}-terms.

  \medskip An object-logic introduces another layer on top of Pure,
  e.g.\ with types @{text "i"} for individuals and @{text "o"} for
  propositions, term constants @{text "Trueprop :: o \<Rightarrow> prop"} as
  (implicit) derivability judgment and connectives like @{text "\<and> :: o
  \<Rightarrow> o \<Rightarrow> o"} or @{text "\<forall> :: (i \<Rightarrow> o) \<Rightarrow> o"}, and axioms for object-level
  rules such as @{text "conjI: A \<Longrightarrow> B \<Longrightarrow> A \<and> B"} or @{text "allI: (\<And>x. B
  x) \<Longrightarrow> \<forall>x. B x"}.  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.
*}


subsection {* Reasoning with rules \label{sec:framework-resolution} *}

text {*
  Primitive inferences mostly serve foundational purposes.  The main
  reasoning mechanisms of Pure operate on nested natural deduction
  rules expressed as formulae, using @{text "\<And>"} to bind local
  parameters and @{text "\<Longrightarrow>"} to express entailment.  Multiple
  parameters and premises are represented by repeating these
  connectives in a right-associative manner.

  Since @{text "\<And>"} and @{text "\<Longrightarrow>"} 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{Hereditary Harrop Formula} \cite{Miller:1991} which is of the
  form @{text "\<And>x\<^isub>1 \<dots> x\<^isub>m. H\<^isub>1 \<Longrightarrow> \<dots> H\<^isub>n \<Longrightarrow>
  A"} for @{text "m, n \<ge> 0"}, and @{text "A"} atomic, and @{text
  "H\<^isub>1, \<dots>, H\<^isub>n"} being recursively of the same format.
  Following the convention that outermost quantifiers are implicit,
  Horn clauses @{text "A\<^isub>1 \<Longrightarrow> \<dots> A\<^isub>n \<Longrightarrow> A"} are a special
  case of this.

  For example, @{text "\<inter>"}-introduction rule encountered before is
  represented as a Pure theorem as follows:
  \[
  @{text "IntI:"}~@{prop "x \<in> A \<Longrightarrow> x \<in> B \<Longrightarrow> x \<in> A \<inter> B"}
  \]

  \noindent This is a plain Horn clause, since no further nesting on
  the left is involved.  The general @{text "\<Inter>"}-introduction
  corresponds to a Hereditary Harrop Formula with one additional level
  of nesting:
  \[
  @{text "InterI:"}~@{prop "(\<And>A. A \<in> \<A> \<Longrightarrow> x \<in> A) \<Longrightarrow> x \<in> \<Inter>\<A>"}
  \]

  \medskip Goals are also represented as rules: @{text "A\<^isub>1 \<Longrightarrow>
  \<dots> A\<^isub>n \<Longrightarrow> C"} states that the sub-goals @{text "A\<^isub>1, \<dots>,
  A\<^isub>n"} entail the result @{text "C"}; for @{text "n = 0"} the
  goal is finished.  To allow @{text "C"} being a rule statement
  itself, we introduce the protective marker @{text "# :: prop \<Rightarrow>
  prop"}, 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})]{@{text "C \<Longrightarrow> #C"}}{} &
  \infer[(@{inference_def finish})]{@{text C}}{@{text "#C"}}
  \end{array}
  \]

  \noindent 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 @{text "\<^vec>x"} stands for @{text
  "x\<^isub>1, \<dots>, x\<^isub>n"} (@{text "n \<ge> 0"}).

  \[
  \infer[(@{inference_def resolution})]
  {@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> \<^vec>A (\<^vec>a \<^vec>x))\<vartheta> \<Longrightarrow> C\<vartheta>"}}
  {\begin{tabular}{rl}
    @{text "rule:"} &
    @{text "\<^vec>A \<^vec>a \<Longrightarrow> B \<^vec>a"} \\
    @{text "goal:"} &
    @{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> B' \<^vec>x) \<Longrightarrow> C"} \\
    @{text "goal unifier:"} &
    @{text "(\<lambda>\<^vec>x. B (\<^vec>a \<^vec>x))\<vartheta> = B'\<vartheta>"} \\
   \end{tabular}}
  \]

  \medskip

  \[
  \infer[(@{inference_def assumption})]{@{text "C\<vartheta>"}}
  {\begin{tabular}{rl}
    @{text "goal:"} &
    @{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> A \<^vec>x) \<Longrightarrow> C"} \\
    @{text "assm unifier:"} & @{text "A\<vartheta> = H\<^sub>i\<vartheta>"}~~\text{(for some~@{text "H\<^sub>i"})} \\
   \end{tabular}}
  \]

  The following trace illustrates goal-oriented reasoning in
  Isabelle/Pure:

  {\footnotesize
  \medskip
  \begin{tabular}{r@ {\quad}l}
  @{text "(A \<and> B \<Longrightarrow> B \<and> A) \<Longrightarrow> #(A \<and> B \<Longrightarrow> B \<and> A)"} & @{text "(init)"} \\
  @{text "(A \<and> B \<Longrightarrow> B) \<Longrightarrow> (A \<and> B \<Longrightarrow> A) \<Longrightarrow> #\<dots>"} & @{text "(resolution B \<Longrightarrow> A \<Longrightarrow> B \<and> A)"} \\
  @{text "(A \<and> B \<Longrightarrow> A \<and> B) \<Longrightarrow> (A \<and> B \<Longrightarrow> A) \<Longrightarrow> #\<dots>"} & @{text "(resolution A \<and> B \<Longrightarrow> B)"} \\
  @{text "(A \<and> B \<Longrightarrow> A) \<Longrightarrow> #\<dots>"} & @{text "(assumption)"} \\
  @{text "(A \<and> B \<Longrightarrow> A \<and> B) \<Longrightarrow> #\<dots>"} & @{text "(resolution A \<and> B \<Longrightarrow> A)"} \\
  @{text "#\<dots>"} & @{text "(assumption)"} \\
  @{text "A \<and> B \<Longrightarrow> B \<and> A"} & @{text "(finish)"} \\
  \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
  @{text "#"}:

  \[
  \infer[(@{inference refinement})]
  {@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> \<^vec>G' (\<^vec>a \<^vec>x))\<vartheta> \<Longrightarrow> C\<vartheta>"}}
  {\begin{tabular}{rl}
    @{text "sub\<hyphen>proof:"} &
    @{text "\<^vec>G \<^vec>a \<Longrightarrow> B \<^vec>a"} \\
    @{text "goal:"} &
    @{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> B' \<^vec>x) \<Longrightarrow> C"} \\
    @{text "goal unifier:"} &
    @{text "(\<lambda>\<^vec>x. B (\<^vec>a \<^vec>x))\<vartheta> = B'\<vartheta>"} \\
    @{text "assm unifiers:"} &
    @{text "(\<lambda>\<^vec>x. G\<^sub>j (\<^vec>a \<^vec>x))\<vartheta> = #H\<^sub>i\<vartheta>"} \\
    & \quad (for each marked @{text "G\<^sub>j"} some @{text "#H\<^sub>i"}) \\
   \end{tabular}}
  \]

  \noindent Here the @{text "sub\<hyphen>proof"} 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 @{text "G"} 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.
*}


section {* The Isar proof language \label{sec:framework-isar} *}

text {*
  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 @{text "proof"}), which is embedded into theory
  specification elements such as @{command theorem}; see also
  \secref{sec:framework-stmt} for the separate category @{text
  "statement"}.

  \medskip
  \begin{tabular}{rcl}