wenzelm@26869: % wenzelm@26869: \begin{isabellebody}% wenzelm@26869: \def\isabellecontext{Spec}% wenzelm@26869: % wenzelm@26869: \isadelimtheory wenzelm@26869: \isanewline wenzelm@26869: \isanewline wenzelm@26869: % wenzelm@26869: \endisadelimtheory wenzelm@26869: % wenzelm@26869: \isatagtheory wenzelm@26869: \isacommand{theory}\isamarkupfalse% wenzelm@26869: \ Spec\isanewline wenzelm@26869: \isakeyword{imports}\ 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@27047: \isamarkupchapter{Theory specifications% wenzelm@26869: } wenzelm@26869: \isamarkuptrue% wenzelm@26869: % 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@26902: \indexdef{}{command}{theory}\hypertarget{command.theory}{\hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}}} & : & \isartrans{toplevel}{theory} \\ wenzelm@27042: \indexdef{global}{command}{end}\hypertarget{command.global.end}{\hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}}} & : & \isartrans{theory}{toplevel} \\ wenzelm@26870: \end{matharray} wenzelm@26870: wenzelm@27042: Isabelle/Isar theories are defined via theory file, which contain wenzelm@27042: both specifications and proofs; occasionally definitional mechanisms wenzelm@27042: also require some explicit proof. The theory body may be wenzelm@27042: sub-structered by means of \emph{local theory} target mechanisms, wenzelm@27042: notably \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}} and \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}. wenzelm@26870: wenzelm@26902: The first ``real'' command of any theory has to be \hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}}, which starts a new theory based on the merge of existing wenzelm@26902: ones. Just preceding the \hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}} keyword, there may be wenzelm@26902: an optional \hyperlink{command.header}{\mbox{\isa{\isacommand{header}}}} declaration, which is relevant to wenzelm@26870: document preparation only; it acts very much like a special wenzelm@27052: pre-theory markup command (cf.\ \secref{sec:markup}). The \hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}} command concludes a theory development; it has to be wenzelm@27052: the very last command of any theory file loaded in batch-mode. wenzelm@26870: wenzelm@26870: \begin{rail} wenzelm@26870: 'theory' name 'imports' (name +) uses? 'begin' wenzelm@26870: ; wenzelm@26870: wenzelm@26870: uses: 'uses' ((name | parname) +); wenzelm@26870: \end{rail} wenzelm@26870: wenzelm@26870: \begin{descr} wenzelm@26870: wenzelm@26902: \item [\hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}}~\isa{{\isachardoublequote}A\ {\isasymIMPORTS}\ B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n\ {\isasymBEGIN}{\isachardoublequote}}] starts a new theory \isa{A} based on the wenzelm@26870: merge of existing theories \isa{{\isachardoublequote}B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n{\isachardoublequote}}. wenzelm@26870: wenzelm@26870: Due to inclusion of several ancestors, the overall theory structure wenzelm@26870: emerging in an Isabelle session forms a directed acyclic graph wenzelm@26870: (DAG). Isabelle's theory loader ensures that the sources wenzelm@26870: contributing to the development graph are always up-to-date. wenzelm@26870: Changed files are automatically reloaded when processing theory wenzelm@26870: headers. 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@26870: loaded immediately (as ML), unless the name is put in parentheses, wenzelm@26870: which merely documents the dependency to be resolved later in the wenzelm@26902: text (typically via explicit \indexref{}{command}{use}\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}} in the body text, wenzelm@26870: see \secref{sec:ML}). wenzelm@26870: wenzelm@27042: \item [\hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}}] concludes the current theory wenzelm@27042: definition. wenzelm@27042: wenzelm@27042: \end{descr}% wenzelm@27042: \end{isamarkuptext}% wenzelm@27042: \isamarkuptrue% wenzelm@27042: % 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@27042: (cf.\ \secref{sec:class}); the name ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' signifies the wenzelm@27042: global theory context. wenzelm@27042: wenzelm@27042: \begin{matharray}{rcll} wenzelm@27042: \indexdef{}{command}{context}\hypertarget{command.context}{\hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}} & : & \isartrans{theory}{local{\dsh}theory} \\ wenzelm@27042: \indexdef{local}{command}{end}\hypertarget{command.local.end}{\hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}}} & : & \isartrans{local{\dsh}theory}{theory} \\ wenzelm@27042: \end{matharray} wenzelm@27042: wenzelm@27042: \indexouternonterm{target} wenzelm@27042: \begin{rail} wenzelm@27042: 'context' name 'begin' wenzelm@27042: ; wenzelm@27042: wenzelm@27042: target: '(' 'in' name ')' wenzelm@27042: ; wenzelm@27042: \end{rail} wenzelm@27042: wenzelm@27042: \begin{descr} wenzelm@27042: wenzelm@27042: \item [\hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}~\isa{{\isachardoublequote}c\ {\isasymBEGIN}{\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@27042: \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@27042: \item [\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}{\isachardoublequote}}] given after any local theory command wenzelm@27042: specifies an immediate target, e.g.\ ``\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}\ {\isasymdots}{\isachardoublequote}}'' or ``\hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}\ {\isasymdots}{\isachardoublequote}}''. This works both in a local or wenzelm@27042: global theory context; the current target context will be suspended wenzelm@27042: for this command only. Note that ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ {\isacharminus}{\isacharparenright}{\isachardoublequote}}'' will wenzelm@27042: always produce a global result independently of the current target wenzelm@27042: context. wenzelm@27042: wenzelm@27042: \end{descr} 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@27042: \isa{c} with parameter \isa{x} and assumption \isa{{\isachardoublequote}A{\isacharbrackleft}x{\isacharbrackright}{\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@27042: \isa{{\isachardoublequote}a\ {\isasymequiv}\ t{\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}} becomes \isa{{\isachardoublequote}c{\isachardot}a\ {\isacharquery}x\ {\isasymequiv}\ t{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}{\isachardoublequote}} at the theory wenzelm@27042: level (for arbitrary \isa{{\isachardoublequote}{\isacharquery}x{\isachardoublequote}}), together with a local wenzelm@27042: abbreviation \isa{{\isachardoublequote}c\ {\isasymequiv}\ c{\isachardot}a\ x{\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@27042: generalizing the parameters of the context. For example, \isa{{\isachardoublequote}a{\isacharcolon}\ B{\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}} becomes \isa{{\isachardoublequote}c{\isachardot}a{\isacharcolon}\ A{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}\ {\isasymLongrightarrow}\ B{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}{\isachardoublequote}}, again for arbitrary wenzelm@27042: \isa{{\isachardoublequote}{\isacharquery}x{\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@27042: \indexdef{}{command}{axiomatization}\hypertarget{command.axiomatization}{\hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{axiomatization}}}}} & : & \isarkeep{local{\dsh}theory} & (axiomatic!)\\ wenzelm@27042: \indexdef{}{command}{definition}\hypertarget{command.definition}{\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}} & : & \isarkeep{local{\dsh}theory} \\ wenzelm@27042: \indexdef{}{attribute}{defn}\hypertarget{attribute.defn}{\hyperlink{attribute.defn}{\mbox{\isa{defn}}}} & : & \isaratt \\ wenzelm@27042: \indexdef{}{command}{abbreviation}\hypertarget{command.abbreviation}{\hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}} & : & \isarkeep{local{\dsh}theory} \\ wenzelm@27042: \indexdef{}{command}{print\_abbrevs}\hypertarget{command.print-abbrevs}{\hyperlink{command.print-abbrevs}{\mbox{\isa{\isacommand{print{\isacharunderscore}abbrevs}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ wenzelm@27042: \indexdef{}{command}{notation}\hypertarget{command.notation}{\hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}} & : & \isarkeep{local{\dsh}theory} \\ wenzelm@27042: \indexdef{}{command}{no\_notation}\hypertarget{command.no-notation}{\hyperlink{command.no-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}}}} & : & \isarkeep{local{\dsh}theory} \\ 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@27042: \begin{rail} wenzelm@27042: 'axiomatization' target? fixes? ('where' specs)? wenzelm@27042: ; wenzelm@27042: 'definition' target? (decl 'where')? thmdecl? prop wenzelm@27042: ; wenzelm@27042: 'abbreviation' target? mode? (decl 'where')? prop wenzelm@27042: ; wenzelm@27042: ('notation' | 'no\_notation') target? mode? (nameref structmixfix + 'and') wenzelm@27042: ; wenzelm@27042: wenzelm@27042: fixes: ((name ('::' type)? mixfix? | vars) + 'and') wenzelm@27042: ; wenzelm@27042: specs: (thmdecl? props + 'and') wenzelm@27042: ; wenzelm@27042: decl: name ('::' type)? mixfix? wenzelm@27042: ; wenzelm@27042: \end{rail} wenzelm@27042: wenzelm@27042: \begin{descr} wenzelm@27042: wenzelm@27042: \item [\hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{axiomatization}}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymdots}\ c\isactrlsub m\ {\isasymWHERE}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}] introduces several constants wenzelm@27042: simultaneously and states axiomatic properties for these. The wenzelm@27042: constants are marked as being specified once and for all, which wenzelm@27042: prevents additional specifications being issued later on. wenzelm@27042: wenzelm@27042: Note that axiomatic specifications are only appropriate when wenzelm@27042: declaring a new logical system. Normal applications should only use wenzelm@27042: definitional mechanisms! wenzelm@27042: wenzelm@27042: \item [\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}~\isa{{\isachardoublequote}c\ {\isasymWHERE}\ eq{\isachardoublequote}}] produces an wenzelm@27042: internal definition \isa{{\isachardoublequote}c\ {\isasymequiv}\ t{\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@27042: object-logic. This usually covers object-level equality \isa{{\isachardoublequote}x\ {\isacharequal}\ y{\isachardoublequote}} and equivalence \isa{{\isachardoublequote}A\ {\isasymleftrightarrow}\ B{\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@27042: well as additional conditions, e.g.\ \isa{{\isachardoublequote}f\ x\ y\ {\isacharequal}\ t{\isachardoublequote}} instead of wenzelm@27042: \isa{{\isachardoublequote}f\ {\isasymequiv}\ {\isasymlambda}x\ y{\isachardot}\ t{\isachardoublequote}} and \isa{{\isachardoublequote}y\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ g\ x\ y\ {\isacharequal}\ u{\isachardoublequote}} instead of an wenzelm@27042: unrestricted \isa{{\isachardoublequote}g\ {\isasymequiv}\ {\isasymlambda}x\ y{\isachardot}\ u{\isachardoublequote}}. wenzelm@27042: wenzelm@27042: \item [\hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}~\isa{{\isachardoublequote}c\ {\isasymWHERE}\ eq{\isachardoublequote}}] introduces wenzelm@27042: a syntactic constant which is associated with a certain term wenzelm@27042: according 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@27042: \item [\hyperlink{command.print-abbrevs}{\mbox{\isa{\isacommand{print{\isacharunderscore}abbrevs}}}}] prints all constant abbreviations wenzelm@27042: of the current context. wenzelm@27042: wenzelm@27042: \item [\hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}}] associates mixfix wenzelm@27042: syntax with an existing constant or fixed variable. This is a wenzelm@27042: robust interface to the underlying \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} primitive wenzelm@27042: (\secref{sec:syn-trans}). Type declaration and internal syntactic wenzelm@27042: representation of the given entity is retrieved from the context. wenzelm@27042: wenzelm@27042: \item [\hyperlink{command.no-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}}}] is similar to \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}, but removes the specified syntax annotation from the wenzelm@27042: present context. wenzelm@27042: wenzelm@27042: \end{descr} wenzelm@27042: wenzelm@27042: All of these specifications support local theory targets (cf.\ wenzelm@27042: \secref{sec:target}).% 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@27042: \indexdef{}{command}{declaration}\hypertarget{command.declaration}{\hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}} & : & \isarkeep{local{\dsh}theory} \\ wenzelm@27042: \indexdef{}{command}{declare}\hypertarget{command.declare}{\hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}}} & : & \isarkeep{local{\dsh}theory} \\ wenzelm@27042: \end{matharray} wenzelm@27042: wenzelm@27042: \begin{rail} wenzelm@27042: 'declaration' target? text wenzelm@27042: ; wenzelm@27042: 'declare' target? (thmrefs + 'and') wenzelm@27042: ; wenzelm@27042: \end{rail} wenzelm@27042: wenzelm@27042: \begin{descr} wenzelm@27042: wenzelm@27042: \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@27042: \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@27042: \end{descr}% 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}% wenzelm@27042: Locales are 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: % wenzelm@27042: \isamarkupsubsection{Locale specifications% wenzelm@27042: } wenzelm@27042: \isamarkuptrue% wenzelm@27042: % wenzelm@27042: \begin{isamarkuptext}% wenzelm@27042: \begin{matharray}{rcl} wenzelm@27042: \indexdef{}{command}{locale}\hypertarget{command.locale}{\hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}} & : & \isartrans{theory}{local{\dsh}theory} \\ wenzelm@27042: \indexdef{}{command}{print\_locale}\hypertarget{command.print-locale}{\hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ wenzelm@27042: \indexdef{}{command}{print\_locales}\hypertarget{command.print-locales}{\hyperlink{command.print-locales}{\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ wenzelm@27042: \indexdef{}{method}{intro\_locales}\hypertarget{method.intro-locales}{\hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}}} & : & \isarmeth \\ wenzelm@27042: \indexdef{}{method}{unfold\_locales}\hypertarget{method.unfold-locales}{\hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}}} & : & \isarmeth \\ wenzelm@27042: \end{matharray} wenzelm@27042: wenzelm@27042: \indexouternonterm{contextexpr}\indexouternonterm{contextelem} wenzelm@27042: \indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes} wenzelm@27042: \indexisarelem{defines}\indexisarelem{notes}\indexisarelem{includes} wenzelm@27042: \begin{rail} wenzelm@27042: 'locale' ('(open)')? name ('=' localeexpr)? 'begin'? wenzelm@27042: ; wenzelm@27042: 'print\_locale' '!'? localeexpr wenzelm@27042: ; wenzelm@27042: localeexpr: ((contextexpr '+' (contextelem+)) | contextexpr | (contextelem+)) wenzelm@27042: ; wenzelm@27042: wenzelm@27042: contextexpr: nameref | '(' contextexpr ')' | wenzelm@27042: (contextexpr (name mixfix? +)) | (contextexpr + '+') wenzelm@27042: ; wenzelm@27042: contextelem: fixes | constrains | assumes | defines | notes wenzelm@27042: ; wenzelm@27042: fixes: 'fixes' ((name ('::' type)? structmixfix? | vars) + 'and') wenzelm@27042: ; wenzelm@27042: constrains: 'constrains' (name '::' type + 'and') wenzelm@27042: ; wenzelm@27042: assumes: 'assumes' (thmdecl? props + 'and') wenzelm@27042: ; wenzelm@27042: defines: 'defines' (thmdecl? prop proppat? + 'and') wenzelm@27042: ; wenzelm@27042: notes: 'notes' (thmdef? thmrefs + 'and') wenzelm@27042: ; wenzelm@27042: includes: 'includes' contextexpr wenzelm@27042: ; wenzelm@27042: \end{rail} wenzelm@27042: wenzelm@27042: \begin{descr} wenzelm@27042: wenzelm@27042: \item [\hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}~\isa{{\isachardoublequote}loc\ {\isacharequal}\ import\ {\isacharplus}\ body{\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: wenzelm@27042: The \isa{import} consists of a structured context expression, wenzelm@27042: consisting of references to existing locales, renamed contexts, or wenzelm@27042: merged contexts. Renaming uses positional notation: \isa{{\isachardoublequote}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n{\isachardoublequote}} means that (a prefix of) the fixed wenzelm@27042: parameters of context \isa{c} are named \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub n{\isachardoublequote}}; a ``\isa{{\isacharunderscore}}'' (underscore) means to skip that wenzelm@27042: position. Renaming by default deletes concrete syntax, but new wenzelm@27042: syntax may by specified with a mixfix annotation. An exeption of wenzelm@27042: this rule is the special syntax declared with ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymSTRUCTURE}{\isacharparenright}{\isachardoublequote}}'' (see below), which is neither deleted nor can it wenzelm@27042: be changed. Merging proceeds from left-to-right, suppressing any wenzelm@27042: duplicates stemming from different paths through the import wenzelm@27042: hierarchy. wenzelm@27042: wenzelm@27042: The \isa{body} consists of basic context elements, further context wenzelm@27042: expressions may be included as well. wenzelm@27042: wenzelm@27042: \begin{descr} wenzelm@27042: wenzelm@27042: \item [\hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}}~\isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}}] declares a local wenzelm@27042: parameter of type \isa{{\isasymtau}} and mixfix annotation \isa{mx} (both wenzelm@27042: are optional). The special syntax declaration ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymSTRUCTURE}{\isacharparenright}{\isachardoublequote}}'' means that \isa{x} may be referenced wenzelm@27042: implicitly in this context. wenzelm@27042: wenzelm@27042: \item [\hyperlink{element.constrains}{\mbox{\isa{\isakeyword{constrains}}}}~\isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isachardoublequote}}] introduces a type wenzelm@27042: constraint \isa{{\isasymtau}} on the local parameter \isa{x}. wenzelm@27042: wenzelm@27042: \item [\hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\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@27042: \item [\hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ x\ {\isasymequiv}\ t{\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@27042: ``\hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}}~\isa{{\isachardoublequote}f\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n\ {\isasymequiv}\ t{\isachardoublequote}}''. wenzelm@27042: wenzelm@27042: \item [\hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}}~\isa{{\isachardoublequote}a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\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@27042: \item [\hyperlink{element.includes}{\mbox{\isa{\isakeyword{includes}}}}~\isa{c}] copies the specified context wenzelm@27042: in a statically scoped manner. Only available in the long goal wenzelm@27042: format of \secref{sec:goals}. wenzelm@27042: wenzelm@27042: In contrast, the initial \isa{import} specification of a locale wenzelm@27042: expression maintains a dynamic relation to the locales being wenzelm@27042: referenced (benefiting from any later fact declarations in the wenzelm@27042: obvious manner). wenzelm@27042: wenzelm@27042: \end{descr} wenzelm@27042: wenzelm@27042: Note that ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIS}\ p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub n{\isacharparenright}{\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: wenzelm@27042: \medskip By default, locale specifications are ``closed up'' by wenzelm@27042: turning the given text into a predicate definition \isa{loc{\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@27042: object-logic setup (e.g.\ replacing \isa{{\isasymAnd}} by \isa{{\isasymforall}}, and wenzelm@27042: \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}} by \isa{{\isachardoublequote}{\isasymlongrightarrow}{\isachardoublequote}} in HOL; see also wenzelm@27042: \secref{sec:object-logic}). Separate introduction rules \isa{loc{\isacharunderscore}axioms{\isachardot}intro} and \isa{loc{\isachardot}intro} are provided as well. wenzelm@27042: wenzelm@27042: The \isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}} option of a locale specification prevents both wenzelm@27042: the current \isa{loc{\isacharunderscore}axioms} and cumulative \isa{loc} predicate wenzelm@27042: constructions. Predicates are also omitted for empty specification wenzelm@27042: texts. wenzelm@27042: wenzelm@27042: \item [\hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{{\isachardoublequote}import\ {\isacharplus}\ body{\isachardoublequote}}] prints the wenzelm@27042: specified locale expression in a flattened form. The notable wenzelm@27042: special case \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{loc} just prints the wenzelm@27042: contents of the named locale, but keep in mind that type-inference wenzelm@27042: will normalize type variables according to the usual alphabetical wenzelm@27042: order. The command omits \hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}} elements by default. wenzelm@27042: Use \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}} to get them included. wenzelm@27042: wenzelm@27042: \item [\hyperlink{command.print-locales}{\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}}] prints the names of all locales wenzelm@27042: of the current theory. wenzelm@27042: wenzelm@27042: \item [\hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}} and \hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}}] wenzelm@27042: repeatedly expand all introduction rules of locale predicates of the wenzelm@27042: theory. While \hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}} only applies the \isa{loc{\isachardot}intro} introduction rules and therefore does not decend to wenzelm@27042: assumptions, \hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}} is more aggressive and applies wenzelm@27042: \isa{loc{\isacharunderscore}axioms{\isachardot}intro} as well. Both methods are aware of locale wenzelm@27042: specifications entailed by the context, both from target and wenzelm@27042: \hyperlink{element.includes}{\mbox{\isa{\isakeyword{includes}}}} statements, and from interpretations (see wenzelm@27042: below). New goals that are entailed by the current context are wenzelm@27042: discharged automatically. wenzelm@27042: wenzelm@27042: \end{descr}% wenzelm@27042: \end{isamarkuptext}% wenzelm@27042: \isamarkuptrue% wenzelm@27042: % wenzelm@27042: \isamarkupsubsection{Interpretation of locales% wenzelm@27042: } wenzelm@27042: \isamarkuptrue% wenzelm@27042: % wenzelm@27042: \begin{isamarkuptext}% wenzelm@27042: Locale expressions (more precisely, \emph{context expressions}) may wenzelm@27042: be instantiated, and the instantiated facts added to the current wenzelm@27042: context. This requires a proof of the instantiated specification wenzelm@27042: and is called \emph{locale interpretation}. Interpretation is wenzelm@27042: possible in theories and locales (command \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}) and also within a proof body (command \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}). wenzelm@27042: wenzelm@27042: \begin{matharray}{rcl} wenzelm@27042: \indexdef{}{command}{interpretation}\hypertarget{command.interpretation}{\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}} & : & \isartrans{theory}{proof(prove)} \\ wenzelm@27042: \indexdef{}{command}{interpret}\hypertarget{command.interpret}{\hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\ wenzelm@27042: \indexdef{}{command}{print\_interps}\hypertarget{command.print-interps}{\hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ wenzelm@27042: \end{matharray} wenzelm@27042: wenzelm@27042: \indexouternonterm{interp} wenzelm@27042: \begin{rail} wenzelm@27042: 'interpretation' (interp | name ('<' | subseteq) contextexpr) wenzelm@27042: ; wenzelm@27042: 'interpret' interp wenzelm@27042: ; wenzelm@27042: 'print\_interps' '!'? name wenzelm@27042: ; wenzelm@27042: instantiation: ('[' (inst+) ']')? wenzelm@27042: ; wenzelm@27042: interp: thmdecl? \\ (contextexpr instantiation | wenzelm@27042: name instantiation 'where' (thmdecl? prop + 'and')) wenzelm@27042: ; wenzelm@27042: \end{rail} wenzelm@27042: wenzelm@27042: \begin{descr} wenzelm@27042: wenzelm@27042: \item [\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isachardoublequote}expr\ insts\ {\isasymWHERE}\ eqns{\isachardoublequote}}] wenzelm@27042: wenzelm@27042: The first form of \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}} interprets \isa{expr} in the theory. The instantiation is given as a list of terms wenzelm@27042: \isa{insts} and is positional. All parameters must receive an wenzelm@27042: instantiation term --- with the exception of defined parameters. wenzelm@27042: These are, if omitted, derived from the defining equation and other wenzelm@27042: instantiations. Use ``\isa{{\isacharunderscore}}'' to omit an instantiation term. wenzelm@27042: wenzelm@27042: The command generates proof obligations for the instantiated wenzelm@27042: specifications (assumes and defines elements). Once these are wenzelm@27042: discharged by the user, instantiated facts are added to the theory wenzelm@27042: in a post-processing phase. wenzelm@27042: wenzelm@27042: Additional equations, which are unfolded in facts 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 wenzelm@27042: definition specification elements. The equations must be proved. wenzelm@27042: Note that if equations are present, the context expression is wenzelm@27042: restricted to a locale name. wenzelm@27042: wenzelm@27042: The command is aware of interpretations already active in the wenzelm@27042: theory. No proof obligations are generated for those, neither is wenzelm@27042: post-processing applied to their facts. This avoids duplication of wenzelm@27042: interpreted facts, in particular. Note that, in the case of a wenzelm@27042: locale with import, parts of the interpretation may already be wenzelm@27042: active. The command will only generate proof obligations and wenzelm@27042: process facts for new parts. wenzelm@27042: wenzelm@27042: The context expression may be preceded by a name and/or attributes. wenzelm@27042: These take effect in the post-processing of facts. The name is used wenzelm@27042: to prefix fact names, for example to avoid accidental hiding of wenzelm@27042: other facts. Attributes are applied after attributes of the wenzelm@27042: interpreted facts. wenzelm@27042: wenzelm@27042: Adding facts to locales has the effect of adding interpreted facts wenzelm@27042: to the theory for all active interpretations also. That is, wenzelm@27042: interpretations dynamically participate in any facts added to wenzelm@27042: locales. wenzelm@27042: wenzelm@27042: \item [\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isachardoublequote}name\ {\isasymsubseteq}\ expr{\isachardoublequote}}] wenzelm@27042: wenzelm@27042: This form of the command interprets \isa{expr} in the locale wenzelm@27042: \isa{name}. It requires a proof that the specification of \isa{name} implies the specification of \isa{expr}. As in the wenzelm@27042: localized version of the theorem command, the proof is in the wenzelm@27042: context of \isa{name}. After the proof obligation has been wenzelm@27042: dischared, the facts of \isa{expr} become part of locale \isa{name} as \emph{derived} context elements and are available when the wenzelm@27042: context \isa{name} is subsequently entered. Note that, like wenzelm@27042: import, this is dynamic: facts added to a locale part of \isa{expr} after interpretation become also available in \isa{name}. wenzelm@27042: Like facts of renamed context elements, facts obtained by wenzelm@27042: interpretation may be accessed by prefixing with the parameter wenzelm@27042: renaming (where the parameters are separated by ``\isa{{\isacharunderscore}}''). wenzelm@27042: wenzelm@27042: Unlike interpretation in theories, instantiation is confined to the wenzelm@27042: renaming of parameters, which may be specified as part of the wenzelm@27042: context expression \isa{expr}. Using defined parameters in \isa{name} one may achieve an effect similar to instantiation, though. wenzelm@27042: wenzelm@27042: Only specification fragments of \isa{expr} that are not already wenzelm@27042: part of \isa{name} (be it imported, derived or a derived fragment wenzelm@27042: of the import) are considered by interpretation. This enables wenzelm@27042: circular interpretations. wenzelm@27042: wenzelm@27042: If interpretations of \isa{name} exist in the current theory, the wenzelm@27042: command adds interpretations for \isa{expr} as well, with the same wenzelm@27042: prefix and attributes, although only for fragments of \isa{expr} wenzelm@27042: that are not interpreted in the theory already. wenzelm@27042: wenzelm@27042: \item [\hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}~\isa{{\isachardoublequote}expr\ insts\ {\isasymWHERE}\ eqns{\isachardoublequote}}] wenzelm@27042: interprets \isa{expr} in the proof context and is otherwise wenzelm@27042: similar to interpretation in theories. wenzelm@27042: wenzelm@27042: \item [\hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}}~\isa{loc}] prints the wenzelm@27042: interpretations of a particular locale \isa{loc} that are active wenzelm@27042: in the current context, either theory or proof context. The wenzelm@27042: exclamation point argument triggers printing of \emph{witness} wenzelm@27042: theorems justifying interpretations. These are normally omitted wenzelm@27042: from the output. wenzelm@27042: wenzelm@27042: \end{descr} 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.\ wenzelm@27042: the Simplifier or Classical Reasoner. Since the behavior of such wenzelm@27042: automated reasoning tools is \emph{not} stable under wenzelm@27042: interpretation morphisms, manual declarations might have to be wenzelm@27042: issued. wenzelm@27042: \end{warn} wenzelm@27042: wenzelm@27042: \begin{warn} wenzelm@27042: An interpretation in a theory 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 wenzelm@27042: first. A warning is issued, since it is likely that these could wenzelm@27042: have been generalized in the first place. The locale package does wenzelm@27042: not attempt to remove subsumed 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@27042: \isa{{\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@27042: \indexdef{}{command}{class}\hypertarget{command.class}{\hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}} & : & \isartrans{theory}{local{\dsh}theory} \\ wenzelm@27042: \indexdef{}{command}{instantiation}\hypertarget{command.instantiation}{\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}} & : & \isartrans{theory}{local{\dsh}theory} \\ wenzelm@27042: \indexdef{}{command}{instance}\hypertarget{command.instance}{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}} & : & \isartrans{local{\dsh}theory}{local{\dsh}theory} \\ wenzelm@27042: \indexdef{}{command}{subclass}\hypertarget{command.subclass}{\hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}} & : & \isartrans{local{\dsh}theory}{local{\dsh}theory} \\ wenzelm@27042: \indexdef{}{command}{print\_classes}\hypertarget{command.print-classes}{\hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ wenzelm@27042: \indexdef{}{method}{intro\_classes}\hypertarget{method.intro-classes}{\hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}} & : & \isarmeth \\ wenzelm@27042: \end{matharray} wenzelm@27042: wenzelm@27042: \begin{rail} wenzelm@27042: 'class' name '=' ((superclassexpr '+' (contextelem+)) | superclassexpr | (contextelem+)) \\ wenzelm@27042: 'begin'? wenzelm@27042: ; wenzelm@27042: 'instantiation' (nameref + 'and') '::' arity 'begin' wenzelm@27042: ; wenzelm@27042: 'instance' wenzelm@27042: ; wenzelm@27042: 'subclass' target? nameref wenzelm@27042: ; wenzelm@27042: 'print\_classes' wenzelm@27042: ; wenzelm@27042: wenzelm@27042: superclassexpr: nameref | (nameref '+' superclassexpr) wenzelm@27042: ; wenzelm@27042: \end{rail} wenzelm@27042: wenzelm@27042: \begin{descr} wenzelm@27042: wenzelm@27042: \item [\hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}~\isa{{\isachardoublequote}c\ {\isacharequal}\ superclasses\ {\isacharplus}\ body{\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@27042: theory level (\emph{class operations} \isa{{\isachardoublequote}f\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ f\isactrlsub n{\isachardoublequote}} of class \isa{c}), mapping the local type parameter wenzelm@27042: \isa{{\isasymalpha}} to a schematic type variable \isa{{\isachardoublequote}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isachardoublequote}}. wenzelm@27042: wenzelm@27042: Likewise, \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}} in \isa{body} are also lifted, wenzelm@27042: mapping each local parameter \isa{{\isachardoublequote}f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} to its wenzelm@27042: corresponding global constant \isa{{\isachardoublequote}f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}}. The wenzelm@27042: corresponding introduction rule is provided as \isa{c{\isacharunderscore}class{\isacharunderscore}axioms{\isachardot}intro}. This rule should be rarely needed directly wenzelm@27042: --- the \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} method takes care of the details of wenzelm@27042: class membership proofs. wenzelm@27042: wenzelm@27042: \item [\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}\ s\ {\isasymBEGIN}{\isachardoublequote}}] opens a theory target (cf.\ wenzelm@27042: \secref{sec:target}) which allows to specify class operations \isa{{\isachardoublequote}f\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ f\isactrlsub n{\isachardoublequote}} corresponding to sort \isa{s} at the wenzelm@27042: particular type instance \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ s\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}}. A plain \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} command wenzelm@27042: in the target body poses a goal stating these type arities. The wenzelm@27042: target is 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; wenzelm@27042: this corresponds nicely to mutual recursive type definitions, e.g.\ wenzelm@27042: in Isabelle/HOL. wenzelm@27042: wenzelm@27042: \item [\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}] in an instantiation target body sets wenzelm@27042: 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{\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@27042: \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: wenzelm@27042: \item [\hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}}] prints all classes in the current wenzelm@27042: theory. wenzelm@27042: wenzelm@27042: \item [\hyperlink{method.intro-classes}{\mbox{\isa{intro{\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@27042: single ``\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}}'' proof step. wenzelm@26870: wenzelm@26870: \end{descr}% wenzelm@26870: \end{isamarkuptext}% wenzelm@26870: \isamarkuptrue% wenzelm@26870: % 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@27042: \item Local constant declarations \isa{{\isachardoublequote}g{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} referring to the wenzelm@27042: local type parameter \isa{{\isasymalpha}} and local parameters \isa{{\isachardoublequote}f{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} wenzelm@27042: are accompanied by theory-level constants \isa{{\isachardoublequote}g{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}} wenzelm@27042: referring to theory-level class operations \isa{{\isachardoublequote}f{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}}. wenzelm@27042: wenzelm@27042: \item Local theorem bindings are lifted as are assumptions. wenzelm@27042: wenzelm@27042: \item Local syntax refers to local operations \isa{{\isachardoublequote}g{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} and wenzelm@27042: global operations \isa{{\isachardoublequote}g{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\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: % wenzelm@27054: \isamarkupsubsection{Old-style axiomatic type classes \label{sec:axclass}% wenzelm@27042: } wenzelm@27042: \isamarkuptrue% wenzelm@27042: % wenzelm@27042: \begin{isamarkuptext}% wenzelm@27054: \begin{matharray}{rcl} wenzelm@27042: \indexdef{}{command}{axclass}\hypertarget{command.axclass}{\hyperlink{command.axclass}{\mbox{\isa{\isacommand{axclass}}}}} & : & \isartrans{theory}{theory} \\ wenzelm@27042: \indexdef{}{command}{instance}\hypertarget{command.instance}{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}} & : & \isartrans{theory}{proof(prove)} \\ wenzelm@27042: \end{matharray} wenzelm@27042: wenzelm@27042: Axiomatic type classes are Isabelle/Pure's primitive wenzelm@27042: \emph{definitional} interface to type classes. For practical wenzelm@27042: applications, you should consider using classes wenzelm@27042: (cf.~\secref{sec:classes}) which provide high level interface. wenzelm@27042: wenzelm@27042: \begin{rail} wenzelm@27042: 'axclass' classdecl (axmdecl prop +) wenzelm@27042: ; wenzelm@27042: 'instance' (nameref ('<' | subseteq) nameref | nameref '::' arity) wenzelm@27042: ; wenzelm@27042: \end{rail} wenzelm@27042: wenzelm@27042: \begin{descr} wenzelm@27042: wenzelm@27042: \item [\hyperlink{command.axclass}{\mbox{\isa{\isacommand{axclass}}}}~\isa{{\isachardoublequote}c\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ axms{\isachardoublequote}}] defines an axiomatic type class as the intersection of wenzelm@27042: existing classes, with additional axioms holding. Class axioms may wenzelm@27042: not contain more than one type variable. The class axioms (with wenzelm@27042: implicit sort constraints added) are bound to the given names. wenzelm@27042: Furthermore a class introduction rule is generated (being bound as wenzelm@27042: \isa{c{\isacharunderscore}class{\isachardot}intro}); this rule is employed by method \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} to support instantiation proofs of this class. wenzelm@27042: wenzelm@27042: The ``class axioms'' are stored as theorems according to the given wenzelm@27042: name specifications, adding \isa{{\isachardoublequote}c{\isacharunderscore}class{\isachardoublequote}} as name space prefix; wenzelm@27042: the same facts are also stored collectively as \isa{c{\isacharunderscore}class{\isachardot}axioms}. wenzelm@27042: wenzelm@27042: \item [\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}} and wenzelm@27042: \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}\ s{\isachardoublequote}}] wenzelm@27042: setup a goal stating a class relation or type arity. The proof wenzelm@27042: would usually proceed by \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}, and then establish wenzelm@27042: the characteristic theorems of the type classes involved. After wenzelm@27042: finishing the proof, the theory will be augmented by a type wenzelm@27042: signature declaration corresponding to the resulting theorem. wenzelm@27042: wenzelm@27042: \end{descr}% wenzelm@27042: \end{isamarkuptext}% wenzelm@27042: \isamarkuptrue% wenzelm@27042: % 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 wenzelm@27042: overloading (see \secref{sec:consts}). 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@27042: \indexdef{}{command}{overloading}\hypertarget{command.overloading}{\hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}}} & : & \isartrans{theory}{local{\dsh}theory} \\ wenzelm@27042: \end{matharray} wenzelm@27042: wenzelm@27042: \begin{rail} wenzelm@27042: 'overloading' \\ wenzelm@27042: ( string ( '==' | equiv ) term ( '(' 'unchecked' ')' )? + ) 'begin' wenzelm@27042: \end{rail} wenzelm@27042: wenzelm@27042: \begin{descr} wenzelm@27042: wenzelm@27042: \item [\hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymequiv}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\isactrlsub {\isadigit{1}}\ {\isasymAND}\ {\isasymdots}\ x\isactrlsub n\ {\isasymequiv}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\isactrlsub n\ {\isasymBEGIN}{\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@27042: by an explicitly given mapping from variable names \isa{{\isachardoublequote}x\isactrlsub i{\isachardoublequote}} to constants \isa{{\isachardoublequote}c\isactrlsub i{\isachardoublequote}} at particular type wenzelm@27042: instances. The definitions themselves are established using common wenzelm@27042: specification tools, using the names \isa{{\isachardoublequote}x\isactrlsub i{\isachardoublequote}} as wenzelm@27042: reference to the corresponding constants. The target is concluded wenzelm@27042: by \hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}}. wenzelm@27042: wenzelm@27042: A \isa{{\isachardoublequote}{\isacharparenleft}unchecked{\isacharparenright}{\isachardoublequote}} option disables global dependency checks for wenzelm@27042: the corresponding definition, which is occasionally useful for wenzelm@27042: exotic overloading. It is at the discretion of the user to avoid wenzelm@27042: malformed theory specifications! wenzelm@27042: wenzelm@27042: \end{descr}% 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@27042: \indexdef{}{command}{use}\hypertarget{command.use}{\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}} & : & \isarkeep{theory~|~local{\dsh}theory} \\ wenzelm@27042: \indexdef{}{command}{ML}\hypertarget{command.ML}{\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}} & : & \isarkeep{theory~|~local{\dsh}theory} \\ wenzelm@27042: \indexdef{}{command}{ML\_val}\hypertarget{command.ML-val}{\hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}}} & : & \isartrans{\cdot}{\cdot} \\ wenzelm@27042: \indexdef{}{command}{ML\_command}\hypertarget{command.ML-command}{\hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}}} & : & \isartrans{\cdot}{\cdot} \\ wenzelm@27042: \indexdef{}{command}{setup}\hypertarget{command.setup}{\hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}} & : & \isartrans{theory}{theory} \\ wenzelm@27042: \indexdef{}{command}{method\_setup}\hypertarget{command.method-setup}{\hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isacharunderscore}setup}}}}} & : & \isartrans{theory}{theory} \\ wenzelm@27042: \end{matharray} wenzelm@27042: wenzelm@27042: \begin{rail} wenzelm@27042: 'use' name wenzelm@27042: ; wenzelm@27042: ('ML' | 'ML\_val' | 'ML\_command' | 'setup') text wenzelm@27042: ; wenzelm@27042: 'method\_setup' name '=' text text wenzelm@27042: ; wenzelm@27042: \end{rail} wenzelm@27042: wenzelm@27042: \begin{descr} wenzelm@27042: wenzelm@27042: \item [\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}~\isa{{\isachardoublequote}file{\isachardoublequote}}] reads and executes ML wenzelm@27042: commands from \isa{{\isachardoublequote}file{\isachardoublequote}}. The current theory context is passed wenzelm@27042: 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@27042: wenzelm@27042: \item [\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}~\isa{{\isachardoublequote}text{\isachardoublequote}}] is similar to \hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}, but executes ML commands directly from the given \isa{{\isachardoublequote}text{\isachardoublequote}}. wenzelm@27042: wenzelm@27042: \item [\hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} and \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}}] are wenzelm@27042: diagnostic versions of \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}, which means that the context wenzelm@27042: may not be updated. \hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} echos the bindings produced wenzelm@27042: at the ML toplevel, but \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}} is silent. wenzelm@27042: wenzelm@27042: \item [\hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}~\isa{{\isachardoublequote}text{\isachardoublequote}}] changes the current theory wenzelm@27042: context by applying \isa{{\isachardoublequote}text{\isachardoublequote}}, which refers to an ML expression wenzelm@27042: of type \verb|"theory -> theory"|. This enables to initialize wenzelm@27042: any object-logic specific tools and packages written in ML, for wenzelm@27042: example. wenzelm@27042: wenzelm@27042: \item [\hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isacharunderscore}setup}}}}~\isa{{\isachardoublequote}name\ {\isacharequal}\ text\ description{\isachardoublequote}}] wenzelm@27042: defines a proof method in the current theory. The given \isa{{\isachardoublequote}text{\isachardoublequote}} has to be an ML expression of type \verb|"Args.src ->|\isasep\isanewline% wenzelm@27042: \verb| Proof.context -> Proof.method"|. Parsing concrete method syntax wenzelm@27042: from \verb|Args.src| input can be quite tedious in general. The wenzelm@27042: following simple examples are for methods without any explicit wenzelm@27042: arguments, or a list of theorems, respectively. wenzelm@27042: wenzelm@27042: %FIXME proper antiquotations wenzelm@27042: {\footnotesize wenzelm@27042: \begin{verbatim} wenzelm@27042: Method.no_args (Method.METHOD (fn facts => foobar_tac)) wenzelm@27042: Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac)) wenzelm@27042: Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac)) wenzelm@27042: Method.thms_ctxt_args (fn thms => fn ctxt => wenzelm@27042: Method.METHOD (fn facts => foobar_tac)) wenzelm@27042: \end{verbatim} wenzelm@27042: } wenzelm@27042: wenzelm@27042: Note that mere tactic emulations may ignore the \isa{facts} wenzelm@27042: parameter above. Proper proof methods would do something wenzelm@27042: appropriate with the list of current facts, though. Single-rule wenzelm@27042: methods usually do strict forward-chaining (e.g.\ by using \verb|Drule.multi_resolves|), while automatic ones just insert the facts wenzelm@27042: using \verb|Method.insert_tac| before applying the main tactic. wenzelm@27042: wenzelm@27042: \end{descr}% wenzelm@27042: \end{isamarkuptext}% wenzelm@27042: \isamarkuptrue% wenzelm@27042: % 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@27042: \indexdef{}{command}{classes}\hypertarget{command.classes}{\hyperlink{command.classes}{\mbox{\isa{\isacommand{classes}}}}} & : & \isartrans{theory}{theory} \\ wenzelm@27042: \indexdef{}{command}{classrel}\hypertarget{command.classrel}{\hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}} & : & \isartrans{theory}{theory} & (axiomatic!) \\ wenzelm@27042: \indexdef{}{command}{defaultsort}\hypertarget{command.defaultsort}{\hyperlink{command.defaultsort}{\mbox{\isa{\isacommand{defaultsort}}}}} & : & \isartrans{theory}{theory} \\ wenzelm@27042: \indexdef{}{command}{class\_deps}\hypertarget{command.class-deps}{\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}}} & : & \isarkeep{theory~|~proof} \\ wenzelm@27042: \end{matharray} wenzelm@27042: wenzelm@27042: \begin{rail} wenzelm@27042: 'classes' (classdecl +) wenzelm@27042: ; wenzelm@27042: 'classrel' (nameref ('<' | subseteq) nameref + 'and') wenzelm@27042: ; wenzelm@27042: 'defaultsort' sort wenzelm@27042: ; wenzelm@27042: \end{rail} wenzelm@27042: wenzelm@27042: \begin{descr} wenzelm@27042: wenzelm@27042: \item [\hyperlink{command.classes}{\mbox{\isa{\isacommand{classes}}}}~\isa{{\isachardoublequote}c\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n{\isachardoublequote}}] wenzelm@27042: declares class \isa{c} to be a subclass of existing classes \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n{\isachardoublequote}}. Cyclic class structures are not permitted. wenzelm@27042: wenzelm@27042: \item [\hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}}] states wenzelm@27042: subclass relations between existing classes \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}{\isachardoublequote}} and wenzelm@27042: \isa{{\isachardoublequote}c\isactrlsub {\isadigit{2}}{\isachardoublequote}}. This is done axiomatically! The \indexref{}{command}{instance}\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} command (see \secref{sec:axclass}) provides a way to wenzelm@27042: introduce proven class relations. wenzelm@27042: wenzelm@27042: \item [\hyperlink{command.defaultsort}{\mbox{\isa{\isacommand{defaultsort}}}}~\isa{s}] makes sort \isa{s} the wenzelm@27042: new default sort for any type variables given without sort wenzelm@27042: constraints. Usually, the default sort would be only changed when wenzelm@27042: defining a new object-logic. wenzelm@27042: wenzelm@27042: \item [\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}}] visualizes the subclass relation, wenzelm@27042: using Isabelle's graph browser tool (see also \cite{isabelle-sys}). wenzelm@27042: wenzelm@27042: \end{descr}% 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@27042: \indexdef{}{command}{types}\hypertarget{command.types}{\hyperlink{command.types}{\mbox{\isa{\isacommand{types}}}}} & : & \isartrans{theory}{theory} \\ wenzelm@27042: \indexdef{}{command}{typedecl}\hypertarget{command.typedecl}{\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}} & : & \isartrans{theory}{theory} \\ wenzelm@27042: \indexdef{}{command}{nonterminals}\hypertarget{command.nonterminals}{\hyperlink{command.nonterminals}{\mbox{\isa{\isacommand{nonterminals}}}}} & : & \isartrans{theory}{theory} \\ wenzelm@27042: \indexdef{}{command}{arities}\hypertarget{command.arities}{\hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}} & : & \isartrans{theory}{theory} & (axiomatic!) \\ wenzelm@27042: \end{matharray} wenzelm@27042: wenzelm@27042: \begin{rail} wenzelm@27042: 'types' (typespec '=' type infix? +) wenzelm@27042: ; wenzelm@27042: 'typedecl' typespec infix? wenzelm@27042: ; wenzelm@27042: 'nonterminals' (name +) wenzelm@27042: ; wenzelm@27042: 'arities' (nameref '::' arity +) wenzelm@27042: ; wenzelm@27042: \end{rail} wenzelm@27042: wenzelm@27042: \begin{descr} wenzelm@27042: wenzelm@27042: \item [\hyperlink{command.types}{\mbox{\isa{\isacommand{types}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t\ {\isacharequal}\ {\isasymtau}{\isachardoublequote}}] wenzelm@27042: introduces \emph{type synonym} \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}} wenzelm@27042: for existing type \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}}. Unlike actual type definitions, as wenzelm@27042: are available in Isabelle/HOL for example, type synonyms are just wenzelm@27042: purely syntactic abbreviations without any logical significance. wenzelm@27042: Internally, type synonyms are fully expanded. wenzelm@27042: wenzelm@27042: \item [\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}}] wenzelm@27042: declares a new type constructor \isa{t}, intended as an actual wenzelm@27042: logical type (of the object-logic, if available). wenzelm@27042: wenzelm@27042: \item [\hyperlink{command.nonterminals}{\mbox{\isa{\isacommand{nonterminals}}}}~\isa{c}] declares type wenzelm@27042: constructors \isa{c} (without arguments) to act as purely wenzelm@27042: syntactic types, i.e.\ nonterminal symbols of Isabelle's inner wenzelm@27042: syntax of terms or types. wenzelm@27042: wenzelm@27042: \item [\hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}\ s{\isachardoublequote}}] augments Isabelle's order-sorted signature of types by new type wenzelm@27042: constructor arities. This is done axiomatically! The \indexref{}{command}{instance}\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} command (see \S\ref{sec:axclass}) provides a way to wenzelm@27042: introduce proven type arities. wenzelm@27042: wenzelm@27042: \end{descr}% wenzelm@27042: \end{isamarkuptext}% wenzelm@27042: \isamarkuptrue% wenzelm@27042: % 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@27042: simplest form of a definition is \isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\ {\isasymequiv}\ t{\isachardoublequote}}, where \isa{c} is a newly declared constant. Isabelle also allows derived forms wenzelm@27042: where the arguments of \isa{c} appear on the left, abbreviating a wenzelm@27042: prefix of \isa{{\isasymlambda}}-abstractions, e.g.\ \isa{{\isachardoublequote}c\ {\isasymequiv}\ {\isasymlambda}x\ y{\isachardot}\ t{\isachardoublequote}} may be wenzelm@27042: written more conveniently as \isa{{\isachardoublequote}c\ x\ y\ {\isasymequiv}\ t{\isachardoublequote}}. Moreover, wenzelm@27042: definitions may be weakened by adding arbitrary pre-conditions: wenzelm@27042: \isa{{\isachardoublequote}A\ {\isasymLongrightarrow}\ c\ x\ y\ {\isasymequiv}\ t{\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@27042: the left-hand side; this prohibits \isa{{\isachardoublequote}{\isadigit{0}}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymequiv}\ length\ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ list{\isacharparenright}{\isachardoublequote}} for example. 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: wenzelm@27042: Overloading means that a constant being declared as \isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ decl{\isachardoublequote}} may be defined separately on type instances \isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}{\isasymbeta}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymbeta}\isactrlsub n{\isacharparenright}\ t\ decl{\isachardoublequote}} for each type constructor \isa{t}. The right-hand side may mention overloaded constants wenzelm@27042: recursively at type instances corresponding to the immediate wenzelm@27042: argument types \isa{{\isachardoublequote}{\isasymbeta}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymbeta}\isactrlsub n{\isachardoublequote}}. Incomplete wenzelm@27042: specification patterns impose global constraints on all occurrences, wenzelm@27042: e.g.\ \isa{{\isachardoublequote}d\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymtimes}\ {\isasymalpha}{\isachardoublequote}} on the left-hand side means that all wenzelm@27042: corresponding occurrences on some right-hand side need to be an wenzelm@27042: instance of this, general \isa{{\isachardoublequote}d\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymtimes}\ {\isasymbeta}{\isachardoublequote}} will be disallowed. wenzelm@27042: wenzelm@27042: \begin{matharray}{rcl} wenzelm@27042: \indexdef{}{command}{consts}\hypertarget{command.consts}{\hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}} & : & \isartrans{theory}{theory} \\ wenzelm@27042: \indexdef{}{command}{defs}\hypertarget{command.defs}{\hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}}} & : & \isartrans{theory}{theory} \\ wenzelm@27042: \indexdef{}{command}{constdefs}\hypertarget{command.constdefs}{\hyperlink{command.constdefs}{\mbox{\isa{\isacommand{constdefs}}}}} & : & \isartrans{theory}{theory} \\ wenzelm@27042: \end{matharray} wenzelm@27042: wenzelm@27042: \begin{rail} wenzelm@27042: 'consts' ((name '::' type mixfix?) +) wenzelm@27042: ; wenzelm@27042: 'defs' ('(' 'unchecked'? 'overloaded'? ')')? \\ (axmdecl prop +) wenzelm@27042: ; wenzelm@27042: \end{rail} wenzelm@27042: wenzelm@27042: \begin{rail} wenzelm@27042: 'constdefs' structs? (constdecl? constdef +) wenzelm@27042: ; wenzelm@27042: wenzelm@27042: structs: '(' 'structure' (vars + 'and') ')' wenzelm@27042: ; wenzelm@27042: constdecl: ((name '::' type mixfix | name '::' type | name mixfix) 'where'?) | name 'where' wenzelm@27042: ; wenzelm@27042: constdef: thmdecl? prop wenzelm@27042: ; wenzelm@27042: \end{rail} wenzelm@27042: wenzelm@27042: \begin{descr} wenzelm@27042: wenzelm@27042: \item [\hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}~\isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}{\isachardoublequote}}] declares constant wenzelm@27042: \isa{c} to have any instance of type scheme \isa{{\isasymsigma}}. The wenzelm@27042: optional mixfix annotations may attach concrete syntax to the wenzelm@27042: constants declared. wenzelm@27042: wenzelm@27042: \item [\hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}}~\isa{{\isachardoublequote}name{\isacharcolon}\ eqn{\isachardoublequote}}] introduces \isa{eqn} wenzelm@27042: as a definitional axiom for some existing constant. wenzelm@27042: wenzelm@27042: The \isa{{\isachardoublequote}{\isacharparenleft}unchecked{\isacharparenright}{\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@27042: The \isa{{\isachardoublequote}{\isacharparenleft}overloaded{\isacharparenright}{\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@27042: \item [\hyperlink{command.constdefs}{\mbox{\isa{\isacommand{constdefs}}}}] provides a streamlined combination of wenzelm@27042: constants declarations and definitions: type-inference takes care of wenzelm@27042: the most general typing of the given specification (the optional wenzelm@27042: type constraint may refer to type-inference dummies ``\isa{{\isacharunderscore}}'' as usual). The resulting type declaration needs to agree with wenzelm@27042: that of the specification; overloading is \emph{not} supported here! wenzelm@27042: wenzelm@27042: The constant name may be omitted altogether, if neither type nor wenzelm@27042: syntax declarations are given. The canonical name of the wenzelm@27042: definitional axiom for constant \isa{c} will be \isa{c{\isacharunderscore}def}, wenzelm@27042: unless specified otherwise. Also note that the given list of wenzelm@27042: specifications is processed in a strictly sequential manner, with wenzelm@27042: type-checking being performed independently. wenzelm@27042: wenzelm@27042: An optional initial context of \isa{{\isachardoublequote}{\isacharparenleft}structure{\isacharparenright}{\isachardoublequote}} declarations wenzelm@27042: admits use of indexed syntax, using the special symbol \verb|\| (printed as ``\isa{{\isachardoublequote}{\isasymindex}{\isachardoublequote}}''). The latter concept is wenzelm@27042: particularly useful with locales (see also \S\ref{sec:locale}). wenzelm@27042: wenzelm@27042: \end{descr}% 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@27042: \indexdef{}{command}{axioms}\hypertarget{command.axioms}{\hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}}} & : & \isartrans{theory}{theory} & (axiomatic!) \\ wenzelm@27042: \indexdef{}{command}{lemmas}\hypertarget{command.lemmas}{\hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}} & : & \isarkeep{local{\dsh}theory} \\ wenzelm@27047: \indexdef{}{command}{theorems}\hypertarget{command.theorems}{\hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}}} & : & \isarkeep{local{\dsh}theory} \\ wenzelm@27042: \end{matharray} wenzelm@27042: wenzelm@27042: \begin{rail} wenzelm@27042: 'axioms' (axmdecl prop +) wenzelm@27042: ; wenzelm@27042: ('lemmas' | 'theorems') target? (thmdef? thmrefs + 'and') wenzelm@27042: ; wenzelm@27042: \end{rail} wenzelm@27042: wenzelm@27042: \begin{descr} wenzelm@27042: wenzelm@27042: \item [\hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\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@27042: \item [\hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}~\isa{{\isachardoublequote}a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}}] wenzelm@27042: retrieves and stores existing facts in the theory context, or the wenzelm@27042: specified target context (see also \secref{sec:target}). Typical wenzelm@27042: applications would also involve attributes, to declare Simplifier wenzelm@27042: rules, for example. wenzelm@27042: wenzelm@27042: \item [\hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}}] is essentially the same as \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}, but marks the result as a different kind of facts. wenzelm@27042: wenzelm@27042: \end{descr}% 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@27042: \begin{matharray}{rcl} wenzelm@27042: \indexdef{}{command}{oracle}\hypertarget{command.oracle}{\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}} & : & \isartrans{theory}{theory} \\ wenzelm@27042: \end{matharray} wenzelm@27042: wenzelm@27042: The oracle interface promotes a given ML function \verb|theory -> T -> term| to \verb|theory -> T -> thm|, for some wenzelm@27042: type \verb|T| given by the user. This acts like an infinitary wenzelm@27042: specification of axioms -- there is no internal check of the wenzelm@27042: correctness of the results! The inference kernel records oracle wenzelm@27042: invocations within the internal derivation object of theorems, and wenzelm@27042: the pretty printer attaches ``\isa{{\isachardoublequote}{\isacharbrackleft}{\isacharbang}{\isacharbrackright}{\isachardoublequote}}'' to indicate results wenzelm@27042: that are not fully checked by Isabelle inferences. wenzelm@27042: wenzelm@27042: \begin{rail} wenzelm@27042: 'oracle' name '(' type ')' '=' text wenzelm@27042: ; wenzelm@27042: \end{rail} wenzelm@27042: wenzelm@27042: \begin{descr} wenzelm@27042: wenzelm@27042: \item [\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}~\isa{{\isachardoublequote}name\ {\isacharparenleft}type{\isacharparenright}\ {\isacharequal}\ text{\isachardoublequote}}] turns the wenzelm@27042: given ML expression \isa{{\isachardoublequote}text{\isachardoublequote}} of type wenzelm@27042: \verb|theory ->|~\isa{{\isachardoublequote}type{\isachardoublequote}}~\verb|-> term| into an wenzelm@27042: ML function of type wenzelm@27042: \verb|theory ->|~\isa{{\isachardoublequote}type{\isachardoublequote}}~\verb|-> thm|, which is wenzelm@27042: bound to the global identifier \verb|name|. wenzelm@27042: wenzelm@27042: \end{descr}% 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@27042: \indexdef{}{command}{global}\hypertarget{command.global}{\hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}}} & : & \isartrans{theory}{theory} \\ wenzelm@27042: \indexdef{}{command}{local}\hypertarget{command.local}{\hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}}} & : & \isartrans{theory}{theory} \\ wenzelm@27042: \indexdef{}{command}{hide}\hypertarget{command.hide}{\hyperlink{command.hide}{\mbox{\isa{\isacommand{hide}}}}} & : & \isartrans{theory}{theory} \\ wenzelm@27042: \end{matharray} wenzelm@27042: wenzelm@27042: \begin{rail} wenzelm@27042: 'hide' ('(open)')? name (nameref + ) wenzelm@27042: ; wenzelm@27042: \end{rail} 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@27042: \begin{descr} wenzelm@27042: wenzelm@27042: \item [\hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}} and \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}}] change the wenzelm@27042: current name declaration mode. Initially, theories start in wenzelm@27042: \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}} mode, causing all names to be automatically wenzelm@27042: qualified by the theory name. Changing this to \hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}} wenzelm@27042: causes all names to be declared without the theory prefix, until wenzelm@27042: \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}} is declared again. wenzelm@27042: wenzelm@27042: Note that global names are prone to get hidden accidently later, wenzelm@27042: when qualified names of the same base name are introduced. wenzelm@27042: wenzelm@27042: \item [\hyperlink{command.hide}{\mbox{\isa{\isacommand{hide}}}}~\isa{{\isachardoublequote}space\ names{\isachardoublequote}}] fully removes wenzelm@27042: declarations from a given name space (which may be \isa{{\isachardoublequote}class{\isachardoublequote}}, wenzelm@27042: \isa{{\isachardoublequote}type{\isachardoublequote}}, \isa{{\isachardoublequote}const{\isachardoublequote}}, or \isa{{\isachardoublequote}fact{\isachardoublequote}}); with the \isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}} option, only the base name is hidden. Global wenzelm@27042: (unqualified) names may never be hidden. wenzelm@27042: wenzelm@27042: Note that hiding name space accesses has no impact on logical wenzelm@27042: declarations -- they remain valid internally. Entities that are no wenzelm@27042: longer accessible to the user are printed with the special qualifier wenzelm@27042: ``\isa{{\isachardoublequote}{\isacharquery}{\isacharquery}{\isachardoublequote}}'' prefixed to the full internal name. wenzelm@27042: wenzelm@27042: \end{descr}% wenzelm@27042: \end{isamarkuptext}% wenzelm@27042: \isamarkuptrue% wenzelm@27042: % wenzelm@27042: \isamarkupsection{Syntax and translations \label{sec:syn-trans}% wenzelm@27042: } wenzelm@27042: \isamarkuptrue% wenzelm@27042: % wenzelm@27042: \begin{isamarkuptext}% wenzelm@27042: \begin{matharray}{rcl} wenzelm@27042: \indexdef{}{command}{syntax}\hypertarget{command.syntax}{\hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}}} & : & \isartrans{theory}{theory} \\ wenzelm@27042: \indexdef{}{command}{no\_syntax}\hypertarget{command.no-syntax}{\hyperlink{command.no-syntax}{\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}}}} & : & \isartrans{theory}{theory} \\ wenzelm@27042: \indexdef{}{command}{translations}\hypertarget{command.translations}{\hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}} & : & \isartrans{theory}{theory} \\ wenzelm@27042: \indexdef{}{command}{no\_translations}\hypertarget{command.no-translations}{\hyperlink{command.no-translations}{\mbox{\isa{\isacommand{no{\isacharunderscore}translations}}}}} & : & \isartrans{theory}{theory} \\ wenzelm@27042: \end{matharray} wenzelm@27042: wenzelm@27042: \begin{rail} wenzelm@27042: ('syntax' | 'no\_syntax') mode? (constdecl +) wenzelm@27042: ; wenzelm@27042: ('translations' | 'no\_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +) wenzelm@27042: ; wenzelm@27042: wenzelm@27042: mode: ('(' ( name | 'output' | name 'output' ) ')') wenzelm@27042: ; wenzelm@27042: transpat: ('(' nameref ')')? string wenzelm@27042: ; wenzelm@27042: \end{rail} wenzelm@27042: wenzelm@27042: \begin{descr} wenzelm@27042: wenzelm@27042: \item [\hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}}~\isa{{\isachardoublequote}{\isacharparenleft}mode{\isacharparenright}\ decls{\isachardoublequote}}] is similar to wenzelm@27042: \hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}~\isa{decls}, except that the actual logical wenzelm@27042: signature extension is omitted. Thus the context free grammar of wenzelm@27042: Isabelle's inner syntax may be augmented in arbitrary ways, wenzelm@27042: independently of the logic. The \isa{mode} argument refers to the wenzelm@27042: print mode that the grammar rules belong; unless the \indexref{}{keyword}{output}\hyperlink{keyword.output}{\mbox{\isa{\isakeyword{output}}}} indicator is given, all productions are added both to the wenzelm@27042: input and output grammar. wenzelm@27042: wenzelm@27042: \item [\hyperlink{command.no-syntax}{\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}}}~\isa{{\isachardoublequote}{\isacharparenleft}mode{\isacharparenright}\ decls{\isachardoublequote}}] removes wenzelm@27042: grammar declarations (and translations) resulting from \isa{decls}, which are interpreted in the same manner as for \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} above. wenzelm@27042: wenzelm@27042: \item [\hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}~\isa{rules}] specifies syntactic wenzelm@27042: translation rules (i.e.\ macros): parse~/ print rules (\isa{{\isachardoublequote}{\isasymrightleftharpoons}{\isachardoublequote}}), wenzelm@27042: parse rules (\isa{{\isachardoublequote}{\isasymrightharpoonup}{\isachardoublequote}}), or print rules (\isa{{\isachardoublequote}{\isasymleftharpoondown}{\isachardoublequote}}). wenzelm@27042: Translation patterns may be prefixed by the syntactic category to be wenzelm@27042: used for parsing; the default is \isa{logic}. wenzelm@27042: wenzelm@27042: \item [\hyperlink{command.no-translations}{\mbox{\isa{\isacommand{no{\isacharunderscore}translations}}}}~\isa{rules}] removes syntactic wenzelm@27042: translation rules, which are interpreted in the same manner as for wenzelm@27042: \hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}} above. wenzelm@27042: wenzelm@27042: \end{descr}% wenzelm@27042: \end{isamarkuptext}% wenzelm@27042: \isamarkuptrue% wenzelm@27042: % wenzelm@27042: \isamarkupsection{Syntax translation functions% wenzelm@27042: } wenzelm@27042: \isamarkuptrue% wenzelm@27042: % wenzelm@27042: \begin{isamarkuptext}% wenzelm@27042: \begin{matharray}{rcl} wenzelm@27042: \indexdef{}{command}{parse\_ast\_translation}\hypertarget{command.parse-ast-translation}{\hyperlink{command.parse-ast-translation}{\mbox{\isa{\isacommand{parse{\isacharunderscore}ast{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\ wenzelm@27042: \indexdef{}{command}{parse\_translation}\hypertarget{command.parse-translation}{\hyperlink{command.parse-translation}{\mbox{\isa{\isacommand{parse{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\ wenzelm@27042: \indexdef{}{command}{print\_translation}\hypertarget{command.print-translation}{\hyperlink{command.print-translation}{\mbox{\isa{\isacommand{print{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\ wenzelm@27042: \indexdef{}{command}{typed\_print\_translation}\hypertarget{command.typed-print-translation}{\hyperlink{command.typed-print-translation}{\mbox{\isa{\isacommand{typed{\isacharunderscore}print{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\ wenzelm@27042: \indexdef{}{command}{print\_ast\_translation}\hypertarget{command.print-ast-translation}{\hyperlink{command.print-ast-translation}{\mbox{\isa{\isacommand{print{\isacharunderscore}ast{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\ wenzelm@27042: \indexdef{}{command}{token\_translation}\hypertarget{command.token-translation}{\hyperlink{command.token-translation}{\mbox{\isa{\isacommand{token{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\ wenzelm@27042: \end{matharray} wenzelm@27042: wenzelm@27042: \begin{rail} wenzelm@27042: ( 'parse\_ast\_translation' | 'parse\_translation' | 'print\_translation' | wenzelm@27042: 'typed\_print\_translation' | 'print\_ast\_translation' ) ('(advanced)')? text wenzelm@27042: ; wenzelm@27042: wenzelm@27042: 'token\_translation' text wenzelm@27042: ; wenzelm@27042: \end{rail} wenzelm@27042: wenzelm@27042: Syntax translation functions written in ML admit almost arbitrary wenzelm@27042: manipulations of Isabelle's inner syntax. Any of the above commands wenzelm@27042: have a single \railqtok{text} argument that refers to an ML wenzelm@27042: expression of appropriate type, which are as follows by default: wenzelm@27042: wenzelm@27042: %FIXME proper antiquotations wenzelm@27042: \begin{ttbox} wenzelm@27042: val parse_ast_translation : (string * (ast list -> ast)) list wenzelm@27042: val parse_translation : (string * (term list -> term)) list wenzelm@27042: val print_translation : (string * (term list -> term)) list wenzelm@27042: val typed_print_translation : wenzelm@27042: (string * (bool -> typ -> term list -> term)) list wenzelm@27042: val print_ast_translation : (string * (ast list -> ast)) list wenzelm@27042: val token_translation : wenzelm@27042: (string * string * (string -> string * real)) list wenzelm@27042: \end{ttbox} wenzelm@27042: wenzelm@27042: If the \isa{{\isachardoublequote}{\isacharparenleft}advanced{\isacharparenright}{\isachardoublequote}} option is given, the corresponding wenzelm@27042: translation functions may depend on the current theory or proof wenzelm@27042: context. This allows to implement advanced syntax mechanisms, as wenzelm@27042: translations functions may refer to specific theory declarations or wenzelm@27042: auxiliary proof data. wenzelm@27042: wenzelm@27042: See also \cite[\S8]{isabelle-ref} for more information on the wenzelm@27042: general concept of syntax transformations in Isabelle. wenzelm@27042: wenzelm@27042: %FIXME proper antiquotations wenzelm@27042: \begin{ttbox} wenzelm@27042: val parse_ast_translation: wenzelm@27047: (string * (Proof.context -> ast list -> ast)) list wenzelm@27042: val parse_translation: wenzelm@27047: (string * (Proof.context -> term list -> term)) list wenzelm@27042: val print_translation: wenzelm@27047: (string * (Proof.context -> term list -> term)) list wenzelm@27042: val typed_print_translation: wenzelm@27047: (string * (Proof.context -> bool -> typ -> term list -> term)) list wenzelm@27042: val print_ast_translation: wenzelm@27047: (string * (Proof.context -> ast list -> ast)) list wenzelm@27042: \end{ttbox}% 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: