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

[Brian Huffman]

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
>