src/HOL/Groups.thy
changeset 63364 4fa441c2f20c
parent 63325 1086d56cde86
child 63456 3365c8ec67bd
     1.1 --- a/src/HOL/Groups.thy	Sat Jul 02 08:41:05 2016 +0200
     1.2 +++ b/src/HOL/Groups.thy	Sat Jul 02 08:41:05 2016 +0200
     1.3 @@ -78,6 +78,83 @@
     1.4  
     1.5  end
     1.6  
     1.7 +locale group = semigroup +
     1.8 +  fixes z :: 'a ("\<^bold>1")
     1.9 +  fixes inverse :: "'a \<Rightarrow> 'a"
    1.10 +  assumes group_left_neutral: "\<^bold>1 \<^bold>* a = a"
    1.11 +  assumes left_inverse [simp]:  "inverse a \<^bold>* a = \<^bold>1"
    1.12 +begin
    1.13 +
    1.14 +lemma left_cancel: "a \<^bold>* b = a \<^bold>* c \<longleftrightarrow> b = c"
    1.15 +proof
    1.16 +  assume "a \<^bold>* b = a \<^bold>* c"
    1.17 +  then have "inverse a \<^bold>* (a \<^bold>* b) = inverse a \<^bold>* (a \<^bold>* c)" by simp
    1.18 +  then have "(inverse a \<^bold>* a) \<^bold>* b = (inverse a \<^bold>* a) \<^bold>* c"
    1.19 +    by (simp only: assoc)
    1.20 +  then show "b = c" by (simp add: group_left_neutral)
    1.21 +qed simp
    1.22 +
    1.23 +sublocale monoid
    1.24 +proof
    1.25 +  fix a
    1.26 +  have "inverse a \<^bold>* a = \<^bold>1" by simp
    1.27 +  then have "inverse a \<^bold>* (a \<^bold>* \<^bold>1) = inverse a \<^bold>* a"
    1.28 +    by (simp add: group_left_neutral assoc [symmetric])
    1.29 +  with left_cancel show "a \<^bold>* \<^bold>1 = a"
    1.30 +    by (simp only: left_cancel)
    1.31 +qed (fact group_left_neutral)
    1.32 +
    1.33 +lemma inverse_unique:
    1.34 +  assumes "a \<^bold>* b = \<^bold>1"
    1.35 +  shows "inverse a = b"
    1.36 +proof -
    1.37 +  from assms have "inverse a \<^bold>* (a \<^bold>* b) = inverse a"
    1.38 +    by simp
    1.39 +  then show ?thesis
    1.40 +    by (simp add: assoc [symmetric])
    1.41 +qed
    1.42 +
    1.43 +lemma inverse_neutral [simp]:
    1.44 +  "inverse \<^bold>1 = \<^bold>1"
    1.45 +  by (rule inverse_unique) simp
    1.46 +
    1.47 +lemma inverse_inverse [simp]:
    1.48 +  "inverse (inverse a) = a"
    1.49 +  by (rule inverse_unique) simp
    1.50 +
    1.51 +lemma right_inverse [simp]:
    1.52 +  "a \<^bold>* inverse a = \<^bold>1"
    1.53 +proof -
    1.54 +  have "a \<^bold>* inverse a = inverse (inverse a) \<^bold>* inverse a"
    1.55 +    by simp
    1.56 +  also have "\<dots> = \<^bold>1"
    1.57 +    by (rule left_inverse)
    1.58 +  then show ?thesis by simp
    1.59 +qed
    1.60 +
    1.61 +lemma inverse_distrib_swap:
    1.62 +  "inverse (a \<^bold>* b) = inverse b \<^bold>* inverse a"
    1.63 +proof (rule inverse_unique)
    1.64 +  have "a \<^bold>* b \<^bold>* (inverse b \<^bold>* inverse a) =
    1.65 +    a \<^bold>* (b \<^bold>* inverse b) \<^bold>* inverse a"
    1.66 +    by (simp only: assoc)
    1.67 +  also have "\<dots> = \<^bold>1"
    1.68 +    by simp
    1.69 +  finally show "a \<^bold>* b \<^bold>* (inverse b \<^bold>* inverse a) = \<^bold>1" .
    1.70 +qed
    1.71 +
    1.72 +lemma right_cancel:
    1.73 +  "b \<^bold>* a = c \<^bold>* a \<longleftrightarrow> b = c"
    1.74 +proof
    1.75 +  assume "b \<^bold>* a = c \<^bold>* a"
    1.76 +  then have "b \<^bold>* a \<^bold>* inverse a= c \<^bold>* a \<^bold>* inverse a"
    1.77 +    by simp
    1.78 +  then show "b = c"
    1.79 +    by (simp add: assoc)
    1.80 +qed simp
    1.81 +
    1.82 +end
    1.83 +
    1.84  
    1.85  subsection \<open>Generic operations\<close>
    1.86  
    1.87 @@ -348,57 +425,35 @@
    1.88  subsection \<open>Groups\<close>
    1.89  
    1.90  class group_add = minus + uminus + monoid_add +
    1.91 -  assumes left_minus [simp]: "- a + a = 0"
    1.92 +  assumes left_minus: "- a + a = 0"
    1.93    assumes add_uminus_conv_diff [simp]: "a + (- b) = a - b"
    1.94  begin
    1.95  
    1.96  lemma diff_conv_add_uminus: "a - b = a + (- b)"
    1.97    by simp
    1.98  
    1.99 +sublocale add: group plus 0 uminus
   1.100 +  by standard (simp_all add: left_minus)
   1.101 +
   1.102  lemma minus_unique:
   1.103    assumes "a + b = 0"
   1.104    shows "- a = b"
   1.105 -proof -
   1.106 -  from assms have "- a = - a + (a + b)" by simp
   1.107 -  also have "\<dots> = b" by (simp add: add.assoc [symmetric])
   1.108 -  finally show ?thesis .
   1.109 -qed
   1.110 +  using assms by (fact add.inverse_unique)
   1.111  
   1.112 -lemma minus_zero [simp]: "- 0 = 0"
   1.113 -proof -
   1.114 -  have "0 + 0 = 0" by (rule add_0_right)
   1.115 -  then show "- 0 = 0" by (rule minus_unique)
   1.116 -qed
   1.117 +lemma minus_zero: "- 0 = 0"
   1.118 +  by (fact add.inverse_neutral)
   1.119  
   1.120 -lemma minus_minus [simp]: "- (- a) = a"
   1.121 -proof -
   1.122 -  have "- a + a = 0" by (rule left_minus)
   1.123 -  then show "- (- a) = a" by (rule minus_unique)
   1.124 -qed
   1.125 +lemma minus_minus: "- (- a) = a"
   1.126 +  by (fact add.inverse_inverse)
   1.127  
   1.128  lemma right_minus: "a + - a = 0"
   1.129 -proof -
   1.130 -  have "a + - a = - (- a) + - a" by simp
   1.131 -  also have "\<dots> = 0" by (rule left_minus)
   1.132 -  finally show ?thesis .
   1.133 -qed
   1.134 +  by (fact add.right_inverse)
   1.135  
   1.136  lemma diff_self [simp]: "a - a = 0"
   1.137    using right_minus [of a] by simp
   1.138  
   1.139  subclass cancel_semigroup_add
   1.140 -proof
   1.141 -  fix a b c :: 'a
   1.142 -  assume "a + b = a + c"
   1.143 -  then have "- a + a + b = - a + a + c"
   1.144 -    unfolding add.assoc by simp
   1.145 -  then show "b = c" by simp
   1.146 -next
   1.147 -  fix a b c :: 'a
   1.148 -  assume "b + a = c + a"
   1.149 -  then have "b + a + - a = c + a  + - a" by simp
   1.150 -  then show "b = c" unfolding add.assoc by simp
   1.151 -qed
   1.152 +  by standard (simp_all add: add.left_cancel add.right_cancel)
   1.153  
   1.154  lemma minus_add_cancel [simp]: "- a + (a + b) = b"
   1.155    by (simp add: add.assoc [symmetric])
   1.156 @@ -413,12 +468,7 @@
   1.157    by (simp only: diff_conv_add_uminus add.assoc) simp
   1.158  
   1.159  lemma minus_add: "- (a + b) = - b + - a"
   1.160 -proof -
   1.161 -  have "(a + b) + (- b + - a) = 0"
   1.162 -    by (simp only: add.assoc add_minus_cancel) simp
   1.163 -  then show "- (a + b) = - b + - a"
   1.164 -    by (rule minus_unique)
   1.165 -qed
   1.166 +  by (fact add.inverse_distrib_swap)
   1.167  
   1.168  lemma right_minus_eq [simp]: "a - b = 0 \<longleftrightarrow> a = b"
   1.169  proof