Hello everyone,
I have a question on how to prove a theorem relying on lemmas with
existentials in their conclusion:
Take an arbitrary theorem of the form
val test = Q.prove (``!P Q R. P ==> ?m. Q m /\ R m``, cheat)
where P may be arbitrarily complex.
If I want to use the aforementioned theorem in another proof obtaining
its conclusion as an additional hypothesis, the only way I can currently
handle this is by writing the conclusion down explicitly and then
discharging the proof with "by":
`?m. Q m /\ R m` by (irule test \\ ...)
In Coq, I could just say
destruct test as ...
which would generate a subgoal for the P occurring on the left side of
the arrow.
Is there a way of having similar behavior in HOL4, or at least to
improve upon writing it all by hand?
Thanks,
Heiko
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
