author  wenzelm 
Tue, 06 Oct 2015 15:14:28 +0200  
changeset 61337  4645502c3c64 
parent 61169  4de9ff3ea29a 
child 61378  3e04c9ca001a 
permissions  rwrr 
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35036
diff
changeset

1 
(* Title: HOL/Groups.thy 
29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
28823
diff
changeset

2 
Author: Gertrud Bauer, Steven Obua, Lawrence C Paulson, Markus Wenzel, Jeremy Avigad 
14738  3 
*) 
4 

60758  5 
section \<open>Groups, also combined with orderings\<close> 
14738  6 

35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35036
diff
changeset

7 
theory Groups 
35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

8 
imports Orderings 
15131  9 
begin 
14738  10 

60758  11 
subsection \<open>Dynamic facts\<close> 
35301
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

12 

57950  13 
named_theorems ac_simps "associativity and commutativity simplification rules" 
36343  14 

15 

60758  16 
text\<open>The rewrites accumulated in @{text algebra_simps} deal with the 
36348
89c54f51f55a
dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
haftmann
parents:
36343
diff
changeset

17 
classical algebraic structures of groups, rings and family. They simplify 
89c54f51f55a
dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
haftmann
parents:
36343
diff
changeset

18 
terms by multiplying everything out (in case of a ring) and bringing sums and 
89c54f51f55a
dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
haftmann
parents:
36343
diff
changeset

19 
products into a canonical form (by ordered rewriting). As a result it decides 
89c54f51f55a
dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
haftmann
parents:
36343
diff
changeset

20 
group and ring equalities but also helps with inequalities. 
89c54f51f55a
dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
haftmann
parents:
36343
diff
changeset

21 

89c54f51f55a
dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
haftmann
parents:
36343
diff
changeset

22 
Of course it also works for fields, but it knows nothing about multiplicative 
60758  23 
inverses or division. This is catered for by @{text field_simps}.\<close> 
36348
89c54f51f55a
dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
haftmann
parents:
36343
diff
changeset

24 

57950  25 
named_theorems algebra_simps "algebra simplification rules" 
35301
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

26 

90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

27 

60758  28 
text\<open>Lemmas @{text field_simps} multiply with denominators in (in)equations 
36348
89c54f51f55a
dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
haftmann
parents:
36343
diff
changeset

29 
if they can be proved to be nonzero (for equations) or positive/negative 
89c54f51f55a
dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
haftmann
parents:
36343
diff
changeset

30 
(for inequations). Can be too aggressive and is therefore separate from the 
60758  31 
more benign @{text algebra_simps}.\<close> 
35301
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

32 

57950  33 
named_theorems field_simps "algebra simplification rules for fields" 
35301
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

34 

90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

35 

60758  36 
subsection \<open>Abstract structures\<close> 
35301
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

37 

60758  38 
text \<open> 
35301
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

39 
These locales provide basic structures for interpretation into 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

40 
bigger structures; extensions require careful thinking, otherwise 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

41 
undesired effects may occur due to interpretation. 
60758  42 
\<close> 
35301
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

43 

90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

44 
locale semigroup = 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

45 
fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "*" 70) 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

46 
assumes assoc [ac_simps]: "a * b * c = a * (b * c)" 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

47 

90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

48 
locale abel_semigroup = semigroup + 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

49 
assumes commute [ac_simps]: "a * b = b * a" 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

50 
begin 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

51 

90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

52 
lemma left_commute [ac_simps]: 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

53 
"b * (a * c) = a * (b * c)" 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

54 
proof  
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

55 
have "(b * a) * c = (a * b) * c" 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

56 
by (simp only: commute) 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

57 
then show ?thesis 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

58 
by (simp only: assoc) 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

59 
qed 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

60 

90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

61 
end 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

62 

35720  63 
locale monoid = semigroup + 
35723
b6cf98f25c3f
tuned monoid locales and prefix of sublocale interpretations
haftmann
parents:
35720
diff
changeset

64 
fixes z :: 'a ("1") 
b6cf98f25c3f
tuned monoid locales and prefix of sublocale interpretations
haftmann
parents:
35720
diff
changeset

65 
assumes left_neutral [simp]: "1 * a = a" 
b6cf98f25c3f
tuned monoid locales and prefix of sublocale interpretations
haftmann
parents:
35720
diff
changeset

66 
assumes right_neutral [simp]: "a * 1 = a" 
35720  67 

68 
locale comm_monoid = abel_semigroup + 

35723
b6cf98f25c3f
tuned monoid locales and prefix of sublocale interpretations
haftmann
parents:
35720
diff
changeset

69 
fixes z :: 'a ("1") 
b6cf98f25c3f
tuned monoid locales and prefix of sublocale interpretations
haftmann
parents:
35720
diff
changeset

70 
assumes comm_neutral: "a * 1 = a" 
54868  71 
begin 
35720  72 

54868  73 
sublocale monoid 
61169  74 
by standard (simp_all add: commute comm_neutral) 
35720  75 

54868  76 
end 
77 

35301
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

78 

60758  79 
subsection \<open>Generic operations\<close> 
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

80 

8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

81 
class zero = 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

82 
fixes zero :: 'a ("0") 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

83 

8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

84 
class one = 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

85 
fixes one :: 'a ("1") 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

86 

36176
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
35828
diff
changeset

87 
hide_const (open) zero one 
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

88 

8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

89 
lemma Let_0 [simp]: "Let 0 f = f 0" 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

90 
unfolding Let_def .. 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

91 

8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

92 
lemma Let_1 [simp]: "Let 1 f = f 1" 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

93 
unfolding Let_def .. 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

94 

60758  95 
setup \<open> 
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

96 
Reorient_Proc.add 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

97 
(fn Const(@{const_name Groups.zero}, _) => true 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

98 
 Const(@{const_name Groups.one}, _) => true 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

99 
 _ => false) 
60758  100 
\<close> 
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

101 

8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

102 
simproc_setup reorient_zero ("0 = x") = Reorient_Proc.proc 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

103 
simproc_setup reorient_one ("1 = x") = Reorient_Proc.proc 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

104 

60758  105 
typed_print_translation \<open> 
42247
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42245
diff
changeset

106 
let 
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42245
diff
changeset

107 
fun tr' c = (c, fn ctxt => fn T => fn ts => 
52210
0226035df99d
more explicit Printer.type_emphasis, depending on show_type_emphasis;
wenzelm
parents:
52143
diff
changeset

108 
if null ts andalso Printer.type_emphasis ctxt T then 
42248  109 
Syntax.const @{syntax_const "_constrain"} $ Syntax.const c $ 
52210
0226035df99d
more explicit Printer.type_emphasis, depending on show_type_emphasis;
wenzelm
parents:
52143
diff
changeset

110 
Syntax_Phases.term_of_typ ctxt T 
0226035df99d
more explicit Printer.type_emphasis, depending on show_type_emphasis;
wenzelm
parents:
52143
diff
changeset

111 
else raise Match); 
42247
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42245
diff
changeset

112 
in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end; 
60758  113 
\<close>  \<open>show types that are presumably too general\<close> 
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

114 

8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

115 
class plus = 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

116 
fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "+" 65) 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

117 

8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

118 
class minus = 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

119 
fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "" 65) 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

120 

8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

121 
class uminus = 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

122 
fixes uminus :: "'a \<Rightarrow> 'a" (" _" [81] 80) 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

123 

8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

124 
class times = 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

125 
fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "*" 70) 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

126 

35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

127 

60758  128 
subsection \<open>Semigroups and Monoids\<close> 
14738  129 

22390  130 
class semigroup_add = plus + 
36348
89c54f51f55a
dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
haftmann
parents:
36343
diff
changeset

131 
assumes add_assoc [algebra_simps, field_simps]: "(a + b) + c = a + (b + c)" 
54868  132 
begin 
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

133 

54868  134 
sublocale add!: semigroup plus 
61169  135 
by standard (fact add_assoc) 
22390  136 

54868  137 
end 
138 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56950
diff
changeset

139 
hide_fact add_assoc 
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56950
diff
changeset

140 

22390  141 
class ab_semigroup_add = semigroup_add + 
36348
89c54f51f55a
dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
haftmann
parents:
36343
diff
changeset

142 
assumes add_commute [algebra_simps, field_simps]: "a + b = b + a" 
54868  143 
begin 
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

144 

54868  145 
sublocale add!: abel_semigroup plus 
61169  146 
by standard (fact add_commute) 
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

147 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56950
diff
changeset

148 
declare add.left_commute [algebra_simps, field_simps] 
25062  149 

61337  150 
lemmas add_ac = add.assoc add.commute add.left_commute 
57571
d38a98f496dd
reinstated popular add_ac and mult_ac to avoid needless incompatibilities in user space
nipkow
parents:
57514
diff
changeset

151 

25062  152 
end 
14738  153 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56950
diff
changeset

154 
hide_fact add_commute 
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56950
diff
changeset

155 

61337  156 
lemmas add_ac = add.assoc add.commute add.left_commute 
57571
d38a98f496dd
reinstated popular add_ac and mult_ac to avoid needless incompatibilities in user space
nipkow
parents:
57514
diff
changeset

157 

