[isabelle] Proving lemmas containing a squareroot



Hi

I'm hoping some of you could help me with the following lemma:

consts
pl :: "real => real"

axioms
gt: "EX x y. pl x > pl y"

lemma rt4: "ALL a b. sqrt(4) / pl a > sqrt(4) / pl b"
using gt
sledgehammer;

It seems like a rather simple lemma but sledgehammer (E, SPASS, and
Vampire) can't seem to return the set of theorems for metis. Does
anyone know how to prove it?

Moreover, if I simplify the lemma by removing the sqrt to:

lemma rt4: "ALL a b. (4) / pl a > (4) / pl b"
using gt
sledgehammer;

Vampire gives me a minimal set of 14 theorems for metis:

apply (metis comm_monoid_add.mult_commute comp_arith(112)
divide_inverse eq_diff_eq' eq_number_of inverse_inverse_eq
linorder_neqE_ordered_idom monoid_add_class.add_0_right
mult.diff_right mult.zero_left real_less_def real_mult_right_cancel
rel_simps(38) rel_simps(46))

However, metis actually will not terminate. Assuming those 14 theorems
are the required theorems, why is having sqrt so difficult for
sledgehammer?

Thanks!

Michael





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