author  haftmann 
Sat, 05 Jul 2014 11:01:53 +0200  
changeset 57514  bdc2c6b40bf2 
parent 57512  cc97b347b301 
child 58622  aa99568f56de 
permissions  rwrr 
16932  1 
(* Title: HOL/Library/BigO.thy 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

2 
Authors: Jeremy Avigad and Kevin Donnelly 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

3 
*) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

4 

d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

5 
header {* Big O notation *} 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

6 

d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

7 
theory BigO 
38622  8 
imports Complex_Main Function_Algebras Set_Algebras 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

9 
begin 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

10 

d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

11 
text {* 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

12 
This library is designed to support asymptotic ``big O'' calculations, 
17199
59c1bfc81d91
moved lemmas that require the HOLComplex logic image to Complex/ex/BigO_Complex.thy;
wenzelm
parents:
16961
diff
changeset

13 
i.e.~reasoning with expressions of the form $f = O(g)$ and $f = g + 
59c1bfc81d91
moved lemmas that require the HOLComplex logic image to Complex/ex/BigO_Complex.thy;
wenzelm
parents:
16961
diff
changeset

14 
O(h)$. An earlier version of this library is described in detail in 
59c1bfc81d91
moved lemmas that require the HOLComplex logic image to Complex/ex/BigO_Complex.thy;
wenzelm
parents:
16961
diff
changeset

15 
\cite{AvigadDonnelly}. 
59c1bfc81d91
moved lemmas that require the HOLComplex logic image to Complex/ex/BigO_Complex.thy;
wenzelm
parents:
16961
diff
changeset

16 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

17 
The main changes in this version are as follows: 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

18 
\begin{itemize} 
17199
59c1bfc81d91
moved lemmas that require the HOLComplex logic image to Complex/ex/BigO_Complex.thy;
wenzelm
parents:
16961
diff
changeset

19 
\item We have eliminated the @{text O} operator on sets. (Most uses of this seem 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

20 
to be inessential.) 
17199
59c1bfc81d91
moved lemmas that require the HOLComplex logic image to Complex/ex/BigO_Complex.thy;
wenzelm
parents:
16961
diff
changeset

21 
\item We no longer use @{text "+"} as output syntax for @{text "+o"} 
55821  22 
\item Lemmas involving @{text "sumr"} have been replaced by more general lemmas 
17199
59c1bfc81d91
moved lemmas that require the HOLComplex logic image to Complex/ex/BigO_Complex.thy;
wenzelm
parents:
16961
diff
changeset

23 
involving `@{text "setsum"}. 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

24 
\item The library has been expanded, with e.g.~support for expressions of 
17199
59c1bfc81d91
moved lemmas that require the HOLComplex logic image to Complex/ex/BigO_Complex.thy;
wenzelm
parents:
16961
diff
changeset

25 
the form @{text "f < g + O(h)"}. 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

26 
\end{itemize} 
17199
59c1bfc81d91
moved lemmas that require the HOLComplex logic image to Complex/ex/BigO_Complex.thy;
wenzelm
parents:
16961
diff
changeset

27 

59c1bfc81d91
moved lemmas that require the HOLComplex logic image to Complex/ex/BigO_Complex.thy;
wenzelm
parents:
16961
diff
changeset

28 
Note also since the Big O library includes rules that demonstrate set 
59c1bfc81d91
moved lemmas that require the HOLComplex logic image to Complex/ex/BigO_Complex.thy;
wenzelm
parents:
16961
diff
changeset

29 
inclusion, to use the automated reasoners effectively with the library 
59c1bfc81d91
moved lemmas that require the HOLComplex logic image to Complex/ex/BigO_Complex.thy;
wenzelm
parents:
16961
diff
changeset

30 
one should redeclare the theorem @{text "subsetI"} as an intro rule, 
59c1bfc81d91
moved lemmas that require the HOLComplex logic image to Complex/ex/BigO_Complex.thy;
wenzelm
parents:
16961
diff
changeset

31 
rather than as an @{text "intro!"} rule, for example, using 
59c1bfc81d91
moved lemmas that require the HOLComplex logic image to Complex/ex/BigO_Complex.thy;
wenzelm
parents:
16961
diff
changeset

32 
\isa{\isakeyword{declare}}~@{text "subsetI [del, intro]"}. 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

33 
*} 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

34 

d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

35 
subsection {* Definitions *} 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

36 

55821  37 
definition bigo :: "('a \<Rightarrow> 'b::linordered_idom) \<Rightarrow> ('a \<Rightarrow> 'b) set" ("(1O'(_'))") 
38 
where "O(f:: 'a \<Rightarrow> 'b) = {h. \<exists>c. \<forall>x. abs (h x) \<le> c * abs (f x)}" 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

39 

55821  40 
lemma bigo_pos_const: 
41 
"(\<exists>c::'a::linordered_idom. \<forall>x. abs (h x) \<le> c * abs (f x)) \<longleftrightarrow> 

42 
(\<exists>c. 0 < c \<and> (\<forall>x. abs (h x) \<le> c * abs (f x)))" 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

43 
apply auto 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

44 
apply (case_tac "c = 0") 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

45 
apply simp 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

46 
apply (rule_tac x = "1" in exI) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

47 
apply simp 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

48 
apply (rule_tac x = "abs c" in exI) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

49 
apply auto 
55821  50 
apply (subgoal_tac "c * abs (f x) \<le> abs c * abs (f x)") 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

51 
apply (erule_tac x = x in allE) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

52 
apply force 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

53 
apply (rule mult_right_mono) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

54 
apply (rule abs_ge_self) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

55 
apply (rule abs_ge_zero) 
22665  56 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

57 

55821  58 
lemma bigo_alt_def: "O(f) = {h. \<exists>c. 0 < c \<and> (\<forall>x. abs (h x) \<le> c * abs (f x))}" 
22665  59 
by (auto simp add: bigo_def bigo_pos_const) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

60 

55821  61 
lemma bigo_elt_subset [intro]: "f \<in> O(g) \<Longrightarrow> O(f) \<le> O(g)" 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

62 
apply (auto simp add: bigo_alt_def) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

63 
apply (rule_tac x = "ca * c" in exI) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

64 
apply (rule conjI) 
56544  65 
apply simp 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

66 
apply (rule allI) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

67 
apply (drule_tac x = "xa" in spec)+ 
55821  68 
apply (subgoal_tac "ca * abs (f xa) \<le> ca * (c * abs (g xa))") 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

69 
apply (erule order_trans) 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

70 
apply (simp add: ac_simps) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

71 
apply (rule mult_left_mono, assumption) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

72 
apply (rule order_less_imp_le, assumption) 
22665  73 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

74 

55821  75 
lemma bigo_refl [intro]: "f \<in> O(f)" 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

76 
apply(auto simp add: bigo_def) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

77 
apply(rule_tac x = 1 in exI) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

78 
apply simp 
22665  79 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

80 

55821  81 
lemma bigo_zero: "0 \<in> O(g)" 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

82 
apply (auto simp add: bigo_def func_zero) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

83 
apply (rule_tac x = 0 in exI) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

84 
apply auto 
22665  85 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

86 

55821  87 
lemma bigo_zero2: "O(\<lambda>x. 0) = {\<lambda>x. 0}" 
88 
by (auto simp add: bigo_def) 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

89 

55821  90 
lemma bigo_plus_self_subset [intro]: "O(f) + O(f) \<subseteq> O(f)" 
26814
b3e8d5ec721d
Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with
berghofe
parents:
25592
diff
changeset

91 
apply (auto simp add: bigo_alt_def set_plus_def) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

92 
apply (rule_tac x = "c + ca" in exI) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

93 
apply auto 
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

94 
apply (simp add: ring_distribs func_plus) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

95 
apply (rule order_trans) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

96 
apply (rule abs_triangle_ineq) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

97 
apply (rule add_mono) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

98 
apply force 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

99 
apply force 
55821  100 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

101 

47445
69e96e5500df
Set_Algebras: removed syntax \<oplus> and \<otimes>, in favour of plain + and *
krauss
parents:
47108
diff
changeset

102 
lemma bigo_plus_idemp [simp]: "O(f) + O(f) = O(f)" 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

103 
apply (rule equalityI) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

104 
apply (rule bigo_plus_self_subset) 
55821  105 
apply (rule set_zero_plus2) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

106 
apply (rule bigo_zero) 
22665  107 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

108 

55821  109 
lemma bigo_plus_subset [intro]: "O(f + g) \<subseteq> O(f) + O(g)" 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

110 
apply (rule subsetI) 
26814
b3e8d5ec721d
Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with
berghofe
parents:
25592
diff
changeset

111 
apply (auto simp add: bigo_def bigo_pos_const func_plus set_plus_def) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

112 
apply (subst bigo_pos_const [symmetric])+ 
55821  113 
apply (rule_tac x = "\<lambda>n. if abs (g n) \<le> (abs (f n)) then x n else 0" in exI) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

114 
apply (rule conjI) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

115 
apply (rule_tac x = "c + c" in exI) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

116 
apply (clarsimp) 
55821  117 
apply (subgoal_tac "c * abs (f xa + g xa) \<le> (c + c) * abs (f xa)") 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

118 
apply (erule_tac x = xa in allE) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

119 
apply (erule order_trans) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

120 
apply (simp) 
55821  121 
apply (subgoal_tac "c * abs (f xa + g xa) \<le> c * (abs (f xa) + abs (g xa))") 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

122 
apply (erule order_trans) 
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

123 
apply (simp add: ring_distribs) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

124 
apply (rule mult_left_mono) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

125 
apply (simp add: abs_triangle_ineq) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

126 
apply (simp add: order_less_le) 
55821  127 
apply (rule_tac x = "\<lambda>n. if (abs (f n)) < abs (g n) then x n else 0" in exI) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

128 
apply (rule conjI) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

129 
apply (rule_tac x = "c + c" in exI) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

130 
apply auto 
55821  131 
apply (subgoal_tac "c * abs (f xa + g xa) \<le> (c + c) * abs (g xa)") 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

132 
apply (erule_tac x = xa in allE) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

133 
apply (erule order_trans) 
55821  134 
apply simp 
135 
apply (subgoal_tac "c * abs (f xa + g xa) \<le> c * (abs (f xa) + abs (g xa))") 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

136 
apply (erule order_trans) 
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

137 
apply (simp add: ring_distribs) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

138 
apply (rule mult_left_mono) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

139 
apply (rule abs_triangle_ineq) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

140 
apply (simp add: order_less_le) 
22665  141 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

142 

55821  143 
lemma bigo_plus_subset2 [intro]: "A \<subseteq> O(f) \<Longrightarrow> B \<subseteq> O(f) \<Longrightarrow> A + B \<subseteq> O(f)" 
144 
apply (subgoal_tac "A + B \<subseteq> O(f) + O(f)") 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

145 
apply (erule order_trans) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

146 
apply simp 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

147 
apply (auto del: subsetI simp del: bigo_plus_idemp) 
22665  148 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

149 

55821  150 
lemma bigo_plus_eq: "\<forall>x. 0 \<le> f x \<Longrightarrow> \<forall>x. 0 \<le> g x \<Longrightarrow> O(f + g) = O(f) + O(g)" 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

151 
apply (rule equalityI) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

152 
apply (rule bigo_plus_subset) 
26814
b3e8d5ec721d
Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with
berghofe
parents:
25592
diff
changeset

153 
apply (simp add: bigo_alt_def set_plus_def func_plus) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

154 
apply clarify 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

155 
apply (rule_tac x = "max c ca" in exI) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

156 
apply (rule conjI) 
55821  157 
apply (subgoal_tac "c \<le> max c ca") 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

158 
apply (erule order_less_le_trans) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

159 
apply assumption 
54863
82acc20ded73
prefer more canonical names for lemmas on min/max
haftmann
parents:
54230
diff
changeset

160 
apply (rule max.cobounded1) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

161 
apply clarify 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

162 
apply (drule_tac x = "xa" in spec)+ 
55821  163 
apply (subgoal_tac "0 \<le> f xa + g xa") 
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset

164 
apply (simp add: ring_distribs) 
55821  165 
apply (subgoal_tac "abs (a xa + b xa) \<le> abs (a xa) + abs (b xa)") 
166 
apply (subgoal_tac "abs (a xa) + abs (b xa) \<le> max c ca * f xa + max c ca * g xa") 

167 
apply force 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

168 
apply (rule add_mono) 
55821  169 
apply (subgoal_tac "c * f xa \<le> max c ca * f xa") 
170 
apply force 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

171 
apply (rule mult_right_mono) 
54863
82acc20ded73
prefer more canonical names for lemmas on min/max
haftmann
parents:
54230
diff
changeset

172 
apply (rule max.cobounded1) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

173 
apply assumption 
55821  174 
apply (subgoal_tac "ca * g xa \<le> max c ca * g xa") 
175 
apply force 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

176 
apply (rule mult_right_mono) 
54863
82acc20ded73
prefer more canonical names for lemmas on min/max
haftmann
parents:
54230
diff
changeset

177 
apply (rule max.cobounded2) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

178 
apply assumption 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

179 
apply (rule abs_triangle_ineq) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

180 
apply (rule add_nonneg_nonneg) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

181 
apply assumption+ 
22665  182 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

183 

55821  184 
lemma bigo_bounded_alt: "\<forall>x. 0 \<le> f x \<Longrightarrow> \<forall>x. f x \<le> c * g x \<Longrightarrow> f \<in> O(g)" 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

185 
apply (auto simp add: bigo_def) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

186 
apply (rule_tac x = "abs c" in exI) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

187 
apply auto 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

188 
apply (drule_tac x = x in spec)+ 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

189 
apply (simp add: abs_mult [symmetric]) 
22665  190 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

191 

55821  192 
lemma bigo_bounded: "\<forall>x. 0 \<le> f x \<Longrightarrow> \<forall>x. f x \<le> g x \<Longrightarrow> f \<in> O(g)" 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

193 
apply (erule bigo_bounded_alt [of f 1 g]) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

194 
apply simp 
22665  195 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

196 

55821  197 
lemma bigo_bounded2: "\<forall>x. lb x \<le> f x \<Longrightarrow> \<forall>x. f x \<le> lb x + g x \<Longrightarrow> f \<in> lb +o O(g)" 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

198 
apply (rule set_minus_imp_plus) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

199 
apply (rule bigo_bounded) 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
47445
diff
changeset

200 
apply (auto simp add: fun_Compl_def func_plus) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

201 
apply (drule_tac x = x in spec)+ 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

202 
apply force 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

203 
apply (drule_tac x = x in spec)+ 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

204 
apply force 
22665  205 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

206 

55821  207 
lemma bigo_abs: "(\<lambda>x. abs (f x)) =o O(f)" 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

208 
apply (unfold bigo_def) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

209 
apply auto 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

210 
apply (rule_tac x = 1 in exI) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

211 
apply auto 
22665  212 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

213 

55821  214 
lemma bigo_abs2: "f =o O(\<lambda>x. abs (f x))" 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

215 
apply (unfold bigo_def) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

216 
apply auto 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

217 
apply (rule_tac x = 1 in exI) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

218 
apply auto 
22665  219 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

220 

55821  221 
lemma bigo_abs3: "O(f) = O(\<lambda>x. abs (f x))" 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

222 
apply (rule equalityI) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

223 
apply (rule bigo_elt_subset) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

224 
apply (rule bigo_abs2) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

225 
apply (rule bigo_elt_subset) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

226 
apply (rule bigo_abs) 
22665  227 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

228 

55821  229 
lemma bigo_abs4: "f =o g +o O(h) \<Longrightarrow> (\<lambda>x. abs (f x)) =o (\<lambda>x. abs (g x)) +o O(h)" 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

230 
apply (drule set_plus_imp_minus) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

231 
apply (rule set_minus_imp_plus) 
26814
b3e8d5ec721d
Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with
berghofe
parents:
25592
diff
changeset

232 
apply (subst fun_diff_def) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

233 
proof  
55821  234 
assume a: "f  g \<in> O(h)" 
235 
have "(\<lambda>x. abs (f x)  abs (g x)) =o O(\<lambda>x. abs (abs (f x)  abs (g x)))" 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

236 
by (rule bigo_abs2) 
55821  237 
also have "\<dots> \<subseteq> O(\<lambda>x. abs (f x  g x))" 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

238 
apply (rule bigo_elt_subset) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

239 
apply (rule bigo_bounded) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

240 
apply force 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

241 
apply (rule allI) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

242 
apply (rule abs_triangle_ineq3) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

243 
done 
55821  244 
also have "\<dots> \<subseteq> O(f  g)" 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

245 
apply (rule bigo_elt_subset) 
26814
b3e8d5ec721d
Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with
berghofe
parents:
25592
diff
changeset

246 
apply (subst fun_diff_def) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

247 
apply (rule bigo_abs) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

248 
done 
55821  249 
also from a have "\<dots> \<subseteq> O(h)" 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

250 
by (rule bigo_elt_subset) 
55821  251 
finally show "(\<lambda>x. abs (f x)  abs (g x)) \<in> O(h)". 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

252 
qed 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

253 

55821  254 
lemma bigo_abs5: "f =o O(g) \<Longrightarrow> (\<lambda>x. abs (f x)) =o O(g)" 
22665  255 
by (unfold bigo_def, auto) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

256 

55821  257 
lemma bigo_elt_subset2 [intro]: "f \<in> g +o O(h) \<Longrightarrow> O(f) \<subseteq> O(g) + O(h)" 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

258 
proof  
55821  259 
assume "f \<in> g +o O(h)" 
260 
also have "\<dots> \<subseteq> O(g) + O(h)" 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

261 
by (auto del: subsetI) 
55821  262 
also have "\<dots> = O(\<lambda>x. abs (g x)) + O(\<lambda>x. abs (h x))" 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

263 
apply (subst bigo_abs3 [symmetric])+ 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

264 
apply (rule refl) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

265 
done 
55821  266 
also have "\<dots> = O((\<lambda>x. abs (g x)) + (\<lambda>x. abs (h x)))" 
267 
by (rule bigo_plus_eq [symmetric]) auto 

268 
finally have "f \<in> \<dots>" . 

269 
then have "O(f) \<subseteq> \<dots>" 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

270 
by (elim bigo_elt_subset) 
55821  271 
also have "\<dots> = O(\<lambda>x. abs (g x)) + O(\<lambda>x. abs (h x))" 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

272 
by (rule bigo_plus_eq, auto) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

273 
finally show ?thesis 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

274 
by (simp add: bigo_abs3 [symmetric]) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

275 
qed 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

276 

55821  277 
lemma bigo_mult [intro]: "O(f)*O(g) \<subseteq> O(f * g)" 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

278 
apply (rule subsetI) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

279 
apply (subst bigo_def) 
26814
b3e8d5ec721d
Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with
berghofe
parents:
25592
diff
changeset

280 
apply (auto simp add: bigo_alt_def set_times_def func_times) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

281 
apply (rule_tac x = "c * ca" in exI) 
55821  282 
apply (rule allI) 
283 
apply (erule_tac x = x in allE)+ 

284 
apply (subgoal_tac "c * ca * abs (f x * g x) = (c * abs (f x)) * (ca * abs (g x))") 

285 
apply (erule ssubst) 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

286 
apply (subst abs_mult) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

287 
apply (rule mult_mono) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

288 
apply assumption+ 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

289 
apply auto 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

290 
apply (simp add: ac_simps abs_mult) 
22665  291 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

292 

55821  293 
lemma bigo_mult2 [intro]: "f *o O(g) \<subseteq> O(f * g)" 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

294 
apply (auto simp add: bigo_def elt_set_times_def func_times abs_mult) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

295 
apply (rule_tac x = c in exI) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

296 
apply auto 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

297 
apply (drule_tac x = x in spec) 
55821  298 
apply (subgoal_tac "abs (f x) * abs (b x) \<le> abs (f x) * (c * abs (g x))") 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

299 
apply (force simp add: ac_simps) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

300 
apply (rule mult_left_mono, assumption) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

301 
apply (rule abs_ge_zero) 
22665  302 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

303 

55821  304 
lemma bigo_mult3: "f \<in> O(h) \<Longrightarrow> g \<in> O(j) \<Longrightarrow> f * g \<in> O(h * j)" 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

305 
apply (rule subsetD) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

306 
apply (rule bigo_mult) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

307 
apply (erule set_times_intro, assumption) 
22665  308 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

309 

55821  310 
lemma bigo_mult4 [intro]: "f \<in> k +o O(h) \<Longrightarrow> g * f \<in> (g * k) +o O(g * h)" 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

311 
apply (drule set_plus_imp_minus) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

312 
apply (rule set_minus_imp_plus) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

313 
apply (drule bigo_mult3 [where g = g and j = g]) 
29667  314 
apply (auto simp add: algebra_simps) 
22665  315 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

316 

41528  317 
lemma bigo_mult5: 
55821  318 
fixes f :: "'a \<Rightarrow> 'b::linordered_field" 
319 
assumes "\<forall>x. f x \<noteq> 0" 

320 
shows "O(f * g) \<subseteq> f *o O(g)" 

41528  321 
proof 
322 
fix h 

55821  323 
assume "h \<in> O(f * g)" 
324 
then have "(\<lambda>x. 1 / (f x)) * h \<in> (\<lambda>x. 1 / f x) *o O(f * g)" 

41528  325 
by auto 
55821  326 
also have "\<dots> \<subseteq> O((\<lambda>x. 1 / f x) * (f * g))" 
41528  327 
by (rule bigo_mult2) 
55821  328 
also have "(\<lambda>x. 1 / f x) * (f * g) = g" 
329 
apply (simp add: func_times) 

41528  330 
apply (rule ext) 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

331 
apply (simp add: assms nonzero_divide_eq_eq ac_simps) 
41528  332 
done 
55821  333 
finally have "(\<lambda>x. (1::'b) / f x) * h \<in> O(g)" . 
334 
then have "f * ((\<lambda>x. (1::'b) / f x) * h) \<in> f *o O(g)" 

41528  335 
by auto 
55821  336 
also have "f * ((\<lambda>x. (1::'b) / f x) * h) = h" 
337 
apply (simp add: func_times) 

41528  338 
apply (rule ext) 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

339 
apply (simp add: assms nonzero_divide_eq_eq ac_simps) 
41528  340 
done 
55821  341 
finally show "h \<in> f *o O(g)" . 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

342 
qed 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

343 

55821  344 
lemma bigo_mult6: 
345 
fixes f :: "'a \<Rightarrow> 'b::linordered_field" 

346 
shows "\<forall>x. f x \<noteq> 0 \<Longrightarrow> O(f * g) = f *o O(g)" 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

347 
apply (rule equalityI) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

348 
apply (erule bigo_mult5) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

349 
apply (rule bigo_mult2) 
22665  350 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

351 

55821  352 
lemma bigo_mult7: 
353 
fixes f :: "'a \<Rightarrow> 'b::linordered_field" 

354 
shows "\<forall>x. f x \<noteq> 0 \<Longrightarrow> O(f * g) \<subseteq> O(f) * O(g)" 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

355 
apply (subst bigo_mult6) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

356 
apply assumption 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

357 
apply (rule set_times_mono3) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

358 
apply (rule bigo_refl) 
22665  359 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

360 

55821  361 
lemma bigo_mult8: 
362 
fixes f :: "'a \<Rightarrow> 'b::linordered_field" 

363 
shows "\<forall>x. f x \<noteq> 0 \<Longrightarrow> O(f * g) = O(f) * O(g)" 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

364 
apply (rule equalityI) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

365 
apply (erule bigo_mult7) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

366 
apply (rule bigo_mult) 
22665  367 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

368 

55821  369 
lemma bigo_minus [intro]: "f \<in> O(g) \<Longrightarrow>  f \<in> O(g)" 
26814
b3e8d5ec721d
Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with
berghofe
parents:
25592
diff
changeset

370 
by (auto simp add: bigo_def fun_Compl_def) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

371 

55821  372 
lemma bigo_minus2: "f \<in> g +o O(h) \<Longrightarrow>  f \<in> g +o O(h)" 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

373 
apply (rule set_minus_imp_plus) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

374 
apply (drule set_plus_imp_minus) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

375 
apply (drule bigo_minus) 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
47445
diff
changeset

376 
apply simp 
22665  377 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

378 

55821  379 
lemma bigo_minus3: "O( f) = O(f)" 
41528  380 
by (auto simp add: bigo_def fun_Compl_def) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

381 

55821  382 
lemma bigo_plus_absorb_lemma1: "f \<in> O(g) \<Longrightarrow> f +o O(g) \<subseteq> O(g)" 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

383 
proof  
55821  384 
assume a: "f \<in> O(g)" 
385 
show "f +o O(g) \<subseteq> O(g)" 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

386 
proof  
55821  387 
have "f \<in> O(f)" by auto 
388 
then have "f +o O(g) \<subseteq> O(f) + O(g)" 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

389 
by (auto del: subsetI) 
55821  390 
also have "\<dots> \<subseteq> O(g) + O(g)" 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

391 
proof  
55821  392 
from a have "O(f) \<subseteq> O(g)" by (auto del: subsetI) 
56796  393 
then show ?thesis by (auto del: subsetI) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

394 
qed 
55821  395 
also have "\<dots> \<subseteq> O(g)" by simp 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

396 
finally show ?thesis . 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

397 
qed 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

398 
qed 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

399 

55821  400 
lemma bigo_plus_absorb_lemma2: "f \<in> O(g) \<Longrightarrow> O(g) \<subseteq> f +o O(g)" 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

401 
proof  
55821  402 
assume a: "f \<in> O(g)" 
403 
show "O(g) \<subseteq> f +o O(g)" 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

404 
proof  
55821  405 
from a have " f \<in> O(g)" 
406 
by auto 

407 
then have " f +o O(g) \<subseteq> O(g)" 

408 
by (elim bigo_plus_absorb_lemma1) 

409 
then have "f +o ( f +o O(g)) \<subseteq> f +o O(g)" 

410 
by auto 

411 
also have "f +o ( f +o O(g)) = O(g)" 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

412 
by (simp add: set_plus_rearranges) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

413 
finally show ?thesis . 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

414 
qed 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

415 
qed 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

416 

55821  417 
lemma bigo_plus_absorb [simp]: "f \<in> O(g) \<Longrightarrow> f +o O(g) = O(g)" 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

418 
apply (rule equalityI) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

419 
apply (erule bigo_plus_absorb_lemma1) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

420 
apply (erule bigo_plus_absorb_lemma2) 
22665  421 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

422 

55821  423 
lemma bigo_plus_absorb2 [intro]: "f \<in> O(g) \<Longrightarrow> A \<subseteq> O(g) \<Longrightarrow> f +o A \<subseteq> O(g)" 
424 
apply (subgoal_tac "f +o A \<subseteq> f +o O(g)") 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

425 
apply force+ 
22665  426 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

427 

55821  428 
lemma bigo_add_commute_imp: "f \<in> g +o O(h) \<Longrightarrow> g \<in> f +o O(h)" 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

429 
apply (subst set_minus_plus [symmetric]) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

430 
apply (subgoal_tac "g  f =  (f  g)") 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

431 
apply (erule ssubst) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

432 
apply (rule bigo_minus) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

433 
apply (subst set_minus_plus) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

434 
apply assumption 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

435 
apply (simp add: ac_simps) 
22665  436 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

437 

55821  438 
lemma bigo_add_commute: "f \<in> g +o O(h) \<longleftrightarrow> g \<in> f +o O(h)" 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

439 
apply (rule iffI) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

440 
apply (erule bigo_add_commute_imp)+ 
22665  441 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

442 

55821  443 
lemma bigo_const1: "(\<lambda>x. c) \<in> O(\<lambda>x. 1)" 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

444 
by (auto simp add: bigo_def ac_simps) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

445 

55821  446 
lemma bigo_const2 [intro]: "O(\<lambda>x. c) \<subseteq> O(\<lambda>x. 1)" 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

447 
apply (rule bigo_elt_subset) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

448 
apply (rule bigo_const1) 
22665  449 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

450 

55821  451 
lemma bigo_const3: 
452 
fixes c :: "'a::linordered_field" 

453 
shows "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. 1) \<in> O(\<lambda>x. c)" 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

454 
apply (simp add: bigo_def) 
55821  455 
apply (rule_tac x = "abs (inverse c)" in exI) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

456 
apply (simp add: abs_mult [symmetric]) 
22665  457 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

458 

55821  459 
lemma bigo_const4: 
460 
fixes c :: "'a::linordered_field" 

461 
shows "c \<noteq> 0 \<Longrightarrow> O(\<lambda>x. 1) \<subseteq> O(\<lambda>x. c)" 

462 
apply (rule bigo_elt_subset) 

463 
apply (rule bigo_const3) 

464 
apply assumption 

465 
done 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

466 

55821  467 
lemma bigo_const [simp]: 
468 
fixes c :: "'a::linordered_field" 

469 
shows "c \<noteq> 0 \<Longrightarrow> O(\<lambda>x. c) = O(\<lambda>x. 1)" 

470 
apply (rule equalityI) 

471 
apply (rule bigo_const2) 

472 
apply (rule bigo_const4) 

473 
apply assumption 

474 
done 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

475 

55821  476 
lemma bigo_const_mult1: "(\<lambda>x. c * f x) \<in> O(f)" 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

477 
apply (simp add: bigo_def) 
55821  478 
apply (rule_tac x = "abs c" in exI) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

479 
apply (auto simp add: abs_mult [symmetric]) 
22665  480 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

481 

55821  482 
lemma bigo_const_mult2: "O(\<lambda>x. c * f x) \<subseteq> O(f)" 
483 
apply (rule bigo_elt_subset) 

484 
apply (rule bigo_const_mult1) 

485 
done 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

486 

55821  487 
lemma bigo_const_mult3: 
488 
fixes c :: "'a::linordered_field" 

489 
shows "c \<noteq> 0 \<Longrightarrow> f \<in> O(\<lambda>x. c * f x)" 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

490 
apply (simp add: bigo_def) 
55821  491 
apply (rule_tac x = "abs (inverse c)" in exI) 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

492 
apply (simp add: abs_mult [symmetric] mult.assoc [symmetric]) 
22665  493 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

494 

55821  495 
lemma bigo_const_mult4: 
496 
fixes c :: "'a::linordered_field" 

497 
shows "c \<noteq> 0 \<Longrightarrow> O(f) \<subseteq> O(\<lambda>x. c * f x)" 

498 
apply (rule bigo_elt_subset) 

499 
apply (rule bigo_const_mult3) 

500 
apply assumption 

501 
done 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

502 

55821  503 
lemma bigo_const_mult [simp]: 
504 
fixes c :: "'a::linordered_field" 

505 
shows "c \<noteq> 0 \<Longrightarrow> O(\<lambda>x. c * f x) = O(f)" 

506 
apply (rule equalityI) 

507 
apply (rule bigo_const_mult2) 

508 
apply (erule bigo_const_mult4) 

509 
done 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

510 

55821  511 
lemma bigo_const_mult5 [simp]: 
512 
fixes c :: "'a::linordered_field" 

513 
shows "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. c) *o O(f) = O(f)" 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

514 
apply (auto del: subsetI) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

515 
apply (rule order_trans) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

516 
apply (rule bigo_mult2) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

517 
apply (simp add: func_times) 
41528  518 
apply (auto intro!: simp add: bigo_def elt_set_times_def func_times) 
55821  519 
apply (rule_tac x = "\<lambda>y. inverse c * x y" in exI) 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

520 
apply (simp add: mult.assoc [symmetric] abs_mult) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

521 
apply (rule_tac x = "abs (inverse c) * ca" in exI) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

522 
apply (rule allI) 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

523 
apply (subst mult.assoc) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

524 
apply (rule mult_left_mono) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

525 
apply (erule spec) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

526 
apply force 
22665  527 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

528 

55821  529 
lemma bigo_const_mult6 [intro]: "(\<lambda>x. c) *o O(f) \<subseteq> O(f)" 
41528  530 
apply (auto intro!: simp add: bigo_def elt_set_times_def func_times) 
55821  531 
apply (rule_tac x = "ca * abs c" in exI) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

532 
apply (rule allI) 
55821  533 
apply (subgoal_tac "ca * abs c * abs (f x) = abs c * (ca * abs (f x))") 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

534 
apply (erule ssubst) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

535 
apply (subst abs_mult) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

536 
apply (rule mult_left_mono) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

537 
apply (erule spec) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

538 
apply simp 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

539 
apply(simp add: ac_simps) 
22665  540 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

541 

55821  542 
lemma bigo_const_mult7 [intro]: "f =o O(g) \<Longrightarrow> (\<lambda>x. c * f x) =o O(g)" 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

543 
proof  
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

544 
assume "f =o O(g)" 
55821  545 
then have "(\<lambda>x. c) * f =o (\<lambda>x. c) *o O(g)" 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

546 
by auto 
55821  547 
also have "(\<lambda>x. c) * f = (\<lambda>x. c * f x)" 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

548 
by (simp add: func_times) 
55821  549 
also have "(\<lambda>x. c) *o O(g) \<subseteq> O(g)" 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

550 
by (auto del: subsetI) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

551 
finally show ?thesis . 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

552 
qed 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

553 

55821  554 
lemma bigo_compose1: "f =o O(g) \<Longrightarrow> (\<lambda>x. f (k x)) =o O(\<lambda>x. g (k x))" 
555 
unfolding bigo_def by auto 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

556 

55821  557 
lemma bigo_compose2: "f =o g +o O(h) \<Longrightarrow> 
558 
(\<lambda>x. f (k x)) =o (\<lambda>x. g (k x)) +o O(\<lambda>x. h(k x))" 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
47445
diff
changeset

559 
apply (simp only: set_minus_plus [symmetric] fun_Compl_def func_plus) 
55821  560 
apply (drule bigo_compose1) 
561 
apply (simp add: fun_diff_def) 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
47445
diff
changeset

562 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

563 

22665  564 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

565 
subsection {* Setsum *} 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

566 

55821  567 
lemma bigo_setsum_main: "\<forall>x. \<forall>y \<in> A x. 0 \<le> h x y \<Longrightarrow> 
568 
\<exists>c. \<forall>x. \<forall>y \<in> A x. abs (f x y) \<le> c * (h x y) \<Longrightarrow> 

569 
(\<lambda>x. \<Sum>y \<in> A x. f x y) =o O(\<lambda>x. \<Sum>y \<in> A x. h x y)" 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

570 
apply (auto simp add: bigo_def) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

571 
apply (rule_tac x = "abs c" in exI) 
17199
59c1bfc81d91
moved lemmas that require the HOLComplex logic image to Complex/ex/BigO_Complex.thy;
wenzelm
parents:
16961
diff
changeset

572 
apply (subst abs_of_nonneg) back back 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

573 
apply (rule setsum_nonneg) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

574 
apply force 
19279  575 
apply (subst setsum_right_distrib) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

576 
apply (rule allI) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

577 
apply (rule order_trans) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

578 
apply (rule setsum_abs) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

579 
apply (rule setsum_mono) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

580 
apply (rule order_trans) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

581 
apply (drule spec)+ 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

582 
apply (drule bspec)+ 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

583 
apply assumption+ 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

584 
apply (drule bspec) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

585 
apply assumption+ 
55821  586 
apply (rule mult_right_mono) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

587 
apply (rule abs_ge_self) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

588 
apply force 
22665  589 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

590 

55821  591 
lemma bigo_setsum1: "\<forall>x y. 0 \<le> h x y \<Longrightarrow> 
592 
\<exists>c. \<forall>x y. abs (f x y) \<le> c * h x y \<Longrightarrow> 

593 
(\<lambda>x. \<Sum>y \<in> A x. f x y) =o O(\<lambda>x. \<Sum>y \<in> A x. h x y)" 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

594 
apply (rule bigo_setsum_main) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

595 
apply force 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

596 
apply clarsimp 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

597 
apply (rule_tac x = c in exI) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

598 
apply force 
22665  599 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

600 

55821  601 
lemma bigo_setsum2: "\<forall>y. 0 \<le> h y \<Longrightarrow> 
602 
\<exists>c. \<forall>y. abs (f y) \<le> c * (h y) \<Longrightarrow> 

603 
(\<lambda>x. \<Sum>y \<in> A x. f y) =o O(\<lambda>x. \<Sum>y \<in> A x. h y)" 

604 
by (rule bigo_setsum1) auto 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

605 

55821  606 
lemma bigo_setsum3: "f =o O(h) \<Longrightarrow> 
607 
(\<lambda>x. \<Sum>y \<in> A x. l x y * f (k x y)) =o O(\<lambda>x. \<Sum>y \<in> A x. abs (l x y * h (k x y)))" 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

608 
apply (rule bigo_setsum1) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

609 
apply (rule allI)+ 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

610 
apply (rule abs_ge_zero) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

611 
apply (unfold bigo_def) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

612 
apply auto 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

613 
apply (rule_tac x = c in exI) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

614 
apply (rule allI)+ 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

615 
apply (subst abs_mult)+ 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

616 
apply (subst mult.left_commute) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

617 
apply (rule mult_left_mono) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

618 
apply (erule spec) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

619 
apply (rule abs_ge_zero) 
22665  620 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

621 

55821  622 
lemma bigo_setsum4: "f =o g +o O(h) \<Longrightarrow> 
623 
(\<lambda>x. \<Sum>y \<in> A x. l x y * f (k x y)) =o 

624 
(\<lambda>x. \<Sum>y \<in> A x. l x y * g (k x y)) +o 

625 
O(\<lambda>x. \<Sum>y \<in> A x. abs (l x y * h (k x y)))" 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

626 
apply (rule set_minus_imp_plus) 
26814
b3e8d5ec721d
Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with
berghofe
parents:
25592
diff
changeset

627 
apply (subst fun_diff_def) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

628 
apply (subst setsum_subtractf [symmetric]) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

629 
apply (subst right_diff_distrib [symmetric]) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

630 
apply (rule bigo_setsum3) 
26814
b3e8d5ec721d
Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with
berghofe
parents:
25592
diff
changeset

631 
apply (subst fun_diff_def [symmetric]) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

632 
apply (erule set_plus_imp_minus) 
22665  633 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

634 

55821  635 
lemma bigo_setsum5: "f =o O(h) \<Longrightarrow> \<forall>x y. 0 \<le> l x y \<Longrightarrow> 
636 
\<forall>x. 0 \<le> h x \<Longrightarrow> 

637 
(\<lambda>x. \<Sum>y \<in> A x. l x y * f (k x y)) =o 

638 
O(\<lambda>x. \<Sum>y \<in> A x. l x y * h (k x y))" 

639 
apply (subgoal_tac "(\<lambda>x. \<Sum>y \<in> A x. l x y * h (k x y)) = 

640 
(\<lambda>x. \<Sum>y \<in> A x. abs (l x y * h (k x y)))") 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

641 
apply (erule ssubst) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

642 
apply (erule bigo_setsum3) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

643 
apply (rule ext) 
57418  644 
apply (rule setsum.cong) 
645 
apply (rule refl) 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

646 
apply (subst abs_of_nonneg) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

647 
apply auto 
22665  648 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

649 

55821  650 
lemma bigo_setsum6: "f =o g +o O(h) \<Longrightarrow> \<forall>x y. 0 \<le> l x y \<Longrightarrow> 
651 
\<forall>x. 0 \<le> h x \<Longrightarrow> 

652 
(\<lambda>x. \<Sum>y \<in> A x. l x y * f (k x y)) =o 

653 
(\<lambda>x. \<Sum>y \<in> A x. l x y * g (k x y)) +o 

654 
O(\<lambda>x. \<Sum>y \<in> A x. l x y * h (k x y))" 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

655 
apply (rule set_minus_imp_plus) 
26814
b3e8d5ec721d
Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with
berghofe
parents:
25592
diff
changeset

656 
apply (subst fun_diff_def) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

657 
apply (subst setsum_subtractf [symmetric]) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

658 
apply (subst right_diff_distrib [symmetric]) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

659 
apply (rule bigo_setsum5) 
26814
b3e8d5ec721d
Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with
berghofe
parents:
25592
diff
changeset

660 
apply (subst fun_diff_def [symmetric]) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

661 
apply (drule set_plus_imp_minus) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

662 
apply auto 
22665  663 
done 
664 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

665 

d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

666 
subsection {* Misc useful stuff *} 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

667 

55821  668 
lemma bigo_useful_intro: "A \<subseteq> O(f) \<Longrightarrow> B \<subseteq> O(f) \<Longrightarrow> A + B \<subseteq> O(f)" 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

669 
apply (subst bigo_plus_idemp [symmetric]) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

670 
apply (rule set_plus_mono2) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

671 
apply assumption+ 
22665  672 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

673 

55821  674 
lemma bigo_useful_add: "f =o O(h) \<Longrightarrow> g =o O(h) \<Longrightarrow> f + g =o O(h)" 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

675 
apply (subst bigo_plus_idemp [symmetric]) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

676 
apply (rule set_plus_intro) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

677 
apply assumption+ 
22665  678 
done 
55821  679 

680 
lemma bigo_useful_const_mult: 

681 
fixes c :: "'a::linordered_field" 

682 
shows "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. c) * f =o O(h) \<Longrightarrow> f =o O(h)" 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

683 
apply (rule subsetD) 
55821  684 
apply (subgoal_tac "(\<lambda>x. 1 / c) *o O(h) \<subseteq> O(h)") 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

685 
apply assumption 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

686 
apply (rule bigo_const_mult6) 
55821  687 
apply (subgoal_tac "f = (\<lambda>x. 1 / c) * ((\<lambda>x. c) * f)") 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

688 
apply (erule ssubst) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

689 
apply (erule set_times_intro2) 
23413
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23373
diff
changeset

690 
apply (simp add: func_times) 
22665  691 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

692 

55821  693 
lemma bigo_fix: "(\<lambda>x::nat. f (x + 1)) =o O(\<lambda>x. h (x + 1)) \<Longrightarrow> f 0 = 0 \<Longrightarrow> f =o O(h)" 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

694 
apply (simp add: bigo_alt_def) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

695 
apply auto 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

696 
apply (rule_tac x = c in exI) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

697 
apply auto 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

698 
apply (case_tac "x = 0") 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

699 
apply simp 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

700 
apply (subgoal_tac "x = Suc (x  1)") 
17199
59c1bfc81d91
moved lemmas that require the HOLComplex logic image to Complex/ex/BigO_Complex.thy;
wenzelm
parents:
16961
diff
changeset

701 
apply (erule ssubst) back 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

702 
apply (erule spec) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

703 
apply simp 
22665  704 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

705 

55821  706 
lemma bigo_fix2: 
707 
"(\<lambda>x. f ((x::nat) + 1)) =o (\<lambda>x. g(x + 1)) +o O(\<lambda>x. h(x + 1)) \<Longrightarrow> 

708 
f 0 = g 0 \<Longrightarrow> f =o g +o O(h)" 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

709 
apply (rule set_minus_imp_plus) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

710 
apply (rule bigo_fix) 
26814
b3e8d5ec721d
Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with
berghofe
parents:
25592
diff
changeset

711 
apply (subst fun_diff_def) 
b3e8d5ec721d
Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with
berghofe
parents:
25592
diff
changeset

712 
apply (subst fun_diff_def [symmetric]) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

713 
apply (rule set_plus_imp_minus) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

714 
apply simp 
26814
b3e8d5ec721d
Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with
berghofe
parents:
25592
diff
changeset

715 
apply (simp add: fun_diff_def) 
22665  716 
done 
717 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

718 

d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

719 
subsection {* Less than or equal to *} 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

720 

55821  721 
definition lesso :: "('a \<Rightarrow> 'b::linordered_idom) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" (infixl "<o" 70) 
722 
where "f <o g = (\<lambda>x. max (f x  g x) 0)" 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

723 

55821  724 
lemma bigo_lesseq1: "f =o O(h) \<Longrightarrow> \<forall>x. abs (g x) \<le> abs (f x) \<Longrightarrow> g =o O(h)" 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

725 
apply (unfold bigo_def) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

726 
apply clarsimp 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

727 
apply (rule_tac x = c in exI) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

728 
apply (rule allI) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

729 
apply (rule order_trans) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

730 
apply (erule spec)+ 
22665  731 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

732 

55821  733 
lemma bigo_lesseq2: "f =o O(h) \<Longrightarrow> \<forall>x. abs (g x) \<le> f x \<Longrightarrow> g =o O(h)" 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

734 
apply (erule bigo_lesseq1) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

735 
apply (rule allI) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

736 
apply (drule_tac x = x in spec) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

737 
apply (rule order_trans) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

738 
apply assumption 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

739 
apply (rule abs_ge_self) 
22665  740 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

741 

55821  742 
lemma bigo_lesseq3: "f =o O(h) \<Longrightarrow> \<forall>x. 0 \<le> g x \<Longrightarrow> \<forall>x. g x \<le> f x \<Longrightarrow> g =o O(h)" 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

743 
apply (erule bigo_lesseq2) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

744 
apply (rule allI) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

745 
apply (subst abs_of_nonneg) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

746 
apply (erule spec)+ 
22665  747 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

748 

55821  749 
lemma bigo_lesseq4: "f =o O(h) \<Longrightarrow> 
750 
\<forall>x. 0 \<le> g x \<Longrightarrow> \<forall>x. g x \<le> abs (f x) \<Longrightarrow> g =o O(h)" 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

751 
apply (erule bigo_lesseq1) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

752 
apply (rule allI) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

753 
apply (subst abs_of_nonneg) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

754 
apply (erule spec)+ 
22665  755 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

756 

55821  757 
lemma bigo_lesso1: "\<forall>x. f x \<le> g x \<Longrightarrow> f <o g =o O(h)" 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

758 
apply (unfold lesso_def) 
55821  759 
apply (subgoal_tac "(\<lambda>x. max (f x  g x) 0) = 0") 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

760 
apply (erule ssubst) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

761 
apply (rule bigo_zero) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

762 
apply (unfold func_zero) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

763 
apply (rule ext) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

764 
apply (simp split: split_max) 
22665  765 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

766 

55821  767 
lemma bigo_lesso2: "f =o g +o O(h) \<Longrightarrow> 
768 
\<forall>x. 0 \<le> k x \<Longrightarrow> \<forall>x. k x \<le> f x \<Longrightarrow> k <o g =o O(h)" 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

769 
apply (unfold lesso_def) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

770 
apply (rule bigo_lesseq4) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

771 
apply (erule set_plus_imp_minus) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

772 
apply (rule allI) 
54863
82acc20ded73
prefer more canonical names for lemmas on min/max
haftmann
parents:
54230
diff
changeset

773 
apply (rule max.cobounded2) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

774 
apply (rule allI) 
26814
b3e8d5ec721d
Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with
berghofe
parents:
25592
diff
changeset

775 
apply (subst fun_diff_def) 
55821  776 
apply (case_tac "0 \<le> k x  g x") 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

777 
apply simp 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

778 
apply (subst abs_of_nonneg) 
17199
59c1bfc81d91
moved lemmas that require the HOLComplex logic image to Complex/ex/BigO_Complex.thy;
wenzelm
parents:
16961
diff
changeset

779 
apply (drule_tac x = x in spec) back 
29667  780 
apply (simp add: algebra_simps) 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
47445
diff
changeset

781 
apply (subst diff_conv_add_uminus)+ 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

782 
apply (rule add_right_mono) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

783 
apply (erule spec) 
55821  784 
apply (rule order_trans) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

785 
prefer 2 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

786 
apply (rule abs_ge_zero) 
29667  787 
apply (simp add: algebra_simps) 
22665  788 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

789 

55821  790 
lemma bigo_lesso3: "f =o g +o O(h) \<Longrightarrow> 
791 
\<forall>x. 0 \<le> k x \<Longrightarrow> \<forall>x. g x \<le> k x \<Longrightarrow> f <o k =o O(h)" 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

792 
apply (unfold lesso_def) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

793 
apply (rule bigo_lesseq4) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

794 
apply (erule set_plus_imp_minus) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

795 
apply (rule allI) 
54863
82acc20ded73
prefer more canonical names for lemmas on min/max
haftmann
parents:
54230
diff
changeset

796 
apply (rule max.cobounded2) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

797 
apply (rule allI) 
26814
b3e8d5ec721d
Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with
berghofe
parents:
25592
diff
changeset

798 
apply (subst fun_diff_def) 
55821  799 
apply (case_tac "0 \<le> f x  k x") 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

800 
apply simp 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

801 
apply (subst abs_of_nonneg) 
17199
59c1bfc81d91
moved lemmas that require the HOLComplex logic image to Complex/ex/BigO_Complex.thy;
wenzelm
parents:
16961
diff
changeset

802 
apply (drule_tac x = x in spec) back 
29667  803 
apply (simp add: algebra_simps) 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
47445
diff
changeset

804 
apply (subst diff_conv_add_uminus)+ 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

805 
apply (rule add_left_mono) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

806 
apply (rule le_imp_neg_le) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

807 
apply (erule spec) 
55821  808 
apply (rule order_trans) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

809 
prefer 2 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

810 
apply (rule abs_ge_zero) 
29667  811 
apply (simp add: algebra_simps) 
22665  812 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

813 

55821  814 
lemma bigo_lesso4: 
815 
fixes k :: "'a \<Rightarrow> 'b::linordered_field" 

816 
shows "f <o g =o O(k) \<Longrightarrow> g =o h +o O(k) \<Longrightarrow> f <o h =o O(k)" 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

817 
apply (unfold lesso_def) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

818 
apply (drule set_plus_imp_minus) 
17199
59c1bfc81d91
moved lemmas that require the HOLComplex logic image to Complex/ex/BigO_Complex.thy;
wenzelm
parents:
16961
diff
changeset

819 
apply (drule bigo_abs5) back 
26814
b3e8d5ec721d
Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with
berghofe
parents:
25592
diff
changeset

820 
apply (simp add: fun_diff_def) 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

821 
apply (drule bigo_useful_add) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

822 
apply assumption 
17199
59c1bfc81d91
moved lemmas that require the HOLComplex logic image to Complex/ex/BigO_Complex.thy;
wenzelm
parents:
16961
diff
changeset

823 
apply (erule bigo_lesseq2) back 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

824 
apply (rule allI) 
55821  825 
apply (auto simp add: func_plus fun_diff_def algebra_simps split: split_max abs_split) 
22665  826 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

827 

55821  828 
lemma bigo_lesso5: "f <o g =o O(h) \<Longrightarrow> \<exists>C. \<forall>x. f x \<le> g x + C * abs (h x)" 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

829 
apply (simp only: lesso_def bigo_alt_def) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

830 
apply clarsimp 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

831 
apply (rule_tac x = c in exI) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

832 
apply (rule allI) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

833 
apply (drule_tac x = x in spec) 
55821  834 
apply (subgoal_tac "abs (max (f x  g x) 0) = max (f x  g x) 0") 
835 
apply (clarsimp simp add: algebra_simps) 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

836 
apply (rule abs_of_nonneg) 
54863
82acc20ded73
prefer more canonical names for lemmas on min/max
haftmann
parents:
54230
diff
changeset

837 
apply (rule max.cobounded2) 
22665  838 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

839 

55821  840 
lemma lesso_add: "f <o g =o O(h) \<Longrightarrow> k <o l =o O(h) \<Longrightarrow> (f + k) <o (g + l) =o O(h)" 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

841 
apply (unfold lesso_def) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

842 
apply (rule bigo_lesseq3) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

843 
apply (erule bigo_useful_add) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

844 
apply assumption 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

845 
apply (force split: split_max) 
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

846 
apply (auto split: split_max simp add: func_plus) 
22665  847 
done 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

848 

55821  849 
lemma bigo_LIMSEQ1: "f =o O(g) \<Longrightarrow> g > 0 \<Longrightarrow> f > (0::real)" 
31337  850 
apply (simp add: LIMSEQ_iff bigo_alt_def) 
29786  851 
apply clarify 
852 
apply (drule_tac x = "r / c" in spec) 

853 
apply (drule mp) 

56541  854 
apply simp 
29786  855 
apply clarify 
856 
apply (rule_tac x = no in exI) 

857 
apply (rule allI) 

858 
apply (drule_tac x = n in spec)+ 

859 
apply (rule impI) 

860 
apply (drule mp) 

861 
apply assumption 

862 
apply (rule order_le_less_trans) 

863 
apply assumption 

864 
apply (rule order_less_le_trans) 

55821  865 
apply (subgoal_tac "c * abs (g n) < c * (r / c)") 
29786  866 
apply assumption 
867 
apply (erule mult_strict_left_mono) 

868 
apply assumption 

869 
apply simp 

55821  870 
done 
29786  871 

55821  872 
lemma bigo_LIMSEQ2: "f =o g +o O(h) \<Longrightarrow> h > 0 \<Longrightarrow> f > a \<Longrightarrow> g > (a::real)" 
29786  873 
apply (drule set_plus_imp_minus) 
874 
apply (drule bigo_LIMSEQ1) 

875 
apply assumption 

876 
apply (simp only: fun_diff_def) 

877 
apply (erule LIMSEQ_diff_approach_zero2) 

878 
apply assumption 

55821  879 
done 
29786  880 

16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset

881 
end 