# HG changeset patch
# User haftmann
# Date 1376832590 -7200
# Node ID d165213e3924c07c80294de465707748d829bbd0
# Parent  41fc65da66f1b2d7c043282f63b9f95558fa0616
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs

diff -r 41fc65da66f1 -r d165213e3924 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Sun Aug 18 15:29:50 2013 +0200
+++ b/src/HOL/Code_Numeral.thy	Sun Aug 18 15:29:50 2013 +0200
@@ -223,6 +223,21 @@
   "of_nat (nat_of_integer k) = max 0 k"
   by transfer auto
 
+instance integer :: semiring_numeral_div
+  by intro_classes (transfer,
+    fact semiring_numeral_div_class.diff_invert_add1
+    semiring_numeral_div_class.le_add_diff_inverse2
+    semiring_numeral_div_class.mult_div_cancel
+    semiring_numeral_div_class.div_less
+    semiring_numeral_div_class.mod_less
+    semiring_numeral_div_class.div_positive
+    semiring_numeral_div_class.mod_less_eq_dividend
+    semiring_numeral_div_class.pos_mod_bound
+    semiring_numeral_div_class.pos_mod_sign
+    semiring_numeral_div_class.mod_mult2_eq
+    semiring_numeral_div_class.div_mult2_eq
+    semiring_numeral_div_class.discrete)+
+
 
 subsection {* Code theorems for target language integers *}
 
@@ -347,24 +362,15 @@
   "snd (divmod_abs k l) = \<bar>k\<bar> mod \<bar>l\<bar>"
   by (simp add: divmod_abs_def)
 
-lemma divmod_abs_terminate_code [code]:
-  "divmod_abs (Neg k) (Neg l) = divmod_abs (Pos k) (Pos l)"
-  "divmod_abs (Neg k) (Pos l) = divmod_abs (Pos k) (Pos l)"
-  "divmod_abs (Pos k) (Neg l) = divmod_abs (Pos k) (Pos l)"
+lemma divmod_abs_code [code]:
+  "divmod_abs (Pos k) (Pos l) = divmod k l"
+  "divmod_abs (Neg k) (Neg l) = divmod k l"
+  "divmod_abs (Neg k) (Pos l) = divmod k l"
+  "divmod_abs (Pos k) (Neg l) = divmod k l"
   "divmod_abs j 0 = (0, \<bar>j\<bar>)"
   "divmod_abs 0 j = (0, 0)"
   by (simp_all add: prod_eq_iff)
 
