# HG changeset patch
# User huffman
# Date 1329744226 -3600
# Node ID 866bce5442a34334c754b5405053ea15eb4a4890
# Parent  d1dcb91a512e08d8da33cd1fac778bd28c7644c9
simplify projections on simultaneous computations of div and mod; tuned structure (from Florian Haftmann)

diff -r d1dcb91a512e -r 866bce5442a3 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Mon Feb 20 12:37:17 2012 +0100
+++ b/src/HOL/Divides.thy	Mon Feb 20 14:23:46 2012 +0100
@@ -523,9 +523,6 @@
   means of @{const divmod_nat_rel}:
 *}
 
-instantiation nat :: semiring_div
-begin
-
 definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
   "divmod_nat m n = (THE qr. divmod_nat_rel m n qr)"
 
@@ -543,28 +540,39 @@
   shows "divmod_nat m n = qr"
   using assms by (auto intro: divmod_nat_rel_unique divmod_nat_rel_divmod_nat)
 
+instantiation nat :: semiring_div
+begin
+
 definition div_nat where
   "m div n = fst (divmod_nat m n)"
 
+lemma fst_divmod_nat [simp]:
+  "fst (divmod_nat m n) = m div n"
+  by (simp add: div_nat_def)
+
 definition mod_nat where
   "m mod n = snd (divmod_nat m n)"
 
+lemma snd_divmod_nat [simp]:
+  "snd (divmod_nat m n) = m mod n"
+  by (simp add: mod_nat_def)
+
 lemma divmod_nat_div_mod:
   "divmod_nat m n = (m div n, m mod n)"
-  unfolding div_nat_def mod_nat_def by simp
+  by (simp add: prod_eq_iff)
 
 lemma div_eq:
   assumes "divmod_nat_rel m n (q, r)" 
   shows "m div n = q"
-  using assms by (auto dest: divmod_nat_eq simp add: divmod_nat_div_mod)
+  using assms by (auto dest!: divmod_nat_eq simp add: prod_eq_iff)
 
 lemma mod_eq:
   assumes "divmod_nat_rel m n (q, r)" 
   shows "m mod n = r"
-  using assms by (auto dest: divmod_nat_eq simp add: divmod_nat_div_mod)
+  using assms by (auto dest!: divmod_nat_eq simp add: prod_eq_iff)
 
 lemma divmod_nat_rel: "divmod_nat_rel m n (m div n, m mod n)"
-  by (simp add: div_nat_def mod_nat_def divmod_nat_rel_divmod_nat)
+  using divmod_nat_rel_divmod_nat by (simp add: divmod_nat_div_mod)
 
 lemma divmod_nat_zero:
   "divmod_nat m 0 = (0, m)"
@@ -613,25 +621,25 @@
   fixes m n :: nat
   assumes "m < n"
   shows "m div n = 0"
-  using assms divmod_nat_base divmod_nat_div_mod by simp
+  using assms divmod_nat_base by (simp add: prod_eq_iff)
 
 lemma le_div_geq:
   fixes m n :: nat
   assumes "0 < n" and "n \<le> m"
   shows "m div n = Suc ((m - n) div n)"
-  using assms divmod_nat_step divmod_nat_div_mod by simp
+  using assms divmod_nat_step by (simp add: prod_eq_iff)
 
 lemma mod_less [simp]:
   fixes m n :: nat
   assumes "m < n"
   shows "m mod n = m"
-  using assms divmod_nat_base divmod_nat_div_mod by simp
+  using assms divmod_nat_base by (simp add: prod_eq_iff)
 
 lemma le_mod_geq:
   fixes m n :: nat
   assumes "n \<le> m"
   shows "m mod n = (m - n) mod n"
-  using assms divmod_nat_step divmod_nat_div_mod by (cases "n = 0") simp_all
+  using assms divmod_nat_step by (cases "n = 0") (simp_all add: prod_eq_iff)
 
 instance proof -
   have [simp]: "\<And>n::nat. n div 0 = 0"
@@ -673,8 +681,7 @@
 
 lemma divmod_nat_if [code]: "divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
   let (q, r) = divmod_nat (m - n) n in (Suc q, r))"
-by (simp add: divmod_nat_zero divmod_nat_base divmod_nat_step)
-    (simp add: divmod_nat_div_mod)
+  by (simp add: prod_eq_iff prod_case_beta not_less le_div_geq le_mod_geq)
 
 text {* Simproc for cancelling @{const div} and @{const mod} *}
 
@@ -807,12 +814,11 @@
   done
 
 
-subsubsection{*Further Facts about Quotient and Remainder*}
+subsubsection {* Further Facts about Quotient and Remainder *}
 
 lemma div_1 [simp]: "m div Suc 0 = m"
 by (induct m) (simp_all add: div_geq)
 
