simplify projections on simultaneous computations of div and mod; tuned structure (from Florian Haftmann)
authorhuffman
Mon Feb 20 14:23:46 2012 +0100 (2012-02-20)
changeset 46551866bce5442a3
parent 46547 d1dcb91a512e
child 46552 5d33a3269029
simplify projections on simultaneous computations of div and mod; tuned structure (from Florian Haftmann)
src/HOL/Divides.thy
     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.92 -    (simp add: divmod_nat_div_mod)
    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