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

Re: Moving existential quantifiers out over universal quantifiers

Paul: You should be able to state the choice principle
 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)))
as a rewrite rule with equality instead of implies.

You can then invoke it either by installing it an applying ASSERT,
or manually through REWRITE.  The only hitch is that when I tried it,
I found a bug in the higher-order matching that would cause the match to
fail.  I've fixed this and it will appear in the patch file shortly.
The fix, in case you need it right away is:

(defun make-lambda-expr-iter (args* instance)
  (if (null args*) instance
      (make!-lambda-expr (car args*) 
	    (make-lambda-expr-iter (cdr args*)

Cheers, Shankar