author  huffman 
Thu, 14 Dec 2006 21:33:47 +0100  
changeset 21851  030f46b8c4b5 
parent 21848  b35faf14a89f 
permissions  rwrr 
10751  1 
(* Title : HyperPow.thy 
2 
Author : Jacques D. Fleuriot 

3 
Copyright : 1998 University of Cambridge 

14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

4 
Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4 
10751  5 
*) 
6 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

7 
header{*Exponentials on the Hyperreals*} 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

8 

15131  9 
theory HyperPow 
21256  10 
imports HyperArith HyperNat Parity 
15131  11 
begin 
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset

12 

17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset

13 
(* consts hpowr :: "[hypreal,nat] => hypreal" *) 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

14 

17298  15 
lemma hpowr_0 [simp]: "r ^ 0 = (1::hypreal)" 
16 
by (rule power_0) 

17 

18 
lemma hpowr_Suc [simp]: "r ^ (Suc n) = (r::hypreal) * (r ^ n)" 

19 
by (rule power_Suc) 

10751  20 

19765  21 
definition 
10751  22 
(* hypernatural powers of hyperreals *) 
21848  23 
pow :: "['a::power star, nat star] \<Rightarrow> 'a star" (infixr "pow" 80) where 
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset

24 
hyperpow_def [transfer_unfold]: 
21848  25 
"R pow N = ( *f2* op ^) R N" 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

26 

744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

27 
lemma hrealpow_two: "(r::hypreal) ^ Suc (Suc 0) = r * r" 
14443
75910c7557c5
generic theorems about exponentials; general tidying up
paulson
parents:
14435
diff
changeset

28 
by simp 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

29 

15003  30 
lemma hrealpow_two_le [simp]: "(0::hypreal) \<le> r ^ Suc (Suc 0)" 
14371
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14348
diff
changeset

31 
by (auto simp add: zero_le_mult_iff) 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

32 

15003  33 
lemma hrealpow_two_le_add_order [simp]: 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

34 
"(0::hypreal) \<le> u ^ Suc (Suc 0) + v ^ Suc (Suc 0)" 
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset

35 
by (simp only: hrealpow_two_le add_nonneg_nonneg) 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

36 

15003  37 
lemma hrealpow_two_le_add_order2 [simp]: 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

38 
"(0::hypreal) \<le> u ^ Suc (Suc 0) + v ^ Suc (Suc 0) + w ^ Suc (Suc 0)" 
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset

39 
by (simp only: hrealpow_two_le add_nonneg_nonneg) 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

40 

744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

41 
lemma hypreal_add_nonneg_eq_0_iff: 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

42 
"[ 0 \<le> x; 0 \<le> y ] ==> (x+y = 0) = (x = 0 & y = (0::hypreal))" 
15003  43 
by arith 
44 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

45 

744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

46 
text{*FIXME: DELETE THESE*} 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

47 
lemma hypreal_three_squares_add_zero_iff: 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

48 
"(x*x + y*y + z*z = 0) = (x = 0 & y = 0 & z = (0::hypreal))" 
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset

49 
apply (simp only: zero_le_square add_nonneg_nonneg hypreal_add_nonneg_eq_0_iff, auto) 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

50 
done 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

51 

744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

52 
lemma hrealpow_three_squares_add_zero_iff [simp]: 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

53 
"(x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + z ^ Suc (Suc 0) = (0::hypreal)) = 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

54 
(x = 0 & y = 0 & z = 0)" 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

55 
by (simp only: hypreal_three_squares_add_zero_iff hrealpow_two) 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

56 

16924  57 
(*FIXME: This and RealPow.abs_realpow_two should be replaced by an abstract 
58 
result proved in Ring_and_Field*) 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

59 
lemma hrabs_hrealpow_two [simp]: 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

60 
"abs(x ^ Suc (Suc 0)) = (x::hypreal) ^ Suc (Suc 0)" 
16924  61 
by (simp add: abs_mult) 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

62 

744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

