wneuper/isa: doc-src/IsarRef/Thy/document/Spec.tex@3f19e324ff59

1 %

     2 \begin{isabellebody}%

     3 \def\isabellecontext{Spec}%

4 %

     5 \isadelimtheory

6 %

     7 \endisadelimtheory

8 %

     9 \isatagtheory

    10 \isacommand{theory}\isamarkupfalse%

    11 \ Spec\isanewline

    12 \isakeyword{imports}\ Base\ Main\isanewline

    13 \isakeyword{begin}%

    14 \endisatagtheory

    15 {\isafoldtheory}%

    16 %

    17 \isadelimtheory

    18 %

    19 \endisadelimtheory

    20 %

    21 \isamarkupchapter{Theory specifications%

    22 }

    23 \isamarkuptrue%

    24 %

    25 \begin{isamarkuptext}%

    26 The Isabelle/Isar theory format integrates specifications and

    27   proofs, supporting interactive development with unlimited undo

    28   operation.  There is an integrated document preparation system (see

    29   \chref{ch:document-prep}), for typesetting formal developments

    30   together with informal text.  The resulting hyper-linked PDF

    31   documents can be used both for WWW presentation and printed copies.

    33   The Isar proof language (see \chref{ch:proofs}) is embedded into the

    34   theory language as a proper sub-language.  Proof mode is entered by

    35   stating some \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}} or \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}} at the theory

    36   level, and left again with the final conclusion (e.g.\ via \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}).  Some theory specification mechanisms also require a proof,

    37   such as \hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}} in HOL, which demands non-emptiness of

    38   the representing sets.%

    39 \end{isamarkuptext}%

    40 \isamarkuptrue%

    41 %

    42 \isamarkupsection{Defining theories \label{sec:begin-thy}%

    43 }

    44 \isamarkuptrue%

    45 %

    46 \begin{isamarkuptext}%

    47 \begin{matharray}{rcl}

    48     \indexdef{}{command}{theory}\hypertarget{command.theory}{\hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}toplevel\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\

    49     \indexdef{global}{command}{end}\hypertarget{command.global.end}{\hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ toplevel{\isaliteral{22}{\isachardoublequote}}} \\

    50   \end{matharray}

    52   Isabelle/Isar theories are defined via theory files, which may

    53   contain both specifications and proofs; occasionally definitional

    54   mechanisms also require some explicit proof.  The theory body may be

    55   sub-structured by means of \emph{local theory targets}, such as

    56   \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}} and \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}.

    58   The first proper command of a theory is \hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}}, which

    59   indicates imports of previous theories and optional dependencies on

    60   other source files (usually in ML).  Just preceding the initial

    61   \hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}} command there may be an optional \hyperlink{command.header}{\mbox{\isa{\isacommand{header}}}} declaration, which is only relevant to document

    62   preparation: see also the other section markup commands in

    63   \secref{sec:markup}.

    65   A theory is concluded by a final \hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}} command,

    66   one that does not belong to a local theory target.  No further

    67   commands may follow such a global \hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}},

    68   although some user-interfaces might pretend that trailing input is

    69   admissible.

    71   \begin{railoutput}

    72 \rail@begin{4}{}

    73 \rail@term{\hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}}}[]

    74 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

    75 \rail@cr{2}

    76 \rail@term{\isa{\isakeyword{imports}}}[]

    77 \rail@plus

    78 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

    79 \rail@nextplus{3}

    80 \rail@endplus

    81 \rail@bar

    82 \rail@nextbar{3}

    83 \rail@nont{\isa{uses}}[]

    84 \rail@endbar

    85 \rail@term{\isa{\isakeyword{begin}}}[]

    86 \rail@end

    87 \rail@begin{3}{\isa{uses}}

    88 \rail@term{\isa{\isakeyword{uses}}}[]

    89 \rail@plus

    90 \rail@bar

    91 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

    92 \rail@nextbar{1}

    93 \rail@nont{\hyperlink{syntax.parname}{\mbox{\isa{parname}}}}[]

    94 \rail@endbar

    95 \rail@nextplus{2}

    96 \rail@endplus

    97 \rail@end

    98 \end{railoutput}

   101   \begin{description}

   103   \item \hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{5C3C494D504F5254533E}{\isasymIMPORTS}}\ B\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ B\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C424547494E3E}{\isasymBEGIN}}{\isaliteral{22}{\isachardoublequote}}}

   104   starts a new theory \isa{A} based on the merge of existing

   105   theories \isa{{\isaliteral{22}{\isachardoublequote}}B\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ B\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}.

   107   Due to the possibility to import more than one ancestor, the

   108   resulting theory structure of an Isabelle session forms a directed

   109   acyclic graph (DAG).  Isabelle's theory loader ensures that the

   110   sources contributing to the development graph are always up-to-date:

   111   changed files are automatically reloaded whenever a theory header

   112   specification is processed.

   114   The optional \indexdef{}{keyword}{uses}\hypertarget{keyword.uses}{\hyperlink{keyword.uses}{\mbox{\isa{\isakeyword{uses}}}}} specification declares additional

   115   dependencies on extra files (usually ML sources).  Files will be

   116   loaded immediately (as ML), unless the name is parenthesized.  The

   117   latter case records a dependency that needs to be resolved later in

   118   the text, usually via explicit \indexref{}{command}{use}\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}} for ML files;

   119   other file formats require specific load commands defined by the

   120   corresponding tools or packages.

   122   \item \hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}} concludes the current theory

   123   definition.  Note that local theory targets involve a local

   124   \hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}}, which is clear from the nesting.

   126   \end{description}%

   127 \end{isamarkuptext}%

   128 \isamarkuptrue%

   129 %

   130 \isamarkupsection{Local theory targets \label{sec:target}%

   131 }

   132 \isamarkuptrue%

   133 %

   134 \begin{isamarkuptext}%

   135 A local theory target is a context managed separately within the

   136   enclosing theory.  Contexts may introduce parameters (fixed

   137   variables) and assumptions (hypotheses).  Definitions and theorems

   138   depending on the context may be added incrementally later on.  Named

   139   contexts refer to locales (cf.\ \secref{sec:locale}) or type classes

   140   (cf.\ \secref{sec:class}); the name ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{22}{\isachardoublequote}}}'' signifies the

   141   global theory context.

   143   \begin{matharray}{rcll}

   144     \indexdef{}{command}{context}\hypertarget{command.context}{\hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\

   145     \indexdef{local}{command}{end}\hypertarget{command.local.end}{\hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\

   146   \end{matharray}

   148   \begin{railoutput}

   149 \rail@begin{1}{}

   150 \rail@term{\hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}}[]

   151 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

   152 \rail@term{\isa{\isakeyword{begin}}}[]

   153 \rail@end

   154 \rail@begin{1}{\indexdef{}{syntax}{target}\hypertarget{syntax.target}{\hyperlink{syntax.target}{\mbox{\isa{target}}}}}

   155 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]

   156 \rail@term{\isa{\isakeyword{in}}}[]

   157 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

   158 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]

   159 \rail@end

   160 \end{railoutput}

   163   \begin{description}

   165   \item \hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{5C3C424547494E3E}{\isasymBEGIN}}{\isaliteral{22}{\isachardoublequote}}} recommences an

   166   existing locale or class context \isa{c}.  Note that locale and

   167   class definitions allow to include the \hyperlink{keyword.begin}{\mbox{\isa{\isakeyword{begin}}}} keyword as

   168   well, in order to continue the local theory immediately after the

   169   initial specification.

   171   \item \hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}} concludes the current local theory

   172   and continues the enclosing global theory.  Note that a global

   173   \hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}} has a different meaning: it concludes the

   174   theory itself (\secref{sec:begin-thy}).

   176   \item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}}\indexdef{}{keyword}{in}\hypertarget{keyword.in}{\hyperlink{keyword.in}{\mbox{\isa{\isakeyword{in}}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} given after any

   177   local theory command specifies an immediate target, e.g.\

   178   ``\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C494E3E}{\isasymIN}}\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}'' or ``\hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C494E3E}{\isasymIN}}\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}''.  This works both in a local or

   179   global theory context; the current target context will be suspended

   180   for this command only.  Note that ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C494E3E}{\isasymIN}}\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'' will

   181   always produce a global result independently of the current target

   182   context.

   184   \end{description}

   186   The exact meaning of results produced within a local theory context

   187   depends on the underlying target infrastructure (locale, type class

   188   etc.).  The general idea is as follows, considering a context named

   189   \isa{c} with parameter \isa{x} and assumption \isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}}.

   191   Definitions are exported by introducing a global version with

   192   additional arguments; a syntactic abbreviation links the long form

   193   with the abstract version of the target context.  For example,

   194   \isa{{\isaliteral{22}{\isachardoublequote}}a\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} becomes \isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{2E}{\isachardot}}a\ {\isaliteral{3F}{\isacharquery}}x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} at the theory

   195   level (for arbitrary \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}x{\isaliteral{22}{\isachardoublequote}}}), together with a local

   196   abbreviation \isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ c{\isaliteral{2E}{\isachardot}}a\ x{\isaliteral{22}{\isachardoublequote}}} in the target context (for the

   197   fixed parameter \isa{x}).

   199   Theorems are exported by discharging the assumptions and

   200   generalizing the parameters of the context.  For example, \isa{{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{3A}{\isacharcolon}}\ B{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} becomes \isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{2E}{\isachardot}}a{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}x{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}}, again for arbitrary

   201   \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}x{\isaliteral{22}{\isachardoublequote}}}.%

   202 \end{isamarkuptext}%

   203 \isamarkuptrue%

   204 %

   205 \isamarkupsection{Basic specification elements%

   206 }

   207 \isamarkuptrue%

   208 %

   209 \begin{isamarkuptext}%

   210 \begin{matharray}{rcll}

   211     \indexdef{}{command}{axiomatization}\hypertarget{command.axiomatization}{\hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{axiomatization}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} & (axiomatic!) \\

   212     \indexdef{}{command}{definition}\hypertarget{command.definition}{\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\

   213     \indexdef{}{attribute}{defn}\hypertarget{attribute.defn}{\hyperlink{attribute.defn}{\mbox{\isa{defn}}}} & : & \isa{attribute} \\

   214     \indexdef{}{command}{abbreviation}\hypertarget{command.abbreviation}{\hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\

   215     \indexdef{}{command}{print\_abbrevs}\hypertarget{command.print-abbrevs}{\hyperlink{command.print-abbrevs}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}abbrevs}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ {\isaliteral{22}{\isachardoublequote}}} \\

   216   \end{matharray}

   218   These specification mechanisms provide a slightly more abstract view

   219   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

   220   \secref{sec:axms-thms}).  In particular, type-inference is commonly

   221   available, and result names need not be given.

   223   \begin{railoutput}

   224 \rail@begin{2}{}

   225 \rail@term{\hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{axiomatization}}}}}[]

   226 \rail@bar

   227 \rail@nextbar{1}

   228 \rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]

   229 \rail@endbar

   230 \rail@bar

   231 \rail@nextbar{1}

   232 \rail@term{\isa{\isakeyword{where}}}[]

   233 \rail@nont{\isa{specs}}[]

   234 \rail@endbar

   235 \rail@end

   236 \rail@begin{5}{}

   237 \rail@term{\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}}[]

   238 \rail@bar

   239 \rail@nextbar{1}

   240 \rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]

   241 \rail@endbar

   242 \rail@cr{3}

   243 \rail@bar

   244 \rail@nextbar{4}

   245 \rail@nont{\isa{decl}}[]

   246 \rail@term{\isa{\isakeyword{where}}}[]

   247 \rail@endbar

   248 \rail@bar

   249 \rail@nextbar{4}

   250 \rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]

   251 \rail@endbar

   252 \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]

   253 \rail@end

   254 \rail@begin{5}{}

   255 \rail@term{\hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}}[]

   256 \rail@bar

   257 \rail@nextbar{1}

   258 \rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]

   259 \rail@endbar

   260 \rail@bar

   261 \rail@nextbar{1}

   262 \rail@nont{\hyperlink{syntax.mode}{\mbox{\isa{mode}}}}[]

   263 \rail@endbar

   264 \rail@cr{3}

   265 \rail@bar

   266 \rail@nextbar{4}

   267 \rail@nont{\isa{decl}}[]

   268 \rail@term{\isa{\isakeyword{where}}}[]

   269 \rail@endbar

   270 \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]

   271 \rail@end

   272 \rail@begin{4}{\indexdef{}{syntax}{fixes}\hypertarget{syntax.fixes}{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}}

   273 \rail@plus

   274 \rail@bar

   275 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

   276 \rail@bar

   277 \rail@nextbar{1}

   278 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}}}[]

   279 \rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]

   280 \rail@endbar

   281 \rail@bar

   282 \rail@nextbar{1}

   283 \rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]

   284 \rail@endbar

   285 \rail@nextbar{2}

   286 \rail@nont{\hyperlink{syntax.vars}{\mbox{\isa{vars}}}}[]

   287 \rail@endbar

   288 \rail@nextplus{3}

   289 \rail@cterm{\isa{\isakeyword{and}}}[]

   290 \rail@endplus

   291 \rail@end

   292 \rail@begin{3}{\isa{specs}}

   293 \rail@plus

   294 \rail@bar

   295 \rail@nextbar{1}

   296 \rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]

   297 \rail@endbar

   298 \rail@nont{\hyperlink{syntax.props}{\mbox{\isa{props}}}}[]

   299 \rail@nextplus{2}

   300 \rail@cterm{\isa{\isakeyword{and}}}[]

   301 \rail@endplus

   302 \rail@end

   303 \rail@begin{2}{\isa{decl}}

   304 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

   305 \rail@bar

   306 \rail@nextbar{1}

   307 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}}}[]

   308 \rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]

   309 \rail@endbar

   310 \rail@bar

   311 \rail@nextbar{1}

   312 \rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]

   313 \rail@endbar

   314 \rail@end

   315 \end{railoutput}

   318   \begin{description}

   320   \item \hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{axiomatization}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub m\ {\isaliteral{5C3C57484552453E}{\isasymWHERE}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}

   321   introduces several constants simultaneously and states axiomatic

   322   properties for these.  The constants are marked as being specified

   323   once and for all, which prevents additional specifications being

   324   issued later on.

   326   Note that axiomatic specifications are only appropriate when

   327   declaring a new logical system; axiomatic specifications are

   328   restricted to global theory contexts.  Normal applications should

   329   only use definitional mechanisms!

   331   \item \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{5C3C57484552453E}{\isasymWHERE}}\ eq{\isaliteral{22}{\isachardoublequote}}} produces an

   332   internal definition \isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t{\isaliteral{22}{\isachardoublequote}}} according to the specification

   333   given as \isa{eq}, which is then turned into a proven fact.  The

   334   given proposition may deviate from internal meta-level equality

   335   according to the rewrite rules declared as \hyperlink{attribute.defn}{\mbox{\isa{defn}}} by the

   336   object-logic.  This usually covers object-level equality \isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{22}{\isachardoublequote}}} and equivalence \isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{5C3C6C65667472696768746172726F773E}{\isasymleftrightarrow}}\ B{\isaliteral{22}{\isachardoublequote}}}.  End-users normally need not

   337   change the \hyperlink{attribute.defn}{\mbox{\isa{defn}}} setup.

   339   Definitions may be presented with explicit arguments on the LHS, as

   340   well as additional conditions, e.g.\ \isa{{\isaliteral{22}{\isachardoublequote}}f\ x\ y\ {\isaliteral{3D}{\isacharequal}}\ t{\isaliteral{22}{\isachardoublequote}}} instead of

   341   \isa{{\isaliteral{22}{\isachardoublequote}}f\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x\ y{\isaliteral{2E}{\isachardot}}\ t{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}y\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isadigit{0}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ g\ x\ y\ {\isaliteral{3D}{\isacharequal}}\ u{\isaliteral{22}{\isachardoublequote}}} instead of an

   342   unrestricted \isa{{\isaliteral{22}{\isachardoublequote}}g\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x\ y{\isaliteral{2E}{\isachardot}}\ u{\isaliteral{22}{\isachardoublequote}}}.

   344   \item \hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{5C3C57484552453E}{\isasymWHERE}}\ eq{\isaliteral{22}{\isachardoublequote}}} introduces a

   345   syntactic constant which is associated with a certain term according

   346   to the meta-level equality \isa{eq}.

   348   Abbreviations participate in the usual type-inference process, but

   349   are expanded before the logic ever sees them.  Pretty printing of

   350   terms involves higher-order rewriting with rules stemming from

   351   reverted abbreviations.  This needs some care to avoid overlapping

   352   or looping syntactic replacements!

   354   The optional \isa{mode} specification restricts output to a

   355   particular print mode; using ``\isa{input}'' here achieves the

   356   effect of one-way abbreviations.  The mode may also include an

   357   ``\hyperlink{keyword.output}{\mbox{\isa{\isakeyword{output}}}}'' qualifier that affects the concrete syntax

   358   declared for abbreviations, cf.\ \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} in

   359   \secref{sec:syn-trans}.

   361   \item \hyperlink{command.print-abbrevs}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}abbrevs}}}} prints all constant abbreviations

   362   of the current context.

   364   \end{description}%

   365 \end{isamarkuptext}%

   366 \isamarkuptrue%

   367 %

   368 \isamarkupsection{Generic declarations%

   369 }

   370 \isamarkuptrue%

   371 %

   372 \begin{isamarkuptext}%

   373 Arbitrary operations on the background context may be wrapped-up as

   374   generic declaration elements.  Since the underlying concept of local

   375   theories may be subject to later re-interpretation, there is an

   376   additional dependency on a morphism that tells the difference of the

   377   original declaration context wrt.\ the application context

   378   encountered later on.  A fact declaration is an important special

   379   case: it consists of a theorem which is applied to the context by

   380   means of an attribute.

   382   \begin{matharray}{rcl}

   383     \indexdef{}{command}{declaration}\hypertarget{command.declaration}{\hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\

   384     \indexdef{}{command}{syntax\_declaration}\hypertarget{command.syntax-declaration}{\hyperlink{command.syntax-declaration}{\mbox{\isa{\isacommand{syntax{\isaliteral{5F}{\isacharunderscore}}declaration}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\

   385     \indexdef{}{command}{declare}\hypertarget{command.declare}{\hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\

   386   \end{matharray}

   388   \begin{railoutput}

   389 \rail@begin{5}{}

   390 \rail@bar

   391 \rail@term{\hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}}[]

   392 \rail@nextbar{1}

   393 \rail@term{\hyperlink{command.syntax-declaration}{\mbox{\isa{\isacommand{syntax{\isaliteral{5F}{\isacharunderscore}}declaration}}}}}[]

   394 \rail@endbar

   395 \rail@bar

   396 \rail@nextbar{1}

   397 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]

   398 \rail@term{\isa{\isakeyword{pervasive}}}[]

   399 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]

   400 \rail@endbar

   401 \rail@cr{3}

   402 \rail@bar

   403 \rail@nextbar{4}

   404 \rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]

   405 \rail@endbar

   406 \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]

   407 \rail@end

   408 \rail@begin{2}{}

   409 \rail@term{\hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}}}[]

   410 \rail@bar

   411 \rail@nextbar{1}

   412 \rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]

   413 \rail@endbar

   414 \rail@plus

   415 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]

   416 \rail@nextplus{1}

   417 \rail@cterm{\isa{\isakeyword{and}}}[]

   418 \rail@endplus

   419 \rail@end

   420 \end{railoutput}

   423   \begin{description}

   425   \item \hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}~\isa{d} adds the declaration

   426   function \isa{d} of ML type \verb|declaration|, to the current

   427   local theory under construction.  In later application contexts, the

   428   function is transformed according to the morphisms being involved in

   429   the interpretation hierarchy.

   431   If the \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}pervasive{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} option is given, the corresponding

   432   declaration is applied to all possible contexts involved, including

   433   the global background theory.

   435   \item \hyperlink{command.syntax-declaration}{\mbox{\isa{\isacommand{syntax{\isaliteral{5F}{\isacharunderscore}}declaration}}}} is similar to \hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}, but is meant to affect only ``syntactic'' tools by

   436   convention (such as notation and type-checking information).

   438   \item \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}}~\isa{thms} declares theorems to the

   439   current local theory context.  No theorem binding is involved here,

   440   unlike \hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}} or \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}} (cf.\

   441   \secref{sec:axms-thms}), so \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}} only has the effect

   442   of applying attributes as included in the theorem specification.

   444   \end{description}%

   445 \end{isamarkuptext}%

   446 \isamarkuptrue%

   447 %

   448 \isamarkupsection{Locales \label{sec:locale}%

   449 }

   450 \isamarkuptrue%

   451 %

   452 \begin{isamarkuptext}%

   453 Locales are parametric named local contexts, consisting of a list of

   454   declaration elements that are modeled after the Isar proof context

   455   commands (cf.\ \secref{sec:proof-context}).%

   456 \end{isamarkuptext}%

   457 \isamarkuptrue%

   458 %

   459 \isamarkupsubsection{Locale expressions \label{sec:locale-expr}%

   460 }

   461 \isamarkuptrue%

   462 %

   463 \begin{isamarkuptext}%

   464 A \emph{locale expression} denotes a structured context composed of

   465   instances of existing locales.  The context consists of a list of

   466   instances of declaration elements from the locales.  Two locale

   467   instances are equal if they are of the same locale and the

   468   parameters are instantiated with equivalent terms.  Declaration

   469   elements from equal instances are never repeated, thus avoiding

   470   duplicate declarations.

   472   \begin{railoutput}

   473 \rail@begin{3}{\indexdef{}{syntax}{locale\_expr}\hypertarget{syntax.locale-expr}{\hyperlink{syntax.locale-expr}{\mbox{\isa{locale{\isaliteral{5F}{\isacharunderscore}}expr}}}}}

   474 \rail@plus

   475 \rail@nont{\isa{instance}}[]

   476 \rail@nextplus{1}

   477 \rail@cterm{\isa{{\isaliteral{2B}{\isacharplus}}}}[]

   478 \rail@endplus

   479 \rail@bar

   480 \rail@nextbar{1}

   481 \rail@term{\isa{\isakeyword{for}}}[]

   482 \rail@plus

   483 \rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]

   484 \rail@nextplus{2}

   485 \rail@cterm{\isa{\isakeyword{and}}}[]

   486 \rail@endplus

   487 \rail@endbar

   488 \rail@end

   489 \rail@begin{2}{\isa{instance}}

   490 \rail@bar

   491 \rail@nextbar{1}

   492 \rail@nont{\isa{qualifier}}[]

   493 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]

   494 \rail@endbar

   495 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]

   496 \rail@bar

   497 \rail@nont{\isa{pos{\isaliteral{5F}{\isacharunderscore}}insts}}[]

   498 \rail@nextbar{1}

   499 \rail@nont{\isa{named{\isaliteral{5F}{\isacharunderscore}}insts}}[]

   500 \rail@endbar

   501 \rail@end

   502 \rail@begin{3}{\isa{qualifier}}

   503 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

   504 \rail@bar

   505 \rail@nextbar{1}

   506 \rail@bar

   507 \rail@term{\isa{{\isaliteral{3F}{\isacharquery}}}}[]

   508 \rail@nextbar{2}

   509 \rail@term{\isa{{\isaliteral{21}{\isacharbang}}}}[]

   510 \rail@endbar

   511 \rail@endbar

   512 \rail@end

   513 \rail@begin{3}{\isa{pos{\isaliteral{5F}{\isacharunderscore}}insts}}

   514 \rail@plus

   515 \rail@nextplus{1}

   516 \rail@bar

   517 \rail@term{\isa{{\isaliteral{5F}{\isacharunderscore}}}}[]

   518 \rail@nextbar{2}

   519 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]

   520 \rail@endbar

   521 \rail@endplus

   522 \rail@end

   523 \rail@begin{2}{\isa{named{\isaliteral{5F}{\isacharunderscore}}insts}}

   524 \rail@term{\isa{\isakeyword{where}}}[]

   525 \rail@plus

   526 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

   527 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]

   528 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]

   529 \rail@nextplus{1}

   530 \rail@cterm{\isa{\isakeyword{and}}}[]

   531 \rail@endplus

   532 \rail@end

   533 \end{railoutput}

   536   A locale instance consists of a reference to a locale and either

   537   positional or named parameter instantiations.  Identical

   538   instantiations (that is, those that instante a parameter by itself)

   539   may be omitted.  The notation `\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}}' enables to omit the

   540   instantiation for a parameter inside a positional instantiation.

   542   Terms in instantiations are from the context the locale expressions

   543   is declared in.  Local names may be added to this context with the

   544   optional for clause.  In addition, syntax declarations from one

   545   instance are effective when parsing subsequent instances of the same

   546   expression.

   548   Instances have an optional qualifier which applies to names in

   549   declarations.  Names include local definitions and theorem names.

   550   If present, the qualifier itself is either optional

   551   (``\texttt{?}''), which means that it may be omitted on input of the

   552   qualified name, or mandatory (``\texttt{!}'').  If neither

   553   ``\texttt{?}'' nor ``\texttt{!}'' are present, the command's default

   554   is used.  For \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}} and \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}

   555   the default is ``mandatory'', for \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}} and \hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}} the default is ``optional''.%

   556 \end{isamarkuptext}%

   557 \isamarkuptrue%

   558 %

   559 \isamarkupsubsection{Locale declarations%

   560 }

   561 \isamarkuptrue%

   562 %

   563 \begin{isamarkuptext}%

   564 \begin{matharray}{rcl}

   565     \indexdef{}{command}{locale}\hypertarget{command.locale}{\hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\

   566     \indexdef{}{command}{print\_locale}\hypertarget{command.print-locale}{\hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}locale}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\

   567     \indexdef{}{command}{print\_locales}\hypertarget{command.print-locales}{\hyperlink{command.print-locales}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}locales}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\

   568     \indexdef{}{method}{intro\_locales}\hypertarget{method.intro-locales}{\hyperlink{method.intro-locales}{\mbox{\isa{intro{\isaliteral{5F}{\isacharunderscore}}locales}}}} & : & \isa{method} \\

   569     \indexdef{}{method}{unfold\_locales}\hypertarget{method.unfold-locales}{\hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isaliteral{5F}{\isacharunderscore}}locales}}}} & : & \isa{method} \\

   570   \end{matharray}

   572   \indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes}

   573   \indexisarelem{defines}\indexisarelem{notes}

   574   \begin{railoutput}

   575 \rail@begin{2}{}

   576 \rail@term{\hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}}[]

   577 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

   578 \rail@bar

   579 \rail@nextbar{1}

   580 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]

   581 \rail@nont{\hyperlink{syntax.locale}{\mbox{\isa{locale}}}}[]

   582 \rail@endbar

   583 \rail@bar

   584 \rail@nextbar{1}

   585 \rail@term{\isa{\isakeyword{begin}}}[]

   586 \rail@endbar

   587 \rail@end

   588 \rail@begin{2}{}

   589 \rail@term{\hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}locale}}}}}[]

   590 \rail@bar

   591 \rail@nextbar{1}

   592 \rail@term{\isa{{\isaliteral{21}{\isacharbang}}}}[]

   593 \rail@endbar

   594 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]

   595 \rail@end

   596 \rail@begin{5}{\indexdef{}{syntax}{locale}\hypertarget{syntax.locale}{\hyperlink{syntax.locale}{\mbox{\isa{locale}}}}}

   597 \rail@bar

   598 \rail@plus

   599 \rail@nont{\hyperlink{syntax.context-elem}{\mbox{\isa{context{\isaliteral{5F}{\isacharunderscore}}elem}}}}[]

   600 \rail@nextplus{1}

   601 \rail@endplus

   602 \rail@nextbar{2}

   603 \rail@nont{\hyperlink{syntax.locale-expr}{\mbox{\isa{locale{\isaliteral{5F}{\isacharunderscore}}expr}}}}[]

   604 \rail@bar

   605 \rail@nextbar{3}

   606 \rail@term{\isa{{\isaliteral{2B}{\isacharplus}}}}[]

   607 \rail@plus

   608 \rail@nont{\hyperlink{syntax.context-elem}{\mbox{\isa{context{\isaliteral{5F}{\isacharunderscore}}elem}}}}[]

   609 \rail@nextplus{4}

   610 \rail@endplus

   611 \rail@endbar

   612 \rail@endbar

   613 \rail@end

   614 \rail@begin{12}{\indexdef{}{syntax}{context\_elem}\hypertarget{syntax.context-elem}{\hyperlink{syntax.context-elem}{\mbox{\isa{context{\isaliteral{5F}{\isacharunderscore}}elem}}}}}

   615 \rail@bar

   616 \rail@term{\isa{\isakeyword{fixes}}}[]

   617 \rail@plus

   618 \rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]

   619 \rail@nextplus{1}

   620 \rail@cterm{\isa{\isakeyword{and}}}[]

   621 \rail@endplus

   622 \rail@nextbar{2}

   623 \rail@term{\isa{\isakeyword{constrains}}}[]

   624 \rail@plus

   625 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

   626 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}}}[]

   627 \rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]

   628 \rail@nextplus{3}

   629 \rail@cterm{\isa{\isakeyword{and}}}[]

   630 \rail@endplus

   631 \rail@nextbar{4}

   632 \rail@term{\isa{\isakeyword{assumes}}}[]

   633 \rail@plus

   634 \rail@nont{\hyperlink{syntax.props}{\mbox{\isa{props}}}}[]

   635 \rail@nextplus{5}

   636 \rail@cterm{\isa{\isakeyword{and}}}[]

   637 \rail@endplus

   638 \rail@nextbar{6}

   639 \rail@term{\isa{\isakeyword{defines}}}[]

   640 \rail@plus

   641 \rail@bar

   642 \rail@nextbar{7}

   643 \rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]

   644 \rail@endbar

   645 \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]

   646 \rail@bar

   647 \rail@nextbar{7}

   648 \rail@nont{\hyperlink{syntax.proppat}{\mbox{\isa{proppat}}}}[]

   649 \rail@endbar

   650 \rail@nextplus{8}

   651 \rail@cterm{\isa{\isakeyword{and}}}[]

   652 \rail@endplus

   653 \rail@nextbar{9}

   654 \rail@term{\isa{\isakeyword{notes}}}[]

   655 \rail@plus

   656 \rail@bar

   657 \rail@nextbar{10}

   658 \rail@nont{\hyperlink{syntax.thmdef}{\mbox{\isa{thmdef}}}}[]

   659 \rail@endbar

   660 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]

   661 \rail@nextplus{11}

   662 \rail@cterm{\isa{\isakeyword{and}}}[]

   663 \rail@endplus

   664 \rail@endbar

   665 \rail@end

   666 \end{railoutput}

   669   \begin{description}

   671   \item \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}loc\ {\isaliteral{3D}{\isacharequal}}\ import\ {\isaliteral{2B}{\isacharplus}}\ body{\isaliteral{22}{\isachardoublequote}}} defines a

   672   new locale \isa{loc} as a context consisting of a certain view of

   673   existing locales (\isa{import}) plus some additional elements

   674   (\isa{body}).  Both \isa{import} and \isa{body} are optional;

   675   the degenerate form \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}~\isa{loc} defines an empty

   676   locale, which may still be useful to collect declarations of facts

   677   later on.  Type-inference on locale expressions automatically takes

   678   care of the most general typing that the combined context elements

   679   may acquire.

   681   The \isa{import} consists of a structured locale expression; see

   682   \secref{sec:proof-context} above.  Its for clause defines the local

   683   parameters of the \isa{import}.  In addition, locale parameters

   684   whose instantance is omitted automatically extend the (possibly

   685   empty) for clause: they are inserted at its beginning.  This means

   686   that these parameters may be referred to from within the expression

   687   and also in the subsequent context elements and provides a

   688   notational convenience for the inheritance of parameters in locale

   689   declarations.

   691   The \isa{body} consists of context elements.

   693   \begin{description}

   695   \item \hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\ {\isaliteral{28}{\isacharparenleft}}mx{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} declares a local

   696   parameter of type \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} and mixfix annotation \isa{mx} (both

   697   are optional).  The special syntax declaration ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C5354525543545552453E}{\isasymSTRUCTURE}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'' means that \isa{x} may be referenced

   698   implicitly in this context.

   700   \item \hyperlink{element.constrains}{\mbox{\isa{\isakeyword{constrains}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}} introduces a type

   701   constraint \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} on the local parameter \isa{x}.  This

   702   element is deprecated.  The type constraint should be introduced in

   703   the for clause or the relevant \hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}} element.

   705   \item \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}

   706   introduces local premises, similar to \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}} within a

   707   proof (cf.\ \secref{sec:proof-context}).

   709   \item \hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{3A}{\isacharcolon}}\ x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t{\isaliteral{22}{\isachardoublequote}}} defines a previously

   710   declared parameter.  This is similar to \hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}} within a

   711   proof (cf.\ \secref{sec:proof-context}), but \hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}}

   712   takes an equational proposition instead of variable-term pair.  The

   713   left-hand side of the equation may have additional arguments, e.g.\

   714   ``\hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}f\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t{\isaliteral{22}{\isachardoublequote}}}''.

   716   \item \hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\ {\isaliteral{3D}{\isacharequal}}\ b\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ b\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}

   717   reconsiders facts within a local context.  Most notably, this may

   718   include arbitrary declarations in any attribute specifications

   719   included here, e.g.\ a local \hyperlink{attribute.simp}{\mbox{\isa{simp}}} rule.

   721   The initial \isa{import} specification of a locale expression

   722   maintains a dynamic relation to the locales being referenced

   723   (benefiting from any later fact declarations in the obvious manner).

   725   \end{description}

   727   Note that ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C49533E}{\isasymIS}}\ p\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ p\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'' patterns given

   728   in the syntax of \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}} and \hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}} above

   729   are illegal in locale definitions.  In the long goal format of

   730   \secref{sec:goals}, term bindings may be included as expected,

   731   though.

   733   \medskip Locale specifications are ``closed up'' by

   734   turning the given text into a predicate definition \isa{loc{\isaliteral{5F}{\isacharunderscore}}axioms} and deriving the original assumptions as local lemmas

   735   (modulo local definitions).  The predicate statement covers only the

   736   newly specified assumptions, omitting the content of included locale

   737   expressions.  The full cumulative view is only provided on export,

   738   involving another predicate \isa{loc} that refers to the complete

   739   specification text.

   741   In any case, the predicate arguments are those locale parameters

   742   that actually occur in the respective piece of text.  Also note that

   743   these predicates operate at the meta-level in theory, but the locale

   744   packages attempts to internalize statements according to the

   745   object-logic setup (e.g.\ replacing \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}} by \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}}, and

   746   \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{22}{\isachardoublequote}}} by \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}{\isaliteral{22}{\isachardoublequote}}} in HOL; see also

   747   \secref{sec:object-logic}).  Separate introduction rules \isa{loc{\isaliteral{5F}{\isacharunderscore}}axioms{\isaliteral{2E}{\isachardot}}intro} and \isa{loc{\isaliteral{2E}{\isachardot}}intro} are provided as well.

   749   \item \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}locale}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}locale{\isaliteral{22}{\isachardoublequote}}} prints the

   750   contents of the named locale.  The command omits \hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}}

   751   elements by default.  Use \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}locale}}}}\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{21}{\isacharbang}}{\isaliteral{22}{\isachardoublequote}}} to

   752   have them included.

   754   \item \hyperlink{command.print-locales}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}locales}}}} prints the names of all locales

   755   of the current theory.

   757   \item \hyperlink{method.intro-locales}{\mbox{\isa{intro{\isaliteral{5F}{\isacharunderscore}}locales}}} and \hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isaliteral{5F}{\isacharunderscore}}locales}}}

   758   repeatedly expand all introduction rules of locale predicates of the

   759   theory.  While \hyperlink{method.intro-locales}{\mbox{\isa{intro{\isaliteral{5F}{\isacharunderscore}}locales}}} only applies the \isa{loc{\isaliteral{2E}{\isachardot}}intro} introduction rules and therefore does not decend to

   760   assumptions, \hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isaliteral{5F}{\isacharunderscore}}locales}}} is more aggressive and applies

   761   \isa{loc{\isaliteral{5F}{\isacharunderscore}}axioms{\isaliteral{2E}{\isachardot}}intro} as well.  Both methods are aware of locale

   762   specifications entailed by the context, both from target statements,

   763   and from interpretations (see below).  New goals that are entailed

   764   by the current context are discharged automatically.

   766   \end{description}%

   767 \end{isamarkuptext}%

   768 \isamarkuptrue%

   769 %

   770 \isamarkupsubsection{Locale interpretations%

   771 }

   772 \isamarkuptrue%

   773 %

   774 \begin{isamarkuptext}%

   775 Locale expressions may be instantiated, and the instantiated facts

   776   added to the current context.  This requires a proof of the

   777   instantiated specification and is called \emph{locale

   778   interpretation}.  Interpretation is possible in locales \hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}}, theories (command \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}) and

   779   also within a proof body (command \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}).

   781   \begin{matharray}{rcl}

   782     \indexdef{}{command}{interpretation}\hypertarget{command.interpretation}{\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\

   783     \indexdef{}{command}{interpret}\hypertarget{command.interpret}{\hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7C}{\isacharbar}}\ proof{\isaliteral{28}{\isacharparenleft}}chain{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\

   784     \indexdef{}{command}{sublocale}\hypertarget{command.sublocale}{\hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\

   785     \indexdef{}{command}{print\_dependencies}\hypertarget{command.print-dependencies}{\hyperlink{command.print-dependencies}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}dependencies}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\

   786     \indexdef{}{command}{print\_interps}\hypertarget{command.print-interps}{\hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}interps}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\

   787   \end{matharray}

   789   \begin{railoutput}

   790 \rail@begin{2}{}

   791 \rail@term{\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}}[]

   792 \rail@nont{\hyperlink{syntax.locale-expr}{\mbox{\isa{locale{\isaliteral{5F}{\isacharunderscore}}expr}}}}[]

   793 \rail@bar

   794 \rail@nextbar{1}

   795 \rail@nont{\isa{equations}}[]

   796 \rail@endbar

   797 \rail@end

   798 \rail@begin{2}{}

   799 \rail@term{\hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}}[]

   800 \rail@nont{\hyperlink{syntax.locale-expr}{\mbox{\isa{locale{\isaliteral{5F}{\isacharunderscore}}expr}}}}[]

   801 \rail@bar

   802 \rail@nextbar{1}

   803 \rail@nont{\isa{equations}}[]

   804 \rail@endbar

   805 \rail@end

   806 \rail@begin{5}{}

   807 \rail@term{\hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}}}[]

   808 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]

   809 \rail@bar

   810 \rail@term{\isa{{\isaliteral{3C}{\isacharless}}}}[]

   811 \rail@nextbar{1}

   812 \rail@term{\isa{{\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}}}[]

   813 \rail@endbar

   814 \rail@nont{\hyperlink{syntax.locale-expr}{\mbox{\isa{locale{\isaliteral{5F}{\isacharunderscore}}expr}}}}[]

   815 \rail@cr{3}

   816 \rail@bar

   817 \rail@nextbar{4}

   818 \rail@nont{\isa{equations}}[]

   819 \rail@endbar

   820 \rail@end

   821 \rail@begin{2}{}

   822 \rail@term{\hyperlink{command.print-dependencies}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}dependencies}}}}}[]

   823 \rail@bar

   824 \rail@nextbar{1}

   825 \rail@term{\isa{{\isaliteral{21}{\isacharbang}}}}[]

   826 \rail@endbar

   827 \rail@nont{\hyperlink{syntax.locale-expr}{\mbox{\isa{locale{\isaliteral{5F}{\isacharunderscore}}expr}}}}[]

   828 \rail@end

   829 \rail@begin{1}{}

   830 \rail@term{\hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}interps}}}}}[]

   831 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]

   832 \rail@end

   833 \rail@begin{3}{\isa{equations}}

   834 \rail@term{\isa{\isakeyword{where}}}[]

   835 \rail@plus

   836 \rail@bar

   837 \rail@nextbar{1}

   838 \rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]

   839 \rail@endbar

   840 \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]

   841 \rail@nextplus{2}

   842 \rail@cterm{\isa{\isakeyword{and}}}[]

   843 \rail@endplus

   844 \rail@end

   845 \end{railoutput}

   848   \begin{description}

   850   \item \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}expr\ {\isaliteral{5C3C57484552453E}{\isasymWHERE}}\ eqns{\isaliteral{22}{\isachardoublequote}}}

   851   interprets \isa{expr} in the theory.  The command generates proof

   852   obligations for the instantiated specifications (assumes and defines

   853   elements).  Once these are discharged by the user, instantiated

   854   facts are added to the theory in a post-processing phase.

   856   Additional equations, which are unfolded during

   857   post-processing, may be given after the keyword \hyperlink{keyword.where}{\mbox{\isa{\isakeyword{where}}}}.

   858   This is useful for interpreting concepts introduced through

   859   definitions.  The equations must be proved.

   861   The command is aware of interpretations already active in the

   862   theory, but does not simplify the goal automatically.  In order to

   863   simplify the proof obligations use methods \hyperlink{method.intro-locales}{\mbox{\isa{intro{\isaliteral{5F}{\isacharunderscore}}locales}}}

   864   or \hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isaliteral{5F}{\isacharunderscore}}locales}}}.  Post-processing is not applied to

   865   facts of interpretations that are already active.  This avoids

   866   duplication of interpreted facts, in particular.  Note that, in the

   867   case of a locale with import, parts of the interpretation may

   868   already be active.  The command will only process facts for new

   869   parts.

   871   Adding facts to locales has the effect of adding interpreted facts

   872   to the theory for all interpretations as well.  That is,

   873   interpretations dynamically participate in any facts added to

   874   locales.  Note that if a theory inherits additional facts for a

   875   locale through one parent and an interpretation of that locale

   876   through another parent, the additional facts will not be

   877   interpreted.

   879   \item \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}expr\ {\isaliteral{5C3C57484552453E}{\isasymWHERE}}\ eqns{\isaliteral{22}{\isachardoublequote}}} interprets

   880   \isa{expr} in the proof context and is otherwise similar to

   881   interpretation in theories.  Note that rewrite rules given to

   882   \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}} after the \hyperlink{keyword.where}{\mbox{\isa{\isakeyword{where}}}} keyword should be

   883   explicitly universally quantified.

   885   \item \hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}name\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ expr\ {\isaliteral{5C3C57484552453E}{\isasymWHERE}}\ eqns{\isaliteral{22}{\isachardoublequote}}}

   886   interprets \isa{expr} in the locale \isa{name}.  A proof that

   887   the specification of \isa{name} implies the specification of

   888   \isa{expr} is required.  As in the localized version of the

   889   theorem command, the proof is in the context of \isa{name}.  After

   890   the proof obligation has been discharged, the facts of \isa{expr}

   891   become part of locale \isa{name} as \emph{derived} context

   892   elements and are available when the context \isa{name} is

   893   subsequently entered.  Note that, like import, this is dynamic:

   894   facts added to a locale part of \isa{expr} after interpretation

   895   become also available in \isa{name}.

   897   Only specification fragments of \isa{expr} that are not already

   898   part of \isa{name} (be it imported, derived or a derived fragment

   899   of the import) are considered in this process.  This enables

   900   circular interpretations provided that no infinite chains are

   901   generated in the locale hierarchy.

   903   If interpretations of \isa{name} exist in the current theory, the

   904   command adds interpretations for \isa{expr} as well, with the same

   905   qualifier, although only for fragments of \isa{expr} that are not

   906   interpreted in the theory already.

   908   Equations given after \hyperlink{keyword.where}{\mbox{\isa{\isakeyword{where}}}} amend the morphism through

   909   which \isa{expr} is interpreted.  This enables to map definitions

   910   from the interpreted locales to entities of \isa{name}.  This

   911   feature is experimental.

   913   \item \hyperlink{command.print-dependencies}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}dependencies}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}expr{\isaliteral{22}{\isachardoublequote}}} is useful for

   914   understanding the effect of an interpretation of \isa{{\isaliteral{22}{\isachardoublequote}}expr{\isaliteral{22}{\isachardoublequote}}}.  It

   915   lists all locale instances for which interpretations would be added

   916   to the current context.  Variant \hyperlink{command.print-dependencies}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}dependencies}}}}\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{21}{\isacharbang}}{\isaliteral{22}{\isachardoublequote}}} prints all locale instances that

   917   would be considered for interpretation, and would be interpreted in

   918   an empty context (that is, without interpretations).

   920   \item \hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}interps}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}locale{\isaliteral{22}{\isachardoublequote}}} lists all

   921   interpretations of \isa{{\isaliteral{22}{\isachardoublequote}}locale{\isaliteral{22}{\isachardoublequote}}} in the current theory or proof

   922   context, including those due to a combination of a \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}} or \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}} and one or several

   923   \hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}} declarations.

   925   \end{description}

   927   \begin{warn}

   928     Since attributes are applied to interpreted theorems,

   929     interpretation may modify the context of common proof tools, e.g.\

   930     the Simplifier or Classical Reasoner.  As the behavior of such

   931     tools is \emph{not} stable under interpretation morphisms, manual

   932     declarations might have to be added to the target context of the

   933     interpretation to revert such declarations.

   934   \end{warn}

   936   \begin{warn}

   937     An interpretation in a theory or proof context may subsume previous

   938     interpretations.  This happens if the same specification fragment

   939     is interpreted twice and the instantiation of the second

   940     interpretation is more general than the interpretation of the

   941     first.  The locale package does not attempt to remove subsumed

   942     interpretations.

   943   \end{warn}%

   944 \end{isamarkuptext}%

   945 \isamarkuptrue%

   946 %

   947 \isamarkupsection{Classes \label{sec:class}%

   948 }

   949 \isamarkuptrue%

   950 %

   951 \begin{isamarkuptext}%

   952 A class is a particular locale with \emph{exactly one} type variable

   953   \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}}.  Beyond the underlying locale, a corresponding type class

   954   is established which is interpreted logically as axiomatic type

   955   class \cite{Wenzel:1997:TPHOL} whose logical content are the

   956   assumptions of the locale.  Thus, classes provide the full

   957   generality of locales combined with the commodity of type classes

   958   (notably type-inference).  See \cite{isabelle-classes} for a short

   959   tutorial.

   961   \begin{matharray}{rcl}

   962     \indexdef{}{command}{class}\hypertarget{command.class}{\hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\

   963     \indexdef{}{command}{instantiation}\hypertarget{command.instantiation}{\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\

   964     \indexdef{}{command}{instance}\hypertarget{command.instance}{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\

   965     \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\

   966     \indexdef{}{command}{subclass}\hypertarget{command.subclass}{\hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\

   967     \indexdef{}{command}{print\_classes}\hypertarget{command.print-classes}{\hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}classes}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\

   968     \indexdef{}{command}{class\_deps}\hypertarget{command.class-deps}{\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isaliteral{5F}{\isacharunderscore}}deps}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\

   969     \indexdef{}{method}{intro\_classes}\hypertarget{method.intro-classes}{\hyperlink{method.intro-classes}{\mbox{\isa{intro{\isaliteral{5F}{\isacharunderscore}}classes}}}} & : & \isa{method} \\

   970   \end{matharray}

   972   \begin{railoutput}

   973 \rail@begin{2}{}

   974 \rail@term{\hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}}[]

   975 \rail@nont{\isa{class{\isaliteral{5F}{\isacharunderscore}}spec}}[]

   976 \rail@bar

   977 \rail@nextbar{1}

   978 \rail@term{\isa{\isakeyword{begin}}}[]

   979 \rail@endbar

   980 \rail@end

   981 \rail@begin{5}{\isa{class{\isaliteral{5F}{\isacharunderscore}}spec}}

   982 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

   983 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]

   984 \rail@bar

   985 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]

   986 \rail@term{\isa{{\isaliteral{2B}{\isacharplus}}}}[]

   987 \rail@plus

   988 \rail@nont{\hyperlink{syntax.context-elem}{\mbox{\isa{context{\isaliteral{5F}{\isacharunderscore}}elem}}}}[]

   989 \rail@nextplus{1}

   990 \rail@endplus

   991 \rail@nextbar{2}

   992 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]

   993 \rail@nextbar{3}

   994 \rail@plus

   995 \rail@nont{\hyperlink{syntax.context-elem}{\mbox{\isa{context{\isaliteral{5F}{\isacharunderscore}}elem}}}}[]

   996 \rail@nextplus{4}

   997 \rail@endplus

   998 \rail@endbar

   999 \rail@end

  1000 \rail@begin{2}{}

  1001 \rail@term{\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}}[]

  1002 \rail@plus

  1003 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]

  1004 \rail@nextplus{1}

  1005 \rail@cterm{\isa{\isakeyword{and}}}[]

  1006 \rail@endplus

  1007 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}}}[]

  1008 \rail@nont{\hyperlink{syntax.arity}{\mbox{\isa{arity}}}}[]

  1009 \rail@term{\isa{\isakeyword{begin}}}[]

  1010 \rail@end

  1011 \rail@begin{5}{}

  1012 \rail@term{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}}[]

  1013 \rail@bar

  1014 \rail@nextbar{1}

  1015 \rail@plus

  1016 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]

  1017 \rail@nextplus{2}

  1018 \rail@cterm{\isa{\isakeyword{and}}}[]

  1019 \rail@endplus

  1020 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}}}[]

  1021 \rail@nont{\hyperlink{syntax.arity}{\mbox{\isa{arity}}}}[]

  1022 \rail@nextbar{3}

  1023 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]

  1024 \rail@bar

  1025 \rail@term{\isa{{\isaliteral{3C}{\isacharless}}}}[]

  1026 \rail@nextbar{4}

  1027 \rail@term{\isa{{\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}}}[]

  1028 \rail@endbar

  1029 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]

  1030 \rail@endbar

  1031 \rail@end

  1032 \rail@begin{2}{}

  1033 \rail@term{\hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}}[]

  1034 \rail@bar

  1035 \rail@nextbar{1}

  1036 \rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]

  1037 \rail@endbar

  1038 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]

  1039 \rail@end

  1040 \end{railoutput}

  1043   \begin{description}

  1045   \item \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{3D}{\isacharequal}}\ superclasses\ {\isaliteral{2B}{\isacharplus}}\ body{\isaliteral{22}{\isachardoublequote}}} defines

  1046   a new class \isa{c}, inheriting from \isa{superclasses}.  This

  1047   introduces a locale \isa{c} with import of all locales \isa{superclasses}.

  1049   Any \hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}} in \isa{body} are lifted to the global

  1050   theory level (\emph{class operations} \isa{{\isaliteral{22}{\isachardoublequote}}f\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ f\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} of class \isa{c}), mapping the local type parameter

  1051   \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}} to a schematic type variable \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ c{\isaliteral{22}{\isachardoublequote}}}.

  1053   Likewise, \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}} in \isa{body} are also lifted,

  1054   mapping each local parameter \isa{{\isaliteral{22}{\isachardoublequote}}f\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} to its

  1055   corresponding global constant \isa{{\isaliteral{22}{\isachardoublequote}}f\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ c{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}}.  The

  1056   corresponding introduction rule is provided as \isa{c{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{5F}{\isacharunderscore}}axioms{\isaliteral{2E}{\isachardot}}intro}.  This rule should be rarely needed directly

  1057   --- the \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isaliteral{5F}{\isacharunderscore}}classes}}} method takes care of the details of

  1058   class membership proofs.

  1060   \item \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}t\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}s\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ s\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}s\ {\isaliteral{5C3C424547494E3E}{\isasymBEGIN}}{\isaliteral{22}{\isachardoublequote}}} opens a theory target (cf.\ \secref{sec:target}) which

  1061   allows to specify class operations \isa{{\isaliteral{22}{\isachardoublequote}}f\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ f\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} corresponding

  1062   to sort \isa{s} at the particular type instance \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ s\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ s\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}}.  A plain \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} command in the

  1063   target body poses a goal stating these type arities.  The target is

  1064   concluded by an \indexref{local}{command}{end}\hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}} command.

  1066   Note that a list of simultaneous type constructors may be given;

  1067   this corresponds nicely to mutually recursive type definitions, e.g.\

  1068   in Isabelle/HOL.

  1070   \item \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} in an instantiation target body sets

  1071   up a goal stating the type arities claimed at the opening \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}.  The proof would usually proceed by \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isaliteral{5F}{\isacharunderscore}}classes}}}, and then establish the characteristic theorems of

  1072   the type classes involved.  After finishing the proof, the

  1073   background theory will be augmented by the proven type arities.

  1075   On the theory level, \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}t\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}s\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ s\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}s{\isaliteral{22}{\isachardoublequote}}} provides a convenient way to instantiate a type class with no

  1076   need to specify operations: one can continue with the

  1077   instantiation proof immediately.

  1079   \item \hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}~\isa{c} in a class context for class

  1080   \isa{d} sets up a goal stating that class \isa{c} is logically

  1081   contained in class \isa{d}.  After finishing the proof, class

  1082   \isa{d} is proven to be subclass \isa{c} and the locale \isa{c} is interpreted into \isa{d} simultaneously.

  1084   A weakend form of this is available through a further variant of

  1085   \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}:  \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}} opens

  1086   a proof that class \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}} implies \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}} without reference

  1087   to the underlying locales;  this is useful if the properties to prove

  1088   the logical connection are not sufficent on the locale level but on

  1089   the theory level.

  1091   \item \hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}classes}}}} prints all classes in the current

  1092   theory.

  1094   \item \hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isaliteral{5F}{\isacharunderscore}}deps}}}} visualizes all classes and their

  1095   subclass relations as a Hasse diagram.

  1097   \item \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isaliteral{5F}{\isacharunderscore}}classes}}} repeatedly expands all class

  1098   introduction rules of this theory.  Note that this method usually

  1099   needs not be named explicitly, as it is already included in the

  1100   default proof step (e.g.\ of \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}).  In particular,

  1101   instantiation of trivial (syntactic) classes may be performed by a

  1102   single ``\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}}}}'' proof step.

  1104   \end{description}%

  1105 \end{isamarkuptext}%

  1106 \isamarkuptrue%

  1107 %

  1108 \isamarkupsubsection{The class target%

  1109 }

  1110 \isamarkuptrue%

  1111 %

  1112 \begin{isamarkuptext}%

  1113 %FIXME check

  1115   A named context may refer to a locale (cf.\ \secref{sec:target}).

  1116   If this locale is also a class \isa{c}, apart from the common

  1117   locale target behaviour the following happens.

  1119   \begin{itemize}

  1121   \item Local constant declarations \isa{{\isaliteral{22}{\isachardoublequote}}g{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} referring to the

  1122   local type parameter \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}} and local parameters \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}}

  1123   are accompanied by theory-level constants \isa{{\isaliteral{22}{\isachardoublequote}}g{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ c{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}}

  1124   referring to theory-level class operations \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ c{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}}.

  1126   \item Local theorem bindings are lifted as are assumptions.

  1128   \item Local syntax refers to local operations \isa{{\isaliteral{22}{\isachardoublequote}}g{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} and

  1129   global operations \isa{{\isaliteral{22}{\isachardoublequote}}g{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ c{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} uniformly.  Type inference

  1130   resolves ambiguities.  In rare cases, manual type annotations are

  1131   needed.

  1133   \end{itemize}%

  1134 \end{isamarkuptext}%

  1135 \isamarkuptrue%

  1136 %

  1137 \isamarkupsubsection{Co-regularity of type classes and arities%

  1138 }

  1139 \isamarkuptrue%

  1140 %

  1141 \begin{isamarkuptext}%

  1142 The class relation together with the collection of

  1143   type-constructor arities must obey the principle of

  1144   \emph{co-regularity} as defined below.

  1146   \medskip For the subsequent formulation of co-regularity we assume

  1147   that the class relation is closed by transitivity and reflexivity.

  1148   Moreover the collection of arities \isa{{\isaliteral{22}{\isachardoublequote}}t\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec s{\isaliteral{29}{\isacharparenright}}c{\isaliteral{22}{\isachardoublequote}}} is

  1149   completed such that \isa{{\isaliteral{22}{\isachardoublequote}}t\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec s{\isaliteral{29}{\isacharparenright}}c{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ c{\isaliteral{27}{\isacharprime}}{\isaliteral{22}{\isachardoublequote}}}

  1150   implies \isa{{\isaliteral{22}{\isachardoublequote}}t\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec s{\isaliteral{29}{\isacharparenright}}c{\isaliteral{27}{\isacharprime}}{\isaliteral{22}{\isachardoublequote}}} for all such declarations.

  1152   Treating sorts as finite sets of classes (meaning the intersection),

  1153   the class relation \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}} is extended to sorts as

  1154   follows:

  1155   \[

  1156     \isa{{\isaliteral{22}{\isachardoublequote}}s\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ s\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ s\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ s\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}}

  1157   \]

  1159   This relation on sorts is further extended to tuples of sorts (of

  1160   the same length) in the component-wise way.

  1162   \smallskip Co-regularity of the class relation together with the

  1163   arities relation means:

  1164   \[

  1165     \isa{{\isaliteral{22}{\isachardoublequote}}t\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec s\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ t\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec s\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec s\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec s\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}}

  1166   \]

  1167   \noindent for all such arities.  In other words, whenever the result

  1168   classes of some type-constructor arities are related, then the

  1169   argument sorts need to be related in the same way.

  1171   \medskip Co-regularity is a very fundamental property of the

  1172   order-sorted algebra of types.  For example, it entails principle

  1173   types and most general unifiers, e.g.\ see \cite{nipkow-prehofer}.%

  1174 \end{isamarkuptext}%

  1175 \isamarkuptrue%

  1176 %

  1177 \isamarkupsection{Unrestricted overloading%

  1178 }

  1179 \isamarkuptrue%

  1180 %

  1181 \begin{isamarkuptext}%

  1182 Isabelle/Pure's definitional schemes support certain forms of

  1183   overloading (see \secref{sec:consts}).  Overloading means that a

  1184   constant being declared as \isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ decl{\isaliteral{22}{\isachardoublequote}}} may be

  1185   defined separately on type instances

  1186   \isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}\ t\ decl{\isaliteral{22}{\isachardoublequote}}}

  1187   for each type constructor \isa{t}.  At most occassions

  1188   overloading will be used in a Haskell-like fashion together with

  1189   type classes by means of \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} (see

  1190   \secref{sec:class}).  Sometimes low-level overloading is desirable.

  1191   The \hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}} target provides a convenient view for

  1192   end-users.

  1194   \begin{matharray}{rcl}

  1195     \indexdef{}{command}{overloading}\hypertarget{command.overloading}{\hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\

  1196   \end{matharray}

  1198   \begin{railoutput}

  1199 \rail@begin{2}{}

  1200 \rail@term{\hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}}}[]

  1201 \rail@plus

  1202 \rail@nont{\isa{spec}}[]

  1203 \rail@nextplus{1}

  1204 \rail@endplus

  1205 \rail@term{\isa{\isakeyword{begin}}}[]

  1206 \rail@end

  1207 \rail@begin{2}{\isa{spec}}

  1208 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

  1209 \rail@bar

  1210 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}}}[]

  1211 \rail@nextbar{1}

  1212 \rail@term{\isa{{\isaliteral{5C3C65717569763E}{\isasymequiv}}}}[]

  1213 \rail@endbar

  1214 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]

  1215 \rail@bar

  1216 \rail@nextbar{1}

  1217 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]

  1218 \rail@term{\isa{\isakeyword{unchecked}}}[]

  1219 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]

  1220 \rail@endbar

  1221 \rail@end

  1222 \end{railoutput}

  1225   \begin{description}

  1227   \item \hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C414E443E}{\isasymAND}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C424547494E3E}{\isasymBEGIN}}{\isaliteral{22}{\isachardoublequote}}}

  1228   opens a theory target (cf.\ \secref{sec:target}) which allows to

  1229   specify constants with overloaded definitions.  These are identified

  1230   by an explicitly given mapping from variable names \isa{{\isaliteral{22}{\isachardoublequote}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} to

  1231   constants \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} at particular type instances.  The

  1232   definitions themselves are established using common specification

  1233   tools, using the names \isa{{\isaliteral{22}{\isachardoublequote}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} as reference to the

  1234   corresponding constants.  The target is concluded by \hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}}.

  1236   A \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}unchecked{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} option disables global dependency checks for

  1237   the corresponding definition, which is occasionally useful for

  1238   exotic overloading (see \secref{sec:consts} for a precise description).

  1239   It is at the discretion of the user to avoid

  1240   malformed theory specifications!

  1242   \end{description}%

  1243 \end{isamarkuptext}%

  1244 \isamarkuptrue%

  1245 %

  1246 \isamarkupsection{Incorporating ML code \label{sec:ML}%

  1247 }

  1248 \isamarkuptrue%

  1249 %

  1250 \begin{isamarkuptext}%

  1251 \begin{matharray}{rcl}

  1252     \indexdef{}{command}{use}\hypertarget{command.use}{\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\

  1253     \indexdef{}{command}{ML}\hypertarget{command.ML}{\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\

  1254     \indexdef{}{command}{ML\_prf}\hypertarget{command.ML-prf}{\hyperlink{command.ML-prf}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}prf}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{22}{\isachardoublequote}}} \\

  1255     \indexdef{}{command}{ML\_val}\hypertarget{command.ML-val}{\hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}val}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}any\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\

  1256     \indexdef{}{command}{ML\_command}\hypertarget{command.ML-command}{\hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}command}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}any\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\

  1257     \indexdef{}{command}{setup}\hypertarget{command.setup}{\hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\

  1258     \indexdef{}{command}{local\_setup}\hypertarget{command.local-setup}{\hyperlink{command.local-setup}{\mbox{\isa{\isacommand{local{\isaliteral{5F}{\isacharunderscore}}setup}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\

  1259     \indexdef{}{command}{attribute\_setup}\hypertarget{command.attribute-setup}{\hyperlink{command.attribute-setup}{\mbox{\isa{\isacommand{attribute{\isaliteral{5F}{\isacharunderscore}}setup}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\

  1260   \end{matharray}

  1262   \begin{railoutput}

  1263 \rail@begin{1}{}

  1264 \rail@term{\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}}[]

  1265 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

  1266 \rail@end

  1267 \rail@begin{6}{}

  1268 \rail@bar

  1269 \rail@term{\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}}[]

  1270 \rail@nextbar{1}

  1271 \rail@term{\hyperlink{command.ML-prf}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}prf}}}}}[]

  1272 \rail@nextbar{2}

  1273 \rail@term{\hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}val}}}}}[]

  1274 \rail@nextbar{3}

  1275 \rail@term{\hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}command}}}}}[]

  1276 \rail@nextbar{4}

  1277 \rail@term{\hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}}[]

  1278 \rail@nextbar{5}

  1279 \rail@term{\hyperlink{command.local-setup}{\mbox{\isa{\isacommand{local{\isaliteral{5F}{\isacharunderscore}}setup}}}}}[]

  1280 \rail@endbar

  1281 \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]

  1282 \rail@end

  1283 \rail@begin{1}{}

  1284 \rail@term{\hyperlink{command.attribute-setup}{\mbox{\isa{\isacommand{attribute{\isaliteral{5F}{\isacharunderscore}}setup}}}}}[]

  1285 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

  1286 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]

  1287 \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]

  1288 \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]

  1289 \rail@end

  1290 \end{railoutput}

  1293   \begin{description}

  1295   \item \hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}file{\isaliteral{22}{\isachardoublequote}}} reads and executes ML

  1296   commands from \isa{{\isaliteral{22}{\isachardoublequote}}file{\isaliteral{22}{\isachardoublequote}}}.  The current theory context is passed

  1297   down to the ML toplevel and may be modified, using \verb|Context.>>| or derived ML commands.  The file name is checked with

  1298   the \indexref{}{keyword}{uses}\hyperlink{keyword.uses}{\mbox{\isa{\isakeyword{uses}}}} dependency declaration given in the theory

  1299   header (see also \secref{sec:begin-thy}).

  1301   Top-level ML bindings are stored within the (global or local) theory

  1302   context.

  1304   \item \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}text{\isaliteral{22}{\isachardoublequote}}} is similar to \hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}},

  1305   but executes ML commands directly from the given \isa{{\isaliteral{22}{\isachardoublequote}}text{\isaliteral{22}{\isachardoublequote}}}.

  1306   Top-level ML bindings are stored within the (global or local) theory

  1307   context.

  1309   \item \hyperlink{command.ML-prf}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}prf}}}} is analogous to \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}} but works

  1310   within a proof context.

  1312   Top-level ML bindings are stored within the proof context in a

  1313   purely sequential fashion, disregarding the nested proof structure.

  1314   ML bindings introduced by \hyperlink{command.ML-prf}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}prf}}}} are discarded at the

  1315   end of the proof.

  1317   \item \hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}val}}}} and \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}command}}}} are diagnostic

  1318   versions of \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}, which means that the context may not be

  1319   updated.  \hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}val}}}} echos the bindings produced at the ML

  1320   toplevel, but \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}command}}}} is silent.

  1322   \item \hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}text{\isaliteral{22}{\isachardoublequote}}} changes the current theory

  1323   context by applying \isa{{\isaliteral{22}{\isachardoublequote}}text{\isaliteral{22}{\isachardoublequote}}}, which refers to an ML expression

  1324   of type \verb|theory -> theory|.  This enables to initialize

  1325   any object-logic specific tools and packages written in ML, for

  1326   example.

  1328   \item \hyperlink{command.local-setup}{\mbox{\isa{\isacommand{local{\isaliteral{5F}{\isacharunderscore}}setup}}}} is similar to \hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}} for

  1329   a local theory context, and an ML expression of type \verb|local_theory -> local_theory|.  This allows to

  1330   invoke local theory specification packages without going through

  1331   concrete outer syntax, for example.

  1333   \item \hyperlink{command.attribute-setup}{\mbox{\isa{\isacommand{attribute{\isaliteral{5F}{\isacharunderscore}}setup}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}name\ {\isaliteral{3D}{\isacharequal}}\ text\ description{\isaliteral{22}{\isachardoublequote}}}

  1334   defines an attribute in the current theory.  The given \isa{{\isaliteral{22}{\isachardoublequote}}text{\isaliteral{22}{\isachardoublequote}}} has to be an ML expression of type

  1335   \verb|attribute context_parser|, cf.\ basic parsers defined in

  1336   structure \verb|Args| and \verb|Attrib|.

  1338   In principle, attributes can operate both on a given theorem and the

  1339   implicit context, although in practice only one is modified and the

  1340   other serves as parameter.  Here are examples for these two cases:

  1342   \end{description}%

  1343 \end{isamarkuptext}%

  1344 \isamarkuptrue%

  1345 %

  1346 \isadelimML

  1347 \ \ %

  1348 \endisadelimML

  1349 %

  1350 \isatagML

  1351 \isacommand{attribute{\isaliteral{5F}{\isacharunderscore}}setup}\isamarkupfalse%

  1352 \ my{\isaliteral{5F}{\isacharunderscore}}rule\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline

  1353 \ \ \ \ Attrib{\isaliteral{2E}{\isachardot}}thms\ {\isaliteral{3E}{\isachargreater}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}fn\ ths\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\isanewline

  1354 \ \ \ \ \ \ Thm{\isaliteral{2E}{\isachardot}}rule{\isaliteral{5F}{\isacharunderscore}}attribute\isanewline

  1355 \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}fn\ context{\isaliteral{3A}{\isacharcolon}}\ Context{\isaliteral{2E}{\isachardot}}generic\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ fn\ th{\isaliteral{3A}{\isacharcolon}}\ thm\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\isanewline

  1356 \ \ \ \ \ \ \ \ \ \ let\ val\ th{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ th\ OF\ ths\isanewline

  1357 \ \ \ \ \ \ \ \ \ \ in\ th{\isaliteral{27}{\isacharprime}}\ end{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}my\ rule{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

  1358 \isanewline

  1359 \ \ \isacommand{attribute{\isaliteral{5F}{\isacharunderscore}}setup}\isamarkupfalse%

  1360 \ my{\isaliteral{5F}{\isacharunderscore}}declaration\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline

  1361 \ \ \ \ Attrib{\isaliteral{2E}{\isachardot}}thms\ {\isaliteral{3E}{\isachargreater}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}fn\ ths\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\isanewline

  1362 \ \ \ \ \ \ Thm{\isaliteral{2E}{\isachardot}}declaration{\isaliteral{5F}{\isacharunderscore}}attribute\isanewline

  1363 \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}fn\ th{\isaliteral{3A}{\isacharcolon}}\ thm\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ fn\ context{\isaliteral{3A}{\isacharcolon}}\ Context{\isaliteral{2E}{\isachardot}}generic\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\isanewline

  1364 \ \ \ \ \ \ \ \ \ \ let\ val\ context{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ context\isanewline

  1365 \ \ \ \ \ \ \ \ \ \ in\ context{\isaliteral{27}{\isacharprime}}\ end{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}my\ declaration{\isaliteral{22}{\isachardoublequoteclose}}%

  1366 \endisatagML

  1367 {\isafoldML}%

  1368 %

  1369 \isadelimML

  1370 %

  1371 \endisadelimML

  1372 %

  1373 \isamarkupsection{Primitive specification elements%

  1374 }

  1375 \isamarkuptrue%

  1376 %

  1377 \isamarkupsubsection{Type classes and sorts \label{sec:classes}%

  1378 }

  1379 \isamarkuptrue%

  1380 %

  1381 \begin{isamarkuptext}%

  1382 \begin{matharray}{rcll}

  1383     \indexdef{}{command}{classes}\hypertarget{command.classes}{\hyperlink{command.classes}{\mbox{\isa{\isacommand{classes}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\

  1384     \indexdef{}{command}{classrel}\hypertarget{command.classrel}{\hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} & (axiomatic!) \\

  1385     \indexdef{}{command}{default\_sort}\hypertarget{command.default-sort}{\hyperlink{command.default-sort}{\mbox{\isa{\isacommand{default{\isaliteral{5F}{\isacharunderscore}}sort}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}}

  1386   \end{matharray}

  1388   \begin{railoutput}

  1389 \rail@begin{2}{}

  1390 \rail@term{\hyperlink{command.classes}{\mbox{\isa{\isacommand{classes}}}}}[]

  1391 \rail@plus

  1392 \rail@nont{\hyperlink{syntax.classdecl}{\mbox{\isa{classdecl}}}}[]

  1393 \rail@nextplus{1}

  1394 \rail@endplus

  1395 \rail@end

  1396 \rail@begin{3}{}

  1397 \rail@term{\hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}}[]

  1398 \rail@plus

  1399 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]

  1400 \rail@bar

  1401 \rail@term{\isa{{\isaliteral{3C}{\isacharless}}}}[]

  1402 \rail@nextbar{1}

  1403 \rail@term{\isa{{\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}}}[]

  1404 \rail@endbar

  1405 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]

  1406 \rail@nextplus{2}

  1407 \rail@cterm{\isa{\isakeyword{and}}}[]

  1408 \rail@endplus

  1409 \rail@end

  1410 \rail@begin{1}{}

  1411 \rail@term{\hyperlink{command.default-sort}{\mbox{\isa{\isacommand{default{\isaliteral{5F}{\isacharunderscore}}sort}}}}}[]

  1412 \rail@nont{\hyperlink{syntax.sort}{\mbox{\isa{sort}}}}[]

  1413 \rail@end

  1414 \end{railoutput}

  1417   \begin{description}

  1419   \item \hyperlink{command.classes}{\mbox{\isa{\isacommand{classes}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} declares class

  1420   \isa{c} to be a subclass of existing classes \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}.

  1421   Isabelle implicitly maintains the transitive closure of the class

  1422   hierarchy.  Cyclic class structures are not permitted.

  1424   \item \hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}} states subclass

  1425   relations between existing classes \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}}.

  1426   This is done axiomatically!  The \indexref{}{command}{subclass}\hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}} and

  1427   \indexref{}{command}{instance}\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} commands (see \secref{sec:class}) provide

  1428   a way to introduce proven class relations.

  1430   \item \hyperlink{command.default-sort}{\mbox{\isa{\isacommand{default{\isaliteral{5F}{\isacharunderscore}}sort}}}}~\isa{s} makes sort \isa{s} the

  1431   new default sort for any type variable that is given explicitly in

  1432   the text, but lacks a sort constraint (wrt.\ the current context).

  1433   Type variables generated by type inference are not affected.

  1435   Usually the default sort is only changed when defining a new

  1436   object-logic.  For example, the default sort in Isabelle/HOL is

  1437   \isa{type}, the class of all HOL types.

  1439   When merging theories, the default sorts of the parents are

  1440   logically intersected, i.e.\ the representations as lists of classes

  1441   are joined.

  1443   \end{description}%

  1444 \end{isamarkuptext}%

  1445 \isamarkuptrue%

  1446 %

  1447 \isamarkupsubsection{Types and type abbreviations \label{sec:types-pure}%

  1448 }

  1449 \isamarkuptrue%

  1450 %

  1451 \begin{isamarkuptext}%

  1452 \begin{matharray}{rcll}

  1453     \indexdef{}{command}{type\_synonym}\hypertarget{command.type-synonym}{\hyperlink{command.type-synonym}{\mbox{\isa{\isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\

  1454     \indexdef{}{command}{typedecl}\hypertarget{command.typedecl}{\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\

  1455     \indexdef{}{command}{arities}\hypertarget{command.arities}{\hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} & (axiomatic!) \\

  1456   \end{matharray}

  1458   \begin{railoutput}

  1459 \rail@begin{2}{}

  1460 \rail@term{\hyperlink{command.type-synonym}{\mbox{\isa{\isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}}}}}[]

  1461 \rail@nont{\hyperlink{syntax.typespec}{\mbox{\isa{typespec}}}}[]

  1462 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]

  1463 \rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]

  1464 \rail@bar

  1465 \rail@nextbar{1}

  1466 \rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]

  1467 \rail@endbar

  1468 \rail@end

  1469 \rail@begin{2}{}

  1470 \rail@term{\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}}[]

  1471 \rail@nont{\hyperlink{syntax.typespec}{\mbox{\isa{typespec}}}}[]

  1472 \rail@bar

  1473 \rail@nextbar{1}

  1474 \rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]

  1475 \rail@endbar

  1476 \rail@end

  1477 \rail@begin{2}{}

  1478 \rail@term{\hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}}[]

  1479 \rail@plus

  1480 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]

  1481 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}}}[]

  1482 \rail@nont{\hyperlink{syntax.arity}{\mbox{\isa{arity}}}}[]

  1483 \rail@nextplus{1}

  1484 \rail@endplus

  1485 \rail@end

  1486 \end{railoutput}

  1489   \begin{description}

  1491   \item \hyperlink{command.type-synonym}{\mbox{\isa{\isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}\ t\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}}

  1492   introduces a \emph{type synonym} \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}} for the

  1493   existing type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}}.  Unlike actual type definitions, as are

  1494   available in Isabelle/HOL for example, type synonyms are merely

  1495   syntactic abbreviations without any logical significance.

  1496   Internally, type synonyms are fully expanded.

  1498   \item \hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}} declares a new

  1499   type constructor \isa{t}.  If the object-logic defines a base sort

  1500   \isa{s}, then the constructor is declared to operate on that, via

  1501   the axiomatic specification \hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}t\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}s{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ s{\isaliteral{29}{\isacharparenright}}s{\isaliteral{22}{\isachardoublequote}}}.

  1503   \item \hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}t\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}s\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ s\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}s{\isaliteral{22}{\isachardoublequote}}} augments

  1504   Isabelle's order-sorted signature of types by new type constructor

  1505   arities.  This is done axiomatically!  The \indexref{}{command}{instantiation}\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}

  1506   target (see \secref{sec:class}) provides a way to introduce

  1507   proven type arities.

  1509   \end{description}%

  1510 \end{isamarkuptext}%

  1511 \isamarkuptrue%

  1512 %

  1513 \isamarkupsubsection{Constants and definitions \label{sec:consts}%

  1514 }

  1515 \isamarkuptrue%

  1516 %

  1517 \begin{isamarkuptext}%

  1518 Definitions essentially express abbreviations within the logic.  The

  1519   simplest form of a definition is \isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t{\isaliteral{22}{\isachardoublequote}}}, where \isa{c} is a newly declared constant.  Isabelle also allows derived forms

  1520   where the arguments of \isa{c} appear on the left, abbreviating a

  1521   prefix of \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}}-abstractions, e.g.\ \isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x\ y{\isaliteral{2E}{\isachardot}}\ t{\isaliteral{22}{\isachardoublequote}}} may be

  1522   written more conveniently as \isa{{\isaliteral{22}{\isachardoublequote}}c\ x\ y\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t{\isaliteral{22}{\isachardoublequote}}}.  Moreover,

  1523   definitions may be weakened by adding arbitrary pre-conditions:

  1524   \isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ c\ x\ y\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t{\isaliteral{22}{\isachardoublequote}}}.

  1526   \medskip The built-in well-formedness conditions for definitional

  1527   specifications are:

  1529   \begin{itemize}

  1531   \item Arguments (on the left-hand side) must be distinct variables.

  1533   \item All variables on the right-hand side must also appear on the

  1534   left-hand side.

  1536   \item All type variables on the right-hand side must also appear on

  1537   the left-hand side; this prohibits \isa{{\isaliteral{22}{\isachardoublequote}}{\isadigit{0}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ length\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ list{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} for example.

  1539   \item The definition must not be recursive.  Most object-logics

  1540   provide definitional principles that can be used to express

  1541   recursion safely.

  1543   \end{itemize}

  1545   The right-hand side of overloaded definitions may mention overloaded constants

  1546   recursively at type instances corresponding to the immediate

  1547   argument types \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}.  Incomplete

  1548   specification patterns impose global constraints on all occurrences,

  1549   e.g.\ \isa{{\isaliteral{22}{\isachardoublequote}}d\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{22}{\isachardoublequote}}} on the left-hand side means that all

  1550   corresponding occurrences on some right-hand side need to be an

  1551   instance of this, general \isa{{\isaliteral{22}{\isachardoublequote}}d\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}{\isaliteral{22}{\isachardoublequote}}} will be disallowed.

  1553   \begin{matharray}{rcl}

  1554     \indexdef{}{command}{consts}\hypertarget{command.consts}{\hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\

  1555     \indexdef{}{command}{defs}\hypertarget{command.defs}{\hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\

  1556   \end{matharray}

  1558   \begin{railoutput}

  1559 \rail@begin{3}{}

  1560 \rail@term{\hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}}[]

  1561 \rail@plus

  1562 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

  1563 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}}}[]

  1564 \rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]

  1565 \rail@bar

  1566 \rail@nextbar{1}

  1567 \rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]

  1568 \rail@endbar

  1569 \rail@nextplus{2}

  1570 \rail@endplus

  1571 \rail@end

  1572 \rail@begin{2}{}

  1573 \rail@term{\hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}}}[]

  1574 \rail@bar

  1575 \rail@nextbar{1}

  1576 \rail@nont{\isa{opt}}[]

  1577 \rail@endbar

  1578 \rail@plus

  1579 \rail@nont{\hyperlink{syntax.axmdecl}{\mbox{\isa{axmdecl}}}}[]

  1580 \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]

  1581 \rail@nextplus{1}

  1582 \rail@endplus

  1583 \rail@end

  1584 \rail@begin{2}{\isa{opt}}

  1585 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]

  1586 \rail@bar

  1587 \rail@nextbar{1}

  1588 \rail@term{\isa{\isakeyword{unchecked}}}[]

  1589 \rail@endbar

  1590 \rail@bar

  1591 \rail@nextbar{1}

  1592 \rail@term{\isa{\isakeyword{overloaded}}}[]

  1593 \rail@endbar

  1594 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]

  1595 \rail@end

  1596 \end{railoutput}

  1599   \begin{description}

  1601   \item \hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{22}{\isachardoublequote}}} declares constant \isa{c} to have any instance of type scheme \isa{{\isaliteral{5C3C7369676D613E}{\isasymsigma}}}.  The optional

  1602   mixfix annotations may attach concrete syntax to the constants

  1603   declared.

  1605   \item \hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}name{\isaliteral{3A}{\isacharcolon}}\ eqn{\isaliteral{22}{\isachardoublequote}}} introduces \isa{eqn}

  1606   as a definitional axiom for some existing constant.

  1608   The \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}unchecked{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} option disables global dependency checks

  1609   for this definition, which is occasionally useful for exotic

  1610   overloading.  It is at the discretion of the user to avoid malformed

  1611   theory specifications!

  1613   The \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}overloaded{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} option declares definitions to be

  1614   potentially overloaded.  Unless this option is given, a warning

  1615   message would be issued for any definitional equation with a more

  1616   special type than that of the corresponding constant declaration.

  1618   \end{description}%

  1619 \end{isamarkuptext}%

  1620 \isamarkuptrue%

  1621 %

  1622 \isamarkupsection{Axioms and theorems \label{sec:axms-thms}%

  1623 }

  1624 \isamarkuptrue%

  1625 %

  1626 \begin{isamarkuptext}%

  1627 \begin{matharray}{rcll}

  1628     \indexdef{}{command}{axioms}\hypertarget{command.axioms}{\hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} & (axiomatic!) \\

  1629     \indexdef{}{command}{lemmas}\hypertarget{command.lemmas}{\hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\

  1630     \indexdef{}{command}{theorems}\hypertarget{command.theorems}{\hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\

  1631   \end{matharray}

  1633   \begin{railoutput}

  1634 \rail@begin{2}{}

  1635 \rail@term{\hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}}}[]

  1636 \rail@plus

  1637 \rail@nont{\hyperlink{syntax.axmdecl}{\mbox{\isa{axmdecl}}}}[]

  1638 \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]

  1639 \rail@nextplus{1}

  1640 \rail@endplus

  1641 \rail@end

  1642 \rail@begin{3}{}

  1643 \rail@bar

  1644 \rail@term{\hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}}[]

  1645 \rail@nextbar{1}

  1646 \rail@term{\hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}}}[]

  1647 \rail@endbar

  1648 \rail@bar

  1649 \rail@nextbar{1}

  1650 \rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]

  1651 \rail@endbar

  1652 \rail@plus

  1653 \rail@bar

  1654 \rail@nextbar{1}

  1655 \rail@nont{\hyperlink{syntax.thmdef}{\mbox{\isa{thmdef}}}}[]

  1656 \rail@endbar

  1657 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]

  1658 \rail@nextplus{2}

  1659 \rail@cterm{\isa{\isakeyword{and}}}[]

  1660 \rail@endplus

  1661 \rail@end

  1662 \end{railoutput}

  1665   \begin{description}

  1667   \item \hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} introduces arbitrary

  1668   statements as axioms of the meta-logic.  In fact, axioms are

  1669   ``axiomatic theorems'', and may be referred later just as any other

  1670   theorem.

  1672   Axioms are usually only introduced when declaring new logical

  1673   systems.  Everyday work is typically done the hard way, with proper

  1674   definitions and proven theorems.

  1676   \item \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\ {\isaliteral{3D}{\isacharequal}}\ b\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ b\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} retrieves and stores

  1677   existing facts in the theory context, or the specified target

  1678   context (see also \secref{sec:target}).  Typical applications would

  1679   also involve attributes, to declare Simplifier rules, for example.

  1681   \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.

  1683   \end{description}%

  1684 \end{isamarkuptext}%

  1685 \isamarkuptrue%

  1686 %

  1687 \isamarkupsection{Oracles%

  1688 }

  1689 \isamarkuptrue%

  1690 %

  1691 \begin{isamarkuptext}%

  1692 Oracles allow Isabelle to take advantage of external reasoners

  1693   such as arithmetic decision procedures, model checkers, fast

  1694   tautology checkers or computer algebra systems.  Invoked as an

  1695   oracle, an external reasoner can create arbitrary Isabelle theorems.

  1697   It is the responsibility of the user to ensure that the external

  1698   reasoner is as trustworthy as the application requires.  Another

  1699   typical source of errors is the linkup between Isabelle and the

  1700   external tool, not just its concrete implementation, but also the

  1701   required translation between two different logical environments.

  1703   Isabelle merely guarantees well-formedness of the propositions being

  1704   asserted, and records within the internal derivation object how

  1705   presumed theorems depend on unproven suppositions.

  1707   \begin{matharray}{rcll}

  1708     \indexdef{}{command}{oracle}\hypertarget{command.oracle}{\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} & (axiomatic!) \\

  1709   \end{matharray}

  1711   \begin{railoutput}

  1712 \rail@begin{1}{}

  1713 \rail@term{\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}}[]

  1714 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]

  1715 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]

  1716 \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]

  1717 \rail@end

  1718 \end{railoutput}

  1721   \begin{description}

  1723   \item \hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}name\ {\isaliteral{3D}{\isacharequal}}\ text{\isaliteral{22}{\isachardoublequote}}} turns the given ML

  1724   expression \isa{{\isaliteral{22}{\isachardoublequote}}text{\isaliteral{22}{\isachardoublequote}}} of type \verb|'a -> cterm| into an

  1725   ML function of type \verb|'a -> thm|, which is bound to the

  1726   global identifier \verb|name|.  This acts like an infinitary

  1727   specification of axioms!  Invoking the oracle only works within the

  1728   scope of the resulting theory.

  1730   \end{description}

  1732   See \verb|~~/src/HOL/ex/Iff_Oracle.thy| for a worked example of

  1733   defining a new primitive rule as oracle, and turning it into a proof

  1734   method.%

  1735 \end{isamarkuptext}%

  1736 \isamarkuptrue%

  1737 %

  1738 \isamarkupsection{Name spaces%

  1739 }

  1740 \isamarkuptrue%

  1741 %

  1742 \begin{isamarkuptext}%

  1743 \begin{matharray}{rcl}

  1744     \indexdef{}{command}{hide\_class}\hypertarget{command.hide-class}{\hyperlink{command.hide-class}{\mbox{\isa{\isacommand{hide{\isaliteral{5F}{\isacharunderscore}}class}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\

  1745     \indexdef{}{command}{hide\_type}\hypertarget{command.hide-type}{\hyperlink{command.hide-type}{\mbox{\isa{\isacommand{hide{\isaliteral{5F}{\isacharunderscore}}type}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\

  1746     \indexdef{}{command}{hide\_const}\hypertarget{command.hide-const}{\hyperlink{command.hide-const}{\mbox{\isa{\isacommand{hide{\isaliteral{5F}{\isacharunderscore}}const}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\

  1747     \indexdef{}{command}{hide\_fact}\hypertarget{command.hide-fact}{\hyperlink{command.hide-fact}{\mbox{\isa{\isacommand{hide{\isaliteral{5F}{\isacharunderscore}}fact}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\

  1748   \end{matharray}

  1750   \begin{railoutput}

  1751 \rail@begin{4}{}

  1752 \rail@bar

  1753 \rail@nont{\hyperlink{command.hide-class}{\mbox{\isa{\isacommand{hide{\isaliteral{5F}{\isacharunderscore}}class}}}}}[]

  1754 \rail@nextbar{1}

  1755 \rail@nont{\hyperlink{command.hide-type}{\mbox{\isa{\isacommand{hide{\isaliteral{5F}{\isacharunderscore}}type}}}}}[]

  1756 \rail@nextbar{2}

  1757 \rail@nont{\hyperlink{command.hide-const}{\mbox{\isa{\isacommand{hide{\isaliteral{5F}{\isacharunderscore}}const}}}}}[]

  1758 \rail@nextbar{3}

  1759 \rail@nont{\hyperlink{command.hide-fact}{\mbox{\isa{\isacommand{hide{\isaliteral{5F}{\isacharunderscore}}fact}}}}}[]

  1760 \rail@endbar

  1761 \rail@bar

  1762 \rail@nextbar{1}

  1763 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]

  1764 \rail@term{\isa{\isakeyword{open}}}[]

  1765 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]

  1766 \rail@endbar

  1767 \rail@plus

  1768 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]

  1769 \rail@nextplus{1}

  1770 \rail@endplus

  1771 \rail@end

  1772 \end{railoutput}

  1775   Isabelle organizes any kind of name declarations (of types,

  1776   constants, theorems etc.) by separate hierarchically structured name

  1777   spaces.  Normally the user does not have to control the behavior of

  1778   name spaces by hand, yet the following commands provide some way to

  1779   do so.

  1781   \begin{description}

  1783   \item \hyperlink{command.hide-class}{\mbox{\isa{\isacommand{hide{\isaliteral{5F}{\isacharunderscore}}class}}}}~\isa{names} fully removes class

  1784   declarations from a given name space; with the \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}open{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}

  1785   option, only the base name is hidden.

  1787   Note that hiding name space accesses has no impact on logical

  1788   declarations --- they remain valid internally.  Entities that are no

  1789   longer accessible to the user are printed with the special qualifier

  1790   ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}}'' prefixed to the full internal name.

  1792   \item \hyperlink{command.hide-type}{\mbox{\isa{\isacommand{hide{\isaliteral{5F}{\isacharunderscore}}type}}}}, \hyperlink{command.hide-const}{\mbox{\isa{\isacommand{hide{\isaliteral{5F}{\isacharunderscore}}const}}}}, and \hyperlink{command.hide-fact}{\mbox{\isa{\isacommand{hide{\isaliteral{5F}{\isacharunderscore}}fact}}}} are similar to \hyperlink{command.hide-class}{\mbox{\isa{\isacommand{hide{\isaliteral{5F}{\isacharunderscore}}class}}}}, but hide types,

  1793   constants, and facts, respectively.

  1795   \end{description}%

  1796 \end{isamarkuptext}%

  1797 \isamarkuptrue%

  1798 %

  1799 \isadelimtheory

  1800 %

  1801 \endisadelimtheory

  1802 %

  1803 \isatagtheory

  1804 \isacommand{end}\isamarkupfalse%

  1805 %

  1806 \endisatagtheory

  1807 {\isafoldtheory}%

  1808 %

  1809 \isadelimtheory

  1810 %

  1811 \endisadelimtheory

  1812 \isanewline

  1813 \end{isabellebody}%

  1814 %%% Local Variables:

  1815 %%% mode: latex

  1816 %%% TeX-master: "root"

  1817 %%% End:

author	wenzelm
	Thu, 05 May 2011 23:15:11 +0200
changeset 43575	3f19e324ff59
parent 43535	2080fe35abea
child 43576	528a2ba8fa74
permissions	-rw-r--r--