src/HOL/Real/RealPow.thy
changeset 14334 6137d24eef79
parent 14304 cc0b4bbfbc43
child 14348 744c868ee0b7
     1.1 --- a/src/HOL/Real/RealPow.thy	Mon Dec 29 06:49:26 2003 +0100
     1.2 +++ b/src/HOL/Real/RealPow.thy	Thu Jan 01 10:06:32 2004 +0100
     1.3 @@ -28,7 +28,7 @@
     1.4  
     1.5  lemma realpow_inverse: "inverse ((r::real) ^ n) = (inverse r) ^ n"
     1.6  apply (induct_tac "n")
     1.7 -apply (auto simp add: real_inverse_distrib)
     1.8 +apply (auto simp add: inverse_mult_distrib)
     1.9  done
    1.10  
    1.11  lemma realpow_abs: "abs(r ^ n) = abs(r::real) ^ n"
    1.12 @@ -38,7 +38,7 @@
    1.13  
    1.14  lemma realpow_add: "(r::real) ^ (n + m) = (r ^ n) * (r ^ m)"
    1.15  apply (induct_tac "n")
    1.16 -apply (auto simp add: real_mult_ac)
    1.17 +apply (auto simp add: mult_ac)
    1.18  done
    1.19  
    1.20  lemma realpow_one [simp]: "(r::real) ^ 1 = r"
    1.21 @@ -49,17 +49,17 @@
    1.22  
    1.23  lemma realpow_gt_zero [rule_format]: "(0::real) < r --> 0 < r ^ n"
    1.24  apply (induct_tac "n")
    1.25 -apply (auto intro: real_mult_order simp add: real_zero_less_one)
    1.26 +apply (auto intro: real_mult_order simp add: zero_less_one)
    1.27  done
    1.28  
    1.29  lemma realpow_ge_zero [rule_format]: "(0::real) \<le> r --> 0 \<le> r ^ n"
    1.30  apply (induct_tac "n")
    1.31 -apply (auto simp add: real_0_le_mult_iff)
    1.32 +apply (auto simp add: zero_le_mult_iff)
    1.33  done
    1.34  
    1.35  lemma realpow_le [rule_format]: "(0::real) \<le> x & x \<le> y --> x ^ n \<le> y ^ n"
    1.36  apply (induct_tac "n")
    1.37 -apply (auto intro!: real_mult_le_mono)
    1.38 +apply (auto intro!: mult_mono)
    1.39  apply (simp (no_asm_simp) add: realpow_ge_zero)
    1.40  done
    1.41  
    1.42 @@ -90,7 +90,7 @@
    1.43  
    1.44  lemma realpow_mult: "((r::real) * s) ^ n = (r ^ n) * (s ^ n)"
    1.45  apply (induct_tac "n")
    1.46 -apply (auto simp add: real_mult_ac)
    1.47 +apply (auto simp add: mult_ac)
    1.48  done
    1.49  
    1.50  lemma realpow_two_le [simp]: "(0::real) \<le> r^ Suc (Suc 0)"
    1.51 @@ -106,14 +106,15 @@
    1.52  apply auto
    1.53  apply (cut_tac real_zero_less_one)
    1.54  apply (frule_tac x = 0 in order_less_trans, assumption)
    1.55 -apply (drule_tac  z = r and x = 1 in real_mult_less_mono1)
    1.56 -apply (auto intro: order_less_trans)
    1.57 +apply (frule_tac c = r and a = 1 in mult_strict_right_mono)
    1.58 +apply assumption; 
    1.59 +apply (simp add: ); 
    1.60  done
    1.61  
    1.62  lemma realpow_ge_one [rule_format]: "(1::real) < r --> 1 \<le> r ^ n"
    1.63  apply (induct_tac "n", auto)
    1.64  apply (subgoal_tac "1*1 \<le> r * r^n")
    1.65 -apply (rule_tac [2] real_mult_le_mono, auto)
    1.66 +apply (rule_tac [2] mult_mono, auto)
    1.67  done
    1.68  
    1.69  lemma realpow_ge_one2: "(1::real) \<le> r ==> 1 \<le> r ^ n"
    1.70 @@ -170,7 +171,7 @@
    1.71  apply (simp_all (no_asm_simp))
    1.72  apply clarify
    1.73  apply (subgoal_tac "r * r ^ na \<le> 1 * r ^ n", simp)
    1.74 -apply (rule real_mult_le_mono)
    1.75 +apply (rule mult_mono)
    1.76  apply (auto simp add: realpow_ge_zero less_Suc_eq)
    1.77  done
    1.78  
    1.79 @@ -237,7 +238,7 @@
    1.80  
    1.81  lemma realpow_two_diff: "(x::real)^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)"
    1.82  apply (unfold real_diff_def)
    1.83 -apply (simp add: real_add_mult_distrib2 real_add_mult_distrib real_mult_ac)
    1.84 +apply (simp add: right_distrib left_distrib mult_ac)
    1.85  done
    1.86  
    1.87  lemma realpow_two_disj: "((x::real)^Suc (Suc 0) = y^Suc (Suc 0)) = (x = y | x = -y)"
    1.88 @@ -247,7 +248,7 @@
    1.89  
    1.90  (* used in Transc *)
    1.91  lemma realpow_diff: "[|(x::real) \<noteq> 0; m \<le> n |] ==> x ^ (n - m) = x ^ n * inverse (x ^ m)"
    1.92 -by (auto simp add: le_eq_less_or_eq less_iff_Suc_add realpow_add realpow_not_zero real_mult_ac)
    1.93 +by (auto simp add: le_eq_less_or_eq less_iff_Suc_add realpow_add realpow_not_zero mult_ac)
    1.94  
    1.95  lemma realpow_real_of_nat: "real (m::nat) ^ n = real (m ^ n)"
    1.96  apply (induct_tac "n")
    1.97 @@ -256,7 +257,7 @@
    1.98  
    1.99  lemma realpow_real_of_nat_two_pos [simp] : "0 < real (Suc (Suc 0) ^ n)"
   1.100  apply (induct_tac "n")
   1.101 -apply (auto simp add: real_of_nat_mult real_0_less_mult_iff)
   1.102 +apply (auto simp add: real_of_nat_mult zero_less_mult_iff)
   1.103  done
   1.104  
   1.105  lemma realpow_increasing:
   1.106 @@ -284,12 +285,12 @@
   1.107  
   1.108  lemma zero_less_realpow_abs_iff [simp]: "(0 < (abs x)^n) = (x \<noteq> (0::real) | n=0)"
   1.109  apply (induct_tac "n")
   1.110 -apply (auto simp add: real_0_less_mult_iff)
   1.111 +apply (auto simp add: zero_less_mult_iff)
   1.112  done
   1.113  
   1.114  lemma zero_le_realpow_abs [simp]: "(0::real) \<le> (abs x)^n"
   1.115  apply (induct_tac "n")
   1.116 -apply (auto simp add: real_0_le_mult_iff)
   1.117 +apply (auto simp add: zero_le_mult_iff)
   1.118  done
   1.119  
   1.120  
   1.121 @@ -332,7 +333,7 @@
   1.122    by (auto intro: real_sum_squares_cancel)
   1.123  
   1.124  lemma real_squared_diff_one_factored: "x*x - (1::real) = (x + 1)*(x - 1)"
   1.125 -apply (auto simp add: real_add_mult_distrib real_add_mult_distrib2 real_diff_def)
   1.126 +apply (auto simp add: left_distrib right_distrib real_diff_def)
   1.127  done
   1.128  
   1.129  lemma real_mult_is_one: "(x*x = (1::real)) = (x = 1 | x = - 1)"
   1.130 @@ -357,14 +358,14 @@
   1.131        ==> inverse x * y < inverse x1 * u"
   1.132  apply (rule_tac c=x in mult_less_imp_less_left) 
   1.133  apply (auto simp add: real_mult_assoc [symmetric])
   1.134 -apply (simp (no_asm) add: real_mult_ac)
   1.135 +apply (simp (no_asm) add: mult_ac)
   1.136  apply (rule_tac c=x1 in mult_less_imp_less_right) 
   1.137 -apply (auto simp add: real_mult_ac)
   1.138 +apply (auto simp add: mult_ac)
   1.139  done
   1.140  
   1.141  text{*Used once: in Hyperreal/Transcendental.ML*}
   1.142  lemma real_mult_inverse_cancel2: "[|(0::real) < x;0 < x1; x1 * y < x * u |] ==> y * inverse x < u * inverse x1"
   1.143 -apply (auto dest: real_mult_inverse_cancel simp add: real_mult_ac)
   1.144 +apply (auto dest: real_mult_inverse_cancel simp add: mult_ac)
   1.145  done
   1.146  
   1.147  lemma inverse_real_of_nat_gt_zero: "0 < inverse (real (Suc n))"
   1.148 @@ -403,18 +404,18 @@
   1.149  
   1.150  lemma realpow_ge_zero2 [rule_format (no_asm)]: "(0::real) \<le> r --> 0 \<le> r ^ n"
   1.151  apply (induct_tac "n")
   1.152 -apply (auto simp add: real_0_le_mult_iff)
   1.153 +apply (auto simp add: zero_le_mult_iff)
   1.154  done
   1.155  
   1.156  lemma realpow_le2 [rule_format (no_asm)]: "(0::real) \<le> x & x \<le> y --> x ^ n \<le> y ^ n"
   1.157  apply (induct_tac "n")
   1.158 -apply (auto intro!: real_mult_le_mono simp add: realpow_ge_zero2)
   1.159 +apply (auto intro!: mult_mono simp add: realpow_ge_zero2)
   1.160  done
   1.161  
   1.162  lemma realpow_Suc_gt_one: "(1::real) < r ==> 1 < r ^ (Suc n)"
   1.163  apply (frule_tac n = "n" in realpow_ge_one)
   1.164  apply (drule real_le_imp_less_or_eq, safe)
   1.165 -apply (frule real_zero_less_one [THEN real_less_trans])
   1.166 +apply (frule zero_less_one [THEN real_less_trans])
   1.167  apply (drule_tac y = "r ^ n" in real_mult_less_mono2)
   1.168  apply assumption
   1.169  apply (auto dest: real_less_trans)