Re: [isabelle] arith



Thank you, that should not be the case, will look into it (at some point).

Tobias

John Matthews schrieb:
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.