1288 |
1288 |
1289 class semidom_divide_unit_factor = semidom_divide + unit_factor + |
1289 class semidom_divide_unit_factor = semidom_divide + unit_factor + |
1290 assumes unit_factor_0 [simp]: "unit_factor 0 = 0" |
1290 assumes unit_factor_0 [simp]: "unit_factor 0 = 0" |
1291 and is_unit_unit_factor: "a dvd 1 \<Longrightarrow> unit_factor a = a" |
1291 and is_unit_unit_factor: "a dvd 1 \<Longrightarrow> unit_factor a = a" |
1292 and unit_factor_is_unit: "a \<noteq> 0 \<Longrightarrow> unit_factor a dvd 1" |
1292 and unit_factor_is_unit: "a \<noteq> 0 \<Longrightarrow> unit_factor a dvd 1" |
1293 and unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b" |
1293 and unit_factor_mult_unit_left: "a dvd 1 \<Longrightarrow> unit_factor (a * b) = a * unit_factor b" |
1294 \<comment> \<open>This fine-grained hierarchy will later on allow lean normalization of polynomials\<close> |
1294 \<comment> \<open>This fine-grained hierarchy will later on allow lean normalization of polynomials\<close> |
1295 |
1295 begin |
|
1296 |
|
1297 lemma unit_factor_mult_unit_right: "a dvd 1 \<Longrightarrow> unit_factor (b * a) = unit_factor b * a" |
|
1298 using unit_factor_mult_unit_left[of a b] by (simp add: mult_ac) |
|
1299 |
|
1300 lemmas [simp] = unit_factor_mult_unit_left unit_factor_mult_unit_right |
|
1301 |
|
1302 end |
|
1303 |
1296 class normalization_semidom = algebraic_semidom + semidom_divide_unit_factor + |
1304 class normalization_semidom = algebraic_semidom + semidom_divide_unit_factor + |
1297 fixes normalize :: "'a \<Rightarrow> 'a" |
1305 fixes normalize :: "'a \<Rightarrow> 'a" |
1298 assumes unit_factor_mult_normalize [simp]: "unit_factor a * normalize a = a" |
1306 assumes unit_factor_mult_normalize [simp]: "unit_factor a * normalize a = a" |
1299 and normalize_0 [simp]: "normalize 0 = 0" |
1307 and normalize_0 [simp]: "normalize 0 = 0" |
1300 begin |
1308 begin |
1432 next |
1440 next |
1433 assume ?rhs |
1441 assume ?rhs |
1434 then show ?lhs by simp |
1442 then show ?lhs by simp |
1435 qed |
1443 qed |
1436 |
1444 |
1437 lemma normalize_mult: "normalize (a * b) = normalize a * normalize b" |
|
1438 proof (cases "a = 0 \<or> b = 0") |
|
1439 case True |
|
1440 then show ?thesis by auto |
|
1441 next |
|
1442 case False |
|
1443 have "unit_factor (a * b) * normalize (a * b) = a * b" |
|
1444 by (rule unit_factor_mult_normalize) |
|
1445 then have "normalize (a * b) = a * b div unit_factor (a * b)" |
|
1446 by simp |
|
1447 also have "\<dots> = a * b div unit_factor (b * a)" |
|
1448 by (simp add: ac_simps) |
|
1449 also have "\<dots> = a * b div unit_factor b div unit_factor a" |
|
1450 using False by (simp add: unit_factor_mult is_unit_div_mult2_eq [symmetric]) |
|
1451 also have "\<dots> = a * (b div unit_factor b) div unit_factor a" |
|
1452 using False by (subst unit_div_mult_swap) simp_all |
|
1453 also have "\<dots> = normalize a * normalize b" |
|
1454 using False |
|
1455 by (simp add: mult.commute [of a] mult.commute [of "normalize a"] unit_div_mult_swap [symmetric]) |
|
1456 finally show ?thesis . |
|
1457 qed |
|
1458 |
|
1459 lemma unit_factor_idem [simp]: "unit_factor (unit_factor a) = unit_factor a" |
1445 lemma unit_factor_idem [simp]: "unit_factor (unit_factor a) = unit_factor a" |
1460 by (cases "a = 0") (auto intro: is_unit_unit_factor) |
1446 by (cases "a = 0") (auto intro: is_unit_unit_factor) |
1461 |
1447 |
1462 lemma normalize_unit_factor [simp]: "a \<noteq> 0 \<Longrightarrow> normalize (unit_factor a) = 1" |
1448 lemma normalize_unit_factor [simp]: "a \<noteq> 0 \<Longrightarrow> normalize (unit_factor a) = 1" |
1463 by (rule is_unit_normalize) simp |
1449 by (rule is_unit_normalize) simp |
1464 |
1450 |
|
1451 lemma normalize_mult_unit_left [simp]: |
|
1452 assumes "a dvd 1" |
|
1453 shows "normalize (a * b) = normalize b" |
|
1454 proof (cases "b = 0") |
|
1455 case False |
|
1456 have "a * unit_factor b * normalize (a * b) = unit_factor (a * b) * normalize (a * b)" |
|
1457 using assms by (subst unit_factor_mult_unit_left) auto |
|
1458 also have "\<dots> = a * b" by simp |
|
1459 also have "b = unit_factor b * normalize b" by simp |
|
1460 hence "a * b = a * unit_factor b * normalize b" |
|
1461 by (simp only: mult_ac) |
|
1462 finally show ?thesis |
|
1463 using assms False by auto |
|
1464 qed auto |
|
1465 |
|
1466 lemma normalize_mult_unit_right [simp]: |
|
1467 assumes "b dvd 1" |
|
1468 shows "normalize (a * b) = normalize a" |
|
1469 using assms by (subst mult.commute) auto |
|
1470 |
1465 lemma normalize_idem [simp]: "normalize (normalize a) = normalize a" |
1471 lemma normalize_idem [simp]: "normalize (normalize a) = normalize a" |
1466 proof (cases "a = 0") |
1472 proof (cases "a = 0") |
1467 case True |
|
1468 then show ?thesis by simp |
|
1469 next |
|
1470 case False |
1473 case False |
1471 have "normalize a = normalize (unit_factor a * normalize a)" |
1474 have "normalize a = normalize (unit_factor a * normalize a)" |
1472 by simp |
1475 by simp |
1473 also have "\<dots> = normalize (unit_factor a) * normalize (normalize a)" |
1476 also from False have "\<dots> = normalize (normalize a)" |
1474 by (simp only: normalize_mult) |
1477 by (subst normalize_mult_unit_left) auto |
1475 finally show ?thesis |
1478 finally show ?thesis .. |
1476 using False by simp_all |
1479 qed auto |
1477 qed |
|
1478 |
1480 |
1479 lemma unit_factor_normalize [simp]: |
1481 lemma unit_factor_normalize [simp]: |
1480 assumes "a \<noteq> 0" |
1482 assumes "a \<noteq> 0" |
1481 shows "unit_factor (normalize a) = 1" |
1483 shows "unit_factor (normalize a) = 1" |
1482 proof - |
1484 proof - |
1488 by simp |
1490 by simp |
1489 with * have "unit_factor (normalize a) * normalize a div normalize a = normalize a div normalize a" |
1491 with * have "unit_factor (normalize a) * normalize a div normalize a = normalize a div normalize a" |
1490 by simp |
1492 by simp |
1491 with * show ?thesis |
1493 with * show ?thesis |
1492 by simp |
1494 by simp |
1493 qed |
|
1494 |
|
1495 lemma dvd_unit_factor_div: |
|
1496 assumes "b dvd a" |
|
1497 shows "unit_factor (a div b) = unit_factor a div unit_factor b" |
|
1498 proof - |
|
1499 from assms have "a = a div b * b" |
|
1500 by simp |
|
1501 then have "unit_factor a = unit_factor (a div b * b)" |
|
1502 by simp |
|
1503 then show ?thesis |
|
1504 by (cases "b = 0") (simp_all add: unit_factor_mult) |
|
1505 qed |
|
1506 |
|
1507 lemma dvd_normalize_div: |
|
1508 assumes "b dvd a" |
|
1509 shows "normalize (a div b) = normalize a div normalize b" |
|
1510 proof - |
|
1511 from assms have "a = a div b * b" |
|
1512 by simp |
|
1513 then have "normalize a = normalize (a div b * b)" |
|
1514 by simp |
|
1515 then show ?thesis |
|
1516 by (cases "b = 0") (simp_all add: normalize_mult) |
|
1517 qed |
1495 qed |
1518 |
1496 |
1519 lemma normalize_dvd_iff [simp]: "normalize a dvd b \<longleftrightarrow> a dvd b" |
1497 lemma normalize_dvd_iff [simp]: "normalize a dvd b \<longleftrightarrow> a dvd b" |
1520 proof - |
1498 proof - |
1521 have "normalize a dvd b \<longleftrightarrow> unit_factor a * normalize a dvd b" |
1499 have "normalize a dvd b \<longleftrightarrow> unit_factor a * normalize a dvd b" |
1580 with False have "1 = c * d" |
1558 with False have "1 = c * d" |
1581 unfolding mult_cancel_left by simp |
1559 unfolding mult_cancel_left by simp |
1582 then have "is_unit c" and "is_unit d" |
1560 then have "is_unit c" and "is_unit d" |
1583 by auto |
1561 by auto |
1584 with a b show ?thesis |
1562 with a b show ?thesis |
1585 by (simp add: normalize_mult is_unit_normalize) |
1563 by (simp add: is_unit_normalize) |
1586 qed |
1564 qed |
1587 |
1565 |
1588 lemma associatedD1: "normalize a = normalize b \<Longrightarrow> a dvd b" |
1566 lemma associatedD1: "normalize a = normalize b \<Longrightarrow> a dvd b" |
1589 using dvd_normalize_iff [of _ b, symmetric] normalize_dvd_iff [of a _, symmetric] |
1567 using dvd_normalize_iff [of _ b, symmetric] normalize_dvd_iff [of a _, symmetric] |
1590 by simp |
1568 by simp |
1641 by simp |
1619 by simp |
1642 then show ?thesis |
1620 then show ?thesis |
1643 by simp |
1621 by simp |
1644 qed |
1622 qed |
1645 |
1623 |
1646 end |
1624 lemma normalize_mult_normalize_left [simp]: "normalize (normalize a * b) = normalize (a * b)" |
|
1625 by (rule associated_eqI) (auto intro!: mult_dvd_mono) |
|
1626 |
|
1627 lemma normalize_mult_normalize_right [simp]: "normalize (a * normalize b) = normalize (a * b)" |
|
1628 by (rule associated_eqI) (auto intro!: mult_dvd_mono) |
|
1629 |
|
1630 end |
|
1631 |
|
1632 |
|
1633 class normalization_semidom_multiplicative = normalization_semidom + |
|
1634 assumes unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b" |
|
1635 begin |
|
1636 |
|
1637 lemma normalize_mult: "normalize (a * b) = normalize a * normalize b" |
|
1638 proof (cases "a = 0 \<or> b = 0") |
|
1639 case True |
|
1640 then show ?thesis by auto |
|
1641 next |
|
1642 case False |
|
1643 have "unit_factor (a * b) * normalize (a * b) = a * b" |
|
1644 by (rule unit_factor_mult_normalize) |
|
1645 then have "normalize (a * b) = a * b div unit_factor (a * b)" |
|
1646 by simp |
|
1647 also have "\<dots> = a * b div unit_factor (b * a)" |
|
1648 by (simp add: ac_simps) |
|
1649 also have "\<dots> = a * b div unit_factor b div unit_factor a" |
|
1650 using False by (simp add: unit_factor_mult is_unit_div_mult2_eq [symmetric]) |
|
1651 also have "\<dots> = a * (b div unit_factor b) div unit_factor a" |
|
1652 using False by (subst unit_div_mult_swap) simp_all |
|
1653 also have "\<dots> = normalize a * normalize b" |
|
1654 using False |
|
1655 by (simp add: mult.commute [of a] mult.commute [of "normalize a"] unit_div_mult_swap [symmetric]) |
|
1656 finally show ?thesis . |
|
1657 qed |
|
1658 |
|
1659 lemma dvd_unit_factor_div: |
|
1660 assumes "b dvd a" |
|
1661 shows "unit_factor (a div b) = unit_factor a div unit_factor b" |
|
1662 proof - |
|
1663 from assms have "a = a div b * b" |
|
1664 by simp |
|
1665 then have "unit_factor a = unit_factor (a div b * b)" |
|
1666 by simp |
|
1667 then show ?thesis |
|
1668 by (cases "b = 0") (simp_all add: unit_factor_mult) |
|
1669 qed |
|
1670 |
|
1671 lemma dvd_normalize_div: |
|
1672 assumes "b dvd a" |
|
1673 shows "normalize (a div b) = normalize a div normalize b" |
|
1674 proof - |
|
1675 from assms have "a = a div b * b" |
|
1676 by simp |
|
1677 then have "normalize a = normalize (a div b * b)" |
|
1678 by simp |
|
1679 then show ?thesis |
|
1680 by (cases "b = 0") (simp_all add: normalize_mult) |
|
1681 qed |
|
1682 |
|
1683 end |
|
1684 |
|
1685 |
1647 |
1686 |
1648 |
1687 |
1649 text \<open>Syntactic division remainder operator\<close> |
1688 text \<open>Syntactic division remainder operator\<close> |
1650 |
1689 |
1651 class modulo = dvd + divide + |
1690 class modulo = dvd + divide + |