src/HOL/Divides.thy
changeset 34126 8a2c5d7aff51
parent 33804 39b494e8c055
child 34225 21c5405deb6b
     1.1 --- a/src/HOL/Divides.thy	Thu Dec 17 15:22:27 2009 +0100
     1.2 +++ b/src/HOL/Divides.thy	Fri Dec 18 12:00:29 2009 +0100
     1.3 @@ -2443,6 +2443,17 @@
     1.4  declare dvd_eq_mod_eq_0_number_of [simp]
     1.5  
     1.6  
     1.7 +subsubsection {* Nitpick *}
     1.8 +
     1.9 +lemma zmod_zdiv_equality':
    1.10 +"(m\<Colon>int) mod n = m - (m div n) * n"
    1.11 +by (rule_tac P="%x. m mod n = x - (m div n) * n"
    1.12 +    in subst [OF mod_div_equality [of _ n]])
    1.13 +   arith
    1.14 +
    1.15 +lemmas [nitpick_def] = mod_div_equality' [THEN eq_reflection]
    1.16 +                       zmod_zdiv_equality' [THEN eq_reflection]
    1.17 +
    1.18  subsubsection {* Code generation *}
    1.19  
    1.20  definition pdivmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where