equal
deleted
inserted
replaced
130 apply (simp add: ring_distribs) |
130 apply (simp add: ring_distribs) |
131 apply (rule mult_left_mono) |
131 apply (rule mult_left_mono) |
132 apply (simp add: abs_triangle_ineq) |
132 apply (simp add: abs_triangle_ineq) |
133 apply (simp add: order_less_le) |
133 apply (simp add: order_less_le) |
134 apply (rule mult_nonneg_nonneg) |
134 apply (rule mult_nonneg_nonneg) |
135 apply (rule add_nonneg_nonneg) |
|
136 apply auto |
135 apply auto |
137 apply (rule_tac x = "%n. if (abs (f n)) < abs (g n) then x n else 0" |
136 apply (rule_tac x = "%n. if (abs (f n)) < abs (g n) then x n else 0" |
138 in exI) |
137 in exI) |
139 apply (rule conjI) |
138 apply (rule conjI) |
140 apply (rule_tac x = "c + c" in exI) |
139 apply (rule_tac x = "c + c" in exI) |
148 apply (simp add: ring_distribs) |
147 apply (simp add: ring_distribs) |
149 apply (rule mult_left_mono) |
148 apply (rule mult_left_mono) |
150 apply (rule abs_triangle_ineq) |
149 apply (rule abs_triangle_ineq) |
151 apply (simp add: order_less_le) |
150 apply (simp add: order_less_le) |
152 apply (rule mult_nonneg_nonneg) |
151 apply (rule mult_nonneg_nonneg) |
153 apply (rule add_nonneg_nonneg) |
152 apply (erule order_less_imp_le) |
154 apply (erule order_less_imp_le)+ |
153 apply simp |
155 apply simp |
|
156 apply (rule ext) |
|
157 apply (auto simp add: if_splits linorder_not_le) |
|
158 done |
154 done |
159 |
155 |
160 lemma bigo_plus_subset2 [intro]: "A <= O(f) ==> B <= O(f) ==> A \<oplus> B <= O(f)" |
156 lemma bigo_plus_subset2 [intro]: "A <= O(f) ==> B <= O(f) ==> A \<oplus> B <= O(f)" |
161 apply (subgoal_tac "A \<oplus> B <= O(f) \<oplus> O(f)") |
157 apply (subgoal_tac "A \<oplus> B <= O(f) \<oplus> O(f)") |
162 apply (erule order_trans) |
158 apply (erule order_trans) |