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



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

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/.

Hope this helps.

Peter





On Tue, May 21, 2013 at 9:24 PM, Gottfried Barrow
<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.