Josh Chen (Aug 10 2019 at 21:23): 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'".
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).
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: Apr 24 2024 at 08:20 UTC