Email Gateway (Aug 22 2022 at 15:22): Email Gateway (Aug 22 2022 at 15:22):From: Diego Marmsoler <diego.marmsoler@tum.de>
Dear all,
Im 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
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: Nov 21 2024 at 12:39 UTC