# Re: [isabelle] Non-termination of simp

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 - ...)
--
Peter
On Fr, 2015-03-13 at 09:21 +0100, Mathias Fleury wrote:
> 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
>

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*