Dear Ed,
as Manuel indicated, you'll likely have to define your function in
another way.
One way would be to use mutual recursion:
function (sequential)
interesting :: "nat ⇒ t ⇒ t" and
boring :: "nat ⇒ t ⇒ t"
where
"interesting k (N n) = N (n + k)"
| "interesting k (A t) = A (interesting (k + 1) t)"
| "interesting k t = boring k t"
| "boring k (N n) = N n"
| "boring k (A t) = A (interesting k (boring k t))"
| "boring k (B t1 t2) = B (interesting k (boring k t1)) (interesting k
(boring k t2))"
by (pat_completeness) auto
where your "boring" is replaced by a variant that only takes "k" as
parameter. Then we can prove that both functions are size-preserving, as
already suggested by Manuel.
lemma [termination_simp]:
shows "interesting_boring_dom (Inl (k, t)) ⟹ size (interesting k t) =
size t"
and "interesting_boring_dom (Inr (k, t)) ⟹ size (boring k t) = size t"
by (induct k t and k t rule: interesting_boring.pinduct)
(simp_all add: interesting.psimps boring.psimps)
Which incidentally suffices for termination:
termination by (lexicographic_order)
It remains to show that this actually corresponds to your original
function specification. Here, I use "boring'" for your "boring".
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))"
Your definition of "interesting" (modulo "case" on the right vs.
pattern-matching on the left) can be obtained by mutual induction:
lemma
shows "interesting k s =
(case s of
N n ⇒ N (n + k)
| A t ⇒ A (interesting (k + 1) t)
| t ⇒ boring' (interesting k) t)"
and "boring k s = boring' (interesting k) s"
by (induct k s and k s rule: interesting_boring.induct) auto
cheers
chris
PS: For those who care and know what I'm talking about: termination of
the TRS corresponding to "interesting" and "boring" is trivial for
modern termination tools. Maybe a reason to revive IsaFoR/TermFun? ;)