src/HOL/Metis_Examples/Big_O.thy
 changeset 57514 bdc2c6b40bf2 parent 57512 cc97b347b301 child 58889 5b7a9633cfa8
```     1.1 --- a/src/HOL/Metis_Examples/Big_O.thy	Sat Jul 05 10:09:01 2014 +0200
1.2 +++ b/src/HOL/Metis_Examples/Big_O.thy	Sat Jul 05 11:01:53 2014 +0200
1.3 @@ -301,7 +301,7 @@
1.4  lemma bigo_mult [intro]: "O(f) * O(g) <= O(f * g)"
1.5  apply (rule subsetI)
1.6  apply (subst bigo_def)
1.7 -apply (auto simp del: abs_mult mult_ac
1.8 +apply (auto simp del: abs_mult ac_simps
1.9              simp add: bigo_alt_def set_times_def func_times)
1.10  (* sledgehammer *)
1.11  apply (rule_tac x = "c * ca" in exI)
1.12 @@ -334,7 +334,7 @@
1.13        by (rule bigo_mult2)
1.14      also have "(\<lambda>x. 1 / f x) * (f * g) = g"
1.16 -      by (metis (lifting, no_types) a ext mult_ac(2) nonzero_divide_eq_eq)
1.17 +      by (metis (lifting, no_types) a ext mult.commute nonzero_divide_eq_eq)
1.18      finally have "(\<lambda>x. (1\<Colon>'b) / f x) * h : O(g)".
1.19      then have "f * ((\<lambda>x. (1\<Colon>'b) / f x) * h) : f *o O(g)"
1.20        by auto
1.21 @@ -396,7 +396,7 @@
1.23
1.24  lemma bigo_const1: "(\<lambda>x. c) : O(\<lambda>x. 1)"
1.25 -by (auto simp add: bigo_def mult_ac)
1.26 +by (auto simp add: bigo_def ac_simps)
1.27
1.28  lemma bigo_const2 [intro]: "O(\<lambda>x. c) \<le> O(\<lambda>x. 1)"
1.29  by (metis bigo_const1 bigo_elt_subset)
1.30 @@ -462,13 +462,13 @@
1.31    hence "\<exists>(v\<Colon>'a) (u\<Colon>'a) SKF\<^sub>7\<Colon>'a \<Rightarrow> 'b. \<bar>inverse c\<bar> * \<bar>g (SKF\<^sub>7 (u * v))\<bar> \<le> u * (v * \<bar>f (SKF\<^sub>7 (u * v))\<bar>)"
1.32      by (metis comm_mult_left_mono)
1.33    thus "\<exists>ca\<Colon>'a. \<forall>x\<Colon>'b. \<bar>inverse c\<bar> * \<bar>g x\<bar> \<le> ca * \<bar>f x\<bar>"
1.34 -    using A2 F4 by (metis ab_semigroup_mult_class.mult_ac(1) comm_mult_left_mono)
1.35 +    using A2 F4 by (metis mult.assoc comm_mult_left_mono)
1.36  qed
1.37
1.38  lemma bigo_const_mult6 [intro]: "(\<lambda>x. c) *o O(f) <= O(f)"
1.39    apply (auto intro!: subsetI
1.40      simp add: bigo_def elt_set_times_def func_times
1.41 -    simp del: abs_mult mult_ac)
1.42 +    simp del: abs_mult ac_simps)
1.43  (* sledgehammer *)
1.44    apply (rule_tac x = "ca * (abs c)" in exI)
1.45    apply (rule allI)
1.46 @@ -478,7 +478,7 @@
1.47    apply (rule mult_left_mono)
1.48    apply (erule spec)
1.49    apply simp
1.50 -  apply (simp add: mult_ac)
1.51 +  apply (simp add: ac_simps)
1.52  done
1.53
1.54  lemma bigo_const_mult7 [intro]: "f =o O(g) \<Longrightarrow> (\<lambda>x. c * f x) =o O(g)"
```