Re: [isabelle] Query towards pseudo constructors



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:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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