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 joachim-breitner.de> wrote:
Am Mittwoch, den 06.10.2010, 17:36 +0200 schrieb John Munroe:
> c :: real
> ax1 : "c > 0"
> lemma "EX z. c = z"
> 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);
e-Mail: mail at joachim-breitner.de
Jabber-ID: nomeata at joachim-breitner.de
This archive was generated by a fusion of
Pipermail (Mailman edition) and