author wenzelm Mon, 25 Feb 2013 20:11:42 +0100 changeset 51264 aba03f0c6254 parent 51263 31e786e0e6a7 child 51277 546a9a1c315d
fixed document;
```--- a/src/HOL/Library/Function_Growth.thy	Sun Feb 24 20:29:13 2013 +0100
+++ b/src/HOL/Library/Function_Growth.thy	Mon Feb 25 20:11:42 2013 +0100
@@ -11,7 +11,7 @@

text {*
When comparing growth of functions in computer science, it is common to adhere
-  on Landau Symbols (\<guillemotright>O-Notation\<guillemotleft>).  However these come at the cost of notational
+  on Landau Symbols (``O-Notation'').  However these come at the cost of notational
oddities, particularly writing @{text "f = O(g)"} for @{text "f \<in> O(g)"} etc.

Here we suggest a diffent way, following Hardy (G.~H.~Hardy and J.~E.~Littlewood,
@@ -152,7 +152,7 @@
However @{text "f \<in> o(g) \<longrightarrow> f \<prec> g"} is provable, and this yields a
handy introduction rule.

-  Note that D. Knuth ignores @{text o} altogether.  So what\<dots>
+  Note that D. Knuth ignores @{text o} altogether.  So what \dots

Something still has to be said about the coefficient @{text c} in
the definition of @{text "(\<prec>)"}.  In the typical definition of @{text o},
@@ -291,10 +291,10 @@
text {* @{prop "(\<lambda>n. Suc k * f n) \<cong> f"} *}

lemma "f \<lesssim> (\<lambda>n. f n + g n)"
-by rule auto
+  by rule auto

lemma "(\<lambda>_. 0) \<prec> (\<lambda>n. Suc k)"
-by (rule less_fun_strongI) auto
+  by (rule less_fun_strongI) auto

lemma "(\<lambda>_. k) \<prec> Discrete.log"
proof (rule less_fun_strongI)
@@ -335,10 +335,10 @@
qed

lemma "id \<prec> (\<lambda>n. n\<twosuperior>)"
-by (rule less_fun_strongI) (auto simp add: power2_eq_square)
+  by (rule less_fun_strongI) (auto simp add: power2_eq_square)

lemma "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. n ^ Suc k)"
-by (rule less_fun_strongI) auto
+  by (rule less_fun_strongI) auto

text {* @{prop "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. 2 ^ n)"} *}
```