author huffman Mon Feb 20 14:23:46 2012 +0100 (2012-02-20) changeset 46551 866bce5442a3 parent 46547 d1dcb91a512e child 46552 5d33a3269029
simplify projections on simultaneous computations of div and mod; tuned structure (from Florian Haftmann)
 src/HOL/Divides.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Divides.thy	Mon Feb 20 12:37:17 2012 +0100
1.2 +++ b/src/HOL/Divides.thy	Mon Feb 20 14:23:46 2012 +0100
1.3 @@ -523,9 +523,6 @@
1.4    means of @{const divmod_nat_rel}:
1.5  *}
1.6
1.7 -instantiation nat :: semiring_div
1.8 -begin
1.9 -
1.10  definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
1.11    "divmod_nat m n = (THE qr. divmod_nat_rel m n qr)"
1.12
1.13 @@ -543,28 +540,39 @@
1.14    shows "divmod_nat m n = qr"
1.15    using assms by (auto intro: divmod_nat_rel_unique divmod_nat_rel_divmod_nat)
1.16
1.17 +instantiation nat :: semiring_div
1.18 +begin
1.19 +
1.20  definition div_nat where
1.21    "m div n = fst (divmod_nat m n)"
1.22
1.23 +lemma fst_divmod_nat [simp]:
1.24 +  "fst (divmod_nat m n) = m div n"
1.25 +  by (simp add: div_nat_def)
1.26 +
1.27  definition mod_nat where
1.28    "m mod n = snd (divmod_nat m n)"
1.29
1.30 +lemma snd_divmod_nat [simp]:
1.31 +  "snd (divmod_nat m n) = m mod n"
1.32 +  by (simp add: mod_nat_def)
1.33 +
1.34  lemma divmod_nat_div_mod:
1.35    "divmod_nat m n = (m div n, m mod n)"
1.36 -  unfolding div_nat_def mod_nat_def by simp
1.37 +  by (simp add: prod_eq_iff)
1.38
1.39  lemma div_eq:
1.40    assumes "divmod_nat_rel m n (q, r)"
1.41    shows "m div n = q"
1.42 -  using assms by (auto dest: divmod_nat_eq simp add: divmod_nat_div_mod)
1.43 +  using assms by (auto dest!: divmod_nat_eq simp add: prod_eq_iff)
1.44
1.45  lemma mod_eq:
1.46    assumes "divmod_nat_rel m n (q, r)"
1.47    shows "m mod n = r"
1.48 -  using assms by (auto dest: divmod_nat_eq simp add: divmod_nat_div_mod)
1.49 +  using assms by (auto dest!: divmod_nat_eq simp add: prod_eq_iff)
1.50
1.51  lemma divmod_nat_rel: "divmod_nat_rel m n (m div n, m mod n)"
1.52 -  by (simp add: div_nat_def mod_nat_def divmod_nat_rel_divmod_nat)
1.53 +  using divmod_nat_rel_divmod_nat by (simp add: divmod_nat_div_mod)
1.54
1.55  lemma divmod_nat_zero:
1.56    "divmod_nat m 0 = (0, m)"
1.57 @@ -613,25 +621,25 @@
1.58    fixes m n :: nat
1.59    assumes "m < n"
1.60    shows "m div n = 0"
1.61 -  using assms divmod_nat_base divmod_nat_div_mod by simp
1.62 +  using assms divmod_nat_base by (simp add: prod_eq_iff)
1.63
1.64  lemma le_div_geq:
1.65    fixes m n :: nat
1.66    assumes "0 < n" and "n \<le> m"
1.67    shows "m div n = Suc ((m - n) div n)"
1.68 -  using assms divmod_nat_step divmod_nat_div_mod by simp
1.69 +  using assms divmod_nat_step by (simp add: prod_eq_iff)
1.70
1.71  lemma mod_less [simp]:
1.72    fixes m n :: nat
1.73    assumes "m < n"
1.74    shows "m mod n = m"
1.75 -  using assms divmod_nat_base divmod_nat_div_mod by simp
1.76 +  using assms divmod_nat_base by (simp add: prod_eq_iff)
1.77
1.78  lemma le_mod_geq:
1.79    fixes m n :: nat
1.80    assumes "n \<le> m"
1.81    shows "m mod n = (m - n) mod n"
1.82 -  using assms divmod_nat_step divmod_nat_div_mod by (cases "n = 0") simp_all
1.83 +  using assms divmod_nat_step by (cases "n = 0") (simp_all add: prod_eq_iff)
1.84
1.85  instance proof -
1.86    have [simp]: "\<And>n::nat. n div 0 = 0"
1.87 @@ -673,8 +681,7 @@
1.88
1.89  lemma divmod_nat_if [code]: "divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
1.90    let (q, r) = divmod_nat (m - n) n in (Suc q, r))"
1.91 -by (simp add: divmod_nat_zero divmod_nat_base divmod_nat_step)
1.93 +  by (simp add: prod_eq_iff prod_case_beta not_less le_div_geq le_mod_geq)
1.94
1.95  text {* Simproc for cancelling @{const div} and @{const mod} *}
1.96
1.97 @@ -807,12 +814,11 @@
1.98    done
1.99
1.100
1.101 -subsubsection{*Further Facts about Quotient and Remainder*}
1.102 +subsubsection {* Further Facts about Quotient and Remainder *}
1.103
1.104  lemma div_1 [simp]: "m div Suc 0 = m"
1.105  by (induct m) (simp_all add: div_geq)
1.106
1.107 -
1.108  (* Monotonicity of div in first argument *)
1.109  lemma div_le_mono [rule_format (no_asm)]:
1.110      "\<forall>m::nat. m \<le> n --> (m div k) \<le> (n div k)"
1.111 @@ -1018,7 +1024,7 @@
1.112  qed
1.113
1.114
1.115 -subsubsection {*An ``induction'' law for modulus arithmetic.*}
1.116 +subsubsection {* An ``induction'' law for modulus arithmetic. *}
1.117
1.118  lemma mod_induct_0:
1.119    assumes step: "\<forall>i<p. P i \<longrightarrow> P ((Suc i) mod p)"
1.120 @@ -1228,19 +1234,27 @@
1.121  instantiation int :: Divides.div
1.122  begin
1.123
1.124 -definition
1.125 +definition div_int where
1.126    "a div b = fst (divmod_int a b)"
1.127
1.128 -definition
1.129 +lemma fst_divmod_int [simp]:
1.130 +  "fst (divmod_int a b) = a div b"
1.131 +  by (simp add: div_int_def)
1.132 +
1.133 +definition mod_int where
1.134   "a mod b = snd (divmod_int a b)"
1.135
1.136 +lemma snd_divmod_int [simp]:
1.137 +  "snd (divmod_int a b) = a mod b"
1.138 +  by (simp add: mod_int_def)
1.139 +
1.140  instance ..
1.141
1.142  end
1.143
1.144  lemma divmod_int_mod_div:
1.145    "divmod_int p q = (p div q, p mod q)"
1.146 -  by (auto simp add: div_int_def mod_int_def)
1.147 +  by (simp add: prod_eq_iff)
1.148
1.149  text{*
1.150  Here is the division algorithm in ML:
1.151 @@ -1271,8 +1285,7 @@
1.152  *}
1.153
1.154
1.155 -
1.156 -subsubsection{*Uniqueness and Monotonicity of Quotients and Remainders*}
1.157 +subsubsection {* Uniqueness and Monotonicity of Quotients and Remainders *}
1.158
1.159  lemma unique_quotient_lemma:
1.160       "[| b*q' + r'  \<le> b*q + r;  0 \<le> r';  r' < b;  r < b |]
1.161 @@ -1312,7 +1325,7 @@
1.162  done
1.163
1.164
1.165 -subsubsection{*Correctness of @{term posDivAlg}, the Algorithm for Non-Negative Dividends*}
1.166 +subsubsection {* Correctness of @{term posDivAlg}, the Algorithm for Non-Negative Dividends *}
1.167
1.168  text{*And positive divisors*}
1.169
1.170 @@ -1347,7 +1360,7 @@
1.171    done
1.172
1.173
1.174 -subsubsection{*Correctness of @{term negDivAlg}, the Algorithm for Negative Dividends*}
1.175 +subsubsection {* Correctness of @{term negDivAlg}, the Algorithm for Negative Dividends *}
1.176
1.177  text{*And positive divisors*}
1.178
1.179 @@ -1377,7 +1390,7 @@
1.180    done
1.181
1.182
1.183 -subsubsection{*Existence Shown by Proving the Division Algorithm to be Correct*}
1.184 +subsubsection {* Existence Shown by Proving the Division Algorithm to be Correct *}
1.185
1.186  (*the case a=0*)
1.187  lemma divmod_int_rel_0: "b \<noteq> 0 ==> divmod_int_rel 0 b (0, 0)"
1.188 @@ -1411,7 +1424,7 @@
1.189  lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)"
1.190  apply (case_tac "b = 0", simp)
1.191  apply (cut_tac a = a and b = b in divmod_int_correct)
1.192 -apply (auto simp add: divmod_int_rel_def div_int_def mod_int_def)
1.193 +apply (auto simp add: divmod_int_rel_def prod_eq_iff)
1.194  done
1.195
1.196  lemma zdiv_zmod_equality: "(b * (a div b) + (a mod b)) + k = (a::int)+k"
1.197 @@ -1442,7 +1455,7 @@
1.198
1.199  lemma pos_mod_conj : "(0::int) < b ==> 0 \<le> a mod b & a mod b < b"
1.200  apply (cut_tac a = a and b = b in divmod_int_correct)
1.201 -apply (auto simp add: divmod_int_rel_def mod_int_def)
1.202 +apply (auto simp add: divmod_int_rel_def prod_eq_iff)
1.203  done
1.204
1.205  lemmas pos_mod_sign [simp] = pos_mod_conj [THEN conjunct1]
1.206 @@ -1450,14 +1463,14 @@
1.207
1.208  lemma neg_mod_conj : "b < (0::int) ==> a mod b \<le> 0 & b < a mod b"
1.209  apply (cut_tac a = a and b = b in divmod_int_correct)
1.210 -apply (auto simp add: divmod_int_rel_def div_int_def mod_int_def)
1.211 +apply (auto simp add: divmod_int_rel_def prod_eq_iff)
1.212  done
1.213
1.214  lemmas neg_mod_sign [simp] = neg_mod_conj [THEN conjunct1]
1.215     and neg_mod_bound [simp] = neg_mod_conj [THEN conjunct2]
1.216
1.217
1.218 -subsubsection{*General Properties of div and mod*}
1.219 +subsubsection {* General Properties of div and mod *}
1.220
1.221  lemma divmod_int_rel_div_mod: "b \<noteq> 0 ==> divmod_int_rel a b (a div b, a mod b)"
1.222  apply (cut_tac a = a and b = b in zmod_zdiv_equality)
1.223 @@ -1521,7 +1534,7 @@
1.224  done
1.225
1.226
1.227 -subsubsection{*Laws for div and mod with Unary Minus*}
1.228 +subsubsection {* Laws for div and mod with Unary Minus *}
1.229
1.230  lemma zminus1_lemma:
1.231       "divmod_int_rel a b (q, r)
1.232 @@ -1569,7 +1582,7 @@
1.233    unfolding zmod_zminus2_eq_if by auto
1.234
1.235
1.236 -subsubsection{*Division of a Number by Itself*}
1.237 +subsubsection {* Division of a Number by Itself *}
1.238
1.239  lemma self_quotient_aux1: "[| (0::int) < a; a = r + a*q; r < a |] ==> 1 \<le> q"
1.240  apply (subgoal_tac "0 < a*q")
1.241 @@ -1605,7 +1618,7 @@
1.242  done
1.243
1.244
1.245 -subsubsection{*Computation of Division and Remainder*}
1.246 +subsubsection {* Computation of Division and Remainder *}
1.247
1.248  lemma zdiv_zero [simp]: "(0::int) div b = 0"
1.249  by (simp add: div_int_def divmod_int_def)
1.250 @@ -1748,7 +1761,7 @@
1.251  lemmas negDivAlg_eqn_1_number_of [simp] = negDivAlg_eqn [of concl: 1 "number_of w"] for w
1.252
1.253
1.254 -subsubsection{*Monotonicity in the First Argument (Dividend)*}
1.255 +subsubsection {* Monotonicity in the First Argument (Dividend) *}
1.256
1.257  lemma zdiv_mono1: "[| a \<le> a';  0 < (b::int) |] ==> a div b \<le> a' div b"
1.258  apply (cut_tac a = a and b = b in zmod_zdiv_equality)
1.259 @@ -1767,7 +1780,7 @@
1.260  done
1.261
1.262
1.263 -subsubsection{*Monotonicity in the Second Argument (Divisor)*}
1.264 +subsubsection {* Monotonicity in the Second Argument (Divisor) *}
1.265
1.266  lemma q_pos_lemma:
1.267       "[| 0 \<le> b'*q' + r'; r' < b';  0 < b' |] ==> 0 \<le> (q'::int)"
1.268 @@ -1829,7 +1842,7 @@
1.269  done
1.270
1.271
1.272 -subsubsection{*More Algebraic Laws for div and mod*}
1.273 +subsubsection {* More Algebraic Laws for div and mod *}
1.274
1.275  text{*proving (a*b) div c = a * (b div c) + a * (b mod c) *}
1.276
1.277 @@ -1929,7 +1942,7 @@
1.278  lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1]
1.279
1.280
1.281 -subsubsection{*Proving  @{term "a div (b*c) = (a div b) div c"} *}
1.282 +subsubsection {* Proving  @{term "a div (b*c) = (a div b) div c"} *}
1.283
1.284  (*The condition c>0 seems necessary.  Consider that 7 div ~6 = ~2 but
1.285    7 div 2 div ~3 = 3 div ~3 = ~1.  The subcase (a div b) mod c = 0 seems
1.286 @@ -1990,7 +2003,7 @@
1.287  done
1.288
1.289
1.290 -subsubsection {*Splitting Rules for div and mod*}
1.291 +subsubsection {* Splitting Rules for div and mod *}
1.292
1.293  text{*The proofs of the two lemmas below are essentially identical*}
1.294
1.295 @@ -2051,7 +2064,7 @@
1.296  declare split_zmod [of _ _ "number_of k", arith_split] for k
1.297
1.298
1.299 -subsubsection{*Speeding up the Division Algorithm with Shifting*}
1.300 +subsubsection {* Speeding up the Division Algorithm with Shifting *}
1.301
1.302  text{*computing div by shifting *}
1.303
1.304 @@ -2105,7 +2118,7 @@
1.305  done
1.306
1.307
1.308 -subsubsection{*Computing mod by Shifting (proofs resemble those for div)*}
1.309 +subsubsection {* Computing mod by Shifting (proofs resemble those for div) *}
1.310
1.311  lemma pos_zmod_mult_2:
1.312    fixes a b :: int
1.313 @@ -2169,7 +2182,7 @@
1.314  qed
1.315
1.316
1.317 -subsubsection{*Quotients of Signs*}
1.318 +subsubsection {* Quotients of Signs *}
1.319
1.320  lemma div_neg_pos_less0: "[| a < (0::int);  0 < b |] ==> a div b < 0"
1.321  apply (subgoal_tac "a div b \<le> -1", force)
1.322 @@ -2225,7 +2238,6 @@
1.323  using int_one_le_iff_zero_less[of "a div b"] zdiv_mono1[of b a b]apply simp
1.324  done
1.325
1.326 -
1.327  lemma zmod_le_nonneg_dividend: "(m::int) \<ge> 0 ==> m mod k \<le> m"
1.328  apply (rule split_zmod[THEN iffD2])
1.329  apply(fastforce dest: q_pos_lemma intro: split_mult_pos_le)
1.330 @@ -2384,7 +2396,7 @@
1.331  proof-
1.332    from xy have th: "int x - int y = int (x - y)" by simp
1.333    from xyn have "int x mod int n = int y mod int n"
1.334 -    by (simp add: zmod_int[symmetric])
1.335 +    by (simp add: zmod_int [symmetric])
1.336    hence "int n dvd int x - int y" by (simp only: zmod_eq_dvd_iff[symmetric])
1.337    hence "n dvd x - y" by (simp add: th zdvd_int)
1.338    then show ?thesis using xy unfolding dvd_def apply clarsimp apply (rule_tac x="k" in exI) by arith
```