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

misc cleanup;

%
\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{Local variables%
}
\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 -> 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{Schematic polymorphism%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
FIXME%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Assumptions%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
FIXME%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Conclusions%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
FIXME%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Structured proofs \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: