162 apply (subst bigo_pos_const [symmetric])+ |
162 apply (subst bigo_pos_const [symmetric])+ |
163 apply (rule_tac x = "\<lambda>n. if abs (g n) <= (abs (f n)) then x n else 0" in exI) |
163 apply (rule_tac x = "\<lambda>n. if abs (g n) <= (abs (f n)) then x n else 0" in exI) |
164 apply (rule conjI) |
164 apply (rule conjI) |
165 apply (rule_tac x = "c + c" in exI) |
165 apply (rule_tac x = "c + c" in exI) |
166 apply clarsimp |
166 apply clarsimp |
167 apply auto |
167 apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (f xa)") |
168 apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (f xa)") |
168 apply (metis mult_2 order_trans) |
169 apply (metis mult_2 order_trans) |
169 apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))") |
170 apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))") |
170 apply (erule order_trans) |
171 apply (erule order_trans) |
171 apply (simp add: ring_distribs) |
172 apply (simp add: ring_distribs) |
172 apply (rule mult_left_mono) |
173 apply (rule mult_left_mono) |
173 apply (simp add: abs_triangle_ineq) |
174 apply (simp add: abs_triangle_ineq) |
174 apply (simp add: order_less_le) |
175 apply (simp add: order_less_le) |
|
176 apply (rule mult_nonneg_nonneg) |
|
177 apply auto |
|
178 apply (rule_tac x = "\<lambda>n. if (abs (f n)) < abs (g n) then x n else 0" in exI) |
175 apply (rule_tac x = "\<lambda>n. if (abs (f n)) < abs (g n) then x n else 0" in exI) |
179 apply (rule conjI) |
176 apply (rule conjI) |
180 apply (rule_tac x = "c + c" in exI) |
177 apply (rule_tac x = "c + c" in exI) |
181 apply auto |
178 apply auto |
182 apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (g xa)") |
179 apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (g xa)") |
183 apply (metis order_trans mult_2) |
180 apply (metis order_trans mult_2) |
184 apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))") |
181 apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))") |
185 apply (erule order_trans) |
182 apply (erule order_trans) |
186 apply (simp add: ring_distribs) |
183 apply (simp add: ring_distribs) |
187 apply (metis abs_triangle_ineq mult_le_cancel_left_pos) |
184 by (metis abs_triangle_ineq mult_le_cancel_left_pos) |
188 by (metis abs_ge_zero abs_of_pos zero_le_mult_iff) |
|
189 |
185 |
190 lemma bigo_plus_subset2 [intro]: "A <= O(f) \<Longrightarrow> B <= O(f) \<Longrightarrow> A + B <= O(f)" |
186 lemma bigo_plus_subset2 [intro]: "A <= O(f) \<Longrightarrow> B <= O(f) \<Longrightarrow> A + B <= O(f)" |
191 by (metis bigo_plus_idemp set_plus_mono2) |
187 by (metis bigo_plus_idemp set_plus_mono2) |
192 |
188 |
193 lemma bigo_plus_eq: "\<forall>x. 0 <= f x \<Longrightarrow> \<forall>x. 0 <= g x \<Longrightarrow> O(f + g) = O(f) + O(g)" |
189 lemma bigo_plus_eq: "\<forall>x. 0 <= f x \<Longrightarrow> \<forall>x. 0 <= g x \<Longrightarrow> O(f + g) = O(f) + O(g)" |