# [isabelle] Query towards pseudo constructors

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
--
Wenda Li
PhD Candidate
Computer Laboratory
University of Cambridge

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