src/HOL/Library/BigO.thy
 author wenzelm Sat Mar 01 13:05:46 2014 +0100 (2014-03-01) changeset 55821 44055f07cbd8 parent 54863 82acc20ded73 child 56536 aefb4a8da31f permissions -rw-r--r--
more symbols, less parentheses;
     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 (rule mult_pos_pos)

    66   apply assumption+

    67   apply (rule allI)

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

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

    70   apply (erule order_trans)

    71   apply (simp add: mult_ac)

    72   apply (rule mult_left_mono, assumption)

    73   apply (rule order_less_imp_le, assumption)

    74   done

    75

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

    77   apply(auto simp add: bigo_def)

    78   apply(rule_tac x = 1 in exI)

    79   apply simp

    80   done

    81

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

    83   apply (auto simp add: bigo_def func_zero)

    84   apply (rule_tac x = 0 in exI)

    85   apply auto

    86   done

    87

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

    89   by (auto simp add: bigo_def)

    90

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

    92   apply (auto simp add: bigo_alt_def set_plus_def)

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

    94   apply auto

    95   apply (simp add: ring_distribs func_plus)

    96   apply (rule order_trans)

    97   apply (rule abs_triangle_ineq)

    98   apply (rule add_mono)

    99   apply force

   100   apply force

   101   done

   102

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

   104   apply (rule equalityI)

   105   apply (rule bigo_plus_self_subset)

   106   apply (rule set_zero_plus2)

   107   apply (rule bigo_zero)

   108   done

   109

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

   111   apply (rule subsetI)

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

   113   apply (subst bigo_pos_const [symmetric])+

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

   115   apply (rule conjI)

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

   117   apply (clarsimp)

   118   apply (auto)

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

   120   apply (erule_tac x = xa in allE)

   121   apply (erule order_trans)

   122   apply (simp)

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

   124   apply (erule order_trans)

   125   apply (simp add: ring_distribs)

   126   apply (rule mult_left_mono)

   127   apply (simp add: abs_triangle_ineq)

   128   apply (simp add: order_less_le)

   129   apply (rule mult_nonneg_nonneg)

   130   apply auto

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

   132   apply (rule conjI)

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

   134   apply auto

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

   136   apply (erule_tac x = xa in allE)

   137   apply (erule order_trans)

   138   apply simp

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

   140   apply (erule order_trans)

   141   apply (simp add: ring_distribs)

   142   apply (rule mult_left_mono)

   143   apply (rule abs_triangle_ineq)

   144   apply (simp add: order_less_le)

   145   apply (rule mult_nonneg_nonneg)

   146   apply (erule order_less_imp_le)

   147   apply simp

   148   done

   149

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

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

   152   apply (erule order_trans)

   153   apply simp

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

   155   done

   156

   157 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)"

   158   apply (rule equalityI)

   159   apply (rule bigo_plus_subset)

   160   apply (simp add: bigo_alt_def set_plus_def func_plus)

   161   apply clarify

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

   163   apply (rule conjI)

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

   165   apply (erule order_less_le_trans)

   166   apply assumption

   167   apply (rule max.cobounded1)

   168   apply clarify

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

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

   171   apply (simp add: ring_distribs)

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

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

   174   apply force

   175   apply (rule add_mono)

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

   177   apply force

   178   apply (rule mult_right_mono)

   179   apply (rule max.cobounded1)

   180   apply assumption

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

   182   apply force

   183   apply (rule mult_right_mono)

   184   apply (rule max.cobounded2)

   185   apply assumption

   186   apply (rule abs_triangle_ineq)

   187   apply (rule add_nonneg_nonneg)

   188   apply assumption+

   189   done

   190

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

   192   apply (auto simp add: bigo_def)

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

   194   apply auto

   195   apply (drule_tac x = x in spec)+

   196   apply (simp add: abs_mult [symmetric])

   197   done

   198

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

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

   201   apply simp

   202   done

   203

   204 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)"

   205   apply (rule set_minus_imp_plus)

   206   apply (rule bigo_bounded)

   207   apply (auto simp add: fun_Compl_def func_plus)

   208   apply (drule_tac x = x in spec)+

   209   apply force

   210   apply (drule_tac x = x in spec)+

   211   apply force

   212   done

   213

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

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

   222   apply (unfold bigo_def)

   223   apply auto

   224   apply (rule_tac x = 1 in exI)

   225   apply auto

   226   done

   227

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

   229   apply (rule equalityI)

   230   apply (rule bigo_elt_subset)

   231   apply (rule bigo_abs2)

   232   apply (rule bigo_elt_subset)

   233   apply (rule bigo_abs)

   234   done

   235

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

   237   apply (drule set_plus_imp_minus)

   238   apply (rule set_minus_imp_plus)

   239   apply (subst fun_diff_def)

   240 proof -

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

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

   243     by (rule bigo_abs2)

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

   245     apply (rule bigo_elt_subset)

   246     apply (rule bigo_bounded)

   247     apply force

   248     apply (rule allI)

   249     apply (rule abs_triangle_ineq3)

   250     done

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

   252     apply (rule bigo_elt_subset)

   253     apply (subst fun_diff_def)

   254     apply (rule bigo_abs)

   255     done

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

   257     by (rule bigo_elt_subset)

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

   259 qed

   260

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

   262   by (unfold bigo_def, auto)

   263

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

   265 proof -

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

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

   268     by (auto del: subsetI)

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

   270     apply (subst bigo_abs3 [symmetric])+

   271     apply (rule refl)

   272     done

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

   274     by (rule bigo_plus_eq [symmetric]) auto

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

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

   277     by (elim bigo_elt_subset)

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

   279     by (rule bigo_plus_eq, auto)

   280   finally show ?thesis

   281     by (simp add: bigo_abs3 [symmetric])

   282 qed

   283

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

   285   apply (rule subsetI)

   286   apply (subst bigo_def)

   287   apply (auto simp add: bigo_alt_def set_times_def func_times)

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

   289   apply (rule allI)

   290   apply (erule_tac x = x in allE)+

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

   292   apply (erule ssubst)

   293   apply (subst abs_mult)

   294   apply (rule mult_mono)

   295   apply assumption+

   296   apply (rule mult_nonneg_nonneg)

   297   apply auto

   298   apply (simp add: mult_ac abs_mult)

   299   done

   300

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

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

   303   apply (rule_tac x = c in exI)

   304   apply auto

   305   apply (drule_tac x = x in spec)

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

   307   apply (force simp add: mult_ac)

   308   apply (rule mult_left_mono, assumption)

   309   apply (rule abs_ge_zero)

   310   done

   311

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

   313   apply (rule subsetD)

   314   apply (rule bigo_mult)

   315   apply (erule set_times_intro, assumption)

   316   done

   317

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

   319   apply (drule set_plus_imp_minus)

   320   apply (rule set_minus_imp_plus)

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

   322   apply (auto simp add: algebra_simps)

   323   done

   324

   325 lemma bigo_mult5:

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

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

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

   329 proof

   330   fix h

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

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

   333     by auto

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

   335     by (rule bigo_mult2)

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

   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 have "(\<lambda>x. (1::'b) / f x) * h \<in> O(g)" .

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

   343     by auto

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

   345     apply (simp add: func_times)

   346     apply (rule ext)

   347     apply (simp add: assms nonzero_divide_eq_eq mult_ac)

   348     done

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

   350 qed

   351

   352 lemma bigo_mult6:

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

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

   355   apply (rule equalityI)

   356   apply (erule bigo_mult5)

   357   apply (rule bigo_mult2)

   358   done

   359

   360 lemma bigo_mult7:

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

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

   363   apply (subst bigo_mult6)

   364   apply assumption

   365   apply (rule set_times_mono3)

   366   apply (rule bigo_refl)

   367   done

   368

   369 lemma bigo_mult8:

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

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

   372   apply (rule equalityI)

   373   apply (erule bigo_mult7)

   374   apply (rule bigo_mult)

   375   done

   376

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

   378   by (auto simp add: bigo_def fun_Compl_def)

   379

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

   381   apply (rule set_minus_imp_plus)

   382   apply (drule set_plus_imp_minus)

   383   apply (drule bigo_minus)

   384   apply simp

   385   done

   386

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

   388   by (auto simp add: bigo_def fun_Compl_def)

   389

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

   391 proof -

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

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

   394   proof -

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

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

   397       by (auto del: subsetI)

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

   399     proof -

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

   401       thus ?thesis by (auto del: subsetI)

   402     qed

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

   404     finally show ?thesis .

   405   qed

   406 qed

   407

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

   409 proof -

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

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

   412   proof -

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

   414       by auto

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

   416       by (elim bigo_plus_absorb_lemma1)

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

   418       by auto

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

   420       by (simp add: set_plus_rearranges)

   421     finally show ?thesis .

   422   qed

   423 qed

   424

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

   426   apply (rule equalityI)

   427   apply (erule bigo_plus_absorb_lemma1)

   428   apply (erule bigo_plus_absorb_lemma2)

   429   done

   430

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

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

   433   apply force+

   434   done

   435

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

   437   apply (subst set_minus_plus [symmetric])

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

   439   apply (erule ssubst)

   440   apply (rule bigo_minus)

   441   apply (subst set_minus_plus)

   442   apply assumption

   443   apply (simp add: add_ac)

   444   done

   445

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

   447   apply (rule iffI)

   448   apply (erule bigo_add_commute_imp)+

   449   done

   450

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

   452   by (auto simp add: bigo_def mult_ac)

   453

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

   455   apply (rule bigo_elt_subset)

   456   apply (rule bigo_const1)

   457   done

   458

   459 lemma bigo_const3:

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

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

   462   apply (simp add: bigo_def)

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

   464   apply (simp add: abs_mult [symmetric])

   465   done

   466

   467 lemma bigo_const4:

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

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

   470   apply (rule bigo_elt_subset)

   471   apply (rule bigo_const3)

   472   apply assumption

   473   done

   474

   475 lemma bigo_const [simp]:

   476   fixes c :: "'a::linordered_field"

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

   478   apply (rule equalityI)

   479   apply (rule bigo_const2)

   480   apply (rule bigo_const4)

   481   apply assumption

   482   done

   483

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

   485   apply (simp add: bigo_def)

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

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

   488   done

   489

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

   491   apply (rule bigo_elt_subset)

   492   apply (rule bigo_const_mult1)

   493   done

   494

   495 lemma bigo_const_mult3:

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

   497   shows "c \<noteq> 0 \<Longrightarrow> f \<in> O(\<lambda>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:

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

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

   506   apply (rule bigo_elt_subset)

   507   apply (rule bigo_const_mult3)

   508   apply assumption

   509   done

   510

   511 lemma bigo_const_mult [simp]:

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

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

   514   apply (rule equalityI)

   515   apply (rule bigo_const_mult2)

   516   apply (erule bigo_const_mult4)

   517   done

   518

   519 lemma bigo_const_mult5 [simp]:

   520   fixes c :: "'a::linordered_field"

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

   522   apply (auto del: subsetI)

   523   apply (rule order_trans)

   524   apply (rule bigo_mult2)

   525   apply (simp add: func_times)

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

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

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

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

   530   apply (rule allI)

   531   apply (subst mult_assoc)

   532   apply (rule mult_left_mono)

   533   apply (erule spec)

   534   apply force

   535   done

   536

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

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

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

   540   apply (rule allI)

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

   542   apply (erule ssubst)

   543   apply (subst abs_mult)

   544   apply (rule mult_left_mono)

   545   apply (erule spec)

   546   apply simp

   547   apply(simp add: mult_ac)

   548   done

   549

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

   551 proof -

   552   assume "f =o O(g)"

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

   554     by auto

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

   556     by (simp add: func_times)

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

   558     by (auto del: subsetI)

   559   finally show ?thesis .

   560 qed

   561

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

   563   unfolding bigo_def by auto

   564

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

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

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

   568   apply (drule bigo_compose1)

   569   apply (simp add: fun_diff_def)

   570   done

   571

   572

   573 subsection {* Setsum *}

   574

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

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

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

   578   apply (auto simp add: bigo_def)

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

   580   apply (subst abs_of_nonneg) back back

   581   apply (rule setsum_nonneg)

   582   apply force

   583   apply (subst setsum_right_distrib)

   584   apply (rule allI)

   585   apply (rule order_trans)

   586   apply (rule setsum_abs)

   587   apply (rule setsum_mono)

   588   apply (rule order_trans)

   589   apply (drule spec)+

   590   apply (drule bspec)+

   591   apply assumption+

   592   apply (drule bspec)

   593   apply assumption+

   594   apply (rule mult_right_mono)

   595   apply (rule abs_ge_self)

   596   apply force

   597   done

   598

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

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

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

   602   apply (rule bigo_setsum_main)

   603   apply force

   604   apply clarsimp

   605   apply (rule_tac x = c in exI)

   606   apply force

   607   done

   608

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

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

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

   612   by (rule bigo_setsum1) auto

   613

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

   615     (\<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)))"

   616   apply (rule bigo_setsum1)

   617   apply (rule allI)+

   618   apply (rule abs_ge_zero)

   619   apply (unfold bigo_def)

   620   apply auto

   621   apply (rule_tac x = c in exI)

   622   apply (rule allI)+

   623   apply (subst abs_mult)+

   624   apply (subst mult_left_commute)

   625   apply (rule mult_left_mono)

   626   apply (erule spec)

   627   apply (rule abs_ge_zero)

   628   done

   629

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

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

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

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

   634   apply (rule set_minus_imp_plus)

   635   apply (subst fun_diff_def)

   636   apply (subst setsum_subtractf [symmetric])

   637   apply (subst right_diff_distrib [symmetric])

   638   apply (rule bigo_setsum3)

   639   apply (subst fun_diff_def [symmetric])

   640   apply (erule set_plus_imp_minus)

   641   done

   642

   643 lemma bigo_setsum5: "f =o O(h) \<Longrightarrow> \<forall>x y. 0 \<le> l x y \<Longrightarrow>

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

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

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

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

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

   649   apply (erule ssubst)

   650   apply (erule bigo_setsum3)

   651   apply (rule ext)

   652   apply (rule setsum_cong2)

   653   apply (subst abs_of_nonneg)

   654   apply (rule mult_nonneg_nonneg)

   655   apply auto

   656   done

   657

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

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

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

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

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

   663   apply (rule set_minus_imp_plus)

   664   apply (subst fun_diff_def)

   665   apply (subst setsum_subtractf [symmetric])

   666   apply (subst right_diff_distrib [symmetric])

   667   apply (rule bigo_setsum5)

   668   apply (subst fun_diff_def [symmetric])

   669   apply (drule set_plus_imp_minus)

   670   apply auto

   671   done

   672

   673

   674 subsection {* Misc useful stuff *}

   675

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

   677   apply (subst bigo_plus_idemp [symmetric])

   678   apply (rule set_plus_mono2)

   679   apply assumption+

   680   done

   681

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

   683   apply (subst bigo_plus_idemp [symmetric])

   684   apply (rule set_plus_intro)

   685   apply assumption+

   686   done

   687

   688 lemma bigo_useful_const_mult:

   689   fixes c :: "'a::linordered_field"

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

   691   apply (rule subsetD)

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

   693   apply assumption

   694   apply (rule bigo_const_mult6)

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

   696   apply (erule ssubst)

   697   apply (erule set_times_intro2)

   698   apply (simp add: func_times)

   699   done

   700

   701 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)"

   702   apply (simp add: bigo_alt_def)

   703   apply auto

   704   apply (rule_tac x = c in exI)

   705   apply auto

   706   apply (case_tac "x = 0")

   707   apply simp

   708   apply (rule mult_nonneg_nonneg)

   709   apply force

   710   apply force

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

   712   apply (erule ssubst) back

   713   apply (erule spec)

   714   apply simp

   715   done

   716

   717 lemma bigo_fix2:

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

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

   720   apply (rule set_minus_imp_plus)

   721   apply (rule bigo_fix)

   722   apply (subst fun_diff_def)

   723   apply (subst fun_diff_def [symmetric])

   724   apply (rule set_plus_imp_minus)

   725   apply simp

   726   apply (simp add: fun_diff_def)

   727   done

   728

   729

   730 subsection {* Less than or equal to *}

   731

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

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

   734

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

   736   apply (unfold bigo_def)

   737   apply clarsimp

   738   apply (rule_tac x = c in exI)

   739   apply (rule allI)

   740   apply (rule order_trans)

   741   apply (erule spec)+

   742   done

   743

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

   745   apply (erule bigo_lesseq1)

   746   apply (rule allI)

   747   apply (drule_tac x = x in spec)

   748   apply (rule order_trans)

   749   apply assumption

   750   apply (rule abs_ge_self)

   751   done

   752

   753 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)"

   754   apply (erule bigo_lesseq2)

   755   apply (rule allI)

   756   apply (subst abs_of_nonneg)

   757   apply (erule spec)+

   758   done

   759

   760 lemma bigo_lesseq4: "f =o O(h) \<Longrightarrow>

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

   762   apply (erule bigo_lesseq1)

   763   apply (rule allI)

   764   apply (subst abs_of_nonneg)

   765   apply (erule spec)+

   766   done

   767

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

   769   apply (unfold lesso_def)

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

   771   apply (erule ssubst)

   772   apply (rule bigo_zero)

   773   apply (unfold func_zero)

   774   apply (rule ext)

   775   apply (simp split: split_max)

   776   done

   777

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

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

   785   apply (rule allI)

   786   apply (subst fun_diff_def)

   787   apply (case_tac "0 \<le> 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_conv_add_uminus)+

   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) \<Longrightarrow>

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

   803   apply (unfold lesso_def)

   804   apply (rule bigo_lesseq4)

   805   apply (erule set_plus_imp_minus)

   806   apply (rule allI)

   807   apply (rule max.cobounded2)

   808   apply (rule allI)

   809   apply (subst fun_diff_def)

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

   811   apply simp

   812   apply (subst abs_of_nonneg)

   813   apply (drule_tac x = x in spec) back

   814   apply (simp add: algebra_simps)

   815   apply (subst diff_conv_add_uminus)+

   816   apply (rule add_left_mono)

   817   apply (rule le_imp_neg_le)

   818   apply (erule spec)

   819   apply (rule order_trans)

   820   prefer 2

   821   apply (rule abs_ge_zero)

   822   apply (simp add: algebra_simps)

   823   done

   824

   825 lemma bigo_lesso4:

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

   827   shows "f <o g =o O(k) \<Longrightarrow> g =o h +o O(k) \<Longrightarrow> 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 split: split_max abs_split)

   837   done

   838

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

   840   apply (simp only: lesso_def bigo_alt_def)

   841   apply clarsimp

   842   apply (rule_tac x = c in exI)

   843   apply (rule allI)

   844   apply (drule_tac x = x in spec)

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

   846   apply (clarsimp simp add: algebra_simps)

   847   apply (rule abs_of_nonneg)

   848   apply (rule max.cobounded2)

   849   done

   850

   851 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)"

   852   apply (unfold lesso_def)

   853   apply (rule bigo_lesseq3)

   854   apply (erule bigo_useful_add)

   855   apply assumption

   856   apply (force split: split_max)

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

   858   done

   859

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

   861   apply (simp add: LIMSEQ_iff bigo_alt_def)

   862   apply clarify

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

   864   apply (drule mp)

   865   apply (erule divide_pos_pos)

   866   apply assumption

   867   apply clarify

   868   apply (rule_tac x = no in exI)

   869   apply (rule allI)

   870   apply (drule_tac x = n in spec)+

   871   apply (rule impI)

   872   apply (drule mp)

   873   apply assumption

   874   apply (rule order_le_less_trans)

   875   apply assumption

   876   apply (rule order_less_le_trans)

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

   878   apply assumption

   879   apply (erule mult_strict_left_mono)

   880   apply assumption

   881   apply simp

   882   done

   883

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

   885   apply (drule set_plus_imp_minus)

   886   apply (drule bigo_LIMSEQ1)

   887   apply assumption

   888   apply (simp only: fun_diff_def)

   889   apply (erule LIMSEQ_diff_approach_zero2)

   890   apply assumption

   891   done

   892

   893 end
`