diff -r ea9b2e5ca9fc -r 9c9baae29217 src/HOL/Library/Function_Growth.thy --- a/src/HOL/Library/Function_Growth.thy Sun Oct 08 22:28:19 2017 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,454 +0,0 @@ - -(* Author: Florian Haftmann, TU Muenchen *) - -section \Comparing growth of functions on natural numbers by a preorder relation\ - -theory Function_Growth -imports Main Preorder Discrete -begin - -(* FIXME move *) - -context linorder -begin - -lemma mono_invE: - fixes f :: "'a \ 'b::order" - assumes "mono f" - assumes "f x < f y" - obtains "x < y" -proof - show "x < y" - proof (rule ccontr) - assume "\ x < y" - then have "y \ x" by simp - with \mono f\ obtain "f y \ f x" by (rule monoE) - with \f x < f y\ show False by simp - qed -qed - -end - -lemma (in semidom_divide) power_diff: - fixes a :: 'a - assumes "a \ 0" - assumes "m \ n" - shows "a ^ (m - n) = (a ^ m) div (a ^ n)" -proof - - define q where "q = m - n" - with assms have "m = q + n" by (simp add: q_def) - with q_def show ?thesis using \a \ 0\ by (simp add: power_add) -qed - - -subsection \Motivation\ - -text \ - When comparing growth of functions in computer science, it is common to adhere - on Landau Symbols (O-Notation''). However these come at the cost of notational - oddities, particularly writing \f = O(g)\ for \f \ O(g)\ etc. - - Here we suggest a different way, following Hardy (G.~H.~Hardy and J.~E.~Littlewood, - Some problems of Diophantine approximation, Acta Mathematica 37 (1914), p.~225). - We establish a quasi order relation \\\ on functions such that - \f \ g \ f \ O(g)\. From a didactic point of view, this does not only - avoid the notational oddities mentioned above but also emphasizes the key insight - of a growth hierarchy of functions: - $$\n. 0) \ (\n. k) \ Discrete.log \ Discrete.sqrt \ id \ \\. -\ - -subsection \Model\ - -text \ - Our growth functions are of type \\ \ \\. This is different - to the usual conventions for Landau symbols for which \\ \ \\ - would be appropriate, but we argue that \\ \ \\ is more - appropriate for analysis, whereas our setting is discrete. - - Note that we also restrict the additional coefficients to \\\, something - we discuss at the particular definitions. -\ - -subsection \The \\\ relation\ - -definition less_eq_fun :: "(nat \ nat) \ (nat \ nat) \ bool" (infix "\" 50) -where - "f \ g \ (\c>0. \n. \m>n. f m \ c * g m)" - -text \ - This yields \f \ g \ f \ O(g)\. Note that \c\ is restricted to - \\\. This does not pose any problems since if \f \ O(g)\ holds for - a \c \ \\, it also holds for \\c\ \ \\ by transitivity. -\ - -lemma less_eq_funI [intro?]: - assumes "\c>0. \n. \m>n. f m \ c * g m" - shows "f \ g" - unfolding less_eq_fun_def by (rule assms) - -lemma not_less_eq_funI: - assumes "\c n. c > 0 \ \m>n. c * g m < f m" - shows "\ f \ g" - using assms unfolding less_eq_fun_def linorder_not_le [symmetric] by blast - -lemma less_eq_funE [elim?]: - assumes "f \ g" - obtains n c where "c > 0" and "\m. m > n \ f m \ c * g m" - using assms unfolding less_eq_fun_def by blast - -lemma not_less_eq_funE: - assumes "\ f \ g" and "c > 0" - obtains m where "m > n" and "c * g m < f m" - using assms unfolding less_eq_fun_def linorder_not_le [symmetric] by blast - - -subsection \The \\\ relation, the equivalence relation induced by \\\\ - -definition equiv_fun :: "(nat \ nat) \ (nat \ nat) \ bool" (infix "\" 50) -where - "f \ g \ - (\c\<^sub>1>0. \c\<^sub>2>0. \n. \m>n. f m \ c\<^sub>1 * g m \ g m \ c\<^sub>2 * f m)" - -text \ - This yields \f \ g \ f \ \(g)\. Concerning \c\<^sub>1\ and \c\<^sub>2\ - restricted to @{typ nat}, see note above on \($$\. -\ - -lemma equiv_funI: - assumes "\c\<^sub>1>0. \c\<^sub>2>0. \n. \m>n. f m \ c\<^sub>1 * g m \ g m \ c\<^sub>2 * f m" - shows "f \ g" - unfolding equiv_fun_def by (rule assms) - -lemma not_equiv_funI: - assumes "\c\<^sub>1 c\<^sub>2 n. c\<^sub>1 > 0 \ c\<^sub>2 > 0 \ - \m>n. c\<^sub>1 * f m < g m \ c\<^sub>2 * g m < f m" - shows "\ f \ g" - using assms unfolding equiv_fun_def linorder_not_le [symmetric] by blast - -lemma equiv_funE: - assumes "f \ g" - obtains n c\<^sub>1 c\<^sub>2 where "c\<^sub>1 > 0" and "c\<^sub>2 > 0" - and "\m. m > n \ f m \ c\<^sub>1 * g m \ g m \ c\<^sub>2 * f m" - using assms unfolding equiv_fun_def by blast - -lemma not_equiv_funE: - fixes n c\<^sub>1 c\<^sub>2 - assumes "\ f \ g" and "c\<^sub>1 > 0" and "c\<^sub>2 > 0" - obtains m where "m > n" - and "c\<^sub>1 * f m < g m \ c\<^sub>2 * g m < f m" - using assms unfolding equiv_fun_def linorder_not_le [symmetric] by blast - - -subsection \The \\\ relation, the strict part of \\\\ - -definition less_fun :: "(nat \ nat) \ (nat \ nat) \ bool" (infix "\" 50) -where - "f \ g \ f \ g \ \ g \ f" - -lemma less_funI: - assumes "\c>0. \n. \m>n. f m \ c * g m" - and "\c n. c > 0 \ \m>n. c * f m < g m" - shows "f \ g" - using assms unfolding less_fun_def less_eq_fun_def linorder_not_less [symmetric] by blast - -lemma not_less_funI: - assumes "\c n. c > 0 \ \m>n. c * g m < f m" - and "\c>0. \n. \m>n. g m \ c * f m" - shows "\ f \ g" - using assms unfolding less_fun_def less_eq_fun_def linorder_not_less [symmetric] by blast - -lemma less_funE [elim?]: - assumes "f \ g" - obtains n c where "c > 0" and "\m. m > n \ f m \ c * g m" - and "\c n. c > 0 \ \m>n. c * f m < g m" -proof - - from assms have "f \ g" and "\ g \ f" by (simp_all add: less_fun_def) - from \f \ g\ obtain n c where *:"c > 0" "m > n \ f m \ c * g m" for m - by (rule less_eq_funE) blast - { fix c n :: nat - assume "c > 0" - with \\ g \ f\ obtain m where "m > n" "c * f m < g m" - by (rule not_less_eq_funE) blast - then have **: "\m>n. c * f m < g m" by blast - } note ** = this - from * ** show thesis by (rule that) -qed - -lemma not_less_funE: - assumes "\ f \ g" and "c > 0" - obtains m where "m > n" and "c * g m < f m" - | d q where "\m. d > 0 \ m > q \ g q \ d * f q" - using assms unfolding less_fun_def linorder_not_less [symmetric] by blast - -text \ - I did not find a proof for \f \ g \ f \ o(g)\. Maybe this only - holds if \f\ and/or \g\ are of a certain class of functions. - However \f \ o(g) \ f \ g\ is provable, and this yields a - handy introduction rule. - - Note that D. Knuth ignores \o\ altogether. So what \dots - - Something still has to be said about the coefficient \c\ in - the definition of \. In the typical definition of \o\, - it occurs on the \emph{right} hand side of the \(>)\. The reason - is that the situation is dual to the definition of \O\: the definition - works since \c\ may become arbitrary small. Since this is not possible - within @{term \}, we push the coefficient to the left hand side instead such - that it may become arbitrary big instead. -\ - -lemma less_fun_strongI: - assumes "\c. c > 0 \ \n. \m>n. c * f m < g m" - shows "f \ g" -proof (rule less_funI) - have "1 > (0::nat)" by simp - with assms [OF this] obtain n where *: "m > n \ 1 * f m < g m" for m - by blast - have "\m>n. f m \ 1 * g m" - proof (rule allI, rule impI) - fix m - assume "m > n" - with * have "1 * f m < g m" by simp - then show "f m \ 1 * g m" by simp - qed - with \1 > 0\ show "\c>0. \n. \m>n. f m \ c * g m" by blast - fix c n :: nat - assume "c > 0" - with assms obtain q where "m > q \ c * f m < g m" for m by blast - then have "c * f (Suc (q + n)) < g (Suc (q + n))" by simp - moreover have "Suc (q + n) > n" by simp - ultimately show "\m>n. c * f m < g m" by blast -qed - - -subsection \\\\ is a preorder\ - -text \This yields all lemmas relating \\\, \\\ and \\\.\ - -interpretation fun_order: preorder_equiv less_eq_fun less_fun - rewrites "fun_order.equiv = equiv_fun" -proof - - interpret preorder: preorder_equiv less_eq_fun less_fun - proof - fix f g h - show "f \ f" - proof - have "\n. \m>n. f m \ 1 * f m" by auto - then show "\c>0. \n. \m>n. f m \ c * f m" by blast - qed - show "f \ g \ f \ g \ \ g \ f" - by (fact less_fun_def) - assume "f \ g" and "g \ h" - show "f \ h" - proof - from \f \ g\ obtain n\<^sub>1 c\<^sub>1 - where "c\<^sub>1 > 0" and P\<^sub>1: "\m. m > n\<^sub>1 \ f m \ c\<^sub>1 * g m" - by rule blast - from \g \ h\ obtain n\<^sub>2 c\<^sub>2 - where "c\<^sub>2 > 0" and P\<^sub>2: "\m. m > n\<^sub>2 \ g m \ c\<^sub>2 * h m" - by rule blast - have "\m>max n\<^sub>1 n\<^sub>2. f m \ (c\<^sub>1 * c\<^sub>2) * h m" - proof (rule allI, rule impI) - fix m - assume Q: "m > max n\<^sub>1 n\<^sub>2" - from P\<^sub>1 Q have *: "f m \ c\<^sub>1 * g m" by simp - from P\<^sub>2 Q have "g m \ c\<^sub>2 * h m" by simp - with \c\<^sub>1 > 0\ have "c\<^sub>1 * g m \ (c\<^sub>1 * c\<^sub>2) * h m" by simp - with * show "f m \ (c\<^sub>1 * c\<^sub>2) * h m" by (rule order_trans) - qed - then have "\n. \m>n. f m \ (c\<^sub>1 * c\<^sub>2) * h m" by rule - moreover from \c\<^sub>1 > 0\ \c\<^sub>2 > 0\ have "c\<^sub>1 * c\<^sub>2 > 0" by simp - ultimately show "\c>0. \n. \m>n. f m \ c * h m" by blast - qed - qed - from preorder.preorder_equiv_axioms show "class.preorder_equiv less_eq_fun less_fun" . - show "preorder_equiv.equiv less_eq_fun = equiv_fun" - proof (rule ext, rule ext, unfold preorder.equiv_def) - fix f g - show "f \ g \ g \ f \ f \ g" - proof - assume "f \ g" - then obtain n c\<^sub>1 c\<^sub>2 where "c\<^sub>1 > 0" and "c\<^sub>2 > 0" - and *: "\m. m > n \ f m \ c\<^sub>1 * g m \ g m \ c\<^sub>2 * f m" - by (rule equiv_funE) blast - have "\m>n. f m \ c\<^sub>1 * g m" - proof (rule allI, rule impI) - fix m - assume "m > n" - with * show "f m \ c\<^sub>1 * g m" by simp - qed - with \c\<^sub>1 > 0\ have "\c>0. \n. \m>n. f m \ c * g m" by blast - then have "f \ g" .. - have "\m>n. g m \ c\<^sub>2 * f m" - proof (rule allI, rule impI) - fix m - assume "m > n" - with * show "g m \ c\<^sub>2 * f m" by simp - qed - with \c\<^sub>2 > 0\ have "\c>0. \n. \m>n. g m \ c * f m" by blast - then have "g \ f" .. - from \f \ g\ and \g \ f\ show "f \ g \ g \ f" .. - next - assume "f \ g \ g \ f" - then have "f \ g" and "g \ f" by auto - from \f \ g\ obtain n\<^sub>1 c\<^sub>1 where "c\<^sub>1 > 0" - and P\<^sub>1: "\m. m > n\<^sub>1 \ f m \ c\<^sub>1 * g m" by rule blast - from \g \ f\ obtain n\<^sub>2 c\<^sub>2 where "c\<^sub>2 > 0" - and P\<^sub>2: "\m. m > n\<^sub>2 \ g m \ c\<^sub>2 * f m" by rule blast - have "\m>max n\<^sub>1 n\<^sub>2. f m \ c\<^sub>1 * g m \ g m \ c\<^sub>2 * f m" - proof (rule allI, rule impI) - fix m - assume Q: "m > max n\<^sub>1 n\<^sub>2" - from P\<^sub>1 Q have "f m \ c\<^sub>1 * g m" by simp - moreover from P\<^sub>2 Q have "g m \ c\<^sub>2 * f m" by simp - ultimately show "f m \ c\<^sub>1 * g m \ g m \ c\<^sub>2 * f m" .. - qed - with \c\<^sub>1 > 0\ \c\<^sub>2 > 0\ have "\c\<^sub>1>0. \c\<^sub>2>0. \n. - \m>n. f m \ c\<^sub>1 * g m \ g m \ c\<^sub>2 * f m" by blast - then show "f \ g" by (rule equiv_funI) - qed - qed -qed - -declare fun_order.antisym [intro?] - - -subsection \Simple examples\ - -text \ - Most of these are left as constructive exercises for the reader. Note that additional - preconditions to the functions may be necessary. The list here is by no means to be - intended as complete construction set for typical functions, here surely something - has to be added yet. -\ - -text \@{prop "(\n. f n + k) \ f"}\ - -lemma equiv_fun_mono_const: - assumes "mono f" and "\n. f n > 0" - shows "(\n. f n + k) \ f" -proof (cases "k = 0") - case True then show ?thesis by simp -next - case False - show ?thesis - proof - show "(\n. f n + k) \ f" - proof - from \\n. f n > 0\ obtain n where "f n > 0" .. - have "\m>n. f m + k \ Suc k * f m" - proof (rule allI, rule impI) - fix m - assume "n < m" - with \mono f\ have "f n \ f m" - using less_imp_le_nat monoE by blast - with \0 < f n\ have "0 < f m" by auto - then obtain l where "f m = Suc l" by (cases "f m") simp_all - then show "f m + k \ Suc k * f m" by simp - qed - then show "\c>0. \n. \m>n. f m + k \ c * f m" by blast - qed - show "f \ (\n. f n + k)" - proof - have "f m \ 1 * (f m + k)" for m by simp - then show "\c>0. \n. \m>n. f m \ c * (f m + k)" by blast - qed - qed -qed - -lemma - assumes "strict_mono f" - shows "(\n. f n + k) \ f" -proof (rule equiv_fun_mono_const) - from assms show "mono f" by (rule strict_mono_mono) - show "\n. 0 < f n" - proof (rule ccontr) - assume "\ (\n. 0 < f n)" - then have "\n. f n = 0" by simp - then have "f 0 = f 1" by simp - moreover from \strict_mono f\ have "f 0 < f 1" - by (simp add: strict_mono_def) - ultimately show False by simp - qed -qed - -lemma - "(\n. Suc k * f n) \ f" -proof - show "(\n. Suc k * f n) \ f" - proof - have "Suc k * f m \ Suc k * f m" for m by simp - then show "\c>0. \n. \m>n. Suc k * f m \ c * f m" by blast - qed - show "f \ (\n. Suc k * f n)" - proof - have "f m \ 1 * (Suc k * f m)" for m by simp - then show "\c>0. \n. \m>n. f m \ c * (Suc k * f m)" by blast - qed -qed - -lemma - "f \ (\n. f n + g n)" - by rule auto - -lemma - "(\_. 0) \ (\n. Suc k)" - by (rule less_fun_strongI) auto - -lemma - "(\_. k) \ Discrete.log" -proof (rule less_fun_strongI) - fix c :: nat - have "\m>2 ^ (Suc (c * k)). c * k < Discrete.log m" - proof (rule allI, rule impI) - fix m :: nat - assume "2 ^ Suc (c * k) < m" - then have "2 ^ Suc (c * k) \ m" by simp - with log_mono have "Discrete.log (2 ^ (Suc (c * k))) \ Discrete.log m" - by (blast dest: monoD) - moreover have "c * k < Discrete.log (2 ^ (Suc (c * k)))" by simp - ultimately show "c * k < Discrete.log m" by auto - qed - then show "\n. \m>n. c * k < Discrete.log m" .. -qed - -(*lemma - "Discrete.log \ Discrete.sqrt" -proof (rule less_fun_strongI)*) -text \@{prop "Discrete.log \ Discrete.sqrt"}\ - -lemma - "Discrete.sqrt \ id" -proof (rule less_fun_strongI) - fix c :: nat - assume "0 < c" - have "\m>(Suc c)\<^sup>2. c * Discrete.sqrt m < id m" - proof (rule allI, rule impI) - fix m - assume "(Suc c)\<^sup>2 < m" - then have "(Suc c)\<^sup>2 \ m" by simp - with mono_sqrt have "Discrete.sqrt ((Suc c)\<^sup>2) \ Discrete.sqrt m" by (rule monoE) - then have "Suc c \ Discrete.sqrt m" by simp - then have "c < Discrete.sqrt m" by simp - moreover from \(Suc c)\<^sup>2 < m\ have "Discrete.sqrt m > 0" by simp - ultimately have "c * Discrete.sqrt m < Discrete.sqrt m * Discrete.sqrt m" by simp - also have "\ \ m" by (simp add: power2_eq_square [symmetric]) - finally show "c * Discrete.sqrt m < id m" by simp - qed - then show "\n. \m>n. c * Discrete.sqrt m < id m" .. -qed - -lemma - "id \ (\n. n\<^sup>2)" - by (rule less_fun_strongI) (auto simp add: power2_eq_square) - -lemma - "(\n. n ^ k) \ (\n. n ^ Suc k)" - by (rule less_fun_strongI) auto - -(*lemma - "(\n. n ^ k) \ (\n. 2 ^ n)" -proof (rule less_fun_strongI)*) -text \@{prop "(\n. n ^ k) \ (\n. 2 ^ n)"}\ - -end