author | blanchet |
Wed, 15 Dec 2010 11:26:28 +0100 | |
changeset 41140 | 9c68004b8c9d |
parent 39302 | d7728f65b353 |
child 41413 | 64cd30d6b0b8 |
permissions | -rw-r--r-- |
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 {* |
|
36809 | 11 |
We establish a preorder releation @{text "\<lesssim>"} on functions from |
12 |
@{text "\<nat>"} to @{text "\<nat>"} such that @{text "f \<lesssim> g \<longleftrightarrow> f \<in> O(g)"}. |
|
31381 | 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)"}, |
|
36809 | 178 |
i.e.~@{prop "f \<prec> g \<longleftrightarrow> (\<forall>c. \<exists>n. \<forall>m>n. f m < Suc c * g m)"} but did not |
179 |
manage to do so. |
|
31381 | 180 |
*} |
181 |
||
182 |
||
36809 | 183 |
subsection {* Assert that @{text "\<lesssim>"} is indeed a preorder *} |
31381 | 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" |
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
39198
diff
changeset
|
192 |
by (simp add: fun_eq_iff equiv_def equiv_fun_less_eq_fun) |
31381 | 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 |