src/HOL/Metis_Examples/Big_O.thy
changeset 47108 2a1953f0d20d
parent 46644 bd03e0890699
child 47445 69e96e5500df
     1.1 --- a/src/HOL/Metis_Examples/Big_O.thy	Sat Mar 24 16:27:04 2012 +0100
     1.2 +++ b/src/HOL/Metis_Examples/Big_O.thy	Sun Mar 25 20:15:39 2012 +0200
     1.3 @@ -16,7 +16,7 @@
     1.4  
     1.5  subsection {* Definitions *}
     1.6  
     1.7 -definition bigo :: "('a => 'b\<Colon>{linordered_idom,number_ring}) => ('a => 'b) set" ("(1O'(_'))") where
     1.8 +definition bigo :: "('a => 'b\<Colon>linordered_idom) => ('a => 'b) set" ("(1O'(_'))") where
     1.9    "O(f\<Colon>('a => 'b)) == {h. \<exists>c. \<forall>x. abs (h x) <= c * abs (f x)}"
    1.10  
    1.11  lemma bigo_pos_const:
    1.12 @@ -180,7 +180,7 @@
    1.13   apply (rule_tac x = "c + c" in exI)
    1.14   apply auto
    1.15   apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (g xa)")
    1.16 -  apply (metis order_trans semiring_mult_2)
    1.17 +  apply (metis order_trans mult_2)
    1.18   apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))")
    1.19    apply (erule order_trans)
    1.20    apply (simp add: ring_distribs)
    1.21 @@ -325,7 +325,7 @@
    1.22  by (metis bigo_mult2 set_plus_mono_b set_times_intro2 set_times_plus_distrib)
    1.23  
    1.24  lemma bigo_mult5: "\<forall>x. f x ~= 0 \<Longrightarrow>
    1.25 -    O(f * g) <= (f\<Colon>'a => ('b\<Colon>{linordered_field,number_ring})) *o O(g)"
    1.26 +    O(f * g) <= (f\<Colon>'a => ('b\<Colon>linordered_field)) *o O(g)"
    1.27  proof -
    1.28    assume a: "\<forall>x. f x ~= 0"
    1.29    show "O(f * g) <= f *o O(g)"
    1.30 @@ -351,21 +351,21 @@
    1.31  qed
    1.32  
    1.33  lemma bigo_mult6:
    1.34 -"\<forall>x. f x \<noteq> 0 \<Longrightarrow> O(f * g) = (f\<Colon>'a \<Rightarrow> ('b\<Colon>{linordered_field,number_ring})) *o O(g)"
    1.35 +"\<forall>x. f x \<noteq> 0 \<Longrightarrow> O(f * g) = (f\<Colon>'a \<Rightarrow> ('b\<Colon>linordered_field)) *o O(g)"
    1.36  by (metis bigo_mult2 bigo_mult5 order_antisym)
    1.37  
    1.38  (*proof requires relaxing relevance: 2007-01-25*)
    1.39  declare bigo_mult6 [simp]
    1.40  
    1.41  lemma bigo_mult7:
    1.42 -"\<forall>x. f x \<noteq> 0 \<Longrightarrow> O(f * g) \<le> O(f\<Colon>'a \<Rightarrow> ('b\<Colon>{linordered_field,number_ring})) \<otimes> O(g)"
    1.43 +"\<forall>x. f x \<noteq> 0 \<Longrightarrow> O(f * g) \<le> O(f\<Colon>'a \<Rightarrow> ('b\<Colon>linordered_field)) \<otimes> O(g)"
    1.44  by (metis bigo_refl bigo_mult6 set_times_mono3)
    1.45  
    1.46  declare bigo_mult6 [simp del]
    1.47  declare bigo_mult7 [intro!]
    1.48  
    1.49  lemma bigo_mult8:
    1.50 -"\<forall>x. f x \<noteq> 0 \<Longrightarrow> O(f * g) = O(f\<Colon>'a \<Rightarrow> ('b\<Colon>{linordered_field,number_ring})) \<otimes> O(g)"
    1.51 +"\<forall>x. f x \<noteq> 0 \<Longrightarrow> O(f * g) = O(f\<Colon>'a \<Rightarrow> ('b\<Colon>linordered_field)) \<otimes> O(g)"
    1.52  by (metis bigo_mult bigo_mult7 order_antisym_conv)
    1.53  
    1.54  lemma bigo_minus [intro]: "f : O(g) \<Longrightarrow> - f : O(g)"
    1.55 @@ -405,14 +405,14 @@
    1.56  lemma bigo_const2 [intro]: "O(\<lambda>x. c) \<le> O(\<lambda>x. 1)"
    1.57  by (metis bigo_const1 bigo_elt_subset)
    1.58  
    1.59 -lemma bigo_const3: "(c\<Colon>'a\<Colon>{linordered_field,number_ring}) ~= 0 \<Longrightarrow> (\<lambda>x. 1) : O(\<lambda>x. c)"
    1.60 +lemma bigo_const3: "(c\<Colon>'a\<Colon>linordered_field) ~= 0 \<Longrightarrow> (\<lambda>x. 1) : O(\<lambda>x. c)"
    1.61  apply (simp add: bigo_def)
    1.62  by (metis abs_eq_0 left_inverse order_refl)
    1.63  
    1.64 -lemma bigo_const4: "(c\<Colon>'a\<Colon>{linordered_field,number_ring}) ~= 0 \<Longrightarrow> O(\<lambda>x. 1) <= O(\<lambda>x. c)"
    1.65 +lemma bigo_const4: "(c\<Colon>'a\<Colon>linordered_field) ~= 0 \<Longrightarrow> O(\<lambda>x. 1) <= O(\<lambda>x. c)"
    1.66  by (metis bigo_elt_subset bigo_const3)
    1.67  
    1.68 -lemma bigo_const [simp]: "(c\<Colon>'a\<Colon>{linordered_field,number_ring}) ~= 0 \<Longrightarrow>
    1.69 +lemma bigo_const [simp]: "(c\<Colon>'a\<Colon>linordered_field) ~= 0 \<Longrightarrow>
    1.70      O(\<lambda>x. c) = O(\<lambda>x. 1)"
    1.71  by (metis bigo_const2 bigo_const4 equalityI)
    1.72  
    1.73 @@ -423,19 +423,19 @@
    1.74  lemma bigo_const_mult2: "O(\<lambda>x. c * f x) \<le> O(f)"
    1.75  by (rule bigo_elt_subset, rule bigo_const_mult1)
    1.76  
    1.77 -lemma bigo_const_mult3: "(c\<Colon>'a\<Colon>{linordered_field,number_ring}) ~= 0 \<Longrightarrow> f : O(\<lambda>x. c * f x)"
    1.78 +lemma bigo_const_mult3: "(c\<Colon>'a\<Colon>linordered_field) ~= 0 \<Longrightarrow> f : O(\<lambda>x. c * f x)"
    1.79  apply (simp add: bigo_def)
    1.80  by (metis (no_types) abs_mult mult_assoc mult_1 order_refl left_inverse)
    1.81  
    1.82  lemma bigo_const_mult4:
    1.83 -"(c\<Colon>'a\<Colon>{linordered_field,number_ring}) \<noteq> 0 \<Longrightarrow> O(f) \<le> O(\<lambda>x. c * f x)"
    1.84 +"(c\<Colon>'a\<Colon>linordered_field) \<noteq> 0 \<Longrightarrow> O(f) \<le> O(\<lambda>x. c * f x)"
    1.85  by (metis bigo_elt_subset bigo_const_mult3)
    1.86  
    1.87 -lemma bigo_const_mult [simp]: "(c\<Colon>'a\<Colon>{linordered_field,number_ring}) ~= 0 \<Longrightarrow>
    1.88 +lemma bigo_const_mult [simp]: "(c\<Colon>'a\<Colon>linordered_field) ~= 0 \<Longrightarrow>
    1.89      O(\<lambda>x. c * f x) = O(f)"
    1.90  by (metis equalityI bigo_const_mult2 bigo_const_mult4)
    1.91  
    1.92 -lemma bigo_const_mult5 [simp]: "(c\<Colon>'a\<Colon>{linordered_field,number_ring}) ~= 0 \<Longrightarrow>
    1.93 +lemma bigo_const_mult5 [simp]: "(c\<Colon>'a\<Colon>linordered_field) ~= 0 \<Longrightarrow>
    1.94      (\<lambda>x. c) *o O(f) = O(f)"
    1.95    apply (auto del: subsetI)
    1.96    apply (rule order_trans)
    1.97 @@ -587,7 +587,7 @@
    1.98    apply assumption+
    1.99  done
   1.100  
   1.101 -lemma bigo_useful_const_mult: "(c\<Colon>'a\<Colon>{linordered_field,number_ring}) ~= 0 \<Longrightarrow>
   1.102 +lemma bigo_useful_const_mult: "(c\<Colon>'a\<Colon>linordered_field) ~= 0 \<Longrightarrow>
   1.103      (\<lambda>x. c) * f =o O(h) \<Longrightarrow> f =o O(h)"
   1.104    apply (rule subsetD)
   1.105    apply (subgoal_tac "(\<lambda>x. 1 / c) *o O(h) <= O(h)")
   1.106 @@ -696,7 +696,7 @@
   1.107  by (metis abs_ge_zero linorder_linear min_max.sup_absorb1 min_max.sup_commute)
   1.108  
   1.109  lemma bigo_lesso4:
   1.110 -  "f <o g =o O(k\<Colon>'a=>'b\<Colon>{linordered_field,number_ring}) \<Longrightarrow>
   1.111 +  "f <o g =o O(k\<Colon>'a=>'b\<Colon>{linordered_field}) \<Longrightarrow>
   1.112     g =o h +o O(k) \<Longrightarrow> f <o h =o O(k)"
   1.113  apply (unfold lesso_def)
   1.114  apply (drule set_plus_imp_minus)