```Hi,

I had a look at my old Free-Groups AFP entry, where I had some partial
refactoring in my local branch. While continuing a bit on it, I had a
need for these lemmas, and I believe they should go into the
Algebra/Groups (also attached):

lemma (in group) int_pow_one' [simp]:
"x ∈ carrier G ⟹ x (^) (1::int) = x"

lemma (in group) int_pow_neg [simp]:
"x ∈ carrier G ⟹ x (^) (-i::int) = inv (x (^) i)"

lemma (in group) int_pow_closed [intro, simp]:
"x ∈ carrier G ==> x (^) (i::int) ∈ carrier G"

assumes "x ∈ carrier G"
shows "x (^) (i + j::int) = x (^) i ⊗ x (^) j"
proof-
(* A simple solver for equations with inv and ⊗ *)
have [simp]:"⋀ a b c. a ∈ carrier G ⟹ b ∈ carrier G ⟹ c ∈ carrier G ⟹ a = inv b ⊗ c ⟷ c = b ⊗ a" by (metis inv_equality l_inv_ex l_one m_assoc r_inv)
have [simp]:"⋀ a b c. a ∈ carrier G ⟹ b ∈ carrier G ⟹ c ∈ carrier G ⟹ a = b ⊗ inv c ⟷ b = a ⊗ c" by (metis inv_equality l_inv_ex l_one m_assoc r_inv)
have [simp]:"- i - j = - j - i" by simp
from assms
qed

The [simp] on the last lemma is probably debatable, I don’t have strong

Greetings,
Joachim

--
Joachim “nomeata” Breitner
mail at joachim-breitner.de • http://www.joachim-breitner.de/
Jabber: nomeata at joachim-breitner.de  • GPG-Key: 0x4743206C
Debian Developer: nomeata at debian.org
```
```theory Submission
imports  "~~/src/HOL/Algebra/Group"
begin

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

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

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

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