Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] primcorec on enat


view this post on Zulip Email Gateway (Aug 22 2022 at 15:22):

From: Diego Marmsoler <diego.marmsoler@tum.de>
Dear all,

I’m currently trying to develop an Isabelle/HOL Theory using the new
“codatatype” package.

I have constructed a simple codatatype similar to a lazy list and wanted to
implement a primitive corecursive function which returns the length of this
list as an enat (extended natural number from the
Coinductive/Coinductive_Nat package).

My problem is now that I get an error message “enat is not a codatatype”.
Thus, it cannot be used as a return type for corecursive functions.

My question is now whether someone knows about an implementation of extended
natural numbers as codatatype so that it can be used as return value for
corecursive functions?

Many thanks,

Best,

Diego
smime.p7s

view this post on Zulip Email Gateway (Aug 22 2022 at 15:22):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Diego,

Extended natural numbers can be seen both as

datatype enat = enat nat | \<infinity>

and as

codatatype enat = 0 | eSuc enat

In Isabelle/HOL's library, extended natural numbers are defined with the datatype
representation in mind. My AFP entry Coinductive
(https://www.isa-afp.org/entries/Coinductive.shtml) provides the coinductive view for
enat. That it, defines the relevant constants and reasoning principles for considering
enat as a codatatype. Unfortunately, you cannot register it as a codatatype once it has
been defined as a datatype. Thus, you have to define your length function directly using
the coiterator enat_unfold instead of using primrec, which basically does this internally
for you. The reasoning is the same in both cases.

Also note that my AFP entry also contains a large library about lazy lists, which also
includes a length function.

Hope this helps,
Andreas


Last updated: Mar 29 2024 at 12:28 UTC