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



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


On 12/4/2013 3:52 PM, Randy Pollack wrote:
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







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.