# [isabelle] Unify.matchers and term representation

```Hello,

I see that the instantiations Unify.matchers finds may not necessarily
have the simplest internal representation. For example:

ML {*
val trm = @{term "(bar::nat set) = bar"};
val pat = @{cpat "(?foo::(?'a => ?'b) => ?'c) (bar::(?'a => ?'b))"}
|> term_of;
val mtchsq = Unify.matchers @{theory} [(pat,trm)];
val mtchs = Seq.list_of mtchsq;
*}

The first match gives this instantiation for ?foo:

[?foo::(nat => bool) => ?'c := %a::nat => bool. a = a]

Now, if we look at the internal representation of the term, it actually is:

Abs ("", "Nat.nat => HOL.bool",
Const ("HOL.eq", "(Nat.nat => HOL.bool) => (Nat.nat => HOL.bool)
=> HOL.bool") \$
Abs ("", "Nat.nat", Bound 1 \$ Bound 0) \$ Abs ("", "Nat.nat",
Bound 1 \$ Bound 0))

It is unnecessarily large. A simpler representation would be:

Abs ("", "Nat.nat  => HOL.bool",
Const ("HOL.eq", "(Nat.nat => HOL.bool) => (Nat.nat => HOL.bool)
=> HOL.bool") \$ Bound 0 \$
Bound 0)

My question is: Is there a way to reduce the internal representation
of a term from one that contains "reducible" lambda expressions (like
in the first) to one that is leaner (like in the second) in general?
Or, is there a simple way to make the matcher algorithm spit out
leaner internal representations?

Thank you for the help in advance.

John

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.