147 apply (rule_tac x = "succ (n) " in bexI) |
147 apply (rule_tac x = "succ (n) " in bexI) |
148 apply auto |
148 apply auto |
149 done |
149 done |
150 |
150 |
151 lemma zadd_succ_lemma: |
151 lemma zadd_succ_lemma: |
152 "z \<in> int ==> (w $+ $# succ(m) $<= z) <-> (w $+ $#m $< z)" |
152 "z \<in> int ==> (w $+ $# succ(m) $<= z) \<longleftrightarrow> (w $+ $#m $< z)" |
153 apply (simp only: not_zless_iff_zle [THEN iff_sym] zless_add_succ_iff) |
153 apply (simp only: not_zless_iff_zle [THEN iff_sym] zless_add_succ_iff) |
154 apply (auto intro: zle_anti_sym elim: zless_asym |
154 apply (auto intro: zle_anti_sym elim: zless_asym |
155 simp add: zless_imp_zle not_zless_iff_zle) |
155 simp add: zless_imp_zle not_zless_iff_zle) |
156 done |
156 done |
157 |
157 |
158 lemma zadd_succ_zle_iff: "(w $+ $# succ(m) $<= z) <-> (w $+ $#m $< z)" |
158 lemma zadd_succ_zle_iff: "(w $+ $# succ(m) $<= z) \<longleftrightarrow> (w $+ $#m $< z)" |
159 apply (cut_tac z = "intify (z)" in zadd_succ_lemma) |
159 apply (cut_tac z = "intify (z)" in zadd_succ_lemma) |
160 apply auto |
160 apply auto |
161 done |
161 done |
162 |
162 |
163 (** Inequality reasoning **) |
163 (** Inequality reasoning **) |
164 |
164 |
165 lemma zless_add1_iff_zle: "(w $< z $+ #1) <-> (w$<=z)" |
165 lemma zless_add1_iff_zle: "(w $< z $+ #1) \<longleftrightarrow> (w$<=z)" |
166 apply (subgoal_tac "#1 = $# 1") |
166 apply (subgoal_tac "#1 = $# 1") |
167 apply (simp only: zless_add_succ_iff zle_def) |
167 apply (simp only: zless_add_succ_iff zle_def) |
168 apply auto |
168 apply auto |
169 done |
169 done |
170 |
170 |
171 lemma add1_zle_iff: "(w $+ #1 $<= z) <-> (w $< z)" |
171 lemma add1_zle_iff: "(w $+ #1 $<= z) \<longleftrightarrow> (w $< z)" |
172 apply (subgoal_tac "#1 = $# 1") |
172 apply (subgoal_tac "#1 = $# 1") |
173 apply (simp only: zadd_succ_zle_iff) |
173 apply (simp only: zadd_succ_zle_iff) |
174 apply auto |
174 apply auto |
175 done |
175 done |
176 |
176 |
177 lemma add1_left_zle_iff: "(#1 $+ w $<= z) <-> (w $< z)" |
177 lemma add1_left_zle_iff: "(#1 $+ w $<= z) \<longleftrightarrow> (w $< z)" |
178 apply (subst zadd_commute) |
178 apply (subst zadd_commute) |
179 apply (rule add1_zle_iff) |
179 apply (rule add1_zle_iff) |
180 done |
180 done |
181 |
181 |
182 |
182 |
278 |
278 |
279 |
279 |
280 (** Products of zeroes **) |
280 (** Products of zeroes **) |
281 |
281 |
282 lemma zmult_eq_lemma: |
282 lemma zmult_eq_lemma: |
283 "[| m \<in> int; n \<in> int |] ==> (m = #0 | n = #0) <-> (m$*n = #0)" |
283 "[| m \<in> int; n \<in> int |] ==> (m = #0 | n = #0) \<longleftrightarrow> (m$*n = #0)" |
284 apply (case_tac "m $< #0") |
284 apply (case_tac "m $< #0") |
285 apply (auto simp add: not_zless_iff_zle zle_def neq_iff_zless) |
285 apply (auto simp add: not_zless_iff_zle zle_def neq_iff_zless) |
286 apply (force dest: zmult_zless_mono1_neg zmult_zless_mono1)+ |
286 apply (force dest: zmult_zless_mono1_neg zmult_zless_mono1)+ |
287 done |
287 done |
288 |
288 |
289 lemma zmult_eq_0_iff [iff]: "(m$*n = #0) <-> (intify(m) = #0 | intify(n) = #0)" |
289 lemma zmult_eq_0_iff [iff]: "(m$*n = #0) \<longleftrightarrow> (intify(m) = #0 | intify(n) = #0)" |
290 apply (simp add: zmult_eq_lemma) |
290 apply (simp add: zmult_eq_lemma) |
291 done |
291 done |
292 |
292 |
293 |
293 |
294 (** Cancellation laws for k*m < k*n and m*k < n*k, also for @{text"\<le>"} and =, |
294 (** Cancellation laws for k*m < k*n and m*k < n*k, also for @{text"\<le>"} and =, |
295 but not (yet?) for k*m < n*k. **) |
295 but not (yet?) for k*m < n*k. **) |
296 |
296 |
297 lemma zmult_zless_lemma: |
297 lemma zmult_zless_lemma: |
298 "[| k \<in> int; m \<in> int; n \<in> int |] |
298 "[| k \<in> int; m \<in> int; n \<in> int |] |
299 ==> (m$*k $< n$*k) <-> ((#0 $< k & m$<n) | (k $< #0 & n$<m))" |
299 ==> (m$*k $< n$*k) \<longleftrightarrow> ((#0 $< k & m$<n) | (k $< #0 & n$<m))" |
300 apply (case_tac "k = #0") |
300 apply (case_tac "k = #0") |
301 apply (auto simp add: neq_iff_zless zmult_zless_mono1 zmult_zless_mono1_neg) |
301 apply (auto simp add: neq_iff_zless zmult_zless_mono1 zmult_zless_mono1_neg) |
302 apply (auto simp add: not_zless_iff_zle |
302 apply (auto simp add: not_zless_iff_zle |
303 not_zle_iff_zless [THEN iff_sym, of "m$*k"] |
303 not_zle_iff_zless [THEN iff_sym, of "m$*k"] |
304 not_zle_iff_zless [THEN iff_sym, of m]) |
304 not_zle_iff_zless [THEN iff_sym, of m]) |
305 apply (auto elim: notE |
305 apply (auto elim: notE |
306 simp add: zless_imp_zle zmult_zle_mono1 zmult_zle_mono1_neg) |
306 simp add: zless_imp_zle zmult_zle_mono1 zmult_zle_mono1_neg) |
307 done |
307 done |
308 |
308 |
309 lemma zmult_zless_cancel2: |
309 lemma zmult_zless_cancel2: |
310 "(m$*k $< n$*k) <-> ((#0 $< k & m$<n) | (k $< #0 & n$<m))" |
310 "(m$*k $< n$*k) \<longleftrightarrow> ((#0 $< k & m$<n) | (k $< #0 & n$<m))" |
311 apply (cut_tac k = "intify (k)" and m = "intify (m)" and n = "intify (n)" |
311 apply (cut_tac k = "intify (k)" and m = "intify (m)" and n = "intify (n)" |
312 in zmult_zless_lemma) |
312 in zmult_zless_lemma) |
313 apply auto |
313 apply auto |
314 done |
314 done |
315 |
315 |
316 lemma zmult_zless_cancel1: |
316 lemma zmult_zless_cancel1: |
317 "(k$*m $< k$*n) <-> ((#0 $< k & m$<n) | (k $< #0 & n$<m))" |
317 "(k$*m $< k$*n) \<longleftrightarrow> ((#0 $< k & m$<n) | (k $< #0 & n$<m))" |
318 by (simp add: zmult_commute [of k] zmult_zless_cancel2) |
318 by (simp add: zmult_commute [of k] zmult_zless_cancel2) |
319 |
319 |
320 lemma zmult_zle_cancel2: |
320 lemma zmult_zle_cancel2: |
321 "(m$*k $<= n$*k) <-> ((#0 $< k \<longrightarrow> m$<=n) & (k $< #0 \<longrightarrow> n$<=m))" |
321 "(m$*k $<= n$*k) \<longleftrightarrow> ((#0 $< k \<longrightarrow> m$<=n) & (k $< #0 \<longrightarrow> n$<=m))" |
322 by (auto simp add: not_zless_iff_zle [THEN iff_sym] zmult_zless_cancel2) |
322 by (auto simp add: not_zless_iff_zle [THEN iff_sym] zmult_zless_cancel2) |
323 |
323 |
324 lemma zmult_zle_cancel1: |
324 lemma zmult_zle_cancel1: |
325 "(k$*m $<= k$*n) <-> ((#0 $< k \<longrightarrow> m$<=n) & (k $< #0 \<longrightarrow> n$<=m))" |
325 "(k$*m $<= k$*n) \<longleftrightarrow> ((#0 $< k \<longrightarrow> m$<=n) & (k $< #0 \<longrightarrow> n$<=m))" |
326 by (auto simp add: not_zless_iff_zle [THEN iff_sym] zmult_zless_cancel1) |
326 by (auto simp add: not_zless_iff_zle [THEN iff_sym] zmult_zless_cancel1) |
327 |
327 |
328 lemma int_eq_iff_zle: "[| m \<in> int; n \<in> int |] ==> m=n <-> (m $<= n & n $<= m)" |
328 lemma int_eq_iff_zle: "[| m \<in> int; n \<in> int |] ==> m=n \<longleftrightarrow> (m $<= n & n $<= m)" |
329 apply (blast intro: zle_refl zle_anti_sym) |
329 apply (blast intro: zle_refl zle_anti_sym) |
330 done |
330 done |
331 |
331 |
332 lemma zmult_cancel2_lemma: |
332 lemma zmult_cancel2_lemma: |
333 "[| k \<in> int; m \<in> int; n \<in> int |] ==> (m$*k = n$*k) <-> (k=#0 | m=n)" |
333 "[| k \<in> int; m \<in> int; n \<in> int |] ==> (m$*k = n$*k) \<longleftrightarrow> (k=#0 | m=n)" |
334 apply (simp add: int_eq_iff_zle [of "m$*k"] int_eq_iff_zle [of m]) |
334 apply (simp add: int_eq_iff_zle [of "m$*k"] int_eq_iff_zle [of m]) |
335 apply (auto simp add: zmult_zle_cancel2 neq_iff_zless) |
335 apply (auto simp add: zmult_zle_cancel2 neq_iff_zless) |
336 done |
336 done |
337 |
337 |
338 lemma zmult_cancel2 [simp]: |
338 lemma zmult_cancel2 [simp]: |
339 "(m$*k = n$*k) <-> (intify(k) = #0 | intify(m) = intify(n))" |
339 "(m$*k = n$*k) \<longleftrightarrow> (intify(k) = #0 | intify(m) = intify(n))" |
340 apply (rule iff_trans) |
340 apply (rule iff_trans) |
341 apply (rule_tac [2] zmult_cancel2_lemma) |
341 apply (rule_tac [2] zmult_cancel2_lemma) |
342 apply auto |
342 apply auto |
343 done |
343 done |
344 |
344 |
345 lemma zmult_cancel1 [simp]: |
345 lemma zmult_cancel1 [simp]: |
346 "(k$*m = k$*n) <-> (intify(k) = #0 | intify(m) = intify(n))" |
346 "(k$*m = k$*n) \<longleftrightarrow> (intify(k) = #0 | intify(m) = intify(n))" |
347 by (simp add: zmult_commute [of k] zmult_cancel2) |
347 by (simp add: zmult_commute [of k] zmult_cancel2) |
348 |
348 |
349 |
349 |
350 subsection{* Uniqueness and monotonicity of quotients and remainders *} |
350 subsection{* Uniqueness and monotonicity of quotients and remainders *} |
351 |
351 |
496 apply (drule zmult_pos_neg, assumption) |
496 apply (drule zmult_pos_neg, assumption) |
497 apply (auto dest: zless_not_sym simp add: zmult_commute) |
497 apply (auto dest: zless_not_sym simp add: zmult_commute) |
498 done |
498 done |
499 |
499 |
500 lemma int_0_less_mult_iff: |
500 lemma int_0_less_mult_iff: |
501 "(#0 $< x $* y) <-> (#0 $< x & #0 $< y | x $< #0 & y $< #0)" |
501 "(#0 $< x $* y) \<longleftrightarrow> (#0 $< x & #0 $< y | x $< #0 & y $< #0)" |
502 apply (cut_tac x = "intify (x)" and y = "intify (y)" in int_0_less_lemma) |
502 apply (cut_tac x = "intify (x)" and y = "intify (y)" in int_0_less_lemma) |
503 apply auto |
503 apply auto |
504 done |
504 done |
505 |
505 |
506 lemma int_0_le_lemma: |
506 lemma int_0_le_lemma: |
507 "[| x \<in> int; y \<in> int |] |
507 "[| x \<in> int; y \<in> int |] |
508 ==> (#0 $<= x $* y) <-> (#0 $<= x & #0 $<= y | x $<= #0 & y $<= #0)" |
508 ==> (#0 $<= x $* y) \<longleftrightarrow> (#0 $<= x & #0 $<= y | x $<= #0 & y $<= #0)" |
509 by (auto simp add: zle_def not_zless_iff_zle int_0_less_mult_iff) |
509 by (auto simp add: zle_def not_zless_iff_zle int_0_less_mult_iff) |
510 |
510 |
511 lemma int_0_le_mult_iff: |
511 lemma int_0_le_mult_iff: |
512 "(#0 $<= x $* y) <-> ((#0 $<= x & #0 $<= y) | (x $<= #0 & y $<= #0))" |
512 "(#0 $<= x $* y) \<longleftrightarrow> ((#0 $<= x & #0 $<= y) | (x $<= #0 & y $<= #0))" |
513 apply (cut_tac x = "intify (x)" and y = "intify (y)" in int_0_le_lemma) |
513 apply (cut_tac x = "intify (x)" and y = "intify (y)" in int_0_le_lemma) |
514 apply auto |
514 apply auto |
515 done |
515 done |
516 |
516 |
517 lemma zmult_less_0_iff: |
517 lemma zmult_less_0_iff: |
518 "(x $* y $< #0) <-> (#0 $< x & y $< #0 | x $< #0 & #0 $< y)" |
518 "(x $* y $< #0) \<longleftrightarrow> (#0 $< x & y $< #0 | x $< #0 & #0 $< y)" |
519 apply (auto simp add: int_0_le_mult_iff not_zle_iff_zless [THEN iff_sym]) |
519 apply (auto simp add: int_0_le_mult_iff not_zle_iff_zless [THEN iff_sym]) |
520 apply (auto dest: zless_not_sym simp add: not_zle_iff_zless) |
520 apply (auto dest: zless_not_sym simp add: not_zle_iff_zless) |
521 done |
521 done |
522 |
522 |
523 lemma zmult_le_0_iff: |
523 lemma zmult_le_0_iff: |
524 "(x $* y $<= #0) <-> (#0 $<= x & y $<= #0 | x $<= #0 & #0 $<= y)" |
524 "(x $* y $<= #0) \<longleftrightarrow> (#0 $<= x & y $<= #0 | x $<= #0 & #0 $<= y)" |
525 by (auto dest: zless_not_sym |
525 by (auto dest: zless_not_sym |
526 simp add: int_0_less_mult_iff not_zless_iff_zle [THEN iff_sym]) |
526 simp add: int_0_less_mult_iff not_zless_iff_zle [THEN iff_sym]) |
527 |
527 |
528 |
528 |
529 (*Typechecking for posDivAlg*) |
529 (*Typechecking for posDivAlg*) |
1654 lemma zdiv_nonneg_neg_le0: "[| #0 $<= a; b $< #0 |] ==> a zdiv b $<= #0" |
1654 lemma zdiv_nonneg_neg_le0: "[| #0 $<= a; b $< #0 |] ==> a zdiv b $<= #0" |
1655 apply (drule zdiv_mono1_neg) |
1655 apply (drule zdiv_mono1_neg) |
1656 apply auto |
1656 apply auto |
1657 done |
1657 done |
1658 |
1658 |
1659 lemma pos_imp_zdiv_nonneg_iff: "#0 $< b ==> (#0 $<= a zdiv b) <-> (#0 $<= a)" |
1659 lemma pos_imp_zdiv_nonneg_iff: "#0 $< b ==> (#0 $<= a zdiv b) \<longleftrightarrow> (#0 $<= a)" |
1660 apply auto |
1660 apply auto |
1661 apply (drule_tac [2] zdiv_mono1) |
1661 apply (drule_tac [2] zdiv_mono1) |
1662 apply (auto simp add: neq_iff_zless) |
1662 apply (auto simp add: neq_iff_zless) |
1663 apply (simp (no_asm_use) add: not_zless_iff_zle [THEN iff_sym]) |
1663 apply (simp (no_asm_use) add: not_zless_iff_zle [THEN iff_sym]) |
1664 apply (blast intro: zdiv_neg_pos_less0) |
1664 apply (blast intro: zdiv_neg_pos_less0) |
1665 done |
1665 done |
1666 |
1666 |
1667 lemma neg_imp_zdiv_nonneg_iff: "b $< #0 ==> (#0 $<= a zdiv b) <-> (a $<= #0)" |
1667 lemma neg_imp_zdiv_nonneg_iff: "b $< #0 ==> (#0 $<= a zdiv b) \<longleftrightarrow> (a $<= #0)" |
1668 apply (subst zdiv_zminus_zminus [symmetric]) |
1668 apply (subst zdiv_zminus_zminus [symmetric]) |
1669 apply (rule iff_trans) |
1669 apply (rule iff_trans) |
1670 apply (rule pos_imp_zdiv_nonneg_iff) |
1670 apply (rule pos_imp_zdiv_nonneg_iff) |
1671 apply auto |
1671 apply auto |
1672 done |
1672 done |
1673 |
1673 |
1674 (*But not (a zdiv b $<= 0 iff a$<=0); consider a=1, b=2 when a zdiv b = 0.*) |
1674 (*But not (a zdiv b $<= 0 iff a$<=0); consider a=1, b=2 when a zdiv b = 0.*) |
1675 lemma pos_imp_zdiv_neg_iff: "#0 $< b ==> (a zdiv b $< #0) <-> (a $< #0)" |
1675 lemma pos_imp_zdiv_neg_iff: "#0 $< b ==> (a zdiv b $< #0) \<longleftrightarrow> (a $< #0)" |
1676 apply (simp (no_asm_simp) add: not_zle_iff_zless [THEN iff_sym]) |
1676 apply (simp (no_asm_simp) add: not_zle_iff_zless [THEN iff_sym]) |
1677 apply (erule pos_imp_zdiv_nonneg_iff) |
1677 apply (erule pos_imp_zdiv_nonneg_iff) |
1678 done |
1678 done |
1679 |
1679 |
1680 (*Again the law fails for $<=: consider a = -1, b = -2 when a zdiv b = 0*) |
1680 (*Again the law fails for $<=: consider a = -1, b = -2 when a zdiv b = 0*) |
1681 lemma neg_imp_zdiv_neg_iff: "b $< #0 ==> (a zdiv b $< #0) <-> (#0 $< a)" |
1681 lemma neg_imp_zdiv_neg_iff: "b $< #0 ==> (a zdiv b $< #0) \<longleftrightarrow> (#0 $< a)" |
1682 apply (simp (no_asm_simp) add: not_zle_iff_zless [THEN iff_sym]) |
1682 apply (simp (no_asm_simp) add: not_zle_iff_zless [THEN iff_sym]) |
1683 apply (erule neg_imp_zdiv_nonneg_iff) |
1683 apply (erule neg_imp_zdiv_nonneg_iff) |
1684 done |
1684 done |
1685 |
1685 |
1686 (* |
1686 (* |