1(*:maxLineLen=78:*)
2
3theory Spec
4  imports Main Base
5begin
6
7chapter \<open>Specifications\<close>
8
9text \<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
24section \<open>Defining theories \label{sec:begin-thy}\<close>
25
26text \<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 Pure}, 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 Main} 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\<close> or @{keyword "keywords"}~\<^verbatim>\<open>"datatype"\<close> \<open>:: thy_decl\<close> for
97  theory-level declarations 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
117section \<open>Local theory targets \label{sec:target}\<close>
118
119text \<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
206section \<open>Bundled declarations \label{sec:bundle}\<close>
207
208text \<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(*>*)
279bundle trace = [[simp_trace, linarith_trace, metis_trace, smt_trace]]
280
281lemma "x = x"
282  including trace by metis
283(*<*)end(*>*)
284
285
286section \<open>Term definitions \label{sec:term-definitions}\<close>
287
288text \<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
351section \<open>Axiomatizations \label{sec:axiomatizations}\<close>
352
353text \<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
385section \<open>Generic declarations\<close>
386
387text \<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
410  declaration}, to the current local theory under construction. In later
411  application contexts, the function is transformed according to the morphisms
412  being involved in the interpretation hierarchy.
413
414  If the \<^theory_text>\<open>(pervasive)\<close> option is given, the corresponding declaration is
415  applied to all possible contexts involved, including the global background
416  theory.
417
418  \<^descr> \<^theory_text>\<open>syntax_declaration\<close> is similar to \<^theory_text>\<open>declaration\<close>, but is meant to affect
419  only ``syntactic'' tools by convention (such as notation and type-checking
420  information).
421
422  \<^descr> \<^theory_text>\<open>declare thms\<close> declares theorems to the current local theory context. No
423  theorem binding is involved here, unlike \<^theory_text>\<open>lemmas\<close> (cf.\
424  \secref{sec:theorems}), so \<^theory_text>\<open>declare\<close> only has the effect of applying
425  attributes as included in the theorem specification.
426\<close>
427
428
429section \<open>Locales \label{sec:locale}\<close>
430
431text \<open>
432  A locale is a functor that maps parameters (including implicit type
433  parameters) and a specification to a list of declarations. The syntax of
434  locales is modeled after the Isar proof context commands (cf.\
435  \secref{sec:proof-context}).
436
437  Locale hierarchies are supported by maintaining a graph of dependencies
438  between locale instances in the global theory. Dependencies may be
439  introduced through import (where a locale is defined as sublocale of the
440  imported instances) or by proving that an existing locale is a sublocale of
441  one or several locale instances.
442
443  A locale may be opened with the purpose of appending to its list of
444  declarations (cf.\ \secref{sec:target}). When opening a locale declarations
445  from all dependencies are collected and are presented as a local theory. In
446  this process, which is called \<^emph>\<open>roundup\<close>, redundant locale instances are
447  omitted. A locale instance is redundant if it is subsumed by an instance
448  encountered earlier. A more detailed description of this process is
449  available elsewhere @{cite Ballarin2014}.
450\<close>
451
452
453subsection \<open>Locale expressions \label{sec:locale-expr}\<close>
454
455text \<open>
456  A \<^emph>\<open>locale expression\<close> denotes a context composed of instances of existing
457  locales. The context consists of the declaration elements from the locale
458  instances. Redundant locale instances are omitted according to roundup.
459
460  @{rail \<open>
461    @{syntax_def locale_expr}: (instance + '+') @{syntax for_fixes}
462    ;
463    instance: (qualifier ':')? @{syntax name} (pos_insts | named_insts) \<newline>
464      rewrites?
465    ;
466    qualifier: @{syntax name} ('?')?
467    ;
468    pos_insts: ('_' | @{syntax term})*
469    ;
470    named_insts: @'where' (@{syntax name} '=' @{syntax term} + @'and')
471    ;
472    rewrites: @'rewrites' (@{syntax thmdecl}? @{syntax prop} + @'and')
473  \<close>}
474
475  A locale instance consists of a reference to a locale and either positional
476  or named parameter instantiations optionally followed by rewrites clauses.
477  Identical instantiations (that is, those
478  that instantiate a parameter by itself) may be omitted. The notation ``\<open>_\<close>''
479  enables to omit the instantiation for a parameter inside a positional
480  instantiation.
481
482  Terms in instantiations are from the context the locale expressions is
483  declared in. Local names may be added to this context with the optional
484  \<^theory_text>\<open>for\<close> clause. This is useful for shadowing names bound in outer contexts,
485  and for declaring syntax. In addition, syntax declarations from one instance
486  are effective when parsing subsequent instances of the same expression.
487
488  Instances have an optional qualifier which applies to names in declarations.
489  Names include local definitions and theorem names. If present, the qualifier
490  itself is either mandatory (default) or non-mandatory (when followed by
491  ``\<^verbatim>\<open>?\<close>''). Non-mandatory means that the qualifier may be omitted on input.
492  Qualifiers only affect name spaces; they play no role in determining whether
493  one locale instance subsumes another.
494
495  Rewrite clauses amend instances with equations that act as rewrite rules.
496  This is particularly useful for changing concepts introduced through
497  definitions. Rewrite clauses are available only in interpretation commands
498  (see \secref{sec:locale-interpretation} below) and must be proved the user.
499\<close>
500
501
502subsection \<open>Locale declarations\<close>
503
504text \<open>
505  \begin{matharray}{rcl}
506    @{command_def "locale"} & : & \<open>theory \<rightarrow> local_theory\<close> \\
507    @{command_def "experiment"} & : & \<open>theory \<rightarrow> local_theory\<close> \\
508    @{command_def "print_locale"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
509    @{command_def "print_locales"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
510    @{command_def "locale_deps"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
511    @{method_def intro_locales} & : & \<open>method\<close> \\
512    @{method_def unfold_locales} & : & \<open>method\<close> \\
513  \end{matharray}
514
515  \indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes}
516  \indexisarelem{defines}\indexisarelem{notes}
517  @{rail \<open>
518    @@{command locale} @{syntax name} ('=' @{syntax locale})? @'begin'?
519    ;
520    @@{command experiment} (@{syntax context_elem}*) @'begin'
521    ;
522    @@{command print_locale} '!'? @{syntax name}
523    ;
524    @@{command print_locales} ('!'?)
525    ;
526    @{syntax_def locale}: @{syntax context_elem}+ |
527      @{syntax locale_expr} ('+' (@{syntax context_elem}+))?
528    ;
529    @{syntax_def context_elem}:
530      @'fixes' @{syntax vars} |
531      @'constrains' (@{syntax name} '::' @{syntax type} + @'and') |
532      @'assumes' (@{syntax props} + @'and') |
533      @'defines' (@{syntax thmdecl}? @{syntax prop} @{syntax prop_pat}? + @'and') |
534      @'notes' (@{syntax thmdef}? @{syntax thms} + @'and')
535  \<close>}
536
537  \<^descr> \<^theory_text>\<open>locale loc = import + body\<close> defines a new locale \<open>loc\<close> as a context
538  consisting of a certain view of existing locales (\<open>import\<close>) plus some
539  additional elements (\<open>body\<close>). Both \<open>import\<close> and \<open>body\<close> are optional; the
540  degenerate form \<^theory_text>\<open>locale loc\<close> defines an empty locale, which may still be
541  useful to collect declarations of facts later on. Type-inference on locale
542  expressions automatically takes care of the most general typing that the
543  combined context elements may acquire.
544
545  The \<open>import\<close> consists of a locale expression; see \secref{sec:proof-context}
546  above. Its \<^theory_text>\<open>for\<close> clause defines the parameters of \<open>import\<close>. These are
547  parameters of the defined locale. Locale parameters whose instantiation is
548  omitted automatically extend the (possibly empty) \<^theory_text>\<open>for\<close> clause: they are
549  inserted at its beginning. This means that these parameters may be referred
550  to from within the expression and also in the subsequent context elements
551  and provides a notational convenience for the inheritance of parameters in
552  locale declarations.
553
554  The \<open>body\<close> consists of context elements.
555
556    \<^descr> @{element "fixes"}~\<open>x :: \<tau> (mx)\<close> declares a local parameter of type \<open>\<tau>\<close>
557    and mixfix annotation \<open>mx\<close> (both are optional). The special syntax
558    declaration ``\<open>(\<close>@{keyword_ref "structure"}\<open>)\<close>'' means that \<open>x\<close> may be
559    referenced implicitly in this context.
560
561    \<^descr> @{element "constrains"}~\<open>x :: \<tau>\<close> introduces a type constraint \<open>\<tau>\<close> on the
562    local parameter \<open>x\<close>. This element is deprecated. The type constraint
563    should be introduced in the \<^theory_text>\<open>for\<close> clause or the relevant @{element
564    "fixes"} element.
565
566    \<^descr> @{element "assumes"}~\<open>a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close> introduces local premises, similar
567    to \<^theory_text>\<open>assume\<close> within a proof (cf.\ \secref{sec:proof-context}).
568
569    \<^descr> @{element "defines"}~\<open>a: x \<equiv> t\<close> defines a previously declared parameter.
570    This is similar to \<^theory_text>\<open>define\<close> within a proof (cf.\
571    \secref{sec:proof-context}), but @{element "defines"} is restricted to
572    Pure equalities and the defined variable needs to be declared beforehand
573    via @{element "fixes"}. The left-hand side of the equation may have
574    additional arguments, e.g.\ ``@{element "defines"}~\<open>f x\<^sub>1 \<dots> x\<^sub>n \<equiv> t\<close>'',
575    which need to be free in the context.
576
577    \<^descr> @{element "notes"}~\<open>a = b\<^sub>1 \<dots> b\<^sub>n\<close> reconsiders facts within a local
578    context. Most notably, this may include arbitrary declarations in any
579    attribute specifications included here, e.g.\ a local @{attribute simp}
580    rule.
581
582  Both @{element "assumes"} and @{element "defines"} elements contribute to
583  the locale specification. When defining an operation derived from the
584  parameters, \<^theory_text>\<open>definition\<close> (\secref{sec:term-definitions}) is usually more
585  appropriate.
586
587  Note that ``\<^theory_text>\<open>(is p\<^sub>1 \<dots> p\<^sub>n)\<close>'' patterns given in the syntax of @{element
588  "assumes"} and @{element "defines"} above are illegal in locale definitions.
589  In the long goal format of \secref{sec:goals}, term bindings may be included
590  as expected, though.
591
592  \<^medskip>
593  Locale specifications are ``closed up'' by turning the given text into a
594  predicate definition \<open>loc_axioms\<close> and deriving the original assumptions as
595  local lemmas (modulo local definitions). The predicate statement covers only
596  the newly specified assumptions, omitting the content of included locale
597  expressions. The full cumulative view is only provided on export, involving
598  another predicate \<open>loc\<close> that refers to the complete specification text.
599
600  In any case, the predicate arguments are those locale parameters that
601  actually occur in the respective piece of text. Also these predicates
602  operate at the meta-level in theory, but the locale packages attempts to
603  internalize statements according to the object-logic setup (e.g.\ replacing
604  \<open>\<And>\<close> by \<open>\<forall>\<close>, and \<open>\<Longrightarrow>\<close> by \<open>\<longrightarrow>\<close> in HOL; see also \secref{sec:object-logic}).
605  Separate introduction rules \<open>loc_axioms.intro\<close> and \<open>loc.intro\<close> are provided
606  as well.
607
608  \<^descr> \<^theory_text>\<open>experiment exprs begin\<close> opens an anonymous locale context with private
609  naming policy. Specifications in its body are inaccessible from outside.
610  This is useful to perform experiments, without polluting the name space.
611
612  \<^descr> \<^theory_text>\<open>print_locale locale\<close> prints the contents of the named locale. The
613  command omits @{element "notes"} elements by default. Use \<^theory_text>\<open>print_locale!\<close>
614  to have them included.
615
616  \<^descr> \<^theory_text>\<open>print_locales\<close> prints the names of all locales of the current theory;
617  the ``\<open>!\<close>'' option indicates extra verbosity.
618
619  \<^descr> \<^theory_text>\<open>locale_deps\<close> visualizes all locales and their relations as a Hasse
620  diagram. This includes locales defined as type classes (\secref{sec:class}).
621  See also \<^theory_text>\<open>print_dependencies\<close> below.
622
623  \<^descr> @{method intro_locales} and @{method unfold_locales} repeatedly expand all
624  introduction rules of locale predicates of the theory. While @{method
625  intro_locales} only applies the \<open>loc.intro\<close> introduction rules and therefore
626  does not descend to assumptions, @{method unfold_locales} is more aggressive
627  and applies \<open>loc_axioms.intro\<close> as well. Both methods are aware of locale
628  specifications entailed by the context, both from target statements, and
629  from interpretations (see below). New goals that are entailed by the current
630  context are discharged automatically.
631\<close>
632
633
634subsection \<open>Locale interpretation \label{sec:locale-interpretation}\<close>
635
636text \<open>
637  \begin{matharray}{rcl}
638    @{command "interpretation"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close> \\
639    @{command_def "interpret"} & : & \<open>proof(state) | proof(chain) \<rightarrow> proof(prove)\<close> \\
640    @{command_def "global_interpretation"} & : & \<open>theory | local_theory \<rightarrow> proof(prove)\<close> \\
641    @{command_def "sublocale"} & : & \<open>theory | local_theory \<rightarrow> proof(prove)\<close> \\
642    @{command_def "print_dependencies"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
643    @{command_def "print_interps"}\<open>\<^sup>*\<close> & :  & \<open>context \<rightarrow>\<close> \\
644  \end{matharray}
645
646  Locales may be instantiated, and the resulting instantiated declarations
647  added to the current context. This requires proof (of the instantiated
648  specification) and is called \<^emph>\<open>locale interpretation\<close>. Interpretation is
649  possible within arbitrary local theories (\<^theory_text>\<open>interpretation\<close>), within proof
650  bodies (\<^theory_text>\<open>interpret\<close>), into global theories (\<^theory_text>\<open>global_interpretation\<close>) and
651  into locales (\<^theory_text>\<open>sublocale\<close>).
652
653  @{rail \<open>
654    @@{command interpretation} @{syntax locale_expr}
655    ;
656    @@{command interpret} @{syntax locale_expr}
657    ;
658    @@{command global_interpretation} @{syntax locale_expr} definitions?
659    ;
660    @@{command sublocale} (@{syntax name} ('<' | '\<subseteq>'))? @{syntax locale_expr} \<newline>
661      definitions?
662    ;
663    @@{command print_dependencies} '!'? @{syntax locale_expr}
664    ;
665    @@{command print_interps} @{syntax name}
666    ;
667
668    definitions: @'defines' (@{syntax thmdecl}? @{syntax name} \<newline>
669      @{syntax mixfix}? @'=' @{syntax term} + @'and');
670  \<close>}
671
672  The core of each interpretation command is a locale expression \<open>expr\<close>; the
673  command generates proof obligations for the instantiated specifications.
674  Once these are discharged by the user, instantiated declarations (in
675  particular, facts) are added to the context in a post-processing phase, in a
676  manner specific to each command.
677
678  Interpretation commands are aware of interpretations that are already
679  active: post-processing is achieved through a variant of roundup that takes
680  interpretations of the current global or local theory into account. In order
681  to simplify the proof obligations according to existing interpretations use
682  methods @{method intro_locales} or @{method unfold_locales}.
683
684  Rewrites clauses \<^theory_text>\<open>rewrites eqns\<close> occur within expressions. They amend the
685  morphism through which a locale instance is interpreted with rewrite rules,
686  also called rewrite morphisms. This is particularly useful for interpreting
687  concepts introduced through definitions. The equations must be proved the
688  user. To enable syntax of the instantiated locale within the equation, while
689  reading a locale expression, equations of a locale instance are read in a
690  temporary context where the instance is already activated. If activation
691  fails, typically due to duplicate constant declarations, processing falls
692  back to reading the equation first.
693
694  Given definitions \<open>defs\<close> produce corresponding definitions in the local
695  theory's underlying target \<^emph>\<open>and\<close> amend the morphism with rewrite rules
696  stemming from the symmetric of those definitions. Hence these need not be
697  proved explicitly the user. Such rewrite definitions are a even more useful
698  device for interpreting concepts introduced through definitions, but they
699  are only supported for interpretation commands operating in a local theory
700  whose implementing target actually supports this.  Note that despite
701  the suggestive \<^theory_text>\<open>and\<close> connective, \<open>defs\<close>
702  are processed sequentially without mutual recursion.
703
704  \<^descr> \<^theory_text>\<open>interpretation expr\<close> interprets \<open>expr\<close> into a local theory
705  such that its lifetime is limited to the current context block (e.g. a
706  locale or unnamed context). At the closing @{command end} of the block the
707  interpretation and its declarations disappear. Hence facts based on
708  interpretation can be established without creating permanent links to the
709  interpreted locale instances, as would be the case with @{command
710  sublocale}.
711
712  When used on the level of a global theory, there is no end of a current
713  context block, hence \<^theory_text>\<open>interpretation\<close> behaves identically to
714  \<^theory_text>\<open>global_interpretation\<close> then.
715
716  \<^descr> \<^theory_text>\<open>interpret expr\<close> interprets \<open>expr\<close> into a proof context:
717  the interpretation and its declarations disappear when closing the current
718  proof block. Note that for \<^theory_text>\<open>interpret\<close> the \<open>eqns\<close> should be explicitly
719  universally quantified.
720
721  \<^descr> \<^theory_text>\<open>global_interpretation defines defs\<close> interprets \<open>expr\<close>
722  into a global theory.
723
724  When adding declarations to locales, interpreted versions of these
725  declarations are added to the global theory for all interpretations in the
726  global theory as well. That is, interpretations into global theories
727  dynamically participate in any declarations added to locales.
728
729  Free variables in the interpreted expression are allowed. They are turned
730  into schematic variables in the generated declarations. In order to use a
731  free variable whose name is already bound in the context --- for example,
732  because a constant of that name exists --- add it to the \<^theory_text>\<open>for\<close> clause.
733
734  \<^descr> \<^theory_text>\<open>sublocale name \<subseteq> expr defines defs\<close> interprets \<open>expr\<close>
735  into the locale \<open>name\<close>. A proof that the specification of \<open>name\<close> implies the
736  specification of \<open>expr\<close> is required. As in the localized version of the
737  theorem command, the proof is in the context of \<open>name\<close>. After the proof
738  obligation has been discharged, the locale hierarchy is changed as if \<open>name\<close>
739  imported \<open>expr\<close> (hence the name \<^theory_text>\<open>sublocale\<close>). When the context of \<open>name\<close> is
740  subsequently entered, traversing the locale hierarchy will involve the
741  locale instances of \<open>expr\<close>, and their declarations will be added to the
742  context. This makes \<^theory_text>\<open>sublocale\<close> dynamic: extensions of a locale that is
743  instantiated in \<open>expr\<close> may take place after the \<^theory_text>\<open>sublocale\<close> declaration and
744  still become available in the context. Circular \<^theory_text>\<open>sublocale\<close> declarations
745  are allowed as long as they do not lead to infinite chains.
746
747  If interpretations of \<open>name\<close> exist in the current global theory, the command
748  adds interpretations for \<open>expr\<close> as well, with the same qualifier, although
749  only for fragments of \<open>expr\<close> that are not interpreted in the theory already.
750
751  Rewrites clauses in the expression or rewrite definitions \<open>defs\<close> can help break
752  infinite chains induced by circular \<^theory_text>\<open>sublocale\<close> declarations.
753
754  In a named context block the \<^theory_text>\<open>sublocale\<close> command may also be used, but the
755  locale argument must be omitted. The command then refers to the locale (or
756  class) target of the context block.
757
758  \<^descr> \<^theory_text>\<open>print_dependencies expr\<close> is useful for understanding the effect of an
759  interpretation of \<open>expr\<close> in the current context. It lists all locale
760  instances for which interpretations would be added to the current context.
761  Variant \<^theory_text>\<open>print_dependencies!\<close> does not generalize parameters and assumes an
762  empty context --- that is, it prints all locale instances that would be
763  considered for interpretation. The latter is useful for understanding the
764  dependencies of a locale expression.
765
766  \<^descr> \<^theory_text>\<open>print_interps locale\<close> lists all interpretations of \<open>locale\<close> in the
767  current theory or proof context, including those due to a combination of an
768  \<^theory_text>\<open>interpretation\<close> or \<^theory_text>\<open>interpret\<close> and one or several \<^theory_text>\<open>sublocale\<close>
769  declarations.
770
771  \begin{warn}
772    If a global theory inherits declarations (body elements) for a locale from
773    one parent and an interpretation of that locale from another parent, the
774    interpretation will not be applied to the declarations.
775  \end{warn}
776
777  \begin{warn}
778    Since attributes are applied to interpreted theorems, interpretation may
779    modify the context of common proof tools, e.g.\ the Simplifier or
780    Classical Reasoner. As the behaviour of such tools is \<^emph>\<open>not\<close> stable under
781    interpretation morphisms, manual declarations might have to be added to
782    the target context of the interpretation to revert such declarations.
783  \end{warn}
784
785  \begin{warn}
786    An interpretation in a local theory or proof context may subsume previous
787    interpretations. This happens if the same specification fragment is
788    interpreted twice and the instantiation of the second interpretation is
789    more general than the interpretation of the first. The locale package does
790    not attempt to remove subsumed interpretations.
791  \end{warn}
792
793  \begin{warn}
794    While \<^theory_text>\<open>interpretation (in c) \<dots>\<close> is admissible, it is not useful since
795    its result is discarded immediately.
796  \end{warn}
797\<close>
798
799
800section \<open>Classes \label{sec:class}\<close>
801
802text \<open>
803  \begin{matharray}{rcl}
804    @{command_def "class"} & : & \<open>theory \<rightarrow> local_theory\<close> \\
805    @{command_def "instantiation"} & : & \<open>theory \<rightarrow> local_theory\<close> \\
806    @{command_def "instance"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
807    @{command "instance"} & : & \<open>theory \<rightarrow> proof(prove)\<close> \\
808    @{command_def "subclass"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
809    @{command_def "print_classes"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
810    @{command_def "class_deps"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
811    @{method_def intro_classes} & : & \<open>method\<close> \\
812  \end{matharray}
813
814  A class is a particular locale with \<^emph>\<open>exactly one\<close> type variable \<open>\<alpha>\<close>. Beyond
815  the underlying locale, a corresponding type class is established which is
816  interpreted logically as axiomatic type class @{cite "Wenzel:1997:TPHOL"}
817  whose logical content are the assumptions of the locale. Thus, classes
818  provide the full generality of locales combined with the commodity of type
819  classes (notably type-inference). See @{cite "isabelle-classes"} for a short
820  tutorial.
821
822  @{rail \<open>
823    @@{command class} class_spec @'begin'?
824    ;
825    class_spec: @{syntax name} '='
826      ((@{syntax name} '+' (@{syntax context_elem}+)) |
827        @{syntax name} | (@{syntax context_elem}+))
828    ;
829    @@{command instantiation} (@{syntax name} + @'and') '::' @{syntax arity} @'begin'
830    ;
831    @@{command instance} (() | (@{syntax name} + @'and') '::' @{syntax arity} |
832      @{syntax name} ('<' | '\<subseteq>') @{syntax name} )
833    ;
834    @@{command subclass} @{syntax name}
835    ;
836    @@{command class_deps} (class_bounds class_bounds?)?
837    ;
838    class_bounds: @{syntax sort} | '(' (@{syntax sort} + @'|') ')'
839  \<close>}
840
841  \<^descr> \<^theory_text>\<open>class c = superclasses + body\<close> defines a new class \<open>c\<close>, inheriting from
842  \<open>superclasses\<close>. This introduces a locale \<open>c\<close> with import of all locales
843  \<open>superclasses\<close>.
844
845  Any @{element "fixes"} in \<open>body\<close> are lifted to the global theory level
846  (\<^emph>\<open>class operations\<close> \<open>f\<^sub>1, \<dots>, f\<^sub>n\<close> of class \<open>c\<close>), mapping the local type
847  parameter \<open>\<alpha>\<close> to a schematic type variable \<open>?\<alpha> :: c\<close>.
848
849  Likewise, @{element "assumes"} in \<open>body\<close> are also lifted, mapping each local
850  parameter \<open>f :: \<tau>[\<alpha>]\<close> to its corresponding global constant \<open>f :: \<tau>[?\<alpha> ::
851  c]\<close>. The corresponding introduction rule is provided as
852  \<open>c_class_axioms.intro\<close>. This rule should be rarely needed directly --- the
853  @{method intro_classes} method takes care of the details of class membership
854  proofs.
855
856  \<^descr> \<^theory_text>\<open>instantiation t :: (s\<^sub>1, \<dots>, s\<^sub>n)s begin\<close> opens a target (cf.\
857  \secref{sec:target}) which allows to specify class operations \<open>f\<^sub>1, \<dots>, f\<^sub>n\<close>
858  corresponding to sort \<open>s\<close> at the particular type instance \<open>(\<alpha>\<^sub>1 :: s\<^sub>1, \<dots>,
859  \<alpha>\<^sub>n :: s\<^sub>n) t\<close>. A plain \<^theory_text>\<open>instance\<close> command in the target body poses a goal
860  stating these type arities. The target is concluded by an @{command_ref
861  (local) "end"} command.
862
863  Note that a list of simultaneous type constructors may be given; this
864  corresponds nicely to mutually recursive type definitions, e.g.\ in
865  Isabelle/HOL.
866
867  \<^descr> \<^theory_text>\<open>instance\<close> in an instantiation target body sets up a goal stating the
868  type arities claimed at the opening \<^theory_text>\<open>instantiation\<close>. The proof would
869  usually proceed by @{method intro_classes}, and then establish the
870  characteristic theorems of the type classes involved. After finishing the
871  proof, the background theory will be augmented by the proven type arities.
872
873  On the theory level, \<^theory_text>\<open>instance t :: (s\<^sub>1, \<dots>, s\<^sub>n)s\<close> provides a convenient
874  way to instantiate a type class with no need to specify operations: one can
875  continue with the instantiation proof immediately.
876
877  \<^descr> \<^theory_text>\<open>subclass c\<close> in a class context for class \<open>d\<close> sets up a goal stating that
878  class \<open>c\<close> is logically contained in class \<open>d\<close>. After finishing the proof,
879  class \<open>d\<close> is proven to be subclass \<open>c\<close> and the locale \<open>c\<close> is interpreted
880  into \<open>d\<close> simultaneously.
881
882  A weakened form of this is available through a further variant of @{command
883  instance}: \<^theory_text>\<open>instance c\<^sub>1 \<subseteq> c\<^sub>2\<close> opens a proof that class \<open>c\<^sub>2\<close> implies
884  \<open>c\<^sub>1\<close> without reference to the underlying locales; this is useful if the
885  properties to prove the logical connection are not sufficient on the locale
886  level but on the theory level.
887
888  \<^descr> \<^theory_text>\<open>print_classes\<close> prints all classes in the current theory.
889
890  \<^descr> \<^theory_text>\<open>class_deps\<close> visualizes classes and their subclass relations as a
891  directed acyclic graph. By default, all classes from the current theory
892  context are show. This may be restricted by optional bounds as follows:
893  \<^theory_text>\<open>class_deps upper\<close> or \<^theory_text>\<open>class_deps upper lower\<close>. A class is visualized, iff
894  it is a subclass of some sort from \<open>upper\<close> and a superclass of some sort
895  from \<open>lower\<close>.
896
897  \<^descr> @{method intro_classes} repeatedly expands all class introduction rules of
898  this theory. Note that this method usually needs not be named explicitly, as
899  it is already included in the default proof step (e.g.\ of \<^theory_text>\<open>proof\<close>). In
900  particular, instantiation of trivial (syntactic) classes may be performed by
901  a single ``\<^theory_text>\<open>..\<close>'' proof step.
902\<close>
903
904
905subsection \<open>The class target\<close>
906
907text \<open>
908  %FIXME check
909
910  A named context may refer to a locale (cf.\ \secref{sec:target}). If this
911  locale is also a class \<open>c\<close>, apart from the common locale target behaviour
912  the following happens.
913
914    \<^item> Local constant declarations \<open>g[\<alpha>]\<close> referring to the local type parameter
915    \<open>\<alpha>\<close> and local parameters \<open>f[\<alpha>]\<close> are accompanied by theory-level constants
916    \<open>g[?\<alpha> :: c]\<close> referring to theory-level class operations \<open>f[?\<alpha> :: c]\<close>.
917
918    \<^item> Local theorem bindings are lifted as are assumptions.
919
920    \<^item> Local syntax refers to local operations \<open>g[\<alpha>]\<close> and global operations
921    \<open>g[?\<alpha> :: c]\<close> uniformly. Type inference resolves ambiguities. In rare
922    cases, manual type annotations are needed.
923\<close>
924
925
926subsection \<open>Co-regularity of type classes and arities\<close>
927
928text \<open>
929  The class relation together with the collection of type-constructor arities
930  must obey the principle of \<^emph>\<open>co-regularity\<close> as defined below.
931
932  \<^medskip>
933  For the subsequent formulation of co-regularity we assume that the class
934  relation is closed by transitivity and reflexivity. Moreover the collection
935  of arities \<open>t :: (\<^vec>s)c\<close> is completed such that \<open>t :: (\<^vec>s)c\<close> and
936  \<open>c \<subseteq> c'\<close> implies \<open>t :: (\<^vec>s)c'\<close> for all such declarations.
937
938  Treating sorts as finite sets of classes (meaning the intersection), the
939  class relation \<open>c\<^sub>1 \<subseteq> c\<^sub>2\<close> is extended to sorts as follows:
940  \[
941    \<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>
942  \]
943
944  This relation on sorts is further extended to tuples of sorts (of the same
945  length) in the component-wise way.
946
947  \<^medskip>
948  Co-regularity of the class relation together with the arities relation
949  means:
950  \[
951    \<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>
952  \]
953  for all such arities. In other words, whenever the result classes of some
954  type-constructor arities are related, then the argument sorts need to be
955  related in the same way.
956
957  \<^medskip>
958  Co-regularity is a very fundamental property of the order-sorted algebra of
959  types. For example, it entails principle types and most general unifiers,
960  e.g.\ see @{cite "nipkow-prehofer"}.
961\<close>
962
963
964section \<open>Overloaded constant definitions \label{sec:overloading}\<close>
965
966text \<open>
967  Definitions essentially express abbreviations within the logic. The simplest
968  form of a definition is \<open>c :: \<sigma> \<equiv> t\<close>, where \<open>c\<close> is a new constant and \<open>t\<close> is
969  a closed term that does not mention \<open>c\<close>. Moreover, so-called \<^emph>\<open>hidden
970  polymorphism\<close> is excluded: all type variables in \<open>t\<close> need to occur in its
971  type \<open>\<sigma>\<close>.
972
973  \<^emph>\<open>Overloading\<close> means that a constant being declared as \<open>c :: \<alpha> decl\<close> may be
974  defined separately on type instances \<open>c :: (\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n)\<kappa> decl\<close> for each
975  type constructor \<open>\<kappa>\<close>. At most occasions overloading will be used in a
976  Haskell-like fashion together with type classes by means of \<^theory_text>\<open>instantiation\<close>
977  (see \secref{sec:class}). Sometimes low-level overloading is desirable; this
978  is supported by \<^theory_text>\<open>consts\<close> and \<^theory_text>\<open>overloading\<close> explained below.
979
980  The right-hand side of overloaded definitions may mention overloaded
981  constants recursively at type instances corresponding to the immediate
982  argument types \<open>\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n\<close>. Incomplete specification patterns impose
983  global constraints on all occurrences. E.g.\ \<open>d :: \<alpha> \<times> \<alpha>\<close> on the left-hand
984  side means that all corresponding occurrences on some right-hand side need
985  to be an instance of this, and general \<open>d :: \<alpha> \<times> \<beta>\<close> will be disallowed. Full
986  details are given by Kun\v{c}ar @{cite "Kuncar:2015"}.
987
988  \<^medskip>
989  The \<^theory_text>\<open>consts\<close> command and the \<^theory_text>\<open>overloading\<close> target provide a convenient
990  interface for end-users. Regular specification elements such as @{command
991  definition}, @{command inductive}, @{command function} may be used in the
992  body. It is also possible to use \<^theory_text>\<open>consts c :: \<sigma>\<close> with later \<^theory_text>\<open>overloading c
993  \<equiv> c :: \<sigma>\<close> to keep the declaration and definition of a constant separate.
994
995  \begin{matharray}{rcl}
996    @{command_def "consts"} & : & \<open>theory \<rightarrow> theory\<close> \\
997    @{command_def "overloading"} & : & \<open>theory \<rightarrow> local_theory\<close> \\
998  \end{matharray}
999
1000  @{rail \<open>
1001    @@{command consts} ((@{syntax name} '::' @{syntax type} @{syntax mixfix}?) +)
1002    ;
1003    @@{command overloading} ( spec + ) @'begin'
1004    ;
1005    spec: @{syntax name} ( '\<equiv>' | '==' ) @{syntax term} ( '(' @'unchecked' ')' )?
1006  \<close>}
1007
1008  \<^descr> \<^theory_text>\<open>consts c :: \<sigma>\<close> declares constant \<open>c\<close> to have any instance of type scheme
1009  \<open>\<sigma>\<close>. The optional mixfix annotations may attach concrete syntax to the
1010  constants declared.
1011
1012  \<^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
1013  a theory target (cf.\ \secref{sec:target}) which allows to specify already
1014  declared constants via definitions in the body. These are identified by an
1015  explicitly given mapping from variable names \<open>x\<^sub>i\<close> to constants \<open>c\<^sub>i\<close> at
1016  particular type instances. The definitions themselves are established using
1017  common specification tools, using the names \<open>x\<^sub>i\<close> as reference to the
1018  corresponding constants.
1019
1020  Option \<^theory_text>\<open>(unchecked)\<close> disables global dependency checks for the
1021  corresponding definition, which is occasionally useful for exotic
1022  overloading; this is a form of axiomatic specification. It is at the
1023  discretion of the user to avoid malformed theory specifications!
1024\<close>
1025
1026
1027subsubsection \<open>Example\<close>
1028
1029consts Length :: "'a \<Rightarrow> nat"
1030
1031overloading
1032  Length\<^sub>0 \<equiv> "Length :: unit \<Rightarrow> nat"
1033  Length\<^sub>1 \<equiv> "Length :: 'a \<times> unit \<Rightarrow> nat"
1034  Length\<^sub>2 \<equiv> "Length :: 'a \<times> 'b \<times> unit \<Rightarrow> nat"
1035  Length\<^sub>3 \<equiv> "Length :: 'a \<times> 'b \<times> 'c \<times> unit \<Rightarrow> nat"
1036begin
1037
1038fun Length\<^sub>0 :: "unit \<Rightarrow> nat" where "Length\<^sub>0 () = 0"
1039fun Length\<^sub>1 :: "'a \<times> unit \<Rightarrow> nat" where "Length\<^sub>1 (a, ()) = 1"
1040fun Length\<^sub>2 :: "'a \<times> 'b \<times> unit \<Rightarrow> nat" where "Length\<^sub>2 (a, b, ()) = 2"
1041fun Length\<^sub>3 :: "'a \<times> 'b \<times> 'c \<times> unit \<Rightarrow> nat" where "Length\<^sub>3 (a, b, c, ()) = 3"
1042
1043end
1044
1045lemma "Length (a, b, c, ()) = 3" by simp
1046lemma "Length ((a, b), (c, d), ()) = 2" by simp
1047lemma "Length ((a, b, c, d, e), ()) = 1" by simp
1048
1049
1050section \<open>Incorporating ML code \label{sec:ML}\<close>
1051
1052text \<open>
1053  \begin{matharray}{rcl}
1054    @{command_def "SML_file"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
1055    @{command_def "SML_file_debug"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
1056    @{command_def "SML_file_no_debug"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
1057    @{command_def "ML_file"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
1058    @{command_def "ML_file_debug"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
1059    @{command_def "ML_file_no_debug"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
1060    @{command_def "ML"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
1061    @{command_def "ML_export"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
1062    @{command_def "ML_prf"} & : & \<open>proof \<rightarrow> proof\<close> \\
1063    @{command_def "ML_val"} & : & \<open>any \<rightarrow>\<close> \\
1064    @{command_def "ML_command"} & : & \<open>any \<rightarrow>\<close> \\
1065    @{command_def "setup"} & : & \<open>theory \<rightarrow> theory\<close> \\
1066    @{command_def "local_setup"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
1067    @{command_def "attribute_setup"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
1068  \end{matharray}
1069  \begin{tabular}{rcll}
1070    @{attribute_def ML_print_depth} & : & \<open>attribute\<close> & default 10 \\
1071    @{attribute_def ML_source_trace} & : & \<open>attribute\<close> & default \<open>false\<close> \\
1072    @{attribute_def ML_debugger} & : & \<open>attribute\<close> & default \<open>false\<close> \\
1073    @{attribute_def ML_exception_trace} & : & \<open>attribute\<close> & default \<open>false\<close> \\
1074    @{attribute_def ML_exception_debugger} & : & \<open>attribute\<close> & default \<open>false\<close> \\
1075  \end{tabular}
1076
1077  @{rail \<open>
1078    (@@{command SML_file} |
1079      @@{command SML_file_debug} |
1080      @@{command SML_file_no_debug} |
1081      @@{command ML_file} |
1082      @@{command ML_file_debug} |
1083      @@{command ML_file_no_debug}) @{syntax name} ';'?
1084    ;
1085    (@@{command ML} | @@{command ML_export} | @@{command ML_prf} |
1086      @@{command ML_val} | @@{command ML_command} | @@{command setup} |
1087      @@{command local_setup}) @{syntax text}
1088    ;
1089    @@{command attribute_setup} @{syntax name} '=' @{syntax text} @{syntax text}?
1090  \<close>}
1091
1092  \<^descr> \<^theory_text>\<open>SML_file name\<close> reads and evaluates the given Standard ML file. Top-level
1093  SML bindings are stored within the (global or local) theory context; the
1094  initial environment is restricted to the Standard ML implementation of
1095  Poly/ML, without the many add-ons of Isabelle/ML. Multiple \<^theory_text>\<open>SML_file\<close>
1096  commands may be used to build larger Standard ML projects, independently of
1097  the regular Isabelle/ML environment.
1098
1099  \<^descr> \<^theory_text>\<open>ML_file name\<close> reads and evaluates the given ML file. The current theory
1100  context is passed down to the ML toplevel and may be modified, using @{ML
1101  "Context.>>"} or derived ML commands. Top-level ML bindings are stored
1102  within the (global or local) theory context.
1103
1104  \<^descr> \<^theory_text>\<open>SML_file_debug\<close>, \<^theory_text>\<open>SML_file_no_debug\<close>, \<^theory_text>\<open>ML_file_debug\<close>, and
1105  \<^theory_text>\<open>ML_file_no_debug\<close> change the @{attribute ML_debugger} option locally while
1106  the given file is compiled.
1107
1108  \<^descr> \<^theory_text>\<open>ML\<close> is similar to \<^theory_text>\<open>ML_file\<close>, but evaluates directly the given \<open>text\<close>.
1109  Top-level ML bindings are stored within the (global or local) theory
1110  context.
1111
1112  \<^descr> \<^theory_text>\<open>ML_export\<close> is similar to \<^theory_text>\<open>ML\<close>, but the resulting toplevel bindings are
1113  exported to the global bootstrap environment of the ML process --- it has
1114  a lasting effect that cannot be retracted. This allows ML evaluation
1115  without a formal theory context, e.g. for command-line tools via @{tool
1116  process} @{cite "isabelle-system"}.
1117
1118  \<^descr> \<^theory_text>\<open>ML_prf\<close> is analogous to \<^theory_text>\<open>ML\<close> but works within a proof context.
1119  Top-level ML bindings are stored within the proof context in a purely
1120  sequential fashion, disregarding the nested proof structure. ML bindings
1121  introduced by \<^theory_text>\<open>ML_prf\<close> are discarded at the end of the proof.
1122
1123  \<^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
1124  that the context may not be updated. \<^theory_text>\<open>ML_val\<close> echos the bindings produced
1125  at the ML toplevel, but \<^theory_text>\<open>ML_command\<close> is silent.
1126
1127  \<^descr> \<^theory_text>\<open>setup "text"\<close> changes the current theory context by applying \<open>text\<close>,
1128  which refers to an ML expression of type @{ML_type "theory -> theory"}. This
1129  enables to initialize any object-logic specific tools and packages written
1130  in ML, for example.
1131
1132  \<^descr> \<^theory_text>\<open>local_setup\<close> is similar to \<^theory_text>\<open>setup\<close> for a local theory context, and an
1133  ML expression of type @{ML_type "local_theory -> local_theory"}. This allows
1134  to invoke local theory specification packages without going through concrete
1135  outer syntax, for example.
1136
1137  \<^descr> \<^theory_text>\<open>attribute_setup name = "text" description\<close> defines an attribute in the
1138  current context. The given \<open>text\<close> has to be an ML expression of type
1139  @{ML_type "attribute context_parser"}, cf.\ basic parsers defined in
1140  structure @{ML_structure Args} and @{ML_structure Attrib}.
1141
1142  In principle, attributes can operate both on a given theorem and the
1143  implicit context, although in practice only one is modified and the other
1144  serves as parameter. Here are examples for these two cases:
1145\<close>
1146
1147(*<*)experiment begin(*>*)
1148        attribute_setup my_rule =
1149          \<open>Attrib.thms >> (fn ths =>
1150            Thm.rule_attribute ths
1151              (fn context: Context.generic => fn th: thm =>
1152                let val th' = th OF ths
1153                in th' end))\<close>
1154
1155        attribute_setup my_declaration =
1156          \<open>Attrib.thms >> (fn ths =>
1157            Thm.declaration_attribute
1158              (fn th: thm => fn context: Context.generic =>
1159                let val context' = context
1160                in context' end))\<close>
1161(*<*)end(*>*)
1162
1163text \<open>
1164  \<^descr> @{attribute ML_print_depth} controls the printing depth of the ML toplevel
1165  pretty printer. Typically the limit should be less than 10. Bigger values
1166  such as 100--1000 are occasionally useful for debugging.
1167
1168  \<^descr> @{attribute ML_source_trace} indicates whether the source text that is
1169  given to the ML compiler should be output: it shows the raw Standard ML
1170  after expansion of Isabelle/ML antiquotations.
1171
1172  \<^descr> @{attribute ML_debugger} controls compilation of sources with or without
1173  debugging information. The global system option @{system_option_ref
1174  ML_debugger} does the same when building a session image. It is also
1175  possible use commands like \<^theory_text>\<open>ML_file_debug\<close> etc. The ML debugger is
1176  explained further in @{cite "isabelle-jedit"}.
1177
1178  \<^descr> @{attribute ML_exception_trace} indicates whether the ML run-time system
1179  should print a detailed stack trace on exceptions. The result is dependent
1180  on various ML compiler optimizations. The boundary for the exception trace
1181  is the current Isar command transactions: it is occasionally better to
1182  insert the combinator @{ML Runtime.exn_trace} into ML code for debugging
1183  @{cite "isabelle-implementation"}, closer to the point where it actually
1184  happens.
1185
1186  \<^descr> @{attribute ML_exception_debugger} controls detailed exception trace via
1187  the Poly/ML debugger, at the cost of extra compile-time and run-time
1188  overhead. Relevant ML modules need to be compiled beforehand with debugging
1189  enabled, see @{attribute ML_debugger} above.
1190\<close>
1191
1192
1193section \<open>External file dependencies\<close>
1194
1195text \<open>
1196  \begin{matharray}{rcl}
1197    @{command_def "external_file"} & : & \<open>any \<rightarrow> any\<close> \\
1198  \end{matharray}
1199
1200  @{rail \<open>@@{command external_file} @{syntax name} ';'?\<close>}
1201
1202  \<^descr> \<^theory_text>\<open>external_file name\<close> declares the formal dependency on the given file
1203  name, such that the Isabelle build process knows about it (see also @{cite
1204  "isabelle-system"}). The file can be read e.g.\ in Isabelle/ML via @{ML
1205  File.read}, without specific management by the Prover IDE.
1206\<close>
1207
1208
1209
1210section \<open>Primitive specification elements\<close>
1211
1212subsection \<open>Sorts\<close>
1213
1214text \<open>
1215  \begin{matharray}{rcll}
1216    @{command_def "default_sort"} & : & \<open>local_theory \<rightarrow> local_theory\<close>
1217  \end{matharray}
1218
1219  @{rail \<open>
1220    @@{command default_sort} @{syntax sort}
1221  \<close>}
1222
1223  \<^descr> \<^theory_text>\<open>default_sort s\<close> makes sort \<open>s\<close> the new default sort for any type
1224  variable that is given explicitly in the text, but lacks a sort constraint
1225  (wrt.\ the current context). Type variables generated by type inference are
1226  not affected.
1227
1228  Usually the default sort is only changed when defining a new object-logic.
1229  For example, the default sort in Isabelle/HOL is @{class type}, the class of
1230  all HOL types.
1231
1232  When merging theories, the default sorts of the parents are logically
1233  intersected, i.e.\ the representations as lists of classes are joined.
1234\<close>
1235
1236
1237subsection \<open>Types \label{sec:types-pure}\<close>
1238
1239text \<open>
1240  \begin{matharray}{rcll}
1241    @{command_def "type_synonym"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
1242    @{command_def "typedecl"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
1243  \end{matharray}
1244
1245  @{rail \<open>
1246    @@{command type_synonym} (@{syntax typespec} '=' @{syntax type} @{syntax mixfix}?)
1247    ;
1248    @@{command typedecl} @{syntax typespec} @{syntax mixfix}?
1249  \<close>}
1250
1251  \<^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>,
1252  \<alpha>\<^sub>n) t\<close> for the existing type \<open>\<tau>\<close>. Unlike the semantic type definitions in
1253  Isabelle/HOL, type synonyms are merely syntactic abbreviations without any
1254  logical significance. Internally, type synonyms are fully expanded.
1255
1256  \<^descr> \<^theory_text>\<open>typedecl (\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t\<close> declares a new type constructor \<open>t\<close>. If the
1257  object-logic defines a base sort \<open>s\<close>, then the constructor is declared to
1258  operate on that, via the axiomatic type-class instance \<open>t :: (s, \<dots>, s)s\<close>.
1259
1260
1261  \begin{warn}
1262    If you introduce a new type axiomatically, i.e.\ via @{command_ref
1263    typedecl} and @{command_ref axiomatization}
1264    (\secref{sec:axiomatizations}), the minimum requirement is that it has a
1265    non-empty model, to avoid immediate collapse of the logical environment.
1266    Moreover, one needs to demonstrate that the interpretation of such
1267    free-form axiomatizations can coexist with other axiomatization schemes
1268    for types, notably @{command_def typedef} in Isabelle/HOL
1269    (\secref{sec:hol-typedef}), or any other extension that people might have
1270    introduced elsewhere.
1271  \end{warn}
1272\<close>
1273
1274
1275section \<open>Naming existing theorems \label{sec:theorems}\<close>
1276
1277text \<open>
1278  \begin{matharray}{rcll}
1279    @{command_def "lemmas"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
1280    @{command_def "named_theorems"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
1281  \end{matharray}
1282
1283  @{rail \<open>
1284    @@{command lemmas} (@{syntax thmdef}? @{syntax thms} + @'and')
1285      @{syntax for_fixes}
1286    ;
1287    @@{command named_theorems} (@{syntax name} @{syntax text}? + @'and')
1288  \<close>}
1289
1290  \<^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
1291  facts (with attributes) in the current context, which may be augmented by
1292  local variables. Results are standardized before being stored, i.e.\
1293  schematic variables are renamed to enforce index \<open>0\<close> uniformly.
1294
1295  \<^descr> \<^theory_text>\<open>named_theorems name description\<close> declares a dynamic fact within the
1296  context. The same \<open>name\<close> is used to define an attribute with the usual
1297  \<open>add\<close>/\<open>del\<close> syntax (e.g.\ see \secref{sec:simp-rules}) to maintain the
1298  content incrementally, in canonical declaration order of the text structure.
1299\<close>
1300
1301
1302section \<open>Oracles\<close>
1303
1304text \<open>
1305  \begin{matharray}{rcll}
1306    @{command_def "oracle"} & : & \<open>theory \<rightarrow> theory\<close> & (axiomatic!) \\
1307  \end{matharray}
1308
1309  Oracles allow Isabelle to take advantage of external reasoners such as
1310  arithmetic decision procedures, model checkers, fast tautology checkers or
1311  computer algebra systems. Invoked as an oracle, an external reasoner can
1312  create arbitrary Isabelle theorems.
1313
1314  It is the responsibility of the user to ensure that the external reasoner is
1315  as trustworthy as the application requires. Another typical source of errors
1316  is the linkup between Isabelle and the external tool, not just its concrete
1317  implementation, but also the required translation between two different
1318  logical environments.
1319
1320  Isabelle merely guarantees well-formedness of the propositions being
1321  asserted, and records within the internal derivation object how presumed
1322  theorems depend on unproven suppositions.
1323
1324  @{rail \<open>
1325    @@{command oracle} @{syntax name} '=' @{syntax text}
1326  \<close>}
1327
1328  \<^descr> \<^theory_text>\<open>oracle name = "text"\<close> turns the given ML expression \<open>text\<close> of type
1329  @{ML_text "'a -> cterm"} into an ML function of type @{ML_text "'a -> thm"},
1330  which is bound to the global identifier @{ML_text name}. This acts like an
1331  infinitary specification of axioms! Invoking the oracle only works within
1332  the scope of the resulting theory.
1333
1334
1335  See \<^file>\<open>~~/src/HOL/ex/Iff_Oracle.thy\<close> for a worked example of defining a new
1336  primitive rule as oracle, and turning it into a proof method.
1337\<close>
1338
1339
1340section \<open>Name spaces\<close>
1341
1342text \<open>
1343  \begin{matharray}{rcl}
1344    @{command_def "alias"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
1345    @{command_def "type_alias"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
1346    @{command_def "hide_class"} & : & \<open>theory \<rightarrow> theory\<close> \\
1347    @{command_def "hide_type"} & : & \<open>theory \<rightarrow> theory\<close> \\
1348    @{command_def "hide_const"} & : & \<open>theory \<rightarrow> theory\<close> \\
1349    @{command_def "hide_fact"} & : & \<open>theory \<rightarrow> theory\<close> \\
1350  \end{matharray}
1351
1352  @{rail \<open>
1353    (@{command alias} | @{command type_alias}) @{syntax name} '=' @{syntax name}
1354    ;
1355    (@{command hide_class} | @{command hide_type} |
1356      @{command hide_const} | @{command hide_fact}) ('(' @'open' ')')? (@{syntax name} + )
1357  \<close>}
1358
1359  Isabelle organizes any kind of name declarations (of types, constants,
1360  theorems etc.) by separate hierarchically structured name spaces. Normally
1361  the user does not have to control the behaviour of name spaces by hand, yet
1362  the following commands provide some way to do so.
1363
1364  \<^descr> \<^theory_text>\<open>alias\<close> and \<^theory_text>\<open>type_alias\<close> introduce aliases for constants and type
1365  constructors, respectively. This allows adhoc changes to name-space
1366  accesses.
1367
1368  \<^descr> \<^theory_text>\<open>type_alias b = c\<close> introduces an alias for an existing type constructor.
1369
1370  \<^descr> \<^theory_text>\<open>hide_class names\<close> fully removes class declarations from a given name
1371  space; with the \<open>(open)\<close> option, only the unqualified base name is hidden.
1372
1373  Note that hiding name space accesses has no impact on logical declarations
1374  --- they remain valid internally. Entities that are no longer accessible to
1375  the user are printed with the special qualifier ``\<open>??\<close>'' prefixed to the
1376  full internal name.
1377
1378  \<^descr> \<^theory_text>\<open>hide_type\<close>, \<^theory_text>\<open>hide_const\<close>, and \<^theory_text>\<open>hide_fact\<close> are similar to
1379  \<^theory_text>\<open>hide_class\<close>, but hide types, constants, and facts, respectively.
1380\<close>
1381
1382end
1383