Email Gateway (Aug 19 2022 at 09:36): Email Gateway (Aug 19 2022 at 09:36):From: Alfio Martini <alfio.martini@acm.org>
Dear Isabelle Users,
This is a very simple question:
Assume a language L specifiied by a datatype D, where L = Lang(D). If L is
a subset of L', how
can I write in Isabelle a datatype D', that extends D such that Lang(D')=
L'?
More generally, how can I model datatype morphisms in Isabelle, so that the
case above
is just a simple inclusion arrow.
Many thanks!
Email Gateway (Aug 19 2022 at 09:36):From: Alfio Martini <alfio.martini@acm.org>
Well...I see two ways to do it with my little knowledge of Isabelle:
1) I have just to write a recursive function from D into D' and this is
the morphism I wanted (similar to what is done with boolean datatypes
in the LNCS Tutorial).
2)just to include D as a type (prefixed by a dummy constructor)
in the definition of D'. This seems to be the easiest way, if the D is a
proper subset of D',
and the one I decided to use.
Best!
Last updated: Apr 26 2024 at 16:20 UTC