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

doc-src/Ref/theories.tex

author | clasohm |

Fri Dec 01 12:27:09 1995 +0100 (1995-12-01) | |

changeset 1380 | 2f8055af9c04 |

parent 1369 | b82815e61b30 |

child 1387 | 9bcad9c22fd4 |

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

changed HTML documentation

1 %% $Id$

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

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

5 \index{reading!axioms|see{{\tt assume_ax}}}

6 Theories organize the syntax, declarations and axioms of a mathematical

7 development. They are built, starting from the Pure theory, by extending

8 and merging existing theories. They have the \ML\ type \mltydx{theory}.

9 Theory operations signal errors by raising exception \xdx{THEORY},

10 returning a message and a list of theories.

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

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

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

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

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

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

18 also merged. Every theory carries a unique signature.

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

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

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

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

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

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

29 Theories are usually defined using theory definition files (which have a name

30 suffix {\tt .thy}). There is also a low level interface provided by certain

31 \ML{} functions (see \S\ref{BuildingATheory}).

32 Appendix~\ref{app:TheorySyntax} presents the concrete syntax for theory

33 definitions; here is an explanation of the constituent parts:

34 \begin{description}

35 \item[{\it theoryDef}]

36 is the full definition. The new theory is called $id$. It is the union

37 of the named {\bf parent theories}\indexbold{theories!parent}, possibly

38 extended with new classes, etc. The basic theory, which contains only

39 the meta-logic, is called \thydx{Pure}.

41 Normally each {\it name\/} is an identifier, the name of the parent theory.

42 Quoted strings can be used to document additional file dependencies; see

43 \S\ref{LoadingTheories} for details.

45 \item[$classes$]

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

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

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

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

50 necessary to declare {\tt c < e} in addition to {\tt c < d} and {\tt d <

51 e}.

53 \item[$default$]

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

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

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

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

58 intersection).

60 \item[$sort$]

61 is a finite set of classes. A single class $id$ abbreviates the singleton

62 set {\tt\{}$id${\tt\}}.

64 \item[$types$]

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

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

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

68 indicate the number~$n$.

70 A {\bf type synonym}\indexbold{type synonyms} is an abbreviation

71 $(\alpha@1,\dots,\alpha@n)name = \mbox{\tt"}\tau\mbox{\tt"}$, where

72 $name$ can be a string and $\tau$ must be enclosed in quotation marks.

74 \item[$infix$]

75 declares a type or constant to be an infix operator of priority $nat$

76 associating to the left ({\tt infixl}) or right ({\tt infixr}). Only

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

78 ('a,'b)~"*"~(infixr~20)}, which expresses binary product types.

80 \item[$arities$]

81 is a series of arity declarations. Each assigns arities to type

82 constructors. The $name$ must be an existing type constructor, which is

83 given the additional arity $arity$.

85 \item[$constDecl$]

86 is a series of constant declarations. Each new constant $name$ is given

87 the specified type. The optional $mixfix$ annotations may

88 attach concrete syntax to the constant. A variant of {\tt consts} is the

89 {\tt syntax} section\index{*syntax section}, which adds just syntax without

90 declaring logical constants.

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

93 annotations can take three forms:

94 \begin{itemize}

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

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

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

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

99 the priority of the whole construct.

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

102 infix} status.

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

105 binder} status. The declaration {\tt binder} $\cal Q$ $p$ causes

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

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

108 \end{itemize}

110 \item[$trans$]

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

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

113 ==}).

115 \item[$rule$]

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

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

118 theory file.

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

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

122 \end{description}

123 %

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

125 declarations, translation rules and the {\tt ML} section in more detail.

128 \subsection{*Classes and arities}

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

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

132 arity declarations must obey two conditions:

133 \begin{itemize}

134 \item There must be no two declarations $ty :: (\vec{r})c$ and $ty ::

135 (\vec{s})c$ with $\vec{r} \neq \vec{s}$. For example, the following is

136 forbidden:

137 \begin{ttbox}

138 types

139 'a ty

