FDL > PVS > Prelude > union_adt_reduce : Theory

PVS-2.4 prelude.pvs

union_adt_reduce [T1:TYPE, T2:TYPE, range:TYPE] : THEORY
BEGIN

IMPORTING union adt[T1, T2]

reduce((inl?_fun:[T1- > range]), (inr?_fun:[T2- > range])) : RECURSIVE [union- > range] =
LAMBDA (union_adtvar:union) : LET (red:[union- > range]) = reduce(inl?_fun, inr?_fun) IN CASES union_adtvar OF inl(inl1_var): inl?_fun(inl1_var), inr(inr1_var): inr?_fun(inr1_var) ENDCASES
;

REDUCE((inl?_fun:[[T1, union]- > range]), (inr?_fun:[[T2, union]- > range])) : RECURSIVE [union- > range] =
LAMBDA (union_adtvar:union) : LET (red:[union- > range]) = REDUCE(inl?_fun, inr?_fun) IN CASES union_adtvar OF inl(inl1_var): inl?_fun(inl1_var, union_adtvar), inr(inr1_var): inr?_fun(inr1_var, union_adtvar) ENDCASES
;

END union_adt_reduce