doc-src/IsarRef/Thy/document/Spec.tex
 author wenzelm Tue Jun 03 00:03:54 2008 +0200 (2008-06-03) changeset 27054 f1ef0973d0a8 parent 27052 5c48cecb981b child 27057 ecbe1afe800b permissions -rw-r--r--
updated generated file;
     1 %

     2 \begin{isabellebody}%

     3 \def\isabellecontext{Spec}%

     4 %

     5 \isadelimtheory

     6 \isanewline

     7 \isanewline

     8 %

     9 \endisadelimtheory

    10 %

    11 \isatagtheory

    12 \isacommand{theory}\isamarkupfalse%

    13 \ Spec\isanewline

    14 \isakeyword{imports}\ Main\isanewline

    15 \isakeyword{begin}%

    16 \endisatagtheory

    17 {\isafoldtheory}%

    18 %

    19 \isadelimtheory

    20 %

    21 \endisadelimtheory

    22 %

    23 \isamarkupchapter{Theory specifications%

    24 }

    25 \isamarkuptrue%

    26 %

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

    28 }

    29 \isamarkuptrue%

    30 %

    31 \begin{isamarkuptext}%

    32 \begin{matharray}{rcl}

    33     \indexdef{}{command}{theory}\hypertarget{command.theory}{\hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}}} & : & \isartrans{toplevel}{theory} \\

    34     \indexdef{global}{command}{end}\hypertarget{command.global.end}{\hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}}} & : & \isartrans{theory}{toplevel} \\

    35   \end{matharray}

    36

    37   Isabelle/Isar theories are defined via theory file, which contain

    38   both specifications and proofs; occasionally definitional mechanisms

    39   also require some explicit proof.  The theory body may be

    40   sub-structered by means of \emph{local theory} target mechanisms,

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

    42

    43   The first real'' command of any theory has to be \hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}}, which starts a new theory based on the merge of existing

    44   ones.  Just preceding the \hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}} keyword, there may be

    45   an optional \hyperlink{command.header}{\mbox{\isa{\isacommand{header}}}} declaration, which is relevant to

    46   document preparation only; it acts very much like a special

    47   pre-theory markup command (cf.\ \secref{sec:markup}).  The \hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}} command concludes a theory development; it has to be

    48   the very last command of any theory file loaded in batch-mode.

    49

    50   \begin{rail}

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

    52     ;

    53

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

    55   \end{rail}

    56

    57   \begin{descr}

    58

    59   \item [\hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}}~\isa{{\isachardoublequote}A\ {\isasymIMPORTS}\ B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n\ {\isasymBEGIN}{\isachardoublequote}}] starts a new theory \isa{A} based on the

    60   merge of existing theories \isa{{\isachardoublequote}B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n{\isachardoublequote}}.

    61

    62   Due to inclusion of several ancestors, the overall theory structure

    63   emerging in an Isabelle session forms a directed acyclic graph

    64   (DAG).  Isabelle's theory loader ensures that the sources

    65   contributing to the development graph are always up-to-date.

    66   Changed files are automatically reloaded when processing theory

    67   headers.

    68

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

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

    71   loaded immediately (as ML), unless the name is put in parentheses,

    72   which merely documents the dependency to be resolved later in the

    73   text (typically via explicit \indexref{}{command}{use}\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}} in the body text,

    74   see \secref{sec:ML}).

    75

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

    77   definition.

    78

    79   \end{descr}%

    80 \end{isamarkuptext}%

    81 \isamarkuptrue%

    82 %

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

    84 }

    85 \isamarkuptrue%

    86 %

    87 \begin{isamarkuptext}%

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

    89   enclosing theory.  Contexts may introduce parameters (fixed

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

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

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

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

    94   global theory context.

    95

    96   \begin{matharray}{rcll}

    97     \indexdef{}{command}{context}\hypertarget{command.context}{\hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}} & : & \isartrans{theory}{local{\dsh}theory} \\

    98     \indexdef{local}{command}{end}\hypertarget{command.local.end}{\hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}}} & : & \isartrans{local{\dsh}theory}{theory} \\

    99   \end{matharray}

   100

   101   \indexouternonterm{target}

   102   \begin{rail}

   103     'context' name 'begin'

   104     ;

   105

   106     target: '(' 'in' name ')'

   107     ;

   108   \end{rail}

   109

   110   \begin{descr}

   111

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

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

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

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

   116   initial specification.

   117

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

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

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

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

   122

   123   \item [\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}{\isachardoublequote}}] given after any local theory command

   124   specifies an immediate target, e.g.\ \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}\ {\isasymdots}{\isachardoublequote}}'' or \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}\ {\isasymdots}{\isachardoublequote}}''.  This works both in a local or

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

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

   127   always produce a global result independently of the current target

   128   context.

   129

   130   \end{descr}

   131

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

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

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

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

   136

   137   Definitions are exported by introducing a global version with

   138   additional arguments; a syntactic abbreviation links the long form

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

   140   \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

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

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

   143   fixed parameter \isa{x}).

   144

   145   Theorems are exported by discharging the assumptions and

   146   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

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

   148 \end{isamarkuptext}%

   149 \isamarkuptrue%

   150 %

   151 \isamarkupsection{Basic specification elements%

   152 }

   153 \isamarkuptrue%

   154 %

   155 \begin{isamarkuptext}%

   156 \begin{matharray}{rcll}

   157     \indexdef{}{command}{axiomatization}\hypertarget{command.axiomatization}{\hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{axiomatization}}}}} & : & \isarkeep{local{\dsh}theory} & (axiomatic!)\\

   158     \indexdef{}{command}{definition}\hypertarget{command.definition}{\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}} & : & \isarkeep{local{\dsh}theory} \\

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

   160     \indexdef{}{command}{abbreviation}\hypertarget{command.abbreviation}{\hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}} & : & \isarkeep{local{\dsh}theory} \\

   161     \indexdef{}{command}{print\_abbrevs}\hypertarget{command.print-abbrevs}{\hyperlink{command.print-abbrevs}{\mbox{\isa{\isacommand{print{\isacharunderscore}abbrevs}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\

   162     \indexdef{}{command}{notation}\hypertarget{command.notation}{\hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}} & : & \isarkeep{local{\dsh}theory} \\

   163     \indexdef{}{command}{no\_notation}\hypertarget{command.no-notation}{\hyperlink{command.no-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}}}} & : & \isarkeep{local{\dsh}theory} \\

   164   \end{matharray}

   165

   166   These specification mechanisms provide a slightly more abstract view

   167   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

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

   169   available, and result names need not be given.

   170

   171   \begin{rail}

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

   173     ;

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

   175     ;

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

   177     ;

   178     ('notation' | 'no\_notation') target? mode? (nameref structmixfix + 'and')

   179     ;

   180

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

   182     ;

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

   184     ;

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

   186     ;

   187   \end{rail}

   188

   189   \begin{descr}

   190

   191   \item [\hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{axiomatization}}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymdots}\ c\isactrlsub m\ {\isasymWHERE}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}] introduces several constants

   192   simultaneously and states axiomatic properties for these.  The

   193   constants are marked as being specified once and for all, which

   194   prevents additional specifications being issued later on.

   195

   196   Note that axiomatic specifications are only appropriate when

   197   declaring a new logical system.  Normal applications should only use

   198   definitional mechanisms!

   199

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

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

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

   203   given proposition may deviate from internal meta-level equality

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

   205   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

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

   207

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

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

   210   \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

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

   212

   213   \item [\hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}~\isa{{\isachardoublequote}c\ {\isasymWHERE}\ eq{\isachardoublequote}}] introduces

   214   a syntactic constant which is associated with a certain term

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

   216

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

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

   219   terms involves higher-order rewriting with rules stemming from

   220   reverted abbreviations.  This needs some care to avoid overlapping

   221   or looping syntactic replacements!

   222

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

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

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

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

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

   228   \secref{sec:syn-trans}.

   229

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

   231   of the current context.

   232

   233   \item [\hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}}] associates mixfix

   234   syntax with an existing constant or fixed variable.  This is a

   235   robust interface to the underlying \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} primitive

   236   (\secref{sec:syn-trans}).  Type declaration and internal syntactic

   237   representation of the given entity is retrieved from the context.

   238

   239   \item [\hyperlink{command.no-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}}}] is similar to \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}, but removes the specified syntax annotation from the

   240   present context.

   241

   242   \end{descr}

   243

   244   All of these specifications support local theory targets (cf.\

   245   \secref{sec:target}).%

   246 \end{isamarkuptext}%

   247 \isamarkuptrue%

   248 %

   249 \isamarkupsection{Generic declarations%

   250 }

   251 \isamarkuptrue%

   252 %

   253 \begin{isamarkuptext}%

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

   255   generic declaration elements.  Since the underlying concept of local

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

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

   258   original declaration context wrt.\ the application context

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

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

   261   means of an attribute.

   262

   263   \begin{matharray}{rcl}

   264     \indexdef{}{command}{declaration}\hypertarget{command.declaration}{\hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}} & : & \isarkeep{local{\dsh}theory} \\

   265     \indexdef{}{command}{declare}\hypertarget{command.declare}{\hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}}} & : & \isarkeep{local{\dsh}theory} \\

   266   \end{matharray}

   267

   268   \begin{rail}

   269     'declaration' target? text

   270     ;

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

   272     ;

   273   \end{rail}

   274

   275   \begin{descr}

   276

   277   \item [\hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}~\isa{d}] adds the declaration

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

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

   280   function is transformed according to the morphisms being involved in

   281   the interpretation hierarchy.

   282

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

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

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

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

   287   of applying attributes as included in the theorem specification.

   288

   289   \end{descr}%

   290 \end{isamarkuptext}%

   291 \isamarkuptrue%

   292 %

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

   294 }

   295 \isamarkuptrue%

   296 %

   297 \begin{isamarkuptext}%

   298 Locales are named local contexts, consisting of a list of

   299   declaration elements that are modeled after the Isar proof context

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

   301 \end{isamarkuptext}%

   302 \isamarkuptrue%

   303 %

   304 \isamarkupsubsection{Locale specifications%

   305 }

   306 \isamarkuptrue%

   307 %

   308 \begin{isamarkuptext}%

   309 \begin{matharray}{rcl}

   310     \indexdef{}{command}{locale}\hypertarget{command.locale}{\hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}} & : & \isartrans{theory}{local{\dsh}theory} \\

   311     \indexdef{}{command}{print\_locale}\hypertarget{command.print-locale}{\hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\

   312     \indexdef{}{command}{print\_locales}\hypertarget{command.print-locales}{\hyperlink{command.print-locales}{\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\

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

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

   315   \end{matharray}

   316

   317   \indexouternonterm{contextexpr}\indexouternonterm{contextelem}

   318   \indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes}

   319   \indexisarelem{defines}\indexisarelem{notes}\indexisarelem{includes}

   320   \begin{rail}

   321     'locale' ('(open)')? name ('=' localeexpr)? 'begin'?

   322     ;

   323     'print\_locale' '!'? localeexpr

   324     ;

   325     localeexpr: ((contextexpr '+' (contextelem+)) | contextexpr | (contextelem+))

   326     ;

   327

   328     contextexpr: nameref | '(' contextexpr ')' |

   329     (contextexpr (name mixfix? +)) | (contextexpr + '+')

   330     ;

   331     contextelem: fixes | constrains | assumes | defines | notes

   332     ;

   333     fixes: 'fixes' ((name ('::' type)? structmixfix? | vars) + 'and')

   334     ;

   335     constrains: 'constrains' (name '::' type + 'and')

   336     ;

   337     assumes: 'assumes' (thmdecl? props + 'and')

   338     ;

   339     defines: 'defines' (thmdecl? prop proppat? + 'and')

   340     ;

   341     notes: 'notes' (thmdef? thmrefs + 'and')

   342     ;

   343     includes: 'includes' contextexpr

   344     ;

   345   \end{rail}

   346

   347   \begin{descr}

   348

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

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

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

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

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

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

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

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

   357   may acquire.

   358

   359   The \isa{import} consists of a structured context expression,

   360   consisting of references to existing locales, renamed contexts, or

   361   merged contexts.  Renaming uses positional notation: \isa{{\isachardoublequote}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n{\isachardoublequote}} means that (a prefix of) the fixed

   362   parameters of context \isa{c} are named \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub n{\isachardoublequote}}; a \isa{{\isacharunderscore}}'' (underscore) means to skip that

   363   position.  Renaming by default deletes concrete syntax, but new

   364   syntax may by specified with a mixfix annotation.  An exeption of

   365   this rule is the special syntax declared with \isa{{\isachardoublequote}{\isacharparenleft}{\isasymSTRUCTURE}{\isacharparenright}{\isachardoublequote}}'' (see below), which is neither deleted nor can it

   366   be changed.  Merging proceeds from left-to-right, suppressing any

   367   duplicates stemming from different paths through the import

   368   hierarchy.

   369

   370   The \isa{body} consists of basic context elements, further context

   371   expressions may be included as well.

   372

   373   \begin{descr}

   374

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

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

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

   378   implicitly in this context.

   379

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

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

   382

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

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

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

   386

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

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

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

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

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

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

   393

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

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

   396   include arbitrary declarations in any attribute specifications

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

   398

   399   \item [\hyperlink{element.includes}{\mbox{\isa{\isakeyword{includes}}}}~\isa{c}] copies the specified context

   400   in a statically scoped manner.  Only available in the long goal

   401   format of \secref{sec:goals}.

   402

   403   In contrast, the initial \isa{import} specification of a locale

   404   expression maintains a dynamic relation to the locales being

   405   referenced (benefiting from any later fact declarations in the

   406   obvious manner).

   407

   408   \end{descr}

   409

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

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

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

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

   414   though.

   415

   416   \medskip By default, locale specifications are closed up'' by

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

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

   419   newly specified assumptions, omitting the content of included locale

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

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

   422   specification text.

   423

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

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

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

   427   packages attempts to internalize statements according to the

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

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

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

   431

   432   The \isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}} option of a locale specification prevents both

   433   the current \isa{loc{\isacharunderscore}axioms} and cumulative \isa{loc} predicate

   434   constructions.  Predicates are also omitted for empty specification

   435   texts.

   436

   437   \item [\hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{{\isachardoublequote}import\ {\isacharplus}\ body{\isachardoublequote}}] prints the

   438   specified locale expression in a flattened form.  The notable

   439   special case \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{loc} just prints the

   440   contents of the named locale, but keep in mind that type-inference

   441   will normalize type variables according to the usual alphabetical

   442   order.  The command omits \hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}} elements by default.

   443   Use \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}} to get them included.

   444

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

   446   of the current theory.

   447

   448   \item [\hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}} and \hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}}]

   449   repeatedly expand all introduction rules of locale predicates of the

   450   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

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

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

   453   specifications entailed by the context, both from target and

   454   \hyperlink{element.includes}{\mbox{\isa{\isakeyword{includes}}}} statements, and from interpretations (see

   455   below).  New goals that are entailed by the current context are

   456   discharged automatically.

   457

   458   \end{descr}%

   459 \end{isamarkuptext}%

   460 \isamarkuptrue%

   461 %

   462 \isamarkupsubsection{Interpretation of locales%

   463 }

   464 \isamarkuptrue%

   465 %

   466 \begin{isamarkuptext}%

   467 Locale expressions (more precisely, \emph{context expressions}) may

   468   be instantiated, and the instantiated facts added to the current

   469   context.  This requires a proof of the instantiated specification

   470   and is called \emph{locale interpretation}.  Interpretation is

   471   possible in theories and locales (command \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}) and also within a proof body (command \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}).

   472

   473   \begin{matharray}{rcl}

   474     \indexdef{}{command}{interpretation}\hypertarget{command.interpretation}{\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}} & : & \isartrans{theory}{proof(prove)} \\

   475     \indexdef{}{command}{interpret}\hypertarget{command.interpret}{\hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\

   476     \indexdef{}{command}{print\_interps}\hypertarget{command.print-interps}{\hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : &  \isarkeep{theory~|~proof} \\

   477   \end{matharray}

   478

   479   \indexouternonterm{interp}

   480   \begin{rail}

   481     'interpretation' (interp | name ('<' | subseteq) contextexpr)

   482     ;

   483     'interpret' interp

   484     ;

   485     'print\_interps' '!'? name

   486     ;

   487     instantiation: ('[' (inst+) ']')?

   488     ;

   489     interp: thmdecl? \\ (contextexpr instantiation |

   490       name instantiation 'where' (thmdecl? prop + 'and'))

   491     ;

   492   \end{rail}

   493

   494   \begin{descr}

   495

   496   \item [\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isachardoublequote}expr\ insts\ {\isasymWHERE}\ eqns{\isachardoublequote}}]

   497

   498   The first form of \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}} interprets \isa{expr} in the theory.  The instantiation is given as a list of terms

   499   \isa{insts} and is positional.  All parameters must receive an

   500   instantiation term --- with the exception of defined parameters.

   501   These are, if omitted, derived from the defining equation and other

   502   instantiations.  Use \isa{{\isacharunderscore}}'' to omit an instantiation term.

   503

   504   The command generates proof obligations for the instantiated

   505   specifications (assumes and defines elements).  Once these are

   506   discharged by the user, instantiated facts are added to the theory

   507   in a post-processing phase.

   508

   509   Additional equations, which are unfolded in facts during

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

   511   This is useful for interpreting concepts introduced through

   512   definition specification elements.  The equations must be proved.

   513   Note that if equations are present, the context expression is

   514   restricted to a locale name.

   515

   516   The command is aware of interpretations already active in the

   517   theory.  No proof obligations are generated for those, neither is

   518   post-processing applied to their facts.  This avoids duplication of

   519   interpreted facts, in particular.  Note that, in the case of a

   520   locale with import, parts of the interpretation may already be

   521   active.  The command will only generate proof obligations and

   522   process facts for new parts.

   523

   524   The context expression may be preceded by a name and/or attributes.

   525   These take effect in the post-processing of facts.  The name is used

   526   to prefix fact names, for example to avoid accidental hiding of

   527   other facts.  Attributes are applied after attributes of the

   528   interpreted facts.

   529

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

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

   532   interpretations dynamically participate in any facts added to

   533   locales.

   534

   535   \item [\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isachardoublequote}name\ {\isasymsubseteq}\ expr{\isachardoublequote}}]

   536

   537   This form of the command interprets \isa{expr} in the locale

   538   \isa{name}.  It requires a proof that the specification of \isa{name} implies the specification of \isa{expr}.  As in the

   539   localized version of the theorem command, the proof is in the

   540   context of \isa{name}.  After the proof obligation has been

   541   dischared, the facts of \isa{expr} become part of locale \isa{name} as \emph{derived} context elements and are available when the

   542   context \isa{name} is subsequently entered.  Note that, like

   543   import, this is dynamic: facts added to a locale part of \isa{expr} after interpretation become also available in \isa{name}.

   544   Like facts of renamed context elements, facts obtained by

   545   interpretation may be accessed by prefixing with the parameter

   546   renaming (where the parameters are separated by \isa{{\isacharunderscore}}'').

   547

   548   Unlike interpretation in theories, instantiation is confined to the

   549   renaming of parameters, which may be specified as part of the

   550   context expression \isa{expr}.  Using defined parameters in \isa{name} one may achieve an effect similar to instantiation, though.

   551

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

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

   554   of the import) are considered by interpretation.  This enables

   555   circular interpretations.

   556

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

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

   559   prefix and attributes, although only for fragments of \isa{expr}

   560   that are not interpreted in the theory already.

   561

   562   \item [\hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}~\isa{{\isachardoublequote}expr\ insts\ {\isasymWHERE}\ eqns{\isachardoublequote}}]

   563   interprets \isa{expr} in the proof context and is otherwise

   564   similar to interpretation in theories.

   565

   566   \item [\hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}}~\isa{loc}] prints the

   567   interpretations of a particular locale \isa{loc} that are active

   568   in the current context, either theory or proof context.  The

   569   exclamation point argument triggers printing of \emph{witness}

   570   theorems justifying interpretations.  These are normally omitted

   571   from the output.

   572

   573   \end{descr}

   574

   575   \begin{warn}

   576     Since attributes are applied to interpreted theorems,

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

   578     the Simplifier or Classical Reasoner.  Since the behavior of such

   579     automated reasoning tools is \emph{not} stable under

   580     interpretation morphisms, manual declarations might have to be

   581     issued.

   582   \end{warn}

   583

   584   \begin{warn}

   585     An interpretation in a theory may subsume previous

   586     interpretations.  This happens if the same specification fragment

   587     is interpreted twice and the instantiation of the second

   588     interpretation is more general than the interpretation of the

   589     first.  A warning is issued, since it is likely that these could

   590     have been generalized in the first place.  The locale package does

   591     not attempt to remove subsumed interpretations.

   592   \end{warn}%

   593 \end{isamarkuptext}%

   594 \isamarkuptrue%

   595 %

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

   597 }

   598 \isamarkuptrue%

   599 %

   600 \begin{isamarkuptext}%

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

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

   603   is established which is interpreted logically as axiomatic type

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

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

   606   generality of locales combined with the commodity of type classes

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

   608   tutorial.

   609

   610   \begin{matharray}{rcl}

   611     \indexdef{}{command}{class}\hypertarget{command.class}{\hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}} & : & \isartrans{theory}{local{\dsh}theory} \\

   612     \indexdef{}{command}{instantiation}\hypertarget{command.instantiation}{\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}} & : & \isartrans{theory}{local{\dsh}theory} \\

   613     \indexdef{}{command}{instance}\hypertarget{command.instance}{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}} & : & \isartrans{local{\dsh}theory}{local{\dsh}theory} \\

   614     \indexdef{}{command}{subclass}\hypertarget{command.subclass}{\hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}} & : & \isartrans{local{\dsh}theory}{local{\dsh}theory} \\

   615     \indexdef{}{command}{print\_classes}\hypertarget{command.print-classes}{\hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\

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

   617   \end{matharray}

   618

   619   \begin{rail}

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

   621       'begin'?

   622     ;

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

   624     ;

   625     'instance'

   626     ;

   627     'subclass' target? nameref

   628     ;

   629     'print\_classes'

   630     ;

   631

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

   633     ;

   634   \end{rail}

   635

   636   \begin{descr}

   637

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

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

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

   641

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

   643   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

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

   645

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

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

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

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

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

   651   class membership proofs.

   652

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

   654   \secref{sec:target}) which allows to specify class operations \isa{{\isachardoublequote}f\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ f\isactrlsub n{\isachardoublequote}} corresponding to sort \isa{s} at the

   655   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

   656   in the target body poses a goal stating these type arities.  The

   657   target is concluded by an \indexref{local}{command}{end}\hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}} command.

   658

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

   660   this corresponds nicely to mutual recursive type definitions, e.g.\

   661   in Isabelle/HOL.

   662

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

   664   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

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

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

   667

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

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

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

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

   672

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

   674   theory.

   675

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

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

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

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

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

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

   682

   683   \end{descr}%

   684 \end{isamarkuptext}%

   685 \isamarkuptrue%

   686 %

   687 \isamarkupsubsection{The class target%

   688 }

   689 \isamarkuptrue%

   690 %

   691 \begin{isamarkuptext}%

   692 %FIXME check

   693

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

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

   696   locale target behaviour the following happens.

   697

   698   \begin{itemize}

   699

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

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

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

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

   704

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

   706

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

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

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

   710   needed.

   711

   712   \end{itemize}%

   713 \end{isamarkuptext}%

   714 \isamarkuptrue%

   715 %

   716 \isamarkupsubsection{Old-style axiomatic type classes \label{sec:axclass}%

   717 }

   718 \isamarkuptrue%

   719 %

   720 \begin{isamarkuptext}%

   721 \begin{matharray}{rcl}

   722     \indexdef{}{command}{axclass}\hypertarget{command.axclass}{\hyperlink{command.axclass}{\mbox{\isa{\isacommand{axclass}}}}} & : & \isartrans{theory}{theory} \\

   723     \indexdef{}{command}{instance}\hypertarget{command.instance}{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}} & : & \isartrans{theory}{proof(prove)} \\

   724   \end{matharray}

   725

   726   Axiomatic type classes are Isabelle/Pure's primitive

   727   \emph{definitional} interface to type classes.  For practical

   728   applications, you should consider using classes

   729   (cf.~\secref{sec:classes}) which provide high level interface.

   730

   731   \begin{rail}

   732     'axclass' classdecl (axmdecl prop +)

   733     ;

   734     'instance' (nameref ('<' | subseteq) nameref | nameref '::' arity)

   735     ;

   736   \end{rail}

   737

   738   \begin{descr}

   739

   740   \item [\hyperlink{command.axclass}{\mbox{\isa{\isacommand{axclass}}}}~\isa{{\isachardoublequote}c\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ axms{\isachardoublequote}}] defines an axiomatic type class as the intersection of

   741   existing classes, with additional axioms holding.  Class axioms may

   742   not contain more than one type variable.  The class axioms (with

   743   implicit sort constraints added) are bound to the given names.

   744   Furthermore a class introduction rule is generated (being bound as

   745   \isa{c{\isacharunderscore}class{\isachardot}intro}); this rule is employed by method \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} to support instantiation proofs of this class.

   746

   747   The class axioms'' are stored as theorems according to the given

   748   name specifications, adding \isa{{\isachardoublequote}c{\isacharunderscore}class{\isachardoublequote}} as name space prefix;

   749   the same facts are also stored collectively as \isa{c{\isacharunderscore}class{\isachardot}axioms}.

   750

   751   \item [\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}} and

   752   \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}}]

   753   setup a goal stating a class relation or type arity.  The proof

   754   would usually proceed by \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}, and then establish

   755   the characteristic theorems of the type classes involved.  After

   756   finishing the proof, the theory will be augmented by a type

   757   signature declaration corresponding to the resulting theorem.

   758

   759   \end{descr}%

   760 \end{isamarkuptext}%

   761 \isamarkuptrue%

   762 %

   763 \isamarkupsection{Unrestricted overloading%

   764 }

   765 \isamarkuptrue%

   766 %

   767 \begin{isamarkuptext}%

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

   769   overloading (see \secref{sec:consts}).  At most occassions

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

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

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

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

   774   end-users.

   775

   776   \begin{matharray}{rcl}

   777     \indexdef{}{command}{overloading}\hypertarget{command.overloading}{\hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}}} & : & \isartrans{theory}{local{\dsh}theory} \\

   778   \end{matharray}

   779

   780   \begin{rail}

   781     'overloading' \\

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

   783   \end{rail}

   784

   785   \begin{descr}

   786

   787   \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}}]

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

   789   specify constants with overloaded definitions.  These are identified

   790   by an explicitly given mapping from variable names \isa{{\isachardoublequote}x\isactrlsub i{\isachardoublequote}} to constants \isa{{\isachardoublequote}c\isactrlsub i{\isachardoublequote}} at particular type

   791   instances.  The definitions themselves are established using common

   792   specification tools, using the names \isa{{\isachardoublequote}x\isactrlsub i{\isachardoublequote}} as

   793   reference to the corresponding constants.  The target is concluded

   794   by \hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}}.

   795

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

   797   the corresponding definition, which is occasionally useful for

   798   exotic overloading.  It is at the discretion of the user to avoid

   799   malformed theory specifications!

   800

   801   \end{descr}%

   802 \end{isamarkuptext}%

   803 \isamarkuptrue%

   804 %

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

   806 }

   807 \isamarkuptrue%

   808 %

   809 \begin{isamarkuptext}%

   810 \begin{matharray}{rcl}

   811     \indexdef{}{command}{use}\hypertarget{command.use}{\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}} & : & \isarkeep{theory~|~local{\dsh}theory} \\

   812     \indexdef{}{command}{ML}\hypertarget{command.ML}{\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}} & : & \isarkeep{theory~|~local{\dsh}theory} \\

   813     \indexdef{}{command}{ML\_val}\hypertarget{command.ML-val}{\hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}}} & : & \isartrans{\cdot}{\cdot} \\

   814     \indexdef{}{command}{ML\_command}\hypertarget{command.ML-command}{\hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}}} & : & \isartrans{\cdot}{\cdot} \\

   815     \indexdef{}{command}{setup}\hypertarget{command.setup}{\hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}} & : & \isartrans{theory}{theory} \\

   816     \indexdef{}{command}{method\_setup}\hypertarget{command.method-setup}{\hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isacharunderscore}setup}}}}} & : & \isartrans{theory}{theory} \\

   817   \end{matharray}

   818

   819   \begin{rail}

   820     'use' name

   821     ;

   822     ('ML' | 'ML\_val' | 'ML\_command' | 'setup') text

   823     ;

   824     'method\_setup' name '=' text text

   825     ;

   826   \end{rail}

   827

   828   \begin{descr}

   829

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

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

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

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

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

   835

   836   \item [\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}~\isa{{\isachardoublequote}text{\isachardoublequote}}] is similar to \hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}, but executes ML commands directly from the given \isa{{\isachardoublequote}text{\isachardoublequote}}.

   837

   838   \item [\hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} and \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}}] are

   839   diagnostic versions of \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}, which means that the context

   840   may not be updated.  \hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} echos the bindings produced

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

   842

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

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

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

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

   847   example.

   848

   849   \item [\hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isacharunderscore}setup}}}}~\isa{{\isachardoublequote}name\ {\isacharequal}\ text\ description{\isachardoublequote}}]

   850   defines a proof method in the current theory.  The given \isa{{\isachardoublequote}text{\isachardoublequote}} has to be an ML expression of type \verb|"Args.src ->|\isasep\isanewline%

   851 \verb|  Proof.context -> Proof.method"|.  Parsing concrete method syntax

   852   from \verb|Args.src| input can be quite tedious in general.  The

   853   following simple examples are for methods without any explicit

   854   arguments, or a list of theorems, respectively.

   855

   856 %FIXME proper antiquotations

   857 {\footnotesize

   858 \begin{verbatim}

   859  Method.no_args (Method.METHOD (fn facts => foobar_tac))

   860  Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac))

   861  Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac))

   862  Method.thms_ctxt_args (fn thms => fn ctxt =>

   863     Method.METHOD (fn facts => foobar_tac))

   864 \end{verbatim}

   865 }

   866

   867   Note that mere tactic emulations may ignore the \isa{facts}

   868   parameter above.  Proper proof methods would do something

   869   appropriate with the list of current facts, though.  Single-rule

   870   methods usually do strict forward-chaining (e.g.\ by using \verb|Drule.multi_resolves|), while automatic ones just insert the facts

   871   using \verb|Method.insert_tac| before applying the main tactic.

   872

   873   \end{descr}%

   874 \end{isamarkuptext}%

   875 \isamarkuptrue%

   876 %

   877 \isamarkupsection{Primitive specification elements%

   878 }

   879 \isamarkuptrue%

   880 %

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

   882 }

   883 \isamarkuptrue%

   884 %

   885 \begin{isamarkuptext}%

   886 \begin{matharray}{rcll}

   887     \indexdef{}{command}{classes}\hypertarget{command.classes}{\hyperlink{command.classes}{\mbox{\isa{\isacommand{classes}}}}} & : & \isartrans{theory}{theory} \\

   888     \indexdef{}{command}{classrel}\hypertarget{command.classrel}{\hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}} & : & \isartrans{theory}{theory} & (axiomatic!) \\

   889     \indexdef{}{command}{defaultsort}\hypertarget{command.defaultsort}{\hyperlink{command.defaultsort}{\mbox{\isa{\isacommand{defaultsort}}}}} & : & \isartrans{theory}{theory} \\

   890     \indexdef{}{command}{class\_deps}\hypertarget{command.class-deps}{\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}}} & : & \isarkeep{theory~|~proof} \\

   891   \end{matharray}

   892

   893   \begin{rail}

   894     'classes' (classdecl +)

   895     ;

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

   897     ;

   898     'defaultsort' sort

   899     ;

   900   \end{rail}

   901

   902   \begin{descr}

   903

   904   \item [\hyperlink{command.classes}{\mbox{\isa{\isacommand{classes}}}}~\isa{{\isachardoublequote}c\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n{\isachardoublequote}}]

   905   declares class \isa{c} to be a subclass of existing classes \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n{\isachardoublequote}}.  Cyclic class structures are not permitted.

   906

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

   908   subclass relations between existing classes \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}{\isachardoublequote}} and

   909   \isa{{\isachardoublequote}c\isactrlsub {\isadigit{2}}{\isachardoublequote}}.  This is done axiomatically!  The \indexref{}{command}{instance}\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} command (see \secref{sec:axclass}) provides a way to

   910   introduce proven class relations.

   911

   912   \item [\hyperlink{command.defaultsort}{\mbox{\isa{\isacommand{defaultsort}}}}~\isa{s}] makes sort \isa{s} the

   913   new default sort for any type variables given without sort

   914   constraints.  Usually, the default sort would be only changed when

   915   defining a new object-logic.

   916

   917   \item [\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}}] visualizes the subclass relation,

   918   using Isabelle's graph browser tool (see also \cite{isabelle-sys}).

   919

   920   \end{descr}%

   921 \end{isamarkuptext}%

   922 \isamarkuptrue%

   923 %

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

   925 }

   926 \isamarkuptrue%

   927 %

   928 \begin{isamarkuptext}%

   929 \begin{matharray}{rcll}

   930     \indexdef{}{command}{types}\hypertarget{command.types}{\hyperlink{command.types}{\mbox{\isa{\isacommand{types}}}}} & : & \isartrans{theory}{theory} \\

   931     \indexdef{}{command}{typedecl}\hypertarget{command.typedecl}{\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}} & : & \isartrans{theory}{theory} \\

   932     \indexdef{}{command}{nonterminals}\hypertarget{command.nonterminals}{\hyperlink{command.nonterminals}{\mbox{\isa{\isacommand{nonterminals}}}}} & : & \isartrans{theory}{theory} \\

   933     \indexdef{}{command}{arities}\hypertarget{command.arities}{\hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}} & : & \isartrans{theory}{theory} & (axiomatic!) \\

   934   \end{matharray}

   935

   936   \begin{rail}

   937     'types' (typespec '=' type infix? +)

   938     ;

   939     'typedecl' typespec infix?

   940     ;

   941     'nonterminals' (name +)

   942     ;

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

   944     ;

   945   \end{rail}

   946

   947   \begin{descr}

   948

   949   \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}}]

   950   introduces \emph{type synonym} \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}}

   951   for existing type \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}}.  Unlike actual type definitions, as

   952   are available in Isabelle/HOL for example, type synonyms are just

   953   purely syntactic abbreviations without any logical significance.

   954   Internally, type synonyms are fully expanded.

   955

   956   \item [\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}}]

   957   declares a new type constructor \isa{t}, intended as an actual

   958   logical type (of the object-logic, if available).

   959

   960   \item [\hyperlink{command.nonterminals}{\mbox{\isa{\isacommand{nonterminals}}}}~\isa{c}] declares type

   961   constructors \isa{c} (without arguments) to act as purely

   962   syntactic types, i.e.\ nonterminal symbols of Isabelle's inner

   963   syntax of terms or types.

   964

   965   \item [\hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}\ s{\isachardoublequote}}] augments Isabelle's order-sorted signature of types by new type

   966   constructor arities.  This is done axiomatically!  The \indexref{}{command}{instance}\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} command (see \S\ref{sec:axclass}) provides a way to

   967   introduce proven type arities.

   968

   969   \end{descr}%

   970 \end{isamarkuptext}%

   971 \isamarkuptrue%

   972 %

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

   974 }

   975 \isamarkuptrue%

   976 %

   977 \begin{isamarkuptext}%

   978 Definitions essentially express abbreviations within the logic.  The

   979   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

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

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

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

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

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

   985

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

   987   specifications are:

   988

   989   \begin{itemize}

   990

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

   992

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

   994   left-hand side.

   995

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

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

   998

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

  1000   provide definitional principles that can be used to express

  1001   recursion safely.

  1002

  1003   \end{itemize}

  1004

  1005   Overloading means that a constant being declared as \isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ decl{\isachardoublequote}} may be defined separately on type instances \isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}{\isasymbeta}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymbeta}\isactrlsub n{\isacharparenright}\ t\ decl{\isachardoublequote}} for each type constructor \isa{t}.  The right-hand side may mention overloaded constants

  1006   recursively at type instances corresponding to the immediate

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

  1008   specification patterns impose global constraints on all occurrences,

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

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

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

  1012

  1013   \begin{matharray}{rcl}

  1014     \indexdef{}{command}{consts}\hypertarget{command.consts}{\hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}} & : & \isartrans{theory}{theory} \\

  1015     \indexdef{}{command}{defs}\hypertarget{command.defs}{\hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}}} & : & \isartrans{theory}{theory} \\

  1016     \indexdef{}{command}{constdefs}\hypertarget{command.constdefs}{\hyperlink{command.constdefs}{\mbox{\isa{\isacommand{constdefs}}}}} & : & \isartrans{theory}{theory} \\

  1017   \end{matharray}

  1018

  1019   \begin{rail}

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

  1021     ;

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

  1023     ;

  1024   \end{rail}

  1025

  1026   \begin{rail}

  1027     'constdefs' structs? (constdecl? constdef +)

  1028     ;

  1029

  1030     structs: '(' 'structure' (vars + 'and') ')'

  1031     ;

  1032     constdecl:  ((name '::' type mixfix | name '::' type | name mixfix) 'where'?) | name 'where'

  1033     ;

  1034     constdef: thmdecl? prop

  1035     ;

  1036   \end{rail}

  1037

  1038   \begin{descr}

  1039

  1040   \item [\hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}~\isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}{\isachardoublequote}}] declares constant

  1041   \isa{c} to have any instance of type scheme \isa{{\isasymsigma}}.  The

  1042   optional mixfix annotations may attach concrete syntax to the

  1043   constants declared.

  1044

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

  1046   as a definitional axiom for some existing constant.

  1047

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

  1049   for this definition, which is occasionally useful for exotic

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

  1051   theory specifications!

  1052

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

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

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

  1056   special type than that of the corresponding constant declaration.

  1057

  1058   \item [\hyperlink{command.constdefs}{\mbox{\isa{\isacommand{constdefs}}}}] provides a streamlined combination of

  1059   constants declarations and definitions: type-inference takes care of

  1060   the most general typing of the given specification (the optional

  1061   type constraint may refer to type-inference dummies \isa{{\isacharunderscore}}'' as usual).  The resulting type declaration needs to agree with

  1062   that of the specification; overloading is \emph{not} supported here!

  1063

  1064   The constant name may be omitted altogether, if neither type nor

  1065   syntax declarations are given.  The canonical name of the

  1066   definitional axiom for constant \isa{c} will be \isa{c{\isacharunderscore}def},

  1067   unless specified otherwise.  Also note that the given list of

  1068   specifications is processed in a strictly sequential manner, with

  1069   type-checking being performed independently.

  1070

  1071   An optional initial context of \isa{{\isachardoublequote}{\isacharparenleft}structure{\isacharparenright}{\isachardoublequote}} declarations

  1072   admits use of indexed syntax, using the special symbol \verb|\<index>| (printed as \isa{{\isachardoublequote}{\isasymindex}{\isachardoublequote}}'').  The latter concept is

  1073   particularly useful with locales (see also \S\ref{sec:locale}).

  1074

  1075   \end{descr}%

  1076 \end{isamarkuptext}%

  1077 \isamarkuptrue%

  1078 %

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

  1080 }

  1081 \isamarkuptrue%

  1082 %

  1083 \begin{isamarkuptext}%

  1084 \begin{matharray}{rcll}

  1085     \indexdef{}{command}{axioms}\hypertarget{command.axioms}{\hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}}} & : & \isartrans{theory}{theory} & (axiomatic!) \\

  1086     \indexdef{}{command}{lemmas}\hypertarget{command.lemmas}{\hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}} & : & \isarkeep{local{\dsh}theory} \\

  1087     \indexdef{}{command}{theorems}\hypertarget{command.theorems}{\hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}}} & : & \isarkeep{local{\dsh}theory} \\

  1088   \end{matharray}

  1089

  1090   \begin{rail}

  1091     'axioms' (axmdecl prop +)

  1092     ;

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

  1094     ;

  1095   \end{rail}

  1096

  1097   \begin{descr}

  1098

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

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

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

  1102   theorem.

  1103

  1104   Axioms are usually only introduced when declaring new logical

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

  1106   definitions and proven theorems.

  1107

  1108   \item [\hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}~\isa{{\isachardoublequote}a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}}]

  1109   retrieves and stores existing facts in the theory context, or the

  1110   specified target context (see also \secref{sec:target}).  Typical

  1111   applications would also involve attributes, to declare Simplifier

  1112   rules, for example.

  1113

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

  1115

  1116   \end{descr}%

  1117 \end{isamarkuptext}%

  1118 \isamarkuptrue%

  1119 %

  1120 \isamarkupsection{Oracles%

  1121 }

  1122 \isamarkuptrue%

  1123 %

  1124 \begin{isamarkuptext}%

  1125 \begin{matharray}{rcl}

  1126     \indexdef{}{command}{oracle}\hypertarget{command.oracle}{\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}} & : & \isartrans{theory}{theory} \\

  1127   \end{matharray}

  1128

  1129   The oracle interface promotes a given ML function \verb|theory -> T -> term| to \verb|theory -> T -> thm|, for some

  1130   type \verb|T| given by the user.  This acts like an infinitary

  1131   specification of axioms -- there is no internal check of the

  1132   correctness of the results!  The inference kernel records oracle

  1133   invocations within the internal derivation object of theorems, and

  1134   the pretty printer attaches \isa{{\isachardoublequote}{\isacharbrackleft}{\isacharbang}{\isacharbrackright}{\isachardoublequote}}'' to indicate results

  1135   that are not fully checked by Isabelle inferences.

  1136

  1137   \begin{rail}

  1138     'oracle' name '(' type ')' '=' text

  1139     ;

  1140   \end{rail}

  1141

  1142   \begin{descr}

  1143

  1144   \item [\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}~\isa{{\isachardoublequote}name\ {\isacharparenleft}type{\isacharparenright}\ {\isacharequal}\ text{\isachardoublequote}}] turns the

  1145   given ML expression \isa{{\isachardoublequote}text{\isachardoublequote}} of type

  1146   \verb|theory ->|~\isa{{\isachardoublequote}type{\isachardoublequote}}~\verb|-> term| into an

  1147   ML function of type

  1148   \verb|theory ->|~\isa{{\isachardoublequote}type{\isachardoublequote}}~\verb|-> thm|, which is

  1149   bound to the global identifier \verb|name|.

  1150

  1151   \end{descr}%

  1152 \end{isamarkuptext}%

  1153 \isamarkuptrue%

  1154 %

  1155 \isamarkupsection{Name spaces%

  1156 }

  1157 \isamarkuptrue%

  1158 %

  1159 \begin{isamarkuptext}%

  1160 \begin{matharray}{rcl}

  1161     \indexdef{}{command}{global}\hypertarget{command.global}{\hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}}} & : & \isartrans{theory}{theory} \\

  1162     \indexdef{}{command}{local}\hypertarget{command.local}{\hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}}} & : & \isartrans{theory}{theory} \\

  1163     \indexdef{}{command}{hide}\hypertarget{command.hide}{\hyperlink{command.hide}{\mbox{\isa{\isacommand{hide}}}}} & : & \isartrans{theory}{theory} \\

  1164   \end{matharray}

  1165

  1166   \begin{rail}

  1167     'hide' ('(open)')? name (nameref + )

  1168     ;

  1169   \end{rail}

  1170

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

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

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

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

  1175   do so.

  1176

  1177   \begin{descr}

  1178

  1179   \item [\hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}} and \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}}] change the

  1180   current name declaration mode.  Initially, theories start in

  1181   \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}} mode, causing all names to be automatically

  1182   qualified by the theory name.  Changing this to \hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}}

  1183   causes all names to be declared without the theory prefix, until

  1184   \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}} is declared again.

  1185

  1186   Note that global names are prone to get hidden accidently later,

  1187   when qualified names of the same base name are introduced.

  1188

  1189   \item [\hyperlink{command.hide}{\mbox{\isa{\isacommand{hide}}}}~\isa{{\isachardoublequote}space\ names{\isachardoublequote}}] fully removes

  1190   declarations from a given name space (which may be \isa{{\isachardoublequote}class{\isachardoublequote}},

  1191   \isa{{\isachardoublequote}type{\isachardoublequote}}, \isa{{\isachardoublequote}const{\isachardoublequote}}, or \isa{{\isachardoublequote}fact{\isachardoublequote}}); with the \isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}} option, only the base name is hidden.  Global

  1192   (unqualified) names may never be hidden.

  1193

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

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

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

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

  1198

  1199   \end{descr}%

  1200 \end{isamarkuptext}%

  1201 \isamarkuptrue%

  1202 %

  1203 \isamarkupsection{Syntax and translations \label{sec:syn-trans}%

  1204 }

  1205 \isamarkuptrue%

  1206 %

  1207 \begin{isamarkuptext}%

  1208 \begin{matharray}{rcl}

  1209     \indexdef{}{command}{syntax}\hypertarget{command.syntax}{\hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}}} & : & \isartrans{theory}{theory} \\

  1210     \indexdef{}{command}{no\_syntax}\hypertarget{command.no-syntax}{\hyperlink{command.no-syntax}{\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}}}} & : & \isartrans{theory}{theory} \\

  1211     \indexdef{}{command}{translations}\hypertarget{command.translations}{\hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}} & : & \isartrans{theory}{theory} \\

  1212     \indexdef{}{command}{no\_translations}\hypertarget{command.no-translations}{\hyperlink{command.no-translations}{\mbox{\isa{\isacommand{no{\isacharunderscore}translations}}}}} & : & \isartrans{theory}{theory} \\

  1213   \end{matharray}

  1214

  1215   \begin{rail}

  1216     ('syntax' | 'no\_syntax') mode? (constdecl +)

  1217     ;

  1218     ('translations' | 'no\_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)

  1219     ;

  1220

  1221     mode: ('(' ( name | 'output' | name 'output' ) ')')

  1222     ;

  1223     transpat: ('(' nameref ')')? string

  1224     ;

  1225   \end{rail}

  1226

  1227   \begin{descr}

  1228

  1229   \item [\hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}}~\isa{{\isachardoublequote}{\isacharparenleft}mode{\isacharparenright}\ decls{\isachardoublequote}}] is similar to

  1230   \hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}~\isa{decls}, except that the actual logical

  1231   signature extension is omitted.  Thus the context free grammar of

  1232   Isabelle's inner syntax may be augmented in arbitrary ways,

  1233   independently of the logic.  The \isa{mode} argument refers to the

  1234   print mode that the grammar rules belong; unless the \indexref{}{keyword}{output}\hyperlink{keyword.output}{\mbox{\isa{\isakeyword{output}}}} indicator is given, all productions are added both to the

  1235   input and output grammar.

  1236

  1237   \item [\hyperlink{command.no-syntax}{\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}}}~\isa{{\isachardoublequote}{\isacharparenleft}mode{\isacharparenright}\ decls{\isachardoublequote}}] removes

  1238   grammar declarations (and translations) resulting from \isa{decls}, which are interpreted in the same manner as for \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} above.

  1239

  1240   \item [\hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}~\isa{rules}] specifies syntactic

  1241   translation rules (i.e.\ macros): parse~/ print rules (\isa{{\isachardoublequote}{\isasymrightleftharpoons}{\isachardoublequote}}),

  1242   parse rules (\isa{{\isachardoublequote}{\isasymrightharpoonup}{\isachardoublequote}}), or print rules (\isa{{\isachardoublequote}{\isasymleftharpoondown}{\isachardoublequote}}).

  1243   Translation patterns may be prefixed by the syntactic category to be

  1244   used for parsing; the default is \isa{logic}.

  1245

  1246   \item [\hyperlink{command.no-translations}{\mbox{\isa{\isacommand{no{\isacharunderscore}translations}}}}~\isa{rules}] removes syntactic

  1247   translation rules, which are interpreted in the same manner as for

  1248   \hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}} above.

  1249

  1250   \end{descr}%

  1251 \end{isamarkuptext}%

  1252 \isamarkuptrue%

  1253 %

  1254 \isamarkupsection{Syntax translation functions%

  1255 }

  1256 \isamarkuptrue%

  1257 %

  1258 \begin{isamarkuptext}%

  1259 \begin{matharray}{rcl}

  1260     \indexdef{}{command}{parse\_ast\_translation}\hypertarget{command.parse-ast-translation}{\hyperlink{command.parse-ast-translation}{\mbox{\isa{\isacommand{parse{\isacharunderscore}ast{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\

  1261     \indexdef{}{command}{parse\_translation}\hypertarget{command.parse-translation}{\hyperlink{command.parse-translation}{\mbox{\isa{\isacommand{parse{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\

  1262     \indexdef{}{command}{print\_translation}\hypertarget{command.print-translation}{\hyperlink{command.print-translation}{\mbox{\isa{\isacommand{print{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\

  1263     \indexdef{}{command}{typed\_print\_translation}\hypertarget{command.typed-print-translation}{\hyperlink{command.typed-print-translation}{\mbox{\isa{\isacommand{typed{\isacharunderscore}print{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\

  1264     \indexdef{}{command}{print\_ast\_translation}\hypertarget{command.print-ast-translation}{\hyperlink{command.print-ast-translation}{\mbox{\isa{\isacommand{print{\isacharunderscore}ast{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\

  1265     \indexdef{}{command}{token\_translation}\hypertarget{command.token-translation}{\hyperlink{command.token-translation}{\mbox{\isa{\isacommand{token{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\

  1266   \end{matharray}

  1267

  1268   \begin{rail}

  1269   ( 'parse\_ast\_translation' | 'parse\_translation' | 'print\_translation' |

  1270     'typed\_print\_translation' | 'print\_ast\_translation' ) ('(advanced)')? text

  1271   ;

  1272

  1273   'token\_translation' text

  1274   ;

  1275   \end{rail}

  1276

  1277   Syntax translation functions written in ML admit almost arbitrary

  1278   manipulations of Isabelle's inner syntax.  Any of the above commands

  1279   have a single \railqtok{text} argument that refers to an ML

  1280   expression of appropriate type, which are as follows by default:

  1281

  1282 %FIXME proper antiquotations

  1283 \begin{ttbox}

  1284 val parse_ast_translation   : (string * (ast list -> ast)) list

  1285 val parse_translation       : (string * (term list -> term)) list

  1286 val print_translation       : (string * (term list -> term)) list

  1287 val typed_print_translation :

  1288   (string * (bool -> typ -> term list -> term)) list

  1289 val print_ast_translation   : (string * (ast list -> ast)) list

  1290 val token_translation       :

  1291   (string * string * (string -> string * real)) list

  1292 \end{ttbox}

  1293

  1294   If the \isa{{\isachardoublequote}{\isacharparenleft}advanced{\isacharparenright}{\isachardoublequote}} option is given, the corresponding

  1295   translation functions may depend on the current theory or proof

  1296   context.  This allows to implement advanced syntax mechanisms, as

  1297   translations functions may refer to specific theory declarations or

  1298   auxiliary proof data.

  1299

  1300   See also \cite[\S8]{isabelle-ref} for more information on the

  1301   general concept of syntax transformations in Isabelle.

  1302

  1303 %FIXME proper antiquotations

  1304 \begin{ttbox}

  1305 val parse_ast_translation:

  1306   (string * (Proof.context -> ast list -> ast)) list

  1307 val parse_translation:

  1308   (string * (Proof.context -> term list -> term)) list

  1309 val print_translation:

  1310   (string * (Proof.context -> term list -> term)) list

  1311 val typed_print_translation:

  1312   (string * (Proof.context -> bool -> typ -> term list -> term)) list

  1313 val print_ast_translation:

  1314   (string * (Proof.context -> ast list -> ast)) list

  1315 \end{ttbox}%

  1316 \end{isamarkuptext}%

  1317 \isamarkuptrue%

  1318 %

  1319 \isadelimtheory

  1320 %

  1321 \endisadelimtheory

  1322 %

  1323 \isatagtheory

  1324 \isacommand{end}\isamarkupfalse%

  1325 %

  1326 \endisatagtheory

  1327 {\isafoldtheory}%

  1328 %

  1329 \isadelimtheory

  1330 %

  1331 \endisadelimtheory

  1332 \isanewline

  1333 \end{isabellebody}%

  1334 %%% Local Variables:

  1335 %%% mode: latex

  1336 %%% TeX-master: "root"

  1337 %%% End: