equal
deleted
inserted
replaced
129 moreover have "a div b = a div b" .. |
129 moreover have "a div b = a div b" .. |
130 moreover have "a mod b = a mod b" .. |
130 moreover have "a mod b = a mod b" .. |
131 note that ultimately show thesis by blast |
131 note that ultimately show thesis by blast |
132 qed |
132 qed |
133 |
133 |
134 lemma dvd_eq_mod_eq_0 [code_unfold]: "a dvd b \<longleftrightarrow> b mod a = 0" |
134 lemma dvd_eq_mod_eq_0 [code, code_unfold, code_inline del]: "a dvd b \<longleftrightarrow> b mod a = 0" |
135 proof |
135 proof |
136 assume "b mod a = 0" |
136 assume "b mod a = 0" |
137 with mod_div_equality [of b a] have "b div a * a = b" by simp |
137 with mod_div_equality [of b a] have "b div a * a = b" by simp |
138 then have "b = a * (b div a)" unfolding mult_commute .. |
138 then have "b = a * (b div a)" unfolding mult_commute .. |
139 then have "\<exists>c. b = a * c" .. |
139 then have "\<exists>c. b = a * c" .. |
2458 have "k \<noteq> 0 \<Longrightarrow> l \<noteq> 0 \<Longrightarrow> 0 < l \<and> 0 \<le> k \<or> l < 0 \<and> k < 0 \<longleftrightarrow> sgn k = sgn l" |
2458 have "k \<noteq> 0 \<Longrightarrow> l \<noteq> 0 \<Longrightarrow> 0 < l \<and> 0 \<le> k \<or> l < 0 \<and> k < 0 \<longleftrightarrow> sgn k = sgn l" |
2459 by (auto simp add: not_less sgn_if) |
2459 by (auto simp add: not_less sgn_if) |
2460 then show ?thesis by (simp add: divmod_int_pdivmod) |
2460 then show ?thesis by (simp add: divmod_int_pdivmod) |
2461 qed |
2461 qed |
2462 |
2462 |
|
2463 code_modulename SML |
|
2464 Divides Arith |
|
2465 |
|
2466 code_modulename OCaml |
|
2467 Divides Arith |
|
2468 |
|
2469 code_modulename Haskell |
|
2470 Divides Arith |
|
2471 |
2463 end |
2472 end |