--- a/src/HOL/Metis_Examples/BigO.thy Mon Feb 08 17:12:32 2010 +0100
+++ b/src/HOL/Metis_Examples/BigO.thy Mon Feb 08 17:12:38 2010 +0100
@@ -368,7 +368,7 @@
f : O(g)"
apply (auto simp add: bigo_def)
(*Version 1: one-shot proof*)
- apply (metis OrderedGroup.abs_le_D1 linorder_class.not_less order_less_le Orderings.xt1(12) Ring_and_Field.abs_mult)
+ apply (metis abs_le_D1 linorder_class.not_less order_less_le Orderings.xt1(12) abs_mult)
done
lemma (*bigo_bounded_alt:*) "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==>
@@ -595,8 +595,8 @@
using [[ atp_problem_prefix = "BigO__bigo_mult_simpler" ]]
prefer 2
apply (metis mult_assoc mult_left_commute
- OrderedGroup.abs_of_pos OrderedGroup.mult_left_commute
- Ring_and_Field.abs_mult Ring_and_Field.mult_pos_pos)
+ abs_of_pos mult_left_commute
+ abs_mult mult_pos_pos)
apply (erule ssubst)
apply (subst abs_mult)
(*not qute BigO__bigo_mult_simpler_1 (a hard problem!) as abs_mult has
@@ -613,32 +613,32 @@
\<le> (c\<Colon>'b\<Colon>linordered_idom) * \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar> *
((ca\<Colon>'b\<Colon>linordered_idom) * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar>)"
have 4: "\<bar>c\<Colon>'b\<Colon>linordered_idom\<bar> = c"
- by (metis OrderedGroup.abs_of_pos 0)
+ by (metis abs_of_pos 0)
have 5: "\<And>X1\<Colon>'b\<Colon>linordered_idom. (c\<Colon>'b\<Colon>linordered_idom) * \<bar>X1\<bar> = \<bar>c * X1\<bar>"
- by (metis Ring_and_Field.abs_mult 4)
+ by (metis abs_mult 4)
have 6: "(0\<Colon>'b\<Colon>linordered_idom) = (1\<Colon>'b\<Colon>linordered_idom) \<or>
(0\<Colon>'b\<Colon>linordered_idom) < (1\<Colon>'b\<Colon>linordered_idom)"
- by (metis OrderedGroup.abs_not_less_zero Ring_and_Field.abs_one Ring_and_Field.linorder_neqE_linordered_idom)
+ by (metis abs_not_less_zero abs_one linorder_neqE_linordered_idom)
have 7: "(0\<Colon>'b\<Colon>linordered_idom) < (1\<Colon>'b\<Colon>linordered_idom)"
- by (metis 6 Ring_and_Field.one_neq_zero)
+ by (metis 6 one_neq_zero)
have 8: "\<bar>1\<Colon>'b\<Colon>linordered_idom\<bar> = (1\<Colon>'b\<Colon>linordered_idom)"
- by (metis OrderedGroup.abs_of_pos 7)
+ by (metis abs_of_pos 7)
have 9: "\<And>X1\<Colon>'b\<Colon>linordered_idom. (0\<Colon>'b\<Colon>linordered_idom) \<le> (c\<Colon>'b\<Colon>linordered_idom) * \<bar>X1\<bar>"
- by (metis OrderedGroup.abs_ge_zero 5)
+ by (metis abs_ge_zero 5)
have 10: "\<And>X1\<Colon>'b\<Colon>linordered_idom. X1 * (1\<Colon>'b\<Colon>linordered_idom) = X1"
- by (metis Ring_and_Field.mult_cancel_right2 mult_commute)
+ by (metis mult_cancel_right2 mult_commute)
have 11: "\<And>X1\<Colon>'b\<Colon>linordered_idom. \<bar>\<bar>X1\<bar>\<bar> = \<bar>X1\<bar> * \<bar>1\<Colon>'b\<Colon>linordered_idom\<bar>"
- by (metis Ring_and_Field.abs_mult OrderedGroup.abs_idempotent 10)
+ by (metis abs_mult abs_idempotent 10)
have 12: "\<And>X1\<Colon>'b\<Colon>linordered_idom. \<bar>\<bar>X1\<bar>\<bar> = \<bar>X1\<bar>"
by (metis 11 8 10)
have 13: "\<And>X1\<Colon>'b\<Colon>linordered_idom. (0\<Colon>'b\<Colon>linordered_idom) \<le> \<bar>X1\<bar>"
- by (metis OrderedGroup.abs_ge_zero 12)
+ by (metis abs_ge_zero 12)
have 14: "\<not> (0\<Colon>'b\<Colon>linordered_idom)
\<le> (c\<Colon>'b\<Colon>linordered_idom) * \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) (x\<Colon>'a)\<bar> \<or>
\<not> (0\<Colon>'b\<Colon>linordered_idom) \<le> \<bar>(b\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar> \<or>
\<not> \<bar>b x\<bar> \<le> (ca\<Colon>'b\<Colon>linordered_idom) * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar> \<or>
\<not> \<bar>(a\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar> \<le> c * \<bar>f x\<bar>"
- by (metis 3 Ring_and_Field.mult_mono)
+ by (metis 3 mult_mono)
have 15: "\<not> (0\<Colon>'b\<Colon>linordered_idom) \<le> \<bar>(b\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) (x\<Colon>'a)\<bar> \<or>
\<not> \<bar>b x\<bar> \<le> (ca\<Colon>'b\<Colon>linordered_idom) * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar> \<or>
\<not> \<bar>(a\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar>
@@ -1078,7 +1078,7 @@
apply (rule_tac x = c in exI)
apply safe
apply (case_tac "x = 0")
-apply (metis OrderedGroup.abs_ge_zero OrderedGroup.abs_zero order_less_le Ring_and_Field.split_mult_pos_le)
+apply (metis abs_ge_zero abs_zero order_less_le split_mult_pos_le)
apply (subgoal_tac "x = Suc (x - 1)")
apply metis
apply simp