src/HOL/Divides.thy
changeset 60353 838025c6e278
parent 60352 d46de31a50c4
child 60429 d3d1e185cd63
     1.1 --- a/src/HOL/Divides.thy	Mon Jun 01 18:59:21 2015 +0200
     1.2 +++ b/src/HOL/Divides.thy	Mon Jun 01 18:59:22 2015 +0200
     1.3 @@ -31,7 +31,13 @@
     1.4      and div_mult_mult1 [simp]: "c \<noteq> 0 \<Longrightarrow> (c * a) div (c * b) = a div b"
     1.5  begin
     1.6  
     1.7 -subclass semiring_no_zero_divisors ..
     1.8 +subclass semidom_divide
     1.9 +proof
    1.10 +  fix b a
    1.11 +  assume "b \<noteq> 0"
    1.12 +  then show "a * b div b = a"
    1.13 +    using div_mult_self1 [of b 0 a] by (simp add: ac_simps)
    1.14 +qed simp
    1.15  
    1.16  lemma power_not_zero: -- \<open>FIXME cf. @{text field_power_not_zero}\<close>
    1.17    "a \<noteq> 0 \<Longrightarrow> a ^ n \<noteq> 0"
    1.18 @@ -107,11 +113,13 @@
    1.19    "(b * c + a) mod b = a mod b"
    1.20    by (simp add: add.commute)
    1.21  
    1.22 -lemma div_mult_self1_is_id [simp]: "b \<noteq> 0 \<Longrightarrow> b * a div b = a"
    1.23 -  using div_mult_self2 [of b 0 a] by simp
    1.24 -
    1.25 -lemma div_mult_self2_is_id [simp]: "b \<noteq> 0 \<Longrightarrow> a * b div b = a"
    1.26 -  using div_mult_self1 [of b 0 a] by simp
    1.27 +lemma div_mult_self1_is_id:
    1.28 +  "b \<noteq> 0 \<Longrightarrow> b * a div b = a"
    1.29 +  by (fact nonzero_mult_divide_cancel_left)
    1.30 +
    1.31 +lemma div_mult_self2_is_id:
    1.32 +  "b \<noteq> 0 \<Longrightarrow> a * b div b = a"
    1.33 +  by (fact nonzero_mult_divide_cancel_right)
    1.34  
    1.35  lemma mod_mult_self1_is_0 [simp]: "b * a mod b = 0"
    1.36    using mod_mult_self2 [of 0 b a] by simp
    1.37 @@ -439,21 +447,21 @@
    1.38  next
    1.39    assume "b div a = c"
    1.40    then have "b div a * a = c * a" by simp
    1.41 -  moreover from `a dvd b` have "b div a * a = b" by (simp add: dvd_div_mult_self)
    1.42 +  moreover from `a dvd b` have "b div a * a = b" by simp
    1.43    ultimately show "b = c * a" by simp
    1.44  qed
    1.45     
    1.46  lemma dvd_div_div_eq_mult:
    1.47    assumes "a \<noteq> 0" "c \<noteq> 0" and "a dvd b" "c dvd d"
    1.48    shows "b div a = d div c \<longleftrightarrow> b * c = a * d"
    1.49 -  using assms by (auto simp add: mult.commute [of _ a] dvd_div_mult_self dvd_div_eq_mult div_mult_swap intro: sym)
    1.50 +  using assms by (auto simp add: mult.commute [of _ a] dvd_div_eq_mult div_mult_swap intro: sym)
    1.51  
    1.52  end
    1.53  
    1.54  class ring_div = comm_ring_1 + semiring_div
    1.55  begin
    1.56  
    1.57 -subclass idom ..
    1.58 +subclass idom_divide ..
    1.59  
    1.60  text {* Negation respects modular equivalence. *}
    1.61