*To*: John Munroe <munddr at gmail.com>*Subject*: Re: [isabelle] Prove by instantiation*From*: Joachim Breitner <mail at joachim-breitner.de>*Date*: Wed, 06 Oct 2010 21:38:49 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <AANLkTik+p8WQyO-LMrypo3VpPNzFFKoTG_0Y_k8hsMBq@mail.gmail.com>*References*: <AANLkTik+p8WQyO-LMrypo3VpPNzFFKoTG_0Y_k8hsMBq@mail.gmail.com>*Sender*: Joachim Breitner <msg at joachim-breitner.de>

Hello, Am Mittwoch, den 06.10.2010, 17:36 +0200 schrieb John Munroe: > axiomatization > c :: real > where > ax1 : "c > 0" > > lemma "EX z. c = z" > sorry > > Can the quantifier be proved by instantiation only? Perhaps, this > question logically follows: is there an expression y such that apply > (rule exI [where x=y])? > > Thank you for the help. I’m not sure what you mean, but maybe this is it? lemma "EX z. c = z" apply (rule exI[of _ c]) apply (rule refl); done Greetings, Joachim -- Joachim Breitner e-Mail: mail at joachim-breitner.de Homepage: http://www.joachim-breitner.de ICQ#: 74513189 Jabber-ID: nomeata at joachim-breitner.de

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] Prove by instantiation***From:*munddr

**Re: [isabelle] Prove by instantiation***From:*munddr

**References**:**[isabelle] Prove by instantiation***From:*John Munroe

- Previous by Date: Re: [isabelle] G.U.T.
- Next by Date: Re: [isabelle] Prove by instantiation
- Previous by Thread: [isabelle] Prove by instantiation
- Next by Thread: Re: [isabelle] Prove by instantiation
- Cl-isabelle-users October 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