Re: [isabelle] Rep problem

Gabriele Pozzani wrote:

I defined the type:
consts n::nat
typedef enne = "{x::nat. x>=0 & x<=n}"
automatically Isabelle has defined the function Rep_enne::enne => nat.

Now I have to demonstrate the lemma
Rep_enne i < n

How can I access and use the Rep_enne function definition in the proof?

Thank you very much

See chapter 8.5.2 in the Isabelle/HOL tutorial.

Steven Obua

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