src/HOL/Library/BigO.thy
 author hoelzl Tue Jul 19 14:37:49 2011 +0200 (2011-07-19) changeset 43922 c6f35921056e parent 42285 8d91a85b6d91 child 45270 d5b5c9259afd permissions -rw-r--r--
     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) \<oplus> 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) \<oplus> 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) \<oplus> 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 assumption

   133   apply (simp add: order_less_le)

   134   apply (rule mult_left_mono)

   135   apply (simp add: abs_triangle_ineq)

   136   apply (simp add: order_less_le)

   137   apply (rule mult_nonneg_nonneg)

   138   apply (rule add_nonneg_nonneg)

   139   apply auto

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

   141      in exI)

   142   apply (rule conjI)

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

   144   apply auto

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

   146   apply (erule_tac x = xa in allE)

   147   apply (erule order_trans)

   148   apply (simp)

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

   150   apply (erule order_trans)

   151   apply (simp add: ring_distribs)

   152   apply (rule mult_left_mono)

   153   apply (simp add: order_less_le)

   154   apply (simp add: order_less_le)

   155   apply (rule mult_left_mono)

   156   apply (rule abs_triangle_ineq)

   157   apply (simp add: order_less_le)

   158   apply (rule mult_nonneg_nonneg)

   159   apply (rule add_nonneg_nonneg)

   160   apply (erule order_less_imp_le)+

   161   apply simp

   162   apply (rule ext)

   163   apply (auto simp add: if_splits linorder_not_le)

   164   done

   165

   166 lemma bigo_plus_subset2 [intro]: "A <= O(f) ==> B <= O(f) ==> A \<oplus> B <= O(f)"

   167   apply (subgoal_tac "A \<oplus> B <= O(f) \<oplus> O(f)")

   168   apply (erule order_trans)

   169   apply simp

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

   171   done

   172

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

   174     O(f + g) = O(f) \<oplus> O(g)"

   175   apply (rule equalityI)

   176   apply (rule bigo_plus_subset)

   177   apply (simp add: bigo_alt_def set_plus_def func_plus)

   178   apply clarify

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

   180   apply (rule conjI)

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

   182   apply (erule order_less_le_trans)

   183   apply assumption

   184   apply (rule le_maxI1)

   185   apply clarify

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

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

   188   apply (simp add: ring_distribs)

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

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

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

   192   apply (force)

   193   apply (rule add_mono)

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

   195   apply (force)

   196   apply (rule mult_right_mono)

   197   apply (rule le_maxI1)

   198   apply assumption

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

   200   apply (force)

   201   apply (rule mult_right_mono)

   202   apply (rule le_maxI2)

   203   apply assumption

   204   apply (rule abs_triangle_ineq)

   205   apply (rule add_nonneg_nonneg)

   206   apply assumption+

   207   done

   208

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

   210     f : O(g)"

   211   apply (auto simp add: bigo_def)

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

   213   apply auto

   214   apply (drule_tac x = x in spec)+

   215   apply (simp add: abs_mult [symmetric])

   216   done

   217

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

   219     f : O(g)"

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

   221   apply simp

   222   done

   223

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

   225     f : lb +o O(g)"

   226   apply (rule set_minus_imp_plus)

   227   apply (rule bigo_bounded)

   228   apply (auto simp add: diff_minus fun_Compl_def func_plus)

   229   apply (drule_tac x = x in spec)+

   230   apply force

   231   apply (drule_tac x = x in spec)+

   232   apply force

   233   done

   234

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

   236   apply (unfold bigo_def)

   237   apply auto

   238   apply (rule_tac x = 1 in exI)

   239   apply auto

   240   done

   241

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

   243   apply (unfold bigo_def)

   244   apply auto

   245   apply (rule_tac x = 1 in exI)

   246   apply auto

   247   done

   248

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

   250   apply (rule equalityI)

   251   apply (rule bigo_elt_subset)

   252   apply (rule bigo_abs2)

   253   apply (rule bigo_elt_subset)

   254   apply (rule bigo_abs)

   255   done

   256

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

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

   259   apply (drule set_plus_imp_minus)

   260   apply (rule set_minus_imp_plus)

   261   apply (subst fun_diff_def)

   262 proof -

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

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

   265     by (rule bigo_abs2)

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

   267     apply (rule bigo_elt_subset)

   268     apply (rule bigo_bounded)

   269     apply force

   270     apply (rule allI)

   271     apply (rule abs_triangle_ineq3)

   272     done

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

   274     apply (rule bigo_elt_subset)

   275     apply (subst fun_diff_def)

   276     apply (rule bigo_abs)

   277     done

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

   279     by (rule bigo_elt_subset)

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

   281 qed

   282

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

   284   by (unfold bigo_def, auto)

   285

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

   287 proof -

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

   289   also have "... <= O(g) \<oplus> O(h)"

   290     by (auto del: subsetI)

   291   also have "... = O(%x. abs(g x)) \<oplus> O(%x. abs(h x))"

   292     apply (subst bigo_abs3 [symmetric])+

   293     apply (rule refl)

   294     done

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

   296     by (rule bigo_plus_eq [symmetric], auto)

   297   finally have "f : ...".

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

   299     by (elim bigo_elt_subset)

   300   also have "... = O(%x. abs(g x)) \<oplus> O(%x. abs(h x))"

   301     by (rule bigo_plus_eq, auto)

   302   finally show ?thesis

   303     by (simp add: bigo_abs3 [symmetric])

   304 qed

   305

   306 lemma bigo_mult [intro]: "O(f)\<otimes>O(g) <= O(f * g)"

   307   apply (rule subsetI)

   308   apply (subst bigo_def)

   309   apply (auto simp add: bigo_alt_def set_times_def func_times)

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

   311   apply(rule allI)

   312   apply(erule_tac x = x in allE)+

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

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

   315   apply(erule ssubst)

   316   apply (subst abs_mult)

   317   apply (rule mult_mono)

   318   apply assumption+

   319   apply (rule mult_nonneg_nonneg)

   320   apply auto

   321   apply (simp add: mult_ac abs_mult)

   322   done

   323

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

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

   326   apply (rule_tac x = c in exI)

   327   apply auto

   328   apply (drule_tac x = x in spec)

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

   330   apply (force simp add: mult_ac)

   331   apply (rule mult_left_mono, assumption)

   332   apply (rule abs_ge_zero)

   333   done

   334

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

   336   apply (rule subsetD)

   337   apply (rule bigo_mult)

   338   apply (erule set_times_intro, assumption)

   339   done

   340

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

   342   apply (drule set_plus_imp_minus)

   343   apply (rule set_minus_imp_plus)

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

   345   apply (auto simp add: algebra_simps)

   346   done

   347

   348 lemma bigo_mult5:

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

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

   351 proof

   352   fix h

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

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

   355     by auto

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

   357     by (rule bigo_mult2)

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

   359     apply (simp add: func_times)

   360     apply (rule ext)

   361     apply (simp add: assms nonzero_divide_eq_eq mult_ac)

   362     done

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

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

   365     by auto

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

   367     apply (simp add: func_times)

   368     apply (rule ext)

   369     apply (simp add: assms nonzero_divide_eq_eq mult_ac)

   370     done

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

   372 qed

   373

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

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

   376   apply (rule equalityI)

   377   apply (erule bigo_mult5)

   378   apply (rule bigo_mult2)

   379   done

   380

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

   382     O(f * g) <= O(f::'a => ('b::linordered_field)) \<otimes> O(g)"

   383   apply (subst bigo_mult6)

   384   apply assumption

   385   apply (rule set_times_mono3)

   386   apply (rule bigo_refl)

   387   done

   388

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

   390     O(f * g) = O(f::'a => ('b::linordered_field)) \<otimes> O(g)"

   391   apply (rule equalityI)

   392   apply (erule bigo_mult7)

   393   apply (rule bigo_mult)

   394   done

   395

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

   397   by (auto simp add: bigo_def fun_Compl_def)

   398

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

   400   apply (rule set_minus_imp_plus)

   401   apply (drule set_plus_imp_minus)

   402   apply (drule bigo_minus)

   403   apply (simp add: diff_minus)

   404   done

   405

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

   407   by (auto simp add: bigo_def fun_Compl_def)

   408

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

   410 proof -

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

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

   413   proof -

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

   415     then have "f +o O(g) <= O(f) \<oplus> O(g)"

   416       by (auto del: subsetI)

   417     also have "... <= O(g) \<oplus> O(g)"

   418     proof -

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

   420       thus ?thesis by (auto del: subsetI)

   421     qed

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

   423     finally show ?thesis .

   424   qed

   425 qed

   426

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

   428 proof -

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

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

   431   proof -

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

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

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

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

   436       by (simp add: set_plus_rearranges)

   437     finally show ?thesis .

   438   qed

   439 qed

   440

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

   442   apply (rule equalityI)

   443   apply (erule bigo_plus_absorb_lemma1)

   444   apply (erule bigo_plus_absorb_lemma2)

   445   done

   446

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

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

   449   apply force+

   450   done

   451

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

   453   apply (subst set_minus_plus [symmetric])

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

   455   apply (erule ssubst)

   456   apply (rule bigo_minus)

   457   apply (subst set_minus_plus)

   458   apply assumption

   459   apply  (simp add: diff_minus add_ac)

   460   done

   461

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

   463   apply (rule iffI)

   464   apply (erule bigo_add_commute_imp)+

   465   done

   466

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

   468   by (auto simp add: bigo_def mult_ac)

   469

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

   471   apply (rule bigo_elt_subset)

   472   apply (rule bigo_const1)

   473   done

   474

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

   476   apply (simp add: bigo_def)

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

   478   apply (simp add: abs_mult [symmetric])

   479   done

   480

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

   482   by (rule bigo_elt_subset, rule bigo_const3, assumption)

   483

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

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

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

   487

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

   489   apply (simp add: bigo_def)

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

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

   492   done

   493

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

   495   by (rule bigo_elt_subset, rule bigo_const_mult1)

   496

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

   498   apply (simp add: bigo_def)

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

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

   501   done

   502

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

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

   505   by (rule bigo_elt_subset, rule bigo_const_mult3, assumption)

   506

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

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

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

   510

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

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

   513   apply (auto del: subsetI)

   514   apply (rule order_trans)

   515   apply (rule bigo_mult2)

   516   apply (simp add: func_times)

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

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

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

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

   521   apply (rule allI)

   522   apply (subst mult_assoc)

   523   apply (rule mult_left_mono)

   524   apply (erule spec)

   525   apply force

   526   done

   527

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

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

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

   531   apply (rule allI)

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

   533   apply (erule ssubst)

   534   apply (subst abs_mult)

   535   apply (rule mult_left_mono)

   536   apply (erule spec)

   537   apply simp

   538   apply(simp add: mult_ac)

   539   done

   540

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

   542 proof -

   543   assume "f =o O(g)"

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

   545     by auto

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

   547     by (simp add: func_times)

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

   549     by (auto del: subsetI)

   550   finally show ?thesis .

   551 qed

   552

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

   554 by (unfold bigo_def, auto)

   555

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

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

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

   559       func_plus)

   560   apply (erule bigo_compose1)

   561 done

   562

   563

   564 subsection {* Setsum *}

   565

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

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

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

   569   apply (auto simp add: bigo_def)

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

   571   apply (subst abs_of_nonneg) back back

   572   apply (rule setsum_nonneg)

   573   apply force

   574   apply (subst setsum_right_distrib)

   575   apply (rule allI)

   576   apply (rule order_trans)

   577   apply (rule setsum_abs)

   578   apply (rule setsum_mono)

   579   apply (rule order_trans)

   580   apply (drule spec)+

   581   apply (drule bspec)+

   582   apply assumption+

   583   apply (drule bspec)

   584   apply assumption+

   585   apply (rule mult_right_mono)

   586   apply (rule abs_ge_self)

   587   apply force

   588   done

   589

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

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

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

   593   apply (rule bigo_setsum_main)

   594   apply force

   595   apply clarsimp

   596   apply (rule_tac x = c in exI)

   597   apply force

   598   done

   599

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

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

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

   603   by (rule bigo_setsum1, auto)

   604

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

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

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

   608   apply (rule bigo_setsum1)

   609   apply (rule allI)+

   610   apply (rule abs_ge_zero)

   611   apply (unfold bigo_def)

   612   apply auto

   613   apply (rule_tac x = c in exI)

   614   apply (rule allI)+

   615   apply (subst abs_mult)+

   616   apply (subst mult_left_commute)

   617   apply (rule mult_left_mono)

   618   apply (erule spec)

   619   apply (rule abs_ge_zero)

   620   done

   621

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

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

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

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

   626   apply (rule set_minus_imp_plus)

   627   apply (subst fun_diff_def)

   628   apply (subst setsum_subtractf [symmetric])

   629   apply (subst right_diff_distrib [symmetric])

   630   apply (rule bigo_setsum3)

   631   apply (subst fun_diff_def [symmetric])

   632   apply (erule set_plus_imp_minus)

   633   done

   634

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

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

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

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

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

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

   641   apply (erule ssubst)

   642   apply (erule bigo_setsum3)

   643   apply (rule ext)

   644   apply (rule setsum_cong2)

   645   apply (subst abs_of_nonneg)

   646   apply (rule mult_nonneg_nonneg)

   647   apply auto

   648   done

   649

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

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

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

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

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

   655   apply (rule set_minus_imp_plus)

   656   apply (subst fun_diff_def)

   657   apply (subst setsum_subtractf [symmetric])

   658   apply (subst right_diff_distrib [symmetric])

   659   apply (rule bigo_setsum5)

   660   apply (subst fun_diff_def [symmetric])

   661   apply (drule set_plus_imp_minus)

   662   apply auto

   663   done

   664

   665

   666 subsection {* Misc useful stuff *}

   667

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

   669   A \<oplus> B <= O(f)"

   670   apply (subst bigo_plus_idemp [symmetric])

   671   apply (rule set_plus_mono2)

   672   apply assumption+

   673   done

   674

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

   676   apply (subst bigo_plus_idemp [symmetric])

   677   apply (rule set_plus_intro)

   678   apply assumption+

   679   done

   680

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

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

   683   apply (rule subsetD)

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

   685   apply assumption

   686   apply (rule bigo_const_mult6)

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

   688   apply (erule ssubst)

   689   apply (erule set_times_intro2)

   690   apply (simp add: func_times)

   691   done

   692

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

   694     f =o O(h)"

   695   apply (simp add: bigo_alt_def)

   696   apply auto

   697   apply (rule_tac x = c in exI)

   698   apply auto

   699   apply (case_tac "x = 0")

   700   apply simp

   701   apply (rule mult_nonneg_nonneg)

   702   apply force

   703   apply force

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

   705   apply (erule ssubst) back

   706   apply (erule spec)

   707   apply simp

   708   done

   709

   710 lemma bigo_fix2:

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

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

   713   apply (rule set_minus_imp_plus)

   714   apply (rule bigo_fix)

   715   apply (subst fun_diff_def)

   716   apply (subst fun_diff_def [symmetric])

   717   apply (rule set_plus_imp_minus)

   718   apply simp

   719   apply (simp add: fun_diff_def)

   720   done

   721

   722

   723 subsection {* Less than or equal to *}

   724

   725 definition

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

   727     (infixl "<o" 70) where

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

   729

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

   731     g =o O(h)"

   732   apply (unfold bigo_def)

   733   apply clarsimp

   734   apply (rule_tac x = c in exI)

   735   apply (rule allI)

   736   apply (rule order_trans)

   737   apply (erule spec)+

   738   done

   739

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

   741       g =o O(h)"

   742   apply (erule bigo_lesseq1)

   743   apply (rule allI)

   744   apply (drule_tac x = x in spec)

   745   apply (rule order_trans)

   746   apply assumption

   747   apply (rule abs_ge_self)

   748   done

   749

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

   751     g =o O(h)"

   752   apply (erule bigo_lesseq2)

   753   apply (rule allI)

   754   apply (subst abs_of_nonneg)

   755   apply (erule spec)+

   756   done

   757

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

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

   760       g =o O(h)"

   761   apply (erule bigo_lesseq1)

   762   apply (rule allI)

   763   apply (subst abs_of_nonneg)

   764   apply (erule spec)+

   765   done

   766

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

   768   apply (unfold lesso_def)

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

   770   apply (erule ssubst)

   771   apply (rule bigo_zero)

   772   apply (unfold func_zero)

   773   apply (rule ext)

   774   apply (simp split: split_max)

   775   done

   776

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

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

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

   780   apply (unfold lesso_def)

   781   apply (rule bigo_lesseq4)

   782   apply (erule set_plus_imp_minus)

   783   apply (rule allI)

   784   apply (rule le_maxI2)

   785   apply (rule allI)

   786   apply (subst fun_diff_def)

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

   788   apply simp

   789   apply (subst abs_of_nonneg)

   790   apply (drule_tac x = x in spec) back

   791   apply (simp add: algebra_simps)

   792   apply (subst diff_minus)+

   793   apply (rule add_right_mono)

   794   apply (erule spec)

   795   apply (rule order_trans)

   796   prefer 2

   797   apply (rule abs_ge_zero)

   798   apply (simp add: algebra_simps)

   799   done

   800

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

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

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

   804   apply (unfold lesso_def)

   805   apply (rule bigo_lesseq4)

   806   apply (erule set_plus_imp_minus)

   807   apply (rule allI)

   808   apply (rule le_maxI2)

   809   apply (rule allI)

   810   apply (subst fun_diff_def)

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

   812   apply simp

   813   apply (subst abs_of_nonneg)

   814   apply (drule_tac x = x in spec) back

   815   apply (simp add: algebra_simps)

   816   apply (subst diff_minus)+

   817   apply (rule add_left_mono)

   818   apply (rule le_imp_neg_le)

   819   apply (erule spec)

   820   apply (rule order_trans)

   821   prefer 2

   822   apply (rule abs_ge_zero)

   823   apply (simp add: algebra_simps)

   824   done

   825

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

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

   828   apply (unfold lesso_def)

   829   apply (drule set_plus_imp_minus)

   830   apply (drule bigo_abs5) back

   831   apply (simp add: fun_diff_def)

   832   apply (drule bigo_useful_add)

   833   apply assumption

   834   apply (erule bigo_lesseq2) back

   835   apply (rule allI)

   836   apply (auto simp add: func_plus fun_diff_def algebra_simps

   837     split: split_max abs_split)

   838   done

   839

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

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

   842   apply (simp only: lesso_def bigo_alt_def)

   843   apply clarsimp

   844   apply (rule_tac x = c in exI)

   845   apply (rule allI)

   846   apply (drule_tac x = x in spec)

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

   848   apply (clarsimp simp add: algebra_simps)

   849   apply (rule abs_of_nonneg)

   850   apply (rule le_maxI2)

   851   done

   852

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

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

   855   apply (unfold lesso_def)

   856   apply (rule bigo_lesseq3)

   857   apply (erule bigo_useful_add)

   858   apply assumption

   859   apply (force split: split_max)

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

   861   done

   862

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

   864   apply (simp add: LIMSEQ_iff bigo_alt_def)

   865   apply clarify

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

   867   apply (drule mp)

   868   apply (erule divide_pos_pos)

   869   apply assumption

   870   apply clarify

   871   apply (rule_tac x = no in exI)

   872   apply (rule allI)

   873   apply (drule_tac x = n in spec)+

   874   apply (rule impI)

   875   apply (drule mp)

   876   apply assumption

   877   apply (rule order_le_less_trans)

   878   apply assumption

   879   apply (rule order_less_le_trans)

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

   881   apply assumption

   882   apply (erule mult_strict_left_mono)

   883   apply assumption

   884   apply simp

   885 done

   886

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

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

   889   apply (drule set_plus_imp_minus)

   890   apply (drule bigo_LIMSEQ1)

   891   apply assumption

   892   apply (simp only: fun_diff_def)

   893   apply (erule LIMSEQ_diff_approach_zero2)

   894   apply assumption

   895 done

   896

   897 end
`