equal
deleted
inserted
replaced
209 then show ?thesis by (simp add: add_divide_distrib algebra_simps `d ~= 0`) |
209 then show ?thesis by (simp add: add_divide_distrib algebra_simps `d ~= 0`) |
210 qed |
210 qed |
211 |
211 |
212 lemma of_int_div: "(d::int) ~= 0 ==> d dvd n ==> |
212 lemma of_int_div: "(d::int) ~= 0 ==> d dvd n ==> |
213 (of_int(n div d)::'a::field_char_0) = of_int n / of_int d" |
213 (of_int(n div d)::'a::field_char_0) = of_int n / of_int d" |
214 apply (frule of_int_div_aux [of d n, where ?'a = 'a]) |
214 using of_int_div_aux [of d n, where ?'a = 'a] by simp |
215 apply simp |
|
216 apply (simp add: dvd_eq_mod_eq_0) |
|
217 done |
|
218 |
|
219 |
215 |
220 lemma normNum[simp]: "INum (normNum x) = (INum x :: 'a::{field_char_0, field_inverse_zero})" |
216 lemma normNum[simp]: "INum (normNum x) = (INum x :: 'a::{field_char_0, field_inverse_zero})" |
221 proof - |
217 proof - |
222 obtain a b where x: "x = (a, b)" by (cases x) |
218 obtain a b where x: "x = (a, b)" by (cases x) |
223 { assume "a = 0 \<or> b = 0" |
219 { assume "a = 0 \<or> b = 0" |