Email Gateway (Aug 19 2022 at 17:20): Email Gateway (Aug 19 2022 at 17:20):From: Mathias Fleury <mathias.fleury12@gmail.com>
Hello List,
I have defined an recursive function over sets (either the set is infinite or empty, or I take the minimum of the set), but it leads to non-termination of simp, when applied to an expression containing the function (see full theory attached):
function f :: "'v :: linorder set => 'v list" where
"f vars =
(if ~finite vars \<or> vars = {} then []
else f (vars - {Min vars}))"
by auto
termination by (relation "measure card") (simp_all add: card_gt_0_iff)
lemma
shows "[] = f s"
(this simp-call is not terminating)
apply simp
Given the simplifier trace, I think that simp is doing a case distinction whether the set is empty or not, meaning that it then tries to simplify the recursive call of the function, where the same occurs: case distinction and recursive call of simp. Is there a way to avoid this non-termination?
Many thanks in advance,
Mathias Fleury
Simp_blocking.thy
Email Gateway (Aug 19 2022 at 17:20):From: Peter Lammich <lammich@in.tum.de>
The simplifier will "split" on if's by default, thus
inlining your function again and again.
A standard way around this (also documented in the function tutorial) is
to make the simp-rules conditional, i.e.
~finite | vars ={} ==> f x = []
finite; vars~={} ==> f x = f (vars - ...)
Last updated: Apr 16 2024 at 08:18 UTC