theory Submission
imports  "~~/src/HOL/Algebra/Group"
begin


lemma (in group) int_pow_one' [simp]:
  "x \<in> carrier G \<Longrightarrow> x (^) (1::int) = x"
  by (simp add: int_pow_def2)

lemma (in group) int_pow_neg [simp]:
  "x \<in> carrier G \<Longrightarrow> x (^) (-i::int) = inv (x (^) i)"
  by (simp add: int_pow_def2) 

lemma (in group) int_pow_closed [intro, simp]:
  "x \<in> carrier G ==> x (^) (i::int) \<in> carrier G"
  by (simp add: int_pow_def2) 

lemma (in group) int_pow_add [simp]:
  assumes "x \<in> carrier G"
  shows "x (^) (i + j::int) = x (^) i \<otimes> x (^) j"
proof-
  (* A simple solver for equations with inv and \<otimes> *)
  have [simp]:"\<And> a b c. a \<in> carrier G \<Longrightarrow> b \<in> carrier G \<Longrightarrow> c \<in> carrier G \<Longrightarrow> a = inv b \<otimes> c \<longleftrightarrow> c = b \<otimes> a" by (metis inv_equality l_inv_ex l_one m_assoc r_inv)
  have [simp]:"\<And> a b c. a \<in> carrier G \<Longrightarrow> b \<in> carrier G \<Longrightarrow> c \<in> carrier G \<Longrightarrow> a = b \<otimes> inv c \<longleftrightarrow> b = a \<otimes> c" by (metis inv_equality l_inv_ex l_one m_assoc r_inv)
  have [simp]:"- i - j = - j - i" by simp
  from assms
  show ?thesis by (auto simp add: int_pow_def2 nat_add_distrib[symmetric] nat_pow_mult inv_mult_group[symmetric])
qed

end