src/HOL/Library/BigO.thy
changeset 61945 1135b8de26c3
parent 61762 d50b993b4fb9
child 61969 e01015e49041
     1.1 --- a/src/HOL/Library/BigO.thy	Mon Dec 28 01:26:34 2015 +0100
     1.2 +++ b/src/HOL/Library/BigO.thy	Mon Dec 28 01:28:28 2015 +0100
     1.3 @@ -35,19 +35,19 @@
     1.4  subsection \<open>Definitions\<close>
     1.5  
     1.6  definition bigo :: "('a \<Rightarrow> 'b::linordered_idom) \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(1O'(_'))")
     1.7 -  where "O(f:: 'a \<Rightarrow> 'b) = {h. \<exists>c. \<forall>x. abs (h x) \<le> c * abs (f x)}"
     1.8 +  where "O(f:: 'a \<Rightarrow> 'b) = {h. \<exists>c. \<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>}"
     1.9  
    1.10  lemma bigo_pos_const:
    1.11 -  "(\<exists>c::'a::linordered_idom. \<forall>x. abs (h x) \<le> c * abs (f x)) \<longleftrightarrow>
    1.12 -    (\<exists>c. 0 < c \<and> (\<forall>x. abs (h x) \<le> c * abs (f x)))"
    1.13 +  "(\<exists>c::'a::linordered_idom. \<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>) \<longleftrightarrow>
    1.14 +    (\<exists>c. 0 < c \<and> (\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>))"
    1.15    apply auto
    1.16    apply (case_tac "c = 0")
    1.17    apply simp
    1.18    apply (rule_tac x = "1" in exI)
    1.19    apply simp
    1.20 -  apply (rule_tac x = "abs c" in exI)
    1.21 +  apply (rule_tac x = "\<bar>c\<bar>" in exI)
    1.22    apply auto
    1.23 -  apply (subgoal_tac "c * abs (f x) \<le> abs c * abs (f x)")
    1.24 +  apply (subgoal_tac "c * \<bar>f x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>")
    1.25    apply (erule_tac x = x in allE)
    1.26    apply force
    1.27    apply (rule mult_right_mono)
    1.28 @@ -55,7 +55,7 @@
    1.29    apply (rule abs_ge_zero)
    1.30    done
    1.31  
    1.32 -lemma bigo_alt_def: "O(f) = {h. \<exists>c. 0 < c \<and> (\<forall>x. abs (h x) \<le> c * abs (f x))}"
    1.33 +lemma bigo_alt_def: "O(f) = {h. \<exists>c. 0 < c \<and> (\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>)}"
    1.34    by (auto simp add: bigo_def bigo_pos_const)
    1.35  
    1.36  lemma bigo_elt_subset [intro]: "f \<in> O(g) \<Longrightarrow> O(f) \<le> O(g)"
    1.37 @@ -65,7 +65,7 @@
    1.38    apply simp
    1.39    apply (rule allI)
    1.40    apply (drule_tac x = "xa" in spec)+
    1.41 -  apply (subgoal_tac "ca * abs (f xa) \<le> ca * (c * abs (g xa))")
    1.42 +  apply (subgoal_tac "ca * \<bar>f xa\<bar> \<le> ca * (c * \<bar>g xa\<bar>)")
    1.43    apply (erule order_trans)
    1.44    apply (simp add: ac_simps)
    1.45    apply (rule mult_left_mono, assumption)
    1.46 @@ -110,29 +110,29 @@
    1.47    apply (rule subsetI)
    1.48    apply (auto simp add: bigo_def bigo_pos_const func_plus set_plus_def)
    1.49    apply (subst bigo_pos_const [symmetric])+
    1.50 -  apply (rule_tac x = "\<lambda>n. if abs (g n) \<le> (abs (f n)) then x n else 0" in exI)
    1.51 +  apply (rule_tac x = "\<lambda>n. if \<bar>g n\<bar> \<le> \<bar>f n\<bar> then x n else 0" in exI)
    1.52    apply (rule conjI)
    1.53    apply (rule_tac x = "c + c" in exI)
    1.54    apply (clarsimp)
    1.55 -  apply (subgoal_tac "c * abs (f xa + g xa) \<le> (c + c) * abs (f xa)")
    1.56 +  apply (subgoal_tac "c * \<bar>f xa + g xa\<bar> \<le> (c + c) * \<bar>f xa\<bar>")
    1.57    apply (erule_tac x = xa in allE)
    1.58    apply (erule order_trans)
    1.59    apply (simp)
    1.60 -  apply (subgoal_tac "c * abs (f xa + g xa) \<le> c * (abs (f xa) + abs (g xa))")
    1.61 +  apply (subgoal_tac "c * \<bar>f xa + g xa\<bar> \<le> c * (\<bar>f xa\<bar> + \<bar>g xa\<bar>)")
    1.62    apply (erule order_trans)
    1.63    apply (simp add: ring_distribs)
    1.64    apply (rule mult_left_mono)
    1.65    apply (simp add: abs_triangle_ineq)
    1.66    apply (simp add: order_less_le)
    1.67 -  apply (rule_tac x = "\<lambda>n. if (abs (f n)) < abs (g n) then x n else 0" in exI)
    1.68 +  apply (rule_tac x = "\<lambda>n. if \<bar>f n\<bar> < \<bar>g n\<bar> then x n else 0" in exI)
    1.69    apply (rule conjI)
    1.70    apply (rule_tac x = "c + c" in exI)
    1.71    apply auto
    1.72 -  apply (subgoal_tac "c * abs (f xa + g xa) \<le> (c + c) * abs (g xa)")
    1.73 +  apply (subgoal_tac "c * \<bar>f xa + g xa\<bar> \<le> (c + c) * \<bar>g xa\<bar>")
    1.74    apply (erule_tac x = xa in allE)
    1.75    apply (erule order_trans)
    1.76    apply simp
    1.77 -  apply (subgoal_tac "c * abs (f xa + g xa) \<le> c * (abs (f xa) + abs (g xa))")
    1.78 +  apply (subgoal_tac "c * \<bar>f xa + g xa\<bar> \<le> c * (\<bar>f xa\<bar> + \<bar>g xa\<bar>)")
    1.79    apply (erule order_trans)
    1.80    apply (simp add: ring_distribs)
    1.81    apply (rule mult_left_mono)
    1.82 @@ -162,8 +162,8 @@
    1.83    apply (drule_tac x = "xa" in spec)+
    1.84    apply (subgoal_tac "0 \<le> f xa + g xa")
    1.85    apply (simp add: ring_distribs)
    1.86 -  apply (subgoal_tac "abs (a xa + b xa) \<le> abs (a xa) + abs (b xa)")
    1.87 -  apply (subgoal_tac "abs (a xa) + abs (b xa) \<le> max c ca * f xa + max c ca * g xa")
    1.88 +  apply (subgoal_tac "\<bar>a xa + b xa\<bar> \<le> \<bar>a xa\<bar> + \<bar>b xa\<bar>")
    1.89 +  apply (subgoal_tac "\<bar>a xa\<bar> + \<bar>b xa\<bar> \<le> max c ca * f xa + max c ca * g xa")
    1.90    apply force
    1.91    apply (rule add_mono)
    1.92    apply (subgoal_tac "c * f xa \<le> max c ca * f xa")
    1.93 @@ -183,7 +183,7 @@
    1.94  
    1.95  lemma bigo_bounded_alt: "\<forall>x. 0 \<le> f x \<Longrightarrow> \<forall>x. f x \<le> c * g x \<Longrightarrow> f \<in> O(g)"
    1.96    apply (auto simp add: bigo_def)
    1.97 -  apply (rule_tac x = "abs c" in exI)
    1.98 +  apply (rule_tac x = "\<bar>c\<bar>" in exI)
    1.99    apply auto
   1.100    apply (drule_tac x = x in spec)+
   1.101    apply (simp add: abs_mult [symmetric])
   1.102 @@ -202,21 +202,21 @@
   1.103    apply force
   1.104    done
   1.105  
   1.106 -lemma bigo_abs: "(\<lambda>x. abs (f x)) =o O(f)"
   1.107 +lemma bigo_abs: "(\<lambda>x. \<bar>f x\<bar>) =o O(f)"
   1.108    apply (unfold bigo_def)
   1.109    apply auto
   1.110    apply (rule_tac x = 1 in exI)
   1.111    apply auto
   1.112    done
   1.113  
   1.114 -lemma bigo_abs2: "f =o O(\<lambda>x. abs (f x))"
   1.115 +lemma bigo_abs2: "f =o O(\<lambda>x. \<bar>f x\<bar>)"
   1.116    apply (unfold bigo_def)
   1.117    apply auto
   1.118    apply (rule_tac x = 1 in exI)
   1.119    apply auto
   1.120    done
   1.121  
   1.122 -lemma bigo_abs3: "O(f) = O(\<lambda>x. abs (f x))"
   1.123 +lemma bigo_abs3: "O(f) = O(\<lambda>x. \<bar>f x\<bar>)"
   1.124    apply (rule equalityI)
   1.125    apply (rule bigo_elt_subset)
   1.126    apply (rule bigo_abs2)
   1.127 @@ -224,15 +224,15 @@
   1.128    apply (rule bigo_abs)
   1.129    done
   1.130  
   1.131 -lemma bigo_abs4: "f =o g +o O(h) \<Longrightarrow> (\<lambda>x. abs (f x)) =o (\<lambda>x. abs (g x)) +o O(h)"
   1.132 +lemma bigo_abs4: "f =o g +o O(h) \<Longrightarrow> (\<lambda>x. \<bar>f x\<bar>) =o (\<lambda>x. \<bar>g x\<bar>) +o O(h)"
   1.133    apply (drule set_plus_imp_minus)
   1.134    apply (rule set_minus_imp_plus)
   1.135    apply (subst fun_diff_def)
   1.136  proof -
   1.137    assume a: "f - g \<in> O(h)"
   1.138 -  have "(\<lambda>x. abs (f x) - abs (g x)) =o O(\<lambda>x. abs (abs (f x) - abs (g x)))"
   1.139 +  have "(\<lambda>x. \<bar>f x\<bar> - \<bar>g x\<bar>) =o O(\<lambda>x. \<bar>\<bar>f x\<bar> - \<bar>g x\<bar>\<bar>)"
   1.140      by (rule bigo_abs2)
   1.141 -  also have "\<dots> \<subseteq> O(\<lambda>x. abs (f x - g x))"
   1.142 +  also have "\<dots> \<subseteq> O(\<lambda>x. \<bar>f x - g x\<bar>)"
   1.143      apply (rule bigo_elt_subset)
   1.144      apply (rule bigo_bounded)
   1.145      apply force
   1.146 @@ -246,10 +246,10 @@
   1.147      done
   1.148    also from a have "\<dots> \<subseteq> O(h)"
   1.149      by (rule bigo_elt_subset)
   1.150 -  finally show "(\<lambda>x. abs (f x) - abs (g x)) \<in> O(h)".
   1.151 +  finally show "(\<lambda>x. \<bar>f x\<bar> - \<bar>g x\<bar>) \<in> O(h)".
   1.152  qed
   1.153  
   1.154 -lemma bigo_abs5: "f =o O(g) \<Longrightarrow> (\<lambda>x. abs (f x)) =o O(g)"
   1.155 +lemma bigo_abs5: "f =o O(g) \<Longrightarrow> (\<lambda>x. \<bar>f x\<bar>) =o O(g)"
   1.156    by (unfold bigo_def, auto)
   1.157  
   1.158  lemma bigo_elt_subset2 [intro]: "f \<in> g +o O(h) \<Longrightarrow> O(f) \<subseteq> O(g) + O(h)"
   1.159 @@ -257,16 +257,16 @@
   1.160    assume "f \<in> g +o O(h)"
   1.161    also have "\<dots> \<subseteq> O(g) + O(h)"
   1.162      by (auto del: subsetI)
   1.163 -  also have "\<dots> = O(\<lambda>x. abs (g x)) + O(\<lambda>x. abs (h x))"
   1.164 +  also have "\<dots> = O(\<lambda>x. \<bar>g x\<bar>) + O(\<lambda>x. \<bar>h x\<bar>)"
   1.165      apply (subst bigo_abs3 [symmetric])+
   1.166      apply (rule refl)
   1.167      done
   1.168 -  also have "\<dots> = O((\<lambda>x. abs (g x)) + (\<lambda>x. abs (h x)))"
   1.169 +  also have "\<dots> = O((\<lambda>x. \<bar>g x\<bar>) + (\<lambda>x. \<bar>h x\<bar>))"
   1.170      by (rule bigo_plus_eq [symmetric]) auto
   1.171    finally have "f \<in> \<dots>" .
   1.172    then have "O(f) \<subseteq> \<dots>"
   1.173      by (elim bigo_elt_subset)
   1.174 -  also have "\<dots> = O(\<lambda>x. abs (g x)) + O(\<lambda>x. abs (h x))"
   1.175 +  also have "\<dots> = O(\<lambda>x. \<bar>g x\<bar>) + O(\<lambda>x. \<bar>h x\<bar>)"
   1.176      by (rule bigo_plus_eq, auto)
   1.177    finally show ?thesis
   1.178      by (simp add: bigo_abs3 [symmetric])
   1.179 @@ -279,7 +279,7 @@
   1.180    apply (rule_tac x = "c * ca" in exI)
   1.181    apply (rule allI)
   1.182    apply (erule_tac x = x in allE)+
   1.183 -  apply (subgoal_tac "c * ca * abs (f x * g x) = (c * abs (f x)) * (ca * abs (g x))")
   1.184 +  apply (subgoal_tac "c * ca * \<bar>f x * g x\<bar> = (c * \<bar>f x\<bar>) * (ca * \<bar>g x\<bar>)")
   1.185    apply (erule ssubst)
   1.186    apply (subst abs_mult)
   1.187    apply (rule mult_mono)
   1.188 @@ -293,7 +293,7 @@
   1.189    apply (rule_tac x = c in exI)
   1.190    apply auto
   1.191    apply (drule_tac x = x in spec)
   1.192 -  apply (subgoal_tac "abs (f x) * abs (b x) \<le> abs (f x) * (c * abs (g x))")
   1.193 +  apply (subgoal_tac "\<bar>f x\<bar> * \<bar>b x\<bar> \<le> \<bar>f x\<bar> * (c * \<bar>g x\<bar>)")
   1.194    apply (force simp add: ac_simps)
   1.195    apply (rule mult_left_mono, assumption)
   1.196    apply (rule abs_ge_zero)
   1.197 @@ -450,7 +450,7 @@
   1.198    fixes c :: "'a::linordered_field"
   1.199    shows "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. 1) \<in> O(\<lambda>x. c)"
   1.200    apply (simp add: bigo_def)
   1.201 -  apply (rule_tac x = "abs (inverse c)" in exI)
   1.202 +  apply (rule_tac x = "\<bar>inverse c\<bar>" in exI)
   1.203    apply (simp add: abs_mult [symmetric])
   1.204    done
   1.205  
   1.206 @@ -473,7 +473,7 @@
   1.207  
   1.208  lemma bigo_const_mult1: "(\<lambda>x. c * f x) \<in> O(f)"
   1.209    apply (simp add: bigo_def)
   1.210 -  apply (rule_tac x = "abs c" in exI)
   1.211 +  apply (rule_tac x = "\<bar>c\<bar>" in exI)
   1.212    apply (auto simp add: abs_mult [symmetric])
   1.213    done
   1.214  
   1.215 @@ -486,7 +486,7 @@
   1.216    fixes c :: "'a::linordered_field"
   1.217    shows "c \<noteq> 0 \<Longrightarrow> f \<in> O(\<lambda>x. c * f x)"
   1.218    apply (simp add: bigo_def)
   1.219 -  apply (rule_tac x = "abs (inverse c)" in exI)
   1.220 +  apply (rule_tac x = "\<bar>inverse c\<bar>" in exI)
   1.221    apply (simp add: abs_mult mult.assoc [symmetric])
   1.222    done
   1.223  
   1.224 @@ -516,15 +516,15 @@
   1.225    apply (auto intro!: simp add: bigo_def elt_set_times_def func_times)
   1.226    apply (rule_tac x = "\<lambda>y. inverse c * x y" in exI)
   1.227    apply (simp add: mult.assoc [symmetric] abs_mult)
   1.228 -  apply (rule_tac x = "abs (inverse c) * ca" in exI)
   1.229 +  apply (rule_tac x = "\<bar>inverse c\<bar> * ca" in exI)
   1.230    apply auto
   1.231    done
   1.232  
   1.233  lemma bigo_const_mult6 [intro]: "(\<lambda>x. c) *o O(f) \<subseteq> O(f)"
   1.234    apply (auto intro!: simp add: bigo_def elt_set_times_def func_times)
   1.235 -  apply (rule_tac x = "ca * abs c" in exI)
   1.236 +  apply (rule_tac x = "ca * \<bar>c\<bar>" in exI)
   1.237    apply (rule allI)
   1.238 -  apply (subgoal_tac "ca * abs c * abs (f x) = abs c * (ca * abs (f x))")
   1.239 +  apply (subgoal_tac "ca * \<bar>c\<bar> * \<bar>f x\<bar> = \<bar>c\<bar> * (ca * \<bar>f x\<bar>)")
   1.240    apply (erule ssubst)
   1.241    apply (subst abs_mult)
   1.242    apply (rule mult_left_mono)
   1.243 @@ -559,10 +559,10 @@
   1.244  subsection \<open>Setsum\<close>
   1.245  
   1.246  lemma bigo_setsum_main: "\<forall>x. \<forall>y \<in> A x. 0 \<le> h x y \<Longrightarrow>
   1.247 -    \<exists>c. \<forall>x. \<forall>y \<in> A x. abs (f x y) \<le> c * (h x y) \<Longrightarrow>
   1.248 +    \<exists>c. \<forall>x. \<forall>y \<in> A x. \<bar>f x y\<bar> \<le> c * h x y \<Longrightarrow>
   1.249        (\<lambda>x. \<Sum>y \<in> A x. f x y) =o O(\<lambda>x. \<Sum>y \<in> A x. h x y)"
   1.250    apply (auto simp add: bigo_def)
   1.251 -  apply (rule_tac x = "abs c" in exI)
   1.252 +  apply (rule_tac x = "\<bar>c\<bar>" in exI)
   1.253    apply (subst abs_of_nonneg) back back
   1.254    apply (rule setsum_nonneg)
   1.255    apply force
   1.256 @@ -583,7 +583,7 @@
   1.257    done
   1.258  
   1.259  lemma bigo_setsum1: "\<forall>x y. 0 \<le> h x y \<Longrightarrow>
   1.260 -    \<exists>c. \<forall>x y. abs (f x y) \<le> c * h x y \<Longrightarrow>
   1.261 +    \<exists>c. \<forall>x y. \<bar>f x y\<bar> \<le> c * h x y \<Longrightarrow>
   1.262        (\<lambda>x. \<Sum>y \<in> A x. f x y) =o O(\<lambda>x. \<Sum>y \<in> A x. h x y)"
   1.263    apply (rule bigo_setsum_main)
   1.264    apply force
   1.265 @@ -593,12 +593,12 @@
   1.266    done
   1.267  
   1.268  lemma bigo_setsum2: "\<forall>y. 0 \<le> h y \<Longrightarrow>
   1.269 -    \<exists>c. \<forall>y. abs (f y) \<le> c * (h y) \<Longrightarrow>
   1.270 +    \<exists>c. \<forall>y. \<bar>f y\<bar> \<le> c * (h y) \<Longrightarrow>
   1.271        (\<lambda>x. \<Sum>y \<in> A x. f y) =o O(\<lambda>x. \<Sum>y \<in> A x. h y)"
   1.272    by (rule bigo_setsum1) auto
   1.273  
   1.274  lemma bigo_setsum3: "f =o O(h) \<Longrightarrow>
   1.275 -    (\<lambda>x. \<Sum>y \<in> A x. l x y * f (k x y)) =o O(\<lambda>x. \<Sum>y \<in> A x. abs (l x y * h (k x y)))"
   1.276 +    (\<lambda>x. \<Sum>y \<in> A x. l x y * f (k x y)) =o O(\<lambda>x. \<Sum>y \<in> A x. \<bar>l x y * h (k x y)\<bar>)"
   1.277    apply (rule bigo_setsum1)
   1.278    apply (rule allI)+
   1.279    apply (rule abs_ge_zero)
   1.280 @@ -616,7 +616,7 @@
   1.281  lemma bigo_setsum4: "f =o g +o O(h) \<Longrightarrow>
   1.282      (\<lambda>x. \<Sum>y \<in> A x. l x y * f (k x y)) =o
   1.283        (\<lambda>x. \<Sum>y \<in> A x. l x y * g (k x y)) +o
   1.284 -        O(\<lambda>x. \<Sum>y \<in> A x. abs (l x y * h (k x y)))"
   1.285 +        O(\<lambda>x. \<Sum>y \<in> A x. \<bar>l x y * h (k x y)\<bar>)"
   1.286    apply (rule set_minus_imp_plus)
   1.287    apply (subst fun_diff_def)
   1.288    apply (subst setsum_subtractf [symmetric])
   1.289 @@ -631,7 +631,7 @@
   1.290        (\<lambda>x. \<Sum>y \<in> A x. l x y * f (k x y)) =o
   1.291          O(\<lambda>x. \<Sum>y \<in> A x. l x y * h (k x y))"
   1.292    apply (subgoal_tac "(\<lambda>x. \<Sum>y \<in> A x. l x y * h (k x y)) =
   1.293 -      (\<lambda>x. \<Sum>y \<in> A x. abs (l x y * h (k x y)))")
   1.294 +      (\<lambda>x. \<Sum>y \<in> A x. \<bar>l x y * h (k x y)\<bar>)")
   1.295    apply (erule ssubst)
   1.296    apply (erule bigo_setsum3)
   1.297    apply (rule ext)
   1.298 @@ -715,7 +715,7 @@
   1.299  definition lesso :: "('a \<Rightarrow> 'b::linordered_idom) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"  (infixl "<o" 70)
   1.300    where "f <o g = (\<lambda>x. max (f x - g x) 0)"
   1.301  
   1.302 -lemma bigo_lesseq1: "f =o O(h) \<Longrightarrow> \<forall>x. abs (g x) \<le> abs (f x) \<Longrightarrow> g =o O(h)"
   1.303 +lemma bigo_lesseq1: "f =o O(h) \<Longrightarrow> \<forall>x. \<bar>g x\<bar> \<le> \<bar>f x\<bar> \<Longrightarrow> g =o O(h)"
   1.304    apply (unfold bigo_def)
   1.305    apply clarsimp
   1.306    apply (rule_tac x = c in exI)
   1.307 @@ -724,7 +724,7 @@
   1.308    apply (erule spec)+
   1.309    done
   1.310  
   1.311 -lemma bigo_lesseq2: "f =o O(h) \<Longrightarrow> \<forall>x. abs (g x) \<le> f x \<Longrightarrow> g =o O(h)"
   1.312 +lemma bigo_lesseq2: "f =o O(h) \<Longrightarrow> \<forall>x. \<bar>g x\<bar> \<le> f x \<Longrightarrow> g =o O(h)"
   1.313    apply (erule bigo_lesseq1)
   1.314    apply (rule allI)
   1.315    apply (drule_tac x = x in spec)
   1.316 @@ -741,7 +741,7 @@
   1.317    done
   1.318  
   1.319  lemma bigo_lesseq4: "f =o O(h) \<Longrightarrow>
   1.320 -    \<forall>x. 0 \<le> g x \<Longrightarrow> \<forall>x. g x \<le> abs (f x) \<Longrightarrow> g =o O(h)"
   1.321 +    \<forall>x. 0 \<le> g x \<Longrightarrow> \<forall>x. g x \<le> \<bar>f x\<bar> \<Longrightarrow> g =o O(h)"
   1.322    apply (erule bigo_lesseq1)
   1.323    apply (rule allI)
   1.324    apply (subst abs_of_nonneg)
   1.325 @@ -819,13 +819,13 @@
   1.326    apply (auto simp add: func_plus fun_diff_def algebra_simps split: split_max abs_split)
   1.327    done
   1.328  
   1.329 -lemma bigo_lesso5: "f <o g =o O(h) \<Longrightarrow> \<exists>C. \<forall>x. f x \<le> g x + C * abs (h x)"
   1.330 +lemma bigo_lesso5: "f <o g =o O(h) \<Longrightarrow> \<exists>C. \<forall>x. f x \<le> g x + C * \<bar>h x\<bar>"
   1.331    apply (simp only: lesso_def bigo_alt_def)
   1.332    apply clarsimp
   1.333    apply (rule_tac x = c in exI)
   1.334    apply (rule allI)
   1.335    apply (drule_tac x = x in spec)
   1.336 -  apply (subgoal_tac "abs (max (f x - g x) 0) = max (f x - g x) 0")
   1.337 +  apply (subgoal_tac "\<bar>max (f x - g x) 0\<bar> = max (f x - g x) 0")
   1.338    apply (clarsimp simp add: algebra_simps)
   1.339    apply (rule abs_of_nonneg)
   1.340    apply (rule max.cobounded2)
   1.341 @@ -856,7 +856,7 @@
   1.342    apply (rule order_le_less_trans)
   1.343    apply assumption
   1.344    apply (rule order_less_le_trans)
   1.345 -  apply (subgoal_tac "c * abs (g n) < c * (r / c)")
   1.346 +  apply (subgoal_tac "c * \<bar>g n\<bar> < c * (r / c)")
   1.347    apply assumption
   1.348    apply (erule mult_strict_left_mono)
   1.349    apply assumption