[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Don't understand this TCC



Can someone help?  I have a simple theory in which I try to introduce a
generic, extended version of the real-valued sum operation for finite
sets.  The theory takes two types as parameters, one declared to be "FROM"
the other, the first intended to be the domain supertype for the extended
version of sum, the other intended to be the original domain type. Here's
the theory:

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Extended_Real_Summation[BD_HDS: TYPE, BD: TYPE FROM BD_HDS] : THEORY

BEGIN

IMPORTING finite_sets@finite_sets_sum_real[BD]

extended_real_sum: [[setof[BD_HDS],[BD_HDS -> real]] -> real] =
  extend[[setof[BD_HDS],[BD_HDS -> real]],
         [finite_set[BD],[BD -> real]],
         real,
         0](sum)

END Extended_Real_Summation
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

When I typecheck this theory, I get the following TCC, which as I
understand it, is not in general provable for all possible type actuals
that could be passed in for the two type parameters:

extended_real_sum_TCC1: OBLIGATION
  (FORALL (x: BD_HDS): BD_pred(x)) AND (FORALL (x: BD_HDS): BD_pred(x));

Isn't this asking me to show twice over that any instance the supertype
is an instance of the subtype?  Why am I getting this TCC?

Thanks in advance for any help,

Mark Aronszajn

Reusable Software Research Group
Dept. of Comp. Sci. & Elec. Eng.
West Virginia University