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

Moving existential quantifiers out over universal quantifiers





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.

This approach leads to tedious, unmaintainable, proofs.


I can see the way forward in writing my first PVS strategy, but before
I embark on this endeavor, I was wondering whether anyone else has met
and solved the same problem, or whether I'm missing something obvious.


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.

I can't help feeling that I may be missing something obvious.


-- 
Paul Loewenstein          Sun Microsystems Inc., Mailstop UMPK12-302
Staff Engineer            901 San Antonio Road, Palo Alto, California 94303
		          Tel: 650-786-6015  FAX: 650-568-9603
                          paul.loewenstein@eng.sun.com