src/HOL/Groups.thy
changeset 54868 bab6cade3cc5
parent 54703 499f92dc6e45
child 56950 c49edf06f8e4
     1.1 --- a/src/HOL/Groups.thy	Thu Dec 26 22:47:49 2013 +0100
     1.2 +++ b/src/HOL/Groups.thy	Fri Dec 27 14:35:14 2013 +0100
     1.3 @@ -90,10 +90,13 @@
     1.4  locale comm_monoid = abel_semigroup +
     1.5    fixes z :: 'a ("1")
     1.6    assumes comm_neutral: "a * 1 = a"
     1.7 +begin
     1.8  
     1.9 -sublocale comm_monoid < monoid
    1.10 +sublocale monoid
    1.11    by default (simp_all add: commute comm_neutral)
    1.12  
    1.13 +end
    1.14 +
    1.15  
    1.16  subsection {* Generic operations *}
    1.17  
    1.18 @@ -148,19 +151,20 @@
    1.19  
    1.20  class semigroup_add = plus +
    1.21    assumes add_assoc [algebra_simps, field_simps]: "(a + b) + c = a + (b + c)"
    1.22 +begin
    1.23  
    1.24 -sublocale semigroup_add < add!: semigroup plus
    1.25 +sublocale add!: semigroup plus
    1.26    by default (fact add_assoc)
    1.27  
    1.28 +end
    1.29 +
    1.30  class ab_semigroup_add = semigroup_add +
    1.31    assumes add_commute [algebra_simps, field_simps]: "a + b = b + a"
    1.32 +begin
    1.33  
    1.34 -sublocale ab_semigroup_add < add!: abel_semigroup plus
    1.35 +sublocale add!: abel_semigroup plus
    1.36    by default (fact add_commute)
    1.37  
    1.38 -context ab_semigroup_add
    1.39 -begin
    1.40 -
    1.41  lemmas add_left_commute [algebra_simps, field_simps] = add.left_commute
    1.42  
    1.43  theorems add_ac = add_assoc add_commute add_left_commute
    1.44 @@ -171,19 +175,20 @@
    1.45  
    1.46  class semigroup_mult = times +
    1.47    assumes mult_assoc [algebra_simps, field_simps]: "(a * b) * c = a * (b * c)"
    1.48 +begin
    1.49  
    1.50 -sublocale semigroup_mult < mult!: semigroup times
    1.51 +sublocale mult!: semigroup times
    1.52    by default (fact mult_assoc)
    1.53  
    1.54 +end
    1.55 +
    1.56  class ab_semigroup_mult = semigroup_mult +
    1.57    assumes mult_commute [algebra_simps, field_simps]: "a * b = b * a"
    1.58 +begin
    1.59  
    1.60 -sublocale ab_semigroup_mult < mult!: abel_semigroup times
    1.61 +sublocale mult!: abel_semigroup times
    1.62    by default (fact mult_commute)
    1.63  
    1.64 -context ab_semigroup_mult
    1.65 -begin
    1.66 -
    1.67  lemmas mult_left_commute [algebra_simps, field_simps] = mult.left_commute
    1.68  
    1.69  theorems mult_ac = mult_assoc mult_commute mult_left_commute
    1.70 @@ -195,22 +200,28 @@
    1.71  class monoid_add = zero + semigroup_add +
    1.72    assumes add_0_left: "0 + a = a"
    1.73      and add_0_right: "a + 0 = a"
    1.74 +begin
    1.75  
    1.76 -sublocale monoid_add < add!: monoid plus 0
    1.77 +sublocale add!: monoid plus 0
    1.78    by default (fact add_0_left add_0_right)+
    1.79  
    1.80 +end
    1.81 +
    1.82  lemma zero_reorient: "0 = x \<longleftrightarrow> x = 0"
    1.83 -by (rule eq_commute)
    1.84 +  by (fact eq_commute)
    1.85  
    1.86  class comm_monoid_add = zero + ab_semigroup_add +
    1.87    assumes add_0: "0 + a = a"
    1.88 +begin
    1.89  
    1.90 -sublocale comm_monoid_add < add!: comm_monoid plus 0
    1.91 +sublocale add!: comm_monoid plus 0
    1.92    by default (insert add_0, simp add: ac_simps)
    1.93  
    1.94 -subclass (in comm_monoid_add) monoid_add
    1.95 +subclass monoid_add
    1.96    by default (fact add.left_neutral add.right_neutral)+
    1.97  
    1.98 +end
    1.99 +
   1.100  class comm_monoid_diff = comm_monoid_add + minus +
   1.101    assumes diff_zero [simp]: "a - 0 = a"
   1.102      and zero_diff [simp]: "0 - a = 0"
   1.103 @@ -265,22 +276,28 @@
   1.104  class monoid_mult = one + semigroup_mult +
   1.105    assumes mult_1_left: "1 * a  = a"
   1.106      and mult_1_right: "a * 1 = a"
   1.107 +begin
   1.108  
   1.109 -sublocale monoid_mult < mult!: monoid times 1
   1.110 +sublocale mult!: monoid times 1
   1.111    by default (fact mult_1_left mult_1_right)+
   1.112  
   1.113 +end
   1.114 +
   1.115  lemma one_reorient: "1 = x \<longleftrightarrow> x = 1"
   1.116 -by (rule eq_commute)
   1.117 +  by (fact eq_commute)
   1.118  
   1.119  class comm_monoid_mult = one + ab_semigroup_mult +
   1.120    assumes mult_1: "1 * a = a"
   1.121 +begin
   1.122  
   1.123 -sublocale comm_monoid_mult < mult!: comm_monoid times 1
   1.124 +sublocale mult!: comm_monoid times 1
   1.125    by default (insert mult_1, simp add: ac_simps)
   1.126  
   1.127 -subclass (in comm_monoid_mult) monoid_mult
   1.128 +subclass monoid_mult
   1.129    by default (fact mult.left_neutral mult.right_neutral)+
   1.130  
   1.131 +end
   1.132 +
   1.133  class cancel_semigroup_add = semigroup_add +
   1.134    assumes add_left_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
   1.135    assumes add_right_imp_eq: "b + a = c + a \<Longrightarrow> b = c"