src/HOL/MetisExamples/BigO.thy
author wenzelm
Mon Mar 16 18:24:30 2009 +0100 (2009-03-16)
changeset 30549 d2d7874648bd
parent 29823 0ab754d13ccd
child 32864 a226f29d4bdc
permissions -rw-r--r--
simplified method setup;
paulson@23449
     1
(*  Title:      HOL/MetisExamples/BigO.thy
paulson@23449
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@23449
     3
paulson@23449
     4
Testing the metis method
paulson@23449
     5
*)
paulson@23449
     6
paulson@23449
     7
header {* Big O notation *}
paulson@23449
     8
paulson@23449
     9
theory BigO
haftmann@29823
    10
imports "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Main SetsAndFunctions 
paulson@23449
    11
begin
paulson@23449
    12
paulson@23449
    13
subsection {* Definitions *}
paulson@23449
    14
haftmann@29511
    15
definition bigo :: "('a => 'b::ordered_idom) => ('a => 'b) set"    ("(1O'(_'))") where
paulson@23449
    16
  "O(f::('a => 'b)) ==   {h. EX c. ALL x. abs (h x) <= c * abs (f x)}"
paulson@23449
    17
wenzelm@28592
    18
ML_command{*AtpWrapper.problem_name := "BigO__bigo_pos_const"*}
paulson@23449
    19
lemma bigo_pos_const: "(EX (c::'a::ordered_idom). 
paulson@23449
    20
    ALL x. (abs (h x)) <= (c * (abs (f x))))
paulson@23449
    21
      = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
paulson@23449
    22
  apply auto
paulson@23449
    23
  apply (case_tac "c = 0", simp)
paulson@23449
    24
  apply (rule_tac x = "1" in exI, simp)
haftmann@25304
    25
  apply (rule_tac x = "abs c" in exI, auto)
haftmann@25304
    26
  apply (metis abs_ge_minus_self abs_ge_zero abs_minus_cancel abs_of_nonneg equation_minus_iff Orderings.xt1(6) abs_mult)
paulson@23449
    27
  done
paulson@23449
    28
paulson@23449
    29
(*** Now various verions with an increasing modulus ***)
paulson@23449
    30
paulson@26333
    31
declare [[sledgehammer_modulus = 1]]
paulson@23449
    32
wenzelm@26312
    33
lemma (*bigo_pos_const:*) "(EX (c::'a::ordered_idom). 
paulson@23449
    34
    ALL x. (abs (h x)) <= (c * (abs (f x))))
paulson@23449
    35
      = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
paulson@23449
    36
  apply auto
paulson@23449
    37
  apply (case_tac "c = 0", simp)
paulson@23449
    38
  apply (rule_tac x = "1" in exI, simp)
paulson@23449
    39
  apply (rule_tac x = "abs c" in exI, auto)
paulson@23449
    40
proof (neg_clausify)
paulson@23449
    41
fix c x
paulson@24937
    42
have 0: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom. \<bar>X1 * X2\<bar> = \<bar>X2 * X1\<bar>"
paulson@24937
    43
  by (metis abs_mult mult_commute)
paulson@24937
    44
