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

```Hi.

The congruence rules for case_prod do not work with the higher-order
term that %(_,_) _ translates to.

Try, e.g.,
Â lemma [fundef_cong]:
ÂÂÂÂassumes "(case m of (a,b) â t a b c) = (case m' of (a,b) â t' a b
c')"
ÂÂÂÂshows "case_prod (Îa b c. t a b c) m c = case_prod (Îa b c. t' a b
c) m' c'"ÂÂ
ÂÂÂÂusing assms by (auto split: prod.split) Â

to convert the higher-order term inside the case expression to a first-
order term, on which the cong-rule for case_prod will work.

--
Â Peter

On Mi, 2017-08-09 at 14:43 +0200, Christian Sternagel wrote:
> 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.