# [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.*