Re: [isabelle] Generalized elimination rule?
Exactly. I ran into this situation, when proving elimination rules
(e.g., on Isar, containing "obtains").
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 ?)
obtains x where "bar x"
** 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).
This archive was generated by a fusion of
Pipermail (Mailman edition) and