summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

doc-src/Ref/theories.tex

author | wenzelm |

Mon Aug 28 13:52:38 2000 +0200 (2000-08-28) | |

changeset 9695 | ec7d7f877712 |

parent 8136 | 8c65f3ca13f2 |

child 11052 | 1379e49c0ee9 |

permissions | -rw-r--r-- |

proper setup of iman.sty/extra.sty/ttbox.sty;

2 %% $Id$

4 \chapter{Theories, Terms and Types} \label{theories}

5 \index{theories|(}\index{signatures|bold}

6 \index{reading!axioms|see{\texttt{assume_ax}}} Theories organize the syntax,

7 declarations and axioms of a mathematical development. They are built,

8 starting from the Pure or CPure theory, by extending and merging existing

9 theories. They have the \ML\ type \mltydx{theory}. Theory operations signal

10 errors by raising exception \xdx{THEORY}, returning a message and a list of

11 theories.

13 Signatures, which contain information about sorts, types, constants and

14 syntax, have the \ML\ type~\mltydx{Sign.sg}. For identification, each

15 signature carries a unique list of \bfindex{stamps}, which are \ML\

16 references to strings. The strings serve as human-readable names; the

17 references serve as unique identifiers. Each primitive signature has a

18 single stamp. When two signatures are merged, their lists of stamps are

19 also merged. Every theory carries a unique signature.

21 Terms and types are the underlying representation of logical syntax. Their

22 \ML\ definitions are irrelevant to naive Isabelle users. Programmers who

23 wish to extend Isabelle may need to know such details, say to code a tactic

24 that looks for subgoals of a particular form. Terms and types may be

25 `certified' to be well-formed with respect to a given signature.

28 \section{Defining theories}\label{sec:ref-defining-theories}

30 Theories are defined via theory files $name$\texttt{.thy} (there are also

31 \ML-level interfaces which are only intended for people building advanced

32 theory definition packages). Appendix~\ref{app:TheorySyntax} presents the

33 concrete syntax for theory files; here follows an explanation of the

34 constituent parts.

35 \begin{description}

36 \item[{\it theoryDef}] is the full definition. The new theory is called $id$.

37 It is the union of the named \textbf{parent

38 theories}\indexbold{theories!parent}, possibly extended with new

39 components. \thydx{Pure} and \thydx{CPure} are the basic theories, which

40 contain only the meta-logic. They differ just in their concrete syntax for

41 function applications.

43 The new theory begins as a merge of its parents.

44 \begin{ttbox}

45 Attempt to merge different versions of theories: "\(T@1\)", \(\ldots\), "\(T@n\)"

46 \end{ttbox}

47 This error may especially occur when a theory is redeclared --- say to

48 change an inappropriate definition --- and bindings to old versions persist.

49 Isabelle ensures that old and new theories of the same name are not involved

50 in a proof.

52 \item[$classes$]

53 is a series of class declarations. Declaring {\tt$id$ < $id@1$ \dots\

54 $id@n$} makes $id$ a subclass of the existing classes $id@1\dots

55 id@n$. This rules out cyclic class structures. Isabelle automatically

56 computes the transitive closure of subclass hierarchies; it is not

57 necessary to declare \texttt{c < e} in addition to \texttt{c < d} and \texttt{d <

58 e}.

60 \item[$default$]

61 introduces $sort$ as the new default sort for type variables. This applies

62 to unconstrained type variables in an input string but not to type

63 variables created internally. If omitted, the default sort is the listwise

64 union of the default sorts of the parent theories (i.e.\ their logical

65 intersection).

67 \item[$sort$] is a finite set of classes. A single class $id$ abbreviates the

68 sort $\{id\}$.

70 \item[$types$]

71 is a series of type declarations. Each declares a new type constructor

72 or type synonym. An $n$-place type constructor is specified by

73 $(\alpha@1,\dots,\alpha@n)name$, where the type variables serve only to

74 indicate the number~$n$.

76 A \textbf{type synonym}\indexbold{type synonyms} is an abbreviation

77 $(\alpha@1,\dots,\alpha@n)name = \tau$, where $name$ and $\tau$ can

78 be strings.

80 \item[$infix$]

81 declares a type or constant to be an infix operator having priority $nat$

82 and associating to the left (\texttt{infixl}) or right (\texttt{infixr}).

83 Only 2-place type constructors can have infix status; an example is {\tt

84 ('a,'b)~"*"~(infixr~20)}, which may express binary product types.

86 \item[$arities$] is a series of type arity declarations. Each assigns

87 arities to type constructors. The $name$ must be an existing type

88 constructor, which is given the additional arity $arity$.

90 \item[$nonterminals$]\index{*nonterminal symbols} declares purely

91 syntactic types to be used as nonterminal symbols of the context

92 free grammar.

94 \item[$consts$] is a series of constant declarations. Each new

95 constant $name$ is given the specified type. The optional $mixfix$

96 annotations may attach concrete syntax to the constant.

98 \item[$syntax$] \index{*syntax section}\index{print mode} is a variant

99 of $consts$ which adds just syntax without actually declaring

100 logical constants. This gives full control over a theory's context

101 free grammar. The optional $mode$ specifies the print mode where the

102 mixfix productions should be added. If there is no \texttt{output}

103 option given, all productions are also added to the input syntax

104 (regardless of the print mode).

106 \item[$mixfix$] \index{mixfix declarations}

107 annotations can take three forms:

108 \begin{itemize}

109 \item A mixfix template given as a $string$ of the form

110 {\tt"}\dots{\tt\_}\dots{\tt\_}\dots{\tt"} where the $i$-th underscore

111 indicates the position where the $i$-th argument should go. The list

112 of numbers gives the priority of each argument. The final number gives

113 the priority of the whole construct.

115 \item A constant $f$ of type $\tau@1\To(\tau@2\To\tau)$ can be given {\bf

116 infix} status.

118 \item A constant $f$ of type $(\tau@1\To\tau@2)\To\tau$ can be given {\bf

119 binder} status. The declaration \texttt{binder} $\cal Q$ $p$ causes

120 ${\cal Q}\,x.F(x)$ to be treated

121 like $f(F)$, where $p$ is the priority.

122 \end{itemize}

124 \item[$trans$]

125 specifies syntactic translation rules (macros). There are three forms:

126 parse rules (\texttt{=>}), print rules (\texttt{<=}), and parse/print rules ({\tt

127 ==}).

129 \item[$rules$]

130 is a series of rule declarations. Each has a name $id$ and the formula is

131 given by the $string$. Rule names must be distinct within any single

132 theory.

134 \item[$defs$] is a series of definitions. They are just like $rules$, except

135 that every $string$ must be a definition (see below for details).

137 \item[$constdefs$] combines the declaration of constants and their

138 definition. The first $string$ is the type, the second the definition.

140 \item[$axclass$] \index{*axclass section} defines an \rmindex{axiomatic type

141 class} \cite{Wenzel:1997:TPHOL} as the intersection of existing classes,

142 with additional axioms holding. Class axioms may not contain more than one

143 type variable. The class axioms (with implicit sort constraints added) are

144 bound to the given names. Furthermore a class introduction rule is

145 generated, which is automatically employed by $instance$ to prove

146 instantiations of this class.

148 \item[$instance$] \index{*instance section} proves class inclusions or

149 type arities at the logical level and then transfers these to the

150 type signature. The instantiation is proven and checked properly.

151 The user has to supply sufficient witness information: theorems

152 ($longident$), axioms ($string$), or even arbitrary \ML{} tactic

153 code $verbatim$.

155 \item[$oracle$] links the theory to a trusted external reasoner. It is

156 allowed to create theorems, but each theorem carries a proof object

157 describing the oracle invocation. See \S\ref{sec:oracles} for details.

159 \item[$local$, $global$] change the current name declaration mode.

160 Initially, theories start in $local$ mode, causing all names of

161 types, constants, axioms etc.\ to be automatically qualified by the

162 theory name. Changing this to $global$ causes all names to be

163 declared as short base names only.

165 The $local$ and $global$ declarations act like switches, affecting

166 all following theory sections until changed again explicitly. Also

167 note that the final state at the end of the theory will persist. In

168 particular, this determines how the names of theorems stored later

169 on are handled.

171 \item[$setup$]\index{*setup!theory} applies a list of ML functions to

172 the theory. The argument should denote a value of type

173 \texttt{(theory -> theory) list}. Typically, ML packages are

174 initialized in this way.

176 \item[$ml$] \index{*ML section}

177 consists of \ML\ code, typically for parse and print translation functions.

178 \end{description}

179 %

180 Chapters~\ref{Defining-Logics} and \ref{chap:syntax} explain mixfix

181 declarations, translation rules and the \texttt{ML} section in more detail.

184 \subsection{Definitions}\indexbold{definitions}

186 \textbf{Definitions} are intended to express abbreviations. The simplest

187 form of a definition is $f \equiv t$, where $f$ is a constant.

188 Isabelle also allows a derived forms where the arguments of~$f$ appear

189 on the left, abbreviating a string of $\lambda$-abstractions.

191 Isabelle makes the following checks on definitions:

192 \begin{itemize}

193 \item Arguments (on the left-hand side) must be distinct variables.

194 \item All variables on the right-hand side must also appear on the left-hand

195 side.

196 \item All type variables on the right-hand side must also appear on

197 the left-hand side; this prohibits definitions such as {\tt

198 (zero::nat) == length ([]::'a list)}.

199 \item The definition must not be recursive. Most object-logics provide

200 definitional principles that can be used to express recursion safely.

201 \end{itemize}

202 These checks are intended to catch the sort of errors that might be made

203 accidentally. Misspellings, for instance, might result in additional

204 variables appearing on the right-hand side. More elaborate checks could be

205 made, but the cost might be overly strict rules on declaration order, etc.

208 \subsection{*Classes and arities}

209 \index{classes!context conditions}\index{arities!context conditions}

211 In order to guarantee principal types~\cite{nipkow-prehofer},

212 arity declarations must obey two conditions:

213 \begin{itemize}

214 \item There must not be any two declarations $ty :: (\vec{r})c$ and

215 $ty :: (\vec{s})c$ with $\vec{r} \neq \vec{s}$. For example, this

216 excludes the following:

217 \begin{ttbox}

218 arities

219 foo :: (\{logic{\}}) logic

220 foo :: (\{{\}})logic

221 \end{ttbox}

223 \item If there are two declarations $ty :: (s@1,\dots,s@n)c$ and $ty ::

224 (s@1',\dots,s@n')c'$ such that $c' < c$ then $s@i' \preceq s@i$ must hold

225 for $i=1,\dots,n$. The relationship $\preceq$, defined as

226 \[ s' \preceq s \iff \forall c\in s. \exists c'\in s'.~ c'\le c, \]

227 expresses that the set of types represented by $s'$ is a subset of the

228 set of types represented by $s$. Assuming $term \preceq logic$, the

229 following is forbidden:

230 \begin{ttbox}

231 arities

232 foo :: (\{logic{\}})logic

233 foo :: (\{{\}})term

234 \end{ttbox}

236 \end{itemize}

239 \section{The theory loader}\label{sec:more-theories}

240 \index{theories!reading}\index{files!reading}

242 Isabelle's theory loader manages dependencies of the internal graph of theory

243 nodes (the \emph{theory database}) and the external view of the file system.

244 See \S\ref{sec:intro-theories} for its most basic commands, such as

245 \texttt{use_thy}. There are a few more operations available.

247 \begin{ttbox}

248 use_thy_only : string -> unit

249 update_thy_only : string -> unit

250 touch_thy : string -> unit

251 remove_thy : string -> unit

252 delete_tmpfiles : bool ref \hfill\textbf{initially true}

253 \end{ttbox}

255 \begin{ttdescription}

256 \item[\ttindexbold{use_thy_only} "$name$";] is similar to \texttt{use_thy},

257 but processes the actual theory file $name$\texttt{.thy} only, ignoring

258 $name$\texttt{.ML}. This might be useful in replaying proof scripts by hand

259 from the very beginning, starting with the fresh theory.

261 \item[\ttindexbold{update_thy_only} "$name$";] is similar to

262 \texttt{update_thy}, but processes the actual theory file

263 $name$\texttt{.thy} only, ignoring $name$\texttt{.ML}.

265 \item[\ttindexbold{touch_thy} "$name$";] marks theory node $name$ of the

266 internal graph as outdated. While the theory remains usable, subsequent

267 operations such as \texttt{use_thy} may cause a reload.

269 \item[\ttindexbold{remove_thy} "$name$";] deletes theory node $name$,

270 including \emph{all} of its descendants. Beware! This is a quick way to

271 dispose a large number of theories at once. Note that {\ML} bindings to

272 theorems etc.\ of removed theories may still persist.

274 \item[reset \ttindexbold{delete_tmpfiles};] processing theory files usually

275 involves temporary {\ML} files to be created. By default, these are deleted

276 afterwards. Resetting the \texttt{delete_tmpfiles} flag inhibits this,

277 leaving the generated code for debugging purposes. The basic location for

278 temporary files is determined by the \texttt{ISABELLE_TMP} environment

279 variable (which is private to the running Isabelle process and may be

280 retrieved by \ttindex{getenv} from {\ML}).

281 \end{ttdescription}

283 \medskip Theory and {\ML} files are located by skimming through the

284 directories listed in Isabelle's internal load path, which merely contains the

285 current directory ``\texttt{.}'' by default. The load path may be accessed by

286 the following operations.

288 \begin{ttbox}

289 show_path: unit -> string list

290 add_path: string -> unit

291 del_path: string -> unit

292 reset_path: unit -> unit

293 with_path: string -> ('a -> 'b) -> 'a -> 'b

294 \end{ttbox}

296 \begin{ttdescription}

297 \item[\ttindexbold{show_path}();] displays the load path components in

298 canonical string representation (which is always according to Unix rules).

300 \item[\ttindexbold{add_path} "$dir$";] adds component $dir$ to the beginning

301 of the load path.

303 \item[\ttindexbold{del_path} "$dir$";] removes any occurrences of component

304 $dir$ from the load path.

306 \item[\ttindexbold{reset_path}();] resets the load path to ``\texttt{.}''

307 (current directory) only.

309 \item[\ttindexbold{with_path} "$dir$" $f$ $x$;] temporarily adds component

310 $dir$ to the beginning of the load path before executing $(f~x)$.

312 \end{ttdescription}

314 Furthermore, in operations referring indirectly to some file (e.g.\

315 \texttt{use_dir}) the argument may be prefixed by a directory that will be

316 temporarily appended to the load path, too.

319 \section{Locales}

320 \label{Locales}

322 Locales \cite{kammueller-locales} are a concept of local proof contexts. They

323 are introduced as named syntactic objects within theories and can be

324 opened in any descendant theory.

326 \subsection{Declaring Locales}

328 A locale is declared in a theory section that starts with the

329 keyword \texttt{locale}. It consists typically of three parts, the

330 \texttt{fixes} part, the \texttt{assumes} part, and the \texttt{defines} part.

331 Appendix \ref{app:TheorySyntax} presents the full syntax.

333 \subsubsection{Parts of Locales}

335 The subsection introduced by the keyword \texttt{fixes} declares the locale

336 constants in a way that closely resembles a global \texttt{consts}

337 declaration. In particular, there may be an optional pretty printing syntax

338 for the locale constants.

340 The subsequent \texttt{assumes} part specifies the locale rules. They are

341 defined like \texttt{rules}: by an identifier followed by the rule

342 given as a string. Locale rules admit the statement of local assumptions

343 about the locale constants. The \texttt{assumes} part is optional. Non-fixed

344 variables in locale rules are automatically bound by the universal quantifier

345 \texttt{!!} of the meta-logic.

347 Finally, the \texttt{defines} part introduces the definitions that are

348 available in the locale. Locale constants declared in the \texttt{fixes}

349 section are defined using the meta-equality \texttt{==}. If the

350 locale constant is a functiond then its definition can (as usual) have

351 variables on the left-hand side acting as formal parameters; they are

352 considered as schematic variables and are automatically generalized by

353 universal quantification of the meta-logic. The right hand side of a

354 definition must not contain variables that are not already on the left hand

355 side. In so far locale definitions behave like theory level definitions.

356 However, the locale concept realizes \emph{dependent definitions}: any variable

357 that is fixed as a locale constant can occur on the right hand side of

358 definitions. For an illustration of these dependent definitions see the

359 occurrence of the locale constant \texttt{G} on the right hand side of the

360 definitions of the locale \texttt{group} below. Naturally, definitions can

361 already use the syntax of the locale constants in the \texttt{fixes}

362 subsection. The \texttt{defines} part is, as the \texttt{assumes} part,

363 optional.

365 \subsubsection{Example for Definition}

366 The concrete syntax of locale definitions is demonstrated by example below.

368 Locale \texttt{group} assumes the definition of groups in a theory

369 file\footnote{This and other examples are from \texttt{HOL/ex}.}. A locale

370 defining a convenient proof environment for group related proofs may be

371 added to the theory as follows:

372 \begin{ttbox}

373 locale group =

374 fixes

375 G :: "'a grouptype"

376 e :: "'a"

377 binop :: "'a => 'a => 'a" (infixr "#" 80)

378 inv :: "'a => 'a" ("i(_)" [90] 91)

379 assumes

380 Group_G "G: Group"

381 defines

382 e_def "e == unit G"

383 binop_def "x # y == bin_op G x y"

384 inv_def "i(x) == inverse G x"

385 \end{ttbox}

387 \subsubsection{Polymorphism}

389 In contrast to polymorphic definitions in theories, the use of the

390 same type variable for the declaration of different locale constants in the

391 fixes part means \emph{the same} type. In other words, the scope of the

392 polymorphic variables is extended over all constant declarations of a locale.

393 In the above example \texttt{'a} refers to the same type which is fixed inside

394 the locale. In an exported theorem (see \S\ref{sec:locale-export}) the

395 constructors of locale \texttt{group} are polymorphic, yet only simultaneously

396 instantiatable.

398 \subsubsection{Nested Locales}

400 A locale can be defined as the extension of a previously defined

401 locale. This operation of extension is optional and is syntactically

402 expressed as

403 \begin{ttbox}

404 locale foo = bar + ...

405 \end{ttbox}

406 The locale \texttt{foo} builds on the constants and syntax of the locale {\tt

407 bar}. That is, all contents of the locale \texttt{bar} can be used in

408 definitions and rules of the corresponding parts of the locale {\tt

409 foo}. Although locale \texttt{foo} assumes the \texttt{fixes} part of \texttt{bar} it

410 does not automatically subsume its rules and definitions. Normally, one

411 expects to use locale \texttt{foo} only if locale \texttt{bar} is already

412 active. These aspects of use and activation of locales are considered in the

413 subsequent section.

416 \subsection{Locale Scope}

418 Locales are by default inactive, but they can be invoked. The list of

419 currently active locales is called \emph{scope}. The process of activating

420 them is called \emph{opening}; the reverse is \emph{closing}.

422 \subsubsection{Scope}

423 The locale scope is part of each theory. It is a dynamic stack containing

424 all active locales at a certain point in an interactive session.

425 The scope lives until all locales are explicitly closed. At one time there

426 can be more than one locale open. The contents of these various active

427 locales are all visible in the scope. In case of nested locales for example,

428 the nesting is actually reflected to the scope, which contains the nested

429 locales as layers. To check the state of the scope during a development the

430 function \texttt{Print\_scope} may be used. It displays the names of all open

431 locales on the scope. The function \texttt{print\_locales} applied to a theory

432 displays all locales contained in that theory and in addition also the

433 current scope.

435 The scope is manipulated by the commands for opening and closing of locales.

437 \subsubsection{Opening}

438 Locales can be \emph{opened} at any point during a session where

439 we want to prove theorems concerning the locale. Opening a locale means

440 making its contents visible by pushing it onto the scope of the current

441 theory. Inside a scope of opened locales, theorems can use all definitions and

442 rules contained in the locales on the scope. The rules and definitions may

443 be accessed individually using the function \ttindex{thm}. This function is

444 applied to the names assigned to locale rules and definitions as

445 strings. The opening command is called \texttt{Open\_locale} and takes the

446 name of the locale to be opened as its argument.

448 If one opens a locale \texttt{foo} that is defined by extension from locale

449 \texttt{bar}, the function \texttt{Open\_locale} checks if locale \texttt{bar}

450 is open. If so, then it just opens \texttt{foo}, if not, then it prints a

451 message and opens \texttt{bar} before opening \texttt{foo}. Naturally, this

452 carries on, if \texttt{bar} is again an extension.

454 \subsubsection{Closing}

456 \emph{Closing} means to cancel the last opened locale, pushing it out of the

457 scope. Theorems proved during the life cycle of this locale will be disabled,

458 unless they have been explicitly exported, as described below. However, when

459 the same locale is opened again these theorems may be used again as well,

460 provided that they were saved as theorems in the first place, using

461 \texttt{qed} or ML assignment. The command \texttt{Close\_locale} takes a

462 locale name as a string and checks if this locale is actually the topmost

463 locale on the scope. If this is the case, it removes this locale, otherwise

464 it prints a warning message and does not change the scope.

466 \subsubsection{Export of Theorems}

467 \label{sec:locale-export}

469 Export of theorems transports theorems out of the scope of locales. Locale

470 rules that have been used in the proof of an exported theorem inside the

471 locale are carried by the exported form of the theorem as its individual

472 meta-assumptions. The locale constants are universally quantified variables

473 in these theorems, hence such theorems can be instantiated individually.

474 Definitions become unfolded; locale constants that were merely used for

475 definitions vanish. Logically, exporting corresponds to a combined

476 application of introduction rules for implication and universal

477 quantification. Exporting forms a kind of normalization of theorems in a

478 locale scope.

480 According to the possibility of nested locales there are two different forms

481 of export. The first one is realized by the function \texttt{export} that

482 exports theorems through all layers of opened locales of the scope. Hence,

483 the application of export to a theorem yields a theorem of the global level,

484 that is, the current theory context without any local assumptions or

485 definitions.

487 When locales are nested we might want to export a theorem, not to the global

488 level of the current theory but just to the previous level. The other export

489 function, \texttt{Export}, transports theorems one level up in the scope; the

490 theorem still uses locale constants, definitions and rules of the locales

491 underneath.

493 \subsection{Functions for Locales}

494 \label{Syntax}

495 \index{locales!functions}

497 Here is a quick reference list of locale functions.

498 \begin{ttbox}

499 Open_locale : xstring -> unit

500 Close_locale : xstring -> unit

501 export : thm -> thm

502 Export : thm -> thm

503 thm : xstring -> thm

504 Print_scope : unit -> unit

505 print_locales: theory -> unit

506 \end{ttbox}

507 \begin{ttdescription}

508 \item[\ttindexbold{Open_locale} $xstring$]

509 opens the locale {\it xstring}, adding it to the scope of the theory of the

510 current context. If the opened locale is built by extension, the ancestors

511 are opened automatically.

513 \item[\ttindexbold{Close_locale} $xstring$] eliminates the locale {\it

514 xstring} from the scope if it is the topmost item on it, otherwise it does

515 not change the scope and produces a warning.

517 \item[\ttindexbold{export} $thm$] locale definitions become expanded in {\it

518 thm} and locale rules that were used in the proof of {\it thm} become part

519 of its individual assumptions. This normalization happens with respect to

520 \emph{all open locales} on the scope.

522 \item[\ttindexbold{Export} $thm$] works like \texttt{export} but normalizes

523 theorems only up to the previous level of locales on the scope.

525 \item[\ttindexbold{thm} $xstring$] applied to the name of a locale definition

526 or rule it returns the definition as a theorem.

528 \item[\ttindexbold{Print_scope}()] prints the names of the locales in the

529 current scope of the current theory context.

531 \item[\ttindexbold{print_locale} $theory$] prints all locales that are

532 contained in {\it theory} directly or indirectly. It also displays the

533 current scope similar to \texttt{Print\_scope}.

534 \end{ttdescription}

537 \section{Basic operations on theories}\label{BasicOperationsOnTheories}

539 \subsection{*Theory inclusion}

540 \begin{ttbox}

541 subthy : theory * theory -> bool

542 eq_thy : theory * theory -> bool

543 transfer : theory -> thm -> thm

544 transfer_sg : Sign.sg -> thm -> thm

545 \end{ttbox}

547 Inclusion and equality of theories is determined by unique

548 identification stamps that are created when declaring new components.

549 Theorems contain a reference to the theory (actually to its signature)

550 they have been derived in. Transferring theorems to super theories

551 has no logical significance, but may affect some operations in subtle

552 ways (e.g.\ implicit merges of signatures when applying rules, or

553 pretty printing of theorems).

555 \begin{ttdescription}

557 \item[\ttindexbold{subthy} ($thy@1$, $thy@2$)] determines if $thy@1$

558 is included in $thy@2$ wrt.\ identification stamps.

560 \item[\ttindexbold{eq_thy} ($thy@1$, $thy@2$)] determines if $thy@1$

561 is exactly the same as $thy@2$.

563 \item[\ttindexbold{transfer} $thy$ $thm$] transfers theorem $thm$ to

564 theory $thy$, provided the latter includes the theory of $thm$.

566 \item[\ttindexbold{transfer_sg} $sign$ $thm$] is similar to

567 \texttt{transfer}, but identifies the super theory via its

568 signature.

570 \end{ttdescription}

573 \subsection{*Primitive theories}

574 \begin{ttbox}

575 ProtoPure.thy : theory

576 Pure.thy : theory

577 CPure.thy : theory

578 \end{ttbox}

579 \begin{description}

580 \item[\ttindexbold{ProtoPure.thy}, \ttindexbold{Pure.thy},

581 \ttindexbold{CPure.thy}] contain the syntax and signature of the

582 meta-logic. There are basically no axioms: meta-level inferences

583 are carried out by \ML\ functions. \texttt{Pure} and \texttt{CPure}

584 just differ in their concrete syntax of prefix function application:

585 $t(u@1, \ldots, u@n)$ in \texttt{Pure} vs.\ $t\,u@1,\ldots\,u@n$ in

586 \texttt{CPure}. \texttt{ProtoPure} is their common parent,

587 containing no syntax for printing prefix applications at all!

589 %% FIXME

590 %\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"} $\cdots$] extends

591 % the theory $thy$ with new types, constants, etc. $T$ identifies the theory

592 % internally. When a theory is redeclared, say to change an incorrect axiom,

593 % bindings to the old axiom may persist. Isabelle ensures that the old and

594 % new theories are not involved in the same proof. Attempting to combine

595 % different theories having the same name $T$ yields the fatal error

596 %extend_theory : theory -> string -> \(\cdots\) -> theory

597 %\begin{ttbox}

598 %Attempt to merge different versions of theory: \(T\)

599 %\end{ttbox}

600 \end{description}

602 %% FIXME

603 %\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"}

604 % ($classes$, $default$, $types$, $arities$, $consts$, $sextopt$) $rules$]

605 %\hfill\break %%% include if line is just too short

606 %is the \ML{} equivalent of the following theory definition:

607 %\begin{ttbox}

608 %\(T\) = \(thy\) +

609 %classes \(c\) < \(c@1\),\(\dots\),\(c@m\)

610 % \dots

611 %default {\(d@1,\dots,d@r\)}

612 %types \(tycon@1\),\dots,\(tycon@i\) \(n\)

613 % \dots

614 %arities \(tycon@1'\),\dots,\(tycon@j'\) :: (\(s@1\),\dots,\(s@n\))\(c\)

615 % \dots

616 %consts \(b@1\),\dots,\(b@k\) :: \(\tau\)

617 % \dots

618 %rules \(name\) \(rule\)

619 % \dots

620 %end

621 %\end{ttbox}

622 %where

623 %\begin{tabular}[t]{l@{~=~}l}

624 %$classes$ & \tt[("$c$",["$c@1$",\dots,"$c@m$"]),\dots] \\

625 %$default$ & \tt["$d@1$",\dots,"$d@r$"]\\

626 %$types$ & \tt[([$tycon@1$,\dots,$tycon@i$], $n$),\dots] \\

627 %$arities$ & \tt[([$tycon'@1$,\dots,$tycon'@j$], ([$s@1$,\dots,$s@n$],$c$)),\dots]

628 %\\

629 %$consts$ & \tt[([$b@1$,\dots,$b@k$],$\tau$),\dots] \\

630 %$rules$ & \tt[("$name$",$rule$),\dots]

631 %\end{tabular}

634 \subsection{Inspecting a theory}\label{sec:inspct-thy}

635 \index{theories!inspecting|bold}

636 \begin{ttbox}

637 print_syntax : theory -> unit

638 print_theory : theory -> unit

639 parents_of : theory -> theory list

640 ancestors_of : theory -> theory list

641 sign_of : theory -> Sign.sg

642 Sign.stamp_names_of : Sign.sg -> string list

643 \end{ttbox}

644 These provide means of viewing a theory's components.

645 \begin{ttdescription}

646 \item[\ttindexbold{print_syntax} $thy$] prints the syntax of $thy$

647 (grammar, macros, translation functions etc., see

648 page~\pageref{pg:print_syn} for more details).

650 \item[\ttindexbold{print_theory} $thy$] prints the logical parts of

651 $thy$, excluding the syntax.

653 \item[\ttindexbold{parents_of} $thy$] returns the direct ancestors

654 of~$thy$.

656 \item[\ttindexbold{ancestors_of} $thy$] returns all ancestors of~$thy$

657 (not including $thy$ itself).

659 \item[\ttindexbold{sign_of} $thy$] returns the signature associated

660 with~$thy$. It is useful with functions like {\tt

661 read_instantiate_sg}, which take a signature as an argument.

663 \item[\ttindexbold{Sign.stamp_names_of} $sg$]\index{signatures}

664 returns the names of the identification \rmindex{stamps} of ax

665 signature. These coincide with the names of its full ancestry

666 including that of $sg$ itself.

668 \end{ttdescription}

671 \section{Terms}

672 \index{terms|bold}

673 Terms belong to the \ML\ type \mltydx{term}, which is a concrete datatype

674 with six constructors:

675 \begin{ttbox}

676 type indexname = string * int;

677 infix 9 $;

678 datatype term = Const of string * typ

679 | Free of string * typ

680 | Var of indexname * typ

681 | Bound of int

682 | Abs of string * typ * term

683 | op $ of term * term;

684 \end{ttbox}

685 \begin{ttdescription}

686 \item[\ttindexbold{Const} ($a$, $T$)] \index{constants|bold}

687 is the \textbf{constant} with name~$a$ and type~$T$. Constants include

688 connectives like $\land$ and $\forall$ as well as constants like~0

689 and~$Suc$. Other constants may be required to define a logic's concrete

690 syntax.

692 \item[\ttindexbold{Free} ($a$, $T$)] \index{variables!free|bold}

693 is the \textbf{free variable} with name~$a$ and type~$T$.

695 \item[\ttindexbold{Var} ($v$, $T$)] \index{unknowns|bold}

696 is the \textbf{scheme variable} with indexname~$v$ and type~$T$. An

697 \mltydx{indexname} is a string paired with a non-negative index, or

698 subscript; a term's scheme variables can be systematically renamed by

699 incrementing their subscripts. Scheme variables are essentially free

700 variables, but may be instantiated during unification.

702 \item[\ttindexbold{Bound} $i$] \index{variables!bound|bold}

703 is the \textbf{bound variable} with de Bruijn index~$i$, which counts the

704 number of lambdas, starting from zero, between a variable's occurrence

705 and its binding. The representation prevents capture of variables. For

706 more information see de Bruijn \cite{debruijn72} or

707 Paulson~\cite[page~376]{paulson-ml2}.

709 \item[\ttindexbold{Abs} ($a$, $T$, $u$)]

710 \index{lambda abs@$\lambda$-abstractions|bold}

711 is the $\lambda$-\textbf{abstraction} with body~$u$, and whose bound

712 variable has name~$a$ and type~$T$. The name is used only for parsing

713 and printing; it has no logical significance.

715 \item[$t$ \$ $u$] \index{$@{\tt\$}|bold} \index{function applications|bold}

716 is the \textbf{application} of~$t$ to~$u$.

717 \end{ttdescription}

718 Application is written as an infix operator to aid readability. Here is an

719 \ML\ pattern to recognize FOL formulae of the form~$A\imp B$, binding the

720 subformulae to~$A$ and~$B$:

721 \begin{ttbox}

722 Const("Trueprop",_) $ (Const("op -->",_) $ A $ B)

723 \end{ttbox}

726 \section{*Variable binding}

727 \begin{ttbox}

728 loose_bnos : term -> int list

729 incr_boundvars : int -> term -> term

730 abstract_over : term*term -> term

731 variant_abs : string * typ * term -> string * term

732 aconv : term * term -> bool\hfill\textbf{infix}

733 \end{ttbox}

734 These functions are all concerned with the de Bruijn representation of

735 bound variables.

736 \begin{ttdescription}

737 \item[\ttindexbold{loose_bnos} $t$]

738 returns the list of all dangling bound variable references. In

739 particular, \texttt{Bound~0} is loose unless it is enclosed in an

740 abstraction. Similarly \texttt{Bound~1} is loose unless it is enclosed in

741 at least two abstractions; if enclosed in just one, the list will contain

742 the number 0. A well-formed term does not contain any loose variables.

744 \item[\ttindexbold{incr_boundvars} $j$]

745 increases a term's dangling bound variables by the offset~$j$. This is

746 required when moving a subterm into a context where it is enclosed by a

747 different number of abstractions. Bound variables with a matching

748 abstraction are unaffected.

750 \item[\ttindexbold{abstract_over} $(v,t)$]

751 forms the abstraction of~$t$ over~$v$, which may be any well-formed term.

752 It replaces every occurrence of \(v\) by a \texttt{Bound} variable with the

753 correct index.

755 \item[\ttindexbold{variant_abs} $(a,T,u)$]

756 substitutes into $u$, which should be the body of an abstraction.

757 It replaces each occurrence of the outermost bound variable by a free

758 variable. The free variable has type~$T$ and its name is a variant

759 of~$a$ chosen to be distinct from all constants and from all variables

760 free in~$u$.

762 \item[$t$ \ttindexbold{aconv} $u$]

763 tests whether terms~$t$ and~$u$ are \(\alpha\)-convertible: identical up

764 to renaming of bound variables.

765 \begin{itemize}

766 \item

767 Two constants, \texttt{Free}s, or \texttt{Var}s are \(\alpha\)-convertible

768 if their names and types are equal.

769 (Variables having the same name but different types are thus distinct.

770 This confusing situation should be avoided!)

771 \item

772 Two bound variables are \(\alpha\)-convertible

773 if they have the same number.

774 \item

775 Two abstractions are \(\alpha\)-convertible

776 if their bodies are, and their bound variables have the same type.

777 \item

778 Two applications are \(\alpha\)-convertible

779 if the corresponding subterms are.

780 \end{itemize}

782 \end{ttdescription}

784 \section{Certified terms}\index{terms!certified|bold}\index{signatures}

785 A term $t$ can be \textbf{certified} under a signature to ensure that every type

786 in~$t$ is well-formed and every constant in~$t$ is a type instance of a

787 constant declared in the signature. The term must be well-typed and its use

788 of bound variables must be well-formed. Meta-rules such as \texttt{forall_elim}

789 take certified terms as arguments.

791 Certified terms belong to the abstract type \mltydx{cterm}.

792 Elements of the type can only be created through the certification process.

793 In case of error, Isabelle raises exception~\ttindex{TERM}\@.

795 \subsection{Printing terms}

796 \index{terms!printing of}

797 \begin{ttbox}

798 string_of_cterm : cterm -> string

799 Sign.string_of_term : Sign.sg -> term -> string

800 \end{ttbox}

801 \begin{ttdescription}

802 \item[\ttindexbold{string_of_cterm} $ct$]

803 displays $ct$ as a string.

805 \item[\ttindexbold{Sign.string_of_term} $sign$ $t$]

806 displays $t$ as a string, using the syntax of~$sign$.

807 \end{ttdescription}

809 \subsection{Making and inspecting certified terms}

810 \begin{ttbox}

811 cterm_of : Sign.sg -> term -> cterm

812 read_cterm : Sign.sg -> string * typ -> cterm

813 cert_axm : Sign.sg -> string * term -> string * term

814 read_axm : Sign.sg -> string * string -> string * term

815 rep_cterm : cterm -> \{T:typ, t:term, sign:Sign.sg, maxidx:int\}

816 Sign.certify_term : Sign.sg -> term -> term * typ * int

817 \end{ttbox}

818 \begin{ttdescription}

820 \item[\ttindexbold{cterm_of} $sign$ $t$] \index{signatures} certifies

821 $t$ with respect to signature~$sign$.

823 \item[\ttindexbold{read_cterm} $sign$ ($s$, $T$)] reads the string~$s$

824 using the syntax of~$sign$, creating a certified term. The term is

825 checked to have type~$T$; this type also tells the parser what kind

826 of phrase to parse.

828 \item[\ttindexbold{cert_axm} $sign$ ($name$, $t$)] certifies $t$ with

829 respect to $sign$ as a meta-proposition and converts all exceptions

830 to an error, including the final message

831 \begin{ttbox}

832 The error(s) above occurred in axiom "\(name\)"

833 \end{ttbox}

835 \item[\ttindexbold{read_axm} $sign$ ($name$, $s$)] similar to {\tt

836 cert_axm}, but first reads the string $s$ using the syntax of

837 $sign$.

839 \item[\ttindexbold{rep_cterm} $ct$] decomposes $ct$ as a record

840 containing its type, the term itself, its signature, and the maximum

841 subscript of its unknowns. The type and maximum subscript are

842 computed during certification.

844 \item[\ttindexbold{Sign.certify_term}] is a more primitive version of

845 \texttt{cterm_of}, returning the internal representation instead of

846 an abstract \texttt{cterm}.

848 \end{ttdescription}

851 \section{Types}\index{types|bold}

852 Types belong to the \ML\ type \mltydx{typ}, which is a concrete datatype with

853 three constructor functions. These correspond to type constructors, free

854 type variables and schematic type variables. Types are classified by sorts,

855 which are lists of classes (representing an intersection). A class is

856 represented by a string.

857 \begin{ttbox}

858 type class = string;

859 type sort = class list;

861 datatype typ = Type of string * typ list

862 | TFree of string * sort

863 | TVar of indexname * sort;

865 infixr 5 -->;

866 fun S --> T = Type ("fun", [S, T]);

867 \end{ttbox}

868 \begin{ttdescription}

869 \item[\ttindexbold{Type} ($a$, $Ts$)] \index{type constructors|bold}

870 applies the \textbf{type constructor} named~$a$ to the type operand list~$Ts$.

871 Type constructors include~\tydx{fun}, the binary function space

872 constructor, as well as nullary type constructors such as~\tydx{prop}.

873 Other type constructors may be introduced. In expressions, but not in

874 patterns, \hbox{\tt$S$-->$T$} is a convenient shorthand for function

875 types.

877 \item[\ttindexbold{TFree} ($a$, $s$)] \index{type variables|bold}

878 is the \textbf{type variable} with name~$a$ and sort~$s$.

880 \item[\ttindexbold{TVar} ($v$, $s$)] \index{type unknowns|bold}

881 is the \textbf{type unknown} with indexname~$v$ and sort~$s$.

882 Type unknowns are essentially free type variables, but may be

883 instantiated during unification.

884 \end{ttdescription}

887 \section{Certified types}

888 \index{types!certified|bold}

889 Certified types, which are analogous to certified terms, have type

890 \ttindexbold{ctyp}.

892 \subsection{Printing types}

893 \index{types!printing of}

894 \begin{ttbox}

895 string_of_ctyp : ctyp -> string

896 Sign.string_of_typ : Sign.sg -> typ -> string

897 \end{ttbox}

898 \begin{ttdescription}

899 \item[\ttindexbold{string_of_ctyp} $cT$]

900 displays $cT$ as a string.

902 \item[\ttindexbold{Sign.string_of_typ} $sign$ $T$]

903 displays $T$ as a string, using the syntax of~$sign$.

904 \end{ttdescription}

907 \subsection{Making and inspecting certified types}

908 \begin{ttbox}

909 ctyp_of : Sign.sg -> typ -> ctyp

910 rep_ctyp : ctyp -> \{T: typ, sign: Sign.sg\}

911 Sign.certify_typ : Sign.sg -> typ -> typ

912 \end{ttbox}

913 \begin{ttdescription}

915 \item[\ttindexbold{ctyp_of} $sign$ $T$] \index{signatures} certifies

916 $T$ with respect to signature~$sign$.

918 \item[\ttindexbold{rep_ctyp} $cT$] decomposes $cT$ as a record

919 containing the type itself and its signature.

921 \item[\ttindexbold{Sign.certify_typ}] is a more primitive version of

922 \texttt{ctyp_of}, returning the internal representation instead of

923 an abstract \texttt{ctyp}.

925 \end{ttdescription}

928 \section{Oracles: calling trusted external reasoners}

929 \label{sec:oracles}

930 \index{oracles|(}

932 Oracles allow Isabelle to take advantage of external reasoners such as

933 arithmetic decision procedures, model checkers, fast tautology checkers or

934 computer algebra systems. Invoked as an oracle, an external reasoner can

935 create arbitrary Isabelle theorems. It is your responsibility to ensure that

936 the external reasoner is as trustworthy as your application requires.

937 Isabelle's proof objects~(\S\ref{sec:proofObjects}) record how each theorem

938 depends upon oracle calls.

940 \begin{ttbox}

941 invoke_oracle : theory -> xstring -> Sign.sg * object -> thm

942 Theory.add_oracle : bstring * (Sign.sg * object -> term) -> theory

943 -> theory

944 \end{ttbox}

945 \begin{ttdescription}

946 \item[\ttindexbold{invoke_oracle} $thy$ $name$ ($sign$, $data$)]

947 invokes the oracle $name$ of theory $thy$ passing the information

948 contained in the exception value $data$ and creating a theorem

949 having signature $sign$. Note that type \ttindex{object} is just an

950 abbreviation for \texttt{exn}. Errors arise if $thy$ does not have

951 an oracle called $name$, if the oracle rejects its arguments or if

952 its result is ill-typed.

954 \item[\ttindexbold{Theory.add_oracle} $name$ $fun$ $thy$] extends

955 $thy$ by oracle $fun$ called $name$. It is seldom called

956 explicitly, as there is concrete syntax for oracles in theory files.

957 \end{ttdescription}

959 A curious feature of {\ML} exceptions is that they are ordinary constructors.

960 The {\ML} type \texttt{exn} is a datatype that can be extended at any time. (See

961 my {\em {ML} for the Working Programmer}~\cite{paulson-ml2}, especially

962 page~136.) The oracle mechanism takes advantage of this to allow an oracle to

963 take any information whatever.

965 There must be some way of invoking the external reasoner from \ML, either

966 because it is coded in {\ML} or via an operating system interface. Isabelle

967 expects the {\ML} function to take two arguments: a signature and an

968 exception object.

969 \begin{itemize}

970 \item The signature will typically be that of a desendant of the theory

971 declaring the oracle. The oracle will use it to distinguish constants from

972 variables, etc., and it will be attached to the generated theorems.

974 \item The exception is used to pass arbitrary information to the oracle. This

975 information must contain a full description of the problem to be solved by

976 the external reasoner, including any additional information that might be

977 required. The oracle may raise the exception to indicate that it cannot

978 solve the specified problem.

979 \end{itemize}

981 A trivial example is provided in theory \texttt{FOL/ex/IffOracle}. This

982 oracle generates tautologies of the form $P\bimp\cdots\bimp P$, with

983 an even number of $P$s.

985 The \texttt{ML} section of \texttt{IffOracle.thy} begins by declaring

986 a few auxiliary functions (suppressed below) for creating the

987 tautologies. Then it declares a new exception constructor for the

988 information required by the oracle: here, just an integer. It finally

989 defines the oracle function itself.

990 \begin{ttbox}

991 exception IffOracleExn of int;\medskip

992 fun mk_iff_oracle (sign, IffOracleExn n) =

993 if n > 0 andalso n mod 2 = 0

994 then Trueprop \$ mk_iff n

995 else raise IffOracleExn n;

996 \end{ttbox}

997 Observe the function's two arguments, the signature \texttt{sign} and the

998 exception given as a pattern. The function checks its argument for

999 validity. If $n$ is positive and even then it creates a tautology

1000 containing $n$ occurrences of~$P$. Otherwise it signals error by

1001 raising its own exception (just by happy coincidence). Errors may be

1002 signalled by other means, such as returning the theorem \texttt{True}.

1003 Please ensure that the oracle's result is correctly typed; Isabelle

1004 will reject ill-typed theorems by raising a cryptic exception at top

1005 level.

1007 The \texttt{oracle} section of \texttt{IffOracle.thy} installs above

1008 \texttt{ML} function as follows:

1009 \begin{ttbox}

1010 IffOracle = FOL +\medskip

1011 oracle

1012 iff = mk_iff_oracle\medskip

1013 end

1014 \end{ttbox}

1016 Now in \texttt{IffOracle.ML} we first define a wrapper for invoking

1017 the oracle:

1018 \begin{ttbox}

1019 fun iff_oracle n = invoke_oracle IffOracle.thy "iff"

1020 (sign_of IffOracle.thy, IffOracleExn n);

1021 \end{ttbox}

1023 Here are some example applications of the \texttt{iff} oracle. An

1024 argument of 10 is allowed, but one of 5 is forbidden:

1025 \begin{ttbox}

1026 iff_oracle 10;

1027 {\out "P <-> P <-> P <-> P <-> P <-> P <-> P <-> P <-> P <-> P" : thm}

1028 iff_oracle 5;

1029 {\out Exception- IffOracleExn 5 raised}

1030 \end{ttbox}

1032 \index{oracles|)}

1033 \index{theories|)}

1036 %%% Local Variables:

1037 %%% mode: latex

1038 %%% TeX-master: "ref"

1039 %%% End: