minor tweaks
authorpaulson
Fri Dec 19 10:38:48 2003 +0100 (2003-12-19)
changeset 14304cc0b4bbfbc43
parent 14303 995212a00a50
child 14305 f17ca9f6dc8c
minor tweaks
src/HOL/Complex/Complex.ML
src/HOL/Real/RealOrd.thy
src/HOL/Real/RealPow.thy
     1.1 --- a/src/HOL/Complex/Complex.ML	Fri Dec 19 10:38:39 2003 +0100
     1.2 +++ b/src/HOL/Complex/Complex.ML	Fri Dec 19 10:38:48 2003 +0100
     1.3 @@ -823,7 +823,7 @@
     1.4  by (res_inst_tac [("z","z")] eq_Abs_complex 1);
     1.5  by (asm_simp_tac (simpset() addsimps [complex_mod,complex_cnj,
     1.6      complex_mult, CLAIM "0 ^ 2 = (0::real)"]) 1);
     1.7 -by (simp_tac (simpset() addsimps [realpow_two_eq_mult]) 1);
     1.8 +by (simp_tac (simpset() addsimps [realpow_two_eq_mult, real_abs_def]) 1);
     1.9  qed "complex_mod_mult_cnj";
    1.10  
    1.11  Goalw [cmod_def] "cmod(Abs_complex(x,y)) ^ 2 = x ^ 2 + y ^ 2";
     2.1 --- a/src/HOL/Real/RealOrd.thy	Fri Dec 19 10:38:39 2003 +0100
     2.2 +++ b/src/HOL/Real/RealOrd.thy	Fri Dec 19 10:38:48 2003 +0100
     2.3 @@ -380,6 +380,7 @@
     2.4  lemma real_mult_less_mono1: "[| (0::real) < z; x < y |] ==> x*z < y*z"
     2.5   by (rule Ring_and_Field.mult_strict_right_mono)
     2.6  
     2.7 +text{*The precondition could be weakened to @{term "0\<le>x"}*}
     2.8  lemma real_mult_less_mono:
     2.9       "[| u<v;  x<y;  (0::real) < v;  0 < x |] ==> u*x < v* y"
    2.10   by (simp add: Ring_and_Field.mult_strict_mono order_less_imp_le)
    2.11 @@ -395,14 +396,10 @@
    2.12    by (force elim: order_less_asym
    2.13              simp add: Ring_and_Field.mult_le_cancel_left)
    2.14  
    2.15 +text{*Only two uses?*}
    2.16  lemma real_mult_less_mono':
    2.17       "[| x < y;  r1 < r2;  (0::real) \<le> r1;  0 \<le> x|] ==> r1 * x < r2 * y"
    2.18 -apply (subgoal_tac "0<r2")
    2.19 - prefer 2 apply (blast intro: order_le_less_trans)
    2.20 -apply (case_tac "x=0")
    2.21 -apply (auto dest!: order_le_imp_less_or_eq 
    2.22 -            intro: real_mult_less_mono real_mult_order)
    2.23 -done
    2.24 + by (rule Ring_and_Field.mult_strict_mono')
    2.25  
    2.26  lemma real_inverse_less_swap:
    2.27       "[| 0 < r; r < x |] ==> inverse x < inverse (r::real)"
    2.28 @@ -443,13 +440,13 @@
    2.29    by (rule Ring_and_Field.zero_less_mult_iff) 
    2.30  
    2.31  lemma real_0_le_mult_iff: "((0::real)\<le>x*y) = (0\<le>x & 0\<le>y | x\<le>0 & y\<le>0)"
    2.32 -  by (rule zero_le_mult_iff) 
    2.33 +  by (rule Ring_and_Field.zero_le_mult_iff) 
    2.34  
    2.35  lemma real_mult_less_0_iff: "(x*y < (0::real)) = (0<x & y<0 | x<0 & 0<y)"
    2.36 -  by (rule mult_less_0_iff) 
    2.37 +  by (rule Ring_and_Field.mult_less_0_iff) 
    2.38  
    2.39  lemma real_mult_le_0_iff: "(x*y \<le> (0::real)) = (0\<le>x & y\<le>0 | x\<le>0 & 0\<le>y)"
    2.40 -  by (rule mult_le_0_iff) 
    2.41 +  by (rule Ring_and_Field.mult_le_0_iff) 
    2.42  
    2.43  subsection{*Hardly Used Theorems to be Deleted*}
    2.44  
    2.45 @@ -728,6 +725,13 @@
    2.46  apply (simp add: real_of_nat_Suc add_commute)
    2.47  done
    2.48  
    2.49 +lemma real_mult_self_sum_ge_zero: "(0::real) \<le> x*x + y*y"
    2.50 +proof -
    2.51 +  have "0 + 0 \<le> x*x + y*y" by (blast intro: add_mono zero_le_square)
    2.52 +  thus ?thesis by simp
    2.53 +qed
    2.54 +
    2.55 +declare real_mult_self_sum_ge_zero [simp]
    2.56  
    2.57  ML
    2.58  {*
    2.59 @@ -929,6 +933,7 @@
    2.60  
    2.61  val real_minus_add_distrib = thm"real_minus_add_distrib";
    2.62  val real_add_left_cancel = thm"real_add_left_cancel";
    2.63 +val real_mult_self_sum_ge_zero = thm "real_mult_self_sum_ge_zero";
    2.64  *}
    2.65  
    2.66  end
     3.1 --- a/src/HOL/Real/RealPow.thy	Fri Dec 19 10:38:39 2003 +0100
     3.2 +++ b/src/HOL/Real/RealPow.thy	Fri Dec 19 10:38:48 2003 +0100
     3.3 @@ -342,7 +342,7 @@
     3.4  done
     3.5  declare real_mult_is_one [iff]
     3.6  
     3.7 -lemma real_le_add_half_cancel: "(x + y/2 <= (y::real)) = (x <= y /2)"
     3.8 +lemma real_le_add_half_cancel: "(x + y/2 \<le> (y::real)) = (x \<le> y /2)"
     3.9  apply auto
    3.10  done
    3.11  declare real_le_add_half_cancel [simp]
    3.12 @@ -372,7 +372,7 @@
    3.13  done
    3.14  declare inverse_real_of_nat_gt_zero [simp]
    3.15  
    3.16 -lemma inverse_real_of_nat_ge_zero: "0 <= inverse (real (Suc n))"
    3.17 +lemma inverse_real_of_nat_ge_zero: "0 \<le> inverse (real (Suc n))"
    3.18  apply auto
    3.19  done
    3.20  declare inverse_real_of_nat_ge_zero [simp]
    3.21 @@ -401,12 +401,12 @@
    3.22  apply (auto simp add: realpow_mult realpow_inverse)
    3.23  done
    3.24  
    3.25 -lemma realpow_ge_zero2 [rule_format (no_asm)]: "(0::real) <= r --> 0 <= r ^ n"
    3.26 +lemma realpow_ge_zero2 [rule_format (no_asm)]: "(0::real) \<le> r --> 0 \<le> r ^ n"
    3.27  apply (induct_tac "n")
    3.28  apply (auto simp add: real_0_le_mult_iff)
    3.29  done
    3.30  
    3.31 -lemma realpow_le2 [rule_format (no_asm)]: "(0::real) <= x & x <= y --> x ^ n <= y ^ n"
    3.32 +lemma realpow_le2 [rule_format (no_asm)]: "(0::real) \<le> x & x \<le> y --> x ^ n \<le> y ^ n"
    3.33  apply (induct_tac "n")
    3.34  apply (auto intro!: real_mult_le_mono simp add: realpow_ge_zero2)
    3.35  done
    3.36 @@ -425,25 +425,18 @@
    3.37  done
    3.38  declare realpow_two_sum_zero_iff [simp]
    3.39  
    3.40 -lemma realpow_two_le_add_order: "(0::real) <= u ^ 2 + v ^ 2"
    3.41 +lemma realpow_two_le_add_order: "(0::real) \<le> u ^ 2 + v ^ 2"
    3.42  apply (rule real_le_add_order)
    3.43  apply (auto simp add: numeral_2_eq_2)
    3.44  done
    3.45  declare realpow_two_le_add_order [simp]
    3.46  
    3.47 -lemma realpow_two_le_add_order2: "(0::real) <= u ^ 2 + v ^ 2 + w ^ 2"
    3.48 +lemma realpow_two_le_add_order2: "(0::real) \<le> u ^ 2 + v ^ 2 + w ^ 2"
    3.49  apply (rule real_le_add_order)+
    3.50  apply (auto simp add: numeral_2_eq_2)
    3.51  done
    3.52  declare realpow_two_le_add_order2 [simp]
    3.53  
    3.54 -lemma real_mult_self_sum_ge_zero: "(0::real) <= x*x + y*y"
    3.55 -apply (cut_tac u = "x" and v = "y" in realpow_two_le_add_order)
    3.56 -apply (auto simp add: numeral_2_eq_2)
    3.57 -done
    3.58 -declare real_mult_self_sum_ge_zero [simp]
    3.59 -declare real_mult_self_sum_ge_zero [THEN abs_eqI1, simp]
    3.60 -
    3.61  lemma real_sum_square_gt_zero: "x ~= 0 ==> (0::real) < x * x + y * y"
    3.62  apply (cut_tac x = "x" and y = "y" in real_mult_self_sum_ge_zero)
    3.63  apply (drule real_le_imp_less_or_eq)
    3.64 @@ -456,13 +449,13 @@
    3.65  apply (erule real_sum_square_gt_zero)
    3.66  done
    3.67  
    3.68 -lemma real_minus_mult_self_le: "-(u * u) <= (x * (x::real))"
    3.69 +lemma real_minus_mult_self_le: "-(u * u) \<le> (x * (x::real))"
    3.70  apply (rule_tac j = "0" in real_le_trans)
    3.71  apply auto
    3.72  done
    3.73  declare real_minus_mult_self_le [simp]
    3.74  
    3.75 -lemma realpow_square_minus_le: "-(u ^ 2) <= (x::real) ^ 2"
    3.76 +lemma realpow_square_minus_le: "-(u ^ 2) \<le> (x::real) ^ 2"
    3.77  apply (auto simp add: numeral_2_eq_2)
    3.78  done
    3.79  declare realpow_square_minus_le [simp]
    3.80 @@ -494,7 +487,7 @@
    3.81  done
    3.82  declare lemma_realpow_16 [simp]
    3.83  
    3.84 -lemma zero_le_x_squared: "(0::real) <= x^2"
    3.85 +lemma zero_le_x_squared: "(0::real) \<le> x^2"
    3.86  apply (simp add: numeral_2_eq_2)
    3.87  done
    3.88  declare zero_le_x_squared [simp]
    3.89 @@ -588,7 +581,6 @@
    3.90  val realpow_two_sum_zero_iff = thm "realpow_two_sum_zero_iff";
    3.91  val realpow_two_le_add_order = thm "realpow_two_le_add_order";
    3.92  val realpow_two_le_add_order2 = thm "realpow_two_le_add_order2";
    3.93 -val real_mult_self_sum_ge_zero = thm "real_mult_self_sum_ge_zero";
    3.94  val real_sum_square_gt_zero = thm "real_sum_square_gt_zero";
    3.95  val real_sum_square_gt_zero2 = thm "real_sum_square_gt_zero2";
    3.96  val real_minus_mult_self_le = thm "real_minus_mult_self_le";