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