author | haftmann |
Wed, 06 Sep 2006 13:48:02 +0200 | |
changeset 20485 | 3078fd2eec7b |
parent 19765 | dfe940911617 |
child 20558 | 759c8f2ead69 |
permissions | -rw-r--r-- |
13957 | 1 |
(* Title: NSComplex.thy |
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset
|
2 |
ID: $Id$ |
13957 | 3 |
Author: Jacques D. Fleuriot |
4 |
Copyright: 2001 University of Edinburgh |
|
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset
|
5 |
Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4 |
13957 | 6 |
*) |
7 |
||
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset
|
8 |
header{*Nonstandard Complex Numbers*} |
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset
|
9 |
|
15131 | 10 |
theory NSComplex |
15140 | 11 |
imports Complex |
15131 | 12 |
begin |
13957 | 13 |
|
17300 | 14 |
types hcomplex = "complex star" |
13957 | 15 |
|
19765 | 16 |
abbreviation |
17 |
hcomplex_of_complex :: "complex => complex star" |
|
18 |
"hcomplex_of_complex == star_of" |
|
14377 | 19 |
|
19765 | 20 |
definition |
13957 | 21 |
|
22 |
(*--- real and Imaginary parts ---*) |
|
14314 | 23 |
|
24 |
hRe :: "hcomplex => hypreal" |
|
19765 | 25 |
"hRe = *f* Re" |
13957 | 26 |
|
14314 | 27 |
hIm :: "hcomplex => hypreal" |
19765 | 28 |
"hIm = *f* Im" |
13957 | 29 |
|
30 |
||
31 |
(*----------- modulus ------------*) |
|
32 |
||
14314 | 33 |
hcmod :: "hcomplex => hypreal" |
19765 | 34 |
"hcmod = *f* cmod" |
13957 | 35 |
|
14314 | 36 |
(*------ imaginary unit ----------*) |
37 |
||
38 |
iii :: hcomplex |
|
19765 | 39 |
"iii = star_of ii" |
13957 | 40 |
|
41 |
(*------- complex conjugate ------*) |
|
42 |
||
14314 | 43 |
hcnj :: "hcomplex => hcomplex" |
19765 | 44 |
"hcnj = *f* cnj" |
13957 | 45 |
|
14314 | 46 |
(*------------ Argand -------------*) |
13957 | 47 |
|
14314 | 48 |
hsgn :: "hcomplex => hcomplex" |
19765 | 49 |
"hsgn = *f* sgn" |
13957 | 50 |
|
14314 | 51 |
harg :: "hcomplex => hypreal" |
19765 | 52 |
"harg = *f* arg" |
13957 | 53 |
|
54 |
(* abbreviation for (cos a + i sin a) *) |
|
14314 | 55 |
hcis :: "hypreal => hcomplex" |
19765 | 56 |
"hcis = *f* cis" |
13957 | 57 |
|
14314 | 58 |
(*----- injection from hyperreals -----*) |
59 |
||
60 |
hcomplex_of_hypreal :: "hypreal => hcomplex" |
|
19765 | 61 |
"hcomplex_of_hypreal = *f* complex_of_real" |
13957 | 62 |
|
14653 | 63 |
(* abbreviation for r*(cos a + i sin a) *) |
64 |
hrcis :: "[hypreal, hypreal] => hcomplex" |
|
19765 | 65 |
"hrcis = *f2* rcis" |
14653 | 66 |
|
13957 | 67 |
(*------------ e ^ (x + iy) ------------*) |
68 |
||
14314 | 69 |
hexpi :: "hcomplex => hcomplex" |
19765 | 70 |
"hexpi = *f* expi" |
14314 | 71 |
|
14377 | 72 |
HComplex :: "[hypreal,hypreal] => hcomplex" |
19765 | 73 |
"HComplex = *f2* Complex" |
13957 | 74 |
|
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
75 |
hcpow :: "[hcomplex,hypnat] => hcomplex" (infixr "hcpow" 80) |
19765 | 76 |
"(z::hcomplex) hcpow (n::hypnat) = ( *f2* op ^) z n" |
13957 | 77 |
|
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
78 |
lemmas hcomplex_defs [transfer_unfold] = |
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
79 |
hRe_def hIm_def hcmod_def iii_def hcnj_def hsgn_def harg_def hcis_def |
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
80 |
hcomplex_of_hypreal_def hrcis_def hexpi_def HComplex_def hcpow_def |
14374 | 81 |
|
14314 | 82 |
|
83 |
subsection{*Properties of Nonstandard Real and Imaginary Parts*} |
|
84 |
||
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
85 |
lemma hRe: "hRe (star_n X) = star_n (%n. Re(X n))" |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
86 |
by (simp add: hRe_def starfun) |
14314 | 87 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
88 |
lemma hIm: "hIm (star_n X) = star_n (%n. Im(X n))" |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
89 |
by (simp add: hIm_def starfun) |
14314 | 90 |
|
14335 | 91 |
lemma hcomplex_hRe_hIm_cancel_iff: |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
92 |
"!!w z. (w=z) = (hRe(w) = hRe(z) & hIm(w) = hIm(z))" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
93 |
by (transfer, rule complex_Re_Im_cancel_iff) |
14314 | 94 |
|
14377 | 95 |
lemma hcomplex_equality [intro?]: "hRe z = hRe w ==> hIm z = hIm w ==> z = w" |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
96 |
by (simp add: hcomplex_hRe_hIm_cancel_iff) |
14377 | 97 |
|
14374 | 98 |
lemma hcomplex_hRe_zero [simp]: "hRe 0 = 0" |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
99 |
by (simp add: hRe star_n_zero_num) |
14314 | 100 |
|
14374 | 101 |
lemma hcomplex_hIm_zero [simp]: "hIm 0 = 0" |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
102 |
by (simp add: hIm star_n_zero_num) |
14314 | 103 |
|
14374 | 104 |
lemma hcomplex_hRe_one [simp]: "hRe 1 = 1" |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
105 |
by (simp add: hRe star_n_one_num) |
14314 | 106 |
|
14374 | 107 |
lemma hcomplex_hIm_one [simp]: "hIm 1 = 0" |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
108 |
by (simp add: hIm star_n_one_num star_n_zero_num) |
14314 | 109 |
|
110 |
||
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
111 |
subsection{*Addition for Nonstandard Complex Numbers*} |
14314 | 112 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
113 |
lemma hRe_add: "!!x y. hRe(x + y) = hRe(x) + hRe(y)" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
114 |
by (transfer, rule complex_Re_add) |
14314 | 115 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
116 |
lemma hIm_add: "!!x y. hIm(x + y) = hIm(x) + hIm(y)" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
117 |
by (transfer, rule complex_Im_add) |
14374 | 118 |
|
14318 | 119 |
subsection{*More Minus Laws*} |
120 |
||
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
121 |
lemma hRe_minus: "!!z. hRe(-z) = - hRe(z)" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
122 |
by (transfer, rule complex_Re_minus) |
14318 | 123 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
124 |
lemma hIm_minus: "!!z. hIm(-z) = - hIm(z)" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
125 |
by (transfer, rule complex_Im_minus) |
14318 | 126 |
|
127 |
lemma hcomplex_add_minus_eq_minus: |
|
128 |
"x + y = (0::hcomplex) ==> x = -y" |
|
14738 | 129 |
apply (drule OrderedGroup.equals_zero_I) |
14374 | 130 |
apply (simp add: minus_equation_iff [of x y]) |
14318 | 131 |
done |
132 |
||
14377 | 133 |
lemma hcomplex_i_mult_eq [simp]: "iii * iii = - 1" |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
134 |
by (simp add: iii_def star_of_def star_n_mult star_n_one_num star_n_minus) |
14377 | 135 |
|
136 |
lemma hcomplex_i_mult_left [simp]: "iii * (iii * z) = -z" |
|
137 |
by (simp add: mult_assoc [symmetric]) |
|
138 |
||
139 |
lemma hcomplex_i_not_zero [simp]: "iii \<noteq> 0" |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
140 |
by (simp add: iii_def star_of_def star_n_zero_num star_n_eq_iff) |
14377 | 141 |
|
14318 | 142 |
|
143 |
subsection{*More Multiplication Laws*} |
|
144 |
||
14374 | 145 |
lemma hcomplex_mult_minus_one [simp]: "- 1 * (z::hcomplex) = -z" |
146 |
by simp |
|
14318 | 147 |
|
14374 | 148 |
lemma hcomplex_mult_minus_one_right [simp]: "(z::hcomplex) * - 1 = -z" |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
149 |
by simp |
14318 | 150 |
|
14335 | 151 |
lemma hcomplex_mult_left_cancel: |
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
152 |
"(c::hcomplex) \<noteq> (0::hcomplex) ==> (c*a=c*b) = (a=b)" |
14374 | 153 |
by (simp add: field_mult_cancel_left) |
14314 | 154 |
|
14335 | 155 |
lemma hcomplex_mult_right_cancel: |
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
156 |
"(c::hcomplex) \<noteq> (0::hcomplex) ==> (a*c=b*c) = (a=b)" |
14374 | 157 |
by (simp add: Ring_and_Field.field_mult_cancel_right) |
14314 | 158 |
|
159 |
||
14318 | 160 |
subsection{*Subraction and Division*} |
14314 | 161 |
|
14374 | 162 |
lemma hcomplex_diff_eq_eq [simp]: "((x::hcomplex) - y = z) = (x = z + y)" |
14738 | 163 |
by (rule OrderedGroup.diff_eq_eq) |
14314 | 164 |
|
165 |
lemma hcomplex_add_divide_distrib: "(x+y)/(z::hcomplex) = x/z + y/z" |
|
14374 | 166 |
by (rule Ring_and_Field.add_divide_distrib) |
14314 | 167 |
|
168 |
||
169 |
subsection{*Embedding Properties for @{term hcomplex_of_hypreal} Map*} |
|
170 |
||
171 |
lemma hcomplex_of_hypreal: |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
172 |
"hcomplex_of_hypreal (star_n X) = star_n (%n. complex_of_real (X n))" |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
173 |
by (simp add: hcomplex_of_hypreal_def starfun) |
14314 | 174 |
|
14374 | 175 |
lemma hcomplex_of_hypreal_cancel_iff [iff]: |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
176 |
"!!x y. (hcomplex_of_hypreal x = hcomplex_of_hypreal y) = (x = y)" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
177 |
by (transfer, simp) |
14314 | 178 |
|
14374 | 179 |
lemma hcomplex_of_hypreal_one [simp]: "hcomplex_of_hypreal 1 = 1" |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
180 |
by (simp add: hcomplex_of_hypreal star_n_one_num) |
14314 | 181 |
|
14374 | 182 |
lemma hcomplex_of_hypreal_zero [simp]: "hcomplex_of_hypreal 0 = 0" |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
183 |
by (simp add: star_n_zero_num hcomplex_of_hypreal) |
14374 | 184 |
|
15013 | 185 |
lemma hcomplex_of_hypreal_minus [simp]: |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
186 |
"!!x. hcomplex_of_hypreal(-x) = - hcomplex_of_hypreal x" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
187 |
by (transfer, simp) |
15013 | 188 |
|
189 |
lemma hcomplex_of_hypreal_inverse [simp]: |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
190 |
"!!x. hcomplex_of_hypreal(inverse x) = inverse(hcomplex_of_hypreal x)" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
191 |
by (transfer, simp) |
15013 | 192 |
|
193 |
lemma hcomplex_of_hypreal_add [simp]: |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
194 |
"!!x y. hcomplex_of_hypreal (x + y) = |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
195 |
hcomplex_of_hypreal x + hcomplex_of_hypreal y" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
196 |
by (transfer, simp) |
15013 | 197 |
|
198 |
lemma hcomplex_of_hypreal_diff [simp]: |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
199 |
"!!x y. hcomplex_of_hypreal (x - y) = |
15013 | 200 |
hcomplex_of_hypreal x - hcomplex_of_hypreal y " |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
201 |
by (transfer, simp) |
15013 | 202 |
|
203 |
lemma hcomplex_of_hypreal_mult [simp]: |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
204 |
"!!x y. hcomplex_of_hypreal (x * y) = |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
205 |
hcomplex_of_hypreal x * hcomplex_of_hypreal y" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
206 |
by (transfer, simp) |
15013 | 207 |
|
208 |
lemma hcomplex_of_hypreal_divide [simp]: |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
209 |
"!!x y. hcomplex_of_hypreal(x/y) = |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
210 |
hcomplex_of_hypreal x / hcomplex_of_hypreal y" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
211 |
by (transfer, simp) |
15013 | 212 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
213 |
lemma hRe_hcomplex_of_hypreal [simp]: "!!z. hRe(hcomplex_of_hypreal z) = z" |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
214 |
by (transfer, simp) |
14314 | 215 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
216 |
lemma hIm_hcomplex_of_hypreal [simp]: "!!z. hIm(hcomplex_of_hypreal z) = 0" |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
217 |
by (transfer, simp) |
14314 | 218 |
|
14374 | 219 |
lemma hcomplex_of_hypreal_epsilon_not_zero [simp]: |
220 |
"hcomplex_of_hypreal epsilon \<noteq> 0" |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
221 |
by (simp add: hcomplex_of_hypreal epsilon_def star_n_zero_num star_n_eq_iff) |
14314 | 222 |
|
14318 | 223 |
|
14377 | 224 |
subsection{*HComplex theorems*} |
225 |
||
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
226 |
lemma hRe_HComplex [simp]: "!!x y. hRe (HComplex x y) = x" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
227 |
by (transfer, simp) |
14377 | 228 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
229 |
lemma hIm_HComplex [simp]: "!!x y. hIm (HComplex x y) = y" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
230 |
by (transfer, simp) |
14377 | 231 |
|
232 |
text{*Relates the two nonstandard constructions*} |
|
17300 | 233 |
lemma HComplex_eq_Abs_star_Complex: |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
234 |
"HComplex (star_n X) (star_n Y) = |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
235 |
star_n (%n::nat. Complex (X n) (Y n))" |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
236 |
by (simp add: hcomplex_hRe_hIm_cancel_iff hRe hIm) |
14377 | 237 |
|
238 |
lemma hcomplex_surj [simp]: "HComplex (hRe z) (hIm z) = z" |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
239 |
by (simp add: hcomplex_equality) |
14377 | 240 |
|
17300 | 241 |
lemma hcomplex_induct [case_names rect(*, induct type: hcomplex*)]: |
14377 | 242 |
"(\<And>x y. P (HComplex x y)) ==> P z" |
243 |
by (rule hcomplex_surj [THEN subst], blast) |
|
244 |
||
245 |
||
14318 | 246 |
subsection{*Modulus (Absolute Value) of Nonstandard Complex Number*} |
14314 | 247 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
248 |
lemma hcmod: "hcmod (star_n X) = star_n (%n. cmod (X n))" |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
249 |
by (simp add: hcmod_def starfun) |
14314 | 250 |
|
14374 | 251 |
lemma hcmod_zero [simp]: "hcmod(0) = 0" |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
252 |
by (simp add: star_n_zero_num hcmod) |
14314 | 253 |
|
14374 | 254 |
lemma hcmod_one [simp]: "hcmod(1) = 1" |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
255 |
by (simp add: hcmod star_n_one_num) |
14314 | 256 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
257 |
lemma hcmod_hcomplex_of_hypreal [simp]: |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
258 |
"!!x. hcmod(hcomplex_of_hypreal x) = abs x" |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
259 |
by (transfer, simp) |
14314 | 260 |
|
14335 | 261 |
lemma hcomplex_of_hypreal_abs: |
262 |
"hcomplex_of_hypreal (abs x) = |
|
14314 | 263 |
hcomplex_of_hypreal(hcmod(hcomplex_of_hypreal x))" |
14374 | 264 |
by simp |
14314 | 265 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
266 |
lemma HComplex_inject [simp]: |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
267 |
"!!x y x' y'. HComplex x y = HComplex x' y' = (x=x' & y=y')" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
268 |
by (transfer, simp) |
14377 | 269 |
|
270 |
lemma HComplex_add [simp]: |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
271 |
"!!x1 y1 x2 y2. HComplex x1 y1 + HComplex x2 y2 = HComplex (x1+x2) (y1+y2)" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
272 |
by (transfer, simp) |
14377 | 273 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
274 |
lemma HComplex_minus [simp]: "!!x y. - HComplex x y = HComplex (-x) (-y)" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
275 |
by (transfer, simp) |
14377 | 276 |
|
277 |
lemma HComplex_diff [simp]: |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
278 |
"!!x1 y1 x2 y2. HComplex x1 y1 - HComplex x2 y2 = HComplex (x1-x2) (y1-y2)" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
279 |
by (transfer, rule complex_diff) |
14377 | 280 |
|
281 |
lemma HComplex_mult [simp]: |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
282 |
"!!x1 y1 x2 y2. HComplex x1 y1 * HComplex x2 y2 = |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
283 |
HComplex (x1*x2 - y1*y2) (x1*y2 + y1*x2)" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
284 |
by (transfer, rule complex_mult) |
14377 | 285 |
|
286 |
(*HComplex_inverse is proved below*) |
|
287 |
||
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
288 |
lemma hcomplex_of_hypreal_eq: "!!r. hcomplex_of_hypreal r = HComplex r 0" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
289 |
apply (transfer) |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
290 |
apply (simp add: complex_of_real_def) |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
291 |
done |
14377 | 292 |
|
293 |
lemma HComplex_add_hcomplex_of_hypreal [simp]: |
|
294 |
"HComplex x y + hcomplex_of_hypreal r = HComplex (x+r) y" |
|
295 |
by (simp add: hcomplex_of_hypreal_eq) |
|
296 |
||
297 |
lemma hcomplex_of_hypreal_add_HComplex [simp]: |
|
298 |
"hcomplex_of_hypreal r + HComplex x y = HComplex (r+x) y" |
|
299 |
by (simp add: i_def hcomplex_of_hypreal_eq) |
|
300 |
||
301 |
lemma HComplex_mult_hcomplex_of_hypreal: |
|
302 |
"HComplex x y * hcomplex_of_hypreal r = HComplex (x*r) (y*r)" |
|
303 |
by (simp add: hcomplex_of_hypreal_eq) |
|
304 |
||
305 |
lemma hcomplex_of_hypreal_mult_HComplex: |
|
306 |
"hcomplex_of_hypreal r * HComplex x y = HComplex (r*x) (r*y)" |
|
307 |
by (simp add: i_def hcomplex_of_hypreal_eq) |
|
308 |
||
309 |
lemma i_hcomplex_of_hypreal [simp]: |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
310 |
"!!r. iii * hcomplex_of_hypreal r = HComplex 0 r" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
311 |
by (transfer, rule i_complex_of_real) |
14377 | 312 |
|
313 |
lemma hcomplex_of_hypreal_i [simp]: |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
314 |
"!!r. hcomplex_of_hypreal r * iii = HComplex 0 r" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
315 |
by (transfer, rule complex_of_real_i) |
14377 | 316 |
|
14314 | 317 |
|
318 |
subsection{*Conjugation*} |
|
319 |
||
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
320 |
lemma hcnj: "hcnj (star_n X) = star_n (%n. cnj(X n))" |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
321 |
by (simp add: hcnj_def starfun) |
14314 | 322 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
323 |
lemma hcomplex_hcnj_cancel_iff [iff]: "!!x y. (hcnj x = hcnj y) = (x = y)" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
324 |
by (transfer, rule complex_cnj_cancel_iff) |
14374 | 325 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
326 |
lemma hcomplex_hcnj_hcnj [simp]: "!!z. hcnj (hcnj z) = z" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
327 |
by (transfer, rule complex_cnj_cnj) |
14314 | 328 |
|
14374 | 329 |
lemma hcomplex_hcnj_hcomplex_of_hypreal [simp]: |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
330 |
"!!x. hcnj (hcomplex_of_hypreal x) = hcomplex_of_hypreal x" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
331 |
by (transfer, rule complex_cnj_complex_of_real) |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
332 |
|
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
333 |
lemma hcomplex_hmod_hcnj [simp]: "!!z. hcmod (hcnj z) = hcmod z" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
334 |
by (transfer, rule complex_mod_cnj) |
14314 | 335 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
336 |
lemma hcomplex_hcnj_minus: "!!z. hcnj (-z) = - hcnj z" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
337 |
by (transfer, rule complex_cnj_minus) |
14314 | 338 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
339 |
lemma hcomplex_hcnj_inverse: "!!z. hcnj(inverse z) = inverse(hcnj z)" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
340 |
by (transfer, rule complex_cnj_inverse) |
14314 | 341 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
342 |
lemma hcomplex_hcnj_add: "!!w z. hcnj(w + z) = hcnj(w) + hcnj(z)" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
343 |
by (transfer, rule complex_cnj_add) |
14314 | 344 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
345 |
lemma hcomplex_hcnj_diff: "!!w z. hcnj(w - z) = hcnj(w) - hcnj(z)" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
346 |
by (transfer, rule complex_cnj_diff) |
14314 | 347 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
348 |
lemma hcomplex_hcnj_mult: "!!w z. hcnj(w * z) = hcnj(w) * hcnj(z)" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
349 |
by (transfer, rule complex_cnj_mult) |
14314 | 350 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
351 |
lemma hcomplex_hcnj_divide: "!!w z. hcnj(w / z) = (hcnj w)/(hcnj z)" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
352 |
by (transfer, rule complex_cnj_divide) |
14314 | 353 |
|
14374 | 354 |
lemma hcnj_one [simp]: "hcnj 1 = 1" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
355 |
by (transfer, rule complex_cnj_one) |
14314 | 356 |
|
14374 | 357 |
lemma hcomplex_hcnj_zero [simp]: "hcnj 0 = 0" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
358 |
by (transfer, rule complex_cnj_zero) |
14374 | 359 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
360 |
lemma hcomplex_hcnj_zero_iff [iff]: "!!z. (hcnj z = 0) = (z = 0)" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
361 |
by (transfer, rule complex_cnj_zero_iff) |
14314 | 362 |
|
14335 | 363 |
lemma hcomplex_mult_hcnj: |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
364 |
"!!z. z * hcnj z = hcomplex_of_hypreal (hRe(z) ^ 2 + hIm(z) ^ 2)" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
365 |
by (transfer, rule complex_mult_cnj) |
14314 | 366 |
|
367 |
||
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
368 |
subsection{*More Theorems about the Function @{term hcmod}*} |
14314 | 369 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
370 |
lemma hcomplex_hcmod_eq_zero_cancel [simp]: "!!x. (hcmod x = 0) = (x = 0)" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
371 |
by (transfer, rule complex_mod_eq_zero_cancel) |
14314 | 372 |
|
14374 | 373 |
lemma hcmod_hcomplex_of_hypreal_of_nat [simp]: |
14335 | 374 |
"hcmod (hcomplex_of_hypreal(hypreal_of_nat n)) = hypreal_of_nat n" |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
375 |
by (simp add: abs_if linorder_not_less) |
14314 | 376 |
|
14374 | 377 |
lemma hcmod_hcomplex_of_hypreal_of_hypnat [simp]: |
14335 | 378 |
"hcmod (hcomplex_of_hypreal(hypreal_of_hypnat n)) = hypreal_of_hypnat n" |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
379 |
by (simp add: abs_if linorder_not_less) |
14314 | 380 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
381 |
lemma hcmod_minus [simp]: "!!x. hcmod (-x) = hcmod(x)" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
382 |
by (transfer, rule complex_mod_minus) |
14314 | 383 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
384 |
lemma hcmod_mult_hcnj: "!!z. hcmod(z * hcnj(z)) = hcmod(z) ^ 2" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
385 |
by (transfer, rule complex_mod_mult_cnj) |
14314 | 386 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
387 |
lemma hcmod_ge_zero [simp]: "!!x. (0::hypreal) \<le> hcmod x" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
388 |
by (transfer, rule complex_mod_ge_zero) |
14314 | 389 |
|
14374 | 390 |
lemma hrabs_hcmod_cancel [simp]: "abs(hcmod x) = hcmod x" |
391 |
by (simp add: abs_if linorder_not_less) |
|
14314 | 392 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
393 |
lemma hcmod_mult: "!!x y. hcmod(x*y) = hcmod(x) * hcmod(y)" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
394 |
by (transfer, rule complex_mod_mult) |
14314 | 395 |
|
396 |
lemma hcmod_add_squared_eq: |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
397 |
"!!x y. hcmod(x + y) ^ 2 = hcmod(x) ^ 2 + hcmod(y) ^ 2 + 2 * hRe(x * hcnj y)" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
398 |
by (transfer, rule complex_mod_add_squared_eq) |
14314 | 399 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
400 |
lemma hcomplex_hRe_mult_hcnj_le_hcmod [simp]: |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
401 |
"!!x y. hRe(x * hcnj y) \<le> hcmod(x * hcnj y)" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
402 |
by (transfer, simp) |
14314 | 403 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
404 |
lemma hcomplex_hRe_mult_hcnj_le_hcmod2 [simp]: |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
405 |
"!!x y. hRe(x * hcnj y) \<le> hcmod(x * y)" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
406 |
by (transfer, simp) |
14314 | 407 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
408 |
lemma hcmod_triangle_squared [simp]: |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
409 |
"!!x y. hcmod (x + y) ^ 2 \<le> (hcmod(x) + hcmod(y)) ^ 2" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
410 |
by (transfer, simp) |
14314 | 411 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
412 |
lemma hcmod_triangle_ineq [simp]: |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
413 |
"!!x y. hcmod (x + y) \<le> hcmod(x) + hcmod(y)" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
414 |
by (transfer, simp) |
14314 | 415 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
416 |
lemma hcmod_triangle_ineq2 [simp]: |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
417 |
"!!a b. hcmod(b + a) - hcmod b \<le> hcmod a" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
418 |
by (transfer, simp) |
14314 | 419 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
420 |
lemma hcmod_diff_commute: "!!x y. hcmod (x - y) = hcmod (y - x)" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
421 |
by (transfer, rule complex_mod_diff_commute) |
14314 | 422 |
|
14335 | 423 |
lemma hcmod_add_less: |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
424 |
"!!x y r s. [| hcmod x < r; hcmod y < s |] ==> hcmod (x + y) < r + s" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
425 |
by (transfer, rule complex_mod_add_less) |
14314 | 426 |
|
14335 | 427 |
lemma hcmod_mult_less: |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
428 |
"!!x y r s. [| hcmod x < r; hcmod y < s |] ==> hcmod (x * y) < r * s" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
429 |
by (transfer, rule complex_mod_mult_less) |
14314 | 430 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
431 |
lemma hcmod_diff_ineq [simp]: "!!a b. hcmod(a) - hcmod(b) \<le> hcmod(a + b)" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
432 |
by (transfer, simp) |
14314 | 433 |
|
434 |
||
435 |
subsection{*A Few Nonlinear Theorems*} |
|
436 |
||
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
437 |
lemma hcpow: "star_n X hcpow 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:
17373
diff
changeset
|
438 |
by (simp add: hcpow_def starfun2_star_n) |
14314 | 439 |
|
14335 | 440 |
lemma hcomplex_of_hypreal_hyperpow: |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
441 |
"!!x n. hcomplex_of_hypreal (x pow n) = (hcomplex_of_hypreal x) hcpow n" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
442 |
by (transfer, rule complex_of_real_pow) |
14314 | 443 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
444 |
lemma hcmod_hcpow: "!!x n. hcmod(x hcpow n) = hcmod(x) pow n" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
445 |
by (transfer, rule complex_mod_complexpow) |
14314 | 446 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
447 |
lemma hcmod_hcomplex_inverse: "!!x. hcmod(inverse x) = inverse(hcmod x)" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
448 |
by (transfer, rule complex_mod_inverse) |
14314 | 449 |
|
14374 | 450 |
lemma hcmod_divide: "hcmod(x/y) = hcmod(x)/(hcmod y)" |
17300 | 451 |
by (simp add: divide_inverse hcmod_mult hcmod_hcomplex_inverse) |
14314 | 452 |
|
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
453 |
|
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
454 |
subsection{*Exponentiation*} |
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
455 |
|
17300 | 456 |
lemma hcomplexpow_0 [simp]: "z ^ 0 = (1::hcomplex)" |
457 |
by (rule power_0) |
|
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
458 |
|
17300 | 459 |
lemma hcomplexpow_Suc [simp]: "z ^ (Suc n) = (z::hcomplex) * (z ^ n)" |
460 |
by (rule power_Suc) |
|
461 |
||
14377 | 462 |
lemma hcomplexpow_i_squared [simp]: "iii ^ 2 = - 1" |
463 |
by (simp add: power2_eq_square) |
|
464 |
||
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
465 |
|
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
466 |
lemma hcomplex_of_hypreal_pow: |
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
467 |
"hcomplex_of_hypreal (x ^ n) = (hcomplex_of_hypreal x) ^ n" |
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
468 |
apply (induct_tac "n") |
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
469 |
apply (auto simp add: hcomplex_of_hypreal_mult [symmetric]) |
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
470 |
done |
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
471 |
|
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
472 |
lemma hcomplex_hcnj_pow: "hcnj(z ^ n) = hcnj(z) ^ n" |
14314 | 473 |
apply (induct_tac "n") |
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
474 |
apply (auto simp add: hcomplex_hcnj_mult) |
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
475 |
done |
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
476 |
|
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
477 |
lemma hcmod_hcomplexpow: "hcmod(x ^ n) = hcmod(x) ^ n" |
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
478 |
apply (induct_tac "n") |
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
479 |
apply (auto simp add: hcmod_mult) |
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
480 |
done |
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
481 |
|
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
482 |
lemma hcpow_minus: |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
483 |
"!!x n. (-x::hcomplex) hcpow n = |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
484 |
(if ( *p* even) n then (x hcpow n) else -(x hcpow n))" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
485 |
by (transfer, rule neg_power_if) |
14314 | 486 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
487 |
lemma hcpow_mult: |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
488 |
"!!r s n. ((r::hcomplex) * s) hcpow n = (r hcpow n) * (s hcpow n)" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
489 |
by (transfer, rule power_mult_distrib) |
14314 | 490 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
491 |
lemma hcpow_zero [simp]: "!!n. 0 hcpow (n + 1) = 0" |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
492 |
by (transfer, simp) |
14314 | 493 |
|
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
494 |
lemma hcpow_zero2 [simp]: "0 hcpow (hSuc n) = 0" |
14374 | 495 |
by (simp add: hSuc_def) |
14314 | 496 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
497 |
lemma hcpow_not_zero [simp,intro]: |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
498 |
"!!r n. r \<noteq> 0 ==> r hcpow n \<noteq> (0::hcomplex)" |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
499 |
by (transfer, simp) |
14314 | 500 |
|
501 |
lemma hcpow_zero_zero: "r hcpow n = (0::hcomplex) ==> r = 0" |
|
14374 | 502 |
by (blast intro: ccontr dest: hcpow_not_zero) |
14314 | 503 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
504 |
lemma star_n_divide: "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:
17373
diff
changeset
|
505 |
by (simp add: star_divide_def starfun2_star_n) |
14377 | 506 |
|
14314 | 507 |
subsection{*The Function @{term hsgn}*} |
508 |
||
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
509 |
lemma hsgn: "hsgn (star_n X) = star_n (%n. sgn (X n))" |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
510 |
by (simp add: hsgn_def starfun) |
14314 | 511 |
|
14374 | 512 |
lemma hsgn_zero [simp]: "hsgn 0 = 0" |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
513 |
by (simp add: star_n_zero_num hsgn) |
14314 | 514 |
|
14374 | 515 |
lemma hsgn_one [simp]: "hsgn 1 = 1" |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
516 |
by (simp add: star_n_one_num hsgn) |
14314 | 517 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
518 |
lemma hsgn_minus: "!!z. hsgn (-z) = - hsgn(z)" |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
519 |
by (transfer, rule sgn_minus) |
14314 | 520 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
521 |
lemma hsgn_eq: "!!z. hsgn z = z / hcomplex_of_hypreal (hcmod z)" |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
522 |
by (transfer, rule sgn_eq) |
14314 | 523 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
524 |
lemma hcmod_i: "!!x y. hcmod (HComplex x y) = ( *f* sqrt) (x ^ 2 + y ^ 2)" |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
525 |
by (transfer, rule complex_mod) |
14314 | 526 |
|
14377 | 527 |
lemma hcomplex_eq_cancel_iff1 [simp]: |
528 |
"(hcomplex_of_hypreal xa = HComplex x y) = (xa = x & y = 0)" |
|
529 |
by (simp add: hcomplex_of_hypreal_eq) |
|
14314 | 530 |
|
14374 | 531 |
lemma hcomplex_eq_cancel_iff2 [simp]: |
14377 | 532 |
"(HComplex x y = hcomplex_of_hypreal xa) = (x = xa & y = 0)" |
533 |
by (simp add: hcomplex_of_hypreal_eq) |
|
14314 | 534 |
|
14377 | 535 |
lemma HComplex_eq_0 [simp]: "(HComplex x y = 0) = (x = 0 & y = 0)" |
536 |
by (insert hcomplex_eq_cancel_iff2 [of _ _ 0], simp) |
|
14314 | 537 |
|
14377 | 538 |
lemma HComplex_eq_1 [simp]: "(HComplex x y = 1) = (x = 1 & y = 0)" |
539 |
by (insert hcomplex_eq_cancel_iff2 [of _ _ 1], simp) |
|
14314 | 540 |
|
14377 | 541 |
lemma i_eq_HComplex_0_1: "iii = HComplex 0 1" |
542 |
by (insert hcomplex_of_hypreal_i [of 1], simp) |
|
14314 | 543 |
|
14377 | 544 |
lemma HComplex_eq_i [simp]: "(HComplex x y = iii) = (x = 0 & y = 1)" |
545 |
by (simp add: i_eq_HComplex_0_1) |
|
14314 | 546 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
547 |
lemma hRe_hsgn [simp]: "!!z. hRe(hsgn z) = hRe(z)/hcmod z" |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
548 |
by (transfer, simp) |
14314 | 549 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
550 |
lemma hIm_hsgn [simp]: "!!z. hIm(hsgn z) = hIm(z)/hcmod z" |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
551 |
by (transfer, simp) |
14314 | 552 |
|
15085
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15013
diff
changeset
|
553 |
(*????move to RealDef????*) |
14374 | 554 |
lemma real_two_squares_add_zero_iff [simp]: "(x*x + y*y = 0) = ((x::real) = 0 & y = 0)" |
15085
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15013
diff
changeset
|
555 |
by (auto intro: real_sum_squares_cancel iff: real_add_eq_0_iff) |
14314 | 556 |
|
14335 | 557 |
lemma hcomplex_inverse_complex_split: |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
558 |
"!!x y. inverse(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y) = |
14314 | 559 |
hcomplex_of_hypreal(x/(x ^ 2 + y ^ 2)) - |
560 |
iii * hcomplex_of_hypreal(y/(x ^ 2 + y ^ 2))" |
|
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
561 |
by (transfer, rule complex_inverse_complex_split) |
14374 | 562 |
|
14377 | 563 |
lemma HComplex_inverse: |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
564 |
"!!x y. inverse (HComplex x y) = |
14377 | 565 |
HComplex (x/(x ^ 2 + y ^ 2)) (-y/(x ^ 2 + y ^ 2))" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
566 |
by (transfer, rule complex_inverse) |
14377 | 567 |
|
14374 | 568 |
lemma hRe_mult_i_eq[simp]: |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
569 |
"!!y. hRe (iii * hcomplex_of_hypreal y) = 0" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
570 |
by (transfer, simp) |
14314 | 571 |
|
14374 | 572 |
lemma hIm_mult_i_eq [simp]: |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
573 |
"!!y. hIm (iii * hcomplex_of_hypreal y) = y" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
574 |
by (transfer, simp) |
14314 | 575 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
576 |
lemma hcmod_mult_i [simp]: "!!y. hcmod (iii * hcomplex_of_hypreal y) = abs y" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
577 |
by (transfer, simp) |
14314 | 578 |
|
14374 | 579 |
lemma hcmod_mult_i2 [simp]: "hcmod (hcomplex_of_hypreal y * iii) = abs y" |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
580 |
by (simp only: hcmod_mult_i mult_commute) |
14314 | 581 |
|
582 |
(*---------------------------------------------------------------------------*) |
|
583 |
(* harg *) |
|
584 |
(*---------------------------------------------------------------------------*) |
|
585 |
||
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
586 |
lemma harg: "harg (star_n X) = star_n (%n. arg (X n))" |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
587 |
by (simp add: harg_def starfun) |
14314 | 588 |
|
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
589 |
lemma cos_harg_i_mult_zero_pos: |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
590 |
"!!y. 0 < y ==> ( *f* cos) (harg(HComplex 0 y)) = 0" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
591 |
by (transfer, rule cos_arg_i_mult_zero_pos) |
14314 | 592 |
|
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
593 |
lemma cos_harg_i_mult_zero_neg: |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
594 |
"!!y. y < 0 ==> ( *f* cos) (harg(HComplex 0 y)) = 0" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
595 |
by (transfer, rule cos_arg_i_mult_zero_neg) |
14314 | 596 |
|
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
597 |
lemma cos_harg_i_mult_zero [simp]: |
14377 | 598 |
"y \<noteq> 0 ==> ( *f* cos) (harg(HComplex 0 y)) = 0" |
599 |
by (auto simp add: linorder_neq_iff |
|
600 |
cos_harg_i_mult_zero_pos cos_harg_i_mult_zero_neg) |
|
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
601 |
|
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
602 |
lemma hcomplex_of_hypreal_zero_iff [simp]: |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
603 |
"!!y. (hcomplex_of_hypreal y = 0) = (y = 0)" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
604 |
by (transfer, simp) |
14314 | 605 |
|
606 |
||
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
607 |
subsection{*Polar Form for Nonstandard Complex Numbers*} |
14314 | 608 |
|
14335 | 609 |
lemma complex_split_polar2: |
14377 | 610 |
"\<forall>n. \<exists>r a. (z n) = complex_of_real r * (Complex (cos a) (sin a))" |
611 |
by (blast intro: complex_split_polar) |
|
612 |
||
613 |
lemma lemma_hypreal_P_EX2: |
|
614 |
"(\<exists>(x::hypreal) y. P x y) = |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
615 |
(\<exists>f g. P (star_n f) (star_n g))" |
14377 | 616 |
apply auto |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
617 |
apply (rule_tac x = x in star_cases) |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
618 |
apply (rule_tac x = y in star_cases, auto) |
14314 | 619 |
done |
620 |
||
621 |
lemma hcomplex_split_polar: |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
622 |
"!!z. \<exists>r a. z = hcomplex_of_hypreal r * (HComplex(( *f* cos) a)(( *f* sin) a))" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
623 |
by (transfer, rule complex_split_polar) |
14314 | 624 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
625 |
lemma hcis: "hcis (star_n X) = star_n (%n. cis (X n))" |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
626 |
by (simp add: hcis_def starfun) |
14314 | 627 |
|
628 |
lemma hcis_eq: |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
629 |
"!!a. hcis a = |
14314 | 630 |
(hcomplex_of_hypreal(( *f* cos) a) + |
631 |
iii * hcomplex_of_hypreal(( *f* sin) a))" |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
632 |
by (transfer, simp add: cis_def) |
14314 | 633 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
634 |
lemma hrcis: "hrcis (star_n X) (star_n Y) = star_n (%n. rcis (X n) (Y n))" |
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17373
diff
changeset
|
635 |
by (simp add: hrcis_def starfun2_star_n) |
14314 | 636 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
637 |
lemma hrcis_Ex: "!!z. \<exists>r a. z = hrcis r a" |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
638 |
by (transfer, rule rcis_Ex) |
14314 | 639 |
|
14374 | 640 |
lemma hRe_hcomplex_polar [simp]: |
14377 | 641 |
"hRe (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = |
642 |
r * ( *f* cos) a" |
|
643 |
by (simp add: hcomplex_of_hypreal_mult_HComplex) |
|
14314 | 644 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
645 |
lemma hRe_hrcis [simp]: "!!r a. hRe(hrcis r a) = r * ( *f* cos) a" |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
646 |
by (transfer, rule Re_rcis) |
14314 | 647 |
|
14374 | 648 |
lemma hIm_hcomplex_polar [simp]: |
14377 | 649 |
"hIm (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = |
650 |
r * ( *f* sin) a" |
|
651 |
by (simp add: hcomplex_of_hypreal_mult_HComplex) |
|
14314 | 652 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
653 |
lemma hIm_hrcis [simp]: "!!r a. hIm(hrcis r a) = r * ( *f* sin) a" |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
654 |
by (transfer, rule Im_rcis) |
14314 | 655 |
|
14377 | 656 |
|
657 |
lemma hcmod_unit_one [simp]: |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
658 |
"!!a. hcmod (HComplex (( *f* cos) a) (( *f* sin) a)) = 1" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
659 |
by (transfer, simp) |
14377 | 660 |
|
14374 | 661 |
lemma hcmod_complex_polar [simp]: |
14377 | 662 |
"hcmod (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = |
663 |
abs r" |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
664 |
by (simp only: hcmod_mult hcmod_unit_one, simp) |
14314 | 665 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
666 |
lemma hcmod_hrcis [simp]: "!!r a. hcmod(hrcis r a) = abs r" |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
667 |
by (transfer, rule complex_mod_rcis) |
14314 | 668 |
|
669 |
(*---------------------------------------------------------------------------*) |
|
670 |
(* (r1 * hrcis a) * (r2 * hrcis b) = r1 * r2 * hrcis (a + b) *) |
|
671 |
(*---------------------------------------------------------------------------*) |
|
672 |
||
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
673 |
lemma hcis_hrcis_eq: "!!a. hcis a = hrcis 1 a" |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
674 |
by (transfer, rule cis_rcis_eq) |
14314 | 675 |
declare hcis_hrcis_eq [symmetric, simp] |
676 |
||
677 |
lemma hrcis_mult: |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
678 |
"!!a b r1 r2. hrcis r1 a * hrcis r2 b = hrcis (r1*r2) (a + b)" |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
679 |
by (transfer, rule rcis_mult) |
14314 | 680 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
681 |
lemma hcis_mult: "!!a b. hcis a * hcis b = hcis (a + b)" |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
682 |
by (transfer, rule cis_mult) |
14314 | 683 |
|
14374 | 684 |
lemma hcis_zero [simp]: "hcis 0 = 1" |
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
685 |
by (transfer, rule cis_zero) |
14314 | 686 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
687 |
lemma hrcis_zero_mod [simp]: "!!a. hrcis 0 a = 0" |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
688 |
by (transfer, rule rcis_zero_mod) |
14314 | 689 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
690 |
lemma hrcis_zero_arg [simp]: "!!r. hrcis r 0 = hcomplex_of_hypreal r" |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
691 |
by (transfer, rule rcis_zero_arg) |
14314 | 692 |
|
14374 | 693 |
lemma hcomplex_i_mult_minus [simp]: "iii * (iii * x) = - x" |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
694 |
by (simp add: mult_assoc [symmetric]) |
14314 | 695 |
|
14374 | 696 |
lemma hcomplex_i_mult_minus2 [simp]: "iii * iii * x = - x" |
697 |
by simp |
|
14314 | 698 |
|
699 |
lemma hcis_hypreal_of_nat_Suc_mult: |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
700 |
"!!a. hcis (hypreal_of_nat (Suc n) * a) = |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
701 |
hcis a * hcis (hypreal_of_nat n * a)" |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
702 |
apply (unfold hypreal_of_nat_def) |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
703 |
apply transfer |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
704 |
apply (fold real_of_nat_def) |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
705 |
apply (rule cis_real_of_nat_Suc_mult) |
14314 | 706 |
done |
707 |
||
708 |
lemma NSDeMoivre: "(hcis a) ^ n = hcis (hypreal_of_nat n * a)" |
|
709 |
apply (induct_tac "n") |
|
14374 | 710 |
apply (simp_all add: hcis_hypreal_of_nat_Suc_mult) |
14314 | 711 |
done |
712 |
||
14335 | 713 |
lemma hcis_hypreal_of_hypnat_Suc_mult: |
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
714 |
"!! a n. hcis (hypreal_of_hypnat (n + 1) * a) = |
14314 | 715 |
hcis a * hcis (hypreal_of_hypnat n * a)" |
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
716 |
by (transfer, simp add: cis_real_of_nat_Suc_mult) |
14314 | 717 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
718 |
lemma NSDeMoivre_ext: |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
719 |
"!!a n. (hcis a) hcpow n = hcis (hypreal_of_hypnat n * a)" |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
720 |
by (transfer, rule DeMoivre) |
14314 | 721 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
722 |
lemma NSDeMoivre2: |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
723 |
"!!a r. (hrcis r a) ^ n = hrcis (r ^ n) (hypreal_of_nat n * a)" |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
724 |
apply (unfold hypreal_of_nat_def) |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
725 |
apply transfer |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
726 |
apply (fold real_of_nat_def) |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
727 |
apply (rule DeMoivre2) |
14314 | 728 |
done |
729 |
||
730 |
lemma DeMoivre2_ext: |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
731 |
"!! a r n. (hrcis r a) hcpow n = hrcis (r pow n) (hypreal_of_hypnat n * a)" |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
732 |
by (transfer, rule DeMoivre2) |
14374 | 733 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
734 |
lemma hcis_inverse [simp]: "!!a. inverse(hcis a) = hcis (-a)" |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
735 |
by (transfer, simp) |
14314 | 736 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
737 |
lemma hrcis_inverse: "!!a r. inverse(hrcis r a) = hrcis (inverse r) (-a)" |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
738 |
by (transfer, simp add: rcis_inverse inverse_eq_divide [symmetric]) |
14314 | 739 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
740 |
lemma hRe_hcis [simp]: "!!a. hRe(hcis a) = ( *f* cos) a" |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
741 |
by (transfer, rule Re_cis) |
14314 | 742 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
743 |
lemma hIm_hcis [simp]: "!!a. hIm(hcis a) = ( *f* sin) a" |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
744 |
by (transfer, rule Im_cis) |
14314 | 745 |
|
14374 | 746 |
lemma cos_n_hRe_hcis_pow_n: "( *f* cos) (hypreal_of_nat n * a) = hRe(hcis a ^ n)" |
14377 | 747 |
by (simp add: NSDeMoivre) |
14314 | 748 |
|
14374 | 749 |
lemma sin_n_hIm_hcis_pow_n: "( *f* sin) (hypreal_of_nat n * a) = hIm(hcis a ^ n)" |
14377 | 750 |
by (simp add: NSDeMoivre) |
14314 | 751 |
|
14374 | 752 |
lemma cos_n_hRe_hcis_hcpow_n: "( *f* cos) (hypreal_of_hypnat n * a) = hRe(hcis a hcpow n)" |
14377 | 753 |
by (simp add: NSDeMoivre_ext) |
14314 | 754 |
|
14374 | 755 |
lemma sin_n_hIm_hcis_hcpow_n: "( *f* sin) (hypreal_of_hypnat n * a) = hIm(hcis a hcpow n)" |
14377 | 756 |
by (simp add: NSDeMoivre_ext) |
14314 | 757 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
758 |
lemma hexpi_add: "!!a b. hexpi(a + b) = hexpi(a) * hexpi(b)" |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
759 |
by (transfer, rule expi_add) |
14314 | 760 |
|
761 |
||
14374 | 762 |
subsection{*@{term hcomplex_of_complex}: the Injection from |
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
763 |
type @{typ complex} to to @{typ hcomplex}*} |
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
764 |
|
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
765 |
lemma inj_hcomplex_of_complex: "inj(hcomplex_of_complex)" |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
766 |
by (rule inj_onI, simp) |
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
767 |
|
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
768 |
lemma hcomplex_of_complex_i: "iii = hcomplex_of_complex ii" |
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
769 |
by (simp add: iii_def) |
14314 | 770 |
|
771 |
lemma hRe_hcomplex_of_complex: |
|
772 |
"hRe (hcomplex_of_complex z) = hypreal_of_real (Re z)" |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
773 |
by (transfer, rule refl) |
14314 | 774 |
|
775 |
lemma hIm_hcomplex_of_complex: |
|
776 |
"hIm (hcomplex_of_complex z) = hypreal_of_real (Im z)" |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
777 |
by (transfer, rule refl) |
14314 | 778 |
|
779 |
lemma hcmod_hcomplex_of_complex: |
|
780 |
"hcmod (hcomplex_of_complex x) = hypreal_of_real (cmod x)" |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
781 |
by (transfer, rule refl) |
14314 | 782 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
783 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
784 |
subsection{*Numerals and Arithmetic*} |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
785 |
|
20485 | 786 |
lemma hcomplex_number_of_def: "(number_of w :: hcomplex) == of_int w" |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
787 |
by (transfer, rule number_of_eq [THEN eq_reflection]) |
15013 | 788 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
789 |
lemma hcomplex_of_hypreal_eq_hcomplex_of_complex: |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
790 |
"hcomplex_of_hypreal (hypreal_of_real x) = |
15013 | 791 |
hcomplex_of_complex (complex_of_real x)" |
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
792 |
by (transfer, rule refl) |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
793 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
794 |
lemma hcomplex_hypreal_number_of: |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
795 |
"hcomplex_of_complex (number_of w) = hcomplex_of_hypreal(number_of w)" |
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
796 |
by (transfer, rule complex_number_of [symmetric]) |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
797 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
798 |
text{*This theorem is necessary because theorems such as |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
799 |
@{text iszero_number_of_0} only hold for ordered rings. They cannot |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
800 |
be generalized to fields in general because they fail for finite fields. |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
801 |
They work for type complex because the reals can be embedded in them.*} |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
802 |
lemma iszero_hcomplex_number_of [simp]: |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
803 |
"iszero (number_of w :: hcomplex) = iszero (number_of w :: real)" |
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
804 |
by (transfer iszero_def, simp) |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
805 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
806 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
807 |
(* |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
808 |
Goal "z + hcnj z = |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
809 |
hcomplex_of_hypreal (2 * hRe(z))" |
17300 | 810 |
by (res_inst_tac [("z","z")] eq_Abs_star 1); |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
811 |
by (auto_tac (claset(),HOL_ss addsimps [hRe,hcnj,star_n_add, |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
812 |
hypreal_mult,hcomplex_of_hypreal,complex_add_cnj])); |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
813 |
qed "star_n_add_hcnj"; |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
814 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
815 |
Goal "z - hcnj z = \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
816 |
\ hcomplex_of_hypreal (hypreal_of_real #2 * hIm(z)) * iii"; |
17300 | 817 |
by (res_inst_tac [("z","z")] eq_Abs_star 1); |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
818 |
by (auto_tac (claset(),simpset() addsimps [hIm,hcnj,hcomplex_diff, |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
819 |
hypreal_of_real_def,hypreal_mult,hcomplex_of_hypreal, |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
820 |
complex_diff_cnj,iii_def,star_n_mult])); |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
821 |
qed "hcomplex_diff_hcnj"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
822 |
*) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
823 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
824 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
825 |
(*** Real and imaginary stuff ***) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
826 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
827 |
(*Convert??? |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
828 |
Goalw [hcomplex_number_of_def] |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
829 |
"((number_of xa :: hcomplex) + iii * number_of ya = |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
830 |
number_of xb + iii * number_of yb) = |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
831 |
(((number_of xa :: hcomplex) = number_of xb) & |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
832 |
((number_of ya :: hcomplex) = number_of yb))" |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
833 |
by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff, |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
834 |
hcomplex_hypreal_number_of])); |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
835 |
qed "hcomplex_number_of_eq_cancel_iff"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
836 |
Addsimps [hcomplex_number_of_eq_cancel_iff]; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
837 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
838 |
Goalw [hcomplex_number_of_def] |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
839 |
"((number_of xa :: hcomplex) + number_of ya * iii = \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
840 |
\ number_of xb + number_of yb * iii) = \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
841 |
\ (((number_of xa :: hcomplex) = number_of xb) & \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
842 |
\ ((number_of ya :: hcomplex) = number_of yb))"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
843 |
by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iffA, |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
844 |
hcomplex_hypreal_number_of])); |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
845 |
qed "hcomplex_number_of_eq_cancel_iffA"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
846 |
Addsimps [hcomplex_number_of_eq_cancel_iffA]; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
847 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
848 |
Goalw [hcomplex_number_of_def] |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
849 |
"((number_of xa :: hcomplex) + number_of ya * iii = \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
850 |
\ number_of xb + iii * number_of yb) = \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
851 |
\ (((number_of xa :: hcomplex) = number_of xb) & \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
852 |
\ ((number_of ya :: hcomplex) = number_of yb))"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
853 |
by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iffB, |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
854 |
hcomplex_hypreal_number_of])); |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
855 |
qed "hcomplex_number_of_eq_cancel_iffB"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
856 |
Addsimps [hcomplex_number_of_eq_cancel_iffB]; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
857 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
858 |
Goalw [hcomplex_number_of_def] |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
859 |
"((number_of xa :: hcomplex) + iii * number_of ya = \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
860 |
\ number_of xb + number_of yb * iii) = \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
861 |
\ (((number_of xa :: hcomplex) = number_of xb) & \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
862 |
\ ((number_of ya :: hcomplex) = number_of yb))"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
863 |
by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iffC, |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
864 |
hcomplex_hypreal_number_of])); |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
865 |
qed "hcomplex_number_of_eq_cancel_iffC"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
866 |
Addsimps [hcomplex_number_of_eq_cancel_iffC]; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
867 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
868 |
Goalw [hcomplex_number_of_def] |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
869 |
"((number_of xa :: hcomplex) + iii * number_of ya = \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
870 |
\ number_of xb) = \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
871 |
\ (((number_of xa :: hcomplex) = number_of xb) & \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
872 |
\ ((number_of ya :: hcomplex) = 0))"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
873 |
by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff2, |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
874 |
hcomplex_hypreal_number_of,hcomplex_of_hypreal_zero_iff])); |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
875 |
qed "hcomplex_number_of_eq_cancel_iff2"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
876 |
Addsimps [hcomplex_number_of_eq_cancel_iff2]; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
877 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
878 |
Goalw [hcomplex_number_of_def] |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
879 |
"((number_of xa :: hcomplex) + number_of ya * iii = \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
880 |
\ number_of xb) = \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
881 |
\ (((number_of xa :: hcomplex) = number_of xb) & \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
882 |
\ ((number_of ya :: hcomplex) = 0))"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
883 |
by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff2a, |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
884 |
hcomplex_hypreal_number_of,hcomplex_of_hypreal_zero_iff])); |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
885 |
qed "hcomplex_number_of_eq_cancel_iff2a"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
886 |
Addsimps [hcomplex_number_of_eq_cancel_iff2a]; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
887 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
888 |
Goalw [hcomplex_number_of_def] |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
889 |
"((number_of xa :: hcomplex) + iii * number_of ya = \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
890 |
\ iii * number_of yb) = \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
891 |
\ (((number_of xa :: hcomplex) = 0) & \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
892 |
\ ((number_of ya :: hcomplex) = number_of yb))"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
893 |
by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff3, |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
894 |
hcomplex_hypreal_number_of,hcomplex_of_hypreal_zero_iff])); |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
895 |
qed "hcomplex_number_of_eq_cancel_iff3"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
896 |
Addsimps [hcomplex_number_of_eq_cancel_iff3]; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
897 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
898 |
Goalw [hcomplex_number_of_def] |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
899 |
"((number_of xa :: hcomplex) + number_of ya * iii= \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
900 |
\ iii * number_of yb) = \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
901 |
\ (((number_of xa :: hcomplex) = 0) & \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
902 |
\ ((number_of ya :: hcomplex) = number_of yb))"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
903 |
by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff3a, |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
904 |
hcomplex_hypreal_number_of,hcomplex_of_hypreal_zero_iff])); |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
905 |
qed "hcomplex_number_of_eq_cancel_iff3a"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
906 |
Addsimps [hcomplex_number_of_eq_cancel_iff3a]; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
907 |
*) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
908 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
909 |
lemma hcomplex_number_of_hcnj [simp]: |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
910 |
"hcnj (number_of v :: hcomplex) = number_of v" |
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
911 |
by (transfer, rule complex_number_of_cnj) |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
912 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
913 |
lemma hcomplex_number_of_hcmod [simp]: |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
914 |
"hcmod(number_of v :: hcomplex) = abs (number_of v :: hypreal)" |
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
915 |
by (transfer, rule complex_number_of_cmod) |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
916 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
917 |
lemma hcomplex_number_of_hRe [simp]: |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
918 |
"hRe(number_of v :: hcomplex) = number_of v" |
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
919 |
by (transfer, simp) |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
920 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
921 |
lemma hcomplex_number_of_hIm [simp]: |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
922 |
"hIm(number_of v :: hcomplex) = 0" |
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
923 |
by (transfer, simp) |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
924 |
|
13957 | 925 |
end |