*To*: Tobias Nipkow <nipkow at in.tum.de>*Subject*: Re: [isabelle] Problem during goal simplification*From*: Omar MontaÃo Rivas <omar.montano at upslp.edu.mx>*Date*: Thu, 21 Apr 2016 18:09:44 -0500*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <57193E46.20502@in.tum.de>*References*: <CADnpnWRvtCO_3yO=xtjOc8_7KNRe2V_gMiP9Cw_AAaufabNQMw@mail.gmail.com> <57193E46.20502@in.tum.de>*Sender*: omarmrivas at gmail.com

Thanks! Good to know how to control if splits during simplification. Omar. 2016-04-21 15:55 GMT-05:00 Tobias Nipkow <nipkow at in.tum.de>: > Frankly, it is hard to say. Maybe the if-splits created some premises that > constitute a nonterminating set of equations? That's heuristic proof > automation for you. > > The following proof script simplifies the goal completely. Although the > resulting goal is unenlightening (for me), the script may be of use: > > 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 > > This does the job. A second call to simp (which is not influenced by that > "using") fails, showing that the result is fully simplified. > > 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 >> >> >

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

**Re: [isabelle] Problem during goal simplification***From:*Tobias Nipkow

- Previous by Date: [isabelle] ML goes "incommunicado" for minutes at a time during sledgehammering
- Next by Date: [isabelle] HOFM @ STAF / SEFM 2016: call for papers
- Previous by Thread: Re: [isabelle] Problem during goal simplification
- Next by Thread: [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