Re: [isabelle] Query towards pseudo constructors

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.


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.