Re: [isabelle] Curried functions in binding operators



Dear Florian,

I am not sure that this would work in general, because "fst x" and "snd x" need not both be in the remaining term. In my example, we would get "Î(a, d). h (fst a) d y" in the first step. For a, there is only "fst a", but no "snd a", so should the simproc trigger once more?

What is more severe is that I do not see how one can possibly get back the original variable names. Once split_def has been unfolded, they seem to be gone forever.

Andreas

On 15/02/15 10:26, Florian Haftmann wrote:
Here are my attempts so far:

1. apply(unfold split_def)
This works but the resulting subgoal is

   "g x Â= (Îy. f x Â= (Îx. h (fst (fst x)) (snd x) y)) = foo

which is much harder to read than the desired

   "g x Â= (Îy. f x Â= (Î((b, c), d). h b d y)) = foo"

I have never tried to tackle that issue, but a rough idea comes to my
mind: an optional simproc which collapses (%x. â fst x â snd x) to (%(a,
b). â a â b â).  No idea how this would work in practice.

	Florian





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