Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Rep problem

view this post on Zulip Email Gateway (Aug 18 2022 at 09:47):

From: Gabriele Pozzani <gabriele.pozzani@gmail.com>
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

view this post on Zulip Email Gateway (Aug 18 2022 at 09:47):

From: Steven Obua <obua@in.tum.de>
Gabriele Pozzani wrote:

See chapter 8.5.2 in the Isabelle/HOL tutorial.

Steven Obua

Last updated: May 03 2024 at 04:19 UTC