22390  158 
class semigroup_mult = times + 
36348
89c54f51f55a
dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
haftmann
parents:
36343
diff
changeset

159 
assumes mult_assoc [algebra_simps, field_simps]: "(a * b) * c = a * (b * c)" 
54868  160 
begin 
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

161 

54868  162 
sublocale mult!: semigroup times 
61169  163 
by standard (fact mult_assoc) 
14738  164 

54868  165 
end 
166 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56950
diff
changeset

167 
hide_fact mult_assoc 
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56950
diff
changeset

168 

22390  169 
class ab_semigroup_mult = semigroup_mult + 
36348
89c54f51f55a
dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
haftmann
parents:
36343
diff
changeset

170 
assumes mult_commute [algebra_simps, field_simps]: "a * b = b * a" 
54868  171 
begin 
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

172 

54868  173 
sublocale mult!: abel_semigroup times 
61169  174 
by standard (fact mult_commute) 
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

175 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56950
diff
changeset

176 
declare mult.left_commute [algebra_simps, field_simps] 
25062  177 

61337  178 
lemmas mult_ac = mult.assoc mult.commute mult.left_commute 
57571
d38a98f496dd
reinstated popular add_ac and mult_ac to avoid needless incompatibilities in user space
nipkow
parents:
57514
diff
changeset

179 

23181  180 
end 
14738  181 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56950
diff
changeset

182 
hide_fact mult_commute 
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56950
diff
changeset

183 

61337  184 
lemmas mult_ac = mult.assoc mult.commute mult.left_commute 
57571
d38a98f496dd
reinstated popular add_ac and mult_ac to avoid needless incompatibilities in user space
nipkow
parents:
57514
diff
changeset

185 

23085  186 
class monoid_add = zero + semigroup_add + 
35720  187 
assumes add_0_left: "0 + a = a" 
188 
and add_0_right: "a + 0 = a" 

54868  189 
begin 
35720  190 

54868  191 
sublocale add!: monoid plus 0 
61169  192 
by standard (fact add_0_left add_0_right)+ 
23085  193 

54868  194 
end 
195 

26071  196 
lemma zero_reorient: "0 = x \<longleftrightarrow> x = 0" 
54868  197 
by (fact eq_commute) 
26071  198 

22390  199 
class comm_monoid_add = zero + ab_semigroup_add + 
25062  200 
assumes add_0: "0 + a = a" 
54868  201 
begin 
23085  202 

59559
35da1bbf234e
more canonical order of subscriptions avoids superfluous facts
haftmann
parents:
59557
diff
changeset

203 
subclass monoid_add 
61169  204 
by standard (simp_all add: add_0 add.commute [of _ 0]) 
25062  205 

59559
35da1bbf234e
more canonical order of subscriptions avoids superfluous facts
haftmann
parents:
59557
diff
changeset

206 
sublocale add!: comm_monoid plus 0 
61169  207 
by standard (simp add: ac_simps) 
14738  208 

54868  209 
end 
210 

22390  211 
class monoid_mult = one + semigroup_mult + 
35720  212 
assumes mult_1_left: "1 * a = a" 
213 
and mult_1_right: "a * 1 = a" 

54868  214 
begin 
35720  215 

54868  216 
sublocale mult!: monoid times 1 
61169  217 
by standard (fact mult_1_left mult_1_right)+ 
14738  218 

54868  219 
end 
220 

26071  221 
lemma one_reorient: "1 = x \<longleftrightarrow> x = 1" 
54868  222 
by (fact eq_commute) 
26071  223 

22390  224 
class comm_monoid_mult = one + ab_semigroup_mult + 
25062  225 
assumes mult_1: "1 * a = a" 
54868  226 
begin 
14738  227 

59559
35da1bbf234e
more canonical order of subscriptions avoids superfluous facts
haftmann
parents:
59557
diff
changeset

228 
subclass monoid_mult 
61169  229 
by standard (simp_all add: mult_1 mult.commute [of _ 1]) 
25062  230 

59559
35da1bbf234e
more canonical order of subscriptions avoids superfluous facts
haftmann
parents:
59557
diff
changeset

231 
sublocale mult!: comm_monoid times 1 
61169  232 
by standard (simp add: ac_simps) 
14738  233 

54868  234 
end 
235 

22390  236 
class cancel_semigroup_add = semigroup_add + 
25062  237 
assumes add_left_imp_eq: "a + b = a + c \<Longrightarrow> b = c" 
238 
assumes add_right_imp_eq: "b + a = c + a \<Longrightarrow> b = c" 

27474
a89d755b029d
move proofs of add_left_cancel and add_right_cancel into the correct locale
huffman
parents:
27250
diff
changeset

239 
begin 
a89d755b029d
move proofs of add_left_cancel and add_right_cancel into the correct locale
huffman
parents:
27250
diff
changeset

240 

a89d755b029d
move proofs of add_left_cancel and add_right_cancel into the correct locale
huffman
parents:
27250
diff
changeset

241 
lemma add_left_cancel [simp]: 
a89d755b029d
move proofs of add_left_cancel and add_right_cancel into the correct locale
huffman
parents:
27250
diff
changeset

242 
"a + b = a + c \<longleftrightarrow> b = c" 
29667  243 
by (blast dest: add_left_imp_eq) 
27474
a89d755b029d
move proofs of add_left_cancel and add_right_cancel into the correct locale
huffman
parents:
27250
diff
changeset

244 

a89d755b029d
move proofs of add_left_cancel and add_right_cancel into the correct locale
huffman
parents:
27250
diff
changeset

245 
lemma add_right_cancel [simp]: 
a89d755b029d
move proofs of add_left_cancel and add_right_cancel into the correct locale
huffman
parents:
27250
diff
changeset

246 
"b + a = c + a \<longleftrightarrow> b = c" 
29667  247 
by (blast dest: add_right_imp_eq) 
27474
a89d755b029d
move proofs of add_left_cancel and add_right_cancel into the correct locale
huffman
parents:
27250
diff
changeset

248 

a89d755b029d
move proofs of add_left_cancel and add_right_cancel into the correct locale
huffman
parents:
27250
diff
changeset

249 
end 
14738  250 

59815
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

251 
class cancel_ab_semigroup_add = ab_semigroup_add + minus + 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

252 
assumes add_diff_cancel_left' [simp]: "(a + b)  a = b" 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

253 
assumes diff_diff_add [algebra_simps, field_simps]: "a  b  c = a  (b + c)" 
25267  254 
begin 
14738  255 

59815
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

256 
lemma add_diff_cancel_right' [simp]: 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

257 
"(a + b)  b = a" 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

258 
using add_diff_cancel_left' [of b a] by (simp add: ac_simps) 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

259 

25267  260 
subclass cancel_semigroup_add 
28823  261 
proof 
22390  262 
fix a b c :: 'a 
59815
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

263 
assume "a + b = a + c" 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

264 
then have "a + b  a = a + c  a" 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

265 
by simp 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

266 
then show "b = c" 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

267 
by simp 
22390  268 
next 
14738  269 
fix a b c :: 'a 
270 
assume "b + a = c + a" 

59815
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

271 
then have "b + a  a = c + a  a" 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

272 
by simp 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

273 
then show "b = c" 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

274 
by simp 
14738  275 
qed 
276 

59815
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

277 
lemma add_diff_cancel_left [simp]: 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

278 
"(c + a)  (c + b) = a  b" 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

279 
unfolding diff_diff_add [symmetric] by simp 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

280 

cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

281 
lemma add_diff_cancel_right [simp]: 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

282 
"(a + c)  (b + c) = a  b" 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

283 
using add_diff_cancel_left [symmetric] by (simp add: ac_simps) 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

284 

cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

285 
lemma diff_right_commute: 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

286 
"a  c  b = a  b  c" 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

287 
by (simp add: diff_diff_add add.commute) 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

288 

25267  289 
end 
290 

29904  291 
class cancel_comm_monoid_add = cancel_ab_semigroup_add + comm_monoid_add 
59322  292 
begin 
293 

59815
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

294 
lemma diff_zero [simp]: 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

295 
"a  0 = a" 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

296 
using add_diff_cancel_right' [of a 0] by simp 
59322  297 

298 
lemma diff_cancel [simp]: 

299 
"a  a = 0" 

300 
proof  

301 
have "(a + 0)  (a + 0) = 0" by (simp only: add_diff_cancel_left diff_zero) 

302 
then show ?thesis by simp 

303 
qed 

304 

305 
lemma add_implies_diff: 

306 
assumes "c + b = a" 

307 
shows "c = a  b" 

308 
proof  

309 
from assms have "(b + c)  (b + 0) = a  b" by (simp add: add.commute) 

310 
then show "c = a  b" by simp 

311 
qed 

312 

59815
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

313 
end 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

314 

cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

315 
class comm_monoid_diff = cancel_comm_monoid_add + 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

316 
assumes zero_diff [simp]: "0  a = 0" 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

317 
begin 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

318 

cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

319 
lemma diff_add_zero [simp]: 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

320 
"a  (a + b) = 0" 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

321 
proof  
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

322 
have "a  (a + b) = (a + 0)  (a + b)" by simp 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

323 
also have "\<dots> = 0" by (simp only: add_diff_cancel_left zero_diff) 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

