Re: [isabelle] Datatype Morphisms in Isabelle
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.
On Sat, Dec 22, 2012 at 2:40 PM, Alfio Martini <alfio.martini at acm.org>wrote:
> 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')=
> More generally, how can I model datatype morphisms in Isabelle, so that
> the case above
> is just a simple inclusion arrow.
> Many thanks!
> Alfio Ricardo Martini
> PhD in Computer Science (TU Berlin)
> Associate Professor at Faculty of Informatics (PUCRS)
> Coordenador do Curso de Ciência da Computação
> Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
> 90619-900 -Porto Alegre - RS - Brasil
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Coordenador do Curso de Ciência da Computação
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil
This archive was generated by a fusion of
Pipermail (Mailman edition) and