--- a/doc-src/IsarRef/Thy/document/pure.tex Mon Jun 02 22:50:27 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/pure.tex Mon Jun 02 22:50:29 2008 +0200
@@ -24,629 +24,6 @@
}
\isamarkuptrue%
%
-\begin{isamarkuptext}%
-Subsequently, we introduce the main part of Pure theory and proof
- commands, together with fundamental proof methods and attributes.
- \Chref{ch:gen-tools} describes further Isar elements provided by
- generic tools and packages (such as the Simplifier) that are either
- part of Pure Isabelle or pre-installed in most object logics.
- Specific language elements introduced by the major object-logics are
- described in \chref{ch:hol} (Isabelle/HOL), \chref{ch:holcf}
- (Isabelle/HOLCF), and \chref{ch:zf} (Isabelle/ZF). Nevertheless,
- examples given in the generic parts will usually refer to
- Isabelle/HOL as well.
-
- \medskip Isar commands may be either \emph{proper} document
- constructors, or \emph{improper commands}. Some proof methods and
- attributes introduced later are classified as improper as well.
- Improper Isar language elements, which are subsequently marked by
- ``\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}'', are often helpful when developing proof
- documents, while their use is discouraged for the final
- human-readable outcome. Typical examples are diagnostic commands
- that print terms or theorems according to the current context; other
- commands emulate old-style tactical theorem proving.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsection{Theory commands%
-}
-\isamarkuptrue%
-%
-\isamarkupsubsection{Markup commands \label{sec:markup-thy}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcl}
- \indexdef{}{command}{chapter}\hypertarget{command.chapter}{\hyperlink{command.chapter}{\mbox{\isa{\isacommand{chapter}}}}} & : & \isarkeep{local{\dsh}theory} \\
- \indexdef{}{command}{section}\hypertarget{command.section}{\hyperlink{command.section}{\mbox{\isa{\isacommand{section}}}}} & : & \isarkeep{local{\dsh}theory} \\
- \indexdef{}{command}{subsection}\hypertarget{command.subsection}{\hyperlink{command.subsection}{\mbox{\isa{\isacommand{subsection}}}}} & : & \isarkeep{local{\dsh}theory} \\
- \indexdef{}{command}{subsubsection}\hypertarget{command.subsubsection}{\hyperlink{command.subsubsection}{\mbox{\isa{\isacommand{subsubsection}}}}} & : & \isarkeep{local{\dsh}theory} \\
- \indexdef{}{command}{text}\hypertarget{command.text}{\hyperlink{command.text}{\mbox{\isa{\isacommand{text}}}}} & : & \isarkeep{local{\dsh}theory} \\
- \indexdef{}{command}{text\_raw}\hypertarget{command.text-raw}{\hyperlink{command.text-raw}{\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}}}} & : & \isarkeep{local{\dsh}theory} \\
- \end{matharray}
-
- Apart from formal comments (see \secref{sec:comments}), markup
- commands provide a structured way to insert text into the document
- generated from a theory (see \cite{isabelle-sys} for more
- information on Isabelle's document preparation tools).
-
- \begin{rail}
- ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') target? text
- ;
- 'text\_raw' text
- ;
- \end{rail}
-
- \begin{descr}
-
- \item [\hyperlink{command.chapter}{\mbox{\isa{\isacommand{chapter}}}}, \hyperlink{command.section}{\mbox{\isa{\isacommand{section}}}}, \hyperlink{command.subsection}{\mbox{\isa{\isacommand{subsection}}}}, and \hyperlink{command.subsubsection}{\mbox{\isa{\isacommand{subsubsection}}}}] mark chapter and
- section headings.
-
- \item [\hyperlink{command.text}{\mbox{\isa{\isacommand{text}}}}] specifies paragraphs of plain text.
-
- \item [\hyperlink{command.text-raw}{\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}}}] inserts {\LaTeX} source into the
- output, without additional markup. Thus the full range of document
- manipulations becomes available.
-
- \end{descr}
-
- The \isa{{\isachardoublequote}text{\isachardoublequote}} argument of these markup commands (except for
- \hyperlink{command.text-raw}{\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}}}) may contain references to formal entities
- (``antiquotations'', see also \secref{sec:antiq}). These are
- interpreted in the present theory context, or the named \isa{{\isachardoublequote}target{\isachardoublequote}}.
-
- Any of these markup elements corresponds to a {\LaTeX} command with
- the name prefixed by \verb|\isamarkup|. For the sectioning
- commands this is a plain macro with a single argument, e.g.\
- \verb|\isamarkupchapter{|\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}\verb|}| for
- \hyperlink{command.chapter}{\mbox{\isa{\isacommand{chapter}}}}. The \hyperlink{command.text}{\mbox{\isa{\isacommand{text}}}} markup results in a
- {\LaTeX} environment \verb|\begin{isamarkuptext}| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|\end{isamarkuptext}|, while \hyperlink{command.text-raw}{\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}}}
- causes the text to be inserted directly into the {\LaTeX} source.
-
- \medskip Additional markup commands are available for proofs (see
- \secref{sec:markup-prf}). Also note that the \indexref{}{command}{header}\hyperlink{command.header}{\mbox{\isa{\isacommand{header}}}} declaration (see \secref{sec:begin-thy}) admits to insert
- section markup just preceding the actual theory definition.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Type classes and sorts \label{sec:classes}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcll}
- \indexdef{}{command}{classes}\hypertarget{command.classes}{\hyperlink{command.classes}{\mbox{\isa{\isacommand{classes}}}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{classrel}\hypertarget{command.classrel}{\hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}} & : & \isartrans{theory}{theory} & (axiomatic!) \\
- \indexdef{}{command}{defaultsort}\hypertarget{command.defaultsort}{\hyperlink{command.defaultsort}{\mbox{\isa{\isacommand{defaultsort}}}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{class\_deps}\hypertarget{command.class-deps}{\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}}} & : & \isarkeep{theory~|~proof} \\
- \end{matharray}
-
- \begin{rail}
- 'classes' (classdecl +)
- ;
- 'classrel' (nameref ('<' | subseteq) nameref + 'and')
- ;
- 'defaultsort' sort
- ;
- \end{rail}
-
- \begin{descr}
-
- \item [\hyperlink{command.classes}{\mbox{\isa{\isacommand{classes}}}}~\isa{{\isachardoublequote}c\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n{\isachardoublequote}}]
- declares class \isa{c} to be a subclass of existing classes \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n{\isachardoublequote}}. Cyclic class structures are not permitted.
-
- \item [\hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}}] states
- subclass relations between existing classes \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}{\isachardoublequote}} and
- \isa{{\isachardoublequote}c\isactrlsub {\isadigit{2}}{\isachardoublequote}}. This is done axiomatically! The \indexref{}{command}{instance}\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} command (see \secref{sec:axclass}) provides a way to
- introduce proven class relations.
-
- \item [\hyperlink{command.defaultsort}{\mbox{\isa{\isacommand{defaultsort}}}}~\isa{s}] makes sort \isa{s} the
- new default sort for any type variables given without sort
- constraints. Usually, the default sort would be only changed when
- defining a new object-logic.
-
- \item [\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}}] visualizes the subclass relation,
- using Isabelle's graph browser tool (see also \cite{isabelle-sys}).
-
- \end{descr}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Primitive types and type abbreviations \label{sec:types-pure}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcll}
- \indexdef{}{command}{types}\hypertarget{command.types}{\hyperlink{command.types}{\mbox{\isa{\isacommand{types}}}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{typedecl}\hypertarget{command.typedecl}{\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{nonterminals}\hypertarget{command.nonterminals}{\hyperlink{command.nonterminals}{\mbox{\isa{\isacommand{nonterminals}}}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{arities}\hypertarget{command.arities}{\hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}} & : & \isartrans{theory}{theory} & (axiomatic!) \\
- \end{matharray}
-
- \begin{rail}
- 'types' (typespec '=' type infix? +)
- ;
- 'typedecl' typespec infix?
- ;
- 'nonterminals' (name +)
- ;
- 'arities' (nameref '::' arity +)
- ;
- \end{rail}
-
- \begin{descr}
-
- \item [\hyperlink{command.types}{\mbox{\isa{\isacommand{types}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t\ {\isacharequal}\ {\isasymtau}{\isachardoublequote}}]
- introduces \emph{type synonym} \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}}
- for existing type \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}}. Unlike actual type definitions, as
- are available in Isabelle/HOL for example, type synonyms are just
- purely syntactic abbreviations without any logical significance.
- Internally, type synonyms are fully expanded.
-
- \item [\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}}]
- declares a new type constructor \isa{t}, intended as an actual
- logical type (of the object-logic, if available).
-
- \item [\hyperlink{command.nonterminals}{\mbox{\isa{\isacommand{nonterminals}}}}~\isa{c}] declares type
- constructors \isa{c} (without arguments) to act as purely
- syntactic types, i.e.\ nonterminal symbols of Isabelle's inner
- syntax of terms or types.
-
- \item [\hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}\ s{\isachardoublequote}}] augments Isabelle's order-sorted signature of types by new type
- constructor arities. This is done axiomatically! The \indexref{}{command}{instance}\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} command (see \S\ref{sec:axclass}) provides a way to
- introduce proven type arities.
-
- \end{descr}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Primitive constants and definitions \label{sec:consts}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Definitions essentially express abbreviations within the logic. The
- simplest form of a definition is \isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\ {\isasymequiv}\ t{\isachardoublequote}}, where \isa{c} is a newly declared constant. Isabelle also allows derived forms
- where the arguments of \isa{c} appear on the left, abbreviating a
- prefix of \isa{{\isasymlambda}}-abstractions, e.g.\ \isa{{\isachardoublequote}c\ {\isasymequiv}\ {\isasymlambda}x\ y{\isachardot}\ t{\isachardoublequote}} may be
- written more conveniently as \isa{{\isachardoublequote}c\ x\ y\ {\isasymequiv}\ t{\isachardoublequote}}. Moreover,
- definitions may be weakened by adding arbitrary pre-conditions:
- \isa{{\isachardoublequote}A\ {\isasymLongrightarrow}\ c\ x\ y\ {\isasymequiv}\ t{\isachardoublequote}}.
-
- \medskip The built-in well-formedness conditions for definitional
- specifications are:
-
- \begin{itemize}
-
- \item Arguments (on the left-hand side) must be distinct variables.
-
- \item All variables on the right-hand side must also appear on the
- left-hand side.
-
- \item All type variables on the right-hand side must also appear on
- the left-hand side; this prohibits \isa{{\isachardoublequote}{\isadigit{0}}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymequiv}\ length\ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ list{\isacharparenright}{\isachardoublequote}} for example.
-
- \item The definition must not be recursive. Most object-logics
- provide definitional principles that can be used to express
- recursion safely.
-
- \end{itemize}
-
- Overloading means that a constant being declared as \isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ decl{\isachardoublequote}} may be defined separately on type instances \isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}{\isasymbeta}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymbeta}\isactrlsub n{\isacharparenright}\ t\ decl{\isachardoublequote}} for each type constructor \isa{t}. The right-hand side may mention overloaded constants
- recursively at type instances corresponding to the immediate
- argument types \isa{{\isachardoublequote}{\isasymbeta}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymbeta}\isactrlsub n{\isachardoublequote}}. Incomplete
- specification patterns impose global constraints on all occurrences,
- e.g.\ \isa{{\isachardoublequote}d\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymtimes}\ {\isasymalpha}{\isachardoublequote}} on the left-hand side means that all
- corresponding occurrences on some right-hand side need to be an
- instance of this, general \isa{{\isachardoublequote}d\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymtimes}\ {\isasymbeta}{\isachardoublequote}} will be disallowed.
-
- \begin{matharray}{rcl}
- \indexdef{}{command}{consts}\hypertarget{command.consts}{\hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{defs}\hypertarget{command.defs}{\hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{constdefs}\hypertarget{command.constdefs}{\hyperlink{command.constdefs}{\mbox{\isa{\isacommand{constdefs}}}}} & : & \isartrans{theory}{theory} \\
- \end{matharray}
-
- \begin{rail}
- 'consts' ((name '::' type mixfix?) +)
- ;
- 'defs' ('(' 'unchecked'? 'overloaded'? ')')? \\ (axmdecl prop +)
- ;
- \end{rail}
-
- \begin{rail}
- 'constdefs' structs? (constdecl? constdef +)
- ;
-
- structs: '(' 'structure' (vars + 'and') ')'
- ;
- constdecl: ((name '::' type mixfix | name '::' type | name mixfix) 'where'?) | name 'where'
- ;
- constdef: thmdecl? prop
- ;
- \end{rail}
-
- \begin{descr}
-
- \item [\hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}~\isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}{\isachardoublequote}}] declares constant
- \isa{c} to have any instance of type scheme \isa{{\isasymsigma}}. The
- optional mixfix annotations may attach concrete syntax to the
- constants declared.
-
- \item [\hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}}~\isa{{\isachardoublequote}name{\isacharcolon}\ eqn{\isachardoublequote}}] introduces \isa{eqn}
- as a definitional axiom for some existing constant.
-
- The \isa{{\isachardoublequote}{\isacharparenleft}unchecked{\isacharparenright}{\isachardoublequote}} option disables global dependency checks
- for this definition, which is occasionally useful for exotic
- overloading. It is at the discretion of the user to avoid malformed
- theory specifications!
-
- The \isa{{\isachardoublequote}{\isacharparenleft}overloaded{\isacharparenright}{\isachardoublequote}} option declares definitions to be
- potentially overloaded. Unless this option is given, a warning
- message would be issued for any definitional equation with a more
- special type than that of the corresponding constant declaration.
-
- \item [\hyperlink{command.constdefs}{\mbox{\isa{\isacommand{constdefs}}}}] provides a streamlined combination of
- constants declarations and definitions: type-inference takes care of
- the most general typing of the given specification (the optional
- type constraint may refer to type-inference dummies ``\isa{{\isacharunderscore}}'' as usual). The resulting type declaration needs to agree with
- that of the specification; overloading is \emph{not} supported here!
-
- The constant name may be omitted altogether, if neither type nor
- syntax declarations are given. The canonical name of the
- definitional axiom for constant \isa{c} will be \isa{c{\isacharunderscore}def},
- unless specified otherwise. Also note that the given list of
- specifications is processed in a strictly sequential manner, with
- type-checking being performed independently.
-
- An optional initial context of \isa{{\isachardoublequote}{\isacharparenleft}structure{\isacharparenright}{\isachardoublequote}} declarations
- admits use of indexed syntax, using the special symbol \verb|\<index>| (printed as ``\isa{{\isachardoublequote}{\isasymindex}{\isachardoublequote}}''). The latter concept is
- particularly useful with locales (see also \S\ref{sec:locale}).
-
- \end{descr}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Syntax and translations \label{sec:syn-trans}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcl}
- \indexdef{}{command}{syntax}\hypertarget{command.syntax}{\hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{no\_syntax}\hypertarget{command.no-syntax}{\hyperlink{command.no-syntax}{\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{translations}\hypertarget{command.translations}{\hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{no\_translations}\hypertarget{command.no-translations}{\hyperlink{command.no-translations}{\mbox{\isa{\isacommand{no{\isacharunderscore}translations}}}}} & : & \isartrans{theory}{theory} \\
- \end{matharray}
-
- \begin{rail}
- ('syntax' | 'no\_syntax') mode? (constdecl +)
- ;
- ('translations' | 'no\_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
- ;
-
- mode: ('(' ( name | 'output' | name 'output' ) ')')
- ;
- transpat: ('(' nameref ')')? string
- ;
- \end{rail}
-
- \begin{descr}
-
- \item [\hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}}~\isa{{\isachardoublequote}{\isacharparenleft}mode{\isacharparenright}\ decls{\isachardoublequote}}] is similar to
- \hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}~\isa{decls}, except that the actual logical
- signature extension is omitted. Thus the context free grammar of
- Isabelle's inner syntax may be augmented in arbitrary ways,
- independently of the logic. The \isa{mode} argument refers to the
- print mode that the grammar rules belong; unless the \indexref{}{keyword}{output}\hyperlink{keyword.output}{\mbox{\isa{\isakeyword{output}}}} indicator is given, all productions are added both to the
- input and output grammar.
-
- \item [\hyperlink{command.no-syntax}{\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}}}~\isa{{\isachardoublequote}{\isacharparenleft}mode{\isacharparenright}\ decls{\isachardoublequote}}] removes
- grammar declarations (and translations) resulting from \isa{decls}, which are interpreted in the same manner as for \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} above.
-
- \item [\hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}~\isa{rules}] specifies syntactic
- translation rules (i.e.\ macros): parse~/ print rules (\isa{{\isachardoublequote}{\isasymrightleftharpoons}{\isachardoublequote}}),
- parse rules (\isa{{\isachardoublequote}{\isasymrightharpoonup}{\isachardoublequote}}), or print rules (\isa{{\isachardoublequote}{\isasymleftharpoondown}{\isachardoublequote}}).
- Translation patterns may be prefixed by the syntactic category to be
- used for parsing; the default is \isa{logic}.
-
- \item [\hyperlink{command.no-translations}{\mbox{\isa{\isacommand{no{\isacharunderscore}translations}}}}~\isa{rules}] removes syntactic
- translation rules, which are interpreted in the same manner as for
- \hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}} above.
-
- \end{descr}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Axioms and theorems \label{sec:axms-thms}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcll}
- \indexdef{}{command}{axioms}\hypertarget{command.axioms}{\hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}}} & : & \isartrans{theory}{theory} & (axiomatic!) \\
- \indexdef{}{command}{lemmas}\hypertarget{command.lemmas}{\hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}} & : & \isarkeep{local{\dsh}theory} \\
- \indexdef{}{command}{theorems}\hypertarget{command.theorems}{\hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}}} & : & isarkeep{local{\dsh}theory} \\
- \end{matharray}
-
- \begin{rail}
- 'axioms' (axmdecl prop +)
- ;
- ('lemmas' | 'theorems') target? (thmdef? thmrefs + 'and')
- ;
- \end{rail}
-
- \begin{descr}
-
- \item [\hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}}] introduces arbitrary
- statements as axioms of the meta-logic. In fact, axioms are
- ``axiomatic theorems'', and may be referred later just as any other
- theorem.
-
- Axioms are usually only introduced when declaring new logical
- systems. Everyday work is typically done the hard way, with proper
- definitions and proven theorems.
-
- \item [\hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}~\isa{{\isachardoublequote}a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}}]
- retrieves and stores existing facts in the theory context, or the
- specified target context (see also \secref{sec:target}). Typical
- applications would also involve attributes, to declare Simplifier
- rules, for example.
-
- \item [\hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}}] is essentially the same as \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}, but marks the result as a different kind of facts.
-
- \end{descr}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Name spaces%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcl}
- \indexdef{}{command}{global}\hypertarget{command.global}{\hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{local}\hypertarget{command.local}{\hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{hide}\hypertarget{command.hide}{\hyperlink{command.hide}{\mbox{\isa{\isacommand{hide}}}}} & : & \isartrans{theory}{theory} \\
- \end{matharray}
-
- \begin{rail}
- 'hide' ('(open)')? name (nameref + )
- ;
- \end{rail}
-
- Isabelle organizes any kind of name declarations (of types,
- constants, theorems etc.) by separate hierarchically structured name
- spaces. Normally the user does not have to control the behavior of
- name spaces by hand, yet the following commands provide some way to
- do so.
-
- \begin{descr}
-
- \item [\hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}} and \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}}] change the
- current name declaration mode. Initially, theories start in
- \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}} mode, causing all names to be automatically
- qualified by the theory name. Changing this to \hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}}
- causes all names to be declared without the theory prefix, until
- \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}} is declared again.
-
- Note that global names are prone to get hidden accidently later,
- when qualified names of the same base name are introduced.
-
- \item [\hyperlink{command.hide}{\mbox{\isa{\isacommand{hide}}}}~\isa{{\isachardoublequote}space\ names{\isachardoublequote}}] fully removes
- declarations from a given name space (which may be \isa{{\isachardoublequote}class{\isachardoublequote}},
- \isa{{\isachardoublequote}type{\isachardoublequote}}, \isa{{\isachardoublequote}const{\isachardoublequote}}, or \isa{{\isachardoublequote}fact{\isachardoublequote}}); with the \isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}} option, only the base name is hidden. Global
- (unqualified) names may never be hidden.
-
- Note that hiding name space accesses has no impact on logical
- declarations -- they remain valid internally. Entities that are no
- longer accessible to the user are printed with the special qualifier
- ``\isa{{\isachardoublequote}{\isacharquery}{\isacharquery}{\isachardoublequote}}'' prefixed to the full internal name.
-
- \end{descr}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Incorporating ML code \label{sec:ML}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcl}
- \indexdef{}{command}{use}\hypertarget{command.use}{\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}} & : & \isarkeep{theory~|~local{\dsh}theory} \\
- \indexdef{}{command}{ML}\hypertarget{command.ML}{\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}} & : & \isarkeep{theory~|~local{\dsh}theory} \\
- \indexdef{}{command}{ML\_val}\hypertarget{command.ML-val}{\hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}}} & : & \isartrans{\cdot}{\cdot} \\
- \indexdef{}{command}{ML\_command}\hypertarget{command.ML-command}{\hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}}} & : & \isartrans{\cdot}{\cdot} \\
- \indexdef{}{command}{setup}\hypertarget{command.setup}{\hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{method\_setup}\hypertarget{command.method-setup}{\hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isacharunderscore}setup}}}}} & : & \isartrans{theory}{theory} \\
- \end{matharray}
-
- \begin{rail}
- 'use' name
- ;
- ('ML' | 'ML\_val' | 'ML\_command' | 'setup') text
- ;
- 'method\_setup' name '=' text text
- ;
- \end{rail}
-
- \begin{descr}
-
- \item [\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}~\isa{{\isachardoublequote}file{\isachardoublequote}}] reads and executes ML
- commands from \isa{{\isachardoublequote}file{\isachardoublequote}}. The current theory context is passed
- down to the ML toplevel and may be modified, using \verb|"Context.>>"| or derived ML commands. The file name is checked with
- the \indexref{}{keyword}{uses}\hyperlink{keyword.uses}{\mbox{\isa{\isakeyword{uses}}}} dependency declaration given in the theory
- header (see also \secref{sec:begin-thy}).
-
- \item [\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}~\isa{{\isachardoublequote}text{\isachardoublequote}}] is similar to \hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}, but executes ML commands directly from the given \isa{{\isachardoublequote}text{\isachardoublequote}}.
-
- \item [\hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} and \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}}] are
- diagnostic versions of \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}, which means that the context
- may not be updated. \hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} echos the bindings produced
- at the ML toplevel, but \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}} is silent.
-
- \item [\hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}~\isa{{\isachardoublequote}text{\isachardoublequote}}] changes the current theory
- context by applying \isa{{\isachardoublequote}text{\isachardoublequote}}, which refers to an ML expression
- of type \verb|"theory -> theory"|. This enables to initialize
- any object-logic specific tools and packages written in ML, for
- example.
-
- \item [\hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isacharunderscore}setup}}}}~\isa{{\isachardoublequote}name\ {\isacharequal}\ text\ description{\isachardoublequote}}]
- defines a proof method in the current theory. The given \isa{{\isachardoublequote}text{\isachardoublequote}} has to be an ML expression of type \verb|"Args.src ->|\isasep\isanewline%
-\verb| Proof.context -> Proof.method"|. Parsing concrete method syntax
- from \verb|Args.src| input can be quite tedious in general. The
- following simple examples are for methods without any explicit
- arguments, or a list of theorems, respectively.
-
-%FIXME proper antiquotations
-{\footnotesize
-\begin{verbatim}
- Method.no_args (Method.METHOD (fn facts => foobar_tac))
- Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac))
- Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac))
- Method.thms_ctxt_args (fn thms => fn ctxt =>
- Method.METHOD (fn facts => foobar_tac))
-\end{verbatim}
-}
-
- Note that mere tactic emulations may ignore the \isa{facts}
- parameter above. Proper proof methods would do something
- appropriate with the list of current facts, though. Single-rule
- methods usually do strict forward-chaining (e.g.\ by using \verb|Drule.multi_resolves|), while automatic ones just insert the facts
- using \verb|Method.insert_tac| before applying the main tactic.
-
- \end{descr}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Syntax translation functions%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcl}
- \indexdef{}{command}{parse\_ast\_translation}\hypertarget{command.parse-ast-translation}{\hyperlink{command.parse-ast-translation}{\mbox{\isa{\isacommand{parse{\isacharunderscore}ast{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{parse\_translation}\hypertarget{command.parse-translation}{\hyperlink{command.parse-translation}{\mbox{\isa{\isacommand{parse{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{print\_translation}\hypertarget{command.print-translation}{\hyperlink{command.print-translation}{\mbox{\isa{\isacommand{print{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{typed\_print\_translation}\hypertarget{command.typed-print-translation}{\hyperlink{command.typed-print-translation}{\mbox{\isa{\isacommand{typed{\isacharunderscore}print{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{print\_ast\_translation}\hypertarget{command.print-ast-translation}{\hyperlink{command.print-ast-translation}{\mbox{\isa{\isacommand{print{\isacharunderscore}ast{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{token\_translation}\hypertarget{command.token-translation}{\hyperlink{command.token-translation}{\mbox{\isa{\isacommand{token{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\
- \end{matharray}
-
- \begin{rail}
- ( 'parse\_ast\_translation' | 'parse\_translation' | 'print\_translation' |
- 'typed\_print\_translation' | 'print\_ast\_translation' ) ('(advanced)')? text
- ;
-
- 'token\_translation' text
- ;
- \end{rail}
-
- Syntax translation functions written in ML admit almost arbitrary
- manipulations of Isabelle's inner syntax. Any of the above commands
- have a single \railqtok{text} argument that refers to an ML
- expression of appropriate type, which are as follows by default:
-
-%FIXME proper antiquotations
-\begin{ttbox}
-val parse_ast_translation : (string * (ast list -> ast)) list
-val parse_translation : (string * (term list -> term)) list
-val print_translation : (string * (term list -> term)) list
-val typed_print_translation :
- (string * (bool -> typ -> term list -> term)) list
-val print_ast_translation : (string * (ast list -> ast)) list
-val token_translation :
- (string * string * (string -> string * real)) list
-\end{ttbox}
-
- If the \isa{{\isachardoublequote}{\isacharparenleft}advanced{\isacharparenright}{\isachardoublequote}} option is given, the corresponding
- translation functions may depend on the current theory or proof
- context. This allows to implement advanced syntax mechanisms, as
- translations functions may refer to specific theory declarations or
- auxiliary proof data.
-
- See also \cite[\S8]{isabelle-ref} for more information on the
- general concept of syntax transformations in Isabelle.
-
-%FIXME proper antiquotations
-\begin{ttbox}
-val parse_ast_translation:
- (string * (Context.generic -> ast list -> ast)) list
-val parse_translation:
- (string * (Context.generic -> term list -> term)) list
-val print_translation:
- (string * (Context.generic -> term list -> term)) list
-val typed_print_translation:
- (string * (Context.generic -> bool -> typ -> term list -> term)) list
-val print_ast_translation:
- (string * (Context.generic -> ast list -> ast)) list
-\end{ttbox}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Oracles%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcl}
- \indexdef{}{command}{oracle}\hypertarget{command.oracle}{\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}} & : & \isartrans{theory}{theory} \\
- \end{matharray}
-
- The oracle interface promotes a given ML function \verb|theory -> T -> term| to \verb|theory -> T -> thm|, for some
- type \verb|T| given by the user. This acts like an infinitary
- specification of axioms -- there is no internal check of the
- correctness of the results! The inference kernel records oracle
- invocations within the internal derivation object of theorems, and
- the pretty printer attaches ``\isa{{\isachardoublequote}{\isacharbrackleft}{\isacharbang}{\isacharbrackright}{\isachardoublequote}}'' to indicate results
- that are not fully checked by Isabelle inferences.
-
- \begin{rail}
- 'oracle' name '(' type ')' '=' text
- ;
- \end{rail}
-
- \begin{descr}
-
- \item [\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}~\isa{{\isachardoublequote}name\ {\isacharparenleft}type{\isacharparenright}\ {\isacharequal}\ text{\isachardoublequote}}] turns the
- given ML expression \isa{{\isachardoublequote}text{\isachardoublequote}} of type
- \verb|theory ->|~\isa{{\isachardoublequote}type{\isachardoublequote}}~\verb|-> term| into an
- ML function of type
- \verb|theory ->|~\isa{{\isachardoublequote}type{\isachardoublequote}}~\verb|-> thm|, which is
- bound to the global identifier \verb|name|.
-
- \end{descr}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsection{Proof commands%
-}
-\isamarkuptrue%
-%
-\isamarkupsubsection{Markup commands \label{sec:markup-prf}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcl}
- \indexdef{}{command}{sect}\hypertarget{command.sect}{\hyperlink{command.sect}{\mbox{\isa{\isacommand{sect}}}}} & : & \isartrans{proof}{proof} \\
- \indexdef{}{command}{subsect}\hypertarget{command.subsect}{\hyperlink{command.subsect}{\mbox{\isa{\isacommand{subsect}}}}} & : & \isartrans{proof}{proof} \\
- \indexdef{}{command}{subsubsect}\hypertarget{command.subsubsect}{\hyperlink{command.subsubsect}{\mbox{\isa{\isacommand{subsubsect}}}}} & : & \isartrans{proof}{proof} \\
- \indexdef{}{command}{txt}\hypertarget{command.txt}{\hyperlink{command.txt}{\mbox{\isa{\isacommand{txt}}}}} & : & \isartrans{proof}{proof} \\
- \indexdef{}{command}{txt\_raw}\hypertarget{command.txt-raw}{\hyperlink{command.txt-raw}{\mbox{\isa{\isacommand{txt{\isacharunderscore}raw}}}}} & : & \isartrans{proof}{proof} \\
- \end{matharray}
-
- These markup commands for proof mode closely correspond to the ones
- of theory mode (see \S\ref{sec:markup-thy}).
-
- \begin{rail}
- ('sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt\_raw') text
- ;
- \end{rail}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
\isamarkupsection{Other commands%
}
\isamarkuptrue%
@@ -871,15 +248,11 @@
\indexdef{}{command}{cd}\hypertarget{command.cd}{\hyperlink{command.cd}{\mbox{\isa{\isacommand{cd}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
\indexdef{}{command}{pwd}\hypertarget{command.pwd}{\hyperlink{command.pwd}{\mbox{\isa{\isacommand{pwd}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
\indexdef{}{command}{use\_thy}\hypertarget{command.use-thy}{\hyperlink{command.use-thy}{\mbox{\isa{\isacommand{use{\isacharunderscore}thy}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
- \indexdef{}{command}{display\_drafts}\hypertarget{command.display-drafts}{\hyperlink{command.display-drafts}{\mbox{\isa{\isacommand{display{\isacharunderscore}drafts}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
- \indexdef{}{command}{print\_drafts}\hypertarget{command.print-drafts}{\hyperlink{command.print-drafts}{\mbox{\isa{\isacommand{print{\isacharunderscore}drafts}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
\end{matharray}
\begin{rail}
('cd' | 'use\_thy' | 'update\_thy') name
;
- ('display\_drafts' | 'print\_drafts') (name +)
- ;
\end{rail}
\begin{descr}
@@ -893,11 +266,6 @@
These system commands are scarcely used when working interactively,
since loading of theories is done automatically as required.
- \item [\hyperlink{command.display-drafts}{\mbox{\isa{\isacommand{display{\isacharunderscore}drafts}}}}~\isa{paths} and \hyperlink{command.print-drafts}{\mbox{\isa{\isacommand{print{\isacharunderscore}drafts}}}}~\isa{paths}] perform simple output of a given list
- of raw source files. Only those symbols that do not require
- additional {\LaTeX} packages are displayed properly, everything else
- is left verbatim.
-
\end{descr}%
\end{isamarkuptext}%
\isamarkuptrue%