# Re: [isabelle] Prove by instantiation

`Thanks for the replies. I'm trying to not prove it by reflexivity, but
``instead by instantiating z to an expression that follows from ax1. Such an
``expression should probably say that "a real that is greater than 0", but I
``can't quite see how that can be expressed.
`
Thanks
John
On Oct 6, 2010 9:38pm, Joachim Breitner <mail at joachim-breitner.de> wrote:

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

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