author  haftmann 
Fri, 19 Feb 2010 14:47:01 +0100  
changeset 35267  8dfd816713c6 
parent 35216  7641e8d831d2 
child 35301  90e42f9ba4d1 
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 

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

5 
header {* Groups, also combined with orderings *} 
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 
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

9 
uses ("~~/src/Provers/Arith/abel_cancel.ML") 
15131  10 
begin 
14738  11 

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

12 
subsection {* Generic operations *} 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

13 

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

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

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

16 

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

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

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

19 

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

20 
hide (open) const zero one 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

21 

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

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

23 
"_index1" :: index ("\<^sub>1") 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

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

25 
(index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>" 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

26 

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

27 
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

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

29 

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

30 
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

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

32 

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

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

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

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

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

37 
 _ => false) 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

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

39 

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

40 
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

41 
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

42 

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

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

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

45 
fun tr' c = (c, fn show_sorts => fn T => fn ts => 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

46 
if (not o null) ts orelse T = dummyT 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

47 
orelse not (! show_types) andalso can Term.dest_Type T 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

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

49 
else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T); 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

50 
in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end; 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

51 
*}  {* show types that are presumably too general *} 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

52 

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

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

54 
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

55 

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

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

57 
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

58 

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

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

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

61 

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

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

63 
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

64 

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

65 
use "~~/src/Provers/Arith/abel_cancel.ML" 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

66 

