[isabelle] Bijection f: nat --> nat x nat

Hi people,

I want to prove this lemma:

lemma bijection: "?f::(nat × nat => nat). bij f"

My idea was to define a function like this:

fun f :: "nat × nat => nat" where
  "f (0,0) = 0" |
  "f (n, Suc m) = Suc (f (Suc n, m))" |
  "f (Suc n, 0) = Suc (f (0, n))"

This function should go along each diagonal in nat x nat counting the tuples.
Unfortunately isabelle can't find a termination order.

Has anyone an idea, to prove this lemma?

Best wishes

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