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 <[email protected]>
Date: Tuesday, 21 August 2018 at 06:57
To: "[email protected]" <[email protected]>
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
<[email protected]<mailto:[email protected]>> 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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
