author  wenzelm 
Mon, 16 Mar 2009 17:48:02 +0100  
changeset 30546  b3b1f4184ae4 
parent 30526  7f9a9ec1c94d 
child 31047  c13b0406c039 
permissions  rwrr 
26869  1 
theory Spec 
2 
imports Main 

3 
begin 

4 

27046  5 
chapter {* Theory specifications *} 
26869  6 

29745  7 
text {* 
8 
The Isabelle/Isar theory format integrates specifications and 

9 
proofs, supporting interactive development with unlimited undo 

10 
operation. There is an integrated document preparation system (see 

11 
\chref{ch:documentprep}), for typesetting formal developments 

12 
together with informal text. The resulting hyperlinked PDF 

13 
documents can be used both for WWW presentation and printed copies. 

14 

15 
The Isar proof language (see \chref{ch:proofs}) is embedded into the 

16 
theory language as a proper sublanguage. Proof mode is entered by 

17 
stating some @{command theorem} or @{command lemma} at the theory 

18 
level, and left again with the final conclusion (e.g.\ via @{command 

19 
qed}). Some theory specification mechanisms also require a proof, 

20 
such as @{command typedef} in HOL, which demands nonemptiness of 

21 
the representing sets. 

22 
*} 

23 

24 

26870  25 
section {* Defining theories \label{sec:beginthy} *} 
26 

