I am trying to use the rule linordered_field_class.frac_le in an Isar proof. Here is the code snippet (it may depend on the previous parts of the proof, but that is unlikely). n is of type nat.
...
then have 4:"2 ≤ (2^(n+1)::real)" by simp
have 1:"(0::real)≤(1::real)" by simp
have 2: "1≤(1::real)" by simp
have 3:"(0::real)≤(2::real)" by simp
from 1 2 3 4 have "1/(2^(n+1))≤1/(2::real)" by (rule linordered_field_class.frac_le)
I think I have applied the rule correctly, but it complains 'Failed to finish proof'. I thought it might be a type error, hence the overkill with :: real, but I couldn't fix it. Does anyone know what might be the problem, and how to fix it? Or just an alternative way to prove that sort of statement.
If you look at the rule frac_le, the third premise is of the form 0 < ?w, but the fact that you chain in in the third position is 0 ≤ 2. If you replace that with 0 < 2, it works fine.
Note that you can save a lot of these tedious manual steps by just writing auto intro: frac_le or even simp add: divide_simps or simp add: field_simps. Algebraic reasoning in Isabelle tends to be very tedious unless you make good use of the existing automation.