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



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

On 12/05/2013 08:52 AM, 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.