src/HOL/Library/Function_Growth.thy
 author Andreas Lochbihler Wed Feb 27 10:33:30 2013 +0100 (2013-02-27) changeset 51288 be7e9a675ec9 parent 51264 aba03f0c6254 child 51542 738598beeb26 permissions -rw-r--r--
add wellorder instance for Numeral_Type (suggested by Jesus Aransay)
2 (* Author: Florian Haftmann, TU Muenchen *)
4 header {* Comparing growth of functions on natural numbers by a preorder relation *}
6 theory Function_Growth
7 imports Main "~~/src/HOL/Library/Preorder" "~~/src/HOL/Library/Discrete"
8 begin
10 subsection {* Motivation *}
12 text {*
13   When comparing growth of functions in computer science, it is common to adhere
14   on Landau Symbols (O-Notation'').  However these come at the cost of notational
15   oddities, particularly writing @{text "f = O(g)"} for @{text "f \<in> O(g)"} etc.
17   Here we suggest a diffent way, following Hardy (G.~H.~Hardy and J.~E.~Littlewood,
18   Some problems of Diophantine approximation, Acta Mathematica 37 (1914), p.~225).
19   We establish a quasi order relation @{text "\<lesssim>"} on functions such that
20   @{text "f \<lesssim> g \<longleftrightarrow> f \<in> O(g)"}.  From a didactic point of view, this does not only
21   avoid the notational oddities mentioned above but also emphasizes the key insight
22   of a growth hierachy of functions:
23   @{text "(\<lambda>n. 0) \<lesssim> (\<lambda>n. k) \<lesssim> Discrete.log \<lesssim> Discrete.sqrt \<lesssim> id \<lesssim> \<dots>"}.
24 *}
26 subsection {* Model *}
28 text {*
29   Our growth functions are of type @{text "\<nat> \<Rightarrow> \<nat>"}.  This is different
30   to the usual conventions for Landau symbols for which @{text "\<real> \<Rightarrow> \<real>"}
31   would be appropriate, but we argue that @{text "\<real> \<Rightarrow> \<real>"} is more
32   appropriate for analysis, whereas our setting is discrete.
34   Note that we also restrict the additional coefficients to @{text \<nat>}, something
35   we discuss at the particular definitions.
36 *}
38 subsection {* The @{text "\<lesssim>"} relation *}
40 definition less_eq_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<lesssim>" 50)
41 where
42   "f \<lesssim> g \<longleftrightarrow> (\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m)"
44 text {*
45   This yields @{text "f \<lesssim> g \<longleftrightarrow> f \<in> O(g)"}.  Note that @{text c} is restricted to
46   @{text \<nat>}.  This does not pose any problems since if @{text "f \<in> O(g)"} holds for
47   a @{text "c \<in> \<real>"}, it also holds for @{text "\<lceil>c\<rceil> \<in> \<nat>"} by transitivity.
48 *}
50 lemma less_eq_funI [intro?]:
51   assumes "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m"
52   shows "f \<lesssim> g"
53   unfolding less_eq_fun_def by (rule assms)
55 lemma not_less_eq_funI:
56   assumes "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * g m < f m"
57   shows "\<not> f \<lesssim> g"
58   using assms unfolding less_eq_fun_def linorder_not_le [symmetric] by blast
60 lemma less_eq_funE [elim?]:
61   assumes "f \<lesssim> g"
62   obtains n c where "c > 0" and "\<And>m. m > n \<Longrightarrow> f m \<le> c * g m"
63   using assms unfolding less_eq_fun_def by blast
65 lemma not_less_eq_funE:
66   assumes "\<not> f \<lesssim> g" and "c > 0"
67   obtains m where "m > n" and "c * g m < f m"
68   using assms unfolding less_eq_fun_def linorder_not_le [symmetric] by blast
71 subsection {* The @{text "\<approx>"} relation, the equivalence relation induced by @{text "\<lesssim>"} *}
73 definition equiv_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<cong>" 50)
74 where
75   "f \<cong> g \<longleftrightarrow>
76     (\<exists>c\<^isub>1>0. \<exists>c\<^isub>2>0. \<exists>n. \<forall>m>n. f m \<le> c\<^isub>1 * g m \<and> g m \<le> c\<^isub>2 * f m)"
78 text {*
79   This yields @{text "f \<cong> g \<longleftrightarrow> f \<in> \<Theta>(g)"}.  Concerning @{text "c\<^isub>1"} and @{text "c\<^isub>2"}
80   restricted to @{typ nat}, see note above on @{text "(\<lesssim>)"}.
81 *}
83 lemma equiv_funI [intro?]:
84   assumes "\<exists>c\<^isub>1>0. \<exists>c\<^isub>2>0. \<exists>n. \<forall>m>n. f m \<le> c\<^isub>1 * g m \<and> g m \<le> c\<^isub>2 * f m"
85   shows "f \<cong> g"
86   unfolding equiv_fun_def by (rule assms)
88 lemma not_equiv_funI:
89   assumes "\<And>c\<^isub>1 c\<^isub>2 n. c\<^isub>1 > 0 \<Longrightarrow> c\<^isub>2 > 0 \<Longrightarrow>
90     \<exists>m>n. c\<^isub>1 * f m < g m \<or> c\<^isub>2 * g m < f m"
91   shows "\<not> f \<cong> g"
92   using assms unfolding equiv_fun_def linorder_not_le [symmetric] by blast
94 lemma equiv_funE [elim?]:
95   assumes "f \<cong> g"
96   obtains n c\<^isub>1 c\<^isub>2 where "c\<^isub>1 > 0" and "c\<^isub>2 > 0"
97     and "\<And>m. m > n \<Longrightarrow> f m \<le> c\<^isub>1 * g m \<and> g m \<le> c\<^isub>2 * f m"
98   using assms unfolding equiv_fun_def by blast
100 lemma not_equiv_funE:
101   fixes n c\<^isub>1 c\<^isub>2
102   assumes "\<not> f \<cong> g" and "c\<^isub>1 > 0" and "c\<^isub>2 > 0"
103   obtains m where "m > n"
104     and "c\<^isub>1 * f m < g m \<or> c\<^isub>2 * g m < f m"
105   using assms unfolding equiv_fun_def linorder_not_le [symmetric] by blast
108 subsection {* The @{text "\<prec>"} relation, the strict part of @{text "\<lesssim>"} *}
110 definition less_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<prec>" 50)
111 where
112   "f \<prec> g \<longleftrightarrow> f \<lesssim> g \<and> \<not> g \<lesssim> f"
114 lemma less_funI:
115   assumes "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m"
116     and "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * f m < g m"
117   shows "f \<prec> g"
118   using assms unfolding less_fun_def less_eq_fun_def linorder_not_less [symmetric] by blast
120 lemma not_less_funI:
121   assumes "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * g m < f m"
122     and "\<exists>c>0. \<exists>n. \<forall>m>n. g m \<le> c * f m"
123   shows "\<not> f \<prec> g"
124   using assms unfolding less_fun_def less_eq_fun_def linorder_not_less [symmetric] by blast
126 lemma less_funE [elim?]:
127   assumes "f \<prec> g"
128   obtains n c where "c > 0" and "\<And>m. m > n \<Longrightarrow> f m \<le> c * g m"
129     and "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * f m < g m"
130 proof -
131   from assms have "f \<lesssim> g" and "\<not> g \<lesssim> f" by (simp_all add: less_fun_def)
132   from f \<lesssim> g obtain n c where *:"c > 0" "\<And>m. m > n \<Longrightarrow> f m \<le> c * g m"
133     by (rule less_eq_funE) blast
134   { fix c n :: nat
135     assume "c > 0"
136     with \<not> g \<lesssim> f obtain m where "m > n" "c * f m < g m"
137       by (rule not_less_eq_funE) blast
138     then have **: "\<exists>m>n. c * f m < g m" by blast
139   } note ** = this
140   from * ** show thesis by (rule that)
141 qed
143 lemma not_less_funE:
144   assumes "\<not> f \<prec> g" and "c > 0"
145   obtains m where "m > n" and "c * g m < f m"
146     | d q where "\<And>m. d > 0 \<Longrightarrow> m > q \<Longrightarrow> g q \<le> d * f q"
147   using assms unfolding less_fun_def linorder_not_less [symmetric] by blast
149 text {*
150   I did not found a proof for @{text "f \<prec> g \<longleftrightarrow> f \<in> o(g)"}.  Maybe this only
151   holds if @{text f} and/or @{text g} are of a certain class of functions.
152   However @{text "f \<in> o(g) \<longrightarrow> f \<prec> g"} is provable, and this yields a
153   handy introduction rule.
155   Note that D. Knuth ignores @{text o} altogether.  So what \dots
157   Something still has to be said about the coefficient @{text c} in
158   the definition of @{text "(\<prec>)"}.  In the typical definition of @{text o},
159   it occurs on the \emph{right} hand side of the @{text "(>)"}.  The reason
160   is that the situation is dual to the definition of @{text O}: the definition
161   works since @{text c} may become arbitrary small.  Since this is not possible
162   within @{term \<nat>}, we push the coefficient to the left hand side instead such
163   that it become arbitrary big instead.
164 *}
166 lemma less_fun_strongI:
167   assumes "\<And>c. c > 0 \<Longrightarrow> \<exists>n. \<forall>m>n. c * f m < g m"
168   shows "f \<prec> g"
169 proof (rule less_funI)
170   have "1 > (0::nat)" by simp
171   from assms 1 > 0 have "\<exists>n. \<forall>m>n. 1 * f m < g m" .
172   then obtain n where *: "\<And>m. m > n \<Longrightarrow> 1 * f m < g m" by blast
173   have "\<forall>m>n. f m \<le> 1 * g m"
174   proof (rule allI, rule impI)
175     fix m
176     assume "m > n"
177     with * have "1 * f m < g m" by simp
178     then show "f m \<le> 1 * g m" by simp
179   qed
180   with 1 > 0 show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m" by blast
181   fix c n :: nat
182   assume "c > 0"
183   with assms obtain q where "\<And>m. m > q \<Longrightarrow> c * f m < g m" by blast
184   then have "c * f (Suc (q + n)) < g (Suc (q + n))" by simp
185   moreover have "Suc (q + n) > n" by simp
186   ultimately show "\<exists>m>n. c * f m < g m" by blast
187 qed
190 subsection {* @{text "\<lesssim>"} is a preorder *}
192 text {* This yields all lemmas relating @{text "\<lesssim>"}, @{text "\<prec>"} and @{text "\<cong>"}. *}
194 interpretation fun_order: preorder_equiv less_eq_fun less_fun
195   where "preorder_equiv.equiv less_eq_fun = equiv_fun"
196 proof -
197   interpret preorder: preorder_equiv less_eq_fun less_fun
198   proof
199     fix f g h
200     show "f \<lesssim> f"
201     proof
202       have "\<exists>n. \<forall>m>n. f m \<le> 1 * f m" by auto
203       then show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * f m" by blast
204     qed
205     show "f \<prec> g \<longleftrightarrow> f \<lesssim> g \<and> \<not> g \<lesssim> f"
206       by (fact less_fun_def)
207     assume "f \<lesssim> g" and "g \<lesssim> h"
208     show "f \<lesssim> h"
209     proof
210       from f \<lesssim> g obtain n\<^isub>1 c\<^isub>1
211         where "c\<^isub>1 > 0" and P\<^isub>1: "\<And>m. m > n\<^isub>1 \<Longrightarrow> f m \<le> c\<^isub>1 * g m"
212         by rule blast
213       from g \<lesssim> h obtain n\<^isub>2 c\<^isub>2
214         where "c\<^isub>2 > 0" and P\<^isub>2: "\<And>m. m > n\<^isub>2 \<Longrightarrow> g m \<le> c\<^isub>2 * h m"
215         by rule blast
216       have "\<forall>m>max n\<^isub>1 n\<^isub>2. f m \<le> (c\<^isub>1 * c\<^isub>2) * h m"
217       proof (rule allI, rule impI)
218         fix m
219         assume Q: "m > max n\<^isub>1 n\<^isub>2"
220         from P\<^isub>1 Q have *: "f m \<le> c\<^isub>1 * g m" by simp
221         from P\<^isub>2 Q have "g m \<le> c\<^isub>2 * h m" by simp
222         with c\<^isub>1 > 0 have "c\<^isub>1 * g m \<le> (c\<^isub>1 * c\<^isub>2) * h m" by simp
223         with * show "f m \<le> (c\<^isub>1 * c\<^isub>2) * h m" by (rule order_trans)
224       qed
225       then have "\<exists>n. \<forall>m>n. f m \<le> (c\<^isub>1 * c\<^isub>2) * h m" by rule
226       moreover from c\<^isub>1 > 0 c\<^isub>2 > 0 have "c\<^isub>1 * c\<^isub>2 > 0" by (rule mult_pos_pos)
227       ultimately show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * h m" by blast
228     qed
229   qed
230   from preorder.preorder_equiv_axioms show "class.preorder_equiv less_eq_fun less_fun" .
231   show "preorder_equiv.equiv less_eq_fun = equiv_fun"
232   proof (rule ext, rule ext, unfold preorder.equiv_def)
233     fix f g
234     show "f \<lesssim> g \<and> g \<lesssim> f \<longleftrightarrow> f \<cong> g"
235     proof
236       assume "f \<cong> g"
237       then obtain n c\<^isub>1 c\<^isub>2 where "c\<^isub>1 > 0" and "c\<^isub>2 > 0"
238         and *: "\<And>m. m > n \<Longrightarrow> f m \<le> c\<^isub>1 * g m \<and> g m \<le> c\<^isub>2 * f m"
239         by rule blast
240       have "\<forall>m>n. f m \<le> c\<^isub>1 * g m"
241       proof (rule allI, rule impI)
242         fix m
243         assume "m > n"
244         with * show "f m \<le> c\<^isub>1 * g m" by simp
245       qed
246       with c\<^isub>1 > 0 have "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m" by blast
247       then have "f \<lesssim> g" ..
248       have "\<forall>m>n. g m \<le> c\<^isub>2 * f m"
249       proof (rule allI, rule impI)
250         fix m
251         assume "m > n"
252         with * show "g m \<le> c\<^isub>2 * f m" by simp
253       qed
254       with c\<^isub>2 > 0 have "\<exists>c>0. \<exists>n. \<forall>m>n. g m \<le> c * f m" by blast
255       then have "g \<lesssim> f" ..
256       from f \<lesssim> g and g \<lesssim> f show "f \<lesssim> g \<and> g \<lesssim> f" ..
257     next
258       assume "f \<lesssim> g \<and> g \<lesssim> f"
259       then have "f \<lesssim> g" and "g \<lesssim> f" by auto
260       from f \<lesssim> g obtain n\<^isub>1 c\<^isub>1 where "c\<^isub>1 > 0"
261         and P\<^isub>1: "\<And>m. m > n\<^isub>1 \<Longrightarrow> f m \<le> c\<^isub>1 * g m" by rule blast
262       from g \<lesssim> f obtain n\<^isub>2 c\<^isub>2 where "c\<^isub>2 > 0"
263         and P\<^isub>2: "\<And>m. m > n\<^isub>2 \<Longrightarrow> g m \<le> c\<^isub>2 * f m" by rule blast
264       have "\<forall>m>max n\<^isub>1 n\<^isub>2. f m \<le> c\<^isub>1 * g m \<and> g m \<le> c\<^isub>2 * f m"
265       proof (rule allI, rule impI)
266         fix m
267         assume Q: "m > max n\<^isub>1 n\<^isub>2"
268         from P\<^isub>1 Q have "f m \<le> c\<^isub>1 * g m" by simp
269         moreover from P\<^isub>2 Q have "g m \<le> c\<^isub>2 * f m" by simp
270         ultimately show "f m \<le> c\<^isub>1 * g m \<and> g m \<le> c\<^isub>2 * f m" ..
271       qed
272       with c\<^isub>1 > 0 c\<^isub>2 > 0 have "\<exists>c\<^isub>1>0. \<exists>c\<^isub>2>0. \<exists>n.
273         \<forall>m>n. f m \<le> c\<^isub>1 * g m \<and> g m \<le> c\<^isub>2 * f m" by blast
274       then show "f \<cong> g" ..
275     qed
276   qed
277 qed
280 subsection {* Simple examples *}
282 text {*
283   Most of these are left as constructive exercises for the reader.  Note that additional
284   preconditions to the functions may be necessary.  The list here is by no means to be
285   intended as complete contruction set for typical functions, here surely something
286   has to be added yet.
287 *}
289 text {* @{prop "(\<lambda>n. f n + k) \<cong> f"} *}
291 text {* @{prop "(\<lambda>n. Suc k * f n) \<cong> f"} *}
293 lemma "f \<lesssim> (\<lambda>n. f n + g n)"
294   by rule auto
296 lemma "(\<lambda>_. 0) \<prec> (\<lambda>n. Suc k)"
297   by (rule less_fun_strongI) auto
299 lemma "(\<lambda>_. k) \<prec> Discrete.log"
300 proof (rule less_fun_strongI)
301   fix c :: nat
302   have "\<forall>m>2 ^ (Suc (c * k)). c * k < Discrete.log m"
303   proof (rule allI, rule impI)
304     fix m :: nat
305     assume "2 ^ Suc (c * k) < m"
306     then have "2 ^ Suc (c * k) \<le> m" by simp
307     with log_mono have "Discrete.log (2 ^ (Suc (c * k))) \<le> Discrete.log m"
308       by (blast dest: monoD)
309     moreover have "c * k < Discrete.log (2 ^ (Suc (c * k)))" by simp
310     ultimately show "c * k < Discrete.log m" by auto
311   qed
312   then show "\<exists>n. \<forall>m>n. c * k < Discrete.log m" ..
313 qed
315 text {* @{prop "Discrete.log \<prec> Discrete.sqrt"} *}
317 lemma "Discrete.sqrt \<prec> id"
318 proof (rule less_fun_strongI)
319   fix c :: nat
320   assume "0 < c"
321   have "\<forall>m>(Suc c)\<twosuperior>. c * Discrete.sqrt m < id m"
322   proof (rule allI, rule impI)
323     fix m
324     assume "(Suc c)\<twosuperior> < m"
325     then have "(Suc c)\<twosuperior> \<le> m" by simp
326     with mono_sqrt have "Discrete.sqrt ((Suc c)\<twosuperior>) \<le> Discrete.sqrt m" by (rule monoE)
327     then have "Suc c \<le> Discrete.sqrt m" by simp
328     then have "c < Discrete.sqrt m" by simp
329     moreover from (Suc c)\<twosuperior> < m have "Discrete.sqrt m > 0" by simp
330     ultimately have "c * Discrete.sqrt m < Discrete.sqrt m * Discrete.sqrt m" by simp
331     also have "\<dots> \<le> m" by (simp add: power2_eq_square [symmetric])
332     finally show "c * Discrete.sqrt m < id m" by simp
333   qed
334   then show "\<exists>n. \<forall>m>n. c * Discrete.sqrt m < id m" ..
335 qed
337 lemma "id \<prec> (\<lambda>n. n\<twosuperior>)"
338   by (rule less_fun_strongI) (auto simp add: power2_eq_square)
340 lemma "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. n ^ Suc k)"
341   by (rule less_fun_strongI) auto
343 text {* @{prop "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. 2 ^ n)"} *}
345 end