# Re: [isabelle] Quotients and code generation for higher-order functions

```Dear Andreas,

```
Thanks for reminding me of the non-canonical representation, I will have a similar issue in my formalization :-) However, in my understanding, a canonical representation is important when using "code abstype"/"code abstract" to restore executability (e.g. Rat.thy Polynomial.thy), while with "code_datatype" it seems that we can deal with executability in a more flexible way (e.g. Real.thy).
```
In this case, if we can prove

```
lemma [code]:"bind_bar (abs_bar x) f = abs_bar (bind x (Îu. rep_bar (f u)))" sorry
```
we should be able to evaluate

value "bind_bar (abs_bar (Stop (1::nat))) (Îu. abs_bar(Stop (u+2)))"

```
value "bind_bar (abs_bar (Go (Îx::nat. Stop (x+2)))) (Îu. abs_bar(Stop (u+2)))"
```
Please correct me if I am wrong at any point.

Wenda

On 2015-07-24 12:14, Andreas Lochbihler wrote:
```
```Hi Wenda,

On 24/07/15 13:05, Wenda Li wrote:
```
lemma [code]:"bind_bar (abs_bar x) f = abs_bar (bind x (Îu. rep_bar (f u)))" sorry
```
Can you prove this in your theory?
```
```Of course, this type-checks and is provable. However, I'd need a code
equation for rep_bar in the form "rep_bar (Abs_bar x) = ...". And for
this, I'd need a notion of canonical representative in the raw type,
which I don't have at the moment. It would require a lot of work (in
Isabelle) to define such a notion. Moreover, the generated code would
have to transform everything into the normal form, which can be
computationally prohibitive.

Best,
Andreas

```
```On 2015-07-24 07:51, Andreas Lochbihler wrote:
```
```Dear all,

I am currently stuck at setting up code generation for a quotient
type. To that end, I have declared an embedding from the raw type to
the quotient type as pseudo-constructor with code_datatype and am now
trying to prove equations that pattern-match on the
pseudo-constructor. There are no canonical representatives in my raw
```
type, so I cannot define an executable function from the quotient type
```to the raw type.

I am stuck at lifting functions in which the quotient type occurs as
the result of higher-order functions. The problem is that I do not
know how to pattern-match on a pseudo-constructor in the result of a
function. Here is an example:

datatype 'a foo = Stop 'a | Go "nat â 'a foo"

primrec bind :: "'a foo â ('a â 'b foo) â 'b foo" where
"bind (Stop x) f = f x"
| "bind (Go c) f = Go (Îx. bind (c x) f)"

```
axiomatization rel :: "'a foo â 'a foo â bool" where rel_eq: "equivp rel"
```  quotient_type 'a bar = "'a foo" / rel by(rule rel_eq)
code_datatype abs_bar

```
lift_definition bind_bar :: "'a bar â ('a â 'b bar) â 'b bar" is bind sorry
```
```
My problem is now to state and prove code equations for bind_bar. Obviously,
```
lemma "bind_bar (abs_bar x) f = abs_bar (bind x f)"

```
does not work, as bind expects f to return a foo, but f returns a bar.
```My next attempt is to inline the recursion of bind. The case for Stop
is easy, but I am out of ideas for Go.

lemma "bind_bar (abs_bar (Stop x)) f = f x"
"bind_bar (abs_bar (Go c)) f = ???"

```
Is there a solution to my problem? Or am I completely on the wrong track.
```
Thanks for any ideas,
Andreas
```
```
```
```
--
Wenda Li
PhD Candidate
Computer Laboratory
University of Cambridge

```

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