[isabelle] Questions about arith

Should I expect the following to be solved by arith? Or presburger? Or some other procedure? Or does the presence of the "f" go beyond what these procedures can handle? Is there an extension to presburger that can handle problems of this form?

lemma "
! (x::num) y z (f::num=>num).
(x < y) & (f x < f y) & (!x::num. z <= x --> (f x = f z)) --> x < z
apply(intro allI impI, elim conjE)
apply(rule ccontr)
apply(frule_tac x=x in spec)
apply(drule_tac x=y in spec)



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