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.

Best!

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')=
> L'?
>
> 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 MHonArc.