Re: [isabelle] eta-contracted definitions and unfolding



Quoting Makarius <makarius at sketis.net>:

On Wed, 8 Apr 2009, Peter Gammie wrote:

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

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

For now you can use the following workaround:

  lemma "f' = g'"
    unfolding f_def_raw g_def_raw ...

There is another workaround that I have used before. You can just use an eta-expanded version of your lemma, like this:

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

lemma foo: "(%x y. f' x y) = (%x y. g' x y)"
unfolding f'_def g'_def
sorry

Also note that the eta-expanded version of a lemma will work anywhere the eta-contracted version will, for example:

lemma bar: "f' = g'"
by (rule foo)

- Brian







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