src/HOL/Library/BigO.thy
changeset 55821 44055f07cbd8
parent 54863 82acc20ded73
child 56536 aefb4a8da31f
     1.1 --- a/src/HOL/Library/BigO.thy	Sat Mar 01 12:07:26 2014 +0100
     1.2 +++ b/src/HOL/Library/BigO.thy	Sat Mar 01 13:05:46 2014 +0100
     1.3 @@ -19,7 +19,7 @@
     1.4  \item We have eliminated the @{text O} operator on sets. (Most uses of this seem
     1.5    to be inessential.)
     1.6  \item We no longer use @{text "+"} as output syntax for @{text "+o"}
     1.7 -\item Lemmas involving @{text "sumr"} have been replaced by more general lemmas 
     1.8 +\item Lemmas involving @{text "sumr"} have been replaced by more general lemmas
     1.9    involving `@{text "setsum"}.
    1.10  \item The library has been expanded, with e.g.~support for expressions of
    1.11    the form @{text "f < g + O(h)"}.
    1.12 @@ -34,14 +34,12 @@
    1.13  
    1.14  subsection {* Definitions *}
    1.15  
    1.16 -definition
    1.17 -  bigo :: "('a => 'b::linordered_idom) => ('a => 'b) set"  ("(1O'(_'))") where
    1.18 -  "O(f::('a => 'b)) =
    1.19 -      {h. EX c. ALL x. abs (h x) <= c * abs (f x)}"
    1.20 +definition bigo :: "('a \<Rightarrow> 'b::linordered_idom) \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(1O'(_'))")
    1.21 +  where "O(f:: 'a \<Rightarrow> 'b) = {h. \<exists>c. \<forall>x. abs (h x) \<le> c * abs (f x)}"
    1.22  
    1.23 -lemma bigo_pos_const: "(EX (c::'a::linordered_idom). 
    1.24 -    ALL x. (abs (h x)) <= (c * (abs (f x))))
    1.25 -      = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
    1.26 +lemma bigo_pos_const:
    1.27 +  "(\<exists>c::'a::linordered_idom. \<forall>x. abs (h x) \<le> c * abs (f x)) \<longleftrightarrow>
    1.28 +    (\<exists>c. 0 < c \<and> (\<forall>x. abs (h x) \<le> c * abs (f x)))"
    1.29    apply auto
    1.30    apply (case_tac "c = 0")
    1.31    apply simp
    1.32 @@ -49,7 +47,7 @@
    1.33    apply simp
    1.34    apply (rule_tac x = "abs c" in exI)
    1.35    apply auto
    1.36 -  apply (subgoal_tac "c * abs(f x) <= abs c * abs (f x)")
    1.37 +  apply (subgoal_tac "c * abs (f x) \<le> abs c * abs (f x)")
    1.38    apply (erule_tac x = x in allE)
    1.39    apply force
    1.40    apply (rule mult_right_mono)
    1.41 @@ -57,42 +55,40 @@
    1.42    apply (rule abs_ge_zero)
    1.43    done
    1.44  
    1.45 -lemma bigo_alt_def: "O(f) = 
    1.46 -    {h. EX c. (0 < c & (ALL x. abs (h x) <= c * abs (f x)))}"
    1.47 +lemma bigo_alt_def: "O(f) = {h. \<exists>c. 0 < c \<and> (\<forall>x. abs (h x) \<le> c * abs (f x))}"
    1.48    by (auto simp add: bigo_def bigo_pos_const)
    1.49  
    1.50 -lemma bigo_elt_subset [intro]: "f : O(g) ==> O(f) <= O(g)"
    1.51 +lemma bigo_elt_subset [intro]: "f \<in> O(g) \<Longrightarrow> O(f) \<le> O(g)"
    1.52    apply (auto simp add: bigo_alt_def)
    1.53    apply (rule_tac x = "ca * c" in exI)
    1.54    apply (rule conjI)
    1.55    apply (rule mult_pos_pos)
    1.56 -  apply (assumption)+
    1.57 +  apply assumption+
    1.58    apply (rule allI)
    1.59    apply (drule_tac x = "xa" in spec)+
    1.60 -  apply (subgoal_tac "ca * abs(f xa) <= ca * (c * abs(g xa))")
    1.61 +  apply (subgoal_tac "ca * abs (f xa) \<le> ca * (c * abs (g xa))")
    1.62    apply (erule order_trans)
    1.63    apply (simp add: mult_ac)
    1.64    apply (rule mult_left_mono, assumption)
    1.65    apply (rule order_less_imp_le, assumption)
    1.66    done
    1.67  
    1.68 -lemma bigo_refl [intro]: "f : O(f)"
    1.69 +lemma bigo_refl [intro]: "f \<in> O(f)"
    1.70    apply(auto simp add: bigo_def)
    1.71    apply(rule_tac x = 1 in exI)
    1.72    apply simp
    1.73    done
    1.74  
    1.75 -lemma bigo_zero: "0 : O(g)"
    1.76 +lemma bigo_zero: "0 \<in> O(g)"
    1.77    apply (auto simp add: bigo_def func_zero)
    1.78    apply (rule_tac x = 0 in exI)
    1.79    apply auto
    1.80    done
    1.81  
    1.82 -lemma bigo_zero2: "O(%x.0) = {%x.0}"
    1.83 -  by (auto simp add: bigo_def) 
    1.84 +lemma bigo_zero2: "O(\<lambda>x. 0) = {\<lambda>x. 0}"
    1.85 +  by (auto simp add: bigo_def)
    1.86  
    1.87 -lemma bigo_plus_self_subset [intro]: 
    1.88 -  "O(f) + O(f) <= O(f)"
    1.89 +lemma bigo_plus_self_subset [intro]: "O(f) + O(f) \<subseteq> O(f)"
    1.90    apply (auto simp add: bigo_alt_def set_plus_def)
    1.91    apply (rule_tac x = "c + ca" in exI)
    1.92    apply auto
    1.93 @@ -102,30 +98,29 @@
    1.94    apply (rule add_mono)
    1.95    apply force
    1.96    apply force
    1.97 -done
    1.98 +  done
    1.99  
   1.100  lemma bigo_plus_idemp [simp]: "O(f) + O(f) = O(f)"
   1.101    apply (rule equalityI)
   1.102    apply (rule bigo_plus_self_subset)
   1.103 -  apply (rule set_zero_plus2) 
   1.104 +  apply (rule set_zero_plus2)
   1.105    apply (rule bigo_zero)
   1.106    done
   1.107  
   1.108 -lemma bigo_plus_subset [intro]: "O(f + g) <= O(f) + O(g)"
   1.109 +lemma bigo_plus_subset [intro]: "O(f + g) \<subseteq> O(f) + O(g)"
   1.110    apply (rule subsetI)
   1.111    apply (auto simp add: bigo_def bigo_pos_const func_plus set_plus_def)
   1.112    apply (subst bigo_pos_const [symmetric])+
   1.113 -  apply (rule_tac x = 
   1.114 -    "%n. if abs (g n) <= (abs (f n)) then x n else 0" in exI)
   1.115 +  apply (rule_tac x = "\<lambda>n. if abs (g n) \<le> (abs (f n)) then x n else 0" in exI)
   1.116    apply (rule conjI)
   1.117    apply (rule_tac x = "c + c" in exI)
   1.118    apply (clarsimp)
   1.119    apply (auto)
   1.120 -  apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (f xa)")
   1.121 +  apply (subgoal_tac "c * abs (f xa + g xa) \<le> (c + c) * abs (f xa)")
   1.122    apply (erule_tac x = xa in allE)
   1.123    apply (erule order_trans)
   1.124    apply (simp)
   1.125 -  apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))")
   1.126 +  apply (subgoal_tac "c * abs (f xa + g xa) \<le> c * (abs (f xa) + abs (g xa))")
   1.127    apply (erule order_trans)
   1.128    apply (simp add: ring_distribs)
   1.129    apply (rule mult_left_mono)
   1.130 @@ -133,16 +128,15 @@
   1.131    apply (simp add: order_less_le)
   1.132    apply (rule mult_nonneg_nonneg)
   1.133    apply auto
   1.134 -  apply (rule_tac x = "%n. if (abs (f n)) <  abs (g n) then x n else 0" 
   1.135 -     in exI)
   1.136 +  apply (rule_tac x = "\<lambda>n. if (abs (f n)) < abs (g n) then x n else 0" in exI)
   1.137    apply (rule conjI)
   1.138    apply (rule_tac x = "c + c" in exI)
   1.139    apply auto
   1.140 -  apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (g xa)")
   1.141 +  apply (subgoal_tac "c * abs (f xa + g xa) \<le> (c + c) * abs (g xa)")
   1.142    apply (erule_tac x = xa in allE)
   1.143    apply (erule order_trans)
   1.144 -  apply (simp)
   1.145 -  apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))")
   1.146 +  apply simp
   1.147 +  apply (subgoal_tac "c * abs (f xa + g xa) \<le> c * (abs (f xa) + abs (g xa))")
   1.148    apply (erule order_trans)
   1.149    apply (simp add: ring_distribs)
   1.150    apply (rule mult_left_mono)
   1.151 @@ -153,41 +147,39 @@
   1.152    apply simp
   1.153    done
   1.154  
   1.155 -lemma bigo_plus_subset2 [intro]: "A <= O(f) ==> B <= O(f) ==> A + B <= O(f)"
   1.156 -  apply (subgoal_tac "A + B <= O(f) + O(f)")
   1.157 +lemma bigo_plus_subset2 [intro]: "A \<subseteq> O(f) \<Longrightarrow> B \<subseteq> O(f) \<Longrightarrow> A + B \<subseteq> O(f)"
   1.158 +  apply (subgoal_tac "A + B \<subseteq> O(f) + O(f)")
   1.159    apply (erule order_trans)
   1.160    apply simp
   1.161    apply (auto del: subsetI simp del: bigo_plus_idemp)
   1.162    done
   1.163  
   1.164 -lemma bigo_plus_eq: "ALL x. 0 <= f x ==> ALL x. 0 <= g x ==> 
   1.165 -    O(f + g) = O(f) + O(g)"
   1.166 +lemma bigo_plus_eq: "\<forall>x. 0 \<le> f x \<Longrightarrow> \<forall>x. 0 \<le> g x \<Longrightarrow> O(f + g) = O(f) + O(g)"
   1.167    apply (rule equalityI)
   1.168    apply (rule bigo_plus_subset)
   1.169    apply (simp add: bigo_alt_def set_plus_def func_plus)
   1.170    apply clarify
   1.171    apply (rule_tac x = "max c ca" in exI)
   1.172    apply (rule conjI)
   1.173 -  apply (subgoal_tac "c <= max c ca")
   1.174 +  apply (subgoal_tac "c \<le> max c ca")
   1.175    apply (erule order_less_le_trans)
   1.176    apply assumption
   1.177    apply (rule max.cobounded1)
   1.178    apply clarify
   1.179    apply (drule_tac x = "xa" in spec)+
   1.180 -  apply (subgoal_tac "0 <= f xa + g xa")
   1.181 +  apply (subgoal_tac "0 \<le> f xa + g xa")
   1.182    apply (simp add: ring_distribs)
   1.183 -  apply (subgoal_tac "abs(a xa + b xa) <= abs(a xa) + abs(b xa)")
   1.184 -  apply (subgoal_tac "abs(a xa) + abs(b xa) <= 
   1.185 -      max c ca * f xa + max c ca * g xa")
   1.186 -  apply (force)
   1.187 +  apply (subgoal_tac "abs (a xa + b xa) \<le> abs (a xa) + abs (b xa)")
   1.188 +  apply (subgoal_tac "abs (a xa) + abs (b xa) \<le> max c ca * f xa + max c ca * g xa")
   1.189 +  apply force
   1.190    apply (rule add_mono)
   1.191 -  apply (subgoal_tac "c * f xa <= max c ca * f xa")
   1.192 -  apply (force)
   1.193 +  apply (subgoal_tac "c * f xa \<le> max c ca * f xa")
   1.194 +  apply force
   1.195    apply (rule mult_right_mono)
   1.196    apply (rule max.cobounded1)
   1.197    apply assumption
   1.198 -  apply (subgoal_tac "ca * g xa <= max c ca * g xa")
   1.199 -  apply (force)
   1.200 +  apply (subgoal_tac "ca * g xa \<le> max c ca * g xa")
   1.201 +  apply force
   1.202    apply (rule mult_right_mono)
   1.203    apply (rule max.cobounded2)
   1.204    apply assumption
   1.205 @@ -196,8 +188,7 @@
   1.206    apply assumption+
   1.207    done
   1.208  
   1.209 -lemma bigo_bounded_alt: "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> 
   1.210 -    f : O(g)" 
   1.211 +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.212    apply (auto simp add: bigo_def)
   1.213    apply (rule_tac x = "abs c" in exI)
   1.214    apply auto
   1.215 @@ -205,14 +196,12 @@
   1.216    apply (simp add: abs_mult [symmetric])
   1.217    done
   1.218  
   1.219 -lemma bigo_bounded: "ALL x. 0 <= f x ==> ALL x. f x <= g x ==> 
   1.220 -    f : O(g)" 
   1.221 +lemma bigo_bounded: "\<forall>x. 0 \<le> f x \<Longrightarrow> \<forall>x. f x \<le> g x \<Longrightarrow> f \<in> O(g)"
   1.222    apply (erule bigo_bounded_alt [of f 1 g])
   1.223    apply simp
   1.224    done
   1.225  
   1.226 -lemma bigo_bounded2: "ALL x. lb x <= f x ==> ALL x. f x <= lb x + g x ==>
   1.227 -    f : lb +o O(g)"
   1.228 +lemma bigo_bounded2: "\<forall>x. lb x \<le> f x \<Longrightarrow> \<forall>x. f x \<le> lb x + g x \<Longrightarrow> f \<in> lb +o O(g)"
   1.229    apply (rule set_minus_imp_plus)
   1.230    apply (rule bigo_bounded)
   1.231    apply (auto simp add: fun_Compl_def func_plus)
   1.232 @@ -222,21 +211,21 @@
   1.233    apply force
   1.234    done
   1.235  
   1.236 -lemma bigo_abs: "(%x. abs(f x)) =o O(f)" 
   1.237 +lemma bigo_abs: "(\<lambda>x. abs (f x)) =o O(f)"
   1.238    apply (unfold bigo_def)
   1.239    apply auto
   1.240    apply (rule_tac x = 1 in exI)
   1.241    apply auto
   1.242    done
   1.243  
   1.244 -lemma bigo_abs2: "f =o O(%x. abs(f x))"
   1.245 +lemma bigo_abs2: "f =o O(\<lambda>x. abs (f x))"
   1.246    apply (unfold bigo_def)
   1.247    apply auto
   1.248    apply (rule_tac x = 1 in exI)
   1.249    apply auto
   1.250    done
   1.251  
   1.252 -lemma bigo_abs3: "O(f) = O(%x. abs(f x))"
   1.253 +lemma bigo_abs3: "O(f) = O(\<lambda>x. abs (f x))"
   1.254    apply (rule equalityI)
   1.255    apply (rule bigo_elt_subset)
   1.256    apply (rule bigo_abs2)
   1.257 @@ -244,65 +233,63 @@
   1.258    apply (rule bigo_abs)
   1.259    done
   1.260  
   1.261 -lemma bigo_abs4: "f =o g +o O(h) ==> 
   1.262 -    (%x. abs (f x)) =o (%x. abs (g x)) +o O(h)"
   1.263 +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.264    apply (drule set_plus_imp_minus)
   1.265    apply (rule set_minus_imp_plus)
   1.266    apply (subst fun_diff_def)
   1.267  proof -
   1.268 -  assume a: "f - g : O(h)"
   1.269 -  have "(%x. abs (f x) - abs (g x)) =o O(%x. abs(abs (f x) - abs (g x)))"
   1.270 +  assume a: "f - g \<in> O(h)"
   1.271 +  have "(\<lambda>x. abs (f x) - abs (g x)) =o O(\<lambda>x. abs (abs (f x) - abs (g x)))"
   1.272      by (rule bigo_abs2)
   1.273 -  also have "... <= O(%x. abs (f x - g x))"
   1.274 +  also have "\<dots> \<subseteq> O(\<lambda>x. abs (f x - g x))"
   1.275      apply (rule bigo_elt_subset)
   1.276      apply (rule bigo_bounded)
   1.277      apply force
   1.278      apply (rule allI)
   1.279      apply (rule abs_triangle_ineq3)
   1.280      done
   1.281 -  also have "... <= O(f - g)"
   1.282 +  also have "\<dots> \<subseteq> O(f - g)"
   1.283      apply (rule bigo_elt_subset)
   1.284      apply (subst fun_diff_def)
   1.285      apply (rule bigo_abs)
   1.286      done
   1.287 -  also from a have "... <= O(h)"
   1.288 +  also from a have "\<dots> \<subseteq> O(h)"
   1.289      by (rule bigo_elt_subset)
   1.290 -  finally show "(%x. abs (f x) - abs (g x)) : O(h)".
   1.291 +  finally show "(\<lambda>x. abs (f x) - abs (g x)) \<in> O(h)".
   1.292  qed
   1.293  
   1.294 -lemma bigo_abs5: "f =o O(g) ==> (%x. abs(f x)) =o O(g)" 
   1.295 +lemma bigo_abs5: "f =o O(g) \<Longrightarrow> (\<lambda>x. abs (f x)) =o O(g)"
   1.296    by (unfold bigo_def, auto)
   1.297  
   1.298 -lemma bigo_elt_subset2 [intro]: "f : g +o O(h) ==> O(f) <= O(g) + O(h)"
   1.299 +lemma bigo_elt_subset2 [intro]: "f \<in> g +o O(h) \<Longrightarrow> O(f) \<subseteq> O(g) + O(h)"
   1.300  proof -
   1.301 -  assume "f : g +o O(h)"
   1.302 -  also have "... <= O(g) + O(h)"
   1.303 +  assume "f \<in> g +o O(h)"
   1.304 +  also have "\<dots> \<subseteq> O(g) + O(h)"
   1.305      by (auto del: subsetI)
   1.306 -  also have "... = O(%x. abs(g x)) + O(%x. abs(h x))"
   1.307 +  also have "\<dots> = O(\<lambda>x. abs (g x)) + O(\<lambda>x. abs (h x))"
   1.308      apply (subst bigo_abs3 [symmetric])+
   1.309      apply (rule refl)
   1.310      done
   1.311 -  also have "... = O((%x. abs(g x)) + (%x. abs(h x)))"
   1.312 -    by (rule bigo_plus_eq [symmetric], auto)
   1.313 -  finally have "f : ...".
   1.314 -  then have "O(f) <= ..."
   1.315 +  also have "\<dots> = O((\<lambda>x. abs (g x)) + (\<lambda>x. abs (h x)))"
   1.316 +    by (rule bigo_plus_eq [symmetric]) auto
   1.317 +  finally have "f \<in> \<dots>" .
   1.318 +  then have "O(f) \<subseteq> \<dots>"
   1.319      by (elim bigo_elt_subset)
   1.320 -  also have "... = O(%x. abs(g x)) + O(%x. abs(h x))"
   1.321 +  also have "\<dots> = O(\<lambda>x. abs (g x)) + O(\<lambda>x. abs (h x))"
   1.322      by (rule bigo_plus_eq, auto)
   1.323    finally show ?thesis
   1.324      by (simp add: bigo_abs3 [symmetric])
   1.325  qed
   1.326  
   1.327 -lemma bigo_mult [intro]: "O(f)*O(g) <= O(f * g)"
   1.328 +lemma bigo_mult [intro]: "O(f)*O(g) \<subseteq> O(f * g)"
   1.329    apply (rule subsetI)
   1.330    apply (subst bigo_def)
   1.331    apply (auto simp add: bigo_alt_def set_times_def func_times)
   1.332    apply (rule_tac x = "c * ca" in exI)
   1.333 -  apply(rule allI)
   1.334 -  apply(erule_tac x = x in allE)+
   1.335 -  apply(subgoal_tac "c * ca * abs(f x * g x) = 
   1.336 -      (c * abs(f x)) * (ca * abs(g x))")
   1.337 -  apply(erule ssubst)
   1.338 +  apply (rule allI)
   1.339 +  apply (erule_tac x = x in allE)+
   1.340 +  apply (subgoal_tac "c * ca * abs (f x * g x) = (c * abs (f x)) * (ca * abs (g x))")
   1.341 +  apply (erule ssubst)
   1.342    apply (subst abs_mult)
   1.343    apply (rule mult_mono)
   1.344    apply assumption+
   1.345 @@ -311,24 +298,24 @@
   1.346    apply (simp add: mult_ac abs_mult)
   1.347    done
   1.348  
   1.349 -lemma bigo_mult2 [intro]: "f *o O(g) <= O(f * g)"
   1.350 +lemma bigo_mult2 [intro]: "f *o O(g) \<subseteq> O(f * g)"
   1.351    apply (auto simp add: bigo_def elt_set_times_def func_times abs_mult)
   1.352    apply (rule_tac x = c in exI)
   1.353    apply auto
   1.354    apply (drule_tac x = x in spec)
   1.355 -  apply (subgoal_tac "abs(f x) * abs(b x) <= abs(f x) * (c * abs(g x))")
   1.356 +  apply (subgoal_tac "abs (f x) * abs (b x) \<le> abs (f x) * (c * abs (g x))")
   1.357    apply (force simp add: mult_ac)
   1.358    apply (rule mult_left_mono, assumption)
   1.359    apply (rule abs_ge_zero)
   1.360    done
   1.361  
   1.362 -lemma bigo_mult3: "f : O(h) ==> g : O(j) ==> f * g : O(h * j)"
   1.363 +lemma bigo_mult3: "f \<in> O(h) \<Longrightarrow> g \<in> O(j) \<Longrightarrow> f * g \<in> O(h * j)"
   1.364    apply (rule subsetD)
   1.365    apply (rule bigo_mult)
   1.366    apply (erule set_times_intro, assumption)
   1.367    done
   1.368  
   1.369 -lemma bigo_mult4 [intro]:"f : k +o O(h) ==> g * f : (g * k) +o O(g * h)"
   1.370 +lemma bigo_mult4 [intro]: "f \<in> k +o O(h) \<Longrightarrow> g * f \<in> (g * k) +o O(g * h)"
   1.371    apply (drule set_plus_imp_minus)
   1.372    apply (rule set_minus_imp_plus)
   1.373    apply (drule bigo_mult3 [where g = g and j = g])
   1.374 @@ -336,110 +323,117 @@
   1.375    done
   1.376  
   1.377  lemma bigo_mult5:
   1.378 -  assumes "ALL x. f x ~= 0"
   1.379 -  shows "O(f * g) <= (f::'a => ('b::linordered_field)) *o O(g)"
   1.380 +  fixes f :: "'a \<Rightarrow> 'b::linordered_field"
   1.381 +  assumes "\<forall>x. f x \<noteq> 0"
   1.382 +  shows "O(f * g) \<subseteq> f *o O(g)"
   1.383  proof
   1.384    fix h
   1.385 -  assume "h : O(f * g)"
   1.386 -  then have "(%x. 1 / (f x)) * h : (%x. 1 / f x) *o O(f * g)"
   1.387 +  assume "h \<in> O(f * g)"
   1.388 +  then have "(\<lambda>x. 1 / (f x)) * h \<in> (\<lambda>x. 1 / f x) *o O(f * g)"
   1.389      by auto
   1.390 -  also have "... <= O((%x. 1 / f x) * (f * g))"
   1.391 +  also have "\<dots> \<subseteq> O((\<lambda>x. 1 / f x) * (f * g))"
   1.392      by (rule bigo_mult2)
   1.393 -  also have "(%x. 1 / f x) * (f * g) = g"
   1.394 -    apply (simp add: func_times) 
   1.395 +  also have "(\<lambda>x. 1 / f x) * (f * g) = g"
   1.396 +    apply (simp add: func_times)
   1.397      apply (rule ext)
   1.398      apply (simp add: assms nonzero_divide_eq_eq mult_ac)
   1.399      done
   1.400 -  finally have "(%x. (1::'b) / f x) * h : O(g)" .
   1.401 -  then have "f * ((%x. (1::'b) / f x) * h) : f *o O(g)"
   1.402 +  finally have "(\<lambda>x. (1::'b) / f x) * h \<in> O(g)" .
   1.403 +  then have "f * ((\<lambda>x. (1::'b) / f x) * h) \<in> f *o O(g)"
   1.404      by auto
   1.405 -  also have "f * ((%x. (1::'b) / f x) * h) = h"
   1.406 -    apply (simp add: func_times) 
   1.407 +  also have "f * ((\<lambda>x. (1::'b) / f x) * h) = h"
   1.408 +    apply (simp add: func_times)
   1.409      apply (rule ext)
   1.410      apply (simp add: assms nonzero_divide_eq_eq mult_ac)
   1.411      done
   1.412 -  finally show "h : f *o O(g)" .
   1.413 +  finally show "h \<in> f *o O(g)" .
   1.414  qed
   1.415  
   1.416 -lemma bigo_mult6: "ALL x. f x ~= 0 ==>
   1.417 -    O(f * g) = (f::'a => ('b::linordered_field)) *o O(g)"
   1.418 +lemma bigo_mult6:
   1.419 +  fixes f :: "'a \<Rightarrow> 'b::linordered_field"
   1.420 +  shows "\<forall>x. f x \<noteq> 0 \<Longrightarrow> O(f * g) = f *o O(g)"
   1.421    apply (rule equalityI)
   1.422    apply (erule bigo_mult5)
   1.423    apply (rule bigo_mult2)
   1.424    done
   1.425  
   1.426 -lemma bigo_mult7: "ALL x. f x ~= 0 ==>
   1.427 -    O(f * g) <= O(f::'a => ('b::linordered_field)) * O(g)"
   1.428 +lemma bigo_mult7:
   1.429 +  fixes f :: "'a \<Rightarrow> 'b::linordered_field"
   1.430 +  shows "\<forall>x. f x \<noteq> 0 \<Longrightarrow> O(f * g) \<subseteq> O(f) * O(g)"
   1.431    apply (subst bigo_mult6)
   1.432    apply assumption
   1.433    apply (rule set_times_mono3)
   1.434    apply (rule bigo_refl)
   1.435    done
   1.436  
   1.437 -lemma bigo_mult8: "ALL x. f x ~= 0 ==>
   1.438 -    O(f * g) = O(f::'a => ('b::linordered_field)) * O(g)"
   1.439 +lemma bigo_mult8:
   1.440 +  fixes f :: "'a \<Rightarrow> 'b::linordered_field"
   1.441 +  shows "\<forall>x. f x \<noteq> 0 \<Longrightarrow> O(f * g) = O(f) * O(g)"
   1.442    apply (rule equalityI)
   1.443    apply (erule bigo_mult7)
   1.444    apply (rule bigo_mult)
   1.445    done
   1.446  
   1.447 -lemma bigo_minus [intro]: "f : O(g) ==> - f : O(g)"
   1.448 +lemma bigo_minus [intro]: "f \<in> O(g) \<Longrightarrow> - f \<in> O(g)"
   1.449    by (auto simp add: bigo_def fun_Compl_def)
   1.450  
   1.451 -lemma bigo_minus2: "f : g +o O(h) ==> -f : -g +o O(h)"
   1.452 +lemma bigo_minus2: "f \<in> g +o O(h) \<Longrightarrow> - f \<in> -g +o O(h)"
   1.453    apply (rule set_minus_imp_plus)
   1.454    apply (drule set_plus_imp_minus)
   1.455    apply (drule bigo_minus)
   1.456    apply simp
   1.457    done
   1.458  
   1.459 -lemma bigo_minus3: "O(-f) = O(f)"
   1.460 +lemma bigo_minus3: "O(- f) = O(f)"
   1.461    by (auto simp add: bigo_def fun_Compl_def)
   1.462  
   1.463 -lemma bigo_plus_absorb_lemma1: "f : O(g) ==> f +o O(g) <= O(g)"
   1.464 +lemma bigo_plus_absorb_lemma1: "f \<in> O(g) \<Longrightarrow> f +o O(g) \<subseteq> O(g)"
   1.465  proof -
   1.466 -  assume a: "f : O(g)"
   1.467 -  show "f +o O(g) <= O(g)"
   1.468 +  assume a: "f \<in> O(g)"
   1.469 +  show "f +o O(g) \<subseteq> O(g)"
   1.470    proof -
   1.471 -    have "f : O(f)" by auto
   1.472 -    then have "f +o O(g) <= O(f) + O(g)"
   1.473 +    have "f \<in> O(f)" by auto
   1.474 +    then have "f +o O(g) \<subseteq> O(f) + O(g)"
   1.475        by (auto del: subsetI)
   1.476 -    also have "... <= O(g) + O(g)"
   1.477 +    also have "\<dots> \<subseteq> O(g) + O(g)"
   1.478      proof -
   1.479 -      from a have "O(f) <= O(g)" by (auto del: subsetI)
   1.480 +      from a have "O(f) \<subseteq> O(g)" by (auto del: subsetI)
   1.481        thus ?thesis by (auto del: subsetI)
   1.482      qed
   1.483 -    also have "... <= O(g)" by simp
   1.484 +    also have "\<dots> \<subseteq> O(g)" by simp
   1.485      finally show ?thesis .
   1.486    qed
   1.487  qed
   1.488  
   1.489 -lemma bigo_plus_absorb_lemma2: "f : O(g) ==> O(g) <= f +o O(g)"
   1.490 +lemma bigo_plus_absorb_lemma2: "f \<in> O(g) \<Longrightarrow> O(g) \<subseteq> f +o O(g)"
   1.491  proof -
   1.492 -  assume a: "f : O(g)"
   1.493 -  show "O(g) <= f +o O(g)"
   1.494 +  assume a: "f \<in> O(g)"
   1.495 +  show "O(g) \<subseteq> f +o O(g)"
   1.496    proof -
   1.497 -    from a have "-f : O(g)" by auto
   1.498 -    then have "-f +o O(g) <= O(g)" by (elim bigo_plus_absorb_lemma1)
   1.499 -    then have "f +o (-f +o O(g)) <= f +o O(g)" by auto
   1.500 -    also have "f +o (-f +o O(g)) = O(g)"
   1.501 +    from a have "- f \<in> O(g)"
   1.502 +      by auto
   1.503 +    then have "- f +o O(g) \<subseteq> O(g)"
   1.504 +      by (elim bigo_plus_absorb_lemma1)
   1.505 +    then have "f +o (- f +o O(g)) \<subseteq> f +o O(g)"
   1.506 +      by auto
   1.507 +    also have "f +o (- f +o O(g)) = O(g)"
   1.508        by (simp add: set_plus_rearranges)
   1.509      finally show ?thesis .
   1.510    qed
   1.511  qed
   1.512  
   1.513 -lemma bigo_plus_absorb [simp]: "f : O(g) ==> f +o O(g) = O(g)"
   1.514 +lemma bigo_plus_absorb [simp]: "f \<in> O(g) \<Longrightarrow> f +o O(g) = O(g)"
   1.515    apply (rule equalityI)
   1.516    apply (erule bigo_plus_absorb_lemma1)
   1.517    apply (erule bigo_plus_absorb_lemma2)
   1.518    done
   1.519  
   1.520 -lemma bigo_plus_absorb2 [intro]: "f : O(g) ==> A <= O(g) ==> f +o A <= O(g)"
   1.521 -  apply (subgoal_tac "f +o A <= f +o O(g)")
   1.522 +lemma bigo_plus_absorb2 [intro]: "f \<in> O(g) \<Longrightarrow> A \<subseteq> O(g) \<Longrightarrow> f +o A \<subseteq> O(g)"
   1.523 +  apply (subgoal_tac "f +o A \<subseteq> f +o O(g)")
   1.524    apply force+
   1.525    done
   1.526  
   1.527 -lemma bigo_add_commute_imp: "f : g +o O(h) ==> g : f +o O(h)"
   1.528 +lemma bigo_add_commute_imp: "f \<in> g +o O(h) \<Longrightarrow> g \<in> f +o O(h)"
   1.529    apply (subst set_minus_plus [symmetric])
   1.530    apply (subgoal_tac "g - f = - (f - g)")
   1.531    apply (erule ssubst)
   1.532 @@ -449,63 +443,88 @@
   1.533    apply (simp add: add_ac)
   1.534    done
   1.535  
   1.536 -lemma bigo_add_commute: "(f : g +o O(h)) = (g : f +o O(h))"
   1.537 +lemma bigo_add_commute: "f \<in> g +o O(h) \<longleftrightarrow> g \<in> f +o O(h)"
   1.538    apply (rule iffI)
   1.539    apply (erule bigo_add_commute_imp)+
   1.540    done
   1.541  
   1.542 -lemma bigo_const1: "(%x. c) : O(%x. 1)"
   1.543 +lemma bigo_const1: "(\<lambda>x. c) \<in> O(\<lambda>x. 1)"
   1.544    by (auto simp add: bigo_def mult_ac)
   1.545  
   1.546 -lemma bigo_const2 [intro]: "O(%x. c) <= O(%x. 1)"
   1.547 +lemma bigo_const2 [intro]: "O(\<lambda>x. c) \<subseteq> O(\<lambda>x. 1)"
   1.548    apply (rule bigo_elt_subset)
   1.549    apply (rule bigo_const1)
   1.550    done
   1.551  
   1.552 -lemma bigo_const3: "(c::'a::linordered_field) ~= 0 ==> (%x. 1) : O(%x. c)"
   1.553 +lemma bigo_const3:
   1.554 +  fixes c :: "'a::linordered_field"
   1.555 +  shows "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. 1) \<in> O(\<lambda>x. c)"
   1.556    apply (simp add: bigo_def)
   1.557 -  apply (rule_tac x = "abs(inverse c)" in exI)
   1.558 +  apply (rule_tac x = "abs (inverse c)" in exI)
   1.559    apply (simp add: abs_mult [symmetric])
   1.560    done
   1.561  
   1.562 -lemma bigo_const4: "(c::'a::linordered_field) ~= 0 ==> O(%x. 1) <= O(%x. c)"
   1.563 -  by (rule bigo_elt_subset, rule bigo_const3, assumption)
   1.564 +lemma bigo_const4:
   1.565 +  fixes c :: "'a::linordered_field"
   1.566 +  shows "c \<noteq> 0 \<Longrightarrow> O(\<lambda>x. 1) \<subseteq> O(\<lambda>x. c)"
   1.567 +  apply (rule bigo_elt_subset)
   1.568 +  apply (rule bigo_const3)
   1.569 +  apply assumption
   1.570 +  done
   1.571  
   1.572 -lemma bigo_const [simp]: "(c::'a::linordered_field) ~= 0 ==> 
   1.573 -    O(%x. c) = O(%x. 1)"
   1.574 -  by (rule equalityI, rule bigo_const2, rule bigo_const4, assumption)
   1.575 +lemma bigo_const [simp]:
   1.576 +  fixes c :: "'a::linordered_field"
   1.577 +  shows "c \<noteq> 0 \<Longrightarrow> O(\<lambda>x. c) = O(\<lambda>x. 1)"
   1.578 +  apply (rule equalityI)
   1.579 +  apply (rule bigo_const2)
   1.580 +  apply (rule bigo_const4)
   1.581 +  apply assumption
   1.582 +  done
   1.583  
   1.584 -lemma bigo_const_mult1: "(%x. c * f x) : O(f)"
   1.585 +lemma bigo_const_mult1: "(\<lambda>x. c * f x) \<in> O(f)"
   1.586    apply (simp add: bigo_def)
   1.587 -  apply (rule_tac x = "abs(c)" in exI)
   1.588 +  apply (rule_tac x = "abs c" in exI)
   1.589    apply (auto simp add: abs_mult [symmetric])
   1.590    done
   1.591  
   1.592 -lemma bigo_const_mult2: "O(%x. c * f x) <= O(f)"
   1.593 -  by (rule bigo_elt_subset, rule bigo_const_mult1)
   1.594 +lemma bigo_const_mult2: "O(\<lambda>x. c * f x) \<subseteq> O(f)"
   1.595 +  apply (rule bigo_elt_subset)
   1.596 +  apply (rule bigo_const_mult1)
   1.597 +  done
   1.598  
   1.599 -lemma bigo_const_mult3: "(c::'a::linordered_field) ~= 0 ==> f : O(%x. c * f x)"
   1.600 +lemma bigo_const_mult3:
   1.601 +  fixes c :: "'a::linordered_field"
   1.602 +  shows "c \<noteq> 0 \<Longrightarrow> f \<in> O(\<lambda>x. c * f x)"
   1.603    apply (simp add: bigo_def)
   1.604 -  apply (rule_tac x = "abs(inverse c)" in exI)
   1.605 +  apply (rule_tac x = "abs (inverse c)" in exI)
   1.606    apply (simp add: abs_mult [symmetric] mult_assoc [symmetric])
   1.607    done
   1.608  
   1.609 -lemma bigo_const_mult4: "(c::'a::linordered_field) ~= 0 ==> 
   1.610 -    O(f) <= O(%x. c * f x)"
   1.611 -  by (rule bigo_elt_subset, rule bigo_const_mult3, assumption)
   1.612 +lemma bigo_const_mult4:
   1.613 +  fixes c :: "'a::linordered_field"
   1.614 +  shows "c \<noteq> 0 \<Longrightarrow> O(f) \<subseteq> O(\<lambda>x. c * f x)"
   1.615 +  apply (rule bigo_elt_subset)
   1.616 +  apply (rule bigo_const_mult3)
   1.617 +  apply assumption
   1.618 +  done
   1.619  
   1.620 -lemma bigo_const_mult [simp]: "(c::'a::linordered_field) ~= 0 ==> 
   1.621 -    O(%x. c * f x) = O(f)"
   1.622 -  by (rule equalityI, rule bigo_const_mult2, erule bigo_const_mult4)
   1.623 +lemma bigo_const_mult [simp]:
   1.624 +  fixes c :: "'a::linordered_field"
   1.625 +  shows "c \<noteq> 0 \<Longrightarrow> O(\<lambda>x. c * f x) = O(f)"
   1.626 +  apply (rule equalityI)
   1.627 +  apply (rule bigo_const_mult2)
   1.628 +  apply (erule bigo_const_mult4)
   1.629 +  done
   1.630  
   1.631 -lemma bigo_const_mult5 [simp]: "(c::'a::linordered_field) ~= 0 ==> 
   1.632 -    (%x. c) *o O(f) = O(f)"
   1.633 +lemma bigo_const_mult5 [simp]:
   1.634 +  fixes c :: "'a::linordered_field"
   1.635 +  shows "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. c) *o O(f) = O(f)"
   1.636    apply (auto del: subsetI)
   1.637    apply (rule order_trans)
   1.638    apply (rule bigo_mult2)
   1.639    apply (simp add: func_times)
   1.640    apply (auto intro!: simp add: bigo_def elt_set_times_def func_times)
   1.641 -  apply (rule_tac x = "%y. inverse c * x y" in exI)
   1.642 +  apply (rule_tac x = "\<lambda>y. inverse c * x y" in exI)
   1.643    apply (simp add: mult_assoc [symmetric] abs_mult)
   1.644    apply (rule_tac x = "abs (inverse c) * ca" in exI)
   1.645    apply (rule allI)
   1.646 @@ -515,11 +534,11 @@
   1.647    apply force
   1.648    done
   1.649  
   1.650 -lemma bigo_const_mult6 [intro]: "(%x. c) *o O(f) <= O(f)"
   1.651 +lemma bigo_const_mult6 [intro]: "(\<lambda>x. c) *o O(f) \<subseteq> O(f)"
   1.652    apply (auto intro!: simp add: bigo_def elt_set_times_def func_times)
   1.653 -  apply (rule_tac x = "ca * (abs c)" in exI)
   1.654 +  apply (rule_tac x = "ca * abs c" in exI)
   1.655    apply (rule allI)
   1.656 -  apply (subgoal_tac "ca * abs(c) * abs(f x) = abs(c) * (ca * abs(f x))")
   1.657 +  apply (subgoal_tac "ca * abs c * abs (f x) = abs c * (ca * abs (f x))")
   1.658    apply (erule ssubst)
   1.659    apply (subst abs_mult)
   1.660    apply (rule mult_left_mono)
   1.661 @@ -528,33 +547,34 @@
   1.662    apply(simp add: mult_ac)
   1.663    done
   1.664  
   1.665 -lemma bigo_const_mult7 [intro]: "f =o O(g) ==> (%x. c * f x) =o O(g)"
   1.666 +lemma bigo_const_mult7 [intro]: "f =o O(g) \<Longrightarrow> (\<lambda>x. c * f x) =o O(g)"
   1.667  proof -
   1.668    assume "f =o O(g)"
   1.669 -  then have "(%x. c) * f =o (%x. c) *o O(g)"
   1.670 +  then have "(\<lambda>x. c) * f =o (\<lambda>x. c) *o O(g)"
   1.671      by auto
   1.672 -  also have "(%x. c) * f = (%x. c * f x)"
   1.673 +  also have "(\<lambda>x. c) * f = (\<lambda>x. c * f x)"
   1.674      by (simp add: func_times)
   1.675 -  also have "(%x. c) *o O(g) <= O(g)"
   1.676 +  also have "(\<lambda>x. c) *o O(g) \<subseteq> O(g)"
   1.677      by (auto del: subsetI)
   1.678    finally show ?thesis .
   1.679  qed
   1.680  
   1.681 -lemma bigo_compose1: "f =o O(g) ==> (%x. f(k x)) =o O(%x. g(k x))"
   1.682 -by (unfold bigo_def, auto)
   1.683 +lemma bigo_compose1: "f =o O(g) \<Longrightarrow> (\<lambda>x. f (k x)) =o O(\<lambda>x. g (k x))"
   1.684 +  unfolding bigo_def by auto
   1.685  
   1.686 -lemma bigo_compose2: "f =o g +o O(h) ==> (%x. f(k x)) =o (%x. g(k x)) +o 
   1.687 -    O(%x. h(k x))"
   1.688 +lemma bigo_compose2: "f =o g +o O(h) \<Longrightarrow>
   1.689 +    (\<lambda>x. f (k x)) =o (\<lambda>x. g (k x)) +o O(\<lambda>x. h(k x))"
   1.690    apply (simp only: set_minus_plus [symmetric] fun_Compl_def func_plus)
   1.691 -  apply (drule bigo_compose1) apply (simp add: fun_diff_def)
   1.692 +  apply (drule bigo_compose1)
   1.693 +  apply (simp add: fun_diff_def)
   1.694    done
   1.695  
   1.696  
   1.697  subsection {* Setsum *}
   1.698  
   1.699 -lemma bigo_setsum_main: "ALL x. ALL y : A x. 0 <= h x y ==> 
   1.700 -    EX c. ALL x. ALL y : A x. abs(f x y) <= c * (h x y) ==>
   1.701 -      (%x. SUM y : A x. f x y) =o O(%x. SUM y : A x. h x y)"  
   1.702 +lemma bigo_setsum_main: "\<forall>x. \<forall>y \<in> A x. 0 \<le> h x y \<Longrightarrow>
   1.703 +    \<exists>c. \<forall>x. \<forall>y \<in> A x. abs (f x y) \<le> c * (h x y) \<Longrightarrow>
   1.704 +      (\<lambda>x. \<Sum>y \<in> A x. f x y) =o O(\<lambda>x. \<Sum>y \<in> A x. h x y)"
   1.705    apply (auto simp add: bigo_def)
   1.706    apply (rule_tac x = "abs c" in exI)
   1.707    apply (subst abs_of_nonneg) back back
   1.708 @@ -571,14 +591,14 @@
   1.709    apply assumption+
   1.710    apply (drule bspec)
   1.711    apply assumption+
   1.712 -  apply (rule mult_right_mono) 
   1.713 +  apply (rule mult_right_mono)
   1.714    apply (rule abs_ge_self)
   1.715    apply force
   1.716    done
   1.717  
   1.718 -lemma bigo_setsum1: "ALL x y. 0 <= h x y ==> 
   1.719 -    EX c. ALL x y. abs(f x y) <= c * (h x y) ==>
   1.720 -      (%x. SUM y : A x. f x y) =o O(%x. SUM y : A x. h x y)"
   1.721 +lemma bigo_setsum1: "\<forall>x y. 0 \<le> h x y \<Longrightarrow>
   1.722 +    \<exists>c. \<forall>x y. abs (f x y) \<le> c * h x y \<Longrightarrow>
   1.723 +      (\<lambda>x. \<Sum>y \<in> A x. f x y) =o O(\<lambda>x. \<Sum>y \<in> A x. h x y)"
   1.724    apply (rule bigo_setsum_main)
   1.725    apply force
   1.726    apply clarsimp
   1.727 @@ -586,14 +606,13 @@
   1.728    apply force
   1.729    done
   1.730  
   1.731 -lemma bigo_setsum2: "ALL y. 0 <= h y ==> 
   1.732 -    EX c. ALL y. abs(f y) <= c * (h y) ==>
   1.733 -      (%x. SUM y : A x. f y) =o O(%x. SUM y : A x. h y)"
   1.734 -  by (rule bigo_setsum1, auto)  
   1.735 +lemma bigo_setsum2: "\<forall>y. 0 \<le> h y \<Longrightarrow>
   1.736 +    \<exists>c. \<forall>y. abs (f y) \<le> c * (h y) \<Longrightarrow>
   1.737 +      (\<lambda>x. \<Sum>y \<in> A x. f y) =o O(\<lambda>x. \<Sum>y \<in> A x. h y)"
   1.738 +  by (rule bigo_setsum1) auto
   1.739  
   1.740 -lemma bigo_setsum3: "f =o O(h) ==>
   1.741 -    (%x. SUM y : A x. (l x y) * f(k x y)) =o
   1.742 -      O(%x. SUM y : A x. abs(l x y * h(k x y)))"
   1.743 +lemma bigo_setsum3: "f =o O(h) \<Longrightarrow>
   1.744 +    (\<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.745    apply (rule bigo_setsum1)
   1.746    apply (rule allI)+
   1.747    apply (rule abs_ge_zero)
   1.748 @@ -608,10 +627,10 @@
   1.749    apply (rule abs_ge_zero)
   1.750    done
   1.751  
   1.752 -lemma bigo_setsum4: "f =o g +o O(h) ==>
   1.753 -    (%x. SUM y : A x. l x y * f(k x y)) =o
   1.754 -      (%x. SUM y : A x. l x y * g(k x y)) +o
   1.755 -        O(%x. SUM y : A x. abs(l x y * h(k x y)))"
   1.756 +lemma bigo_setsum4: "f =o g +o O(h) \<Longrightarrow>
   1.757 +    (\<lambda>x. \<Sum>y \<in> A x. l x y * f (k x y)) =o
   1.758 +      (\<lambda>x. \<Sum>y \<in> A x. l x y * g (k x y)) +o
   1.759 +        O(\<lambda>x. \<Sum>y \<in> A x. abs (l x y * h (k x y)))"
   1.760    apply (rule set_minus_imp_plus)
   1.761    apply (subst fun_diff_def)
   1.762    apply (subst setsum_subtractf [symmetric])
   1.763 @@ -621,12 +640,12 @@
   1.764    apply (erule set_plus_imp_minus)
   1.765    done
   1.766  
   1.767 -lemma bigo_setsum5: "f =o O(h) ==> ALL x y. 0 <= l x y ==> 
   1.768 -    ALL x. 0 <= h x ==>
   1.769 -      (%x. SUM y : A x. (l x y) * f(k x y)) =o
   1.770 -        O(%x. SUM y : A x. (l x y) * h(k x y))" 
   1.771 -  apply (subgoal_tac "(%x. SUM y : A x. (l x y) * h(k x y)) = 
   1.772 -      (%x. SUM y : A x. abs((l x y) * h(k x y)))")
   1.773 +lemma bigo_setsum5: "f =o O(h) \<Longrightarrow> \<forall>x y. 0 \<le> l x y \<Longrightarrow>
   1.774 +    \<forall>x. 0 \<le> h x \<Longrightarrow>
   1.775 +      (\<lambda>x. \<Sum>y \<in> A x. l x y * f (k x y)) =o
   1.776 +        O(\<lambda>x. \<Sum>y \<in> A x. l x y * h (k x y))"
   1.777 +  apply (subgoal_tac "(\<lambda>x. \<Sum>y \<in> A x. l x y * h (k x y)) =
   1.778 +      (\<lambda>x. \<Sum>y \<in> A x. abs (l x y * h (k x y)))")
   1.779    apply (erule ssubst)
   1.780    apply (erule bigo_setsum3)
   1.781    apply (rule ext)
   1.782 @@ -636,11 +655,11 @@
   1.783    apply auto
   1.784    done
   1.785  
   1.786 -lemma bigo_setsum6: "f =o g +o O(h) ==> ALL x y. 0 <= l x y ==>
   1.787 -    ALL x. 0 <= h x ==>
   1.788 -      (%x. SUM y : A x. (l x y) * f(k x y)) =o
   1.789 -        (%x. SUM y : A x. (l x y) * g(k x y)) +o
   1.790 -          O(%x. SUM y : A x. (l x y) * h(k x y))" 
   1.791 +lemma bigo_setsum6: "f =o g +o O(h) \<Longrightarrow> \<forall>x y. 0 \<le> l x y \<Longrightarrow>
   1.792 +    \<forall>x. 0 \<le> h x \<Longrightarrow>
   1.793 +      (\<lambda>x. \<Sum>y \<in> A x. l x y * f (k x y)) =o
   1.794 +        (\<lambda>x. \<Sum>y \<in> A x. l x y * g (k x y)) +o
   1.795 +          O(\<lambda>x. \<Sum>y \<in> A x. l x y * h (k x y))"
   1.796    apply (rule set_minus_imp_plus)
   1.797    apply (subst fun_diff_def)
   1.798    apply (subst setsum_subtractf [symmetric])
   1.799 @@ -654,33 +673,32 @@
   1.800  
   1.801  subsection {* Misc useful stuff *}
   1.802  
   1.803 -lemma bigo_useful_intro: "A <= O(f) ==> B <= O(f) ==>
   1.804 -  A + B <= O(f)"
   1.805 +lemma bigo_useful_intro: "A \<subseteq> O(f) \<Longrightarrow> B \<subseteq> O(f) \<Longrightarrow> A + B \<subseteq> O(f)"
   1.806    apply (subst bigo_plus_idemp [symmetric])
   1.807    apply (rule set_plus_mono2)
   1.808    apply assumption+
   1.809    done
   1.810  
   1.811 -lemma bigo_useful_add: "f =o O(h) ==> g =o O(h) ==> f + g =o O(h)"
   1.812 +lemma bigo_useful_add: "f =o O(h) \<Longrightarrow> g =o O(h) \<Longrightarrow> f + g =o O(h)"
   1.813    apply (subst bigo_plus_idemp [symmetric])
   1.814    apply (rule set_plus_intro)
   1.815    apply assumption+
   1.816    done
   1.817 -  
   1.818 -lemma bigo_useful_const_mult: "(c::'a::linordered_field) ~= 0 ==> 
   1.819 -    (%x. c) * f =o O(h) ==> f =o O(h)"
   1.820 +
   1.821 +lemma bigo_useful_const_mult:
   1.822 +  fixes c :: "'a::linordered_field"
   1.823 +  shows "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. c) * f =o O(h) \<Longrightarrow> f =o O(h)"
   1.824    apply (rule subsetD)
   1.825 -  apply (subgoal_tac "(%x. 1 / c) *o O(h) <= O(h)")
   1.826 +  apply (subgoal_tac "(\<lambda>x. 1 / c) *o O(h) \<subseteq> O(h)")
   1.827    apply assumption
   1.828    apply (rule bigo_const_mult6)
   1.829 -  apply (subgoal_tac "f = (%x. 1 / c) * ((%x. c) * f)")
   1.830 +  apply (subgoal_tac "f = (\<lambda>x. 1 / c) * ((\<lambda>x. c) * f)")
   1.831    apply (erule ssubst)
   1.832    apply (erule set_times_intro2)
   1.833    apply (simp add: func_times)
   1.834    done
   1.835  
   1.836 -lemma bigo_fix: "(%x. f ((x::nat) + 1)) =o O(%x. h(x + 1)) ==> f 0 = 0 ==>
   1.837 -    f =o O(h)"
   1.838 +lemma bigo_fix: "(\<lambda>x::nat. f (x + 1)) =o O(\<lambda>x. h (x + 1)) \<Longrightarrow> f 0 = 0 \<Longrightarrow> f =o O(h)"
   1.839    apply (simp add: bigo_alt_def)
   1.840    apply auto
   1.841    apply (rule_tac x = c in exI)
   1.842 @@ -696,9 +714,9 @@
   1.843    apply simp
   1.844    done
   1.845  
   1.846 -lemma bigo_fix2: 
   1.847 -    "(%x. f ((x::nat) + 1)) =o (%x. g(x + 1)) +o O(%x. h(x + 1)) ==> 
   1.848 -       f 0 = g 0 ==> f =o g +o O(h)"
   1.849 +lemma bigo_fix2:
   1.850 +    "(\<lambda>x. f ((x::nat) + 1)) =o (\<lambda>x. g(x + 1)) +o O(\<lambda>x. h(x + 1)) \<Longrightarrow>
   1.851 +       f 0 = g 0 \<Longrightarrow> f =o g +o O(h)"
   1.852    apply (rule set_minus_imp_plus)
   1.853    apply (rule bigo_fix)
   1.854    apply (subst fun_diff_def)
   1.855 @@ -711,13 +729,10 @@
   1.856  
   1.857  subsection {* Less than or equal to *}
   1.858  
   1.859 -definition
   1.860 -  lesso :: "('a => 'b::linordered_idom) => ('a => 'b) => ('a => 'b)"
   1.861 -    (infixl "<o" 70) where
   1.862 -  "f <o g = (%x. max (f x - g x) 0)"
   1.863 +definition lesso :: "('a \<Rightarrow> 'b::linordered_idom) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"  (infixl "<o" 70)
   1.864 +  where "f <o g = (\<lambda>x. max (f x - g x) 0)"
   1.865  
   1.866 -lemma bigo_lesseq1: "f =o O(h) ==> ALL x. abs (g x) <= abs (f x) ==>
   1.867 -    g =o O(h)"
   1.868 +lemma bigo_lesseq1: "f =o O(h) \<Longrightarrow> \<forall>x. abs (g x) \<le> abs (f x) \<Longrightarrow> g =o O(h)"
   1.869    apply (unfold bigo_def)
   1.870    apply clarsimp
   1.871    apply (rule_tac x = c in exI)
   1.872 @@ -726,8 +741,7 @@
   1.873    apply (erule spec)+
   1.874    done
   1.875  
   1.876 -lemma bigo_lesseq2: "f =o O(h) ==> ALL x. abs (g x) <= f x ==>
   1.877 -      g =o O(h)"
   1.878 +lemma bigo_lesseq2: "f =o O(h) \<Longrightarrow> \<forall>x. abs (g x) \<le> f x \<Longrightarrow> g =o O(h)"
   1.879    apply (erule bigo_lesseq1)
   1.880    apply (rule allI)
   1.881    apply (drule_tac x = x in spec)
   1.882 @@ -736,26 +750,24 @@
   1.883    apply (rule abs_ge_self)
   1.884    done
   1.885  
   1.886 -lemma bigo_lesseq3: "f =o O(h) ==> ALL x. 0 <= g x ==> ALL x. g x <= f x ==>
   1.887 -    g =o O(h)"
   1.888 +lemma bigo_lesseq3: "f =o O(h) \<Longrightarrow> \<forall>x. 0 \<le> g x \<Longrightarrow> \<forall>x. g x \<le> f x \<Longrightarrow> g =o O(h)"
   1.889    apply (erule bigo_lesseq2)
   1.890    apply (rule allI)
   1.891    apply (subst abs_of_nonneg)
   1.892    apply (erule spec)+
   1.893    done
   1.894  
   1.895 -lemma bigo_lesseq4: "f =o O(h) ==>
   1.896 -    ALL x. 0 <= g x ==> ALL x. g x <= abs (f x) ==>
   1.897 -      g =o O(h)"
   1.898 +lemma bigo_lesseq4: "f =o O(h) \<Longrightarrow>
   1.899 +    \<forall>x. 0 \<le> g x \<Longrightarrow> \<forall>x. g x \<le> abs (f x) \<Longrightarrow> g =o O(h)"
   1.900    apply (erule bigo_lesseq1)
   1.901    apply (rule allI)
   1.902    apply (subst abs_of_nonneg)
   1.903    apply (erule spec)+
   1.904    done
   1.905  
   1.906 -lemma bigo_lesso1: "ALL x. f x <= g x ==> f <o g =o O(h)"
   1.907 +lemma bigo_lesso1: "\<forall>x. f x \<le> g x \<Longrightarrow> f <o g =o O(h)"
   1.908    apply (unfold lesso_def)
   1.909 -  apply (subgoal_tac "(%x. max (f x - g x) 0) = 0")
   1.910 +  apply (subgoal_tac "(\<lambda>x. max (f x - g x) 0) = 0")
   1.911    apply (erule ssubst)
   1.912    apply (rule bigo_zero)
   1.913    apply (unfold func_zero)
   1.914 @@ -763,9 +775,8 @@
   1.915    apply (simp split: split_max)
   1.916    done
   1.917  
   1.918 -lemma bigo_lesso2: "f =o g +o O(h) ==>
   1.919 -    ALL x. 0 <= k x ==> ALL x. k x <= f x ==>
   1.920 -      k <o g =o O(h)"
   1.921 +lemma bigo_lesso2: "f =o g +o O(h) \<Longrightarrow>
   1.922 +    \<forall>x. 0 \<le> k x \<Longrightarrow> \<forall>x. k x \<le> f x \<Longrightarrow> k <o g =o O(h)"
   1.923    apply (unfold lesso_def)
   1.924    apply (rule bigo_lesseq4)
   1.925    apply (erule set_plus_imp_minus)
   1.926 @@ -773,7 +784,7 @@
   1.927    apply (rule max.cobounded2)
   1.928    apply (rule allI)
   1.929    apply (subst fun_diff_def)
   1.930 -  apply (case_tac "0 <= k x - g x")
   1.931 +  apply (case_tac "0 \<le> k x - g x")
   1.932    apply simp
   1.933    apply (subst abs_of_nonneg)
   1.934    apply (drule_tac x = x in spec) back
   1.935 @@ -781,15 +792,14 @@
   1.936    apply (subst diff_conv_add_uminus)+
   1.937    apply (rule add_right_mono)
   1.938    apply (erule spec)
   1.939 -  apply (rule order_trans) 
   1.940 +  apply (rule order_trans)
   1.941    prefer 2
   1.942    apply (rule abs_ge_zero)
   1.943    apply (simp add: algebra_simps)
   1.944    done
   1.945  
   1.946 -lemma bigo_lesso3: "f =o g +o O(h) ==>
   1.947 -    ALL x. 0 <= k x ==> ALL x. g x <= k x ==>
   1.948 -      f <o k =o O(h)"
   1.949 +lemma bigo_lesso3: "f =o g +o O(h) \<Longrightarrow>
   1.950 +    \<forall>x. 0 \<le> k x \<Longrightarrow> \<forall>x. g x \<le> k x \<Longrightarrow> f <o k =o O(h)"
   1.951    apply (unfold lesso_def)
   1.952    apply (rule bigo_lesseq4)
   1.953    apply (erule set_plus_imp_minus)
   1.954 @@ -797,7 +807,7 @@
   1.955    apply (rule max.cobounded2)
   1.956    apply (rule allI)
   1.957    apply (subst fun_diff_def)
   1.958 -  apply (case_tac "0 <= f x - k x")
   1.959 +  apply (case_tac "0 \<le> f x - k x")
   1.960    apply simp
   1.961    apply (subst abs_of_nonneg)
   1.962    apply (drule_tac x = x in spec) back
   1.963 @@ -806,14 +816,15 @@
   1.964    apply (rule add_left_mono)
   1.965    apply (rule le_imp_neg_le)
   1.966    apply (erule spec)
   1.967 -  apply (rule order_trans) 
   1.968 +  apply (rule order_trans)
   1.969    prefer 2
   1.970    apply (rule abs_ge_zero)
   1.971    apply (simp add: algebra_simps)
   1.972    done
   1.973  
   1.974 -lemma bigo_lesso4: "f <o g =o O(k::'a=>'b::linordered_field) ==>
   1.975 -    g =o h +o O(k) ==> f <o h =o O(k)"
   1.976 +lemma bigo_lesso4:
   1.977 +  fixes k :: "'a \<Rightarrow> 'b::linordered_field"
   1.978 +  shows "f <o g =o O(k) \<Longrightarrow> g =o h +o O(k) \<Longrightarrow> f <o h =o O(k)"
   1.979    apply (unfold lesso_def)
   1.980    apply (drule set_plus_imp_minus)
   1.981    apply (drule bigo_abs5) back
   1.982 @@ -822,25 +833,22 @@
   1.983    apply assumption
   1.984    apply (erule bigo_lesseq2) back
   1.985    apply (rule allI)
   1.986 -  apply (auto simp add: func_plus fun_diff_def algebra_simps
   1.987 -    split: split_max abs_split)
   1.988 +  apply (auto simp add: func_plus fun_diff_def algebra_simps split: split_max abs_split)
   1.989    done
   1.990  
   1.991 -lemma bigo_lesso5: "f <o g =o O(h) ==>
   1.992 -    EX C. ALL x. f x <= g x + C * abs(h x)"
   1.993 +lemma bigo_lesso5: "f <o g =o O(h) \<Longrightarrow> \<exists>C. \<forall>x. f x \<le> g x + C * abs (h x)"
   1.994    apply (simp only: lesso_def bigo_alt_def)
   1.995    apply clarsimp
   1.996    apply (rule_tac x = c in exI)
   1.997    apply (rule allI)
   1.998    apply (drule_tac x = x in spec)
   1.999 -  apply (subgoal_tac "abs(max (f x - g x) 0) = max (f x - g x) 0")
  1.1000 -  apply (clarsimp simp add: algebra_simps) 
  1.1001 +  apply (subgoal_tac "abs (max (f x - g x) 0) = max (f x - g x) 0")
  1.1002 +  apply (clarsimp simp add: algebra_simps)
  1.1003    apply (rule abs_of_nonneg)
  1.1004    apply (rule max.cobounded2)
  1.1005    done
  1.1006  
  1.1007 -lemma lesso_add: "f <o g =o O(h) ==>
  1.1008 -      k <o l =o O(h) ==> (f + k) <o (g + l) =o O(h)"
  1.1009 +lemma lesso_add: "f <o g =o O(h) \<Longrightarrow> k <o l =o O(h) \<Longrightarrow> (f + k) <o (g + l) =o O(h)"
  1.1010    apply (unfold lesso_def)
  1.1011    apply (rule bigo_lesseq3)
  1.1012    apply (erule bigo_useful_add)
  1.1013 @@ -849,7 +857,7 @@
  1.1014    apply (auto split: split_max simp add: func_plus)
  1.1015    done
  1.1016  
  1.1017 -lemma bigo_LIMSEQ1: "f =o O(g) ==> g ----> 0 ==> f ----> (0::real)"
  1.1018 +lemma bigo_LIMSEQ1: "f =o O(g) \<Longrightarrow> g ----> 0 \<Longrightarrow> f ----> (0::real)"
  1.1019    apply (simp add: LIMSEQ_iff bigo_alt_def)
  1.1020    apply clarify
  1.1021    apply (drule_tac x = "r / c" in spec)
  1.1022 @@ -866,21 +874,20 @@
  1.1023    apply (rule order_le_less_trans)
  1.1024    apply assumption
  1.1025    apply (rule order_less_le_trans)
  1.1026 -  apply (subgoal_tac "c * abs(g n) < c * (r / c)")
  1.1027 +  apply (subgoal_tac "c * abs (g n) < c * (r / c)")
  1.1028    apply assumption
  1.1029    apply (erule mult_strict_left_mono)
  1.1030    apply assumption
  1.1031    apply simp
  1.1032 -done
  1.1033 +  done
  1.1034  
  1.1035 -lemma bigo_LIMSEQ2: "f =o g +o O(h) ==> h ----> 0 ==> f ----> a 
  1.1036 -    ==> g ----> (a::real)"
  1.1037 +lemma bigo_LIMSEQ2: "f =o g +o O(h) \<Longrightarrow> h ----> 0 \<Longrightarrow> f ----> a \<Longrightarrow> g ----> (a::real)"
  1.1038    apply (drule set_plus_imp_minus)
  1.1039    apply (drule bigo_LIMSEQ1)
  1.1040    apply assumption
  1.1041    apply (simp only: fun_diff_def)
  1.1042    apply (erule LIMSEQ_diff_approach_zero2)
  1.1043    apply assumption
  1.1044 -done
  1.1045 +  done
  1.1046  
  1.1047  end