1.1 --- a/src/HOL/Library/BigO.thy Fri Apr 13 21:26:34 2007 +0200
1.2 +++ b/src/HOL/Library/BigO.thy Fri Apr 13 21:26:35 2007 +0200
1.3 @@ -59,11 +59,11 @@
1.4 apply (rule mult_right_mono)
1.5 apply (rule abs_ge_self)
1.6 apply (rule abs_ge_zero)
1.7 -done
1.8 + done
1.9
1.10 lemma bigo_alt_def: "O(f) =
1.11 {h. EX c. (0 < c & (ALL x. abs (h x) <= c * abs (f x)))}"
1.12 -by (auto simp add: bigo_def bigo_pos_const)
1.13 + by (auto simp add: bigo_def bigo_pos_const)
1.14
1.15 lemma bigo_elt_subset [intro]: "f : O(g) ==> O(f) <= O(g)"
1.16 apply (auto simp add: bigo_alt_def)
1.17 @@ -78,25 +78,25 @@
1.18 apply (simp add: mult_ac)
1.19 apply (rule mult_left_mono, assumption)
1.20 apply (rule order_less_imp_le, assumption)
1.21 -done
1.22 + done
1.23
1.24 lemma bigo_refl [intro]: "f : O(f)"
1.25 apply(auto simp add: bigo_def)
1.26 apply(rule_tac x = 1 in exI)
1.27 apply simp
1.28 -done
1.29 + done
1.30
1.31 lemma bigo_zero: "0 : O(g)"
1.32 apply (auto simp add: bigo_def func_zero)
1.33 apply (rule_tac x = 0 in exI)
1.34 apply auto
1.35 -done
1.36 + done
1.37
1.38 lemma bigo_zero2: "O(%x.0) = {%x.0}"
1.39 apply (auto simp add: bigo_def)
1.40 apply (rule ext)
1.41 apply auto
1.42 -done
1.43 + done
1.44
1.45 lemma bigo_plus_self_subset [intro]:
1.46 "O(f) + O(f) <= O(f)"
1.47 @@ -116,7 +116,7 @@
1.48 apply (rule bigo_plus_self_subset)
1.49 apply (rule set_zero_plus2)
1.50 apply (rule bigo_zero)
1.51 -done
1.52 + done
1.53
1.54 lemma bigo_plus_subset [intro]: "O(f + g) <= O(f) + O(g)"
1.55 apply (rule subsetI)
1.56 @@ -168,17 +168,17 @@
1.57 apply simp
1.58 apply (rule ext)
1.59 apply (auto simp add: if_splits linorder_not_le)
1.60 -done
1.61 + done
1.62
1.63 lemma bigo_plus_subset2 [intro]: "A <= O(f) ==> B <= O(f) ==> A + B <= O(f)"
1.64 apply (subgoal_tac "A + B <= O(f) + O(f)")
1.65 apply (erule order_trans)
1.66 apply simp
1.67 apply (auto del: subsetI simp del: bigo_plus_idemp)
1.68 -done
1.69 + done
1.70
1.71 lemma bigo_plus_eq: "ALL x. 0 <= f x ==> ALL x. 0 <= g x ==>
1.72 - O(f + g) = O(f) + O(g)"
1.73 + O(f + g) = O(f) + O(g)"
1.74 apply (rule equalityI)
1.75 apply (rule bigo_plus_subset)
1.76 apply (simp add: bigo_alt_def set_plus func_plus)
1.77 @@ -211,7 +211,7 @@
1.78 apply (rule abs_triangle_ineq)
1.79 apply (rule add_nonneg_nonneg)
1.80 apply assumption+
1.81 -done
1.82 + done
1.83
1.84 lemma bigo_bounded_alt: "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==>
1.85 f : O(g)"
1.86 @@ -220,13 +220,13 @@
1.87 apply auto
1.88 apply (drule_tac x = x in spec)+
1.89 apply (simp add: abs_mult [symmetric])
1.90 -done
1.91 + done
1.92
1.93 lemma bigo_bounded: "ALL x. 0 <= f x ==> ALL x. f x <= g x ==>
1.94 f : O(g)"
1.95 apply (erule bigo_bounded_alt [of f 1 g])
1.96 apply simp
1.97 -done
1.98 + done
1.99
1.100 lemma bigo_bounded2: "ALL x. lb x <= f x ==> ALL x. f x <= lb x + g x ==>
1.101 f : lb +o O(g)"
1.102 @@ -237,21 +237,21 @@
1.103 apply force
1.104 apply (drule_tac x = x in spec)+
1.105 apply force
1.106 -done
1.107 + done
1.108
1.109 lemma bigo_abs: "(%x. abs(f x)) =o O(f)"
1.110 apply (unfold bigo_def)
1.111 apply auto
1.112 apply (rule_tac x = 1 in exI)
1.113 apply auto
1.114 -done
1.115 + done
1.116
1.117 lemma bigo_abs2: "f =o O(%x. abs(f x))"
1.118 apply (unfold bigo_def)
1.119 apply auto
1.120 apply (rule_tac x = 1 in exI)
1.121 apply auto
1.122 -done
1.123 + done
1.124
1.125 lemma bigo_abs3: "O(f) = O(%x. abs(f x))"
1.126 apply (rule equalityI)
1.127 @@ -259,7 +259,7 @@
1.128 apply (rule bigo_abs2)
1.129 apply (rule bigo_elt_subset)
1.130 apply (rule bigo_abs)
1.131 -done
1.132 + done
1.133
1.134 lemma bigo_abs4: "f =o g +o O(h) ==>
1.135 (%x. abs (f x)) =o (%x. abs (g x)) +o O(h)"
1.136 @@ -288,7 +288,7 @@
1.137 qed
1.138
1.139 lemma bigo_abs5: "f =o O(g) ==> (%x. abs(f x)) =o O(g)"
1.140 -by (unfold bigo_def, auto)
1.141 + by (unfold bigo_def, auto)
1.142
1.143 lemma bigo_elt_subset2 [intro]: "f : g +o O(h) ==> O(f) <= O(g) + O(h)"
1.144 proof -
1.145 @@ -326,7 +326,7 @@
1.146 apply (rule mult_nonneg_nonneg)
1.147 apply auto
1.148 apply (simp add: mult_ac abs_mult)
1.149 -done
1.150 + done
1.151
1.152 lemma bigo_mult2 [intro]: "f *o O(g) <= O(f * g)"
1.153 apply (auto simp add: bigo_def elt_set_times_def func_times abs_mult)
1.154 @@ -337,20 +337,20 @@
1.155 apply (force simp add: mult_ac)
1.156 apply (rule mult_left_mono, assumption)
1.157 apply (rule abs_ge_zero)
1.158 -done
1.159 + done
1.160
1.161 lemma bigo_mult3: "f : O(h) ==> g : O(j) ==> f * g : O(h * j)"
1.162 apply (rule subsetD)
1.163 apply (rule bigo_mult)
1.164 apply (erule set_times_intro, assumption)
1.165 -done
1.166 + done
1.167
1.168 lemma bigo_mult4 [intro]:"f : k +o O(h) ==> g * f : (g * k) +o O(g * h)"
1.169 apply (drule set_plus_imp_minus)
1.170 apply (rule set_minus_imp_plus)
1.171 apply (drule bigo_mult3 [where g = g and j = g])
1.172 apply (auto simp add: ring_eq_simps mult_ac)
1.173 -done
1.174 + done
1.175
1.176 lemma bigo_mult5: "ALL x. f x ~= 0 ==>
1.177 O(f * g) <= (f::'a => ('b::ordered_field)) *o O(g)"
1.178 @@ -386,7 +386,7 @@
1.179 apply (rule equalityI)
1.180 apply (erule bigo_mult5)
1.181 apply (rule bigo_mult2)
1.182 -done
1.183 + done
1.184
1.185 lemma bigo_mult7: "ALL x. f x ~= 0 ==>
1.186 O(f * g) <= O(f::'a => ('b::ordered_field)) * O(g)"
1.187 @@ -394,14 +394,14 @@
1.188 apply assumption
1.189 apply (rule set_times_mono3)
1.190 apply (rule bigo_refl)
1.191 -done
1.192 + done
1.193
1.194 lemma bigo_mult8: "ALL x. f x ~= 0 ==>
1.195 O(f * g) = O(f::'a => ('b::ordered_field)) * O(g)"
1.196 apply (rule equalityI)
1.197 apply (erule bigo_mult7)
1.198 apply (rule bigo_mult)
1.199 -done
1.200 + done
1.201
1.202 lemma bigo_minus [intro]: "f : O(g) ==> - f : O(g)"
1.203 by (auto simp add: bigo_def func_minus)
1.204 @@ -411,7 +411,7 @@
1.205 apply (drule set_plus_imp_minus)
1.206 apply (drule bigo_minus)
1.207 apply (simp add: diff_minus)
1.208 -done
1.209 + done
1.210
1.211 lemma bigo_minus3: "O(-f) = O(f)"
1.212 by (auto simp add: bigo_def func_minus abs_minus_cancel)
1.213 @@ -452,12 +452,12 @@
1.214 apply (rule equalityI)
1.215 apply (erule bigo_plus_absorb_lemma1)
1.216 apply (erule bigo_plus_absorb_lemma2)
1.217 -done
1.218 + done
1.219
1.220 lemma bigo_plus_absorb2 [intro]: "f : O(g) ==> A <= O(g) ==> f +o A <= O(g)"
1.221 apply (subgoal_tac "f +o A <= f +o O(g)")
1.222 apply force+
1.223 -done
1.224 + done
1.225
1.226 lemma bigo_add_commute_imp: "f : g +o O(h) ==> g : f +o O(h)"
1.227 apply (subst set_minus_plus [symmetric])
1.228 @@ -467,56 +467,56 @@
1.229 apply (subst set_minus_plus)
1.230 apply assumption
1.231 apply (simp add: diff_minus add_ac)
1.232 -done
1.233 + done
1.234
1.235 lemma bigo_add_commute: "(f : g +o O(h)) = (g : f +o O(h))"
1.236 apply (rule iffI)
1.237 apply (erule bigo_add_commute_imp)+
1.238 -done
1.239 + done
1.240
1.241 lemma bigo_const1: "(%x. c) : O(%x. 1)"
1.242 -by (auto simp add: bigo_def mult_ac)
1.243 + by (auto simp add: bigo_def mult_ac)
1.244
1.245 lemma bigo_const2 [intro]: "O(%x. c) <= O(%x. 1)"
1.246 apply (rule bigo_elt_subset)
1.247 apply (rule bigo_const1)
1.248 -done
1.249 + done
1.250
1.251 lemma bigo_const3: "(c::'a::ordered_field) ~= 0 ==> (%x. 1) : O(%x. c)"
1.252 apply (simp add: bigo_def)
1.253 apply (rule_tac x = "abs(inverse c)" in exI)
1.254 apply (simp add: abs_mult [symmetric])
1.255 -done
1.256 + done
1.257
1.258 lemma bigo_const4: "(c::'a::ordered_field) ~= 0 ==> O(%x. 1) <= O(%x. c)"
1.259 -by (rule bigo_elt_subset, rule bigo_const3, assumption)
1.260 + by (rule bigo_elt_subset, rule bigo_const3, assumption)
1.261
1.262 lemma bigo_const [simp]: "(c::'a::ordered_field) ~= 0 ==>
1.263 O(%x. c) = O(%x. 1)"
1.264 -by (rule equalityI, rule bigo_const2, rule bigo_const4, assumption)
1.265 + by (rule equalityI, rule bigo_const2, rule bigo_const4, assumption)
1.266
1.267 lemma bigo_const_mult1: "(%x. c * f x) : O(f)"
1.268 apply (simp add: bigo_def)
1.269 apply (rule_tac x = "abs(c)" in exI)
1.270 apply (auto simp add: abs_mult [symmetric])
1.271 -done
1.272 + done
1.273
1.274 lemma bigo_const_mult2: "O(%x. c * f x) <= O(f)"
1.275 -by (rule bigo_elt_subset, rule bigo_const_mult1)
1.276 + by (rule bigo_elt_subset, rule bigo_const_mult1)
1.277
1.278 lemma bigo_const_mult3: "(c::'a::ordered_field) ~= 0 ==> f : O(%x. c * f x)"
1.279 apply (simp add: bigo_def)
1.280 apply (rule_tac x = "abs(inverse c)" in exI)
1.281 apply (simp add: abs_mult [symmetric] mult_assoc [symmetric])
1.282 -done
1.283 + done
1.284
1.285 lemma bigo_const_mult4: "(c::'a::ordered_field) ~= 0 ==>
1.286 O(f) <= O(%x. c * f x)"
1.287 -by (rule bigo_elt_subset, rule bigo_const_mult3, assumption)
1.288 + by (rule bigo_elt_subset, rule bigo_const_mult3, assumption)
1.289
1.290 lemma bigo_const_mult [simp]: "(c::'a::ordered_field) ~= 0 ==>
1.291 O(%x. c * f x) = O(f)"
1.292 -by (rule equalityI, rule bigo_const_mult2, erule bigo_const_mult4)
1.293 + by (rule equalityI, rule bigo_const_mult2, erule bigo_const_mult4)
1.294
1.295 lemma bigo_const_mult5 [simp]: "(c::'a::ordered_field) ~= 0 ==>
1.296 (%x. c) *o O(f) = O(f)"
1.297 @@ -533,7 +533,7 @@
1.298 apply (rule mult_left_mono)
1.299 apply (erule spec)
1.300 apply force
1.301 -done
1.302 + done
1.303
1.304 lemma bigo_const_mult6 [intro]: "(%x. c) *o O(f) <= O(f)"
1.305 apply (auto intro!: subsetI
1.306 @@ -547,7 +547,7 @@
1.307 apply (erule spec)
1.308 apply simp
1.309 apply(simp add: mult_ac)
1.310 -done
1.311 + done
1.312
1.313 lemma bigo_const_mult7 [intro]: "f =o O(g) ==> (%x. c * f x) =o O(g)"
1.314 proof -
1.315 @@ -571,6 +571,7 @@
1.316 apply (erule bigo_compose1)
1.317 done
1.318
1.319 +
1.320 subsection {* Setsum *}
1.321
1.322 lemma bigo_setsum_main: "ALL x. ALL y : A x. 0 <= h x y ==>
1.323 @@ -595,7 +596,7 @@
1.324 apply (rule mult_right_mono)
1.325 apply (rule abs_ge_self)
1.326 apply force
1.327 -done
1.328 + done
1.329
1.330 lemma bigo_setsum1: "ALL x y. 0 <= h x y ==>
1.331 EX c. ALL x y. abs(f x y) <= c * (h x y) ==>
1.332 @@ -605,12 +606,12 @@
1.333 apply clarsimp
1.334 apply (rule_tac x = c in exI)
1.335 apply force
1.336 -done
1.337 + done
1.338
1.339 lemma bigo_setsum2: "ALL y. 0 <= h y ==>
1.340 EX c. ALL y. abs(f y) <= c * (h y) ==>
1.341 (%x. SUM y : A x. f y) =o O(%x. SUM y : A x. h y)"
1.342 -by (rule bigo_setsum1, auto)
1.343 + by (rule bigo_setsum1, auto)
1.344
1.345 lemma bigo_setsum3: "f =o O(h) ==>
1.346 (%x. SUM y : A x. (l x y) * f(k x y)) =o
1.347 @@ -627,7 +628,7 @@
1.348 apply (rule mult_left_mono)
1.349 apply (erule spec)
1.350 apply (rule abs_ge_zero)
1.351 -done
1.352 + done
1.353
1.354 lemma bigo_setsum4: "f =o g +o O(h) ==>
1.355 (%x. SUM y : A x. l x y * f(k x y)) =o
1.356 @@ -640,7 +641,7 @@
1.357 apply (rule bigo_setsum3)
1.358 apply (subst func_diff [symmetric])
1.359 apply (erule set_plus_imp_minus)
1.360 -done
1.361 + done
1.362
1.363 lemma bigo_setsum5: "f =o O(h) ==> ALL x y. 0 <= l x y ==>
1.364 ALL x. 0 <= h x ==>
1.365 @@ -655,7 +656,7 @@
1.366 apply (subst abs_of_nonneg)
1.367 apply (rule mult_nonneg_nonneg)
1.368 apply auto
1.369 -done
1.370 + done
1.371
1.372 lemma bigo_setsum6: "f =o g +o O(h) ==> ALL x y. 0 <= l x y ==>
1.373 ALL x. 0 <= h x ==>
1.374 @@ -670,7 +671,8 @@
1.375 apply (subst func_diff [symmetric])
1.376 apply (drule set_plus_imp_minus)
1.377 apply auto
1.378 -done
1.379 + done
1.380 +
1.381
1.382 subsection {* Misc useful stuff *}
1.383
1.384 @@ -679,13 +681,13 @@
1.385 apply (subst bigo_plus_idemp [symmetric])
1.386 apply (rule set_plus_mono2)
1.387 apply assumption+
1.388 -done
1.389 + done
1.390
1.391 lemma bigo_useful_add: "f =o O(h) ==> g =o O(h) ==> f + g =o O(h)"
1.392 apply (subst bigo_plus_idemp [symmetric])
1.393 apply (rule set_plus_intro)
1.394 apply assumption+
1.395 -done
1.396 + done
1.397
1.398 lemma bigo_useful_const_mult: "(c::'a::ordered_field) ~= 0 ==>
1.399 (%x. c) * f =o O(h) ==> f =o O(h)"
1.400 @@ -701,7 +703,7 @@
1.401 apply (subst times_divide_eq_left [symmetric])
1.402 apply (subst divide_self)
1.403 apply (assumption, simp)
1.404 -done
1.405 + done
1.406
1.407 lemma bigo_fix: "(%x. f ((x::nat) + 1)) =o O(%x. h(x + 1)) ==> f 0 = 0 ==>
1.408 f =o O(h)"
1.409 @@ -718,7 +720,7 @@
1.410 apply (erule ssubst) back
1.411 apply (erule spec)
1.412 apply simp
1.413 -done
1.414 + done
1.415
1.416 lemma bigo_fix2:
1.417 "(%x. f ((x::nat) + 1)) =o (%x. g(x + 1)) +o O(%x. h(x + 1)) ==>
1.418 @@ -730,7 +732,8 @@
1.419 apply (rule set_plus_imp_minus)
1.420 apply simp
1.421 apply (simp add: func_diff)
1.422 -done
1.423 + done
1.424 +
1.425
1.426 subsection {* Less than or equal to *}
1.427
1.428 @@ -747,7 +750,7 @@
1.429 apply (rule allI)
1.430 apply (rule order_trans)
1.431 apply (erule spec)+
1.432 -done
1.433 + done
1.434
1.435 lemma bigo_lesseq2: "f =o O(h) ==> ALL x. abs (g x) <= f x ==>
1.436 g =o O(h)"
1.437 @@ -757,15 +760,15 @@
1.438 apply (rule order_trans)
1.439 apply assumption
1.440 apply (rule abs_ge_self)
1.441 -done
1.442 + done
1.443
1.444 lemma bigo_lesseq3: "f =o O(h) ==> ALL x. 0 <= g x ==> ALL x. g x <= f x ==>
1.445 - g =o O(h)"
1.446 + g =o O(h)"
1.447 apply (erule bigo_lesseq2)
1.448 apply (rule allI)
1.449 apply (subst abs_of_nonneg)
1.450 apply (erule spec)+
1.451 -done
1.452 + done
1.453
1.454 lemma bigo_lesseq4: "f =o O(h) ==>
1.455 ALL x. 0 <= g x ==> ALL x. g x <= abs (f x) ==>
1.456 @@ -774,7 +777,7 @@
1.457 apply (rule allI)
1.458 apply (subst abs_of_nonneg)
1.459 apply (erule spec)+
1.460 -done
1.461 + done
1.462
1.463 lemma bigo_lesso1: "ALL x. f x <= g x ==> f <o g =o O(h)"
1.464 apply (unfold lesso_def)
1.465 @@ -784,7 +787,7 @@
1.466 apply (unfold func_zero)
1.467 apply (rule ext)
1.468 apply (simp split: split_max)
1.469 -done
1.470 + done
1.471
1.472 lemma bigo_lesso2: "f =o g +o O(h) ==>
1.473 ALL x. 0 <= k x ==> ALL x. k x <= f x ==>
1.474 @@ -808,7 +811,7 @@
1.475 prefer 2
1.476 apply (rule abs_ge_zero)
1.477 apply (simp add: compare_rls)
1.478 -done
1.479 + done
1.480
1.481 lemma bigo_lesso3: "f =o g +o O(h) ==>
1.482 ALL x. 0 <= k x ==> ALL x. g x <= k x ==>
1.483 @@ -833,7 +836,7 @@
1.484 prefer 2
1.485 apply (rule abs_ge_zero)
1.486 apply (simp add: compare_rls)
1.487 -done
1.488 + done
1.489
1.490 lemma bigo_lesso4: "f <o g =o O(k::'a=>'b::ordered_field) ==>
1.491 g =o h +o O(k) ==> f <o h =o O(k)"
1.492 @@ -847,7 +850,7 @@
1.493 apply (rule allI)
1.494 apply (auto simp add: func_plus func_diff compare_rls
1.495 split: split_max abs_split)
1.496 -done
1.497 + done
1.498
1.499 lemma bigo_lesso5: "f <o g =o O(h) ==>
1.500 EX C. ALL x. f x <= g x + C * abs(h x)"
1.501 @@ -860,7 +863,7 @@
1.502 apply (clarsimp simp add: compare_rls add_ac)
1.503 apply (rule abs_of_nonneg)
1.504 apply (rule le_maxI2)
1.505 -done
1.506 + done
1.507
1.508 lemma lesso_add: "f <o g =o O(h) ==>
1.509 k <o l =o O(h) ==> (f + k) <o (g + l) =o O(h)"
1.510 @@ -870,6 +873,6 @@
1.511 apply assumption
1.512 apply (force split: split_max)
1.513 apply (auto split: split_max simp add: func_plus)
1.514 -done
1.515 + done
1.516
1.517 end