src/HOL/Library/BigO.thy
 author wenzelm Tue Apr 29 22:50:55 2014 +0200 (2014-04-29) changeset 56796 9f84219715a7 parent 56544 b60d5d119489 child 57418 6ab1c7cb0b8d permissions -rw-r--r--
tuned proofs;
     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 bigo :: "('a \<Rightarrow> 'b::linordered_idom) \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(1O'(_'))")

    38   where "O(f:: 'a \<Rightarrow> 'b) = {h. \<exists>c. \<forall>x. abs (h x) \<le> c * abs (f x)}"

    39

    40 lemma bigo_pos_const:

    41   "(\<exists>c::'a::linordered_idom. \<forall>x. abs (h x) \<le> c * abs (f x)) \<longleftrightarrow>

    42     (\<exists>c. 0 < c \<and> (\<forall>x. abs (h x) \<le> c * abs (f x)))"

    43   apply auto

    44   apply (case_tac "c = 0")

    45   apply simp

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

    47   apply simp

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

    49   apply auto

    50   apply (subgoal_tac "c * abs (f x) \<le> abs c * abs (f x)")

    51   apply (erule_tac x = x in allE)

    52   apply force

    53   apply (rule mult_right_mono)

    54   apply (rule abs_ge_self)

    55   apply (rule abs_ge_zero)

    56   done

    57

    58 lemma bigo_alt_def: "O(f) = {h. \<exists>c. 0 < c \<and> (\<forall>x. abs (h x) \<le> c * abs (f x))}"

    59   by (auto simp add: bigo_def bigo_pos_const)

    60

    61 lemma bigo_elt_subset [intro]: "f \<in> O(g) \<Longrightarrow> O(f) \<le> O(g)"

    62   apply (auto simp add: bigo_alt_def)

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

    64   apply (rule conjI)

    65   apply simp

    66   apply (rule allI)

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

    68   apply (subgoal_tac "ca * abs (f xa) \<le> ca * (c * abs (g xa))")

    69   apply (erule order_trans)

    70   apply (simp add: mult_ac)

    71   apply (rule mult_left_mono, assumption)

    72   apply (rule order_less_imp_le, assumption)

    73   done

    74

    75 lemma bigo_refl [intro]: "f \<in> O(f)"

    76   apply(auto simp add: bigo_def)

    77   apply(rule_tac x = 1 in exI)

    78   apply simp

    79   done

    80

    81 lemma bigo_zero: "0 \<in> O(g)"

    82   apply (auto simp add: bigo_def func_zero)

    83   apply (rule_tac x = 0 in exI)

    84   apply auto

    85   done

    86

    87 lemma bigo_zero2: "O(\<lambda>x. 0) = {\<lambda>x. 0}"

    88   by (auto simp add: bigo_def)

    89

    90 lemma bigo_plus_self_subset [intro]: "O(f) + O(f) \<subseteq> O(f)"

    91   apply (auto simp add: bigo_alt_def set_plus_def)

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

    93   apply auto

    94   apply (simp add: ring_distribs func_plus)

    95   apply (rule order_trans)

    96   apply (rule abs_triangle_ineq)

    97   apply (rule add_mono)

    98   apply force

    99   apply force

   100   done

   101

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

   103   apply (rule equalityI)

   104   apply (rule bigo_plus_self_subset)

   105   apply (rule set_zero_plus2)

   106   apply (rule bigo_zero)

   107   done

   108

   109 lemma bigo_plus_subset [intro]: "O(f + g) \<subseteq> O(f) + O(g)"

   110   apply (rule subsetI)

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

   112   apply (subst bigo_pos_const [symmetric])+

   113   apply (rule_tac x = "\<lambda>n. if abs (g n) \<le> (abs (f n)) then x n else 0" in exI)

   114   apply (rule conjI)

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

   116   apply (clarsimp)

   117   apply (subgoal_tac "c * abs (f xa + g xa) \<le> (c + c) * abs (f xa)")

   118   apply (erule_tac x = xa in allE)

   119   apply (erule order_trans)

   120   apply (simp)

   121   apply (subgoal_tac "c * abs (f xa + g xa) \<le> c * (abs (f xa) + abs (g xa))")

   122   apply (erule order_trans)

   123   apply (simp add: ring_distribs)

   124   apply (rule mult_left_mono)

   125   apply (simp add: abs_triangle_ineq)

   126   apply (simp add: order_less_le)

   127   apply (rule_tac x = "\<lambda>n. if (abs (f n)) < abs (g n) then x n else 0" in exI)

   128   apply (rule conjI)

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

   130   apply auto

   131   apply (subgoal_tac "c * abs (f xa + g xa) \<le> (c + c) * abs (g 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) \<le> 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 (rule abs_triangle_ineq)

   140   apply (simp add: order_less_le)

   141   done

   142

   143 lemma bigo_plus_subset2 [intro]: "A \<subseteq> O(f) \<Longrightarrow> B \<subseteq> O(f) \<Longrightarrow> A + B \<subseteq> O(f)"

   144   apply (subgoal_tac "A + B \<subseteq> O(f) + O(f)")

   145   apply (erule order_trans)

   146   apply simp

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

   148   done

   149

   150 lemma bigo_plus_eq: "\<forall>x. 0 \<le> f x \<Longrightarrow> \<forall>x. 0 \<le> g x \<Longrightarrow> O(f + g) = O(f) + O(g)"

   151   apply (rule equalityI)

   152   apply (rule bigo_plus_subset)

   153   apply (simp add: bigo_alt_def set_plus_def func_plus)

   154   apply clarify

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

   156   apply (rule conjI)

   157   apply (subgoal_tac "c \<le> max c ca")

   158   apply (erule order_less_le_trans)

   159   apply assumption

   160   apply (rule max.cobounded1)

   161   apply clarify

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

   163   apply (subgoal_tac "0 \<le> f xa + g xa")

   164   apply (simp add: ring_distribs)

   165   apply (subgoal_tac "abs (a xa + b xa) \<le> abs (a xa) + abs (b xa)")

   166   apply (subgoal_tac "abs (a xa) + abs (b xa) \<le> max c ca * f xa + max c ca * g xa")

   167   apply force

   168   apply (rule add_mono)

   169   apply (subgoal_tac "c * f xa \<le> max c ca * f xa")

   170   apply force

   171   apply (rule mult_right_mono)

   172   apply (rule max.cobounded1)

   173   apply assumption

   174   apply (subgoal_tac "ca * g xa \<le> max c ca * g xa")

   175   apply force

   176   apply (rule mult_right_mono)

   177   apply (rule max.cobounded2)

   178   apply assumption

   179   apply (rule abs_triangle_ineq)

   180   apply (rule add_nonneg_nonneg)

   181   apply assumption+

   182   done

   183

   184 lemma bigo_bounded_alt: "\<forall>x. 0 \<le> f x \<Longrightarrow> \<forall>x. f x \<le> c * g x \<Longrightarrow> f \<in> O(g)"

   185   apply (auto simp add: bigo_def)

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

   187   apply auto

   188   apply (drule_tac x = x in spec)+

   189   apply (simp add: abs_mult [symmetric])

   190   done

   191

   192 lemma bigo_bounded: "\<forall>x. 0 \<le> f x \<Longrightarrow> \<forall>x. f x \<le> g x \<Longrightarrow> f \<in> O(g)"

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

   194   apply simp

   195   done

   196

   197 lemma bigo_bounded2: "\<forall>x. lb x \<le> f x \<Longrightarrow> \<forall>x. f x \<le> lb x + g x \<Longrightarrow> f \<in> lb +o O(g)"

   198   apply (rule set_minus_imp_plus)

   199   apply (rule bigo_bounded)

   200   apply (auto simp add: fun_Compl_def func_plus)

   201   apply (drule_tac x = x in spec)+

   202   apply force

   203   apply (drule_tac x = x in spec)+

   204   apply force

   205   done

   206

   207 lemma bigo_abs: "(\<lambda>x. abs (f x)) =o O(f)"

   208   apply (unfold bigo_def)

   209   apply auto

   210   apply (rule_tac x = 1 in exI)

   211   apply auto

   212   done

   213

   214 lemma bigo_abs2: "f =o O(\<lambda>x. abs (f x))"

   215   apply (unfold bigo_def)

   216   apply auto

   217   apply (rule_tac x = 1 in exI)

   218   apply auto

   219   done

   220

   221 lemma bigo_abs3: "O(f) = O(\<lambda>x. abs (f x))"

   222   apply (rule equalityI)

   223   apply (rule bigo_elt_subset)

   224   apply (rule bigo_abs2)

   225   apply (rule bigo_elt_subset)

   226   apply (rule bigo_abs)

   227   done

   228

   229 lemma bigo_abs4: "f =o g +o O(h) \<Longrightarrow> (\<lambda>x. abs (f x)) =o (\<lambda>x. abs (g x)) +o O(h)"

   230   apply (drule set_plus_imp_minus)

   231   apply (rule set_minus_imp_plus)

   232   apply (subst fun_diff_def)

   233 proof -

   234   assume a: "f - g \<in> O(h)"

   235   have "(\<lambda>x. abs (f x) - abs (g x)) =o O(\<lambda>x. abs (abs (f x) - abs (g x)))"

   236     by (rule bigo_abs2)

   237   also have "\<dots> \<subseteq> O(\<lambda>x. abs (f x - g x))"

   238     apply (rule bigo_elt_subset)

   239     apply (rule bigo_bounded)

   240     apply force

   241     apply (rule allI)

   242     apply (rule abs_triangle_ineq3)

   243     done

   244   also have "\<dots> \<subseteq> O(f - g)"

   245     apply (rule bigo_elt_subset)

   246     apply (subst fun_diff_def)

   247     apply (rule bigo_abs)

   248     done

   249   also from a have "\<dots> \<subseteq> O(h)"

   250     by (rule bigo_elt_subset)

   251   finally show "(\<lambda>x. abs (f x) - abs (g x)) \<in> O(h)".

   252 qed

   253

   254 lemma bigo_abs5: "f =o O(g) \<Longrightarrow> (\<lambda>x. abs (f x)) =o O(g)"

   255   by (unfold bigo_def, auto)

   256

   257 lemma bigo_elt_subset2 [intro]: "f \<in> g +o O(h) \<Longrightarrow> O(f) \<subseteq> O(g) + O(h)"

   258 proof -

   259   assume "f \<in> g +o O(h)"

   260   also have "\<dots> \<subseteq> O(g) + O(h)"

   261     by (auto del: subsetI)

   262   also have "\<dots> = O(\<lambda>x. abs (g x)) + O(\<lambda>x. abs (h x))"

   263     apply (subst bigo_abs3 [symmetric])+

   264     apply (rule refl)

   265     done

   266   also have "\<dots> = O((\<lambda>x. abs (g x)) + (\<lambda>x. abs (h x)))"

   267     by (rule bigo_plus_eq [symmetric]) auto

   268   finally have "f \<in> \<dots>" .

   269   then have "O(f) \<subseteq> \<dots>"

   270     by (elim bigo_elt_subset)

   271   also have "\<dots> = O(\<lambda>x. abs (g x)) + O(\<lambda>x. abs (h x))"

   272     by (rule bigo_plus_eq, auto)

   273   finally show ?thesis

   274     by (simp add: bigo_abs3 [symmetric])

   275 qed

   276

   277 lemma bigo_mult [intro]: "O(f)*O(g) \<subseteq> O(f * g)"

   278   apply (rule subsetI)

   279   apply (subst bigo_def)

   280   apply (auto simp add: bigo_alt_def set_times_def func_times)

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

   282   apply (rule allI)

   283   apply (erule_tac x = x in allE)+

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

   285   apply (erule ssubst)

   286   apply (subst abs_mult)

   287   apply (rule mult_mono)

   288   apply assumption+

   289   apply auto

   290   apply (simp add: mult_ac abs_mult)

   291   done

   292

   293 lemma bigo_mult2 [intro]: "f *o O(g) \<subseteq> O(f * g)"

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

   295   apply (rule_tac x = c in exI)

   296   apply auto

   297   apply (drule_tac x = x in spec)

   298   apply (subgoal_tac "abs (f x) * abs (b x) \<le> abs (f x) * (c * abs (g x))")

   299   apply (force simp add: mult_ac)

   300   apply (rule mult_left_mono, assumption)

   301   apply (rule abs_ge_zero)

   302   done

   303

   304 lemma bigo_mult3: "f \<in> O(h) \<Longrightarrow> g \<in> O(j) \<Longrightarrow> f * g \<in> O(h * j)"

   305   apply (rule subsetD)

   306   apply (rule bigo_mult)

   307   apply (erule set_times_intro, assumption)

   308   done

   309

   310 lemma bigo_mult4 [intro]: "f \<in> k +o O(h) \<Longrightarrow> g * f \<in> (g * k) +o O(g * h)"

   311   apply (drule set_plus_imp_minus)

   312   apply (rule set_minus_imp_plus)

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

   314   apply (auto simp add: algebra_simps)

   315   done

   316

   317 lemma bigo_mult5:

   318   fixes f :: "'a \<Rightarrow> 'b::linordered_field"

   319   assumes "\<forall>x. f x \<noteq> 0"

   320   shows "O(f * g) \<subseteq> f *o O(g)"

   321 proof

   322   fix h

   323   assume "h \<in> O(f * g)"

   324   then have "(\<lambda>x. 1 / (f x)) * h \<in> (\<lambda>x. 1 / f x) *o O(f * g)"

   325     by auto

   326   also have "\<dots> \<subseteq> O((\<lambda>x. 1 / f x) * (f * g))"

   327     by (rule bigo_mult2)

   328   also have "(\<lambda>x. 1 / f x) * (f * g) = g"

   329     apply (simp add: func_times)

   330     apply (rule ext)

   331     apply (simp add: assms nonzero_divide_eq_eq mult_ac)

   332     done

   333   finally have "(\<lambda>x. (1::'b) / f x) * h \<in> O(g)" .

   334   then have "f * ((\<lambda>x. (1::'b) / f x) * h) \<in> f *o O(g)"

   335     by auto

   336   also have "f * ((\<lambda>x. (1::'b) / f x) * h) = h"

   337     apply (simp add: func_times)

   338     apply (rule ext)

   339     apply (simp add: assms nonzero_divide_eq_eq mult_ac)

   340     done

   341   finally show "h \<in> f *o O(g)" .

   342 qed

   343

   344 lemma bigo_mult6:

   345   fixes f :: "'a \<Rightarrow> 'b::linordered_field"

   346   shows "\<forall>x. f x \<noteq> 0 \<Longrightarrow> O(f * g) = f *o O(g)"

   347   apply (rule equalityI)

   348   apply (erule bigo_mult5)

   349   apply (rule bigo_mult2)

   350   done

   351

   352 lemma bigo_mult7:

   353   fixes f :: "'a \<Rightarrow> 'b::linordered_field"

   354   shows "\<forall>x. f x \<noteq> 0 \<Longrightarrow> O(f * g) \<subseteq> O(f) * O(g)"

   355   apply (subst bigo_mult6)

   356   apply assumption

   357   apply (rule set_times_mono3)

   358   apply (rule bigo_refl)

   359   done

   360

   361 lemma bigo_mult8:

   362   fixes f :: "'a \<Rightarrow> 'b::linordered_field"

   363   shows "\<forall>x. f x \<noteq> 0 \<Longrightarrow> O(f * g) = O(f) * O(g)"

   364   apply (rule equalityI)

   365   apply (erule bigo_mult7)

   366   apply (rule bigo_mult)

   367   done

   368

   369 lemma bigo_minus [intro]: "f \<in> O(g) \<Longrightarrow> - f \<in> O(g)"

   370   by (auto simp add: bigo_def fun_Compl_def)

   371

   372 lemma bigo_minus2: "f \<in> g +o O(h) \<Longrightarrow> - f \<in> -g +o O(h)"

   373   apply (rule set_minus_imp_plus)

   374   apply (drule set_plus_imp_minus)

   375   apply (drule bigo_minus)

   376   apply simp

   377   done

   378

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

   380   by (auto simp add: bigo_def fun_Compl_def)

   381

   382 lemma bigo_plus_absorb_lemma1: "f \<in> O(g) \<Longrightarrow> f +o O(g) \<subseteq> O(g)"

   383 proof -

   384   assume a: "f \<in> O(g)"

   385   show "f +o O(g) \<subseteq> O(g)"

   386   proof -

   387     have "f \<in> O(f)" by auto

   388     then have "f +o O(g) \<subseteq> O(f) + O(g)"

   389       by (auto del: subsetI)

   390     also have "\<dots> \<subseteq> O(g) + O(g)"

   391     proof -

   392       from a have "O(f) \<subseteq> O(g)" by (auto del: subsetI)

   393       then show ?thesis by (auto del: subsetI)

   394     qed

   395     also have "\<dots> \<subseteq> O(g)" by simp

   396     finally show ?thesis .

   397   qed

   398 qed

   399

   400 lemma bigo_plus_absorb_lemma2: "f \<in> O(g) \<Longrightarrow> O(g) \<subseteq> f +o O(g)"

   401 proof -

   402   assume a: "f \<in> O(g)"

   403   show "O(g) \<subseteq> f +o O(g)"

   404   proof -

   405     from a have "- f \<in> O(g)"

   406       by auto

   407     then have "- f +o O(g) \<subseteq> O(g)"

   408       by (elim bigo_plus_absorb_lemma1)

   409     then have "f +o (- f +o O(g)) \<subseteq> f +o O(g)"

   410       by auto

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

   412       by (simp add: set_plus_rearranges)

   413     finally show ?thesis .

   414   qed

   415 qed

   416

   417 lemma bigo_plus_absorb [simp]: "f \<in> O(g) \<Longrightarrow> f +o O(g) = O(g)"

   418   apply (rule equalityI)

   419   apply (erule bigo_plus_absorb_lemma1)

   420   apply (erule bigo_plus_absorb_lemma2)

   421   done

   422

   423 lemma bigo_plus_absorb2 [intro]: "f \<in> O(g) \<Longrightarrow> A \<subseteq> O(g) \<Longrightarrow> f +o A \<subseteq> O(g)"

   424   apply (subgoal_tac "f +o A \<subseteq> f +o O(g)")

   425   apply force+

   426   done

   427

   428 lemma bigo_add_commute_imp: "f \<in> g +o O(h) \<Longrightarrow> g \<in> f +o O(h)"

   429   apply (subst set_minus_plus [symmetric])

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

   431   apply (erule ssubst)

   432   apply (rule bigo_minus)

   433   apply (subst set_minus_plus)

   434   apply assumption

   435   apply (simp add: add_ac)

   436   done

   437

   438 lemma bigo_add_commute: "f \<in> g +o O(h) \<longleftrightarrow> g \<in> f +o O(h)"

   439   apply (rule iffI)

   440   apply (erule bigo_add_commute_imp)+

   441   done

   442

   443 lemma bigo_const1: "(\<lambda>x. c) \<in> O(\<lambda>x. 1)"

   444   by (auto simp add: bigo_def mult_ac)

   445

   446 lemma bigo_const2 [intro]: "O(\<lambda>x. c) \<subseteq> O(\<lambda>x. 1)"

   447   apply (rule bigo_elt_subset)

   448   apply (rule bigo_const1)

   449   done

   450

   451 lemma bigo_const3:

   452   fixes c :: "'a::linordered_field"

   453   shows "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. 1) \<in> O(\<lambda>x. c)"

   454   apply (simp add: bigo_def)

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

   456   apply (simp add: abs_mult [symmetric])

   457   done

   458

   459 lemma bigo_const4:

   460   fixes c :: "'a::linordered_field"

   461   shows "c \<noteq> 0 \<Longrightarrow> O(\<lambda>x. 1) \<subseteq> O(\<lambda>x. c)"

   462   apply (rule bigo_elt_subset)

   463   apply (rule bigo_const3)

   464   apply assumption

   465   done

   466

   467 lemma bigo_const [simp]:

   468   fixes c :: "'a::linordered_field"

   469   shows "c \<noteq> 0 \<Longrightarrow> O(\<lambda>x. c) = O(\<lambda>x. 1)"

   470   apply (rule equalityI)

   471   apply (rule bigo_const2)

   472   apply (rule bigo_const4)

   473   apply assumption

   474   done

   475

   476 lemma bigo_const_mult1: "(\<lambda>x. c * f x) \<in> O(f)"

   477   apply (simp add: bigo_def)

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

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

   480   done

   481

   482 lemma bigo_const_mult2: "O(\<lambda>x. c * f x) \<subseteq> O(f)"

   483   apply (rule bigo_elt_subset)

   484   apply (rule bigo_const_mult1)

   485   done

   486

   487 lemma bigo_const_mult3:

   488   fixes c :: "'a::linordered_field"

   489   shows "c \<noteq> 0 \<Longrightarrow> f \<in> O(\<lambda>x. c * f x)"

   490   apply (simp add: bigo_def)

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

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

   493   done

   494

   495 lemma bigo_const_mult4:

   496   fixes c :: "'a::linordered_field"

   497   shows "c \<noteq> 0 \<Longrightarrow> O(f) \<subseteq> O(\<lambda>x. c * f x)"

   498   apply (rule bigo_elt_subset)

   499   apply (rule bigo_const_mult3)

   500   apply assumption

   501   done

   502

   503 lemma bigo_const_mult [simp]:

   504   fixes c :: "'a::linordered_field"

   505   shows "c \<noteq> 0 \<Longrightarrow> O(\<lambda>x. c * f x) = O(f)"

   506   apply (rule equalityI)

   507   apply (rule bigo_const_mult2)

   508   apply (erule bigo_const_mult4)

   509   done

   510

   511 lemma bigo_const_mult5 [simp]:

   512   fixes c :: "'a::linordered_field"

   513   shows "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. c) *o O(f) = O(f)"

   514   apply (auto del: subsetI)

   515   apply (rule order_trans)

   516   apply (rule bigo_mult2)

   517   apply (simp add: func_times)

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

   519   apply (rule_tac x = "\<lambda>y. inverse c * x y" in exI)

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

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

   522   apply (rule allI)

   523   apply (subst mult_assoc)

   524   apply (rule mult_left_mono)

   525   apply (erule spec)

   526   apply force

   527   done

   528

   529 lemma bigo_const_mult6 [intro]: "(\<lambda>x. c) *o O(f) \<subseteq> O(f)"

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

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

   532   apply (rule allI)

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

   534   apply (erule ssubst)

   535   apply (subst abs_mult)

   536   apply (rule mult_left_mono)

   537   apply (erule spec)

   538   apply simp

   539   apply(simp add: mult_ac)

   540   done

   541

   542 lemma bigo_const_mult7 [intro]: "f =o O(g) \<Longrightarrow> (\<lambda>x. c * f x) =o O(g)"

   543 proof -

   544   assume "f =o O(g)"

   545   then have "(\<lambda>x. c) * f =o (\<lambda>x. c) *o O(g)"

   546     by auto

   547   also have "(\<lambda>x. c) * f = (\<lambda>x. c * f x)"

   548     by (simp add: func_times)

   549   also have "(\<lambda>x. c) *o O(g) \<subseteq> O(g)"

   550     by (auto del: subsetI)

   551   finally show ?thesis .

   552 qed

   553

   554 lemma bigo_compose1: "f =o O(g) \<Longrightarrow> (\<lambda>x. f (k x)) =o O(\<lambda>x. g (k x))"

   555   unfolding bigo_def by auto

   556

   557 lemma bigo_compose2: "f =o g +o O(h) \<Longrightarrow>

   558     (\<lambda>x. f (k x)) =o (\<lambda>x. g (k x)) +o O(\<lambda>x. h(k x))"

   559   apply (simp only: set_minus_plus [symmetric] fun_Compl_def func_plus)

   560   apply (drule bigo_compose1)

   561   apply (simp add: fun_diff_def)

   562   done

   563

   564

   565 subsection {* Setsum *}

   566

   567 lemma bigo_setsum_main: "\<forall>x. \<forall>y \<in> A x. 0 \<le> h x y \<Longrightarrow>

   568     \<exists>c. \<forall>x. \<forall>y \<in> A x. abs (f x y) \<le> c * (h x y) \<Longrightarrow>

   569       (\<lambda>x. \<Sum>y \<in> A x. f x y) =o O(\<lambda>x. \<Sum>y \<in> A x. h x y)"

   570   apply (auto simp add: bigo_def)

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

   572   apply (subst abs_of_nonneg) back back

   573   apply (rule setsum_nonneg)

   574   apply force

   575   apply (subst setsum_right_distrib)

   576   apply (rule allI)

   577   apply (rule order_trans)

   578   apply (rule setsum_abs)

   579   apply (rule setsum_mono)

   580   apply (rule order_trans)

   581   apply (drule spec)+

   582   apply (drule bspec)+

   583   apply assumption+

   584   apply (drule bspec)

   585   apply assumption+

   586   apply (rule mult_right_mono)

   587   apply (rule abs_ge_self)

   588   apply force

   589   done

   590

   591 lemma bigo_setsum1: "\<forall>x y. 0 \<le> h x y \<Longrightarrow>

   592     \<exists>c. \<forall>x y. abs (f x y) \<le> c * h x y \<Longrightarrow>

   593       (\<lambda>x. \<Sum>y \<in> A x. f x y) =o O(\<lambda>x. \<Sum>y \<in> A x. h x y)"

   594   apply (rule bigo_setsum_main)

   595   apply force

   596   apply clarsimp

   597   apply (rule_tac x = c in exI)

   598   apply force

   599   done

   600

   601 lemma bigo_setsum2: "\<forall>y. 0 \<le> h y \<Longrightarrow>

   602     \<exists>c. \<forall>y. abs (f y) \<le> c * (h y) \<Longrightarrow>

   603       (\<lambda>x. \<Sum>y \<in> A x. f y) =o O(\<lambda>x. \<Sum>y \<in> A x. h y)"

   604   by (rule bigo_setsum1) auto

   605

   606 lemma bigo_setsum3: "f =o O(h) \<Longrightarrow>

   607     (\<lambda>x. \<Sum>y \<in> A x. l x y * f (k x y)) =o O(\<lambda>x. \<Sum>y \<in> 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) \<Longrightarrow>

   623     (\<lambda>x. \<Sum>y \<in> A x. l x y * f (k x y)) =o

   624       (\<lambda>x. \<Sum>y \<in> A x. l x y * g (k x y)) +o

   625         O(\<lambda>x. \<Sum>y \<in> 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) \<Longrightarrow> \<forall>x y. 0 \<le> l x y \<Longrightarrow>

   636     \<forall>x. 0 \<le> h x \<Longrightarrow>

   637       (\<lambda>x. \<Sum>y \<in> A x. l x y * f (k x y)) =o

   638         O(\<lambda>x. \<Sum>y \<in> A x. l x y * h (k x y))"

   639   apply (subgoal_tac "(\<lambda>x. \<Sum>y \<in> A x. l x y * h (k x y)) =

   640       (\<lambda>x. \<Sum>y \<in> 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 auto

   647   done

   648

   649 lemma bigo_setsum6: "f =o g +o O(h) \<Longrightarrow> \<forall>x y. 0 \<le> l x y \<Longrightarrow>

   650     \<forall>x. 0 \<le> h x \<Longrightarrow>

   651       (\<lambda>x. \<Sum>y \<in> A x. l x y * f (k x y)) =o

   652         (\<lambda>x. \<Sum>y \<in> A x. l x y * g (k x y)) +o

   653           O(\<lambda>x. \<Sum>y \<in> A x. l x y * h (k x y))"

   654   apply (rule set_minus_imp_plus)

   655   apply (subst fun_diff_def)

   656   apply (subst setsum_subtractf [symmetric])

   657   apply (subst right_diff_distrib [symmetric])

   658   apply (rule bigo_setsum5)

   659   apply (subst fun_diff_def [symmetric])

   660   apply (drule set_plus_imp_minus)

   661   apply auto

   662   done

   663

   664

   665 subsection {* Misc useful stuff *}

   666

   667 lemma bigo_useful_intro: "A \<subseteq> O(f) \<Longrightarrow> B \<subseteq> O(f) \<Longrightarrow> A + B \<subseteq> O(f)"

   668   apply (subst bigo_plus_idemp [symmetric])

   669   apply (rule set_plus_mono2)

   670   apply assumption+

   671   done

   672

   673 lemma bigo_useful_add: "f =o O(h) \<Longrightarrow> g =o O(h) \<Longrightarrow> f + g =o O(h)"

   674   apply (subst bigo_plus_idemp [symmetric])

   675   apply (rule set_plus_intro)

   676   apply assumption+

   677   done

   678

   679 lemma bigo_useful_const_mult:

   680   fixes c :: "'a::linordered_field"

   681   shows "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. c) * f =o O(h) \<Longrightarrow> f =o O(h)"

   682   apply (rule subsetD)

   683   apply (subgoal_tac "(\<lambda>x. 1 / c) *o O(h) \<subseteq> O(h)")

   684   apply assumption

   685   apply (rule bigo_const_mult6)

   686   apply (subgoal_tac "f = (\<lambda>x. 1 / c) * ((\<lambda>x. c) * f)")

   687   apply (erule ssubst)

   688   apply (erule set_times_intro2)

   689   apply (simp add: func_times)

   690   done

   691

   692 lemma bigo_fix: "(\<lambda>x::nat. f (x + 1)) =o O(\<lambda>x. h (x + 1)) \<Longrightarrow> f 0 = 0 \<Longrightarrow> f =o O(h)"

   693   apply (simp add: bigo_alt_def)

   694   apply auto

   695   apply (rule_tac x = c in exI)

   696   apply auto

   697   apply (case_tac "x = 0")

   698   apply simp

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

   700   apply (erule ssubst) back

   701   apply (erule spec)

   702   apply simp

   703   done

   704

   705 lemma bigo_fix2:

   706     "(\<lambda>x. f ((x::nat) + 1)) =o (\<lambda>x. g(x + 1)) +o O(\<lambda>x. h(x + 1)) \<Longrightarrow>

   707        f 0 = g 0 \<Longrightarrow> f =o g +o O(h)"

   708   apply (rule set_minus_imp_plus)

   709   apply (rule bigo_fix)

   710   apply (subst fun_diff_def)

   711   apply (subst fun_diff_def [symmetric])

   712   apply (rule set_plus_imp_minus)

   713   apply simp

   714   apply (simp add: fun_diff_def)

   715   done

   716

   717

   718 subsection {* Less than or equal to *}

   719

   720 definition lesso :: "('a \<Rightarrow> 'b::linordered_idom) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"  (infixl "<o" 70)

   721   where "f <o g = (\<lambda>x. max (f x - g x) 0)"

   722

   723 lemma bigo_lesseq1: "f =o O(h) \<Longrightarrow> \<forall>x. abs (g x) \<le> abs (f x) \<Longrightarrow> g =o O(h)"

   724   apply (unfold bigo_def)

   725   apply clarsimp

   726   apply (rule_tac x = c in exI)

   727   apply (rule allI)

   728   apply (rule order_trans)

   729   apply (erule spec)+

   730   done

   731

   732 lemma bigo_lesseq2: "f =o O(h) \<Longrightarrow> \<forall>x. abs (g x) \<le> f x \<Longrightarrow> g =o O(h)"

   733   apply (erule bigo_lesseq1)

   734   apply (rule allI)

   735   apply (drule_tac x = x in spec)

   736   apply (rule order_trans)

   737   apply assumption

   738   apply (rule abs_ge_self)

   739   done

   740

   741 lemma bigo_lesseq3: "f =o O(h) \<Longrightarrow> \<forall>x. 0 \<le> g x \<Longrightarrow> \<forall>x. g x \<le> f x \<Longrightarrow> 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) \<Longrightarrow>

   749     \<forall>x. 0 \<le> g x \<Longrightarrow> \<forall>x. g x \<le> abs (f x) \<Longrightarrow> g =o O(h)"

   750   apply (erule bigo_lesseq1)

   751   apply (rule allI)

   752   apply (subst abs_of_nonneg)

   753   apply (erule spec)+

   754   done

   755

   756 lemma bigo_lesso1: "\<forall>x. f x \<le> g x \<Longrightarrow> f <o g =o O(h)"

   757   apply (unfold lesso_def)

   758   apply (subgoal_tac "(\<lambda>x. max (f x - g x) 0) = 0")

   759   apply (erule ssubst)

   760   apply (rule bigo_zero)

   761   apply (unfold func_zero)

   762   apply (rule ext)

   763   apply (simp split: split_max)

   764   done

   765

   766 lemma bigo_lesso2: "f =o g +o O(h) \<Longrightarrow>

   767     \<forall>x. 0 \<le> k x \<Longrightarrow> \<forall>x. k x \<le> f x \<Longrightarrow> k <o g =o O(h)"

   768   apply (unfold lesso_def)

   769   apply (rule bigo_lesseq4)

   770   apply (erule set_plus_imp_minus)

   771   apply (rule allI)

   772   apply (rule max.cobounded2)

   773   apply (rule allI)

   774   apply (subst fun_diff_def)

   775   apply (case_tac "0 \<le> k x - g x")

   776   apply simp

   777   apply (subst abs_of_nonneg)

   778   apply (drule_tac x = x in spec) back

   779   apply (simp add: algebra_simps)

   780   apply (subst diff_conv_add_uminus)+

   781   apply (rule add_right_mono)

   782   apply (erule spec)

   783   apply (rule order_trans)

   784   prefer 2

   785   apply (rule abs_ge_zero)

   786   apply (simp add: algebra_simps)

   787   done

   788

   789 lemma bigo_lesso3: "f =o g +o O(h) \<Longrightarrow>

   790     \<forall>x. 0 \<le> k x \<Longrightarrow> \<forall>x. g x \<le> k x \<Longrightarrow> f <o k =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 max.cobounded2)

   796   apply (rule allI)

   797   apply (subst fun_diff_def)

   798   apply (case_tac "0 \<le> f x - k x")

   799   apply simp

   800   apply (subst abs_of_nonneg)

   801   apply (drule_tac x = x in spec) back

   802   apply (simp add: algebra_simps)

   803   apply (subst diff_conv_add_uminus)+

   804   apply (rule add_left_mono)

   805   apply (rule le_imp_neg_le)

   806   apply (erule spec)

   807   apply (rule order_trans)

   808   prefer 2

   809   apply (rule abs_ge_zero)

   810   apply (simp add: algebra_simps)

   811   done

   812

   813 lemma bigo_lesso4:

   814   fixes k :: "'a \<Rightarrow> 'b::linordered_field"

   815   shows "f <o g =o O(k) \<Longrightarrow> g =o h +o O(k) \<Longrightarrow> f <o h =o O(k)"

   816   apply (unfold lesso_def)

   817   apply (drule set_plus_imp_minus)

   818   apply (drule bigo_abs5) back

   819   apply (simp add: fun_diff_def)

   820   apply (drule bigo_useful_add)

   821   apply assumption

   822   apply (erule bigo_lesseq2) back

   823   apply (rule allI)

   824   apply (auto simp add: func_plus fun_diff_def algebra_simps split: split_max abs_split)

   825   done

   826

   827 lemma bigo_lesso5: "f <o g =o O(h) \<Longrightarrow> \<exists>C. \<forall>x. f x \<le> g x + C * abs (h x)"

   828   apply (simp only: lesso_def bigo_alt_def)

   829   apply clarsimp

   830   apply (rule_tac x = c in exI)

   831   apply (rule allI)

   832   apply (drule_tac x = x in spec)

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

   834   apply (clarsimp simp add: algebra_simps)

   835   apply (rule abs_of_nonneg)

   836   apply (rule max.cobounded2)

   837   done

   838

   839 lemma lesso_add: "f <o g =o O(h) \<Longrightarrow> k <o l =o O(h) \<Longrightarrow> (f + k) <o (g + l) =o O(h)"

   840   apply (unfold lesso_def)

   841   apply (rule bigo_lesseq3)

   842   apply (erule bigo_useful_add)

   843   apply assumption

   844   apply (force split: split_max)

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

   846   done

   847

   848 lemma bigo_LIMSEQ1: "f =o O(g) \<Longrightarrow> g ----> 0 \<Longrightarrow> f ----> (0::real)"

   849   apply (simp add: LIMSEQ_iff bigo_alt_def)

   850   apply clarify

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

   852   apply (drule mp)

   853   apply simp

   854   apply clarify

   855   apply (rule_tac x = no in exI)

   856   apply (rule allI)

   857   apply (drule_tac x = n in spec)+

   858   apply (rule impI)

   859   apply (drule mp)

   860   apply assumption

   861   apply (rule order_le_less_trans)

   862   apply assumption

   863   apply (rule order_less_le_trans)

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

   865   apply assumption

   866   apply (erule mult_strict_left_mono)

   867   apply assumption

   868   apply simp

   869   done

   870

   871 lemma bigo_LIMSEQ2: "f =o g +o O(h) \<Longrightarrow> h ----> 0 \<Longrightarrow> f ----> a \<Longrightarrow> g ----> (a::real)"

   872   apply (drule set_plus_imp_minus)

   873   apply (drule bigo_LIMSEQ1)

   874   apply assumption

   875   apply (simp only: fun_diff_def)

   876   apply (erule LIMSEQ_diff_approach_zero2)

   877   apply assumption

   878   done

   879

   880 end
`