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.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.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
```