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