*To*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Subject*: Re: [isabelle] Query towards pseudo constructors*From*: Wenda Li <wl302 at cam.ac.uk>*Date*: Thu, 04 Sep 2014 13:12:22 +0100*Cc*: Cl-isabelle Users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <54081168.1020403@informatik.tu-muenchen.de>*References*: <d74e6e04f522e64ca4e1f0e01e9f58c5@cam.ac.uk> <54081168.1020403@informatik.tu-muenchen.de>*User-agent*: Roundcube Webmail/1.0.2

Hi Florian, Many thanks for your clarification, it helps a lot.

A pseudo constructor declared using »code_datatype« must be surjective. A pseudo constructor declared using »[code abstype]« must be injective.

Best, Wenda On 2014-09-04 08:14, Florian Haftmann wrote:

Hi Wenda, I am not sure which documentation you have read so far. The »Tutorial on code generation« contains some explanations and examples concerning datatype abstraction. There is also a substantial publication »Data Refinement in Isabelle/HOL«. In short, it is helpful to thinkg about pseudo constructors as morphisms. A pseudo constructor declared using »code_datatype« must be surjective. A pseudo constructor declared using »[code abstype]« must be injective. Cheers, Florian On 03.09.2014 21:41, Wenda Li wrote:Dear data refinement experts, I am trying to learn something about code generation. Based on what I have seen so far, there are two ways to introduce a pseudo constructor for an abstract type A: 1) define constant f:: C => A and g::A => C, and then prove lemma [code abstype]: f (g x) = x ,and f becomes a pseudo constructor for the abstract type A 2) define constant f:: C => A, and then declare code_datatype f Based on my observations, only one of them is used at a time: "Int.thy": code_datatype "0::int" Pos Neg "Real.thy": code_datatype Ratreal "Multiset.thy": code_datatype multiset_of have adopted the second approach, while "Rat.thy": lemma [code abstype]:"Frct (quotient_of q) = q" "Polynomial.thy": lemma Poly_coeffs [simp, code abstype]: "Poly (coeffs p) = p" have adopted the first approach. It seems that the "code_datatype" approach is more flexible than the"abstype" approach, as multiple constructors can be introduced (I amnotsure if it is not case for the "abstype" approach) and the cardinality of C can be smaller than that of A (e.g. Ratreal in "Real.thy"). My question is: what is the main difference between these two approaches? When shall I choose one over the other? Many thanks in advance, Wenda

-- Wenda Li PhD Candidate Computer Laboratory University of Cambridge

**Follow-Ups**:**Re: [isabelle] Query towards pseudo constructors***From:*Florian Haftmann

**References**:**[isabelle] Query towards pseudo constructors***From:*Wenda Li

**Re: [isabelle] Query towards pseudo constructors***From:*Florian Haftmann

- Previous by Date: [isabelle] new AFP entry: Priority Queues Based on Braun Trees
- Next by Date: Re: [isabelle] Query towards pseudo constructors
- Previous by Thread: Re: [isabelle] Query towards pseudo constructors
- Next by Thread: Re: [isabelle] Query towards pseudo constructors
- 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