Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] typedef in recursive datatype


view this post on Zulip Email Gateway (Aug 19 2022 at 13:52):

From: Walther Neuper <wneuper@ist.tugraz.at>
I want to re-use an elaborated "typedef" (with identifier "ttt")

definition ppp :: "'a ⇒ bool" where "ppp p = True"
typedef 'a ttt = "{p::'a. ppp p}" unfolding ppp_def by auto

in a recursive datatype

datatype 'a ddd = C0 'a | Cn "('a ddd) ttt"

and get the understandable error message

Non-admissible type expression
'a ddd ttt
"Test.ttt" is not a datatype - can't use it in nested recursion

What is the best way to re-use "ttt" in "ddd" ?
Walther

view this post on Zulip Email Gateway (Aug 19 2022 at 13:52):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Walther,

The old datatype package supports recursion only through datatypes created by the old
datatype package (or registered with rep_datatype). The new datatype package
(~~/src/HOL/BNF/BNF) supports recursion through arbitrary bounded natural functors (BNFs).
However, typedefs are in general not bounded natural function. If your typedef is a BNF,
you can register it with the bnf command. Examples for registration can be found in
~~/src/HOL/BNF/More_BNFs.

Best,
Andreas

view this post on Zulip Email Gateway (Aug 19 2022 at 13:52):

From: Walther Neuper <wneuper@ist.tugraz.at>
On 03/27/2014 09:35 AM, Andreas Lochbihler wrote:

Hi Walther,

The old datatype package supports recursion only through datatypes
created by the old datatype package (or registered with rep_datatype).
The new datatype package (~~/src/HOL/BNF/BNF) supports recursion
through arbitrary bounded natural functors (BNFs). However, typedefs
are in general not bounded natural function. If your typedef is a BNF,
you can register it with the bnf command.

Thank you very much!

Since our typedef is not a BNF, we would need a workaround, which I'll
shortcut by a simpler way (just a list) now.

Examples for registration can be found in ~~/src/HOL/BNF/More_BNFs.

Best,
Andreas

On 27/03/14 09:02, Walther Neuper wrote:

I want to re-use an elaborated "typedef" (with identifier "ttt")

definition ppp :: "'a ⇒ bool" where "ppp p = True"
typedef 'a ttt = "{p::'a. ppp p}" unfolding ppp_def by auto

in a recursive datatype

datatype 'a ddd = C0 'a | Cn "('a ddd) ttt"

and get the understandable error message

Non-admissible type expression
'a ddd ttt
"Test.ttt" is not a datatype - can't use it in nested recursion

What is the best way to re-use "ttt" in "ddd" ?
Walther


Last updated: Mar 29 2024 at 08:18 UTC