*To*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Subject*: Re: [isabelle] Generalized elimination rule?*From*: Peter Lammich <peter.lammich at uni-muenster.de>*Date*: Wed, 10 Mar 2010 09:36:17 +0100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, Brian Huffman <brianh at cs.pdx.edu>*In-reply-to*: <4B96F982.3000205@rsise.anu.edu.au>*References*: <4B86BBA6.803@uni-muenster.de> <cc2478ab1002251054r16465cc0t1f7be1a9ad9a44f2@mail.gmail.com> <4B870B93.1030904@rsise.anu.edu.au> <4B967FA7.80405@uni-muenster.de> <4B96F982.3000205@rsise.anu.edu.au>*User-agent*: Thunderbird 2.0.0.22 (X11/20090625)

Dear Peter, I'm not quite sure if I understand you correctly.Are you talking about the situation where there is a premise (amongthe list of premises of a subgoal) of the form !!x. _==>_ ?(Isn't this rather unusual - could I see an example of how this arises ?)

lemma foo: assumes bla obtains x where "bar x" apply -

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 withmeta-level stuff, and previously I have found that playing around withmeta-level props instead of object level bools doesn't seem to work asexpected. However to my surprise the attached does seem to work - tryit out and see if it works on your problem example.

Thank you very much.

Best, Peter

Regards, Jeremy

**References**:**Re: [isabelle] Generalized elimination rule?***From:*Peter Lammich

**Re: [isabelle] Generalized elimination rule?***From:*Jeremy Dawson

- Previous by Date: Re: [isabelle] bijections to/from the natural numbers
- Next by Date: [isabelle] Automatheo 2010 at FLoC: Call for Papers, Talks, and System Demonstrations
- Previous by Thread: Re: [isabelle] Generalized elimination rule?
- Next by Thread: [isabelle] bijections to/from the natural numbers
- Cl-isabelle-users March 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list