generalized euclidean ring prerequisites
authorhaftmann
Fri Jun 12 21:52:49 2015 +0200 (2015-06-12)
changeset 6043763edc650cf67
parent 60436 77e694c0c919
child 60438 e1c345094813
generalized euclidean ring prerequisites
src/HOL/Number_Theory/Euclidean_Algorithm.thy
     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"