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

[Gottfried Barrow]

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

[Peter Vincent Homeier]

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
<gottfrie...@gmx.com>wrote:

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

[Gottfried Barrow]

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