# HG changeset patch
# User paulson
# Date 1071826728 -3600
# Node ID cc0b4bbfbc43ae37eef0684381487cd9933e94e1
# Parent  995212a00a50b1aaa51031712d2fba5df07b4114
minor tweaks

diff -r 995212a00a50 -r cc0b4bbfbc43 src/HOL/Complex/Complex.ML
--- a/src/HOL/Complex/Complex.ML	Fri Dec 19 10:38:39 2003 +0100
+++ b/src/HOL/Complex/Complex.ML	Fri Dec 19 10:38:48 2003 +0100
@@ -823,7 +823,7 @@
 by (res_inst_tac [("z","z")] eq_Abs_complex 1);
 by (asm_simp_tac (simpset() addsimps [complex_mod,complex_cnj,
     complex_mult, CLAIM "0 ^ 2 = (0::real)"]) 1);
-by (simp_tac (simpset() addsimps [realpow_two_eq_mult]) 1);
+by (simp_tac (simpset() addsimps [realpow_two_eq_mult, real_abs_def]) 1);
 qed "complex_mod_mult_cnj";
 
 Goalw [cmod_def] "cmod(Abs_complex(x,y)) ^ 2 = x ^ 2 + y ^ 2";
diff -r 995212a00a50 -r cc0b4bbfbc43 src/HOL/Real/RealOrd.thy
--- a/src/HOL/Real/RealOrd.thy	Fri Dec 19 10:38:39 2003 +0100
+++ b/src/HOL/Real/RealOrd.thy	Fri Dec 19 10:38:48 2003 +0100
@@ -380,6 +380,7 @@
 lemma real_mult_less_mono1: "[| (0::real) < z; x < y |] ==> x*z < y*z"
  by (rule Ring_and_Field.mult_strict_right_mono)
 
+text{*The precondition could be weakened to @{term "0\<le>x"}*}
 lemma real_mult_less_mono:
      "[| u<v;  x<y;  (0::real) < v;  0 < x |] ==> u*x < v* y"
  by (simp add: Ring_and_Field.mult_strict_mono order_less_imp_le)
@@ -395,14 +396,10 @@
   by (force elim: order_less_asym
             simp add: Ring_and_Field.mult_le_cancel_left)
 
+text{*Only two uses?*}
 lemma real_mult_less_mono':
      "[| x < y;  r1 < r2;  (0::real) \<le> r1;  0 \<le> x|] ==> r1 * x < r2 * y"
