# Re: [isabelle] Query towards pseudo constructors

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.

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«.

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"

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?

Wenda



--
Wenda Li
PhD Candidate
Computer Laboratory
University of Cambridge



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