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