# HG changeset patch
# User huffman
# Date 1179123313 -7200
# Node ID b3a5569a81e5fe4c53dbe7b8ce9f5afa08cf9c9b
# Parent  82a799ae757945d4d5437979157d81aa3eecd052
cleaned up

diff -r 82a799ae7579 -r b3a5569a81e5 src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Mon May 14 08:12:38 2007 +0200
+++ b/src/HOL/Real/RealDef.thy	Mon May 14 08:15:13 2007 +0200
@@ -112,13 +112,7 @@
 lemma realrel_in_real [simp]: "realrel``{(x,y)}: Real"
 by (simp add: Real_def realrel_def quotient_def, blast)
 
-
-lemma inj_on_Abs_Real: "inj_on Abs_Real Real"
-apply (rule inj_on_inverseI)
-apply (erule Abs_Real_inverse)
-done
-
-declare inj_on_Abs_Real [THEN inj_on_iff, simp]
+declare Abs_Real_inject [simp]
 declare Abs_Real_inverse [simp]
 
 
@@ -299,11 +293,6 @@
   show "inverse 0 = (0::real)" by (rule INVERSE_ZERO)
 qed
 
-
-(*Pull negations out*)
-declare minus_mult_right [symmetric, simp] 
-        minus_mult_left [symmetric, simp]
-
 lemma real_mult_1_right: "z * (1::real) = z"
   by (rule OrderedGroup.mult_1_right)
 
@@ -602,26 +591,19 @@
 done
 
 lemma real_add_order: "[| 0 < x; 0 < y |] ==> (0::real) < x + y"
-by (drule add_strict_mono [of concl: 0 0], assumption, simp)
+by (rule add_pos_pos)
 
 lemma real_le_add_order: "[| 0 \<le> x; 0 \<le> y |] ==> (0::real) \<le> x + y"
-apply (drule order_le_imp_less_or_eq)+
-apply (auto intro: real_add_order order_less_imp_le)
-done
+by (rule add_nonneg_nonneg)
 
 lemma real_inverse_unique: "x*y = (1::real) ==> y = inverse x"
-apply (case_tac "x \<noteq> 0")
-apply (rule_tac c1 = x in real_mult_left_cancel [THEN iffD1], auto)
-done
+by (rule inverse_unique [symmetric])
 
 lemma real_inverse_gt_one: "[| (0::real) < x; x < 1 |] ==> 1 < inverse x"
-by (auto dest: less_imp_inverse_less)
+by (simp add: one_less_inverse_iff)
 
 lemma real_mult_self_sum_ge_zero: "(0::real) \<le> x*x + y*y"
-proof -
-  have "0 + 0 \<le> x*x + y*y" by (blast intro: add_mono zero_le_square)
-  thus ?thesis by simp
-qed
+by (intro add_nonneg_nonneg zero_le_square)
 
 
 subsection{*Embedding the Integers into the Reals*}
@@ -1017,7 +999,7 @@
 by (simp add: abs_if)
 
 lemma abs_real_of_nat_cancel [simp]: "abs (real x) = real (x::nat)"
-by (simp add: real_of_nat_ge_zero)
+by (rule abs_of_nonneg [OF real_of_nat_ge_zero])
 
 lemma abs_add_one_not_less_self [simp]: "~ abs(x) + (1::real) < x"
 by simp
diff -r 82a799ae7579 -r b3a5569a81e5 src/HOL/Real/RealPow.thy
--- a/src/HOL/Real/RealPow.thy	Mon May 14 08:12:38 2007 +0200
+++ b/src/HOL/Real/RealPow.thy	Mon May 14 08:15:13 2007 +0200
@@ -67,7 +67,7 @@
 by (insert power_decreasing [of 1 "Suc n" r], simp)
 
 lemma realpow_Suc_less_one: "[| 0 < r; r < (1::real) |] ==> r ^ Suc n < 1"
-by (insert power_strict_decreasing [of 0 "Suc n" r], simp)
+by (rule power_Suc_less_one)
 
 lemma realpow_minus_mult [rule_format]:
      "0 < n --> (x::real) ^ (n - 1) * x = x ^ n" 
@@ -115,9 +115,7 @@
 done
 
 lemma zero_le_realpow_abs [simp]: "(0::real) \<le> (abs x)^n"
-apply (induct "n")
-apply (auto simp add: zero_le_mult_iff)
-done
+by (rule zero_le_power_abs)
 
 
 subsection{*Literal Arithmetic Involving Powers, Type @{typ real}*}