14738  67 
text {* 
68 
The theory of partially ordered groups is taken from the books: 

69 
\begin{itemize} 

70 
\item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979 

71 
\item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963 

72 
\end{itemize} 

73 
Most of the used notions can also be looked up in 

74 
\begin{itemize} 

14770  75 
\item \url{http://www.mathworld.com} by Eric Weisstein et. al. 
14738  76 
\item \emph{Algebra I} by van der Waerden, Springer. 
77 
\end{itemize} 

78 
*} 

79 

31902  80 
ML {* 
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

81 
structure Algebra_Simps = Named_Thms( 
31902  82 
val name = "algebra_simps" 
83 
val description = "algebra simplification rules" 

84 
) 

29667  85 
*} 
86 

31902  87 
setup Algebra_Simps.setup 
29667  88 

89 
text{* The rewrites accumulated in @{text algebra_simps} deal with the 

90 
classical algebraic structures of groups, rings and family. They simplify 

91 
terms by multiplying everything out (in case of a ring) and bringing sums and 

92 
products into a canonical form (by ordered rewriting). As a result it decides 

93 
group and ring equalities but also helps with inequalities. 

94 

95 
Of course it also works for fields, but it knows nothing about multiplicative 

96 
inverses or division. This is catered for by @{text field_simps}. *} 

97 

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

98 

23085  99 
subsection {* Semigroups and Monoids *} 
14738  100 

22390  101 
class semigroup_add = plus + 
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

102 
assumes add_assoc [algebra_simps]: "(a + b) + c = a + (b + c)" 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

103 

ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

104 
sublocale semigroup_add < plus!: semigroup plus proof 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

105 
qed (fact add_assoc) 
22390  106 

107 
class ab_semigroup_add = semigroup_add + 

34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

108 
assumes add_commute [algebra_simps]: "a + b = b + a" 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

109 

ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

110 
sublocale ab_semigroup_add < plus!: abel_semigroup plus proof 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

111 
qed (fact add_commute) 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

112 

ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

113 
context ab_semigroup_add 
25062  114 
begin 
14738  115 

34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

116 
lemmas add_left_commute [algebra_simps] = plus.left_commute 
25062  117 

118 
theorems add_ac = add_assoc add_commute add_left_commute 

119 

120 
end 

14738  121 

122 
theorems add_ac = add_assoc add_commute add_left_commute 

123 

22390  124 
class semigroup_mult = times + 
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

125 
assumes mult_assoc [algebra_simps]: "(a * b) * c = a * (b * c)" 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

126 

ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

127 
sublocale semigroup_mult < times!: semigroup times proof 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

128 
qed (fact mult_assoc) 
14738  129 

22390  130 
class ab_semigroup_mult = semigroup_mult + 
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

131 
assumes mult_commute [algebra_simps]: "a * b = b * a" 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

132 

ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

133 
sublocale ab_semigroup_mult < times!: abel_semigroup times proof 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

134 
qed (fact mult_commute) 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

135 

ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

136 
context ab_semigroup_mult 
23181  137 
begin 
14738  138 

34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

139 
lemmas mult_left_commute [algebra_simps] = times.left_commute 
25062  140 

141 
theorems mult_ac = mult_assoc mult_commute mult_left_commute 

23181  142 

143 
end 

14738  144 

145 
theorems mult_ac = mult_assoc mult_commute mult_left_commute 

146 

26015  147 
class ab_semigroup_idem_mult = ab_semigroup_mult + 
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

148 
assumes mult_idem: "x * x = x" 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

149 

ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

150 
sublocale ab_semigroup_idem_mult < times!: semilattice times proof 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

151 
qed (fact mult_idem) 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

152 

ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

153 
context ab_semigroup_idem_mult 
26015  154 
begin 
155 

34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

156 
lemmas mult_left_idem = times.left_idem 
26015  157 

158 
end 

159 

23085  160 
class monoid_add = zero + semigroup_add + 
25062  161 
assumes add_0_left [simp]: "0 + a = a" 
162 
and add_0_right [simp]: "a + 0 = a" 

23085  163 

26071  164 
lemma zero_reorient: "0 = x \<longleftrightarrow> x = 0" 
29667  165 
by (rule eq_commute) 
26071  166 

22390  167 
class comm_monoid_add = zero + ab_semigroup_add + 
25062  168 
assumes add_0: "0 + a = a" 
169 
begin 

23085  170 

25062  171 
subclass monoid_add 
28823  172 
proof qed (insert add_0, simp_all add: add_commute) 
25062  173 

174 
end 

14738  175 

22390  176 
class monoid_mult = one + semigroup_mult + 
25062  177 
assumes mult_1_left [simp]: "1 * a = a" 
178 
assumes mult_1_right [simp]: "a * 1 = a" 

14738  179 

26071  180 
lemma one_reorient: "1 = x \<longleftrightarrow> x = 1" 
29667  181 
by (rule eq_commute) 
26071  182 

22390  183 
class comm_monoid_mult = one + ab_semigroup_mult + 
25062  184 
assumes mult_1: "1 * a = a" 
185 
begin 

14738  186 

25062  187 
subclass monoid_mult 
28823  188 
proof qed (insert mult_1, simp_all add: mult_commute) 
25062  189 

190 
end 

14738  191 

22390  192 
class cancel_semigroup_add = semigroup_add + 
25062  193 
assumes add_left_imp_eq: "a + b = a + c \<Longrightarrow> b = c" 
194 
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

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

196 

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

197 
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

198 
"a + b = a + c \<longleftrightarrow> b = c" 
29667  199 
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

200 

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

201 
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

202 
"b + a = c + a \<longleftrightarrow> b = c" 
29667  203 
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

204 

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

205 
end 
14738  206 

22390  207 
class cancel_ab_semigroup_add = ab_semigroup_add + 
25062  208 
assumes add_imp_eq: "a + b = a + c \<Longrightarrow> b = c" 
25267  209 
begin 
14738  210 

25267  211 
subclass cancel_semigroup_add 
28823  212 
proof 
22390  213 
fix a b c :: 'a 
214 
assume "a + b = a + c" 

215 
then show "b = c" by (rule add_imp_eq) 

216 
next 

14738  217 
fix a b c :: 'a 
218 
assume "b + a = c + a" 

22390  219 
then have "a + b = a + c" by (simp only: add_commute) 
220 
then show "b = c" by (rule add_imp_eq) 

14738  221 
qed 
222 

25267  223 
end 
224 

29904  225 
class cancel_comm_monoid_add = cancel_ab_semigroup_add + comm_monoid_add 
226 

227 

23085  228 
subsection {* Groups *} 
229 

25762  230 
class group_add = minus + uminus + monoid_add + 
25062  231 
assumes left_minus [simp]: " a + a = 0" 
232 
assumes diff_minus: "a  b = a + ( b)" 

233 
begin 

23085  234 

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

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

236 
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

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

238 
have " a =  a + (a + b)" using assms by simp 
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

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

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

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

242 

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

243 
lemmas equals_zero_I = minus_unique (* legacy name *) 
14738  244 

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

247 
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

248 
thus " 0 = 0" by (rule minus_unique) 
14738  249 
qed 
250 

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

253 
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

254 
thus " ( a) = a" by (rule minus_unique) 
23085  255 
qed 
14738  256 

25062  257 
lemma right_minus [simp]: "a +  a = 0" 
14738  258 
proof  
25062  259 
have "a +  a =  ( a) +  a" by simp 
260 
also have "\<dots> = 0" by (rule left_minus) 

14738  261 
finally show ?thesis . 
262 
qed 

263 

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

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

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

266 

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

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

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

269 

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

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

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

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

273 
by (simp add: add_assoc add_minus_cancel) 
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

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

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

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

277 

25062  278 
lemma right_minus_eq: "a  b = 0 \<longleftrightarrow> a = b" 
14738  279 
proof 
23085  280 
assume "a  b = 0" 
281 
have "a = (a  b) + b" by (simp add:diff_minus add_assoc) 

282 
also have "\<dots> = b" using `a  b = 0` by simp 

283 
finally show "a = b" . 

14738  284 
next 
23085  285 
assume "a = b" thus "a  b = 0" by (simp add: diff_minus) 
14738  286 
qed 
287 

25062  288 
lemma diff_self [simp]: "a  a = 0" 
29667  289 
by (simp add: diff_minus) 
14738  290 

25062  291 
lemma diff_0 [simp]: "0  a =  a" 
29667  292 
by (simp add: diff_minus) 
14738  293 

25062  294 
lemma diff_0_right [simp]: "a  0 = a" 
29667  295 
by (simp add: diff_minus) 
14738  296 

25062  297 
lemma diff_minus_eq_add [simp]: "a   b = a + b" 
29667  298 
by (simp add: diff_minus) 
14738  299 

25062  300 
lemma neg_equal_iff_equal [simp]: 
301 
" a =  b \<longleftrightarrow> a = b" 

14738  302 
proof 
303 
assume " a =  b" 

29667  304 
hence " ( a) =  ( b)" by simp 
25062  305 
thus "a = b" by simp 
14738  306 
next 
25062  307 
assume "a = b" 
308 
thus " a =  b" by simp 

14738  309 
qed 
310 

25062  311 
lemma neg_equal_0_iff_equal [simp]: 
312 
" a = 0 \<longleftrightarrow> a = 0" 

29667  313 
by (subst neg_equal_iff_equal [symmetric], simp) 
14738  314 

25062  315 
lemma neg_0_equal_iff_equal [simp]: 
316 
"0 =  a \<longleftrightarrow> 0 = a" 

29667  317 
by (subst neg_equal_iff_equal [symmetric], simp) 
14738  318 

319 
text{*The next two equations can make the simplifier loop!*} 

320 

25062  321 
lemma equation_minus_iff: 
322 
"a =  b \<longleftrightarrow> b =  a" 

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

326 
qed 

327 

328 
lemma minus_equation_iff: 

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

330 
proof  

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

14738  332 
thus ?thesis by (simp add: eq_commute) 
333 
qed 

334 

28130
32b4185bfdc7
move diff_add_cancel, add_diff_cancel from class ab_group_add to group_add
huffman
parents:
27516
diff
changeset

335 
lemma diff_add_cancel: "a  b + b = a" 
29667  336 
by (simp add: diff_minus add_assoc) 
28130
32b4185bfdc7
move diff_add_cancel, add_diff_cancel from class ab_group_add to group_add
huffman
parents:
27516
diff
changeset

337 

32b4185bfdc7
move diff_add_cancel, add_diff_cancel from class ab_group_add to group_add
huffman
parents:
27516
diff
changeset

338 
lemma add_diff_cancel: "a + b  b = a" 
29667  339 
by (simp add: diff_minus add_assoc) 
340 

341 
declare diff_minus[symmetric, algebra_simps] 

28130
32b4185bfdc7
move diff_add_cancel, add_diff_cancel from class ab_group_add to group_add
huffman
parents:
27516
diff
changeset

342 

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

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

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

345 
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

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

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

348 
moreover have "a + (b +  b) = (a + b) +  b" 
c9ced4f54e82
generalize lemma eq_neg_iff_add_eq_0, and move to OrderedGroup
huffman
parents:
29904
diff
changeset

349 
by (simp only: add_assoc) 
c9ced4f54e82
generalize lemma eq_neg_iff_add_eq_0, and move to OrderedGroup
huffman
parents:
29904
diff
changeset

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

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

352 

25062  353 
end 
354 

25762  355 
class ab_group_add = minus + uminus + comm_monoid_add + 
25062  356 
assumes ab_left_minus: " a + a = 0" 
357 
assumes ab_diff_minus: "a  b = a + ( b)" 

25267  358 
begin 
25062  359 

25267  360 
subclass group_add 
28823  361 
proof qed (simp_all add: ab_left_minus ab_diff_minus) 
25062  362 

29904  363 
subclass cancel_comm_monoid_add 
28823  364 
proof 
25062  365 
fix a b c :: 'a 
366 
assume "a + b = a + c" 

367 
then have " a + a + b =  a + a + c" 

368 
unfolding add_assoc by simp 

369 
then show "b = c" by simp 

370 
qed 

371 

29667  372 
lemma uminus_add_conv_diff[algebra_simps]: 
25062  373 
" a + b = b  a" 
29667  374 
by (simp add:diff_minus add_commute) 
25062  375 

376 
lemma minus_add_distrib [simp]: 

377 
" (a + b) =  a +  b" 

34146
14595e0c27e8
rename equals_zero_I to minus_unique (keep old name too)
huffman
parents:
33364
diff
changeset

378 
by (rule minus_unique) (simp add: add_ac) 
25062  379 

380 
lemma minus_diff_eq [simp]: 

381 
" (a  b) = b  a" 

29667  382 
by (simp add: diff_minus add_commute) 
25077  383 

29667  384 
lemma add_diff_eq[algebra_simps]: "a + (b  c) = (a + b)  c" 
385 
by (simp add: diff_minus add_ac) 

25077  386 

29667  387 
lemma diff_add_eq[algebra_simps]: "(a  b) + c = (a + c)  b" 
388 
by (simp add: diff_minus add_ac) 

25077  389 

29667  390 
lemma diff_eq_eq[algebra_simps]: "a  b = c \<longleftrightarrow> a = c + b" 
391 
by (auto simp add: diff_minus add_assoc) 

25077  392 

29667  393 
lemma eq_diff_eq[algebra_simps]: "a = c  b \<longleftrightarrow> a + b = c" 
394 
by (auto simp add: diff_minus add_assoc) 

25077  395 

29667  396 
lemma diff_diff_eq[algebra_simps]: "(a  b)  c = a  (b + c)" 
397 
by (simp add: diff_minus add_ac) 

25077  398 

29667  399 
lemma diff_diff_eq2[algebra_simps]: "a  (b  c) = (a + c)  b" 
400 
by (simp add: diff_minus add_ac) 

25077  401 

402 
lemma eq_iff_diff_eq_0: "a = b \<longleftrightarrow> a  b = 0" 

29667  403 
by (simp add: algebra_simps) 
25077  404 

35216  405 
(* FIXME: duplicates right_minus_eq from class group_add *) 
406 
(* but only this one is declared as a simp rule. *) 

30629  407 
lemma diff_eq_0_iff_eq [simp, noatp]: "a  b = 0 \<longleftrightarrow> a = b" 
408 
by (simp add: algebra_simps) 

409 

25062  410 
end 
14738  411 

412 
subsection {* (Partially) Ordered Groups *} 

413 

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

414 
class ordered_ab_semigroup_add = order + ab_semigroup_add + 
25062  415 
assumes add_left_mono: "a \<le> b \<Longrightarrow> c + a \<le> c + b" 
416 
begin 

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

417 

25062  418 
lemma add_right_mono: 
419 
"a \<le> b \<Longrightarrow> a + c \<le> b + c" 

29667  420 
by (simp add: add_commute [of _ c] add_left_mono) 
14738  421 

422 
text {* nonstrict, in both arguments *} 

423 
lemma add_mono: 

25062  424 
"a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c \<le> b + d" 
14738  425 
apply (erule add_right_mono [THEN order_trans]) 
426 
apply (simp add: add_commute add_left_mono) 

427 
done 

428 

25062  429 
end 
430 

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

431 
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

432 
ordered_ab_semigroup_add + cancel_ab_semigroup_add 
25062  433 
begin 
434 

14738  435 
lemma add_strict_left_mono: 
25062  436 
"a < b \<Longrightarrow> c + a < c + b" 
29667  437 
by (auto simp add: less_le add_left_mono) 
14738  438 

439 
lemma add_strict_right_mono: 

25062  440 
"a < b \<Longrightarrow> a + c < b + c" 
29667  441 
by (simp add: add_commute [of _ c] add_strict_left_mono) 
14738  442 

443 
text{*Strict monotonicity in both arguments*} 

25062  444 
lemma add_strict_mono: 
445 
"a < b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d" 

446 
apply (erule add_strict_right_mono [THEN less_trans]) 

14738  447 
apply (erule add_strict_left_mono) 
448 
done 

449 

450 
lemma add_less_le_mono: 

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

453 
apply (erule add_left_mono) 

14738  454 
done 
455 

456 
lemma add_le_less_mono: 

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

14738  459 
apply (erule add_strict_left_mono) 
460 
done 

461 

25062  462 
end 
463 

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

464 
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

465 
ordered_cancel_ab_semigroup_add + 
25062  466 
assumes add_le_imp_le_left: "c + a \<le> c + b \<Longrightarrow> a \<le> b" 
467 
begin 

468 

14738  469 
lemma add_less_imp_less_left: 
29667  470 
assumes less: "c + a < c + b" shows "a < b" 
14738  471 
proof  
472 
from less have le: "c + a <= c + b" by (simp add: order_le_less) 

473 
have "a <= b" 

474 
apply (insert le) 

475 
apply (drule add_le_imp_le_left) 

476 
by (insert le, drule add_le_imp_le_left, assumption) 

477 
moreover have "a \<noteq> b" 

478 
proof (rule ccontr) 

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

480 
then have "a = b" by simp 

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

482 
with less show "False"by simp 

483 
qed 

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

485 
qed 

486 

487 
lemma add_less_imp_less_right: 

25062  488 
"a + c < b + c \<Longrightarrow> a < b" 
14738  489 
apply (rule add_less_imp_less_left [of c]) 
490 
apply (simp add: add_commute) 

491 
done 

492 

493 
lemma add_less_cancel_left [simp]: 

25062  494 
"c + a < c + b \<longleftrightarrow> a < b" 
29667  495 
by (blast intro: add_less_imp_less_left add_strict_left_mono) 
14738  496 

497 
lemma add_less_cancel_right [simp]: 

25062  498 
"a + c < b + c \<longleftrightarrow> a < b" 
29667  499 
by (blast intro: add_less_imp_less_right add_strict_right_mono) 
14738  500 

501 
lemma add_le_cancel_left [simp]: 

25062  502 
"c + a \<le> c + b \<longleftrightarrow> a \<le> b" 
29667  503 
by (auto, drule add_le_imp_le_left, simp_all add: add_left_mono) 
14738  504 

505 
lemma add_le_cancel_right [simp]: 

25062  506 
"a + c \<le> b + c \<longleftrightarrow> a \<le> b" 
29667  507 
by (simp add: add_commute [of a c] add_commute [of b c]) 
14738  508 

509 
lemma add_le_imp_le_right: 

25062  510 
"a + c \<le> b + c \<Longrightarrow> a \<le> b" 
29667  511 
by simp 
25062  512 

25077  513 
lemma max_add_distrib_left: 
514 
"max x y + z = max (x + z) (y + z)" 

515 
unfolding max_def by auto 

516 

517 
lemma min_add_distrib_left: 

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

519 
unfolding min_def by auto 

520 

25062  521 
end 
522 

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

523 
subsection {* Support for reasoning about signs *} 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

524 

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

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

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

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

528 

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

529 
lemma add_pos_nonneg: 
29667  530 
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

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

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

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

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

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

536 

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

537 
lemma add_pos_pos: 
29667  538 
assumes "0 < a" and "0 < b" shows "0 < a + b" 
539 
by (rule add_pos_nonneg) (insert assms, auto) 

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

540 

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

541 
lemma add_nonneg_pos: 
29667  542 
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

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

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

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

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

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

548 

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

549 
lemma add_nonneg_nonneg: 
29667  550 
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

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

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

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

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

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

556 

30691  557 
lemma add_neg_nonpos: 
29667  558 
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

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

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

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

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

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

564 

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

565 
lemma add_neg_neg: 
29667  566 
assumes "a < 0" and "b < 0" shows "a + b < 0" 
567 
by (rule add_neg_nonpos) (insert assms, auto) 

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

568 

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

569 
lemma add_nonpos_neg: 
29667  570 
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

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

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

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

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

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

576 

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

577 
lemma add_nonpos_nonpos: 
29667  578 
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

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

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

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

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

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

584 

30691  585 
lemmas add_sign_intros = 
586 
add_pos_nonneg add_pos_pos add_nonneg_pos add_nonneg_nonneg 

587 
add_neg_nonpos add_neg_neg add_nonpos_neg add_nonpos_nonpos 

588 

29886  589 
lemma add_nonneg_eq_0_iff: 
590 
assumes x: "0 \<le> x" and y: "0 \<le> y" 

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

592 
proof (intro iffI conjI) 

593 
have "x = x + 0" by simp 

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

595 
also assume "x + y = 0" 

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

597 
finally show "x = 0" . 

598 
next 

599 
have "y = 0 + y" by simp 

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

601 
also assume "x + y = 0" 

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

603 
finally show "y = 0" . 

604 
next 

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

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

607 
qed 

608 

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

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

610 

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

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

612 
ab_group_add + ordered_ab_semigroup_add 
25062  613 
begin 
614 

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

615 
subclass ordered_cancel_ab_semigroup_add .. 
25062  616 

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

617 
subclass ordered_ab_semigroup_add_imp_le 
28823  618 
proof 
25062  619 
fix a b c :: 'a 
620 
assume "c + a \<le> c + b" 

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

622 
hence "((c) + c) + a \<le> ((c) + c) + b" by (simp only: add_assoc) 

623 
thus "a \<le> b" by simp 

624 
qed 

625 

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

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

627 

25077  628 
lemma max_diff_distrib_left: 
629 
shows "max x y  z = max (x  z) (y  z)" 

29667  630 
by (simp add: diff_minus, rule max_add_distrib_left) 
25077  631 

632 
lemma min_diff_distrib_left: 

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

29667  634 
by (simp add: diff_minus, rule min_add_distrib_left) 
25077  635 

636 
lemma le_imp_neg_le: 

29667  637 
assumes "a \<le> b" shows "b \<le> a" 
25077  638 
proof  
29667  639 
have "a+a \<le> a+b" using `a \<le> b` by (rule add_left_mono) 
640 
hence "0 \<le> a+b" by simp 

641 
hence "0 + (b) \<le> (a + b) + (b)" by (rule add_right_mono) 

642 
thus ?thesis by (simp add: add_assoc) 

25077  643 
qed 
644 

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

646 
proof 

647 
assume " b \<le>  a" 

29667  648 
hence " ( a) \<le>  ( b)" by (rule le_imp_neg_le) 
25077  649 
thus "a\<le>b" by simp 
650 
next 

651 
assume "a\<le>b" 

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

653 
qed 

654 

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

29667  656 
by (subst neg_le_iff_le [symmetric], simp) 
25077  657 

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

29667  659 
by (subst neg_le_iff_le [symmetric], simp) 
25077  660 

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

29667  662 
by (force simp add: less_le) 
25077  663 

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

29667  665 
by (subst neg_less_iff_less [symmetric], simp) 
25077  666 

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

29667  668 
by (subst neg_less_iff_less [symmetric], simp) 
25077  669 

670 
text{*The next several equations can make the simplifier loop!*} 

671 

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

673 
proof  

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

675 
thus ?thesis by simp 

676 
qed 

677 

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

679 
proof  

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

681 
thus ?thesis by simp 

682 
qed 

683 

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

685 
proof  

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

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

688 
apply (auto simp only: le_less) 

689 
apply (drule mm) 

690 
apply (simp_all) 

691 
apply (drule mm[simplified], assumption) 

692 
done 

693 
then show ?thesis by simp 

694 
qed 

695 

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

29667  697 
by (auto simp add: le_less minus_less_iff) 
25077  698 

699 
lemma less_iff_diff_less_0: "a < b \<longleftrightarrow> a  b < 0" 

700 
proof  

701 
have "(a < b) = (a + ( b) < b + (b))" 

702 
by (simp only: add_less_cancel_right) 

703 
also have "... = (a  b < 0)" by (simp add: diff_minus) 

704 
finally show ?thesis . 

705 
qed 

706 

29667  707 
lemma diff_less_eq[algebra_simps]: "a  b < c \<longleftrightarrow> a < c + b" 
25077  708 
apply (subst less_iff_diff_less_0 [of a]) 
709 
apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst]) 

