src/HOL/Divides.thy
changeset 53069 d165213e3924
parent 53068 41fc65da66f1
child 53070 6a3410845bb2
     1.1 --- a/src/HOL/Divides.thy	Sun Aug 18 15:29:50 2013 +0200
     1.2 +++ b/src/HOL/Divides.thy	Sun Aug 18 15:29:50 2013 +0200
     1.3 @@ -660,6 +660,19 @@
     1.4    with False show ?thesis by simp
     1.5  qed
     1.6  
     1.7 +lemma divmod_cancel [code]:
     1.8 +  "divmod (Num.Bit0 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r))" (is ?P)
     1.9 +  "divmod (Num.Bit1 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r + 1))" (is ?Q)
    1.10 +proof -
    1.11 +  have *: "\<And>q. numeral (Num.Bit0 q) = 2 * numeral q"
    1.12 +    "\<And>q. numeral (Num.Bit1 q) = 2 * numeral q + 1"
    1.13 +    by (simp_all only: numeral_mult numeral.simps distrib) simp_all
    1.14 +  have "1 div 2 = 0" "1 mod 2 = 1" by (auto intro: div_less mod_less)
    1.15 +  then show ?P and ?Q
    1.16 +    by (simp_all add: prod_eq_iff split_def * [of m] * [of n] mod_mult_mult1
    1.17 +      div_mult2_eq [of _ _ 2] mod_mult2_eq [of _ _ 2] add.commute del: numeral_times_numeral)
    1.18 + qed
    1.19 +
    1.20  end
    1.21  
    1.22  hide_fact (open) diff_invert_add1 le_add_diff_inverse2 diff_zero
    1.23 @@ -1846,7 +1859,11 @@
    1.24    by (rule mod_int_unique [of a b q r],
    1.25      simp add: divmod_int_rel_def)
    1.26  
    1.27 -(* simprocs adapted from HOL/ex/Binary.thy *)
    1.28 +text {*
    1.29 +  numeral simprocs -- high chance that these can be replaced
    1.30 +  by divmod algorithm from @{class semiring_numeral_div}
    1.31 +*}
    1.32 +
    1.33  ML {*
    1.34  local
    1.35    val mk_number = HOLogic.mk_number HOLogic.intT
    1.36 @@ -2573,37 +2590,55 @@
    1.37  
    1.38  subsubsection {* Code generation *}
    1.39  
    1.40 -definition pdivmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
    1.41 -  "pdivmod k l = (\<bar>k\<bar> div \<bar>l\<bar>, \<bar>k\<bar> mod \<bar>l\<bar>)"
    1.42 -
    1.43 -lemma pdivmod_posDivAlg [code]:
    1.44 -  "pdivmod k l = (if l = 0 then (0, \<bar>k\<bar>) else posDivAlg \<bar>k\<bar> \<bar>l\<bar>)"
    1.45 -by (subst posDivAlg_div_mod) (simp_all add: pdivmod_def)
    1.46 -
    1.47 -lemma divmod_int_pdivmod: "divmod_int k l = (if k = 0 then (0, 0) else if l = 0 then (0, k) else
    1.48 +definition divmod_abs :: "int \<Rightarrow> int \<Rightarrow> int \<times> int"
    1.49 +where
    1.50 +  "divmod_abs k l = (\<bar>k\<bar> div \<bar>l\<bar>, \<bar>k\<bar> mod \<bar>l\<bar>)"
    1.51 +
    1.52 +lemma fst_divmod_abs [simp]:
    1.53 +  "fst (divmod_abs k l) = \<bar>k\<bar> div \<bar>l\<bar>"
    1.54 +  by (simp add: divmod_abs_def)
    1.55 +
    1.56 +lemma snd_divmod_abs [simp]:
    1.57 +  "snd (divmod_abs k l) = \<bar>k\<bar> mod \<bar>l\<bar>"
    1.58 +  by (simp add: divmod_abs_def)
    1.59 +
    1.60 +lemma divmod_abs_code [code]:
    1.61 +  "divmod_abs (Int.Pos k) (Int.Pos l) = divmod k l"
    1.62 +  "divmod_abs (Int.Neg k) (Int.Neg l) = divmod k l"
    1.63 +  "divmod_abs (Int.Neg k) (Int.Pos l) = divmod k l"
    1.64 +  "divmod_abs (Int.Pos k) (Int.Neg l) = divmod k l"
    1.65 +  "divmod_abs j 0 = (0, \<bar>j\<bar>)"
    1.66 +  "divmod_abs 0 j = (0, 0)"
    1.67 +  by (simp_all add: prod_eq_iff)
    1.68 +
    1.69 +lemma divmod_int_divmod_abs:
    1.70 +  "divmod_int k l = (if k = 0 then (0, 0) else if l = 0 then (0, k) else
    1.71    apsnd ((op *) (sgn l)) (if 0 < l \<and> 0 \<le> k \<or> l < 0 \<and> k < 0
    1.72 -    then pdivmod k l
    1.73 -    else (let (r, s) = pdivmod k l in
    1.74 +    then divmod_abs k l
    1.75 +    else (let (r, s) = divmod_abs k l in
    1.76         if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))"
    1.77  proof -
    1.78    have aux: "\<And>q::int. - k = l * q \<longleftrightarrow> k = l * - q" by auto
    1.79    show ?thesis
    1.80 -    by (simp add: divmod_int_mod_div pdivmod_def)
    1.81 +    by (simp add: prod_eq_iff split_def Let_def)
    1.82        (auto simp add: aux not_less not_le zdiv_zminus1_eq_if
    1.83        zmod_zminus1_eq_if zdiv_zminus2_eq_if zmod_zminus2_eq_if)
    1.84  qed
    1.85  
    1.86 -lemma divmod_int_code [code]: "divmod_int k l = (if k = 0 then (0, 0) else if l = 0 then (0, k) else
    1.87 +lemma divmod_int_code [code]:
    1.88 +  "divmod_int k l = (if k = 0 then (0, 0) else if l = 0 then (0, k) else
    1.89    apsnd ((op *) (sgn l)) (if sgn k = sgn l
    1.90 -    then pdivmod k l
    1.91 -    else (let (r, s) = pdivmod k l in
    1.92 +    then divmod_abs k l
    1.93 +    else (let (r, s) = divmod_abs k l in
    1.94        if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))"
    1.95  proof -
    1.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"
    1.97      by (auto simp add: not_less sgn_if)
    1.98 -  then show ?thesis by (simp add: divmod_int_pdivmod)
    1.99 +  then show ?thesis by (simp add: divmod_int_divmod_abs)
   1.100  qed
   1.101  
   1.102 +hide_const (open) divmod_abs
   1.103 +
   1.104  code_identifier
   1.105    code_module Divides \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
   1.106