*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Termination of function with let-binding on left-nested tuples*From*: Mathieu Giorgino <mathieu.giorgino at IRIT.FR>*Date*: Fri, 29 Jul 2011 16:45:29 +0200*Organization*: IRIT*User-agent*: KMail/4.6.1 (Linux/2.6.39-ARCH; KDE/4.6.5; x86_64; ; )

Hi all, I just noticed a problem with "let" bindings on left-nested tuples in function definitions. For example, these 2 functions -- each written with "function" and "fun" -- are exactly the same, excepted for the nesting of tuples. ----------- theory Scratch imports Main begin function (sequential) f1 :: "(nat * nat * nat) \<Rightarrow> unit" where "f1 (_, _, 0) = ()" | "f1 n = (let (a1, a2, a3) = n in f1 (a2+2, a1+1, a3 - 1))" by pat_completeness auto termination apply (relation "measure (snd o snd)") apply (auto simp del:in_measure) by auto fun f1' :: "(nat * nat * nat) \<Rightarrow> unit" where "f1' (_, _, 0) = ()" | "f1' n = (let (a1, a2, a3) = n in f1' (a2+2, a1+1, a3 - 1))" 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 termination apply (relation "measure snd") apply (auto simp del:in_measures) oops fun f2' :: "((nat * nat) * nat) \<Rightarrow> unit" where "f2' ((_, _), 0) = ()" | "f2' n = (let ((a1, a2), a3) = n in f2' ((a2+2, a1+1), a3 - 1))" ----------- 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. In these examples, the let could be replaced by the function pattern matching but this problem also prevents those let-bindings in more complicated functions. An idea on what is going wrong ? Thanks, Mathieu

**Follow-Ups**:**Re: [isabelle] Termination of function with let-binding on left-nested tuples***From:*Brian Huffman

**Re: [isabelle] Termination of function with let-binding on left-nested tuples***From:*Alexander Krauss

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