710 
apply (simp add: diff_minus add_ac) 

711 
done 

712 

29667  713 
lemma less_diff_eq[algebra_simps]: "a < c  b \<longleftrightarrow> a + b < c" 
25077  714 
apply (subst less_iff_diff_less_0 [of "plus a b"]) 
715 
apply (subst less_iff_diff_less_0 [of a]) 

716 
apply (simp add: diff_minus add_ac) 

717 
done 

718 

29667  719 
lemma diff_le_eq[algebra_simps]: "a  b \<le> c \<longleftrightarrow> a \<le> c + b" 
720 
by (auto simp add: le_less diff_less_eq diff_add_cancel add_diff_cancel) 

25077  721 

29667  722 
lemma le_diff_eq[algebra_simps]: "a \<le> c  b \<longleftrightarrow> a + b \<le> c" 
723 
by (auto simp add: le_less less_diff_eq diff_add_cancel add_diff_cancel) 

25077  724 

725 
lemma le_iff_diff_le_0: "a \<le> b \<longleftrightarrow> a  b \<le> 0" 

29667  726 
by (simp add: algebra_simps) 
25077  727 

29667  728 
text{*Legacy  use @{text algebra_simps} *} 
29833  729 
lemmas group_simps[noatp] = algebra_simps 
25230  730 

