# HG changeset patch
# User haftmann
# Date 1449829917 -3600
# Node ID c43f87119d80578a5e1c1c2ee6eb1f770649fb8e
# Parent  4f5ab843cf5b573ebbf78ccdb8ad39c1a48a46f3
modernized

diff -r 4f5ab843cf5b -r c43f87119d80 src/HOL/Library/Discrete.thy
--- 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>
 
diff -r 4f5ab843cf5b -r c43f87119d80 src/HOL/Library/Function_Growth.thy
--- 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
-