27 
text {* 

28 
\begin{matharray}{rcl} 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

29 
@{command_def "theory"} & : & @{text "toplevel \<rightarrow> theory"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

30 
@{command_def (global) "end"} & : & @{text "theory \<rightarrow> toplevel"} \\ 
26870  31 
\end{matharray} 
32 

28745  33 
Isabelle/Isar theories are defined via theory files, which may 
34 
contain both specifications and proofs; occasionally definitional 

35 
mechanisms also require some explicit proof. The theory body may be 

36 
substructured by means of \emph{local theory targets}, such as 

37 
@{command "locale"} and @{command "class"}. 

26870  38 

28745  39 
The first proper command of a theory is @{command "theory"}, which 
40 
indicates imports of previous theories and optional dependencies on 

41 
other source files (usually in ML). Just preceding the initial 

42 
@{command "theory"} command there may be an optional @{command 

43 
"header"} declaration, which is only relevant to document 

44 
preparation: see also the other section markup commands in 

45 
\secref{sec:markup}. 

46 

47 
A theory is concluded by a final @{command (global) "end"} command, 

48 
one that does not belong to a local theory target. No further 

49 
commands may follow such a global @{command (global) "end"}, 

50 
although some userinterfaces might pretend that trailing input is 

51 
admissible. 

26870  52 

53 
\begin{rail} 

54 
'theory' name 'imports' (name +) uses? 'begin' 

55 
; 

56 

57 
uses: 'uses' ((name  parname) +); 

58 
\end{rail} 

59 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

60 
\begin{description} 
26870  61 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

62 
\item @{command "theory"}~@{text "A \<IMPORTS> B\<^sub>1 \<dots> B\<^sub>n \<BEGIN>"} 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

63 
starts a new theory @{text A} based on the merge of existing 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

64 
theories @{text "B\<^sub>1 \<dots> B\<^sub>n"}. 
26870  65 

28745  66 
Due to the possibility to import more than one ancestor, the 
67 
resulting theory structure of an Isabelle session forms a directed 

68 
acyclic graph (DAG). Isabelle's theory loader ensures that the 

69 
sources contributing to the development graph are always uptodate: 

70 
changed files are automatically reloaded whenever a theory header 

71 
specification is processed. 

26870  72 

73 
The optional @{keyword_def "uses"} specification declares additional 

74 
dependencies on extra files (usually ML sources). Files will be 

28745  75 
loaded immediately (as ML), unless the name is parenthesized. The 
76 
latter case records a dependency that needs to be resolved later in 

77 
the text, usually via explicit @{command_ref "use"} for ML files; 

78 
other file formats require specific load commands defined by the 

79 
corresponding tools or packages. 

26870  80 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

81 
\item @{command (global) "end"} concludes the current theory 
28745  82 
definition. Note that local theory targets involve a local 
83 
@{command (local) "end"}, which is clear from the nesting. 

27040  84 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

85 
\end{description} 
27040  86 
*} 
87 

88 

89 
section {* Local theory targets \label{sec:target} *} 

90 

91 
text {* 

92 
A local theory target is a context managed separately within the 

93 
enclosing theory. Contexts may introduce parameters (fixed 

94 
variables) and assumptions (hypotheses). Definitions and theorems 

95 
depending on the context may be added incrementally later on. Named 

96 
contexts refer to locales (cf.\ \secref{sec:locale}) or type classes 

97 
(cf.\ \secref{sec:class}); the name ``@{text ""}'' signifies the 

98 
global theory context. 

99 

100 
\begin{matharray}{rcll} 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

101 
@{command_def "context"} & : & @{text "theory \<rightarrow> local_theory"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

102 
@{command_def (local) "end"} & : & @{text "local_theory \<rightarrow> theory"} \\ 
27040  103 
\end{matharray} 
104 

105 
\indexouternonterm{target} 

106 
\begin{rail} 

107 
'context' name 'begin' 

108 
; 

109 

110 
target: '(' 'in' name ')' 

111 
; 

112 
\end{rail} 

113 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

114 
\begin{description} 
27040  115 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

116 
\item @{command "context"}~@{text "c \<BEGIN>"} recommences an 
27040  117 
existing locale or class context @{text c}. Note that locale and 
27051  118 
class definitions allow to include the @{keyword "begin"} keyword as 
119 
well, in order to continue the local theory immediately after the 

120 
initial specification. 

27040  121 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

122 
\item @{command (local) "end"} concludes the current local theory 
27040  123 
and continues the enclosing global theory. Note that a global 
124 
@{command (global) "end"} has a different meaning: it concludes the 

125 
theory itself (\secref{sec:beginthy}). 

126 

29745  127 
\item @{text "("}@{keyword_def "in"}~@{text "c)"} given after any 
128 
local theory command specifies an immediate target, e.g.\ 

129 
``@{command "definition"}~@{text "(\<IN> c) \<dots>"}'' or ``@{command 

27040  130 
"theorem"}~@{text "(\<IN> c) \<dots>"}''. This works both in a local or 
131 
global theory context; the current target context will be suspended 

132 
for this command only. Note that ``@{text "(\<IN> )"}'' will 

133 
always produce a global result independently of the current target 

134 
context. 

135 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

136 
\end{description} 
27040  137 

138 
The exact meaning of results produced within a local theory context 

139 
depends on the underlying target infrastructure (locale, type class 

140 
etc.). The general idea is as follows, considering a context named 

141 
@{text c} with parameter @{text x} and assumption @{text "A[x]"}. 

142 

143 
Definitions are exported by introducing a global version with 

144 
additional arguments; a syntactic abbreviation links the long form 

145 
with the abstract version of the target context. For example, 

146 
@{text "a \<equiv> t[x]"} becomes @{text "c.a ?x \<equiv> t[?x]"} at the theory 

147 
level (for arbitrary @{text "?x"}), together with a local 

148 
abbreviation @{text "c \<equiv> c.a x"} in the target context (for the 

149 
fixed parameter @{text x}). 

150 

151 
Theorems are exported by discharging the assumptions and 

152 
generalizing the parameters of the context. For example, @{text "a: 

153 
B[x]"} becomes @{text "c.a: A[?x] \<Longrightarrow> B[?x]"}, again for arbitrary 

154 
@{text "?x"}. 

155 
*} 

156 

157 

158 
section {* Basic specification elements *} 

159 

160 
text {* 

161 
\begin{matharray}{rcll} 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

162 
@{command_def "axiomatization"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!)\\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

163 
@{command_def "definition"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

164 
@{attribute_def "defn"} & : & @{text attribute} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

165 
@{command_def "abbreviation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

166 
@{command_def "print_abbrevs"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow> "} \\ 
27040  167 
\end{matharray} 
168 

169 
These specification mechanisms provide a slightly more abstract view 

170 
than the underlying primitives of @{command "consts"}, @{command 

171 
"defs"} (see \secref{sec:consts}), and @{command "axioms"} (see 

172 
\secref{sec:axmsthms}). In particular, typeinference is commonly 

173 
available, and result names need not be given. 

174 

175 
\begin{rail} 

176 
'axiomatization' target? fixes? ('where' specs)? 

177 
; 

178 
'definition' target? (decl 'where')? thmdecl? prop 

179 
; 

180 
'abbreviation' target? mode? (decl 'where')? prop 

181 
; 

182 

183 
fixes: ((name ('::' type)? mixfix?  vars) + 'and') 

184 
; 

185 
specs: (thmdecl? props + 'and') 

186 
; 

187 
decl: name ('::' type)? mixfix? 

188 
; 

189 
\end{rail} 

190 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

191 
\begin{description} 
27040  192 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

193 
\item @{command "axiomatization"}~@{text "c\<^sub>1 \<dots> c\<^sub>m \<WHERE> \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

194 
introduces several constants simultaneously and states axiomatic 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

195 
properties for these. The constants are marked as being specified 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

196 
once and for all, which prevents additional specifications being 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

197 
issued later on. 
27040  198 

199 
Note that axiomatic specifications are only appropriate when 

28114  200 
declaring a new logical system; axiomatic specifications are 
201 
restricted to global theory contexts. Normal applications should 

202 
only use definitional mechanisms! 

27040  203 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

204 
\item @{command "definition"}~@{text "c \<WHERE> eq"} produces an 
27040  205 
internal definition @{text "c \<equiv> t"} according to the specification 
206 
given as @{text eq}, which is then turned into a proven fact. The 

207 
given proposition may deviate from internal metalevel equality 

208 
according to the rewrite rules declared as @{attribute defn} by the 

209 
objectlogic. This usually covers objectlevel equality @{text "x = 

210 
y"} and equivalence @{text "A \<leftrightarrow> B"}. Endusers normally need not 

211 
change the @{attribute defn} setup. 

212 

213 
Definitions may be presented with explicit arguments on the LHS, as 

214 
well as additional conditions, e.g.\ @{text "f x y = t"} instead of 

215 
@{text "f \<equiv> \<lambda>x y. t"} and @{text "y \<noteq> 0 \<Longrightarrow> g x y = u"} instead of an 

216 
unrestricted @{text "g \<equiv> \<lambda>x y. u"}. 

217 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

218 
\item @{command "abbreviation"}~@{text "c \<WHERE> eq"} introduces a 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

219 
syntactic constant which is associated with a certain term according 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

220 
to the metalevel equality @{text eq}. 
27040  221 

222 
Abbreviations participate in the usual typeinference process, but 

223 
are expanded before the logic ever sees them. Pretty printing of 

224 
terms involves higherorder rewriting with rules stemming from 

225 
reverted abbreviations. This needs some care to avoid overlapping 

226 
or looping syntactic replacements! 

227 

228 
The optional @{text mode} specification restricts output to a 

229 
particular print mode; using ``@{text input}'' here achieves the 

230 
effect of oneway abbreviations. The mode may also include an 

231 
``@{keyword "output"}'' qualifier that affects the concrete syntax 

232 
declared for abbreviations, cf.\ @{command "syntax"} in 

233 
\secref{sec:syntrans}. 

234 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

235 
\item @{command "print_abbrevs"} prints all constant abbreviations 
27040  236 
of the current context. 
237 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

238 
\end{description} 
27040  239 
*} 
240 

241 

242 
section {* Generic declarations *} 

243 

244 
text {* 

245 
Arbitrary operations on the background context may be wrappedup as 

246 
generic declaration elements. Since the underlying concept of local 

247 
theories may be subject to later reinterpretation, there is an 

248 
additional dependency on a morphism that tells the difference of the 

249 
original declaration context wrt.\ the application context 

250 
encountered later on. A fact declaration is an important special 

251 
case: it consists of a theorem which is applied to the context by 

252 
means of an attribute. 

253 

254 
\begin{matharray}{rcl} 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

255 
@{command_def "declaration"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

256 
@{command_def "declare"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ 
27040  257 
\end{matharray} 
258 

259 
\begin{rail} 

260 
'declaration' target? text 

261 
; 

262 
'declare' target? (thmrefs + 'and') 

263 
; 

264 
\end{rail} 

265 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

266 
\begin{description} 
27040  267 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

268 
\item @{command "declaration"}~@{text d} adds the declaration 
27040  269 
function @{text d} of ML type @{ML_type declaration}, to the current 
270 
local theory under construction. In later application contexts, the 

271 
function is transformed according to the morphisms being involved in 

272 
the interpretation hierarchy. 

273 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

274 
\item @{command "declare"}~@{text thms} declares theorems to the 
27040  275 
current local theory context. No theorem binding is involved here, 
276 
unlike @{command "theorems"} or @{command "lemmas"} (cf.\ 

277 
\secref{sec:axmsthms}), so @{command "declare"} only has the effect 

278 
of applying attributes as included in the theorem specification. 

279 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

280 
\end{description} 
27040  281 
*} 
282 

283 

284 
section {* Locales \label{sec:locale} *} 

285 

286 
text {* 

287 
Locales are named local contexts, consisting of a list of 

288 
declaration elements that are modeled after the Isar proof context 

289 
commands (cf.\ \secref{sec:proofcontext}). 

290 
*} 

291 

292 

293 
subsection {* Locale specifications *} 

294 

295 
text {* 

296 
\begin{matharray}{rcl} 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

297 
@{command_def "locale"} & : & @{text "theory \<rightarrow> local_theory"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

298 
@{command_def "print_locale"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

299 
@{command_def "print_locales"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

300 
@{method_def intro_locales} & : & @{text method} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

301 
@{method_def unfold_locales} & : & @{text method} \\ 
27040  302 
\end{matharray} 
303 

304 
\indexouternonterm{contextexpr}\indexouternonterm{contextelem} 

305 
\indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes} 

28787  306 
\indexisarelem{defines}\indexisarelem{notes} 
27040  307 
\begin{rail} 
27681  308 
'locale' name ('=' localeexpr)? 'begin'? 
27040  309 
; 
310 
'print\_locale' '!'? localeexpr 

311 
; 

312 
localeexpr: ((contextexpr '+' (contextelem+))  contextexpr  (contextelem+)) 

313 
; 

314 

315 
contextexpr: nameref  '(' contextexpr ')'  

316 
(contextexpr (name mixfix? +))  (contextexpr + '+') 

317 
; 

318 
contextelem: fixes  constrains  assumes  defines  notes 

319 
; 

320 
fixes: 'fixes' ((name ('::' type)? structmixfix?  vars) + 'and') 

321 
; 

322 
constrains: 'constrains' (name '::' type + 'and') 

323 
; 

324 
assumes: 'assumes' (thmdecl? props + 'and') 

325 
; 

326 
defines: 'defines' (thmdecl? prop proppat? + 'and') 

327 
; 

328 
notes: 'notes' (thmdef? thmrefs + 'and') 

329 
; 

330 
\end{rail} 

331 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

332 
\begin{description} 
27040  333 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

334 
\item @{command "locale"}~@{text "loc = import + body"} defines a 
27040  335 
new locale @{text loc} as a context consisting of a certain view of 
336 
existing locales (@{text import}) plus some additional elements 

337 
(@{text body}). Both @{text import} and @{text body} are optional; 

338 
the degenerate form @{command "locale"}~@{text loc} defines an empty 

339 
locale, which may still be useful to collect declarations of facts 

340 
later on. Typeinference on locale expressions automatically takes 

341 
care of the most general typing that the combined context elements 

342 
may acquire. 

343 

344 
The @{text import} consists of a structured context expression, 

345 
consisting of references to existing locales, renamed contexts, or 

346 
merged contexts. Renaming uses positional notation: @{text "c 

347 
x\<^sub>1 \<dots> x\<^sub>n"} means that (a prefix of) the fixed 

348 
parameters of context @{text c} are named @{text "x\<^sub>1, \<dots>, 

349 
x\<^sub>n"}; a ``@{text _}'' (underscore) means to skip that 

350 
position. Renaming by default deletes concrete syntax, but new 

351 
syntax may by specified with a mixfix annotation. An exeption of 

352 
this rule is the special syntax declared with ``@{text 

353 
"(\<STRUCTURE>)"}'' (see below), which is neither deleted nor can it 

354 
be changed. Merging proceeds from lefttoright, suppressing any 

355 
duplicates stemming from different paths through the import 

356 
hierarchy. 

357 

358 
The @{text body} consists of basic context elements, further context 

359 
expressions may be included as well. 

360 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

361 
\begin{description} 
27040  362 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

363 
\item @{element "fixes"}~@{text "x :: \<tau> (mx)"} declares a local 
27040  364 
parameter of type @{text \<tau>} and mixfix annotation @{text mx} (both 
365 
are optional). The special syntax declaration ``@{text 

366 
"(\<STRUCTURE>)"}'' means that @{text x} may be referenced 

367 
implicitly in this context. 

368 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

369 
\item @{element "constrains"}~@{text "x :: \<tau>"} introduces a type 
27040  370 
constraint @{text \<tau>} on the local parameter @{text x}. 
371 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

372 
\item @{element "assumes"}~@{text "a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} 
27040  373 
introduces local premises, similar to @{command "assume"} within a 
374 
proof (cf.\ \secref{sec:proofcontext}). 

375 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

376 
\item @{element "defines"}~@{text "a: x \<equiv> t"} defines a previously 
27040  377 
declared parameter. This is similar to @{command "def"} within a 
378 
proof (cf.\ \secref{sec:proofcontext}), but @{element "defines"} 

379 
takes an equational proposition instead of variableterm pair. The 

380 
lefthand side of the equation may have additional arguments, e.g.\ 

381 
``@{element "defines"}~@{text "f x\<^sub>1 \<dots> x\<^sub>n \<equiv> t"}''. 

382 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

383 
\item @{element "notes"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"} 
27040  384 
reconsiders facts within a local context. Most notably, this may 
385 
include arbitrary declarations in any attribute specifications 

386 
included here, e.g.\ a local @{attribute simp} rule. 

387 

28787  388 
The initial @{text import} specification of a locale expression 
389 
maintains a dynamic relation to the locales being referenced 

390 
(benefiting from any later fact declarations in the obvious manner). 

27040  391 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

392 
\end{description} 
27040  393 

394 
Note that ``@{text "(\<IS> p\<^sub>1 \<dots> p\<^sub>n)"}'' patterns given 

395 
in the syntax of @{element "assumes"} and @{element "defines"} above 

396 
are illegal in locale definitions. In the long goal format of 

397 
\secref{sec:goals}, term bindings may be included as expected, 

398 
though. 

399 

400 
\medskip By default, locale specifications are ``closed up'' by 

401 
turning the given text into a predicate definition @{text 

402 
loc_axioms} and deriving the original assumptions as local lemmas 

403 
(modulo local definitions). The predicate statement covers only the 

404 
newly specified assumptions, omitting the content of included locale 

405 
expressions. The full cumulative view is only provided on export, 

406 
involving another predicate @{text loc} that refers to the complete 

407 
specification text. 

408 

409 
In any case, the predicate arguments are those locale parameters 

410 
that actually occur in the respective piece of text. Also note that 

411 
these predicates operate at the metalevel in theory, but the locale 

412 
packages attempts to internalize statements according to the 

413 
objectlogic setup (e.g.\ replacing @{text \<And>} by @{text \<forall>}, and 

414 
@{text "\<Longrightarrow>"} by @{text "\<longrightarrow>"} in HOL; see also 

415 
\secref{sec:objectlogic}). Separate introduction rules @{text 

416 
loc_axioms.intro} and @{text loc.intro} are provided as well. 

417 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

418 
\item @{command "print_locale"}~@{text "import + body"} prints the 
27040  419 
specified locale expression in a flattened form. The notable 
420 
special case @{command "print_locale"}~@{text loc} just prints the 

421 
contents of the named locale, but keep in mind that typeinference 

422 
will normalize type variables according to the usual alphabetical 

423 
order. The command omits @{element "notes"} elements by default. 

424 
Use @{command "print_locale"}@{text "!"} to get them included. 

425 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

426 
\item @{command "print_locales"} prints the names of all locales 
27040  427 
of the current theory. 
428 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

429 
\item @{method intro_locales} and @{method unfold_locales} 
27040  430 
repeatedly expand all introduction rules of locale predicates of the 
431 
theory. While @{method intro_locales} only applies the @{text 

432 
loc.intro} introduction rules and therefore does not decend to 

433 
assumptions, @{method unfold_locales} is more aggressive and applies 

434 
@{text loc_axioms.intro} as well. Both methods are aware of locale 

28787  435 
specifications entailed by the context, both from target statements, 
436 
and from interpretations (see below). New goals that are entailed 

437 
by the current context are discharged automatically. 

27040  438 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

439 
\end{description} 
27040  440 
*} 
441 

442 

443 
subsection {* Interpretation of locales *} 

444 

445 
text {* 

446 
Locale expressions (more precisely, \emph{context expressions}) may 

447 
be instantiated, and the instantiated facts added to the current 

448 
context. This requires a proof of the instantiated specification 

449 
and is called \emph{locale interpretation}. Interpretation is 

450 
possible in theories and locales (command @{command 

451 
"interpretation"}) and also within a proof body (command @{command 

452 
"interpret"}). 

453 

454 
\begin{matharray}{rcl} 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

455 
@{command_def "interpretation"} & : & @{text "theory \<rightarrow> proof(prove)"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

456 
@{command_def "interpret"} & : & @{text "proof(state)  proof(chain \<rightarrow> proof(prove)"} \\ 
27040  457 
\end{matharray} 
458 

459 
\indexouternonterm{interp} 

460 
\begin{rail} 

461 
'interpretation' (interp  name ('<'  subseteq) contextexpr) 

462 
; 

463 
'interpret' interp 

464 
; 

465 
instantiation: ('[' (inst+) ']')? 

466 
; 

28085
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
27681
diff
changeset

467 
interp: (name ':')? \\ (contextexpr instantiation  
27040  468 
name instantiation 'where' (thmdecl? prop + 'and')) 
469 
; 

470 
\end{rail} 

471 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

472 
\begin{description} 
27040  473 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

474 
\item @{command "interpretation"}~@{text "expr insts \<WHERE> eqns"} 
27040  475 

476 
The first form of @{command "interpretation"} interprets @{text 

477 
expr} in the theory. The instantiation is given as a list of terms 

478 
@{text insts} and is positional. All parameters must receive an 

479 
instantiation term  with the exception of defined parameters. 

480 
These are, if omitted, derived from the defining equation and other 

481 
instantiations. Use ``@{text _}'' to omit an instantiation term. 

482 

483 
The command generates proof obligations for the instantiated 

484 
specifications (assumes and defines elements). Once these are 

485 
discharged by the user, instantiated facts are added to the theory 

486 
in a postprocessing phase. 

487 

488 
Additional equations, which are unfolded in facts during 

489 
postprocessing, may be given after the keyword @{keyword "where"}. 

490 
This is useful for interpreting concepts introduced through 

491 
definition specification elements. The equations must be proved. 

492 
Note that if equations are present, the context expression is 

493 
restricted to a locale name. 

494 

495 
The command is aware of interpretations already active in the 

28085
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
27681
diff
changeset

496 
theory, but does not simplify the goal automatically. In order to 
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
27681
diff
changeset

497 
simplify the proof obligations use methods @{method intro_locales} 
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
27681
diff
changeset

498 
or @{method unfold_locales}. Postprocessing is not applied to 
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
27681
diff
changeset

499 
facts of interpretations that are already active. This avoids 
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
27681
diff
changeset

500 
duplication of interpreted facts, in particular. Note that, in the 
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
27681
diff
changeset

501 
case of a locale with import, parts of the interpretation may 
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
27681
diff
changeset

502 
already be active. The command will only process facts for new 
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
27681
diff
changeset

503 
parts. 
27040  504 

28085
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
27681
diff
changeset

505 
The context expression may be preceded by a name, which takes effect 
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
27681
diff
changeset

506 
in the postprocessing of facts. It is used to prefix fact names, 
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
27681
diff
changeset

507 
for example to avoid accidental hiding of other facts. 
27040  508 

509 
Adding facts to locales has the effect of adding interpreted facts 

510 
to the theory for all active interpretations also. That is, 

511 
interpretations dynamically participate in any facts added to 

512 
locales. 

513 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

514 
\item @{command "interpretation"}~@{text "name \<subseteq> expr"} 
27040  515 

516 
This form of the command interprets @{text expr} in the locale 

517 
@{text name}. It requires a proof that the specification of @{text 

518 
name} implies the specification of @{text expr}. As in the 

519 
localized version of the theorem command, the proof is in the 

520 
context of @{text name}. After the proof obligation has been 

521 
dischared, the facts of @{text expr} become part of locale @{text 

522 
name} as \emph{derived} context elements and are available when the 

523 
context @{text name} is subsequently entered. Note that, like 

524 
import, this is dynamic: facts added to a locale part of @{text 

525 
expr} after interpretation become also available in @{text name}. 

526 
Like facts of renamed context elements, facts obtained by 

527 
interpretation may be accessed by prefixing with the parameter 

528 
renaming (where the parameters are separated by ``@{text _}''). 

529 

530 
Unlike interpretation in theories, instantiation is confined to the 

531 
renaming of parameters, which may be specified as part of the 

532 
context expression @{text expr}. Using defined parameters in @{text 

533 
name} one may achieve an effect similar to instantiation, though. 

534 

535 
Only specification fragments of @{text expr} that are not already 

536 
part of @{text name} (be it imported, derived or a derived fragment 

537 
of the import) are considered by interpretation. This enables 

538 
circular interpretations. 

539 

540 
If interpretations of @{text name} exist in the current theory, the 

541 
command adds interpretations for @{text expr} as well, with the same 

542 
prefix and attributes, although only for fragments of @{text expr} 

543 
that are not interpreted in the theory already. 

544 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

545 
\item @{command "interpret"}~@{text "expr insts \<WHERE> eqns"} 
27040  546 
interprets @{text expr} in the proof context and is otherwise 
547 
similar to interpretation in theories. 

548 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

549 
\end{description} 
27040  550 

551 
\begin{warn} 

552 
Since attributes are applied to interpreted theorems, 

553 
interpretation may modify the context of common proof tools, e.g.\ 

554 
the Simplifier or Classical Reasoner. Since the behavior of such 

555 
automated reasoning tools is \emph{not} stable under 

556 
interpretation morphisms, manual declarations might have to be 

557 
issued. 

558 
\end{warn} 

559 

560 
\begin{warn} 

561 
An interpretation in a theory may subsume previous 

562 
interpretations. This happens if the same specification fragment 

563 
is interpreted twice and the instantiation of the second 

564 
interpretation is more general than the interpretation of the 

565 
first. A warning is issued, since it is likely that these could 

566 
have been generalized in the first place. The locale package does 

567 
not attempt to remove subsumed interpretations. 

568 
\end{warn} 

569 
*} 

570 

571 

572 
section {* Classes \label{sec:class} *} 

573 

574 
text {* 

575 
A class is a particular locale with \emph{exactly one} type variable 

576 
@{text \<alpha>}. Beyond the underlying locale, a corresponding type class 

577 
is established which is interpreted logically as axiomatic type 

578 
class \cite{Wenzel:1997:TPHOL} whose logical content are the 

579 
assumptions of the locale. Thus, classes provide the full 

580 
generality of locales combined with the commodity of type classes 

581 
(notably typeinference). See \cite{isabelleclasses} for a short 

582 
tutorial. 

583 

584 
\begin{matharray}{rcl} 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

585 
@{command_def "class"} & : & @{text "theory \<rightarrow> local_theory"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

586 
@{command_def "instantiation"} & : & @{text "theory \<rightarrow> local_theory"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

587 
@{command_def "instance"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

588 
@{command_def "subclass"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

589 
@{command_def "print_classes"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ 
29706  590 
@{command_def "class_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ 
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

591 
@{method_def intro_classes} & : & @{text method} \\ 
27040  592 
\end{matharray} 
593 

594 
\begin{rail} 

595 
'class' name '=' ((superclassexpr '+' (contextelem+))  superclassexpr  (contextelem+)) \\ 

596 
'begin'? 

597 
; 

598 
'instantiation' (nameref + 'and') '::' arity 'begin' 

599 
; 

600 
'instance' 

601 
; 

602 
'subclass' target? nameref 

603 
; 

604 
'print\_classes' 

605 
; 

29706  606 
'class\_deps' 
607 
; 

27040  608 

609 
superclassexpr: nameref  (nameref '+' superclassexpr) 

610 
; 

611 
\end{rail} 

612 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

613 
\begin{description} 
27040  614 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

615 
\item @{command "class"}~@{text "c = superclasses + body"} defines 
27040  616 
a new class @{text c}, inheriting from @{text superclasses}. This 
617 
introduces a locale @{text c} with import of all locales @{text 

618 
superclasses}. 

619 

620 
Any @{element "fixes"} in @{text body} are lifted to the global 

621 
theory level (\emph{class operations} @{text "f\<^sub>1, \<dots>, 

622 
f\<^sub>n"} of class @{text c}), mapping the local type parameter 

623 
@{text \<alpha>} to a schematic type variable @{text "?\<alpha> :: c"}. 

624 

625 
Likewise, @{element "assumes"} in @{text body} are also lifted, 

626 
mapping each local parameter @{text "f :: \<tau>[\<alpha>]"} to its 

627 
corresponding global constant @{text "f :: \<tau>[?\<alpha> :: c]"}. The 

628 
corresponding introduction rule is provided as @{text 

629 
c_class_axioms.intro}. This rule should be rarely needed directly 

630 
 the @{method intro_classes} method takes care of the details of 

631 
class membership proofs. 

632 

28768
a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

633 
\item @{command "instantiation"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n)s 
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

634 
\<BEGIN>"} opens a theory target (cf.\ \secref{sec:target}) which 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

635 
allows to specify class operations @{text "f\<^sub>1, \<dots>, f\<^sub>n"} corresponding 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

636 
to sort @{text s} at the particular type instance @{text "(\<alpha>\<^sub>1 :: s\<^sub>1, 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

637 
\<dots>, \<alpha>\<^sub>n :: s\<^sub>n) t"}. A plain @{command "instance"} command in the 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

638 
target body poses a goal stating these type arities. The target is 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

639 
concluded by an @{command_ref (local) "end"} command. 
27040  640 

641 
Note that a list of simultaneous type constructors may be given; 

642 
this corresponds nicely to mutual recursive type definitions, e.g.\ 

643 
in Isabelle/HOL. 

644 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

645 
\item @{command "instance"} in an instantiation target body sets 
27040  646 
up a goal stating the type arities claimed at the opening @{command 
647 
"instantiation"}. The proof would usually proceed by @{method 

648 
intro_classes}, and then establish the characteristic theorems of 

649 
the type classes involved. After finishing the proof, the 

650 
background theory will be augmented by the proven type arities. 

651 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

652 
\item @{command "subclass"}~@{text c} in a class context for class 
27040  653 
@{text d} sets up a goal stating that class @{text c} is logically 
654 
contained in class @{text d}. After finishing the proof, class 

655 
@{text d} is proven to be subclass @{text c} and the locale @{text 

656 
c} is interpreted into @{text d} simultaneously. 

657 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

658 
\item @{command "print_classes"} prints all classes in the current 
27040  659 
theory. 
660 

29706  661 
\item @{command "class_deps"} visualizes all classes and their 
662 
subclass relations as a Hasse diagram. 

663 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

664 
\item @{method intro_classes} repeatedly expands all class 
27040  665 
introduction rules of this theory. Note that this method usually 
666 
needs not be named explicitly, as it is already included in the 

667 
default proof step (e.g.\ of @{command "proof"}). In particular, 

668 
instantiation of trivial (syntactic) classes may be performed by a 

669 
single ``@{command ".."}'' proof step. 

26870  670 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

671 
\end{description} 
26870  672 
*} 
673 

27040  674 

675 
subsection {* The class target *} 

676 

677 
text {* 

678 
%FIXME check 

679 

680 
A named context may refer to a locale (cf.\ \secref{sec:target}). 

681 
If this locale is also a class @{text c}, apart from the common 

682 
locale target behaviour the following happens. 

683 

684 
\begin{itemize} 

685 

686 
\item Local constant declarations @{text "g[\<alpha>]"} referring to the 

687 
local type parameter @{text \<alpha>} and local parameters @{text "f[\<alpha>]"} 

688 
are accompanied by theorylevel constants @{text "g[?\<alpha> :: c]"} 

689 
referring to theorylevel class operations @{text "f[?\<alpha> :: c]"}. 

690 

691 
\item Local theorem bindings are lifted as are assumptions. 

692 

693 
\item Local syntax refers to local operations @{text "g[\<alpha>]"} and 

694 
global operations @{text "g[?\<alpha> :: c]"} uniformly. Type inference 

695 
resolves ambiguities. In rare cases, manual type annotations are 

696 
needed. 

697 

698 
\end{itemize} 

699 
*} 

700 

701 

27053  702 
subsection {* Oldstyle axiomatic type classes \label{sec:axclass} *} 
27040  703 

704 
text {* 

705 
\begin{matharray}{rcl} 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

706 
@{command_def "axclass"} & : & @{text "theory \<rightarrow> theory"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

707 
@{command_def "instance"} & : & @{text "theory \<rightarrow> proof(prove)"} \\ 
27040  708 
\end{matharray} 
709 

710 
Axiomatic type classes are Isabelle/Pure's primitive 

711 
\emph{definitional} interface to type classes. For practical 

712 
applications, you should consider using classes 

713 
(cf.~\secref{sec:classes}) which provide high level interface. 

714 

715 
\begin{rail} 

716 
'axclass' classdecl (axmdecl prop +) 

717 
; 

718 
'instance' (nameref ('<'  subseteq) nameref  nameref '::' arity) 

719 
; 

720 
\end{rail} 

721 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

722 
\begin{description} 
27040  723 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

724 
\item @{command "axclass"}~@{text "c \<subseteq> c\<^sub>1, \<dots>, c\<^sub>n axms"} defines an 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

725 
axiomatic type class as the intersection of existing classes, with 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

726 
additional axioms holding. Class axioms may not contain more than 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

727 
one type variable. The class axioms (with implicit sort constraints 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

728 
added) are bound to the given names. Furthermore a class 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

729 
introduction rule is generated (being bound as @{text 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

730 
c_class.intro}); this rule is employed by method @{method 
27040  731 
intro_classes} to support instantiation proofs of this class. 
732 

28767  733 
The ``class axioms'' (which are derived from the internal class 
734 
definition) are stored as theorems according to the given name 

735 
specifications; the name space prefix @{text "c_class"} is added 

736 
here. The full collection of these facts is also stored as @{text 

27040  737 
c_class.axioms}. 
738 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

739 
\item @{command "instance"}~@{text "c\<^sub>1 \<subseteq> c\<^sub>2"} and @{command 
28768
a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

740 
"instance"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n)s"} setup a goal stating a class 
a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

741 
relation or type arity. The proof would usually proceed by @{method 
a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

742 
intro_classes}, and then establish the characteristic theorems of 
a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

743 
the type classes involved. After finishing the proof, the theory 
a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

744 
will be augmented by a type signature declaration corresponding to 
a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

745 
the resulting theorem. 
27040  746 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

747 
\end{description} 
27040  748 
*} 
749 

750 

751 
section {* Unrestricted overloading *} 

752 

753 
text {* 

754 
Isabelle/Pure's definitional schemes support certain forms of 

755 
overloading (see \secref{sec:consts}). At most occassions 

756 
overloading will be used in a Haskelllike fashion together with 

757 
type classes by means of @{command "instantiation"} (see 

758 
\secref{sec:class}). Sometimes lowlevel overloading is desirable. 

759 
The @{command "overloading"} target provides a convenient view for 

760 
endusers. 

761 

762 
\begin{matharray}{rcl} 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

763 
@{command_def "overloading"} & : & @{text "theory \<rightarrow> local_theory"} \\ 
27040  764 
\end{matharray} 
765 

766 
\begin{rail} 

767 
'overloading' \\ 

768 
( string ( '=='  equiv ) term ( '(' 'unchecked' ')' )? + ) 'begin' 

769 
\end{rail} 

770 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

771 
\begin{description} 
27040  772 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

773 
\item @{command "overloading"}~@{text "x\<^sub>1 \<equiv> c\<^sub>1 :: \<tau>\<^sub>1 \<AND> \<dots> x\<^sub>n \<equiv> c\<^sub>n :: \<tau>\<^sub>n \<BEGIN>"} 
27040  774 
opens a theory target (cf.\ \secref{sec:target}) which allows to 
775 
specify constants with overloaded definitions. These are identified 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

776 
by an explicitly given mapping from variable names @{text "x\<^sub>i"} to 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

777 
constants @{text "c\<^sub>i"} at particular type instances. The 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

778 
definitions themselves are established using common specification 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

779 
tools, using the names @{text "x\<^sub>i"} as reference to the 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

780 
corresponding constants. The target is concluded by @{command 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

781 
(local) "end"}. 
27040  782 

783 
A @{text "(unchecked)"} option disables global dependency checks for 

784 
the corresponding definition, which is occasionally useful for 

785 
exotic overloading. It is at the discretion of the user to avoid 

786 
malformed theory specifications! 

787 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

788 
\end{description} 
27040  789 
*} 
790 

791 

792 
section {* Incorporating ML code \label{sec:ML} *} 

793 

794 
text {* 

795 
\begin{matharray}{rcl} 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

796 
@{command_def "use"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

797 
@{command_def "ML"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

798 
@{command_def "ML_prf"} & : & @{text "proof \<rightarrow> proof"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

799 
@{command_def "ML_val"} & : & @{text "any \<rightarrow>"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

800 
@{command_def "ML_command"} & : & @{text "any \<rightarrow>"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

801 
@{command_def "setup"} & : & @{text "theory \<rightarrow> theory"} \\ 
30461  802 
@{command_def "local_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ 
30526  803 
@{command_def "attribute_setup"} & : & @{text "theory \<rightarrow> theory"} \\ 
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

804 
\end{matharray} 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

805 

cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

806 
\begin{mldecls} 
28758  807 
@{index_ML bind_thms: "string * thm list > unit"} \\ 
808 
@{index_ML bind_thm: "string * thm > unit"} \\ 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

809 
\end{mldecls} 
27040  810 

811 
\begin{rail} 

812 
'use' name 

813 
; 

30461  814 
('ML'  'ML\_prf'  'ML\_val'  'ML\_command'  'setup'  'local\_setup') text 
27040  815 
; 
30526  816 
'attribute\_setup' name '=' text text 
817 
; 

27040  818 
\end{rail} 
819 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

820 
\begin{description} 
27040  821 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

822 
\item @{command "use"}~@{text "file"} reads and executes ML 
27040  823 
commands from @{text "file"}. The current theory context is passed 
30461  824 
down to the ML toplevel and may be modified, using @{ML 
27040  825 
"Context.>>"} or derived ML commands. The file name is checked with 
826 
the @{keyword_ref "uses"} dependency declaration given in the theory 

827 
header (see also \secref{sec:beginthy}). 

28281  828 

829 
Toplevel ML bindings are stored within the (global or local) theory 

830 
context. 

27040  831 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

832 
\item @{command "ML"}~@{text "text"} is similar to @{command "use"}, 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

833 
but executes ML commands directly from the given @{text "text"}. 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

834 
Toplevel ML bindings are stored within the (global or local) theory 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

835 
context. 
28281  836 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

837 
\item @{command "ML_prf"} is analogous to @{command "ML"} but works 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

838 
within a proof context. 
28281  839 

840 
Toplevel ML bindings are stored within the proof context in a 

841 
purely sequential fashion, disregarding the nested proof structure. 

842 
ML bindings introduced by @{command "ML_prf"} are discarded at the 

843 
end of the proof. 

27040  844 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

845 
\item @{command "ML_val"} and @{command "ML_command"} are diagnostic 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

846 
versions of @{command "ML"}, which means that the context may not be 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

847 
updated. @{command "ML_val"} echos the bindings produced at the ML 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

848 
toplevel, but @{command "ML_command"} is silent. 
27040  849 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

850 
\item @{command "setup"}~@{text "text"} changes the current theory 
27040  851 
context by applying @{text "text"}, which refers to an ML expression 
30461  852 
of type @{ML_type "theory > theory"}. This enables to initialize 
853 
any objectlogic specific tools and packages written in ML, for 

854 
example. 

855 

856 
\item @{command "local_setup"} is similar to @{command "setup"} for 

857 
a local theory context, and an ML expression of type @{ML_type 

858 
"local_theory > local_theory"}. This allows to 

859 
invoke local theory specification packages without going through 

860 
concrete outer syntax, for example. 

28758  861 

30526  862 
\item @{command "attribute_setup"}~@{text "name = text description"} 
863 
defines an attribute in the current theory. The given @{text 

864 
"text"} has to be an ML expression of type 

865 
@{ML_type "attribute context_parser"}, cf.\ basic parsers defined in 

866 
structure @{ML_struct Args} and @{ML_struct Attrib}. 

867 

868 
In principle, attributes can operate both on a given theorem and the 

869 
implicit context, although in practice only one is modified and the 

870 
other serves as parameter. Here are examples for these two cases: 

871 

872 
\end{description} 

873 
*} 

874 

875 
attribute_setup my_rule = {* 

876 
Attrib.thms >> (fn ths => 

877 
Thm.rule_attribute (fn context: Context.generic => fn th: thm => 

878 
let val th' = th OF ths 

879 
in th' end)) *} "my rule" 

880 

30546  881 
attribute_setup my_declaration = {* 
30526  882 
Attrib.thms >> (fn ths => 
883 
Thm.declaration_attribute (fn th: thm => fn context: Context.generic => 

884 
let val context' = context 

885 
in context' end)) *} "my declaration" 

886 

887 
text {* 

888 
\begin{description} 

889 

28758  890 
\item @{ML bind_thms}~@{text "(name, thms)"} stores a list of 
891 
theorems produced in ML both in the theory context and the ML 

892 
toplevel, associating it with the provided name. Theorems are put 

893 
into a global ``standard'' format before being stored. 

894 

895 
\item @{ML bind_thm} is similar to @{ML bind_thms} but refers to a 

896 
singleton theorem. 

27040  897 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

898 
\end{description} 
27040  899 
*} 
900 

901 

902 
section {* Primitive specification elements *} 

903 

904 
subsection {* Type classes and sorts \label{sec:classes} *} 

905 

906 
text {* 

907 
\begin{matharray}{rcll} 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

908 
@{command_def "classes"} & : & @{text "theory \<rightarrow> theory"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

909 
@{command_def "classrel"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

910 
@{command_def "defaultsort"} & : & @{text "theory \<rightarrow> theory"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

911 
@{command_def "class_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ 
27040  912 
\end{matharray} 
913 

914 
\begin{rail} 

915 
'classes' (classdecl +) 

916 
; 

917 
'classrel' (nameref ('<'  subseteq) nameref + 'and') 

918 
; 

919 
'defaultsort' sort 

920 
; 

921 
\end{rail} 

922 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

923 
\begin{description} 
27040  924 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

925 
\item @{command "classes"}~@{text "c \<subseteq> c\<^sub>1, \<dots>, c\<^sub>n"} declares class 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

926 
@{text c} to be a subclass of existing classes @{text "c\<^sub>1, \<dots>, c\<^sub>n"}. 
28767  927 
Isabelle implicitly maintains the transitive closure of the class 
928 
hierarchy. Cyclic class structures are not permitted. 

27040  929 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

930 
\item @{command "classrel"}~@{text "c\<^sub>1 \<subseteq> c\<^sub>2"} states subclass 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

931 
relations between existing classes @{text "c\<^sub>1"} and @{text "c\<^sub>2"}. 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

932 
This is done axiomatically! The @{command_ref "instance"} command 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

933 
(see \secref{sec:axclass}) provides a way to introduce proven class 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

934 
relations. 
27040  935 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

936 
\item @{command "defaultsort"}~@{text s} makes sort @{text s} the 
28767  937 
new default sort for any type variable that is given explicitly in 
938 
the text, but lacks a sort constraint (wrt.\ the current context). 

939 
Type variables generated by type inference are not affected. 

940 

941 
Usually the default sort is only changed when defining a new 

942 
objectlogic. For example, the default sort in Isabelle/HOL is 

943 
@{text type}, the class of all HOL types. %FIXME sort antiq? 

944 

945 
When merging theories, the default sorts of the parents are 

946 
logically intersected, i.e.\ the representations as lists of classes 

947 
are joined. 

27040  948 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

949 
\item @{command "class_deps"} visualizes the subclass relation, 
27040  950 
using Isabelle's graph browser tool (see also \cite{isabellesys}). 
951 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

952 
\end{description} 
27040  953 
*} 
954 

955 

956 
subsection {* Types and type abbreviations \label{sec:typespure} *} 

957 

958 
text {* 

959 
\begin{matharray}{rcll} 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

960 
@{command_def "types"} & : & @{text "theory \<rightarrow> theory"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

961 
@{command_def "typedecl"} & : & @{text "theory \<rightarrow> theory"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

962 
@{command_def "arities"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\ 
27040  963 
\end{matharray} 
964 

965 
\begin{rail} 

966 
'types' (typespec '=' type infix? +) 

967 
; 

968 
'typedecl' typespec infix? 

969 
; 

970 
'arities' (nameref '::' arity +) 

971 
; 

972 
\end{rail} 

973 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

974 
\begin{description} 
27040  975 

28767  976 
\item @{command "types"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = \<tau>"} introduces a 
977 
\emph{type synonym} @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} for the existing type 

978 
@{text "\<tau>"}. Unlike actual type definitions, as are available in 

979 
Isabelle/HOL for example, type synonyms are merely syntactic 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

980 
abbreviations without any logical significance. Internally, type 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

981 
synonyms are fully expanded. 
27040  982 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

983 
\item @{command "typedecl"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} declares a new 
28767  984 
type constructor @{text t}. If the objectlogic defines a base sort 
985 
@{text s}, then the constructor is declared to operate on that, via 

986 
the axiomatic specification @{command arities}~@{text "t :: (s, \<dots>, 

28768
a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

987 
s)s"}. 
27040  988 

28768
a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

989 
\item @{command "arities"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n)s"} augments 
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

990 
Isabelle's ordersorted signature of types by new type constructor 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

991 
arities. This is done axiomatically! The @{command_ref "instance"} 
28768
a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

992 
command (see \secref{sec:axclass}) provides a way to introduce 
a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

993 
proven type arities. 
27040  994 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

995 
\end{description} 
27040  996 
*} 
997 

998 

28768
a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

999 
subsection {* Coregularity of type classes and arities *} 
a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

1000 

a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

1001 
text {* The class relation together with the collection of 
a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

1002 
typeconstructor arities must obey the principle of 
a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

1003 
\emph{coregularity} as defined below. 
a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

1004 

a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

1005 
\medskip For the subsequent formulation of coregularity we assume 
a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

1006 
that the class relation is closed by transitivity and reflexivity. 
a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

1007 
Moreover the collection of arities @{text "t :: (\<^vec>s)c"} is 
a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

1008 
completed such that @{text "t :: (\<^vec>s)c"} and @{text "c \<subseteq> c'"} 
a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

1009 
implies @{text "t :: (\<^vec>s)c'"} for all such declarations. 
a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

1010 

a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

1011 
Treating sorts as finite sets of classes (meaning the intersection), 
a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

1012 
the class relation @{text "c\<^sub>1 \<subseteq> c\<^sub>2"} is extended to sorts as 
a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

1013 
follows: 
a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

1014 
\[ 
a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

1015 
@{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"} 
a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

1016 
\] 
a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

1017 

a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

1018 
This relation on sorts is further extended to tuples of sorts (of 
a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

1019 
the same length) in the componentwise way. 
a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

1020 

a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

1021 
\smallskip Coregularity of the class relation together with the 
a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

1022 
arities relation means: 
a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

1023 
\[ 
a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

1024 
@{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"} 
a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

1025 
\] 
a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

1026 
\noindent for all such arities. In other words, whenever the result 
a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

1027 
classes of some typeconstructor arities are related, then the 
a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

1028 
argument sorts need to be related in the same way. 
a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

1029 

a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

1030 
\medskip Coregularity is a very fundamental property of the 
a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

1031 
ordersorted algebra of types. For example, it entails principle 
a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

1032 
types and most general unifiers, e.g.\ see \cite{nipkowprehofer}. 
a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

1033 
*} 
a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

1034 

a056077b65a1
added section "Coregularity of type classes and arities" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

1035 

27040  1036 
subsection {* Constants and definitions \label{sec:consts} *} 
1037 

1038 
text {* 

1039 
Definitions essentially express abbreviations within the logic. The 

1040 
simplest form of a definition is @{text "c :: \<sigma> \<equiv> t"}, where @{text 

1041 
c} is a newly declared constant. Isabelle also allows derived forms 

1042 
where the arguments of @{text c} appear on the left, abbreviating a 

1043 
prefix of @{text \<lambda>}abstractions, e.g.\ @{text "c \<equiv> \<lambda>x y. t"} may be 

1044 
written more conveniently as @{text "c x y \<equiv> t"}. Moreover, 

1045 
definitions may be weakened by adding arbitrary preconditions: 

1046 
@{text "A \<Longrightarrow> c x y \<equiv> t"}. 

1047 

1048 
\medskip The builtin wellformedness conditions for definitional 

1049 
specifications are: 

1050 

1051 
\begin{itemize} 

1052 

1053 
\item Arguments (on the lefthand side) must be distinct variables. 

1054 

1055 
\item All variables on the righthand side must also appear on the 

1056 
lefthand side. 

1057 

1058 
\item All type variables on the righthand side must also appear on 

1059 
the lefthand side; this prohibits @{text "0 :: nat \<equiv> length ([] :: 

1060 
\<alpha> list)"} for example. 

1061 

1062 
\item The definition must not be recursive. Most objectlogics 

1063 
provide definitional principles that can be used to express 

1064 
recursion safely. 

1065 

1066 
\end{itemize} 

1067 

1068 
Overloading means that a constant being declared as @{text "c :: \<alpha> 

1069 
decl"} may be defined separately on type instances @{text "c :: 

1070 
(\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n) t decl"} for each type constructor @{text 

1071 
t}. The righthand side may mention overloaded constants 

1072 
recursively at type instances corresponding to the immediate 

1073 
argument types @{text "\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n"}. Incomplete 

1074 
specification patterns impose global constraints on all occurrences, 

1075 
e.g.\ @{text "d :: \<alpha> \<times> \<alpha>"} on the lefthand side means that all 

1076 
corresponding occurrences on some righthand side need to be an 

1077 
instance of this, general @{text "d :: \<alpha> \<times> \<beta>"} will be disallowed. 

1078 

1079 
\begin{matharray}{rcl} 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

1080 
@{command_def "consts"} & : & @{text "theory \<rightarrow> theory"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

1081 
@{command_def "defs"} & : & @{text "theory \<rightarrow> theory"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

1082 
@{command_def "constdefs"} & : & @{text "theory \<rightarrow> theory"} \\ 
27040  1083 
\end{matharray} 
1084 

1085 
\begin{rail} 

1086 
'consts' ((name '::' type mixfix?) +) 

1087 
; 

1088 
'defs' ('(' 'unchecked'? 'overloaded'? ')')? \\ (axmdecl prop +) 

1089 
; 

1090 
\end{rail} 

1091 

1092 
\begin{rail} 

1093 
'constdefs' structs? (constdecl? constdef +) 

1094 
; 

1095 

1096 
structs: '(' 'structure' (vars + 'and') ')' 

1097 
; 

1098 
constdecl: ((name '::' type mixfix  name '::' type  name mixfix) 'where'?)  name 'where' 

1099 
; 

1100 
constdef: thmdecl? prop 

1101 
; 

1102 
\end{rail} 

1103 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

1104 
\begin{description} 
27040  1105 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

1106 
\item @{command "consts"}~@{text "c :: \<sigma>"} declares constant @{text 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

1107 
c} to have any instance of type scheme @{text \<sigma>}. The optional 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

1108 
mixfix annotations may attach concrete syntax to the constants 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

1109 
declared. 
27040  1110 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

1111 
\item @{command "defs"}~@{text "name: eqn"} introduces @{text eqn} 
27040  1112 
as a definitional axiom for some existing constant. 
1113 

1114 
The @{text "(unchecked)"} option disables global dependency checks 

1115 
for this definition, which is occasionally useful for exotic 

1116 
overloading. It is at the discretion of the user to avoid malformed 

1117 
theory specifications! 

1118 

1119 
The @{text "(overloaded)"} option declares definitions to be 

1120 
potentially overloaded. Unless this option is given, a warning 

1121 
message would be issued for any definitional equation with a more 

1122 
special type than that of the corresponding constant declaration. 

1123 

28767  1124 
\item @{command "constdefs"} combines constant declarations and 
1125 
definitions, with typeinference taking care of the most general 

1126 
typing of the given specification (the optional type constraint may 

1127 
refer to typeinference dummies ``@{text _}'' as usual). The 

1128 
resulting type declaration needs to agree with that of the 

1129 
specification; overloading is \emph{not} supported here! 

27040  1130 

1131 
The constant name may be omitted altogether, if neither type nor 

1132 
syntax declarations are given. The canonical name of the 

1133 
definitional axiom for constant @{text c} will be @{text c_def}, 

1134 
unless specified otherwise. Also note that the given list of 

1135 
specifications is processed in a strictly sequential manner, with 

1136 
typechecking being performed independently. 

1137 

1138 
An optional initial context of @{text "(structure)"} declarations 

1139 
admits use of indexed syntax, using the special symbol @{verbatim 

1140 
"\<index>"} (printed as ``@{text "\<index>"}''). The latter concept is 

28767  1141 
particularly useful with locales (see also \secref{sec:locale}). 
27040  1142 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

1143 
\end{description} 
27040  1144 
*} 
1145 

1146 

1147 
section {* Axioms and theorems \label{sec:axmsthms} *} 

1148 

1149 
text {* 

1150 
\begin{matharray}{rcll} 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

1151 
@{command_def "axioms"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

1152 
@{command_def "lemmas"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

1153 
@{command_def "theorems"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ 
27040  1154 
\end{matharray} 
1155 

1156 
\begin{rail} 

1157 
'axioms' (axmdecl prop +) 

1158 
; 

1159 
('lemmas'  'theorems') target? (thmdef? thmrefs + 'and') 

1160 
; 

1161 
\end{rail} 

1162 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

1163 
\begin{description} 
27040  1164 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

1165 
\item @{command "axioms"}~@{text "a: \<phi>"} introduces arbitrary 
27040  1166 
statements as axioms of the metalogic. In fact, axioms are 
1167 
``axiomatic theorems'', and may be referred later just as any other 

1168 
theorem. 

1169 

1170 
Axioms are usually only introduced when declaring new logical 

1171 
systems. Everyday work is typically done the hard way, with proper 

1172 
definitions and proven theorems. 

1173 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

1174 
\item @{command "lemmas"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"} retrieves and stores 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

1175 
existing facts in the theory context, or the specified target 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

1176 
context (see also \secref{sec:target}). Typical applications would 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

1177 
also involve attributes, to declare Simplifier rules, for example. 
27040  1178 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

1179 
\item @{command "theorems"} is essentially the same as @{command 
27040  1180 
"lemmas"}, but marks the result as a different kind of facts. 
1181 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

1182 
\end{description} 
27040  1183 
*} 
1184 

1185 

1186 
section {* Oracles *} 

1187 

28756  1188 
text {* Oracles allow Isabelle to take advantage of external reasoners 
1189 
such as arithmetic decision procedures, model checkers, fast 

1190 
tautology checkers or computer algebra systems. Invoked as an 

1191 
oracle, an external reasoner can create arbitrary Isabelle theorems. 

1192 

1193 
It is the responsibility of the user to ensure that the external 

1194 
reasoner is as trustworthy as the application requires. Another 

1195 
typical source of errors is the linkup between Isabelle and the 

1196 
external tool, not just its concrete implementation, but also the 

1197 
required translation between two different logical environments. 

1198 

1199 
Isabelle merely guarantees wellformedness of the propositions being 

1200 
asserted, and records within the internal derivation object how 

1201 
presumed theorems depend on unproven suppositions. 

1202 

27040  1203 
\begin{matharray}{rcl} 
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

1204 
@{command_def "oracle"} & : & @{text "theory \<rightarrow> theory"} \\ 
27040  1205 
\end{matharray} 
1206 

1207 
\begin{rail} 

28290  1208 
'oracle' name '=' text 
27040  1209 
; 
1210 
\end{rail} 

1211 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

1212 
\begin{description} 
27040  1213 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

1214 
\item @{command "oracle"}~@{text "name = text"} turns the given ML 
28290  1215 
expression @{text "text"} of type @{ML_text "'a > cterm"} into an 
1216 
ML function of type @{ML_text "'a > thm"}, which is bound to the 

28756  1217 
global identifier @{ML_text name}. This acts like an infinitary 
1218 
specification of axioms! Invoking the oracle only works within the 

1219 
scope of the resulting theory. 

27040  1220 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

1221 
\end{description} 
28756  1222 

29752  1223 
See @{"file" "~~/src/FOL/ex/Iff_Oracle.thy"} for a worked example of 
28756  1224 
defining a new primitive rule as oracle, and turning it into a proof 
1225 
method. 

27040  1226 
*} 
1227 

1228 

1229 
section {* Name spaces *} 

1230 

1231 
text {* 

1232 
\begin{matharray}{rcl} 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

1233 
@{command_def "global"} & : & @{text "theory \<rightarrow> theory"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

1234 
@{command_def "local"} & : & @{text "theory \<rightarrow> theory"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

1235 
@{command_def "hide"} & : & @{text "theory \<rightarrow> theory"} \\ 
27040  1236 
\end{matharray} 
1237 

1238 
\begin{rail} 

1239 
'hide' ('(open)')? name (nameref + ) 

1240 
; 

1241 
\end{rail} 

1242 

1243 
Isabelle organizes any kind of name declarations (of types, 

1244 
constants, theorems etc.) by separate hierarchically structured name 

1245 
spaces. Normally the user does not have to control the behavior of 

1246 
name spaces by hand, yet the following commands provide some way to 

1247 
do so. 

1248 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

1249 
\begin{description} 
27040  1250 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

1251 
\item @{command "global"} and @{command "local"} change the current 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

1252 
name declaration mode. Initially, theories start in @{command 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

1253 
"local"} mode, causing all names to be automatically qualified by 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

1254 
the theory name. Changing this to @{command "global"} causes all 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

1255 
names to be declared without the theory prefix, until @{command 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

1256 
"local"} is declared again. 
27040  1257 

1258 
Note that global names are prone to get hidden accidently later, 

1259 
when qualified names of the same base name are introduced. 

1260 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset

1261 
\item @{command "hide"}~@{text "space names"} fully removes 
27040  1262 
declarations from a given name space (which may be @{text "class"}, 
1263 
@{text "type"}, @{text "const"}, or @{text "fact"}); with the @{text 

1264 
"(open)"} option, only the base name is hidden. Global 

1265 