*To*: Wenda Li <wl302 at cam.ac.uk>, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Subject*: Re: [isabelle] Query towards pseudo constructors*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Mon, 22 Sep 2014 10:31:49 +0200*Cc*: Cl-isabelle Users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <eff80b81fb58b7f752afc49e4d0b81c9@cam.ac.uk>*References*: <d74e6e04f522e64ca4e1f0e01e9f58c5@cam.ac.uk> <54081168.1020403@informatik.tu-muenchen.de> <21fa3c01d09af9820081106700365fd7@cam.ac.uk> <54085786.5070005@informatik.tu-muenchen.de> <54085E03.1050800@inf.ethz.ch> <5409FE8B.60204@informatik.tu-muenchen.de> <eff80b81fb58b7f752afc49e4d0b81c9@cam.ac.uk>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.0

Dear Wenda,

lemma [code]: "g x = (case C x' of 0 => True)"

Hope this helps, Andreas On 21/09/14 22:29, Wenda Li wrote:

Hi Florian and Andreas, Many thanks for your previous emails. I now have some further confusions. Suppose I have a type A: consts P:: "real ⇒ bool" typedef A="{x::real. P x}" sorry Then, I provide a pseudo constructor C for A: consts C:: "nat ⇒ A" consts C':: "A ⇒ nat" lemma [code abstype]:"C (C' x) = x" sorry After that, I define a function g and provide an code equation: consts g::"A ⇒ bool" lemma [code]: "g (C 0) = True" sorry Now, I want to check code equations for g and see evaluation of g (C 0): code_thms g value "g (C 0)" but both fail due to "C" is not a constructor, on left hand side of equation, in theorem: g (C zero_nat_inst.zero_nat) ≡ True However, if I specify code_datatype C then everything goes as expected. I am a little confused by the behaviour, since I was assuming both "code abstype" and "code_datatype" provide a way to construct a pseudo constructor. Many thanks for any advice, Wenda On 2014-09-05 19:18, Florian Haftmann wrote:Hi all, this time I strongly hope that I am more awake than when I wrote the other two mails ;-). It's indeed not about surjective vs. injective, but about surjective vs. total. Have C :: s => t If C is a total function, then it is suitable for code_datatype. If C is surjective (but not necessarily total), then it is suitable for [code abstype]. Note that in the sense of HOL each function is total. »C is partial« here means that in generated code C will only be applied to certain values of s (»abstract datatype«). Hope this helps, Florian On 04.09.2014 14:41, Andreas Lochbihler wrote:Hi Wenda and Florian, Just my 50 cents: pseudo-constructors with code_datatype can be neither injective nor surjective. List.set and List.coset are examples of this case. Andreas On 04/09/14 14:13, Florian Haftmann wrote:Hi Wenda, On 04.09.2014 14:12, Wenda Li wrote: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.Do you mean the other way around? Ratreal::"rat => real" in "Real.thy" (declared using "code_datatype") is an injective but not surjective function, while Frct:: "int \times int => rat" (declared using "[code abstype]") is a surjective but not injective function. Sorry if I have messed with any definitions.thanks for clarifying, I have made a slip here. Cheers, FlorianBest, 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 am not sure 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

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

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

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

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

**Re: [isabelle] Query towards pseudo constructors***From:*Andreas Lochbihler

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

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

- Previous by Date: Re: [isabelle] detaching sml mode from Prover IDE
- Next by Date: Re: [isabelle] Usability Lifting and Transfer
- Previous by Thread: Re: [isabelle] Query towards pseudo constructors
- Next by Thread: [isabelle] Indent command in JEDIT/ISabelle
- 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