324 
finally show ?thesis . 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

325 
qed 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

326 

59322  327 
end 
328 

29904  329 

60758  330 
subsection \<open>Groups\<close> 
23085  331 

25762  332 
class group_add = minus + uminus + monoid_add + 
25062  333 
assumes left_minus [simp]: " a + a = 0" 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

334 
assumes add_uminus_conv_diff [simp]: "a + ( b) = a  b" 
25062  335 
begin 
23085  336 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

337 
lemma diff_conv_add_uminus: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

338 
"a  b = a + ( b)" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

339 
by simp 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

340 

34147
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

341 
lemma minus_unique: 
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

342 
assumes "a + b = 0" shows " a = b" 
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

343 
proof  
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

344 
have " a =  a + (a + b)" using assms by simp 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56950
diff
changeset

345 
also have "\<dots> = b" by (simp add: add.assoc [symmetric]) 
34147
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

346 
finally show ?thesis . 
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

347 
qed 
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

348 

25062  349 
lemma minus_zero [simp]: " 0 = 0" 
14738  350 
proof  
34147
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

351 
have "0 + 0 = 0" by (rule add_0_right) 
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

352 
thus " 0 = 0" by (rule minus_unique) 
14738  353 
qed 
354 

25062  355 
lemma minus_minus [simp]: " ( a) = a" 
23085  356 
proof  
34147
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

357 
have " a + a = 0" by (rule left_minus) 
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

358 
thus " ( a) = a" by (rule minus_unique) 
23085  359 
qed 
14738  360 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

361 
lemma right_minus: "a +  a = 0" 
14738  362 
proof  
25062  363 
have "a +  a =  ( a) +  a" by simp 
364 
also have "\<dots> = 0" by (rule left_minus) 

14738  365 
finally show ?thesis . 
366 
qed 

367 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

368 
lemma diff_self [simp]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

369 
"a  a = 0" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

370 
using right_minus [of a] by simp 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

371 

40368
47c186c8577d
added class relation group_add < cancel_semigroup_add
haftmann
parents:
39134
diff
changeset

372 
subclass cancel_semigroup_add 
47c186c8577d
added class relation group_add < cancel_semigroup_add
haftmann
parents:
39134
diff
changeset

373 
proof 
47c186c8577d
added class relation group_add < cancel_semigroup_add
haftmann
parents:
39134
diff
changeset

374 
fix a b c :: 'a 
47c186c8577d
added class relation group_add < cancel_semigroup_add
haftmann
parents:
39134
diff
changeset

375 
assume "a + b = a + c" 
47c186c8577d
added class relation group_add < cancel_semigroup_add
haftmann
parents:
39134
diff
changeset

376 
then have " a + a + b =  a + a + c" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56950
diff
changeset

377 
unfolding add.assoc by simp 
40368
47c186c8577d
added class relation group_add < cancel_semigroup_add
haftmann
parents:
39134
diff
changeset

378 
then show "b = c" by simp 
47c186c8577d
added class relation group_add < cancel_semigroup_add
haftmann
parents:
39134
diff
changeset

379 
next 
47c186c8577d
added class relation group_add < cancel_semigroup_add
haftmann
parents:
39134
diff
changeset

380 
fix a b c :: 'a 
47c186c8577d
added class relation group_add < cancel_semigroup_add
haftmann
parents:
39134
diff
changeset

381 
assume "b + a = c + a" 
47c186c8577d
added class relation group_add < cancel_semigroup_add
haftmann
parents:
39134
diff
changeset

382 
then have "b + a +  a = c + a +  a" by simp 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56950
diff
changeset

383 
then show "b = c" unfolding add.assoc by simp 
40368
47c186c8577d
added class relation group_add < cancel_semigroup_add
haftmann
parents:
39134
diff
changeset

384 
qed 
47c186c8577d
added class relation group_add < cancel_semigroup_add
haftmann
parents:
39134
diff
changeset

385 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

386 
lemma minus_add_cancel [simp]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

387 
" a + (a + b) = b" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56950
diff
changeset

388 
by (simp add: add.assoc [symmetric]) 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

389 

b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

390 
lemma add_minus_cancel [simp]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

391 
"a + ( a + b) = b" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56950
diff
changeset

392 
by (simp add: add.assoc [symmetric]) 
34147
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

393 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

394 
lemma diff_add_cancel [simp]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

395 
"a  b + b = a" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56950
diff
changeset

396 
by (simp only: diff_conv_add_uminus add.assoc) simp 
34147
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

397 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

398 
lemma add_diff_cancel [simp]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

399 
"a + b  b = a" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56950
diff
changeset

400 
by (simp only: diff_conv_add_uminus add.assoc) simp 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

401 

b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

402 
lemma minus_add: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

403 
" (a + b) =  b +  a" 
34147
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

404 
proof  
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

405 
have "(a + b) + ( b +  a) = 0" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56950
diff
changeset

406 
by (simp only: add.assoc add_minus_cancel) simp 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

407 
then show " (a + b) =  b +  a" 
34147
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

408 
by (rule minus_unique) 
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

409 
qed 
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

410 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

411 
lemma right_minus_eq [simp]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

412 
"a  b = 0 \<longleftrightarrow> a = b" 
14738  413 
proof 
23085  414 
assume "a  b = 0" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56950
diff
changeset

415 
have "a = (a  b) + b" by (simp add: add.assoc) 
60758  416 
also have "\<dots> = b" using \<open>a  b = 0\<close> by simp 
23085  417 
finally show "a = b" . 
14738  418 
next 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

419 
assume "a = b" thus "a  b = 0" by simp 
14738  420 
qed 
421 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

422 
lemma eq_iff_diff_eq_0: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

423 
"a = b \<longleftrightarrow> a  b = 0" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

424 
by (fact right_minus_eq [symmetric]) 
14738  425 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

426 
lemma diff_0 [simp]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

427 
"0  a =  a" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

428 
by (simp only: diff_conv_add_uminus add_0_left) 
14738  429 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

430 
lemma diff_0_right [simp]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

431 
"a  0 = a" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

432 
by (simp only: diff_conv_add_uminus minus_zero add_0_right) 
14738  433 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

434 
lemma diff_minus_eq_add [simp]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

435 
"a   b = a + b" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

436 
by (simp only: diff_conv_add_uminus minus_minus) 
14738  437 

25062  438 
lemma neg_equal_iff_equal [simp]: 
439 
" a =  b \<longleftrightarrow> a = b" 

14738  440 
proof 
441 
assume " a =  b" 

29667  442 
hence " ( a) =  ( b)" by simp 
25062  443 
thus "a = b" by simp 
14738  444 
next 
25062  445 
assume "a = b" 
446 
thus " a =  b" by simp 

14738  447 
qed 
448 

25062  449 
lemma neg_equal_0_iff_equal [simp]: 
450 
" a = 0 \<longleftrightarrow> a = 0" 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

451 
by (subst neg_equal_iff_equal [symmetric]) simp 
14738  452 

25062  453 
lemma neg_0_equal_iff_equal [simp]: 
454 
"0 =  a \<longleftrightarrow> 0 = a" 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

455 
by (subst neg_equal_iff_equal [symmetric]) simp 
14738  456 

60758  457 
text\<open>The next two equations can make the simplifier loop!\<close> 
14738  458 

25062  459 
lemma equation_minus_iff: 
460 
"a =  b \<longleftrightarrow> b =  a" 

14738  461 
proof  
25062  462 
have " ( a) =  b \<longleftrightarrow>  a = b" by (rule neg_equal_iff_equal) 
463 
thus ?thesis by (simp add: eq_commute) 

464 
qed 

465 

466 
lemma minus_equation_iff: 

467 
" a = b \<longleftrightarrow>  b = a" 

468 
proof  

469 
have " a =  ( b) \<longleftrightarrow> a = b" by (rule neg_equal_iff_equal) 

14738  470 
thus ?thesis by (simp add: eq_commute) 
471 
qed 

472 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

473 
lemma eq_neg_iff_add_eq_0: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

474 
"a =  b \<longleftrightarrow> a + b = 0" 
29914
c9ced4f54e82
generalize lemma eq_neg_iff_add_eq_0, and move to OrderedGroup
huffman
parents:
29904
diff
changeset

475 
proof 
c9ced4f54e82
generalize lemma eq_neg_iff_add_eq_0, and move to OrderedGroup
huffman
parents:
29904
diff
changeset

476 
assume "a =  b" then show "a + b = 0" by simp 
c9ced4f54e82
generalize lemma eq_neg_iff_add_eq_0, and move to OrderedGroup
huffman
parents:
29904
diff
changeset

477 
next 
c9ced4f54e82
generalize lemma eq_neg_iff_add_eq_0, and move to OrderedGroup
huffman
parents:
29904
diff
changeset

478 
assume "a + b = 0" 
c9ced4f54e82
generalize lemma eq_neg_iff_add_eq_0, and move to OrderedGroup
huffman
parents:
29904
diff
changeset

479 
moreover have "a + (b +  b) = (a + b) +  b" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56950
diff
changeset

480 
by (simp only: add.assoc) 
29914
c9ced4f54e82
generalize lemma eq_neg_iff_add_eq_0, and move to OrderedGroup
huffman
parents:
29904
diff
changeset