140 arities

141 ty :: ({\ttlbrace}logic{\ttrbrace}) logic

142 ty :: ({\ttlbrace}{\ttrbrace})logic

143 \end{ttbox}

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

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

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

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

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

150 types represented by $s$. For example, the following is forbidden:

151 \begin{ttbox}

152 classes

153 term < logic

154 types

155 'a ty

156 arities

157 ty :: ({\ttlbrace}logic{\ttrbrace})logic

158 ty :: ({\ttlbrace}{\ttrbrace})term

159 \end{ttbox}

161 \end{itemize}

164 \section{Loading a new theory}\label{LoadingTheories}

165 \index{theories!loading}\index{files!reading}

166 \begin{ttbox}

167 use_thy : string -> unit

168 time_use_thy : string -> unit

169 loadpath : string list ref \hfill{\bf initially {\tt["."]}}

170 delete_tmpfiles : bool ref \hfill{\bf initially true}

171 \end{ttbox}

173 \begin{ttdescription}

174 \item[\ttindexbold{use_thy} $thyname$]

175 reads the theory $thyname$ and creates an \ML{} structure as described below.

177 \item[\ttindexbold{time_use_thy} $thyname$]

178 calls {\tt use_thy} $thyname$ and reports the time taken.

180 \item[\ttindexbold{loadpath}]

181 contains a list of directories to search when locating the files that

182 define a theory. This list is only used if the theory name in {\tt

183 use_thy} does not specify the path explicitly.

185 \item[\ttindexbold{delete_tmpfiles} := false;]

186 suppresses the deletion of temporary files.

187 \end{ttdescription}

188 %

189 Each theory definition must reside in a separate file. Let the file {\it

190 T}{\tt.thy} contain the definition of a theory called~$T$, whose parent

191 theories are $TB@1$ \dots $TB@n$. Calling \ttindexbold{use_thy}~{\tt"{\it

192 T\/}"} reads the file {\it T}{\tt.thy}, writes a temporary \ML{}

193 file {\tt.{\it T}.thy.ML}, and reads the latter file. Recursive {\tt

194 use_thy} calls load those parent theories that have not been loaded

195 previously; the recursive calls may continue to any depth. One {\tt use_thy}

196 call can read an entire logic provided all theories are linked appropriately.

198 The result is an \ML\ structure~$T$ containing at least a component {\tt thy}

199 for the new theory and components for each of the rules. The structure also

200 contains the definitions of the {\tt ML} section, if present. The file

201 {\tt.{\it T}.thy.ML} is then deleted if {\tt delete_tmpfiles} is set to {\tt

202 true} and no errors occurred.

204 Finally the file {\it T}{\tt.ML} is read, if it exists. This file normally

205 begins with the declaration {\tt open~$T$} and contains proofs involving

206 the new theory.

208 Some applications construct theories directly by calling \ML\ functions. In

209 this situation there is no {\tt.thy} file, only an {\tt.ML} file. The

210 {\tt.ML} file must declare an \ML\ structure having the theory's name and a

211 component {\tt thy} containing the new theory object.

212 Section~\ref{sec:pseudo-theories} below describes a way of linking such

213 theories to their parents.

215 \begin{warn}

216 Temporary files are written to the current directory, so this must be

217 writable. Isabelle inherits the current directory from the operating

218 system; you can change it within Isabelle by typing {\tt

219 cd"$dir$"}\index{*cd}.

220 \end{warn}

223 \section{Reloading modified theories}\label{sec:reloading-theories}

224 \indexbold{theories!reloading}

225 \begin{ttbox}

226 update : unit -> unit

227 unlink_thy : string -> unit

228 \end{ttbox}

229 Changing a theory on disk often makes it necessary to reload all theories

230 descended from it. However, {\tt use_thy} reads only one theory, even if

231 some of the parent theories are out of date. In this case you should call

232 {\tt update()}.

234 Isabelle keeps track of all loaded theories and their files. If

235 \ttindex{use_thy} finds that the theory to be loaded has been read before,

