author | haftmann |
Wed, 31 Oct 2007 10:10:50 +0100 | |
changeset 25247 | 7bacd1798fc4 |
parent 23126 | 93f8cb025afd |
child 27148 | 5b78e50adc49 |
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 |
22655 | 11 |
imports Complex "../Hyperreal/NSA" |
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 |
||
22883
005be8dafce0
hcomplex_of_hypreal abbreviates of_hypreal; removed redundant lemmas
huffman
parents:
22860
diff
changeset
|
65 |
abbreviation |
005be8dafce0
hcomplex_of_hypreal abbreviates of_hypreal; removed redundant lemmas
huffman
parents:
22860
diff
changeset
|
66 |
hcomplex_of_hypreal :: "hypreal \<Rightarrow> hcomplex" where |
005be8dafce0
hcomplex_of_hypreal abbreviates of_hypreal; removed redundant lemmas
huffman
parents:
22860
diff
changeset
|
67 |
"hcomplex_of_hypreal \<equiv> of_hypreal" |
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" |
22890 | 82 |
|
17332
4910cf8c0cd2
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents:
17318
diff
changeset
|
83 |
lemmas hcomplex_defs [transfer_unfold] = |
20558 | 84 |
hRe_def hIm_def iii_def hcnj_def hsgn_def harg_def hcis_def |
22883
005be8dafce0
hcomplex_of_hypreal abbreviates of_hypreal; removed redundant lemmas
huffman
parents:
22860
diff
changeset
|
85 |
hrcis_def hexpi_def HComplex_def |
14374 | 86 |
|
21839
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21404
diff
changeset
|
87 |
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
|
88 |
by (simp add: hcomplex_defs) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21404
diff
changeset
|
89 |
|
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21404
diff
changeset
|
90 |
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
|
91 |
by (simp add: hcomplex_defs) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21404
diff
changeset
|
92 |
|
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21404
diff
changeset
|
93 |
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
|
94 |
by (simp add: hcomplex_defs) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21404
diff
changeset
|
95 |
|
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21404
diff
changeset
|
96 |
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
|
97 |
by (simp add: hcomplex_defs) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21404
diff
changeset
|
98 |
|
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21404
diff
changeset
|
99 |
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
|
100 |
by (simp add: hcomplex_defs) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21404
diff
changeset
|
101 |
|
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21404
diff
changeset
|
102 |
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
|
103 |
by (simp add: hcomplex_defs) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21404
diff
changeset
|
104 |
|
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21404
diff
changeset
|
105 |
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
|
106 |
by (simp add: hcomplex_defs) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21404
diff
changeset
|
107 |
|
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21404
diff
changeset
|
108 |
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
|
109 |
by (simp add: hcomplex_defs) |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21404
diff
changeset
|
110 |
|
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21404
diff
changeset
|
111 |
lemma Standard_hrcis [simp]: |
54018ed3b99d
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
huffman
parents:
21404
diff
changeset
|
112 |
"\<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
|
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_HComplex [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> HComplex 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 |
|
20558 | 119 |
lemma hcmod_def: "hcmod = *f* cmod" |
120 |
by (rule hnorm_def) |
|
121 |
||
14314 | 122 |
|
123 |
subsection{*Properties of Nonstandard Real and Imaginary Parts*} |
|
124 |
||
14335 | 125 |
lemma hcomplex_hRe_hIm_cancel_iff: |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
126 |
"!!w z. (w=z) = (hRe(w) = hRe(z) & hIm(w) = hIm(z))" |
20727 | 127 |
by transfer (rule complex_Re_Im_cancel_iff) |
14314 | 128 |
|
20727 | 129 |
lemma hcomplex_equality [intro?]: |
130 |
"!!z w. hRe z = hRe w ==> hIm z = hIm w ==> z = w" |
|
131 |
by transfer (rule complex_equality) |
|
14377 | 132 |
|
14374 | 133 |
lemma hcomplex_hRe_zero [simp]: "hRe 0 = 0" |
20727 | 134 |
by transfer (rule complex_Re_zero) |
14314 | 135 |
|
14374 | 136 |
lemma hcomplex_hIm_zero [simp]: "hIm 0 = 0" |
20727 | 137 |
by transfer (rule complex_Im_zero) |
14314 | 138 |
|
14374 | 139 |
lemma hcomplex_hRe_one [simp]: "hRe 1 = 1" |
20727 | 140 |
by transfer (rule complex_Re_one) |
14314 | 141 |
|
14374 | 142 |
lemma hcomplex_hIm_one [simp]: "hIm 1 = 0" |
20727 | 143 |
by transfer (rule complex_Im_one) |
14314 | 144 |
|
145 |
||
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
146 |
subsection{*Addition for Nonstandard Complex Numbers*} |
14314 | 147 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
148 |
lemma hRe_add: "!!x y. hRe(x + y) = hRe(x) + hRe(y)" |
20727 | 149 |
by transfer (rule complex_Re_add) |
14314 | 150 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
151 |
lemma hIm_add: "!!x y. hIm(x + y) = hIm(x) + hIm(y)" |
20727 | 152 |
by transfer (rule complex_Im_add) |
14374 | 153 |
|
14318 | 154 |
subsection{*More Minus Laws*} |
155 |
||
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
156 |
lemma hRe_minus: "!!z. hRe(-z) = - hRe(z)" |
20727 | 157 |
by transfer (rule complex_Re_minus) |
14318 | 158 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
159 |
lemma hIm_minus: "!!z. hIm(-z) = - hIm(z)" |
20727 | 160 |
by transfer (rule complex_Im_minus) |
14318 | 161 |
|
162 |
lemma hcomplex_add_minus_eq_minus: |
|
163 |
"x + y = (0::hcomplex) ==> x = -y" |
|
14738 | 164 |
apply (drule OrderedGroup.equals_zero_I) |
14374 | 165 |
apply (simp add: minus_equation_iff [of x y]) |
14318 | 166 |
done |
167 |
||
14377 | 168 |
lemma hcomplex_i_mult_eq [simp]: "iii * iii = - 1" |
20727 | 169 |
by transfer (rule i_mult_eq2) |
14377 | 170 |
|
20727 | 171 |
lemma hcomplex_i_mult_left [simp]: "!!z. iii * (iii * z) = -z" |
172 |
by transfer (rule complex_i_mult_minus) |
|
14377 | 173 |
|
174 |
lemma hcomplex_i_not_zero [simp]: "iii \<noteq> 0" |
|
20727 | 175 |
by transfer (rule complex_i_not_zero) |
14377 | 176 |
|
14318 | 177 |
|
178 |
subsection{*More Multiplication Laws*} |
|
179 |
||
20727 | 180 |
lemma hcomplex_mult_minus_one: "- 1 * (z::hcomplex) = -z" |
14374 | 181 |
by simp |
14318 | 182 |
|
20727 | 183 |
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
|
184 |
by simp |
14318 | 185 |
|
14335 | 186 |
lemma hcomplex_mult_left_cancel: |
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
187 |
"(c::hcomplex) \<noteq> (0::hcomplex) ==> (c*a=c*b) = (a=b)" |
20727 | 188 |
by simp |
14314 | 189 |
|
14335 | 190 |
lemma hcomplex_mult_right_cancel: |
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
191 |
"(c::hcomplex) \<noteq> (0::hcomplex) ==> (a*c=b*c) = (a=b)" |
20727 | 192 |
by simp |
14314 | 193 |
|
194 |
||
14318 | 195 |
subsection{*Subraction and Division*} |
14314 | 196 |
|
14374 | 197 |
lemma hcomplex_diff_eq_eq [simp]: "((x::hcomplex) - y = z) = (x = z + y)" |
22883
005be8dafce0
hcomplex_of_hypreal abbreviates of_hypreal; removed redundant lemmas
huffman
parents:
22860
diff
changeset
|
198 |
(* TODO: delete *) |
14738 | 199 |
by (rule OrderedGroup.diff_eq_eq) |
14314 | 200 |
|
201 |
||
202 |
subsection{*Embedding Properties for @{term hcomplex_of_hypreal} Map*} |
|
203 |
||
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
204 |
lemma hRe_hcomplex_of_hypreal [simp]: "!!z. hRe(hcomplex_of_hypreal z) = z" |
20727 | 205 |
by transfer (rule Re_complex_of_real) |
14314 | 206 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
207 |
lemma hIm_hcomplex_of_hypreal [simp]: "!!z. hIm(hcomplex_of_hypreal z) = 0" |
20727 | 208 |
by transfer (rule Im_complex_of_real) |
14314 | 209 |
|
14374 | 210 |
lemma hcomplex_of_hypreal_epsilon_not_zero [simp]: |
211 |
"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
|
212 |
by (simp add: hypreal_epsilon_not_zero) |
14318 | 213 |
|
14377 | 214 |
subsection{*HComplex theorems*} |
215 |
||
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
216 |
lemma hRe_HComplex [simp]: "!!x y. hRe (HComplex x y) = x" |
20727 | 217 |
by transfer (rule Re) |
14377 | 218 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
219 |
lemma hIm_HComplex [simp]: "!!x y. hIm (HComplex x y) = y" |
20727 | 220 |
by transfer (rule Im) |
14377 | 221 |
|
20727 | 222 |
lemma hcomplex_surj [simp]: "!!z. HComplex (hRe z) (hIm z) = z" |
223 |
by transfer (rule complex_surj) |
|
14377 | 224 |
|
17300 | 225 |
lemma hcomplex_induct [case_names rect(*, induct type: hcomplex*)]: |
14377 | 226 |
"(\<And>x y. P (HComplex x y)) ==> P z" |
227 |
by (rule hcomplex_surj [THEN subst], blast) |
|
228 |
||
229 |
||
14318 | 230 |
subsection{*Modulus (Absolute Value) of Nonstandard Complex Number*} |
14314 | 231 |
|
14335 | 232 |
lemma hcomplex_of_hypreal_abs: |
233 |
"hcomplex_of_hypreal (abs x) = |
|
14314 | 234 |
hcomplex_of_hypreal(hcmod(hcomplex_of_hypreal x))" |
14374 | 235 |
by simp |
14314 | 236 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
237 |
lemma HComplex_inject [simp]: |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
238 |
"!!x y x' y'. HComplex x y = HComplex x' y' = (x=x' & y=y')" |
20727 | 239 |
by transfer (rule complex.inject) |
14377 | 240 |
|
241 |
lemma HComplex_add [simp]: |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
242 |
"!!x1 y1 x2 y2. HComplex x1 y1 + HComplex x2 y2 = HComplex (x1+x2) (y1+y2)" |
20727 | 243 |
by transfer (rule complex_add) |
14377 | 244 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
245 |
lemma HComplex_minus [simp]: "!!x y. - HComplex x y = HComplex (-x) (-y)" |
20727 | 246 |
by transfer (rule complex_minus) |
14377 | 247 |
|
248 |
lemma HComplex_diff [simp]: |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
249 |
"!!x1 y1 x2 y2. HComplex x1 y1 - HComplex x2 y2 = HComplex (x1-x2) (y1-y2)" |
20727 | 250 |
by transfer (rule complex_diff) |
14377 | 251 |
|
252 |
lemma HComplex_mult [simp]: |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
253 |
"!!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
|
254 |
HComplex (x1*x2 - y1*y2) (x1*y2 + y1*x2)" |
20727 | 255 |
by transfer (rule complex_mult) |
14377 | 256 |
|
257 |
(*HComplex_inverse is proved below*) |
|
258 |
||
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
259 |
lemma hcomplex_of_hypreal_eq: "!!r. hcomplex_of_hypreal r = HComplex r 0" |
20727 | 260 |
by transfer (rule complex_of_real_def) |
14377 | 261 |
|
262 |
lemma HComplex_add_hcomplex_of_hypreal [simp]: |
|
20727 | 263 |
"!!x y r. HComplex x y + hcomplex_of_hypreal r = HComplex (x+r) y" |
264 |
by transfer (rule Complex_add_complex_of_real) |
|
14377 | 265 |
|
266 |
lemma hcomplex_of_hypreal_add_HComplex [simp]: |
|
20727 | 267 |
"!!r x y. hcomplex_of_hypreal r + HComplex x y = HComplex (r+x) y" |
268 |
by transfer (rule complex_of_real_add_Complex) |
|
14377 | 269 |
|
270 |
lemma HComplex_mult_hcomplex_of_hypreal: |
|
20727 | 271 |
"!!x y r. HComplex x y * hcomplex_of_hypreal r = HComplex (x*r) (y*r)" |
272 |
by transfer (rule Complex_mult_complex_of_real) |
|
14377 | 273 |
|
274 |
lemma hcomplex_of_hypreal_mult_HComplex: |
|
20727 | 275 |
"!!r x y. hcomplex_of_hypreal r * HComplex x y = HComplex (r*x) (r*y)" |
276 |
by transfer (rule complex_of_real_mult_Complex) |
|
14377 | 277 |
|
278 |
lemma i_hcomplex_of_hypreal [simp]: |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
279 |
"!!r. iii * hcomplex_of_hypreal r = HComplex 0 r" |
20727 | 280 |
by transfer (rule i_complex_of_real) |
14377 | 281 |
|
282 |
lemma hcomplex_of_hypreal_i [simp]: |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
283 |
"!!r. hcomplex_of_hypreal r * iii = HComplex 0 r" |
20727 | 284 |
by transfer (rule complex_of_real_i) |
14377 | 285 |
|
14314 | 286 |
|
287 |
subsection{*Conjugation*} |
|
288 |
||
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
289 |
lemma hcomplex_hcnj_cancel_iff [iff]: "!!x y. (hcnj x = hcnj y) = (x = y)" |
20727 | 290 |
by transfer (rule complex_cnj_cancel_iff) |
14374 | 291 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
292 |
lemma hcomplex_hcnj_hcnj [simp]: "!!z. hcnj (hcnj z) = z" |
20727 | 293 |
by transfer (rule complex_cnj_cnj) |
14314 | 294 |
|
14374 | 295 |
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
|
296 |
"!!x. hcnj (hcomplex_of_hypreal x) = hcomplex_of_hypreal x" |
20727 | 297 |
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
|
298 |
|
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
299 |
lemma hcomplex_hmod_hcnj [simp]: "!!z. hcmod (hcnj z) = hcmod z" |
20727 | 300 |
by transfer (rule complex_mod_cnj) |
14314 | 301 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
302 |
lemma hcomplex_hcnj_minus: "!!z. hcnj (-z) = - hcnj z" |
20727 | 303 |
by transfer (rule complex_cnj_minus) |
14314 | 304 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
305 |
lemma hcomplex_hcnj_inverse: "!!z. hcnj(inverse z) = inverse(hcnj z)" |
20727 | 306 |
by transfer (rule complex_cnj_inverse) |
14314 | 307 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
308 |
lemma hcomplex_hcnj_add: "!!w z. hcnj(w + z) = hcnj(w) + hcnj(z)" |
20727 | 309 |
by transfer (rule complex_cnj_add) |
14314 | 310 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
311 |
lemma hcomplex_hcnj_diff: "!!w z. hcnj(w - z) = hcnj(w) - hcnj(z)" |
20727 | 312 |
by transfer (rule complex_cnj_diff) |
14314 | 313 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
314 |
lemma hcomplex_hcnj_mult: "!!w z. hcnj(w * z) = hcnj(w) * hcnj(z)" |
20727 | 315 |
by transfer (rule complex_cnj_mult) |
14314 | 316 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
317 |
lemma hcomplex_hcnj_divide: "!!w z. hcnj(w / z) = (hcnj w)/(hcnj z)" |
20727 | 318 |
by transfer (rule complex_cnj_divide) |
14314 | 319 |
|
14374 | 320 |
lemma hcnj_one [simp]: "hcnj 1 = 1" |
20727 | 321 |
by transfer (rule complex_cnj_one) |
14314 | 322 |
|
14374 | 323 |
lemma hcomplex_hcnj_zero [simp]: "hcnj 0 = 0" |
20727 | 324 |
by transfer (rule complex_cnj_zero) |
14374 | 325 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
326 |
lemma hcomplex_hcnj_zero_iff [iff]: "!!z. (hcnj z = 0) = (z = 0)" |
20727 | 327 |
by transfer (rule complex_cnj_zero_iff) |
14314 | 328 |
|
14335 | 329 |
lemma hcomplex_mult_hcnj: |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
330 |
"!!z. z * hcnj z = hcomplex_of_hypreal (hRe(z) ^ 2 + hIm(z) ^ 2)" |
20727 | 331 |
by transfer (rule complex_mult_cnj) |
14314 | 332 |
|
333 |
||
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
334 |
subsection{*More Theorems about the Function @{term hcmod}*} |
14314 | 335 |
|
14374 | 336 |
lemma hcmod_hcomplex_of_hypreal_of_nat [simp]: |
14335 | 337 |
"hcmod (hcomplex_of_hypreal(hypreal_of_nat n)) = hypreal_of_nat n" |
20727 | 338 |
by simp |
14314 | 339 |
|
14374 | 340 |
lemma hcmod_hcomplex_of_hypreal_of_hypnat [simp]: |
14335 | 341 |
"hcmod (hcomplex_of_hypreal(hypreal_of_hypnat n)) = hypreal_of_hypnat n" |
20727 | 342 |
by simp |
14314 | 343 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
344 |
lemma hcmod_mult_hcnj: "!!z. hcmod(z * hcnj(z)) = hcmod(z) ^ 2" |
20727 | 345 |
by transfer (rule complex_mod_mult_cnj) |
14314 | 346 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
347 |
lemma hcmod_triangle_ineq2 [simp]: |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
348 |
"!!a b. hcmod(b + a) - hcmod b \<le> hcmod a" |
20727 | 349 |
by transfer (rule complex_mod_triangle_ineq2) |
14314 | 350 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
351 |
lemma hcmod_diff_ineq [simp]: "!!a b. hcmod(a) - hcmod(b) \<le> hcmod(a + b)" |
22914 | 352 |
by transfer (rule norm_diff_ineq) |
14314 | 353 |
|
354 |
||
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
355 |
subsection{*Exponentiation*} |
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
356 |
|
17300 | 357 |
lemma hcomplexpow_0 [simp]: "z ^ 0 = (1::hcomplex)" |
358 |
by (rule power_0) |
|
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
359 |
|
17300 | 360 |
lemma hcomplexpow_Suc [simp]: "z ^ (Suc n) = (z::hcomplex) * (z ^ n)" |
361 |
by (rule power_Suc) |
|
362 |
||
23126 | 363 |
lemma hcomplexpow_i_squared [simp]: "iii ^ 2 = -1" |
364 |
by transfer (rule power2_i) |
|
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
365 |
|
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
366 |
lemma hcomplex_of_hypreal_pow: |
20727 | 367 |
"!!x. hcomplex_of_hypreal (x ^ n) = (hcomplex_of_hypreal x) ^ n" |
368 |
by transfer (rule of_real_power) |
|
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
369 |
|
20727 | 370 |
lemma hcomplex_hcnj_pow: "!!z. hcnj(z ^ n) = hcnj(z) ^ n" |
23126 | 371 |
by transfer (rule complex_cnj_power) |
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
372 |
|
20727 | 373 |
lemma hcmod_hcomplexpow: "!!x. hcmod(x ^ n) = hcmod(x) ^ n" |
374 |
by transfer (rule norm_power) |
|
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
375 |
|
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
376 |
lemma hcpow_minus: |
21848 | 377 |
"!!x n. (-x::hcomplex) pow n = |
378 |
(if ( *p* even) n then (x pow n) else -(x pow n))" |
|
20727 | 379 |
by transfer (rule neg_power_if) |
14314 | 380 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
381 |
lemma hcpow_mult: |
21848 | 382 |
"!!r s n. ((r::hcomplex) * s) pow n = (r pow n) * (s pow n)" |
20727 | 383 |
by transfer (rule power_mult_distrib) |
14314 | 384 |
|
21848 | 385 |
lemma hcpow_zero2 [simp]: |
386 |
"\<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
|
387 |
by transfer (rule power_0_Suc) |
14314 | 388 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
389 |
lemma hcpow_not_zero [simp,intro]: |
21848 | 390 |
"!!r n. r \<noteq> 0 ==> r pow n \<noteq> (0::hcomplex)" |
391 |
by (rule hyperpow_not_zero) |
|
14314 | 392 |
|
21848 | 393 |
lemma hcpow_zero_zero: "r pow n = (0::hcomplex) ==> r = 0" |
14374 | 394 |
by (blast intro: ccontr dest: hcpow_not_zero) |
14314 | 395 |
|
396 |
subsection{*The Function @{term hsgn}*} |
|
397 |
||
14374 | 398 |
lemma hsgn_zero [simp]: "hsgn 0 = 0" |
20727 | 399 |
by transfer (rule sgn_zero) |
14314 | 400 |
|
14374 | 401 |
lemma hsgn_one [simp]: "hsgn 1 = 1" |
20727 | 402 |
by transfer (rule sgn_one) |
14314 | 403 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
404 |
lemma hsgn_minus: "!!z. hsgn (-z) = - hsgn(z)" |
20727 | 405 |
by transfer (rule sgn_minus) |
14314 | 406 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
407 |
lemma hsgn_eq: "!!z. hsgn z = z / hcomplex_of_hypreal (hcmod z)" |
20727 | 408 |
by transfer (rule sgn_eq) |
14314 | 409 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
410 |
lemma hcmod_i: "!!x y. hcmod (HComplex x y) = ( *f* sqrt) (x ^ 2 + y ^ 2)" |
23126 | 411 |
by transfer (rule complex_norm) |
14314 | 412 |
|
14377 | 413 |
lemma hcomplex_eq_cancel_iff1 [simp]: |
414 |
"(hcomplex_of_hypreal xa = HComplex x y) = (xa = x & y = 0)" |
|
415 |
by (simp add: hcomplex_of_hypreal_eq) |
|
14314 | 416 |
|
14374 | 417 |
lemma hcomplex_eq_cancel_iff2 [simp]: |
14377 | 418 |
"(HComplex x y = hcomplex_of_hypreal xa) = (x = xa & y = 0)" |
419 |
by (simp add: hcomplex_of_hypreal_eq) |
|
14314 | 420 |
|
20727 | 421 |
lemma HComplex_eq_0 [simp]: "!!x y. (HComplex x y = 0) = (x = 0 & y = 0)" |
422 |
by transfer (rule Complex_eq_0) |
|
14314 | 423 |
|
20727 | 424 |
lemma HComplex_eq_1 [simp]: "!!x y. (HComplex x y = 1) = (x = 1 & y = 0)" |
425 |
by transfer (rule Complex_eq_1) |
|
14314 | 426 |
|
14377 | 427 |
lemma i_eq_HComplex_0_1: "iii = HComplex 0 1" |
20727 | 428 |
by transfer (rule i_def [THEN meta_eq_to_obj_eq]) |
14314 | 429 |
|
20727 | 430 |
lemma HComplex_eq_i [simp]: "!!x y. (HComplex x y = iii) = (x = 0 & y = 1)" |
431 |
by transfer (rule Complex_eq_i) |
|
14314 | 432 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
433 |
lemma hRe_hsgn [simp]: "!!z. hRe(hsgn z) = hRe(z)/hcmod z" |
20727 | 434 |
by transfer (rule Re_sgn) |
14314 | 435 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
436 |
lemma hIm_hsgn [simp]: "!!z. hIm(hsgn z) = hIm(z)/hcmod z" |
20727 | 437 |
by transfer (rule Im_sgn) |
14314 | 438 |
|
14335 | 439 |
lemma hcomplex_inverse_complex_split: |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
440 |
"!!x y. inverse(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y) = |
14314 | 441 |
hcomplex_of_hypreal(x/(x ^ 2 + y ^ 2)) - |
442 |
iii * hcomplex_of_hypreal(y/(x ^ 2 + y ^ 2))" |
|
20727 | 443 |
by transfer (rule complex_inverse_complex_split) |
14374 | 444 |
|
14377 | 445 |
lemma HComplex_inverse: |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
446 |
"!!x y. inverse (HComplex x y) = |
14377 | 447 |
HComplex (x/(x ^ 2 + y ^ 2)) (-y/(x ^ 2 + y ^ 2))" |
20727 | 448 |
by transfer (rule complex_inverse) |
14377 | 449 |
|
14374 | 450 |
lemma hRe_mult_i_eq[simp]: |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
451 |
"!!y. hRe (iii * hcomplex_of_hypreal y) = 0" |
20727 | 452 |
by transfer simp |
14314 | 453 |
|
14374 | 454 |
lemma hIm_mult_i_eq [simp]: |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
455 |
"!!y. hIm (iii * hcomplex_of_hypreal y) = y" |
20727 | 456 |
by transfer simp |
14314 | 457 |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
458 |
lemma hcmod_mult_i [simp]: "!!y. hcmod (iii * hcomplex_of_hypreal y) = abs y" |
20727 | 459 |
by transfer simp |
14314 | 460 |
|
20727 | 461 |
lemma hcmod_mult_i2 [simp]: "!!y. hcmod (hcomplex_of_hypreal y * iii) = abs y" |
462 |
by transfer simp |
|
14314 | 463 |
|
464 |
(*---------------------------------------------------------------------------*) |
|
465 |
(* harg *) |
|
466 |
(*---------------------------------------------------------------------------*) |
|
467 |
||
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
468 |
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
|
469 |
"!!y. 0 < y ==> ( *f* cos) (harg(HComplex 0 y)) = 0" |
20727 | 470 |
by transfer (rule cos_arg_i_mult_zero_pos) |
14314 | 471 |
|
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
472 |
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
|
473 |
"!!y. y < 0 ==> ( *f* cos) (harg(HComplex 0 y)) = 0" |
20727 | 474 |
by transfer (rule cos_arg_i_mult_zero_neg) |
14314 | 475 |
|
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
476 |
lemma cos_harg_i_mult_zero [simp]: |
20727 | 477 |
"!!y. y \<noteq> 0 ==> ( *f* cos) (harg(HComplex 0 y)) = 0" |
478 |
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
|
479 |
|
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
480 |
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
|
481 |
"!!y. (hcomplex_of_hypreal y = 0) = (y = 0)" |
20727 | 482 |
by transfer (rule of_real_eq_0_iff) |
14314 | 483 |
|
484 |
||
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
485 |
subsection{*Polar Form for Nonstandard Complex Numbers*} |
14314 | 486 |
|
14335 | 487 |
lemma complex_split_polar2: |
14377 | 488 |
"\<forall>n. \<exists>r a. (z n) = complex_of_real r * (Complex (cos a) (sin a))" |
489 |
by (blast intro: complex_split_polar) |
|
490 |
||
14314 | 491 |
lemma hcomplex_split_polar: |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
492 |
"!!z. \<exists>r a. z = hcomplex_of_hypreal r * (HComplex(( *f* cos) a)(( *f* sin) a))" |
20727 | 493 |
by transfer (rule complex_split_polar) |
14314 | 494 |
|
495 |
lemma hcis_eq: |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
496 |
"!!a. hcis a = |
14314 | 497 |
(hcomplex_of_hypreal(( *f* cos) a) + |
498 |
iii * hcomplex_of_hypreal(( *f* sin) a))" |
|
20727 | 499 |
by transfer (simp add: cis_def) |
14314 | 500 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
501 |
lemma hrcis_Ex: "!!z. \<exists>r a. z = hrcis r a" |
20727 | 502 |
by transfer (rule rcis_Ex) |
14314 | 503 |
|
14374 | 504 |
lemma hRe_hcomplex_polar [simp]: |
20727 | 505 |
"!!r a. hRe (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = |
14377 | 506 |
r * ( *f* cos) a" |
20727 | 507 |
by transfer simp |
14314 | 508 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
509 |
lemma hRe_hrcis [simp]: "!!r a. hRe(hrcis r a) = r * ( *f* cos) a" |
20727 | 510 |
by transfer (rule Re_rcis) |
14314 | 511 |
|
14374 | 512 |
lemma hIm_hcomplex_polar [simp]: |
20727 | 513 |
"!!r a. hIm (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = |
14377 | 514 |
r * ( *f* sin) a" |
20727 | 515 |
by transfer simp |
14314 | 516 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
517 |
lemma hIm_hrcis [simp]: "!!r a. hIm(hrcis r a) = r * ( *f* sin) a" |
20727 | 518 |
by transfer (rule Im_rcis) |
14377 | 519 |
|
520 |
lemma hcmod_unit_one [simp]: |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
521 |
"!!a. hcmod (HComplex (( *f* cos) a) (( *f* sin) a)) = 1" |
20727 | 522 |
by transfer (rule cmod_unit_one) |
14377 | 523 |
|
14374 | 524 |
lemma hcmod_complex_polar [simp]: |
20727 | 525 |
"!!r a. hcmod (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = |
14377 | 526 |
abs r" |
20727 | 527 |
by transfer (rule cmod_complex_polar) |
14314 | 528 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
529 |
lemma hcmod_hrcis [simp]: "!!r a. hcmod(hrcis r a) = abs r" |
20727 | 530 |
by transfer (rule complex_mod_rcis) |
14314 | 531 |
|
532 |
(*---------------------------------------------------------------------------*) |
|
533 |
(* (r1 * hrcis a) * (r2 * hrcis b) = r1 * r2 * hrcis (a + b) *) |
|
534 |
(*---------------------------------------------------------------------------*) |
|
535 |
||
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
536 |
lemma hcis_hrcis_eq: "!!a. hcis a = hrcis 1 a" |
20727 | 537 |
by transfer (rule cis_rcis_eq) |
14314 | 538 |
declare hcis_hrcis_eq [symmetric, simp] |
539 |
||
540 |
lemma hrcis_mult: |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
541 |
"!!a b r1 r2. hrcis r1 a * hrcis r2 b = hrcis (r1*r2) (a + b)" |
20727 | 542 |
by transfer (rule rcis_mult) |
14314 | 543 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
544 |
lemma hcis_mult: "!!a b. hcis a * hcis b = hcis (a + b)" |
20727 | 545 |
by transfer (rule cis_mult) |
14314 | 546 |
|
14374 | 547 |
lemma hcis_zero [simp]: "hcis 0 = 1" |
20727 | 548 |
by transfer (rule cis_zero) |
14314 | 549 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
550 |
lemma hrcis_zero_mod [simp]: "!!a. hrcis 0 a = 0" |
20727 | 551 |
by transfer (rule rcis_zero_mod) |
14314 | 552 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
553 |
lemma hrcis_zero_arg [simp]: "!!r. hrcis r 0 = hcomplex_of_hypreal r" |
20727 | 554 |
by transfer (rule rcis_zero_arg) |
14314 | 555 |
|
20727 | 556 |
lemma hcomplex_i_mult_minus [simp]: "!!x. iii * (iii * x) = - x" |
557 |
by transfer (rule complex_i_mult_minus) |
|
14314 | 558 |
|
14374 | 559 |
lemma hcomplex_i_mult_minus2 [simp]: "iii * iii * x = - x" |
560 |
by simp |
|
14314 | 561 |
|
562 |
lemma hcis_hypreal_of_nat_Suc_mult: |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
563 |
"!!a. hcis (hypreal_of_nat (Suc n) * a) = |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
564 |
hcis a * hcis (hypreal_of_nat n * a)" |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
565 |
apply transfer |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
566 |
apply (fold real_of_nat_def) |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
567 |
apply (rule cis_real_of_nat_Suc_mult) |
14314 | 568 |
done |
569 |
||
20727 | 570 |
lemma NSDeMoivre: "!!a. (hcis a) ^ n = hcis (hypreal_of_nat n * a)" |
571 |
apply transfer |
|
572 |
apply (fold real_of_nat_def) |
|
573 |
apply (rule DeMoivre) |
|
14314 | 574 |
done |
575 |
||
14335 | 576 |
lemma hcis_hypreal_of_hypnat_Suc_mult: |
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
577 |
"!! a n. hcis (hypreal_of_hypnat (n + 1) * a) = |
14314 | 578 |
hcis a * hcis (hypreal_of_hypnat n * a)" |
21864
2ecfd8985982
hypreal_of_hypnat abbreviates more general of_hypnat
huffman
parents:
21848
diff
changeset
|
579 |
by transfer (fold real_of_nat_def, simp add: cis_real_of_nat_Suc_mult) |
14314 | 580 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
581 |
lemma NSDeMoivre_ext: |
21848 | 582 |
"!!a n. (hcis a) pow n = hcis (hypreal_of_hypnat n * a)" |
21864
2ecfd8985982
hypreal_of_hypnat abbreviates more general of_hypnat
huffman
parents:
21848
diff
changeset
|
583 |
by transfer (fold real_of_nat_def, rule DeMoivre) |
14314 | 584 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
585 |
lemma NSDeMoivre2: |
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
586 |
"!!a r. (hrcis r a) ^ n = hrcis (r ^ n) (hypreal_of_nat n * a)" |
21864
2ecfd8985982
hypreal_of_hypnat abbreviates more general of_hypnat
huffman
parents:
21848
diff
changeset
|
587 |
by transfer (fold real_of_nat_def, rule DeMoivre2) |
14314 | 588 |
|
589 |
lemma DeMoivre2_ext: |
|
21848 | 590 |
"!! a r n. (hrcis r a) pow n = hrcis (r pow n) (hypreal_of_hypnat n * a)" |
21864
2ecfd8985982
hypreal_of_hypnat abbreviates more general of_hypnat
huffman
parents:
21848
diff
changeset
|
591 |
by transfer (fold real_of_nat_def, rule DeMoivre2) |
14374 | 592 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
593 |
lemma hcis_inverse [simp]: "!!a. inverse(hcis a) = hcis (-a)" |
20727 | 594 |
by transfer (rule cis_inverse) |
14314 | 595 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
596 |
lemma hrcis_inverse: "!!a r. inverse(hrcis r a) = hrcis (inverse r) (-a)" |
20727 | 597 |
by transfer (simp add: rcis_inverse inverse_eq_divide [symmetric]) |
14314 | 598 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
599 |
lemma hRe_hcis [simp]: "!!a. hRe(hcis a) = ( *f* cos) a" |
20727 | 600 |
by transfer (rule Re_cis) |
14314 | 601 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
602 |
lemma hIm_hcis [simp]: "!!a. hIm(hcis a) = ( *f* sin) a" |
20727 | 603 |
by transfer (rule Im_cis) |
14314 | 604 |
|
14374 | 605 |
lemma cos_n_hRe_hcis_pow_n: "( *f* cos) (hypreal_of_nat n * a) = hRe(hcis a ^ n)" |
14377 | 606 |
by (simp add: NSDeMoivre) |
14314 | 607 |
|
14374 | 608 |
lemma sin_n_hIm_hcis_pow_n: "( *f* sin) (hypreal_of_nat n * a) = hIm(hcis a ^ n)" |
14377 | 609 |
by (simp add: NSDeMoivre) |
14314 | 610 |
|
21848 | 611 |
lemma cos_n_hRe_hcis_hcpow_n: "( *f* cos) (hypreal_of_hypnat n * a) = hRe(hcis a pow n)" |
14377 | 612 |
by (simp add: NSDeMoivre_ext) |
14314 | 613 |
|
21848 | 614 |
lemma sin_n_hIm_hcis_hcpow_n: "( *f* sin) (hypreal_of_hypnat n * a) = hIm(hcis a pow n)" |
14377 | 615 |
by (simp add: NSDeMoivre_ext) |
14314 | 616 |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17332
diff
changeset
|
617 |
lemma hexpi_add: "!!a b. hexpi(a + b) = hexpi(a) * hexpi(b)" |
20727 | 618 |
by transfer (rule expi_add) |
14314 | 619 |
|
620 |
||
14374 | 621 |
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
|
622 |
type @{typ complex} to to @{typ hcomplex}*} |
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
623 |
|
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
624 |
lemma inj_hcomplex_of_complex: "inj(hcomplex_of_complex)" |
22883
005be8dafce0
hcomplex_of_hypreal abbreviates of_hypreal; removed redundant lemmas
huffman
parents:
22860
diff
changeset
|
625 |
(* TODO: delete *) |
005be8dafce0
hcomplex_of_hypreal abbreviates of_hypreal; removed redundant lemmas
huffman
parents:
22860
diff
changeset
|
626 |
by (rule inj_star_of) |
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
627 |
|
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14341
diff
changeset
|
628 |
lemma hcomplex_of_complex_i: "iii = hcomplex_of_complex ii" |
20727 | 629 |
by (rule iii_def) |
14314 | 630 |
|
631 |
lemma hRe_hcomplex_of_complex: |
|
632 |
"hRe (hcomplex_of_complex z) = hypreal_of_real (Re z)" |
|
20727 | 633 |
by transfer (rule refl) |
14314 | 634 |
|
635 |
lemma hIm_hcomplex_of_complex: |
|
636 |
"hIm (hcomplex_of_complex z) = hypreal_of_real (Im z)" |
|
20727 | 637 |
by transfer (rule refl) |
14314 | 638 |
|
639 |
lemma hcmod_hcomplex_of_complex: |
|
640 |
"hcmod (hcomplex_of_complex x) = hypreal_of_real (cmod x)" |
|
20727 | 641 |
by transfer (rule refl) |
14314 | 642 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
643 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
644 |
subsection{*Numerals and Arithmetic*} |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
645 |
|
20485 | 646 |
lemma hcomplex_number_of_def: "(number_of w :: hcomplex) == of_int w" |
20727 | 647 |
by transfer (rule number_of_eq [THEN eq_reflection]) |
15013 | 648 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
649 |
lemma hcomplex_of_hypreal_eq_hcomplex_of_complex: |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
650 |
"hcomplex_of_hypreal (hypreal_of_real x) = |
15013 | 651 |
hcomplex_of_complex (complex_of_real x)" |
20727 | 652 |
by transfer (rule refl) |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
653 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
654 |
lemma hcomplex_hypreal_number_of: |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
655 |
"hcomplex_of_complex (number_of w) = hcomplex_of_hypreal(number_of w)" |
23126 | 656 |
by transfer (rule of_real_number_of_eq [symmetric]) |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
657 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
658 |
(* |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
659 |
Goal "z + hcnj z = |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
660 |
hcomplex_of_hypreal (2 * hRe(z))" |
17300 | 661 |
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
|
662 |
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
|
663 |
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
|
664 |
qed "star_n_add_hcnj"; |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
665 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
666 |
Goal "z - hcnj z = \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
667 |
\ hcomplex_of_hypreal (hypreal_of_real #2 * hIm(z)) * iii"; |
17300 | 668 |
by (res_inst_tac [("z","z")] eq_Abs_star 1); |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
669 |
by (auto_tac (claset(),simpset() addsimps [hIm,hcnj,hcomplex_diff, |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
670 |
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
|
671 |
complex_diff_cnj,iii_def,star_n_mult])); |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
672 |
qed "hcomplex_diff_hcnj"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
673 |
*) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
674 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
675 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
676 |
(*** Real and imaginary stuff ***) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
677 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
678 |
(*Convert??? |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
679 |
Goalw [hcomplex_number_of_def] |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
680 |
"((number_of xa :: hcomplex) + iii * number_of ya = |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
681 |
number_of xb + iii * number_of yb) = |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
682 |
(((number_of xa :: hcomplex) = number_of xb) & |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
683 |
((number_of ya :: hcomplex) = number_of yb))" |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
684 |
by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff, |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
685 |
hcomplex_hypreal_number_of])); |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
686 |
qed "hcomplex_number_of_eq_cancel_iff"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
687 |
Addsimps [hcomplex_number_of_eq_cancel_iff]; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
688 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
689 |
Goalw [hcomplex_number_of_def] |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
690 |
"((number_of xa :: hcomplex) + number_of ya * iii = \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
691 |
\ number_of xb + number_of yb * iii) = \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
692 |
\ (((number_of xa :: hcomplex) = number_of xb) & \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
693 |
\ ((number_of ya :: hcomplex) = number_of yb))"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
694 |
by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iffA, |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
695 |
hcomplex_hypreal_number_of])); |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
696 |
qed "hcomplex_number_of_eq_cancel_iffA"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
697 |
Addsimps [hcomplex_number_of_eq_cancel_iffA]; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
698 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
699 |
Goalw [hcomplex_number_of_def] |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
700 |
"((number_of xa :: hcomplex) + number_of ya * iii = \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
701 |
\ number_of xb + iii * number_of yb) = \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
702 |
\ (((number_of xa :: hcomplex) = number_of xb) & \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
703 |
\ ((number_of ya :: hcomplex) = number_of yb))"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
704 |
by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iffB, |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
705 |
hcomplex_hypreal_number_of])); |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
706 |
qed "hcomplex_number_of_eq_cancel_iffB"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
707 |
Addsimps [hcomplex_number_of_eq_cancel_iffB]; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
708 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
709 |
Goalw [hcomplex_number_of_def] |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
710 |
"((number_of xa :: hcomplex) + iii * number_of ya = \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
711 |
\ number_of xb + number_of yb * iii) = \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
712 |
\ (((number_of xa :: hcomplex) = number_of xb) & \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
713 |
\ ((number_of ya :: hcomplex) = number_of yb))"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
714 |
by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iffC, |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
715 |
hcomplex_hypreal_number_of])); |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
716 |
qed "hcomplex_number_of_eq_cancel_iffC"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
717 |
Addsimps [hcomplex_number_of_eq_cancel_iffC]; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
718 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
719 |
Goalw [hcomplex_number_of_def] |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
720 |
"((number_of xa :: hcomplex) + iii * number_of ya = \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
721 |
\ number_of xb) = \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
722 |
\ (((number_of xa :: hcomplex) = number_of xb) & \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
723 |
\ ((number_of ya :: hcomplex) = 0))"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
724 |
by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff2, |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
725 |
hcomplex_hypreal_number_of,hcomplex_of_hypreal_zero_iff])); |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
726 |
qed "hcomplex_number_of_eq_cancel_iff2"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
727 |
Addsimps [hcomplex_number_of_eq_cancel_iff2]; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
728 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
729 |
Goalw [hcomplex_number_of_def] |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
730 |
"((number_of xa :: hcomplex) + number_of ya * iii = \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
731 |
\ number_of xb) = \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
732 |
\ (((number_of xa :: hcomplex) = number_of xb) & \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
733 |
\ ((number_of ya :: hcomplex) = 0))"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
734 |
by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff2a, |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
735 |
hcomplex_hypreal_number_of,hcomplex_of_hypreal_zero_iff])); |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
736 |
qed "hcomplex_number_of_eq_cancel_iff2a"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
737 |
Addsimps [hcomplex_number_of_eq_cancel_iff2a]; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
738 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
739 |
Goalw [hcomplex_number_of_def] |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
740 |
"((number_of xa :: hcomplex) + iii * number_of ya = \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
741 |
\ iii * number_of yb) = \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
742 |
\ (((number_of xa :: hcomplex) = 0) & \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
743 |
\ ((number_of ya :: hcomplex) = number_of yb))"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
744 |
by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff3, |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
745 |
hcomplex_hypreal_number_of,hcomplex_of_hypreal_zero_iff])); |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
746 |
qed "hcomplex_number_of_eq_cancel_iff3"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
747 |
Addsimps [hcomplex_number_of_eq_cancel_iff3]; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
748 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
749 |
Goalw [hcomplex_number_of_def] |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
750 |
"((number_of xa :: hcomplex) + number_of ya * iii= \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
751 |
\ iii * number_of yb) = \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
752 |
\ (((number_of xa :: hcomplex) = 0) & \ |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
753 |
\ ((number_of ya :: hcomplex) = number_of yb))"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
754 |
by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff3a, |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
755 |
hcomplex_hypreal_number_of,hcomplex_of_hypreal_zero_iff])); |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
756 |
qed "hcomplex_number_of_eq_cancel_iff3a"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
757 |
Addsimps [hcomplex_number_of_eq_cancel_iff3a]; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
758 |
*) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
759 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
760 |
lemma hcomplex_number_of_hcnj [simp]: |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
761 |
"hcnj (number_of v :: hcomplex) = number_of v" |
23126 | 762 |
by transfer (rule complex_cnj_number_of) |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
763 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
764 |
lemma hcomplex_number_of_hcmod [simp]: |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
765 |
"hcmod(number_of v :: hcomplex) = abs (number_of v :: hypreal)" |
23126 | 766 |
by transfer (rule norm_number_of) |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
767 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
768 |
lemma hcomplex_number_of_hRe [simp]: |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
769 |
"hRe(number_of v :: hcomplex) = number_of v" |
23126 | 770 |
by transfer (rule complex_Re_number_of) |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
771 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
772 |
lemma hcomplex_number_of_hIm [simp]: |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
773 |
"hIm(number_of v :: hcomplex) = 0" |
23126 | 774 |
by transfer (rule complex_Im_number_of) |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset
|
775 |
|
13957 | 776 |
end |