25077  731 
end 
732 

29667  733 
text{*Legacy  use @{text algebra_simps} *} 
29833  734 
lemmas group_simps[noatp] = algebra_simps 
25230  735 

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

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

737 
linorder + ordered_ab_semigroup_add 
25062  738 

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

739 
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

740 
linorder + ordered_cancel_ab_semigroup_add 
25267  741 
begin 
25062  742 

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

743 
subclass linordered_ab_semigroup_add .. 
25062  744 

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

745 
subclass ordered_ab_semigroup_add_imp_le 
28823  746 
proof 
25062  747 
fix a b c :: 'a 
748 
assume le: "c + a <= c + b" 

749 
show "a <= b" 

750 
proof (rule ccontr) 

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

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

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

754 
have "a = b" 

755 
apply (insert le) 

756 
apply (insert le2) 

757 
apply (drule antisym, simp_all) 

758 
done 

759 
with w show False 

760 
by (simp add: linorder_not_le [symmetric]) 

761 
qed 

762 
qed 

763 

25267  764 
end 
765 

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

766 
class linordered_ab_group_add = linorder + ordered_ab_group_add 
25267  767 
begin 
25230  768 

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

769 
subclass linordered_cancel_ab_semigroup_add .. 
25230  770 

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

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

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

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

774 
assume A: " a \<le> a" show "0 \<le> a" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

