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.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))