author haftmann Sun Aug 18 15:29:50 2013 +0200 (2013-08-18) changeset 53067 ee0b7c2315d2 parent 53066 1f61a923c2d6 child 53068 41fc65da66f1
type class for generic division algorithm on numerals
 src/HOL/Divides.thy file | annotate | diff | revisions
```     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.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.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')"