# HG changeset patch
# User huffman
# Date 1332844974 -7200
# Node ID 02d6b816e4b30d94d70aa6ed0594e6cc7f894449
# Parent  97c3676c5c9452c793059ecf0f28a27edd5c268f
move int::ring_div instance upward, simplify several proofs

diff -r 97c3676c5c94 -r 02d6b816e4b3 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Tue Mar 27 11:45:02 2012 +0200
+++ b/src/HOL/Divides.thy	Tue Mar 27 12:42:54 2012 +0200
@@ -1352,26 +1352,73 @@
 by (force simp add: linorder_neq_iff divmod_int_rel_0 divmod_int_def divmod_int_rel_neg
                     posDivAlg_correct negDivAlg_correct)
 
+lemma divmod_int_unique:
+  assumes "divmod_int_rel a b qr" 
+  shows "divmod_int a b = qr"
+  using assms divmod_int_correct [of a b]
+  using unique_quotient [of a b] unique_remainder [of a b]
+  by (metis pair_collapse)
+
+lemma divmod_int_rel_div_mod: "divmod_int_rel a b (a div b, a mod b)"
+  using divmod_int_correct by (simp add: divmod_int_mod_div)
+
+lemma div_int_unique: "divmod_int_rel a b (q, r) \<Longrightarrow> a div b = q"
+  by (simp add: divmod_int_rel_div_mod [THEN unique_quotient])
+
+lemma mod_int_unique: "divmod_int_rel a b (q, r) \<Longrightarrow> a mod b = r"
+  by (simp add: divmod_int_rel_div_mod [THEN unique_remainder])
+
+instance int :: ring_div
+proof
+  fix a b :: int
+  show "a div b * b + a mod b = a"
+    using divmod_int_rel_div_mod [of a b]
+    unfolding divmod_int_rel_def by (simp add: mult_commute)
+next
+  fix a b c :: int
+  assume "b \<noteq> 0"
+  hence "divmod_int_rel (a + c * b) b (c + a div b, a mod b)"
+    using divmod_int_rel_div_mod [of a b]
+    unfolding divmod_int_rel_def by (auto simp: algebra_simps)
+  thus "(a + c * b) div b = c + a div b"
+    by (rule div_int_unique)
+next
+  fix a b c :: int
+  assume "c \<noteq> 0"
+  hence "\<And>q r. divmod_int_rel a b (q, r)
+    \<Longrightarrow> divmod_int_rel (c * a) (c * b) (q, c * r)"
+    unfolding divmod_int_rel_def
+    by - (rule linorder_cases [of 0 b], auto simp: algebra_simps
+      mult_less_0_iff zero_less_mult_iff mult_strict_right_mono
+      mult_strict_right_mono_neg zero_le_mult_iff mult_le_0_iff)
+  hence "divmod_int_rel (c * a) (c * b) (a div b, c * (a mod b))"
+    using divmod_int_rel_div_mod [of a b] .
+  thus "(c * a) div (c * b) = a div b"
+    by (rule div_int_unique)
+next
+  fix a :: int show "a div 0 = 0"
+    by (rule div_int_unique, simp add: divmod_int_rel_def)
+next
+  fix a :: int show "0 div a = 0"
+    by (rule div_int_unique, auto simp add: divmod_int_rel_def)
+qed
+
 text{*Arbitrary definitions for division by zero.  Useful to simplify 
     certain equations.*}
 
 lemma DIVISION_BY_ZERO [simp]: "a div (0::int) = 0 & a mod (0::int) = a"
-by (simp add: div_int_def mod_int_def divmod_int_def posDivAlg.simps)  
-
+  by simp (* FIXME: delete *)
 
 text{*Basic laws about division and remainder*}
 
 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 prod_eq_iff)
-done
+  by (fact mod_div_equality2 [symmetric])
 
 lemma zdiv_zmod_equality: "(b * (a div b) + (a mod b)) + k = (a::int)+k"
-by(simp add: zmod_zdiv_equality[symmetric])
+  by (fact div_mod_equality2)
 
 lemma zdiv_zmod_equality2: "((a div b) * b + (a mod b)) + k = (a::int)+k"
-by(simp add: mult_commute zmod_zdiv_equality[symmetric])
+  by (fact div_mod_equality)
 
 text {* Tool setup *}
 
@@ -1396,18 +1443,16 @@
 
 simproc_setup cancel_div_mod_int ("(k::int) + l") = {* K Cancel_Div_Mod_Int.proc *}
 
