| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Doc/Isar_Ref/ (Columbo Version 0.7©) Datei vom 16.11.2025 mit Größe 86 kB |
|
Quelle Spec.thy Sprache: Isabelle |
|||||||||
|
(*:maxLineLen=78:*)
theory Spec imports Main Base begin chapter \<open>Specifications\<close> text \<open> The Isabelle/Isar theory format integrates specifications and proofs, with support for interactive development by continuous document editing. There is a separate document preparation system (see \chref{ch:document-prep}), for typesetting formal developments together with informal text. The resulting hyper-linked PDF documents can be used both for WWW presentation and printed copies. The Isar proof language (see \chref{ch:proofs}) is embedded into the theory language as a proper sub-language. Proof mode is entered by stating some \<^theory_text>\<open>theorem\<close> or \<^theory_text>\<open>lemma\<close> at the theory level, a conclusion (e.g.\ via \<^theory_text>\<open>qed\<close>). \<close> section \<open>Defining theories \label{sec:begin-thy}\<close> text \<open> \begin{matharray}{rcl} @{command_def "theory"} & : & \<open>toplevel \<rightarrow> theory\<close> \\ @{command_def (global) "end"} & : & \<open>theory \<rightarrow> toplevel\<close> \\ @{command_def "thy_deps"}\<open>\<^sup>*\<close> & : & \<open>theory \<rightarrow>\<close> \end{matharray} Isabelle/Isar theories are defined via theory files, which consist of an outermost sequence of definition--statement--proof elements. Some definitions are self-sufficient (e.g.\ \<^theory_text>\<open>fun\<close> in Isabelle/HOL), wi foundational proofs performed internally. Other definitions require an explicit proof as justification (e.g.\ \<^theory_text>\<open>function\<close> and \<^theory_te Isabelle/HOL). Plain statements like \<^theory_text>\<open>theorem\<close> or \<^theory_text>\< special case of that, defining a theorem from a given proposition and its proof. The theory body may be sub-structured by means of \<^emph>\<open>local theory targets\<close>, such as \<^theory_text>\<open>locale\<close> and \<^theory_text>\<open>class\<close>. It is also pos end\<close> blocks to delimited a local theory context: a \<^emph>\<open>named context\<close> to augment a locale or class specification, or an \<^emph>\<open>unnamed context\<close> to refer to local parameters and assumptions that are discharged later. See \secref{sec:target} for more details. \<^medskip> A theory is commenced by the \<^theory_text>\<open>theory\<close> command, which indicates impor previous theories, according to an acyclic foundational order. Before the initial \<^theory_text>\<open>theory\<close> command, there may be optional document header mat (like \<^theory_text>\<open>section\<close> or \<^theory_text>\<open>text\<close>, see \secref{se is outside of the formal theory context, though. A theory is concluded by a final @{command (global) "end"} command, one that does not belong to a local theory target. No further commands may follow such a global @{command (global) "end"}. \<^rail>\<open> @@{command theory} @{syntax system_name} @'imports' (@{syntax system_name} +) \<newline> keywords? abbrevs? @'begin' ; keywords: @'keywords' (keyword_decls + @'and') ; keyword_decls: (@{syntax string} +) ('::' @{syntax name} @{syntax tags})? ; abbrevs: @'abbrevs' (((text+) '=' (text+)) + @'and') ; @@{command thy_deps} (thy_bounds thy_bounds?)? ; thy_bounds: @{syntax name} | '(' (@{syntax name} + @'|') ')' \<close> \<^descr> \<^theory_text>\<open>theory A imports B\<^sub>1 \<dots> B\<^sub>n begin\<close> starts a new t merge of existing theories \<open>B\<^sub>1 \<dots> B\<^sub>n\<close>. Due to the possibility to impor more than one ancestor, the resulting theory structure of an Isabelle session forms a directed acyclic graph (DAG). Isabelle takes care that sources contributing to the development graph are always up-to-date: changed files are automatically rechecked whenever a theory header specification is processed. Empty imports are only allowed in the bootstrap process of the special theory \<^theory>\<open>Pure\<close>, which is the start of any other formal development based on Isabelle. Regular user theories usually refer to some more complex entry point, such as theory \<^theory>\<open>Main\<close> in Isabelle/HOL. The @{keyword_def "keywords"} specification declares outer syntax (\chref{ch:outer-syntax}) that is introduced in this theory later on (rare in end-user applications). Both minor keywords and major keywords of the Isar command language need to be specified, in order to make parsing of proof documents work properly. Command keywords need to be classified according to their structural role in the formal text. Examples may be seen in Isabelle/HOL sources itself, such as @{keyword "keywords"}~\<^verbatim>\<open>"typedef"\< \<open>:: thy_goal_defn\<close> or @{keyword "keywords"}~\<^verbatim>\<open>"datatype"\<close> theory-level definitions with and without proof, respectively. Additional @{syntax tags} provide defaults for document preparation (\secref{sec:document-markers}). The @{keyword_def "abbrevs"} specification declares additional abbreviations for syntactic completion. The default for a new keyword is just its name, but completion may be avoided by defining @{keyword "abbrevs"} with empty text. \<^descr> @{command (global) "end"} concludes the current theory definition. Note that some other commands, e.g.\ local theory targets \<^theory_text>\<open>locale\<close> or \<^t may involve a \<^theory_text>\<open>begin\<close> that needs to be matched by @{command (local) "e according to the usual rules for nested blocks. \<^descr> \<^theory_text>\<open>thy_deps\<close> visualizes the theory hierarchy as a directed ac By default, all imported theories are shown. This may be restricted by specifying bounds wrt. the theory inclusion relation. \<close> section \<open>Local theory targets \label{sec:target}\<close> text \<open> \begin{matharray}{rcll} @{command_def "context"} & : & \<open>theory \<rightarrow> local_theory\<close> \\ @{command_def (local) "end"} & : & \<open>local_theory \<rightarrow> theory\<close> \\ @{keyword_def "private"} \\ @{keyword_def "qualified"} \\ \end{matharray} A local theory target is a specification context that is managed separately within the enclosing theory. Contexts may introduce parameters (fixed variables) and assumptions (hypotheses). Definitions and theorems depending on the context may be added incrementally later on. \<^emph>\<open>Named contexts\<close> refer to locales (cf.\ \secref{sec:locale}) or type classes (cf.\ \secref{sec:class}); the name ``\<open>-\<close>'' signifies the global theory context. \<^emph>\<open>Unnamed contexts\<close> may introduce additional parameters and assumptions, a results produced in the context are generalized accordingly. Such auxiliary contexts may be nested within other targets, like \<^theory_text>\<open>locale\<close>, \<^theor \<^theory_text>\<open>instantiation\<close>, \<^theory_text>\<open>overloading\<close>. \<^rail>\<open> @@{command context} @{syntax name} @{syntax_ref "opening"}? @'begin' ; @@{command context} @{syntax_ref "includes"}? (@{syntax context_elem} * ) @'begin' ; @{syntax_def target}: '(' @'in' @{syntax name} ')' \<close> \<^descr> \<^theory_text>\<open>context c bundles begin\<close> opens a named context, by recommen locale or class \<open>c\<close>. Note that locale and class definitions allow to include the \<^theory_text>\<open>begin\<close> keyword as well, in order to continue the local theory immediately after the initial specification. Optionally given \<open>bundles\<close> only take effect in the surface context within the \<^theory_text>\<open>be \<^theory_text>\<open>end\<close> block. \<^descr> \<^theory_text>\<open>context bundles elements begin\<close> opens an unnamed context, the enclosing global or local theory target by the given declaration bundles (\secref{sec:bundle}) and context elements (\<^theory_text>\<open>fixes\<close>, \<^theory_t means any results stemming from definitions and proofs in the extended context will be exported into the enclosing target by lifting over extra parameters and premises. \<^descr> @{command (local) "end"} concludes the current local theory, according to the nesting of contexts. Note that a global @{command (global) "end"} has a different meaning: it concludes the theory itself (\secref{sec:begin-thy}). \<^descr> \<^theory_text>\<open>private\<close> or \<^theory_text>\<open>qualified\<close> may be gi theory command. This restricts name space accesses to the local scope, as determined by the enclosing \<^theory_text>\<open>context begin \<dots> end\<close> block. Outsid a \<^theory_text>\<open>private\<close> name is inaccessible, and a \<^theory_text>\<open>qualifi accessible with some qualification. Neither a global \<^theory_text>\<open>theory\<close> nor a \<^theory_text>\<open>locale\<close> ta itself: an extra unnamed context is required to use \<^theory_text>\<open>private\<close> or \<^theory_text>\<open>qualified\<close> here. \<^descr> \<open>(\<close>@{keyword_def "in"}~\<open>c)\<close> given after any local theory comma an immediate target, e.g.\ ``\<^theory_text>\<open>definition (in c)\<close>'' or ``\<^theory_text>\<open>theorem (in c)\<close>''. This works both in a local or global theory cont the current target context will be suspended for this command only. Note that ``\<^theory_text>\<open>(in -)\<close>'' will always produce a global result independently current target context. Any specification element that operates on \<open>local_theory\<close> according to this manual implicitly allows the above target syntax \<^theory_text>\<open>(in c)\<close>, but indiv syntax diagrams omit that aspect for clarity. \<^medskip> The exact meaning of results produced within a local theory context depends on the underlying target infrastructure (locale, type class etc.). The general idea is as follows, considering a context named \<open>c\<close> with parameter \<open>x\<close> and assumption \<open>A[x]\<close>. Definitions are exported by introducing a global version with additional arguments; a syntactic abbreviation links the long form with the abstract version of the target context. For example, \<open>a \<equiv> t[x]\<close> becomes \<open>c.a ?x \<equ t[?x]\<close> at the theory level (for arbitrary \<open>?x\<close>), together with a local abbreviation \<open>a \<equiv> c.a x\<close> in the target context (for the fixed parameter \<open>x\<close>). Theorems are exported by discharging the assumptions and generalizing the parameters of the context. For example, \<open>a: B[x]\<close> becomes \<open>c.a: A[?x] \<Longrig B[?x]\<close>, again for arbitrary \<open>?x\<close>. \<close> section \<open>Bundled declarations \label{sec:bundle}\<close> text \<open> \begin{matharray}{rcl} @{command_def "bundle"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \ @{command "bundle"} & : & \<open>theory \<rightarrow> local_theory\<close> \\ @{command_def "unbundle"} & : & \<open>local_theory \<rightarrow> local_theory\<clos @{command_def "print_bundles"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow> @{command_def "include"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> @{command_def "including"} & : & \<open>proof(prove) \<rightarrow> proof(prove)\<clo @{keyword_def "includes"} & : & syntax \\ @{keyword_def "opening"} & : & syntax \\ \end{matharray} The outer syntax of fact expressions (\secref{sec:syn-att}) involves theorems and attributes, which are evaluated in the context and applied to it. Attributes may declare theorems to the context, as in \<open>this_rule [intro] that_rule [elim]\<close> for example. Configuration options (\secref{sec:config}) are special declaration attributes that operate on the context without a theorem, as in \<open>[[show_types = false]]\<close> for example. Expressions of this form may be defined as \<^emph>\<open>bundled declarations\<close> in the context, and included in other situations later on. Including declaration bundles augments a local context casually without logical dependencies, which is in contrast to locales and locale interpretation (\secref{sec:locale}). \<^rail>\<open> (@@{command bundle} | @@{command open_bundle}) @{syntax name} \<newline> ( '=' @{syntax thms} @{syntax for_fixes} | @'begin') ; @@{command unbundle} @{syntax bundles} ; @@{command print_bundles} ('!'?) ; (@@{command include} | @@{command including}) @{syntax bundles} ; @{syntax_def "includes"}: @'includes' @{syntax bundles} ; @{syntax_def "opening"}: @'opening' @{syntax bundles} ; @{syntax bundles}: ('no')? @{syntax name} + @'and' \<close> \<^descr> \<^theory_text>\<open>bundle b = decls\<close> defines a bundle of declarations in the cur context. The RHS is similar to the one of the \<^theory_text>\<open>declare\<close> command. Bundl defined in local theory targets are subject to transformations via morphisms, when moved into different application contexts; this works analogously to any other local theory specification. \<^descr> \<^theory_text>\<open>bundle b begin body end\<close> defines a bundle of declarations fr \<open>body\<close> of local theory specifications. It may consist of commands that are technically equivalent to \<^theory_text>\<open>declare\<close> or \<^theory_text>\<open>declar \<^theory_text>\<open>notation\<close>, for example. Named fact declarations like ``\<^theory_ b\<close>'' or ``\<^theory_text>\<open>lemma a [simp]: B \<proof>\<close>'' are also admitted, but th bindings are not recorded in the bundle. \<^descr> \<^theory_text>\<open>open_bundle b\<close> is like \<^theory_text>\<open>bundle b\<close> declarations are activated immediately, but also named for later re-use. \<^descr> \<^theory_text>\<open>unbundle \<^vec>b\<close> activates the declarations from the give the current local theory context. This is analogous to \<^theory_text>\<open>lemmas\<close> (\secref{sec:theorems}) with the expanded bundles. \<^descr> \<^theory_text>\<open>print_bundles\<close> prints the named bundles that are availabl current context; the ``\<open>!\<close>'' option indicates extra verbosity. \<^descr> \<^theory_text>\<open>include \<^vec>b\<close> activates the declarations from the given proof body (forward mode). This is analogous to \<^theory_text>\<open>note\<close> (\secref{sec:proof-facts}) with the expanded bundles. \<^descr> \<^theory_text>\<open>including \<^vec>b\<close> is similar to \<^theory_text>\<open>inclu refinement (backward mode). This is analogous to \<^theory_text>\<open>using\<close> (\secref{sec:proof-facts}) with the expanded bundles. \<^descr> \<^theory_text>\<open>includes \<^vec>b\<close> is similar to \<^theory_text>\<open>includ specification context: unnamed \<^theory_text>\<open>context\<close>s and long statements of \<^theory_text>\<open>theorem\<close>. \<^descr> \<^theory_text>\<open>opening \<^vec>b\<close> is similar to \<^theory_text>\<open>include specification context: \<^theory_text>\<open>locale\<close>s, \<^theory_text>\<open>class\<clo effect is confined to the surface context within the specification block itself and the corresponding \<^theory_text>\<open>begin\<close> / \<^theory_text>\<open>end\<clo \<^descr> Bundle names may be prefixed by the reserved word \<^verbatim>\<open>no\<close> to indicat the polarity of certain declaration commands should be inverted, notably: \<^item> @{command syntax} versus @{command no_syntax} \<^item> @{command translations} versus @{command no_translations} \<^item> @{command notation} versus @{command no_notation} \<^item> @{command type_notation} versus @{command no_type_notation} \<^item> @{command adhoc_overloading} versus @{command no_adhoc_overloading} This also works recursively for the @{command unbundle} command as declaration inside a @{command bundle} definition: \<^verbatim>\<open>no\<close> means that both the order and polarity of declarations is reversed (following algebraic group laws). Here is an artificial example of bundling various configuration options: \<close> (*<*)experiment begin(*>*) bundle trace = [[simp_trace, linarith_trace, metis_trace, smt_trace]] lemma "x = x" including trace by metis (*<*)end(*>*) section \<open>Term definitions \label{sec:term-definitions}\<close> text \<open> \begin{matharray}{rcll} @{command_def "definition"} & : & \<open>local_theory \<rightarrow> local_theory\<cl @{attribute_def "defn"} & : & \<open>attribute\<close> \\ @{command_def "print_defn_rules"}\<open>\<^sup>*\<close> & : & \<open>context \<rightar @{command_def "abbreviation"} & : & \<open>local_theory \<rightarrow> local_theory\< @{command_def "print_abbrevs"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow> \end{matharray} Term definitions may either happen within the logic (as equational axioms of a certain form (see also \secref{sec:overloading}), or outside of it as rewrite system on abstract syntax. The second form is called ``abbreviation''. \<^rail>\<open> @@{command definition} decl? definition ; @@{command abbreviation} @{syntax mode}? decl? abbreviation ; @@{command print_abbrevs} ('!'?) ; decl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}? @'where' ; definition: @{syntax thmdecl}? @{syntax prop} @{syntax spec_prems} @{syntax for_fixes} ; abbreviation: @{syntax prop} @{syntax for_fixes} \<close> \<^descr> \<^theory_text>\<open>definition c where eq\<close> produces an internal definition \<op to the specification given as \<open>eq\<close>, which is then turned into a proven fact. The given proposition may deviate from internal meta-level equality according to the rewrite rules declared as @{attribute defn} by the object-logic. This usually covers object-level equality \<open>x = y\<close> and equivalence \<open>A \<longleftrightarrow> B\<close>. End-users normally need not change the @{a defn} setup. Definitions may be presented with explicit arguments on the LHS, as well as additional conditions, e.g.\ \<open>f x y = t\<close> instead of \<open>f \<equiv> \<lambda>x y. t\<close> \<Longrightarrow> g x y = u\<close> instead of an unrestricted \<open>g \<equiv> \<lambda>x y. u\<close>. \<^descr> \<^theory_text>\<open>print_defn_rules\<close> prints the definitional rewrite rules @{attribute defn} in the current context. \<^descr> \<^theory_text>\<open>abbreviation c where eq\<close> introduces a syntactic constant w associated with a certain term according to the meta-level equality \<open>eq\<close>. Abbreviations participate in the usual type-inference process, but are expanded before the logic ever sees them. Pretty printing of terms involves higher-order rewriting with rules stemming from reverted abbreviations. This needs some care to avoid overlapping or looping syntactic replacements! The optional \<open>mode\<close> specification restricts output to a particular print mode; using ``\<open>input\<close>'' here achieves the effect of one-way abbreviations. The mode may also include an ``\<^theory_text>\<open>output\<close>'' qualifier that affects the concrete syntax declared for abbreviations, cf.\ \<^theory_text>\<open>syntax\<close> in \secref{sec:syn-trans}. \<^descr> \<^theory_text>\<open>print_abbrevs\<close> prints all constant abbreviations of the c the ``\<open>!\<close>'' option indicates extra verbosity. \<close> section \<open>Axiomatizations \label{sec:axiomatizations}\<close> text \<open> \begin{matharray}{rcll} @{command_def "axiomatization"} & : & \<open>theory \<rightarrow> theory\<close> & \end{matharray} \<^rail>\<open> @@{command axiomatization} @{syntax vars}? (@'where' axiomatization)? ; axiomatization: (@{syntax thmdecl} @{syntax prop} + @'and') @{syntax spec_prems} @{syntax for_fixes} \<close> \<^descr> \<^theory_text>\<open>axiomatization c\<^sub>1 \<dots> c\<^sub>m where \<phi>\<^sub>1 \<dots> \<p simultaneously and states axiomatic properties for these. The constants are marked as being specified once and for all, which prevents additional specifications for the same constants later on, but it is always possible to emit axiomatizations without referring to particular constants. Note that lack of precise dependency tracking of axiomatizations may disrupt the well-formedness of an otherwise definitional theory. Axiomatization is restricted to a global theory context: support for local theory targets \secref{sec:target} would introduce an extra dimension of uncertainty what the written specifications really are, and make it infeasible to argue why they are correct. Axiomatic specifications are required when declaring a new logical system within Isabelle/Pure, but in an application environment like Isabelle/HOL the user normally stays within definitional mechanisms provided by the logic and its libraries. \<close> section \<open>Generic declarations\<close> text \<open> \begin{matharray}{rcl} @{command_def "declaration"} & : & \<open>local_theory \<rightarrow> local_theory\<c @{command_def "syntax_declaration"} & : & \<open>local_theory \<rightarrow> local_t @{command_def "declare"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \end{matharray} Arbitrary operations on the background context may be wrapped-up as generic declaration elements. Since the underlying concept of local theories may be subject to later re-interpretation, there is an additional dependency on a morphism that tells the difference of the original declaration context wrt.\ the application context encountered later on. A fact declaration is an important special case: it consists of a theorem which is applied to the context by means of an attribute. \<^rail>\<open> (@@{command declaration} | @@{command syntax_declaration}) ('(' @'pervasive' ')')? \<newline> @{syntax text} ; @@{command declare} (@{syntax thms} + @'and') \<close> \<^descr> \<^theory_text>\<open>declaration d\<close> adds the declaration function \<open>d\<clos application contexts, the function is transformed according to the morphisms being involved in the interpretation hierarchy. If the \<^theory_text>\<open>(pervasive)\<close> option is given, the corresponding declaratio applied to all possible contexts involved, including the global background theory. \<^descr> \<^theory_text>\<open>syntax_declaration\<close> is similar to \<^theory_text>\<open>de only ``syntactic'' tools by convention (such as notation and type-checking information). \<^descr> \<^theory_text>\<open>declare thms\<close> declares theorems to the current local theor theorem binding is involved here, unlike \<^theory_text>\<open>lemmas\<close> (cf.\ \secref{sec:theorems}), so \<^theory_text>\<open>declare\<close> only has the effect of applyi attributes as included in the theorem specification. \<close> section \<open>Locales \label{sec:locale}\<close> text \<open> A locale is a functor that maps parameters (including implicit type parameters) and a specification to a list of declarations. The syntax of locales is modeled after the Isar proof context commands (cf.\ \secref{sec:proof-context}). Locale hierarchies are supported by maintaining a graph of dependencies between locale instances in the global theory. Dependencies may be introduced through import (where a locale is defined as sublocale of the imported instances) or by proving that an existing locale is a sublocale of one or several locale instances. A locale may be opened with the purpose of appending to its list of declarations (cf.\ \secref{sec:target}). When opening a locale declarations from all dependencies are collected and are presented as a local theory. In this process, which is called \<^emph>\<open>roundup\<close>, redundant locale instances are omitted. A locale instance is redundant if it is subsumed by an instance encountered earlier. A more detailed description of this process is available elsewhere \<^cite>\<open>Ballarin2014\<close>. \<close> subsection \<open>Locale expressions \label{sec:locale-expr}\<close> text \<open> A \<^emph>\<open>locale expression\<close> denotes a context composed of instances of existing locales. The context consists of the declaration elements from the locale instances. Redundant locale instances are omitted according to roundup. \<^rail>\<open> @{syntax_def locale_expr}: (instance + '+') @{syntax for_fixes} ; instance: (qualifier ':')? @{syntax name} (pos_insts | named_insts) \<newline> rewrites? ; qualifier: @{syntax name} ('?')? ; pos_insts: ('_' | @{syntax term})* ; named_insts: @'where' (@{syntax name} '=' @{syntax term} + @'and') ; rewrites: @'rewrites' (@{syntax thmdecl}? @{syntax prop} + @'and') \<close> A locale instance consists of a reference to a locale and either positional or named parameter instantiations optionally followed by rewrites clauses. Identical instantiations (that is, those that instantiate a parameter by itself) may be omitted. The notation ``\<open>_\<close>'' enables to omit the instantiation for a parameter inside a positional instantiation. Terms in instantiations are from the context the locale expressions is declared in. Local names may be added to this context with the optional \<^theory_text>\<open>for\<close> clause. This is useful for shadowing names bound in outer conte and for declaring syntax. In addition, syntax declarations from one instance are effective when parsing subsequent instances of the same expression. Instances have an optional qualifier which applies to names in declarations. Names include local definitions and theorem names. If present, the qualifier itself is either mandatory (default) or non-mandatory (when followed by ``\<^verbatim>\<open>?\<close>''). Non-mandatory means that the qualifier may be omitted on inpu Qualifiers only affect name spaces; they play no role in determining whether one locale instance subsumes another. Rewrite clauses amend instances with equations that act as rewrite rules. This is particularly useful for changing concepts introduced through definitions. Rewrite clauses are available only in interpretation commands (see \secref{sec:locale-interpretation} below) and must be proved the user. \<close> subsection \<open>Locale declarations\<close> text \<open> \begin{tabular}{rcl} @{command_def "locale"} & : & \<open>theory \<rightarrow> local_theory\<close> \\ @{command_def "experiment"} & : & \<open>theory \<rightarrow> local_theory\<close> \\ @{command_def "print_locale"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\< @{command_def "print_locales"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow> @{command_def "locale_deps"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<c \end{tabular} @{index_ref \<open>\<^theory_text>\<open>fixes\<close> (element)\<close>} @{index_ref \<open>\<^theory_text>\<open>constrains\<close> (element)\<close>} @{index_ref \<open>\<^theory_text>\<open>assumes\<close> (element)\<close>} @{index_ref \<open>\<^theory_text>\<open>defines\<close> (element)\<close>} @{index_ref \<open>\<^theory_text>\<open>notes\<close> (element)\<close>} \<^rail>\<open> @@{command locale} @{syntax name} ('=' @{syntax locale})? @'begin'? ; @@{command experiment} (@{syntax context_elem}*) @'begin' ; @@{command print_locale} '!'? @{syntax name} ; @@{command print_locales} ('!'?) ; @{syntax_def locale}: @{syntax context_elem}+ | @{syntax_ref "opening"} ('+' (@{syntax context_elem}+))? | @{syntax locale_expr} @{syntax_ref "opening"}? ('+' (@{syntax context_elem}+))? ; @{syntax_def context_elem}: @'fixes' @{syntax vars} | @'constrains' (@{syntax name} '::' @{syntax type} + @'and') | @'assumes' (@{syntax props} + @'and') | @'defines' (@{syntax thmdecl}? @{syntax prop} @{syntax prop_pat}? + @'and') | @'notes' (@{syntax thmdef}? @{syntax thms} + @'and') \<close> \<^descr> \<^theory_text>\<open>locale loc = import opening bundles + body\<close> defines a new loc as a context consisting of a certain view of existing locales (\<open>import\<close>) plus some additional elements (\<open>body\<close>) with declaration \<open>bundles\<close> enriching the of the command itself. All \<open>import\<close>, \<open>bundles\<close> and \<open>body\<close> are o degenerate form \<^theory_text>\<open>locale loc\<close> defines an empty locale, which may stil useful to collect declarations of facts later on. Type-inference on locale expressions automatically takes care of the most general typing that the combined context elements may acquire. The \<open>import\<close> consists of a locale expression; see \secref{sec:locale-expr} above. Its \<^theory_text>\<open>for\<close> clause defines the parameters of \<open>import\<clos parameters of the defined locale. Locale parameters whose instantiation is omitted automatically extend the (possibly empty) \<^theory_text>\<open>for\<close> clause: th inserted at its beginning. This means that these parameters may be referred to from within the expression and also in the subsequent context elements and provides a notational convenience for the inheritance of parameters in locale declarations. Declarations from \<open>bundles\<close>, see \secref{sec:bundle}, are effective in the entire command including a subsequent \<^theory_text>\<open>begin\<close> / \<^theory_text>\<ope not contribute to the declarations stored in the locale. The \<open>body\<close> consists of context elements: \<^descr> @{element "fixes"}~\<open>x :: \<tau> (mx)\<close> declares a local parameter of type \<ope and mixfix annotation \<open>mx\<close> (both are optional). The special syntax declaration ``\<open>(\<close>@{keyword_ref "structure"}\<open>)\<close>'' means that \<open>x\< referenced implicitly in this context. \<^descr> @{element "constrains"}~\<open>x :: \<tau>\<close> introduces a type constraint \<open>\<t local parameter \<open>x\<close>. This element is deprecated. The type constraint should be introduced in the \<^theory_text>\<open>for\<close> clause or the relevant @{element "fixes"} element. \<^descr> @{element "assumes"}~\<open>a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close> introduces local to \<^theory_text>\<open>assume\<close> within a proof (cf.\ \secref{sec:proof-context}). \<^descr> @{element "defines"}~\<open>a: x \<equiv> t\<close> defines a previously declared parame This is similar to \<^theory_text>\<open>define\<close> within a proof (cf.\ \secref{sec:proof-context}), but @{element "defines"} is restricted to Pure equalities and the defined variable needs to be declared beforehand via @{element "fixes"}. The left-hand side of the equation may have additional arguments, e.g.\ ``@{element "defines"}~\<open>f x\<^sub>1 \<dots> x\<^sub>n \<equiv> t\< which need to be free in the context. \<^descr> @{element "notes"}~\<open>a = b\<^sub>1 \<dots> b\<^sub>n\<close> reconsiders facts within a context. Most notably, this may include arbitrary declarations in any attribute specifications included here, e.g.\ a local @{attribute simp} rule. Both @{element "assumes"} and @{element "defines"} elements contribute to the locale specification. When defining an operation derived from the parameters, \<^theory_text>\<open>definition\<close> (\secref{sec:term-definitions}) is us appropriate. Note that ``\<^theory_text>\<open>(is p\<^sub>1 \<dots> p\<^sub>n)\<close>'' patterns given in the syn "assumes"} and @{element "defines"} above are illegal in locale definitions. In the long goal format of \secref{sec:goals}, term bindings may be included as expected, though. \<^medskip> Locale specifications are ``closed up'' by turning the given text into a predicate definition \<open>loc_axioms\<close> and deriving the original assumptions as local lemmas (modulo local definitions). The predicate statement covers only the newly specified assumptions, omitting the content of included locale expressions. The full cumulative view is only provided on export, involving another predicate \<open>loc\<close> that refers to the complete specification text. In any case, the predicate arguments are those locale parameters that actually occur in the respective piece of text. Also these predicates operate at the meta-level in theory, but the locale packages attempts to internalize statements according to the object-logic setup (e.g.\ replacing \<open>\<And>\<close> by \<open>\<forall>\<close>, and \<open>\<Longrightarrow>\<close> by \<open>\<longrig Separate introduction rules \<open>loc_axioms.intro\<close> and \<open>loc.intro\<close> are pr as well. \<^descr> \<^theory_text>\<open>experiment body begin\<close> opens an anonymous locale context w naming policy. Specifications in its body are inaccessible from outside. This is useful to perform experiments, without polluting the name space. \<^descr> \<^theory_text>\<open>print_locale "locale"\<close> prints the contents of the named lo command omits @{element "notes"} elements by default. Use \<^theory_text>\<open>print_locale to have them included. \<^descr> \<^theory_text>\<open>print_locales\<close> prints the names of all locales of the curre the ``\<open>!\<close>'' option indicates extra verbosity. \<^descr> \<^theory_text>\<open>locale_deps\<close> visualizes all locales and their relations a diagram. This includes locales defined as type classes (\secref{sec:class}). \<close> subsection \<open>Locale interpretation \label{sec:locale-interpretation}\<close> text \<open> \begin{matharray}{rcl} @{command "interpretation"} & : & \<open>local_theory \<rightarrow> proof(prove)\<cl @{command_def "interpret"} & : & \<open>proof(state) | proof(chain) \<rightarrow> pro @{command_def "global_interpretation"} & : & \<open>theory | local_theory \<rightar @{command_def "sublocale"} & : & \<open>theory | local_theory \<rightarrow> proof(pro @{command_def "print_interps"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow> @{method_def intro_locales} & : & \<open>method\<close> \\ @{method_def unfold_locales} & : & \<open>method\<close> \\ @{attribute_def trace_locales} & : & \mbox{\<open>attribute\<close> \quad default \<o \end{matharray} Locales may be instantiated, and the resulting instantiated declarations added to the current context. This requires proof (of the instantiated specification) and is called \<^emph>\<open>locale interpretation\<close>. Interpretation is possible within arbitrary local theories (\<^theory_text>\<open>interpretation\<close>), wit bodies (\<^theory_text>\<open>interpret\<close>), into global theories (\<^theory_text>\<open>g into locales (\<^theory_text>\<open>sublocale\<close>). \<^rail>\<open> @@{command interpretation} @{syntax locale_expr} ; @@{command interpret} @{syntax locale_expr} ; @@{command global_interpretation} @{syntax locale_expr} definitions? ; @@{command sublocale} (@{syntax name} ('<' | '\ definitions? ; @@{command print_interps} @{syntax name} ; definitions: @'defines' (@{syntax thmdecl}? @{syntax name} \<newline> @{syntax mixfix}? '=' @{syntax term} + @'and'); \<close> The core of each interpretation command is a locale expression \<open>expr\<close>; the command generates proof obligations for the instantiated specifications. Once these are discharged by the user, instantiated declarations (in particular, facts) are added to the context in a post-processing phase, in a manner specific to each command. Interpretation commands are aware of interpretations that are already active: post-processing is achieved through a variant of roundup that takes interpretations of the current global or local theory into account. In order to simplify the proof obligations according to existing interpretations use methods @{method intro_locales} or @{method unfold_locales}. Rewrites clauses \<^theory_text>\<open>rewrites eqns\<close> occur within expressions. They am morphism through which a locale instance is interpreted with rewrite rules, also called rewrite morphisms. This is particularly useful for interpreting concepts introduced through definitions. The equations must be proved the user. To enable syntax of the instantiated locale within the equation, while reading a locale expression, equations of a locale instance are read in a temporary context where the instance is already activated. If activation fails, typically due to duplicate constant declarations, processing falls back to reading the equation first. Given definitions \<open>defs\<close> produce corresponding definitions in the local theory's underlying target \<^emph>\ stemming from the symmetric of those definitions. Hence these need not be proved explicitly the user. Such rewrite definitions are a even more useful device for interpreting concepts introduced through definitions, but they are only supported for interpretation commands operating in a local theory whose implementing target actually supports this. Note that despite the suggestive \<^theory_text>\<open>and\<close> connective, \<open>defs\<close> are processed sequentially without mutual recursion. \<^descr> \<^theory_text>\<open>interpretation expr\<close> interprets \<open>expr\<close> into a l such that its lifetime is limited to the current context block (e.g. a locale or unnamed context). At the closing @{command end} of the block the interpretation and its declarations disappear. Hence facts based on interpretation can be established without creating permanent links to the interpreted locale instances, as would be the case with @{command sublocale}. When used on the level of a global theory, there is no end of a current context block, hence \<^theory_text>\<open>interpretation\<close> behaves identically to \<^theory_text>\<open>global_interpretation\<close> then. \<^descr> \<^theory_text>\<open>interpret expr\<close> interprets \<open>expr\<close> into a proof c the interpretation and its declarations disappear when closing the current proof block. Note that for \<^theory_text>\<open>interpret\<close> the \<open>eqns\<close> should b universally quantified. \<^descr> \<^theory_text>\<open>global_interpretation expr defines defs\<close> interprets \<op into a global theory. When adding declarations to locales, interpreted versions of these declarations are added to the global theory for all interpretations in the global theory as well. That is, interpretations into global theories dynamically participate in any declarations added to locales. Free variables in the interpreted expression are allowed. They are turned into schematic variables in the generated declarations. In order to use a free variable whose name is already bound in the context --- for example, because a constant of that name exists --- add it to the \<^theory_text>\<open>for\<close> clause. When used in a nested target, resulting declarations are propagated through the whole target stack. \<^descr> \<^theory_text>\<open>sublocale name \<subseteq> expr defines defs\<close> interprets \<o into the locale \<open>name\<close>. A proof that the specification of \<open>name\<close> implies t specification of \<open>expr\<close> is required. As in the localized version of the theorem command, the proof is in the context of \<open>name\<close>. After the proof obligation has been discharged, the locale hierarchy is changed as if \<open>name\<close> imported \<open>expr\<close> (hence the name \<^theory_text>\<open>sublocale\<close>). When the co subsequently entered, traversing the locale hierarchy will involve the locale instances of \<open>expr\<close>, and their declarations will be added to the context. This makes \<^theory_text>\<open>sublocale\<close> dynamic: extensions of a locale tha instantiated in \<open>expr\<close> may take place after the \<^theory_text>\<open>sublocale\<clo still become available in the context. Circular \<^theory_text>\<open>sublocale\<close> declar are allowed as long as they do not lead to infinite chains. If interpretations of \<open>name\<close> exist in the current global theory, the command adds interpretations for \<open>expr\<close> as well, with the same qualifier, although only for fragments of \<open>expr\<close> that are not interpreted in the theory already. Rewrites clauses in the expression or rewrite definitions \<open>defs\<close> can help break infinite chains induced by circular \<^theory_text>\<open>sublocale\<close> declarations. In a named context block the \<^theory_text>\<open>sublocale\<close> command may also be used, but locale argument must be omitted. The command then refers to the locale (or class) target of the context block. \<^descr> \<^theory_text>\<open>print_interps name\<close> lists all interpretations of locale \< current theory or proof context, including those due to a combination of an \<^theory_text>\<open>interpretation\<close> or \<^theory_text>\<open>interpret\<close> and one o declarations. \<^descr> @{method intro_locales} and @{method unfold_locales} repeatedly expand all introduction rules of locale predicates of the theory. While @{method intro_locales} only applies the \<open>loc.intro\<close> introduction rules and therefore does not descend to assumptions, @{method unfold_locales} is more aggressive and applies \<open>loc_axioms.intro\<close> as well. Both methods are aware of locale specifications entailed by the context, both from target statements, and from interpretations (see below). New goals that are entailed by the current context are discharged automatically. While @{method unfold_locales} is part of the default method for \<^theory_text>\<open>proof\<c and often invoked ``behind the scenes'', @{method intro_locales} helps understand which proof obligations originated from which locale instances. The latter method is useful while developing proofs but rare in finished developments. \<^descr> @{attribute trace_locales}, when set to \<open>true\<close>, prints the locale instances activated during roundup. Use this when locale commands yield obscure errors or for understanding local theories created by complex locale hierarchies. \begin{warn} If a global theory inherits declarations (body elements) for a locale from one parent and an interpretation of that locale from another parent, the interpretation will not be applied to the declarations. \end{warn} \begin{warn} Since attributes are applied to interpreted theorems, interpretation may modify the context of common proof tools, e.g.\ the Simplifier or Classical Reasoner. As the behaviour of such tools is \<^emph>\<open>not\<close> stable under interpretation morphisms, manual declarations might have to be added to the target context of the interpretation to revert such declarations. \end{warn} \begin{warn} An interpretation in a local theory or proof context may subsume previous interpretations. This happens if the same specification fragment is interpreted twice and the instantiation of the second interpretation is more general than the interpretation of the first. The locale package does not attempt to remove subsumed interpretations. \end{warn} \begin{warn} While \<^theory_text>\<open>interpretation (in c) \<dots>\<close> is admissible, it is not useful s its result is discarded immediately. \end{warn} \<close> section \<open>Classes \label{sec:class}\<close> text \<open> \begin{matharray}{rcl} @{command_def "class"} & : & \<open>theory \<rightarrow> local_theory\<close> \\ @{command_def "instantiation"} & : & \<open>theory \<rightarrow> local_theory\<close> @{command_def "instance"} & : & \<open>local_theory \<rightarrow> local_theory\<clos @{command "instance"} & : & \<open>theory \<rightarrow> proof(prove)\<close> \\ @{command_def "subclass"} & : & \<open>local_theory \<rightarrow> local_theory\<clos @{command_def "print_classes"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow> @{command_def "class_deps"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<cl @{method_def intro_classes} & : & \<open>method\<close> \\ \end{matharray} A class is a particular locale with \<^emph>\<open>exactly one\<close> type variable \<open>\<alpha>\< the underlying locale, a corresponding type class is established which is interpreted logically as axiomatic type class \<^cite>\<open>"Wenzel:1997:TPHOL"\<close> whose logical content are the assumptions of the locale. Thus, classes provide the full generality of locales combined with the commodity of type classes (notably type-inference). See \<^cite>\<open>"isabelle-classes"\<close> for a short tutorial. \<^rail>\<open> @@{command class} class_spec @'begin'? ; class_spec: @{syntax name} '=' ((@{syntax name} @{syntax_ref "opening"}? '+' (@{syntax context_elem}+)) | @{syntax name} @{syntax_ref "opening"}? | @{syntax_ref "opening"}? '+' (@{syntax context_elem}+)) ; @@{command instantiation} (@{syntax name} + @'and') '::' @{syntax arity} @'begin' ; @@{command instance} (() | (@{syntax name} + @'and') '::' @{syntax arity} | @{syntax name} ('<' | '\ ; @@{command subclass} @{syntax name} ; @@{command class_deps} (class_bounds class_bounds?)? ; class_bounds: @{syntax sort} | '(' (@{syntax sort} + @'|') ')' \<close> \<^descr> \<^theory_text>\<open>class c = superclasses bundles + body\<close> defines a new class \<o \<open>superclasses\<close>. This introduces a locale \<open>c\<close> with import of all locales \<open>superclasses\<close>. Any @{element "fixes"} in \<open>body\<close> are lifted to the global theory level (\<^emph>\<open>class operations\<close> \<open>f\<^sub>1, \<dots>, f\<^sub>n\<close> of class \<open>c\<c parameter \<open>\<alpha>\<close> to a schematic type variable \<open>?\<alpha> :: c\<close>. Likewise, @{element "assumes"} in \<open>body\<close> are also lifted, mapping each local parameter \<open>f :: \<tau>[\<alpha>]\<close> to its corresponding global constant \<open>f :: \<tau>[ c]\<close>. The corresponding introduction rule is provided as \<open>c_class_axioms.intro\<close>. This rule should be rarely needed directly --- the @{method intro_classes} method takes care of the details of class membership proofs. Optionally given \<open>bundles\<close> take effect in the surface context within the \<open>body\<close> and the potentially following \<^theory_text>\<open>begin\<close> / \<^theory_ \<^descr> \<^theory_text>\<open>instantiation t :: (s\<^sub>1, \<dots>, s\<^sub>n)s begin\<close> open \secref{sec:target}) which allows to specify class operations \<open>f\<^sub>1, \<dots>, f\<^sub> corresponding to sort \<open>s\<close> at the particular type instance \<open>(\<alpha>\<^sub>1 :: s\< \<alpha>\<^sub>n :: s\<^sub>n) t\<close>. A plain \<^theory_text>\<open>instance\<close> command in the stating these type arities. The target is concluded by an @{command_ref (local) "end"} command. Note that a list of simultaneous type constructors may be given; this corresponds nicely to mutually recursive type definitions, e.g.\ in Isabelle/HOL. \<^descr> \<^theory_text>\<open>instance\<close> in an instantiation target body sets up a goal sta type arities claimed at the opening \<^theory_text>\<open>instantiation\<close>. The proof woul usually proceed by @{method intro_classes}, and then establish the characteristic theorems of the type classes involved. After finishing the proof, the background theory will be augmented by the proven type arities. On the theory level, \<^theory_text>\<open>instance t :: (s\<^sub>1, \<dots>, s\<^sub>n)s\<close> prov way to instantiate a type class with no need to specify operations: one can continue with the instantiation proof immediately. \<^descr> \<^theory_text>\<open>subclass c\<close> in a class context for class \<open>d\<close> sets u class \<open>c\<close> is logically contained in class \<open>d\<close>. After finishing the proof, class \<open>d\<close> is proven to be subclass \<open>c\<close> and the locale \<open>c\<close> is inter into \<open>d\<close> simultaneously. A weakened form of this is available through a further variant of @{command instance}: \<^theory_text>\<open>instance c\<^sub>1 \<subseteq> c\<^sub>2\<close> opens a proof that \<open>c\<^sub>1\<close> without reference to the underlying locales; this is useful if the properties to prove the logical connection are not sufficient on the locale level but on the theory level. \<^descr> \<^theory_text>\<open>print_classes\<close> prints all classes in the current theory. \<^descr> \<^theory_text>\<open>class_deps\<close> visualizes classes and their subclass relati directed acyclic graph. By default, all classes from the current theory context are show. This may be restricted by optional bounds as follows: \<^theory_text>\<open>class_deps upper\<close> or \<^theory_text>\<open>class_deps upper lower\< it is a subclass of some sort from \<open>upper\<close> and a superclass of some sort from \<open>lower\<close>. \<^descr> @{method intro_classes} repeatedly expands all class introduction rules of this theory. Note that this method usually needs not be named explicitly, as it is already included in the default proof step (e.g.\ of \<^theory_text>\<open>proof\<close>). I particular, instantiation of trivial (syntactic) classes may be performed by a single ``\<^theory_text>\<open>..\<close>'' proof step. \<close> subsection \<open>The class target\<close> text \<open> %FIXME check A named context may refer to a locale (cf.\ \secref{sec:target}). If this locale is also a class \<open>c\<close>, apart from the common locale target behaviour the following happens. \<^item> Local constant declarations \<open>g[\<alpha>]\<close> referring to the local type parame \<open>\<alpha>\<close> and local parameters \<open>f[\<alpha>]\<close> are accompanied by theory-le \<open>g[?\<alpha> :: c]\<close> referring to theory-level class operations \<open>f[?\<alpha> :: c] \<^item> Local theorem bindings are lifted as are assumptions. \<^item> Local syntax refers to local operations \<open>g[\<alpha>]\<close> and global operations \<open>g[?\<alpha> :: c]\<close> uniformly. Type inference resolves ambiguities. In rare cases, manual type annotations are needed. \<close> subsection \<open>Co-regularity of type classes and arities\<close> text \<open> The class relation together with the collection of type-constructor arities must obey the principle of \<^emph>\<open>co-regularity\<close> as defined below. \<^medskip> For the subsequent formulation of co-regularity we assume that the class relation is closed by transitivity and reflexivity. Moreover the collection of arities \<open>t :: (\<^vec>s)c\<close> is completed such that \<open>t :: (\<^vec>s)c\<close> and \<open>c \<subseteq> c'\<close> implies \<open>t :: (\<^vec>s)c'\<close> for all such declarations. Treating sorts as finite sets of classes (meaning the intersection), the class relation \<open>c\<^sub>1 \<subseteq> c\<^sub>2\<close> is extended to sorts as follows: \[ \<open>s\<^sub>1 \<subseteq> s\<^sub>2 \<equiv> \<forall>c\<^sub>2 \<in> s\<^sub>2. \<exists>c\<^sub>1 \<in> s\<^s \] This relation on sorts is further extended to tuples of sorts (of the same length) in the component-wise way. \<^medskip> Co-regularity of the class relation together with the arities relation means: \[ \<open>t :: (\<^vec>s\<^sub>1)c\<^sub>1 \<Longrightarrow> t :: (\<^vec>s\<^sub>2)c\<^sub>2 \<Longrightar \] for all such arities. In other words, whenever the result classes of some type-constructor arities are related, then the argument sorts need to be related in the same way. \<^medskip> Co-regularity is a very fundamental property of the order-sorted algebra of types. For example, it entails principal types and most general unifiers, e.g.\ see \<^cite>\<open>"nipkow-prehofer"\<close>. \<close> section \<open>Overloaded constant definitions \label{sec:overloading}\<close> text \<open> Definitions essentially express abbreviations within the logic. The simplest form of a definition is \<open>c :: \<sigma> \<equiv> t\<close>, where \<open>c\<close> is a new constant an a closed term that does not mention \<open>c\<close>. Moreover, so-called \<^emph>\<open>hidden polymorphism\<close> is excluded: all type variables in \<open>t\<close> need to occur in its type \<open>\<sigma>\<close>. \<^emph>\<open>Overloading\<close> means that a constant being declared as \<open>c :: \<alpha> decl\< defined separately on type instances \<open>c :: (\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n)\<kappa> dec type constructor \<open>\<kappa>\<close>. At most occasions overloading will be used in a Haskell-like fashion together with type classes by means of \<^theory_text>\<open>instantiati (see \secref{sec:class}). Sometimes low-level overloading is desirable; this is supported by \<^theory_text>\<open>consts\<close> and \<^theory_text>\<open>overloading\<clos The right-hand side of overloaded definitions may mention overloaded constants recursively at type instances corresponding to the immediate argument types \<open>\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n\<close>. Incomplete specification pat global constraints on all occurrences. E.g.\ \<open>d :: \<alpha> \<times> \<alpha>\<close> on the left side means that all corresponding occurrences on some right-hand side need to be an instance of this, and general \<open>d :: \<alpha> \<times> \<beta>\<close> will be disallowed. F details are given by Kun\v{c}ar \<^cite>\<open>"Kuncar:2015"\<close>. \<^medskip> The \<^theory_text>\<open>consts\<close> command and the \<^theory_text>\<open>overloading\<clos interface for end-users. Regular specification elements such as @{command definition}, @{command inductive}, @{command function} may be used in the body. It is also possible to use \<^theory_text>\<open>consts c :: \<sigma>\<close> with later \<^theo \<equiv> c :: \<sigma>\<close> to keep the declaration and definition of a constant separate. \begin{matharray}{rcl} @{command_def "consts"} & : & \<open>theory \<rightarrow> theory\<close> \\ @{command_def "overloading"} & : & \<open>theory \<rightarrow> local_theory\<close> \\ \end{matharray} \<^rail>\<open> @@{command consts} ((@{syntax name} '::' @{syntax type} @{syntax mixfix}?) +) ; @@{command overloading} ( spec + ) @'begin' ; spec: @{syntax name} ( '\ \<close> \<^descr> \<^theory_text>\<open>consts c :: \<sigma>\<close> declares constant \<open>c\<close> to have \<open>\<sigma>\<close>. The optional mixfix annotations may attach concrete syntax to the constants declared. \<^descr> \<^theory_text>\<open>overloading x\<^sub>1 \<equiv> c\<^sub>1 :: \<tau>\<^sub>1 \<dots> x\<^sub>n a theory target (cf.\ \secref{sec:target}) which allows to specify already declared constants via definitions in the body. These are identified by an explicitly given mapping from variable names \<open>x\<^sub>i\<close> to constants \<open>c\<^sub>i particular type instances. The definitions themselves are established using common specification tools, using the names \<open>x\<^sub>i\<close> as reference to the corresponding constants. Option \<^theory_text>\<open>(unchecked)\<close> disables global dependency checks for the corresponding definition, which is occasionally useful for exotic overloading; this is a form of axiomatic specification. It is at the discretion of the user to avoid malformed theory specifications! \<close> subsubsection \<open>Example\<close> consts Length :: "'a \ overloading Length\<^sub>0 \<equiv> "Length :: unit \<Rightarrow> nat" Length\<^sub>1 \<equiv> "Length :: 'a \<times> unit \<Rightarrow> nat" Length\<^sub>2 \<equiv> "Length :: 'a \<times> 'b \<times> unit \<Rightarrow> nat" Length\<^sub>3 \<equiv> "Length :: 'a \<times> 'b \<times> 'c \<times> unit \<Rightarrow> nat" begin fun Length\<^sub>0 :: "unit \<Rightarrow> nat" where "Length\<^sub>0 () = 0" fun Length\<^sub>1 :: "'a \<times> unit \<Rightarrow> nat" where "Length\<^sub>1 (a, ()) = 1" fun Length\<^sub>2 :: "'a \<times> 'b \<times> unit \<Rightarrow> nat" where "Length\<^sub>2 (a, b, ()) = fun Length\<^sub>3 :: "'a \<times> 'b \<times> 'c \<times> unit \<Rightarrow> nat" where "Length\<^sub>3 ( end lemma "Length (a, b, c, ()) = 3" by simp lemma "Length ((a, b), (c, d), ()) = 2" by simp lemma "Length ((a, b, c, d, e), ()) = 1" by simp section \<open>Overloaded constant abbreviations: adhoc overloading\<close> text \<open> \begin{tabular}{rcll} @{command_def "adhoc_overloading"} & : & \<open>local_theory \<rightarrow> local_th @{command_def "no_adhoc_overloading"} & : & \<open>local_theory \<rightarrow> local @{attribute_def "show_variants"} & : & \<open>attribute\<close> & default \<open>f \end{tabular} \<^medskip> Adhoc overloading allows to overload a constant depending on its type. Typically this involves the introduction of an uninterpreted constant (used for input and output) and the addition of some variants (used internally). For examples see \<^file>\<open>~~/src/HOL/Examples/Adhoc_Overloading.thy\<close> and \<^file>\<open>~~/src/HOL/Library/Monad_Syntax.thy\<close>. \<^rail>\<open> (@@{command adhoc_overloading} | @@{command no_adhoc_overloading}) \<newline> (@{syntax name} ('==' | '\ \<close> \<^descr> @{command "adhoc_overloading"}~\<open>c \<rightleftharpoons> v\<^sub>1 ... v\<^sub>n\<c existing constant. \<^descr> @{command "no_adhoc_overloading"} is similar to @{command "adhoc_overloading"}, but removes the specified variants from the present context. \<^descr> @{attribute "show_variants"} controls printing of variants of overloaded constants. If enabled, the internally used variants are printed instead of their respective overloaded constants. This is occasionally useful to check whether the system agrees with a user's expectations about derived variants. \<close> section \<open>Incorporating ML code \label{sec:ML}\<close> text \<open> \begin{matharray}{rcl} @{command_def "SML_file"} & : & \<open>local_theory \<rightarrow> local_theory\<clos @{command_def "SML_file_debug"} & : & \<open>local_theory \<rightarrow> local_theor @{command_def "SML_file_no_debug"} & : & \<open>local_theory \<rightarrow> local_th @{command_def "ML_file"} & : & \<open>local_theory \<rightarrow> local_theory\<close> @{command_def "ML_file_debug"} & : & \<open>local_theory \<rightarrow> local_theory @{command_def "ML_file_no_debug"} & : & \<open>local_theory \<rightarrow> local_the @{command_def "ML"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\ @{command_def "ML_export"} & : & \<open>local_theory \<rightarrow> local_theory\<clo @{command_def "ML_prf"} & : & \<open>proof \<rightarrow> proof\<close> \\ @{command_def "ML_val"} & : & \<open>any \<rightarrow>\<close> \\ @{command_def "ML_command"} & : & \<open>any \<rightarrow>\<close> \\ @{command_def "setup"} & : & \<open>theory \<rightarrow> theory\<close> \\ @{command_def "local_setup"} & : & \<open>local_theory \<rightarrow> local_theory\<c @{command_def "attribute_setup"} & : & \<open>local_theory \<rightarrow> local_theo \end{matharray} \begin{tabular}{rcll} @{attribute_def ML_print_depth} & : & \<open>attribute\<close> & default 10 \\ @{attribute_def ML_source_trace} & : & \<open>attribute\<close> & default \<open>f @{attribute_def ML_debugger} & : & \<open>attribute\<close> & default \<open>false @{attribute_def ML_exception_trace} & : & \<open>attribute\<close> & default \<op @{attribute_def ML_exception_debugger} & : & \<open>attribute\<close> & default @{attribute_def ML_environment} & : & \<open>attribute\<close> & default \<open>Is \end{tabular} \<^rail>\<open> (@@{command SML_file} | @@{command SML_file_debug} | @@{command SML_file_no_debug} | @@{command ML_file} | @@{command ML_file_debug} | @@{command ML_file_no_debug}) @{syntax name} ';'? ; (@@{command ML} | @@{command ML_export} | @@{command ML_prf} | @@{command ML_val} | @@{command ML_command} | @@{command setup} | @@{command local_setup}) @{syntax text} ; @@{command attribute_setup} @{syntax name} '=' @{syntax text} @{syntax text}? \<close> \<^descr> \<^theory_text>\<open>SML_file name\<close> reads and evaluates the given Standard ML fi --> -------------------- --> maximum size reached --> -------------------- ¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.16Bemerkung: (vorverarbeitet) ¤*Bot Zugriff |
|
2026-03-28