--- a/src/HOL/Import/HOL/real.imp Sun May 09 09:39:01 2010 -0700
+++ b/src/HOL/Import/HOL/real.imp Sun May 09 14:21:44 2010 -0700
@@ -247,7 +247,7 @@
"REAL_INV_POS" > "Rings.positive_imp_inverse_positive"
"REAL_INV_NZ" > "Rings.nonzero_imp_inverse_nonzero"
"REAL_INV_MUL" > "HOL4Real.real.REAL_INV_MUL"
- "REAL_INV_LT1" > "RealDef.real_inverse_gt_one"
+ "REAL_INV_LT1" > "Fields.one_less_inverse"
"REAL_INV_INV" > "Rings.inverse_inverse_eq"
"REAL_INV_EQ_0" > "Rings.inverse_nonzero_iff_nonzero"
"REAL_INV_1OVER" > "Rings.inverse_eq_divide"
--- a/src/HOL/RealDef.thy Sun May 09 09:39:01 2010 -0700
+++ b/src/HOL/RealDef.thy Sun May 09 14:21:44 2010 -0700
@@ -506,26 +506,24 @@
subsection{*More Lemmas*}
+text {* BH: These lemmas should not be necessary; they should be
+covered by existing simp rules and simplification procedures. *}
+
lemma real_mult_left_cancel: "(c::real) \<noteq> 0 ==> (c*a=c*b) = (a=b)"
-by auto
+by simp (* redundant with mult_cancel_left *)
lemma real_mult_right_cancel: "(c::real) \<noteq> 0 ==> (a*c=b*c) = (a=b)"
-by auto
+by simp (* redundant with mult_cancel_right *)
lemma real_mult_less_iff1 [simp]: "(0::real) < z ==> (x*z < y*z) = (x < y)"
- by (force elim: order_less_asym
- simp add: mult_less_cancel_right)
+by simp (* solved by linordered_ring_less_cancel_factor simproc *)
lemma real_mult_le_cancel_iff1 [simp]: "(0::real) < z ==> (x*z \<le> y*z) = (x\<le>y)"
-apply (simp add: mult_le_cancel_right)
-apply (blast intro: elim: order_less_asym)
-done
+by simp (* solved by linordered_ring_le_cancel_factor simproc *)
lemma real_mult_le_cancel_iff2 [simp]: "(0::real) < z ==> (z*x \<le> z*y) = (x\<le>y)"
-by(simp add:mult_commute)
-
-lemma real_inverse_gt_one: "[| (0::real) < x; x < 1 |] ==> 1 < inverse x"
-by (simp add: one_less_inverse_iff) (* TODO: generalize/move *)
+by (rule mult_le_cancel_left_pos)
+(* BH: Why doesn't "simp" prove this one, like it does the last one? *)
subsection {* Embedding numbers into the Reals *}
@@ -773,10 +771,6 @@
lemma not_real_of_nat_less_zero [simp]: "~ real (n::nat) < 0"
by (simp add: add: real_of_nat_def)
-(* FIXME: duplicates real_of_nat_ge_zero *)
-lemma real_of_nat_ge_zero_cancel_iff: "(0 \<le> real (n::nat))"
-by (simp add: add: real_of_nat_def)
-
lemma nat_less_real_le: "((n::nat) < m) = (real n + 1 <= real m)"
apply (subgoal_tac "real n + 1 = real (Suc n)")
apply simp
@@ -1013,12 +1007,6 @@
by auto
-(*
-FIXME: we should have this, as for type int, but many proofs would break.
-It replaces x+-y by x-y.
-declare real_diff_def [symmetric, simp]
-*)
-
subsubsection{*Density of the Reals*}
lemma real_lbound_gt_zero:
--- a/src/HOL/SEQ.thy Sun May 09 09:39:01 2010 -0700
+++ b/src/HOL/SEQ.thy Sun May 09 14:21:44 2010 -0700
@@ -1289,7 +1289,7 @@
hence x0: "0 < x" by simp
assume x1: "x < 1"
from x0 x1 have "1 < inverse x"
- by (rule real_inverse_gt_one)
+ by (rule one_less_inverse)
hence "(\<lambda>n. inverse (inverse x ^ n)) ----> 0"
by (rule LIMSEQ_inverse_realpow_zero)
thus ?thesis by (simp add: power_inverse)
--- a/src/HOL/Transcendental.thy Sun May 09 09:39:01 2010 -0700
+++ b/src/HOL/Transcendental.thy Sun May 09 14:21:44 2010 -0700
@@ -1089,7 +1089,7 @@
apply (rule_tac x = 1 and y = y in linorder_cases)
apply (drule order_less_imp_le [THEN lemma_exp_total])
apply (rule_tac [2] x = 0 in exI)
-apply (frule_tac [3] real_inverse_gt_one)
+apply (frule_tac [3] one_less_inverse)
apply (drule_tac [4] order_less_imp_le [THEN lemma_exp_total], auto)
apply (rule_tac x = "-x" in exI)
apply (simp add: exp_minus)