diff options
Diffstat (limited to 'src/algebra')
| -rw-r--r-- | src/algebra/Makefile.in | 3 | ||||
| -rw-r--r-- | src/algebra/Makefile.pamphlet | 3 | ||||
| -rw-r--r-- | src/algebra/catdef.spad.pamphlet | 29 |
3 files changed, 30 insertions, 5 deletions
diff --git a/src/algebra/Makefile.in b/src/algebra/Makefile.in index 6093c019..52db4771 100644 --- a/src/algebra/Makefile.in +++ b/src/algebra/Makefile.in @@ -346,6 +346,7 @@ $(OUT)/PDDOM.$(FASLEXT): $(OUT)/TYPE.$(FASLEXT) $(OUT)/PDSPC.$(FASLEXT): $(OUT)/PDDOM.$(FASLEXT) $(OUT)/DSEXT.$(FASLEXT): $(OUT)/DIFFSPC.$(FASLEXT) $(OUT)/PDSPC.$(FASLEXT) $(OUT)/ORDTYPE.$(FASLEXT): $(OUT)/BASTYPE.$(FASLEXT) +$(OUT)/ORDSTRCT.$(FASLEXT): $(OUT)/ORDTYPE.$(FASLEXT) $(OUT)/HOMOTOP.$(FASLEXT) axiom_algebra_layer_0 = \ AHYP ATTREG CFCAT ELTAB KOERCE KONVERT \ @@ -373,7 +374,7 @@ axiom_algebra_layer_0 = \ LIST DIFFDOM DIFFDOM- DIFFSPC DIFFSPC- DIFFMOD \ LINEXP PATMAB REAL CHARZ LOGIC LOGIC- \ RTVALUE SYSPTR PDDOM PDDOM- PDSPC PDSPC- \ - DSEXT DSEXT- ORDTYPE ORDTYPE- + DSEXT DSEXT- ORDTYPE ORDTYPE- ORDSTRCT axiom_algebra_layer_0_nrlibs = \ $(addsuffix .NRLIB/code.$(FASLEXT),$(axiom_algebra_layer_0)) diff --git a/src/algebra/Makefile.pamphlet b/src/algebra/Makefile.pamphlet index 2d3e0908..f57b7839 100644 --- a/src/algebra/Makefile.pamphlet +++ b/src/algebra/Makefile.pamphlet @@ -300,6 +300,7 @@ $(OUT)/PDDOM.$(FASLEXT): $(OUT)/TYPE.$(FASLEXT) $(OUT)/PDSPC.$(FASLEXT): $(OUT)/PDDOM.$(FASLEXT) $(OUT)/DSEXT.$(FASLEXT): $(OUT)/DIFFSPC.$(FASLEXT) $(OUT)/PDSPC.$(FASLEXT) $(OUT)/ORDTYPE.$(FASLEXT): $(OUT)/BASTYPE.$(FASLEXT) +$(OUT)/ORDSTRCT.$(FASLEXT): $(OUT)/ORDTYPE.$(FASLEXT) $(OUT)/HOMOTOP.$(FASLEXT) axiom_algebra_layer_0 = \ AHYP ATTREG CFCAT ELTAB KOERCE KONVERT \ @@ -327,7 +328,7 @@ axiom_algebra_layer_0 = \ LIST DIFFDOM DIFFDOM- DIFFSPC DIFFSPC- DIFFMOD \ LINEXP PATMAB REAL CHARZ LOGIC LOGIC- \ RTVALUE SYSPTR PDDOM PDDOM- PDSPC PDSPC- \ - DSEXT DSEXT- ORDTYPE ORDTYPE- + DSEXT DSEXT- ORDTYPE ORDTYPE- ORDSTRCT axiom_algebra_layer_0_nrlibs = \ $(addsuffix .NRLIB/code.$(FASLEXT),$(axiom_algebra_layer_0)) diff --git a/src/algebra/catdef.spad.pamphlet b/src/algebra/catdef.spad.pamphlet index 06723e56..76b0f796 100644 --- a/src/algebra/catdef.spad.pamphlet +++ b/src/algebra/catdef.spad.pamphlet @@ -245,9 +245,10 @@ BasicType(): Category == Type with ++ Category of types equipped with a total ordering. ++ Axioms: ++ forall(x,y) -++ x > y = y < x -++ x <= y = not(y > x) -++ x >= y = not(x < y) +++ x > y <=> y < x +++ x <= y <=> not(y > x) +++ x >= y <=> not(x < y) +++ x <= y and x >= y => x = y OrderedType(): Category == BasicType with < : (%,%) -> Boolean ++ \spad{x < y} holds if \spad{x} is less than \spad{y} in the @@ -282,6 +283,27 @@ OrderedType(): Category == BasicType with @ +\section{Ordered Structure} + +<<domain ORDSTRCT OrderedStructure>>= +++ Author: Gabriel Dos Reis +++ Date Created: June 28, 2010 +++ Date Last Modified: June 28, 2010 +++ See Also: OrderedType +++ Description: +++ This domain turns any total ordering \spad{f} on a type \spad{T} into +++ a model of the category \spadtype{OrderedType}. +)abbrev domain ORDSTRCT OrderedStructure +OrderedStructure(T: Type,f: (T,T) -> Boolean): Public == Private where + Public == Join(OrderedType,HomotopicTo T) + Private == T add + coerce(x: %): T == rep x + coerce(y: T): % == per y + x < y == f(rep x,rep y) + +@ + + \section{category BMODULE BiModule} @@ -2032,6 +2054,7 @@ VectorSpace(S:Field): Category == Module(S) with <<category BASTYPE BasicType>> <<category ORDTYPE OrderedType>> +<<domain ORDSTRCT OrderedStructure>> <<category SETCAT SetCategory>> <<category STEP StepThrough>> <<category SGROUP SemiGroup>> |