src/HOL/IntDiv.thy

   assume ?rhs then obtain q1 q2 where q12: "x + n * q1 = y + n * q2" by blast
   hence "(x + n * q1) mod n = (y + n * q2) mod n" by simp
   thus  ?lhs by simp
 qed
 
+lemma div_nat_number_of [simp]:
+     "(number_of v :: nat)  div  number_of v' =  
+          (if neg (number_of v :: int) then 0  
+           else nat (number_of v div number_of v'))"
+  unfolding nat_number_of_def number_of_is_id neg_def
+  by (simp add: nat_div_distrib)
+
+lemma one_div_nat_number_of [simp]:
+     "Suc 0 div number_of v' = nat (1 div number_of v')" 
+by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric]) 
+
+lemma mod_nat_number_of [simp]:
+     "(number_of v :: nat)  mod  number_of v' =  
+        (if neg (number_of v :: int) then 0  
+         else if neg (number_of v' :: int) then number_of v  
+         else nat (number_of v mod number_of v'))"
+  unfolding nat_number_of_def number_of_is_id neg_def
+  by (simp add: nat_mod_distrib)
+
+lemma one_mod_nat_number_of [simp]:
+     "Suc 0 mod number_of v' =  
+        (if neg (number_of v' :: int) then Suc 0
+         else nat (1 mod number_of v'))"
+by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric]) 
+
+lemmas dvd_eq_mod_eq_0_number_of =
+  dvd_eq_mod_eq_0 [of "number_of x" "number_of y", standard]
+
+declare dvd_eq_mod_eq_0_number_of [simp]
+
 
 subsection {* Code generation *}
 
 definition pdivmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
   "pdivmod k l = (\<bar>k\<bar> div \<bar>l\<bar>, \<bar>k\<bar> mod \<bar>l\<bar>)"