*To*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Subject*: Re: [isabelle] Query towards pseudo constructors*From*: Wenda Li <wl302 at cam.ac.uk>*Date*: Sun, 21 Sep 2014 21:29:05 +0100*Cc*: Cl-isabelle Users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <5409FE8B.60204@informatik.tu-muenchen.de>*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>*User-agent*: Roundcube Webmail/1.0.2

Hi Florian and Andreas,

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

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 surjectivevs.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 beneitherinjective 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 besurjective. A pseudo constructor declared using »[code abstype]«mustbe injective.Do you mean the other way around? Ratreal::"rat => real" in"Real.thy"(declared using "code_datatype") is an injective but not surjectivefunction, while Frct:: "int \times int => rat" (declared using"[codeabstype]") is a surjective but not injective function. Sorry if Ihavemessed 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»Tutorialon code generation« contains some explanations and examplesconcerningdatatype abstraction. There is also a substantial publication»DataRefinement in Isabelle/HOL«. In short, it is helpful to thinkg about pseudo constructors asmorphisms. A pseudo constructor declared using »code_datatype«must besurjective. A pseudo constructor declared using »[code abstype]«mustbe 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 onwhat Ihave seen so far, there are two ways to introduce a pseudoconstructorfor 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 typeA2) 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 thanthe"abstype" approach, as multiple constructors can be introduced (I am notsure if it is not case for the "abstype" approach) and thecardinalityof 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:*Andreas Lochbihler

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

- Previous by Date: [isabelle] New AFP entry: The Sturm-Tarski Theorem
- Next by Date: Re: [isabelle] detaching sml mode from Prover IDE
- 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