Email Gateway (Dec 20 2022 at 13:52): 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: Jan 04 2025 at 20:18 UTC