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