-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 prod_eq_iff)
-done
+lemma pos_mod_conj: "(0::int) < b \<Longrightarrow> 0 \<le> a mod b \<and> a mod b < b"
+  using divmod_int_correct [of a b]
+  by (auto simp add: divmod_int_rel_def prod_eq_iff)
 
 lemmas pos_mod_sign [simp] = pos_mod_conj [THEN conjunct1]
    and pos_mod_bound [simp] = pos_mod_conj [THEN conjunct2]
 
-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 prod_eq_iff)
-done
+lemma neg_mod_conj: "b < (0::int) \<Longrightarrow> a mod b \<le> 0 \<and> b < a mod b"
+  using divmod_int_correct [of a b]
+  by (auto simp add: divmod_int_rel_def prod_eq_iff)
 
 lemmas neg_mod_sign [simp] = neg_mod_conj [THEN conjunct1]
    and neg_mod_bound [simp] = neg_mod_conj [THEN conjunct2]
@@ -1415,17 +1460,6 @@
 
 subsubsection {* General Properties of div and mod *}
 
-lemma divmod_int_rel_div_mod: "divmod_int_rel a b (a div b, a mod b)"
-apply (cut_tac a = a and b = b in zmod_zdiv_equality)
-apply (force simp add: divmod_int_rel_def linorder_neq_iff)
-done
-
-lemma div_int_unique: "[| divmod_int_rel a b (q, r) |] ==> a div b = q"
-by (simp add: divmod_int_rel_div_mod [THEN unique_quotient])
-
-lemma mod_int_unique: "[| divmod_int_rel a b (q, r) |] ==> a mod b = r"
-by (simp add: divmod_int_rel_div_mod [THEN unique_remainder])
-
 lemma div_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a div b = 0"
 apply (rule div_int_unique)
 apply (auto simp add: divmod_int_rel_def)
@@ -1463,16 +1497,11 @@
 
 (*Simpler laws such as -a div b = -(a div b) FAIL, but see just below*)
 lemma zdiv_zminus_zminus [simp]: "(-a) div (-b) = a div (b::int)"
-apply (simp add: divmod_int_rel_div_mod [THEN divmod_int_rel_neg, simplified, 
-                                 THEN div_int_unique, THEN sym])
-
-done
+  using div_mult_mult1 [of "-1" a b] by simp (* FIXME: generalize *)
 
 (*Simpler laws such as -a mod b = -(a mod b) FAIL, but see just below*)
 lemma zmod_zminus_zminus [simp]: "(-a) mod (-b) = - (a mod (b::int))"
-apply (subst divmod_int_rel_div_mod [THEN divmod_int_rel_neg, simplified, THEN mod_int_unique],
-       auto)
-done
+  using mod_mult_mult1 [of "-1" a b] by simp (* FIXME: generalize *)
 
 
 subsubsection {* Laws for div and mod with Unary Minus *}
@@ -1502,10 +1531,10 @@
   unfolding zmod_zminus1_eq_if by auto
 
 lemma zdiv_zminus2: "a div (-b) = (-a::int) div b"
-by (cut_tac a = "-a" in zdiv_zminus_zminus, auto)
+  using zdiv_zminus_zminus [of "-a" b] by simp (* FIXME: generalize *)
 
 lemma zmod_zminus2: "a mod (-b) = - ((-a::int) mod b)"
-by (cut_tac a = "-a" and b = b in zmod_zminus_zminus, auto)
+  using zmod_zminus_zminus [of "-a" b] by simp (* FIXME: generalize*)
 
 lemma zdiv_zminus2_eq_if:
      "b \<noteq> (0::int)  
@@ -1550,25 +1579,23 @@
 done
 
 lemma zdiv_self [simp]: "a \<noteq> 0 ==> a div a = (1::int)"
-by (simp add: divmod_int_rel_div_mod [THEN self_quotient])
+  by (fact div_self) (* FIXME: delete *)
 
 (*Here we have 0 mod 0 = 0, also assumed by Knuth (who puts m mod 0 = 0) *)
 lemma zmod_self [simp]: "a mod a = (0::int)"
-apply (case_tac "a = 0", simp)
-apply (simp add: divmod_int_rel_div_mod [THEN self_remainder])
-done
+  by (fact mod_self) (* FIXME: delete *)
 
 
 subsubsection {* Computation of Division and Remainder *}
 
 lemma zdiv_zero [simp]: "(0::int) div b = 0"
