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

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