[isabelle] Unify.matchers and term representation


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.


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