equal
deleted
inserted
replaced
17 |
17 |
18 lemma two_realpow_gt [simp]: "real (n::nat) < 2 ^ n" |
18 lemma two_realpow_gt [simp]: "real (n::nat) < 2 ^ n" |
19 apply (induct "n") |
19 apply (induct "n") |
20 apply (auto simp add: real_of_nat_Suc) |
20 apply (auto simp add: real_of_nat_Suc) |
21 apply (subst mult_2) |
21 apply (subst mult_2) |
22 apply (rule add_less_le_mono) |
22 apply (erule add_less_le_mono) |
23 apply (auto simp add: two_realpow_ge_one) |
23 apply (rule two_realpow_ge_one) |
24 done |
24 done |
25 |
25 |
26 lemma realpow_Suc_le_self: "[| 0 \<le> r; r \<le> (1::real) |] ==> r ^ Suc n \<le> r" |
26 lemma realpow_Suc_le_self: "[| 0 \<le> r; r \<le> (1::real) |] ==> r ^ Suc n \<le> r" |
27 by (insert power_decreasing [of 1 "Suc n" r], simp) |
27 by (insert power_decreasing [of 1 "Suc n" r], simp) |
28 |
28 |
55 apply (auto simp add: real_of_nat_one real_of_nat_mult) |
55 apply (auto simp add: real_of_nat_one real_of_nat_mult) |
56 done |
56 done |
57 |
57 |
58 lemma realpow_real_of_nat_two_pos [simp] : "0 < real (Suc (Suc 0) ^ n)" |
58 lemma realpow_real_of_nat_two_pos [simp] : "0 < real (Suc (Suc 0) ^ n)" |
59 apply (induct "n") |
59 apply (induct "n") |
60 apply (auto simp add: real_of_nat_mult zero_less_mult_iff) |
60 apply (auto simp add: zero_less_mult_iff) |
61 done |
61 done |
62 |
62 |
63 (* used by AFP Integration theory *) |
63 (* used by AFP Integration theory *) |
64 lemma realpow_increasing: |
64 lemma realpow_increasing: |
65 "[|(0::real) \<le> x; 0 \<le> y; x ^ Suc n \<le> y ^ Suc n|] ==> x \<le> y" |
65 "[|(0::real) \<le> x; 0 \<le> y; x ^ Suc n \<le> y ^ Suc n|] ==> x \<le> y" |