Re: [isabelle] Be nice to have short tutorials on Quotient Types and Lifting



On 5/22/2013 9:15 AM, Peter Vincent Homeier wrote:
To provide "some real understanding of what's going on," you may wish to check one of the original writings about quotient types and lifting, written about the HOL4 implementation:

http://www.trustworthytools.com/quotients/quotient.pdf

Peter,

Thanks for the link.

Mick Jagger comes to mind. You don't always get what you want, but if you try sometimes, you just might find, you get what you need, yea yea, you just might find, you get what you need, yea yea, and so forth.

You chapter seven relating the choice operator with the definite choice operator might speed up certain learning processes for me. I've been thinking I'll have to eventually figure out the choice operator, where as a running process, I've intentionally thought many times to not think about the THE operator in HOL.thy.

The actual internal computations involved in lifting a theorem is rather complicated, and would take too long to describe even in a 50 page paper, but the source code of the package is rather well commented, if you can read Standard ML. The source code can be read in the source of the HOL4 system, in the directory <root>/src/quotient/src/.

Yea, so maybe I'm talking more about a user's manual type of doc, rather than one on the theory. Partly it's just a need to document the mechanics of using lifting and quotient types with lots of example and a few high level concepts on what the syntax means.

Like, there's some kind of naming scheme where things are named by adding suffixes and prefixes to other things, but I haven't found where all that's documented and explained in detail to a user for the Isabelle/HOL lifting and quotients packages.

Thanks,
GB



Hope this helps.

Peter





On Tue, May 21, 2013 at 9:24 PM, Gottfried Barrow <gottfried.barrow at gmx.com <mailto:gottfried.barrow at gmx.com>> wrote:

    No one needs to respond to this, but I make this a global request,
    rather than just mention it in another email I'm working on.

    I've been getting some mileage out of a short example using
    lifting that Brian Huffman provided me on Stackoverflow, and just
    using what I see in the sources as templates, but I don't have any
    real understanding of what's going on.

    I'm seeing quotient types and lifting show up in lots of places,
    but I haven't noticed anything in the way of tutorials, and even
    searches in the collection of most documents don't return much, if
    anything.

    In isar-ref.pdf, lifting is all through the document, which
    probably is a big part of why I've been thinking I see it
    mentioned a lot.

    It'd be nice to have something along the lines of the locales,
    classes, codegen, nitpick, sledgehammer, and functions documents.

    I assume no one has time. That's why I say there's no need to respond.

    Regards,
    GB




--
"In Your majesty ride prosperously
because of truth, humility, and righteousness;
and Your right hand shall teach You awesome things." (Psalm 45:4)




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