Re: [isabelle] Problems with code-datatype

Hi René,

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")
You can avoid the duplicate test by lifting the invariant no_B to the type "no_B option". To that end, you have to introduce another type constructor, say no_B_option (see below for an adaptation of your example). The tricky bit is to get from no_B_option back to no_B option. There, you must not use lifting in the result type; otherwise, the same problem reoccurs. Here, I use a a case combinator, but your real use case might require something else.

Hope this helps,

datatype test = A | B | C
typedef no_B = "{ t :: test. t ~= B}" by auto

setup_lifting type_definition_no_B

lift_definition A_no_B :: "no_B" is A by simp
lift_definition C_no_B :: "no_B" is C by simp

typedef no_B_option = "{x. B ∉ set_option x}" by auto

setup_lifting type_definition_no_B_option

lift_definition get_no_B' :: "test ⇒ no_B_option"
is "λt . if t = B then None else Some t" by simp

lift_definition unpack_no_B_option :: "no_B_option ⇒ no_B option"
is "λx. (case x of None ⇒ None | Some A ⇒ Some A_no_B | Some C ⇒ Some C_no_B)" .

definition get_no_B :: "test ⇒ no_B option"
where "get_no_B t = unpack_no_B_option (get_no_B' t)"

export_code get_no_B

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