src/HOL/Library/BigO.thy
changeset 54863 82acc20ded73
parent 54230 b1d955791529
child 55821 44055f07cbd8
     1.1 --- a/src/HOL/Library/BigO.thy	Wed Dec 25 17:39:06 2013 +0100
     1.2 +++ b/src/HOL/Library/BigO.thy	Wed Dec 25 17:39:06 2013 +0100
     1.3 @@ -171,7 +171,7 @@
     1.4    apply (subgoal_tac "c <= max c ca")
     1.5    apply (erule order_less_le_trans)
     1.6    apply assumption
     1.7 -  apply (rule le_maxI1)
     1.8 +  apply (rule max.cobounded1)
     1.9    apply clarify
    1.10    apply (drule_tac x = "xa" in spec)+
    1.11    apply (subgoal_tac "0 <= f xa + g xa")
    1.12 @@ -184,12 +184,12 @@
    1.13    apply (subgoal_tac "c * f xa <= max c ca * f xa")
    1.14    apply (force)
    1.15    apply (rule mult_right_mono)
    1.16 -  apply (rule le_maxI1)
    1.17 +  apply (rule max.cobounded1)
    1.18    apply assumption
    1.19    apply (subgoal_tac "ca * g xa <= max c ca * g xa")
    1.20    apply (force)
    1.21    apply (rule mult_right_mono)
    1.22 -  apply (rule le_maxI2)
    1.23 +  apply (rule max.cobounded2)
    1.24    apply assumption
    1.25    apply (rule abs_triangle_ineq)
    1.26    apply (rule add_nonneg_nonneg)
    1.27 @@ -770,7 +770,7 @@
    1.28    apply (rule bigo_lesseq4)
    1.29    apply (erule set_plus_imp_minus)
    1.30    apply (rule allI)
    1.31 -  apply (rule le_maxI2)
    1.32 +  apply (rule max.cobounded2)
    1.33    apply (rule allI)
    1.34    apply (subst fun_diff_def)
    1.35    apply (case_tac "0 <= k x - g x")
    1.36 @@ -794,7 +794,7 @@
    1.37    apply (rule bigo_lesseq4)
    1.38    apply (erule set_plus_imp_minus)
    1.39    apply (rule allI)
    1.40 -  apply (rule le_maxI2)
    1.41 +  apply (rule max.cobounded2)
    1.42    apply (rule allI)
    1.43    apply (subst fun_diff_def)
    1.44    apply (case_tac "0 <= f x - k x")
    1.45 @@ -836,7 +836,7 @@
    1.46    apply (subgoal_tac "abs(max (f x - g x) 0) = max (f x - g x) 0")
    1.47    apply (clarsimp simp add: algebra_simps) 
    1.48    apply (rule abs_of_nonneg)
    1.49 -  apply (rule le_maxI2)
    1.50 +  apply (rule max.cobounded2)
    1.51    done
    1.52  
    1.53  lemma lesso_add: "f <o g =o O(h) ==>