src/HOL/Library/BigO.thy
author wenzelm
Mon Dec 28 01:28:28 2015 +0100 (2015-12-28)
changeset 61945 1135b8de26c3
parent 61762 d50b993b4fb9
child 61969 e01015e49041
permissions -rw-r--r--
more symbols;
wenzelm@16932
     1
(*  Title:      HOL/Library/BigO.thy
avigad@16908
     2
    Authors:    Jeremy Avigad and Kevin Donnelly
avigad@16908
     3
*)
avigad@16908
     4
wenzelm@60500
     5
section \<open>Big O notation\<close>
avigad@16908
     6
avigad@16908
     7
theory BigO
haftmann@38622
     8
imports Complex_Main Function_Algebras Set_Algebras
avigad@16908
     9
begin
avigad@16908
    10
wenzelm@60500
    11
text \<open>
avigad@16908
    12
This library is designed to support asymptotic ``big O'' calculations,
wenzelm@17199
    13
i.e.~reasoning with expressions of the form $f = O(g)$ and $f = g +
wenzelm@17199
    14
O(h)$.  An earlier version of this library is described in detail in
wenzelm@58622
    15
@{cite "Avigad-Donnelly"}.
wenzelm@17199
    16
avigad@16908
    17
The main changes in this version are as follows:
avigad@16908
    18
\begin{itemize}
wenzelm@61585
    19
\item We have eliminated the \<open>O\<close> operator on sets. (Most uses of this seem
avigad@16908
    20
  to be inessential.)
wenzelm@61585
    21
\item We no longer use \<open>+\<close> as output syntax for \<open>+o\<close>
wenzelm@61585
    22
