[isabelle] Code generation from abstract types

```Dear all,

we were trying to carry out an experiment in code generation over the
Multivariate Analysis Library in Isabelle.

Our idea was to generate code from operations on vectors and matrices,
as defined in that library; in the library, there exists a "vec" type
which is defined as the set of functions from an underlying finite
type to any type. The Abs and Rep operations between that type and the
function type a are called, respectively, vec_lambda (given a function
it returns a "vec") and vec_nth (it returns a function from a "vec").
Matrices are then defined as a "vec of a vec".

When we try to generate code from definitions about vectors (the zero
vector, addition, multiplication), things work perfectly, making use
of the "code abstype" and "code abstract" labels:

theory execution
imports Main
"~~/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space"
begin

lemma [code abstype]: "vec_lambda (vec_nth g) = g" by (metis vec_nth_inverse)

lemma [code abstract]: "vec_nth 0 = (%x. 0)" by (metis zero_index)

lemma [code abstract]: "vec_nth (a + b) =  (%i. a\$i + b\$i)" by (metis

export_code
"(0:: ('a::{zero,plus},'b::finite) vec)"
"op + :: ('a::{zero,plus},'b::finite) vec => ('a,'b) vec => ('a,'b) vec"

When we try to generate code for operations over matrices which return
a matrix (for instance, matrix multiplication), we do not know how to
define the "code abstract" lemma for such operation, since it involves
a "vec_nth of a vec_lambda of a vec_nth", for which the code generator
produces a "violation abstraction error":

lemma mat_mult [code abstract]: "vec_nth (m ** m') = (%f. vec_lambda
(%c. setsum (%k. ((m\$f)\$k) * ((m'\$k)\$c)) (UNIV :: 'n::finite set)))"
unfolding matrix_matrix_mult_def
using vec_lambda_beta by auto

Is there a way to express the previous lemma and that code generation
for matrix multiplication is still possible? Is anybody aware of any
possible workaround?

Thanks a lot for any hint, sorry for not being capable of translating
the example to a generic setting,

Jesus

On Sat, Dec 22, 2012 at 6:44 PM, Alfio Martini <alfio.martini at acm.org> wrote:
> 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

--
Jesús María Aransay Azofra