--- a/src/Doc/Isar_Ref/Spec.thy Fri Nov 13 21:31:04 2015 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy Fri Nov 13 21:43:31 2015 +0100
@@ -6,18 +6,18 @@
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.
+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 @{command theorem} or @{command lemma} at the theory
- level, and left again with the final conclusion (e.g.\ via @{command
- qed}).
+ 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}).
\<close>
@@ -32,32 +32,32 @@
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.\ @{command fun} in Isabelle/HOL),
- with foundational proofs performed internally. Other definitions require
- an explicit proof as justification (e.g.\ @{command function} and
- @{command termination} in Isabelle/HOL). Plain statements like @{command
- theorem} or @{command lemma} are merely a special case of that, defining a
- theorem from a given proposition and its proof.
+ definitions are self-sufficient (e.g.\ @{command fun} in Isabelle/HOL), with
+ foundational proofs performed internally. Other definitions require an
+ explicit proof as justification (e.g.\ @{command function} and @{command
+ termination} in Isabelle/HOL). Plain statements like @{command theorem} or
+ @{command lemma} are merely a 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 @{command "locale"} and @{command "class"}. It is also
- possible to use @{command context}~@{keyword "begin"}~\dots~@{command end}
- 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.
+ The theory body may be sub-structured by means of \<^emph>\<open>local theory targets\<close>,
+ such as @{command "locale"} and @{command "class"}. It is also possible to
+ use @{command context}~@{keyword "begin"}~\dots~@{command end} 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 @{command "theory"} command, which
- indicates imports of previous theories, according to an acyclic
- foundational order. Before the initial @{command "theory"} command, there
- may be optional document header material (like @{command section} or
- @{command text}, see \secref{sec:markup}). The document header is outside
- of the formal theory context, though.
+ A theory is commenced by the @{command "theory"} command, which indicates
+ imports of previous theories, according to an acyclic foundational order.
+ Before the initial @{command "theory"} command, there may be optional
+ document header material (like @{command section} or @{command text}, see
+ \secref{sec:markup}). The document header 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"}.
+ 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 name} imports? keywords? \<newline> @'begin'
@@ -74,47 +74,43 @@
thy_bounds: @{syntax name} | '(' (@{syntax name} + @'|') ')'
\<close>}
- \<^descr> @{command "theory"}~\<open>A \<IMPORTS> B\<^sub>1 \<dots> B\<^sub>n \<BEGIN>\<close>
- starts a new theory \<open>A\<close> based on the merge of existing
- theories \<open>B\<^sub>1 \<dots> B\<^sub>n\<close>. 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.
+ \<^descr> @{command "theory"}~\<open>A \<IMPORTS> B\<^sub>1 \<dots> B\<^sub>n \<BEGIN>\<close> starts a new theory
+ \<open>A\<close> based on the merge of existing theories \<open>B\<^sub>1 \<dots> B\<^sub>n\<close>. 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.
Empty imports are only allowed in the bootstrap process of the special
theory @{theory Pure}, 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 Main} in Isabelle/HOL.
+ based on Isabelle. Regular user theories usually refer to some more complex
+ entry point, such as theory @{theory Main} in Isabelle/HOL.
- 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>\<open>"typedef"\<close>
- \<open>:: thy_goal\<close> or @{keyword "keywords"}~\<^verbatim>\<open>"datatype"\<close> \<open>:: thy_decl\<close>
- for theory-level declarations
- with and without proof, respectively. Additional @{syntax tags}
- provide defaults for document preparation (\secref{sec:tags}).
+ 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>\<open>"typedef"\<close>
+ \<open>:: thy_goal\<close> or @{keyword "keywords"}~\<^verbatim>\<open>"datatype"\<close> \<open>:: thy_decl\<close> for
+ theory-level declarations with and without proof, respectively. Additional
+ @{syntax tags} provide defaults for document preparation
+ (\secref{sec:tags}).
- It is possible to specify an alternative completion via \<^verbatim>\<open>==\<close>~\<open>text\<close>,
- while the default is the corresponding keyword name.
+ It is possible to specify an alternative completion via \<^verbatim>\<open>==\<close>~\<open>text\<close>, while
+ the default is the corresponding keyword name.
- \<^descr> @{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.
+ \<^descr> @{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.
- \<^descr> @{command thy_deps} visualizes the theory hierarchy as a directed
- acyclic graph. By default, all imported theories are shown, taking the
- base session as a starting point. Alternatively, it is possibly to
- restrict the full theory graph by giving bounds, analogously to
- @{command_ref class_deps}.
+ \<^descr> @{command thy_deps} visualizes the theory hierarchy as a directed acyclic
+ graph. By default, all imported theories are shown, taking the base session
+ as a starting point. Alternatively, it is possibly to restrict the full
+ theory graph by giving bounds, analogously to @{command_ref class_deps}.
\<close>
@@ -128,20 +124,19 @@
@{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.
+ 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>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, 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"}.
+ \<^emph>\<open>Unnamed contexts\<close> 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 \<open>
@@{command context} @{syntax nameref} @'begin'
@@ -151,66 +146,61 @@
@{syntax_def target}: '(' @'in' @{syntax nameref} ')'
\<close>}
- \<^descr> @{command "context"}~\<open>c \<BEGIN>\<close> opens a named
- context, by recommencing an existing locale or class \<open>c\<close>.
- 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.
+ \<^descr> @{command "context"}~\<open>c \<BEGIN>\<close> opens a named context, by recommencing
+ an existing locale or class \<open>c\<close>. 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.
- \<^descr> @{command "context"}~\<open>bundles elements \<BEGIN>\<close> opens
- an unnamed context, by extending the enclosing global or local
- theory target by the given declaration bundles (\secref{sec:bundle})
- and context elements (\<open>\<FIXES>\<close>, \<open>\<ASSUMES>\<close>
- 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.
+ \<^descr> @{command "context"}~\<open>bundles elements \<BEGIN>\<close> opens an unnamed context,
+ by extending the enclosing global or local theory target by the given
+ declaration bundles (\secref{sec:bundle}) and context elements (\<open>\<FIXES>\<close>,
+ \<open>\<ASSUMES>\<close> 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.
+
+ \<^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> @{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> @{keyword "private"} or @{keyword "qualified"} may be given as
- modifiers before any local theory command. This restricts name space
- accesses to the local scope, as determined by the enclosing @{command
- "context"}~@{keyword "begin"}~\dots~@{command "end"} block. Outside its
- scope, a @{keyword "private"} name is inaccessible, and a @{keyword
- "qualified"} name is only accessible with some qualification.
+ \<^descr> @{keyword "private"} or @{keyword "qualified"} may be given as modifiers
+ before any local theory command. This restricts name space accesses to the
+ local scope, as determined by the enclosing @{command "context"}~@{keyword
+ "begin"}~\dots~@{command "end"} block. Outside its scope, a @{keyword
+ "private"} name is inaccessible, and a @{keyword "qualified"} name is only
+ accessible with some qualification.
- Neither a global @{command theory} nor a @{command locale} target provides
- a local scope by itself: an extra unnamed context is required to use
- @{keyword "private"} or @{keyword "qualified"} here.
+ Neither a global @{command theory} nor a @{command locale} target provides a
+ local scope by itself: an extra unnamed context is required to use @{keyword
+ "private"} or @{keyword "qualified"} here.
- \<^descr> \<open>(\<close>@{keyword_def "in"}~\<open>c)\<close> given after any local
- theory command specifies an immediate target, e.g.\ ``@{command
- "definition"}~\<open>(\<IN> c)\<close>'' or ``@{command "theorem"}~\<open>(\<IN> c)\<close>''. This works both in a local or global theory context; the
- current target context will be suspended for this command only. Note that
- ``\<open>(\<IN> -)\<close>'' will always produce a global result independently
- of the current target context.
+ \<^descr> \<open>(\<close>@{keyword_def "in"}~\<open>c)\<close> given after any local theory command specifies
+ an immediate target, e.g.\ ``@{command "definition"}~\<open>(\<IN> c)\<close>'' or
+ ``@{command "theorem"}~\<open>(\<IN> c)\<close>''. This works both in a local or global
+ theory context; the current target context will be suspended for this
+ command only. Note that ``\<open>(\<IN> -)\<close>'' will always produce a global result
+ independently of the current target context.
- Any specification element that operates on \<open>local_theory\<close> according
- to this manual implicitly allows the above target syntax \<open>(\<close>@{keyword "in"}~\<open>c)\<close>, but individual syntax diagrams omit that
- aspect for clarity.
+ Any specification element that operates on \<open>local_theory\<close> according to this
+ manual implicitly allows the above target syntax \<open>(\<close>@{keyword "in"}~\<open>c)\<close>,
+ but individual 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>.
+ 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 \<equiv> t[?x]\<close> at the theory
- level (for arbitrary \<open>?x\<close>), together with a local
- abbreviation \<open>c \<equiv> c.a x\<close> in the target context (for the
- fixed parameter \<open>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 \<equiv>
+ t[?x]\<close> at the theory level (for arbitrary \<open>?x\<close>), together with a local
+ abbreviation \<open>c \<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] \<Longrightarrow> B[?x]\<close>, again for arbitrary
- \<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] \<Longrightarrow>
+ B[?x]\<close>, again for arbitrary \<open>?x\<close>.
\<close>
@@ -226,18 +216,17 @@
\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.
+ 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}).
+ 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} @{syntax name} '=' @{syntax thmrefs} @{syntax for_fixes}
@@ -249,35 +238,29 @@
@{syntax_def "includes"}: @'includes' (@{syntax nameref}+)
\<close>}
- \<^descr> @{command bundle}~\<open>b = decls\<close> 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.
+ \<^descr> @{command bundle}~\<open>b = decls\<close> 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.
- \<^descr> @{command print_bundles} prints the named bundles that are available
- in the current context; the ``\<open>!\<close>'' option indicates extra
- verbosity.
+ \<^descr> @{command print_bundles} prints the named bundles that are available in
+ the current context; the ``\<open>!\<close>'' option indicates extra verbosity.
- \<^descr> @{command include}~\<open>b\<^sub>1 \<dots> b\<^sub>n\<close> 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.
+ \<^descr> @{command include}~\<open>b\<^sub>1 \<dots> b\<^sub>n\<close> 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.
- \<^descr> @{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.
+ \<^descr> @{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.
- \<^descr> @{keyword "includes"}~\<open>b\<^sub>1 \<dots> b\<^sub>n\<close> 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.
+ \<^descr> @{keyword "includes"}~\<open>b\<^sub>1 \<dots> b\<^sub>n\<close> 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.
- Here is an artificial example of bundling various configuration
- options:
+ Here is an artificial example of bundling various configuration options:
\<close>
(*<*)experiment begin(*>*)
@@ -299,8 +282,8 @@
@{command_def "print_abbrevs"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
\end{matharray}
- Term definitions may either happen within the logic (as equational axioms
- of a certain form, see also see \secref{sec:consts}), or outside of it as
+ Term definitions may either happen within the logic (as equational axioms of
+ a certain form, see also see \secref{sec:consts}), or outside of it as
rewrite system on abstract syntax. The second form is called
``abbreviation''.
@@ -315,38 +298,34 @@
@@{command print_abbrevs} ('!'?)
\<close>}
- \<^descr> @{command "definition"}~\<open>c \<WHERE> eq\<close> produces an
- internal definition \<open>c \<equiv> t\<close> according 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 \<leftrightarrow> B\<close>. End-users normally need not
- change the @{attribute defn} setup.
+ \<^descr> @{command "definition"}~\<open>c \<WHERE> eq\<close> produces an internal definition \<open>c
+ \<equiv> t\<close> according 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 \<leftrightarrow> B\<close>. 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.\ \<open>f x y = t\<close> instead of
- \<open>f \<equiv> \<lambda>x y. t\<close> and \<open>y \<noteq> 0 \<Longrightarrow> g x y = u\<close> instead of an
- unrestricted \<open>g \<equiv> \<lambda>x y. u\<close>.
+ 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> and \<open>y \<noteq> 0
+ \<Longrightarrow> g x y = u\<close> instead of an unrestricted \<open>g \<equiv> \<lambda>x y. u\<close>.
\<^descr> @{command "print_defn_rules"} prints the definitional rewrite rules
declared via @{attribute defn} in the current context.
- \<^descr> @{command "abbreviation"}~\<open>c \<WHERE> eq\<close> introduces a
- syntactic constant which is associated with a certain term according
- to the meta-level equality \<open>eq\<close>.
+ \<^descr> @{command "abbreviation"}~\<open>c \<WHERE> eq\<close> introduces a syntactic constant
+ which is 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!
+ 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
- ``@{keyword "output"}'' qualifier that affects the concrete syntax
- declared for abbreviations, cf.\ @{command "syntax"} in
+ 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 ``@{keyword "output"}'' qualifier that affects
+ the concrete syntax declared for abbreviations, cf.\ @{command "syntax"} in
\secref{sec:syn-trans}.
\<^descr> @{command "print_abbrevs"} prints all constant abbreviations of the
@@ -367,14 +346,13 @@
specs: (@{syntax thmdecl}? @{syntax props} + @'and')
\<close>}
- \<^descr> @{command "axiomatization"}~\<open>c\<^sub>1 \<dots> c\<^sub>m \<WHERE> \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close>
- 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 for the same constants
- later on, but it is always possible do 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.
+ \<^descr> @{command "axiomatization"}~\<open>c\<^sub>1 \<dots> c\<^sub>m \<WHERE> \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close> 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 for the same constants later on, but it is always
+ possible do 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
@@ -383,8 +361,8 @@
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.
+ the user normally stays within definitional mechanisms provided by the logic
+ and its libraries.
\<close>
@@ -397,14 +375,13 @@
@{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.
+ 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})
@@ -413,25 +390,23 @@
@@{command declare} (@{syntax thmrefs} + @'and')
\<close>}
- \<^descr> @{command "declaration"}~\<open>d\<close> adds the declaration
- function \<open>d\<close> 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.
+ \<^descr> @{command "declaration"}~\<open>d\<close> adds the declaration function \<open>d\<close> 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 \<open>(pervasive)\<close> option is given, the corresponding
- declaration is applied to all possible contexts involved, including
- the global background theory.
+ If the \<open>(pervasive)\<close> option is given, the corresponding declaration is
+ applied to all possible contexts involved, including the global background
+ theory.
- \<^descr> @{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).
+ \<^descr> @{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).
- \<^descr> @{command "declare"}~\<open>thms\<close> declares theorems to the
- current local theory context. No theorem binding is involved here,
- unlike @{command "lemmas"} (cf.\ \secref{sec:theorems}), so
- @{command "declare"} only has the effect of applying attributes as
- included in the theorem specification.
+ \<^descr> @{command "declare"}~\<open>thms\<close> declares theorems to the current local theory
+ context. No theorem binding is involved here, unlike @{command "lemmas"}
+ (cf.\ \secref{sec:theorems}), so @{command "declare"} only has the effect of
+ applying attributes as included in the theorem specification.
\<close>
@@ -439,25 +414,23 @@
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}).
+ 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.
+ 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 Ballarin2014}.
+ 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 Ballarin2014}.
\<close>
@@ -537,109 +510,100 @@
@'notes' (@{syntax thmdef}? @{syntax thmrefs} + @'and')
\<close>}
- \<^descr> @{command "locale"}~\<open>loc = import + body\<close> defines a
- new locale \<open>loc\<close> as a context consisting of a certain view of
- existing locales (\<open>import\<close>) plus some additional elements
- (\<open>body\<close>). Both \<open>import\<close> and \<open>body\<close> are optional;
- the degenerate form @{command "locale"}~\<open>loc\<close> 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.
+ \<^descr> @{command "locale"}~\<open>loc = import + body\<close> defines a new locale \<open>loc\<close> as a
+ context consisting of a certain view of existing locales (\<open>import\<close>) plus
+ some additional elements (\<open>body\<close>). Both \<open>import\<close> and \<open>body\<close> are optional;
+ the degenerate form @{command "locale"}~\<open>loc\<close> 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 \<open>import\<close> consists of a locale expression; see
- \secref{sec:proof-context} above. Its @{keyword "for"} clause defines
- the parameters of \<open>import\<close>. These are parameters of
- the defined locale. Locale parameters whose instantiation is
- omitted automatically extend the (possibly empty) @{keyword "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 \<open>import\<close> consists of a locale expression; see \secref{sec:proof-context}
+ above. Its @{keyword "for"} clause defines the parameters of \<open>import\<close>. These
+ are parameters of the defined locale. Locale parameters whose instantiation
+ is omitted automatically extend the (possibly empty) @{keyword "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 \<open>body\<close> consists of context elements.
- \<^descr> @{element "fixes"}~\<open>x :: \<tau> (mx)\<close> declares a local
- parameter of type \<open>\<tau>\<close> and mixfix annotation \<open>mx\<close> (both
- are optional). The special syntax declaration ``\<open>(\<close>@{keyword_ref "structure"}\<open>)\<close>'' means that \<open>x\<close> may
- be referenced implicitly in this context.
+ \<^descr> @{element "fixes"}~\<open>x :: \<tau> (mx)\<close> declares a local parameter of type \<open>\<tau>\<close>
+ and mixfix annotation \<open>mx\<close> (both are optional). The special syntax
+ declaration ``\<open>(\<close>@{keyword_ref "structure"}\<open>)\<close>'' means that \<open>x\<close> may be
+ referenced implicitly in this context.
- \<^descr> @{element "constrains"}~\<open>x :: \<tau>\<close> introduces a type
- constraint \<open>\<tau>\<close> on the local parameter \<open>x\<close>. This
- element is deprecated. The type constraint should be introduced in
- the @{keyword "for"} clause or the relevant @{element "fixes"} element.
+ \<^descr> @{element "constrains"}~\<open>x :: \<tau>\<close> introduces a type constraint \<open>\<tau>\<close> on the
+ local parameter \<open>x\<close>. This element is deprecated. The type constraint
+ should be introduced in the @{keyword "for"} clause or the relevant
+ @{element "fixes"} element.
- \<^descr> @{element "assumes"}~\<open>a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close>
- introduces local premises, similar to @{command "assume"} within a
- proof (cf.\ \secref{sec:proof-context}).
+ \<^descr> @{element "assumes"}~\<open>a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close> introduces local premises, similar
+ to @{command "assume"} within a proof (cf.\ \secref{sec:proof-context}).
- \<^descr> @{element "defines"}~\<open>a: x \<equiv> t\<close> 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"}~\<open>f x\<^sub>1 \<dots> x\<^sub>n \<equiv> t\<close>''.
+ \<^descr> @{element "defines"}~\<open>a: x \<equiv> t\<close> 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"}~\<open>f
+ x\<^sub>1 \<dots> x\<^sub>n \<equiv> t\<close>''.
- \<^descr> @{element "notes"}~\<open>a = b\<^sub>1 \<dots> b\<^sub>n\<close>
- 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.
+ \<^descr> @{element "notes"}~\<open>a = b\<^sub>1 \<dots> b\<^sub>n\<close> 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.
- Both @{element "assumes"} and @{element "defines"} elements
- contribute to the locale specification. When defining an operation
- derived from the parameters, @{command "definition"}
- (\secref{sec:term-definitions}) is usually more appropriate.
+ Both @{element "assumes"} and @{element "defines"} elements contribute to
+ the locale specification. When defining an operation derived from the
+ parameters, @{command "definition"} (\secref{sec:term-definitions}) is
+ usually more appropriate.
- Note that ``\<open>(\<IS> p\<^sub>1 \<dots> p\<^sub>n)\<close>'' 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.
+ Note that ``\<open>(\<IS> p\<^sub>1 \<dots> p\<^sub>n)\<close>'' 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 \<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.
+ 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>\<longrightarrow>\<close> in HOL; see also
- \secref{sec:object-logic}). Separate introduction rules \<open>loc_axioms.intro\<close> and \<open>loc.intro\<close> are provided as well.
+ 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>\<longrightarrow>\<close> in HOL; see also \secref{sec:object-logic}).
+ Separate introduction rules \<open>loc_axioms.intro\<close> and \<open>loc.intro\<close> are provided
+ as well.
- \<^descr> @{command experiment}~\<open>exprs\<close>~@{keyword "begin"} opens an
- anonymous locale context with private naming policy. Specifications in its
- body are inaccessible from outside. This is useful to perform experiments,
- without polluting the name space.
+ \<^descr> @{command experiment}~\<open>exprs\<close>~@{keyword "begin"} opens an anonymous locale
+ context with private naming policy. Specifications in its body are
+ inaccessible from outside. This is useful to perform experiments, without
+ polluting the name space.
- \<^descr> @{command "print_locale"}~\<open>locale\<close> prints the
- contents of the named locale. The command omits @{element "notes"}
- elements by default. Use @{command "print_locale"}\<open>!\<close> to
- have them included.
+ \<^descr> @{command "print_locale"}~\<open>locale\<close> prints the contents of the named
+ locale. The command omits @{element "notes"} elements by default. Use
+ @{command "print_locale"}\<open>!\<close> to have them included.
- \<^descr> @{command "print_locales"} prints the names of all locales of the
- current theory; the ``\<open>!\<close>'' option indicates extra verbosity.
+ \<^descr> @{command "print_locales"} prints the names of all locales of the current
+ theory; the ``\<open>!\<close>'' option indicates extra verbosity.
- \<^descr> @{command "locale_deps"} visualizes all locales and their
- relations as a Hasse diagram. This includes locales defined as type
- classes (\secref{sec:class}). See also @{command
- "print_dependencies"} below.
+ \<^descr> @{command "locale_deps"} visualizes all locales and their relations as a
+ Hasse diagram. This includes locales defined as type classes
+ (\secref{sec:class}). See also @{command "print_dependencies"} below.
- \<^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.
+ \<^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.
\<close>
@@ -654,12 +618,11 @@
@{command_def "print_interps"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
\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 in locales (@{command
- "sublocale"}), global and local theories (@{command
- "interpretation"}) and also within proof bodies (@{command
+ 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 in locales (@{command "sublocale"}), global and local theories
+ (@{command "interpretation"}) and also within proof bodies (@{command
"interpret"}).
@{rail \<open>
@@ -678,125 +641,107 @@
equations: @'rewrites' (@{syntax thmdecl}? @{syntax prop} + @'and')
\<close>}
- \<^descr> @{command "interpretation"}~\<open>expr\<close>~@{keyword "rewrites"}~\<open>eqns\<close>
- interprets \<open>expr\<close> in a global or local theory. 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 theory in a post-processing
- phase.
+ \<^descr> @{command "interpretation"}~\<open>expr\<close>~@{keyword "rewrites"}~\<open>eqns\<close> interprets
+ \<open>expr\<close> in a global or local theory. 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 theory in
+ a post-processing phase.
The command is aware of interpretations that are already active.
- Post-processing is achieved through a variant of roundup that takes
- the 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}.
+ Post-processing is achieved through a variant of roundup that takes the
+ 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}.
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 in global
- theories dynamically participate in any declarations added to
- locales.
+ declarations are added to the global theory for all interpretations in the
+ global theory as well. That is, interpretations in global theories
+ dynamically participate in any declarations added to locales.
- In contrast, the lifetime of an interpretation in a local theory is
- limited to the current context block. At the closing @{command end}
- of the block the interpretation and its declarations disappear.
- This enables establishing facts based on interpretations without
- creating permanent links to the interpreted locale instances, as
- would be the case with @{command sublocale}.
- While @{command "interpretation"}~\<open>(\<IN> c)
- \<dots>\<close> is technically possible, it is not useful since its result is
- discarded immediately.
+ In contrast, the lifetime of an interpretation in a local theory is limited
+ to the current context block. At the closing @{command end} of the block the
+ interpretation and its declarations disappear. This enables establishing
+ facts based on interpretations without creating permanent links to the
+ interpreted locale instances, as would be the case with @{command
+ sublocale}. While @{command "interpretation"}~\<open>(\<IN> c) \<dots>\<close> is technically
+ possible, it is not useful since its result is discarded immediately.
- 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 @{keyword "for"} clause.
+ 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 @{keyword "for"}
+ clause.
- The equations \<open>eqns\<close> yield \<^emph>\<open>rewrite morphisms\<close>, which are
- unfolded during post-processing and are useful for interpreting
- concepts introduced through definitions. The equations must be
- proved.
+ The equations \<open>eqns\<close> yield \<^emph>\<open>rewrite morphisms\<close>, which are unfolded during
+ post-processing and are useful for interpreting concepts introduced through
+ definitions. The equations must be proved.
\<^descr> @{command "interpret"}~\<open>expr\<close>~@{keyword "rewrites"}~\<open>eqns\<close> interprets
- \<open>expr\<close> in the proof context and is otherwise similar to
- interpretation in local theories. Note that for @{command
- "interpret"} the \<open>eqns\<close> should be
+ \<open>expr\<close> in the proof context and is otherwise similar to interpretation in
+ local theories. Note that for @{command "interpret"} the \<open>eqns\<close> should be
explicitly universally quantified.
\<^descr> @{command "sublocale"}~\<open>name \<subseteq> expr\<close>~@{keyword "rewrites"}~\<open>eqns\<close>
- interprets \<open>expr\<close> in the locale \<open>name\<close>. A proof that
- the specification of \<open>name\<close> implies the 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
- @{command "sublocale"}). When the context of \<open>name\<close> is
- 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 @{command "sublocale"}
- dynamic: extensions of a locale that is instantiated in \<open>expr\<close>
- may take place after the @{command "sublocale"} declaration and
- still become available in the context. Circular @{command
- "sublocale"} declarations are allowed as long as they do not lead to
- infinite chains.
+ interprets \<open>expr\<close> in the locale \<open>name\<close>. A proof that the specification of
+ \<open>name\<close> implies the 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 @{command "sublocale"}). When the
+ context of \<open>name\<close> is 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 @{command "sublocale"} dynamic: extensions
+ of a locale that is instantiated in \<open>expr\<close> may take place after the
+ @{command "sublocale"} declaration and still become available in the
+ context. Circular @{command "sublocale"} declarations 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.
+ 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.
- The equations \<open>eqns\<close> amend the morphism through
- which \<open>expr\<close> is interpreted. This enables mapping definitions
- from the interpreted locales to entities of \<open>name\<close> and can
- help break infinite chains induced by circular @{command
+ The equations \<open>eqns\<close> amend the morphism through which \<open>expr\<close> is interpreted.
+ This enables mapping definitions from the interpreted locales to entities of
+ \<open>name\<close> and can help break infinite chains induced by circular @{command
"sublocale"} declarations.
- In a named context block the @{command sublocale} command may also
- be used, but the locale argument must be omitted. The command then
- refers to the locale (or class) target of the context block.
+ In a named context block the @{command sublocale} command may also be used,
+ but the locale argument must be omitted. The command then refers to the
+ locale (or class) target of the context block.
- \<^descr> @{command "print_dependencies"}~\<open>expr\<close> is useful for
- understanding the effect of an interpretation of \<open>expr\<close> in
- the current context. It lists all locale instances for which
- interpretations would be added to the current context. Variant
- @{command "print_dependencies"}\<open>!\<close> does not generalize
- parameters and assumes an empty context --- that is, it prints all
- locale instances that would be considered for interpretation. The
- latter is useful for understanding the dependencies of a locale
- expression.
+ \<^descr> @{command "print_dependencies"}~\<open>expr\<close> is useful for understanding the
+ effect of an interpretation of \<open>expr\<close> in the current context. It lists all
+ locale instances for which interpretations would be added to the current
+ context. Variant @{command "print_dependencies"}\<open>!\<close> does not generalize
+ parameters and assumes an empty context --- that is, it prints all locale
+ instances that would be considered for interpretation. The latter is useful
+ for understanding the dependencies of a locale expression.
- \<^descr> @{command "print_interps"}~\<open>locale\<close> lists all
- interpretations of \<open>locale\<close> in the current theory or proof
- context, including those due to a combination of an @{command
- "interpretation"} or @{command "interpret"} and one or several
- @{command "sublocale"} declarations.
+ \<^descr> @{command "print_interps"}~\<open>locale\<close> lists all interpretations of \<open>locale\<close>
+ in the current theory or proof context, including those due to a combination
+ of an @{command "interpretation"} or @{command "interpret"} and one or
+ several @{command "sublocale"} declarations.
\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.
+ 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 behavior 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.
+ 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>\<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.
+ 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}
\<close>
@@ -804,15 +749,14 @@
subsubsection \<open>Permanent locale interpretation\<close>
text \<open>
- Permanent locale interpretation is a library extension on top
- of @{command "interpretation"} and @{command "sublocale"}. It is
- available by importing theory @{file "~~/src/Tools/Permanent_Interpretation.thy"}
- and provides
+ Permanent locale interpretation is a library extension on top of @{command
+ "interpretation"} and @{command "sublocale"}. It is available by importing
+ theory @{file "~~/src/Tools/Permanent_Interpretation.thy"} and provides
- \<^enum> a unified view on arbitrary suitable local theories as interpretation target;
+ \<^enum> a unified view on arbitrary suitable local theories as interpretation
+ target;
- \<^enum> rewrite morphisms by means of \<^emph>\<open>rewrite definitions\<close>.
-
+ \<^enum> rewrite morphisms by means of \<^emph>\<open>rewrite definitions\<close>.
\begin{matharray}{rcl}
@{command_def "permanent_interpretation"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close>
@@ -827,47 +771,44 @@
equations: @'rewrites' (@{syntax thmdecl}? @{syntax prop} + @'and')
\<close>}
- \<^descr> @{command "permanent_interpretation"}~\<open>expr \<DEFINING> defs\<close>~@{keyword "rewrites"}~\<open>eqns\<close>
- interprets \<open>expr\<close> in the current local theory. The command
- generates proof obligations for the instantiated specifications.
- Instantiated declarations (in particular, facts) are added to the
- local theory's underlying target in a post-processing phase. When
- adding declarations to locales, interpreted versions of these
- declarations are added to any target for all interpretations
- in that target as well. That is, permanent interpretations
- dynamically participate in any declarations added to
- locales.
+ \<^descr> @{command "permanent_interpretation"}~\<open>expr \<DEFINING> defs\<close>~@{keyword
+ "rewrites"}~\<open>eqns\<close> interprets \<open>expr\<close> in the current local theory. The
+ command generates proof obligations for the instantiated specifications.
+ Instantiated declarations (in particular, facts) are added to the local
+ theory's underlying target in a post-processing phase. When adding
+ declarations to locales, interpreted versions of these declarations are
+ added to any target for all interpretations in that target as well. That is,
+ permanent interpretations dynamically participate in any declarations added
+ to locales.
- The local theory's underlying target must explicitly support
- permanent interpretations. Prominent examples are global theories
- (where @{command "permanent_interpretation"} is technically
- corresponding to @{command "interpretation"}) and locales
- (where @{command "permanent_interpretation"} is technically
- corresponding to @{command "sublocale"}). Unnamed contexts
- (see \secref{sec:target}) are not admissible since they are
- non-permanent due to their very nature.
+ The local theory's underlying target must explicitly support permanent
+ interpretations. Prominent examples are global theories (where @{command
+ "permanent_interpretation"} is technically corresponding to @{command
+ "interpretation"}) and locales (where @{command "permanent_interpretation"}
+ is technically corresponding to @{command "sublocale"}). Unnamed contexts
+ (see \secref{sec:target}) are not admissible since they are non-permanent
+ due to their very nature.
- In additions to \<^emph>\<open>rewrite morphisms\<close> specified by \<open>eqns\<close>,
- also \<^emph>\<open>rewrite definitions\<close> may be specified. Semantically, a
- rewrite definition
+ In additions to \<^emph>\<open>rewrite morphisms\<close> specified by \<open>eqns\<close>, also \<^emph>\<open>rewrite
+ definitions\<close> may be specified. Semantically, a rewrite definition
- \<^item> produces a corresponding definition in
- the local theory's underlying target \<^emph>\<open>and\<close>
+ \<^item> produces a corresponding definition in the local theory's underlying
+ target \<^emph>\<open>and\<close>
- \<^item> augments the rewrite morphism with the equation
- stemming from the symmetric of the corresponding definition.
+ \<^item> augments the rewrite morphism with the equation stemming from the
+ symmetric of the corresponding definition.
- This is technically different to to a naive combination
- of a conventional definition and an explicit rewrite equation:
+ This is technically different to to a naive combination of a conventional
+ definition and an explicit rewrite equation:
- \<^item> Definitions are parsed in the syntactic interpretation
- context, just like equations.
+ \<^item> Definitions are parsed in the syntactic interpretation context, just
+ like equations.
- \<^item> The proof needs not consider the equations stemming from
- definitions -- they are proved implicitly by construction.
+ \<^item> The proof needs not consider the equations stemming from definitions --
+ they are proved implicitly by construction.
- Rewrite definitions yield a pattern for introducing new explicit
- operations for existing terms after interpretation.
+ Rewrite definitions yield a pattern for introducing new explicit operations
+ for existing terms after interpretation.
\<close>
@@ -885,13 +826,12 @@
@{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>\<close>. 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
+ A class is a particular locale with \<^emph>\<open>exactly one\<close> type variable \<open>\<alpha>\<close>. 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 \<open>
@@ -913,75 +853,68 @@
class_bounds: @{syntax sort} | '(' (@{syntax sort} + @'|') ')'
\<close>}
- \<^descr> @{command "class"}~\<open>c = superclasses + body\<close> defines
- a new class \<open>c\<close>, inheriting from \<open>superclasses\<close>. This
- introduces a locale \<open>c\<close> with import of all locales \<open>superclasses\<close>.
+ \<^descr> @{command "class"}~\<open>c = superclasses + body\<close> defines a new class \<open>c\<close>,
+ inheriting from \<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\<close>), mapping the local type 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>[?\<alpha> :: 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.
+ 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\<close>), mapping the local type
+ parameter \<open>\<alpha>\<close> to a schematic type variable \<open>?\<alpha> :: c\<close>.
- \<^descr> @{command "instantiation"}~\<open>t :: (s\<^sub>1, \<dots>, s\<^sub>n)s
- \<BEGIN>\<close> opens a target (cf.\ \secref{sec:target}) which
- allows to specify class operations \<open>f\<^sub>1, \<dots>, f\<^sub>n\<close> corresponding
- to sort \<open>s\<close> at the particular type instance \<open>(\<alpha>\<^sub>1 :: s\<^sub>1,
- \<dots>, \<alpha>\<^sub>n :: s\<^sub>n) t\<close>. 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.
+ 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>[?\<alpha> ::
+ 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.
- 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> @{command "instantiation"}~\<open>t :: (s\<^sub>1, \<dots>, s\<^sub>n)s \<BEGIN>\<close> opens a target
+ (cf.\ \secref{sec:target}) which allows to specify class operations \<open>f\<^sub>1, \<dots>,
+ f\<^sub>n\<close> corresponding to sort \<open>s\<close> at the particular type instance \<open>(\<alpha>\<^sub>1 :: s\<^sub>1,
+ \<dots>, \<alpha>\<^sub>n :: s\<^sub>n) t\<close>. 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.
- \<^descr> @{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.
+ Note that a list of simultaneous type constructors may be given; this
+ corresponds nicely to mutually recursive type definitions, e.g.\ in
+ Isabelle/HOL.
- On the theory level, @{command "instance"}~\<open>t :: (s\<^sub>1, \<dots>,
- s\<^sub>n)s\<close> provides a convenient way to instantiate a type class with no
- need to specify operations: one can continue with the
- instantiation proof immediately.
+ \<^descr> @{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.
- \<^descr> @{command "subclass"}~\<open>c\<close> in a class context for class
- \<open>d\<close> sets up a goal stating that 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 interpreted into \<open>d\<close> simultaneously.
+ On the theory level, @{command "instance"}~\<open>t :: (s\<^sub>1, \<dots>, s\<^sub>n)s\<close> provides a
+ convenient way to instantiate a type class with no need to specify
+ operations: one can continue with the instantiation proof immediately.
- A weakened form of this is available through a further variant of
- @{command instance}: @{command instance}~\<open>c\<^sub>1 \<subseteq> c\<^sub>2\<close> opens
- a proof that class \<open>c\<^sub>2\<close> implies \<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> @{command "subclass"}~\<open>c\<close> in a class context for class \<open>d\<close> sets up a goal
+ stating that 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
+ interpreted into \<open>d\<close> simultaneously.
- \<^descr> @{command "print_classes"} prints all classes in the current
- theory.
+ A weakened form of this is available through a further variant of @{command
+ instance}: @{command instance}~\<open>c\<^sub>1 \<subseteq> c\<^sub>2\<close> opens a proof that class \<open>c\<^sub>2\<close>
+ implies \<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> @{command "print_classes"} prints all classes in the current theory.
- \<^descr> @{command "class_deps"} visualizes classes and their subclass
- relations as a directed acyclic graph. By default, all classes from the
- current theory context are show. This may be restricted by optional bounds
- as follows: @{command "class_deps"}~\<open>upper\<close> or @{command
- "class_deps"}~\<open>upper lower\<close>. A class is visualized, iff it is a
- subclass of some sort from \<open>upper\<close> and a superclass of some sort
- from \<open>lower\<close>.
+ \<^descr> @{command "class_deps"} visualizes classes and their subclass relations as
+ a directed acyclic graph. By default, all classes from the current theory
+ context are show. This may be restricted by optional bounds as follows:
+ @{command "class_deps"}~\<open>upper\<close> or @{command "class_deps"}~\<open>upper lower\<close>. A
+ class is visualized, iff 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 @{command "proof"}). In particular,
- instantiation of trivial (syntactic) classes may be performed by a
- single ``@{command ".."}'' proof step.
+ \<^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 @{command
+ "proof"}). In particular, instantiation of trivial (syntactic) classes may
+ be performed by a single ``@{command ".."}'' proof step.
\<close>
@@ -990,61 +923,57 @@
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.
+ 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 parameter \<open>\<alpha>\<close> and local parameters \<open>f[\<alpha>]\<close>
- are accompanied by theory-level constants \<open>g[?\<alpha> :: c]\<close>
- referring to theory-level class operations \<open>f[?\<alpha> :: c]\<close>.
+ \<^item> Local constant declarations \<open>g[\<alpha>]\<close> referring to the local type parameter
+ \<open>\<alpha>\<close> and local parameters \<open>f[\<alpha>]\<close> are accompanied by theory-level constants
+ \<open>g[?\<alpha> :: c]\<close> referring to theory-level class operations \<open>f[?\<alpha> :: c]\<close>.
- \<^item> Local theorem bindings are lifted as are assumptions.
+ \<^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.
+ \<^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.
+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.
+ 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:
+ 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\<^sub>1. c\<^sub>1 \<subseteq> c\<^sub>2\<close>
\]
- This relation on sorts is further extended to tuples of sorts (of
- the same length) in the component-wise way.
+ 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:
+ 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 \<Longrightarrow> c\<^sub>1 \<subseteq> c\<^sub>2 \<Longrightarrow> \<^vec>s\<^sub>1 \<subseteq> \<^vec>s\<^sub>2\<close>
\]
- 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.
+ 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"}.
+ 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"}.
\<close>
@@ -1055,17 +984,14 @@
@{command_def "overloading"} & : & \<open>theory \<rightarrow> local_theory\<close> \\
\end{matharray}
- Isabelle/Pure's definitional schemes support certain forms of
- overloading (see \secref{sec:consts}). Overloading means that a
- constant being declared as \<open>c :: \<alpha> decl\<close> may be
- defined separately on type instances
- \<open>c :: (\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n) t decl\<close>
- for each type constructor \<open>t\<close>. At most occasions
- 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.
+ Isabelle/Pure's definitional schemes support certain forms of overloading
+ (see \secref{sec:consts}). Overloading means that a constant being declared
+ as \<open>c :: \<alpha> decl\<close> may be defined separately on type instances \<open>c :: (\<beta>\<^sub>1, \<dots>,
+ \<beta>\<^sub>n) t decl\<close> for each type constructor \<open>t\<close>. At most occasions 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 \<open>
@@{command overloading} ( spec + ) @'begin'
@@ -1073,21 +999,19 @@
spec: @{syntax name} ( '==' | '\<equiv>' ) @{syntax term} ( '(' @'unchecked' ')' )?
\<close>}
- \<^descr> @{command "overloading"}~\<open>x\<^sub>1 \<equiv> c\<^sub>1 :: \<tau>\<^sub>1 \<AND> \<dots> x\<^sub>n \<equiv> c\<^sub>n :: \<tau>\<^sub>n \<BEGIN>\<close>
- 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 \<open>x\<^sub>i\<close> to
- constants \<open>c\<^sub>i\<close> at 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. The target is concluded by @{command
- (local) "end"}.
+ \<^descr> @{command "overloading"}~\<open>x\<^sub>1 \<equiv> c\<^sub>1 :: \<tau>\<^sub>1 \<AND> \<dots> x\<^sub>n \<equiv> c\<^sub>n :: \<tau>\<^sub>n
+ \<BEGIN>\<close> 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 \<open>x\<^sub>i\<close> to constants \<open>c\<^sub>i\<close> at
+ 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. The target is concluded by @{command (local)
+ "end"}.
- A \<open>(unchecked)\<close> 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!
+ A \<open>(unchecked)\<close> 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!
\<close>
@@ -1120,56 +1044,51 @@
@@{command attribute_setup} @{syntax name} '=' @{syntax text} @{syntax text}?
\<close>}
- \<^descr> @{command "SML_file"}~\<open>name\<close> reads and evaluates the
- given Standard ML file. Top-level SML bindings are stored within
- the theory context; the initial environment is restricted to the
- Standard ML implementation of Poly/ML, without the many add-ons of
- Isabelle/ML. Multiple @{command "SML_file"} commands may be used to
- build larger Standard ML projects, independently of the regular
- Isabelle/ML environment.
+ \<^descr> @{command "SML_file"}~\<open>name\<close> reads and evaluates the given Standard ML
+ file. Top-level SML bindings are stored within the theory context; the
+ initial environment is restricted to the Standard ML implementation of
+ Poly/ML, without the many add-ons of Isabelle/ML. Multiple @{command
+ "SML_file"} commands may be used to build larger Standard ML projects,
+ independently of the regular Isabelle/ML environment.
- \<^descr> @{command "ML_file"}~\<open>name\<close> 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.
+ \<^descr> @{command "ML_file"}~\<open>name\<close> 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.
- \<^descr> @{command "ML"}~\<open>text\<close> is similar to @{command
- "ML_file"}, but evaluates directly the given \<open>text\<close>.
- Top-level ML bindings are stored within the (global or local) theory
- context.
+ \<^descr> @{command "ML"}~\<open>text\<close> is similar to @{command "ML_file"}, but evaluates
+ directly the given \<open>text\<close>. Top-level ML bindings are stored within the
+ (global or local) theory context.
- \<^descr> @{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.
+ \<^descr> @{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.
- \<^descr> @{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.
+ \<^descr> @{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.
- \<^descr> @{command "setup"}~\<open>text\<close> changes the current theory
- context by applying \<open>text\<close>, 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.
+ \<^descr> @{command "setup"}~\<open>text\<close> changes the current theory context by applying
+ \<open>text\<close>, 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.
- \<^descr> @{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.
+ \<^descr> @{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.
- \<^descr> @{command "attribute_setup"}~\<open>name = text description\<close>
- defines an attribute in the current context. The given \<open>text\<close> has to be an ML expression of type
- @{ML_type "attribute context_parser"}, cf.\ basic parsers defined in
- structure @{ML_structure Args} and @{ML_structure Attrib}.
+ \<^descr> @{command "attribute_setup"}~\<open>name = text description\<close> defines an
+ attribute in the current context. The given \<open>text\<close> has to be an ML
+ expression of type @{ML_type "attribute context_parser"}, cf.\ basic parsers
+ defined in structure @{ML_structure Args} and @{ML_structure 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:
+ implicit context, although in practice only one is modified and the other
+ serves as parameter. Here are examples for these two cases:
\<close>
(*<*)experiment begin(*>*)
@@ -1189,26 +1108,24 @@
(*<*)end(*>*)
text \<open>
- \<^descr> @{attribute ML_print_depth} controls the printing depth of the ML
- toplevel pretty printer; the precise effect depends on the ML compiler and
- run-time system. Typically the limit should be less than 10. Bigger values
- such as 100--1000 are occasionally useful for debugging.
+ \<^descr> @{attribute ML_print_depth} controls the printing depth of the ML toplevel
+ pretty printer; the precise effect depends on the ML compiler and run-time
+ system. Typically the limit should be less than 10. Bigger values such as
+ 100--1000 are occasionally useful for debugging.
- \<^descr> @{attribute ML_source_trace} indicates whether the source text that
- is given to the ML compiler should be output: it shows the raw Standard ML
+ \<^descr> @{attribute ML_source_trace} indicates whether the source text that is
+ given to the ML compiler should be output: it shows the raw Standard ML
after expansion of Isabelle/ML antiquotations.
- \<^descr> @{attribute ML_exception_trace} indicates whether the ML run-time
- system should print a detailed stack trace on exceptions. The result is
- dependent on the particular ML compiler version. Note that after Poly/ML
- 5.3 some optimizations in the run-time systems may hinder exception
- traces.
+ \<^descr> @{attribute ML_exception_trace} indicates whether the ML run-time system
+ should print a detailed stack trace on exceptions. The result is dependent
+ on the particular ML compiler version. Note that after Poly/ML 5.3 some
+ optimizations in the run-time systems may hinder exception traces.
The boundary for the exception trace is the current Isar command
transactions. It is occasionally better to insert the combinator @{ML
Runtime.exn_trace} into ML code for debugging @{cite
- "isabelle-implementation"}, closer to the point where it actually
- happens.
+ "isabelle-implementation"}, closer to the point where it actually happens.
\<close>
@@ -1225,18 +1142,17 @@
@@{command default_sort} @{syntax sort}
\<close>}
- \<^descr> @{command "default_sort"}~\<open>s\<close> makes sort \<open>s\<close> 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.
+ \<^descr> @{command "default_sort"}~\<open>s\<close> makes sort \<open>s\<close> 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.
+ 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.
+ When merging theories, the default sorts of the parents are logically
+ intersected, i.e.\ the representations as lists of classes are joined.
\<close>
@@ -1254,27 +1170,28 @@
@@{command typedecl} @{syntax typespec} @{syntax mixfix}?
\<close>}
- \<^descr> @{command "type_synonym"}~\<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = \<tau>\<close> introduces a
- \<^emph>\<open>type synonym\<close> \<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t\<close> for the existing type \<open>\<tau>\<close>. Unlike the semantic type definitions in Isabelle/HOL, type synonyms
- are merely syntactic abbreviations without any logical significance.
- Internally, type synonyms are fully expanded.
+ \<^descr> @{command "type_synonym"}~\<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = \<tau>\<close> introduces a \<^emph>\<open>type
+ synonym\<close> \<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t\<close> for the existing type \<open>\<tau>\<close>. Unlike the semantic
+ type definitions in Isabelle/HOL, type synonyms are merely syntactic
+ abbreviations without any logical significance. Internally, type synonyms
+ are fully expanded.
- \<^descr> @{command "typedecl"}~\<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t\<close> declares a new
- type constructor \<open>t\<close>. If the object-logic defines a base sort
- \<open>s\<close>, then the constructor is declared to operate on that, via
- the axiomatic type-class instance \<open>t :: (s, \<dots>, s)s\<close>.
+ \<^descr> @{command "typedecl"}~\<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t\<close> declares a new type constructor
+ \<open>t\<close>. If the object-logic defines a base sort \<open>s\<close>, then the constructor is
+ declared to operate on that, via the axiomatic type-class instance \<open>t :: (s,
+ \<dots>, s)s\<close>.
\begin{warn}
- If you introduce a new type axiomatically, i.e.\ via @{command_ref
- typedecl} and @{command_ref axiomatization}
- (\secref{sec:axiomatizations}), the minimum requirement is that it has a
- non-empty model, to avoid immediate collapse of the logical environment.
- Moreover, one needs to demonstrate that the interpretation of such
- free-form axiomatizations can coexist with other axiomatization schemes
- for types, notably @{command_def typedef} in Isabelle/HOL
- (\secref{sec:hol-typedef}), or any other extension that people might have
- introduced elsewhere.
+ If you introduce a new type axiomatically, i.e.\ via @{command_ref
+ typedecl} and @{command_ref axiomatization}
+ (\secref{sec:axiomatizations}), the minimum requirement is that it has a
+ non-empty model, to avoid immediate collapse of the logical environment.
+ Moreover, one needs to demonstrate that the interpretation of such
+ free-form axiomatizations can coexist with other axiomatization schemes
+ for types, notably @{command_def typedef} in Isabelle/HOL
+ (\secref{sec:hol-typedef}), or any other extension that people might have
+ introduced elsewhere.
\end{warn}
\<close>
@@ -1287,39 +1204,34 @@
@{command_def "defs"} & : & \<open>theory \<rightarrow> theory\<close> \\
\end{matharray}
- 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 newly declared constant. Isabelle also allows derived forms
- where the arguments of \<open>c\<close> appear on the left, abbreviating a
- prefix of \<open>\<lambda>\<close>-abstractions, e.g.\ \<open>c \<equiv> \<lambda>x y. t\<close> may be
- written more conveniently as \<open>c x y \<equiv> t\<close>. Moreover,
- definitions may be weakened by adding arbitrary pre-conditions:
- \<open>A \<Longrightarrow> c x y \<equiv> t\<close>.
+ 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 newly declared
+ constant. Isabelle also allows derived forms where the arguments of \<open>c\<close>
+ appear on the left, abbreviating a prefix of \<open>\<lambda>\<close>-abstractions, e.g.\ \<open>c \<equiv> \<lambda>x
+ y. t\<close> may be written more conveniently as \<open>c x y \<equiv> t\<close>. Moreover, definitions
+ may be weakened by adding arbitrary pre-conditions: \<open>A \<Longrightarrow> c x y \<equiv> t\<close>.
\<^medskip>
- The built-in well-formedness conditions for definitional
- specifications are:
-
- \<^item> Arguments (on the left-hand side) must be distinct variables.
+ The built-in well-formedness conditions for definitional specifications are:
- \<^item> All variables on the right-hand side must also appear on the
- left-hand side.
+ \<^item> Arguments (on the left-hand side) must be distinct variables.
- \<^item> All type variables on the right-hand side must also appear on
- the left-hand side; this prohibits \<open>0 :: nat \<equiv> length ([] ::
- \<alpha> list)\<close> for example.
+ \<^item> All variables on the right-hand side must also appear on the left-hand
+ side.
- \<^item> The definition must not be recursive. Most object-logics
- provide definitional principles that can be used to express
- recursion safely.
+ \<^item> All type variables on the right-hand side must also appear on the
+ left-hand side; this prohibits \<open>0 :: nat \<equiv> length ([] :: \<alpha> list)\<close> for
+ example.
+ \<^item> The definition must not be recursive. Most object-logics provide
+ definitional principles that can be used to express recursion safely.
- 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 patterns impose global constraints on all occurrences,
- e.g.\ \<open>d :: \<alpha> \<times> \<alpha>\<close> on the left-hand side means that all
- corresponding occurrences on some right-hand side need to be an
- instance of this, general \<open>d :: \<alpha> \<times> \<beta>\<close> will be disallowed.
+ 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 patterns impose
+ global constraints on all occurrences, e.g.\ \<open>d :: \<alpha> \<times> \<alpha>\<close> on the left-hand
+ side means that all corresponding occurrences on some right-hand side need
+ to be an instance of this, general \<open>d :: \<alpha> \<times> \<beta>\<close> will be disallowed.
@{rail \<open>
@@{command consts} ((@{syntax name} '::' @{syntax type} @{syntax mixfix}?) +)
@@ -1329,22 +1241,21 @@
opt: '(' @'unchecked'? @'overloaded'? ')'
\<close>}
- \<^descr> @{command "consts"}~\<open>c :: \<sigma>\<close> declares constant \<open>c\<close> to have any instance of type scheme \<open>\<sigma>\<close>. The optional
- mixfix annotations may attach concrete syntax to the constants
- declared.
+ \<^descr> @{command "consts"}~\<open>c :: \<sigma>\<close> declares constant \<open>c\<close> to have any instance of
+ type scheme \<open>\<sigma>\<close>. The optional mixfix annotations may attach concrete syntax
+ to the constants declared.
- \<^descr> @{command "defs"}~\<open>name: eqn\<close> introduces \<open>eqn\<close>
- as a definitional axiom for some existing constant.
+ \<^descr> @{command "defs"}~\<open>name: eqn\<close> introduces \<open>eqn\<close> as a definitional axiom for
+ some existing constant.
- The \<open>(unchecked)\<close> 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 \<open>(unchecked)\<close> 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 \<open>(overloaded)\<close> 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.
+ The \<open>(overloaded)\<close> 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.
\<close>
@@ -1363,17 +1274,15 @@
@@{command named_theorems} (@{syntax name} @{syntax text}? + @'and')
\<close>}
- \<^descr> @{command "lemmas"}~\<open>a = b\<^sub>1 \<dots> b\<^sub>n\<close>~@{keyword_def
- "for"}~\<open>x\<^sub>1 \<dots> x\<^sub>m\<close> 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 \<open>0\<close> uniformly.
+ \<^descr> @{command "lemmas"}~\<open>a = b\<^sub>1 \<dots> b\<^sub>n\<close>~@{keyword_def "for"}~\<open>x\<^sub>1 \<dots> x\<^sub>m\<close>
+ 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 \<open>0\<close> uniformly.
- \<^descr> @{command "named_theorems"}~\<open>name description\<close> declares a
- dynamic fact within the context. The same \<open>name\<close> is used to define
- an attribute with the usual \<open>add\<close>/\<open>del\<close> syntax (e.g.\ see
- \secref{sec:simp-rules}) to maintain the content incrementally, in
- canonical declaration order of the text structure.
+ \<^descr> @{command "named_theorems"}~\<open>name description\<close> declares a dynamic fact
+ within the context. The same \<open>name\<close> is used to define an attribute with the
+ usual \<open>add\<close>/\<open>del\<close> syntax (e.g.\ see \secref{sec:simp-rules}) to maintain the
+ content incrementally, in canonical declaration order of the text structure.
\<close>
@@ -1384,36 +1293,34 @@
@{command_def "oracle"} & : & \<open>theory \<rightarrow> theory\<close> & (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.
+ 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.
+ 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.
+ asserted, and records within the internal derivation object how presumed
+ theorems depend on unproven suppositions.
@{rail \<open>
@@{command oracle} @{syntax name} '=' @{syntax text}
\<close>}
- \<^descr> @{command "oracle"}~\<open>name = text\<close> turns the given ML
- expression \<open>text\<close> 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.
+ \<^descr> @{command "oracle"}~\<open>name = text\<close> turns the given ML expression \<open>text\<close> 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.
- 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.
+ 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.
\<close>
@@ -1432,20 +1339,19 @@
@{command hide_const} | @{command hide_fact} ) ('(' @'open' ')')? (@{syntax nameref} + )
\<close>}
- 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.
+ 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.
- \<^descr> @{command "hide_class"}~\<open>names\<close> fully removes class
- declarations from a given name space; with the \<open>(open)\<close>
- option, only the unqualified base name is hidden.
+ \<^descr> @{command "hide_class"}~\<open>names\<close> fully removes class declarations from a
+ given name space; with the \<open>(open)\<close> option, only the unqualified 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
- ``\<open>??\<close>'' prefixed to the full internal name.
+ 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 ``\<open>??\<close>'' prefixed to the
+ full internal name.
\<^descr> @{command "hide_type"}, @{command "hide_const"}, and @{command
"hide_fact"} are similar to @{command "hide_class"}, but hide types,