Unification issues with OF · Isabelle/ML

I am trying to use the OF combinator with the abstraction theorem from Pure, i.e. (⋀x. ?f x ≡ ?g x) ⟹ λx. ?f x ≡ λx. ?g x. But trying to instantiate the abstraction theorem with the theorem ⋀x. f x ≡ g x yields a unification error (OF: no unifiers). Unification tracing reveals that the clash occurs between Pure.all =/= Pure.eq, but unifying the terms of the theorems manually works fine. Is OF doing something to the theorems that I am not aware of and if so, how can I make the instantiation work?

Mathias Fleury (Jun 18 2021 at 08:18):

lemma H1: ‹(⋀x. f x ≡ g x) ⟹ λx. f x ≡ λx. g x›
  by auto

context
  assumes H2: ‹⋀x. f x ≡ g x›
begin

thm H1[OF H2]

ML ‹@{thm H1} OF @{thms H2}›
end

Mathias Fleury (Jun 18 2021 at 08:19):

Remark however that you don't get exactly the theorem you want because of HO unification

Mathias Fleury (Jun 18 2021 at 08:26):

The HO unification is probably your problem, but we need more details (don't forget to @{print} intermediate results if you are using ML)

Paul Bachmann (Jun 18 2021 at 09:23):

The problem seems to be that the theorem that I want to use as H2 has, in ML, the form Const ("Pure.all", "(?'a1 ⇒ prop) ⇒ prop") $ Abs ("x", "?'a1", ...) while your H2 theorem has the bound variable replacd by a Var. I need this because I explicitly want the x variable to be the bound variable in the lambda term of the conclusion of H1 and my f and g terms might be more complicated and might contain more variables. However, I could also try using the version with a Var in H2, but as you suspected, the unification result I get from that is not exactly what I want, since I simply want f and g in H1 to be instantiated with f and g from H2.

Manuel Eberl (Jun 18 2021 at 09:54):

I think the problem is that instantiation with OF can only instantiate schematic variables, not variables bound by a Pure.all. This is usually not a problem because all theorems you can normally get your hands on have schematic variables instead of outermost-level-universally-meta-quantified variables anyway.

Manuel Eberl (Jun 18 2021 at 09:55):

If you really do have a theorem with outermost-level Pure.all and want to instantiate these variables, you will have to do an explicit elimination of the universal quantifier using e.g. the corresponding functions from the Thm module.

Stream: Isabelle/ML

Topic: Unification issues with OF