src/HOL/Groups.thy
 changeset 63588 d0e2bad67bd4 parent 63456 3365c8ec67bd child 63680 6e1e8b5abbfa
```     1.1 --- a/src/HOL/Groups.thy	Tue Aug 02 21:04:52 2016 +0200
1.2 +++ b/src/HOL/Groups.thy	Tue Aug 02 21:05:34 2016 +0200
1.3 @@ -1,48 +1,46 @@
1.4 -(*  Title:   HOL/Groups.thy
1.5 -    Author:  Gertrud Bauer, Steven Obua, Lawrence C Paulson, Markus Wenzel, Jeremy Avigad
1.6 +(*  Title:      HOL/Groups.thy
1.7 +    Author:     Gertrud Bauer
1.8 +    Author:     Steven Obua
1.9 +    Author:     Lawrence C Paulson
1.10 +    Author:     Markus Wenzel
1.11 +    Author:     Jeremy Avigad
1.12  *)
1.13
1.14  section \<open>Groups, also combined with orderings\<close>
1.15
1.16  theory Groups
1.17 -imports Orderings
1.18 +  imports Orderings
1.19  begin
1.20
1.21  subsection \<open>Dynamic facts\<close>
1.22
1.23  named_theorems ac_simps "associativity and commutativity simplification rules"
1.24 -
1.25 +  and algebra_simps "algebra simplification rules"
1.26 +  and field_simps "algebra simplification rules for fields"
1.27
1.28  text \<open>
1.29 -  The rewrites accumulated in \<open>algebra_simps\<close> deal with the
1.30 -  classical algebraic structures of groups, rings and family. They simplify
1.31 -  terms by multiplying everything out (in case of a ring) and bringing sums and
1.32 -  products into a canonical form (by ordered rewriting). As a result it decides
1.33 -  group and ring equalities but also helps with inequalities.
1.34 -
1.35 -  Of course it also works for fields, but it knows nothing about multiplicative
1.36 -  inverses or division. This is catered for by \<open>field_simps\<close>.
1.37 -\<close>
1.38 +  The rewrites accumulated in \<open>algebra_simps\<close> deal with the classical
1.39 +  algebraic structures of groups, rings and family. They simplify terms by
1.40 +  multiplying everything out (in case of a ring) and bringing sums and
1.41 +  products into a canonical form (by ordered rewriting). As a result it
1.42 +  decides group and ring equalities but also helps with inequalities.
1.43
1.44 -named_theorems algebra_simps "algebra simplification rules"
1.45 -
1.46 +  Of course it also works for fields, but it knows nothing about
1.47 +  multiplicative inverses or division. This is catered for by \<open>field_simps\<close>.
1.48
1.49 -text \<open>
1.50 -  Lemmas \<open>field_simps\<close> multiply with denominators in (in)equations
1.51 -  if they can be proved to be non-zero (for equations) or positive/negative
1.52 -  (for inequations). Can be too aggressive and is therefore separate from the
1.53 -  more benign \<open>algebra_simps\<close>.
1.54 +  Facts in \<open>field_simps\<close> multiply with denominators in (in)equations if they
1.55 +  can be proved to be non-zero (for equations) or positive/negative (for
1.56 +  inequalities). Can be too aggressive and is therefore separate from the more
1.57 +  benign \<open>algebra_simps\<close>.
1.58  \<close>
1.59
1.60 -named_theorems field_simps "algebra simplification rules for fields"
1.61 -
1.62
1.63  subsection \<open>Abstract structures\<close>
1.64
1.65  text \<open>
1.66 -  These locales provide basic structures for interpretation into
1.67 -  bigger structures;  extensions require careful thinking, otherwise
1.68 -  undesired effects may occur due to interpretation.
1.69 +  These locales provide basic structures for interpretation into bigger
1.70 +  structures; extensions require careful thinking, otherwise undesired effects
1.71 +  may occur due to interpretation.
1.72  \<close>
1.73
1.74  locale semigroup =
1.75 @@ -114,16 +112,13 @@
1.76      by (simp add: assoc [symmetric])
1.77  qed
1.78
1.79 -lemma inverse_neutral [simp]:
1.80 -  "inverse \<^bold>1 = \<^bold>1"
1.81 +lemma inverse_neutral [simp]: "inverse \<^bold>1 = \<^bold>1"
1.82    by (rule inverse_unique) simp
1.83
1.84 -lemma inverse_inverse [simp]:
1.85 -  "inverse (inverse a) = a"
1.86 +lemma inverse_inverse [simp]: "inverse (inverse a) = a"
1.87    by (rule inverse_unique) simp
1.88
1.89 -lemma right_inverse [simp]:
1.90 -  "a \<^bold>* inverse a = \<^bold>1"
1.91 +lemma right_inverse [simp]: "a \<^bold>* inverse a = \<^bold>1"
1.92  proof -
1.93    have "a \<^bold>* inverse a = inverse (inverse a) \<^bold>* inverse a"
1.94      by simp
1.95 @@ -132,8 +127,7 @@
1.96    then show ?thesis by simp
1.97  qed
1.98
1.99 -lemma inverse_distrib_swap:
1.100 -  "inverse (a \<^bold>* b) = inverse b \<^bold>* inverse a"
1.101 +lemma inverse_distrib_swap: "inverse (a \<^bold>* b) = inverse b \<^bold>* inverse a"
1.102  proof (rule inverse_unique)
1.103    have "a \<^bold>* b \<^bold>* (inverse b \<^bold>* inverse a) =
1.104      a \<^bold>* (b \<^bold>* inverse b) \<^bold>* inverse a"
1.105 @@ -143,8 +137,7 @@
1.106    finally show "a \<^bold>* b \<^bold>* (inverse b \<^bold>* inverse a) = \<^bold>1" .
1.107  qed
1.108
1.109 -lemma right_cancel:
1.110 -  "b \<^bold>* a = c \<^bold>* a \<longleftrightarrow> b = c"
1.111 +lemma right_cancel: "b \<^bold>* a = c \<^bold>* a \<longleftrightarrow> b = c"
1.112  proof
1.113    assume "b \<^bold>* a = c \<^bold>* a"
1.114    then have "b \<^bold>* a \<^bold>* inverse a= c \<^bold>* a \<^bold>* inverse a"
1.115 @@ -435,10 +428,8 @@
1.116  sublocale add: group plus 0 uminus
1.117    by standard (simp_all add: left_minus)
1.118
1.119 -lemma minus_unique:
1.120 -  assumes "a + b = 0"
1.121 -  shows "- a = b"
1.122 -  using assms by (fact add.inverse_unique)
1.123 +lemma minus_unique: "a + b = 0 \<Longrightarrow> - a = b"
1.124 +  by (fact add.inverse_unique)
1.125
1.126  lemma minus_zero: "- 0 = 0"
1.127    by (fact add.inverse_neutral)
1.128 @@ -701,8 +692,8 @@
1.129
1.130  lemma add_le_cancel_left [simp]: "c + a \<le> c + b \<longleftrightarrow> a \<le> b"
1.131    apply auto
1.132 -  apply (drule add_le_imp_le_left)
1.133 -  apply (simp_all add: add_left_mono)
1.134 +   apply (drule add_le_imp_le_left)
1.135 +   apply (simp_all add: add_left_mono)
1.136    done
1.137
1.138  lemma add_le_cancel_right [simp]: "a + c \<le> b + c \<longleftrightarrow> a \<le> b"
1.139 @@ -803,36 +794,28 @@
1.140  class ordered_ab_semigroup_monoid_add_imp_le = monoid_add + ordered_ab_semigroup_add_imp_le
1.141  begin
1.142
1.143 -lemma add_less_same_cancel1 [simp]:
1.144 -  "b + a < b \<longleftrightarrow> a < 0"
1.145 +lemma add_less_same_cancel1 [simp]: "b + a < b \<longleftrightarrow> a < 0"
1.146    using add_less_cancel_left [of _ _ 0] by simp
1.147
1.148 -lemma add_less_same_cancel2 [simp]:
1.149 -  "a + b < b \<longleftrightarrow> a < 0"
1.150 +lemma add_less_same_cancel2 [simp]: "a + b < b \<longleftrightarrow> a < 0"
1.151    using add_less_cancel_right [of _ _ 0] by simp
1.152
1.153 -lemma less_add_same_cancel1 [simp]:
1.154 -  "a < a + b \<longleftrightarrow> 0 < b"
1.155 +lemma less_add_same_cancel1 [simp]: "a < a + b \<longleftrightarrow> 0 < b"
1.156    using add_less_cancel_left [of _ 0] by simp
1.157
1.158 -lemma less_add_same_cancel2 [simp]:
1.159 -  "a < b + a \<longleftrightarrow> 0 < b"
1.160 +lemma less_add_same_cancel2 [simp]: "a < b + a \<longleftrightarrow> 0 < b"
1.161    using add_less_cancel_right [of 0] by simp
1.162
1.163 -lemma add_le_same_cancel1 [simp]:
1.164 -  "b + a \<le> b \<longleftrightarrow> a \<le> 0"
1.165 +lemma add_le_same_cancel1 [simp]: "b + a \<le> b \<longleftrightarrow> a \<le> 0"
1.166    using add_le_cancel_left [of _ _ 0] by simp
1.167
1.168 -lemma add_le_same_cancel2 [simp]:
1.169 -  "a + b \<le> b \<longleftrightarrow> a \<le> 0"
1.170 +lemma add_le_same_cancel2 [simp]: "a + b \<le> b \<longleftrightarrow> a \<le> 0"
1.171    using add_le_cancel_right [of _ _ 0] by simp
1.172
1.173 -lemma le_add_same_cancel1 [simp]:
1.174 -  "a \<le> a + b \<longleftrightarrow> 0 \<le> b"
1.175 +lemma le_add_same_cancel1 [simp]: "a \<le> a + b \<longleftrightarrow> 0 \<le> b"
1.176    using add_le_cancel_left [of _ 0] by simp
1.177
1.178 -lemma le_add_same_cancel2 [simp]:
1.179 -  "a \<le> b + a \<longleftrightarrow> 0 \<le> b"
1.180 +lemma le_add_same_cancel2 [simp]: "a \<le> b + a \<longleftrightarrow> 0 \<le> b"
1.181    using add_le_cancel_right [of 0] by simp
1.182
1.183  subclass cancel_comm_monoid_add
1.184 @@ -911,7 +894,7 @@
1.185
1.186  lemma less_minus_iff: "a < - b \<longleftrightarrow> b < - a"
1.187  proof -
1.188 -  have "- (-a) < - b \<longleftrightarrow> b < - a"
1.189 +  have "- (- a) < - b \<longleftrightarrow> b < - a"
1.190      by (rule neg_less_iff_less)
1.191    then show ?thesis by simp
1.192  qed
1.193 @@ -925,12 +908,12 @@
1.194
1.195  lemma le_minus_iff: "a \<le> - b \<longleftrightarrow> b \<le> - a"
1.196  proof -
1.197 -  have mm: "- (- a) < -b \<Longrightarrow> - (- b) < -a" for a b :: 'a
1.198 +  have mm: "- (- a) < - b \<Longrightarrow> - (- b) < -a" for a b :: 'a
1.199      by (simp only: minus_less_iff)
1.200 -  have "- (- a) \<le> -b \<longleftrightarrow> b \<le> - a"
1.201 +  have "- (- a) \<le> - b \<longleftrightarrow> b \<le> - a"
1.202      apply (auto simp only: le_less)
1.203 -    apply (drule mm)
1.204 -    apply (simp_all)
1.205 +      apply (drule mm)
1.206 +      apply (simp_all)
1.207      apply (drule mm[simplified], assumption)
1.208      done
1.209    then show ?thesis by simp
1.210 @@ -1039,11 +1022,11 @@
1.211    proof (rule ccontr)
1.212      assume *: "\<not> ?thesis"
1.213      then have "b \<le> a" by (simp add: linorder_not_le)
1.214 -    then have le2: "c + b \<le> c + a" by (rule add_left_mono)
1.215 -    have "a = b"
1.216 -      apply (insert le1 le2)
1.217 +    then have "c + b \<le> c + a" by (rule add_left_mono)
1.218 +    with le1 have "a = b"
1.219 +      apply -
1.220        apply (drule antisym)
1.221 -      apply simp_all
1.222 +       apply simp_all
1.223        done
1.224      with * show False
1.225        by (simp add: linorder_not_le [symmetric])
1.226 @@ -1117,8 +1100,8 @@
1.227
1.228  lemma double_zero_sym [simp]: "0 = a + a \<longleftrightarrow> a = 0"
1.229    apply (rule iffI)
1.230 -  apply (drule sym)
1.231 -  apply simp_all
1.232 +   apply (drule sym)
1.233 +   apply simp_all
1.234    done
1.235
1.236  lemma zero_less_double_add_iff_zero_less_single_add [simp]: "0 < a + a \<longleftrightarrow> 0 < a"
1.237 @@ -1342,7 +1325,7 @@
1.238    fixes x::"'a::{dense_linorder,ordered_ab_group_add_abs}"
1.239    shows "(\<And>e. 0 < e \<Longrightarrow> \<bar>x\<bar> \<le> e) \<Longrightarrow> x = 0"
1.240    apply (cases "\<bar>x\<bar> = 0")
1.241 -  apply simp
1.242 +   apply simp
1.243    apply (simp only: zero_less_abs_iff [symmetric])
1.244    apply (drule dense)
1.245    apply (auto simp add: not_less [symmetric])
1.246 @@ -1402,7 +1385,7 @@
1.247  begin
1.248
1.249  context
1.250 -  fixes a b
1.251 +  fixes a b :: 'a
1.252    assumes le: "a \<le> b"
1.253  begin
1.254
```