add lemmas about monoids and groups
authorAndreas Lochbihler
Wed Nov 11 09:06:30 2015 +0100 (2015-11-11)
changeset 616288dd2bd4fe30b
parent 61626 c304402cc3df
child 61629 90f54d9e63f2
add lemmas about monoids and groups
src/HOL/Algebra/Coset.thy
src/HOL/Algebra/Group.thy
     1.1 --- a/src/HOL/Algebra/Coset.thy	Tue Nov 10 23:41:20 2015 +0100
     1.2 +++ b/src/HOL/Algebra/Coset.thy	Wed Nov 11 09:06:30 2015 +0100
     1.3 @@ -759,6 +759,9 @@
     1.4    order :: "('a, 'b) monoid_scheme \<Rightarrow> nat"
     1.5    where "order S = card (carrier S)"
     1.6  
     1.7 +lemma (in monoid) order_gt_0_iff_finite: "0 < order G \<longleftrightarrow> finite (carrier G)"
     1.8 +by(auto simp add: order_def card_gt_0_iff)
     1.9 +
    1.10  lemma (in group) rcosets_part_G:
    1.11    assumes "subgroup H G"
    1.12    shows "\<Union>(rcosets H) = carrier G"
     2.1 --- a/src/HOL/Algebra/Group.thy	Tue Nov 10 23:41:20 2015 +0100
     2.2 +++ b/src/HOL/Algebra/Group.thy	Wed Nov 11 09:06:30 2015 +0100
     2.3 @@ -44,6 +44,9 @@
     2.4      in if z < 0 then inv\<^bsub>G\<^esub> (p (nat (-z))) else p (nat z))"
     2.5  end
     2.6  
     2.7 +lemma int_pow_int: "x (^)\<^bsub>G\<^esub> (int n) = x (^)\<^bsub>G\<^esub> n"
     2.8 +by(simp add: int_pow_def nat_pow_def)
     2.9 +
    2.10  locale monoid =
    2.11    fixes G (structure)
    2.12    assumes m_closed [intro, simp]:
    2.13 @@ -187,6 +190,9 @@
    2.14    with G show ?thesis by (simp del: r_one add: m_assoc Units_closed)
    2.15  qed
    2.16  
    2.17 +lemma (in monoid) carrier_not_empty: "carrier G \<noteq> {}"
    2.18 +by auto
    2.19 +
    2.20  text \<open>Power\<close>
    2.21  
    2.22  lemma (in monoid) nat_pow_closed [intro, simp]:
    2.23 @@ -434,7 +440,16 @@
    2.24      by (auto simp add: int_pow_def2 inv_solve_left inv_solve_right nat_add_distrib [symmetric] nat_pow_mult )
    2.25  qed
    2.26  
    2.27 - 
    2.28 +lemma (in group) int_pow_diff:
    2.29 +  "x \<in> carrier G \<Longrightarrow> x (^) (n - m :: int) = x (^) n \<otimes> inv (x (^) m)"
    2.30 +by(simp only: diff_conv_add_uminus int_pow_mult int_pow_neg)
    2.31 +
    2.32 +lemma (in group) inj_on_multc: "c \<in> carrier G \<Longrightarrow> inj_on (\<lambda>x. x \<otimes> c) (carrier G)"
    2.33 +by(simp add: inj_on_def)
    2.34 +
    2.35 +lemma (in group) inj_on_cmult: "c \<in> carrier G \<Longrightarrow> inj_on (\<lambda>x. c \<otimes> x) (carrier G)"
    2.36 +by(simp add: inj_on_def)
    2.37 +
    2.38  subsection \<open>Subgroups\<close>
    2.39  
    2.40  locale subgroup =