added Landau theory
authorhaftmann
Tue Jun 02 18:26:01 2009 +0200 (2009-06-02)
changeset 31381b3a785a69538
parent 31380 f25536c0bb80
child 31382 5c563b968832
added Landau theory
src/HOL/ex/Landau.thy
src/HOL/ex/ROOT.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/ex/Landau.thy	Tue Jun 02 18:26:01 2009 +0200
     1.3 @@ -0,0 +1,226 @@
     1.4 +
     1.5 +(* Author: Florian Haftmann, TU Muenchen *)
     1.6 +
     1.7 +header {* Comparing growth of functions on natural numbers by a preorder relation *}
     1.8 +
     1.9 +theory Landau
    1.10 +imports Main Preorder
    1.11 +begin
    1.12 +
    1.13 +text {*
    1.14 +  We establish a preorder releation @{text "\<lesssim>"} on functions
    1.15 +  from @{text "\<nat>"} to @{text "\<nat>"} such that @{text "f \<lesssim> g \<longleftrightarrow> f \<in> O(g)"}.
    1.16 +*}
    1.17 +
    1.18 +subsection {* Auxiliary *}
    1.19 +
    1.20 +lemma Ex_All_bounded:
    1.21 +  fixes n :: nat
    1.22 +  assumes "\<exists>n. \<forall>m\<ge>n. P m"
    1.23 +  obtains m where "m \<ge> n" and "P m"
    1.24 +proof -
    1.25 +  from assms obtain q where m_q: "\<forall>m\<ge>q. P m" ..
    1.26 +  let ?m = "max q n"
    1.27 +  have "?m \<ge> n" by auto
    1.28 +  moreover from m_q have "P ?m" by auto
    1.29 +  ultimately show thesis ..
    1.30 +qed
    1.31 +    
    1.32 +
    1.33 +subsection {* The @{text "\<lesssim>"} relation *}
    1.34 +
    1.35 +definition less_eq_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<lesssim>" 50) where
    1.36 +  "f \<lesssim> g \<longleftrightarrow> (\<exists>c n. \<forall>m\<ge>n. f m \<le> Suc c * g m)"
    1.37 +
    1.38 +lemma less_eq_fun_intro:
    1.39 +  assumes "\<exists>c n. \<forall>m\<ge>n. f m \<le> Suc c * g m"
    1.40 +  shows "f \<lesssim> g"
    1.41 +  unfolding less_eq_fun_def by (rule assms)
    1.42 +
    1.43 +lemma less_eq_fun_not_intro:
    1.44 +  assumes "\<And>c n. \<exists>m\<ge>n. Suc c * g m < f m"
    1.45 +  shows "\<not> f \<lesssim> g"
    1.46 +  using assms unfolding less_eq_fun_def linorder_not_le [symmetric]
    1.47 +  by blast
    1.48 +
    1.49 +lemma less_eq_fun_elim:
    1.50 +  assumes "f \<lesssim> g"
    1.51 +  obtains n c where "\<And>m. m \<ge> n \<Longrightarrow> f m \<le> Suc c * g m"
    1.52 +  using assms unfolding less_eq_fun_def by blast
    1.53 +
    1.54 +lemma less_eq_fun_not_elim:
    1.55 +  assumes "\<not> f \<lesssim> g"
    1.56 +  obtains m where "m \<ge> n" and "Suc c * g m < f m"
    1.57 +  using assms unfolding less_eq_fun_def linorder_not_le [symmetric]
    1.58 +  by blast
    1.59 +
    1.60 +lemma less_eq_fun_refl:
    1.61 +  "f \<lesssim> f"
    1.62 +proof (rule less_eq_fun_intro)
    1.63 +  have "\<exists>n. \<forall>m\<ge>n. f m \<le> Suc 0 * f m" by auto
    1.64 +  then show "\<exists>c n. \<forall>m\<ge>n. f m \<le> Suc c * f m" by blast
    1.65 +qed
    1.66 +
    1.67 +lemma less_eq_fun_trans:
    1.68 +  assumes f_g: "f \<lesssim> g" and g_h: "g \<lesssim> h"
    1.69 +  shows f_h: "f \<lesssim> h"
    1.70 +proof -
    1.71 +  from f_g obtain n\<^isub>1 c\<^isub>1
    1.72 +    where P1: "\<And>m. m \<ge> n\<^isub>1 \<Longrightarrow> f m \<le> Suc c\<^isub>1 * g m"
    1.73 +  by (erule less_eq_fun_elim)
    1.74 +  moreover from g_h obtain n\<^isub>2 c\<^isub>2
    1.75 +    where P2: "\<And>m. m \<ge> n\<^isub>2 \<Longrightarrow> g m \<le> Suc c\<^isub>2 * h m"
    1.76 +  by (erule less_eq_fun_elim)
    1.77 +  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"
    1.78 +  by auto
    1.79 +  moreover {
    1.80 +    fix k l r :: nat
    1.81 +    assume k_l: "k \<le> Suc c\<^isub>1 * l" and l_r: "l \<le> Suc c\<^isub>2 * r"
    1.82 +    from l_r have "Suc c\<^isub>1 * l \<le> (Suc c\<^isub>1 * Suc c\<^isub>2) * r"
    1.83 +    by (auto simp add: mult_le_cancel_left mult_assoc simp del: times_nat.simps mult_Suc_right)
    1.84 +    with k_l have "k \<le> (Suc c\<^isub>1 * Suc c\<^isub>2) * r" by (rule preorder_class.order_trans)
    1.85 +  }
    1.86 +  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
    1.87 +  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
    1.88 +  then show ?thesis unfolding less_eq_fun_def by blast
    1.89 +qed
    1.90 +
    1.91 +
    1.92 +subsection {* The @{text "\<approx>"} relation, the equivalence relation induced by @{text "\<lesssim>"} *}
    1.93 +
    1.94 +definition equiv_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<cong>" 50) where
    1.95 +  "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)"
    1.96 +
    1.97 +lemma equiv_fun_intro:
    1.98 +  assumes "\<exists>d c n. \<forall>m\<ge>n. g m \<le> Suc d * f m \<and> f m \<le> Suc c * g m"
    1.99 +  shows "f \<cong> g"
   1.100 +  unfolding equiv_fun_def by (rule assms)
   1.101 +
   1.102 +lemma equiv_fun_not_intro:
   1.103 +  assumes "\<And>d c n. \<exists>m\<ge>n. Suc d * f m < g m \<or> Suc c * g m < f m"
   1.104 +  shows "\<not> f \<cong> g"
   1.105 +  unfolding equiv_fun_def
   1.106 +  by (auto simp add: assms linorder_not_le
   1.107 +    simp del: times_nat.simps mult_Suc_right)
   1.108 +
   1.109 +lemma equiv_fun_elim:
   1.110 +  assumes "f \<cong> g"
   1.111 +  obtains n d c
   1.112 +    where "\<And>m. m \<ge> n \<Longrightarrow> g m \<le> Suc d * f m \<and> f m \<le> Suc c * g m"
   1.113 +  using assms unfolding equiv_fun_def by blast
   1.114 +
   1.115 +lemma equiv_fun_not_elim:
   1.116 +  fixes n d c
   1.117 +  assumes "\<not> f \<cong> g"
   1.118 +  obtains m where "m \<ge> n"
   1.119 +    and "Suc d * f m < g m \<or> Suc c * g m < f m"
   1.120 +  using assms unfolding equiv_fun_def
   1.121 +  by (auto simp add: linorder_not_le, blast)
   1.122 +
   1.123 +lemma equiv_fun_less_eq_fun:
   1.124 +  "f \<cong> g \<longleftrightarrow> f \<lesssim> g \<and> g \<lesssim> f"
   1.125 +proof
   1.126 +  assume x_y: "f \<cong> g"
   1.127 +  then obtain n d c
   1.128 +    where interv: "\<And>m. m \<ge> n \<Longrightarrow> g m \<le> Suc d * f m \<and> f m \<le> Suc c * g m"
   1.129 +  by (erule equiv_fun_elim)
   1.130 +  from interv have "\<exists>c n. \<forall>m \<ge> n. f m \<le> Suc c * g m" by auto
   1.131 +  then have f_g: "f \<lesssim> g" by (rule less_eq_fun_intro)
   1.132 +  from interv have "\<exists>d n. \<forall>m \<ge> n. g m \<le> Suc d * f m" by auto
   1.133 +  then have g_f: "g \<lesssim> f" by (rule less_eq_fun_intro)
   1.134 +  from f_g g_f show "f \<lesssim> g \<and> g \<lesssim> f" by auto
   1.135 +next
   1.136 +  assume assm: "f \<lesssim> g \<and> g \<lesssim> f"
   1.137 +  from assm less_eq_fun_elim obtain c n\<^isub>1 where
   1.138 +    bound1: "\<And>m. m \<ge> n\<^isub>1 \<Longrightarrow> f m \<le> Suc c * g m" 
   1.139 +    by blast
   1.140 +  from assm less_eq_fun_elim obtain d n\<^isub>2 where
   1.141 +    bound2: "\<And>m. m \<ge> n\<^isub>2 \<Longrightarrow> g m \<le> Suc d * f m"
   1.142 +    by blast
   1.143 +  from bound2 have "\<And>m. m \<ge> max n\<^isub>1 n\<^isub>2 \<Longrightarrow> g m \<le> Suc d * f m"
   1.144 +  by auto
   1.145 +  with bound1
   1.146 +    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"
   1.147 +    by auto
   1.148 +  then
   1.149 +    have "\<exists>d c n. \<forall>m\<ge>n. g m \<le> Suc d * f m \<and> f m \<le> Suc c * g m"
   1.150 +    by blast
   1.151 +  then show "f \<cong> g" by (rule equiv_fun_intro)
   1.152 +qed
   1.153 +
   1.154 +subsection {* The @{text "\<prec>"} relation, the strict part of @{text "\<lesssim>"} *}
   1.155 +
   1.156 +definition less_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<prec>" 50) where
   1.157 +  "f \<prec> g \<longleftrightarrow> f \<lesssim> g \<and> \<not> g \<lesssim> f"
   1.158 +
   1.159 +lemma less_fun_intro:
   1.160 +  assumes "\<And>c. \<exists>n. \<forall>m\<ge>n. Suc c * f m < g m"
   1.161 +  shows "f \<prec> g"
   1.162 +proof (unfold less_fun_def, rule conjI)
   1.163 +  from assms obtain n
   1.164 +    where "\<forall>m\<ge>n. Suc 0 * f m < g m" ..
   1.165 +  then have "\<forall>m\<ge>n. f m \<le> Suc 0 * g m" by auto
   1.166 +  then have "\<exists>c n. \<forall>m\<ge>n. f m \<le> Suc c * g m" by blast
   1.167 +  then show "f \<lesssim> g" by (rule less_eq_fun_intro)
   1.168 +next
   1.169 +  show "\<not> g \<lesssim> f"
   1.170 +  proof (rule less_eq_fun_not_intro)
   1.171 +    fix c n :: nat
   1.172 +    from assms have "\<exists>n. \<forall>m\<ge>n. Suc c * f m < g m" by blast
   1.173 +    then obtain m where "m \<ge> n" and "Suc c * f m < g m"
   1.174 +      by (rule Ex_All_bounded)
   1.175 +    then show "\<exists>m\<ge>n. Suc c * f m < g m" by blast
   1.176 +  qed
   1.177 +qed
   1.178 +
   1.179 +text {*
   1.180 +  We would like to show (or refute) that @{text "f \<prec> g \<longleftrightarrow> f \<in> o(g)"},
   1.181 +  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
   1.182 +  do so.
   1.183 +*}
   1.184 +
   1.185 +
   1.186 +subsection {* Assert that @{text "\<lesssim>"} is ineed a preorder *}
   1.187 +
   1.188 +interpretation fun_order: preorder_equiv less_eq_fun less_fun
   1.189 +  where "preorder_equiv.equiv less_eq_fun = equiv_fun"
   1.190 +proof -
   1.191 +  interpret preorder_equiv less_eq_fun less_fun proof
   1.192 +  qed (simp_all add: less_fun_def less_eq_fun_refl, auto intro: less_eq_fun_trans)
   1.193 +  show "preorder_equiv less_eq_fun less_fun" using preorder_equiv_axioms .
   1.194 +  show "preorder_equiv.equiv less_eq_fun = equiv_fun"
   1.195 +    by (simp add: expand_fun_eq equiv_def equiv_fun_less_eq_fun)
   1.196 +qed
   1.197 +
   1.198 +
   1.199 +subsection {* Simple examples *}
   1.200 +
   1.201 +lemma "(\<lambda>_. n) \<lesssim> (\<lambda>n. n)"
   1.202 +proof (rule less_eq_fun_intro)
   1.203 +  show "\<exists>c q. \<forall>m\<ge>q. n \<le> Suc c * m"
   1.204 +  proof -
   1.205 +    have "\<forall>m\<ge>n. n \<le> Suc 0 * m" by simp
   1.206 +    then show ?thesis by blast
   1.207 +  qed
   1.208 +qed
   1.209 +
   1.210 +lemma "(\<lambda>n. n) \<cong> (\<lambda>n. Suc k * n)"
   1.211 +proof (rule equiv_fun_intro)
   1.212 +  show "\<exists>d c n. \<forall>m\<ge>n. Suc k * m \<le> Suc d * m \<and> m \<le> Suc c * (Suc k * m)"
   1.213 +  proof -
   1.214 +    have "\<forall>m\<ge>n. Suc k * m \<le> Suc k * m \<and> m \<le> Suc c * (Suc k * m)" by simp
   1.215 +    then show ?thesis by blast
   1.216 +  qed
   1.217 +qed  
   1.218 +
   1.219 +lemma "(\<lambda>_. n) \<prec> (\<lambda>n. n)"
   1.220 +proof (rule less_fun_intro)
   1.221 +  fix c
   1.222 +  show "\<exists>q. \<forall>m\<ge>q. Suc c * n < m"
   1.223 +  proof -
   1.224 +    have "\<forall>m\<ge>Suc c * n + 1. Suc c * n < m" by simp
   1.225 +    then show ?thesis by blast
   1.226 +  qed
   1.227 +qed
   1.228 +
   1.229 +end
     2.1 --- a/src/HOL/ex/ROOT.ML	Tue Jun 02 16:23:43 2009 +0200
     2.2 +++ b/src/HOL/ex/ROOT.ML	Tue Jun 02 18:26:01 2009 +0200
     2.3 @@ -6,7 +6,6 @@
     2.4  no_document use_thys [
     2.5    "State_Monad",
     2.6    "Efficient_Nat_examples",
     2.7 -  "ExecutableContent",
     2.8    "FuncSet",
     2.9    "Word",
    2.10    "Eval_Examples",
    2.11 @@ -67,7 +66,8 @@
    2.12    "HarmonicSeries",
    2.13    "Refute_Examples",
    2.14    "Quickcheck_Examples",
    2.15 -  "Formal_Power_Series_Examples"
    2.16 +  "Formal_Power_Series_Examples",
    2.17 +  "Landau"
    2.18  ];
    2.19  
    2.20  setmp Proofterm.proofs 2 use_thy "Hilbert_Classical";