wenzelm@26869: %
wenzelm@26869: \begin{isabellebody}%
wenzelm@26869: \def\isabellecontext{Spec}%
wenzelm@26869: %
wenzelm@26869: \isadelimtheory
wenzelm@26869: %
wenzelm@26869: \endisadelimtheory
wenzelm@26869: %
wenzelm@26869: \isatagtheory
wenzelm@26869: \isacommand{theory}\isamarkupfalse%
wenzelm@26869: \ Spec\isanewline
wenzelm@43522: \isakeyword{imports}\ Base\ Main\isanewline
wenzelm@26869: \isakeyword{begin}%
wenzelm@26869: \endisatagtheory
wenzelm@26869: {\isafoldtheory}%
wenzelm@26869: %
wenzelm@26869: \isadelimtheory
wenzelm@26869: %
wenzelm@26869: \endisadelimtheory
wenzelm@26869: %
wenzelm@44140: \isamarkupchapter{Specifications%
wenzelm@26869: }
wenzelm@26869: \isamarkuptrue%
wenzelm@26869: %
wenzelm@30072: \begin{isamarkuptext}%
wenzelm@30072: The Isabelle/Isar theory format integrates specifications and
wenzelm@30072:   proofs, supporting interactive development with unlimited undo
wenzelm@30072:   operation.  There is an integrated document preparation system (see
wenzelm@30072:   \chref{ch:document-prep}), for typesetting formal developments
wenzelm@30072:   together with informal text.  The resulting hyper-linked PDF
wenzelm@30072:   documents can be used both for WWW presentation and printed copies.
wenzelm@30072: 
wenzelm@30072:   The Isar proof language (see \chref{ch:proofs}) is embedded into the
wenzelm@30072:   theory language as a proper sub-language.  Proof mode is entered by
wenzelm@30072:   stating some \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}} or \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}} at the theory
wenzelm@30072:   level, and left again with the final conclusion (e.g.\ via \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}).  Some theory specification mechanisms also require a proof,
wenzelm@30072:   such as \hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}} in HOL, which demands non-emptiness of
wenzelm@30072:   the representing sets.%
wenzelm@30072: \end{isamarkuptext}%
wenzelm@30072: \isamarkuptrue%
wenzelm@30072: %
wenzelm@26870: \isamarkupsection{Defining theories \label{sec:begin-thy}%
wenzelm@26870: }
wenzelm@26870: \isamarkuptrue%
wenzelm@26870: %
wenzelm@26870: \begin{isamarkuptext}%
wenzelm@26870: \begin{matharray}{rcl}
wenzelm@40685:     \indexdef{}{command}{theory}\hypertarget{command.theory}{\hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}toplevel\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@40685:     \indexdef{global}{command}{end}\hypertarget{command.global.end}{\hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ toplevel{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@26870:   \end{matharray}
wenzelm@26870: 
wenzelm@28788:   Isabelle/Isar theories are defined via theory files, which may
wenzelm@28788:   contain both specifications and proofs; occasionally definitional
wenzelm@28788:   mechanisms also require some explicit proof.  The theory body may be
wenzelm@28788:   sub-structured by means of \emph{local theory targets}, such as
wenzelm@28788:   \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}} and \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}.
wenzelm@26870: 
wenzelm@28788:   The first proper command of a theory is \hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}}, which
wenzelm@28788:   indicates imports of previous theories and optional dependencies on
wenzelm@28788:   other source files (usually in ML).  Just preceding the initial
wenzelm@28788:   \hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}} command there may be an optional \hyperlink{command.header}{\mbox{\isa{\isacommand{header}}}} declaration, which is only relevant to document
wenzelm@28788:   preparation: see also the other section markup commands in
wenzelm@28788:   \secref{sec:markup}.
wenzelm@28788: 
wenzelm@28788:   A theory is concluded by a final \hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}} command,
wenzelm@28788:   one that does not belong to a local theory target.  No further
wenzelm@28788:   commands may follow such a global \hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}},
wenzelm@28788:   although some user-interfaces might pretend that trailing input is
wenzelm@28788:   admissible.
wenzelm@26870: 
wenzelm@43467:   \begin{railoutput}
wenzelm@43575: \rail@begin{4}{}
wenzelm@43467: \rail@term{\hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}}}[]
wenzelm@43467: \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
wenzelm@43575: \rail@cr{2}
wenzelm@43467: \rail@term{\isa{\isakeyword{imports}}}[]
wenzelm@43467: \rail@plus
wenzelm@43467: \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
wenzelm@43575: \rail@nextplus{3}
wenzelm@43467: \rail@endplus
wenzelm@43467: \rail@bar
wenzelm@43575: \rail@nextbar{3}
wenzelm@43467: \rail@nont{\isa{uses}}[]
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@term{\isa{\isakeyword{begin}}}[]
wenzelm@43467: \rail@end
wenzelm@43467: \rail@begin{3}{\isa{uses}}
wenzelm@43467: \rail@term{\isa{\isakeyword{uses}}}[]
wenzelm@43467: \rail@plus
wenzelm@43467: \rail@bar
wenzelm@43467: \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
wenzelm@43467: \rail@nextbar{1}
wenzelm@43467: \rail@nont{\hyperlink{syntax.parname}{\mbox{\isa{parname}}}}[]
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@nextplus{2}
wenzelm@43467: \rail@endplus
wenzelm@43467: \rail@end
wenzelm@43467: \end{railoutput}
wenzelm@26870: 
wenzelm@26870: 
wenzelm@28788:   \begin{description}
wenzelm@26870: 
wenzelm@40685:   \item \hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{5C3C494D504F5254533E}{\isasymIMPORTS}}\ B\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ B\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C424547494E3E}{\isasymBEGIN}}{\isaliteral{22}{\isachardoublequote}}}
wenzelm@28788:   starts a new theory \isa{A} based on the merge of existing
wenzelm@40685:   theories \isa{{\isaliteral{22}{\isachardoublequote}}B\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ B\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}.
wenzelm@26870:   
wenzelm@28788:   Due to the possibility to import more than one ancestor, the
wenzelm@28788:   resulting theory structure of an Isabelle session forms a directed
wenzelm@28788:   acyclic graph (DAG).  Isabelle's theory loader ensures that the
wenzelm@28788:   sources contributing to the development graph are always up-to-date:
wenzelm@28788:   changed files are automatically reloaded whenever a theory header
wenzelm@28788:   specification is processed.
wenzelm@26870:   
wenzelm@26902:   The optional \indexdef{}{keyword}{uses}\hypertarget{keyword.uses}{\hyperlink{keyword.uses}{\mbox{\isa{\isakeyword{uses}}}}} specification declares additional
wenzelm@26870:   dependencies on extra files (usually ML sources).  Files will be
wenzelm@28788:   loaded immediately (as ML), unless the name is parenthesized.  The
wenzelm@28788:   latter case records a dependency that needs to be resolved later in
wenzelm@28788:   the text, usually via explicit \indexref{}{command}{use}\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}} for ML files;
wenzelm@28788:   other file formats require specific load commands defined by the
wenzelm@28788:   corresponding tools or packages.
wenzelm@26870:   
wenzelm@28788:   \item \hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}} concludes the current theory
wenzelm@28788:   definition.  Note that local theory targets involve a local
wenzelm@28788:   \hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}}, which is clear from the nesting.
wenzelm@26870: 
wenzelm@28788:   \end{description}%
wenzelm@26870: \end{isamarkuptext}%
wenzelm@26870: \isamarkuptrue%
wenzelm@26870: %
wenzelm@27042: \isamarkupsection{Local theory targets \label{sec:target}%
wenzelm@27042: }
wenzelm@27042: \isamarkuptrue%
wenzelm@27042: %
wenzelm@27042: \begin{isamarkuptext}%
wenzelm@27042: A local theory target is a context managed separately within the
wenzelm@27042:   enclosing theory.  Contexts may introduce parameters (fixed
wenzelm@27042:   variables) and assumptions (hypotheses).  Definitions and theorems
wenzelm@27042:   depending on the context may be added incrementally later on.  Named
wenzelm@27042:   contexts refer to locales (cf.\ \secref{sec:locale}) or type classes
wenzelm@40685:   (cf.\ \secref{sec:class}); the name ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{22}{\isachardoublequote}}}'' signifies the
wenzelm@27042:   global theory context.
wenzelm@27042: 
wenzelm@27042:   \begin{matharray}{rcll}
wenzelm@40685:     \indexdef{}{command}{context}\hypertarget{command.context}{\hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@40685:     \indexdef{local}{command}{end}\hypertarget{command.local.end}{\hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@27042:   \end{matharray}
wenzelm@27042: 
wenzelm@43467:   \begin{railoutput}
wenzelm@43535: \rail@begin{1}{}
wenzelm@43467: \rail@term{\hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}}[]
wenzelm@47870: \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
wenzelm@43467: \rail@term{\isa{\isakeyword{begin}}}[]
wenzelm@43467: \rail@end
wenzelm@43467: \rail@begin{1}{\indexdef{}{syntax}{target}\hypertarget{syntax.target}{\hyperlink{syntax.target}{\mbox{\isa{target}}}}}
wenzelm@43467: \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
wenzelm@43467: \rail@term{\isa{\isakeyword{in}}}[]
wenzelm@47870: \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
wenzelm@43467: \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
wenzelm@43467: \rail@end
wenzelm@43467: \end{railoutput}
wenzelm@27042: 
wenzelm@27042: 
wenzelm@28788:   \begin{description}
wenzelm@27042:   
wenzelm@40685:   \item \hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{5C3C424547494E3E}{\isasymBEGIN}}{\isaliteral{22}{\isachardoublequote}}} recommences an
wenzelm@27042:   existing locale or class context \isa{c}.  Note that locale and
wenzelm@27052:   class definitions allow to include the \hyperlink{keyword.begin}{\mbox{\isa{\isakeyword{begin}}}} keyword as
wenzelm@27052:   well, in order to continue the local theory immediately after the
wenzelm@27052:   initial specification.
wenzelm@27042:   
wenzelm@28788:   \item \hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}} concludes the current local theory
wenzelm@27042:   and continues the enclosing global theory.  Note that a global
wenzelm@27042:   \hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}} has a different meaning: it concludes the
wenzelm@27042:   theory itself (\secref{sec:begin-thy}).
wenzelm@27042:   
wenzelm@40685:   \item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}}\indexdef{}{keyword}{in}\hypertarget{keyword.in}{\hyperlink{keyword.in}{\mbox{\isa{\isakeyword{in}}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} given after any
wenzelm@30072:   local theory command specifies an immediate target, e.g.\
wenzelm@40685:   ``\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C494E3E}{\isasymIN}}\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}'' or ``\hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C494E3E}{\isasymIN}}\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}''.  This works both in a local or
wenzelm@27042:   global theory context; the current target context will be suspended
wenzelm@40685:   for this command only.  Note that ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C494E3E}{\isasymIN}}\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'' will
wenzelm@27042:   always produce a global result independently of the current target
wenzelm@27042:   context.
wenzelm@27042: 
wenzelm@28788:   \end{description}
wenzelm@27042: 
wenzelm@27042:   The exact meaning of results produced within a local theory context
wenzelm@27042:   depends on the underlying target infrastructure (locale, type class
wenzelm@27042:   etc.).  The general idea is as follows, considering a context named
wenzelm@40685:   \isa{c} with parameter \isa{x} and assumption \isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}}.
wenzelm@27042:   
wenzelm@27042:   Definitions are exported by introducing a global version with
wenzelm@27042:   additional arguments; a syntactic abbreviation links the long form
wenzelm@27042:   with the abstract version of the target context.  For example,
wenzelm@40685:   \isa{{\isaliteral{22}{\isachardoublequote}}a\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} becomes \isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{2E}{\isachardot}}a\ {\isaliteral{3F}{\isacharquery}}x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} at the theory
wenzelm@40685:   level (for arbitrary \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}x{\isaliteral{22}{\isachardoublequote}}}), together with a local
wenzelm@40685:   abbreviation \isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ c{\isaliteral{2E}{\isachardot}}a\ x{\isaliteral{22}{\isachardoublequote}}} in the target context (for the
wenzelm@27042:   fixed parameter \isa{x}).
wenzelm@27042: 
wenzelm@27042:   Theorems are exported by discharging the assumptions and
wenzelm@40685:   generalizing the parameters of the context.  For example, \isa{{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{3A}{\isacharcolon}}\ B{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} becomes \isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{2E}{\isachardot}}a{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}x{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}}, again for arbitrary
wenzelm@40685:   \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}x{\isaliteral{22}{\isachardoublequote}}}.%
wenzelm@27042: \end{isamarkuptext}%
wenzelm@27042: \isamarkuptrue%
wenzelm@27042: %
wenzelm@27042: \isamarkupsection{Basic specification elements%
wenzelm@27042: }
wenzelm@27042: \isamarkuptrue%
wenzelm@27042: %
wenzelm@27042: \begin{isamarkuptext}%
wenzelm@27042: \begin{matharray}{rcll}
wenzelm@40685:     \indexdef{}{command}{axiomatization}\hypertarget{command.axiomatization}{\hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{axiomatization}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} & (axiomatic!) \\
wenzelm@40685:     \indexdef{}{command}{definition}\hypertarget{command.definition}{\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@28788:     \indexdef{}{attribute}{defn}\hypertarget{attribute.defn}{\hyperlink{attribute.defn}{\mbox{\isa{defn}}}} & : & \isa{attribute} \\
wenzelm@40685:     \indexdef{}{command}{abbreviation}\hypertarget{command.abbreviation}{\hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@40685:     \indexdef{}{command}{print\_abbrevs}\hypertarget{command.print-abbrevs}{\hyperlink{command.print-abbrevs}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}abbrevs}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ {\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@27042:   \end{matharray}
wenzelm@27042: 
wenzelm@27042:   These specification mechanisms provide a slightly more abstract view
wenzelm@27042:   than the underlying primitives of \hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}, \hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}} (see \secref{sec:consts}), and \hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}} (see
wenzelm@27042:   \secref{sec:axms-thms}).  In particular, type-inference is commonly
wenzelm@27042:   available, and result names need not be given.
wenzelm@27042: 
wenzelm@43467:   \begin{railoutput}
wenzelm@43535: \rail@begin{2}{}
wenzelm@43467: \rail@term{\hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{axiomatization}}}}}[]
wenzelm@43467: \rail@bar
wenzelm@43467: \rail@nextbar{1}
wenzelm@43467: \rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@bar
wenzelm@43467: \rail@nextbar{1}
wenzelm@43467: \rail@term{\isa{\isakeyword{where}}}[]
wenzelm@43467: \rail@nont{\isa{specs}}[]
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@end
wenzelm@43575: \rail@begin{5}{}
wenzelm@43467: \rail@term{\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}}[]
wenzelm@43467: \rail@bar
wenzelm@43467: \rail@nextbar{1}
wenzelm@43467: \rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
wenzelm@43467: \rail@endbar
wenzelm@43575: \rail@cr{3}
wenzelm@43467: \rail@bar
wenzelm@43575: \rail@nextbar{4}
wenzelm@43467: \rail@nont{\isa{decl}}[]
wenzelm@43467: \rail@term{\isa{\isakeyword{where}}}[]
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@bar
wenzelm@43575: \rail@nextbar{4}
wenzelm@43467: \rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
wenzelm@43467: \rail@end
wenzelm@43575: \rail@begin{5}{}
wenzelm@43467: \rail@term{\hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}}[]
wenzelm@43467: \rail@bar
wenzelm@43467: \rail@nextbar{1}
wenzelm@43467: \rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@bar
wenzelm@43467: \rail@nextbar{1}
wenzelm@43467: \rail@nont{\hyperlink{syntax.mode}{\mbox{\isa{mode}}}}[]
wenzelm@43467: \rail@endbar
wenzelm@43575: \rail@cr{3}
wenzelm@43467: \rail@bar
wenzelm@43575: \rail@nextbar{4}
wenzelm@43467: \rail@nont{\isa{decl}}[]
wenzelm@43467: \rail@term{\isa{\isakeyword{where}}}[]
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
wenzelm@43467: \rail@end
wenzelm@43467: \rail@begin{4}{\indexdef{}{syntax}{fixes}\hypertarget{syntax.fixes}{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}}
wenzelm@43467: \rail@plus
wenzelm@43467: \rail@bar
wenzelm@43467: \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
wenzelm@43467: \rail@bar
wenzelm@43467: \rail@nextbar{1}
wenzelm@43467: \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}}}[]
wenzelm@43467: \rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@bar
wenzelm@43467: \rail@nextbar{1}
wenzelm@43467: \rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@nextbar{2}
wenzelm@43467: \rail@nont{\hyperlink{syntax.vars}{\mbox{\isa{vars}}}}[]
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@nextplus{3}
wenzelm@43467: \rail@cterm{\isa{\isakeyword{and}}}[]
wenzelm@43467: \rail@endplus
wenzelm@43467: \rail@end
wenzelm@43467: \rail@begin{3}{\isa{specs}}
wenzelm@43467: \rail@plus
wenzelm@43467: \rail@bar
wenzelm@43467: \rail@nextbar{1}
wenzelm@43467: \rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@nont{\hyperlink{syntax.props}{\mbox{\isa{props}}}}[]
wenzelm@43467: \rail@nextplus{2}
wenzelm@43467: \rail@cterm{\isa{\isakeyword{and}}}[]
wenzelm@43467: \rail@endplus
wenzelm@43467: \rail@end
wenzelm@43467: \rail@begin{2}{\isa{decl}}
wenzelm@43467: \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
wenzelm@43467: \rail@bar
wenzelm@43467: \rail@nextbar{1}
wenzelm@43467: \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}}}[]
wenzelm@43467: \rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@bar
wenzelm@43467: \rail@nextbar{1}
wenzelm@43467: \rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@end
wenzelm@43467: \end{railoutput}
wenzelm@27042: 
wenzelm@27042: 
wenzelm@28788:   \begin{description}
wenzelm@27042:   
wenzelm@40685:   \item \hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{axiomatization}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub m\ {\isaliteral{5C3C57484552453E}{\isasymWHERE}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}
wenzelm@28788:   introduces several constants simultaneously and states axiomatic
wenzelm@28788:   properties for these.  The constants are marked as being specified
wenzelm@28788:   once and for all, which prevents additional specifications being
wenzelm@28788:   issued later on.
wenzelm@27042:   
wenzelm@27042:   Note that axiomatic specifications are only appropriate when
wenzelm@28110:   declaring a new logical system; axiomatic specifications are
wenzelm@28110:   restricted to global theory contexts.  Normal applications should
wenzelm@28110:   only use definitional mechanisms!
wenzelm@27042: 
wenzelm@40685:   \item \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{5C3C57484552453E}{\isasymWHERE}}\ eq{\isaliteral{22}{\isachardoublequote}}} produces an
wenzelm@40685:   internal definition \isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t{\isaliteral{22}{\isachardoublequote}}} according to the specification
wenzelm@27042:   given as \isa{eq}, which is then turned into a proven fact.  The
wenzelm@27042:   given proposition may deviate from internal meta-level equality
wenzelm@27042:   according to the rewrite rules declared as \hyperlink{attribute.defn}{\mbox{\isa{defn}}} by the
wenzelm@40685:   object-logic.  This usually covers object-level equality \isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{22}{\isachardoublequote}}} and equivalence \isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{5C3C6C65667472696768746172726F773E}{\isasymleftrightarrow}}\ B{\isaliteral{22}{\isachardoublequote}}}.  End-users normally need not
wenzelm@27042:   change the \hyperlink{attribute.defn}{\mbox{\isa{defn}}} setup.
wenzelm@27042:   
wenzelm@27042:   Definitions may be presented with explicit arguments on the LHS, as
wenzelm@40685:   well as additional conditions, e.g.\ \isa{{\isaliteral{22}{\isachardoublequote}}f\ x\ y\ {\isaliteral{3D}{\isacharequal}}\ t{\isaliteral{22}{\isachardoublequote}}} instead of
wenzelm@40685:   \isa{{\isaliteral{22}{\isachardoublequote}}f\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x\ y{\isaliteral{2E}{\isachardot}}\ t{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}y\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isadigit{0}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ g\ x\ y\ {\isaliteral{3D}{\isacharequal}}\ u{\isaliteral{22}{\isachardoublequote}}} instead of an
wenzelm@40685:   unrestricted \isa{{\isaliteral{22}{\isachardoublequote}}g\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x\ y{\isaliteral{2E}{\isachardot}}\ u{\isaliteral{22}{\isachardoublequote}}}.
wenzelm@27042:   
wenzelm@40685:   \item \hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{5C3C57484552453E}{\isasymWHERE}}\ eq{\isaliteral{22}{\isachardoublequote}}} introduces a
wenzelm@28788:   syntactic constant which is associated with a certain term according
wenzelm@28788:   to the meta-level equality \isa{eq}.
wenzelm@27042:   
wenzelm@27042:   Abbreviations participate in the usual type-inference process, but
wenzelm@27042:   are expanded before the logic ever sees them.  Pretty printing of
wenzelm@27042:   terms involves higher-order rewriting with rules stemming from
wenzelm@27042:   reverted abbreviations.  This needs some care to avoid overlapping
wenzelm@27042:   or looping syntactic replacements!
wenzelm@27042:   
wenzelm@27042:   The optional \isa{mode} specification restricts output to a
wenzelm@27042:   particular print mode; using ``\isa{input}'' here achieves the
wenzelm@27042:   effect of one-way abbreviations.  The mode may also include an
wenzelm@27042:   ``\hyperlink{keyword.output}{\mbox{\isa{\isakeyword{output}}}}'' qualifier that affects the concrete syntax
wenzelm@27042:   declared for abbreviations, cf.\ \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} in
wenzelm@27042:   \secref{sec:syn-trans}.
wenzelm@27042:   
wenzelm@40685:   \item \hyperlink{command.print-abbrevs}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}abbrevs}}}} prints all constant abbreviations
wenzelm@27042:   of the current context.
wenzelm@27042:   
wenzelm@28788:   \end{description}%
wenzelm@27042: \end{isamarkuptext}%
wenzelm@27042: \isamarkuptrue%
wenzelm@27042: %
wenzelm@27042: \isamarkupsection{Generic declarations%
wenzelm@27042: }
wenzelm@27042: \isamarkuptrue%
wenzelm@27042: %
wenzelm@27042: \begin{isamarkuptext}%
wenzelm@27042: Arbitrary operations on the background context may be wrapped-up as
wenzelm@27042:   generic declaration elements.  Since the underlying concept of local
wenzelm@27042:   theories may be subject to later re-interpretation, there is an
wenzelm@27042:   additional dependency on a morphism that tells the difference of the
wenzelm@27042:   original declaration context wrt.\ the application context
wenzelm@27042:   encountered later on.  A fact declaration is an important special
wenzelm@27042:   case: it consists of a theorem which is applied to the context by
wenzelm@27042:   means of an attribute.
wenzelm@27042: 
wenzelm@27042:   \begin{matharray}{rcl}
wenzelm@40685:     \indexdef{}{command}{declaration}\hypertarget{command.declaration}{\hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@41034:     \indexdef{}{command}{syntax\_declaration}\hypertarget{command.syntax-declaration}{\hyperlink{command.syntax-declaration}{\mbox{\isa{\isacommand{syntax{\isaliteral{5F}{\isacharunderscore}}declaration}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@40685:     \indexdef{}{command}{declare}\hypertarget{command.declare}{\hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@27042:   \end{matharray}
wenzelm@27042: 
wenzelm@43467:   \begin{railoutput}
wenzelm@43575: \rail@begin{5}{}
wenzelm@43467: \rail@bar
wenzelm@43467: \rail@term{\hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}}[]
wenzelm@43467: \rail@nextbar{1}
wenzelm@43467: \rail@term{\hyperlink{command.syntax-declaration}{\mbox{\isa{\isacommand{syntax{\isaliteral{5F}{\isacharunderscore}}declaration}}}}}[]
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@bar
wenzelm@43467: \rail@nextbar{1}
wenzelm@43467: \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
wenzelm@43467: \rail@term{\isa{\isakeyword{pervasive}}}[]
wenzelm@43467: \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
wenzelm@43467: \rail@endbar
wenzelm@43575: \rail@cr{3}
wenzelm@43467: \rail@bar
wenzelm@43575: \rail@nextbar{4}
wenzelm@43467: \rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
wenzelm@43467: \rail@end
wenzelm@43535: \rail@begin{2}{}
wenzelm@43467: \rail@term{\hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}}}[]
wenzelm@43467: \rail@bar
wenzelm@43467: \rail@nextbar{1}
wenzelm@43467: \rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@plus
wenzelm@43467: \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
wenzelm@43467: \rail@nextplus{1}
wenzelm@43467: \rail@cterm{\isa{\isakeyword{and}}}[]
wenzelm@43467: \rail@endplus
wenzelm@43467: \rail@end
wenzelm@43467: \end{railoutput}
wenzelm@43467: 
wenzelm@27042: 
wenzelm@28788:   \begin{description}
wenzelm@27042: 
wenzelm@28788:   \item \hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}~\isa{d} adds the declaration
wenzelm@27042:   function \isa{d} of ML type \verb|declaration|, to the current
wenzelm@27042:   local theory under construction.  In later application contexts, the
wenzelm@27042:   function is transformed according to the morphisms being involved in
wenzelm@27042:   the interpretation hierarchy.
wenzelm@27042: 
wenzelm@40685:   If the \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}pervasive{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} option is given, the corresponding
wenzelm@33516:   declaration is applied to all possible contexts involved, including
wenzelm@33516:   the global background theory.
wenzelm@33516: 
wenzelm@41034:   \item \hyperlink{command.syntax-declaration}{\mbox{\isa{\isacommand{syntax{\isaliteral{5F}{\isacharunderscore}}declaration}}}} is similar to \hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}, but is meant to affect only ``syntactic'' tools by
wenzelm@41034:   convention (such as notation and type-checking information).
wenzelm@41034: 
wenzelm@28788:   \item \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}}~\isa{thms} declares theorems to the
wenzelm@27042:   current local theory context.  No theorem binding is involved here,
wenzelm@27042:   unlike \hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}} or \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}} (cf.\
wenzelm@27042:   \secref{sec:axms-thms}), so \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}} only has the effect
wenzelm@27042:   of applying attributes as included in the theorem specification.
wenzelm@27042: 
wenzelm@28788:   \end{description}%
wenzelm@27042: \end{isamarkuptext}%
wenzelm@27042: \isamarkuptrue%
wenzelm@27042: %
wenzelm@27042: \isamarkupsection{Locales \label{sec:locale}%
wenzelm@27042: }
wenzelm@27042: \isamarkuptrue%
wenzelm@27042: %
wenzelm@27042: \begin{isamarkuptext}%
ballarin@33846: Locales are parametric named local contexts, consisting of a list of
wenzelm@27042:   declaration elements that are modeled after the Isar proof context
wenzelm@27042:   commands (cf.\ \secref{sec:proof-context}).%
wenzelm@27042: \end{isamarkuptext}%
wenzelm@27042: \isamarkuptrue%
wenzelm@27042: %
ballarin@33846: \isamarkupsubsection{Locale expressions \label{sec:locale-expr}%
ballarin@33846: }
ballarin@33846: \isamarkuptrue%
ballarin@33846: %
ballarin@33846: \begin{isamarkuptext}%
ballarin@33846: A \emph{locale expression} denotes a structured context composed of
ballarin@33846:   instances of existing locales.  The context consists of a list of
ballarin@33846:   instances of declaration elements from the locales.  Two locale
ballarin@33846:   instances are equal if they are of the same locale and the
ballarin@33846:   parameters are instantiated with equivalent terms.  Declaration
ballarin@33846:   elements from equal instances are never repeated, thus avoiding
ballarin@33846:   duplicate declarations.
ballarin@33846: 
wenzelm@43467:   \begin{railoutput}
wenzelm@43488: \rail@begin{3}{\indexdef{}{syntax}{locale\_expr}\hypertarget{syntax.locale-expr}{\hyperlink{syntax.locale-expr}{\mbox{\isa{locale{\isaliteral{5F}{\isacharunderscore}}expr}}}}}
wenzelm@43467: \rail@plus
wenzelm@43467: \rail@nont{\isa{instance}}[]
wenzelm@43467: \rail@nextplus{1}
wenzelm@43467: \rail@cterm{\isa{{\isaliteral{2B}{\isacharplus}}}}[]
wenzelm@43467: \rail@endplus
wenzelm@43467: \rail@bar
wenzelm@43467: \rail@nextbar{1}
wenzelm@43467: \rail@term{\isa{\isakeyword{for}}}[]
wenzelm@43467: \rail@plus
wenzelm@43467: \rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]
wenzelm@43467: \rail@nextplus{2}
wenzelm@43467: \rail@cterm{\isa{\isakeyword{and}}}[]
wenzelm@43467: \rail@endplus
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@end
wenzelm@43467: \rail@begin{2}{\isa{instance}}
wenzelm@43467: \rail@bar
wenzelm@43467: \rail@nextbar{1}
wenzelm@43467: \rail@nont{\isa{qualifier}}[]
wenzelm@43467: \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
wenzelm@43467: \rail@bar
wenzelm@43488: \rail@nont{\isa{pos{\isaliteral{5F}{\isacharunderscore}}insts}}[]
wenzelm@43467: \rail@nextbar{1}
wenzelm@43488: \rail@nont{\isa{named{\isaliteral{5F}{\isacharunderscore}}insts}}[]
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@end
wenzelm@43467: \rail@begin{3}{\isa{qualifier}}
wenzelm@43467: \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
wenzelm@43467: \rail@bar
wenzelm@43467: \rail@nextbar{1}
wenzelm@43467: \rail@bar
wenzelm@43467: \rail@term{\isa{{\isaliteral{3F}{\isacharquery}}}}[]
wenzelm@43467: \rail@nextbar{2}
wenzelm@43467: \rail@term{\isa{{\isaliteral{21}{\isacharbang}}}}[]
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@end
wenzelm@43488: \rail@begin{3}{\isa{pos{\isaliteral{5F}{\isacharunderscore}}insts}}
wenzelm@43467: \rail@plus
wenzelm@43467: \rail@nextplus{1}
wenzelm@43467: \rail@bar
wenzelm@43467: \rail@term{\isa{{\isaliteral{5F}{\isacharunderscore}}}}[]
wenzelm@43467: \rail@nextbar{2}
wenzelm@43467: \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@endplus
wenzelm@43467: \rail@end
wenzelm@43488: \rail@begin{2}{\isa{named{\isaliteral{5F}{\isacharunderscore}}insts}}
wenzelm@43467: \rail@term{\isa{\isakeyword{where}}}[]
wenzelm@43467: \rail@plus
wenzelm@43467: \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
wenzelm@43467: \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
wenzelm@43467: \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
wenzelm@43467: \rail@nextplus{1}
wenzelm@43467: \rail@cterm{\isa{\isakeyword{and}}}[]
wenzelm@43467: \rail@endplus
wenzelm@43467: \rail@end
wenzelm@43467: \end{railoutput}
wenzelm@43467: 
ballarin@33846: 
ballarin@33846:   A locale instance consists of a reference to a locale and either
ballarin@33846:   positional or named parameter instantiations.  Identical
ballarin@33846:   instantiations (that is, those that instante a parameter by itself)
wenzelm@40685:   may be omitted.  The notation `\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}}' enables to omit the
wenzelm@40517:   instantiation for a parameter inside a positional instantiation.
ballarin@33846: 
ballarin@33846:   Terms in instantiations are from the context the locale expressions
ballarin@33846:   is declared in.  Local names may be added to this context with the
ballarin@33846:   optional for clause.  In addition, syntax declarations from one
ballarin@33846:   instance are effective when parsing subsequent instances of the same
ballarin@33846:   expression.
ballarin@33846: 
ballarin@33846:   Instances have an optional qualifier which applies to names in
ballarin@33846:   declarations.  Names include local definitions and theorem names.
ballarin@33846:   If present, the qualifier itself is either optional
ballarin@33846:   (``\texttt{?}''), which means that it may be omitted on input of the
ballarin@33846:   qualified name, or mandatory (``\texttt{!}'').  If neither
ballarin@33846:   ``\texttt{?}'' nor ``\texttt{!}'' are present, the command's default
ballarin@33846:   is used.  For \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}} and \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}
ballarin@33846:   the default is ``mandatory'', for \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}} and \hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}} the default is ``optional''.%
ballarin@33846: \end{isamarkuptext}%
ballarin@33846: \isamarkuptrue%
ballarin@33846: %
ballarin@33846: \isamarkupsubsection{Locale declarations%
wenzelm@27042: }
wenzelm@27042: \isamarkuptrue%
wenzelm@27042: %
wenzelm@27042: \begin{isamarkuptext}%
wenzelm@27042: \begin{matharray}{rcl}
wenzelm@40685:     \indexdef{}{command}{locale}\hypertarget{command.locale}{\hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@40685:     \indexdef{}{command}{print\_locale}\hypertarget{command.print-locale}{\hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}locale}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@40685:     \indexdef{}{command}{print\_locales}\hypertarget{command.print-locales}{\hyperlink{command.print-locales}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}locales}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@40685:     \indexdef{}{method}{intro\_locales}\hypertarget{method.intro-locales}{\hyperlink{method.intro-locales}{\mbox{\isa{intro{\isaliteral{5F}{\isacharunderscore}}locales}}}} & : & \isa{method} \\
wenzelm@40685:     \indexdef{}{method}{unfold\_locales}\hypertarget{method.unfold-locales}{\hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isaliteral{5F}{\isacharunderscore}}locales}}}} & : & \isa{method} \\
wenzelm@27042:   \end{matharray}
wenzelm@27042: 
wenzelm@27042:   \indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes}
wenzelm@28788:   \indexisarelem{defines}\indexisarelem{notes}
wenzelm@43467:   \begin{railoutput}
wenzelm@43535: \rail@begin{2}{}
wenzelm@43467: \rail@term{\hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}}[]
wenzelm@43467: \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
wenzelm@43467: \rail@bar
wenzelm@43467: \rail@nextbar{1}
wenzelm@43467: \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
wenzelm@43467: \rail@nont{\hyperlink{syntax.locale}{\mbox{\isa{locale}}}}[]
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@bar
wenzelm@43467: \rail@nextbar{1}
wenzelm@43467: \rail@term{\isa{\isakeyword{begin}}}[]
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@end
wenzelm@43535: \rail@begin{2}{}
wenzelm@43467: \rail@term{\hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}locale}}}}}[]
wenzelm@43467: \rail@bar
wenzelm@43467: \rail@nextbar{1}
wenzelm@43467: \rail@term{\isa{{\isaliteral{21}{\isacharbang}}}}[]
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
wenzelm@43467: \rail@end
wenzelm@43467: \rail@begin{5}{\indexdef{}{syntax}{locale}\hypertarget{syntax.locale}{\hyperlink{syntax.locale}{\mbox{\isa{locale}}}}}
wenzelm@43467: \rail@bar
wenzelm@43467: \rail@plus
wenzelm@43488: \rail@nont{\hyperlink{syntax.context-elem}{\mbox{\isa{context{\isaliteral{5F}{\isacharunderscore}}elem}}}}[]
wenzelm@43467: \rail@nextplus{1}
wenzelm@43467: \rail@endplus
wenzelm@43467: \rail@nextbar{2}
wenzelm@43488: \rail@nont{\hyperlink{syntax.locale-expr}{\mbox{\isa{locale{\isaliteral{5F}{\isacharunderscore}}expr}}}}[]
wenzelm@43467: \rail@bar
wenzelm@43467: \rail@nextbar{3}
wenzelm@43467: \rail@term{\isa{{\isaliteral{2B}{\isacharplus}}}}[]
wenzelm@43467: \rail@plus
wenzelm@43488: \rail@nont{\hyperlink{syntax.context-elem}{\mbox{\isa{context{\isaliteral{5F}{\isacharunderscore}}elem}}}}[]
wenzelm@43467: \rail@nextplus{4}
wenzelm@43467: \rail@endplus
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@end
wenzelm@43488: \rail@begin{12}{\indexdef{}{syntax}{context\_elem}\hypertarget{syntax.context-elem}{\hyperlink{syntax.context-elem}{\mbox{\isa{context{\isaliteral{5F}{\isacharunderscore}}elem}}}}}
wenzelm@43467: \rail@bar
wenzelm@43467: \rail@term{\isa{\isakeyword{fixes}}}[]
wenzelm@43467: \rail@plus
wenzelm@43467: \rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]
wenzelm@43467: \rail@nextplus{1}
wenzelm@43467: \rail@cterm{\isa{\isakeyword{and}}}[]
wenzelm@43467: \rail@endplus
wenzelm@43467: \rail@nextbar{2}
wenzelm@43467: \rail@term{\isa{\isakeyword{constrains}}}[]
wenzelm@43467: \rail@plus
wenzelm@43467: \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
wenzelm@43467: \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}}}[]
wenzelm@43467: \rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
wenzelm@43467: \rail@nextplus{3}
wenzelm@43467: \rail@cterm{\isa{\isakeyword{and}}}[]
wenzelm@43467: \rail@endplus
wenzelm@43467: \rail@nextbar{4}
wenzelm@43467: \rail@term{\isa{\isakeyword{assumes}}}[]
wenzelm@43467: \rail@plus
wenzelm@43467: \rail@nont{\hyperlink{syntax.props}{\mbox{\isa{props}}}}[]
wenzelm@43467: \rail@nextplus{5}
wenzelm@43467: \rail@cterm{\isa{\isakeyword{and}}}[]
wenzelm@43467: \rail@endplus
wenzelm@43467: \rail@nextbar{6}
wenzelm@43467: \rail@term{\isa{\isakeyword{defines}}}[]
wenzelm@43467: \rail@plus
wenzelm@43467: \rail@bar
wenzelm@43467: \rail@nextbar{7}
wenzelm@43467: \rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
wenzelm@43467: \rail@bar
wenzelm@43467: \rail@nextbar{7}
wenzelm@43576: \rail@nont{\hyperlink{syntax.prop-pat}{\mbox{\isa{prop{\isaliteral{5F}{\isacharunderscore}}pat}}}}[]
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@nextplus{8}
wenzelm@43467: \rail@cterm{\isa{\isakeyword{and}}}[]
wenzelm@43467: \rail@endplus
wenzelm@43467: \rail@nextbar{9}
wenzelm@43467: \rail@term{\isa{\isakeyword{notes}}}[]
wenzelm@43467: \rail@plus
wenzelm@43467: \rail@bar
wenzelm@43467: \rail@nextbar{10}
wenzelm@43467: \rail@nont{\hyperlink{syntax.thmdef}{\mbox{\isa{thmdef}}}}[]
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
wenzelm@43467: \rail@nextplus{11}
wenzelm@43467: \rail@cterm{\isa{\isakeyword{and}}}[]
wenzelm@43467: \rail@endplus
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@end
wenzelm@43467: \end{railoutput}
wenzelm@43467: 
wenzelm@27042: 
wenzelm@28788:   \begin{description}
wenzelm@27042:   
wenzelm@40685:   \item \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}loc\ {\isaliteral{3D}{\isacharequal}}\ import\ {\isaliteral{2B}{\isacharplus}}\ body{\isaliteral{22}{\isachardoublequote}}} defines a
wenzelm@27042:   new locale \isa{loc} as a context consisting of a certain view of
wenzelm@27042:   existing locales (\isa{import}) plus some additional elements
wenzelm@27042:   (\isa{body}).  Both \isa{import} and \isa{body} are optional;
wenzelm@27042:   the degenerate form \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}~\isa{loc} defines an empty
wenzelm@27042:   locale, which may still be useful to collect declarations of facts
wenzelm@27042:   later on.  Type-inference on locale expressions automatically takes
wenzelm@27042:   care of the most general typing that the combined context elements
wenzelm@27042:   may acquire.
wenzelm@27042: 
ballarin@33846:   The \isa{import} consists of a structured locale expression; see
ballarin@33846:   \secref{sec:proof-context} above.  Its for clause defines the local
ballarin@33846:   parameters of the \isa{import}.  In addition, locale parameters
ballarin@33846:   whose instantance is omitted automatically extend the (possibly
ballarin@33846:   empty) for clause: they are inserted at its beginning.  This means
ballarin@33846:   that these parameters may be referred to from within the expression
ballarin@33846:   and also in the subsequent context elements and provides a
ballarin@33846:   notational convenience for the inheritance of parameters in locale
ballarin@33846:   declarations.
wenzelm@27042: 
ballarin@33846:   The \isa{body} consists of context elements.
wenzelm@27042: 
wenzelm@28788:   \begin{description}
wenzelm@27042: 
wenzelm@40685:   \item \hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\ {\isaliteral{28}{\isacharparenleft}}mx{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} declares a local
wenzelm@40685:   parameter of type \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} and mixfix annotation \isa{mx} (both
wenzelm@40685:   are optional).  The special syntax declaration ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C5354525543545552453E}{\isasymSTRUCTURE}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'' means that \isa{x} may be referenced
wenzelm@27042:   implicitly in this context.
wenzelm@27042: 
wenzelm@40685:   \item \hyperlink{element.constrains}{\mbox{\isa{\isakeyword{constrains}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}} introduces a type
wenzelm@40685:   constraint \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} on the local parameter \isa{x}.  This
ballarin@38356:   element is deprecated.  The type constraint should be introduced in
ballarin@33846:   the for clause or the relevant \hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}} element.
wenzelm@27042: 
wenzelm@40685:   \item \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}
wenzelm@27042:   introduces local premises, similar to \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}} within a
wenzelm@27042:   proof (cf.\ \secref{sec:proof-context}).
wenzelm@27042: 
wenzelm@40685:   \item \hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{3A}{\isacharcolon}}\ x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t{\isaliteral{22}{\isachardoublequote}}} defines a previously
wenzelm@27042:   declared parameter.  This is similar to \hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}} within a
wenzelm@27042:   proof (cf.\ \secref{sec:proof-context}), but \hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}}
wenzelm@27042:   takes an equational proposition instead of variable-term pair.  The
wenzelm@27042:   left-hand side of the equation may have additional arguments, e.g.\
wenzelm@40685:   ``\hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}f\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t{\isaliteral{22}{\isachardoublequote}}}''.
wenzelm@27042: 
wenzelm@40685:   \item \hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\ {\isaliteral{3D}{\isacharequal}}\ b\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ b\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}
wenzelm@27042:   reconsiders facts within a local context.  Most notably, this may
wenzelm@27042:   include arbitrary declarations in any attribute specifications
wenzelm@27042:   included here, e.g.\ a local \hyperlink{attribute.simp}{\mbox{\isa{simp}}} rule.
wenzelm@27042: 
wenzelm@28788:   The initial \isa{import} specification of a locale expression
wenzelm@28788:   maintains a dynamic relation to the locales being referenced
wenzelm@28788:   (benefiting from any later fact declarations in the obvious manner).
wenzelm@27042: 
wenzelm@28788:   \end{description}
wenzelm@27042:   
wenzelm@40685:   Note that ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C49533E}{\isasymIS}}\ p\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ p\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'' patterns given
wenzelm@27042:   in the syntax of \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}} and \hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}} above
wenzelm@27042:   are illegal in locale definitions.  In the long goal format of
wenzelm@27042:   \secref{sec:goals}, term bindings may be included as expected,
wenzelm@27042:   though.
wenzelm@27042:   
ballarin@33846:   \medskip Locale specifications are ``closed up'' by
wenzelm@40685:   turning the given text into a predicate definition \isa{loc{\isaliteral{5F}{\isacharunderscore}}axioms} and deriving the original assumptions as local lemmas
wenzelm@27042:   (modulo local definitions).  The predicate statement covers only the
wenzelm@27042:   newly specified assumptions, omitting the content of included locale
wenzelm@27042:   expressions.  The full cumulative view is only provided on export,
wenzelm@27042:   involving another predicate \isa{loc} that refers to the complete
wenzelm@27042:   specification text.
wenzelm@27042:   
wenzelm@27042:   In any case, the predicate arguments are those locale parameters
wenzelm@27042:   that actually occur in the respective piece of text.  Also note that
wenzelm@27042:   these predicates operate at the meta-level in theory, but the locale
wenzelm@27042:   packages attempts to internalize statements according to the
wenzelm@40685:   object-logic setup (e.g.\ replacing \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}} by \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}}, and
wenzelm@40685:   \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{22}{\isachardoublequote}}} by \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}{\isaliteral{22}{\isachardoublequote}}} in HOL; see also
wenzelm@40685:   \secref{sec:object-logic}).  Separate introduction rules \isa{loc{\isaliteral{5F}{\isacharunderscore}}axioms{\isaliteral{2E}{\isachardot}}intro} and \isa{loc{\isaliteral{2E}{\isachardot}}intro} are provided as well.
wenzelm@27042:   
wenzelm@40685:   \item \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}locale}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}locale{\isaliteral{22}{\isachardoublequote}}} prints the
ballarin@33868:   contents of the named locale.  The command omits \hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}}
wenzelm@40685:   elements by default.  Use \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}locale}}}}\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{21}{\isacharbang}}{\isaliteral{22}{\isachardoublequote}}} to
ballarin@33868:   have them included.
wenzelm@27042: 
wenzelm@40685:   \item \hyperlink{command.print-locales}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}locales}}}} prints the names of all locales
wenzelm@27042:   of the current theory.
wenzelm@27042: 
wenzelm@40685:   \item \hyperlink{method.intro-locales}{\mbox{\isa{intro{\isaliteral{5F}{\isacharunderscore}}locales}}} and \hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isaliteral{5F}{\isacharunderscore}}locales}}}
wenzelm@27042:   repeatedly expand all introduction rules of locale predicates of the
wenzelm@40685:   theory.  While \hyperlink{method.intro-locales}{\mbox{\isa{intro{\isaliteral{5F}{\isacharunderscore}}locales}}} only applies the \isa{loc{\isaliteral{2E}{\isachardot}}intro} introduction rules and therefore does not decend to
wenzelm@40685:   assumptions, \hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isaliteral{5F}{\isacharunderscore}}locales}}} is more aggressive and applies
wenzelm@40685:   \isa{loc{\isaliteral{5F}{\isacharunderscore}}axioms{\isaliteral{2E}{\isachardot}}intro} as well.  Both methods are aware of locale
ballarin@28728:   specifications entailed by the context, both from target statements,
ballarin@28728:   and from interpretations (see below).  New goals that are entailed
ballarin@28728:   by the current context are discharged automatically.
wenzelm@27042: 
wenzelm@28788:   \end{description}%
wenzelm@27042: \end{isamarkuptext}%
wenzelm@27042: \isamarkuptrue%
wenzelm@27042: %
ballarin@33846: \isamarkupsubsection{Locale interpretations%
wenzelm@27042: }
wenzelm@27042: \isamarkuptrue%
wenzelm@27042: %
wenzelm@27042: \begin{isamarkuptext}%
ballarin@33846: Locale expressions may be instantiated, and the instantiated facts
ballarin@33846:   added to the current context.  This requires a proof of the
ballarin@33846:   instantiated specification and is called \emph{locale
ballarin@33846:   interpretation}.  Interpretation is possible in locales \hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}}, theories (command \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}) and
ballarin@33846:   also within a proof body (command \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}).
wenzelm@27042: 
wenzelm@27042:   \begin{matharray}{rcl}
wenzelm@40685:     \indexdef{}{command}{interpretation}\hypertarget{command.interpretation}{\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@40685:     \indexdef{}{command}{interpret}\hypertarget{command.interpret}{\hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7C}{\isacharbar}}\ proof{\isaliteral{28}{\isacharparenleft}}chain{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
ballarin@41682:     \indexdef{}{command}{sublocale}\hypertarget{command.sublocale}{\hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
ballarin@41683:     \indexdef{}{command}{print\_dependencies}\hypertarget{command.print-dependencies}{\hyperlink{command.print-dependencies}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}dependencies}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@40685:     \indexdef{}{command}{print\_interps}\hypertarget{command.print-interps}{\hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}interps}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@27042:   \end{matharray}
wenzelm@27042: 
wenzelm@43467:   \begin{railoutput}
wenzelm@43535: \rail@begin{2}{}
wenzelm@43467: \rail@term{\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}}[]
wenzelm@43488: \rail@nont{\hyperlink{syntax.locale-expr}{\mbox{\isa{locale{\isaliteral{5F}{\isacharunderscore}}expr}}}}[]
wenzelm@43467: \rail@bar
wenzelm@43467: \rail@nextbar{1}
wenzelm@43467: \rail@nont{\isa{equations}}[]
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@end
wenzelm@43535: \rail@begin{2}{}
wenzelm@43467: \rail@term{\hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}}[]
wenzelm@43488: \rail@nont{\hyperlink{syntax.locale-expr}{\mbox{\isa{locale{\isaliteral{5F}{\isacharunderscore}}expr}}}}[]
wenzelm@43467: \rail@bar
wenzelm@43467: \rail@nextbar{1}
wenzelm@43467: \rail@nont{\isa{equations}}[]
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@end
wenzelm@43575: \rail@begin{5}{}
wenzelm@43467: \rail@term{\hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}}}[]
wenzelm@43467: \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
wenzelm@43467: \rail@bar
wenzelm@43467: \rail@term{\isa{{\isaliteral{3C}{\isacharless}}}}[]
wenzelm@43467: \rail@nextbar{1}
wenzelm@43467: \rail@term{\isa{{\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}}}[]
wenzelm@43467: \rail@endbar
wenzelm@43488: \rail@nont{\hyperlink{syntax.locale-expr}{\mbox{\isa{locale{\isaliteral{5F}{\isacharunderscore}}expr}}}}[]
wenzelm@43575: \rail@cr{3}
wenzelm@43467: \rail@bar
wenzelm@43575: \rail@nextbar{4}
wenzelm@43467: \rail@nont{\isa{equations}}[]
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@end
wenzelm@43535: \rail@begin{2}{}
wenzelm@43467: \rail@term{\hyperlink{command.print-dependencies}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}dependencies}}}}}[]
wenzelm@43467: \rail@bar
wenzelm@43467: \rail@nextbar{1}
wenzelm@43467: \rail@term{\isa{{\isaliteral{21}{\isacharbang}}}}[]
wenzelm@43467: \rail@endbar
wenzelm@43488: \rail@nont{\hyperlink{syntax.locale-expr}{\mbox{\isa{locale{\isaliteral{5F}{\isacharunderscore}}expr}}}}[]
wenzelm@43467: \rail@end
wenzelm@43535: \rail@begin{1}{}
wenzelm@43467: \rail@term{\hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}interps}}}}}[]
wenzelm@43467: \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
wenzelm@43467: \rail@end
wenzelm@43467: \rail@begin{3}{\isa{equations}}
wenzelm@43467: \rail@term{\isa{\isakeyword{where}}}[]
wenzelm@43467: \rail@plus
wenzelm@43467: \rail@bar
wenzelm@43467: \rail@nextbar{1}
wenzelm@43467: \rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
wenzelm@43467: \rail@nextplus{2}
wenzelm@43467: \rail@cterm{\isa{\isakeyword{and}}}[]
wenzelm@43467: \rail@endplus
wenzelm@43467: \rail@end
wenzelm@43467: \end{railoutput}
wenzelm@43467: 
wenzelm@27042: 
wenzelm@28788:   \begin{description}
wenzelm@27042: 
wenzelm@40685:   \item \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}expr\ {\isaliteral{5C3C57484552453E}{\isasymWHERE}}\ eqns{\isaliteral{22}{\isachardoublequote}}}
ballarin@33846:   interprets \isa{expr} in the theory.  The command generates proof
ballarin@33846:   obligations for the instantiated specifications (assumes and defines
ballarin@33846:   elements).  Once these are discharged by the user, instantiated
ballarin@33846:   facts are added to the theory in a post-processing phase.
wenzelm@27042: 
ballarin@33846:   Additional equations, which are unfolded during
wenzelm@27042:   post-processing, may be given after the keyword \hyperlink{keyword.where}{\mbox{\isa{\isakeyword{where}}}}.
wenzelm@27042:   This is useful for interpreting concepts introduced through
ballarin@41682:   definitions.  The equations must be proved.
wenzelm@27042: 
wenzelm@27042:   The command is aware of interpretations already active in the
ballarin@28085:   theory, but does not simplify the goal automatically.  In order to
wenzelm@40685:   simplify the proof obligations use methods \hyperlink{method.intro-locales}{\mbox{\isa{intro{\isaliteral{5F}{\isacharunderscore}}locales}}}
wenzelm@40685:   or \hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isaliteral{5F}{\isacharunderscore}}locales}}}.  Post-processing is not applied to
ballarin@28085:   facts of interpretations that are already active.  This avoids
ballarin@28085:   duplication of interpreted facts, in particular.  Note that, in the
ballarin@28085:   case of a locale with import, parts of the interpretation may
ballarin@28085:   already be active.  The command will only process facts for new
ballarin@28085:   parts.
wenzelm@27042: 
wenzelm@27042:   Adding facts to locales has the effect of adding interpreted facts
ballarin@41682:   to the theory for all interpretations as well.  That is,
wenzelm@27042:   interpretations dynamically participate in any facts added to
ballarin@41682:   locales.  Note that if a theory inherits additional facts for a
ballarin@41682:   locale through one parent and an interpretation of that locale
ballarin@41682:   through another parent, the additional facts will not be
ballarin@41682:   interpreted.
wenzelm@27042: 
wenzelm@40685:   \item \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}expr\ {\isaliteral{5C3C57484552453E}{\isasymWHERE}}\ eqns{\isaliteral{22}{\isachardoublequote}}} interprets
ballarin@38356:   \isa{expr} in the proof context and is otherwise similar to
ballarin@38356:   interpretation in theories.  Note that rewrite rules given to
ballarin@41682:   \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}} after the \hyperlink{keyword.where}{\mbox{\isa{\isakeyword{where}}}} keyword should be
ballarin@41682:   explicitly universally quantified.
ballarin@41682: 
ballarin@41682:   \item \hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}name\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ expr\ {\isaliteral{5C3C57484552453E}{\isasymWHERE}}\ eqns{\isaliteral{22}{\isachardoublequote}}}
ballarin@41682:   interprets \isa{expr} in the locale \isa{name}.  A proof that
ballarin@41682:   the specification of \isa{name} implies the specification of
ballarin@41682:   \isa{expr} is required.  As in the localized version of the
ballarin@41682:   theorem command, the proof is in the context of \isa{name}.  After
ballarin@41682:   the proof obligation has been discharged, the facts of \isa{expr}
ballarin@41682:   become part of locale \isa{name} as \emph{derived} context
ballarin@41682:   elements and are available when the context \isa{name} is
ballarin@41682:   subsequently entered.  Note that, like import, this is dynamic:
ballarin@41682:   facts added to a locale part of \isa{expr} after interpretation
ballarin@41682:   become also available in \isa{name}.
ballarin@41682: 
ballarin@41682:   Only specification fragments of \isa{expr} that are not already
ballarin@41682:   part of \isa{name} (be it imported, derived or a derived fragment
ballarin@41682:   of the import) are considered in this process.  This enables
ballarin@41682:   circular interpretations provided that no infinite chains are
ballarin@41682:   generated in the locale hierarchy.
ballarin@41682: 
ballarin@41682:   If interpretations of \isa{name} exist in the current theory, the
ballarin@41682:   command adds interpretations for \isa{expr} as well, with the same
ballarin@41682:   qualifier, although only for fragments of \isa{expr} that are not
ballarin@41682:   interpreted in the theory already.
ballarin@41682: 
ballarin@41682:   Equations given after \hyperlink{keyword.where}{\mbox{\isa{\isakeyword{where}}}} amend the morphism through
ballarin@41682:   which \isa{expr} is interpreted.  This enables to map definitions
ballarin@41682:   from the interpreted locales to entities of \isa{name}.  This
ballarin@41682:   feature is experimental.
wenzelm@27042: 
ballarin@41683:   \item \hyperlink{command.print-dependencies}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}dependencies}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}expr{\isaliteral{22}{\isachardoublequote}}} is useful for
ballarin@41683:   understanding the effect of an interpretation of \isa{{\isaliteral{22}{\isachardoublequote}}expr{\isaliteral{22}{\isachardoublequote}}}.  It
ballarin@41683:   lists all locale instances for which interpretations would be added
ballarin@41683:   to the current context.  Variant \hyperlink{command.print-dependencies}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}dependencies}}}}\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{21}{\isacharbang}}{\isaliteral{22}{\isachardoublequote}}} prints all locale instances that
ballarin@41683:   would be considered for interpretation, and would be interpreted in
ballarin@41683:   an empty context (that is, without interpretations).
ballarin@41683: 
wenzelm@40685:   \item \hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}interps}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}locale{\isaliteral{22}{\isachardoublequote}}} lists all
wenzelm@40685:   interpretations of \isa{{\isaliteral{22}{\isachardoublequote}}locale{\isaliteral{22}{\isachardoublequote}}} in the current theory or proof
ballarin@38356:   context, including those due to a combination of a \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}} or \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}} and one or several
ballarin@38356:   \hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}} declarations.
ballarin@33868: 
wenzelm@28788:   \end{description}
wenzelm@27042: 
wenzelm@27042:   \begin{warn}
wenzelm@27042:     Since attributes are applied to interpreted theorems,
wenzelm@27042:     interpretation may modify the context of common proof tools, e.g.\
ballarin@33868:     the Simplifier or Classical Reasoner.  As the behavior of such
ballarin@33868:     tools is \emph{not} stable under interpretation morphisms, manual
ballarin@33868:     declarations might have to be added to the target context of the
ballarin@33868:     interpretation to revert such declarations.
wenzelm@27042:   \end{warn}
wenzelm@27042: 
wenzelm@27042:   \begin{warn}
ballarin@38356:     An interpretation in a theory or proof context may subsume previous
wenzelm@27042:     interpretations.  This happens if the same specification fragment
wenzelm@27042:     is interpreted twice and the instantiation of the second
wenzelm@27042:     interpretation is more general than the interpretation of the
ballarin@33846:     first.  The locale package does not attempt to remove subsumed
ballarin@33846:     interpretations.
wenzelm@27042:   \end{warn}%
wenzelm@27042: \end{isamarkuptext}%
wenzelm@27042: \isamarkuptrue%
wenzelm@27042: %
wenzelm@27042: \isamarkupsection{Classes \label{sec:class}%
wenzelm@27042: }
wenzelm@27042: \isamarkuptrue%
wenzelm@27042: %
wenzelm@27042: \begin{isamarkuptext}%
wenzelm@27042: A class is a particular locale with \emph{exactly one} type variable
wenzelm@40685:   \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}}.  Beyond the underlying locale, a corresponding type class
wenzelm@27042:   is established which is interpreted logically as axiomatic type
wenzelm@27042:   class \cite{Wenzel:1997:TPHOL} whose logical content are the
wenzelm@27042:   assumptions of the locale.  Thus, classes provide the full
wenzelm@27042:   generality of locales combined with the commodity of type classes
wenzelm@27042:   (notably type-inference).  See \cite{isabelle-classes} for a short
wenzelm@27042:   tutorial.
wenzelm@27042: 
wenzelm@27042:   \begin{matharray}{rcl}
wenzelm@40685:     \indexdef{}{command}{class}\hypertarget{command.class}{\hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@40685:     \indexdef{}{command}{instantiation}\hypertarget{command.instantiation}{\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@40685:     \indexdef{}{command}{instance}\hypertarget{command.instance}{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@43497:     \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@40685:     \indexdef{}{command}{subclass}\hypertarget{command.subclass}{\hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@40685:     \indexdef{}{command}{print\_classes}\hypertarget{command.print-classes}{\hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}classes}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@40685:     \indexdef{}{command}{class\_deps}\hypertarget{command.class-deps}{\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isaliteral{5F}{\isacharunderscore}}deps}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@40685:     \indexdef{}{method}{intro\_classes}\hypertarget{method.intro-classes}{\hyperlink{method.intro-classes}{\mbox{\isa{intro{\isaliteral{5F}{\isacharunderscore}}classes}}}} & : & \isa{method} \\
wenzelm@27042:   \end{matharray}
wenzelm@27042: 
wenzelm@43467:   \begin{railoutput}
wenzelm@43575: \rail@begin{2}{}
wenzelm@43467: \rail@term{\hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}}[]
wenzelm@43575: \rail@nont{\isa{class{\isaliteral{5F}{\isacharunderscore}}spec}}[]
wenzelm@43575: \rail@bar
wenzelm@43575: \rail@nextbar{1}
wenzelm@43575: \rail@term{\isa{\isakeyword{begin}}}[]
wenzelm@43575: \rail@endbar
wenzelm@43575: \rail@end
wenzelm@43575: \rail@begin{5}{\isa{class{\isaliteral{5F}{\isacharunderscore}}spec}}
wenzelm@43467: \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
wenzelm@43467: \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
wenzelm@43467: \rail@bar
wenzelm@43488: \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
wenzelm@43467: \rail@term{\isa{{\isaliteral{2B}{\isacharplus}}}}[]
wenzelm@43467: \rail@plus
wenzelm@43488: \rail@nont{\hyperlink{syntax.context-elem}{\mbox{\isa{context{\isaliteral{5F}{\isacharunderscore}}elem}}}}[]
wenzelm@43467: \rail@nextplus{1}
wenzelm@43467: \rail@endplus
wenzelm@43467: \rail@nextbar{2}
wenzelm@43488: \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
wenzelm@43467: \rail@nextbar{3}
wenzelm@43467: \rail@plus
wenzelm@43488: \rail@nont{\hyperlink{syntax.context-elem}{\mbox{\isa{context{\isaliteral{5F}{\isacharunderscore}}elem}}}}[]
wenzelm@43467: \rail@nextplus{4}
wenzelm@43467: \rail@endplus
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@end
wenzelm@43535: \rail@begin{2}{}
wenzelm@43467: \rail@term{\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}}[]
wenzelm@43467: \rail@plus
wenzelm@43467: \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
wenzelm@43467: \rail@nextplus{1}
wenzelm@43467: \rail@cterm{\isa{\isakeyword{and}}}[]
wenzelm@43467: \rail@endplus
wenzelm@43467: \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}}}[]
wenzelm@43467: \rail@nont{\hyperlink{syntax.arity}{\mbox{\isa{arity}}}}[]
wenzelm@43467: \rail@term{\isa{\isakeyword{begin}}}[]
wenzelm@43467: \rail@end
wenzelm@43575: \rail@begin{5}{}
wenzelm@43467: \rail@term{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}}[]
wenzelm@43575: \rail@bar
wenzelm@43575: \rail@nextbar{1}
wenzelm@43467: \rail@plus
wenzelm@43467: \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
wenzelm@43575: \rail@nextplus{2}
wenzelm@43467: \rail@cterm{\isa{\isakeyword{and}}}[]
wenzelm@43467: \rail@endplus
wenzelm@43467: \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}}}[]
wenzelm@43467: \rail@nont{\hyperlink{syntax.arity}{\mbox{\isa{arity}}}}[]
wenzelm@43575: \rail@nextbar{3}
wenzelm@43575: \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
wenzelm@43575: \rail@bar
wenzelm@43575: \rail@term{\isa{{\isaliteral{3C}{\isacharless}}}}[]
wenzelm@43575: \rail@nextbar{4}
wenzelm@43575: \rail@term{\isa{{\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}}}[]
wenzelm@43575: \rail@endbar
wenzelm@43575: \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
wenzelm@43575: \rail@endbar
wenzelm@43467: \rail@end
wenzelm@43535: \rail@begin{2}{}
wenzelm@43467: \rail@term{\hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}}[]
wenzelm@43467: \rail@bar
wenzelm@43467: \rail@nextbar{1}
wenzelm@43467: \rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
wenzelm@43467: \rail@end
wenzelm@43467: \end{railoutput}
wenzelm@43488: 
wenzelm@27042: 
wenzelm@28788:   \begin{description}
wenzelm@27042: 
wenzelm@40685:   \item \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{3D}{\isacharequal}}\ superclasses\ {\isaliteral{2B}{\isacharplus}}\ body{\isaliteral{22}{\isachardoublequote}}} defines
wenzelm@27042:   a new class \isa{c}, inheriting from \isa{superclasses}.  This
wenzelm@27042:   introduces a locale \isa{c} with import of all locales \isa{superclasses}.
wenzelm@27042: 
wenzelm@27042:   Any \hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}} in \isa{body} are lifted to the global
wenzelm@40685:   theory level (\emph{class operations} \isa{{\isaliteral{22}{\isachardoublequote}}f\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ f\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} of class \isa{c}), mapping the local type parameter
wenzelm@40685:   \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}} to a schematic type variable \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ c{\isaliteral{22}{\isachardoublequote}}}.
wenzelm@27042: 
wenzelm@27042:   Likewise, \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}} in \isa{body} are also lifted,
wenzelm@40685:   mapping each local parameter \isa{{\isaliteral{22}{\isachardoublequote}}f\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} to its
wenzelm@40685:   corresponding global constant \isa{{\isaliteral{22}{\isachardoublequote}}f\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ c{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}}.  The
wenzelm@40685:   corresponding introduction rule is provided as \isa{c{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{5F}{\isacharunderscore}}axioms{\isaliteral{2E}{\isachardot}}intro}.  This rule should be rarely needed directly
wenzelm@40685:   --- the \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isaliteral{5F}{\isacharunderscore}}classes}}} method takes care of the details of
wenzelm@27042:   class membership proofs.
wenzelm@27042: 
wenzelm@40685:   \item \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}t\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}s\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ s\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}s\ {\isaliteral{5C3C424547494E3E}{\isasymBEGIN}}{\isaliteral{22}{\isachardoublequote}}} opens a theory target (cf.\ \secref{sec:target}) which
wenzelm@40685:   allows to specify class operations \isa{{\isaliteral{22}{\isachardoublequote}}f\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ f\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} corresponding
wenzelm@40685:   to sort \isa{s} at the particular type instance \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ s\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ s\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}}.  A plain \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} command in the
wenzelm@28788:   target body poses a goal stating these type arities.  The target is
wenzelm@28788:   concluded by an \indexref{local}{command}{end}\hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}} command.
wenzelm@27042: 
wenzelm@27042:   Note that a list of simultaneous type constructors may be given;
haftmann@31908:   this corresponds nicely to mutually recursive type definitions, e.g.\
wenzelm@27042:   in Isabelle/HOL.
wenzelm@27042: 
wenzelm@28788:   \item \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} in an instantiation target body sets
wenzelm@40685:   up a goal stating the type arities claimed at the opening \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}.  The proof would usually proceed by \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isaliteral{5F}{\isacharunderscore}}classes}}}, and then establish the characteristic theorems of
wenzelm@27042:   the type classes involved.  After finishing the proof, the
wenzelm@27042:   background theory will be augmented by the proven type arities.
wenzelm@27042: 
wenzelm@40685:   On the theory level, \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}t\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}s\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ s\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}s{\isaliteral{22}{\isachardoublequote}}} provides a convenient way to instantiate a type class with no
wenzelm@37115:   need to specify operations: one can continue with the
haftmann@31681:   instantiation proof immediately.
haftmann@31681: 
wenzelm@28788:   \item \hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}~\isa{c} in a class context for class
wenzelm@27042:   \isa{d} sets up a goal stating that class \isa{c} is logically
wenzelm@27042:   contained in class \isa{d}.  After finishing the proof, class
wenzelm@27042:   \isa{d} is proven to be subclass \isa{c} and the locale \isa{c} is interpreted into \isa{d} simultaneously.
wenzelm@27042: 
haftmann@31681:   A weakend form of this is available through a further variant of
wenzelm@40685:   \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}:  \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}} opens
wenzelm@40685:   a proof that class \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}} implies \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}} without reference
haftmann@31681:   to the underlying locales;  this is useful if the properties to prove
haftmann@31681:   the logical connection are not sufficent on the locale level but on
haftmann@31681:   the theory level.
haftmann@31681: 
wenzelm@40685:   \item \hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}classes}}}} prints all classes in the current
wenzelm@27042:   theory.
wenzelm@27042: 
wenzelm@40685:   \item \hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isaliteral{5F}{\isacharunderscore}}deps}}}} visualizes all classes and their
haftmann@29706:   subclass relations as a Hasse diagram.
haftmann@29706: 
wenzelm@40685:   \item \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isaliteral{5F}{\isacharunderscore}}classes}}} repeatedly expands all class
wenzelm@27042:   introduction rules of this theory.  Note that this method usually
wenzelm@27042:   needs not be named explicitly, as it is already included in the
wenzelm@27042:   default proof step (e.g.\ of \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}).  In particular,
wenzelm@27042:   instantiation of trivial (syntactic) classes may be performed by a
wenzelm@40685:   single ``\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}}}}'' proof step.
wenzelm@27042: 
wenzelm@28788:   \end{description}%
wenzelm@27042: \end{isamarkuptext}%
wenzelm@27042: \isamarkuptrue%
wenzelm@27042: %
wenzelm@27042: \isamarkupsubsection{The class target%
wenzelm@27042: }
wenzelm@27042: \isamarkuptrue%
wenzelm@27042: %
wenzelm@27042: \begin{isamarkuptext}%
wenzelm@27042: %FIXME check
wenzelm@27042: 
wenzelm@27042:   A named context may refer to a locale (cf.\ \secref{sec:target}).
wenzelm@27042:   If this locale is also a class \isa{c}, apart from the common
wenzelm@27042:   locale target behaviour the following happens.
wenzelm@27042: 
wenzelm@27042:   \begin{itemize}
wenzelm@27042: 
wenzelm@40685:   \item Local constant declarations \isa{{\isaliteral{22}{\isachardoublequote}}g{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} referring to the
wenzelm@40685:   local type parameter \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}} and local parameters \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}}
wenzelm@40685:   are accompanied by theory-level constants \isa{{\isaliteral{22}{\isachardoublequote}}g{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ c{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}}
wenzelm@40685:   referring to theory-level class operations \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ c{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}}.
wenzelm@27042: 
wenzelm@27042:   \item Local theorem bindings are lifted as are assumptions.
wenzelm@27042: 
wenzelm@40685:   \item Local syntax refers to local operations \isa{{\isaliteral{22}{\isachardoublequote}}g{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} and
wenzelm@40685:   global operations \isa{{\isaliteral{22}{\isachardoublequote}}g{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ c{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} uniformly.  Type inference
wenzelm@27042:   resolves ambiguities.  In rare cases, manual type annotations are
wenzelm@27042:   needed.
wenzelm@27042:   
wenzelm@27042:   \end{itemize}%
wenzelm@27042: \end{isamarkuptext}%
wenzelm@27042: \isamarkuptrue%
wenzelm@27042: %
haftmann@37768: \isamarkupsubsection{Co-regularity of type classes and arities%
haftmann@37768: }
haftmann@37768: \isamarkuptrue%
haftmann@37768: %
haftmann@37768: \begin{isamarkuptext}%
haftmann@37768: The class relation together with the collection of
haftmann@37768:   type-constructor arities must obey the principle of
haftmann@37768:   \emph{co-regularity} as defined below.
haftmann@37768: 
haftmann@37768:   \medskip For the subsequent formulation of co-regularity we assume
haftmann@37768:   that the class relation is closed by transitivity and reflexivity.
wenzelm@40685:   Moreover the collection of arities \isa{{\isaliteral{22}{\isachardoublequote}}t\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec s{\isaliteral{29}{\isacharparenright}}c{\isaliteral{22}{\isachardoublequote}}} is
wenzelm@40685:   completed such that \isa{{\isaliteral{22}{\isachardoublequote}}t\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec s{\isaliteral{29}{\isacharparenright}}c{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ c{\isaliteral{27}{\isacharprime}}{\isaliteral{22}{\isachardoublequote}}}
wenzelm@40685:   implies \isa{{\isaliteral{22}{\isachardoublequote}}t\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec s{\isaliteral{29}{\isacharparenright}}c{\isaliteral{27}{\isacharprime}}{\isaliteral{22}{\isachardoublequote}}} for all such declarations.
haftmann@37768: 
haftmann@37768:   Treating sorts as finite sets of classes (meaning the intersection),
wenzelm@40685:   the class relation \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}} is extended to sorts as
haftmann@37768:   follows:
haftmann@37768:   \[
wenzelm@40685:     \isa{{\isaliteral{22}{\isachardoublequote}}s\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ s\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ s\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ s\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}}
haftmann@37768:   \]
haftmann@37768: 
haftmann@37768:   This relation on sorts is further extended to tuples of sorts (of
haftmann@37768:   the same length) in the component-wise way.
haftmann@37768: 
haftmann@37768:   \smallskip Co-regularity of the class relation together with the
haftmann@37768:   arities relation means:
haftmann@37768:   \[
wenzelm@40685:     \isa{{\isaliteral{22}{\isachardoublequote}}t\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec s\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ t\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec s\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec s\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec s\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}}
haftmann@37768:   \]
haftmann@37768:   \noindent for all such arities.  In other words, whenever the result
haftmann@37768:   classes of some type-constructor arities are related, then the
haftmann@37768:   argument sorts need to be related in the same way.
haftmann@37768: 
haftmann@37768:   \medskip Co-regularity is a very fundamental property of the
haftmann@37768:   order-sorted algebra of types.  For example, it entails principle
haftmann@37768:   types and most general unifiers, e.g.\ see \cite{nipkow-prehofer}.%
haftmann@37768: \end{isamarkuptext}%
haftmann@37768: \isamarkuptrue%
haftmann@37768: %
wenzelm@27042: \isamarkupsection{Unrestricted overloading%
wenzelm@27042: }
wenzelm@27042: \isamarkuptrue%
wenzelm@27042: %
wenzelm@27042: \begin{isamarkuptext}%
wenzelm@27042: Isabelle/Pure's definitional schemes support certain forms of
haftmann@31047:   overloading (see \secref{sec:consts}).  Overloading means that a
wenzelm@40685:   constant being declared as \isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ decl{\isaliteral{22}{\isachardoublequote}}} may be
haftmann@31047:   defined separately on type instances
wenzelm@40685:   \isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}\ t\ decl{\isaliteral{22}{\isachardoublequote}}}
haftmann@31047:   for each type constructor \isa{t}.  At most occassions
wenzelm@27042:   overloading will be used in a Haskell-like fashion together with
wenzelm@27042:   type classes by means of \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} (see
wenzelm@27042:   \secref{sec:class}).  Sometimes low-level overloading is desirable.
wenzelm@27042:   The \hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}} target provides a convenient view for
wenzelm@27042:   end-users.
wenzelm@27042: 
wenzelm@27042:   \begin{matharray}{rcl}
wenzelm@40685:     \indexdef{}{command}{overloading}\hypertarget{command.overloading}{\hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@27042:   \end{matharray}
wenzelm@27042: 
wenzelm@43467:   \begin{railoutput}
wenzelm@43575: \rail@begin{2}{}
wenzelm@43467: \rail@term{\hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}}}[]
wenzelm@43467: \rail@plus
wenzelm@43575: \rail@nont{\isa{spec}}[]
wenzelm@43575: \rail@nextplus{1}
wenzelm@43575: \rail@endplus
wenzelm@43575: \rail@term{\isa{\isakeyword{begin}}}[]
wenzelm@43575: \rail@end
wenzelm@43575: \rail@begin{2}{\isa{spec}}
wenzelm@43488: \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
wenzelm@43467: \rail@bar
wenzelm@43467: \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}}}[]
wenzelm@43575: \rail@nextbar{1}
wenzelm@43467: \rail@term{\isa{{\isaliteral{5C3C65717569763E}{\isasymequiv}}}}[]
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
wenzelm@43467: \rail@bar
wenzelm@43575: \rail@nextbar{1}
wenzelm@43467: \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
wenzelm@43467: \rail@term{\isa{\isakeyword{unchecked}}}[]
wenzelm@43467: \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@end
wenzelm@43467: \end{railoutput}
wenzelm@43488: 
wenzelm@27042: 
wenzelm@28788:   \begin{description}
wenzelm@27042: 
wenzelm@40685:   \item \hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C414E443E}{\isasymAND}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C424547494E3E}{\isasymBEGIN}}{\isaliteral{22}{\isachardoublequote}}}
wenzelm@27042:   opens a theory target (cf.\ \secref{sec:target}) which allows to
wenzelm@27042:   specify constants with overloaded definitions.  These are identified
wenzelm@40685:   by an explicitly given mapping from variable names \isa{{\isaliteral{22}{\isachardoublequote}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} to
wenzelm@40685:   constants \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} at particular type instances.  The
wenzelm@28788:   definitions themselves are established using common specification
wenzelm@40685:   tools, using the names \isa{{\isaliteral{22}{\isachardoublequote}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} as reference to the
wenzelm@28788:   corresponding constants.  The target is concluded by \hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}}.
wenzelm@27042: 
wenzelm@40685:   A \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}unchecked{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} option disables global dependency checks for
wenzelm@27042:   the corresponding definition, which is occasionally useful for
haftmann@31047:   exotic overloading (see \secref{sec:consts} for a precise description).
haftmann@31047:   It is at the discretion of the user to avoid
wenzelm@27042:   malformed theory specifications!
wenzelm@27042: 
wenzelm@28788:   \end{description}%
wenzelm@27042: \end{isamarkuptext}%
wenzelm@27042: \isamarkuptrue%
wenzelm@27042: %
wenzelm@27042: \isamarkupsection{Incorporating ML code \label{sec:ML}%
wenzelm@27042: }
wenzelm@27042: \isamarkuptrue%
wenzelm@27042: %
wenzelm@27042: \begin{isamarkuptext}%
wenzelm@27042: \begin{matharray}{rcl}
wenzelm@40685:     \indexdef{}{command}{use}\hypertarget{command.use}{\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@40685:     \indexdef{}{command}{ML}\hypertarget{command.ML}{\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@40685:     \indexdef{}{command}{ML\_prf}\hypertarget{command.ML-prf}{\hyperlink{command.ML-prf}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}prf}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@40685:     \indexdef{}{command}{ML\_val}\hypertarget{command.ML-val}{\hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}val}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}any\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@40685:     \indexdef{}{command}{ML\_command}\hypertarget{command.ML-command}{\hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}command}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}any\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@40685:     \indexdef{}{command}{setup}\hypertarget{command.setup}{\hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@40685:     \indexdef{}{command}{local\_setup}\hypertarget{command.local-setup}{\hyperlink{command.local-setup}{\mbox{\isa{\isacommand{local{\isaliteral{5F}{\isacharunderscore}}setup}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@40685:     \indexdef{}{command}{attribute\_setup}\hypertarget{command.attribute-setup}{\hyperlink{command.attribute-setup}{\mbox{\isa{\isacommand{attribute{\isaliteral{5F}{\isacharunderscore}}setup}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@27042:   \end{matharray}
wenzelm@27042: 
wenzelm@43467:   \begin{railoutput}
wenzelm@43535: \rail@begin{1}{}
wenzelm@43467: \rail@term{\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}}[]
wenzelm@43467: \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
wenzelm@43467: \rail@end
wenzelm@43535: \rail@begin{6}{}
wenzelm@43467: \rail@bar
wenzelm@43467: \rail@term{\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}}[]
wenzelm@43467: \rail@nextbar{1}
wenzelm@43467: \rail@term{\hyperlink{command.ML-prf}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}prf}}}}}[]
wenzelm@43467: \rail@nextbar{2}
wenzelm@43467: \rail@term{\hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}val}}}}}[]
wenzelm@43467: \rail@nextbar{3}
wenzelm@43467: \rail@term{\hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}command}}}}}[]
wenzelm@43467: \rail@nextbar{4}
wenzelm@43467: \rail@term{\hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}}[]
wenzelm@43467: \rail@nextbar{5}
wenzelm@43467: \rail@term{\hyperlink{command.local-setup}{\mbox{\isa{\isacommand{local{\isaliteral{5F}{\isacharunderscore}}setup}}}}}[]
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
wenzelm@43467: \rail@end
wenzelm@43684: \rail@begin{2}{}
wenzelm@43467: \rail@term{\hyperlink{command.attribute-setup}{\mbox{\isa{\isacommand{attribute{\isaliteral{5F}{\isacharunderscore}}setup}}}}}[]
wenzelm@43467: \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
wenzelm@43467: \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
wenzelm@43467: \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
wenzelm@43684: \rail@bar
wenzelm@43684: \rail@nextbar{1}
wenzelm@43467: \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
wenzelm@43684: \rail@endbar
wenzelm@43467: \rail@end
wenzelm@43467: \end{railoutput}
wenzelm@43467: 
wenzelm@27042: 
wenzelm@28788:   \begin{description}
wenzelm@27042: 
wenzelm@40685:   \item \hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}file{\isaliteral{22}{\isachardoublequote}}} reads and executes ML
wenzelm@40685:   commands from \isa{{\isaliteral{22}{\isachardoublequote}}file{\isaliteral{22}{\isachardoublequote}}}.  The current theory context is passed
wenzelm@28788:   down to the ML toplevel and may be modified, using \verb|Context.>>| or derived ML commands.  The file name is checked with
wenzelm@27042:   the \indexref{}{keyword}{uses}\hyperlink{keyword.uses}{\mbox{\isa{\isakeyword{uses}}}} dependency declaration given in the theory
wenzelm@27042:   header (see also \secref{sec:begin-thy}).
wenzelm@28281: 
wenzelm@28281:   Top-level ML bindings are stored within the (global or local) theory
wenzelm@28281:   context.
wenzelm@27042:   
wenzelm@40685:   \item \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}text{\isaliteral{22}{\isachardoublequote}}} is similar to \hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}},
wenzelm@40685:   but executes ML commands directly from the given \isa{{\isaliteral{22}{\isachardoublequote}}text{\isaliteral{22}{\isachardoublequote}}}.
wenzelm@28788:   Top-level ML bindings are stored within the (global or local) theory
wenzelm@28788:   context.
wenzelm@28281: 
wenzelm@40685:   \item \hyperlink{command.ML-prf}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}prf}}}} is analogous to \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}} but works
wenzelm@28788:   within a proof context.
wenzelm@28281: 
wenzelm@28281:   Top-level ML bindings are stored within the proof context in a
wenzelm@28281:   purely sequential fashion, disregarding the nested proof structure.
wenzelm@40685:   ML bindings introduced by \hyperlink{command.ML-prf}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}prf}}}} are discarded at the
wenzelm@28281:   end of the proof.
wenzelm@27042: 
wenzelm@40685:   \item \hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}val}}}} and \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}command}}}} are diagnostic
wenzelm@28788:   versions of \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}, which means that the context may not be
wenzelm@40685:   updated.  \hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}val}}}} echos the bindings produced at the ML
wenzelm@40685:   toplevel, but \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}command}}}} is silent.
wenzelm@27042:   
wenzelm@40685:   \item \hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}text{\isaliteral{22}{\isachardoublequote}}} changes the current theory
wenzelm@40685:   context by applying \isa{{\isaliteral{22}{\isachardoublequote}}text{\isaliteral{22}{\isachardoublequote}}}, which refers to an ML expression
wenzelm@30463:   of type \verb|theory -> theory|.  This enables to initialize
wenzelm@30463:   any object-logic specific tools and packages written in ML, for
wenzelm@30463:   example.
wenzelm@30463: 
wenzelm@40685:   \item \hyperlink{command.local-setup}{\mbox{\isa{\isacommand{local{\isaliteral{5F}{\isacharunderscore}}setup}}}} is similar to \hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}} for
wenzelm@30463:   a local theory context, and an ML expression of type \verb|local_theory -> local_theory|.  This allows to
wenzelm@30463:   invoke local theory specification packages without going through
wenzelm@30463:   concrete outer syntax, for example.
wenzelm@28788: 
wenzelm@40685:   \item \hyperlink{command.attribute-setup}{\mbox{\isa{\isacommand{attribute{\isaliteral{5F}{\isacharunderscore}}setup}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}name\ {\isaliteral{3D}{\isacharequal}}\ text\ description{\isaliteral{22}{\isachardoublequote}}}
wenzelm@40685:   defines an attribute in the current theory.  The given \isa{{\isaliteral{22}{\isachardoublequote}}text{\isaliteral{22}{\isachardoublequote}}} has to be an ML expression of type
wenzelm@30529:   \verb|attribute context_parser|, cf.\ basic parsers defined in
wenzelm@30529:   structure \verb|Args| and \verb|Attrib|.
wenzelm@30529: 
wenzelm@30529:   In principle, attributes can operate both on a given theorem and the
wenzelm@30529:   implicit context, although in practice only one is modified and the
wenzelm@30529:   other serves as parameter.  Here are examples for these two cases:
wenzelm@30529: 
wenzelm@30529:   \end{description}%
wenzelm@30529: \end{isamarkuptext}%
wenzelm@30529: \isamarkuptrue%
wenzelm@30529: %
wenzelm@30529: \isadelimML
wenzelm@43575: \ \ %
wenzelm@30529: \endisadelimML
wenzelm@30529: %
wenzelm@30529: \isatagML
wenzelm@40685: \isacommand{attribute{\isaliteral{5F}{\isacharunderscore}}setup}\isamarkupfalse%
wenzelm@40685: \ my{\isaliteral{5F}{\isacharunderscore}}rule\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
wenzelm@43575: \ \ \ \ Attrib{\isaliteral{2E}{\isachardot}}thms\ {\isaliteral{3E}{\isachargreater}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}fn\ ths\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\isanewline
wenzelm@43575: \ \ \ \ \ \ Thm{\isaliteral{2E}{\isachardot}}rule{\isaliteral{5F}{\isacharunderscore}}attribute\isanewline
wenzelm@43575: \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}fn\ context{\isaliteral{3A}{\isacharcolon}}\ Context{\isaliteral{2E}{\isachardot}}generic\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ fn\ th{\isaliteral{3A}{\isacharcolon}}\ thm\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\isanewline
wenzelm@40685: \ \ \ \ \ \ \ \ \ \ let\ val\ th{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ th\ OF\ ths\isanewline
wenzelm@44140: \ \ \ \ \ \ \ \ \ \ in\ th{\isaliteral{27}{\isacharprime}}\ end{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
wenzelm@30529: \isanewline
wenzelm@43575: \ \ \isacommand{attribute{\isaliteral{5F}{\isacharunderscore}}setup}\isamarkupfalse%
wenzelm@40685: \ my{\isaliteral{5F}{\isacharunderscore}}declaration\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
wenzelm@43575: \ \ \ \ Attrib{\isaliteral{2E}{\isachardot}}thms\ {\isaliteral{3E}{\isachargreater}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}fn\ ths\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\isanewline
wenzelm@43575: \ \ \ \ \ \ Thm{\isaliteral{2E}{\isachardot}}declaration{\isaliteral{5F}{\isacharunderscore}}attribute\isanewline
wenzelm@43575: \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}fn\ th{\isaliteral{3A}{\isacharcolon}}\ thm\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ fn\ context{\isaliteral{3A}{\isacharcolon}}\ Context{\isaliteral{2E}{\isachardot}}generic\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\isanewline
wenzelm@40685: \ \ \ \ \ \ \ \ \ \ let\ val\ context{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ context\isanewline
wenzelm@44140: \ \ \ \ \ \ \ \ \ \ in\ context{\isaliteral{27}{\isacharprime}}\ end{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}%
wenzelm@30529: \endisatagML
wenzelm@30529: {\isafoldML}%
wenzelm@30529: %
wenzelm@30529: \isadelimML
wenzelm@30529: %
wenzelm@30529: \endisadelimML
wenzelm@30529: %
wenzelm@27042: \isamarkupsection{Primitive specification elements%
wenzelm@27042: }
wenzelm@27042: \isamarkuptrue%
wenzelm@27042: %
wenzelm@27042: \isamarkupsubsection{Type classes and sorts \label{sec:classes}%
wenzelm@27042: }
wenzelm@27042: \isamarkuptrue%
wenzelm@27042: %
wenzelm@27042: \begin{isamarkuptext}%
wenzelm@27042: \begin{matharray}{rcll}
wenzelm@40685:     \indexdef{}{command}{classes}\hypertarget{command.classes}{\hyperlink{command.classes}{\mbox{\isa{\isacommand{classes}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@40685:     \indexdef{}{command}{classrel}\hypertarget{command.classrel}{\hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} & (axiomatic!) \\
wenzelm@40685:     \indexdef{}{command}{default\_sort}\hypertarget{command.default-sort}{\hyperlink{command.default-sort}{\mbox{\isa{\isacommand{default{\isaliteral{5F}{\isacharunderscore}}sort}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}}
wenzelm@27042:   \end{matharray}
wenzelm@27042: 
wenzelm@43467:   \begin{railoutput}
wenzelm@43535: \rail@begin{2}{}
wenzelm@43467: \rail@term{\hyperlink{command.classes}{\mbox{\isa{\isacommand{classes}}}}}[]
wenzelm@43467: \rail@plus
wenzelm@43467: \rail@nont{\hyperlink{syntax.classdecl}{\mbox{\isa{classdecl}}}}[]
wenzelm@43467: \rail@nextplus{1}
wenzelm@43467: \rail@endplus
wenzelm@43467: \rail@end
wenzelm@43535: \rail@begin{3}{}
wenzelm@43467: \rail@term{\hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}}[]
wenzelm@43467: \rail@plus
wenzelm@43467: \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
wenzelm@43467: \rail@bar
wenzelm@43467: \rail@term{\isa{{\isaliteral{3C}{\isacharless}}}}[]
wenzelm@43467: \rail@nextbar{1}
wenzelm@43467: \rail@term{\isa{{\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}}}[]
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
wenzelm@43467: \rail@nextplus{2}
wenzelm@43467: \rail@cterm{\isa{\isakeyword{and}}}[]
wenzelm@43467: \rail@endplus
wenzelm@43467: \rail@end
wenzelm@43535: \rail@begin{1}{}
wenzelm@43467: \rail@term{\hyperlink{command.default-sort}{\mbox{\isa{\isacommand{default{\isaliteral{5F}{\isacharunderscore}}sort}}}}}[]
wenzelm@43467: \rail@nont{\hyperlink{syntax.sort}{\mbox{\isa{sort}}}}[]
wenzelm@43467: \rail@end
wenzelm@43467: \end{railoutput}
wenzelm@43467: 
wenzelm@27042: 
wenzelm@28788:   \begin{description}
wenzelm@27042: 
wenzelm@40685:   \item \hyperlink{command.classes}{\mbox{\isa{\isacommand{classes}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} declares class
wenzelm@40685:   \isa{c} to be a subclass of existing classes \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}.
wenzelm@28788:   Isabelle implicitly maintains the transitive closure of the class
wenzelm@28788:   hierarchy.  Cyclic class structures are not permitted.
wenzelm@27042: 
wenzelm@40685:   \item \hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}} states subclass
wenzelm@40685:   relations between existing classes \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}}.
haftmann@37768:   This is done axiomatically!  The \indexref{}{command}{subclass}\hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}} and
haftmann@37768:   \indexref{}{command}{instance}\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} commands (see \secref{sec:class}) provide
haftmann@37768:   a way to introduce proven class relations.
wenzelm@27042: 
wenzelm@40685:   \item \hyperlink{command.default-sort}{\mbox{\isa{\isacommand{default{\isaliteral{5F}{\isacharunderscore}}sort}}}}~\isa{s} makes sort \isa{s} the
wenzelm@28788:   new default sort for any type variable that is given explicitly in
wenzelm@28788:   the text, but lacks a sort constraint (wrt.\ the current context).
wenzelm@28788:   Type variables generated by type inference are not affected.
wenzelm@27042: 
wenzelm@28788:   Usually the default sort is only changed when defining a new
wenzelm@28788:   object-logic.  For example, the default sort in Isabelle/HOL is
wenzelm@40270:   \isa{type}, the class of all HOL types.
wenzelm@28788: 
wenzelm@28788:   When merging theories, the default sorts of the parents are
wenzelm@28788:   logically intersected, i.e.\ the representations as lists of classes
wenzelm@28788:   are joined.
wenzelm@28788: 
wenzelm@28788:   \end{description}%
wenzelm@27042: \end{isamarkuptext}%
wenzelm@27042: \isamarkuptrue%
wenzelm@27042: %
wenzelm@27042: \isamarkupsubsection{Types and type abbreviations \label{sec:types-pure}%
wenzelm@27042: }
wenzelm@27042: \isamarkuptrue%
wenzelm@27042: %
wenzelm@27042: \begin{isamarkuptext}%
wenzelm@27042: \begin{matharray}{rcll}
wenzelm@41497:     \indexdef{}{command}{type\_synonym}\hypertarget{command.type-synonym}{\hyperlink{command.type-synonym}{\mbox{\isa{\isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@40685:     \indexdef{}{command}{typedecl}\hypertarget{command.typedecl}{\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@40685:     \indexdef{}{command}{arities}\hypertarget{command.arities}{\hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} & (axiomatic!) \\
wenzelm@27042:   \end{matharray}
wenzelm@27042: 
wenzelm@43467:   \begin{railoutput}
wenzelm@43535: \rail@begin{2}{}
wenzelm@43467: \rail@term{\hyperlink{command.type-synonym}{\mbox{\isa{\isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}}}}}[]
wenzelm@43467: \rail@nont{\hyperlink{syntax.typespec}{\mbox{\isa{typespec}}}}[]
wenzelm@43467: \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
wenzelm@43467: \rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
wenzelm@43467: \rail@bar
wenzelm@43467: \rail@nextbar{1}
wenzelm@43467: \rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@end
wenzelm@43535: \rail@begin{2}{}
wenzelm@43467: \rail@term{\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}}[]
wenzelm@43467: \rail@nont{\hyperlink{syntax.typespec}{\mbox{\isa{typespec}}}}[]
wenzelm@43467: \rail@bar
wenzelm@43467: \rail@nextbar{1}
wenzelm@43467: \rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@end
wenzelm@43535: \rail@begin{2}{}
wenzelm@43467: \rail@term{\hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}}[]
wenzelm@43467: \rail@plus
wenzelm@43467: \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
wenzelm@43467: \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}}}[]
wenzelm@43467: \rail@nont{\hyperlink{syntax.arity}{\mbox{\isa{arity}}}}[]
wenzelm@43467: \rail@nextplus{1}
wenzelm@43467: \rail@endplus
wenzelm@43467: \rail@end
wenzelm@43467: \end{railoutput}
wenzelm@43467: 
wenzelm@27042: 
wenzelm@28788:   \begin{description}
wenzelm@27042: 
wenzelm@41497:   \item \hyperlink{command.type-synonym}{\mbox{\isa{\isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}\ t\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}}
wenzelm@41497:   introduces a \emph{type synonym} \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}} for the
wenzelm@41497:   existing type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}}.  Unlike actual type definitions, as are
wenzelm@41497:   available in Isabelle/HOL for example, type synonyms are merely
wenzelm@41497:   syntactic abbreviations without any logical significance.
wenzelm@41497:   Internally, type synonyms are fully expanded.
wenzelm@27042:   
wenzelm@40685:   \item \hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}} declares a new
wenzelm@28788:   type constructor \isa{t}.  If the object-logic defines a base sort
wenzelm@28788:   \isa{s}, then the constructor is declared to operate on that, via
wenzelm@40685:   the axiomatic specification \hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}t\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}s{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ s{\isaliteral{29}{\isacharparenright}}s{\isaliteral{22}{\isachardoublequote}}}.
wenzelm@27042: 
wenzelm@40685:   \item \hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}t\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}s\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ s\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}s{\isaliteral{22}{\isachardoublequote}}} augments
wenzelm@28788:   Isabelle's order-sorted signature of types by new type constructor
haftmann@35282:   arities.  This is done axiomatically!  The \indexref{}{command}{instantiation}\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}
haftmann@35282:   target (see \secref{sec:class}) provides a way to introduce
wenzelm@28788:   proven type arities.
wenzelm@27042: 
wenzelm@28788:   \end{description}%
wenzelm@28788: \end{isamarkuptext}%
wenzelm@28788: \isamarkuptrue%
wenzelm@28788: %
wenzelm@27042: \isamarkupsubsection{Constants and definitions \label{sec:consts}%
wenzelm@27042: }
wenzelm@27042: \isamarkuptrue%
wenzelm@27042: %
wenzelm@27042: \begin{isamarkuptext}%
wenzelm@27042: Definitions essentially express abbreviations within the logic.  The
wenzelm@40685:   simplest form of a definition is \isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t{\isaliteral{22}{\isachardoublequote}}}, where \isa{c} is a newly declared constant.  Isabelle also allows derived forms
wenzelm@27042:   where the arguments of \isa{c} appear on the left, abbreviating a
wenzelm@40685:   prefix of \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}}-abstractions, e.g.\ \isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x\ y{\isaliteral{2E}{\isachardot}}\ t{\isaliteral{22}{\isachardoublequote}}} may be
wenzelm@40685:   written more conveniently as \isa{{\isaliteral{22}{\isachardoublequote}}c\ x\ y\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t{\isaliteral{22}{\isachardoublequote}}}.  Moreover,
wenzelm@27042:   definitions may be weakened by adding arbitrary pre-conditions:
wenzelm@40685:   \isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ c\ x\ y\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t{\isaliteral{22}{\isachardoublequote}}}.
wenzelm@27042: 
wenzelm@27042:   \medskip The built-in well-formedness conditions for definitional
wenzelm@27042:   specifications are:
wenzelm@27042: 
wenzelm@27042:   \begin{itemize}
wenzelm@27042: 
wenzelm@27042:   \item Arguments (on the left-hand side) must be distinct variables.
wenzelm@27042: 
wenzelm@27042:   \item All variables on the right-hand side must also appear on the
wenzelm@27042:   left-hand side.
wenzelm@27042: 
wenzelm@27042:   \item All type variables on the right-hand side must also appear on
wenzelm@40685:   the left-hand side; this prohibits \isa{{\isaliteral{22}{\isachardoublequote}}{\isadigit{0}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ length\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ list{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} for example.
wenzelm@27042: 
wenzelm@27042:   \item The definition must not be recursive.  Most object-logics
wenzelm@27042:   provide definitional principles that can be used to express
wenzelm@27042:   recursion safely.
wenzelm@27042: 
wenzelm@27042:   \end{itemize}
wenzelm@27042: 
haftmann@31047:   The right-hand side of overloaded definitions may mention overloaded constants
wenzelm@27042:   recursively at type instances corresponding to the immediate
wenzelm@40685:   argument types \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}.  Incomplete
wenzelm@27042:   specification patterns impose global constraints on all occurrences,
wenzelm@40685:   e.g.\ \isa{{\isaliteral{22}{\isachardoublequote}}d\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{22}{\isachardoublequote}}} on the left-hand side means that all
wenzelm@27042:   corresponding occurrences on some right-hand side need to be an
wenzelm@40685:   instance of this, general \isa{{\isaliteral{22}{\isachardoublequote}}d\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}{\isaliteral{22}{\isachardoublequote}}} will be disallowed.
wenzelm@27042: 
wenzelm@27042:   \begin{matharray}{rcl}
wenzelm@40685:     \indexdef{}{command}{consts}\hypertarget{command.consts}{\hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@40685:     \indexdef{}{command}{defs}\hypertarget{command.defs}{\hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@27042:   \end{matharray}
wenzelm@27042: 
wenzelm@43467:   \begin{railoutput}
wenzelm@43535: \rail@begin{3}{}
wenzelm@43467: \rail@term{\hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}}[]
wenzelm@43467: \rail@plus
wenzelm@43467: \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
wenzelm@43467: \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}}}[]
wenzelm@43467: \rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
wenzelm@43467: \rail@bar
wenzelm@43467: \rail@nextbar{1}
wenzelm@43467: \rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@nextplus{2}
wenzelm@43467: \rail@endplus
wenzelm@43467: \rail@end
wenzelm@43575: \rail@begin{2}{}
wenzelm@43467: \rail@term{\hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}}}[]
wenzelm@43467: \rail@bar
wenzelm@43467: \rail@nextbar{1}
wenzelm@43575: \rail@nont{\isa{opt}}[]
wenzelm@43575: \rail@endbar
wenzelm@43575: \rail@plus
wenzelm@43575: \rail@nont{\hyperlink{syntax.axmdecl}{\mbox{\isa{axmdecl}}}}[]
wenzelm@43575: \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
wenzelm@43575: \rail@nextplus{1}
wenzelm@43575: \rail@endplus
wenzelm@43575: \rail@end
wenzelm@43575: \rail@begin{2}{\isa{opt}}
wenzelm@43467: \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
wenzelm@43467: \rail@bar
wenzelm@43575: \rail@nextbar{1}
wenzelm@43467: \rail@term{\isa{\isakeyword{unchecked}}}[]
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@bar
wenzelm@43575: \rail@nextbar{1}
wenzelm@43467: \rail@term{\isa{\isakeyword{overloaded}}}[]
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
wenzelm@43467: \rail@end
wenzelm@43467: \end{railoutput}
wenzelm@43467: 
wenzelm@27042: 
wenzelm@28788:   \begin{description}
wenzelm@27042: 
wenzelm@40685:   \item \hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{22}{\isachardoublequote}}} declares constant \isa{c} to have any instance of type scheme \isa{{\isaliteral{5C3C7369676D613E}{\isasymsigma}}}.  The optional
wenzelm@28788:   mixfix annotations may attach concrete syntax to the constants
wenzelm@28788:   declared.
wenzelm@27042:   
wenzelm@40685:   \item \hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}name{\isaliteral{3A}{\isacharcolon}}\ eqn{\isaliteral{22}{\isachardoublequote}}} introduces \isa{eqn}
wenzelm@27042:   as a definitional axiom for some existing constant.
wenzelm@27042:   
wenzelm@40685:   The \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}unchecked{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} option disables global dependency checks
wenzelm@27042:   for this definition, which is occasionally useful for exotic
wenzelm@27042:   overloading.  It is at the discretion of the user to avoid malformed
wenzelm@27042:   theory specifications!
wenzelm@27042:   
wenzelm@40685:   The \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}overloaded{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} option declares definitions to be
wenzelm@27042:   potentially overloaded.  Unless this option is given, a warning
wenzelm@27042:   message would be issued for any definitional equation with a more
wenzelm@27042:   special type than that of the corresponding constant declaration.
wenzelm@27042:   
wenzelm@28788:   \end{description}%
wenzelm@27042: \end{isamarkuptext}%
wenzelm@27042: \isamarkuptrue%
wenzelm@27042: %
wenzelm@27042: \isamarkupsection{Axioms and theorems \label{sec:axms-thms}%
wenzelm@27042: }
wenzelm@27042: \isamarkuptrue%
wenzelm@27042: %
wenzelm@27042: \begin{isamarkuptext}%
wenzelm@27042: \begin{matharray}{rcll}
wenzelm@40685:     \indexdef{}{command}{axioms}\hypertarget{command.axioms}{\hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} & (axiomatic!) \\
wenzelm@40685:     \indexdef{}{command}{lemmas}\hypertarget{command.lemmas}{\hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@40685:     \indexdef{}{command}{theorems}\hypertarget{command.theorems}{\hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@27042:   \end{matharray}
wenzelm@27042: 
wenzelm@43467:   \begin{railoutput}
wenzelm@43535: \rail@begin{2}{}
wenzelm@43467: \rail@term{\hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}}}[]
wenzelm@43467: \rail@plus
wenzelm@43467: \rail@nont{\hyperlink{syntax.axmdecl}{\mbox{\isa{axmdecl}}}}[]
wenzelm@43467: \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
wenzelm@43467: \rail@nextplus{1}
wenzelm@43467: \rail@endplus
wenzelm@43467: \rail@end
wenzelm@46471: \rail@begin{6}{}
wenzelm@43467: \rail@bar
wenzelm@43467: \rail@term{\hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}}[]
wenzelm@43467: \rail@nextbar{1}
wenzelm@43467: \rail@term{\hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}}}[]
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@bar
wenzelm@43467: \rail@nextbar{1}
wenzelm@43467: \rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
wenzelm@43467: \rail@endbar
wenzelm@46471: \rail@cr{3}
wenzelm@43467: \rail@plus
wenzelm@43467: \rail@bar
wenzelm@46471: \rail@nextbar{4}
wenzelm@43467: \rail@nont{\hyperlink{syntax.thmdef}{\mbox{\isa{thmdef}}}}[]
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
wenzelm@46471: \rail@nextplus{5}
wenzelm@43467: \rail@cterm{\isa{\isakeyword{and}}}[]
wenzelm@43467: \rail@endplus
wenzelm@46471: \rail@bar
wenzelm@46471: \rail@nextbar{4}
wenzelm@46471: \rail@term{\isa{\isakeyword{for}}}[]
wenzelm@46471: \rail@plus
wenzelm@46471: \rail@nont{\hyperlink{syntax.vars}{\mbox{\isa{vars}}}}[]
wenzelm@46471: \rail@nextplus{5}
wenzelm@46471: \rail@cterm{\isa{\isakeyword{and}}}[]
wenzelm@46471: \rail@endplus
wenzelm@46471: \rail@endbar
wenzelm@43467: \rail@end
wenzelm@43467: \end{railoutput}
wenzelm@43467: 
wenzelm@27042: 
wenzelm@28788:   \begin{description}
wenzelm@27042:   
wenzelm@40685:   \item \hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} introduces arbitrary
wenzelm@27042:   statements as axioms of the meta-logic.  In fact, axioms are
wenzelm@27042:   ``axiomatic theorems'', and may be referred later just as any other
wenzelm@27042:   theorem.
wenzelm@27042:   
wenzelm@27042:   Axioms are usually only introduced when declaring new logical
wenzelm@27042:   systems.  Everyday work is typically done the hard way, with proper
wenzelm@27042:   definitions and proven theorems.
wenzelm@27042:   
wenzelm@46471:   \item \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\ {\isaliteral{3D}{\isacharequal}}\ b\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ b\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}~\indexdef{}{keyword}{for}\hypertarget{keyword.for}{\hyperlink{keyword.for}{\mbox{\isa{\isakeyword{for}}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{22}{\isachardoublequote}}} evaluates given facts (with attributes) in
wenzelm@46471:   the current context, which may be augmented by local variables.
wenzelm@46471:   Results are standardized before being stored, i.e.\ schematic
wenzelm@46471:   variables are renamed to enforce index \isa{{\isaliteral{22}{\isachardoublequote}}{\isadigit{0}}{\isaliteral{22}{\isachardoublequote}}} uniformly.
wenzelm@46471: 
wenzelm@46471:   \item \hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}} is the same as \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}, but
wenzelm@46471:   marks the result as a different kind of facts.
wenzelm@27042: 
wenzelm@28788:   \end{description}%
wenzelm@27042: \end{isamarkuptext}%
wenzelm@27042: \isamarkuptrue%
wenzelm@27042: %
wenzelm@27042: \isamarkupsection{Oracles%
wenzelm@27042: }
wenzelm@27042: \isamarkuptrue%
wenzelm@27042: %
wenzelm@27042: \begin{isamarkuptext}%
wenzelm@28788: Oracles allow Isabelle to take advantage of external reasoners
wenzelm@28788:   such as arithmetic decision procedures, model checkers, fast
wenzelm@28788:   tautology checkers or computer algebra systems.  Invoked as an
wenzelm@28788:   oracle, an external reasoner can create arbitrary Isabelle theorems.
wenzelm@28788: 
wenzelm@28788:   It is the responsibility of the user to ensure that the external
wenzelm@28788:   reasoner is as trustworthy as the application requires.  Another
wenzelm@28788:   typical source of errors is the linkup between Isabelle and the
wenzelm@28788:   external tool, not just its concrete implementation, but also the
wenzelm@28788:   required translation between two different logical environments.
wenzelm@28788: 
wenzelm@28788:   Isabelle merely guarantees well-formedness of the propositions being
wenzelm@28788:   asserted, and records within the internal derivation object how
wenzelm@28788:   presumed theorems depend on unproven suppositions.
wenzelm@28788: 
wenzelm@40496:   \begin{matharray}{rcll}
wenzelm@40685:     \indexdef{}{command}{oracle}\hypertarget{command.oracle}{\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} & (axiomatic!) \\
wenzelm@27042:   \end{matharray}
wenzelm@27042: 
wenzelm@43467:   \begin{railoutput}
wenzelm@43535: \rail@begin{1}{}
wenzelm@43467: \rail@term{\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}}[]
wenzelm@43467: \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
wenzelm@43467: \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
wenzelm@43467: \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
wenzelm@43467: \rail@end
wenzelm@43467: \end{railoutput}
wenzelm@43467: 
wenzelm@27042: 
wenzelm@28788:   \begin{description}
wenzelm@27042: 
wenzelm@40685:   \item \hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}name\ {\isaliteral{3D}{\isacharequal}}\ text{\isaliteral{22}{\isachardoublequote}}} turns the given ML
wenzelm@40685:   expression \isa{{\isaliteral{22}{\isachardoublequote}}text{\isaliteral{22}{\isachardoublequote}}} of type \verb|'a -> cterm| into an
wenzelm@28291:   ML function of type \verb|'a -> thm|, which is bound to the
wenzelm@28788:   global identifier \verb|name|.  This acts like an infinitary
wenzelm@28788:   specification of axioms!  Invoking the oracle only works within the
wenzelm@28788:   scope of the resulting theory.
wenzelm@27042: 
wenzelm@28788:   \end{description}
wenzelm@28788: 
wenzelm@41052:   See \verb|~~/src/HOL/ex/Iff_Oracle.thy| for a worked example of
wenzelm@28788:   defining a new primitive rule as oracle, and turning it into a proof
wenzelm@28788:   method.%
wenzelm@27042: \end{isamarkuptext}%
wenzelm@27042: \isamarkuptrue%
wenzelm@27042: %
wenzelm@27042: \isamarkupsection{Name spaces%
wenzelm@27042: }
wenzelm@27042: \isamarkuptrue%
wenzelm@27042: %
wenzelm@27042: \begin{isamarkuptext}%
wenzelm@27042: \begin{matharray}{rcl}
wenzelm@40685:     \indexdef{}{command}{hide\_class}\hypertarget{command.hide-class}{\hyperlink{command.hide-class}{\mbox{\isa{\isacommand{hide{\isaliteral{5F}{\isacharunderscore}}class}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@40685:     \indexdef{}{command}{hide\_type}\hypertarget{command.hide-type}{\hyperlink{command.hide-type}{\mbox{\isa{\isacommand{hide{\isaliteral{5F}{\isacharunderscore}}type}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@40685:     \indexdef{}{command}{hide\_const}\hypertarget{command.hide-const}{\hyperlink{command.hide-const}{\mbox{\isa{\isacommand{hide{\isaliteral{5F}{\isacharunderscore}}const}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@40685:     \indexdef{}{command}{hide\_fact}\hypertarget{command.hide-fact}{\hyperlink{command.hide-fact}{\mbox{\isa{\isacommand{hide{\isaliteral{5F}{\isacharunderscore}}fact}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
wenzelm@27042:   \end{matharray}
wenzelm@27042: 
wenzelm@43467:   \begin{railoutput}
wenzelm@43535: \rail@begin{4}{}
wenzelm@43467: \rail@bar
wenzelm@43467: \rail@nont{\hyperlink{command.hide-class}{\mbox{\isa{\isacommand{hide{\isaliteral{5F}{\isacharunderscore}}class}}}}}[]
wenzelm@43467: \rail@nextbar{1}
wenzelm@43467: \rail@nont{\hyperlink{command.hide-type}{\mbox{\isa{\isacommand{hide{\isaliteral{5F}{\isacharunderscore}}type}}}}}[]
wenzelm@43467: \rail@nextbar{2}
wenzelm@43467: \rail@nont{\hyperlink{command.hide-const}{\mbox{\isa{\isacommand{hide{\isaliteral{5F}{\isacharunderscore}}const}}}}}[]
wenzelm@43467: \rail@nextbar{3}
wenzelm@43467: \rail@nont{\hyperlink{command.hide-fact}{\mbox{\isa{\isacommand{hide{\isaliteral{5F}{\isacharunderscore}}fact}}}}}[]
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@bar
wenzelm@43467: \rail@nextbar{1}
wenzelm@43467: \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
wenzelm@43467: \rail@term{\isa{\isakeyword{open}}}[]
wenzelm@43467: \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
wenzelm@43467: \rail@endbar
wenzelm@43467: \rail@plus
wenzelm@43467: \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
wenzelm@43467: \rail@nextplus{1}
wenzelm@43467: \rail@endplus
wenzelm@43467: \rail@end
wenzelm@43467: \end{railoutput}
wenzelm@43467: 
wenzelm@27042: 
wenzelm@27042:   Isabelle organizes any kind of name declarations (of types,
wenzelm@27042:   constants, theorems etc.) by separate hierarchically structured name
wenzelm@27042:   spaces.  Normally the user does not have to control the behavior of
wenzelm@27042:   name spaces by hand, yet the following commands provide some way to
wenzelm@27042:   do so.
wenzelm@27042: 
wenzelm@28788:   \begin{description}
wenzelm@27042: 
wenzelm@40685:   \item \hyperlink{command.hide-class}{\mbox{\isa{\isacommand{hide{\isaliteral{5F}{\isacharunderscore}}class}}}}~\isa{names} fully removes class
wenzelm@40685:   declarations from a given name space; with the \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}open{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}
krauss@40158:   option, only the base name is hidden.
wenzelm@36177: 
wenzelm@27042:   Note that hiding name space accesses has no impact on logical
wenzelm@28788:   declarations --- they remain valid internally.  Entities that are no
wenzelm@27042:   longer accessible to the user are printed with the special qualifier
wenzelm@40685:   ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}}'' prefixed to the full internal name.
wenzelm@27042: 
wenzelm@40685:   \item \hyperlink{command.hide-type}{\mbox{\isa{\isacommand{hide{\isaliteral{5F}{\isacharunderscore}}type}}}}, \hyperlink{command.hide-const}{\mbox{\isa{\isacommand{hide{\isaliteral{5F}{\isacharunderscore}}const}}}}, and \hyperlink{command.hide-fact}{\mbox{\isa{\isacommand{hide{\isaliteral{5F}{\isacharunderscore}}fact}}}} are similar to \hyperlink{command.hide-class}{\mbox{\isa{\isacommand{hide{\isaliteral{5F}{\isacharunderscore}}class}}}}, but hide types,
wenzelm@36177:   constants, and facts, respectively.
wenzelm@36177:   
wenzelm@28788:   \end{description}%
wenzelm@27042: \end{isamarkuptext}%
wenzelm@27042: \isamarkuptrue%
wenzelm@27042: %
wenzelm@26869: \isadelimtheory
wenzelm@26869: %
wenzelm@26869: \endisadelimtheory
wenzelm@26869: %
wenzelm@26869: \isatagtheory
wenzelm@26869: \isacommand{end}\isamarkupfalse%
wenzelm@26869: %
wenzelm@26869: \endisatagtheory
wenzelm@26869: {\isafoldtheory}%
wenzelm@26869: %
wenzelm@26869: \isadelimtheory
wenzelm@26869: %
wenzelm@26869: \endisadelimtheory
wenzelm@26869: \isanewline
wenzelm@26869: \end{isabellebody}%
wenzelm@26869: %%% Local Variables:
wenzelm@26869: %%% mode: latex
wenzelm@26869: %%% TeX-master: "root"
wenzelm@26869: %%% End: