# 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.