-
 (* Monotonicity of div in first argument *)
 lemma div_le_mono [rule_format (no_asm)]:
     "\<forall>m::nat. m \<le> n --> (m div k) \<le> (n div k)"
@@ -1018,7 +1024,7 @@
 qed
 
 
-subsubsection {*An ``induction'' law for modulus arithmetic.*}
+subsubsection {* An ``induction'' law for modulus arithmetic. *}
 
 lemma mod_induct_0:
   assumes step: "\<forall>i<p. P i \<longrightarrow> P ((Suc i) mod p)"
@@ -1228,19 +1234,27 @@
 instantiation int :: Divides.div
 begin
 
-definition
+definition div_int where
   "a div b = fst (divmod_int a b)"
 
-definition
+lemma fst_divmod_int [simp]:
+  "fst (divmod_int a b) = a div b"
+  by (simp add: div_int_def)
+
+definition mod_int where
  "a mod b = snd (divmod_int a b)"
 
+lemma snd_divmod_int [simp]:
+  "snd (divmod_int a b) = a mod b"
+  by (simp add: mod_int_def)
+
 instance ..
 
 end
 
 lemma divmod_int_mod_div:
   "divmod_int p q = (p div q, p mod q)"
-  by (auto simp add: div_int_def mod_int_def)
+  by (simp add: prod_eq_iff)
 
 text{*
 Here is the division algorithm in ML:
@@ -1271,8 +1285,7 @@
 *}
 
 
-
-subsubsection{*Uniqueness and Monotonicity of Quotients and Remainders*}
+subsubsection {* Uniqueness and Monotonicity of Quotients and Remainders *}
 
 lemma unique_quotient_lemma:
      "[| b*q' + r'  \<le> b*q + r;  0 \<le> r';  r' < b;  r < b |]  
@@ -1312,7 +1325,7 @@
 done
 
 
-subsubsection{*Correctness of @{term posDivAlg}, the Algorithm for Non-Negative Dividends*}
+subsubsection {* Correctness of @{term posDivAlg}, the Algorithm for Non-Negative Dividends *}
 
 text{*And positive divisors*}
 
@@ -1347,7 +1360,7 @@
   done
 
 
-subsubsection{*Correctness of @{term negDivAlg}, the Algorithm for Negative Dividends*}
+subsubsection {* Correctness of @{term negDivAlg}, the Algorithm for Negative Dividends *}
 
 text{*And positive divisors*}
 
@@ -1377,7 +1390,7 @@
   done
 
 
-subsubsection{*Existence Shown by Proving the Division Algorithm to be Correct*}
+subsubsection {* Existence Shown by Proving the Division Algorithm to be Correct *}
 
 (*the case a=0*)
 lemma divmod_int_rel_0: "b \<noteq> 0 ==> divmod_int_rel 0 b (0, 0)"
@@ -1411,7 +1424,7 @@
 lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)"
 apply (case_tac "b = 0", simp)
 apply (cut_tac a = a and b = b in divmod_int_correct)
-apply (auto simp add: divmod_int_rel_def div_int_def mod_int_def)
+apply (auto simp add: divmod_int_rel_def prod_eq_iff)
 done
 
 lemma zdiv_zmod_equality: "(b * (a div b) + (a mod b)) + k = (a::int)+k"
@@ -1442,7 +1455,7 @@
 
 lemma pos_mod_conj : "(0::int) < b ==> 0 \<le> a mod b & a mod b < b"
 apply (cut_tac a = a and b = b in divmod_int_correct)
-apply (auto simp add: divmod_int_rel_def mod_int_def)
+apply (auto simp add: divmod_int_rel_def prod_eq_iff)
 done
 
 lemmas pos_mod_sign [simp] = pos_mod_conj [THEN conjunct1]
@@ -1450,14 +1463,14 @@
 
 lemma neg_mod_conj : "b < (0::int) ==> a mod b \<le> 0 & b < a mod b"
 apply (cut_tac a = a and b = b in divmod_int_correct)
-apply (auto simp add: divmod_int_rel_def div_int_def mod_int_def)
+apply (auto simp add: divmod_int_rel_def prod_eq_iff)
 done
 
 lemmas neg_mod_sign [simp] = neg_mod_conj [THEN conjunct1]
    and neg_mod_bound [simp] = neg_mod_conj [THEN conjunct2]
 
 
-subsubsection{*General Properties of div and mod*}
+subsubsection {* General Properties of div and mod *}
 
 lemma divmod_int_rel_div_mod: "b \<noteq> 0 ==> divmod_int_rel a b (a div b, a mod b)"
 apply (cut_tac a = a and b = b in zmod_zdiv_equality)
@@ -1521,7 +1534,7 @@
 done
 
 
