10253
|
1 |
<html>
|
|
2 |
|
|
3 |
<!-- $Id$ -->
|
|
4 |
|
|
5 |
<head><title>HOL-Library/README</title></head>
|
|
6 |
|
|
7 |
<body>
|
|
8 |
|
|
9 |
<h1>HOL-Library: supplemental theories for main Isabelle/HOL</h1>
|
|
10 |
|
|
11 |
This is a collection of generic theories that may be used together
|
|
12 |
with main Isabelle/HOL. Note that theory loader path already includes
|
|
13 |
this directory by default.
|
|
14 |
|
|
15 |
<p>
|
|
16 |
|
|
17 |
Addition of new theories should be done with some care, as the
|
|
18 |
``module system'' of Isabelle is rather simplistic. The following
|
|
19 |
guidelines may be helpful to achieve maximum re-usability and minimum
|
|
20 |
clashes with existing developments.
|
|
21 |
|
|
22 |
<dl>
|
|
23 |
|
|
24 |
<dt><strong>Files</strong>
|
|
25 |
<dd>Avoid unnecessary scattering of theories over several files. Use
|
|
26 |
new-style theories only, as old ones tend to clutter the file space
|
|
27 |
with separate <tt>.thy</tt> and <tt>.ML</tt> files.
|
|
28 |
|
|
29 |
<dt><strong>Examples</strong>
|
|
30 |
|
|
31 |
<dd>Theories should be as ``generic'' as is sensible. Unused (or
|
|
32 |
rather unusable?) standalone theories should be avoided; common
|
|
33 |
applications should actually refer to the present theory. Small
|
|
34 |
example uses may be included as well, but should be put in a separate
|
|
35 |
theory, such as <tt>Foobar</tt> accompanied by
|
|
36 |
<tt>Foobar_Examples</tt>.
|
|
37 |
|
|
38 |
<dt><strong>Theory names</strong>
|
|
39 |
<dd>The theory loader name space is <em>flat</em>, so use sufficiently
|
|
40 |
long and descriptive names to reduce the danger of clashes with the
|
|
41 |
user's own theories. The convention for theory names is as follows:
|
|
42 |
<tt>Foobar_Doobar</tt> (this looks best in LaTeX output).
|
|
43 |
|
|
44 |
<dt><strong>Names of logical items</strong>
|
|
45 |
<dd>There are separate hierarchically structured name spaces for
|
|
46 |
types, constants, theorems etc. Nevertheless, some care should be
|
|
47 |
taken, as the name spaces are always ``open''. Use adequate names;
|
|
48 |
avoid unreadable abbreviations. The general naming convention is to
|
|
49 |
separate word constituents by underscores, as in <tt>foo_bar</tt> or
|
|
50 |
<tt>Foo_Bar</tt> (this looks best in LaTeX output).
|
|
51 |
|
|
52 |
<p>
|
|
53 |
|
|
54 |
Note that syntax is <em>global</em>; qualified names loose syntax on
|
|
55 |
output. Do not use ``exotic'' symbols for syntax (such as
|
|
56 |
<tt>\<oplus></tt>), but leave these for user applications.
|
|
57 |
|
|
58 |
<dt><strong>Global context declarations</strong>
|
|
59 |
<dd>Only items introduced in the present theory should be declared
|
|
60 |
globally (e.g. as Simplifier rules). Note that adding / deleting
|
|
61 |
rules stemming from parent theories may result in strange behavior
|
|
62 |
later, depending on the user's arrangement of import lists.
|
|
63 |
|
|
64 |
<dt><strong>Mathematical symbols</strong>
|
|
65 |
<dd>Non-ASCII symbols should be used with some care. In particular,
|
|
66 |
avoid unreadable arrows: <tt>==></tt> should be preferred over
|
|
67 |
<tt>\<Longrightarrow></tt>. Use <tt>isatool unsymbolize</tt> to
|
|
68 |
clean up the sources.
|
|
69 |
|
|
70 |
<p>
|
|
71 |
|
|
72 |
The following ASCII symbols of HOL should be generally avoided:
|
|
73 |
<tt>@</tt>, <tt>!</tt>, <tt>?</tt>, <tt>?!</tt>, <tt>%</tt>, better
|
|
74 |
use <tt>SOME</tt>, <tt>ALL</tt> (or <tt>\<forall></tt>),
|
|
75 |
<tt>EX</tt> (or <tt>\<exists></tt>), <tt>EX!</tt> (or
|
|
76 |
<tt>\<exists;>!</tt>), <tt>\<lambda></tt>, respectively.
|
|
77 |
Note that bracket notation <tt>[| |]</tt> looks bad in LaTeX
|
|
78 |
output.
|
|
79 |
|
|
80 |
<p>
|
|
81 |
|
|
82 |
Some additional mathematical symbols are quite suitable for both
|
|
83 |
readable sources and output document:
|
|
84 |
<tt>\<Inter></tt>,
|
|
85 |
<tt>\<Union></tt>,
|
|
86 |
<tt>\<and></tt>,
|
|
87 |
<tt>\<in></tt>,
|
|
88 |
<tt>\<inter></tt>,
|
|
89 |
<tt>\<not></tt>,
|
|
90 |
<tt>\<noteq></tt>,
|
|
91 |
<tt>\<notin></tt>,
|
|
92 |
<tt>\<or></tt>,
|
|
93 |
<tt>\<subset></tt>,
|
|
94 |
<tt>\<subseteq></tt>,
|
|
95 |
<tt>\<times></tt>,
|
|
96 |
<tt>\<union></tt>.
|
|
97 |
|
|
98 |
<dt><strong>Spacing</strong>
|
|
99 |
|
|
100 |
<dd>Isabelle is able to produce a high-quality LaTeX document from the
|
|
101 |
theory sources, provided some minor issues are taken care of. In
|
|
102 |
particular, spacing and line breaks are directly taken from source
|
|
103 |
text. Incidently, output looks very good common type-setting
|
|
104 |
conventions are observed: put a single space <em>after</em> each
|
|
105 |
punctuation character ("<tt>,</tt>", "<tt>.</tt>", etc.), but none
|
|
106 |
before it; do not extra spaces inside of parentheses, unless the
|
|
107 |
delimiters are composed of multiple symbols (as in
|
|
108 |
<tt>[| |]</tt>); do not attempt to simulate table markup with
|
|
109 |
spaces, avoid ``hanging'' indentations.
|
|
110 |
|
|
111 |
</dl>
|
|
112 |
|
|
113 |
</body>
|
|
114 |
</html>
|