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