equal
deleted
inserted
replaced
90 apply (rule_tac x = 0 in exI) |
90 apply (rule_tac x = 0 in exI) |
91 apply auto |
91 apply auto |
92 done |
92 done |
93 |
93 |
94 lemma bigo_zero2: "O(%x.0) = {%x.0}" |
94 lemma bigo_zero2: "O(%x.0) = {%x.0}" |
95 apply (auto simp add: bigo_def) |
95 by (auto simp add: bigo_def) |
96 apply (rule ext) |
|
97 apply auto |
|
98 done |
|
99 |
96 |
100 lemma bigo_plus_self_subset [intro]: |
97 lemma bigo_plus_self_subset [intro]: |
101 "O(f) \<oplus> O(f) <= O(f)" |
98 "O(f) \<oplus> O(f) <= O(f)" |
102 apply (auto simp add: bigo_alt_def set_plus_def) |
99 apply (auto simp add: bigo_alt_def set_plus_def) |
103 apply (rule_tac x = "c + ca" in exI) |
100 apply (rule_tac x = "c + ca" in exI) |