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.