481 
ultimately show "a =  b" by simp 
c9ced4f54e82
generalize lemma eq_neg_iff_add_eq_0, and move to OrderedGroup
huffman
parents:
29904
diff
changeset

482 
qed 
c9ced4f54e82
generalize lemma eq_neg_iff_add_eq_0, and move to OrderedGroup
huffman
parents:
29904
diff
changeset

483 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

484 
lemma add_eq_0_iff2: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

485 
"a + b = 0 \<longleftrightarrow> a =  b" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

486 
by (fact eq_neg_iff_add_eq_0 [symmetric]) 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

487 

b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

488 
lemma neg_eq_iff_add_eq_0: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

489 
" a = b \<longleftrightarrow> a + b = 0" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

490 
by (auto simp add: add_eq_0_iff2) 
44348  491 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

492 
lemma add_eq_0_iff: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

493 
"a + b = 0 \<longleftrightarrow> b =  a" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

494 
by (auto simp add: neg_eq_iff_add_eq_0 [symmetric]) 
45548
3e2722d66169
Groups.thy: generalize several lemmas from class ab_group_add to class group_add
huffman
parents:
45294
diff
changeset

495 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

496 
lemma minus_diff_eq [simp]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

497 
" (a  b) = b  a" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56950
diff
changeset

498 
by (simp only: neg_eq_iff_add_eq_0 diff_conv_add_uminus add.assoc minus_add_cancel) simp 
45548
3e2722d66169
Groups.thy: generalize several lemmas from class ab_group_add to class group_add
huffman
parents:
45294
diff
changeset

499 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

500 
lemma add_diff_eq [algebra_simps, field_simps]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

501 
"a + (b  c) = (a + b)  c" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56950
diff
changeset

502 
by (simp only: diff_conv_add_uminus add.assoc) 
45548
3e2722d66169
Groups.thy: generalize several lemmas from class ab_group_add to class group_add
huffman
parents:
45294
diff
changeset

503 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

504 
lemma diff_add_eq_diff_diff_swap: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

505 
"a  (b + c) = a  c  b" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56950
diff
changeset

506 
by (simp only: diff_conv_add_uminus add.assoc minus_add) 
45548
3e2722d66169
Groups.thy: generalize several lemmas from class ab_group_add to class group_add
huffman
parents:
45294
diff
changeset

507 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

508 
lemma diff_eq_eq [algebra_simps, field_simps]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

509 
"a  b = c \<longleftrightarrow> a = c + b" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

510 
by auto 
45548
3e2722d66169
Groups.thy: generalize several lemmas from class ab_group_add to class group_add
huffman
parents:
45294
diff
changeset

511 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

512 
lemma eq_diff_eq [algebra_simps, field_simps]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

513 
"a = c  b \<longleftrightarrow> a + b = c" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

514 
by auto 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

515 

b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

516 
lemma diff_diff_eq2 [algebra_simps, field_simps]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

517 
"a  (b  c) = (a + c)  b" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56950
diff
changeset

518 
by (simp only: diff_conv_add_uminus add.assoc) simp 
45548
3e2722d66169
Groups.thy: generalize several lemmas from class ab_group_add to class group_add
huffman
parents:
45294
diff
changeset

519 

3e2722d66169
Groups.thy: generalize several lemmas from class ab_group_add to class group_add
huffman
parents:
45294
diff
changeset

520 
lemma diff_eq_diff_eq: 
3e2722d66169
Groups.thy: generalize several lemmas from class ab_group_add to class group_add
huffman
parents:
45294
diff
changeset

521 
"a  b = c  d \<Longrightarrow> a = b \<longleftrightarrow> c = d" 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

522 
by (simp only: eq_iff_diff_eq_0 [of a b] eq_iff_diff_eq_0 [of c d]) 
45548
3e2722d66169
Groups.thy: generalize several lemmas from class ab_group_add to class group_add
huffman
parents:
45294
diff
changeset

523 

25062  524 
end 
525 

25762  526 
class ab_group_add = minus + uminus + comm_monoid_add + 
25062  527 
assumes ab_left_minus: " a + a = 0" 
59557  528 
assumes ab_diff_conv_add_uminus: "a  b = a + ( b)" 
25267  529 
begin 
25062  530 

25267  531 
subclass group_add 
59557  532 
proof qed (simp_all add: ab_left_minus ab_diff_conv_add_uminus) 
25062  533 

29904  534 
subclass cancel_comm_monoid_add 
28823  535 
proof 
25062  536 
fix a b c :: 'a 
59815
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

537 
have "b + a  a = b" 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

538 
by simp 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

539 
then show "a + b  a = b" 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

540 
by (simp add: ac_simps) 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

541 
show "a  b  c = a  (b + c)" 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59559
diff
changeset

542 
by (simp add: algebra_simps) 
25062  543 
qed 
544 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

545 
lemma uminus_add_conv_diff [simp]: 
25062  546 
" a + b = b  a" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56950
diff
changeset

547 
by (simp add: add.commute) 
25062  548 

549 
lemma minus_add_distrib [simp]: 

550 
" (a + b) =  a +  b" 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

551 
by (simp add: algebra_simps) 
25062  552 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

553 
lemma diff_add_eq [algebra_simps, field_simps]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

554 
"(a  b) + c = (a + c)  b" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

555 
by (simp add: algebra_simps) 
25077  556 

25062  557 
end 
14738  558 

37884
314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
36977
diff
changeset

559 

60758  560 
subsection \<open>(Partially) Ordered Groups\<close> 
14738  561 

60758  562 
text \<open> 
35301
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

563 
The theory of partially ordered groups is taken from the books: 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

564 
\begin{itemize} 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

565 
\item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

566 
\item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

567 
\end{itemize} 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

568 
Most of the used notions can also be looked up in 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

569 
\begin{itemize} 
54703  570 
\item @{url "http://www.mathworld.com"} by Eric Weisstein et. al. 
35301
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

571 
\item \emph{Algebra I} by van der Waerden, Springer. 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

572 
\end{itemize} 
60758  573 
\<close> 
35301
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

574 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

575 
class ordered_ab_semigroup_add = order + ab_semigroup_add + 
25062  576 
assumes add_left_mono: "a \<le> b \<Longrightarrow> c + a \<le> c + b" 
577 
begin 

24380
c215e256beca
moved ordered_ab_semigroup_add to OrderedGroup.thy
haftmann
parents:
24286
diff
changeset

578 

25062  579 
lemma add_right_mono: 
580 
"a \<le> b \<Longrightarrow> a + c \<le> b + c" 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56950
diff
changeset

581 
by (simp add: add.commute [of _ c] add_left_mono) 
14738  582 

60758  583 
text \<open>nonstrict, in both arguments\<close> 
14738  584 
lemma add_mono: 
25062  585 
"a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c \<le> b + d" 
14738  586 
apply (erule add_right_mono [THEN order_trans]) 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56950
diff
changeset

587 
apply (simp add: add.commute add_left_mono) 
14738  588 
done 
589 

25062  590 
end 
591 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

592 
class ordered_cancel_ab_semigroup_add = 
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

593 
ordered_ab_semigroup_add + cancel_ab_semigroup_add 
25062  594 
begin 
595 

14738  596 
lemma add_strict_left_mono: 
25062  597 
"a < b \<Longrightarrow> c + a < c + b" 
29667  598 
by (auto simp add: less_le add_left_mono) 
14738  599 

600 
lemma add_strict_right_mono: 

25062  601 
"a < b \<Longrightarrow> a + c < b + c" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56950
diff
changeset

602 
by (simp add: add.commute [of _ c] add_strict_left_mono) 
14738  603 

60758  604 
text\<open>Strict monotonicity in both arguments\<close> 
25062  605 
lemma add_strict_mono: 
606 
"a < b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d" 

607 
apply (erule add_strict_right_mono [THEN less_trans]) 

14738  608 
apply (erule add_strict_left_mono) 
609 
done 

610 

611 
lemma add_less_le_mono: 

25062  612 
"a < b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c < b + d" 
613 
apply (erule add_strict_right_mono [THEN less_le_trans]) 

614 
apply (erule add_left_mono) 

14738  615 
done 
616 

617 
lemma add_le_less_mono: 

25062  618 
"a \<le> b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d" 
619 
apply (erule add_right_mono [THEN le_less_trans]) 

14738  620 
apply (erule add_strict_left_mono) 
621 
done 

622 

25062  623 
end 
624 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

625 
class ordered_ab_semigroup_add_imp_le = 
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

626 
ordered_cancel_ab_semigroup_add + 
25062  627 
assumes add_le_imp_le_left: "c + a \<le> c + b \<Longrightarrow> a \<le> b" 
628 
begin 

629 

14738  630 
lemma add_less_imp_less_left: 
29667  631 
assumes less: "c + a < c + b" shows "a < b" 
14738  632 
proof  
633 
from less have le: "c + a <= c + b" by (simp add: order_le_less) 

634 
have "a <= b" 

635 
apply (insert le) 

636 
apply (drule add_le_imp_le_left) 

637 
by (insert le, drule add_le_imp_le_left, assumption) 

638 
moreover have "a \<noteq> b" 

