author haftmann Thu Oct 29 22:13:09 2009 +0100 (2009-10-29) changeset 33340 a165b97f3658 parent 33322 6ff4674499ca child 33341 5a989586d102
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
 src/HOL/Code_Numeral.thy file | annotate | diff | revisions src/HOL/Divides.thy file | annotate | diff | revisions src/HOL/IntDiv.thy file | annotate | diff | revisions src/HOL/Nat_Transfer.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Code_Numeral.thy	Thu Oct 29 13:37:55 2009 +0100
1.2 +++ b/src/HOL/Code_Numeral.thy	Thu Oct 29 22:13:09 2009 +0100
1.3 @@ -172,7 +172,7 @@
1.4    "n < m \<longleftrightarrow> nat_of n < nat_of m"
1.5
1.6  instance proof
1.7 -qed (auto simp add: code_numeral left_distrib div_mult_self1)
1.8 +qed (auto simp add: code_numeral left_distrib intro: mult_commute)
1.9
1.10  end
1.11
1.12 @@ -268,7 +268,15 @@
1.13  lemma int_of_code [code]:
1.14    "int_of k = (if k = 0 then 0
1.15      else (if k mod 2 = 0 then 2 * int_of (k div 2) else 2 * int_of (k div 2) + 1))"
1.16 -  by (auto simp add: int_of_def mod_div_equality')
1.17 +proof -
1.18 +  have "(nat_of k div 2) * 2 + nat_of k mod 2 = nat_of k"
1.19 +    by (rule mod_div_equality)
1.20 +  then have "int ((nat_of k div 2) * 2 + nat_of k mod 2) = int (nat_of k)"
1.21 +    by simp
1.22 +  then have "int (nat_of k) = int (nat_of k div 2) * 2 + int (nat_of k mod 2)"
1.23 +    unfolding int_mult zadd_int [symmetric] by simp
1.24 +  then show ?thesis by (auto simp add: int_of_def mult_ac)
1.25 +qed
1.26
1.27  hide (open) const of_nat nat_of int_of
1.28
```
```     2.1 --- a/src/HOL/Divides.thy	Thu Oct 29 13:37:55 2009 +0100
2.2 +++ b/src/HOL/Divides.thy	Thu Oct 29 22:13:09 2009 +0100
2.3 @@ -7,15 +7,7 @@
2.4
2.5  theory Divides
2.6  imports Nat_Numeral Nat_Transfer
2.7 -uses
2.8 -  "~~/src/Provers/Arith/assoc_fold.ML"
2.9 -  "~~/src/Provers/Arith/cancel_numerals.ML"
2.10 -  "~~/src/Provers/Arith/combine_numerals.ML"
2.11 -  "~~/src/Provers/Arith/cancel_numeral_factor.ML"
2.12 -  "~~/src/Provers/Arith/extract_common_term.ML"
2.13 -  ("Tools/numeral_simprocs.ML")
2.14 -  ("Tools/nat_numeral_simprocs.ML")
2.15 -  "~~/src/Provers/Arith/cancel_div_mod.ML"
2.16 +uses "~~/src/Provers/Arith/cancel_div_mod.ML"
2.17  begin
2.18
2.19  subsection {* Syntactic division operations *}
2.20 @@ -435,18 +427,18 @@
2.21    @{term "q\<Colon>nat"}(uotient) and @{term "r\<Colon>nat"}(emainder).
2.22  *}
2.23
2.24 -definition divmod_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat \<Rightarrow> bool" where
2.25 -  "divmod_rel m n qr \<longleftrightarrow>
2.26 +definition divmod_nat_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat \<Rightarrow> bool" where
2.27 +  "divmod_nat_rel m n qr \<longleftrightarrow>
2.28      m = fst qr * n + snd qr \<and>
2.29        (if n = 0 then fst qr = 0 else if n > 0 then 0 \<le> snd qr \<and> snd qr < n else n < snd qr \<and> snd qr \<le> 0)"
2.30
2.31 -text {* @{const divmod_rel} is total: *}
2.32 +text {* @{const divmod_nat_rel} is total: *}
2.33
2.34 -lemma divmod_rel_ex:
2.35 -  obtains q r where "divmod_rel m n (q, r)"
2.36 +lemma divmod_nat_rel_ex:
2.37 +  obtains q r where "divmod_nat_rel m n (q, r)"
2.38  proof (cases "n = 0")
2.39    case True  with that show thesis
2.40 -    by (auto simp add: divmod_rel_def)
2.41 +    by (auto simp add: divmod_nat_rel_def)
2.42  next
2.43    case False
2.44    have "\<exists>q r. m = q * n + r \<and> r < n"
2.45 @@ -470,19 +462,19 @@
2.46      qed
2.47    qed
2.48    with that show thesis
2.49 -    using `n \<noteq> 0` by (auto simp add: divmod_rel_def)
2.50 +    using `n \<noteq> 0` by (auto simp add: divmod_nat_rel_def)
2.51  qed
2.52
2.53 -text {* @{const divmod_rel} is injective: *}
2.54 +text {* @{const divmod_nat_rel} is injective: *}
2.55
2.56 -lemma divmod_rel_unique:
2.57 -  assumes "divmod_rel m n qr"
2.58 -    and "divmod_rel m n qr'"
2.59 +lemma divmod_nat_rel_unique:
2.60 +  assumes "divmod_nat_rel m n qr"
2.61 +    and "divmod_nat_rel m n qr'"
2.62    shows "qr = qr'"
2.63  proof (cases "n = 0")
2.64    case True with assms show ?thesis
2.65      by (cases qr, cases qr')
2.66 -      (simp add: divmod_rel_def)
2.67 +      (simp add: divmod_nat_rel_def)
2.68  next
2.69    case False
2.70    have aux: "\<And>q r q' r'. q' * n + r' = q * n + r \<Longrightarrow> r < n \<Longrightarrow> q' \<le> (q\<Colon>nat)"
2.71 @@ -491,91 +483,91 @@
2.72    apply (auto simp add: add_mult_distrib)
2.73    done
2.74    from `n \<noteq> 0` assms have "fst qr = fst qr'"
2.75 -    by (auto simp add: divmod_rel_def intro: order_antisym dest: aux sym)
2.76 +    by (auto simp add: divmod_nat_rel_def intro: order_antisym dest: aux sym)
2.77    moreover from this assms have "snd qr = snd qr'"
2.78 -    by (simp add: divmod_rel_def)
2.79 +    by (simp add: divmod_nat_rel_def)
2.80    ultimately show ?thesis by (cases qr, cases qr') simp
2.81  qed
2.82
2.83  text {*
2.84    We instantiate divisibility on the natural numbers by
2.85 -  means of @{const divmod_rel}:
2.86 +  means of @{const divmod_nat_rel}:
2.87  *}
2.88
2.89  instantiation nat :: semiring_div
2.90  begin
2.91
2.92 -definition divmod :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
2.93 -  [code del]: "divmod m n = (THE qr. divmod_rel m n qr)"
2.94 +definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
2.95 +  [code del]: "divmod_nat m n = (THE qr. divmod_nat_rel m n qr)"
2.96
2.97 -lemma divmod_rel_divmod:
2.98 -  "divmod_rel m n (divmod m n)"
2.99 +lemma divmod_nat_rel_divmod_nat:
2.100 +  "divmod_nat_rel m n (divmod_nat m n)"
2.101  proof -
2.102 -  from divmod_rel_ex
2.103 -    obtain qr where rel: "divmod_rel m n qr" .
2.104 +  from divmod_nat_rel_ex
2.105 +    obtain qr where rel: "divmod_nat_rel m n qr" .
2.106    then show ?thesis
2.107 -  by (auto simp add: divmod_def intro: theI elim: divmod_rel_unique)
2.108 +  by (auto simp add: divmod_nat_def intro: theI elim: divmod_nat_rel_unique)
2.109  qed
2.110
2.111 -lemma divmod_eq:
2.112 -  assumes "divmod_rel m n qr"
2.113 -  shows "divmod m n = qr"
2.114 -  using assms by (auto intro: divmod_rel_unique divmod_rel_divmod)
2.115 +lemma divmod_nat_eq:
2.116 +  assumes "divmod_nat_rel m n qr"
2.117 +  shows "divmod_nat m n = qr"
2.118 +  using assms by (auto intro: divmod_nat_rel_unique divmod_nat_rel_divmod_nat)
2.119
2.120  definition div_nat where
2.121 -  "m div n = fst (divmod m n)"
2.122 +  "m div n = fst (divmod_nat m n)"
2.123
2.124  definition mod_nat where
2.125 -  "m mod n = snd (divmod m n)"
2.126 +  "m mod n = snd (divmod_nat m n)"
2.127
2.128 -lemma divmod_div_mod:
2.129 -  "divmod m n = (m div n, m mod n)"
2.130 +lemma divmod_nat_div_mod:
2.131 +  "divmod_nat m n = (m div n, m mod n)"
2.132    unfolding div_nat_def mod_nat_def by simp
2.133
2.134  lemma div_eq:
2.135 -  assumes "divmod_rel m n (q, r)"
2.136 +  assumes "divmod_nat_rel m n (q, r)"
2.137    shows "m div n = q"
2.138 -  using assms by (auto dest: divmod_eq simp add: divmod_div_mod)
2.139 +  using assms by (auto dest: divmod_nat_eq simp add: divmod_nat_div_mod)
2.140
2.141  lemma mod_eq:
2.142 -  assumes "divmod_rel m n (q, r)"
2.143 +  assumes "divmod_nat_rel m n (q, r)"
2.144    shows "m mod n = r"
2.145 -  using assms by (auto dest: divmod_eq simp add: divmod_div_mod)
2.146 +  using assms by (auto dest: divmod_nat_eq simp add: divmod_nat_div_mod)
2.147
2.148 -lemma divmod_rel: "divmod_rel m n (m div n, m mod n)"
2.149 -  by (simp add: div_nat_def mod_nat_def divmod_rel_divmod)
2.150 +lemma divmod_nat_rel: "divmod_nat_rel m n (m div n, m mod n)"
2.151 +  by (simp add: div_nat_def mod_nat_def divmod_nat_rel_divmod_nat)
2.152
2.153 -lemma divmod_zero:
2.154 -  "divmod m 0 = (0, m)"
2.155 +lemma divmod_nat_zero:
2.156 +  "divmod_nat m 0 = (0, m)"
2.157  proof -
2.158 -  from divmod_rel [of m 0] show ?thesis
2.159 -    unfolding divmod_div_mod divmod_rel_def by simp
2.160 +  from divmod_nat_rel [of m 0] show ?thesis
2.161 +    unfolding divmod_nat_div_mod divmod_nat_rel_def by simp
2.162  qed
2.163
2.164 -lemma divmod_base:
2.165 +lemma divmod_nat_base:
2.166    assumes "m < n"
2.167 -  shows "divmod m n = (0, m)"
2.168 +  shows "divmod_nat m n = (0, m)"
2.169  proof -
2.170 -  from divmod_rel [of m n] show ?thesis
2.171 -    unfolding divmod_div_mod divmod_rel_def
2.172 +  from divmod_nat_rel [of m n] show ?thesis
2.173 +    unfolding divmod_nat_div_mod divmod_nat_rel_def
2.174      using assms by (cases "m div n = 0")
2.175        (auto simp add: gr0_conv_Suc [of "m div n"])
2.176  qed
2.177
2.178 -lemma divmod_step:
2.179 +lemma divmod_nat_step:
2.180    assumes "0 < n" and "n \<le> m"
2.181 -  shows "divmod m n = (Suc ((m - n) div n), (m - n) mod n)"
2.182 +  shows "divmod_nat m n = (Suc ((m - n) div n), (m - n) mod n)"
2.183  proof -
2.184 -  from divmod_rel have divmod_m_n: "divmod_rel m n (m div n, m mod n)" .
2.185 +  from divmod_nat_rel have divmod_nat_m_n: "divmod_nat_rel m n (m div n, m mod n)" .
2.186    with assms have m_div_n: "m div n \<ge> 1"
2.187 -    by (cases "m div n") (auto simp add: divmod_rel_def)
2.188 -  from assms divmod_m_n have "divmod_rel (m - n) n (m div n - Suc 0, m mod n)"
2.189 -    by (cases "m div n") (auto simp add: divmod_rel_def)
2.190 -  with divmod_eq have "divmod (m - n) n = (m div n - Suc 0, m mod n)" by simp
2.191 -  moreover from divmod_div_mod have "divmod (m - n) n = ((m - n) div n, (m - n) mod n)" .
2.192 +    by (cases "m div n") (auto simp add: divmod_nat_rel_def)
2.193 +  from assms divmod_nat_m_n have "divmod_nat_rel (m - n) n (m div n - Suc 0, m mod n)"
2.194 +    by (cases "m div n") (auto simp add: divmod_nat_rel_def)
2.195 +  with divmod_nat_eq have "divmod_nat (m - n) n = (m div n - Suc 0, m mod n)" by simp
2.196 +  moreover from divmod_nat_div_mod have "divmod_nat (m - n) n = ((m - n) div n, (m - n) mod n)" .
2.197    ultimately have "m div n = Suc ((m - n) div n)"
2.198      and "m mod n = (m - n) mod n" using m_div_n by simp_all
2.199 -  then show ?thesis using divmod_div_mod by simp
2.200 +  then show ?thesis using divmod_nat_div_mod by simp
2.201  qed
2.202
2.203  text {* The ''recursion'' equations for @{const div} and @{const mod} *}
2.204 @@ -584,29 +576,29 @@
2.205    fixes m n :: nat
2.206    assumes "m < n"
2.207    shows "m div n = 0"
2.208 -  using assms divmod_base divmod_div_mod by simp
2.209 +  using assms divmod_nat_base divmod_nat_div_mod by simp
2.210
2.211  lemma le_div_geq:
2.212    fixes m n :: nat
2.213    assumes "0 < n" and "n \<le> m"
2.214    shows "m div n = Suc ((m - n) div n)"
2.215 -  using assms divmod_step divmod_div_mod by simp
2.216 +  using assms divmod_nat_step divmod_nat_div_mod by simp
2.217
2.218  lemma mod_less [simp]:
2.219    fixes m n :: nat
2.220    assumes "m < n"
2.221    shows "m mod n = m"
2.222 -  using assms divmod_base divmod_div_mod by simp
2.223 +  using assms divmod_nat_base divmod_nat_div_mod by simp
2.224
2.225  lemma le_mod_geq:
2.226    fixes m n :: nat
2.227    assumes "n \<le> m"
2.228    shows "m mod n = (m - n) mod n"
2.229 -  using assms divmod_step divmod_div_mod by (cases "n = 0") simp_all
2.230 +  using assms divmod_nat_step divmod_nat_div_mod by (cases "n = 0") simp_all
2.231
2.232  instance proof -
2.233    have [simp]: "\<And>n::nat. n div 0 = 0"
2.234 -    by (simp add: div_nat_def divmod_zero)
2.235 +    by (simp add: div_nat_def divmod_nat_zero)
2.236    have [simp]: "\<And>n::nat. 0 div n = 0"
2.237    proof -
2.238      fix n :: nat
2.239 @@ -616,7 +608,7 @@
2.240    show "OFCLASS(nat, semiring_div_class)" proof
2.241      fix m n :: nat
2.242      show "m div n * n + m mod n = m"
2.243 -      using divmod_rel [of m n] by (simp add: divmod_rel_def)
2.244 +      using divmod_nat_rel [of m n] by (simp add: divmod_nat_rel_def)
2.245    next
2.246      fix m n q :: nat
2.247      assume "n \<noteq> 0"
2.248 @@ -631,10 +623,10 @@
2.249      next
2.250        case True with `m \<noteq> 0`
2.251          have "m > 0" and "n > 0" and "q > 0" by auto
2.252 -      then have "\<And>a b. divmod_rel n q (a, b) \<Longrightarrow> divmod_rel (m * n) (m * q) (a, m * b)"
2.253 -        by (auto simp add: divmod_rel_def) (simp_all add: algebra_simps)
2.254 -      moreover from divmod_rel have "divmod_rel n q (n div q, n mod q)" .
2.255 -      ultimately have "divmod_rel (m * n) (m * q) (n div q, m * (n mod q))" .
2.256 +      then have "\<And>a b. divmod_nat_rel n q (a, b) \<Longrightarrow> divmod_nat_rel (m * n) (m * q) (a, m * b)"
2.257 +        by (auto simp add: divmod_nat_rel_def) (simp_all add: algebra_simps)
2.258 +      moreover from divmod_nat_rel have "divmod_nat_rel n q (n div q, n mod q)" .
2.259 +      ultimately have "divmod_nat_rel (m * n) (m * q) (n div q, m * (n mod q))" .
2.260        then show ?thesis by (simp add: div_eq)
2.261      qed
2.262    qed simp_all
2.263 @@ -676,10 +668,10 @@
2.264
2.265  text {* code generator setup *}
2.266
2.267 -lemma divmod_if [code]: "divmod m n = (if n = 0 \<or> m < n then (0, m) else
2.268 -  let (q, r) = divmod (m - n) n in (Suc q, r))"
2.269 -by (simp add: divmod_zero divmod_base divmod_step)
2.270 -    (simp add: divmod_div_mod)
2.271 +lemma divmod_nat_if [code]: "divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
2.272 +  let (q, r) = divmod_nat (m - n) n in (Suc q, r))"
2.273 +by (simp add: divmod_nat_zero divmod_nat_base divmod_nat_step)
2.274 +    (simp add: divmod_nat_div_mod)
2.275
2.276  code_modulename SML
2.277    Divides Nat
2.278 @@ -712,7 +704,7 @@
2.279    fixes m n :: nat
2.280    assumes "n > 0"
2.281    shows "m mod n < (n::nat)"
2.282 -  using assms divmod_rel [of m n] unfolding divmod_rel_def by auto
2.283 +  using assms divmod_nat_rel [of m n] unfolding divmod_nat_rel_def by auto
2.284
2.285  lemma mod_less_eq_dividend [simp]:
2.286    fixes m n :: nat
2.287 @@ -753,27 +745,27 @@
2.288
2.289  subsubsection {* Quotient and Remainder *}
2.290
2.291 -lemma divmod_rel_mult1_eq:
2.292 -  "divmod_rel b c (q, r) \<Longrightarrow> c > 0
2.293 -   \<Longrightarrow> divmod_rel (a * b) c (a * q + a * r div c, a * r mod c)"
2.294 -by (auto simp add: split_ifs divmod_rel_def algebra_simps)
2.295 +lemma divmod_nat_rel_mult1_eq:
2.296 +  "divmod_nat_rel b c (q, r) \<Longrightarrow> c > 0
2.297 +   \<Longrightarrow> divmod_nat_rel (a * b) c (a * q + a * r div c, a * r mod c)"
2.298 +by (auto simp add: split_ifs divmod_nat_rel_def algebra_simps)
2.299
2.300  lemma div_mult1_eq:
2.301    "(a * b) div c = a * (b div c) + a * (b mod c) div (c::nat)"
2.302  apply (cases "c = 0", simp)
2.303 -apply (blast intro: divmod_rel [THEN divmod_rel_mult1_eq, THEN div_eq])
2.304 +apply (blast intro: divmod_nat_rel [THEN divmod_nat_rel_mult1_eq, THEN div_eq])
2.305  done
2.306
2.307 -lemma divmod_rel_add1_eq:
2.308 -  "divmod_rel a c (aq, ar) \<Longrightarrow> divmod_rel b c (bq, br) \<Longrightarrow>  c > 0
2.309 -   \<Longrightarrow> divmod_rel (a + b) c (aq + bq + (ar + br) div c, (ar + br) mod c)"
2.310 -by (auto simp add: split_ifs divmod_rel_def algebra_simps)
2.311 +lemma divmod_nat_rel_add1_eq:
2.312 +  "divmod_nat_rel a c (aq, ar) \<Longrightarrow> divmod_nat_rel b c (bq, br) \<Longrightarrow>  c > 0
2.313 +   \<Longrightarrow> divmod_nat_rel (a + b) c (aq + bq + (ar + br) div c, (ar + br) mod c)"
2.314 +by (auto simp add: split_ifs divmod_nat_rel_def algebra_simps)
2.315
2.316  (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
2.317  lemma div_add1_eq:
2.318    "(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"
2.319  apply (cases "c = 0", simp)
2.320 -apply (blast intro: divmod_rel_add1_eq [THEN div_eq] divmod_rel)
2.321 +apply (blast intro: divmod_nat_rel_add1_eq [THEN div_eq] divmod_nat_rel)
2.322  done
2.323
2.324  lemma mod_lemma: "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c"
2.325 @@ -783,21 +775,21 @@
2.326    apply (simp add: add_mult_distrib2)
2.327    done
2.328
2.329 -lemma divmod_rel_mult2_eq:
2.330 -  "divmod_rel a b (q, r) \<Longrightarrow> 0 < b \<Longrightarrow> 0 < c
2.331 -   \<Longrightarrow> divmod_rel a (b * c) (q div c, b *(q mod c) + r)"
2.332 -by (auto simp add: mult_ac divmod_rel_def add_mult_distrib2 [symmetric] mod_lemma)
2.333 +lemma divmod_nat_rel_mult2_eq:
2.334 +  "divmod_nat_rel a b (q, r) \<Longrightarrow> 0 < b \<Longrightarrow> 0 < c
2.335 +   \<Longrightarrow> divmod_nat_rel a (b * c) (q div c, b *(q mod c) + r)"
2.336 +by (auto simp add: mult_ac divmod_nat_rel_def add_mult_distrib2 [symmetric] mod_lemma)
2.337
2.338  lemma div_mult2_eq: "a div (b*c) = (a div b) div (c::nat)"
2.339    apply (cases "b = 0", simp)
2.340    apply (cases "c = 0", simp)
2.341 -  apply (force simp add: divmod_rel [THEN divmod_rel_mult2_eq, THEN div_eq])
2.342 +  apply (force simp add: divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN div_eq])
2.343    done
2.344
2.345  lemma mod_mult2_eq: "a mod (b*c) = b*(a div b mod c) + a mod (b::nat)"
2.346    apply (cases "b = 0", simp)
2.347    apply (cases "c = 0", simp)
2.348 -  apply (auto simp add: mult_commute divmod_rel [THEN divmod_rel_mult2_eq, THEN mod_eq])
2.349 +  apply (auto simp add: mult_commute divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN mod_eq])
2.350    done
2.351
2.352
2.353 @@ -944,9 +936,9 @@
2.354    from A B show ?lhs ..
2.355  next
2.356    assume P: ?lhs
2.357 -  then have "divmod_rel m n (q, m - n * q)"
2.358 -    unfolding divmod_rel_def by (auto simp add: mult_ac)
2.359 -  with divmod_rel_unique divmod_rel [of m n]
2.360 +  then have "divmod_nat_rel m n (q, m - n * q)"
2.361 +    unfolding divmod_nat_rel_def by (auto simp add: mult_ac)
2.362 +  with divmod_nat_rel_unique divmod_nat_rel [of m n]
2.363    have "(q, m - n * q) = (m div n, m mod n)" by auto
2.364    then show ?rhs by simp
2.365  qed
2.366 @@ -1144,114 +1136,4 @@
2.367      Suc_mod_eq_add3_mod [of _ "number_of v", standard]
2.368  declare Suc_mod_eq_add3_mod_number_of [simp]
2.369
2.370 -
2.371 -subsection {* Proof Tools setup; Combination and Cancellation Simprocs *}
2.372 -
2.373 -declare split_div[of _ _ "number_of k", standard, arith_split]
2.374 -declare split_mod[of _ _ "number_of k", standard, arith_split]
2.375 -
2.376 -
2.377 -subsubsection{*For @{text combine_numerals}*}
2.378 -
2.379 -lemma left_add_mult_distrib: "i*u + (j*u + k) = (i+j)*u + (k::nat)"
2.380 -by (simp add: add_mult_distrib)
2.381 -
2.382 -
2.383 -subsubsection{*For @{text cancel_numerals}*}
2.384 -
2.385 -lemma nat_diff_add_eq1:
2.386 -     "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)"
2.387 -by (simp split add: nat_diff_split add: add_mult_distrib)
2.388 -
2.389 -lemma nat_diff_add_eq2:
2.390 -     "i <= (j::nat) ==> ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))"
2.391 -by (simp split add: nat_diff_split add: add_mult_distrib)
2.392 -
2.393 -lemma nat_eq_add_iff1:
2.394 -     "j <= (i::nat) ==> (i*u + m = j*u + n) = ((i-j)*u + m = n)"
2.395 -by (auto split add: nat_diff_split simp add: add_mult_distrib)
2.396 -
2.397 -lemma nat_eq_add_iff2:
2.398 -     "i <= (j::nat) ==> (i*u + m = j*u + n) = (m = (j-i)*u + n)"
2.399 -by (auto split add: nat_diff_split simp add: add_mult_distrib)
2.400 -
2.401 -lemma nat_less_add_iff1:
2.402 -     "j <= (i::nat) ==> (i*u + m < j*u + n) = ((i-j)*u + m < n)"
2.403 -by (auto split add: nat_diff_split simp add: add_mult_distrib)
2.404 -
2.405 -lemma nat_less_add_iff2:
2.406 -     "i <= (j::nat) ==> (i*u + m < j*u + n) = (m < (j-i)*u + n)"
2.407 -by (auto split add: nat_diff_split simp add: add_mult_distrib)
2.408 -
2.409 -lemma nat_le_add_iff1:
2.410 -     "j <= (i::nat) ==> (i*u + m <= j*u + n) = ((i-j)*u + m <= n)"
2.411 -by (auto split add: nat_diff_split simp add: add_mult_distrib)
2.412 -
2.413 -lemma nat_le_add_iff2:
2.414 -     "i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)"
2.415 -by (auto split add: nat_diff_split simp add: add_mult_distrib)
2.416 -
2.417 -
2.418 -subsubsection{*For @{text cancel_numeral_factors} *}
2.419 -
2.420 -lemma nat_mult_le_cancel1: "(0::nat) < k ==> (k*m <= k*n) = (m<=n)"
2.421 -by auto
2.422 -
2.423 -lemma nat_mult_less_cancel1: "(0::nat) < k ==> (k*m < k*n) = (m<n)"
2.424 -by auto
2.425 -
2.426 -lemma nat_mult_eq_cancel1: "(0::nat) < k ==> (k*m = k*n) = (m=n)"
2.427 -by auto
2.428 -
2.429 -lemma nat_mult_div_cancel1: "(0::nat) < k ==> (k*m) div (k*n) = (m div n)"
2.430 -by auto
2.431 -
2.432 -lemma nat_mult_dvd_cancel_disj[simp]:
2.433 -  "(k*m) dvd (k*n) = (k=0 | m dvd (n::nat))"
2.434 -by(auto simp: dvd_eq_mod_eq_0 mod_mult_distrib2[symmetric])
2.435 -
2.436 -lemma nat_mult_dvd_cancel1: "0 < k \<Longrightarrow> (k*m) dvd (k*n::nat) = (m dvd n)"
2.437 -by(auto)
2.438 -
2.439 -
2.440 -subsubsection{*For @{text cancel_factor} *}
2.441 -
2.442 -lemma nat_mult_le_cancel_disj: "(k*m <= k*n) = ((0::nat) < k --> m<=n)"
2.443 -by auto
2.444 -
2.445 -lemma nat_mult_less_cancel_disj: "(k*m < k*n) = ((0::nat) < k & m<n)"
2.446 -by auto
2.447 -
2.448 -lemma nat_mult_eq_cancel_disj: "(k*m = k*n) = (k = (0::nat) | m=n)"
2.449 -by auto
2.450 -
2.451 -lemma nat_mult_div_cancel_disj[simp]:
2.452 -     "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)"
2.453 -by (simp add: nat_mult_div_cancel1)
2.454 -
2.455 -
2.456 -use "Tools/numeral_simprocs.ML"
2.457 -
2.458 -use "Tools/nat_numeral_simprocs.ML"
2.459 -
2.460 -declaration {*
2.461 -  K (Lin_Arith.add_simps (@{thms neg_simps} @ [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}])
2.462 -  #> Lin_Arith.add_simps (@{thms ring_distribs} @ [@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1},
2.463 -     @{thm nat_0}, @{thm nat_1},
2.464 -     @{thm add_nat_number_of}, @{thm diff_nat_number_of}, @{thm mult_nat_number_of},
2.465 -     @{thm eq_nat_number_of}, @{thm less_nat_number_of}, @{thm le_number_of_eq_not_less},
2.466 -     @{thm le_Suc_number_of}, @{thm le_number_of_Suc},
2.467 -     @{thm less_Suc_number_of}, @{thm less_number_of_Suc},
2.468 -     @{thm Suc_eq_number_of}, @{thm eq_number_of_Suc},
2.469 -     @{thm mult_Suc}, @{thm mult_Suc_right},
2.470 -     @{thm add_Suc}, @{thm add_Suc_right},
2.471 -     @{thm eq_number_of_0}, @{thm eq_0_number_of}, @{thm less_0_number_of},
2.472 -     @{thm of_int_number_of_eq}, @{thm of_nat_number_of_eq}, @{thm nat_number_of},
2.473 -     @{thm if_True}, @{thm if_False}])
2.474 -  #> Lin_Arith.add_simprocs (Numeral_Simprocs.assoc_fold_simproc
2.475 -      :: Numeral_Simprocs.combine_numerals
2.476 -      :: Numeral_Simprocs.cancel_numerals)
2.477 -  #> Lin_Arith.add_simprocs (Nat_Numeral_Simprocs.combine_numerals :: Nat_Numeral_Simprocs.cancel_numerals))
2.478 -*}
2.479 -
2.480  end
```
```     3.1 --- a/src/HOL/IntDiv.thy	Thu Oct 29 13:37:55 2009 +0100
3.2 +++ b/src/HOL/IntDiv.thy	Thu Oct 29 22:13:09 2009 +0100
3.3 @@ -7,11 +7,19 @@
3.4
3.5  theory IntDiv
3.6  imports Int Divides FunDef
3.7 +uses
3.8 +  "~~/src/Provers/Arith/assoc_fold.ML"
3.9 +  "~~/src/Provers/Arith/cancel_numerals.ML"
3.10 +  "~~/src/Provers/Arith/combine_numerals.ML"
3.11 +  "~~/src/Provers/Arith/cancel_numeral_factor.ML"
3.12 +  "~~/src/Provers/Arith/extract_common_term.ML"
3.13 +  ("Tools/numeral_simprocs.ML")
3.14 +  ("Tools/nat_numeral_simprocs.ML")
3.15  begin
3.16
3.17 -definition divmod_rel :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool" where
3.18 +definition divmod_int_rel :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool" where
3.19      --{*definition of quotient and remainder*}
3.20 -    [code]: "divmod_rel a b = (\<lambda>(q, r). a = b * q + r \<and>
3.21 +    [code]: "divmod_int_rel a b = (\<lambda>(q, r). a = b * q + r \<and>
3.22                 (if 0 < b then 0 \<le> r \<and> r < b else b < r \<and> r \<le> 0))"
3.23
3.24  definition adjust :: "int \<Rightarrow> int \<times> int \<Rightarrow> int \<times> int" where
3.25 @@ -24,24 +32,26 @@
3.26    "posDivAlg a b = (if a < b \<or>  b \<le> 0 then (0, a)
3.27       else adjust b (posDivAlg a (2 * b)))"
3.28  by auto
3.29 -termination by (relation "measure (\<lambda>(a, b). nat (a - b + 1))") auto
3.30 +termination by (relation "measure (\<lambda>(a, b). nat (a - b + 1))")
3.31 +  (auto simp add: mult_2)
3.32
3.33  text{*algorithm for the case @{text "a<0, b>0"}*}
3.34  function negDivAlg :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
3.35    "negDivAlg a b = (if 0 \<le>a + b \<or> b \<le> 0  then (-1, a + b)
3.36       else adjust b (negDivAlg a (2 * b)))"
3.37  by auto
3.38 -termination by (relation "measure (\<lambda>(a, b). nat (- a - b))") auto
3.39 +termination by (relation "measure (\<lambda>(a, b). nat (- a - b))")
3.40 +  (auto simp add: mult_2)
3.41
3.42  text{*algorithm for the general case @{term "b\<noteq>0"}*}
3.43  definition negateSnd :: "int \<times> int \<Rightarrow> int \<times> int" where
3.44    [code_unfold]: "negateSnd = apsnd uminus"
3.45
3.46 -definition divmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
3.47 +definition divmod_int :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
3.48      --{*The full division algorithm considers all possible signs for a, b
3.49         including the special case @{text "a=0, b<0"} because
3.50         @{term negDivAlg} requires @{term "a<0"}.*}
3.51 -  "divmod a b = (if 0 \<le> a then if 0 \<le> b then posDivAlg a b
3.52 +  "divmod_int a b = (if 0 \<le> a then if 0 \<le> b then posDivAlg a b
3.53                    else if a = 0 then (0, 0)
3.54                         else negateSnd (negDivAlg (-a) (-b))
3.55                 else
3.56 @@ -52,18 +62,18 @@
3.57  begin
3.58
3.59  definition
3.60 -  div_def: "a div b = fst (divmod a b)"
3.61 +  "a div b = fst (divmod_int a b)"
3.62
3.63  definition
3.64 -  mod_def: "a mod b = snd (divmod a b)"
3.65 + "a mod b = snd (divmod_int a b)"
3.66
3.67  instance ..
3.68
3.69  end
3.70
3.71 -lemma divmod_mod_div:
3.72 -  "divmod p q = (p div q, p mod q)"
3.73 -  by (auto simp add: div_def mod_def)
3.74 +lemma divmod_int_mod_div:
3.75 +  "divmod_int p q = (p div q, p mod q)"
3.76 +  by (auto simp add: div_int_def mod_int_def)
3.77
3.78  text{*
3.79  Here is the division algorithm in ML:
3.80 @@ -117,9 +127,9 @@
3.81      auto)
3.82
3.83  lemma unique_quotient:
3.84 -     "[| divmod_rel a b (q, r); divmod_rel a b (q', r');  b \<noteq> 0 |]
3.85 +     "[| divmod_int_rel a b (q, r); divmod_int_rel a b (q', r');  b \<noteq> 0 |]
3.86        ==> q = q'"
3.87 -apply (simp add: divmod_rel_def linorder_neq_iff split: split_if_asm)
3.88 +apply (simp add: divmod_int_rel_def linorder_neq_iff split: split_if_asm)
3.89  apply (blast intro: order_antisym
3.90               dest: order_eq_refl [THEN unique_quotient_lemma]
3.91               order_eq_refl [THEN unique_quotient_lemma_neg] sym)+
3.92 @@ -127,10 +137,10 @@
3.93
3.94
3.95  lemma unique_remainder:
3.96 -     "[| divmod_rel a b (q, r); divmod_rel a b (q', r');  b \<noteq> 0 |]
3.97 +     "[| divmod_int_rel a b (q, r); divmod_int_rel a b (q', r');  b \<noteq> 0 |]
3.98        ==> r = r'"
3.99  apply (subgoal_tac "q = q'")
3.100 - apply (simp add: divmod_rel_def)
3.101 + apply (simp add: divmod_int_rel_def)
3.102  apply (blast intro: unique_quotient)
3.103  done
3.104
3.105 @@ -157,15 +167,15 @@
3.106  text{*Correctness of @{term posDivAlg}: it computes quotients correctly*}
3.107  theorem posDivAlg_correct:
3.108    assumes "0 \<le> a" and "0 < b"
3.109 -  shows "divmod_rel a b (posDivAlg a b)"
3.110 +  shows "divmod_int_rel a b (posDivAlg a b)"
3.111  using prems apply (induct a b rule: posDivAlg.induct)
3.112  apply auto
3.113 -apply (simp add: divmod_rel_def)
3.114 +apply (simp add: divmod_int_rel_def)
3.115  apply (subst posDivAlg_eqn, simp add: right_distrib)
3.116  apply (case_tac "a < b")
3.117  apply simp_all
3.118  apply (erule splitE)
3.119 -apply (auto simp add: right_distrib Let_def)
3.120 +apply (auto simp add: right_distrib Let_def mult_ac mult_2_right)
3.121  done
3.122
3.123
3.124 @@ -186,23 +196,23 @@
3.125    It doesn't work if a=0 because the 0/b equals 0, not -1*)
3.126  lemma negDivAlg_correct:
3.127    assumes "a < 0" and "b > 0"
3.128 -  shows "divmod_rel a b (negDivAlg a b)"
3.129 +  shows "divmod_int_rel a b (negDivAlg a b)"
3.130  using prems apply (induct a b rule: negDivAlg.induct)
3.131  apply (auto simp add: linorder_not_le)
3.132 -apply (simp add: divmod_rel_def)
3.133 +apply (simp add: divmod_int_rel_def)
3.134  apply (subst negDivAlg_eqn, assumption)
3.135  apply (case_tac "a + b < (0\<Colon>int)")
3.136  apply simp_all
3.137  apply (erule splitE)
3.138 -apply (auto simp add: right_distrib Let_def)
3.139 +apply (auto simp add: right_distrib Let_def mult_ac mult_2_right)
3.140  done
3.141
3.142
3.143  subsection{*Existence Shown by Proving the Division Algorithm to be Correct*}
3.144
3.145  (*the case a=0*)
3.146 -lemma divmod_rel_0: "b \<noteq> 0 ==> divmod_rel 0 b (0, 0)"
3.147 -by (auto simp add: divmod_rel_def linorder_neq_iff)
3.148 +lemma divmod_int_rel_0: "b \<noteq> 0 ==> divmod_int_rel 0 b (0, 0)"
3.149 +by (auto simp add: divmod_int_rel_def linorder_neq_iff)
3.150
3.151  lemma posDivAlg_0 [simp]: "posDivAlg 0 b = (0, 0)"
3.152  by (subst posDivAlg.simps, auto)
3.153 @@ -213,26 +223,26 @@
3.154  lemma negateSnd_eq [simp]: "negateSnd(q,r) = (q,-r)"
3.155  by (simp add: negateSnd_def)
3.156
3.157 -lemma divmod_rel_neg: "divmod_rel (-a) (-b) qr ==> divmod_rel a b (negateSnd qr)"
3.158 -by (auto simp add: split_ifs divmod_rel_def)
3.159 +lemma divmod_int_rel_neg: "divmod_int_rel (-a) (-b) qr ==> divmod_int_rel a b (negateSnd qr)"
3.160 +by (auto simp add: split_ifs divmod_int_rel_def)
3.161
3.162 -lemma divmod_correct: "b \<noteq> 0 ==> divmod_rel a b (divmod a b)"
3.163 -by (force simp add: linorder_neq_iff divmod_rel_0 divmod_def divmod_rel_neg
3.164 +lemma divmod_int_correct: "b \<noteq> 0 ==> divmod_int_rel a b (divmod_int a b)"
3.165 +by (force simp add: linorder_neq_iff divmod_int_rel_0 divmod_int_def divmod_int_rel_neg
3.166                      posDivAlg_correct negDivAlg_correct)
3.167
3.168  text{*Arbitrary definitions for division by zero.  Useful to simplify
3.169      certain equations.*}
3.170
3.171  lemma DIVISION_BY_ZERO [simp]: "a div (0::int) = 0 & a mod (0::int) = a"
3.172 -by (simp add: div_def mod_def divmod_def posDivAlg.simps)
3.173 +by (simp add: div_int_def mod_int_def divmod_int_def posDivAlg.simps)
3.174
3.175
3.176  text{*Basic laws about division and remainder*}
3.177
3.178  lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)"
3.179  apply (case_tac "b = 0", simp)
3.180 -apply (cut_tac a = a and b = b in divmod_correct)
3.181 -apply (auto simp add: divmod_rel_def div_def mod_def)
3.182 +apply (cut_tac a = a and b = b in divmod_int_correct)
3.183 +apply (auto simp add: divmod_int_rel_def div_int_def mod_int_def)
3.184  done
3.185
3.186  lemma zdiv_zmod_equality: "(b * (a div b) + (a mod b)) + k = (a::int)+k"
3.187 @@ -246,13 +256,47 @@
3.188  ML {*
3.189  local
3.190
3.191 +fun mk_number T n = HOLogic.number_of_const T \$ HOLogic.mk_numeral n;
3.192 +
3.193 +fun find_first_numeral past (t::terms) =
3.194 +        ((snd (HOLogic.dest_number t), rev past @ terms)
3.195 +         handle TERM _ => find_first_numeral (t::past) terms)
3.196 +  | find_first_numeral past [] = raise TERM("find_first_numeral", []);
3.197 +
3.198 +val mk_plus = HOLogic.mk_binop @{const_name HOL.plus};
3.199 +
3.200 +fun mk_minus t =
3.201 +  let val T = Term.fastype_of t
3.202 +  in Const (@{const_name HOL.uminus}, T --> T) \$ t end;
3.203 +
3.204 +(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
3.205 +fun mk_sum T []        = mk_number T 0
3.206 +  | mk_sum T [t,u]     = mk_plus (t, u)
3.207 +  | mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts);
3.208 +
3.209 +(*this version ALWAYS includes a trailing zero*)
3.210 +fun long_mk_sum T []        = mk_number T 0
3.211 +  | long_mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts);
3.212 +
3.213 +val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} Term.dummyT;
3.214 +
3.215 +(*decompose additions AND subtractions as a sum*)
3.216 +fun dest_summing (pos, Const (@{const_name HOL.plus}, _) \$ t \$ u, ts) =
3.217 +        dest_summing (pos, t, dest_summing (pos, u, ts))
3.218 +  | dest_summing (pos, Const (@{const_name HOL.minus}, _) \$ t \$ u, ts) =
3.219 +        dest_summing (pos, t, dest_summing (not pos, u, ts))
3.220 +  | dest_summing (pos, t, ts) =
3.221 +        if pos then t::ts else mk_minus t :: ts;
3.222 +
3.223 +fun dest_sum t = dest_summing (true, t, []);
3.224 +
3.225  structure CancelDivMod = CancelDivModFun(struct
3.226
3.227    val div_name = @{const_name div};
3.228    val mod_name = @{const_name mod};
3.229    val mk_binop = HOLogic.mk_binop;
3.230 -  val mk_sum = Numeral_Simprocs.mk_sum HOLogic.intT;
3.231 -  val dest_sum = Numeral_Simprocs.dest_sum;
3.232 +  val mk_sum = mk_sum HOLogic.intT;
3.233 +  val dest_sum = dest_sum;
3.234
3.235    val div_mod_eqs = map mk_meta_eq [@{thm zdiv_zmod_equality}, @{thm zdiv_zmod_equality2}];
3.236
3.237 @@ -274,16 +318,16 @@
3.238  *}
3.239
3.240  lemma pos_mod_conj : "(0::int) < b ==> 0 \<le> a mod b & a mod b < b"
3.241 -apply (cut_tac a = a and b = b in divmod_correct)
3.242 -apply (auto simp add: divmod_rel_def mod_def)
3.243 +apply (cut_tac a = a and b = b in divmod_int_correct)
3.244 +apply (auto simp add: divmod_int_rel_def mod_int_def)
3.245  done
3.246
3.247  lemmas pos_mod_sign  [simp] = pos_mod_conj [THEN conjunct1, standard]
3.248     and pos_mod_bound [simp] = pos_mod_conj [THEN conjunct2, standard]
3.249
3.250  lemma neg_mod_conj : "b < (0::int) ==> a mod b \<le> 0 & b < a mod b"
3.251 -apply (cut_tac a = a and b = b in divmod_correct)
3.252 -apply (auto simp add: divmod_rel_def div_def mod_def)
3.253 +apply (cut_tac a = a and b = b in divmod_int_correct)
3.254 +apply (auto simp add: divmod_int_rel_def div_int_def mod_int_def)
3.255  done
3.256
3.257  lemmas neg_mod_sign  [simp] = neg_mod_conj [THEN conjunct1, standard]
3.258 @@ -293,47 +337,47 @@
3.259
3.260  subsection{*General Properties of div and mod*}
3.261
3.262 -lemma divmod_rel_div_mod: "b \<noteq> 0 ==> divmod_rel a b (a div b, a mod b)"
3.263 +lemma divmod_int_rel_div_mod: "b \<noteq> 0 ==> divmod_int_rel a b (a div b, a mod b)"
3.264  apply (cut_tac a = a and b = b in zmod_zdiv_equality)
3.265 -apply (force simp add: divmod_rel_def linorder_neq_iff)
3.266 +apply (force simp add: divmod_int_rel_def linorder_neq_iff)
3.267  done
3.268
3.269 -lemma divmod_rel_div: "[| divmod_rel a b (q, r);  b \<noteq> 0 |] ==> a div b = q"
3.270 -by (simp add: divmod_rel_div_mod [THEN unique_quotient])
3.271 +lemma divmod_int_rel_div: "[| divmod_int_rel a b (q, r);  b \<noteq> 0 |] ==> a div b = q"
3.272 +by (simp add: divmod_int_rel_div_mod [THEN unique_quotient])
3.273
3.274 -lemma divmod_rel_mod: "[| divmod_rel a b (q, r);  b \<noteq> 0 |] ==> a mod b = r"
3.275 -by (simp add: divmod_rel_div_mod [THEN unique_remainder])
3.276 +lemma divmod_int_rel_mod: "[| divmod_int_rel a b (q, r);  b \<noteq> 0 |] ==> a mod b = r"
3.277 +by (simp add: divmod_int_rel_div_mod [THEN unique_remainder])
3.278
3.279  lemma div_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a div b = 0"
3.280 -apply (rule divmod_rel_div)
3.281 -apply (auto simp add: divmod_rel_def)
3.282 +apply (rule divmod_int_rel_div)
3.283 +apply (auto simp add: divmod_int_rel_def)
3.284  done
3.285
3.286  lemma div_neg_neg_trivial: "[| a \<le> (0::int);  b < a |] ==> a div b = 0"
3.287 -apply (rule divmod_rel_div)
3.288 -apply (auto simp add: divmod_rel_def)
3.289 +apply (rule divmod_int_rel_div)
3.290 +apply (auto simp add: divmod_int_rel_def)
3.291  done
3.292
3.293  lemma div_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a div b = -1"
3.294 -apply (rule divmod_rel_div)
3.295 -apply (auto simp add: divmod_rel_def)
3.296 +apply (rule divmod_int_rel_div)
3.297 +apply (auto simp add: divmod_int_rel_def)
3.298  done
3.299
3.300  (*There is no div_neg_pos_trivial because  0 div b = 0 would supersede it*)
3.301
3.302  lemma mod_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a mod b = a"
3.303 -apply (rule_tac q = 0 in divmod_rel_mod)
3.304 -apply (auto simp add: divmod_rel_def)
3.305 +apply (rule_tac q = 0 in divmod_int_rel_mod)
3.306 +apply (auto simp add: divmod_int_rel_def)
3.307  done
3.308
3.309  lemma mod_neg_neg_trivial: "[| a \<le> (0::int);  b < a |] ==> a mod b = a"
3.310 -apply (rule_tac q = 0 in divmod_rel_mod)
3.311 -apply (auto simp add: divmod_rel_def)
3.312 +apply (rule_tac q = 0 in divmod_int_rel_mod)
3.313 +apply (auto simp add: divmod_int_rel_def)
3.314  done
3.315
3.316  lemma mod_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a mod b = a+b"
3.317 -apply (rule_tac q = "-1" in divmod_rel_mod)
3.318 -apply (auto simp add: divmod_rel_def)
3.319 +apply (rule_tac q = "-1" in divmod_int_rel_mod)
3.320 +apply (auto simp add: divmod_int_rel_def)
3.321  done
3.322
3.323  text{*There is no @{text mod_neg_pos_trivial}.*}
3.324 @@ -342,15 +386,15 @@
3.325  (*Simpler laws such as -a div b = -(a div b) FAIL, but see just below*)
3.326  lemma zdiv_zminus_zminus [simp]: "(-a) div (-b) = a div (b::int)"
3.327  apply (case_tac "b = 0", simp)
3.328 -apply (simp add: divmod_rel_div_mod [THEN divmod_rel_neg, simplified,
3.329 -                                 THEN divmod_rel_div, THEN sym])
3.330 +apply (simp add: divmod_int_rel_div_mod [THEN divmod_int_rel_neg, simplified,
3.331 +                                 THEN divmod_int_rel_div, THEN sym])
3.332
3.333  done
3.334
3.335  (*Simpler laws such as -a mod b = -(a mod b) FAIL, but see just below*)
3.336  lemma zmod_zminus_zminus [simp]: "(-a) mod (-b) = - (a mod (b::int))"
3.337  apply (case_tac "b = 0", simp)
3.338 -apply (subst divmod_rel_div_mod [THEN divmod_rel_neg, simplified, THEN divmod_rel_mod],
3.339 +apply (subst divmod_int_rel_div_mod [THEN divmod_int_rel_neg, simplified, THEN divmod_int_rel_mod],
3.340         auto)
3.341  done
3.342
3.343 @@ -358,22 +402,22 @@
3.344  subsection{*Laws for div and mod with Unary Minus*}
3.345
3.346  lemma zminus1_lemma:
3.347 -     "divmod_rel a b (q, r)
3.348 -      ==> divmod_rel (-a) b (if r=0 then -q else -q - 1,
3.349 +     "divmod_int_rel a b (q, r)
3.350 +      ==> divmod_int_rel (-a) b (if r=0 then -q else -q - 1,
3.351                            if r=0 then 0 else b-r)"
3.352 -by (force simp add: split_ifs divmod_rel_def linorder_neq_iff right_diff_distrib)
3.353 +by (force simp add: split_ifs divmod_int_rel_def linorder_neq_iff right_diff_distrib)
3.354
3.355
3.356  lemma zdiv_zminus1_eq_if:
3.357       "b \<noteq> (0::int)
3.358        ==> (-a) div b =
3.359            (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
3.360 -by (blast intro: divmod_rel_div_mod [THEN zminus1_lemma, THEN divmod_rel_div])
3.361 +by (blast intro: divmod_int_rel_div_mod [THEN zminus1_lemma, THEN divmod_int_rel_div])
3.362
3.363  lemma zmod_zminus1_eq_if:
3.364       "(-a::int) mod b = (if a mod b = 0 then 0 else  b - (a mod b))"
3.365  apply (case_tac "b = 0", simp)
3.366 -apply (blast intro: divmod_rel_div_mod [THEN zminus1_lemma, THEN divmod_rel_mod])
3.367 +apply (blast intro: divmod_int_rel_div_mod [THEN zminus1_lemma, THEN divmod_int_rel_mod])
3.368  done
3.369
3.370  lemma zmod_zminus1_not_zero:
3.371 @@ -416,88 +460,88 @@
3.372  apply (simp add: right_diff_distrib)
3.373  done
3.374
3.375 -lemma self_quotient: "[| divmod_rel a a (q, r);  a \<noteq> (0::int) |] ==> q = 1"
3.376 -apply (simp add: split_ifs divmod_rel_def linorder_neq_iff)
3.377 +lemma self_quotient: "[| divmod_int_rel a a (q, r);  a \<noteq> (0::int) |] ==> q = 1"
3.378 +apply (simp add: split_ifs divmod_int_rel_def linorder_neq_iff)
3.379  apply (rule order_antisym, safe, simp_all)
3.380  apply (rule_tac [3] a = "-a" and r = "-r" in self_quotient_aux1)
3.381  apply (rule_tac a = "-a" and r = "-r" in self_quotient_aux2)
3.382  apply (force intro: self_quotient_aux1 self_quotient_aux2 simp add: add_commute)+
3.383  done
3.384
3.385 -lemma self_remainder: "[| divmod_rel a a (q, r);  a \<noteq> (0::int) |] ==> r = 0"
3.386 +lemma self_remainder: "[| divmod_int_rel a a (q, r);  a \<noteq> (0::int) |] ==> r = 0"
3.387  apply (frule self_quotient, assumption)
3.388 -apply (simp add: divmod_rel_def)
3.389 +apply (simp add: divmod_int_rel_def)
3.390  done
3.391
3.392  lemma zdiv_self [simp]: "a \<noteq> 0 ==> a div a = (1::int)"
3.393 -by (simp add: divmod_rel_div_mod [THEN self_quotient])
3.394 +by (simp add: divmod_int_rel_div_mod [THEN self_quotient])
3.395
3.396  (*Here we have 0 mod 0 = 0, also assumed by Knuth (who puts m mod 0 = 0) *)
3.397  lemma zmod_self [simp]: "a mod a = (0::int)"
3.398  apply (case_tac "a = 0", simp)
3.399 -apply (simp add: divmod_rel_div_mod [THEN self_remainder])
3.400 +apply (simp add: divmod_int_rel_div_mod [THEN self_remainder])
3.401  done
3.402
3.403
3.404  subsection{*Computation of Division and Remainder*}
3.405
3.406  lemma zdiv_zero [simp]: "(0::int) div b = 0"
3.407 -by (simp add: div_def divmod_def)
3.408 +by (simp add: div_int_def divmod_int_def)
3.409
3.410  lemma div_eq_minus1: "(0::int) < b ==> -1 div b = -1"
3.411 -by (simp add: div_def divmod_def)
3.412 +by (simp add: div_int_def divmod_int_def)
3.413
3.414  lemma zmod_zero [simp]: "(0::int) mod b = 0"
3.415 -by (simp add: mod_def divmod_def)
3.416 +by (simp add: mod_int_def divmod_int_def)
3.417
3.418  lemma zmod_minus1: "(0::int) < b ==> -1 mod b = b - 1"
3.419 -by (simp add: mod_def divmod_def)
3.420 +by (simp add: mod_int_def divmod_int_def)
3.421
3.422  text{*a positive, b positive *}
3.423
3.424  lemma div_pos_pos: "[| 0 < a;  0 \<le> b |] ==> a div b = fst (posDivAlg a b)"
3.425 -by (simp add: div_def divmod_def)
3.426 +by (simp add: div_int_def divmod_int_def)
3.427
3.428  lemma mod_pos_pos: "[| 0 < a;  0 \<le> b |] ==> a mod b = snd (posDivAlg a b)"
3.429 -by (simp add: mod_def divmod_def)
3.430 +by (simp add: mod_int_def divmod_int_def)
3.431
3.432  text{*a negative, b positive *}
3.433
3.434  lemma div_neg_pos: "[| a < 0;  0 < b |] ==> a div b = fst (negDivAlg a b)"
3.435 -by (simp add: div_def divmod_def)
3.436 +by (simp add: div_int_def divmod_int_def)
3.437
3.438  lemma mod_neg_pos: "[| a < 0;  0 < b |] ==> a mod b = snd (negDivAlg a b)"
3.439 -by (simp add: mod_def divmod_def)
3.440 +by (simp add: mod_int_def divmod_int_def)
3.441
3.442  text{*a positive, b negative *}
3.443
3.444  lemma div_pos_neg:
3.445       "[| 0 < a;  b < 0 |] ==> a div b = fst (negateSnd (negDivAlg (-a) (-b)))"
3.446 -by (simp add: div_def divmod_def)
3.447 +by (simp add: div_int_def divmod_int_def)
3.448
3.449  lemma mod_pos_neg:
3.450       "[| 0 < a;  b < 0 |] ==> a mod b = snd (negateSnd (negDivAlg (-a) (-b)))"
3.451 -by (simp add: mod_def divmod_def)
3.452 +by (simp add: mod_int_def divmod_int_def)
3.453
3.454  text{*a negative, b negative *}
3.455
3.456  lemma div_neg_neg:
3.457       "[| a < 0;  b \<le> 0 |] ==> a div b = fst (negateSnd (posDivAlg (-a) (-b)))"
3.458 -by (simp add: div_def divmod_def)
3.459 +by (simp add: div_int_def divmod_int_def)
3.460
3.461  lemma mod_neg_neg:
3.462       "[| a < 0;  b \<le> 0 |] ==> a mod b = snd (negateSnd (posDivAlg (-a) (-b)))"
3.463 -by (simp add: mod_def divmod_def)
3.464 +by (simp add: mod_int_def divmod_int_def)
3.465
3.466  text {*Simplify expresions in which div and mod combine numerical constants*}
3.467
3.468 -lemma divmod_relI:
3.469 +lemma divmod_int_relI:
3.470    "\<lbrakk>a == b * q + r; if 0 < b then 0 \<le> r \<and> r < b else b < r \<and> r \<le> 0\<rbrakk>
3.471 -    \<Longrightarrow> divmod_rel a b (q, r)"
3.472 -  unfolding divmod_rel_def by simp
3.473 +    \<Longrightarrow> divmod_int_rel a b (q, r)"
3.474 +  unfolding divmod_int_rel_def by simp
3.475
3.476 -lemmas divmod_rel_div_eq = divmod_relI [THEN divmod_rel_div, THEN eq_reflection]
3.477 -lemmas divmod_rel_mod_eq = divmod_relI [THEN divmod_rel_mod, THEN eq_reflection]
3.478 +lemmas divmod_int_rel_div_eq = divmod_int_relI [THEN divmod_int_rel_div, THEN eq_reflection]
3.479 +lemmas divmod_int_rel_mod_eq = divmod_int_relI [THEN divmod_int_rel_mod, THEN eq_reflection]
3.480  lemmas arithmetic_simps =
3.481    arith_simps
3.482    add_special
3.483 @@ -533,10 +577,10 @@
3.484  *}
3.485
3.486  simproc_setup binary_int_div ("number_of m div number_of n :: int") =
3.487 -  {* K (divmod_proc (@{thm divmod_rel_div_eq})) *}
3.488 +  {* K (divmod_proc (@{thm divmod_int_rel_div_eq})) *}
3.489
3.490  simproc_setup binary_int_mod ("number_of m mod number_of n :: int") =
3.491 -  {* K (divmod_proc (@{thm divmod_rel_mod_eq})) *}
3.492 +  {* K (divmod_proc (@{thm divmod_int_rel_mod_eq})) *}
3.493
3.494  lemmas posDivAlg_eqn_number_of [simp] =
3.495      posDivAlg_eqn [of "number_of v" "number_of w", standard]
3.496 @@ -666,18 +710,18 @@
3.497  text{*proving (a*b) div c = a * (b div c) + a * (b mod c) *}
3.498
3.499  lemma zmult1_lemma:
3.500 -     "[| divmod_rel b c (q, r);  c \<noteq> 0 |]
3.501 -      ==> divmod_rel (a * b) c (a*q + a*r div c, a*r mod c)"
3.502 -by (force simp add: split_ifs divmod_rel_def linorder_neq_iff right_distrib)
3.503 +     "[| divmod_int_rel b c (q, r);  c \<noteq> 0 |]
3.504 +      ==> divmod_int_rel (a * b) c (a*q + a*r div c, a*r mod c)"
3.505 +by (auto simp add: split_ifs divmod_int_rel_def linorder_neq_iff right_distrib mult_ac)
3.506
3.507  lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)"
3.508  apply (case_tac "c = 0", simp)
3.509 -apply (blast intro: divmod_rel_div_mod [THEN zmult1_lemma, THEN divmod_rel_div])
3.510 +apply (blast intro: divmod_int_rel_div_mod [THEN zmult1_lemma, THEN divmod_int_rel_div])
3.511  done
3.512
3.513  lemma zmod_zmult1_eq: "(a*b) mod c = a*(b mod c) mod (c::int)"
3.514  apply (case_tac "c = 0", simp)
3.515 -apply (blast intro: divmod_rel_div_mod [THEN zmult1_lemma, THEN divmod_rel_mod])
3.516 +apply (blast intro: divmod_int_rel_div_mod [THEN zmult1_lemma, THEN divmod_int_rel_mod])
3.517  done
3.518
3.519  lemma zmod_zdiv_trivial: "(a mod b) div b = (0::int)"
3.520 @@ -688,15 +732,15 @@
3.521  text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *}
3.522
3.523  lemma zadd1_lemma:
3.524 -     "[| divmod_rel a c (aq, ar);  divmod_rel b c (bq, br);  c \<noteq> 0 |]
3.525 -      ==> divmod_rel (a+b) c (aq + bq + (ar+br) div c, (ar+br) mod c)"
3.526 -by (force simp add: split_ifs divmod_rel_def linorder_neq_iff right_distrib)
3.527 +     "[| divmod_int_rel a c (aq, ar);  divmod_int_rel b c (bq, br);  c \<noteq> 0 |]
3.528 +      ==> divmod_int_rel (a+b) c (aq + bq + (ar+br) div c, (ar+br) mod c)"
3.529 +by (force simp add: split_ifs divmod_int_rel_def linorder_neq_iff right_distrib)
3.530
3.531  (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
3.532  lemma zdiv_zadd1_eq:
3.533       "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)"
3.534  apply (case_tac "c = 0", simp)
3.535 -apply (blast intro: zadd1_lemma [OF divmod_rel_div_mod divmod_rel_div_mod] divmod_rel_div)
3.536 +apply (blast intro: zadd1_lemma [OF divmod_int_rel_div_mod divmod_int_rel_div_mod] divmod_int_rel_div)
3.537  done
3.538
3.539  instance int :: ring_div
3.540 @@ -715,15 +759,15 @@
3.541    next
3.542      case True then have "b \<noteq> 0" and "c \<noteq> 0" by auto
3.543      with `a \<noteq> 0`
3.544 -    have "\<And>q r. divmod_rel b c (q, r) \<Longrightarrow> divmod_rel (a * b) (a * c) (q, a * r)"
3.545 -      apply (auto simp add: divmod_rel_def)
3.546 +    have "\<And>q r. divmod_int_rel b c (q, r) \<Longrightarrow> divmod_int_rel (a * b) (a * c) (q, a * r)"
3.547 +      apply (auto simp add: divmod_int_rel_def)
3.548        apply (auto simp add: algebra_simps)
3.549 -      apply (auto simp add: zero_less_mult_iff zero_le_mult_iff mult_le_0_iff)
3.550 +      apply (auto simp add: zero_less_mult_iff zero_le_mult_iff mult_le_0_iff mult_commute [of a] mult_less_cancel_right)
3.551        done
3.552 -    moreover with `c \<noteq> 0` divmod_rel_div_mod have "divmod_rel b c (b div c, b mod c)" by auto
3.553 -    ultimately have "divmod_rel (a * b) (a * c) (b div c, a * (b mod c))" .
3.554 +    moreover with `c \<noteq> 0` divmod_int_rel_div_mod have "divmod_int_rel b c (b div c, b mod c)" by auto
3.555 +    ultimately have "divmod_int_rel (a * b) (a * c) (b div c, a * (b mod c))" .
3.556      moreover from  `a \<noteq> 0` `c \<noteq> 0` have "a * c \<noteq> 0" by simp
3.557 -    ultimately show ?thesis by (rule divmod_rel_div)
3.558 +    ultimately show ?thesis by (rule divmod_int_rel_div)
3.559    qed
3.560  qed auto
3.561
3.562 @@ -735,9 +779,9 @@
3.563    case True then show ?thesis by (simp add: posDivAlg.simps)
3.564  next
3.565    case False with assms posDivAlg_correct
3.566 -    have "divmod_rel k l (fst (posDivAlg k l), snd (posDivAlg k l))"
3.567 +    have "divmod_int_rel k l (fst (posDivAlg k l), snd (posDivAlg k l))"
3.568      by simp
3.569 -  from divmod_rel_div [OF this `l \<noteq> 0`] divmod_rel_mod [OF this `l \<noteq> 0`]
3.570 +  from divmod_int_rel_div [OF this `l \<noteq> 0`] divmod_int_rel_mod [OF this `l \<noteq> 0`]
3.571    show ?thesis by simp
3.572  qed
3.573
3.574 @@ -748,9 +792,9 @@
3.575  proof -
3.576    from assms have "l \<noteq> 0" by simp
3.577    from assms negDivAlg_correct
3.578 -    have "divmod_rel k l (fst (negDivAlg k l), snd (negDivAlg k l))"
3.579 +    have "divmod_int_rel k l (fst (negDivAlg k l), snd (negDivAlg k l))"
3.580      by simp
3.581 -  from divmod_rel_div [OF this `l \<noteq> 0`] divmod_rel_mod [OF this `l \<noteq> 0`]
3.582 +  from divmod_int_rel_div [OF this `l \<noteq> 0`] divmod_int_rel_mod [OF this `l \<noteq> 0`]
3.583    show ?thesis by simp
3.584  qed
3.585
3.586 @@ -804,21 +848,21 @@
3.587  apply simp
3.588  done
3.589
3.590 -lemma zmult2_lemma: "[| divmod_rel a b (q, r);  b \<noteq> 0;  0 < c |]
3.591 -      ==> divmod_rel a (b * c) (q div c, b*(q mod c) + r)"
3.592 -by (auto simp add: mult_ac divmod_rel_def linorder_neq_iff
3.593 +lemma zmult2_lemma: "[| divmod_int_rel a b (q, r);  b \<noteq> 0;  0 < c |]
3.594 +      ==> divmod_int_rel a (b * c) (q div c, b*(q mod c) + r)"
3.595 +by (auto simp add: mult_ac divmod_int_rel_def linorder_neq_iff
3.596                     zero_less_mult_iff right_distrib [symmetric]
3.597                     zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4)
3.598
3.599  lemma zdiv_zmult2_eq: "(0::int) < c ==> a div (b*c) = (a div b) div c"
3.600  apply (case_tac "b = 0", simp)
3.601 -apply (force simp add: divmod_rel_div_mod [THEN zmult2_lemma, THEN divmod_rel_div])
3.602 +apply (force simp add: divmod_int_rel_div_mod [THEN zmult2_lemma, THEN divmod_int_rel_div])
3.603  done
3.604
3.605  lemma zmod_zmult2_eq:
3.606       "(0::int) < c ==> a mod (b*c) = b*(a div b mod c) + a mod b"
3.607  apply (case_tac "b = 0", simp)
3.608 -apply (force simp add: divmod_rel_div_mod [THEN zmult2_lemma, THEN divmod_rel_mod])
3.609 +apply (force simp add: divmod_int_rel_div_mod [THEN zmult2_lemma, THEN divmod_int_rel_mod])
3.610  done
3.611
3.612
3.613 @@ -912,16 +956,17 @@
3.614  lemma neg_zdiv_mult_2: "a \<le> (0::int) ==> (1 + 2*b) div (2*a) = (b+1) div a"
3.615  apply (subgoal_tac " (1 + 2* (-b - 1)) div (2 * (-a)) = (-b - 1) div (-a) ")
3.616  apply (rule_tac [2] pos_zdiv_mult_2)
3.617 -apply (auto simp add: minus_mult_right [symmetric] right_diff_distrib)
3.618 +apply (auto simp add: right_diff_distrib)
3.619  apply (subgoal_tac " (-1 - (2 * b)) = - (1 + (2 * b))")
3.620 -apply (simp only: zdiv_zminus_zminus diff_minus minus_add_distrib [symmetric],
3.621 -       simp)
3.622 +apply (simp only: zdiv_zminus_zminus diff_minus minus_add_distrib [symmetric])
3.623 +apply (simp_all add: algebra_simps)
3.624 +apply (simp only: ab_diff_minus minus_add_distrib [symmetric] number_of_Min zdiv_zminus_zminus)
3.625  done
3.626
3.627  lemma zdiv_number_of_Bit0 [simp]:
3.628       "number_of (Int.Bit0 v) div number_of (Int.Bit0 w) =
3.629            number_of v div (number_of w :: int)"
3.630 -by (simp only: number_of_eq numeral_simps) simp
3.631 +by (simp only: number_of_eq numeral_simps) (simp add: mult_2 [symmetric])
3.632
3.633  lemma zdiv_number_of_Bit1 [simp]:
3.634       "number_of (Int.Bit1 v) div number_of (Int.Bit0 w) =
3.635 @@ -929,45 +974,49 @@
3.636             then number_of v div (number_of w)
3.637             else (number_of v + (1::int)) div (number_of w))"
3.638  apply (simp only: number_of_eq numeral_simps UNIV_I split: split_if)
3.639 -apply (simp add: pos_zdiv_mult_2 neg_zdiv_mult_2 add_ac)
3.640 +apply (simp add: pos_zdiv_mult_2 neg_zdiv_mult_2 add_ac mult_2 [symmetric])
3.641  done
3.642
3.643
3.644  subsection{*Computing mod by Shifting (proofs resemble those for div)*}
3.645
3.646  lemma pos_zmod_mult_2:
3.647 -     "(0::int) \<le> a ==> (1 + 2*b) mod (2*a) = 1 + 2 * (b mod a)"
3.648 -apply (case_tac "a = 0", simp)
3.649 -apply (subgoal_tac "1 < a * 2")
3.650 - prefer 2 apply arith
3.651 -apply (subgoal_tac "2* (1 + b mod a) \<le> 2*a")
3.652 - apply (rule_tac [2] mult_left_mono)
3.653 -apply (auto simp add: add_commute [of 1] mult_commute add1_zle_eq
3.654 -                      pos_mod_bound)
3.655 -apply (subst mod_add_eq)
3.656 -apply (simp add: mod_mult_mult2 mod_pos_pos_trivial)
3.657 -apply (rule mod_pos_pos_trivial)
3.658 -apply (auto simp add: mod_pos_pos_trivial ring_distribs)
3.659 -apply (subgoal_tac "0 \<le> b mod a", arith, simp)
3.660 -done
3.661 +  fixes a b :: int
3.662 +  assumes "0 \<le> a"
3.663 +  shows "(1 + 2 * b) mod (2 * a) = 1 + 2 * (b mod a)"
3.664 +proof (cases "0 < a")
3.665 +  case False with assms show ?thesis by simp
3.666 +next
3.667 +  case True
3.668 +  then have "b mod a < a" by (rule pos_mod_bound)
3.669 +  then have "1 + b mod a \<le> a" by simp
3.670 +  then have A: "2 * (1 + b mod a) \<le> 2 * a" by simp
3.671 +  from `0 < a` have "0 \<le> b mod a" by (rule pos_mod_sign)
3.672 +  then have B: "0 \<le> 1 + 2 * (b mod a)" by simp
3.673 +  have "((1\<Colon>int) mod ((2\<Colon>int) * a) + (2\<Colon>int) * b mod ((2\<Colon>int) * a)) mod ((2\<Colon>int) * a) = (1\<Colon>int) + (2\<Colon>int) * (b mod a)"
3.674 +    using `0 < a` and A
3.675 +    by (auto simp add: mod_mult_mult1 mod_pos_pos_trivial ring_distribs intro!: mod_pos_pos_trivial B)
3.676 +  then show ?thesis by (subst mod_add_eq)
3.677 +qed
3.678
3.679  lemma neg_zmod_mult_2:
3.680 -     "a \<le> (0::int) ==> (1 + 2*b) mod (2*a) = 2 * ((b+1) mod a) - 1"
3.681 -apply (subgoal_tac "(1 + 2* (-b - 1)) mod (2* (-a)) =
3.682 -                    1 + 2* ((-b - 1) mod (-a))")
3.683 -apply (rule_tac [2] pos_zmod_mult_2)
3.684 -apply (auto simp add: right_diff_distrib)
3.685 -apply (subgoal_tac " (-1 - (2 * b)) = - (1 + (2 * b))")
3.686 - prefer 2 apply simp
3.687 -apply (simp only: zmod_zminus_zminus diff_minus minus_add_distrib [symmetric])
3.688 -done
3.689 +  fixes a b :: int
3.690 +  assumes "a \<le> 0"
3.691 +  shows "(1 + 2 * b) mod (2 * a) = 2 * ((b + 1) mod a) - 1"
3.692 +proof -
3.693 +  from assms have "0 \<le> - a" by auto
3.694 +  then have "(1 + 2 * (- b - 1)) mod (2 * (- a)) = 1 + 2 * ((- b - 1) mod (- a))"
3.695 +    by (rule pos_zmod_mult_2)
3.696 +  then show ?thesis by (simp add: zmod_zminus2 algebra_simps)
3.697 +     (simp add: diff_minus add_ac)
3.698 +qed
3.699
3.700  lemma zmod_number_of_Bit0 [simp]:
3.701       "number_of (Int.Bit0 v) mod number_of (Int.Bit0 w) =
3.702        (2::int) * (number_of v mod number_of w)"
3.703  apply (simp only: number_of_eq numeral_simps)
3.704  apply (simp add: mod_mult_mult1 pos_zmod_mult_2
3.705 -                 neg_zmod_mult_2 add_ac)
3.706 +                 neg_zmod_mult_2 add_ac mult_2 [symmetric])
3.707  done
3.708
3.709  lemma zmod_number_of_Bit1 [simp]:
3.710 @@ -977,7 +1026,7 @@
3.711                  else 2 * ((number_of v + (1::int)) mod number_of w) - 1)"
3.712  apply (simp only: number_of_eq numeral_simps)
3.713  apply (simp add: mod_mult_mult1 pos_zmod_mult_2
3.714 -                 neg_zmod_mult_2 add_ac)
3.715 +                 neg_zmod_mult_2 add_ac mult_2 [symmetric])
3.716  done
3.717
3.718
3.719 @@ -1045,7 +1094,7 @@
3.720  apply (subst split_div, auto)
3.721  apply (subst split_zdiv, auto)
3.722  apply (rule_tac a="int (b * i) + int j" and b="int b" and r="int j" and r'=ja in IntDiv.unique_quotient)
3.723 -apply (auto simp add: IntDiv.divmod_rel_def of_nat_mult)
3.724 +apply (auto simp add: IntDiv.divmod_int_rel_def of_nat_mult)
3.725  done
3.726
3.727  lemma zmod_int: "int (a mod b) = (int a) mod (int b)"
3.728 @@ -1053,7 +1102,7 @@
3.729  apply (subst split_zmod, auto)
3.730  apply (rule_tac a="int (b * i) + int j" and b="int b" and q="int i" and q'=ia
3.731         in unique_remainder)
3.732 -apply (auto simp add: IntDiv.divmod_rel_def of_nat_mult)
3.733 +apply (auto simp add: IntDiv.divmod_int_rel_def of_nat_mult)
3.734  done
3.735
3.736  lemma abs_div: "(y::int) dvd x \<Longrightarrow> abs (x div y) = abs x div abs y"
3.737 @@ -1123,7 +1172,7 @@
3.738  lemma of_int_num [code]:
3.739    "of_int k = (if k = 0 then 0 else if k < 0 then
3.740       - of_int (- k) else let
3.741 -       (l, m) = divmod k 2;
3.742 +       (l, m) = divmod_int k 2;
3.743         l' = of_int l
3.744       in if m = 0 then l' + l' else l' + l' + 1)"
3.745  proof -
3.746 @@ -1151,7 +1200,7 @@
3.747      show "x * of_int 2 = x + x"
3.748      unfolding int2 of_int_add right_distrib by simp
3.749    qed
3.750 -  from aux1 show ?thesis by (auto simp add: divmod_mod_div Let_def aux2 aux3)
3.751 +  from aux1 show ?thesis by (auto simp add: divmod_int_mod_div Let_def aux2 aux3)
3.752  qed
3.753
3.754  end
3.755 @@ -1278,7 +1327,7 @@
3.756    "pdivmod k l = (if l = 0 then (0, \<bar>k\<bar>) else posDivAlg \<bar>k\<bar> \<bar>l\<bar>)"
3.757  by (subst posDivAlg_div_mod) (simp_all add: pdivmod_def)
3.758
3.759 -lemma divmod_pdivmod: "divmod k l = (if k = 0 then (0, 0) else if l = 0 then (0, k) else
3.760 +lemma divmod_int_pdivmod: "divmod_int k l = (if k = 0 then (0, 0) else if l = 0 then (0, k) else
3.761    apsnd ((op *) (sgn l)) (if 0 < l \<and> 0 \<le> k \<or> l < 0 \<and> k < 0
3.762      then pdivmod k l
3.763      else (let (r, s) = pdivmod k l in
3.764 @@ -1286,12 +1335,12 @@
3.765  proof -
3.766    have aux: "\<And>q::int. - k = l * q \<longleftrightarrow> k = l * - q" by auto
3.767    show ?thesis
3.768 -    by (simp add: divmod_mod_div pdivmod_def)
3.769 +    by (simp add: divmod_int_mod_div pdivmod_def)
3.770        (auto simp add: aux not_less not_le zdiv_zminus1_eq_if
3.771        zmod_zminus1_eq_if zdiv_zminus2_eq_if zmod_zminus2_eq_if)
3.772  qed
3.773
3.774 -lemma divmod_code [code]: "divmod k l = (if k = 0 then (0, 0) else if l = 0 then (0, k) else
3.775 +lemma divmod_int_code [code]: "divmod_int k l = (if k = 0 then (0, 0) else if l = 0 then (0, k) else
3.776    apsnd ((op *) (sgn l)) (if sgn k = sgn l
3.777      then pdivmod k l
3.778      else (let (r, s) = pdivmod k l in
3.779 @@ -1299,7 +1348,7 @@
3.780  proof -
3.781    have "k \<noteq> 0 \<Longrightarrow> l \<noteq> 0 \<Longrightarrow> 0 < l \<and> 0 \<le> k \<or> l < 0 \<and> k < 0 \<longleftrightarrow> sgn k = sgn l"
3.782      by (auto simp add: not_less sgn_if)
3.783 -  then show ?thesis by (simp add: divmod_pdivmod)
3.784 +  then show ?thesis by (simp add: divmod_int_pdivmod)
3.785  qed
3.786
3.787  code_modulename SML
3.788 @@ -1311,4 +1360,115 @@
3.789  code_modulename Haskell
3.790    IntDiv Integer
3.791
3.792 +
3.793 +
3.794 +subsection {* Proof Tools setup; Combination and Cancellation Simprocs *}
3.795 +
3.796 +declare split_div[of _ _ "number_of k", standard, arith_split]
3.797 +declare split_mod[of _ _ "number_of k", standard, arith_split]
3.798 +
3.799 +
3.800 +subsubsection{*For @{text combine_numerals}*}
3.801 +
3.802 +lemma left_add_mult_distrib: "i*u + (j*u + k) = (i+j)*u + (k::nat)"
3.803 +by (simp add: add_mult_distrib)
3.804 +
3.805 +
3.806 +subsubsection{*For @{text cancel_numerals}*}
3.807 +
3.808 +lemma nat_diff_add_eq1:
3.809 +     "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)"
3.810 +by (simp split add: nat_diff_split add: add_mult_distrib)
3.811 +
3.812 +lemma nat_diff_add_eq2:
3.813 +     "i <= (j::nat) ==> ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))"
3.814 +by (simp split add: nat_diff_split add: add_mult_distrib)
3.815 +
3.816 +lemma nat_eq_add_iff1:
3.817 +     "j <= (i::nat) ==> (i*u + m = j*u + n) = ((i-j)*u + m = n)"
3.818 +by (auto split add: nat_diff_split simp add: add_mult_distrib)
3.819 +
3.820 +lemma nat_eq_add_iff2:
3.821 +     "i <= (j::nat) ==> (i*u + m = j*u + n) = (m = (j-i)*u + n)"
3.822 +by (auto split add: nat_diff_split simp add: add_mult_distrib)
3.823 +
3.824 +lemma nat_less_add_iff1:
3.825 +     "j <= (i::nat) ==> (i*u + m < j*u + n) = ((i-j)*u + m < n)"
3.826 +by (auto split add: nat_diff_split simp add: add_mult_distrib)
3.827 +
3.828 +lemma nat_less_add_iff2:
3.829 +     "i <= (j::nat) ==> (i*u + m < j*u + n) = (m < (j-i)*u + n)"
3.830 +by (auto split add: nat_diff_split simp add: add_mult_distrib)
3.831 +
3.832 +lemma nat_le_add_iff1:
3.833 +     "j <= (i::nat) ==> (i*u + m <= j*u + n) = ((i-j)*u + m <= n)"
3.834 +by (auto split add: nat_diff_split simp add: add_mult_distrib)
3.835 +
3.836 +lemma nat_le_add_iff2:
3.837 +     "i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)"
3.838 +by (auto split add: nat_diff_split simp add: add_mult_distrib)
3.839 +
3.840 +
3.841 +subsubsection{*For @{text cancel_numeral_factors} *}
3.842 +
3.843 +lemma nat_mult_le_cancel1: "(0::nat) < k ==> (k*m <= k*n) = (m<=n)"
3.844 +by auto
3.845 +
3.846 +lemma nat_mult_less_cancel1: "(0::nat) < k ==> (k*m < k*n) = (m<n)"
3.847 +by auto
3.848 +
3.849 +lemma nat_mult_eq_cancel1: "(0::nat) < k ==> (k*m = k*n) = (m=n)"
3.850 +by auto
3.851 +
3.852 +lemma nat_mult_div_cancel1: "(0::nat) < k ==> (k*m) div (k*n) = (m div n)"
3.853 +by auto
3.854 +
3.855 +lemma nat_mult_dvd_cancel_disj[simp]:
3.856 +  "(k*m) dvd (k*n) = (k=0 | m dvd (n::nat))"
3.857 +by(auto simp: dvd_eq_mod_eq_0 mod_mult_distrib2[symmetric])
3.858 +
3.859 +lemma nat_mult_dvd_cancel1: "0 < k \<Longrightarrow> (k*m) dvd (k*n::nat) = (m dvd n)"
3.860 +by(auto)
3.861 +
3.862 +
3.863 +subsubsection{*For @{text cancel_factor} *}
3.864 +
3.865 +lemma nat_mult_le_cancel_disj: "(k*m <= k*n) = ((0::nat) < k --> m<=n)"
3.866 +by auto
3.867 +
3.868 +lemma nat_mult_less_cancel_disj: "(k*m < k*n) = ((0::nat) < k & m<n)"
3.869 +by auto
3.870 +
3.871 +lemma nat_mult_eq_cancel_disj: "(k*m = k*n) = (k = (0::nat) | m=n)"
3.872 +by auto
3.873 +
3.874 +lemma nat_mult_div_cancel_disj[simp]:
3.875 +     "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)"
3.876 +by (simp add: nat_mult_div_cancel1)
3.877 +
3.878 +
3.879 +use "Tools/numeral_simprocs.ML"
3.880 +
3.881 +use "Tools/nat_numeral_simprocs.ML"
3.882 +
3.883 +declaration {*
3.884 +  K (Lin_Arith.add_simps (@{thms neg_simps} @ [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}])
3.885 +  #> Lin_Arith.add_simps (@{thms ring_distribs} @ [@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1},
3.886 +     @{thm nat_0}, @{thm nat_1},
3.887 +     @{thm add_nat_number_of}, @{thm diff_nat_number_of}, @{thm mult_nat_number_of},
3.888 +     @{thm eq_nat_number_of}, @{thm less_nat_number_of}, @{thm le_number_of_eq_not_less},
3.889 +     @{thm le_Suc_number_of}, @{thm le_number_of_Suc},
3.890 +     @{thm less_Suc_number_of}, @{thm less_number_of_Suc},
3.891 +     @{thm Suc_eq_number_of}, @{thm eq_number_of_Suc},
3.892 +     @{thm mult_Suc}, @{thm mult_Suc_right},
3.893 +     @{thm add_Suc}, @{thm add_Suc_right},
3.894 +     @{thm eq_number_of_0}, @{thm eq_0_number_of}, @{thm less_0_number_of},
3.895 +     @{thm of_int_number_of_eq}, @{thm of_nat_number_of_eq}, @{thm nat_number_of},
3.896 +     @{thm if_True}, @{thm if_False}])
3.897 +  #> Lin_Arith.add_simprocs (Numeral_Simprocs.assoc_fold_simproc
3.898 +      :: Numeral_Simprocs.combine_numerals
3.899 +      :: Numeral_Simprocs.cancel_numerals)
3.900 +  #> Lin_Arith.add_simprocs (Nat_Numeral_Simprocs.combine_numerals :: Nat_Numeral_Simprocs.cancel_numerals))
3.901 +*}
3.902 +
3.903  end
```
```     4.1 --- a/src/HOL/Nat_Transfer.thy	Thu Oct 29 13:37:55 2009 +0100
4.2 +++ b/src/HOL/Nat_Transfer.thy	Thu Oct 29 22:13:09 2009 +0100
4.3 @@ -67,8 +67,7 @@
4.4      "(2::int) >= 0"
4.5      "(3::int) >= 0"
4.6      "int z >= 0"
4.7 -  apply (auto simp add: zero_le_mult_iff tsub_def)
4.8 -done
4.9 +  by (auto simp add: zero_le_mult_iff tsub_def)
4.10
4.11  lemma transfer_nat_int_relations:
4.12      "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
```