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