Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Looking for Transfer Package Introduction in I...

view this post on Zulip Email Gateway (Oct 03 2024 at 19:50):

From: "Hu, Jilin" <hujilin@illinois.edu>
Hello everyone,

Is there some examples or tutorials for the transfer package? I am learning the transfer but the only introduction I can find is the paper “Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL”.

For example, below is a basic structure. What is transfer doing specifically? How can I understand what happens when “apply transfer”.
[cid:image001.png@01DB15A2.4F2A7770]
Thank you very much!

Sincerely,
Jilin Hu

image001.png

view this post on Zulip Email Gateway (Oct 04 2024 at 09:09):

From: Gunnar Teege <cl-isabelle-users@lists.cam.ac.uk>
Am 03.10.24 um 21:48 schrieb Hu, Jilin:

Is there some examples or tutorials for the transfer package? I am
learning the transfer but the only introduction I can find is the paper
“Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL”.

I am not aware of any other, only the (very short) description in the
Isar reference manual. However, I am currently working on a section
about lifting and transfer for the next release of my "Gentle
introduction to Isabelle and Isabelle HOL". You may look forward to it.

For example, below is a basic structure. What is transfer doing
specifically? How can I understand what happens when “apply transfer”.

Put simply it replaces functions defined by lift_definition by their
definition. In your example it replaces pos_mult by the multiplication
(*). Additionally it adapts quantification of variables of type pos_int
according to the type definition. So in your example "apply transfer"
replaces the goal by
⋀(x::nat) y::nat. ⟦(0::nat) < x; (0::nat) < y⟧ ⟹ x * y = y * x
which can be solved by (simp add: mult.commute).

Regards
Gunnar

smime.p7s

view this post on Zulip Email Gateway (Oct 04 2024 at 09:28):

From: Kevin Kappelmann <kevin.kappelmann@tum.de>
Hi Jilin,

You can read about the details of the algorithm in Ondřej Kunčar's thesis:

https://www21.in.tum.de/~kuncar/documents/kuncar-phdthesis.pdf

Best wishes,

Kevin

On 03.10.24 21:48, Hu, Jilin wrote:

Hello everyone,

Is there some examples or tutorials for the transfer package? I am
learning the transfer but the only introduction I can find is the paper
“Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL”.

For example, below is a basic structure. What is transfer doing
specifically? How can I understand what happens when “apply transfer”.

Thank you very much!

Sincerely,

Jilin Hu

Last updated: Jan 04 2025 at 20:18 UTC