author  haftmann 
Tue, 04 May 2010 08:55:43 +0200  
changeset 36635  080b755377c0 
parent 31381  b3a785a69538 
child 36809  354b15d5b4ca 
permissions  rwrr 
31381  1 

2 
(* Author: Florian Haftmann, TU Muenchen *) 

3 

4 
header {* Comparing growth of functions on natural numbers by a preorder relation *} 

5 

6 
theory Landau 

7 
imports Main Preorder 

8 
begin 

9 

10 
text {* 

11 
We establish a preorder releation @{text "\<lesssim>"} on functions 

12 
from @{text "\<nat>"} to @{text "\<nat>"} such that @{text "f \<lesssim> g \<longleftrightarrow> f \<in> O(g)"}. 

13 
*} 

14 

15 
subsection {* Auxiliary *} 

16 

17 
lemma Ex_All_bounded: 

18 
fixes n :: nat 

19 
assumes "\<exists>n. \<forall>m\<ge>n. P m" 

20 
obtains m where "m \<ge> n" and "P m" 

21 
proof  

22 
from assms obtain q where m_q: "\<forall>m\<ge>q. P m" .. 

23 
let ?m = "max q n" 

24 
have "?m \<ge> n" by auto 

25 
moreover from m_q have "P ?m" by auto 

26 
ultimately show thesis .. 

27 
qed 

28 

29 

30 
subsection {* The @{text "\<lesssim>"} relation *} 

31 

32 
definition less_eq_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<lesssim>" 50) where 

33 
"f \<lesssim> g \<longleftrightarrow> (\<exists>c n. \<forall>m\<ge>n. f m \<le> Suc c * g m)" 

34 

35 
lemma less_eq_fun_intro: 

36 
assumes "\<exists>c n. \<forall>m\<ge>n. f m \<le> Suc c * g m" 

37 
shows "f \<lesssim> g" 

38 
unfolding less_eq_fun_def by (rule assms) 

39 

40 
lemma less_eq_fun_not_intro: 

41 
assumes "\<And>c n. \<exists>m\<ge>n. Suc c * g m < f m" 

42 
shows "\<not> f \<lesssim> g" 

43 
using assms unfolding less_eq_fun_def linorder_not_le [symmetric] 

44 
by blast 

45 

46 
lemma less_eq_fun_elim: 

47 
assumes "f \<lesssim> g" 

48 
obtains n c where "\<And>m. m \<ge> n \<Longrightarrow> f m \<le> Suc c * g m" 

49 
using assms unfolding less_eq_fun_def by blast 

50 

51 
lemma less_eq_fun_not_elim: 

52 
assumes "\<not> f \<lesssim> g" 

53 
obtains m where "m \<ge> n" and "Suc c * g m < f m" 

54 
using assms unfolding less_eq_fun_def linorder_not_le [symmetric] 

55 
by blast 

56 

57 
lemma less_eq_fun_refl: 

58 
"f \<lesssim> f" 

59 
proof (rule less_eq_fun_intro) 

60 
have "\<exists>n. \<forall>m\<ge>n. f m \<le> Suc 0 * f m" by auto 

61 
then show "\<exists>c n. \<forall>m\<ge>n. f m \<le> Suc c * f m" by blast 

62 
qed 

63 

64 
lemma less_eq_fun_trans: 

65 
assumes f_g: "f \<lesssim> g" and g_h: "g \<lesssim> h" 

66 
shows f_h: "f \<lesssim> h" 

67 
proof  

68 
from f_g obtain n\<^isub>1 c\<^isub>1 

69 
where P1: "\<And>m. m \<ge> n\<^isub>1 \<Longrightarrow> f m \<le> Suc c\<^isub>1 * g m" 

70 
by (erule less_eq_fun_elim) 

71 
moreover from g_h obtain n\<^isub>2 c\<^isub>2 

72 
where P2: "\<And>m. m \<ge> n\<^isub>2 \<Longrightarrow> g m \<le> Suc c\<^isub>2 * h m" 

73 
by (erule less_eq_fun_elim) 

74 
ultimately have "\<And>m. m \<ge> max n\<^isub>1 n\<^isub>2 \<Longrightarrow> f m \<le> Suc c\<^isub>1 * g m \<and> g m \<le> Suc c\<^isub>2 * h m" 

75 
by auto 

76 
moreover { 

77 
fix k l r :: nat 

78 
assume k_l: "k \<le> Suc c\<^isub>1 * l" and l_r: "l \<le> Suc c\<^isub>2 * r" 

79 
from l_r have "Suc c\<^isub>1 * l \<le> (Suc c\<^isub>1 * Suc c\<^isub>2) * r" 

80 
by (auto simp add: mult_le_cancel_left mult_assoc simp del: times_nat.simps mult_Suc_right) 

81 
with k_l have "k \<le> (Suc c\<^isub>1 * Suc c\<^isub>2) * r" by (rule preorder_class.order_trans) 

82 
} 

