--- a/src/HOL/Library/Discrete.thy Thu Dec 10 21:39:33 2015 +0100
+++ b/src/HOL/Library/Discrete.thy Fri Dec 11 11:31:57 2015 +0100
@@ -14,6 +14,28 @@
qualified fun log :: "nat \<Rightarrow> nat"
where [simp del]: "log n = (if n < 2 then 0 else Suc (log (n div 2)))"
+lemma log_induct [consumes 1, case_names one double]:
+ fixes n :: nat
+ assumes "n > 0"
+ assumes one: "P 1"
+ assumes double: "\<And>n. n \<ge> 2 \<Longrightarrow> P (n div 2) \<Longrightarrow> P n"
+ shows "P n"
+using `n > 0` proof (induct n rule: log.induct)
+ fix n
+ assume "\<not> n < 2 \<Longrightarrow>
+ 0 < n div 2 \<Longrightarrow> P (n div 2)"
+ then have *: "n \<ge> 2 \<Longrightarrow> P (n div 2)" by simp
+ assume "n > 0"
+ show "P n"
+ proof (cases "n = 1")
+ case True with one show ?thesis by simp
+ next
+ case False with `n > 0` have "n \<ge> 2" by auto
+ moreover with * have "P (n div 2)" .
+ ultimately show ?thesis by (rule double)
+ qed
+qed
+
lemma log_zero [simp]: "log 0 = 0"
by (simp add: log.simps)
@@ -51,22 +73,41 @@
case (1 m)
then have mn2: "m div 2 \<le> n div 2" by arith
show "log m \<le> log n"
- proof (cases "m < 2")
- case True
+ proof (cases "m \<ge> 2")
+ case False
then have "m = 0 \<or> m = 1" by arith
then show ?thesis by (auto simp del: One_nat_def)
next
- case False
- with mn2 have "m \<ge> 2" and "n \<ge> 2" by auto arith
- from False have m2_0: "m div 2 \<noteq> 0" by arith
+ case True then have "\<not> m < 2" by simp
+ with mn2 have "n \<ge> 2" by arith
+ from True have m2_0: "m div 2 \<noteq> 0" by arith
with mn2 have n2_0: "n div 2 \<noteq> 0" by arith
- from False "1.hyps" mn2 have "log (m div 2) \<le> log (n div 2)" by blast
+ from `\<not> m < 2` "1.hyps" mn2 have "log (m div 2) \<le> log (n div 2)" by blast
with m2_0 n2_0 have "log (2 * (m div 2)) \<le> log (2 * (n div 2))" by simp
with m2_0 n2_0 \<open>m \<ge> 2\<close> \<open>n \<ge> 2\<close> show ?thesis by (simp only: log_rec [of m] log_rec [of n]) simp
qed
qed
qed
+lemma log_exp2_le:
+ assumes "n > 0"
+ shows "2 ^ log n \<le> n"
+using assms proof (induct n rule: log_induct)
+ show "2 ^ log 1 \<le> (1 :: nat)" by simp
+next
+ fix n :: nat
+ assume "n \<ge> 2"
+ with log_mono have "log n \<ge> Suc 0"
+ by (simp add: log.simps)
+ assume "2 ^ log (n div 2) \<le> n div 2"
+ with `n \<ge> 2` have "2 ^ (log n - Suc 0) \<le> n div 2" by simp
+ then have "2 ^ (log n - Suc 0) * 2 ^ 1 \<le> n div 2 * 2" by simp
+ with `log n \<ge> Suc 0` have "2 ^ log n \<le> n div 2 * 2"
+ unfolding power_add [symmetric] by simp
+ also have "n div 2 * 2 \<le> n" by (cases "even n") simp_all
+ finally show "2 ^ log n \<le> n" .
+qed
+
subsection \<open>Discrete square root\<close>
--- a/src/HOL/Library/Function_Growth.thy Thu Dec 10 21:39:33 2015 +0100
+++ b/src/HOL/Library/Function_Growth.thy Fri Dec 11 11:31:57 2015 +0100
@@ -7,6 +7,40 @@
imports Main Preorder Discrete
begin
+(* FIXME move *)
+
+context linorder
+begin
+
+lemma mono_invE:
+ fixes f :: "'a \<Rightarrow> 'b::order"
+ assumes "mono f"
+ assumes "f x < f y"
+ obtains "x < y"
+proof
+ show "x < y"
+ proof (rule ccontr)
+ assume "\<not> x < y"
+ then have "y \<le> x" by simp
+ with \<open>mono f\<close> obtain "f y \<le> f x" by (rule monoE)
+ with \<open>f x < f y\<close> show False by simp
+ qed
+qed
+
+end
+
+lemma (in semidom_divide) power_diff:
+ fixes a :: 'a
+ assumes "a \<noteq> 0"
+ assumes "m \<ge> n"
+ shows "a ^ (m - n) = (a ^ m) div (a ^ n)"
+proof -
+ def q == "m - n"
+ moreover with assms have "m = q + n" by (simp add: q_def)
+ ultimately show ?thesis using `a \<noteq> 0` by (simp add: power_add)
+qed
+
+
subsection \<open>Motivation\<close>
text \<open>
@@ -80,7 +114,7 @@
restricted to @{typ nat}, see note above on \<open>(\<lesssim>)\<close>.
\<close>
-lemma equiv_funI [intro?]:
+lemma equiv_funI:
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"
shows "f \<cong> g"
unfolding equiv_fun_def by (rule assms)
@@ -91,7 +125,7 @@
shows "\<not> f \<cong> g"
using assms unfolding equiv_fun_def linorder_not_le [symmetric] by blast
-lemma equiv_funE [elim?]:
+lemma equiv_funE:
assumes "f \<cong> g"
obtains n c\<^sub>1 c\<^sub>2 where "c\<^sub>1 > 0" and "c\<^sub>2 > 0"
and "\<And>m. m > n \<Longrightarrow> f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m"
@@ -160,7 +194,7 @@
is that the situation is dual to the definition of \<open>O\<close>: the definition
works since \<open>c\<close> may become arbitrary small. Since this is not possible
within @{term \<nat>}, we push the coefficient to the left hand side instead such
- that it become arbitrary big instead.
+ that it may become arbitrary big instead.
\<close>
lemma less_fun_strongI:
@@ -192,7 +226,7 @@
text \<open>This yields all lemmas relating \<open>\<lesssim>\<close>, \<open>\<prec>\<close> and \<open>\<cong>\<close>.\<close>
interpretation fun_order: preorder_equiv less_eq_fun less_fun
- rewrites "preorder_equiv.equiv less_eq_fun = equiv_fun"
+ rewrites "fun_order.equiv = equiv_fun"
proof -
interpret preorder: preorder_equiv less_eq_fun less_fun
proof
@@ -236,7 +270,7 @@
assume "f \<cong> g"
then obtain n c\<^sub>1 c\<^sub>2 where "c\<^sub>1 > 0" and "c\<^sub>2 > 0"
and *: "\<And>m. m > n \<Longrightarrow> f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m"
- by rule blast
+ by (rule equiv_funE) blast
have "\<forall>m>n. f m \<le> c\<^sub>1 * g m"
proof (rule allI, rule impI)
fix m
@@ -271,11 +305,13 @@
qed
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.
\<forall>m>n. f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m" by blast
- then show "f \<cong> g" ..
+ then show "f \<cong> g" by (rule equiv_funI)
qed
qed
qed
+declare fun_order.antisym [intro?]
+
subsection \<open>Simple examples\<close>
@@ -288,15 +324,79 @@
text \<open>@{prop "(\<lambda>n. f n + k) \<cong> f"}\<close>
-text \<open>@{prop "(\<lambda>n. Suc k * f n) \<cong> f"}\<close>
+lemma equiv_fun_mono_const:
+ assumes "mono f" and "\<exists>n. f n > 0"
+ shows "(\<lambda>n. f n + k) \<cong> f"
+proof (cases "k = 0")
+ case True then show ?thesis by simp
+next
+ case False
+ show ?thesis
+ proof
+ show "(\<lambda>n. f n + k) \<lesssim> f"
+ proof
+ from `\<exists>n. f n > 0` obtain n where "f n > 0" ..
+ have "\<forall>m>n. f m + k \<le> Suc k * f m"
+ proof (rule allI, rule impI)
+ fix m
+ assume "n < m"
+ with `mono f` have "f n \<le> 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 \<le> Suc k * f m" by simp
+ qed
+ then show "\<exists>c>0. \<exists>n. \<forall>m>n. f m + k \<le> c * f m" by blast
+ qed
+ show "f \<lesssim> (\<lambda>n. f n + k)"
+ proof
+ have "f m \<le> 1 * (f m + k)" for m by simp
+ then show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * (f m + k)" by blast
+ qed
+ qed
+qed
-lemma "f \<lesssim> (\<lambda>n. f n + g n)"
+lemma
+ assumes "strict_mono f"
+ shows "(\<lambda>n. f n + k) \<cong> f"
+proof (rule equiv_fun_mono_const)
+ from assms show "mono f" by (rule strict_mono_mono)
+ show "\<exists>n. 0 < f n"
+ proof (rule ccontr)
+ assume "\<not> (\<exists>n. 0 < f n)"
+ then have "\<And>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
+ "(\<lambda>n. Suc k * f n) \<cong> f"
+proof
+ show "(\<lambda>n. Suc k * f n) \<lesssim> f"
+ proof
+ have "Suc k * f m \<le> Suc k * f m" for m by simp
+ then show "\<exists>c>0. \<exists>n. \<forall>m>n. Suc k * f m \<le> c * f m" by blast
+ qed
+ show "f \<lesssim> (\<lambda>n. Suc k * f n)"
+ proof
+ have "f m \<le> 1 * (Suc k * f m)" for m by simp
+ then show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * (Suc k * f m)" by blast
+ qed
+qed
+
+lemma
+ "f \<lesssim> (\<lambda>n. f n + g n)"
by rule auto
-lemma "(\<lambda>_. 0) \<prec> (\<lambda>n. Suc k)"
+lemma
+ "(\<lambda>_. 0) \<prec> (\<lambda>n. Suc k)"
by (rule less_fun_strongI) auto
-lemma "(\<lambda>_. k) \<prec> Discrete.log"
+lemma
+ "(\<lambda>_. k) \<prec> Discrete.log"
proof (rule less_fun_strongI)
fix c :: nat
have "\<forall>m>2 ^ (Suc (c * k)). c * k < Discrete.log m"
@@ -311,10 +411,14 @@
qed
then show "\<exists>n. \<forall>m>n. c * k < Discrete.log m" ..
qed
-
+
+(*lemma
+ "Discrete.log \<prec> Discrete.sqrt"
+proof (rule less_fun_strongI)*)
text \<open>@{prop "Discrete.log \<prec> Discrete.sqrt"}\<close>
-lemma "Discrete.sqrt \<prec> id"
+lemma
+ "Discrete.sqrt \<prec> id"
proof (rule less_fun_strongI)
fix c :: nat
assume "0 < c"
@@ -334,13 +438,17 @@
then show "\<exists>n. \<forall>m>n. c * Discrete.sqrt m < id m" ..
qed
-lemma "id \<prec> (\<lambda>n. n\<^sup>2)"
+lemma
+ "id \<prec> (\<lambda>n. n\<^sup>2)"
by (rule less_fun_strongI) (auto simp add: power2_eq_square)
-lemma "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. n ^ Suc k)"
+lemma
+ "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. n ^ Suc k)"
by (rule less_fun_strongI) auto
+(*lemma
+ "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. 2 ^ n)"
+proof (rule less_fun_strongI)*)
text \<open>@{prop "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. 2 ^ n)"}\<close>
end
-