src/HOL/IntDiv.thy
changeset 33296 a3924d1069e5
parent 32960 69916a850301
child 33318 ddd97d9dfbfb
     1.1 --- a/src/HOL/IntDiv.thy	Wed Oct 28 17:44:03 2009 +0100
     1.2 +++ b/src/HOL/IntDiv.thy	Wed Oct 28 19:09:47 2009 +0100
     1.3 @@ -1318,6 +1318,36 @@
     1.4    thus  ?lhs by simp
     1.5  qed
     1.6  
     1.7 +lemma div_nat_number_of [simp]:
     1.8 +     "(number_of v :: nat)  div  number_of v' =  
     1.9 +          (if neg (number_of v :: int) then 0  
    1.10 +           else nat (number_of v div number_of v'))"
    1.11 +  unfolding nat_number_of_def number_of_is_id neg_def
    1.12 +  by (simp add: nat_div_distrib)
    1.13 +
    1.14 +lemma one_div_nat_number_of [simp]:
    1.15 +     "Suc 0 div number_of v' = nat (1 div number_of v')" 
    1.16 +by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric]) 
    1.17 +
    1.18 +lemma mod_nat_number_of [simp]:
    1.19 +     "(number_of v :: nat)  mod  number_of v' =  
    1.20 +        (if neg (number_of v :: int) then 0  
    1.21 +         else if neg (number_of v' :: int) then number_of v  
    1.22 +         else nat (number_of v mod number_of v'))"
    1.23 +  unfolding nat_number_of_def number_of_is_id neg_def
    1.24 +  by (simp add: nat_mod_distrib)
    1.25 +
    1.26 +lemma one_mod_nat_number_of [simp]:
    1.27 +     "Suc 0 mod number_of v' =  
    1.28 +        (if neg (number_of v' :: int) then Suc 0
    1.29 +         else nat (1 mod number_of v'))"
    1.30 +by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric]) 
    1.31 +
    1.32 +lemmas dvd_eq_mod_eq_0_number_of =
    1.33 +  dvd_eq_mod_eq_0 [of "number_of x" "number_of y", standard]
    1.34 +
    1.35 +declare dvd_eq_mod_eq_0_number_of [simp]
    1.36 +
    1.37  
    1.38  subsection {* Code generation *}
    1.39