[isabelle] Proving lemmas containing a squareroot
I'm hoping some of you could help me with the following lemma:
pl :: "real => real"
gt: "EX x y. pl x > pl y"
lemma rt4: "ALL a b. sqrt(4) / pl a > sqrt(4) / pl b"
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"
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
mult.diff_right mult.zero_left real_less_def real_mult_right_cancel
However, metis actually will not terminate. Assuming those 14 theorems
are the required theorems, why is having sqrt so difficult for
This archive was generated by a fusion of
Pipermail (Mailman edition) and