Thanks, irule rules! It is interesting that even though I used Q.SPEC to
specialize some quantifiers, irule treats those just as free variables, and
Q.SPEC acted as rename. I should just use irule and then EXISTS_TAC.
Haitao
On Thu, Feb 28, 2019 at 6:00 PM wrote:
> Use irule; it normalises
I have a theorem that is in a form like !x y z. a ==> b ==> c ==> d and I
would like to match d to the goal. It seems that I need to convert all the
antecedents into a conjunction first. I can (UNDISCH_ALL o SPEC_ALL) to
move everything to the assumptions. But how do I get the conjunctions of
all
Hi Haitao,
it all depends on what exactly you want to do. Sometimes it is as easy
as using GSYM instead of SYM. Of you can use something like DEPTH_CONV
or ONCE_DEPTH_CONV. That's how GSYM is defined in terms of SYM. Or you
could use something more specialised like STRIP_BINDER_CONV or
Rules like SYM do not work with top level binders. What is the recommended
way to use them with binders without having to stack up SPEC and GEN?
Thanks,
Haitao
___
hol-info mailing list
hol-info@lists.sourceforge.net
