%------------------------------------------------------------------------------
% Pointwise Ordering in Disjoint Union types
%
% Author: David Lester <[email protected]> Manchester University
%
% Version 1.0 03/30/06
%------------------------------------------------------------------------------
sum_orders[T1,T2:TYPE]: THEORY
BEGIN
r1: VAR pred[[T1,T1]]
r2: VAR pred[[T2,T2]]
x,y: VAR union[T1,T2]
; % syntax
+(r1,r2)(x,y):bool = (inl?(x) AND inl?(y) AND r1(left(x), left(y))) OR
(inr?(x) AND inr?(y) AND r2(right(x),right(y)))
sum_preserves_reflexive: JUDGEMENT
+(r1:(reflexive?[T1]),r2:(reflexive?[T2]))
HAS_TYPE (reflexive?[union[T1,T2]])
sum_preserves_transitive: JUDGEMENT
+(r1:(transitive?[T1]),r2:(transitive?[T2]))
HAS_TYPE (transitive?[union[T1,T2]])
sum_preserves_antisymmetric: JUDGEMENT
+(r1:(antisymmetric?[T1]),r2:(antisymmetric?[T2]))
HAS_TYPE (antisymmetric?[union[T1,T2]])
sum_preserves_preorder: JUDGEMENT
+(r1:(preorder?[T1]),r2:(preorder?[T2]))
HAS_TYPE (preorder?[union[T1,T2]])
sum_preserves_partial_order: JUDGEMENT
+(r1:(partial_order?[T1]),r2:(partial_order?[T2]))
HAS_TYPE (partial_order?[union[T1,T2]])
IMPORTING directed_orders[T1], directed_orders[T2],
directed_orders[union[T1,T2]]
sum_preserves_directed_complete: JUDGEMENT
+(r1:(directed_complete?[T1]),r2:(directed_complete?[T2]))
HAS_TYPE (directed_complete?[union[T1,T2]])
sum_preserves_directed_complete_partial_order: JUDGEMENT
+(r1:(directed_complete_partial_order?[T1]),
r2:(directed_complete_partial_order?[T2]))
HAS_TYPE (directed_complete_partial_order?[union[T1,T2]])
END sum_orders
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
