moved lemmas
authornipkow
Thu Oct 06 11:38:05 2016 +0200 (2016-10-06)
changeset 6406540d440b75b00
parent 64019 b8f8fe506585
child 64066 666c7475f4f7
moved lemmas
src/HOL/Data_Structures/Balance.thy
src/HOL/Power.thy
     1.1 --- a/src/HOL/Data_Structures/Balance.thy	Wed Oct 05 21:27:21 2016 +0200
     1.2 +++ b/src/HOL/Data_Structures/Balance.thy	Thu Oct 06 11:38:05 2016 +0200
     1.3 @@ -11,9 +11,10 @@
     1.4  (* mv *)
     1.5  
     1.6  text \<open>The lemmas about \<open>floor\<close> and \<open>ceiling\<close> of \<open>log 2\<close> should be generalized
     1.7 -from 2 to \<open>n\<close> and should be made executable. \<close>
     1.8 +from 2 to \<open>n\<close> and should be made executable. In the end they should be moved
     1.9 +to theory \<open>Log_Nat\<close> and \<open>floorlog\<close> should be replaced.\<close>
    1.10  
    1.11 -lemma floor_log_nat: fixes b n k :: nat
    1.12 +lemma floor_log_nat_ivl: fixes b n k :: nat
    1.13  assumes "b \<ge> 2" "b^n \<le> k" "k < b^(n+1)"
    1.14  shows "floor (log b (real k)) = int(n)"
    1.15  proof -
    1.16 @@ -32,7 +33,7 @@
    1.17    qed
    1.18  qed
    1.19  
    1.20 -lemma ceil_log_nat: fixes b n k :: nat
    1.21 +lemma ceil_log_nat_ivl: fixes b n k :: nat
    1.22  assumes "b \<ge> 2" "b^n < k" "k \<le> b^(n+1)"
    1.23  shows "ceiling (log b (real k)) = int(n)+1"
    1.24  proof(rule ceiling_eq)
    1.25 @@ -47,47 +48,6 @@
    1.26      using assms(1,2) by(simp add: log_le_iff add_ac)
    1.27  qed
    1.28  
    1.29 -lemma ex_power_ivl1: fixes b k :: nat assumes "b \<ge> 2"
    1.30 -shows "k \<ge> 1 \<Longrightarrow> \<exists>n. b^n \<le> k \<and> k < b^(n+1)" (is "_ \<Longrightarrow> \<exists>n. ?P k n")
    1.31 -proof(induction k)
    1.32 -  case 0 thus ?case by simp
    1.33 -next
    1.34 -  case (Suc k)
    1.35 -  show ?case
    1.36 -  proof cases
    1.37 -    assume "k=0"
    1.38 -    hence "?P (Suc k) 0"
    1.39 -      using assms by simp
    1.40 -    thus ?case ..
    1.41 -  next
    1.42 -    assume "k\<noteq>0"
    1.43 -    with Suc obtain n where IH: "?P k n" by auto
    1.44 -    show ?case
    1.45 -    proof (cases "k = b^(n+1) - 1")
    1.46 -      case True
    1.47 -      hence "?P (Suc k) (n+1)" using assms
    1.48 -        by (simp add: not_less_eq_eq[symmetric])
    1.49 -      thus ?thesis ..
    1.50 -    next
    1.51 -      case False
    1.52 -      hence "?P (Suc k) n" using IH by auto
    1.53 -      thus ?thesis ..
    1.54 -    qed
    1.55 -  qed
    1.56 -qed
    1.57 -
    1.58 -lemma ex_power_ivl2: fixes b k :: nat assumes "b \<ge> 2" "(k::nat) \<ge> 2"
    1.59 -shows "\<exists>n. b^n < k \<and> k \<le> b^(n+1)"
    1.60 -proof -
    1.61 -  have "1 \<le> k - 1"
    1.62 -    using assms(2) by arith
    1.63 -  from ex_power_ivl1[OF assms(1) this]
    1.64 -  obtain n where "b ^ n \<le> k - 1 \<and> k - 1 < b ^ (n + 1)" ..
    1.65 -  hence "b^n < k \<and> k \<le> b^(n+1)"
    1.66 -    using assms by auto
    1.67 -  thus ?thesis ..
    1.68 -qed
    1.69 -
    1.70  lemma ceil_log2_div2: assumes "n \<ge> 2"
    1.71  shows "ceiling(log 2 (real n)) = ceiling(log 2 ((n-1) div 2 + 1)) + 1"
    1.72  proof cases
    1.73 @@ -107,7 +67,7 @@
    1.74    finally have *: "n \<le> \<dots>" .
    1.75    have "2^(i+1) < n"
    1.76      using i(1) by (auto simp add: less_Suc_eq_0_disj)
    1.77 -  from ceil_log_nat[OF _ this *] ceil_log_nat[OF _ i]
    1.78 +  from ceil_log_nat_ivl[OF _ this *] ceil_log_nat_ivl[OF _ i]
    1.79    show ?thesis by simp
    1.80  qed
    1.81  
    1.82 @@ -130,7 +90,7 @@
    1.83    finally have *: "2^(i+1) \<le> \<dots>" .
    1.84    have "n < 2^(i+1+1)"
    1.85      using i(2) by simp
    1.86 -  from floor_log_nat[OF _ * this] floor_log_nat[OF _ i]
    1.87 +  from floor_log_nat_ivl[OF _ * this] floor_log_nat_ivl[OF _ i]
    1.88    show ?thesis by simp
    1.89  qed
    1.90  
     2.1 --- a/src/HOL/Power.thy	Wed Oct 05 21:27:21 2016 +0200
     2.2 +++ b/src/HOL/Power.thy	Thu Oct 06 11:38:05 2016 +0200
     2.3 @@ -792,6 +792,44 @@
     2.4    qed
     2.5  qed
     2.6  
     2.7 +lemma ex_power_ivl1: fixes b k :: nat assumes "b \<ge> 2"
     2.8 +shows "k \<ge> 1 \<Longrightarrow> \<exists>n. b^n \<le> k \<and> k < b^(n+1)" (is "_ \<Longrightarrow> \<exists>n. ?P k n")
     2.9 +proof(induction k)
    2.10 +  case 0 thus ?case by simp
    2.11 +next
    2.12 +  case (Suc k)
    2.13 +  show ?case
    2.14 +  proof cases
    2.15 +    assume "k=0"
    2.16 +    hence "?P (Suc k) 0" using assms by simp
    2.17 +    thus ?case ..
    2.18 +  next
    2.19 +    assume "k\<noteq>0"
    2.20 +    with Suc obtain n where IH: "?P k n" by auto
    2.21 +    show ?case
    2.22 +    proof (cases "k = b^(n+1) - 1")
    2.23 +      case True
    2.24 +      hence "?P (Suc k) (n+1)" using assms
    2.25 +        by (simp add: power_less_power_Suc)
    2.26 +      thus ?thesis ..
    2.27 +    next
    2.28 +      case False
    2.29 +      hence "?P (Suc k) n" using IH by auto
    2.30 +      thus ?thesis ..
    2.31 +    qed
    2.32 +  qed
    2.33 +qed
    2.34 +
    2.35 +lemma ex_power_ivl2: fixes b k :: nat assumes "b \<ge> 2" "k \<ge> 2"
    2.36 +shows "\<exists>n. b^n < k \<and> k \<le> b^(n+1)"
    2.37 +proof -
    2.38 +  have "1 \<le> k - 1" using assms(2) by arith
    2.39 +  from ex_power_ivl1[OF assms(1) this]
    2.40 +  obtain n where "b ^ n \<le> k - 1 \<and> k - 1 < b ^ (n + 1)" ..
    2.41 +  hence "b^n < k \<and> k \<le> b^(n+1)" using assms by auto
    2.42 +  thus ?thesis ..
    2.43 +qed
    2.44 +
    2.45  
    2.46  subsubsection \<open>Cardinality of the Powerset\<close>
    2.47