src/HOL/MetisExamples/BigO.thy
changeset 25304 7491c00f0915
parent 25087 5908591fb881
child 25592 e8ddaf6bf5df
     1.1 --- a/src/HOL/MetisExamples/BigO.thy	Tue Nov 06 08:47:25 2007 +0100
     1.2 +++ b/src/HOL/MetisExamples/BigO.thy	Tue Nov 06 08:47:30 2007 +0100
     1.3 @@ -25,8 +25,8 @@
     1.4    apply auto
     1.5    apply (case_tac "c = 0", simp)
     1.6    apply (rule_tac x = "1" in exI, simp)
     1.7 -  apply (rule_tac x = "abs c" in exI, auto);
     1.8 -  apply (metis abs_ge_minus_self abs_ge_zero abs_minus_cancel abs_of_nonneg equation_minus_iff Orderings.xt1(6) abs_le_mult)
     1.9 +  apply (rule_tac x = "abs c" in exI, auto)
    1.10 +  apply (metis abs_ge_minus_self abs_ge_zero abs_minus_cancel abs_of_nonneg equation_minus_iff Orderings.xt1(6) abs_mult)
    1.11    done
    1.12  
    1.13  (*** Now various verions with an increasing modulus ***)
    1.14 @@ -858,11 +858,12 @@
    1.15    apply (simp add: bigo_def abs_mult)
    1.16  proof (neg_clausify)
    1.17  fix x
    1.18 -assume 0: "\<And>xa. \<not> \<bar>c\<bar> * \<bar>f (x xa)\<bar> \<le> xa * \<bar>f (x xa)\<bar>"
    1.19 -have 1: "\<And>X2. \<not> \<bar>c * f (x X2)\<bar> \<le> X2 * \<bar>f (x X2)\<bar>"
    1.20 -  by (metis 0 abs_mult)
    1.21 +assume 0: "\<And>xa\<Colon>'b\<Colon>ordered_idom.
    1.22 +   \<not> \<bar>c\<Colon>'b\<Colon>ordered_idom\<bar> *
    1.23 +     \<bar>(f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a\<Colon>type) xa)\<bar>
    1.24 +     \<le> xa * \<bar>f (x xa)\<bar>"
    1.25  show "False"
    1.26 -  by (metis 1 abs_le_mult)
    1.27 +  by (metis linorder_neq_iff linorder_antisym_conv1 0)
    1.28  qed
    1.29  
    1.30  lemma bigo_const_mult2: "O(%x. c * f x) <= O(f)"