\item Lemmas involving \<open>sumr\<close> have been replaced by more general lemmas
wenzelm@61585
    23
  involving `\<open>setsum\<close>.
avigad@16908
    24
\item The library has been expanded, with e.g.~support for expressions of
wenzelm@61585
    25
  the form \<open>f < g + O(h)\<close>.
avigad@16908
    26
\end{itemize}
wenzelm@17199
    27
wenzelm@17199
    28
Note also since the Big O library includes rules that demonstrate set
wenzelm@17199
    29
inclusion, to use the automated reasoners effectively with the library
wenzelm@61585
    30
one should redeclare the theorem \<open>subsetI\<close> as an intro rule,
wenzelm@61585
    31
rather than as an \<open>intro!\<close> rule, for example, using
wenzelm@61585
    32
\isa{\isakeyword{declare}}~\<open>subsetI [del, intro]\<close>.
wenzelm@60500
    33
\<close>
avigad@16908
    34
wenzelm@60500
    35
subsection \<open>Definitions\<close>
avigad@16908
    36
wenzelm@55821
    37
definition bigo :: "('a \<Rightarrow> 'b::linordered_idom) \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(1O'(_'))")
wenzelm@61945
    38
  where "O(f:: 'a \<Rightarrow> 'b) = {h. \<exists>c. \<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>}"
avigad@16908
    39
wenzelm@55821
    40
lemma bigo_pos_const:
wenzelm@61945
    41
  "(\<exists>c::'a::linordered_idom. \<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>) \<longleftrightarrow>
wenzelm@61945
    42
    (\<exists>c. 0 < c \<and> (\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>))"
avigad@16908
    43
  apply auto
avigad@16908
    44
  apply (case_tac "c = 0")
avigad@16908
    45
  apply simp
avigad@16908
    46
  apply (rule_tac x = "1" in exI)
avigad@16908
    47
  apply simp
wenzelm@61945
    48
  apply (rule_tac x = "\<bar>c\<bar>" in exI)
avigad@16908
    49
  apply auto
wenzelm@61945
    50
  apply (subgoal_tac "c * \<bar>f x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>")
avigad@16908
    51
  apply (erule_tac x = x in allE)
avigad@16908
    52
  apply force
avigad@16908
    53
  apply (rule mult_right_mono)
avigad@16908
    54
  apply (rule abs_ge_self)
avigad@16908
    55
  apply (rule abs_ge_zero)
wenzelm@22665
    56
  done
avigad@16908
    57
wenzelm@61945
    58
lemma bigo_alt_def: "O(f) = {h. \<exists>c. 0 < c \<and> (\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>)}"
wenzelm@22665
    59
  by (auto simp add: bigo_def bigo_pos_const)
avigad@16908
    60
wenzelm@55821
    61
lemma bigo_elt_subset [intro]: "f \<in> O(g) \<Longrightarrow> O(f) \<le> O(g)"
avigad@16908
    62
  apply (auto simp add: bigo_alt_def)
avigad@16908
    63
  apply (rule_tac x = "ca * c" in exI)
avigad@16908
    64
  apply (rule conjI)
nipkow@56544
    65
  apply simp
avigad@16908
    66
  apply (rule allI)
avigad@16908
    67
  apply (drule_tac x = "xa" in spec)+
wenzelm@61945
    68
  apply (subgoal_tac "ca * \<bar>f xa\<bar> \<le> ca * (c * \<bar>g xa\<bar>)")
avigad@16908
    69
  apply (erule order_trans)
haftmann@57514
    70
  apply (simp add: ac_simps)
avigad@16908
    71
  apply (rule mult_left_mono, assumption)
avigad@16908
    72
  apply (rule order_less_imp_le, assumption)
wenzelm@22665
    73
  done
avigad@16908
    74
wenzelm@55821
    75
lemma bigo_refl [intro]: "f \<in> O(f)"
avigad@16908
    76
  apply(auto simp add: bigo_def)
avigad@16908
    77
  apply(rule_tac x = 1 in exI)
avigad@16908
    78
  apply simp
wenzelm@22665
    79
  done
avigad@16908
    80
wenzelm@55821
    81
lemma bigo_zero: "0 \<in> O(g)"
avigad@16908
    82
  apply (auto simp add: bigo_def func_zero)
avigad@16908
    83
  apply (rule_tac x = 0 in exI)
avigad@16908
    84
  apply auto
wenzelm@22665
    85
  done
avigad@16908
    86
wenzelm@55821
    87
lemma bigo_zero2: "O(\<lambda>x. 0) = {\<lambda>x. 0}"
wenzelm@55821
    88
  by (auto simp add: bigo_def)
avigad@16908
    89
wenzelm@55821
    90
lemma bigo_plus_self_subset [intro]: "O(f) + O(f) \<subseteq> O(f)"
berghofe@26814
    91
  apply (auto simp add: bigo_alt_def set_plus_def)
avigad@16908
    92
  apply (rule_tac x = "c + ca" in exI)
avigad@16908
    93
  apply auto
nipkow@23477
    94
  apply (simp add: ring_distribs func_plus)
avigad@16908
    95
  apply (rule order_trans)
avigad@16908
    96
  apply (rule abs_triangle_ineq)
avigad@16908
    97
  apply (rule add_mono)
avigad@16908
    98
  apply force
avigad@16908
    99
  apply force
wenzelm@55821
   100
  done
avigad@16908
   101
krauss@47445
   102
lemma bigo_plus_idemp [simp]: "O(f) + O(f) = O(f)"
avigad@16908
   103
  apply (rule equalityI)
avigad@16908
   104
  apply (rule bigo_plus_self_subset)
wenzelm@55821
   105
  apply (rule set_zero_plus2)
avigad@16908
   106
  apply (rule bigo_zero)
wenzelm@22665
   107
  done
avigad@16908
   108
wenzelm@55821
   109
lemma bigo_plus_subset [intro]: "O(f + g) \<subseteq> O(f) + O(g)"
avigad@16908
   110
  apply (rule subsetI)
berghofe@26814
   111
  apply (auto simp add: bigo_def bigo_pos_const func_plus set_plus_def)
avigad@16908
   112
  apply (subst bigo_pos_const [symmetric])+
wenzelm@61945
   113
  apply (rule_tac x = "\<lambda>n. if \<bar>g n\<bar> \<le> \<bar>f n\<bar> then x n else 0" in exI)
avigad@16908
   114
  apply (rule conjI)
avigad@16908
   115
  apply (rule_tac x = "c + c" in exI)
avigad@16908
   116
  apply (clarsimp)
wenzelm@61945
   117
  apply (subgoal_tac "c * \<bar>f xa + g xa\<bar> \<le> (c + c) * \<bar>f xa\<bar>")
avigad@16908
   118
  apply (erule_tac x = xa in allE)
avigad@16908
   119
  apply (erule order_trans)
avigad@16908
   120
  apply (simp)
wenzelm@61945
   121
  apply (subgoal_tac "c * \<bar>f xa + g xa\<bar> \<le> c * (\<bar>f xa\<bar> + \<bar>g xa\<bar>)")
avigad@16908
   122
  apply (erule order_trans)
nipkow@23477
   123
  apply (simp add: ring_distribs)
avigad@16908
   124
  apply (rule mult_left_mono)
avigad@16908
   125
  apply (simp add: abs_triangle_ineq)
avigad@16908
   126
  apply (simp add: order_less_le)
wenzelm@61945
   127
  apply (rule_tac x = "\<lambda>n. if \<bar>f n\<bar> < \<bar>g n\<bar> then x n else 0" in exI)
avigad@16908
   128
  apply (rule conjI)
avigad@16908
   129
  apply (rule_tac x = "c + c" in exI)
avigad@16908
   130
  apply auto
wenzelm@61945
   131
  apply (subgoal_tac "c * \<bar>f xa + g xa\<bar> \<le> (c + c) * \<bar>g xa\<bar>")
avigad@16908
   132
  apply (erule_tac x = xa in allE)
avigad@16908
   133
  apply (erule order_trans)
wenzelm@55821
   134
  apply simp
wenzelm@61945
   135
  apply (subgoal_tac "c * \<bar>f xa + g xa\<bar> \<le> c * (\<bar>f xa\<bar> + \<bar>g xa\<bar>)")
avigad@16908
   136
  apply (erule order_trans)
nipkow@23477
   137
  apply (simp add: ring_distribs)
avigad@16908
   138
  apply (rule mult_left_mono)
avigad@16908
   139
  apply (rule abs_triangle_ineq)
avigad@16908
   140
  apply (simp add: order_less_le)
wenzelm@22665
   141
  done
avigad@16908
   142
wenzelm@55821
   143
lemma bigo_plus_subset2 [intro]: "A \<subseteq> O(f) \<Longrightarrow> B \<subseteq> O(f) \<Longrightarrow> A + B \<subseteq> O(f)"
wenzelm@55821
   144
  apply (subgoal_tac "A + B \<subseteq> O(f) + O(f)")
avigad@16908
   145
  apply (erule order_trans)
avigad@16908
   146
  apply simp
avigad@16908
   147
  apply (auto del: subsetI simp del: bigo_plus_idemp)
wenzelm@22665
   148
  done
avigad@16908
   149
wenzelm@55821
   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)"
avigad@16908
   151
  apply (rule equalityI)
avigad@16908
   152
  apply (rule bigo_plus_subset)
berghofe@26814
   153
  apply (simp add: bigo_alt_def set_plus_def func_plus)
avigad@16908
   154
  apply clarify
avigad@16908
   155
  apply (rule_tac x = "max c ca" in exI)
avigad@16908
   156
  apply (rule conjI)
wenzelm@55821
   157
  apply (subgoal_tac "c \<le> max c ca")
avigad@16908
   158
  apply (erule order_less_le_trans)
avigad@16908
   159
  apply assumption
haftmann@54863
   160
  apply (rule max.cobounded1)
avigad@16908
   161
  apply clarify
avigad@16908
   162
  apply (drule_tac x = "xa" in spec)+
wenzelm@55821
   163
  apply (subgoal_tac "0 \<le> f xa + g xa")
nipkow@23477
   164
  apply (simp add: ring_distribs)
wenzelm@61945
   165
  apply (subgoal_tac "\<bar>a xa + b xa\<bar> \<le> \<bar>a xa\<bar> + \<bar>b xa\<bar>")
wenzelm@61945
   166
  apply (subgoal_tac "\<bar>a xa\<bar> + \<bar>b xa\<bar> \<le> max c ca * f xa + max c ca * g xa")
wenzelm@55821
   167
  apply force
avigad@16908
   168
  apply (rule add_mono)
wenzelm@55821
   169
  apply (subgoal_tac "c * f xa \<le> max c ca * f xa")
wenzelm@55821
   170
  apply force
avigad@16908
   171
  apply (rule mult_right_mono)
haftmann@54863
   172
  apply (rule max.cobounded1)
avigad@16908
   173
  apply assumption
wenzelm@55821
   174
  apply (subgoal_tac "ca * g xa \<le> max c ca * g xa")
wenzelm@55821
   175
  apply force
avigad@16908
   176
  apply (rule mult_right_mono)
haftmann@54863
   177
  apply (rule max.cobounded2)
avigad@16908
   178
  apply assumption
avigad@16908
   179
  apply (rule abs_triangle_ineq)
avigad@16908
   180
  apply (rule add_nonneg_nonneg)
avigad@16908
   181
  apply assumption+
wenzelm@22665
   182
  done
avigad@16908
   183
wenzelm@55821
   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)"
avigad@16908
   185
  apply (auto simp add: bigo_def)
wenzelm@61945
   186
  apply (rule_tac x = "\<bar>c\<bar>" in exI)
avigad@16908
   187
  apply auto
avigad@16908
   188
  apply (drule_tac x = x in spec)+
avigad@16908
   189
  apply (simp add: abs_mult [symmetric])
wenzelm@22665
   190
  done
avigad@16908
   191
wenzelm@55821
   192
lemma bigo_bounded: "\<forall>x. 0 \<le> f x \<Longrightarrow> \<forall>x. f x \<le> g x \<Longrightarrow> f \<in> O(g)"
avigad@16908
   193
  apply (erule bigo_bounded_alt [of f 1 g])
avigad@16908
   194
  apply simp
wenzelm@22665
   195
  done
avigad@16908
   196
wenzelm@55821
   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)"
avigad@16908
   198
  apply (rule set_minus_imp_plus)
avigad@16908
   199
  apply (rule bigo_bounded)
haftmann@54230
   200
  apply (auto simp add: fun_Compl_def func_plus)
avigad@16908
   201
  apply (drule_tac x = x in spec)+
avigad@16908
   202
  apply force
wenzelm@22665
   203
  done
avigad@16908
   204
wenzelm@61945
   205
lemma bigo_abs: "(\<lambda>x. \<bar>f x\<bar>) =o O(f)"
avigad@16908
   206
  apply (unfold bigo_def)
avigad@16908
   207
  apply auto
avigad@16908
   208
  apply (rule_tac x = 1 in exI)
avigad@16908
   209
  apply auto
wenzelm@22665
   210
  done
avigad@16908
   211
wenzelm@61945
   212
lemma bigo_abs2: "f =o O(\<lambda>x. \<bar>f x\<bar>)"
avigad@16908
   213
  apply (unfold bigo_def)
avigad@16908
   214
  apply auto
avigad@16908
   215
  apply (rule_tac x = 1 in exI)
avigad@16908
   216
  apply auto
wenzelm@22665
   217
  done
avigad@16908
   218
wenzelm@61945
   219
lemma bigo_abs3: "O(f) = O(\<lambda>x. \<bar>f x\<bar>)"
avigad@16908
   220
  apply (rule equalityI)
avigad@16908
   221
  apply (rule bigo_elt_subset)
avigad@16908
   222
  apply (rule bigo_abs2)
avigad@16908
   223
  apply (rule bigo_elt_subset)
avigad@16908
   224
  apply (rule bigo_abs)
wenzelm@22665
   225
  done
avigad@16908
   226
wenzelm@61945
   227
lemma bigo_abs4: "f =o g +o O(h) \<Longrightarrow> (\<lambda>x. \<bar>f x\<bar>) =o (\<lambda>x. \<bar>g x\<bar>) +o O(h)"
avigad@16908
   228
  apply (drule set_plus_imp_minus)
avigad@16908
   229
  apply (rule set_minus_imp_plus)
berghofe@26814
   230
  apply (subst fun_diff_def)
avigad@16908
   231
proof -
wenzelm@55821
   232
  assume a: "f - g \<in> O(h)"
wenzelm@61945
   233
  have "(\<lambda>x. \<bar>f x\<bar> - \<bar>g x\<bar>) =o O(\<lambda>x. \<bar>\<bar>f x\<bar> - \<bar>g x\<bar>\<bar>)"
avigad@16908
   234
    by (rule bigo_abs2)
wenzelm@61945
   235
  also have "\<dots> \<subseteq> O(\<lambda>x. \<bar>f x - g x\<bar>)"
avigad@16908
   236
    apply (rule bigo_elt_subset)
avigad@16908
   237
    apply (rule bigo_bounded)
avigad@16908
   238
    apply force
avigad@16908
   239
    apply (rule allI)
avigad@16908
   240
    apply (rule abs_triangle_ineq3)
avigad@16908
   241
    done
wenzelm@55821
   242
  also have "\<dots> \<subseteq> O(f - g)"
avigad@16908
   243
    apply (rule bigo_elt_subset)
berghofe@26814
   244
    apply (subst fun_diff_def)
avigad@16908
   245
    apply (rule bigo_abs)
avigad@16908
   246
    done
wenzelm@55821
   247
  also from a have "\<dots> \<subseteq> O(h)"
avigad@16908
   248
    by (rule bigo_elt_subset)
wenzelm@61945
   249
  finally show "(\<lambda>x. \<bar>f x\<bar> - \<bar>g x\<bar>) \<in> O(h)".
avigad@16908
   250
qed
avigad@16908
   251
wenzelm@61945
   252
lemma bigo_abs5: "f =o O(g) \<Longrightarrow> (\<lambda>x. \<bar>f x\<bar>) =o O(g)"
wenzelm@22665
   253
  by (unfold bigo_def, auto)
avigad@16908
   254
wenzelm@55821
   255
lemma bigo_elt_subset2 [intro]: "f \<in> g +o O(h) \<Longrightarrow> O(f) \<subseteq> O(g) + O(h)"
avigad@16908
   256
proof -
wenzelm@55821
   257
  assume "f \<in> g +o O(h)"
wenzelm@55821
   258
  also have "\<dots> \<subseteq> O(g) + O(h)"
avigad@16908
   259
    by (auto del: subsetI)
wenzelm@61945
   260
  also have "\<dots> = O(\<lambda>x. \<bar>g x\<bar>) + O(\<lambda>x. \<bar>h x\<bar>)"
avigad@16908
   261
    apply (subst bigo_abs3 [symmetric])+
avigad@16908
   262
    apply (rule refl)
avigad@16908
   263
    done
wenzelm@61945
   264
  also have "\<dots> = O((\<lambda>x. \<bar>g x\<bar>) + (\<lambda>x. \<bar>h x\<bar>))"
wenzelm@55821
   265
    by (rule bigo_plus_eq [symmetric]) auto
wenzelm@55821
   266
  finally have "f \<in> \<dots>" .
wenzelm@55821
   267
  then have "O(f) \<subseteq> \<dots>"
avigad@16908
   268
    by (elim bigo_elt_subset)
wenzelm@61945
   269
  also have "\<dots> = O(\<lambda>x. \<bar>g x\<bar>) + O(\<lambda>x. \<bar>h x\<bar>)"
avigad@16908
   270
    by (rule bigo_plus_eq, auto)
avigad@16908
   271
  finally show ?thesis
avigad@16908
   272
    by (simp add: bigo_abs3 [symmetric])
avigad@16908
   273
qed
avigad@16908
   274
wenzelm@55821
   275
lemma bigo_mult [intro]: "O(f)*O(g) \<subseteq> O(f * g)"
avigad@16908
   276
  apply (rule subsetI)
avigad@16908
   277
  apply (subst bigo_def)
berghofe@26814
   278
  apply (auto simp add: bigo_alt_def set_times_def func_times)
avigad@16908
   279
  apply (rule_tac x = "c * ca" in exI)
wenzelm@55821
   280
  apply (rule allI)
wenzelm@55821
   281
  apply (erule_tac x = x in allE)+
wenzelm@61945
   282
  apply (subgoal_tac "c * ca * \<bar>f x * g x\<bar> = (c * \<bar>f x\<bar>) * (ca * \<bar>g x\<bar>)")
wenzelm@55821
   283
  apply (erule ssubst)
avigad@16908
   284
  apply (subst abs_mult)
avigad@16908
   285
  apply (rule mult_mono)
avigad@16908
   286
  apply assumption+
avigad@16908
   287
  apply auto
haftmann@57514
   288
  apply (simp add: ac_simps abs_mult)
wenzelm@22665
   289
  done
avigad@16908
   290
wenzelm@55821
   291
lemma bigo_mult2 [intro]: "f *o O(g) \<subseteq> O(f * g)"
avigad@16908
   292
  apply (auto simp add: bigo_def elt_set_times_def func_times abs_mult)
avigad@16908
   293
  apply (rule_tac x = c in exI)
avigad@16908
   294
  apply auto
avigad@16908
   295
  apply (drule_tac x = x in spec)
wenzelm@61945
   296
  apply (subgoal_tac "\<bar>f x\<bar> * \<bar>b x\<bar> \<le> \<bar>f x\<bar> * (c * \<bar>g x\<bar>)")
haftmann@57514
   297
  apply (force simp add: ac_simps)
avigad@16908
   298
  apply (rule mult_left_mono, assumption)
avigad@16908
   299
  apply (rule abs_ge_zero)
wenzelm@22665
   300
  done
avigad@16908
   301
wenzelm@55821
   302
lemma bigo_mult3: "f \<in> O(h) \<Longrightarrow> g \<in> O(j) \<Longrightarrow> f * g \<in> O(h * j)"
avigad@16908
   303
  apply (rule subsetD)
avigad@16908
   304
  apply (rule bigo_mult)
avigad@16908
   305
  apply (erule set_times_intro, assumption)
wenzelm@22665
   306
  done
avigad@16908
   307
wenzelm@55821
   308
lemma bigo_mult4 [intro]: "f \<in> k +o O(h) \<Longrightarrow> g * f \<in> (g * k) +o O(g * h)"
avigad@16908
   309
  apply (drule set_plus_imp_minus)
avigad@16908
   310
  apply (rule set_minus_imp_plus)
avigad@16908
   311
  apply (drule bigo_mult3 [where g = g and j = g])
nipkow@29667
   312
  apply (auto simp add: algebra_simps)
wenzelm@22665
   313
  done
avigad@16908
   314
wenzelm@41528
   315
lemma bigo_mult5:
wenzelm@55821
   316
  fixes f :: "'a \<Rightarrow> 'b::linordered_field"
wenzelm@55821
   317
  assumes "\<forall>x. f x \<noteq> 0"
wenzelm@55821
   318
  shows "O(f * g) \<subseteq> f *o O(g)"
wenzelm@41528
   319
proof
wenzelm@41528
   320
  fix h
wenzelm@55821
   321
  assume "h \<in> O(f * g)"
wenzelm@55821
   322
  then have "(\<lambda>x. 1 / (f x)) * h \<in> (\<lambda>x. 1 / f x) *o O(f * g)"
wenzelm@41528
   323
    by auto
wenzelm@55821
   324
  also have "\<dots> \<subseteq> O((\<lambda>x. 1 / f x) * (f * g))"
wenzelm@41528
   325
    by (rule bigo_mult2)
wenzelm@55821
   326
  also have "(\<lambda>x. 1 / f x) * (f * g) = g"
wenzelm@55821
   327
    apply (simp add: func_times)
wenzelm@41528
   328
    apply (rule ext)
haftmann@57514
   329
    apply (simp add: assms nonzero_divide_eq_eq ac_simps)
wenzelm@41528
   330
    done
wenzelm@55821
   331
  finally have "(\<lambda>x. (1::'b) / f x) * h \<in> O(g)" .
wenzelm@55821
   332
  then have "f * ((\<lambda>x. (1::'b) / f x) * h) \<in> f *o O(g)"
wenzelm@41528
   333
    by auto
wenzelm@55821
   334
  also have "f * ((\<lambda>x. (1::'b) / f x) * h) = h"
wenzelm@55821
   335
    apply (simp add: func_times)
wenzelm@41528
   336
    apply (rule ext)
haftmann@57514
   337
    apply (simp add: assms nonzero_divide_eq_eq ac_simps)
wenzelm@41528
   338
    done
wenzelm@55821
   339
  finally show "h \<in> f *o O(g)" .
avigad@16908
   340
qed
avigad@16908
   341
wenzelm@55821
   342
lemma bigo_mult6:
wenzelm@55821
   343
  fixes f :: "'a \<Rightarrow> 'b::linordered_field"
wenzelm@55821
   344
  shows "\<forall>x. f x \<noteq> 0 \<Longrightarrow> O(f * g) = f *o O(g)"
avigad@16908
   345
  apply (rule equalityI)
avigad@16908
   346
  apply (erule bigo_mult5)
avigad@16908
   347
  apply (rule bigo_mult2)
wenzelm@22665
   348
  done
avigad@16908
   349
wenzelm@55821
   350
lemma bigo_mult7:
wenzelm@55821
   351
  fixes f :: "'a \<Rightarrow> 'b::linordered_field"
wenzelm@55821
   352
  shows "\<forall>x. f x \<noteq> 0 \<Longrightarrow> O(f * g) \<subseteq> O(f) * O(g)"
avigad@16908
   353
  apply (subst bigo_mult6)
avigad@16908
   354
  apply assumption
avigad@16908
   355
  apply (rule set_times_mono3)
avigad@16908
   356
  apply (rule bigo_refl)
wenzelm@22665
   357
  done
avigad@16908
   358
wenzelm@55821
   359
lemma bigo_mult8:
wenzelm@55821
   360
  fixes f :: "'a \<Rightarrow> 'b::linordered_field"
wenzelm@55821
   361
  shows "\<forall>x. f x \<noteq> 0 \<Longrightarrow> O(f * g) = O(f) * O(g)"
avigad@16908
   362
  apply (rule equalityI)
avigad@16908
   363
  apply (erule bigo_mult7)
avigad@16908
   364
  apply (rule bigo_mult)
wenzelm@22665
   365
  done
avigad@16908
   366
wenzelm@55821
   367
lemma bigo_minus [intro]: "f \<in> O(g) \<Longrightarrow> - f \<in> O(g)"
berghofe@26814
   368
  by (auto simp add: bigo_def fun_Compl_def)
avigad@16908
   369
wenzelm@55821
   370
lemma bigo_minus2: "f \<in> g +o O(h) \<Longrightarrow> - f \<in> -g +o O(h)"
avigad@16908
   371
  apply (rule set_minus_imp_plus)
avigad@16908
   372
  apply (drule set_plus_imp_minus)
avigad@16908
   373
  apply (drule bigo_minus)
haftmann@54230
   374
  apply simp
wenzelm@22665
   375
  done
avigad@16908
   376
wenzelm@55821
   377
lemma bigo_minus3: "O(- f) = O(f)"
wenzelm@41528
   378
  by (auto simp add: bigo_def fun_Compl_def)
avigad@16908
   379
wenzelm@55821
   380
lemma bigo_plus_absorb_lemma1: "f \<in> O(g) \<Longrightarrow> f +o O(g) \<subseteq> O(g)"
avigad@16908
   381
proof -
wenzelm@55821
   382
  assume a: "f \<in> O(g)"
wenzelm@55821
   383
  show "f +o O(g) \<subseteq> O(g)"
avigad@16908
   384
  proof -
wenzelm@55821
   385
    have "f \<in> O(f)" by auto
wenzelm@55821
   386
    then have "f +o O(g) \<subseteq> O(f) + O(g)"
avigad@16908
   387
      by (auto del: subsetI)
wenzelm@55821
   388
    also have "\<dots> \<subseteq> O(g) + O(g)"
avigad@16908
   389
    proof -
wenzelm@55821
   390
      from a have "O(f) \<subseteq> O(g)" by (auto del: subsetI)
wenzelm@56796
   391
      then show ?thesis by (auto del: subsetI)
avigad@16908
   392
    qed
wenzelm@55821
   393
    also have "\<dots> \<subseteq> O(g)" by simp
avigad@16908
   394
    finally show ?thesis .
avigad@16908
   395
  qed
avigad@16908
   396
qed
avigad@16908
   397
wenzelm@55821
   398
lemma bigo_plus_absorb_lemma2: "f \<in> O(g) \<Longrightarrow> O(g) \<subseteq> f +o O(g)"
avigad@16908
   399
proof -
wenzelm@55821
   400
  assume a: "f \<in> O(g)"
wenzelm@55821
   401
  show "O(g) \<subseteq> f +o O(g)"
avigad@16908
   402
  proof -
wenzelm@55821
   403
    from a have "- f \<in> O(g)"
wenzelm@55821
   404
      by auto
wenzelm@55821
   405
    then have "- f +o O(g) \<subseteq> O(g)"
wenzelm@55821
   406
      by (elim bigo_plus_absorb_lemma1)
wenzelm@55821
   407
    then have "f +o (- f +o O(g)) \<subseteq> f +o O(g)"
wenzelm@55821
   408
      by auto
wenzelm@55821
   409
    also have "f +o (- f +o O(g)) = O(g)"
avigad@16908
   410
      by (simp add: set_plus_rearranges)
avigad@16908
   411
    finally show ?thesis .
avigad@16908
   412
  qed
avigad@16908
   413
qed
avigad@16908
   414
wenzelm@55821
   415
lemma bigo_plus_absorb [simp]: "f \<in> O(g) \<Longrightarrow> f +o O(g) = O(g)"
avigad@16908
   416
  apply (rule equalityI)
avigad@16908
   417
  apply (erule bigo_plus_absorb_lemma1)
avigad@16908
   418
  apply (erule bigo_plus_absorb_lemma2)
wenzelm@22665
   419
  done
avigad@16908
   420
wenzelm@55821
   421
lemma bigo_plus_absorb2 [intro]: "f \<in> O(g) \<Longrightarrow> A \<subseteq> O(g) \<Longrightarrow> f +o A \<subseteq> O(g)"
wenzelm@55821
   422
  apply (subgoal_tac "f +o A \<subseteq> f +o O(g)")
avigad@16908
   423
  apply force+
wenzelm@22665
   424
  done
avigad@16908
   425
wenzelm@55821
   426
lemma bigo_add_commute_imp: "f \<in> g +o O(h) \<Longrightarrow> g \<in> f +o O(h)"
avigad@16908
   427
  apply (subst set_minus_plus [symmetric])
avigad@16908
   428
  apply (subgoal_tac "g - f = - (f - g)")
avigad@16908
   429
  apply (erule ssubst)
avigad@16908
   430
  apply (rule bigo_minus)
avigad@16908
   431
  apply (subst set_minus_plus)
avigad@16908
   432
  apply assumption
haftmann@57514
   433
  apply (simp add: ac_simps)
wenzelm@22665
   434
  done
avigad@16908
   435
wenzelm@55821
   436
lemma bigo_add_commute: "f \<in> g +o O(h) \<longleftrightarrow> g \<in> f +o O(h)"
avigad@16908
   437
  apply (rule iffI)
avigad@16908
   438
  apply (erule bigo_add_commute_imp)+
wenzelm@22665
   439
  done
avigad@16908
   440
wenzelm@55821
   441
lemma bigo_const1: "(\<lambda>x. c) \<in> O(\<lambda>x. 1)"
haftmann@57514
   442
  by (auto simp add: bigo_def ac_simps)
avigad@16908
   443
wenzelm@55821
   444
lemma bigo_const2 [intro]: "O(\<lambda>x. c) \<subseteq> O(\<lambda>x. 1)"
avigad@16908
   445
  apply (rule bigo_elt_subset)
avigad@16908
   446
  apply (rule bigo_const1)
wenzelm@22665
   447
  done
avigad@16908
   448
wenzelm@55821
   449
lemma bigo_const3:
wenzelm@55821
   450
  fixes c :: "'a::linordered_field"
wenzelm@55821
   451
  shows "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. 1) \<in> O(\<lambda>x. c)"
avigad@16908
   452
  apply (simp add: bigo_def)
wenzelm@61945
   453
  apply (rule_tac x = "\<bar>inverse c\<bar>" in exI)
avigad@16908
   454
  apply (simp add: abs_mult [symmetric])
wenzelm@22665
   455
  done
avigad@16908
   456
wenzelm@55821
   457
lemma bigo_const4:
wenzelm@55821
   458
  fixes c :: "'a::linordered_field"
wenzelm@55821
   459
  shows "c \<noteq> 0 \<Longrightarrow> O(\<lambda>x. 1) \<subseteq> O(\<lambda>x. c)"
wenzelm@55821
   460
  apply (rule bigo_elt_subset)
wenzelm@55821
   461
  apply (rule bigo_const3)
wenzelm@55821
   462
  apply assumption
wenzelm@55821
   463
  done
avigad@16908
   464
wenzelm@55821
   465
lemma bigo_const [simp]:
wenzelm@55821
   466
  fixes c :: "'a::linordered_field"
wenzelm@55821
   467
  shows "c \<noteq> 0 \<Longrightarrow> O(\<lambda>x. c) = O(\<lambda>x. 1)"
wenzelm@55821
   468
  apply (rule equalityI)
wenzelm@55821
   469
  apply (rule bigo_const2)
wenzelm@55821
   470
  apply (rule bigo_const4)
wenzelm@55821
   471
  apply assumption
wenzelm@55821
   472
  done
avigad@16908
   473
wenzelm@55821
   474
lemma bigo_const_mult1: "(\<lambda>x. c * f x) \<in> O(f)"
avigad@16908
   475
  apply (simp add: bigo_def)
wenzelm@61945
   476
  apply (rule_tac x = "\<bar>c\<bar>" in exI)
avigad@16908
   477
  apply (auto simp add: abs_mult [symmetric])
wenzelm@22665
   478
  done
avigad@16908
   479
wenzelm@55821
   480
lemma bigo_const_mult2: "O(\<lambda>x. c * f x) \<subseteq> O(f)"
wenzelm@55821
   481
  apply (rule bigo_elt_subset)
wenzelm@55821
   482
  apply (rule bigo_const_mult1)
wenzelm@55821
   483
  done
avigad@16908
   484
wenzelm@55821
   485
lemma bigo_const_mult3:
wenzelm@55821
   486
  fixes c :: "'a::linordered_field"
wenzelm@55821
   487
  shows "c \<noteq> 0 \<Longrightarrow> f \<in> O(\<lambda>x. c * f x)"
avigad@16908
   488
  apply (simp add: bigo_def)
wenzelm@61945
   489
  apply (rule_tac x = "\<bar>inverse c\<bar>" in exI)
haftmann@59867
   490
  apply (simp add: abs_mult mult.assoc [symmetric])
wenzelm@22665
   491
  done
avigad@16908
   492
wenzelm@55821
   493
lemma bigo_const_mult4:
wenzelm@55821
   494
  fixes c :: "'a::linordered_field"
wenzelm@55821
   495
  shows "c \<noteq> 0 \<Longrightarrow> O(f) \<subseteq> O(\<lambda>x. c * f x)"
wenzelm@55821
   496
  apply (rule bigo_elt_subset)
wenzelm@55821
   497
  apply (rule bigo_const_mult3)
wenzelm@55821
   498
  apply assumption
wenzelm@55821
   499
  done
avigad@16908
   500
wenzelm@55821
   501
lemma bigo_const_mult [simp]:
wenzelm@55821
   502
  fixes c :: "'a::linordered_field"
wenzelm@55821
   503
  shows "c \<noteq> 0 \<Longrightarrow> O(\<lambda>x. c * f x) = O(f)"
wenzelm@55821
   504
  apply (rule equalityI)
wenzelm@55821
   505
  apply (rule bigo_const_mult2)
wenzelm@55821
   506
  apply (erule bigo_const_mult4)
wenzelm@55821
   507
  done
avigad@16908
   508
wenzelm@55821
   509
lemma bigo_const_mult5 [simp]:
wenzelm@55821
   510
  fixes c :: "'a::linordered_field"
wenzelm@55821
   511
  shows "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. c) *o O(f) = O(f)"
avigad@16908
   512
  apply (auto del: subsetI)
avigad@16908
   513
  apply (rule order_trans)
avigad@16908
   514
  apply (rule bigo_mult2)
avigad@16908
   515
  apply (simp add: func_times)
wenzelm@41528
   516
  apply (auto intro!: simp add: bigo_def elt_set_times_def func_times)
wenzelm@55821
   517
  apply (rule_tac x = "\<lambda>y. inverse c * x y" in exI)
haftmann@57512
   518
  apply (simp add: mult.assoc [symmetric] abs_mult)
wenzelm@61945
   519
  apply (rule_tac x = "\<bar>inverse c\<bar> * ca" in exI)
haftmann@59867
   520
  apply auto
wenzelm@22665
   521
  done
avigad@16908
   522
wenzelm@55821
   523
lemma bigo_const_mult6 [intro]: "(\<lambda>x. c) *o O(f) \<subseteq> O(f)"
wenzelm@41528
   524
  apply (auto intro!: simp add: bigo_def elt_set_times_def func_times)
wenzelm@61945
   525
  apply (rule_tac x = "ca * \<bar>c\<bar>" in exI)
avigad@16908
   526
  apply (rule allI)
wenzelm@61945
   527
  apply (subgoal_tac "ca * \<bar>c\<bar> * \<bar>f x\<bar> = \<bar>c\<bar> * (ca * \<bar>f x\<bar>)")
avigad@16908
   528
  apply (erule ssubst)
avigad@16908
   529
  apply (subst abs_mult)
avigad@16908
   530
  apply (rule mult_left_mono)
avigad@16908
   531
  apply (erule spec)
avigad@16908
   532
  apply simp
haftmann@57514
   533
  apply(simp add: ac_simps)
wenzelm@22665
   534
  done
avigad@16908
   535
wenzelm@55821
   536
lemma bigo_const_mult7 [intro]: "f =o O(g) \<Longrightarrow> (\<lambda>x. c * f x) =o O(g)"
avigad@16908
   537
proof -
avigad@16908
   538
  assume "f =o O(g)"
wenzelm@55821
   539
  then have "(\<lambda>x. c) * f =o (\<lambda>x. c) *o O(g)"
avigad@16908
   540
    by auto
wenzelm@55821
   541
  also have "(\<lambda>x. c) * f = (\<lambda>x. c * f x)"
avigad@16908
   542
    by (simp add: func_times)
wenzelm@55821
   543
  also have "(\<lambda>x. c) *o O(g) \<subseteq> O(g)"
avigad@16908
   544
    by (auto del: subsetI)
avigad@16908
   545
  finally show ?thesis .
avigad@16908
   546
qed
avigad@16908
   547
wenzelm@55821
   548
lemma bigo_compose1: "f =o O(g) \<Longrightarrow> (\<lambda>x. f (k x)) =o O(\<lambda>x. g (k x))"
wenzelm@55821
   549
  unfolding bigo_def by auto
avigad@16908
   550
wenzelm@55821
   551
lemma bigo_compose2: "f =o g +o O(h) \<Longrightarrow>
wenzelm@55821
   552
    (\<lambda>x. f (k x)) =o (\<lambda>x. g (k x)) +o O(\<lambda>x. h(k x))"
haftmann@54230
   553
  apply (simp only: set_minus_plus [symmetric] fun_Compl_def func_plus)
wenzelm@55821
   554
  apply (drule bigo_compose1)
wenzelm@55821
   555
  apply (simp add: fun_diff_def)
haftmann@54230
   556
  done
avigad@16908
   557
wenzelm@22665
   558
wenzelm@60500
   559
subsection \<open>Setsum\<close>
avigad@16908
   560
wenzelm@55821
   561
lemma bigo_setsum_main: "\<forall>x. \<forall>y \<in> A x. 0 \<le> h x y \<Longrightarrow>
wenzelm@61945
   562
    \<exists>c. \<forall>x. \<forall>y \<in> A x. \<bar>f x y\<bar> \<le> c * h x y \<Longrightarrow>
wenzelm@55821
   563
      (\<lambda>x. \<Sum>y \<in> A x. f x y) =o O(\<lambda>x. \<Sum>y \<in> A x. h x y)"
avigad@16908
   564
  apply (auto simp add: bigo_def)
wenzelm@61945
   565
  apply (rule_tac x = "\<bar>c\<bar>" in exI)
wenzelm@17199
   566
  apply (subst abs_of_nonneg) back back
avigad@16908
   567
  apply (rule setsum_nonneg)
avigad@16908
   568
  apply force
ballarin@19279
   569
  apply (subst setsum_right_distrib)
avigad@16908
   570
  apply (rule allI)
avigad@16908
   571
  apply (rule order_trans)
avigad@16908
   572
  apply (rule setsum_abs)
avigad@16908
   573
  apply (rule setsum_mono)
avigad@16908
   574
  apply (rule order_trans)
avigad@16908
   575
  apply (drule spec)+
avigad@16908
   576
  apply (drule bspec)+
avigad@16908
   577
  apply assumption+
avigad@16908
   578
  apply (drule bspec)
avigad@16908
   579
  apply assumption+
wenzelm@55821
   580
  apply (rule mult_right_mono)
avigad@16908
   581
  apply (rule abs_ge_self)
avigad@16908
   582
  apply force
wenzelm@22665
   583
  done
avigad@16908
   584
wenzelm@55821
   585
lemma bigo_setsum1: "\<forall>x y. 0 \<le> h x y \<Longrightarrow>
wenzelm@61945
   586
    \<exists>c. \<forall>x y. \<bar>f x y\<bar> \<le> c * h x y \<Longrightarrow>
wenzelm@55821
   587
      (\<lambda>x. \<Sum>y \<in> A x. f x y) =o O(\<lambda>x. \<Sum>y \<in> A x. h x y)"
avigad@16908
   588
  apply (rule bigo_setsum_main)
avigad@16908
   589
  apply force
avigad@16908
   590
  apply clarsimp
avigad@16908
   591
  apply (rule_tac x = c in exI)
avigad@16908
   592
  apply force
wenzelm@22665
   593
  done
avigad@16908
   594
wenzelm@55821
   595
lemma bigo_setsum2: "\<forall>y. 0 \<le> h y \<Longrightarrow>
wenzelm@61945
   596
    \<exists>c. \<forall>y. \<bar>f y\<bar> \<le> c * (h y) \<Longrightarrow>
wenzelm@55821
   597
      (\<lambda>x. \<Sum>y \<in> A x. f y) =o O(\<lambda>x. \<Sum>y \<in> A x. h y)"
wenzelm@55821
   598
  by (rule bigo_setsum1) auto
avigad@16908
   599
wenzelm@55821
   600
lemma bigo_setsum3: "f =o O(h) \<Longrightarrow>
wenzelm@61945
   601
    (\<lambda>x. \<Sum>y \<in> A x. l x y * f (k x y)) =o O(\<lambda>x. \<Sum>y \<in> A x. \<bar>l x y * h (k x y)\<bar>)"
avigad@16908
   602
  apply (rule bigo_setsum1)
avigad@16908
   603
  apply (rule allI)+
avigad@16908
   604
  apply (rule abs_ge_zero)
avigad@16908
   605
  apply (unfold bigo_def)
avigad@16908
   606
  apply auto
avigad@16908
   607
  apply (rule_tac x = c in exI)
avigad@16908
   608
  apply (rule allI)+
avigad@16908
   609
  apply (subst abs_mult)+
haftmann@57512
   610
  apply (subst mult.left_commute)
avigad@16908
   611
  apply (rule mult_left_mono)
avigad@16908
   612
  apply (erule spec)
avigad@16908
   613
  apply (rule abs_ge_zero)
wenzelm@22665
   614
  done
avigad@16908
   615
wenzelm@55821
   616
lemma bigo_setsum4: "f =o g +o O(h) \<Longrightarrow>
wenzelm@55821
   617
    (\<lambda>x. \<Sum>y \<in> A x. l x y * f (k x y)) =o
wenzelm@55821
   618
      (\<lambda>x. \<Sum>y \<in> A x. l x y * g (k x y)) +o
wenzelm@61945
   619
        O(\<lambda>x. \<Sum>y \<in> A x. \<bar>l x y * h (k x y)\<bar>)"
avigad@16908
   620
  apply (rule set_minus_imp_plus)
berghofe@26814
   621
  apply (subst fun_diff_def)
avigad@16908
   622
  apply (subst setsum_subtractf [symmetric])
avigad@16908
   623
  apply (subst right_diff_distrib [symmetric])
avigad@16908
   624
  apply (rule bigo_setsum3)
berghofe@26814
   625
  apply (subst fun_diff_def [symmetric])
avigad@16908
   626
  apply (erule set_plus_imp_minus)
wenzelm@22665
   627
  done
avigad@16908
   628
wenzelm@55821
   629
lemma bigo_setsum5: "f =o O(h) \<Longrightarrow> \<forall>x y. 0 \<le> l x y \<Longrightarrow>
wenzelm@55821
   630
    \<forall>x. 0 \<le> h x \<Longrightarrow>
wenzelm@55821
   631
      (\<lambda>x. \<Sum>y \<in> A x. l x y * f (k x y)) =o
wenzelm@55821
   632
        O(\<lambda>x. \<Sum>y \<in> A x. l x y * h (k x y))"
wenzelm@55821
   633
  apply (subgoal_tac "(\<lambda>x. \<Sum>y \<in> A x. l x y * h (k x y)) =
wenzelm@61945
   634
      (\<lambda>x. \<Sum>y \<in> A x. \<bar>l x y * h (k x y)\<bar>)")
avigad@16908
   635
  apply (erule ssubst)
avigad@16908
   636
  apply (erule bigo_setsum3)
avigad@16908
   637
  apply (rule ext)
haftmann@57418
   638
  apply (rule setsum.cong)
haftmann@57418
   639
  apply (rule refl)
avigad@16908
   640
  apply (subst abs_of_nonneg)
avigad@16908
   641
  apply auto
wenzelm@22665
   642
  done
avigad@16908
   643
wenzelm@55821
   644
lemma bigo_setsum6: "f =o g +o O(h) \<Longrightarrow> \<forall>x y. 0 \<le> l x y \<Longrightarrow>
wenzelm@55821
   645
    \<forall>x. 0 \<le> h x \<Longrightarrow>
wenzelm@55821
   646
      (\<lambda>x. \<Sum>y \<in> A x. l x y * f (k x y)) =o
wenzelm@55821
   647
        (\<lambda>x. \<Sum>y \<in> A x. l x y * g (k x y)) +o
wenzelm@55821
   648
          O(\<lambda>x. \<Sum>y \<in> A x. l x y * h (k x y))"
avigad@16908
   649
  apply (rule set_minus_imp_plus)
berghofe@26814
   650
  apply (subst fun_diff_def)
avigad@16908
   651
  apply (subst setsum_subtractf [symmetric])
avigad@16908
   652
  apply (subst right_diff_distrib [symmetric])
avigad@16908
   653
  apply (rule bigo_setsum5)
berghofe@26814
   654
  apply (subst fun_diff_def [symmetric])
avigad@16908
   655
  apply (drule set_plus_imp_minus)
avigad@16908
   656
  apply auto
wenzelm@22665
   657
  done
wenzelm@22665
   658
avigad@16908
   659
wenzelm@60500
   660
subsection \<open>Misc useful stuff\<close>
avigad@16908
   661
wenzelm@55821
   662
lemma bigo_useful_intro: "A \<subseteq> O(f) \<Longrightarrow> B \<subseteq> O(f) \<Longrightarrow> A + B \<subseteq> O(f)"
avigad@16908
   663
  apply (subst bigo_plus_idemp [symmetric])
avigad@16908
   664
  apply (rule set_plus_mono2)
avigad@16908
   665
  apply assumption+
wenzelm@22665
   666
  done
avigad@16908
   667
wenzelm@55821
   668
lemma bigo_useful_add: "f =o O(h) \<Longrightarrow> g =o O(h) \<Longrightarrow> f + g =o O(h)"
avigad@16908
   669
  apply (subst bigo_plus_idemp [symmetric])
avigad@16908
   670
  apply (rule set_plus_intro)
avigad@16908
   671
  apply assumption+
wenzelm@22665
   672
  done
wenzelm@55821
   673
wenzelm@55821
   674
lemma bigo_useful_const_mult:
wenzelm@55821
   675
  fixes c :: "'a::linordered_field"
wenzelm@55821
   676
  shows "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. c) * f =o O(h) \<Longrightarrow> f =o O(h)"
avigad@16908
   677
  apply (rule subsetD)
wenzelm@55821
   678
  apply (subgoal_tac "(\<lambda>x. 1 / c) *o O(h) \<subseteq> O(h)")
avigad@16908
   679
  apply assumption
avigad@16908
   680
  apply (rule bigo_const_mult6)
wenzelm@55821
   681
  apply (subgoal_tac "f = (\<lambda>x. 1 / c) * ((\<lambda>x. c) * f)")
avigad@16908
   682
  apply (erule ssubst)
avigad@16908
   683
  apply (erule set_times_intro2)
nipkow@23413
   684
  apply (simp add: func_times)
wenzelm@22665
   685
  done
avigad@16908
   686
wenzelm@55821
   687
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)"
avigad@16908
   688
  apply (simp add: bigo_alt_def)
avigad@16908
   689
  apply auto
avigad@16908
   690
  apply (rule_tac x = c in exI)
avigad@16908
   691
  apply auto
avigad@16908
   692
  apply (case_tac "x = 0")
avigad@16908
   693
  apply simp
avigad@16908
   694
  apply (subgoal_tac "x = Suc (x - 1)")
wenzelm@17199
   695
  apply (erule ssubst) back
avigad@16908
   696
  apply (erule spec)
avigad@16908
   697
  apply simp
wenzelm@22665
   698
  done
avigad@16908
   699
wenzelm@55821
   700
lemma bigo_fix2:
wenzelm@55821
   701
    "(\<lambda>x. f ((x::nat) + 1)) =o (\<lambda>x. g(x + 1)) +o O(\<lambda>x. h(x + 1)) \<Longrightarrow>
wenzelm@55821
   702
       f 0 = g 0 \<Longrightarrow> f =o g +o O(h)"
avigad@16908
   703
  apply (rule set_minus_imp_plus)
avigad@16908
   704
  apply (rule bigo_fix)
berghofe@26814
   705
  apply (subst fun_diff_def)
berghofe@26814
   706
  apply (subst fun_diff_def [symmetric])
avigad@16908
   707
  apply (rule set_plus_imp_minus)
avigad@16908
   708
  apply simp
berghofe@26814
   709
  apply (simp add: fun_diff_def)
wenzelm@22665
   710
  done
wenzelm@22665
   711
avigad@16908
   712
wenzelm@60500
   713
subsection \<open>Less than or equal to\<close>
avigad@16908
   714
wenzelm@55821
   715
definition lesso :: "('a \<Rightarrow> 'b::linordered_idom) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"  (infixl "<o" 70)
wenzelm@55821
   716
  where "f <o g = (\<lambda>x. max (f x - g x) 0)"
avigad@16908
   717
wenzelm@61945
   718
lemma bigo_lesseq1: "f =o O(h) \<Longrightarrow> \<forall>x. \<bar>g x\<bar> \<le> \<bar>f x\<bar> \<Longrightarrow> g =o O(h)"
avigad@16908
   719
  apply (unfold bigo_def)
avigad@16908
   720
  apply clarsimp
avigad@16908
   721
  apply (rule_tac x = c in exI)
avigad@16908
   722
  apply (rule allI)
avigad@16908
   723
  apply (rule order_trans)
avigad@16908
   724
  apply (erule spec)+
wenzelm@22665
   725
  done
avigad@16908
   726
wenzelm@61945
   727
lemma bigo_lesseq2: "f =o O(h) \<Longrightarrow> \<forall>x. \<bar>g x\<bar> \<le> f x \<Longrightarrow> g =o O(h)"
avigad@16908
   728
  apply (erule bigo_lesseq1)
avigad@16908
   729
  apply (rule allI)
avigad@16908
   730
  apply (drule_tac x = x in spec)
avigad@16908
   731
  apply (rule order_trans)
avigad@16908
   732
  apply assumption
avigad@16908
   733
  apply (rule abs_ge_self)
wenzelm@22665
   734
  done
avigad@16908
   735
wenzelm@55821
   736
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)"
avigad@16908
   737
  apply (erule bigo_lesseq2)
avigad@16908
   738
  apply (rule allI)
avigad@16908
   739
  apply (subst abs_of_nonneg)
avigad@16908
   740
  apply (erule spec)+
wenzelm@22665
   741
  done
avigad@16908
   742
wenzelm@55821
   743
lemma bigo_lesseq4: "f =o O(h) \<Longrightarrow>
wenzelm@61945
   744
    \<forall>x. 0 \<le> g x \<Longrightarrow> \<forall>x. g x \<le> \<bar>f x\<bar> \<Longrightarrow> g =o O(h)"
avigad@16908
   745
  apply (erule bigo_lesseq1)
avigad@16908
   746
  apply (rule allI)
avigad@16908
   747
  apply (subst abs_of_nonneg)
avigad@16908
   748
  apply (erule spec)+
wenzelm@22665
   749
  done
avigad@16908
   750
wenzelm@55821
   751
lemma bigo_lesso1: "\<forall>x. f x \<le> g x \<Longrightarrow> f <o g =o O(h)"
avigad@16908
   752
  apply (unfold lesso_def)
wenzelm@55821
   753
  apply (subgoal_tac "(\<lambda>x. max (f x - g x) 0) = 0")
avigad@16908
   754
  apply (erule ssubst)
avigad@16908
   755
  apply (rule bigo_zero)
avigad@16908
   756
  apply (unfold func_zero)
avigad@16908
   757
  apply (rule ext)
avigad@16908
   758
  apply (simp split: split_max)
wenzelm@22665
   759
  done
avigad@16908
   760
wenzelm@55821
   761
lemma bigo_lesso2: "f =o g +o O(h) \<Longrightarrow>
wenzelm@55821
   762
    \<forall>x. 0 \<le> k x \<Longrightarrow> \<forall>x. k x \<le> f x \<Longrightarrow> k <o g =o O(h)"
avigad@16908
   763
  apply (unfold lesso_def)
avigad@16908
   764
  apply (rule bigo_lesseq4)
avigad@16908
   765
  apply (erule set_plus_imp_minus)
avigad@16908
   766
  apply (rule allI)
haftmann@54863
   767
  apply (rule max.cobounded2)
avigad@16908
   768
  apply (rule allI)
berghofe@26814
   769
  apply (subst fun_diff_def)
wenzelm@55821
   770
  apply (case_tac "0 \<le> k x - g x")
avigad@16908
   771
  apply simp
avigad@16908
   772
  apply (subst abs_of_nonneg)
wenzelm@17199
   773
  apply (drule_tac x = x in spec) back
nipkow@29667
   774
  apply (simp add: algebra_simps)
haftmann@54230
   775
  apply (subst diff_conv_add_uminus)+
avigad@16908
   776
  apply (rule add_right_mono)
avigad@16908
   777
  apply (erule spec)
wenzelm@55821
   778
  apply (rule order_trans)
avigad@16908
   779
  prefer 2
avigad@16908
   780
  apply (rule abs_ge_zero)
nipkow@29667
   781
  apply (simp add: algebra_simps)
wenzelm@22665
   782
  done
avigad@16908
   783
wenzelm@55821
   784
lemma bigo_lesso3: "f =o g +o O(h) \<Longrightarrow>
wenzelm@55821
   785
    \<forall>x. 0 \<le> k x \<Longrightarrow> \<forall>x. g x \<le> k x \<Longrightarrow> f <o k =o O(h)"
avigad@16908
   786
  apply (unfold lesso_def)
avigad@16908
   787
  apply (rule bigo_lesseq4)
avigad@16908
   788
  apply (erule set_plus_imp_minus)
avigad@16908
   789
  apply (rule allI)
haftmann@54863
   790
  apply (rule max.cobounded2)
avigad@16908
   791
  apply (rule allI)
berghofe@26814
   792
  apply (subst fun_diff_def)
wenzelm@55821
   793
  apply (case_tac "0 \<le> f x - k x")
avigad@16908
   794
  apply simp
avigad@16908
   795
  apply (subst abs_of_nonneg)
wenzelm@17199
   796
  apply (drule_tac x = x in spec) back
nipkow@29667
   797
  apply (simp add: algebra_simps)
haftmann@54230
   798
  apply (subst diff_conv_add_uminus)+
avigad@16908
   799
  apply (rule add_left_mono)
avigad@16908
   800
  apply (rule le_imp_neg_le)
avigad@16908
   801
  apply (erule spec)
wenzelm@55821
   802
  apply (rule order_trans)
avigad@16908
   803
  prefer 2
avigad@16908
   804
  apply (rule abs_ge_zero)
nipkow@29667
   805
  apply (simp add: algebra_simps)
wenzelm@22665
   806
  done
avigad@16908
   807
wenzelm@55821
   808
lemma bigo_lesso4:
wenzelm@55821
   809
  fixes k :: "'a \<Rightarrow> 'b::linordered_field"
wenzelm@55821
   810
  shows "f <o g =o O(k) \<Longrightarrow> g =o h +o O(k) \<Longrightarrow> f <o h =o O(k)"
avigad@16908
   811
  apply (unfold lesso_def)
avigad@16908
   812
  apply (drule set_plus_imp_minus)
wenzelm@17199
   813
  apply (drule bigo_abs5) back
berghofe@26814
   814
  apply (simp add: fun_diff_def)
avigad@16908
   815
  apply (drule bigo_useful_add)
avigad@16908
   816
  apply assumption
wenzelm@17199
   817
  apply (erule bigo_lesseq2) back
avigad@16908
   818
  apply (rule allI)
wenzelm@55821
   819
  apply (auto simp add: func_plus fun_diff_def algebra_simps split: split_max abs_split)
wenzelm@22665
   820
  done
avigad@16908
   821
wenzelm@61945
   822
lemma bigo_lesso5: "f <o g =o O(h) \<Longrightarrow> \<exists>C. \<forall>x. f x \<le> g x + C * \<bar>h x\<bar>"
avigad@16908
   823
  apply (simp only: lesso_def bigo_alt_def)
avigad@16908
   824
  apply clarsimp
avigad@16908
   825
  apply (rule_tac x = c in exI)
avigad@16908
   826
  apply (rule allI)
avigad@16908
   827
  apply (drule_tac x = x in spec)
wenzelm@61945
   828
  apply (subgoal_tac "\<bar>max (f x - g x) 0\<bar> = max (f x - g x) 0")
wenzelm@55821
   829
  apply (clarsimp simp add: algebra_simps)
avigad@16908
   830
  apply (rule abs_of_nonneg)
haftmann@54863
   831
  apply (rule max.cobounded2)
wenzelm@22665
   832
  done
avigad@16908
   833
wenzelm@55821
   834
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)"
avigad@16908
   835
  apply (unfold lesso_def)
avigad@16908
   836
  apply (rule bigo_lesseq3)
avigad@16908
   837
  apply (erule bigo_useful_add)
avigad@16908
   838
  apply assumption
avigad@16908
   839
  apply (force split: split_max)
avigad@16908
   840
  apply (auto split: split_max simp add: func_plus)
wenzelm@22665
   841
  done
avigad@16908
   842
wenzelm@55821
   843
lemma bigo_LIMSEQ1: "f =o O(g) \<Longrightarrow> g ----> 0 \<Longrightarrow> f ----> (0::real)"
huffman@31337
   844
  apply (simp add: LIMSEQ_iff bigo_alt_def)
haftmann@29786
   845
  apply clarify
haftmann@29786
   846
  apply (drule_tac x = "r / c" in spec)
haftmann@29786
   847
  apply (drule mp)
nipkow@56541
   848
  apply simp
haftmann@29786
   849
  apply clarify
haftmann@29786
   850
  apply (rule_tac x = no in exI)
haftmann@29786
   851
  apply (rule allI)
haftmann@29786
   852
  apply (drule_tac x = n in spec)+
haftmann@29786
   853
  apply (rule impI)
haftmann@29786
   854
  apply (drule mp)
haftmann@29786
   855
  apply assumption
haftmann@29786
   856
  apply (rule order_le_less_trans)
haftmann@29786
   857
  apply assumption
haftmann@29786
   858
  apply (rule order_less_le_trans)
wenzelm@61945
   859
  apply (subgoal_tac "c * \<bar>g n\<bar> < c * (r / c)")
haftmann@29786
   860
  apply assumption
haftmann@29786
   861
  apply (erule mult_strict_left_mono)
haftmann@29786
   862
  apply assumption
haftmann@29786
   863
  apply simp
wenzelm@55821
   864
  done
haftmann@29786
   865
wenzelm@55821
   866
lemma bigo_LIMSEQ2: "f =o g +o O(h) \<Longrightarrow> h ----> 0 \<Longrightarrow> f ----> a \<Longrightarrow> g ----> (a::real)"
haftmann@29786
   867
  apply (drule set_plus_imp_minus)
haftmann@29786
   868
  apply (drule bigo_LIMSEQ1)
haftmann@29786
   869
  apply assumption
haftmann@29786
   870
  apply (simp only: fun_diff_def)
lp15@60142
   871
  apply (erule Lim_transform2)
haftmann@29786
   872
  apply assumption
wenzelm@55821
   873
  done
haftmann@29786
   874
avigad@16908
   875
end