[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)
apply(simp)
done

Thanks

Tom





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