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