*To*: Mathieu Giorgino <mathieu.giorgino at IRIT.FR>*Subject*: Re: [isabelle] Termination of function with let-binding on left-nested tuples*From*: Alexander Krauss <krauss at in.tum.de>*Date*: Sat, 30 Jul 2011 22:19:01 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <1375594.JkJhBao4WR@leh>*References*: <1375594.JkJhBao4WR@leh>*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.9.1.16) Gecko/20101227 Icedove/3.0.11

Hi Matthieu,

function (sequential) f2 :: "((nat * nat) * nat) \<Rightarrow> unit" where "f2 ((_, _), 0) = ()" | "f2 n = (let ((a1, a2), a3) = n in f2 ((a2+2,a1+1), a3 - 1))" by pat_completeness auto

[...]

Then it seems impossible to prove the termination of f2 (and "fun f2'" fails). In the termination proof, we can see there is no equality relation for the second component of the outermost pair. It seems to be related to congruence rules in some way but I couldn't figure out the exact problem.

Here is a different instance of the same problem, which is a bit clearer: function f3 :: "bool => nat => nat" where "f3 _ 0 = 0" | "f3 b (Suc n) = (case b of True => f3 True | False => id) n"

Alex

**References**:**[isabelle] Termination of function with let-binding on left-nested tuples***From:*Mathieu Giorgino

- Previous by Date: Re: [isabelle] the state of the lattice theories
- Next by Date: Re: [isabelle] lattice syntax problems (OR: what does it mean to merge two theories?)
- Previous by Thread: Re: [isabelle] Termination of function with let-binding on left-nested tuples
- Cl-isabelle-users July 2011 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