*To*: Alfio Martini <alfio.martini at acm.org>*Subject*: Re: [isabelle] Linear Arithmetic Split Limit Exceeded*From*: Makarius <makarius at sketis.net>*Date*: Thu, 7 Feb 2013 14:31:24 +0100 (CET)*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <CAAPnxw0uTzaLgEqj99ap8YNDyZiJxwWkgkEwK+81JsrTaUFxyA@mail.gmail.com>*References*: <CAAPnxw0uTzaLgEqj99ap8YNDyZiJxwWkgkEwK+81JsrTaUFxyA@mail.gmail.com>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

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.

Makarius

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

**References**:**[isabelle] Linear Arithmetic Split Limit Exceeded***From:*Alfio Martini

- Previous by Date: Re: [isabelle] Where to learn about the Mini-Haskell of the code generator?
- Next by Date: Re: [isabelle] Isabelle2013-RC3 available for testing
- Previous by Thread: [isabelle] Linear Arithmetic Split Limit Exceeded
- 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