Email Gateway (Aug 19 2022 at 12:15): Email Gateway (Aug 19 2022 at 12:15):From: Joachim Breitner <mail@joachim-breitner.de>
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"
by (simp add: int_pow_def2)
lemma (in group) int_pow_neg [simp]:
"x ∈ carrier G ⟹ x (^) (-i::int) = inv (x (^) i)"
by (simp add: int_pow_def2)
lemma (in group) int_pow_closed [intro, simp]:
"x ∈ carrier G ==> x (^) (i::int) ∈ carrier G"
by (simp add: int_pow_def2)
lemma (in group) int_pow_add [simp]:
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
show ?thesis by (auto simp add: int_pow_def2 nat_add_distrib[symmetric] nat_pow_mult inv_mult_group[symmetric])
qed
The [simp] on the last lemma is probably debatable, I don’t have strong
opinions about it.
Greetings,
Joachim
Submission.thy
signature.asc
Email Gateway (Aug 19 2022 at 12:15):From: Clemens Ballarin <ballarin@in.tum.de>
I will take care of this. Thanks!
Clemens
Last updated: Apr 24 2024 at 01:07 UTC