-apply (subgoal_tac "0<r2")
- prefer 2 apply (blast intro: order_le_less_trans)
-apply (case_tac "x=0")
-apply (auto dest!: order_le_imp_less_or_eq 
-            intro: real_mult_less_mono real_mult_order)
-done
+ by (rule Ring_and_Field.mult_strict_mono')
 
 lemma real_inverse_less_swap:
      "[| 0 < r; r < x |] ==> inverse x < inverse (r::real)"
@@ -443,13 +440,13 @@
   by (rule Ring_and_Field.zero_less_mult_iff) 
 
 lemma real_0_le_mult_iff: "((0::real)\<le>x*y) = (0\<le>x & 0\<le>y | x\<le>0 & y\<le>0)"
-  by (rule zero_le_mult_iff) 
+  by (rule Ring_and_Field.zero_le_mult_iff) 
 
 lemma real_mult_less_0_iff: "(x*y < (0::real)) = (0<x & y<0 | x<0 & 0<y)"
-  by (rule mult_less_0_iff) 
+  by (rule Ring_and_Field.mult_less_0_iff) 
 
 lemma real_mult_le_0_iff: "(x*y \<le> (0::real)) = (0\<le>x & y\<le>0 | x\<le>0 & 0\<le>y)"
-  by (rule mult_le_0_iff) 
+  by (rule Ring_and_Field.mult_le_0_iff) 
 
 subsection{*Hardly Used Theorems to be Deleted*}
 
@@ -728,6 +725,13 @@
 apply (simp add: real_of_nat_Suc add_commute)
 done
 
+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
+
+declare real_mult_self_sum_ge_zero [simp]
 
 ML
 {*
@@ -929,6 +933,7 @@
 
 val real_minus_add_distrib = thm"real_minus_add_distrib";
 val real_add_left_cancel = thm"real_add_left_cancel";
+val real_mult_self_sum_ge_zero = thm "real_mult_self_sum_ge_zero";
 *}
 
 end
diff -r 995212a00a50 -r cc0b4bbfbc43 src/HOL/Real/RealPow.thy
--- a/src/HOL/Real/RealPow.thy	Fri Dec 19 10:38:39 2003 +0100
+++ b/src/HOL/Real/RealPow.thy	Fri Dec 19 10:38:48 2003 +0100
@@ -342,7 +342,7 @@
 done
 declare real_mult_is_one [iff]
 
-lemma real_le_add_half_cancel: "(x + y/2 <= (y::real)) = (x <= y /2)"
+lemma real_le_add_half_cancel: "(x + y/2 \<le> (y::real)) = (x \<le> y /2)"
 apply auto
 done
 declare real_le_add_half_cancel [simp]
@@ -372,7 +372,7 @@
 done
 declare inverse_real_of_nat_gt_zero [simp]
 
-lemma inverse_real_of_nat_ge_zero: "0 <= inverse (real (Suc n))"
+lemma inverse_real_of_nat_ge_zero: "0 \<le> inverse (real (Suc n))"
 apply auto
 done
 declare inverse_real_of_nat_ge_zero [simp]
@@ -401,12 +401,12 @@
 apply (auto simp add: realpow_mult realpow_inverse)
 done
 
-lemma realpow_ge_zero2 [rule_format (no_asm)]: "(0::real) <= r --> 0 <= r ^ n"
+lemma realpow_ge_zero2 [rule_format (no_asm)]: "(0::real) \<le> r --> 0 \<le> r ^ n"
 apply (induct_tac "n")
 apply (auto simp add: real_0_le_mult_iff)
 done
 
-lemma realpow_le2 [rule_format (no_asm)]: "(0::real) <= x & x <= y --> x ^ n <= y ^ n"
+lemma realpow_le2 [rule_format (no_asm)]: "(0::real) \<le> x & x \<le> y --> x ^ n \<le> y ^ n"
 apply (induct_tac "n")
 apply (auto intro!: real_mult_le_mono simp add: realpow_ge_zero2)
 done
@@ -425,25 +425,18 @@
 done
 declare realpow_two_sum_zero_iff [simp]
 
-lemma realpow_two_le_add_order: "(0::real) <= u ^ 2 + v ^ 2"
+lemma realpow_two_le_add_order: "(0::real) \<le> u ^ 2 + v ^ 2"
 apply (rule real_le_add_order)
 apply (auto simp add: numeral_2_eq_2)
 done
 declare realpow_two_le_add_order [simp]
 
-lemma realpow_two_le_add_order2: "(0::real) <= u ^ 2 + v ^ 2 + w ^ 2"
+lemma realpow_two_le_add_order2: "(0::real) \<le> u ^ 2 + v ^ 2 + w ^ 2"
 apply (rule real_le_add_order)+
 apply (auto simp add: numeral_2_eq_2)
 done
 declare realpow_two_le_add_order2 [simp]
 
-lemma real_mult_self_sum_ge_zero: "(0::real) <= x*x + y*y"
-apply (cut_tac u = "x" and v = "y" in realpow_two_le_add_order)
-apply (auto simp add: numeral_2_eq_2)
-done
-declare real_mult_self_sum_ge_zero [simp]
-declare real_mult_self_sum_ge_zero [THEN abs_eqI1, simp]
-
 lemma real_sum_square_gt_zero: "x ~= 0 ==> (0::real) < x * x + y * y"
 apply (cut_tac x = "x" and y = "y" in real_mult_self_sum_ge_zero)
 apply (drule real_le_imp_less_or_eq)
@@ -456,13 +449,13 @@
 apply (erule real_sum_square_gt_zero)
 done
 
-lemma real_minus_mult_self_le: "-(u * u) <= (x * (x::real))"
+lemma real_minus_mult_self_le: "-(u * u) \<le> (x * (x::real))"
 apply (rule_tac j = "0" in real_le_trans)
 apply auto
 done
 declare real_minus_mult_self_le [simp]
 
-lemma realpow_square_minus_le: "-(u ^ 2) <= (x::real) ^ 2"
+lemma realpow_square_minus_le: "-(u ^ 2) \<le> (x::real) ^ 2"
 apply (auto simp add: numeral_2_eq_2)
 done
 declare realpow_square_minus_le [simp]
@@ -494,7 +487,7 @@
 done
 declare lemma_realpow_16 [simp]
 
-lemma zero_le_x_squared: "(0::real) <= x^2"
+lemma zero_le_x_squared: "(0::real) \<le> x^2"
 apply (simp add: numeral_2_eq_2)
 done
 declare zero_le_x_squared [simp]
@@ -588,7 +581,6 @@
 val realpow_two_sum_zero_iff = thm "realpow_two_sum_zero_iff";
 val realpow_two_le_add_order = thm "realpow_two_le_add_order";
 val realpow_two_le_add_order2 = thm "realpow_two_le_add_order2";
-val real_mult_self_sum_ge_zero = thm "real_mult_self_sum_ge_zero";
 val real_sum_square_gt_zero = thm "real_sum_square_gt_zero";
 val real_sum_square_gt_zero2 = thm "real_sum_square_gt_zero2";
 val real_minus_mult_self_le = thm "real_minus_mult_self_le";