1.1 --- a/src/HOL/IntDiv.thy	Mon Feb 16 13:38:17 2009 +0100
     1.2 +++ b/src/HOL/IntDiv.thy	Mon Feb 16 19:11:15 2009 +0100
     1.3 @@ -377,6 +377,11 @@
     1.4  apply (blast intro: divmod_rel_div_mod [THEN zminus1_lemma, THEN divmod_rel_mod])
     1.5  done
     1.6  
     1.7 +lemma zmod_zminus1_not_zero:
     1.8 +  fixes k l :: int
     1.9 +  shows "- k mod l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
    1.10 +  unfolding zmod_zminus1_eq_if by auto
    1.11 +
    1.12  lemma zdiv_zminus2: "a div (-b) = (-a::int) div b"
    1.13  by (cut_tac a = "-a" in zdiv_zminus_zminus, auto)
    1.14  
    1.15 @@ -393,6 +398,11 @@
    1.16       "a mod (-b::int) = (if a mod b = 0 then 0 else  (a mod b) - b)"
    1.17  by (simp add: zmod_zminus1_eq_if zmod_zminus2)
    1.18  
    1.19 +lemma zmod_zminus2_not_zero:
    1.20 +  fixes k l :: int
    1.21 +  shows "k mod - l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
    1.22 +  unfolding zmod_zminus2_eq_if by auto 
    1.23 +
    1.24  
    1.25  subsection{*Division of a Number by Itself*}
    1.26  
    1.27 @@ -1523,6 +1533,40 @@
    1.28    thus  ?lhs by simp
    1.29  qed
    1.30  
    1.31 +
    1.32 +subsection {* Code generation *}
    1.33 +
    1.34 +definition pdivmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
    1.35 +  "pdivmod k l = (\<bar>k\<bar> div \<bar>l\<bar>, \<bar>k\<bar> mod \<bar>l\<bar>)"
    1.36 +
    1.37 +lemma pdivmod_posDivAlg [code]:
    1.38 +  "pdivmod k l = (if l = 0 then (0, \<bar>k\<bar>) else posDivAlg \<bar>k\<bar> \<bar>l\<bar>)"
    1.39 +by (subst posDivAlg_div_mod) (simp_all add: pdivmod_def)
    1.40 +
    1.41 +lemma divmod_pdivmod: "divmod k l = (if k = 0 then (0, 0) else if l = 0 then (0, k) else
    1.42 +  apsnd ((op *) (sgn l)) (if 0 < l \<and> 0 \<le> k \<or> l < 0 \<and> k < 0
    1.43 +    then pdivmod k l
    1.44 +    else (let (r, s) = pdivmod k l in
    1.45 +      if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))"
    1.46 +proof -
    1.47 +  have aux: "\<And>q::int. - k = l * q \<longleftrightarrow> k = l * - q" by auto
    1.48 +  show ?thesis
    1.49 +    by (simp add: divmod_mod_div pdivmod_def)
    1.50 +      (auto simp add: aux not_less not_le zdiv_zminus1_eq_if
    1.51 +      zmod_zminus1_eq_if zdiv_zminus2_eq_if zmod_zminus2_eq_if)
    1.52 +qed
    1.53 +
    1.54 +lemma divmod_code [code]: "divmod k l = (if k = 0 then (0, 0) else if l = 0 then (0, k) else
    1.55 +  apsnd ((op *) (sgn l)) (if sgn k = sgn l
    1.56 +    then pdivmod k l
    1.57 +    else (let (r, s) = pdivmod k l in
    1.58 +      if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))"
    1.59 +proof -
    1.60 +  have "k \<noteq> 0 \<Longrightarrow> l \<noteq> 0 \<Longrightarrow> 0 < l \<and> 0 \<le> k \<or> l < 0 \<and> k < 0 \<longleftrightarrow> sgn k = sgn l"
    1.61 +    by (auto simp add: not_less sgn_if)
    1.62 +  then show ?thesis by (simp add: divmod_pdivmod)
    1.63 +qed
    1.64 +
    1.65  code_modulename SML
    1.66    IntDiv Integer
    1.67