author | haftmann |
Tue, 10 Jul 2007 17:30:45 +0200 | |
changeset 23706 | b7abba3c230e |
parent 22888 | ff6559234a89 |
child 24075 | 366d4d234814 |
permissions | -rw-r--r-- |
20245 | 1 |
(* Title : HOL/Hyperreal/HyperDef.thy |
10751 | 2 |
ID : $Id$ |
3 |
Author : Jacques D. Fleuriot |
|
4 |
Copyright : 1998 University of Cambridge |
|
14468 | 5 |
Conversion to Isar and new proofs by Lawrence C Paulson, 2004 |
13487 | 6 |
*) |
10751 | 7 |
|
14468 | 8 |
header{*Construction of Hyperreals Using Ultrafilters*} |
9 |
||
15131 | 10 |
theory HyperDef |
21865
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
11 |
imports HyperNat "../Real/Real" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
12 |
uses ("hypreal_arith.ML") |
15131 | 13 |
begin |
10751 | 14 |
|
17298 | 15 |
types hypreal = "real star" |
14299 | 16 |
|
19380 | 17 |
abbreviation |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
18 |
hypreal_of_real :: "real => real star" where |
19380 | 19 |
"hypreal_of_real == star_of" |
10751 | 20 |
|
21865
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
21 |
abbreviation |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
22 |
hypreal_of_hypnat :: "hypnat \<Rightarrow> hypreal" where |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
23 |
"hypreal_of_hypnat \<equiv> of_hypnat" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
24 |
|
19765 | 25 |
definition |
21787
9edd495b6330
consistent naming for FreeUltrafilterNat lemmas; cleaned up
huffman
parents:
21588
diff
changeset
|
26 |
omega :: hypreal where |
9edd495b6330
consistent naming for FreeUltrafilterNat lemmas; cleaned up
huffman
parents:
21588
diff
changeset
|
27 |
-- {*an infinite number @{text "= [<1,2,3,...>]"} *} |
9edd495b6330
consistent naming for FreeUltrafilterNat lemmas; cleaned up
huffman
parents:
21588
diff
changeset
|
28 |
"omega = star_n (\<lambda>n. real (Suc n))" |
13487 | 29 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
30 |
definition |
21787
9edd495b6330
consistent naming for FreeUltrafilterNat lemmas; cleaned up
huffman
parents:
21588
diff
changeset
|
31 |
epsilon :: hypreal where |
9edd495b6330
consistent naming for FreeUltrafilterNat lemmas; cleaned up
huffman
parents:
21588
diff
changeset
|
32 |
-- {*an infinitesimal number @{text "= [<1,1/2,1/3,...>]"} *} |
9edd495b6330
consistent naming for FreeUltrafilterNat lemmas; cleaned up
huffman
parents:
21588
diff
changeset
|
33 |
"epsilon = star_n (\<lambda>n. inverse (real (Suc n)))" |
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
34 |
|
21210 | 35 |
notation (xsymbols) |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
36 |
omega ("\<omega>") and |
19765 | 37 |
epsilon ("\<epsilon>") |
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
38 |
|
21210 | 39 |
notation (HTML output) |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
40 |
omega ("\<omega>") and |
19765 | 41 |
epsilon ("\<epsilon>") |
14565 | 42 |
|
14329 | 43 |
|
20555 | 44 |
subsection {* Real vector class instances *} |
45 |
||
46 |
instance star :: (scaleR) scaleR .. |
|
47 |
||
48 |
defs (overloaded) |
|
49 |
star_scaleR_def [transfer_unfold]: "scaleR r \<equiv> *f* (scaleR r)" |
|
50 |
||
21787
9edd495b6330
consistent naming for FreeUltrafilterNat lemmas; cleaned up
huffman
parents:
21588
diff
changeset
|
51 |
lemma Standard_scaleR [simp]: "x \<in> Standard \<Longrightarrow> scaleR r x \<in> Standard" |
20726 | 52 |
by (simp add: star_scaleR_def) |
53 |
||
21787
9edd495b6330
consistent naming for FreeUltrafilterNat lemmas; cleaned up
huffman
parents:
21588
diff
changeset
|
54 |
lemma star_of_scaleR [simp]: "star_of (scaleR r x) = scaleR r (star_of x)" |
20726 | 55 |
by transfer (rule refl) |
56 |
||
20555 | 57 |
instance star :: (real_vector) real_vector |
58 |
proof |
|
59 |
fix a b :: real |
|
21787
9edd495b6330
consistent naming for FreeUltrafilterNat lemmas; cleaned up
huffman
parents:
21588
diff
changeset
|
60 |
show "\<And>x y::'a star. scaleR a (x + y) = scaleR a x + scaleR a y" |
20555 | 61 |
by transfer (rule scaleR_right_distrib) |
21787
9edd495b6330
consistent naming for FreeUltrafilterNat lemmas; cleaned up
huffman
parents:
21588
diff
changeset
|
62 |
show "\<And>x::'a star. scaleR (a + b) x = scaleR a x + scaleR b x" |
20555 | 63 |
by transfer (rule scaleR_left_distrib) |
21787
9edd495b6330
consistent naming for FreeUltrafilterNat lemmas; cleaned up
huffman
parents:
21588
diff
changeset
|
64 |
show "\<And>x::'a star. scaleR a (scaleR b x) = scaleR (a * b) x" |
20765 | 65 |
by transfer (rule scaleR_scaleR) |
21787
9edd495b6330
consistent naming for FreeUltrafilterNat lemmas; cleaned up
huffman
parents:
21588
diff
changeset
|
66 |
show "\<And>x::'a star. scaleR 1 x = x" |
20555 | 67 |
by transfer (rule scaleR_one) |
68 |
qed |
|
69 |
||
70 |
instance star :: (real_algebra) real_algebra |
|
71 |
proof |
|
72 |
fix a :: real |
|
21787
9edd495b6330
consistent naming for FreeUltrafilterNat lemmas; cleaned up
huffman
parents:
21588
diff
changeset
|
73 |
show "\<And>x y::'a star. scaleR a x * y = scaleR a (x * y)" |
20555 | 74 |
by transfer (rule mult_scaleR_left) |
21787
9edd495b6330
consistent naming for FreeUltrafilterNat lemmas; cleaned up
huffman
parents:
21588
diff
changeset
|
75 |
show "\<And>x y::'a star. x * scaleR a y = scaleR a (x * y)" |
20555 | 76 |
by transfer (rule mult_scaleR_right) |
77 |
qed |
|
78 |
||
79 |
instance star :: (real_algebra_1) real_algebra_1 .. |
|
80 |
||
20584
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20555
diff
changeset
|
81 |
instance star :: (real_div_algebra) real_div_algebra .. |
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20555
diff
changeset
|
82 |
|
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20555
diff
changeset
|
83 |
instance star :: (real_field) real_field .. |
60b1d52a455d
added classes real_div_algebra and real_field; added lemmas
huffman
parents:
20555
diff
changeset
|
84 |
|
20726 | 85 |
lemma star_of_real_def [transfer_unfold]: "of_real r = star_of (of_real r)" |
86 |
by (unfold of_real_def, transfer, rule refl) |
|
87 |
||
88 |
lemma Standard_of_real [simp]: "of_real r \<in> Standard" |
|
89 |
by (simp add: star_of_real_def) |
|
20555 | 90 |
|
91 |
lemma star_of_of_real [simp]: "star_of (of_real r) = of_real r" |
|
92 |
by transfer (rule refl) |
|
93 |
||
20729 | 94 |
lemma of_real_eq_star_of [simp]: "of_real = star_of" |
95 |
proof |
|
96 |
fix r :: real |
|
97 |
show "of_real r = star_of r" |
|
98 |
by transfer simp |
|
99 |
qed |
|
100 |
||
101 |
lemma Reals_eq_Standard: "(Reals :: hypreal set) = Standard" |
|
20765 | 102 |
by (simp add: Reals_def Standard_def) |
20729 | 103 |
|
20555 | 104 |
|
22877 | 105 |
subsection {* Injection from @{typ hypreal} *} |
106 |
||
107 |
definition |
|
108 |
of_hypreal :: "hypreal \<Rightarrow> 'a::real_algebra_1 star" where |
|
109 |
"of_hypreal = *f* of_real" |
|
110 |
||
111 |
declare of_hypreal_def [transfer_unfold] |
|
112 |
||
113 |
lemma Standard_of_hypreal [simp]: |
|
114 |
"r \<in> Standard \<Longrightarrow> of_hypreal r \<in> Standard" |
|
115 |
by (simp add: of_hypreal_def) |
|
116 |
||
117 |
lemma of_hypreal_0 [simp]: "of_hypreal 0 = 0" |
|
118 |
by transfer (rule of_real_0) |
|
119 |
||
120 |
lemma of_hypreal_1 [simp]: "of_hypreal 1 = 1" |
|
121 |
by transfer (rule of_real_1) |
|
122 |
||
123 |
lemma of_hypreal_add [simp]: |
|
124 |
"\<And>x y. of_hypreal (x + y) = of_hypreal x + of_hypreal y" |
|
125 |
by transfer (rule of_real_add) |
|
126 |
||
127 |
lemma of_hypreal_minus [simp]: "\<And>x. of_hypreal (- x) = - of_hypreal x" |
|
128 |
by transfer (rule of_real_minus) |
|
129 |
||
130 |
lemma of_hypreal_diff [simp]: |
|
131 |
"\<And>x y. of_hypreal (x - y) = of_hypreal x - of_hypreal y" |
|
132 |
by transfer (rule of_real_diff) |
|
133 |
||
134 |
lemma of_hypreal_mult [simp]: |
|
135 |
"\<And>x y. of_hypreal (x * y) = of_hypreal x * of_hypreal y" |
|
136 |
by transfer (rule of_real_mult) |
|
137 |
||
138 |
lemma of_hypreal_inverse [simp]: |
|
139 |
"\<And>x. of_hypreal (inverse x) = |
|
140 |
inverse (of_hypreal x :: 'a::{real_div_algebra,division_by_zero} star)" |
|
141 |
by transfer (rule of_real_inverse) |
|
142 |
||
143 |
lemma of_hypreal_divide [simp]: |
|
144 |
"\<And>x y. of_hypreal (x / y) = |
|
145 |
(of_hypreal x / of_hypreal y :: 'a::{real_field,division_by_zero} star)" |
|
146 |
by transfer (rule of_real_divide) |
|
147 |
||
148 |
lemma of_hypreal_eq_iff [simp]: |
|
149 |
"\<And>x y. (of_hypreal x = of_hypreal y) = (x = y)" |
|
150 |
by transfer (rule of_real_eq_iff) |
|
151 |
||
152 |
lemma of_hypreal_eq_0_iff [simp]: |
|
153 |
"\<And>x. (of_hypreal x = 0) = (x = 0)" |
|
154 |
by transfer (rule of_real_eq_0_iff) |
|
155 |
||
156 |
||
17298 | 157 |
subsection{*Properties of @{term starrel}*} |
14329 | 158 |
|
21787
9edd495b6330
consistent naming for FreeUltrafilterNat lemmas; cleaned up
huffman
parents:
21588
diff
changeset
|
159 |
lemma lemma_starrel_refl [simp]: "x \<in> starrel `` {x}" |
9edd495b6330
consistent naming for FreeUltrafilterNat lemmas; cleaned up
huffman
parents:
21588
diff
changeset
|
160 |
by (simp add: starrel_def) |
9edd495b6330
consistent naming for FreeUltrafilterNat lemmas; cleaned up
huffman
parents:
21588
diff
changeset
|
161 |
|
9edd495b6330
consistent naming for FreeUltrafilterNat lemmas; cleaned up
huffman
parents:
21588
diff
changeset
|
162 |
lemma starrel_in_hypreal [simp]: "starrel``{x}:star" |
9edd495b6330
consistent naming for FreeUltrafilterNat lemmas; cleaned up
huffman
parents:
21588
diff
changeset
|
163 |
by (simp add: star_def starrel_def quotient_def, blast) |
9edd495b6330
consistent naming for FreeUltrafilterNat lemmas; cleaned up
huffman
parents:
21588
diff
changeset
|
164 |
|
9edd495b6330
consistent naming for FreeUltrafilterNat lemmas; cleaned up
huffman
parents:
21588
diff
changeset
|
165 |
declare Abs_star_inject [simp] Abs_star_inverse [simp] |
9edd495b6330
consistent naming for FreeUltrafilterNat lemmas; cleaned up
huffman
parents:
21588
diff
changeset
|
166 |
declare equiv_starrel [THEN eq_equiv_class_iff, simp] |
14299 | 167 |
|
14329 | 168 |
subsection{*@{term hypreal_of_real}: |
169 |
the Injection from @{typ real} to @{typ hypreal}*} |
|
14299 | 170 |
|
21810
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21787
diff
changeset
|
171 |
lemma inj_star_of: "inj star_of" |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17301
diff
changeset
|
172 |
by (rule inj_onI, simp) |
14299 | 173 |
|
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20245
diff
changeset
|
174 |
lemma mem_Rep_star_iff: "(X \<in> Rep_star x) = (x = star_n X)" |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20245
diff
changeset
|
175 |
by (cases x, simp add: star_n_def) |
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20245
diff
changeset
|
176 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17301
diff
changeset
|
177 |
lemma Rep_star_star_n_iff [simp]: |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17301
diff
changeset
|
178 |
"(X \<in> Rep_star (star_n Y)) = ({n. Y n = X n} \<in> \<U>)" |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17301
diff
changeset
|
179 |
by (simp add: star_n_def) |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17301
diff
changeset
|
180 |
|
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17301
diff
changeset
|
181 |
lemma Rep_star_star_n: "X \<in> Rep_star (star_n X)" |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17301
diff
changeset
|
182 |
by simp |
14329 | 183 |
|
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
184 |
subsection{* Properties of @{term star_n} *} |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17301
diff
changeset
|
185 |
|
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17301
diff
changeset
|
186 |
lemma star_n_add: |
17298 | 187 |
"star_n X + 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:
17318
diff
changeset
|
188 |
by (simp only: star_add_def starfun2_star_n) |
14329 | 189 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17301
diff
changeset
|
190 |
lemma star_n_minus: |
17298 | 191 |
"- star_n X = star_n (%n. -(X n))" |
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
192 |
by (simp only: star_minus_def starfun_star_n) |
14299 | 193 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17301
diff
changeset
|
194 |
lemma star_n_diff: |
17298 | 195 |
"star_n X - 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:
17318
diff
changeset
|
196 |
by (simp only: star_diff_def starfun2_star_n) |
14299 | 197 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17301
diff
changeset
|
198 |
lemma star_n_mult: |
17298 | 199 |
"star_n X * 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:
17318
diff
changeset
|
200 |
by (simp only: star_mult_def starfun2_star_n) |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17301
diff
changeset
|
201 |
|
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17301
diff
changeset
|
202 |
lemma star_n_inverse: |
17301 | 203 |
"inverse (star_n X) = star_n (%n. inverse(X n))" |
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
204 |
by (simp only: star_inverse_def starfun_star_n) |
14299 | 205 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17301
diff
changeset
|
206 |
lemma star_n_le: |
17298 | 207 |
"star_n X \<le> star_n Y = |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14361
diff
changeset
|
208 |
({n. X n \<le> Y n} \<in> FreeUltrafilterNat)" |
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
209 |
by (simp only: star_le_def starP2_star_n) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
210 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
211 |
lemma star_n_less: |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
212 |
"star_n X < star_n Y = ({n. X n < Y n} \<in> FreeUltrafilterNat)" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
213 |
by (simp only: star_less_def starP2_star_n) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
214 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
215 |
lemma star_n_zero_num: "0 = star_n (%n. 0)" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
216 |
by (simp only: star_zero_def star_of_def) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
217 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
218 |
lemma star_n_one_num: "1 = star_n (%n. 1)" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
219 |
by (simp only: star_one_def star_of_def) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
220 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
221 |
lemma star_n_abs: |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
222 |
"abs (star_n X) = star_n (%n. abs (X n))" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
223 |
by (simp only: star_abs_def starfun_star_n) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
224 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
225 |
subsection{*Misc Others*} |
14299 | 226 |
|
14370 | 227 |
lemma hypreal_not_refl2: "!!(x::hypreal). x < y ==> x \<noteq> y" |
15539 | 228 |
by (auto) |
14329 | 229 |
|
14331 | 230 |
lemma hypreal_eq_minus_iff: "((x::hypreal) = y) = (x + - y = 0)" |
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset
|
231 |
by auto |
14331 | 232 |
|
14329 | 233 |
lemma hypreal_mult_left_cancel: "(c::hypreal) \<noteq> 0 ==> (c*a=c*b) = (a=b)" |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
234 |
by auto |
14329 | 235 |
|
236 |
lemma hypreal_mult_right_cancel: "(c::hypreal) \<noteq> 0 ==> (a*c=b*c) = (a=b)" |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
237 |
by auto |
14329 | 238 |
|
14301 | 239 |
lemma hypreal_omega_gt_zero [simp]: "0 < omega" |
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
240 |
by (simp add: omega_def star_n_zero_num star_n_less) |
14370 | 241 |
|
242 |
subsection{*Existence of Infinite Hyperreal Number*} |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17301
diff
changeset
|
243 |
|
14370 | 244 |
text{*Existence of infinite number not corresponding to any real number. |
245 |
Use assumption that member @{term FreeUltrafilterNat} is not finite.*} |
|
246 |
||
247 |
||
248 |
text{*A few lemmas first*} |
|
249 |
||
250 |
lemma lemma_omega_empty_singleton_disj: "{n::nat. x = real n} = {} | |
|
251 |
(\<exists>y. {n::nat. x = real n} = {y})" |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
252 |
by force |
14370 | 253 |
|
254 |
lemma lemma_finite_omega_set: "finite {n::nat. x = real n}" |
|
255 |
by (cut_tac x = x in lemma_omega_empty_singleton_disj, auto) |
|
256 |
||
257 |
lemma not_ex_hypreal_of_real_eq_omega: |
|
258 |
"~ (\<exists>x. hypreal_of_real x = omega)" |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17301
diff
changeset
|
259 |
apply (simp add: omega_def) |
17298 | 260 |
apply (simp add: star_of_def star_n_eq_iff) |
14370 | 261 |
apply (auto simp add: real_of_nat_Suc diff_eq_eq [symmetric] |
21855
74909ecaf20a
remove ultra tactic and redundant FreeUltrafilterNat lemmas
huffman
parents:
21810
diff
changeset
|
262 |
lemma_finite_omega_set [THEN FreeUltrafilterNat.finite]) |
14370 | 263 |
done |
264 |
||
265 |
lemma hypreal_of_real_not_eq_omega: "hypreal_of_real x \<noteq> omega" |
|
14705 | 266 |
by (insert not_ex_hypreal_of_real_eq_omega, auto) |
14370 | 267 |
|
268 |
text{*Existence of infinitesimal number also not corresponding to any |
|
269 |
real number*} |
|
270 |
||
271 |
lemma lemma_epsilon_empty_singleton_disj: |
|
272 |
"{n::nat. x = inverse(real(Suc n))} = {} | |
|
273 |
(\<exists>y. {n::nat. x = inverse(real(Suc n))} = {y})" |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
274 |
by auto |
14370 | 275 |
|
276 |
lemma lemma_finite_epsilon_set: "finite {n. x = inverse(real(Suc n))}" |
|
277 |
by (cut_tac x = x in lemma_epsilon_empty_singleton_disj, auto) |
|
278 |
||
14705 | 279 |
lemma not_ex_hypreal_of_real_eq_epsilon: "~ (\<exists>x. hypreal_of_real x = epsilon)" |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17301
diff
changeset
|
280 |
by (auto simp add: epsilon_def star_of_def star_n_eq_iff |
21855
74909ecaf20a
remove ultra tactic and redundant FreeUltrafilterNat lemmas
huffman
parents:
21810
diff
changeset
|
281 |
lemma_finite_epsilon_set [THEN FreeUltrafilterNat.finite]) |
14370 | 282 |
|
283 |
lemma hypreal_of_real_not_eq_epsilon: "hypreal_of_real x \<noteq> epsilon" |
|
14705 | 284 |
by (insert not_ex_hypreal_of_real_eq_epsilon, auto) |
14370 | 285 |
|
286 |
lemma hypreal_epsilon_not_zero: "epsilon \<noteq> 0" |
|
17298 | 287 |
by (simp add: epsilon_def star_zero_def star_of_def star_n_eq_iff |
288 |
del: star_of_zero) |
|
14370 | 289 |
|
290 |
lemma hypreal_epsilon_inverse_omega: "epsilon = inverse(omega)" |
|
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17318
diff
changeset
|
291 |
by (simp add: epsilon_def omega_def star_n_inverse) |
14370 | 292 |
|
20753 | 293 |
lemma hypreal_epsilon_gt_zero: "0 < epsilon" |
294 |
by (simp add: hypreal_epsilon_inverse_omega) |
|
295 |
||
21865
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
296 |
subsection{*Absolute Value Function for the Hyperreals*} |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
297 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
298 |
lemma hrabs_add_less: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
299 |
"[| abs x < r; abs y < s |] ==> abs(x+y) < r + (s::hypreal)" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
300 |
by (simp add: abs_if split: split_if_asm) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
301 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
302 |
lemma hrabs_less_gt_zero: "abs x < r ==> (0::hypreal) < r" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
303 |
by (blast intro!: order_le_less_trans abs_ge_zero) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
304 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
305 |
lemma hrabs_disj: "abs x = (x::'a::abs_if) | abs x = -x" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
306 |
by (simp add: abs_if) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
307 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
308 |
lemma hrabs_add_lemma_disj: "(y::hypreal) + - x + (y + - z) = abs (x + - z) ==> y = z | x = y" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
309 |
by (simp add: abs_if split add: split_if_asm) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
310 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
311 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
312 |
subsection{*Embedding the Naturals into the Hyperreals*} |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
313 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
314 |
abbreviation |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
315 |
hypreal_of_nat :: "nat => hypreal" where |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
316 |
"hypreal_of_nat == of_nat" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
317 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
318 |
lemma SNat_eq: "Nats = {n. \<exists>N. n = hypreal_of_nat N}" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
319 |
by (simp add: Nats_def image_def) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
320 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
321 |
(*------------------------------------------------------------*) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
322 |
(* naturals embedded in hyperreals *) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
323 |
(* is a hyperreal c.f. NS extension *) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
324 |
(*------------------------------------------------------------*) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
325 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
326 |
lemma hypreal_of_nat_eq: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
327 |
"hypreal_of_nat (n::nat) = hypreal_of_real (real n)" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
328 |
by (simp add: real_of_nat_def) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
329 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
330 |
lemma hypreal_of_nat: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
331 |
"hypreal_of_nat m = star_n (%n. real m)" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
332 |
apply (fold star_of_def) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
333 |
apply (simp add: real_of_nat_def) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
334 |
done |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
335 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
336 |
(* |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
337 |
FIXME: we should declare this, as for type int, but many proofs would break. |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
338 |
It replaces x+-y by x-y. |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
339 |
Addsimps [symmetric hypreal_diff_def] |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
340 |
*) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
341 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
342 |
use "hypreal_arith.ML" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
343 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
344 |
setup hypreal_arith_setup |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
345 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
346 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
347 |
subsection {* Exponentials on the Hyperreals *} |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
348 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
349 |
lemma hpowr_0 [simp]: "r ^ 0 = (1::hypreal)" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
350 |
by (rule power_0) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
351 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
352 |
lemma hpowr_Suc [simp]: "r ^ (Suc n) = (r::hypreal) * (r ^ n)" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
353 |
by (rule power_Suc) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
354 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
355 |
lemma hrealpow_two: "(r::hypreal) ^ Suc (Suc 0) = r * r" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
356 |
by simp |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
357 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
358 |
lemma hrealpow_two_le [simp]: "(0::hypreal) \<le> r ^ Suc (Suc 0)" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
359 |
by (auto simp add: zero_le_mult_iff) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
360 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
361 |
lemma hrealpow_two_le_add_order [simp]: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
362 |
"(0::hypreal) \<le> u ^ Suc (Suc 0) + v ^ Suc (Suc 0)" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
363 |
by (simp only: hrealpow_two_le add_nonneg_nonneg) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
364 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
365 |
lemma hrealpow_two_le_add_order2 [simp]: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
366 |
"(0::hypreal) \<le> u ^ Suc (Suc 0) + v ^ Suc (Suc 0) + w ^ Suc (Suc 0)" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
367 |
by (simp only: hrealpow_two_le add_nonneg_nonneg) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
368 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
369 |
lemma hypreal_add_nonneg_eq_0_iff: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
370 |
"[| 0 \<le> x; 0 \<le> y |] ==> (x+y = 0) = (x = 0 & y = (0::hypreal))" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
371 |
by arith |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
372 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
373 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
374 |
text{*FIXME: DELETE THESE*} |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
375 |
lemma hypreal_three_squares_add_zero_iff: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
376 |
"(x*x + y*y + z*z = 0) = (x = 0 & y = 0 & z = (0::hypreal))" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
377 |
apply (simp only: zero_le_square add_nonneg_nonneg hypreal_add_nonneg_eq_0_iff, auto) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
378 |
done |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
379 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
380 |
lemma hrealpow_three_squares_add_zero_iff [simp]: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
381 |
"(x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + z ^ Suc (Suc 0) = (0::hypreal)) = |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
382 |
(x = 0 & y = 0 & z = 0)" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
383 |
by (simp only: hypreal_three_squares_add_zero_iff hrealpow_two) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
384 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
385 |
(*FIXME: This and RealPow.abs_realpow_two should be replaced by an abstract |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
386 |
result proved in Ring_and_Field*) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
387 |
lemma hrabs_hrealpow_two [simp]: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
388 |
"abs(x ^ Suc (Suc 0)) = (x::hypreal) ^ Suc (Suc 0)" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
389 |
by (simp add: abs_mult) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
390 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
391 |
lemma two_hrealpow_ge_one [simp]: "(1::hypreal) \<le> 2 ^ n" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
392 |
by (insert power_increasing [of 0 n "2::hypreal"], simp) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
393 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
394 |
lemma two_hrealpow_gt [simp]: "hypreal_of_nat n < 2 ^ n" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
395 |
apply (induct_tac "n") |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
396 |
apply (auto simp add: left_distrib) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
397 |
apply (cut_tac n = n in two_hrealpow_ge_one, arith) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
398 |
done |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
399 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
400 |
lemma hrealpow: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
401 |
"star_n X ^ m = star_n (%n. (X n::real) ^ m)" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
402 |
apply (induct_tac "m") |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
403 |
apply (auto simp add: star_n_one_num star_n_mult power_0) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
404 |
done |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
405 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
406 |
lemma hrealpow_sum_square_expand: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
407 |
"(x + (y::hypreal)) ^ Suc (Suc 0) = |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
408 |
x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + (hypreal_of_nat (Suc (Suc 0)))*x*y" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
409 |
by (simp add: right_distrib left_distrib) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
410 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
411 |
lemma power_hypreal_of_real_number_of: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
412 |
"(number_of v :: hypreal) ^ n = hypreal_of_real ((number_of v) ^ n)" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
413 |
by simp |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
414 |
declare power_hypreal_of_real_number_of [of _ "number_of w", standard, simp] |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
415 |
(* |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
416 |
lemma hrealpow_HFinite: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
417 |
fixes x :: "'a::{real_normed_algebra,recpower} star" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
418 |
shows "x \<in> HFinite ==> x ^ n \<in> HFinite" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
419 |
apply (induct_tac "n") |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
420 |
apply (auto simp add: power_Suc intro: HFinite_mult) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
421 |
done |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
422 |
*) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
423 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
424 |
subsection{*Powers with Hypernatural Exponents*} |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
425 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
426 |
definition |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
427 |
(* hypernatural powers of hyperreals *) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
428 |
pow :: "['a::power star, nat star] \<Rightarrow> 'a star" (infixr "pow" 80) where |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
429 |
hyperpow_def [transfer_unfold]: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
430 |
"R pow N = ( *f2* op ^) R N" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
431 |
|
22879 | 432 |
lemma Standard_hyperpow [simp]: |
433 |
"\<lbrakk>r \<in> Standard; n \<in> Standard\<rbrakk> \<Longrightarrow> r pow n \<in> Standard" |
|
434 |
unfolding hyperpow_def by simp |
|
435 |
||
21865
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
436 |
lemma hyperpow: "star_n X pow star_n Y = star_n (%n. X n ^ Y n)" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
437 |
by (simp add: hyperpow_def starfun2_star_n) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
438 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
439 |
lemma hyperpow_zero [simp]: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
440 |
"\<And>n. (0::'a::{recpower,semiring_0} star) pow (n + (1::hypnat)) = 0" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
441 |
by transfer simp |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
442 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
443 |
lemma hyperpow_not_zero: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
444 |
"\<And>r n. r \<noteq> (0::'a::{recpower,field} star) ==> r pow n \<noteq> 0" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
445 |
by transfer (rule field_power_not_zero) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
446 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
447 |
lemma hyperpow_inverse: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
448 |
"\<And>r n. r \<noteq> (0::'a::{recpower,division_by_zero,field} star) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
449 |
\<Longrightarrow> inverse (r pow n) = (inverse r) pow n" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
450 |
by transfer (rule power_inverse) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
451 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
452 |
lemma hyperpow_hrabs: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
453 |
"\<And>r n. abs (r::'a::{recpower,ordered_idom} star) pow n = abs (r pow n)" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
454 |
by transfer (rule power_abs [symmetric]) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
455 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
456 |
lemma hyperpow_add: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
457 |
"\<And>r n m. (r::'a::recpower star) pow (n + m) = (r pow n) * (r pow m)" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
458 |
by transfer (rule power_add) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
459 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
460 |
lemma hyperpow_one [simp]: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
461 |
"\<And>r. (r::'a::recpower star) pow (1::hypnat) = r" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
462 |
by transfer (rule power_one_right) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
463 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
464 |
lemma hyperpow_two: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
465 |
"\<And>r. (r::'a::recpower star) pow ((1::hypnat) + (1::hypnat)) = r * r" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
466 |
by transfer (simp add: power_Suc) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
467 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
468 |
lemma hyperpow_gt_zero: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
469 |
"\<And>r n. (0::'a::{recpower,ordered_semidom} star) < r \<Longrightarrow> 0 < r pow n" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
470 |
by transfer (rule zero_less_power) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
471 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
472 |
lemma hyperpow_ge_zero: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
473 |
"\<And>r n. (0::'a::{recpower,ordered_semidom} star) \<le> r \<Longrightarrow> 0 \<le> r pow n" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
474 |
by transfer (rule zero_le_power) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
475 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
476 |
lemma hyperpow_le: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
477 |
"\<And>x y n. \<lbrakk>(0::'a::{recpower,ordered_semidom} star) < x; x \<le> y\<rbrakk> |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
478 |
\<Longrightarrow> x pow n \<le> y pow n" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
479 |
by transfer (rule power_mono [OF _ order_less_imp_le]) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
480 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
481 |
lemma hyperpow_eq_one [simp]: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
482 |
"\<And>n. 1 pow n = (1::'a::recpower star)" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
483 |
by transfer (rule power_one) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
484 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
485 |
lemma hrabs_hyperpow_minus_one [simp]: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
486 |
"\<And>n. abs(-1 pow n) = (1::'a::{number_ring,recpower,ordered_idom} star)" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
487 |
by transfer (rule abs_power_minus_one) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
488 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
489 |
lemma hyperpow_mult: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
490 |
"\<And>r s n. (r * s::'a::{comm_monoid_mult,recpower} star) pow n |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
491 |
= (r pow n) * (s pow n)" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
492 |
by transfer (rule power_mult_distrib) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
493 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
494 |
lemma hyperpow_two_le [simp]: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
495 |
"(0::'a::{recpower,ordered_ring_strict} star) \<le> r pow (1 + 1)" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
496 |
by (auto simp add: hyperpow_two zero_le_mult_iff) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
497 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
498 |
lemma hrabs_hyperpow_two [simp]: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
499 |
"abs(x pow (1 + 1)) = |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
500 |
(x::'a::{recpower,ordered_ring_strict} star) pow (1 + 1)" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
501 |
by (simp only: abs_of_nonneg hyperpow_two_le) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
502 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
503 |
lemma hyperpow_two_hrabs [simp]: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
504 |
"abs(x::'a::{recpower,ordered_idom} star) pow (1 + 1) = x pow (1 + 1)" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
505 |
by (simp add: hyperpow_hrabs) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
506 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
507 |
text{*The precondition could be weakened to @{term "0\<le>x"}*} |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
508 |
lemma hypreal_mult_less_mono: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
509 |
"[| u<v; x<y; (0::hypreal) < v; 0 < x |] ==> u*x < v* y" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
510 |
by (simp add: Ring_and_Field.mult_strict_mono order_less_imp_le) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
511 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
512 |
lemma hyperpow_two_gt_one: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
513 |
"\<And>r::'a::{recpower,ordered_semidom} star. 1 < r \<Longrightarrow> 1 < r pow (1 + 1)" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
514 |
by transfer (simp add: power_gt1) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
515 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
516 |
lemma hyperpow_two_ge_one: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
517 |
"\<And>r::'a::{recpower,ordered_semidom} star. 1 \<le> r \<Longrightarrow> 1 \<le> r pow (1 + 1)" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
518 |
by transfer (simp add: one_le_power) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
519 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
520 |
lemma two_hyperpow_ge_one [simp]: "(1::hypreal) \<le> 2 pow n" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
521 |
apply (rule_tac y = "1 pow n" in order_trans) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
522 |
apply (rule_tac [2] hyperpow_le, auto) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
523 |
done |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
524 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
525 |
lemma hyperpow_minus_one2 [simp]: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
526 |
"!!n. -1 pow ((1 + 1)*n) = (1::hypreal)" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
527 |
by transfer (subst power_mult, simp) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
528 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
529 |
lemma hyperpow_less_le: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
530 |
"!!r n N. [|(0::hypreal) \<le> r; r \<le> 1; n < N|] ==> r pow N \<le> r pow n" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
531 |
by transfer (rule power_decreasing [OF order_less_imp_le]) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
532 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
533 |
lemma hyperpow_SHNat_le: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
534 |
"[| 0 \<le> r; r \<le> (1::hypreal); N \<in> HNatInfinite |] |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
535 |
==> ALL n: Nats. r pow N \<le> r pow n" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
536 |
by (auto intro!: hyperpow_less_le simp add: HNatInfinite_iff) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
537 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
538 |
lemma hyperpow_realpow: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
539 |
"(hypreal_of_real r) pow (hypnat_of_nat n) = hypreal_of_real (r ^ n)" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
540 |
by transfer (rule refl) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
541 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
542 |
lemma hyperpow_SReal [simp]: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
543 |
"(hypreal_of_real r) pow (hypnat_of_nat n) \<in> Reals" |
22879 | 544 |
by (simp add: Reals_eq_Standard) |
21865
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
545 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
546 |
lemma hyperpow_zero_HNatInfinite [simp]: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
547 |
"N \<in> HNatInfinite ==> (0::hypreal) pow N = 0" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
548 |
by (drule HNatInfinite_is_Suc, auto) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
549 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
550 |
lemma hyperpow_le_le: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
551 |
"[| (0::hypreal) \<le> r; r \<le> 1; n \<le> N |] ==> r pow N \<le> r pow n" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
552 |
apply (drule order_le_less [of n, THEN iffD1]) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
553 |
apply (auto intro: hyperpow_less_le) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
554 |
done |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
555 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
556 |
lemma hyperpow_Suc_le_self2: |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
557 |
"[| (0::hypreal) \<le> r; r < 1 |] ==> r pow (n + (1::hypnat)) \<le> r" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
558 |
apply (drule_tac n = " (1::hypnat) " in hyperpow_le_le) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
559 |
apply auto |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
560 |
done |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
561 |
|
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
562 |
lemma hyperpow_hypnat_of_nat: "\<And>x. x pow hypnat_of_nat n = x ^ n" |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
563 |
by transfer (rule refl) |
55cc354fd2d9
moved several theorems; rearranged theory dependencies
huffman
parents:
21856
diff
changeset
|
564 |
|
22888 | 565 |
lemma of_hypreal_hyperpow: |
566 |
"\<And>x n. of_hypreal (x pow n) = |
|
567 |
(of_hypreal x::'a::{real_algebra_1,recpower} star) pow n" |
|
568 |
by transfer (rule of_real_power) |
|
569 |
||
10751 | 570 |
end |