src/HOL/Divides.thy
changeset 47141 02d6b816e4b3
parent 47140 97c3676c5c94
child 47142 d64fa2ca54b8
     1.1 --- a/src/HOL/Divides.thy	Tue Mar 27 11:45:02 2012 +0200
     1.2 +++ b/src/HOL/Divides.thy	Tue Mar 27 12:42:54 2012 +0200
     1.3 @@ -1352,26 +1352,73 @@
     1.4  by (force simp add: linorder_neq_iff divmod_int_rel_0 divmod_int_def divmod_int_rel_neg
     1.5                      posDivAlg_correct negDivAlg_correct)
     1.6  
     1.7 +lemma divmod_int_unique:
     1.8 +  assumes "divmod_int_rel a b qr" 
     1.9 +  shows "divmod_int a b = qr"
    1.10 +  using assms divmod_int_correct [of a b]
    1.11 +  using unique_quotient [of a b] unique_remainder [of a b]
    1.12 +  by (metis pair_collapse)
    1.13 +
    1.14 +lemma divmod_int_rel_div_mod: "divmod_int_rel a b (a div b, a mod b)"
    1.15 +  using divmod_int_correct by (simp add: divmod_int_mod_div)
    1.16 +
    1.17 +lemma div_int_unique: "divmod_int_rel a b (q, r) \<Longrightarrow> a div b = q"
    1.18 +  by (simp add: divmod_int_rel_div_mod [THEN unique_quotient])
    1.19 +
    1.20 +lemma mod_int_unique: "divmod_int_rel a b (q, r) \<Longrightarrow> a mod b = r"
    1.21 +  by (simp add: divmod_int_rel_div_mod [THEN unique_remainder])
    1.22 +
    1.23 +instance int :: ring_div
    1.24 +proof
    1.25 +  fix a b :: int
    1.26 +  show "a div b * b + a mod b = a"
    1.27 +    using divmod_int_rel_div_mod [of a b]
    1.28 +    unfolding divmod_int_rel_def by (simp add: mult_commute)
    1.29 +next
    1.30 +  fix a b c :: int
    1.31 +  assume "b \<noteq> 0"
    1.32 +  hence "divmod_int_rel (a + c * b) b (c + a div b, a mod b)"
    1.33 +    using divmod_int_rel_div_mod [of a b]
    1.34 +    unfolding divmod_int_rel_def by (auto simp: algebra_simps)
    1.35 +  thus "(a + c * b) div b = c + a div b"
    1.36 +    by (rule div_int_unique)
    1.37 +next
    1.38 +  fix a b c :: int
    1.39 +  assume "c \<noteq> 0"
    1.40 +  hence "\<And>q r. divmod_int_rel a b (q, r)
    1.41 +    \<Longrightarrow> divmod_int_rel (c * a) (c * b) (q, c * r)"
    1.42 +    unfolding divmod_int_rel_def
    1.43 +    by - (rule linorder_cases [of 0 b], auto simp: algebra_simps
    1.44 +      mult_less_0_iff zero_less_mult_iff mult_strict_right_mono
    1.45 +      mult_strict_right_mono_neg zero_le_mult_iff mult_le_0_iff)
    1.46 +  hence "divmod_int_rel (c * a) (c * b) (a div b, c * (a mod b))"
    1.47 +    using divmod_int_rel_div_mod [of a b] .
    1.48 +  thus "(c * a) div (c * b) = a div b"
    1.49 +    by (rule div_int_unique)
    1.50 +next
    1.51 +  fix a :: int show "a div 0 = 0"
    1.52 +    by (rule div_int_unique, simp add: divmod_int_rel_def)
    1.53 +next
    1.54 +  fix a :: int show "0 div a = 0"
    1.55 +    by (rule div_int_unique, auto simp add: divmod_int_rel_def)
    1.56 +qed
    1.57 +
    1.58  text{*Arbitrary definitions for division by zero.  Useful to simplify 
    1.59      certain equations.*}
    1.60  
    1.61  lemma DIVISION_BY_ZERO [simp]: "a div (0::int) = 0 & a mod (0::int) = a"
    1.62 -by (simp add: div_int_def mod_int_def divmod_int_def posDivAlg.simps)  
    1.63 -
    1.64 +  by simp (* FIXME: delete *)
    1.65  
    1.66  text{*Basic laws about division and remainder*}
    1.67  
    1.68  lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)"
    1.69 -apply (case_tac "b = 0", simp)
    1.70 -apply (cut_tac a = a and b = b in divmod_int_correct)
    1.71 -apply (auto simp add: divmod_int_rel_def prod_eq_iff)
    1.72 -done
    1.73 +  by (fact mod_div_equality2 [symmetric])
    1.74  
    1.75  lemma zdiv_zmod_equality: "(b * (a div b) + (a mod b)) + k = (a::int)+k"
    1.76 -by(simp add: zmod_zdiv_equality[symmetric])
    1.77 +  by (fact div_mod_equality2)
    1.78  
    1.79  lemma zdiv_zmod_equality2: "((a div b) * b + (a mod b)) + k = (a::int)+k"
    1.80 -by(simp add: mult_commute zmod_zdiv_equality[symmetric])
    1.81 +  by (fact div_mod_equality)
    1.82  
    1.83  text {* Tool setup *}
    1.84  
    1.85 @@ -1396,18 +1443,16 @@
    1.86  
    1.87  simproc_setup cancel_div_mod_int ("(k::int) + l") = {* K Cancel_Div_Mod_Int.proc *}
    1.88  
    1.89 -lemma pos_mod_conj : "(0::int) < b ==> 0 \<le> a mod b & a mod b < b"
    1.90 -apply (cut_tac a = a and b = b in divmod_int_correct)
    1.91 -apply (auto simp add: divmod_int_rel_def prod_eq_iff)
    1.92 -done
    1.93 +lemma pos_mod_conj: "(0::int) < b \<Longrightarrow> 0 \<le> a mod b \<and> a mod b < b"
    1.94 +  using divmod_int_correct [of a b]
    1.95 +  by (auto simp add: divmod_int_rel_def prod_eq_iff)
    1.96  
    1.97  lemmas pos_mod_sign [simp] = pos_mod_conj [THEN conjunct1]
    1.98     and pos_mod_bound [simp] = pos_mod_conj [THEN conjunct2]
    1.99  
   1.100 -lemma neg_mod_conj : "b < (0::int) ==> a mod b \<le> 0 & b < a mod b"
   1.101 -apply (cut_tac a = a and b = b in divmod_int_correct)
   1.102 -apply (auto simp add: divmod_int_rel_def prod_eq_iff)
   1.103 -done
   1.104 +lemma neg_mod_conj: "b < (0::int) \<Longrightarrow> a mod b \<le> 0 \<and> b < a mod b"
   1.105 +  using divmod_int_correct [of a b]
   1.106 +  by (auto simp add: divmod_int_rel_def prod_eq_iff)
   1.107  
   1.108  lemmas neg_mod_sign [simp] = neg_mod_conj [THEN conjunct1]
   1.109     and neg_mod_bound [simp] = neg_mod_conj [THEN conjunct2]
   1.110 @@ -1415,17 +1460,6 @@
   1.111  
   1.112  subsubsection {* General Properties of div and mod *}
   1.113  
   1.114 -lemma divmod_int_rel_div_mod: "divmod_int_rel a b (a div b, a mod b)"
   1.115 -apply (cut_tac a = a and b = b in zmod_zdiv_equality)
   1.116 -apply (force simp add: divmod_int_rel_def linorder_neq_iff)
   1.117 -done
   1.118 -
   1.119 -lemma div_int_unique: "[| divmod_int_rel a b (q, r) |] ==> a div b = q"
   1.120 -by (simp add: divmod_int_rel_div_mod [THEN unique_quotient])
   1.121 -
   1.122 -lemma mod_int_unique: "[| divmod_int_rel a b (q, r) |] ==> a mod b = r"
   1.123 -by (simp add: divmod_int_rel_div_mod [THEN unique_remainder])
   1.124 -
   1.125  lemma div_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a div b = 0"
   1.126  apply (rule div_int_unique)
   1.127  apply (auto simp add: divmod_int_rel_def)
   1.128 @@ -1463,16 +1497,11 @@
   1.129  
   1.130  (*Simpler laws such as -a div b = -(a div b) FAIL, but see just below*)
   1.131  lemma zdiv_zminus_zminus [simp]: "(-a) div (-b) = a div (b::int)"
   1.132 -apply (simp add: divmod_int_rel_div_mod [THEN divmod_int_rel_neg, simplified, 
   1.133 -                                 THEN div_int_unique, THEN sym])
   1.134 -
   1.135 -done
   1.136 +  using div_mult_mult1 [of "-1" a b] by simp (* FIXME: generalize *)
   1.137  
   1.138  (*Simpler laws such as -a mod b = -(a mod b) FAIL, but see just below*)
   1.139  lemma zmod_zminus_zminus [simp]: "(-a) mod (-b) = - (a mod (b::int))"
   1.140 -apply (subst divmod_int_rel_div_mod [THEN divmod_int_rel_neg, simplified, THEN mod_int_unique],
   1.141 -       auto)
   1.142 -done
   1.143 +  using mod_mult_mult1 [of "-1" a b] by simp (* FIXME: generalize *)
   1.144  
   1.145  
   1.146  subsubsection {* Laws for div and mod with Unary Minus *}
   1.147 @@ -1502,10 +1531,10 @@
   1.148    unfolding zmod_zminus1_eq_if by auto
   1.149  
   1.150  lemma zdiv_zminus2: "a div (-b) = (-a::int) div b"
   1.151 -by (cut_tac a = "-a" in zdiv_zminus_zminus, auto)
   1.152 +  using zdiv_zminus_zminus [of "-a" b] by simp (* FIXME: generalize *)
   1.153  
   1.154  lemma zmod_zminus2: "a mod (-b) = - ((-a::int) mod b)"
   1.155 -by (cut_tac a = "-a" and b = b in zmod_zminus_zminus, auto)
   1.156 +  using zmod_zminus_zminus [of "-a" b] by simp (* FIXME: generalize*)
   1.157  
   1.158  lemma zdiv_zminus2_eq_if:
   1.159       "b \<noteq> (0::int)  
   1.160 @@ -1550,25 +1579,23 @@
   1.161  done
   1.162  
   1.163  lemma zdiv_self [simp]: "a \<noteq> 0 ==> a div a = (1::int)"
   1.164 -by (simp add: divmod_int_rel_div_mod [THEN self_quotient])
   1.165 +  by (fact div_self) (* FIXME: delete *)
   1.166  
   1.167  (*Here we have 0 mod 0 = 0, also assumed by Knuth (who puts m mod 0 = 0) *)
   1.168  lemma zmod_self [simp]: "a mod a = (0::int)"
   1.169 -apply (case_tac "a = 0", simp)
   1.170 -apply (simp add: divmod_int_rel_div_mod [THEN self_remainder])
   1.171 -done
   1.172 +  by (fact mod_self) (* FIXME: delete *)
   1.173  
   1.174  
   1.175  subsubsection {* Computation of Division and Remainder *}
   1.176  
   1.177  lemma zdiv_zero [simp]: "(0::int) div b = 0"
   1.178 -by (simp add: div_int_def divmod_int_def)
   1.179 +  by (fact div_0) (* FIXME: delete *)
   1.180  
   1.181  lemma div_eq_minus1: "(0::int) < b ==> -1 div b = -1"
   1.182  by (simp add: div_int_def divmod_int_def)
   1.183  
   1.184  lemma zmod_zero [simp]: "(0::int) mod b = 0"
   1.185 -by (simp add: mod_int_def divmod_int_def)
   1.186 +  by (fact mod_0) (* FIXME: delete *)
   1.187  
   1.188  lemma zmod_minus1: "(0::int) < b ==> -1 mod b = b - 1"
   1.189  by (simp add: mod_int_def divmod_int_def)
   1.190 @@ -1686,10 +1713,11 @@
   1.191  apply (cut_tac a = a and b = "-1" in neg_mod_sign)
   1.192  apply (cut_tac [2] a = a and b = "-1" in neg_mod_bound)
   1.193  apply (auto simp del: neg_mod_sign neg_mod_bound)
   1.194 -done
   1.195 +done (* FIXME: generalize *)
   1.196  
   1.197  lemma zdiv_minus1_right [simp]: "a div (-1::int) = -a"
   1.198  by (cut_tac a = a and b = "-1" in zmod_zdiv_equality, auto)
   1.199 +(* FIXME: generalize *)
   1.200  
   1.201  (** The last remaining special cases for constant arithmetic:
   1.202      1 div z and 1 mod z **)
   1.203 @@ -1811,14 +1839,10 @@
   1.204  done
   1.205  
   1.206  lemma zmod_zmult1_eq: "(a*b) mod c = a*(b mod c) mod (c::int)"
   1.207 -apply (case_tac "c = 0", simp)
   1.208 -apply (blast intro: divmod_int_rel_div_mod [THEN zmult1_lemma, THEN mod_int_unique])
   1.209 -done
   1.210 +  by (fact mod_mult_right_eq) (* FIXME: delete *)
   1.211  
   1.212  lemma zmod_zdiv_trivial: "(a mod b) div b = (0::int)"
   1.213 -apply (case_tac "b = 0", simp)
   1.214 -apply (auto simp add: linorder_neq_iff div_pos_pos_trivial div_neg_neg_trivial)
   1.215 -done
   1.216 +  by (fact mod_div_trivial) (* FIXME: delete *)
   1.217  
   1.218  text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *}
   1.219  
   1.220 @@ -1834,33 +1858,6 @@
   1.221  apply (blast intro: zadd1_lemma [OF divmod_int_rel_div_mod divmod_int_rel_div_mod] div_int_unique)
   1.222  done
   1.223  
   1.224 -instance int :: ring_div
   1.225 -proof
   1.226 -  fix a b c :: int
   1.227 -  assume not0: "b \<noteq> 0"
   1.228 -  show "(a + c * b) div b = c + a div b"
   1.229 -    unfolding zdiv_zadd1_eq [of a "c * b"] using not0 
   1.230 -      by (simp add: zmod_zmult1_eq zmod_zdiv_trivial zdiv_zmult1_eq)
   1.231 -next
   1.232 -  fix a b c :: int
   1.233 -  assume "a \<noteq> 0"
   1.234 -  then show "(a * b) div (a * c) = b div c"
   1.235 -  proof (cases "b \<noteq> 0 \<and> c \<noteq> 0")
   1.236 -    case False then show ?thesis by auto
   1.237 -  next
   1.238 -    case True then have "b \<noteq> 0" and "c \<noteq> 0" by auto
   1.239 -    with `a \<noteq> 0`
   1.240 -    have "\<And>q r. divmod_int_rel b c (q, r) \<Longrightarrow> divmod_int_rel (a * b) (a * c) (q, a * r)"
   1.241 -      apply (auto simp add: divmod_int_rel_def split: split_if_asm)
   1.242 -      apply (auto simp add: algebra_simps)
   1.243 -      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)
   1.244 -      done
   1.245 -    moreover with `c \<noteq> 0` divmod_int_rel_div_mod have "divmod_int_rel b c (b div c, b mod c)" by auto
   1.246 -    ultimately have "divmod_int_rel (a * b) (a * c) (b div c, a * (b mod c))" .
   1.247 -    from this show ?thesis by (rule div_int_unique)
   1.248 -  qed
   1.249 -qed auto
   1.250 -
   1.251  lemma posDivAlg_div_mod:
   1.252    assumes "k \<ge> 0"
   1.253    and "l \<ge> 0"
   1.254 @@ -1896,8 +1893,7 @@
   1.255  
   1.256  lemma zmod_zdiv_equality':
   1.257    "(m\<Colon>int) mod n = m - (m div n) * n"
   1.258 -  by (rule_tac P="%x. m mod n = x - (m div n) * n" in subst [OF mod_div_equality [of _ n]])
   1.259 -    arith
   1.260 +  using mod_div_equality [of m n] by arith
   1.261  
   1.262  
   1.263  subsubsection {* Proving  @{term "a div (b*c) = (a div b) div c"} *}