Theory Power_int

section ‹ Integer Powers ›

theory Power_int
  imports "HOL.Real"
begin

text ‹ The standard HOL power operator is only for natural powers. This operator allows integers. ›

definition intpow :: "'a::{linordered_field}  int  'a" (infixr "^Z" 80) where
"intpow x n = (if (n < 0) then inverse (x ^ nat (-n)) else (x ^ nat n))"

lemma intpow_zero [simp]: "x ^Z 0 = 1"
  by (simp add: intpow_def)

lemma intpow_spos [simp]: "x > 0  x ^Z n > 0"
  by (simp add: intpow_def)

lemma intpow_one [simp]: "x ^Z 1 = x"
  by (simp add: intpow_def)

lemma one_intpow [simp]: "1 ^Z n = 1"
  by (simp add: intpow_def)

lemma intpow_plus: "x > 0  x ^Z (m + n) = x ^Z m * x ^Z n"
  apply (simp add: intpow_def field_simps power_add)
  apply (metis (no_types, opaque_lifting) abs_ge_zero add.commute add_diff_cancel_right' nat_add_distrib power_add uminus_add_conv_diff zabs_def)
  done

lemma intpow_mult_combine: "x > 0  x ^Z m * (x ^Z n * y) = x ^Z (m + n) * y"
  by (simp add: intpow_plus)

lemma intpow_pos [simp]: "n  0  x ^Z n = x ^ nat n"
  by (simp add: intpow_def)

lemma intpow_uminus: "x ^Z -n = inverse (x ^Z n)"
  by (simp add: intpow_def)

lemma intpow_uminus_nat: "n  0  x ^Z -n = inverse (x ^ nat n)"
  by (simp add: intpow_def)

lemma intpow_inverse: "inverse a ^Z n = inverse (a ^Z n)"
  by (simp add: intpow_def power_inverse)

lemma intpow_mult_distrib: "(x * y) ^Z m = x ^Z m * y ^Z m"
  by (simp add: intpow_def power_mult_distrib)

end