Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
authoravigad
Mon Jul 25 18:54:49 2005 +0200 (2005-07-25)
changeset 16908d374530bfaaa
parent 16907 2187e3f94761
child 16909 acbc7a9c3864
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
NEWS
src/HOL/IsaMakefile
src/HOL/Library/BigO.thy
src/HOL/Library/Library.thy
src/HOL/Library/SetsAndFunctions.thy
     1.1 --- a/NEWS	Mon Jul 25 15:51:30 2005 +0200
     1.2 +++ b/NEWS	Mon Jul 25 18:54:49 2005 +0200
     1.3 @@ -389,6 +389,12 @@
     1.4  * Theory RComplete: expanded support for floor and ceiling functions.
     1.5  
     1.6  
     1.7 +*** HOL-Library ***
     1.8 +
     1.9 +* Theories SetsAndFunctions and BigO support asymptotic "big O" calculations.
    1.10 +See the notes in BigO.thy.
    1.11 +
    1.12 +
    1.13  *** HOLCF ***
    1.14  
    1.15  * HOLCF: discontinued special version of 'constdefs' (which used to
     2.1 --- a/src/HOL/IsaMakefile	Mon Jul 25 15:51:30 2005 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Mon Jul 25 18:54:49 2005 +0200
     2.3 @@ -176,6 +176,7 @@
     2.4  HOL-Library: HOL $(LOG)/HOL-Library.gz
     2.5  
     2.6  $(LOG)/HOL-Library.gz: $(OUT)/HOL Library/Accessible_Part.thy \
     2.7 +  Library/SetsAndFunctions.thy Library/BigO.thy \
     2.8    Library/EfficientNat.thy Library/FuncSet.thy Library/Library.thy \
     2.9    Library/List_Prefix.thy Library/Multiset.thy Library/NatPair.thy \
    2.10    Library/Permutation.thy Library/Primes.thy Library/Quotient.thy \
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Library/BigO.thy	Mon Jul 25 18:54:49 2005 +0200
     3.3 @@ -0,0 +1,916 @@
     3.4 +(*  Title:      BigO.thy
     3.5 +    Authors:    Jeremy Avigad and Kevin Donnelly
     3.6 +*)
     3.7 +
     3.8 +header {* Big O notation *}
     3.9 +
    3.10 +theory BigO
    3.11 +imports SetsAndFunctions
    3.12 +begin
    3.13 +
    3.14 +text {*
    3.15 +This library is designed to support asymptotic ``big O'' calculations,
    3.16 +i.e.~reasoning with expressions of the form $f = O(g)$ and $f = g + O(h)$.
    3.17 +An earlier version of this library is described in detail in
    3.18 +\begin{quote}
    3.19 +Avigad, Jeremy, and Kevin Donnelly, \emph{Formalizing O notation in 
    3.20 +Isabelle/HOL}, in David Basin and Micha\"el Rusiowitch, editors, 
    3.21 +\emph{Automated Reasoning: second international conference, IJCAR 2004}, 
    3.22 +Springer, 357--371, 2004.
    3.23 +\end{quote}
    3.24 +The main changes in this version are as follows:
    3.25 +\begin{itemize}
    3.26 +\item We have eliminated the $O$ operator on sets. (Most uses of this seem
    3.27 +  to be inessential.)
    3.28 +\item We no longer use $+$ as output syntax for $+o$.
    3.29 +\item Lemmas involving ``sumr-pos'' have been replaced by more
    3.30 +  general lemmas involving ``setsum''.
    3.31 +\item The library has been expanded, with e.g.~support for expressions of
    3.32 +  the form $f < g + O(h)$.
    3.33 +\end{itemize}
    3.34 +Note that two lemmas at the end of this file are commented out, as they 
    3.35 +require the HOL-Complex library.
    3.36 +
    3.37 +Note also since the Big O library includes rules that demonstrate set 
    3.38 +inclusion, to use the automated reasoners effectively with the library one 
    3.39 +should redeclare the theorem ``subsetI'' as an intro rule, rather than as 
    3.40 +an intro! rule, for example, using ``declare subsetI [del, intro]''.
    3.41 +*}
    3.42 +
    3.43 +subsection {* Definitions *}
    3.44 +
    3.45 +constdefs 
    3.46 +
    3.47 +  bigo :: "('a => 'b::ordered_idom) => ('a => 'b) set"    ("(1O'(_'))")
    3.48 +  "O(f::('a => 'b)) == 
    3.49 +      {h. EX c. ALL x. abs (h x) <= c * abs (f x)}"
    3.50 +
    3.51 +lemma bigo_pos_const: "(EX (c::'a::ordered_idom). 
    3.52 +    ALL x. (abs (h x)) <= (c * (abs (f x))))
    3.53 +      = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
    3.54 +  apply auto
    3.55 +  apply (case_tac "c = 0")
    3.56 +  apply simp
    3.57 +  apply (rule_tac x = "1" in exI)
    3.58 +  apply simp
    3.59 +  apply (rule_tac x = "abs c" in exI)
    3.60 +  apply auto
    3.61 +  apply (subgoal_tac "c * abs(f x) <= abs c * abs (f x)")
    3.62 +  apply (erule_tac x = x in allE)
    3.63 +  apply force
    3.64 +  apply (rule mult_right_mono)
    3.65 +  apply (rule abs_ge_self)
    3.66 +  apply (rule abs_ge_zero)
    3.67 +done
    3.68 +
    3.69 +lemma bigo_alt_def: "O(f) = 
    3.70 +    {h. EX c. (0 < c & (ALL x. abs (h x) <= c * abs (f x)))}"
    3.71 +by (auto simp add: bigo_def bigo_pos_const)
    3.72 +
    3.73 +lemma bigo_elt_subset [intro]: "f : O(g) ==> O(f) <= O(g)"
    3.74 +  apply (auto simp add: bigo_alt_def)
    3.75 +  apply (rule_tac x = "ca * c" in exI)
    3.76 +  apply (rule conjI)
    3.77 +  apply (rule mult_pos_pos)
    3.78 +  apply (assumption)+
    3.79 +  apply (rule allI)
    3.80 +  apply (drule_tac x = "xa" in spec)+
    3.81 +  apply (subgoal_tac "ca * abs(f xa) <= ca * (c * abs(g xa))")
    3.82 +  apply (erule order_trans)
    3.83 +  apply (simp add: mult_ac)
    3.84 +  apply (rule mult_left_mono, assumption)
    3.85 +  apply (rule order_less_imp_le, assumption)
    3.86 +done
    3.87 +
    3.88 +lemma bigo_refl [intro]: "f : O(f)"
    3.89 +  apply(auto simp add: bigo_def)
    3.90 +  apply(rule_tac x = 1 in exI)
    3.91 +  apply simp
    3.92 +done
    3.93 +
    3.94 +lemma bigo_zero: "0 : O(g)"
    3.95 +  apply (auto simp add: bigo_def func_zero)
    3.96 +  apply (rule_tac x = 0 in exI)
    3.97 +  apply auto
    3.98 +done
    3.99 +
   3.100 +lemma bigo_zero2: "O(%x.0) = {%x.0}"
   3.101 +  apply (auto simp add: bigo_def) 
   3.102 +  apply (rule ext)
   3.103 +  apply auto
   3.104 +done
   3.105 +
   3.106 +lemma bigo_plus_self_subset [intro]: 
   3.107 +  "O(f) + O(f) <= O(f)"
   3.108 +  apply (auto simp add: bigo_alt_def set_plus)
   3.109 +  apply (rule_tac x = "c + ca" in exI)
   3.110 +  apply auto
   3.111 +  apply (simp add: ring_distrib func_plus)
   3.112 +  apply (rule order_trans)
   3.113 +  apply (rule abs_triangle_ineq)
   3.114 +  apply (rule add_mono)
   3.115 +  apply force
   3.116 +  apply force
   3.117 +done
   3.118 +
   3.119 +lemma bigo_plus_idemp [simp]: "O(f) + O(f) = O(f)"
   3.120 +  apply (rule equalityI)
   3.121 +  apply (rule bigo_plus_self_subset)
   3.122 +  apply (rule set_zero_plus2) 
   3.123 +  apply (rule bigo_zero)
   3.124 +done
   3.125 +
   3.126 +lemma bigo_plus_subset [intro]: "O(f + g) <= O(f) + O(g)"
   3.127 +  apply (rule subsetI)
   3.128 +  apply (auto simp add: bigo_def bigo_pos_const func_plus set_plus)
   3.129 +  apply (subst bigo_pos_const [symmetric])+
   3.130 +  apply (rule_tac x = 
   3.131 +    "%n. if abs (g n) <= (abs (f n)) then x n else 0" in exI)
   3.132 +  apply (rule conjI)
   3.133 +  apply (rule_tac x = "c + c" in exI)
   3.134 +  apply (clarsimp)
   3.135 +  apply (auto)
   3.136 +  apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (f xa)")
   3.137 +  apply (erule_tac x = xa in allE)
   3.138 +  apply (erule order_trans)
   3.139 +  apply (simp)
   3.140 +  apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))")
   3.141 +  apply (erule order_trans)
   3.142 +  apply (simp add: ring_distrib)
   3.143 +  apply (rule mult_left_mono)
   3.144 +  apply assumption
   3.145 +  apply (simp add: order_less_le)
   3.146 +  apply (rule mult_left_mono)
   3.147 +  apply (simp add: abs_triangle_ineq)
   3.148 +  apply (simp add: order_less_le)
   3.149 +  apply (rule mult_nonneg_nonneg)
   3.150 +  apply (rule add_nonneg_nonneg)
   3.151 +  apply auto
   3.152 +  apply (rule_tac x = "%n. if (abs (f n)) <  abs (g n) then x n else 0" 
   3.153 +     in exI)
   3.154 +  apply (rule conjI)
   3.155 +  apply (rule_tac x = "c + c" in exI)
   3.156 +  apply auto
   3.157 +  apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (g xa)")
   3.158 +  apply (erule_tac x = xa in allE)
   3.159 +  apply (erule order_trans)
   3.160 +  apply (simp)
   3.161 +  apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))")
   3.162 +  apply (erule order_trans)
   3.163 +  apply (simp add: ring_distrib)
   3.164 +  apply (rule mult_left_mono)
   3.165 +  apply (simp add: order_less_le)
   3.166 +  apply (simp add: order_less_le)
   3.167 +  apply (rule mult_left_mono)
   3.168 +  apply (rule abs_triangle_ineq)
   3.169 +  apply (simp add: order_less_le)
   3.170 +  apply (rule mult_nonneg_nonneg)
   3.171 +  apply (rule add_nonneg_nonneg)
   3.172 +  apply (erule order_less_imp_le)+
   3.173 +  apply simp
   3.174 +  apply (rule ext)
   3.175 +  apply (auto simp add: if_splits linorder_not_le)
   3.176 +done
   3.177 +
   3.178 +lemma bigo_plus_subset2 [intro]: "A <= O(f) ==> B <= O(f) ==> A + B <= O(f)"
   3.179 +  apply (subgoal_tac "A + B <= O(f) + O(f)")
   3.180 +  apply (erule order_trans)
   3.181 +  apply simp
   3.182 +  apply (auto del: subsetI simp del: bigo_plus_idemp)
   3.183 +done
   3.184 +
   3.185 +lemma bigo_plus_eq: "ALL x. 0 <= f x ==> ALL x. 0 <= g x ==> 
   3.186 +  O(f + g) = O(f) + O(g)"
   3.187 +  apply (rule equalityI)
   3.188 +  apply (rule bigo_plus_subset)
   3.189 +  apply (simp add: bigo_alt_def set_plus func_plus)
   3.190 +  apply clarify
   3.191 +  apply (rule_tac x = "max c ca" in exI)
   3.192 +  apply (rule conjI)
   3.193 +  apply (subgoal_tac "c <= max c ca")
   3.194 +  apply (erule order_less_le_trans)
   3.195 +  apply assumption
   3.196 +  apply (rule le_maxI1)
   3.197 +  apply clarify
   3.198 +  apply (drule_tac x = "xa" in spec)+
   3.199 +  apply (subgoal_tac "0 <= f xa + g xa")
   3.200 +  apply (simp add: ring_distrib)
   3.201 +  apply (subgoal_tac "abs(a xa + b xa) <= abs(a xa) + abs(b xa)")
   3.202 +  apply (subgoal_tac "abs(a xa) + abs(b xa) <= 
   3.203 +      max c ca * f xa + max c ca * g xa")
   3.204 +  apply (force)
   3.205 +  apply (rule add_mono)
   3.206 +  apply (subgoal_tac "c * f xa <= max c ca * f xa")
   3.207 +  apply (force)
   3.208 +  apply (rule mult_right_mono)
   3.209 +  apply (rule le_maxI1)
   3.210 +  apply assumption
   3.211 +  apply (subgoal_tac "ca * g xa <= max c ca * g xa")
   3.212 +  apply (force)
   3.213 +  apply (rule mult_right_mono)
   3.214 +  apply (rule le_maxI2)
   3.215 +  apply assumption
   3.216 +  apply (rule abs_triangle_ineq)
   3.217 +  apply (rule add_nonneg_nonneg)
   3.218 +  apply assumption+
   3.219 +done
   3.220 +
   3.221 +lemma bigo_bounded_alt: "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> 
   3.222 +    f : O(g)" 
   3.223 +  apply (auto simp add: bigo_def)
   3.224 +  apply (rule_tac x = "abs c" in exI)
   3.225 +  apply auto
   3.226 +  apply (drule_tac x = x in spec)+
   3.227 +  apply (simp add: abs_mult [symmetric])
   3.228 +done
   3.229 +
   3.230 +lemma bigo_bounded: "ALL x. 0 <= f x ==> ALL x. f x <= g x ==> 
   3.231 +    f : O(g)" 
   3.232 +  apply (erule bigo_bounded_alt [of f 1 g])
   3.233 +  apply simp
   3.234 +done
   3.235 +
   3.236 +lemma bigo_bounded2: "ALL x. lb x <= f x ==> ALL x. f x <= lb x + g x ==>
   3.237 +    f : lb +o O(g)"
   3.238 +  apply (rule set_minus_imp_plus)
   3.239 +  apply (rule bigo_bounded)
   3.240 +  apply (auto simp add: diff_minus func_minus func_plus)
   3.241 +  apply (drule_tac x = x in spec)+
   3.242 +  apply force
   3.243 +  apply (drule_tac x = x in spec)+
   3.244 +  apply force
   3.245 +done
   3.246 +
   3.247 +lemma bigo_abs: "(%x. abs(f x)) =o O(f)" 
   3.248 +  apply (unfold bigo_def)
   3.249 +  apply auto
   3.250 +  apply (rule_tac x = 1 in exI)
   3.251 +  apply auto
   3.252 +done
   3.253 +
   3.254 +lemma bigo_abs2: "f =o O(%x. abs(f x))"
   3.255 +  apply (unfold bigo_def)
   3.256 +  apply auto
   3.257 +  apply (rule_tac x = 1 in exI)
   3.258 +  apply auto
   3.259 +done
   3.260 +
   3.261 +lemma bigo_abs3: "O(f) = O(%x. abs(f x))"
   3.262 +  apply (rule equalityI)
   3.263 +  apply (rule bigo_elt_subset)
   3.264 +  apply (rule bigo_abs2)
   3.265 +  apply (rule bigo_elt_subset)
   3.266 +  apply (rule bigo_abs)
   3.267 +done
   3.268 +
   3.269 +lemma bigo_abs4: "f =o g +o O(h) ==> 
   3.270 +    (%x. abs (f x)) =o (%x. abs (g x)) +o O(h)"
   3.271 +  apply (drule set_plus_imp_minus)
   3.272 +  apply (rule set_minus_imp_plus)
   3.273 +  apply (subst func_diff)
   3.274 +proof -
   3.275 +  assume a: "f - g : O(h)"
   3.276 +  have "(%x. abs (f x) - abs (g x)) =o O(%x. abs(abs (f x) - abs (g x)))"
   3.277 +    by (rule bigo_abs2)
   3.278 +  also have "... <= O(%x. abs (f x - g x))"
   3.279 +    apply (rule bigo_elt_subset)
   3.280 +    apply (rule bigo_bounded)
   3.281 +    apply force
   3.282 +    apply (rule allI)
   3.283 +    apply (rule abs_triangle_ineq3)
   3.284 +    done
   3.285 +  also have "... <= O(f - g)"
   3.286 +    apply (rule bigo_elt_subset)
   3.287 +    apply (subst func_diff)
   3.288 +    apply (rule bigo_abs)
   3.289 +    done
   3.290 +  also have "... <= O(h)"
   3.291 +    by (rule bigo_elt_subset)
   3.292 +  finally show "(%x. abs (f x) - abs (g x)) : O(h)".
   3.293 +qed
   3.294 +
   3.295 +lemma bigo_abs5: "f =o O(g) ==> (%x. abs(f x)) =o O(g)" 
   3.296 +by (unfold bigo_def, auto)
   3.297 +
   3.298 +lemma bigo_elt_subset2 [intro]: "f : g +o O(h) ==> O(f) <= O(g) + O(h)"
   3.299 +proof -
   3.300 +  assume "f : g +o O(h)"
   3.301 +  also have "... <= O(g) + O(h)"
   3.302 +    by (auto del: subsetI)
   3.303 +  also have "... = O(%x. abs(g x)) + O(%x. abs(h x))"
   3.304 +    apply (subst bigo_abs3 [symmetric])+
   3.305 +    apply (rule refl)
   3.306 +    done
   3.307 +  also have "... = O((%x. abs(g x)) + (%x. abs(h x)))"
   3.308 +    by (rule bigo_plus_eq [symmetric], auto)
   3.309 +  finally have "f : ...".
   3.310 +  then have "O(f) <= ..."
   3.311 +    by (elim bigo_elt_subset)
   3.312 +  also have "... = O(%x. abs(g x)) + O(%x. abs(h x))"
   3.313 +    by (rule bigo_plus_eq, auto)
   3.314 +  finally show ?thesis
   3.315 +    by (simp add: bigo_abs3 [symmetric])
   3.316 +qed
   3.317 +
   3.318 +lemma bigo_mult [intro]: "O(f)*O(g) <= O(f * g)"
   3.319 +  apply (rule subsetI)
   3.320 +  apply (subst bigo_def)
   3.321 +  apply (auto simp add: bigo_alt_def set_times func_times)
   3.322 +  apply (rule_tac x = "c * ca" in exI)
   3.323 +  apply(rule allI)
   3.324 +  apply(erule_tac x = x in allE)+
   3.325 +  apply(subgoal_tac "c * ca * abs(f x * g x) = 
   3.326 +      (c * abs(f x)) * (ca * abs(g x))")
   3.327 +  apply(erule ssubst)
   3.328 +  apply (subst abs_mult)
   3.329 +  apply (rule mult_mono)
   3.330 +  apply assumption+
   3.331 +  apply (rule mult_nonneg_nonneg)
   3.332 +  apply auto
   3.333 +  apply (simp add: mult_ac abs_mult)
   3.334 +done
   3.335 +
   3.336 +lemma bigo_mult2 [intro]: "f *o O(g) <= O(f * g)"
   3.337 +  apply (auto simp add: bigo_def elt_set_times_def func_times abs_mult)
   3.338 +  apply (rule_tac x = c in exI)
   3.339 +  apply auto
   3.340 +  apply (drule_tac x = x in spec)
   3.341 +  apply (subgoal_tac "abs(f x) * abs(b x) <= abs(f x) * (c * abs(g x))")
   3.342 +  apply (force simp add: mult_ac)
   3.343 +  apply (rule mult_left_mono, assumption)
   3.344 +  apply (rule abs_ge_zero)
   3.345 +done
   3.346 +
   3.347 +lemma bigo_mult3: "f : O(h) ==> g : O(j) ==> f * g : O(h * j)"
   3.348 +  apply (rule subsetD)
   3.349 +  apply (rule bigo_mult)
   3.350 +  apply (erule set_times_intro, assumption)
   3.351 +done
   3.352 +
   3.353 +lemma bigo_mult4 [intro]:"f : k +o O(h) ==> g * f : (g * k) +o O(g * h)"
   3.354 +  apply (drule set_plus_imp_minus)
   3.355 +  apply (rule set_minus_imp_plus)
   3.356 +  apply (drule bigo_mult3 [where g = g and j = g])
   3.357 +  apply (auto simp add: ring_eq_simps mult_ac)
   3.358 +done
   3.359 +
   3.360 +lemma bigo_mult5: "ALL x. f x ~= 0 ==>
   3.361 +    O(f * g) <= (f::'a => ('b::ordered_field)) *o O(g)"
   3.362 +proof -
   3.363 +  assume "ALL x. f x ~= 0"
   3.364 +  show "O(f * g) <= f *o O(g)"
   3.365 +  proof
   3.366 +    fix h
   3.367 +    assume "h : O(f * g)"
   3.368 +    then have "(%x. 1 / (f x)) * h : (%x. 1 / f x) *o O(f * g)"
   3.369 +      by auto
   3.370 +    also have "... <= O((%x. 1 / f x) * (f * g))"
   3.371 +      by (rule bigo_mult2)
   3.372 +    also have "(%x. 1 / f x) * (f * g) = g"
   3.373 +      apply (simp add: func_times) 
   3.374 +      apply (rule ext)
   3.375 +      apply (simp add: prems nonzero_divide_eq_eq mult_ac)
   3.376 +      done
   3.377 +    finally have "(%x. (1::'b) / f x) * h : O(g)".
   3.378 +    then have "f * ((%x. (1::'b) / f x) * h) : f *o O(g)"
   3.379 +      by auto
   3.380 +    also have "f * ((%x. (1::'b) / f x) * h) = h"
   3.381 +      apply (simp add: func_times) 
   3.382 +      apply (rule ext)
   3.383 +      apply (simp add: prems nonzero_divide_eq_eq mult_ac)
   3.384 +      done
   3.385 +    finally show "h : f *o O(g)".
   3.386 +  qed
   3.387 +qed
   3.388 +
   3.389 +lemma bigo_mult6: "ALL x. f x ~= 0 ==>
   3.390 +    O(f * g) = (f::'a => ('b::ordered_field)) *o O(g)"
   3.391 +  apply (rule equalityI)
   3.392 +  apply (erule bigo_mult5)
   3.393 +  apply (rule bigo_mult2)
   3.394 +done
   3.395 +
   3.396 +lemma bigo_mult7: "ALL x. f x ~= 0 ==>
   3.397 +    O(f * g) <= O(f::'a => ('b::ordered_field)) * O(g)"
   3.398 +  apply (subst bigo_mult6)
   3.399 +  apply assumption
   3.400 +  apply (rule set_times_mono3)
   3.401 +  apply (rule bigo_refl)
   3.402 +done
   3.403 +
   3.404 +lemma bigo_mult8: "ALL x. f x ~= 0 ==>
   3.405 +    O(f * g) = O(f::'a => ('b::ordered_field)) * O(g)"
   3.406 +  apply (rule equalityI)
   3.407 +  apply (erule bigo_mult7)
   3.408 +  apply (rule bigo_mult)
   3.409 +done
   3.410 +
   3.411 +lemma bigo_minus [intro]: "f : O(g) ==> - f : O(g)"
   3.412 +  by (auto simp add: bigo_def func_minus)
   3.413 +
   3.414 +lemma bigo_minus2: "f : g +o O(h) ==> -f : -g +o O(h)"
   3.415 +  apply (rule set_minus_imp_plus)
   3.416 +  apply (drule set_plus_imp_minus)
   3.417 +  apply (drule bigo_minus)
   3.418 +  apply (simp add: diff_minus)
   3.419 +done
   3.420 +
   3.421 +lemma bigo_minus3: "O(-f) = O(f)"
   3.422 +  by (auto simp add: bigo_def func_minus abs_minus_cancel)
   3.423 +
   3.424 +lemma bigo_plus_absorb_lemma1: "f : O(g) ==> f +o O(g) <= O(g)"
   3.425 +proof -
   3.426 +  assume a: "f : O(g)"
   3.427 +  show "f +o O(g) <= O(g)"
   3.428 +  proof -
   3.429 +    have "f : O(f)" by auto
   3.430 +    then have "f +o O(g) <= O(f) + O(g)"
   3.431 +      by (auto del: subsetI)
   3.432 +    also have "... <= O(g) + O(g)"
   3.433 +    proof -
   3.434 +      from a have "O(f) <= O(g)" by (auto del: subsetI)
   3.435 +      thus ?thesis by (auto del: subsetI)
   3.436 +    qed
   3.437 +    also have "... <= O(g)" by (simp add: bigo_plus_idemp)
   3.438 +    finally show ?thesis .
   3.439 +  qed
   3.440 +qed
   3.441 +
   3.442 +lemma bigo_plus_absorb_lemma2: "f : O(g) ==> O(g) <= f +o O(g)"
   3.443 +proof -
   3.444 +  assume a: "f : O(g)"
   3.445 +  show "O(g) <= f +o O(g)"
   3.446 +  proof -
   3.447 +    from a have "-f : O(g)" by auto
   3.448 +    then have "-f +o O(g) <= O(g)" by (elim bigo_plus_absorb_lemma1)
   3.449 +    then have "f +o (-f +o O(g)) <= f +o O(g)" by auto
   3.450 +    also have "f +o (-f +o O(g)) = O(g)"
   3.451 +      by (simp add: set_plus_rearranges)
   3.452 +    finally show ?thesis .
   3.453 +  qed
   3.454 +qed
   3.455 +
   3.456 +lemma bigo_plus_absorb [simp]: "f : O(g) ==> f +o O(g) = O(g)"
   3.457 +  apply (rule equalityI)
   3.458 +  apply (erule bigo_plus_absorb_lemma1)
   3.459 +  apply (erule bigo_plus_absorb_lemma2)
   3.460 +done
   3.461 +
   3.462 +lemma bigo_plus_absorb2 [intro]: "f : O(g) ==> A <= O(g) ==> f +o A <= O(g)"
   3.463 +  apply (subgoal_tac "f +o A <= f +o O(g)")
   3.464 +  apply force+
   3.465 +done
   3.466 +
   3.467 +lemma bigo_add_commute_imp: "f : g +o O(h) ==> g : f +o O(h)"
   3.468 +  apply (subst set_minus_plus [symmetric])
   3.469 +  apply (subgoal_tac "g - f = - (f - g)")
   3.470 +  apply (erule ssubst)
   3.471 +  apply (rule bigo_minus)
   3.472 +  apply (subst set_minus_plus)
   3.473 +  apply assumption
   3.474 +  apply  (simp add: diff_minus add_ac)
   3.475 +done
   3.476 +
   3.477 +lemma bigo_add_commute: "(f : g +o O(h)) = (g : f +o O(h))"
   3.478 +  apply (rule iffI)
   3.479 +  apply (erule bigo_add_commute_imp)+
   3.480 +done
   3.481 +
   3.482 +lemma bigo_const1: "(%x. c) : O(%x. 1)"
   3.483 +by (auto simp add: bigo_def mult_ac)
   3.484 +
   3.485 +lemma bigo_const2 [intro]: "O(%x. c) <= O(%x. 1)"
   3.486 +  apply (rule bigo_elt_subset)
   3.487 +  apply (rule bigo_const1)
   3.488 +done
   3.489 +
   3.490 +lemma bigo_const3: "(c::'a::ordered_field) ~= 0 ==> (%x. 1) : O(%x. c)"
   3.491 +  apply (simp add: bigo_def)
   3.492 +  apply (rule_tac x = "abs(inverse c)" in exI)
   3.493 +  apply (simp add: abs_mult [symmetric])
   3.494 +done
   3.495 +
   3.496 +lemma bigo_const4: "(c::'a::ordered_field) ~= 0 ==> O(%x. 1) <= O(%x. c)"
   3.497 +by (rule bigo_elt_subset, rule bigo_const3, assumption)
   3.498 +
   3.499 +lemma bigo_const [simp]: "(c::'a::ordered_field) ~= 0 ==> 
   3.500 +    O(%x. c) = O(%x. 1)"
   3.501 +by (rule equalityI, rule bigo_const2, rule bigo_const4, assumption)
   3.502 +
   3.503 +lemma bigo_const_mult1: "(%x. c * f x) : O(f)"
   3.504 +  apply (simp add: bigo_def)
   3.505 +  apply (rule_tac x = "abs(c)" in exI)
   3.506 +  apply (auto simp add: abs_mult [symmetric])
   3.507 +done
   3.508 +
   3.509 +lemma bigo_const_mult2: "O(%x. c * f x) <= O(f)"
   3.510 +by (rule bigo_elt_subset, rule bigo_const_mult1)
   3.511 +
   3.512 +lemma bigo_const_mult3: "(c::'a::ordered_field) ~= 0 ==> f : O(%x. c * f x)"
   3.513 +  apply (simp add: bigo_def)
   3.514 +  apply (rule_tac x = "abs(inverse c)" in exI)
   3.515 +  apply (simp add: abs_mult [symmetric] mult_assoc [symmetric])
   3.516 +done
   3.517 +
   3.518 +lemma bigo_const_mult4: "(c::'a::ordered_field) ~= 0 ==> 
   3.519 +    O(f) <= O(%x. c * f x)"
   3.520 +by (rule bigo_elt_subset, rule bigo_const_mult3, assumption)
   3.521 +
   3.522 +lemma bigo_const_mult [simp]: "(c::'a::ordered_field) ~= 0 ==> 
   3.523 +    O(%x. c * f x) = O(f)"
   3.524 +by (rule equalityI, rule bigo_const_mult2, erule bigo_const_mult4)
   3.525 +
   3.526 +lemma bigo_const_mult5 [simp]: "(c::'a::ordered_field) ~= 0 ==> 
   3.527 +    (%x. c) *o O(f) = O(f)"
   3.528 +  apply (auto del: subsetI)
   3.529 +  apply (rule order_trans)
   3.530 +  apply (rule bigo_mult2)
   3.531 +  apply (simp add: func_times)
   3.532 +  apply (auto intro!: subsetI simp add: bigo_def elt_set_times_def func_times)
   3.533 +  apply (rule_tac x = "%y. inverse c * x y" in exI)
   3.534 +  apply (simp add: mult_assoc [symmetric] abs_mult)
   3.535 +  apply (rule_tac x = "abs (inverse c) * ca" in exI)
   3.536 +  apply (rule allI)
   3.537 +  apply (subst mult_assoc)
   3.538 +  apply (rule mult_left_mono)
   3.539 +  apply (erule spec)
   3.540 +  apply force
   3.541 +done
   3.542 +
   3.543 +lemma bigo_const_mult6 [intro]: "(%x. c) *o O(f) <= O(f)"
   3.544 +  apply (auto intro!: subsetI
   3.545 +    simp add: bigo_def elt_set_times_def func_times)
   3.546 +  apply (rule_tac x = "ca * (abs c)" in exI)
   3.547 +  apply (rule allI)
   3.548 +  apply (subgoal_tac "ca * abs(c) * abs(f x) = abs(c) * (ca * abs(f x))")
   3.549 +  apply (erule ssubst)
   3.550 +  apply (subst abs_mult)
   3.551 +  apply (rule mult_left_mono)
   3.552 +  apply (erule spec)
   3.553 +  apply simp
   3.554 +  apply(simp add: mult_ac)
   3.555 +done
   3.556 +
   3.557 +lemma bigo_const_mult7 [intro]: "f =o O(g) ==> (%x. c * f x) =o O(g)"
   3.558 +proof -
   3.559 +  assume "f =o O(g)"
   3.560 +  then have "(%x. c) * f =o (%x. c) *o O(g)"
   3.561 +    by auto
   3.562 +  also have "(%x. c) * f = (%x. c * f x)"
   3.563 +    by (simp add: func_times)
   3.564 +  also have "(%x. c) *o O(g) <= O(g)"
   3.565 +    by (auto del: subsetI)
   3.566 +  finally show ?thesis .
   3.567 +qed
   3.568 +
   3.569 +lemma bigo_compose1: "f =o O(g) ==> (%x. f(k x)) =o O(%x. g(k x))"
   3.570 +by (unfold bigo_def, auto)
   3.571 +
   3.572 +lemma bigo_compose2: "f =o g +o O(h) ==> (%x. f(k x)) =o (%x. g(k x)) +o 
   3.573 +    O(%x. h(k x))"
   3.574 +  apply (simp only: set_minus_plus [symmetric] diff_minus func_minus
   3.575 +      func_plus)
   3.576 +  apply (erule bigo_compose1)
   3.577 +done
   3.578 +
   3.579 +subsection {* Setsum *}
   3.580 +
   3.581 +lemma bigo_setsum_main: "ALL x. ALL y : A x. 0 <= h x y ==> 
   3.582 +    EX c. ALL x. ALL y : A x. abs(f x y) <= c * (h x y) ==>
   3.583 +      (%x. SUM y : A x. f x y) =o O(%x. SUM y : A x. h x y)"  
   3.584 +  apply (auto simp add: bigo_def)
   3.585 +  apply (rule_tac x = "abs c" in exI)
   3.586 +  apply (subst abs_of_nonneg);back;back
   3.587 +  apply (rule setsum_nonneg)
   3.588 +  apply force
   3.589 +  apply (subst setsum_mult)
   3.590 +  apply (rule allI)
   3.591 +  apply (rule order_trans)
   3.592 +  apply (rule setsum_abs)
   3.593 +  apply (rule setsum_mono)
   3.594 +  apply (rule order_trans)
   3.595 +  apply (drule spec)+
   3.596 +  apply (drule bspec)+
   3.597 +  apply assumption+
   3.598 +  apply (drule bspec)
   3.599 +  apply assumption+
   3.600 +  apply (rule mult_right_mono) 
   3.601 +  apply (rule abs_ge_self)
   3.602 +  apply force
   3.603 +done
   3.604 +
   3.605 +lemma bigo_setsum1: "ALL x y. 0 <= h x y ==> 
   3.606 +    EX c. ALL x y. abs(f x y) <= c * (h x y) ==>
   3.607 +      (%x. SUM y : A x. f x y) =o O(%x. SUM y : A x. h x y)"
   3.608 +  apply (rule bigo_setsum_main)
   3.609 +  apply force
   3.610 +  apply clarsimp
   3.611 +  apply (rule_tac x = c in exI)
   3.612 +  apply force
   3.613 +done
   3.614 +
   3.615 +lemma bigo_setsum2: "ALL y. 0 <= h y ==> 
   3.616 +    EX c. ALL y. abs(f y) <= c * (h y) ==>
   3.617 +      (%x. SUM y : A x. f y) =o O(%x. SUM y : A x. h y)"
   3.618 +by (rule bigo_setsum1, auto)  
   3.619 +
   3.620 +lemma bigo_setsum3: "f =o O(h) ==>
   3.621 +    (%x. SUM y : A x. (l x y) * f(k x y)) =o
   3.622 +      O(%x. SUM y : A x. abs(l x y * h(k x y)))"
   3.623 +  apply (rule bigo_setsum1)
   3.624 +  apply (rule allI)+
   3.625 +  apply (rule abs_ge_zero)
   3.626 +  apply (unfold bigo_def)
   3.627 +  apply auto
   3.628 +  apply (rule_tac x = c in exI)
   3.629 +  apply (rule allI)+
   3.630 +  apply (subst abs_mult)+
   3.631 +  apply (subst mult_left_commute)
   3.632 +  apply (rule mult_left_mono)
   3.633 +  apply (erule spec)
   3.634 +  apply (rule abs_ge_zero)
   3.635 +done
   3.636 +
   3.637 +lemma bigo_setsum4: "f =o g +o O(h) ==>
   3.638 +    (%x. SUM y : A x. l x y * f(k x y)) =o
   3.639 +      (%x. SUM y : A x. l x y * g(k x y)) +o
   3.640 +        O(%x. SUM y : A x. abs(l x y * h(k x y)))"
   3.641 +  apply (rule set_minus_imp_plus)
   3.642 +  apply (subst func_diff)
   3.643 +  apply (subst setsum_subtractf [symmetric])
   3.644 +  apply (subst right_diff_distrib [symmetric])
   3.645 +  apply (rule bigo_setsum3)
   3.646 +  apply (subst func_diff [symmetric])
   3.647 +  apply (erule set_plus_imp_minus)
   3.648 +done
   3.649 +
   3.650 +lemma bigo_setsum5: "f =o O(h) ==> ALL x y. 0 <= l x y ==> 
   3.651 +    ALL x. 0 <= h x ==>
   3.652 +      (%x. SUM y : A x. (l x y) * f(k x y)) =o
   3.653 +        O(%x. SUM y : A x. (l x y) * h(k x y))" 
   3.654 +  apply (subgoal_tac "(%x. SUM y : A x. (l x y) * h(k x y)) = 
   3.655 +      (%x. SUM y : A x. abs((l x y) * h(k x y)))")
   3.656 +  apply (erule ssubst)
   3.657 +  apply (erule bigo_setsum3)
   3.658 +  apply (rule ext)
   3.659 +  apply (rule setsum_cong2)
   3.660 +  apply (subst abs_of_nonneg)
   3.661 +  apply (rule mult_nonneg_nonneg)
   3.662 +  apply auto
   3.663 +done
   3.664 +
   3.665 +lemma bigo_setsum6: "f =o g +o O(h) ==> ALL x y. 0 <= l x y ==>
   3.666 +    ALL x. 0 <= h x ==>
   3.667 +      (%x. SUM y : A x. (l x y) * f(k x y)) =o
   3.668 +        (%x. SUM y : A x. (l x y) * g(k x y)) +o
   3.669 +          O(%x. SUM y : A x. (l x y) * h(k x y))" 
   3.670 +  apply (rule set_minus_imp_plus)
   3.671 +  apply (subst func_diff)
   3.672 +  apply (subst setsum_subtractf [symmetric])
   3.673 +  apply (subst right_diff_distrib [symmetric])
   3.674 +  apply (rule bigo_setsum5)
   3.675 +  apply (subst func_diff [symmetric])
   3.676 +  apply (drule set_plus_imp_minus)
   3.677 +  apply auto
   3.678 +done
   3.679 +
   3.680 +subsection {* Misc useful stuff *}
   3.681 +
   3.682 +lemma bigo_useful_intro: "A <= O(f) ==> B <= O(f) ==>
   3.683 +  A + B <= O(f)"
   3.684 +  apply (subst bigo_plus_idemp [symmetric])
   3.685 +  apply (rule set_plus_mono2)
   3.686 +  apply assumption+
   3.687 +done
   3.688 +
   3.689 +lemma bigo_useful_add: "f =o O(h) ==> g =o O(h) ==> f + g =o O(h)"
   3.690 +  apply (subst bigo_plus_idemp [symmetric])
   3.691 +  apply (rule set_plus_intro)
   3.692 +  apply assumption+
   3.693 +done
   3.694 +  
   3.695 +lemma bigo_useful_const_mult: "(c::'a::ordered_field) ~= 0 ==> 
   3.696 +    (%x. c) * f =o O(h) ==> f =o O(h)"
   3.697 +  apply (rule subsetD)
   3.698 +  apply (subgoal_tac "(%x. 1 / c) *o O(h) <= O(h)")
   3.699 +  apply assumption
   3.700 +  apply (rule bigo_const_mult6)
   3.701 +  apply (subgoal_tac "f = (%x. 1 / c) * ((%x. c) * f)")
   3.702 +  apply (erule ssubst)
   3.703 +  apply (erule set_times_intro2)
   3.704 +  apply (simp add: func_times) 
   3.705 +  apply (rule ext)
   3.706 +  apply (subst times_divide_eq_left [symmetric])
   3.707 +  apply (subst divide_self)
   3.708 +  apply (assumption, simp)
   3.709 +done
   3.710 +
   3.711 +lemma bigo_fix: "(%x. f ((x::nat) + 1)) =o O(%x. h(x + 1)) ==> f 0 = 0 ==>
   3.712 +    f =o O(h)"
   3.713 +  apply (simp add: bigo_alt_def)
   3.714 +  apply auto
   3.715 +  apply (rule_tac x = c in exI)
   3.716 +  apply auto
   3.717 +  apply (case_tac "x = 0")
   3.718 +  apply simp
   3.719 +  apply (rule mult_nonneg_nonneg)
   3.720 +  apply force
   3.721 +  apply force
   3.722 +  apply (subgoal_tac "x = Suc (x - 1)")
   3.723 +  apply (erule ssubst)back
   3.724 +  apply (erule spec)
   3.725 +  apply simp
   3.726 +done
   3.727 +
   3.728 +lemma bigo_fix2: 
   3.729 +    "(%x. f ((x::nat) + 1)) =o (%x. g(x + 1)) +o O(%x. h(x + 1)) ==> 
   3.730 +       f 0 = g 0 ==> f =o g +o O(h)"
   3.731 +  apply (rule set_minus_imp_plus)
   3.732 +  apply (rule bigo_fix)
   3.733 +  apply (subst func_diff)
   3.734 +  apply (subst func_diff [symmetric])
   3.735 +  apply (rule set_plus_imp_minus)
   3.736 +  apply simp
   3.737 +  apply (simp add: func_diff)
   3.738 +done
   3.739 +
   3.740 +subsection {* Less than or equal to *}
   3.741 +
   3.742 +constdefs 
   3.743 +  lesso :: "('a => 'b::ordered_idom) => ('a => 'b) => ('a => 'b)"
   3.744 +      (infixl "<o" 70)
   3.745 +  "f <o g == (%x. max (f x - g x) 0)"
   3.746 +
   3.747 +lemma bigo_lesseq1: "f =o O(h) ==> ALL x. abs (g x) <= abs (f x) ==>
   3.748 +    g =o O(h)"
   3.749 +  apply (unfold bigo_def)
   3.750 +  apply clarsimp
   3.751 +  apply (rule_tac x = c in exI)
   3.752 +  apply (rule allI)
   3.753 +  apply (rule order_trans)
   3.754 +  apply (erule spec)+
   3.755 +done
   3.756 +
   3.757 +lemma bigo_lesseq2: "f =o O(h) ==> ALL x. abs (g x) <= f x ==>
   3.758 +      g =o O(h)"
   3.759 +  apply (erule bigo_lesseq1)
   3.760 +  apply (rule allI)
   3.761 +  apply (drule_tac x = x in spec)
   3.762 +  apply (rule order_trans)
   3.763 +  apply assumption
   3.764 +  apply (rule abs_ge_self)
   3.765 +done
   3.766 +
   3.767 +lemma bigo_lesseq3: "f =o O(h) ==> ALL x. 0 <= g x ==> ALL x. g x <= f x ==>
   3.768 +      g =o O(h)"
   3.769 +  apply (erule bigo_lesseq2)
   3.770 +  apply (rule allI)
   3.771 +  apply (subst abs_of_nonneg)
   3.772 +  apply (erule spec)+
   3.773 +done
   3.774 +
   3.775 +lemma bigo_lesseq4: "f =o O(h) ==>
   3.776 +    ALL x. 0 <= g x ==> ALL x. g x <= abs (f x) ==>
   3.777 +      g =o O(h)"
   3.778 +  apply (erule bigo_lesseq1)
   3.779 +  apply (rule allI)
   3.780 +  apply (subst abs_of_nonneg)
   3.781 +  apply (erule spec)+
   3.782 +done
   3.783 +
   3.784 +lemma bigo_lesso1: "ALL x. f x <= g x ==> f <o g =o O(h)"
   3.785 +  apply (unfold lesso_def)
   3.786 +  apply (subgoal_tac "(%x. max (f x - g x) 0) = 0")
   3.787 +  apply (erule ssubst)
   3.788 +  apply (rule bigo_zero)
   3.789 +  apply (unfold func_zero)
   3.790 +  apply (rule ext)
   3.791 +  apply (simp split: split_max)
   3.792 +done
   3.793 +
   3.794 +lemma bigo_lesso2: "f =o g +o O(h) ==>
   3.795 +    ALL x. 0 <= k x ==> ALL x. k x <= f x ==>
   3.796 +      k <o g =o O(h)"
   3.797 +  apply (unfold lesso_def)
   3.798 +  apply (rule bigo_lesseq4)
   3.799 +  apply (erule set_plus_imp_minus)
   3.800 +  apply (rule allI)
   3.801 +  apply (rule le_maxI2)
   3.802 +  apply (rule allI)
   3.803 +  apply (subst func_diff)
   3.804 +  apply (case_tac "0 <= k x - g x")
   3.805 +  apply simp
   3.806 +  apply (subst abs_of_nonneg)
   3.807 +  apply (drule_tac x = x in spec)back
   3.808 +  apply (simp add: compare_rls)
   3.809 +  apply (subst diff_minus)+
   3.810 +  apply (rule add_right_mono)
   3.811 +  apply (erule spec)
   3.812 +  apply (rule order_trans) 
   3.813 +  prefer 2
   3.814 +  apply (rule abs_ge_zero)
   3.815 +  apply (simp add: compare_rls)
   3.816 +done
   3.817 +
   3.818 +lemma bigo_lesso3: "f =o g +o O(h) ==>
   3.819 +    ALL x. 0 <= k x ==> ALL x. g x <= k x ==>
   3.820 +      f <o k =o O(h)"
   3.821 +  apply (unfold lesso_def)
   3.822 +  apply (rule bigo_lesseq4)
   3.823 +  apply (erule set_plus_imp_minus)
   3.824 +  apply (rule allI)
   3.825 +  apply (rule le_maxI2)
   3.826 +  apply (rule allI)
   3.827 +  apply (subst func_diff)
   3.828 +  apply (case_tac "0 <= f x - k x")
   3.829 +  apply simp
   3.830 +  apply (subst abs_of_nonneg)
   3.831 +  apply (drule_tac x = x in spec)back
   3.832 +  apply (simp add: compare_rls)
   3.833 +  apply (subst diff_minus)+
   3.834 +  apply (rule add_left_mono)
   3.835 +  apply (rule le_imp_neg_le)
   3.836 +  apply (erule spec)
   3.837 +  apply (rule order_trans) 
   3.838 +  prefer 2
   3.839 +  apply (rule abs_ge_zero)
   3.840 +  apply (simp add: compare_rls)
   3.841 +done
   3.842 +
   3.843 +lemma bigo_lesso4: "f <o g =o O(k::'a=>'b::ordered_field) ==>
   3.844 +    g =o h +o O(k) ==> f <o h =o O(k)"
   3.845 +  apply (unfold lesso_def)
   3.846 +  apply (drule set_plus_imp_minus)
   3.847 +  apply (drule bigo_abs5)back
   3.848 +  apply (simp add: func_diff)
   3.849 +  apply (drule bigo_useful_add)
   3.850 +  apply assumption
   3.851 +  apply (erule bigo_lesseq2)back
   3.852 +  apply (rule allI)
   3.853 +  apply (auto simp add: func_plus func_diff compare_rls 
   3.854 +    split: split_max abs_split)
   3.855 +done
   3.856 +
   3.857 +lemma bigo_lesso5: "f <o g =o O(h) ==>
   3.858 +    EX C. ALL x. f x <= g x + C * abs(h x)"
   3.859 +  apply (simp only: lesso_def bigo_alt_def)
   3.860 +  apply clarsimp
   3.861 +  apply (rule_tac x = c in exI)
   3.862 +  apply (rule allI)
   3.863 +  apply (drule_tac x = x in spec)
   3.864 +  apply (subgoal_tac "abs(max (f x - g x) 0) = max (f x - g x) 0")
   3.865 +  apply (clarsimp simp add: compare_rls add_ac) 
   3.866 +  apply (rule abs_of_nonneg)
   3.867 +  apply (rule le_maxI2)
   3.868 +done
   3.869 +
   3.870 +lemma lesso_add: "f <o g =o O(h) ==>
   3.871 +      k <o l =o O(h) ==> (f + k) <o (g + l) =o O(h)"
   3.872 +  apply (unfold lesso_def)
   3.873 +  apply (rule bigo_lesseq3)
   3.874 +  apply (erule bigo_useful_add)
   3.875 +  apply assumption
   3.876 +  apply (force split: split_max)
   3.877 +  apply (auto split: split_max simp add: func_plus)
   3.878 +done
   3.879 +
   3.880 +(* 
   3.881 +These last two lemmas require the HOL-Complex library.
   3.882 +
   3.883 +lemma bigo_LIMSEQ1: "f =o O(g) ==> g ----> 0 ==> f ----> 0"
   3.884 +  apply (simp add: LIMSEQ_def bigo_alt_def)
   3.885 +  apply clarify
   3.886 +  apply (drule_tac x = "r / c" in spec)
   3.887 +  apply (drule mp)
   3.888 +  apply (erule divide_pos_pos)
   3.889 +  apply assumption
   3.890 +  apply clarify
   3.891 +  apply (rule_tac x = no in exI)
   3.892 +  apply (rule allI)
   3.893 +  apply (drule_tac x = n in spec)+
   3.894 +  apply (rule impI)
   3.895 +  apply (drule mp)
   3.896 +  apply assumption
   3.897 +  apply (rule order_le_less_trans)
   3.898 +  apply assumption
   3.899 +  apply (rule order_less_le_trans)
   3.900 +  apply (subgoal_tac "c * abs(g n) < c * (r / c)")
   3.901 +  apply assumption
   3.902 +  apply (erule mult_strict_left_mono)
   3.903 +  apply assumption
   3.904 +  apply simp
   3.905 +done
   3.906 +
   3.907 +lemma bigo_LIMSEQ2: "f =o g +o O(h) ==> h ----> 0 ==> f ----> a 
   3.908 +    ==> g ----> a"
   3.909 +  apply (drule set_plus_imp_minus)
   3.910 +  apply (drule bigo_LIMSEQ1)
   3.911 +  apply assumption
   3.912 +  apply (simp only: func_diff)
   3.913 +  apply (erule LIMSEQ_diff_approach_zero2)
   3.914 +  apply assumption
   3.915 +done
   3.916 +
   3.917 +*)
   3.918 +
   3.919 +end
     4.1 --- a/src/HOL/Library/Library.thy	Mon Jul 25 15:51:30 2005 +0200
     4.2 +++ b/src/HOL/Library/Library.thy	Mon Jul 25 18:54:49 2005 +0200
     4.3 @@ -2,6 +2,7 @@
     4.4  theory Library
     4.5  imports
     4.6    Accessible_Part
     4.7 +  BigO
     4.8    Continuity
     4.9    EfficientNat
    4.10    FuncSet
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Library/SetsAndFunctions.thy	Mon Jul 25 18:54:49 2005 +0200
     5.3 @@ -0,0 +1,376 @@
     5.4 +(*  Title:      SetsAndFunctions.thy
     5.5 +    Author:     Jeremy Avigad and Kevin Donnelly
     5.6 +*)
     5.7 +
     5.8 +header {* Operations on sets and functions *}
     5.9 +
    5.10 +theory SetsAndFunctions
    5.11 +imports Main
    5.12 +begin
    5.13 +
    5.14 +text {* 
    5.15 +This library lifts operations like addition and muliplication to sets and
    5.16 +functions of appropriate types. It was designed to support asymptotic
    5.17 +calculations. See the comments at the top of BigO.thy
    5.18 +*}
    5.19 +
    5.20 +subsection {* Basic definitions *} 
    5.21 +
    5.22 +instance set :: (plus)plus
    5.23 +by intro_classes
    5.24 +
    5.25 +instance fun :: (type,plus)plus
    5.26 +by intro_classes
    5.27 +
    5.28 +defs (overloaded)
    5.29 +  func_plus: "f + g == (%x. f x + g x)"
    5.30 +  set_plus: "A + B == {c. EX a:A. EX b:B. c = a + b}"
    5.31 +
    5.32 +instance set :: (times)times
    5.33 +by intro_classes
    5.34 +
    5.35 +instance fun :: (type,times)times
    5.36 +by intro_classes
    5.37 +
    5.38 +defs (overloaded)
    5.39 +  func_times: "f * g == (%x. f x * g x)" 
    5.40 +  set_times:"A * B == {c. EX a:A. EX b:B. c = a * b}"
    5.41 +
    5.42 +instance fun :: (type,minus)minus
    5.43 +by intro_classes
    5.44 +
    5.45 +defs (overloaded)
    5.46 +  func_minus: "- f == (%x. - f x)"
    5.47 +  func_diff: "f - g == %x. f x - g x"                 
    5.48 +
    5.49 +instance fun :: (type,zero)zero
    5.50 +by intro_classes
    5.51 +
    5.52 +instance set :: (zero)zero
    5.53 +by(intro_classes)
    5.54 +
    5.55 +defs (overloaded)
    5.56 +  func_zero: "0::(('a::type) => ('b::zero)) == %x. 0"
    5.57 +  set_zero: "0::('a::zero)set == {0}"
    5.58 +
    5.59 +instance fun :: (type,one)one
    5.60 +by intro_classes
    5.61 +
    5.62 +instance set :: (one)one
    5.63 +by intro_classes
    5.64 +
    5.65 +defs (overloaded)
    5.66 +  func_one: "1::(('a::type) => ('b::one)) == %x. 1"
    5.67 +  set_one: "1::('a::one)set == {1}"
    5.68 +
    5.69 +constdefs 
    5.70 +  elt_set_plus :: "'a::plus => 'a set => 'a set"    (infixl "+o" 70)
    5.71 +  "a +o B == {c. EX b:B. c = a + b}"
    5.72 +
    5.73 +  elt_set_times :: "'a::times => 'a set => 'a set"  (infixl "*o" 80)
    5.74 +  "a *o B == {c. EX b:B. c = a * b}"
    5.75 +
    5.76 +syntax
    5.77 +  "elt_set_eq" :: "'a => 'a set => bool"      (infix "=o" 50)
    5.78 +
    5.79 +translations
    5.80 +  "x =o A" => "x : A"
    5.81 +
    5.82 +instance fun :: (type,semigroup_add)semigroup_add
    5.83 +  apply intro_classes
    5.84 +  apply (auto simp add: func_plus add_assoc)
    5.85 +done
    5.86 +
    5.87 +instance fun :: (type,comm_monoid_add)comm_monoid_add
    5.88 +  apply intro_classes
    5.89 +  apply (auto simp add: func_zero func_plus add_ac)
    5.90 +done
    5.91 +
    5.92 +instance fun :: (type,ab_group_add)ab_group_add
    5.93 +  apply intro_classes
    5.94 +  apply (simp add: func_minus func_plus func_zero)
    5.95 +  apply (simp add: func_minus func_plus func_diff diff_minus)
    5.96 +done
    5.97 +
    5.98 +instance fun :: (type,semigroup_mult)semigroup_mult
    5.99 +  apply intro_classes
   5.100 +  apply (auto simp add: func_times mult_assoc)
   5.101 +done
   5.102 +
   5.103 +instance fun :: (type,comm_monoid_mult)comm_monoid_mult
   5.104 +  apply intro_classes
   5.105 +  apply (auto simp add: func_one func_times mult_ac)
   5.106 +done
   5.107 +
   5.108 +instance fun :: (type,comm_ring_1)comm_ring_1
   5.109 +  apply intro_classes
   5.110 +  apply (auto simp add: func_plus func_times func_minus func_diff ext 
   5.111 +    func_one func_zero ring_eq_simps) 
   5.112 +  apply (drule fun_cong)
   5.113 +  apply simp
   5.114 +done
   5.115 +
   5.116 +instance set :: (semigroup_add)semigroup_add
   5.117 +  apply intro_classes
   5.118 +  apply (unfold set_plus)
   5.119 +  apply (force simp add: add_assoc)
   5.120 +done
   5.121 +
   5.122 +instance set :: (semigroup_mult)semigroup_mult
   5.123 +  apply intro_classes
   5.124 +  apply (unfold set_times)
   5.125 +  apply (force simp add: mult_assoc)
   5.126 +done
   5.127 +
   5.128 +instance set :: (comm_monoid_add)comm_monoid_add
   5.129 +  apply intro_classes
   5.130 +  apply (unfold set_plus)
   5.131 +  apply (force simp add: add_ac)
   5.132 +  apply (unfold set_zero)
   5.133 +  apply force
   5.134 +done
   5.135 +
   5.136 +instance set :: (comm_monoid_mult)comm_monoid_mult
   5.137 +  apply intro_classes
   5.138 +  apply (unfold set_times)
   5.139 +  apply (force simp add: mult_ac)
   5.140 +  apply (unfold set_one)
   5.141 +  apply force
   5.142 +done
   5.143 +
   5.144 +subsection {* Basic properties *}
   5.145 +
   5.146 +lemma set_plus_intro [intro]: "a : C ==> b : D ==> a + b : C + D" 
   5.147 +by (auto simp add: set_plus)
   5.148 +
   5.149 +lemma set_plus_intro2 [intro]: "b : C ==> a + b : a +o C"
   5.150 +by (auto simp add: elt_set_plus_def)
   5.151 +
   5.152 +lemma set_plus_rearrange: "((a::'a::comm_monoid_add) +o C) + 
   5.153 +  (b +o D) = (a + b) +o (C + D)"
   5.154 +  apply (auto simp add: elt_set_plus_def set_plus add_ac)
   5.155 +  apply (rule_tac x = "ba + bb" in exI)
   5.156 +  apply (auto simp add: add_ac)
   5.157 +  apply (rule_tac x = "aa + a" in exI)
   5.158 +  apply (auto simp add: add_ac)
   5.159 +done
   5.160 +
   5.161 +lemma set_plus_rearrange2: "(a::'a::semigroup_add) +o (b +o C) = 
   5.162 +  (a + b) +o C"
   5.163 +by (auto simp add: elt_set_plus_def add_assoc)
   5.164 +
   5.165 +lemma set_plus_rearrange3: "((a::'a::semigroup_add) +o B) + C = 
   5.166 +  a +o (B + C)"
   5.167 +  apply (auto simp add: elt_set_plus_def set_plus)
   5.168 +  apply (blast intro: add_ac)
   5.169 +  apply (rule_tac x = "a + aa" in exI)
   5.170 +  apply (rule conjI)
   5.171 +  apply (rule_tac x = "aa" in bexI)
   5.172 +  apply auto
   5.173 +  apply (rule_tac x = "ba" in bexI)
   5.174 +  apply (auto simp add: add_ac)
   5.175 +done
   5.176 +
   5.177 +theorem set_plus_rearrange4: "C + ((a::'a::comm_monoid_add) +o D) = 
   5.178 +    a +o (C + D)" 
   5.179 +  apply (auto intro!: subsetI simp add: elt_set_plus_def set_plus add_ac)
   5.180 +  apply (rule_tac x = "aa + ba" in exI)
   5.181 +  apply (auto simp add: add_ac)
   5.182 +done
   5.183 +
   5.184 +theorems set_plus_rearranges = set_plus_rearrange set_plus_rearrange2
   5.185 +  set_plus_rearrange3 set_plus_rearrange4
   5.186 +
   5.187 +lemma set_plus_mono [intro!]: "C <= D ==> a +o C <= a +o D"
   5.188 +by (auto simp add: elt_set_plus_def)
   5.189 +
   5.190 +lemma set_plus_mono2 [intro]: "(C::('a::plus) set) <= D ==> E <= F ==> 
   5.191 +    C + E <= D + F"
   5.192 +by (auto simp add: set_plus)
   5.193 +
   5.194 +lemma set_plus_mono3 [intro]: "a : C ==> a +o D <= C + D"
   5.195 +by (auto simp add: elt_set_plus_def set_plus)
   5.196 +
   5.197 +lemma set_plus_mono4 [intro]: "(a::'a::comm_monoid_add) : C ==> 
   5.198 +  a +o D <= D + C" 
   5.199 +by (auto simp add: elt_set_plus_def set_plus add_ac)
   5.200 +
   5.201 +lemma set_plus_mono5: "a:C ==> B <= D ==> a +o B <= C + D"
   5.202 +  apply (subgoal_tac "a +o B <= a +o D")
   5.203 +  apply (erule order_trans)
   5.204 +  apply (erule set_plus_mono3)
   5.205 +  apply (erule set_plus_mono)
   5.206 +done
   5.207 +
   5.208 +lemma set_plus_mono_b: "C <= D ==> x : a +o C 
   5.209 +    ==> x : a +o D"
   5.210 +  apply (frule set_plus_mono)
   5.211 +  apply auto
   5.212 +done
   5.213 +
   5.214 +lemma set_plus_mono2_b: "C <= D ==> E <= F ==> x : C + E ==> 
   5.215 +    x : D + F"
   5.216 +  apply (frule set_plus_mono2)
   5.217 +  prefer 2
   5.218 +  apply force
   5.219 +  apply assumption
   5.220 +done
   5.221 +
   5.222 +lemma set_plus_mono3_b: "a : C ==> x : a +o D ==> x : C + D"
   5.223 +  apply (frule set_plus_mono3)
   5.224 +  apply auto
   5.225 +done
   5.226 +
   5.227 +lemma set_plus_mono4_b: "(a::'a::comm_monoid_add) : C ==> 
   5.228 +  x : a +o D ==> x : D + C" 
   5.229 +  apply (frule set_plus_mono4)
   5.230 +  apply auto
   5.231 +done
   5.232 +
   5.233 +lemma set_zero_plus [simp]: "(0::'a::comm_monoid_add) +o C = C"
   5.234 +by (auto simp add: elt_set_plus_def)
   5.235 +
   5.236 +lemma set_zero_plus2: "(0::'a::comm_monoid_add) : A ==> B <= A + B"
   5.237 +  apply (auto intro!: subsetI simp add: set_plus)
   5.238 +  apply (rule_tac x = 0 in bexI)
   5.239 +  apply (rule_tac x = x in bexI)
   5.240 +  apply (auto simp add: add_ac)
   5.241 +done
   5.242 +
   5.243 +lemma set_plus_imp_minus: "(a::'a::ab_group_add) : b +o C ==> (a - b) : C"
   5.244 +by (auto simp add: elt_set_plus_def add_ac diff_minus)
   5.245 +
   5.246 +lemma set_minus_imp_plus: "(a::'a::ab_group_add) - b : C ==> a : b +o C"
   5.247 +  apply (auto simp add: elt_set_plus_def add_ac diff_minus)
   5.248 +  apply (subgoal_tac "a = (a + - b) + b")
   5.249 +  apply (rule bexI, assumption, assumption)
   5.250 +  apply (auto simp add: add_ac)
   5.251 +done
   5.252 +
   5.253 +lemma set_minus_plus: "((a::'a::ab_group_add) - b : C) = (a : b +o C)"
   5.254 +by (rule iffI, rule set_minus_imp_plus, assumption, rule set_plus_imp_minus, 
   5.255 +    assumption)
   5.256 +
   5.257 +lemma set_times_intro [intro]: "a : C ==> b : D ==> a * b : C * D" 
   5.258 +by (auto simp add: set_times)
   5.259 +
   5.260 +lemma set_times_intro2 [intro!]: "b : C ==> a * b : a *o C"
   5.261 +by (auto simp add: elt_set_times_def)
   5.262 +
   5.263 +lemma set_times_rearrange: "((a::'a::comm_monoid_mult) *o C) * 
   5.264 +  (b *o D) = (a * b) *o (C * D)"
   5.265 +  apply (auto simp add: elt_set_times_def set_times)
   5.266 +  apply (rule_tac x = "ba * bb" in exI)
   5.267 +  apply (auto simp add: mult_ac)
   5.268 +  apply (rule_tac x = "aa * a" in exI)
   5.269 +  apply (auto simp add: mult_ac)
   5.270 +done
   5.271 +
   5.272 +lemma set_times_rearrange2: "(a::'a::semigroup_mult) *o (b *o C) = 
   5.273 +  (a * b) *o C"
   5.274 +by (auto simp add: elt_set_times_def mult_assoc)
   5.275 +
   5.276 +lemma set_times_rearrange3: "((a::'a::semigroup_mult) *o B) * C = 
   5.277 +  a *o (B * C)"
   5.278 +  apply (auto simp add: elt_set_times_def set_times)
   5.279 +  apply (blast intro: mult_ac)
   5.280 +  apply (rule_tac x = "a * aa" in exI)
   5.281 +  apply (rule conjI)
   5.282 +  apply (rule_tac x = "aa" in bexI)
   5.283 +  apply auto
   5.284 +  apply (rule_tac x = "ba" in bexI)
   5.285 +  apply (auto simp add: mult_ac)
   5.286 +done
   5.287 +
   5.288 +theorem set_times_rearrange4: "C * ((a::'a::comm_monoid_mult) *o D) = 
   5.289 +    a *o (C * D)" 
   5.290 +  apply (auto intro!: subsetI simp add: elt_set_times_def set_times 
   5.291 +    mult_ac)
   5.292 +  apply (rule_tac x = "aa * ba" in exI)
   5.293 +  apply (auto simp add: mult_ac)
   5.294 +done
   5.295 +
   5.296 +theorems set_times_rearranges = set_times_rearrange set_times_rearrange2
   5.297 +  set_times_rearrange3 set_times_rearrange4
   5.298 +
   5.299 +lemma set_times_mono [intro]: "C <= D ==> a *o C <= a *o D"
   5.300 +by (auto simp add: elt_set_times_def)
   5.301 +
   5.302 +lemma set_times_mono2 [intro]: "(C::('a::times) set) <= D ==> E <= F ==> 
   5.303 +    C * E <= D * F"
   5.304 +by (auto simp add: set_times)
   5.305 +
   5.306 +lemma set_times_mono3 [intro]: "a : C ==> a *o D <= C * D"
   5.307 +by (auto simp add: elt_set_times_def set_times)
   5.308 +
   5.309 +lemma set_times_mono4 [intro]: "(a::'a::comm_monoid_mult) : C ==> 
   5.310 +  a *o D <= D * C" 
   5.311 +by (auto simp add: elt_set_times_def set_times mult_ac)
   5.312 +
   5.313 +lemma set_times_mono5: "a:C ==> B <= D ==> a *o B <= C * D"
   5.314 +  apply (subgoal_tac "a *o B <= a *o D")
   5.315 +  apply (erule order_trans)
   5.316 +  apply (erule set_times_mono3)
   5.317 +  apply (erule set_times_mono)
   5.318 +done
   5.319 +
   5.320 +lemma set_times_mono_b: "C <= D ==> x : a *o C 
   5.321 +    ==> x : a *o D"
   5.322 +  apply (frule set_times_mono)
   5.323 +  apply auto
   5.324 +done
   5.325 +
   5.326 +lemma set_times_mono2_b: "C <= D ==> E <= F ==> x : C * E ==> 
   5.327 +    x : D * F"
   5.328 +  apply (frule set_times_mono2)
   5.329 +  prefer 2
   5.330 +  apply force
   5.331 +  apply assumption
   5.332 +done
   5.333 +
   5.334 +lemma set_times_mono3_b: "a : C ==> x : a *o D ==> x : C * D"
   5.335 +  apply (frule set_times_mono3)
   5.336 +  apply auto
   5.337 +done
   5.338 +
   5.339 +lemma set_times_mono4_b: "(a::'a::comm_monoid_mult) : C ==> 
   5.340 +  x : a *o D ==> x : D * C" 
   5.341 +  apply (frule set_times_mono4)
   5.342 +  apply auto
   5.343 +done
   5.344 +
   5.345 +lemma set_one_times [simp]: "(1::'a::comm_monoid_mult) *o C = C"
   5.346 +by (auto simp add: elt_set_times_def)
   5.347 +
   5.348 +lemma set_times_plus_distrib: "(a::'a::semiring) *o (b +o C)= 
   5.349 +  (a * b) +o (a *o C)"
   5.350 +by (auto simp add: elt_set_plus_def elt_set_times_def ring_distrib)
   5.351 +
   5.352 +lemma set_times_plus_distrib2: "(a::'a::semiring) *o (B + C) = 
   5.353 +  (a *o B) + (a *o C)"
   5.354 +  apply (auto simp add: set_plus elt_set_times_def ring_distrib)
   5.355 +  apply blast
   5.356 +  apply (rule_tac x = "b + bb" in exI)
   5.357 +  apply (auto simp add: ring_distrib)
   5.358 +done
   5.359 +
   5.360 +lemma set_times_plus_distrib3: "((a::'a::semiring) +o C) * D <= 
   5.361 +    a *o D + C * D"
   5.362 +  apply (auto intro!: subsetI simp add: 
   5.363 +    elt_set_plus_def elt_set_times_def set_times 
   5.364 +    set_plus ring_distrib)
   5.365 +  apply auto
   5.366 +done
   5.367 +
   5.368 +theorems set_times_plus_distribs = set_times_plus_distrib
   5.369 +  set_times_plus_distrib2
   5.370 +
   5.371 +lemma set_neg_intro: "(a::'a::ring_1) : (- 1) *o C ==> 
   5.372 +    - a : C" 
   5.373 +by (auto simp add: elt_set_times_def)
   5.374 +
   5.375 +lemma set_neg_intro2: "(a::'a::ring_1) : C ==>
   5.376 +    - a : (- 1) *o C"
   5.377 +by (auto simp add: elt_set_times_def)
   5.378 +  
   5.379 +end