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.