775 
proof (rule classical) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

776 
assume "\<not> 0 \<le> a" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

777 
then have "a < 0" by auto 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

778 
with A have " a < 0" by (rule le_less_trans) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

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

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

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

782 
assume A: "0 \<le> a" show " a \<le> a" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

783 
proof (rule order_trans) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

784 
show " a \<le> 0" using A by (simp add: minus_le_iff) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

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

786 
show "0 \<le> a" using A . 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

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

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

789 

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

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

791 
" 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

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

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

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

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

796 
then have "a \<le> 0" by auto 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

797 
with A have " a < 0" by (rule less_le_trans) 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

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

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

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

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

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

803 
show " a < 0" using A by (simp add: minus_le_iff) 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

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

805 
show "0 < a" using A . 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

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

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

808 

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

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

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

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

812 
assume A: "a \<le>  a" show "a \<le> 0" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

813 
proof (rule classical) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

814 
assume "\<not> a \<le> 0" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

815 
then have "0 < a" by auto 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

816 
then have "0 <  a" using A by (rule less_le_trans) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

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

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

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

820 
assume A: "a \<le> 0" show "a \<le>  a" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

821 
proof (rule order_trans) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

822 
show "0 \<le>  a" using A by (simp add: minus_le_iff) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

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

824 
show "a \<le> 0" using A . 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

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

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

827 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

844 

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

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

846 
" 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

847 
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

848 

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

849 
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

850 
"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

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

852 
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

