src/HOL/Library/BigO.thy
changeset 47445 69e96e5500df
parent 47108 2a1953f0d20d
child 54230 b1d955791529
     1.1 --- a/src/HOL/Library/BigO.thy	Thu Apr 12 22:55:11 2012 +0200
     1.2 +++ b/src/HOL/Library/BigO.thy	Thu Apr 12 23:07:01 2012 +0200
     1.3 @@ -92,7 +92,7 @@
     1.4    by (auto simp add: bigo_def) 
     1.5  
     1.6  lemma bigo_plus_self_subset [intro]: 
     1.7 -  "O(f) \<oplus> O(f) <= O(f)"
     1.8 +  "O(f) + O(f) <= O(f)"
     1.9    apply (auto simp add: bigo_alt_def set_plus_def)
    1.10    apply (rule_tac x = "c + ca" in exI)
    1.11    apply auto
    1.12 @@ -104,14 +104,14 @@
    1.13    apply force
    1.14  done
    1.15  
    1.16 -lemma bigo_plus_idemp [simp]: "O(f) \<oplus> O(f) = O(f)"
    1.17 +lemma bigo_plus_idemp [simp]: "O(f) + O(f) = O(f)"
    1.18    apply (rule equalityI)
    1.19    apply (rule bigo_plus_self_subset)
    1.20    apply (rule set_zero_plus2) 
    1.21    apply (rule bigo_zero)
    1.22    done
    1.23  
    1.24 -lemma bigo_plus_subset [intro]: "O(f + g) <= O(f) \<oplus> O(g)"
    1.25 +lemma bigo_plus_subset [intro]: "O(f + g) <= O(f) + O(g)"
    1.26    apply (rule subsetI)
    1.27    apply (auto simp add: bigo_def bigo_pos_const func_plus set_plus_def)
    1.28    apply (subst bigo_pos_const [symmetric])+
    1.29 @@ -153,15 +153,15 @@
    1.30    apply simp
    1.31    done
    1.32  
    1.33 -lemma bigo_plus_subset2 [intro]: "A <= O(f) ==> B <= O(f) ==> A \<oplus> B <= O(f)"
    1.34 -  apply (subgoal_tac "A \<oplus> B <= O(f) \<oplus> O(f)")
    1.35 +lemma bigo_plus_subset2 [intro]: "A <= O(f) ==> B <= O(f) ==> A + B <= O(f)"
    1.36 +  apply (subgoal_tac "A + B <= O(f) + O(f)")
    1.37    apply (erule order_trans)
    1.38    apply simp
    1.39    apply (auto del: subsetI simp del: bigo_plus_idemp)
    1.40    done
    1.41  
    1.42  lemma bigo_plus_eq: "ALL x. 0 <= f x ==> ALL x. 0 <= g x ==> 
    1.43 -    O(f + g) = O(f) \<oplus> O(g)"
    1.44 +    O(f + g) = O(f) + O(g)"
    1.45    apply (rule equalityI)
    1.46    apply (rule bigo_plus_subset)
    1.47    apply (simp add: bigo_alt_def set_plus_def func_plus)
    1.48 @@ -273,12 +273,12 @@
    1.49  lemma bigo_abs5: "f =o O(g) ==> (%x. abs(f x)) =o O(g)" 
    1.50    by (unfold bigo_def, auto)
    1.51  
    1.52 -lemma bigo_elt_subset2 [intro]: "f : g +o O(h) ==> O(f) <= O(g) \<oplus> O(h)"
    1.53 +lemma bigo_elt_subset2 [intro]: "f : g +o O(h) ==> O(f) <= O(g) + O(h)"
    1.54  proof -
    1.55    assume "f : g +o O(h)"
    1.56 -  also have "... <= O(g) \<oplus> O(h)"
    1.57 +  also have "... <= O(g) + O(h)"
    1.58      by (auto del: subsetI)
    1.59 -  also have "... = O(%x. abs(g x)) \<oplus> O(%x. abs(h x))"
    1.60 +  also have "... = O(%x. abs(g x)) + O(%x. abs(h x))"
    1.61      apply (subst bigo_abs3 [symmetric])+
    1.62      apply (rule refl)
    1.63      done
    1.64 @@ -287,13 +287,13 @@
    1.65    finally have "f : ...".
    1.66    then have "O(f) <= ..."
    1.67      by (elim bigo_elt_subset)
    1.68 -  also have "... = O(%x. abs(g x)) \<oplus> O(%x. abs(h x))"
    1.69 +  also have "... = O(%x. abs(g x)) + O(%x. abs(h x))"
    1.70      by (rule bigo_plus_eq, auto)
    1.71    finally show ?thesis
    1.72      by (simp add: bigo_abs3 [symmetric])
    1.73  qed
    1.74  
    1.75 -lemma bigo_mult [intro]: "O(f)\<otimes>O(g) <= O(f * g)"
    1.76 +lemma bigo_mult [intro]: "O(f)*O(g) <= O(f * g)"
    1.77    apply (rule subsetI)
    1.78    apply (subst bigo_def)
    1.79    apply (auto simp add: bigo_alt_def set_times_def func_times)
    1.80 @@ -369,7 +369,7 @@
    1.81    done
    1.82  
    1.83  lemma bigo_mult7: "ALL x. f x ~= 0 ==>
    1.84 -    O(f * g) <= O(f::'a => ('b::linordered_field)) \<otimes> O(g)"
    1.85 +    O(f * g) <= O(f::'a => ('b::linordered_field)) * O(g)"
    1.86    apply (subst bigo_mult6)
    1.87    apply assumption
    1.88    apply (rule set_times_mono3)
    1.89 @@ -377,7 +377,7 @@
    1.90    done
    1.91  
    1.92  lemma bigo_mult8: "ALL x. f x ~= 0 ==>
    1.93 -    O(f * g) = O(f::'a => ('b::linordered_field)) \<otimes> O(g)"
    1.94 +    O(f * g) = O(f::'a => ('b::linordered_field)) * O(g)"
    1.95    apply (rule equalityI)
    1.96    apply (erule bigo_mult7)
    1.97    apply (rule bigo_mult)
    1.98 @@ -402,9 +402,9 @@
    1.99    show "f +o O(g) <= O(g)"
   1.100    proof -
   1.101      have "f : O(f)" by auto
   1.102 -    then have "f +o O(g) <= O(f) \<oplus> O(g)"
   1.103 +    then have "f +o O(g) <= O(f) + O(g)"
   1.104        by (auto del: subsetI)
   1.105 -    also have "... <= O(g) \<oplus> O(g)"
   1.106 +    also have "... <= O(g) + O(g)"
   1.107      proof -
   1.108        from a have "O(f) <= O(g)" by (auto del: subsetI)
   1.109        thus ?thesis by (auto del: subsetI)
   1.110 @@ -656,7 +656,7 @@
   1.111  subsection {* Misc useful stuff *}
   1.112  
   1.113  lemma bigo_useful_intro: "A <= O(f) ==> B <= O(f) ==>
   1.114 -  A \<oplus> B <= O(f)"
   1.115 +  A + B <= O(f)"
   1.116    apply (subst bigo_plus_idemp [symmetric])
   1.117    apply (rule set_plus_mono2)
   1.118    apply assumption+