[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?


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