src/HOL/Library/BigO.thy
 author wenzelm Thu Oct 16 22:44:24 2008 +0200 (2008-10-16) changeset 28615 4c8fa015ec7f parent 27487 c8a6ce181805 child 29667 53103fc8ffa3 permissions -rwxr-xr-x
explicit SORT_CONSTRAINT for proofs depending implicitly on certain sorts;
     1 (*  Title:      HOL/Library/BigO.thy

     2     ID:		$Id$

     3     Authors:    Jeremy Avigad and Kevin Donnelly

     4 *)

     5

     6 header {* Big O notation *}

     7

     8 theory BigO

     9 imports Plain "~~/src/HOL/Presburger" SetsAndFunctions

    10 begin

    11

    12 text {*

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

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

    16 \cite{Avigad-Donnelly}.

    17

    18 The main changes in this version are as follows:

    19 \begin{itemize}

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

    21   to be inessential.)

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

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

    24   involving @{text "setsum"}.

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

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

    27 \end{itemize}

    28

    29 See \verb,Complex/ex/BigO_Complex.thy, for additional lemmas that

    30 require the \verb,HOL-Complex, logic image.

    31

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

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

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

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

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

    37 *}

    38

    39 subsection {* Definitions *}

    40

    41 definition

    42   bigo :: "('a => 'b::ordered_idom) => ('a => 'b) set"  ("(1O'(_'))") where

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

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

    45

    46 lemma bigo_pos_const: "(EX (c::'a::ordered_idom).

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

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

    49   apply auto

    50   apply (case_tac "c = 0")

    51   apply simp

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

    53   apply simp

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

    55   apply auto

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

    57   apply (erule_tac x = x in allE)

    58   apply force

    59   apply (rule mult_right_mono)

    60   apply (rule abs_ge_self)

    61   apply (rule abs_ge_zero)

    62   done

    63

    64 lemma bigo_alt_def: "O(f) =

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

    66   by (auto simp add: bigo_def bigo_pos_const)

    67

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

    69   apply (auto simp add: bigo_alt_def)

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

    71   apply (rule conjI)

    72   apply (rule mult_pos_pos)

    73   apply (assumption)+

    74   apply (rule allI)

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

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

    77   apply (erule order_trans)

    78   apply (simp add: mult_ac)

    79   apply (rule mult_left_mono, assumption)

    80   apply (rule order_less_imp_le, assumption)

    81   done

    82

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

    84   apply(auto simp add: bigo_def)

    85   apply(rule_tac x = 1 in exI)

    86   apply simp

    87   done

    88

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

    90   apply (auto simp add: bigo_def func_zero)

    91   apply (rule_tac x = 0 in exI)

    92   apply auto

    93   done

    94

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

    96   apply (auto simp add: bigo_def)

    97   apply (rule ext)

    98   apply auto

    99   done

   100

   101 lemma bigo_plus_self_subset [intro]:

   102   "O(f) \<oplus> O(f) <= O(f)"

   103   apply (auto simp add: bigo_alt_def set_plus_def)

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

   105   apply auto

   106   apply (simp add: ring_distribs func_plus)

   107   apply (rule order_trans)

   108   apply (rule abs_triangle_ineq)

   109   apply (rule add_mono)

   110   apply force

   111   apply force

   112 done

   113

   114 lemma bigo_plus_idemp [simp]: "O(f) \<oplus> O(f) = O(f)"

   115   apply (rule equalityI)

   116   apply (rule bigo_plus_self_subset)

   117   apply (rule set_zero_plus2)

   118   apply (rule bigo_zero)

   119   done

   120

   121 lemma bigo_plus_subset [intro]: "O(f + g) <= O(f) \<oplus> O(g)"

   122   apply (rule subsetI)

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

   124   apply (subst bigo_pos_const [symmetric])+

   125   apply (rule_tac x =

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

   127   apply (rule conjI)

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

   129   apply (clarsimp)

   130   apply (auto)

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

   132   apply (erule_tac x = xa in allE)

   133   apply (erule order_trans)

   134   apply (simp)

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

   136   apply (erule order_trans)

   137   apply (simp add: ring_distribs)

   138   apply (rule mult_left_mono)

   139   apply assumption

   140   apply (simp add: order_less_le)

   141   apply (rule mult_left_mono)

   142   apply (simp add: abs_triangle_ineq)

   143   apply (simp add: order_less_le)

   144   apply (rule mult_nonneg_nonneg)

   145   apply (rule add_nonneg_nonneg)

   146   apply auto

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

   148      in exI)

   149   apply (rule conjI)

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

   151   apply auto

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

   153   apply (erule_tac x = xa in allE)

   154   apply (erule order_trans)

   155   apply (simp)

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

   157   apply (erule order_trans)

   158   apply (simp add: ring_distribs)

   159   apply (rule mult_left_mono)

   160   apply (simp add: order_less_le)

   161   apply (simp add: order_less_le)

   162   apply (rule mult_left_mono)

   163   apply (rule abs_triangle_ineq)

   164   apply (simp add: order_less_le)

   165   apply (rule mult_nonneg_nonneg)

   166   apply (rule add_nonneg_nonneg)

   167   apply (erule order_less_imp_le)+

   168   apply simp

   169   apply (rule ext)

   170   apply (auto simp add: if_splits linorder_not_le)

   171   done

   172

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

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

   175   apply (erule order_trans)

   176   apply simp

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

   178   done

   179

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

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

   182   apply (rule equalityI)

   183   apply (rule bigo_plus_subset)

   184   apply (simp add: bigo_alt_def set_plus_def func_plus)

   185   apply clarify

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

   187   apply (rule conjI)

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

   189   apply (erule order_less_le_trans)

   190   apply assumption

   191   apply (rule le_maxI1)

   192   apply clarify

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

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

   195   apply (simp add: ring_distribs)

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

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

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

   199   apply (force)

   200   apply (rule add_mono)

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

   202   apply (force)

   203   apply (rule mult_right_mono)

   204   apply (rule le_maxI1)

   205   apply assumption

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

   207   apply (force)

   208   apply (rule mult_right_mono)

   209   apply (rule le_maxI2)

   210   apply assumption

   211   apply (rule abs_triangle_ineq)

   212   apply (rule add_nonneg_nonneg)

   213   apply assumption+

   214   done

   215

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

   217     f : O(g)"

   218   apply (auto simp add: bigo_def)

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

   220   apply auto

   221   apply (drule_tac x = x in spec)+

   222   apply (simp add: abs_mult [symmetric])

   223   done

   224

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

   226     f : O(g)"

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

   228   apply simp

   229   done

   230

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

   232     f : lb +o O(g)"

   233   apply (rule set_minus_imp_plus)

   234   apply (rule bigo_bounded)

   235   apply (auto simp add: diff_minus fun_Compl_def func_plus)

   236   apply (drule_tac x = x in spec)+

   237   apply force

   238   apply (drule_tac x = x in spec)+

   239   apply force

   240   done

   241

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

   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_abs2: "f =o O(%x. abs(f x))"

   250   apply (unfold bigo_def)

   251   apply auto

   252   apply (rule_tac x = 1 in exI)

   253   apply auto

   254   done

   255

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

   257   apply (rule equalityI)

   258   apply (rule bigo_elt_subset)

   259   apply (rule bigo_abs2)

   260   apply (rule bigo_elt_subset)

   261   apply (rule bigo_abs)

   262   done

   263

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

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

   266   apply (drule set_plus_imp_minus)

   267   apply (rule set_minus_imp_plus)

   268   apply (subst fun_diff_def)

   269 proof -

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

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

   272     by (rule bigo_abs2)

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

   274     apply (rule bigo_elt_subset)

   275     apply (rule bigo_bounded)

   276     apply force

   277     apply (rule allI)

   278     apply (rule abs_triangle_ineq3)

   279     done

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

   281     apply (rule bigo_elt_subset)

   282     apply (subst fun_diff_def)

   283     apply (rule bigo_abs)

   284     done

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

   286     by (rule bigo_elt_subset)

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

   288 qed

   289

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

   291   by (unfold bigo_def, auto)

   292

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

   294 proof -

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

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

   297     by (auto del: subsetI)

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

   299     apply (subst bigo_abs3 [symmetric])+

   300     apply (rule refl)

   301     done

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

   303     by (rule bigo_plus_eq [symmetric], auto)

   304   finally have "f : ...".

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

   306     by (elim bigo_elt_subset)

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

   308     by (rule bigo_plus_eq, auto)

   309   finally show ?thesis

   310     by (simp add: bigo_abs3 [symmetric])

   311 qed

   312

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

   314   apply (rule subsetI)

   315   apply (subst bigo_def)

   316   apply (auto simp add: bigo_alt_def set_times_def func_times)

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

   318   apply(rule allI)

   319   apply(erule_tac x = x in allE)+

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

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

   322   apply(erule ssubst)

   323   apply (subst abs_mult)

   324   apply (rule mult_mono)

   325   apply assumption+

   326   apply (rule mult_nonneg_nonneg)

   327   apply auto

   328   apply (simp add: mult_ac abs_mult)

   329   done

   330

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

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

   333   apply (rule_tac x = c in exI)

   334   apply auto

   335   apply (drule_tac x = x in spec)

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

   337   apply (force simp add: mult_ac)

   338   apply (rule mult_left_mono, assumption)

   339   apply (rule abs_ge_zero)

   340   done

   341

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

   343   apply (rule subsetD)

   344   apply (rule bigo_mult)

   345   apply (erule set_times_intro, assumption)

   346   done

   347

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

   349   apply (drule set_plus_imp_minus)

   350   apply (rule set_minus_imp_plus)

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

   352   apply (auto simp add: ring_simps)

   353   done

   354

   355 lemma bigo_mult5: "ALL x. f x ~= 0 ==>

   356     O(f * g) <= (f::'a => ('b::ordered_field)) *o O(g)"

   357 proof -

   358   assume "ALL x. f x ~= 0"

   359   show "O(f * g) <= f *o O(g)"

   360   proof

   361     fix h

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

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

   364       by auto

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

   366       by (rule bigo_mult2)

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

   368       apply (simp add: func_times)

   369       apply (rule ext)

   370       apply (simp add: prems nonzero_divide_eq_eq mult_ac)

   371       done

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

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

   374       by auto

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

   376       apply (simp add: func_times)

   377       apply (rule ext)

   378       apply (simp add: prems nonzero_divide_eq_eq mult_ac)

   379       done

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

   381   qed

   382 qed

   383

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

   385     O(f * g) = (f::'a => ('b::ordered_field)) *o O(g)"

   386   apply (rule equalityI)

   387   apply (erule bigo_mult5)

   388   apply (rule bigo_mult2)

   389   done

   390

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

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

   393   apply (subst bigo_mult6)

   394   apply assumption

   395   apply (rule set_times_mono3)

   396   apply (rule bigo_refl)

   397   done

   398

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

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

   401   apply (rule equalityI)

   402   apply (erule bigo_mult7)

   403   apply (rule bigo_mult)

   404   done

   405

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

   407   by (auto simp add: bigo_def fun_Compl_def)

   408

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

   410   apply (rule set_minus_imp_plus)

   411   apply (drule set_plus_imp_minus)

   412   apply (drule bigo_minus)

   413   apply (simp add: diff_minus)

   414   done

   415

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

   417   by (auto simp add: bigo_def fun_Compl_def abs_minus_cancel)

   418

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

   420 proof -

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

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

   423   proof -

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

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

   426       by (auto del: subsetI)

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

   428     proof -

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

   430       thus ?thesis by (auto del: subsetI)

   431     qed

   432     also have "... <= O(g)" by (simp add: bigo_plus_idemp)

   433     finally show ?thesis .

   434   qed

   435 qed

   436

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

   438 proof -

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

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

   441   proof -

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

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

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

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

   446       by (simp add: set_plus_rearranges)

   447     finally show ?thesis .

   448   qed

   449 qed

   450

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

   452   apply (rule equalityI)

   453   apply (erule bigo_plus_absorb_lemma1)

   454   apply (erule bigo_plus_absorb_lemma2)

   455   done

   456

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

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

   459   apply force+

   460   done

   461

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

   463   apply (subst set_minus_plus [symmetric])

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

   465   apply (erule ssubst)

   466   apply (rule bigo_minus)

   467   apply (subst set_minus_plus)

   468   apply assumption

   469   apply  (simp add: diff_minus add_ac)

   470   done

   471

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

   473   apply (rule iffI)

   474   apply (erule bigo_add_commute_imp)+

   475   done

   476

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

   478   by (auto simp add: bigo_def mult_ac)

   479

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

   481   apply (rule bigo_elt_subset)

   482   apply (rule bigo_const1)

   483   done

   484

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

   486   apply (simp add: bigo_def)

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

   488   apply (simp add: abs_mult [symmetric])

   489   done

   490

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

   492   by (rule bigo_elt_subset, rule bigo_const3, assumption)

   493

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

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

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

   497

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

   499   apply (simp add: bigo_def)

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

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

   502   done

   503

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

   505   by (rule bigo_elt_subset, rule bigo_const_mult1)

   506

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

   508   apply (simp add: bigo_def)

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

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

   511   done

   512

   513 lemma bigo_const_mult4: "(c::'a::ordered_field) ~= 0 ==>

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

   515   by (rule bigo_elt_subset, rule bigo_const_mult3, assumption)

   516

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

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

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

   520

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

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

   523   apply (auto del: subsetI)

   524   apply (rule order_trans)

   525   apply (rule bigo_mult2)

   526   apply (simp add: func_times)

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

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

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

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

   531   apply (rule allI)

   532   apply (subst mult_assoc)

   533   apply (rule mult_left_mono)

   534   apply (erule spec)

   535   apply force

   536   done

   537

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

   539   apply (auto intro!: subsetI

   540     simp add: bigo_def elt_set_times_def func_times)

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

   542   apply (rule allI)

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

   544   apply (erule ssubst)

   545   apply (subst abs_mult)

   546   apply (rule mult_left_mono)

   547   apply (erule spec)

   548   apply simp

   549   apply(simp add: mult_ac)

   550   done

   551

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

   553 proof -

   554   assume "f =o O(g)"

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

   556     by auto

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

   558     by (simp add: func_times)

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

   560     by (auto del: subsetI)

   561   finally show ?thesis .

   562 qed

   563

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

   565 by (unfold bigo_def, auto)

   566

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

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

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

   570       func_plus)

   571   apply (erule bigo_compose1)

   572 done

   573

   574

   575 subsection {* Setsum *}

   576

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

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

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

   580   apply (auto simp add: bigo_def)

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

   582   apply (subst abs_of_nonneg) back back

   583   apply (rule setsum_nonneg)

   584   apply force

   585   apply (subst setsum_right_distrib)

   586   apply (rule allI)

   587   apply (rule order_trans)

   588   apply (rule setsum_abs)

   589   apply (rule setsum_mono)

   590   apply (rule order_trans)

   591   apply (drule spec)+

   592   apply (drule bspec)+

   593   apply assumption+

   594   apply (drule bspec)

   595   apply assumption+

   596   apply (rule mult_right_mono)

   597   apply (rule abs_ge_self)

   598   apply force

   599   done

   600

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

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

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

   604   apply (rule bigo_setsum_main)

   605   apply force

   606   apply clarsimp

   607   apply (rule_tac x = c in exI)

   608   apply force

   609   done

   610

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

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

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

   614   by (rule bigo_setsum1, auto)

   615

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

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

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

   619   apply (rule bigo_setsum1)

   620   apply (rule allI)+

   621   apply (rule abs_ge_zero)

   622   apply (unfold bigo_def)

   623   apply auto

   624   apply (rule_tac x = c in exI)

   625   apply (rule allI)+

   626   apply (subst abs_mult)+

   627   apply (subst mult_left_commute)

   628   apply (rule mult_left_mono)

   629   apply (erule spec)

   630   apply (rule abs_ge_zero)

   631   done

   632

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

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

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

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

   637   apply (rule set_minus_imp_plus)

   638   apply (subst fun_diff_def)

   639   apply (subst setsum_subtractf [symmetric])

   640   apply (subst right_diff_distrib [symmetric])

   641   apply (rule bigo_setsum3)

   642   apply (subst fun_diff_def [symmetric])

   643   apply (erule set_plus_imp_minus)

   644   done

   645

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

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

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

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

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

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

   652   apply (erule ssubst)

   653   apply (erule bigo_setsum3)

   654   apply (rule ext)

   655   apply (rule setsum_cong2)

   656   apply (subst abs_of_nonneg)

   657   apply (rule mult_nonneg_nonneg)

   658   apply auto

   659   done

   660

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

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

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

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

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

   666   apply (rule set_minus_imp_plus)

   667   apply (subst fun_diff_def)

   668   apply (subst setsum_subtractf [symmetric])

   669   apply (subst right_diff_distrib [symmetric])

   670   apply (rule bigo_setsum5)

   671   apply (subst fun_diff_def [symmetric])

   672   apply (drule set_plus_imp_minus)

   673   apply auto

   674   done

   675

   676

   677 subsection {* Misc useful stuff *}

   678

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

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

   681   apply (subst bigo_plus_idemp [symmetric])

   682   apply (rule set_plus_mono2)

   683   apply assumption+

   684   done

   685

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

   687   apply (subst bigo_plus_idemp [symmetric])

   688   apply (rule set_plus_intro)

   689   apply assumption+

   690   done

   691

   692 lemma bigo_useful_const_mult: "(c::'a::ordered_field) ~= 0 ==>

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

   694   apply (rule subsetD)

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

   696   apply assumption

   697   apply (rule bigo_const_mult6)

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

   699   apply (erule ssubst)

   700   apply (erule set_times_intro2)

   701   apply (simp add: func_times)

   702   done

   703

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

   705     f =o O(h)"

   706   apply (simp add: bigo_alt_def)

   707   apply auto

   708   apply (rule_tac x = c in exI)

   709   apply auto

   710   apply (case_tac "x = 0")

   711   apply simp

   712   apply (rule mult_nonneg_nonneg)

   713   apply force

   714   apply force

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

   716   apply (erule ssubst) back

   717   apply (erule spec)

   718   apply simp

   719   done

   720

   721 lemma bigo_fix2:

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

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

   724   apply (rule set_minus_imp_plus)

   725   apply (rule bigo_fix)

   726   apply (subst fun_diff_def)

   727   apply (subst fun_diff_def [symmetric])

   728   apply (rule set_plus_imp_minus)

   729   apply simp

   730   apply (simp add: fun_diff_def)

   731   done

   732

   733

   734 subsection {* Less than or equal to *}

   735

   736 definition

   737   lesso :: "('a => 'b::ordered_idom) => ('a => 'b) => ('a => 'b)"

   738     (infixl "<o" 70) where

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

   740

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

   742     g =o O(h)"

   743   apply (unfold bigo_def)

   744   apply clarsimp

   745   apply (rule_tac x = c in exI)

   746   apply (rule allI)

   747   apply (rule order_trans)

   748   apply (erule spec)+

   749   done

   750

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

   752       g =o O(h)"

   753   apply (erule bigo_lesseq1)

   754   apply (rule allI)

   755   apply (drule_tac x = x in spec)

   756   apply (rule order_trans)

   757   apply assumption

   758   apply (rule abs_ge_self)

   759   done

   760

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

   762     g =o O(h)"

   763   apply (erule bigo_lesseq2)

   764   apply (rule allI)

   765   apply (subst abs_of_nonneg)

   766   apply (erule spec)+

   767   done

   768

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

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

   771       g =o O(h)"

   772   apply (erule bigo_lesseq1)

   773   apply (rule allI)

   774   apply (subst abs_of_nonneg)

   775   apply (erule spec)+

   776   done

   777

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

   779   apply (unfold lesso_def)

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

   781   apply (erule ssubst)

   782   apply (rule bigo_zero)

   783   apply (unfold func_zero)

   784   apply (rule ext)

   785   apply (simp split: split_max)

   786   done

   787

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

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

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

   791   apply (unfold lesso_def)

   792   apply (rule bigo_lesseq4)

   793   apply (erule set_plus_imp_minus)

   794   apply (rule allI)

   795   apply (rule le_maxI2)

   796   apply (rule allI)

   797   apply (subst fun_diff_def)

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

   799   apply simp

   800   apply (subst abs_of_nonneg)

   801   apply (drule_tac x = x in spec) back

   802   apply (simp add: compare_rls)

   803   apply (subst diff_minus)+

   804   apply (rule add_right_mono)

   805   apply (erule spec)

   806   apply (rule order_trans)

   807   prefer 2

   808   apply (rule abs_ge_zero)

   809   apply (simp add: compare_rls)

   810   done

   811

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

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

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

   815   apply (unfold lesso_def)

   816   apply (rule bigo_lesseq4)

   817   apply (erule set_plus_imp_minus)

   818   apply (rule allI)

   819   apply (rule le_maxI2)

   820   apply (rule allI)

   821   apply (subst fun_diff_def)

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

   823   apply simp

   824   apply (subst abs_of_nonneg)

   825   apply (drule_tac x = x in spec) back

   826   apply (simp add: compare_rls)

   827   apply (subst diff_minus)+

   828   apply (rule add_left_mono)

   829   apply (rule le_imp_neg_le)

   830   apply (erule spec)

   831   apply (rule order_trans)

   832   prefer 2

   833   apply (rule abs_ge_zero)

   834   apply (simp add: compare_rls)

   835   done

   836

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

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

   839   apply (unfold lesso_def)

   840   apply (drule set_plus_imp_minus)

   841   apply (drule bigo_abs5) back

   842   apply (simp add: fun_diff_def)

   843   apply (drule bigo_useful_add)

   844   apply assumption

   845   apply (erule bigo_lesseq2) back

   846   apply (rule allI)

   847   apply (auto simp add: func_plus fun_diff_def compare_rls

   848     split: split_max abs_split)

   849   done

   850

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

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

   853   apply (simp only: lesso_def bigo_alt_def)

   854   apply clarsimp

   855   apply (rule_tac x = c in exI)

   856   apply (rule allI)

   857   apply (drule_tac x = x in spec)

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

   859   apply (clarsimp simp add: compare_rls add_ac)

   860   apply (rule abs_of_nonneg)

   861   apply (rule le_maxI2)

   862   done

   863

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

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

   866   apply (unfold lesso_def)

   867   apply (rule bigo_lesseq3)

   868   apply (erule bigo_useful_add)

   869   apply assumption

   870   apply (force split: split_max)

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

   872   done

   873

   874 end
`