Re: [isabelle] Query towards pseudo constructors

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.

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,

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,
>>     Florian
>>> 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
>>>>> 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


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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