Re: [isabelle] Prove by instantiation



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

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



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