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.


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