236 it determines whether to reload the theory as follows. First it looks for

237 the theory's files in their previous location. If it finds them, it

238 compares their modification times to the internal data and stops if they

239 are equal. If the files have been moved, {\tt use_thy} searches for them

240 as it would for a new theory. After {\tt use_thy} reloads a theory, it

241 marks the children as out-of-date.

243 \begin{ttdescription}

244 \item[\ttindexbold{update}()]

245 reloads all modified theories and their descendants in the correct order.

247 \item[\ttindexbold{unlink_thy} $thyname$]\indexbold{theories!removing}

248 informs Isabelle that theory $thyname$ no longer exists. If you delete the

249 theory files for $thyname$ then you must execute {\tt unlink_thy};

250 otherwise {\tt update} will complain about a missing file.

251 \end{ttdescription}

254 \goodbreak

255 \subsection{Important note for Poly/ML users}\index{Poly/{\ML} compiler}

256 The theory mechanism depends upon reference variables. At the end of a

257 Poly/\ML{} session, the contents of references are lost unless they are

258 declared in the current database. In particular, assignments to references

259 of the {\tt Pure} database are lost, including all information about loaded

260 theories. To avoid losing this information simply call

261 \begin{ttbox}

262 init_thy_reader();

263 \end{ttbox}

264 when building the new database.

267 \subsection{*Pseudo theories}\label{sec:pseudo-theories}

268 \indexbold{theories!pseudo}%

269 Any automatic reloading facility requires complete knowledge of all

270 dependencies. Sometimes theories depend on objects created in \ML{} files

271 with no associated theory definition file. These objects may be theories but

272 they could also be theorems, proof procedures, etc.

274 Unless such dependencies are documented, {\tt update} fails to reload these

275 \ML{} files and the system is left in a state where some objects, such as

276 theorems, still refer to old versions of theories. This may lead to the

277 error

278 \begin{ttbox}

279 Attempt to merge different versions of theories: \dots

280 \end{ttbox}

281 Therefore there is a way to link theories and {\bf orphaned} \ML{} files ---

282 those not associated with a theory definition.

284 Let us assume we have an orphaned \ML{} file named {\tt orphan.ML} and a

285 theory~$B$ that depends on {\tt orphan.ML} --- for example, {\tt B.ML} uses

286 theorems proved in {\tt orphan.ML}. Then {\tt B.thy} should

287 mention this dependency as follows:

288 \begin{ttbox}

289 B = \(\ldots\) + "orphan" + \(\ldots\)

290 \end{ttbox}

291 Quoted strings stand for theories which have to be loaded before the

292 current theory is read but which are not used in building the base of

293 theory~$B$. Whenever {\tt orphan} changes and is reloaded, Isabelle

294 knows that $B$ has to be updated, too.

296 Note that it's necessary for {\tt orphan} to declare a special ML

297 object of type {\tt theory} which is present in all theories. This is

298 normally achieved by adding the file {\tt orphan.thy} to make {\tt

299 orphan} a {\bf pseudo theory}. A minimum version of {\tt orphan.thy}

300 would be

302 \begin{ttbox}

303 orphan = Pure

304 \end{ttbox}

306 which uses {\tt Pure} to make a dummy theory. Normally though the

307 orphaned file has its own dependencies. If {\tt orphan.ML} depends on

308 theories or files $A@1$, \ldots, $A@n$, record this by creating the

309 pseudo theory in the following way:

310 \begin{ttbox}

311 orphan = \(A@1\) + \(\ldots\) + \(A@n\)

312 \end{ttbox}

313 The resulting theory ensures that {\tt update} reloads {\tt orphan}

314 whenever it reloads one of the $A@i$.

316 For an extensive example of how this technique can be used to link lots of

317 theory files and load them by just a few {\tt use_thy} calls, consult the

318 sources of \ZF{} set theory.

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

323 \subsection{Extracting an axiom or theorem from a theory}

324 \index{theories!axioms of}\index{axioms!extracting}

