src/HOL/Log.thy
changeset 41550 efa734d9b221
parent 36777 be5461582d0f
child 45892 8dcf6692433f
     1.1 --- a/src/HOL/Log.thy	Fri Jan 14 15:43:04 2011 +0100
     1.2 +++ b/src/HOL/Log.thy	Fri Jan 14 15:44:47 2011 +0100
     1.3 @@ -251,10 +251,11 @@
     1.4    apply (erule order_less_imp_le)
     1.5  done
     1.6  
     1.7 -lemma ln_powr_bound2: "1 < x ==> 0 < a ==> (ln x) powr a <= (a powr a) * x"
     1.8 +lemma ln_powr_bound2:
     1.9 +  assumes "1 < x" and "0 < a"
    1.10 +  shows "(ln x) powr a <= (a powr a) * x"
    1.11  proof -
    1.12 -  assume "1 < x" and "0 < a"
    1.13 -  then have "ln x <= (x powr (1 / a)) / (1 / a)"
    1.14 +  from assms have "ln x <= (x powr (1 / a)) / (1 / a)"
    1.15      apply (intro ln_powr_bound)
    1.16      apply (erule order_less_imp_le)
    1.17      apply (rule divide_pos_pos)
    1.18 @@ -264,14 +265,14 @@
    1.19      by simp
    1.20    finally have "(ln x) powr a <= (a * (x powr (1 / a))) powr a"
    1.21      apply (intro powr_mono2)
    1.22 -    apply (rule order_less_imp_le, rule prems)
    1.23 +    apply (rule order_less_imp_le, rule assms)
    1.24      apply (rule ln_gt_zero)
    1.25 -    apply (rule prems)
    1.26 +    apply (rule assms)
    1.27      apply assumption
    1.28      done
    1.29    also have "... = (a powr a) * ((x powr (1 / a)) powr a)"
    1.30      apply (rule powr_mult)
    1.31 -    apply (rule prems)
    1.32 +    apply (rule assms)
    1.33      apply (rule powr_gt_zero)
    1.34      done
    1.35    also have "(x powr (1 / a)) powr a = x powr ((1 / a) * a)"
    1.36 @@ -279,35 +280,37 @@
    1.37    also have "... = x"
    1.38      apply simp
    1.39      apply (subgoal_tac "a ~= 0")
    1.40 -    apply (insert prems, auto)
    1.41 +    using assms apply auto
    1.42      done
    1.43    finally show ?thesis .
    1.44  qed
    1.45  
    1.46 -lemma LIMSEQ_neg_powr: "0 < s ==> (%x. (real x) powr - s) ----> 0"
    1.47 +lemma LIMSEQ_neg_powr:
    1.48 +  assumes s: "0 < s"
    1.49 +  shows "(%x. (real x) powr - s) ----> 0"
    1.50    apply (unfold LIMSEQ_iff)
    1.51    apply clarsimp
    1.52    apply (rule_tac x = "natfloor(r powr (1 / - s)) + 1" in exI)
    1.53    apply clarify
    1.54 -  proof -
    1.55 -    fix r fix n
    1.56 -    assume "0 < s" and "0 < r" and "natfloor (r powr (1 / - s)) + 1 <= n"
    1.57 -    have "r powr (1 / - s) < real(natfloor(r powr (1 / - s))) + 1"
    1.58 -      by (rule real_natfloor_add_one_gt)
    1.59 -    also have "... = real(natfloor(r powr (1 / -s)) + 1)"
    1.60 -      by simp
    1.61 -    also have "... <= real n"
    1.62 -      apply (subst real_of_nat_le_iff)
    1.63 -      apply (rule prems)
    1.64 -      done
    1.65 -    finally have "r powr (1 / - s) < real n".
    1.66 -    then have "real n powr (- s) < (r powr (1 / - s)) powr - s" 
    1.67 -      apply (intro powr_less_mono2_neg)
    1.68 -      apply (auto simp add: prems)
    1.69 -      done
    1.70 -    also have "... = r"
    1.71 -      by (simp add: powr_powr prems less_imp_neq [THEN not_sym])
    1.72 -    finally show "real n powr - s < r" .
    1.73 -  qed
    1.74 +proof -
    1.75 +  fix r fix n
    1.76 +  assume r: "0 < r" and n: "natfloor (r powr (1 / - s)) + 1 <= n"
    1.77 +  have "r powr (1 / - s) < real(natfloor(r powr (1 / - s))) + 1"
    1.78 +    by (rule real_natfloor_add_one_gt)
    1.79 +  also have "... = real(natfloor(r powr (1 / -s)) + 1)"
    1.80 +    by simp
    1.81 +  also have "... <= real n"
    1.82 +    apply (subst real_of_nat_le_iff)
    1.83 +    apply (rule n)
    1.84 +    done
    1.85 +  finally have "r powr (1 / - s) < real n".
    1.86 +  then have "real n powr (- s) < (r powr (1 / - s)) powr - s" 
    1.87 +    apply (intro powr_less_mono2_neg)
    1.88 +    apply (auto simp add: s)
    1.89 +    done
    1.90 +  also have "... = r"
    1.91 +    by (simp add: powr_powr s r less_imp_neq [THEN not_sym])
    1.92 +  finally show "real n powr - s < r" .
    1.93 +qed
    1.94  
    1.95  end