-lemma divmod_abs_rec_code [code]:
-  "divmod_abs (Pos k) (Pos l) =
-    (let j = sub k l in
-       if j < 0 then (0, Pos k)
-       else let (q, r) = divmod_abs j (Pos l) in (q + 1, r))"
-  apply (simp add: prod_eq_iff Let_def prod_case_beta)
-  apply transfer
-  apply (simp add: sub_non_negative sub_negative div_pos_pos_trivial mod_pos_pos_trivial div_pos_geq mod_pos_geq)
-  done
-
 lemma divmod_integer_code [code]:
   "divmod_integer k l =
     (if k = 0 then (0, 0) else if l = 0 then (0, k) else
diff -r 41fc65da66f1 -r d165213e3924 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sun Aug 18 15:29:50 2013 +0200
+++ b/src/HOL/Divides.thy	Sun Aug 18 15:29:50 2013 +0200
@@ -660,6 +660,19 @@
   with False show ?thesis by simp
 qed
 
+lemma divmod_cancel [code]:
+  "divmod (Num.Bit0 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r))" (is ?P)
+  "divmod (Num.Bit1 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r + 1))" (is ?Q)
+proof -
+  have *: "\<And>q. numeral (Num.Bit0 q) = 2 * numeral q"
+    "\<And>q. numeral (Num.Bit1 q) = 2 * numeral q + 1"
+    by (simp_all only: numeral_mult numeral.simps distrib) simp_all
+  have "1 div 2 = 0" "1 mod 2 = 1" by (auto intro: div_less mod_less)
+  then show ?P and ?Q
+    by (simp_all add: prod_eq_iff split_def * [of m] * [of n] mod_mult_mult1
+      div_mult2_eq [of _ _ 2] mod_mult2_eq [of _ _ 2] add.commute del: numeral_times_numeral)
+ qed
+
 end
 
 hide_fact (open) diff_invert_add1 le_add_diff_inverse2 diff_zero
@@ -1846,7 +1859,11 @@
   by (rule mod_int_unique [of a b q r],
     simp add: divmod_int_rel_def)
 
-(* simprocs adapted from HOL/ex/Binary.thy *)
+text {*
+  numeral simprocs -- high chance that these can be replaced
+  by divmod algorithm from @{class semiring_numeral_div}
+*}
+
 ML {*
 local
   val mk_number = HOLogic.mk_number HOLogic.intT
@@ -2573,37 +2590,55 @@
 
 subsubsection {* 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_int_pdivmod: "divmod_int k l = (if k = 0 then (0, 0) else if l = 0 then (0, k) else
+definition divmod_abs :: "int \<Rightarrow> int \<Rightarrow> int \<times> int"
+where
+  "divmod_abs k l = (\<bar>k\<bar> div \<bar>l\<bar>, \<bar>k\<bar> mod \<bar>l\<bar>)"
+
+lemma fst_divmod_abs [simp]:
+  "fst (divmod_abs k l) = \<bar>k\<bar> div \<bar>l\<bar>"
+  by (simp add: divmod_abs_def)
+
+lemma snd_divmod_abs [simp]:
+  "snd (divmod_abs k l) = \<bar>k\<bar> mod \<bar>l\<bar>"
+  by (simp add: divmod_abs_def)
+
+lemma divmod_abs_code [code]:
+  "divmod_abs (Int.Pos k) (Int.Pos l) = divmod k l"
+  "divmod_abs (Int.Neg k) (Int.Neg l) = divmod k l"
+  "divmod_abs (Int.Neg k) (Int.Pos l) = divmod k l"
+  "divmod_abs (Int.Pos k) (Int.Neg l) = divmod k l"
+  "divmod_abs j 0 = (0, \<bar>j\<bar>)"
+  "divmod_abs 0 j = (0, 0)"
+  by (simp_all add: prod_eq_iff)
+
+lemma divmod_int_divmod_abs:
+  "divmod_int 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
+    then divmod_abs k l
+    else (let (r, s) = divmod_abs 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_int_mod_div pdivmod_def)
+    by (simp add: prod_eq_iff split_def Let_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_int_code [code]: "divmod_int k l = (if k = 0 then (0, 0) else if l = 0 then (0, k) else
+lemma divmod_int_code [code]:
+  "divmod_int 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
+    then divmod_abs k l
+    else (let (r, s) = divmod_abs 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_int_pdivmod)
+  then show ?thesis by (simp add: divmod_int_divmod_abs)
 qed
 
+hide_const (open) divmod_abs
+
 code_identifier
   code_module Divides \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
 
diff -r 41fc65da66f1 -r d165213e3924 src/HOL/Library/Code_Binary_Nat.thy
--- a/src/HOL/Library/Code_Binary_Nat.thy	Sun Aug 18 15:29:50 2013 +0200
+++ b/src/HOL/Library/Code_Binary_Nat.thy	Sun Aug 18 15:29:50 2013 +0200
@@ -130,6 +130,15 @@
   "nat_of_num k < nat_of_num l \<longleftrightarrow> k < l"
   by (simp_all add: nat_of_num_numeral)
 
+lemma [code, code del]:
+  "divmod_nat = divmod_nat" ..
+  
+lemma divmod_nat_code [code]:
+  "divmod_nat (nat_of_num k) (nat_of_num l) = divmod k l"
+  "divmod_nat m 0 = (0, m)"
+  "divmod_nat 0 n = (0, 0)"
+  by (simp_all add: prod_eq_iff nat_of_num_numeral del: div_nat_numeral mod_nat_numeral)
+
 
 subsection {* Conversions *}
 
diff -r 41fc65da66f1 -r d165213e3924 src/HOL/Library/Code_Target_Int.thy
--- a/src/HOL/Library/Code_Target_Int.thy	Sun Aug 18 15:29:50 2013 +0200
+++ b/src/HOL/Library/Code_Target_Int.thy	Sun Aug 18 15:29:50 2013 +0200
@@ -65,9 +65,9 @@
   by simp
 
 lemma [code]:
-  "pdivmod k l = map_pair int_of_integer int_of_integer
+  "Divides.divmod_abs k l = map_pair int_of_integer int_of_integer
     (Code_Numeral.divmod_abs (of_int k) (of_int l))"
-  by (simp add: prod_eq_iff pdivmod_def)
+  by (simp add: prod_eq_iff)
 
 lemma [code]:
   "k div l = int_of_integer (of_int k div of_int l)"