1.1 --- a/src/HOL/IntDiv.thy	Sat Feb 16 16:52:09 2008 +0100
     1.2 +++ b/src/HOL/IntDiv.thy	Sun Feb 17 06:49:53 2008 +0100
     1.3 @@ -1062,14 +1062,18 @@
     1.4  lemma not_0_le_lemma: "~ 0 \<le> x ==> x \<le> (0::int)"
     1.5  by auto
     1.6  
     1.7 -lemma zdiv_number_of_BIT[simp]:
     1.8 -     "number_of (v BIT b) div number_of (w BIT bit.B0) =  
     1.9 -          (if b=bit.B0 | (0::int) \<le> number_of w                    
    1.10 +lemma zdiv_number_of_Bit0 [simp]:
    1.11 +     "number_of (Int.Bit0 v) div number_of (Int.Bit0 w) =  
    1.12 +          number_of v div (number_of w :: int)"
    1.13 +by (simp only: number_of_eq numeral_simps) simp
    1.14 +
    1.15 +lemma zdiv_number_of_Bit1 [simp]:
    1.16 +     "number_of (Int.Bit1 v) div number_of (Int.Bit0 w) =  
    1.17 +          (if (0::int) \<le> number_of w                    
    1.18             then number_of v div (number_of w)     
    1.19             else (number_of v + (1::int)) div (number_of w))"
    1.20  apply (simp only: number_of_eq numeral_simps UNIV_I split: split_if) 
    1.21 -apply (simp add: zdiv_zmult_zmult1 pos_zdiv_mult_2 neg_zdiv_mult_2 add_ac 
    1.22 -            split: bit.split)
    1.23 +apply (simp add: zdiv_zmult_zmult1 pos_zdiv_mult_2 neg_zdiv_mult_2 add_ac)
    1.24  done
    1.25  
    1.26  
    1.27 @@ -1087,7 +1091,7 @@
    1.28  apply (subst zmod_zadd1_eq)
    1.29  apply (simp add: zmod_zmult_zmult2 mod_pos_pos_trivial)
    1.30  apply (rule mod_pos_pos_trivial)
    1.31 -apply (auto simp add: mod_pos_pos_trivial left_distrib)
    1.32 +apply (auto simp add: mod_pos_pos_trivial ring_distribs)
    1.33  apply (subgoal_tac "0 \<le> b mod a", arith, simp)
    1.34  done
    1.35  
    1.36 @@ -1102,14 +1106,20 @@
    1.37  apply (simp only: zmod_zminus_zminus diff_minus minus_add_distrib [symmetric])
    1.38  done
    1.39  
    1.40 -lemma zmod_number_of_BIT [simp]:
    1.41 -     "number_of (v BIT b) mod number_of (w BIT bit.B0) =  
    1.42 -      (case b of
    1.43 -          bit.B0 => 2 * (number_of v mod number_of w)
    1.44 -        | bit.B1 => if (0::int) \<le> number_of w  
    1.45 +lemma zmod_number_of_Bit0 [simp]:
    1.46 +     "number_of (Int.Bit0 v) mod number_of (Int.Bit0 w) =  
    1.47 +      (2::int) * (number_of v mod number_of w)"
    1.48 +apply (simp only: number_of_eq numeral_simps) 
    1.49 +apply (simp add: zmod_zmult_zmult1 pos_zmod_mult_2 
    1.50 +                 not_0_le_lemma neg_zmod_mult_2 add_ac)
    1.51 +done
    1.52 +
    1.53 +lemma zmod_number_of_Bit1 [simp]:
    1.54 +     "number_of (Int.Bit1 v) mod number_of (Int.Bit0 w) =  
    1.55 +      (if (0::int) \<le> number_of w  
    1.56                  then 2 * (number_of v mod number_of w) + 1     
    1.57                  else 2 * ((number_of v + (1::int)) mod number_of w) - 1)"
    1.58 -apply (simp only: number_of_eq numeral_simps UNIV_I split: bit.split) 
    1.59 +apply (simp only: number_of_eq numeral_simps) 
    1.60  apply (simp add: zmod_zmult_zmult1 pos_zmod_mult_2 
    1.61                   not_0_le_lemma neg_zmod_mult_2 add_ac)
    1.62  done