|
1 (* Title: ZF/Int.thy |
|
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
3 Copyright 1993 University of Cambridge |
|
4 *) |
|
5 |
|
6 section\<open>The Integers as Equivalence Classes Over Pairs of Natural Numbers\<close> |
|
7 |
|
8 theory Int imports EquivClass ArithSimp begin |
|
9 |
|
10 definition |
|
11 intrel :: i where |
|
12 "intrel == {p \<in> (nat*nat)*(nat*nat). |
|
13 \<exists>x1 y1 x2 y2. p=<<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1}" |
|
14 |
|
15 definition |
|
16 int :: i where |
|
17 "int == (nat*nat)//intrel" |
|
18 |
|
19 definition |
|
20 int_of :: "i=>i" \<comment> \<open>coercion from nat to int\<close> ("$# _" [80] 80) where |
|
21 "$# m == intrel `` {<natify(m), 0>}" |
|
22 |
|
23 definition |
|
24 intify :: "i=>i" \<comment> \<open>coercion from ANYTHING to int\<close> where |
|
25 "intify(m) == if m \<in> int then m else $#0" |
|
26 |
|
27 definition |
|
28 raw_zminus :: "i=>i" where |
|
29 "raw_zminus(z) == \<Union><x,y>\<in>z. intrel``{<y,x>}" |
|
30 |
|
31 definition |
|
32 zminus :: "i=>i" ("$- _" [80] 80) where |
|
33 "$- z == raw_zminus (intify(z))" |
|
34 |
|
35 definition |
|
36 znegative :: "i=>o" where |
|
37 "znegative(z) == \<exists>x y. x<y & y\<in>nat & <x,y>\<in>z" |
|
38 |
|
39 definition |
|
40 iszero :: "i=>o" where |
|
41 "iszero(z) == z = $# 0" |
|
42 |
|
43 definition |
|
44 raw_nat_of :: "i=>i" where |
|
45 "raw_nat_of(z) == natify (\<Union><x,y>\<in>z. x#-y)" |
|
46 |
|
47 definition |
|
48 nat_of :: "i=>i" where |
|
49 "nat_of(z) == raw_nat_of (intify(z))" |
|
50 |
|
51 definition |
|
52 zmagnitude :: "i=>i" where |
|
53 \<comment> \<open>could be replaced by an absolute value function from int to int?\<close> |
|
54 "zmagnitude(z) == |
|
55 THE m. m\<in>nat & ((~ znegative(z) & z = $# m) | |
|
56 (znegative(z) & $- z = $# m))" |
|
57 |
|
58 definition |
|
59 raw_zmult :: "[i,i]=>i" where |
|
60 (*Cannot use UN<x1,y2> here or in zadd because of the form of congruent2. |
|
61 Perhaps a "curried" or even polymorphic congruent predicate would be |
|
62 better.*) |
|
63 "raw_zmult(z1,z2) == |
|
64 \<Union>p1\<in>z1. \<Union>p2\<in>z2. split(%x1 y1. split(%x2 y2. |
|
65 intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1)" |
|
66 |
|
67 definition |
|
68 zmult :: "[i,i]=>i" (infixl "$*" 70) where |
|
69 "z1 $* z2 == raw_zmult (intify(z1),intify(z2))" |
|
70 |
|
71 definition |
|
72 raw_zadd :: "[i,i]=>i" where |
|
73 "raw_zadd (z1, z2) == |
|
74 \<Union>z1\<in>z1. \<Union>z2\<in>z2. let <x1,y1>=z1; <x2,y2>=z2 |
|
75 in intrel``{<x1#+x2, y1#+y2>}" |
|
76 |
|
77 definition |
|
78 zadd :: "[i,i]=>i" (infixl "$+" 65) where |
|
79 "z1 $+ z2 == raw_zadd (intify(z1),intify(z2))" |
|
80 |
|
81 definition |
|
82 zdiff :: "[i,i]=>i" (infixl "$-" 65) where |
|
83 "z1 $- z2 == z1 $+ zminus(z2)" |
|
84 |
|
85 definition |
|
86 zless :: "[i,i]=>o" (infixl "$<" 50) where |
|
87 "z1 $< z2 == znegative(z1 $- z2)" |
|
88 |
|
89 definition |
|
90 zle :: "[i,i]=>o" (infixl "$\<le>" 50) where |
|
91 "z1 $\<le> z2 == z1 $< z2 | intify(z1)=intify(z2)" |
|
92 |
|
93 |
|
94 declare quotientE [elim!] |
|
95 |
|
96 subsection\<open>Proving that @{term intrel} is an equivalence relation\<close> |
|
97 |
|
98 (** Natural deduction for intrel **) |
|
99 |
|
100 lemma intrel_iff [simp]: |
|
101 "<<x1,y1>,<x2,y2>>: intrel \<longleftrightarrow> |
|
102 x1\<in>nat & y1\<in>nat & x2\<in>nat & y2\<in>nat & x1#+y2 = x2#+y1" |
|
103 by (simp add: intrel_def) |
|
104 |
|
105 lemma intrelI [intro!]: |
|
106 "[| x1#+y2 = x2#+y1; x1\<in>nat; y1\<in>nat; x2\<in>nat; y2\<in>nat |] |
|
107 ==> <<x1,y1>,<x2,y2>>: intrel" |
|
108 by (simp add: intrel_def) |
|
109 |
|
110 lemma intrelE [elim!]: |
|
111 "[| p \<in> intrel; |
|
112 !!x1 y1 x2 y2. [| p = <<x1,y1>,<x2,y2>>; x1#+y2 = x2#+y1; |
|
113 x1\<in>nat; y1\<in>nat; x2\<in>nat; y2\<in>nat |] ==> Q |] |
|
114 ==> Q" |
|
115 by (simp add: intrel_def, blast) |
|
116 |
|
117 lemma int_trans_lemma: |
|
118 "[| x1 #+ y2 = x2 #+ y1; x2 #+ y3 = x3 #+ y2 |] ==> x1 #+ y3 = x3 #+ y1" |
|
119 apply (rule sym) |
|
120 apply (erule add_left_cancel)+ |
|
121 apply (simp_all (no_asm_simp)) |
|
122 done |
|
123 |
|
124 lemma equiv_intrel: "equiv(nat*nat, intrel)" |
|
125 apply (simp add: equiv_def refl_def sym_def trans_def) |
|
126 apply (fast elim!: sym int_trans_lemma) |
|
127 done |
|
128 |
|
129 lemma image_intrel_int: "[| m\<in>nat; n\<in>nat |] ==> intrel `` {<m,n>} \<in> int" |
|
130 by (simp add: int_def) |
|
131 |
|
132 declare equiv_intrel [THEN eq_equiv_class_iff, simp] |
|
133 declare conj_cong [cong] |
|
134 |
|
135 lemmas eq_intrelD = eq_equiv_class [OF _ equiv_intrel] |
|
136 |
|
137 (** int_of: the injection from nat to int **) |
|
138 |
|
139 lemma int_of_type [simp,TC]: "$#m \<in> int" |
|
140 by (simp add: int_def quotient_def int_of_def, auto) |
|
141 |
|
142 lemma int_of_eq [iff]: "($# m = $# n) \<longleftrightarrow> natify(m)=natify(n)" |
|
143 by (simp add: int_of_def) |
|
144 |
|
145 lemma int_of_inject: "[| $#m = $#n; m\<in>nat; n\<in>nat |] ==> m=n" |
|
146 by (drule int_of_eq [THEN iffD1], auto) |
|
147 |
|
148 |
|
149 (** intify: coercion from anything to int **) |
|
150 |
|
151 lemma intify_in_int [iff,TC]: "intify(x) \<in> int" |
|
152 by (simp add: intify_def) |
|
153 |
|
154 lemma intify_ident [simp]: "n \<in> int ==> intify(n) = n" |
|
155 by (simp add: intify_def) |
|
156 |
|
157 |
|
158 subsection\<open>Collapsing rules: to remove @{term intify} |
|
159 from arithmetic expressions\<close> |
|
160 |
|
161 lemma intify_idem [simp]: "intify(intify(x)) = intify(x)" |
|
162 by simp |
|
163 |
|
164 lemma int_of_natify [simp]: "$# (natify(m)) = $# m" |
|
165 by (simp add: int_of_def) |
|
166 |
|
167 lemma zminus_intify [simp]: "$- (intify(m)) = $- m" |
|
168 by (simp add: zminus_def) |
|
169 |
|
170 (** Addition **) |
|
171 |
|
172 lemma zadd_intify1 [simp]: "intify(x) $+ y = x $+ y" |
|
173 by (simp add: zadd_def) |
|
174 |
|
175 lemma zadd_intify2 [simp]: "x $+ intify(y) = x $+ y" |
|
176 by (simp add: zadd_def) |
|
177 |
|
178 (** Subtraction **) |
|
179 |
|
180 lemma zdiff_intify1 [simp]:"intify(x) $- y = x $- y" |
|
181 by (simp add: zdiff_def) |
|
182 |
|
183 lemma zdiff_intify2 [simp]:"x $- intify(y) = x $- y" |
|
184 by (simp add: zdiff_def) |
|
185 |
|
186 (** Multiplication **) |
|
187 |
|
188 lemma zmult_intify1 [simp]:"intify(x) $* y = x $* y" |
|
189 by (simp add: zmult_def) |
|
190 |
|
191 lemma zmult_intify2 [simp]:"x $* intify(y) = x $* y" |
|
192 by (simp add: zmult_def) |
|
193 |
|
194 (** Orderings **) |
|
195 |
|
196 lemma zless_intify1 [simp]:"intify(x) $< y \<longleftrightarrow> x $< y" |
|
197 by (simp add: zless_def) |
|
198 |
|
199 lemma zless_intify2 [simp]:"x $< intify(y) \<longleftrightarrow> x $< y" |
|
200 by (simp add: zless_def) |
|
201 |
|
202 lemma zle_intify1 [simp]:"intify(x) $\<le> y \<longleftrightarrow> x $\<le> y" |
|
203 by (simp add: zle_def) |
|
204 |
|
205 lemma zle_intify2 [simp]:"x $\<le> intify(y) \<longleftrightarrow> x $\<le> y" |
|
206 by (simp add: zle_def) |
|
207 |
|
208 |
|
209 subsection\<open>@{term zminus}: unary negation on @{term int}\<close> |
|
210 |
|
211 lemma zminus_congruent: "(%<x,y>. intrel``{<y,x>}) respects intrel" |
|
212 by (auto simp add: congruent_def add_ac) |
|
213 |
|
214 lemma raw_zminus_type: "z \<in> int ==> raw_zminus(z) \<in> int" |
|
215 apply (simp add: int_def raw_zminus_def) |
|
216 apply (typecheck add: UN_equiv_class_type [OF equiv_intrel zminus_congruent]) |
|
217 done |
|
218 |
|
219 lemma zminus_type [TC,iff]: "$-z \<in> int" |
|
220 by (simp add: zminus_def raw_zminus_type) |
|
221 |
|
222 lemma raw_zminus_inject: |
|
223 "[| raw_zminus(z) = raw_zminus(w); z \<in> int; w \<in> int |] ==> z=w" |
|
224 apply (simp add: int_def raw_zminus_def) |
|
225 apply (erule UN_equiv_class_inject [OF equiv_intrel zminus_congruent], safe) |
|
226 apply (auto dest: eq_intrelD simp add: add_ac) |
|
227 done |
|
228 |
|
229 lemma zminus_inject_intify [dest!]: "$-z = $-w ==> intify(z) = intify(w)" |
|
230 apply (simp add: zminus_def) |
|
231 apply (blast dest!: raw_zminus_inject) |
|
232 done |
|
233 |
|
234 lemma zminus_inject: "[| $-z = $-w; z \<in> int; w \<in> int |] ==> z=w" |
|
235 by auto |
|
236 |
|
237 lemma raw_zminus: |
|
238 "[| x\<in>nat; y\<in>nat |] ==> raw_zminus(intrel``{<x,y>}) = intrel `` {<y,x>}" |
|
239 apply (simp add: raw_zminus_def UN_equiv_class [OF equiv_intrel zminus_congruent]) |
|
240 done |
|
241 |
|
242 lemma zminus: |
|
243 "[| x\<in>nat; y\<in>nat |] |
|
244 ==> $- (intrel``{<x,y>}) = intrel `` {<y,x>}" |
|
245 by (simp add: zminus_def raw_zminus image_intrel_int) |
|
246 |
|
247 lemma raw_zminus_zminus: "z \<in> int ==> raw_zminus (raw_zminus(z)) = z" |
|
248 by (auto simp add: int_def raw_zminus) |
|
249 |
|
250 lemma zminus_zminus_intify [simp]: "$- ($- z) = intify(z)" |
|
251 by (simp add: zminus_def raw_zminus_type raw_zminus_zminus) |
|
252 |
|
253 lemma zminus_int0 [simp]: "$- ($#0) = $#0" |
|
254 by (simp add: int_of_def zminus) |
|
255 |
|
256 lemma zminus_zminus: "z \<in> int ==> $- ($- z) = z" |
|
257 by simp |
|
258 |
|
259 |
|
260 subsection\<open>@{term znegative}: the test for negative integers\<close> |
|
261 |
|
262 lemma znegative: "[| x\<in>nat; y\<in>nat |] ==> znegative(intrel``{<x,y>}) \<longleftrightarrow> x<y" |
|
263 apply (cases "x<y") |
|
264 apply (auto simp add: znegative_def not_lt_iff_le) |
|
265 apply (subgoal_tac "y #+ x2 < x #+ y2", force) |
|
266 apply (rule add_le_lt_mono, auto) |
|
267 done |
|
268 |
|
269 (*No natural number is negative!*) |
|
270 lemma not_znegative_int_of [iff]: "~ znegative($# n)" |
|
271 by (simp add: znegative int_of_def) |
|
272 |
|
273 lemma znegative_zminus_int_of [simp]: "znegative($- $# succ(n))" |
|
274 by (simp add: znegative int_of_def zminus natify_succ) |
|
275 |
|
276 lemma not_znegative_imp_zero: "~ znegative($- $# n) ==> natify(n)=0" |
|
277 by (simp add: znegative int_of_def zminus Ord_0_lt_iff [THEN iff_sym]) |
|
278 |
|
279 |
|
280 subsection\<open>@{term nat_of}: Coercion of an Integer to a Natural Number\<close> |
|
281 |
|
282 lemma nat_of_intify [simp]: "nat_of(intify(z)) = nat_of(z)" |
|
283 by (simp add: nat_of_def) |
|
284 |
|
285 lemma nat_of_congruent: "(\<lambda>x. (\<lambda>\<langle>x,y\<rangle>. x #- y)(x)) respects intrel" |
|
286 by (auto simp add: congruent_def split: nat_diff_split) |
|
287 |
|
288 lemma raw_nat_of: |
|
289 "[| x\<in>nat; y\<in>nat |] ==> raw_nat_of(intrel``{<x,y>}) = x#-y" |
|
290 by (simp add: raw_nat_of_def UN_equiv_class [OF equiv_intrel nat_of_congruent]) |
|
291 |
|
292 lemma raw_nat_of_int_of: "raw_nat_of($# n) = natify(n)" |
|
293 by (simp add: int_of_def raw_nat_of) |
|
294 |
|
295 lemma nat_of_int_of [simp]: "nat_of($# n) = natify(n)" |
|
296 by (simp add: raw_nat_of_int_of nat_of_def) |
|
297 |
|
298 lemma raw_nat_of_type: "raw_nat_of(z) \<in> nat" |
|
299 by (simp add: raw_nat_of_def) |
|
300 |
|
301 lemma nat_of_type [iff,TC]: "nat_of(z) \<in> nat" |
|
302 by (simp add: nat_of_def raw_nat_of_type) |
|
303 |
|
304 subsection\<open>zmagnitude: magnitide of an integer, as a natural number\<close> |
|
305 |
|
306 lemma zmagnitude_int_of [simp]: "zmagnitude($# n) = natify(n)" |
|
307 by (auto simp add: zmagnitude_def int_of_eq) |
|
308 |
|
309 lemma natify_int_of_eq: "natify(x)=n ==> $#x = $# n" |
|
310 apply (drule sym) |
|
311 apply (simp (no_asm_simp) add: int_of_eq) |
|
312 done |
|
313 |
|
314 lemma zmagnitude_zminus_int_of [simp]: "zmagnitude($- $# n) = natify(n)" |
|
315 apply (simp add: zmagnitude_def) |
|
316 apply (rule the_equality) |
|
317 apply (auto dest!: not_znegative_imp_zero natify_int_of_eq |
|
318 iff del: int_of_eq, auto) |
|
319 done |
|
320 |
|
321 lemma zmagnitude_type [iff,TC]: "zmagnitude(z)\<in>nat" |
|
322 apply (simp add: zmagnitude_def) |
|
323 apply (rule theI2, auto) |
|
324 done |
|
325 |
|
326 lemma not_zneg_int_of: |
|
327 "[| z \<in> int; ~ znegative(z) |] ==> \<exists>n\<in>nat. z = $# n" |
|
328 apply (auto simp add: int_def znegative int_of_def not_lt_iff_le) |
|
329 apply (rename_tac x y) |
|
330 apply (rule_tac x="x#-y" in bexI) |
|
331 apply (auto simp add: add_diff_inverse2) |
|
332 done |
|
333 |
|
334 lemma not_zneg_mag [simp]: |
|
335 "[| z \<in> int; ~ znegative(z) |] ==> $# (zmagnitude(z)) = z" |
|
336 by (drule not_zneg_int_of, auto) |
|
337 |
|
338 lemma zneg_int_of: |
|
339 "[| znegative(z); z \<in> int |] ==> \<exists>n\<in>nat. z = $- ($# succ(n))" |
|
340 by (auto simp add: int_def znegative zminus int_of_def dest!: less_imp_succ_add) |
|
341 |
|
342 lemma zneg_mag [simp]: |
|
343 "[| znegative(z); z \<in> int |] ==> $# (zmagnitude(z)) = $- z" |
|
344 by (drule zneg_int_of, auto) |
|
345 |
|
346 lemma int_cases: "z \<in> int ==> \<exists>n\<in>nat. z = $# n | z = $- ($# succ(n))" |
|
347 apply (case_tac "znegative (z) ") |
|
348 prefer 2 apply (blast dest: not_zneg_mag sym) |
|
349 apply (blast dest: zneg_int_of) |
|
350 done |
|
351 |
|
352 lemma not_zneg_raw_nat_of: |
|
353 "[| ~ znegative(z); z \<in> int |] ==> $# (raw_nat_of(z)) = z" |
|
354 apply (drule not_zneg_int_of) |
|
355 apply (auto simp add: raw_nat_of_type raw_nat_of_int_of) |
|
356 done |
|
357 |
|
358 lemma not_zneg_nat_of_intify: |
|
359 "~ znegative(intify(z)) ==> $# (nat_of(z)) = intify(z)" |
|
360 by (simp (no_asm_simp) add: nat_of_def not_zneg_raw_nat_of) |
|
361 |
|
362 lemma not_zneg_nat_of: "[| ~ znegative(z); z \<in> int |] ==> $# (nat_of(z)) = z" |
|
363 apply (simp (no_asm_simp) add: not_zneg_nat_of_intify) |
|
364 done |
|
365 |
|
366 lemma zneg_nat_of [simp]: "znegative(intify(z)) ==> nat_of(z) = 0" |
|
367 apply (subgoal_tac "intify(z) \<in> int") |
|
368 apply (simp add: int_def) |
|
369 apply (auto simp add: znegative nat_of_def raw_nat_of |
|
370 split: nat_diff_split) |
|
371 done |
|
372 |
|
373 |
|
374 subsection\<open>@{term zadd}: addition on int\<close> |
|
375 |
|
376 text\<open>Congruence Property for Addition\<close> |
|
377 lemma zadd_congruent2: |
|
378 "(%z1 z2. let <x1,y1>=z1; <x2,y2>=z2 |
|
379 in intrel``{<x1#+x2, y1#+y2>}) |
|
380 respects2 intrel" |
|
381 apply (simp add: congruent2_def) |
|
382 (*Proof via congruent2_commuteI seems longer*) |
|
383 apply safe |
|
384 apply (simp (no_asm_simp) add: add_assoc Let_def) |
|
385 (*The rest should be trivial, but rearranging terms is hard |
|
386 add_ac does not help rewriting with the assumptions.*) |
|
387 apply (rule_tac m1 = x1a in add_left_commute [THEN ssubst]) |
|
388 apply (rule_tac m1 = x2a in add_left_commute [THEN ssubst]) |
|
389 apply (simp (no_asm_simp) add: add_assoc [symmetric]) |
|
390 done |
|
391 |
|
392 lemma raw_zadd_type: "[| z \<in> int; w \<in> int |] ==> raw_zadd(z,w) \<in> int" |
|
393 apply (simp add: int_def raw_zadd_def) |
|
394 apply (rule UN_equiv_class_type2 [OF equiv_intrel zadd_congruent2], assumption+) |
|
395 apply (simp add: Let_def) |
|
396 done |
|
397 |
|
398 lemma zadd_type [iff,TC]: "z $+ w \<in> int" |
|
399 by (simp add: zadd_def raw_zadd_type) |
|
400 |
|
401 lemma raw_zadd: |
|
402 "[| x1\<in>nat; y1\<in>nat; x2\<in>nat; y2\<in>nat |] |
|
403 ==> raw_zadd (intrel``{<x1,y1>}, intrel``{<x2,y2>}) = |
|
404 intrel `` {<x1#+x2, y1#+y2>}" |
|
405 apply (simp add: raw_zadd_def |
|
406 UN_equiv_class2 [OF equiv_intrel equiv_intrel zadd_congruent2]) |
|
407 apply (simp add: Let_def) |
|
408 done |
|
409 |
|
410 lemma zadd: |
|
411 "[| x1\<in>nat; y1\<in>nat; x2\<in>nat; y2\<in>nat |] |
|
412 ==> (intrel``{<x1,y1>}) $+ (intrel``{<x2,y2>}) = |
|
413 intrel `` {<x1#+x2, y1#+y2>}" |
|
414 by (simp add: zadd_def raw_zadd image_intrel_int) |
|
415 |
|
416 lemma raw_zadd_int0: "z \<in> int ==> raw_zadd ($#0,z) = z" |
|
417 by (auto simp add: int_def int_of_def raw_zadd) |
|
418 |
|
419 lemma zadd_int0_intify [simp]: "$#0 $+ z = intify(z)" |
|
420 by (simp add: zadd_def raw_zadd_int0) |
|
421 |
|
422 lemma zadd_int0: "z \<in> int ==> $#0 $+ z = z" |
|
423 by simp |
|
424 |
|
425 lemma raw_zminus_zadd_distrib: |
|
426 "[| z \<in> int; w \<in> int |] ==> $- raw_zadd(z,w) = raw_zadd($- z, $- w)" |
|
427 by (auto simp add: zminus raw_zadd int_def) |
|
428 |
|
429 lemma zminus_zadd_distrib [simp]: "$- (z $+ w) = $- z $+ $- w" |
|
430 by (simp add: zadd_def raw_zminus_zadd_distrib) |
|
431 |
|
432 lemma raw_zadd_commute: |
|
433 "[| z \<in> int; w \<in> int |] ==> raw_zadd(z,w) = raw_zadd(w,z)" |
|
434 by (auto simp add: raw_zadd add_ac int_def) |
|
435 |
|
436 lemma zadd_commute: "z $+ w = w $+ z" |
|
437 by (simp add: zadd_def raw_zadd_commute) |
|
438 |
|
439 lemma raw_zadd_assoc: |
|
440 "[| z1: int; z2: int; z3: int |] |
|
441 ==> raw_zadd (raw_zadd(z1,z2),z3) = raw_zadd(z1,raw_zadd(z2,z3))" |
|
442 by (auto simp add: int_def raw_zadd add_assoc) |
|
443 |
|
444 lemma zadd_assoc: "(z1 $+ z2) $+ z3 = z1 $+ (z2 $+ z3)" |
|
445 by (simp add: zadd_def raw_zadd_type raw_zadd_assoc) |
|
446 |
|
447 (*For AC rewriting*) |
|
448 lemma zadd_left_commute: "z1$+(z2$+z3) = z2$+(z1$+z3)" |
|
449 apply (simp add: zadd_assoc [symmetric]) |
|
450 apply (simp add: zadd_commute) |
|
451 done |
|
452 |
|
453 (*Integer addition is an AC operator*) |
|
454 lemmas zadd_ac = zadd_assoc zadd_commute zadd_left_commute |
|
455 |
|
456 lemma int_of_add: "$# (m #+ n) = ($#m) $+ ($#n)" |
|
457 by (simp add: int_of_def zadd) |
|
458 |
|
459 lemma int_succ_int_1: "$# succ(m) = $# 1 $+ ($# m)" |
|
460 by (simp add: int_of_add [symmetric] natify_succ) |
|
461 |
|
462 lemma int_of_diff: |
|
463 "[| m\<in>nat; n \<le> m |] ==> $# (m #- n) = ($#m) $- ($#n)" |
|
464 apply (simp add: int_of_def zdiff_def) |
|
465 apply (frule lt_nat_in_nat) |
|
466 apply (simp_all add: zadd zminus add_diff_inverse2) |
|
467 done |
|
468 |
|
469 lemma raw_zadd_zminus_inverse: "z \<in> int ==> raw_zadd (z, $- z) = $#0" |
|
470 by (auto simp add: int_def int_of_def zminus raw_zadd add_commute) |
|
471 |
|
472 lemma zadd_zminus_inverse [simp]: "z $+ ($- z) = $#0" |
|
473 apply (simp add: zadd_def) |
|
474 apply (subst zminus_intify [symmetric]) |
|
475 apply (rule intify_in_int [THEN raw_zadd_zminus_inverse]) |
|
476 done |
|
477 |
|
478 lemma zadd_zminus_inverse2 [simp]: "($- z) $+ z = $#0" |
|
479 by (simp add: zadd_commute zadd_zminus_inverse) |
|
480 |
|
481 lemma zadd_int0_right_intify [simp]: "z $+ $#0 = intify(z)" |
|
482 by (rule trans [OF zadd_commute zadd_int0_intify]) |
|
483 |
|
484 lemma zadd_int0_right: "z \<in> int ==> z $+ $#0 = z" |
|
485 by simp |
|
486 |
|
487 |
|
488 subsection\<open>@{term zmult}: Integer Multiplication\<close> |
|
489 |
|
490 text\<open>Congruence property for multiplication\<close> |
|
491 lemma zmult_congruent2: |
|
492 "(%p1 p2. split(%x1 y1. split(%x2 y2. |
|
493 intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1)) |
|
494 respects2 intrel" |
|
495 apply (rule equiv_intrel [THEN congruent2_commuteI], auto) |
|
496 (*Proof that zmult is congruent in one argument*) |
|
497 apply (rename_tac x y) |
|
498 apply (frule_tac t = "%u. x#*u" in sym [THEN subst_context]) |
|
499 apply (drule_tac t = "%u. y#*u" in subst_context) |
|
500 apply (erule add_left_cancel)+ |
|
501 apply (simp_all add: add_mult_distrib_left) |
|
502 done |
|
503 |
|
504 |
|
505 lemma raw_zmult_type: "[| z \<in> int; w \<in> int |] ==> raw_zmult(z,w) \<in> int" |
|
506 apply (simp add: int_def raw_zmult_def) |
|
507 apply (rule UN_equiv_class_type2 [OF equiv_intrel zmult_congruent2], assumption+) |
|
508 apply (simp add: Let_def) |
|
509 done |
|
510 |
|
511 lemma zmult_type [iff,TC]: "z $* w \<in> int" |
|
512 by (simp add: zmult_def raw_zmult_type) |
|
513 |
|
514 lemma raw_zmult: |
|
515 "[| x1\<in>nat; y1\<in>nat; x2\<in>nat; y2\<in>nat |] |
|
516 ==> raw_zmult(intrel``{<x1,y1>}, intrel``{<x2,y2>}) = |
|
517 intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}" |
|
518 by (simp add: raw_zmult_def |
|
519 UN_equiv_class2 [OF equiv_intrel equiv_intrel zmult_congruent2]) |
|
520 |
|
521 lemma zmult: |
|
522 "[| x1\<in>nat; y1\<in>nat; x2\<in>nat; y2\<in>nat |] |
|
523 ==> (intrel``{<x1,y1>}) $* (intrel``{<x2,y2>}) = |
|
524 intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}" |
|
525 by (simp add: zmult_def raw_zmult image_intrel_int) |
|
526 |
|
527 lemma raw_zmult_int0: "z \<in> int ==> raw_zmult ($#0,z) = $#0" |
|
528 by (auto simp add: int_def int_of_def raw_zmult) |
|
529 |
|
530 lemma zmult_int0 [simp]: "$#0 $* z = $#0" |
|
531 by (simp add: zmult_def raw_zmult_int0) |
|
532 |
|
533 lemma raw_zmult_int1: "z \<in> int ==> raw_zmult ($#1,z) = z" |
|
534 by (auto simp add: int_def int_of_def raw_zmult) |
|
535 |
|
536 lemma zmult_int1_intify [simp]: "$#1 $* z = intify(z)" |
|
537 by (simp add: zmult_def raw_zmult_int1) |
|
538 |
|
539 lemma zmult_int1: "z \<in> int ==> $#1 $* z = z" |
|
540 by simp |
|
541 |
|
542 lemma raw_zmult_commute: |
|
543 "[| z \<in> int; w \<in> int |] ==> raw_zmult(z,w) = raw_zmult(w,z)" |
|
544 by (auto simp add: int_def raw_zmult add_ac mult_ac) |
|
545 |
|
546 lemma zmult_commute: "z $* w = w $* z" |
|
547 by (simp add: zmult_def raw_zmult_commute) |
|
548 |
|
549 lemma raw_zmult_zminus: |
|
550 "[| z \<in> int; w \<in> int |] ==> raw_zmult($- z, w) = $- raw_zmult(z, w)" |
|
551 by (auto simp add: int_def zminus raw_zmult add_ac) |
|
552 |
|
553 lemma zmult_zminus [simp]: "($- z) $* w = $- (z $* w)" |
|
554 apply (simp add: zmult_def raw_zmult_zminus) |
|
555 apply (subst zminus_intify [symmetric], rule raw_zmult_zminus, auto) |
|
556 done |
|
557 |
|
558 lemma zmult_zminus_right [simp]: "w $* ($- z) = $- (w $* z)" |
|
559 by (simp add: zmult_commute [of w]) |
|
560 |
|
561 lemma raw_zmult_assoc: |
|
562 "[| z1: int; z2: int; z3: int |] |
|
563 ==> raw_zmult (raw_zmult(z1,z2),z3) = raw_zmult(z1,raw_zmult(z2,z3))" |
|
564 by (auto simp add: int_def raw_zmult add_mult_distrib_left add_ac mult_ac) |
|
565 |
|
566 lemma zmult_assoc: "(z1 $* z2) $* z3 = z1 $* (z2 $* z3)" |
|
567 by (simp add: zmult_def raw_zmult_type raw_zmult_assoc) |
|
568 |
|
569 (*For AC rewriting*) |
|
570 lemma zmult_left_commute: "z1$*(z2$*z3) = z2$*(z1$*z3)" |
|
571 apply (simp add: zmult_assoc [symmetric]) |
|
572 apply (simp add: zmult_commute) |
|
573 done |
|
574 |
|
575 (*Integer multiplication is an AC operator*) |
|
576 lemmas zmult_ac = zmult_assoc zmult_commute zmult_left_commute |
|
577 |
|
578 lemma raw_zadd_zmult_distrib: |
|
579 "[| z1: int; z2: int; w \<in> int |] |
|
580 ==> raw_zmult(raw_zadd(z1,z2), w) = |
|
581 raw_zadd (raw_zmult(z1,w), raw_zmult(z2,w))" |
|
582 by (auto simp add: int_def raw_zadd raw_zmult add_mult_distrib_left add_ac mult_ac) |
|
583 |
|
584 lemma zadd_zmult_distrib: "(z1 $+ z2) $* w = (z1 $* w) $+ (z2 $* w)" |
|
585 by (simp add: zmult_def zadd_def raw_zadd_type raw_zmult_type |
|
586 raw_zadd_zmult_distrib) |
|
587 |
|
588 lemma zadd_zmult_distrib2: "w $* (z1 $+ z2) = (w $* z1) $+ (w $* z2)" |
|
589 by (simp add: zmult_commute [of w] zadd_zmult_distrib) |
|
590 |
|
591 lemmas int_typechecks = |
|
592 int_of_type zminus_type zmagnitude_type zadd_type zmult_type |
|
593 |
|
594 |
|
595 (*** Subtraction laws ***) |
|
596 |
|
597 lemma zdiff_type [iff,TC]: "z $- w \<in> int" |
|
598 by (simp add: zdiff_def) |
|
599 |
|
600 lemma zminus_zdiff_eq [simp]: "$- (z $- y) = y $- z" |
|
601 by (simp add: zdiff_def zadd_commute) |
|
602 |
|
603 lemma zdiff_zmult_distrib: "(z1 $- z2) $* w = (z1 $* w) $- (z2 $* w)" |
|
604 apply (simp add: zdiff_def) |
|
605 apply (subst zadd_zmult_distrib) |
|
606 apply (simp add: zmult_zminus) |
|
607 done |
|
608 |
|
609 lemma zdiff_zmult_distrib2: "w $* (z1 $- z2) = (w $* z1) $- (w $* z2)" |
|
610 by (simp add: zmult_commute [of w] zdiff_zmult_distrib) |
|
611 |
|
612 lemma zadd_zdiff_eq: "x $+ (y $- z) = (x $+ y) $- z" |
|
613 by (simp add: zdiff_def zadd_ac) |
|
614 |
|
615 lemma zdiff_zadd_eq: "(x $- y) $+ z = (x $+ z) $- y" |
|
616 by (simp add: zdiff_def zadd_ac) |
|
617 |
|
618 |
|
619 subsection\<open>The "Less Than" Relation\<close> |
|
620 |
|
621 (*"Less than" is a linear ordering*) |
|
622 lemma zless_linear_lemma: |
|
623 "[| z \<in> int; w \<in> int |] ==> z$<w | z=w | w$<z" |
|
624 apply (simp add: int_def zless_def znegative_def zdiff_def, auto) |
|
625 apply (simp add: zadd zminus image_iff Bex_def) |
|
626 apply (rule_tac i = "xb#+ya" and j = "xc #+ y" in Ord_linear_lt) |
|
627 apply (force dest!: spec simp add: add_ac)+ |
|
628 done |
|
629 |
|
630 lemma zless_linear: "z$<w | intify(z)=intify(w) | w$<z" |
|
631 apply (cut_tac z = " intify (z) " and w = " intify (w) " in zless_linear_lemma) |
|
632 apply auto |
|
633 done |
|
634 |
|
635 lemma zless_not_refl [iff]: "~ (z$<z)" |
|
636 by (auto simp add: zless_def znegative_def int_of_def zdiff_def) |
|
637 |
|
638 lemma neq_iff_zless: "[| x \<in> int; y \<in> int |] ==> (x \<noteq> y) \<longleftrightarrow> (x $< y | y $< x)" |
|
639 by (cut_tac z = x and w = y in zless_linear, auto) |
|
640 |
|
641 lemma zless_imp_intify_neq: "w $< z ==> intify(w) \<noteq> intify(z)" |
|
642 apply auto |
|
643 apply (subgoal_tac "~ (intify (w) $< intify (z))") |
|
644 apply (erule_tac [2] ssubst) |
|
645 apply (simp (no_asm_use)) |
|
646 apply auto |
|
647 done |
|
648 |
|
649 (*This lemma allows direct proofs of other <-properties*) |
|
650 lemma zless_imp_succ_zadd_lemma: |
|
651 "[| w $< z; w \<in> int; z \<in> int |] ==> (\<exists>n\<in>nat. z = w $+ $#(succ(n)))" |
|
652 apply (simp add: zless_def znegative_def zdiff_def int_def) |
|
653 apply (auto dest!: less_imp_succ_add simp add: zadd zminus int_of_def) |
|
654 apply (rule_tac x = k in bexI) |
|
655 apply (erule_tac i="succ (v)" for v in add_left_cancel, auto) |
|
656 done |
|
657 |
|
658 lemma zless_imp_succ_zadd: |
|
659 "w $< z ==> (\<exists>n\<in>nat. w $+ $#(succ(n)) = intify(z))" |
|
660 apply (subgoal_tac "intify (w) $< intify (z) ") |
|
661 apply (drule_tac w = "intify (w) " in zless_imp_succ_zadd_lemma) |
|
662 apply auto |
|
663 done |
|
664 |
|
665 lemma zless_succ_zadd_lemma: |
|
666 "w \<in> int ==> w $< w $+ $# succ(n)" |
|
667 apply (simp add: zless_def znegative_def zdiff_def int_def) |
|
668 apply (auto simp add: zadd zminus int_of_def image_iff) |
|
669 apply (rule_tac x = 0 in exI, auto) |
|
670 done |
|
671 |
|
672 lemma zless_succ_zadd: "w $< w $+ $# succ(n)" |
|
673 by (cut_tac intify_in_int [THEN zless_succ_zadd_lemma], auto) |
|
674 |
|
675 lemma zless_iff_succ_zadd: |
|
676 "w $< z \<longleftrightarrow> (\<exists>n\<in>nat. w $+ $#(succ(n)) = intify(z))" |
|
677 apply (rule iffI) |
|
678 apply (erule zless_imp_succ_zadd, auto) |
|
679 apply (rename_tac "n") |
|
680 apply (cut_tac w = w and n = n in zless_succ_zadd, auto) |
|
681 done |
|
682 |
|
683 lemma zless_int_of [simp]: "[| m\<in>nat; n\<in>nat |] ==> ($#m $< $#n) \<longleftrightarrow> (m<n)" |
|
684 apply (simp add: less_iff_succ_add zless_iff_succ_zadd int_of_add [symmetric]) |
|
685 apply (blast intro: sym) |
|
686 done |
|
687 |
|
688 lemma zless_trans_lemma: |
|
689 "[| x $< y; y $< z; x \<in> int; y \<in> int; z \<in> int |] ==> x $< z" |
|
690 apply (simp add: zless_def znegative_def zdiff_def int_def) |
|
691 apply (auto simp add: zadd zminus image_iff) |
|
692 apply (rename_tac x1 x2 y1 y2) |
|
693 apply (rule_tac x = "x1#+x2" in exI) |
|
694 apply (rule_tac x = "y1#+y2" in exI) |
|
695 apply (auto simp add: add_lt_mono) |
|
696 apply (rule sym) |
|
697 apply hypsubst_thin |
|
698 apply (erule add_left_cancel)+ |
|
699 apply auto |
|
700 done |
|
701 |
|
702 lemma zless_trans [trans]: "[| x $< y; y $< z |] ==> x $< z" |
|
703 apply (subgoal_tac "intify (x) $< intify (z) ") |
|
704 apply (rule_tac [2] y = "intify (y) " in zless_trans_lemma) |
|
705 apply auto |
|
706 done |
|
707 |
|
708 lemma zless_not_sym: "z $< w ==> ~ (w $< z)" |
|
709 by (blast dest: zless_trans) |
|
710 |
|
711 (* [| z $< w; ~ P ==> w $< z |] ==> P *) |
|
712 lemmas zless_asym = zless_not_sym [THEN swap] |
|
713 |
|
714 lemma zless_imp_zle: "z $< w ==> z $\<le> w" |
|
715 by (simp add: zle_def) |
|
716 |
|
717 lemma zle_linear: "z $\<le> w | w $\<le> z" |
|
718 apply (simp add: zle_def) |
|
719 apply (cut_tac zless_linear, blast) |
|
720 done |
|
721 |
|
722 |
|
723 subsection\<open>Less Than or Equals\<close> |
|
724 |
|
725 lemma zle_refl: "z $\<le> z" |
|
726 by (simp add: zle_def) |
|
727 |
|
728 lemma zle_eq_refl: "x=y ==> x $\<le> y" |
|
729 by (simp add: zle_refl) |
|
730 |
|
731 lemma zle_anti_sym_intify: "[| x $\<le> y; y $\<le> x |] ==> intify(x) = intify(y)" |
|
732 apply (simp add: zle_def, auto) |
|
733 apply (blast dest: zless_trans) |
|
734 done |
|
735 |
|
736 lemma zle_anti_sym: "[| x $\<le> y; y $\<le> x; x \<in> int; y \<in> int |] ==> x=y" |
|
737 by (drule zle_anti_sym_intify, auto) |
|
738 |
|
739 lemma zle_trans_lemma: |
|
740 "[| x \<in> int; y \<in> int; z \<in> int; x $\<le> y; y $\<le> z |] ==> x $\<le> z" |
|
741 apply (simp add: zle_def, auto) |
|
742 apply (blast intro: zless_trans) |
|
743 done |
|
744 |
|
745 lemma zle_trans [trans]: "[| x $\<le> y; y $\<le> z |] ==> x $\<le> z" |
|
746 apply (subgoal_tac "intify (x) $\<le> intify (z) ") |
|
747 apply (rule_tac [2] y = "intify (y) " in zle_trans_lemma) |
|
748 apply auto |
|
749 done |
|
750 |
|
751 lemma zle_zless_trans [trans]: "[| i $\<le> j; j $< k |] ==> i $< k" |
|
752 apply (auto simp add: zle_def) |
|
753 apply (blast intro: zless_trans) |
|
754 apply (simp add: zless_def zdiff_def zadd_def) |
|
755 done |
|
756 |
|
757 lemma zless_zle_trans [trans]: "[| i $< j; j $\<le> k |] ==> i $< k" |
|
758 apply (auto simp add: zle_def) |
|
759 apply (blast intro: zless_trans) |
|
760 apply (simp add: zless_def zdiff_def zminus_def) |
|
761 done |
|
762 |
|
763 lemma not_zless_iff_zle: "~ (z $< w) \<longleftrightarrow> (w $\<le> z)" |
|
764 apply (cut_tac z = z and w = w in zless_linear) |
|
765 apply (auto dest: zless_trans simp add: zle_def) |
|
766 apply (auto dest!: zless_imp_intify_neq) |
|
767 done |
|
768 |
|
769 lemma not_zle_iff_zless: "~ (z $\<le> w) \<longleftrightarrow> (w $< z)" |
|
770 by (simp add: not_zless_iff_zle [THEN iff_sym]) |
|
771 |
|
772 |
|
773 subsection\<open>More subtraction laws (for \<open>zcompare_rls\<close>)\<close> |
|
774 |
|
775 lemma zdiff_zdiff_eq: "(x $- y) $- z = x $- (y $+ z)" |
|
776 by (simp add: zdiff_def zadd_ac) |
|
777 |
|
778 lemma zdiff_zdiff_eq2: "x $- (y $- z) = (x $+ z) $- y" |
|
779 by (simp add: zdiff_def zadd_ac) |
|
780 |
|
781 lemma zdiff_zless_iff: "(x$-y $< z) \<longleftrightarrow> (x $< z $+ y)" |
|
782 by (simp add: zless_def zdiff_def zadd_ac) |
|
783 |
|
784 lemma zless_zdiff_iff: "(x $< z$-y) \<longleftrightarrow> (x $+ y $< z)" |
|
785 by (simp add: zless_def zdiff_def zadd_ac) |
|
786 |
|
787 lemma zdiff_eq_iff: "[| x \<in> int; z \<in> int |] ==> (x$-y = z) \<longleftrightarrow> (x = z $+ y)" |
|
788 by (auto simp add: zdiff_def zadd_assoc) |
|
789 |
|
790 lemma eq_zdiff_iff: "[| x \<in> int; z \<in> int |] ==> (x = z$-y) \<longleftrightarrow> (x $+ y = z)" |
|
791 by (auto simp add: zdiff_def zadd_assoc) |
|
792 |
|
793 lemma zdiff_zle_iff_lemma: |
|
794 "[| x \<in> int; z \<in> int |] ==> (x$-y $\<le> z) \<longleftrightarrow> (x $\<le> z $+ y)" |
|
795 by (auto simp add: zle_def zdiff_eq_iff zdiff_zless_iff) |
|
796 |
|
797 lemma zdiff_zle_iff: "(x$-y $\<le> z) \<longleftrightarrow> (x $\<le> z $+ y)" |
|
798 by (cut_tac zdiff_zle_iff_lemma [OF intify_in_int intify_in_int], simp) |
|
799 |
|
800 lemma zle_zdiff_iff_lemma: |
|
801 "[| x \<in> int; z \<in> int |] ==>(x $\<le> z$-y) \<longleftrightarrow> (x $+ y $\<le> z)" |
|
802 apply (auto simp add: zle_def zdiff_eq_iff zless_zdiff_iff) |
|
803 apply (auto simp add: zdiff_def zadd_assoc) |
|
804 done |
|
805 |
|
806 lemma zle_zdiff_iff: "(x $\<le> z$-y) \<longleftrightarrow> (x $+ y $\<le> z)" |
|
807 by (cut_tac zle_zdiff_iff_lemma [ OF intify_in_int intify_in_int], simp) |
|
808 |
|
809 text\<open>This list of rewrites simplifies (in)equalities by bringing subtractions |
|
810 to the top and then moving negative terms to the other side. |
|
811 Use with \<open>zadd_ac\<close>\<close> |
|
812 lemmas zcompare_rls = |
|
813 zdiff_def [symmetric] |
|
814 zadd_zdiff_eq zdiff_zadd_eq zdiff_zdiff_eq zdiff_zdiff_eq2 |
|
815 zdiff_zless_iff zless_zdiff_iff zdiff_zle_iff zle_zdiff_iff |
|
816 zdiff_eq_iff eq_zdiff_iff |
|
817 |
|
818 |
|
819 subsection\<open>Monotonicity and Cancellation Results for Instantiation |
|
820 of the CancelNumerals Simprocs\<close> |
|
821 |
|
822 lemma zadd_left_cancel: |
|
823 "[| w \<in> int; w': int |] ==> (z $+ w' = z $+ w) \<longleftrightarrow> (w' = w)" |
|
824 apply safe |
|
825 apply (drule_tac t = "%x. x $+ ($-z) " in subst_context) |
|
826 apply (simp add: zadd_ac) |
|
827 done |
|
828 |
|
829 lemma zadd_left_cancel_intify [simp]: |
|
830 "(z $+ w' = z $+ w) \<longleftrightarrow> intify(w') = intify(w)" |
|
831 apply (rule iff_trans) |
|
832 apply (rule_tac [2] zadd_left_cancel, auto) |
|
833 done |
|
834 |
|
835 lemma zadd_right_cancel: |
|
836 "[| w \<in> int; w': int |] ==> (w' $+ z = w $+ z) \<longleftrightarrow> (w' = w)" |
|
837 apply safe |
|
838 apply (drule_tac t = "%x. x $+ ($-z) " in subst_context) |
|
839 apply (simp add: zadd_ac) |
|
840 done |
|
841 |
|
842 lemma zadd_right_cancel_intify [simp]: |
|
843 "(w' $+ z = w $+ z) \<longleftrightarrow> intify(w') = intify(w)" |
|
844 apply (rule iff_trans) |
|
845 apply (rule_tac [2] zadd_right_cancel, auto) |
|
846 done |
|
847 |
|
848 lemma zadd_right_cancel_zless [simp]: "(w' $+ z $< w $+ z) \<longleftrightarrow> (w' $< w)" |
|
849 by (simp add: zdiff_zless_iff [THEN iff_sym] zdiff_def zadd_assoc) |
|
850 |
|
851 lemma zadd_left_cancel_zless [simp]: "(z $+ w' $< z $+ w) \<longleftrightarrow> (w' $< w)" |
|
852 by (simp add: zadd_commute [of z] zadd_right_cancel_zless) |
|
853 |
|
854 lemma zadd_right_cancel_zle [simp]: "(w' $+ z $\<le> w $+ z) \<longleftrightarrow> w' $\<le> w" |
|
855 by (simp add: zle_def) |
|
856 |
|
857 lemma zadd_left_cancel_zle [simp]: "(z $+ w' $\<le> z $+ w) \<longleftrightarrow> w' $\<le> w" |
|
858 by (simp add: zadd_commute [of z] zadd_right_cancel_zle) |
|
859 |
|
860 |
|
861 (*"v $\<le> w ==> v$+z $\<le> w$+z"*) |
|
862 lemmas zadd_zless_mono1 = zadd_right_cancel_zless [THEN iffD2] |
|
863 |
|
864 (*"v $\<le> w ==> z$+v $\<le> z$+w"*) |
|
865 lemmas zadd_zless_mono2 = zadd_left_cancel_zless [THEN iffD2] |
|
866 |
|
867 (*"v $\<le> w ==> v$+z $\<le> w$+z"*) |
|
868 lemmas zadd_zle_mono1 = zadd_right_cancel_zle [THEN iffD2] |
|
869 |
|
870 (*"v $\<le> w ==> z$+v $\<le> z$+w"*) |
|
871 lemmas zadd_zle_mono2 = zadd_left_cancel_zle [THEN iffD2] |
|
872 |
|
873 lemma zadd_zle_mono: "[| w' $\<le> w; z' $\<le> z |] ==> w' $+ z' $\<le> w $+ z" |
|
874 by (erule zadd_zle_mono1 [THEN zle_trans], simp) |
|
875 |
|
876 lemma zadd_zless_mono: "[| w' $< w; z' $\<le> z |] ==> w' $+ z' $< w $+ z" |
|
877 by (erule zadd_zless_mono1 [THEN zless_zle_trans], simp) |
|
878 |
|
879 |
|
880 subsection\<open>Comparison laws\<close> |
|
881 |
|
882 lemma zminus_zless_zminus [simp]: "($- x $< $- y) \<longleftrightarrow> (y $< x)" |
|
883 by (simp add: zless_def zdiff_def zadd_ac) |
|
884 |
|
885 lemma zminus_zle_zminus [simp]: "($- x $\<le> $- y) \<longleftrightarrow> (y $\<le> x)" |
|
886 by (simp add: not_zless_iff_zle [THEN iff_sym]) |
|
887 |
|
888 subsubsection\<open>More inequality lemmas\<close> |
|
889 |
|
890 lemma equation_zminus: "[| x \<in> int; y \<in> int |] ==> (x = $- y) \<longleftrightarrow> (y = $- x)" |
|
891 by auto |
|
892 |
|
893 lemma zminus_equation: "[| x \<in> int; y \<in> int |] ==> ($- x = y) \<longleftrightarrow> ($- y = x)" |
|
894 by auto |
|
895 |
|
896 lemma equation_zminus_intify: "(intify(x) = $- y) \<longleftrightarrow> (intify(y) = $- x)" |
|
897 apply (cut_tac x = "intify (x) " and y = "intify (y) " in equation_zminus) |
|
898 apply auto |
|
899 done |
|
900 |
|
901 lemma zminus_equation_intify: "($- x = intify(y)) \<longleftrightarrow> ($- y = intify(x))" |
|
902 apply (cut_tac x = "intify (x) " and y = "intify (y) " in zminus_equation) |
|
903 apply auto |
|
904 done |
|
905 |
|
906 |
|
907 subsubsection\<open>The next several equations are permutative: watch out!\<close> |
|
908 |
|
909 lemma zless_zminus: "(x $< $- y) \<longleftrightarrow> (y $< $- x)" |
|
910 by (simp add: zless_def zdiff_def zadd_ac) |
|
911 |
|
912 lemma zminus_zless: "($- x $< y) \<longleftrightarrow> ($- y $< x)" |
|
913 by (simp add: zless_def zdiff_def zadd_ac) |
|
914 |
|
915 lemma zle_zminus: "(x $\<le> $- y) \<longleftrightarrow> (y $\<le> $- x)" |
|
916 by (simp add: not_zless_iff_zle [THEN iff_sym] zminus_zless) |
|
917 |
|
918 lemma zminus_zle: "($- x $\<le> y) \<longleftrightarrow> ($- y $\<le> x)" |
|
919 by (simp add: not_zless_iff_zle [THEN iff_sym] zless_zminus) |
|
920 |
|
921 end |