1497 by (simp add: mult.assoc) |
1497 by (simp add: mult.assoc) |
1498 qed |
1498 qed |
1499 then show ?thesis by simp |
1499 then show ?thesis by simp |
1500 qed |
1500 qed |
1501 |
1501 |
1502 theorem zdvd_int: "x dvd y \<longleftrightarrow> int x dvd int y" |
1502 lemma int_dvd_int_iff [simp]: |
1503 proof - |
1503 "int m dvd int n \<longleftrightarrow> m dvd n" |
1504 have "x dvd y" if "int y = int x * k" for k |
1504 proof - |
|
1505 have "m dvd n" if "int n = int m * k" for k |
1505 proof (cases k) |
1506 proof (cases k) |
1506 case (nonneg n) |
1507 case (nonneg q) |
1507 with that have "y = x * n" |
1508 with that have "n = m * q" |
1508 by (simp del: of_nat_mult add: of_nat_mult [symmetric]) |
1509 by (simp del: of_nat_mult add: of_nat_mult [symmetric]) |
1509 then show ?thesis .. |
1510 then show ?thesis .. |
1510 next |
1511 next |
1511 case (neg n) |
1512 case (neg q) |
1512 with that have "int y = int x * (- int (Suc n))" |
1513 with that have "int n = int m * (- int (Suc q))" |
1513 by simp |
1514 by simp |
1514 also have "\<dots> = - (int x * int (Suc n))" |
1515 also have "\<dots> = - (int m * int (Suc q))" |
1515 by (simp only: mult_minus_right) |
1516 by (simp only: mult_minus_right) |
1516 also have "\<dots> = - int (x * Suc n)" |
1517 also have "\<dots> = - int (m * Suc q)" |
1517 by (simp only: of_nat_mult [symmetric]) |
1518 by (simp only: of_nat_mult [symmetric]) |
1518 finally have "- int (x * Suc n) = int y" .. |
1519 finally have "- int (m * Suc q) = int n" .. |
1519 then show ?thesis |
1520 then show ?thesis |
1520 by (simp only: negative_eq_positive) auto |
1521 by (simp only: negative_eq_positive) auto |
1521 qed |
1522 qed |
|
1523 then show ?thesis by (auto simp add: dvd_def) |
|
1524 qed |
|
1525 |
|
1526 lemma dvd_nat_abs_iff [simp]: |
|
1527 "n dvd nat \<bar>k\<bar> \<longleftrightarrow> int n dvd k" |
|
1528 proof - |
|
1529 have "n dvd nat \<bar>k\<bar> \<longleftrightarrow> int n dvd int (nat \<bar>k\<bar>)" |
|
1530 by (simp only: int_dvd_int_iff) |
1522 then show ?thesis |
1531 then show ?thesis |
1523 by (auto elim!: dvdE simp only: dvd_triv_left of_nat_mult) |
1532 by simp |
1524 qed |
1533 qed |
1525 |
1534 |
1526 lemma zdvd1_eq[simp]: "x dvd 1 \<longleftrightarrow> \<bar>x\<bar> = 1" |
1535 lemma nat_abs_dvd_iff [simp]: |
1527 (is "?lhs \<longleftrightarrow> ?rhs") |
1536 "nat \<bar>k\<bar> dvd n \<longleftrightarrow> k dvd int n" |
|
1537 proof - |
|
1538 have "nat \<bar>k\<bar> dvd n \<longleftrightarrow> int (nat \<bar>k\<bar>) dvd int n" |
|
1539 by (simp only: int_dvd_int_iff) |
|
1540 then show ?thesis |
|
1541 by simp |
|
1542 qed |
|
1543 |
|
1544 lemma zdvd1_eq [simp]: "x dvd 1 \<longleftrightarrow> \<bar>x\<bar> = 1" (is "?lhs \<longleftrightarrow> ?rhs") |
1528 for x :: int |
1545 for x :: int |
1529 proof |
1546 proof |
1530 assume ?lhs |
1547 assume ?lhs |
1531 then have "int (nat \<bar>x\<bar>) dvd int (nat 1)" by simp |
1548 then have "nat \<bar>x\<bar> dvd nat \<bar>1\<bar>" |
1532 then have "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int) |
1549 by (simp only: nat_abs_dvd_iff) simp |
1533 then have "nat \<bar>x\<bar> = 1" by simp |
1550 then have "nat \<bar>x\<bar> = 1" |
1534 then show ?rhs by (cases "x < 0") auto |
1551 by simp |
|
1552 then show ?rhs |
|
1553 by (cases "x < 0") simp_all |
1535 next |
1554 next |
1536 assume ?rhs |
1555 assume ?rhs |
1537 then have "x = 1 \<or> x = - 1" by auto |
1556 then have "x = 1 \<or> x = - 1" |
1538 then show ?lhs by (auto intro: dvdI) |
1557 by auto |
|
1558 then show ?lhs |
|
1559 by (auto intro: dvdI) |
1539 qed |
1560 qed |
1540 |
1561 |
1541 lemma zdvd_mult_cancel1: |
1562 lemma zdvd_mult_cancel1: |
1542 fixes m :: int |
1563 fixes m :: int |
1543 assumes mp: "m \<noteq> 0" |
1564 assumes mp: "m \<noteq> 0" |
1552 then have "m * n dvd m * 1" by simp |
1573 then have "m * n dvd m * 1" by simp |
1553 from zdvd_mult_cancel[OF this mp] show ?rhs |
1574 from zdvd_mult_cancel[OF this mp] show ?rhs |
1554 by (simp only: zdvd1_eq) |
1575 by (simp only: zdvd1_eq) |
1555 qed |
1576 qed |
1556 |
1577 |
1557 lemma int_dvd_iff: "int m dvd z \<longleftrightarrow> m dvd nat \<bar>z\<bar>" |
|
1558 by (cases "z \<ge> 0") (simp_all add: zdvd_int) |
|
1559 |
|
1560 lemma dvd_int_iff: "z dvd int m \<longleftrightarrow> nat \<bar>z\<bar> dvd m" |
|
1561 by (cases "z \<ge> 0") (simp_all add: zdvd_int) |
|
1562 |
|
1563 lemma dvd_int_unfold_dvd_nat: "k dvd l \<longleftrightarrow> nat \<bar>k\<bar> dvd nat \<bar>l\<bar>" |
|
1564 by (simp add: dvd_int_iff [symmetric]) |
|
1565 |
|
1566 lemma nat_dvd_iff: "nat z dvd m \<longleftrightarrow> (if 0 \<le> z then z dvd int m else m = 0)" |
1578 lemma nat_dvd_iff: "nat z dvd m \<longleftrightarrow> (if 0 \<le> z then z dvd int m else m = 0)" |
1567 by (auto simp add: dvd_int_iff) |
1579 using nat_abs_dvd_iff [of z m] by (cases "z \<ge> 0") auto |
1568 |
1580 |
1569 lemma eq_nat_nat_iff: "0 \<le> z \<Longrightarrow> 0 \<le> z' \<Longrightarrow> nat z = nat z' \<longleftrightarrow> z = z'" |
1581 lemma eq_nat_nat_iff: "0 \<le> z \<Longrightarrow> 0 \<le> z' \<Longrightarrow> nat z = nat z' \<longleftrightarrow> z = z'" |
1570 by (auto elim: nonneg_int_cases) |
1582 by (auto elim: nonneg_int_cases) |
1571 |
1583 |
1572 lemma nat_power_eq: "0 \<le> z \<Longrightarrow> nat (z ^ n) = nat z ^ n" |
1584 lemma nat_power_eq: "0 \<le> z \<Longrightarrow> nat (z ^ n) = nat z ^ n" |