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

*To*: pvs-help@csl.sri.com*Subject*: Re: Moving existential quantifiers out over universal quantifiers*From*: Bruno Dutertre <bruno@sdl.sri.com>*Date*: Fri, 01 Oct 1999 10:30:30 -0700*CC*: pvs-help@csl.sri.com*References*: <199909302207.PAA02125@heavengate.eng.sun.com>*Sender*: bruno@csl.sri.com

Paul Loewenstein wrote: > > I have proofs that have antecedent formulas of the form: > > FORALL (x: a): EXISTS (y: b): Formula (x, y) > > which I need to convert to the form: > > EXISTS (z: [a -> b]): FORALL (x: a): Formula (x, z (x)) > > so I can skolemize z without instantiating x. > > I currently do this rather tediously by hand specialization of the lemma: > > FORALL (P: [a -> [b -> boolean]]): > (FORALL (x:a): EXISTS (y:b): P (x) (y)) IMPLIES > (EXISTS (z:[a -> b]): FORALL (x:a): P (x) (z (x))) > > which, somewhat to my surprise, turned out to be provable without > restricting a or b to be non-empty. > (FORWARD-CHAIN ...) with this lemma is capable of instantiating P automatically, at least in simple cases. You could use a stronger lemma as a rewrite rule: FORALL P: (FORALL x: EXISTS y P(x, y)) IFF (EXISTS z: FORALL x: P(x, z(x))). Rewriting with this lemma works better than forward-chaining with the other one. > I also need to apply eagerly the much simpler operation corresponding > to the theorem: > > FORALL (P, Q: [a -> boolean]): > (FORALL (x:a): P (a) AND Q (a)) IMPLIES > (FORALL (x:a): P (a)) AND (FORALL (x:a): Q (a)) > > which would be my zeroth strategy to write. > Rewriting also works here. The rewrite rule is already in the prelude: lemma forall_and in theory quantifier_props. -- Bruno Dutertre | bruno@sdl.sri.com SDL, SRI International | fax: 650 859-2844 333 Ravenswood Avenue, Menlo Park CA 94025 | tel: 650 859-2717

- Prev by Date:
**Moving existential quantifiers out over universal quantifiers** - Next by Date:
**Re: Moving existential quantifiers out over universal quantifiers** - Prev by thread:
**Moving existential quantifiers out over universal quantifiers** - Next by thread:
**Re: Moving existential quantifiers out over universal quantifiers** - Index(es):