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? ;)

*Post by Manuel Eberl*Unfortunately, it's not that easy.

You pass the "interesting" function to the "boring" function as a

parameter, and the "boring" function applies that function that it is

given to things. In order for this to work, you need to essentially show

that the "interesting" function that you are defining is only called on

values for which it terminates (i.e. that are smaller than the original

argument that it got)

Normally, this is done with a fundef_cong rule, but in this case, I

don't see how that is possible, because the values that "interesting" is

called on by "boring" are "boring f t1" and "boring f t2" – that means

that you are relying on the fact that the "interesting" function does

not increase the size of its argument.

assumes "⋀y. size (f y) = size y"

shows "size (boring f x) = size x"

using assms by (induction x) simp_all

assumes "interesting_dom (k, t)"

shows "size (interesting k t) = size t"

using assms

interesting.psimps same_size_boring)

However, I have no idea how you would then go on and prove termination.

Termination proofs depend on the call graph that is computed for the

recursive definition, and if you don't have a fundef_cong rule for

boring, that call graph – as you discovered yourself – will be too

coarse (i.e. you will not have the information that you need in your

termination proof). However, as I see it, any cong rule for "boring"

would have to be conditional, which is, as far as I am aware, not

possible for fundef_cong rules.

What you are trying to do may therefore very well be outside of what the

function package can do. (although I'm not 100% sure about that – still,

even if it is possible, I would bet it will be ugly)

My advice would be: try to define your functions in a simpler way.

Proofs involving nested recursion tend to get very ugly very quickly,

because the termination of your function depends on the semantics of

your function, and semantic properties are difficult to use without a

full termination proof.

Cheers,

Manuel