src/HOL/Library/BigO.thy
 author Christian Sternagel Thu Dec 13 13:11:38 2012 +0100 (2012-12-13) changeset 50516 ed6b40d15d1c parent 47445 69e96e5500df child 54230 b1d955791529 permissions -rw-r--r--
renamed "emb" to "list_hembeq";
make "list_hembeq" reflexive independent of the base order;
renamed "sub" to "sublisteq";
dropped "transp_on" (state transitivity explicitly instead);
no need to hide "sub" after renaming;
replaced some ASCII symbols by proper Isabelle symbols;
NEWS
     1 (*  Title:      HOL/Library/BigO.thy

     2     Authors:    Jeremy Avigad and Kevin Donnelly

     3 *)

     4

     5 header {* Big O notation *}

     6

     7 theory BigO

     8 imports Complex_Main Function_Algebras Set_Algebras

     9 begin

    10

    11 text {*

    12 This library is designed to support asymptotic big O'' calculations,

    13 i.e.~reasoning with expressions of the form $f = O(g)$ and $f = g +   14 O(h)$.  An earlier version of this library is described in detail in

    15 \cite{Avigad-Donnelly}.

    16

    17 The main changes in this version are as follows:

    18 \begin{itemize}

    19 \item We have eliminated the @{text O} operator on sets. (Most uses of this seem

    20   to be inessential.)

    21 \item We no longer use @{text "+"} as output syntax for @{text "+o"}

    22 \item Lemmas involving @{text "sumr"} have been replaced by more general lemmas

    23   involving @{text "setsum"}.

    24 \item The library has been expanded, with e.g.~support for expressions of

    25   the form @{text "f < g + O(h)"}.

    26 \end{itemize}

    27

    28 Note also since the Big O library includes rules that demonstrate set

    29 inclusion, to use the automated reasoners effectively with the library

    30 one should redeclare the theorem @{text "subsetI"} as an intro rule,

    31 rather than as an @{text "intro!"} rule, for example, using

    32 \isa{\isakeyword{declare}}~@{text "subsetI [del, intro]"}.

    33 *}

    34

    35 subsection {* Definitions *}

    36

    37 definition

    38   bigo :: "('a => 'b::linordered_idom) => ('a => 'b) set"  ("(1O'(_'))") where

    39   "O(f::('a => 'b)) =

    40       {h. EX c. ALL x. abs (h x) <= c * abs (f x)}"

    41

    42 lemma bigo_pos_const: "(EX (c::'a::linordered_idom).

    43     ALL x. (abs (h x)) <= (c * (abs (f x))))

    44       = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"

    45   apply auto

    46   apply (case_tac "c = 0")

    47   apply simp

    48   apply (rule_tac x = "1" in exI)

    49   apply simp

    50   apply (rule_tac x = "abs c" in exI)

    51   apply auto

    52   apply (subgoal_tac "c * abs(f x) <= abs c * abs (f x)")

    53   apply (erule_tac x = x in allE)

    54   apply force

    55   apply (rule mult_right_mono)

    56   apply (rule abs_ge_self)

    57   apply (rule abs_ge_zero)

    58   done

    59

    60 lemma bigo_alt_def: "O(f) =

    61     {h. EX c. (0 < c & (ALL x. abs (h x) <= c * abs (f x)))}"

    62   by (auto simp add: bigo_def bigo_pos_const)

    63

    64 lemma bigo_elt_subset [intro]: "f : O(g) ==> O(f) <= O(g)"

    65   apply (auto simp add: bigo_alt_def)

    66   apply (rule_tac x = "ca * c" in exI)

    67   apply (rule conjI)

    68   apply (rule mult_pos_pos)

    69   apply (assumption)+

    70   apply (rule allI)

    71   apply (drule_tac x = "xa" in spec)+

    72   apply (subgoal_tac "ca * abs(f xa) <= ca * (c * abs(g xa))")

    73   apply (erule order_trans)

    74   apply (simp add: mult_ac)

    75   apply (rule mult_left_mono, assumption)

    76   apply (rule order_less_imp_le, assumption)

    77   done

    78

    79 lemma bigo_refl [intro]: "f : O(f)"

    80   apply(auto simp add: bigo_def)

    81   apply(rule_tac x = 1 in exI)

    82   apply simp

    83   done

    84

    85 lemma bigo_zero: "0 : O(g)"

    86   apply (auto simp add: bigo_def func_zero)

    87   apply (rule_tac x = 0 in exI)

    88   apply auto

    89   done

    90

    91 lemma bigo_zero2: "O(%x.0) = {%x.0}"

    92   by (auto simp add: bigo_def)

    93

    94 lemma bigo_plus_self_subset [intro]:

    95   "O(f) + O(f) <= O(f)"

    96   apply (auto simp add: bigo_alt_def set_plus_def)

    97   apply (rule_tac x = "c + ca" in exI)

    98   apply auto

    99   apply (simp add: ring_distribs func_plus)

   100   apply (rule order_trans)

   101   apply (rule abs_triangle_ineq)

   102   apply (rule add_mono)

   103   apply force

   104   apply force

   105 done

   106

   107 lemma bigo_plus_idemp [simp]: "O(f) + O(f) = O(f)"

   108   apply (rule equalityI)

   109   apply (rule bigo_plus_self_subset)

   110   apply (rule set_zero_plus2)

   111   apply (rule bigo_zero)

   112   done

   113

   114 lemma bigo_plus_subset [intro]: "O(f + g) <= O(f) + O(g)"

   115   apply (rule subsetI)

   116   apply (auto simp add: bigo_def bigo_pos_const func_plus set_plus_def)

   117   apply (subst bigo_pos_const [symmetric])+

   118   apply (rule_tac x =

   119     "%n. if abs (g n) <= (abs (f n)) then x n else 0" in exI)

   120   apply (rule conjI)

   121   apply (rule_tac x = "c + c" in exI)

   122   apply (clarsimp)

   123   apply (auto)

   124   apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (f xa)")

   125   apply (erule_tac x = xa in allE)

   126   apply (erule order_trans)

   127   apply (simp)

   128   apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))")

   129   apply (erule order_trans)

   130   apply (simp add: ring_distribs)

   131   apply (rule mult_left_mono)

   132   apply (simp add: abs_triangle_ineq)

   133   apply (simp add: order_less_le)

   134   apply (rule mult_nonneg_nonneg)

   135   apply auto

   136   apply (rule_tac x = "%n. if (abs (f n)) <  abs (g n) then x n else 0"

   137      in exI)

   138   apply (rule conjI)

   139   apply (rule_tac x = "c + c" in exI)

   140   apply auto

   141   apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (g xa)")

   142   apply (erule_tac x = xa in allE)

   143   apply (erule order_trans)

   144   apply (simp)

   145   apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))")

   146   apply (erule order_trans)

   147   apply (simp add: ring_distribs)

   148   apply (rule mult_left_mono)

   149   apply (rule abs_triangle_ineq)

   150   apply (simp add: order_less_le)

   151   apply (rule mult_nonneg_nonneg)

   152   apply (erule order_less_imp_le)

   153   apply simp

   154   done

   155

   156 lemma bigo_plus_subset2 [intro]: "A <= O(f) ==> B <= O(f) ==> A + B <= O(f)"

   157   apply (subgoal_tac "A + B <= O(f) + O(f)")

   158   apply (erule order_trans)

   159   apply simp

   160   apply (auto del: subsetI simp del: bigo_plus_idemp)

   161   done

   162

   163 lemma bigo_plus_eq: "ALL x. 0 <= f x ==> ALL x. 0 <= g x ==>

   164     O(f + g) = O(f) + O(g)"

   165   apply (rule equalityI)

   166   apply (rule bigo_plus_subset)

   167   apply (simp add: bigo_alt_def set_plus_def func_plus)

   168   apply clarify

   169   apply (rule_tac x = "max c ca" in exI)

   170   apply (rule conjI)

   171   apply (subgoal_tac "c <= max c ca")

   172   apply (erule order_less_le_trans)

   173   apply assumption

   174   apply (rule le_maxI1)

   175   apply clarify

   176   apply (drule_tac x = "xa" in spec)+

   177   apply (subgoal_tac "0 <= f xa + g xa")

   178   apply (simp add: ring_distribs)

   179   apply (subgoal_tac "abs(a xa + b xa) <= abs(a xa) + abs(b xa)")

   180   apply (subgoal_tac "abs(a xa) + abs(b xa) <=

   181       max c ca * f xa + max c ca * g xa")

   182   apply (force)

   183   apply (rule add_mono)

   184   apply (subgoal_tac "c * f xa <= max c ca * f xa")

   185   apply (force)

   186   apply (rule mult_right_mono)

   187   apply (rule le_maxI1)

   188   apply assumption

   189   apply (subgoal_tac "ca * g xa <= max c ca * g xa")

   190   apply (force)

   191   apply (rule mult_right_mono)

   192   apply (rule le_maxI2)

   193   apply assumption

   194   apply (rule abs_triangle_ineq)

   195   apply (rule add_nonneg_nonneg)

   196   apply assumption+

   197   done

   198

   199 lemma bigo_bounded_alt: "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==>

   200     f : O(g)"

   201   apply (auto simp add: bigo_def)

   202   apply (rule_tac x = "abs c" in exI)

   203   apply auto

   204   apply (drule_tac x = x in spec)+

   205   apply (simp add: abs_mult [symmetric])

   206   done

   207

   208 lemma bigo_bounded: "ALL x. 0 <= f x ==> ALL x. f x <= g x ==>

   209     f : O(g)"

   210   apply (erule bigo_bounded_alt [of f 1 g])

   211   apply simp

   212   done

   213

   214 lemma bigo_bounded2: "ALL x. lb x <= f x ==> ALL x. f x <= lb x + g x ==>

   215     f : lb +o O(g)"

   216   apply (rule set_minus_imp_plus)

   217   apply (rule bigo_bounded)

   218   apply (auto simp add: diff_minus fun_Compl_def func_plus)

   219   apply (drule_tac x = x in spec)+

   220   apply force

   221   apply (drule_tac x = x in spec)+

   222   apply force

   223   done

   224

   225 lemma bigo_abs: "(%x. abs(f x)) =o O(f)"

   226   apply (unfold bigo_def)

   227   apply auto

   228   apply (rule_tac x = 1 in exI)

   229   apply auto

   230   done

   231

   232 lemma bigo_abs2: "f =o O(%x. abs(f x))"

   233   apply (unfold bigo_def)

   234   apply auto

   235   apply (rule_tac x = 1 in exI)

   236   apply auto

   237   done

   238

   239 lemma bigo_abs3: "O(f) = O(%x. abs(f x))"

   240   apply (rule equalityI)

   241   apply (rule bigo_elt_subset)

   242   apply (rule bigo_abs2)

   243   apply (rule bigo_elt_subset)

   244   apply (rule bigo_abs)

   245   done

   246

   247 lemma bigo_abs4: "f =o g +o O(h) ==>

   248     (%x. abs (f x)) =o (%x. abs (g x)) +o O(h)"

   249   apply (drule set_plus_imp_minus)

   250   apply (rule set_minus_imp_plus)

   251   apply (subst fun_diff_def)

   252 proof -

   253   assume a: "f - g : O(h)"

   254   have "(%x. abs (f x) - abs (g x)) =o O(%x. abs(abs (f x) - abs (g x)))"

   255     by (rule bigo_abs2)

   256   also have "... <= O(%x. abs (f x - g x))"

   257     apply (rule bigo_elt_subset)

   258     apply (rule bigo_bounded)

   259     apply force

   260     apply (rule allI)

   261     apply (rule abs_triangle_ineq3)

   262     done

   263   also have "... <= O(f - g)"

   264     apply (rule bigo_elt_subset)

   265     apply (subst fun_diff_def)

   266     apply (rule bigo_abs)

   267     done

   268   also from a have "... <= O(h)"

   269     by (rule bigo_elt_subset)

   270   finally show "(%x. abs (f x) - abs (g x)) : O(h)".

   271 qed

   272

   273 lemma bigo_abs5: "f =o O(g) ==> (%x. abs(f x)) =o O(g)"

   274   by (unfold bigo_def, auto)

   275

   276 lemma bigo_elt_subset2 [intro]: "f : g +o O(h) ==> O(f) <= O(g) + O(h)"

   277 proof -

   278   assume "f : g +o O(h)"

   279   also have "... <= O(g) + O(h)"

   280     by (auto del: subsetI)

   281   also have "... = O(%x. abs(g x)) + O(%x. abs(h x))"

   282     apply (subst bigo_abs3 [symmetric])+

   283     apply (rule refl)

   284     done

   285   also have "... = O((%x. abs(g x)) + (%x. abs(h x)))"

   286     by (rule bigo_plus_eq [symmetric], auto)

   287   finally have "f : ...".

   288   then have "O(f) <= ..."

   289     by (elim bigo_elt_subset)

   290   also have "... = O(%x. abs(g x)) + O(%x. abs(h x))"

   291     by (rule bigo_plus_eq, auto)

   292   finally show ?thesis

   293     by (simp add: bigo_abs3 [symmetric])

   294 qed

   295

   296 lemma bigo_mult [intro]: "O(f)*O(g) <= O(f * g)"

   297   apply (rule subsetI)

   298   apply (subst bigo_def)

   299   apply (auto simp add: bigo_alt_def set_times_def func_times)

   300   apply (rule_tac x = "c * ca" in exI)

   301   apply(rule allI)

   302   apply(erule_tac x = x in allE)+

   303   apply(subgoal_tac "c * ca * abs(f x * g x) =

   304       (c * abs(f x)) * (ca * abs(g x))")

   305   apply(erule ssubst)

   306   apply (subst abs_mult)

   307   apply (rule mult_mono)

   308   apply assumption+

   309   apply (rule mult_nonneg_nonneg)

   310   apply auto

   311   apply (simp add: mult_ac abs_mult)

   312   done

   313

   314 lemma bigo_mult2 [intro]: "f *o O(g) <= O(f * g)"

   315   apply (auto simp add: bigo_def elt_set_times_def func_times abs_mult)

   316   apply (rule_tac x = c in exI)

   317   apply auto

   318   apply (drule_tac x = x in spec)

   319   apply (subgoal_tac "abs(f x) * abs(b x) <= abs(f x) * (c * abs(g x))")

   320   apply (force simp add: mult_ac)

   321   apply (rule mult_left_mono, assumption)

   322   apply (rule abs_ge_zero)

   323   done

   324

   325 lemma bigo_mult3: "f : O(h) ==> g : O(j) ==> f * g : O(h * j)"

   326   apply (rule subsetD)

   327   apply (rule bigo_mult)

   328   apply (erule set_times_intro, assumption)

   329   done

   330

   331 lemma bigo_mult4 [intro]:"f : k +o O(h) ==> g * f : (g * k) +o O(g * h)"

   332   apply (drule set_plus_imp_minus)

   333   apply (rule set_minus_imp_plus)

   334   apply (drule bigo_mult3 [where g = g and j = g])

   335   apply (auto simp add: algebra_simps)

   336   done

   337

   338 lemma bigo_mult5:

   339   assumes "ALL x. f x ~= 0"

   340   shows "O(f * g) <= (f::'a => ('b::linordered_field)) *o O(g)"

   341 proof

   342   fix h

   343   assume "h : O(f * g)"

   344   then have "(%x. 1 / (f x)) * h : (%x. 1 / f x) *o O(f * g)"

   345     by auto

   346   also have "... <= O((%x. 1 / f x) * (f * g))"

   347     by (rule bigo_mult2)

   348   also have "(%x. 1 / f x) * (f * g) = g"

   349     apply (simp add: func_times)

   350     apply (rule ext)

   351     apply (simp add: assms nonzero_divide_eq_eq mult_ac)

   352     done

   353   finally have "(%x. (1::'b) / f x) * h : O(g)" .

   354   then have "f * ((%x. (1::'b) / f x) * h) : f *o O(g)"

   355     by auto

   356   also have "f * ((%x. (1::'b) / f x) * h) = h"

   357     apply (simp add: func_times)

   358     apply (rule ext)

   359     apply (simp add: assms nonzero_divide_eq_eq mult_ac)

   360     done

   361   finally show "h : f *o O(g)" .

   362 qed

   363

   364 lemma bigo_mult6: "ALL x. f x ~= 0 ==>

   365     O(f * g) = (f::'a => ('b::linordered_field)) *o O(g)"

   366   apply (rule equalityI)

   367   apply (erule bigo_mult5)

   368   apply (rule bigo_mult2)

   369   done

   370

   371 lemma bigo_mult7: "ALL x. f x ~= 0 ==>

   372     O(f * g) <= O(f::'a => ('b::linordered_field)) * O(g)"

   373   apply (subst bigo_mult6)

   374   apply assumption

   375   apply (rule set_times_mono3)

   376   apply (rule bigo_refl)

   377   done

   378

   379 lemma bigo_mult8: "ALL x. f x ~= 0 ==>

   380     O(f * g) = O(f::'a => ('b::linordered_field)) * O(g)"

   381   apply (rule equalityI)

   382   apply (erule bigo_mult7)

   383   apply (rule bigo_mult)

   384   done

   385

   386 lemma bigo_minus [intro]: "f : O(g) ==> - f : O(g)"

   387   by (auto simp add: bigo_def fun_Compl_def)

   388

   389 lemma bigo_minus2: "f : g +o O(h) ==> -f : -g +o O(h)"

   390   apply (rule set_minus_imp_plus)

   391   apply (drule set_plus_imp_minus)

   392   apply (drule bigo_minus)

   393   apply (simp add: diff_minus)

   394   done

   395

   396 lemma bigo_minus3: "O(-f) = O(f)"

   397   by (auto simp add: bigo_def fun_Compl_def)

   398

   399 lemma bigo_plus_absorb_lemma1: "f : O(g) ==> f +o O(g) <= O(g)"

   400 proof -

   401   assume a: "f : O(g)"

   402   show "f +o O(g) <= O(g)"

   403   proof -

   404     have "f : O(f)" by auto

   405     then have "f +o O(g) <= O(f) + O(g)"

   406       by (auto del: subsetI)

   407     also have "... <= O(g) + O(g)"

   408     proof -

   409       from a have "O(f) <= O(g)" by (auto del: subsetI)

   410       thus ?thesis by (auto del: subsetI)

   411     qed

   412     also have "... <= O(g)" by simp

   413     finally show ?thesis .

   414   qed

   415 qed

   416

   417 lemma bigo_plus_absorb_lemma2: "f : O(g) ==> O(g) <= f +o O(g)"

   418 proof -

   419   assume a: "f : O(g)"

   420   show "O(g) <= f +o O(g)"

   421   proof -

   422     from a have "-f : O(g)" by auto

   423     then have "-f +o O(g) <= O(g)" by (elim bigo_plus_absorb_lemma1)

   424     then have "f +o (-f +o O(g)) <= f +o O(g)" by auto

   425     also have "f +o (-f +o O(g)) = O(g)"

   426       by (simp add: set_plus_rearranges)

   427     finally show ?thesis .

   428   qed

   429 qed

   430

   431 lemma bigo_plus_absorb [simp]: "f : O(g) ==> f +o O(g) = O(g)"

   432   apply (rule equalityI)

   433   apply (erule bigo_plus_absorb_lemma1)

   434   apply (erule bigo_plus_absorb_lemma2)

   435   done

   436

   437 lemma bigo_plus_absorb2 [intro]: "f : O(g) ==> A <= O(g) ==> f +o A <= O(g)"

   438   apply (subgoal_tac "f +o A <= f +o O(g)")

   439   apply force+

   440   done

   441

   442 lemma bigo_add_commute_imp: "f : g +o O(h) ==> g : f +o O(h)"

   443   apply (subst set_minus_plus [symmetric])

   444   apply (subgoal_tac "g - f = - (f - g)")

   445   apply (erule ssubst)

   446   apply (rule bigo_minus)

   447   apply (subst set_minus_plus)

   448   apply assumption

   449   apply  (simp add: diff_minus add_ac)

   450   done

   451

   452 lemma bigo_add_commute: "(f : g +o O(h)) = (g : f +o O(h))"

   453   apply (rule iffI)

   454   apply (erule bigo_add_commute_imp)+

   455   done

   456

   457 lemma bigo_const1: "(%x. c) : O(%x. 1)"

   458   by (auto simp add: bigo_def mult_ac)

   459

   460 lemma bigo_const2 [intro]: "O(%x. c) <= O(%x. 1)"

   461   apply (rule bigo_elt_subset)

   462   apply (rule bigo_const1)

   463   done

   464

   465 lemma bigo_const3: "(c::'a::linordered_field) ~= 0 ==> (%x. 1) : O(%x. c)"

   466   apply (simp add: bigo_def)

   467   apply (rule_tac x = "abs(inverse c)" in exI)

   468   apply (simp add: abs_mult [symmetric])

   469   done

   470

   471 lemma bigo_const4: "(c::'a::linordered_field) ~= 0 ==> O(%x. 1) <= O(%x. c)"

   472   by (rule bigo_elt_subset, rule bigo_const3, assumption)

   473

   474 lemma bigo_const [simp]: "(c::'a::linordered_field) ~= 0 ==>

   475     O(%x. c) = O(%x. 1)"

   476   by (rule equalityI, rule bigo_const2, rule bigo_const4, assumption)

   477

   478 lemma bigo_const_mult1: "(%x. c * f x) : O(f)"

   479   apply (simp add: bigo_def)

   480   apply (rule_tac x = "abs(c)" in exI)

   481   apply (auto simp add: abs_mult [symmetric])

   482   done

   483

   484 lemma bigo_const_mult2: "O(%x. c * f x) <= O(f)"

   485   by (rule bigo_elt_subset, rule bigo_const_mult1)

   486

   487 lemma bigo_const_mult3: "(c::'a::linordered_field) ~= 0 ==> f : O(%x. c * f x)"

   488   apply (simp add: bigo_def)

   489   apply (rule_tac x = "abs(inverse c)" in exI)

   490   apply (simp add: abs_mult [symmetric] mult_assoc [symmetric])

   491   done

   492

   493 lemma bigo_const_mult4: "(c::'a::linordered_field) ~= 0 ==>

   494     O(f) <= O(%x. c * f x)"

   495   by (rule bigo_elt_subset, rule bigo_const_mult3, assumption)

   496

   497 lemma bigo_const_mult [simp]: "(c::'a::linordered_field) ~= 0 ==>

   498     O(%x. c * f x) = O(f)"

   499   by (rule equalityI, rule bigo_const_mult2, erule bigo_const_mult4)

   500

   501 lemma bigo_const_mult5 [simp]: "(c::'a::linordered_field) ~= 0 ==>

   502     (%x. c) *o O(f) = O(f)"

   503   apply (auto del: subsetI)

   504   apply (rule order_trans)

   505   apply (rule bigo_mult2)

   506   apply (simp add: func_times)

   507   apply (auto intro!: simp add: bigo_def elt_set_times_def func_times)

   508   apply (rule_tac x = "%y. inverse c * x y" in exI)

   509   apply (simp add: mult_assoc [symmetric] abs_mult)

   510   apply (rule_tac x = "abs (inverse c) * ca" in exI)

   511   apply (rule allI)

   512   apply (subst mult_assoc)

   513   apply (rule mult_left_mono)

   514   apply (erule spec)

   515   apply force

   516   done

   517

   518 lemma bigo_const_mult6 [intro]: "(%x. c) *o O(f) <= O(f)"

   519   apply (auto intro!: simp add: bigo_def elt_set_times_def func_times)

   520   apply (rule_tac x = "ca * (abs c)" in exI)

   521   apply (rule allI)

   522   apply (subgoal_tac "ca * abs(c) * abs(f x) = abs(c) * (ca * abs(f x))")

   523   apply (erule ssubst)

   524   apply (subst abs_mult)

   525   apply (rule mult_left_mono)

   526   apply (erule spec)

   527   apply simp

   528   apply(simp add: mult_ac)

   529   done

   530

   531 lemma bigo_const_mult7 [intro]: "f =o O(g) ==> (%x. c * f x) =o O(g)"

   532 proof -

   533   assume "f =o O(g)"

   534   then have "(%x. c) * f =o (%x. c) *o O(g)"

   535     by auto

   536   also have "(%x. c) * f = (%x. c * f x)"

   537     by (simp add: func_times)

   538   also have "(%x. c) *o O(g) <= O(g)"

   539     by (auto del: subsetI)

   540   finally show ?thesis .

   541 qed

   542

   543 lemma bigo_compose1: "f =o O(g) ==> (%x. f(k x)) =o O(%x. g(k x))"

   544 by (unfold bigo_def, auto)

   545

   546 lemma bigo_compose2: "f =o g +o O(h) ==> (%x. f(k x)) =o (%x. g(k x)) +o

   547     O(%x. h(k x))"

   548   apply (simp only: set_minus_plus [symmetric] diff_minus fun_Compl_def

   549       func_plus)

   550   apply (erule bigo_compose1)

   551 done

   552

   553

   554 subsection {* Setsum *}

   555

   556 lemma bigo_setsum_main: "ALL x. ALL y : A x. 0 <= h x y ==>

   557     EX c. ALL x. ALL y : A x. abs(f x y) <= c * (h x y) ==>

   558       (%x. SUM y : A x. f x y) =o O(%x. SUM y : A x. h x y)"

   559   apply (auto simp add: bigo_def)

   560   apply (rule_tac x = "abs c" in exI)

   561   apply (subst abs_of_nonneg) back back

   562   apply (rule setsum_nonneg)

   563   apply force

   564   apply (subst setsum_right_distrib)

   565   apply (rule allI)

   566   apply (rule order_trans)

   567   apply (rule setsum_abs)

   568   apply (rule setsum_mono)

   569   apply (rule order_trans)

   570   apply (drule spec)+

   571   apply (drule bspec)+

   572   apply assumption+

   573   apply (drule bspec)

   574   apply assumption+

   575   apply (rule mult_right_mono)

   576   apply (rule abs_ge_self)

   577   apply force

   578   done

   579

   580 lemma bigo_setsum1: "ALL x y. 0 <= h x y ==>

   581     EX c. ALL x y. abs(f x y) <= c * (h x y) ==>

   582       (%x. SUM y : A x. f x y) =o O(%x. SUM y : A x. h x y)"

   583   apply (rule bigo_setsum_main)

   584   apply force

   585   apply clarsimp

   586   apply (rule_tac x = c in exI)

   587   apply force

   588   done

   589

   590 lemma bigo_setsum2: "ALL y. 0 <= h y ==>

   591     EX c. ALL y. abs(f y) <= c * (h y) ==>

   592       (%x. SUM y : A x. f y) =o O(%x. SUM y : A x. h y)"

   593   by (rule bigo_setsum1, auto)

   594

   595 lemma bigo_setsum3: "f =o O(h) ==>

   596     (%x. SUM y : A x. (l x y) * f(k x y)) =o

   597       O(%x. SUM y : A x. abs(l x y * h(k x y)))"

   598   apply (rule bigo_setsum1)

   599   apply (rule allI)+

   600   apply (rule abs_ge_zero)

   601   apply (unfold bigo_def)

   602   apply auto

   603   apply (rule_tac x = c in exI)

   604   apply (rule allI)+

   605   apply (subst abs_mult)+

   606   apply (subst mult_left_commute)

   607   apply (rule mult_left_mono)

   608   apply (erule spec)

   609   apply (rule abs_ge_zero)

   610   done

   611

   612 lemma bigo_setsum4: "f =o g +o O(h) ==>

   613     (%x. SUM y : A x. l x y * f(k x y)) =o

   614       (%x. SUM y : A x. l x y * g(k x y)) +o

   615         O(%x. SUM y : A x. abs(l x y * h(k x y)))"

   616   apply (rule set_minus_imp_plus)

   617   apply (subst fun_diff_def)

   618   apply (subst setsum_subtractf [symmetric])

   619   apply (subst right_diff_distrib [symmetric])

   620   apply (rule bigo_setsum3)

   621   apply (subst fun_diff_def [symmetric])

   622   apply (erule set_plus_imp_minus)

   623   done

   624

   625 lemma bigo_setsum5: "f =o O(h) ==> ALL x y. 0 <= l x y ==>

   626     ALL x. 0 <= h x ==>

   627       (%x. SUM y : A x. (l x y) * f(k x y)) =o

   628         O(%x. SUM y : A x. (l x y) * h(k x y))"

   629   apply (subgoal_tac "(%x. SUM y : A x. (l x y) * h(k x y)) =

   630       (%x. SUM y : A x. abs((l x y) * h(k x y)))")

   631   apply (erule ssubst)

   632   apply (erule bigo_setsum3)

   633   apply (rule ext)

   634   apply (rule setsum_cong2)

   635   apply (subst abs_of_nonneg)

   636   apply (rule mult_nonneg_nonneg)

   637   apply auto

   638   done

   639

   640 lemma bigo_setsum6: "f =o g +o O(h) ==> ALL x y. 0 <= l x y ==>

   641     ALL x. 0 <= h x ==>

   642       (%x. SUM y : A x. (l x y) * f(k x y)) =o

   643         (%x. SUM y : A x. (l x y) * g(k x y)) +o

   644           O(%x. SUM y : A x. (l x y) * h(k x y))"

   645   apply (rule set_minus_imp_plus)

   646   apply (subst fun_diff_def)

   647   apply (subst setsum_subtractf [symmetric])

   648   apply (subst right_diff_distrib [symmetric])

   649   apply (rule bigo_setsum5)

   650   apply (subst fun_diff_def [symmetric])

   651   apply (drule set_plus_imp_minus)

   652   apply auto

   653   done

   654

   655

   656 subsection {* Misc useful stuff *}

   657

   658 lemma bigo_useful_intro: "A <= O(f) ==> B <= O(f) ==>

   659   A + B <= O(f)"

   660   apply (subst bigo_plus_idemp [symmetric])

   661   apply (rule set_plus_mono2)

   662   apply assumption+

   663   done

   664

   665 lemma bigo_useful_add: "f =o O(h) ==> g =o O(h) ==> f + g =o O(h)"

   666   apply (subst bigo_plus_idemp [symmetric])

   667   apply (rule set_plus_intro)

   668   apply assumption+

   669   done

   670

   671 lemma bigo_useful_const_mult: "(c::'a::linordered_field) ~= 0 ==>

   672     (%x. c) * f =o O(h) ==> f =o O(h)"

   673   apply (rule subsetD)

   674   apply (subgoal_tac "(%x. 1 / c) *o O(h) <= O(h)")

   675   apply assumption

   676   apply (rule bigo_const_mult6)

   677   apply (subgoal_tac "f = (%x. 1 / c) * ((%x. c) * f)")

   678   apply (erule ssubst)

   679   apply (erule set_times_intro2)

   680   apply (simp add: func_times)

   681   done

   682

   683 lemma bigo_fix: "(%x. f ((x::nat) + 1)) =o O(%x. h(x + 1)) ==> f 0 = 0 ==>

   684     f =o O(h)"

   685   apply (simp add: bigo_alt_def)

   686   apply auto

   687   apply (rule_tac x = c in exI)

   688   apply auto

   689   apply (case_tac "x = 0")

   690   apply simp

   691   apply (rule mult_nonneg_nonneg)

   692   apply force

   693   apply force

   694   apply (subgoal_tac "x = Suc (x - 1)")

   695   apply (erule ssubst) back

   696   apply (erule spec)

   697   apply simp

   698   done

   699

   700 lemma bigo_fix2:

   701     "(%x. f ((x::nat) + 1)) =o (%x. g(x + 1)) +o O(%x. h(x + 1)) ==>

   702        f 0 = g 0 ==> f =o g +o O(h)"

   703   apply (rule set_minus_imp_plus)

   704   apply (rule bigo_fix)

   705   apply (subst fun_diff_def)

   706   apply (subst fun_diff_def [symmetric])

   707   apply (rule set_plus_imp_minus)

   708   apply simp

   709   apply (simp add: fun_diff_def)

   710   done

   711

   712

   713 subsection {* Less than or equal to *}

   714

   715 definition

   716   lesso :: "('a => 'b::linordered_idom) => ('a => 'b) => ('a => 'b)"

   717     (infixl "<o" 70) where

   718   "f <o g = (%x. max (f x - g x) 0)"

   719

   720 lemma bigo_lesseq1: "f =o O(h) ==> ALL x. abs (g x) <= abs (f x) ==>

   721     g =o O(h)"

   722   apply (unfold bigo_def)

   723   apply clarsimp

   724   apply (rule_tac x = c in exI)

   725   apply (rule allI)

   726   apply (rule order_trans)

   727   apply (erule spec)+

   728   done

   729

   730 lemma bigo_lesseq2: "f =o O(h) ==> ALL x. abs (g x) <= f x ==>

   731       g =o O(h)"

   732   apply (erule bigo_lesseq1)

   733   apply (rule allI)

   734   apply (drule_tac x = x in spec)

   735   apply (rule order_trans)

   736   apply assumption

   737   apply (rule abs_ge_self)

   738   done

   739

   740 lemma bigo_lesseq3: "f =o O(h) ==> ALL x. 0 <= g x ==> ALL x. g x <= f x ==>

   741     g =o O(h)"

   742   apply (erule bigo_lesseq2)

   743   apply (rule allI)

   744   apply (subst abs_of_nonneg)

   745   apply (erule spec)+

   746   done

   747

   748 lemma bigo_lesseq4: "f =o O(h) ==>

   749     ALL x. 0 <= g x ==> ALL x. g x <= abs (f x) ==>

   750       g =o O(h)"

   751   apply (erule bigo_lesseq1)

   752   apply (rule allI)

   753   apply (subst abs_of_nonneg)

   754   apply (erule spec)+

   755   done

   756

   757 lemma bigo_lesso1: "ALL x. f x <= g x ==> f <o g =o O(h)"

   758   apply (unfold lesso_def)

   759   apply (subgoal_tac "(%x. max (f x - g x) 0) = 0")

   760   apply (erule ssubst)

   761   apply (rule bigo_zero)

   762   apply (unfold func_zero)

   763   apply (rule ext)

   764   apply (simp split: split_max)

   765   done

   766

   767 lemma bigo_lesso2: "f =o g +o O(h) ==>

   768     ALL x. 0 <= k x ==> ALL x. k x <= f x ==>

   769       k <o g =o O(h)"

   770   apply (unfold lesso_def)

   771   apply (rule bigo_lesseq4)

   772   apply (erule set_plus_imp_minus)

   773   apply (rule allI)

   774   apply (rule le_maxI2)

   775   apply (rule allI)

   776   apply (subst fun_diff_def)

   777   apply (case_tac "0 <= k x - g x")

   778   apply simp

   779   apply (subst abs_of_nonneg)

   780   apply (drule_tac x = x in spec) back

   781   apply (simp add: algebra_simps)

   782   apply (subst diff_minus)+

   783   apply (rule add_right_mono)

   784   apply (erule spec)

   785   apply (rule order_trans)

   786   prefer 2

   787   apply (rule abs_ge_zero)

   788   apply (simp add: algebra_simps)

   789   done

   790

   791 lemma bigo_lesso3: "f =o g +o O(h) ==>

   792     ALL x. 0 <= k x ==> ALL x. g x <= k x ==>

   793       f <o k =o O(h)"

   794   apply (unfold lesso_def)

   795   apply (rule bigo_lesseq4)

   796   apply (erule set_plus_imp_minus)

   797   apply (rule allI)

   798   apply (rule le_maxI2)

   799   apply (rule allI)

   800   apply (subst fun_diff_def)

   801   apply (case_tac "0 <= f x - k x")

   802   apply simp

   803   apply (subst abs_of_nonneg)

   804   apply (drule_tac x = x in spec) back

   805   apply (simp add: algebra_simps)

   806   apply (subst diff_minus)+

   807   apply (rule add_left_mono)

   808   apply (rule le_imp_neg_le)

   809   apply (erule spec)

   810   apply (rule order_trans)

   811   prefer 2

   812   apply (rule abs_ge_zero)

   813   apply (simp add: algebra_simps)

   814   done

   815

   816 lemma bigo_lesso4: "f <o g =o O(k::'a=>'b::linordered_field) ==>

   817     g =o h +o O(k) ==> f <o h =o O(k)"

   818   apply (unfold lesso_def)

   819   apply (drule set_plus_imp_minus)

   820   apply (drule bigo_abs5) back

   821   apply (simp add: fun_diff_def)

   822   apply (drule bigo_useful_add)

   823   apply assumption

   824   apply (erule bigo_lesseq2) back

   825   apply (rule allI)

   826   apply (auto simp add: func_plus fun_diff_def algebra_simps

   827     split: split_max abs_split)

   828   done

   829

   830 lemma bigo_lesso5: "f <o g =o O(h) ==>

   831     EX C. ALL x. f x <= g x + C * abs(h x)"

   832   apply (simp only: lesso_def bigo_alt_def)

   833   apply clarsimp

   834   apply (rule_tac x = c in exI)

   835   apply (rule allI)

   836   apply (drule_tac x = x in spec)

   837   apply (subgoal_tac "abs(max (f x - g x) 0) = max (f x - g x) 0")

   838   apply (clarsimp simp add: algebra_simps)

   839   apply (rule abs_of_nonneg)

   840   apply (rule le_maxI2)

   841   done

   842

   843 lemma lesso_add: "f <o g =o O(h) ==>

   844       k <o l =o O(h) ==> (f + k) <o (g + l) =o O(h)"

   845   apply (unfold lesso_def)

   846   apply (rule bigo_lesseq3)

   847   apply (erule bigo_useful_add)

   848   apply assumption

   849   apply (force split: split_max)

   850   apply (auto split: split_max simp add: func_plus)

   851   done

   852

   853 lemma bigo_LIMSEQ1: "f =o O(g) ==> g ----> 0 ==> f ----> (0::real)"

   854   apply (simp add: LIMSEQ_iff bigo_alt_def)

   855   apply clarify

   856   apply (drule_tac x = "r / c" in spec)

   857   apply (drule mp)

   858   apply (erule divide_pos_pos)

   859   apply assumption

   860   apply clarify

   861   apply (rule_tac x = no in exI)

   862   apply (rule allI)

   863   apply (drule_tac x = n in spec)+

   864   apply (rule impI)

   865   apply (drule mp)

   866   apply assumption

   867   apply (rule order_le_less_trans)

   868   apply assumption

   869   apply (rule order_less_le_trans)

   870   apply (subgoal_tac "c * abs(g n) < c * (r / c)")

   871   apply assumption

   872   apply (erule mult_strict_left_mono)

   873   apply assumption

   874   apply simp

   875 done

   876

   877 lemma bigo_LIMSEQ2: "f =o g +o O(h) ==> h ----> 0 ==> f ----> a

   878     ==> g ----> (a::real)"

   879   apply (drule set_plus_imp_minus)

   880   apply (drule bigo_LIMSEQ1)

   881   apply assumption

   882   apply (simp only: fun_diff_def)

   883   apply (erule LIMSEQ_diff_approach_zero2)

   884   apply assumption

   885 done

   886

   887 end
`