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
```