src/HOL/Power.thy
changeset 64065 40d440b75b00
parent 63924 f91766530e13
child 64715 33d5fa0ce6e5
     1.1 --- a/src/HOL/Power.thy	Wed Oct 05 21:27:21 2016 +0200
     1.2 +++ b/src/HOL/Power.thy	Thu Oct 06 11:38:05 2016 +0200
     1.3 @@ -792,6 +792,44 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 +lemma ex_power_ivl1: fixes b k :: nat assumes "b \<ge> 2"
     1.8 +shows "k \<ge> 1 \<Longrightarrow> \<exists>n. b^n \<le> k \<and> k < b^(n+1)" (is "_ \<Longrightarrow> \<exists>n. ?P k n")
     1.9 +proof(induction k)
    1.10 +  case 0 thus ?case by simp
    1.11 +next
    1.12 +  case (Suc k)
    1.13 +  show ?case
    1.14 +  proof cases
    1.15 +    assume "k=0"
    1.16 +    hence "?P (Suc k) 0" using assms by simp
    1.17 +    thus ?case ..
    1.18 +  next
    1.19 +    assume "k\<noteq>0"
    1.20 +    with Suc obtain n where IH: "?P k n" by auto
    1.21 +    show ?case
    1.22 +    proof (cases "k = b^(n+1) - 1")
    1.23 +      case True
    1.24 +      hence "?P (Suc k) (n+1)" using assms
    1.25 +        by (simp add: power_less_power_Suc)
    1.26 +      thus ?thesis ..
    1.27 +    next
    1.28 +      case False
    1.29 +      hence "?P (Suc k) n" using IH by auto
    1.30 +      thus ?thesis ..
    1.31 +    qed
    1.32 +  qed
    1.33 +qed
    1.34 +
    1.35 +lemma ex_power_ivl2: fixes b k :: nat assumes "b \<ge> 2" "k \<ge> 2"
    1.36 +shows "\<exists>n. b^n < k \<and> k \<le> b^(n+1)"
    1.37 +proof -
    1.38 +  have "1 \<le> k - 1" using assms(2) by arith
    1.39 +  from ex_power_ivl1[OF assms(1) this]
    1.40 +  obtain n where "b ^ n \<le> k - 1 \<and> k - 1 < b ^ (n + 1)" ..
    1.41 +  hence "b^n < k \<and> k \<le> b^(n+1)" using assms by auto
    1.42 +  thus ?thesis ..
    1.43 +qed
    1.44 +
    1.45  
    1.46  subsubsection \<open>Cardinality of the Powerset\<close>
    1.47