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

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