execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
authorhaftmann
Sun Aug 18 15:29:50 2013 +0200 (2013-08-18)
changeset 53069d165213e3924
parent 53068 41fc65da66f1
child 53070 6a3410845bb2
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
src/HOL/Code_Numeral.thy
src/HOL/Divides.thy
src/HOL/Library/Code_Binary_Nat.thy
src/HOL/Library/Code_Target_Int.thy
     1.1 --- a/src/HOL/Code_Numeral.thy	Sun Aug 18 15:29:50 2013 +0200
     1.2 +++ b/src/HOL/Code_Numeral.thy	Sun Aug 18 15:29:50 2013 +0200
     1.3 @@ -223,6 +223,21 @@
     1.4    "of_nat (nat_of_integer k) = max 0 k"
     1.5    by transfer auto
     1.6  
     1.7 +instance integer :: semiring_numeral_div
     1.8 +  by intro_classes (transfer,
     1.9 +    fact semiring_numeral_div_class.diff_invert_add1
    1.10 +    semiring_numeral_div_class.le_add_diff_inverse2
    1.11 +    semiring_numeral_div_class.mult_div_cancel
    1.12 +    semiring_numeral_div_class.div_less
    1.13 +    semiring_numeral_div_class.mod_less
    1.14 +    semiring_numeral_div_class.div_positive
    1.15 +    semiring_numeral_div_class.mod_less_eq_dividend
    1.16 +    semiring_numeral_div_class.pos_mod_bound
    1.17 +    semiring_numeral_div_class.pos_mod_sign
    1.18 +    semiring_numeral_div_class.mod_mult2_eq
    1.19 +    semiring_numeral_div_class.div_mult2_eq
    1.20 +    semiring_numeral_div_class.discrete)+
    1.21 +
    1.22  
    1.23  subsection {* Code theorems for target language integers *}
    1.24  
    1.25 @@ -347,24 +362,15 @@
    1.26    "snd (divmod_abs k l) = \<bar>k\<bar> mod \<bar>l\<bar>"
    1.27    by (simp add: divmod_abs_def)
    1.28  
    1.29 -lemma divmod_abs_terminate_code [code]:
    1.30 -  "divmod_abs (Neg k) (Neg l) = divmod_abs (Pos k) (Pos l)"
    1.31 -  "divmod_abs (Neg k) (Pos l) = divmod_abs (Pos k) (Pos l)"
    1.32 -  "divmod_abs (Pos k) (Neg l) = divmod_abs (Pos k) (Pos l)"
    1.33 +lemma divmod_abs_code [code]:
    1.34 +  "divmod_abs (Pos k) (Pos l) = divmod k l"
    1.35 +  "divmod_abs (Neg k) (Neg l) = divmod k l"
    1.36 +  "divmod_abs (Neg k) (Pos l) = divmod k l"
    1.37 +  "divmod_abs (Pos k) (Neg l) = divmod k l"
    1.38    "divmod_abs j 0 = (0, \<bar>j\<bar>)"
    1.39    "divmod_abs 0 j = (0, 0)"
    1.40    by (simp_all add: prod_eq_iff)
    1.41  
    1.42 -lemma divmod_abs_rec_code [code]:
    1.43 -  "divmod_abs (Pos k) (Pos l) =
    1.44 -    (let j = sub k l in
    1.45 -       if j < 0 then (0, Pos k)
    1.46 -       else let (q, r) = divmod_abs j (Pos l) in (q + 1, r))"
    1.47 -  apply (simp add: prod_eq_iff Let_def prod_case_beta)
    1.48 -  apply transfer
    1.49 -  apply (simp add: sub_non_negative sub_negative div_pos_pos_trivial mod_pos_pos_trivial div_pos_geq mod_pos_geq)
    1.50 -  done
    1.51 -
    1.52  lemma divmod_integer_code [code]:
    1.53    "divmod_integer k l =
    1.54      (if k = 0 then (0, 0) else if l = 0 then (0, k) else
     2.1 --- a/src/HOL/Divides.thy	Sun Aug 18 15:29:50 2013 +0200
     2.2 +++ b/src/HOL/Divides.thy	Sun Aug 18 15:29:50 2013 +0200
     2.3 @@ -660,6 +660,19 @@
     2.4    with False show ?thesis by simp
     2.5  qed
     2.6  
     2.7 +lemma divmod_cancel [code]:
     2.8 +  "divmod (Num.Bit0 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r))" (is ?P)
     2.9 +  "divmod (Num.Bit1 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r + 1))" (is ?Q)
    2.10 +proof -
    2.11 +  have *: "\<And>q. numeral (Num.Bit0 q) = 2 * numeral q"
    2.12 +    "\<And>q. numeral (Num.Bit1 q) = 2 * numeral q + 1"
    2.13 +    by (simp_all only: numeral_mult numeral.simps distrib) simp_all
    2.14 +  have "1 div 2 = 0" "1 mod 2 = 1" by (auto intro: div_less mod_less)
    2.15 +  then show ?P and ?Q
    2.16 +    by (simp_all add: prod_eq_iff split_def * [of m] * [of n] mod_mult_mult1
    2.17 +      div_mult2_eq [of _ _ 2] mod_mult2_eq [of _ _ 2] add.commute del: numeral_times_numeral)
    2.18 + qed
    2.19 +
    2.20  end
    2.21  
    2.22  hide_fact (open) diff_invert_add1 le_add_diff_inverse2 diff_zero
    2.23 @@ -1846,7 +1859,11 @@
    2.24    by (rule mod_int_unique [of a b q r],
    2.25      simp add: divmod_int_rel_def)
    2.26  
    2.27 -(* simprocs adapted from HOL/ex/Binary.thy *)
    2.28 +text {*
    2.29 +  numeral simprocs -- high chance that these can be replaced
    2.30 +  by divmod algorithm from @{class semiring_numeral_div}
    2.31 +*}
    2.32 +
    2.33  ML {*
    2.34  local
    2.35    val mk_number = HOLogic.mk_number HOLogic.intT
    2.36 @@ -2573,37 +2590,55 @@
    2.37  
    2.38  subsubsection {* Code generation *}
    2.39  
    2.40 -definition pdivmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
    2.41 -  "pdivmod k l = (\<bar>k\<bar> div \<bar>l\<bar>, \<bar>k\<bar> mod \<bar>l\<bar>)"
    2.42 -
    2.43 -lemma pdivmod_posDivAlg [code]:
    2.44 -  "pdivmod k l = (if l = 0 then (0, \<bar>k\<bar>) else posDivAlg \<bar>k\<bar> \<bar>l\<bar>)"
    2.45 -by (subst posDivAlg_div_mod) (simp_all add: pdivmod_def)
    2.46 -
    2.47 -lemma divmod_int_pdivmod: "divmod_int k l = (if k = 0 then (0, 0) else if l = 0 then (0, k) else
    2.48 +definition divmod_abs :: "int \<Rightarrow> int \<Rightarrow> int \<times> int"
    2.49 +where
    2.50 +  "divmod_abs k l = (\<bar>k\<bar> div \<bar>l\<bar>, \<bar>k\<bar> mod \<bar>l\<bar>)"
    2.51 +
    2.52 +lemma fst_divmod_abs [simp]:
    2.53 +  "fst (divmod_abs k l) = \<bar>k\<bar> div \<bar>l\<bar>"
    2.54 +  by (simp add: divmod_abs_def)
    2.55 +
    2.56 +lemma snd_divmod_abs [simp]:
    2.57 +  "snd (divmod_abs k l) = \<bar>k\<bar> mod \<bar>l\<bar>"
    2.58 +  by (simp add: divmod_abs_def)
    2.59 +
    2.60 +lemma divmod_abs_code [code]:
    2.61 +  "divmod_abs (Int.Pos k) (Int.Pos l) = divmod k l"
    2.62 +  "divmod_abs (Int.Neg k) (Int.Neg l) = divmod k l"
    2.63 +  "divmod_abs (Int.Neg k) (Int.Pos l) = divmod k l"
    2.64 +  "divmod_abs (Int.Pos k) (Int.Neg l) = divmod k l"
    2.65 +  "divmod_abs j 0 = (0, \<bar>j\<bar>)"
    2.66 +  "divmod_abs 0 j = (0, 0)"
    2.67 +  by (simp_all add: prod_eq_iff)
    2.68 +
    2.69 +lemma divmod_int_divmod_abs:
    2.70 +  "divmod_int k l = (if k = 0 then (0, 0) else if l = 0 then (0, k) else
    2.71    apsnd ((op *) (sgn l)) (if 0 < l \<and> 0 \<le> k \<or> l < 0 \<and> k < 0
    2.72 -    then pdivmod k l
    2.73 -    else (let (r, s) = pdivmod k l in
    2.74 +    then divmod_abs k l
    2.75 +    else (let (r, s) = divmod_abs k l in
    2.76         if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))"
    2.77  proof -
    2.78    have aux: "\<And>q::int. - k = l * q \<longleftrightarrow> k = l * - q" by auto
    2.79    show ?thesis
    2.80 -    by (simp add: divmod_int_mod_div pdivmod_def)
    2.81 +    by (simp add: prod_eq_iff split_def Let_def)
    2.82        (auto simp add: aux not_less not_le zdiv_zminus1_eq_if
    2.83        zmod_zminus1_eq_if zdiv_zminus2_eq_if zmod_zminus2_eq_if)
    2.84  qed
    2.85  
    2.86 -lemma divmod_int_code [code]: "divmod_int k l = (if k = 0 then (0, 0) else if l = 0 then (0, k) else
    2.87 +lemma divmod_int_code [code]:
    2.88 +  "divmod_int k l = (if k = 0 then (0, 0) else if l = 0 then (0, k) else
    2.89    apsnd ((op *) (sgn l)) (if sgn k = sgn l
    2.90 -    then pdivmod k l
    2.91 -    else (let (r, s) = pdivmod k l in
    2.92 +    then divmod_abs k l
    2.93 +    else (let (r, s) = divmod_abs k l in
    2.94        if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))"
    2.95  proof -
    2.96    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"
    2.97      by (auto simp add: not_less sgn_if)
    2.98 -  then show ?thesis by (simp add: divmod_int_pdivmod)
    2.99 +  then show ?thesis by (simp add: divmod_int_divmod_abs)
   2.100  qed
   2.101  
   2.102 +hide_const (open) divmod_abs
   2.103 +
   2.104  code_identifier
   2.105    code_module Divides \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
   2.106  
     3.1 --- a/src/HOL/Library/Code_Binary_Nat.thy	Sun Aug 18 15:29:50 2013 +0200
     3.2 +++ b/src/HOL/Library/Code_Binary_Nat.thy	Sun Aug 18 15:29:50 2013 +0200
     3.3 @@ -130,6 +130,15 @@
     3.4    "nat_of_num k < nat_of_num l \<longleftrightarrow> k < l"
     3.5    by (simp_all add: nat_of_num_numeral)
     3.6  
     3.7 +lemma [code, code del]:
     3.8 +  "divmod_nat = divmod_nat" ..
     3.9 +  
    3.10 +lemma divmod_nat_code [code]:
    3.11 +  "divmod_nat (nat_of_num k) (nat_of_num l) = divmod k l"
    3.12 +  "divmod_nat m 0 = (0, m)"
    3.13 +  "divmod_nat 0 n = (0, 0)"
    3.14 +  by (simp_all add: prod_eq_iff nat_of_num_numeral del: div_nat_numeral mod_nat_numeral)
    3.15 +
    3.16  
    3.17  subsection {* Conversions *}
    3.18  
     4.1 --- a/src/HOL/Library/Code_Target_Int.thy	Sun Aug 18 15:29:50 2013 +0200
     4.2 +++ b/src/HOL/Library/Code_Target_Int.thy	Sun Aug 18 15:29:50 2013 +0200
     4.3 @@ -65,9 +65,9 @@
     4.4    by simp
     4.5  
     4.6  lemma [code]:
     4.7 -  "pdivmod k l = map_pair int_of_integer int_of_integer
     4.8 +  "Divides.divmod_abs k l = map_pair int_of_integer int_of_integer
     4.9      (Code_Numeral.divmod_abs (of_int k) (of_int l))"
    4.10 -  by (simp add: prod_eq_iff pdivmod_def)
    4.11 +  by (simp add: prod_eq_iff)
    4.12  
    4.13  lemma [code]:
    4.14    "k div l = int_of_integer (of_int k div of_int l)"