moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
authorhaftmann
Thu Oct 29 22:13:09 2009 +0100 (2009-10-29)
changeset 33340a165b97f3658
parent 33322 6ff4674499ca
child 33341 5a989586d102
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
src/HOL/Code_Numeral.thy
src/HOL/Divides.thy
src/HOL/IntDiv.thy
src/HOL/Nat_Transfer.thy
     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>