author | wenzelm |
Wed, 01 Apr 2015 23:59:56 +0200 | |
changeset 59905 | 678c9e625782 |
parent 59901 | 840d03805755 |
child 59917 | 9830c944670f |
permissions | -rw-r--r-- |
26869 | 1 |
theory Spec |
59003
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
2 |
imports Base Main "~~/src/Tools/Permanent_Interpretation" |
26869 | 3 |
begin |
4 |
||
58618 | 5 |
chapter \<open>Specifications\<close> |
26869 | 6 |
|
59781 | 7 |
text \<open>The Isabelle/Isar theory format integrates specifications and proofs, |
8 |
with support for interactive development by continuous document editing. |
|
9 |
There is a separate document preparation system (see |
|
10 |
\chref{ch:document-prep}), for typesetting formal developments together |
|
11 |
with informal text. The resulting hyper-linked PDF documents can be used |
|
12 |
both for WWW presentation and printed copies. |
|
29745 | 13 |
|
14 |
The Isar proof language (see \chref{ch:proofs}) is embedded into the |
|
15 |
theory language as a proper sub-language. Proof mode is entered by |
|
16 |
stating some @{command theorem} or @{command lemma} at the theory |
|
17 |
level, and left again with the final conclusion (e.g.\ via @{command |
|
59781 | 18 |
qed}). |
58618 | 19 |
\<close> |
29745 | 20 |
|
21 |
||
58618 | 22 |
section \<open>Defining theories \label{sec:begin-thy}\<close> |
26870 | 23 |
|
58618 | 24 |
text \<open> |
26870 | 25 |
\begin{matharray}{rcl} |
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
26 |
@{command_def "theory"} & : & @{text "toplevel \<rightarrow> theory"} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
27 |
@{command_def (global) "end"} & : & @{text "theory \<rightarrow> toplevel"} \\ |
26870 | 28 |
\end{matharray} |
29 |
||
59781 | 30 |
Isabelle/Isar theories are defined via theory files, which consist of an |
31 |
outermost sequence of definition--statement--proof elements. Some |
|
32 |
definitions are self-sufficient (e.g.\ @{command fun} in Isabelle/HOL), |
|
33 |
with foundational proofs performed internally. Other definitions require |
|
34 |
an explicit proof as justification (e.g.\ @{command function} and |
|
35 |
@{command termination} in Isabelle/HOL). Plain statements like @{command |
|
36 |
theorem} or @{command lemma} are merely a special case of that, defining a |
|
37 |
theorem from a given proposition and its proof. |
|
26870 | 38 |
|
59781 | 39 |
The theory body may be sub-structured by means of \emph{local theory |
40 |
targets}, such as @{command "locale"} and @{command "class"}. It is also |
|
41 |
possible to use @{command context}~@{keyword "begin"}~\dots~@{command end} |
|
42 |
blocks to delimited a local theory context: a \emph{named context} to |
|
43 |
augment a locale or class specification, or an \emph{unnamed context} to |
|
44 |
refer to local parameters and assumptions that are discharged later. See |
|
45 |
\secref{sec:target} for more details. |
|
28745 | 46 |
|
59781 | 47 |
\medskip A theory is commenced by the @{command "theory"} command, which |
48 |
indicates imports of previous theories, according to an acyclic |
|
49 |
foundational order. Before the initial @{command "theory"} command, there |
|
50 |
may be optional document header material (like @{command section} or |
|
51 |
@{command text}, see \secref{sec:markup}). The document header is outside |
|
52 |
of the formal theory context, though. |
|
53 |
||
54 |
A theory is concluded by a final @{command (global) "end"} command, one |
|
55 |
that does not belong to a local theory target. No further commands may |
|
56 |
follow such a global @{command (global) "end"}. |
|
26870 | 57 |
|
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
58 |
@{rail \<open> |
59781 | 59 |
@@{command theory} @{syntax name} imports? keywords? \<newline> @'begin' |
26870 | 60 |
; |
47114
7c9e31ffcd9e
updated theory header syntax and related details;
wenzelm
parents:
46999
diff
changeset
|
61 |
imports: @'imports' (@{syntax name} +) |
7c9e31ffcd9e
updated theory header syntax and related details;
wenzelm
parents:
46999
diff
changeset
|
62 |
; |
50128
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
49243
diff
changeset
|
63 |
keywords: @'keywords' (keyword_decls + @'and') |
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
49243
diff
changeset
|
64 |
; |
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
49243
diff
changeset
|
65 |
keyword_decls: (@{syntax string} +) |
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
49243
diff
changeset
|
66 |
('::' @{syntax name} @{syntax tags})? ('==' @{syntax name})? |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
67 |
\<close>} |
26870 | 68 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
69 |
\begin{description} |
26870 | 70 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
71 |
\item @{command "theory"}~@{text "A \<IMPORTS> B\<^sub>1 \<dots> B\<^sub>n \<BEGIN>"} |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
72 |
starts a new theory @{text A} based on the merge of existing |
47114
7c9e31ffcd9e
updated theory header syntax and related details;
wenzelm
parents:
46999
diff
changeset
|
73 |
theories @{text "B\<^sub>1 \<dots> B\<^sub>n"}. Due to the possibility to import more |
7c9e31ffcd9e
updated theory header syntax and related details;
wenzelm
parents:
46999
diff
changeset
|
74 |
than one ancestor, the resulting theory structure of an Isabelle |
7c9e31ffcd9e
updated theory header syntax and related details;
wenzelm
parents:
46999
diff
changeset
|
75 |
session forms a directed acyclic graph (DAG). Isabelle takes care |
7c9e31ffcd9e
updated theory header syntax and related details;
wenzelm
parents:
46999
diff
changeset
|
76 |
that sources contributing to the development graph are always |
7c9e31ffcd9e
updated theory header syntax and related details;
wenzelm
parents:
46999
diff
changeset
|
77 |
up-to-date: changed files are automatically rechecked whenever a |
7c9e31ffcd9e
updated theory header syntax and related details;
wenzelm
parents:
46999
diff
changeset
|
78 |
theory header specification is processed. |
7c9e31ffcd9e
updated theory header syntax and related details;
wenzelm
parents:
46999
diff
changeset
|
79 |
|
59781 | 80 |
Empty imports are only allowed in the bootstrap process of the special |
81 |
theory @{theory Pure}, which is the start of any other formal development |
|
82 |
based on Isabelle. Regular user theories usually refer to some more |
|
83 |
complex entry point, such as theory @{theory Main} in Isabelle/HOL. |
|
84 |
||
47114
7c9e31ffcd9e
updated theory header syntax and related details;
wenzelm
parents:
46999
diff
changeset
|
85 |
The optional @{keyword_def "keywords"} specification declares outer |
7c9e31ffcd9e
updated theory header syntax and related details;
wenzelm
parents:
46999
diff
changeset
|
86 |
syntax (\chref{ch:outer-syntax}) that is introduced in this theory |
7c9e31ffcd9e
updated theory header syntax and related details;
wenzelm
parents:
46999
diff
changeset
|
87 |
later on (rare in end-user applications). Both minor keywords and |
7c9e31ffcd9e
updated theory header syntax and related details;
wenzelm
parents:
46999
diff
changeset
|
88 |
major keywords of the Isar command language need to be specified, in |
7c9e31ffcd9e
updated theory header syntax and related details;
wenzelm
parents:
46999
diff
changeset
|
89 |
order to make parsing of proof documents work properly. Command |
7c9e31ffcd9e
updated theory header syntax and related details;
wenzelm
parents:
46999
diff
changeset
|
90 |
keywords need to be classified according to their structural role in |
7c9e31ffcd9e
updated theory header syntax and related details;
wenzelm
parents:
46999
diff
changeset
|
91 |
the formal text. Examples may be seen in Isabelle/HOL sources |
58724 | 92 |
itself, such as @{keyword "keywords"}~@{verbatim \<open>"typedef"\<close>} |
47114
7c9e31ffcd9e
updated theory header syntax and related details;
wenzelm
parents:
46999
diff
changeset
|
93 |
@{text ":: thy_goal"} or @{keyword "keywords"}~@{verbatim |
58724 | 94 |
\<open>"datatype"\<close>} @{text ":: thy_decl"} for theory-level declarations |
47114
7c9e31ffcd9e
updated theory header syntax and related details;
wenzelm
parents:
46999
diff
changeset
|
95 |
with and without proof, respectively. Additional @{syntax tags} |
7c9e31ffcd9e
updated theory header syntax and related details;
wenzelm
parents:
46999
diff
changeset
|
96 |
provide defaults for document preparation (\secref{sec:tags}). |
50128
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
49243
diff
changeset
|
97 |
|
59781 | 98 |
It is possible to specify an alternative completion via @{verbatim |
99 |
"=="}~@{text "text"}, while the default is the corresponding keyword name. |
|
26870 | 100 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
101 |
\item @{command (global) "end"} concludes the current theory |
47114
7c9e31ffcd9e
updated theory header syntax and related details;
wenzelm
parents:
46999
diff
changeset
|
102 |
definition. Note that some other commands, e.g.\ local theory |
7c9e31ffcd9e
updated theory header syntax and related details;
wenzelm
parents:
46999
diff
changeset
|
103 |
targets @{command locale} or @{command class} may involve a |
7c9e31ffcd9e
updated theory header syntax and related details;
wenzelm
parents:
46999
diff
changeset
|
104 |
@{keyword "begin"} that needs to be matched by @{command (local) |
7c9e31ffcd9e
updated theory header syntax and related details;
wenzelm
parents:
46999
diff
changeset
|
105 |
"end"}, according to the usual rules for nested blocks. |
27040 | 106 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
107 |
\end{description} |
58618 | 108 |
\<close> |
27040 | 109 |
|
110 |
||
58618 | 111 |
section \<open>Local theory targets \label{sec:target}\<close> |
27040 | 112 |
|
58618 | 113 |
text \<open> |
47483 | 114 |
\begin{matharray}{rcll} |
115 |
@{command_def "context"} & : & @{text "theory \<rightarrow> local_theory"} \\ |
|
116 |
@{command_def (local) "end"} & : & @{text "local_theory \<rightarrow> theory"} \\ |
|
117 |
\end{matharray} |
|
118 |
||
59781 | 119 |
A local theory target is a specification context that is managed |
120 |
separately within the enclosing theory. Contexts may introduce parameters |
|
121 |
(fixed variables) and assumptions (hypotheses). Definitions and theorems |
|
47482
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47114
diff
changeset
|
122 |
depending on the context may be added incrementally later on. |
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47114
diff
changeset
|
123 |
|
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47114
diff
changeset
|
124 |
\emph{Named contexts} refer to locales (cf.\ \secref{sec:locale}) or |
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47114
diff
changeset
|
125 |
type classes (cf.\ \secref{sec:class}); the name ``@{text "-"}'' |
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47114
diff
changeset
|
126 |
signifies the global theory context. |
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47114
diff
changeset
|
127 |
|
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47114
diff
changeset
|
128 |
\emph{Unnamed contexts} may introduce additional parameters and |
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47114
diff
changeset
|
129 |
assumptions, and results produced in the context are generalized |
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47114
diff
changeset
|
130 |
accordingly. Such auxiliary contexts may be nested within other |
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47114
diff
changeset
|
131 |
targets, like @{command "locale"}, @{command "class"}, @{command |
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47114
diff
changeset
|
132 |
"instantiation"}, @{command "overloading"}. |
27040 | 133 |
|
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
134 |
@{rail \<open> |
47484 | 135 |
@@{command context} @{syntax nameref} @'begin' |
27040 | 136 |
; |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
137 |
@@{command context} @{syntax_ref "includes"}? (@{syntax context_elem} * ) @'begin' |
47484 | 138 |
; |
46999 | 139 |
@{syntax_def target}: '(' @'in' @{syntax nameref} ')' |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
140 |
\<close>} |
27040 | 141 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
142 |
\begin{description} |
27040 | 143 |
|
47482
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47114
diff
changeset
|
144 |
\item @{command "context"}~@{text "c \<BEGIN>"} opens a named |
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47114
diff
changeset
|
145 |
context, by recommencing an existing locale or class @{text c}. |
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47114
diff
changeset
|
146 |
Note that locale and class definitions allow to include the |
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47114
diff
changeset
|
147 |
@{keyword "begin"} keyword as well, in order to continue the local |
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47114
diff
changeset
|
148 |
theory immediately after the initial specification. |
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47114
diff
changeset
|
149 |
|
47484 | 150 |
\item @{command "context"}~@{text "bundles elements \<BEGIN>"} opens |
151 |
an unnamed context, by extending the enclosing global or local |
|
152 |
theory target by the given declaration bundles (\secref{sec:bundle}) |
|
153 |
and context elements (@{text "\<FIXES>"}, @{text "\<ASSUMES>"} |
|
154 |
etc.). This means any results stemming from definitions and proofs |
|
155 |
in the extended context will be exported into the enclosing target |
|
156 |
by lifting over extra parameters and premises. |
|
27040 | 157 |
|
47482
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47114
diff
changeset
|
158 |
\item @{command (local) "end"} concludes the current local theory, |
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47114
diff
changeset
|
159 |
according to the nesting of contexts. Note that a global @{command |
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47114
diff
changeset
|
160 |
(global) "end"} has a different meaning: it concludes the theory |
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47114
diff
changeset
|
161 |
itself (\secref{sec:begin-thy}). |
27040 | 162 |
|
59783
00b62aa9f430
tuned syntax diagrams -- no duplication of "target";
wenzelm
parents:
59781
diff
changeset
|
163 |
\item @{text "("}@{keyword_def "in"}~@{text "c)"} given after any local |
00b62aa9f430
tuned syntax diagrams -- no duplication of "target";
wenzelm
parents:
59781
diff
changeset
|
164 |
theory command specifies an immediate target, e.g.\ ``@{command |
00b62aa9f430
tuned syntax diagrams -- no duplication of "target";
wenzelm
parents:
59781
diff
changeset
|
165 |
"definition"}~@{text "(\<IN> c)"}'' or ``@{command "theorem"}~@{text |
00b62aa9f430
tuned syntax diagrams -- no duplication of "target";
wenzelm
parents:
59781
diff
changeset
|
166 |
"(\<IN> c)"}''. This works both in a local or global theory context; the |
00b62aa9f430
tuned syntax diagrams -- no duplication of "target";
wenzelm
parents:
59781
diff
changeset
|
167 |
current target context will be suspended for this command only. Note that |
00b62aa9f430
tuned syntax diagrams -- no duplication of "target";
wenzelm
parents:
59781
diff
changeset
|
168 |
``@{text "(\<IN> -)"}'' will always produce a global result independently |
00b62aa9f430
tuned syntax diagrams -- no duplication of "target";
wenzelm
parents:
59781
diff
changeset
|
169 |
of the current target context. |
27040 | 170 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
171 |
\end{description} |
27040 | 172 |
|
59783
00b62aa9f430
tuned syntax diagrams -- no duplication of "target";
wenzelm
parents:
59781
diff
changeset
|
173 |
Any specification element that operates on @{text local_theory} according |
00b62aa9f430
tuned syntax diagrams -- no duplication of "target";
wenzelm
parents:
59781
diff
changeset
|
174 |
to this manual implicitly allows the above target syntax @{text |
00b62aa9f430
tuned syntax diagrams -- no duplication of "target";
wenzelm
parents:
59781
diff
changeset
|
175 |
"("}@{keyword "in"}~@{text "c)"}, but individual syntax diagrams omit that |
00b62aa9f430
tuned syntax diagrams -- no duplication of "target";
wenzelm
parents:
59781
diff
changeset
|
176 |
aspect for clarity. |
00b62aa9f430
tuned syntax diagrams -- no duplication of "target";
wenzelm
parents:
59781
diff
changeset
|
177 |
|
00b62aa9f430
tuned syntax diagrams -- no duplication of "target";
wenzelm
parents:
59781
diff
changeset
|
178 |
\medskip The exact meaning of results produced within a local theory |
00b62aa9f430
tuned syntax diagrams -- no duplication of "target";
wenzelm
parents:
59781
diff
changeset
|
179 |
context depends on the underlying target infrastructure (locale, type |
00b62aa9f430
tuned syntax diagrams -- no duplication of "target";
wenzelm
parents:
59781
diff
changeset
|
180 |
class etc.). The general idea is as follows, considering a context named |
27040 | 181 |
@{text c} with parameter @{text x} and assumption @{text "A[x]"}. |
182 |
||
183 |
Definitions are exported by introducing a global version with |
|
184 |
additional arguments; a syntactic abbreviation links the long form |
|
185 |
with the abstract version of the target context. For example, |
|
186 |
@{text "a \<equiv> t[x]"} becomes @{text "c.a ?x \<equiv> t[?x]"} at the theory |
|
187 |
level (for arbitrary @{text "?x"}), together with a local |
|
188 |
abbreviation @{text "c \<equiv> c.a x"} in the target context (for the |
|
189 |
fixed parameter @{text x}). |
|
190 |
||
191 |
Theorems are exported by discharging the assumptions and |
|
192 |
generalizing the parameters of the context. For example, @{text "a: |
|
193 |
B[x]"} becomes @{text "c.a: A[?x] \<Longrightarrow> B[?x]"}, again for arbitrary |
|
194 |
@{text "?x"}. |
|
59783
00b62aa9f430
tuned syntax diagrams -- no duplication of "target";
wenzelm
parents:
59781
diff
changeset
|
195 |
\<close> |
27040 | 196 |
|
197 |
||
58618 | 198 |
section \<open>Bundled declarations \label{sec:bundle}\<close> |
47484 | 199 |
|
58618 | 200 |
text \<open> |
47484 | 201 |
\begin{matharray}{rcl} |
202 |
@{command_def "bundle"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ |
|
203 |
@{command_def "print_bundles"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow> "} \\ |
|
204 |
@{command_def "include"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\ |
|
205 |
@{command_def "including"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\ |
|
206 |
@{keyword_def "includes"} & : & syntax \\ |
|
207 |
\end{matharray} |
|
208 |
||
209 |
The outer syntax of fact expressions (\secref{sec:syn-att}) involves |
|
210 |
theorems and attributes, which are evaluated in the context and |
|
211 |
applied to it. Attributes may declare theorems to the context, as |
|
212 |
in @{text "this_rule [intro] that_rule [elim]"} for example. |
|
213 |
Configuration options (\secref{sec:config}) are special declaration |
|
214 |
attributes that operate on the context without a theorem, as in |
|
215 |
@{text "[[show_types = false]]"} for example. |
|
216 |
||
217 |
Expressions of this form may be defined as \emph{bundled |
|
218 |
declarations} in the context, and included in other situations later |
|
219 |
on. Including declaration bundles augments a local context casually |
|
220 |
without logical dependencies, which is in contrast to locales and |
|
221 |
locale interpretation (\secref{sec:locale}). |
|
222 |
||
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
223 |
@{rail \<open> |
59785 | 224 |
@@{command bundle} @{syntax name} '=' @{syntax thmrefs} @{syntax for_fixes} |
47484 | 225 |
; |
226 |
(@@{command include} | @@{command including}) (@{syntax nameref}+) |
|
227 |
; |
|
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
228 |
@{syntax_def "includes"}: @'includes' (@{syntax nameref}+) |
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
229 |
\<close>} |
47484 | 230 |
|
231 |
\begin{description} |
|
232 |
||
233 |
\item @{command bundle}~@{text "b = decls"} defines a bundle of |
|
234 |
declarations in the current context. The RHS is similar to the one |
|
235 |
of the @{command declare} command. Bundles defined in local theory |
|
236 |
targets are subject to transformations via morphisms, when moved |
|
237 |
into different application contexts; this works analogously to any |
|
238 |
other local theory specification. |
|
239 |
||
240 |
\item @{command print_bundles} prints the named bundles that are |
|
241 |
available in the current context. |
|
242 |
||
243 |
\item @{command include}~@{text "b\<^sub>1 \<dots> b\<^sub>n"} includes the declarations |
|
244 |
from the given bundles into the current proof body context. This is |
|
245 |
analogous to @{command "note"} (\secref{sec:proof-facts}) with the |
|
246 |
expanded bundles. |
|
247 |
||
248 |
\item @{command including} is similar to @{command include}, but |
|
249 |
works in proof refinement (backward mode). This is analogous to |
|
250 |
@{command "using"} (\secref{sec:proof-facts}) with the expanded |
|
251 |
bundles. |
|
252 |
||
253 |
\item @{keyword "includes"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"} is similar to |
|
254 |
@{command include}, but works in situations where a specification |
|
255 |
context is constructed, notably for @{command context} and long |
|
256 |
statements of @{command theorem} etc. |
|
257 |
||
258 |
\end{description} |
|
259 |
||
260 |
Here is an artificial example of bundling various configuration |
|
58618 | 261 |
options:\<close> |
47484 | 262 |
|
59905 | 263 |
(*<*)experiment begin(*>*) |
53536
69c943125fd3
do not expose internal flags to attribute name space;
wenzelm
parents:
53370
diff
changeset
|
264 |
bundle trace = [[simp_trace, linarith_trace, metis_trace, smt_trace]] |
47484 | 265 |
|
266 |
lemma "x = x" |
|
267 |
including trace by metis |
|
59905 | 268 |
(*<*)end(*>*) |
47484 | 269 |
|
270 |
||
58618 | 271 |
section \<open>Term definitions \label{sec:term-definitions}\<close> |
27040 | 272 |
|
58618 | 273 |
text \<open> |
27040 | 274 |
\begin{matharray}{rcll} |
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
275 |
@{command_def "definition"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
276 |
@{attribute_def "defn"} & : & @{text attribute} \\ |
51585 | 277 |
@{command_def "print_defn_rules"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow> "} \\ |
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
278 |
@{command_def "abbreviation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
279 |
@{command_def "print_abbrevs"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow> "} \\ |
27040 | 280 |
\end{matharray} |
281 |
||
57487 | 282 |
Term definitions may either happen within the logic (as equational axioms |
283 |
of a certain form, see also see \secref{sec:consts}), or outside of it as |
|
284 |
rewrite system on abstract syntax. The second form is called |
|
285 |
``abbreviation''. |
|
27040 | 286 |
|
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
287 |
@{rail \<open> |
59783
00b62aa9f430
tuned syntax diagrams -- no duplication of "target";
wenzelm
parents:
59781
diff
changeset
|
288 |
@@{command definition} (decl @'where')? @{syntax thmdecl}? @{syntax prop} |
27040 | 289 |
; |
59783
00b62aa9f430
tuned syntax diagrams -- no duplication of "target";
wenzelm
parents:
59781
diff
changeset
|
290 |
@@{command abbreviation} @{syntax mode}? \<newline> |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
41435
diff
changeset
|
291 |
(decl @'where')? @{syntax prop} |
27040 | 292 |
; |
293 |
||
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
41435
diff
changeset
|
294 |
decl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}? |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
295 |
\<close>} |
27040 | 296 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
297 |
\begin{description} |
27040 | 298 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
299 |
\item @{command "definition"}~@{text "c \<WHERE> eq"} produces an |
27040 | 300 |
internal definition @{text "c \<equiv> t"} according to the specification |
301 |
given as @{text eq}, which is then turned into a proven fact. The |
|
302 |
given proposition may deviate from internal meta-level equality |
|
303 |
according to the rewrite rules declared as @{attribute defn} by the |
|
304 |
object-logic. This usually covers object-level equality @{text "x = |
|
305 |
y"} and equivalence @{text "A \<leftrightarrow> B"}. End-users normally need not |
|
306 |
change the @{attribute defn} setup. |
|
307 |
||
308 |
Definitions may be presented with explicit arguments on the LHS, as |
|
309 |
well as additional conditions, e.g.\ @{text "f x y = t"} instead of |
|
310 |
@{text "f \<equiv> \<lambda>x y. t"} and @{text "y \<noteq> 0 \<Longrightarrow> g x y = u"} instead of an |
|
311 |
unrestricted @{text "g \<equiv> \<lambda>x y. u"}. |
|
51585 | 312 |
|
313 |
\item @{command "print_defn_rules"} prints the definitional rewrite rules |
|
314 |
declared via @{attribute defn} in the current context. |
|
315 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
316 |
\item @{command "abbreviation"}~@{text "c \<WHERE> eq"} introduces a |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
317 |
syntactic constant which is associated with a certain term according |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
318 |
to the meta-level equality @{text eq}. |
27040 | 319 |
|
320 |
Abbreviations participate in the usual type-inference process, but |
|
321 |
are expanded before the logic ever sees them. Pretty printing of |
|
322 |
terms involves higher-order rewriting with rules stemming from |
|
323 |
reverted abbreviations. This needs some care to avoid overlapping |
|
324 |
or looping syntactic replacements! |
|
325 |
||
326 |
The optional @{text mode} specification restricts output to a |
|
327 |
particular print mode; using ``@{text input}'' here achieves the |
|
328 |
effect of one-way abbreviations. The mode may also include an |
|
329 |
``@{keyword "output"}'' qualifier that affects the concrete syntax |
|
330 |
declared for abbreviations, cf.\ @{command "syntax"} in |
|
331 |
\secref{sec:syn-trans}. |
|
332 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
333 |
\item @{command "print_abbrevs"} prints all constant abbreviations |
27040 | 334 |
of the current context. |
335 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
336 |
\end{description} |
58618 | 337 |
\<close> |
27040 | 338 |
|
339 |
||
58618 | 340 |
section \<open>Axiomatizations \label{sec:axiomatizations}\<close> |
57487 | 341 |
|
58618 | 342 |
text \<open> |
57487 | 343 |
\begin{matharray}{rcll} |
344 |
@{command_def "axiomatization"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\ |
|
345 |
\end{matharray} |
|
346 |
||
347 |
@{rail \<open> |
|
348 |
@@{command axiomatization} @{syntax "fixes"}? (@'where' specs)? |
|
349 |
; |
|
350 |
specs: (@{syntax thmdecl}? @{syntax props} + @'and') |
|
351 |
\<close>} |
|
352 |
||
353 |
\begin{description} |
|
354 |
||
355 |
\item @{command "axiomatization"}~@{text "c\<^sub>1 \<dots> c\<^sub>m \<WHERE> \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} |
|
356 |
introduces several constants simultaneously and states axiomatic |
|
357 |
properties for these. The constants are marked as being specified once and |
|
358 |
for all, which prevents additional specifications for the same constants |
|
359 |
later on, but it is always possible do emit axiomatizations without |
|
360 |
referring to particular constants. Note that lack of precise dependency |
|
361 |
tracking of axiomatizations may disrupt the well-formedness of an |
|
362 |
otherwise definitional theory. |
|
363 |
||
364 |
Axiomatization is restricted to a global theory context: support for local |
|
365 |
theory targets \secref{sec:target} would introduce an extra dimension of |
|
366 |
uncertainty what the written specifications really are, and make it |
|
367 |
infeasible to argue why they are correct. |
|
368 |
||
369 |
Axiomatic specifications are required when declaring a new logical system |
|
370 |
within Isabelle/Pure, but in an application environment like Isabelle/HOL |
|
371 |
the user normally stays within definitional mechanisms provided by the |
|
372 |
logic and its libraries. |
|
373 |
||
374 |
\end{description} |
|
58618 | 375 |
\<close> |
57487 | 376 |
|
377 |
||
58618 | 378 |
section \<open>Generic declarations\<close> |
27040 | 379 |
|
58618 | 380 |
text \<open> |
47483 | 381 |
\begin{matharray}{rcl} |
382 |
@{command_def "declaration"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ |
|
383 |
@{command_def "syntax_declaration"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ |
|
384 |
@{command_def "declare"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ |
|
385 |
\end{matharray} |
|
386 |
||
27040 | 387 |
Arbitrary operations on the background context may be wrapped-up as |
388 |
generic declaration elements. Since the underlying concept of local |
|
389 |
theories may be subject to later re-interpretation, there is an |
|
390 |
additional dependency on a morphism that tells the difference of the |
|
391 |
original declaration context wrt.\ the application context |
|
392 |
encountered later on. A fact declaration is an important special |
|
393 |
case: it consists of a theorem which is applied to the context by |
|
394 |
means of an attribute. |
|
395 |
||
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
396 |
@{rail \<open> |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
41435
diff
changeset
|
397 |
(@@{command declaration} | @@{command syntax_declaration}) |
59783
00b62aa9f430
tuned syntax diagrams -- no duplication of "target";
wenzelm
parents:
59781
diff
changeset
|
398 |
('(' @'pervasive' ')')? \<newline> @{syntax text} |
27040 | 399 |
; |
59783
00b62aa9f430
tuned syntax diagrams -- no duplication of "target";
wenzelm
parents:
59781
diff
changeset
|
400 |
@@{command declare} (@{syntax thmrefs} + @'and') |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
401 |
\<close>} |
27040 | 402 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
403 |
\begin{description} |
27040 | 404 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
405 |
\item @{command "declaration"}~@{text d} adds the declaration |
27040 | 406 |
function @{text d} of ML type @{ML_type declaration}, to the current |
407 |
local theory under construction. In later application contexts, the |
|
408 |
function is transformed according to the morphisms being involved in |
|
409 |
the interpretation hierarchy. |
|
410 |
||
33516 | 411 |
If the @{text "(pervasive)"} option is given, the corresponding |
412 |
declaration is applied to all possible contexts involved, including |
|
413 |
the global background theory. |
|
414 |
||
40784 | 415 |
\item @{command "syntax_declaration"} is similar to @{command |
416 |
"declaration"}, but is meant to affect only ``syntactic'' tools by |
|
417 |
convention (such as notation and type-checking information). |
|
418 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
419 |
\item @{command "declare"}~@{text thms} declares theorems to the |
27040 | 420 |
current local theory context. No theorem binding is involved here, |
421 |
unlike @{command "theorems"} or @{command "lemmas"} (cf.\ |
|
51313 | 422 |
\secref{sec:theorems}), so @{command "declare"} only has the effect |
27040 | 423 |
of applying attributes as included in the theorem specification. |
424 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
425 |
\end{description} |
58618 | 426 |
\<close> |
27040 | 427 |
|
428 |
||
58618 | 429 |
section \<open>Locales \label{sec:locale}\<close> |
27040 | 430 |
|
58618 | 431 |
text \<open> |
54049 | 432 |
A locale is a functor that maps parameters (including implicit type |
433 |
parameters) and a specification to a list of declarations. The |
|
434 |
syntax of locales is modeled after the Isar proof context commands |
|
435 |
(cf.\ \secref{sec:proof-context}). |
|
436 |
||
437 |
Locale hierarchies are supported by maintaining a graph of |
|
438 |
dependencies between locale instances in the global theory. |
|
439 |
Dependencies may be introduced through import (where a locale is |
|
440 |
defined as sublocale of the imported instances) or by proving that |
|
441 |
an existing locale is a sublocale of one or several locale |
|
442 |
instances. |
|
443 |
||
444 |
A locale may be opened with the purpose of appending to its list of |
|
445 |
declarations (cf.\ \secref{sec:target}). When opening a locale |
|
446 |
declarations from all dependencies are collected and are presented |
|
447 |
as a local theory. In this process, which is called \emph{roundup}, |
|
448 |
redundant locale instances are omitted. A locale instance is |
|
449 |
redundant if it is subsumed by an instance encountered earlier. A |
|
450 |
more detailed description of this process is available elsewhere |
|
58552 | 451 |
@{cite Ballarin2014}. |
58618 | 452 |
\<close> |
27040 | 453 |
|
454 |
||
58618 | 455 |
subsection \<open>Locale expressions \label{sec:locale-expr}\<close> |
33846 | 456 |
|
58618 | 457 |
text \<open> |
54049 | 458 |
A \emph{locale expression} denotes a context composed of instances |
459 |
of existing locales. The context consists of the declaration |
|
460 |
elements from the locale instances. Redundant locale instances are |
|
461 |
omitted according to roundup. |
|
33846 | 462 |
|
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
463 |
@{rail \<open> |
59785 | 464 |
@{syntax_def locale_expr}: (instance + '+') @{syntax for_fixes} |
33846 | 465 |
; |
42617 | 466 |
instance: (qualifier ':')? @{syntax nameref} (pos_insts | named_insts) |
33846 | 467 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
41435
diff
changeset
|
468 |
qualifier: @{syntax name} ('?' | '!')? |
33846 | 469 |
; |
42617 | 470 |
pos_insts: ('_' | @{syntax term})* |
33846 | 471 |
; |
42617 | 472 |
named_insts: @'where' (@{syntax name} '=' @{syntax term} + @'and') |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
473 |
\<close>} |
33846 | 474 |
|
475 |
A locale instance consists of a reference to a locale and either |
|
476 |
positional or named parameter instantiations. Identical |
|
54049 | 477 |
instantiations (that is, those that instantiate a parameter by itself) |
40256 | 478 |
may be omitted. The notation `@{text "_"}' enables to omit the |
479 |
instantiation for a parameter inside a positional instantiation. |
|
33846 | 480 |
|
481 |
Terms in instantiations are from the context the locale expressions |
|
482 |
is declared in. Local names may be added to this context with the |
|
48824
45d0e40b07af
Clarification: free variables allowed in interpreted locale instances.
ballarin
parents:
47484
diff
changeset
|
483 |
optional @{keyword "for"} clause. This is useful for shadowing names |
45d0e40b07af
Clarification: free variables allowed in interpreted locale instances.
ballarin
parents:
47484
diff
changeset
|
484 |
bound in outer contexts, and for declaring syntax. In addition, |
45d0e40b07af
Clarification: free variables allowed in interpreted locale instances.
ballarin
parents:
47484
diff
changeset
|
485 |
syntax declarations from one instance are effective when parsing |
45d0e40b07af
Clarification: free variables allowed in interpreted locale instances.
ballarin
parents:
47484
diff
changeset
|
486 |
subsequent instances of the same expression. |
33846 | 487 |
|
488 |
Instances have an optional qualifier which applies to names in |
|
489 |
declarations. Names include local definitions and theorem names. |
|
490 |
If present, the qualifier itself is either optional |
|
491 |
(``\texttt{?}''), which means that it may be omitted on input of the |
|
492 |
qualified name, or mandatory (``\texttt{!}''). If neither |
|
493 |
``\texttt{?}'' nor ``\texttt{!}'' are present, the command's default |
|
494 |
is used. For @{command "interpretation"} and @{command "interpret"} |
|
495 |
the default is ``mandatory'', for @{command "locale"} and @{command |
|
54049 | 496 |
"sublocale"} the default is ``optional''. Qualifiers play no role |
497 |
in determining whether one locale instance subsumes another. |
|
58618 | 498 |
\<close> |
33846 | 499 |
|
500 |
||
58618 | 501 |
subsection \<open>Locale declarations\<close> |
27040 | 502 |
|
58618 | 503 |
text \<open> |
27040 | 504 |
\begin{matharray}{rcl} |
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
505 |
@{command_def "locale"} & : & @{text "theory \<rightarrow> local_theory"} \\ |
59901 | 506 |
@{command_def "experiment"} & : & @{text "theory \<rightarrow> local_theory"} \\ |
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
507 |
@{command_def "print_locale"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
508 |
@{command_def "print_locales"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
50716 | 509 |
@{command_def "locale_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
510 |
@{method_def intro_locales} & : & @{text method} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
511 |
@{method_def unfold_locales} & : & @{text method} \\ |
27040 | 512 |
\end{matharray} |
513 |
||
514 |
\indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes} |
|
28787 | 515 |
\indexisarelem{defines}\indexisarelem{notes} |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
516 |
@{rail \<open> |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
41435
diff
changeset
|
517 |
@@{command locale} @{syntax name} ('=' @{syntax locale})? @'begin'? |
27040 | 518 |
; |
59901 | 519 |
@@{command experiment} (@{syntax context_elem}*) @'begin' |
520 |
; |
|
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
41435
diff
changeset
|
521 |
@@{command print_locale} '!'? @{syntax nameref} |
27040 | 522 |
; |
42617 | 523 |
@{syntax_def locale}: @{syntax context_elem}+ | |
524 |
@{syntax locale_expr} ('+' (@{syntax context_elem}+))? |
|
27040 | 525 |
; |
42617 | 526 |
@{syntax_def context_elem}: |
59785 | 527 |
@'fixes' @{syntax "fixes"} | |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
41435
diff
changeset
|
528 |
@'constrains' (@{syntax name} '::' @{syntax type} + @'and') | |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
41435
diff
changeset
|
529 |
@'assumes' (@{syntax props} + @'and') | |
42705 | 530 |
@'defines' (@{syntax thmdecl}? @{syntax prop} @{syntax prop_pat}? + @'and') | |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
41435
diff
changeset
|
531 |
@'notes' (@{syntax thmdef}? @{syntax thmrefs} + @'and') |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
532 |
\<close>} |
27040 | 533 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
534 |
\begin{description} |
27040 | 535 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
536 |
\item @{command "locale"}~@{text "loc = import + body"} defines a |
27040 | 537 |
new locale @{text loc} as a context consisting of a certain view of |
538 |
existing locales (@{text import}) plus some additional elements |
|
539 |
(@{text body}). Both @{text import} and @{text body} are optional; |
|
540 |
the degenerate form @{command "locale"}~@{text loc} defines an empty |
|
541 |
locale, which may still be useful to collect declarations of facts |
|
542 |
later on. Type-inference on locale expressions automatically takes |
|
543 |
care of the most general typing that the combined context elements |
|
544 |
may acquire. |
|
545 |
||
54049 | 546 |
The @{text import} consists of a locale expression; see |
547 |
\secref{sec:proof-context} above. Its @{keyword "for"} clause defines |
|
548 |
the parameters of @{text import}. These are parameters of |
|
549 |
the defined locale. Locale parameters whose instantiation is |
|
550 |
omitted automatically extend the (possibly empty) @{keyword "for"} |
|
551 |
clause: they are inserted at its beginning. This means that these |
|
552 |
parameters may be referred to from within the expression and also in |
|
553 |
the subsequent context elements and provides a notational |
|
554 |
convenience for the inheritance of parameters in locale |
|
33846 | 555 |
declarations. |
27040 | 556 |
|
33846 | 557 |
The @{text body} consists of context elements. |
27040 | 558 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
559 |
\begin{description} |
27040 | 560 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
561 |
\item @{element "fixes"}~@{text "x :: \<tau> (mx)"} declares a local |
27040 | 562 |
parameter of type @{text \<tau>} and mixfix annotation @{text mx} (both |
563 |
are optional). The special syntax declaration ``@{text |
|
51657
3db1bbc82d8d
more accurate documentation of "(structure)" mixfix;
wenzelm
parents:
51585
diff
changeset
|
564 |
"("}@{keyword_ref "structure"}@{text ")"}'' means that @{text x} may |
3db1bbc82d8d
more accurate documentation of "(structure)" mixfix;
wenzelm
parents:
51585
diff
changeset
|
565 |
be referenced implicitly in this context. |
27040 | 566 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
567 |
\item @{element "constrains"}~@{text "x :: \<tau>"} introduces a type |
33846 | 568 |
constraint @{text \<tau>} on the local parameter @{text x}. This |
38110 | 569 |
element is deprecated. The type constraint should be introduced in |
54049 | 570 |
the @{keyword "for"} clause or the relevant @{element "fixes"} element. |
27040 | 571 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
572 |
\item @{element "assumes"}~@{text "a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} |
27040 | 573 |
introduces local premises, similar to @{command "assume"} within a |
574 |
proof (cf.\ \secref{sec:proof-context}). |
|
575 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
576 |
\item @{element "defines"}~@{text "a: x \<equiv> t"} defines a previously |
27040 | 577 |
declared parameter. This is similar to @{command "def"} within a |
578 |
proof (cf.\ \secref{sec:proof-context}), but @{element "defines"} |
|
579 |
takes an equational proposition instead of variable-term pair. The |
|
580 |
left-hand side of the equation may have additional arguments, e.g.\ |
|
581 |
``@{element "defines"}~@{text "f x\<^sub>1 \<dots> x\<^sub>n \<equiv> t"}''. |
|
582 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
583 |
\item @{element "notes"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"} |
27040 | 584 |
reconsiders facts within a local context. Most notably, this may |
585 |
include arbitrary declarations in any attribute specifications |
|
586 |
included here, e.g.\ a local @{attribute simp} rule. |
|
587 |
||
54049 | 588 |
\end{description} |
27040 | 589 |
|
54049 | 590 |
Both @{element "assumes"} and @{element "defines"} elements |
591 |
contribute to the locale specification. When defining an operation |
|
592 |
derived from the parameters, @{command "definition"} |
|
57487 | 593 |
(\secref{sec:term-definitions}) is usually more appropriate. |
27040 | 594 |
|
595 |
Note that ``@{text "(\<IS> p\<^sub>1 \<dots> p\<^sub>n)"}'' patterns given |
|
596 |
in the syntax of @{element "assumes"} and @{element "defines"} above |
|
597 |
are illegal in locale definitions. In the long goal format of |
|
598 |
\secref{sec:goals}, term bindings may be included as expected, |
|
599 |
though. |
|
600 |
||
33846 | 601 |
\medskip Locale specifications are ``closed up'' by |
27040 | 602 |
turning the given text into a predicate definition @{text |
603 |
loc_axioms} and deriving the original assumptions as local lemmas |
|
604 |
(modulo local definitions). The predicate statement covers only the |
|
605 |
newly specified assumptions, omitting the content of included locale |
|
606 |
expressions. The full cumulative view is only provided on export, |
|
607 |
involving another predicate @{text loc} that refers to the complete |
|
608 |
specification text. |
|
609 |
||
610 |
In any case, the predicate arguments are those locale parameters |
|
54049 | 611 |
that actually occur in the respective piece of text. Also these |
612 |
predicates operate at the meta-level in theory, but the locale |
|
27040 | 613 |
packages attempts to internalize statements according to the |
614 |
object-logic setup (e.g.\ replacing @{text \<And>} by @{text \<forall>}, and |
|
615 |
@{text "\<Longrightarrow>"} by @{text "\<longrightarrow>"} in HOL; see also |
|
616 |
\secref{sec:object-logic}). Separate introduction rules @{text |
|
617 |
loc_axioms.intro} and @{text loc.intro} are provided as well. |
|
59901 | 618 |
|
619 |
\item @{command experiment}~@{text exprs}~@{keyword "begin"} opens an |
|
620 |
anonymous locale context with private naming policy. Specifications in its |
|
621 |
body are inaccessible from outside. This is useful to perform experiments, |
|
622 |
without polluting the name space. |
|
623 |
||
33867 | 624 |
\item @{command "print_locale"}~@{text "locale"} prints the |
625 |
contents of the named locale. The command omits @{element "notes"} |
|
626 |
elements by default. Use @{command "print_locale"}@{text "!"} to |
|
627 |
have them included. |
|
27040 | 628 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
629 |
\item @{command "print_locales"} prints the names of all locales |
27040 | 630 |
of the current theory. |
631 |
||
50716 | 632 |
\item @{command "locale_deps"} visualizes all locales and their |
633 |
relations as a Hasse diagram. This includes locales defined as type |
|
54049 | 634 |
classes (\secref{sec:class}). See also @{command |
635 |
"print_dependencies"} below. |
|
50716 | 636 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
637 |
\item @{method intro_locales} and @{method unfold_locales} |
27040 | 638 |
repeatedly expand all introduction rules of locale predicates of the |
639 |
theory. While @{method intro_locales} only applies the @{text |
|
54049 | 640 |
loc.intro} introduction rules and therefore does not descend to |
27040 | 641 |
assumptions, @{method unfold_locales} is more aggressive and applies |
642 |
@{text loc_axioms.intro} as well. Both methods are aware of locale |
|
28787 | 643 |
specifications entailed by the context, both from target statements, |
644 |
and from interpretations (see below). New goals that are entailed |
|
645 |
by the current context are discharged automatically. |
|
27040 | 646 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
647 |
\end{description} |
58618 | 648 |
\<close> |
27040 | 649 |
|
650 |
||
58618 | 651 |
subsection \<open>Locale interpretation\<close> |
27040 | 652 |
|
58618 | 653 |
text \<open> |
27040 | 654 |
\begin{matharray}{rcl} |
53368
92b9965f479d
Clarifies documentation of interpretation in local theories.
ballarin
parents:
53015
diff
changeset
|
655 |
@{command_def "interpretation"} & : & @{text "theory | local_theory \<rightarrow> proof(prove)"} \\ |
33846 | 656 |
@{command_def "interpret"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\ |
53368
92b9965f479d
Clarifies documentation of interpretation in local theories.
ballarin
parents:
53015
diff
changeset
|
657 |
@{command_def "sublocale"} & : & @{text "theory | local_theory \<rightarrow> proof(prove)"} \\ |
41435 | 658 |
@{command_def "print_dependencies"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
33846 | 659 |
@{command_def "print_interps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
27040 | 660 |
\end{matharray} |
661 |
||
54049 | 662 |
Locales may be instantiated, and the resulting instantiated |
663 |
declarations added to the current context. This requires proof (of |
|
664 |
the instantiated specification) and is called \emph{locale |
|
665 |
interpretation}. Interpretation is possible in locales (@{command |
|
666 |
"sublocale"}), global and local theories (@{command |
|
667 |
"interpretation"}) and also within proof bodies (@{command |
|
48824
45d0e40b07af
Clarification: free variables allowed in interpreted locale instances.
ballarin
parents:
47484
diff
changeset
|
668 |
"interpret"}). |
47483 | 669 |
|
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
670 |
@{rail \<open> |
53368
92b9965f479d
Clarifies documentation of interpretation in local theories.
ballarin
parents:
53015
diff
changeset
|
671 |
@@{command interpretation} @{syntax locale_expr} equations? |
27040 | 672 |
; |
42617 | 673 |
@@{command interpret} @{syntax locale_expr} equations? |
27040 | 674 |
; |
55029
61a6bf7d4b02
clarified @{rail} syntax: prefer explicit \<newline> symbol;
wenzelm
parents:
54049
diff
changeset
|
675 |
@@{command sublocale} (@{syntax nameref} ('<' | '\<subseteq>'))? @{syntax locale_expr} \<newline> |
42704 | 676 |
equations? |
33846 | 677 |
; |
42617 | 678 |
@@{command print_dependencies} '!'? @{syntax locale_expr} |
27040 | 679 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
41435
diff
changeset
|
680 |
@@{command print_interps} @{syntax nameref} |
41434
710cdb9e0d17
Documentation for 'interpret' and 'sublocale' with mixins.
ballarin
parents:
41249
diff
changeset
|
681 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
41435
diff
changeset
|
682 |
|
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
41435
diff
changeset
|
683 |
equations: @'where' (@{syntax thmdecl}? @{syntax prop} + @'and') |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
684 |
\<close>} |
27040 | 685 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
686 |
\begin{description} |
27040 | 687 |
|
33867 | 688 |
\item @{command "interpretation"}~@{text "expr \<WHERE> eqns"} |
54049 | 689 |
interprets @{text expr} in a global or local theory. The command |
690 |
generates proof obligations for the instantiated specifications. |
|
691 |
Once these are discharged by the user, instantiated declarations (in |
|
692 |
particular, facts) are added to the theory in a post-processing |
|
693 |
phase. |
|
53368
92b9965f479d
Clarifies documentation of interpretation in local theories.
ballarin
parents:
53015
diff
changeset
|
694 |
|
54049 | 695 |
The command is aware of interpretations that are already active. |
696 |
Post-processing is achieved through a variant of roundup that takes |
|
697 |
the interpretations of the current global or local theory into |
|
698 |
account. In order to simplify the proof obligations according to |
|
699 |
existing interpretations use methods @{method intro_locales} or |
|
700 |
@{method unfold_locales}. |
|
53368
92b9965f479d
Clarifies documentation of interpretation in local theories.
ballarin
parents:
53015
diff
changeset
|
701 |
|
53369
b4bcac7d065b
Clarifies that interpretation does not only apply to facts, but to declaratoins in general.
ballarin
parents:
53368
diff
changeset
|
702 |
When adding declarations to locales, interpreted versions of these |
b4bcac7d065b
Clarifies that interpretation does not only apply to facts, but to declaratoins in general.
ballarin
parents:
53368
diff
changeset
|
703 |
declarations are added to the global theory for all interpretations |
b4bcac7d065b
Clarifies that interpretation does not only apply to facts, but to declaratoins in general.
ballarin
parents:
53368
diff
changeset
|
704 |
in the global theory as well. That is, interpretations in global |
b4bcac7d065b
Clarifies that interpretation does not only apply to facts, but to declaratoins in general.
ballarin
parents:
53368
diff
changeset
|
705 |
theories dynamically participate in any declarations added to |
54049 | 706 |
locales. |
707 |
||
708 |
In contrast, the lifetime of an interpretation in a local theory is |
|
709 |
limited to the current context block. At the closing @{command end} |
|
710 |
of the block the interpretation and its declarations disappear. |
|
711 |
This enables establishing facts based on interpretations without |
|
712 |
creating permanent links to the interpreted locale instances, as |
|
713 |
would be the case with @{command sublocale}. |
|
714 |
While @{command "interpretation"}~@{text "(\<IN> c) |
|
715 |
\<dots>"} is technically possible, it is not useful since its result is |
|
716 |
discarded immediately. |
|
33846 | 717 |
|
48824
45d0e40b07af
Clarification: free variables allowed in interpreted locale instances.
ballarin
parents:
47484
diff
changeset
|
718 |
Free variables in the interpreted expression are allowed. They are |
45d0e40b07af
Clarification: free variables allowed in interpreted locale instances.
ballarin
parents:
47484
diff
changeset
|
719 |
turned into schematic variables in the generated declarations. In |
45d0e40b07af
Clarification: free variables allowed in interpreted locale instances.
ballarin
parents:
47484
diff
changeset
|
720 |
order to use a free variable whose name is already bound in the |
45d0e40b07af
Clarification: free variables allowed in interpreted locale instances.
ballarin
parents:
47484
diff
changeset
|
721 |
context --- for example, because a constant of that name exists --- |
54049 | 722 |
add it to the @{keyword "for"} clause. |
48824
45d0e40b07af
Clarification: free variables allowed in interpreted locale instances.
ballarin
parents:
47484
diff
changeset
|
723 |
|
53370
7a41ec2cc522
Further clarifies sublocale and rewrite morphisms.
ballarin
parents:
53369
diff
changeset
|
724 |
The equations @{text eqns} yield \emph{rewrite morphisms}, which are |
7a41ec2cc522
Further clarifies sublocale and rewrite morphisms.
ballarin
parents:
53369
diff
changeset
|
725 |
unfolded during post-processing and are useful for interpreting |
7a41ec2cc522
Further clarifies sublocale and rewrite morphisms.
ballarin
parents:
53369
diff
changeset
|
726 |
concepts introduced through definitions. The equations must be |
7a41ec2cc522
Further clarifies sublocale and rewrite morphisms.
ballarin
parents:
53369
diff
changeset
|
727 |
proved. |
27040 | 728 |
|
38110 | 729 |
\item @{command "interpret"}~@{text "expr \<WHERE> eqns"} interprets |
730 |
@{text expr} in the proof context and is otherwise similar to |
|
53370
7a41ec2cc522
Further clarifies sublocale and rewrite morphisms.
ballarin
parents:
53369
diff
changeset
|
731 |
interpretation in local theories. Note that for @{command |
7a41ec2cc522
Further clarifies sublocale and rewrite morphisms.
ballarin
parents:
53369
diff
changeset
|
732 |
"interpret"} the @{text eqns} should be |
41434
710cdb9e0d17
Documentation for 'interpret' and 'sublocale' with mixins.
ballarin
parents:
41249
diff
changeset
|
733 |
explicitly universally quantified. |
710cdb9e0d17
Documentation for 'interpret' and 'sublocale' with mixins.
ballarin
parents:
41249
diff
changeset
|
734 |
|
710cdb9e0d17
Documentation for 'interpret' and 'sublocale' with mixins.
ballarin
parents:
41249
diff
changeset
|
735 |
\item @{command "sublocale"}~@{text "name \<subseteq> expr \<WHERE> |
710cdb9e0d17
Documentation for 'interpret' and 'sublocale' with mixins.
ballarin
parents:
41249
diff
changeset
|
736 |
eqns"} |
710cdb9e0d17
Documentation for 'interpret' and 'sublocale' with mixins.
ballarin
parents:
41249
diff
changeset
|
737 |
interprets @{text expr} in the locale @{text name}. A proof that |
710cdb9e0d17
Documentation for 'interpret' and 'sublocale' with mixins.
ballarin
parents:
41249
diff
changeset
|
738 |
the specification of @{text name} implies the specification of |
710cdb9e0d17
Documentation for 'interpret' and 'sublocale' with mixins.
ballarin
parents:
41249
diff
changeset
|
739 |
@{text expr} is required. As in the localized version of the |
710cdb9e0d17
Documentation for 'interpret' and 'sublocale' with mixins.
ballarin
parents:
41249
diff
changeset
|
740 |
theorem command, the proof is in the context of @{text name}. After |
53370
7a41ec2cc522
Further clarifies sublocale and rewrite morphisms.
ballarin
parents:
53369
diff
changeset
|
741 |
the proof obligation has been discharged, the locale hierarchy is |
7a41ec2cc522
Further clarifies sublocale and rewrite morphisms.
ballarin
parents:
53369
diff
changeset
|
742 |
changed as if @{text name} imported @{text expr} (hence the name |
7a41ec2cc522
Further clarifies sublocale and rewrite morphisms.
ballarin
parents:
53369
diff
changeset
|
743 |
@{command "sublocale"}). When the context of @{text name} is |
54049 | 744 |
subsequently entered, traversing the locale hierarchy will involve |
53370
7a41ec2cc522
Further clarifies sublocale and rewrite morphisms.
ballarin
parents:
53369
diff
changeset
|
745 |
the locale instances of @{text expr}, and their declarations will be |
7a41ec2cc522
Further clarifies sublocale and rewrite morphisms.
ballarin
parents:
53369
diff
changeset
|
746 |
added to the context. This makes @{command "sublocale"} |
7a41ec2cc522
Further clarifies sublocale and rewrite morphisms.
ballarin
parents:
53369
diff
changeset
|
747 |
dynamic: extensions of a locale that is instantiated in @{text expr} |
7a41ec2cc522
Further clarifies sublocale and rewrite morphisms.
ballarin
parents:
53369
diff
changeset
|
748 |
may take place after the @{command "sublocale"} declaration and |
7a41ec2cc522
Further clarifies sublocale and rewrite morphisms.
ballarin
parents:
53369
diff
changeset
|
749 |
still become available in the context. Circular @{command |
7a41ec2cc522
Further clarifies sublocale and rewrite morphisms.
ballarin
parents:
53369
diff
changeset
|
750 |
"sublocale"} declarations are allowed as long as they do not lead to |
54049 | 751 |
infinite chains. |
41434
710cdb9e0d17
Documentation for 'interpret' and 'sublocale' with mixins.
ballarin
parents:
41249
diff
changeset
|
752 |
|
53368
92b9965f479d
Clarifies documentation of interpretation in local theories.
ballarin
parents:
53015
diff
changeset
|
753 |
If interpretations of @{text name} exist in the current global |
92b9965f479d
Clarifies documentation of interpretation in local theories.
ballarin
parents:
53015
diff
changeset
|
754 |
theory, the command adds interpretations for @{text expr} as well, |
92b9965f479d
Clarifies documentation of interpretation in local theories.
ballarin
parents:
53015
diff
changeset
|
755 |
with the same qualifier, although only for fragments of @{text expr} |
92b9965f479d
Clarifies documentation of interpretation in local theories.
ballarin
parents:
53015
diff
changeset
|
756 |
that are not interpreted in the theory already. |
41434
710cdb9e0d17
Documentation for 'interpret' and 'sublocale' with mixins.
ballarin
parents:
41249
diff
changeset
|
757 |
|
53370
7a41ec2cc522
Further clarifies sublocale and rewrite morphisms.
ballarin
parents:
53369
diff
changeset
|
758 |
The equations @{text eqns} amend the morphism through |
7a41ec2cc522
Further clarifies sublocale and rewrite morphisms.
ballarin
parents:
53369
diff
changeset
|
759 |
which @{text expr} is interpreted. This enables mapping definitions |
7a41ec2cc522
Further clarifies sublocale and rewrite morphisms.
ballarin
parents:
53369
diff
changeset
|
760 |
from the interpreted locales to entities of @{text name} and can |
54049 | 761 |
help break infinite chains induced by circular @{command |
762 |
"sublocale"} declarations. |
|
27040 | 763 |
|
53368
92b9965f479d
Clarifies documentation of interpretation in local theories.
ballarin
parents:
53015
diff
changeset
|
764 |
In a named context block the @{command sublocale} command may also |
92b9965f479d
Clarifies documentation of interpretation in local theories.
ballarin
parents:
53015
diff
changeset
|
765 |
be used, but the locale argument must be omitted. The command then |
92b9965f479d
Clarifies documentation of interpretation in local theories.
ballarin
parents:
53015
diff
changeset
|
766 |
refers to the locale (or class) target of the context block. |
51747 | 767 |
|
41435 | 768 |
\item @{command "print_dependencies"}~@{text "expr"} is useful for |
54049 | 769 |
understanding the effect of an interpretation of @{text "expr"} in |
770 |
the current context. It lists all locale instances for which |
|
771 |
interpretations would be added to the current context. Variant |
|
772 |
@{command "print_dependencies"}@{text "!"} does not generalize |
|
773 |
parameters and assumes an empty context --- that is, it prints all |
|
774 |
locale instances that would be considered for interpretation. The |
|
775 |
latter is useful for understanding the dependencies of a locale |
|
776 |
expression. |
|
41435 | 777 |
|
33867 | 778 |
\item @{command "print_interps"}~@{text "locale"} lists all |
38110 | 779 |
interpretations of @{text "locale"} in the current theory or proof |
51565 | 780 |
context, including those due to a combination of an @{command |
38110 | 781 |
"interpretation"} or @{command "interpret"} and one or several |
782 |
@{command "sublocale"} declarations. |
|
33867 | 783 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
784 |
\end{description} |
27040 | 785 |
|
786 |
\begin{warn} |
|
54049 | 787 |
If a global theory inherits declarations (body elements) for a |
788 |
locale from one parent and an interpretation of that locale from |
|
789 |
another parent, the interpretation will not be applied to the |
|
790 |
declarations. |
|
791 |
\end{warn} |
|
792 |
||
793 |
\begin{warn} |
|
27040 | 794 |
Since attributes are applied to interpreted theorems, |
795 |
interpretation may modify the context of common proof tools, e.g.\ |
|
33867 | 796 |
the Simplifier or Classical Reasoner. As the behavior of such |
797 |
tools is \emph{not} stable under interpretation morphisms, manual |
|
798 |
declarations might have to be added to the target context of the |
|
799 |
interpretation to revert such declarations. |
|
27040 | 800 |
\end{warn} |
801 |
||
802 |
\begin{warn} |
|
51747 | 803 |
An interpretation in a local theory or proof context may subsume previous |
27040 | 804 |
interpretations. This happens if the same specification fragment |
805 |
is interpreted twice and the instantiation of the second |
|
806 |
interpretation is more general than the interpretation of the |
|
33846 | 807 |
first. The locale package does not attempt to remove subsumed |
808 |
interpretations. |
|
27040 | 809 |
\end{warn} |
58618 | 810 |
\<close> |
27040 | 811 |
|
812 |
||
59003
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
813 |
subsubsection \<open>Permanent locale interpretation\<close> |
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
814 |
|
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
815 |
text \<open> |
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
816 |
Permanent locale interpretation is a library extension on top |
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
817 |
of @{command "interpretation"} and @{command "sublocale"}. It is |
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
818 |
available by importing theory @{file "~~/src/Tools/Permanent_Interpretation.thy"} |
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
819 |
and provides |
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
820 |
\begin{enumerate} |
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
821 |
\item a unified view on arbitrary suitable local theories as interpretation target; |
59320
a375de4dc07a
avoid technical term "mixin" in user documentation text
haftmann
parents:
59028
diff
changeset
|
822 |
\item rewrite morphisms by means of \emph{rewrite definitions}. |
59003
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
823 |
\end{enumerate} |
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
824 |
|
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
825 |
\begin{matharray}{rcl} |
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
826 |
@{command_def "permanent_interpretation"} & : & @{text "local_theory \<rightarrow> proof(prove)"} |
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
827 |
\end{matharray} |
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
828 |
|
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
829 |
@{rail \<open> |
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
830 |
@@{command permanent_interpretation} @{syntax locale_expr} \<newline> |
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
831 |
definitions? equations? |
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
832 |
; |
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
833 |
|
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
834 |
definitions: @'defining' (@{syntax thmdecl}? @{syntax name} \<newline> |
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
835 |
@{syntax mixfix}? @'=' @{syntax term} + @'and'); |
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
836 |
equations: @'where' (@{syntax thmdecl}? @{syntax prop} + @'and') |
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
837 |
\<close>} |
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
838 |
|
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
839 |
\begin{description} |
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
840 |
|
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
841 |
\item @{command "permanent_interpretation"}~@{text "expr \<DEFINING> defs \<WHERE> eqns"} |
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
842 |
interprets @{text expr} in the current local theory. The command |
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
843 |
generates proof obligations for the instantiated specifications. |
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
844 |
Instantiated declarations (in particular, facts) are added to the |
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
845 |
local theory's underlying target in a post-processing phase. When |
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
846 |
adding declarations to locales, interpreted versions of these |
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
847 |
declarations are added to any target for all interpretations |
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
848 |
in that target as well. That is, permanent interpretations |
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
849 |
dynamically participate in any declarations added to |
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
850 |
locales. |
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
851 |
|
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
852 |
The local theory's underlying target must explicitly support |
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
853 |
permanent interpretations. Prominent examples are global theories |
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
854 |
(where @{command "permanent_interpretation"} is technically |
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
855 |
corresponding to @{command "interpretation"}) and locales |
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
856 |
(where @{command "permanent_interpretation"} is technically |
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
857 |
corresponding to @{command "sublocale"}). Unnamed contexts |
59320
a375de4dc07a
avoid technical term "mixin" in user documentation text
haftmann
parents:
59028
diff
changeset
|
858 |
(see \secref{sec:target}) are not admissible since they are |
59003
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
859 |
non-permanent due to their very nature. |
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
860 |
|
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
861 |
In additions to \emph{rewrite morphisms} specified by @{text eqns}, |
59320
a375de4dc07a
avoid technical term "mixin" in user documentation text
haftmann
parents:
59028
diff
changeset
|
862 |
also \emph{rewrite definitions} may be specified. Semantically, a |
a375de4dc07a
avoid technical term "mixin" in user documentation text
haftmann
parents:
59028
diff
changeset
|
863 |
rewrite definition |
a375de4dc07a
avoid technical term "mixin" in user documentation text
haftmann
parents:
59028
diff
changeset
|
864 |
|
a375de4dc07a
avoid technical term "mixin" in user documentation text
haftmann
parents:
59028
diff
changeset
|
865 |
\begin{itemize} |
a375de4dc07a
avoid technical term "mixin" in user documentation text
haftmann
parents:
59028
diff
changeset
|
866 |
|
a375de4dc07a
avoid technical term "mixin" in user documentation text
haftmann
parents:
59028
diff
changeset
|
867 |
\item produces a corresponding definition in |
a375de4dc07a
avoid technical term "mixin" in user documentation text
haftmann
parents:
59028
diff
changeset
|
868 |
the local theory's underlying target \emph{and} |
a375de4dc07a
avoid technical term "mixin" in user documentation text
haftmann
parents:
59028
diff
changeset
|
869 |
|
a375de4dc07a
avoid technical term "mixin" in user documentation text
haftmann
parents:
59028
diff
changeset
|
870 |
\item augments the rewrite morphism with the equation |
a375de4dc07a
avoid technical term "mixin" in user documentation text
haftmann
parents:
59028
diff
changeset
|
871 |
stemming from the symmetric of the corresponding definition. |
59003
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
872 |
|
59320
a375de4dc07a
avoid technical term "mixin" in user documentation text
haftmann
parents:
59028
diff
changeset
|
873 |
\end{itemize} |
59003
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
874 |
|
59320
a375de4dc07a
avoid technical term "mixin" in user documentation text
haftmann
parents:
59028
diff
changeset
|
875 |
This is technically different to to a naive combination |
a375de4dc07a
avoid technical term "mixin" in user documentation text
haftmann
parents:
59028
diff
changeset
|
876 |
of a conventional definition and an explicit rewrite equation: |
59003
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
877 |
|
59320
a375de4dc07a
avoid technical term "mixin" in user documentation text
haftmann
parents:
59028
diff
changeset
|
878 |
\begin{itemize} |
59003
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
879 |
|
59320
a375de4dc07a
avoid technical term "mixin" in user documentation text
haftmann
parents:
59028
diff
changeset
|
880 |
\item Definitions are parsed in the syntactic interpretation |
a375de4dc07a
avoid technical term "mixin" in user documentation text
haftmann
parents:
59028
diff
changeset
|
881 |
context, just like equations. |
a375de4dc07a
avoid technical term "mixin" in user documentation text
haftmann
parents:
59028
diff
changeset
|
882 |
|
a375de4dc07a
avoid technical term "mixin" in user documentation text
haftmann
parents:
59028
diff
changeset
|
883 |
\item The proof needs not consider the equations stemming from |
59003
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
884 |
definitions -- they are proved implicitly by construction. |
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
885 |
|
59320
a375de4dc07a
avoid technical term "mixin" in user documentation text
haftmann
parents:
59028
diff
changeset
|
886 |
\end{itemize} |
59003
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
887 |
|
59320
a375de4dc07a
avoid technical term "mixin" in user documentation text
haftmann
parents:
59028
diff
changeset
|
888 |
Rewrite definitions yield a pattern for introducing new explicit |
59003
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
889 |
operations for existing terms after interpretation. |
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
890 |
|
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
891 |
\end{description} |
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
892 |
\<close> |
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
893 |
|
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
894 |
|
58618 | 895 |
section \<open>Classes \label{sec:class}\<close> |
27040 | 896 |
|
58618 | 897 |
text \<open> |
27040 | 898 |
\begin{matharray}{rcl} |
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
899 |
@{command_def "class"} & : & @{text "theory \<rightarrow> local_theory"} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
900 |
@{command_def "instantiation"} & : & @{text "theory \<rightarrow> local_theory"} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
901 |
@{command_def "instance"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ |
42626 | 902 |
@{command "instance"} & : & @{text "theory \<rightarrow> proof(prove)"} \\ |
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
903 |
@{command_def "subclass"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
904 |
@{command_def "print_classes"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
29706 | 905 |
@{command_def "class_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
906 |
@{method_def intro_classes} & : & @{text method} \\ |
27040 | 907 |
\end{matharray} |
908 |
||
47483 | 909 |
A class is a particular locale with \emph{exactly one} type variable |
910 |
@{text \<alpha>}. Beyond the underlying locale, a corresponding type class |
|
911 |
is established which is interpreted logically as axiomatic type |
|
58552 | 912 |
class @{cite "Wenzel:1997:TPHOL"} whose logical content are the |
47483 | 913 |
assumptions of the locale. Thus, classes provide the full |
914 |
generality of locales combined with the commodity of type classes |
|
58552 | 915 |
(notably type-inference). See @{cite "isabelle-classes"} for a short |
47483 | 916 |
tutorial. |
917 |
||
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
918 |
@{rail \<open> |
42704 | 919 |
@@{command class} class_spec @'begin'? |
920 |
; |
|
921 |
class_spec: @{syntax name} '=' |
|
42617 | 922 |
((@{syntax nameref} '+' (@{syntax context_elem}+)) | |
42704 | 923 |
@{syntax nameref} | (@{syntax context_elem}+)) |
27040 | 924 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
41435
diff
changeset
|
925 |
@@{command instantiation} (@{syntax nameref} + @'and') '::' @{syntax arity} @'begin' |
27040 | 926 |
; |
42704 | 927 |
@@{command instance} (() | (@{syntax nameref} + @'and') '::' @{syntax arity} | |
928 |
@{syntax nameref} ('<' | '\<subseteq>') @{syntax nameref} ) |
|
31681 | 929 |
; |
59783
00b62aa9f430
tuned syntax diagrams -- no duplication of "target";
wenzelm
parents:
59781
diff
changeset
|
930 |
@@{command subclass} @{syntax nameref} |
58202 | 931 |
; |
59422 | 932 |
@@{command class_deps} ( ( @{syntax sort} | ( '(' ( @{syntax sort} + @'|' ) ')' ) ) \<newline> |
933 |
( @{syntax sort} | ( '(' ( @{syntax sort} + @'|' ) ')' ) )? )? |
|
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
934 |
\<close>} |
27040 | 935 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
936 |
\begin{description} |
27040 | 937 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
938 |
\item @{command "class"}~@{text "c = superclasses + body"} defines |
27040 | 939 |
a new class @{text c}, inheriting from @{text superclasses}. This |
940 |
introduces a locale @{text c} with import of all locales @{text |
|
941 |
superclasses}. |
|
942 |
||
943 |
Any @{element "fixes"} in @{text body} are lifted to the global |
|
944 |
theory level (\emph{class operations} @{text "f\<^sub>1, \<dots>, |
|
945 |
f\<^sub>n"} of class @{text c}), mapping the local type parameter |
|
946 |
@{text \<alpha>} to a schematic type variable @{text "?\<alpha> :: c"}. |
|
947 |
||
948 |
Likewise, @{element "assumes"} in @{text body} are also lifted, |
|
949 |
mapping each local parameter @{text "f :: \<tau>[\<alpha>]"} to its |
|
950 |
corresponding global constant @{text "f :: \<tau>[?\<alpha> :: c]"}. The |
|
951 |
corresponding introduction rule is provided as @{text |
|
952 |
c_class_axioms.intro}. This rule should be rarely needed directly |
|
953 |
--- the @{method intro_classes} method takes care of the details of |
|
954 |
class membership proofs. |
|
955 |
||
28768
a056077b65a1
added section "Co-regularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
956 |
\item @{command "instantiation"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n)s |
51747 | 957 |
\<BEGIN>"} opens a target (cf.\ \secref{sec:target}) which |
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
958 |
allows to specify class operations @{text "f\<^sub>1, \<dots>, f\<^sub>n"} corresponding |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
959 |
to sort @{text s} at the particular type instance @{text "(\<alpha>\<^sub>1 :: s\<^sub>1, |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
960 |
\<dots>, \<alpha>\<^sub>n :: s\<^sub>n) t"}. A plain @{command "instance"} command in the |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
961 |
target body poses a goal stating these type arities. The target is |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
962 |
concluded by an @{command_ref (local) "end"} command. |
27040 | 963 |
|
964 |
Note that a list of simultaneous type constructors may be given; |
|
31914 | 965 |
this corresponds nicely to mutually recursive type definitions, e.g.\ |
27040 | 966 |
in Isabelle/HOL. |
967 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
968 |
\item @{command "instance"} in an instantiation target body sets |
27040 | 969 |
up a goal stating the type arities claimed at the opening @{command |
970 |
"instantiation"}. The proof would usually proceed by @{method |
|
971 |
intro_classes}, and then establish the characteristic theorems of |
|
972 |
the type classes involved. After finishing the proof, the |
|
973 |
background theory will be augmented by the proven type arities. |
|
974 |
||
31681 | 975 |
On the theory level, @{command "instance"}~@{text "t :: (s\<^sub>1, \<dots>, |
976 |
s\<^sub>n)s"} provides a convenient way to instantiate a type class with no |
|
37112 | 977 |
need to specify operations: one can continue with the |
31681 | 978 |
instantiation proof immediately. |
979 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
980 |
\item @{command "subclass"}~@{text c} in a class context for class |
27040 | 981 |
@{text d} sets up a goal stating that class @{text c} is logically |
982 |
contained in class @{text d}. After finishing the proof, class |
|
983 |
@{text d} is proven to be subclass @{text c} and the locale @{text |
|
984 |
c} is interpreted into @{text d} simultaneously. |
|
985 |
||
56594 | 986 |
A weakened form of this is available through a further variant of |
31681 | 987 |
@{command instance}: @{command instance}~@{text "c\<^sub>1 \<subseteq> c\<^sub>2"} opens |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51747
diff
changeset
|
988 |
a proof that class @{text "c\<^sub>2"} implies @{text "c\<^sub>1"} without reference |
31681 | 989 |
to the underlying locales; this is useful if the properties to prove |
56594 | 990 |
the logical connection are not sufficient on the locale level but on |
31681 | 991 |
the theory level. |
992 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
993 |
\item @{command "print_classes"} prints all classes in the current |
27040 | 994 |
theory. |
995 |
||
29706 | 996 |
\item @{command "class_deps"} visualizes all classes and their |
59422 | 997 |
subclass relations as a Hasse diagram. An optional first argument |
998 |
constrains the set of classes to all subclasses of at least one given |
|
999 |
sort, an optional second rgument to all superclasses of at least one given |
|
1000 |
sort. |
|
29706 | 1001 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
1002 |
\item @{method intro_classes} repeatedly expands all class |
27040 | 1003 |
introduction rules of this theory. Note that this method usually |
1004 |
needs not be named explicitly, as it is already included in the |
|
1005 |
default proof step (e.g.\ of @{command "proof"}). In particular, |
|
1006 |
instantiation of trivial (syntactic) classes may be performed by a |
|
1007 |
single ``@{command ".."}'' proof step. |
|
26870 | 1008 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
1009 |
\end{description} |
58618 | 1010 |
\<close> |
26870 | 1011 |
|
27040 | 1012 |
|
58618 | 1013 |
subsection \<open>The class target\<close> |
27040 | 1014 |
|
58618 | 1015 |
text \<open> |
27040 | 1016 |
%FIXME check |
1017 |
||
1018 |
A named context may refer to a locale (cf.\ \secref{sec:target}). |
|
1019 |
If this locale is also a class @{text c}, apart from the common |
|
1020 |
locale target behaviour the following happens. |
|
1021 |
||
1022 |
\begin{itemize} |
|
1023 |
||
1024 |
\item Local constant declarations @{text "g[\<alpha>]"} referring to the |
|
1025 |
local type parameter @{text \<alpha>} and local parameters @{text "f[\<alpha>]"} |
|
1026 |
are accompanied by theory-level constants @{text "g[?\<alpha> :: c]"} |
|
1027 |
referring to theory-level class operations @{text "f[?\<alpha> :: c]"}. |
|
1028 |
||
1029 |
\item Local theorem bindings are lifted as are assumptions. |
|
1030 |
||
1031 |
\item Local syntax refers to local operations @{text "g[\<alpha>]"} and |
|
1032 |
global operations @{text "g[?\<alpha> :: c]"} uniformly. Type inference |
|
1033 |
resolves ambiguities. In rare cases, manual type annotations are |
|
1034 |
needed. |
|
1035 |
||
1036 |
\end{itemize} |
|
58618 | 1037 |
\<close> |
27040 | 1038 |
|
1039 |
||
58618 | 1040 |
subsection \<open>Co-regularity of type classes and arities\<close> |
37768
e86221f3bac7
moved co-regularity to class section; avoid duplicated class_deps
haftmann
parents:
37112
diff
changeset
|
1041 |
|
58618 | 1042 |
text \<open>The class relation together with the collection of |
37768
e86221f3bac7
moved co-regularity to class section; avoid duplicated class_deps
haftmann
parents:
37112
diff
changeset
|
1043 |
type-constructor arities must obey the principle of |
e86221f3bac7
moved co-regularity to class section; avoid duplicated class_deps
haftmann
parents:
37112
diff
changeset
|
1044 |
\emph{co-regularity} as defined below. |
e86221f3bac7
moved co-regularity to class section; avoid duplicated class_deps
haftmann
parents:
37112
diff
changeset
|
1045 |
|
e86221f3bac7
moved co-regularity to class section; avoid duplicated class_deps
haftmann
parents:
37112
diff
changeset
|
1046 |
\medskip For the subsequent formulation of co-regularity we assume |
e86221f3bac7
moved co-regularity to class section; avoid duplicated class_deps
haftmann
parents:
37112
diff
changeset
|
1047 |
that the class relation is closed by transitivity and reflexivity. |
e86221f3bac7
moved co-regularity to class section; avoid duplicated class_deps
haftmann
parents:
37112
diff
changeset
|
1048 |
Moreover the collection of arities @{text "t :: (\<^vec>s)c"} is |
e86221f3bac7
moved co-regularity to class section; avoid duplicated class_deps
haftmann
parents:
37112
diff
changeset
|
1049 |
completed such that @{text "t :: (\<^vec>s)c"} and @{text "c \<subseteq> c'"} |
e86221f3bac7
moved co-regularity to class section; avoid duplicated class_deps
haftmann
parents:
37112
diff
changeset
|
1050 |
implies @{text "t :: (\<^vec>s)c'"} for all such declarations. |
e86221f3bac7
moved co-regularity to class section; avoid duplicated class_deps
haftmann
parents:
37112
diff
changeset
|
1051 |
|
e86221f3bac7
moved co-regularity to class section; avoid duplicated class_deps
haftmann
parents:
37112
diff
changeset
|
1052 |
Treating sorts as finite sets of classes (meaning the intersection), |
e86221f3bac7
moved co-regularity to class section; avoid duplicated class_deps
haftmann
parents:
37112
diff
changeset
|
1053 |
the class relation @{text "c\<^sub>1 \<subseteq> c\<^sub>2"} is extended to sorts as |
e86221f3bac7
moved co-regularity to class section; avoid duplicated class_deps
haftmann
parents:
37112
diff
changeset
|
1054 |
follows: |
e86221f3bac7
moved co-regularity to class section; avoid duplicated class_deps
haftmann
parents:
37112
diff
changeset
|
1055 |
\[ |
e86221f3bac7
moved co-regularity to class section; avoid duplicated class_deps
haftmann
parents:
37112
diff
changeset
|
1056 |
@{text "s\<^sub>1 \<subseteq> s\<^sub>2 \<equiv> \<forall>c\<^sub>2 \<in> s\<^sub>2. \<exists>c\<^sub>1 \<in> s\<^sub>1. c\<^sub>1 \<subseteq> c\<^sub>2"} |
e86221f3bac7
moved co-regularity to class section; avoid duplicated class_deps
haftmann
parents:
37112
diff
changeset
|
1057 |
\] |
e86221f3bac7
moved co-regularity to class section; avoid duplicated class_deps
haftmann
parents:
37112
diff
changeset
|
1058 |
|
e86221f3bac7
moved co-regularity to class section; avoid duplicated class_deps
haftmann
parents:
37112
diff
changeset
|
1059 |
This relation on sorts is further extended to tuples of sorts (of |
e86221f3bac7
moved co-regularity to class section; avoid duplicated class_deps
haftmann
parents:
37112
diff
changeset
|
1060 |
the same length) in the component-wise way. |
e86221f3bac7
moved co-regularity to class section; avoid duplicated class_deps
haftmann
parents:
37112
diff
changeset
|
1061 |
|
e86221f3bac7
moved co-regularity to class section; avoid duplicated class_deps
haftmann
parents:
37112
diff
changeset
|
1062 |
\smallskip Co-regularity of the class relation together with the |
e86221f3bac7
moved co-regularity to class section; avoid duplicated class_deps
haftmann
parents:
37112
diff
changeset
|
1063 |
arities relation means: |
e86221f3bac7
moved co-regularity to class section; avoid duplicated class_deps
haftmann
parents:
37112
diff
changeset
|
1064 |
\[ |
e86221f3bac7
moved co-regularity to class section; avoid duplicated class_deps
haftmann
parents:
37112
diff
changeset
|
1065 |
@{text "t :: (\<^vec>s\<^sub>1)c\<^sub>1 \<Longrightarrow> t :: (\<^vec>s\<^sub>2)c\<^sub>2 \<Longrightarrow> c\<^sub>1 \<subseteq> c\<^sub>2 \<Longrightarrow> \<^vec>s\<^sub>1 \<subseteq> \<^vec>s\<^sub>2"} |
e86221f3bac7
moved co-regularity to class section; avoid duplicated class_deps
haftmann
parents:
37112
diff
changeset
|
1066 |
\] |
e86221f3bac7
moved co-regularity to class section; avoid duplicated class_deps
haftmann
parents:
37112
diff
changeset
|
1067 |
\noindent for all such arities. In other words, whenever the result |
e86221f3bac7
moved co-regularity to class section; avoid duplicated class_deps
haftmann
parents:
37112
diff
changeset
|
1068 |
classes of some type-constructor arities are related, then the |
e86221f3bac7
moved co-regularity to class section; avoid duplicated class_deps
haftmann
parents:
37112
diff
changeset
|
1069 |
argument sorts need to be related in the same way. |
e86221f3bac7
moved co-regularity to class section; avoid duplicated class_deps
haftmann
parents:
37112
diff
changeset
|
1070 |
|
e86221f3bac7
moved co-regularity to class section; avoid duplicated class_deps
haftmann
parents:
37112
diff
changeset
|
1071 |
\medskip Co-regularity is a very fundamental property of the |
e86221f3bac7
moved co-regularity to class section; avoid duplicated class_deps
haftmann
parents:
37112
diff
changeset
|
1072 |
order-sorted algebra of types. For example, it entails principle |
58552 | 1073 |
types and most general unifiers, e.g.\ see @{cite "nipkow-prehofer"}. |
58618 | 1074 |
\<close> |
37768
e86221f3bac7
moved co-regularity to class section; avoid duplicated class_deps
haftmann
parents:
37112
diff
changeset
|
1075 |
|
e86221f3bac7
moved co-regularity to class section; avoid duplicated class_deps
haftmann
parents:
37112
diff
changeset
|
1076 |
|
58618 | 1077 |
section \<open>Unrestricted overloading\<close> |
27040 | 1078 |
|
58618 | 1079 |
text \<open> |
47483 | 1080 |
\begin{matharray}{rcl} |
1081 |
@{command_def "overloading"} & : & @{text "theory \<rightarrow> local_theory"} \\ |
|
1082 |
\end{matharray} |
|
1083 |
||
27040 | 1084 |
Isabelle/Pure's definitional schemes support certain forms of |
31047 | 1085 |
overloading (see \secref{sec:consts}). Overloading means that a |
1086 |
constant being declared as @{text "c :: \<alpha> decl"} may be |
|
1087 |
defined separately on type instances |
|
1088 |
@{text "c :: (\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n) t decl"} |
|
56594 | 1089 |
for each type constructor @{text t}. At most occasions |
27040 | 1090 |
overloading will be used in a Haskell-like fashion together with |
1091 |
type classes by means of @{command "instantiation"} (see |
|
1092 |
\secref{sec:class}). Sometimes low-level overloading is desirable. |
|
1093 |
The @{command "overloading"} target provides a convenient view for |
|
1094 |
end-users. |
|
1095 |
||
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
1096 |
@{rail \<open> |
42704 | 1097 |
@@{command overloading} ( spec + ) @'begin' |
1098 |
; |
|
1099 |
spec: @{syntax name} ( '==' | '\<equiv>' ) @{syntax term} ( '(' @'unchecked' ')' )? |
|
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
1100 |
\<close>} |
27040 | 1101 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
1102 |
\begin{description} |
27040 | 1103 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
1104 |
\item @{command "overloading"}~@{text "x\<^sub>1 \<equiv> c\<^sub>1 :: \<tau>\<^sub>1 \<AND> \<dots> x\<^sub>n \<equiv> c\<^sub>n :: \<tau>\<^sub>n \<BEGIN>"} |
27040 | 1105 |
opens a theory target (cf.\ \secref{sec:target}) which allows to |
1106 |
specify constants with overloaded definitions. These are identified |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
1107 |
by an explicitly given mapping from variable names @{text "x\<^sub>i"} to |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
1108 |
constants @{text "c\<^sub>i"} at particular type instances. The |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
1109 |
definitions themselves are established using common specification |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
1110 |
tools, using the names @{text "x\<^sub>i"} as reference to the |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
1111 |
corresponding constants. The target is concluded by @{command |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
1112 |
(local) "end"}. |
27040 | 1113 |
|
1114 |
A @{text "(unchecked)"} option disables global dependency checks for |
|
1115 |
the corresponding definition, which is occasionally useful for |
|
31047 | 1116 |
exotic overloading (see \secref{sec:consts} for a precise description). |
1117 |
It is at the discretion of the user to avoid |
|
27040 | 1118 |
malformed theory specifications! |
1119 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
1120 |
\end{description} |
58618 | 1121 |
\<close> |
27040 | 1122 |
|
1123 |
||
58618 | 1124 |
section \<open>Incorporating ML code \label{sec:ML}\<close> |
27040 | 1125 |
|
58618 | 1126 |
text \<open> |
27040 | 1127 |
\begin{matharray}{rcl} |
56275
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
55837
diff
changeset
|
1128 |
@{command_def "SML_file"} & : & @{text "theory \<rightarrow> theory"} \\ |
48890
d72ca5742f80
'ML_file' evaluates ML text from a file directly within the theory, without predeclaration via 'uses';
wenzelm
parents:
48824
diff
changeset
|
1129 |
@{command_def "ML_file"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ |
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
1130 |
@{command_def "ML"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
1131 |
@{command_def "ML_prf"} & : & @{text "proof \<rightarrow> proof"} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
1132 |
@{command_def "ML_val"} & : & @{text "any \<rightarrow>"} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
1133 |
@{command_def "ML_command"} & : & @{text "any \<rightarrow>"} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
1134 |
@{command_def "setup"} & : & @{text "theory \<rightarrow> theory"} \\ |
30461 | 1135 |
@{command_def "local_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ |
57941
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57487
diff
changeset
|
1136 |
@{command_def "attribute_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ |
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
1137 |
\end{matharray} |
57478 | 1138 |
\begin{tabular}{rcll} |
1139 |
@{attribute_def ML_print_depth} & : & @{text attribute} & default 10 \\ |
|
1140 |
@{attribute_def ML_source_trace} & : & @{text attribute} & default @{text false} \\ |
|
1141 |
@{attribute_def ML_exception_trace} & : & @{text attribute} & default @{text false} \\ |
|
1142 |
\end{tabular} |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
1143 |
|
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
1144 |
@{rail \<open> |
56275
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
55837
diff
changeset
|
1145 |
(@@{command SML_file} | @@{command ML_file}) @{syntax name} |
27040 | 1146 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
41435
diff
changeset
|
1147 |
(@@{command ML} | @@{command ML_prf} | @@{command ML_val} | |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
41435
diff
changeset
|
1148 |
@@{command ML_command} | @@{command setup} | @@{command local_setup}) @{syntax text} |
27040 | 1149 |
; |
59783
00b62aa9f430
tuned syntax diagrams -- no duplication of "target";
wenzelm
parents:
59781
diff
changeset
|
1150 |
@@{command attribute_setup} @{syntax name} '=' @{syntax text} @{syntax text}? |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
1151 |
\<close>} |
27040 | 1152 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
1153 |
\begin{description} |
27040 | 1154 |
|
56275
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
55837
diff
changeset
|
1155 |
\item @{command "SML_file"}~@{text "name"} reads and evaluates the |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
55837
diff
changeset
|
1156 |
given Standard ML file. Top-level SML bindings are stored within |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
55837
diff
changeset
|
1157 |
the theory context; the initial environment is restricted to the |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
55837
diff
changeset
|
1158 |
Standard ML implementation of Poly/ML, without the many add-ons of |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
55837
diff
changeset
|
1159 |
Isabelle/ML. Multiple @{command "SML_file"} commands may be used to |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
55837
diff
changeset
|
1160 |
build larger Standard ML projects, independently of the regular |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
55837
diff
changeset
|
1161 |
Isabelle/ML environment. |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
55837
diff
changeset
|
1162 |
|
48890
d72ca5742f80
'ML_file' evaluates ML text from a file directly within the theory, without predeclaration via 'uses';
wenzelm
parents:
48824
diff
changeset
|
1163 |
\item @{command "ML_file"}~@{text "name"} reads and evaluates the |
d72ca5742f80
'ML_file' evaluates ML text from a file directly within the theory, without predeclaration via 'uses';
wenzelm
parents:
48824
diff
changeset
|
1164 |
given ML file. The current theory context is passed down to the ML |
d72ca5742f80
'ML_file' evaluates ML text from a file directly within the theory, without predeclaration via 'uses';
wenzelm
parents:
48824
diff
changeset
|
1165 |
toplevel and may be modified, using @{ML "Context.>>"} or derived ML |
d72ca5742f80
'ML_file' evaluates ML text from a file directly within the theory, without predeclaration via 'uses';
wenzelm
parents:
48824
diff
changeset
|
1166 |
commands. Top-level ML bindings are stored within the (global or |
d72ca5742f80
'ML_file' evaluates ML text from a file directly within the theory, without predeclaration via 'uses';
wenzelm
parents:
48824
diff
changeset
|
1167 |
local) theory context. |
27040 | 1168 |
|
48890
d72ca5742f80
'ML_file' evaluates ML text from a file directly within the theory, without predeclaration via 'uses';
wenzelm
parents:
48824
diff
changeset
|
1169 |
\item @{command "ML"}~@{text "text"} is similar to @{command |
d72ca5742f80
'ML_file' evaluates ML text from a file directly within the theory, without predeclaration via 'uses';
wenzelm
parents:
48824
diff
changeset
|
1170 |
"ML_file"}, but evaluates directly the given @{text "text"}. |
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
1171 |
Top-level ML bindings are stored within the (global or local) theory |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
1172 |
context. |
28281 | 1173 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
1174 |
\item @{command "ML_prf"} is analogous to @{command "ML"} but works |
48890
d72ca5742f80
'ML_file' evaluates ML text from a file directly within the theory, without predeclaration via 'uses';
wenzelm
parents:
48824
diff
changeset
|
1175 |
within a proof context. Top-level ML bindings are stored within the |
d72ca5742f80
'ML_file' evaluates ML text from a file directly within the theory, without predeclaration via 'uses';
wenzelm
parents:
48824
diff
changeset
|
1176 |
proof context in a purely sequential fashion, disregarding the |
d72ca5742f80
'ML_file' evaluates ML text from a file directly within the theory, without predeclaration via 'uses';
wenzelm
parents:
48824
diff
changeset
|
1177 |
nested proof structure. ML bindings introduced by @{command |
d72ca5742f80
'ML_file' evaluates ML text from a file directly within the theory, without predeclaration via 'uses';
wenzelm
parents:
48824
diff
changeset
|
1178 |
"ML_prf"} are discarded at the end of the proof. |
27040 | 1179 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
1180 |
\item @{command "ML_val"} and @{command "ML_command"} are diagnostic |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
1181 |
versions of @{command "ML"}, which means that the context may not be |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
1182 |
updated. @{command "ML_val"} echos the bindings produced at the ML |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
1183 |
toplevel, but @{command "ML_command"} is silent. |
27040 | 1184 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
1185 |
\item @{command "setup"}~@{text "text"} changes the current theory |
27040 | 1186 |
context by applying @{text "text"}, which refers to an ML expression |
30461 | 1187 |
of type @{ML_type "theory -> theory"}. This enables to initialize |
1188 |
any object-logic specific tools and packages written in ML, for |
|
1189 |
example. |
|
1190 |
||
1191 |
\item @{command "local_setup"} is similar to @{command "setup"} for |
|
1192 |
a local theory context, and an ML expression of type @{ML_type |
|
1193 |
"local_theory -> local_theory"}. This allows to |
|
1194 |
invoke local theory specification packages without going through |
|
1195 |
concrete outer syntax, for example. |
|
28758 | 1196 |
|
30526 | 1197 |
\item @{command "attribute_setup"}~@{text "name = text description"} |
57941
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57487
diff
changeset
|
1198 |
defines an attribute in the current context. The given @{text |
30526 | 1199 |
"text"} has to be an ML expression of type |
1200 |
@{ML_type "attribute context_parser"}, cf.\ basic parsers defined in |
|
55837 | 1201 |
structure @{ML_structure Args} and @{ML_structure Attrib}. |
30526 | 1202 |
|
1203 |
In principle, attributes can operate both on a given theorem and the |
|
1204 |
implicit context, although in practice only one is modified and the |
|
1205 |
other serves as parameter. Here are examples for these two cases: |
|
1206 |
||
1207 |
\end{description} |
|
58618 | 1208 |
\<close> |
30526 | 1209 |
|
59905 | 1210 |
(*<*)experiment begin(*>*) |
58619 | 1211 |
attribute_setup my_rule = |
1212 |
\<open>Attrib.thms >> (fn ths => |
|
42704 | 1213 |
Thm.rule_attribute |
1214 |
(fn context: Context.generic => fn th: thm => |
|
30526 | 1215 |
let val th' = th OF ths |
58618 | 1216 |
in th' end))\<close> |
30526 | 1217 |
|
58619 | 1218 |
attribute_setup my_declaration = |
1219 |
\<open>Attrib.thms >> (fn ths => |
|
42704 | 1220 |
Thm.declaration_attribute |
1221 |
(fn th: thm => fn context: Context.generic => |
|
30526 | 1222 |
let val context' = context |
58618 | 1223 |
in context' end))\<close> |
59905 | 1224 |
(*<*)end(*>*) |
30526 | 1225 |
|
58618 | 1226 |
text \<open> |
57478 | 1227 |
\begin{description} |
1228 |
||
1229 |
\item @{attribute ML_print_depth} controls the printing depth of the ML |
|
1230 |
toplevel pretty printer; the precise effect depends on the ML compiler and |
|
1231 |
run-time system. Typically the limit should be less than 10. Bigger values |
|
1232 |
such as 100--1000 are occasionally useful for debugging. |
|
1233 |
||
1234 |
\item @{attribute ML_source_trace} indicates whether the source text that |
|
1235 |
is given to the ML compiler should be output: it shows the raw Standard ML |
|
1236 |
after expansion of Isabelle/ML antiquotations. |
|
1237 |
||
1238 |
\item @{attribute ML_exception_trace} indicates whether the ML run-time |
|
1239 |
system should print a detailed stack trace on exceptions. The result is |
|
1240 |
dependent on the particular ML compiler version. Note that after Poly/ML |
|
1241 |
5.3 some optimizations in the run-time systems may hinder exception |
|
1242 |
traces. |
|
1243 |
||
1244 |
The boundary for the exception trace is the current Isar command |
|
1245 |
transactions. It is occasionally better to insert the combinator @{ML |
|
58552 | 1246 |
Runtime.exn_trace} into ML code for debugging @{cite |
1247 |
"isabelle-implementation"}, closer to the point where it actually |
|
57478 | 1248 |
happens. |
1249 |
||
1250 |
\end{description} |
|
58618 | 1251 |
\<close> |
57478 | 1252 |
|
27040 | 1253 |
|
58618 | 1254 |
section \<open>Primitive specification elements\<close> |
27040 | 1255 |
|
58618 | 1256 |
subsection \<open>Sorts\<close> |
27040 | 1257 |
|
58618 | 1258 |
text \<open> |
27040 | 1259 |
\begin{matharray}{rcll} |
37768
e86221f3bac7
moved co-regularity to class section; avoid duplicated class_deps
haftmann
parents:
37112
diff
changeset
|
1260 |
@{command_def "default_sort"} & : & @{text "local_theory \<rightarrow> local_theory"} |
27040 | 1261 |
\end{matharray} |
1262 |
||
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
1263 |
@{rail \<open> |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
41435
diff
changeset
|
1264 |
@@{command default_sort} @{syntax sort} |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
1265 |
\<close>} |
27040 | 1266 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
1267 |
\begin{description} |
27040 | 1268 |
|
36454
f2b5bcc61a8c
command 'defaultsort' is renamed to 'default_sort', it works within a local theory context;
wenzelm
parents:
36178
diff
changeset
|
1269 |
\item @{command "default_sort"}~@{text s} makes sort @{text s} the |
28767 | 1270 |
new default sort for any type variable that is given explicitly in |
1271 |
the text, but lacks a sort constraint (wrt.\ the current context). |
|
1272 |
Type variables generated by type inference are not affected. |
|
1273 |
||
1274 |
Usually the default sort is only changed when defining a new |
|
1275 |
object-logic. For example, the default sort in Isabelle/HOL is |
|
39831 | 1276 |
@{class type}, the class of all HOL types. |
28767 | 1277 |
|
1278 |
When merging theories, the default sorts of the parents are |
|
1279 |
logically intersected, i.e.\ the representations as lists of classes |
|
1280 |
are joined. |
|
27040 | 1281 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
1282 |
\end{description} |
58618 | 1283 |
\<close> |
27040 | 1284 |
|
1285 |
||
58618 | 1286 |
subsection \<open>Types \label{sec:types-pure}\<close> |
27040 | 1287 |
|
58618 | 1288 |
text \<open> |
27040 | 1289 |
\begin{matharray}{rcll} |
41249
26f12f98f50a
Command 'type_synonym' (with single argument) supersedes 'types' (legacy feature);
wenzelm
parents:
40800
diff
changeset
|
1290 |
@{command_def "type_synonym"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ |
35681 | 1291 |
@{command_def "typedecl"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ |
27040 | 1292 |
\end{matharray} |
1293 |
||
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
1294 |
@{rail \<open> |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
41435
diff
changeset
|
1295 |
@@{command type_synonym} (@{syntax typespec} '=' @{syntax type} @{syntax mixfix}?) |
27040 | 1296 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
41435
diff
changeset
|
1297 |
@@{command typedecl} @{syntax typespec} @{syntax mixfix}? |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
1298 |
\<close>} |
27040 | 1299 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
1300 |
\begin{description} |
27040 | 1301 |
|
57487 | 1302 |
\item @{command "type_synonym"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = \<tau>"} introduces a |
1303 |
\emph{type synonym} @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} for the existing type @{text |
|
1304 |
"\<tau>"}. Unlike the semantic type definitions in Isabelle/HOL, type synonyms |
|
1305 |
are merely syntactic abbreviations without any logical significance. |
|
41249
26f12f98f50a
Command 'type_synonym' (with single argument) supersedes 'types' (legacy feature);
wenzelm
parents:
40800
diff
changeset
|
1306 |
Internally, type synonyms are fully expanded. |
27040 | 1307 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
1308 |
\item @{command "typedecl"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} declares a new |
28767 | 1309 |
type constructor @{text t}. If the object-logic defines a base sort |
1310 |
@{text s}, then the constructor is declared to operate on that, via |
|
55385
169e12bbf9a3
discontinued axiomatic 'classes', 'classrel', 'arities';
wenzelm
parents:
55117
diff
changeset
|
1311 |
the axiomatic type-class instance @{text "t :: (s, \<dots>, s)s"}. |
27040 | 1312 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
1313 |
\end{description} |
57487 | 1314 |
|
1315 |
\begin{warn} |
|
1316 |
If you introduce a new type axiomatically, i.e.\ via @{command_ref |
|
1317 |
typedecl} and @{command_ref axiomatization} |
|
1318 |
(\secref{sec:axiomatizations}), the minimum requirement is that it has a |
|
1319 |
non-empty model, to avoid immediate collapse of the logical environment. |
|
1320 |
Moreover, one needs to demonstrate that the interpretation of such |
|
1321 |
free-form axiomatizations can coexist with other axiomatization schemes |
|
1322 |
for types, notably @{command_def typedef} in Isabelle/HOL |
|
1323 |
(\secref{sec:hol-typedef}), or any other extension that people might have |
|
1324 |
introduced elsewhere. |
|
1325 |
\end{warn} |
|
58618 | 1326 |
\<close> |
27040 | 1327 |
|
1328 |
||
58618 | 1329 |
subsection \<open>Constants and definitions \label{sec:consts}\<close> |
27040 | 1330 |
|
58618 | 1331 |
text \<open> |
47483 | 1332 |
\begin{matharray}{rcl} |
1333 |
@{command_def "consts"} & : & @{text "theory \<rightarrow> theory"} \\ |
|
1334 |
@{command_def "defs"} & : & @{text "theory \<rightarrow> theory"} \\ |
|
1335 |
\end{matharray} |
|
1336 |
||
27040 | 1337 |
Definitions essentially express abbreviations within the logic. The |
1338 |
simplest form of a definition is @{text "c :: \<sigma> \<equiv> t"}, where @{text |
|
1339 |
c} is a newly declared constant. Isabelle also allows derived forms |
|
1340 |
where the arguments of @{text c} appear on the left, abbreviating a |
|
1341 |
prefix of @{text \<lambda>}-abstractions, e.g.\ @{text "c \<equiv> \<lambda>x y. t"} may be |
|
1342 |
written more conveniently as @{text "c x y \<equiv> t"}. Moreover, |
|
1343 |
definitions may be weakened by adding arbitrary pre-conditions: |
|
1344 |
@{text "A \<Longrightarrow> c x y \<equiv> t"}. |
|
1345 |
||
1346 |
\medskip The built-in well-formedness conditions for definitional |
|
1347 |
specifications are: |
|
1348 |
||
1349 |
\begin{itemize} |
|
1350 |
||
1351 |
\item Arguments (on the left-hand side) must be distinct variables. |
|
1352 |
||
1353 |
\item All variables on the right-hand side must also appear on the |
|
1354 |
left-hand side. |
|
1355 |
||
1356 |
\item All type variables on the right-hand side must also appear on |
|
1357 |
the left-hand side; this prohibits @{text "0 :: nat \<equiv> length ([] :: |
|
1358 |
\<alpha> list)"} for example. |
|
1359 |
||
1360 |
\item The definition must not be recursive. Most object-logics |
|
1361 |
provide definitional principles that can be used to express |
|
1362 |
recursion safely. |
|
1363 |
||
1364 |
\end{itemize} |
|
1365 |
||
31047 | 1366 |
The right-hand side of overloaded definitions may mention overloaded constants |
27040 | 1367 |
recursively at type instances corresponding to the immediate |
1368 |
argument types @{text "\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n"}. Incomplete |
|
1369 |
specification patterns impose global constraints on all occurrences, |
|
1370 |
e.g.\ @{text "d :: \<alpha> \<times> \<alpha>"} on the left-hand side means that all |
|
1371 |
corresponding occurrences on some right-hand side need to be an |
|
1372 |
instance of this, general @{text "d :: \<alpha> \<times> \<beta>"} will be disallowed. |
|
1373 |
||
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
1374 |
@{rail \<open> |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
41435
diff
changeset
|
1375 |
@@{command consts} ((@{syntax name} '::' @{syntax type} @{syntax mixfix}?) +) |
27040 | 1376 |
; |
42704 | 1377 |
@@{command defs} opt? (@{syntax axmdecl} @{syntax prop} +) |
1378 |
; |
|
1379 |
opt: '(' @'unchecked'? @'overloaded'? ')' |
|
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
1380 |
\<close>} |
27040 | 1381 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
1382 |
\begin{description} |
27040 | 1383 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
1384 |
\item @{command "consts"}~@{text "c :: \<sigma>"} declares constant @{text |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
1385 |
c} to have any instance of type scheme @{text \<sigma>}. The optional |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
1386 |
mixfix annotations may attach concrete syntax to the constants |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
1387 |
declared. |
27040 | 1388 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
1389 |
\item @{command "defs"}~@{text "name: eqn"} introduces @{text eqn} |
27040 | 1390 |
as a definitional axiom for some existing constant. |
1391 |
||
1392 |
The @{text "(unchecked)"} option disables global dependency checks |
|
1393 |
for this definition, which is occasionally useful for exotic |
|
1394 |
overloading. It is at the discretion of the user to avoid malformed |
|
1395 |
theory specifications! |
|
1396 |
||
1397 |
The @{text "(overloaded)"} option declares definitions to be |
|
1398 |
potentially overloaded. Unless this option is given, a warning |
|
1399 |
message would be issued for any definitional equation with a more |
|
1400 |
special type than that of the corresponding constant declaration. |
|
1401 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
1402 |
\end{description} |
58618 | 1403 |
\<close> |
27040 | 1404 |
|
1405 |
||
58618 | 1406 |
section \<open>Naming existing theorems \label{sec:theorems}\<close> |
27040 | 1407 |
|
58618 | 1408 |
text \<open> |
27040 | 1409 |
\begin{matharray}{rcll} |
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
1410 |
@{command_def "lemmas"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
1411 |
@{command_def "theorems"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ |
57946
6a26aa5fa65e
updated documentation concerning 'named_theorems';
wenzelm
parents:
57941
diff
changeset
|
1412 |
@{command_def "named_theorems"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ |
27040 | 1413 |
\end{matharray} |
1414 |
||
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
1415 |
@{rail \<open> |
59785 | 1416 |
(@@{command lemmas} | @@{command theorems}) (@{syntax thmdef}? @{syntax thmrefs} + @'and') |
1417 |
@{syntax for_fixes} |
|
57946
6a26aa5fa65e
updated documentation concerning 'named_theorems';
wenzelm
parents:
57941
diff
changeset
|
1418 |
; |
59785 | 1419 |
@@{command named_theorems} (@{syntax name} @{syntax text}? + @'and') |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
1420 |
\<close>} |
27040 | 1421 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
1422 |
\begin{description} |
27040 | 1423 |
|
45600
1bbbac9a0cb0
'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
wenzelm
parents:
42936
diff
changeset
|
1424 |
\item @{command "lemmas"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"}~@{keyword_def |
1bbbac9a0cb0
'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
wenzelm
parents:
42936
diff
changeset
|
1425 |
"for"}~@{text "x\<^sub>1 \<dots> x\<^sub>m"} evaluates given facts (with attributes) in |
1bbbac9a0cb0
'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
wenzelm
parents:
42936
diff
changeset
|
1426 |
the current context, which may be augmented by local variables. |
1bbbac9a0cb0
'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
wenzelm
parents:
42936
diff
changeset
|
1427 |
Results are standardized before being stored, i.e.\ schematic |
1bbbac9a0cb0
'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
wenzelm
parents:
42936
diff
changeset
|
1428 |
variables are renamed to enforce index @{text "0"} uniformly. |
1bbbac9a0cb0
'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
wenzelm
parents:
42936
diff
changeset
|
1429 |
|
1bbbac9a0cb0
'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
wenzelm
parents:
42936
diff
changeset
|
1430 |
\item @{command "theorems"} is the same as @{command "lemmas"}, but |
1bbbac9a0cb0
'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
wenzelm
parents:
42936
diff
changeset
|
1431 |
marks the result as a different kind of facts. |
27040 | 1432 |
|
57946
6a26aa5fa65e
updated documentation concerning 'named_theorems';
wenzelm
parents:
57941
diff
changeset
|
1433 |
\item @{command "named_theorems"}~@{text "name description"} declares a |
6a26aa5fa65e
updated documentation concerning 'named_theorems';
wenzelm
parents:
57941
diff
changeset
|
1434 |
dynamic fact within the context. The same @{text name} is used to define |
6a26aa5fa65e
updated documentation concerning 'named_theorems';
wenzelm
parents:
57941
diff
changeset
|
1435 |
an attribute with the usual @{text add}/@{text del} syntax (e.g.\ see |
6a26aa5fa65e
updated documentation concerning 'named_theorems';
wenzelm
parents:
57941
diff
changeset
|
1436 |
\secref{sec:simp-rules}) to maintain the content incrementally, in |
6a26aa5fa65e
updated documentation concerning 'named_theorems';
wenzelm
parents:
57941
diff
changeset
|
1437 |
canonical declaration order of the text structure. |
6a26aa5fa65e
updated documentation concerning 'named_theorems';
wenzelm
parents:
57941
diff
changeset
|
1438 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
1439 |
\end{description} |
58618 | 1440 |
\<close> |
27040 | 1441 |
|
1442 |
||
58618 | 1443 |
section \<open>Oracles\<close> |
27040 | 1444 |
|
58618 | 1445 |
text \<open> |
47483 | 1446 |
\begin{matharray}{rcll} |
1447 |
@{command_def "oracle"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\ |
|
1448 |
\end{matharray} |
|
1449 |
||
1450 |
Oracles allow Isabelle to take advantage of external reasoners such |
|
1451 |
as arithmetic decision procedures, model checkers, fast tautology |
|
1452 |
checkers or computer algebra systems. Invoked as an oracle, an |
|
1453 |
external reasoner can create arbitrary Isabelle theorems. |
|
28756 | 1454 |
|
1455 |
It is the responsibility of the user to ensure that the external |
|
1456 |
reasoner is as trustworthy as the application requires. Another |
|
1457 |
typical source of errors is the linkup between Isabelle and the |
|
1458 |
external tool, not just its concrete implementation, but also the |
|
1459 |
required translation between two different logical environments. |
|
1460 |
||
1461 |
Isabelle merely guarantees well-formedness of the propositions being |
|
1462 |
asserted, and records within the internal derivation object how |
|
1463 |
presumed theorems depend on unproven suppositions. |
|
1464 |
||
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
1465 |
@{rail \<open> |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
41435
diff
changeset
|
1466 |
@@{command oracle} @{syntax name} '=' @{syntax text} |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
1467 |
\<close>} |
27040 | 1468 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
1469 |
\begin{description} |
27040 | 1470 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
1471 |
\item @{command "oracle"}~@{text "name = text"} turns the given ML |
28290 | 1472 |
expression @{text "text"} of type @{ML_text "'a -> cterm"} into an |
1473 |
ML function of type @{ML_text "'a -> thm"}, which is bound to the |
|
28756 | 1474 |
global identifier @{ML_text name}. This acts like an infinitary |
1475 |
specification of axioms! Invoking the oracle only works within the |
|
1476 |
scope of the resulting theory. |
|
27040 | 1477 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
1478 |
\end{description} |
28756 | 1479 |
|
40800
330eb65c9469
Parse.liberal_name for document antiquotations and attributes;
wenzelm
parents:
40784
diff
changeset
|
1480 |
See @{file "~~/src/HOL/ex/Iff_Oracle.thy"} for a worked example of |
28756 | 1481 |
defining a new primitive rule as oracle, and turning it into a proof |
1482 |
method. |
|
58618 | 1483 |
\<close> |
27040 | 1484 |
|
1485 |
||
58618 | 1486 |
section \<open>Name spaces\<close> |
27040 | 1487 |
|
58618 | 1488 |
text \<open> |
27040 | 1489 |
\begin{matharray}{rcl} |
36177
8e0770d2e499
separate commands 'hide_class', 'hide_type', 'hide_const', 'hide_fact';
wenzelm
parents:
35681
diff
changeset
|
1490 |
@{command_def "hide_class"} & : & @{text "theory \<rightarrow> theory"} \\ |
8e0770d2e499
separate commands 'hide_class', 'hide_type', 'hide_const', 'hide_fact';
wenzelm
parents:
35681
diff
changeset
|
1491 |
@{command_def "hide_type"} & : & @{text "theory \<rightarrow> theory"} \\ |
8e0770d2e499
separate commands 'hide_class', 'hide_type', 'hide_const', 'hide_fact';
wenzelm
parents:
35681
diff
changeset
|
1492 |
@{command_def "hide_const"} & : & @{text "theory \<rightarrow> theory"} \\ |
8e0770d2e499
separate commands 'hide_class', 'hide_type', 'hide_const', 'hide_fact';
wenzelm
parents:
35681
diff
changeset
|
1493 |
@{command_def "hide_fact"} & : & @{text "theory \<rightarrow> theory"} \\ |
27040 | 1494 |
\end{matharray} |
1495 |
||
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
1496 |
@{rail \<open> |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
41435
diff
changeset
|
1497 |
( @{command hide_class} | @{command hide_type} | |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
41435
diff
changeset
|
1498 |
@{command hide_const} | @{command hide_fact} ) ('(' @'open' ')')? (@{syntax nameref} + ) |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
1499 |
\<close>} |
27040 | 1500 |
|
1501 |
Isabelle organizes any kind of name declarations (of types, |
|
1502 |
constants, theorems etc.) by separate hierarchically structured name |
|
1503 |
spaces. Normally the user does not have to control the behavior of |
|
1504 |
name spaces by hand, yet the following commands provide some way to |
|
1505 |
do so. |
|
1506 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
1507 |
\begin{description} |
27040 | 1508 |
|
36177
8e0770d2e499
separate commands 'hide_class', 'hide_type', 'hide_const', 'hide_fact';
wenzelm
parents:
35681
diff
changeset
|
1509 |
\item @{command "hide_class"}~@{text names} fully removes class |
8e0770d2e499
separate commands 'hide_class', 'hide_type', 'hide_const', 'hide_fact';
wenzelm
parents:
35681
diff
changeset
|
1510 |
declarations from a given name space; with the @{text "(open)"} |
39977
c9cbc16e93ce
do not mention unqualified names, now that 'global' and 'local' are gone
krauss
parents:
39214
diff
changeset
|
1511 |
option, only the base name is hidden. |
36177
8e0770d2e499
separate commands 'hide_class', 'hide_type', 'hide_const', 'hide_fact';
wenzelm
parents:
35681
diff
changeset
|
1512 |
|
27040 | 1513 |
Note that hiding name space accesses has no impact on logical |
28756 | 1514 |
declarations --- they remain valid internally. Entities that are no |
27040 | 1515 |
longer accessible to the user are printed with the special qualifier |
1516 |
``@{text "??"}'' prefixed to the full internal name. |
|
1517 |
||
36177
8e0770d2e499
separate commands 'hide_class', 'hide_type', 'hide_const', 'hide_fact';
wenzelm
parents:
35681
diff
changeset
|
1518 |
\item @{command "hide_type"}, @{command "hide_const"}, and @{command |
8e0770d2e499
separate commands 'hide_class', 'hide_type', 'hide_const', 'hide_fact';
wenzelm
parents:
35681
diff
changeset
|
1519 |
"hide_fact"} are similar to @{command "hide_class"}, but hide types, |
8e0770d2e499
separate commands 'hide_class', 'hide_type', 'hide_const', 'hide_fact';
wenzelm
parents:
35681
diff
changeset
|
1520 |
constants, and facts, respectively. |
8e0770d2e499
separate commands 'hide_class', 'hide_type', 'hide_const', 'hide_fact';
wenzelm
parents:
35681
diff
changeset
|
1521 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
1522 |
\end{description} |
58618 | 1523 |
\<close> |
27040 | 1524 |
|
26869 | 1525 |
end |