src/HOL/Library/README.html
author Andreas Lochbihler
Wed Feb 27 10:33:30 2013 +0100 (2013-02-27)
changeset 51288 be7e9a675ec9
parent 42062 9fe5daa2e705
child 57412 b441f330078b
permissions -rw-r--r--
add wellorder instance for Numeral_Type (suggested by Jesus Aransay)
     1 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
     2 
     3 <html>
     4 
     5 <head>
     6   <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
     7   <title>HOL-Library/README</title>
     8 </head>
     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
    15 with main Isabelle/HOL.
    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>
    27 
    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
    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
    38 theory, such as <tt>Foobar</tt> accompanied by
    39 <tt>Foobar_Examples</tt>.
    40 
    41 <dt><strong>Theory names</strong>
    42 
    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>
    49 
    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 
    59 Note that syntax is <em>global</em>; qualified names lose syntax on
    60 output.  Do not use ``exotic'' symbols for syntax (such as
    61 <tt>\&lt;oplus&gt;</tt>), but leave these for user applications.
    62 
    63 <dt><strong>Global context declarations</strong>
    64 
    65 <dd>Only items introduced in the present theory should be declared
    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.
    69 
    70 <dt><strong>Mathematical symbols</strong>
    71 
    72 <dd>Non-ASCII symbols should be used as appropriate, with some
    73 care. In particular, avoid unreadable arrows: <tt>==&gt;</tt> should
    74 be preferred over <tt>\&lt;Longrightarrow&gt;</tt>. Use <tt>isabelle
    75 unsymbolize</tt> to clean up the sources.
    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>\&lt;forall&gt;</tt>),
    82 <tt>EX</tt> (or <tt>\&lt;exists&gt;</tt>), <tt>EX!</tt> (or
    83 <tt>\&lt;exists&gt;!</tt>), <tt>\&lt;lambda&gt;</tt>, respectively.
    84 Note that bracket notation <tt>[|&nbsp;|]</tt> looks bad in LaTeX
    85 output.
    86 
    87 <p>
    88 
    89 Some additional mathematical symbols are quite suitable for both
    90 readable sources and the output document:
    91 <tt>\&lt;Inter&gt;</tt>,
    92 <tt>\&lt;Union&gt;</tt>,
    93 <tt>\&lt;and&gt;</tt>,
    94 <tt>\&lt;in&gt;</tt>,
    95 <tt>\&lt;inter&gt;</tt>,
    96 <tt>\&lt;le&gt;</tt>,
    97 <tt>\&lt;not&gt;</tt>,
    98 <tt>\&lt;noteq&gt;</tt>,
    99 <tt>\&lt;notin&gt;</tt>,
   100 <tt>\&lt;or&gt;</tt>,
   101 <tt>\&lt;subset&gt;</tt>,
   102 <tt>\&lt;subseteq&gt;</tt>,
   103 <tt>\&lt;times&gt;</tt>,
   104 <tt>\&lt;union&gt;</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
   111 text.  Incidentally, output looks very good if common type-setting
   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>[|&nbsp;|]</tt>); do not attempt to simulate table markup with
   117 spaces, avoid ``hanging'' indentations.
   118 
   119 </dl>
   120 
   121 </body>
   122 </html>