cleaned up and tuned
authorhaftmann
Sat Dec 02 16:50:53 2017 +0000 (7 months ago)
changeset 671167397a6df81d8
parent 67115 2977773a481c
child 67117 19f627407264
cleaned up and tuned
src/HOL/Int.thy
src/HOL/Num.thy
src/HOL/Tools/int_arith.ML
     1.1 --- a/src/HOL/Int.thy	Sat Dec 02 16:50:53 2017 +0000
     1.2 +++ b/src/HOL/Int.thy	Sat Dec 02 16:50:53 2017 +0000
     1.3 @@ -203,13 +203,6 @@
     1.4    then show ?rhs by simp
     1.5  qed
     1.6  
     1.7 -lemmas int_distrib =
     1.8 -  distrib_right [of z1 z2 w]
     1.9 -  distrib_left [of w z1 z2]
    1.10 -  left_diff_distrib [of z1 z2 w]
    1.11 -  right_diff_distrib [of w z1 z2]
    1.12 -  for z1 z2 w :: int
    1.13 -
    1.14  
    1.15  subsection \<open>Embedding of the Integers into any \<open>ring_1\<close>: \<open>of_int\<close>\<close>
    1.16  
    1.17 @@ -778,14 +771,6 @@
    1.18    "(\<And>n. P (int n)) \<Longrightarrow> (\<And>n. P (- (int (Suc n)))) \<Longrightarrow> P z"
    1.19    by (cases z) auto
    1.20  
    1.21 -lemma Let_numeral [simp]: "Let (numeral v) f = f (numeral v)"
    1.22 -  \<comment> \<open>Unfold all \<open>let\<close>s involving constants\<close>
    1.23 -  by (fact Let_numeral) \<comment> \<open>FIXME drop\<close>
    1.24 -
    1.25 -lemma Let_neg_numeral [simp]: "Let (- numeral v) f = f (- numeral v)"
    1.26 -  \<comment> \<open>Unfold all \<open>let\<close>s involving constants\<close>
    1.27 -  by (fact Let_neg_numeral) \<comment> \<open>FIXME drop\<close>
    1.28 -
    1.29  lemma sgn_mult_dvd_iff [simp]:
    1.30    "sgn r * l dvd k \<longleftrightarrow> l dvd k \<and> (r = 0 \<longrightarrow> k = 0)" for k l r :: int
    1.31    by (cases r rule: int_cases3) auto
    1.32 @@ -811,20 +796,6 @@
    1.33    then show ?thesis ..
    1.34  qed
    1.35  
    1.36 -text \<open>Unfold \<open>min\<close> and \<open>max\<close> on numerals.\<close>
    1.37 -
    1.38 -lemmas max_number_of [simp] =
    1.39 -  max_def [of "numeral u" "numeral v"]
    1.40 -  max_def [of "numeral u" "- numeral v"]
    1.41 -  max_def [of "- numeral u" "numeral v"]
    1.42 -  max_def [of "- numeral u" "- numeral v"] for u v
    1.43 -
    1.44 -lemmas min_number_of [simp] =
    1.45 -  min_def [of "numeral u" "numeral v"]
    1.46 -  min_def [of "numeral u" "- numeral v"]
    1.47 -  min_def [of "- numeral u" "numeral v"]
    1.48 -  min_def [of "- numeral u" "- numeral v"] for u v
    1.49 -
    1.50  
    1.51  subsubsection \<open>Binary comparisons\<close>
    1.52  
    1.53 @@ -857,8 +828,6 @@
    1.54  
    1.55  subsubsection \<open>Comparisons, for Ordered Rings\<close>
    1.56  
    1.57 -lemmas double_eq_0_iff = double_zero
    1.58 -
    1.59  lemma odd_nonzero: "1 + z + z \<noteq> 0"
    1.60    for z :: int
    1.61  proof (cases z)
    1.62 @@ -866,7 +835,7 @@
    1.63    have le: "0 \<le> z + z"
    1.64      by (simp add: nonneg add_increasing)
    1.65    then show ?thesis
    1.66 -    using  le_imp_0_less [OF le] by (auto simp: add.assoc)
    1.67 +    using le_imp_0_less [OF le] by (auto simp: ac_simps)
    1.68  next
    1.69    case (neg n)
    1.70    show ?thesis
    1.71 @@ -1017,7 +986,7 @@
    1.72      assume ?lhs
    1.73      with a have "of_int (z + z) = (of_int 0 :: 'a)" by simp
    1.74      then have "z + z = 0" by (simp only: of_int_eq_iff)
    1.75 -    then have "z = 0" by (simp only: double_eq_0_iff)
    1.76 +    then have "z = 0" by (simp only: double_zero)
    1.77      with a show ?rhs by simp
    1.78    qed
    1.79  qed
    1.80 @@ -1075,15 +1044,6 @@
    1.81    by (induct A rule: infinite_finite_induct) auto
    1.82  
    1.83  
    1.84 -text \<open>Legacy theorems\<close>
    1.85 -
    1.86 -lemmas int_sum = of_nat_sum [where 'a=int]
    1.87 -lemmas int_prod = of_nat_prod [where 'a=int]
    1.88 -lemmas zle_int = of_nat_le_iff [where 'a=int]
    1.89 -lemmas int_int_eq = of_nat_eq_iff [where 'a=int]
    1.90 -lemmas nonneg_eq_int = nonneg_int_cases
    1.91 -
    1.92 -
    1.93  subsection \<open>Setting up simplification procedures\<close>
    1.94  
    1.95  lemmas of_int_simps =
    1.96 @@ -1147,13 +1107,12 @@
    1.97  lemma one_less_nat_eq [simp]: "Suc 0 < nat z \<longleftrightarrow> 1 < z"
    1.98    using zless_nat_conj [of 1 z] by auto
    1.99  
   1.100 -text \<open>
   1.101 -  This simplifies expressions of the form @{term "int n = z"} where
   1.102 -  \<open>z\<close> is an integer literal.
   1.103 -\<close>
   1.104 -lemmas int_eq_iff_numeral [simp] = int_eq_iff [of _ "numeral v"] for v
   1.105 +lemma int_eq_iff_numeral [simp]:
   1.106 +  "int m = numeral v \<longleftrightarrow> m = numeral v"
   1.107 +  by (simp add: int_eq_iff)
   1.108  
   1.109 -lemma nat_abs_int_diff: "nat \<bar>int a - int b\<bar> = (if a \<le> b then b - a else a - b)"
   1.110 +lemma nat_abs_int_diff:
   1.111 +  "nat \<bar>int a - int b\<bar> = (if a \<le> b then b - a else a - b)"
   1.112    by auto
   1.113  
   1.114  lemma nat_int_add: "nat (int a + int b) = a + b"
   1.115 @@ -1377,36 +1336,33 @@
   1.116  
   1.117  subsection \<open>Intermediate value theorems\<close>
   1.118  
   1.119 -lemma int_val_lemma: "(\<forall>i<n. \<bar>f (i + 1) - f i\<bar> \<le> 1) \<longrightarrow> f 0 \<le> k \<longrightarrow> k \<le> f n \<longrightarrow> (\<exists>i \<le> n. f i = k)"
   1.120 +lemma nat_intermed_int_val:
   1.121 +  "\<exists>i. m \<le> i \<and> i \<le> n \<and> f i = k"
   1.122 +  if "\<forall>i. m \<le> i \<and> i < n \<longrightarrow> \<bar>f (Suc i) - f i\<bar> \<le> 1"
   1.123 +    "m \<le> n" "f m \<le> k" "k \<le> f n"
   1.124 +  for m n :: nat and k :: int
   1.125 +proof -
   1.126 +  have "(\<forall>i<n. \<bar>f (Suc i) - f i\<bar> \<le> 1) \<Longrightarrow> f 0 \<le> k \<Longrightarrow> k \<le> f n
   1.127 +    \<Longrightarrow> (\<exists>i \<le> n. f i = k)"
   1.128 +  for n :: nat and f
   1.129 +    apply (induct n)
   1.130 +     apply auto
   1.131 +    apply (erule_tac x = n in allE)
   1.132 +    apply (case_tac "k = f (Suc n)")
   1.133 +     apply (auto simp add: abs_if split: if_split_asm intro: le_SucI)
   1.134 +    done
   1.135 +  from this [of "n - m" "f \<circ> plus m"] that show ?thesis
   1.136 +    apply auto
   1.137 +    apply (rule_tac x = "m + i" in exI)
   1.138 +    apply auto
   1.139 +    done
   1.140 +qed
   1.141 +
   1.142 +lemma nat0_intermed_int_val:
   1.143 +  "\<exists>i\<le>n. f i = k"
   1.144 +  if "\<forall>i<n. \<bar>f (i + 1) - f i\<bar> \<le> 1" "f 0 \<le> k" "k \<le> f n"
   1.145    for n :: nat and k :: int
   1.146 -  unfolding One_nat_def
   1.147 -  apply (induct n)
   1.148 -   apply simp
   1.149 -  apply (intro strip)
   1.150 -  apply (erule impE)
   1.151 -   apply simp
   1.152 -  apply (erule_tac x = n in allE)
   1.153 -  apply simp
   1.154 -  apply (case_tac "k = f (Suc n)")
   1.155 -   apply force
   1.156 -  apply (erule impE)
   1.157 -   apply (simp add: abs_if split: if_split_asm)
   1.158 -  apply (blast intro: le_SucI)
   1.159 -  done
   1.160 -
   1.161 -lemmas nat0_intermed_int_val = int_val_lemma [rule_format (no_asm)]
   1.162 -
   1.163 -lemma nat_intermed_int_val:
   1.164 -  "\<forall>i. m \<le> i \<and> i < n \<longrightarrow> \<bar>f (i + 1) - f i\<bar> \<le> 1 \<Longrightarrow> m < n \<Longrightarrow>
   1.165 -    f m \<le> k \<Longrightarrow> k \<le> f n \<Longrightarrow> \<exists>i. m \<le> i \<and> i \<le> n \<and> f i = k"
   1.166 -    for f :: "nat \<Rightarrow> int" and k :: int
   1.167 -  apply (cut_tac n = "n-m" and f = "\<lambda>i. f (i + m)" and k = k in int_val_lemma)
   1.168 -  unfolding One_nat_def
   1.169 -  apply simp
   1.170 -  apply (erule exE)
   1.171 -  apply (rule_tac x = "i+m" in exI)
   1.172 -  apply arith
   1.173 -  done
   1.174 +  using nat_intermed_int_val [of 0 n f k] that by auto
   1.175  
   1.176  
   1.177  subsection \<open>Products and 1, by T. M. Rasmussen\<close>
   1.178 @@ -1465,129 +1421,6 @@
   1.179  qed
   1.180  
   1.181  
   1.182 -subsection \<open>Further theorems on numerals\<close>
   1.183 -
   1.184 -subsubsection \<open>Special Simplification for Constants\<close>
   1.185 -
   1.186 -text \<open>These distributive laws move literals inside sums and differences.\<close>
   1.187 -
   1.188 -lemmas distrib_right_numeral [simp] = distrib_right [of _ _ "numeral v"] for v
   1.189 -lemmas distrib_left_numeral [simp] = distrib_left [of "numeral v"] for v
   1.190 -lemmas left_diff_distrib_numeral [simp] = left_diff_distrib [of _ _ "numeral v"] for v
   1.191 -lemmas right_diff_distrib_numeral [simp] = right_diff_distrib [of "numeral v"] for v
   1.192 -
   1.193 -text \<open>These are actually for fields, like real: but where else to put them?\<close>
   1.194 -
   1.195 -lemmas zero_less_divide_iff_numeral [simp, no_atp] = zero_less_divide_iff [of "numeral w"] for w
   1.196 -lemmas divide_less_0_iff_numeral [simp, no_atp] = divide_less_0_iff [of "numeral w"] for w
   1.197 -lemmas zero_le_divide_iff_numeral [simp, no_atp] = zero_le_divide_iff [of "numeral w"] for w
   1.198 -lemmas divide_le_0_iff_numeral [simp, no_atp] = divide_le_0_iff [of "numeral w"] for w
   1.199 -
   1.200 -
   1.201 -text \<open>Replaces \<open>inverse #nn\<close> by \<open>1/#nn\<close>.  It looks
   1.202 -  strange, but then other simprocs simplify the quotient.\<close>
   1.203 -
   1.204 -lemmas inverse_eq_divide_numeral [simp] =
   1.205 -  inverse_eq_divide [of "numeral w"] for w
   1.206 -
   1.207 -lemmas inverse_eq_divide_neg_numeral [simp] =
   1.208 -  inverse_eq_divide [of "- numeral w"] for w
   1.209 -
   1.210 -text \<open>These laws simplify inequalities, moving unary minus from a term
   1.211 -  into the literal.\<close>
   1.212 -
   1.213 -lemmas equation_minus_iff_numeral [no_atp] =
   1.214 -  equation_minus_iff [of "numeral v"] for v
   1.215 -
   1.216 -lemmas minus_equation_iff_numeral [no_atp] =
   1.217 -  minus_equation_iff [of _ "numeral v"] for v
   1.218 -
   1.219 -lemmas le_minus_iff_numeral [no_atp] =
   1.220 -  le_minus_iff [of "numeral v"] for v
   1.221 -
   1.222 -lemmas minus_le_iff_numeral [no_atp] =
   1.223 -  minus_le_iff [of _ "numeral v"] for v
   1.224 -
   1.225 -lemmas less_minus_iff_numeral [no_atp] =
   1.226 -  less_minus_iff [of "numeral v"] for v
   1.227 -
   1.228 -lemmas minus_less_iff_numeral [no_atp] =
   1.229 -  minus_less_iff [of _ "numeral v"] for v
   1.230 -
   1.231 -(* FIXME maybe simproc *)
   1.232 -
   1.233 -
   1.234 -text \<open>Cancellation of constant factors in comparisons (\<open><\<close> and \<open>\<le>\<close>)\<close>
   1.235 -
   1.236 -lemmas mult_less_cancel_left_numeral [simp, no_atp] = mult_less_cancel_left [of "numeral v"] for v
   1.237 -lemmas mult_less_cancel_right_numeral [simp, no_atp] = mult_less_cancel_right [of _ "numeral v"] for v
   1.238 -lemmas mult_le_cancel_left_numeral [simp, no_atp] = mult_le_cancel_left [of "numeral v"] for v
   1.239 -lemmas mult_le_cancel_right_numeral [simp, no_atp] = mult_le_cancel_right [of _ "numeral v"] for v
   1.240 -
   1.241 -
   1.242 -text \<open>Multiplying out constant divisors in comparisons (\<open><\<close>, \<open>\<le>\<close> and \<open>=\<close>)\<close>
   1.243 -
   1.244 -named_theorems divide_const_simps "simplification rules to simplify comparisons involving constant divisors"
   1.245 -
   1.246 -lemmas le_divide_eq_numeral1 [simp,divide_const_simps] =
   1.247 -  pos_le_divide_eq [of "numeral w", OF zero_less_numeral]
   1.248 -  neg_le_divide_eq [of "- numeral w", OF neg_numeral_less_zero] for w
   1.249 -
   1.250 -lemmas divide_le_eq_numeral1 [simp,divide_const_simps] =
   1.251 -  pos_divide_le_eq [of "numeral w", OF zero_less_numeral]
   1.252 -  neg_divide_le_eq [of "- numeral w", OF neg_numeral_less_zero] for w
   1.253 -
   1.254 -lemmas less_divide_eq_numeral1 [simp,divide_const_simps] =
   1.255 -  pos_less_divide_eq [of "numeral w", OF zero_less_numeral]
   1.256 -  neg_less_divide_eq [of "- numeral w", OF neg_numeral_less_zero] for w
   1.257 -
   1.258 -lemmas divide_less_eq_numeral1 [simp,divide_const_simps] =
   1.259 -  pos_divide_less_eq [of "numeral w", OF zero_less_numeral]
   1.260 -  neg_divide_less_eq [of "- numeral w", OF neg_numeral_less_zero] for w
   1.261 -
   1.262 -lemmas eq_divide_eq_numeral1 [simp,divide_const_simps] =
   1.263 -  eq_divide_eq [of _ _ "numeral w"]
   1.264 -  eq_divide_eq [of _ _ "- numeral w"] for w
   1.265 -
   1.266 -lemmas divide_eq_eq_numeral1 [simp,divide_const_simps] =
   1.267 -  divide_eq_eq [of _ "numeral w"]
   1.268 -  divide_eq_eq [of _ "- numeral w"] for w
   1.269 -
   1.270 -
   1.271 -subsubsection \<open>Optional Simplification Rules Involving Constants\<close>
   1.272 -
   1.273 -text \<open>Simplify quotients that are compared with a literal constant.\<close>
   1.274 -
   1.275 -lemmas le_divide_eq_numeral [divide_const_simps] =
   1.276 -  le_divide_eq [of "numeral w"]
   1.277 -  le_divide_eq [of "- numeral w"] for w
   1.278 -
   1.279 -lemmas divide_le_eq_numeral [divide_const_simps] =
   1.280 -  divide_le_eq [of _ _ "numeral w"]
   1.281 -  divide_le_eq [of _ _ "- numeral w"] for w
   1.282 -
   1.283 -lemmas less_divide_eq_numeral [divide_const_simps] =
   1.284 -  less_divide_eq [of "numeral w"]
   1.285 -  less_divide_eq [of "- numeral w"] for w
   1.286 -
   1.287 -lemmas divide_less_eq_numeral [divide_const_simps] =
   1.288 -  divide_less_eq [of _ _ "numeral w"]
   1.289 -  divide_less_eq [of _ _ "- numeral w"] for w
   1.290 -
   1.291 -lemmas eq_divide_eq_numeral [divide_const_simps] =
   1.292 -  eq_divide_eq [of "numeral w"]
   1.293 -  eq_divide_eq [of "- numeral w"] for w
   1.294 -
   1.295 -lemmas divide_eq_eq_numeral [divide_const_simps] =
   1.296 -  divide_eq_eq [of _ _ "numeral w"]
   1.297 -  divide_eq_eq [of _ _ "- numeral w"] for w
   1.298 -
   1.299 -
   1.300 -text \<open>Not good as automatic simprules because they cause case splits.\<close>
   1.301 -lemmas [divide_const_simps] =
   1.302 -  le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1
   1.303 -
   1.304 -
   1.305  subsection \<open>The divides relation\<close>
   1.306  
   1.307  lemma zdvd_antisym_nonneg: "0 \<le> m \<Longrightarrow> 0 \<le> n \<Longrightarrow> m dvd n \<Longrightarrow> n dvd m \<Longrightarrow> m = n"
   1.308 @@ -1734,7 +1567,7 @@
   1.309    by (auto simp add: dvd_int_iff)
   1.310  
   1.311  lemma eq_nat_nat_iff: "0 \<le> z \<Longrightarrow> 0 \<le> z' \<Longrightarrow> nat z = nat z' \<longleftrightarrow> z = z'"
   1.312 -  by (auto elim!: nonneg_eq_int)
   1.313 +  by (auto elim: nonneg_int_cases)
   1.314  
   1.315  lemma nat_power_eq: "0 \<le> z \<Longrightarrow> nat (z ^ n) = nat z ^ n"
   1.316    by (induct n) (simp_all add: nat_mult_distrib)
   1.317 @@ -1977,4 +1810,22 @@
   1.318  lifting_update int.lifting
   1.319  lifting_forget int.lifting
   1.320  
   1.321 +
   1.322 +subsection \<open>Duplicates\<close>
   1.323 +
   1.324 +lemmas int_sum = of_nat_sum [where 'a=int]
   1.325 +lemmas int_prod = of_nat_prod [where 'a=int]
   1.326 +lemmas zle_int = of_nat_le_iff [where 'a=int]
   1.327 +lemmas int_int_eq = of_nat_eq_iff [where 'a=int]
   1.328 +lemmas nonneg_eq_int = nonneg_int_cases
   1.329 +lemmas double_eq_0_iff = double_zero
   1.330 +
   1.331 +lemmas int_distrib =
   1.332 +  distrib_right [of z1 z2 w]
   1.333 +  distrib_left [of w z1 z2]
   1.334 +  left_diff_distrib [of z1 z2 w]
   1.335 +  right_diff_distrib [of w z1 z2]
   1.336 +  for z1 z2 w :: int
   1.337 +
   1.338  end
   1.339 +
     2.1 --- a/src/HOL/Num.thy	Sat Dec 02 16:50:53 2017 +0000
     2.2 +++ b/src/HOL/Num.thy	Sat Dec 02 16:50:53 2017 +0000
     2.3 @@ -695,6 +695,20 @@
     2.4  
     2.5  end
     2.6  
     2.7 +text \<open>Unfold \<open>min\<close> and \<open>max\<close> on numerals.\<close>
     2.8 +
     2.9 +lemmas max_number_of [simp] =
    2.10 +  max_def [of "numeral u" "numeral v"]
    2.11 +  max_def [of "numeral u" "- numeral v"]
    2.12 +  max_def [of "- numeral u" "numeral v"]
    2.13 +  max_def [of "- numeral u" "- numeral v"] for u v
    2.14 +
    2.15 +lemmas min_number_of [simp] =
    2.16 +  min_def [of "numeral u" "numeral v"]
    2.17 +  min_def [of "numeral u" "- numeral v"]
    2.18 +  min_def [of "- numeral u" "numeral v"]
    2.19 +  min_def [of "- numeral u" "- numeral v"] for u v
    2.20 +
    2.21  
    2.22  subsubsection \<open>Multiplication and negation: class \<open>ring_1\<close>\<close>
    2.23  
    2.24 @@ -1117,6 +1131,125 @@
    2.25  declare (in semiring_numeral) numeral_times_numeral [simp]
    2.26  declare (in ring_1) mult_neg_numeral_simps [simp]
    2.27  
    2.28 +
    2.29 +subsubsection \<open>Special Simplification for Constants\<close>
    2.30 +
    2.31 +text \<open>These distributive laws move literals inside sums and differences.\<close>
    2.32 +
    2.33 +lemmas distrib_right_numeral [simp] = distrib_right [of _ _ "numeral v"] for v
    2.34 +lemmas distrib_left_numeral [simp] = distrib_left [of "numeral v"] for v
    2.35 +lemmas left_diff_distrib_numeral [simp] = left_diff_distrib [of _ _ "numeral v"] for v
    2.36 +lemmas right_diff_distrib_numeral [simp] = right_diff_distrib [of "numeral v"] for v
    2.37 +
    2.38 +text \<open>These are actually for fields, like real\<close>
    2.39 +
    2.40 +lemmas zero_less_divide_iff_numeral [simp, no_atp] = zero_less_divide_iff [of "numeral w"] for w
    2.41 +lemmas divide_less_0_iff_numeral [simp, no_atp] = divide_less_0_iff [of "numeral w"] for w
    2.42 +lemmas zero_le_divide_iff_numeral [simp, no_atp] = zero_le_divide_iff [of "numeral w"] for w
    2.43 +lemmas divide_le_0_iff_numeral [simp, no_atp] = divide_le_0_iff [of "numeral w"] for w
    2.44 +
    2.45 +text \<open>Replaces \<open>inverse #nn\<close> by \<open>1/#nn\<close>.  It looks
    2.46 +  strange, but then other simprocs simplify the quotient.\<close>
    2.47 +
    2.48 +lemmas inverse_eq_divide_numeral [simp] =
    2.49 +  inverse_eq_divide [of "numeral w"] for w
    2.50 +
    2.51 +lemmas inverse_eq_divide_neg_numeral [simp] =
    2.52 +  inverse_eq_divide [of "- numeral w"] for w
    2.53 +
    2.54 +text \<open>These laws simplify inequalities, moving unary minus from a term
    2.55 +  into the literal.\<close>
    2.56 +
    2.57 +lemmas equation_minus_iff_numeral [no_atp] =
    2.58 +  equation_minus_iff [of "numeral v"] for v
    2.59 +
    2.60 +lemmas minus_equation_iff_numeral [no_atp] =
    2.61 +  minus_equation_iff [of _ "numeral v"] for v
    2.62 +
    2.63 +lemmas le_minus_iff_numeral [no_atp] =
    2.64 +  le_minus_iff [of "numeral v"] for v
    2.65 +
    2.66 +lemmas minus_le_iff_numeral [no_atp] =
    2.67 +  minus_le_iff [of _ "numeral v"] for v
    2.68 +
    2.69 +lemmas less_minus_iff_numeral [no_atp] =
    2.70 +  less_minus_iff [of "numeral v"] for v
    2.71 +
    2.72 +lemmas minus_less_iff_numeral [no_atp] =
    2.73 +  minus_less_iff [of _ "numeral v"] for v
    2.74 +
    2.75 +(* FIXME maybe simproc *)
    2.76 +
    2.77 +text \<open>Cancellation of constant factors in comparisons (\<open><\<close> and \<open>\<le>\<close>)\<close>
    2.78 +
    2.79 +lemmas mult_less_cancel_left_numeral [simp, no_atp] = mult_less_cancel_left [of "numeral v"] for v
    2.80 +lemmas mult_less_cancel_right_numeral [simp, no_atp] = mult_less_cancel_right [of _ "numeral v"] for v
    2.81 +lemmas mult_le_cancel_left_numeral [simp, no_atp] = mult_le_cancel_left [of "numeral v"] for v
    2.82 +lemmas mult_le_cancel_right_numeral [simp, no_atp] = mult_le_cancel_right [of _ "numeral v"] for v
    2.83 +
    2.84 +text \<open>Multiplying out constant divisors in comparisons (\<open><\<close>, \<open>\<le>\<close> and \<open>=\<close>)\<close>
    2.85 +
    2.86 +named_theorems divide_const_simps "simplification rules to simplify comparisons involving constant divisors"
    2.87 +
    2.88 +lemmas le_divide_eq_numeral1 [simp,divide_const_simps] =
    2.89 +  pos_le_divide_eq [of "numeral w", OF zero_less_numeral]
    2.90 +  neg_le_divide_eq [of "- numeral w", OF neg_numeral_less_zero] for w
    2.91 +
    2.92 +lemmas divide_le_eq_numeral1 [simp,divide_const_simps] =
    2.93 +  pos_divide_le_eq [of "numeral w", OF zero_less_numeral]
    2.94 +  neg_divide_le_eq [of "- numeral w", OF neg_numeral_less_zero] for w
    2.95 +
    2.96 +lemmas less_divide_eq_numeral1 [simp,divide_const_simps] =
    2.97 +  pos_less_divide_eq [of "numeral w", OF zero_less_numeral]
    2.98 +  neg_less_divide_eq [of "- numeral w", OF neg_numeral_less_zero] for w
    2.99 +
   2.100 +lemmas divide_less_eq_numeral1 [simp,divide_const_simps] =
   2.101 +  pos_divide_less_eq [of "numeral w", OF zero_less_numeral]
   2.102 +  neg_divide_less_eq [of "- numeral w", OF neg_numeral_less_zero] for w
   2.103 +
   2.104 +lemmas eq_divide_eq_numeral1 [simp,divide_const_simps] =
   2.105 +  eq_divide_eq [of _ _ "numeral w"]
   2.106 +  eq_divide_eq [of _ _ "- numeral w"] for w
   2.107 +
   2.108 +lemmas divide_eq_eq_numeral1 [simp,divide_const_simps] =
   2.109 +  divide_eq_eq [of _ "numeral w"]
   2.110 +  divide_eq_eq [of _ "- numeral w"] for w
   2.111 +
   2.112 +
   2.113 +subsubsection \<open>Optional Simplification Rules Involving Constants\<close>
   2.114 +
   2.115 +text \<open>Simplify quotients that are compared with a literal constant.\<close>
   2.116 +
   2.117 +lemmas le_divide_eq_numeral [divide_const_simps] =
   2.118 +  le_divide_eq [of "numeral w"]
   2.119 +  le_divide_eq [of "- numeral w"] for w
   2.120 +
   2.121 +lemmas divide_le_eq_numeral [divide_const_simps] =
   2.122 +  divide_le_eq [of _ _ "numeral w"]
   2.123 +  divide_le_eq [of _ _ "- numeral w"] for w
   2.124 +
   2.125 +lemmas less_divide_eq_numeral [divide_const_simps] =
   2.126 +  less_divide_eq [of "numeral w"]
   2.127 +  less_divide_eq [of "- numeral w"] for w
   2.128 +
   2.129 +lemmas divide_less_eq_numeral [divide_const_simps] =
   2.130 +  divide_less_eq [of _ _ "numeral w"]
   2.131 +  divide_less_eq [of _ _ "- numeral w"] for w
   2.132 +
   2.133 +lemmas eq_divide_eq_numeral [divide_const_simps] =
   2.134 +  eq_divide_eq [of "numeral w"]
   2.135 +  eq_divide_eq [of "- numeral w"] for w
   2.136 +
   2.137 +lemmas divide_eq_eq_numeral [divide_const_simps] =
   2.138 +  divide_eq_eq [of _ _ "numeral w"]
   2.139 +  divide_eq_eq [of _ _ "- numeral w"] for w
   2.140 +
   2.141 +text \<open>Not good as automatic simprules because they cause case splits.\<close>
   2.142 +
   2.143 +lemmas [divide_const_simps] =
   2.144 +  le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1
   2.145 +
   2.146 +
   2.147  subsection \<open>Setting up simprocs\<close>
   2.148  
   2.149  lemma mult_numeral_1: "Numeral1 * a = a"
     3.1 --- a/src/HOL/Tools/int_arith.ML	Sat Dec 02 16:50:53 2017 +0000
     3.2 +++ b/src/HOL/Tools/int_arith.ML	Sat Dec 02 16:50:53 2017 +0000
     3.3 @@ -78,7 +78,7 @@
     3.4    else Numeral.mk_cnumber (Thm.ctyp_of ctxt T) n;
     3.5  
     3.6  val setup =
     3.7 -  Lin_Arith.add_inj_thms [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
     3.8 +  Lin_Arith.add_inj_thms [@{thm of_nat_le_iff} RS iffD2, @{thm of_nat_eq_iff} RS iffD2]
     3.9    #> Lin_Arith.add_lessD @{thm zless_imp_add1_zle}
    3.10    #> Lin_Arith.add_simps @{thms of_nat_simps of_int_simps}
    3.11    #> Lin_Arith.add_simps