type class for generic division algorithm on numerals
authorhaftmann
Sun Aug 18 15:29:50 2013 +0200 (2013-08-18)
changeset 53067ee0b7c2315d2
parent 53066 1f61a923c2d6
child 53068 41fc65da66f1
type class for generic division algorithm on numerals
src/HOL/Divides.thy
     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 @@ -480,6 +480,192 @@
     1.4  end
     1.5  
     1.6  
     1.7 +subsection {* Generic numeral division with a pragmatic type class *}
     1.8 +
     1.9 +text {*
    1.10 +  The following type class contains everything necessary to formulate
    1.11 +  a division algorithm in ring structures with numerals, restricted
    1.12 +  to its positive segments.  This is its primary motiviation, and it
    1.13 +  could surely be formulated using a more fine-grained, more algebraic
    1.14 +  and less technical class hierarchy.
    1.15 +*}
    1.16 +
    1.17 +
    1.18 +class semiring_numeral_div = linordered_semidom + minus + semiring_div +
    1.19 +  assumes diff_invert_add1: "a + b = c \<Longrightarrow> a = c - b"
    1.20 +    and le_add_diff_inverse2: "b \<le> a \<Longrightarrow> a - b + b = a"
    1.21 +  assumes mult_div_cancel: "b * (a div b) = a - a mod b"
    1.22 +    and div_less: "0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a div b = 0"
    1.23 +    and mod_less: " 0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a mod b = a"
    1.24 +    and div_positive: "0 < b \<Longrightarrow> b \<le> a \<Longrightarrow> a div b > 0"
    1.25 +    and mod_less_eq_dividend: "0 \<le> a \<Longrightarrow> a mod b \<le> a"
    1.26 +    and pos_mod_bound: "0 < b \<Longrightarrow> a mod b < b"
    1.27 +    and pos_mod_sign: "0 < b \<Longrightarrow> 0 \<le> a mod b"
    1.28 +    and mod_mult2_eq: "0 \<le> c \<Longrightarrow> a mod (b * c) = b * (a div b mod c) + a mod b"
    1.29 +    and div_mult2_eq: "0 \<le> c \<Longrightarrow> a div (b * c) = a div b div c"
    1.30 +  assumes discrete: "a < b \<longleftrightarrow> a + 1 \<le> b"
    1.31 +begin
    1.32 +
    1.33 +lemma diff_zero [simp]:
    1.34 +  "a - 0 = a"
    1.35 +  by (rule diff_invert_add1 [symmetric]) simp
    1.36 +
    1.37 +lemma parity:
    1.38 +  "a mod 2 = 0 \<or> a mod 2 = 1"
    1.39 +proof (rule ccontr)
    1.40 +  assume "\<not> (a mod 2 = 0 \<or> a mod 2 = 1)"
    1.41 +  then have "a mod 2 \<noteq> 0" and "a mod 2 \<noteq> 1" by simp_all
    1.42 +  have "0 < 2" by simp
    1.43 +  with pos_mod_bound pos_mod_sign have "0 \<le> a mod 2" "a mod 2 < 2" by simp_all
    1.44 +  with `a mod 2 \<noteq> 0` have "0 < a mod 2" by simp
    1.45 +  with discrete have "1 \<le> a mod 2" by simp
    1.46 +  with `a mod 2 \<noteq> 1` have "1 < a mod 2" by simp
    1.47 +  with discrete have "2 \<le> a mod 2" by simp
    1.48 +  with `a mod 2 < 2` show False by simp
    1.49 +qed
    1.50 +
    1.51 +lemma divmod_digit_1:
    1.52 +  assumes "0 \<le> a" "0 < b" and "b \<le> a mod (2 * b)"
    1.53 +  shows "2 * (a div (2 * b)) + 1 = a div b" (is "?P")
    1.54 +    and "a mod (2 * b) - b = a mod b" (is "?Q")
    1.55 +proof -
    1.56 +  from assms mod_less_eq_dividend [of a "2 * b"] have "b \<le> a"
    1.57 +    by (auto intro: trans)
    1.58 +  with `0 < b` have "0 < a div b" by (auto intro: div_positive)
    1.59 +  then have [simp]: "1 \<le> a div b" by (simp add: discrete)
    1.60 +  with `0 < b` have mod_less: "a mod b < b" by (simp add: pos_mod_bound)
    1.61 +  def w \<equiv> "a div b mod 2" with parity have w_exhaust: "w = 0 \<or> w = 1" by auto
    1.62 +  have mod_w: "a mod (2 * b) = a mod b + b * w"
    1.63 +    by (simp add: w_def mod_mult2_eq ac_simps)
    1.64 +  from assms w_exhaust have "w = 1"
    1.65 +    by (auto simp add: mod_w) (insert mod_less, auto)
    1.66 +  with mod_w have mod: "a mod (2 * b) = a mod b + b" by simp
    1.67 +  have "2 * (a div (2 * b)) = a div b - w"
    1.68 +    by (simp add: w_def div_mult2_eq mult_div_cancel ac_simps)
    1.69 +  with `w = 1` have div: "2 * (a div (2 * b)) = a div b - 1" by simp
    1.70 +  then show ?P and ?Q
    1.71 +    by (simp_all add: div mod diff_invert_add1 [symmetric] le_add_diff_inverse2)
    1.72 +qed
    1.73 +
    1.74 +lemma divmod_digit_0:
    1.75 +  assumes "0 < b" and "a mod (2 * b) < b"
    1.76 +  shows "2 * (a div (2 * b)) = a div b" (is "?P")
    1.77 +    and "a mod (2 * b) = a mod b" (is "?Q")
    1.78 +proof -
    1.79 +  def w \<equiv> "a div b mod 2" with parity have w_exhaust: "w = 0 \<or> w = 1" by auto
    1.80 +  have mod_w: "a mod (2 * b) = a mod b + b * w"
    1.81 +    by (simp add: w_def mod_mult2_eq ac_simps)
    1.82 +  moreover have "b \<le> a mod b + b"
    1.83 +  proof -
    1.84 +    from `0 < b` pos_mod_sign have "0 \<le> a mod b" by blast
    1.85 +    then have "0 + b \<le> a mod b + b" by (rule add_right_mono)
    1.86 +    then show ?thesis by simp
    1.87 +  qed
    1.88 +  moreover note assms w_exhaust
    1.89 +  ultimately have "w = 0" by auto
    1.90 +  find_theorems "_ + ?b < _ + ?b"
    1.91 +  with mod_w have mod: "a mod (2 * b) = a mod b" by simp
    1.92 +  have "2 * (a div (2 * b)) = a div b - w"
    1.93 +    by (simp add: w_def div_mult2_eq mult_div_cancel ac_simps)
    1.94 +  with `w = 0` have div: "2 * (a div (2 * b)) = a div b" by simp
    1.95 +  then show ?P and ?Q
    1.96 +    by (simp_all add: div mod)
    1.97 +qed
    1.98 +
    1.99 +definition divmod :: "num \<Rightarrow> num \<Rightarrow> 'a \<times> 'a"
   1.100 +where
   1.101 +  "divmod m n = (numeral m div numeral n, numeral m mod numeral n)"
   1.102 +
   1.103 +lemma fst_divmod [simp]:
   1.104 +  "fst (divmod m n) = numeral m div numeral n"
   1.105 +  by (simp add: divmod_def)
   1.106 +
   1.107 +lemma snd_divmod [simp]:
   1.108 +  "snd (divmod m n) = numeral m mod numeral n"
   1.109 +  by (simp add: divmod_def)
   1.110 +
   1.111 +definition divmod_step :: "num \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<times> 'a"
   1.112 +where
   1.113 +  "divmod_step l qr = (let (q, r) = qr
   1.114 +    in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
   1.115 +    else (2 * q, r))"
   1.116 +
   1.117 +text {*
   1.118 +  This is a formulation of one step (referring to one digit position)
   1.119 +  in school-method division: compare the dividend at the current
   1.120 +  digit position with the remained from previous division steps
   1.121 +  and evaluate accordingly.
   1.122 +*}
   1.123 +
   1.124 +lemma divmod_step_eq [code]:
   1.125 +  "divmod_step l (q, r) = (if numeral l \<le> r
   1.126 +    then (2 * q + 1, r - numeral l) else (2 * q, r))"
   1.127 +  by (simp add: divmod_step_def)
   1.128 +
   1.129 +lemma divmod_step_simps [simp]:
   1.130 +  "r < numeral l \<Longrightarrow> divmod_step l (q, r) = (2 * q, r)"
   1.131 +  "numeral l \<le> r \<Longrightarrow> divmod_step l (q, r) = (2 * q + 1, r - numeral l)"
   1.132 +  by (auto simp add: divmod_step_eq not_le)
   1.133 +
   1.134 +text {*
   1.135 +  This is a formulation of school-method division.
   1.136 +  If the divisor is smaller than the dividend, terminate.
   1.137 +  If not, shift the dividend to the right until termination
   1.138 +  occurs and then reiterate single division steps in the
   1.139 +  opposite direction.
   1.140 +*}
   1.141 +
   1.142 +lemma divmod_divmod_step [code]:
   1.143 +  "divmod m n = (if m < n then (0, numeral m)
   1.144 +    else divmod_step n (divmod m (Num.Bit0 n)))"
   1.145 +proof (cases "m < n")
   1.146 +  case True then have "numeral m < numeral n" by simp
   1.147 +  then show ?thesis
   1.148 +    by (simp add: prod_eq_iff div_less mod_less)
   1.149 +next
   1.150 +  case False
   1.151 +  have "divmod m n =
   1.152 +    divmod_step n (numeral m div (2 * numeral n),
   1.153 +      numeral m mod (2 * numeral n))"
   1.154 +  proof (cases "numeral n \<le> numeral m mod (2 * numeral n)")
   1.155 +    case True
   1.156 +    with divmod_step_simps
   1.157 +      have "divmod_step n (numeral m div (2 * numeral n), numeral m mod (2 * numeral n)) =
   1.158 +        (2 * (numeral m div (2 * numeral n)) + 1, numeral m mod (2 * numeral n) - numeral n)"
   1.159 +        by blast
   1.160 +    moreover from True divmod_digit_1 [of "numeral m" "numeral n"]
   1.161 +      have "2 * (numeral m div (2 * numeral n)) + 1 = numeral m div numeral n"
   1.162 +      and "numeral m mod (2 * numeral n) - numeral n = numeral m mod numeral n"
   1.163 +      by simp_all
   1.164 +    ultimately show ?thesis by (simp only: divmod_def)
   1.165 +  next
   1.166 +    case False then have *: "numeral m mod (2 * numeral n) < numeral n"
   1.167 +      by (simp add: not_le)
   1.168 +    with divmod_step_simps
   1.169 +      have "divmod_step n (numeral m div (2 * numeral n), numeral m mod (2 * numeral n)) =
   1.170 +        (2 * (numeral m div (2 * numeral n)), numeral m mod (2 * numeral n))"
   1.171 +        by blast
   1.172 +    moreover from * divmod_digit_0 [of "numeral n" "numeral m"]
   1.173 +      have "2 * (numeral m div (2 * numeral n)) = numeral m div numeral n"
   1.174 +      and "numeral m mod (2 * numeral n) = numeral m mod numeral n"
   1.175 +      by (simp_all only: zero_less_numeral)
   1.176 +    ultimately show ?thesis by (simp only: divmod_def)
   1.177 +  qed
   1.178 +  then have "divmod m n =
   1.179 +    divmod_step n (numeral m div numeral (Num.Bit0 n),
   1.180 +      numeral m mod numeral (Num.Bit0 n))"
   1.181 +    by (simp only: numeral.simps distrib mult_1) 
   1.182 +  then have "divmod m n = divmod_step n (divmod m (Num.Bit0 n))"
   1.183 +    by (simp add: divmod_def)
   1.184 +  with False show ?thesis by simp
   1.185 +qed
   1.186 +
   1.187 +end
   1.188 +
   1.189 +hide_fact (open) diff_invert_add1 le_add_diff_inverse2 diff_zero
   1.190 +  -- {* restore simple accesses for more general variants of theorems *}
   1.191 +
   1.192 +  
   1.193  subsection {* Division on @{typ nat} *}
   1.194  
   1.195  text {*
   1.196 @@ -1191,6 +1377,9 @@
   1.197    shows "n mod 2 \<noteq> 0 \<longleftrightarrow> n mod 2 = 1"
   1.198    by simp
   1.199  
   1.200 +instance nat :: semiring_numeral_div
   1.201 +  by intro_classes (auto intro: div_positive simp add: mult_div_cancel mod_mult2_eq div_mult2_eq)
   1.202 +
   1.203  
   1.204  subsection {* Division on @{typ int} *}
   1.205  
   1.206 @@ -1199,6 +1388,14 @@
   1.207    "divmod_int_rel a b = (\<lambda>(q, r). a = b * q + r \<and>
   1.208      (if 0 < b then 0 \<le> r \<and> r < b else if b < 0 then b < r \<and> r \<le> 0 else q = 0))"
   1.209  
   1.210 +text {*
   1.211 +  The following algorithmic devlopment actually echos what has already
   1.212 +  been developed in class @{class semiring_numeral_div}.  In the long
   1.213 +  run it seems better to derive division on @{typ int} just from
   1.214 +  division on @{typ nat} and instantiate @{class semiring_numeral_div}
   1.215 +  accordingly.
   1.216 +*}
   1.217 +
   1.218  definition adjust :: "int \<Rightarrow> int \<times> int \<Rightarrow> int \<times> int" where
   1.219      --{*for the division algorithm*}
   1.220      "adjust b = (\<lambda>(q, r). if 0 \<le> r - b then (2 * q + 1, r - b)
   1.221 @@ -2330,6 +2527,12 @@
   1.222    thus  ?lhs by simp
   1.223  qed
   1.224  
   1.225 +text {*
   1.226 +  This re-embedding of natural division on integers goes back to the
   1.227 +  time when numerals had been signed numerals.  It should
   1.228 +  now be placed by the algorithm developed in @{class semiring_numeral_div}.  
   1.229 +*}
   1.230 +
   1.231  lemma div_nat_numeral [simp]:
   1.232    "(numeral v :: nat) div numeral v' = nat (numeral v div numeral v')"
   1.233    by (simp add: nat_div_distrib)
   1.234 @@ -2351,6 +2554,11 @@
   1.235    shows "k mod 2 \<noteq> 0 \<longleftrightarrow> k mod 2 = 1"
   1.236    by auto
   1.237  
   1.238 +instance int :: semiring_numeral_div
   1.239 +  by intro_classes (auto intro: zmod_le_nonneg_dividend simp add: zmult_div_cancel
   1.240 +    pos_imp_zdiv_pos_iff div_pos_pos_trivial mod_pos_pos_trivial,
   1.241 +    auto intro: zmod_zmult2_eq zdiv_zmult2_eq simp add: le_less)
   1.242 +
   1.243  
   1.244  subsubsection {* Tools setup *}
   1.245