63 
lemma two_hrealpow_ge_one [simp]: "(1::hypreal) \<le> 2 ^ n" 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

64 
by (insert power_increasing [of 0 n "2::hypreal"], simp) 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

65 

15003  66 
lemma two_hrealpow_gt [simp]: "hypreal_of_nat n < 2 ^ n" 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

67 
apply (induct_tac "n") 
20730  68 
apply (auto simp add: left_distrib) 
14371
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14348
diff
changeset

69 
apply (cut_tac n = n in two_hrealpow_ge_one, arith) 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

70 
done 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

71 

744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

72 
lemma hrealpow: 
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset

73 
"star_n X ^ m = star_n (%n. (X n::real) ^ m)" 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

74 
apply (induct_tac "m") 
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset

75 
apply (auto simp add: star_n_one_num star_n_mult power_0) 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

76 
done 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

77 

744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

78 
lemma hrealpow_sum_square_expand: 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

79 
"(x + (y::hypreal)) ^ Suc (Suc 0) = 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

80 
x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + (hypreal_of_nat (Suc (Suc 0)))*x*y" 
20730  81 
by (simp add: right_distrib left_distrib) 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

82 

744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

83 

744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

84 
subsection{*Literal Arithmetic Involving Powers and Type @{typ hypreal}*} 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

85 

744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

86 
lemma power_hypreal_of_real_number_of: 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

87 
"(number_of v :: hypreal) ^ n = hypreal_of_real ((number_of v) ^ n)" 
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset

88 
by simp 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

89 
declare power_hypreal_of_real_number_of [of _ "number_of w", standard, simp] 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

90 

20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
19765
diff
changeset

91 
lemma hrealpow_HFinite: 
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
19765
diff
changeset

92 
fixes x :: "'a::{real_normed_algebra,recpower} star" 
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
19765
diff
changeset

93 
shows "x \<in> HFinite ==> x ^ n \<in> HFinite" 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

94 
apply (induct_tac "n") 
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
19765
diff
changeset

95 
apply (auto simp add: power_Suc intro: HFinite_mult) 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

96 
done 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

97 

744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

98 

744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

99 
subsection{*Powers with Hypernatural Exponents*} 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

100 

17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset

101 
lemma hyperpow: "star_n X pow star_n Y = star_n (%n. X n ^ Y n)" 
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17332
diff
changeset

102 
by (simp add: hyperpow_def starfun2_star_n) 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

103 

21848  104 
lemma hyperpow_zero [simp]: 
105 
"\<And>n. (0::'a::{recpower,semiring_0} star) pow (n + (1::hypnat)) = 0" 

106 
by transfer simp 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

107 

21848  108 
lemma hyperpow_not_zero: 
109 
"\<And>r n. r \<noteq> (0::'a::{recpower,field} star) ==> r pow n \<noteq> 0" 

110 
by transfer (rule field_power_not_zero) 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

111 

744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

112 
lemma hyperpow_inverse: 
21848  113 
"\<And>r n. r \<noteq> (0::'a::{recpower,division_by_zero,field} star) 
114 
\<Longrightarrow> inverse (r pow n) = (inverse r) pow n" 

115 
by transfer (rule power_inverse) 

17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset

116 

21848  117 
lemma hyperpow_hrabs: 
118 
"\<And>r n. abs (r::'a::{recpower,ordered_idom} star) pow n = abs (r pow n)" 

119 
by transfer (rule power_abs [symmetric]) 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

120 

21848  121 
lemma hyperpow_add: 
122 
"\<And>r n m. (r::'a::recpower star) pow (n + m) = (r pow n) * (r pow m)" 

123 
by transfer (rule power_add) 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

124 

21848  125 
lemma hyperpow_one [simp]: 
126 
"\<And>r. (r::'a::recpower star) pow (1::hypnat) = r" 

127 
by transfer (rule power_one_right) 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

128 

744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

129 
lemma hyperpow_two: 
21848  130 
"\<And>r. (r::'a::recpower star) pow ((1::hypnat) + (1::hypnat)) = r * r" 
131 
by transfer (simp add: power_Suc) 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

