Well founded induction on trees

I have an exam (Functional Programming in SML) coming up in a week. I have become fairly confident in the programming language SML and the functional paradigm, but I have a quite big problem with proves.

I am trying to开发者_运维知识库 solve the following question which was a part of the last year exam:

---

Consider the following declarations of a datatype for trees and of two functions:

datatype tree = Lf | Br of int * tree * tree;

fun size Lf = 0
| size(Br(i,t1,t2)) = 1 + size t1 + size t2;

fun sizeI Lf k = k
| sizeI (Br(i,t1,t2)) k = sizeI t1 (1 + sizeI t2 k);

Prove that

sizeI tr k = k + size tr

holds for all trees tr and all integers k.

---

I want to solve the above question by using Well Founded Induction. To start, I have solved the base case:

k = 0 & tr = Lf

sizeI Lf 0 = 0+size Lf
0 = 0

Then I have tried solving the inductive step, but got stuck:

sizeI tr k = k + size tr
sizeI Br(k,t1,t2) k = k + size Br (k,t1,t2)
size t1 (1+ sizeI t2 k) = k+1+size t1 + size t2
.... STUUUUCK

I would REALLY appreciate ANY help here. If you have any links or tips with induction in general (please don't point me at the evil "Well-founded relation" article on Wikipedia), I would be really happy. Also, if you can help me with this one question...

THANKS! :-)

---

To do well-found induction, first you need to define a well-found relation on trees:

Binary relation c where (t1, k1) c (t,k) if t1 is a subtree of t is a well-found relation.

Second, state your induction hypothesis:

t1 and t2 are subtrees of t, we have:

sizeI t1 k1 = k1 + size t1 (1)
sizeI t2 k2 = k2 + size t2 (2)

We must establish:

sizeI Br(i,t1,t2) k = k + size Br(i,t1,t2)

You have already done the base case.

Induction case:

Notice that:

sizeI Br(i,t1,t2) k
= sizeI t1 (1 + sizeI t2 k) // definition of sizeI
= 1 + sizeI t2 k + size t1 // induction hypothesis (1)
=  1 + k + size t2 + size t1 // induction hypothesis (2)
= k + size Br(i, t1, t2) // definition of size

We completed the proof.