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"
This archive was generated by a fusion of
Pipermail (Mailman edition) and