# [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
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

(* works fine *)

(* No code equations for get_no_B *)

declare get_no_B.abs_eq[code]

(* 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.