--- 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";
--- 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
--- 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";