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

reasoning with typepreds



A TCC is generated by a theory I typechecked and in discharging that TCC I
am faced with proving the following sequent:

[-1]  Sample_pred(s!1)
  |-------
[1]   s!1`Entry_Count(x1!1) >= 0

where variable 's!1' is of type Sample, and the antecedent was introduced
by a call to (typepred "s!1").  The theory in question has a parameter for
a type, Entry, and the type, Sample, is itself declared in the theory as
follows:

Sample: TYPE FROM
  [# Entry_Count: ({f: [Entry -> nat]| is_finite({y: Entry| f(y) > 0})})
     Accepting: bool
  #]

So I should be able to prove the above sequent if I can make use of the
information in this type declaration.  But what rule can I use to get at
this information.  I've come up against similar problems involving
reasoning with the results of the typepred rule on several occasions.  Can
anyone help?

Thanks in advance,

Mark Aronszajn

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