src/HOL/Metis_Examples/BigO.thy
 changeset 35050 9f841f20dca6 parent 35028 108662d50512 child 35416 d8d7d1b785af
```     1.1 --- a/src/HOL/Metis_Examples/BigO.thy	Mon Feb 08 17:12:32 2010 +0100
1.2 +++ b/src/HOL/Metis_Examples/BigO.thy	Mon Feb 08 17:12:38 2010 +0100
1.3 @@ -368,7 +368,7 @@
1.4      f : O(g)"
1.5    apply (auto simp add: bigo_def)
1.6  (*Version 1: one-shot proof*)
1.7 -  apply (metis OrderedGroup.abs_le_D1 linorder_class.not_less  order_less_le  Orderings.xt1(12)  Ring_and_Field.abs_mult)
1.8 +  apply (metis abs_le_D1 linorder_class.not_less  order_less_le  Orderings.xt1(12)  abs_mult)
1.9    done
1.10
1.11  lemma (*bigo_bounded_alt:*) "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==>
1.12 @@ -595,8 +595,8 @@
1.13  using [[ atp_problem_prefix = "BigO__bigo_mult_simpler" ]]
1.14  prefer 2
1.15  apply (metis mult_assoc mult_left_commute
1.16 -  OrderedGroup.abs_of_pos OrderedGroup.mult_left_commute
1.17 -  Ring_and_Field.abs_mult Ring_and_Field.mult_pos_pos)
1.18 +  abs_of_pos mult_left_commute
1.19 +  abs_mult mult_pos_pos)
1.20    apply (erule ssubst)
1.21    apply (subst abs_mult)
1.22  (*not qute BigO__bigo_mult_simpler_1 (a hard problem!) as abs_mult has
1.23 @@ -613,32 +613,32 @@
1.24    \<le> (c\<Colon>'b\<Colon>linordered_idom) * \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar> *
1.25      ((ca\<Colon>'b\<Colon>linordered_idom) * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar>)"
1.26  have 4: "\<bar>c\<Colon>'b\<Colon>linordered_idom\<bar> = c"
1.27 -  by (metis OrderedGroup.abs_of_pos 0)
1.28 +  by (metis abs_of_pos 0)
1.29  have 5: "\<And>X1\<Colon>'b\<Colon>linordered_idom. (c\<Colon>'b\<Colon>linordered_idom) * \<bar>X1\<bar> = \<bar>c * X1\<bar>"
1.30 -  by (metis Ring_and_Field.abs_mult 4)
1.31 +  by (metis abs_mult 4)
1.32  have 6: "(0\<Colon>'b\<Colon>linordered_idom) = (1\<Colon>'b\<Colon>linordered_idom) \<or>
1.33  (0\<Colon>'b\<Colon>linordered_idom) < (1\<Colon>'b\<Colon>linordered_idom)"
1.34 -  by (metis OrderedGroup.abs_not_less_zero Ring_and_Field.abs_one Ring_and_Field.linorder_neqE_linordered_idom)
1.35 +  by (metis abs_not_less_zero abs_one linorder_neqE_linordered_idom)
1.36  have 7: "(0\<Colon>'b\<Colon>linordered_idom) < (1\<Colon>'b\<Colon>linordered_idom)"
1.37 -  by (metis 6 Ring_and_Field.one_neq_zero)
1.38 +  by (metis 6 one_neq_zero)
1.39  have 8: "\<bar>1\<Colon>'b\<Colon>linordered_idom\<bar> = (1\<Colon>'b\<Colon>linordered_idom)"
1.40 -  by (metis OrderedGroup.abs_of_pos 7)
1.41 +  by (metis abs_of_pos 7)
1.42  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>"
1.43 -  by (metis OrderedGroup.abs_ge_zero 5)
1.44 +  by (metis abs_ge_zero 5)
1.45  have 10: "\<And>X1\<Colon>'b\<Colon>linordered_idom. X1 * (1\<Colon>'b\<Colon>linordered_idom) = X1"
1.46 -  by (metis Ring_and_Field.mult_cancel_right2 mult_commute)
1.47 +  by (metis mult_cancel_right2 mult_commute)
1.48  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>"
1.49 -  by (metis Ring_and_Field.abs_mult OrderedGroup.abs_idempotent 10)
1.50 +  by (metis abs_mult abs_idempotent 10)
1.51  have 12: "\<And>X1\<Colon>'b\<Colon>linordered_idom. \<bar>\<bar>X1\<bar>\<bar> = \<bar>X1\<bar>"
1.52    by (metis 11 8 10)
1.53  have 13: "\<And>X1\<Colon>'b\<Colon>linordered_idom. (0\<Colon>'b\<Colon>linordered_idom) \<le> \<bar>X1\<bar>"
1.54 -  by (metis OrderedGroup.abs_ge_zero 12)
1.55 +  by (metis abs_ge_zero 12)
1.56  have 14: "\<not> (0\<Colon>'b\<Colon>linordered_idom)
1.57    \<le> (c\<Colon>'b\<Colon>linordered_idom) * \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) (x\<Colon>'a)\<bar> \<or>
1.58  \<not> (0\<Colon>'b\<Colon>linordered_idom) \<le> \<bar>(b\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar> \<or>
1.59  \<not> \<bar>b x\<bar> \<le> (ca\<Colon>'b\<Colon>linordered_idom) * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar> \<or>
1.60  \<not> \<bar>(a\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar> \<le> c * \<bar>f x\<bar>"
1.61 -  by (metis 3 Ring_and_Field.mult_mono)
1.62 +  by (metis 3 mult_mono)
1.63  have 15: "\<not> (0\<Colon>'b\<Colon>linordered_idom) \<le> \<bar>(b\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) (x\<Colon>'a)\<bar> \<or>
1.64  \<not> \<bar>b x\<bar> \<le> (ca\<Colon>'b\<Colon>linordered_idom) * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar> \<or>
1.65  \<not> \<bar>(a\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar>
1.66 @@ -1078,7 +1078,7 @@
1.67    apply (rule_tac x = c in exI)
1.68    apply safe
1.69    apply (case_tac "x = 0")
1.70 -apply (metis OrderedGroup.abs_ge_zero  OrderedGroup.abs_zero  order_less_le  Ring_and_Field.split_mult_pos_le)
1.71 +apply (metis abs_ge_zero  abs_zero  order_less_le  split_mult_pos_le)
1.72    apply (subgoal_tac "x = Suc (x - 1)")
1.73    apply metis
1.74    apply simp
```