*To*: Peter Vincent Homeier <palantir at trustworthytools.com>*Subject*: Re: [isabelle] Be nice to have short tutorials on Quotient Types and Lifting*From*: Gottfried Barrow <gottfried.barrow at gmx.com>*Date*: Wed, 22 May 2013 11:07:42 -0500*Cc*: Isabelle Users ML <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <CAGneiuKE0z2USTOQoL204WH29U9sWPHFJSFoS98gO1=YxDoqmA@mail.gmail.com>*References*: <519C1E60.8080300@gmx.com> <CAGneiuKE0z2USTOQoL204WH29U9sWPHFJSFoS98gO1=YxDoqmA@mail.gmail.com>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

On 5/22/2013 9:15 AM, Peter Vincent Homeier wrote:

To provide "some real understanding of what's going on," you may wishto check one of the original writings about quotient types andlifting, written about the HOL4 implementation:http://www.trustworthytools.com/quotients/quotient.pdf

Peter, Thanks for the link.

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

Thanks, GB

Hope this helps. PeterOn 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)

**References**:**[isabelle] Be nice to have short tutorials on Quotient Types and Lifting***From:*Gottfried Barrow

**Re: [isabelle] Be nice to have short tutorials on Quotient Types and Lifting***From:*Peter Vincent Homeier

- Previous by Date: Re: [isabelle] [isabelle-dev] The-operator
- Next by Date: [isabelle] Two lemmas about lists constructed from finite sets that I'd like Isabelle to provide
- Previous by Thread: Re: [isabelle] Be nice to have short tutorials on Quotient Types and Lifting
- Next by Thread: [isabelle] LFMTP'13: Logical Frameworks and Meta-Languages (CFP)
- Cl-isabelle-users May 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list