src/HOL/Library/Function_Growth.thy
author wenzelm
Wed Jun 17 11:03:05 2015 +0200 (2015-06-17)
changeset 60500 903bb1495239
parent 59113 3cded6b57a82
child 61566 c3d6e570ccef
permissions -rw-r--r--
isabelle update_cartouches;
     1 
     2 (* Author: Florian Haftmann, TU Muenchen *)
     3 
     4 section \<open>Comparing growth of functions on natural numbers by a preorder relation\<close>
     5 
     6 theory Function_Growth
     7 imports Main Preorder Discrete
     8 begin
     9 
    10 subsection \<open>Motivation\<close>
    11 
    12 text \<open>
    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.
    16   
    17   Here we suggest a different 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 hierarchy of functions:
    23   @{text "(\<lambda>n. 0) \<lesssim> (\<lambda>n. k) \<lesssim> Discrete.log \<lesssim> Discrete.sqrt \<lesssim> id \<lesssim> \<dots>"}.
    24 \<close>
    25 
    26 subsection \<open>Model\<close>
    27 
    28 text \<open>
    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.
    33 
    34   Note that we also restrict the additional coefficients to @{text \<nat>}, something
    35   we discuss at the particular definitions.
    36 \<close>
    37 
    38 subsection \<open>The @{text "\<lesssim>"} relation\<close>
    39 
    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)"
    43 
    44 text \<open>
    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 \<close>
    49 
    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)
    54 
    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
    59 
    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
    64 
    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
    69 
    70 
    71 subsection \<open>The @{text "\<approx>"} relation, the equivalence relation induced by @{text "\<lesssim>"}\<close>
    72 
    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\<^sub>1>0. \<exists>c\<^sub>2>0. \<exists>n. \<forall>m>n. f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m)"
    77 
    78 text \<open>
    79   This yields @{text "f \<cong> g \<longleftrightarrow> f \<in> \<Theta>(g)"}.  Concerning @{text "c\<^sub>1"} and @{text "c\<^sub>2"}
    80   restricted to @{typ nat}, see note above on @{text "(\<lesssim>)"}.
    81 \<close>
    82 
    83 lemma equiv_funI [intro?]:
    84   assumes "\<exists>c\<^sub>1>0. \<exists>c\<^sub>2>0. \<exists>n. \<forall>m>n. f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m"
    85   shows "f \<cong> g"
    86   unfolding equiv_fun_def by (rule assms)
    87 
    88 lemma not_equiv_funI:
    89   assumes "\<And>c\<^sub>1 c\<^sub>2 n. c\<^sub>1 > 0 \<Longrightarrow> c\<^sub>2 > 0 \<Longrightarrow>
    90     \<exists>m>n. c\<^sub>1 * f m < g m \<or> c\<^sub>2 * g m < f m"
    91   shows "\<not> f \<cong> g"
    92   using assms unfolding equiv_fun_def linorder_not_le [symmetric] by blast
    93 
    94 lemma equiv_funE [elim?]:
    95   assumes "f \<cong> g"
    96   obtains n c\<^sub>1 c\<^sub>2 where "c\<^sub>1 > 0" and "c\<^sub>2 > 0"
    97     and "\<And>m. m > n \<Longrightarrow> f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m"
    98   using assms unfolding equiv_fun_def by blast
    99 
   100 lemma not_equiv_funE:
   101   fixes n c\<^sub>1 c\<^sub>2
   102   assumes "\<not> f \<cong> g" and "c\<^sub>1 > 0" and "c\<^sub>2 > 0"
   103   obtains m where "m > n"
   104     and "c\<^sub>1 * f m < g m \<or> c\<^sub>2 * g m < f m"
   105   using assms unfolding equiv_fun_def linorder_not_le [symmetric] by blast
   106 
   107 
   108 subsection \<open>The @{text "\<prec>"} relation, the strict part of @{text "\<lesssim>"}\<close>
   109 
   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"
   113 
   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
   119 
   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
   125 
   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 \<open>f \<lesssim> g\<close> 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 \<open>\<not> g \<lesssim> f\<close> 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
   142 
   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
   148 
   149 text \<open>
   150   I did not find 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.
   154 
   155   Note that D. Knuth ignores @{text o} altogether.  So what \dots
   156 
   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 \<close>
   165 
   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 \<open>1 > 0\<close> 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 \<open>1 > 0\<close> 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
   188 
   189 
   190 subsection \<open>@{text "\<lesssim>"} is a preorder\<close>
   191 
   192 text \<open>This yields all lemmas relating @{text "\<lesssim>"}, @{text "\<prec>"} and @{text "\<cong>"}.\<close>
   193 
   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 \<open>f \<lesssim> g\<close> obtain n\<^sub>1 c\<^sub>1
   211         where "c\<^sub>1 > 0" and P\<^sub>1: "\<And>m. m > n\<^sub>1 \<Longrightarrow> f m \<le> c\<^sub>1 * g m"
   212         by rule blast
   213       from \<open>g \<lesssim> h\<close> obtain n\<^sub>2 c\<^sub>2
   214         where "c\<^sub>2 > 0" and P\<^sub>2: "\<And>m. m > n\<^sub>2 \<Longrightarrow> g m \<le> c\<^sub>2 * h m"
   215         by rule blast
   216       have "\<forall>m>max n\<^sub>1 n\<^sub>2. f m \<le> (c\<^sub>1 * c\<^sub>2) * h m"
   217       proof (rule allI, rule impI)
   218         fix m
   219         assume Q: "m > max n\<^sub>1 n\<^sub>2"
   220         from P\<^sub>1 Q have *: "f m \<le> c\<^sub>1 * g m" by simp
   221         from P\<^sub>2 Q have "g m \<le> c\<^sub>2 * h m" by simp
   222         with \<open>c\<^sub>1 > 0\<close> have "c\<^sub>1 * g m \<le> (c\<^sub>1 * c\<^sub>2) * h m" by simp
   223         with * show "f m \<le> (c\<^sub>1 * c\<^sub>2) * h m" by (rule order_trans)
   224       qed
   225       then have "\<exists>n. \<forall>m>n. f m \<le> (c\<^sub>1 * c\<^sub>2) * h m" by rule
   226       moreover from \<open>c\<^sub>1 > 0\<close> \<open>c\<^sub>2 > 0\<close> have "c\<^sub>1 * c\<^sub>2 > 0" by simp
   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\<^sub>1 c\<^sub>2 where "c\<^sub>1 > 0" and "c\<^sub>2 > 0"
   238         and *: "\<And>m. m > n \<Longrightarrow> f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m"
   239         by rule blast
   240       have "\<forall>m>n. f m \<le> c\<^sub>1 * g m"
   241       proof (rule allI, rule impI)
   242         fix m
   243         assume "m > n"
   244         with * show "f m \<le> c\<^sub>1 * g m" by simp
   245       qed
   246       with \<open>c\<^sub>1 > 0\<close> 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\<^sub>2 * f m"
   249       proof (rule allI, rule impI)
   250         fix m
   251         assume "m > n"
   252         with * show "g m \<le> c\<^sub>2 * f m" by simp
   253       qed
   254       with \<open>c\<^sub>2 > 0\<close> 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 \<open>f \<lesssim> g\<close> and \<open>g \<lesssim> f\<close> 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 \<open>f \<lesssim> g\<close> obtain n\<^sub>1 c\<^sub>1 where "c\<^sub>1 > 0"
   261         and P\<^sub>1: "\<And>m. m > n\<^sub>1 \<Longrightarrow> f m \<le> c\<^sub>1 * g m" by rule blast
   262       from \<open>g \<lesssim> f\<close> obtain n\<^sub>2 c\<^sub>2 where "c\<^sub>2 > 0"
   263         and P\<^sub>2: "\<And>m. m > n\<^sub>2 \<Longrightarrow> g m \<le> c\<^sub>2 * f m" by rule blast
   264       have "\<forall>m>max n\<^sub>1 n\<^sub>2. f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m"
   265       proof (rule allI, rule impI)
   266         fix m
   267         assume Q: "m > max n\<^sub>1 n\<^sub>2"
   268         from P\<^sub>1 Q have "f m \<le> c\<^sub>1 * g m" by simp
   269         moreover from P\<^sub>2 Q have "g m \<le> c\<^sub>2 * f m" by simp
   270         ultimately show "f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m" ..
   271       qed
   272       with \<open>c\<^sub>1 > 0\<close> \<open>c\<^sub>2 > 0\<close> have "\<exists>c\<^sub>1>0. \<exists>c\<^sub>2>0. \<exists>n.
   273         \<forall>m>n. f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m" by blast
   274       then show "f \<cong> g" ..
   275     qed
   276   qed
   277 qed
   278 
   279 
   280 subsection \<open>Simple examples\<close>
   281 
   282 text \<open>
   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 construction set for typical functions, here surely something
   286   has to be added yet.
   287 \<close>
   288 
   289 text \<open>@{prop "(\<lambda>n. f n + k) \<cong> f"}\<close>
   290 
   291 text \<open>@{prop "(\<lambda>n. Suc k * f n) \<cong> f"}\<close>
   292 
   293 lemma "f \<lesssim> (\<lambda>n. f n + g n)"
   294   by rule auto
   295 
   296 lemma "(\<lambda>_. 0) \<prec> (\<lambda>n. Suc k)"
   297   by (rule less_fun_strongI) auto
   298 
   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
   314   
   315 text \<open>@{prop "Discrete.log \<prec> Discrete.sqrt"}\<close>
   316 
   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)\<^sup>2. c * Discrete.sqrt m < id m"
   322   proof (rule allI, rule impI)
   323     fix m
   324     assume "(Suc c)\<^sup>2 < m"
   325     then have "(Suc c)\<^sup>2 \<le> m" by simp
   326     with mono_sqrt have "Discrete.sqrt ((Suc c)\<^sup>2) \<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 \<open>(Suc c)\<^sup>2 < m\<close> 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
   336 
   337 lemma "id \<prec> (\<lambda>n. n\<^sup>2)"
   338   by (rule less_fun_strongI) (auto simp add: power2_eq_square)
   339 
   340 lemma "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. n ^ Suc k)"
   341   by (rule less_fun_strongI) auto
   342 
   343 text \<open>@{prop "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. 2 ^ n)"}\<close>
   344 
   345 end
   346