161 show "0 \<noteq> (1::int)" |
161 show "0 \<noteq> (1::int)" |
162 by (simp add: Zero_int_def One_int_def) |
162 by (simp add: Zero_int_def One_int_def) |
163 qed |
163 qed |
164 |
164 |
165 lemma int_def: "of_nat m = Abs_Integ (intrel `` {(m, 0)})" |
165 lemma int_def: "of_nat m = Abs_Integ (intrel `` {(m, 0)})" |
166 by (induct m, simp_all add: Zero_int_def One_int_def add) |
166 by (induct m) (simp_all add: Zero_int_def One_int_def add) |
167 |
167 |
168 |
168 |
169 subsection {* The @{text "\<le>"} Ordering *} |
169 subsection {* The @{text "\<le>"} Ordering *} |
170 |
170 |
171 lemma le: |
171 lemma le: |
217 text{*Strict Monotonicity of Multiplication*} |
217 text{*Strict Monotonicity of Multiplication*} |
218 |
218 |
219 text{*strict, in 1st argument; proof is by induction on k>0*} |
219 text{*strict, in 1st argument; proof is by induction on k>0*} |
220 lemma zmult_zless_mono2_lemma: |
220 lemma zmult_zless_mono2_lemma: |
221 "(i::int)<j ==> 0<k ==> of_nat k * i < of_nat k * j" |
221 "(i::int)<j ==> 0<k ==> of_nat k * i < of_nat k * j" |
222 apply (induct "k", simp) |
222 apply (induct k) |
|
223 apply simp |
223 apply (simp add: left_distrib) |
224 apply (simp add: left_distrib) |
224 apply (case_tac "k=0") |
225 apply (case_tac "k=0") |
225 apply (simp_all add: add_strict_mono) |
226 apply (simp_all add: add_strict_mono) |
226 done |
227 done |
227 |
228 |
297 |
298 |
298 lemma of_int_1 [simp]: "of_int 1 = 1" |
299 lemma of_int_1 [simp]: "of_int 1 = 1" |
299 by (simp add: of_int One_int_def) |
300 by (simp add: of_int One_int_def) |
300 |
301 |
301 lemma of_int_add [simp]: "of_int (w+z) = of_int w + of_int z" |
302 lemma of_int_add [simp]: "of_int (w+z) = of_int w + of_int z" |
302 by (cases w, cases z, simp add: algebra_simps of_int add) |
303 by (cases w, cases z) (simp add: algebra_simps of_int add) |
303 |
304 |
304 lemma of_int_minus [simp]: "of_int (-z) = - (of_int z)" |
305 lemma of_int_minus [simp]: "of_int (-z) = - (of_int z)" |
305 by (cases z, simp add: algebra_simps of_int minus) |
306 by (cases z) (simp add: algebra_simps of_int minus) |
306 |
307 |
307 lemma of_int_diff [simp]: "of_int (w - z) = of_int w - of_int z" |
308 lemma of_int_diff [simp]: "of_int (w - z) = of_int w - of_int z" |
308 by (simp add: diff_minus Groups.diff_minus) |
309 by (simp add: diff_minus Groups.diff_minus) |
309 |
310 |
310 lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z" |
311 lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z" |
327 class ring_char_0 = ring_1 + semiring_char_0 |
328 class ring_char_0 = ring_1 + semiring_char_0 |
328 begin |
329 begin |
329 |
330 |
330 lemma of_int_eq_iff [simp]: |
331 lemma of_int_eq_iff [simp]: |
331 "of_int w = of_int z \<longleftrightarrow> w = z" |
332 "of_int w = of_int z \<longleftrightarrow> w = z" |
332 apply (cases w, cases z, simp add: of_int) |
333 apply (cases w, cases z) |
|
334 apply (simp add: of_int) |
333 apply (simp only: diff_eq_eq diff_add_eq eq_diff_eq) |
335 apply (simp only: diff_eq_eq diff_add_eq eq_diff_eq) |
334 apply (simp only: of_nat_add [symmetric] of_nat_eq_iff) |
336 apply (simp only: of_nat_add [symmetric] of_nat_eq_iff) |
335 done |
337 done |
336 |
338 |
337 text{*Special cases where either operand is zero*} |
339 text{*Special cases where either operand is zero*} |
351 text{*Every @{text linordered_idom} has characteristic zero.*} |
353 text{*Every @{text linordered_idom} has characteristic zero.*} |
352 subclass ring_char_0 .. |
354 subclass ring_char_0 .. |
353 |
355 |
354 lemma of_int_le_iff [simp]: |
356 lemma of_int_le_iff [simp]: |
355 "of_int w \<le> of_int z \<longleftrightarrow> w \<le> z" |
357 "of_int w \<le> of_int z \<longleftrightarrow> w \<le> z" |
356 by (cases w, cases z, simp add: of_int le minus algebra_simps of_nat_add [symmetric] del: of_nat_add) |
358 by (cases w, cases z) |
|
359 (simp add: of_int le minus algebra_simps of_nat_add [symmetric] del: of_nat_add) |
357 |
360 |
358 lemma of_int_less_iff [simp]: |
361 lemma of_int_less_iff [simp]: |
359 "of_int w < of_int z \<longleftrightarrow> w < z" |
362 "of_int w < of_int z \<longleftrightarrow> w < z" |
360 by (simp add: less_le order_less_le) |
363 by (simp add: less_le order_less_le) |
361 |
364 |
403 (* FIXME: duplicates nat_0 *) |
406 (* FIXME: duplicates nat_0 *) |
404 lemma nat_zero [simp]: "nat 0 = 0" |
407 lemma nat_zero [simp]: "nat 0 = 0" |
405 by (simp add: Zero_int_def nat) |
408 by (simp add: Zero_int_def nat) |
406 |
409 |
407 lemma int_nat_eq [simp]: "of_nat (nat z) = (if 0 \<le> z then z else 0)" |
410 lemma int_nat_eq [simp]: "of_nat (nat z) = (if 0 \<le> z then z else 0)" |
408 by (cases z, simp add: nat le int_def Zero_int_def) |
411 by (cases z) (simp add: nat le int_def Zero_int_def) |
409 |
412 |
410 corollary nat_0_le: "0 \<le> z ==> of_nat (nat z) = z" |
413 corollary nat_0_le: "0 \<le> z ==> of_nat (nat z) = z" |
411 by simp |
414 by simp |
412 |
415 |
413 lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0" |
416 lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0" |
414 by (cases z, simp add: nat le Zero_int_def) |
417 by (cases z) (simp add: nat le Zero_int_def) |
415 |
418 |
416 lemma nat_le_eq_zle: "0 < w | 0 \<le> z ==> (nat w \<le> nat z) = (w\<le>z)" |
419 lemma nat_le_eq_zle: "0 < w | 0 \<le> z ==> (nat w \<le> nat z) = (w\<le>z)" |
417 apply (cases w, cases z) |
420 apply (cases w, cases z) |
418 apply (simp add: nat le linorder_not_le [symmetric] Zero_int_def, arith) |
421 apply (simp add: nat le linorder_not_le [symmetric] Zero_int_def, arith) |
419 done |
422 done |
435 assumes "0 \<le> z" and "\<And>m. z = of_nat m \<Longrightarrow> P" |
438 assumes "0 \<le> z" and "\<And>m. z = of_nat m \<Longrightarrow> P" |
436 shows P |
439 shows P |
437 using assms by (blast dest: nat_0_le sym) |
440 using assms by (blast dest: nat_0_le sym) |
438 |
441 |
439 lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = of_nat m else m=0)" |
442 lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = of_nat m else m=0)" |
440 by (cases w, simp add: nat le int_def Zero_int_def, arith) |
443 by (cases w) (simp add: nat le int_def Zero_int_def, arith) |
441 |
444 |
442 corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = of_nat m else m=0)" |
445 corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = of_nat m else m=0)" |
443 by (simp only: eq_commute [of m] nat_eq_iff) |
446 by (simp only: eq_commute [of m] nat_eq_iff) |
444 |
447 |
445 lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < of_nat m)" |
448 lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < of_nat m)" |
456 lemma zero_less_nat_eq [simp]: "(0 < nat z) = (0 < z)" |
459 lemma zero_less_nat_eq [simp]: "(0 < nat z) = (0 < z)" |
457 by (insert zless_nat_conj [of 0], auto) |
460 by (insert zless_nat_conj [of 0], auto) |
458 |
461 |
459 lemma nat_add_distrib: |
462 lemma nat_add_distrib: |
460 "[| (0::int) \<le> z; 0 \<le> z' |] ==> nat (z+z') = nat z + nat z'" |
463 "[| (0::int) \<le> z; 0 \<le> z' |] ==> nat (z+z') = nat z + nat z'" |
461 by (cases z, cases z', simp add: nat add le Zero_int_def) |
464 by (cases z, cases z') (simp add: nat add le Zero_int_def) |
462 |
465 |
463 lemma nat_diff_distrib: |
466 lemma nat_diff_distrib: |
464 "[| (0::int) \<le> z'; z' \<le> z |] ==> nat (z-z') = nat z - nat z'" |
467 "[| (0::int) \<le> z'; z' \<le> z |] ==> nat (z-z') = nat z - nat z'" |
465 by (cases z, cases z', |
468 by (cases z, cases z') |
466 simp add: nat add minus diff_minus le Zero_int_def) |
469 (simp add: nat add minus diff_minus le Zero_int_def) |
467 |
470 |
468 lemma nat_zminus_int [simp]: "nat (- (of_nat n)) = 0" |
471 lemma nat_zminus_int [simp]: "nat (- (of_nat n)) = 0" |
469 by (simp add: int_def minus nat Zero_int_def) |
472 by (simp add: int_def minus nat Zero_int_def) |
470 |
473 |
471 lemma zless_nat_eq_int_zless: "(m < nat z) = (of_nat m < z)" |
474 lemma zless_nat_eq_int_zless: "(m < nat z) = (of_nat m < z)" |
472 by (cases z, simp add: nat less int_def, arith) |
475 by (cases z) (simp add: nat less int_def, arith) |
473 |
476 |
474 context ring_1 |
477 context ring_1 |
475 begin |
478 begin |
476 |
479 |
477 lemma of_nat_nat: "0 \<le> z \<Longrightarrow> of_nat (nat z) = of_int z" |
480 lemma of_nat_nat: "0 \<le> z \<Longrightarrow> of_nat (nat z) = of_int z" |
545 subsection {* Cases and induction *} |
548 subsection {* Cases and induction *} |
546 |
549 |
547 text{*Now we replace the case analysis rule by a more conventional one: |
550 text{*Now we replace the case analysis rule by a more conventional one: |
548 whether an integer is negative or not.*} |
551 whether an integer is negative or not.*} |
549 |
552 |
550 theorem int_cases [cases type: int, case_names nonneg neg]: |
553 theorem int_cases [case_names nonneg neg, cases type: int]: |
551 "[|!! n. (z \<Colon> int) = of_nat n ==> P; !! n. z = - (of_nat (Suc n)) ==> P |] ==> P" |
554 "[|!! n. (z \<Colon> int) = of_nat n ==> P; !! n. z = - (of_nat (Suc n)) ==> P |] ==> P" |
552 apply (cases "z < 0", blast dest!: negD) |
555 apply (cases "z < 0") |
|
556 apply (blast dest!: negD) |
553 apply (simp add: linorder_not_less del: of_nat_Suc) |
557 apply (simp add: linorder_not_less del: of_nat_Suc) |
554 apply auto |
558 apply auto |
555 apply (blast dest: nat_0_le [THEN sym]) |
559 apply (blast dest: nat_0_le [THEN sym]) |
556 done |
560 done |
557 |
561 |
558 theorem int_of_nat_induct [induct type: int, case_names nonneg neg]: |
562 theorem int_of_nat_induct [case_names nonneg neg, induct type: int]: |
559 "[|!! n. P (of_nat n \<Colon> int); !!n. P (- (of_nat (Suc n))) |] ==> P z" |
563 "[|!! n. P (of_nat n \<Colon> int); !!n. P (- (of_nat (Suc n))) |] ==> P z" |
560 by (cases z rule: int_cases) auto |
564 by (cases z) auto |
561 |
565 |
562 text{*Contributed by Brian Huffman*} |
566 text{*Contributed by Brian Huffman*} |
563 theorem int_diff_cases: |
567 theorem int_diff_cases: |
564 obtains (diff) m n where "(z\<Colon>int) = of_nat m - of_nat n" |
568 obtains (diff) m n where "(z\<Colon>int) = of_nat m - of_nat n" |
565 apply (cases z rule: eq_Abs_Integ) |
569 apply (cases z rule: eq_Abs_Integ) |
820 finally show "0 < 1 + z" . |
824 finally show "0 < 1 + z" . |
821 qed |
825 qed |
822 |
826 |
823 lemma odd_less_0_iff: |
827 lemma odd_less_0_iff: |
824 "(1 + z + z < 0) = (z < (0::int))" |
828 "(1 + z + z < 0) = (z < (0::int))" |
825 proof (cases z rule: int_cases) |
829 proof (cases z) |
826 case (nonneg n) |
830 case (nonneg n) |
827 thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing |
831 thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing |
828 le_imp_0_less [THEN order_less_imp_le]) |
832 le_imp_0_less [THEN order_less_imp_le]) |
829 next |
833 next |
830 case (neg n) |
834 case (neg n) |
1157 finally show ?thesis . |
1161 finally show ?thesis . |
1158 qed |
1162 qed |
1159 |
1163 |
1160 lemma odd_less_0: |
1164 lemma odd_less_0: |
1161 "(1 + z + z < 0) = (z < (0::int))" |
1165 "(1 + z + z < 0) = (z < (0::int))" |
1162 proof (cases z rule: int_cases) |
1166 proof (cases z) |
1163 case (nonneg n) |
1167 case (nonneg n) |
1164 thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing |
1168 then show ?thesis |
1165 le_imp_0_less [THEN order_less_imp_le]) |
1169 by (simp add: linorder_not_less add_assoc add_increasing |
|
1170 le_imp_0_less [THEN order_less_imp_le]) |
1166 next |
1171 next |
1167 case (neg n) |
1172 case (neg n) |
1168 thus ?thesis by (simp del: of_nat_Suc of_nat_add of_nat_1 |
1173 then show ?thesis |
1169 add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric]) |
1174 by (simp del: of_nat_Suc of_nat_add of_nat_1 |
|
1175 add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric]) |
1170 qed |
1176 qed |
1171 |
1177 |
1172 text {* Less-Than or Equals *} |
1178 text {* Less-Than or Equals *} |
1173 |
1179 |
1174 text {* Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals. *} |
1180 text {* Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals. *} |
1707 assumes ge: "k \<le> i" and |
1713 assumes ge: "k \<le> i" and |
1708 base: "P k" and |
1714 base: "P k" and |
1709 step: "\<And>i. k \<le> i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)" |
1715 step: "\<And>i. k \<le> i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)" |
1710 shows "P i" |
1716 shows "P i" |
1711 proof - |
1717 proof - |
1712 { fix n have "\<And>i::int. n = nat(i-k) \<Longrightarrow> k \<le> i \<Longrightarrow> P i" |
1718 { fix n |
|
1719 have "\<And>i::int. n = nat (i - k) \<Longrightarrow> k \<le> i \<Longrightarrow> P i" |
1713 proof (induct n) |
1720 proof (induct n) |
1714 case 0 |
1721 case 0 |
1715 hence "i = k" by arith |
1722 hence "i = k" by arith |
1716 thus "P i" using base by simp |
1723 thus "P i" using base by simp |
1717 next |
1724 next |
1718 case (Suc n) |
1725 case (Suc n) |
1719 then have "n = nat((i - 1) - k)" by arith |
1726 then have "n = nat((i - 1) - k)" by arith |
1720 moreover |
1727 moreover |
1721 have ki1: "k \<le> i - 1" using Suc.prems by arith |
1728 have ki1: "k \<le> i - 1" using Suc.prems by arith |
1722 ultimately |
1729 ultimately |
1723 have "P(i - 1)" by(rule Suc.hyps) |
1730 have "P (i - 1)" by (rule Suc.hyps) |
1724 from step[OF ki1 this] show ?case by simp |
1731 from step [OF ki1 this] show ?case by simp |
1725 qed |
1732 qed |
1726 } |
1733 } |
1727 with ge show ?thesis by fast |
1734 with ge show ?thesis by fast |
1728 qed |
1735 qed |
1729 |
1736 |
1737 using gr apply arith |
1744 using gr apply arith |
1738 apply(rule base) |
1745 apply(rule base) |
1739 apply (rule step, simp+) |
1746 apply (rule step, simp+) |
1740 done |
1747 done |
1741 |
1748 |
1742 theorem int_le_induct[consumes 1,case_names base step]: |
1749 theorem int_le_induct [consumes 1, case_names base step]: |
1743 assumes le: "i \<le> (k::int)" and |
1750 assumes le: "i \<le> (k::int)" and |
1744 base: "P(k)" and |
1751 base: "P(k)" and |
1745 step: "\<And>i. \<lbrakk>i \<le> k; P i\<rbrakk> \<Longrightarrow> P(i - 1)" |
1752 step: "\<And>i. \<lbrakk>i \<le> k; P i\<rbrakk> \<Longrightarrow> P(i - 1)" |
1746 shows "P i" |
1753 shows "P i" |
1747 proof - |
1754 proof - |
1748 { fix n have "\<And>i::int. n = nat(k-i) \<Longrightarrow> i \<le> k \<Longrightarrow> P i" |
1755 { fix n |
|
1756 have "\<And>i::int. n = nat(k-i) \<Longrightarrow> i \<le> k \<Longrightarrow> P i" |
1749 proof (induct n) |
1757 proof (induct n) |
1750 case 0 |
1758 case 0 |
1751 hence "i = k" by arith |
1759 hence "i = k" by arith |
1752 thus "P i" using base by simp |
1760 thus "P i" using base by simp |
1753 next |
1761 next |
1754 case (Suc n) |
1762 case (Suc n) |
1755 hence "n = nat(k - (i+1))" by arith |
1763 hence "n = nat (k - (i + 1))" by arith |
1756 moreover |
1764 moreover |
1757 have ki1: "i + 1 \<le> k" using Suc.prems by arith |
1765 have ki1: "i + 1 \<le> k" using Suc.prems by arith |
1758 ultimately |
1766 ultimately |
1759 have "P(i+1)" by(rule Suc.hyps) |
1767 have "P (i + 1)" by(rule Suc.hyps) |
1760 from step[OF ki1 this] show ?case by simp |
1768 from step[OF ki1 this] show ?case by simp |
1761 qed |
1769 qed |
1762 } |
1770 } |
1763 with le show ?thesis by fast |
1771 with le show ?thesis by fast |
1764 qed |
1772 qed |
1765 |
1773 |
1766 theorem int_less_induct [consumes 1,case_names base step]: |
1774 theorem int_less_induct [consumes 1, case_names base step]: |
1767 assumes less: "(i::int) < k" and |
1775 assumes less: "(i::int) < k" and |
1768 base: "P(k - 1)" and |
1776 base: "P(k - 1)" and |
1769 step: "\<And>i. \<lbrakk>i < k; P i\<rbrakk> \<Longrightarrow> P(i - 1)" |
1777 step: "\<And>i. \<lbrakk>i < k; P i\<rbrakk> \<Longrightarrow> P(i - 1)" |
1770 shows "P i" |
1778 shows "P i" |
1771 apply(rule int_le_induct[of _ "k - 1"]) |
1779 apply(rule int_le_induct[of _ "k - 1"]) |
1780 and step1: "\<And>i. k \<le> i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)" |
1788 and step1: "\<And>i. k \<le> i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)" |
1781 and step2: "\<And>i. k \<ge> i \<Longrightarrow> P i \<Longrightarrow> P (i - 1)" |
1789 and step2: "\<And>i. k \<ge> i \<Longrightarrow> P i \<Longrightarrow> P (i - 1)" |
1782 shows "P i" |
1790 shows "P i" |
1783 proof - |
1791 proof - |
1784 have "i \<le> k \<or> i \<ge> k" by arith |
1792 have "i \<le> k \<or> i \<ge> k" by arith |
1785 then show ?thesis proof |
1793 then show ?thesis |
1786 assume "i \<ge> k" then show ?thesis using base |
1794 proof |
|
1795 assume "i \<ge> k" |
|
1796 then show ?thesis using base |
1787 by (rule int_ge_induct) (fact step1) |
1797 by (rule int_ge_induct) (fact step1) |
1788 next |
1798 next |
1789 assume "i \<le> k" then show ?thesis using base |
1799 assume "i \<le> k" |
|
1800 then show ?thesis using base |
1790 by (rule int_le_induct) (fact step2) |
1801 by (rule int_le_induct) (fact step2) |
1791 qed |
1802 qed |
1792 qed |
1803 qed |
1793 |
1804 |
1794 subsection{*Intermediate value theorems*} |
1805 subsection{*Intermediate value theorems*} |
1795 |
1806 |
1796 lemma int_val_lemma: |
1807 lemma int_val_lemma: |
1797 "(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) --> |
1808 "(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) --> |
1798 f 0 \<le> k --> k \<le> f n --> (\<exists>i \<le> n. f i = (k::int))" |
1809 f 0 \<le> k --> k \<le> f n --> (\<exists>i \<le> n. f i = (k::int))" |
1799 unfolding One_nat_def |
1810 unfolding One_nat_def |
1800 apply (induct n, simp) |
1811 apply (induct n) |
|
1812 apply simp |
1801 apply (intro strip) |
1813 apply (intro strip) |
1802 apply (erule impE, simp) |
1814 apply (erule impE, simp) |
1803 apply (erule_tac x = n in allE, simp) |
1815 apply (erule_tac x = n in allE, simp) |
1804 apply (case_tac "k = f (Suc n)") |
1816 apply (case_tac "k = f (Suc n)") |
1805 apply force |
1817 apply force |
2118 proof - |
2130 proof - |
2119 have "\<And>k. int y = int x * k \<Longrightarrow> x dvd y" |
2131 have "\<And>k. int y = int x * k \<Longrightarrow> x dvd y" |
2120 proof - |
2132 proof - |
2121 fix k |
2133 fix k |
2122 assume A: "int y = int x * k" |
2134 assume A: "int y = int x * k" |
2123 then show "x dvd y" proof (cases k) |
2135 then show "x dvd y" |
2124 case (1 n) with A have "y = x * n" by (simp add: of_nat_mult [symmetric]) |
2136 proof (cases k) |
|
2137 case (nonneg n) |
|
2138 with A have "y = x * n" by (simp add: of_nat_mult [symmetric]) |
2125 then show ?thesis .. |
2139 then show ?thesis .. |
2126 next |
2140 next |
2127 case (2 n) with A have "int y = int x * (- int (Suc n))" by simp |
2141 case (neg n) |
|
2142 with A have "int y = int x * (- int (Suc n))" by simp |
2128 also have "\<dots> = - (int x * int (Suc n))" by (simp only: mult_minus_right) |
2143 also have "\<dots> = - (int x * int (Suc n))" by (simp only: mult_minus_right) |
2129 also have "\<dots> = - int (x * Suc n)" by (simp only: of_nat_mult [symmetric]) |
2144 also have "\<dots> = - int (x * Suc n)" by (simp only: of_nat_mult [symmetric]) |
2130 finally have "- int (x * Suc n) = int y" .. |
2145 finally have "- int (x * Suc n) = int y" .. |
2131 then show ?thesis by (simp only: negative_eq_positive) auto |
2146 then show ?thesis by (simp only: negative_eq_positive) auto |
2132 qed |
2147 qed |
2133 qed |
2148 qed |
2134 then show ?thesis by (auto elim!: dvdE simp only: dvd_triv_left of_nat_mult) |
2149 then show ?thesis by (auto elim!: dvdE simp only: dvd_triv_left of_nat_mult) |
2135 qed |
2150 qed |
2136 |
2151 |
2137 lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)" |
2152 lemma zdvd1_eq[simp]: "(x::int) dvd 1 = (\<bar>x\<bar> = 1)" |
2138 proof |
2153 proof |
2139 assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by simp |
2154 assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by simp |
2140 hence "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int) |
2155 hence "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int) |
2141 hence "nat \<bar>x\<bar> = 1" by simp |
2156 hence "nat \<bar>x\<bar> = 1" by simp |
2142 thus "\<bar>x\<bar> = 1" by (cases "x < 0", auto) |
2157 thus "\<bar>x\<bar> = 1" by (cases "x < 0") auto |
2143 next |
2158 next |
2144 assume "\<bar>x\<bar>=1" |
2159 assume "\<bar>x\<bar>=1" |
2145 then have "x = 1 \<or> x = -1" by auto |
2160 then have "x = 1 \<or> x = -1" by auto |
2146 then show "x dvd 1" by (auto intro: dvdI) |
2161 then show "x dvd 1" by (auto intro: dvdI) |
2147 qed |
2162 qed |
2148 |
2163 |
2149 lemma zdvd_mult_cancel1: |
2164 lemma zdvd_mult_cancel1: |
2150 assumes mp:"m \<noteq>(0::int)" shows "(m * n dvd m) = (\<bar>n\<bar> = 1)" |
2165 assumes mp:"m \<noteq>(0::int)" shows "(m * n dvd m) = (\<bar>n\<bar> = 1)" |
2151 proof |
2166 proof |
2152 assume n1: "\<bar>n\<bar> = 1" thus "m * n dvd m" |
2167 assume n1: "\<bar>n\<bar> = 1" thus "m * n dvd m" |
2153 by (cases "n >0", auto simp add: minus_equation_iff) |
2168 by (cases "n >0") (auto simp add: minus_equation_iff) |
2154 next |
2169 next |
2155 assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp |
2170 assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp |
2156 from zdvd_mult_cancel[OF H2 mp] show "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq) |
2171 from zdvd_mult_cancel[OF H2 mp] show "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq) |
2157 qed |
2172 qed |
2158 |
2173 |
2172 lemma nat_power_eq: |
2187 lemma nat_power_eq: |
2173 "0 \<le> z \<Longrightarrow> nat (z ^ n) = nat z ^ n" |
2188 "0 \<le> z \<Longrightarrow> nat (z ^ n) = nat z ^ n" |
2174 by (induct n) (simp_all add: nat_mult_distrib) |
2189 by (induct n) (simp_all add: nat_mult_distrib) |
2175 |
2190 |
2176 lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)" |
2191 lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)" |
2177 apply (rule_tac z=n in int_cases) |
2192 apply (cases n) |
2178 apply (auto simp add: dvd_int_iff) |
2193 apply (auto simp add: dvd_int_iff) |
2179 apply (rule_tac z=z in int_cases) |
2194 apply (cases z) |
2180 apply (auto simp add: dvd_imp_le) |
2195 apply (auto simp add: dvd_imp_le) |
2181 done |
2196 done |
2182 |
2197 |
2183 lemma zdvd_period: |
2198 lemma zdvd_period: |
2184 fixes a d :: int |
2199 fixes a d :: int |
2185 assumes "a dvd d" |
2200 assumes "a dvd d" |
2186 shows "a dvd (x + t) \<longleftrightarrow> a dvd ((x + c * d) + t)" |
2201 shows "a dvd (x + t) \<longleftrightarrow> a dvd ((x + c * d) + t)" |
2187 proof - |
2202 proof - |
2188 from assms obtain k where "d = a * k" by (rule dvdE) |
2203 from assms obtain k where "d = a * k" by (rule dvdE) |
2189 show ?thesis proof |
2204 show ?thesis |
|
2205 proof |
2190 assume "a dvd (x + t)" |
2206 assume "a dvd (x + t)" |
2191 then obtain l where "x + t = a * l" by (rule dvdE) |
2207 then obtain l where "x + t = a * l" by (rule dvdE) |
2192 then have "x = a * l - t" by simp |
2208 then have "x = a * l - t" by simp |
2193 with `d = a * k` show "a dvd x + c * d + t" by simp |
2209 with `d = a * k` show "a dvd x + c * d + t" by simp |
2194 next |
2210 next |