[isabelle] Bijection f: nat --> nat x nat
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: [isabelle] Bijection f: nat --> nat x nat
- From: Markus Schmetkamp <m.schmetkamp at gmx.de>
- Date: Thu, 13 Feb 2014 16:41:54 +0100
- In-reply-to: <52C59841.email@example.com>
- References: <52C59841.firstname.lastname@example.org>
- User-agent: Mozilla/5.0 (X11; Linux i686; rv:24.0) Gecko/20100101 Thunderbird/24.0
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and