# [isabelle] Function definition

Hi, I'm running into issues delegating the "boring"/homomorphic parts of
recursion over a datatype. Consider the following:

datatype t = N nat | A t | B t t

fun boring :: "(t => t) => t => t" where
"boring f (N n) = N n"
| "boring f (A t) = A (f (boring f t))"
| "boring f (B t1 t2) = B (f (boring f t1)) (f (boring f t2))"

function (sequential) interesting :: "nat => t => t" where
"interesting k (N n) = N (n + k)"
| "interesting k (A t) = A (interesting (k + 1) t)"
| "interesting k t = boring (interesting k) t"
by pat_completeness auto

I hope you can convince yourself that interesting should terminate by
size of the second recursive call argument. Unfortunately, since the
recursive call is hidden by boring, the standard relation "measure ..."
technique doesn't work (you end up with a goal like !!k x l r. ((k, x),
(k, B l r)) \in measure ... for arbitrary x, which doesn't look provable).

Does anyone know how to proceed?

Regards,
--Ed



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