Hello,
I am needing to transform a goal of the form: "?x.!y. (P x y)" into
"!y.?x. (P x y)" but I haven't been able to find anything like that in
the "bool" theory (or anywhere else). I looked for it using:
DB.match ["-"] ``!P. (!x.?y. P) ==> (?y.!x. P)``;
but this didn't bring any results.
On the other hand, I know it is true that:
?x.!y. (P x y) ==> !y.?x. (P x y)
(which is what I need).
I also tried doing:
e (Q_TAC SUFF_TAC <instance of what I want to prove> THEN1 METIS_TAC [])
but it failed.
Is there any way to do this in HOL? How do I look for this kind of
rules/conversions in the existing theories?
Thank you,
Juan
-------------------------------------------------------------------------
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2005.
http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
