src/HOL/Divides.thy
changeset 64240 eabf80376aab
parent 64238 b60a9752b6d0
child 64242 93c6f0da5c70
     1.1 --- a/src/HOL/Divides.thy	Sun Oct 16 09:31:03 2016 +0200
     1.2 +++ b/src/HOL/Divides.thy	Sun Oct 16 09:31:04 2016 +0200
     1.3 @@ -26,18 +26,6 @@
     1.4      using div_mult_self1 [of b 0 a] by (simp add: ac_simps div_0)
     1.5  qed (simp add: div_by_0)
     1.6  
     1.7 -lemma div_by_1:
     1.8 -  "a div 1 = a"
     1.9 -  by (fact divide_1)
    1.10 -
    1.11 -lemma div_mult_self1_is_id:
    1.12 -  "b \<noteq> 0 \<Longrightarrow> b * a div b = a"
    1.13 -  by (fact nonzero_mult_divide_cancel_left)
    1.14 -
    1.15 -lemma div_mult_self2_is_id:
    1.16 -  "b \<noteq> 0 \<Longrightarrow> a * b div b = a"
    1.17 -  by (fact nonzero_mult_divide_cancel_right)
    1.18 -
    1.19  text \<open>@{const divide} and @{const modulo}\<close>
    1.20  
    1.21  lemma div_mod_equality: "((a div b) * b + a mod b) + c = a + c"
    1.22 @@ -412,7 +400,7 @@
    1.23  apply (auto simp add: dvd_def)
    1.24  apply (subgoal_tac "-(y * k) = y * - k")
    1.25   apply (simp only:)
    1.26 - apply (erule div_mult_self1_is_id)
    1.27 + apply (erule nonzero_mult_div_cancel_left)
    1.28  apply simp
    1.29  done
    1.30  
    1.31 @@ -420,7 +408,7 @@
    1.32  apply (case_tac "y = 0") apply simp
    1.33  apply (auto simp add: dvd_def)
    1.34  apply (subgoal_tac "y * k = -y * -k")
    1.35 - apply (erule ssubst, rule div_mult_self1_is_id)
    1.36 + apply (erule ssubst, rule nonzero_mult_div_cancel_left)
    1.37   apply simp
    1.38  apply simp
    1.39  done
    1.40 @@ -1817,7 +1805,7 @@
    1.41      by (cases "0::int" k rule: linorder_cases) simp_all
    1.42    then show "is_unit (unit_factor k)"
    1.43      by simp
    1.44 -qed (simp_all add: sgn_times mult_sgn_abs)
    1.45 +qed (simp_all add: sgn_mult mult_sgn_abs)
    1.46    
    1.47  end
    1.48    
    1.49 @@ -2707,4 +2695,6 @@
    1.50    "numeral x dvd (numeral y :: 'a) \<longleftrightarrow> numeral y mod numeral x = (0 :: 'a::semiring_div)"
    1.51    by (fact dvd_eq_mod_eq_0)
    1.52  
    1.53 +hide_fact (open) div_0 div_by_0
    1.54 +
    1.55  end