853 
then have a: " a = a" by (rule minus_unique) 
35216  854 
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

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

856 

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

857 
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

858 
"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

859 
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

860 

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

861 
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

862 
"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

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

864 
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

865 
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

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

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

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

870 
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

871 
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

872 
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

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

874 

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

875 
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

876 
"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

877 
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

878 

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

879 
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

880 
"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

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

882 
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

883 
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

884 
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

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

886 

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

887 
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

888 
"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

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

890 
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

891 
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

892 
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

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

894 

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

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

896 
"a \<le>  a \<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

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

898 
from add_le_cancel_left [of " a" "a + a" 0] 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

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

900 
by (simp add: add_assoc [symmetric]) 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

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

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

903 

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

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

905 
" a \<le> 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

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

907 
from add_le_cancel_left [of " a" 0 "a + a"] 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

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

909 
by (simp add: add_assoc [symmetric]) 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

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

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

912 

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

913 
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

914 
" 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

915 
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

916 

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

917 
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

918 
" 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

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

920 

25267  921 
end 
922 

25077  923 
 {* FIXME localize the following *} 
14738  924 

15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

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

926 
fixes c :: "'a::{ordered_ab_semigroup_add_imp_le, comm_monoid_add}" 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

927 
shows "[0\<le>a; b\<le>c] ==> b \<le> a + c" 
14738  928 
by (insert add_mono [of 0 a b c], simp) 
929 

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

931 
fixes c :: "'a::{ordered_ab_semigroup_add_imp_le, comm_monoid_add}" 
15539  932 
shows "[0\<le>c; b\<le>a] ==> b \<le> a + c" 
933 
by (simp add:add_increasing add_commute[of a]) 

934 

15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

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

936 
fixes c :: "'a::{ordered_ab_semigroup_add_imp_le, comm_monoid_add}" 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

937 
shows "[0<a; b\<le>c] ==> b < a + c" 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

938 
by (insert add_less_le_mono [of 0 a b c], simp) 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

939 

ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

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

941 
fixes c :: "'a::{ordered_ab_semigroup_add_imp_le, comm_monoid_add}" 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

942 
shows "[0\<le>a; b<c] ==> b < a + c" 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

943 
by (insert add_le_less_mono [of 0 a b c], simp) 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

944 

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

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

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

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

948 

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

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

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

951 

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

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

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

954 

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

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

956 

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

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

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

959 

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

960 
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

961 
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

962 

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

963 
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

964 
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

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

966 

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

967 
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

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

969 

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

970 
end 
14738  971 

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

972 
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

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

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

975 
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

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

977 
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

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

979 

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

982 

983 
lemma abs_of_nonneg [simp]: 

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

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

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

989 
qed (rule abs_ge_self) 

990 

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

29667  992 
by (rule antisym) 
993 
(auto intro!: abs_ge_self abs_leI order_trans [of "uminus (abs a)" zero "abs a"]) 

25307  994 

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

996 
proof  

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

998 
proof (rule antisym) 

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

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

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

1002 
with abs_ge_self [of "uminus a"] have " a \<le> 0" by auto 

1003 
with neg_le_0_iff_le show "0 \<le> a" by auto 

1004 
qed 

1005 
then show ?thesis by auto 

1006 
qed 

1007 

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

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

1010 

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

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

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

1013 
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

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

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

1016 

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

1017 
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

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

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

1020 
then have "\<bar>a\<bar> = 0" by (rule antisym) simp 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1021 
thus "a = 0" by simp 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

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

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

1024 
thus "\<bar>a\<bar> \<le> 0" by simp 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

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

1026 

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

1027 
lemma zero_less_abs_iff [simp]: "0 < \<bar>a\<bar> \<longleftrightarrow> a \<noteq> 0" 
29667  1028 
by (simp add: less_le) 
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1029 

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

1030 
lemma abs_not_less_zero [simp]: "\<not> \<bar>a\<bar> < 0" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

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

1032 
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

1033 
show ?thesis by (simp add: a) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1034 
qed 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16417
diff
changeset

1035 

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

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

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

1038 
have " a \<le> \<bar>a\<bar>" by (rule abs_ge_self) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

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

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

1041 

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

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

1043 
"\<bar>a  b\<bar> = \<bar>b  a\<bar>" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

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

1045 
have "\<bar>a  b\<bar> = \<bar> (a  b)\<bar>" by (simp only: abs_minus_cancel) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1046 
also have "... = \<bar>b  a\<bar>" by simp 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1047 
finally show ?thesis . 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

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

1049 

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

1050 
lemma abs_of_pos: "0 < a \<Longrightarrow> \<bar>a\<bar> = a" 
29667  1051 
by (rule abs_of_nonneg, rule less_imp_le) 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16417
diff
changeset

1052 

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

1053 
lemma abs_of_nonpos [simp]: 
29667  1054 
assumes "a \<le> 0" shows "\<bar>a\<bar> =  a" 
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

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

1056 
let ?b = " a" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1057 
have " ?b \<le> 0 \<Longrightarrow> \<bar> ?b\<bar> =  ( ?b)" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1058 
unfolding abs_minus_cancel [of "?b"] 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1059 
unfolding neg_le_0_iff_le [of "?b"] 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1060 
unfolding minus_minus by (erule abs_of_nonneg) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1061 
then show ?thesis using assms by auto 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

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

1063 

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

1064 
lemma abs_of_neg: "a < 0 \<Longrightarrow> \<bar>a\<bar> =  a" 
29667  1065 
by (rule abs_of_nonpos, rule less_imp_le) 
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1066 

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

1067 
lemma abs_le_D1: "\<bar>a\<bar> \<le> b \<Longrightarrow> a \<le> b" 
29667  1068 
by (insert abs_ge_self, blast intro: order_trans) 
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1069 

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

1070 
lemma abs_le_D2: "\<bar>a\<bar> \<le> b \<Longrightarrow>  a \<le> b" 
29667  1071 
by (insert abs_le_D1 [of "uminus a"], simp) 
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1072 

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

