author | haftmann |
Fri, 05 Feb 2010 14:33:50 +0100 | |
changeset 35028 | 108662d50512 |
parent 34973 | ae634fad947e |
child 35036 | b8c8d01cc20d |
permissions | -rw-r--r-- |
14770 | 1 |
(* Title: HOL/OrderedGroup.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 |
||
5 |
header {* Ordered Groups *} |
|
6 |
||
15131 | 7 |
theory OrderedGroup |
22452
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset
|
8 |
imports Lattices |
19798 | 9 |
uses "~~/src/Provers/Arith/abel_cancel.ML" |
15131 | 10 |
begin |
14738 | 11 |
|
12 |
text {* |
|
13 |
The theory of partially ordered groups is taken from the books: |
|
14 |
\begin{itemize} |
|
15 |
\item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979 |
|
16 |
\item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963 |
|
17 |
\end{itemize} |
|
18 |
Most of the used notions can also be looked up in |
|
19 |
\begin{itemize} |
|
14770 | 20 |
\item \url{http://www.mathworld.com} by Eric Weisstein et. al. |
14738 | 21 |
\item \emph{Algebra I} by van der Waerden, Springer. |
22 |
\end{itemize} |
|
23 |
*} |
|
24 |
||
31902 | 25 |
ML {* |
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset
|
26 |
structure Algebra_Simps = Named_Thms( |
31902 | 27 |
val name = "algebra_simps" |
28 |
val description = "algebra simplification rules" |
|
29 |
) |
|
29667 | 30 |
*} |
31 |
||
31902 | 32 |
setup Algebra_Simps.setup |
29667 | 33 |
|
34 |
text{* The rewrites accumulated in @{text algebra_simps} deal with the |
|
35 |
classical algebraic structures of groups, rings and family. They simplify |
|
36 |
terms by multiplying everything out (in case of a ring) and bringing sums and |
|
37 |
products into a canonical form (by ordered rewriting). As a result it decides |
|
38 |
group and ring equalities but also helps with inequalities. |
|
39 |
||
40 |
Of course it also works for fields, but it knows nothing about multiplicative |
|
41 |
inverses or division. This is catered for by @{text field_simps}. *} |
|
42 |
||
23085 | 43 |
subsection {* Semigroups and Monoids *} |
14738 | 44 |
|
22390 | 45 |
class semigroup_add = plus + |
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset
|
46 |
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
|
47 |
|
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset
|
48 |
sublocale semigroup_add < plus!: semigroup plus proof |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset
|
49 |
qed (fact add_assoc) |
22390 | 50 |
|
51 |
class ab_semigroup_add = semigroup_add + |
|
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset
|
52 |
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
|
53 |
|
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset
|
54 |
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
|
55 |
qed (fact add_commute) |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset
|
56 |
|
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset
|
57 |
context ab_semigroup_add |
25062 | 58 |
begin |
14738 | 59 |
|
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset
|
60 |
lemmas add_left_commute [algebra_simps] = plus.left_commute |
25062 | 61 |
|
62 |
theorems add_ac = add_assoc add_commute add_left_commute |
|
63 |
||
64 |
end |
|
14738 | 65 |
|
66 |
theorems add_ac = add_assoc add_commute add_left_commute |
|
67 |
||
22390 | 68 |
class semigroup_mult = times + |
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset
|
69 |
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
|
70 |
|
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset
|
71 |
sublocale semigroup_mult < times!: semigroup times proof |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset
|
72 |
qed (fact mult_assoc) |
14738 | 73 |
|
22390 | 74 |
class ab_semigroup_mult = semigroup_mult + |
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset
|
75 |
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
|
76 |
|
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset
|
77 |
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
|
78 |
qed (fact mult_commute) |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset
|
79 |
|
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset
|
80 |
context ab_semigroup_mult |
23181 | 81 |
begin |
14738 | 82 |
|
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset
|
83 |
lemmas mult_left_commute [algebra_simps] = times.left_commute |
25062 | 84 |
|
85 |
theorems mult_ac = mult_assoc mult_commute mult_left_commute |
|
23181 | 86 |
|
87 |
end |
|
14738 | 88 |
|
89 |
theorems mult_ac = mult_assoc mult_commute mult_left_commute |
|
90 |
||
26015 | 91 |
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
|
92 |
assumes mult_idem: "x * x = x" |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset
|
93 |
|
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset
|
94 |
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
|
95 |
qed (fact mult_idem) |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset
|
96 |
|
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset
|
97 |
context ab_semigroup_idem_mult |
26015 | 98 |
begin |
99 |
||
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset
|
100 |
lemmas mult_left_idem = times.left_idem |
26015 | 101 |
|
102 |
end |
|
103 |
||
23085 | 104 |
class monoid_add = zero + semigroup_add + |
25062 | 105 |
assumes add_0_left [simp]: "0 + a = a" |
106 |
and add_0_right [simp]: "a + 0 = a" |
|
23085 | 107 |
|
26071 | 108 |
lemma zero_reorient: "0 = x \<longleftrightarrow> x = 0" |
29667 | 109 |
by (rule eq_commute) |
26071 | 110 |
|
22390 | 111 |
class comm_monoid_add = zero + ab_semigroup_add + |
25062 | 112 |
assumes add_0: "0 + a = a" |
113 |
begin |
|
23085 | 114 |
|
25062 | 115 |
subclass monoid_add |
28823 | 116 |
proof qed (insert add_0, simp_all add: add_commute) |
25062 | 117 |
|
118 |
end |
|
14738 | 119 |
|
22390 | 120 |
class monoid_mult = one + semigroup_mult + |
25062 | 121 |
assumes mult_1_left [simp]: "1 * a = a" |
122 |
assumes mult_1_right [simp]: "a * 1 = a" |
|
14738 | 123 |
|
26071 | 124 |
lemma one_reorient: "1 = x \<longleftrightarrow> x = 1" |
29667 | 125 |
by (rule eq_commute) |
26071 | 126 |
|
22390 | 127 |
class comm_monoid_mult = one + ab_semigroup_mult + |
25062 | 128 |
assumes mult_1: "1 * a = a" |
129 |
begin |
|
14738 | 130 |
|
25062 | 131 |
subclass monoid_mult |
28823 | 132 |
proof qed (insert mult_1, simp_all add: mult_commute) |
25062 | 133 |
|
134 |
end |
|
14738 | 135 |
|
22390 | 136 |
class cancel_semigroup_add = semigroup_add + |
25062 | 137 |
assumes add_left_imp_eq: "a + b = a + c \<Longrightarrow> b = c" |
138 |
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
|
139 |
begin |
a89d755b029d
move proofs of add_left_cancel and add_right_cancel into the correct locale
huffman
parents:
27250
diff
changeset
|
140 |
|
a89d755b029d
move proofs of add_left_cancel and add_right_cancel into the correct locale
huffman
parents:
27250
diff
changeset
|
141 |
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
|
142 |
"a + b = a + c \<longleftrightarrow> b = c" |
29667 | 143 |
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
|
144 |
|
a89d755b029d
move proofs of add_left_cancel and add_right_cancel into the correct locale
huffman
parents:
27250
diff
changeset
|
145 |
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
|
146 |
"b + a = c + a \<longleftrightarrow> b = c" |
29667 | 147 |
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
|
148 |
|
a89d755b029d
move proofs of add_left_cancel and add_right_cancel into the correct locale
huffman
parents:
27250
diff
changeset
|
149 |
end |
14738 | 150 |
|
22390 | 151 |
class cancel_ab_semigroup_add = ab_semigroup_add + |
25062 | 152 |
assumes add_imp_eq: "a + b = a + c \<Longrightarrow> b = c" |
25267 | 153 |
begin |
14738 | 154 |
|
25267 | 155 |
subclass cancel_semigroup_add |
28823 | 156 |
proof |
22390 | 157 |
fix a b c :: 'a |
158 |
assume "a + b = a + c" |
|
159 |
then show "b = c" by (rule add_imp_eq) |
|
160 |
next |
|
14738 | 161 |
fix a b c :: 'a |
162 |
assume "b + a = c + a" |
|
22390 | 163 |
then have "a + b = a + c" by (simp only: add_commute) |
164 |
then show "b = c" by (rule add_imp_eq) |
|
14738 | 165 |
qed |
166 |
||
25267 | 167 |
end |
168 |
||
29904 | 169 |
class cancel_comm_monoid_add = cancel_ab_semigroup_add + comm_monoid_add |
170 |
||
171 |
||
23085 | 172 |
subsection {* Groups *} |
173 |
||
25762 | 174 |
class group_add = minus + uminus + monoid_add + |
25062 | 175 |
assumes left_minus [simp]: "- a + a = 0" |
176 |
assumes diff_minus: "a - b = a + (- b)" |
|
177 |
begin |
|
23085 | 178 |
|
34147
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset
|
179 |
lemma minus_unique: |
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset
|
180 |
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
|
181 |
proof - |
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset
|
182 |
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
|
183 |
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
|
184 |
finally show ?thesis . |
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset
|
185 |
qed |
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset
|
186 |
|
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset
|
187 |
lemmas equals_zero_I = minus_unique (* legacy name *) |
14738 | 188 |
|
25062 | 189 |
lemma minus_zero [simp]: "- 0 = 0" |
14738 | 190 |
proof - |
34147
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset
|
191 |
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
|
192 |
thus "- 0 = 0" by (rule minus_unique) |
14738 | 193 |
qed |
194 |
||
25062 | 195 |
lemma minus_minus [simp]: "- (- a) = a" |
23085 | 196 |
proof - |
34147
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset
|
197 |
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
|
198 |
thus "- (- a) = a" by (rule minus_unique) |
23085 | 199 |
qed |
14738 | 200 |
|
25062 | 201 |
lemma right_minus [simp]: "a + - a = 0" |
14738 | 202 |
proof - |
25062 | 203 |
have "a + - a = - (- a) + - a" by simp |
204 |
also have "\<dots> = 0" by (rule left_minus) |
|
14738 | 205 |
finally show ?thesis . |
206 |
qed |
|
207 |
||
34147
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset
|
208 |
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
|
209 |
by (simp add: add_assoc [symmetric]) |
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset
|
210 |
|
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset
|
211 |
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
|
212 |
by (simp add: add_assoc [symmetric]) |
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset
|
213 |
|
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset
|
214 |
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
|
215 |
proof - |
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset
|
216 |
have "(a + b) + (- b + - a) = 0" |
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset
|
217 |
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
|
218 |
thus "- (a + b) = - b + - a" |
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset
|
219 |
by (rule minus_unique) |
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset
|
220 |
qed |
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset
|
221 |
|
25062 | 222 |
lemma right_minus_eq: "a - b = 0 \<longleftrightarrow> a = b" |
14738 | 223 |
proof |
23085 | 224 |
assume "a - b = 0" |
225 |
have "a = (a - b) + b" by (simp add:diff_minus add_assoc) |
|
226 |
also have "\<dots> = b" using `a - b = 0` by simp |
|
227 |
finally show "a = b" . |
|
14738 | 228 |
next |
23085 | 229 |
assume "a = b" thus "a - b = 0" by (simp add: diff_minus) |
14738 | 230 |
qed |
231 |
||
25062 | 232 |
lemma diff_self [simp]: "a - a = 0" |
29667 | 233 |
by (simp add: diff_minus) |
14738 | 234 |
|
25062 | 235 |
lemma diff_0 [simp]: "0 - a = - a" |
29667 | 236 |
by (simp add: diff_minus) |
14738 | 237 |
|
25062 | 238 |
lemma diff_0_right [simp]: "a - 0 = a" |
29667 | 239 |
by (simp add: diff_minus) |
14738 | 240 |
|
25062 | 241 |
lemma diff_minus_eq_add [simp]: "a - - b = a + b" |
29667 | 242 |
by (simp add: diff_minus) |
14738 | 243 |
|
25062 | 244 |
lemma neg_equal_iff_equal [simp]: |
245 |
"- a = - b \<longleftrightarrow> a = b" |
|
14738 | 246 |
proof |
247 |
assume "- a = - b" |
|
29667 | 248 |
hence "- (- a) = - (- b)" by simp |
25062 | 249 |
thus "a = b" by simp |
14738 | 250 |
next |
25062 | 251 |
assume "a = b" |
252 |
thus "- a = - b" by simp |
|
14738 | 253 |
qed |
254 |
||
25062 | 255 |
lemma neg_equal_0_iff_equal [simp]: |
256 |
"- a = 0 \<longleftrightarrow> a = 0" |
|
29667 | 257 |
by (subst neg_equal_iff_equal [symmetric], simp) |
14738 | 258 |
|
25062 | 259 |
lemma neg_0_equal_iff_equal [simp]: |
260 |
"0 = - a \<longleftrightarrow> 0 = a" |
|
29667 | 261 |
by (subst neg_equal_iff_equal [symmetric], simp) |
14738 | 262 |
|
263 |
text{*The next two equations can make the simplifier loop!*} |
|
264 |
||
25062 | 265 |
lemma equation_minus_iff: |
266 |
"a = - b \<longleftrightarrow> b = - a" |
|
14738 | 267 |
proof - |
25062 | 268 |
have "- (- a) = - b \<longleftrightarrow> - a = b" by (rule neg_equal_iff_equal) |
269 |
thus ?thesis by (simp add: eq_commute) |
|
270 |
qed |
|
271 |
||
272 |
lemma minus_equation_iff: |
|
273 |
"- a = b \<longleftrightarrow> - b = a" |
|
274 |
proof - |
|
275 |
have "- a = - (- b) \<longleftrightarrow> a = -b" by (rule neg_equal_iff_equal) |
|
14738 | 276 |
thus ?thesis by (simp add: eq_commute) |
277 |
qed |
|
278 |
||
28130
32b4185bfdc7
move diff_add_cancel, add_diff_cancel from class ab_group_add to group_add
huffman
parents:
27516
diff
changeset
|
279 |
lemma diff_add_cancel: "a - b + b = a" |
29667 | 280 |
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
|
281 |
|
32b4185bfdc7
move diff_add_cancel, add_diff_cancel from class ab_group_add to group_add
huffman
parents:
27516
diff
changeset
|
282 |
lemma add_diff_cancel: "a + b - b = a" |
29667 | 283 |
by (simp add: diff_minus add_assoc) |
284 |
||
285 |
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
|
286 |
|
29914
c9ced4f54e82
generalize lemma eq_neg_iff_add_eq_0, and move to OrderedGroup
huffman
parents:
29904
diff
changeset
|
287 |
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
|
288 |
proof |
c9ced4f54e82
generalize lemma eq_neg_iff_add_eq_0, and move to OrderedGroup
huffman
parents:
29904
diff
changeset
|
289 |
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
|
290 |
next |
c9ced4f54e82
generalize lemma eq_neg_iff_add_eq_0, and move to OrderedGroup
huffman
parents:
29904
diff
changeset
|
291 |
assume "a + b = 0" |
c9ced4f54e82
generalize lemma eq_neg_iff_add_eq_0, and move to OrderedGroup
huffman
parents:
29904
diff
changeset
|
292 |
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
|
293 |
by (simp only: add_assoc) |
c9ced4f54e82
generalize lemma eq_neg_iff_add_eq_0, and move to OrderedGroup
huffman
parents:
29904
diff
changeset
|
294 |
ultimately show "a = - b" by simp |
c9ced4f54e82
generalize lemma eq_neg_iff_add_eq_0, and move to OrderedGroup
huffman
parents:
29904
diff
changeset
|
295 |
qed |
c9ced4f54e82
generalize lemma eq_neg_iff_add_eq_0, and move to OrderedGroup
huffman
parents:
29904
diff
changeset
|
296 |
|
25062 | 297 |
end |
298 |
||
25762 | 299 |
class ab_group_add = minus + uminus + comm_monoid_add + |
25062 | 300 |
assumes ab_left_minus: "- a + a = 0" |
301 |
assumes ab_diff_minus: "a - b = a + (- b)" |
|
25267 | 302 |
begin |
25062 | 303 |
|
25267 | 304 |
subclass group_add |
28823 | 305 |
proof qed (simp_all add: ab_left_minus ab_diff_minus) |
25062 | 306 |
|
29904 | 307 |
subclass cancel_comm_monoid_add |
28823 | 308 |
proof |
25062 | 309 |
fix a b c :: 'a |
310 |
assume "a + b = a + c" |
|
311 |
then have "- a + a + b = - a + a + c" |
|
312 |
unfolding add_assoc by simp |
|
313 |
then show "b = c" by simp |
|
314 |
qed |
|
315 |
||
29667 | 316 |
lemma uminus_add_conv_diff[algebra_simps]: |
25062 | 317 |
"- a + b = b - a" |
29667 | 318 |
by (simp add:diff_minus add_commute) |
25062 | 319 |
|
320 |
lemma minus_add_distrib [simp]: |
|
321 |
"- (a + b) = - a + - b" |
|
34146
14595e0c27e8
rename equals_zero_I to minus_unique (keep old name too)
huffman
parents:
33364
diff
changeset
|
322 |
by (rule minus_unique) (simp add: add_ac) |
25062 | 323 |
|
324 |
lemma minus_diff_eq [simp]: |
|
325 |
"- (a - b) = b - a" |
|
29667 | 326 |
by (simp add: diff_minus add_commute) |
25077 | 327 |
|
29667 | 328 |
lemma add_diff_eq[algebra_simps]: "a + (b - c) = (a + b) - c" |
329 |
by (simp add: diff_minus add_ac) |
|
25077 | 330 |
|
29667 | 331 |
lemma diff_add_eq[algebra_simps]: "(a - b) + c = (a + c) - b" |
332 |
by (simp add: diff_minus add_ac) |
|
25077 | 333 |
|
29667 | 334 |
lemma diff_eq_eq[algebra_simps]: "a - b = c \<longleftrightarrow> a = c + b" |
335 |
by (auto simp add: diff_minus add_assoc) |
|
25077 | 336 |
|
29667 | 337 |
lemma eq_diff_eq[algebra_simps]: "a = c - b \<longleftrightarrow> a + b = c" |
338 |
by (auto simp add: diff_minus add_assoc) |
|
25077 | 339 |
|
29667 | 340 |
lemma diff_diff_eq[algebra_simps]: "(a - b) - c = a - (b + c)" |
341 |
by (simp add: diff_minus add_ac) |
|
25077 | 342 |
|
29667 | 343 |
lemma diff_diff_eq2[algebra_simps]: "a - (b - c) = (a + c) - b" |
344 |
by (simp add: diff_minus add_ac) |
|
25077 | 345 |
|
346 |
lemma eq_iff_diff_eq_0: "a = b \<longleftrightarrow> a - b = 0" |
|
29667 | 347 |
by (simp add: algebra_simps) |
25077 | 348 |
|
30629 | 349 |
lemma diff_eq_0_iff_eq [simp, noatp]: "a - b = 0 \<longleftrightarrow> a = b" |
350 |
by (simp add: algebra_simps) |
|
351 |
||
25062 | 352 |
end |
14738 | 353 |
|
354 |
subsection {* (Partially) Ordered Groups *} |
|
355 |
||
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
356 |
class ordered_ab_semigroup_add = order + ab_semigroup_add + |
25062 | 357 |
assumes add_left_mono: "a \<le> b \<Longrightarrow> c + a \<le> c + b" |
358 |
begin |
|
24380
c215e256beca
moved ordered_ab_semigroup_add to OrderedGroup.thy
haftmann
parents:
24286
diff
changeset
|
359 |
|
25062 | 360 |
lemma add_right_mono: |
361 |
"a \<le> b \<Longrightarrow> a + c \<le> b + c" |
|
29667 | 362 |
by (simp add: add_commute [of _ c] add_left_mono) |
14738 | 363 |
|
364 |
text {* non-strict, in both arguments *} |
|
365 |
lemma add_mono: |
|
25062 | 366 |
"a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c \<le> b + d" |
14738 | 367 |
apply (erule add_right_mono [THEN order_trans]) |
368 |
apply (simp add: add_commute add_left_mono) |
|
369 |
done |
|
370 |
||
25062 | 371 |
end |
372 |
||
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
373 |
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
|
374 |
ordered_ab_semigroup_add + cancel_ab_semigroup_add |
25062 | 375 |
begin |
376 |
||
14738 | 377 |
lemma add_strict_left_mono: |
25062 | 378 |
"a < b \<Longrightarrow> c + a < c + b" |
29667 | 379 |
by (auto simp add: less_le add_left_mono) |
14738 | 380 |
|
381 |
lemma add_strict_right_mono: |
|
25062 | 382 |
"a < b \<Longrightarrow> a + c < b + c" |
29667 | 383 |
by (simp add: add_commute [of _ c] add_strict_left_mono) |
14738 | 384 |
|
385 |
text{*Strict monotonicity in both arguments*} |
|
25062 | 386 |
lemma add_strict_mono: |
387 |
"a < b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d" |
|
388 |
apply (erule add_strict_right_mono [THEN less_trans]) |
|
14738 | 389 |
apply (erule add_strict_left_mono) |
390 |
done |
|
391 |
||
392 |
lemma add_less_le_mono: |
|
25062 | 393 |
"a < b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c < b + d" |
394 |
apply (erule add_strict_right_mono [THEN less_le_trans]) |
|
395 |
apply (erule add_left_mono) |
|
14738 | 396 |
done |
397 |
||
398 |
lemma add_le_less_mono: |
|
25062 | 399 |
"a \<le> b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d" |
400 |
apply (erule add_right_mono [THEN le_less_trans]) |
|
14738 | 401 |
apply (erule add_strict_left_mono) |
402 |
done |
|
403 |
||
25062 | 404 |
end |
405 |
||
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
406 |
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
|
407 |
ordered_cancel_ab_semigroup_add + |
25062 | 408 |
assumes add_le_imp_le_left: "c + a \<le> c + b \<Longrightarrow> a \<le> b" |
409 |
begin |
|
410 |
||
14738 | 411 |
lemma add_less_imp_less_left: |
29667 | 412 |
assumes less: "c + a < c + b" shows "a < b" |
14738 | 413 |
proof - |
414 |
from less have le: "c + a <= c + b" by (simp add: order_le_less) |
|
415 |
have "a <= b" |
|
416 |
apply (insert le) |
|
417 |
apply (drule add_le_imp_le_left) |
|
418 |
by (insert le, drule add_le_imp_le_left, assumption) |
|
419 |
moreover have "a \<noteq> b" |
|
420 |
proof (rule ccontr) |
|
421 |
assume "~(a \<noteq> b)" |
|
422 |
then have "a = b" by simp |
|
423 |
then have "c + a = c + b" by simp |
|
424 |
with less show "False"by simp |
|
425 |
qed |
|
426 |
ultimately show "a < b" by (simp add: order_le_less) |
|
427 |
qed |
|
428 |
||
429 |
lemma add_less_imp_less_right: |
|
25062 | 430 |
"a + c < b + c \<Longrightarrow> a < b" |
14738 | 431 |
apply (rule add_less_imp_less_left [of c]) |
432 |
apply (simp add: add_commute) |
|
433 |
done |
|
434 |
||
435 |
lemma add_less_cancel_left [simp]: |
|
25062 | 436 |
"c + a < c + b \<longleftrightarrow> a < b" |
29667 | 437 |
by (blast intro: add_less_imp_less_left add_strict_left_mono) |
14738 | 438 |
|
439 |
lemma add_less_cancel_right [simp]: |
|
25062 | 440 |
"a + c < b + c \<longleftrightarrow> a < b" |
29667 | 441 |
by (blast intro: add_less_imp_less_right add_strict_right_mono) |
14738 | 442 |
|
443 |
lemma add_le_cancel_left [simp]: |
|
25062 | 444 |
"c + a \<le> c + b \<longleftrightarrow> a \<le> b" |
29667 | 445 |
by (auto, drule add_le_imp_le_left, simp_all add: add_left_mono) |
14738 | 446 |
|
447 |
lemma add_le_cancel_right [simp]: |
|
25062 | 448 |
"a + c \<le> b + c \<longleftrightarrow> a \<le> b" |
29667 | 449 |
by (simp add: add_commute [of a c] add_commute [of b c]) |
14738 | 450 |
|
451 |
lemma add_le_imp_le_right: |
|
25062 | 452 |
"a + c \<le> b + c \<Longrightarrow> a \<le> b" |
29667 | 453 |
by simp |
25062 | 454 |
|
25077 | 455 |
lemma max_add_distrib_left: |
456 |
"max x y + z = max (x + z) (y + z)" |
|
457 |
unfolding max_def by auto |
|
458 |
||
459 |
lemma min_add_distrib_left: |
|
460 |
"min x y + z = min (x + z) (y + z)" |
|
461 |
unfolding min_def by auto |
|
462 |
||
25062 | 463 |
end |
464 |
||
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
465 |
subsection {* Support for reasoning about signs *} |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
466 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
467 |
class ordered_comm_monoid_add = |
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
468 |
ordered_cancel_ab_semigroup_add + comm_monoid_add |
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
469 |
begin |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
470 |
|
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
471 |
lemma add_pos_nonneg: |
29667 | 472 |
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
|
473 |
proof - |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
474 |
have "0 + 0 < a + b" |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
475 |
using assms by (rule add_less_le_mono) |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
476 |
then show ?thesis by simp |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
477 |
qed |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
478 |
|
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
479 |
lemma add_pos_pos: |
29667 | 480 |
assumes "0 < a" and "0 < b" shows "0 < a + b" |
481 |
by (rule add_pos_nonneg) (insert assms, auto) |
|
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
482 |
|
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
483 |
lemma add_nonneg_pos: |
29667 | 484 |
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
|
485 |
proof - |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
486 |
have "0 + 0 < a + b" |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
487 |
using assms by (rule add_le_less_mono) |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
488 |
then show ?thesis by simp |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
489 |
qed |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
490 |
|
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
491 |
lemma add_nonneg_nonneg: |
29667 | 492 |
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
|
493 |
proof - |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
494 |
have "0 + 0 \<le> a + b" |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
495 |
using assms by (rule add_mono) |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
496 |
then show ?thesis by simp |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
497 |
qed |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
498 |
|
30691 | 499 |
lemma add_neg_nonpos: |
29667 | 500 |
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
|
501 |
proof - |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
502 |
have "a + b < 0 + 0" |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
503 |
using assms by (rule add_less_le_mono) |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
504 |
then show ?thesis by simp |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
505 |
qed |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
506 |
|
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
507 |
lemma add_neg_neg: |
29667 | 508 |
assumes "a < 0" and "b < 0" shows "a + b < 0" |
509 |
by (rule add_neg_nonpos) (insert assms, auto) |
|
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
510 |
|
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
511 |
lemma add_nonpos_neg: |
29667 | 512 |
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
|
513 |
proof - |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
514 |
have "a + b < 0 + 0" |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
515 |
using assms by (rule add_le_less_mono) |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
516 |
then show ?thesis by simp |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
517 |
qed |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
518 |
|
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
519 |
lemma add_nonpos_nonpos: |
29667 | 520 |
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
|
521 |
proof - |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
522 |
have "a + b \<le> 0 + 0" |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
523 |
using assms by (rule add_mono) |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
524 |
then show ?thesis by simp |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
525 |
qed |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
526 |
|
30691 | 527 |
lemmas add_sign_intros = |
528 |
add_pos_nonneg add_pos_pos add_nonneg_pos add_nonneg_nonneg |
|
529 |
add_neg_nonpos add_neg_neg add_nonpos_neg add_nonpos_nonpos |
|
530 |
||
29886 | 531 |
lemma add_nonneg_eq_0_iff: |
532 |
assumes x: "0 \<le> x" and y: "0 \<le> y" |
|
533 |
shows "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0" |
|
534 |
proof (intro iffI conjI) |
|
535 |
have "x = x + 0" by simp |
|
536 |
also have "x + 0 \<le> x + y" using y by (rule add_left_mono) |
|
537 |
also assume "x + y = 0" |
|
538 |
also have "0 \<le> x" using x . |
|
539 |
finally show "x = 0" . |
|
540 |
next |
|
541 |
have "y = 0 + y" by simp |
|
542 |
also have "0 + y \<le> x + y" using x by (rule add_right_mono) |
|
543 |
also assume "x + y = 0" |
|
544 |
also have "0 \<le> y" using y . |
|
545 |
finally show "y = 0" . |
|
546 |
next |
|
547 |
assume "x = 0 \<and> y = 0" |
|
548 |
then show "x + y = 0" by simp |
|
549 |
qed |
|
550 |
||
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
551 |
end |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
552 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
553 |
class ordered_ab_group_add = |
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
554 |
ab_group_add + ordered_ab_semigroup_add |
25062 | 555 |
begin |
556 |
||
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
557 |
subclass ordered_cancel_ab_semigroup_add .. |
25062 | 558 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
559 |
subclass ordered_ab_semigroup_add_imp_le |
28823 | 560 |
proof |
25062 | 561 |
fix a b c :: 'a |
562 |
assume "c + a \<le> c + b" |
|
563 |
hence "(-c) + (c + a) \<le> (-c) + (c + b)" by (rule add_left_mono) |
|
564 |
hence "((-c) + c) + a \<le> ((-c) + c) + b" by (simp only: add_assoc) |
|
565 |
thus "a \<le> b" by simp |
|
566 |
qed |
|
567 |
||
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
568 |
subclass ordered_comm_monoid_add .. |
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
569 |
|
25077 | 570 |
lemma max_diff_distrib_left: |
571 |
shows "max x y - z = max (x - z) (y - z)" |
|
29667 | 572 |
by (simp add: diff_minus, rule max_add_distrib_left) |
25077 | 573 |
|
574 |
lemma min_diff_distrib_left: |
|
575 |
shows "min x y - z = min (x - z) (y - z)" |
|
29667 | 576 |
by (simp add: diff_minus, rule min_add_distrib_left) |
25077 | 577 |
|
578 |
lemma le_imp_neg_le: |
|
29667 | 579 |
assumes "a \<le> b" shows "-b \<le> -a" |
25077 | 580 |
proof - |
29667 | 581 |
have "-a+a \<le> -a+b" using `a \<le> b` by (rule add_left_mono) |
582 |
hence "0 \<le> -a+b" by simp |
|
583 |
hence "0 + (-b) \<le> (-a + b) + (-b)" by (rule add_right_mono) |
|
584 |
thus ?thesis by (simp add: add_assoc) |
|
25077 | 585 |
qed |
586 |
||
587 |
lemma neg_le_iff_le [simp]: "- b \<le> - a \<longleftrightarrow> a \<le> b" |
|
588 |
proof |
|
589 |
assume "- b \<le> - a" |
|
29667 | 590 |
hence "- (- a) \<le> - (- b)" by (rule le_imp_neg_le) |
25077 | 591 |
thus "a\<le>b" by simp |
592 |
next |
|
593 |
assume "a\<le>b" |
|
594 |
thus "-b \<le> -a" by (rule le_imp_neg_le) |
|
595 |
qed |
|
596 |
||
597 |
lemma neg_le_0_iff_le [simp]: "- a \<le> 0 \<longleftrightarrow> 0 \<le> a" |
|
29667 | 598 |
by (subst neg_le_iff_le [symmetric], simp) |
25077 | 599 |
|
600 |
lemma neg_0_le_iff_le [simp]: "0 \<le> - a \<longleftrightarrow> a \<le> 0" |
|
29667 | 601 |
by (subst neg_le_iff_le [symmetric], simp) |
25077 | 602 |
|
603 |
lemma neg_less_iff_less [simp]: "- b < - a \<longleftrightarrow> a < b" |
|
29667 | 604 |
by (force simp add: less_le) |
25077 | 605 |
|
606 |
lemma neg_less_0_iff_less [simp]: "- a < 0 \<longleftrightarrow> 0 < a" |
|
29667 | 607 |
by (subst neg_less_iff_less [symmetric], simp) |
25077 | 608 |
|
609 |
lemma neg_0_less_iff_less [simp]: "0 < - a \<longleftrightarrow> a < 0" |
|
29667 | 610 |
by (subst neg_less_iff_less [symmetric], simp) |
25077 | 611 |
|
612 |
text{*The next several equations can make the simplifier loop!*} |
|
613 |
||
614 |
lemma less_minus_iff: "a < - b \<longleftrightarrow> b < - a" |
|
615 |
proof - |
|
616 |
have "(- (-a) < - b) = (b < - a)" by (rule neg_less_iff_less) |
|
617 |
thus ?thesis by simp |
|
618 |
qed |
|
619 |
||
620 |
lemma minus_less_iff: "- a < b \<longleftrightarrow> - b < a" |
|
621 |
proof - |
|
622 |
have "(- a < - (-b)) = (- b < a)" by (rule neg_less_iff_less) |
|
623 |
thus ?thesis by simp |
|
624 |
qed |
|
625 |
||
626 |
lemma le_minus_iff: "a \<le> - b \<longleftrightarrow> b \<le> - a" |
|
627 |
proof - |
|
628 |
have mm: "!! a (b::'a). (-(-a)) < -b \<Longrightarrow> -(-b) < -a" by (simp only: minus_less_iff) |
|
629 |
have "(- (- a) <= -b) = (b <= - a)" |
|
630 |
apply (auto simp only: le_less) |
|
631 |
apply (drule mm) |
|
632 |
apply (simp_all) |
|
633 |
apply (drule mm[simplified], assumption) |
|
634 |
done |
|
635 |
then show ?thesis by simp |
|
636 |
qed |
|
637 |
||
638 |
lemma minus_le_iff: "- a \<le> b \<longleftrightarrow> - b \<le> a" |
|
29667 | 639 |
by (auto simp add: le_less minus_less_iff) |
25077 | 640 |
|
641 |
lemma less_iff_diff_less_0: "a < b \<longleftrightarrow> a - b < 0" |
|
642 |
proof - |
|
643 |
have "(a < b) = (a + (- b) < b + (-b))" |
|
644 |
by (simp only: add_less_cancel_right) |
|
645 |
also have "... = (a - b < 0)" by (simp add: diff_minus) |
|
646 |
finally show ?thesis . |
|
647 |
qed |
|
648 |
||
29667 | 649 |
lemma diff_less_eq[algebra_simps]: "a - b < c \<longleftrightarrow> a < c + b" |
25077 | 650 |
apply (subst less_iff_diff_less_0 [of a]) |
651 |
apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst]) |
|
652 |
apply (simp add: diff_minus add_ac) |
|
653 |
done |
|
654 |
||
29667 | 655 |
lemma less_diff_eq[algebra_simps]: "a < c - b \<longleftrightarrow> a + b < c" |
25077 | 656 |
apply (subst less_iff_diff_less_0 [of "plus a b"]) |
657 |
apply (subst less_iff_diff_less_0 [of a]) |
|
658 |
apply (simp add: diff_minus add_ac) |
|
659 |
done |
|
660 |
||
29667 | 661 |
lemma diff_le_eq[algebra_simps]: "a - b \<le> c \<longleftrightarrow> a \<le> c + b" |
662 |
by (auto simp add: le_less diff_less_eq diff_add_cancel add_diff_cancel) |
|
25077 | 663 |
|
29667 | 664 |
lemma le_diff_eq[algebra_simps]: "a \<le> c - b \<longleftrightarrow> a + b \<le> c" |
665 |
by (auto simp add: le_less less_diff_eq diff_add_cancel add_diff_cancel) |
|
25077 | 666 |
|
667 |
lemma le_iff_diff_le_0: "a \<le> b \<longleftrightarrow> a - b \<le> 0" |
|
29667 | 668 |
by (simp add: algebra_simps) |
25077 | 669 |
|
29667 | 670 |
text{*Legacy - use @{text algebra_simps} *} |
29833 | 671 |
lemmas group_simps[noatp] = algebra_simps |
25230 | 672 |
|
25077 | 673 |
end |
674 |
||
29667 | 675 |
text{*Legacy - use @{text algebra_simps} *} |
29833 | 676 |
lemmas group_simps[noatp] = algebra_simps |
25230 | 677 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
678 |
class linordered_ab_semigroup_add = |
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
679 |
linorder + ordered_ab_semigroup_add |
25062 | 680 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
681 |
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
|
682 |
linorder + ordered_cancel_ab_semigroup_add |
25267 | 683 |
begin |
25062 | 684 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
685 |
subclass linordered_ab_semigroup_add .. |
25062 | 686 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
687 |
subclass ordered_ab_semigroup_add_imp_le |
28823 | 688 |
proof |
25062 | 689 |
fix a b c :: 'a |
690 |
assume le: "c + a <= c + b" |
|
691 |
show "a <= b" |
|
692 |
proof (rule ccontr) |
|
693 |
assume w: "~ a \<le> b" |
|
694 |
hence "b <= a" by (simp add: linorder_not_le) |
|
695 |
hence le2: "c + b <= c + a" by (rule add_left_mono) |
|
696 |
have "a = b" |
|
697 |
apply (insert le) |
|
698 |
apply (insert le2) |
|
699 |
apply (drule antisym, simp_all) |
|
700 |
done |
|
701 |
with w show False |
|
702 |
by (simp add: linorder_not_le [symmetric]) |
|
703 |
qed |
|
704 |
qed |
|
705 |
||
25267 | 706 |
end |
707 |
||
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
708 |
class linordered_ab_group_add = linorder + ordered_ab_group_add |
25267 | 709 |
begin |
25230 | 710 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
711 |
subclass linordered_cancel_ab_semigroup_add .. |
25230 | 712 |
|
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
713 |
lemma neg_less_eq_nonneg: |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
714 |
"- a \<le> a \<longleftrightarrow> 0 \<le> a" |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
715 |
proof |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
716 |
assume A: "- a \<le> a" show "0 \<le> a" |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
717 |
proof (rule classical) |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
718 |
assume "\<not> 0 \<le> a" |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
719 |
then have "a < 0" by auto |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
720 |
with A have "- a < 0" by (rule le_less_trans) |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
721 |
then show ?thesis by auto |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
722 |
qed |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
723 |
next |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
724 |
assume A: "0 \<le> a" show "- a \<le> a" |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
725 |
proof (rule order_trans) |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
726 |
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
|
727 |
next |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
728 |
show "0 \<le> a" using A . |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
729 |
qed |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
730 |
qed |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
731 |
|
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
732 |
lemma less_eq_neg_nonpos: |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
733 |
"a \<le> - a \<longleftrightarrow> a \<le> 0" |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
734 |
proof |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
735 |
assume A: "a \<le> - a" show "a \<le> 0" |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
736 |
proof (rule classical) |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
737 |
assume "\<not> a \<le> 0" |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
738 |
then have "0 < a" by auto |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
739 |
then have "0 < - a" using A by (rule less_le_trans) |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
740 |
then show ?thesis by auto |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
741 |
qed |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
742 |
next |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
743 |
assume A: "a \<le> 0" show "a \<le> - a" |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
744 |
proof (rule order_trans) |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
745 |
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
|
746 |
next |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
747 |
show "a \<le> 0" using A . |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
748 |
qed |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
749 |
qed |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
750 |
|
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
751 |
lemma equal_neg_zero: |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
752 |
"a = - a \<longleftrightarrow> a = 0" |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
753 |
proof |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
754 |
assume "a = 0" then show "a = - a" by simp |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
755 |
next |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
756 |
assume A: "a = - a" show "a = 0" |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
757 |
proof (cases "0 \<le> a") |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
758 |
case True with A have "0 \<le> - a" by auto |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
759 |
with le_minus_iff have "a \<le> 0" by simp |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
760 |
with True show ?thesis by (auto intro: order_trans) |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
761 |
next |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
762 |
case False then have B: "a \<le> 0" by auto |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
763 |
with A have "- a \<le> 0" by auto |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
764 |
with B show ?thesis by (auto intro: order_trans) |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
765 |
qed |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
766 |
qed |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
767 |
|
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
768 |
lemma neg_equal_zero: |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
769 |
"- a = a \<longleftrightarrow> a = 0" |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
770 |
unfolding equal_neg_zero [symmetric] by auto |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
771 |
|
25267 | 772 |
end |
773 |
||
25077 | 774 |
-- {* FIXME localize the following *} |
14738 | 775 |
|
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset
|
776 |
lemma add_increasing: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
777 |
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
|
778 |
shows "[|0\<le>a; b\<le>c|] ==> b \<le> a + c" |
14738 | 779 |
by (insert add_mono [of 0 a b c], simp) |
780 |
||
15539 | 781 |
lemma add_increasing2: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
782 |
fixes c :: "'a::{ordered_ab_semigroup_add_imp_le, comm_monoid_add}" |
15539 | 783 |
shows "[|0\<le>c; b\<le>a|] ==> b \<le> a + c" |
784 |
by (simp add:add_increasing add_commute[of a]) |
|
785 |
||
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset
|
786 |
lemma add_strict_increasing: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
787 |
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
|
788 |
shows "[|0<a; b\<le>c|] ==> b < a + c" |
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset
|
789 |
by (insert add_less_le_mono [of 0 a b c], simp) |
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset
|
790 |
|
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset
|
791 |
lemma add_strict_increasing2: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
792 |
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
|
793 |
shows "[|0\<le>a; b<c|] ==> b < a + c" |
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset
|
794 |
by (insert add_le_less_mono [of 0 a b c], simp) |
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset
|
795 |
|
14738 | 796 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
797 |
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
|
798 |
assumes abs_ge_zero [simp]: "\<bar>a\<bar> \<ge> 0" |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
799 |
and abs_ge_self: "a \<le> \<bar>a\<bar>" |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
800 |
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
|
801 |
and abs_minus_cancel [simp]: "\<bar>-a\<bar> = \<bar>a\<bar>" |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
802 |
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
|
803 |
begin |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
804 |
|
25307 | 805 |
lemma abs_minus_le_zero: "- \<bar>a\<bar> \<le> 0" |
806 |
unfolding neg_le_0_iff_le by simp |
|
807 |
||
808 |
lemma abs_of_nonneg [simp]: |
|
29667 | 809 |
assumes nonneg: "0 \<le> a" shows "\<bar>a\<bar> = a" |
25307 | 810 |
proof (rule antisym) |
811 |
from nonneg le_imp_neg_le have "- a \<le> 0" by simp |
|
812 |
from this nonneg have "- a \<le> a" by (rule order_trans) |
|
813 |
then show "\<bar>a\<bar> \<le> a" by (auto intro: abs_leI) |
|
814 |
qed (rule abs_ge_self) |
|
815 |
||
816 |
lemma abs_idempotent [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>" |
|
29667 | 817 |
by (rule antisym) |
818 |
(auto intro!: abs_ge_self abs_leI order_trans [of "uminus (abs a)" zero "abs a"]) |
|
25307 | 819 |
|
820 |
lemma abs_eq_0 [simp]: "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0" |
|
821 |
proof - |
|
822 |
have "\<bar>a\<bar> = 0 \<Longrightarrow> a = 0" |
|
823 |
proof (rule antisym) |
|
824 |
assume zero: "\<bar>a\<bar> = 0" |
|
825 |
with abs_ge_self show "a \<le> 0" by auto |
|
826 |
from zero have "\<bar>-a\<bar> = 0" by simp |
|
827 |
with abs_ge_self [of "uminus a"] have "- a \<le> 0" by auto |
|
828 |
with neg_le_0_iff_le show "0 \<le> a" by auto |
|
829 |
qed |
|
830 |
then show ?thesis by auto |
|
831 |
qed |
|
832 |
||
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
833 |
lemma abs_zero [simp]: "\<bar>0\<bar> = 0" |
29667 | 834 |
by simp |
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16417
diff
changeset
|
835 |
|
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
836 |
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
|
837 |
proof - |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
838 |
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
|
839 |
thus ?thesis by simp |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
840 |
qed |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
841 |
|
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
842 |
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
|
843 |
proof |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
844 |
assume "\<bar>a\<bar> \<le> 0" |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
845 |
then have "\<bar>a\<bar> = 0" by (rule antisym) simp |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
846 |
thus "a = 0" by simp |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
847 |
next |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
848 |
assume "a = 0" |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
849 |
thus "\<bar>a\<bar> \<le> 0" by simp |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
850 |
qed |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
851 |
|
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
852 |
lemma zero_less_abs_iff [simp]: "0 < \<bar>a\<bar> \<longleftrightarrow> a \<noteq> 0" |
29667 | 853 |
by (simp add: less_le) |
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
854 |
|
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
855 |
lemma abs_not_less_zero [simp]: "\<not> \<bar>a\<bar> < 0" |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
856 |
proof - |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
857 |
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
|
858 |
show ?thesis by (simp add: a) |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
859 |
qed |
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16417
diff
changeset
|
860 |
|
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
861 |
lemma abs_ge_minus_self: "- a \<le> \<bar>a\<bar>" |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
862 |
proof - |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
863 |
have "- a \<le> \<bar>-a\<bar>" by (rule abs_ge_self) |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
864 |
then show ?thesis by simp |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
865 |
qed |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
866 |
|
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
867 |
lemma abs_minus_commute: |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
868 |
"\<bar>a - b\<bar> = \<bar>b - a\<bar>" |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
869 |
proof - |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
870 |
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
|
871 |
also have "... = \<bar>b - a\<bar>" by simp |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
872 |
finally show ?thesis . |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
873 |
qed |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
874 |
|
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
875 |
lemma abs_of_pos: "0 < a \<Longrightarrow> \<bar>a\<bar> = a" |
29667 | 876 |
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
|
877 |
|
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
878 |
lemma abs_of_nonpos [simp]: |
29667 | 879 |
assumes "a \<le> 0" shows "\<bar>a\<bar> = - a" |
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
880 |
proof - |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
881 |
let ?b = "- a" |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
882 |
have "- ?b \<le> 0 \<Longrightarrow> \<bar>- ?b\<bar> = - (- ?b)" |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
883 |
unfolding abs_minus_cancel [of "?b"] |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
884 |
unfolding neg_le_0_iff_le [of "?b"] |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
885 |
unfolding minus_minus by (erule abs_of_nonneg) |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
886 |
then show ?thesis using assms by auto |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
887 |
qed |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
888 |
|
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
889 |
lemma abs_of_neg: "a < 0 \<Longrightarrow> \<bar>a\<bar> = - a" |
29667 | 890 |
by (rule abs_of_nonpos, rule less_imp_le) |
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
891 |
|
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
892 |
lemma abs_le_D1: "\<bar>a\<bar> \<le> b \<Longrightarrow> a \<le> b" |
29667 | 893 |
by (insert abs_ge_self, blast intro: order_trans) |
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
894 |
|
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
895 |
lemma abs_le_D2: "\<bar>a\<bar> \<le> b \<Longrightarrow> - a \<le> b" |
29667 | 896 |
by (insert abs_le_D1 [of "uminus a"], simp) |
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
897 |
|
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
898 |
lemma abs_le_iff: "\<bar>a\<bar> \<le> b \<longleftrightarrow> a \<le> b \<and> - a \<le> b" |
29667 | 899 |
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
|
900 |
|
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
901 |
lemma abs_triangle_ineq2: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>a - b\<bar>" |
29667 | 902 |
apply (simp add: algebra_simps) |
903 |
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
|
904 |
apply (erule ssubst) |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
905 |
apply (rule abs_triangle_ineq) |
29667 | 906 |
apply (rule arg_cong[of _ _ abs]) |
907 |
apply (simp add: algebra_simps) |
|
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16417
diff
changeset
|
908 |
done |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16417
diff
changeset
|
909 |
|
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
910 |
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
|
911 |
apply (subst abs_le_iff) |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
912 |
apply auto |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
913 |
apply (rule abs_triangle_ineq2) |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
914 |
apply (subst abs_minus_commute) |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
915 |
apply (rule abs_triangle_ineq2) |
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16417
diff
changeset
|
916 |
done |
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16417
diff
changeset
|
917 |
|
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
918 |
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
|
919 |
proof - |
29667 | 920 |
have "abs(a - b) = abs(a + - b)" by (subst diff_minus, rule refl) |
921 |
also have "... <= abs a + abs (- b)" by (rule abs_triangle_ineq) |
|
922 |
finally show ?thesis by simp |
|
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
923 |
qed |
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16417
diff
changeset
|
924 |
|
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
925 |
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
|
926 |
proof - |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
927 |
have "\<bar>a + b - (c+d)\<bar> = \<bar>(a-c) + (b-d)\<bar>" by (simp add: diff_minus add_ac) |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
928 |
also have "... \<le> \<bar>a-c\<bar> + \<bar>b-d\<bar>" by (rule abs_triangle_ineq) |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
929 |
finally show ?thesis . |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
930 |
qed |
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16417
diff
changeset
|
931 |
|
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
932 |
lemma abs_add_abs [simp]: |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
933 |
"\<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
|
934 |
proof (rule antisym) |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
935 |
show "?L \<ge> ?R" by(rule abs_ge_self) |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
936 |
next |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
937 |
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
|
938 |
also have "\<dots> = ?R" by simp |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
939 |
finally show "?L \<le> ?R" . |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
940 |
qed |
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
941 |
|
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset
|
942 |
end |
14738 | 943 |
|
22452
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset
|
944 |
|
14738 | 945 |
subsection {* Lattice Ordered (Abelian) Groups *} |
946 |
||
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
947 |
class semilattice_inf_ab_group_add = ordered_ab_group_add + semilattice_inf |
25090 | 948 |
begin |
14738 | 949 |
|
25090 | 950 |
lemma add_inf_distrib_left: |
951 |
"a + inf b c = inf (a + b) (a + c)" |
|
952 |
apply (rule antisym) |
|
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22390
diff
changeset
|
953 |
apply (simp_all add: le_infI) |
25090 | 954 |
apply (rule add_le_imp_le_left [of "uminus a"]) |
955 |
apply (simp only: add_assoc [symmetric], simp) |
|
21312 | 956 |
apply rule |
957 |
apply (rule add_le_imp_le_left[of "a"], simp only: add_assoc[symmetric], simp)+ |
|
14738 | 958 |
done |
959 |
||
25090 | 960 |
lemma add_inf_distrib_right: |
961 |
"inf a b + c = inf (a + c) (b + c)" |
|
962 |
proof - |
|
963 |
have "c + inf a b = inf (c+a) (c+b)" by (simp add: add_inf_distrib_left) |
|
964 |
thus ?thesis by (simp add: add_commute) |
|
965 |
qed |
|
966 |
||
967 |
end |
|
968 |
||
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
969 |
class semilattice_sup_ab_group_add = ordered_ab_group_add + semilattice_sup |
25090 | 970 |
begin |
971 |
||
972 |
lemma add_sup_distrib_left: |
|
973 |
"a + sup b c = sup (a + b) (a + c)" |
|
974 |
apply (rule antisym) |
|
975 |
apply (rule add_le_imp_le_left [of "uminus a"]) |
|
14738 | 976 |
apply (simp only: add_assoc[symmetric], simp) |
21312 | 977 |
apply rule |
978 |
apply (rule add_le_imp_le_left [of "a"], simp only: add_assoc[symmetric], simp)+ |
|
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22390
diff
changeset
|
979 |
apply (rule le_supI) |
21312 | 980 |
apply (simp_all) |
14738 | 981 |
done |
982 |
||
25090 | 983 |
lemma add_sup_distrib_right: |
984 |
"sup a b + c = sup (a+c) (b+c)" |
|
14738 | 985 |
proof - |
22452
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset
|
986 |
have "c + sup a b = sup (c+a) (c+b)" by (simp add: add_sup_distrib_left) |
14738 | 987 |
thus ?thesis by (simp add: add_commute) |
988 |
qed |
|
989 |
||
25090 | 990 |
end |
991 |
||
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
992 |
class lattice_ab_group_add = ordered_ab_group_add + lattice |
25090 | 993 |
begin |
994 |
||
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
995 |
subclass semilattice_inf_ab_group_add .. |
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
996 |
subclass semilattice_sup_ab_group_add .. |
25090 | 997 |
|
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22390
diff
changeset
|
998 |
lemmas add_sup_inf_distribs = add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left |
14738 | 999 |
|
25090 | 1000 |
lemma inf_eq_neg_sup: "inf a b = - sup (-a) (-b)" |
22452
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset
|
1001 |
proof (rule inf_unique) |
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset
|
1002 |
fix a b :: 'a |
25090 | 1003 |
show "- sup (-a) (-b) \<le> a" |
1004 |
by (rule add_le_imp_le_right [of _ "sup (uminus a) (uminus b)"]) |
|
1005 |
(simp, simp add: add_sup_distrib_left) |
|
22452
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset
|
1006 |
next |
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset
|
1007 |
fix a b :: 'a |
25090 | 1008 |
show "- sup (-a) (-b) \<le> b" |
1009 |
by (rule add_le_imp_le_right [of _ "sup (uminus a) (uminus b)"]) |
|
1010 |
(simp, simp add: add_sup_distrib_left) |
|
22452
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset
|
1011 |
next |
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset
|
1012 |
fix a b c :: 'a |
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset
|
1013 |
assume "a \<le> b" "a \<le> c" |
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset
|
1014 |
then show "a \<le> - sup (-b) (-c)" by (subst neg_le_iff_le [symmetric]) |
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset
|
1015 |
(simp add: le_supI) |
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset
|
1016 |
qed |
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset
|
1017 |
|
25090 | 1018 |
lemma sup_eq_neg_inf: "sup a b = - inf (-a) (-b)" |
22452
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset
|
1019 |
proof (rule sup_unique) |
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset
|
1020 |
fix a b :: 'a |
25090 | 1021 |
show "a \<le> - inf (-a) (-b)" |
1022 |
by (rule add_le_imp_le_right [of _ "inf (uminus a) (uminus b)"]) |
|
1023 |
(simp, simp add: add_inf_distrib_left) |
|
22452
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset
|
1024 |
next |
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset
|
1025 |
fix a b :: 'a |
25090 | 1026 |
show "b \<le> - inf (-a) (-b)" |
1027 |
by (rule add_le_imp_le_right [of _ "inf (uminus a) (uminus b)"]) |
|
1028 |
(simp, simp add: add_inf_distrib_left) |
|
22452
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset
|
1029 |
next |
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset
|
1030 |
fix a b c :: 'a |
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset
|
1031 |
assume "a \<le> c" "b \<le> c" |
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset
|
1032 |
then show "- inf (-a) (-b) \<le> c" by (subst neg_le_iff_le [symmetric]) |
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset
|
1033 |
(simp add: le_infI) |
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset
|
1034 |
qed |
14738 | 1035 |
|
25230 | 1036 |
lemma neg_inf_eq_sup: "- inf a b = sup (-a) (-b)" |
29667 | 1037 |
by (simp add: inf_eq_neg_sup) |
25230 | 1038 |
|
1039 |
lemma neg_sup_eq_inf: "- sup a b = inf (-a) (-b)" |
|
29667 | 1040 |
by (simp add: sup_eq_neg_inf) |
25230 | 1041 |
|
25090 | 1042 |
lemma add_eq_inf_sup: "a + b = sup a b + inf a b" |
14738 | 1043 |
proof - |
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22390
diff
changeset
|
1044 |
have "0 = - inf 0 (a-b) + inf (a-b) 0" by (simp add: inf_commute) |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22390
diff
changeset
|
1045 |
hence "0 = sup 0 (b-a) + inf (a-b) 0" by (simp add: inf_eq_neg_sup) |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22390
diff
changeset
|
1046 |
hence "0 = (-a + sup a b) + (inf a b + (-b))" |
29667 | 1047 |
by (simp add: add_sup_distrib_left add_inf_distrib_right) |
1048 |
(simp add: algebra_simps) |
|
1049 |
thus ?thesis by (simp add: algebra_simps) |
|
14738 | 1050 |
qed |
1051 |
||
1052 |
subsection {* Positive Part, Negative Part, Absolute Value *} |
|
1053 |
||
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22390
diff
changeset
|
1054 |
definition |
25090 | 1055 |
nprt :: "'a \<Rightarrow> 'a" where |
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22390
diff
changeset
|
1056 |
"nprt x = inf x 0" |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22390
diff
changeset
|
1057 |
|
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22390
diff
changeset
|
1058 |
definition |
25090 | 1059 |
pprt :: "'a \<Rightarrow> 'a" where |
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22390
diff
changeset
|
1060 |
"pprt x = sup x 0" |
14738 | 1061 |
|
25230 | 1062 |
lemma pprt_neg: "pprt (- x) = - nprt x" |
1063 |
proof - |
|
1064 |
have "sup (- x) 0 = sup (- x) (- 0)" unfolding minus_zero .. |
|
1065 |
also have "\<dots> = - inf x 0" unfolding neg_inf_eq_sup .. |
|
1066 |
finally have "sup (- x) 0 = - inf x 0" . |
|
1067 |
then show ?thesis unfolding pprt_def nprt_def . |
|
1068 |
qed |
|
1069 |
||
1070 |
lemma nprt_neg: "nprt (- x) = - pprt x" |
|
1071 |
proof - |
|
1072 |
from pprt_neg have "pprt (- (- x)) = - nprt (- x)" . |
|
1073 |
then have "pprt x = - nprt (- x)" by simp |
|
1074 |
then show ?thesis by simp |
|
1075 |
qed |
|
1076 |
||
14738 | 1077 |
lemma prts: "a = pprt a + nprt a" |
29667 | 1078 |
by (simp add: pprt_def nprt_def add_eq_inf_sup[symmetric]) |
14738 | 1079 |
|
1080 |
lemma zero_le_pprt[simp]: "0 \<le> pprt a" |
|
29667 | 1081 |
by (simp add: pprt_def) |
14738 | 1082 |
|
1083 |
lemma nprt_le_zero[simp]: "nprt a \<le> 0" |
|
29667 | 1084 |
by (simp add: nprt_def) |
14738 | 1085 |
|
25090 | 1086 |
lemma le_eq_neg: "a \<le> - b \<longleftrightarrow> a + b \<le> 0" (is "?l = ?r") |
14738 | 1087 |
proof - |
1088 |
have a: "?l \<longrightarrow> ?r" |
|
1089 |
apply (auto) |
|
25090 | 1090 |
apply (rule add_le_imp_le_right[of _ "uminus b" _]) |
14738 | 1091 |
apply (simp add: add_assoc) |
1092 |
done |
|
1093 |
have b: "?r \<longrightarrow> ?l" |
|
1094 |
apply (auto) |
|
1095 |
apply (rule add_le_imp_le_right[of _ "b" _]) |
|
1096 |
apply (simp) |
|
1097 |
done |
|
1098 |
from a b show ?thesis by blast |
|
1099 |
qed |
|
1100 |
||
15580 | 1101 |
lemma pprt_0[simp]: "pprt 0 = 0" by (simp add: pprt_def) |
1102 |
lemma nprt_0[simp]: "nprt 0 = 0" by (simp add: nprt_def) |
|
1103 |
||
25090 | 1104 |
lemma pprt_eq_id [simp, noatp]: "0 \<le> x \<Longrightarrow> pprt x = x" |
32642
026e7c6a6d08
be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
haftmann
parents:
32437
diff
changeset
|
1105 |
by (simp add: pprt_def sup_aci sup_absorb1) |
15580 | 1106 |
|
25090 | 1107 |
lemma nprt_eq_id [simp, noatp]: "x \<le> 0 \<Longrightarrow> nprt x = x" |
32642
026e7c6a6d08
be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
haftmann
parents:
32437
diff
changeset
|
1108 |
by (simp add: nprt_def inf_aci inf_absorb1) |
15580 | 1109 |
|
25090 | 1110 |
lemma pprt_eq_0 [simp, noatp]: "x \<le> 0 \<Longrightarrow> pprt x = 0" |
32642
026e7c6a6d08
be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
haftmann
parents:
32437
diff
changeset
|
1111 |
by (simp add: pprt_def sup_aci sup_absorb2) |
15580 | 1112 |
|
25090 | 1113 |
lemma nprt_eq_0 [simp, noatp]: "0 \<le> x \<Longrightarrow> nprt x = 0" |
32642
026e7c6a6d08
be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
haftmann
parents:
32437
diff
changeset
|
1114 |
by (simp add: nprt_def inf_aci inf_absorb2) |
15580 | 1115 |
|
25090 | 1116 |
lemma sup_0_imp_0: "sup a (- a) = 0 \<Longrightarrow> a = 0" |
14738 | 1117 |
proof - |
1118 |
{ |
|
1119 |
fix a::'a |
|
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22390
diff
changeset
|
1120 |
assume hyp: "sup a (-a) = 0" |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22390
diff
changeset
|
1121 |
hence "sup a (-a) + a = a" by (simp) |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22390
diff
changeset
|
1122 |
hence "sup (a+a) 0 = a" by (simp add: add_sup_distrib_right) |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22390
diff
changeset
|
1123 |
hence "sup (a+a) 0 <= a" by (simp) |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22390
diff
changeset
|
1124 |
hence "0 <= a" by (blast intro: order_trans inf_sup_ord) |
14738 | 1125 |
} |
1126 |
note p = this |
|
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22390
diff
changeset
|
1127 |
assume hyp:"sup a (-a) = 0" |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22390
diff
changeset
|
1128 |
hence hyp2:"sup (-a) (-(-a)) = 0" by (simp add: sup_commute) |
14738 | 1129 |
from p[OF hyp] p[OF hyp2] show "a = 0" by simp |
1130 |
qed |
|
1131 |
||
25090 | 1132 |
lemma inf_0_imp_0: "inf a (-a) = 0 \<Longrightarrow> a = 0" |
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22390
diff
changeset
|
1133 |
apply (simp add: inf_eq_neg_sup) |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22390
diff
changeset
|
1134 |
apply (simp add: sup_commute) |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22390
diff
changeset
|
1135 |
apply (erule sup_0_imp_0) |
15481 | 1136 |
done |
14738 | 1137 |
|
25090 | 1138 |
lemma inf_0_eq_0 [simp, noatp]: "inf a (- a) = 0 \<longleftrightarrow> a = 0" |
29667 | 1139 |
by (rule, erule inf_0_imp_0) simp |
14738 | 1140 |
|
25090 | 1141 |
lemma sup_0_eq_0 [simp, noatp]: "sup a (- a) = 0 \<longleftrightarrow> a = 0" |
29667 | 1142 |
by (rule, erule sup_0_imp_0) simp |
14738 | 1143 |
|
25090 | 1144 |
lemma zero_le_double_add_iff_zero_le_single_add [simp]: |
1145 |
"0 \<le> a + a \<longleftrightarrow> 0 \<le> a" |
|
14738 | 1146 |
proof |
1147 |
assume "0 <= a + a" |
|
32642
026e7c6a6d08
be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
haftmann
parents:
32437
diff
changeset
|
1148 |
hence a:"inf (a+a) 0 = 0" by (simp add: inf_commute inf_absorb1) |
25090 | 1149 |
have "(inf a 0)+(inf a 0) = inf (inf (a+a) 0) a" (is "?l=_") |
32064 | 1150 |
by (simp add: add_sup_inf_distribs inf_aci) |
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22390
diff
changeset
|
1151 |
hence "?l = 0 + inf a 0" by (simp add: a, simp add: inf_commute) |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22390
diff
changeset
|
1152 |
hence "inf a 0 = 0" by (simp only: add_right_cancel) |
32436
10cd49e0c067
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
nipkow
parents:
32075
diff
changeset
|
1153 |
then show "0 <= a" unfolding le_iff_inf by (simp add: inf_commute) |
10cd49e0c067
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
nipkow
parents:
32075
diff
changeset
|
1154 |
next |
14738 | 1155 |
assume a: "0 <= a" |
1156 |
show "0 <= a + a" by (simp add: add_mono[OF a a, simplified]) |
|
1157 |
qed |
|
1158 |
||
25090 | 1159 |
lemma double_zero: "a + a = 0 \<longleftrightarrow> a = 0" |
1160 |
proof |
|
1161 |
assume assm: "a + a = 0" |
|
1162 |
then have "a + a + - a = - a" by simp |
|
1163 |
then have "a + (a + - a) = - a" by (simp only: add_assoc) |
|
32642
026e7c6a6d08
be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
haftmann
parents:
32437
diff
changeset
|
1164 |
then have a: "- a = a" by simp |
25102
db3e412c4cb1
antisymmetry not a default intro rule any longer
haftmann
parents:
25090
diff
changeset
|
1165 |
show "a = 0" apply (rule antisym) |
25090 | 1166 |
apply (unfold neg_le_iff_le [symmetric, of a]) |
1167 |
unfolding a apply simp |
|
1168 |
unfolding zero_le_double_add_iff_zero_le_single_add [symmetric, of a] |
|
1169 |
unfolding assm unfolding le_less apply simp_all done |
|
1170 |
next |
|
1171 |
assume "a = 0" then show "a + a = 0" by simp |
|
1172 |
qed |
|
1173 |
||
1174 |
lemma zero_less_double_add_iff_zero_less_single_add: |
|
1175 |
"0 < a + a \<longleftrightarrow> 0 < a" |
|
1176 |
proof (cases "a = 0") |
|
1177 |
case True then show ?thesis by auto |
|
1178 |
next |
|
1179 |
case False then show ?thesis (*FIXME tune proof*) |
|
1180 |
unfolding less_le apply simp apply rule |
|
1181 |
apply clarify |
|
1182 |
apply rule |
|
1183 |
apply assumption |
|
1184 |
apply (rule notI) |
|
1185 |
unfolding double_zero [symmetric, of a] apply simp |
|
1186 |
done |
|
1187 |
qed |
|
1188 |
||
1189 |
lemma double_add_le_zero_iff_single_add_le_zero [simp]: |
|
1190 |
"a + a \<le> 0 \<longleftrightarrow> a \<le> 0" |
|
14738 | 1191 |
proof - |
25090 | 1192 |
have "a + a \<le> 0 \<longleftrightarrow> 0 \<le> - (a + a)" by (subst le_minus_iff, simp) |
1193 |
moreover have "\<dots> \<longleftrightarrow> a \<le> 0" by (simp add: zero_le_double_add_iff_zero_le_single_add) |
|
14738 | 1194 |
ultimately show ?thesis by blast |
1195 |
qed |
|
1196 |
||
25090 | 1197 |
lemma double_add_less_zero_iff_single_less_zero [simp]: |
1198 |
"a + a < 0 \<longleftrightarrow> a < 0" |
|
1199 |
proof - |
|
1200 |
have "a + a < 0 \<longleftrightarrow> 0 < - (a + a)" by (subst less_minus_iff, simp) |
|
1201 |
moreover have "\<dots> \<longleftrightarrow> a < 0" by (simp add: zero_less_double_add_iff_zero_less_single_add) |
|
1202 |
ultimately show ?thesis by blast |
|
14738 | 1203 |
qed |
1204 |
||
25230 | 1205 |
declare neg_inf_eq_sup [simp] neg_sup_eq_inf [simp] |
1206 |
||
1207 |
lemma le_minus_self_iff: "a \<le> - a \<longleftrightarrow> a \<le> 0" |
|
1208 |
proof - |
|
1209 |
from add_le_cancel_left [of "uminus a" "plus a a" zero] |
|
1210 |
have "(a <= -a) = (a+a <= 0)" |
|
1211 |
by (simp add: add_assoc[symmetric]) |
|
1212 |
thus ?thesis by simp |
|
1213 |
qed |
|
1214 |
||
1215 |
lemma minus_le_self_iff: "- a \<le> a \<longleftrightarrow> 0 \<le> a" |
|
1216 |
proof - |
|
1217 |
from add_le_cancel_left [of "uminus a" zero "plus a a"] |
|
1218 |
have "(-a <= a) = (0 <= a+a)" |
|
1219 |
by (simp add: add_assoc[symmetric]) |
|
1220 |
thus ?thesis by simp |
|
1221 |
qed |
|
1222 |
||
1223 |
lemma zero_le_iff_zero_nprt: "0 \<le> a \<longleftrightarrow> nprt a = 0" |
|
32436
10cd49e0c067
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
nipkow
parents:
32075
diff
changeset
|
1224 |
unfolding le_iff_inf by (simp add: nprt_def inf_commute) |
25230 | 1225 |
|
1226 |
lemma le_zero_iff_zero_pprt: "a \<le> 0 \<longleftrightarrow> pprt a = 0" |
|
32436
10cd49e0c067
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
nipkow
parents:
32075
diff
changeset
|
1227 |
unfolding le_iff_sup by (simp add: pprt_def sup_commute) |
25230 | 1228 |
|
1229 |
lemma le_zero_iff_pprt_id: "0 \<le> a \<longleftrightarrow> pprt a = a" |
|
32436
10cd49e0c067
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
nipkow
parents:
32075
diff
changeset
|
1230 |
unfolding le_iff_sup by (simp add: pprt_def sup_commute) |
25230 | 1231 |
|
1232 |
lemma zero_le_iff_nprt_id: "a \<le> 0 \<longleftrightarrow> nprt a = a" |
|
32436
10cd49e0c067
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
nipkow
parents:
32075
diff
changeset
|
1233 |
unfolding le_iff_inf by (simp add: nprt_def inf_commute) |
25230 | 1234 |
|
1235 |
lemma pprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> pprt a \<le> pprt b" |
|
32436
10cd49e0c067
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
nipkow
parents:
32075
diff
changeset
|
1236 |
unfolding le_iff_sup by (simp add: pprt_def sup_aci sup_assoc [symmetric, of a]) |
25230 | 1237 |
|
1238 |
lemma nprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> nprt a \<le> nprt b" |
|
32436
10cd49e0c067
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
nipkow
parents:
32075
diff
changeset
|
1239 |
unfolding le_iff_inf by (simp add: nprt_def inf_aci inf_assoc [symmetric, of a]) |
25230 | 1240 |
|
25090 | 1241 |
end |
1242 |
||
1243 |
lemmas add_sup_inf_distribs = add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left |
|
1244 |
||
25230 | 1245 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
1246 |
class lattice_ab_group_add_abs = lattice_ab_group_add + abs + |
25230 | 1247 |
assumes abs_lattice: "\<bar>a\<bar> = sup a (- a)" |
1248 |
begin |
|
1249 |
||
1250 |
lemma abs_prts: "\<bar>a\<bar> = pprt a - nprt a" |
|
1251 |
proof - |
|
1252 |
have "0 \<le> \<bar>a\<bar>" |
|
1253 |
proof - |
|
1254 |
have a: "a \<le> \<bar>a\<bar>" and b: "- a \<le> \<bar>a\<bar>" by (auto simp add: abs_lattice) |
|
1255 |
show ?thesis by (rule add_mono [OF a b, simplified]) |
|
1256 |
qed |
|
1257 |
then have "0 \<le> sup a (- a)" unfolding abs_lattice . |
|
1258 |
then have "sup (sup a (- a)) 0 = sup a (- a)" by (rule sup_absorb1) |
|
1259 |
then show ?thesis |
|
32064 | 1260 |
by (simp add: add_sup_inf_distribs sup_aci |
25230 | 1261 |
pprt_def nprt_def diff_minus abs_lattice) |
1262 |
qed |
|
1263 |
||
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
1264 |
subclass ordered_ab_group_add_abs |
29557 | 1265 |
proof |
25230 | 1266 |
have abs_ge_zero [simp]: "\<And>a. 0 \<le> \<bar>a\<bar>" |
1267 |
proof - |
|
1268 |
fix a b |
|
1269 |
have a: "a \<le> \<bar>a\<bar>" and b: "- a \<le> \<bar>a\<bar>" by (auto simp add: abs_lattice) |
|
1270 |
show "0 \<le> \<bar>a\<bar>" by (rule add_mono [OF a b, simplified]) |
|
1271 |
qed |
|
1272 |
have abs_leI: "\<And>a b. a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b" |
|
1273 |
by (simp add: abs_lattice le_supI) |
|
29557 | 1274 |
fix a b |
1275 |
show "0 \<le> \<bar>a\<bar>" by simp |
|
1276 |
show "a \<le> \<bar>a\<bar>" |
|
1277 |
by (auto simp add: abs_lattice) |
|
1278 |
show "\<bar>-a\<bar> = \<bar>a\<bar>" |
|
1279 |
by (simp add: abs_lattice sup_commute) |
|
1280 |
show "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b" by (fact abs_leI) |
|
1281 |
show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>" |
|
1282 |
proof - |
|
1283 |
have g:"abs a + abs b = sup (a+b) (sup (-a-b) (sup (-a+b) (a + (-b))))" (is "_=sup ?m ?n") |
|
32064 | 1284 |
by (simp add: abs_lattice add_sup_inf_distribs sup_aci diff_minus) |
29557 | 1285 |
have a:"a+b <= sup ?m ?n" by (simp) |
1286 |
have b:"-a-b <= ?n" by (simp) |
|
1287 |
have c:"?n <= sup ?m ?n" by (simp) |
|
1288 |
from b c have d: "-a-b <= sup ?m ?n" by(rule order_trans) |
|
1289 |
have e:"-a-b = -(a+b)" by (simp add: diff_minus) |
|
1290 |
from a d e have "abs(a+b) <= sup ?m ?n" |
|
1291 |
by (drule_tac abs_leI, auto) |
|
1292 |
with g[symmetric] show ?thesis by simp |
|
1293 |
qed |
|
25230 | 1294 |
qed |
1295 |
||
1296 |
end |
|
1297 |
||
25090 | 1298 |
lemma sup_eq_if: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
1299 |
fixes a :: "'a\<Colon>{lattice_ab_group_add, linorder}" |
25090 | 1300 |
shows "sup a (- a) = (if a < 0 then - a else a)" |
1301 |
proof - |
|
1302 |
note add_le_cancel_right [of a a "- a", symmetric, simplified] |
|
1303 |
moreover note add_le_cancel_right [of "-a" a a, symmetric, simplified] |
|
32642
026e7c6a6d08
be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
haftmann
parents:
32437
diff
changeset
|
1304 |
then show ?thesis by (auto simp: sup_max min_max.sup_absorb1 min_max.sup_absorb2) |
25090 | 1305 |
qed |
1306 |
||
1307 |
lemma abs_if_lattice: |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
1308 |
fixes a :: "'a\<Colon>{lattice_ab_group_add_abs, linorder}" |
25090 | 1309 |
shows "\<bar>a\<bar> = (if a < 0 then - a else a)" |
29667 | 1310 |
by auto |
25090 | 1311 |
|
1312 |
||
14754
a080eeeaec14
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
obua
parents:
14738
diff
changeset
|
1313 |
text {* Needed for abelian cancellation simprocs: *} |
a080eeeaec14
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
obua
parents:
14738
diff
changeset
|
1314 |
|
a080eeeaec14
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
obua
parents:
14738
diff
changeset
|
1315 |
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
|
1316 |
apply (subst add_left_commute) |
a080eeeaec14
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
obua
parents:
14738
diff
changeset
|
1317 |
apply (subst add_left_cancel) |
a080eeeaec14
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
obua
parents:
14738
diff
changeset
|
1318 |
apply simp |
a080eeeaec14
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
obua
parents:
14738
diff
changeset
|
1319 |
done |
a080eeeaec14
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
obua
parents:
14738
diff
changeset
|
1320 |
|
a080eeeaec14
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
obua
parents:
14738
diff
changeset
|
1321 |
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
|
1322 |
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
|
1323 |
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
|
1324 |
done |
a080eeeaec14
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
obua
parents:
14738
diff
changeset
|
1325 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
1326 |
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
|
1327 |
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
|
1328 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
1329 |
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
|
1330 |
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
|
1331 |
apply (simp add: neg_le_iff_le[symmetric, of "y-x" 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
|
1332 |
done |
a080eeeaec14
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
obua
parents:
14738
diff
changeset
|
1333 |
|
a080eeeaec14
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
obua
parents:
14738
diff
changeset
|
1334 |
lemma eq_eqI: "(x::'a::ab_group_add) - y = x' - y' \<Longrightarrow> (x = y) = (x' = y')" |
30629 | 1335 |
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
|
1336 |
|
a080eeeaec14
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
obua
parents:
14738
diff
changeset
|
1337 |
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
|
1338 |
by (simp add: diff_minus) |
a080eeeaec14
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
obua
parents:
14738
diff
changeset
|
1339 |
|
25090 | 1340 |
lemma le_add_right_mono: |
15178 | 1341 |
assumes |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
1342 |
"a <= b + (c::'a::ordered_ab_group_add)" |
15178 | 1343 |
"c <= d" |
1344 |
shows "a <= b + d" |
|
1345 |
apply (rule_tac order_trans[where y = "b+c"]) |
|
1346 |
apply (simp_all add: prems) |
|
1347 |
done |
|
1348 |
||
1349 |
lemma estimate_by_abs: |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
1350 |
"a + b <= (c::'a::lattice_ab_group_add_abs) \<Longrightarrow> a <= c + abs b" |
15178 | 1351 |
proof - |
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23389
diff
changeset
|
1352 |
assume "a+b <= c" |
29667 | 1353 |
hence 2: "a <= c+(-b)" by (simp add: algebra_simps) |
15178 | 1354 |
have 3: "(-b) <= abs b" by (rule abs_ge_minus_self) |
1355 |
show ?thesis by (rule le_add_right_mono[OF 2 3]) |
|
1356 |
qed |
|
1357 |
||
25090 | 1358 |
subsection {* Tools setup *} |
1359 |
||
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
1360 |
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
|
1361 |
fixes i j k :: "'a\<Colon>ordered_ab_semigroup_add" |
25077 | 1362 |
shows "i \<le> j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l" |
1363 |
and "i = j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l" |
|
1364 |
and "i \<le> j \<and> k = l \<Longrightarrow> i + k \<le> j + l" |
|
1365 |
and "i = j \<and> k = l \<Longrightarrow> i + k = j + l" |
|
1366 |
by (rule add_mono, clarify+)+ |
|
1367 |
||
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34973
diff
changeset
|
1368 |
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
|
1369 |
fixes i j k :: "'a\<Colon>ordered_cancel_ab_semigroup_add" |
25077 | 1370 |
shows "i < j \<and> k = l \<Longrightarrow> i + k < j + l" |
1371 |
and "i = j \<and> k < l \<Longrightarrow> i + k < j + l" |
|
1372 |
and "i < j \<and> k \<le> l \<Longrightarrow> i + k < j + l" |
|
1373 |
and "i \<le> j \<and> k < l \<Longrightarrow> i + k < j + l" |
|
1374 |
and "i < j \<and> k < l \<Longrightarrow> i + k < j + l" |
|
1375 |
by (auto intro: add_strict_right_mono add_strict_left_mono |
|
1376 |
add_less_le_mono add_le_less_mono add_strict_mono) |
|
1377 |
||
17085 | 1378 |
text{*Simplification of @{term "x-y < 0"}, etc.*} |
29833 | 1379 |
lemmas diff_less_0_iff_less [simp, noatp] = less_iff_diff_less_0 [symmetric] |
1380 |
lemmas diff_le_0_iff_le [simp, noatp] = le_iff_diff_le_0 [symmetric] |
|
17085 | 1381 |
|
22482 | 1382 |
ML {* |
27250 | 1383 |
structure ab_group_add_cancel = Abel_Cancel |
1384 |
( |
|
22482 | 1385 |
|
1386 |
(* term order for abelian groups *) |
|
1387 |
||
1388 |
fun agrp_ord (Const (a, _)) = find_index (fn a' => a = a') |
|
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset
|
1389 |
[@{const_name Algebras.zero}, @{const_name Algebras.plus}, |
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset
|
1390 |
@{const_name Algebras.uminus}, @{const_name Algebras.minus}] |
22482 | 1391 |
| agrp_ord _ = ~1; |
1392 |
||
29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
28823
diff
changeset
|
1393 |
fun termless_agrp (a, b) = (TermOrd.term_lpo agrp_ord (a, b) = LESS); |
22482 | 1394 |
|
1395 |
local |
|
1396 |
val ac1 = mk_meta_eq @{thm add_assoc}; |
|
1397 |
val ac2 = mk_meta_eq @{thm add_commute}; |
|
1398 |
val ac3 = mk_meta_eq @{thm add_left_commute}; |
|
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset
|
1399 |
fun solve_add_ac thy _ (_ $ (Const (@{const_name Algebras.plus},_) $ _ $ _) $ _) = |
22482 | 1400 |
SOME ac1 |
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset
|
1401 |
| solve_add_ac thy _ (_ $ x $ (Const (@{const_name Algebras.plus},_) $ y $ z)) = |
22482 | 1402 |
if termless_agrp (y, x) then SOME ac3 else NONE |
1403 |
| solve_add_ac thy _ (_ $ x $ y) = |
|
1404 |
if termless_agrp (y, x) then SOME ac2 else NONE |
|
1405 |
| solve_add_ac thy _ _ = NONE |
|
1406 |
in |
|
32010 | 1407 |
val add_ac_proc = Simplifier.simproc @{theory} |
22482 | 1408 |
"add_ac_proc" ["x + y::'a::ab_semigroup_add"] solve_add_ac; |
1409 |
end; |
|
1410 |
||
27250 | 1411 |
val eq_reflection = @{thm eq_reflection}; |
1412 |
||
1413 |
val T = @{typ "'a::ab_group_add"}; |
|
1414 |
||
22482 | 1415 |
val cancel_ss = HOL_basic_ss settermless termless_agrp |
1416 |
addsimprocs [add_ac_proc] addsimps |
|
23085 | 1417 |
[@{thm add_0_left}, @{thm add_0_right}, @{thm diff_def}, |
22482 | 1418 |
@{thm minus_add_distrib}, @{thm minus_minus}, @{thm minus_zero}, |
1419 |
@{thm right_minus}, @{thm left_minus}, @{thm add_minus_cancel}, |
|
1420 |
@{thm minus_add_cancel}]; |
|
27250 | 1421 |
|
1422 |
val sum_pats = [@{cterm "x + y::'a::ab_group_add"}, @{cterm "x - y::'a::ab_group_add"}]; |
|
22482 | 1423 |
|
22548 | 1424 |
val eqI_rules = [@{thm less_eqI}, @{thm le_eqI}, @{thm eq_eqI}]; |
22482 | 1425 |
|
1426 |
val dest_eqI = |
|
1427 |
fst o HOLogic.dest_bin "op =" HOLogic.boolT o HOLogic.dest_Trueprop o concl_of; |
|
1428 |
||
27250 | 1429 |
); |
22482 | 1430 |
*} |
1431 |
||
26480 | 1432 |
ML {* |
22482 | 1433 |
Addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]; |
1434 |
*} |
|
17085 | 1435 |
|
33364 | 1436 |
code_modulename SML |
1437 |
OrderedGroup Arith |
|
1438 |
||
1439 |
code_modulename OCaml |
|
1440 |
OrderedGroup Arith |
|
1441 |
||
1442 |
code_modulename Haskell |
|
1443 |
OrderedGroup Arith |
|
1444 |
||
14738 | 1445 |
end |