src/HOL/Library/Function_Growth.thy
changeset 60500 903bb1495239
parent 59113 3cded6b57a82
child 61566 c3d6e570ccef
     1.1 --- a/src/HOL/Library/Function_Growth.thy	Wed Jun 17 10:57:11 2015 +0200
     1.2 +++ b/src/HOL/Library/Function_Growth.thy	Wed Jun 17 11:03:05 2015 +0200
     1.3 @@ -1,15 +1,15 @@
     1.4  
     1.5  (* Author: Florian Haftmann, TU Muenchen *)
     1.6  
     1.7 -section {* Comparing growth of functions on natural numbers by a preorder relation *}
     1.8 +section \<open>Comparing growth of functions on natural numbers by a preorder relation\<close>
     1.9  
    1.10  theory Function_Growth
    1.11  imports Main Preorder Discrete
    1.12  begin
    1.13  
    1.14 -subsection {* Motivation *}
    1.15 +subsection \<open>Motivation\<close>
    1.16  
    1.17 -text {*
    1.18 +text \<open>
    1.19    When comparing growth of functions in computer science, it is common to adhere
    1.20    on Landau Symbols (``O-Notation'').  However these come at the cost of notational
    1.21    oddities, particularly writing @{text "f = O(g)"} for @{text "f \<in> O(g)"} etc.
    1.22 @@ -21,11 +21,11 @@
    1.23    avoid the notational oddities mentioned above but also emphasizes the key insight
    1.24    of a growth hierarchy of functions:
    1.25    @{text "(\<lambda>n. 0) \<lesssim> (\<lambda>n. k) \<lesssim> Discrete.log \<lesssim> Discrete.sqrt \<lesssim> id \<lesssim> \<dots>"}.
    1.26 -*}
    1.27 +\<close>
    1.28  
    1.29 -subsection {* Model *}
    1.30 +subsection \<open>Model\<close>
    1.31  
    1.32 -text {*
    1.33 +text \<open>
    1.34    Our growth functions are of type @{text "\<nat> \<Rightarrow> \<nat>"}.  This is different
    1.35    to the usual conventions for Landau symbols for which @{text "\<real> \<Rightarrow> \<real>"}
    1.36    would be appropriate, but we argue that @{text "\<real> \<Rightarrow> \<real>"} is more
    1.37 @@ -33,19 +33,19 @@
    1.38  
    1.39    Note that we also restrict the additional coefficients to @{text \<nat>}, something
    1.40    we discuss at the particular definitions.
    1.41 -*}
    1.42 +\<close>
    1.43  
    1.44 -subsection {* The @{text "\<lesssim>"} relation *}
    1.45 +subsection \<open>The @{text "\<lesssim>"} relation\<close>
    1.46  
    1.47  definition less_eq_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<lesssim>" 50)
    1.48  where
    1.49    "f \<lesssim> g \<longleftrightarrow> (\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m)"
    1.50  
    1.51 -text {*
    1.52 +text \<open>
    1.53    This yields @{text "f \<lesssim> g \<longleftrightarrow> f \<in> O(g)"}.  Note that @{text c} is restricted to
    1.54    @{text \<nat>}.  This does not pose any problems since if @{text "f \<in> O(g)"} holds for
    1.55    a @{text "c \<in> \<real>"}, it also holds for @{text "\<lceil>c\<rceil> \<in> \<nat>"} by transitivity.
    1.56 -*}
    1.57 +\<close>
    1.58  
    1.59  lemma less_eq_funI [intro?]:
    1.60    assumes "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m"
    1.61 @@ -68,17 +68,17 @@
    1.62    using assms unfolding less_eq_fun_def linorder_not_le [symmetric] by blast
    1.63  
    1.64  
    1.65 -subsection {* The @{text "\<approx>"} relation, the equivalence relation induced by @{text "\<lesssim>"} *}
    1.66 +subsection \<open>The @{text "\<approx>"} relation, the equivalence relation induced by @{text "\<lesssim>"}\<close>
    1.67  
    1.68  definition equiv_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<cong>" 50)
    1.69  where
    1.70    "f \<cong> g \<longleftrightarrow>
    1.71      (\<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)"
    1.72  
    1.73 -text {*
    1.74 +text \<open>
    1.75    This yields @{text "f \<cong> g \<longleftrightarrow> f \<in> \<Theta>(g)"}.  Concerning @{text "c\<^sub>1"} and @{text "c\<^sub>2"}
    1.76    restricted to @{typ nat}, see note above on @{text "(\<lesssim>)"}.
    1.77 -*}
    1.78 +\<close>
    1.79  
    1.80  lemma equiv_funI [intro?]:
    1.81    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"
    1.82 @@ -105,7 +105,7 @@
    1.83    using assms unfolding equiv_fun_def linorder_not_le [symmetric] by blast
    1.84  
    1.85  
    1.86 -subsection {* The @{text "\<prec>"} relation, the strict part of @{text "\<lesssim>"} *}
    1.87 +subsection \<open>The @{text "\<prec>"} relation, the strict part of @{text "\<lesssim>"}\<close>
    1.88  
    1.89  definition less_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<prec>" 50)
    1.90  where
    1.91 @@ -129,11 +129,11 @@
    1.92      and "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * f m < g m"
    1.93  proof -
    1.94    from assms have "f \<lesssim> g" and "\<not> g \<lesssim> f" by (simp_all add: less_fun_def)
    1.95 -  from `f \<lesssim> g` obtain n c where *:"c > 0" "\<And>m. m > n \<Longrightarrow> f m \<le> c * g m"
    1.96 +  from \<open>f \<lesssim> g\<close> obtain n c where *:"c > 0" "\<And>m. m > n \<Longrightarrow> f m \<le> c * g m"
    1.97      by (rule less_eq_funE) blast
    1.98    { fix c n :: nat
    1.99      assume "c > 0"
   1.100 -    with `\<not> g \<lesssim> f` obtain m where "m > n" "c * f m < g m"
   1.101 +    with \<open>\<not> g \<lesssim> f\<close> obtain m where "m > n" "c * f m < g m"
   1.102        by (rule not_less_eq_funE) blast
   1.103      then have **: "\<exists>m>n. c * f m < g m" by blast
   1.104    } note ** = this
   1.105 @@ -146,7 +146,7 @@
   1.106      | d q where "\<And>m. d > 0 \<Longrightarrow> m > q \<Longrightarrow> g q \<le> d * f q"
   1.107    using assms unfolding less_fun_def linorder_not_less [symmetric] by blast
   1.108  
   1.109 -text {*
   1.110 +text \<open>
   1.111    I did not find a proof for @{text "f \<prec> g \<longleftrightarrow> f \<in> o(g)"}.  Maybe this only
   1.112    holds if @{text f} and/or @{text g} are of a certain class of functions.
   1.113    However @{text "f \<in> o(g) \<longrightarrow> f \<prec> g"} is provable, and this yields a
   1.114 @@ -161,14 +161,14 @@
   1.115    works since @{text c} may become arbitrary small.  Since this is not possible
   1.116    within @{term \<nat>}, we push the coefficient to the left hand side instead such
   1.117    that it become arbitrary big instead.
   1.118 -*}
   1.119 +\<close>
   1.120  
   1.121  lemma less_fun_strongI:
   1.122    assumes "\<And>c. c > 0 \<Longrightarrow> \<exists>n. \<forall>m>n. c * f m < g m"
   1.123    shows "f \<prec> g"
   1.124  proof (rule less_funI)
   1.125    have "1 > (0::nat)" by simp
   1.126 -  from assms `1 > 0` have "\<exists>n. \<forall>m>n. 1 * f m < g m" .
   1.127 +  from assms \<open>1 > 0\<close> have "\<exists>n. \<forall>m>n. 1 * f m < g m" .
   1.128    then obtain n where *: "\<And>m. m > n \<Longrightarrow> 1 * f m < g m" by blast
   1.129    have "\<forall>m>n. f m \<le> 1 * g m"
   1.130    proof (rule allI, rule impI)
   1.131 @@ -177,7 +177,7 @@
   1.132      with * have "1 * f m < g m" by simp
   1.133      then show "f m \<le> 1 * g m" by simp
   1.134    qed
   1.135 -  with `1 > 0` show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m" by blast
   1.136 +  with \<open>1 > 0\<close> show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m" by blast
   1.137    fix c n :: nat
   1.138    assume "c > 0"
   1.139    with assms obtain q where "\<And>m. m > q \<Longrightarrow> c * f m < g m" by blast
   1.140 @@ -187,9 +187,9 @@
   1.141  qed
   1.142  
   1.143  
   1.144 -subsection {* @{text "\<lesssim>"} is a preorder *}
   1.145 +subsection \<open>@{text "\<lesssim>"} is a preorder\<close>
   1.146  
   1.147 -text {* This yields all lemmas relating @{text "\<lesssim>"}, @{text "\<prec>"} and @{text "\<cong>"}. *}
   1.148 +text \<open>This yields all lemmas relating @{text "\<lesssim>"}, @{text "\<prec>"} and @{text "\<cong>"}.\<close>
   1.149  
   1.150  interpretation fun_order: preorder_equiv less_eq_fun less_fun
   1.151    where "preorder_equiv.equiv less_eq_fun = equiv_fun"
   1.152 @@ -207,10 +207,10 @@
   1.153      assume "f \<lesssim> g" and "g \<lesssim> h"
   1.154      show "f \<lesssim> h"
   1.155      proof
   1.156 -      from `f \<lesssim> g` obtain n\<^sub>1 c\<^sub>1
   1.157 +      from \<open>f \<lesssim> g\<close> obtain n\<^sub>1 c\<^sub>1
   1.158          where "c\<^sub>1 > 0" and P\<^sub>1: "\<And>m. m > n\<^sub>1 \<Longrightarrow> f m \<le> c\<^sub>1 * g m"
   1.159          by rule blast
   1.160 -      from `g \<lesssim> h` obtain n\<^sub>2 c\<^sub>2
   1.161 +      from \<open>g \<lesssim> h\<close> obtain n\<^sub>2 c\<^sub>2
   1.162          where "c\<^sub>2 > 0" and P\<^sub>2: "\<And>m. m > n\<^sub>2 \<Longrightarrow> g m \<le> c\<^sub>2 * h m"
   1.163          by rule blast
   1.164        have "\<forall>m>max n\<^sub>1 n\<^sub>2. f m \<le> (c\<^sub>1 * c\<^sub>2) * h m"
   1.165 @@ -219,11 +219,11 @@
   1.166          assume Q: "m > max n\<^sub>1 n\<^sub>2"
   1.167          from P\<^sub>1 Q have *: "f m \<le> c\<^sub>1 * g m" by simp
   1.168          from P\<^sub>2 Q have "g m \<le> c\<^sub>2 * h m" by simp
   1.169 -        with `c\<^sub>1 > 0` have "c\<^sub>1 * g m \<le> (c\<^sub>1 * c\<^sub>2) * h m" by simp
   1.170 +        with \<open>c\<^sub>1 > 0\<close> have "c\<^sub>1 * g m \<le> (c\<^sub>1 * c\<^sub>2) * h m" by simp
   1.171          with * show "f m \<le> (c\<^sub>1 * c\<^sub>2) * h m" by (rule order_trans)
   1.172        qed
   1.173        then have "\<exists>n. \<forall>m>n. f m \<le> (c\<^sub>1 * c\<^sub>2) * h m" by rule
   1.174 -      moreover from `c\<^sub>1 > 0` `c\<^sub>2 > 0` have "c\<^sub>1 * c\<^sub>2 > 0" by simp
   1.175 +      moreover from \<open>c\<^sub>1 > 0\<close> \<open>c\<^sub>2 > 0\<close> have "c\<^sub>1 * c\<^sub>2 > 0" by simp
   1.176        ultimately show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * h m" by blast
   1.177      qed
   1.178    qed
   1.179 @@ -243,7 +243,7 @@
   1.180          assume "m > n"
   1.181          with * show "f m \<le> c\<^sub>1 * g m" by simp
   1.182        qed
   1.183 -      with `c\<^sub>1 > 0` have "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m" by blast
   1.184 +      with \<open>c\<^sub>1 > 0\<close> have "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m" by blast
   1.185        then have "f \<lesssim> g" ..
   1.186        have "\<forall>m>n. g m \<le> c\<^sub>2 * f m"
   1.187        proof (rule allI, rule impI)
   1.188 @@ -251,15 +251,15 @@
   1.189          assume "m > n"
   1.190          with * show "g m \<le> c\<^sub>2 * f m" by simp
   1.191        qed
   1.192 -      with `c\<^sub>2 > 0` have "\<exists>c>0. \<exists>n. \<forall>m>n. g m \<le> c * f m" by blast
   1.193 +      with \<open>c\<^sub>2 > 0\<close> have "\<exists>c>0. \<exists>n. \<forall>m>n. g m \<le> c * f m" by blast
   1.194        then have "g \<lesssim> f" ..
   1.195 -      from `f \<lesssim> g` and `g \<lesssim> f` show "f \<lesssim> g \<and> g \<lesssim> f" ..
   1.196 +      from \<open>f \<lesssim> g\<close> and \<open>g \<lesssim> f\<close> show "f \<lesssim> g \<and> g \<lesssim> f" ..
   1.197      next
   1.198        assume "f \<lesssim> g \<and> g \<lesssim> f"
   1.199        then have "f \<lesssim> g" and "g \<lesssim> f" by auto
   1.200 -      from `f \<lesssim> g` obtain n\<^sub>1 c\<^sub>1 where "c\<^sub>1 > 0"
   1.201 +      from \<open>f \<lesssim> g\<close> obtain n\<^sub>1 c\<^sub>1 where "c\<^sub>1 > 0"
   1.202          and P\<^sub>1: "\<And>m. m > n\<^sub>1 \<Longrightarrow> f m \<le> c\<^sub>1 * g m" by rule blast
   1.203 -      from `g \<lesssim> f` obtain n\<^sub>2 c\<^sub>2 where "c\<^sub>2 > 0"
   1.204 +      from \<open>g \<lesssim> f\<close> obtain n\<^sub>2 c\<^sub>2 where "c\<^sub>2 > 0"
   1.205          and P\<^sub>2: "\<And>m. m > n\<^sub>2 \<Longrightarrow> g m \<le> c\<^sub>2 * f m" by rule blast
   1.206        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"
   1.207        proof (rule allI, rule impI)
   1.208 @@ -269,7 +269,7 @@
   1.209          moreover from P\<^sub>2 Q have "g m \<le> c\<^sub>2 * f m" by simp
   1.210          ultimately show "f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m" ..
   1.211        qed
   1.212 -      with `c\<^sub>1 > 0` `c\<^sub>2 > 0` have "\<exists>c\<^sub>1>0. \<exists>c\<^sub>2>0. \<exists>n.
   1.213 +      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.
   1.214          \<forall>m>n. f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m" by blast
   1.215        then show "f \<cong> g" ..
   1.216      qed
   1.217 @@ -277,18 +277,18 @@
   1.218  qed
   1.219  
   1.220  
   1.221 -subsection {* Simple examples *}
   1.222 +subsection \<open>Simple examples\<close>
   1.223  
   1.224 -text {*
   1.225 +text \<open>
   1.226    Most of these are left as constructive exercises for the reader.  Note that additional
   1.227    preconditions to the functions may be necessary.  The list here is by no means to be
   1.228    intended as complete construction set for typical functions, here surely something
   1.229    has to be added yet.
   1.230 -*}
   1.231 +\<close>
   1.232  
   1.233 -text {* @{prop "(\<lambda>n. f n + k) \<cong> f"} *}
   1.234 +text \<open>@{prop "(\<lambda>n. f n + k) \<cong> f"}\<close>
   1.235  
   1.236 -text {* @{prop "(\<lambda>n. Suc k * f n) \<cong> f"} *}
   1.237 +text \<open>@{prop "(\<lambda>n. Suc k * f n) \<cong> f"}\<close>
   1.238  
   1.239  lemma "f \<lesssim> (\<lambda>n. f n + g n)"
   1.240    by rule auto
   1.241 @@ -312,7 +312,7 @@
   1.242    then show "\<exists>n. \<forall>m>n. c * k < Discrete.log m" ..
   1.243  qed
   1.244    
   1.245 -text {* @{prop "Discrete.log \<prec> Discrete.sqrt"} *}
   1.246 +text \<open>@{prop "Discrete.log \<prec> Discrete.sqrt"}\<close>
   1.247  
   1.248  lemma "Discrete.sqrt \<prec> id"
   1.249  proof (rule less_fun_strongI)
   1.250 @@ -326,7 +326,7 @@
   1.251      with mono_sqrt have "Discrete.sqrt ((Suc c)\<^sup>2) \<le> Discrete.sqrt m" by (rule monoE)
   1.252      then have "Suc c \<le> Discrete.sqrt m" by simp
   1.253      then have "c < Discrete.sqrt m" by simp
   1.254 -    moreover from `(Suc c)\<^sup>2 < m` have "Discrete.sqrt m > 0" by simp
   1.255 +    moreover from \<open>(Suc c)\<^sup>2 < m\<close> have "Discrete.sqrt m > 0" by simp
   1.256      ultimately have "c * Discrete.sqrt m < Discrete.sqrt m * Discrete.sqrt m" by simp
   1.257      also have "\<dots> \<le> m" by (simp add: power2_eq_square [symmetric])
   1.258      finally show "c * Discrete.sqrt m < id m" by simp
   1.259 @@ -340,7 +340,7 @@
   1.260  lemma "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. n ^ Suc k)"
   1.261    by (rule less_fun_strongI) auto
   1.262  
   1.263 -text {* @{prop "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. 2 ^ n)"} *}
   1.264 +text \<open>@{prop "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. 2 ^ n)"}\<close>
   1.265  
   1.266  end
   1.267