src/HOL/Library/BigO.thy
changeset 16908 d374530bfaaa
child 16932 0bca871f5a21
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/BigO.thy	Mon Jul 25 18:54:49 2005 +0200
     1.3 @@ -0,0 +1,916 @@
     1.4 +(*  Title:      BigO.thy
     1.5 +    Authors:    Jeremy Avigad and Kevin Donnelly
     1.6 +*)
     1.7 +
     1.8 +header {* Big O notation *}
     1.9 +
    1.10 +theory BigO
    1.11 +imports SetsAndFunctions
    1.12 +begin
    1.13 +
    1.14 +text {*
    1.15 +This library is designed to support asymptotic ``big O'' calculations,
    1.16 +i.e.~reasoning with expressions of the form $f = O(g)$ and $f = g + O(h)$.
    1.17 +An earlier version of this library is described in detail in
    1.18 +\begin{quote}
    1.19 +Avigad, Jeremy, and Kevin Donnelly, \emph{Formalizing O notation in 
    1.20 +Isabelle/HOL}, in David Basin and Micha\"el Rusiowitch, editors, 
    1.21 +\emph{Automated Reasoning: second international conference, IJCAR 2004}, 
    1.22 +Springer, 357--371, 2004.
    1.23 +\end{quote}
    1.24 +The main changes in this version are as follows:
    1.25 +\begin{itemize}
    1.26 +\item We have eliminated the $O$ operator on sets. (Most uses of this seem
    1.27 +  to be inessential.)
    1.28 +\item We no longer use $+$ as output syntax for $+o$.
    1.29 +\item Lemmas involving ``sumr-pos'' have been replaced by more
    1.30 +  general lemmas involving ``setsum''.
    1.31 +\item The library has been expanded, with e.g.~support for expressions of
    1.32 +  the form $f < g + O(h)$.
    1.33 +\end{itemize}
    1.34 +Note that two lemmas at the end of this file are commented out, as they 
    1.35 +require the HOL-Complex library.
    1.36 +
    1.37 +Note also since the Big O library includes rules that demonstrate set 
    1.38 +inclusion, to use the automated reasoners effectively with the library one 
    1.39 +should redeclare the theorem ``subsetI'' as an intro rule, rather than as 
    1.40 +an intro! rule, for example, using ``declare subsetI [del, intro]''.
    1.41 +*}
    1.42 +
    1.43 +subsection {* Definitions *}
    1.44 +
    1.45 +constdefs 
    1.46 +
    1.47 +  bigo :: "('a => 'b::ordered_idom) => ('a => 'b) set"    ("(1O'(_'))")
    1.48 +  "O(f::('a => 'b)) == 
    1.49 +      {h. EX c. ALL x. abs (h x) <= c * abs (f x)}"
    1.50 +
    1.51 +lemma bigo_pos_const: "(EX (c::'a::ordered_idom). 
    1.52 +    ALL x. (abs (h x)) <= (c * (abs (f x))))
    1.53 +      = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
    1.54 +  apply auto
    1.55 +  apply (case_tac "c = 0")
    1.56 +  apply simp
    1.57 +  apply (rule_tac x = "1" in exI)
    1.58 +  apply simp
    1.59 +  apply (rule_tac x = "abs c" in exI)
    1.60 +  apply auto
    1.61 +  apply (subgoal_tac "c * abs(f x) <= abs c * abs (f x)")
    1.62 +  apply (erule_tac x = x in allE)
    1.63 +  apply force
    1.64 +  apply (rule mult_right_mono)
    1.65 +  apply (rule abs_ge_self)
    1.66 +  apply (rule abs_ge_zero)
    1.67 +done
    1.68 +
    1.69 +lemma bigo_alt_def: "O(f) = 
    1.70 +    {h. EX c. (0 < c & (ALL x. abs (h x) <= c * abs (f x)))}"
    1.71 +by (auto simp add: bigo_def bigo_pos_const)
    1.72 +
    1.73 +lemma bigo_elt_subset [intro]: "f : O(g) ==> O(f) <= O(g)"
    1.74 +  apply (auto simp add: bigo_alt_def)
    1.75 +  apply (rule_tac x = "ca * c" in exI)
    1.76 +  apply (rule conjI)
    1.77 +  apply (rule mult_pos_pos)
    1.78 +  apply (assumption)+
    1.79 +  apply (rule allI)
    1.80 +  apply (drule_tac x = "xa" in spec)+
    1.81 +  apply (subgoal_tac "ca * abs(f xa) <= ca * (c * abs(g xa))")
    1.82 +  apply (erule order_trans)
    1.83 +  apply (simp add: mult_ac)
    1.84 +  apply (rule mult_left_mono, assumption)
    1.85 +  apply (rule order_less_imp_le, assumption)
    1.86 +done
    1.87 +
    1.88 +lemma bigo_refl [intro]: "f : O(f)"
    1.89 +  apply(auto simp add: bigo_def)
    1.90 +  apply(rule_tac x = 1 in exI)
    1.91 +  apply simp
    1.92 +done
    1.93 +
    1.94 +lemma bigo_zero: "0 : O(g)"
    1.95 +  apply (auto simp add: bigo_def func_zero)
    1.96 +  apply (rule_tac x = 0 in exI)
    1.97 +  apply auto
    1.98 +done
    1.99 +
   1.100 +lemma bigo_zero2: "O(%x.0) = {%x.0}"
   1.101 +  apply (auto simp add: bigo_def) 
   1.102 +  apply (rule ext)
   1.103 +  apply auto
   1.104 +done
   1.105 +
   1.106 +lemma bigo_plus_self_subset [intro]: 
   1.107 +  "O(f) + O(f) <= O(f)"
   1.108 +  apply (auto simp add: bigo_alt_def set_plus)
   1.109 +  apply (rule_tac x = "c + ca" in exI)
   1.110 +  apply auto
   1.111 +  apply (simp add: ring_distrib func_plus)
   1.112 +  apply (rule order_trans)
   1.113 +  apply (rule abs_triangle_ineq)
   1.114 +  apply (rule add_mono)
   1.115 +  apply force
   1.116 +  apply force
   1.117 +done
   1.118 +
   1.119 +lemma bigo_plus_idemp [simp]: "O(f) + O(f) = O(f)"
   1.120 +  apply (rule equalityI)
   1.121 +  apply (rule bigo_plus_self_subset)
   1.122 +  apply (rule set_zero_plus2) 
   1.123 +  apply (rule bigo_zero)
   1.124 +done
   1.125 +
   1.126 +lemma bigo_plus_subset [intro]: "O(f + g) <= O(f) + O(g)"
   1.127 +  apply (rule subsetI)
   1.128 +  apply (auto simp add: bigo_def bigo_pos_const func_plus set_plus)
   1.129 +  apply (subst bigo_pos_const [symmetric])+
   1.130 +  apply (rule_tac x = 
   1.131 +    "%n. if abs (g n) <= (abs (f n)) then x n else 0" in exI)
   1.132 +  apply (rule conjI)
   1.133 +  apply (rule_tac x = "c + c" in exI)
   1.134 +  apply (clarsimp)
   1.135 +  apply (auto)
   1.136 +  apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (f xa)")
   1.137 +  apply (erule_tac x = xa in allE)
   1.138 +  apply (erule order_trans)
   1.139 +  apply (simp)
   1.140 +  apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))")
   1.141 +  apply (erule order_trans)
   1.142 +  apply (simp add: ring_distrib)
   1.143 +  apply (rule mult_left_mono)
   1.144 +  apply assumption
   1.145 +  apply (simp add: order_less_le)
   1.146 +  apply (rule mult_left_mono)
   1.147 +  apply (simp add: abs_triangle_ineq)
   1.148 +  apply (simp add: order_less_le)
   1.149 +  apply (rule mult_nonneg_nonneg)
   1.150 +  apply (rule add_nonneg_nonneg)
   1.151 +  apply auto
   1.152 +  apply (rule_tac x = "%n. if (abs (f n)) <  abs (g n) then x n else 0" 
   1.153 +     in exI)
   1.154 +  apply (rule conjI)
   1.155 +  apply (rule_tac x = "c + c" in exI)
   1.156 +  apply auto
   1.157 +  apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (g xa)")
   1.158 +  apply (erule_tac x = xa in allE)
   1.159 +  apply (erule order_trans)
   1.160 +  apply (simp)
   1.161 +  apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))")
   1.162 +  apply (erule order_trans)
   1.163 +  apply (simp add: ring_distrib)
   1.164 +  apply (rule mult_left_mono)
   1.165 +  apply (simp add: order_less_le)
   1.166 +  apply (simp add: order_less_le)
   1.167 +  apply (rule mult_left_mono)
   1.168 +  apply (rule abs_triangle_ineq)
   1.169 +  apply (simp add: order_less_le)
   1.170 +  apply (rule mult_nonneg_nonneg)
   1.171 +  apply (rule add_nonneg_nonneg)
   1.172 +  apply (erule order_less_imp_le)+
   1.173 +  apply simp
   1.174 +  apply (rule ext)
   1.175 +  apply (auto simp add: if_splits linorder_not_le)
   1.176 +done
   1.177 +
   1.178 +lemma bigo_plus_subset2 [intro]: "A <= O(f) ==> B <= O(f) ==> A + B <= O(f)"
   1.179 +  apply (subgoal_tac "A + B <= O(f) + O(f)")
   1.180 +  apply (erule order_trans)
   1.181 +  apply simp
   1.182 +  apply (auto del: subsetI simp del: bigo_plus_idemp)
   1.183 +done
   1.184 +
   1.185 +lemma bigo_plus_eq: "ALL x. 0 <= f x ==> ALL x. 0 <= g x ==> 
   1.186 +  O(f + g) = O(f) + O(g)"
   1.187 +  apply (rule equalityI)
   1.188 +  apply (rule bigo_plus_subset)
   1.189 +  apply (simp add: bigo_alt_def set_plus func_plus)
   1.190 +  apply clarify
   1.191 +  apply (rule_tac x = "max c ca" in exI)
   1.192 +  apply (rule conjI)
   1.193 +  apply (subgoal_tac "c <= max c ca")
   1.194 +  apply (erule order_less_le_trans)
   1.195 +  apply assumption
   1.196 +  apply (rule le_maxI1)
   1.197 +  apply clarify
   1.198 +  apply (drule_tac x = "xa" in spec)+
   1.199 +  apply (subgoal_tac "0 <= f xa + g xa")
   1.200 +  apply (simp add: ring_distrib)
   1.201 +  apply (subgoal_tac "abs(a xa + b xa) <= abs(a xa) + abs(b xa)")
   1.202 +  apply (subgoal_tac "abs(a xa) + abs(b xa) <= 
   1.203 +      max c ca * f xa + max c ca * g xa")
   1.204 +  apply (force)
   1.205 +  apply (rule add_mono)
   1.206 +  apply (subgoal_tac "c * f xa <= max c ca * f xa")
   1.207 +  apply (force)
   1.208 +  apply (rule mult_right_mono)
   1.209 +  apply (rule le_maxI1)
   1.210 +  apply assumption
   1.211 +  apply (subgoal_tac "ca * g xa <= max c ca * g xa")
   1.212 +  apply (force)
   1.213 +  apply (rule mult_right_mono)
   1.214 +  apply (rule le_maxI2)
   1.215 +  apply assumption
   1.216 +  apply (rule abs_triangle_ineq)
   1.217 +  apply (rule add_nonneg_nonneg)
   1.218 +  apply assumption+
   1.219 +done
   1.220 +
   1.221 +lemma bigo_bounded_alt: "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> 
   1.222 +    f : O(g)" 
   1.223 +  apply (auto simp add: bigo_def)
   1.224 +  apply (rule_tac x = "abs c" in exI)
   1.225 +  apply auto
   1.226 +  apply (drule_tac x = x in spec)+
   1.227 +  apply (simp add: abs_mult [symmetric])
   1.228 +done
   1.229 +
   1.230 +lemma bigo_bounded: "ALL x. 0 <= f x ==> ALL x. f x <= g x ==> 
   1.231 +    f : O(g)" 
   1.232 +  apply (erule bigo_bounded_alt [of f 1 g])
   1.233 +  apply simp
   1.234 +done
   1.235 +
   1.236 +lemma bigo_bounded2: "ALL x. lb x <= f x ==> ALL x. f x <= lb x + g x ==>
   1.237 +    f : lb +o O(g)"
   1.238 +  apply (rule set_minus_imp_plus)
   1.239 +  apply (rule bigo_bounded)
   1.240 +  apply (auto simp add: diff_minus func_minus func_plus)
   1.241 +  apply (drule_tac x = x in spec)+
   1.242 +  apply force
   1.243 +  apply (drule_tac x = x in spec)+
   1.244 +  apply force
   1.245 +done
   1.246 +
   1.247 +lemma bigo_abs: "(%x. abs(f x)) =o O(f)" 
   1.248 +  apply (unfold bigo_def)
   1.249 +  apply auto
   1.250 +  apply (rule_tac x = 1 in exI)
   1.251 +  apply auto
   1.252 +done
   1.253 +
   1.254 +lemma bigo_abs2: "f =o O(%x. abs(f x))"
   1.255 +  apply (unfold bigo_def)
   1.256 +  apply auto
   1.257 +  apply (rule_tac x = 1 in exI)
   1.258 +  apply auto
   1.259 +done
   1.260 +
   1.261 +lemma bigo_abs3: "O(f) = O(%x. abs(f x))"
   1.262 +  apply (rule equalityI)
   1.263 +  apply (rule bigo_elt_subset)
   1.264 +  apply (rule bigo_abs2)
   1.265 +  apply (rule bigo_elt_subset)
   1.266 +  apply (rule bigo_abs)
   1.267 +done
   1.268 +
   1.269 +lemma bigo_abs4: "f =o g +o O(h) ==> 
   1.270 +    (%x. abs (f x)) =o (%x. abs (g x)) +o O(h)"
   1.271 +  apply (drule set_plus_imp_minus)
   1.272 +  apply (rule set_minus_imp_plus)
   1.273 +  apply (subst func_diff)
   1.274 +proof -
   1.275 +  assume a: "f - g : O(h)"
   1.276 +  have "(%x. abs (f x) - abs (g x)) =o O(%x. abs(abs (f x) - abs (g x)))"
   1.277 +    by (rule bigo_abs2)
   1.278 +  also have "... <= O(%x. abs (f x - g x))"
   1.279 +    apply (rule bigo_elt_subset)
   1.280 +    apply (rule bigo_bounded)
   1.281 +    apply force
   1.282 +    apply (rule allI)
   1.283 +    apply (rule abs_triangle_ineq3)
   1.284 +    done
   1.285 +  also have "... <= O(f - g)"
   1.286 +    apply (rule bigo_elt_subset)
   1.287 +    apply (subst func_diff)
   1.288 +    apply (rule bigo_abs)
   1.289 +    done
   1.290 +  also have "... <= O(h)"
   1.291 +    by (rule bigo_elt_subset)
   1.292 +  finally show "(%x. abs (f x) - abs (g x)) : O(h)".
   1.293 +qed
   1.294 +
   1.295 +lemma bigo_abs5: "f =o O(g) ==> (%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 +proof -
   1.300 +  assume "f : g +o O(h)"
   1.301 +  also have "... <= O(g) + O(h)"
   1.302 +    by (auto del: subsetI)
   1.303 +  also have "... = O(%x. abs(g x)) + O(%x. abs(h x))"
   1.304 +    apply (subst bigo_abs3 [symmetric])+
   1.305 +    apply (rule refl)
   1.306 +    done
   1.307 +  also have "... = O((%x. abs(g x)) + (%x. abs(h x)))"
   1.308 +    by (rule bigo_plus_eq [symmetric], auto)
   1.309 +  finally have "f : ...".
   1.310 +  then have "O(f) <= ..."
   1.311 +    by (elim bigo_elt_subset)
   1.312 +  also have "... = O(%x. abs(g x)) + O(%x. abs(h x))"
   1.313 +    by (rule bigo_plus_eq, auto)
   1.314 +  finally show ?thesis
   1.315 +    by (simp add: bigo_abs3 [symmetric])
   1.316 +qed
   1.317 +
   1.318 +lemma bigo_mult [intro]: "O(f)*O(g) <= O(f * g)"
   1.319 +  apply (rule subsetI)
   1.320 +  apply (subst bigo_def)
   1.321 +  apply (auto simp add: bigo_alt_def set_times func_times)
   1.322 +  apply (rule_tac x = "c * ca" in exI)
   1.323 +  apply(rule allI)
   1.324 +  apply(erule_tac x = x in allE)+
   1.325 +  apply(subgoal_tac "c * ca * abs(f x * g x) = 
   1.326 +      (c * abs(f x)) * (ca * abs(g x))")
   1.327 +  apply(erule ssubst)
   1.328 +  apply (subst abs_mult)
   1.329 +  apply (rule mult_mono)
   1.330 +  apply assumption+
   1.331 +  apply (rule mult_nonneg_nonneg)
   1.332 +  apply auto
   1.333 +  apply (simp add: mult_ac abs_mult)
   1.334 +done
   1.335 +
   1.336 +lemma bigo_mult2 [intro]: "f *o O(g) <= O(f * g)"
   1.337 +  apply (auto simp add: bigo_def elt_set_times_def func_times abs_mult)
   1.338 +  apply (rule_tac x = c in exI)
   1.339 +  apply auto
   1.340 +  apply (drule_tac x = x in spec)
   1.341 +  apply (subgoal_tac "abs(f x) * abs(b x) <= abs(f x) * (c * abs(g x))")
   1.342 +  apply (force simp add: mult_ac)
   1.343 +  apply (rule mult_left_mono, assumption)
   1.344 +  apply (rule abs_ge_zero)
   1.345 +done
   1.346 +
   1.347 +lemma bigo_mult3: "f : O(h) ==> g : O(j) ==> f * g : O(h * j)"
   1.348 +  apply (rule subsetD)
   1.349 +  apply (rule bigo_mult)
   1.350 +  apply (erule set_times_intro, assumption)
   1.351 +done
   1.352 +
   1.353 +lemma bigo_mult4 [intro]:"f : k +o O(h) ==> g * f : (g * k) +o O(g * h)"
   1.354 +  apply (drule set_plus_imp_minus)
   1.355 +  apply (rule set_minus_imp_plus)
   1.356 +  apply (drule bigo_mult3 [where g = g and j = g])
   1.357 +  apply (auto simp add: ring_eq_simps mult_ac)
   1.358 +done
   1.359 +
   1.360 +lemma bigo_mult5: "ALL x. f x ~= 0 ==>
   1.361 +    O(f * g) <= (f::'a => ('b::ordered_field)) *o O(g)"
   1.362 +proof -
   1.363 +  assume "ALL x. f x ~= 0"
   1.364 +  show "O(f * g) <= f *o O(g)"
   1.365 +  proof
   1.366 +    fix h
   1.367 +    assume "h : O(f * g)"
   1.368 +    then have "(%x. 1 / (f x)) * h : (%x. 1 / f x) *o O(f * g)"
   1.369 +      by auto
   1.370 +    also have "... <= O((%x. 1 / f x) * (f * g))"
   1.371 +      by (rule bigo_mult2)
   1.372 +    also have "(%x. 1 / f x) * (f * g) = g"
   1.373 +      apply (simp add: func_times) 
   1.374 +      apply (rule ext)
   1.375 +      apply (simp add: prems nonzero_divide_eq_eq mult_ac)
   1.376 +      done
   1.377 +    finally have "(%x. (1::'b) / f x) * h : O(g)".
   1.378 +    then have "f * ((%x. (1::'b) / f x) * h) : f *o O(g)"
   1.379 +      by auto
   1.380 +    also have "f * ((%x. (1::'b) / f x) * h) = h"
   1.381 +      apply (simp add: func_times) 
   1.382 +      apply (rule ext)
   1.383 +      apply (simp add: prems nonzero_divide_eq_eq mult_ac)
   1.384 +      done
   1.385 +    finally show "h : f *o O(g)".
   1.386 +  qed
   1.387 +qed
   1.388 +
   1.389 +lemma bigo_mult6: "ALL x. f x ~= 0 ==>
   1.390 +    O(f * g) = (f::'a => ('b::ordered_field)) *o O(g)"
   1.391 +  apply (rule equalityI)
   1.392 +  apply (erule bigo_mult5)
   1.393 +  apply (rule bigo_mult2)
   1.394 +done
   1.395 +
   1.396 +lemma bigo_mult7: "ALL x. f x ~= 0 ==>
   1.397 +    O(f * g) <= O(f::'a => ('b::ordered_field)) * O(g)"
   1.398 +  apply (subst bigo_mult6)
   1.399 +  apply assumption
   1.400 +  apply (rule set_times_mono3)
   1.401 +  apply (rule bigo_refl)
   1.402 +done
   1.403 +
   1.404 +lemma bigo_mult8: "ALL x. f x ~= 0 ==>
   1.405 +    O(f * g) = O(f::'a => ('b::ordered_field)) * O(g)"
   1.406 +  apply (rule equalityI)
   1.407 +  apply (erule bigo_mult7)
   1.408 +  apply (rule bigo_mult)
   1.409 +done
   1.410 +
   1.411 +lemma bigo_minus [intro]: "f : O(g) ==> - f : O(g)"
   1.412 +  by (auto simp add: bigo_def func_minus)
   1.413 +
   1.414 +lemma bigo_minus2: "f : g +o O(h) ==> -f : -g +o O(h)"
   1.415 +  apply (rule set_minus_imp_plus)
   1.416 +  apply (drule set_plus_imp_minus)
   1.417 +  apply (drule bigo_minus)
   1.418 +  apply (simp add: diff_minus)
   1.419 +done
   1.420 +
   1.421 +lemma bigo_minus3: "O(-f) = O(f)"
   1.422 +  by (auto simp add: bigo_def func_minus abs_minus_cancel)
   1.423 +
   1.424 +lemma bigo_plus_absorb_lemma1: "f : O(g) ==> f +o O(g) <= O(g)"
   1.425 +proof -
   1.426 +  assume a: "f : O(g)"
   1.427 +  show "f +o O(g) <= O(g)"
   1.428 +  proof -
   1.429 +    have "f : O(f)" by auto
   1.430 +    then have "f +o O(g) <= O(f) + O(g)"
   1.431 +      by (auto del: subsetI)
   1.432 +    also have "... <= O(g) + O(g)"
   1.433 +    proof -
   1.434 +      from a have "O(f) <= O(g)" by (auto del: subsetI)
   1.435 +      thus ?thesis by (auto del: subsetI)
   1.436 +    qed
   1.437 +    also have "... <= O(g)" by (simp add: bigo_plus_idemp)
   1.438 +    finally show ?thesis .
   1.439 +  qed
   1.440 +qed
   1.441 +
   1.442 +lemma bigo_plus_absorb_lemma2: "f : O(g) ==> O(g) <= f +o O(g)"
   1.443 +proof -
   1.444 +  assume a: "f : O(g)"
   1.445 +  show "O(g) <= f +o O(g)"
   1.446 +  proof -
   1.447 +    from a have "-f : O(g)" by auto
   1.448 +    then have "-f +o O(g) <= O(g)" by (elim bigo_plus_absorb_lemma1)
   1.449 +    then have "f +o (-f +o O(g)) <= f +o O(g)" by auto
   1.450 +    also have "f +o (-f +o O(g)) = O(g)"
   1.451 +      by (simp add: set_plus_rearranges)
   1.452 +    finally show ?thesis .
   1.453 +  qed
   1.454 +qed
   1.455 +
   1.456 +lemma bigo_plus_absorb [simp]: "f : O(g) ==> f +o O(g) = O(g)"
   1.457 +  apply (rule equalityI)
   1.458 +  apply (erule bigo_plus_absorb_lemma1)
   1.459 +  apply (erule bigo_plus_absorb_lemma2)
   1.460 +done
   1.461 +
   1.462 +lemma bigo_plus_absorb2 [intro]: "f : O(g) ==> A <= O(g) ==> f +o A <= O(g)"
   1.463 +  apply (subgoal_tac "f +o A <= f +o O(g)")
   1.464 +  apply force+
   1.465 +done
   1.466 +
   1.467 +lemma bigo_add_commute_imp: "f : g +o O(h) ==> g : f +o O(h)"
   1.468 +  apply (subst set_minus_plus [symmetric])
   1.469 +  apply (subgoal_tac "g - f = - (f - g)")
   1.470 +  apply (erule ssubst)
   1.471 +  apply (rule bigo_minus)
   1.472 +  apply (subst set_minus_plus)
   1.473 +  apply assumption
   1.474 +  apply  (simp add: diff_minus add_ac)
   1.475 +done
   1.476 +
   1.477 +lemma bigo_add_commute: "(f : g +o O(h)) = (g : f +o O(h))"
   1.478 +  apply (rule iffI)
   1.479 +  apply (erule bigo_add_commute_imp)+
   1.480 +done
   1.481 +
   1.482 +lemma bigo_const1: "(%x. c) : O(%x. 1)"
   1.483 +by (auto simp add: bigo_def mult_ac)
   1.484 +
   1.485 +lemma bigo_const2 [intro]: "O(%x. c) <= O(%x. 1)"
   1.486 +  apply (rule bigo_elt_subset)
   1.487 +  apply (rule bigo_const1)
   1.488 +done
   1.489 +
   1.490 +lemma bigo_const3: "(c::'a::ordered_field) ~= 0 ==> (%x. 1) : O(%x. c)"
   1.491 +  apply (simp add: bigo_def)
   1.492 +  apply (rule_tac x = "abs(inverse c)" in exI)
   1.493 +  apply (simp add: abs_mult [symmetric])
   1.494 +done
   1.495 +
   1.496 +lemma bigo_const4: "(c::'a::ordered_field) ~= 0 ==> O(%x. 1) <= O(%x. c)"
   1.497 +by (rule bigo_elt_subset, rule bigo_const3, assumption)
   1.498 +
   1.499 +lemma bigo_const [simp]: "(c::'a::ordered_field) ~= 0 ==> 
   1.500 +    O(%x. c) = O(%x. 1)"
   1.501 +by (rule equalityI, rule bigo_const2, rule bigo_const4, assumption)
   1.502 +
   1.503 +lemma bigo_const_mult1: "(%x. c * f x) : O(f)"
   1.504 +  apply (simp add: bigo_def)
   1.505 +  apply (rule_tac x = "abs(c)" in exI)
   1.506 +  apply (auto simp add: abs_mult [symmetric])
   1.507 +done
   1.508 +
   1.509 +lemma bigo_const_mult2: "O(%x. c * f x) <= O(f)"
   1.510 +by (rule bigo_elt_subset, rule bigo_const_mult1)
   1.511 +
   1.512 +lemma bigo_const_mult3: "(c::'a::ordered_field) ~= 0 ==> f : O(%x. c * f x)"
   1.513 +  apply (simp add: bigo_def)
   1.514 +  apply (rule_tac x = "abs(inverse c)" in exI)
   1.515 +  apply (simp add: abs_mult [symmetric] mult_assoc [symmetric])
   1.516 +done
   1.517 +
   1.518 +lemma bigo_const_mult4: "(c::'a::ordered_field) ~= 0 ==> 
   1.519 +    O(f) <= O(%x. c * f x)"
   1.520 +by (rule bigo_elt_subset, rule bigo_const_mult3, assumption)
   1.521 +
   1.522 +lemma bigo_const_mult [simp]: "(c::'a::ordered_field) ~= 0 ==> 
   1.523 +    O(%x. c * f x) = O(f)"
   1.524 +by (rule equalityI, rule bigo_const_mult2, erule bigo_const_mult4)
   1.525 +
   1.526 +lemma bigo_const_mult5 [simp]: "(c::'a::ordered_field) ~= 0 ==> 
   1.527 +    (%x. c) *o O(f) = O(f)"
   1.528 +  apply (auto del: subsetI)
   1.529 +  apply (rule order_trans)
   1.530 +  apply (rule bigo_mult2)
   1.531 +  apply (simp add: func_times)
   1.532 +  apply (auto intro!: subsetI simp add: bigo_def elt_set_times_def func_times)
   1.533 +  apply (rule_tac x = "%y. inverse c * x y" in exI)
   1.534 +  apply (simp add: mult_assoc [symmetric] abs_mult)
   1.535 +  apply (rule_tac x = "abs (inverse c) * ca" in exI)
   1.536 +  apply (rule allI)
   1.537 +  apply (subst mult_assoc)
   1.538 +  apply (rule mult_left_mono)
   1.539 +  apply (erule spec)
   1.540 +  apply force
   1.541 +done
   1.542 +
   1.543 +lemma bigo_const_mult6 [intro]: "(%x. c) *o O(f) <= O(f)"
   1.544 +  apply (auto intro!: subsetI
   1.545 +    simp add: bigo_def elt_set_times_def func_times)
   1.546 +  apply (rule_tac x = "ca * (abs c)" in exI)
   1.547 +  apply (rule allI)
   1.548 +  apply (subgoal_tac "ca * abs(c) * abs(f x) = abs(c) * (ca * abs(f x))")
   1.549 +  apply (erule ssubst)
   1.550 +  apply (subst abs_mult)
   1.551 +  apply (rule mult_left_mono)
   1.552 +  apply (erule spec)
   1.553 +  apply simp
   1.554 +  apply(simp add: mult_ac)
   1.555 +done
   1.556 +
   1.557 +lemma bigo_const_mult7 [intro]: "f =o O(g) ==> (%x. c * f x) =o O(g)"
   1.558 +proof -
   1.559 +  assume "f =o O(g)"
   1.560 +  then have "(%x. c) * f =o (%x. c) *o O(g)"
   1.561 +    by auto
   1.562 +  also have "(%x. c) * f = (%x. c * f x)"
   1.563 +    by (simp add: func_times)
   1.564 +  also have "(%x. c) *o O(g) <= O(g)"
   1.565 +    by (auto del: subsetI)
   1.566 +  finally show ?thesis .
   1.567 +qed
   1.568 +
   1.569 +lemma bigo_compose1: "f =o O(g) ==> (%x. f(k x)) =o O(%x. g(k x))"
   1.570 +by (unfold bigo_def, auto)
   1.571 +
   1.572 +lemma bigo_compose2: "f =o g +o O(h) ==> (%x. f(k x)) =o (%x. g(k x)) +o 
   1.573 +    O(%x. h(k x))"
   1.574 +  apply (simp only: set_minus_plus [symmetric] diff_minus func_minus
   1.575 +      func_plus)
   1.576 +  apply (erule bigo_compose1)
   1.577 +done
   1.578 +
   1.579 +subsection {* Setsum *}
   1.580 +
   1.581 +lemma bigo_setsum_main: "ALL x. ALL y : A x. 0 <= h x y ==> 
   1.582 +    EX c. ALL x. ALL y : A x. abs(f x y) <= c * (h x y) ==>
   1.583 +      (%x. SUM y : A x. f x y) =o O(%x. SUM y : A x. h x y)"  
   1.584 +  apply (auto simp add: bigo_def)
   1.585 +  apply (rule_tac x = "abs c" in exI)
   1.586 +  apply (subst abs_of_nonneg);back;back
   1.587 +  apply (rule setsum_nonneg)
   1.588 +  apply force
   1.589 +  apply (subst setsum_mult)
   1.590 +  apply (rule allI)
   1.591 +  apply (rule order_trans)
   1.592 +  apply (rule setsum_abs)
   1.593 +  apply (rule setsum_mono)
   1.594 +  apply (rule order_trans)
   1.595 +  apply (drule spec)+
   1.596 +  apply (drule bspec)+
   1.597 +  apply assumption+
   1.598 +  apply (drule bspec)
   1.599 +  apply assumption+
   1.600 +  apply (rule mult_right_mono) 
   1.601 +  apply (rule abs_ge_self)
   1.602 +  apply force
   1.603 +done
   1.604 +
   1.605 +lemma bigo_setsum1: "ALL x y. 0 <= h x y ==> 
   1.606 +    EX c. ALL x y. abs(f x y) <= c * (h x y) ==>
   1.607 +      (%x. SUM y : A x. f x y) =o O(%x. SUM y : A x. h x y)"
   1.608 +  apply (rule bigo_setsum_main)
   1.609 +  apply force
   1.610 +  apply clarsimp
   1.611 +  apply (rule_tac x = c in exI)
   1.612 +  apply force
   1.613 +done
   1.614 +
   1.615 +lemma bigo_setsum2: "ALL y. 0 <= h y ==> 
   1.616 +    EX c. ALL y. abs(f y) <= c * (h y) ==>
   1.617 +      (%x. SUM y : A x. f y) =o O(%x. SUM y : A x. h y)"
   1.618 +by (rule bigo_setsum1, auto)  
   1.619 +
   1.620 +lemma bigo_setsum3: "f =o O(h) ==>
   1.621 +    (%x. SUM y : A x. (l x y) * f(k x y)) =o
   1.622 +      O(%x. SUM y : A x. abs(l x y * h(k x y)))"
   1.623 +  apply (rule bigo_setsum1)
   1.624 +  apply (rule allI)+
   1.625 +  apply (rule abs_ge_zero)
   1.626 +  apply (unfold bigo_def)
   1.627 +  apply auto
   1.628 +  apply (rule_tac x = c in exI)
   1.629 +  apply (rule allI)+
   1.630 +  apply (subst abs_mult)+
   1.631 +  apply (subst mult_left_commute)
   1.632 +  apply (rule mult_left_mono)
   1.633 +  apply (erule spec)
   1.634 +  apply (rule abs_ge_zero)
   1.635 +done
   1.636 +
   1.637 +lemma bigo_setsum4: "f =o g +o O(h) ==>
   1.638 +    (%x. SUM y : A x. l x y * f(k x y)) =o
   1.639 +      (%x. SUM y : A x. l x y * g(k x y)) +o
   1.640 +        O(%x. SUM y : A x. abs(l x y * h(k x y)))"
   1.641 +  apply (rule set_minus_imp_plus)
   1.642 +  apply (subst func_diff)
   1.643 +  apply (subst setsum_subtractf [symmetric])
   1.644 +  apply (subst right_diff_distrib [symmetric])
   1.645 +  apply (rule bigo_setsum3)
   1.646 +  apply (subst func_diff [symmetric])
   1.647 +  apply (erule set_plus_imp_minus)
   1.648 +done
   1.649 +
   1.650 +lemma bigo_setsum5: "f =o O(h) ==> ALL x y. 0 <= l x y ==> 
   1.651 +    ALL x. 0 <= h x ==>
   1.652 +      (%x. SUM y : A x. (l x y) * f(k x y)) =o
   1.653 +        O(%x. SUM y : A x. (l x y) * h(k x y))" 
   1.654 +  apply (subgoal_tac "(%x. SUM y : A x. (l x y) * h(k x y)) = 
   1.655 +      (%x. SUM y : A x. abs((l x y) * h(k x y)))")
   1.656 +  apply (erule ssubst)
   1.657 +  apply (erule bigo_setsum3)
   1.658 +  apply (rule ext)
   1.659 +  apply (rule setsum_cong2)
   1.660 +  apply (subst abs_of_nonneg)
   1.661 +  apply (rule mult_nonneg_nonneg)
   1.662 +  apply auto
   1.663 +done
   1.664 +
   1.665 +lemma bigo_setsum6: "f =o g +o O(h) ==> ALL x y. 0 <= l x y ==>
   1.666 +    ALL x. 0 <= h x ==>
   1.667 +      (%x. SUM y : A x. (l x y) * f(k x y)) =o
   1.668 +        (%x. SUM y : A x. (l x y) * g(k x y)) +o
   1.669 +          O(%x. SUM y : A x. (l x y) * h(k x y))" 
   1.670 +  apply (rule set_minus_imp_plus)
   1.671 +  apply (subst func_diff)
   1.672 +  apply (subst setsum_subtractf [symmetric])
   1.673 +  apply (subst right_diff_distrib [symmetric])
   1.674 +  apply (rule bigo_setsum5)
   1.675 +  apply (subst func_diff [symmetric])
   1.676 +  apply (drule set_plus_imp_minus)
   1.677 +  apply auto
   1.678 +done
   1.679 +
   1.680 +subsection {* Misc useful stuff *}
   1.681 +
   1.682 +lemma bigo_useful_intro: "A <= O(f) ==> B <= O(f) ==>
   1.683 +  A + B <= O(f)"
   1.684 +  apply (subst bigo_plus_idemp [symmetric])
   1.685 +  apply (rule set_plus_mono2)
   1.686 +  apply assumption+
   1.687 +done
   1.688 +
   1.689 +lemma bigo_useful_add: "f =o O(h) ==> g =o O(h) ==> f + g =o O(h)"
   1.690 +  apply (subst bigo_plus_idemp [symmetric])
   1.691 +  apply (rule set_plus_intro)
   1.692 +  apply assumption+
   1.693 +done
   1.694 +  
   1.695 +lemma bigo_useful_const_mult: "(c::'a::ordered_field) ~= 0 ==> 
   1.696 +    (%x. c) * f =o O(h) ==> f =o O(h)"
   1.697 +  apply (rule subsetD)
   1.698 +  apply (subgoal_tac "(%x. 1 / c) *o O(h) <= O(h)")
   1.699 +  apply assumption
   1.700 +  apply (rule bigo_const_mult6)
   1.701 +  apply (subgoal_tac "f = (%x. 1 / c) * ((%x. c) * f)")
   1.702 +  apply (erule ssubst)
   1.703 +  apply (erule set_times_intro2)
   1.704 +  apply (simp add: func_times) 
   1.705 +  apply (rule ext)
   1.706 +  apply (subst times_divide_eq_left [symmetric])
   1.707 +  apply (subst divide_self)
   1.708 +  apply (assumption, simp)
   1.709 +done
   1.710 +
   1.711 +lemma bigo_fix: "(%x. f ((x::nat) + 1)) =o O(%x. h(x + 1)) ==> f 0 = 0 ==>
   1.712 +    f =o O(h)"
   1.713 +  apply (simp add: bigo_alt_def)
   1.714 +  apply auto
   1.715 +  apply (rule_tac x = c in exI)
   1.716 +  apply auto
   1.717 +  apply (case_tac "x = 0")
   1.718 +  apply simp
   1.719 +  apply (rule mult_nonneg_nonneg)
   1.720 +  apply force
   1.721 +  apply force
   1.722 +  apply (subgoal_tac "x = Suc (x - 1)")
   1.723 +  apply (erule ssubst)back
   1.724 +  apply (erule spec)
   1.725 +  apply simp
   1.726 +done
   1.727 +
   1.728 +lemma bigo_fix2: 
   1.729 +    "(%x. f ((x::nat) + 1)) =o (%x. g(x + 1)) +o O(%x. h(x + 1)) ==> 
   1.730 +       f 0 = g 0 ==> f =o g +o O(h)"
   1.731 +  apply (rule set_minus_imp_plus)
   1.732 +  apply (rule bigo_fix)
   1.733 +  apply (subst func_diff)
   1.734 +  apply (subst func_diff [symmetric])
   1.735 +  apply (rule set_plus_imp_minus)
   1.736 +  apply simp
   1.737 +  apply (simp add: func_diff)
   1.738 +done
   1.739 +
   1.740 +subsection {* Less than or equal to *}
   1.741 +
   1.742 +constdefs 
   1.743 +  lesso :: "('a => 'b::ordered_idom) => ('a => 'b) => ('a => 'b)"
   1.744 +      (infixl "<o" 70)
   1.745 +  "f <o g == (%x. max (f x - g x) 0)"
   1.746 +
   1.747 +lemma bigo_lesseq1: "f =o O(h) ==> ALL x. abs (g x) <= abs (f x) ==>
   1.748 +    g =o O(h)"
   1.749 +  apply (unfold bigo_def)
   1.750 +  apply clarsimp
   1.751 +  apply (rule_tac x = c in exI)
   1.752 +  apply (rule allI)
   1.753 +  apply (rule order_trans)
   1.754 +  apply (erule spec)+
   1.755 +done
   1.756 +
   1.757 +lemma bigo_lesseq2: "f =o O(h) ==> ALL x. abs (g x) <= f x ==>
   1.758 +      g =o O(h)"
   1.759 +  apply (erule bigo_lesseq1)
   1.760 +  apply (rule allI)
   1.761 +  apply (drule_tac x = x in spec)
   1.762 +  apply (rule order_trans)
   1.763 +  apply assumption
   1.764 +  apply (rule abs_ge_self)
   1.765 +done
   1.766 +
   1.767 +lemma bigo_lesseq3: "f =o O(h) ==> ALL x. 0 <= g x ==> ALL x. g x <= f x ==>
   1.768 +      g =o O(h)"
   1.769 +  apply (erule bigo_lesseq2)
   1.770 +  apply (rule allI)
   1.771 +  apply (subst abs_of_nonneg)
   1.772 +  apply (erule spec)+
   1.773 +done
   1.774 +
   1.775 +lemma bigo_lesseq4: "f =o O(h) ==>
   1.776 +    ALL x. 0 <= g x ==> ALL x. g x <= abs (f x) ==>
   1.777 +      g =o O(h)"
   1.778 +  apply (erule bigo_lesseq1)
   1.779 +  apply (rule allI)
   1.780 +  apply (subst abs_of_nonneg)
   1.781 +  apply (erule spec)+
   1.782 +done
   1.783 +
   1.784 +lemma bigo_lesso1: "ALL x. f x <= g x ==> f <o g =o O(h)"
   1.785 +  apply (unfold lesso_def)
   1.786 +  apply (subgoal_tac "(%x. max (f x - g x) 0) = 0")
   1.787 +  apply (erule ssubst)
   1.788 +  apply (rule bigo_zero)
   1.789 +  apply (unfold func_zero)
   1.790 +  apply (rule ext)
   1.791 +  apply (simp split: split_max)
   1.792 +done
   1.793 +
   1.794 +lemma bigo_lesso2: "f =o g +o O(h) ==>
   1.795 +    ALL x. 0 <= k x ==> ALL x. k x <= f x ==>
   1.796 +      k <o g =o O(h)"
   1.797 +  apply (unfold lesso_def)
   1.798 +  apply (rule bigo_lesseq4)
   1.799 +  apply (erule set_plus_imp_minus)
   1.800 +  apply (rule allI)
   1.801 +  apply (rule le_maxI2)
   1.802 +  apply (rule allI)
   1.803 +  apply (subst func_diff)
   1.804 +  apply (case_tac "0 <= k x - g x")
   1.805 +  apply simp
   1.806 +  apply (subst abs_of_nonneg)
   1.807 +  apply (drule_tac x = x in spec)back
   1.808 +  apply (simp add: compare_rls)
   1.809 +  apply (subst diff_minus)+
   1.810 +  apply (rule add_right_mono)
   1.811 +  apply (erule spec)
   1.812 +  apply (rule order_trans) 
   1.813 +  prefer 2
   1.814 +  apply (rule abs_ge_zero)
   1.815 +  apply (simp add: compare_rls)
   1.816 +done
   1.817 +
   1.818 +lemma bigo_lesso3: "f =o g +o O(h) ==>
   1.819 +    ALL x. 0 <= k x ==> ALL x. g x <= k x ==>
   1.820 +      f <o k =o O(h)"
   1.821 +  apply (unfold lesso_def)
   1.822 +  apply (rule bigo_lesseq4)
   1.823 +  apply (erule set_plus_imp_minus)
   1.824 +  apply (rule allI)
   1.825 +  apply (rule le_maxI2)
   1.826 +  apply (rule allI)
   1.827 +  apply (subst func_diff)
   1.828 +  apply (case_tac "0 <= f x - k x")
   1.829 +  apply simp
   1.830 +  apply (subst abs_of_nonneg)
   1.831 +  apply (drule_tac x = x in spec)back
   1.832 +  apply (simp add: compare_rls)
   1.833 +  apply (subst diff_minus)+
   1.834 +  apply (rule add_left_mono)
   1.835 +  apply (rule le_imp_neg_le)
   1.836 +  apply (erule spec)
   1.837 +  apply (rule order_trans) 
   1.838 +  prefer 2
   1.839 +  apply (rule abs_ge_zero)
   1.840 +  apply (simp add: compare_rls)
   1.841 +done
   1.842 +
   1.843 +lemma bigo_lesso4: "f <o g =o O(k::'a=>'b::ordered_field) ==>
   1.844 +    g =o h +o O(k) ==> f <o h =o O(k)"
   1.845 +  apply (unfold lesso_def)
   1.846 +  apply (drule set_plus_imp_minus)
   1.847 +  apply (drule bigo_abs5)back
   1.848 +  apply (simp add: func_diff)
   1.849 +  apply (drule bigo_useful_add)
   1.850 +  apply assumption
   1.851 +  apply (erule bigo_lesseq2)back
   1.852 +  apply (rule allI)
   1.853 +  apply (auto simp add: func_plus func_diff compare_rls 
   1.854 +    split: split_max abs_split)
   1.855 +done
   1.856 +
   1.857 +lemma bigo_lesso5: "f <o g =o O(h) ==>
   1.858 +    EX C. ALL x. f x <= g x + C * abs(h x)"
   1.859 +  apply (simp only: lesso_def bigo_alt_def)
   1.860 +  apply clarsimp
   1.861 +  apply (rule_tac x = c in exI)
   1.862 +  apply (rule allI)
   1.863 +  apply (drule_tac x = x in spec)
   1.864 +  apply (subgoal_tac "abs(max (f x - g x) 0) = max (f x - g x) 0")
   1.865 +  apply (clarsimp simp add: compare_rls add_ac) 
   1.866 +  apply (rule abs_of_nonneg)
   1.867 +  apply (rule le_maxI2)
   1.868 +done
   1.869 +
   1.870 +lemma lesso_add: "f <o g =o O(h) ==>
   1.871 +      k <o l =o O(h) ==> (f + k) <o (g + l) =o O(h)"
   1.872 +  apply (unfold lesso_def)
   1.873 +  apply (rule bigo_lesseq3)
   1.874 +  apply (erule bigo_useful_add)
   1.875 +  apply assumption
   1.876 +  apply (force split: split_max)
   1.877 +  apply (auto split: split_max simp add: func_plus)
   1.878 +done
   1.879 +
   1.880 +(* 
   1.881 +These last two lemmas require the HOL-Complex library.
   1.882 +
   1.883 +lemma bigo_LIMSEQ1: "f =o O(g) ==> g ----> 0 ==> f ----> 0"
   1.884 +  apply (simp add: LIMSEQ_def bigo_alt_def)
   1.885 +  apply clarify
   1.886 +  apply (drule_tac x = "r / c" in spec)
   1.887 +  apply (drule mp)
   1.888 +  apply (erule divide_pos_pos)
   1.889 +  apply assumption
   1.890 +  apply clarify
   1.891 +  apply (rule_tac x = no in exI)
   1.892 +  apply (rule allI)
   1.893 +  apply (drule_tac x = n in spec)+
   1.894 +  apply (rule impI)
   1.895 +  apply (drule mp)
   1.896 +  apply assumption
   1.897 +  apply (rule order_le_less_trans)
   1.898 +  apply assumption
   1.899 +  apply (rule order_less_le_trans)
   1.900 +  apply (subgoal_tac "c * abs(g n) < c * (r / c)")
   1.901 +  apply assumption
   1.902 +  apply (erule mult_strict_left_mono)
   1.903 +  apply assumption
   1.904 +  apply simp
   1.905 +done
   1.906 +
   1.907 +lemma bigo_LIMSEQ2: "f =o g +o O(h) ==> h ----> 0 ==> f ----> a 
   1.908 +    ==> g ----> a"
   1.909 +  apply (drule set_plus_imp_minus)
   1.910 +  apply (drule bigo_LIMSEQ1)
   1.911 +  apply assumption
   1.912 +  apply (simp only: func_diff)
   1.913 +  apply (erule LIMSEQ_diff_approach_zero2)
   1.914 +  apply assumption
   1.915 +done
   1.916 +
   1.917 +*)
   1.918 +
   1.919 +end