639 
proof (rule ccontr) 

640 
assume "~(a \<noteq> b)" 

641 
then have "a = b" by simp 

642 
then have "c + a = c + b" by simp 

643 
with less show "False"by simp 

644 
qed 

645 
ultimately show "a < b" by (simp add: order_le_less) 

646 
qed 

647 

648 
lemma add_less_imp_less_right: 

25062  649 
"a + c < b + c \<Longrightarrow> a < b" 
14738  650 
apply (rule add_less_imp_less_left [of c]) 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56950
diff
changeset

651 
apply (simp add: add.commute) 
14738  652 
done 
653 

654 
lemma add_less_cancel_left [simp]: 

25062  655 
"c + a < c + b \<longleftrightarrow> a < b" 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

656 
by (blast intro: add_less_imp_less_left add_strict_left_mono) 
14738  657 

658 
lemma add_less_cancel_right [simp]: 

25062  659 
"a + c < b + c \<longleftrightarrow> a < b" 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

660 
by (blast intro: add_less_imp_less_right add_strict_right_mono) 
14738  661 

662 
lemma add_le_cancel_left [simp]: 

25062  663 
"c + a \<le> c + b \<longleftrightarrow> a \<le> b" 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

664 
by (auto, drule add_le_imp_le_left, simp_all add: add_left_mono) 
14738  665 

666 
lemma add_le_cancel_right [simp]: 

25062  667 
"a + c \<le> b + c \<longleftrightarrow> a \<le> b" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56950
diff
changeset

668 
by (simp add: add.commute [of a c] add.commute [of b c]) 
14738  669 

670 
lemma add_le_imp_le_right: 

25062  671 
"a + c \<le> b + c \<Longrightarrow> a \<le> b" 
29667  672 
by simp 
25062  673 

25077  674 
lemma max_add_distrib_left: 
675 
"max x y + z = max (x + z) (y + z)" 

676 
unfolding max_def by auto 

677 

678 
lemma min_add_distrib_left: 

679 
"min x y + z = min (x + z) (y + z)" 

680 
unfolding min_def by auto 

681 

44848
f4d0b060c7ca
remove lemmas nat_add_min_{left,right} in favor of generic lemmas min_add_distrib_{left,right}
huffman
parents:
44433
diff
changeset

682 
lemma max_add_distrib_right: 
f4d0b060c7ca
remove lemmas nat_add_min_{left,right} in favor of generic lemmas min_add_distrib_{left,right}
huffman
parents:
44433
diff
changeset

683 
"x + max y z = max (x + y) (x + z)" 
f4d0b060c7ca
remove lemmas nat_add_min_{left,right} in favor of generic lemmas min_add_distrib_{left,right}
huffman
parents:
44433
diff
changeset

684 
unfolding max_def by auto 
f4d0b060c7ca
remove lemmas nat_add_min_{left,right} in favor of generic lemmas min_add_distrib_{left,right}
huffman
parents:
44433
diff
changeset

685 

f4d0b060c7ca
remove lemmas nat_add_min_{left,right} in favor of generic lemmas min_add_distrib_{left,right}
huffman
parents:
44433
diff
changeset

686 
lemma min_add_distrib_right: 
f4d0b060c7ca
remove lemmas nat_add_min_{left,right} in favor of generic lemmas min_add_distrib_{left,right}
huffman
parents:
44433
diff
changeset

687 
"x + min y z = min (x + y) (x + z)" 
f4d0b060c7ca
remove lemmas nat_add_min_{left,right} in favor of generic lemmas min_add_distrib_{left,right}
huffman
parents:
44433
diff
changeset

688 
unfolding min_def by auto 
f4d0b060c7ca
remove lemmas nat_add_min_{left,right} in favor of generic lemmas min_add_distrib_{left,right}
huffman
parents:
44433
diff
changeset

689 

25062  690 
end 
691 

52289  692 
class ordered_cancel_comm_monoid_diff = comm_monoid_diff + ordered_ab_semigroup_add_imp_le + 
693 
assumes le_iff_add: "a \<le> b \<longleftrightarrow> (\<exists>c. b = a + c)" 

694 
begin 

695 

696 
context 

697 
fixes a b 

698 
assumes "a \<le> b" 

699 
begin 

700 

701 
lemma add_diff_inverse: 

702 
"a + (b  a) = b" 

60758  703 
using \<open>a \<le> b\<close> by (auto simp add: le_iff_add) 
52289  704 

705 
lemma add_diff_assoc: 

706 
"c + (b  a) = c + b  a" 

60758  707 
using \<open>a \<le> b\<close> by (auto simp add: le_iff_add add.left_commute [of c]) 
52289  708 

709 
lemma add_diff_assoc2: 

710 
"b  a + c = b + c  a" 

60758  711 
using \<open>a \<le> b\<close> by (auto simp add: le_iff_add add.assoc) 
52289  712 

713 
lemma diff_add_assoc: 

714 
"c + b  a = c + (b  a)" 

60758  715 
using \<open>a \<le> b\<close> by (simp add: add.commute add_diff_assoc) 
52289  716 

717 
lemma diff_add_assoc2: 

718 
"b + c  a = b  a + c" 

60758  719 
using \<open>a \<le> b\<close>by (simp add: add.commute add_diff_assoc) 
52289  720 

721 
lemma diff_diff_right: 

722 
"c  (b  a) = c + a  b" 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56950
diff
changeset

723 
by (simp add: add_diff_inverse add_diff_cancel_left [of a c "b  a", symmetric] add.commute) 
52289  724 

725 
lemma diff_add: 

726 
"b  a + a = b" 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56950
diff
changeset

727 
by (simp add: add.commute add_diff_inverse) 
52289  728 

729 
lemma le_add_diff: 

730 
"c \<le> b + c  a" 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56950
diff
changeset

731 
by (auto simp add: add.commute diff_add_assoc2 le_iff_add) 
52289  732 

733 
lemma le_imp_diff_is_add: 

734 
"a \<le> b \<Longrightarrow> b  a = c \<longleftrightarrow> b = c + a" 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56950
diff
changeset

735 
by (auto simp add: add.commute add_diff_inverse) 
52289  736 

737 
lemma le_diff_conv2: 

738 
"c \<le> b  a \<longleftrightarrow> c + a \<le> b" (is "?P \<longleftrightarrow> ?Q") 

739 
proof 

740 
assume ?P 

741 
then have "c + a \<le> b  a + a" by (rule add_right_mono) 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56950
diff
changeset

742 
then show ?Q by (simp add: add_diff_inverse add.commute) 
52289  743 
next 
744 
assume ?Q 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56950
diff
changeset

745 
then have "a + c \<le> a + (b  a)" by (simp add: add_diff_inverse add.commute) 
52289  746 
then show ?P by simp 
747 
qed 

748 

749 
end 

750 

751 
end 

752 

753 

60758  754 
subsection \<open>Support for reasoning about signs\<close> 
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

755 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

756 
class ordered_comm_monoid_add = 
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

757 
ordered_cancel_ab_semigroup_add + comm_monoid_add 
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

758 
begin 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

759 

0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

760 
lemma add_pos_nonneg: 
29667  761 
assumes "0 < a" and "0 \<le> b" shows "0 < a + b" 
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

762 
proof  
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

763 
have "0 + 0 < a + b" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

764 
using assms by (rule add_less_le_mono) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

765 
then show ?thesis by simp 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

766 
qed 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

767 

0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

768 
lemma add_pos_pos: 
29667  769 
assumes "0 < a" and "0 < b" shows "0 < a + b" 
770 
by (rule add_pos_nonneg) (insert assms, auto) 

25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

771 

0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

772 
lemma add_nonneg_pos: 
29667  773 
assumes "0 \<le> a" and "0 < b" shows "0 < a + b" 
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

774 
proof  
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

775 
have "0 + 0 < a + b" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

776 
using assms by (rule add_le_less_mono) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

777 
then show ?thesis by simp 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

778 
qed 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

779 

36977
71c8973a604b
declare add_nonneg_nonneg [simp]; remove nowredundant lemmas realpow_two_le_order(2)
huffman
parents:
36348
diff
changeset

780 
lemma add_nonneg_nonneg [simp]: 
29667  781 
assumes "0 \<le> a" and "0 \<le> b" shows "0 \<le> a + b" 
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

782 
proof  
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

783 
have "0 + 0 \<le> a + b" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

784 
using assms by (rule add_mono) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

785 
then show ?thesis by simp 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

786 
qed 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

787 

30691  788 
lemma add_neg_nonpos: 
29667  789 
assumes "a < 0" and "b \<le> 0" shows "a + b < 0" 
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

790 
proof  
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

791 
have "a + b < 0 + 0" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

792 
using assms by (rule add_less_le_mono) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

793 
then show ?thesis by simp 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

794 
qed 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

795 

0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

796 
lemma add_neg_neg: 
29667  797 
assumes "a < 0" and "b < 0" shows "a + b < 0" 
798 
by (rule add_neg_nonpos) (insert assms, auto) 

25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

799 

0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

800 
lemma add_nonpos_neg: 
29667  801 
assumes "a \<le> 0" and "b < 0" shows "a + b < 0" 
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

802 
proof  
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

803 
have "a + b < 0 + 0" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

