Re: [isabelle] Generalized elimination rule?




Dear Peter,

I'm not quite sure if I understand you correctly.

Are you talking about the situation where there is a premise (among the list of premises of a subgoal) of the form !!x. _==>_ ?
(Isn't this rather unusual - could I see an example of how this arises ?)
Exactly. I ran into this situation, when proving elimination rules (e.g., on Isar, containing "obtains").

lemma foo:
 assumes bla
 obtains x where "bar x"
 apply -
** You end up with a subgoal something like [| bla; !!x. bar x ==> thesis |] ==> thesis


Certainly, keep, as I defined it, won't wrap around a premise of the form
!!x. _==>_ because such a premise is of type prop, not bool.
Isabelle generally - I think - wasn't intended to work very much with meta-level stuff, and previously I have found that playing around with meta-level props instead of object level bools doesn't seem to work as expected. However to my surprise the attached does seem to work - try it out and see if it works on your problem example.
Thank you very much.
I certainly will try it. (For now, I modified the val nhyps=... to only count plain premises).

Best,
 Peter


Regards,

Jeremy








This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.