132 

21848  133 
lemma hyperpow_gt_zero: 
134 
"\<And>r n. (0::'a::{recpower,ordered_semidom} star) < r \<Longrightarrow> 0 < r pow n" 

135 
by transfer (rule zero_less_power) 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

136 

21848  137 
lemma hyperpow_ge_zero: 
138 
"\<And>r n. (0::'a::{recpower,ordered_semidom} star) \<le> r \<Longrightarrow> 0 \<le> r pow n" 

139 
by transfer (rule zero_le_power) 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

140 

17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset

141 
lemma hyperpow_le: 
21848  142 
"\<And>x y n. \<lbrakk>(0::'a::{recpower,ordered_semidom} star) < x; x \<le> y\<rbrakk> 
143 
\<Longrightarrow> x pow n \<le> y pow n" 

144 
by transfer (rule power_mono [OF _ order_less_imp_le]) 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

145 

21848  146 
lemma hyperpow_eq_one [simp]: 
147 
"\<And>n. 1 pow n = (1::'a::recpower star)" 

148 
by transfer (rule power_one) 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

149 

21848  150 
lemma hrabs_hyperpow_minus_one [simp]: 
151 
"\<And>n. abs(1 pow n) = (1::'a::{number_ring,recpower,ordered_idom} star)" 

152 
by transfer (rule abs_power_minus_one) 

17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset

153 

21848  154 
lemma hyperpow_mult: 
155 
"\<And>r s n. (r * s::'a::{comm_monoid_mult,recpower} star) pow n 

156 
= (r pow n) * (s pow n)" 

157 
by transfer (rule power_mult_distrib) 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

158 

21848  159 
lemma hyperpow_two_le [simp]: 
160 
"(0::'a::{recpower,ordered_ring_strict} star) \<le> r pow (1 + 1)" 

14371
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14348
diff
changeset

161 
by (auto simp add: hyperpow_two zero_le_mult_iff) 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

162 

21848  163 
lemma hrabs_hyperpow_two [simp]: 
164 
"abs(x pow (1 + 1)) = 

