Re: [isabelle] Prove by instantiation


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

Attachment: signature.asc
Description: This is a digitally signed message part

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