[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Type-correctness conditions in HOL
I'm trying to provide some of the functionality of the PVS type-system
in the HOL theorem-prover, by beefing up an existing `restricted
quantifier' library to generate type-correctness conditions whenever
it performs `restricted-beta reduction'.
Example in PVS notation:
(LAMBDA (y : P) : y) x
would reduce to
x
with the type-correctness condition
P x.
I've implemented a contextual rewriter so that the right context is
generated for my type-correctness conditions, and I'd like help with a
situation where a condition I generate is too strong.
A : TYPE
P : [A -> bool]
term1 : bool = EXISTS (x : A) : (LAMBDA (y : P) : TRUE) x
term2 : bool = EXISTS (x : P) : TRUE
Here is a minimal PVS theory, where term2 ==> term1, because if you
instantiate the EXISTS in term1 to any x in P then you get TRUE.
The problem is that although term1 may be true (because term2 might
be), the TCC generated for term1 (by my own system and also, I
believe, PVS) is the following:
term_TCC1: OBLIGATION FORALL (x : A) : P(x);
Which may well be false. Can this `too-strong' TCC cause any problems
in PVS?
Thanks,
Joe Hurd
P.S. Thanks to Marieke Huisman and Mike Jones for valuable discussion
and a PVS example.