*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Bijection f: nat --> nat x nat*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Thu, 13 Feb 2014 17:14:35 +0100*In-reply-to*: <52FCE7C2.80107@gmx.de>*References*: <52C59841.90906@gmx.de> <52FCE7C2.80107@gmx.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.2.0

Hallo, 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. Cheers, Manuel 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 > tuples. > Unfortunately isabelle can't find a termination order. > > Has anyone an idea, to prove this lemma? > > Best wishes > Markus

**Follow-Ups**:**Re: [isabelle] Bijection f: nat --> nat x nat***From:*Andreas Lochbihler

**References**:**[isabelle] Bijection f: nat --> nat x nat***From:*Markus Schmetkamp

- Previous by Date: [isabelle] Bijection f: nat --> nat x nat
- Next by Date: Re: [isabelle] Bijection f: nat --> nat x nat
- Previous by Thread: [isabelle] Bijection f: nat --> nat x nat
- Next by Thread: Re: [isabelle] Bijection f: nat --> nat x nat
- Cl-isabelle-users February 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list