doc-src/IsarImplementation/Thy/document/proof.tex

tuned;

%
\begin{isabellebody}%
\def\isabellecontext{proof}%
%
\isadelimtheory
\isanewline
\isanewline
\isanewline
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ {\isachardoublequoteopen}proof{\isachardoublequoteclose}\ \isakeyword{imports}\ base\ \isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isamarkupchapter{Structured proofs%
}
\isamarkuptrue%
%
\isamarkupsection{Variables and schematic polymorphism%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
FIXME%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
  \indexml{Variable.declare-term}\verb|Variable.declare_term: term -> Proof.context -> Proof.context| \\
  \indexml{Variable.add-fixes}\verb|Variable.add_fixes: string list -> Proof.context -> string list * Proof.context| \\
  \indexml{Variable.import}\verb|Variable.import: bool ->|\isasep\isanewline%
\verb|  thm list -> Proof.context -> ((ctyp list * cterm list) * thm list) * Proof.context| \\
  \indexml{Variable.export}\verb|Variable.export: Proof.context -> Proof.context -> thm list -> thm list| \\
  \indexml{Variable.trade}\verb|Variable.trade: Proof.context -> (thm list -> thm list) -> thm list -> thm list| \\
  \indexml{Variable.polymorphic}\verb|Variable.polymorphic: Proof.context -> term list -> term list| \\
  \end{mldecls}

  \begin{description}

  \item \verb|Variable.declare_term|~\isa{t\ ctxt} declares term
  \isa{t} to belong to the context.  This fixes free type
  variables, but not term variables.  Constraints for type and term
  variables are declared uniformly.

  \item \verb|Variable.add_fixes|~\isa{xs\ ctxt} fixes term
  variables \isa{xs} and returns the internal names of the
  resulting Skolem constants.  Note that term fixes refer to
  \emph{all} type instances that may occur in the future.

  \item \verb|Variable.invent_fixes| is similar to \verb|Variable.add_fixes|, but the given names merely act as hints for
  internal fixes produced here.

  \item \verb|Variable.import|~\isa{open\ ths\ ctxt} augments the
  context by new fixes for the schematic type and term variables
  occurring in \isa{ths}.  The \isa{open} flag indicates
  whether the fixed names should be accessible to the user, otherwise
  internal names are chosen.

  \item \verb|Variable.export|~\isa{inner\ outer\ ths} generalizes
  fixed type and term variables in \isa{ths} according to the
  difference of the \isa{inner} and \isa{outer} context.  Note
  that type variables occurring in term variables are still fixed.

  \verb|Variable.export| essentially reverses the effect of \verb|Variable.import| (up to renaming of schematic variables.

  \item \verb|Variable.trade| composes \verb|Variable.import| and \verb|Variable.export|, i.e.\ it provides a view on facts with all
  variables being fixed in the current context.

  \item \verb|Variable.polymorphic|~\isa{ctxt\ ts} generalizes type
  variables in \isa{ts} as far as possible, even those occurring
  in fixed term variables.  This operation essentially reverses the
  default policy of type-inference to introduce local polymorphism as
  fixed types.

  \end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\begin{isamarkuptext}%
FIXME%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Assumptions%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
An \emph{assumption} is a proposition that it is postulated in the
  current context.  Local conclusions may use assumptions as
  additional facts, but this imposes implicit hypotheses that weaken
  the overall statement.

  Assumptions are restricted to fixed non-schematic statements, all
  generality needs to be expressed by explicit quantifiers.
  Nevertheless, the result will be in HHF normal form with outermost
  quantifiers stripped.  For example, by assuming \isa{{\isasymAnd}x\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}{\isachardot}\ P\ x} we get \isa{{\isasymAnd}x\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}{\isachardot}\ P\ x\ {\isasymturnstile}\ P\ {\isacharquery}x} for arbitrary \isa{{\isacharquery}x}
  of the fixed type \isa{{\isasymalpha}}.  Local derivations accumulate more
  and more explicit references to hypotheses: \isa{A\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ A\isactrlisub n\ {\isasymturnstile}\ B} where \isa{A\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ A\isactrlisub n} needs to
  be covered by the assumptions of the current context.

  \medskip The \isa{add{\isacharunderscore}assms} operation augments the context by
  local assumptions, which are parameterized by an arbitrary \isa{export} rule (see below).

  The \isa{export} operation moves facts from a (larger) inner
  context into a (smaller) outer context, by discharging the
  difference of the assumptions as specified by the associated export
  rules.  Note that the discharged portion is determined by the
  difference contexts, not the facts being exported!  There is a
  separate flag to indicate a goal context, where the result is meant
  to refine an enclosing sub-goal of a structured proof state (cf.\
  \secref{sec:isar-proof-state}).

  \medskip The most basic export rule discharges assumptions directly
  by means of the \isa{{\isasymLongrightarrow}} introduction rule:
  \[
  \infer[(\isa{{\isasymLongrightarrow}{\isacharunderscore}intro})]{\isa{{\isasymGamma}\ {\isacharbackslash}\ A\ {\isasymturnstile}\ A\ {\isasymLongrightarrow}\ B}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B}}
  \]

  The variant for goal refinements marks the newly introduced
  premises, which causes the builtin goal refinement scheme of Isar to
  enforce unification with local premises within the goal:
  \[
  \infer[(\isa{{\isacharhash}{\isasymLongrightarrow}{\isacharunderscore}intro})]{\isa{{\isasymGamma}\ {\isacharbackslash}\ A\ {\isasymturnstile}\ {\isacharhash}A\ {\isasymLongrightarrow}\ B}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B}}
  \]

  \medskip Alternative assumptions may perform arbitrary
  transformations on export, as long as a particular portion of
  hypotheses is removed from the given facts.  For example, a local
  definition works by fixing \isa{x} and assuming \isa{x\ {\isasymequiv}\ t},
  with the following export rule to reverse the effect:
  \[
  \infer{\isa{{\isasymGamma}\ {\isacharbackslash}\ x\ {\isasymequiv}\ t\ {\isasymturnstile}\ B\ t}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B\ x}}
  \]

  \medskip The general concept supports block-structured reasoning
  nicely, with arbitrary mechanisms for introducing local assumptions.
  The common reasoning pattern is as follows:

  \medskip
  \begin{tabular}{l}
  \isa{add{\isacharunderscore}assms\ e\isactrlisub {\isadigit{1}}\ A\isactrlisub {\isadigit{1}}} \\
  \isa{{\isasymdots}} \\
  \isa{add{\isacharunderscore}assms\ e\isactrlisub n\ A\isactrlisub n} \\
  \isa{export} \\
  \end{tabular}
  \medskip

  \noindent The final \isa{export} will turn any fact \isa{A\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ A\isactrlisub n\ {\isasymturnstile}\ B} into some \isa{{\isasymturnstile}\ B{\isacharprime}}, by
  applying the export rules \isa{e\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ e\isactrlisub n}
  inside-out.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
  \indexmltype{Assumption.export}\verb|type Assumption.export| \\
  \indexml{Assumption.assume}\verb|Assumption.assume: cterm -> thm| \\
  \indexml{Assumption.add-assms}\verb|Assumption.add_assms: Assumption.export ->|\isasep\isanewline%