83 
ultimately have "\<And>m. m \<ge> max n\<^isub>1 n\<^isub>2 \<Longrightarrow> f m \<le> (Suc c\<^isub>1 * Suc c\<^isub>2) * h m" by auto 

84 
then have "\<And>m. m \<ge> max n\<^isub>1 n\<^isub>2 \<Longrightarrow> f m \<le> Suc ((Suc c\<^isub>1 * Suc c\<^isub>2)  1) * h m" by auto 

85 
then show ?thesis unfolding less_eq_fun_def by blast 

86 
qed 

87 

88 

89 
subsection {* The @{text "\<approx>"} relation, the equivalence relation induced by @{text "\<lesssim>"} *} 

90 

91 
definition equiv_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<cong>" 50) where 

92 
"f \<cong> g \<longleftrightarrow> (\<exists>d c n. \<forall>m\<ge>n. g m \<le> Suc d * f m \<and> f m \<le> Suc c * g m)" 

93 

94 
lemma equiv_fun_intro: 

95 
assumes "\<exists>d c n. \<forall>m\<ge>n. g m \<le> Suc d * f m \<and> f m \<le> Suc c * g m" 

96 
shows "f \<cong> g" 

97 
unfolding equiv_fun_def by (rule assms) 

98 

99 
lemma equiv_fun_not_intro: 

100 
assumes "\<And>d c n. \<exists>m\<ge>n. Suc d * f m < g m \<or> Suc c * g m < f m" 

101 
shows "\<not> f \<cong> g" 

102 
unfolding equiv_fun_def 

103 
by (auto simp add: assms linorder_not_le 

104 
simp del: times_nat.simps mult_Suc_right) 

105 

106 
lemma equiv_fun_elim: 

107 
assumes "f \<cong> g" 

108 
obtains n d c 

109 
where "\<And>m. m \<ge> n \<Longrightarrow> g m \<le> Suc d * f m \<and> f m \<le> Suc c * g m" 

110 
using assms unfolding equiv_fun_def by blast 

111 

112 
lemma equiv_fun_not_elim: 

113 
fixes n d c 

114 
assumes "\<not> f \<cong> g" 

115 
obtains m where "m \<ge> n" 

116 
and "Suc d * f m < g m \<or> Suc c * g m < f m" 

117 
using assms unfolding equiv_fun_def 

118 
by (auto simp add: linorder_not_le, blast) 

119 

120 
lemma equiv_fun_less_eq_fun: 

121 
"f \<cong> g \<longleftrightarrow> f \<lesssim> g \<and> g \<lesssim> f" 

122 
proof 

123 
assume x_y: "f \<cong> g" 

124 
then obtain n d c 

125 
where interv: "\<And>m. m \<ge> n \<Longrightarrow> g m \<le> Suc d * f m \<and> f m \<le> Suc c * g m" 

126 
by (erule equiv_fun_elim) 

127 
from interv have "\<exists>c n. \<forall>m \<ge> n. f m \<le> Suc c * g m" by auto 

128 
then have f_g: "f \<lesssim> g" by (rule less_eq_fun_intro) 

129 
from interv have "\<exists>d n. \<forall>m \<ge> n. g m \<le> Suc d * f m" by auto 

130 
then have g_f: "g \<lesssim> f" by (rule less_eq_fun_intro) 

131 
from f_g g_f show "f \<lesssim> g \<and> g \<lesssim> f" by auto 

132 
next 

133 
assume assm: "f \<lesssim> g \<and> g \<lesssim> f" 

134 
from assm less_eq_fun_elim obtain c n\<^isub>1 where 

135 
bound1: "\<And>m. m \<ge> n\<^isub>1 \<Longrightarrow> f m \<le> Suc c * g m" 

136 
by blast 

137 
from assm less_eq_fun_elim obtain d n\<^isub>2 where 

138 
bound2: "\<And>m. m \<ge> n\<^isub>2 \<Longrightarrow> g m \<le> Suc d * f m" 

139 
by blast 

140 
from bound2 have "\<And>m. m \<ge> max n\<^isub>1 n\<^isub>2 \<Longrightarrow> g m \<le> Suc d * f m" 

141 
by auto 

142 
with bound1 

143 
have "\<forall>m \<ge> max n\<^isub>1 n\<^isub>2. g m \<le> Suc d * f m \<and> f m \<le> Suc c * g m" 

