Email Gateway (Aug 22 2022 at 15:50): 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
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: Nov 21 2024 at 12:39 UTC