[isabelle] Beta-contraction



Hi List,

I have

    ...
    val ctxt = put_simpset HOL_ss ctxt addsimps inline_thms
  in
    Conv.fconv_rule ( Simplifier.rewrite ctxt ) thm


Unfortunately, the resulting theorem is not beta-contracted (it
contains (%x. ...) x ). 

However, both inline_thms and thm contain no beta redexes.


Is it expected behaviour of the simplifier to introduce 
new beta-redexes, or is this behaviour undesired, and worth
investigating?

In my application the beta-redexes cause problems in further
conversions, as some operations on Thm seem to silently remove them,
and Thm.equals (used in conversion) cannot match (aconv) the terms any
more.
Of cause, I can quick-fix this by introducing Thm.beta_conv, but I
always thought that expected behaviour of Isabelle functions is not to
produce beta-redexes ? 

Thanks for any explanations,
  Peter









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