equal
deleted
inserted
replaced
18 and mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "mod" 70) |
18 and mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "mod" 70) |
19 |
19 |
20 |
20 |
21 subsection {* Abstract division in commutative semirings. *} |
21 subsection {* Abstract division in commutative semirings. *} |
22 |
22 |
23 class semiring_div = comm_semiring_1_cancel + div + |
23 class semiring_div = comm_semiring_1_cancel + div + |
24 assumes mod_div_equality: "a div b * b + a mod b = a" |
24 assumes mod_div_equality: "a div b * b + a mod b = a" |
25 and div_by_0 [simp]: "a div 0 = 0" |
25 and div_by_0 [simp]: "a div 0 = 0" |
26 and div_0 [simp]: "0 div a = 0" |
26 and div_0 [simp]: "0 div a = 0" |
27 and div_mult_self1 [simp]: "b \<noteq> 0 \<Longrightarrow> (a + c * b) div b = c + a div b" |
27 and div_mult_self1 [simp]: "b \<noteq> 0 \<Longrightarrow> (a + c * b) div b = c + a div b" |
28 begin |
28 begin |
798 unfolding dvd_def |
798 unfolding dvd_def |
799 by (force dest: mult_eq_self_implies_10 simp add: mult_assoc mult_eq_1_iff) |
799 by (force dest: mult_eq_self_implies_10 simp add: mult_assoc mult_eq_1_iff) |
800 |
800 |
801 text {* @{term "op dvd"} is a partial order *} |
801 text {* @{term "op dvd"} is a partial order *} |
802 |
802 |
803 class_interpretation dvd: order ["op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> m dvd n"] |
803 interpretation dvd!: order "op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> m dvd n" |
804 proof qed (auto intro: dvd_refl dvd_trans dvd_anti_sym) |
804 proof qed (auto intro: dvd_refl dvd_trans dvd_anti_sym) |
805 |
805 |
806 lemma dvd_diff: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)" |
806 lemma dvd_diff: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)" |
807 unfolding dvd_def |
807 unfolding dvd_def |
808 by (blast intro: diff_mult_distrib2 [symmetric]) |
808 by (blast intro: diff_mult_distrib2 [symmetric]) |