dropped theory Arith_Tools
authorhaftmann
Sun Mar 22 20:46:11 2009 +0100 (2009-03-22)
changeset 30654254478a8dd05
parent 30653 fbd548c4bb6a
child 30655 88131f2807b6
dropped theory Arith_Tools
src/HOL/Arith_Tools.thy
src/HOL/Groebner_Basis.thy
src/HOL/IsaMakefile
src/HOL/Library/Topology_Euclidean_Space.thy
     1.1 --- a/src/HOL/Arith_Tools.thy	Sun Mar 22 20:46:11 2009 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,388 +0,0 @@
     1.4 -(*  Title:      HOL/Arith_Tools.thy
     1.5 -    ID:         $Id$
     1.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Author:     Amine Chaieb, TU Muenchen
     1.8 -*)
     1.9 -
    1.10 -header {* Setup of arithmetic tools *}
    1.11 -
    1.12 -theory Arith_Tools
    1.13 -imports NatBin
    1.14 -uses
    1.15 -  "~~/src/Provers/Arith/cancel_numeral_factor.ML"
    1.16 -  "~~/src/Provers/Arith/extract_common_term.ML"
    1.17 -  "Tools/int_factor_simprocs.ML"
    1.18 -  "Tools/nat_simprocs.ML"
    1.19 -  "Tools/Qelim/qelim.ML"
    1.20 -begin
    1.21 -
    1.22 -subsection {* Simprocs for the Naturals *}
    1.23 -
    1.24 -declaration {* K nat_simprocs_setup *}
    1.25 -
    1.26 -subsubsection{*For simplifying @{term "Suc m - K"} and  @{term "K - Suc m"}*}
    1.27 -
    1.28 -text{*Where K above is a literal*}
    1.29 -
    1.30 -lemma Suc_diff_eq_diff_pred: "Numeral0 < n ==> Suc m - n = m - (n - Numeral1)"
    1.31 -by (simp add: numeral_0_eq_0 numeral_1_eq_1 split add: nat_diff_split)
    1.32 -
    1.33 -text {*Now just instantiating @{text n} to @{text "number_of v"} does
    1.34 -  the right simplification, but with some redundant inequality
    1.35 -  tests.*}
    1.36 -lemma neg_number_of_pred_iff_0:
    1.37 -  "neg (number_of (Int.pred v)::int) = (number_of v = (0::nat))"
    1.38 -apply (subgoal_tac "neg (number_of (Int.pred v)) = (number_of v < Suc 0) ")
    1.39 -apply (simp only: less_Suc_eq_le le_0_eq)
    1.40 -apply (subst less_number_of_Suc, simp)
    1.41 -done
    1.42 -
    1.43 -text{*No longer required as a simprule because of the @{text inverse_fold}
    1.44 -   simproc*}
    1.45 -lemma Suc_diff_number_of:
    1.46 -     "Int.Pls < v ==>
    1.47 -      Suc m - (number_of v) = m - (number_of (Int.pred v))"
    1.48 -apply (subst Suc_diff_eq_diff_pred)
    1.49 -apply simp
    1.50 -apply (simp del: nat_numeral_1_eq_1)
    1.51 -apply (auto simp only: diff_nat_number_of less_0_number_of [symmetric]
    1.52 -                        neg_number_of_pred_iff_0)
    1.53 -done
    1.54 -
    1.55 -lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n"
    1.56 -by (simp add: numerals split add: nat_diff_split)
    1.57 -
    1.58 -
    1.59 -subsubsection{*For @{term nat_case} and @{term nat_rec}*}
    1.60 -
    1.61 -lemma nat_case_number_of [simp]:
    1.62 -     "nat_case a f (number_of v) =
    1.63 -        (let pv = number_of (Int.pred v) in
    1.64 -         if neg pv then a else f (nat pv))"
    1.65 -by (simp split add: nat.split add: Let_def neg_number_of_pred_iff_0)
    1.66 -
    1.67 -lemma nat_case_add_eq_if [simp]:
    1.68 -     "nat_case a f ((number_of v) + n) =
    1.69 -       (let pv = number_of (Int.pred v) in
    1.70 -         if neg pv then nat_case a f n else f (nat pv + n))"
    1.71 -apply (subst add_eq_if)
    1.72 -apply (simp split add: nat.split
    1.73 -            del: nat_numeral_1_eq_1
    1.74 -            add: nat_numeral_1_eq_1 [symmetric]
    1.75 -                 numeral_1_eq_Suc_0 [symmetric]
    1.76 -                 neg_number_of_pred_iff_0)
    1.77 -done
    1.78 -
    1.79 -lemma nat_rec_number_of [simp]:
    1.80 -     "nat_rec a f (number_of v) =
    1.81 -        (let pv = number_of (Int.pred v) in
    1.82 -         if neg pv then a else f (nat pv) (nat_rec a f (nat pv)))"
    1.83 -apply (case_tac " (number_of v) ::nat")
    1.84 -apply (simp_all (no_asm_simp) add: Let_def neg_number_of_pred_iff_0)
    1.85 -apply (simp split add: split_if_asm)
    1.86 -done
    1.87 -
    1.88 -lemma nat_rec_add_eq_if [simp]:
    1.89 -     "nat_rec a f (number_of v + n) =
    1.90 -        (let pv = number_of (Int.pred v) in
    1.91 -         if neg pv then nat_rec a f n
    1.92 -                   else f (nat pv + n) (nat_rec a f (nat pv + n)))"
    1.93 -apply (subst add_eq_if)
    1.94 -apply (simp split add: nat.split
    1.95 -            del: nat_numeral_1_eq_1
    1.96 -            add: nat_numeral_1_eq_1 [symmetric]
    1.97 -                 numeral_1_eq_Suc_0 [symmetric]
    1.98 -                 neg_number_of_pred_iff_0)
    1.99 -done
   1.100 -
   1.101 -
   1.102 -subsubsection{*Various Other Lemmas*}
   1.103 -
   1.104 -text {*Evens and Odds, for Mutilated Chess Board*}
   1.105 -
   1.106 -text{*Lemmas for specialist use, NOT as default simprules*}
   1.107 -lemma nat_mult_2: "2 * z = (z+z::nat)"
   1.108 -proof -
   1.109 -  have "2*z = (1 + 1)*z" by simp
   1.110 -  also have "... = z+z" by (simp add: left_distrib)
   1.111 -  finally show ?thesis .
   1.112 -qed
   1.113 -
   1.114 -lemma nat_mult_2_right: "z * 2 = (z+z::nat)"
   1.115 -by (subst mult_commute, rule nat_mult_2)
   1.116 -
   1.117 -text{*Case analysis on @{term "n<2"}*}
   1.118 -lemma less_2_cases: "(n::nat) < 2 ==> n = 0 | n = Suc 0"
   1.119 -by arith
   1.120 -
   1.121 -lemma div2_Suc_Suc [simp]: "Suc(Suc m) div 2 = Suc (m div 2)"
   1.122 -by arith
   1.123 -
   1.124 -lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)"
   1.125 -by (simp add: nat_mult_2 [symmetric])
   1.126 -
   1.127 -lemma mod2_Suc_Suc [simp]: "Suc(Suc(m)) mod 2 = m mod 2"
   1.128 -apply (subgoal_tac "m mod 2 < 2")
   1.129 -apply (erule less_2_cases [THEN disjE])
   1.130 -apply (simp_all (no_asm_simp) add: Let_def mod_Suc nat_1)
   1.131 -done
   1.132 -
   1.133 -lemma mod2_gr_0 [simp]: "!!m::nat. (0 < m mod 2) = (m mod 2 = 1)"
   1.134 -apply (subgoal_tac "m mod 2 < 2")
   1.135 -apply (force simp del: mod_less_divisor, simp)
   1.136 -done
   1.137 -
   1.138 -text{*Removal of Small Numerals: 0, 1 and (in additive positions) 2*}
   1.139 -
   1.140 -lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)"
   1.141 -by simp
   1.142 -
   1.143 -lemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)"
   1.144 -by simp
   1.145 -
   1.146 -text{*Can be used to eliminate long strings of Sucs, but not by default*}
   1.147 -lemma Suc3_eq_add_3: "Suc (Suc (Suc n)) = 3 + n"
   1.148 -by simp
   1.149 -
   1.150 -
   1.151 -text{*These lemmas collapse some needless occurrences of Suc:
   1.152 -    at least three Sucs, since two and fewer are rewritten back to Suc again!
   1.153 -    We already have some rules to simplify operands smaller than 3.*}
   1.154 -
   1.155 -lemma div_Suc_eq_div_add3 [simp]: "m div (Suc (Suc (Suc n))) = m div (3+n)"
   1.156 -by (simp add: Suc3_eq_add_3)
   1.157 -
   1.158 -lemma mod_Suc_eq_mod_add3 [simp]: "m mod (Suc (Suc (Suc n))) = m mod (3+n)"
   1.159 -by (simp add: Suc3_eq_add_3)
   1.160 -
   1.161 -lemma Suc_div_eq_add3_div: "(Suc (Suc (Suc m))) div n = (3+m) div n"
   1.162 -by (simp add: Suc3_eq_add_3)
   1.163 -
   1.164 -lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n"
   1.165 -by (simp add: Suc3_eq_add_3)
   1.166 -
   1.167 -lemmas Suc_div_eq_add3_div_number_of =
   1.168 -    Suc_div_eq_add3_div [of _ "number_of v", standard]
   1.169 -declare Suc_div_eq_add3_div_number_of [simp]
   1.170 -
   1.171 -lemmas Suc_mod_eq_add3_mod_number_of =
   1.172 -    Suc_mod_eq_add3_mod [of _ "number_of v", standard]
   1.173 -declare Suc_mod_eq_add3_mod_number_of [simp]
   1.174 -
   1.175 -
   1.176 -subsubsection{*Special Simplification for Constants*}
   1.177 -
   1.178 -text{*These belong here, late in the development of HOL, to prevent their
   1.179 -interfering with proofs of abstract properties of instances of the function
   1.180 -@{term number_of}*}
   1.181 -
   1.182 -text{*These distributive laws move literals inside sums and differences.*}
   1.183 -lemmas left_distrib_number_of = left_distrib [of _ _ "number_of v", standard]
   1.184 -declare left_distrib_number_of [simp]
   1.185 -
   1.186 -lemmas right_distrib_number_of = right_distrib [of "number_of v", standard]
   1.187 -declare right_distrib_number_of [simp]
   1.188 -
   1.189 -
   1.190 -lemmas left_diff_distrib_number_of =
   1.191 -    left_diff_distrib [of _ _ "number_of v", standard]
   1.192 -declare left_diff_distrib_number_of [simp]
   1.193 -
   1.194 -lemmas right_diff_distrib_number_of =
   1.195 -    right_diff_distrib [of "number_of v", standard]
   1.196 -declare right_diff_distrib_number_of [simp]
   1.197 -
   1.198 -
   1.199 -text{*These are actually for fields, like real: but where else to put them?*}
   1.200 -lemmas zero_less_divide_iff_number_of =
   1.201 -    zero_less_divide_iff [of "number_of w", standard]
   1.202 -declare zero_less_divide_iff_number_of [simp,noatp]
   1.203 -
   1.204 -lemmas divide_less_0_iff_number_of =
   1.205 -    divide_less_0_iff [of "number_of w", standard]
   1.206 -declare divide_less_0_iff_number_of [simp,noatp]
   1.207 -
   1.208 -lemmas zero_le_divide_iff_number_of =
   1.209 -    zero_le_divide_iff [of "number_of w", standard]
   1.210 -declare zero_le_divide_iff_number_of [simp,noatp]
   1.211 -
   1.212 -lemmas divide_le_0_iff_number_of =
   1.213 -    divide_le_0_iff [of "number_of w", standard]
   1.214 -declare divide_le_0_iff_number_of [simp,noatp]
   1.215 -
   1.216 -
   1.217 -(****
   1.218 -IF times_divide_eq_right and times_divide_eq_left are removed as simprules,
   1.219 -then these special-case declarations may be useful.
   1.220 -
   1.221 -text{*These simprules move numerals into numerators and denominators.*}
   1.222 -lemma times_recip_eq_right [simp]: "a * (1/c) = a / (c::'a::field)"
   1.223 -by (simp add: times_divide_eq)
   1.224 -
   1.225 -lemma times_recip_eq_left [simp]: "(1/c) * a = a / (c::'a::field)"
   1.226 -by (simp add: times_divide_eq)
   1.227 -
   1.228 -lemmas times_divide_eq_right_number_of =
   1.229 -    times_divide_eq_right [of "number_of w", standard]
   1.230 -declare times_divide_eq_right_number_of [simp]
   1.231 -
   1.232 -lemmas times_divide_eq_right_number_of =
   1.233 -    times_divide_eq_right [of _ _ "number_of w", standard]
   1.234 -declare times_divide_eq_right_number_of [simp]
   1.235 -
   1.236 -lemmas times_divide_eq_left_number_of =
   1.237 -    times_divide_eq_left [of _ "number_of w", standard]
   1.238 -declare times_divide_eq_left_number_of [simp]
   1.239 -
   1.240 -lemmas times_divide_eq_left_number_of =
   1.241 -    times_divide_eq_left [of _ _ "number_of w", standard]
   1.242 -declare times_divide_eq_left_number_of [simp]
   1.243 -
   1.244 -****)
   1.245 -
   1.246 -text {*Replaces @{text "inverse #nn"} by @{text "1/#nn"}.  It looks
   1.247 -  strange, but then other simprocs simplify the quotient.*}
   1.248 -
   1.249 -lemmas inverse_eq_divide_number_of =
   1.250 -    inverse_eq_divide [of "number_of w", standard]
   1.251 -declare inverse_eq_divide_number_of [simp]
   1.252 -
   1.253 -
   1.254 -text {*These laws simplify inequalities, moving unary minus from a term
   1.255 -into the literal.*}
   1.256 -lemmas less_minus_iff_number_of =
   1.257 -    less_minus_iff [of "number_of v", standard]
   1.258 -declare less_minus_iff_number_of [simp,noatp]
   1.259 -
   1.260 -lemmas le_minus_iff_number_of =
   1.261 -    le_minus_iff [of "number_of v", standard]
   1.262 -declare le_minus_iff_number_of [simp,noatp]
   1.263 -
   1.264 -lemmas equation_minus_iff_number_of =
   1.265 -    equation_minus_iff [of "number_of v", standard]
   1.266 -declare equation_minus_iff_number_of [simp,noatp]
   1.267 -
   1.268 -
   1.269 -lemmas minus_less_iff_number_of =
   1.270 -    minus_less_iff [of _ "number_of v", standard]
   1.271 -declare minus_less_iff_number_of [simp,noatp]
   1.272 -
   1.273 -lemmas minus_le_iff_number_of =
   1.274 -    minus_le_iff [of _ "number_of v", standard]
   1.275 -declare minus_le_iff_number_of [simp,noatp]
   1.276 -
   1.277 -lemmas minus_equation_iff_number_of =
   1.278 -    minus_equation_iff [of _ "number_of v", standard]
   1.279 -declare minus_equation_iff_number_of [simp,noatp]
   1.280 -
   1.281 -
   1.282 -text{*To Simplify Inequalities Where One Side is the Constant 1*}
   1.283 -
   1.284 -lemma less_minus_iff_1 [simp,noatp]:
   1.285 -  fixes b::"'b::{ordered_idom,number_ring}"
   1.286 -  shows "(1 < - b) = (b < -1)"
   1.287 -by auto
   1.288 -
   1.289 -lemma le_minus_iff_1 [simp,noatp]:
   1.290 -  fixes b::"'b::{ordered_idom,number_ring}"
   1.291 -  shows "(1 \<le> - b) = (b \<le> -1)"
   1.292 -by auto
   1.293 -
   1.294 -lemma equation_minus_iff_1 [simp,noatp]:
   1.295 -  fixes b::"'b::number_ring"
   1.296 -  shows "(1 = - b) = (b = -1)"
   1.297 -by (subst equation_minus_iff, auto)
   1.298 -
   1.299 -lemma minus_less_iff_1 [simp,noatp]:
   1.300 -  fixes a::"'b::{ordered_idom,number_ring}"
   1.301 -  shows "(- a < 1) = (-1 < a)"
   1.302 -by auto
   1.303 -
   1.304 -lemma minus_le_iff_1 [simp,noatp]:
   1.305 -  fixes a::"'b::{ordered_idom,number_ring}"
   1.306 -  shows "(- a \<le> 1) = (-1 \<le> a)"
   1.307 -by auto
   1.308 -
   1.309 -lemma minus_equation_iff_1 [simp,noatp]:
   1.310 -  fixes a::"'b::number_ring"
   1.311 -  shows "(- a = 1) = (a = -1)"
   1.312 -by (subst minus_equation_iff, auto)
   1.313 -
   1.314 -
   1.315 -text {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"}) *}
   1.316 -
   1.317 -lemmas mult_less_cancel_left_number_of =
   1.318 -    mult_less_cancel_left [of "number_of v", standard]
   1.319 -declare mult_less_cancel_left_number_of [simp,noatp]
   1.320 -
   1.321 -lemmas mult_less_cancel_right_number_of =
   1.322 -    mult_less_cancel_right [of _ "number_of v", standard]
   1.323 -declare mult_less_cancel_right_number_of [simp,noatp]
   1.324 -
   1.325 -lemmas mult_le_cancel_left_number_of =
   1.326 -    mult_le_cancel_left [of "number_of v", standard]
   1.327 -declare mult_le_cancel_left_number_of [simp,noatp]
   1.328 -
   1.329 -lemmas mult_le_cancel_right_number_of =
   1.330 -    mult_le_cancel_right [of _ "number_of v", standard]
   1.331 -declare mult_le_cancel_right_number_of [simp,noatp]
   1.332 -
   1.333 -
   1.334 -text {*Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\<le>"} and @{text "="}) *}
   1.335 -
   1.336 -lemmas le_divide_eq_number_of1 [simp] = le_divide_eq [of _ _ "number_of w", standard]
   1.337 -lemmas divide_le_eq_number_of1 [simp] = divide_le_eq [of _ "number_of w", standard]
   1.338 -lemmas less_divide_eq_number_of1 [simp] = less_divide_eq [of _ _ "number_of w", standard]
   1.339 -lemmas divide_less_eq_number_of1 [simp] = divide_less_eq [of _ "number_of w", standard]
   1.340 -lemmas eq_divide_eq_number_of1 [simp] = eq_divide_eq [of _ _ "number_of w", standard]
   1.341 -lemmas divide_eq_eq_number_of1 [simp] = divide_eq_eq [of _ "number_of w", standard]
   1.342 -
   1.343 -
   1.344 -subsubsection{*Optional Simplification Rules Involving Constants*}
   1.345 -
   1.346 -text{*Simplify quotients that are compared with a literal constant.*}
   1.347 -
   1.348 -lemmas le_divide_eq_number_of = le_divide_eq [of "number_of w", standard]
   1.349 -lemmas divide_le_eq_number_of = divide_le_eq [of _ _ "number_of w", standard]
   1.350 -lemmas less_divide_eq_number_of = less_divide_eq [of "number_of w", standard]
   1.351 -lemmas divide_less_eq_number_of = divide_less_eq [of _ _ "number_of w", standard]
   1.352 -lemmas eq_divide_eq_number_of = eq_divide_eq [of "number_of w", standard]
   1.353 -lemmas divide_eq_eq_number_of = divide_eq_eq [of _ _ "number_of w", standard]
   1.354 -
   1.355 -
   1.356 -text{*Not good as automatic simprules because they cause case splits.*}
   1.357 -lemmas divide_const_simps =
   1.358 -  le_divide_eq_number_of divide_le_eq_number_of less_divide_eq_number_of
   1.359 -  divide_less_eq_number_of eq_divide_eq_number_of divide_eq_eq_number_of
   1.360 -  le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1
   1.361 -
   1.362 -text{*Division By @{text "-1"}*}
   1.363 -
   1.364 -lemma divide_minus1 [simp]:
   1.365 -     "x/-1 = -(x::'a::{field,division_by_zero,number_ring})"
   1.366 -by simp
   1.367 -
   1.368 -lemma minus1_divide [simp]:
   1.369 -     "-1 / (x::'a::{field,division_by_zero,number_ring}) = - (1/x)"
   1.370 -by (simp add: divide_inverse inverse_minus_eq)
   1.371 -
   1.372 -lemma half_gt_zero_iff:
   1.373 -     "(0 < r/2) = (0 < (r::'a::{ordered_field,division_by_zero,number_ring}))"
   1.374 -by auto
   1.375 -
   1.376 -lemmas half_gt_zero = half_gt_zero_iff [THEN iffD2, standard]
   1.377 -declare half_gt_zero [simp]
   1.378 -
   1.379 -(* The following lemma should appear in Divides.thy, but there the proof
   1.380 -   doesn't work. *)
   1.381 -
   1.382 -lemma nat_dvd_not_less:
   1.383 -  "[| 0 < m; m < n |] ==> \<not> n dvd (m::nat)"
   1.384 -  by (unfold dvd_def) auto
   1.385 -
   1.386 -ML {*
   1.387 -val divide_minus1 = @{thm divide_minus1};
   1.388 -val minus1_divide = @{thm minus1_divide};
   1.389 -*}
   1.390 -
   1.391 -end
     2.1 --- a/src/HOL/Groebner_Basis.thy	Sun Mar 22 20:46:11 2009 +0100
     2.2 +++ b/src/HOL/Groebner_Basis.thy	Sun Mar 22 20:46:11 2009 +0100
     2.3 @@ -5,7 +5,7 @@
     2.4  header {* Semiring normalization and Groebner Bases *}
     2.5  
     2.6  theory Groebner_Basis
     2.7 -imports Arith_Tools
     2.8 +imports NatBin
     2.9  uses
    2.10    "Tools/Groebner_Basis/misc.ML"
    2.11    "Tools/Groebner_Basis/normalizer_data.ML"
     3.1 --- a/src/HOL/IsaMakefile	Sun Mar 22 20:46:11 2009 +0100
     3.2 +++ b/src/HOL/IsaMakefile	Sun Mar 22 20:46:11 2009 +0100
     3.3 @@ -204,7 +204,6 @@
     3.4  	@$(ISABELLE_TOOL) usedir -b -f plain.ML -g true $(OUT)/Pure HOL-Plain
     3.5  
     3.6  MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \
     3.7 -  Arith_Tools.thy \
     3.8    ATP_Linkup.thy \
     3.9    Code_Eval.thy \
    3.10    Code_Message.thy \
     4.1 --- a/src/HOL/Library/Topology_Euclidean_Space.thy	Sun Mar 22 20:46:11 2009 +0100
     4.2 +++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Sun Mar 22 20:46:11 2009 +0100
     4.3 @@ -6,10 +6,9 @@
     4.4  header {* Elementary topology in Euclidean space. *}
     4.5  
     4.6  theory Topology_Euclidean_Space
     4.7 -  imports SEQ Euclidean_Space
     4.8 +imports SEQ Euclidean_Space
     4.9  begin
    4.10  
    4.11 -
    4.12  declare fstcart_pastecart[simp] sndcart_pastecart[simp]
    4.13  
    4.14  subsection{* General notion of a topology *}
    4.15 @@ -474,7 +473,7 @@
    4.16    have th0: "\<And>d x y z. (d x z :: real) <= d x y + d y z \<Longrightarrow> d y z = d z y
    4.17                 ==> ~(d x y * 2 < d x z \<and> d z y * 2 < d x z)" by arith
    4.18    have "?P ?U ?V" using dist_pos_lt[OF xy] th0[of dist,OF dist_triangle dist_sym]
    4.19 -    by (auto simp add: dist_refl expand_set_eq Arith_Tools.less_divide_eq_number_of1)
    4.20 +    by (auto simp add: dist_refl expand_set_eq less_divide_eq_number_of1)
    4.21    then show ?thesis by blast
    4.22  qed
    4.23  
    4.24 @@ -662,7 +661,7 @@
    4.25  	have "?k/2 \<ge> 0" using kp by simp
    4.26  	then obtain w where w: "dist y w = ?k/ 2" by (metis vector_choose_dist)
    4.27  	from iT[unfolded expand_set_eq mem_interior]
    4.28 -	have "\<not> ball w (?k/4) \<subseteq> T" using kp by (auto simp add: Arith_Tools.less_divide_eq_number_of1)
    4.29 +	have "\<not> ball w (?k/4) \<subseteq> T" using kp by (auto simp add: less_divide_eq_number_of1)
    4.30  	then obtain z where z: "dist w z < ?k/4" "z \<notin> T" by (auto simp add: subset_eq)
    4.31  	have "z \<notin> T \<and> z\<noteq> y \<and> dist z y < d \<and> dist x z < e" using z apply simp
    4.32  	  using w e(1) d apply (auto simp only: dist_sym)
    4.33 @@ -1323,7 +1322,7 @@
    4.34      assume "e>0"
    4.35      hence *:"eventually (\<lambda>x. dist (f x) l < e/2) net"
    4.36              "eventually (\<lambda>x. dist (g x) m < e/2) net" using as
    4.37 -      by (auto intro: tendstoD simp del: Arith_Tools.less_divide_eq_number_of1)
    4.38 +      by (auto intro: tendstoD simp del: less_divide_eq_number_of1)
    4.39      hence "eventually (\<lambda>x. dist (f x + g x) (l + m) < e) net"
    4.40      proof(cases "trivial_limit net")
    4.41        case True
    4.42 @@ -3957,7 +3956,7 @@
    4.43        hence fx0:"f x \<noteq> 0" using `l \<noteq> 0` by auto
    4.44        hence fxl0: "(f x) * l \<noteq> 0" using `l \<noteq> 0` by auto
    4.45        from * have **:"\<bar>f x - l\<bar> < l\<twosuperior> * e / 2" by auto
    4.46 -      have "\<bar>f x\<bar> * 2 \<ge> \<bar>l\<bar>" using * by (auto simp del: Arith_Tools.less_divide_eq_number_of1)
    4.47 +      have "\<bar>f x\<bar> * 2 \<ge> \<bar>l\<bar>" using * by (auto simp del: less_divide_eq_number_of1)
    4.48        hence "\<bar>f x\<bar> * 2 * \<bar>l\<bar>  \<ge> \<bar>l\<bar> * \<bar>l\<bar>" unfolding mult_le_cancel_right by auto
    4.49        hence "\<bar>f x * l\<bar> * 2  \<ge> \<bar>l\<bar>^2" unfolding real_mult_commute and power2_eq_square by auto
    4.50        hence ***:"inverse \<bar>f x * l\<bar> \<le> inverse (l\<twosuperior> / 2)" using fxl0
    4.51 @@ -4319,7 +4318,7 @@
    4.52        have "a$i < b$i" using as[THEN spec[where x=i]] by auto
    4.53        hence "a$i < ((1/2) *s (a+b)) $ i" "((1/2) *s (a+b)) $ i < b$i"
    4.54  	unfolding vector_smult_component and vector_add_component
    4.55 -	by (auto simp add: Arith_Tools.less_divide_eq_number_of1)  }
    4.56 +	by (auto simp add: less_divide_eq_number_of1)  }
    4.57      hence "{a <..< b} \<noteq> {}" using mem_interval(1)[of "?x" a b] by auto  }
    4.58    ultimately show ?th1 by blast
    4.59  
    4.60 @@ -4334,7 +4333,7 @@
    4.61        have "a$i \<le> b$i" using as[THEN spec[where x=i]] by auto
    4.62        hence "a$i \<le> ((1/2) *s (a+b)) $ i" "((1/2) *s (a+b)) $ i \<le> b$i"
    4.63  	unfolding vector_smult_component and vector_add_component
    4.64 -	by (auto simp add: Arith_Tools.less_divide_eq_number_of1)  }
    4.65 +	by (auto simp add: less_divide_eq_number_of1)  }
    4.66      hence "{a .. b} \<noteq> {}" using mem_interval(2)[of "?x" a b] by auto  }
    4.67    ultimately show ?th2 by blast
    4.68  qed
    4.69 @@ -4398,13 +4397,13 @@
    4.70        { fix j
    4.71  	have "c $ j < ?x $ j \<and> ?x $ j < d $ j" unfolding Cart_lambda_beta
    4.72  	  apply(cases "j=i") using as(2)[THEN spec[where x=j]]
    4.73 -	  by (auto simp add: Arith_Tools.less_divide_eq_number_of1 as2)  }
    4.74 +	  by (auto simp add: less_divide_eq_number_of1 as2)  }
    4.75        hence "?x\<in>{c<..<d}" unfolding mem_interval by auto
    4.76        moreover
    4.77        have "?x\<notin>{a .. b}"
    4.78  	unfolding mem_interval apply auto apply(rule_tac x=i in exI)
    4.79  	using as(2)[THEN spec[where x=i]] and as2
    4.80 -	by (auto simp add: Arith_Tools.less_divide_eq_number_of1)
    4.81 +	by (auto simp add: less_divide_eq_number_of1)
    4.82        ultimately have False using as by auto  }
    4.83      hence "a$i \<le> c$i" by(rule ccontr)auto
    4.84      moreover
    4.85 @@ -4413,13 +4412,13 @@
    4.86        { fix j
    4.87  	have "d $ j > ?x $ j \<and> ?x $ j > c $ j" unfolding Cart_lambda_beta
    4.88  	  apply(cases "j=i") using as(2)[THEN spec[where x=j]]
    4.89 -	  by (auto simp add: Arith_Tools.less_divide_eq_number_of1 as2)  }
    4.90 +	  by (auto simp add: less_divide_eq_number_of1 as2)  }
    4.91        hence "?x\<in>{c<..<d}" unfolding mem_interval by auto
    4.92        moreover
    4.93        have "?x\<notin>{a .. b}"
    4.94  	unfolding mem_interval apply auto apply(rule_tac x=i in exI)
    4.95  	using as(2)[THEN spec[where x=i]] and as2
    4.96 -	by (auto simp add: Arith_Tools.less_divide_eq_number_of1)
    4.97 +	by (auto simp add: less_divide_eq_number_of1)
    4.98        ultimately have False using as by auto  }
    4.99      hence "b$i \<ge> d$i" by(rule ccontr)auto
   4.100      ultimately
   4.101 @@ -4450,7 +4449,7 @@
   4.102  lemma inter_interval: fixes a :: "'a::linorder^'n::finite" shows
   4.103   "{a .. b} \<inter> {c .. d} =  {(\<chi> i. max (a$i) (c$i)) .. (\<chi> i. min (b$i) (d$i))}"
   4.104    unfolding expand_set_eq and Int_iff and mem_interval
   4.105 -  by (auto simp add: Arith_Tools.less_divide_eq_number_of1 intro!: bexI)
   4.106 +  by (auto simp add: less_divide_eq_number_of1 intro!: bexI)
   4.107  
   4.108  (* Moved interval_open_subset_closed a bit upwards *)
   4.109  
   4.110 @@ -4565,7 +4564,7 @@
   4.111      have "a $ i < ((1 / 2) *s (a + b)) $ i \<and> ((1 / 2) *s (a + b)) $ i < b $ i"
   4.112        using assms[unfolded interval_ne_empty, THEN spec[where x=i]]
   4.113        unfolding vector_smult_component and vector_add_component
   4.114 -      by(auto simp add: Arith_Tools.less_divide_eq_number_of1)  }
   4.115 +      by(auto simp add: less_divide_eq_number_of1)  }
   4.116    thus ?thesis unfolding mem_interval by auto
   4.117  qed
   4.118  
   4.119 @@ -5633,7 +5632,7 @@
   4.120      { assume as:"dist a b > dist (f n x) (f n y)"
   4.121        then obtain Na Nb where "\<forall>m\<ge>Na. dist (f (r m) x) a < (dist a b - dist (f n x) (f n y)) / 2"
   4.122  	and "\<forall>m\<ge>Nb. dist (f (r m) y) b < (dist a b - dist (f n x) (f n y)) / 2"
   4.123 -	using lima limb unfolding h_def Lim_sequentially by (fastsimp simp del: Arith_Tools.less_divide_eq_number_of1)
   4.124 +	using lima limb unfolding h_def Lim_sequentially by (fastsimp simp del: less_divide_eq_number_of1)
   4.125        hence "dist (f (r (Na + Nb + n)) x - f (r (Na + Nb + n)) y) (a - b) < dist a b - dist (f n x) (f n y)"
   4.126  	apply(erule_tac x="Na+Nb+n" in allE)
   4.127  	apply(erule_tac x="Na+Nb+n" in allE) apply simp