src/HOL/ex/Landau.thy
author wenzelm
Wed Dec 29 17:34:41 2010 +0100 (2010-12-29)
changeset 41413 64cd30d6b0b8
parent 39302 d7728f65b353
permissions -rw-r--r--
explicit file specifications -- avoid secondary load path;
     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 "~~/src/HOL/Library/Preorder"
     8 begin
     9 
    10 text {*
    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)"}.
    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
   179   manage to do so.
   180 *}
   181 
   182 
   183 subsection {* Assert that @{text "\<lesssim>"} is indeed 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)
   190   show "class.preorder_equiv less_eq_fun less_fun" using preorder_equiv_axioms .
   191   show "preorder_equiv.equiv less_eq_fun = equiv_fun"
   192     by (simp add: fun_eq_iff 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