# HG changeset patch
# User haftmann
# Date 1376832590 -7200
# Node ID ee0b7c2315d24533e056444b9b00177305f0ff97
# Parent  1f61a923c2d60be2c9ef287e70f6874987897efb
type class for generic division algorithm on numerals

diff -r 1f61a923c2d6 -r ee0b7c2315d2 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
@@ -480,6 +480,192 @@
 end
 
 
+subsection {* Generic numeral division with a pragmatic type class *}
+
+text {*
+  The following type class contains everything necessary to formulate
+  a division algorithm in ring structures with numerals, restricted
+  to its positive segments.  This is its primary motiviation, and it
+  could surely be formulated using a more fine-grained, more algebraic
+  and less technical class hierarchy.
+*}
+
+
+class semiring_numeral_div = linordered_semidom + minus + semiring_div +
+  assumes diff_invert_add1: "a + b = c \<Longrightarrow> a = c - b"
+    and le_add_diff_inverse2: "b \<le> a \<Longrightarrow> a - b + b = a"
+  assumes mult_div_cancel: "b * (a div b) = a - a mod b"
+    and div_less: "0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a div b = 0"
+    and mod_less: " 0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a mod b = a"
+    and div_positive: "0 < b \<Longrightarrow> b \<le> a \<Longrightarrow> a div b > 0"
+    and mod_less_eq_dividend: "0 \<le> a \<Longrightarrow> a mod b \<le> a"
+    and pos_mod_bound: "0 < b \<Longrightarrow> a mod b < b"
+    and pos_mod_sign: "0 < b \<Longrightarrow> 0 \<le> a mod b"
+    and mod_mult2_eq: "0 \<le> c \<Longrightarrow> a mod (b * c) = b * (a div b mod c) + a mod b"
+    and div_mult2_eq: "0 \<le> c \<Longrightarrow> a div (b * c) = a div b div c"
+  assumes discrete: "a < b \<longleftrightarrow> a + 1 \<le> b"
+begin
+
+lemma diff_zero [simp]:
+  "a - 0 = a"
+  by (rule diff_invert_add1 [symmetric]) simp
+
+lemma parity:
+  "a mod 2 = 0 \<or> a mod 2 = 1"
+proof (rule ccontr)
+  assume "\<not> (a mod 2 = 0 \<or> a mod 2 = 1)"
+  then have "a mod 2 \<noteq> 0" and "a mod 2 \<noteq> 1" by simp_all
+  have "0 < 2" by simp
+  with pos_mod_bound pos_mod_sign have "0 \<le> a mod 2" "a mod 2 < 2" by simp_all
+  with `a mod 2 \<noteq> 0` have "0 < a mod 2" by simp
+  with discrete have "1 \<le> a mod 2" by simp
+  with `a mod 2 \<noteq> 1` have "1 < a mod 2" by simp
+  with discrete have "2 \<le> a mod 2" by simp
+  with `a mod 2 < 2` show False by simp
+qed
+
+lemma divmod_digit_1:
+  assumes "0 \<le> a" "0 < b" and "b \<le> a mod (2 * b)"
+  shows "2 * (a div (2 * b)) + 1 = a div b" (is "?P")
+    and "a mod (2 * b) - b = a mod b" (is "?Q")
+proof -
+  from assms mod_less_eq_dividend [of a "2 * b"] have "b \<le> a"
+    by (auto intro: trans)
+  with `0 < b` have "0 < a div b" by (auto intro: div_positive)
+  then have [simp]: "1 \<le> a div b" by (simp add: discrete)
+  with `0 < b` have mod_less: "a mod b < b" by (simp add: pos_mod_bound)
+  def w \<equiv> "a div b mod 2" with parity have w_exhaust: "w = 0 \<or> w = 1" by auto
+  have mod_w: "a mod (2 * b) = a mod b + b * w"
+    by (simp add: w_def mod_mult2_eq ac_simps)
+  from assms w_exhaust have "w = 1"
+    by (auto simp add: mod_w) (insert mod_less, auto)
+  with mod_w have mod: "a mod (2 * b) = a mod b + b" by simp
+  have "2 * (a div (2 * b)) = a div b - w"
+    by (simp add: w_def div_mult2_eq mult_div_cancel ac_simps)
+  with `w = 1` have div: "2 * (a div (2 * b)) = a div b - 1" by simp
+  then show ?P and ?Q
+    by (simp_all add: div mod diff_invert_add1 [symmetric] le_add_diff_inverse2)
+qed
+
+lemma divmod_digit_0:
+  assumes "0 < b" and "a mod (2 * b) < b"
+  shows "2 * (a div (2 * b)) = a div b" (is "?P")
+    and "a mod (2 * b) = a mod b" (is "?Q")
+proof -
+  def w \<equiv> "a div b mod 2" with parity have w_exhaust: "w = 0 \<or> w = 1" by auto
+  have mod_w: "a mod (2 * b) = a mod b + b * w"
+    by (simp add: w_def mod_mult2_eq ac_simps)
+  moreover have "b \<le> a mod b + b"
+  proof -
+    from `0 < b` pos_mod_sign have "0 \<le> a mod b" by blast
+    then have "0 + b \<le> a mod b + b" by (rule add_right_mono)
+    then show ?thesis by simp
+  qed
+  moreover note assms w_exhaust
+  ultimately have "w = 0" by auto
+  find_theorems "_ + ?b < _ + ?b"
+  with mod_w have mod: "a mod (2 * b) = a mod b" by simp
+  have "2 * (a div (2 * b)) = a div b - w"
+    by (simp add: w_def div_mult2_eq mult_div_cancel ac_simps)
+  with `w = 0` have div: "2 * (a div (2 * b)) = a div b" by simp
+  then show ?P and ?Q
+    by (simp_all add: div mod)
+qed
+
+definition divmod :: "num \<Rightarrow> num \<Rightarrow> 'a \<times> 'a"
+where
+  "divmod m n = (numeral m div numeral n, numeral m mod numeral n)"
+
+lemma fst_divmod [simp]:
+  "fst (divmod m n) = numeral m div numeral n"
+  by (simp add: divmod_def)
+
+lemma snd_divmod [simp]:
+  "snd (divmod m n) = numeral m mod numeral n"
+  by (simp add: divmod_def)
+
+definition divmod_step :: "num \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<times> 'a"
+where
+  "divmod_step l qr = (let (q, r) = qr
+    in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
+    else (2 * q, r))"
+
+text {*
+  This is a formulation of one step (referring to one digit position)
+  in school-method division: compare the dividend at the current
+  digit position with the remained from previous division steps
+  and evaluate accordingly.
+*}
+
+lemma divmod_step_eq [code]:
+  "divmod_step l (q, r) = (if numeral l \<le> r
+    then (2 * q + 1, r - numeral l) else (2 * q, r))"
+  by (simp add: divmod_step_def)
+
+lemma divmod_step_simps [simp]:
+  "r < numeral l \<Longrightarrow> divmod_step l (q, r) = (2 * q, r)"
+  "numeral l \<le> r \<Longrightarrow> divmod_step l (q, r) = (2 * q + 1, r - numeral l)"
+  by (auto simp add: divmod_step_eq not_le)
+
+text {*
+  This is a formulation of school-method division.
+  If the divisor is smaller than the dividend, terminate.
+  If not, shift the dividend to the right until termination
+  occurs and then reiterate single division steps in the
+  opposite direction.
+*}
+
+lemma divmod_divmod_step [code]:
+  "divmod m n = (if m < n then (0, numeral m)
+    else divmod_step n (divmod m (Num.Bit0 n)))"
+proof (cases "m < n")
+  case True then have "numeral m < numeral n" by simp
+  then show ?thesis
+    by (simp add: prod_eq_iff div_less mod_less)
+next
+  case False
+  have "divmod m n =
+    divmod_step n (numeral m div (2 * numeral n),
+      numeral m mod (2 * numeral n))"
+  proof (cases "numeral n \<le> numeral m mod (2 * numeral n)")
+    case True
+    with divmod_step_simps
+      have "divmod_step n (numeral m div (2 * numeral n), numeral m mod (2 * numeral n)) =
+        (2 * (numeral m div (2 * numeral n)) + 1, numeral m mod (2 * numeral n) - numeral n)"
+        by blast
+    moreover from True divmod_digit_1 [of "numeral m" "numeral n"]
+      have "2 * (numeral m div (2 * numeral n)) + 1 = numeral m div numeral n"
+      and "numeral m mod (2 * numeral n) - numeral n = numeral m mod numeral n"
+      by simp_all
+    ultimately show ?thesis by (simp only: divmod_def)
+  next
+    case False then have *: "numeral m mod (2 * numeral n) < numeral n"
+      by (simp add: not_le)
+    with divmod_step_simps
+      have "divmod_step n (numeral m div (2 * numeral n), numeral m mod (2 * numeral n)) =
+        (2 * (numeral m div (2 * numeral n)), numeral m mod (2 * numeral n))"
+        by blast
+    moreover from * divmod_digit_0 [of "numeral n" "numeral m"]
+      have "2 * (numeral m div (2 * numeral n)) = numeral m div numeral n"
+      and "numeral m mod (2 * numeral n) = numeral m mod numeral n"
+      by (simp_all only: zero_less_numeral)
+    ultimately show ?thesis by (simp only: divmod_def)
+  qed
+  then have "divmod m n =
+    divmod_step n (numeral m div numeral (Num.Bit0 n),
+      numeral m mod numeral (Num.Bit0 n))"
+    by (simp only: numeral.simps distrib mult_1) 
+  then have "divmod m n = divmod_step n (divmod m (Num.Bit0 n))"
+    by (simp add: divmod_def)
+  with False show ?thesis by simp
+qed
+
+end
+
+hide_fact (open) diff_invert_add1 le_add_diff_inverse2 diff_zero
+  -- {* restore simple accesses for more general variants of theorems *}
+
+  
 subsection {* Division on @{typ nat} *}
 
 text {*
@@ -1191,6 +1377,9 @@
   shows "n mod 2 \<noteq> 0 \<longleftrightarrow> n mod 2 = 1"
   by simp
 
+instance nat :: semiring_numeral_div
+  by intro_classes (auto intro: div_positive simp add: mult_div_cancel mod_mult2_eq div_mult2_eq)
+
 
 subsection {* Division on @{typ int} *}
 
@@ -1199,6 +1388,14 @@
   "divmod_int_rel a b = (\<lambda>(q, r). a = b * q + r \<and>
     (if 0 < b then 0 \<le> r \<and> r < b else if b < 0 then b < r \<and> r \<le> 0 else q = 0))"
 
