[isabelle] eta-contracted definitions and unfolding



Hello,

I've got a few definitions that are supposed to be partially applied, and unfolding them when they are eta-contracted and unsaturated fails (silently in the case of 'unfolding'). I am surprised this doesn't work in Isabelle2008, e.g.:

theory t
imports Main
begin

constdefs
  f :: "nat ⇒ nat ⇒ nat"
  "f x y ≡ x + y"

  g :: "nat ⇒ nat ⇒ nat"
  "g x y ≡ y + x"

lemma "f = g"
  unfolding f_def g_def
  sorry

definition "f' x y ≡ x + y"
definition "g' x y ≡ y + x"

lemma "f' = g'"
  unfolding f_def g_def
  sorry

end

Has Isabelle always behaved like this?

In my particular cases I can use extensionality, but I'm keen to know if there are alternatives.

Thanks,
Peter.




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