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

You might save some effort by using looking at ~~/src/HOL/Library/Nat_Bijection. It defines a suitable function prod_encode and proves that it is bijection in lemma bij_prod_encode.


On 13/02/14 17:14, Manuel Eberl wrote:

I will not prove the entire lemma for you, but I can tell you how to
prove the termination of your function.

Your function requires a non-trivial termination relation, one that
Isabelle's function package cannot find automatically. I suggest a
lexicographic ordering w.r.t. the sum of the two arguments and the
second argument, i.e. in every recursive call, either the sum of the
argument decreases or it stays the same and the second element decreases.

In Isabelle, that can be done like this:

function 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))"
by pat_completeness simp_all
termination by (relation "(λ(a,b). a+b) <*mlex*> measure snd")
(auto intro: wf_mlex mlex_less mlex_leq)

“measure”is a function that takes a measuring function (i.e. 'a => nat)
and turns it into the associated strict ordering relation. <*mlex*> is
an operator that takes a relation and combines it with another measure
to a new lexicographic ordering relation.


On 02/13/2014 04:41 PM, Markus Schmetkamp wrote:
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
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.