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)"
```