author haftmann Fri Jun 12 21:52:49 2015 +0200 (2015-06-12) changeset 60437 63edc650cf67 parent 60436 77e694c0c919 child 60438 e1c345094813
generalized euclidean ring prerequisites
```     1.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Fri Jun 12 21:52:48 2015 +0200
1.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Fri Jun 12 21:52:49 2015 +0200
1.3 @@ -29,9 +29,40 @@
1.4
1.5  end
1.6
1.7 -context semiring_div
1.8 +context semidom_divide
1.9  begin
1.10 +
1.11 +lemma div_self [simp]:
1.12 +  assumes "a \<noteq> 0"
1.13 +  shows "a div a = 1"
1.14 +  using assms nonzero_mult_divide_cancel_left [of a 1] by simp
1.15
1.16 +lemma dvd_div_mult_self [simp]:
1.17 +  "a dvd b \<Longrightarrow> b div a * a = b"
1.18 +  by (cases "a = 0") (auto elim: dvdE simp add: ac_simps)
1.19 +
1.20 +lemma dvd_mult_div_cancel [simp]:
1.21 +  "a dvd b \<Longrightarrow> a * (b div a) = b"
1.22 +  using dvd_div_mult_self [of a b] by (simp add: ac_simps)
1.23 +
1.24 +lemma div_mult_swap:
1.25 +  assumes "c dvd b"
1.26 +  shows "a * (b div c) = (a * b) div c"
1.27 +proof (cases "c = 0")
1.28 +  case True then show ?thesis by simp
1.29 +next
1.30 +  case False from assms obtain d where "b = c * d" ..
1.31 +  moreover from False have "a * divide (d * c) c = ((a * d) * c) div c"
1.32 +    by simp
1.33 +  ultimately show ?thesis by (simp add: ac_simps)
1.34 +qed
1.35 +
1.36 +lemma dvd_div_mult:
1.37 +  assumes "c dvd b"
1.38 +  shows "b div c * a = (b * a) div c"
1.39 +  using assms div_mult_swap [of c b a] by (simp add: ac_simps)
1.40 +
1.41 +
1.42  text \<open>Units: invertible elements in a ring\<close>
1.43
1.44  abbreviation is_unit :: "'a \<Rightarrow> bool"
```