author | huffman |
Thu, 14 Dec 2006 18:10:38 +0100 | |
changeset 21847 | 59a68ed9f2f2 |
parent 21839 | 54018ed3b99d |
child 21848 | b35faf14a89f |
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" |
13957 | 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" |
13957 | 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 |
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
89 |
hcomplex_of_hypreal_def hrcis_def hexpi_def HComplex_def hcpow_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: |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
466 |
"!!x n. hcomplex_of_hypreal (x pow n) = (hcomplex_of_hypreal x) hcpow n" |
20727 | 467 |
by transfer (rule complex_of_real_pow) |
14314 | 468 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
469 |
lemma hcmod_hcpow: "!!x n. hcmod(x hcpow 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: |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
501 |
"!!x n. (-x::hcomplex) hcpow n = |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
502 |
(if ( *p* even) n then (x hcpow n) else -(x hcpow 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: |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
506 |
"!!r s n. ((r::hcomplex) * s) hcpow n = (r hcpow n) * (s hcpow n)" |
20727 | 507 |
by transfer (rule power_mult_distrib) |
14314 | 508 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
509 |
lemma hcpow_zero [simp]: "!!n. 0 hcpow (n + 1) = 0" |
20727 | 510 |
by transfer simp |
14314 | 511 |
|
20727 | 512 |
lemma hcpow_zero2 [simp]: "!!n. 0 hcpow (hSuc n) = 0" |
21847
59a68ed9f2f2
redefine hSuc as *f* Suc, and move to HyperNat.thy
huffman
parents:
21839
diff
changeset
|
513 |
by transfer (rule power_0_Suc) |
14314 | 514 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
515 |
lemma hcpow_not_zero [simp,intro]: |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
516 |
"!!r n. r \<noteq> 0 ==> r hcpow n \<noteq> (0::hcomplex)" |
20727 | 517 |
by transfer (rule field_power_not_zero) |
14314 | 518 |
|
519 |
lemma hcpow_zero_zero: "r hcpow n = (0::hcomplex) ==> r = 0" |
|
14374 | 520 |
by (blast intro: ccontr dest: hcpow_not_zero) |
14314 | 521 |
|
522 |
subsection{*The Function @{term hsgn}*} |
|
523 |
||
14374 | 524 |
lemma hsgn_zero [simp]: "hsgn 0 = 0" |
20727 | 525 |
by transfer (rule sgn_zero) |
14314 | 526 |
|
14374 | 527 |
lemma hsgn_one [simp]: "hsgn 1 = 1" |
20727 | 528 |
by transfer (rule sgn_one) |
14314 | 529 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
530 |
lemma hsgn_minus: "!!z. hsgn (-z) = - hsgn(z)" |
20727 | 531 |
by transfer (rule sgn_minus) |
14314 | 532 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
533 |
lemma hsgn_eq: "!!z. hsgn z = z / hcomplex_of_hypreal (hcmod z)" |
20727 | 534 |
by transfer (rule sgn_eq) |
14314 | 535 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
536 |
lemma hcmod_i: "!!x y. hcmod (HComplex x y) = ( *f* sqrt) (x ^ 2 + y ^ 2)" |
20727 | 537 |
by transfer (rule complex_mod) |
14314 | 538 |
|
14377 | 539 |
lemma hcomplex_eq_cancel_iff1 [simp]: |
540 |
"(hcomplex_of_hypreal xa = HComplex x y) = (xa = x & y = 0)" |
|
541 |
by (simp add: hcomplex_of_hypreal_eq) |
|
14314 | 542 |
|
14374 | 543 |
lemma hcomplex_eq_cancel_iff2 [simp]: |
14377 | 544 |
"(HComplex x y = hcomplex_of_hypreal xa) = (x = xa & y = 0)" |
545 |
by (simp add: hcomplex_of_hypreal_eq) |
|
14314 | 546 |
|
20727 | 547 |
lemma HComplex_eq_0 [simp]: "!!x y. (HComplex x y = 0) = (x = 0 & y = 0)" |
548 |
by transfer (rule Complex_eq_0) |
|
14314 | 549 |
|
20727 | 550 |
lemma HComplex_eq_1 [simp]: "!!x y. (HComplex x y = 1) = (x = 1 & y = 0)" |
551 |
by transfer (rule Complex_eq_1) |
|
14314 | 552 |
|
14377 | 553 |
lemma i_eq_HComplex_0_1: "iii = HComplex 0 1" |
20727 | 554 |
by transfer (rule i_def [THEN meta_eq_to_obj_eq]) |
14314 | 555 |
|
20727 | 556 |
lemma HComplex_eq_i [simp]: "!!x y. (HComplex x y = iii) = (x = 0 & y = 1)" |
557 |
by transfer (rule Complex_eq_i) |
|
14314 | 558 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
559 |
lemma hRe_hsgn [simp]: "!!z. hRe(hsgn z) = hRe(z)/hcmod z" |
20727 | 560 |
by transfer (rule Re_sgn) |
14314 | 561 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
562 |
lemma hIm_hsgn [simp]: "!!z. hIm(hsgn z) = hIm(z)/hcmod z" |
20727 | 563 |
by transfer (rule Im_sgn) |
14314 | 564 |
|
15085
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15013
diff
changeset
|
565 |
(*????move to RealDef????*) |
14374 | 566 |
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
|
567 |
by (auto intro: real_sum_squares_cancel iff: real_add_eq_0_iff) |
14314 | 568 |
|
14335 | 569 |
lemma hcomplex_inverse_complex_split: |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
570 |
"!!x y. inverse(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y) = |
14314 | 571 |
hcomplex_of_hypreal(x/(x ^ 2 + y ^ 2)) - |
572 |
iii * hcomplex_of_hypreal(y/(x ^ 2 + y ^ 2))" |
|
20727 | 573 |
by transfer (rule complex_inverse_complex_split) |
14374 | 574 |
|
14377 | 575 |
lemma HComplex_inverse: |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
576 |
"!!x y. inverse (HComplex x y) = |
14377 | 577 |
HComplex (x/(x ^ 2 + y ^ 2)) (-y/(x ^ 2 + y ^ 2))" |
20727 | 578 |
by transfer (rule complex_inverse) |
14377 | 579 |
|
14374 | 580 |
lemma hRe_mult_i_eq[simp]: |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
581 |
"!!y. hRe (iii * hcomplex_of_hypreal y) = 0" |
20727 | 582 |
by transfer simp |
14314 | 583 |
|
14374 | 584 |
lemma hIm_mult_i_eq [simp]: |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
585 |
"!!y. hIm (iii * hcomplex_of_hypreal y) = y" |
20727 | 586 |
by transfer simp |
14314 | 587 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
588 |
lemma hcmod_mult_i [simp]: "!!y. hcmod (iii * hcomplex_of_hypreal y) = abs y" |
20727 | 589 |
by transfer simp |
14314 | 590 |
|
20727 | 591 |
lemma hcmod_mult_i2 [simp]: "!!y. hcmod (hcomplex_of_hypreal y * iii) = abs y" |
592 |
by transfer simp |
|
14314 | 593 |
|
594 |
(*---------------------------------------------------------------------------*) |
|
595 |
(* harg *) |
|
596 |
(*---------------------------------------------------------------------------*) |
|
597 |
||
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
598 |
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
|
599 |
"!!y. 0 < y ==> ( *f* cos) (harg(HComplex 0 y)) = 0" |
20727 | 600 |
by transfer (rule cos_arg_i_mult_zero_pos) |
14314 | 601 |
|
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
602 |
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
|
603 |
"!!y. y < 0 ==> ( *f* cos) (harg(HComplex 0 y)) = 0" |
20727 | 604 |
by transfer (rule cos_arg_i_mult_zero_neg) |
14314 | 605 |
|
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
606 |
lemma cos_harg_i_mult_zero [simp]: |
20727 | 607 |
"!!y. y \<noteq> 0 ==> ( *f* cos) (harg(HComplex 0 y)) = 0" |
608 |
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
|
609 |
|
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
610 |
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
|
611 |
"!!y. (hcomplex_of_hypreal y = 0) = (y = 0)" |
20727 | 612 |
by transfer (rule of_real_eq_0_iff) |
14314 | 613 |
|
614 |
||
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
615 |
subsection{*Polar Form for Nonstandard Complex Numbers*} |
14314 | 616 |
|
14335 | 617 |
lemma complex_split_polar2: |
14377 | 618 |
"\<forall>n. \<exists>r a. (z n) = complex_of_real r * (Complex (cos a) (sin a))" |
619 |
by (blast intro: complex_split_polar) |
|
620 |
||
14314 | 621 |
lemma hcomplex_split_polar: |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
622 |
"!!z. \<exists>r a. z = hcomplex_of_hypreal r * (HComplex(( *f* cos) a)(( *f* sin) a))" |
20727 | 623 |
by transfer (rule complex_split_polar) |
14314 | 624 |
|
625 |
lemma hcis_eq: |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
626 |
"!!a. hcis a = |
14314 | 627 |
(hcomplex_of_hypreal(( *f* cos) a) + |
628 |
iii * hcomplex_of_hypreal(( *f* sin) a))" |
|
20727 | 629 |
by transfer (simp add: cis_def) |
14314 | 630 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
631 |
lemma hrcis_Ex: "!!z. \<exists>r a. z = hrcis r a" |
20727 | 632 |
by transfer (rule rcis_Ex) |
14314 | 633 |
|
14374 | 634 |
lemma hRe_hcomplex_polar [simp]: |
20727 | 635 |
"!!r a. hRe (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = |
14377 | 636 |
r * ( *f* cos) a" |
20727 | 637 |
by transfer simp |
14314 | 638 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
639 |
lemma hRe_hrcis [simp]: "!!r a. hRe(hrcis r a) = r * ( *f* cos) a" |
20727 | 640 |
by transfer (rule Re_rcis) |
14314 | 641 |
|
14374 | 642 |
lemma hIm_hcomplex_polar [simp]: |
20727 | 643 |
"!!r a. hIm (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = |
14377 | 644 |
r * ( *f* sin) a" |
20727 | 645 |
by transfer simp |
14314 | 646 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
647 |
lemma hIm_hrcis [simp]: "!!r a. hIm(hrcis r a) = r * ( *f* sin) a" |
20727 | 648 |
by transfer (rule Im_rcis) |
14377 | 649 |
|
650 |
lemma hcmod_unit_one [simp]: |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
651 |
"!!a. hcmod (HComplex (( *f* cos) a) (( *f* sin) a)) = 1" |
20727 | 652 |
by transfer (rule cmod_unit_one) |
14377 | 653 |
|
14374 | 654 |
lemma hcmod_complex_polar [simp]: |
20727 | 655 |
"!!r a. hcmod (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = |
14377 | 656 |
abs r" |
20727 | 657 |
by transfer (rule cmod_complex_polar) |
14314 | 658 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
659 |
lemma hcmod_hrcis [simp]: "!!r a. hcmod(hrcis r a) = abs r" |
20727 | 660 |
by transfer (rule complex_mod_rcis) |
14314 | 661 |
|
662 |
(*---------------------------------------------------------------------------*) |
|
663 |
(* (r1 * hrcis a) * (r2 * hrcis b) = r1 * r2 * hrcis (a + b) *) |
|
664 |
(*---------------------------------------------------------------------------*) |
|
665 |
||
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
666 |
lemma hcis_hrcis_eq: "!!a. hcis a = hrcis 1 a" |
20727 | 667 |
by transfer (rule cis_rcis_eq) |
14314 | 668 |
declare hcis_hrcis_eq [symmetric, simp] |
669 |
||
670 |
lemma hrcis_mult: |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
671 |
"!!a b r1 r2. hrcis r1 a * hrcis r2 b = hrcis (r1*r2) (a + b)" |
20727 | 672 |
by transfer (rule rcis_mult) |
14314 | 673 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
674 |
lemma hcis_mult: "!!a b. hcis a * hcis b = hcis (a + b)" |
20727 | 675 |
by transfer (rule cis_mult) |
14314 | 676 |
|
14374 | 677 |
lemma hcis_zero [simp]: "hcis 0 = 1" |
20727 | 678 |
by transfer (rule cis_zero) |
14314 | 679 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
680 |
lemma hrcis_zero_mod [simp]: "!!a. hrcis 0 a = 0" |
20727 | 681 |
by transfer (rule rcis_zero_mod) |
14314 | 682 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
683 |
lemma hrcis_zero_arg [simp]: "!!r. hrcis r 0 = hcomplex_of_hypreal r" |
20727 | 684 |
by transfer (rule rcis_zero_arg) |
14314 | 685 |
|
20727 | 686 |
lemma hcomplex_i_mult_minus [simp]: "!!x. iii * (iii * x) = - x" |
687 |
by transfer (rule complex_i_mult_minus) |
|
14314 | 688 |
|
14374 | 689 |
lemma hcomplex_i_mult_minus2 [simp]: "iii * iii * x = - x" |
690 |
by simp |
|
14314 | 691 |
|
692 |
lemma hcis_hypreal_of_nat_Suc_mult: |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
693 |
"!!a. hcis (hypreal_of_nat (Suc n) * a) = |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
694 |
hcis a * hcis (hypreal_of_nat n * a)" |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
695 |
apply transfer |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
696 |
apply (fold real_of_nat_def) |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
697 |
apply (rule cis_real_of_nat_Suc_mult) |
14314 | 698 |
done |
699 |
||
20727 | 700 |
lemma NSDeMoivre: "!!a. (hcis a) ^ n = hcis (hypreal_of_nat n * a)" |
701 |
apply transfer |
|
702 |
apply (fold real_of_nat_def) |
|
703 |
apply (rule DeMoivre) |
|
14314 | 704 |
done |
705 |
||
14335 | 706 |
lemma hcis_hypreal_of_hypnat_Suc_mult: |
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
707 |
"!! a n. hcis (hypreal_of_hypnat (n + 1) * a) = |
14314 | 708 |
hcis a * hcis (hypreal_of_hypnat n * a)" |
20727 | 709 |
by transfer (simp add: cis_real_of_nat_Suc_mult) |
14314 | 710 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
711 |
lemma NSDeMoivre_ext: |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
712 |
"!!a n. (hcis a) hcpow n = hcis (hypreal_of_hypnat n * a)" |
20727 | 713 |
by transfer (rule DeMoivre) |
14314 | 714 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
715 |
lemma NSDeMoivre2: |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
716 |
"!!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
|
717 |
apply transfer |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
718 |
apply (fold real_of_nat_def) |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
719 |
apply (rule DeMoivre2) |
14314 | 720 |
done |
721 |
||
722 |
lemma DeMoivre2_ext: |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
723 |
"!! a r n. (hrcis r a) hcpow n = hrcis (r pow n) (hypreal_of_hypnat n * a)" |
20727 | 724 |
by transfer (rule DeMoivre2) |
14374 | 725 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
726 |
lemma hcis_inverse [simp]: "!!a. inverse(hcis a) = hcis (-a)" |
20727 | 727 |
by transfer (rule cis_inverse) |
14314 | 728 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
729 |
lemma hrcis_inverse: "!!a r. inverse(hrcis r a) = hrcis (inverse r) (-a)" |
20727 | 730 |
by transfer (simp add: rcis_inverse inverse_eq_divide [symmetric]) |
14314 | 731 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
732 |
lemma hRe_hcis [simp]: "!!a. hRe(hcis a) = ( *f* cos) a" |
20727 | 733 |
by transfer (rule Re_cis) |
14314 | 734 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
735 |
lemma hIm_hcis [simp]: "!!a. hIm(hcis a) = ( *f* sin) a" |
20727 | 736 |
by transfer (rule Im_cis) |
14314 | 737 |
|
14374 | 738 |
lemma cos_n_hRe_hcis_pow_n: "( *f* cos) (hypreal_of_nat n * a) = hRe(hcis a ^ n)" |
14377 | 739 |
by (simp add: NSDeMoivre) |
14314 | 740 |
|
14374 | 741 |
lemma sin_n_hIm_hcis_pow_n: "( *f* sin) (hypreal_of_nat n * a) = hIm(hcis a ^ n)" |
14377 | 742 |
by (simp add: NSDeMoivre) |
14314 | 743 |
|
14374 | 744 |
lemma cos_n_hRe_hcis_hcpow_n: "( *f* cos) (hypreal_of_hypnat n * a) = hRe(hcis a hcpow n)" |
14377 | 745 |
by (simp add: NSDeMoivre_ext) |
14314 | 746 |
|
14374 | 747 |
lemma sin_n_hIm_hcis_hcpow_n: "( *f* sin) (hypreal_of_hypnat n * a) = hIm(hcis a hcpow n)" |
14377 | 748 |
by (simp add: NSDeMoivre_ext) |
14314 | 749 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
750 |
lemma hexpi_add: "!!a b. hexpi(a + b) = hexpi(a) * hexpi(b)" |
20727 | 751 |
by transfer (rule expi_add) |
14314 | 752 |
|
753 |
||
14374 | 754 |
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
|
755 |
type @{typ complex} to to @{typ hcomplex}*} |
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
756 |
|
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
757 |
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
|
758 |
by (rule inj_onI, simp) |
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
759 |
|
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
760 |
lemma hcomplex_of_complex_i: "iii = hcomplex_of_complex ii" |
20727 | 761 |
by (rule iii_def) |
14314 | 762 |
|
763 |
lemma hRe_hcomplex_of_complex: |
|
764 |
"hRe (hcomplex_of_complex z) = hypreal_of_real (Re z)" |
|
20727 | 765 |
by transfer (rule refl) |
14314 | 766 |
|
767 |
lemma hIm_hcomplex_of_complex: |
|
768 |
"hIm (hcomplex_of_complex z) = hypreal_of_real (Im z)" |
|
20727 | 769 |
by transfer (rule refl) |
14314 | 770 |
|
771 |
lemma hcmod_hcomplex_of_complex: |
|
772 |
"hcmod (hcomplex_of_complex x) = hypreal_of_real (cmod x)" |
|
20727 | 773 |
by transfer (rule refl) |
14314 | 774 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
775 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
776 |
subsection{*Numerals and Arithmetic*} |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
777 |
|
20485 | 778 |
lemma hcomplex_number_of_def: "(number_of w :: hcomplex) == of_int w" |
20727 | 779 |
by transfer (rule number_of_eq [THEN eq_reflection]) |
15013 | 780 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
781 |
lemma hcomplex_of_hypreal_eq_hcomplex_of_complex: |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
782 |
"hcomplex_of_hypreal (hypreal_of_real x) = |
15013 | 783 |
hcomplex_of_complex (complex_of_real x)" |
20727 | 784 |
by transfer (rule refl) |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
785 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
786 |
lemma hcomplex_hypreal_number_of: |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
787 |
"hcomplex_of_complex (number_of w) = hcomplex_of_hypreal(number_of w)" |
20727 | 788 |
by transfer (rule complex_number_of [symmetric]) |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
789 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
790 |
text{*This theorem is necessary because theorems such as |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
791 |
@{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
|
792 |
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
|
793 |
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
|
794 |
lemma iszero_hcomplex_number_of [simp]: |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
795 |
"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
|
796 |
by (transfer iszero_def, simp) |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
797 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
798 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
799 |
(* |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
800 |
Goal "z + hcnj z = |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
801 |
hcomplex_of_hypreal (2 * hRe(z))" |
17300 | 802 |
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
|
803 |
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
|
804 |
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
|
805 |
qed "star_n_add_hcnj"; |
14387
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 (hypreal_of_real #2 * hIm(z)) * iii"; |
17300 | 809 |
by (res_inst_tac [("z","z")] eq_Abs_star 1); |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
810 |
by (auto_tac (claset(),simpset() addsimps [hIm,hcnj,hcomplex_diff, |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
811 |
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
|
812 |
complex_diff_cnj,iii_def,star_n_mult])); |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
813 |
qed "hcomplex_diff_hcnj"; |
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 |
|
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 |
(*** Real and imaginary stuff ***) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
818 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
819 |
(*Convert??? |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
820 |
Goalw [hcomplex_number_of_def] |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
821 |
"((number_of xa :: hcomplex) + iii * number_of ya = |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
822 |
number_of xb + iii * number_of yb) = |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
823 |
(((number_of xa :: hcomplex) = number_of xb) & |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
824 |
((number_of ya :: hcomplex) = number_of yb))" |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
825 |
by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff, |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
826 |
hcomplex_hypreal_number_of])); |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
827 |
qed "hcomplex_number_of_eq_cancel_iff"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
828 |
Addsimps [hcomplex_number_of_eq_cancel_iff]; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
829 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
830 |
Goalw [hcomplex_number_of_def] |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
831 |
"((number_of xa :: hcomplex) + number_of ya * iii = \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
832 |
\ number_of xb + number_of yb * iii) = \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
833 |
\ (((number_of xa :: hcomplex) = number_of xb) & \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
834 |
\ ((number_of ya :: hcomplex) = number_of yb))"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
835 |
by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iffA, |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
836 |
hcomplex_hypreal_number_of])); |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
837 |
qed "hcomplex_number_of_eq_cancel_iffA"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
838 |
Addsimps [hcomplex_number_of_eq_cancel_iffA]; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
839 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
840 |
Goalw [hcomplex_number_of_def] |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
841 |
"((number_of xa :: hcomplex) + number_of ya * iii = \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
842 |
\ number_of xb + iii * number_of yb) = \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
843 |
\ (((number_of xa :: hcomplex) = number_of xb) & \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
844 |
\ ((number_of ya :: hcomplex) = number_of yb))"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
845 |
by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iffB, |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
846 |
hcomplex_hypreal_number_of])); |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
847 |
qed "hcomplex_number_of_eq_cancel_iffB"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
848 |
Addsimps [hcomplex_number_of_eq_cancel_iffB]; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
849 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
850 |
Goalw [hcomplex_number_of_def] |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
851 |
"((number_of xa :: hcomplex) + iii * number_of ya = \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
852 |
\ number_of xb + number_of yb * iii) = \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
853 |
\ (((number_of xa :: hcomplex) = number_of xb) & \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
854 |
\ ((number_of ya :: hcomplex) = number_of yb))"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
855 |
by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iffC, |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
856 |
hcomplex_hypreal_number_of])); |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
857 |
qed "hcomplex_number_of_eq_cancel_iffC"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
858 |
Addsimps [hcomplex_number_of_eq_cancel_iffC]; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
859 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
860 |
Goalw [hcomplex_number_of_def] |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
861 |
"((number_of xa :: hcomplex) + iii * number_of ya = \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
862 |
\ number_of xb) = \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
863 |
\ (((number_of xa :: hcomplex) = number_of xb) & \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
864 |
\ ((number_of ya :: hcomplex) = 0))"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
865 |
by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff2, |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
866 |
hcomplex_hypreal_number_of,hcomplex_of_hypreal_zero_iff])); |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
867 |
qed "hcomplex_number_of_eq_cancel_iff2"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
868 |
Addsimps [hcomplex_number_of_eq_cancel_iff2]; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
869 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
870 |
Goalw [hcomplex_number_of_def] |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
871 |
"((number_of xa :: hcomplex) + number_of ya * iii = \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
872 |
\ number_of xb) = \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
873 |
\ (((number_of xa :: hcomplex) = number_of xb) & \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
874 |
\ ((number_of ya :: hcomplex) = 0))"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
875 |
by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff2a, |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
876 |
hcomplex_hypreal_number_of,hcomplex_of_hypreal_zero_iff])); |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
877 |
qed "hcomplex_number_of_eq_cancel_iff2a"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
878 |
Addsimps [hcomplex_number_of_eq_cancel_iff2a]; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
879 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
880 |
Goalw [hcomplex_number_of_def] |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
881 |
"((number_of xa :: hcomplex) + iii * number_of ya = \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
882 |
\ iii * number_of yb) = \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
883 |
\ (((number_of xa :: hcomplex) = 0) & \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
884 |
\ ((number_of ya :: hcomplex) = number_of yb))"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
885 |
by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff3, |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
886 |
hcomplex_hypreal_number_of,hcomplex_of_hypreal_zero_iff])); |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
887 |
qed "hcomplex_number_of_eq_cancel_iff3"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
888 |
Addsimps [hcomplex_number_of_eq_cancel_iff3]; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
889 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
890 |
Goalw [hcomplex_number_of_def] |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
891 |
"((number_of xa :: hcomplex) + number_of ya * iii= \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
892 |
\ iii * number_of yb) = \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
893 |
\ (((number_of xa :: hcomplex) = 0) & \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
894 |
\ ((number_of ya :: hcomplex) = number_of yb))"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
895 |
by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff3a, |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
896 |
hcomplex_hypreal_number_of,hcomplex_of_hypreal_zero_iff])); |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
897 |
qed "hcomplex_number_of_eq_cancel_iff3a"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
898 |
Addsimps [hcomplex_number_of_eq_cancel_iff3a]; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
899 |
*) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
900 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
901 |
lemma hcomplex_number_of_hcnj [simp]: |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
902 |
"hcnj (number_of v :: hcomplex) = number_of v" |
20727 | 903 |
by transfer (rule complex_number_of_cnj) |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
904 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
905 |
lemma hcomplex_number_of_hcmod [simp]: |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
906 |
"hcmod(number_of v :: hcomplex) = abs (number_of v :: hypreal)" |
20727 | 907 |
by transfer (rule complex_number_of_cmod) |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
908 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
909 |
lemma hcomplex_number_of_hRe [simp]: |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
910 |
"hRe(number_of v :: hcomplex) = number_of v" |
20727 | 911 |
by transfer (rule complex_number_of_Re) |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
912 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
913 |
lemma hcomplex_number_of_hIm [simp]: |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
914 |
"hIm(number_of v :: hcomplex) = 0" |
20727 | 915 |
by transfer (rule complex_number_of_Im) |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
916 |
|
13957 | 917 |
end |