## Stream: Isabelle/ML

### Topic: Unification issues with OF

#### Paul Bachmann (Jun 17 2021 at 23:02):

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):

We need more details to understand your problem. The following works:

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

#### Lukas Stevens (Jun 18 2021 at 10:00):

In general, you should probably keep it to schematic variables if possible.

Last updated: Dec 07 2023 at 12:30 UTC