-by (simp add: div_int_def divmod_int_def)
+  by (fact div_0) (* FIXME: delete *)
 
 lemma div_eq_minus1: "(0::int) < b ==> -1 div b = -1"
 by (simp add: div_int_def divmod_int_def)
 
 lemma zmod_zero [simp]: "(0::int) mod b = 0"
-by (simp add: mod_int_def divmod_int_def)
+  by (fact mod_0) (* FIXME: delete *)
 
 lemma zmod_minus1: "(0::int) < b ==> -1 mod b = b - 1"
 by (simp add: mod_int_def divmod_int_def)
@@ -1686,10 +1713,11 @@
 apply (cut_tac a = a and b = "-1" in neg_mod_sign)
 apply (cut_tac [2] a = a and b = "-1" in neg_mod_bound)
 apply (auto simp del: neg_mod_sign neg_mod_bound)
-done
+done (* FIXME: generalize *)
 
 lemma zdiv_minus1_right [simp]: "a div (-1::int) = -a"
 by (cut_tac a = a and b = "-1" in zmod_zdiv_equality, auto)
+(* FIXME: generalize *)
 
 (** The last remaining special cases for constant arithmetic:
     1 div z and 1 mod z **)
@@ -1811,14 +1839,10 @@
 done
 
 lemma zmod_zmult1_eq: "(a*b) mod c = a*(b mod c) mod (c::int)"
-apply (case_tac "c = 0", simp)
-apply (blast intro: divmod_int_rel_div_mod [THEN zmult1_lemma, THEN mod_int_unique])
-done
+  by (fact mod_mult_right_eq) (* FIXME: delete *)
 
 lemma zmod_zdiv_trivial: "(a mod b) div b = (0::int)"
-apply (case_tac "b = 0", simp)
-apply (auto simp add: linorder_neq_iff div_pos_pos_trivial div_neg_neg_trivial)
-done
+  by (fact mod_div_trivial) (* FIXME: delete *)
 
 text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *}
 
@@ -1834,33 +1858,6 @@
 apply (blast intro: zadd1_lemma [OF divmod_int_rel_div_mod divmod_int_rel_div_mod] div_int_unique)
 done
 
-instance int :: ring_div
-proof
-  fix a b c :: int
-  assume not0: "b \<noteq> 0"
-  show "(a + c * b) div b = c + a div b"
-    unfolding zdiv_zadd1_eq [of a "c * b"] using not0 
-      by (simp add: zmod_zmult1_eq zmod_zdiv_trivial zdiv_zmult1_eq)
-next
-  fix a b c :: int
-  assume "a \<noteq> 0"
-  then show "(a * b) div (a * c) = b div c"
-  proof (cases "b \<noteq> 0 \<and> c \<noteq> 0")
-    case False then show ?thesis by auto
-  next
-    case True then have "b \<noteq> 0" and "c \<noteq> 0" by auto
-    with `a \<noteq> 0`
-    have "\<And>q r. divmod_int_rel b c (q, r) \<Longrightarrow> divmod_int_rel (a * b) (a * c) (q, a * r)"
-      apply (auto simp add: divmod_int_rel_def split: split_if_asm)
-      apply (auto simp add: algebra_simps)
-      apply (auto simp add: zero_less_mult_iff zero_le_mult_iff mult_le_0_iff mult_commute [of a] mult_less_cancel_right mult_less_0_iff)
-      done
-    moreover with `c \<noteq> 0` divmod_int_rel_div_mod have "divmod_int_rel b c (b div c, b mod c)" by auto
-    ultimately have "divmod_int_rel (a * b) (a * c) (b div c, a * (b mod c))" .
-    from this show ?thesis by (rule div_int_unique)
-  qed
-qed auto
-
 lemma posDivAlg_div_mod:
   assumes "k \<ge> 0"
   and "l \<ge> 0"
@@ -1896,8 +1893,7 @@
 
 lemma zmod_zdiv_equality':
   "(m\<Colon>int) mod n = m - (m div n) * n"
-  by (rule_tac P="%x. m mod n = x - (m div n) * n" in subst [OF mod_div_equality [of _ n]])
-    arith
+  using mod_div_equality [of m n] by arith
 
 
 subsubsection {* Proving  @{term "a div (b*c) = (a div b) div c"} *}