*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Subject*: Re: [isabelle] Quotients and code generation for higher-order functions*From*: Wenda Li <wl302 at cam.ac.uk>*Date*: Fri, 24 Jul 2015 12:05:15 +0100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <55B1E06E.3060006@inf.ethz.ch>*References*: <55B1E06E.3060006@inf.ethz.ch>*User-agent*: Roundcube Webmail/1.0.2

Hi Andreas, How about

Can you prove this in your theory? Best, Wenda 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: "equivprel"quotient_type 'a bar = "'a foo" / rel by(rule rel_eq) code_datatype abs_barlift_definition bind_bar :: "'a bar â ('a â 'b bar) â 'b bar" is bindsorryMy 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 wrongtrack.Thanks for any ideas, Andreas

-- Wenda Li PhD Candidate Computer Laboratory University of Cambridge

**Follow-Ups**:**Re: [isabelle] Quotients and code generation for higher-order functions***From:*Andreas Lochbihler

**References**:**[isabelle] Quotients and code generation for higher-order functions***From:*Andreas Lochbihler

- Previous by Date: [isabelle] Quotients and code generation for higher-order functions
- Next by Date: Re: [isabelle] Quotients and code generation for higher-order functions
- Previous by Thread: [isabelle] Quotients and code generation for higher-order functions
- Next by Thread: Re: [isabelle] Quotients and code generation for higher-order functions
- Cl-isabelle-users July 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list