removed mere toy example from library
authorhaftmann
Sun Oct 08 22:28:19 2017 +0200 (19 months ago)
changeset 667979c9baae29217
parent 66796 ea9b2e5ca9fc
child 66798 39bb2462e681
removed mere toy example from library
src/HOL/Library/Function_Growth.thy
src/HOL/Library/Library.thy
src/HOL/ROOT
src/HOL/ex/Function_Growth.thy
     1.1 --- a/src/HOL/Library/Function_Growth.thy	Sun Oct 08 22:28:19 2017 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,454 +0,0 @@
     1.4 -  
     1.5 -(* Author: Florian Haftmann, TU Muenchen *)
     1.6 -
     1.7 -section \<open>Comparing growth of functions on natural numbers by a preorder relation\<close>
     1.8 -
     1.9 -theory Function_Growth
    1.10 -imports Main Preorder Discrete
    1.11 -begin
    1.12 -
    1.13 -(* FIXME move *)
    1.14 -
    1.15 -context linorder
    1.16 -begin
    1.17 -
    1.18 -lemma mono_invE:
    1.19 -  fixes f :: "'a \<Rightarrow> 'b::order"
    1.20 -  assumes "mono f"
    1.21 -  assumes "f x < f y"
    1.22 -  obtains "x < y"
    1.23 -proof
    1.24 -  show "x < y"
    1.25 -  proof (rule ccontr)
    1.26 -    assume "\<not> x < y"
    1.27 -    then have "y \<le> x" by simp
    1.28 -    with \<open>mono f\<close> obtain "f y \<le> f x" by (rule monoE)
    1.29 -    with \<open>f x < f y\<close> show False by simp
    1.30 -  qed
    1.31 -qed
    1.32 -
    1.33 -end
    1.34 -
    1.35 -lemma (in semidom_divide) power_diff:
    1.36 -  fixes a :: 'a
    1.37 -  assumes "a \<noteq> 0"
    1.38 -  assumes "m \<ge> n"
    1.39 -  shows "a ^ (m - n) = (a ^ m) div (a ^ n)"
    1.40 -proof -
    1.41 -  define q where "q = m - n"
    1.42 -  with assms have "m = q + n" by (simp add: q_def)
    1.43 -  with q_def show ?thesis using \<open>a \<noteq> 0\<close> by (simp add: power_add)
    1.44 -qed
    1.45 -
    1.46 -
    1.47 -subsection \<open>Motivation\<close>
    1.48 -
    1.49 -text \<open>
    1.50 -  When comparing growth of functions in computer science, it is common to adhere
    1.51 -  on Landau Symbols (``O-Notation'').  However these come at the cost of notational
    1.52 -  oddities, particularly writing \<open>f = O(g)\<close> for \<open>f \<in> O(g)\<close> etc.
    1.53 -  
    1.54 -  Here we suggest a different way, following Hardy (G.~H.~Hardy and J.~E.~Littlewood,
    1.55 -  Some problems of Diophantine approximation, Acta Mathematica 37 (1914), p.~225).
    1.56 -  We establish a quasi order relation \<open>\<lesssim>\<close> on functions such that
    1.57 -  \<open>f \<lesssim> g \<longleftrightarrow> f \<in> O(g)\<close>.  From a didactic point of view, this does not only
    1.58 -  avoid the notational oddities mentioned above but also emphasizes the key insight
    1.59 -  of a growth hierarchy of functions:
    1.60 -  \<open>(\<lambda>n. 0) \<lesssim> (\<lambda>n. k) \<lesssim> Discrete.log \<lesssim> Discrete.sqrt \<lesssim> id \<lesssim> \<dots>\<close>.
    1.61 -\<close>
    1.62 -
    1.63 -subsection \<open>Model\<close>
    1.64 -
    1.65 -text \<open>
    1.66 -  Our growth functions are of type \<open>\<nat> \<Rightarrow> \<nat>\<close>.  This is different
    1.67 -  to the usual conventions for Landau symbols for which \<open>\<real> \<Rightarrow> \<real>\<close>
    1.68 -  would be appropriate, but we argue that \<open>\<real> \<Rightarrow> \<real>\<close> is more
    1.69 -  appropriate for analysis, whereas our setting is discrete.
    1.70 -
    1.71 -  Note that we also restrict the additional coefficients to \<open>\<nat>\<close>, something
    1.72 -  we discuss at the particular definitions.
    1.73 -\<close>
    1.74 -
    1.75 -subsection \<open>The \<open>\<lesssim>\<close> relation\<close>
    1.76 -
    1.77 -definition less_eq_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<lesssim>" 50)
    1.78 -where
    1.79 -  "f \<lesssim> g \<longleftrightarrow> (\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m)"
    1.80 -
    1.81 -text \<open>
    1.82 -  This yields \<open>f \<lesssim> g \<longleftrightarrow> f \<in> O(g)\<close>.  Note that \<open>c\<close> is restricted to
    1.83 -  \<open>\<nat>\<close>.  This does not pose any problems since if \<open>f \<in> O(g)\<close> holds for
    1.84 -  a \<open>c \<in> \<real>\<close>, it also holds for \<open>\<lceil>c\<rceil> \<in> \<nat>\<close> by transitivity.
    1.85 -\<close>
    1.86 -
    1.87 -lemma less_eq_funI [intro?]:
    1.88 -  assumes "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m"
    1.89 -  shows "f \<lesssim> g"
    1.90 -  unfolding less_eq_fun_def by (rule assms)
    1.91 -
    1.92 -lemma not_less_eq_funI:
    1.93 -  assumes "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * g m < f m"
    1.94 -  shows "\<not> f \<lesssim> g"
    1.95 -  using assms unfolding less_eq_fun_def linorder_not_le [symmetric] by blast
    1.96 -
    1.97 -lemma less_eq_funE [elim?]:
    1.98 -  assumes "f \<lesssim> g"
    1.99 -  obtains n c where "c > 0" and "\<And>m. m > n \<Longrightarrow> f m \<le> c * g m"
   1.100 -  using assms unfolding less_eq_fun_def by blast
   1.101 -
   1.102 -lemma not_less_eq_funE:
   1.103 -  assumes "\<not> f \<lesssim> g" and "c > 0"
   1.104 -  obtains m where "m > n" and "c * g m < f m"
   1.105 -  using assms unfolding less_eq_fun_def linorder_not_le [symmetric] by blast
   1.106 -
   1.107 -
   1.108 -subsection \<open>The \<open>\<approx>\<close> relation, the equivalence relation induced by \<open>\<lesssim>\<close>\<close>
   1.109 -
   1.110 -definition equiv_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<cong>" 50)
   1.111 -where
   1.112 -  "f \<cong> g \<longleftrightarrow>
   1.113 -    (\<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.114 -
   1.115 -text \<open>
   1.116 -  This yields \<open>f \<cong> g \<longleftrightarrow> f \<in> \<Theta>(g)\<close>.  Concerning \<open>c\<^sub>1\<close> and \<open>c\<^sub>2\<close>
   1.117 -  restricted to @{typ nat}, see note above on \<open>(\<lesssim>)\<close>.
   1.118 -\<close>
   1.119 -
   1.120 -lemma equiv_funI:
   1.121 -  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.122 -  shows "f \<cong> g"
   1.123 -  unfolding equiv_fun_def by (rule assms)
   1.124 -
   1.125 -lemma not_equiv_funI:
   1.126 -  assumes "\<And>c\<^sub>1 c\<^sub>2 n. c\<^sub>1 > 0 \<Longrightarrow> c\<^sub>2 > 0 \<Longrightarrow>
   1.127 -    \<exists>m>n. c\<^sub>1 * f m < g m \<or> c\<^sub>2 * g m < f m"
   1.128 -  shows "\<not> f \<cong> g"
   1.129 -  using assms unfolding equiv_fun_def linorder_not_le [symmetric] by blast
   1.130 -
   1.131 -lemma equiv_funE:
   1.132 -  assumes "f \<cong> g"
   1.133 -  obtains n c\<^sub>1 c\<^sub>2 where "c\<^sub>1 > 0" and "c\<^sub>2 > 0"
   1.134 -    and "\<And>m. m > n \<Longrightarrow> f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m"
   1.135 -  using assms unfolding equiv_fun_def by blast
   1.136 -
   1.137 -lemma not_equiv_funE:
   1.138 -  fixes n c\<^sub>1 c\<^sub>2
   1.139 -  assumes "\<not> f \<cong> g" and "c\<^sub>1 > 0" and "c\<^sub>2 > 0"
   1.140 -  obtains m where "m > n"
   1.141 -    and "c\<^sub>1 * f m < g m \<or> c\<^sub>2 * g m < f m"
   1.142 -  using assms unfolding equiv_fun_def linorder_not_le [symmetric] by blast
   1.143 -
   1.144 -
   1.145 -subsection \<open>The \<open>\<prec>\<close> relation, the strict part of \<open>\<lesssim>\<close>\<close>
   1.146 -
   1.147 -definition less_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<prec>" 50)
   1.148 -where
   1.149 -  "f \<prec> g \<longleftrightarrow> f \<lesssim> g \<and> \<not> g \<lesssim> f"
   1.150 -
   1.151 -lemma less_funI:
   1.152 -  assumes "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m"
   1.153 -    and "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * f m < g m"
   1.154 -  shows "f \<prec> g"
   1.155 -  using assms unfolding less_fun_def less_eq_fun_def linorder_not_less [symmetric] by blast
   1.156 -
   1.157 -lemma not_less_funI:
   1.158 -  assumes "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * g m < f m"
   1.159 -    and "\<exists>c>0. \<exists>n. \<forall>m>n. g m \<le> c * f m"
   1.160 -  shows "\<not> f \<prec> g"
   1.161 -  using assms unfolding less_fun_def less_eq_fun_def linorder_not_less [symmetric] by blast
   1.162 -
   1.163 -lemma less_funE [elim?]:
   1.164 -  assumes "f \<prec> g"
   1.165 -  obtains n c where "c > 0" and "\<And>m. m > n \<Longrightarrow> f m \<le> c * g m"
   1.166 -    and "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * f m < g m"
   1.167 -proof -
   1.168 -  from assms have "f \<lesssim> g" and "\<not> g \<lesssim> f" by (simp_all add: less_fun_def)
   1.169 -  from \<open>f \<lesssim> g\<close> obtain n c where *:"c > 0" "m > n \<Longrightarrow> f m \<le> c * g m" for m
   1.170 -    by (rule less_eq_funE) blast
   1.171 -  { fix c n :: nat
   1.172 -    assume "c > 0"
   1.173 -    with \<open>\<not> g \<lesssim> f\<close> obtain m where "m > n" "c * f m < g m"
   1.174 -      by (rule not_less_eq_funE) blast
   1.175 -    then have **: "\<exists>m>n. c * f m < g m" by blast
   1.176 -  } note ** = this
   1.177 -  from * ** show thesis by (rule that)
   1.178 -qed
   1.179 -
   1.180 -lemma not_less_funE:
   1.181 -  assumes "\<not> f \<prec> g" and "c > 0"
   1.182 -  obtains m where "m > n" and "c * g m < f m"
   1.183 -    | d q where "\<And>m. d > 0 \<Longrightarrow> m > q \<Longrightarrow> g q \<le> d * f q"
   1.184 -  using assms unfolding less_fun_def linorder_not_less [symmetric] by blast
   1.185 -
   1.186 -text \<open>
   1.187 -  I did not find a proof for \<open>f \<prec> g \<longleftrightarrow> f \<in> o(g)\<close>.  Maybe this only
   1.188 -  holds if \<open>f\<close> and/or \<open>g\<close> are of a certain class of functions.
   1.189 -  However \<open>f \<in> o(g) \<longrightarrow> f \<prec> g\<close> is provable, and this yields a
   1.190 -  handy introduction rule.
   1.191 -
   1.192 -  Note that D. Knuth ignores \<open>o\<close> altogether.  So what \dots
   1.193 -
   1.194 -  Something still has to be said about the coefficient \<open>c\<close> in
   1.195 -  the definition of \<open>(\<prec>)\<close>.  In the typical definition of \<open>o\<close>,
   1.196 -  it occurs on the \emph{right} hand side of the \<open>(>)\<close>.  The reason
   1.197 -  is that the situation is dual to the definition of \<open>O\<close>: the definition
   1.198 -  works since \<open>c\<close> may become arbitrary small.  Since this is not possible
   1.199 -  within @{term \<nat>}, we push the coefficient to the left hand side instead such
   1.200 -  that it may become arbitrary big instead.
   1.201 -\<close>
   1.202 -
   1.203 -lemma less_fun_strongI:
   1.204 -  assumes "\<And>c. c > 0 \<Longrightarrow> \<exists>n. \<forall>m>n. c * f m < g m"
   1.205 -  shows "f \<prec> g"
   1.206 -proof (rule less_funI)
   1.207 -  have "1 > (0::nat)" by simp
   1.208 -  with assms [OF this] obtain n where *: "m > n \<Longrightarrow> 1 * f m < g m" for m
   1.209 -    by blast
   1.210 -  have "\<forall>m>n. f m \<le> 1 * g m"
   1.211 -  proof (rule allI, rule impI)
   1.212 -    fix m
   1.213 -    assume "m > n"
   1.214 -    with * have "1 * f m < g m" by simp
   1.215 -    then show "f m \<le> 1 * g m" by simp
   1.216 -  qed
   1.217 -  with \<open>1 > 0\<close> show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m" by blast
   1.218 -  fix c n :: nat
   1.219 -  assume "c > 0"
   1.220 -  with assms obtain q where "m > q \<Longrightarrow> c * f m < g m" for m by blast
   1.221 -  then have "c * f (Suc (q + n)) < g (Suc (q + n))" by simp
   1.222 -  moreover have "Suc (q + n) > n" by simp
   1.223 -  ultimately show "\<exists>m>n. c * f m < g m" by blast
   1.224 -qed
   1.225 -
   1.226 -
   1.227 -subsection \<open>\<open>\<lesssim>\<close> is a preorder\<close>
   1.228 -
   1.229 -text \<open>This yields all lemmas relating \<open>\<lesssim>\<close>, \<open>\<prec>\<close> and \<open>\<cong>\<close>.\<close>
   1.230 -
   1.231 -interpretation fun_order: preorder_equiv less_eq_fun less_fun
   1.232 -  rewrites "fun_order.equiv = equiv_fun"
   1.233 -proof -
   1.234 -  interpret preorder: preorder_equiv less_eq_fun less_fun
   1.235 -  proof
   1.236 -    fix f g h
   1.237 -    show "f \<lesssim> f"
   1.238 -    proof
   1.239 -      have "\<exists>n. \<forall>m>n. f m \<le> 1 * f m" by auto
   1.240 -      then show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * f m" by blast
   1.241 -    qed
   1.242 -    show "f \<prec> g \<longleftrightarrow> f \<lesssim> g \<and> \<not> g \<lesssim> f"
   1.243 -      by (fact less_fun_def)
   1.244 -    assume "f \<lesssim> g" and "g \<lesssim> h"
   1.245 -    show "f \<lesssim> h"
   1.246 -    proof
   1.247 -      from \<open>f \<lesssim> g\<close> obtain n\<^sub>1 c\<^sub>1
   1.248 -        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.249 -        by rule blast
   1.250 -      from \<open>g \<lesssim> h\<close> obtain n\<^sub>2 c\<^sub>2
   1.251 -        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.252 -        by rule blast
   1.253 -      have "\<forall>m>max n\<^sub>1 n\<^sub>2. f m \<le> (c\<^sub>1 * c\<^sub>2) * h m"
   1.254 -      proof (rule allI, rule impI)
   1.255 -        fix m
   1.256 -        assume Q: "m > max n\<^sub>1 n\<^sub>2"
   1.257 -        from P\<^sub>1 Q have *: "f m \<le> c\<^sub>1 * g m" by simp
   1.258 -        from P\<^sub>2 Q have "g m \<le> c\<^sub>2 * h m" by simp
   1.259 -        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.260 -        with * show "f m \<le> (c\<^sub>1 * c\<^sub>2) * h m" by (rule order_trans)
   1.261 -      qed
   1.262 -      then have "\<exists>n. \<forall>m>n. f m \<le> (c\<^sub>1 * c\<^sub>2) * h m" by rule
   1.263 -      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.264 -      ultimately show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * h m" by blast
   1.265 -    qed
   1.266 -  qed
   1.267 -  from preorder.preorder_equiv_axioms show "class.preorder_equiv less_eq_fun less_fun" .
   1.268 -  show "preorder_equiv.equiv less_eq_fun = equiv_fun"
   1.269 -  proof (rule ext, rule ext, unfold preorder.equiv_def)
   1.270 -    fix f g
   1.271 -    show "f \<lesssim> g \<and> g \<lesssim> f \<longleftrightarrow> f \<cong> g"
   1.272 -    proof
   1.273 -      assume "f \<cong> g"
   1.274 -      then obtain n c\<^sub>1 c\<^sub>2 where "c\<^sub>1 > 0" and "c\<^sub>2 > 0"
   1.275 -        and *: "\<And>m. m > n \<Longrightarrow> f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m"
   1.276 -        by (rule equiv_funE) blast
   1.277 -      have "\<forall>m>n. f m \<le> c\<^sub>1 * g m"
   1.278 -      proof (rule allI, rule impI)
   1.279 -        fix m
   1.280 -        assume "m > n"
   1.281 -        with * show "f m \<le> c\<^sub>1 * g m" by simp
   1.282 -      qed
   1.283 -      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.284 -      then have "f \<lesssim> g" ..
   1.285 -      have "\<forall>m>n. g m \<le> c\<^sub>2 * f m"
   1.286 -      proof (rule allI, rule impI)
   1.287 -        fix m
   1.288 -        assume "m > n"
   1.289 -        with * show "g m \<le> c\<^sub>2 * f m" by simp
   1.290 -      qed
   1.291 -      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.292 -      then have "g \<lesssim> f" ..
   1.293 -      from \<open>f \<lesssim> g\<close> and \<open>g \<lesssim> f\<close> show "f \<lesssim> g \<and> g \<lesssim> f" ..
   1.294 -    next
   1.295 -      assume "f \<lesssim> g \<and> g \<lesssim> f"
   1.296 -      then have "f \<lesssim> g" and "g \<lesssim> f" by auto
   1.297 -      from \<open>f \<lesssim> g\<close> obtain n\<^sub>1 c\<^sub>1 where "c\<^sub>1 > 0"
   1.298 -        and P\<^sub>1: "\<And>m. m > n\<^sub>1 \<Longrightarrow> f m \<le> c\<^sub>1 * g m" by rule blast
   1.299 -      from \<open>g \<lesssim> f\<close> obtain n\<^sub>2 c\<^sub>2 where "c\<^sub>2 > 0"
   1.300 -        and P\<^sub>2: "\<And>m. m > n\<^sub>2 \<Longrightarrow> g m \<le> c\<^sub>2 * f m" by rule blast
   1.301 -      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.302 -      proof (rule allI, rule impI)
   1.303 -        fix m
   1.304 -        assume Q: "m > max n\<^sub>1 n\<^sub>2"
   1.305 -        from P\<^sub>1 Q have "f m \<le> c\<^sub>1 * g m" by simp
   1.306 -        moreover from P\<^sub>2 Q have "g m \<le> c\<^sub>2 * f m" by simp
   1.307 -        ultimately show "f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m" ..
   1.308 -      qed
   1.309 -      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.310 -        \<forall>m>n. f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m" by blast
   1.311 -      then show "f \<cong> g" by (rule equiv_funI)
   1.312 -    qed
   1.313 -  qed
   1.314 -qed
   1.315 -
   1.316 -declare fun_order.antisym [intro?]
   1.317 -
   1.318 -
   1.319 -subsection \<open>Simple examples\<close>
   1.320 -
   1.321 -text \<open>
   1.322 -  Most of these are left as constructive exercises for the reader.  Note that additional
   1.323 -  preconditions to the functions may be necessary.  The list here is by no means to be
   1.324 -  intended as complete construction set for typical functions, here surely something
   1.325 -  has to be added yet.
   1.326 -\<close>
   1.327 -
   1.328 -text \<open>@{prop "(\<lambda>n. f n + k) \<cong> f"}\<close>
   1.329 -
   1.330 -lemma equiv_fun_mono_const:
   1.331 -  assumes "mono f" and "\<exists>n. f n > 0"
   1.332 -  shows "(\<lambda>n. f n + k) \<cong> f"
   1.333 -proof (cases "k = 0")
   1.334 -  case True then show ?thesis by simp
   1.335 -next
   1.336 -  case False
   1.337 -  show ?thesis
   1.338 -  proof
   1.339 -    show "(\<lambda>n. f n + k) \<lesssim> f"
   1.340 -    proof
   1.341 -      from \<open>\<exists>n. f n > 0\<close> obtain n where "f n > 0" ..
   1.342 -      have "\<forall>m>n. f m + k \<le> Suc k * f m"
   1.343 -      proof (rule allI, rule impI)
   1.344 -        fix m
   1.345 -        assume "n < m"
   1.346 -        with \<open>mono f\<close> have "f n \<le> f m"
   1.347 -          using less_imp_le_nat monoE by blast
   1.348 -        with  \<open>0 < f n\<close> have "0 < f m" by auto
   1.349 -        then obtain l where "f m = Suc l" by (cases "f m") simp_all
   1.350 -        then show "f m + k \<le> Suc k * f m" by simp
   1.351 -      qed
   1.352 -      then show "\<exists>c>0. \<exists>n. \<forall>m>n. f m + k \<le> c * f m" by blast
   1.353 -    qed
   1.354 -    show "f \<lesssim> (\<lambda>n. f n + k)"
   1.355 -    proof
   1.356 -      have "f m \<le> 1 * (f m + k)" for m by simp
   1.357 -      then show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * (f m + k)" by blast
   1.358 -    qed
   1.359 -  qed
   1.360 -qed
   1.361 -
   1.362 -lemma
   1.363 -  assumes "strict_mono f"
   1.364 -  shows "(\<lambda>n. f n + k) \<cong> f"
   1.365 -proof (rule equiv_fun_mono_const)
   1.366 -  from assms show "mono f" by (rule strict_mono_mono)
   1.367 -  show "\<exists>n. 0 < f n"
   1.368 -  proof (rule ccontr)
   1.369 -    assume "\<not> (\<exists>n. 0 < f n)"
   1.370 -    then have "\<And>n. f n = 0" by simp
   1.371 -    then have "f 0 = f 1" by simp
   1.372 -    moreover from \<open>strict_mono f\<close> have "f 0 < f 1"
   1.373 -      by (simp add: strict_mono_def) 
   1.374 -    ultimately show False by simp
   1.375 -  qed
   1.376 -qed
   1.377 -  
   1.378 -lemma
   1.379 -  "(\<lambda>n. Suc k * f n) \<cong> f"
   1.380 -proof
   1.381 -  show "(\<lambda>n. Suc k * f n) \<lesssim> f"
   1.382 -  proof
   1.383 -    have "Suc k * f m \<le> Suc k * f m" for m by simp
   1.384 -    then show "\<exists>c>0. \<exists>n. \<forall>m>n. Suc k * f m \<le> c * f m" by blast
   1.385 -  qed
   1.386 -  show "f \<lesssim> (\<lambda>n. Suc k * f n)"
   1.387 -  proof
   1.388 -    have "f m \<le> 1 * (Suc k * f m)" for m by simp
   1.389 -    then show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * (Suc k * f m)" by blast
   1.390 -  qed
   1.391 -qed
   1.392 -
   1.393 -lemma
   1.394 -  "f \<lesssim> (\<lambda>n. f n + g n)"
   1.395 -  by rule auto
   1.396 -
   1.397 -lemma
   1.398 -  "(\<lambda>_. 0) \<prec> (\<lambda>n. Suc k)"
   1.399 -  by (rule less_fun_strongI) auto
   1.400 -
   1.401 -lemma
   1.402 -  "(\<lambda>_. k) \<prec> Discrete.log"
   1.403 -proof (rule less_fun_strongI)
   1.404 -  fix c :: nat
   1.405 -  have "\<forall>m>2 ^ (Suc (c * k)). c * k < Discrete.log m"
   1.406 -  proof (rule allI, rule impI)
   1.407 -    fix m :: nat
   1.408 -    assume "2 ^ Suc (c * k) < m"
   1.409 -    then have "2 ^ Suc (c * k) \<le> m" by simp
   1.410 -    with log_mono have "Discrete.log (2 ^ (Suc (c * k))) \<le> Discrete.log m"
   1.411 -      by (blast dest: monoD)
   1.412 -    moreover have "c * k < Discrete.log (2 ^ (Suc (c * k)))" by simp
   1.413 -    ultimately show "c * k < Discrete.log m" by auto
   1.414 -  qed
   1.415 -  then show "\<exists>n. \<forall>m>n. c * k < Discrete.log m" ..
   1.416 -qed
   1.417 -
   1.418 -(*lemma
   1.419 -  "Discrete.log \<prec> Discrete.sqrt"
   1.420 -proof (rule less_fun_strongI)*)
   1.421 -text \<open>@{prop "Discrete.log \<prec> Discrete.sqrt"}\<close>
   1.422 -
   1.423 -lemma
   1.424 -  "Discrete.sqrt \<prec> id"
   1.425 -proof (rule less_fun_strongI)
   1.426 -  fix c :: nat
   1.427 -  assume "0 < c"
   1.428 -  have "\<forall>m>(Suc c)\<^sup>2. c * Discrete.sqrt m < id m"
   1.429 -  proof (rule allI, rule impI)
   1.430 -    fix m
   1.431 -    assume "(Suc c)\<^sup>2 < m"
   1.432 -    then have "(Suc c)\<^sup>2 \<le> m" by simp
   1.433 -    with mono_sqrt have "Discrete.sqrt ((Suc c)\<^sup>2) \<le> Discrete.sqrt m" by (rule monoE)
   1.434 -    then have "Suc c \<le> Discrete.sqrt m" by simp
   1.435 -    then have "c < Discrete.sqrt m" by simp
   1.436 -    moreover from \<open>(Suc c)\<^sup>2 < m\<close> have "Discrete.sqrt m > 0" by simp
   1.437 -    ultimately have "c * Discrete.sqrt m < Discrete.sqrt m * Discrete.sqrt m" by simp
   1.438 -    also have "\<dots> \<le> m" by (simp add: power2_eq_square [symmetric])
   1.439 -    finally show "c * Discrete.sqrt m < id m" by simp
   1.440 -  qed
   1.441 -  then show "\<exists>n. \<forall>m>n. c * Discrete.sqrt m < id m" ..
   1.442 -qed
   1.443 -
   1.444 -lemma
   1.445 -  "id \<prec> (\<lambda>n. n\<^sup>2)"
   1.446 -  by (rule less_fun_strongI) (auto simp add: power2_eq_square)
   1.447 -
   1.448 -lemma
   1.449 -  "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. n ^ Suc k)"
   1.450 -  by (rule less_fun_strongI) auto
   1.451 -
   1.452 -(*lemma 
   1.453 -  "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. 2 ^ n)"
   1.454 -proof (rule less_fun_strongI)*)
   1.455 -text \<open>@{prop "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. 2 ^ n)"}\<close>
   1.456 -
   1.457 -end
     2.1 --- a/src/HOL/Library/Library.thy	Sun Oct 08 22:28:19 2017 +0200
     2.2 +++ b/src/HOL/Library/Library.thy	Sun Oct 08 22:28:19 2017 +0200
     2.3 @@ -17,6 +17,7 @@
     2.4    Countable_Set_Type
     2.5    Debug
     2.6    Diagonal_Subsequence
     2.7 +  Discrete
     2.8    Disjoint_Sets
     2.9    Dlist
    2.10    Extended
    2.11 @@ -28,7 +29,6 @@
    2.12    FSet
    2.13    FuncSet
    2.14    Function_Division
    2.15 -  Function_Growth
    2.16    Fun_Lexorder
    2.17    Going_To_Filter
    2.18    Groups_Big_Fun
     3.1 --- a/src/HOL/ROOT	Sun Oct 08 22:28:19 2017 +0200
     3.2 +++ b/src/HOL/ROOT	Sun Oct 08 22:28:19 2017 +0200
     3.3 @@ -548,6 +548,7 @@
     3.4      Executable_Relation
     3.5      Execute_Choice
     3.6      Functions
     3.7 +    Function_Growth
     3.8      Gauge_Integration
     3.9      Groebner_Examples
    3.10      Guess
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/ex/Function_Growth.thy	Sun Oct 08 22:28:19 2017 +0200
     4.3 @@ -0,0 +1,457 @@
     4.4 +  
     4.5 +(* Author: Florian Haftmann, TU Muenchen *)
     4.6 +
     4.7 +section \<open>Comparing growth of functions on natural numbers by a preorder relation\<close>
     4.8 +
     4.9 +theory Function_Growth
    4.10 +imports
    4.11 +  Main
    4.12 +  "HOL-Library.Preorder"
    4.13 +  "HOL-Library.Discrete"
    4.14 +begin
    4.15 +
    4.16 +(* FIXME move *)
    4.17 +
    4.18 +context linorder
    4.19 +begin
    4.20 +
    4.21 +lemma mono_invE:
    4.22 +  fixes f :: "'a \<Rightarrow> 'b::order"
    4.23 +  assumes "mono f"
    4.24 +  assumes "f x < f y"
    4.25 +  obtains "x < y"
    4.26 +proof
    4.27 +  show "x < y"
    4.28 +  proof (rule ccontr)
    4.29 +    assume "\<not> x < y"
    4.30 +    then have "y \<le> x" by simp
    4.31 +    with \<open>mono f\<close> obtain "f y \<le> f x" by (rule monoE)
    4.32 +    with \<open>f x < f y\<close> show False by simp
    4.33 +  qed
    4.34 +qed
    4.35 +
    4.36 +end
    4.37 +
    4.38 +lemma (in semidom_divide) power_diff:
    4.39 +  fixes a :: 'a
    4.40 +  assumes "a \<noteq> 0"
    4.41 +  assumes "m \<ge> n"
    4.42 +  shows "a ^ (m - n) = (a ^ m) div (a ^ n)"
    4.43 +proof -
    4.44 +  define q where "q = m - n"
    4.45 +  with assms have "m = q + n" by (simp add: q_def)
    4.46 +  with q_def show ?thesis using \<open>a \<noteq> 0\<close> by (simp add: power_add)
    4.47 +qed
    4.48 +
    4.49 +
    4.50 +subsection \<open>Motivation\<close>
    4.51 +
    4.52 +text \<open>
    4.53 +  When comparing growth of functions in computer science, it is common to adhere
    4.54 +  on Landau Symbols (``O-Notation'').  However these come at the cost of notational
    4.55 +  oddities, particularly writing \<open>f = O(g)\<close> for \<open>f \<in> O(g)\<close> etc.
    4.56 +  
    4.57 +  Here we suggest a different way, following Hardy (G.~H.~Hardy and J.~E.~Littlewood,
    4.58 +  Some problems of Diophantine approximation, Acta Mathematica 37 (1914), p.~225).
    4.59 +  We establish a quasi order relation \<open>\<lesssim>\<close> on functions such that
    4.60 +  \<open>f \<lesssim> g \<longleftrightarrow> f \<in> O(g)\<close>.  From a didactic point of view, this does not only
    4.61 +  avoid the notational oddities mentioned above but also emphasizes the key insight
    4.62 +  of a growth hierarchy of functions:
    4.63 +  \<open>(\<lambda>n. 0) \<lesssim> (\<lambda>n. k) \<lesssim> Discrete.log \<lesssim> Discrete.sqrt \<lesssim> id \<lesssim> \<dots>\<close>.
    4.64 +\<close>
    4.65 +
    4.66 +subsection \<open>Model\<close>
    4.67 +
    4.68 +text \<open>
    4.69 +  Our growth functions are of type \<open>\<nat> \<Rightarrow> \<nat>\<close>.  This is different
    4.70 +  to the usual conventions for Landau symbols for which \<open>\<real> \<Rightarrow> \<real>\<close>
    4.71 +  would be appropriate, but we argue that \<open>\<real> \<Rightarrow> \<real>\<close> is more
    4.72 +  appropriate for analysis, whereas our setting is discrete.
    4.73 +
    4.74 +  Note that we also restrict the additional coefficients to \<open>\<nat>\<close>, something
    4.75 +  we discuss at the particular definitions.
    4.76 +\<close>
    4.77 +
    4.78 +subsection \<open>The \<open>\<lesssim>\<close> relation\<close>
    4.79 +
    4.80 +definition less_eq_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<lesssim>" 50)
    4.81 +where
    4.82 +  "f \<lesssim> g \<longleftrightarrow> (\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m)"
    4.83 +
    4.84 +text \<open>
    4.85 +  This yields \<open>f \<lesssim> g \<longleftrightarrow> f \<in> O(g)\<close>.  Note that \<open>c\<close> is restricted to
    4.86 +  \<open>\<nat>\<close>.  This does not pose any problems since if \<open>f \<in> O(g)\<close> holds for
    4.87 +  a \<open>c \<in> \<real>\<close>, it also holds for \<open>\<lceil>c\<rceil> \<in> \<nat>\<close> by transitivity.
    4.88 +\<close>
    4.89 +
    4.90 +lemma less_eq_funI [intro?]:
    4.91 +  assumes "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m"
    4.92 +  shows "f \<lesssim> g"
    4.93 +  unfolding less_eq_fun_def by (rule assms)
    4.94 +
    4.95 +lemma not_less_eq_funI:
    4.96 +  assumes "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * g m < f m"
    4.97 +  shows "\<not> f \<lesssim> g"
    4.98 +  using assms unfolding less_eq_fun_def linorder_not_le [symmetric] by blast
    4.99 +
   4.100 +lemma less_eq_funE [elim?]:
   4.101 +  assumes "f \<lesssim> g"
   4.102 +  obtains n c where "c > 0" and "\<And>m. m > n \<Longrightarrow> f m \<le> c * g m"
   4.103 +  using assms unfolding less_eq_fun_def by blast
   4.104 +
   4.105 +lemma not_less_eq_funE:
   4.106 +  assumes "\<not> f \<lesssim> g" and "c > 0"
   4.107 +  obtains m where "m > n" and "c * g m < f m"
   4.108 +  using assms unfolding less_eq_fun_def linorder_not_le [symmetric] by blast
   4.109 +
   4.110 +
   4.111 +subsection \<open>The \<open>\<approx>\<close> relation, the equivalence relation induced by \<open>\<lesssim>\<close>\<close>
   4.112 +
   4.113 +definition equiv_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<cong>" 50)
   4.114 +where
   4.115 +  "f \<cong> g \<longleftrightarrow>
   4.116 +    (\<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)"
   4.117 +
   4.118 +text \<open>
   4.119 +  This yields \<open>f \<cong> g \<longleftrightarrow> f \<in> \<Theta>(g)\<close>.  Concerning \<open>c\<^sub>1\<close> and \<open>c\<^sub>2\<close>
   4.120 +  restricted to @{typ nat}, see note above on \<open>(\<lesssim>)\<close>.
   4.121 +\<close>
   4.122 +
   4.123 +lemma equiv_funI:
   4.124 +  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"
   4.125 +  shows "f \<cong> g"
   4.126 +  unfolding equiv_fun_def by (rule assms)
   4.127 +
   4.128 +lemma not_equiv_funI:
   4.129 +  assumes "\<And>c\<^sub>1 c\<^sub>2 n. c\<^sub>1 > 0 \<Longrightarrow> c\<^sub>2 > 0 \<Longrightarrow>
   4.130 +    \<exists>m>n. c\<^sub>1 * f m < g m \<or> c\<^sub>2 * g m < f m"
   4.131 +  shows "\<not> f \<cong> g"
   4.132 +  using assms unfolding equiv_fun_def linorder_not_le [symmetric] by blast
   4.133 +
   4.134 +lemma equiv_funE:
   4.135 +  assumes "f \<cong> g"
   4.136 +  obtains n c\<^sub>1 c\<^sub>2 where "c\<^sub>1 > 0" and "c\<^sub>2 > 0"
   4.137 +    and "\<And>m. m > n \<Longrightarrow> f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m"
   4.138 +  using assms unfolding equiv_fun_def by blast
   4.139 +
   4.140 +lemma not_equiv_funE:
   4.141 +  fixes n c\<^sub>1 c\<^sub>2
   4.142 +  assumes "\<not> f \<cong> g" and "c\<^sub>1 > 0" and "c\<^sub>2 > 0"
   4.143 +  obtains m where "m > n"
   4.144 +    and "c\<^sub>1 * f m < g m \<or> c\<^sub>2 * g m < f m"
   4.145 +  using assms unfolding equiv_fun_def linorder_not_le [symmetric] by blast
   4.146 +
   4.147 +
   4.148 +subsection \<open>The \<open>\<prec>\<close> relation, the strict part of \<open>\<lesssim>\<close>\<close>
   4.149 +
   4.150 +definition less_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<prec>" 50)
   4.151 +where
   4.152 +  "f \<prec> g \<longleftrightarrow> f \<lesssim> g \<and> \<not> g \<lesssim> f"
   4.153 +
   4.154 +lemma less_funI:
   4.155 +  assumes "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m"
   4.156 +    and "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * f m < g m"
   4.157 +  shows "f \<prec> g"
   4.158 +  using assms unfolding less_fun_def less_eq_fun_def linorder_not_less [symmetric] by blast
   4.159 +
   4.160 +lemma not_less_funI:
   4.161 +  assumes "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * g m < f m"
   4.162 +    and "\<exists>c>0. \<exists>n. \<forall>m>n. g m \<le> c * f m"
   4.163 +  shows "\<not> f \<prec> g"
   4.164 +  using assms unfolding less_fun_def less_eq_fun_def linorder_not_less [symmetric] by blast
   4.165 +
   4.166 +lemma less_funE [elim?]:
   4.167 +  assumes "f \<prec> g"
   4.168 +  obtains n c where "c > 0" and "\<And>m. m > n \<Longrightarrow> f m \<le> c * g m"
   4.169 +    and "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * f m < g m"
   4.170 +proof -
   4.171 +  from assms have "f \<lesssim> g" and "\<not> g \<lesssim> f" by (simp_all add: less_fun_def)
   4.172 +  from \<open>f \<lesssim> g\<close> obtain n c where *:"c > 0" "m > n \<Longrightarrow> f m \<le> c * g m" for m
   4.173 +    by (rule less_eq_funE) blast
   4.174 +  { fix c n :: nat
   4.175 +    assume "c > 0"
   4.176 +    with \<open>\<not> g \<lesssim> f\<close> obtain m where "m > n" "c * f m < g m"
   4.177 +      by (rule not_less_eq_funE) blast
   4.178 +    then have **: "\<exists>m>n. c * f m < g m" by blast
   4.179 +  } note ** = this
   4.180 +  from * ** show thesis by (rule that)
   4.181 +qed
   4.182 +
   4.183 +lemma not_less_funE:
   4.184 +  assumes "\<not> f \<prec> g" and "c > 0"
   4.185 +  obtains m where "m > n" and "c * g m < f m"
   4.186 +    | d q where "\<And>m. d > 0 \<Longrightarrow> m > q \<Longrightarrow> g q \<le> d * f q"
   4.187 +  using assms unfolding less_fun_def linorder_not_less [symmetric] by blast
   4.188 +
   4.189 +text \<open>
   4.190 +  I did not find a proof for \<open>f \<prec> g \<longleftrightarrow> f \<in> o(g)\<close>.  Maybe this only
   4.191 +  holds if \<open>f\<close> and/or \<open>g\<close> are of a certain class of functions.
   4.192 +  However \<open>f \<in> o(g) \<longrightarrow> f \<prec> g\<close> is provable, and this yields a
   4.193 +  handy introduction rule.
   4.194 +
   4.195 +  Note that D. Knuth ignores \<open>o\<close> altogether.  So what \dots
   4.196 +
   4.197 +  Something still has to be said about the coefficient \<open>c\<close> in
   4.198 +  the definition of \<open>(\<prec>)\<close>.  In the typical definition of \<open>o\<close>,
   4.199 +  it occurs on the \emph{right} hand side of the \<open>(>)\<close>.  The reason
   4.200 +  is that the situation is dual to the definition of \<open>O\<close>: the definition
   4.201 +  works since \<open>c\<close> may become arbitrary small.  Since this is not possible
   4.202 +  within @{term \<nat>}, we push the coefficient to the left hand side instead such
   4.203 +  that it may become arbitrary big instead.
   4.204 +\<close>
   4.205 +
   4.206 +lemma less_fun_strongI:
   4.207 +  assumes "\<And>c. c > 0 \<Longrightarrow> \<exists>n. \<forall>m>n. c * f m < g m"
   4.208 +  shows "f \<prec> g"
   4.209 +proof (rule less_funI)
   4.210 +  have "1 > (0::nat)" by simp
   4.211 +  with assms [OF this] obtain n where *: "m > n \<Longrightarrow> 1 * f m < g m" for m
   4.212 +    by blast
   4.213 +  have "\<forall>m>n. f m \<le> 1 * g m"
   4.214 +  proof (rule allI, rule impI)
   4.215 +    fix m
   4.216 +    assume "m > n"
   4.217 +    with * have "1 * f m < g m" by simp
   4.218 +    then show "f m \<le> 1 * g m" by simp
   4.219 +  qed
   4.220 +  with \<open>1 > 0\<close> show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m" by blast
   4.221 +  fix c n :: nat
   4.222 +  assume "c > 0"
   4.223 +  with assms obtain q where "m > q \<Longrightarrow> c * f m < g m" for m by blast
   4.224 +  then have "c * f (Suc (q + n)) < g (Suc (q + n))" by simp
   4.225 +  moreover have "Suc (q + n) > n" by simp
   4.226 +  ultimately show "\<exists>m>n. c * f m < g m" by blast
   4.227 +qed
   4.228 +
   4.229 +
   4.230 +subsection \<open>\<open>\<lesssim>\<close> is a preorder\<close>
   4.231 +
   4.232 +text \<open>This yields all lemmas relating \<open>\<lesssim>\<close>, \<open>\<prec>\<close> and \<open>\<cong>\<close>.\<close>
   4.233 +
   4.234 +interpretation fun_order: preorder_equiv less_eq_fun less_fun
   4.235 +  rewrites "fun_order.equiv = equiv_fun"
   4.236 +proof -
   4.237 +  interpret preorder: preorder_equiv less_eq_fun less_fun
   4.238 +  proof
   4.239 +    fix f g h
   4.240 +    show "f \<lesssim> f"
   4.241 +    proof
   4.242 +      have "\<exists>n. \<forall>m>n. f m \<le> 1 * f m" by auto
   4.243 +      then show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * f m" by blast
   4.244 +    qed
   4.245 +    show "f \<prec> g \<longleftrightarrow> f \<lesssim> g \<and> \<not> g \<lesssim> f"
   4.246 +      by (fact less_fun_def)
   4.247 +    assume "f \<lesssim> g" and "g \<lesssim> h"
   4.248 +    show "f \<lesssim> h"
   4.249 +    proof
   4.250 +      from \<open>f \<lesssim> g\<close> obtain n\<^sub>1 c\<^sub>1
   4.251 +        where "c\<^sub>1 > 0" and P\<^sub>1: "\<And>m. m > n\<^sub>1 \<Longrightarrow> f m \<le> c\<^sub>1 * g m"
   4.252 +        by rule blast
   4.253 +      from \<open>g \<lesssim> h\<close> obtain n\<^sub>2 c\<^sub>2
   4.254 +        where "c\<^sub>2 > 0" and P\<^sub>2: "\<And>m. m > n\<^sub>2 \<Longrightarrow> g m \<le> c\<^sub>2 * h m"
   4.255 +        by rule blast
   4.256 +      have "\<forall>m>max n\<^sub>1 n\<^sub>2. f m \<le> (c\<^sub>1 * c\<^sub>2) * h m"
   4.257 +      proof (rule allI, rule impI)
   4.258 +        fix m
   4.259 +        assume Q: "m > max n\<^sub>1 n\<^sub>2"
   4.260 +        from P\<^sub>1 Q have *: "f m \<le> c\<^sub>1 * g m" by simp
   4.261 +        from P\<^sub>2 Q have "g m \<le> c\<^sub>2 * h m" by simp
   4.262 +        with \<open>c\<^sub>1 > 0\<close> have "c\<^sub>1 * g m \<le> (c\<^sub>1 * c\<^sub>2) * h m" by simp
   4.263 +        with * show "f m \<le> (c\<^sub>1 * c\<^sub>2) * h m" by (rule order_trans)
   4.264 +      qed
   4.265 +      then have "\<exists>n. \<forall>m>n. f m \<le> (c\<^sub>1 * c\<^sub>2) * h m" by rule
   4.266 +      moreover from \<open>c\<^sub>1 > 0\<close> \<open>c\<^sub>2 > 0\<close> have "c\<^sub>1 * c\<^sub>2 > 0" by simp
   4.267 +      ultimately show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * h m" by blast
   4.268 +    qed
   4.269 +  qed
   4.270 +  from preorder.preorder_equiv_axioms show "class.preorder_equiv less_eq_fun less_fun" .
   4.271 +  show "preorder_equiv.equiv less_eq_fun = equiv_fun"
   4.272 +  proof (rule ext, rule ext, unfold preorder.equiv_def)
   4.273 +    fix f g
   4.274 +    show "f \<lesssim> g \<and> g \<lesssim> f \<longleftrightarrow> f \<cong> g"
   4.275 +    proof
   4.276 +      assume "f \<cong> g"
   4.277 +      then obtain n c\<^sub>1 c\<^sub>2 where "c\<^sub>1 > 0" and "c\<^sub>2 > 0"
   4.278 +        and *: "\<And>m. m > n \<Longrightarrow> f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m"
   4.279 +        by (rule equiv_funE) blast
   4.280 +      have "\<forall>m>n. f m \<le> c\<^sub>1 * g m"
   4.281 +      proof (rule allI, rule impI)
   4.282 +        fix m
   4.283 +        assume "m > n"
   4.284 +        with * show "f m \<le> c\<^sub>1 * g m" by simp
   4.285 +      qed
   4.286 +      with \<open>c\<^sub>1 > 0\<close> have "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m" by blast
   4.287 +      then have "f \<lesssim> g" ..
   4.288 +      have "\<forall>m>n. g m \<le> c\<^sub>2 * f m"
   4.289 +      proof (rule allI, rule impI)
   4.290 +        fix m
   4.291 +        assume "m > n"
   4.292 +        with * show "g m \<le> c\<^sub>2 * f m" by simp
   4.293 +      qed
   4.294 +      with \<open>c\<^sub>2 > 0\<close> have "\<exists>c>0. \<exists>n. \<forall>m>n. g m \<le> c * f m" by blast
   4.295 +      then have "g \<lesssim> f" ..
   4.296 +      from \<open>f \<lesssim> g\<close> and \<open>g \<lesssim> f\<close> show "f \<lesssim> g \<and> g \<lesssim> f" ..
   4.297 +    next
   4.298 +      assume "f \<lesssim> g \<and> g \<lesssim> f"
   4.299 +      then have "f \<lesssim> g" and "g \<lesssim> f" by auto
   4.300 +      from \<open>f \<lesssim> g\<close> obtain n\<^sub>1 c\<^sub>1 where "c\<^sub>1 > 0"
   4.301 +        and P\<^sub>1: "\<And>m. m > n\<^sub>1 \<Longrightarrow> f m \<le> c\<^sub>1 * g m" by rule blast
   4.302 +      from \<open>g \<lesssim> f\<close> obtain n\<^sub>2 c\<^sub>2 where "c\<^sub>2 > 0"
   4.303 +        and P\<^sub>2: "\<And>m. m > n\<^sub>2 \<Longrightarrow> g m \<le> c\<^sub>2 * f m" by rule blast
   4.304 +      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"
   4.305 +      proof (rule allI, rule impI)
   4.306 +        fix m
   4.307 +        assume Q: "m > max n\<^sub>1 n\<^sub>2"
   4.308 +        from P\<^sub>1 Q have "f m \<le> c\<^sub>1 * g m" by simp
   4.309 +        moreover from P\<^sub>2 Q have "g m \<le> c\<^sub>2 * f m" by simp
   4.310 +        ultimately show "f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m" ..
   4.311 +      qed
   4.312 +      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.
   4.313 +        \<forall>m>n. f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m" by blast
   4.314 +      then show "f \<cong> g" by (rule equiv_funI)
   4.315 +    qed
   4.316 +  qed
   4.317 +qed
   4.318 +
   4.319 +declare fun_order.antisym [intro?]
   4.320 +
   4.321 +
   4.322 +subsection \<open>Simple examples\<close>
   4.323 +
   4.324 +text \<open>
   4.325 +  Most of these are left as constructive exercises for the reader.  Note that additional
   4.326 +  preconditions to the functions may be necessary.  The list here is by no means to be
   4.327 +  intended as complete construction set for typical functions, here surely something
   4.328 +  has to be added yet.
   4.329 +\<close>
   4.330 +
   4.331 +text \<open>@{prop "(\<lambda>n. f n + k) \<cong> f"}\<close>
   4.332 +
   4.333 +lemma equiv_fun_mono_const:
   4.334 +  assumes "mono f" and "\<exists>n. f n > 0"
   4.335 +  shows "(\<lambda>n. f n + k) \<cong> f"
   4.336 +proof (cases "k = 0")
   4.337 +  case True then show ?thesis by simp
   4.338 +next
   4.339 +  case False
   4.340 +  show ?thesis
   4.341 +  proof
   4.342 +    show "(\<lambda>n. f n + k) \<lesssim> f"
   4.343 +    proof
   4.344 +      from \<open>\<exists>n. f n > 0\<close> obtain n where "f n > 0" ..
   4.345 +      have "\<forall>m>n. f m + k \<le> Suc k * f m"
   4.346 +      proof (rule allI, rule impI)
   4.347 +        fix m
   4.348 +        assume "n < m"
   4.349 +        with \<open>mono f\<close> have "f n \<le> f m"
   4.350 +          using less_imp_le_nat monoE by blast
   4.351 +        with  \<open>0 < f n\<close> have "0 < f m" by auto
   4.352 +        then obtain l where "f m = Suc l" by (cases "f m") simp_all
   4.353 +        then show "f m + k \<le> Suc k * f m" by simp
   4.354 +      qed
   4.355 +      then show "\<exists>c>0. \<exists>n. \<forall>m>n. f m + k \<le> c * f m" by blast
   4.356 +    qed
   4.357 +    show "f \<lesssim> (\<lambda>n. f n + k)"
   4.358 +    proof
   4.359 +      have "f m \<le> 1 * (f m + k)" for m by simp
   4.360 +      then show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * (f m + k)" by blast
   4.361 +    qed
   4.362 +  qed
   4.363 +qed
   4.364 +
   4.365 +lemma
   4.366 +  assumes "strict_mono f"
   4.367 +  shows "(\<lambda>n. f n + k) \<cong> f"
   4.368 +proof (rule equiv_fun_mono_const)
   4.369 +  from assms show "mono f" by (rule strict_mono_mono)
   4.370 +  show "\<exists>n. 0 < f n"
   4.371 +  proof (rule ccontr)
   4.372 +    assume "\<not> (\<exists>n. 0 < f n)"
   4.373 +    then have "\<And>n. f n = 0" by simp
   4.374 +    then have "f 0 = f 1" by simp
   4.375 +    moreover from \<open>strict_mono f\<close> have "f 0 < f 1"
   4.376 +      by (simp add: strict_mono_def) 
   4.377 +    ultimately show False by simp
   4.378 +  qed
   4.379 +qed
   4.380 +  
   4.381 +lemma
   4.382 +  "(\<lambda>n. Suc k * f n) \<cong> f"
   4.383 +proof
   4.384 +  show "(\<lambda>n. Suc k * f n) \<lesssim> f"
   4.385 +  proof
   4.386 +    have "Suc k * f m \<le> Suc k * f m" for m by simp
   4.387 +    then show "\<exists>c>0. \<exists>n. \<forall>m>n. Suc k * f m \<le> c * f m" by blast
   4.388 +  qed
   4.389 +  show "f \<lesssim> (\<lambda>n. Suc k * f n)"
   4.390 +  proof
   4.391 +    have "f m \<le> 1 * (Suc k * f m)" for m by simp
   4.392 +    then show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * (Suc k * f m)" by blast
   4.393 +  qed
   4.394 +qed
   4.395 +
   4.396 +lemma
   4.397 +  "f \<lesssim> (\<lambda>n. f n + g n)"
   4.398 +  by rule auto
   4.399 +
   4.400 +lemma
   4.401 +  "(\<lambda>_. 0) \<prec> (\<lambda>n. Suc k)"
   4.402 +  by (rule less_fun_strongI) auto
   4.403 +
   4.404 +lemma
   4.405 +  "(\<lambda>_. k) \<prec> Discrete.log"
   4.406 +proof (rule less_fun_strongI)
   4.407 +  fix c :: nat
   4.408 +  have "\<forall>m>2 ^ (Suc (c * k)). c * k < Discrete.log m"
   4.409 +  proof (rule allI, rule impI)
   4.410 +    fix m :: nat
   4.411 +    assume "2 ^ Suc (c * k) < m"
   4.412 +    then have "2 ^ Suc (c * k) \<le> m" by simp
   4.413 +    with log_mono have "Discrete.log (2 ^ (Suc (c * k))) \<le> Discrete.log m"
   4.414 +      by (blast dest: monoD)
   4.415 +    moreover have "c * k < Discrete.log (2 ^ (Suc (c * k)))" by simp
   4.416 +    ultimately show "c * k < Discrete.log m" by auto
   4.417 +  qed
   4.418 +  then show "\<exists>n. \<forall>m>n. c * k < Discrete.log m" ..
   4.419 +qed
   4.420 +
   4.421 +(*lemma
   4.422 +  "Discrete.log \<prec> Discrete.sqrt"
   4.423 +proof (rule less_fun_strongI)*)
   4.424 +text \<open>@{prop "Discrete.log \<prec> Discrete.sqrt"}\<close>
   4.425 +
   4.426 +lemma
   4.427 +  "Discrete.sqrt \<prec> id"
   4.428 +proof (rule less_fun_strongI)
   4.429 +  fix c :: nat
   4.430 +  assume "0 < c"
   4.431 +  have "\<forall>m>(Suc c)\<^sup>2. c * Discrete.sqrt m < id m"
   4.432 +  proof (rule allI, rule impI)
   4.433 +    fix m
   4.434 +    assume "(Suc c)\<^sup>2 < m"
   4.435 +    then have "(Suc c)\<^sup>2 \<le> m" by simp
   4.436 +    with mono_sqrt have "Discrete.sqrt ((Suc c)\<^sup>2) \<le> Discrete.sqrt m" by (rule monoE)
   4.437 +    then have "Suc c \<le> Discrete.sqrt m" by simp
   4.438 +    then have "c < Discrete.sqrt m" by simp
   4.439 +    moreover from \<open>(Suc c)\<^sup>2 < m\<close> have "Discrete.sqrt m > 0" by simp
   4.440 +    ultimately have "c * Discrete.sqrt m < Discrete.sqrt m * Discrete.sqrt m" by simp
   4.441 +    also have "\<dots> \<le> m" by (simp add: power2_eq_square [symmetric])
   4.442 +    finally show "c * Discrete.sqrt m < id m" by simp
   4.443 +  qed
   4.444 +  then show "\<exists>n. \<forall>m>n. c * Discrete.sqrt m < id m" ..
   4.445 +qed
   4.446 +
   4.447 +lemma
   4.448 +  "id \<prec> (\<lambda>n. n\<^sup>2)"
   4.449 +  by (rule less_fun_strongI) (auto simp add: power2_eq_square)
   4.450 +
   4.451 +lemma
   4.452 +  "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. n ^ Suc k)"
   4.453 +  by (rule less_fun_strongI) auto
   4.454 +
   4.455 +(*lemma 
   4.456 +  "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. 2 ^ n)"
   4.457 +proof (rule less_fun_strongI)*)
   4.458 +text \<open>@{prop "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. 2 ^ n)"}\<close>
   4.459 +
   4.460 +end