MIME-Version: 1.0
Server: CERN/3.0
Date: Sunday, 24-Nov-96 19:07:05 GMT
Content-Type: text/html
Content-Length: 3468
Last-Modified: Monday, 27-Feb-95 02:06:56 GMT
Summary of Nuprl Theories
Summary of Theories
Each link below leads to a formatted presentation of a Nuprl theory.
A description of the organization of these presentations and of the
meaning of the triples after each link name can be found
here.
-
core_1 (18, 0, 0)
-
Display forms for primitive terms of type-theory. Abstractions for
propositions-as-types correspondence. Parenthesization control.
-
core_2 (40, 102, 347)
-
General-purpose definitions and
theorems.
-
well_fnd (1, 6, 129)
-
Well-founded predicate. Rank induction lemmas and
tactics.
-
int_1 (9, 33, 169)
-
Integer inequalities, subtypes, and
induction lemmas for subtypes.
-
bool_1 (17, 67, 239)
-
Definitions, theorems and tactics for the boolean
type and boolean-related expressions.
-
fun_1 (9, 21, 106)
-
Polymorphic identity and composition functions.
Lemmas covering properties suchas injectivity and
surjectivity.
-
int_2 (9, 143, 937)
-
Defines mod, floor, max and min functions over the
integers.
Lemmas concern basic properties of arithmetic functions over integers, and induction principles.
-
list_1 (16, 54, 315)
-
-
gen_algebra_1 (51, 144, 464)
-
Properties of order and equivalence relations,
and of algebraic functions (e.g. commutativity
associativity).
-
sets_1 (18, 52, 133)
-
Family of classes for types with computable equality and
inequality relations.
-
groups_1 (50, 199, 752)
-
Family of classes for monoids and groups.
Summations with indices from integer subranges. Exponential functions.
-
perms_1 (21, 80, 623)
-
-
perms_2 (5, 34, 422)
-
Introduces the binary relations on lists `is a permutation of',
`is a permutation of up to', and `is equivalent up to'.
-
list_2 (21, 94, 638)
-
Introduces a variety of standard list-related functions,
that assume that list elements come from a type
or monoid with decidable equality.
-
rings_1 (44, 126, 376)
-
Family of classes for rings, integral domains
and fields. Ideals and quotient rings. Sums and products.
-
mset (25, 112, 592)
-
Finite multisets and finite sets. Summation
with indices drawn from multisets. Defines ADT
for free abelian monoids, and demonstrates an instance
of this ADT using multisets.
-
factor_1 (16, 61, 386)
-
Divisibility theory for monoids with cancellation.
Develops theorems characterizing when factorizations are
unique and derives from these the fundamental theorem of
arithmetic.
Last modified February 24th, 1995
Paul Jackson /
jackson@cs.cornell.edu