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