[isabelle] Linear Arithmetic Split Limit Exceeded



Dear Isabelle Users,

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.

Any help on this would be greatly appreciated.

Best!


-- 
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Coordenador do Curso de Ciência da Computação
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil

Attachment: isa2012-equiv-auto-ok.PNG
Description: PNG image

Attachment: isa2012-equiv-auto-finished.PNG
Description: PNG image

Attachment: isa2013-RC2--equiv-auto-loop.PNG
Description: PNG image

Attachment: equiv_error.thy
Description: Binary data



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