|
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> |