src/HOL/Power.thy
changeset 57512 cc97b347b301
parent 57418 6ab1c7cb0b8d
child 57514 bdc2c6b40bf2
equal deleted inserted replaced
57511:de51a86fc903 57512:cc97b347b301
    51   "a ^ 1 = a"
    51   "a ^ 1 = a"
    52   by simp
    52   by simp
    53 
    53 
    54 lemma power_commutes:
    54 lemma power_commutes:
    55   "a ^ n * a = a * a ^ n"
    55   "a ^ n * a = a * a ^ n"
    56   by (induct n) (simp_all add: mult_assoc)
    56   by (induct n) (simp_all add: mult.assoc)
    57 
    57 
    58 lemma power_Suc2:
    58 lemma power_Suc2:
    59   "a ^ Suc n = a ^ n * a"
    59   "a ^ Suc n = a ^ n * a"
    60   by (simp add: power_commutes)
    60   by (simp add: power_commutes)
    61 
    61 
    69 
    69 
    70 lemma power2_eq_square: "a\<^sup>2 = a * a"
    70 lemma power2_eq_square: "a\<^sup>2 = a * a"
    71   by (simp add: numeral_2_eq_2)
    71   by (simp add: numeral_2_eq_2)
    72 
    72 
    73 lemma power3_eq_cube: "a ^ 3 = a * a * a"
    73 lemma power3_eq_cube: "a ^ 3 = a * a * a"
    74   by (simp add: numeral_3_eq_3 mult_assoc)
    74   by (simp add: numeral_3_eq_3 mult.assoc)
    75 
    75 
    76 lemma power_even_eq:
    76 lemma power_even_eq:
    77   "a ^ (2 * n) = (a ^ n)\<^sup>2"
    77   "a ^ (2 * n) = (a ^ n)\<^sup>2"
    78   by (subst mult_commute) (simp add: power_mult)
    78   by (subst mult.commute) (simp add: power_mult)
    79 
    79 
    80 lemma power_odd_eq:
    80 lemma power_odd_eq:
    81   "a ^ Suc (2*n) = a * (a ^ n)\<^sup>2"
    81   "a ^ Suc (2*n) = a * (a ^ n)\<^sup>2"
    82   by (simp add: power_even_eq)
    82   by (simp add: power_even_eq)
    83 
    83 
    86   unfolding numeral_Bit0 power_add Let_def ..
    86   unfolding numeral_Bit0 power_add Let_def ..
    87 
    87 
    88 lemma power_numeral_odd:
    88 lemma power_numeral_odd:
    89   "z ^ numeral (Num.Bit1 w) = (let w = z ^ (numeral w) in z * w * w)"
    89   "z ^ numeral (Num.Bit1 w) = (let w = z ^ (numeral w) in z * w * w)"
    90   unfolding numeral_Bit1 One_nat_def add_Suc_right add_0_right
    90   unfolding numeral_Bit1 One_nat_def add_Suc_right add_0_right
    91   unfolding power_Suc power_add Let_def mult_assoc ..
    91   unfolding power_Suc power_add Let_def mult.assoc ..
    92 
    92 
    93 lemma funpow_times_power:
    93 lemma funpow_times_power:
    94   "(times x ^^ f x) = times (x ^ f x)"
    94   "(times x ^^ f x) = times (x ^ f x)"
    95 proof (induct "f x" arbitrary: f)
    95 proof (induct "f x" arbitrary: f)
    96   case 0 then show ?case by (simp add: fun_eq_iff)
    96   case 0 then show ?case by (simp add: fun_eq_iff)
    98   case (Suc n)
    98   case (Suc n)
    99   def g \<equiv> "\<lambda>x. f x - 1"
    99   def g \<equiv> "\<lambda>x. f x - 1"
   100   with Suc have "n = g x" by simp
   100   with Suc have "n = g x" by simp
   101   with Suc have "times x ^^ g x = times (x ^ g x)" by simp
   101   with Suc have "times x ^^ g x = times (x ^ g x)" by simp
   102   moreover from Suc g_def have "f x = g x + 1" by simp
   102   moreover from Suc g_def have "f x = g x + 1" by simp
   103   ultimately show ?case by (simp add: power_add funpow_add fun_eq_iff mult_assoc)
   103   ultimately show ?case by (simp add: power_add funpow_add fun_eq_iff mult.assoc)
   104 qed
   104 qed
   105 
   105 
   106 end
   106 end
   107 
   107 
   108 context comm_monoid_mult
   108 context comm_monoid_mult
   195   "(- a) ^ n = (- 1) ^ n * a ^ n"
   195   "(- a) ^ n = (- 1) ^ n * a ^ n"
   196 proof (induct n)
   196 proof (induct n)
   197   case 0 show ?case by simp
   197   case 0 show ?case by simp
   198 next
   198 next
   199   case (Suc n) then show ?case
   199   case (Suc n) then show ?case
   200     by (simp del: power_Suc add: power_Suc2 mult_assoc)
   200     by (simp del: power_Suc add: power_Suc2 mult.assoc)
   201 qed
   201 qed
   202 
   202 
   203 lemma power_minus_Bit0:
   203 lemma power_minus_Bit0:
   204   "(- x) ^ numeral (Num.Bit0 k) = x ^ numeral (Num.Bit0 k)"
   204   "(- x) ^ numeral (Num.Bit0 k) = x ^ numeral (Num.Bit0 k)"
   205   by (induct k, simp_all only: numeral_class.numeral.simps power_add
   205   by (induct k, simp_all only: numeral_class.numeral.simps power_add
   624   by (simp add: algebra_simps power2_eq_square mult_2_right)
   624   by (simp add: algebra_simps power2_eq_square mult_2_right)
   625 
   625 
   626 lemma power2_diff:
   626 lemma power2_diff:
   627   fixes x y :: "'a::comm_ring_1"
   627   fixes x y :: "'a::comm_ring_1"
   628   shows "(x - y)\<^sup>2 = x\<^sup>2 + y\<^sup>2 - 2 * x * y"
   628   shows "(x - y)\<^sup>2 = x\<^sup>2 + y\<^sup>2 - 2 * x * y"
   629   by (simp add: ring_distribs power2_eq_square mult_2) (rule mult_commute)
   629   by (simp add: ring_distribs power2_eq_square mult_2) (rule mult.commute)
   630 
   630 
   631 lemma power_0_Suc [simp]:
   631 lemma power_0_Suc [simp]:
   632   "(0::'a::{power, semiring_0}) ^ Suc n = 0"
   632   "(0::'a::{power, semiring_0}) ^ Suc n = 0"
   633   by simp
   633   by simp
   634 
   634