325 \index{theories!theorems of}\index{theorems!extracting}

326 \begin{ttbox}

327 get_axiom : theory -> string -> thm

328 get_thm : theory -> string -> thm

329 assume_ax : theory -> string -> thm

330 \end{ttbox}

331 \begin{ttdescription}

332 \item[\ttindexbold{get_axiom} $thy$ $name$]

333 returns an axiom with the given $name$ from $thy$, raising exception

334 \xdx{THEORY} if none exists. Merging theories can cause several axioms

335 to have the same name; {\tt get_axiom} returns an arbitrary one.

337 \item[\ttindexbold{get_thm} $thy$ $name$]

338 is analogous to {\tt get_axiom}, but looks for a stored theorem. Like

339 {\tt get_axiom} it searches all parents of a theory if the theorem

340 is not associated with $thy$.

342 \item[\ttindexbold{assume_ax} $thy$ $formula$]

343 reads the {\it formula} using the syntax of $thy$, following the same

344 conventions as axioms in a theory definition. You can thus pretend that

345 {\it formula} is an axiom and use the resulting theorem like an axiom.

346 Actually {\tt assume_ax} returns an assumption; \ttindex{result}

347 complains about additional assumptions, but \ttindex{uresult} does not.

349 For example, if {\it formula} is

350 \hbox{\tt a=b ==> b=a} then the resulting theorem has the form

351 \hbox{\verb'?a=?b ==> ?b=?a [!!a b. a=b ==> b=a]'}

352 \end{ttdescription}

354 \subsection{Building a theory}

355 \label{BuildingATheory}

356 \index{theories!constructing|bold}

357 \begin{ttbox}

358 pure_thy : theory

359 merge_theories : theory * theory -> theory

360 \end{ttbox}

361 \begin{ttdescription}

362 \item[\ttindexbold{pure_thy}] contains just the syntax and signature

363 of the meta-logic. There are no axioms: meta-level inferences are carried

364 out by \ML\ functions.

365 \item[\ttindexbold{merge_theories} ($thy@1$, $thy@2$)] merges the two

366 theories $thy@1$ and $thy@2$. The resulting theory contains all of the

367 syntax, signature and axioms of the constituent theories. Merging theories

368 that contain different identification stamps of the same name fails with

369 the following message

370 \begin{ttbox}

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

372 \end{ttbox}

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

374 change an incorrect axiom --- and bindings to old versions persist.

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

376 involved in a proof.

378 %% FIXME

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

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

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

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

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

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

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

386 %\begin{ttbox}

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

388 %\end{ttbox}

389 \end{ttdescription}

391 %% FIXME

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

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

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

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

396 %\begin{ttbox}

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

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

399 % \dots

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

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

402 % \dots

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

404 % \dots

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

406 % \dots

407 %rules \(name\) \(rule\)

408 % \dots

409 %end

410 %\end{ttbox}

411 %where

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

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

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

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

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

417 %\\

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

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

420 %\end{tabular}

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

424 \index{theories!inspecting|bold}

425 \begin{ttbox}

426 print_theory : theory -> unit

427 axioms_of : theory -> (string * thm) list

428 thms_of : theory -> (string * thm) list

429 parents_of : theory -> theory list

430 sign_of : theory -> Sign.sg

431 stamps_of_thy : theory -> string ref list

432 \end{ttbox}

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

434 \begin{ttdescription}

435 \item[\ttindexbold{print_theory} $thy$]

436 prints the contents of $thy$ excluding the syntax related parts (which are

437 shown by {\tt print_syntax}). The output is quite verbose.

439 \item[\ttindexbold{axioms_of} $thy$]

440 returns the additional axioms of the most recent extend node of~$thy$.

442 \item[\ttindexbold{thms_of} $thy$]

443 returns all theorems that are associated with $thy$.

445 \item[\ttindexbold{parents_of} $thy$]

446 returns the direct ancestors of~$thy$.

448 \item[\ttindexbold{sign_of} $thy$]

449 returns the signature associated with~$thy$. It is useful with functions

