Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] type alias mutually defined with a datatype?

view this post on Zulip Email Gateway (Aug 18 2022 at 11:25):

From: Randy Pollack <rpollack@inf.ed.ac.uk>
The following is accepted:

datatype exp =
Evar nat
| Esbst exp sbst
and sbst = "nat => exp"

but what is the meaning of "sbst" after this definition? E.g. the
following is not accepted:

constdefs
sbstid :: "sbst"
"sbstid == %x. Evar x"

What is the story?

Thanks,
Randy

view this post on Zulip Email Gateway (Aug 18 2022 at 11:26):

From: Alexander Krauss <krauss@in.tum.de>
Randy,

... but it is not what one would expect. You have defined a unit
datatype with the single constructor called "nat => exp". :-)

I am not sure if there is a way to refer to the constructor later, but
you can see that it exists:

lemma "(x::sbst) = y)"
apply (cases x)

goal (1 subgoal):

1. x = nat => exp ==> x = y

However, such definitions should probably not be allowed...

Alex

Last updated: May 03 2024 at 08:18 UTC