*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Problem during goal simplification*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Thu, 21 Apr 2016 22:55:34 +0200*In-reply-to*: <CADnpnWRvtCO_3yO=xtjOc8_7KNRe2V_gMiP9Cw_AAaufabNQMw@mail.gmail.com>*References*: <CADnpnWRvtCO_3yO=xtjOc8_7KNRe2V_gMiP9Cw_AAaufabNQMw@mail.gmail.com>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.10; rv:38.0) Gecko/20100101 Thunderbird/38.7.2

apply(split if_split) apply(split if_split) apply (simp split del: if_split) apply(split if_split) apply (simp split del: if_split) apply(split if_split) apply (simp split del: if_split) Here is another gadget for tweaking the simplifier: using [[simp_depth_limit = 3]] apply simp

Tobias On 21/04/2016 21:38, Omar MontaÃo Rivas wrote:

Hi, Does anyone know why the following goal loops after simplification (simp)? Is there a way to avoid non-termination, e.g. by eliminating a rewrite rule or a congruence rule from the simpset? I have tried changing the value of linarith_split_limit but with no success. Thanks, Omar. declare [[linarith_split_limit = 0]] lemma "âf g. â(x::nat) y. f x y = (if 0 = y then if y = 0 then f 0 y else if 0 - 1 - 1 = y then y else y else y) â g x y = (if y - 1 - 1 = (if y - 1 - 1 = (if 0 = y - 1 then y - 1 else (if y = (if y - 1 = y - 1 then y - 1 else y - 1) - 1 - 1 - 1 then y else y) - 1) - 1 - 1 - 1 then if y = (if y = y - 1 - 1 then y - 1 else y) - 1 - 1 - 1 then y else y else y - 1) - 1 - 1 then x else y)" using [[simp_trace]] apply simp

**Attachment:
smime.p7s**

**Follow-Ups**:**Re: [isabelle] Problem during goal simplification***From:*Omar MontaÃo Rivas

**References**:**[isabelle] Problem during goal simplification***From:*Omar MontaÃo Rivas

- Previous by Date: [isabelle] Problem during goal simplification
- Next by Date: [isabelle] ML goes "incommunicado" for minutes at a time during sledgehammering
- Previous by Thread: [isabelle] Problem during goal simplification
- Next by Thread: Re: [isabelle] Problem during goal simplification
- Cl-isabelle-users April 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list