+text {*
+  The following algorithmic devlopment actually echos what has already
+  been developed in class @{class semiring_numeral_div}.  In the long
+  run it seems better to derive division on @{typ int} just from
+  division on @{typ nat} and instantiate @{class semiring_numeral_div}
+  accordingly.
+*}
+
 definition adjust :: "int \<Rightarrow> int \<times> int \<Rightarrow> int \<times> int" where
     --{*for the division algorithm*}
     "adjust b = (\<lambda>(q, r). if 0 \<le> r - b then (2 * q + 1, r - b)
@@ -2330,6 +2527,12 @@
   thus  ?lhs by simp
 qed
 
+text {*
+  This re-embedding of natural division on integers goes back to the
+  time when numerals had been signed numerals.  It should
+  now be placed by the algorithm developed in @{class semiring_numeral_div}.  
+*}
+
 lemma div_nat_numeral [simp]:
   "(numeral v :: nat) div numeral v' = nat (numeral v div numeral v')"
   by (simp add: nat_div_distrib)
@@ -2351,6 +2554,11 @@
   shows "k mod 2 \<noteq> 0 \<longleftrightarrow> k mod 2 = 1"
   by auto
 
+instance int :: semiring_numeral_div
+  by intro_classes (auto intro: zmod_le_nonneg_dividend simp add: zmult_div_cancel
+    pos_imp_zdiv_pos_iff div_pos_pos_trivial mod_pos_pos_trivial,
+    auto intro: zmod_zmult2_eq zdiv_zmult2_eq simp add: le_less)
+
 
 subsubsection {* Tools setup *}