src/HOL/Algebra/Group.thy
changeset 61628 8dd2bd4fe30b
parent 61565 352c73a689da
child 63167 0909deb8059b
     1.1 --- a/src/HOL/Algebra/Group.thy	Tue Nov 10 23:41:20 2015 +0100
     1.2 +++ b/src/HOL/Algebra/Group.thy	Wed Nov 11 09:06:30 2015 +0100
     1.3 @@ -44,6 +44,9 @@
     1.4      in if z < 0 then inv\<^bsub>G\<^esub> (p (nat (-z))) else p (nat z))"
     1.5  end
     1.6  
     1.7 +lemma int_pow_int: "x (^)\<^bsub>G\<^esub> (int n) = x (^)\<^bsub>G\<^esub> n"
     1.8 +by(simp add: int_pow_def nat_pow_def)
     1.9 +
    1.10  locale monoid =
    1.11    fixes G (structure)
    1.12    assumes m_closed [intro, simp]:
    1.13 @@ -187,6 +190,9 @@
    1.14    with G show ?thesis by (simp del: r_one add: m_assoc Units_closed)
    1.15  qed
    1.16  
    1.17 +lemma (in monoid) carrier_not_empty: "carrier G \<noteq> {}"
    1.18 +by auto
    1.19 +
    1.20  text \<open>Power\<close>
    1.21  
    1.22  lemma (in monoid) nat_pow_closed [intro, simp]:
    1.23 @@ -434,7 +440,16 @@
    1.24      by (auto simp add: int_pow_def2 inv_solve_left inv_solve_right nat_add_distrib [symmetric] nat_pow_mult )
    1.25  qed
    1.26  
    1.27 - 
    1.28 +lemma (in group) int_pow_diff:
    1.29 +  "x \<in> carrier G \<Longrightarrow> x (^) (n - m :: int) = x (^) n \<otimes> inv (x (^) m)"
    1.30 +by(simp only: diff_conv_add_uminus int_pow_mult int_pow_neg)
    1.31 +
    1.32 +lemma (in group) inj_on_multc: "c \<in> carrier G \<Longrightarrow> inj_on (\<lambda>x. x \<otimes> c) (carrier G)"
    1.33 +by(simp add: inj_on_def)
    1.34 +
    1.35 +lemma (in group) inj_on_cmult: "c \<in> carrier G \<Longrightarrow> inj_on (\<lambda>x. c \<otimes> x) (carrier G)"
    1.36 +by(simp add: inj_on_def)
    1.37 +
    1.38  subsection \<open>Subgroups\<close>
    1.39  
    1.40  locale subgroup =