src/HOL/Real/RealPow.thy

 apply (auto dest: realpow_not_zero)
 done
 
 lemma realpow_inverse: "inverse ((r::real) ^ n) = (inverse r) ^ n"
 apply (induct_tac "n")
-apply (auto simp add: real_inverse_distrib)
+apply (auto simp add: inverse_mult_distrib)
 done
 
 lemma realpow_abs: "abs(r ^ n) = abs(r::real) ^ n"
 apply (induct_tac "n")
 apply (auto simp add: abs_mult)
 done
 
 lemma realpow_add: "(r::real) ^ (n + m) = (r ^ n) * (r ^ m)"
 apply (induct_tac "n")
-apply (auto simp add: real_mult_ac)
+apply (auto simp add: mult_ac)
 done
 
 lemma realpow_one [simp]: "(r::real) ^ 1 = r"
 by simp
 
 lemma realpow_two: "(r::real)^ (Suc (Suc 0)) = r * r"
 by simp
 
 lemma realpow_gt_zero [rule_format]: "(0::real) < r --> 0 < r ^ n"
 apply (induct_tac "n")
-apply (auto intro: real_mult_order simp add: real_zero_less_one)
+apply (auto intro: real_mult_order simp add: zero_less_one)
 done
 
 lemma realpow_ge_zero [rule_format]: "(0::real) \<le> r --> 0 \<le> r ^ n"
 apply (induct_tac "n")
-apply (auto simp add: real_0_le_mult_iff)
+apply (auto simp add: zero_le_mult_iff)
 done
 
 lemma realpow_le [rule_format]: "(0::real) \<le> x & x \<le> y --> x ^ n \<le> y ^ n"
 apply (induct_tac "n")
-apply (auto intro!: real_mult_le_mono)
+apply (auto intro!: mult_mono)
 apply (simp (no_asm_simp) add: realpow_ge_zero)
 done
 
 lemma realpow_0_left [rule_format, simp]:
      "0 < n --> 0 ^ n = (0::real)"

 apply (auto simp add: abs_mult)
 done
 
 lemma realpow_mult: "((r::real) * s) ^ n = (r ^ n) * (s ^ n)"
 apply (induct_tac "n")
-apply (auto simp add: real_mult_ac)
+apply (auto simp add: mult_ac)
 done
 
 lemma realpow_two_le [simp]: "(0::real) \<le> r^ Suc (Suc 0)"
 by (simp add: real_le_square)
 

 
 lemma realpow_two_gt_one: "(1::real) < r ==> 1 < r^ (Suc (Suc 0))"
 apply auto
 apply (cut_tac real_zero_less_one)
 apply (frule_tac x = 0 in order_less_trans, assumption)
-apply (drule_tac  z = r and x = 1 in real_mult_less_mono1)
-apply (auto intro: order_less_trans)
+apply (frule_tac c = r and a = 1 in mult_strict_right_mono)
+apply assumption; 
+apply (simp add: ); 
 done
 
 lemma realpow_ge_one [rule_format]: "(1::real) < r --> 1 \<le> r ^ n"
 apply (induct_tac "n", auto)
 apply (subgoal_tac "1*1 \<le> r * r^n")
-apply (rule_tac [2] real_mult_le_mono, auto)
+apply (rule_tac [2] mult_mono, auto)
 done
 
 lemma realpow_ge_one2: "(1::real) \<le> r ==> 1 \<le> r ^ n"
 apply (drule order_le_imp_less_or_eq)
 apply (auto dest: realpow_ge_one)

 lemma realpow_less_le [rule_format]: "0 \<le> r & r < (1::real) & n < N --> r ^ N \<le> r ^ n"
 apply (induct_tac "N")
 apply (simp_all (no_asm_simp))
 apply clarify
 apply (subgoal_tac "r * r ^ na \<le> 1 * r ^ n", simp)
-apply (rule real_mult_le_mono)
+apply (rule mult_mono)
 apply (auto simp add: realpow_ge_zero less_Suc_eq)
 done
 
 lemma realpow_le_le: "[| 0 \<le> r; r < (1::real); n \<le> N |] ==> r ^ N \<le> r ^ n"
 apply (drule_tac n = N in le_imp_less_or_eq)

 lemma realpow_two_minus [simp]: "(-x)^Suc (Suc 0) = (x::real)^Suc (Suc 0)"
 by simp
 
 lemma realpow_two_diff: "(x::real)^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)"
 apply (unfold real_diff_def)
-apply (simp add: real_add_mult_distrib2 real_add_mult_distrib real_mult_ac)
+apply (simp add: right_distrib left_distrib mult_ac)
 done
 
 lemma realpow_two_disj: "((x::real)^Suc (Suc 0) = y^Suc (Suc 0)) = (x = y | x = -y)"
 apply (cut_tac x = x and y = y in realpow_two_diff)
 apply (auto simp del: realpow_Suc)
 done
 
 (* used in Transc *)
 lemma realpow_diff: "[|(x::real) \<noteq> 0; m \<le> n |] ==> x ^ (n - m) = x ^ n * inverse (x ^ m)"
-by (auto simp add: le_eq_less_or_eq less_iff_Suc_add realpow_add realpow_not_zero real_mult_ac)
+by (auto simp add: le_eq_less_or_eq less_iff_Suc_add realpow_add realpow_not_zero mult_ac)
 
 lemma realpow_real_of_nat: "real (m::nat) ^ n = real (m ^ n)"
 apply (induct_tac "n")
 apply (auto simp add: real_of_nat_one real_of_nat_mult)
 done
 
 lemma realpow_real_of_nat_two_pos [simp] : "0 < real (Suc (Suc 0) ^ n)"
 apply (induct_tac "n")
-apply (auto simp add: real_of_nat_mult real_0_less_mult_iff)
+apply (auto simp add: real_of_nat_mult zero_less_mult_iff)
 done
 
 lemma realpow_increasing:
   assumes xnonneg: "(0::real) \<le> x"
       and ynonneg: "0 \<le> y"

 lemma realpow_eq_0_iff [simp]: "(x^n = 0) = (x = (0::real) & 0<n)"
 by (induct_tac "n", auto)
 
 lemma zero_less_realpow_abs_iff [simp]: "(0 < (abs x)^n) = (x \<noteq> (0::real) | n=0)"
 apply (induct_tac "n")
-apply (auto simp add: real_0_less_mult_iff)
+apply (auto simp add: zero_less_mult_iff)
 done
 
 lemma zero_le_realpow_abs [simp]: "(0::real) \<le> (abs x)^n"
 apply (induct_tac "n")
-apply (auto simp add: real_0_le_mult_iff)
+apply (auto simp add: zero_le_mult_iff)
 done
 
 
 (*** Literal arithmetic involving powers, type real ***)
 

 text{*Used several times in Hyperreal/Transcendental.ML*}
 lemma real_sum_squares_cancel_a: "x * x = -(y * y) ==> x = (0::real) & y=0"
   by (auto intro: real_sum_squares_cancel)
 
 lemma real_squared_diff_one_factored: "x*x - (1::real) = (x + 1)*(x - 1)"
-apply (auto simp add: real_add_mult_distrib real_add_mult_distrib2 real_diff_def)
+apply (auto simp add: left_distrib right_distrib real_diff_def)
 done
 
 lemma real_mult_is_one: "(x*x = (1::real)) = (x = 1 | x = - 1)"
 apply auto
 apply (drule right_minus_eq [THEN iffD2]) 

 lemma real_mult_inverse_cancel:
      "[|(0::real) < x; 0 < x1; x1 * y < x * u |] 
       ==> inverse x * y < inverse x1 * u"
 apply (rule_tac c=x in mult_less_imp_less_left) 
 apply (auto simp add: real_mult_assoc [symmetric])
-apply (simp (no_asm) add: real_mult_ac)
+apply (simp (no_asm) add: mult_ac)
 apply (rule_tac c=x1 in mult_less_imp_less_right) 
-apply (auto simp add: real_mult_ac)
+apply (auto simp add: mult_ac)
 done
 
 text{*Used once: in Hyperreal/Transcendental.ML*}
 lemma real_mult_inverse_cancel2: "[|(0::real) < x;0 < x1; x1 * y < x * u |] ==> y * inverse x < u * inverse x1"
-apply (auto dest: real_mult_inverse_cancel simp add: real_mult_ac)
+apply (auto dest: real_mult_inverse_cancel simp add: mult_ac)
 done
 
 lemma inverse_real_of_nat_gt_zero: "0 < inverse (real (Suc n))"
 apply auto
 done

 apply (auto simp add: realpow_mult realpow_inverse)
 done
 
 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)
+apply (auto simp add: zero_le_mult_iff)
 done
 
 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)
+apply (auto intro!: mult_mono simp add: realpow_ge_zero2)
 done
 
 lemma realpow_Suc_gt_one: "(1::real) < r ==> 1 < r ^ (Suc n)"
 apply (frule_tac n = "n" in realpow_ge_one)
 apply (drule real_le_imp_less_or_eq, safe)
-apply (frule real_zero_less_one [THEN real_less_trans])
+apply (frule zero_less_one [THEN real_less_trans])
 apply (drule_tac y = "r ^ n" in real_mult_less_mono2)
 apply assumption
 apply (auto dest: real_less_trans)
 done