src/HOL/Divides.thy
changeset 33340 a165b97f3658
parent 33318 ddd97d9dfbfb
child 33361 1f18de40b43f
     1.1 --- a/src/HOL/Divides.thy	Thu Oct 29 13:37:55 2009 +0100
     1.2 +++ b/src/HOL/Divides.thy	Thu Oct 29 22:13:09 2009 +0100
     1.3 @@ -7,15 +7,7 @@
     1.4  
     1.5  theory Divides
     1.6  imports Nat_Numeral Nat_Transfer
     1.7 -uses
     1.8 -  "~~/src/Provers/Arith/assoc_fold.ML"
     1.9 -  "~~/src/Provers/Arith/cancel_numerals.ML"
    1.10 -  "~~/src/Provers/Arith/combine_numerals.ML"
    1.11 -  "~~/src/Provers/Arith/cancel_numeral_factor.ML"
    1.12 -  "~~/src/Provers/Arith/extract_common_term.ML"
    1.13 -  ("Tools/numeral_simprocs.ML")
    1.14 -  ("Tools/nat_numeral_simprocs.ML")
    1.15 -  "~~/src/Provers/Arith/cancel_div_mod.ML"
    1.16 +uses "~~/src/Provers/Arith/cancel_div_mod.ML"
    1.17  begin
    1.18  
    1.19  subsection {* Syntactic division operations *}
    1.20 @@ -435,18 +427,18 @@
    1.21    @{term "q\<Colon>nat"}(uotient) and @{term "r\<Colon>nat"}(emainder).
    1.22  *}
    1.23  
    1.24 -definition divmod_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat \<Rightarrow> bool" where
    1.25 -  "divmod_rel m n qr \<longleftrightarrow>
    1.26 +definition divmod_nat_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat \<Rightarrow> bool" where
    1.27 +  "divmod_nat_rel m n qr \<longleftrightarrow>
    1.28      m = fst qr * n + snd qr \<and>
    1.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)"
    1.30  
    1.31 -text {* @{const divmod_rel} is total: *}
    1.32 +text {* @{const divmod_nat_rel} is total: *}
    1.33  
    1.34 -lemma divmod_rel_ex:
    1.35 -  obtains q r where "divmod_rel m n (q, r)"
    1.36 +lemma divmod_nat_rel_ex:
    1.37 +  obtains q r where "divmod_nat_rel m n (q, r)"
    1.38  proof (cases "n = 0")
    1.39    case True  with that show thesis
    1.40 -    by (auto simp add: divmod_rel_def)
    1.41 +    by (auto simp add: divmod_nat_rel_def)
    1.42  next
    1.43    case False
    1.44    have "\<exists>q r. m = q * n + r \<and> r < n"
    1.45 @@ -470,19 +462,19 @@
    1.46      qed
    1.47    qed
    1.48    with that show thesis
    1.49 -    using `n \<noteq> 0` by (auto simp add: divmod_rel_def)
    1.50 +    using `n \<noteq> 0` by (auto simp add: divmod_nat_rel_def)
    1.51  qed
    1.52  
    1.53 -text {* @{const divmod_rel} is injective: *}
    1.54 +text {* @{const divmod_nat_rel} is injective: *}
    1.55  
    1.56 -lemma divmod_rel_unique:
    1.57 -  assumes "divmod_rel m n qr"
    1.58 -    and "divmod_rel m n qr'"
    1.59 +lemma divmod_nat_rel_unique:
    1.60 +  assumes "divmod_nat_rel m n qr"
    1.61 +    and "divmod_nat_rel m n qr'"
    1.62    shows "qr = qr'"
    1.63  proof (cases "n = 0")
    1.64    case True with assms show ?thesis
    1.65      by (cases qr, cases qr')
    1.66 -      (simp add: divmod_rel_def)
    1.67 +      (simp add: divmod_nat_rel_def)
    1.68  next
    1.69    case False
    1.70    have aux: "\<And>q r q' r'. q' * n + r' = q * n + r \<Longrightarrow> r < n \<Longrightarrow> q' \<le> (q\<Colon>nat)"
    1.71 @@ -491,91 +483,91 @@
    1.72    apply (auto simp add: add_mult_distrib)
    1.73    done
    1.74    from `n \<noteq> 0` assms have "fst qr = fst qr'"
    1.75 -    by (auto simp add: divmod_rel_def intro: order_antisym dest: aux sym)
    1.76 +    by (auto simp add: divmod_nat_rel_def intro: order_antisym dest: aux sym)
    1.77    moreover from this assms have "snd qr = snd qr'"
    1.78 -    by (simp add: divmod_rel_def)
    1.79 +    by (simp add: divmod_nat_rel_def)
    1.80    ultimately show ?thesis by (cases qr, cases qr') simp
    1.81  qed
    1.82  
    1.83  text {*
    1.84    We instantiate divisibility on the natural numbers by
    1.85 -  means of @{const divmod_rel}:
    1.86 +  means of @{const divmod_nat_rel}:
    1.87  *}
    1.88  
    1.89  instantiation nat :: semiring_div
    1.90  begin
    1.91  
    1.92 -definition divmod :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
    1.93 -  [code del]: "divmod m n = (THE qr. divmod_rel m n qr)"
    1.94 +definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
    1.95 +  [code del]: "divmod_nat m n = (THE qr. divmod_nat_rel m n qr)"
    1.96  
    1.97 -lemma divmod_rel_divmod:
    1.98 -  "divmod_rel m n (divmod m n)"
    1.99 +lemma divmod_nat_rel_divmod_nat:
   1.100 +  "divmod_nat_rel m n (divmod_nat m n)"
   1.101  proof -
   1.102 -  from divmod_rel_ex
   1.103 -    obtain qr where rel: "divmod_rel m n qr" .
   1.104 +  from divmod_nat_rel_ex
   1.105 +    obtain qr where rel: "divmod_nat_rel m n qr" .
   1.106    then show ?thesis
   1.107 -  by (auto simp add: divmod_def intro: theI elim: divmod_rel_unique)
   1.108 +  by (auto simp add: divmod_nat_def intro: theI elim: divmod_nat_rel_unique)
   1.109  qed
   1.110  
   1.111 -lemma divmod_eq:
   1.112 -  assumes "divmod_rel m n qr" 
   1.113 -  shows "divmod m n = qr"
   1.114 -  using assms by (auto intro: divmod_rel_unique divmod_rel_divmod)
   1.115 +lemma divmod_nat_eq:
   1.116 +  assumes "divmod_nat_rel m n qr" 
   1.117 +  shows "divmod_nat m n = qr"
   1.118 +  using assms by (auto intro: divmod_nat_rel_unique divmod_nat_rel_divmod_nat)
   1.119  
   1.120  definition div_nat where
   1.121 -  "m div n = fst (divmod m n)"
   1.122 +  "m div n = fst (divmod_nat m n)"
   1.123  
   1.124  definition mod_nat where
   1.125 -  "m mod n = snd (divmod m n)"
   1.126 +  "m mod n = snd (divmod_nat m n)"
   1.127  
   1.128 -lemma divmod_div_mod:
   1.129 -  "divmod m n = (m div n, m mod n)"
   1.130 +lemma divmod_nat_div_mod:
   1.131 +  "divmod_nat m n = (m div n, m mod n)"
   1.132    unfolding div_nat_def mod_nat_def by simp
   1.133  
   1.134  lemma div_eq:
   1.135 -  assumes "divmod_rel m n (q, r)" 
   1.136 +  assumes "divmod_nat_rel m n (q, r)" 
   1.137    shows "m div n = q"
   1.138 -  using assms by (auto dest: divmod_eq simp add: divmod_div_mod)
   1.139 +  using assms by (auto dest: divmod_nat_eq simp add: divmod_nat_div_mod)
   1.140  
   1.141  lemma mod_eq:
   1.142 -  assumes "divmod_rel m n (q, r)" 
   1.143 +  assumes "divmod_nat_rel m n (q, r)" 
   1.144    shows "m mod n = r"
   1.145 -  using assms by (auto dest: divmod_eq simp add: divmod_div_mod)
   1.146 +  using assms by (auto dest: divmod_nat_eq simp add: divmod_nat_div_mod)
   1.147  
   1.148 -lemma divmod_rel: "divmod_rel m n (m div n, m mod n)"
   1.149 -  by (simp add: div_nat_def mod_nat_def divmod_rel_divmod)
   1.150 +lemma divmod_nat_rel: "divmod_nat_rel m n (m div n, m mod n)"
   1.151 +  by (simp add: div_nat_def mod_nat_def divmod_nat_rel_divmod_nat)
   1.152  
   1.153 -lemma divmod_zero:
   1.154 -  "divmod m 0 = (0, m)"
   1.155 +lemma divmod_nat_zero:
   1.156 +  "divmod_nat m 0 = (0, m)"
   1.157  proof -
   1.158 -  from divmod_rel [of m 0] show ?thesis
   1.159 -    unfolding divmod_div_mod divmod_rel_def by simp
   1.160 +  from divmod_nat_rel [of m 0] show ?thesis
   1.161 +    unfolding divmod_nat_div_mod divmod_nat_rel_def by simp
   1.162  qed
   1.163  
   1.164 -lemma divmod_base:
   1.165 +lemma divmod_nat_base:
   1.166    assumes "m < n"
   1.167 -  shows "divmod m n = (0, m)"
   1.168 +  shows "divmod_nat m n = (0, m)"
   1.169  proof -
   1.170 -  from divmod_rel [of m n] show ?thesis
   1.171 -    unfolding divmod_div_mod divmod_rel_def
   1.172 +  from divmod_nat_rel [of m n] show ?thesis
   1.173 +    unfolding divmod_nat_div_mod divmod_nat_rel_def
   1.174      using assms by (cases "m div n = 0")
   1.175        (auto simp add: gr0_conv_Suc [of "m div n"])
   1.176  qed
   1.177  
   1.178 -lemma divmod_step:
   1.179 +lemma divmod_nat_step:
   1.180    assumes "0 < n" and "n \<le> m"
   1.181 -  shows "divmod m n = (Suc ((m - n) div n), (m - n) mod n)"
   1.182 +  shows "divmod_nat m n = (Suc ((m - n) div n), (m - n) mod n)"
   1.183  proof -
   1.184 -  from divmod_rel have divmod_m_n: "divmod_rel m n (m div n, m mod n)" .
   1.185 +  from divmod_nat_rel have divmod_nat_m_n: "divmod_nat_rel m n (m div n, m mod n)" .
   1.186    with assms have m_div_n: "m div n \<ge> 1"
   1.187 -    by (cases "m div n") (auto simp add: divmod_rel_def)
   1.188 -  from assms divmod_m_n have "divmod_rel (m - n) n (m div n - Suc 0, m mod n)"
   1.189 -    by (cases "m div n") (auto simp add: divmod_rel_def)
   1.190 -  with divmod_eq have "divmod (m - n) n = (m div n - Suc 0, m mod n)" by simp
   1.191 -  moreover from divmod_div_mod have "divmod (m - n) n = ((m - n) div n, (m - n) mod n)" .
   1.192 +    by (cases "m div n") (auto simp add: divmod_nat_rel_def)
   1.193 +  from assms divmod_nat_m_n have "divmod_nat_rel (m - n) n (m div n - Suc 0, m mod n)"
   1.194 +    by (cases "m div n") (auto simp add: divmod_nat_rel_def)
   1.195 +  with divmod_nat_eq have "divmod_nat (m - n) n = (m div n - Suc 0, m mod n)" by simp
   1.196 +  moreover from divmod_nat_div_mod have "divmod_nat (m - n) n = ((m - n) div n, (m - n) mod n)" .
   1.197    ultimately have "m div n = Suc ((m - n) div n)"
   1.198      and "m mod n = (m - n) mod n" using m_div_n by simp_all
   1.199 -  then show ?thesis using divmod_div_mod by simp
   1.200 +  then show ?thesis using divmod_nat_div_mod by simp
   1.201  qed
   1.202  
   1.203  text {* The ''recursion'' equations for @{const div} and @{const mod} *}
   1.204 @@ -584,29 +576,29 @@
   1.205    fixes m n :: nat
   1.206    assumes "m < n"
   1.207    shows "m div n = 0"
   1.208 -  using assms divmod_base divmod_div_mod by simp
   1.209 +  using assms divmod_nat_base divmod_nat_div_mod by simp
   1.210  
   1.211  lemma le_div_geq:
   1.212    fixes m n :: nat
   1.213    assumes "0 < n" and "n \<le> m"
   1.214    shows "m div n = Suc ((m - n) div n)"
   1.215 -  using assms divmod_step divmod_div_mod by simp
   1.216 +  using assms divmod_nat_step divmod_nat_div_mod by simp
   1.217  
   1.218  lemma mod_less [simp]:
   1.219    fixes m n :: nat
   1.220    assumes "m < n"
   1.221    shows "m mod n = m"
   1.222 -  using assms divmod_base divmod_div_mod by simp
   1.223 +  using assms divmod_nat_base divmod_nat_div_mod by simp
   1.224  
   1.225  lemma le_mod_geq:
   1.226    fixes m n :: nat
   1.227    assumes "n \<le> m"
   1.228    shows "m mod n = (m - n) mod n"
   1.229 -  using assms divmod_step divmod_div_mod by (cases "n = 0") simp_all
   1.230 +  using assms divmod_nat_step divmod_nat_div_mod by (cases "n = 0") simp_all
   1.231  
   1.232  instance proof -
   1.233    have [simp]: "\<And>n::nat. n div 0 = 0"
   1.234 -    by (simp add: div_nat_def divmod_zero)
   1.235 +    by (simp add: div_nat_def divmod_nat_zero)
   1.236    have [simp]: "\<And>n::nat. 0 div n = 0"
   1.237    proof -
   1.238      fix n :: nat
   1.239 @@ -616,7 +608,7 @@
   1.240    show "OFCLASS(nat, semiring_div_class)" proof
   1.241      fix m n :: nat
   1.242      show "m div n * n + m mod n = m"
   1.243 -      using divmod_rel [of m n] by (simp add: divmod_rel_def)
   1.244 +      using divmod_nat_rel [of m n] by (simp add: divmod_nat_rel_def)
   1.245    next
   1.246      fix m n q :: nat
   1.247      assume "n \<noteq> 0"
   1.248 @@ -631,10 +623,10 @@
   1.249      next
   1.250        case True with `m \<noteq> 0`
   1.251          have "m > 0" and "n > 0" and "q > 0" by auto
   1.252 -      then have "\<And>a b. divmod_rel n q (a, b) \<Longrightarrow> divmod_rel (m * n) (m * q) (a, m * b)"
   1.253 -        by (auto simp add: divmod_rel_def) (simp_all add: algebra_simps)
   1.254 -      moreover from divmod_rel have "divmod_rel n q (n div q, n mod q)" .
   1.255 -      ultimately have "divmod_rel (m * n) (m * q) (n div q, m * (n mod q))" .
   1.256 +      then have "\<And>a b. divmod_nat_rel n q (a, b) \<Longrightarrow> divmod_nat_rel (m * n) (m * q) (a, m * b)"
   1.257 +        by (auto simp add: divmod_nat_rel_def) (simp_all add: algebra_simps)
   1.258 +      moreover from divmod_nat_rel have "divmod_nat_rel n q (n div q, n mod q)" .
   1.259 +      ultimately have "divmod_nat_rel (m * n) (m * q) (n div q, m * (n mod q))" .
   1.260        then show ?thesis by (simp add: div_eq)
   1.261      qed
   1.262    qed simp_all
   1.263 @@ -676,10 +668,10 @@
   1.264  
   1.265  text {* code generator setup *}
   1.266  
   1.267 -lemma divmod_if [code]: "divmod m n = (if n = 0 \<or> m < n then (0, m) else
   1.268 -  let (q, r) = divmod (m - n) n in (Suc q, r))"
   1.269 -by (simp add: divmod_zero divmod_base divmod_step)
   1.270 -    (simp add: divmod_div_mod)
   1.271 +lemma divmod_nat_if [code]: "divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
   1.272 +  let (q, r) = divmod_nat (m - n) n in (Suc q, r))"
   1.273 +by (simp add: divmod_nat_zero divmod_nat_base divmod_nat_step)
   1.274 +    (simp add: divmod_nat_div_mod)
   1.275  
   1.276  code_modulename SML
   1.277    Divides Nat
   1.278 @@ -712,7 +704,7 @@
   1.279    fixes m n :: nat
   1.280    assumes "n > 0"
   1.281    shows "m mod n < (n::nat)"
   1.282 -  using assms divmod_rel [of m n] unfolding divmod_rel_def by auto
   1.283 +  using assms divmod_nat_rel [of m n] unfolding divmod_nat_rel_def by auto
   1.284  
   1.285  lemma mod_less_eq_dividend [simp]:
   1.286    fixes m n :: nat
   1.287 @@ -753,27 +745,27 @@
   1.288  
   1.289  subsubsection {* Quotient and Remainder *}
   1.290  
   1.291 -lemma divmod_rel_mult1_eq:
   1.292 -  "divmod_rel b c (q, r) \<Longrightarrow> c > 0
   1.293 -   \<Longrightarrow> divmod_rel (a * b) c (a * q + a * r div c, a * r mod c)"
   1.294 -by (auto simp add: split_ifs divmod_rel_def algebra_simps)
   1.295 +lemma divmod_nat_rel_mult1_eq:
   1.296 +  "divmod_nat_rel b c (q, r) \<Longrightarrow> c > 0
   1.297 +   \<Longrightarrow> divmod_nat_rel (a * b) c (a * q + a * r div c, a * r mod c)"
   1.298 +by (auto simp add: split_ifs divmod_nat_rel_def algebra_simps)
   1.299  
   1.300  lemma div_mult1_eq:
   1.301    "(a * b) div c = a * (b div c) + a * (b mod c) div (c::nat)"
   1.302  apply (cases "c = 0", simp)
   1.303 -apply (blast intro: divmod_rel [THEN divmod_rel_mult1_eq, THEN div_eq])
   1.304 +apply (blast intro: divmod_nat_rel [THEN divmod_nat_rel_mult1_eq, THEN div_eq])
   1.305  done
   1.306  
   1.307 -lemma divmod_rel_add1_eq:
   1.308 -  "divmod_rel a c (aq, ar) \<Longrightarrow> divmod_rel b c (bq, br) \<Longrightarrow>  c > 0
   1.309 -   \<Longrightarrow> divmod_rel (a + b) c (aq + bq + (ar + br) div c, (ar + br) mod c)"
   1.310 -by (auto simp add: split_ifs divmod_rel_def algebra_simps)
   1.311 +lemma divmod_nat_rel_add1_eq:
   1.312 +  "divmod_nat_rel a c (aq, ar) \<Longrightarrow> divmod_nat_rel b c (bq, br) \<Longrightarrow>  c > 0
   1.313 +   \<Longrightarrow> divmod_nat_rel (a + b) c (aq + bq + (ar + br) div c, (ar + br) mod c)"
   1.314 +by (auto simp add: split_ifs divmod_nat_rel_def algebra_simps)
   1.315  
   1.316  (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
   1.317  lemma div_add1_eq:
   1.318    "(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"
   1.319  apply (cases "c = 0", simp)
   1.320 -apply (blast intro: divmod_rel_add1_eq [THEN div_eq] divmod_rel)
   1.321 +apply (blast intro: divmod_nat_rel_add1_eq [THEN div_eq] divmod_nat_rel)
   1.322  done
   1.323  
   1.324  lemma mod_lemma: "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c"
   1.325 @@ -783,21 +775,21 @@
   1.326    apply (simp add: add_mult_distrib2)
   1.327    done
   1.328  
   1.329 -lemma divmod_rel_mult2_eq:
   1.330 -  "divmod_rel a b (q, r) \<Longrightarrow> 0 < b \<Longrightarrow> 0 < c
   1.331 -   \<Longrightarrow> divmod_rel a (b * c) (q div c, b *(q mod c) + r)"
   1.332 -by (auto simp add: mult_ac divmod_rel_def add_mult_distrib2 [symmetric] mod_lemma)
   1.333 +lemma divmod_nat_rel_mult2_eq:
   1.334 +  "divmod_nat_rel a b (q, r) \<Longrightarrow> 0 < b \<Longrightarrow> 0 < c
   1.335 +   \<Longrightarrow> divmod_nat_rel a (b * c) (q div c, b *(q mod c) + r)"
   1.336 +by (auto simp add: mult_ac divmod_nat_rel_def add_mult_distrib2 [symmetric] mod_lemma)
   1.337  
   1.338  lemma div_mult2_eq: "a div (b*c) = (a div b) div (c::nat)"
   1.339    apply (cases "b = 0", simp)
   1.340    apply (cases "c = 0", simp)
   1.341 -  apply (force simp add: divmod_rel [THEN divmod_rel_mult2_eq, THEN div_eq])
   1.342 +  apply (force simp add: divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN div_eq])
   1.343    done
   1.344  
   1.345  lemma mod_mult2_eq: "a mod (b*c) = b*(a div b mod c) + a mod (b::nat)"
   1.346    apply (cases "b = 0", simp)
   1.347    apply (cases "c = 0", simp)
   1.348 -  apply (auto simp add: mult_commute divmod_rel [THEN divmod_rel_mult2_eq, THEN mod_eq])
   1.349 +  apply (auto simp add: mult_commute divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN mod_eq])
   1.350    done
   1.351  
   1.352  
   1.353 @@ -944,9 +936,9 @@
   1.354    from A B show ?lhs ..
   1.355  next
   1.356    assume P: ?lhs
   1.357 -  then have "divmod_rel m n (q, m - n * q)"
   1.358 -    unfolding divmod_rel_def by (auto simp add: mult_ac)
   1.359 -  with divmod_rel_unique divmod_rel [of m n]
   1.360 +  then have "divmod_nat_rel m n (q, m - n * q)"
   1.361 +    unfolding divmod_nat_rel_def by (auto simp add: mult_ac)
   1.362 +  with divmod_nat_rel_unique divmod_nat_rel [of m n]
   1.363    have "(q, m - n * q) = (m div n, m mod n)" by auto
   1.364    then show ?rhs by simp
   1.365  qed
   1.366 @@ -1144,114 +1136,4 @@
   1.367      Suc_mod_eq_add3_mod [of _ "number_of v", standard]
   1.368  declare Suc_mod_eq_add3_mod_number_of [simp]
   1.369  
   1.370 -
   1.371 -subsection {* Proof Tools setup; Combination and Cancellation Simprocs *}
   1.372 -
   1.373 -declare split_div[of _ _ "number_of k", standard, arith_split]
   1.374 -declare split_mod[of _ _ "number_of k", standard, arith_split]
   1.375 -
   1.376 -
   1.377 -subsubsection{*For @{text combine_numerals}*}
   1.378 -
   1.379 -lemma left_add_mult_distrib: "i*u + (j*u + k) = (i+j)*u + (k::nat)"
   1.380 -by (simp add: add_mult_distrib)
   1.381 -
   1.382 -
   1.383 -subsubsection{*For @{text cancel_numerals}*}
   1.384 -
   1.385 -lemma nat_diff_add_eq1:
   1.386 -     "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)"
   1.387 -by (simp split add: nat_diff_split add: add_mult_distrib)
   1.388 -
   1.389 -lemma nat_diff_add_eq2:
   1.390 -     "i <= (j::nat) ==> ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))"
   1.391 -by (simp split add: nat_diff_split add: add_mult_distrib)
   1.392 -
   1.393 -lemma nat_eq_add_iff1:
   1.394 -     "j <= (i::nat) ==> (i*u + m = j*u + n) = ((i-j)*u + m = n)"
   1.395 -by (auto split add: nat_diff_split simp add: add_mult_distrib)
   1.396 -
   1.397 -lemma nat_eq_add_iff2:
   1.398 -     "i <= (j::nat) ==> (i*u + m = j*u + n) = (m = (j-i)*u + n)"
   1.399 -by (auto split add: nat_diff_split simp add: add_mult_distrib)
   1.400 -
   1.401 -lemma nat_less_add_iff1:
   1.402 -     "j <= (i::nat) ==> (i*u + m < j*u + n) = ((i-j)*u + m < n)"
   1.403 -by (auto split add: nat_diff_split simp add: add_mult_distrib)
   1.404 -
   1.405 -lemma nat_less_add_iff2:
   1.406 -     "i <= (j::nat) ==> (i*u + m < j*u + n) = (m < (j-i)*u + n)"
   1.407 -by (auto split add: nat_diff_split simp add: add_mult_distrib)
   1.408 -
   1.409 -lemma nat_le_add_iff1:
   1.410 -     "j <= (i::nat) ==> (i*u + m <= j*u + n) = ((i-j)*u + m <= n)"
   1.411 -by (auto split add: nat_diff_split simp add: add_mult_distrib)
   1.412 -
   1.413 -lemma nat_le_add_iff2:
   1.414 -     "i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)"
   1.415 -by (auto split add: nat_diff_split simp add: add_mult_distrib)
   1.416 -
   1.417 -
   1.418 -subsubsection{*For @{text cancel_numeral_factors} *}
   1.419 -
   1.420 -lemma nat_mult_le_cancel1: "(0::nat) < k ==> (k*m <= k*n) = (m<=n)"
   1.421 -by auto
   1.422 -
   1.423 -lemma nat_mult_less_cancel1: "(0::nat) < k ==> (k*m < k*n) = (m<n)"
   1.424 -by auto
   1.425 -
   1.426 -lemma nat_mult_eq_cancel1: "(0::nat) < k ==> (k*m = k*n) = (m=n)"
   1.427 -by auto
   1.428 -
   1.429 -lemma nat_mult_div_cancel1: "(0::nat) < k ==> (k*m) div (k*n) = (m div n)"
   1.430 -by auto
   1.431 -
   1.432 -lemma nat_mult_dvd_cancel_disj[simp]:
   1.433 -  "(k*m) dvd (k*n) = (k=0 | m dvd (n::nat))"
   1.434 -by(auto simp: dvd_eq_mod_eq_0 mod_mult_distrib2[symmetric])
   1.435 -
   1.436 -lemma nat_mult_dvd_cancel1: "0 < k \<Longrightarrow> (k*m) dvd (k*n::nat) = (m dvd n)"
   1.437 -by(auto)
   1.438 -
   1.439 -
   1.440 -subsubsection{*For @{text cancel_factor} *}
   1.441 -
   1.442 -lemma nat_mult_le_cancel_disj: "(k*m <= k*n) = ((0::nat) < k --> m<=n)"
   1.443 -by auto
   1.444 -
   1.445 -lemma nat_mult_less_cancel_disj: "(k*m < k*n) = ((0::nat) < k & m<n)"
   1.446 -by auto
   1.447 -
   1.448 -lemma nat_mult_eq_cancel_disj: "(k*m = k*n) = (k = (0::nat) | m=n)"
   1.449 -by auto
   1.450 -
   1.451 -lemma nat_mult_div_cancel_disj[simp]:
   1.452 -     "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)"
   1.453 -by (simp add: nat_mult_div_cancel1)
   1.454 -
   1.455 -
   1.456 -use "Tools/numeral_simprocs.ML"
   1.457 -
   1.458 -use "Tools/nat_numeral_simprocs.ML"
   1.459 -
   1.460 -declaration {* 
   1.461 -  K (Lin_Arith.add_simps (@{thms neg_simps} @ [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}])
   1.462 -  #> Lin_Arith.add_simps (@{thms ring_distribs} @ [@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1},
   1.463 -     @{thm nat_0}, @{thm nat_1},
   1.464 -     @{thm add_nat_number_of}, @{thm diff_nat_number_of}, @{thm mult_nat_number_of},
   1.465 -     @{thm eq_nat_number_of}, @{thm less_nat_number_of}, @{thm le_number_of_eq_not_less},
   1.466 -     @{thm le_Suc_number_of}, @{thm le_number_of_Suc},
   1.467 -     @{thm less_Suc_number_of}, @{thm less_number_of_Suc},
   1.468 -     @{thm Suc_eq_number_of}, @{thm eq_number_of_Suc},
   1.469 -     @{thm mult_Suc}, @{thm mult_Suc_right},
   1.470 -     @{thm add_Suc}, @{thm add_Suc_right},
   1.471 -     @{thm eq_number_of_0}, @{thm eq_0_number_of}, @{thm less_0_number_of},
   1.472 -     @{thm of_int_number_of_eq}, @{thm of_nat_number_of_eq}, @{thm nat_number_of},
   1.473 -     @{thm if_True}, @{thm if_False}])
   1.474 -  #> Lin_Arith.add_simprocs (Numeral_Simprocs.assoc_fold_simproc
   1.475 -      :: Numeral_Simprocs.combine_numerals
   1.476 -      :: Numeral_Simprocs.cancel_numerals)
   1.477 -  #> Lin_Arith.add_simprocs (Nat_Numeral_Simprocs.combine_numerals :: Nat_Numeral_Simprocs.cancel_numerals))
   1.478 -*}
   1.479 -
   1.480  end