144 
by auto 

145 
then 

146 
have "\<exists>d c n. \<forall>m\<ge>n. g m \<le> Suc d * f m \<and> f m \<le> Suc c * g m" 

147 
by blast 

148 
then show "f \<cong> g" by (rule equiv_fun_intro) 

149 
qed 

150 

151 
subsection {* The @{text "\<prec>"} relation, the strict part of @{text "\<lesssim>"} *} 

152 

153 
definition less_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<prec>" 50) where 

154 
"f \<prec> g \<longleftrightarrow> f \<lesssim> g \<and> \<not> g \<lesssim> f" 

155 

156 
lemma less_fun_intro: 

157 
assumes "\<And>c. \<exists>n. \<forall>m\<ge>n. Suc c * f m < g m" 

158 
shows "f \<prec> g" 

159 
proof (unfold less_fun_def, rule conjI) 

160 
from assms obtain n 

161 
where "\<forall>m\<ge>n. Suc 0 * f m < g m" .. 

162 
then have "\<forall>m\<ge>n. f m \<le> Suc 0 * g m" by auto 

163 
then have "\<exists>c n. \<forall>m\<ge>n. f m \<le> Suc c * g m" by blast 

164 
then show "f \<lesssim> g" by (rule less_eq_fun_intro) 

165 
next 

166 
show "\<not> g \<lesssim> f" 

167 
proof (rule less_eq_fun_not_intro) 

168 
fix c n :: nat 

169 
from assms have "\<exists>n. \<forall>m\<ge>n. Suc c * f m < g m" by blast 

170 
then obtain m where "m \<ge> n" and "Suc c * f m < g m" 

171 
by (rule Ex_All_bounded) 

172 
then show "\<exists>m\<ge>n. Suc c * f m < g m" by blast 

173 
qed 

174 
qed 

175 

176 
text {* 

177 
We would like to show (or refute) that @{text "f \<prec> g \<longleftrightarrow> f \<in> o(g)"}, 

178 
i.e.~@{prop "f \<prec> g \<longleftrightarrow> (\<forall>c. \<exists>n. \<forall>m>n. f m < Suc c * g m)"} but did not manage to 

179 
do so. 

180 
*} 

181 

182 

183 
subsection {* Assert that @{text "\<lesssim>"} is ineed a preorder *} 

184 

185 
interpretation fun_order: preorder_equiv less_eq_fun less_fun 

186 
where "preorder_equiv.equiv less_eq_fun = equiv_fun" 

187 
proof  

188 
interpret preorder_equiv less_eq_fun less_fun proof 

189 
qed (simp_all add: less_fun_def less_eq_fun_refl, auto intro: less_eq_fun_trans) 

36635
080b755377c0
locale predicates of classes carry a mandatory "class" prefix
haftmann
parents:
31381
diff
changeset

190 
show "class.preorder_equiv less_eq_fun less_fun" using preorder_equiv_axioms . 
31381  191 
show "preorder_equiv.equiv less_eq_fun = equiv_fun" 
192 
by (simp add: expand_fun_eq equiv_def equiv_fun_less_eq_fun) 

193 
qed 

194 

195 

196 
subsection {* Simple examples *} 

197 

198 
lemma "(\<lambda>_. n) \<lesssim> (\<lambda>n. n)" 

199 
proof (rule less_eq_fun_intro) 

200 
show "\<exists>c q. \<forall>m\<ge>q. n \<le> Suc c * m" 

201 
proof  

202 
have "\<forall>m\<ge>n. n \<le> Suc 0 * m" by simp 

203 
then show ?thesis by blast 

204 
qed 

205 
qed 

206 

207 
lemma "(\<lambda>n. n) \<cong> (\<lambda>n. Suc k * n)" 

208 
proof (rule equiv_fun_intro) 

209 
show "\<exists>d c n. \<forall>m\<ge>n. Suc k * m \<le> Suc d * m \<and> m \<le> Suc c * (Suc k * m)" 

210 
proof  

211 
have "\<forall>m\<ge>n. Suc k * m \<le> Suc k * m \<and> m \<le> Suc c * (Suc k * m)" by simp 

212 
then show ?thesis by blast 

213 
qed 

214 
qed 

215 

216 
lemma "(\<lambda>_. n) \<prec> (\<lambda>n. n)" 

217 
proof (rule less_fun_intro) 

218 
fix c 

219 
show "\<exists>q. \<forall>m\<ge>q. Suc c * n < m" 

220 
proof  

221 
have "\<forall>m\<ge>Suc c * n + 1. Suc c * n < m" by simp 

222 
then show ?thesis by blast 

223 
qed 

224 
qed 

225 

226 
end 