Re: [isabelle] Problem during goal simplification



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
>>
>>
>



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