1073 
lemma abs_le_iff: "\<bar>a\<bar> \<le> b \<longleftrightarrow> a \<le> b \<and>  a \<le> b" 
29667  1074 
by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2) 
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1075 

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

1076 
lemma abs_triangle_ineq2: "\<bar>a\<bar>  \<bar>b\<bar> \<le> \<bar>a  b\<bar>" 
29667  1077 
apply (simp add: algebra_simps) 
1078 
apply (subgoal_tac "abs a = abs (plus b (minus a b))") 

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

1079 
apply (erule ssubst) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1080 
apply (rule abs_triangle_ineq) 
29667  1081 
apply (rule arg_cong[of _ _ abs]) 
1082 
apply (simp add: algebra_simps) 

16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16417
diff
changeset

1083 
done 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16417
diff
changeset

1084 

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

1085 
lemma abs_triangle_ineq3: "\<bar>\<bar>a\<bar>  \<bar>b\<bar>\<bar> \<le> \<bar>a  b\<bar>" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1086 
apply (subst abs_le_iff) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

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

1088 
apply (rule abs_triangle_ineq2) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1089 
apply (subst abs_minus_commute) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1090 
apply (rule abs_triangle_ineq2) 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16417
diff
changeset

1091 
done 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16417
diff
changeset

1092 

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

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

1094 
proof  
29667  1095 
have "abs(a  b) = abs(a +  b)" by (subst diff_minus, rule refl) 
1096 
also have "... <= abs a + abs ( b)" by (rule abs_triangle_ineq) 

1097 
finally show ?thesis by simp 

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

1098 
qed 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16417
diff
changeset

1099 

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

1100 
lemma abs_diff_triangle_ineq: "\<bar>a + b  (c + d)\<bar> \<le> \<bar>a  c\<bar> + \<bar>b  d\<bar>" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

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

1102 
have "\<bar>a + b  (c+d)\<bar> = \<bar>(ac) + (bd)\<bar>" by (simp add: diff_minus add_ac) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1103 
also have "... \<le> \<bar>ac\<bar> + \<bar>bd\<bar>" by (rule abs_triangle_ineq) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1104 
finally show ?thesis . 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1105 
qed 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16417
diff
changeset

1106 

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

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

1108 
"\<bar>\<bar>a\<bar> + \<bar>b\<bar>\<bar> = \<bar>a\<bar> + \<bar>b\<bar>" (is "?L = ?R") 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1109 
proof (rule antisym) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1110 
show "?L \<ge> ?R" by(rule abs_ge_self) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

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

1112 
have "?L \<le> \<bar>\<bar>a\<bar>\<bar> + \<bar>\<bar>b\<bar>\<bar>" by(rule abs_triangle_ineq) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1113 
also have "\<dots> = ?R" by simp 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1114 
finally show "?L \<le> ?R" . 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

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

1116 

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

1117 
end 
14738  1118 

14754
a080eeeaec14
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
obua
parents:
14738
diff
changeset

1119 
text {* Needed for abelian cancellation simprocs: *} 
a080eeeaec14
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
obua
parents:
14738
diff
changeset

1120 

a080eeeaec14
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
obua
parents:
14738
diff
changeset

1121 
lemma add_cancel_21: "((x::'a::ab_group_add) + (y + z) = y + u) = (x + z = u)" 
a080eeeaec14
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
obua
parents:
14738
diff
changeset

1122 
apply (subst add_left_commute) 
a080eeeaec14
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
obua
parents:
14738
diff
changeset

1123 
apply (subst add_left_cancel) 
a080eeeaec14
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
obua
parents:
14738
diff
changeset

1124 
apply simp 
a080eeeaec14
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
obua
parents:
14738
diff
changeset

1125 
done 
a080eeeaec14
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
obua
parents:
14738
diff
changeset

1126 

a080eeeaec14
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
obua
parents:
14738
diff
changeset

1127 
lemma add_cancel_end: "(x + (y + z) = y) = (x =  (z::'a::ab_group_add))" 
a080eeeaec14
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
obua
parents:
14738
diff
changeset

1128 
apply (subst add_cancel_21[of _ _ _ 0, simplified]) 
a080eeeaec14
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
obua
parents:
14738
diff
changeset

1129 
apply (simp add: add_right_cancel[symmetric, of "x" "z" "z", simplified]) 
a080eeeaec14
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
obua
parents:
14738
diff
changeset

1130 
done 
a080eeeaec14
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
obua
parents:
14738
diff
changeset

1131 

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

1132 
lemma less_eqI: "(x::'a::ordered_ab_group_add)  y = x'  y' \<Longrightarrow> (x < y) = (x' < y')" 
14754
a080eeeaec14
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
obua
parents:
14738
diff
changeset

1133 
by (simp add: less_iff_diff_less_0[of x y] less_iff_diff_less_0[of x' y']) 
a080eeeaec14
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
obua
parents:
14738
diff
changeset

1134 

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

1135 
lemma le_eqI: "(x::'a::ordered_ab_group_add)  y = x'  y' \<Longrightarrow> (y <= x) = (y' <= x')" 
14754
a080eeeaec14
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
obua
parents:
14738
diff
changeset

1136 
apply (simp add: le_iff_diff_le_0[of y x] le_iff_diff_le_0[of y' x']) 
a080eeeaec14
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
obua
parents:
14738
diff
changeset

1137 
apply (simp add: neg_le_iff_le[symmetric, of "yx" 0] neg_le_iff_le[symmetric, of "y'x'" 0]) 
a080eeeaec14
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
obua
parents:
14738
diff
changeset

1138 
done 
a080eeeaec14
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
obua
parents:
14738
diff
changeset

1139 

a080eeeaec14
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
obua
parents:
14738
diff
changeset

1140 
lemma eq_eqI: "(x::'a::ab_group_add)  y = x'  y' \<Longrightarrow> (x = y) = (x' = y')" 
30629  1141 
by (simp only: eq_iff_diff_eq_0[of x y] eq_iff_diff_eq_0[of x' y']) 
14754
a080eeeaec14
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
obua
parents:
14738
diff
changeset

