--- a/doc-src/IsarRef/Thy/Spec.thy Tue Aug 28 12:31:53 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1337 +0,0 @@
-theory Spec
-imports Base Main
-begin
-
-chapter {* Specifications *}
-
-text {*
- The Isabelle/Isar theory format integrates specifications and
- proofs, supporting interactive development with unlimited undo
- operation. There is an integrated 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 @{command theorem} or @{command lemma} at the theory
- level, and left again with the final conclusion (e.g.\ via @{command
- qed}). Some theory specification mechanisms also require a proof,
- such as @{command typedef} in HOL, which demands non-emptiness of
- the representing sets.
-*}
-
-
-section {* Defining theories \label{sec:begin-thy} *}
-
-text {*
- \begin{matharray}{rcl}
- @{command_def "theory"} & : & @{text "toplevel \<rightarrow> theory"} \\
- @{command_def (global) "end"} & : & @{text "theory \<rightarrow> toplevel"} \\
- \end{matharray}
-
- Isabelle/Isar theories are defined via theory files, which may
- contain both specifications and proofs; occasionally definitional
- mechanisms also require some explicit proof. The theory body may be
- sub-structured by means of \emph{local theory targets}, such as
- @{command "locale"} and @{command "class"}.
-
- The first proper command of a theory is @{command "theory"}, which
- indicates imports of previous theories and optional dependencies on
- other source files (usually in ML). Just preceding the initial
- @{command "theory"} command there may be an optional @{command
- "header"} declaration, which is only relevant to document
- preparation: see also the other section markup commands in
- \secref{sec:markup}.
-
- 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"},
- although some user-interfaces might pretend that trailing input is
- admissible.
-
- @{rail "
- @@{command theory} @{syntax name} imports \\ keywords? uses? @'begin'
- ;
- imports: @'imports' (@{syntax name} +)
- ;
- keywords: @'keywords' ((@{syntax string} +) ('::' @{syntax name} @{syntax tags})? + @'and')
- ;
- uses: @'uses' ((@{syntax name} | @{syntax parname}) +)
- "}
-
- \begin{description}
-
- \item @{command "theory"}~@{text "A \<IMPORTS> B\<^sub>1 \<dots> B\<^sub>n \<BEGIN>"}
- starts a new theory @{text A} based on the merge of existing
- theories @{text "B\<^sub>1 \<dots> B\<^sub>n"}. Due to the possibility to import 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.
-
- The optional @{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 "\"typedef\""}
- @{text ":: thy_goal"} or @{keyword "keywords"}~@{verbatim
- "\"datatype\""} @{text ":: thy_decl"} for theory-level declarations
- with and without proof, respectively. Additional @{syntax tags}
- provide defaults for document preparation (\secref{sec:tags}).
-
- The optional @{keyword_def "uses"} specification declares additional
- dependencies on external files (notably ML sources). Files will be
- loaded immediately (as ML), unless the name is parenthesized. The
- latter case records a dependency that needs to be resolved later in
- the text, usually via explicit @{command_ref "use"} for ML files;
- other file formats require specific load commands defined by the
- corresponding tools or packages.
-
- \item @{command (global) "end"} concludes the current theory
- definition. Note that some other commands, e.g.\ local theory
- targets @{command locale} or @{command class} may involve a
- @{keyword "begin"} that needs to be matched by @{command (local)
- "end"}, according to the usual rules for nested blocks.
-
- \end{description}
-*}
-
-
-section {* Local theory targets \label{sec:target} *}
-
-text {*
- \begin{matharray}{rcll}
- @{command_def "context"} & : & @{text "theory \<rightarrow> local_theory"} \\
- @{command_def (local) "end"} & : & @{text "local_theory \<rightarrow> theory"} \\
- \end{matharray}
-
- A local theory target is a context 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{Named contexts} refer to locales (cf.\ \secref{sec:locale}) or
- type classes (cf.\ \secref{sec:class}); the name ``@{text "-"}''
- signifies the global theory context.
-
- \emph{Unnamed contexts} may introduce additional parameters and
- assumptions, and results produced in the context are generalized
- accordingly. Such auxiliary contexts may be nested within other
- targets, like @{command "locale"}, @{command "class"}, @{command
- "instantiation"}, @{command "overloading"}.
-
- @{rail "
- @@{command context} @{syntax nameref} @'begin'
- ;
- @@{command context} @{syntax_ref \"includes\"}? (@{syntax context_elem} * ) @'begin'
- ;
- @{syntax_def target}: '(' @'in' @{syntax nameref} ')'
- "}
-
- \begin{description}
-
- \item @{command "context"}~@{text "c \<BEGIN>"} opens a named
- context, by recommencing an existing locale or class @{text c}.
- Note that locale and class definitions allow to include the
- @{keyword "begin"} keyword as well, in order to continue the local
- theory immediately after the initial specification.
-
- \item @{command "context"}~@{text "bundles elements \<BEGIN>"} opens
- an unnamed context, by extending the enclosing global or local
- theory target by the given declaration bundles (\secref{sec:bundle})
- and context elements (@{text "\<FIXES>"}, @{text "\<ASSUMES>"}
- etc.). This 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.
-
- \item @{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}).
-
- \item @{text "("}@{keyword_def "in"}~@{text "c)"} given after any
- local theory command specifies an immediate target, e.g.\
- ``@{command "definition"}~@{text "(\<IN> c) \<dots>"}'' or ``@{command
- "theorem"}~@{text "(\<IN> c) \<dots>"}''. This works both in a local or
- global theory context; the current target context will be suspended
- for this command only. Note that ``@{text "(\<IN> -)"}'' will
- always produce a global result independently of the current target
- context.
-
- \end{description}
-
- 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
- @{text c} with parameter @{text x} and assumption @{text "A[x]"}.
-
- 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,
- @{text "a \<equiv> t[x]"} becomes @{text "c.a ?x \<equiv> t[?x]"} at the theory
- level (for arbitrary @{text "?x"}), together with a local
- abbreviation @{text "c \<equiv> c.a x"} in the target context (for the
- fixed parameter @{text x}).
-
- Theorems are exported by discharging the assumptions and
- generalizing the parameters of the context. For example, @{text "a:
- B[x]"} becomes @{text "c.a: A[?x] \<Longrightarrow> B[?x]"}, again for arbitrary
- @{text "?x"}.
-
- \medskip The Isabelle/HOL library contains numerous applications of
- locales and classes, e.g.\ see @{file "~~/src/HOL/Algebra"}. An
- example for an unnamed auxiliary contexts is given in @{file
- "~~/src/HOL/Isar_Examples/Group_Context.thy"}. *}
-
-
-section {* Bundled declarations \label{sec:bundle} *}
-
-text {*
- \begin{matharray}{rcl}
- @{command_def "bundle"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
- @{command_def "print_bundles"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow> "} \\
- @{command_def "include"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
- @{command_def "including"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\
- @{keyword_def "includes"} & : & 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 @{text "this_rule [intro] that_rule [elim]"} for example.
- Configuration options (\secref{sec:config}) are special declaration
- attributes that operate on the context without a theorem, as in
- @{text "[[show_types = false]]"} for example.
-
- Expressions of this form may be defined as \emph{bundled
- declarations} 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 "
- @@{command bundle} @{syntax target}? \\
- @{syntax name} '=' @{syntax thmrefs} (@'for' (@{syntax vars} + @'and'))?
- ;
- (@@{command include} | @@{command including}) (@{syntax nameref}+)
- ;
- @{syntax_def \"includes\"}: @'includes' (@{syntax nameref}+)
- "}
-
- \begin{description}
-
- \item @{command bundle}~@{text "b = decls"} defines a bundle of
- declarations in the current context. The RHS is similar to the one
- of the @{command declare} command. Bundles 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.
-
- \item @{command print_bundles} prints the named bundles that are
- available in the current context.
-
- \item @{command include}~@{text "b\<^sub>1 \<dots> b\<^sub>n"} includes the declarations
- from the given bundles into the current proof body context. This is
- analogous to @{command "note"} (\secref{sec:proof-facts}) with the
- expanded bundles.
-
- \item @{command including} is similar to @{command include}, but
- works in proof refinement (backward mode). This is analogous to
- @{command "using"} (\secref{sec:proof-facts}) with the expanded
- bundles.
-
- \item @{keyword "includes"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"} is similar to
- @{command include}, but works in situations where a specification
- context is constructed, notably for @{command context} and long
- statements of @{command theorem} etc.
-
- \end{description}
-
- Here is an artificial example of bundling various configuration
- options: *}
-
-bundle trace = [[simp_trace, blast_trace, linarith_trace, metis_trace, smt_trace]]
-
-lemma "x = x"
- including trace by metis
-
-
-section {* Basic specification elements *}
-
-text {*
- \begin{matharray}{rcll}
- @{command_def "axiomatization"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
- @{command_def "definition"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
- @{attribute_def "defn"} & : & @{text attribute} \\
- @{command_def "abbreviation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
- @{command_def "print_abbrevs"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow> "} \\
- \end{matharray}
-
- These specification mechanisms provide a slightly more abstract view
- than the underlying primitives of @{command "consts"}, @{command
- "defs"} (see \secref{sec:consts}), and @{command "axioms"} (see
- \secref{sec:axms-thms}). In particular, type-inference is commonly
- available, and result names need not be given.
-
- @{rail "
- @@{command axiomatization} @{syntax \"fixes\"}? (@'where' specs)?
- ;
- @@{command definition} @{syntax target}? \\
- (decl @'where')? @{syntax thmdecl}? @{syntax prop}
- ;
- @@{command abbreviation} @{syntax target}? @{syntax mode}? \\
- (decl @'where')? @{syntax prop}
- ;
-
- @{syntax_def \"fixes\"}: ((@{syntax name} ('::' @{syntax type})?
- @{syntax mixfix}? | @{syntax vars}) + @'and')
- ;
- specs: (@{syntax thmdecl}? @{syntax props} + @'and')
- ;
- decl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}?
- "}
-
- \begin{description}
-
- \item @{command "axiomatization"}~@{text "c\<^sub>1 \<dots> c\<^sub>m \<WHERE> \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"}
- introduces several constants simultaneously and states axiomatic
- properties for these. The constants are marked as being specified
- once and for all, which prevents additional specifications being
- issued later on.
-
- Note that axiomatic specifications are only appropriate when
- declaring a new logical system; axiomatic specifications are
- restricted to global theory contexts. Normal applications should
- only use definitional mechanisms!
-
- \item @{command "definition"}~@{text "c \<WHERE> eq"} produces an
- internal definition @{text "c \<equiv> t"} according to the specification
- given as @{text eq}, 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 @{text "x =
- y"} and equivalence @{text "A \<leftrightarrow> B"}. End-users normally need not
- change the @{attribute defn} setup.
-
- Definitions may be presented with explicit arguments on the LHS, as
- well as additional conditions, e.g.\ @{text "f x y = t"} instead of
- @{text "f \<equiv> \<lambda>x y. t"} and @{text "y \<noteq> 0 \<Longrightarrow> g x y = u"} instead of an
- unrestricted @{text "g \<equiv> \<lambda>x y. u"}.
-
- \item @{command "abbreviation"}~@{text "c \<WHERE> eq"} introduces a
- syntactic constant which is associated with a certain term according
- to the meta-level equality @{text eq}.
-
- 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 @{text mode} specification restricts output to a
- particular print mode; using ``@{text input}'' here achieves the
- effect of one-way abbreviations. The mode may also include an
- ``@{keyword "output"}'' qualifier that affects the concrete syntax
- declared for abbreviations, cf.\ @{command "syntax"} in
- \secref{sec:syn-trans}.
-
- \item @{command "print_abbrevs"} prints all constant abbreviations
- of the current context.
-
- \end{description}
-*}
-
-
-section {* Generic declarations *}
-
-text {*
- \begin{matharray}{rcl}
- @{command_def "declaration"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
- @{command_def "syntax_declaration"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
- @{command_def "declare"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
- \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 "
- (@@{command declaration} | @@{command syntax_declaration})
- ('(' @'pervasive' ')')? \\ @{syntax target}? @{syntax text}
- ;
- @@{command declare} @{syntax target}? (@{syntax thmrefs} + @'and')
- "}
-
- \begin{description}
-
- \item @{command "declaration"}~@{text d} adds the declaration
- function @{text d} of ML type @{ML_type declaration}, to the current
- local theory under construction. In later application contexts, the
- function is transformed according to the morphisms being involved in
- the interpretation hierarchy.
-
- If the @{text "(pervasive)"} option is given, the corresponding
- declaration is applied to all possible contexts involved, including
- the global background theory.
-
- \item @{command "syntax_declaration"} is similar to @{command
- "declaration"}, but is meant to affect only ``syntactic'' tools by
- convention (such as notation and type-checking information).
-
- \item @{command "declare"}~@{text thms} declares theorems to the
- current local theory context. No theorem binding is involved here,
- unlike @{command "theorems"} or @{command "lemmas"} (cf.\
- \secref{sec:axms-thms}), so @{command "declare"} only has the effect
- of applying attributes as included in the theorem specification.
-
- \end{description}
-*}
-
-
-section {* Locales \label{sec:locale} *}
-
-text {*
- Locales are parametric named local contexts, consisting of a list of
- declaration elements that are modeled after the Isar proof context
- commands (cf.\ \secref{sec:proof-context}).
-*}
-
-
-subsection {* Locale expressions \label{sec:locale-expr} *}
-
-text {*
- A \emph{locale expression} denotes a structured context composed of
- instances of existing locales. The context consists of a list of
- instances of declaration elements from the locales. Two locale
- instances are equal if they are of the same locale and the
- parameters are instantiated with equivalent terms. Declaration
- elements from equal instances are never repeated, thus avoiding
- duplicate declarations. More precisely, declarations from instances
- that are subsumed by earlier instances are omitted.
-
- @{rail "
- @{syntax_def locale_expr}: (instance + '+') (@'for' (@{syntax \"fixes\"} + @'and'))?
- ;
- instance: (qualifier ':')? @{syntax nameref} (pos_insts | named_insts)
- ;
- qualifier: @{syntax name} ('?' | '!')?
- ;
- pos_insts: ('_' | @{syntax term})*
- ;
- named_insts: @'where' (@{syntax name} '=' @{syntax term} + @'and')
- "}
-
- A locale instance consists of a reference to a locale and either
- positional or named parameter instantiations. Identical
- instantiations (that is, those that instante a parameter by itself)
- may be omitted. The notation `@{text "_"}' 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 @{keyword "for"} clause. This is useful for shadowing names
- bound in outer contexts, 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 optional
- (``\texttt{?}''), which means that it may be omitted on input of the
- qualified name, or mandatory (``\texttt{!}''). If neither
- ``\texttt{?}'' nor ``\texttt{!}'' are present, the command's default
- is used. For @{command "interpretation"} and @{command "interpret"}
- the default is ``mandatory'', for @{command "locale"} and @{command
- "sublocale"} the default is ``optional''.
-*}
-
-
-subsection {* Locale declarations *}
-
-text {*
- \begin{matharray}{rcl}
- @{command_def "locale"} & : & @{text "theory \<rightarrow> local_theory"} \\
- @{command_def "print_locale"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
- @{command_def "print_locales"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
- @{method_def intro_locales} & : & @{text method} \\
- @{method_def unfold_locales} & : & @{text method} \\
- \end{matharray}
-
- \indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes}
- \indexisarelem{defines}\indexisarelem{notes}
- @{rail "
- @@{command locale} @{syntax name} ('=' @{syntax locale})? @'begin'?
- ;
- @@{command print_locale} '!'? @{syntax nameref}
- ;
- @{syntax_def locale}: @{syntax context_elem}+ |
- @{syntax locale_expr} ('+' (@{syntax context_elem}+))?
- ;
- @{syntax_def context_elem}:
- @'fixes' (@{syntax \"fixes\"} + @'and') |
- @'constrains' (@{syntax name} '::' @{syntax type} + @'and') |
- @'assumes' (@{syntax props} + @'and') |
- @'defines' (@{syntax thmdecl}? @{syntax prop} @{syntax prop_pat}? + @'and') |
- @'notes' (@{syntax thmdef}? @{syntax thmrefs} + @'and')
- "}
-
- \begin{description}
-
- \item @{command "locale"}~@{text "loc = import + body"} defines a
- new locale @{text loc} as a context consisting of a certain view of
- existing locales (@{text import}) plus some additional elements
- (@{text body}). Both @{text import} and @{text body} are optional;
- the degenerate form @{command "locale"}~@{text loc} defines an empty
- locale, which may still be 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 @{text import} consists of a structured locale expression; see
- \secref{sec:proof-context} above. Its for clause defines the local
- parameters of the @{text import}. In addition, locale parameters
- whose instantance is omitted automatically extend the (possibly
- empty) for clause: they are 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.
-
- The @{text body} consists of context elements.
-
- \begin{description}
-
- \item @{element "fixes"}~@{text "x :: \<tau> (mx)"} declares a local
- parameter of type @{text \<tau>} and mixfix annotation @{text mx} (both
- are optional). The special syntax declaration ``@{text
- "(\<STRUCTURE>)"}'' means that @{text x} may be referenced
- implicitly in this context.
-
- \item @{element "constrains"}~@{text "x :: \<tau>"} introduces a type
- constraint @{text \<tau>} on the local parameter @{text x}. This
- element is deprecated. The type constraint should be introduced in
- the for clause or the relevant @{element "fixes"} element.
-
- \item @{element "assumes"}~@{text "a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"}
- introduces local premises, similar to @{command "assume"} within a
- proof (cf.\ \secref{sec:proof-context}).
-
- \item @{element "defines"}~@{text "a: x \<equiv> t"} defines a previously
- declared parameter. This is similar to @{command "def"} within a
- proof (cf.\ \secref{sec:proof-context}), but @{element "defines"}
- takes an equational proposition instead of variable-term pair. The
- left-hand side of the equation may have additional arguments, e.g.\
- ``@{element "defines"}~@{text "f x\<^sub>1 \<dots> x\<^sub>n \<equiv> t"}''.
-
- \item @{element "notes"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"}
- reconsiders facts within a local context. Most notably, this may
- include arbitrary declarations in any attribute specifications
- included here, e.g.\ a local @{attribute simp} rule.
-
- The initial @{text import} specification of a locale expression
- maintains a dynamic relation to the locales being referenced
- (benefiting from any later fact declarations in the obvious manner).
-
- \end{description}
-
- Note that ``@{text "(\<IS> p\<^sub>1 \<dots> p\<^sub>n)"}'' patterns given
- in the syntax of @{element "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 @{text
- loc_axioms} 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 @{text loc} 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 note that
- 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 @{text \<And>} by @{text \<forall>}, and
- @{text "\<Longrightarrow>"} by @{text "\<longrightarrow>"} in HOL; see also
- \secref{sec:object-logic}). Separate introduction rules @{text
- loc_axioms.intro} and @{text loc.intro} are provided as well.
-
- \item @{command "print_locale"}~@{text "locale"} prints the
- contents of the named locale. The command omits @{element "notes"}
- elements by default. Use @{command "print_locale"}@{text "!"} to
- have them included.
-
- \item @{command "print_locales"} prints the names of all locales
- of the current theory.
-
- \item @{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 @{text
- loc.intro} introduction rules and therefore does not decend to
- assumptions, @{method unfold_locales} is more aggressive and applies
- @{text loc_axioms.intro} 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.
-
- \end{description}
-*}
-
-
-subsection {* Locale interpretation *}
-
-text {*
- \begin{matharray}{rcl}
- @{command_def "interpretation"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
- @{command_def "interpret"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
- @{command_def "sublocale"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
- @{command_def "print_dependencies"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
- @{command_def "print_interps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
- \end{matharray}
-
- Locale expressions may be instantiated, and the instantiated facts
- added to the current context. This requires a proof of the
- instantiated specification and is called \emph{locale
- interpretation}. Interpretation is possible in locales (command
- @{command "sublocale"}), theories (command @{command
- "interpretation"}) and also within proof bodies (command @{command
- "interpret"}).
-
- @{rail "
- @@{command interpretation} @{syntax locale_expr} equations?
- ;
- @@{command interpret} @{syntax locale_expr} equations?
- ;
- @@{command sublocale} @{syntax nameref} ('<' | '\<subseteq>') @{syntax locale_expr} \\
- equations?
- ;
- @@{command print_dependencies} '!'? @{syntax locale_expr}
- ;
- @@{command print_interps} @{syntax nameref}
- ;
-
- equations: @'where' (@{syntax thmdecl}? @{syntax prop} + @'and')
- "}
-
- \begin{description}
-
- \item @{command "interpretation"}~@{text "expr \<WHERE> eqns"}
- interprets @{text expr} in the theory. The command generates proof
- obligations for the instantiated specifications (assumes and defines
- elements). Once these are discharged by the user, instantiated
- facts are added to the theory in a post-processing phase.
-
- 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 ---
- it may be added to the @{keyword "for"} clause.
-
- Additional equations, which are unfolded during
- post-processing, may be given after the keyword @{keyword "where"}.
- This is useful for interpreting concepts introduced through
- definitions. The equations must be proved.
-
- The command is aware of interpretations already active in the
- theory, but does not simplify the goal automatically. In order to
- simplify the proof obligations use methods @{method intro_locales}
- or @{method unfold_locales}. Post-processing is not applied to
- facts of interpretations that are already active. This avoids
- duplication of interpreted facts, in particular. Note that, in the
- case of a locale with import, parts of the interpretation may
- already be active. The command will only process facts for new
- parts.
-
- Adding facts to locales has the effect of adding interpreted facts
- to the theory for all interpretations as well. That is,
- interpretations dynamically participate in any facts added to
- locales. Note that if a theory inherits additional facts for a
- locale through one parent and an interpretation of that locale
- through another parent, the additional facts will not be
- interpreted.
-
- \item @{command "interpret"}~@{text "expr \<WHERE> eqns"} interprets
- @{text expr} in the proof context and is otherwise similar to
- interpretation in theories. Note that rewrite rules given to
- @{command "interpret"} after the @{keyword "where"} keyword should be
- explicitly universally quantified.
-
- \item @{command "sublocale"}~@{text "name \<subseteq> expr \<WHERE>
- eqns"}
- interprets @{text expr} in the locale @{text name}. A proof that
- the specification of @{text name} implies the specification of
- @{text expr} is required. As in the localized version of the
- theorem command, the proof is in the context of @{text name}. After
- the proof obligation has been discharged, the facts of @{text expr}
- become part of locale @{text name} as \emph{derived} context
- elements and are available when the context @{text name} is
- subsequently entered. Note that, like import, this is dynamic:
- facts added to a locale part of @{text expr} after interpretation
- become also available in @{text name}.
-
- Only specification fragments of @{text expr} that are not already
- part of @{text name} (be it imported, derived or a derived fragment
- of the import) are considered in this process. This enables
- circular interpretations provided that no infinite chains are
- generated in the locale hierarchy.
-
- If interpretations of @{text name} exist in the current theory, the
- command adds interpretations for @{text expr} as well, with the same
- qualifier, although only for fragments of @{text expr} that are not
- interpreted in the theory already.
-
- Equations given after @{keyword "where"} amend the morphism through
- which @{text expr} is interpreted. This enables to map definitions
- from the interpreted locales to entities of @{text name}. This
- feature is experimental.
-
- \item @{command "print_dependencies"}~@{text "expr"} is useful for
- understanding the effect of an interpretation of @{text "expr"}. It
- lists all locale instances for which interpretations would be added
- to the current context. Variant @{command
- "print_dependencies"}@{text "!"} prints all locale instances that
- would be considered for interpretation, and would be interpreted in
- an empty context (that is, without interpretations).
-
- \item @{command "print_interps"}~@{text "locale"} lists all
- interpretations of @{text "locale"} in the current theory or proof
- context, including those due to a combination of a @{command
- "interpretation"} or @{command "interpret"} and one or several
- @{command "sublocale"} declarations.
-
- \end{description}
-
- \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 behavior of such
- tools is \emph{not} 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 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}
-*}
-
-
-section {* Classes \label{sec:class} *}
-
-text {*
- \begin{matharray}{rcl}
- @{command_def "class"} & : & @{text "theory \<rightarrow> local_theory"} \\
- @{command_def "instantiation"} & : & @{text "theory \<rightarrow> local_theory"} \\
- @{command_def "instance"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
- @{command "instance"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
- @{command_def "subclass"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
- @{command_def "print_classes"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
- @{command_def "class_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
- @{method_def intro_classes} & : & @{text method} \\
- \end{matharray}
-
- A class is a particular locale with \emph{exactly one} type variable
- @{text \<alpha>}. Beyond the underlying locale, a corresponding type class
- is established which is interpreted logically as axiomatic type
- class \cite{Wenzel:1997:TPHOL} 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{isabelle-classes} for a short
- tutorial.
-
- @{rail "
- @@{command class} class_spec @'begin'?
- ;
- class_spec: @{syntax name} '='
- ((@{syntax nameref} '+' (@{syntax context_elem}+)) |
- @{syntax nameref} | (@{syntax context_elem}+))
- ;
- @@{command instantiation} (@{syntax nameref} + @'and') '::' @{syntax arity} @'begin'
- ;
- @@{command instance} (() | (@{syntax nameref} + @'and') '::' @{syntax arity} |
- @{syntax nameref} ('<' | '\<subseteq>') @{syntax nameref} )
- ;
- @@{command subclass} @{syntax target}? @{syntax nameref}
- "}
-
- \begin{description}
-
- \item @{command "class"}~@{text "c = superclasses + body"} defines
- a new class @{text c}, inheriting from @{text superclasses}. This
- introduces a locale @{text c} with import of all locales @{text
- superclasses}.
-
- Any @{element "fixes"} in @{text body} are lifted to the global
- theory level (\emph{class operations} @{text "f\<^sub>1, \<dots>,
- f\<^sub>n"} of class @{text c}), mapping the local type parameter
- @{text \<alpha>} to a schematic type variable @{text "?\<alpha> :: c"}.
-
- Likewise, @{element "assumes"} in @{text body} are also lifted,
- mapping each local parameter @{text "f :: \<tau>[\<alpha>]"} to its
- corresponding global constant @{text "f :: \<tau>[?\<alpha> :: c]"}. The
- corresponding introduction rule is provided as @{text
- c_class_axioms.intro}. This rule should be rarely needed directly
- --- the @{method intro_classes} method takes care of the details of
- class membership proofs.
-
- \item @{command "instantiation"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n)s
- \<BEGIN>"} opens a theory target (cf.\ \secref{sec:target}) which
- allows to specify class operations @{text "f\<^sub>1, \<dots>, f\<^sub>n"} corresponding
- to sort @{text s} at the particular type instance @{text "(\<alpha>\<^sub>1 :: s\<^sub>1,
- \<dots>, \<alpha>\<^sub>n :: s\<^sub>n) t"}. A plain @{command "instance"} command in the
- target body poses a goal 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.
-
- \item @{command "instance"} in an instantiation target body sets
- up a goal stating the type arities claimed at the opening @{command
- "instantiation"}. The proof would 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, @{command "instance"}~@{text "t :: (s\<^sub>1, \<dots>,
- s\<^sub>n)s"} provides a convenient way to instantiate a type class with no
- need to specify operations: one can continue with the
- instantiation proof immediately.
-
- \item @{command "subclass"}~@{text c} in a class context for class
- @{text d} sets up a goal stating that class @{text c} is logically
- contained in class @{text d}. After finishing the proof, class
- @{text d} is proven to be subclass @{text c} and the locale @{text
- c} is interpreted into @{text d} simultaneously.
-
- A weakend form of this is available through a further variant of
- @{command instance}: @{command instance}~@{text "c\<^sub>1 \<subseteq> c\<^sub>2"} opens
- a proof that class @{text "c\<^isub>2"} implies @{text "c\<^isub>1"} without reference
- to the underlying locales; this is useful if the properties to prove
- the logical connection are not sufficent on the locale level but on
- the theory level.
-
- \item @{command "print_classes"} prints all classes in the current
- theory.
-
- \item @{command "class_deps"} visualizes all classes and their
- subclass relations as a Hasse diagram.
-
- \item @{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 @{command "proof"}). In particular,
- instantiation of trivial (syntactic) classes may be performed by a
- single ``@{command ".."}'' proof step.
-
- \end{description}
-*}
-
-
-subsection {* The class target *}
-
-text {*
- %FIXME check
-
- A named context may refer to a locale (cf.\ \secref{sec:target}).
- If this locale is also a class @{text c}, apart from the common
- locale target behaviour the following happens.
-
- \begin{itemize}
-
- \item Local constant declarations @{text "g[\<alpha>]"} referring to the
- local type parameter @{text \<alpha>} and local parameters @{text "f[\<alpha>]"}
- are accompanied by theory-level constants @{text "g[?\<alpha> :: c]"}
- referring to theory-level class operations @{text "f[?\<alpha> :: c]"}.
-
- \item Local theorem bindings are lifted as are assumptions.
-
- \item Local syntax refers to local operations @{text "g[\<alpha>]"} and
- global operations @{text "g[?\<alpha> :: c]"} uniformly. Type inference
- resolves ambiguities. In rare cases, manual type annotations are
- needed.
-
- \end{itemize}
-*}
-
-
-subsection {* Co-regularity of type classes and arities *}
-
-text {* The class relation together with the collection of
- type-constructor arities must obey the principle of
- \emph{co-regularity} 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 @{text "t :: (\<^vec>s)c"} is
- completed such that @{text "t :: (\<^vec>s)c"} and @{text "c \<subseteq> c'"}
- implies @{text "t :: (\<^vec>s)c'"} for all such declarations.
-
- Treating sorts as finite sets of classes (meaning the intersection),
- the class relation @{text "c\<^sub>1 \<subseteq> c\<^sub>2"} is extended to sorts as
- follows:
- \[
- @{text "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"}
- \]
-
- This relation on sorts is further extended to tuples of sorts (of
- the same length) in the component-wise way.
-
- \smallskip Co-regularity of the class relation together with the
- arities relation means:
- \[
- @{text "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"}
- \]
- \noindent 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 principle
- types and most general unifiers, e.g.\ see \cite{nipkow-prehofer}.
-*}
-
-
-section {* Unrestricted overloading *}
-
-text {*
- \begin{matharray}{rcl}
- @{command_def "overloading"} & : & @{text "theory \<rightarrow> local_theory"} \\
- \end{matharray}
-
- Isabelle/Pure's definitional schemes support certain forms of
- overloading (see \secref{sec:consts}). Overloading means that a
- constant being declared as @{text "c :: \<alpha> decl"} may be
- defined separately on type instances
- @{text "c :: (\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n) t decl"}
- for each type constructor @{text t}. At most occassions
- overloading will be used in a Haskell-like fashion together with
- type classes by means of @{command "instantiation"} (see
- \secref{sec:class}). Sometimes low-level overloading is desirable.
- The @{command "overloading"} target provides a convenient view for
- end-users.
-
- @{rail "
- @@{command overloading} ( spec + ) @'begin'
- ;
- spec: @{syntax name} ( '==' | '\<equiv>' ) @{syntax term} ( '(' @'unchecked' ')' )?
- "}
-
- \begin{description}
-
- \item @{command "overloading"}~@{text "x\<^sub>1 \<equiv> c\<^sub>1 :: \<tau>\<^sub>1 \<AND> \<dots> x\<^sub>n \<equiv> c\<^sub>n :: \<tau>\<^sub>n \<BEGIN>"}
- opens a theory target (cf.\ \secref{sec:target}) which allows to
- specify constants with overloaded definitions. These are identified
- by an explicitly given mapping from variable names @{text "x\<^sub>i"} to
- constants @{text "c\<^sub>i"} at particular type instances. The
- definitions themselves are established using common specification
- tools, using the names @{text "x\<^sub>i"} as reference to the
- corresponding constants. The target is concluded by @{command
- (local) "end"}.
-
- A @{text "(unchecked)"} option disables global dependency checks for
- the corresponding definition, which is occasionally useful for
- exotic overloading (see \secref{sec:consts} for a precise description).
- It is at the discretion of the user to avoid
- malformed theory specifications!
-
- \end{description}
-*}
-
-
-section {* Incorporating ML code \label{sec:ML} *}
-
-text {*
- \begin{matharray}{rcl}
- @{command_def "ML_file"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
- @{command_def "ML"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
- @{command_def "ML_prf"} & : & @{text "proof \<rightarrow> proof"} \\
- @{command_def "ML_val"} & : & @{text "any \<rightarrow>"} \\
- @{command_def "ML_command"} & : & @{text "any \<rightarrow>"} \\
- @{command_def "setup"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def "local_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
- @{command_def "attribute_setup"} & : & @{text "theory \<rightarrow> theory"} \\
- \end{matharray}
-
- @{rail "
- @@{command ML_file} @{syntax name}
- ;
- (@@{command ML} | @@{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}?
- "}
-
- \begin{description}
-
- \item @{command "ML_file"}~@{text "name"} reads and evaluates the
- given ML file. The current theory context is passed down to the ML
- toplevel and may be modified, using @{ML "Context.>>"} or derived ML
- commands. Top-level ML bindings are stored within the (global or
- local) theory context.
-
- \item @{command "ML"}~@{text "text"} is similar to @{command
- "ML_file"}, but evaluates directly the given @{text "text"}.
- Top-level ML bindings are stored within the (global or local) theory
- context.
-
- \item @{command "ML_prf"} is analogous to @{command "ML"} but works
- within a proof context. Top-level ML bindings are stored within the
- proof context in a purely sequential fashion, disregarding the
- nested proof structure. ML bindings introduced by @{command
- "ML_prf"} are discarded at the end of the proof.
-
- \item @{command "ML_val"} and @{command "ML_command"} are diagnostic
- versions of @{command "ML"}, which means that the context may not be
- updated. @{command "ML_val"} echos the bindings produced at the ML
- toplevel, but @{command "ML_command"} is silent.
-
- \item @{command "setup"}~@{text "text"} changes the current theory
- context by applying @{text "text"}, which refers to an ML expression
- of type @{ML_type "theory -> theory"}. This enables to initialize
- any object-logic specific tools and packages written in ML, for
- example.
-
- \item @{command "local_setup"} is similar to @{command "setup"} for
- a local theory context, and an ML expression of type @{ML_type
- "local_theory -> local_theory"}. This allows to
- invoke local theory specification packages without going through
- concrete outer syntax, for example.
-
- \item @{command "attribute_setup"}~@{text "name = text description"}
- defines an attribute in the current theory. The given @{text
- "text"} has to be an ML expression of type
- @{ML_type "attribute context_parser"}, cf.\ basic parsers defined in
- structure @{ML_struct Args} and @{ML_struct Attrib}.
-
- In principle, attributes can operate both on a given theorem and the
- implicit context, although in practice only one is modified and the
- other serves as parameter. Here are examples for these two cases:
-
- \end{description}
-*}
-
- attribute_setup my_rule = {*
- Attrib.thms >> (fn ths =>
- Thm.rule_attribute
- (fn context: Context.generic => fn th: thm =>
- let val th' = th OF ths
- in th' end)) *}
-
- attribute_setup my_declaration = {*
- Attrib.thms >> (fn ths =>
- Thm.declaration_attribute
- (fn th: thm => fn context: Context.generic =>
- let val context' = context
- in context' end)) *}
-
-
-section {* Primitive specification elements *}
-
-subsection {* Type classes and sorts \label{sec:classes} *}
-
-text {*
- \begin{matharray}{rcll}
- @{command_def "classes"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def "classrel"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
- @{command_def "default_sort"} & : & @{text "local_theory \<rightarrow> local_theory"}
- \end{matharray}
-
- @{rail "
- @@{command classes} (@{syntax classdecl} +)
- ;
- @@{command classrel} (@{syntax nameref} ('<' | '\<subseteq>') @{syntax nameref} + @'and')
- ;
- @@{command default_sort} @{syntax sort}
- "}
-
- \begin{description}
-
- \item @{command "classes"}~@{text "c \<subseteq> c\<^sub>1, \<dots>, c\<^sub>n"} declares class
- @{text c} to be a subclass of existing classes @{text "c\<^sub>1, \<dots>, c\<^sub>n"}.
- Isabelle implicitly maintains the transitive closure of the class
- hierarchy. Cyclic class structures are not permitted.
-
- \item @{command "classrel"}~@{text "c\<^sub>1 \<subseteq> c\<^sub>2"} states subclass
- relations between existing classes @{text "c\<^sub>1"} and @{text "c\<^sub>2"}.
- This is done axiomatically! The @{command_ref "subclass"} and
- @{command_ref "instance"} commands (see \secref{sec:class}) provide
- a way to introduce proven class relations.
-
- \item @{command "default_sort"}~@{text s} makes sort @{text s} the
- new default sort for any type variable that is given explicitly in
- the text, but lacks a sort constraint (wrt.\ the current context).
- Type variables generated by type inference are not affected.
-
- Usually the default sort is only changed when defining a new
- object-logic. For example, the default sort in Isabelle/HOL is
- @{class type}, the class of all HOL types.
-
- When merging theories, the default sorts of the parents are
- logically intersected, i.e.\ the representations as lists of classes
- are joined.
-
- \end{description}
-*}
-
-
-subsection {* Types and type abbreviations \label{sec:types-pure} *}
-
-text {*
- \begin{matharray}{rcll}
- @{command_def "type_synonym"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
- @{command_def "typedecl"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
- @{command_def "arities"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
- \end{matharray}
-
- @{rail "
- @@{command type_synonym} (@{syntax typespec} '=' @{syntax type} @{syntax mixfix}?)
- ;
- @@{command typedecl} @{syntax typespec} @{syntax mixfix}?
- ;
- @@{command arities} (@{syntax nameref} '::' @{syntax arity} +)
- "}
-
- \begin{description}
-
- \item @{command "type_synonym"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = \<tau>"}
- introduces a \emph{type synonym} @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} for the
- existing type @{text "\<tau>"}. Unlike actual type definitions, as are
- available in Isabelle/HOL for example, type synonyms are merely
- syntactic abbreviations without any logical significance.
- Internally, type synonyms are fully expanded.
-
- \item @{command "typedecl"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} declares a new
- type constructor @{text t}. If the object-logic defines a base sort
- @{text s}, then the constructor is declared to operate on that, via
- the axiomatic specification @{command arities}~@{text "t :: (s, \<dots>,
- s)s"}.
-
- \item @{command "arities"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n)s"} augments
- Isabelle's order-sorted signature of types by new type constructor
- arities. This is done axiomatically! The @{command_ref "instantiation"}
- target (see \secref{sec:class}) provides a way to introduce
- proven type arities.
-
- \end{description}
-*}
-
-
-subsection {* Constants and definitions \label{sec:consts} *}
-
-text {*
- \begin{matharray}{rcl}
- @{command_def "consts"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def "defs"} & : & @{text "theory \<rightarrow> theory"} \\
- \end{matharray}
-
- Definitions essentially express abbreviations within the logic. The
- simplest form of a definition is @{text "c :: \<sigma> \<equiv> t"}, where @{text
- c} is a newly declared constant. Isabelle also allows derived forms
- where the arguments of @{text c} appear on the left, abbreviating a
- prefix of @{text \<lambda>}-abstractions, e.g.\ @{text "c \<equiv> \<lambda>x y. t"} may be
- written more conveniently as @{text "c x y \<equiv> t"}. Moreover,
- definitions may be weakened by adding arbitrary pre-conditions:
- @{text "A \<Longrightarrow> c x y \<equiv> t"}.
-
- \medskip The built-in well-formedness conditions for definitional
- specifications are:
-
- \begin{itemize}
-
- \item Arguments (on the left-hand side) must be distinct variables.
-
- \item All variables on the right-hand side must also appear on the
- left-hand side.
-
- \item All type variables on the right-hand side must also appear on
- the left-hand side; this prohibits @{text "0 :: nat \<equiv> length ([] ::
- \<alpha> list)"} for example.
-
- \item The definition must not be recursive. Most object-logics
- provide definitional principles that can be used to express
- recursion safely.
-
- \end{itemize}
-
- The right-hand side of overloaded definitions may mention overloaded constants
- recursively at type instances corresponding to the immediate
- argument types @{text "\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n"}. Incomplete
- specification patterns impose global constraints on all occurrences,
- e.g.\ @{text "d :: \<alpha> \<times> \<alpha>"} on the left-hand side means that all
- corresponding occurrences on some right-hand side need to be an
- instance of this, general @{text "d :: \<alpha> \<times> \<beta>"} will be disallowed.
-
- @{rail "
- @@{command consts} ((@{syntax name} '::' @{syntax type} @{syntax mixfix}?) +)
- ;
- @@{command defs} opt? (@{syntax axmdecl} @{syntax prop} +)
- ;
- opt: '(' @'unchecked'? @'overloaded'? ')'
- "}
-
- \begin{description}
-
- \item @{command "consts"}~@{text "c :: \<sigma>"} declares constant @{text
- c} to have any instance of type scheme @{text \<sigma>}. The optional
- mixfix annotations may attach concrete syntax to the constants
- declared.
-
- \item @{command "defs"}~@{text "name: eqn"} introduces @{text eqn}
- as a definitional axiom for some existing constant.
-
- The @{text "(unchecked)"} option disables global dependency checks
- for this definition, which is occasionally useful for exotic
- overloading. It is at the discretion of the user to avoid malformed
- theory specifications!
-
- The @{text "(overloaded)"} option declares definitions to be
- potentially overloaded. Unless this option is given, a warning
- message would be issued for any definitional equation with a more
- special type than that of the corresponding constant declaration.
-
- \end{description}
-*}
-
-
-section {* Axioms and theorems \label{sec:axms-thms} *}
-
-text {*
- \begin{matharray}{rcll}
- @{command_def "axioms"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
- @{command_def "lemmas"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
- @{command_def "theorems"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
- \end{matharray}
-
- @{rail "
- @@{command axioms} (@{syntax axmdecl} @{syntax prop} +)
- ;
- (@@{command lemmas} | @@{command theorems}) @{syntax target}? \\
- (@{syntax thmdef}? @{syntax thmrefs} + @'and')
- (@'for' (@{syntax vars} + @'and'))?
- "}
-
- \begin{description}
-
- \item @{command "axioms"}~@{text "a: \<phi>"} introduces arbitrary
- statements as axioms of the meta-logic. In fact, axioms are
- ``axiomatic theorems'', and may be referred later just as any other
- theorem.
-
- Axioms are usually only introduced when declaring new logical
- systems. Everyday work is typically done the hard way, with proper
- definitions and proven theorems.
-
- \item @{command "lemmas"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"}~@{keyword_def
- "for"}~@{text "x\<^sub>1 \<dots> x\<^sub>m"} evaluates given facts (with attributes) in
- the current context, which may be augmented by local variables.
- Results are standardized before being stored, i.e.\ schematic
- variables are renamed to enforce index @{text "0"} uniformly.
-
- \item @{command "theorems"} is the same as @{command "lemmas"}, but
- marks the result as a different kind of facts.
-
- \end{description}
-*}
-
-
-section {* Oracles *}
-
-text {*
- \begin{matharray}{rcll}
- @{command_def "oracle"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
- \end{matharray}
-
- Oracles allow Isabelle to take advantage of external reasoners such
- as arithmetic decision procedures, model checkers, fast tautology
- checkers or computer algebra systems. Invoked as an oracle, an
- external reasoner can create arbitrary Isabelle theorems.
-
- It is the responsibility of the user to ensure that the external
- reasoner is as trustworthy as the application requires. Another
- typical source of errors is the linkup between Isabelle and the
- external tool, not just its concrete implementation, but also the
- required translation between two different logical environments.
-
- Isabelle merely guarantees well-formedness of the propositions being
- asserted, and records within the internal derivation object how
- presumed theorems depend on unproven suppositions.
-
- @{rail "
- @@{command oracle} @{syntax name} '=' @{syntax text}
- "}
-
- \begin{description}
-
- \item @{command "oracle"}~@{text "name = text"} turns the given ML
- expression @{text "text"} of type @{ML_text "'a -> cterm"} into an
- ML function of type @{ML_text "'a -> thm"}, which is bound to the
- global identifier @{ML_text name}. This acts like an infinitary
- specification of axioms! Invoking the oracle only works within the
- scope of the resulting theory.
-
- \end{description}
-
- See @{file "~~/src/HOL/ex/Iff_Oracle.thy"} for a worked example of
- defining a new primitive rule as oracle, and turning it into a proof
- method.
-*}
-
-
-section {* Name spaces *}
-
-text {*
- \begin{matharray}{rcl}
- @{command_def "hide_class"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def "hide_type"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def "hide_const"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def "hide_fact"} & : & @{text "theory \<rightarrow> theory"} \\
- \end{matharray}
-
- @{rail "
- ( @{command hide_class} | @{command hide_type} |
- @{command hide_const} | @{command hide_fact} ) ('(' @'open' ')')? (@{syntax nameref} + )
- "}
-
- Isabelle organizes any kind of name declarations (of types,
- constants, theorems etc.) by separate hierarchically structured name
- spaces. Normally the user does not have to control the behavior of
- name spaces by hand, yet the following commands provide some way to
- do so.
-
- \begin{description}
-
- \item @{command "hide_class"}~@{text names} fully removes class
- declarations from a given name space; with the @{text "(open)"}
- option, only the base name is hidden.
-
- Note that hiding name space accesses has no impact on logical
- declarations --- they remain valid internally. Entities that are no
- longer accessible to the user are printed with the special qualifier
- ``@{text "??"}'' prefixed to the full internal name.
-
- \item @{command "hide_type"}, @{command "hide_const"}, and @{command
- "hide_fact"} are similar to @{command "hide_class"}, but hide types,
- constants, and facts, respectively.
-
- \end{description}
-*}
-
-end