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