author huffman Tue Mar 27 16:49:23 2012 +0200 (2012-03-27) changeset 47166 108bf76ca00c parent 47165 9344891b504b child 47167 099397de21e3
tuned proofs
 src/HOL/Divides.thy file | annotate | diff | revisions
```     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.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)