src/HOL/Power.thy
changeset 57512 cc97b347b301
parent 57418 6ab1c7cb0b8d
child 57514 bdc2c6b40bf2
     1.1 --- a/src/HOL/Power.thy	Fri Jul 04 20:07:08 2014 +0200
     1.2 +++ b/src/HOL/Power.thy	Fri Jul 04 20:18:47 2014 +0200
     1.3 @@ -53,7 +53,7 @@
     1.4  
     1.5  lemma power_commutes:
     1.6    "a ^ n * a = a * a ^ n"
     1.7 -  by (induct n) (simp_all add: mult_assoc)
     1.8 +  by (induct n) (simp_all add: mult.assoc)
     1.9  
    1.10  lemma power_Suc2:
    1.11    "a ^ Suc n = a ^ n * a"
    1.12 @@ -71,11 +71,11 @@
    1.13    by (simp add: numeral_2_eq_2)
    1.14  
    1.15  lemma power3_eq_cube: "a ^ 3 = a * a * a"
    1.16 -  by (simp add: numeral_3_eq_3 mult_assoc)
    1.17 +  by (simp add: numeral_3_eq_3 mult.assoc)
    1.18  
    1.19  lemma power_even_eq:
    1.20    "a ^ (2 * n) = (a ^ n)\<^sup>2"
    1.21 -  by (subst mult_commute) (simp add: power_mult)
    1.22 +  by (subst mult.commute) (simp add: power_mult)
    1.23  
    1.24  lemma power_odd_eq:
    1.25    "a ^ Suc (2*n) = a * (a ^ n)\<^sup>2"
    1.26 @@ -88,7 +88,7 @@
    1.27  lemma power_numeral_odd:
    1.28    "z ^ numeral (Num.Bit1 w) = (let w = z ^ (numeral w) in z * w * w)"
    1.29    unfolding numeral_Bit1 One_nat_def add_Suc_right add_0_right
    1.30 -  unfolding power_Suc power_add Let_def mult_assoc ..
    1.31 +  unfolding power_Suc power_add Let_def mult.assoc ..
    1.32  
    1.33  lemma funpow_times_power:
    1.34    "(times x ^^ f x) = times (x ^ f x)"
    1.35 @@ -100,7 +100,7 @@
    1.36    with Suc have "n = g x" by simp
    1.37    with Suc have "times x ^^ g x = times (x ^ g x)" by simp
    1.38    moreover from Suc g_def have "f x = g x + 1" by simp
    1.39 -  ultimately show ?case by (simp add: power_add funpow_add fun_eq_iff mult_assoc)
    1.40 +  ultimately show ?case by (simp add: power_add funpow_add fun_eq_iff mult.assoc)
    1.41  qed
    1.42  
    1.43  end
    1.44 @@ -197,7 +197,7 @@
    1.45    case 0 show ?case by simp
    1.46  next
    1.47    case (Suc n) then show ?case
    1.48 -    by (simp del: power_Suc add: power_Suc2 mult_assoc)
    1.49 +    by (simp del: power_Suc add: power_Suc2 mult.assoc)
    1.50  qed
    1.51  
    1.52  lemma power_minus_Bit0:
    1.53 @@ -626,7 +626,7 @@
    1.54  lemma power2_diff:
    1.55    fixes x y :: "'a::comm_ring_1"
    1.56    shows "(x - y)\<^sup>2 = x\<^sup>2 + y\<^sup>2 - 2 * x * y"
    1.57 -  by (simp add: ring_distribs power2_eq_square mult_2) (rule mult_commute)
    1.58 +  by (simp add: ring_distribs power2_eq_square mult_2) (rule mult.commute)
    1.59  
    1.60  lemma power_0_Suc [simp]:
    1.61    "(0::'a::{power, semiring_0}) ^ Suc n = 0"