Mercurialisabelle / diff
summary | shortlog | changelog | graph | tags | branches | files | changeset | file | revisions | annotate | diff | raw
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
isabelle