Yes. Use tactics like drule, dxrule and others in this family. See
https://hol-theorem-prover.org/kananaskis-12-helpdocs/help/Docfiles/HTML/Tactic.drule.html
Alternatively, write in a declarative style:
`e` by metis_tac[th] >>
`f` by metis_tac[] >>
Michael
From: Dylan Melville <dylanmelvi...@gmail.com>
Date: Tuesday, 21 August 2018 at 06:57
To: "hol-info@lists.sourceforge.net" <hol-info@lists.sourceforge.net>
Subject: Re: [Hol-info] Assumptions of goal usage
As a more concise question: can you use assumptions of the hypothesis to
eliminate the assumptions of a theorem?
On Mon, Aug 20, 2018, 4:51 PM Dylan Melville
<dylanmelvi...@gmail.com<mailto:dylanmelvi...@gmail.com>> wrote:
Let's say I have a goal,
a /\ b /\ c ==> d
and 2 theorems
a /\ b ==> e
e ==> f
All I need to do to solve the goal is rewrite using a theorem that states `f`,
however I need to first prove e, which is only probable because the goal
assumes `a`.
The basis of my question, is whether or not I can use an assumption of the goal
outside of a tactical. My proof would be a lot more readable if I could use `a`
and `b` to "prove" `e` outside of a tactical application like ASSUM_LIST and
similar tactics require.
------------------------------------------------------------------------------
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
