[isabelle-dev] Linear arithmetic should have refuted the assumptions.

[Peter Lammich]

Hello Tobias (cc list).

Getting the following warning (during sledgehammer), with the message
to please inform Tobias ... here you are.


I cannot reproduce the warning in an isolated example, as sledgehammer
seems to find+reconstruct a different proof there, and no warning is
issued.

--
  Peter

-----------------------------------------------
* all the variables range over real *

Assumptions:
t1 * (1 + f1 / t2) = (1 + f1 / t2) * t1  [t1 * (1 + f1 / t2) = (1 + f1
/ t2) * t1]
¬ 0 ≤ t1 * (1 + f1 / t2) + - 1 * ((1 + f1 / t2) * t1)  [¬ 0 ≤ t1 * (1 +
f1 / t2) + - 1 * ((1 + f1 / t2) * t1)]

Proved:
f1 * t1 / t2 < t1 * f1 / t2  [¬ 0 ≤ t1 * (1 + f1 / t2) + - 1 * ((1 + f1
/ t2) * t1), t1 * (1 + f1 / t2) = (1 + f1 / t2) * t1]
    
 
Linear arithmetic should have refuted the assumptions.
Please inform Tobias Nipkow.