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.



On Oct 6, 2010 9:38pm, Joachim Breitner <mail at> wrote:

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);





Joachim Breitner

e-Mail: mail at


ICQ#: 74513189

Jabber-ID: nomeata at

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