Why won't the 'linordered_field_class.frac_le' rule work? (Isabelle)

Question

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.

Answer 1

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.