Re: [isabelle] Linear Arithmetic Split Limit Exceeded



On Tue, 5 Feb 2013, Alfio Martini wrote:

In trying to understand a bit the theory "Equiv_Relations.thy" I started to
prove
some (apparently) simple lemmas.

So I defined some equivalence relations on natural numbers using the
remainder operator and proved
some lemmas relating equivalence relations with  its equivalence classes
(partitions).

An unexpected problem occurs in the (experimental, exploratory) proof of
lemma partition_EqR05 (the
last lemma in the theory file).
The proof goes through in Isabelle 2012, but after "apply (auto)"
Isabelle2013-RC2
enters in a loop after a failure  in the linear arithmetic proof procedure
(apparently).

Images showing two (normal) snapshots in Isabelle 2012 and the above
mentioned
crash in Isabelle2013-RC2 are included together with the correspondent
theory file.

The only difference I can see between Isabelle2012 and Isabelle2013-RC2 is that in Isabelle2012 you need to tick "Tracing" in the Output panel to see the very same "linarith_split_limit exceeded (current value is 9)". In both versions the proofs works, but takes very long.

Someone else who understands the "lin_arith" solver needs to explain how to switch it off, or how to do these proofs about "mod" in a better way.


	Makarius





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