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.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.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.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.135
1.136  lemma diff_self [simp]: "a - a = 0"
1.137    using right_minus [of a] by simp
1.138
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.153
1.154  lemma minus_add_cancel [simp]: "- a + (a + b) = b"
1.156 @@ -413,12 +468,7 @@