1142 

a080eeeaec14
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
obua
parents:
14738
diff
changeset

1143 
lemma diff_def: "(x::'a::ab_group_add)  y == x + (y)" 
a080eeeaec14
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
obua
parents:
14738
diff
changeset

1144 
by (simp add: diff_minus) 
a080eeeaec14
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
obua
parents:
14738
diff
changeset

1145 

25090  1146 
lemma le_add_right_mono: 
15178  1147 
assumes 
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

1148 
"a <= b + (c::'a::ordered_ab_group_add)" 
15178  1149 
"c <= d" 
1150 
shows "a <= b + d" 

1151 
apply (rule_tac order_trans[where y = "b+c"]) 

1152 
apply (simp_all add: prems) 

1153 
done 

1154 

1155 

25090  1156 
subsection {* Tools setup *} 
1157 

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

1158 
lemma add_mono_thms_linordered_semiring [noatp]: 
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

1159 
fixes i j k :: "'a\<Colon>ordered_ab_semigroup_add" 
25077  1160 
shows "i \<le> j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l" 
1161 
and "i = j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l" 

1162 
and "i \<le> j \<and> k = l \<Longrightarrow> i + k \<le> j + l" 

1163 
and "i = j \<and> k = l \<Longrightarrow> i + k = j + l" 

1164 
by (rule add_mono, clarify+)+ 

1165 

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

1166 
lemma add_mono_thms_linordered_field [noatp]: 
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

1167 
fixes i j k :: "'a\<Colon>ordered_cancel_ab_semigroup_add" 
25077  1168 
shows "i < j \<and> k = l \<Longrightarrow> i + k < j + l" 
1169 
and "i = j \<and> k < l \<Longrightarrow> i + k < j + l" 

1170 
and "i < j \<and> k \<le> l \<Longrightarrow> i + k < j + l" 

1171 
and "i \<le> j \<and> k < l \<Longrightarrow> i + k < j + l" 

1172 
and "i < j \<and> k < l \<Longrightarrow> i + k < j + l" 

1173 
by (auto intro: add_strict_right_mono add_strict_left_mono 

1174 
add_less_le_mono add_le_less_mono add_strict_mono) 

1175 

17085  1176 
text{*Simplification of @{term "xy < 0"}, etc.*} 
29833  1177 
lemmas diff_less_0_iff_less [simp, noatp] = less_iff_diff_less_0 [symmetric] 
1178 
lemmas diff_le_0_iff_le [simp, noatp] = le_iff_diff_le_0 [symmetric] 

17085  1179 

22482  1180 
ML {* 
27250  1181 
structure ab_group_add_cancel = Abel_Cancel 
1182 
( 

22482  1183 

1184 
(* term order for abelian groups *) 

1185 

1186 
fun agrp_ord (Const (a, _)) = find_index (fn a' => a = a') 

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

1187 
[@{const_name Groups.zero}, @{const_name Groups.plus}, 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

1188 
@{const_name Groups.uminus}, @{const_name Groups.minus}] 
22482  1189 
 agrp_ord _ = ~1; 
1190 

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

1191 
fun termless_agrp (a, b) = (TermOrd.term_lpo agrp_ord (a, b) = LESS); 
22482  1192 

1193 
local 

1194 
val ac1 = mk_meta_eq @{thm add_assoc}; 

1195 
val ac2 = mk_meta_eq @{thm add_commute}; 

1196 
val ac3 = mk_meta_eq @{thm add_left_commute}; 

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

1197 
fun solve_add_ac thy _ (_ $ (Const (@{const_name Groups.plus},_) $ _ $ _) $ _) = 
22482  1198 
SOME ac1 
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

1199 
 solve_add_ac thy _ (_ $ x $ (Const (@{const_name Groups.plus},_) $ y $ z)) = 
22482  1200 
if termless_agrp (y, x) then SOME ac3 else NONE 
1201 
 solve_add_ac thy _ (_ $ x $ y) = 

1202 
if termless_agrp (y, x) then SOME ac2 else NONE 

1203 
 solve_add_ac thy _ _ = NONE 

1204 
in 

32010  1205 
val add_ac_proc = Simplifier.simproc @{theory} 
22482  1206 
"add_ac_proc" ["x + y::'a::ab_semigroup_add"] solve_add_ac; 
1207 
end; 

1208 

27250  1209 
val eq_reflection = @{thm eq_reflection}; 
1210 

1211 
val T = @{typ "'a::ab_group_add"}; 

1212 

22482  1213 
val cancel_ss = HOL_basic_ss settermless termless_agrp 
1214 
addsimprocs [add_ac_proc] addsimps 

23085  1215 
[@{thm add_0_left}, @{thm add_0_right}, @{thm diff_def}, 
22482  1216 
@{thm minus_add_distrib}, @{thm minus_minus}, @{thm minus_zero}, 
1217 
@{thm right_minus}, @{thm left_minus}, @{thm add_minus_cancel}, 

1218 
@{thm minus_add_cancel}]; 

27250  1219 

1220 
val sum_pats = [@{cterm "x + y::'a::ab_group_add"}, @{cterm "x  y::'a::ab_group_add"}]; 

22482  1221 

22548  1222 
val eqI_rules = [@{thm less_eqI}, @{thm le_eqI}, @{thm eq_eqI}]; 
22482  1223 

1224 
val dest_eqI = 

1225 
fst o HOLogic.dest_bin "op =" HOLogic.boolT o HOLogic.dest_Trueprop o concl_of; 

1226 

27250  1227 
); 
22482  1228 
*} 
1229 

26480  1230 
ML {* 
22482  1231 
Addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]; 
1232 
*} 

17085  1233 

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

1235 
Groups Arith 
33364  1236 

1237 
code_modulename OCaml 

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

1238 
Groups Arith 
33364  1239 

1240 
code_modulename Haskell 

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

1241 
Groups Arith 
33364  1242 

14738  1243 
end 