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.15        apply (simp add: func_times)
    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.22  by (metis bigo_add_commute_imp)
    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)"