Thanks. That looks like the thing I need to get my proofs to be shorter.
On 08/30/2017 02:06 PM, michael.norr...@data61.csiro.au wrote:
I don’t know of anything that does exactly this, and it does look like an
appealing thing to have. An easy implementation (tested as per attachment)
would be something like
fun prove_hyp_tac th =
SUBGOAL_THEN (lhand (concl th)) (fn hyp => STRIP_ASSUME_TAC (MP th hyp))
You would then get your effect with
qspecl_then [`param1`, `param2`, `param3`] prove_hyp_tac test
You presumably have to provide the params to the theorem so that you get the
right instantiation and a concrete P to prove.
Screen shot shows it in action. Let me know if that’s not what you meant.
Michael
On 30/8/17, 21:40, "Heiko Becker" <hbec...@mpi-sws.org> wrote:
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
------------------------------------------------------------------------------
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
------------------------------------------------------------------------------
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
