# [isabelle] arith

`I've come across some strange behavior with the arith proof method in
``Isabelle2007. It is able to prove the following lemma:
`
lemma "[| 0 <= (x::int); x div 2 < f x |] ==> x < f x * 2"

`(Here f is a free variable). However, if I turn x into a parameter of
``the subgoal, then arith fails:
`
lemma "!!x. [| 0 <= (x::int); x div 2 < f x |] ==> x < f x * 2"
On the other hand, if I replace (f x) with z, then it works again:
lemma "!!x. [| 0 <= (x::int); x div 2 < z |] ==> x < z * 2"
Thanks,
-john

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*