boyland / twelf-library

This is release 0.9 of John Boyland's Twelf library

(If this directory includes a Makefile, it is the source
of the library Twelf signatures.  The Makefile provided
requires CPP (default "cpp") to be a C pre-processor,
such as /lib/cpp on many Unix systems.)

To make up for a lack of a module system, some of these signatures are
produced through use of the C preprocessor. I also fake a module
system, using backquote ` since . is (correctly) not legal in a name.

The distribution includes the following Twelf files:

     * Some simple definitions that should be standard.
       std.elf (The name is an overreach!)

     * Boolean constants. This includes some standard equality and
       inequality theorems (such as the transitivity of equality) that I
       try to prove for all data types.
       bool.elf

     * Natural numbers (composed using z and s). The signature includes
       plus, times, eq, gt (greater than), and a number of other mainly
       derived relations (minus, ge, lt etc). It also includes a divrem
       operation for integer division with remainder. The package
       includes over 300 theorems about these relations all with
       automatically-checked hand-written proofs (using Twelf 1.5R3).
       nat.elf

     * Pairs. This trivial "functor" of pairs. There is an instantiation
       for pairs of natural numbers that includes an isomorphism from
       pairs to natural numbers, so that pairs can be (indirectly) used
       as keys to maps (q.v.).
       pair.elf (the functor), natpair.elf (pairs of natural
       numbers).

     * Positive rational numbers (represented using continued fractions).
       The signature requires "nat.elf" and "natpair.elf" and includes
       add, mul, equ, grt and derived relations, including similar
       relations as above, but also a div relation. Division is a total
       operation over the positive rationals. The signature includes an
       isomorphism from positive rationals to the natural numbers which
       enables rational numbers to serve as the domain of a map (q.v.).
       The package includes well over 300 fully-proved theorems.
       rat.elf rat0.elf (non-negative rational numbers)

     * Partial maps. This signature represents maps from natural numbers
       to an unspecified datatype data. It must be customized before use.
       It includes over 55 fully-proved theorems. Additionally, if the
       "data" datatype supports leq, join and/or meet operations, there
       are definitions of these operations for maps and over 100 extra
       theorems involving them. We also have the map-domain and map-scale
       add-ons and the map-trans, map-all, map-restrict helper functors.
       map.elf (the signature, hand-written), map.tgz (all of the
       map theorems).

     * Sets of natural numbers. This signature implements finite sets of
       natural numbers. As above, the representation is "adequate": two
       sets are equivalent iff they are equal. The signature is mainly
       generated by instantiating the "map" "functor" with "data" being
       "unit". Among other operations are member, not-member, leq, union,
       intersection, add (single element) and remove (sets). The
       signature includes well over 300 fully proved theorems about these
       operations.
       set.elf

     * Multisets of natural numbers. This signature implements multisets
       as maps to natural numbers. The union operation does an `max'
       operation. It is implemented using that map "functor."
       multiset.elf

     * Vectors (with length). This is a "functor" over a type with both
       "add" an "mul" operations defined. The length is used to ensure
       there is no attempt made to compare (eq), add or dot vectors of
       different length. The "dot" operation is provided only if the
       underlying data type includes a zero.
       vector.elf (the functor), rat0vector.elf (vectors of
       non-negative rational numbers).
       
All of these signatures and sources of generated ELF code are offered
without restriction to anyone who wishes to use them in any way.


Release Notes:

0.9:
   helper functors for map: map-all map-trans map-restrict map-minmax
   many theorems now have a definable worlds.
   exported to git

0.8: 
   README added to release
   single-quotes restricted so that "make" works with modern CPP
   many more set theorems (especially regarding set`remove)

0.7:
   *-unique provided as an alternative to *-deterministic

Last update: October 24, 2012.