Re: [isabelle] Problem during goal simplification



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


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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