src/HOL/Metis_Examples/Big_O.thy
changeset 54863 82acc20ded73
parent 54230 b1d955791529
child 55183 17ec4a29ef71
     1.1 --- a/src/HOL/Metis_Examples/Big_O.thy	Wed Dec 25 17:39:06 2013 +0100
     1.2 +++ b/src/HOL/Metis_Examples/Big_O.thy	Wed Dec 25 17:39:06 2013 +0100
     1.3 @@ -212,8 +212,8 @@
     1.4    apply (metis abs_triangle_ineq)
     1.5   apply (metis add_nonneg_nonneg)
     1.6  apply (rule add_mono)
     1.7 - apply (metis le_maxI2 linorder_linear min_max.sup_absorb1 mult_right_mono xt1(6))
     1.8 -by (metis le_maxI2 linorder_not_le mult_le_cancel_right order_trans)
     1.9 + apply (metis max.cobounded2 linorder_linear max.absorb1 mult_right_mono xt1(6))
    1.10 +by (metis max.cobounded2 linorder_not_le mult_le_cancel_right order_trans)
    1.11  
    1.12  lemma bigo_bounded_alt: "\<forall>x. 0 <= f x \<Longrightarrow> \<forall>x. f x <= c * g x \<Longrightarrow> f : O(g)"
    1.13  apply (auto simp add: bigo_def)
    1.14 @@ -658,7 +658,7 @@
    1.15  apply (subgoal_tac "(\<lambda>x. max (f x - g x) 0) = 0")
    1.16   apply (metis bigo_zero)
    1.17  by (metis (lifting, no_types) func_zero le_fun_def le_iff_diff_le_0
    1.18 -      min_max.sup_absorb2 order_eq_iff)
    1.19 +      max.absorb2 order_eq_iff)
    1.20  
    1.21  lemma bigo_lesso2: "f =o g +o O(h) \<Longrightarrow>
    1.22      \<forall>x. 0 <= k x \<Longrightarrow> \<forall>x. k x <= f x \<Longrightarrow>
    1.23 @@ -667,15 +667,15 @@
    1.24    apply (rule bigo_lesseq4)
    1.25    apply (erule set_plus_imp_minus)
    1.26    apply (rule allI)
    1.27 -  apply (rule le_maxI2)
    1.28 +  apply (rule max.cobounded2)
    1.29    apply (rule allI)
    1.30    apply (subst fun_diff_def)
    1.31  apply (erule thin_rl)
    1.32  (* sledgehammer *)
    1.33  apply (case_tac "0 <= k x - g x")
    1.34   apply (metis (lifting) abs_le_D1 linorder_linear min_diff_distrib_left
    1.35 -          min_max.inf_absorb1 min_max.inf_absorb2 min_max.sup_absorb1)
    1.36 -by (metis abs_ge_zero le_cases min_max.sup_absorb2)
    1.37 +          min.absorb1 min.absorb2 max.absorb1)
    1.38 +by (metis abs_ge_zero le_cases max.absorb2)
    1.39  
    1.40  lemma bigo_lesso3: "f =o g +o O(h) \<Longrightarrow>
    1.41      \<forall>x. 0 <= k x \<Longrightarrow> \<forall>x. g x <= k x \<Longrightarrow>
    1.42 @@ -684,7 +684,7 @@
    1.43  apply (rule bigo_lesseq4)
    1.44    apply (erule set_plus_imp_minus)
    1.45   apply (rule allI)
    1.46 - apply (rule le_maxI2)
    1.47 + apply (rule max.cobounded2)
    1.48  apply (rule allI)
    1.49  apply (subst fun_diff_def)
    1.50  apply (erule thin_rl)
    1.51 @@ -695,7 +695,7 @@
    1.52    apply (drule_tac x = x in spec) back
    1.53    apply (metis diff_less_0_iff_less linorder_not_le not_leE xt1(12) xt1(6))
    1.54   apply (metis add_minus_cancel diff_le_eq le_diff_eq uminus_add_conv_diff)
    1.55 -by (metis abs_ge_zero linorder_linear min_max.sup_absorb1 min_max.sup_commute)
    1.56 +by (metis abs_ge_zero linorder_linear max.absorb1 max.commute)
    1.57  
    1.58  lemma bigo_lesso4:
    1.59    "f <o g =o O(k\<Colon>'a=>'b\<Colon>{linordered_field}) \<Longrightarrow>