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)
     1

     2 (* Author: Florian Haftmann, TU Muenchen *)

     3

     4 header {* Comparing growth of functions on natural numbers by a preorder relation *}

     5

     6 theory Function_Growth

     7 imports Main "~~/src/HOL/Library/Preorder" "~~/src/HOL/Library/Discrete"

     8 begin

     9

    10 subsection {* Motivation *}

    11

    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.

    16

    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 *}

    25

    26 subsection {* Model *}

    27

    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.

    33

    34   Note that we also restrict the additional coefficients to @{text \<nat>}, something

    35   we discuss at the particular definitions.

    36 *}

    37

    38 subsection {* The @{text "\<lesssim>"} relation *}

    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 {*

    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 *}

    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 {* The @{text "\<approx>"} relation, the equivalence relation induced by @{text "\<lesssim>"} *}

    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\<^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)"

    77

    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 *}

    82

    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)

    87

    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

    93

    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

    99

   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

   106

   107

   108 subsection {* The @{text "\<prec>"} relation, the strict part of @{text "\<lesssim>"} *}

   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 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

   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 {*

   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.

   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 *}

   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 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

   188

   189

   190 subsection {* @{text "\<lesssim>"} is a preorder *}

   191

   192 text {* This yields all lemmas relating @{text "\<lesssim>"}, @{text "\<prec>"} and @{text "\<cong>"}. *}

   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 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

   278

   279

   280 subsection {* Simple examples *}

   281

   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 *}

   288

   289 text {* @{prop "(\<lambda>n. f n + k) \<cong> f"} *}

   290

   291 text {* @{prop "(\<lambda>n. Suc k * f n) \<cong> f"} *}

   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 {* @{prop "Discrete.log \<prec> Discrete.sqrt"} *}

   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)\<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

   336

   337 lemma "id \<prec> (\<lambda>n. n\<twosuperior>)"

   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 {* @{prop "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. 2 ^ n)"} *}

   344

   345 end

   346