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

*To*: pvs@csl.sri.com*Subject*: Type-correctness conditions in HOL*From*: Joe Hurd <Joe.Hurd@cl.cam.ac.uk>*Date*: Wed, 02 Aug 2000 17:45:44 +0100*cc*: marieke@cs.kun.nl, mjones@cs.utah.edu, konrad.slind@cl.cam.ac.uk, mike.gordon@cl.cam.ac.uk*Delivery-Date*: Wed Aug 2 09:46:05 2000

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.

**Follow-Ups**:**Re: Type-correctness conditions in HOL***From:*Hendrik Tews <tews@tcs.inf.tu-dresden.de>

- Prev by Date:
**rewriting lemmas** - Next by Date:
**TCC's** - Prev by thread:
**rewriting lemmas** - Next by thread:
**Re: Type-correctness conditions in HOL** - Index(es):