[isabelle] Datatype Morphisms in Isabelle



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.