234 (** Lemmas **) |
218 (** Lemmas **) |
235 |
219 |
236 lemma zadd_assoc_cong: "(z::int) + v = z' + v' ==> z + (v + w) = z' + (v' + w)" |
220 lemma zadd_assoc_cong: "(z::int) + v = z' + v' ==> z + (v + w) = z' + (v' + w)" |
237 by (simp add: zadd_assoc [symmetric]) |
221 by (simp add: zadd_assoc [symmetric]) |
238 |
222 |
239 lemma zadd_assoc_swap: "(z::int) + (v + w) = v + (z + w)" |
|
240 by (rule zadd_commute [THEN zadd_assoc_cong]) |
|
241 |
|
242 |
223 |
243 subsection{*zmult: multiplication on Integ*} |
224 subsection{*zmult: multiplication on Integ*} |
244 |
225 |
245 (*Congruence property for multiplication*) |
226 text{*Congruence property for multiplication*} |
246 lemma zmult_congruent2: "congruent2 intrel |
227 lemma zmult_congruent2: "congruent2 intrel |
247 (%p1 p2. (%(x1,y1). (%(x2,y2). |
228 (%p1 p2. (%(x1,y1). (%(x2,y2). |
248 intrel``{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)" |
229 intrel``{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)" |
249 apply (rule equiv_intrel [THEN congruent2_commuteI]) |
230 apply (rule equiv_intrel [THEN congruent2_commuteI]) |
250 apply (rule_tac [2] p=w in PairE) |
231 apply (force simp add: add_ac mult_ac) |
251 apply (force simp add: add_ac mult_ac, clarify) |
232 apply (clarify, simp del: equiv_intrel_iff add: add_ac mult_ac) |
252 apply (simp (no_asm_simp) del: equiv_intrel_iff add: add_ac mult_ac) |
|
253 apply (rename_tac x1 x2 y1 y2 z1 z2) |
233 apply (rename_tac x1 x2 y1 y2 z1 z2) |
254 apply (rule equiv_class_eq [OF equiv_intrel intrel_iff [THEN iffD2]]) |
234 apply (rule equiv_class_eq [OF equiv_intrel intrel_iff [THEN iffD2]]) |
255 apply (simp add: intrel_def) |
235 apply (subgoal_tac "x1*z1 + y2*z1 = y1*z1 + x2*z1 & x1*z2 + y2*z2 = y1*z2 + x2*z2") |
256 apply (subgoal_tac "x1*z1 + y2*z1 = y1*z1 + x2*z1 & x1*z2 + y2*z2 = y1*z2 + x2*z2", arith) |
236 apply (simp add: mult_ac, arith) |
257 apply (simp add: add_mult_distrib [symmetric]) |
237 apply (simp add: add_mult_distrib [symmetric]) |
258 done |
238 done |
259 |
239 |
260 lemma zmult: |
240 lemma zmult: |
261 "Abs_Integ((intrel``{(x1,y1)})) * Abs_Integ((intrel``{(x2,y2)})) = |
241 "Abs_Integ((intrel``{(x1,y1)})) * Abs_Integ((intrel``{(x2,y2)})) = |
262 Abs_Integ(intrel `` {(x1*x2 + y1*y2, x1*y2 + y1*x2)})" |
242 Abs_Integ(intrel `` {(x1*x2 + y1*y2, x1*y2 + y1*x2)})" |
263 apply (unfold zmult_def) |
243 by (simp add: zmult_def UN_UN_split_split_eq zmult_congruent2 |
264 apply (simp (no_asm_simp) add: UN_UN_split_split_eq zmult_congruent2 equiv_intrel [THEN UN_equiv_class2]) |
244 equiv_intrel [THEN UN_equiv_class2]) |
265 done |
|
266 |
245 |
267 lemma zmult_zminus: "(- z) * w = - (z * (w::int))" |
246 lemma zmult_zminus: "(- z) * w = - (z * (w::int))" |
268 apply (rule_tac z = z in eq_Abs_Integ) |
247 apply (rule eq_Abs_Integ [of z]) |
269 apply (rule_tac z = w in eq_Abs_Integ) |
248 apply (rule eq_Abs_Integ [of w]) |
270 apply (simp (no_asm_simp) add: zminus zmult add_ac) |
249 apply (simp add: zminus zmult add_ac) |
271 done |
250 done |
272 |
251 |
273 lemma zmult_commute: "(z::int) * w = w * z" |
252 lemma zmult_commute: "(z::int) * w = w * z" |
274 apply (rule_tac z = z in eq_Abs_Integ) |
253 apply (rule eq_Abs_Integ [of z]) |
275 apply (rule_tac z = w in eq_Abs_Integ) |
254 apply (rule eq_Abs_Integ [of w]) |
276 apply (simp (no_asm_simp) add: zmult add_ac mult_ac) |
255 apply (simp add: zmult add_ac mult_ac) |
277 done |
256 done |
278 |
257 |
279 lemma zmult_assoc: "((z1::int) * z2) * z3 = z1 * (z2 * z3)" |
258 lemma zmult_assoc: "((z1::int) * z2) * z3 = z1 * (z2 * z3)" |
280 apply (rule_tac z = z1 in eq_Abs_Integ) |
259 apply (rule eq_Abs_Integ [of z1]) |
281 apply (rule_tac z = z2 in eq_Abs_Integ) |
260 apply (rule eq_Abs_Integ [of z2]) |
282 apply (rule_tac z = z3 in eq_Abs_Integ) |
261 apply (rule eq_Abs_Integ [of z3]) |
283 apply (simp (no_asm_simp) add: add_mult_distrib2 zmult add_ac mult_ac) |
262 apply (simp add: add_mult_distrib2 zmult add_ac mult_ac) |
284 done |
263 done |
285 |
264 |
286 lemma zadd_zmult_distrib: "((z1::int) + z2) * w = (z1 * w) + (z2 * w)" |
265 lemma zadd_zmult_distrib: "((z1::int) + z2) * w = (z1 * w) + (z2 * w)" |
287 apply (rule_tac z = z1 in eq_Abs_Integ) |
266 apply (rule eq_Abs_Integ [of z1]) |
288 apply (rule_tac z = z2 in eq_Abs_Integ) |
267 apply (rule eq_Abs_Integ [of z2]) |
289 apply (rule_tac z = w in eq_Abs_Integ) |
268 apply (rule eq_Abs_Integ [of w]) |
290 apply (simp add: add_mult_distrib2 zadd zmult add_ac mult_ac) |
269 apply (simp add: add_mult_distrib2 zadd zmult add_ac mult_ac) |
291 done |
270 done |
292 |
271 |
293 lemma zmult_zminus_right: "w * (- z) = - (w * (z::int))" |
272 lemma zmult_zminus_right: "w * (- z) = - (w * (z::int))" |
294 by (simp add: zmult_commute [of w] zmult_zminus) |
273 by (simp add: zmult_commute [of w] zmult_zminus) |
350 hence "(-k + k) + i = (-k + k) + j" by (simp only: eq zadd_assoc) |
329 hence "(-k + k) + i = (-k + k) + j" by (simp only: eq zadd_assoc) |
351 thus "i = j" by simp |
330 thus "i = j" by simp |
352 qed |
331 qed |
353 |
332 |
354 |
333 |
355 subsection{*Theorems about the Ordering*} |
334 subsection{*The @{text "\<le>"} Ordering*} |
|
335 |
|
336 lemma zle: |
|
337 "(Abs_Integ(intrel``{(x1,y1)}) \<le> Abs_Integ(intrel``{(x2,y2)})) = |
|
338 (x1 + y2 \<le> x2 + y1)" |
|
339 by (force simp add: zle_def) |
|
340 |
|
341 lemma zle_refl: "w \<le> (w::int)" |
|
342 apply (rule eq_Abs_Integ [of w]) |
|
343 apply (force simp add: zle) |
|
344 done |
|
345 |
|
346 lemma zle_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::int)" |
|
347 apply (rule eq_Abs_Integ [of i]) |
|
348 apply (rule eq_Abs_Integ [of j]) |
|
349 apply (rule eq_Abs_Integ [of k]) |
|
350 apply (simp add: zle) |
|
351 done |
|
352 |
|
353 lemma zle_anti_sym: "[| z \<le> w; w \<le> z |] ==> z = (w::int)" |
|
354 apply (rule eq_Abs_Integ [of w]) |
|
355 apply (rule eq_Abs_Integ [of z]) |
|
356 apply (simp add: zle) |
|
357 done |
|
358 |
|
359 (* Axiom 'order_less_le' of class 'order': *) |
|
360 lemma zless_le: "((w::int) < z) = (w \<le> z & w \<noteq> z)" |
|
361 by (simp add: zless_def) |
|
362 |
|
363 instance int :: order |
|
364 proof qed |
|
365 (assumption | |
|
366 rule zle_refl zle_trans zle_anti_sym zless_le)+ |
|
367 |
|
368 (* Axiom 'linorder_linear' of class 'linorder': *) |
|
369 lemma zle_linear: "(z::int) \<le> w | w \<le> z" |
|
370 apply (rule eq_Abs_Integ [of z]) |
|
371 apply (rule eq_Abs_Integ [of w]) |
|
372 apply (simp add: zle linorder_linear) |
|
373 done |
|
374 |
|
375 instance int :: plus_ac0 |
|
376 proof qed (rule zadd_commute zadd_assoc zadd_0)+ |
|
377 |
|
378 instance int :: linorder |
|
379 proof qed (rule zle_linear) |
|
380 |
|
381 |
|
382 lemmas zless_linear = linorder_less_linear [where 'a = int] |
|
383 |
|
384 |
|
385 lemma int_eq_0_conv [simp]: "(int n = 0) = (n = 0)" |
|
386 by (simp add: Zero_int_def) |
356 |
387 |
357 (*This lemma allows direct proofs of other <-properties*) |
388 (*This lemma allows direct proofs of other <-properties*) |
358 lemma zless_iff_Suc_zadd: |
389 lemma zless_iff_Suc_zadd: |
359 "(w < z) = (\<exists>n. z = w + int(Suc n))" |
390 "(w < z) = (\<exists>n. z = w + int(Suc n))" |
360 apply (unfold zless_def neg_def zdiff_def int_def) |
391 apply (rule eq_Abs_Integ [of z]) |
361 apply (rule_tac z = z in eq_Abs_Integ) |
392 apply (rule eq_Abs_Integ [of w]) |
362 apply (rule_tac z = w in eq_Abs_Integ, clarify) |
393 apply (simp add: linorder_not_le [where 'a = int, symmetric] |
363 apply (simp add: zadd zminus) |
394 linorder_not_le [where 'a = nat] |
|
395 zle int_def zdiff_def zadd zminus) |
364 apply (safe dest!: less_imp_Suc_add) |
396 apply (safe dest!: less_imp_Suc_add) |
365 apply (rule_tac x = k in exI) |
397 apply (rule_tac x = k in exI) |
366 apply (simp_all add: add_ac) |
398 apply (simp_all add: add_ac) |
367 done |
399 done |
368 |
400 |
369 lemma zless_zadd_Suc: "z < z + int (Suc n)" |
|
370 by (auto simp add: zless_iff_Suc_zadd zadd_assoc zadd_int) |
|
371 |
|
372 lemma zless_trans: "[| z1<z2; z2<z3 |] ==> z1 < (z3::int)" |
|
373 by (auto simp add: zless_iff_Suc_zadd zadd_assoc zadd_int) |
|
374 |
|
375 lemma zless_not_sym: "!!w::int. z<w ==> ~w<z" |
|
376 apply (safe dest!: zless_iff_Suc_zadd [THEN iffD1]) |
|
377 apply (rule_tac z = z in eq_Abs_Integ, safe) |
|
378 apply (simp add: int_def zadd) |
|
379 done |
|
380 |
|
381 (* [| n<m; ~P ==> m<n |] ==> P *) |
|
382 lemmas zless_asym = zless_not_sym [THEN swap, standard] |
|
383 |
|
384 lemma zless_not_refl: "!!z::int. ~ z<z" |
|
385 apply (rule zless_asym [THEN notI]) |
|
386 apply (assumption+) |
|
387 done |
|
388 |
|
389 (* z<z ==> R *) |
|
390 lemmas zless_irrefl = zless_not_refl [THEN notE, standard, elim!] |
|
391 |
|
392 |
|
393 (*"Less than" is a linear ordering*) |
|
394 lemma zless_linear: |
|
395 "z<w | z=w | w<(z::int)" |
|
396 apply (unfold zless_def neg_def zdiff_def) |
|
397 apply (rule_tac z = z in eq_Abs_Integ) |
|
398 apply (rule_tac z = w in eq_Abs_Integ, safe) |
|
399 apply (simp add: zadd zminus Image_iff Bex_def) |
|
400 apply (rule_tac m1 = "x+ya" and n1 = "xa+y" in less_linear [THEN disjE]) |
|
401 apply (force simp add: add_ac)+ |
|
402 done |
|
403 |
|
404 lemma int_neq_iff: "!!w::int. (w ~= z) = (w<z | z<w)" |
|
405 by (cut_tac zless_linear, blast) |
|
406 |
|
407 (*** eliminates ~= in premises ***) |
|
408 lemmas int_neqE = int_neq_iff [THEN iffD1, THEN disjE, standard] |
|
409 |
|
410 lemma int_eq_0_conv [simp]: "(int n = 0) = (n = 0)" |
|
411 by (simp add: Zero_int_def) |
|
412 |
|
413 lemma zless_int [simp]: "(int m < int n) = (m<n)" |
401 lemma zless_int [simp]: "(int m < int n) = (m<n)" |
414 by (simp add: less_iff_Suc_add zless_iff_Suc_zadd zadd_int) |
402 by (simp add: less_iff_Suc_add zless_iff_Suc_zadd zadd_int) |
415 |
403 |
416 lemma int_less_0_conv [simp]: "~ (int k < 0)" |
404 lemma int_less_0_conv [simp]: "~ (int k < 0)" |
417 by (simp add: Zero_int_def) |
405 by (simp add: Zero_int_def) |
423 by (simp only: Zero_int_def One_int_def One_nat_def zless_int) |
411 by (simp only: Zero_int_def One_int_def One_nat_def zless_int) |
424 |
412 |
425 lemma int_0_neq_1 [simp]: "0 \<noteq> (1::int)" |
413 lemma int_0_neq_1 [simp]: "0 \<noteq> (1::int)" |
426 by (simp only: Zero_int_def One_int_def One_nat_def int_int_eq) |
414 by (simp only: Zero_int_def One_int_def One_nat_def int_int_eq) |
427 |
415 |
428 |
416 lemma zle_int [simp]: "(int m \<le> int n) = (m\<le>n)" |
429 subsection{*Properties of the @{text "\<le>"} Relation*} |
417 by (simp add: linorder_not_less [symmetric]) |
430 |
418 |
431 lemma zle_int [simp]: "(int m <= int n) = (m<=n)" |
419 lemma zero_zle_int [simp]: "(0 \<le> int n)" |
432 by (simp add: zle_def le_def) |
|
433 |
|
434 lemma zero_zle_int [simp]: "(0 <= int n)" |
|
435 by (simp add: Zero_int_def) |
420 by (simp add: Zero_int_def) |
436 |
421 |
437 lemma int_le_0_conv [simp]: "(int n <= 0) = (n = 0)" |
422 lemma int_le_0_conv [simp]: "(int n \<le> 0) = (n = 0)" |
438 by (simp add: Zero_int_def) |
423 by (simp add: Zero_int_def) |
439 |
424 |
440 lemma zle_imp_zless_or_eq: "z <= w ==> z < w | z=(w::int)" |
425 lemma int_0 [simp]: "int 0 = (0::int)" |
441 apply (unfold zle_def) |
426 by (simp add: Zero_int_def) |
442 apply (cut_tac zless_linear) |
427 |
443 apply (blast elim: zless_asym) |
428 lemma int_1 [simp]: "int 1 = 1" |
444 done |
429 by (simp add: One_int_def) |
445 |
430 |
446 lemma zless_or_eq_imp_zle: "z<w | z=w ==> z <= (w::int)" |
431 lemma int_Suc0_eq_1: "int (Suc 0) = 1" |
447 apply (unfold zle_def) |
432 by (simp add: One_int_def One_nat_def) |
448 apply (cut_tac zless_linear) |
433 |
449 apply (blast elim: zless_asym) |
434 subsection{*Monotonicity results*} |
450 done |
435 |
451 |
436 lemma zadd_left_mono: "i \<le> j ==> k + i \<le> k + (j::int)" |
452 lemma int_le_less: "(x <= (y::int)) = (x < y | x=y)" |
437 apply (rule eq_Abs_Integ [of i]) |
453 apply (rule iffI) |
438 apply (rule eq_Abs_Integ [of j]) |
454 apply (erule zle_imp_zless_or_eq) |
439 apply (rule eq_Abs_Integ [of k]) |
455 apply (erule zless_or_eq_imp_zle) |
440 apply (simp add: zle zadd) |
456 done |
441 done |
457 |
442 |
458 lemma zle_refl: "w <= (w::int)" |
443 lemma zadd_strict_right_mono: "i < j ==> i + k < j + (k::int)" |
459 by (simp add: int_le_less) |
444 apply (rule eq_Abs_Integ [of i]) |
460 |
445 apply (rule eq_Abs_Integ [of j]) |
461 (* Axiom 'linorder_linear' of class 'linorder': *) |
446 apply (rule eq_Abs_Integ [of k]) |
462 lemma zle_linear: "(z::int) <= w | w <= z" |
447 apply (simp add: linorder_not_le [where 'a = int, symmetric] |
463 apply (simp add: int_le_less) |
448 linorder_not_le [where 'a = nat] zle zadd) |
464 apply (cut_tac zless_linear, blast) |
449 done |
465 done |
450 |
466 |
451 lemma zadd_zless_mono: "[| w'<w; z'\<le>z |] ==> w' + z' < w + (z::int)" |
467 (* Axiom 'order_trans of class 'order': *) |
452 by (rule order_less_le_trans [OF zadd_strict_right_mono zadd_left_mono]) |
468 lemma zle_trans: "[| i <= j; j <= k |] ==> i <= (k::int)" |
453 |
469 apply (drule zle_imp_zless_or_eq) |
454 |
470 apply (drule zle_imp_zless_or_eq) |
455 subsection{*Strict Monotonicity of Multiplication*} |
471 apply (rule zless_or_eq_imp_zle) |
456 |
472 apply (blast intro: zless_trans) |
457 text{*strict, in 1st argument; proof is by induction on k>0*} |
473 done |
458 lemma zmult_zless_mono2_lemma [rule_format]: |
474 |
459 "i<j ==> 0<k --> int k * i < int k * j" |
475 lemma zle_anti_sym: "[| z <= w; w <= z |] ==> z = (w::int)" |
460 apply (induct_tac "k", simp) |
476 apply (drule zle_imp_zless_or_eq) |
461 apply (simp add: int_Suc) |
477 apply (drule zle_imp_zless_or_eq) |
462 apply (case_tac "n=0") |
478 apply (blast elim: zless_asym) |
463 apply (simp_all add: zadd_zmult_distrib int_Suc0_eq_1 order_le_less) |
479 done |
464 apply (simp add: zadd_zless_mono int_Suc0_eq_1 order_le_less) |
480 |
465 done |
481 (* Axiom 'order_less_le' of class 'order': *) |
466 |
482 lemma int_less_le: "((w::int) < z) = (w <= z & w ~= z)" |
467 lemma zero_le_imp_eq_int: "0 \<le> k ==> \<exists>n. k = int n" |
483 apply (simp add: zle_def int_neq_iff) |
468 apply (rule eq_Abs_Integ [of k]) |
484 apply (blast elim!: zless_asym) |
469 apply (auto simp add: zle zadd int_def Zero_int_def) |
485 done |
470 apply (rule_tac x="x-y" in exI, simp) |
486 |
471 done |
487 instance int :: order |
472 |
488 proof qed (assumption | rule zle_refl zle_trans zle_anti_sym int_less_le)+ |
473 lemma zmult_zless_mono2: "[| i<j; (0::int) < k |] ==> k*i < k*j" |
489 |
474 apply (frule order_less_imp_le [THEN zero_le_imp_eq_int]) |
490 instance int :: plus_ac0 |
475 apply (auto simp add: zmult_zless_mono2_lemma) |
491 proof qed (rule zadd_commute zadd_assoc zadd_0)+ |
476 done |
492 |
477 |
493 instance int :: linorder |
478 |
494 proof qed (rule zle_linear) |
479 defs (overloaded) |
495 |
480 zabs_def: "abs(i::int) == if i < 0 then -i else i" |
496 |
481 |
497 lemma zadd_left_cancel [simp]: "!!w::int. (z + w' = z + w) = (w' = w)" |
482 |
498 by (rule add_left_cancel) |
483 text{*The Integers Form an Ordered Ring*} |
499 |
484 instance int :: ordered_ring |
500 |
485 proof |
|
486 fix i j k :: int |
|
487 show "0 < (1::int)" by (rule int_0_less_1) |
|
488 show "i \<le> j ==> k + i \<le> k + j" by (rule zadd_left_mono) |
|
489 show "i < j ==> 0 < k ==> k * i < k * j" by (rule zmult_zless_mono2) |
|
490 show "\<bar>i\<bar> = (if i < 0 then -i else i)" by (simp only: zabs_def) |
|
491 qed |
|
492 |
|
493 |
|
494 subsection{*Magnitide of an Integer, as a Natural Number: @{term nat}*} |
|
495 |
|
496 constdefs |
|
497 nat :: "int => nat" |
|
498 "nat(Z) == if Z<0 then 0 else (THE m. Z = int m)" |
|
499 |
|
500 lemma nat_int [simp]: "nat(int n) = n" |
|
501 by (unfold nat_def, auto) |
|
502 |
|
503 lemma nat_zero [simp]: "nat 0 = 0" |
|
504 apply (unfold Zero_int_def) |
|
505 apply (rule nat_int) |
|
506 done |
|
507 |
|
508 lemma nat_0_le [simp]: "0 \<le> z ==> int (nat z) = z" |
|
509 apply (rule eq_Abs_Integ [of z]) |
|
510 apply (simp add: nat_def linorder_not_le [symmetric] zle int_def Zero_int_def) |
|
511 apply (subgoal_tac "(THE m. x = m + y) = x-y") |
|
512 apply (auto simp add: the_equality) |
|
513 done |
|
514 |
|
515 lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0" |
|
516 by (simp add: nat_def order_less_le eq_commute [of 0]) |
|
517 |
|
518 text{*An alternative condition is @{term "0 \<le> w"} *} |
|
519 lemma nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)" |
|
520 apply (subst zless_int [symmetric]) |
|
521 apply (simp add: order_le_less) |
|
522 apply (case_tac "w < 0") |
|
523 apply (simp add: order_less_imp_le) |
|
524 apply (blast intro: order_less_trans) |
|
525 apply (simp add: linorder_not_less) |
|
526 done |
|
527 |
|
528 lemma zless_nat_conj: "(nat w < nat z) = (0 < z & w < z)" |
|
529 apply (case_tac "0 < z") |
|
530 apply (auto simp add: nat_mono_iff linorder_not_less) |
|
531 done |
|
532 |
|
533 |
|
534 subsection{*Lemmas about the Function @{term int} and Orderings*} |
|
535 |
|
536 lemma negative_zless_0: "- (int (Suc n)) < 0" |
|
537 by (simp add: zless_def) |
|
538 |
|
539 lemma negative_zless [iff]: "- (int (Suc n)) < int m" |
|
540 by (rule negative_zless_0 [THEN order_less_le_trans], simp) |
|
541 |
|
542 lemma negative_zle_0: "- int n \<le> 0" |
|
543 by (simp add: minus_le_iff) |
|
544 |
|
545 lemma negative_zle [iff]: "- int n \<le> int m" |
|
546 by (rule order_trans [OF negative_zle_0 zero_zle_int]) |
|
547 |
|
548 lemma not_zle_0_negative [simp]: "~ (0 \<le> - (int (Suc n)))" |
|
549 by (subst le_minus_iff, simp) |
|
550 |
|
551 lemma int_zle_neg: "(int n \<le> - int m) = (n = 0 & m = 0)" |
|
552 apply safe |
|
553 apply (drule_tac [2] le_minus_iff [THEN iffD1]) |
|
554 apply (auto dest: zle_trans [OF _ negative_zle_0]) |
|
555 done |
|
556 |
|
557 lemma not_int_zless_negative [simp]: "~ (int n < - int m)" |
|
558 by (simp add: linorder_not_less) |
|
559 |
|
560 lemma negative_eq_positive [simp]: "(- int n = int m) = (n = 0 & m = 0)" |
|
561 by (force simp add: order_eq_iff [of "- int n"] int_zle_neg) |
|
562 |
|
563 lemma zle_iff_zadd: "(w \<le> z) = (\<exists>n. z = w + int n)" |
|
564 by (force intro: exI [of _ "0::nat"] |
|
565 intro!: not_sym [THEN not0_implies_Suc] |
|
566 simp add: zless_iff_Suc_zadd order_le_less) |
|
567 |
|
568 |
|
569 text{*This version is proved for all ordered rings, not just integers! |
|
570 It is proved here because attribute @{text arith_split} is not available |
|
571 in theory @{text Ring_and_Field}. |
|
572 But is it really better than just rewriting with @{text abs_if}?*} |
|
573 lemma abs_split [arith_split]: |
|
574 "P(abs(a::'a::ordered_ring)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))" |
|
575 by (force dest: order_less_le_trans simp add: abs_if linorder_not_less) |
|
576 |
|
577 lemma abs_int_eq [simp]: "abs (int m) = int m" |
|
578 by (simp add: zabs_def) |
|
579 |
|
580 |
|
581 subsection{*Misc Results*} |
|
582 |
|
583 lemma nat_zminus_int [simp]: "nat(- (int n)) = 0" |
|
584 by (auto simp add: nat_def zero_reorient minus_less_iff) |
|
585 |
|
586 lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)" |
|
587 apply (case_tac "0 \<le> z") |
|
588 apply (erule nat_0_le [THEN subst], simp) |
|
589 apply (simp add: linorder_not_le) |
|
590 apply (auto dest: order_less_trans simp add: order_less_imp_le) |
|
591 done |
|
592 |
|
593 |
|
594 |
|
595 subsection{*Monotonicity of Multiplication*} |
|
596 |
|
597 lemma zmult_zle_mono2: "[| i \<le> j; (0::int) \<le> k |] ==> k*i \<le> k*j" |
|
598 by (rule Ring_and_Field.mult_left_mono) |
|
599 |
|
600 lemma zmult_zless_cancel2: "(m*k < n*k) = (((0::int) < k & m<n) | (k<0 & n<m))" |
|
601 by (rule Ring_and_Field.mult_less_cancel_right) |
|
602 |
|
603 lemma zmult_zless_cancel1: |
|
604 "(k*m < k*n) = (((0::int) < k & m<n) | (k < 0 & n<m))" |
|
605 by (rule Ring_and_Field.mult_less_cancel_left) |
|
606 |
|
607 lemma zmult_zle_cancel1: |
|
608 "(k*m \<le> k*n) = (((0::int) < k --> m\<le>n) & (k < 0 --> n\<le>m))" |
|
609 by (rule Ring_and_Field.mult_le_cancel_left) |
|
610 |
|
611 |
|
612 |
|
613 text{*A case theorem distinguishing non-negative and negative int*} |
|
614 |
|
615 lemma negD: "x<0 ==> \<exists>n. x = - (int (Suc n))" |
|
616 by (auto simp add: zless_iff_Suc_zadd |
|
617 diff_eq_eq [symmetric] zdiff_def) |
|
618 |
|
619 lemma int_cases [cases type: int, case_names nonneg neg]: |
|
620 "[|!! n. z = int n ==> P; !! n. z = - (int (Suc n)) ==> P |] ==> P" |
|
621 apply (case_tac "z < 0", blast dest!: negD) |
|
622 apply (simp add: linorder_not_less) |
|
623 apply (blast dest: nat_0_le [THEN sym]) |
|
624 done |
|
625 |
|
626 lemma int_induct [induct type: int, case_names nonneg neg]: |
|
627 "[|!! n. P (int n); !!n. P (- (int (Suc n))) |] ==> P z" |
|
628 by (cases z) auto |
|
629 |
|
630 |
|
631 subsection{*The Constants @{term neg} and @{term iszero}*} |
|
632 |
|
633 constdefs |
|
634 |
|
635 neg :: "'a::ordered_ring => bool" |
|
636 "neg(Z) == Z < 0" |
|
637 |
|
638 (*For simplifying equalities*) |
|
639 iszero :: "'a::semiring => bool" |
|
640 "iszero z == z = (0)" |
|
641 |
|
642 |
|
643 lemma not_neg_int [simp]: "~ neg(int n)" |
|
644 by (simp add: neg_def) |
|
645 |
|
646 lemma neg_zminus_int [simp]: "neg(- (int (Suc n)))" |
|
647 by (simp add: neg_def neg_less_0_iff_less) |
|
648 |
|
649 lemmas neg_eq_less_0 = neg_def |
|
650 |
|
651 lemma not_neg_eq_ge_0: "(~neg x) = (0 \<le> x)" |
|
652 by (simp add: neg_def linorder_not_less) |
|
653 |
|
654 subsection{*To simplify inequalities when Numeral1 can get simplified to 1*} |
|
655 |
|
656 lemma not_neg_0: "~ neg 0" |
|
657 by (simp add: One_int_def neg_def) |
|
658 |
|
659 lemma not_neg_1: "~ neg 1" |
|
660 by (simp add: neg_def linorder_not_less zero_le_one) |
|
661 |
|
662 lemma iszero_0: "iszero 0" |
|
663 by (simp add: iszero_def) |
|
664 |
|
665 lemma not_iszero_1: "~ iszero 1" |
|
666 by (simp add: iszero_def eq_commute) |
|
667 |
|
668 lemma neg_nat: "neg z ==> nat z = 0" |
|
669 by (simp add: nat_def neg_def) |
|
670 |
|
671 lemma not_neg_nat: "~ neg z ==> int (nat z) = z" |
|
672 by (simp add: linorder_not_less neg_def) |
|
673 |
|
674 |
|
675 subsection{*Embedding of the Naturals into any Semiring: @{term of_nat}*} |
|
676 |
|
677 consts of_nat :: "nat => 'a::semiring" |
|
678 |
|
679 primrec |
|
680 of_nat_0: "of_nat 0 = 0" |
|
681 of_nat_Suc: "of_nat (Suc m) = of_nat m + 1" |
|
682 |
|
683 lemma of_nat_1 [simp]: "of_nat 1 = 1" |
|
684 by simp |
|
685 |
|
686 lemma of_nat_add [simp]: "of_nat (m+n) = of_nat m + of_nat n" |
|
687 apply (induct m) |
|
688 apply (simp_all add: add_ac) |
|
689 done |
|
690 |
|
691 lemma of_nat_mult [simp]: "of_nat (m*n) = of_nat m * of_nat n" |
|
692 apply (induct m) |
|
693 apply (simp_all add: mult_ac add_ac right_distrib) |
|
694 done |
|
695 |
|
696 lemma zero_le_imp_of_nat: "0 \<le> (of_nat m::'a::ordered_semiring)" |
|
697 apply (induct m, simp_all) |
|
698 apply (erule order_trans) |
|
699 apply (rule less_add_one [THEN order_less_imp_le]) |
|
700 done |
|
701 |
|
702 lemma less_imp_of_nat_less: |
|
703 "m < n ==> of_nat m < (of_nat n::'a::ordered_semiring)" |
|
704 apply (induct m n rule: diff_induct, simp_all) |
|
705 apply (insert add_le_less_mono [OF zero_le_imp_of_nat zero_less_one], force) |
|
706 done |
|
707 |
|
708 lemma of_nat_less_imp_less: |
|
709 "of_nat m < (of_nat n::'a::ordered_semiring) ==> m < n" |
|
710 apply (induct m n rule: diff_induct, simp_all) |
|
711 apply (insert zero_le_imp_of_nat) |
|
712 apply (force simp add: linorder_not_less [symmetric]) |
|
713 done |
|
714 |
|
715 lemma of_nat_less_iff [simp]: |
|
716 "(of_nat m < (of_nat n::'a::ordered_semiring)) = (m<n)" |
|
717 by (blast intro: of_nat_less_imp_less less_imp_of_nat_less ) |
|
718 |
|
719 text{*Special cases where either operand is zero*} |
|
720 declare of_nat_less_iff [of 0, simplified, simp] |
|
721 declare of_nat_less_iff [of _ 0, simplified, simp] |
|
722 |
|
723 lemma of_nat_le_iff [simp]: |
|
724 "(of_nat m \<le> (of_nat n::'a::ordered_semiring)) = (m \<le> n)" |
|
725 by (simp add: linorder_not_less [symmetric]) |
|
726 |
|
727 text{*Special cases where either operand is zero*} |
|
728 declare of_nat_le_iff [of 0, simplified, simp] |
|
729 declare of_nat_le_iff [of _ 0, simplified, simp] |
|
730 |
|
731 lemma of_nat_eq_iff [simp]: |
|
732 "(of_nat m = (of_nat n::'a::ordered_semiring)) = (m = n)" |
|
733 by (simp add: order_eq_iff) |
|
734 |
|
735 text{*Special cases where either operand is zero*} |
|
736 declare of_nat_eq_iff [of 0, simplified, simp] |
|
737 declare of_nat_eq_iff [of _ 0, simplified, simp] |
|
738 |
|
739 lemma of_nat_diff [simp]: |
|
740 "n \<le> m ==> of_nat (m - n) = of_nat m - (of_nat n :: 'a::ring)" |
|
741 by (simp del: of_nat_add |
|
742 add: compare_rls of_nat_add [symmetric] split add: nat_diff_split) |
|
743 |
|
744 |
|
745 subsection{*The Set of Natural Numbers*} |
|
746 |
|
747 constdefs |
|
748 Nats :: "'a::semiring set" |
|
749 "Nats == range of_nat" |
|
750 |
|
751 syntax (xsymbols) Nats :: "'a set" ("\<nat>") |
|
752 |
|
753 lemma of_nat_in_Nats [simp]: "of_nat n \<in> Nats" |
|
754 by (simp add: Nats_def) |
|
755 |
|
756 lemma Nats_0 [simp]: "0 \<in> Nats" |
|
757 apply (simp add: Nats_def) |
|
758 apply (rule range_eqI) |
|
759 apply (rule of_nat_0 [symmetric]) |
|
760 done |
|
761 |
|
762 lemma Nats_1 [simp]: "1 \<in> Nats" |
|
763 apply (simp add: Nats_def) |
|
764 apply (rule range_eqI) |
|
765 apply (rule of_nat_1 [symmetric]) |
|
766 done |
|
767 |
|
768 lemma Nats_add [simp]: "[|a \<in> Nats; b \<in> Nats|] ==> a+b \<in> Nats" |
|
769 apply (auto simp add: Nats_def) |
|
770 apply (rule range_eqI) |
|
771 apply (rule of_nat_add [symmetric]) |
|
772 done |
|
773 |
|
774 lemma Nats_mult [simp]: "[|a \<in> Nats; b \<in> Nats|] ==> a*b \<in> Nats" |
|
775 apply (auto simp add: Nats_def) |
|
776 apply (rule range_eqI) |
|
777 apply (rule of_nat_mult [symmetric]) |
|
778 done |
|
779 |
|
780 text{*Agreement with the specific embedding for the integers*} |
|
781 lemma int_eq_of_nat: "int = (of_nat :: nat => int)" |
|
782 proof |
|
783 fix n |
|
784 show "int n = of_nat n" by (induct n, simp_all add: int_Suc add_ac) |
|
785 qed |
|
786 |
|
787 |
|
788 subsection{*Embedding of the Integers into any Ring: @{term of_int}*} |
|
789 |
|
790 constdefs |
|
791 of_int :: "int => 'a::ring" |
|
792 "of_int z == |
|
793 (THE a. \<exists>i j. (i,j) \<in> Rep_Integ z & a = (of_nat i) - (of_nat j))" |
|
794 |
|
795 |
|
796 lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j" |
|
797 apply (simp add: of_int_def) |
|
798 apply (rule the_equality, auto) |
|
799 apply (simp add: compare_rls add_ac of_nat_add [symmetric] |
|
800 del: of_nat_add) |
|
801 done |
|
802 |
|
803 lemma of_int_0 [simp]: "of_int 0 = 0" |
|
804 by (simp add: of_int Zero_int_def int_def) |
|
805 |
|
806 lemma of_int_1 [simp]: "of_int 1 = 1" |
|
807 by (simp add: of_int One_int_def int_def) |
|
808 |
|
809 lemma of_int_add [simp]: "of_int (w+z) = of_int w + of_int z" |
|
810 apply (rule eq_Abs_Integ [of w]) |
|
811 apply (rule eq_Abs_Integ [of z]) |
|
812 apply (simp add: compare_rls of_int zadd) |
|
813 done |
|
814 |
|
815 lemma of_int_minus [simp]: "of_int (-z) = - (of_int z)" |
|
816 apply (rule eq_Abs_Integ [of z]) |
|
817 apply (simp add: compare_rls of_int zminus) |
|
818 done |
|
819 |
|
820 lemma of_int_diff [simp]: "of_int (w-z) = of_int w - of_int z" |
|
821 by (simp add: diff_minus) |
|
822 |
|
823 lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z" |
|
824 apply (rule eq_Abs_Integ [of w]) |
|
825 apply (rule eq_Abs_Integ [of z]) |
|
826 apply (simp add: compare_rls of_int left_diff_distrib right_diff_distrib |
|
827 zmult add_ac) |
|
828 done |
|
829 |
|
830 lemma of_int_le_iff [simp]: |
|
831 "(of_int w \<le> (of_int z::'a::ordered_ring)) = (w \<le> z)" |
|
832 apply (rule eq_Abs_Integ [of w]) |
|
833 apply (rule eq_Abs_Integ [of z]) |
|
834 apply (simp add: compare_rls of_int zle zdiff_def zadd zminus |
|
835 of_nat_add [symmetric] del: of_nat_add) |
|
836 done |
|
837 |
|
838 text{*Special cases where either operand is zero*} |
|
839 declare of_int_le_iff [of 0, simplified, simp] |
|
840 declare of_int_le_iff [of _ 0, simplified, simp] |
|
841 |
|
842 lemma of_int_less_iff [simp]: |
|
843 "(of_int w < (of_int z::'a::ordered_ring)) = (w < z)" |
|
844 by (simp add: linorder_not_le [symmetric]) |
|
845 |
|
846 text{*Special cases where either operand is zero*} |
|
847 declare of_int_less_iff [of 0, simplified, simp] |
|
848 declare of_int_less_iff [of _ 0, simplified, simp] |
|
849 |
|
850 lemma of_int_eq_iff [simp]: |
|
851 "(of_int w = (of_int z::'a::ordered_ring)) = (w = z)" |
|
852 by (simp add: order_eq_iff) |
|
853 |
|
854 text{*Special cases where either operand is zero*} |
|
855 declare of_int_eq_iff [of 0, simplified, simp] |
|
856 declare of_int_eq_iff [of _ 0, simplified, simp] |
|
857 |
|
858 |
|
859 subsection{*The Set of Integers*} |
|
860 |
|
861 constdefs |
|
862 Ints :: "'a::ring set" |
|
863 "Ints == range of_int" |
|
864 |
|
865 |
|
866 syntax (xsymbols) |
|
867 Ints :: "'a set" ("\<int>") |
|
868 |
|
869 lemma Ints_0 [simp]: "0 \<in> Ints" |
|
870 apply (simp add: Ints_def) |
|
871 apply (rule range_eqI) |
|
872 apply (rule of_int_0 [symmetric]) |
|
873 done |
|
874 |
|
875 lemma Ints_1 [simp]: "1 \<in> Ints" |
|
876 apply (simp add: Ints_def) |
|
877 apply (rule range_eqI) |
|
878 apply (rule of_int_1 [symmetric]) |
|
879 done |
|
880 |
|
881 lemma Ints_add [simp]: "[|a \<in> Ints; b \<in> Ints|] ==> a+b \<in> Ints" |
|
882 apply (auto simp add: Ints_def) |
|
883 apply (rule range_eqI) |
|
884 apply (rule of_int_add [symmetric]) |
|
885 done |
|
886 |
|
887 lemma Ints_minus [simp]: "a \<in> Ints ==> -a \<in> Ints" |
|
888 apply (auto simp add: Ints_def) |
|
889 apply (rule range_eqI) |
|
890 apply (rule of_int_minus [symmetric]) |
|
891 done |
|
892 |
|
893 lemma Ints_diff [simp]: "[|a \<in> Ints; b \<in> Ints|] ==> a-b \<in> Ints" |
|
894 apply (auto simp add: Ints_def) |
|
895 apply (rule range_eqI) |
|
896 apply (rule of_int_diff [symmetric]) |
|
897 done |
|
898 |
|
899 lemma Ints_mult [simp]: "[|a \<in> Ints; b \<in> Ints|] ==> a*b \<in> Ints" |
|
900 apply (auto simp add: Ints_def) |
|
901 apply (rule range_eqI) |
|
902 apply (rule of_int_mult [symmetric]) |
|
903 done |
|
904 |
|
905 text{*Collapse nested embeddings*} |
|
906 lemma of_int_of_nat_eq [simp]: "of_int (of_nat n) = of_nat n" |
|
907 by (induct n, auto) |
|
908 |
|
909 lemma of_int_int_eq [simp]: "of_int (int n) = int n" |
|
910 by (simp add: int_eq_of_nat) |
|
911 |
|
912 |
|
913 lemma Ints_cases [case_names of_int, cases set: Ints]: |
|
914 "q \<in> \<int> ==> (!!z. q = of_int z ==> C) ==> C" |
|
915 proof (unfold Ints_def) |
|
916 assume "!!z. q = of_int z ==> C" |
|
917 assume "q \<in> range of_int" thus C .. |
|
918 qed |
|
919 |
|
920 lemma Ints_induct [case_names of_int, induct set: Ints]: |
|
921 "q \<in> \<int> ==> (!!z. P (of_int z)) ==> P q" |
|
922 by (rule Ints_cases) auto |
|
923 |
|
924 |
|
925 |
|
926 (*Legacy ML bindings, but no longer the structure Int.*) |
501 ML |
927 ML |
502 {* |
928 {* |
|
929 val zabs_def = thm "zabs_def" |
|
930 val nat_def = thm "nat_def" |
|
931 |
|
932 val int_0 = thm "int_0"; |
|
933 val int_1 = thm "int_1"; |
|
934 val int_Suc0_eq_1 = thm "int_Suc0_eq_1"; |
|
935 val neg_eq_less_0 = thm "neg_eq_less_0"; |
|
936 val not_neg_eq_ge_0 = thm "not_neg_eq_ge_0"; |
|
937 val not_neg_0 = thm "not_neg_0"; |
|
938 val not_neg_1 = thm "not_neg_1"; |
|
939 val iszero_0 = thm "iszero_0"; |
|
940 val not_iszero_1 = thm "not_iszero_1"; |
|
941 val int_0_less_1 = thm "int_0_less_1"; |
|
942 val int_0_neq_1 = thm "int_0_neq_1"; |
|
943 val negative_zless = thm "negative_zless"; |
|
944 val negative_zle = thm "negative_zle"; |
|
945 val not_zle_0_negative = thm "not_zle_0_negative"; |
|
946 val not_int_zless_negative = thm "not_int_zless_negative"; |
|
947 val negative_eq_positive = thm "negative_eq_positive"; |
|
948 val zle_iff_zadd = thm "zle_iff_zadd"; |
|
949 val abs_int_eq = thm "abs_int_eq"; |
|
950 val abs_split = thm"abs_split"; |
|
951 val nat_int = thm "nat_int"; |
|
952 val nat_zminus_int = thm "nat_zminus_int"; |
|
953 val nat_zero = thm "nat_zero"; |
|
954 val not_neg_nat = thm "not_neg_nat"; |
|
955 val neg_nat = thm "neg_nat"; |
|
956 val zless_nat_eq_int_zless = thm "zless_nat_eq_int_zless"; |
|
957 val nat_0_le = thm "nat_0_le"; |
|
958 val nat_le_0 = thm "nat_le_0"; |
|
959 val zless_nat_conj = thm "zless_nat_conj"; |
|
960 val int_cases = thm "int_cases"; |
|
961 |
503 val int_def = thm "int_def"; |
962 val int_def = thm "int_def"; |
504 val neg_def = thm "neg_def"; |
|
505 val iszero_def = thm "iszero_def"; |
|
506 val Zero_int_def = thm "Zero_int_def"; |
963 val Zero_int_def = thm "Zero_int_def"; |
507 val One_int_def = thm "One_int_def"; |
964 val One_int_def = thm "One_int_def"; |
508 val zadd_def = thm "zadd_def"; |
965 val zadd_def = thm "zadd_def"; |
509 val zdiff_def = thm "zdiff_def"; |
966 val zdiff_def = thm "zdiff_def"; |
510 val zless_def = thm "zless_def"; |
967 val zless_def = thm "zless_def"; |