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

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

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

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

**Re: [isabelle] Bijection f: nat --> nat x nat***From:*Manuel Eberl

- Previous by Date: Re: [isabelle] Bijection f: nat --> nat x nat
- Next by Date: Re: [isabelle] Want a type of non-negatives for a field, to work like nat/int
- Previous by Thread: Re: [isabelle] Bijection f: nat --> nat x nat
- Next by Thread: [isabelle] Simplifier internal proof failure
- 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