*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Issue with smt and linear arithmetic*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Sat, 13 Aug 2016 17:19:07 +0200*In-reply-to*: <CAKXUXMwmTGTRa5C-J2_JcEF83mF_22Yd1GUtHBv4eaduVLg=Jg@mail.gmail.com>*References*: <CAKXUXMwmTGTRa5C-J2_JcEF83mF_22Yd1GUtHBv4eaduVLg=Jg@mail.gmail.com>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.10; rv:45.0) Gecko/20100101 Thunderbird/45.2.0

Tobias On 13/08/2016 09:49, Lukas Bulwahn wrote:

Dear Isabelle developers, in my latest Isabelle formalization, I stumbled upon an issue with the linear arithmetic method that the smt method internally uses. I am especially reporting this as this tool asks me to do so with this warning: Linear arithmetic should have refuted the assumptions. Please inform Tobias Nipkow. As it is unclear to me as an user, which tool is to `blame`, I must leave it to you, Jasmin, Sascha and Tobias, to find the details of tool interaction below. The following theory fragment shows the issue I encountered in Isabelle2016 (on Windows 10), but I could not test it on a recent Isabelle developer version yet: â theory Issue imports Transcendental begin text â First, here is the original formulation of the lemma as I encountered the issue. Sledgehammer found the smt proof, but smt then fails. â lemma sin_diff_minus: assumes "0 â x" "x â y" "y â 2 * pi" shows "sin ((x - y) / 2) = - sin ((y - x) / 2)" apply (smt minus_divide_left sin_minus) oops text â In fact, the assumptions are not required for the proof and the issue can be reproduced in a slightly smaller lemma without the use of assumptions. â lemma sin_diff_minus: fixes x y :: real shows "sin ((x - y) / 2) = - sin ((y - x) / 2)" apply (smt minus_divide_left sin_minus) oops text â Fortunately, an alternative proof is quickly found. The lemma is proved with a few simplification steps. â lemma sin_diff_minus: fixes x y :: real shows "sin ((x - y) / 2) = - sin ((y - x) / 2)" by (simp only: sin_minus[symmetric] minus_divide_left minus_diff_eq) end -- Best regards, Lukas

**Attachment:
smime.p7s**

**References**:**[isabelle] Issue with smt and linear arithmetic***From:*Lukas Bulwahn

- Previous by Date: [isabelle] Issue with smt and linear arithmetic
- Next by Date: [isabelle] Question about numerals
- Previous by Thread: [isabelle] Issue with smt and linear arithmetic
- Next by Thread: Re: [isabelle] Issue with smt and linear arithmetic
- Cl-isabelle-users August 2016 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