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