-subsubsection{*Laws for div and mod with Unary Minus*}
+subsubsection {* Laws for div and mod with Unary Minus *}
 
 lemma zminus1_lemma:
      "divmod_int_rel a b (q, r)
@@ -1569,7 +1582,7 @@
   unfolding zmod_zminus2_eq_if by auto 
 
 
-subsubsection{*Division of a Number by Itself*}
+subsubsection {* Division of a Number by Itself *}
 
 lemma self_quotient_aux1: "[| (0::int) < a; a = r + a*q; r < a |] ==> 1 \<le> q"
 apply (subgoal_tac "0 < a*q")
@@ -1605,7 +1618,7 @@
 done
 
 
-subsubsection{*Computation of Division and Remainder*}
+subsubsection {* Computation of Division and Remainder *}
 
 lemma zdiv_zero [simp]: "(0::int) div b = 0"
 by (simp add: div_int_def divmod_int_def)
@@ -1748,7 +1761,7 @@
 lemmas negDivAlg_eqn_1_number_of [simp] = negDivAlg_eqn [of concl: 1 "number_of w"] for w
 
 
-subsubsection{*Monotonicity in the First Argument (Dividend)*}
+subsubsection {* Monotonicity in the First Argument (Dividend) *}
 
 lemma zdiv_mono1: "[| a \<le> a';  0 < (b::int) |] ==> a div b \<le> a' div b"
 apply (cut_tac a = a and b = b in zmod_zdiv_equality)
@@ -1767,7 +1780,7 @@
 done
 
 
-subsubsection{*Monotonicity in the Second Argument (Divisor)*}
+subsubsection {* Monotonicity in the Second Argument (Divisor) *}
 
 lemma q_pos_lemma:
      "[| 0 \<le> b'*q' + r'; r' < b';  0 < b' |] ==> 0 \<le> (q'::int)"
@@ -1829,7 +1842,7 @@
 done
 
 
-subsubsection{*More Algebraic Laws for div and mod*}
+subsubsection {* More Algebraic Laws for div and mod *}
 
 text{*proving (a*b) div c = a * (b div c) + a * (b mod c) *}
 
@@ -1929,7 +1942,7 @@
 lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1]
 
 
-subsubsection{*Proving  @{term "a div (b*c) = (a div b) div c"} *}
+subsubsection {* Proving  @{term "a div (b*c) = (a div b) div c"} *}
 
 (*The condition c>0 seems necessary.  Consider that 7 div ~6 = ~2 but
   7 div 2 div ~3 = 3 div ~3 = ~1.  The subcase (a div b) mod c = 0 seems
@@ -1990,7 +2003,7 @@
 done
 
 
-subsubsection {*Splitting Rules for div and mod*}
+subsubsection {* Splitting Rules for div and mod *}
 
 text{*The proofs of the two lemmas below are essentially identical*}
 
@@ -2051,7 +2064,7 @@
 declare split_zmod [of _ _ "number_of k", arith_split] for k
 
 
-subsubsection{*Speeding up the Division Algorithm with Shifting*}
+subsubsection {* Speeding up the Division Algorithm with Shifting *}
 
 text{*computing div by shifting *}
 
@@ -2105,7 +2118,7 @@
 done
 
 
-subsubsection{*Computing mod by Shifting (proofs resemble those for div)*}
+subsubsection {* Computing mod by Shifting (proofs resemble those for div) *}
 
 lemma pos_zmod_mult_2:
   fixes a b :: int
@@ -2169,7 +2182,7 @@
 qed
 
 
-subsubsection{*Quotients of Signs*}
+subsubsection {* Quotients of Signs *}
 
 lemma div_neg_pos_less0: "[| a < (0::int);  0 < b |] ==> a div b < 0"
 apply (subgoal_tac "a div b \<le> -1", force)
@@ -2225,7 +2238,6 @@
 using int_one_le_iff_zero_less[of "a div b"] zdiv_mono1[of b a b]apply simp
 done
 
-
 lemma zmod_le_nonneg_dividend: "(m::int) \<ge> 0 ==> m mod k \<le> m"
 apply (rule split_zmod[THEN iffD2])
 apply(fastforce dest: q_pos_lemma intro: split_mult_pos_le)
@@ -2384,7 +2396,7 @@
 proof-
   from xy have th: "int x - int y = int (x - y)" by simp 
   from xyn have "int x mod int n = int y mod int n" 
-    by (simp add: zmod_int[symmetric])
+    by (simp add: zmod_int [symmetric])
   hence "int n dvd int x - int y" by (simp only: zmod_eq_dvd_iff[symmetric]) 
   hence "n dvd x - y" by (simp add: th zdvd_int)
   then show ?thesis using xy unfolding dvd_def apply clarsimp apply (rule_tac x="k" in exI) by arith