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