[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