# HG changeset patch
# User ballarin
# Date 1403023304 -7200
# Node ID 3a20f8a24b13fc4c126859901a8c75db5b2dc7aa
# Parent  0260171a51ef3cc2db439f044379db4d720e9b39
Lemmas contributed by Joachim Breitner.

diff -r 0260171a51ef -r 3a20f8a24b13 src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Tue Jun 17 18:33:34 2014 +0200
+++ b/src/HOL/Algebra/Group.thy	Tue Jun 17 18:41:44 2014 +0200
@@ -388,6 +388,14 @@
 apply (rule r_cancel [THEN iffD1], auto)
 done
 
+(* Contributed by Joachim Breitner *)
+lemma (in group) inv_solve_left:
+  "\<lbrakk> a \<in> carrier G; b \<in> carrier G; c \<in> carrier G \<rbrakk> \<Longrightarrow> a = inv b \<otimes> c \<longleftrightarrow> c = b \<otimes> a"
+  by (metis inv_equality l_inv_ex l_one m_assoc r_inv)
+lemma (in group) inv_solve_right:
+  "\<lbrakk> a \<in> carrier G; b \<in> carrier G; c \<in> carrier G \<rbrakk> \<Longrightarrow> a = b \<otimes> inv c \<longleftrightarrow> b = a \<otimes> c"
+  by (metis inv_equality l_inv_ex l_one m_assoc r_inv)
+
 text {* Power *}
 
 lemma (in group) int_pow_def2:
@@ -402,7 +410,30 @@
   "\<one> (^) (z::int) = \<one>"
   by (simp add: int_pow_def2)
 
+(* The following are contributed by Joachim Breitner *)
 
+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_1 [simp]:
+  "x \<in> carrier G \<Longrightarrow> x (^) (1::int) = x"
+  by (simp add: int_pow_def2)
+
+lemma (in group) int_pow_neg:
+  "x \<in> carrier G \<Longrightarrow> x (^) (-i::int) = inv (x (^) i)"
+  by (simp add: int_pow_def2)
+
+lemma (in group) int_pow_mult:
+  "x \<in> carrier G \<Longrightarrow> x (^) (i + j::int) = x (^) i \<otimes> x (^) j"
+proof -
+  have [simp]: "-i - j = -j - i" by simp
+  assume "x : carrier G" then
+  show ?thesis
+    by (auto simp add: int_pow_def2 inv_solve_left inv_solve_right nat_add_distrib [symmetric] nat_pow_mult )
+qed
+
+ 
 subsection {* Subgroups *}
 
 locale subgroup =
@@ -627,6 +658,11 @@
   with x show ?thesis by (simp del: H.r_inv H.Units_r_inv)
 qed
 
+(* Contributed by Joachim Breitner *)
+lemma (in group) int_pow_is_hom:
+  "x \<in> carrier G \<Longrightarrow> (op(^) x) \<in> hom \<lparr> carrier = UNIV, mult = op +, one = 0::int \<rparr> G "
+  unfolding hom_def by (simp add: int_pow_mult)
+
 
 subsection {* Commutative Structures *}