Re: [isabelle] Rep problem



Gabriele Pozzani wrote:

Hello,
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
Gabriele

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.