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