Q:

Converting free variables to bound variables

I want to prove the following lemma
lemma assumes "f (w+n) - f w / n ≤ g (w+n)" 
shows "∀n. (f (w+n) - f w) / n ≤ g (w+n)"

I assumed this would be very simple however it is proving trickier than I first thought. From my thoughts, the inequality in the assumption is valid for all w and n, therefore the result I am trying to prove should also be valid.
I've searched the documentation and ran sledgehammer however I haven't been successful.
Can this be solved or am I trying to prove completely different statements? If so, please could someone explain why. 

A:

As the previous answer already stated, your proposition does not hold. Type classes, however, do not have anything to do with it; it is a very fundamental logical problem.
First of all, it should be noted that your assumption was probably supposed to be
(f (w+n) - f w) / n ≤ g (w+n)

The way you wrote it down, it means
f (w+n) - (f w / n) ≤ g (w+n)

But even when you fix that, it still does not hold, and the reason for that lies in what free variables mean. The convention in Isabelle is that free variables (that are not bound anywhere in the context) in a lemma are implicitly universally qualified. This is usually the convention in mathematics; we write a + b = b + a, not ∀a b. a + b = b + a.
Your lemma therefore means this to Isabelle:
∀f g w n. (f (w+n) - f w) / n ≤ g (w+n) ⟹ ∀n. (f (w+n) - f w) / n ≤ g (w+n)

Informally, what this says is that if the proposition holds for one n, it must hold for all n. This is obviously false. My guess is that you were confused by the fact that when you write down
lemma "(f (w+n) - f w) / n ≤ g (w+n)"

then that already means that it holds for all n (due to the same convention). But when you just take that and past it into the assumption of another lemma, the same convention leads to the opposite meaning: "for any n, if the assumption holds, then ...".
If you really want to state the assumption in such a way that it holds for all n, you have to write
lemma assumes "⋀n. (f (w+n) - f w) / n ≤ g (w+n)" 
      shows   "∀n. (f (w+n) - f w) / n ≤ g (w+n)"

Then the proof is just one application of the rule allI and can be done automatically with blast or auto. Note that ⋀ is Isabelle's universal qualifier in the meta logic. Its meaning is similar to when, in mathematics, you say "Fix some n." or "Let n be a fixed, but arbitrary number".

