Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Lifting and Code Generator

Email Gateway (Jun 24 2025 at 16:05):

From: "\"Marmsoler, Diego\"" <cl-isabelle-users@lists.cam.ac.uk>
Hi List,

I do have a question regarding the lifting package and in particular its impact on the code generator.

Let’s say I have two datatypes A and B and I want to use the lifting package to transfer terms (and properties) from A to B.
Moreover, I have a function defined over B.
Then, after setting up the lifting package, the code generator gives an error that a constructor for B is not a constructor.

Here is a minimal example:

datatype A =
Value

datatype B =
Value

fun myfun where
"myfun Value = Value"

fun A_to_B where
"A_to_B (A.Value) = B.Value"

fun B_to_A where
"B_to_A (B.Value) = A.Value"

fun T where
"T (A.Value) (B.Value) = True"

lemma q: "Quotient (=) A_to_B B_to_A T"
sorry

setup_lifting q

lemma "myfun Value ≡ Value" apply eval

The last line gives the error that B.Value is not a constructor.

Any suggestions about what I am doing wrong here would be much appreciated.

Thanks,

Diego

Diego Marmsoler
Senior Lecturer (Education and Research), Computer Science
PI of Secure Smart Contracts with Isabelle/Solidity (https://sites.exeter.ac.uk/isabelle-solidity/)
Deputy Director of Education and Student Experience
University of Exeter, Innovation 1, Room 10
www: marmsoler.com<http://www.marmsoler.com/>
Twitter: @DiegoMarmsoler<https://twitter.com/DiegoMarmsoler>

Email Gateway (Jun 24 2025 at 16:34):

From: Florian Haftmann <florian.haftmann@cit.tum.de>
Hi Diego,

setup_lifting does some »smart« guessing whether and how the type
relationship can be employed towards code generation.

I found no option to suppress what, but maybe somebody else knows about
this?

You can restore the original code setup issuing

code_datatype B.Value

directly after setup_lifting.

Hope this helps,
Florian

Am 24.06.25 um 18:04 schrieb "Marmsoler, Diego" (via cl-isabelle-users
Mailing List):

Hi List,

I do have a question regarding the lifting package and in particular its
impact on the code generator.

Let’s say I have two datatypes A and B and I want to use the lifting
package to transfer terms (and properties) from A to B.

Moreover, I have a function defined over B.

Then, after setting up the lifting package, the code generator gives an
error that a constructor for B is not a constructor.

Here is a minimal example:

---

datatype A =

Value

datatype B =

Value

fun myfun where

"myfun Value = Value"

fun A_to_B where

"A_to_B (A.Value) = B.Value"

fun B_to_A where

"B_to_A (B.Value) = A.Value"

fun T where

"T (A.Value) (B.Value) = True"

lemma q: "Quotient (=) A_to_B B_to_A T"

sorry

setup_lifting q

lemma "myfun Value ≡ Value" apply eval

---

The last line gives the error that B.Value is not a constructor.

Any suggestions about what I am doing wrong here would be much appreciated.

Thanks,

Diego

Diego Marmsoler
Senior Lecturer (Education and Research), Computer Science
PI of Secure Smart Contracts with Isabelle/Solidity (https://
sites.exeter.ac.uk/isabelle-solidity/ <https://sites.exeter.ac.uk/
isabelle-solidity/>)
Deputy Director of Education and Student Experience
University of Exeter, Innovation 1, Room 10

www: marmsoler.com <http://www.marmsoler.com/>
Twitter: @DiegoMarmsoler <https://twitter.com/DiegoMarmsoler>

OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc

Last updated: Jul 02 2025 at 08:30 UTC