src/Doc/Isar_Ref/Spec.thy
 author wenzelm Thu Mar 14 16:55:06 2019 +0100 (5 weeks ago) changeset 69913 ca515cf61651 parent 69597 ff784d5a5bfb child 69962 82e945d472d5 permissions -rw-r--r--
more specific keyword kinds;
     1 (*:maxLineLen=78:*)

     2

     3 theory Spec

     4   imports Main Base

     5 begin

     6

     7 chapter \<open>Specifications\<close>

     8

     9 text \<open>

    10   The Isabelle/Isar theory format integrates specifications and proofs, with

    11   support for interactive development by continuous document editing. There is

    12   a separate document preparation system (see \chref{ch:document-prep}), for

    13   typesetting formal developments together with informal text. The resulting

    14   hyper-linked PDF documents can be used both for WWW presentation and printed

    15   copies.

    16

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

    18   language as a proper sub-language. Proof mode is entered by stating some

    19   \<^theory_text>\<open>theorem\<close> or \<^theory_text>\<open>lemma\<close> at the theory level, and left again with the final

    20   conclusion (e.g.\ via \<^theory_text>\<open>qed\<close>).

    21 \<close>

    22

    23

    24 section \<open>Defining theories \label{sec:begin-thy}\<close>

    25

    26 text \<open>

    27   \begin{matharray}{rcl}

    28     @{command_def "theory"} & : & \<open>toplevel \<rightarrow> theory\<close> \\

    29     @{command_def (global) "end"} & : & \<open>theory \<rightarrow> toplevel\<close> \\

    30     @{command_def "thy_deps"}\<open>\<^sup>*\<close> & : & \<open>theory \<rightarrow>\<close> \\

    31   \end{matharray}

    32

    33   Isabelle/Isar theories are defined via theory files, which consist of an

    34   outermost sequence of definition--statement--proof elements. Some

    35   definitions are self-sufficient (e.g.\ \<^theory_text>\<open>fun\<close> in Isabelle/HOL), with

    36   foundational proofs performed internally. Other definitions require an

    37   explicit proof as justification (e.g.\ \<^theory_text>\<open>function\<close> and \<^theory_text>\<open>termination\<close> in

    38   Isabelle/HOL). Plain statements like \<^theory_text>\<open>theorem\<close> or \<^theory_text>\<open>lemma\<close> are merely a

    39   special case of that, defining a theorem from a given proposition and its

    40   proof.

    41

    42   The theory body may be sub-structured by means of \<^emph>\<open>local theory targets\<close>,

    43   such as \<^theory_text>\<open>locale\<close> and \<^theory_text>\<open>class\<close>. It is also possible to use \<^theory_text>\<open>context begin \<dots>

    44   end\<close> blocks to delimited a local theory context: a \<^emph>\<open>named context\<close> to

    45   augment a locale or class specification, or an \<^emph>\<open>unnamed context\<close> to refer

    46   to local parameters and assumptions that are discharged later. See

    47   \secref{sec:target} for more details.

    48

    49   \<^medskip>

    50   A theory is commenced by the \<^theory_text>\<open>theory\<close> command, which indicates imports of

    51   previous theories, according to an acyclic foundational order. Before the

    52   initial \<^theory_text>\<open>theory\<close> command, there may be optional document header material

    53   (like \<^theory_text>\<open>section\<close> or \<^theory_text>\<open>text\<close>, see \secref{sec:markup}). The document header

    54   is outside of the formal theory context, though.

    55

    56   A theory is concluded by a final @{command (global) "end"} command, one that

    57   does not belong to a local theory target. No further commands may follow

    58   such a global @{command (global) "end"}.

    59

    60   \<^rail>\<open>

    61     @@{command theory} @{syntax system_name}

    62       @'imports' (@{syntax system_name} +) \<newline>

    63       keywords? abbrevs? @'begin'

    64     ;

    65     keywords: @'keywords' (keyword_decls + @'and')

    66     ;

    67     keyword_decls: (@{syntax string} +) ('::' @{syntax name} @{syntax tags})?

    68     ;

    69     abbrevs: @'abbrevs' (((text+) '=' (text+)) + @'and')

    70     ;

    71     @@{command thy_deps} (thy_bounds thy_bounds?)?

    72     ;

    73     thy_bounds: @{syntax name} | '(' (@{syntax name} + @'|') ')'

    74   \<close>

    75

    76   \<^descr> \<^theory_text>\<open>theory A imports B\<^sub>1 \<dots> B\<^sub>n begin\<close> starts a new theory \<open>A\<close> based on the

    77   merge of existing theories \<open>B\<^sub>1 \<dots> B\<^sub>n\<close>. Due to the possibility to import

    78   more than one ancestor, the resulting theory structure of an Isabelle

    79   session forms a directed acyclic graph (DAG). Isabelle takes care that

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

    81   files are automatically rechecked whenever a theory header specification is

    82   processed.

    83

    84   Empty imports are only allowed in the bootstrap process of the special

    85   theory \<^theory>\<open>Pure\<close>, which is the start of any other formal development

    86   based on Isabelle. Regular user theories usually refer to some more complex

    87   entry point, such as theory \<^theory>\<open>Main\<close> in Isabelle/HOL.

    88

    89   The @{keyword_def "keywords"} specification declares outer syntax

    90   (\chref{ch:outer-syntax}) that is introduced in this theory later on (rare

    91   in end-user applications). Both minor keywords and major keywords of the

    92   Isar command language need to be specified, in order to make parsing of

    93   proof documents work properly. Command keywords need to be classified

    94   according to their structural role in the formal text. Examples may be seen

    95   in Isabelle/HOL sources itself, such as @{keyword "keywords"}~\<^verbatim>\<open>"typedef"\<close>

    96   \<open>:: thy_goal_defn\<close> or @{keyword "keywords"}~\<^verbatim>\<open>"datatype"\<close> \<open>:: thy_defn\<close> for

    97   theory-level definitions with and without proof, respectively. Additional

    98   @{syntax tags} provide defaults for document preparation

    99   (\secref{sec:tags}).

   100

   101   The @{keyword_def "abbrevs"} specification declares additional abbreviations

   102   for syntactic completion. The default for a new keyword is just its name,

   103   but completion may be avoided by defining @{keyword "abbrevs"} with empty

   104   text.

   105

   106   \<^descr> @{command (global) "end"} concludes the current theory definition. Note

   107   that some other commands, e.g.\ local theory targets \<^theory_text>\<open>locale\<close> or \<^theory_text>\<open>class\<close>

   108   may involve a \<^theory_text>\<open>begin\<close> that needs to be matched by @{command (local) "end"},

   109   according to the usual rules for nested blocks.

   110

   111   \<^descr> \<^theory_text>\<open>thy_deps\<close> visualizes the theory hierarchy as a directed acyclic graph.

   112   By default, all imported theories are shown. This may be restricted by

   113   specifying bounds wrt. the theory inclusion relation.

   114 \<close>

   115

   116

   117 section \<open>Local theory targets \label{sec:target}\<close>

   118

   119 text \<open>

   120   \begin{matharray}{rcll}

   121     @{command_def "context"} & : & \<open>theory \<rightarrow> local_theory\<close> \\

   122     @{command_def (local) "end"} & : & \<open>local_theory \<rightarrow> theory\<close> \\

   123     @{keyword_def "private"} \\

   124     @{keyword_def "qualified"} \\

   125   \end{matharray}

   126

   127   A local theory target is a specification context that is managed separately

   128   within the enclosing theory. Contexts may introduce parameters (fixed

   129   variables) and assumptions (hypotheses). Definitions and theorems depending

   130   on the context may be added incrementally later on.

   131

   132   \<^emph>\<open>Named contexts\<close> refer to locales (cf.\ \secref{sec:locale}) or type

   133   classes (cf.\ \secref{sec:class}); the name \<open>-\<close>'' signifies the global

   134   theory context.

   135

   136   \<^emph>\<open>Unnamed contexts\<close> may introduce additional parameters and assumptions, and

   137   results produced in the context are generalized accordingly. Such auxiliary

   138   contexts may be nested within other targets, like \<^theory_text>\<open>locale\<close>, \<^theory_text>\<open>class\<close>,

   139   \<^theory_text>\<open>instantiation\<close>, \<^theory_text>\<open>overloading\<close>.

   140

   141   \<^rail>\<open>

   142     @@{command context} @{syntax name} @'begin'

   143     ;

   144     @@{command context} @{syntax_ref "includes"}? (@{syntax context_elem} * ) @'begin'

   145     ;

   146     @{syntax_def target}: '(' @'in' @{syntax name} ')'

   147   \<close>

   148

   149   \<^descr> \<^theory_text>\<open>context c begin\<close> opens a named context, by recommencing an existing

   150   locale or class \<open>c\<close>. Note that locale and class definitions allow to include

   151   the \<^theory_text>\<open>begin\<close> keyword as well, in order to continue the local theory

   152   immediately after the initial specification.

   153

   154   \<^descr> \<^theory_text>\<open>context bundles elements begin\<close> opens an unnamed context, by extending

   155   the enclosing global or local theory target by the given declaration bundles

   156   (\secref{sec:bundle}) and context elements (\<^theory_text>\<open>fixes\<close>, \<^theory_text>\<open>assumes\<close> etc.). This

   157   means any results stemming from definitions and proofs in the extended

   158   context will be exported into the enclosing target by lifting over extra

   159   parameters and premises.

   160

   161   \<^descr> @{command (local) "end"} concludes the current local theory, according to

   162   the nesting of contexts. Note that a global @{command (global) "end"} has a

   163   different meaning: it concludes the theory itself (\secref{sec:begin-thy}).

   164

   165   \<^descr> \<^theory_text>\<open>private\<close> or \<^theory_text>\<open>qualified\<close> may be given as modifiers before any local

   166   theory command. This restricts name space accesses to the local scope, as

   167   determined by the enclosing \<^theory_text>\<open>context begin \<dots> end\<close> block. Outside its scope,

   168   a \<^theory_text>\<open>private\<close> name is inaccessible, and a \<^theory_text>\<open>qualified\<close> name is only

   169   accessible with some qualification.

   170

   171   Neither a global \<^theory_text>\<open>theory\<close> nor a \<^theory_text>\<open>locale\<close> target provides a local scope by

   172   itself: an extra unnamed context is required to use \<^theory_text>\<open>private\<close> or

   173   \<^theory_text>\<open>qualified\<close> here.

   174

   175   \<^descr> \<open>(\<close>@{keyword_def "in"}~\<open>c)\<close> given after any local theory command specifies

   176   an immediate target, e.g.\ \<^theory_text>\<open>definition (in c)\<close>'' or

   177   \<^theory_text>\<open>theorem (in c)\<close>''. This works both in a local or global theory context;

   178   the current target context will be suspended for this command only. Note

   179   that \<^theory_text>\<open>(in -)\<close>'' will always produce a global result independently of the

   180   current target context.

   181

   182

   183   Any specification element that operates on \<open>local_theory\<close> according to this

   184   manual implicitly allows the above target syntax \<^theory_text>\<open>(in c)\<close>, but individual

   185   syntax diagrams omit that aspect for clarity.

   186

   187   \<^medskip>

   188   The exact meaning of results produced within a local theory context depends

   189   on the underlying target infrastructure (locale, type class etc.). The

   190   general idea is as follows, considering a context named \<open>c\<close> with parameter

   191   \<open>x\<close> and assumption \<open>A[x]\<close>.

   192

   193   Definitions are exported by introducing a global version with additional

   194   arguments; a syntactic abbreviation links the long form with the abstract

   195   version of the target context. For example, \<open>a \<equiv> t[x]\<close> becomes \<open>c.a ?x \<equiv>

   196   t[?x]\<close> at the theory level (for arbitrary \<open>?x\<close>), together with a local

   197   abbreviation \<open>c \<equiv> c.a x\<close> in the target context (for the fixed parameter

   198   \<open>x\<close>).

   199

   200   Theorems are exported by discharging the assumptions and generalizing the

   201   parameters of the context. For example, \<open>a: B[x]\<close> becomes \<open>c.a: A[?x] \<Longrightarrow>

   202   B[?x]\<close>, again for arbitrary \<open>?x\<close>.

   203 \<close>

   204

   205

   206 section \<open>Bundled declarations \label{sec:bundle}\<close>

   207

   208 text \<open>

   209   \begin{matharray}{rcl}

   210     @{command_def "bundle"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\

   211     @{command "bundle"} & : & \<open>theory \<rightarrow> local_theory\<close> \\

   212     @{command_def "print_bundles"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\

   213     @{command_def "include"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\

   214     @{command_def "including"} & : & \<open>proof(prove) \<rightarrow> proof(prove)\<close> \\

   215     @{keyword_def "includes"} & : & syntax \\

   216   \end{matharray}

   217

   218   The outer syntax of fact expressions (\secref{sec:syn-att}) involves

   219   theorems and attributes, which are evaluated in the context and applied to

   220   it. Attributes may declare theorems to the context, as in \<open>this_rule [intro]

   221   that_rule [elim]\<close> for example. Configuration options (\secref{sec:config})

   222   are special declaration attributes that operate on the context without a

   223   theorem, as in \<open>[[show_types = false]]\<close> for example.

   224

   225   Expressions of this form may be defined as \<^emph>\<open>bundled declarations\<close> in the

   226   context, and included in other situations later on. Including declaration

   227   bundles augments a local context casually without logical dependencies,

   228   which is in contrast to locales and locale interpretation

   229   (\secref{sec:locale}).

   230

   231   \<^rail>\<open>

   232     @@{command bundle} @{syntax name}

   233       ( '=' @{syntax thms} @{syntax for_fixes} | @'begin')

   234     ;

   235     @@{command print_bundles} ('!'?)

   236     ;

   237     (@@{command include} | @@{command including}) (@{syntax name}+)

   238     ;

   239     @{syntax_def "includes"}: @'includes' (@{syntax name}+)

   240   \<close>

   241

   242   \<^descr> \<^theory_text>\<open>bundle b = decls\<close> defines a bundle of declarations in the current

   243   context. The RHS is similar to the one of the \<^theory_text>\<open>declare\<close> command. Bundles

   244   defined in local theory targets are subject to transformations via

   245   morphisms, when moved into different application contexts; this works

   246   analogously to any other local theory specification.

   247

   248   \<^descr> \<^theory_text>\<open>bundle b begin body end\<close> defines a bundle of declarations from the

   249   \<open>body\<close> of local theory specifications. It may consist of commands that are

   250   technically equivalent to \<^theory_text>\<open>declare\<close> or \<^theory_text>\<open>declaration\<close>, which also includes

   251   \<^theory_text>\<open>notation\<close>, for example. Named fact declarations like \<^theory_text>\<open>lemmas a [simp] =

   252   b\<close>'' or \<^theory_text>\<open>lemma a [simp]: B \<proof>\<close>'' are also admitted, but the name

   253   bindings are not recorded in the bundle.

   254

   255   \<^descr> \<^theory_text>\<open>print_bundles\<close> prints the named bundles that are available in the

   256   current context; the \<open>!\<close>'' option indicates extra verbosity.

   257

   258   \<^descr> \<^theory_text>\<open>unbundle b\<^sub>1 \<dots> b\<^sub>n\<close> activates the declarations from the given bundles in

   259   the current local theory context. This is analogous to \<^theory_text>\<open>lemmas\<close>

   260   (\secref{sec:theorems}) with the expanded bundles.

   261

   262   \<^descr> \<^theory_text>\<open>include\<close> is similar to \<^theory_text>\<open>unbundle\<close>, but works in a proof body (forward

   263   mode). This is analogous to \<^theory_text>\<open>note\<close> (\secref{sec:proof-facts}) with the

   264   expanded bundles.

   265

   266   \<^descr> \<^theory_text>\<open>including\<close> is similar to \<^theory_text>\<open>include\<close>, but works in proof refinement

   267   (backward mode). This is analogous to \<^theory_text>\<open>using\<close> (\secref{sec:proof-facts})

   268   with the expanded bundles.

   269

   270   \<^descr> \<^theory_text>\<open>includes b\<^sub>1 \<dots> b\<^sub>n\<close> is similar to \<^theory_text>\<open>include\<close>, but works in situations

   271   where a specification context is constructed, notably for \<^theory_text>\<open>context\<close> and

   272   long statements of \<^theory_text>\<open>theorem\<close> etc.

   273

   274

   275   Here is an artificial example of bundling various configuration options:

   276 \<close>

   277

   278 (*<*)experiment begin(*>*)

   279 bundle trace = [[simp_trace, linarith_trace, metis_trace, smt_trace]]

   280

   281 lemma "x = x"

   282   including trace by metis

   283 (*<*)end(*>*)

   284

   285

   286 section \<open>Term definitions \label{sec:term-definitions}\<close>

   287

   288 text \<open>

   289   \begin{matharray}{rcll}

   290     @{command_def "definition"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\

   291     @{attribute_def "defn"} & : & \<open>attribute\<close> \\

   292     @{command_def "print_defn_rules"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\

   293     @{command_def "abbreviation"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\

   294     @{command_def "print_abbrevs"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\

   295   \end{matharray}

   296

   297   Term definitions may either happen within the logic (as equational axioms of

   298   a certain form (see also \secref{sec:overloading}), or outside of it as

   299   rewrite system on abstract syntax. The second form is called

   300   abbreviation''.

   301

   302   \<^rail>\<open>

   303     @@{command definition} decl? definition

   304     ;

   305     @@{command abbreviation} @{syntax mode}? decl? abbreviation

   306     ;

   307     @@{command print_abbrevs} ('!'?)

   308     ;

   309     decl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}? @'where'

   310     ;

   311     definition: @{syntax thmdecl}? @{syntax prop}

   312       @{syntax spec_prems} @{syntax for_fixes}

   313     ;

   314     abbreviation: @{syntax prop} @{syntax for_fixes}

   315   \<close>

   316

   317   \<^descr> \<^theory_text>\<open>definition c where eq\<close> produces an internal definition \<open>c \<equiv> t\<close> according

   318   to the specification given as \<open>eq\<close>, which is then turned into a proven fact.

   319   The given proposition may deviate from internal meta-level equality

   320   according to the rewrite rules declared as @{attribute defn} by the

   321   object-logic. This usually covers object-level equality \<open>x = y\<close> and

   322   equivalence \<open>A \<longleftrightarrow> B\<close>. End-users normally need not change the @{attribute

   323   defn} setup.

   324

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

   326   additional conditions, e.g.\ \<open>f x y = t\<close> instead of \<open>f \<equiv> \<lambda>x y. t\<close> and \<open>y \<noteq> 0

   327   \<Longrightarrow> g x y = u\<close> instead of an unrestricted \<open>g \<equiv> \<lambda>x y. u\<close>.

   328

   329   \<^descr> \<^theory_text>\<open>print_defn_rules\<close> prints the definitional rewrite rules declared via

   330   @{attribute defn} in the current context.

   331

   332   \<^descr> \<^theory_text>\<open>abbreviation c where eq\<close> introduces a syntactic constant which is

   333   associated with a certain term according to the meta-level equality \<open>eq\<close>.

   334

   335   Abbreviations participate in the usual type-inference process, but are

   336   expanded before the logic ever sees them. Pretty printing of terms involves

   337   higher-order rewriting with rules stemming from reverted abbreviations. This

   338   needs some care to avoid overlapping or looping syntactic replacements!

   339

   340   The optional \<open>mode\<close> specification restricts output to a particular print

   341   mode; using \<open>input\<close>'' here achieves the effect of one-way abbreviations.

   342   The mode may also include an \<^theory_text>\<open>output\<close>'' qualifier that affects the

   343   concrete syntax declared for abbreviations, cf.\ \<^theory_text>\<open>syntax\<close> in

   344   \secref{sec:syn-trans}.

   345

   346   \<^descr> \<^theory_text>\<open>print_abbrevs\<close> prints all constant abbreviations of the current context;

   347   the \<open>!\<close>'' option indicates extra verbosity.

   348 \<close>

   349

   350

   351 section \<open>Axiomatizations \label{sec:axiomatizations}\<close>

   352

   353 text \<open>

   354   \begin{matharray}{rcll}

   355     @{command_def "axiomatization"} & : & \<open>theory \<rightarrow> theory\<close> & (axiomatic!) \\

   356   \end{matharray}

   357

   358   \<^rail>\<open>

   359     @@{command axiomatization} @{syntax vars}? (@'where' axiomatization)?

   360     ;

   361     axiomatization: (@{syntax thmdecl} @{syntax prop} + @'and')

   362       @{syntax spec_prems} @{syntax for_fixes}

   363   \<close>

   364

   365   \<^descr> \<^theory_text>\<open>axiomatization c\<^sub>1 \<dots> c\<^sub>m where \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close> introduces several constants

   366   simultaneously and states axiomatic properties for these. The constants are

   367   marked as being specified once and for all, which prevents additional

   368   specifications for the same constants later on, but it is always possible do

   369   emit axiomatizations without referring to particular constants. Note that

   370   lack of precise dependency tracking of axiomatizations may disrupt the

   371   well-formedness of an otherwise definitional theory.

   372

   373   Axiomatization is restricted to a global theory context: support for local

   374   theory targets \secref{sec:target} would introduce an extra dimension of

   375   uncertainty what the written specifications really are, and make it

   376   infeasible to argue why they are correct.

   377

   378   Axiomatic specifications are required when declaring a new logical system

   379   within Isabelle/Pure, but in an application environment like Isabelle/HOL

   380   the user normally stays within definitional mechanisms provided by the logic

   381   and its libraries.

   382 \<close>

   383

   384

   385 section \<open>Generic declarations\<close>

   386

   387 text \<open>

   388   \begin{matharray}{rcl}

   389     @{command_def "declaration"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\

   390     @{command_def "syntax_declaration"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\

   391     @{command_def "declare"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\

   392   \end{matharray}

   393

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

   395   declaration elements. Since the underlying concept of local theories may be

   396   subject to later re-interpretation, there is an additional dependency on a

   397   morphism that tells the difference of the original declaration context wrt.\

   398   the application context encountered later on. A fact declaration is an

   399   important special case: it consists of a theorem which is applied to the

   400   context by means of an attribute.

   401

   402   \<^rail>\<open>

   403     (@@{command declaration} | @@{command syntax_declaration})

   404       ('(' @'pervasive' ')')? \<newline> @{syntax text}

   405     ;

   406     @@{command declare} (@{syntax thms} + @'and')

   407   \<close>

   408

   409   \<^descr> \<^theory_text>\<open>declaration d\<close> adds the declaration function \<open>d\<close> of ML type \<^ML_type>\<open>declaration\<close>, to the current local theory under construction. In later

   410   application contexts, the function is transformed according to the morphisms

   411   being involved in the interpretation hierarchy.

   412

   413   If the \<^theory_text>\<open>(pervasive)\<close> option is given, the corresponding declaration is

   414   applied to all possible contexts involved, including the global background

   415   theory.

   416

   417   \<^descr> \<^theory_text>\<open>syntax_declaration\<close> is similar to \<^theory_text>\<open>declaration\<close>, but is meant to affect

   418   only syntactic'' tools by convention (such as notation and type-checking

   419   information).

   420

   421   \<^descr> \<^theory_text>\<open>declare thms\<close> declares theorems to the current local theory context. No

   422   theorem binding is involved here, unlike \<^theory_text>\<open>lemmas\<close> (cf.\

   423   \secref{sec:theorems}), so \<^theory_text>\<open>declare\<close> only has the effect of applying

   424   attributes as included in the theorem specification.

   425 \<close>

   426

   427

   428 section \<open>Locales \label{sec:locale}\<close>

   429

   430 text \<open>

   431   A locale is a functor that maps parameters (including implicit type

   432   parameters) and a specification to a list of declarations. The syntax of

   433   locales is modeled after the Isar proof context commands (cf.\

   434   \secref{sec:proof-context}).

   435

   436   Locale hierarchies are supported by maintaining a graph of dependencies

   437   between locale instances in the global theory. Dependencies may be

   438   introduced through import (where a locale is defined as sublocale of the

   439   imported instances) or by proving that an existing locale is a sublocale of

   440   one or several locale instances.

   441

   442   A locale may be opened with the purpose of appending to its list of

   443   declarations (cf.\ \secref{sec:target}). When opening a locale declarations

   444   from all dependencies are collected and are presented as a local theory. In

   445   this process, which is called \<^emph>\<open>roundup\<close>, redundant locale instances are

   446   omitted. A locale instance is redundant if it is subsumed by an instance

   447   encountered earlier. A more detailed description of this process is

   448   available elsewhere @{cite Ballarin2014}.

   449 \<close>

   450

   451

   452 subsection \<open>Locale expressions \label{sec:locale-expr}\<close>

   453

   454 text \<open>

   455   A \<^emph>\<open>locale expression\<close> denotes a context composed of instances of existing

   456   locales. The context consists of the declaration elements from the locale

   457   instances. Redundant locale instances are omitted according to roundup.

   458

   459   \<^rail>\<open>

   460     @{syntax_def locale_expr}: (instance + '+') @{syntax for_fixes}

   461     ;

   462     instance: (qualifier ':')? @{syntax name} (pos_insts | named_insts) \<newline>

   463       rewrites?

   464     ;

   465     qualifier: @{syntax name} ('?')?

   466     ;

   467     pos_insts: ('_' | @{syntax term})*

   468     ;

   469     named_insts: @'where' (@{syntax name} '=' @{syntax term} + @'and')

   470     ;

   471     rewrites: @'rewrites' (@{syntax thmdecl}? @{syntax prop} + @'and')

   472   \<close>

   473

   474   A locale instance consists of a reference to a locale and either positional

   475   or named parameter instantiations optionally followed by rewrites clauses.

   476   Identical instantiations (that is, those

   477   that instantiate a parameter by itself) may be omitted. The notation \<open>_\<close>''

   478   enables to omit the instantiation for a parameter inside a positional

   479   instantiation.

   480

   481   Terms in instantiations are from the context the locale expressions is

   482   declared in. Local names may be added to this context with the optional

   483   \<^theory_text>\<open>for\<close> clause. This is useful for shadowing names bound in outer contexts,

   484   and for declaring syntax. In addition, syntax declarations from one instance

   485   are effective when parsing subsequent instances of the same expression.

   486

   487   Instances have an optional qualifier which applies to names in declarations.

   488   Names include local definitions and theorem names. If present, the qualifier

   489   itself is either mandatory (default) or non-mandatory (when followed by

   490   \<^verbatim>\<open>?\<close>''). Non-mandatory means that the qualifier may be omitted on input.

   491   Qualifiers only affect name spaces; they play no role in determining whether

   492   one locale instance subsumes another.

   493

   494   Rewrite clauses amend instances with equations that act as rewrite rules.

   495   This is particularly useful for changing concepts introduced through

   496   definitions. Rewrite clauses are available only in interpretation commands

   497   (see \secref{sec:locale-interpretation} below) and must be proved the user.

   498 \<close>

   499

   500

   501 subsection \<open>Locale declarations\<close>

   502

   503 text \<open>

   504   \begin{matharray}{rcl}

   505     @{command_def "locale"} & : & \<open>theory \<rightarrow> local_theory\<close> \\

   506     @{command_def "experiment"} & : & \<open>theory \<rightarrow> local_theory\<close> \\

   507     @{command_def "print_locale"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\

   508     @{command_def "print_locales"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\

   509     @{command_def "locale_deps"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\

   510     @{method_def intro_locales} & : & \<open>method\<close> \\

   511     @{method_def unfold_locales} & : & \<open>method\<close> \\

   512   \end{matharray}

   513

   514   \indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes}

   515   \indexisarelem{defines}\indexisarelem{notes}

   516   \<^rail>\<open>

   517     @@{command locale} @{syntax name} ('=' @{syntax locale})? @'begin'?

   518     ;

   519     @@{command experiment} (@{syntax context_elem}*) @'begin'

   520     ;

   521     @@{command print_locale} '!'? @{syntax name}

   522     ;

   523     @@{command print_locales} ('!'?)

   524     ;

   525     @{syntax_def locale}: @{syntax context_elem}+ |

   526       @{syntax locale_expr} ('+' (@{syntax context_elem}+))?

   527     ;

   528     @{syntax_def context_elem}:

   529       @'fixes' @{syntax vars} |

   530       @'constrains' (@{syntax name} '::' @{syntax type} + @'and') |

   531       @'assumes' (@{syntax props} + @'and') |

   532       @'defines' (@{syntax thmdecl}? @{syntax prop} @{syntax prop_pat}? + @'and') |

   533       @'notes' (@{syntax thmdef}? @{syntax thms} + @'and')

   534   \<close>

   535

   536   \<^descr> \<^theory_text>\<open>locale loc = import + body\<close> defines a new locale \<open>loc\<close> as a context

   537   consisting of a certain view of existing locales (\<open>import\<close>) plus some

   538   additional elements (\<open>body\<close>). Both \<open>import\<close> and \<open>body\<close> are optional; the

   539   degenerate form \<^theory_text>\<open>locale loc\<close> defines an empty locale, which may still be

   540   useful to collect declarations of facts later on. Type-inference on locale

   541   expressions automatically takes care of the most general typing that the

   542   combined context elements may acquire.

   543

   544   The \<open>import\<close> consists of a locale expression; see \secref{sec:proof-context}

   545   above. Its \<^theory_text>\<open>for\<close> clause defines the parameters of \<open>import\<close>. These are

   546   parameters of the defined locale. Locale parameters whose instantiation is

   547   omitted automatically extend the (possibly empty) \<^theory_text>\<open>for\<close> clause: they are

   548   inserted at its beginning. This means that these parameters may be referred

   549   to from within the expression and also in the subsequent context elements

   550   and provides a notational convenience for the inheritance of parameters in

   551   locale declarations.

   552

   553   The \<open>body\<close> consists of context elements.

   554

   555     \<^descr> @{element "fixes"}~\<open>x :: \<tau> (mx)\<close> declares a local parameter of type \<open>\<tau>\<close>

   556     and mixfix annotation \<open>mx\<close> (both are optional). The special syntax

   557     declaration \<open>(\<close>@{keyword_ref "structure"}\<open>)\<close>'' means that \<open>x\<close> may be

   558     referenced implicitly in this context.

   559

   560     \<^descr> @{element "constrains"}~\<open>x :: \<tau>\<close> introduces a type constraint \<open>\<tau>\<close> on the

   561     local parameter \<open>x\<close>. This element is deprecated. The type constraint

   562     should be introduced in the \<^theory_text>\<open>for\<close> clause or the relevant @{element

   563     "fixes"} element.

   564

   565     \<^descr> @{element "assumes"}~\<open>a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close> introduces local premises, similar

   566     to \<^theory_text>\<open>assume\<close> within a proof (cf.\ \secref{sec:proof-context}).

   567

   568     \<^descr> @{element "defines"}~\<open>a: x \<equiv> t\<close> defines a previously declared parameter.

   569     This is similar to \<^theory_text>\<open>define\<close> within a proof (cf.\

   570     \secref{sec:proof-context}), but @{element "defines"} is restricted to

   571     Pure equalities and the defined variable needs to be declared beforehand

   572     via @{element "fixes"}. The left-hand side of the equation may have

   573     additional arguments, e.g.\ @{element "defines"}~\<open>f x\<^sub>1 \<dots> x\<^sub>n \<equiv> t\<close>'',

   574     which need to be free in the context.

   575

   576     \<^descr> @{element "notes"}~\<open>a = b\<^sub>1 \<dots> b\<^sub>n\<close> reconsiders facts within a local

   577     context. Most notably, this may include arbitrary declarations in any

   578     attribute specifications included here, e.g.\ a local @{attribute simp}

   579     rule.

   580

   581   Both @{element "assumes"} and @{element "defines"} elements contribute to

   582   the locale specification. When defining an operation derived from the

   583   parameters, \<^theory_text>\<open>definition\<close> (\secref{sec:term-definitions}) is usually more

   584   appropriate.

   585

   586   Note that \<^theory_text>\<open>(is p\<^sub>1 \<dots> p\<^sub>n)\<close>'' patterns given in the syntax of @{element

   587   "assumes"} and @{element "defines"} above are illegal in locale definitions.

   588   In the long goal format of \secref{sec:goals}, term bindings may be included

   589   as expected, though.

   590

   591   \<^medskip>

   592   Locale specifications are closed up'' by turning the given text into a

   593   predicate definition \<open>loc_axioms\<close> and deriving the original assumptions as

   594   local lemmas (modulo local definitions). The predicate statement covers only

   595   the newly specified assumptions, omitting the content of included locale

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

   597   another predicate \<open>loc\<close> that refers to the complete specification text.

   598

   599   In any case, the predicate arguments are those locale parameters that

   600   actually occur in the respective piece of text. Also these predicates

   601   operate at the meta-level in theory, but the locale packages attempts to

   602   internalize statements according to the object-logic setup (e.g.\ replacing

   603   \<open>\<And>\<close> by \<open>\<forall>\<close>, and \<open>\<Longrightarrow>\<close> by \<open>\<longrightarrow>\<close> in HOL; see also \secref{sec:object-logic}).

   604   Separate introduction rules \<open>loc_axioms.intro\<close> and \<open>loc.intro\<close> are provided

   605   as well.

   606

   607   \<^descr> \<^theory_text>\<open>experiment exprs begin\<close> opens an anonymous locale context with private

   608   naming policy. Specifications in its body are inaccessible from outside.

   609   This is useful to perform experiments, without polluting the name space.

   610

   611   \<^descr> \<^theory_text>\<open>print_locale "locale"\<close> prints the contents of the named locale. The

   612   command omits @{element "notes"} elements by default. Use \<^theory_text>\<open>print_locale!\<close>

   613   to have them included.

   614

   615   \<^descr> \<^theory_text>\<open>print_locales\<close> prints the names of all locales of the current theory;

   616   the \<open>!\<close>'' option indicates extra verbosity.

   617

   618   \<^descr> \<^theory_text>\<open>locale_deps\<close> visualizes all locales and their relations as a Hasse

   619   diagram. This includes locales defined as type classes (\secref{sec:class}).

   620   See also \<^theory_text>\<open>print_dependencies\<close> below.

   621

   622   \<^descr> @{method intro_locales} and @{method unfold_locales} repeatedly expand all

   623   introduction rules of locale predicates of the theory. While @{method

   624   intro_locales} only applies the \<open>loc.intro\<close> introduction rules and therefore

   625   does not descend to assumptions, @{method unfold_locales} is more aggressive

   626   and applies \<open>loc_axioms.intro\<close> as well. Both methods are aware of locale

   627   specifications entailed by the context, both from target statements, and

   628   from interpretations (see below). New goals that are entailed by the current

   629   context are discharged automatically.

   630 \<close>

   631

   632

   633 subsection \<open>Locale interpretation \label{sec:locale-interpretation}\<close>

   634

   635 text \<open>

   636   \begin{matharray}{rcl}

   637     @{command "interpretation"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close> \\

   638     @{command_def "interpret"} & : & \<open>proof(state) | proof(chain) \<rightarrow> proof(prove)\<close> \\

   639     @{command_def "global_interpretation"} & : & \<open>theory | local_theory \<rightarrow> proof(prove)\<close> \\

   640     @{command_def "sublocale"} & : & \<open>theory | local_theory \<rightarrow> proof(prove)\<close> \\

   641     @{command_def "print_dependencies"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\

   642     @{command_def "print_interps"}\<open>\<^sup>*\<close> & :  & \<open>context \<rightarrow>\<close> \\

   643   \end{matharray}

   644

   645   Locales may be instantiated, and the resulting instantiated declarations

   646   added to the current context. This requires proof (of the instantiated

   647   specification) and is called \<^emph>\<open>locale interpretation\<close>. Interpretation is

   648   possible within arbitrary local theories (\<^theory_text>\<open>interpretation\<close>), within proof

   649   bodies (\<^theory_text>\<open>interpret\<close>), into global theories (\<^theory_text>\<open>global_interpretation\<close>) and

   650   into locales (\<^theory_text>\<open>sublocale\<close>).

   651

   652   \<^rail>\<open>

   653     @@{command interpretation} @{syntax locale_expr}

   654     ;

   655     @@{command interpret} @{syntax locale_expr}

   656     ;

   657     @@{command global_interpretation} @{syntax locale_expr} definitions?

   658     ;

   659     @@{command sublocale} (@{syntax name} ('<' | '\<subseteq>'))? @{syntax locale_expr} \<newline>

   660       definitions?

   661     ;

   662     @@{command print_dependencies} '!'? @{syntax locale_expr}

   663     ;

   664     @@{command print_interps} @{syntax name}

   665     ;

   666

   667     definitions: @'defines' (@{syntax thmdecl}? @{syntax name} \<newline>

   668       @{syntax mixfix}? @'=' @{syntax term} + @'and');

   669   \<close>

   670

   671   The core of each interpretation command is a locale expression \<open>expr\<close>; the

   672   command generates proof obligations for the instantiated specifications.

   673   Once these are discharged by the user, instantiated declarations (in

   674   particular, facts) are added to the context in a post-processing phase, in a

   675   manner specific to each command.

   676

   677   Interpretation commands are aware of interpretations that are already

   678   active: post-processing is achieved through a variant of roundup that takes

   679   interpretations of the current global or local theory into account. In order

   680   to simplify the proof obligations according to existing interpretations use

   681   methods @{method intro_locales} or @{method unfold_locales}.

   682

   683   Rewrites clauses \<^theory_text>\<open>rewrites eqns\<close> occur within expressions. They amend the

   684   morphism through which a locale instance is interpreted with rewrite rules,

   685   also called rewrite morphisms. This is particularly useful for interpreting

   686   concepts introduced through definitions. The equations must be proved the

   687   user. To enable syntax of the instantiated locale within the equation, while

   688   reading a locale expression, equations of a locale instance are read in a

   689   temporary context where the instance is already activated. If activation

   690   fails, typically due to duplicate constant declarations, processing falls

   691   back to reading the equation first.

   692

   693   Given definitions \<open>defs\<close> produce corresponding definitions in the local

   694   theory's underlying target \<^emph>\<open>and\<close> amend the morphism with rewrite rules

   695   stemming from the symmetric of those definitions. Hence these need not be

   696   proved explicitly the user. Such rewrite definitions are a even more useful

   697   device for interpreting concepts introduced through definitions, but they

   698   are only supported for interpretation commands operating in a local theory

   699   whose implementing target actually supports this.  Note that despite

   700   the suggestive \<^theory_text>\<open>and\<close> connective, \<open>defs\<close>

   701   are processed sequentially without mutual recursion.

   702

   703   \<^descr> \<^theory_text>\<open>interpretation expr\<close> interprets \<open>expr\<close> into a local theory

   704   such that its lifetime is limited to the current context block (e.g. a

   705   locale or unnamed context). At the closing @{command end} of the block the

   706   interpretation and its declarations disappear. Hence facts based on

   707   interpretation can be established without creating permanent links to the

   708   interpreted locale instances, as would be the case with @{command

   709   sublocale}.

   710

   711   When used on the level of a global theory, there is no end of a current

   712   context block, hence \<^theory_text>\<open>interpretation\<close> behaves identically to

   713   \<^theory_text>\<open>global_interpretation\<close> then.

   714

   715   \<^descr> \<^theory_text>\<open>interpret expr\<close> interprets \<open>expr\<close> into a proof context:

   716   the interpretation and its declarations disappear when closing the current

   717   proof block. Note that for \<^theory_text>\<open>interpret\<close> the \<open>eqns\<close> should be explicitly

   718   universally quantified.

   719

   720   \<^descr> \<^theory_text>\<open>global_interpretation defines defs\<close> interprets \<open>expr\<close>

   721   into a global theory.

   722

   723   When adding declarations to locales, interpreted versions of these

   724   declarations are added to the global theory for all interpretations in the

   725   global theory as well. That is, interpretations into global theories

   726   dynamically participate in any declarations added to locales.

   727

   728   Free variables in the interpreted expression are allowed. They are turned

   729   into schematic variables in the generated declarations. In order to use a

   730   free variable whose name is already bound in the context --- for example,

   731   because a constant of that name exists --- add it to the \<^theory_text>\<open>for\<close> clause.

   732

   733   \<^descr> \<^theory_text>\<open>sublocale name \<subseteq> expr defines defs\<close> interprets \<open>expr\<close>

   734   into the locale \<open>name\<close>. A proof that the specification of \<open>name\<close> implies the

   735   specification of \<open>expr\<close> is required. As in the localized version of the

   736   theorem command, the proof is in the context of \<open>name\<close>. After the proof

   737   obligation has been discharged, the locale hierarchy is changed as if \<open>name\<close>

   738   imported \<open>expr\<close> (hence the name \<^theory_text>\<open>sublocale\<close>). When the context of \<open>name\<close> is

   739   subsequently entered, traversing the locale hierarchy will involve the

   740   locale instances of \<open>expr\<close>, and their declarations will be added to the

   741   context. This makes \<^theory_text>\<open>sublocale\<close> dynamic: extensions of a locale that is

   742   instantiated in \<open>expr\<close> may take place after the \<^theory_text>\<open>sublocale\<close> declaration and

   743   still become available in the context. Circular \<^theory_text>\<open>sublocale\<close> declarations

   744   are allowed as long as they do not lead to infinite chains.

   745

   746   If interpretations of \<open>name\<close> exist in the current global theory, the command

   747   adds interpretations for \<open>expr\<close> as well, with the same qualifier, although

   748   only for fragments of \<open>expr\<close> that are not interpreted in the theory already.

   749

   750   Rewrites clauses in the expression or rewrite definitions \<open>defs\<close> can help break

   751   infinite chains induced by circular \<^theory_text>\<open>sublocale\<close> declarations.

   752

   753   In a named context block the \<^theory_text>\<open>sublocale\<close> command may also be used, but the

   754   locale argument must be omitted. The command then refers to the locale (or

   755   class) target of the context block.

   756

   757   \<^descr> \<^theory_text>\<open>print_dependencies expr\<close> is useful for understanding the effect of an

   758   interpretation of \<open>expr\<close> in the current context. It lists all locale

   759   instances for which interpretations would be added to the current context.

   760   Variant \<^theory_text>\<open>print_dependencies!\<close> does not generalize parameters and assumes an

   761   empty context --- that is, it prints all locale instances that would be

   762   considered for interpretation. The latter is useful for understanding the

   763   dependencies of a locale expression.

   764

   765   \<^descr> \<^theory_text>\<open>print_interps locale\<close> lists all interpretations of \<open>locale\<close> in the

   766   current theory or proof context, including those due to a combination of an

   767   \<^theory_text>\<open>interpretation\<close> or \<^theory_text>\<open>interpret\<close> and one or several \<^theory_text>\<open>sublocale\<close>

   768   declarations.

   769

   770   \begin{warn}

   771     If a global theory inherits declarations (body elements) for a locale from

   772     one parent and an interpretation of that locale from another parent, the

   773     interpretation will not be applied to the declarations.

   774   \end{warn}

   775

   776   \begin{warn}

   777     Since attributes are applied to interpreted theorems, interpretation may

   778     modify the context of common proof tools, e.g.\ the Simplifier or

   779     Classical Reasoner. As the behaviour of such tools is \<^emph>\<open>not\<close> stable under

   780     interpretation morphisms, manual declarations might have to be added to

   781     the target context of the interpretation to revert such declarations.

   782   \end{warn}

   783

   784   \begin{warn}

   785     An interpretation in a local theory or proof context may subsume previous

   786     interpretations. This happens if the same specification fragment is

   787     interpreted twice and the instantiation of the second interpretation is

   788     more general than the interpretation of the first. The locale package does

   789     not attempt to remove subsumed interpretations.

   790   \end{warn}

   791

   792   \begin{warn}

   793     While \<^theory_text>\<open>interpretation (in c) \<dots>\<close> is admissible, it is not useful since

   794     its result is discarded immediately.

   795   \end{warn}

   796 \<close>

   797

   798

   799 section \<open>Classes \label{sec:class}\<close>

   800

   801 text \<open>

   802   \begin{matharray}{rcl}

   803     @{command_def "class"} & : & \<open>theory \<rightarrow> local_theory\<close> \\

   804     @{command_def "instantiation"} & : & \<open>theory \<rightarrow> local_theory\<close> \\

   805     @{command_def "instance"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\

   806     @{command "instance"} & : & \<open>theory \<rightarrow> proof(prove)\<close> \\

   807     @{command_def "subclass"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\

   808     @{command_def "print_classes"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\

   809     @{command_def "class_deps"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\

   810     @{method_def intro_classes} & : & \<open>method\<close> \\

   811   \end{matharray}

   812

   813   A class is a particular locale with \<^emph>\<open>exactly one\<close> type variable \<open>\<alpha>\<close>. Beyond

   814   the underlying locale, a corresponding type class is established which is

   815   interpreted logically as axiomatic type class @{cite "Wenzel:1997:TPHOL"}

   816   whose logical content are the assumptions of the locale. Thus, classes

   817   provide the full generality of locales combined with the commodity of type

   818   classes (notably type-inference). See @{cite "isabelle-classes"} for a short

   819   tutorial.

   820

   821   \<^rail>\<open>

   822     @@{command class} class_spec @'begin'?

   823     ;

   824     class_spec: @{syntax name} '='

   825       ((@{syntax name} '+' (@{syntax context_elem}+)) |

   826         @{syntax name} | (@{syntax context_elem}+))

   827     ;

   828     @@{command instantiation} (@{syntax name} + @'and') '::' @{syntax arity} @'begin'

   829     ;

   830     @@{command instance} (() | (@{syntax name} + @'and') '::' @{syntax arity} |

   831       @{syntax name} ('<' | '\<subseteq>') @{syntax name} )

   832     ;

   833     @@{command subclass} @{syntax name}

   834     ;

   835     @@{command class_deps} (class_bounds class_bounds?)?

   836     ;

   837     class_bounds: @{syntax sort} | '(' (@{syntax sort} + @'|') ')'

   838   \<close>

   839

   840   \<^descr> \<^theory_text>\<open>class c = superclasses + body\<close> defines a new class \<open>c\<close>, inheriting from

   841   \<open>superclasses\<close>. This introduces a locale \<open>c\<close> with import of all locales

   842   \<open>superclasses\<close>.

   843

   844   Any @{element "fixes"} in \<open>body\<close> are lifted to the global theory level

   845   (\<^emph>\<open>class operations\<close> \<open>f\<^sub>1, \<dots>, f\<^sub>n\<close> of class \<open>c\<close>), mapping the local type

   846   parameter \<open>\<alpha>\<close> to a schematic type variable \<open>?\<alpha> :: c\<close>.

   847

   848   Likewise, @{element "assumes"} in \<open>body\<close> are also lifted, mapping each local

   849   parameter \<open>f :: \<tau>[\<alpha>]\<close> to its corresponding global constant \<open>f :: \<tau>[?\<alpha> ::

   850   c]\<close>. The corresponding introduction rule is provided as

   851   \<open>c_class_axioms.intro\<close>. This rule should be rarely needed directly --- the

   852   @{method intro_classes} method takes care of the details of class membership

   853   proofs.

   854

   855   \<^descr> \<^theory_text>\<open>instantiation t :: (s\<^sub>1, \<dots>, s\<^sub>n)s begin\<close> opens a target (cf.\

   856   \secref{sec:target}) which allows to specify class operations \<open>f\<^sub>1, \<dots>, f\<^sub>n\<close>

   857   corresponding to sort \<open>s\<close> at the particular type instance \<open>(\<alpha>\<^sub>1 :: s\<^sub>1, \<dots>,

   858   \<alpha>\<^sub>n :: s\<^sub>n) t\<close>. A plain \<^theory_text>\<open>instance\<close> command in the target body poses a goal

   859   stating these type arities. The target is concluded by an @{command_ref

   860   (local) "end"} command.

   861

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

   863   corresponds nicely to mutually recursive type definitions, e.g.\ in

   864   Isabelle/HOL.

   865

   866   \<^descr> \<^theory_text>\<open>instance\<close> in an instantiation target body sets up a goal stating the

   867   type arities claimed at the opening \<^theory_text>\<open>instantiation\<close>. The proof would

   868   usually proceed by @{method intro_classes}, and then establish the

   869   characteristic theorems of the type classes involved. After finishing the

   870   proof, the background theory will be augmented by the proven type arities.

   871

   872   On the theory level, \<^theory_text>\<open>instance t :: (s\<^sub>1, \<dots>, s\<^sub>n)s\<close> provides a convenient

   873   way to instantiate a type class with no need to specify operations: one can

   874   continue with the instantiation proof immediately.

   875

   876   \<^descr> \<^theory_text>\<open>subclass c\<close> in a class context for class \<open>d\<close> sets up a goal stating that

   877   class \<open>c\<close> is logically contained in class \<open>d\<close>. After finishing the proof,

   878   class \<open>d\<close> is proven to be subclass \<open>c\<close> and the locale \<open>c\<close> is interpreted

   879   into \<open>d\<close> simultaneously.

   880

   881   A weakened form of this is available through a further variant of @{command

   882   instance}: \<^theory_text>\<open>instance c\<^sub>1 \<subseteq> c\<^sub>2\<close> opens a proof that class \<open>c\<^sub>2\<close> implies

   883   \<open>c\<^sub>1\<close> without reference to the underlying locales; this is useful if the

   884   properties to prove the logical connection are not sufficient on the locale

   885   level but on the theory level.

   886

   887   \<^descr> \<^theory_text>\<open>print_classes\<close> prints all classes in the current theory.

   888

   889   \<^descr> \<^theory_text>\<open>class_deps\<close> visualizes classes and their subclass relations as a

   890   directed acyclic graph. By default, all classes from the current theory

   891   context are show. This may be restricted by optional bounds as follows:

   892   \<^theory_text>\<open>class_deps upper\<close> or \<^theory_text>\<open>class_deps upper lower\<close>. A class is visualized, iff

   893   it is a subclass of some sort from \<open>upper\<close> and a superclass of some sort

   894   from \<open>lower\<close>.

   895

   896   \<^descr> @{method intro_classes} repeatedly expands all class introduction rules of

   897   this theory. Note that this method usually needs not be named explicitly, as

   898   it is already included in the default proof step (e.g.\ of \<^theory_text>\<open>proof\<close>). In

   899   particular, instantiation of trivial (syntactic) classes may be performed by

   900   a single \<^theory_text>\<open>..\<close>'' proof step.

   901 \<close>

   902

   903

   904 subsection \<open>The class target\<close>

   905

   906 text \<open>

   907   %FIXME check

   908

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

   910   locale is also a class \<open>c\<close>, apart from the common locale target behaviour

   911   the following happens.

   912

   913     \<^item> Local constant declarations \<open>g[\<alpha>]\<close> referring to the local type parameter

   914     \<open>\<alpha>\<close> and local parameters \<open>f[\<alpha>]\<close> are accompanied by theory-level constants

   915     \<open>g[?\<alpha> :: c]\<close> referring to theory-level class operations \<open>f[?\<alpha> :: c]\<close>.

   916

   917     \<^item> Local theorem bindings are lifted as are assumptions.

   918

   919     \<^item> Local syntax refers to local operations \<open>g[\<alpha>]\<close> and global operations

   920     \<open>g[?\<alpha> :: c]\<close> uniformly. Type inference resolves ambiguities. In rare

   921     cases, manual type annotations are needed.

   922 \<close>

   923

   924

   925 subsection \<open>Co-regularity of type classes and arities\<close>

   926

   927 text \<open>

   928   The class relation together with the collection of type-constructor arities

   929   must obey the principle of \<^emph>\<open>co-regularity\<close> as defined below.

   930

   931   \<^medskip>

   932   For the subsequent formulation of co-regularity we assume that the class

   933   relation is closed by transitivity and reflexivity. Moreover the collection

   934   of arities \<open>t :: (\<^vec>s)c\<close> is completed such that \<open>t :: (\<^vec>s)c\<close> and

   935   \<open>c \<subseteq> c'\<close> implies \<open>t :: (\<^vec>s)c'\<close> for all such declarations.

   936

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

   938   class relation \<open>c\<^sub>1 \<subseteq> c\<^sub>2\<close> is extended to sorts as follows:

   939   $  940 \<open>s\<^sub>1 \<subseteq> s\<^sub>2 \<equiv> \<forall>c\<^sub>2 \<in> s\<^sub>2. \<exists>c\<^sub>1 \<in> s\<^sub>1. c\<^sub>1 \<subseteq> c\<^sub>2\<close>   941$

   942

   943   This relation on sorts is further extended to tuples of sorts (of the same

   944   length) in the component-wise way.

   945

   946   \<^medskip>

   947   Co-regularity of the class relation together with the arities relation

   948   means:

   949   $  950 \<open>t :: (\<^vec>s\<^sub>1)c\<^sub>1 \<Longrightarrow> t :: (\<^vec>s\<^sub>2)c\<^sub>2 \<Longrightarrow> c\<^sub>1 \<subseteq> c\<^sub>2 \<Longrightarrow> \<^vec>s\<^sub>1 \<subseteq> \<^vec>s\<^sub>2\<close>   951$

   952   for all such arities. In other words, whenever the result classes of some

   953   type-constructor arities are related, then the argument sorts need to be

   954   related in the same way.

   955

   956   \<^medskip>

   957   Co-regularity is a very fundamental property of the order-sorted algebra of

   958   types. For example, it entails principle types and most general unifiers,

   959   e.g.\ see @{cite "nipkow-prehofer"}.

   960 \<close>

   961

   962

   963 section \<open>Overloaded constant definitions \label{sec:overloading}\<close>

   964

   965 text \<open>

   966   Definitions essentially express abbreviations within the logic. The simplest

   967   form of a definition is \<open>c :: \<sigma> \<equiv> t\<close>, where \<open>c\<close> is a new constant and \<open>t\<close> is

   968   a closed term that does not mention \<open>c\<close>. Moreover, so-called \<^emph>\<open>hidden

   969   polymorphism\<close> is excluded: all type variables in \<open>t\<close> need to occur in its

   970   type \<open>\<sigma>\<close>.

   971

   972   \<^emph>\<open>Overloading\<close> means that a constant being declared as \<open>c :: \<alpha> decl\<close> may be

   973   defined separately on type instances \<open>c :: (\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n)\<kappa> decl\<close> for each

   974   type constructor \<open>\<kappa>\<close>. At most occasions overloading will be used in a

   975   Haskell-like fashion together with type classes by means of \<^theory_text>\<open>instantiation\<close>

   976   (see \secref{sec:class}). Sometimes low-level overloading is desirable; this

   977   is supported by \<^theory_text>\<open>consts\<close> and \<^theory_text>\<open>overloading\<close> explained below.

   978

   979   The right-hand side of overloaded definitions may mention overloaded

   980   constants recursively at type instances corresponding to the immediate

   981   argument types \<open>\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n\<close>. Incomplete specification patterns impose

   982   global constraints on all occurrences. E.g.\ \<open>d :: \<alpha> \<times> \<alpha>\<close> on the left-hand

   983   side means that all corresponding occurrences on some right-hand side need

   984   to be an instance of this, and general \<open>d :: \<alpha> \<times> \<beta>\<close> will be disallowed. Full

   985   details are given by Kun\v{c}ar @{cite "Kuncar:2015"}.

   986

   987   \<^medskip>

   988   The \<^theory_text>\<open>consts\<close> command and the \<^theory_text>\<open>overloading\<close> target provide a convenient

   989   interface for end-users. Regular specification elements such as @{command

   990   definition}, @{command inductive}, @{command function} may be used in the

   991   body. It is also possible to use \<^theory_text>\<open>consts c :: \<sigma>\<close> with later \<^theory_text>\<open>overloading c

   992   \<equiv> c :: \<sigma>\<close> to keep the declaration and definition of a constant separate.

   993

   994   \begin{matharray}{rcl}

   995     @{command_def "consts"} & : & \<open>theory \<rightarrow> theory\<close> \\

   996     @{command_def "overloading"} & : & \<open>theory \<rightarrow> local_theory\<close> \\

   997   \end{matharray}

   998

   999   \<^rail>\<open>

  1000     @@{command consts} ((@{syntax name} '::' @{syntax type} @{syntax mixfix}?) +)

  1001     ;

  1002     @@{command overloading} ( spec + ) @'begin'

  1003     ;

  1004     spec: @{syntax name} ( '\<equiv>' | '==' ) @{syntax term} ( '(' @'unchecked' ')' )?

  1005   \<close>

  1006

  1007   \<^descr> \<^theory_text>\<open>consts c :: \<sigma>\<close> declares constant \<open>c\<close> to have any instance of type scheme

  1008   \<open>\<sigma>\<close>. The optional mixfix annotations may attach concrete syntax to the

  1009   constants declared.

  1010

  1011   \<^descr> \<^theory_text>\<open>overloading x\<^sub>1 \<equiv> c\<^sub>1 :: \<tau>\<^sub>1 \<dots> x\<^sub>n \<equiv> c\<^sub>n :: \<tau>\<^sub>n begin \<dots> end\<close> defines

  1012   a theory target (cf.\ \secref{sec:target}) which allows to specify already

  1013   declared constants via definitions in the body. These are identified by an

  1014   explicitly given mapping from variable names \<open>x\<^sub>i\<close> to constants \<open>c\<^sub>i\<close> at

  1015   particular type instances. The definitions themselves are established using

  1016   common specification tools, using the names \<open>x\<^sub>i\<close> as reference to the

  1017   corresponding constants.

  1018

  1019   Option \<^theory_text>\<open>(unchecked)\<close> disables global dependency checks for the

  1020   corresponding definition, which is occasionally useful for exotic

  1021   overloading; this is a form of axiomatic specification. It is at the

  1022   discretion of the user to avoid malformed theory specifications!

  1023 \<close>

  1024

  1025

  1026 subsubsection \<open>Example\<close>

  1027

  1028 consts Length :: "'a \<Rightarrow> nat"

  1029

  1030 overloading

  1031   Length\<^sub>0 \<equiv> "Length :: unit \<Rightarrow> nat"

  1032   Length\<^sub>1 \<equiv> "Length :: 'a \<times> unit \<Rightarrow> nat"

  1033   Length\<^sub>2 \<equiv> "Length :: 'a \<times> 'b \<times> unit \<Rightarrow> nat"

  1034   Length\<^sub>3 \<equiv> "Length :: 'a \<times> 'b \<times> 'c \<times> unit \<Rightarrow> nat"

  1035 begin

  1036

  1037 fun Length\<^sub>0 :: "unit \<Rightarrow> nat" where "Length\<^sub>0 () = 0"

  1038 fun Length\<^sub>1 :: "'a \<times> unit \<Rightarrow> nat" where "Length\<^sub>1 (a, ()) = 1"

  1039 fun Length\<^sub>2 :: "'a \<times> 'b \<times> unit \<Rightarrow> nat" where "Length\<^sub>2 (a, b, ()) = 2"

  1040 fun Length\<^sub>3 :: "'a \<times> 'b \<times> 'c \<times> unit \<Rightarrow> nat" where "Length\<^sub>3 (a, b, c, ()) = 3"

  1041

  1042 end

  1043

  1044 lemma "Length (a, b, c, ()) = 3" by simp

  1045 lemma "Length ((a, b), (c, d), ()) = 2" by simp

  1046 lemma "Length ((a, b, c, d, e), ()) = 1" by simp

  1047

  1048

  1049 section \<open>Incorporating ML code \label{sec:ML}\<close>

  1050

  1051 text \<open>

  1052   \begin{matharray}{rcl}

  1053     @{command_def "SML_file"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\

  1054     @{command_def "SML_file_debug"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\

  1055     @{command_def "SML_file_no_debug"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\

  1056     @{command_def "ML_file"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\

  1057     @{command_def "ML_file_debug"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\

  1058     @{command_def "ML_file_no_debug"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\

  1059     @{command_def "ML"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\

  1060     @{command_def "ML_export"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\

  1061     @{command_def "ML_prf"} & : & \<open>proof \<rightarrow> proof\<close> \\

  1062     @{command_def "ML_val"} & : & \<open>any \<rightarrow>\<close> \\

  1063     @{command_def "ML_command"} & : & \<open>any \<rightarrow>\<close> \\

  1064     @{command_def "setup"} & : & \<open>theory \<rightarrow> theory\<close> \\

  1065     @{command_def "local_setup"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\

  1066     @{command_def "attribute_setup"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\

  1067   \end{matharray}

  1068   \begin{tabular}{rcll}

  1069     @{attribute_def ML_print_depth} & : & \<open>attribute\<close> & default 10 \\

  1070     @{attribute_def ML_source_trace} & : & \<open>attribute\<close> & default \<open>false\<close> \\

  1071     @{attribute_def ML_debugger} & : & \<open>attribute\<close> & default \<open>false\<close> \\

  1072     @{attribute_def ML_exception_trace} & : & \<open>attribute\<close> & default \<open>false\<close> \\

  1073     @{attribute_def ML_exception_debugger} & : & \<open>attribute\<close> & default \<open>false\<close> \\

  1074   \end{tabular}

  1075

  1076   \<^rail>\<open>

  1077     (@@{command SML_file} |

  1078       @@{command SML_file_debug} |

  1079       @@{command SML_file_no_debug} |

  1080       @@{command ML_file} |

  1081       @@{command ML_file_debug} |

  1082       @@{command ML_file_no_debug}) @{syntax name} ';'?

  1083     ;

  1084     (@@{command ML} | @@{command ML_export} | @@{command ML_prf} |

  1085       @@{command ML_val} | @@{command ML_command} | @@{command setup} |

  1086       @@{command local_setup}) @{syntax text}

  1087     ;

  1088     @@{command attribute_setup} @{syntax name} '=' @{syntax text} @{syntax text}?

  1089   \<close>

  1090

  1091   \<^descr> \<^theory_text>\<open>SML_file name\<close> reads and evaluates the given Standard ML file. Top-level

  1092   SML bindings are stored within the (global or local) theory context; the

  1093   initial environment is restricted to the Standard ML implementation of

  1094   Poly/ML, without the many add-ons of Isabelle/ML. Multiple \<^theory_text>\<open>SML_file\<close>

  1095   commands may be used to build larger Standard ML projects, independently of

  1096   the regular Isabelle/ML environment.

  1097

  1098   \<^descr> \<^theory_text>\<open>ML_file name\<close> reads and evaluates the given ML file. The current theory

  1099   context is passed down to the ML toplevel and may be modified, using \<^ML>\<open>Context.>>\<close> or derived ML commands. Top-level ML bindings are stored

  1100   within the (global or local) theory context.

  1101

  1102   \<^descr> \<^theory_text>\<open>SML_file_debug\<close>, \<^theory_text>\<open>SML_file_no_debug\<close>, \<^theory_text>\<open>ML_file_debug\<close>, and

  1103   \<^theory_text>\<open>ML_file_no_debug\<close> change the @{attribute ML_debugger} option locally while

  1104   the given file is compiled.

  1105

  1106   \<^descr> \<^theory_text>\<open>ML\<close> is similar to \<^theory_text>\<open>ML_file\<close>, but evaluates directly the given \<open>text\<close>.

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

  1108   context.

  1109

  1110   \<^descr> \<^theory_text>\<open>ML_export\<close> is similar to \<^theory_text>\<open>ML\<close>, but the resulting toplevel bindings are

  1111   exported to the global bootstrap environment of the ML process --- it has

  1112   a lasting effect that cannot be retracted. This allows ML evaluation

  1113   without a formal theory context, e.g. for command-line tools via @{tool

  1114   process} @{cite "isabelle-system"}.

  1115

  1116   \<^descr> \<^theory_text>\<open>ML_prf\<close> is analogous to \<^theory_text>\<open>ML\<close> but works within a proof context.

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

  1118   sequential fashion, disregarding the nested proof structure. ML bindings

  1119   introduced by \<^theory_text>\<open>ML_prf\<close> are discarded at the end of the proof.

  1120

  1121   \<^descr> \<^theory_text>\<open>ML_val\<close> and \<^theory_text>\<open>ML_command\<close> are diagnostic versions of \<^theory_text>\<open>ML\<close>, which means

  1122   that the context may not be updated. \<^theory_text>\<open>ML_val\<close> echos the bindings produced

  1123   at the ML toplevel, but \<^theory_text>\<open>ML_command\<close> is silent.

  1124

  1125   \<^descr> \<^theory_text>\<open>setup "text"\<close> changes the current theory context by applying \<open>text\<close>,

  1126   which refers to an ML expression of type \<^ML_type>\<open>theory -> theory\<close>. This

  1127   enables to initialize any object-logic specific tools and packages written

  1128   in ML, for example.

  1129

  1130   \<^descr> \<^theory_text>\<open>local_setup\<close> is similar to \<^theory_text>\<open>setup\<close> for a local theory context, and an

  1131   ML expression of type \<^ML_type>\<open>local_theory -> local_theory\<close>. This allows

  1132   to invoke local theory specification packages without going through concrete

  1133   outer syntax, for example.

  1134

  1135   \<^descr> \<^theory_text>\<open>attribute_setup name = "text" description\<close> defines an attribute in the

  1136   current context. The given \<open>text\<close> has to be an ML expression of type

  1137   \<^ML_type>\<open>attribute context_parser\<close>, cf.\ basic parsers defined in

  1138   structure \<^ML_structure>\<open>Args\<close> and \<^ML_structure>\<open>Attrib\<close>.

  1139

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

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

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

  1143 \<close>

  1144

  1145 (*<*)experiment begin(*>*)

  1146         attribute_setup my_rule =

  1147           \<open>Attrib.thms >> (fn ths =>

  1148             Thm.rule_attribute ths

  1149               (fn context: Context.generic => fn th: thm =>

  1150                 let val th' = th OF ths

  1151                 in th' end))\<close>

  1152

  1153         attribute_setup my_declaration =

  1154           \<open>Attrib.thms >> (fn ths =>

  1155             Thm.declaration_attribute

  1156               (fn th: thm => fn context: Context.generic =>

  1157                 let val context' = context

  1158                 in context' end))\<close>

  1159 (*<*)end(*>*)

  1160

  1161 text \<open>

  1162   \<^descr> @{attribute ML_print_depth} controls the printing depth of the ML toplevel

  1163   pretty printer. Typically the limit should be less than 10. Bigger values

  1164   such as 100--1000 are occasionally useful for debugging.

  1165

  1166   \<^descr> @{attribute ML_source_trace} indicates whether the source text that is

  1167   given to the ML compiler should be output: it shows the raw Standard ML

  1168   after expansion of Isabelle/ML antiquotations.

  1169

  1170   \<^descr> @{attribute ML_debugger} controls compilation of sources with or without

  1171   debugging information. The global system option @{system_option_ref

  1172   ML_debugger} does the same when building a session image. It is also

  1173   possible use commands like \<^theory_text>\<open>ML_file_debug\<close> etc. The ML debugger is

  1174   explained further in @{cite "isabelle-jedit"}.

  1175

  1176   \<^descr> @{attribute ML_exception_trace} indicates whether the ML run-time system

  1177   should print a detailed stack trace on exceptions. The result is dependent

  1178   on various ML compiler optimizations. The boundary for the exception trace

  1179   is the current Isar command transactions: it is occasionally better to

  1180   insert the combinator \<^ML>\<open>Runtime.exn_trace\<close> into ML code for debugging

  1181   @{cite "isabelle-implementation"}, closer to the point where it actually

  1182   happens.

  1183

  1184   \<^descr> @{attribute ML_exception_debugger} controls detailed exception trace via

  1185   the Poly/ML debugger, at the cost of extra compile-time and run-time

  1186   overhead. Relevant ML modules need to be compiled beforehand with debugging

  1187   enabled, see @{attribute ML_debugger} above.

  1188 \<close>

  1189

  1190

  1191 section \<open>External file dependencies\<close>

  1192

  1193 text \<open>

  1194   \begin{matharray}{rcl}

  1195     @{command_def "external_file"} & : & \<open>any \<rightarrow> any\<close> \\

  1196   \end{matharray}

  1197

  1198   \<^rail>\<open>@@{command external_file} @{syntax name} ';'?\<close>

  1199

  1200   \<^descr> \<^theory_text>\<open>external_file name\<close> declares the formal dependency on the given file

  1201   name, such that the Isabelle build process knows about it (see also @{cite

  1202   "isabelle-system"}). The file can be read e.g.\ in Isabelle/ML via \<^ML>\<open>File.read\<close>, without specific management by the Prover IDE.

  1203 \<close>

  1204

  1205

  1206

  1207 section \<open>Primitive specification elements\<close>

  1208

  1209 subsection \<open>Sorts\<close>

  1210

  1211 text \<open>

  1212   \begin{matharray}{rcll}

  1213     @{command_def "default_sort"} & : & \<open>local_theory \<rightarrow> local_theory\<close>

  1214   \end{matharray}

  1215

  1216   \<^rail>\<open>

  1217     @@{command default_sort} @{syntax sort}

  1218   \<close>

  1219

  1220   \<^descr> \<^theory_text>\<open>default_sort s\<close> makes sort \<open>s\<close> the new default sort for any type

  1221   variable that is given explicitly in the text, but lacks a sort constraint

  1222   (wrt.\ the current context). Type variables generated by type inference are

  1223   not affected.

  1224

  1225   Usually the default sort is only changed when defining a new object-logic.

  1226   For example, the default sort in Isabelle/HOL is \<^class>\<open>type\<close>, the class of

  1227   all HOL types.

  1228

  1229   When merging theories, the default sorts of the parents are logically

  1230   intersected, i.e.\ the representations as lists of classes are joined.

  1231 \<close>

  1232

  1233

  1234 subsection \<open>Types \label{sec:types-pure}\<close>

  1235

  1236 text \<open>

  1237   \begin{matharray}{rcll}

  1238     @{command_def "type_synonym"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\

  1239     @{command_def "typedecl"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\

  1240   \end{matharray}

  1241

  1242   \<^rail>\<open>

  1243     @@{command type_synonym} (@{syntax typespec} '=' @{syntax type} @{syntax mixfix}?)

  1244     ;

  1245     @@{command typedecl} @{syntax typespec} @{syntax mixfix}?

  1246   \<close>

  1247

  1248   \<^descr> \<^theory_text>\<open>type_synonym (\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = \<tau>\<close> introduces a \<^emph>\<open>type synonym\<close> \<open>(\<alpha>\<^sub>1, \<dots>,

  1249   \<alpha>\<^sub>n) t\<close> for the existing type \<open>\<tau>\<close>. Unlike the semantic type definitions in

  1250   Isabelle/HOL, type synonyms are merely syntactic abbreviations without any

  1251   logical significance. Internally, type synonyms are fully expanded.

  1252

  1253   \<^descr> \<^theory_text>\<open>typedecl (\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t\<close> declares a new type constructor \<open>t\<close>. If the

  1254   object-logic defines a base sort \<open>s\<close>, then the constructor is declared to

  1255   operate on that, via the axiomatic type-class instance \<open>t :: (s, \<dots>, s)s\<close>.

  1256

  1257

  1258   \begin{warn}

  1259     If you introduce a new type axiomatically, i.e.\ via @{command_ref

  1260     typedecl} and @{command_ref axiomatization}

  1261     (\secref{sec:axiomatizations}), the minimum requirement is that it has a

  1262     non-empty model, to avoid immediate collapse of the logical environment.

  1263     Moreover, one needs to demonstrate that the interpretation of such

  1264     free-form axiomatizations can coexist with other axiomatization schemes

  1265     for types, notably @{command_def typedef} in Isabelle/HOL

  1266     (\secref{sec:hol-typedef}), or any other extension that people might have

  1267     introduced elsewhere.

  1268   \end{warn}

  1269 \<close>

  1270

  1271

  1272 section \<open>Naming existing theorems \label{sec:theorems}\<close>

  1273

  1274 text \<open>

  1275   \begin{matharray}{rcll}

  1276     @{command_def "lemmas"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\

  1277     @{command_def "named_theorems"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\

  1278   \end{matharray}

  1279

  1280   \<^rail>\<open>

  1281     @@{command lemmas} (@{syntax thmdef}? @{syntax thms} + @'and')

  1282       @{syntax for_fixes}

  1283     ;

  1284     @@{command named_theorems} (@{syntax name} @{syntax text}? + @'and')

  1285   \<close>

  1286

  1287   \<^descr> \<^theory_text>\<open>lemmas a = b\<^sub>1 \<dots> b\<^sub>n\<close>~@{keyword_def "for"}~\<open>x\<^sub>1 \<dots> x\<^sub>m\<close> evaluates given

  1288   facts (with attributes) in the current context, which may be augmented by

  1289   local variables. Results are standardized before being stored, i.e.\

  1290   schematic variables are renamed to enforce index \<open>0\<close> uniformly.

  1291

  1292   \<^descr> \<^theory_text>\<open>named_theorems name description\<close> declares a dynamic fact within the

  1293   context. The same \<open>name\<close> is used to define an attribute with the usual

  1294   \<open>add\<close>/\<open>del\<close> syntax (e.g.\ see \secref{sec:simp-rules}) to maintain the

  1295   content incrementally, in canonical declaration order of the text structure.

  1296 \<close>

  1297

  1298

  1299 section \<open>Oracles\<close>

  1300

  1301 text \<open>

  1302   \begin{matharray}{rcll}

  1303     @{command_def "oracle"} & : & \<open>theory \<rightarrow> theory\<close> & (axiomatic!) \\

  1304   \end{matharray}

  1305

  1306   Oracles allow Isabelle to take advantage of external reasoners such as

  1307   arithmetic decision procedures, model checkers, fast tautology checkers or

  1308   computer algebra systems. Invoked as an oracle, an external reasoner can

  1309   create arbitrary Isabelle theorems.

  1310

  1311   It is the responsibility of the user to ensure that the external reasoner is

  1312   as trustworthy as the application requires. Another typical source of errors

  1313   is the linkup between Isabelle and the external tool, not just its concrete

  1314   implementation, but also the required translation between two different

  1315   logical environments.

  1316

  1317   Isabelle merely guarantees well-formedness of the propositions being

  1318   asserted, and records within the internal derivation object how presumed

  1319   theorems depend on unproven suppositions.

  1320

  1321   \<^rail>\<open>

  1322     @@{command oracle} @{syntax name} '=' @{syntax text}

  1323   \<close>

  1324

  1325   \<^descr> \<^theory_text>\<open>oracle name = "text"\<close> turns the given ML expression \<open>text\<close> of type

  1326   \<^ML_text>\<open>'a -> cterm\<close> into an ML function of type \<^ML_text>\<open>'a -> thm\<close>,

  1327   which is bound to the global identifier \<^ML_text>\<open>name\<close>. This acts like an

  1328   infinitary specification of axioms! Invoking the oracle only works within

  1329   the scope of the resulting theory.

  1330

  1331

  1332   See \<^file>\<open>~~/src/HOL/ex/Iff_Oracle.thy\<close> for a worked example of defining a new

  1333   primitive rule as oracle, and turning it into a proof method.

  1334 \<close>

  1335

  1336

  1337 section \<open>Name spaces\<close>

  1338

  1339 text \<open>

  1340   \begin{matharray}{rcl}

  1341     @{command_def "alias"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\

  1342     @{command_def "type_alias"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\

  1343     @{command_def "hide_class"} & : & \<open>theory \<rightarrow> theory\<close> \\

  1344     @{command_def "hide_type"} & : & \<open>theory \<rightarrow> theory\<close> \\

  1345     @{command_def "hide_const"} & : & \<open>theory \<rightarrow> theory\<close> \\

  1346     @{command_def "hide_fact"} & : & \<open>theory \<rightarrow> theory\<close> \\

  1347   \end{matharray}

  1348

  1349   \<^rail>\<open>

  1350     (@{command alias} | @{command type_alias}) @{syntax name} '=' @{syntax name}

  1351     ;

  1352     (@{command hide_class} | @{command hide_type} |

  1353       @{command hide_const} | @{command hide_fact}) ('(' @'open' ')')? (@{syntax name} + )

  1354   \<close>

  1355

  1356   Isabelle organizes any kind of name declarations (of types, constants,

  1357   theorems etc.) by separate hierarchically structured name spaces. Normally

  1358   the user does not have to control the behaviour of name spaces by hand, yet

  1359   the following commands provide some way to do so.

  1360

  1361   \<^descr> \<^theory_text>\<open>alias\<close> and \<^theory_text>\<open>type_alias\<close> introduce aliases for constants and type

  1362   constructors, respectively. This allows adhoc changes to name-space

  1363   accesses.

  1364

  1365   \<^descr> \<^theory_text>\<open>type_alias b = c\<close> introduces an alias for an existing type constructor.

  1366

  1367   \<^descr> \<^theory_text>\<open>hide_class names\<close> fully removes class declarations from a given name

  1368   space; with the \<open>(open)\<close> option, only the unqualified base name is hidden.

  1369

  1370   Note that hiding name space accesses has no impact on logical declarations

  1371   --- they remain valid internally. Entities that are no longer accessible to

  1372   the user are printed with the special qualifier \<open>??\<close>'' prefixed to the

  1373   full internal name.

  1374

  1375   \<^descr> \<^theory_text>\<open>hide_type\<close>, \<^theory_text>\<open>hide_const\<close>, and \<^theory_text>\<open>hide_fact\<close> are similar to

  1376   \<^theory_text>\<open>hide_class\<close>, but hide types, constants, and facts, respectively.

  1377 \<close>

  1378

  1379 end