*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Subject*: Re: [isabelle] Fwd: Code generation for typedefs with an invariant*From*: Manuel Eberl <manuel at pruvisto.org>*Date*: Fri, 15 Oct 2021 16:52:18 +0200*Authentication-results*: cam.ac.uk; iprev=pass (mta1.cl.cam.ac.uk) smtp.remote-ip=128.232.0.57; spf=none smtp.mailfrom=pruvisto.org; arc=none*Authentication-results*: cam.ac.uk; iprev=pass (smtprelay07.ispgateway.de) smtp.remote-ip=134.119.228.103; spf=none smtp.mailfrom=pruvisto.org; arc=none*In-reply-to*: <6817a65e-dd1f-385f-7ac7-4a54265f1319@pruvisto.org>*References*: <796951f0-49fc-a0f0-1324-3a0b0ee2ed8d@uibk.ac.at> <6817a65e-dd1f-385f-7ac7-4a54265f1319@pruvisto.org>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:91.0) Gecko/20100101 Thunderbird/91.2.0

mk_pos_nat :: nat ⇒ good_nat option mk_pos_nat n = (if good_nat n then Some (Abs_good_nat n) else None)

rel_fun (=) (rel_option pcr_good_nat) (λn. if good n then Some n else None) mk_good_nat Similarly, the function in my last email have the following relations: rel_fun (=) (list_all2 pcr_good_nat) my_complicated_computation my_complicated_computation' The actual generated code should of course be: mk_pos_nat n = (if good_nat n then Some (Abs_good_nat n) else None

Manuel On 14/10/2021 21:31, Manuel Eberl wrote:

Hello, I have a typedef of the form typedef good_nat = "{n::nat. good n}"and I have an executable function that produces a "nat list" where Ihave proven that all entries are good.How can I lift that to an *executable* function that produces a"good_nat list" instead?The way I see it, the usual approach of doing a "code abstype" andspecifying the code equation in terms of some projection out of the"type with invariant" to "type without invariant" doesn't work herebecause I have lists of these things.I do have a workaround involving a second typedef for intermediateresults, but it is very boilerplatey and I'd be happy to know if thereis something easier.See attachment for all the details. Thanks, Manuel

**Follow-Ups**:**Re: [isabelle] Code generation for typedefs with an invariant***From:*Dmitriy Traytel

**References**:**[isabelle] Fwd: Code generation for typedefs with an invariant***From:*Manuel Eberl

- Previous by Date: [isabelle] Fwd: Code generation for typedefs with an invariant
- Next by Date: Re: [isabelle] Code generation for typedefs with an invariant
- Previous by Thread: [isabelle] Fwd: Code generation for typedefs with an invariant
- Next by Thread: Re: [isabelle] Code generation for typedefs with an invariant
- Cl-isabelle-users October 2021 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