src/HOL/Library/BigO.thy
changeset 35028 108662d50512
parent 31337 a9ed5fcc5e39
child 38622 86fc906dcd86
     1.1 --- a/src/HOL/Library/BigO.thy	Fri Feb 05 14:33:31 2010 +0100
     1.2 +++ b/src/HOL/Library/BigO.thy	Fri Feb 05 14:33:50 2010 +0100
     1.3 @@ -38,11 +38,11 @@
     1.4  subsection {* Definitions *}
     1.5  
     1.6  definition
     1.7 -  bigo :: "('a => 'b::ordered_idom) => ('a => 'b) set"  ("(1O'(_'))") where
     1.8 +  bigo :: "('a => 'b::linordered_idom) => ('a => 'b) set"  ("(1O'(_'))") where
     1.9    "O(f::('a => 'b)) =
    1.10        {h. EX c. ALL x. abs (h x) <= c * abs (f x)}"
    1.11  
    1.12 -lemma bigo_pos_const: "(EX (c::'a::ordered_idom). 
    1.13 +lemma bigo_pos_const: "(EX (c::'a::linordered_idom). 
    1.14      ALL x. (abs (h x)) <= (c * (abs (f x))))
    1.15        = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
    1.16    apply auto
    1.17 @@ -352,7 +352,7 @@
    1.18    done
    1.19  
    1.20  lemma bigo_mult5: "ALL x. f x ~= 0 ==>
    1.21 -    O(f * g) <= (f::'a => ('b::ordered_field)) *o O(g)"
    1.22 +    O(f * g) <= (f::'a => ('b::linordered_field)) *o O(g)"
    1.23  proof -
    1.24    assume "ALL x. f x ~= 0"
    1.25    show "O(f * g) <= f *o O(g)"
    1.26 @@ -381,14 +381,14 @@
    1.27  qed
    1.28  
    1.29  lemma bigo_mult6: "ALL x. f x ~= 0 ==>
    1.30 -    O(f * g) = (f::'a => ('b::ordered_field)) *o O(g)"
    1.31 +    O(f * g) = (f::'a => ('b::linordered_field)) *o O(g)"
    1.32    apply (rule equalityI)
    1.33    apply (erule bigo_mult5)
    1.34    apply (rule bigo_mult2)
    1.35    done
    1.36  
    1.37  lemma bigo_mult7: "ALL x. f x ~= 0 ==>
    1.38 -    O(f * g) <= O(f::'a => ('b::ordered_field)) \<otimes> O(g)"
    1.39 +    O(f * g) <= O(f::'a => ('b::linordered_field)) \<otimes> O(g)"
    1.40    apply (subst bigo_mult6)
    1.41    apply assumption
    1.42    apply (rule set_times_mono3)
    1.43 @@ -396,7 +396,7 @@
    1.44    done
    1.45  
    1.46  lemma bigo_mult8: "ALL x. f x ~= 0 ==>
    1.47 -    O(f * g) = O(f::'a => ('b::ordered_field)) \<otimes> O(g)"
    1.48 +    O(f * g) = O(f::'a => ('b::linordered_field)) \<otimes> O(g)"
    1.49    apply (rule equalityI)
    1.50    apply (erule bigo_mult7)
    1.51    apply (rule bigo_mult)
    1.52 @@ -481,16 +481,16 @@
    1.53    apply (rule bigo_const1)
    1.54    done
    1.55  
    1.56 -lemma bigo_const3: "(c::'a::ordered_field) ~= 0 ==> (%x. 1) : O(%x. c)"
    1.57 +lemma bigo_const3: "(c::'a::linordered_field) ~= 0 ==> (%x. 1) : O(%x. c)"
    1.58    apply (simp add: bigo_def)
    1.59    apply (rule_tac x = "abs(inverse c)" in exI)
    1.60    apply (simp add: abs_mult [symmetric])
    1.61    done
    1.62  
    1.63 -lemma bigo_const4: "(c::'a::ordered_field) ~= 0 ==> O(%x. 1) <= O(%x. c)"
    1.64 +lemma bigo_const4: "(c::'a::linordered_field) ~= 0 ==> O(%x. 1) <= O(%x. c)"
    1.65    by (rule bigo_elt_subset, rule bigo_const3, assumption)
    1.66  
    1.67 -lemma bigo_const [simp]: "(c::'a::ordered_field) ~= 0 ==> 
    1.68 +lemma bigo_const [simp]: "(c::'a::linordered_field) ~= 0 ==> 
    1.69      O(%x. c) = O(%x. 1)"
    1.70    by (rule equalityI, rule bigo_const2, rule bigo_const4, assumption)
    1.71  
    1.72 @@ -503,21 +503,21 @@
    1.73  lemma bigo_const_mult2: "O(%x. c * f x) <= O(f)"
    1.74    by (rule bigo_elt_subset, rule bigo_const_mult1)
    1.75  
    1.76 -lemma bigo_const_mult3: "(c::'a::ordered_field) ~= 0 ==> f : O(%x. c * f x)"
    1.77 +lemma bigo_const_mult3: "(c::'a::linordered_field) ~= 0 ==> f : O(%x. c * f x)"
    1.78    apply (simp add: bigo_def)
    1.79    apply (rule_tac x = "abs(inverse c)" in exI)
    1.80    apply (simp add: abs_mult [symmetric] mult_assoc [symmetric])
    1.81    done
    1.82  
    1.83 -lemma bigo_const_mult4: "(c::'a::ordered_field) ~= 0 ==> 
    1.84 +lemma bigo_const_mult4: "(c::'a::linordered_field) ~= 0 ==> 
    1.85      O(f) <= O(%x. c * f x)"
    1.86    by (rule bigo_elt_subset, rule bigo_const_mult3, assumption)
    1.87  
    1.88 -lemma bigo_const_mult [simp]: "(c::'a::ordered_field) ~= 0 ==> 
    1.89 +lemma bigo_const_mult [simp]: "(c::'a::linordered_field) ~= 0 ==> 
    1.90      O(%x. c * f x) = O(f)"
    1.91    by (rule equalityI, rule bigo_const_mult2, erule bigo_const_mult4)
    1.92  
    1.93 -lemma bigo_const_mult5 [simp]: "(c::'a::ordered_field) ~= 0 ==> 
    1.94 +lemma bigo_const_mult5 [simp]: "(c::'a::linordered_field) ~= 0 ==> 
    1.95      (%x. c) *o O(f) = O(f)"
    1.96    apply (auto del: subsetI)
    1.97    apply (rule order_trans)
    1.98 @@ -688,7 +688,7 @@
    1.99    apply assumption+
   1.100    done
   1.101    
   1.102 -lemma bigo_useful_const_mult: "(c::'a::ordered_field) ~= 0 ==> 
   1.103 +lemma bigo_useful_const_mult: "(c::'a::linordered_field) ~= 0 ==> 
   1.104      (%x. c) * f =o O(h) ==> f =o O(h)"
   1.105    apply (rule subsetD)
   1.106    apply (subgoal_tac "(%x. 1 / c) *o O(h) <= O(h)")
   1.107 @@ -733,7 +733,7 @@
   1.108  subsection {* Less than or equal to *}
   1.109  
   1.110  definition
   1.111 -  lesso :: "('a => 'b::ordered_idom) => ('a => 'b) => ('a => 'b)"
   1.112 +  lesso :: "('a => 'b::linordered_idom) => ('a => 'b) => ('a => 'b)"
   1.113      (infixl "<o" 70) where
   1.114    "f <o g = (%x. max (f x - g x) 0)"
   1.115  
   1.116 @@ -833,7 +833,7 @@
   1.117    apply (simp add: algebra_simps)
   1.118    done
   1.119  
   1.120 -lemma bigo_lesso4: "f <o g =o O(k::'a=>'b::ordered_field) ==>
   1.121 +lemma bigo_lesso4: "f <o g =o O(k::'a=>'b::linordered_field) ==>
   1.122      g =o h +o O(k) ==> f <o h =o O(k)"
   1.123    apply (unfold lesso_def)
   1.124    apply (drule set_plus_imp_minus)