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.