450 like {\tt read_instantiate_sg}, which take a signature as an argument.

452 \item[\ttindexbold{stamps_of_thy} $thy$]\index{signatures}

453 returns the identification \rmindex{stamps} of the signature associated

454 with~$thy$.

455 \end{ttdescription}

458 \section{Generating HTML documents}

459 \index{HTML|bold}

461 Isabelle is able to make HTML documents that show a theory's

462 definition, the theorems proved in its ML file and the relationship

463 with its ancestors and descendants. HTML stands for Hypertext Markup

464 Language and is used in the World Wide Web to represent text

465 containing images and links to other documents. Web browsers like

466 {\tt xmosaic} or {\tt netscape} are used to view these documents.

468 Besides the three HTML files that are made for every theory

469 (definition and theorems, ancestors, descendants), Isabelle stores

470 links to all theories in an index file. These indexes are themself

471 linked with other indexes to represent the hierarchic structure of

472 Isabelle's logics.

474 To make HTML files for logics that are part of the Isabelle

475 distribution, simply set the shell environment variable {\tt

476 MAKE_HTML} before compiling a logic. This works for single logics as

477 well as for the shell script {\tt make-all} (see

478 \ref{sec:shell-scripts}). To make HTML files for {\tt FOL} using a

479 {\tt csh} style shell, the following commands can be used:

481 \begin{ttbox}

482 cd FOL

483 setenv MAKE_HTML

484 make

485 \end{ttbox}

487 As some of Isabelle's logics are based on others (e.g. {\tt ZF} on

488 {\tt FOL}) and because the HTML files list a theory's ancestors, you

489 should not make HTML files for a logic if the HTML files for the base

490 logic do not exist. Otherwise some of the hypertext links might point

491 to non-existing documents.

493 The entry point to all logics is the {\tt index.html} file located in

494 Isabelle's main directory. You can also access a HTML version of the

495 distribution package at

497 \begin{ttbox}

498 http://www4.informatik.tu-muenchen.de/~nipkow/isabelle

499 \end{ttbox}

502 \subsection*{Manual HTML generation}

504 To manually activate and deactivate the generation of HTML files the

505 following commands and reference variables are used:

507 \begin{ttbox}

508 init_html : unit -> unit

509 make_html : bool ref

510 finish_html : unit -> unit

511 \end{ttbox}

513 \begin{ttdescription}

514 \item[\ttindexbold{init_html}]

515 activates the HTML facility. It stores the current working directory

516 as the place where the {\tt index.html} file for all theories loaded

517 afterwards will be stored.

519 \item[\ttindexbold{make_html}]

520 is a boolean reference variable read by {\tt use_thy} and other

521 functions to decide whether HTML files should be made. After you have

522 used {\tt init_html} you can manually change {\tt make_html}'s value

523 to temporarily disable HTML generation.

525 \item[\ttindexbold{finish_html}]

526 has to be called after all theories have been read that should be

527 listed in the current {\tt index.html} file. It reads a temporary

528 file with information about the theories read since the last use of

529 {\tt init_html} and makes the {\tt index.html} file. If {\tt

530 make_html} is {\tt false} nothing is done.

532 The indexes made by this function also contain a link to the {\tt

533 README} file if there exists one in the directory were the index is

534 stored. If there's a {\tt README.html} file it is used instead of

535 {\tt README}.

537 \end{ttdescription}

539 The above functions could be used in the following way:

541 \begin{ttbox}

542 init_html();

543 {\out Setting path for index.html to "/home/stud/clasohm/isabelle/HOL"}

544 use_thy "List";

545 \dots

546 finish_html();

547 \end{ttbox}

549 Please note that HTML files are made only for those theories that are

550 read while {\tt make_html} is {\tt true}. These files may contain

551 links to theories that were read with a {\tt false} {\tt make_html}

552 and therefore point to non-existing files.

555 \subsection*{Extending or adding a logic}

557 If you add a new subdirectory to Isabelle's logics (or add a completly

558 new logic), you would have to call {\tt init_html} at the start of every

