Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Linear arithmetic should have refuted the assu...


view this post on Zulip Email Gateway (Dec 20 2022 at 13:52):

From: Matthias Sleurink <matthias.sleurink@gmail.com>
Dear List,

I found this error message whilst working on homework. I've made a small
reproduction:

theory ErrorReport
imports Main "HOL.Transcendental"
begin
lemma
fixes m n :: nat
assumes A: "4 / 5 = m⇧2 / n⇧2"
shows "5 = m⇧2 / n⇧2 / 4" using A try0
oops
This is the error with the context in the output window:
Assumptions:
(real m)⇧2 * 5 / (real n)⇧2 = 4
(real m)⇧2 / ((real n)⇧2 * 4) = 5 [(real m)⇧2 / ((real n)⇧2 * 4) = 5]

Proved:
96 + a__ * 5 / b__ = 5 * a__ / b__ [a__ / (b__ * 4) = 5, a__ * 5 / b__ = 4]

Linear arithmetic should have refuted the assumptions.
Please inform Tobias Nipkow.

This exact error is repeated 8 times in the output window before "No proof
found" is printed.
For context, I am using Isabelle2022 on Pop os 22.04.

Hope this is enough information,
Matthias Sleurink


Last updated: Mar 29 2024 at 08:18 UTC