Stream: General

Topic: Programmatically eta-reduce theorem conclusion

view this post on Zulip Josh Chen (Aug 10 2019 at 21:23):

Hi all, I want to have an Isabelle/ML function that takes a theorem and completely eta-reduces all the terms in its conclusion. Is there an idiomatic way to do this? I'm still trying to get this working after over a day of "looking up the Isabelle 'documentation'".

view this post on Zulip Mathias Fleury (Aug 11 2019 at 07:51):

IIRC eta reduction is done automatically when constructing theorems (but I don’t have Isabelle to test it right now).

view this post on Zulip Josh Chen (Aug 11 2019 at 15:28):

It "usually" is, but methods (e.g. induction, and maybe the simplifier?) sometimes eta-expand in the middle of a proof and I need the eta-normalized form again.

I've figured it out using conversions and other bits from Thm.ML.

Last updated: Aug 15 2022 at 04:16 UTC