Re: [isabelle] Curried functions in binding operators
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
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.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and