src/HOL/Library/BigO.thy
changeset 22665 cf152ff55d16
parent 21404 eb85850d3eb7
child 23373 ead82c82da9e
     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