equal
deleted
inserted
replaced
63 lemma two_hrealpow_ge_one [simp]: "(1::hypreal) \<le> 2 ^ n" |
63 lemma two_hrealpow_ge_one [simp]: "(1::hypreal) \<le> 2 ^ n" |
64 by (insert power_increasing [of 0 n "2::hypreal"], simp) |
64 by (insert power_increasing [of 0 n "2::hypreal"], simp) |
65 |
65 |
66 lemma two_hrealpow_gt [simp]: "hypreal_of_nat n < 2 ^ n" |
66 lemma two_hrealpow_gt [simp]: "hypreal_of_nat n < 2 ^ n" |
67 apply (induct_tac "n") |
67 apply (induct_tac "n") |
68 apply (auto simp add: hypreal_of_nat_Suc left_distrib) |
68 apply (auto simp add: left_distrib) |
69 apply (cut_tac n = n in two_hrealpow_ge_one, arith) |
69 apply (cut_tac n = n in two_hrealpow_ge_one, arith) |
70 done |
70 done |
71 |
71 |
72 lemma hrealpow: |
72 lemma hrealpow: |
73 "star_n X ^ m = star_n (%n. (X n::real) ^ m)" |
73 "star_n X ^ m = star_n (%n. (X n::real) ^ m)" |
76 done |
76 done |
77 |
77 |
78 lemma hrealpow_sum_square_expand: |
78 lemma hrealpow_sum_square_expand: |
79 "(x + (y::hypreal)) ^ Suc (Suc 0) = |
79 "(x + (y::hypreal)) ^ Suc (Suc 0) = |
80 x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + (hypreal_of_nat (Suc (Suc 0)))*x*y" |
80 x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + (hypreal_of_nat (Suc (Suc 0)))*x*y" |
81 by (simp add: right_distrib left_distrib hypreal_of_nat_Suc) |
81 by (simp add: right_distrib left_distrib) |
82 |
82 |
83 |
83 |
84 subsection{*Literal Arithmetic Involving Powers and Type @{typ hypreal}*} |
84 subsection{*Literal Arithmetic Involving Powers and Type @{typ hypreal}*} |
85 |
85 |
86 lemma power_hypreal_of_real_number_of: |
86 lemma power_hypreal_of_real_number_of: |