39 apply (rule_tac x = "abs c" in exI, auto) |
39 apply (rule_tac x = "abs c" in exI, auto) |
40 proof - |
40 proof - |
41 fix c :: 'a and x :: 'b |
41 fix c :: 'a and x :: 'b |
42 assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>" |
42 assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>" |
43 have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 0 \<le> \<bar>x\<^isub>1\<bar>" by (metis abs_ge_zero) |
43 have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 0 \<le> \<bar>x\<^isub>1\<bar>" by (metis abs_ge_zero) |
44 have F2: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis normalizing.mul_1) |
44 have F2: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis mult_1) |
45 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) |
45 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) |
46 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>" |
46 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>" |
47 by (metis abs_mult) |
47 by (metis abs_mult) |
48 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" |
48 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" |
49 by (metis abs_mult_pos) |
49 by (metis abs_mult_pos) |
64 ALL x. (abs (h x)) <= (c * (abs (f x)))) |
64 ALL x. (abs (h x)) <= (c * (abs (f x)))) |
65 = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))" |
65 = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))" |
66 apply auto |
66 apply auto |
67 apply (case_tac "c = 0", simp) |
67 apply (case_tac "c = 0", simp) |
68 apply (rule_tac x = "1" in exI, simp) |
68 apply (rule_tac x = "1" in exI, simp) |
69 apply (rule_tac x = "abs c" in exI, auto); |
69 apply (rule_tac x = "abs c" in exI, auto) |
70 proof - |
70 proof - |
71 fix c :: 'a and x :: 'b |
71 fix c :: 'a and x :: 'b |
72 assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>" |
72 assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>" |
73 have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis normalizing.mul_1) |
73 have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis mult_1) |
74 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>" |
74 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>" |
75 by (metis abs_mult) |
75 by (metis abs_mult) |
76 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) |
76 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) |
77 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) |
77 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) |
78 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) |
78 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) |
90 apply (rule_tac x = "1" in exI, simp) |
90 apply (rule_tac x = "1" in exI, simp) |
91 apply (rule_tac x = "abs c" in exI, auto) |
91 apply (rule_tac x = "abs c" in exI, auto) |
92 proof - |
92 proof - |
93 fix c :: 'a and x :: 'b |
93 fix c :: 'a and x :: 'b |
94 assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>" |
94 assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>" |
95 have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis normalizing.mul_1) |
95 have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis mult_1) |
96 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) |
96 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) |
97 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) |
97 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) |
98 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) |
98 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) |
99 thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis A1 abs_mult abs_ge_zero) |
99 thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis A1 abs_mult abs_ge_zero) |
100 qed |
100 qed |
109 apply (rule_tac x = "1" in exI, simp) |
109 apply (rule_tac x = "1" in exI, simp) |
110 apply (rule_tac x = "abs c" in exI, auto) |
110 apply (rule_tac x = "abs c" in exI, auto) |
111 proof - |
111 proof - |
112 fix c :: 'a and x :: 'b |
112 fix c :: 'a and x :: 'b |
113 assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>" |
113 assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>" |
114 have "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis normalizing.mul_1) |
114 have "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis mult_1) |
115 hence "\<forall>x\<^isub>3. \<bar>c * \<bar>f x\<^isub>3\<bar>\<bar> = c * \<bar>f x\<^isub>3\<bar>" |
115 hence "\<forall>x\<^isub>3. \<bar>c * \<bar>f x\<^isub>3\<bar>\<bar> = c * \<bar>f x\<^isub>3\<bar>" |
116 by (metis A1 abs_ge_zero order_trans abs_mult_pos abs_one) |
116 by (metis A1 abs_ge_zero order_trans abs_mult_pos abs_one) |
117 hence "\<bar>h x\<bar> \<le> \<bar>c * f x\<bar>" by (metis A1 abs_ge_zero abs_mult_pos abs_mult) |
117 hence "\<bar>h x\<bar> \<le> \<bar>c * f x\<bar>" by (metis A1 abs_ge_zero abs_mult_pos abs_mult) |
118 thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis abs_mult) |
118 thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis abs_mult) |
119 qed |
119 qed |
129 apply (auto simp add: bigo_alt_def) |
129 apply (auto simp add: bigo_alt_def) |
130 apply (rule_tac x = "ca * c" in exI) |
130 apply (rule_tac x = "ca * c" in exI) |
131 apply (rule conjI) |
131 apply (rule conjI) |
132 apply (rule mult_pos_pos) |
132 apply (rule mult_pos_pos) |
133 apply (assumption)+ |
133 apply (assumption)+ |
134 (*sledgehammer*); |
134 (*sledgehammer*) |
135 apply (rule allI) |
135 apply (rule allI) |
136 apply (drule_tac x = "xa" in spec)+ |
136 apply (drule_tac x = "xa" in spec)+ |
137 apply (subgoal_tac "ca * abs(f xa) <= ca * (c * abs(g xa))"); |
137 apply (subgoal_tac "ca * abs(f xa) <= ca * (c * abs(g xa))") |
138 apply (erule order_trans) |
138 apply (erule order_trans) |
139 apply (simp add: mult_ac) |
139 apply (simp add: mult_ac) |
140 apply (rule mult_left_mono, assumption) |
140 apply (rule mult_left_mono, assumption) |
141 apply (rule order_less_imp_le, assumption); |
141 apply (rule order_less_imp_le, assumption) |
142 done |
142 done |
143 |
143 |
144 |
144 |
145 declare [[ atp_problem_prefix = "BigO__bigo_refl" ]] |
145 declare [[ atp_problem_prefix = "BigO__bigo_refl" ]] |
146 lemma bigo_refl [intro]: "f : O(f)" |
146 lemma bigo_refl [intro]: "f : O(f)" |
147 apply (auto simp add: bigo_def) |
147 apply (auto simp add: bigo_def) |
148 by (metis normalizing.mul_1 order_refl) |
148 by (metis mult_1 order_refl) |
149 |
149 |
150 declare [[ atp_problem_prefix = "BigO__bigo_zero" ]] |
150 declare [[ atp_problem_prefix = "BigO__bigo_zero" ]] |
151 lemma bigo_zero: "0 : O(g)" |
151 lemma bigo_zero: "0 : O(g)" |
152 apply (auto simp add: bigo_def func_zero) |
152 apply (auto simp add: bigo_def func_zero) |
153 by (metis normalizing.mul_0 order_refl) |
153 by (metis mult_zero_left order_refl) |
154 |
154 |
155 lemma bigo_zero2: "O(%x.0) = {%x.0}" |
155 lemma bigo_zero2: "O(%x.0) = {%x.0}" |
156 apply (auto simp add: bigo_def) |
156 apply (auto simp add: bigo_def) |
157 apply (rule ext) |
157 apply (rule ext) |
158 apply auto |
158 apply auto |
235 O(f + g) = O(f) \<oplus> O(g)" |
235 O(f + g) = O(f) \<oplus> O(g)" |
236 apply (rule equalityI) |
236 apply (rule equalityI) |
237 apply (rule bigo_plus_subset) |
237 apply (rule bigo_plus_subset) |
238 apply (simp add: bigo_alt_def set_plus_def func_plus) |
238 apply (simp add: bigo_alt_def set_plus_def func_plus) |
239 apply clarify |
239 apply clarify |
240 (*sledgehammer*); |
240 (*sledgehammer*) |
241 apply (rule_tac x = "max c ca" in exI) |
241 apply (rule_tac x = "max c ca" in exI) |
242 apply (rule conjI) |
242 apply (rule conjI) |
243 apply (metis Orderings.less_max_iff_disj) |
243 apply (metis Orderings.less_max_iff_disj) |
244 apply clarify |
244 apply clarify |
245 apply (drule_tac x = "xa" in spec)+ |
245 apply (drule_tac x = "xa" in spec)+ |
305 apply (rule set_minus_imp_plus) |
305 apply (rule set_minus_imp_plus) |
306 apply (rule bigo_bounded) |
306 apply (rule bigo_bounded) |
307 apply (auto simp add: diff_minus fun_Compl_def func_plus) |
307 apply (auto simp add: diff_minus fun_Compl_def func_plus) |
308 prefer 2 |
308 prefer 2 |
309 apply (drule_tac x = x in spec)+ |
309 apply (drule_tac x = x in spec)+ |
310 apply (metis add_right_mono normalizing.semiring_rules(24) diff_add_cancel diff_minus_eq_add le_less order_trans) |
310 apply (metis add_right_mono add_commute diff_add_cancel diff_minus_eq_add le_less order_trans) |
311 proof - |
311 proof - |
312 fix x :: 'a |
312 fix x :: 'a |
313 assume "\<forall>x. lb x \<le> f x" |
313 assume "\<forall>x. lb x \<le> f x" |
314 thus "(0\<Colon>'b) \<le> f x + - lb x" by (metis not_leE diff_minus less_iff_diff_less_0 less_le_not_le) |
314 thus "(0\<Colon>'b) \<le> f x + - lb x" by (metis not_leE diff_minus less_iff_diff_less_0 less_le_not_le) |
315 qed |
315 qed |
316 |
316 |
317 declare [[ atp_problem_prefix = "BigO__bigo_abs" ]] |
317 declare [[ atp_problem_prefix = "BigO__bigo_abs" ]] |
318 lemma bigo_abs: "(%x. abs(f x)) =o O(f)" |
318 lemma bigo_abs: "(%x. abs(f x)) =o O(f)" |
319 apply (unfold bigo_def) |
319 apply (unfold bigo_def) |
320 apply auto |
320 apply auto |
321 by (metis normalizing.mul_1 order_refl) |
321 by (metis mult_1 order_refl) |
322 |
322 |
323 declare [[ atp_problem_prefix = "BigO__bigo_abs2" ]] |
323 declare [[ atp_problem_prefix = "BigO__bigo_abs2" ]] |
324 lemma bigo_abs2: "f =o O(%x. abs(f x))" |
324 lemma bigo_abs2: "f =o O(%x. abs(f x))" |
325 apply (unfold bigo_def) |
325 apply (unfold bigo_def) |
326 apply auto |
326 apply auto |
327 by (metis normalizing.mul_1 order_refl) |
327 by (metis mult_1 order_refl) |
328 |
328 |
329 lemma bigo_abs3: "O(f) = O(%x. abs(f x))" |
329 lemma bigo_abs3: "O(f) = O(%x. abs(f x))" |
330 proof - |
330 proof - |
331 have F1: "\<forall>v u. u \<in> O(v) \<longrightarrow> O(u) \<subseteq> O(v)" by (metis bigo_elt_subset) |
331 have F1: "\<forall>v u. u \<in> O(v) \<longrightarrow> O(u) \<subseteq> O(v)" by (metis bigo_elt_subset) |
332 have F2: "\<forall>u. (\<lambda>R. \<bar>u R\<bar>) \<in> O(u)" by (metis bigo_abs) |
332 have F2: "\<forall>u. (\<lambda>R. \<bar>u R\<bar>) \<in> O(u)" by (metis bigo_abs) |