\verb|  cterm list -> Proof.context -> thm list * Proof.context| \\
  \indexml{Assumption.add-assumes}\verb|Assumption.add_assumes: |\isasep\isanewline%
\verb|  cterm list -> Proof.context -> thm list * Proof.context| \\
  \indexml{Assumption.export}\verb|Assumption.export: bool -> Proof.context -> Proof.context -> thm -> thm| \\
  \end{mldecls}

  \begin{description}

  \item \verb|Assumption.export| represents arbitrary export
  rules, which is any function of type \verb|bool -> cterm list -> thm -> thm|,
  where the \verb|bool| indicates goal mode, and the \verb|cterm list| the collection of assumptions to be discharged
  simultaneously.

  \item \verb|Assumption.assume|~\isa{A} turns proposition \isa{A} into a raw assumption \isa{A\ {\isasymturnstile}\ A{\isacharprime}}, where the conclusion
  \isa{A{\isacharprime}} is in HHF normal form.

  \item \verb|Assumption.add_assms|~\isa{e\ As} augments the context
  by assumptions \isa{As} with export rule \isa{e}.  The
  resulting facts are hypothetical theorems as produced by \verb|Assumption.assume|.

  \item \verb|Assumption.add_assumes|~\isa{As} is a special case of
  \verb|Assumption.add_assms| where the export rule performs \isa{{\isasymLongrightarrow}{\isacharunderscore}intro} or \isa{{\isacharhash}{\isasymLongrightarrow}{\isacharunderscore}intro}, depending on goal mode.

  \item \verb|Assumption.export|~\isa{is{\isacharunderscore}goal\ inner\ outer\ th}
  exports result \isa{th} from the the \isa{inner} context
  back into the \isa{outer} one; \isa{is{\isacharunderscore}goal\ {\isacharequal}\ true} means
  this is a goal context.  The result is in HHF normal form.  Note
  that \verb|ProofContext.export| combines \verb|Variable.export|
  and \verb|Assumption.export| in the canonical way.

  \end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\isamarkupsection{Conclusions%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
FIXME%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Proof states \label{sec:isar-proof-state}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
FIXME

\glossary{Proof state}{The whole configuration of a structured proof,
consisting of a \seeglossary{proof context} and an optional
\seeglossary{structured goal}.  Internally, an Isar proof state is
organized as a stack to accomodate block structure of proof texts.
For historical reasons, a low-level \seeglossary{tactical goal} is
occasionally called ``proof state'' as well.}

\glossary{Structured goal}{FIXME}

\glossary{Goal}{See \seeglossary{tactical goal} or \seeglossary{structured goal}. \norefpage}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Proof methods%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
FIXME%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Attributes%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
FIXME ?!%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\isanewline
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: