[isabelle] Problems with code-datatype



Dear all,

I currently have some trouble when trying to build code for types with invariants.
In principle, I have some 

typedef foo = {b :: bar. P b} ...

and now want to construct some function which creates objects of type bar as follows:

setup_lifting type_definition_foo

lift_definition create_foo :: "bar => foo option" is "% b. if P b then Some b else None" ...

However, then I cannot create code for create_foo:
a simple 
  export_code create_foo in Haskell
fails.

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?

Any help is appreciated,

Kind regards,
René

PS: Below you find a more detailed example

theory Test
imports  
  Main
begin

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 option" 
  is "% t. if t = B then None else Some t" 
  by auto

export_code get_test in Haskell 
(* works fine *)

export_code get_no_B in Haskell
(* No code equations for get_no_B *)

declare get_no_B.abs_eq[code]

export_code get_no_B in Haskell
(* Abstraction violation
(in code equation get_no_B ?x ≡
                  map_option Abs_no_B
                   (if equal_test_inst.equal_test ?x
                        B
                    then None else Some ?x)):
constant Abs_no_B *)
(* somehow the violation is just because the criterion seems to be purely
   syntactic. Via the if-then-else it is guaranteed that the invariant of 
   no_B is satisfied ! *)



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