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 <michael.norr...@data61.csiro.au> wrote: > Use irule; it normalises implicational theorems like this first, and then > basically applies MATCH_MP_TAC. > > > > Michael > > > > *From: *Haitao Zhang <zhtp...@gmail.com> > *Date: *Friday, 1 March 2019 at 11:03 > *To: *hol-info <hol-info@lists.sourceforge.net> > *Subject: *[Hol-info] MATCH_MP_TAC and canonical implication form > > > > 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 the assumptions? If I (GEN_ALL o DISCH_ALL) I would get back to exactly > where I started! :-) > > > > Thanks, > > Haitao >
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
