[isabelle] Termination of function with let-binding on left-nested tuples



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.