804 
using assms by (rule add_le_less_mono) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

805 
then show ?thesis by simp 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

806 
qed 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

807 

0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

808 
lemma add_nonpos_nonpos: 
29667  809 
assumes "a \<le> 0" and "b \<le> 0" shows "a + b \<le> 0" 
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

810 
proof  
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

811 
have "a + b \<le> 0 + 0" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

812 
using assms by (rule add_mono) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

813 
then show ?thesis by simp 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

814 
qed 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

815 

30691  816 
lemmas add_sign_intros = 
817 
add_pos_nonneg add_pos_pos add_nonneg_pos add_nonneg_nonneg 

818 
add_neg_nonpos add_neg_neg add_nonpos_neg add_nonpos_nonpos 

819 

29886  820 
lemma add_nonneg_eq_0_iff: 
821 
assumes x: "0 \<le> x" and y: "0 \<le> y" 

822 
shows "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0" 

823 
proof (intro iffI conjI) 

824 
have "x = x + 0" by simp 

825 
also have "x + 0 \<le> x + y" using y by (rule add_left_mono) 

826 
also assume "x + y = 0" 

827 
also have "0 \<le> x" using x . 

828 
finally show "x = 0" . 

829 
next 

830 
have "y = 0 + y" by simp 

831 
also have "0 + y \<le> x + y" using x by (rule add_right_mono) 

832 
also assume "x + y = 0" 

833 
also have "0 \<le> y" using y . 

834 
finally show "y = 0" . 

835 
next 

836 
assume "x = 0 \<and> y = 0" 

837 
then show "x + y = 0" by simp 

838 
qed 

839 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

840 
lemma add_increasing: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

841 
"0 \<le> a \<Longrightarrow> b \<le> c \<Longrightarrow> b \<le> a + c" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

842 
by (insert add_mono [of 0 a b c], simp) 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

843 

b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

844 
lemma add_increasing2: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

845 
"0 \<le> c \<Longrightarrow> b \<le> a \<Longrightarrow> b \<le> a + c" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56950
diff
changeset

846 
by (simp add: add_increasing add.commute [of a]) 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

847 

b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

848 
lemma add_strict_increasing: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

849 
"0 < a \<Longrightarrow> b \<le> c \<Longrightarrow> b < a + c" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

850 
by (insert add_less_le_mono [of 0 a b c], simp) 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

851 

b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

852 
lemma add_strict_increasing2: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

853 
"0 \<le> a \<Longrightarrow> b < c \<Longrightarrow> b < a + c" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

854 
by (insert add_le_less_mono [of 0 a b c], simp) 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

855 

25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

856 
end 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

857 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

858 
class ordered_ab_group_add = 
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

859 
ab_group_add + ordered_ab_semigroup_add 
25062  860 
begin 
861 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

862 
subclass ordered_cancel_ab_semigroup_add .. 
25062  863 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

864 
subclass ordered_ab_semigroup_add_imp_le 
28823  865 
proof 
25062  866 
fix a b c :: 'a 
867 
assume "c + a \<le> c + b" 

868 
hence "(c) + (c + a) \<le> (c) + (c + b)" by (rule add_left_mono) 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56950
diff
changeset

869 
hence "((c) + c) + a \<le> ((c) + c) + b" by (simp only: add.assoc) 
25062  870 
thus "a \<le> b" by simp 
871 
qed 

872 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

873 
subclass ordered_comm_monoid_add .. 
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

874 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

875 
lemma add_less_same_cancel1 [simp]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

876 
"b + a < b \<longleftrightarrow> a < 0" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

877 
using add_less_cancel_left [of _ _ 0] by simp 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

878 

b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

879 
lemma add_less_same_cancel2 [simp]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

880 
"a + b < b \<longleftrightarrow> a < 0" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

881 
using add_less_cancel_right [of _ _ 0] by simp 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

882 

b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

883 
lemma less_add_same_cancel1 [simp]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

884 
"a < a + b \<longleftrightarrow> 0 < b" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

885 
using add_less_cancel_left [of _ 0] by simp 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

886 

b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

887 
lemma less_add_same_cancel2 [simp]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

888 
"a < b + a \<longleftrightarrow> 0 < b" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

889 
using add_less_cancel_right [of 0] by simp 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

890 

b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

891 
lemma add_le_same_cancel1 [simp]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

892 
"b + a \<le> b \<longleftrightarrow> a \<le> 0" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

893 
using add_le_cancel_left [of _ _ 0] by simp 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

894 

b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

895 
lemma add_le_same_cancel2 [simp]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

896 
"a + b \<le> b \<longleftrightarrow> a \<le> 0" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

897 
using add_le_cancel_right [of _ _ 0] by simp 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

898 

b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

899 
lemma le_add_same_cancel1 [simp]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

900 
"a \<le> a + b \<longleftrightarrow> 0 \<le> b" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

901 
using add_le_cancel_left [of _ 0] by simp 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

902 

b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

903 
lemma le_add_same_cancel2 [simp]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

904 
"a \<le> b + a \<longleftrightarrow> 0 \<le> b" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

905 
using add_le_cancel_right [of 0] by simp 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

906 

25077  907 
lemma max_diff_distrib_left: 
908 
shows "max x y  z = max (x  z) (y  z)" 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

909 
using max_add_distrib_left [of x y " z"] by simp 
25077  910 

911 
lemma min_diff_distrib_left: 

912 
shows "min x y  z = min (x  z) (y  z)" 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

913 
using min_add_distrib_left [of x y " z"] by simp 
25077  914 

915 
lemma le_imp_neg_le: 

29667  916 
assumes "a \<le> b" shows "b \<le> a" 
25077  917 
proof  
60758  918 
have "a+a \<le> a+b" using \<open>a \<le> b\<close> by (rule add_left_mono) 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

919 
then have "0 \<le> a+b" by simp 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

920 
then have "0 + (b) \<le> (a + b) + (b)" by (rule add_right_mono) 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

921 
then show ?thesis by (simp add: algebra_simps) 
25077  922 
qed 
923 

924 
lemma neg_le_iff_le [simp]: " b \<le>  a \<longleftrightarrow> a \<le> b" 

925 
proof 

926 
assume " b \<le>  a" 

29667  927 
hence " ( a) \<le>  ( b)" by (rule le_imp_neg_le) 
25077  928 
thus "a\<le>b" by simp 
929 
next 

930 
assume "a\<le>b" 

931 
thus "b \<le> a" by (rule le_imp_neg_le) 

932 
qed 

933 

934 
lemma neg_le_0_iff_le [simp]: " a \<le> 0 \<longleftrightarrow> 0 \<le> a" 

29667  935 
by (subst neg_le_iff_le [symmetric], simp) 
25077  936 

937 
lemma neg_0_le_iff_le [simp]: "0 \<le>  a \<longleftrightarrow> a \<le> 0" 

29667  938 
by (subst neg_le_iff_le [symmetric], simp) 
25077  939 

940 
lemma neg_less_iff_less [simp]: " b <  a \<longleftrightarrow> a < b" 

29667  941 
by (force simp add: less_le) 
25077  942 

943 
lemma neg_less_0_iff_less [simp]: " a < 0 \<longleftrightarrow> 0 < a" 

29667  944 
by (subst neg_less_iff_less [symmetric], simp) 
25077  945 

946 
lemma neg_0_less_iff_less [simp]: "0 <  a \<longleftrightarrow> a < 0" 

29667  947 
by (subst neg_less_iff_less [symmetric], simp) 
25077  948 

60758  949 
text\<open>The next several equations can make the simplifier loop!\<close> 
25077  950 

951 
lemma less_minus_iff: "a <  b \<longleftrightarrow> b <  a" 

952 
proof  

953 
have "( (a) <  b) = (b <  a)" by (rule neg_less_iff_less) 

954 
thus ?thesis by simp 

955 
qed 

956 

957 
lemma minus_less_iff: " a < b \<longleftrightarrow>  b < a" 

958 
proof  

959 
have "( a <  (b)) = ( b < a)" by (rule neg_less_iff_less) 

960 
thus ?thesis by simp 

961 
qed 

962 

963 
lemma le_minus_iff: "a \<le>  b \<longleftrightarrow> b \<le>  a" 

964 
proof  

965 
have mm: "!! a (b::'a). ((a)) < b \<Longrightarrow> (b) < a" by (simp only: minus_less_iff) 

966 
have "( ( a) <= b) = (b <=  a)" 

967 
apply (auto simp only: le_less) 

968 
apply (drule mm) 

969 
apply (simp_all) 

970 
apply (drule mm[simplified], assumption) 

971 
done 

972 
then show ?thesis by simp 

973 
qed 

974 

975 
lemma minus_le_iff: " a \<le> b \<longleftrightarrow>  b \<le> a" 

29667  976 
by (auto simp add: le_less minus_less_iff) 
25077  977 

54148  978 
lemma diff_less_0_iff_less [simp]: 
37884
314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
36977
diff
changeset

979 
"a  b < 0 \<longleftrightarrow> a < b" 
25077  980 
proof  
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

981 
have "a  b < 0 \<longleftrightarrow> a + ( b) < b + ( b)" by simp 
37884
314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
36977
diff
changeset

