Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Query towards pseudo constructors

view this post on Zulip Email Gateway (Aug 19 2022 at 15:52):

From: Wenda Li <wl302@cam.ac.uk>
Hi Florian and Andreas,

Many thanks for your previous emails. I now have some further
confusions.

Suppose I have a type A:

consts P:: "real ⇒ bool"
typedef A="{x::real. P x}" sorry

Then, I provide a pseudo constructor C for A:

consts C:: "nat ⇒ A"
consts C':: "A ⇒ nat"
lemma [code abstype]:"C (C' x) = x" sorry

After that, I define a function g and provide an code equation:

consts g::"A ⇒ bool"
lemma [code]: "g (C 0) = True" sorry

Now, I want to check code equations for g and see evaluation of g (C 0):

code_thms g
value "g (C 0)"

but both fail due to

"C" is not a constructor, on left hand side of equation, in theorem:
g (C zero_nat_inst.zero_nat) ≡ True

However, if I specify

code_datatype C

then everything goes as expected. I am a little confused by the
behaviour, since I was assuming both "code abstype" and "code_datatype"
provide a way to construct a pseudo constructor.

Many thanks for any advice,
Wenda

view this post on Zulip Email Gateway (Aug 19 2022 at 15:53):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Wenda,

If you declare a pseudo-constructor via code_abstype, then the pseudo-constructor is must
not occur in any code equation. Instead, you have to phrase all theorems using the
destructor. The reason behind this is that such pseudo-constructors are normally used for
types with invariants, and these invariants cannot be expressed by pattern matching. In
this style, your example should be written as follows:

lemma [code]: "g x = (case C x' of 0 => True)"

If your function returns another value of an code_abstype type, you have to apply the
destructor to the left-hand side.

Hope this helps,
Andreas

view this post on Zulip Email Gateway (Aug 19 2022 at 15:54):

From: Wenda Li <wl302@cam.ac.uk>
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

view this post on Zulip Email Gateway (Aug 19 2022 at 15:58):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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
signature.asc

view this post on Zulip Email Gateway (Aug 19 2022 at 15:59):

From: Wenda Li <wl302@cam.ac.uk>
Hi Florian,

Many thanks for your clarification, it helps a lot.

view this post on Zulip Email Gateway (Aug 19 2022 at 16:00):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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

signature.asc

view this post on Zulip Email Gateway (Aug 19 2022 at 16:00):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Wenda and Florian,

Just my 50 cents: pseudo-constructors with code_datatype can be neither injective nor
surjective. List.set and List.coset are examples of this case.

Andreas

view this post on Zulip Email Gateway (Aug 19 2022 at 16:00):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,

this time I strongly hope that I am more awake than when I wrote the
other two mails ;-).

It's indeed not about surjective vs. injective, but about surjective vs.
total.

Have C :: s => t

If C is a total function, then it is suitable for code_datatype.
If C is surjective (but not necessarily total), then it is suitable for
[code abstype].

Note that in the sense of HOL each function is total. »C is partial«
here means that in generated code C will only be applied to certain
values of s (»abstract datatype«).

Hope this helps,
Florian
signature.asc

Last updated: Nov 21 2024 at 12:39 UTC