*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Subject*: Re: [isabelle] Problems with code-datatype*From*: René Thiemann <rene.thiemann at uibk.ac.at>*Date*: Tue, 30 Sep 2014 15:14:27 +0200*Cc*: Wenda Li <wl302 at cam.ac.uk>, Cl-isabelle Users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <5429095F.4080401@inf.ethz.ch>*References*: <25d9ff3ada61aa5addb91990cc942ec0@cam.ac.uk> <0B514A24-8963-4ED7-8FA2-AF999CC7E74C@uibk.ac.at> <5429095F.4080401@inf.ethz.ch>

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é

**Follow-Ups**:**Re: [isabelle] Problems with code-datatype***From:*Andreas Lochbihler

**References**:**Re: [isabelle] Problems with code-datatype***From:*Wenda Li

**Re: [isabelle] Problems with code-datatype***From:*René Thiemann

**Re: [isabelle] Problems with code-datatype***From:*Andreas Lochbihler

- Previous by Date: [isabelle] Isabelle
- Next by Date: Re: [isabelle] Number of undos
- Previous by Thread: Re: [isabelle] Problems with code-datatype
- Next by Thread: Re: [isabelle] Problems with code-datatype
- Cl-isabelle-users September 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list