559 directory's {\tt ROOT.ML} file and {\tt finish_html} at the end of

560 it. This is automatically done if you use

562 \begin{ttbox}\index{use_dir}

563 use_dir : string -> unit

564 \end{ttbox}

566 This function takes a path as its parameter, changes the working

567 directory, calls {\tt init_html} if {\tt make_html} is {\tt true},

568 executes {\tt ROOT.ML}, and calls {\tt finish_html}. The {\tt

569 index.html} file written in this directory will be automatically

570 linked to the first index found in the (recursively searched)

571 superdirectories.

573 Instead of adding something like

575 \begin{ttbox}

576 use"ex/ROOT.ML";

577 \end{ttbox}

579 to the logic's makefile you have to use this:

581 \begin{ttbox}

582 use_dir"ex";

583 \end{ttbox}

585 Since {\tt use_dir} calls {\tt init_html} only if {\tt make_html} is

586 {\tt true} the generation of HTML files depends on the value this

587 reference variable has. It can either be inherited from the used \ML{}

588 database or set in the makefile before {\tt use_dir} is invoked,

589 e.g. to set it's value according to the environment variable {\tt

590 MAKE_HTML}.

592 The generated HTML files contain all theorems that were proved in the

593 theory's \ML{} file with {\tt qed}, {\tt qed_goal} and {\tt qed_goalw},

594 or stored with {\tt bind_thm} and {\tt store_thm}. Additionally there

595 is a hypertext link to the whole \ML{} file.

598 \subsection*{Using someone else's database}

600 To make them independent from their storage place, the HTML files only

601 contain relative paths which are derived from absolute ones like the

602 current working directory, {\tt gif_path} or {\tt base_path}. The

603 latter two are reference variables which are initialized at the time

604 when the {\tt Pure} database is made. Because you need write access

605 for the current directory to make HTML files and therefore (probably)

606 generate them in your home directory, the absolute {\tt base_path} is

607 not correct if you use someone else's database or a database derived

608 from it.

610 In that case you first have to set {\tt base_path} to the value of

611 {\em your} Isabelle main directory, i.e. the directory that contains

612 the subdirectories where standard logics like {\tt FOL} and {\tt HOL}

613 or your own logics are stored.

615 It's also a good idea to set {\tt gif_path} which points to the

616 directory containing two GIF images used in the HTML

617 documents. Normally this is the {\tt Tools} subdirectory of Isabelle's

618 main directory. While its value in general is still valid, your HTML

619 files would depend on files not owned by you. This prevents you from

620 changing the location of the HTML files (as they contain relative

621 paths) and also causes trouble if the database's maker (re)moves the

622 GIFs.

624 Here's what you have to do before invoking {\tt init_html} using

625 someone else's \ML{} database:

627 \begin{ttbox}

628 base_path := "/home/smith/isabelle";

629 gif_path := "/home/smith/isabelle/Tools";

630 init_html();

631 \dots

632 \end{ttbox}

634 \section{Terms}

635 \index{terms|bold}

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

637 with six constructors: there are six kinds of term.

638 \begin{ttbox}

639 type indexname = string * int;

640 infix 9 $;

641 datatype term = Const of string * typ

642 | Free of string * typ

643 | Var of indexname * typ

644 | Bound of int

645 | Abs of string * typ * term

646 | op $ of term * term;

647 \end{ttbox}

648 \begin{ttdescription}

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

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

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

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

653 syntax.

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

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

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

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

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

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

662 incrementing their subscripts. Scheme variables are essentially free

663 variables, but may be instantiated during unification.

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

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

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

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

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

670 Paulson~\cite[page~336]{paulson91}.

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

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

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

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

676 and printing; it has no logical significance.

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

679 is the {\bf application} of~$t$ to~$u$.

680 \end{ttdescription}

681 Application is written as an infix operator to aid readability.

682 Here is an \ML\ pattern to recognize \FOL{} formulae of

683 the form~$A\imp B$, binding the subformulae to~$A$ and~$B$:

684 \begin{ttbox}

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

686 \end{ttbox}

689 \section{Variable binding}

690 \begin{ttbox}

691 loose_bnos : term -> int list

692 incr_boundvars : int -> term -> term

693 abstract_over : term*term -> term

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

695 aconv : term*term -> bool\hfill{\bf infix}

696 \end{ttbox}

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

698 bound variables.

699 \begin{ttdescription}

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

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

702 particular, {\tt Bound~0} is loose unless it is enclosed in an

703 abstraction. Similarly {\tt Bound~1} is loose unless it is enclosed in

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

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

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

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

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

710 different number of abstractions. Bound variables with a matching

711 abstraction are unaffected.

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

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

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

716 correct index.

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

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

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

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

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

723 free in~$u$.

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

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

727 to renaming of bound variables.

728 \begin{itemize}

729 \item

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

731 if their names and types are equal.

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

733 This confusing situation should be avoided!)

