[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
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?


Joe Hurd

P.S. Thanks to Marieke Huisman and Mike Jones for valuable discussion 
and a PVS example.