Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Quotients, lifting and transfer in Isabelle2013-1

view this post on Zulip Email Gateway (Aug 19 2022 at 12:56):

From: Ondřej Kunčar <kuncar@in.tum.de>
Hi Randy,
if you are interested in a total quotient, I guess the best example is a
definition of integers as a quotient of a pair of natural numbers. See
HOL/Int.thy.

For a type copy, HOL/Library/Mapping.thy is indeed a classical example.
You might find the type copy used in HOL/Code_Numeral.thy easier.

Ondrej

view this post on Zulip Email Gateway (Aug 19 2022 at 13:13):

From: Randy Pollack <rpollack@inf.ed.ac.uk>
I want to learn about the new lifting and transfer tools. Where can I
see simple examples of their use in the HOL development?

For a total quotient I looked at the classic example of Dlists (in
src/HOL/Quotient_Examples/DList.thy), but it seems to be using the old
quotient package.

For an (abstract) type copy I looked at src/HOL/Library/Mapping.thy,
but found it not completely simple due to the use of "option" in the
definition of map.

Thanks for any pointers,
Randy

view this post on Zulip Email Gateway (Aug 19 2022 at 13:16):

From: Gottfried Barrow <gottfried.barrow@gmx.com>
I wouldn't know new lifting from old lifting, but for Isabelle2013-1,
FSet.thy was moved from src/HOL/Quotient_Examples to src/HOL/Library.
New work has been done on src/HOL/BNF, as I mention below, and lifting
is involved, so I'd guess it's new lifting.

The Isabelle2013 FSet.thy is shown in this folder:

http://isabelle.in.tum.de/repos/isabelle/file/d90218288d51/src/HOL/Quotient_Examples

The Isabelle2013-2 FSet.thy is in this folder:

http://isabelle.in.tum.de/repos/isabelle/file/4dd08fe126ba/src/HOL/Library

You can see that "lift_definition" is used in the new one, whereas it's
not used in the old one.

FSet.thy, along with Library/Multiset.thy, are imported in More_BNFs:

http://isabelle.in.tum.de/repos/isabelle/file/4dd08fe126ba/src/HOL/BNF

Lifting is used now in Isabelle2013-2 BNF/Countable_Type.thy, where it
wasn't used in Isabelle2013.

I think the closest thing to a tutorial are the 2 papers by Kuncar and
Huffman. They're both titled "Lifting and Transfer: A Modular Design for
Quotients in Isabelle/HOL", but they're not exactly the same:

http://www4.in.tum.de/~kuncar/

Regards,
GB

Last updated: May 06 2024 at 12:29 UTC