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
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
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
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
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: Mar 04 2024 at 10:08 UTC