have 1: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom.
paulson@24937
    45
   X1 \<le> (0\<Colon>'a\<Colon>ordered_idom) \<or> \<bar>X2\<bar> * X1 = \<bar>X2 * X1\<bar>"
paulson@24937
    46
  by (metis abs_mult_pos linorder_linear)
paulson@24937
    47
have 2: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom.
paulson@24937
    48
   \<not> (0\<Colon>'a\<Colon>ordered_idom) < X1 * X2 \<or>
paulson@24937
    49
   \<not> (0\<Colon>'a\<Colon>ordered_idom) \<le> X2 \<or> \<not> X1 \<le> (0\<Colon>'a\<Colon>ordered_idom)"
paulson@24937
    50
  by (metis linorder_not_less mult_nonneg_nonpos2)
paulson@24937
    51
assume 3: "\<And>x\<Colon>'b\<Colon>type.
paulson@24937
    52
   \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar>
paulson@24937
    53
   \<le> (c\<Colon>'a\<Colon>ordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar>"
paulson@24937
    54
assume 4: "\<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) (x\<Colon>'b\<Colon>type)\<bar>
paulson@24937
    55
  \<le> \<bar>c\<Colon>'a\<Colon>ordered_idom\<bar> * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar>"
paulson@24937
    56
have 5: "\<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) (x\<Colon>'b\<Colon>type)\<bar>
paulson@24937
    57
  \<le> \<bar>(c\<Colon>'a\<Colon>ordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar>"
paulson@24937
    58
  by (metis 4 abs_mult)
paulson@24937
    59
have 6: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom.
paulson@24937
    60
   \<not> X1 \<le> (0\<Colon>'a\<Colon>ordered_idom) \<or> X1 \<le> \<bar>X2\<bar>"
paulson@24937
    61
  by (metis abs_ge_zero xt1(6))
paulson@24937
    62
have 7: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom.
paulson@24937
    63
   X1 \<le> \<bar>X2\<bar> \<or> (0\<Colon>'a\<Colon>ordered_idom) < X1"
paulson@24937
    64
  by (metis not_leE 6)
paulson@24937
    65
have 8: "(0\<Colon>'a\<Colon>ordered_idom) < \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) (x\<Colon>'b\<Colon>type)\<bar>"
paulson@24937
    66
  by (metis 5 7)
paulson@24937
    67
have 9: "\<And>X1\<Colon>'a\<Colon>ordered_idom.
paulson@24937
    68
   \<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) (x\<Colon>'b\<Colon>type)\<bar> \<le> X1 \<or>
paulson@24937
    69
   (0\<Colon>'a\<Colon>ordered_idom) < X1"
paulson@24937
    70
  by (metis 8 order_less_le_trans)
paulson@24937
    71
have 10: "(0\<Colon>'a\<Colon>ordered_idom)
paulson@24937
    72
< (c\<Colon>'a\<Colon>ordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) (x\<Colon>'b\<Colon>type)\<bar>"
paulson@24937
    73
  by (metis 3 9)
paulson@24937
    74
have 11: "\<not> (c\<Colon>'a\<Colon>ordered_idom) \<le> (0\<Colon>'a\<Colon>ordered_idom)"
paulson@24937
    75
  by (metis abs_ge_zero 2 10)
paulson@24937
    76
have 12: "\<And>X1\<Colon>'a\<Colon>ordered_idom. (c\<Colon>'a\<Colon>ordered_idom) * \<bar>X1\<bar> = \<bar>X1 * c\<bar>"
paulson@24937
    77
  by (metis mult_commute 1 11)
paulson@24937
    78
have 13: "\<And>X1\<Colon>'b\<Colon>type.
paulson@24937
    79
   - (h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X1
paulson@24937
    80
   \<le> (c\<Colon>'a\<Colon>ordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X1\<bar>"
paulson@24937
    81
  by (metis 3 abs_le_D2)
paulson@24937
    82
have 14: "\<And>X1\<Colon>'b\<Colon>type.
paulson@24937
    83
   - (h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X1
paulson@24937
    84
   \<le> \<bar>(c\<Colon>'a\<Colon>ordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X1\<bar>"
paulson@24937
    85
  by (metis 0 12 13)
paulson@24937
    86
have 15: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom. \<bar>X1 * \<bar>X2\<bar>\<bar> = \<bar>X1 * X2\<bar>"
paulson@24937
    87
  by (metis abs_mult abs_mult_pos abs_ge_zero)
paulson@24937
    88
have 16: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom. X1 \<le> \<bar>X2\<bar> \<or> \<not> X1 \<le> X2"
paulson@24937
    89
  by (metis xt1(6) abs_ge_self)
paulson@24937
    90
have 17: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom. \<not> \<bar>X1\<bar> \<le> X2 \<or> X1 \<le> \<bar>X2\<bar>"
paulson@24937
    91
  by (metis 16 abs_le_D1)
paulson@24937
    92
have 18: "\<And>X1\<Colon>'b\<Colon>type.
paulson@24937
    93
   (h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X1
paulson@24937
    94
   \<le> \<bar>(c\<Colon>'a\<Colon>ordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X1\<bar>"
paulson@24937
    95
  by (metis 17 3 15)
paulson@23449
    96
show "False"
paulson@24937
    97
  by (metis abs_le_iff 5 18 14)
paulson@23449
    98
qed
paulson@23449
    99
paulson@26333
   100
declare [[sledgehammer_modulus = 2]]
paulson@25710
   101
paulson@23449
   102
lemma (*bigo_pos_const:*) "(EX (c::'a::ordered_idom). 
paulson@23449
   103
    ALL x. (abs (h x)) <= (c * (abs (f x))))
paulson@23449
   104
      = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
paulson@23449
   105
  apply auto
paulson@23449
   106
  apply (case_tac "c = 0", simp)
paulson@23449
   107
  apply (rule_tac x = "1" in exI, simp)
paulson@23449
   108
  apply (rule_tac x = "abs c" in exI, auto);
paulson@23449
   109
proof (neg_clausify)
paulson@23449
   110
fix c x
paulson@24937
   111
have 0: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom. \<bar>X1 * X2\<bar> = \<bar>X2 * X1\<bar>"
paulson@24937
   112
  by (metis abs_mult mult_commute)
paulson@24937
   113
assume 1: "\<And>x\<Colon>'b\<Colon>type.
paulson@24937
   114
   \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar>
paulson@24937
   115
   \<le> (c\<Colon>'a\<Colon>ordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar>"
paulson@24937
   116
assume 2: "\<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) (x\<Colon>'b\<Colon>type)\<bar>
paulson@24937
   117
  \<le> \<bar>c\<Colon>'a\<Colon>ordered_idom\<bar> * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar>"
paulson@24937
   118
have 3: "\<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) (x\<Colon>'b\<Colon>type)\<bar>
paulson@24937
   119
  \<le> \<bar>(c\<Colon>'a\<Colon>ordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar>"
paulson@24937
   120
  by (metis 2 abs_mult)
paulson@24937
   121
have 4: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom.
paulson@24937
   122
   \<not> X1 \<le> (0\<Colon>'a\<Colon>ordered_idom) \<or> X1 \<le> \<bar>X2\<bar>"
paulson@24937
   123
  by (metis abs_ge_zero xt1(6))
paulson@24937
   124
have 5: "(0\<Colon>'a\<Colon>ordered_idom) < \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) (x\<Colon>'b\<Colon>type)\<bar>"
paulson@24937
   125
  by (metis not_leE 4 3)
paulson@24937
   126
have 6: "(0\<Colon>'a\<Colon>ordered_idom)
paulson@24937
   127
< (c\<Colon>'a\<Colon>ordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) (x\<Colon>'b\<Colon>type)\<bar>"
paulson@24937
   128
  by (metis 1 order_less_le_trans 5)
paulson@24937
   129
have 7: "\<And>X1\<Colon>'a\<Colon>ordered_idom. (c\<Colon>'a\<Colon>ordered_idom) * \<bar>X1\<bar> = \<bar>X1 * c\<bar>"
paulson@24937
   130
  by (metis abs_ge_zero linorder_not_less mult_nonneg_nonpos2 6 linorder_linear abs_mult_pos mult_commute)
paulson@24937
   131
have 8: "\<And>X1\<Colon>'b\<Colon>type.
paulson@24937
   132
   - (h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X1
paulson@24937
   133
   \<le> \<bar>(c\<Colon>'a\<Colon>ordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X1\<bar>"
paulson@24937
   134
  by (metis 0 7 abs_le_D2 1)
paulson@24937
   135
have 9: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom. \<not> \<bar>X1\<bar> \<le> X2 \<or> X1 \<le> \<bar>X2\<bar>"
paulson@24937
   136
  by (metis abs_ge_self xt1(6) abs_le_D1)
paulson@23449
   137
show "False"
paulson@24937
   138
  by (metis 8 abs_ge_zero abs_mult_pos abs_mult 1 9 3 abs_le_iff)
paulson@23449
   139
qed
paulson@23449
   140
paulson@26333
   141
declare [[sledgehammer_modulus = 3]]
paulson@25710
   142
paulson@23449
   143
lemma (*bigo_pos_const:*) "(EX (c::'a::ordered_idom). 
paulson@23449
   144
    ALL x. (abs (h x)) <= (c * (abs (f x))))
paulson@23449
   145
      = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
paulson@23449
   146
  apply auto
paulson@23449
   147
  apply (case_tac "c = 0", simp)
paulson@23449
   148
  apply (rule_tac x = "1" in exI, simp)
paulson@23449
   149
  apply (rule_tac x = "abs c" in exI, auto);
paulson@23449
   150
proof (neg_clausify)
paulson@23449
   151
fix c x
paulson@24937
   152
assume 0: "\<And>x\<Colon>'b\<Colon>type.
paulson@24937
   153
   \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar>
paulson@24937
   154
   \<le> (c\<Colon>'a\<Colon>ordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar>"
paulson@24937
   155
assume 1: "\<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) (x\<Colon>'b\<Colon>type)\<bar>
paulson@23449
   156
  \<le> \<bar>c\<Colon>'a\<Colon>ordered_idom\<bar> * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) x\<bar>"
paulson@24937
   157
have 2: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom.
paulson@24937
   158
   X1 \<le> \<bar>X2\<bar> \<or> (0\<Colon>'a\<Colon>ordered_idom) < X1"
paulson@24937
   159
  by (metis abs_ge_zero xt1(6) not_leE)
paulson@24937
   160
have 3: "\<not> (c\<Colon>'a\<Colon>ordered_idom) \<le> (0\<Colon>'a\<Colon>ordered_idom)"
paulson@24937
   161
  by (metis abs_ge_zero mult_nonneg_nonpos2 linorder_not_less order_less_le_trans 1 abs_mult 2 0)
paulson@24937
   162
have 4: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom. \<bar>X1 * \<bar>X2\<bar>\<bar> = \<bar>X1 * X2\<bar>"
paulson@24937
   163
  by (metis abs_ge_zero abs_mult_pos abs_mult)
paulson@24937
   164
have 5: "\<And>X1\<Colon>'b\<Colon>type.
paulson@24937
   165
   (h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X1
paulson@24937
   166
   \<le> \<bar>(c\<Colon>'a\<Colon>ordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>ordered_idom) X1\<bar>"
paulson@24937
   167
  by (metis 4 0 xt1(6) abs_ge_self abs_le_D1)
paulson@23449
   168
show "False"
paulson@24937
   169
  by (metis abs_mult mult_commute 3 abs_mult_pos linorder_linear 0 abs_le_D2 5 1 abs_le_iff)
paulson@23449
   170
qed
paulson@23449
   171
paulson@23449
   172
paulson@26333
   173
declare [[sledgehammer_modulus = 1]]
paulson@24545
   174
paulson@24545
   175
lemma (*bigo_pos_const:*) "(EX (c::'a::ordered_idom). 
paulson@24545
   176
    ALL x. (abs (h x)) <= (c * (abs (f x))))
paulson@24545
   177
      = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
paulson@24545
   178
  apply auto
paulson@24545
   179
  apply (case_tac "c = 0", simp)
paulson@24545
   180
  apply (rule_tac x = "1" in exI, simp)
paulson@24545
   181
  apply (rule_tac x = "abs c" in exI, auto);
paulson@24545
   182
proof (neg_clausify)
paulson@24545
   183
fix c x  (*sort/type constraint inserted by hand!*)
paulson@24545
   184
have 0: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2. \<bar>X1 * \<bar>X2\<bar>\<bar> = \<bar>X1 * X2\<bar>"
paulson@24545
   185
  by (metis abs_ge_zero abs_mult_pos abs_mult)
paulson@24545
   186
assume 1: "\<And>A. \<bar>h A\<bar> \<le> c * \<bar>f A\<bar>"
paulson@24545
   187
have 2: "\<And>X1 X2. \<not> \<bar>X1\<bar> \<le> X2 \<or> (0\<Colon>'a) \<le> X2"
paulson@24545
   188
  by (metis abs_ge_zero order_trans)
paulson@24545
   189
have 3: "\<And>X1. (0\<Colon>'a) \<le> c * \<bar>f X1\<bar>"
paulson@24545
   190
  by (metis 1 2)
paulson@24545
   191
have 4: "\<And>X1. c * \<bar>f X1\<bar> = \<bar>c * f X1\<bar>"
paulson@24545
   192
  by (metis 0 abs_of_nonneg 3)
paulson@24545
   193
have 5: "\<And>X1. - h X1 \<le> c * \<bar>f X1\<bar>"
paulson@24545
   194
  by (metis 1 abs_le_D2)
paulson@24545
   195
have 6: "\<And>X1. - h X1 \<le> \<bar>c * f X1\<bar>"
paulson@24545
   196
  by (metis 4 5)
paulson@24545
   197
have 7: "\<And>X1. h X1 \<le> c * \<bar>f X1\<bar>"
paulson@24545
   198
  by (metis 1 abs_le_D1)
paulson@24545
   199
have 8: "\<And>X1. h X1 \<le> \<bar>c * f X1\<bar>"
paulson@24545
   200
  by (metis 4 7)
paulson@24545
   201
assume 9: "\<not> \<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>"
paulson@24545
   202
have 10: "\<not> \<bar>h x\<bar> \<le> \<bar>c * f x\<bar>"
paulson@24545
   203
  by (metis abs_mult 9)
paulson@24545
   204
show "False"
paulson@24545
   205
  by (metis 6 8 10 abs_leI)
paulson@24545
   206
qed
paulson@24545
   207
paulson@24545
   208
paulson@26333
   209
declare [[sledgehammer_sorts = true]]
paulson@24545
   210
paulson@23449
   211
lemma bigo_alt_def: "O(f) = 
paulson@23449
   212
    {h. EX c. (0 < c & (ALL x. abs (h x) <= c * abs (f x)))}"
paulson@23449
   213
by (auto simp add: bigo_def bigo_pos_const)
paulson@23449
   214
wenzelm@28592
   215
ML_command{*AtpWrapper.problem_name := "BigO__bigo_elt_subset"*}
paulson@23449
   216
lemma bigo_elt_subset [intro]: "f : O(g) ==> O(f) <= O(g)"
paulson@23449
   217
  apply (auto simp add: bigo_alt_def)
paulson@23449
   218
  apply (rule_tac x = "ca * c" in exI)
paulson@23449
   219
  apply (rule conjI)
paulson@23449
   220
  apply (rule mult_pos_pos)
paulson@23449
   221
  apply (assumption)+ 
paulson@23449
   222
(*sledgehammer*);
paulson@23449
   223
  apply (rule allI)
paulson@23449
   224
  apply (drule_tac x = "xa" in spec)+
paulson@23449
   225
  apply (subgoal_tac "ca * abs(f xa) <= ca * (c * abs(g xa))");
paulson@23449
   226
  apply (erule order_trans)
paulson@23449
   227
  apply (simp add: mult_ac)
paulson@23449
   228
  apply (rule mult_left_mono, assumption)
paulson@23449
   229
  apply (rule order_less_imp_le, assumption);
paulson@23449
   230
done
paulson@23449
   231
paulson@23449
   232
wenzelm@28592
   233
ML_command{*AtpWrapper.problem_name := "BigO__bigo_refl"*}
paulson@23449
   234
lemma bigo_refl [intro]: "f : O(f)"
paulson@23449
   235
  apply(auto simp add: bigo_def)
paulson@23449
   236
proof (neg_clausify)
paulson@23449
   237
fix x
paulson@24937
   238
assume 0: "\<And>xa. \<not> \<bar>f (x xa)\<bar> \<le> xa * \<bar>f (x xa)\<bar>"
paulson@24937
   239
have 1: "\<And>X2. X2 \<le> (1\<Colon>'b) * X2 \<or> \<not> (1\<Colon>'b) \<le> (1\<Colon>'b)"
paulson@24937
   240
  by (metis mult_le_cancel_right1 order_eq_iff)
paulson@24937
   241
have 2: "\<And>X2. X2 \<le> (1\<Colon>'b) * X2"
paulson@24937
   242
  by (metis order_eq_iff 1)
paulson@24937
   243
show "False"
paulson@23449
   244
  by (metis 0 2)
paulson@23449
   245
qed
paulson@23449
   246
wenzelm@28592
   247
ML_command{*AtpWrapper.problem_name := "BigO__bigo_zero"*}
paulson@23449
   248
lemma bigo_zero: "0 : O(g)"
paulson@23449
   249
  apply (auto simp add: bigo_def func_zero)
paulson@23449
   250
proof (neg_clausify)
paulson@23449
   251
fix x
paulson@24937
   252
assume 0: "\<And>xa. \<not> (0\<Colon>'b) \<le> xa * \<bar>g (x xa)\<bar>"
paulson@24937
   253
have 1: "\<not> (0\<Colon>'b) \<le> (0\<Colon>'b)"
paulson@24937
   254
  by (metis 0 mult_eq_0_iff)
paulson@24937
   255
show "False"
paulson@24937
   256
  by (metis 1 linorder_neq_iff linorder_antisym_conv1)
paulson@23449
   257
qed
paulson@23449
   258
paulson@23449
   259
lemma bigo_zero2: "O(%x.0) = {%x.0}"
paulson@23449
   260
  apply (auto simp add: bigo_def) 
paulson@23449
   261
  apply (rule ext)
paulson@23449
   262
  apply auto
paulson@23449
   263
done
paulson@23449
   264
paulson@23449
   265
lemma bigo_plus_self_subset [intro]: 
berghofe@26814
   266
  "O(f) \<oplus> O(f) <= O(f)"
berghofe@26814
   267
  apply (auto simp add: bigo_alt_def set_plus_def)
paulson@23449
   268
  apply (rule_tac x = "c + ca" in exI)
paulson@23449
   269
  apply auto
nipkow@23477
   270
  apply (simp add: ring_distribs func_plus)
paulson@23449
   271
  apply (blast intro:order_trans abs_triangle_ineq add_mono elim:) 
paulson@23449
   272
done
paulson@23449
   273
berghofe@26814
   274
lemma bigo_plus_idemp [simp]: "O(f) \<oplus> O(f) = O(f)"
paulson@23449
   275
  apply (rule equalityI)
paulson@23449
   276
  apply (rule bigo_plus_self_subset)
paulson@23449
   277
  apply (rule set_zero_plus2) 
paulson@23449
   278
  apply (rule bigo_zero)
paulson@23449
   279
done
paulson@23449
   280
berghofe@26814
   281
lemma bigo_plus_subset [intro]: "O(f + g) <= O(f) \<oplus> O(g)"
paulson@23449
   282
  apply (rule subsetI)
berghofe@26814
   283
  apply (auto simp add: bigo_def bigo_pos_const func_plus set_plus_def)
paulson@23449
   284
  apply (subst bigo_pos_const [symmetric])+
paulson@23449
   285
  apply (rule_tac x = 
paulson@23449
   286
    "%n. if abs (g n) <= (abs (f n)) then x n else 0" in exI)
paulson@23449
   287
  apply (rule conjI)
paulson@23449
   288
  apply (rule_tac x = "c + c" in exI)
paulson@23449
   289
  apply (clarsimp)
paulson@23449
   290
  apply (auto)
paulson@23449
   291
  apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (f xa)")
paulson@23449
   292
  apply (erule_tac x = xa in allE)
paulson@23449
   293
  apply (erule order_trans)
paulson@23449
   294
  apply (simp)
paulson@23449
   295
  apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))")
paulson@23449
   296
  apply (erule order_trans)
nipkow@23477
   297
  apply (simp add: ring_distribs)
paulson@23449
   298
  apply (rule mult_left_mono)
paulson@23449
   299
  apply assumption
paulson@23449
   300
  apply (simp add: order_less_le)
paulson@23449
   301
  apply (rule mult_left_mono)
paulson@23449
   302
  apply (simp add: abs_triangle_ineq)
paulson@23449
   303
  apply (simp add: order_less_le)
paulson@23449
   304
  apply (rule mult_nonneg_nonneg)
paulson@23449
   305
  apply (rule add_nonneg_nonneg)
paulson@23449
   306
  apply auto
paulson@23449
   307
  apply (rule_tac x = "%n. if (abs (f n)) <  abs (g n) then x n else 0" 
paulson@23449
   308
     in exI)
paulson@23449
   309
  apply (rule conjI)
paulson@23449
   310
  apply (rule_tac x = "c + c" in exI)
paulson@23449
   311
  apply auto
paulson@23449
   312
  apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (g xa)")
paulson@23449
   313
  apply (erule_tac x = xa in allE)
paulson@23449
   314
  apply (erule order_trans)
paulson@23449
   315
  apply (simp)
paulson@23449
   316
  apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))")
paulson@23449
   317
  apply (erule order_trans)
nipkow@23477
   318
  apply (simp add: ring_distribs)
paulson@23449
   319
  apply (rule mult_left_mono)
paulson@23449
   320
  apply (simp add: order_less_le)
paulson@23449
   321
  apply (simp add: order_less_le)
paulson@23449
   322
  apply (rule mult_left_mono)
paulson@23449
   323
  apply (rule abs_triangle_ineq)
paulson@23449
   324
  apply (simp add: order_less_le)
paulson@25087
   325
apply (metis abs_not_less_zero double_less_0_iff less_not_permute linorder_not_less mult_less_0_iff)
paulson@23449
   326
  apply (rule ext)
paulson@23449
   327
  apply (auto simp add: if_splits linorder_not_le)
paulson@23449
   328
done
paulson@23449
   329
berghofe@26814
   330
lemma bigo_plus_subset2 [intro]: "A <= O(f) ==> B <= O(f) ==> A \<oplus> B <= O(f)"
berghofe@26814
   331
  apply (subgoal_tac "A \<oplus> B <= O(f) \<oplus> O(f)")
paulson@23449
   332
  apply (erule order_trans)
paulson@23449
   333
  apply simp
paulson@23449
   334
  apply (auto del: subsetI simp del: bigo_plus_idemp)
paulson@23449
   335
done
paulson@23449
   336
wenzelm@28592
   337
ML_command{*AtpWrapper.problem_name := "BigO__bigo_plus_eq"*}
paulson@23449
   338
lemma bigo_plus_eq: "ALL x. 0 <= f x ==> ALL x. 0 <= g x ==> 
berghofe@26814
   339
  O(f + g) = O(f) \<oplus> O(g)"
paulson@23449
   340
  apply (rule equalityI)
paulson@23449
   341
  apply (rule bigo_plus_subset)
berghofe@26814
   342
  apply (simp add: bigo_alt_def set_plus_def func_plus)
paulson@23449
   343
  apply clarify 
paulson@23449
   344
(*sledgehammer*); 
paulson@23449
   345
  apply (rule_tac x = "max c ca" in exI)
paulson@23449
   346
  apply (rule conjI)
paulson@25087
   347
   apply (metis Orderings.less_max_iff_disj)
paulson@23449
   348
  apply clarify
paulson@23449
   349
  apply (drule_tac x = "xa" in spec)+
paulson@23449
   350
  apply (subgoal_tac "0 <= f xa + g xa")
nipkow@23477
   351
  apply (simp add: ring_distribs)
paulson@23449
   352
  apply (subgoal_tac "abs(a xa + b xa) <= abs(a xa) + abs(b xa)")
paulson@23449
   353
  apply (subgoal_tac "abs(a xa) + abs(b xa) <= 
paulson@23449
   354
      max c ca * f xa + max c ca * g xa")
paulson@23449
   355
  apply (blast intro: order_trans)
paulson@23449
   356
  defer 1
paulson@23449
   357
  apply (rule abs_triangle_ineq)
paulson@25087
   358
  apply (metis add_nonneg_nonneg)
paulson@23449
   359
  apply (rule add_mono)
wenzelm@28592
   360
ML_command{*AtpWrapper.problem_name := "BigO__bigo_plus_eq_simpler"*} 
paulson@24942
   361
(*Found by SPASS; SLOW*)
haftmann@29511
   362
apply (metis le_maxI2 linorder_linear linorder_not_le min_max.sup_absorb1 mult_le_cancel_right order_trans)
paulson@25710
   363
apply (metis le_maxI2 linorder_not_le mult_le_cancel_right order_trans)
paulson@23449
   364
done
paulson@23449
   365
wenzelm@28592
   366
ML_command{*AtpWrapper.problem_name := "BigO__bigo_bounded_alt"*}
paulson@23449
   367
lemma bigo_bounded_alt: "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> 
paulson@23449
   368
    f : O(g)" 
paulson@23449
   369
  apply (auto simp add: bigo_def)
paulson@23449
   370
(*Version 1: one-shot proof*)
ballarin@26645
   371
  apply (metis OrderedGroup.abs_le_D1 linorder_class.not_less  order_less_le  Orderings.xt1(12)  Ring_and_Field.abs_mult)
paulson@23449
   372
  done
paulson@23449
   373
wenzelm@26312
   374
lemma (*bigo_bounded_alt:*) "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> 
paulson@23449
   375
    f : O(g)" 
paulson@23449
   376
  apply (auto simp add: bigo_def)
paulson@23449
   377
(*Version 2: single-step proof*)
paulson@23449
   378
proof (neg_clausify)
paulson@23449
   379
fix x
paulson@24937
   380
assume 0: "\<And>x. f x \<le> c * g x"
paulson@24937
   381
assume 1: "\<And>xa. \<not> f (x xa) \<le> xa * \<bar>g (x xa)\<bar>"
paulson@24937
   382
have 2: "\<And>X3. c * g X3 = f X3 \<or> \<not> c * g X3 \<le> f X3"
paulson@24937
   383
  by (metis 0 order_antisym_conv)
paulson@24937
   384
have 3: "\<And>X3. \<not> f (x \<bar>X3\<bar>) \<le> \<bar>X3 * g (x \<bar>X3\<bar>)\<bar>"
paulson@24937
   385
  by (metis 1 abs_mult)
paulson@24937
   386
have 4: "\<And>X1 X3\<Colon>'b\<Colon>ordered_idom. X3 \<le> X1 \<or> X1 \<le> \<bar>X3\<bar>"
paulson@24937
   387
  by (metis linorder_linear abs_le_D1)
paulson@24937
   388
have 5: "\<And>X3::'b. \<bar>X3\<bar> * \<bar>X3\<bar> = X3 * X3"
haftmann@26041
   389
  by (metis abs_mult_self)
paulson@24937
   390
have 6: "\<And>X3. \<not> X3 * X3 < (0\<Colon>'b\<Colon>ordered_idom)"
haftmann@26041
   391
  by (metis not_square_less_zero)
paulson@24937
   392
have 7: "\<And>X1 X3::'b. \<bar>X1\<bar> * \<bar>X3\<bar> = \<bar>X3 * X1\<bar>"
haftmann@26041
   393
  by (metis abs_mult mult_commute)
paulson@24937
   394
have 8: "\<And>X3::'b. X3 * X3 = \<bar>X3 * X3\<bar>"
paulson@24937
   395
  by (metis abs_mult 5)
paulson@24937
   396
have 9: "\<And>X3. X3 * g (x \<bar>X3\<bar>) \<le> f (x \<bar>X3\<bar>)"
paulson@24937
   397
  by (metis 3 4)
paulson@24937
   398
have 10: "c * g (x \<bar>c\<bar>) = f (x \<bar>c\<bar>)"
paulson@24937
   399
  by (metis 2 9)
paulson@24937
   400
have 11: "\<And>X3::'b. \<bar>X3\<bar> * \<bar>\<bar>X3\<bar>\<bar> = \<bar>X3\<bar> * \<bar>X3\<bar>"
paulson@24937
   401
  by (metis abs_idempotent abs_mult 8)
paulson@24937
   402
have 12: "\<And>X3::'b. \<bar>X3 * \<bar>X3\<bar>\<bar> = \<bar>X3\<bar> * \<bar>X3\<bar>"
haftmann@26041
   403
  by (metis mult_commute 7 11)
paulson@24937
   404
have 13: "\<And>X3::'b. \<bar>X3 * \<bar>X3\<bar>\<bar> = X3 * X3"
paulson@24937
   405
  by (metis 8 7 12)
paulson@24937
   406
have 14: "\<And>X3. X3 \<le> \<bar>X3\<bar> \<or> X3 < (0\<Colon>'b)"
paulson@24937
   407
  by (metis abs_ge_self abs_le_D1 abs_if)
paulson@24937
   408
have 15: "\<And>X3. X3 \<le> \<bar>X3\<bar> \<or> \<bar>X3\<bar> < (0\<Colon>'b)"
paulson@24937
   409
  by (metis abs_ge_self abs_le_D1 abs_if)
paulson@24937
   410
have 16: "\<And>X3. X3 * X3 < (0\<Colon>'b) \<or> X3 * \<bar>X3\<bar> \<le> X3 * X3"
paulson@24937
   411
  by (metis 15 13)
paulson@24937
   412
have 17: "\<And>X3::'b. X3 * \<bar>X3\<bar> \<le> X3 * X3"
paulson@24937
   413
  by (metis 16 6)
paulson@24937
   414
have 18: "\<And>X3. X3 \<le> \<bar>X3\<bar> \<or> \<not> X3 < (0\<Colon>'b)"
paulson@24937
   415
  by (metis mult_le_cancel_left 17)
paulson@24937
   416
have 19: "\<And>X3::'b. X3 \<le> \<bar>X3\<bar>"
paulson@24937
   417
  by (metis 18 14)
paulson@24937
   418
have 20: "\<not> f (x \<bar>c\<bar>) \<le> \<bar>f (x \<bar>c\<bar>)\<bar>"
paulson@24937
   419
  by (metis 3 10)
paulson@24937
   420
show "False"
paulson@24937
   421
  by (metis 20 19)
paulson@23449
   422
qed
paulson@23449
   423
paulson@23449
   424
paulson@23449
   425
text{*So here is the easier (and more natural) problem using transitivity*}
wenzelm@28592
   426
ML_command{*AtpWrapper.problem_name := "BigO__bigo_bounded_alt_trans"*}
paulson@23449
   427
lemma "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> f : O(g)" 
paulson@23449
   428
  apply (auto simp add: bigo_def)
paulson@23449
   429
  (*Version 1: one-shot proof*) 
paulson@25710
   430
  apply (metis Orderings.leD Orderings.leI abs_ge_self abs_le_D1 abs_mult abs_of_nonneg order_le_less)
paulson@23449
   431
  done
paulson@23449
   432
paulson@23449
   433
text{*So here is the easier (and more natural) problem using transitivity*}
wenzelm@28592
   434
ML_command{*AtpWrapper.problem_name := "BigO__bigo_bounded_alt_trans"*}
paulson@23449
   435
lemma "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> f : O(g)" 
paulson@23449
   436
  apply (auto simp add: bigo_def)
paulson@23449
   437
(*Version 2: single-step proof*)
paulson@23449
   438
proof (neg_clausify)
paulson@23449
   439
fix x
paulson@23519
   440
assume 0: "\<And>A\<Colon>'a\<Colon>type.
paulson@23519
   441
   (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) A
paulson@23519
   442
   \<le> (c\<Colon>'b\<Colon>ordered_idom) * (g\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) A"
paulson@23519
   443
assume 1: "\<And>A\<Colon>'b\<Colon>ordered_idom.
paulson@23519
   444
   \<not> (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a\<Colon>type) A)
paulson@23519
   445
     \<le> A * \<bar>(g\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) (x A)\<bar>"
paulson@23519
   446
have 2: "\<And>X2\<Colon>'a\<Colon>type.
paulson@23519
   447
   \<not> (c\<Colon>'b\<Colon>ordered_idom) * (g\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) X2
paulson@23519
   448
     < (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) X2"
paulson@23519
   449
  by (metis 0 linorder_not_le)
paulson@23519
   450
have 3: "\<And>X2\<Colon>'b\<Colon>ordered_idom.
paulson@23519
   451
   \<not> (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a\<Colon>type) \<bar>X2\<bar>)
paulson@23519
   452
     \<le> \<bar>X2 * (g\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) (x \<bar>X2\<bar>)\<bar>"
paulson@23519
   453
  by (metis abs_mult 1)
paulson@23519
   454
have 4: "\<And>X2\<Colon>'b\<Colon>ordered_idom.
paulson@23519
   455
   \<bar>X2 * (g\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a\<Colon>type) \<bar>X2\<bar>)\<bar>
paulson@23519
   456
   < (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) (x \<bar>X2\<bar>)"
paulson@23519
   457
  by (metis 3 linorder_not_less)
paulson@23519
   458
have 5: "\<And>X2\<Colon>'b\<Colon>ordered_idom.
paulson@23519
   459
   X2 * (g\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a\<Colon>type) \<bar>X2\<bar>)
paulson@23519
   460
   < (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) (x \<bar>X2\<bar>)"
paulson@23519
   461
  by (metis abs_less_iff 4)
paulson@23519
   462
show "False"
paulson@23519
   463
  by (metis 2 5)
paulson@23449
   464
qed
paulson@23449
   465
paulson@23449
   466
paulson@23449
   467
lemma bigo_bounded: "ALL x. 0 <= f x ==> ALL x. f x <= g x ==> 
paulson@23449
   468
    f : O(g)" 
paulson@23449
   469
  apply (erule bigo_bounded_alt [of f 1 g])
paulson@23449
   470
  apply simp
paulson@23449
   471
done
paulson@23449
   472
wenzelm@28592
   473
ML_command{*AtpWrapper.problem_name := "BigO__bigo_bounded2"*}
paulson@23449
   474
lemma bigo_bounded2: "ALL x. lb x <= f x ==> ALL x. f x <= lb x + g x ==>
paulson@23449
   475
    f : lb +o O(g)"
paulson@23449
   476
  apply (rule set_minus_imp_plus)
paulson@23449
   477
  apply (rule bigo_bounded)
berghofe@26814
   478
  apply (auto simp add: diff_minus fun_Compl_def func_plus)
paulson@23449
   479
  prefer 2
paulson@23449
   480
  apply (drule_tac x = x in spec)+ 
paulson@23449
   481
  apply arith (*not clear that it's provable otherwise*) 
paulson@23449
   482
proof (neg_clausify)
paulson@23449
   483
fix x
paulson@23449
   484
assume 0: "\<And>y. lb y \<le> f y"
paulson@23449
   485
assume 1: "\<not> (0\<Colon>'b) \<le> f x + - lb x"
paulson@23449
   486
have 2: "\<And>X3. (0\<Colon>'b) + X3 = X3"
paulson@23449
   487
  by (metis diff_eq_eq right_minus_eq)
paulson@23449
   488
have 3: "\<not> (0\<Colon>'b) \<le> f x - lb x"
nipkow@29667
   489
  by (metis 1 diff_minus)
paulson@23449
   490
have 4: "\<not> (0\<Colon>'b) + lb x \<le> f x"
paulson@23449
   491
  by (metis 3 le_diff_eq)
paulson@23449
   492
show "False"
paulson@23449
   493
  by (metis 4 2 0)
paulson@23449
   494
qed
paulson@23449
   495
wenzelm@28592
   496
ML_command{*AtpWrapper.problem_name := "BigO__bigo_abs"*}
paulson@23449
   497
lemma bigo_abs: "(%x. abs(f x)) =o O(f)" 
paulson@23449
   498
  apply (unfold bigo_def)
paulson@23449
   499
  apply auto
paulson@23449
   500
proof (neg_clausify)
paulson@23449
   501
fix x
paulson@24937
   502
assume 0: "\<And>xa. \<not> \<bar>f (x xa)\<bar> \<le> xa * \<bar>f (x xa)\<bar>"
paulson@24937
   503
have 1: "\<And>X2. X2 \<le> (1\<Colon>'b) * X2 \<or> \<not> (1\<Colon>'b) \<le> (1\<Colon>'b)"
paulson@24937
   504
  by (metis mult_le_cancel_right1 order_eq_iff)
paulson@24937
   505
have 2: "\<And>X2. X2 \<le> (1\<Colon>'b) * X2"
paulson@24937
   506
  by (metis order_eq_iff 1)
paulson@23449
   507
show "False"
paulson@23449
   508
  by (metis 0 2)
paulson@23449
   509
qed
paulson@23449
   510
wenzelm@28592
   511
ML_command{*AtpWrapper.problem_name := "BigO__bigo_abs2"*}
paulson@23449
   512
lemma bigo_abs2: "f =o O(%x. abs(f x))"
paulson@23449
   513
  apply (unfold bigo_def)
paulson@23449
   514
  apply auto
paulson@23449
   515
proof (neg_clausify)
paulson@23449
   516
fix x
paulson@24937
   517
assume 0: "\<And>xa. \<not> \<bar>f (x xa)\<bar> \<le> xa * \<bar>f (x xa)\<bar>"
paulson@24937
   518
have 1: "\<And>X2. X2 \<le> (1\<Colon>'b) * X2 \<or> \<not> (1\<Colon>'b) \<le> (1\<Colon>'b)"
paulson@24937
   519
  by (metis mult_le_cancel_right1 order_eq_iff)
paulson@24937
   520
have 2: "\<And>X2. X2 \<le> (1\<Colon>'b) * X2"
paulson@24937
   521
  by (metis order_eq_iff 1)
paulson@23449
   522
show "False"
paulson@23449
   523
  by (metis 0 2)
paulson@23449
   524
qed
paulson@23449
   525
 
paulson@23449
   526
lemma bigo_abs3: "O(f) = O(%x. abs(f x))"
paulson@23449
   527
  apply (rule equalityI)
paulson@23449
   528
  apply (rule bigo_elt_subset)
paulson@23449
   529
  apply (rule bigo_abs2)
paulson@23449
   530
  apply (rule bigo_elt_subset)
paulson@23449
   531
  apply (rule bigo_abs)
paulson@23449
   532
done
paulson@23449
   533
paulson@23449
   534
lemma bigo_abs4: "f =o g +o O(h) ==> 
paulson@23449
   535
    (%x. abs (f x)) =o (%x. abs (g x)) +o O(h)"
paulson@23449
   536
  apply (drule set_plus_imp_minus)
paulson@23449
   537
  apply (rule set_minus_imp_plus)
berghofe@26814
   538
  apply (subst fun_diff_def)
paulson@23449
   539
proof -
paulson@23449
   540
  assume a: "f - g : O(h)"
paulson@23449
   541
  have "(%x. abs (f x) - abs (g x)) =o O(%x. abs(abs (f x) - abs (g x)))"
paulson@23449
   542
    by (rule bigo_abs2)
paulson@23449
   543
  also have "... <= O(%x. abs (f x - g x))"
paulson@23449
   544
    apply (rule bigo_elt_subset)
paulson@23449
   545
    apply (rule bigo_bounded)
paulson@23449
   546
    apply force
paulson@23449
   547
    apply (rule allI)
paulson@23449
   548
    apply (rule abs_triangle_ineq3)
paulson@23449
   549
    done
paulson@23449
   550
  also have "... <= O(f - g)"
paulson@23449
   551
    apply (rule bigo_elt_subset)
berghofe@26814
   552
    apply (subst fun_diff_def)
paulson@23449
   553
    apply (rule bigo_abs)
paulson@23449
   554
    done
paulson@23449
   555
  also have "... <= O(h)"
wenzelm@23464
   556
    using a by (rule bigo_elt_subset)
paulson@23449
   557
  finally show "(%x. abs (f x) - abs (g x)) : O(h)".
paulson@23449
   558
qed
paulson@23449
   559
paulson@23449
   560
lemma bigo_abs5: "f =o O(g) ==> (%x. abs(f x)) =o O(g)" 
paulson@23449
   561
by (unfold bigo_def, auto)
paulson@23449
   562
berghofe@26814
   563
lemma bigo_elt_subset2 [intro]: "f : g +o O(h) ==> O(f) <= O(g) \<oplus> O(h)"
paulson@23449
   564
proof -
paulson@23449
   565
  assume "f : g +o O(h)"
berghofe@26814
   566
  also have "... <= O(g) \<oplus> O(h)"
paulson@23449
   567
    by (auto del: subsetI)
berghofe@26814
   568
  also have "... = O(%x. abs(g x)) \<oplus> O(%x. abs(h x))"
paulson@23449
   569
    apply (subst bigo_abs3 [symmetric])+
paulson@23449
   570
    apply (rule refl)
paulson@23449
   571
    done
paulson@23449
   572
  also have "... = O((%x. abs(g x)) + (%x. abs(h x)))"
paulson@23449
   573
    by (rule bigo_plus_eq [symmetric], auto)
paulson@23449
   574
  finally have "f : ...".
paulson@23449
   575
  then have "O(f) <= ..."
paulson@23449
   576
    by (elim bigo_elt_subset)
berghofe@26814
   577
  also have "... = O(%x. abs(g x)) \<oplus> O(%x. abs(h x))"
paulson@23449
   578
    by (rule bigo_plus_eq, auto)
paulson@23449
   579
  finally show ?thesis
paulson@23449
   580
    by (simp add: bigo_abs3 [symmetric])
paulson@23449
   581
qed
paulson@23449
   582
wenzelm@28592
   583
ML_command{*AtpWrapper.problem_name := "BigO__bigo_mult"*}
berghofe@26814
   584
lemma bigo_mult [intro]: "O(f)\<otimes>O(g) <= O(f * g)"
paulson@23449
   585
  apply (rule subsetI)
paulson@23449
   586
  apply (subst bigo_def)
paulson@23449
   587
  apply (auto simp del: abs_mult mult_ac
berghofe@26814
   588
              simp add: bigo_alt_def set_times_def func_times)
paulson@23449
   589
(*sledgehammer*); 
paulson@23449
   590
  apply (rule_tac x = "c * ca" in exI)
paulson@23449
   591
  apply(rule allI)
paulson@23449
   592
  apply(erule_tac x = x in allE)+
paulson@23449
   593
  apply(subgoal_tac "c * ca * abs(f x * g x) = 
paulson@23449
   594
      (c * abs(f x)) * (ca * abs(g x))")
wenzelm@28592
   595
ML_command{*AtpWrapper.problem_name := "BigO__bigo_mult_simpler"*}
paulson@23449
   596
prefer 2 
haftmann@26041
   597
apply (metis mult_assoc mult_left_commute
haftmann@26041
   598
  OrderedGroup.abs_of_pos OrderedGroup.mult_left_commute
haftmann@26041
   599
  Ring_and_Field.abs_mult Ring_and_Field.mult_pos_pos)
haftmann@26041
   600
  apply (erule ssubst) 
paulson@23449
   601
  apply (subst abs_mult)
paulson@23449
   602
(*not qute BigO__bigo_mult_simpler_1 (a hard problem!) as abs_mult has
paulson@23449
   603
  just been done*)
paulson@23449
   604
proof (neg_clausify)
paulson@23449
   605
fix a c b ca x
paulson@23449
   606
assume 0: "(0\<Colon>'b\<Colon>ordered_idom) < (c\<Colon>'b\<Colon>ordered_idom)"
paulson@23449
   607
assume 1: "\<bar>(a\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x\<Colon>'a)\<bar>
paulson@23449
   608
\<le> (c\<Colon>'b\<Colon>ordered_idom) * \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) x\<bar>"
paulson@23449
   609
assume 2: "\<bar>(b\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x\<Colon>'a)\<bar>
paulson@23449
   610
\<le> (ca\<Colon>'b\<Colon>ordered_idom) * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) x\<bar>"
paulson@23449
   611
assume 3: "\<not> \<bar>(a\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x\<Colon>'a)\<bar> *
paulson@23449
   612
  \<bar>(b\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) x\<bar>
paulson@23449
   613
  \<le> (c\<Colon>'b\<Colon>ordered_idom) * \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) x\<bar> *
paulson@23449
   614
    ((ca\<Colon>'b\<Colon>ordered_idom) * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) x\<bar>)"
paulson@23449
   615
have 4: "\<bar>c\<Colon>'b\<Colon>ordered_idom\<bar> = c"
paulson@23449
   616
  by (metis OrderedGroup.abs_of_pos 0)
paulson@23449
   617
have 5: "\<And>X1\<Colon>'b\<Colon>ordered_idom. (c\<Colon>'b\<Colon>ordered_idom) * \<bar>X1\<bar> = \<bar>c * X1\<bar>"
paulson@23449
   618
  by (metis Ring_and_Field.abs_mult 4)
paulson@23449
   619
have 6: "(0\<Colon>'b\<Colon>ordered_idom) = (1\<Colon>'b\<Colon>ordered_idom) \<or>
paulson@23449
   620
(0\<Colon>'b\<Colon>ordered_idom) < (1\<Colon>'b\<Colon>ordered_idom)"
paulson@23449
   621
  by (metis OrderedGroup.abs_not_less_zero Ring_and_Field.abs_one Ring_and_Field.linorder_neqE_ordered_idom)
paulson@23449
   622
have 7: "(0\<Colon>'b\<Colon>ordered_idom) < (1\<Colon>'b\<Colon>ordered_idom)"
paulson@23449
   623
  by (metis 6 Ring_and_Field.one_neq_zero)
paulson@23449
   624
have 8: "\<bar>1\<Colon>'b\<Colon>ordered_idom\<bar> = (1\<Colon>'b\<Colon>ordered_idom)"
paulson@23449
   625
  by (metis OrderedGroup.abs_of_pos 7)
paulson@23449
   626
have 9: "\<And>X1\<Colon>'b\<Colon>ordered_idom. (0\<Colon>'b\<Colon>ordered_idom) \<le> (c\<Colon>'b\<Colon>ordered_idom) * \<bar>X1\<bar>"
paulson@23449
   627
  by (metis OrderedGroup.abs_ge_zero 5)
paulson@23449
   628
have 10: "\<And>X1\<Colon>'b\<Colon>ordered_idom. X1 * (1\<Colon>'b\<Colon>ordered_idom) = X1"
haftmann@26041
   629
  by (metis Ring_and_Field.mult_cancel_right2 mult_commute)
paulson@23449
   630
have 11: "\<And>X1\<Colon>'b\<Colon>ordered_idom. \<bar>\<bar>X1\<bar>\<bar> = \<bar>X1\<bar> * \<bar>1\<Colon>'b\<Colon>ordered_idom\<bar>"
paulson@23449
   631
  by (metis Ring_and_Field.abs_mult OrderedGroup.abs_idempotent 10)
paulson@23449
   632
have 12: "\<And>X1\<Colon>'b\<Colon>ordered_idom. \<bar>\<bar>X1\<bar>\<bar> = \<bar>X1\<bar>"
paulson@23449
   633
  by (metis 11 8 10)
paulson@23449
   634
have 13: "\<And>X1\<Colon>'b\<Colon>ordered_idom. (0\<Colon>'b\<Colon>ordered_idom) \<le> \<bar>X1\<bar>"
paulson@23449
   635
  by (metis OrderedGroup.abs_ge_zero 12)
paulson@23449
   636
have 14: "\<not> (0\<Colon>'b\<Colon>ordered_idom)
paulson@23449
   637
  \<le> (c\<Colon>'b\<Colon>ordered_idom) * \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x\<Colon>'a)\<bar> \<or>
paulson@23449
   638
\<not> (0\<Colon>'b\<Colon>ordered_idom) \<le> \<bar>(b\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) x\<bar> \<or>
paulson@23449
   639
\<not> \<bar>b x\<bar> \<le> (ca\<Colon>'b\<Colon>ordered_idom) * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) x\<bar> \<or>
paulson@23449
   640
\<not> \<bar>(a\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) x\<bar> \<le> c * \<bar>f x\<bar>"
paulson@23449
   641
  by (metis 3 Ring_and_Field.mult_mono)
paulson@23449
   642
have 15: "\<not> (0\<Colon>'b\<Colon>ordered_idom) \<le> \<bar>(b\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x\<Colon>'a)\<bar> \<or>
paulson@23449
   643
\<not> \<bar>b x\<bar> \<le> (ca\<Colon>'b\<Colon>ordered_idom) * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) x\<bar> \<or>
paulson@23449
   644
\<not> \<bar>(a\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) x\<bar>
paulson@23449
   645
  \<le> (c\<Colon>'b\<Colon>ordered_idom) * \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) x\<bar>"
paulson@23449
   646
  by (metis 14 9)
paulson@23449
   647
have 16: "\<not> \<bar>(b\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x\<Colon>'a)\<bar>
paulson@23449
   648
  \<le> (ca\<Colon>'b\<Colon>ordered_idom) * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) x\<bar> \<or>
paulson@23449
   649
\<not> \<bar>(a\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) x\<bar>
paulson@23449
   650
  \<le> (c\<Colon>'b\<Colon>ordered_idom) * \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) x\<bar>"
paulson@23449
   651
  by (metis 15 13)
paulson@23449
   652
have 17: "\<not> \<bar>(a\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x\<Colon>'a)\<bar>
paulson@23449
   653
  \<le> (c\<Colon>'b\<Colon>ordered_idom) * \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) x\<bar>"
paulson@23449
   654
  by (metis 16 2)
paulson@23449
   655
show 18: "False"
paulson@23449
   656
  by (metis 17 1)
paulson@23449
   657
qed
paulson@23449
   658
paulson@23449
   659
wenzelm@28592
   660
ML_command{*AtpWrapper.problem_name := "BigO__bigo_mult2"*}
paulson@23449
   661
lemma bigo_mult2 [intro]: "f *o O(g) <= O(f * g)"
paulson@23449
   662
  apply (auto simp add: bigo_def elt_set_times_def func_times abs_mult)
paulson@23449
   663
(*sledgehammer*); 
paulson@23449
   664
  apply (rule_tac x = c in exI)
paulson@23449
   665
  apply clarify
paulson@23449
   666
  apply (drule_tac x = x in spec)
wenzelm@28592
   667
ML_command{*AtpWrapper.problem_name := "BigO__bigo_mult2_simpler"*}
paulson@24942
   668
(*sledgehammer [no luck]*); 
paulson@23449
   669
  apply (subgoal_tac "abs(f x) * abs(b x) <= abs(f x) * (c * abs(g x))")
paulson@23449
   670
  apply (simp add: mult_ac)
paulson@23449
   671
  apply (rule mult_left_mono, assumption)
paulson@23449
   672
  apply (rule abs_ge_zero)
paulson@23449
   673
done
paulson@23449
   674
wenzelm@28592
   675
ML_command{*AtpWrapper.problem_name:="BigO__bigo_mult3"*}
paulson@23449
   676
lemma bigo_mult3: "f : O(h) ==> g : O(j) ==> f * g : O(h * j)"
paulson@23449
   677
by (metis bigo_mult set_times_intro subset_iff)
paulson@23449
   678
wenzelm@28592
   679
ML_command{*AtpWrapper.problem_name:="BigO__bigo_mult4"*}
paulson@23449
   680
lemma bigo_mult4 [intro]:"f : k +o O(h) ==> g * f : (g * k) +o O(g * h)"
paulson@23449
   681
by (metis bigo_mult2 set_plus_mono_b set_times_intro2 set_times_plus_distrib)
paulson@23449
   682
paulson@23449
   683
paulson@23449
   684
lemma bigo_mult5: "ALL x. f x ~= 0 ==>
paulson@23449
   685
    O(f * g) <= (f::'a => ('b::ordered_field)) *o O(g)"
paulson@23449
   686
proof -
paulson@23449
   687
  assume "ALL x. f x ~= 0"
paulson@23449
   688
  show "O(f * g) <= f *o O(g)"
paulson@23449
   689
  proof
paulson@23449
   690
    fix h
paulson@23449
   691
    assume "h : O(f * g)"
paulson@23449
   692
    then have "(%x. 1 / (f x)) * h : (%x. 1 / f x) *o O(f * g)"
paulson@23449
   693
      by auto
paulson@23449
   694
    also have "... <= O((%x. 1 / f x) * (f * g))"
paulson@23449
   695
      by (rule bigo_mult2)
paulson@23449
   696
    also have "(%x. 1 / f x) * (f * g) = g"
paulson@23449
   697
      apply (simp add: func_times) 
paulson@23449
   698
      apply (rule ext)
paulson@23449
   699
      apply (simp add: prems nonzero_divide_eq_eq mult_ac)
paulson@23449
   700
      done
paulson@23449
   701
    finally have "(%x. (1::'b) / f x) * h : O(g)".
paulson@23449
   702
    then have "f * ((%x. (1::'b) / f x) * h) : f *o O(g)"
paulson@23449
   703
      by auto
paulson@23449
   704
    also have "f * ((%x. (1::'b) / f x) * h) = h"
paulson@23449
   705
      apply (simp add: func_times) 
paulson@23449
   706
      apply (rule ext)
paulson@23449
   707
      apply (simp add: prems nonzero_divide_eq_eq mult_ac)
paulson@23449
   708
      done
paulson@23449
   709
    finally show "h : f *o O(g)".
paulson@23449
   710
  qed
paulson@23449
   711
qed
paulson@23449
   712
wenzelm@28592
   713
ML_command{*AtpWrapper.problem_name := "BigO__bigo_mult6"*}
paulson@23449
   714
lemma bigo_mult6: "ALL x. f x ~= 0 ==>
paulson@23449
   715
    O(f * g) = (f::'a => ('b::ordered_field)) *o O(g)"
paulson@23449
   716
by (metis bigo_mult2 bigo_mult5 order_antisym)
paulson@23449
   717
paulson@23449
   718
(*proof requires relaxing relevance: 2007-01-25*)
wenzelm@28592
   719
ML_command{*AtpWrapper.problem_name := "BigO__bigo_mult7"*}
paulson@23449
   720
  declare bigo_mult6 [simp]
paulson@23449
   721
lemma bigo_mult7: "ALL x. f x ~= 0 ==>
berghofe@26814
   722
    O(f * g) <= O(f::'a => ('b::ordered_field)) \<otimes> O(g)"
paulson@23449
   723
(*sledgehammer*)
paulson@23449
   724
  apply (subst bigo_mult6)
paulson@23449
   725
  apply assumption
paulson@23449
   726
  apply (rule set_times_mono3) 
paulson@23449
   727
  apply (rule bigo_refl)
paulson@23449
   728
done
paulson@23449
   729
  declare bigo_mult6 [simp del]
paulson@23449
   730
wenzelm@28592
   731
ML_command{*AtpWrapper.problem_name := "BigO__bigo_mult8"*}
paulson@23449
   732
  declare bigo_mult7[intro!]
paulson@23449
   733
lemma bigo_mult8: "ALL x. f x ~= 0 ==>
berghofe@26814
   734
    O(f * g) = O(f::'a => ('b::ordered_field)) \<otimes> O(g)"
paulson@23449
   735
by (metis bigo_mult bigo_mult7 order_antisym_conv)
paulson@23449
   736
paulson@23449
   737
lemma bigo_minus [intro]: "f : O(g) ==> - f : O(g)"
berghofe@26814
   738
  by (auto simp add: bigo_def fun_Compl_def)
paulson@23449
   739
paulson@23449
   740
lemma bigo_minus2: "f : g +o O(h) ==> -f : -g +o O(h)"
paulson@23449
   741
  apply (rule set_minus_imp_plus)
paulson@23449
   742
  apply (drule set_plus_imp_minus)
paulson@23449
   743
  apply (drule bigo_minus)
paulson@23449
   744
  apply (simp add: diff_minus)
paulson@23449
   745
done
paulson@23449
   746
paulson@23449
   747
lemma bigo_minus3: "O(-f) = O(f)"
berghofe@26814
   748
  by (auto simp add: bigo_def fun_Compl_def abs_minus_cancel)
paulson@23449
   749
paulson@23449
   750
lemma bigo_plus_absorb_lemma1: "f : O(g) ==> f +o O(g) <= O(g)"
paulson@23449
   751
proof -
paulson@23449
   752
  assume a: "f : O(g)"
paulson@23449
   753
  show "f +o O(g) <= O(g)"
paulson@23449
   754
  proof -
paulson@23449
   755
    have "f : O(f)" by auto
berghofe@26814
   756
    then have "f +o O(g) <= O(f) \<oplus> O(g)"
paulson@23449
   757
      by (auto del: subsetI)
berghofe@26814
   758
    also have "... <= O(g) \<oplus> O(g)"
paulson@23449
   759
    proof -
paulson@23449
   760
      from a have "O(f) <= O(g)" by (auto del: subsetI)
paulson@23449
   761
      thus ?thesis by (auto del: subsetI)
paulson@23449
   762
    qed
paulson@23449
   763
    also have "... <= O(g)" by (simp add: bigo_plus_idemp)
paulson@23449
   764
    finally show ?thesis .
paulson@23449
   765
  qed
paulson@23449
   766
qed
paulson@23449
   767
paulson@23449
   768
lemma bigo_plus_absorb_lemma2: "f : O(g) ==> O(g) <= f +o O(g)"
paulson@23449
   769
proof -
paulson@23449
   770
  assume a: "f : O(g)"
paulson@23449
   771
  show "O(g) <= f +o O(g)"
paulson@23449
   772
  proof -
paulson@23449
   773
    from a have "-f : O(g)" by auto
paulson@23449
   774
    then have "-f +o O(g) <= O(g)" by (elim bigo_plus_absorb_lemma1)
paulson@23449
   775
    then have "f +o (-f +o O(g)) <= f +o O(g)" by auto
paulson@23449
   776
    also have "f +o (-f +o O(g)) = O(g)"
paulson@23449
   777
      by (simp add: set_plus_rearranges)
paulson@23449
   778
    finally show ?thesis .
paulson@23449
   779
  qed
paulson@23449
   780
qed
paulson@23449
   781
wenzelm@28592
   782
ML_command{*AtpWrapper.problem_name:="BigO__bigo_plus_absorb"*}
paulson@23449
   783
lemma bigo_plus_absorb [simp]: "f : O(g) ==> f +o O(g) = O(g)"
paulson@23449
   784
by (metis bigo_plus_absorb_lemma1 bigo_plus_absorb_lemma2 order_eq_iff);
paulson@23449
   785
paulson@23449
   786
lemma bigo_plus_absorb2 [intro]: "f : O(g) ==> A <= O(g) ==> f +o A <= O(g)"
paulson@23449
   787
  apply (subgoal_tac "f +o A <= f +o O(g)")
paulson@23449
   788
  apply force+
paulson@23449
   789
done
paulson@23449
   790
paulson@23449
   791
lemma bigo_add_commute_imp: "f : g +o O(h) ==> g : f +o O(h)"
paulson@23449
   792
  apply (subst set_minus_plus [symmetric])
paulson@23449
   793
  apply (subgoal_tac "g - f = - (f - g)")
paulson@23449
   794
  apply (erule ssubst)
paulson@23449
   795
  apply (rule bigo_minus)
paulson@23449
   796
  apply (subst set_minus_plus)
paulson@23449
   797
  apply assumption
paulson@23449
   798
  apply  (simp add: diff_minus add_ac)
paulson@23449
   799
done
paulson@23449
   800
paulson@23449
   801
lemma bigo_add_commute: "(f : g +o O(h)) = (g : f +o O(h))"
paulson@23449
   802
  apply (rule iffI)
paulson@23449
   803
  apply (erule bigo_add_commute_imp)+
paulson@23449
   804
done
paulson@23449
   805
paulson@23449
   806
lemma bigo_const1: "(%x. c) : O(%x. 1)"
paulson@23449
   807
by (auto simp add: bigo_def mult_ac)
paulson@23449
   808
wenzelm@28592
   809
ML_command{*AtpWrapper.problem_name:="BigO__bigo_const2"*}
paulson@23449
   810
lemma (*bigo_const2 [intro]:*) "O(%x. c) <= O(%x. 1)"
paulson@23449
   811
by (metis bigo_const1 bigo_elt_subset);
paulson@23449
   812
paulson@24855
   813
lemma bigo_const2 [intro]: "O(%x. c::'b::ordered_idom) <= O(%x. 1)";
paulson@23449
   814
(*??FAILS because the two occurrences of COMBK have different polymorphic types
paulson@23449
   815
proof (neg_clausify)
paulson@23449
   816
assume 0: "\<not> O(COMBK (c\<Colon>'b\<Colon>ordered_idom)) \<subseteq> O(COMBK (1\<Colon>'b\<Colon>ordered_idom))"
paulson@23449
   817
have 1: "COMBK (c\<Colon>'b\<Colon>ordered_idom) \<notin> O(COMBK (1\<Colon>'b\<Colon>ordered_idom))"
paulson@23449
   818
apply (rule notI) 
paulson@23449
   819
apply (rule 0 [THEN notE]) 
paulson@23449
   820
apply (rule bigo_elt_subset) 
paulson@23449
   821
apply assumption; 
paulson@23449
   822
sorry
paulson@23449
   823
  by (metis 0 bigo_elt_subset)  loops??
paulson@23449
   824
show "False"
paulson@23449
   825
  by (metis 1 bigo_const1)
paulson@23449
   826
qed
paulson@23449
   827
*)
paulson@23449
   828
  apply (rule bigo_elt_subset)
paulson@23449
   829
  apply (rule bigo_const1)
paulson@23449
   830
done
paulson@23449
   831
wenzelm@28592
   832
ML_command{*AtpWrapper.problem_name := "BigO__bigo_const3"*}
paulson@23449
   833
lemma bigo_const3: "(c::'a::ordered_field) ~= 0 ==> (%x. 1) : O(%x. c)"
paulson@23449
   834
apply (simp add: bigo_def)
paulson@23449
   835
proof (neg_clausify)
paulson@23449
   836
assume 0: "(c\<Colon>'a\<Colon>ordered_field) \<noteq> (0\<Colon>'a\<Colon>ordered_field)"
paulson@23519
   837
assume 1: "\<And>A\<Colon>'a\<Colon>ordered_field. \<not> (1\<Colon>'a\<Colon>ordered_field) \<le> A * \<bar>c\<Colon>'a\<Colon>ordered_field\<bar>"
paulson@23449
   838
have 2: "(0\<Colon>'a\<Colon>ordered_field) = \<bar>c\<Colon>'a\<Colon>ordered_field\<bar> \<or>
paulson@23449
   839
\<not> (1\<Colon>'a\<Colon>ordered_field) \<le> (1\<Colon>'a\<Colon>ordered_field)"
paulson@23449
   840
  by (metis 1 field_inverse)
paulson@23449
   841
have 3: "\<bar>c\<Colon>'a\<Colon>ordered_field\<bar> = (0\<Colon>'a\<Colon>ordered_field)"
paulson@23519
   842
  by (metis linorder_neq_iff linorder_antisym_conv1 2)
paulson@23449
   843
have 4: "(0\<Colon>'a\<Colon>ordered_field) = (c\<Colon>'a\<Colon>ordered_field)"
paulson@23519
   844
  by (metis 3 abs_eq_0)
paulson@23519
   845
show "False"
paulson@23519
   846
  by (metis 0 4)
paulson@23449
   847
qed
paulson@23449
   848
paulson@23449
   849
lemma bigo_const4: "(c::'a::ordered_field) ~= 0 ==> O(%x. 1) <= O(%x. c)"
paulson@23449
   850
by (rule bigo_elt_subset, rule bigo_const3, assumption)
paulson@23449
   851
paulson@23449
   852
lemma bigo_const [simp]: "(c::'a::ordered_field) ~= 0 ==> 
paulson@23449
   853
    O(%x. c) = O(%x. 1)"
paulson@23449
   854
by (rule equalityI, rule bigo_const2, rule bigo_const4, assumption)
paulson@23449
   855
wenzelm@28592
   856
ML_command{*AtpWrapper.problem_name := "BigO__bigo_const_mult1"*}
paulson@23449
   857
lemma bigo_const_mult1: "(%x. c * f x) : O(f)"
paulson@24937
   858
  apply (simp add: bigo_def abs_mult)
paulson@23449
   859
proof (neg_clausify)
paulson@23449
   860
fix x
haftmann@25304
   861
assume 0: "\<And>xa\<Colon>'b\<Colon>ordered_idom.
haftmann@25304
   862
   \<not> \<bar>c\<Colon>'b\<Colon>ordered_idom\<bar> *
haftmann@25304
   863
     \<bar>(f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a\<Colon>type) xa)\<bar>
haftmann@25304
   864
     \<le> xa * \<bar>f (x xa)\<bar>"
paulson@24937
   865
show "False"
haftmann@25304
   866
  by (metis linorder_neq_iff linorder_antisym_conv1 0)
paulson@23449
   867
qed
paulson@23449
   868
paulson@23449
   869
lemma bigo_const_mult2: "O(%x. c * f x) <= O(f)"
paulson@23449
   870
by (rule bigo_elt_subset, rule bigo_const_mult1)
paulson@23449
   871
wenzelm@28592
   872
ML_command{*AtpWrapper.problem_name := "BigO__bigo_const_mult3"*}
paulson@23449
   873
lemma bigo_const_mult3: "(c::'a::ordered_field) ~= 0 ==> f : O(%x. c * f x)"
paulson@23449
   874
  apply (simp add: bigo_def)
paulson@24942
   875
(*sledgehammer [no luck]*); 
paulson@23449
   876
  apply (rule_tac x = "abs(inverse c)" in exI)
paulson@23449
   877
  apply (simp only: abs_mult [symmetric] mult_assoc [symmetric])
paulson@23449
   878
apply (subst left_inverse) 
paulson@23449
   879
apply (auto ); 
paulson@23449
   880
done
paulson@23449
   881
paulson@23449
   882
lemma bigo_const_mult4: "(c::'a::ordered_field) ~= 0 ==> 
paulson@23449
   883
    O(f) <= O(%x. c * f x)"
paulson@23449
   884
by (rule bigo_elt_subset, rule bigo_const_mult3, assumption)
paulson@23449
   885
paulson@23449
   886
lemma bigo_const_mult [simp]: "(c::'a::ordered_field) ~= 0 ==> 
paulson@23449
   887
    O(%x. c * f x) = O(f)"
paulson@23449
   888
by (rule equalityI, rule bigo_const_mult2, erule bigo_const_mult4)
paulson@23449
   889
wenzelm@28592
   890
ML_command{*AtpWrapper.problem_name := "BigO__bigo_const_mult5"*}
paulson@23449
   891
lemma bigo_const_mult5 [simp]: "(c::'a::ordered_field) ~= 0 ==> 
paulson@23449
   892
    (%x. c) *o O(f) = O(f)"
paulson@23449
   893
  apply (auto del: subsetI)
paulson@23449
   894
  apply (rule order_trans)
paulson@23449
   895
  apply (rule bigo_mult2)
paulson@23449
   896
  apply (simp add: func_times)
paulson@23449
   897
  apply (auto intro!: subsetI simp add: bigo_def elt_set_times_def func_times)
paulson@23449
   898
  apply (rule_tac x = "%y. inverse c * x y" in exI)
paulson@24942
   899
  apply (rename_tac g d) 
paulson@24942
   900
  apply safe
paulson@24942
   901
  apply (rule_tac [2] ext) 
paulson@24942
   902
   prefer 2 
haftmann@26041
   903
   apply simp
paulson@24942
   904
  apply (simp add: mult_assoc [symmetric] abs_mult)
paulson@24942
   905
  (*couldn't get this proof without the step above; SLOW*)
haftmann@26041
   906
  apply (metis mult_assoc abs_ge_zero mult_left_mono)
paulson@23449
   907
done
paulson@23449
   908
paulson@23449
   909
wenzelm@28592
   910
ML_command{*AtpWrapper.problem_name := "BigO__bigo_const_mult6"*}
paulson@23449
   911
lemma bigo_const_mult6 [intro]: "(%x. c) *o O(f) <= O(f)"
paulson@23449
   912
  apply (auto intro!: subsetI
paulson@23449
   913
    simp add: bigo_def elt_set_times_def func_times
paulson@23449
   914
    simp del: abs_mult mult_ac)
paulson@23449
   915
(*sledgehammer*); 
paulson@23449
   916
  apply (rule_tac x = "ca * (abs c)" in exI)
paulson@23449
   917
  apply (rule allI)
paulson@23449
   918
  apply (subgoal_tac "ca * abs(c) * abs(f x) = abs(c) * (ca * abs(f x))")
paulson@23449
   919
  apply (erule ssubst)
paulson@23449
   920
  apply (subst abs_mult)
paulson@23449
   921
  apply (rule mult_left_mono)
paulson@23449
   922
  apply (erule spec)
paulson@23449
   923
  apply simp
paulson@23449
   924
  apply(simp add: mult_ac)
paulson@23449
   925
done
paulson@23449
   926
paulson@23449
   927
lemma bigo_const_mult7 [intro]: "f =o O(g) ==> (%x. c * f x) =o O(g)"
paulson@23449
   928
proof -
paulson@23449
   929
  assume "f =o O(g)"
paulson@23449
   930
  then have "(%x. c) * f =o (%x. c) *o O(g)"
paulson@23449
   931
    by auto
paulson@23449
   932
  also have "(%x. c) * f = (%x. c * f x)"
paulson@23449
   933
    by (simp add: func_times)
paulson@23449
   934
  also have "(%x. c) *o O(g) <= O(g)"
paulson@23449
   935
    by (auto del: subsetI)
paulson@23449
   936
  finally show ?thesis .
paulson@23449
   937
qed
paulson@23449
   938
paulson@23449
   939
lemma bigo_compose1: "f =o O(g) ==> (%x. f(k x)) =o O(%x. g(k x))"
paulson@23449
   940
by (unfold bigo_def, auto)
paulson@23449
   941
paulson@23449
   942
lemma bigo_compose2: "f =o g +o O(h) ==> (%x. f(k x)) =o (%x. g(k x)) +o 
paulson@23449
   943
    O(%x. h(k x))"
berghofe@26814
   944
  apply (simp only: set_minus_plus [symmetric] diff_minus fun_Compl_def
paulson@23449
   945
      func_plus)
paulson@23449
   946
  apply (erule bigo_compose1)
paulson@23449
   947
done
paulson@23449
   948
paulson@23449
   949
subsection {* Setsum *}
paulson@23449
   950
paulson@23449
   951
lemma bigo_setsum_main: "ALL x. ALL y : A x. 0 <= h x y ==> 
paulson@23449
   952
    EX c. ALL x. ALL y : A x. abs(f x y) <= c * (h x y) ==>
paulson@23449
   953
      (%x. SUM y : A x. f x y) =o O(%x. SUM y : A x. h x y)"  
paulson@23449
   954
  apply (auto simp add: bigo_def)
paulson@23449
   955
  apply (rule_tac x = "abs c" in exI)
paulson@23449
   956
  apply (subst abs_of_nonneg) back back
paulson@23449
   957
  apply (rule setsum_nonneg)
paulson@23449
   958
  apply force
paulson@23449
   959
  apply (subst setsum_right_distrib)
paulson@23449
   960
  apply (rule allI)
paulson@23449
   961
  apply (rule order_trans)
paulson@23449
   962
  apply (rule setsum_abs)
paulson@23449
   963
  apply (rule setsum_mono)
paulson@23449
   964
apply (blast intro: order_trans mult_right_mono abs_ge_self) 
paulson@23449
   965
done
paulson@23449
   966
wenzelm@28592
   967
ML_command{*AtpWrapper.problem_name := "BigO__bigo_setsum1"*}
paulson@23449
   968
lemma bigo_setsum1: "ALL x y. 0 <= h x y ==> 
paulson@23449
   969
    EX c. ALL x y. abs(f x y) <= c * (h x y) ==>
paulson@23449
   970
      (%x. SUM y : A x. f x y) =o O(%x. SUM y : A x. h x y)"
paulson@23449
   971
  apply (rule bigo_setsum_main)
paulson@23449
   972
(*sledgehammer*); 
paulson@23449
   973
  apply force
paulson@23449
   974
  apply clarsimp
paulson@23449
   975
  apply (rule_tac x = c in exI)
paulson@23449
   976
  apply force
paulson@23449
   977
done
paulson@23449
   978
paulson@23449
   979
lemma bigo_setsum2: "ALL y. 0 <= h y ==> 
paulson@23449
   980
    EX c. ALL y. abs(f y) <= c * (h y) ==>
paulson@23449
   981
      (%x. SUM y : A x. f y) =o O(%x. SUM y : A x. h y)"
paulson@23449
   982
by (rule bigo_setsum1, auto)  
paulson@23449
   983
wenzelm@28592
   984
ML_command{*AtpWrapper.problem_name := "BigO__bigo_setsum3"*}
paulson@23449
   985
lemma bigo_setsum3: "f =o O(h) ==>
paulson@23449
   986
    (%x. SUM y : A x. (l x y) * f(k x y)) =o
paulson@23449
   987
      O(%x. SUM y : A x. abs(l x y * h(k x y)))"
paulson@23449
   988
  apply (rule bigo_setsum1)
paulson@23449
   989
  apply (rule allI)+
paulson@23449
   990
  apply (rule abs_ge_zero)
paulson@23449
   991
  apply (unfold bigo_def)
paulson@23449
   992
  apply (auto simp add: abs_mult);
paulson@23449
   993
(*sledgehammer*); 
paulson@23449
   994
  apply (rule_tac x = c in exI)
paulson@23449
   995
  apply (rule allI)+
paulson@23449
   996
  apply (subst mult_left_commute)
paulson@23449
   997
  apply (rule mult_left_mono)
paulson@23449
   998
  apply (erule spec)
paulson@23449
   999
  apply (rule abs_ge_zero)
paulson@23449
  1000
done
paulson@23449
  1001
paulson@23449
  1002
lemma bigo_setsum4: "f =o g +o O(h) ==>
paulson@23449
  1003
    (%x. SUM y : A x. l x y * f(k x y)) =o
paulson@23449
  1004
      (%x. SUM y : A x. l x y * g(k x y)) +o
paulson@23449
  1005
        O(%x. SUM y : A x. abs(l x y * h(k x y)))"
paulson@23449
  1006
  apply (rule set_minus_imp_plus)
berghofe@26814
  1007
  apply (subst fun_diff_def)
paulson@23449
  1008
  apply (subst setsum_subtractf [symmetric])
paulson@23449
  1009
  apply (subst right_diff_distrib [symmetric])
paulson@23449
  1010
  apply (rule bigo_setsum3)
berghofe@26814
  1011
  apply (subst fun_diff_def [symmetric])
paulson@23449
  1012
  apply (erule set_plus_imp_minus)
paulson@23449
  1013
done
paulson@23449
  1014
wenzelm@28592
  1015
ML_command{*AtpWrapper.problem_name := "BigO__bigo_setsum5"*}
paulson@23449
  1016
lemma bigo_setsum5: "f =o O(h) ==> ALL x y. 0 <= l x y ==> 
paulson@23449
  1017
    ALL x. 0 <= h x ==>
paulson@23449
  1018
      (%x. SUM y : A x. (l x y) * f(k x y)) =o
paulson@23449
  1019
        O(%x. SUM y : A x. (l x y) * h(k x y))" 
paulson@23449
  1020
  apply (subgoal_tac "(%x. SUM y : A x. (l x y) * h(k x y)) = 
paulson@23449
  1021
      (%x. SUM y : A x. abs((l x y) * h(k x y)))")
paulson@23449
  1022
  apply (erule ssubst)
paulson@23449
  1023
  apply (erule bigo_setsum3)
paulson@23449
  1024
  apply (rule ext)
paulson@23449
  1025
  apply (rule setsum_cong2)
paulson@23449
  1026
  apply (thin_tac "f \<in> O(h)") 
paulson@24942
  1027
apply (metis abs_of_nonneg zero_le_mult_iff)
paulson@23449
  1028
done
paulson@23449
  1029
paulson@23449
  1030
lemma bigo_setsum6: "f =o g +o O(h) ==> ALL x y. 0 <= l x y ==>
paulson@23449
  1031
    ALL x. 0 <= h x ==>
paulson@23449
  1032
      (%x. SUM y : A x. (l x y) * f(k x y)) =o
paulson@23449
  1033
        (%x. SUM y : A x. (l x y) * g(k x y)) +o
paulson@23449
  1034
          O(%x. SUM y : A x. (l x y) * h(k x y))" 
paulson@23449
  1035
  apply (rule set_minus_imp_plus)
berghofe@26814
  1036
  apply (subst fun_diff_def)
paulson@23449
  1037
  apply (subst setsum_subtractf [symmetric])
paulson@23449
  1038
  apply (subst right_diff_distrib [symmetric])
paulson@23449
  1039
  apply (rule bigo_setsum5)
berghofe@26814
  1040
  apply (subst fun_diff_def [symmetric])
paulson@23449
  1041
  apply (drule set_plus_imp_minus)
paulson@23449
  1042
  apply auto
paulson@23449
  1043
done
paulson@23449
  1044
paulson@23449
  1045
subsection {* Misc useful stuff *}
paulson@23449
  1046
paulson@23449
  1047
lemma bigo_useful_intro: "A <= O(f) ==> B <= O(f) ==>
berghofe@26814
  1048
  A \<oplus> B <= O(f)"
paulson@23449
  1049
  apply (subst bigo_plus_idemp [symmetric])
paulson@23449
  1050
  apply (rule set_plus_mono2)
paulson@23449
  1051
  apply assumption+
paulson@23449
  1052
done
paulson@23449
  1053
paulson@23449
  1054
lemma bigo_useful_add: "f =o O(h) ==> g =o O(h) ==> f + g =o O(h)"
paulson@23449
  1055
  apply (subst bigo_plus_idemp [symmetric])
paulson@23449
  1056
  apply (rule set_plus_intro)
paulson@23449
  1057
  apply assumption+
paulson@23449
  1058
done
paulson@23449
  1059
  
paulson@23449
  1060
lemma bigo_useful_const_mult: "(c::'a::ordered_field) ~= 0 ==> 
paulson@23449
  1061
    (%x. c) * f =o O(h) ==> f =o O(h)"
paulson@23449
  1062
  apply (rule subsetD)
paulson@23449
  1063
  apply (subgoal_tac "(%x. 1 / c) *o O(h) <= O(h)")
paulson@23449
  1064
  apply assumption
paulson@23449
  1065
  apply (rule bigo_const_mult6)
paulson@23449
  1066
  apply (subgoal_tac "f = (%x. 1 / c) * ((%x. c) * f)")
paulson@23449
  1067
  apply (erule ssubst)
paulson@23449
  1068
  apply (erule set_times_intro2)
paulson@23449
  1069
  apply (simp add: func_times) 
paulson@23449
  1070
done
paulson@23449
  1071
wenzelm@28592
  1072
ML_command{*AtpWrapper.problem_name := "BigO__bigo_fix"*}
paulson@23449
  1073
lemma bigo_fix: "(%x. f ((x::nat) + 1)) =o O(%x. h(x + 1)) ==> f 0 = 0 ==>
paulson@23449
  1074
    f =o O(h)"
paulson@23449
  1075
  apply (simp add: bigo_alt_def)
paulson@23449
  1076
(*sledgehammer*); 
paulson@23449
  1077
  apply clarify
paulson@23449
  1078
  apply (rule_tac x = c in exI)
paulson@23449
  1079
  apply safe
paulson@23449
  1080
  apply (case_tac "x = 0")
paulson@23816
  1081
apply (metis OrderedGroup.abs_ge_zero  OrderedGroup.abs_zero  order_less_le  Ring_and_Field.split_mult_pos_le) 
paulson@23449
  1082
  apply (subgoal_tac "x = Suc (x - 1)")
paulson@23816
  1083
  apply metis
paulson@23449
  1084
  apply simp
paulson@23449
  1085
  done
paulson@23449
  1086
paulson@23449
  1087
paulson@23449
  1088
lemma bigo_fix2: 
paulson@23449
  1089
    "(%x. f ((x::nat) + 1)) =o (%x. g(x + 1)) +o O(%x. h(x + 1)) ==> 
paulson@23449
  1090
       f 0 = g 0 ==> f =o g +o O(h)"
paulson@23449
  1091
  apply (rule set_minus_imp_plus)
paulson@23449
  1092
  apply (rule bigo_fix)
berghofe@26814
  1093
  apply (subst fun_diff_def)
berghofe@26814
  1094
  apply (subst fun_diff_def [symmetric])
paulson@23449
  1095
  apply (rule set_plus_imp_minus)
paulson@23449
  1096
  apply simp
berghofe@26814
  1097
  apply (simp add: fun_diff_def)
paulson@23449
  1098
done
paulson@23449
  1099
paulson@23449
  1100
subsection {* Less than or equal to *}
paulson@23449
  1101
paulson@23449
  1102
constdefs 
paulson@23449
  1103
  lesso :: "('a => 'b::ordered_idom) => ('a => 'b) => ('a => 'b)"
paulson@23449
  1104
      (infixl "<o" 70)
paulson@23449
  1105
  "f <o g == (%x. max (f x - g x) 0)"
paulson@23449
  1106
paulson@23449
  1107
lemma bigo_lesseq1: "f =o O(h) ==> ALL x. abs (g x) <= abs (f x) ==>
paulson@23449
  1108
    g =o O(h)"
paulson@23449
  1109
  apply (unfold bigo_def)
paulson@23449
  1110
  apply clarsimp
paulson@23449
  1111
apply (blast intro: order_trans) 
paulson@23449
  1112
done
paulson@23449
  1113
paulson@23449
  1114
lemma bigo_lesseq2: "f =o O(h) ==> ALL x. abs (g x) <= f x ==>
paulson@23449
  1115
      g =o O(h)"
paulson@23449
  1116
  apply (erule bigo_lesseq1)
paulson@23449
  1117
apply (blast intro: abs_ge_self order_trans) 
paulson@23449
  1118
done
paulson@23449
  1119
paulson@23449
  1120
lemma bigo_lesseq3: "f =o O(h) ==> ALL x. 0 <= g x ==> ALL x. g x <= f x ==>
paulson@23449
  1121
      g =o O(h)"
paulson@23449
  1122
  apply (erule bigo_lesseq2)
paulson@23449
  1123
  apply (rule allI)
paulson@23449
  1124
  apply (subst abs_of_nonneg)
paulson@23449
  1125
  apply (erule spec)+
paulson@23449
  1126
done
paulson@23449
  1127
paulson@23449
  1128
lemma bigo_lesseq4: "f =o O(h) ==>
paulson@23449
  1129
    ALL x. 0 <= g x ==> ALL x. g x <= abs (f x) ==>
paulson@23449
  1130
      g =o O(h)"
paulson@23449
  1131
  apply (erule bigo_lesseq1)
paulson@23449
  1132
  apply (rule allI)
paulson@23449
  1133
  apply (subst abs_of_nonneg)
paulson@23449
  1134
  apply (erule spec)+
paulson@23449
  1135
done
paulson@23449
  1136
wenzelm@28592
  1137
ML_command{*AtpWrapper.problem_name:="BigO__bigo_lesso1"*}
paulson@23449
  1138
lemma bigo_lesso1: "ALL x. f x <= g x ==> f <o g =o O(h)"
paulson@23449
  1139
  apply (unfold lesso_def)
paulson@23449
  1140
  apply (subgoal_tac "(%x. max (f x - g x) 0) = 0")
paulson@24937
  1141
(*??Translation of TSTP raised an exception: Type unification failed: Variable ?'X2.0::type not of sort ord*)
haftmann@25082
  1142
apply (metis bigo_zero)
paulson@23449
  1143
  apply (unfold func_zero)
paulson@23449
  1144
  apply (rule ext)
paulson@23449
  1145
  apply (simp split: split_max)
paulson@23449
  1146
done
paulson@23449
  1147
paulson@23449
  1148
wenzelm@28592
  1149
ML_command{*AtpWrapper.problem_name := "BigO__bigo_lesso2"*}
paulson@23449
  1150
lemma bigo_lesso2: "f =o g +o O(h) ==>
paulson@23449
  1151
    ALL x. 0 <= k x ==> ALL x. k x <= f x ==>
paulson@23449
  1152
      k <o g =o O(h)"
paulson@23449
  1153
  apply (unfold lesso_def)
paulson@23449
  1154
  apply (rule bigo_lesseq4)
paulson@23449
  1155
  apply (erule set_plus_imp_minus)
paulson@23449
  1156
  apply (rule allI)
paulson@23449
  1157
  apply (rule le_maxI2)
paulson@23449
  1158
  apply (rule allI)
berghofe@26814
  1159
  apply (subst fun_diff_def)
paulson@23449
  1160
apply (erule thin_rl)
paulson@23449
  1161
(*sledgehammer*);  
paulson@23449
  1162
  apply (case_tac "0 <= k x - g x")
paulson@24545
  1163
  prefer 2 (*re-order subgoals because I don't know what to put after a structured proof*)
haftmann@29511
  1164
   apply (metis abs_ge_zero abs_minus_commute linorder_linear min_max.sup_absorb1 min_max.sup_commute)
paulson@24545
  1165
proof (neg_clausify)
paulson@24545
  1166
fix x
paulson@24545
  1167
assume 0: "\<And>A. k A \<le> f A"
paulson@24545
  1168
have 1: "\<And>(X1\<Colon>'b\<Colon>ordered_idom) X2. \<not> max X1 X2 < X1"
paulson@24545
  1169
  by (metis linorder_not_less le_maxI1)  (*sort inserted by hand*)
paulson@24545
  1170
assume 2: "(0\<Colon>'b) \<le> k x - g x"
paulson@24545
  1171
have 3: "\<not> k x - g x < (0\<Colon>'b)"
paulson@24545
  1172
  by (metis 2 linorder_not_less)
paulson@24545
  1173
have 4: "\<And>X1 X2. min X1 (k X2) \<le> f X2"
haftmann@29511
  1174
  by (metis min_max.inf_le2 min_max.le_inf_iff min_max.le_iff_inf 0)
paulson@24545
  1175
have 5: "\<bar>g x - f x\<bar> = f x - g x"
haftmann@29511
  1176
  by (metis abs_minus_commute combine_common_factor mult_zero_right minus_add_cancel minus_zero abs_if diff_less_eq min_max.inf_commute 4 linorder_not_le min_max.le_iff_inf 3 diff_less_0_iff_less linorder_not_less)
paulson@24545
  1177
have 6: "max (0\<Colon>'b) (k x - g x) = k x - g x"
haftmann@29511
  1178
  by (metis min_max.le_iff_sup 2)
paulson@24545
  1179
assume 7: "\<not> max (k x - g x) (0\<Colon>'b) \<le> \<bar>f x - g x\<bar>"
paulson@24545
  1180
have 8: "\<not> k x - g x \<le> f x - g x"
haftmann@29511
  1181
  by (metis 5 abs_minus_commute 7 min_max.sup_commute 6)
paulson@24545
  1182
show "False"
haftmann@29511
  1183
  by (metis min_max.sup_commute min_max.inf_commute min_max.sup_inf_absorb min_max.le_iff_inf 0 max_diff_distrib_left 1 linorder_not_le 8)
paulson@24545
  1184
qed
paulson@23449
  1185
wenzelm@28592
  1186
ML_command{*AtpWrapper.problem_name := "BigO__bigo_lesso3"*}
paulson@23449
  1187
lemma bigo_lesso3: "f =o g +o O(h) ==>
paulson@23449
  1188
    ALL x. 0 <= k x ==> ALL x. g x <= k x ==>
paulson@23449
  1189
      f <o k =o O(h)"
paulson@23449
  1190
  apply (unfold lesso_def)
paulson@23449
  1191
  apply (rule bigo_lesseq4)
paulson@23449
  1192
  apply (erule set_plus_imp_minus)
paulson@23449
  1193
  apply (rule allI)
paulson@23449
  1194
  apply (rule le_maxI2)
paulson@23449
  1195
  apply (rule allI)
berghofe@26814
  1196
  apply (subst fun_diff_def)
paulson@23449
  1197
apply (erule thin_rl) 
paulson@23449
  1198
(*sledgehammer*); 
paulson@23449
  1199
  apply (case_tac "0 <= f x - k x")
nipkow@29667
  1200
  apply (simp)
paulson@23449
  1201
  apply (subst abs_of_nonneg)
paulson@23449
  1202
  apply (drule_tac x = x in spec) back
wenzelm@28592
  1203
ML_command{*AtpWrapper.problem_name := "BigO__bigo_lesso3_simpler"*}
paulson@24545
  1204
apply (metis diff_less_0_iff_less linorder_not_le not_leE uminus_add_conv_diff xt1(12) xt1(6))
paulson@24545
  1205
apply (metis add_minus_cancel diff_le_eq le_diff_eq uminus_add_conv_diff)
haftmann@29511
  1206
apply (metis abs_ge_zero linorder_linear min_max.sup_absorb1 min_max.sup_commute)
paulson@23449
  1207
done
paulson@23449
  1208
paulson@23449
  1209
lemma bigo_lesso4: "f <o g =o O(k::'a=>'b::ordered_field) ==>
paulson@23449
  1210
    g =o h +o O(k) ==> f <o h =o O(k)"
paulson@23449
  1211
  apply (unfold lesso_def)
paulson@23449
  1212
  apply (drule set_plus_imp_minus)
paulson@23449
  1213
  apply (drule bigo_abs5) back
berghofe@26814
  1214
  apply (simp add: fun_diff_def)
paulson@23449
  1215
  apply (drule bigo_useful_add)
paulson@23449
  1216
  apply assumption
paulson@23449
  1217
  apply (erule bigo_lesseq2) back
paulson@23449
  1218
  apply (rule allI)
nipkow@29667
  1219
  apply (auto simp add: func_plus fun_diff_def algebra_simps
paulson@23449
  1220
    split: split_max abs_split)
paulson@23449
  1221
done
paulson@23449
  1222
wenzelm@28592
  1223
ML_command{*AtpWrapper.problem_name := "BigO__bigo_lesso5"*}
paulson@23449
  1224
lemma bigo_lesso5: "f <o g =o O(h) ==>
paulson@23449
  1225
    EX C. ALL x. f x <= g x + C * abs(h x)"
paulson@23449
  1226
  apply (simp only: lesso_def bigo_alt_def)
paulson@23449
  1227
  apply clarsimp
paulson@24855
  1228
  apply (metis abs_if abs_mult add_commute diff_le_eq less_not_permute)  
paulson@23449
  1229
done
paulson@23449
  1230
paulson@23449
  1231
end