FYI. Somewhat related functionality is in Q.REFINE_EXISTS_TAC, which
can be used to partially instantiate an existential. But you have to
supply a witness, instead of saying "find a witness in the assumptions".
Konrad.
On Thu, Dec 27, 2012 at 5:55 AM, Ramana Kumar wrote:
> Dear Vincent,
>
> I
Dear Vincent,
I think you are right about SATISFY_ss - it can only prove a goal, not
refine it.
There might be something in quantHeuristicsLib that can help, but I'm not
sure.
Do you have a clone of the HOL4 git repository? You could make a pull
request on github after adding HINT_EXISTS_TAC in a
Hi Michael,
I'm regularly amazed by the pearls that HOL4 contains...
I did not know about the SatisfySimps module!
Now, from my first tests, this can only be used to conclude a goal.
Concretely, if I have a goal of the following form:
?x. P x /\ Q x
0. P t
...
where Q
