# HG changeset patch
# User haftmann
# Date 1234807875 -3600
# Node ID d3dfb67f0f59a55c72bb7bfec8c34325b9aa646e
# Parent  0f0f5fb297ec92952f60013fc190c057a2d6c167
added pdivmod on int (for code generation)

diff -r 0f0f5fb297ec -r d3dfb67f0f59 src/HOL/IntDiv.thy
--- a/src/HOL/IntDiv.thy	Mon Feb 16 13:38:17 2009 +0100
+++ b/src/HOL/IntDiv.thy	Mon Feb 16 19:11:15 2009 +0100
@@ -377,6 +377,11 @@
 apply (blast intro: divmod_rel_div_mod [THEN zminus1_lemma, THEN divmod_rel_mod])
 done
 
+lemma zmod_zminus1_not_zero:
+  fixes k l :: int
+  shows "- k mod l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
+  unfolding zmod_zminus1_eq_if by auto
+
 lemma zdiv_zminus2: "a div (-b) = (-a::int) div b"
 by (cut_tac a = "-a" in zdiv_zminus_zminus, auto)
 
@@ -393,6 +398,11 @@
      "a mod (-b::int) = (if a mod b = 0 then 0 else  (a mod b) - b)"
 by (simp add: zmod_zminus1_eq_if zmod_zminus2)
 
+lemma zmod_zminus2_not_zero:
+  fixes k l :: int
+  shows "k mod - l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
+  unfolding zmod_zminus2_eq_if by auto 
+
 
 subsection{*Division of a Number by Itself*}
 
@@ -1523,6 +1533,40 @@
   thus  ?lhs by simp
 qed
 
+
+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>)"
+
+lemma pdivmod_posDivAlg [code]:
+  "pdivmod k l = (if l = 0 then (0, \<bar>k\<bar>) else posDivAlg \<bar>k\<bar> \<bar>l\<bar>)"
+by (subst posDivAlg_div_mod) (simp_all add: pdivmod_def)
+
+lemma divmod_pdivmod: "divmod k l = (if k = 0 then (0, 0) else if l = 0 then (0, k) else
+  apsnd ((op *) (sgn l)) (if 0 < l \<and> 0 \<le> k \<or> l < 0 \<and> k < 0
+    then pdivmod k l
+    else (let (r, s) = pdivmod k l in
+      if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))"
+proof -
+  have aux: "\<And>q::int. - k = l * q \<longleftrightarrow> k = l * - q" by auto
+  show ?thesis
+    by (simp add: divmod_mod_div pdivmod_def)
+      (auto simp add: aux not_less not_le zdiv_zminus1_eq_if
+      zmod_zminus1_eq_if zdiv_zminus2_eq_if zmod_zminus2_eq_if)
+qed
+
+lemma divmod_code [code]: "divmod k l = (if k = 0 then (0, 0) else if l = 0 then (0, k) else
+  apsnd ((op *) (sgn l)) (if sgn k = sgn l
+    then pdivmod k l
+    else (let (r, s) = pdivmod k l in
+      if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))"
+proof -
+  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"
+    by (auto simp add: not_less sgn_if)
+  then show ?thesis by (simp add: divmod_pdivmod)
+qed
+
 code_modulename SML
   IntDiv Integer
 
diff -r 0f0f5fb297ec -r d3dfb67f0f59 src/HOL/Library/Code_Integer.thy
--- a/src/HOL/Library/Code_Integer.thy	Mon Feb 16 13:38:17 2009 +0100
+++ b/src/HOL/Library/Code_Integer.thy	Mon Feb 16 19:11:15 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Library/Code_Integer.thy
-    ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen
 *)
 
@@ -72,6 +71,11 @@
   (OCaml "Big'_int.mult'_big'_int")
   (Haskell infixl 7 "*")
 
+code_const pdivmod
+  (SML "(fn k => fn l =>/ IntInf.divMod/ (IntInf.abs k,/ IntInf.abs l))")
+  (OCaml "(fun k -> fun l ->/ Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int k)/ (Big'_int.abs'_big'_int l))")
+  (Haskell "(\\k l ->/ divMod/ (abs k)/ (abs l))")
+
 code_const "eq_class.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
   (SML "!((_ : IntInf.int) = _)")
   (OCaml "Big'_int.eq'_big'_int")