Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Code equations for Rep in lift_definition with...


view this post on Zulip Email Gateway (Jun 12 2021 at 10:42):

From: "C.A. Watt" <caw77@cam.ac.uk>
Dear list

I am stuck trying to get an example to generate executable code. A
stripped down version is attached. I define a type "my_nat", set up as a
trivial quotient of nat. I lift a definition

definition all_zeros :: "nat list => bool"

to

lift_definition my_all_zeros :: "my_nat list => bool" is all_zeros .

When I attempt to export the code of the lifted function, I get the
error "No code equations for Rep_my_nat".

It looks like this is caused by the code equation for my_all_zeros
working out as

my_all_zeros ?xa ≡ all_zeros (map Rep_my_nat ?xa)

Is there a way to make code generation work with this quotient/lifting
setup? I found the "code_dt" flag to lift_definition, which seems to be
documented in isar-ref as dealing with something vaguely related, but it
doesn't affect the behaviour here.

Best wishes
Conrad Watt
Test.thy

view this post on Zulip Email Gateway (Jun 13 2021 at 17:56):

From: "C.A. Watt" <caw77@cam.ac.uk>
To follow up, Mark Wassell pointed out to me that changing the
definition of my_nat to

typedef my_nat = "{ n :: nat . True }" by auto

causes code generation to work as expected. It seems that, as part of
the above definition, a lemma

Rep_my_nat: "Rep_my_nat (Abs_my_nat ?x) ≡ ?x"

is generated and used as a code equation, allowing extraction to work.

The declaration in my original example

typedef my_nat = "UNIV :: (nat) set" ..

also causes a lemma of the same name to be generated, but of a very
different form, which presumably can't be used as a code equation, hence
my issues:

Rep_my_nat: "Rep_my_nat ?x \in UNIV"

If I prove the lemma generated by Mark's definition myself and declare
it as [code], extraction works as desired. Does anyone have any insight
as to why these two typedef forms have different behaviour here?

Best wishes
Conrad


Last updated: Oct 25 2021 at 19:15 UTC