Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2004-11-10 16:18:44 -0800 (Wed, 10 Nov 2004)
Revision: 6259
Log message:
Define a type for simple lambda terms.
To do this I had too add several theories:
- Itt_sqsimple defines types with squiggle equality
- Itt_power defines the type Power[i:l]{'T} -- type of all subsets of T.
- Itt_functions defines the image of functions, surjection, injection, reversible function and so on
- Itt_closure defines closure of collection of function on a type T
- Itt_pairwise defines axioms for pairwise functionality (we need this for the induction principle).
- Itt_pairwise2 has theorems that are true only in pairwise functionality.
- Itt_reflection_example_lambda defines the type for simple lambda terms.
Also:
-Add squash stability for <=, >, <, <> in Itt_int_ext
-Add some other simple theorems.
-Add AutoMustComplete option to subtype_axiomFormation.
It could break some proofs, I'll fix them later.
Some proofs are still unfinished.