webertj@15283: webertj@15283: wenzelm@10253: wenzelm@10253: webertj@15582: webertj@15582: webertj@15582: HOL-Library/README webertj@15582: wenzelm@10253: wenzelm@10253: wenzelm@10253: wenzelm@10253:

HOL-Library: supplemental theories for main Isabelle/HOL

wenzelm@10253: wenzelm@10253: This is a collection of generic theories that may be used together blanchet@42062: with main Isabelle/HOL. wenzelm@10253: wenzelm@10253:

wenzelm@10253: wenzelm@10253: Addition of new theories should be done with some care, as the wenzelm@10253: ``module system'' of Isabelle is rather simplistic. The following wenzelm@10253: guidelines may be helpful to achieve maximum re-usability and minimum wenzelm@10253: clashes with existing developments. wenzelm@10253: wenzelm@10253:

wenzelm@10253: wenzelm@10253:
Files wenzelm@10282: wenzelm@10253:
Avoid unnecessary scattering of theories over several files. Use wenzelm@10253: new-style theories only, as old ones tend to clutter the file space wenzelm@10253: with separate .thy and .ML files. wenzelm@10253: wenzelm@10253:
Examples wenzelm@10253: wenzelm@10253:
Theories should be as ``generic'' as is sensible. Unused (or wenzelm@10282: rather unusable?) theories should be avoided; common applications wenzelm@10282: should actually refer to the present theory. Small example uses may wenzelm@10282: be included in the library as well, but should be put in a separate wenzelm@10253: theory, such as Foobar accompanied by wenzelm@10253: Foobar_Examples. wenzelm@10253: wenzelm@10253:
Theory names wenzelm@10282: wenzelm@10253:
The theory loader name space is flat, so use sufficiently wenzelm@10253: long and descriptive names to reduce the danger of clashes with the wenzelm@10253: user's own theories. The convention for theory names is as follows: wenzelm@10253: Foobar_Doobar (this looks best in LaTeX output). wenzelm@10253: wenzelm@10253:
Names of logical items wenzelm@10282: wenzelm@10253:
There are separate hierarchically structured name spaces for wenzelm@10253: types, constants, theorems etc. Nevertheless, some care should be wenzelm@10253: taken, as the name spaces are always ``open''. Use adequate names; wenzelm@10253: avoid unreadable abbreviations. The general naming convention is to wenzelm@10253: separate word constituents by underscores, as in foo_bar or wenzelm@10253: Foo_Bar (this looks best in LaTeX output). wenzelm@10253: wenzelm@10253:

wenzelm@10253: huffman@26406: Note that syntax is global; qualified names lose syntax on wenzelm@10253: output. Do not use ``exotic'' symbols for syntax (such as wenzelm@10253: \<oplus>), but leave these for user applications. wenzelm@10253: wenzelm@10253:

Global context declarations wenzelm@10282: wenzelm@10253:
Only items introduced in the present theory should be declared wenzelm@10282: globally (e.g. as Simplifier rules). Note that adding and deleting wenzelm@10282: rules from parent theories may result in strange behavior later, wenzelm@10282: depending on the user's arrangement of import lists. wenzelm@10253: wenzelm@10253:
Mathematical symbols wenzelm@10282: wenzelm@10282:
Non-ASCII symbols should be used as appropriate, with some wenzelm@10282: care. In particular, avoid unreadable arrows: ==> should wenzelm@28504: be preferred over \<Longrightarrow>. Use isabelle wenzelm@10282: unsymbolize to clean up the sources. wenzelm@10253: wenzelm@10253:

wenzelm@10253: wenzelm@10253: The following ASCII symbols of HOL should be generally avoided: wenzelm@10253: @, !, ?, ?!, %, better wenzelm@10253: use SOME, ALL (or \<forall>), wenzelm@10253: EX (or \<exists>), EX! (or wenzelm@10282: \<exists>!), \<lambda>, respectively. wenzelm@10253: Note that bracket notation [| |] looks bad in LaTeX wenzelm@10253: output. wenzelm@10253: wenzelm@10253:

wenzelm@10253: wenzelm@10253: Some additional mathematical symbols are quite suitable for both wenzelm@10282: readable sources and the output document: wenzelm@10253: \<Inter>, wenzelm@10253: \<Union>, wenzelm@10253: \<and>, wenzelm@10253: \<in>, wenzelm@10253: \<inter>, wenzelm@10334: \<le>, wenzelm@10253: \<not>, wenzelm@10253: \<noteq>, wenzelm@10253: \<notin>, wenzelm@10253: \<or>, wenzelm@10253: \<subset>, wenzelm@10253: \<subseteq>, wenzelm@10253: \<times>, wenzelm@10253: \<union>. wenzelm@10253: wenzelm@10253:

Spacing wenzelm@10253: wenzelm@10253:
Isabelle is able to produce a high-quality LaTeX document from the wenzelm@10253: theory sources, provided some minor issues are taken care of. In wenzelm@10253: particular, spacing and line breaks are directly taken from source huffman@26406: text. Incidentally, output looks very good if common type-setting wenzelm@10253: conventions are observed: put a single space after each wenzelm@10253: punctuation character (",", ".", etc.), but none wenzelm@10253: before it; do not extra spaces inside of parentheses, unless the wenzelm@10253: delimiters are composed of multiple symbols (as in wenzelm@10253: [| |]); do not attempt to simulate table markup with wenzelm@10253: spaces, avoid ``hanging'' indentations. wenzelm@10253: wenzelm@10253:
wenzelm@10253: wenzelm@10253: wenzelm@10253: