Email Gateway (Aug 19 2022 at 11:09): Email Gateway (Aug 19 2022 at 11:09):From: Gottfried Barrow <gottfried.barrow@gmx.com>
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
Email Gateway (Aug 19 2022 at 11:11):From: Peter Vincent Homeier <palantir@trustworthytools.com>
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
Email Gateway (Aug 19 2022 at 11:11):From: Gottfried Barrow <gottfried.barrow@gmx.com>
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:
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@gmx.com <mailto:gottfried.barrow@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)
Last updated: Apr 19 2024 at 12:27 UTC