734 \item

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

736 if they have the same number.

737 \item

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

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

740 \item

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

742 if the corresponding subterms are.

743 \end{itemize}

745 \end{ttdescription}

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

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

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

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

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

752 take certified terms as arguments.

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

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

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

758 \subsection{Printing terms}

759 \index{terms!printing of}

760 \begin{ttbox}

761 string_of_cterm : cterm -> string

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

763 \end{ttbox}

764 \begin{ttdescription}

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

766 displays $ct$ as a string.

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

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

770 \end{ttdescription}

772 \subsection{Making and inspecting certified terms}

773 \begin{ttbox}

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

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

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

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

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

779 \end{ttbox}

780 \begin{ttdescription}

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

782 certifies $t$ with respect to signature~$sign$.

784 \item[\ttindexbold{read_cterm} $sign$ ($s$, $T$)]

785 reads the string~$s$ using the syntax of~$sign$, creating a certified term.

786 The term is checked to have type~$T$; this type also tells the parser what

787 kind of phrase to parse.

789 \item[\ttindexbold{cert_axm} $sign$ ($name$, $t$)]

790 certifies $t$ with respect to $sign$ as a meta-proposition and converts all

791 exceptions to an error, including the final message

792 \begin{ttbox}

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

794 \end{ttbox}

796 \item[\ttindexbold{read_axm} $sign$ ($name$, $s$)]

797 similar to {\tt cert_axm}, but first reads the string $s$ using the syntax of

798 $sign$.

800 \item[\ttindexbold{rep_cterm} $ct$]

801 decomposes $ct$ as a record containing its type, the term itself, its

802 signature, and the maximum subscript of its unknowns. The type and maximum

803 subscript are computed during certification.

804 \end{ttdescription}

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

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

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

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

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

812 represented by a string.

813 \begin{ttbox}

814 type class = string;

815 type sort = class list;

817 datatype typ = Type of string * typ list

818 | TFree of string * sort

819 | TVar of indexname * sort;

821 infixr 5 -->;

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

823 \end{ttbox}

824 \begin{ttdescription}

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

826 applies the {\bf type constructor} named~$a$ to the type operands~$Ts$.

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

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

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

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

831 types.

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

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

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

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

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

839 instantiated during unification.

840 \end{ttdescription}

843 \section{Certified types}

844 \index{types!certified|bold}

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

846 \ttindexbold{ctyp}.

848 \subsection{Printing types}

849 \index{types!printing of}

850 \begin{ttbox}

851 string_of_ctyp : ctyp -> string

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

853 \end{ttbox}

854 \begin{ttdescription}

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

856 displays $cT$ as a string.

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

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

860 \end{ttdescription}

863 \subsection{Making and inspecting certified types}

864 \begin{ttbox}

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

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

867 \end{ttbox}

868 \begin{ttdescription}

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

870 certifies $T$ with respect to signature~$sign$.

872 \item[\ttindexbold{rep_ctyp} $cT$]

873 decomposes $cT$ as a record containing the type itself and its signature.

874 \end{ttdescription}

876 \index{theories|)}