Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] problem with termination of recursive function...


view this post on Zulip Email Gateway (Aug 22 2022 at 15:50):

From: Christian Sternagel <c.sternagel@gmail.com>
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

view this post on Zulip Email Gateway (Aug 22 2022 at 15:50):

From: Peter Lammich <lammich@in.tum.de>
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.


Last updated: Mar 29 2024 at 12:28 UTC