*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Linear Arithmetic Split Limit Exceeded*From*: Alfio Martini <alfio.martini at acm.org>*Date*: Tue, 5 Feb 2013 10:49:57 -0200*Sender*: alfio.martini at gmail.com

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

**Attachment:
isa2012-equiv-auto-finished.PNG**

**Attachment:
isa2013-RC2--equiv-auto-loop.PNG**

**Attachment:
equiv_error.thy**

**Follow-Ups**:**Re: [isabelle] Linear Arithmetic Split Limit Exceeded***From:*Makarius

- Previous by Date: Re: [isabelle] Where to learn about HOL vs FOL?
- Next by Date: [isabelle] PostDoc position on certifying Network Calculus computations within Isabelle
- Previous by Thread: Re: [isabelle] A way to write nested theories in a theory file?
- Next by Thread: Re: [isabelle] Linear Arithmetic Split Limit Exceeded
- Cl-isabelle-users February 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list