Email Gateway (Jun 25 2025 at 21:28): Email Gateway (Jun 25 2025 at 21:28):From: "\"Marmsoler, Diego\"" <cl-isabelle-users@lists.cam.ac.uk>
Hi List,
I do have another question regarding the lifting/transfer package.
When I try to use the transfer proof method to transfer a lemma from one datatype to another it actually did not replace the terms accordingly.
I was able to do it by using transfer_step but it is a bit tedious and I am not sure if it is the way it is supposed to do it or if I am missing something here.
Below is again a concrete example. The issue is with the proof of myfun2.
(**************)
datatype 'a A =
Value 'a
datatype 'a B =
Value 'a
fun myfun1 where
"myfun1 (A.Value a) = a"
fun A_to_B where
"A_to_B (A.Value a) = (B.Value a)"
fun B_to_A where
"B_to_A (B.Value a) = (A.Value a)"
fun T where
"T (A.Value a) (B.Value b) = (a = b)"
lemma q: " Quotient (=) A_to_B B_to_A T"
sorry
setup_lifting q
lift_definition myfun2::"'a B ⇒ 'a" is myfun1 .
lemma myfun2: "myfun2 (B.Value x) = x"
apply transfer_start
apply (subgoal_tac "Transfer.Rel (rel_fun (=) T) A.Value B.Value", assumption)
apply (simp add: Rel_def rel_funI)
apply (subgoal_tac "Transfer.Rel (rel_fun T (=)) myfun1 myfun2",assumption)
apply (metis B.pcr_cr_eq Rel_def myfun2.transfer)
apply transfer_step
apply transfer_step
apply transfer_end
by (simp add: transfer_forall_def)
(**************)
Thanks a lot for your help!
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 26 2025 at 05:45):From: Dmitriy Traytel <cl-isabelle-users@lists.cam.ac.uk>
Hi Diego,
You don’t have the transfer rule for B.Value that relates it to A.Value registered in your setup:
lemma Value_transfer[transfer_rule]: "rel_fun R (pcr_B R) A.Value B.Value"
by (auto simp: rel_fun_def pcr_B_def relcompp_apply intro!: exI[of _ "A.Value _"])
Missing transfer rules are the main reason for transfer to fail. You can inspect existing transfer rules by looking at the theorem transfer_raw. E.g., when searching for B.Value you will see that there is only a parametricity rule for it (one that relates B.Value to another B.Value with a different type) if you do not issue the above declaration.
Best wishes,
Dmitriy
On 25 Jun 2025, at 23.28, Marmsoler, Diego <cl-isabelle-users@lists.cam.ac.uk> wrote:
Hi List,
I do have another question regarding the lifting/transfer package.
When I try to use the transfer proof method to transfer a lemma from one datatype to another it actually did not replace the terms accordingly.
I was able to do it by using transfer_step but it is a bit tedious and I am not sure if it is the way it is supposed to do it or if I am missing something here.
Below is again a concrete example. The issue is with the proof of myfun2.
(**************)
datatype 'a A =
Value 'a
datatype 'a B =
Value 'a
fun myfun1 where
"myfun1 (A.Value a) = a"
fun A_to_B where
"A_to_B (A.Value a) = (B.Value a)"
fun B_to_A where
"B_to_A (B.Value a) = (A.Value a)"
fun T where
"T (A.Value a) (B.Value b) = (a = b)"
lemma q: " Quotient (=) A_to_B B_to_A T"
sorry
setup_lifting q
lift_definition myfun2::"'a B ⇒ 'a" is myfun1 .
lemma myfun2: "myfun2 (B.Value x) = x"
apply transfer_start
apply (subgoal_tac "Transfer.Rel (rel_fun (=) T) A.Value B.Value", assumption)
apply (simp add: Rel_def rel_funI)
apply (subgoal_tac "Transfer.Rel (rel_fun T (=)) myfun1 myfun2",assumption)
apply (metis B.pcr_cr_eq Rel_def myfun2.transfer)
apply transfer_step
apply transfer_step
apply transfer_end
by (simp add: transfer_forall_def)
(**************)
Thanks a lot for your help!
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>
Last updated: Jul 02 2025 at 04:31 UTC