[isabelle-dev] ML tactic for eta-contracting a goal

Brian Huffman brianh at cs.pdx.edu
Sat May 22 21:54:58 CEST 2010

I think I just found answer to my question:

fun eta_tac i = CONVERSION Thm.eta_conversion i

I had never used "CONVERSION" until now. I guess that what it does is
apply the conversion to the entire subgoal?

- Brian

On Sat, May 22, 2010 at 12:07 PM, Brian Huffman <brianh at cs.pdx.edu> wrote:
> Does a simple tactic exist for performing eta-contraction on a goal,
> at the ML level?
> I need to use explicit eta-contraction in some internal proof scripts
> for the HOLCF fixrec package, to avoid the weird interactions with
> eta-contraction and simplifier congruence rules that I have complained
> about recently.
> I found that "apply (subst refl)" will eta-contract the current goal,
> and so currently I am using the following function which does the ML
> equivalent:
> fun eta_tac (ctxt : Proof.context) : int -> tactic =
>  EqSubst.eqsubst_tac ctxt [0] @{thms refl};
> But this code is far from self-explanatory, and it seems like there
> must be a simpler, more direct way to do this. In particular, it
> doesn't seem like eta_tac should need to take a Proof.context as an
> argument.
> - Brian

More information about the isabelle-dev mailing list