[isabelle-dev] Normalise theorem wrt an environment

[Lawrence Paulson]

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
On 28 Sep 2021, 11:19 +0100, Kevin Kappelmann <kevin.kappelmann at tum.de>, wrote:

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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20210929/91ee7d85/attachment.htm>