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"} *}