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?

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

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

The HO unification is probably your problem, but we need more details (don't forget to `@{print}`

intermediate results if you are using ML)

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.

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.

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.

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

Last updated: Dec 07 2023 at 12:30 UTC