*To*: Wenda Li <wl302 at cam.ac.uk>*Subject*: Re: [isabelle] Problems with code-datatype*From*: René Thiemann <rene.thiemann at uibk.ac.at>*Date*: Sun, 28 Sep 2014 09:11:22 +0900*Cc*: Cl-isabelle Users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <25d9ff3ada61aa5addb91990cc942ec0@cam.ac.uk>*References*: <25d9ff3ada61aa5addb91990cc942ec0@cam.ac.uk>

Dear Wenda, >> Reading the manual on code-generation and "Data Refinement in Isabelle/HOL", I realized that >> page 109 it is mentioned that for abstract type A and concrete type C one can >> lift a function f :: C => (C)? => C to a function f whose type should be A => (A)? => A. >> So does that mean that I won't be able to define my function create_foo as essentially it is >> of type C => A? > > This is not quite true, as you can define > > lift_definition g:: "test => no_B " > is "% t. if t = B then A else t" > by auto > > and the code generation works fine. In terms of > > lift_definition get_no_B :: "test => no_B option" > is "% t. if t = B then None else Some t" > by auto > > I think the problem is with > > get_no_B.rep_eq: map_option Rep_no_B (get_no_B ?x) = (if ?x = B then None else Some ?x) I fully agree. > An ideal code abstract equation for type no_B is of the form > > Rep_no_B (f ...) = ... > > so that code equations that preserve invariants of no_B could be derived for f. Lemma get_no_B.rep_eq does not match such format, and I guess that is why code generation fails for get_no_B (although in theory I think we can still derive code equations in such cases). Again I agree, in principle the test ensures that no bad terms can walk below an Abs_no_B. > Experts on data refinements should be able to comment more ;-) > > Hope this helps, Definitely it was helpful, thanks a lot. Based on your definition of get_no_B I now could modify my code as follows to my original setting, which now is code-exportable. datatype test = A | B | C typedef no_B = "{ t :: test. t ~= B}" by auto setup_lifting type_definition_no_B lift_definition get_test :: "no_B => test" is "% x. x" . lift_definition get_no_B' :: "test => no_B" is "% t. if t = B then A else t" by auto definition get_no_B :: "test => no_B option" where "get_no_B t = (if t = B then None else Some (get_no_B' t))" lemma get_no_B: "get_no_B t = Some no_b ==> get_test no_b = t" unfolding get_no_B_def by (cases "t = B", simp_all, transfer, auto) export_code get_test in Haskell export_code get_no_B in Haskell However, this solution has the small problem, that the test "t = B" is done in both get_no_B and get_no_B'. In my real application this test "t = B" is a bit more complicated to compute, so still the solution is not optimal. (The original definition of get_no_B only had one test "t = B") Cheers, René

**Follow-Ups**:**Re: [isabelle] Problems with code-datatype***From:*Andreas Lochbihler

**References**:**Re: [isabelle] Problems with code-datatype***From:*Wenda Li

- Previous by Date: Re: [isabelle] Problems with code-datatype
- Next by Date: [isabelle] nested multiset ordering?
- Previous by Thread: Re: [isabelle] Problems with code-datatype
- Next by Thread: Re: [isabelle] Problems with code-datatype
- Cl-isabelle-users September 2014 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