[isabelle] problem with termination of recursive function with case_prod inside foldl



Dear all,

what is the reason that this function

  fun f :: "'a tree â nat à nat"
    where
      "f (Tree ts) = foldl (Îm t. let (l, k) = m; (u, v) = f t in (u +
l, v + k)) (0, 0) ts"

on the datatype

  datatype 'a tree = Tree "'a tree list"

is automatically proven to be total, while this (almost) equivalent variant

  fun f :: "'a tree â nat à nat"
    where
      "f (Tree ts) = foldl (Î(m, n) t. let (u, v) = f t in (u + m, v +
n)) (0, 0) ts"

is rejected?

There is a fundef_cong installed for case_prod (and "%(x, y). f x y" is
syntax for "case_prod (%x y. f x y)") but it doesn't seem to apply.

cheers

chris







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