1.1 --- a/src/HOL/Divides.thy	Tue Mar 27 19:21:05 2012 +0200
     1.2 +++ b/src/HOL/Divides.thy	Tue Mar 27 16:49:23 2012 +0200
     1.3 @@ -1983,44 +1983,30 @@
     1.4  declare split_zmod [of _ _ "numeral k", arith_split] for k
     1.5  
     1.6  
     1.7 -subsubsection {* Speeding up the Division Algorithm with Shifting *}
     1.8 +subsubsection {* Computing @{text "div"} and @{text "mod"} with shifting *}
     1.9 +
    1.10 +lemma pos_divmod_int_rel_mult_2:
    1.11 +  assumes "0 \<le> b"
    1.12 +  assumes "divmod_int_rel a b (q, r)"
    1.13 +  shows "divmod_int_rel (1 + 2*a) (2*b) (q, 1 + 2*r)"
    1.14 +  using assms unfolding divmod_int_rel_def by auto
    1.15 +
    1.16 +lemma neg_divmod_int_rel_mult_2:
    1.17 +  assumes "b \<le> 0"
    1.18 +  assumes "divmod_int_rel (a + 1) b (q, r)"
    1.19 +  shows "divmod_int_rel (1 + 2*a) (2*b) (q, 2*r - 1)"
    1.20 +  using assms unfolding divmod_int_rel_def by auto
    1.21  
    1.22  text{*computing div by shifting *}
    1.23  
    1.24  lemma pos_zdiv_mult_2: "(0::int) \<le> a ==> (1 + 2*b) div (2*a) = b div a"
    1.25 -proof cases
    1.26 -  assume "a=0"
    1.27 -    thus ?thesis by simp
    1.28 -next
    1.29 -  assume "a\<noteq>0" and le_a: "0\<le>a"   
    1.30 -  hence a_pos: "1 \<le> a" by arith
    1.31 -  hence one_less_a2: "1 < 2 * a" by arith
    1.32 -  hence le_2a: "2 * (1 + b mod a) \<le> 2 * a"
    1.33 -    unfolding mult_le_cancel_left
    1.34 -    by (simp add: add1_zle_eq add_commute [of 1])
    1.35 -  with a_pos have "0 \<le> b mod a" by simp
    1.36 -  hence le_addm: "0 \<le> 1 mod (2*a) + 2*(b mod a)"
    1.37 -    by (simp add: mod_pos_pos_trivial one_less_a2)
    1.38 -  with  le_2a
    1.39 -  have "(1 mod (2*a) + 2*(b mod a)) div (2*a) = 0"
    1.40 -    by (simp add: div_pos_pos_trivial le_addm mod_pos_pos_trivial one_less_a2
    1.41 -                  right_distrib) 
    1.42 -  thus ?thesis
    1.43 -    by (subst zdiv_zadd1_eq,
    1.44 -        simp add: mod_mult_mult1 one_less_a2
    1.45 -                  div_pos_pos_trivial)
    1.46 -qed
    1.47 +  using pos_divmod_int_rel_mult_2 [OF _ divmod_int_rel_div_mod]
    1.48 +  by (rule div_int_unique)
    1.49  
    1.50  lemma neg_zdiv_mult_2: 
    1.51    assumes A: "a \<le> (0::int)" shows "(1 + 2*b) div (2*a) = (b+1) div a"
    1.52 -proof -
    1.53 -  have R: "1 + - (2 * (b + 1)) = - (1 + 2 * b)" by simp
    1.54 -  have "(1 + 2 * (-b - 1)) div (2 * (-a)) = (-b - 1) div (-a)"
    1.55 -    by (rule pos_zdiv_mult_2, simp add: A)
    1.56 -  thus ?thesis
    1.57 -    by (simp only: R div_minus_minus diff_minus
    1.58 -      minus_add_distrib [symmetric] mult_minus_right)
    1.59 -qed
    1.60 +  using neg_divmod_int_rel_mult_2 [OF A divmod_int_rel_div_mod]
    1.61 +  by (rule div_int_unique)
    1.62  
    1.63  (* FIXME: add rules for negative numerals *)
    1.64  lemma zdiv_numeral_Bit0 [simp]:
    1.65 @@ -2036,39 +2022,19 @@
    1.66    unfolding mult_2 [symmetric] add_commute [of _ 1]
    1.67    by (rule pos_zdiv_mult_2, simp)
    1.68  
    1.69 -
    1.70 -subsubsection {* Computing mod by Shifting (proofs resemble those for div) *}
    1.71 -
    1.72  lemma pos_zmod_mult_2:
    1.73    fixes a b :: int
    1.74    assumes "0 \<le> a"
    1.75    shows "(1 + 2 * b) mod (2 * a) = 1 + 2 * (b mod a)"
    1.76 -proof (cases "0 < a")
    1.77 -  case False with assms show ?thesis by simp
    1.78 -next
    1.79 -  case True
    1.80 -  then have "b mod a < a" by (rule pos_mod_bound)
    1.81 -  then have "1 + b mod a \<le> a" by simp
    1.82 -  then have A: "2 * (1 + b mod a) \<le> 2 * a" by simp
    1.83 -  from `0 < a` have "0 \<le> b mod a" by (rule pos_mod_sign)
    1.84 -  then have B: "0 \<le> 1 + 2 * (b mod a)" by simp
    1.85 -  have "((1\<Colon>int) mod ((2\<Colon>int) * a) + (2\<Colon>int) * b mod ((2\<Colon>int) * a)) mod ((2\<Colon>int) * a) = (1\<Colon>int) + (2\<Colon>int) * (b mod a)"
    1.86 -    using `0 < a` and A
    1.87 -    by (auto simp add: mod_mult_mult1 mod_pos_pos_trivial ring_distribs intro!: mod_pos_pos_trivial B)
    1.88 -  then show ?thesis by (subst mod_add_eq)
    1.89 -qed
    1.90 +  using pos_divmod_int_rel_mult_2 [OF assms divmod_int_rel_div_mod]
    1.91 +  by (rule mod_int_unique)
    1.92  
    1.93  lemma neg_zmod_mult_2:
    1.94    fixes a b :: int
    1.95    assumes "a \<le> 0"
    1.96    shows "(1 + 2 * b) mod (2 * a) = 2 * ((b + 1) mod a) - 1"
    1.97 -proof -
    1.98 -  from assms have "0 \<le> - a" by auto
    1.99 -  then have "(1 + 2 * (- b - 1)) mod (2 * (- a)) = 1 + 2 * ((- b - 1) mod (- a))"
   1.100 -    by (rule pos_zmod_mult_2)
   1.101 -  then show ?thesis by (simp add: mod_minus_right algebra_simps)
   1.102 -     (simp add: diff_minus add_ac)
   1.103 -qed
   1.104 +  using neg_divmod_int_rel_mult_2 [OF assms divmod_int_rel_div_mod]
   1.105 +  by (rule mod_int_unique)
   1.106  
   1.107  (* FIXME: add rules for negative numerals *)
   1.108  lemma zmod_numeral_Bit0 [simp]: