src/HOL/Library/BigO.thy
changeset 59867 58043346ca64
parent 58881 b9556a055632
child 60141 833adf7db7d8
     1.1 --- a/src/HOL/Library/BigO.thy	Tue Mar 31 16:49:41 2015 +0100
     1.2 +++ b/src/HOL/Library/BigO.thy	Tue Mar 31 21:54:32 2015 +0200
     1.3 @@ -489,7 +489,7 @@
     1.4    shows "c \<noteq> 0 \<Longrightarrow> f \<in> O(\<lambda>x. c * f x)"
     1.5    apply (simp add: bigo_def)
     1.6    apply (rule_tac x = "abs (inverse c)" in exI)
     1.7 -  apply (simp add: abs_mult [symmetric] mult.assoc [symmetric])
     1.8 +  apply (simp add: abs_mult mult.assoc [symmetric])
     1.9    done
    1.10  
    1.11  lemma bigo_const_mult4:
    1.12 @@ -519,11 +519,7 @@
    1.13    apply (rule_tac x = "\<lambda>y. inverse c * x y" in exI)
    1.14    apply (simp add: mult.assoc [symmetric] abs_mult)
    1.15    apply (rule_tac x = "abs (inverse c) * ca" in exI)
    1.16 -  apply (rule allI)
    1.17 -  apply (subst mult.assoc)
    1.18 -  apply (rule mult_left_mono)
    1.19 -  apply (erule spec)
    1.20 -  apply force
    1.21 +  apply auto
    1.22    done
    1.23  
    1.24  lemma bigo_const_mult6 [intro]: "(\<lambda>x. c) *o O(f) \<subseteq> O(f)"