982 
also have "... \<longleftrightarrow> a < b" by (simp only: add_less_cancel_right) 
25077  983 
finally show ?thesis . 
984 
qed 

985 

37884
314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
36977
diff
changeset

986 
lemmas less_iff_diff_less_0 = diff_less_0_iff_less [symmetric] 
314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
36977
diff
changeset

987 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

988 
lemma diff_less_eq [algebra_simps, field_simps]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

989 
"a  b < c \<longleftrightarrow> a < c + b" 
25077  990 
apply (subst less_iff_diff_less_0 [of a]) 
991 
apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst]) 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

992 
apply (simp add: algebra_simps) 
25077  993 
done 
994 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

995 
lemma less_diff_eq[algebra_simps, field_simps]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

996 
"a < c  b \<longleftrightarrow> a + b < c" 
36302  997 
apply (subst less_iff_diff_less_0 [of "a + b"]) 
25077  998 
apply (subst less_iff_diff_less_0 [of a]) 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

999 
apply (simp add: algebra_simps) 
25077  1000 
done 
1001 

36348
89c54f51f55a
dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
haftmann
parents:
36343
diff
changeset

1002 
lemma diff_le_eq[algebra_simps, field_simps]: "a  b \<le> c \<longleftrightarrow> a \<le> c + b" 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

1003 
by (auto simp add: le_less diff_less_eq ) 
25077  1004 

36348
89c54f51f55a
dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
haftmann
parents:
36343
diff
changeset

1005 
lemma le_diff_eq[algebra_simps, field_simps]: "a \<le> c  b \<longleftrightarrow> a + b \<le> c" 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

1006 
by (auto simp add: le_less less_diff_eq) 
25077  1007 

54148  1008 
lemma diff_le_0_iff_le [simp]: 
37884
314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
36977
diff
changeset

1009 
"a  b \<le> 0 \<longleftrightarrow> a \<le> b" 
314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
36977
diff
changeset

1010 
by (simp add: algebra_simps) 
314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
36977
diff
changeset

1011 

314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
36977
diff
changeset

1012 
lemmas le_iff_diff_le_0 = diff_le_0_iff_le [symmetric] 
314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
36977
diff
changeset

1013 

314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
36977
diff
changeset

1014 
lemma diff_eq_diff_less: 
314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
36977
diff
changeset

1015 
"a  b = c  d \<Longrightarrow> a < b \<longleftrightarrow> c < d" 
314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
36977
diff
changeset

1016 
by (auto simp only: less_iff_diff_less_0 [of a b] less_iff_diff_less_0 [of c d]) 
314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
36977
diff
changeset

1017 

37889
0d8058e0c270
keep explicit diff_def as legacy theorem; modernized abel_cancel simproc setup
haftmann
parents:
37884
diff
changeset

1018 
lemma diff_eq_diff_less_eq: 
0d8058e0c270
keep explicit diff_def as legacy theorem; modernized abel_cancel simproc setup
haftmann
parents:
37884
diff
changeset

1019 
"a  b = c  d \<Longrightarrow> a \<le> b \<longleftrightarrow> c \<le> d" 
0d8058e0c270
keep explicit diff_def as legacy theorem; modernized abel_cancel simproc setup
haftmann
parents:
37884
diff
changeset

1020 
by (auto simp only: le_iff_diff_le_0 [of a b] le_iff_diff_le_0 [of c d]) 
25077  1021 

56950  1022 
lemma diff_mono: "a \<le> b \<Longrightarrow> d \<le> c \<Longrightarrow> a  c \<le> b  d" 
1023 
by (simp add: field_simps add_mono) 

1024 

1025 
lemma diff_left_mono: "b \<le> a \<Longrightarrow> c  a \<le> c  b" 

1026 
by (simp add: field_simps) 

1027 

1028 
lemma diff_right_mono: "a \<le> b \<Longrightarrow> a  c \<le> b  c" 

1029 
by (simp add: field_simps) 

1030 

1031 
lemma diff_strict_mono: "a < b \<Longrightarrow> d < c \<Longrightarrow> a  c < b  d" 

1032 
by (simp add: field_simps add_strict_mono) 

1033 

1034 
lemma diff_strict_left_mono: "b < a \<Longrightarrow> c  a < c  b" 

1035 
by (simp add: field_simps) 

1036 

1037 
lemma diff_strict_right_mono: "a < b \<Longrightarrow> a  c < b  c" 

1038 
by (simp add: field_simps) 

1039 

25077  1040 
end 
1041 

48891  1042 
ML_file "Tools/group_cancel.ML" 
48556
62a3fbf9d35b
replace abel_cancel simprocs with functionally equivalent, but simpler and faster ones
huffman
parents:
45548
diff
changeset

1043 

62a3fbf9d35b
replace abel_cancel simprocs with functionally equivalent, but simpler and faster ones
huffman
parents:
45548
diff
changeset

1044 
simproc_setup group_cancel_add ("a + b::'a::ab_group_add") = 
60758  1045 
\<open>fn phi => fn ss => try Group_Cancel.cancel_add_conv\<close> 
48556
62a3fbf9d35b
replace abel_cancel simprocs with functionally equivalent, but simpler and faster ones
huffman
parents:
45548
diff
changeset

1046 

62a3fbf9d35b
replace abel_cancel simprocs with functionally equivalent, but simpler and faster ones
huffman
parents:
45548
diff
changeset

1047 
simproc_setup group_cancel_diff ("a  b::'a::ab_group_add") = 
60758  1048 
\<open>fn phi => fn ss => try Group_Cancel.cancel_diff_conv\<close> 
37884
314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
36977
diff
changeset

1049 

48556
62a3fbf9d35b
replace abel_cancel simprocs with functionally equivalent, but simpler and faster ones
huffman
parents:
45548
diff
changeset

1050 
simproc_setup group_cancel_eq ("a = (b::'a::ab_group_add)") = 
60758  1051 
\<open>fn phi => fn ss => try Group_Cancel.cancel_eq_conv\<close> 
37889
0d8058e0c270
keep explicit diff_def as legacy theorem; modernized abel_cancel simproc setup
haftmann
parents:
37884
diff
changeset

1052 

48556
62a3fbf9d35b
replace abel_cancel simprocs with functionally equivalent, but simpler and faster ones
huffman
parents:
45548
diff
changeset

1053 
simproc_setup group_cancel_le ("a \<le> (b::'a::ordered_ab_group_add)") = 
60758  1054 
\<open>fn phi => fn ss => try Group_Cancel.cancel_le_conv\<close> 
48556
62a3fbf9d35b
replace abel_cancel simprocs with functionally equivalent, but simpler and faster ones
huffman
parents:
45548
diff
changeset

1055 

62a3fbf9d35b
replace abel_cancel simprocs with functionally equivalent, but simpler and faster ones
huffman
parents:
45548
diff
changeset

1056 
simproc_setup group_cancel_less ("a < (b::'a::ordered_ab_group_add)") = 
60758  1057 
\<open>fn phi => fn ss => try Group_Cancel.cancel_less_conv\<close> 
37884
314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
36977
diff
changeset

1058 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

1059 
class linordered_ab_semigroup_add = 
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

1060 
linorder + ordered_ab_semigroup_add 
25062  1061 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

1062 
class linordered_cancel_ab_semigroup_add = 
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

1063 
linorder + ordered_cancel_ab_semigroup_add 
25267  1064 
begin 
25062  1065 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

1066 
subclass linordered_ab_semigroup_add .. 
25062  1067 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

1068 
subclass ordered_ab_semigroup_add_imp_le 
28823  1069 
proof 
25062  1070 
fix a b c :: 'a 
1071 
assume le: "c + a <= c + b" 

1072 
show "a <= b" 

1073 
proof (rule ccontr) 

1074 
assume w: "~ a \<le> b" 

1075 
hence "b <= a" by (simp add: linorder_not_le) 

1076 
hence le2: "c + b <= c + a" by (rule add_left_mono) 

1077 
have "a = b" 

1078 
apply (insert le) 

1079 
apply (insert le2) 

1080 
apply (drule antisym, simp_all) 

1081 
done 

1082 
with w show False 

1083 
by (simp add: linorder_not_le [symmetric]) 

1084 
qed 

1085 
qed 

1086 

25267  1087 
end 
1088 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

1089 
class linordered_ab_group_add = linorder + ordered_ab_group_add 
25267  1090 
begin 
25230  1091 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

1092 
subclass linordered_cancel_ab_semigroup_add .. 
25230  1093 

35036
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1094 
lemma equal_neg_zero [simp]: 
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1095 
"a =  a \<longleftrightarrow> a = 0" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1096 
proof 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1097 
assume "a = 0" then show "a =  a" by simp 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1098 
next 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1099 
assume A: "a =  a" show "a = 0" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1100 
proof (cases "0 \<le> a") 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1101 
case True with A have "0 \<le>  a" by auto 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1102 
with le_minus_iff have "a \<le> 0" by simp 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1103 
with True show ?thesis by (auto intro: order_trans) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1104 
next 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1105 
case False then have B: "a \<le> 0" by auto 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1106 
with A have " a \<le> 0" by auto 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1107 
with B show ?thesis by (auto intro: order_trans) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1108 
qed 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1109 
qed 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1110 

