# HG changeset patch
# User Andreas Lochbihler
# Date 1447229190 -3600
# Node ID 8dd2bd4fe30b41fbde9bd92bbd842e219f9089fa
# Parent  c304402cc3df3699a290c2f764ffc3701faa9f41
add lemmas about monoids and groups

diff -r c304402cc3df -r 8dd2bd4fe30b src/HOL/Algebra/Coset.thy
--- a/src/HOL/Algebra/Coset.thy	Tue Nov 10 23:41:20 2015 +0100
+++ b/src/HOL/Algebra/Coset.thy	Wed Nov 11 09:06:30 2015 +0100
@@ -759,6 +759,9 @@
   order :: "('a, 'b) monoid_scheme \<Rightarrow> nat"
   where "order S = card (carrier S)"
 
+lemma (in monoid) order_gt_0_iff_finite: "0 < order G \<longleftrightarrow> finite (carrier G)"
+by(auto simp add: order_def card_gt_0_iff)
+
 lemma (in group) rcosets_part_G:
   assumes "subgroup H G"
   shows "\<Union>(rcosets H) = carrier G"
diff -r c304402cc3df -r 8dd2bd4fe30b src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Tue Nov 10 23:41:20 2015 +0100
+++ b/src/HOL/Algebra/Group.thy	Wed Nov 11 09:06:30 2015 +0100
@@ -44,6 +44,9 @@
     in if z < 0 then inv\<^bsub>G\<^esub> (p (nat (-z))) else p (nat z))"
 end
 
+lemma int_pow_int: "x (^)\<^bsub>G\<^esub> (int n) = x (^)\<^bsub>G\<^esub> n"
+by(simp add: int_pow_def nat_pow_def)
+
 locale monoid =
   fixes G (structure)
   assumes m_closed [intro, simp]:
@@ -187,6 +190,9 @@
   with G show ?thesis by (simp del: r_one add: m_assoc Units_closed)
 qed
 
+lemma (in monoid) carrier_not_empty: "carrier G \<noteq> {}"
+by auto
+
 text \<open>Power\<close>
 
 lemma (in monoid) nat_pow_closed [intro, simp]:
@@ -434,7 +440,16 @@
     by (auto simp add: int_pow_def2 inv_solve_left inv_solve_right nat_add_distrib [symmetric] nat_pow_mult )
 qed
 
- 
+lemma (in group) int_pow_diff:
+  "x \<in> carrier G \<Longrightarrow> x (^) (n - m :: int) = x (^) n \<otimes> inv (x (^) m)"
+by(simp only: diff_conv_add_uminus int_pow_mult int_pow_neg)
+
+lemma (in group) inj_on_multc: "c \<in> carrier G \<Longrightarrow> inj_on (\<lambda>x. x \<otimes> c) (carrier G)"
+by(simp add: inj_on_def)
+
+lemma (in group) inj_on_cmult: "c \<in> carrier G \<Longrightarrow> inj_on (\<lambda>x. c \<otimes> x) (carrier G)"
+by(simp add: inj_on_def)
+
 subsection \<open>Subgroups\<close>
 
 locale subgroup =