# Re: [isabelle] Problems with code-datatype

```Hi Andreas,

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

First of all, thanks for your hints.

Unfortunately I was not able to adapt your proposed solution to my case for the following reasons.

1) I do not see why in your solution there is only one test "t = B":
in get_noB' there definitely is one "t = B" test, and the second one is hidden in
unpack_no_B_option, where again you make a case analysis which seems similar to a "t = B" test,
i.e., here you have to choose the reason why the value is in no_B (whether it is the reason A or C)

2) I did not understand why the type-copy no_B_option should help at all: with A_no_B and C_no_B at hand you can
more easily and directly define

definition get_no_B :: "test => no_B option" where
"get_no_B t == if t = B then None else case t of A => Some A_no_B | C => Some C_no_B"

or even

definition get_no_B :: "test => no_B option" where
"get_no_B t == case t of A => Some A_no_B | B => None | C => Some C_no_B"

> Here, I use a a case combinator, but your real use case might require something else.

3) Exactly. In my real case I have

typedef special_functions = "{ f :: nat => nat. P f}"

where P is some predicate of interest on functions. Here, I do not see how I can easily write functions similar to "A_no_B" or "C_no_B"
which always create objects of special_function type (without actually checking P).
This would then again lead to two invocations of checking P: one in the function corresponding to "A_no_B", and the other similar to get_no_B
with then checks whether it should return None or Some.

Cheers,
René

```

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