src/HOL/Metis_Examples/BigO.thy
 author wenzelm Wed Dec 29 17:34:41 2010 +0100 (2010-12-29) changeset 41413 64cd30d6b0b8 parent 41144 509e51b7509a child 41541 1fa4725c4656 permissions -rw-r--r--
explicit file specifications -- avoid secondary load path;
```     1 (*  Title:      HOL/Metis_Examples/BigO.thy
```
```     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     3     Author:     Jasmin Blanchette, TU Muenchen
```
```     4
```
```     5 Testing Metis.
```
```     6 *)
```
```     7
```
```     8 header {* Big O notation *}
```
```     9
```
```    10 theory BigO
```
```    11 imports
```
```    12   "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
```
```    13   Main
```
```    14   "~~/src/HOL/Library/Function_Algebras"
```
```    15   "~~/src/HOL/Library/Set_Algebras"
```
```    16 begin
```
```    17
```
```    18 subsection {* Definitions *}
```
```    19
```
```    20 definition bigo :: "('a => 'b::linordered_idom) => ('a => 'b) set"    ("(1O'(_'))") where
```
```    21   "O(f::('a => 'b)) ==   {h. EX c. ALL x. abs (h x) <= c * abs (f x)}"
```
```    22
```
```    23 declare [[ sledgehammer_problem_prefix = "BigO__bigo_pos_const" ]]
```
```    24 lemma bigo_pos_const: "(EX (c::'a::linordered_idom).
```
```    25     ALL x. (abs (h x)) <= (c * (abs (f x))))
```
```    26       = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
```
```    27   apply auto
```
```    28   apply (case_tac "c = 0", simp)
```
```    29   apply (rule_tac x = "1" in exI, simp)
```
```    30   apply (rule_tac x = "abs c" in exI, auto)
```
```    31   apply (metis abs_ge_zero abs_of_nonneg Orderings.xt1(6) abs_mult)
```
```    32   done
```
```    33
```
```    34 (*** Now various verions with an increasing shrink factor ***)
```
```    35
```
```    36 sledgehammer_params [isar_proof, isar_shrink_factor = 1]
```
```    37
```
```    38 lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom).
```
```    39     ALL x. (abs (h x)) <= (c * (abs (f x))))
```
```    40       = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
```
```    41   apply auto
```
```    42   apply (case_tac "c = 0", simp)
```
```    43   apply (rule_tac x = "1" in exI, simp)
```
```    44   apply (rule_tac x = "abs c" in exI, auto)
```
```    45 proof -
```
```    46   fix c :: 'a and x :: 'b
```
```    47   assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
```
```    48   have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 0 \<le> \<bar>x\<^isub>1\<bar>" by (metis abs_ge_zero)
```
```    49   have F2: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis mult_1)
```
```    50   have F3: "\<forall>x\<^isub>1 x\<^isub>3. x\<^isub>3 \<le> \<bar>h x\<^isub>1\<bar> \<longrightarrow> x\<^isub>3 \<le> c * \<bar>f x\<^isub>1\<bar>" by (metis A1 order_trans)
```
```    51   have F4: "\<forall>x\<^isub>2 x\<^isub>3\<Colon>'a\<Colon>linordered_idom. \<bar>x\<^isub>3\<bar> * \<bar>x\<^isub>2\<bar> = \<bar>x\<^isub>3 * x\<^isub>2\<bar>"
```
```    52     by (metis abs_mult)
```
```    53   have F5: "\<forall>x\<^isub>3 x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 0 \<le> x\<^isub>1 \<longrightarrow> \<bar>x\<^isub>3 * x\<^isub>1\<bar> = \<bar>x\<^isub>3\<bar> * x\<^isub>1"
```
```    54     by (metis abs_mult_pos)
```
```    55   hence "\<forall>x\<^isub>1\<ge>0. \<bar>x\<^isub>1\<Colon>'a\<Colon>linordered_idom\<bar> = \<bar>1\<bar> * x\<^isub>1" by (metis F2)
```
```    56   hence "\<forall>x\<^isub>1\<ge>0. \<bar>x\<^isub>1\<Colon>'a\<Colon>linordered_idom\<bar> = x\<^isub>1" by (metis F2 abs_one)
```
```    57   hence "\<forall>x\<^isub>3. 0 \<le> \<bar>h x\<^isub>3\<bar> \<longrightarrow> \<bar>c * \<bar>f x\<^isub>3\<bar>\<bar> = c * \<bar>f x\<^isub>3\<bar>" by (metis F3)
```
```    58   hence "\<forall>x\<^isub>3. \<bar>c * \<bar>f x\<^isub>3\<bar>\<bar> = c * \<bar>f x\<^isub>3\<bar>" by (metis F1)
```
```    59   hence "\<forall>x\<^isub>3. (0\<Colon>'a) \<le> \<bar>f x\<^isub>3\<bar> \<longrightarrow> c * \<bar>f x\<^isub>3\<bar> = \<bar>c\<bar> * \<bar>f x\<^isub>3\<bar>" by (metis F5)
```
```    60   hence "\<forall>x\<^isub>3. (0\<Colon>'a) \<le> \<bar>f x\<^isub>3\<bar> \<longrightarrow> c * \<bar>f x\<^isub>3\<bar> = \<bar>c * f x\<^isub>3\<bar>" by (metis F4)
```
```    61   hence "\<forall>x\<^isub>3. c * \<bar>f x\<^isub>3\<bar> = \<bar>c * f x\<^isub>3\<bar>" by (metis F1)
```
```    62   hence "\<bar>h x\<bar> \<le> \<bar>c * f x\<bar>" by (metis A1)
```
```    63   thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F4)
```
```    64 qed
```
```    65
```
```    66 sledgehammer_params [isar_proof, isar_shrink_factor = 2]
```
```    67
```
```    68 lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom).
```
```    69     ALL x. (abs (h x)) <= (c * (abs (f x))))
```
```    70       = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
```
```    71   apply auto
```
```    72   apply (case_tac "c = 0", simp)
```
```    73   apply (rule_tac x = "1" in exI, simp)
```
```    74   apply (rule_tac x = "abs c" in exI, auto)
```
```    75 proof -
```
```    76   fix c :: 'a and x :: 'b
```
```    77   assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
```
```    78   have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis mult_1)
```
```    79   have F2: "\<forall>x\<^isub>2 x\<^isub>3\<Colon>'a\<Colon>linordered_idom. \<bar>x\<^isub>3\<bar> * \<bar>x\<^isub>2\<bar> = \<bar>x\<^isub>3 * x\<^isub>2\<bar>"
```
```    80     by (metis abs_mult)
```
```    81   have "\<forall>x\<^isub>1\<ge>0. \<bar>x\<^isub>1\<Colon>'a\<Colon>linordered_idom\<bar> = x\<^isub>1" by (metis F1 abs_mult_pos abs_one)
```
```    82   hence "\<forall>x\<^isub>3. \<bar>c * \<bar>f x\<^isub>3\<bar>\<bar> = c * \<bar>f x\<^isub>3\<bar>" by (metis A1 abs_ge_zero order_trans)
```
```    83   hence "\<forall>x\<^isub>3. 0 \<le> \<bar>f x\<^isub>3\<bar> \<longrightarrow> c * \<bar>f x\<^isub>3\<bar> = \<bar>c * f x\<^isub>3\<bar>" by (metis F2 abs_mult_pos)
```
```    84   hence "\<bar>h x\<bar> \<le> \<bar>c * f x\<bar>" by (metis A1 abs_ge_zero)
```
```    85   thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F2)
```
```    86 qed
```
```    87
```
```    88 sledgehammer_params [isar_proof, isar_shrink_factor = 3]
```
```    89
```
```    90 lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom).
```
```    91     ALL x. (abs (h x)) <= (c * (abs (f x))))
```
```    92       = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
```
```    93   apply auto
```
```    94   apply (case_tac "c = 0", simp)
```
```    95   apply (rule_tac x = "1" in exI, simp)
```
```    96   apply (rule_tac x = "abs c" in exI, auto)
```
```    97 proof -
```
```    98   fix c :: 'a and x :: 'b
```
```    99   assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
```
```   100   have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis mult_1)
```
```   101   have F2: "\<forall>x\<^isub>3 x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 0 \<le> x\<^isub>1 \<longrightarrow> \<bar>x\<^isub>3 * x\<^isub>1\<bar> = \<bar>x\<^isub>3\<bar> * x\<^isub>1" by (metis abs_mult_pos)
```
```   102   hence "\<forall>x\<^isub>1\<ge>0. \<bar>x\<^isub>1\<Colon>'a\<Colon>linordered_idom\<bar> = x\<^isub>1" by (metis F1 abs_one)
```
```   103   hence "\<forall>x\<^isub>3. 0 \<le> \<bar>f x\<^isub>3\<bar> \<longrightarrow> c * \<bar>f x\<^isub>3\<bar> = \<bar>c\<bar> * \<bar>f x\<^isub>3\<bar>" by (metis F2 A1 abs_ge_zero order_trans)
```
```   104   thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis A1 abs_mult abs_ge_zero)
```
```   105 qed
```
```   106
```
```   107 sledgehammer_params [isar_proof, isar_shrink_factor = 4]
```
```   108
```
```   109 lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom).
```
```   110     ALL x. (abs (h x)) <= (c * (abs (f x))))
```
```   111       = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
```
```   112   apply auto
```
```   113   apply (case_tac "c = 0", simp)
```
```   114   apply (rule_tac x = "1" in exI, simp)
```
```   115   apply (rule_tac x = "abs c" in exI, auto)
```
```   116 proof -
```
```   117   fix c :: 'a and x :: 'b
```
```   118   assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
```
```   119   have "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis mult_1)
```
```   120   hence "\<forall>x\<^isub>3. \<bar>c * \<bar>f x\<^isub>3\<bar>\<bar> = c * \<bar>f x\<^isub>3\<bar>"
```
```   121     by (metis A1 abs_ge_zero order_trans abs_mult_pos abs_one)
```
```   122   hence "\<bar>h x\<bar> \<le> \<bar>c * f x\<bar>" by (metis A1 abs_ge_zero abs_mult_pos abs_mult)
```
```   123   thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis abs_mult)
```
```   124 qed
```
```   125
```
```   126 sledgehammer_params [isar_proof, isar_shrink_factor = 1]
```
```   127
```
```   128 lemma bigo_alt_def: "O(f) =
```
```   129     {h. EX c. (0 < c & (ALL x. abs (h x) <= c * abs (f x)))}"
```
```   130 by (auto simp add: bigo_def bigo_pos_const)
```
```   131
```
```   132 declare [[ sledgehammer_problem_prefix = "BigO__bigo_elt_subset" ]]
```
```   133 lemma bigo_elt_subset [intro]: "f : O(g) ==> O(f) <= O(g)"
```
```   134   apply (auto simp add: bigo_alt_def)
```
```   135   apply (rule_tac x = "ca * c" in exI)
```
```   136   apply (rule conjI)
```
```   137   apply (rule mult_pos_pos)
```
```   138   apply (assumption)+
```
```   139 (*sledgehammer*)
```
```   140   apply (rule allI)
```
```   141   apply (drule_tac x = "xa" in spec)+
```
```   142   apply (subgoal_tac "ca * abs(f xa) <= ca * (c * abs(g xa))")
```
```   143   apply (erule order_trans)
```
```   144   apply (simp add: mult_ac)
```
```   145   apply (rule mult_left_mono, assumption)
```
```   146   apply (rule order_less_imp_le, assumption)
```
```   147 done
```
```   148
```
```   149
```
```   150 declare [[ sledgehammer_problem_prefix = "BigO__bigo_refl" ]]
```
```   151 lemma bigo_refl [intro]: "f : O(f)"
```
```   152 apply (auto simp add: bigo_def)
```
```   153 by (metis mult_1 order_refl)
```
```   154
```
```   155 declare [[ sledgehammer_problem_prefix = "BigO__bigo_zero" ]]
```
```   156 lemma bigo_zero: "0 : O(g)"
```
```   157 apply (auto simp add: bigo_def func_zero)
```
```   158 by (metis mult_zero_left order_refl)
```
```   159
```
```   160 lemma bigo_zero2: "O(%x.0) = {%x.0}"
```
```   161   apply (auto simp add: bigo_def)
```
```   162   apply (rule ext)
```
```   163   apply auto
```
```   164 done
```
```   165
```
```   166 lemma bigo_plus_self_subset [intro]:
```
```   167   "O(f) \<oplus> O(f) <= O(f)"
```
```   168   apply (auto simp add: bigo_alt_def set_plus_def)
```
```   169   apply (rule_tac x = "c + ca" in exI)
```
```   170   apply auto
```
```   171   apply (simp add: ring_distribs func_plus)
```
```   172   apply (blast intro:order_trans abs_triangle_ineq add_mono elim:)
```
```   173 done
```
```   174
```
```   175 lemma bigo_plus_idemp [simp]: "O(f) \<oplus> O(f) = O(f)"
```
```   176   apply (rule equalityI)
```
```   177   apply (rule bigo_plus_self_subset)
```
```   178   apply (rule set_zero_plus2)
```
```   179   apply (rule bigo_zero)
```
```   180 done
```
```   181
```
```   182 lemma bigo_plus_subset [intro]: "O(f + g) <= O(f) \<oplus> O(g)"
```
```   183   apply (rule subsetI)
```
```   184   apply (auto simp add: bigo_def bigo_pos_const func_plus set_plus_def)
```
```   185   apply (subst bigo_pos_const [symmetric])+
```
```   186   apply (rule_tac x =
```
```   187     "%n. if abs (g n) <= (abs (f n)) then x n else 0" in exI)
```
```   188   apply (rule conjI)
```
```   189   apply (rule_tac x = "c + c" in exI)
```
```   190   apply (clarsimp)
```
```   191   apply (auto)
```
```   192   apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (f xa)")
```
```   193   apply (erule_tac x = xa in allE)
```
```   194   apply (erule order_trans)
```
```   195   apply (simp)
```
```   196   apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))")
```
```   197   apply (erule order_trans)
```
```   198   apply (simp add: ring_distribs)
```
```   199   apply (rule mult_left_mono)
```
```   200   apply assumption
```
```   201   apply (simp add: order_less_le)
```
```   202   apply (rule mult_left_mono)
```
```   203   apply (simp add: abs_triangle_ineq)
```
```   204   apply (simp add: order_less_le)
```
```   205   apply (rule mult_nonneg_nonneg)
```
```   206   apply (rule add_nonneg_nonneg)
```
```   207   apply auto
```
```   208   apply (rule_tac x = "%n. if (abs (f n)) <  abs (g n) then x n else 0"
```
```   209      in exI)
```
```   210   apply (rule conjI)
```
```   211   apply (rule_tac x = "c + c" in exI)
```
```   212   apply auto
```
```   213   apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (g xa)")
```
```   214   apply (erule_tac x = xa in allE)
```
```   215   apply (erule order_trans)
```
```   216   apply (simp)
```
```   217   apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))")
```
```   218   apply (erule order_trans)
```
```   219   apply (simp add: ring_distribs)
```
```   220   apply (rule mult_left_mono)
```
```   221   apply (simp add: order_less_le)
```
```   222   apply (simp add: order_less_le)
```
```   223   apply (rule mult_left_mono)
```
```   224   apply (rule abs_triangle_ineq)
```
```   225   apply (simp add: order_less_le)
```
```   226 apply (metis abs_not_less_zero double_less_0_iff less_not_permute linorder_not_less mult_less_0_iff)
```
```   227   apply (rule ext)
```
```   228   apply (auto simp add: if_splits linorder_not_le)
```
```   229 done
```
```   230
```
```   231 lemma bigo_plus_subset2 [intro]: "A <= O(f) ==> B <= O(f) ==> A \<oplus> B <= O(f)"
```
```   232   apply (subgoal_tac "A \<oplus> B <= O(f) \<oplus> O(f)")
```
```   233   apply (erule order_trans)
```
```   234   apply simp
```
```   235   apply (auto del: subsetI simp del: bigo_plus_idemp)
```
```   236 done
```
```   237
```
```   238 declare [[ sledgehammer_problem_prefix = "BigO__bigo_plus_eq" ]]
```
```   239 lemma bigo_plus_eq: "ALL x. 0 <= f x ==> ALL x. 0 <= g x ==>
```
```   240   O(f + g) = O(f) \<oplus> O(g)"
```
```   241   apply (rule equalityI)
```
```   242   apply (rule bigo_plus_subset)
```
```   243   apply (simp add: bigo_alt_def set_plus_def func_plus)
```
```   244   apply clarify
```
```   245 (*sledgehammer*)
```
```   246   apply (rule_tac x = "max c ca" in exI)
```
```   247   apply (rule conjI)
```
```   248    apply (metis Orderings.less_max_iff_disj)
```
```   249   apply clarify
```
```   250   apply (drule_tac x = "xa" in spec)+
```
```   251   apply (subgoal_tac "0 <= f xa + g xa")
```
```   252   apply (simp add: ring_distribs)
```
```   253   apply (subgoal_tac "abs(a xa + b xa) <= abs(a xa) + abs(b xa)")
```
```   254   apply (subgoal_tac "abs(a xa) + abs(b xa) <=
```
```   255       max c ca * f xa + max c ca * g xa")
```
```   256   apply (blast intro: order_trans)
```
```   257   defer 1
```
```   258   apply (rule abs_triangle_ineq)
```
```   259   apply (metis add_nonneg_nonneg)
```
```   260   apply (rule add_mono)
```
```   261 using [[ sledgehammer_problem_prefix = "BigO__bigo_plus_eq_simpler" ]]
```
```   262   apply (metis le_maxI2 linorder_linear min_max.sup_absorb1 mult_right_mono xt1(6))
```
```   263   apply (metis le_maxI2 linorder_not_le mult_le_cancel_right order_trans)
```
```   264 done
```
```   265
```
```   266 declare [[ sledgehammer_problem_prefix = "BigO__bigo_bounded_alt" ]]
```
```   267 lemma bigo_bounded_alt: "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==>
```
```   268     f : O(g)"
```
```   269   apply (auto simp add: bigo_def)
```
```   270 (* Version 1: one-line proof *)
```
```   271   apply (metis abs_le_D1 linorder_class.not_less  order_less_le  Orderings.xt1(12)  abs_mult)
```
```   272   done
```
```   273
```
```   274 lemma (*bigo_bounded_alt:*) "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==>
```
```   275     f : O(g)"
```
```   276 apply (auto simp add: bigo_def)
```
```   277 (* Version 2: structured proof *)
```
```   278 proof -
```
```   279   assume "\<forall>x. f x \<le> c * g x"
```
```   280   thus "\<exists>c. \<forall>x. f x \<le> c * \<bar>g x\<bar>" by (metis abs_mult abs_ge_self order_trans)
```
```   281 qed
```
```   282
```
```   283 text{*So here is the easier (and more natural) problem using transitivity*}
```
```   284 declare [[ sledgehammer_problem_prefix = "BigO__bigo_bounded_alt_trans" ]]
```
```   285 lemma "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> f : O(g)"
```
```   286 apply (auto simp add: bigo_def)
```
```   287 (* Version 1: one-line proof *)
```
```   288 by (metis abs_ge_self abs_mult order_trans)
```
```   289
```
```   290 text{*So here is the easier (and more natural) problem using transitivity*}
```
```   291 declare [[ sledgehammer_problem_prefix = "BigO__bigo_bounded_alt_trans" ]]
```
```   292 lemma "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> f : O(g)"
```
```   293   apply (auto simp add: bigo_def)
```
```   294 (* Version 2: structured proof *)
```
```   295 proof -
```
```   296   assume "\<forall>x. f x \<le> c * g x"
```
```   297   thus "\<exists>c. \<forall>x. f x \<le> c * \<bar>g x\<bar>" by (metis abs_mult abs_ge_self order_trans)
```
```   298 qed
```
```   299
```
```   300 lemma bigo_bounded: "ALL x. 0 <= f x ==> ALL x. f x <= g x ==>
```
```   301     f : O(g)"
```
```   302   apply (erule bigo_bounded_alt [of f 1 g])
```
```   303   apply simp
```
```   304 done
```
```   305
```
```   306 declare [[ sledgehammer_problem_prefix = "BigO__bigo_bounded2" ]]
```
```   307 lemma bigo_bounded2: "ALL x. lb x <= f x ==> ALL x. f x <= lb x + g x ==>
```
```   308     f : lb +o O(g)"
```
```   309 apply (rule set_minus_imp_plus)
```
```   310 apply (rule bigo_bounded)
```
```   311  apply (auto simp add: diff_minus fun_Compl_def func_plus)
```
```   312  prefer 2
```
```   313  apply (drule_tac x = x in spec)+
```
```   314  apply (metis add_right_mono add_commute diff_add_cancel diff_minus_eq_add le_less order_trans)
```
```   315 proof -
```
```   316   fix x :: 'a
```
```   317   assume "\<forall>x. lb x \<le> f x"
```
```   318   thus "(0\<Colon>'b) \<le> f x + - lb x" by (metis not_leE diff_minus less_iff_diff_less_0 less_le_not_le)
```
```   319 qed
```
```   320
```
```   321 declare [[ sledgehammer_problem_prefix = "BigO__bigo_abs" ]]
```
```   322 lemma bigo_abs: "(%x. abs(f x)) =o O(f)"
```
```   323 apply (unfold bigo_def)
```
```   324 apply auto
```
```   325 by (metis mult_1 order_refl)
```
```   326
```
```   327 declare [[ sledgehammer_problem_prefix = "BigO__bigo_abs2" ]]
```
```   328 lemma bigo_abs2: "f =o O(%x. abs(f x))"
```
```   329 apply (unfold bigo_def)
```
```   330 apply auto
```
```   331 by (metis mult_1 order_refl)
```
```   332
```
```   333 lemma bigo_abs3: "O(f) = O(%x. abs(f x))"
```
```   334 proof -
```
```   335   have F1: "\<forall>v u. u \<in> O(v) \<longrightarrow> O(u) \<subseteq> O(v)" by (metis bigo_elt_subset)
```
```   336   have F2: "\<forall>u. (\<lambda>R. \<bar>u R\<bar>) \<in> O(u)" by (metis bigo_abs)
```
```   337   have "\<forall>u. u \<in> O(\<lambda>R. \<bar>u R\<bar>)" by (metis bigo_abs2)
```
```   338   thus "O(f) = O(\<lambda>x. \<bar>f x\<bar>)" using F1 F2 by auto
```
```   339 qed
```
```   340
```
```   341 lemma bigo_abs4: "f =o g +o O(h) ==>
```
```   342     (%x. abs (f x)) =o (%x. abs (g x)) +o O(h)"
```
```   343   apply (drule set_plus_imp_minus)
```
```   344   apply (rule set_minus_imp_plus)
```
```   345   apply (subst fun_diff_def)
```
```   346 proof -
```
```   347   assume a: "f - g : O(h)"
```
```   348   have "(%x. abs (f x) - abs (g x)) =o O(%x. abs(abs (f x) - abs (g x)))"
```
```   349     by (rule bigo_abs2)
```
```   350   also have "... <= O(%x. abs (f x - g x))"
```
```   351     apply (rule bigo_elt_subset)
```
```   352     apply (rule bigo_bounded)
```
```   353     apply force
```
```   354     apply (rule allI)
```
```   355     apply (rule abs_triangle_ineq3)
```
```   356     done
```
```   357   also have "... <= O(f - g)"
```
```   358     apply (rule bigo_elt_subset)
```
```   359     apply (subst fun_diff_def)
```
```   360     apply (rule bigo_abs)
```
```   361     done
```
```   362   also have "... <= O(h)"
```
```   363     using a by (rule bigo_elt_subset)
```
```   364   finally show "(%x. abs (f x) - abs (g x)) : O(h)".
```
```   365 qed
```
```   366
```
```   367 lemma bigo_abs5: "f =o O(g) ==> (%x. abs(f x)) =o O(g)"
```
```   368 by (unfold bigo_def, auto)
```
```   369
```
```   370 lemma bigo_elt_subset2 [intro]: "f : g +o O(h) ==> O(f) <= O(g) \<oplus> O(h)"
```
```   371 proof -
```
```   372   assume "f : g +o O(h)"
```
```   373   also have "... <= O(g) \<oplus> O(h)"
```
```   374     by (auto del: subsetI)
```
```   375   also have "... = O(%x. abs(g x)) \<oplus> O(%x. abs(h x))"
```
```   376     apply (subst bigo_abs3 [symmetric])+
```
```   377     apply (rule refl)
```
```   378     done
```
```   379   also have "... = O((%x. abs(g x)) + (%x. abs(h x)))"
```
```   380     by (rule bigo_plus_eq [symmetric], auto)
```
```   381   finally have "f : ...".
```
```   382   then have "O(f) <= ..."
```
```   383     by (elim bigo_elt_subset)
```
```   384   also have "... = O(%x. abs(g x)) \<oplus> O(%x. abs(h x))"
```
```   385     by (rule bigo_plus_eq, auto)
```
```   386   finally show ?thesis
```
```   387     by (simp add: bigo_abs3 [symmetric])
```
```   388 qed
```
```   389
```
```   390 declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult" ]]
```
```   391 lemma bigo_mult [intro]: "O(f)\<otimes>O(g) <= O(f * g)"
```
```   392   apply (rule subsetI)
```
```   393   apply (subst bigo_def)
```
```   394   apply (auto simp del: abs_mult mult_ac
```
```   395               simp add: bigo_alt_def set_times_def func_times)
```
```   396 (*sledgehammer*);
```
```   397   apply (rule_tac x = "c * ca" in exI)
```
```   398   apply(rule allI)
```
```   399   apply(erule_tac x = x in allE)+
```
```   400   apply(subgoal_tac "c * ca * abs(f x * g x) =
```
```   401       (c * abs(f x)) * (ca * abs(g x))")
```
```   402 using [[ sledgehammer_problem_prefix = "BigO__bigo_mult_simpler" ]]
```
```   403 prefer 2
```
```   404 apply (metis mult_assoc mult_left_commute
```
```   405   abs_of_pos mult_left_commute
```
```   406   abs_mult mult_pos_pos)
```
```   407   apply (erule ssubst)
```
```   408   apply (subst abs_mult)
```
```   409 (* not quite as hard as BigO__bigo_mult_simpler_1 (a hard problem!) since
```
```   410    abs_mult has just been done *)
```
```   411 by (metis abs_ge_zero mult_mono')
```
```   412
```
```   413 declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult2" ]]
```
```   414 lemma bigo_mult2 [intro]: "f *o O(g) <= O(f * g)"
```
```   415   apply (auto simp add: bigo_def elt_set_times_def func_times abs_mult)
```
```   416 (*sledgehammer*);
```
```   417   apply (rule_tac x = c in exI)
```
```   418   apply clarify
```
```   419   apply (drule_tac x = x in spec)
```
```   420 using [[ sledgehammer_problem_prefix = "BigO__bigo_mult2_simpler" ]]
```
```   421 (*sledgehammer [no luck]*);
```
```   422   apply (subgoal_tac "abs(f x) * abs(b x) <= abs(f x) * (c * abs(g x))")
```
```   423   apply (simp add: mult_ac)
```
```   424   apply (rule mult_left_mono, assumption)
```
```   425   apply (rule abs_ge_zero)
```
```   426 done
```
```   427
```
```   428 declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult3" ]]
```
```   429 lemma bigo_mult3: "f : O(h) ==> g : O(j) ==> f * g : O(h * j)"
```
```   430 by (metis bigo_mult set_rev_mp set_times_intro)
```
```   431
```
```   432 declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult4" ]]
```
```   433 lemma bigo_mult4 [intro]:"f : k +o O(h) ==> g * f : (g * k) +o O(g * h)"
```
```   434 by (metis bigo_mult2 set_plus_mono_b set_times_intro2 set_times_plus_distrib)
```
```   435
```
```   436
```
```   437 lemma bigo_mult5: "ALL x. f x ~= 0 ==>
```
```   438     O(f * g) <= (f::'a => ('b::linordered_field)) *o O(g)"
```
```   439 proof -
```
```   440   assume "ALL x. f x ~= 0"
```
```   441   show "O(f * g) <= f *o O(g)"
```
```   442   proof
```
```   443     fix h
```
```   444     assume "h : O(f * g)"
```
```   445     then have "(%x. 1 / (f x)) * h : (%x. 1 / f x) *o O(f * g)"
```
```   446       by auto
```
```   447     also have "... <= O((%x. 1 / f x) * (f * g))"
```
```   448       by (rule bigo_mult2)
```
```   449     also have "(%x. 1 / f x) * (f * g) = g"
```
```   450       apply (simp add: func_times)
```
```   451       apply (rule ext)
```
```   452       apply (simp add: prems nonzero_divide_eq_eq mult_ac)
```
```   453       done
```
```   454     finally have "(%x. (1::'b) / f x) * h : O(g)".
```
```   455     then have "f * ((%x. (1::'b) / f x) * h) : f *o O(g)"
```
```   456       by auto
```
```   457     also have "f * ((%x. (1::'b) / f x) * h) = h"
```
```   458       apply (simp add: func_times)
```
```   459       apply (rule ext)
```
```   460       apply (simp add: prems nonzero_divide_eq_eq mult_ac)
```
```   461       done
```
```   462     finally show "h : f *o O(g)".
```
```   463   qed
```
```   464 qed
```
```   465
```
```   466 declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult6" ]]
```
```   467 lemma bigo_mult6: "ALL x. f x ~= 0 ==>
```
```   468     O(f * g) = (f::'a => ('b::linordered_field)) *o O(g)"
```
```   469 by (metis bigo_mult2 bigo_mult5 order_antisym)
```
```   470
```
```   471 (*proof requires relaxing relevance: 2007-01-25*)
```
```   472 declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult7" ]]
```
```   473   declare bigo_mult6 [simp]
```
```   474 lemma bigo_mult7: "ALL x. f x ~= 0 ==>
```
```   475     O(f * g) <= O(f::'a => ('b::linordered_field)) \<otimes> O(g)"
```
```   476 (*sledgehammer*)
```
```   477   apply (subst bigo_mult6)
```
```   478   apply assumption
```
```   479   apply (rule set_times_mono3)
```
```   480   apply (rule bigo_refl)
```
```   481 done
```
```   482   declare bigo_mult6 [simp del]
```
```   483
```
```   484 declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult8" ]]
```
```   485   declare bigo_mult7[intro!]
```
```   486 lemma bigo_mult8: "ALL x. f x ~= 0 ==>
```
```   487     O(f * g) = O(f::'a => ('b::linordered_field)) \<otimes> O(g)"
```
```   488 by (metis bigo_mult bigo_mult7 order_antisym_conv)
```
```   489
```
```   490 lemma bigo_minus [intro]: "f : O(g) ==> - f : O(g)"
```
```   491   by (auto simp add: bigo_def fun_Compl_def)
```
```   492
```
```   493 lemma bigo_minus2: "f : g +o O(h) ==> -f : -g +o O(h)"
```
```   494   apply (rule set_minus_imp_plus)
```
```   495   apply (drule set_plus_imp_minus)
```
```   496   apply (drule bigo_minus)
```
```   497   apply (simp add: diff_minus)
```
```   498 done
```
```   499
```
```   500 lemma bigo_minus3: "O(-f) = O(f)"
```
```   501   by (auto simp add: bigo_def fun_Compl_def abs_minus_cancel)
```
```   502
```
```   503 lemma bigo_plus_absorb_lemma1: "f : O(g) ==> f +o O(g) <= O(g)"
```
```   504 proof -
```
```   505   assume a: "f : O(g)"
```
```   506   show "f +o O(g) <= O(g)"
```
```   507   proof -
```
```   508     have "f : O(f)" by auto
```
```   509     then have "f +o O(g) <= O(f) \<oplus> O(g)"
```
```   510       by (auto del: subsetI)
```
```   511     also have "... <= O(g) \<oplus> O(g)"
```
```   512     proof -
```
```   513       from a have "O(f) <= O(g)" by (auto del: subsetI)
```
```   514       thus ?thesis by (auto del: subsetI)
```
```   515     qed
```
```   516     also have "... <= O(g)" by (simp add: bigo_plus_idemp)
```
```   517     finally show ?thesis .
```
```   518   qed
```
```   519 qed
```
```   520
```
```   521 lemma bigo_plus_absorb_lemma2: "f : O(g) ==> O(g) <= f +o O(g)"
```
```   522 proof -
```
```   523   assume a: "f : O(g)"
```
```   524   show "O(g) <= f +o O(g)"
```
```   525   proof -
```
```   526     from a have "-f : O(g)" by auto
```
```   527     then have "-f +o O(g) <= O(g)" by (elim bigo_plus_absorb_lemma1)
```
```   528     then have "f +o (-f +o O(g)) <= f +o O(g)" by auto
```
```   529     also have "f +o (-f +o O(g)) = O(g)"
```
```   530       by (simp add: set_plus_rearranges)
```
```   531     finally show ?thesis .
```
```   532   qed
```
```   533 qed
```
```   534
```
```   535 declare [[ sledgehammer_problem_prefix = "BigO__bigo_plus_absorb" ]]
```
```   536 lemma bigo_plus_absorb [simp]: "f : O(g) ==> f +o O(g) = O(g)"
```
```   537 by (metis bigo_plus_absorb_lemma1 bigo_plus_absorb_lemma2 order_eq_iff);
```
```   538
```
```   539 lemma bigo_plus_absorb2 [intro]: "f : O(g) ==> A <= O(g) ==> f +o A <= O(g)"
```
```   540   apply (subgoal_tac "f +o A <= f +o O(g)")
```
```   541   apply force+
```
```   542 done
```
```   543
```
```   544 lemma bigo_add_commute_imp: "f : g +o O(h) ==> g : f +o O(h)"
```
```   545   apply (subst set_minus_plus [symmetric])
```
```   546   apply (subgoal_tac "g - f = - (f - g)")
```
```   547   apply (erule ssubst)
```
```   548   apply (rule bigo_minus)
```
```   549   apply (subst set_minus_plus)
```
```   550   apply assumption
```
```   551   apply  (simp add: diff_minus add_ac)
```
```   552 done
```
```   553
```
```   554 lemma bigo_add_commute: "(f : g +o O(h)) = (g : f +o O(h))"
```
```   555   apply (rule iffI)
```
```   556   apply (erule bigo_add_commute_imp)+
```
```   557 done
```
```   558
```
```   559 lemma bigo_const1: "(%x. c) : O(%x. 1)"
```
```   560 by (auto simp add: bigo_def mult_ac)
```
```   561
```
```   562 declare [[ sledgehammer_problem_prefix = "BigO__bigo_const2" ]]
```
```   563 lemma (*bigo_const2 [intro]:*) "O(%x. c) <= O(%x. 1)"
```
```   564 by (metis bigo_const1 bigo_elt_subset);
```
```   565
```
```   566 lemma bigo_const2 [intro]: "O(%x. c::'b::linordered_idom) <= O(%x. 1)";
```
```   567 (* "thus" had to be replaced by "show" with an explicit reference to "F1" *)
```
```   568 proof -
```
```   569   have F1: "\<forall>u. (\<lambda>Q. u) \<in> O(\<lambda>Q. 1)" by (metis bigo_const1)
```
```   570   show "O(\<lambda>x. c) \<subseteq> O(\<lambda>x. 1)" by (metis F1 bigo_elt_subset)
```
```   571 qed
```
```   572
```
```   573 declare [[ sledgehammer_problem_prefix = "BigO__bigo_const3" ]]
```
```   574 lemma bigo_const3: "(c::'a::linordered_field) ~= 0 ==> (%x. 1) : O(%x. c)"
```
```   575 apply (simp add: bigo_def)
```
```   576 by (metis abs_eq_0 left_inverse order_refl)
```
```   577
```
```   578 lemma bigo_const4: "(c::'a::linordered_field) ~= 0 ==> O(%x. 1) <= O(%x. c)"
```
```   579 by (rule bigo_elt_subset, rule bigo_const3, assumption)
```
```   580
```
```   581 lemma bigo_const [simp]: "(c::'a::linordered_field) ~= 0 ==>
```
```   582     O(%x. c) = O(%x. 1)"
```
```   583 by (rule equalityI, rule bigo_const2, rule bigo_const4, assumption)
```
```   584
```
```   585 declare [[ sledgehammer_problem_prefix = "BigO__bigo_const_mult1" ]]
```
```   586 lemma bigo_const_mult1: "(%x. c * f x) : O(f)"
```
```   587   apply (simp add: bigo_def abs_mult)
```
```   588 by (metis le_less)
```
```   589
```
```   590 lemma bigo_const_mult2: "O(%x. c * f x) <= O(f)"
```
```   591 by (rule bigo_elt_subset, rule bigo_const_mult1)
```
```   592
```
```   593 declare [[ sledgehammer_problem_prefix = "BigO__bigo_const_mult3" ]]
```
```   594 lemma bigo_const_mult3: "(c::'a::linordered_field) ~= 0 ==> f : O(%x. c * f x)"
```
```   595   apply (simp add: bigo_def)
```
```   596 (*sledgehammer [no luck]*)
```
```   597   apply (rule_tac x = "abs(inverse c)" in exI)
```
```   598   apply (simp only: abs_mult [symmetric] mult_assoc [symmetric])
```
```   599 apply (subst left_inverse)
```
```   600 apply (auto );
```
```   601 done
```
```   602
```
```   603 lemma bigo_const_mult4: "(c::'a::linordered_field) ~= 0 ==>
```
```   604     O(f) <= O(%x. c * f x)"
```
```   605 by (rule bigo_elt_subset, rule bigo_const_mult3, assumption)
```
```   606
```
```   607 lemma bigo_const_mult [simp]: "(c::'a::linordered_field) ~= 0 ==>
```
```   608     O(%x. c * f x) = O(f)"
```
```   609 by (rule equalityI, rule bigo_const_mult2, erule bigo_const_mult4)
```
```   610
```
```   611 declare [[ sledgehammer_problem_prefix = "BigO__bigo_const_mult5" ]]
```
```   612 lemma bigo_const_mult5 [simp]: "(c::'a::linordered_field) ~= 0 ==>
```
```   613     (%x. c) *o O(f) = O(f)"
```
```   614   apply (auto del: subsetI)
```
```   615   apply (rule order_trans)
```
```   616   apply (rule bigo_mult2)
```
```   617   apply (simp add: func_times)
```
```   618   apply (auto intro!: subsetI simp add: bigo_def elt_set_times_def func_times)
```
```   619   apply (rule_tac x = "%y. inverse c * x y" in exI)
```
```   620   apply (rename_tac g d)
```
```   621   apply safe
```
```   622   apply (rule_tac [2] ext)
```
```   623    prefer 2
```
```   624    apply simp
```
```   625   apply (simp add: mult_assoc [symmetric] abs_mult)
```
```   626   (* couldn't get this proof without the step above *)
```
```   627 proof -
```
```   628   fix g :: "'b \<Rightarrow> 'a" and d :: 'a
```
```   629   assume A1: "c \<noteq> (0\<Colon>'a)"
```
```   630   assume A2: "\<forall>x\<Colon>'b. \<bar>g x\<bar> \<le> d * \<bar>f x\<bar>"
```
```   631   have F1: "inverse \<bar>c\<bar> = \<bar>inverse c\<bar>" using A1 by (metis nonzero_abs_inverse)
```
```   632   have F2: "(0\<Colon>'a) < \<bar>c\<bar>" using A1 by (metis zero_less_abs_iff)
```
```   633   have "(0\<Colon>'a) < \<bar>c\<bar> \<longrightarrow> (0\<Colon>'a) < \<bar>inverse c\<bar>" using F1 by (metis positive_imp_inverse_positive)
```
```   634   hence "(0\<Colon>'a) < \<bar>inverse c\<bar>" using F2 by metis
```
```   635   hence F3: "(0\<Colon>'a) \<le> \<bar>inverse c\<bar>" by (metis order_le_less)
```
```   636   have "\<exists>(u\<Colon>'a) SKF\<^isub>7\<Colon>'a \<Rightarrow> 'b. \<bar>g (SKF\<^isub>7 (\<bar>inverse c\<bar> * u))\<bar> \<le> u * \<bar>f (SKF\<^isub>7 (\<bar>inverse c\<bar> * u))\<bar>"
```
```   637     using A2 by metis
```
```   638   hence F4: "\<exists>(u\<Colon>'a) SKF\<^isub>7\<Colon>'a \<Rightarrow> 'b. \<bar>g (SKF\<^isub>7 (\<bar>inverse c\<bar> * u))\<bar> \<le> u * \<bar>f (SKF\<^isub>7 (\<bar>inverse c\<bar> * u))\<bar> \<and> (0\<Colon>'a) \<le> \<bar>inverse c\<bar>"
```
```   639     using F3 by metis
```
```   640   hence "\<exists>(v\<Colon>'a) (u\<Colon>'a) SKF\<^isub>7\<Colon>'a \<Rightarrow> 'b. \<bar>inverse c\<bar> * \<bar>g (SKF\<^isub>7 (u * v))\<bar> \<le> u * (v * \<bar>f (SKF\<^isub>7 (u * v))\<bar>)"
```
```   641     by (metis comm_mult_left_mono)
```
```   642   thus "\<exists>ca\<Colon>'a. \<forall>x\<Colon>'b. \<bar>inverse c\<bar> * \<bar>g x\<bar> \<le> ca * \<bar>f x\<bar>"
```
```   643     using A2 F4 by (metis ab_semigroup_mult_class.mult_ac(1) comm_mult_left_mono)
```
```   644 qed
```
```   645
```
```   646
```
```   647 declare [[ sledgehammer_problem_prefix = "BigO__bigo_const_mult6" ]]
```
```   648 lemma bigo_const_mult6 [intro]: "(%x. c) *o O(f) <= O(f)"
```
```   649   apply (auto intro!: subsetI
```
```   650     simp add: bigo_def elt_set_times_def func_times
```
```   651     simp del: abs_mult mult_ac)
```
```   652 (*sledgehammer*);
```
```   653   apply (rule_tac x = "ca * (abs c)" in exI)
```
```   654   apply (rule allI)
```
```   655   apply (subgoal_tac "ca * abs(c) * abs(f x) = abs(c) * (ca * abs(f x))")
```
```   656   apply (erule ssubst)
```
```   657   apply (subst abs_mult)
```
```   658   apply (rule mult_left_mono)
```
```   659   apply (erule spec)
```
```   660   apply simp
```
```   661   apply(simp add: mult_ac)
```
```   662 done
```
```   663
```
```   664 lemma bigo_const_mult7 [intro]: "f =o O(g) ==> (%x. c * f x) =o O(g)"
```
```   665 proof -
```
```   666   assume "f =o O(g)"
```
```   667   then have "(%x. c) * f =o (%x. c) *o O(g)"
```
```   668     by auto
```
```   669   also have "(%x. c) * f = (%x. c * f x)"
```
```   670     by (simp add: func_times)
```
```   671   also have "(%x. c) *o O(g) <= O(g)"
```
```   672     by (auto del: subsetI)
```
```   673   finally show ?thesis .
```
```   674 qed
```
```   675
```
```   676 lemma bigo_compose1: "f =o O(g) ==> (%x. f(k x)) =o O(%x. g(k x))"
```
```   677 by (unfold bigo_def, auto)
```
```   678
```
```   679 lemma bigo_compose2: "f =o g +o O(h) ==> (%x. f(k x)) =o (%x. g(k x)) +o
```
```   680     O(%x. h(k x))"
```
```   681   apply (simp only: set_minus_plus [symmetric] diff_minus fun_Compl_def
```
```   682       func_plus)
```
```   683   apply (erule bigo_compose1)
```
```   684 done
```
```   685
```
```   686 subsection {* Setsum *}
```
```   687
```
```   688 lemma bigo_setsum_main: "ALL x. ALL y : A x. 0 <= h x y ==>
```
```   689     EX c. ALL x. ALL y : A x. abs(f x y) <= c * (h x y) ==>
```
```   690       (%x. SUM y : A x. f x y) =o O(%x. SUM y : A x. h x y)"
```
```   691   apply (auto simp add: bigo_def)
```
```   692   apply (rule_tac x = "abs c" in exI)
```
```   693   apply (subst abs_of_nonneg) back back
```
```   694   apply (rule setsum_nonneg)
```
```   695   apply force
```
```   696   apply (subst setsum_right_distrib)
```
```   697   apply (rule allI)
```
```   698   apply (rule order_trans)
```
```   699   apply (rule setsum_abs)
```
```   700   apply (rule setsum_mono)
```
```   701 apply (blast intro: order_trans mult_right_mono abs_ge_self)
```
```   702 done
```
```   703
```
```   704 declare [[ sledgehammer_problem_prefix = "BigO__bigo_setsum1" ]]
```
```   705 lemma bigo_setsum1: "ALL x y. 0 <= h x y ==>
```
```   706     EX c. ALL x y. abs(f x y) <= c * (h x y) ==>
```
```   707       (%x. SUM y : A x. f x y) =o O(%x. SUM y : A x. h x y)"
```
```   708   apply (rule bigo_setsum_main)
```
```   709 (*sledgehammer*);
```
```   710   apply force
```
```   711   apply clarsimp
```
```   712   apply (rule_tac x = c in exI)
```
```   713   apply force
```
```   714 done
```
```   715
```
```   716 lemma bigo_setsum2: "ALL y. 0 <= h y ==>
```
```   717     EX c. ALL y. abs(f y) <= c * (h y) ==>
```
```   718       (%x. SUM y : A x. f y) =o O(%x. SUM y : A x. h y)"
```
```   719 by (rule bigo_setsum1, auto)
```
```   720
```
```   721 declare [[ sledgehammer_problem_prefix = "BigO__bigo_setsum3" ]]
```
```   722 lemma bigo_setsum3: "f =o O(h) ==>
```
```   723     (%x. SUM y : A x. (l x y) * f(k x y)) =o
```
```   724       O(%x. SUM y : A x. abs(l x y * h(k x y)))"
```
```   725   apply (rule bigo_setsum1)
```
```   726   apply (rule allI)+
```
```   727   apply (rule abs_ge_zero)
```
```   728   apply (unfold bigo_def)
```
```   729   apply (auto simp add: abs_mult);
```
```   730 (*sledgehammer*);
```
```   731   apply (rule_tac x = c in exI)
```
```   732   apply (rule allI)+
```
```   733   apply (subst mult_left_commute)
```
```   734   apply (rule mult_left_mono)
```
```   735   apply (erule spec)
```
```   736   apply (rule abs_ge_zero)
```
```   737 done
```
```   738
```
```   739 lemma bigo_setsum4: "f =o g +o O(h) ==>
```
```   740     (%x. SUM y : A x. l x y * f(k x y)) =o
```
```   741       (%x. SUM y : A x. l x y * g(k x y)) +o
```
```   742         O(%x. SUM y : A x. abs(l x y * h(k x y)))"
```
```   743   apply (rule set_minus_imp_plus)
```
```   744   apply (subst fun_diff_def)
```
```   745   apply (subst setsum_subtractf [symmetric])
```
```   746   apply (subst right_diff_distrib [symmetric])
```
```   747   apply (rule bigo_setsum3)
```
```   748   apply (subst fun_diff_def [symmetric])
```
```   749   apply (erule set_plus_imp_minus)
```
```   750 done
```
```   751
```
```   752 declare [[ sledgehammer_problem_prefix = "BigO__bigo_setsum5" ]]
```
```   753 lemma bigo_setsum5: "f =o O(h) ==> ALL x y. 0 <= l x y ==>
```
```   754     ALL x. 0 <= h x ==>
```
```   755       (%x. SUM y : A x. (l x y) * f(k x y)) =o
```
```   756         O(%x. SUM y : A x. (l x y) * h(k x y))"
```
```   757   apply (subgoal_tac "(%x. SUM y : A x. (l x y) * h(k x y)) =
```
```   758       (%x. SUM y : A x. abs((l x y) * h(k x y)))")
```
```   759   apply (erule ssubst)
```
```   760   apply (erule bigo_setsum3)
```
```   761   apply (rule ext)
```
```   762   apply (rule setsum_cong2)
```
```   763   apply (thin_tac "f \<in> O(h)")
```
```   764 apply (metis abs_of_nonneg zero_le_mult_iff)
```
```   765 done
```
```   766
```
```   767 lemma bigo_setsum6: "f =o g +o O(h) ==> ALL x y. 0 <= l x y ==>
```
```   768     ALL x. 0 <= h x ==>
```
```   769       (%x. SUM y : A x. (l x y) * f(k x y)) =o
```
```   770         (%x. SUM y : A x. (l x y) * g(k x y)) +o
```
```   771           O(%x. SUM y : A x. (l x y) * h(k x y))"
```
```   772   apply (rule set_minus_imp_plus)
```
```   773   apply (subst fun_diff_def)
```
```   774   apply (subst setsum_subtractf [symmetric])
```
```   775   apply (subst right_diff_distrib [symmetric])
```
```   776   apply (rule bigo_setsum5)
```
```   777   apply (subst fun_diff_def [symmetric])
```
```   778   apply (drule set_plus_imp_minus)
```
```   779   apply auto
```
```   780 done
```
```   781
```
```   782 subsection {* Misc useful stuff *}
```
```   783
```
```   784 lemma bigo_useful_intro: "A <= O(f) ==> B <= O(f) ==>
```
```   785   A \<oplus> B <= O(f)"
```
```   786   apply (subst bigo_plus_idemp [symmetric])
```
```   787   apply (rule set_plus_mono2)
```
```   788   apply assumption+
```
```   789 done
```
```   790
```
```   791 lemma bigo_useful_add: "f =o O(h) ==> g =o O(h) ==> f + g =o O(h)"
```
```   792   apply (subst bigo_plus_idemp [symmetric])
```
```   793   apply (rule set_plus_intro)
```
```   794   apply assumption+
```
```   795 done
```
```   796
```
```   797 lemma bigo_useful_const_mult: "(c::'a::linordered_field) ~= 0 ==>
```
```   798     (%x. c) * f =o O(h) ==> f =o O(h)"
```
```   799   apply (rule subsetD)
```
```   800   apply (subgoal_tac "(%x. 1 / c) *o O(h) <= O(h)")
```
```   801   apply assumption
```
```   802   apply (rule bigo_const_mult6)
```
```   803   apply (subgoal_tac "f = (%x. 1 / c) * ((%x. c) * f)")
```
```   804   apply (erule ssubst)
```
```   805   apply (erule set_times_intro2)
```
```   806   apply (simp add: func_times)
```
```   807 done
```
```   808
```
```   809 declare [[ sledgehammer_problem_prefix = "BigO__bigo_fix" ]]
```
```   810 lemma bigo_fix: "(%x. f ((x::nat) + 1)) =o O(%x. h(x + 1)) ==> f 0 = 0 ==>
```
```   811     f =o O(h)"
```
```   812   apply (simp add: bigo_alt_def)
```
```   813 (*sledgehammer*);
```
```   814   apply clarify
```
```   815   apply (rule_tac x = c in exI)
```
```   816   apply safe
```
```   817   apply (case_tac "x = 0")
```
```   818 apply (metis abs_ge_zero  abs_zero  order_less_le  split_mult_pos_le)
```
```   819   apply (subgoal_tac "x = Suc (x - 1)")
```
```   820   apply metis
```
```   821   apply simp
```
```   822   done
```
```   823
```
```   824
```
```   825 lemma bigo_fix2:
```
```   826     "(%x. f ((x::nat) + 1)) =o (%x. g(x + 1)) +o O(%x. h(x + 1)) ==>
```
```   827        f 0 = g 0 ==> f =o g +o O(h)"
```
```   828   apply (rule set_minus_imp_plus)
```
```   829   apply (rule bigo_fix)
```
```   830   apply (subst fun_diff_def)
```
```   831   apply (subst fun_diff_def [symmetric])
```
```   832   apply (rule set_plus_imp_minus)
```
```   833   apply simp
```
```   834   apply (simp add: fun_diff_def)
```
```   835 done
```
```   836
```
```   837 subsection {* Less than or equal to *}
```
```   838
```
```   839 definition lesso :: "('a => 'b::linordered_idom) => ('a => 'b) => ('a => 'b)" (infixl "<o" 70) where
```
```   840   "f <o g == (%x. max (f x - g x) 0)"
```
```   841
```
```   842 lemma bigo_lesseq1: "f =o O(h) ==> ALL x. abs (g x) <= abs (f x) ==>
```
```   843     g =o O(h)"
```
```   844   apply (unfold bigo_def)
```
```   845   apply clarsimp
```
```   846 apply (blast intro: order_trans)
```
```   847 done
```
```   848
```
```   849 lemma bigo_lesseq2: "f =o O(h) ==> ALL x. abs (g x) <= f x ==>
```
```   850       g =o O(h)"
```
```   851   apply (erule bigo_lesseq1)
```
```   852 apply (blast intro: abs_ge_self order_trans)
```
```   853 done
```
```   854
```
```   855 lemma bigo_lesseq3: "f =o O(h) ==> ALL x. 0 <= g x ==> ALL x. g x <= f x ==>
```
```   856       g =o O(h)"
```
```   857   apply (erule bigo_lesseq2)
```
```   858   apply (rule allI)
```
```   859   apply (subst abs_of_nonneg)
```
```   860   apply (erule spec)+
```
```   861 done
```
```   862
```
```   863 lemma bigo_lesseq4: "f =o O(h) ==>
```
```   864     ALL x. 0 <= g x ==> ALL x. g x <= abs (f x) ==>
```
```   865       g =o O(h)"
```
```   866   apply (erule bigo_lesseq1)
```
```   867   apply (rule allI)
```
```   868   apply (subst abs_of_nonneg)
```
```   869   apply (erule spec)+
```
```   870 done
```
```   871
```
```   872 declare [[ sledgehammer_problem_prefix = "BigO__bigo_lesso1" ]]
```
```   873 lemma bigo_lesso1: "ALL x. f x <= g x ==> f <o g =o O(h)"
```
```   874 apply (unfold lesso_def)
```
```   875 apply (subgoal_tac "(%x. max (f x - g x) 0) = 0")
```
```   876 proof -
```
```   877   assume "(\<lambda>x. max (f x - g x) 0) = 0"
```
```   878   thus "(\<lambda>x. max (f x - g x) 0) \<in> O(h)" by (metis bigo_zero)
```
```   879 next
```
```   880   show "\<forall>x\<Colon>'a. f x \<le> g x \<Longrightarrow> (\<lambda>x\<Colon>'a. max (f x - g x) (0\<Colon>'b)) = (0\<Colon>'a \<Rightarrow> 'b)"
```
```   881   apply (unfold func_zero)
```
```   882   apply (rule ext)
```
```   883   by (simp split: split_max)
```
```   884 qed
```
```   885
```
```   886 declare [[ sledgehammer_problem_prefix = "BigO__bigo_lesso2" ]]
```
```   887 lemma bigo_lesso2: "f =o g +o O(h) ==>
```
```   888     ALL x. 0 <= k x ==> ALL x. k x <= f x ==>
```
```   889       k <o g =o O(h)"
```
```   890   apply (unfold lesso_def)
```
```   891   apply (rule bigo_lesseq4)
```
```   892   apply (erule set_plus_imp_minus)
```
```   893   apply (rule allI)
```
```   894   apply (rule le_maxI2)
```
```   895   apply (rule allI)
```
```   896   apply (subst fun_diff_def)
```
```   897 apply (erule thin_rl)
```
```   898 (*sledgehammer*);
```
```   899   apply (case_tac "0 <= k x - g x")
```
```   900 (* apply (metis abs_le_iff add_le_imp_le_right diff_minus le_less
```
```   901                 le_max_iff_disj min_max.le_supE min_max.sup_absorb2
```
```   902                 min_max.sup_commute) *)
```
```   903 proof -
```
```   904   fix x :: 'a
```
```   905   assume "\<forall>x\<Colon>'a. k x \<le> f x"
```
```   906   hence F1: "\<forall>x\<^isub>1\<Colon>'a. max (k x\<^isub>1) (f x\<^isub>1) = f x\<^isub>1" by (metis min_max.sup_absorb2)
```
```   907   assume "(0\<Colon>'b) \<le> k x - g x"
```
```   908   hence F2: "max (0\<Colon>'b) (k x - g x) = k x - g x" by (metis min_max.sup_absorb2)
```
```   909   have F3: "\<forall>x\<^isub>1\<Colon>'b. x\<^isub>1 \<le> \<bar>x\<^isub>1\<bar>" by (metis abs_le_iff le_less)
```
```   910   have "\<forall>(x\<^isub>2\<Colon>'b) x\<^isub>1\<Colon>'b. max x\<^isub>1 x\<^isub>2 \<le> x\<^isub>2 \<or> max x\<^isub>1 x\<^isub>2 \<le> x\<^isub>1" by (metis le_less le_max_iff_disj)
```
```   911   hence "\<forall>(x\<^isub>3\<Colon>'b) (x\<^isub>2\<Colon>'b) x\<^isub>1\<Colon>'b. x\<^isub>1 - x\<^isub>2 \<le> x\<^isub>3 - x\<^isub>2 \<or> x\<^isub>3 \<le> x\<^isub>1" by (metis add_le_imp_le_right diff_minus min_max.le_supE)
```
```   912   hence "k x - g x \<le> f x - g x" by (metis F1 le_less min_max.sup_absorb2 min_max.sup_commute)
```
```   913   hence "k x - g x \<le> \<bar>f x - g x\<bar>" by (metis F3 le_max_iff_disj min_max.sup_absorb2)
```
```   914   thus "max (k x - g x) (0\<Colon>'b) \<le> \<bar>f x - g x\<bar>" by (metis F2 min_max.sup_commute)
```
```   915 next
```
```   916   show "\<And>x\<Colon>'a.
```
```   917        \<lbrakk>\<forall>x\<Colon>'a. (0\<Colon>'b) \<le> k x; \<forall>x\<Colon>'a. k x \<le> f x; \<not> (0\<Colon>'b) \<le> k x - g x\<rbrakk>
```
```   918        \<Longrightarrow> max (k x - g x) (0\<Colon>'b) \<le> \<bar>f x - g x\<bar>"
```
```   919     by (metis abs_ge_zero le_cases min_max.sup_absorb2)
```
```   920 qed
```
```   921
```
```   922 declare [[ sledgehammer_problem_prefix = "BigO__bigo_lesso3" ]]
```
```   923 lemma bigo_lesso3: "f =o g +o O(h) ==>
```
```   924     ALL x. 0 <= k x ==> ALL x. g x <= k x ==>
```
```   925       f <o k =o O(h)"
```
```   926   apply (unfold lesso_def)
```
```   927   apply (rule bigo_lesseq4)
```
```   928   apply (erule set_plus_imp_minus)
```
```   929   apply (rule allI)
```
```   930   apply (rule le_maxI2)
```
```   931   apply (rule allI)
```
```   932   apply (subst fun_diff_def)
```
```   933 apply (erule thin_rl)
```
```   934 (*sledgehammer*);
```
```   935   apply (case_tac "0 <= f x - k x")
```
```   936   apply (simp)
```
```   937   apply (subst abs_of_nonneg)
```
```   938   apply (drule_tac x = x in spec) back
```
```   939 using [[ sledgehammer_problem_prefix = "BigO__bigo_lesso3_simpler" ]]
```
```   940 apply (metis diff_less_0_iff_less linorder_not_le not_leE uminus_add_conv_diff xt1(12) xt1(6))
```
```   941 apply (metis add_minus_cancel diff_le_eq le_diff_eq uminus_add_conv_diff)
```
```   942 apply (metis abs_ge_zero linorder_linear min_max.sup_absorb1 min_max.sup_commute)
```
```   943 done
```
```   944
```
```   945 lemma bigo_lesso4: "f <o g =o O(k::'a=>'b::linordered_field) ==>
```
```   946     g =o h +o O(k) ==> f <o h =o O(k)"
```
```   947   apply (unfold lesso_def)
```
```   948   apply (drule set_plus_imp_minus)
```
```   949   apply (drule bigo_abs5) back
```
```   950   apply (simp add: fun_diff_def)
```
```   951   apply (drule bigo_useful_add)
```
```   952   apply assumption
```
```   953   apply (erule bigo_lesseq2) back
```
```   954   apply (rule allI)
```
```   955   apply (auto simp add: func_plus fun_diff_def algebra_simps
```
```   956     split: split_max abs_split)
```
```   957 done
```
```   958
```
```   959 declare [[ sledgehammer_problem_prefix = "BigO__bigo_lesso5" ]]
```
```   960 lemma bigo_lesso5: "f <o g =o O(h) ==>
```
```   961     EX C. ALL x. f x <= g x + C * abs(h x)"
```
```   962   apply (simp only: lesso_def bigo_alt_def)
```
```   963   apply clarsimp
```
```   964   apply (metis abs_if abs_mult add_commute diff_le_eq less_not_permute)
```
```   965 done
```
```   966
```
```   967 end
```