doc-src/IsarRef/Thy/document/Spec.tex
 author wenzelm Fri Oct 29 11:49:56 2010 +0200 (2010-10-29) changeset 40255 9ffbc25e1606 parent 40240 a2dde53b15ef child 40256 eb5412b77ac4 permissions -rw-r--r--
eliminated obsolete \_ escapes in rail environments;
     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}\ 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.

    32

    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{{\isachardoublequote}toplevel\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\

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

    50   \end{matharray}

    51

    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}}}}.

    57

    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}.

    64

    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.

    70

    71   \begin{rail}

    72     'theory' name 'imports' (name +) uses? 'begin'

    73     ;

    74

    75     uses: 'uses' ((name | parname) +);

    76   \end{rail}

    77

    78   \begin{description}

    79

    80   \item \hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}}~\isa{{\isachardoublequote}A\ {\isasymIMPORTS}\ B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n\ {\isasymBEGIN}{\isachardoublequote}}

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

    82   theories \isa{{\isachardoublequote}B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n{\isachardoublequote}}.

    83

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

    85   resulting theory structure of an Isabelle session forms a directed

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

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

    88   changed files are automatically reloaded whenever a theory header

    89   specification is processed.

    90

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

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

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

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

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

    96   other file formats require specific load commands defined by the

    97   corresponding tools or packages.

    98

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

   100   definition.  Note that local theory targets involve a local

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

   102

   103   \end{description}%

   104 \end{isamarkuptext}%

   105 \isamarkuptrue%

   106 %

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

   108 }

   109 \isamarkuptrue%

   110 %

   111 \begin{isamarkuptext}%

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

   113   enclosing theory.  Contexts may introduce parameters (fixed

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

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

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

   117   (cf.\ \secref{sec:class}); the name \isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' signifies the

   118   global theory context.

   119

   120   \begin{matharray}{rcll}

   121     \indexdef{}{command}{context}\hypertarget{command.context}{\hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\

   122     \indexdef{local}{command}{end}\hypertarget{command.local.end}{\hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\

   123   \end{matharray}

   124

   125   \indexouternonterm{target}

   126   \begin{rail}

   127     'context' name 'begin'

   128     ;

   129

   130     target: '(' 'in' name ')'

   131     ;

   132   \end{rail}

   133

   134   \begin{description}

   135

   136   \item \hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}~\isa{{\isachardoublequote}c\ {\isasymBEGIN}{\isachardoublequote}} recommences an

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

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

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

   140   initial specification.

   141

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

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

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

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

   146

   147   \item \isa{{\isachardoublequote}{\isacharparenleft}{\isachardoublequote}}\indexdef{}{keyword}{in}\hypertarget{keyword.in}{\hyperlink{keyword.in}{\mbox{\isa{\isakeyword{in}}}}}~\isa{{\isachardoublequote}c{\isacharparenright}{\isachardoublequote}} given after any

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

   149   \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}\ {\isasymdots}{\isachardoublequote}}'' or \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}\ {\isasymdots}{\isachardoublequote}}''.  This works both in a local or

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

   151   for this command only.  Note that \isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ {\isacharminus}{\isacharparenright}{\isachardoublequote}}'' will

   152   always produce a global result independently of the current target

   153   context.

   154

   155   \end{description}

   156

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

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

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

   160   \isa{c} with parameter \isa{x} and assumption \isa{{\isachardoublequote}A{\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}}.

   161

   162   Definitions are exported by introducing a global version with

   163   additional arguments; a syntactic abbreviation links the long form

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

   165   \isa{{\isachardoublequote}a\ {\isasymequiv}\ t{\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}} becomes \isa{{\isachardoublequote}c{\isachardot}a\ {\isacharquery}x\ {\isasymequiv}\ t{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}{\isachardoublequote}} at the theory

   166   level (for arbitrary \isa{{\isachardoublequote}{\isacharquery}x{\isachardoublequote}}), together with a local

   167   abbreviation \isa{{\isachardoublequote}c\ {\isasymequiv}\ c{\isachardot}a\ x{\isachardoublequote}} in the target context (for the

   168   fixed parameter \isa{x}).

   169

   170   Theorems are exported by discharging the assumptions and

   171   generalizing the parameters of the context.  For example, \isa{{\isachardoublequote}a{\isacharcolon}\ B{\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}} becomes \isa{{\isachardoublequote}c{\isachardot}a{\isacharcolon}\ A{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}\ {\isasymLongrightarrow}\ B{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}{\isachardoublequote}}, again for arbitrary

   172   \isa{{\isachardoublequote}{\isacharquery}x{\isachardoublequote}}.%

   173 \end{isamarkuptext}%

   174 \isamarkuptrue%

   175 %

   176 \isamarkupsection{Basic specification elements%

   177 }

   178 \isamarkuptrue%

   179 %

   180 \begin{isamarkuptext}%

   181 \begin{matharray}{rcll}

   182     \indexdef{}{command}{axiomatization}\hypertarget{command.axiomatization}{\hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{axiomatization}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\

   183     \indexdef{}{command}{definition}\hypertarget{command.definition}{\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\

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

   185     \indexdef{}{command}{abbreviation}\hypertarget{command.abbreviation}{\hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\

   186     \indexdef{}{command}{print\_abbrevs}\hypertarget{command.print-abbrevs}{\hyperlink{command.print-abbrevs}{\mbox{\isa{\isacommand{print{\isacharunderscore}abbrevs}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}\ {\isachardoublequote}} \\

   187   \end{matharray}

   188

   189   These specification mechanisms provide a slightly more abstract view

   190   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

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

   192   available, and result names need not be given.

   193

   194   \begin{rail}

   195     'axiomatization' target? fixes? ('where' specs)?

   196     ;

   197     'definition' target? (decl 'where')? thmdecl? prop

   198     ;

   199     'abbreviation' target? mode? (decl 'where')? prop

   200     ;

   201

   202     fixes: ((name ('::' type)? mixfix? | vars) + 'and')

   203     ;

   204     specs: (thmdecl? props + 'and')

   205     ;

   206     decl: name ('::' type)? mixfix?

   207     ;

   208   \end{rail}

   209

   210   \begin{description}

   211

   212   \item \hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{axiomatization}}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymdots}\ c\isactrlsub m\ {\isasymWHERE}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}

   213   introduces several constants simultaneously and states axiomatic

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

   215   once and for all, which prevents additional specifications being

   216   issued later on.

   217

   218   Note that axiomatic specifications are only appropriate when

   219   declaring a new logical system; axiomatic specifications are

   220   restricted to global theory contexts.  Normal applications should

   221   only use definitional mechanisms!

   222

   223   \item \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}~\isa{{\isachardoublequote}c\ {\isasymWHERE}\ eq{\isachardoublequote}} produces an

   224   internal definition \isa{{\isachardoublequote}c\ {\isasymequiv}\ t{\isachardoublequote}} according to the specification

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

   226   given proposition may deviate from internal meta-level equality

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

   228   object-logic.  This usually covers object-level equality \isa{{\isachardoublequote}x\ {\isacharequal}\ y{\isachardoublequote}} and equivalence \isa{{\isachardoublequote}A\ {\isasymleftrightarrow}\ B{\isachardoublequote}}.  End-users normally need not

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

   230

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

   232   well as additional conditions, e.g.\ \isa{{\isachardoublequote}f\ x\ y\ {\isacharequal}\ t{\isachardoublequote}} instead of

   233   \isa{{\isachardoublequote}f\ {\isasymequiv}\ {\isasymlambda}x\ y{\isachardot}\ t{\isachardoublequote}} and \isa{{\isachardoublequote}y\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ g\ x\ y\ {\isacharequal}\ u{\isachardoublequote}} instead of an

   234   unrestricted \isa{{\isachardoublequote}g\ {\isasymequiv}\ {\isasymlambda}x\ y{\isachardot}\ u{\isachardoublequote}}.

   235

   236   \item \hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}~\isa{{\isachardoublequote}c\ {\isasymWHERE}\ eq{\isachardoublequote}} introduces a

   237   syntactic constant which is associated with a certain term according

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

   239

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

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

   242   terms involves higher-order rewriting with rules stemming from

   243   reverted abbreviations.  This needs some care to avoid overlapping

   244   or looping syntactic replacements!

   245

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

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

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

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

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

   251   \secref{sec:syn-trans}.

   252

   253   \item \hyperlink{command.print-abbrevs}{\mbox{\isa{\isacommand{print{\isacharunderscore}abbrevs}}}} prints all constant abbreviations

   254   of the current context.

   255

   256   \end{description}%

   257 \end{isamarkuptext}%

   258 \isamarkuptrue%

   259 %

   260 \isamarkupsection{Generic declarations%

   261 }

   262 \isamarkuptrue%

   263 %

   264 \begin{isamarkuptext}%

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

   266   generic declaration elements.  Since the underlying concept of local

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

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

   269   original declaration context wrt.\ the application context

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

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

   272   means of an attribute.

   273

   274   \begin{matharray}{rcl}

   275     \indexdef{}{command}{declaration}\hypertarget{command.declaration}{\hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\

   276     \indexdef{}{command}{declare}\hypertarget{command.declare}{\hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\

   277   \end{matharray}

   278

   279   \begin{rail}

   280     'declaration' ('(pervasive)')? target? text

   281     ;

   282     'declare' target? (thmrefs + 'and')

   283     ;

   284   \end{rail}

   285

   286   \begin{description}

   287

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

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

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

   291   function is transformed according to the morphisms being involved in

   292   the interpretation hierarchy.

   293

   294   If the \isa{{\isachardoublequote}{\isacharparenleft}pervasive{\isacharparenright}{\isachardoublequote}} option is given, the corresponding

   295   declaration is applied to all possible contexts involved, including

   296   the global background theory.

   297

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

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

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

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

   302   of applying attributes as included in the theorem specification.

   303

   304   \end{description}%

   305 \end{isamarkuptext}%

   306 \isamarkuptrue%

   307 %

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

   309 }

   310 \isamarkuptrue%

   311 %

   312 \begin{isamarkuptext}%

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

   314   declaration elements that are modeled after the Isar proof context

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

   316 \end{isamarkuptext}%

   317 \isamarkuptrue%

   318 %

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

   320 }

   321 \isamarkuptrue%

   322 %

   323 \begin{isamarkuptext}%

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

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

   326   instances of declaration elements from the locales.  Two locale

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

   328   parameters are instantiated with equivalent terms.  Declaration

   329   elements from equal instances are never repeated, thus avoiding

   330   duplicate declarations.

   331

   332   \indexouternonterm{localeexpr}

   333   \begin{rail}

   334     localeexpr: (instance + '+') ('for' (fixes + 'and'))?

   335     ;

   336     instance: (qualifier ':')? nameref (posinsts | namedinsts)

   337     ;

   338     qualifier: name ('?' | '!')?

   339     ;

   340     posinsts: (term | '_')*

   341     ;

   342     namedinsts: 'where' (name '=' term + 'and')

   343     ;

   344   \end{rail}

   345

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

   347   positional or named parameter instantiations.  Identical

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

   349   may be omitted.  The notation \_' enables to omit the instantiation

   350   for a parameter inside a positional instantiation.

   351

   352   Terms in instantiations are from the context the locale expressions

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

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

   355   instance are effective when parsing subsequent instances of the same

   356   expression.

   357

   358   Instances have an optional qualifier which applies to names in

   359   declarations.  Names include local definitions and theorem names.

   360   If present, the qualifier itself is either optional

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

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

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

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

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

   366 \end{isamarkuptext}%

   367 \isamarkuptrue%

   368 %

   369 \isamarkupsubsection{Locale declarations%

   370 }

   371 \isamarkuptrue%

   372 %

   373 \begin{isamarkuptext}%

   374 \begin{matharray}{rcl}

   375     \indexdef{}{command}{locale}\hypertarget{command.locale}{\hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\

   376     \indexdef{}{command}{print\_locale}\hypertarget{command.print-locale}{\hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\

   377     \indexdef{}{command}{print\_locales}\hypertarget{command.print-locales}{\hyperlink{command.print-locales}{\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\

   378     \indexdef{}{method}{intro\_locales}\hypertarget{method.intro-locales}{\hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}}} & : & \isa{method} \\

   379     \indexdef{}{method}{unfold\_locales}\hypertarget{method.unfold-locales}{\hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}}} & : & \isa{method} \\

   380   \end{matharray}

   381

   382   \indexouternonterm{contextelem}

   383   \indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes}

   384   \indexisarelem{defines}\indexisarelem{notes}

   385   \begin{rail}

   386     'locale' name ('=' locale)? 'begin'?

   387     ;

   388     'print_locale' '!'? nameref

   389     ;

   390     locale: contextelem+ | localeexpr ('+' (contextelem+))?

   391     ;

   392     contextelem:

   393     'fixes' (fixes + 'and')

   394     | 'constrains' (name '::' type + 'and')

   395     | 'assumes' (props + 'and')

   396     | 'defines' (thmdecl? prop proppat? + 'and')

   397     | 'notes' (thmdef? thmrefs + 'and')

   398     ;

   399   \end{rail}

   400

   401   \begin{description}

   402

   403   \item \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}~\isa{{\isachardoublequote}loc\ {\isacharequal}\ import\ {\isacharplus}\ body{\isachardoublequote}} defines a

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

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

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

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

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

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

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

   411   may acquire.

   412

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

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

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

   416   whose instantance is omitted automatically extend the (possibly

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

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

   419   and also in the subsequent context elements and provides a

   420   notational convenience for the inheritance of parameters in locale

   421   declarations.

   422

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

   424

   425   \begin{description}

   426

   427   \item \hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}}~\isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}} declares a local

   428   parameter of type \isa{{\isasymtau}} and mixfix annotation \isa{mx} (both

   429   are optional).  The special syntax declaration \isa{{\isachardoublequote}{\isacharparenleft}{\isasymSTRUCTURE}{\isacharparenright}{\isachardoublequote}}'' means that \isa{x} may be referenced

   430   implicitly in this context.

   431

   432   \item \hyperlink{element.constrains}{\mbox{\isa{\isakeyword{constrains}}}}~\isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isachardoublequote}} introduces a type

   433   constraint \isa{{\isasymtau}} on the local parameter \isa{x}.  This

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

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

   436

   437   \item \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}

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

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

   440

   441   \item \hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ x\ {\isasymequiv}\ t{\isachardoublequote}} defines a previously

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

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

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

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

   446   \hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}}~\isa{{\isachardoublequote}f\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n\ {\isasymequiv}\ t{\isachardoublequote}}''.

   447

   448   \item \hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}}~\isa{{\isachardoublequote}a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}}

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

   450   include arbitrary declarations in any attribute specifications

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

   452

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

   454   maintains a dynamic relation to the locales being referenced

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

   456

   457   \end{description}

   458

   459   Note that \isa{{\isachardoublequote}{\isacharparenleft}{\isasymIS}\ p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub n{\isacharparenright}{\isachardoublequote}}'' patterns given

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

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

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

   463   though.

   464

   465   \medskip Locale specifications are closed up'' by

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

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

   468   newly specified assumptions, omitting the content of included locale

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

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

   471   specification text.

   472

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

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

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

   476   packages attempts to internalize statements according to the

   477   object-logic setup (e.g.\ replacing \isa{{\isasymAnd}} by \isa{{\isasymforall}}, and

   478   \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}} by \isa{{\isachardoublequote}{\isasymlongrightarrow}{\isachardoublequote}} in HOL; see also

   479   \secref{sec:object-logic}).  Separate introduction rules \isa{loc{\isacharunderscore}axioms{\isachardot}intro} and \isa{loc{\isachardot}intro} are provided as well.

   480

   481   \item \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{{\isachardoublequote}locale{\isachardoublequote}} prints the

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

   483   elements by default.  Use \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}} to

   484   have them included.

   485

   486   \item \hyperlink{command.print-locales}{\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}} prints the names of all locales

   487   of the current theory.

   488

   489   \item \hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}} and \hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}}

   490   repeatedly expand all introduction rules of locale predicates of the

   491   theory.  While \hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}} only applies the \isa{loc{\isachardot}intro} introduction rules and therefore does not decend to

   492   assumptions, \hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}} is more aggressive and applies

   493   \isa{loc{\isacharunderscore}axioms{\isachardot}intro} as well.  Both methods are aware of locale

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

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

   496   by the current context are discharged automatically.

   497

   498   \end{description}%

   499 \end{isamarkuptext}%

   500 \isamarkuptrue%

   501 %

   502 \isamarkupsubsection{Locale interpretations%

   503 }

   504 \isamarkuptrue%

   505 %

   506 \begin{isamarkuptext}%

   507 Locale expressions may be instantiated, and the instantiated facts

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

   509   instantiated specification and is called \emph{locale

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

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

   512

   513   \begin{matharray}{rcl}

   514     \indexdef{}{command}{sublocale}\hypertarget{command.sublocale}{\hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\

   515     \indexdef{}{command}{interpretation}\hypertarget{command.interpretation}{\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\

   516     \indexdef{}{command}{interpret}\hypertarget{command.interpret}{\hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}\ {\isacharbar}\ proof{\isacharparenleft}chain{\isacharparenright}\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\

   517     \indexdef{}{command}{print\_interps}\hypertarget{command.print-interps}{\hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\

   518   \end{matharray}

   519

   520   \indexouternonterm{interp}

   521   \begin{rail}

   522     'sublocale' nameref ('<' | subseteq) localeexpr

   523     ;

   524     'interpretation' localeepxr equations?

   525     ;

   526     'interpret' localeexpr equations?

   527     ;

   528     'print_interps' nameref

   529     ;

   530     equations: 'where' (thmdecl? prop + 'and')

   531     ;

   532   \end{rail}

   533

   534   \begin{description}

   535

   536   \item \hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}}~\isa{{\isachardoublequote}name\ {\isasymsubseteq}\ expr{\isachardoublequote}}

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

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

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

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

   541   the proof obligation has been dischared, the facts of \isa{expr}

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

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

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

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

   546   become also available in \isa{name}.

   547

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

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

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

   551   circular interpretations to the extent that no infinite chains are

   552   generated in the locale hierarchy.

   553

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

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

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

   557   interpreted in the theory already.

   558

   559   \item \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isachardoublequote}expr\ {\isasymWHERE}\ eqns{\isachardoublequote}}

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

   561   obligations for the instantiated specifications (assumes and defines

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

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

   564

   565   Additional equations, which are unfolded during

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

   567   This is useful for interpreting concepts introduced through

   568   definition specification elements.  The equations must be proved.

   569

   570   The command is aware of interpretations already active in the

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

   572   simplify the proof obligations use methods \hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}}

   573   or \hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}}.  Post-processing is not applied to

   574   facts of interpretations that are already active.  This avoids

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

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

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

   578   parts.

   579

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

   581   to the theory for all active interpretations also.  That is,

   582   interpretations dynamically participate in any facts added to

   583   locales.

   584

   585   \item \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}~\isa{{\isachardoublequote}expr\ {\isasymWHERE}\ eqns{\isachardoublequote}} interprets

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

   587   interpretation in theories.  Note that rewrite rules given to

   588   \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}} should be explicitly universally quantified.

   589

   590   \item \hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}}~\isa{{\isachardoublequote}locale{\isachardoublequote}} lists all

   591   interpretations of \isa{{\isachardoublequote}locale{\isachardoublequote}} in the current theory or proof

   592   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

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

   594

   595   \end{description}

   596

   597   \begin{warn}

   598     Since attributes are applied to interpreted theorems,

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

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

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

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

   603     interpretation to revert such declarations.

   604   \end{warn}

   605

   606   \begin{warn}

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

   608     interpretations.  This happens if the same specification fragment

   609     is interpreted twice and the instantiation of the second

   610     interpretation is more general than the interpretation of the

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

   612     interpretations.

   613   \end{warn}%

   614 \end{isamarkuptext}%

   615 \isamarkuptrue%

   616 %

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

   618 }

   619 \isamarkuptrue%

   620 %

   621 \begin{isamarkuptext}%

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

   623   \isa{{\isasymalpha}}.  Beyond the underlying locale, a corresponding type class

   624   is established which is interpreted logically as axiomatic type

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

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

   627   generality of locales combined with the commodity of type classes

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

   629   tutorial.

   630

   631   \begin{matharray}{rcl}

   632     \indexdef{}{command}{class}\hypertarget{command.class}{\hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\

   633     \indexdef{}{command}{instantiation}\hypertarget{command.instantiation}{\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\

   634     \indexdef{}{command}{instance}\hypertarget{command.instance}{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\

   635     \indexdef{}{command}{instance}\hypertarget{command.instance}{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\

   636     \indexdef{}{command}{subclass}\hypertarget{command.subclass}{\hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\

   637     \indexdef{}{command}{print\_classes}\hypertarget{command.print-classes}{\hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\

   638     \indexdef{}{command}{class\_deps}\hypertarget{command.class-deps}{\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\

   639     \indexdef{}{method}{intro\_classes}\hypertarget{method.intro-classes}{\hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}} & : & \isa{method} \\

   640   \end{matharray}

   641

   642   \begin{rail}

   643     'class' name '=' ((superclassexpr '+' (contextelem+)) | superclassexpr | (contextelem+)) \\

   644       'begin'?

   645     ;

   646     'instantiation' (nameref + 'and') '::' arity 'begin'

   647     ;

   648     'instance'

   649     ;

   650     'instance' (nameref + 'and') '::' arity

   651     ;

   652     'subclass' target? nameref

   653     ;

   654     'instance' nameref ('<' | subseteq) nameref

   655     ;

   656     'print_classes'

   657     ;

   658     'class_deps'

   659     ;

   660

   661     superclassexpr: nameref | (nameref '+' superclassexpr)

   662     ;

   663   \end{rail}

   664

   665   \begin{description}

   666

   667   \item \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}~\isa{{\isachardoublequote}c\ {\isacharequal}\ superclasses\ {\isacharplus}\ body{\isachardoublequote}} defines

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

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

   670

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

   672   theory level (\emph{class operations} \isa{{\isachardoublequote}f\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ f\isactrlsub n{\isachardoublequote}} of class \isa{c}), mapping the local type parameter

   673   \isa{{\isasymalpha}} to a schematic type variable \isa{{\isachardoublequote}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isachardoublequote}}.

   674

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

   676   mapping each local parameter \isa{{\isachardoublequote}f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} to its

   677   corresponding global constant \isa{{\isachardoublequote}f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}}.  The

   678   corresponding introduction rule is provided as \isa{c{\isacharunderscore}class{\isacharunderscore}axioms{\isachardot}intro}.  This rule should be rarely needed directly

   679   --- the \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} method takes care of the details of

   680   class membership proofs.

   681

   682   \item \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}s\ {\isasymBEGIN}{\isachardoublequote}} opens a theory target (cf.\ \secref{sec:target}) which

   683   allows to specify class operations \isa{{\isachardoublequote}f\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ f\isactrlsub n{\isachardoublequote}} corresponding

   684   to sort \isa{s} at the particular type instance \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ s\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}}.  A plain \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} command in the

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

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

   687

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

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

   690   in Isabelle/HOL.

   691

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

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

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

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

   696

   697   On the theory level, \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}s{\isachardoublequote}} provides a convenient way to instantiate a type class with no

   698   need to specify operations: one can continue with the

   699   instantiation proof immediately.

   700

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

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

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

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

   705

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

   707   \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}:  \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}} opens

   708   a proof that class \isa{{\isachardoublequote}c\isactrlisub {\isadigit{2}}{\isachardoublequote}} implies \isa{{\isachardoublequote}c\isactrlisub {\isadigit{1}}{\isachardoublequote}} without reference

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

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

   711   the theory level.

   712

   713   \item \hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}} prints all classes in the current

   714   theory.

   715

   716   \item \hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}} visualizes all classes and their

   717   subclass relations as a Hasse diagram.

   718

   719   \item \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} repeatedly expands all class

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

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

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

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

   724   single \hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}}'' proof step.

   725

   726   \end{description}%

   727 \end{isamarkuptext}%

   728 \isamarkuptrue%

   729 %

   730 \isamarkupsubsection{The class target%

   731 }

   732 \isamarkuptrue%

   733 %

   734 \begin{isamarkuptext}%

   735 %FIXME check

   736

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

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

   739   locale target behaviour the following happens.

   740

   741   \begin{itemize}

   742

   743   \item Local constant declarations \isa{{\isachardoublequote}g{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} referring to the

   744   local type parameter \isa{{\isasymalpha}} and local parameters \isa{{\isachardoublequote}f{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}}

   745   are accompanied by theory-level constants \isa{{\isachardoublequote}g{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}}

   746   referring to theory-level class operations \isa{{\isachardoublequote}f{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}}.

   747

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

   749

   750   \item Local syntax refers to local operations \isa{{\isachardoublequote}g{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} and

   751   global operations \isa{{\isachardoublequote}g{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}} uniformly.  Type inference

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

   753   needed.

   754

   755   \end{itemize}%

   756 \end{isamarkuptext}%

   757 \isamarkuptrue%

   758 %

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

   760 }

   761 \isamarkuptrue%

   762 %

   763 \begin{isamarkuptext}%

   764 The class relation together with the collection of

   765   type-constructor arities must obey the principle of

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

   767

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

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

   770   Moreover the collection of arities \isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c{\isachardoublequote}} is

   771   completed such that \isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c{\isachardoublequote}} and \isa{{\isachardoublequote}c\ {\isasymsubseteq}\ c{\isacharprime}{\isachardoublequote}}

   772   implies \isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c{\isacharprime}{\isachardoublequote}} for all such declarations.

   773

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

   775   the class relation \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}} is extended to sorts as

   776   follows:

   777   $  778 \isa{{\isachardoublequote}s\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ s\isactrlsub {\isadigit{2}}\ {\isasymequiv}\ {\isasymforall}c\isactrlsub {\isadigit{2}}\ {\isasymin}\ s\isactrlsub {\isadigit{2}}{\isachardot}\ {\isasymexists}c\isactrlsub {\isadigit{1}}\ {\isasymin}\ s\isactrlsub {\isadigit{1}}{\isachardot}\ c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}}   779$

   780

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

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

   783

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

   785   arities relation means:

   786   $  787 \isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s\isactrlsub {\isadigit{1}}{\isacharparenright}c\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s\isactrlsub {\isadigit{2}}{\isacharparenright}c\isactrlsub {\isadigit{2}}\ {\isasymLongrightarrow}\ c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}\ {\isasymLongrightarrow}\ \isactrlvec s\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ \isactrlvec s\isactrlsub {\isadigit{2}}{\isachardoublequote}}   788$

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

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

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

   792

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

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

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

   796 \end{isamarkuptext}%

   797 \isamarkuptrue%

   798 %

   799 \isamarkupsection{Unrestricted overloading%

   800 }

   801 \isamarkuptrue%

   802 %

   803 \begin{isamarkuptext}%

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

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

   806   constant being declared as \isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ decl{\isachardoublequote}} may be

   807   defined separately on type instances

   808   \isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}{\isasymbeta}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymbeta}\isactrlsub n{\isacharparenright}\ t\ decl{\isachardoublequote}}

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

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

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

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

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

   814   end-users.

   815

   816   \begin{matharray}{rcl}

   817     \indexdef{}{command}{overloading}\hypertarget{command.overloading}{\hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\

   818   \end{matharray}

   819

   820   \begin{rail}

   821     'overloading' \\

   822     ( string ( '==' | equiv ) term ( '(' 'unchecked' ')' )? + ) 'begin'

   823   \end{rail}

   824

   825   \begin{description}

   826

   827   \item \hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymequiv}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\isactrlsub {\isadigit{1}}\ {\isasymAND}\ {\isasymdots}\ x\isactrlsub n\ {\isasymequiv}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\isactrlsub n\ {\isasymBEGIN}{\isachardoublequote}}

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

   829   specify constants with overloaded definitions.  These are identified

   830   by an explicitly given mapping from variable names \isa{{\isachardoublequote}x\isactrlsub i{\isachardoublequote}} to

   831   constants \isa{{\isachardoublequote}c\isactrlsub i{\isachardoublequote}} at particular type instances.  The

   832   definitions themselves are established using common specification

   833   tools, using the names \isa{{\isachardoublequote}x\isactrlsub i{\isachardoublequote}} as reference to the

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

   835

   836   A \isa{{\isachardoublequote}{\isacharparenleft}unchecked{\isacharparenright}{\isachardoublequote}} option disables global dependency checks for

   837   the corresponding definition, which is occasionally useful for

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

   839   It is at the discretion of the user to avoid

   840   malformed theory specifications!

   841

   842   \end{description}%

   843 \end{isamarkuptext}%

   844 \isamarkuptrue%

   845 %

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

   847 }

   848 \isamarkuptrue%

   849 %

   850 \begin{isamarkuptext}%

   851 \begin{matharray}{rcl}

   852     \indexdef{}{command}{use}\hypertarget{command.use}{\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\

   853     \indexdef{}{command}{ML}\hypertarget{command.ML}{\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\

   854     \indexdef{}{command}{ML\_prf}\hypertarget{command.ML-prf}{\hyperlink{command.ML-prf}{\mbox{\isa{\isacommand{ML{\isacharunderscore}prf}}}}} & : & \isa{{\isachardoublequote}proof\ {\isasymrightarrow}\ proof{\isachardoublequote}} \\

   855     \indexdef{}{command}{ML\_val}\hypertarget{command.ML-val}{\hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\

   856     \indexdef{}{command}{ML\_command}\hypertarget{command.ML-command}{\hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\

   857     \indexdef{}{command}{setup}\hypertarget{command.setup}{\hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\

   858     \indexdef{}{command}{local\_setup}\hypertarget{command.local-setup}{\hyperlink{command.local-setup}{\mbox{\isa{\isacommand{local{\isacharunderscore}setup}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\

   859     \indexdef{}{command}{attribute\_setup}\hypertarget{command.attribute-setup}{\hyperlink{command.attribute-setup}{\mbox{\isa{\isacommand{attribute{\isacharunderscore}setup}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\

   860   \end{matharray}

   861

   862   \begin{rail}

   863     'use' name

   864     ;

   865     ('ML' | 'ML_prf' | 'ML_val' | 'ML_command' | 'setup' | 'local_setup') text

   866     ;

   867     'attribute_setup' name '=' text text

   868     ;

   869   \end{rail}

   870

   871   \begin{description}

   872

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

   874   commands from \isa{{\isachardoublequote}file{\isachardoublequote}}.  The current theory context is passed

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

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

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

   878

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

   880   context.

   881

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

   883   but executes ML commands directly from the given \isa{{\isachardoublequote}text{\isachardoublequote}}.

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

   885   context.

   886

   887   \item \hyperlink{command.ML-prf}{\mbox{\isa{\isacommand{ML{\isacharunderscore}prf}}}} is analogous to \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}} but works

   888   within a proof context.

   889

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

   891   purely sequential fashion, disregarding the nested proof structure.

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

   893   end of the proof.

   894

   895   \item \hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} and \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}} are diagnostic

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

   897   updated.  \hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} echos the bindings produced at the ML

   898   toplevel, but \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}} is silent.

   899

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

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

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

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

   904   example.

   905

   906   \item \hyperlink{command.local-setup}{\mbox{\isa{\isacommand{local{\isacharunderscore}setup}}}} is similar to \hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}} for

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

   908   invoke local theory specification packages without going through

   909   concrete outer syntax, for example.

   910

   911   \item \hyperlink{command.attribute-setup}{\mbox{\isa{\isacommand{attribute{\isacharunderscore}setup}}}}~\isa{{\isachardoublequote}name\ {\isacharequal}\ text\ description{\isachardoublequote}}

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

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

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

   915

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

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

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

   919

   920   \end{description}%

   921 \end{isamarkuptext}%

   922 \isamarkuptrue%

   923 %

   924 \isadelimML

   925 \ \ \ \ %

   926 \endisadelimML

   927 %

   928 \isatagML

   929 \isacommand{attribute{\isacharunderscore}setup}\isamarkupfalse%

   930 \ my{\isacharunderscore}rule\ {\isacharequal}\ {\isacharverbatimopen}\isanewline

   931 \ \ \ \ \ \ Attrib{\isachardot}thms\ {\isachargreater}{\isachargreater}\ {\isacharparenleft}fn\ ths\ {\isacharequal}{\isachargreater}\isanewline

   932 \ \ \ \ \ \ \ \ Thm{\isachardot}rule{\isacharunderscore}attribute\ {\isacharparenleft}fn\ context{\isacharcolon}\ Context{\isachardot}generic\ {\isacharequal}{\isachargreater}\ fn\ th{\isacharcolon}\ thm\ {\isacharequal}{\isachargreater}\isanewline

   933 \ \ \ \ \ \ \ \ \ \ let\ val\ th{\isacharprime}\ {\isacharequal}\ th\ OF\ ths\isanewline

   934 \ \ \ \ \ \ \ \ \ \ in\ th{\isacharprime}\ end{\isacharparenright}{\isacharparenright}\ {\isacharverbatimclose}\ \ {\isachardoublequoteopen}my\ rule{\isachardoublequoteclose}\isanewline

   935 \isanewline

   936 \ \ \ \ \isacommand{attribute{\isacharunderscore}setup}\isamarkupfalse%

   937 \ my{\isacharunderscore}declaration\ {\isacharequal}\ {\isacharverbatimopen}\isanewline

   938 \ \ \ \ \ \ Attrib{\isachardot}thms\ {\isachargreater}{\isachargreater}\ {\isacharparenleft}fn\ ths\ {\isacharequal}{\isachargreater}\isanewline

   939 \ \ \ \ \ \ \ \ Thm{\isachardot}declaration{\isacharunderscore}attribute\ {\isacharparenleft}fn\ th{\isacharcolon}\ thm\ {\isacharequal}{\isachargreater}\ fn\ context{\isacharcolon}\ Context{\isachardot}generic\ {\isacharequal}{\isachargreater}\isanewline

   940 \ \ \ \ \ \ \ \ \ \ let\ val\ context{\isacharprime}\ {\isacharequal}\ context\isanewline

   941 \ \ \ \ \ \ \ \ \ \ in\ context{\isacharprime}\ end{\isacharparenright}{\isacharparenright}\ {\isacharverbatimclose}\ \ {\isachardoublequoteopen}my\ declaration{\isachardoublequoteclose}%

   942 \endisatagML

   943 {\isafoldML}%

   944 %

   945 \isadelimML

   946 %

   947 \endisadelimML

   948 %

   949 \isamarkupsection{Primitive specification elements%

   950 }

   951 \isamarkuptrue%

   952 %

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

   954 }

   955 \isamarkuptrue%

   956 %

   957 \begin{isamarkuptext}%

   958 \begin{matharray}{rcll}

   959     \indexdef{}{command}{classes}\hypertarget{command.classes}{\hyperlink{command.classes}{\mbox{\isa{\isacommand{classes}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\

   960     \indexdef{}{command}{classrel}\hypertarget{command.classrel}{\hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\

   961     \indexdef{}{command}{default\_sort}\hypertarget{command.default-sort}{\hyperlink{command.default-sort}{\mbox{\isa{\isacommand{default{\isacharunderscore}sort}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}}

   962   \end{matharray}

   963

   964   \begin{rail}

   965     'classes' (classdecl +)

   966     ;

   967     'classrel' (nameref ('<' | subseteq) nameref + 'and')

   968     ;

   969     'default_sort' sort

   970     ;

   971   \end{rail}

   972

   973   \begin{description}

   974

   975   \item \hyperlink{command.classes}{\mbox{\isa{\isacommand{classes}}}}~\isa{{\isachardoublequote}c\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n{\isachardoublequote}} declares class

   976   \isa{c} to be a subclass of existing classes \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n{\isachardoublequote}}.

   977   Isabelle implicitly maintains the transitive closure of the class

   978   hierarchy.  Cyclic class structures are not permitted.

   979

   980   \item \hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}} states subclass

   981   relations between existing classes \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}{\isachardoublequote}} and \isa{{\isachardoublequote}c\isactrlsub {\isadigit{2}}{\isachardoublequote}}.

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

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

   984   a way to introduce proven class relations.

   985

   986   \item \hyperlink{command.default-sort}{\mbox{\isa{\isacommand{default{\isacharunderscore}sort}}}}~\isa{s} makes sort \isa{s} the

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

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

   989   Type variables generated by type inference are not affected.

   990

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

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

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

   994

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

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

   997   are joined.

   998

   999   \end{description}%

  1000 \end{isamarkuptext}%

  1001 \isamarkuptrue%

  1002 %

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

  1004 }

  1005 \isamarkuptrue%

  1006 %

  1007 \begin{isamarkuptext}%

  1008 \begin{matharray}{rcll}

  1009     \indexdef{}{command}{types}\hypertarget{command.types}{\hyperlink{command.types}{\mbox{\isa{\isacommand{types}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\

  1010     \indexdef{}{command}{typedecl}\hypertarget{command.typedecl}{\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\

  1011     \indexdef{}{command}{arities}\hypertarget{command.arities}{\hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\

  1012   \end{matharray}

  1013

  1014   \begin{rail}

  1015     'types' (typespec '=' type mixfix? +)

  1016     ;

  1017     'typedecl' typespec mixfix?

  1018     ;

  1019     'arities' (nameref '::' arity +)

  1020     ;

  1021   \end{rail}

  1022

  1023   \begin{description}

  1024

  1025   \item \hyperlink{command.types}{\mbox{\isa{\isacommand{types}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t\ {\isacharequal}\ {\isasymtau}{\isachardoublequote}} introduces a

  1026   \emph{type synonym} \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}} for the existing type

  1027   \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}}.  Unlike actual type definitions, as are available in

  1028   Isabelle/HOL for example, type synonyms are merely syntactic

  1029   abbreviations without any logical significance.  Internally, type

  1030   synonyms are fully expanded.

  1031

  1032   \item \hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}} declares a new

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

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

  1035   the axiomatic specification \hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s{\isacharparenright}s{\isachardoublequote}}.

  1036

  1037   \item \hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}s{\isachardoublequote}} augments

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

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

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

  1041   proven type arities.

  1042

  1043   \end{description}%

  1044 \end{isamarkuptext}%

  1045 \isamarkuptrue%

  1046 %

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

  1048 }

  1049 \isamarkuptrue%

  1050 %

  1051 \begin{isamarkuptext}%

  1052 Definitions essentially express abbreviations within the logic.  The

  1053   simplest form of a definition is \isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\ {\isasymequiv}\ t{\isachardoublequote}}, where \isa{c} is a newly declared constant.  Isabelle also allows derived forms

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

  1055   prefix of \isa{{\isasymlambda}}-abstractions, e.g.\ \isa{{\isachardoublequote}c\ {\isasymequiv}\ {\isasymlambda}x\ y{\isachardot}\ t{\isachardoublequote}} may be

  1056   written more conveniently as \isa{{\isachardoublequote}c\ x\ y\ {\isasymequiv}\ t{\isachardoublequote}}.  Moreover,

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

  1058   \isa{{\isachardoublequote}A\ {\isasymLongrightarrow}\ c\ x\ y\ {\isasymequiv}\ t{\isachardoublequote}}.

  1059

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

  1061   specifications are:

  1062

  1063   \begin{itemize}

  1064

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

  1066

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

  1068   left-hand side.

  1069

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

  1071   the left-hand side; this prohibits \isa{{\isachardoublequote}{\isadigit{0}}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymequiv}\ length\ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ list{\isacharparenright}{\isachardoublequote}} for example.

  1072

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

  1074   provide definitional principles that can be used to express

  1075   recursion safely.

  1076

  1077   \end{itemize}

  1078

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

  1080   recursively at type instances corresponding to the immediate

  1081   argument types \isa{{\isachardoublequote}{\isasymbeta}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymbeta}\isactrlsub n{\isachardoublequote}}.  Incomplete

  1082   specification patterns impose global constraints on all occurrences,

  1083   e.g.\ \isa{{\isachardoublequote}d\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymtimes}\ {\isasymalpha}{\isachardoublequote}} on the left-hand side means that all

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

  1085   instance of this, general \isa{{\isachardoublequote}d\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymtimes}\ {\isasymbeta}{\isachardoublequote}} will be disallowed.

  1086

  1087   \begin{matharray}{rcl}

  1088     \indexdef{}{command}{consts}\hypertarget{command.consts}{\hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\

  1089     \indexdef{}{command}{defs}\hypertarget{command.defs}{\hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\

  1090   \end{matharray}

  1091

  1092   \begin{rail}

  1093     'consts' ((name '::' type mixfix?) +)

  1094     ;

  1095     'defs' ('(' 'unchecked'? 'overloaded'? ')')? \\ (axmdecl prop +)

  1096     ;

  1097   \end{rail}

  1098

  1099   \begin{description}

  1100

  1101   \item \hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}~\isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}{\isachardoublequote}} declares constant \isa{c} to have any instance of type scheme \isa{{\isasymsigma}}.  The optional

  1102   mixfix annotations may attach concrete syntax to the constants

  1103   declared.

  1104

  1105   \item \hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}}~\isa{{\isachardoublequote}name{\isacharcolon}\ eqn{\isachardoublequote}} introduces \isa{eqn}

  1106   as a definitional axiom for some existing constant.

  1107

  1108   The \isa{{\isachardoublequote}{\isacharparenleft}unchecked{\isacharparenright}{\isachardoublequote}} option disables global dependency checks

  1109   for this definition, which is occasionally useful for exotic

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

  1111   theory specifications!

  1112

  1113   The \isa{{\isachardoublequote}{\isacharparenleft}overloaded{\isacharparenright}{\isachardoublequote}} option declares definitions to be

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

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

  1116   special type than that of the corresponding constant declaration.

  1117

  1118   \end{description}%

  1119 \end{isamarkuptext}%

  1120 \isamarkuptrue%

  1121 %

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

  1123 }

  1124 \isamarkuptrue%

  1125 %

  1126 \begin{isamarkuptext}%

  1127 \begin{matharray}{rcll}

  1128     \indexdef{}{command}{axioms}\hypertarget{command.axioms}{\hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\

  1129     \indexdef{}{command}{lemmas}\hypertarget{command.lemmas}{\hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\

  1130     \indexdef{}{command}{theorems}\hypertarget{command.theorems}{\hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\

  1131   \end{matharray}

  1132

  1133   \begin{rail}

  1134     'axioms' (axmdecl prop +)

  1135     ;

  1136     ('lemmas' | 'theorems') target? (thmdef? thmrefs + 'and')

  1137     ;

  1138   \end{rail}

  1139

  1140   \begin{description}

  1141

  1142   \item \hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} introduces arbitrary

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

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

  1145   theorem.

  1146

  1147   Axioms are usually only introduced when declaring new logical

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

  1149   definitions and proven theorems.

  1150

  1151   \item \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}~\isa{{\isachardoublequote}a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}} retrieves and stores

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

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

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

  1155

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

  1157

  1158   \end{description}%

  1159 \end{isamarkuptext}%

  1160 \isamarkuptrue%

  1161 %

  1162 \isamarkupsection{Oracles%

  1163 }

  1164 \isamarkuptrue%

  1165 %

  1166 \begin{isamarkuptext}%

  1167 Oracles allow Isabelle to take advantage of external reasoners

  1168   such as arithmetic decision procedures, model checkers, fast

  1169   tautology checkers or computer algebra systems.  Invoked as an

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

  1171

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

  1173   reasoner is as trustworthy as the application requires.  Another

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

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

  1176   required translation between two different logical environments.

  1177

  1178   Isabelle merely guarantees well-formedness of the propositions being

  1179   asserted, and records within the internal derivation object how

  1180   presumed theorems depend on unproven suppositions.

  1181

  1182   \begin{matharray}{rcll}

  1183     \indexdef{}{command}{oracle}\hypertarget{command.oracle}{\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\

  1184   \end{matharray}

  1185

  1186   \begin{rail}

  1187     'oracle' name '=' text

  1188     ;

  1189   \end{rail}

  1190

  1191   \begin{description}

  1192

  1193   \item \hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}~\isa{{\isachardoublequote}name\ {\isacharequal}\ text{\isachardoublequote}} turns the given ML

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

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

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

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

  1198   scope of the resulting theory.

  1199

  1200   \end{description}

  1201

  1202   See \hyperlink{file.~~/src/HOL/ex/Iff-Oracle.thy}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}HOL{\isacharslash}ex{\isacharslash}Iff{\isacharunderscore}Oracle{\isachardot}thy}}}} for a worked example of

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

  1204   method.%

  1205 \end{isamarkuptext}%

  1206 \isamarkuptrue%

  1207 %

  1208 \isamarkupsection{Name spaces%

  1209 }

  1210 \isamarkuptrue%

  1211 %

  1212 \begin{isamarkuptext}%

  1213 \begin{matharray}{rcl}

  1214     \indexdef{}{command}{hide\_class}\hypertarget{command.hide-class}{\hyperlink{command.hide-class}{\mbox{\isa{\isacommand{hide{\isacharunderscore}class}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\

  1215     \indexdef{}{command}{hide\_type}\hypertarget{command.hide-type}{\hyperlink{command.hide-type}{\mbox{\isa{\isacommand{hide{\isacharunderscore}type}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\

  1216     \indexdef{}{command}{hide\_const}\hypertarget{command.hide-const}{\hyperlink{command.hide-const}{\mbox{\isa{\isacommand{hide{\isacharunderscore}const}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\

  1217     \indexdef{}{command}{hide\_fact}\hypertarget{command.hide-fact}{\hyperlink{command.hide-fact}{\mbox{\isa{\isacommand{hide{\isacharunderscore}fact}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\

  1218   \end{matharray}

  1219

  1220   \begin{rail}

  1221     ( 'hide_class' | 'hide_type' | 'hide_const' | 'hide_fact' ) ('(open)')? (nameref + )

  1222     ;

  1223   \end{rail}

  1224

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

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

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

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

  1229   do so.

  1230

  1231   \begin{description}

  1232

  1233   \item \hyperlink{command.hide-class}{\mbox{\isa{\isacommand{hide{\isacharunderscore}class}}}}~\isa{names} fully removes class

  1234   declarations from a given name space; with the \isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}}

  1235   option, only the base name is hidden.

  1236

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

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

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

  1240   \isa{{\isachardoublequote}{\isacharquery}{\isacharquery}{\isachardoublequote}}'' prefixed to the full internal name.

  1241

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

  1243   constants, and facts, respectively.

  1244

  1245   \end{description}%

  1246 \end{isamarkuptext}%

  1247 \isamarkuptrue%

  1248 %

  1249 \isadelimtheory

  1250 %

  1251 \endisadelimtheory

  1252 %

  1253 \isatagtheory

  1254 \isacommand{end}\isamarkupfalse%

  1255 %

  1256 \endisatagtheory

  1257 {\isafoldtheory}%

  1258 %

  1259 \isadelimtheory

  1260 %

  1261 \endisadelimtheory

  1262 \isanewline

  1263 \end{isabellebody}%

  1264 %%% Local Variables:

  1265 %%% mode: latex

  1266 %%% TeX-master: "root"

  1267 %%% End:
`