35036
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1111 
lemma neg_equal_zero [simp]: 
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1112 
" a = a \<longleftrightarrow> a = 0" 
35036
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1113 
by (auto dest: sym) 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1114 

54250  1115 
lemma neg_less_eq_nonneg [simp]: 
1116 
" a \<le> a \<longleftrightarrow> 0 \<le> a" 

1117 
proof 

1118 
assume A: " a \<le> a" show "0 \<le> a" 

1119 
proof (rule classical) 

1120 
assume "\<not> 0 \<le> a" 

1121 
then have "a < 0" by auto 

1122 
with A have " a < 0" by (rule le_less_trans) 

1123 
then show ?thesis by auto 

1124 
qed 

1125 
next 

1126 
assume A: "0 \<le> a" show " a \<le> a" 

1127 
proof (rule order_trans) 

1128 
show " a \<le> 0" using A by (simp add: minus_le_iff) 

1129 
next 

1130 
show "0 \<le> a" using A . 

1131 
qed 

1132 
qed 

1133 

1134 
lemma neg_less_pos [simp]: 

1135 
" a < a \<longleftrightarrow> 0 < a" 

1136 
by (auto simp add: less_le) 

1137 

1138 
lemma less_eq_neg_nonpos [simp]: 

1139 
"a \<le>  a \<longleftrightarrow> a \<le> 0" 

1140 
using neg_less_eq_nonneg [of " a"] by simp 

1141 

1142 
lemma less_neg_neg [simp]: 

1143 
"a <  a \<longleftrightarrow> a < 0" 

1144 
using neg_less_pos [of " a"] by simp 

1145 

35036
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1146 
lemma double_zero [simp]: 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1147 
"a + a = 0 \<longleftrightarrow> a = 0" 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1148 
proof 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1149 
assume assm: "a + a = 0" 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1150 
then have a: " a = a" by (rule minus_unique) 
35216  1151 
then show "a = 0" by (simp only: neg_equal_zero) 
35036
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1152 
qed simp 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1153 

b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1154 
lemma double_zero_sym [simp]: 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1155 
"0 = a + a \<longleftrightarrow> a = 0" 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1156 
by (rule, drule sym) simp_all 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1157 

b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1158 
lemma zero_less_double_add_iff_zero_less_single_add [simp]: 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1159 
"0 < a + a \<longleftrightarrow> 0 < a" 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1160 
proof 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1161 
assume "0 < a + a" 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1162 
then have "0  a < a" by (simp only: diff_less_eq) 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1163 
then have " a < a" by simp 
54250  1164 
then show "0 < a" by simp 
35036
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1165 
next 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1166 
assume "0 < a" 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1167 
with this have "0 + 0 < a + a" 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1168 
by (rule add_strict_mono) 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1169 
then show "0 < a + a" by simp 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1170 
qed 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1171 

b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1172 
lemma zero_le_double_add_iff_zero_le_single_add [simp]: 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1173 
"0 \<le> a + a \<longleftrightarrow> 0 \<le> a" 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1174 
by (auto simp add: le_less) 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1175 

b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1176 
lemma double_add_less_zero_iff_single_add_less_zero [simp]: 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1177 
"a + a < 0 \<longleftrightarrow> a < 0" 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1178 
proof  
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1179 
have "\<not> a + a < 0 \<longleftrightarrow> \<not> a < 0" 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1180 
by (simp add: not_less) 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1181 
then show ?thesis by simp 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1182 
qed 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1183 

b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1184 
lemma double_add_le_zero_iff_single_add_le_zero [simp]: 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1185 
"a + a \<le> 0 \<longleftrightarrow> a \<le> 0" 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1186 
proof  
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1187 
have "\<not> a + a \<le> 0 \<longleftrightarrow> \<not> a \<le> 0" 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1188 
by (simp add: not_le) 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1189 
then show ?thesis by simp 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1190 
qed 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1191 

b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1192 
lemma minus_max_eq_min: 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1193 
" max x y = min (x) (y)" 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1194 
by (auto simp add: max_def min_def) 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1195 

b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1196 
lemma minus_min_eq_max: 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1197 
" min x y = max (x) (y)" 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1198 
by (auto simp add: max_def min_def) 
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1199 

25267  1200 
end 
1201 

35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1202 
class abs = 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1203 
fixes abs :: "'a \<Rightarrow> 'a" 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1204 
begin 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1205 

cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1206 
notation (xsymbols) 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1207 
abs ("\<bar>_\<bar>") 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1208 

cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1209 
notation (HTML output) 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1210 
abs ("\<bar>_\<bar>") 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1211 

cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1212 
end 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1213 

cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1214 
class sgn = 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1215 
fixes sgn :: "'a \<Rightarrow> 'a" 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1216 

cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1217 
class abs_if = minus + uminus + ord + zero + abs + 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1218 
assumes abs_if: "\<bar>a\<bar> = (if a < 0 then  a else a)" 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1219 

cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1220 
class sgn_if = minus + uminus + zero + one + ord + sgn + 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1221 
assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else  1)" 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1222 
begin 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1223 

cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1224 
lemma sgn0 [simp]: "sgn 0 = 0" 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1225 
by (simp add:sgn_if) 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1226 

cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1227 
end 
14738  1228 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

1229 
class ordered_ab_group_add_abs = ordered_ab_group_add + abs + 
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1230 
assumes abs_ge_zero [simp]: "\<bar>a\<bar> \<ge> 0" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1231 
and abs_ge_self: "a \<le> \<bar>a\<bar>" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1232 
and abs_leI: "a \<le> b \<Longrightarrow>  a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1233 
and abs_minus_cancel [simp]: "\<bar>a\<bar> = \<bar>a\<bar>" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1234 
and abs_triangle_ineq: "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1235 
begin 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1236 

25307  1237 
lemma abs_minus_le_zero: " \<bar>a\<bar> \<le> 0" 
1238 
unfolding neg_le_0_iff_le by simp 

1239 

1240 
lemma abs_of_nonneg [simp]: 

29667  1241 
assumes nonneg: "0 \<le> a" shows "\<bar>a\<bar> = a" 
25307  1242 
proof (rule antisym) 
1243 
from nonneg le_imp_neg_le have " a \<le> 0" by simp 

1244 
from this nonneg have " a \<le> a" by (rule order_trans) 

1245 
then show "\<bar>a\<bar> \<le> a" by (auto intro: abs_leI) 

1246 
qed (rule abs_ge_self) 

1247 

1248 
lemma abs_idempotent [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>" 

29667  1249 
by (rule antisym) 
36302  1250 
(auto intro!: abs_ge_self abs_leI order_trans [of " \<bar>a\<bar>" 0 "\<bar>a\<bar>"]) 
25307  1251 

1252 
lemma abs_eq_0 [simp]: "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0" 

1253 
proof  

1254 
have "\<bar>a\<bar> = 0 \<Longrightarrow> a = 0" 

1255 
proof (rule antisym) 

1256 
assume zero: "\<bar>a\<bar> = 0" 

1257 
with abs_ge_self show "a \<le> 0" by auto 

1258 
from zero have "\<bar>a\<bar> = 0" by simp 

36302  1259 
with abs_ge_self [of " a"] have " a \<le> 0" by auto 
25307  1260 
with neg_le_0_iff_le show "0 \<le> a" by auto 
1261 
qed 

1262 
then show ?thesis by auto 

1263 
qed 

1264 

25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1265 
lemma abs_zero [simp]: "\<bar>0\<bar> = 0" 
29667  1266 
by simp 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16417
diff
changeset

1267 

54148  1268 
lemma abs_0_eq [simp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0" 
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1269 
proof  
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1270 
have "0 = \<bar>a\<bar> \<longleftrightarrow> \<bar>a\<bar> = 0" by (simp only: eq_ac) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1271 
thus ?thesis by simp 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1272 
qed 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1273 

0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1274 
lemma abs_le_zero_iff [simp]: "\<bar>a\<bar> \<le> 0 \<longleftrightarrow> a = 0" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1275 
proof 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1276 
assume "\<bar>a\<bar> \<le> 0" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1277 
then have "\<bar>a\<bar> = 0" by (rule antisym) simp 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1278 
thus "a = 0" by simp 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1279 
next 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1280 
assume "a = 0" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1281 
thus "\<bar>a\<bar> \<le> 0" by simp 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1282 
qed 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1283 

0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1284 
lemma zero_less_abs_iff [simp]: "0 < \<bar>a\<bar> \<longleftrightarrow> a \<noteq> 0" 
29667  1285 
by (simp add: less_le) 
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1286 

0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1287 
lemma abs_not_less_zero [simp]: "\<not> \<bar>a\<bar> < 0" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1288 
proof  
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1289 
have a: "\<And>x y. x \<le> y \<Longrightarrow> \<not> y < x" by auto 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1290 
show ?thesis by (simp add: a) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1291 
qed 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16417
diff
changeset

1292 

25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1293 
lemma abs_ge_minus_self: " a \<le> \<bar>a\<bar>" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1294 
proof  
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1295 
have " a \<le> \<bar>a\<bar>" by (rule abs_ge_self) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1296 
then show ?thesis by simp 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1297 
qed 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1298 

0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
