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
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
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)"
enters in a loop after a failure in the linear arithmetic proof procedure
Images showing two (normal) snapshots in Isabelle 2012 and the above
crash in Isabelle2013-RC2 are included together with the correspondent
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and