Email Gateway (Sep 28 2021 at 10:19): Email Gateway (Sep 28 2021 at 10:19):From: Kevin Kappelmann <kevin.kappelmann@tum.de>
Dear list,
I see that there are functions to normalise a type (Envir.norm_type) and
a term (Envir.norm_term) wrt an environment. Is there also a function to
normalise a theorem wrt an environment? If not, I think doing such a
normalisation is very common and should be added to Isabelle/Pure.
Attached, find my proposal for such a function (norm_thm) and some
examples why a simpler alternative (that is akin to the function
described in the Isabelle/ML cookbook [1, page 57]) does not work. The
file compiles using the current Isabelle development version.
Happy to hear your feedback. Best wishes,
Kevin
[1] https://nms.kcl.ac.uk/christian.urban/Cookbook/
Scratch.thy
Email Gateway (Sep 29 2021 at 10:37):From: Lawrence Paulson <lp15@cam.ac.uk>
Thanks for the suggestion and code. I wonder however how common it is to normalise a theorem wrt an environment. Environments are an internal data structure largely tied up with unification and not used to that much outside the kernel.
Larry Paulson
Email Gateway (Sep 29 2021 at 10:41):From: Makarius <makarius@sketis.net>
This is true. Even worse there is a second use for matching, with slightly
different meaning of the same data structure. We have a "Paulson regime" and a
"Nipkow regime" here, from the depths of time of Isabelle development (approx.
1990).
(I did not find time to look at the cookbook example yet. It is de-facto
fan-fiction with relatively little relevance to Isabelle sources and development.)
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Sep 29 2021 at 14:42):From: Kevin Kappelmann <kevin.kappelmann@tum.de>
We had two different user stories at our chair:
The resolution-based methods use the higher-order unifier. However,
one might only be interested in results produced by, for example,
first-order unification when resolving two rules. Hence, a first-order
unifier was used to obtain an environment, the rules instantiated, and
then the instantiated rules resolved.
The second use case indeed is tied to unification - I was working on
an extension to the unifier.
Best wishes,
Kevin
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Sep 29 2021 at 15:50):From: Makarius <makarius@sketis.net>
That counts as "dark matter of the Isabelle Universe".
The Isabelle sources are continuously "garbage collected": anything that is
unused, disappears.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Last updated: Feb 01 2025 at 20:19 UTC