165 
(x::'a::{recpower,ordered_ring_strict} star) pow (1 + 1)" 

166 
by (simp only: abs_of_nonneg hyperpow_two_le) 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

167 

21848  168 
lemma hyperpow_two_hrabs [simp]: 
169 
"abs(x::'a::{recpower,ordered_idom} star) pow (1 + 1) = x pow (1 + 1)" 

15003  170 
by (simp add: hyperpow_hrabs) 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

171 

15229  172 
text{*The precondition could be weakened to @{term "0\<le>x"}*} 
173 
lemma hypreal_mult_less_mono: 

174 
"[ u<v; x<y; (0::hypreal) < v; 0 < x ] ==> u*x < v* y" 

175 
by (simp add: Ring_and_Field.mult_strict_mono order_less_imp_le) 

176 

21848  177 
lemma hyperpow_two_gt_one: 
178 
"\<And>r::'a::{recpower,ordered_semidom} star. 1 < r \<Longrightarrow> 1 < r pow (1 + 1)" 

179 
by transfer (simp add: power_gt1) 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

180 

744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

181 
lemma hyperpow_two_ge_one: 
21848  182 
"\<And>r::'a::{recpower,ordered_semidom} star. 1 \<le> r \<Longrightarrow> 1 \<le> r pow (1 + 1)" 
183 
by transfer (simp add: one_le_power) 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

184 

15003  185 
lemma two_hyperpow_ge_one [simp]: "(1::hypreal) \<le> 2 pow n" 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

186 
apply (rule_tac y = "1 pow n" in order_trans) 
14371
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14348
diff
changeset

187 
apply (rule_tac [2] hyperpow_le, auto) 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

188 
done 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

189 

15003  190 
lemma hyperpow_minus_one2 [simp]: 
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset

191 
"!!n. 1 pow ((1 + 1)*n) = (1::hypreal)" 
21848  192 
by transfer (simp) 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

193 

744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

194 
lemma hyperpow_less_le: 
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset

195 
"!!r n N. [(0::hypreal) \<le> r; r \<le> 1; n < N] ==> r pow N \<le> r pow n" 
21848  196 
by transfer (rule power_decreasing [OF order_less_imp_le]) 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

197 

744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

198 
lemma hyperpow_SHNat_le: 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

199 
"[ 0 \<le> r; r \<le> (1::hypreal); N \<in> HNatInfinite ] 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

200 
==> ALL n: Nats. r pow N \<le> r pow n" 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

201 
by (auto intro!: hyperpow_less_le simp add: HNatInfinite_iff) 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

202 

744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

203 
lemma hyperpow_realpow: 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

204 
"(hypreal_of_real r) pow (hypnat_of_nat n) = hypreal_of_real (r ^ n)" 
21851  205 
by transfer (rule refl) 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

206 

15003  207 
lemma hyperpow_SReal [simp]: 
208 
"(hypreal_of_real r) pow (hypnat_of_nat n) \<in> Reals" 

17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset

209 
by (simp del: star_of_power add: hyperpow_realpow SReal_def) 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

210 

15003  211 

212 
lemma hyperpow_zero_HNatInfinite [simp]: 

213 
"N \<in> HNatInfinite ==> (0::hypreal) pow N = 0" 

14371
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14348
diff
changeset

214 
by (drule HNatInfinite_is_Suc, auto) 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

215 

744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

216 
lemma hyperpow_le_le: 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

217 
"[ (0::hypreal) \<le> r; r \<le> 1; n \<le> N ] ==> r pow N \<le> r pow n" 
14371
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14348
diff
changeset

218 
apply (drule order_le_less [of n, THEN iffD1]) 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

219 
apply (auto intro: hyperpow_less_le) 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

220 
done 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

221 

744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

222 
lemma hyperpow_Suc_le_self2: 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

223 
"[ (0::hypreal) \<le> r; r < 1 ] ==> r pow (n + (1::hypnat)) \<le> r" 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

224 
apply (drule_tac n = " (1::hypnat) " in hyperpow_le_le) 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

225 
apply auto 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

226 
done 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

227 

744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

228 
lemma lemma_Infinitesimal_hyperpow: 
21848  229 
"[ (x::hypreal) \<in> Infinitesimal; 0 < N ] ==> abs (x pow N) \<le> abs x" 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

230 
apply (unfold Infinitesimal_def) 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

231 
apply (auto intro!: hyperpow_Suc_le_self2 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

232 
simp add: hyperpow_hrabs [symmetric] hypnat_gt_zero_iff2 abs_ge_zero) 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

233 
done 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

234 

744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

235 
lemma Infinitesimal_hyperpow: 
21848  236 
"[ (x::hypreal) \<in> Infinitesimal; 0 < N ] ==> x pow N \<in> Infinitesimal" 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

237 
apply (rule hrabs_le_Infinitesimal) 
14371
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14348
diff
changeset

238 
apply (rule_tac [2] lemma_Infinitesimal_hyperpow, auto) 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

239 
done 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

240 

21848  241 
lemma hyperpow_hypnat_of_nat: "\<And>x. x pow hypnat_of_nat n = x ^ n" 
242 
by transfer (rule refl) 

243 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

244 
lemma hrealpow_hyperpow_Infinitesimal_iff: 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

245 
"(x ^ n \<in> Infinitesimal) = (x pow (hypnat_of_nat n) \<in> Infinitesimal)" 
21848  246 
by (simp only: hyperpow_hypnat_of_nat) 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

247 

744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

248 
lemma Infinitesimal_hrealpow: 
20541
f614c619b1e1
generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents:
19765
diff
changeset

249 
"[ (x::hypreal) \<in> Infinitesimal; 0 < n ] ==> x ^ n \<in> Infinitesimal" 
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17299
diff
changeset

250 
by (simp add: hrealpow_hyperpow_Infinitesimal_iff Infinitesimal_hyperpow) 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset

251 

10751  252 
end 