[isabelle-dev] Normalise theorem wrt an environment

[Kevin Kappelmann]

We had two different user stories at our chair:

1. 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.

2. The second use case indeed is tied to unification - I was working on
an extension to the unifier.

Best wishes,

Kevin

On 29.09.21 12:36, Lawrence Paulson wrote:
> 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.