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 <[email protected]>, > 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. _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
