src/HOL/Groups.thy
changeset 51546 2e26df807dc7
parent 49690 a6814de45b69
child 52143 36ffe23b25f8
     1.1 --- a/src/HOL/Groups.thy	Tue Mar 26 20:55:21 2013 +0100
     1.2 +++ b/src/HOL/Groups.thy	Tue Mar 26 21:53:56 2013 +0100
     1.3 @@ -91,8 +91,8 @@
     1.4    fixes z :: 'a ("1")
     1.5    assumes comm_neutral: "a * 1 = a"
     1.6  
     1.7 -sublocale comm_monoid < monoid proof
     1.8 -qed (simp_all add: commute comm_neutral)
     1.9 +sublocale comm_monoid < monoid
    1.10 +  by default (simp_all add: commute comm_neutral)
    1.11  
    1.12  
    1.13  subsection {* Generic operations *}
    1.14 @@ -151,14 +151,14 @@
    1.15  class semigroup_add = plus +
    1.16    assumes add_assoc [algebra_simps, field_simps]: "(a + b) + c = a + (b + c)"
    1.17  
    1.18 -sublocale semigroup_add < add!: semigroup plus proof
    1.19 -qed (fact add_assoc)
    1.20 +sublocale semigroup_add < add!: semigroup plus
    1.21 +  by default (fact add_assoc)
    1.22  
    1.23  class ab_semigroup_add = semigroup_add +
    1.24    assumes add_commute [algebra_simps, field_simps]: "a + b = b + a"
    1.25  
    1.26 -sublocale ab_semigroup_add < add!: abel_semigroup plus proof
    1.27 -qed (fact add_commute)
    1.28 +sublocale ab_semigroup_add < add!: abel_semigroup plus
    1.29 +  by default (fact add_commute)
    1.30  
    1.31  context ab_semigroup_add
    1.32  begin
    1.33 @@ -174,14 +174,14 @@
    1.34  class semigroup_mult = times +
    1.35    assumes mult_assoc [algebra_simps, field_simps]: "(a * b) * c = a * (b * c)"
    1.36  
    1.37 -sublocale semigroup_mult < mult!: semigroup times proof
    1.38 -qed (fact mult_assoc)
    1.39 +sublocale semigroup_mult < mult!: semigroup times
    1.40 +  by default (fact mult_assoc)
    1.41  
    1.42  class ab_semigroup_mult = semigroup_mult +
    1.43    assumes mult_commute [algebra_simps, field_simps]: "a * b = b * a"
    1.44  
    1.45 -sublocale ab_semigroup_mult < mult!: abel_semigroup times proof
    1.46 -qed (fact mult_commute)
    1.47 +sublocale ab_semigroup_mult < mult!: abel_semigroup times
    1.48 +  by default (fact mult_commute)
    1.49  
    1.50  context ab_semigroup_mult
    1.51  begin
    1.52 @@ -198,8 +198,8 @@
    1.53    assumes add_0_left: "0 + a = a"
    1.54      and add_0_right: "a + 0 = a"
    1.55  
    1.56 -sublocale monoid_add < add!: monoid plus 0 proof
    1.57 -qed (fact add_0_left add_0_right)+
    1.58 +sublocale monoid_add < add!: monoid plus 0
    1.59 +  by default (fact add_0_left add_0_right)+
    1.60  
    1.61  lemma zero_reorient: "0 = x \<longleftrightarrow> x = 0"
    1.62  by (rule eq_commute)
    1.63 @@ -207,11 +207,11 @@
    1.64  class comm_monoid_add = zero + ab_semigroup_add +
    1.65    assumes add_0: "0 + a = a"
    1.66  
    1.67 -sublocale comm_monoid_add < add!: comm_monoid plus 0 proof
    1.68 -qed (insert add_0, simp add: ac_simps)
    1.69 +sublocale comm_monoid_add < add!: comm_monoid plus 0
    1.70 +  by default (insert add_0, simp add: ac_simps)
    1.71  
    1.72 -subclass (in comm_monoid_add) monoid_add proof
    1.73 -qed (fact add.left_neutral add.right_neutral)+
    1.74 +subclass (in comm_monoid_add) monoid_add
    1.75 +  by default (fact add.left_neutral add.right_neutral)+
    1.76  
    1.77  class comm_monoid_diff = comm_monoid_add + minus +
    1.78    assumes diff_zero [simp]: "a - 0 = a"
    1.79 @@ -268,8 +268,8 @@
    1.80    assumes mult_1_left: "1 * a  = a"
    1.81      and mult_1_right: "a * 1 = a"
    1.82  
    1.83 -sublocale monoid_mult < mult!: monoid times 1 proof
    1.84 -qed (fact mult_1_left mult_1_right)+
    1.85 +sublocale monoid_mult < mult!: monoid times 1
    1.86 +  by default (fact mult_1_left mult_1_right)+
    1.87  
    1.88  lemma one_reorient: "1 = x \<longleftrightarrow> x = 1"
    1.89  by (rule eq_commute)
    1.90 @@ -277,11 +277,11 @@
    1.91  class comm_monoid_mult = one + ab_semigroup_mult +
    1.92    assumes mult_1: "1 * a = a"
    1.93  
    1.94 -sublocale comm_monoid_mult < mult!: comm_monoid times 1 proof
    1.95 -qed (insert mult_1, simp add: ac_simps)
    1.96 +sublocale comm_monoid_mult < mult!: comm_monoid times 1
    1.97 +  by default (insert mult_1, simp add: ac_simps)
    1.98  
    1.99 -subclass (in comm_monoid_mult) monoid_mult proof
   1.100 -qed (fact mult.left_neutral mult.right_neutral)+
   1.101 +subclass (in comm_monoid_mult) monoid_mult
   1.102 +  by default (fact mult.left_neutral mult.right_neutral)+
   1.103  
   1.104  class cancel_semigroup_add = semigroup_add +
   1.105    assumes add_left_imp_eq: "a + b = a + c \<Longrightarrow> b = c"