1(* ================================================================== 2 TITLE: Developing the theory of complex number 3 4 DESCRIPTION : Definitions and properties of the complex data type 5 and arithmetic operations of complex numbers, and many 6 properties organized in terms of group, field and R-module. 7 Moreover, definitions and properties of complex conjugate, 8 modulus and argument principal value of complex, the operation 9 of nature numbers power of complex numbers, the polar form and 10 exponential form of complex numbers. 11 12 AUTHORS : (Copyright) Yong Guan, Liming Li, Minhua Wu and 13 Zhiping Shi 14 Beijing Engineering Research Center of High Reliable 15 Emmbedded System, Capital Normal University, China 16 DATE : 2011.04.23 17 REFERENCES : John Harrison, realScript.sml and complex.ml 18 ================================================================== *) 19 20open HolKernel boolLib Parse bossLib 21open arithmeticTheory numLib pairTheory realTheory realLib transcTheory 22open tautLib AC 23open boolSimps 24 25val _ = new_theory "complex"; 26 27(* ------------------------------------------------------------------ *) 28(* Definition of complex number type. *) 29(* ------------------------------------------------------------------ *) 30 31val _ = type_abbrev ("complex", ``: real # real``); 32 33(*--------------------------------------------------------------------*) 34(* Now prove 2 lemmas. *) 35(*--------------------------------------------------------------------*) 36 37val COMPLEX_LEMMA1= store_thm("COMPLEX_LEMMA1", 38 ``!a:real b:real c:real d:real. 39 (a * c- b * d) pow 2 + (a * d + b * c) pow 2 = 40 (a pow 2 + b pow 2) * (c pow 2 + d pow 2)``, 41 REWRITE_TAC[POW_2] THEN REAL_ARITH_TAC); 42 43val COMPLEX_LEMMA2 = store_thm("COMPLEX_LEMMA2", 44 ``!x y : real. abs x <= sqrt (x pow 2 + y pow 2)``, 45 REPEAT GEN_TAC THEN `0 <= abs x` by PROVE_TAC[ABS_POS] THEN 46 `abs x = sqrt (abs x pow 2)` by PROVE_TAC[POW_2_SQRT] THEN 47 ONCE_ASM_REWRITE_TAC[] THEN REWRITE_TAC[REAL_POW2_ABS] THEN 48 `0 <= x pow 2 /\ 0 <= y pow 2` by PROVE_TAC[REAL_LE_POW2] THEN 49 ` x pow 2 <= x pow 2 + y pow 2` by PROVE_TAC[REAL_LE_ADDR] THEN 50 PROVE_TAC[SQRT_MONO_LE]); 51 52(*--------------------------------------------------------------------*) 53(* Now define real part and imaginary part of complex number. *) 54(*--------------------------------------------------------------------*) 55 56val RE = new_definition("RE",``RE (z:complex) = FST z``); 57 58val IM = new_definition("IM",``IM (z:complex) = SND z``); 59 60val COMPLEX = store_thm("COMPLEX", 61 ``!z:complex. (RE z,IM z) = z``, 62 REWRITE_TAC[RE,IM]); 63 64val COMPLEX_RE_IM_EQ = store_thm("COMPLEX_RE_IM_EQ", 65 ``!z:complex w:complex. (z = w) = (RE z = RE w) /\ (IM z = IM w)``, 66 REWRITE_TAC[RE,IM, PAIR_FST_SND_EQ]); 67 68 69 70(*--------------------------------------------------------------------*) 71(* Now define the inclusion homomorphism: real->complex *) 72(* : num->complex *) 73(*--------------------------------------------------------------------*) 74 75val complex_of_real = new_definition("complex_of_real", 76 ``complex_of_real (x:real) = (x,&0)``); 77 78val RE_COMPLEX_OF_REAL = store_thm("RE_COMPLEX_OF_REAL", 79 ``!x:real. RE (complex_of_real x) = x``, 80 REWRITE_TAC [complex_of_real,RE]); 81 82val IM_COMPLEX_OF_REAL = store_thm("IM_COMPLEX_OF_REAL", 83 ``!x:real. IM (complex_of_real x) = &0``, 84 REWRITE_TAC [complex_of_real, IM]); 85 86val complex_of_num = new_definition 87 ( "complex_of_num", 88 ``complex_of_num (n:num) = complex_of_real (real_of_num n)``); 89 90val _ = add_numeral_form(#"c", SOME "complex_of_num"); 91 92val COMPLEX_0 = store_thm("COMPLEX_0", 93 ``0 = complex_of_real &0``, 94 REWRITE_TAC[complex_of_num]); 95 96val COMPLEX_1 = store_thm("COMPLEX_1", 97 ``1 = complex_of_real 1``, 98 REWRITE_TAC[complex_of_num]); 99 100val COMPLEX_10 = store_thm("COMPLEX_10", 101 ``~(1 = 0)``, 102 REWRITE_TAC[complex_of_num, complex_of_real, COMPLEX_RE_IM_EQ, RE, IM, 103 REAL_10]); 104 105val COMPLEX_0_THM = store_thm("COMPLEX_0_THM", 106 ``!z:complex. (z = 0) = (RE z pow 2 + IM z pow 2 = &0)``, 107 REWRITE_TAC [complex_of_num, complex_of_real,RE, IM, PAIR_FST_SND_EQ, POW_2, 108 REAL_SUMSQ]); 109 110(* ------------------------------------------------------------------ *) 111(* Imaginary unit *) 112(* ------------------------------------------------------------------ *) 113 114val i = new_definition ("i", ``i = (0r,1r)``); 115 116(* ------------------------------------------------------------------ *) 117(* Arithmetic operations. *) 118(* ------------------------------------------------------------------ *) 119 120val complex_add = new_definition 121("complex_add", 122``complex_add (z:complex) (w:complex) = (RE z + RE w,IM z + IM w)``); 123 124val complex_neg = new_definition 125("complex_neg", 126 ``complex_neg (z:complex) = (-RE z, -IM z)``); 127 128val complex_mul = new_definition 129("complex_mul", 130 ``complex_mul (z:complex) (w:complex) = 131 (RE z * RE w - IM z * IM w, RE z * IM w + IM z * RE w)``); 132 133val complex_inv = new_definition 134 ("complex_inv", 135 ``complex_inv (z:complex) = 136 (RE z / ((RE z) pow 2 + (IM z) pow 2), 137 -IM z / ((RE z) pow 2 + (IM z) pow 2))``); 138 139val _ = overload_on ("+", Term`$complex_add`); 140val _ = overload_on ("~", Term`$complex_neg`); 141val _ = overload_on ("*", Term`$complex_mul`); 142val _ = overload_on ("inv", Term`$complex_inv`); 143val _ = overload_on ("numeric_negate", ``$~ : complex->complex``); 144 145val complex_sub = new_definition 146("complex_sub", 147 ``complex_sub (z:complex) (w:complex) = z + ~w``); 148 149val complex_div = new_definition 150("complex_div", 151 ``complex_div (z:complex) (w:complex) = z * inv w``); 152 153val _ = overload_on ("-", Term`$complex_sub`); 154val _ = overload_on (GrammarSpecials.decimal_fraction_special, ``complex_div``) 155val _ = overload_on ("/", Term`complex_div`); 156 157local open complexPP in end 158val _ = add_ML_dependency "complexPP" 159val _ = 160 add_user_printer ("complex.decimalfractions", 161 ``&(NUMERAL x) : complex / &(NUMERAL y)``) 162 163 164(*--------------------------------------------------------------------*) 165(* Prove lots of field theorems *) 166(*--------------------------------------------------------------------*) 167 168val COMPLEX_ADD_COMM = store_thm("COMPLEX_ADD_COMM", 169 ``!z:complex w:complex. z + w = w + z``, 170 REWRITE_TAC [complex_add, RE, IM] THEN PROVE_TAC [REAL_ADD_COMM]); 171 172val COMPLEX_ADD_ASSOC = store_thm("COMPLEX_ADD_ASSOC", 173 ``!z:complex w:complex v:complex. z + (w + v) = z + w + v``, 174 REWRITE_TAC [complex_add, RE, IM] THEN PROVE_TAC [REAL_ADD_ASSOC]); 175 176val COMPLEX_ADD_RID = store_thm("COMPLEX_ADD_RID", 177 ``!z:complex. z + 0 = z``, 178 REWRITE_TAC [complex_of_num,complex_of_real, complex_add, REAL_ADD_RID, 179 RE, IM]); 180 181val COMPLEX_ADD_LID = store_thm("COMPLEX_ADD_LID", 182 ``!z:complex. 0 + z = z``, 183 PROVE_TAC [COMPLEX_ADD_COMM, COMPLEX_ADD_RID]); 184 185val COMPLEX_ADD_RINV = store_thm("COMPLEX_ADD_RINV", 186 ``!z:complex. z + -z = 0``, 187 REWRITE_TAC [complex_of_num, complex_of_real, complex_add, complex_neg, 188 REAL_ADD_RINV, RE, IM]); 189 190val COMPLEX_ADD_LINV = store_thm("COMPLEX_ADD_LINV", 191 ``!z:complex. -z + z = 0``, 192 PROVE_TAC [COMPLEX_ADD_COMM, COMPLEX_ADD_RINV]); 193 194val COMPLEX_MUL_COMM = store_thm("COMPLEX_MUL_COMM", 195 ``!z:complex w:complex. z * w = w * z ``, 196 REPEAT GEN_TAC THEN REWRITE_TAC [complex_mul,RE,IM] THEN 197 PROVE_TAC[REAL_MUL_COMM,REAL_ADD_COMM]); 198 199val COMPLEX_MUL_ASSOC = store_thm("COMPLEX_MUL_ASSOC", 200 ``!z:complex w:complex v:complex. z * (w * v) = z * w * v``, 201 REPEAT GEN_TAC THEN 202 REWRITE_TAC [complex_mul, RE, IM, REAL_SUB_LDISTRIB, REAL_ADD_LDISTRIB, 203 REAL_SUB_RDISTRIB, REAL_ADD_RDISTRIB, REAL_MUL_ASSOC] THEN 204 REWRITE_TAC [real_sub, REAL_NEG_ADD] THEN RW_TAC std_ss[] THEN 205 CONV_TAC(AC_CONV(REAL_ADD_ASSOC,REAL_ADD_SYM))); 206 207val COMPLEX_MUL_RID = store_thm("COMPLEX_MUL_RID", 208 ``!z:complex. z * 1 = z``, 209 REPEAT GEN_TAC THEN 210 REWRITE_TAC [complex_of_num, complex_of_real, complex_mul, REAL_MUL_RZERO, 211 REAL_MUL_RID, REAL_SUB_RZERO, REAL_ADD_LID,RE,IM]); 212 213val COMPLEX_MUL_LID = store_thm("COMPLEX_MUL_LID", 214 ``!z:complex. 1 * z = z``, 215 PROVE_TAC[COMPLEX_MUL_COMM, COMPLEX_MUL_RID]); 216 217val COMPLEX_MUL_RINV = store_thm("COMPLEX_MUL_RINV", 218 ``!z:complex. ~(z = 0) ==> (z * inv z = 1)``, 219 REWRITE_TAC [complex_of_num, complex_of_real, COMPLEX_0_THM, complex_inv, 220 complex_mul, RE, IM, POW_2] THEN 221 RW_TAC std_ss[] THEN 222 `1 = (FST z * FST z + SND z * SND z) / (FST z * FST z + SND z * SND z)` 223 by RW_TAC real_ss[REAL_DIV_REFL] THEN 224 ASM_REWRITE_TAC[] THEN REWRITE_TAC [real_div] THEN REAL_ARITH_TAC); 225 226val COMPLEX_MUL_LINV = store_thm("COMPLEX_MUL_LINV", 227 ``!z:complex. ~(z = 0) ==> (inv z * z = 1)``, 228 PROVE_TAC[COMPLEX_MUL_COMM,COMPLEX_MUL_RINV]); 229 230val COMPLEX_ADD_LDISTRIB = store_thm("COMPLEX_ADD_LDISTRIB", 231 ``!z:complex w:complex v:complex. z * (w + v) = z * w + z * v``, 232 REWRITE_TAC [complex_mul,complex_add,RE,IM,REAL_ADD_LDISTRIB] THEN 233 REWRITE_TAC [real_sub, REAL_NEG_ADD] THEN RW_TAC std_ss[] THEN 234 CONV_TAC(AC_CONV(REAL_ADD_ASSOC,REAL_ADD_SYM))); 235 236val COMPLEX_ADD_RDISTRIB = store_thm("COMPLEX_ADD_RDISTRIB", 237 ``!z:complex w:complex v:complex. (z + w) * v = z * v + w * v``, 238 PROVE_TAC [COMPLEX_MUL_COMM,COMPLEX_ADD_LDISTRIB]); 239 240val COMPLEX_EQ_LADD = store_thm("COMPLEX_EQ_LADD", 241 ``!z:complex w:complex v:complex. (z + w = z + v) = (w = v)``, 242 REWRITE_TAC[complex_add, PAIR_EQ, REAL_EQ_LADD, GSYM COMPLEX_RE_IM_EQ]); 243 244val COMPLEX_EQ_RADD = store_thm("COMPLEX_EQ_RADD", 245 ``!z:complex w:complex v:complex. (z + v = w + v) = (z = w)``, 246 ONCE_REWRITE_TAC [COMPLEX_ADD_COMM] THEN REWRITE_TAC [COMPLEX_EQ_LADD]); 247 248val COMPLEX_ADD_RID_UNIQ = store_thm("COMPLEX_ADD_RID_UNIQ", 249 ``!z:complex w:complex. (z + w = z) = (w = 0)``, 250 REWRITE_TAC [complex_of_num, complex_of_real, complex_add, COMPLEX_RE_IM_EQ, 251 RE, IM, REAL_ADD_RID_UNIQ]); 252 253val COMPLEX_ADD_LID_UNIQ = store_thm("COMPLEX_ADD_LID_UNIQ", 254 ``!z:complex w:complex. (z + w = w) = (z = 0)``, 255 ONCE_REWRITE_TAC [COMPLEX_ADD_COMM] THEN 256 REWRITE_TAC [COMPLEX_ADD_RID_UNIQ]); 257 258val COMPLEX_NEGNEG = store_thm("COMPLEX_NEGNEG", 259 ``!z:complex. --z = z``, 260 REWRITE_TAC [complex_neg, RE, IM, REAL_NEGNEG]); 261 262val COMPLEX_NEG_EQ = store_thm("COMPLEX_NEG_EQ", 263 ``!z:complex w:complex. (-z = w) = (z = -w)``, 264 REWRITE_TAC [complex_neg, COMPLEX_RE_IM_EQ, RE, IM, REAL_NEG_EQ]); 265 266val COMPLEX_EQ_NEG = store_thm("COMPLEX_EQ_NEG", 267 ``!z:complex w:complex. (-z = -w) = (z = w)``, 268 REWRITE_TAC [COMPLEX_NEG_EQ, COMPLEX_NEGNEG]); 269 270val COMPLEX_RNEG_UNIQ = store_thm("COMPLEX_RNEG_UNIQ", 271 ``!z:complex w:complex. (z + w = 0) = (w = -z) ``, 272 REWRITE_TAC [complex_of_num, complex_of_real, GSYM COMPLEX_ADD_RINV] THEN 273 PROVE_TAC [COMPLEX_ADD_COMM, COMPLEX_EQ_LADD]); 274 275val COMPLEX_LNEG_UNIQ = store_thm("COMPLEX_LNEG_UNIQ", 276 ``!z:complex w:complex. (z + w = 0) = (z = -w) ``, 277 PROVE_TAC[COMPLEX_RNEG_UNIQ,COMPLEX_NEG_EQ]); 278 279val COMPLEX_NEG_ADD = store_thm("COMPLEX_NEG_ADD", 280 ``!z:complex w:complex. -(z + w) = -z + -w ``, 281 REWRITE_TAC[complex_neg,complex_add ,RE,IM, REAL_NEG_ADD]); 282 283val COMPLEX_MUL_RZERO = store_thm("COMPLEX_MUL_RZERO", 284 ``!z:complex. z * 0 = 0``, 285 REWRITE_TAC [complex_of_num, complex_of_real, complex_mul, REAL_MUL_RZERO, 286 REAL_ADD_RID, REAL_SUB_RZERO, RE,IM]); 287 288val COMPLEX_MUL_LZERO = store_thm("COMPLEX_MUL_LZERO", 289 ``!z:complex. 0 * z = 0``, 290 PROVE_TAC[COMPLEX_MUL_COMM, COMPLEX_MUL_RZERO]); 291 292val COMPLEX_NEG_LMUL = store_thm("COMPLEX_NEG_LMUL", 293 ``!z:complex w:complex. -(z * w) = -z * w ``, 294 REWRITE_TAC [complex_neg, complex_mul, RE,IM, real_sub, REAL_NEG_ADD, 295 REAL_NEG_LMUL]); 296 297val COMPLEX_NEG_RMUL = store_thm("COMPLEX_NEG_RMUL", 298 ``!z:complex w:complex. -(z * w) = z * -w ``, 299 PROVE_TAC [COMPLEX_NEG_LMUL, COMPLEX_MUL_COMM]); 300 301val COMPLEX_NEG_MUL2 = store_thm("COMPLEX_NEG_MUL2", 302 ``!z:complex w:complex. -z * -w = z * w ``, 303 REWRITE_TAC [GSYM COMPLEX_NEG_LMUL, GSYM COMPLEX_NEG_RMUL, COMPLEX_NEGNEG]); 304 305val COMPLEX_ENTIRE = store_thm("COMPLEX_ENTIRE", 306 ``!z:complex w:complex. 307 (z * w = 0) = (z = 0) \/ (w = 0)``, 308 REWRITE_TAC[complex_of_num, complex_of_real, COMPLEX_0_THM, complex_mul, 309 RE,IM,COMPLEX_LEMMA1,REAL_ENTIRE]); 310 311val COMPLEX_NEG_0 = store_thm("COMPLEX_NEG_0", 312 ``-0 = 0``, 313 REWRITE_TAC [complex_of_num, complex_of_real, complex_neg, RE, IM, 314 REAL_NEG_0]); 315 316val COMPLEX_NEG_EQ0 = store_thm("COMPLEX_NEG_EQ0", 317 ``!z:complex. (-z = 0) = (z = 0)``, 318 REWRITE_TAC[COMPLEX_NEG_EQ,COMPLEX_NEG_0]); 319 320val COMPLEX_SUB_REFL = store_thm("COMPLEX_SUB_REFL", 321 ``!z:complex. z - z = 0``, 322 REPEAT GEN_TAC THEN REWRITE_TAC [complex_sub, COMPLEX_ADD_RINV]); 323 324val COMPLEX_SUB_RZERO = store_thm("COMPLEX_SUB_RZERO", 325 ``!z:complex. z - 0 = z``, 326 REWRITE_TAC [complex_sub, COMPLEX_NEG_0, COMPLEX_ADD_RID]); 327 328val COMPLEX_SUB_LZERO = store_thm("COMPLEX_SUB_LZERO", 329 ``!z:complex. 0 - z = -z``, 330 REWRITE_TAC [complex_sub, COMPLEX_ADD_LID]); 331 332val COMPLEX_SUB_LNEG = store_thm("COMPLEX_SUB_LNEG", 333 ``!z:complex w:complex. -z - w = -(z + w)``, 334 REPEAT GEN_TAC THEN REWRITE_TAC [complex_sub, COMPLEX_NEG_ADD]); 335 336val COMPLEX_SUB_NEG2 = store_thm("COMPLEX_SUB_NEG2", 337 ``!z:complex w:complex. -z - -w = w - z``, 338 REWRITE_TAC[complex_sub, COMPLEX_NEGNEG] THEN PROVE_TAC [COMPLEX_ADD_COMM]); 339 340val COMPLEX_NEG_SUB = store_thm("COMPLEX_NEG_SUB", 341 ``!z:complex w:complex. -(z - w) = w - z ``, 342 REWRITE_TAC[complex_sub, COMPLEX_NEG_ADD, COMPLEX_NEGNEG] THEN 343 PROVE_TAC [COMPLEX_ADD_COMM]); 344 345val COMPLEX_SUB_RNEG = store_thm("COMPLEX_SUB_RNEG", 346 ``!z:complex w:complex. z - -w = z + w``, 347 REPEAT GEN_TAC THEN REWRITE_TAC [complex_sub, COMPLEX_NEGNEG]); 348 349val COMPLEX_SUB_ADD = store_thm ("COMPLEX_SUB_ADD", 350 (``!z:complex w:complex. (z - w) + w = z``), 351 REWRITE_TAC [complex_sub, GSYM COMPLEX_ADD_ASSOC, COMPLEX_ADD_LINV, 352 COMPLEX_ADD_RID]); 353 354val COMPLEX_SUB_ADD2 = store_thm("COMPLEX_SUB_ADD2", 355 (``!z:complex w:complex. w + (z - w) = z``), 356 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[COMPLEX_ADD_COMM] THEN 357 MATCH_ACCEPT_TAC COMPLEX_SUB_ADD); 358 359val COMPLEX_ADD_SUB = store_thm ("COMPLEX_ADD_SUB", 360 (``!z:complex w:complex. (z + w) - z = w``), 361 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[COMPLEX_ADD_COMM] THEN 362 REWRITE_TAC[complex_sub, GSYM COMPLEX_ADD_ASSOC, COMPLEX_ADD_RINV, 363 COMPLEX_ADD_RID]); 364 365val COMPLEX_SUB_SUB = store_thm ("COMPLEX_SUB_SUB", 366 ``!z:complex w:complex. (z - w) - z = -w ``, 367 REPEAT GEN_TAC THEN REWRITE_TAC[complex_sub] THEN 368 REWRITE_TAC[GSYM COMPLEX_ADD_ASSOC] THEN 369 ONCE_REWRITE_TAC[COMPLEX_ADD_COMM] THEN 370 REWRITE_TAC[GSYM COMPLEX_ADD_ASSOC] THEN 371 REWRITE_TAC[COMPLEX_ADD_LINV, COMPLEX_ADD_RID]); 372 373val COMPLEX_SUB_SUB2 = store_thm("COMPLEX_SUB_SUB2", 374 ``!z:complex w:complex. z - (z - w) = w``, 375 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[GSYM COMPLEX_NEGNEG] THEN 376 AP_TERM_TAC THEN REWRITE_TAC[COMPLEX_NEG_SUB, COMPLEX_SUB_SUB]); 377 378val COMPLEX_ADD_SUB2 = store_thm("COMPLEX_ADD_SUB2", 379 ``!z:complex w:complex. z - (z + w) = -w``, 380 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[GSYM COMPLEX_NEG_SUB] THEN 381 AP_TERM_TAC THEN REWRITE_TAC[COMPLEX_ADD_SUB]); 382 383val COMPLEX_ADD2_SUB2 = store_thm("COMPLEX_ADD2_SUB2", 384 ``!z:complex w:complex u:complex v:complex. 385(z + w) - (u + v) = (z - u) + (w - v)``, 386 REPEAT GEN_TAC THEN REWRITE_TAC[complex_sub, COMPLEX_NEG_ADD] THEN 387 CONV_TAC(AC_CONV(COMPLEX_ADD_ASSOC,COMPLEX_ADD_COMM))); 388 389val COMPLEX_SUB_TRIANGLE = store_thm("COMPLEX_SUB_TRIANGLE", 390 ``!z:complex w:complex v:complex. (z - w) + (w - v) = z - v``, 391 REPEAT GEN_TAC THEN REWRITE_TAC[complex_sub] THEN 392 ONCE_REWRITE_TAC[AC(COMPLEX_ADD_ASSOC,COMPLEX_ADD_COMM) 393 ``(a + b) + (c + d) = (b + c) + (a + d)``] THEN 394 REWRITE_TAC[COMPLEX_ADD_LINV, COMPLEX_ADD_LID]); 395 396val COMPLEX_SUB_0 = store_thm("COMPLEX_SUB_0", 397 ``!z:complex w:complex. (z - w = 0) = (z = w)``, 398 REWRITE_TAC [complex_sub, COMPLEX_LNEG_UNIQ , COMPLEX_NEGNEG]); 399 400val COMPLEX_EQ_SUB_LADD = store_thm("COMPLEX_EQ_SUB_LADD", 401 ``!z:complex w:complex v:complex. (z = w - v) = (z + v = w)``, 402 REPEAT GEN_TAC THEN 403 Q.SPECL_THEN [`z`, `w-v`, `v`] (SUBST1_TAC o SYM) COMPLEX_EQ_RADD THEN 404 REWRITE_TAC[COMPLEX_SUB_ADD]); 405 406val COMPLEX_EQ_SUB_RADD = store_thm("COMPLEX_EQ_SUB_RADD", 407 ``!z:complex w:complex v:complex. (z - w = v) = (z = v + w)``, 408 REPEAT GEN_TAC THEN 409 CONV_TAC(SUB_CONV(ONCE_DEPTH_CONV SYM_CONV)) THEN 410 MATCH_ACCEPT_TAC COMPLEX_EQ_SUB_LADD); 411 412val COMPLEX_MUL_RNEG = store_thm("COMPLEX_MUL_RNEG", 413 ``! z:complex w:complex. z * -w = -(z * w)``, 414 REWRITE_TAC[COMPLEX_NEG_RMUL]); 415 416val COMPLEX_MUL_LNEG = store_thm("COMPLEX_MUL_LNEG", 417 ``! z:complex w:complex. -z * w = -(z * w)``, 418 REWRITE_TAC[COMPLEX_NEG_LMUL]); 419 420val COMPLEX_SUB_LDISTRIB = store_thm("COMPLEX_SUB_LDISTRIB", 421 ``!z:complex w:complex v:complex. z * (w - v) = z * w - z * v``, 422 REWRITE_TAC [complex_sub, COMPLEX_ADD_LDISTRIB, GSYM COMPLEX_NEG_RMUL]); 423 424val COMPLEX_SUB_RDISTRIB = store_thm("COMPLEX_SUB_RDISTRIB", 425 ``!z:complex w:complex v:complex. (z - w) * v = z * v - w * v``, 426 PROVE_TAC [COMPLEX_MUL_COMM,COMPLEX_SUB_LDISTRIB]); 427 428val COMPLEX_DIFFSQ = store_thm("COMPLEX_DIFFSQ", 429 ``!z:complex w:complex. (z + w) * (z - w) = z * z - w * w ``, 430 REWRITE_TAC[COMPLEX_ADD_RDISTRIB, COMPLEX_SUB_LDISTRIB, complex_sub, 431 GSYM COMPLEX_ADD_ASSOC, COMPLEX_EQ_LADD] THEN 432 REWRITE_TAC [COMPLEX_ADD_ASSOC, COMPLEX_ADD_LID_UNIQ] THEN 433 PROVE_TAC [COMPLEX_ADD_COMM, COMPLEX_MUL_COMM, COMPLEX_ADD_RINV]); 434 435val COMPLEX_EQ_LMUL = store_thm("COMPLEX_EQ_LMUL", 436 ``!z:complex w:complex v:complex. 437 (z * w = z * v) = (z = 0) \/ (w = v)``, 438 ONCE_REWRITE_TAC [GSYM COMPLEX_SUB_0] THEN 439 REWRITE_TAC [GSYM COMPLEX_SUB_LDISTRIB, COMPLEX_ENTIRE, COMPLEX_SUB_RZERO]); 440 441val COMPLEX_EQ_RMUL = store_thm("COMPLEX_EQ_RMUL", 442 ``!z:complex w:complex v:complex. 443 (z * v = w * v) = (v = 0) \/ (z = w)``, 444 PROVE_TAC[COMPLEX_MUL_COMM, COMPLEX_EQ_LMUL]); 445 446val COMPLEX_EQ_LMUL2 = store_thm("COMPLEX_EQ_LMUL2", 447 ``!z:complex w:complex v:complex. 448 ~(z = 0) ==> ((w = v) = (z * w = z * v))``, 449 REPEAT GEN_TAC THEN DISCH_TAC THEN 450 Q.SPECL_THEN [`z`, `w`, `v`] MP_TAC COMPLEX_EQ_LMUL THEN 451 ASM_REWRITE_TAC[] THEN DISCH_THEN SUBST_ALL_TAC THEN REFL_TAC); 452 453val COMPLEX_EQ_RMUL_IMP = store_thm("COMPLEX_EQ_RMUL_IMP", 454 ``!z:complex w:complex v:complex. 455 ~(z = 0) /\ (w * z = v * z)==> (w = v)``, 456 REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN 457 ASM_REWRITE_TAC[COMPLEX_EQ_RMUL]); 458 459val COMPLEX_EQ_LMUL_IMP = store_thm("COMPLEX_EQ_LMUL_IMP", 460 ``!z:complex w:complex v:complex. 461 ~(z = 0) /\ (z * w = z * v)==> (w = v)``, 462 ONCE_REWRITE_TAC[COMPLEX_MUL_COMM] THEN 463 MATCH_ACCEPT_TAC COMPLEX_EQ_RMUL_IMP); 464 465val COMPLEX_NEG_INV = store_thm("COMPLEX_NEG_INV", 466 ``!z: complex. ~(z = 0) ==> (inv (-z) = -(inv z))``, 467 REWRITE_TAC [COMPLEX_0_THM,complex_inv,complex_neg,RE,IM,POW_2] THEN 468 RW_TAC real_ss[real_div]); 469 470val COMPLEX_INV_MUL = store_thm("COMPLEX_INV_MUL", 471 ``!z:complex w:complex. 472 (z <> 0 /\ w <> 0) ==> (inv (z * w) = inv z * inv w)``, 473 REWRITE_TAC [complex_inv,COMPLEX_0_THM, complex_mul, RE,IM] THEN 474 RW_TAC real_ss[real_div,COMPLEX_LEMMA1,REAL_INV_MUL] THEN REAL_ARITH_TAC); 475 476val COMPLEX_INVINV = store_thm("COMPLEX_INVINV", 477 ``!z: complex. (z <> 0) ==> (inv (inv z) = z)``, 478 REPEAT STRIP_TAC THEN 479 FIRST_ASSUM(MP_TAC o MATCH_MP COMPLEX_MUL_RINV) THEN 480 Q.ASM_CASES_TAC `inv z = 0` THENL[ 481 ASM_REWRITE_TAC[COMPLEX_MUL_RZERO, GSYM COMPLEX_10], 482 Q.SPECL_THEN [`inv(inv z)`, `z`, `inv z`] MP_TAC COMPLEX_EQ_RMUL THEN 483 ASM_REWRITE_TAC[] THEN DISCH_THEN(SUBST1_TAC o SYM) THEN 484 DISCH_THEN SUBST1_TAC THEN MATCH_MP_TAC COMPLEX_MUL_LINV THEN 485 FIRST_ASSUM ACCEPT_TAC 486 ]); 487 488val COMPLEX_LINV_UNIQ = store_thm("COMPLEX_LINV_UNIQ", 489 ``!z:complex w:complex. (z * w = 1) ==> (z = inv w)``, 490 REPEAT GEN_TAC THEN ASM_CASES_TAC (``z = 0``) THENL [ 491 ASM_REWRITE_TAC [COMPLEX_MUL_LZERO, GSYM COMPLEX_10], 492 DISCH_THEN(MP_TAC o AP_TERM (``$* (inv z:complex) ``)) THEN 493 REWRITE_TAC [COMPLEX_MUL_ASSOC] THEN 494 FIRST_ASSUM (fn th=> REWRITE_TAC [MATCH_MP COMPLEX_MUL_LINV th]) THEN 495 REWRITE_TAC [COMPLEX_MUL_LID, COMPLEX_MUL_RID] THEN 496 DISCH_THEN SUBST1_TAC THEN CONV_TAC SYM_CONV THEN 497 POP_ASSUM MP_TAC THEN MATCH_ACCEPT_TAC COMPLEX_INVINV 498 ]); 499 500val COMPLEX_RINV_UNIQ = store_thm("COMPLEX_RINV_UNIQ", 501 ``!z:complex w:complex. (z * w = 1) ==> (w = inv z)``, 502 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[COMPLEX_MUL_COMM] THEN 503 MATCH_ACCEPT_TAC COMPLEX_LINV_UNIQ); 504 505val COMPLEX_INV_0 = store_thm("COMPLEX_INV_0", 506 ``inv 0 = 0c``, 507 RW_TAC real_ss [complex_of_num, complex_of_real, complex_inv, RE, IM, 508 POW_2, real_div, REAL_INV_0]); 509 510val COMPLEX_INV1 = store_thm("COMPLEX_INV1", 511 ``inv 1c = 1``, 512 RW_TAC real_ss [complex_of_num, complex_of_real, complex_inv, RE, IM, 513 POW_2, real_div, REAL_INV1]); 514 515val COMPLEX_INV_INV = store_thm("COMPLEX_INV_INV", 516 ``!z: complex. inv (inv z) = z ``, 517 GEN_TAC THEN Q.ASM_CASES_TAC `z = 0` THENL [ 518 ASM_REWRITE_TAC [COMPLEX_INV_0], 519 MATCH_MP_TAC COMPLEX_INVINV THEN ASM_REWRITE_TAC[] 520 ]); 521 522val COMPLEX_INV_NEG = store_thm("COMPLEX_INV_NEG", 523 ``!z: complex. inv (-z) = -inv z``, 524 GEN_TAC THEN Q.ASM_CASES_TAC `z = 0` THEN 525 ASM_REWRITE_TAC [COMPLEX_INV_0, COMPLEX_NEG_0] THEN 526 MATCH_MP_TAC COMPLEX_NEG_INV THEN ASM_REWRITE_TAC[]); 527 528val COMPLEX_INV_EQ_0 = store_thm ("COMPLEX_INV_EQ_0", 529 ``!z: complex. (inv z = 0) = (z = 0)``, 530 GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN 531 ASM_REWRITE_TAC[COMPLEX_INV_0] THEN 532 ONCE_REWRITE_TAC[GSYM COMPLEX_INV_INV] THEN 533 ASM_REWRITE_TAC[COMPLEX_INV_0]); 534 535val COMPLEX_INV_NZ = store_thm ("COMPLEX_INV_NZ", 536 ``!z:complex. z <> 0 ==> inv z <> 0``, 537 REWRITE_TAC[COMPLEX_INV_EQ_0]); 538 539val COMPLEX_INV_INJ = store_thm("COMPLEX_INV_INJ", 540 ``!z: complex w: complex. (inv z = inv w) = (z = w)``, 541 PROVE_TAC[COMPLEX_INV_INV] ); 542 543val COMPLEX_NEG_LDIV= store_thm("COMPLEX_NEG_LDIV", 544 ``!z w : complex. -(z / w) = -z / w``, 545 REWRITE_TAC[complex_div, COMPLEX_NEG_LMUL]); 546 547val COMPLEX_NEG_RDIV= store_thm("COMPLEX_NEG_RDIV", 548 ``!z w : complex. -(z / w) = z / -w``, 549 REWRITE_TAC[complex_div, COMPLEX_INV_NEG, COMPLEX_NEG_RMUL]); 550 551val COMPLEX_NEG_DIV2= store_thm("COMPLEX_NEG_DIV2", 552 ``!z w : complex. -z / -w = z / w ``, 553 REWRITE_TAC[complex_div, COMPLEX_INV_NEG, COMPLEX_NEG_MUL2]); 554 555val COMPLEX_INV_1OVER= store_thm("COMPLEX_INV_1OVER", 556 ``!z: complex. inv z = 1 / z ``, 557 REWRITE_TAC[complex_div, COMPLEX_MUL_LID]); 558 559val COMPLEX_DIV1= store_thm("COMPLEX_DIV1", 560 ``!z: complex. z / 1 = z ``, 561 REWRITE_TAC[complex_div, COMPLEX_INV1,COMPLEX_MUL_RID]); 562 563val COMPLEX_DIV_ADD = store_thm("COMPLEX_DIV_ADD", 564 ``!z w v :complex. z / v + w / v = (z + w) / v``, 565 REWRITE_TAC[complex_div, GSYM COMPLEX_ADD_RDISTRIB]); 566 567val COMPLEX_DIV_SUB = store_thm("COMPLEX_DIV_SUB", 568 ``!z w v :complex. z / v - w / v = (z - w) / v ``, 569 REWRITE_TAC[complex_div, GSYM COMPLEX_SUB_RDISTRIB]); 570 571val COMPLEX_DIV_RMUL_CANCEL = store_thm ("COMPLEX_DIV_RMUL_CANCEL", 572 ``!v:complex z w. ~(v = 0) ==> ((z * v) / (w * v) = z / w)``, 573 RW_TAC bool_ss [complex_div] THEN 574 Cases_on `w = 0` THEN 575 RW_TAC bool_ss [COMPLEX_MUL_LZERO, COMPLEX_INV_0, COMPLEX_INV_MUL, 576 COMPLEX_MUL_RZERO, COMPLEX_EQ_LMUL, 577 GSYM COMPLEX_MUL_ASSOC] THEN 578 DISJ2_TAC THEN ONCE_REWRITE_TAC [COMPLEX_MUL_COMM] THEN 579 ONCE_REWRITE_TAC [GSYM COMPLEX_MUL_ASSOC] THEN 580 RW_TAC bool_ss [COMPLEX_MUL_LINV, COMPLEX_MUL_RID]); 581 582val COMPLEX_DIV_LMUL_CANCEL = store_thm("COMPLEX_DIV_LMUL_CANCEL", 583 ``!v:complex z w. ~(v = 0) ==> ((v * z) / (v * w) = z / w)``, 584 METIS_TAC [COMPLEX_DIV_RMUL_CANCEL, COMPLEX_MUL_COMM]); 585 586val COMPLEX_DIV_DENOM_CANCEL = store_thm("COMPLEX_DIV_DENOM_CANCEL", 587 ``!z:complex w v. ~(z = 0) ==> ((w / z) / (v / z) = w / v)``, 588 RW_TAC bool_ss [complex_div] THEN 589 Cases_on `w = 0` THEN1 RW_TAC bool_ss [COMPLEX_MUL_LZERO] THEN 590 Cases_on `v = 0` 591 THEN1 RW_TAC bool_ss [COMPLEX_INV_0, COMPLEX_MUL_RZERO, 592 COMPLEX_MUL_LZERO] THEN 593 RW_TAC bool_ss [COMPLEX_INV_MUL, COMPLEX_INV_EQ_0, 594 COMPLEX_INVINV] THEN 595 REWRITE_TAC [GSYM COMPLEX_MUL_ASSOC] THEN 596 RW_TAC bool_ss [COMPLEX_EQ_LMUL] THEN 597 ONCE_REWRITE_TAC [COMPLEX_MUL_COMM] THEN 598 REWRITE_TAC [GSYM COMPLEX_MUL_ASSOC] THEN 599 RW_TAC bool_ss [COMPLEX_MUL_RINV, COMPLEX_MUL_RID]); 600 601val COMPLEX_DIV_INNER_CANCEL = store_thm("COMPLEX_DIV_INNER_CANCEL", 602 ``!z:complex w v. ~(z = 0) ==> ((w / z) * (z / v) = w / v)``, 603 RW_TAC bool_ss [complex_div] THEN 604 Cases_on `w = 0` THEN1 RW_TAC bool_ss [COMPLEX_MUL_LZERO] THEN 605 REWRITE_TAC[GSYM COMPLEX_MUL_ASSOC] THEN 606 RW_TAC bool_ss [COMPLEX_EQ_LMUL] THEN 607 REWRITE_TAC[COMPLEX_MUL_ASSOC] THEN 608 RW_TAC bool_ss [COMPLEX_MUL_LINV, COMPLEX_MUL_LID]); 609 610val COMPLEX_DIV_OUTER_CANCEL = store_thm("COMPLEX_DIV_OUTER_CANCEL", 611 ``!z:complex w v. ~(z = 0) ==> ((z /w) * (v / z) = v / w)``, 612 ONCE_REWRITE_TAC[COMPLEX_MUL_COMM] THEN 613 REWRITE_TAC[COMPLEX_DIV_INNER_CANCEL]); 614 615val COMPLEX_DIV_MUL2 = store_thm("COMPLEX_DIV_MUL2", 616 ``!z:complex w. 617 ~(z = 0) /\ ~(w = 0) ==> !v. v / w = (z * v) / (z * w)``, 618 REPEAT GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN 619 RW_TAC bool_ss [COMPLEX_DIV_LMUL_CANCEL]); 620 621val COMPLEX_ADD_RAT = store_thm ("COMPLEX_ADD_RAT", 622 ``!z:complex w u v. 623 ~(w = 0) /\ ~(v = 0) ==> 624 (z / w + u / v = (z * v + w * u) / (w * v))``, 625 RW_TAC bool_ss [GSYM COMPLEX_DIV_ADD, COMPLEX_DIV_RMUL_CANCEL, 626 COMPLEX_DIV_LMUL_CANCEL]); 627 628val COMPLEX_SUB_RAT = store_thm ("COMPLEX_SUB_RAT", 629 ``!z:complex w u v. 630 ~(w = 0) /\ ~(v = 0) ==> 631 (z / w - u / v = (z * v - w * u) / (w * v))``, 632 RW_TAC bool_ss [complex_sub, COMPLEX_NEG_LDIV] 633 THEN METIS_TAC [COMPLEX_ADD_RAT, COMPLEX_NEG_LMUL, COMPLEX_NEG_RMUL]); 634 635val COMPLEX_DIV_LZERO = store_thm("COMPLEX_DIV_LZERO", 636 ``!z:complex. 0 / z = 0``, 637 REWRITE_TAC[complex_div, COMPLEX_MUL_LZERO]); 638 639val COMPLEX_DIV_REFL = store_thm("COMPLEX_DIV_REFL", 640 ``!z:complex. ~(z = 0) ==> (z / z = 1)``, 641 REWRITE_TAC[complex_div, COMPLEX_MUL_RINV] ); 642 643val COMPLEX_SUB_INV2 = store_thm("COMPLEX_SUB_INV2", 644 ``!z:complex w. 645 (z <> 0 /\ w <> 0) ==> 646 (inv z - inv w = (w - z) / (z * w))``, 647 REWRITE_TAC[complex_div] THEN REPEAT STRIP_TAC THEN 648 IMP_RES_TAC COMPLEX_INV_MUL THEN ASM_REWRITE_TAC[] THEN 649 REWRITE_TAC [COMPLEX_SUB_RDISTRIB, COMPLEX_MUL_ASSOC] THEN 650 IMP_RES_TAC COMPLEX_MUL_RINV THEN ASM_REWRITE_TAC[] THEN 651 REWRITE_TAC [COMPLEX_MUL_LID, GSYM COMPLEX_MUL_ASSOC] THEN 652 ONCE_REWRITE_TAC [COMPLEX_MUL_COMM] THEN 653 REWRITE_TAC [GSYM COMPLEX_MUL_ASSOC] THEN 654 FIRST_ASSUM (fn th=> REWRITE_TAC [MATCH_MP COMPLEX_MUL_LINV th]) THEN 655 REWRITE_TAC[COMPLEX_MUL_RID]); 656 657val COMPLEX_EQ_RDIV_EQ = store_thm("COMPLEX_EQ_RDIV_EQ", 658 ``!z:complex w:complex v:complex. 659 ~(v = 0) ==> ((z = w / v) = (z * v= w))``, 660 REPEAT GEN_TAC THEN REWRITE_TAC[complex_div] THEN 661 DISCH_TAC THEN EQ_TAC THENL [ 662 DISCH_THEN(MP_TAC o AP_TERM ``$* (v:complex)``) THEN 663 ONCE_REWRITE_TAC[COMPLEX_MUL_COMM] THEN 664 RW_TAC bool_ss [COMPLEX_MUL_COMM, GSYM COMPLEX_MUL_ASSOC, 665 COMPLEX_MUL_LINV, COMPLEX_MUL_RID], 666 DISCH_THEN(MP_TAC o AP_TERM ``$* (inv v:complex)``) THEN 667 ONCE_REWRITE_TAC[COMPLEX_MUL_COMM] THEN 668 RW_TAC bool_ss [COMPLEX_MUL_COMM, GSYM COMPLEX_MUL_ASSOC, 669 COMPLEX_MUL_RINV, COMPLEX_MUL_RID] 670 ]); 671 672val COMPLEX_EQ_LDIV_EQ = store_thm("COMPLEX_EQ_LDIV_EQ", 673 ``!z:complex w:complex v:complex. 674 ~(v = 0) ==> ((z / v = w) = (z = w * v))``, 675 REPEAT GEN_TAC THEN REWRITE_TAC[complex_div] THEN 676 DISCH_TAC THEN EQ_TAC THENL [ 677 DISCH_THEN(MP_TAC o AP_TERM (``$* (v:complex)``)) THEN 678 ONCE_REWRITE_TAC[COMPLEX_MUL_COMM] THEN 679 RW_TAC bool_ss [COMPLEX_MUL_COMM, GSYM COMPLEX_MUL_ASSOC, 680 COMPLEX_MUL_LINV, COMPLEX_MUL_RID], 681 DISCH_THEN(MP_TAC o AP_TERM (``$* (inv v:complex)``)) THEN 682 ONCE_REWRITE_TAC[COMPLEX_MUL_COMM] THEN 683 RW_TAC bool_ss [COMPLEX_MUL_COMM, GSYM COMPLEX_MUL_ASSOC, COMPLEX_MUL_RINV, 684 COMPLEX_MUL_RID] 685 ]); 686 687(* ------------------------------------------------------------------ *) 688(* Homomorphic embedding properties for complex_of_real mapping. *) 689(* ------------------------------------------------------------------ *) 690 691val COMPLEX_OF_REAL_EQ = store_thm("COMPLEX_OF_REAL_EQ", 692 ``!x:real y:real. 693 (complex_of_real x = complex_of_real y) = (x = y)``, 694 REWRITE_TAC[complex_of_real, COMPLEX_RE_IM_EQ, RE, IM]); 695 696val COMPLEX_OF_REAL_ADD = store_thm("COMPLEX_OF_REAL_ADD", 697 ``!x:real y:real. 698 complex_of_real x + complex_of_real y = complex_of_real (x + y)``, 699 REWRITE_TAC [complex_of_real,complex_add,RE,IM,REAL_ADD_RID]); 700 701val COMPLEX_OF_REAL_NEG = store_thm("COMPLEX_OF_REAL_NEG", 702 ``!x:real. -complex_of_real x = complex_of_real (-x)``, 703 REWRITE_TAC [complex_of_real,complex_neg,RE,IM,REAL_NEG_0]); 704 705val COMPLEX_OF_REAL_MUL = store_thm("COMPLEX_OF_REAL_MUL", 706 ``!x:real y:real. 707 complex_of_real x * complex_of_real y = complex_of_real (x * y)``, 708 REWRITE_TAC [complex_of_real, complex_mul, RE, IM, REAL_MUL_RZERO, 709 REAL_MUL_LZERO, REAL_SUB_RZERO, REAL_ADD_RID]); 710 711val COMPLEX_OF_REAL_INV = store_thm("COMPLEX_OF_REAL_INV", 712 ``!x:real. inv (complex_of_real x) = complex_of_real (inv x)``, 713 GEN_TAC THEN ASM_CASES_TAC (``x = 0r``) THEN 714 RW_TAC real_ss [complex_inv, complex_of_real, REAL_INV_0, RE, IM, POW_2, 715 REAL_MUL_RZERO, REAL_ADD_RID, real_div, REAL_MUL_LZERO, 716 REAL_NEG_0, REAL_INV_MUL, REAL_MUL_ASSOC, REAL_MUL_RINV, 717 REAL_MUL_LID]); 718 719val COMPLEX_OF_REAL_SUB = store_thm("COMPLEX_OF_REAL_SUB", 720 ``!x:real y:real. 721 complex_of_real x - complex_of_real y = complex_of_real (x - y)``, 722 REWRITE_TAC [real_sub, COMPLEX_OF_REAL_ADD, COMPLEX_OF_REAL_NEG, 723 complex_sub]); 724 725val COMPLEX_OF_REAL_DIV = store_thm("COMPLEX_OF_REAL_DIV", 726 ``!x:real y:real. 727 complex_of_real x / complex_of_real y = complex_of_real (x / y)``, 728 REWRITE_TAC [real_div, COMPLEX_OF_REAL_MUL, COMPLEX_OF_REAL_INV, 729 complex_div]); 730 731(* ------------------------------------------------------------------ *) 732(* Homomorphic embedding properties for complex_of_num mapping. *) 733(* ------------------------------------------------------------------ *) 734 735val COMPLEX_OF_NUM_EQ = store_thm("COMPLEX_OF_NUM_EQ", 736``!m:num n:num. (complex_of_num m = complex_of_num n) = (m = n)``, 737 REWRITE_TAC[complex_of_num, COMPLEX_OF_REAL_EQ,REAL_OF_NUM_EQ]); 738 739val COMPLEX_OF_NUM_ADD = store_thm("COMPLEX_OF_NUM_ADD", 740 ``!m:num n:num. 741 complex_of_num m + complex_of_num n = complex_of_num (m + n)``, 742 REWRITE_TAC [complex_of_num, REAL_OF_NUM_ADD, COMPLEX_OF_REAL_ADD]); 743 744val COMPLEX_OF_NUM_MUL = store_thm("COMPLEX_OF_NUM_MUL", 745 ``!m:num n:num. 746 complex_of_num m * complex_of_num n = complex_of_num (m * n)``, 747 REWRITE_TAC [complex_of_num, REAL_OF_NUM_MUL, COMPLEX_OF_REAL_MUL]); 748 749(* ------------------------------------------------------------------ *) 750(* A tactical to automate very simple algebraic equivalences. *) 751(* ------------------------------------------------------------------ *) 752 753val SIMPLE_COMPLEX_ARITH_TAC = 754 REWRITE_TAC[COMPLEX_RE_IM_EQ, RE, IM, complex_of_real, complex_add, 755 complex_neg, complex_sub, complex_mul] THEN REAL_ARITH_TAC; 756 757(*--------------------------------------------------------------------*) 758(* Define the left scalar multiplication *) 759(* and right scalar multiplication *) 760(*--------------------------------------------------------------------*) 761 762val complex_scalar_lmul = new_definition 763("complex_scalar_lmul", 764``complex_scalar_lmul (k:real) (z:complex) = (k * RE z,k * IM z)``); 765 766val complex_scalar_rmul = new_definition 767("complex_scalar_rmul", 768``complex_scalar_rmul (z:complex) (k:real) = (RE z * k,IM z * k)``); 769 770val _ = overload_on ("*", Term`$complex_scalar_lmul`); 771val _ = overload_on ("*", Term`$complex_scalar_rmul`); 772 773(*--------------------------------------------------------------------*) 774(* The properities of R-module *) 775(*--------------------------------------------------------------------*) 776 777 778val COMPLEX_SCALAR_LMUL = store_thm("COMPLEX_SCALAR_LMUL", 779 ``!k:real l:real z:complex. k * (l * z) = k * l * z``, 780 REWRITE_TAC[complex_scalar_lmul, RE,IM,REAL_MUL_ASSOC]); 781 782val COMPLEX_SCALAR_LMUL_NEG = store_thm("COMPLEX_SCALAR_LMUL_NEG", 783 ``!k:real z:complex. -(k * z) = -k * z``, 784 REWRITE_TAC[complex_scalar_lmul,complex_neg,RE,IM,REAL_NEG_LMUL]); 785 786val COMPLEX_NEG_SCALAR_LMUL = store_thm("COMPLEX_NEG_SCALAR_LMUL", 787 ``!k:real z:complex. k * (-z) = -k * z``, 788 REWRITE_TAC [complex_neg, complex_scalar_lmul, RE, IM, REAL_MUL_LNEG, 789 REAL_MUL_RNEG]); 790 791val COMPLEX_SCALAR_LMUL_ADD = store_thm("COMPLEX_SCALAR_LMUL_ADD", 792 ``!k:real l:real z:complex. (k + l) * z = k * z + l * z``, 793 REWRITE_TAC[complex_add,complex_scalar_lmul,RE,IM,GSYM REAL_ADD_RDISTRIB]); 794 795val COMPLEX_SCALAR_LMUL_SUB = store_thm("COMPLEX_SCALAR_LMUL_SUB", 796 ``!k:real l:real z:complex. (k - l) * z = k * z - l * z``, 797 REWRITE_TAC [complex_sub, COMPLEX_SCALAR_LMUL_NEG, 798 GSYM COMPLEX_SCALAR_LMUL_ADD, real_sub]); 799 800val COMPLEX_ADD_SCALAR_LMUL = store_thm("COMPLEX_ADD_SCALAR_LMUL", 801 ``!k:real z:complex w:complex. k * (z + w) = k * z + k * w``, 802 REWRITE_TAC[complex_add, complex_scalar_lmul, RE, IM, 803 GSYM REAL_ADD_LDISTRIB]); 804 805val COMPLEX_SUB_SCALAR_LMUL = store_thm("COMPLEX_SUB_SCALAR_LMUL", 806 ``!k:real z:complex w:complex. k * (z - w) = k * z - k * w``, 807 REWRITE_TAC[complex_sub, COMPLEX_ADD_SCALAR_LMUL, COMPLEX_NEG_SCALAR_LMUL, 808 COMPLEX_SCALAR_LMUL_NEG]); 809 810val COMPLEX_MUL_SCALAR_LMUL2 = store_thm("COMPLEX_MUL_SCALAR_LMUL2", 811 ``!k:real l:real z:complex w:complex. 812 (k * z) * (l * w) = (k * l) * (z * w)``, 813 REWRITE_TAC [complex_mul, complex_scalar_lmul, RE, IM, PAIR_EQ] THEN 814 REAL_ARITH_TAC); 815 816val COMPLEX_LMUL_SCALAR_LMUL = store_thm("COMPLEX_LMUL_SCALAR_LMUL", 817 ``!k:real z:complex w:complex. (k * z) * w = k * (z * w)``, 818 REWRITE_TAC [complex_mul, complex_scalar_lmul, RE, IM, PAIR_EQ] THEN 819 REAL_ARITH_TAC); 820 821val COMPLEX_RMUL_SCALAR_LMUL = store_thm("COMPLEX_RMUL_SCALAR_LMUL", 822 ``!k:real z:complex w:complex. z * (k * w) = k * (z * w)``, 823 PROVE_TAC[COMPLEX_MUL_COMM, COMPLEX_LMUL_SCALAR_LMUL]); 824 825val COMPLEX_SCALAR_LMUL_ZERO = store_thm("COMPLEX_SCALAR_LMUL_ZERO", 826 ``!z:complex. 0r * z = 0``, 827 REWRITE_TAC[complex_of_num, complex_of_real, complex_scalar_lmul, 828 REAL_MUL_LZERO]); 829 830val COMPLEX_ZERO_SCALAR_LMUL = store_thm("COMPLEX_ZERO_SCALAR_LMUL", 831 ``!k:real. k * 0c = 0``, 832 REWRITE_TAC[complex_of_num, complex_of_real, complex_scalar_lmul, RE, IM, 833 REAL_MUL_RZERO]); 834 835val COMPLEX_SCALAR_LMUL_ONE = store_thm("COMPLEX_SCALAR_LMUL_ONE", 836 ``!z:complex. 1r * z = z``, 837 REWRITE_TAC[complex_scalar_lmul, REAL_MUL_LID,RE,IM]); 838 839val COMPLEX_SCALAR_LMUL_NEG1 = store_thm ("COMPLEX_SCALAR_LMUL_NEG1", 840 ``!z:complex. -1r * z = -z``, 841 GEN_TAC THEN REWRITE_TAC[GSYM COMPLEX_SCALAR_LMUL_NEG] THEN 842 REWRITE_TAC[COMPLEX_SCALAR_LMUL_ONE]); 843 844val COMPLEX_DOUBLE = store_thm ("COMPLEX_DOUBLE", 845 ``!z:complex. z + z = &2 * z``, 846 GEN_TAC THEN REWRITE_TAC[num_CONV ``2:num``, REAL] THEN 847 REWRITE_TAC[COMPLEX_SCALAR_LMUL_ADD, COMPLEX_SCALAR_LMUL_ONE]); 848 849val COMPLEX_SCALAR_LMUL_ENTIRE = store_thm("COMPLEX_SCALAR_LMUL_ENTIRE", 850 ``!k:real z:complex. (k * z = 0) = (k = 0) \/ (z = 0)``, 851 REWRITE_TAC[COMPLEX_0_THM, complex_scalar_lmul, RE,IM, POW_2, REAL_SUMSQ, 852 REAL_ENTIRE, GSYM LEFT_OR_OVER_AND]); 853 854val COMPLEX_EQ_SCALAR_LMUL = store_thm("COMPLEX_EQ_SCALAR_LMUL", 855 ``!k:real z:complex w:complex. (k * z = k * w) = (k = 0) \/ (z = w)``, 856 ONCE_REWRITE_TAC [GSYM COMPLEX_SUB_0] THEN 857 REWRITE_TAC [GSYM COMPLEX_SUB_SCALAR_LMUL, COMPLEX_SCALAR_LMUL_ENTIRE]); 858 859val COMPLEX_SCALAR_LMUL_EQ = store_thm("COMPLEX_SCALAR_LMUL_EQ", 860 ``!k:real l:real z:complex. 861 (k * z = l * z) = (k = l) \/ (z = 0)``, 862 ONCE_REWRITE_TAC [GSYM COMPLEX_SUB_0] THEN 863 REWRITE_TAC [GSYM COMPLEX_SCALAR_LMUL_SUB, COMPLEX_SCALAR_LMUL_ENTIRE, 864 COMPLEX_SUB_RZERO, REAL_SUB_0]); 865 866val COMPLEX_SCALAR_LMUL_EQ1 = store_thm("COMPLEX_SCALAR_LMUL_EQ1", 867 ``!k:real z:complex. (k * z = z) = (k = 1) \/ (z = 0)``, 868 PROVE_TAC[COMPLEX_SCALAR_LMUL_ONE,COMPLEX_SCALAR_LMUL_EQ]); 869 870val COMPLEX_INV_SCALAR_LMUL = store_thm("COMPLEX_INV_SCALAR_LMUL", 871 ``!k:real z:complex. 872 k <> 0 /\ z <> 0 ==> (inv (k * z) = inv k * inv z)``, 873 REWRITE_TAC [COMPLEX_0_THM, complex_inv,complex_scalar_lmul,RE,IM, POW_MUL, 874 GSYM REAL_ADD_LDISTRIB, real_div, REAL_INV_MUL] THEN 875 REPEAT STRIP_TAC THEN 876 `k pow 2 <> 0` by RW_TAC real_ss[POW_2, REAL_ENTIRE] THEN 877 RW_TAC real_ss[REAL_INV_MUL] THEN 878 `inv (k pow 2) = inv k * inv k` by RW_TAC real_ss[POW_2, REAL_INV_MUL] THEN 879 ASM_REWRITE_TAC[REAL_MUL_ASSOC] THENL[ 880 `k * FST z * inv k * inv k = inv k * k * FST z * inv k` by REAL_ARITH_TAC, 881 `k * SND z * inv k * inv k = inv k * k * SND z * inv k` by REAL_ARITH_TAC 882 ] THEN 883 ASM_REWRITE_TAC[] THEN RW_TAC real_ss[REAL_MUL_LINV,REAL_MUL_COMM]); 884 885val COMPLEX_SCALAR_LMUL_DIV2 = store_thm("COMPLEX_SCALAR_LMUL_DIV2", 886 ``!k l :real z w :complex. 887 (l <> 0 /\ w <> 0) ==> ((k * z) / (l * w) = (k / l) * (z / w))``, 888 REWRITE_TAC [complex_div] THEN REPEAT STRIP_TAC THEN 889 IMP_RES_TAC COMPLEX_INV_SCALAR_LMUL THEN ASM_REWRITE_TAC[] THEN 890 REWRITE_TAC [COMPLEX_MUL_SCALAR_LMUL2, real_div]); 891 892val COMPLEX_SCALAR_MUL_COMM = store_thm("COMPLEX_SCALAR_MUL_COMM", 893 ``!k:real z:complex. k * z = z * k ``, 894 PROVE_TAC[complex_scalar_lmul, complex_scalar_rmul, REAL_MUL_COMM]); 895 896val COMPLEX_SCALAR_RMUL = store_thm("COMPLEX_SCALAR_RMUL", 897 ``!k:real l:real z:complex. z * k * l = z * (k * l)``, 898 RW_TAC bool_ss [GSYM COMPLEX_SCALAR_MUL_COMM, COMPLEX_SCALAR_LMUL, 899 REAL_MUL_COMM]); 900 901val COMPLEX_SCALAR_RMUL_NEG = store_thm("COMPLEX_SCALAR_RMUL_NEG", 902 ``!k:real z:complex. -(z * k) = z * -k ``, 903 REWRITE_TAC [GSYM COMPLEX_SCALAR_MUL_COMM, COMPLEX_SCALAR_LMUL_NEG]); 904 905val COMPLEX_NEG_SCALAR_RMUL = store_thm("COMPLEX_NEG_SCALAR_RMUL", 906 ``!k:real z:complex. (-z) * k = z * -k``, 907 REWRITE_TAC [GSYM COMPLEX_SCALAR_MUL_COMM, COMPLEX_NEG_SCALAR_LMUL]); 908 909val COMPLEX_SCALAR_RMUL_ADD = store_thm("COMPLEX_SCALAR_RMUL_ADD", 910 ``!k:real l:real z:complex. z * (k + l) = z * k + z * l``, 911 REWRITE_TAC [GSYM COMPLEX_SCALAR_MUL_COMM, COMPLEX_SCALAR_LMUL_ADD]); 912 913val COMPLEX_SCALAR_RMUL_SUB = store_thm("COMPLEX_RSCALAR_RMUL_SUB", 914 ``!k: real l:real z:complex. z * (k - l) = z * k - z * l ``, 915 REWRITE_TAC [GSYM COMPLEX_SCALAR_MUL_COMM, COMPLEX_SCALAR_LMUL_SUB]); 916 917val COMPLEX_ADD_SCALAR_RMUL = store_thm("COMPLEX_ADD_RSCALAR_RMUL", 918 ``!k:real z:complex w:complex. (z + w) * k = z * k + w * k``, 919 REWRITE_TAC [GSYM COMPLEX_SCALAR_MUL_COMM, COMPLEX_ADD_SCALAR_LMUL]); 920 921val COMPLEX_SUB_SCALAR_RMUL = store_thm("COMPLEX_SUB_SCALAR_RMUL", 922 ``!k:real z:complex w:complex. (z - w) * k = z * k - w * k ``, 923 REWRITE_TAC [GSYM COMPLEX_SCALAR_MUL_COMM, COMPLEX_SUB_SCALAR_LMUL]); 924 925val COMPLEX_SCALAR_RMUL_ZERO = store_thm("COMPLEX_SCALAR_RMUL_ZERO", 926 ``!z:complex. z * 0r = 0``, 927 REWRITE_TAC[complex_of_num, complex_of_real, complex_scalar_rmul, 928 REAL_MUL_RZERO]); 929 930val COMPLEX_ZERO_SCALAR_RMUL = store_thm("COMPLEX_ZERO_SCALAR_RMUL", 931 ``!k:real. 0 * k = 0``, 932 REWRITE_TAC [GSYM COMPLEX_SCALAR_MUL_COMM, COMPLEX_ZERO_SCALAR_LMUL]); 933 934val COMPLEX_SCALAR_RMUL_ONE = store_thm("COMPLEX_SCALAR_RMUL_ONE", 935 ``!z:complex. z * 1r = z``, 936 REWRITE_TAC [GSYM COMPLEX_SCALAR_MUL_COMM, COMPLEX_SCALAR_LMUL_ONE]); 937 938val COMPLEX_SCALAR_RMUL_NEG1 = store_thm ("COMPLEX_SCALAR_RMUL_NEG1", 939 ``!z:complex. z * -1r = -z``, 940 REWRITE_TAC [GSYM COMPLEX_SCALAR_MUL_COMM, COMPLEX_SCALAR_LMUL_NEG1]); 941 942(*--------------------------------------------------------------------*) 943(* Complex conjugate *) 944(*--------------------------------------------------------------------*) 945 946val conj = new_definition 947 ("conj", ``conj (z:complex) = (RE z, -IM z)``); 948 949val CONJ_REAL_REFL= store_thm("CONJ_REAL_REFL", 950 ``!x:real. conj (complex_of_real x) = complex_of_real x``, 951 REWRITE_TAC[complex_of_real,conj, RE,IM, REAL_NEG_0]); 952 953val CONJ_NUM_REFL= store_thm("CONJ_NUM_REFL", 954 ``!n:num. conj (complex_of_num n) = complex_of_num n``, 955 REWRITE_TAC[complex_of_num,CONJ_REAL_REFL]); 956 957val CONJ_ADD = store_thm("CONJ_ADD", 958 ``!z:complex w:complex. conj (z + w) = conj z + conj w``, 959 REWRITE_TAC [conj,complex_add,RE,IM,REAL_NEG_ADD]); 960 961val CONJ_NEG = store_thm("CONJ_NEG", 962 ``!z:complex. conj (-z) = -conj z ``, 963 REWRITE_TAC [complex_neg, conj,RE,IM]); 964 965val CONJ_SUB = store_thm("CONJ_SUB", 966 ``!z:complex w:complex. conj (z - w) = conj z - conj w``, 967 REWRITE_TAC [complex_sub, CONJ_NEG, CONJ_ADD]); 968 969val CONJ_MUL = store_thm("CONJ_MUL", 970 ``!z:complex w:complex. conj (z * w) = conj z * conj w``, 971 REWRITE_TAC [conj,complex_mul, RE,IM,REAL_NEG_ADD, REAL_NEG_MUL2, 972 GSYM REAL_NEG_LMUL, GSYM REAL_NEG_RMUL]); 973 974val CONJ_INV = store_thm("CONJ_INV", 975 ``!z: complex. conj (inv z) = inv (conj z)``, 976 RW_TAC real_ss [conj, complex_inv, RE, IM, POW_2, real_div]); 977 978val CONJ_DIV= store_thm("CONJ_DIV", 979 ``!z:complex w. conj (z / w) = conj z / conj w``, 980 REWRITE_TAC[complex_div, CONJ_MUL, CONJ_INV]); 981 982val CONJ_SCALAR_LMUL = store_thm("CONJ_SCALAR_LMUL", 983 ``!k:real z:complex. conj (k * z) = k * conj z``, 984 REWRITE_TAC [conj,complex_scalar_lmul, RE,IM,REAL_MUL_RNEG]); 985 986val CONJ_CONJ = store_thm("CONJ_CONJ", 987 ``!z:complex. conj (conj z) = z``, 988 REWRITE_TAC[conj, RE,IM,REAL_NEGNEG]); 989 990val CONJ_EQ = store_thm("CONJ_EQ", 991 ``!z:complex w:complex. (conj z = w) = (z = conj w)``, 992 REWRITE_TAC [conj, COMPLEX_RE_IM_EQ, RE, IM, REAL_NEG_EQ]); 993 994val CONJ_EQ2 = store_thm("CONJ_EQ2", 995 ``!z:complex w:complex. (conj z = conj w) = (z = w)``, 996 REWRITE_TAC [CONJ_EQ, CONJ_CONJ]); 997 998val COMPLEX_MUL_RCONJ = store_thm("COMPLEX_MUL_RCONJ", 999 ``!z:complex. 1000 z * conj z = complex_of_real ((RE z) pow 2 + (IM z) pow 2)``, 1001 REWRITE_TAC [complex_mul, conj, complex_of_real, RE, IM, REAL_MUL_RNEG, 1002 REAL_SUB_RNEG] THEN 1003 PROVE_TAC [POW_2, REAL_MUL_COMM, REAL_ADD_LINV]); 1004 1005val COMPLEX_MUL_LCONJ = store_thm("COMPLEX_MUL_RCONJ", 1006 ``!z:complex. 1007 conj z * z = complex_of_real ((RE z) pow 2 + (IM z) pow 2)``, 1008 PROVE_TAC [COMPLEX_MUL_COMM, COMPLEX_MUL_RCONJ]); 1009 1010val CONJ_ZERO = store_thm("CONJ_ZERO", 1011 ``conj 0 = 0``, 1012 REWRITE_TAC [CONJ_NUM_REFL]); 1013 1014(*--------------------------------------------------------------------*) 1015(* Define modulus and argument principal value of complex *) 1016(*--------------------------------------------------------------------*) 1017 1018val modu = new_definition("modu", 1019 ``modu (z:complex) = sqrt( RE z pow 2 + IM z pow 2)``); 1020 1021val arg = new_definition("arg", 1022 ``arg z = 1023 if 0 <= IM z then acs (RE z / modu z) 1024 else -acs (RE z / modu z) + 2 * pi``); 1025 1026(*--------------------------------------------------------------------*) 1027(* The properities of modulus and argument principal value *) 1028(*--------------------------------------------------------------------*) 1029 1030val MODU_POW2 = store_thm("MODU_POW2", 1031 ``!z:complex. modu z pow 2 = RE z pow 2 + IM z pow 2 ``, 1032 REWRITE_TAC[modu] THEN 1033 PROVE_TAC [REAL_LE_POW2, REAL_LE_ADD, SQRT_POW_2]); 1034 1035val RE_IM_LE_MODU= store_thm("RE_IM_LE_MODU", 1036 ``!z:complex. abs (RE z) <= modu z /\ abs (IM z) <= modu z``, 1037 REWRITE_TAC [modu] THEN GEN_TAC THEN CONJ_TAC THENL 1038 [REWRITE_TAC [COMPLEX_LEMMA2], 1039 ONCE_REWRITE_TAC [REAL_ADD_COMM] THEN REWRITE_TAC [COMPLEX_LEMMA2]]); 1040 1041val MODU_POS= store_thm("MODU_POS", 1042 ``!z:complex. 0 <= modu z``, 1043 GEN_TAC THEN REWRITE_TAC[modu] THEN MATCH_MP_TAC SQRT_POS_LE THEN 1044 MATCH_MP_TAC REAL_LE_ADD THEN REWRITE_TAC[REAL_LE_POW2]); 1045 1046val COMPLEX_MUL_RCONJ1 = store_thm("COMPLEX_MUL_RCONJ1", 1047 ``!z:complex. z * conj z = complex_of_real ((modu z) pow 2)``, 1048 REWRITE_TAC[COMPLEX_MUL_RCONJ, MODU_POW2]); 1049 1050val COMPLEX_MUL_LCONJ1 = store_thm("COMPLEX_MUL_LCONJ1", 1051 ``!z:complex. conj z * z = complex_of_real ((modu z) pow 2)``, 1052 REWRITE_TAC[COMPLEX_MUL_LCONJ, MODU_POW2]); 1053 1054val MODU_NEG = store_thm("MODU_NEG", 1055 ``!z:complex. modu (-z) = modu z``, 1056 REWRITE_TAC[modu,complex_neg,RE,IM,POW_2,REAL_NEG_MUL2]); 1057 1058val MODU_SUB = store_thm("MODU_SUB", 1059 ``!z:complex w:complex. modu (z - w) = modu (w - z)``, 1060 REPEAT GEN_TAC THEN 1061 `w - z = -(z - w)` by REWRITE_TAC[COMPLEX_NEG_SUB] THEN 1062 ASM_REWRITE_TAC[] THEN REWRITE_TAC[MODU_NEG]); 1063 1064val MODU_CONJ = store_thm("MODU_CONJ", 1065 ``!z:complex. modu (conj z) = modu z ``, 1066 REWRITE_TAC[modu, conj,RE,IM,POW_2,REAL_NEG_MUL2]); 1067 1068val MODU_MUL = store_thm("MODU_MUL", 1069 ``!z:complex w:complex. modu (z * w) = modu z * modu w``, 1070 REWRITE_TAC [modu, complex_mul, RE, IM, COMPLEX_LEMMA1] THEN 1071 PROVE_TAC [REAL_LE_POW2, REAL_LE_ADD, SQRT_MUL]); 1072 1073val MODU_0 = store_thm("MODU_0", 1074 ``modu 0 = 0 ``, 1075 REWRITE_TAC[complex_of_num,complex_of_real, modu, RE, IM, POW_2, 1076 REAL_MUL_RZERO, REAL_ADD_RID, SQRT_0]); 1077 1078val MODU_1 = store_thm("MODU_1", 1079 ``modu 1 = 1 ``, 1080 REWRITE_TAC[complex_of_num,complex_of_real, modu, RE, IM, POW_2, 1081 REAL_MUL_RID, REAL_MUL_RZERO, REAL_ADD_RID, SQRT_1]); 1082 1083val MODU_COMPLEX_INV = store_thm("MODU_COMPLEX_INV", 1084 ``!z: complex. z <> 0 ==> (modu (inv z) = inv (modu z))``, 1085 REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LINV_UNIQ THEN 1086 REWRITE_TAC[GSYM MODU_MUL] THEN 1087 FIRST_ASSUM(fn th => REWRITE_TAC[MATCH_MP COMPLEX_MUL_LINV th]) THEN 1088 REWRITE_TAC [MODU_1]); 1089 1090val MODU_DIV = store_thm("MODU_DIV", 1091 ``!z w : complex. (w <> 0) ==> (modu(z / w) = modu z / modu w) ``, 1092 REWRITE_TAC[complex_div, MODU_MUL] THEN REPEAT STRIP_TAC THEN 1093 FIRST_ASSUM(fn th => REWRITE_TAC[MATCH_MP MODU_COMPLEX_INV th]) THEN 1094 REWRITE_TAC[real_div]); 1095 1096val MODU_SCALAR_LMUL = store_thm("MODU_SCALAR_LMUL", 1097 ``!k:real z:complex. modu (k * z) = abs k * modu z``, 1098 REWRITE_TAC [modu, complex_scalar_lmul, RE, IM, POW_MUL, 1099 GSYM REAL_ADD_LDISTRIB] THEN 1100 ONCE_REWRITE_TAC [GSYM REAL_POW2_ABS] THEN 1101 PROVE_TAC[REAL_ABS_POS,REAL_LE_POW2,REAL_LE_ADD,SQRT_MUL,POW_2_SQRT]); 1102 1103val MODU_REAL = store_thm("MODU_REAL", 1104 ``!x:real. modu (complex_of_real x) = abs x``, 1105 REWRITE_TAC [complex_of_real, modu, RE, IM, POW_2, REAL_MUL_RZERO, 1106 REAL_ADD_RID] THEN 1107 REWRITE_TAC [GSYM POW_2] THEN 1108 ONCE_REWRITE_TAC [GSYM REAL_POW2_ABS] THEN GEN_TAC THEN 1109 `0 <= abs x` by PROVE_TAC [REAL_ABS_POS] THEN 1110 FIRST_ASSUM (fn th => REWRITE_TAC [MATCH_MP POW_2_SQRT th])); 1111 1112val MODU_NUM = store_thm("MODU_NUM", 1113 ``!n:num. modu (complex_of_num n) = &n``, 1114 REWRITE_TAC [complex_of_num, MODU_REAL, ABS_N]); 1115 1116val MODU_ZERO = store_thm("MODU_ZERO", 1117 ``!z:complex. (z = 0) = (modu z = 0)``, 1118 GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN 1119 ASM_REWRITE_TAC[MODU_0, COMPLEX_0_THM, GSYM MODU_POW2, 1120 num_CONV (``2:num``), POW_0]); 1121 1122val MODU_NZ = store_thm("MODU_NZ", 1123 ``!z:complex. (z <> 0) = 0 < modu z``, 1124 GEN_TAC THEN EQ_TAC THENL [ 1125 REWRITE_TAC[MODU_ZERO] THEN 1126 DISCH_TAC THEN 1127 PROVE_TAC[REAL_LE_LT, MODU_POS], 1128 CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[] THEN 1129 DISCH_THEN SUBST1_TAC THEN 1130 REWRITE_TAC[MODU_0, REAL_LT_REFL] 1131 ]); 1132 1133val MODU_CASES = store_thm("MODU_CASES", 1134 ``!z:complex. (z = 0) \/ 0 < modu z``, 1135 GEN_TAC THEN REWRITE_TAC[GSYM MODU_NZ] THEN 1136 Cases_on `z = 0` THEN ASM_REWRITE_TAC[]); 1137 1138val RE_DIV_MODU_BOUNDS = store_thm("RE_DIV_MODU_BOUNDS", 1139 ``!z:complex. 1140 z <> 0 ==> (-1 <= RE z / modu z /\ RE z / modu z <= 1)``, 1141 GEN_TAC THEN DISCH_TAC THEN CONJ_TAC THENL [ 1142 MATCH_MP_TAC REAL_LE_RDIV THEN CONJ_TAC THENL [ 1143 PROVE_TAC[MODU_NZ], 1144 REWRITE_TAC[REAL_MUL_LNEG,REAL_MUL_LID] THEN 1145 PROVE_TAC[RE_IM_LE_MODU,ABS_BOUNDS] 1146 ], 1147 MATCH_MP_TAC REAL_LE_LDIV THEN CONJ_TAC THENL [ 1148 PROVE_TAC[MODU_NZ], 1149 REWRITE_TAC[REAL_MUL_LNEG,REAL_MUL_LID] THEN 1150 PROVE_TAC[RE_IM_LE_MODU,ABS_BOUNDS] 1151 ] 1152 ]); 1153 1154val IM_DIV_MODU_BOUNDS = store_thm("IM_DIV_MODU_BOUNDS", 1155 ``!z:complex. 1156 z <> 0 ==> (-1 <= IM z / modu z /\ IM z / modu z <= 1)``, 1157 GEN_TAC THEN DISCH_TAC THEN CONJ_TAC THENL [ 1158 MATCH_MP_TAC REAL_LE_RDIV THEN CONJ_TAC THENL [ 1159 PROVE_TAC[MODU_NZ], 1160 REWRITE_TAC[REAL_MUL_LNEG,REAL_MUL_LID] THEN 1161 PROVE_TAC[RE_IM_LE_MODU,ABS_BOUNDS] 1162 ], 1163 MATCH_MP_TAC REAL_LE_LDIV THEN CONJ_TAC THENL [ 1164 PROVE_TAC[MODU_NZ], 1165 REWRITE_TAC[REAL_MUL_LID] THEN 1166 PROVE_TAC[RE_IM_LE_MODU,ABS_BOUNDS] 1167 ] 1168 ]); 1169 1170val RE_DIV_MODU_ACS_BOUNDS = store_thm("RE_DIV_MODU_ACS_BOUNDS", 1171 ``!z:complex. 1172 z <> 0 ==> 1173 (0 <=acs (RE z / modu z) /\ acs (RE z / modu z) <= pi)``, 1174 GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC ACS_BOUNDS THEN 1175 POP_ASSUM MP_TAC THEN MATCH_ACCEPT_TAC RE_DIV_MODU_BOUNDS); 1176 1177val IM_DIV_MODU_ASN_BOUNDS = store_thm("IM_DIV_MODU_ASN_BOUNDS", 1178 ``!z:complex. 1179 z <> 0 ==> 1180 (-(pi/2) <= asn (IM z / modu z) /\ asn (IM z / modu z) <= pi/2)``, 1181 GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC ASN_BOUNDS THEN 1182 POP_ASSUM MP_TAC THEN MATCH_ACCEPT_TAC IM_DIV_MODU_BOUNDS); 1183 1184val RE_DIV_MODU_ACS_COS = store_thm("RE_DIV_MODU_ACS_COS", 1185 ``!z:complex. 1186 z <> 0 ==> (cos ( acs (RE z / modu z)) = RE z / modu z)``, 1187 GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC ACS_COS THEN 1188 POP_ASSUM MP_TAC THEN MATCH_ACCEPT_TAC RE_DIV_MODU_BOUNDS ); 1189 1190val IM_DIV_MODU_ASN_SIN = store_thm("IM_DIV_MODU_ASN_SIN", 1191 ``!z:complex. 1192 z <> 0 ==> (sin ( asn (IM z / modu z)) = IM z / modu z)``, 1193 GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC ASN_SIN THEN 1194 POP_ASSUM MP_TAC THEN MATCH_ACCEPT_TAC IM_DIV_MODU_BOUNDS); 1195 1196val ARG_COS = store_thm("ARG_COS", 1197 ``!z:complex. z <> 0 ==> (cos (arg z) = RE z / modu z)``, 1198 GEN_TAC THEN DISCH_TAC THEN 1199 REWRITE_TAC[arg] THEN COND_CASES_TAC THEN 1200 REWRITE_TAC[COS_PERIODIC, COS_NEG] THEN 1201 MATCH_MP_TAC RE_DIV_MODU_ACS_COS THEN ASM_REWRITE_TAC[]); 1202 1203val ARG_SIN = store_thm("ARG_SIN", 1204 ``!z:complex. z <> 0 ==> (sin (arg z) = IM z / modu z)``, 1205 GEN_TAC THEN DISCH_TAC THEN 1206 REWRITE_TAC[arg] THEN COND_CASES_TAC THENL [ 1207 Q.SUBGOAL_THEN 1208 `sin (acs (RE z / modu z)) = sqrt (1 - cos (acs (RE z / modu z)) pow 2)` 1209 ASSUME_TAC 1210 THENL [ 1211 MATCH_MP_TAC SIN_COS_SQ THEN 1212 MATCH_MP_TAC RE_DIV_MODU_ACS_BOUNDS THEN 1213 ASM_REWRITE_TAC[], 1214 ASM_REWRITE_TAC[] THEN 1215 FIRST_ASSUM (fn th => REWRITE_TAC [MATCH_MP RE_DIV_MODU_ACS_COS th]) THEN 1216 Q.SUBGOAL_THEN `1 - (RE z / modu z) pow 2 = (IM z / modu z) pow 2 ` 1217 ASSUME_TAC 1218 THENL [ 1219 REWRITE_TAC[REAL_EQ_SUB_RADD, REAL_POW_DIV, REAL_DIV_ADD] THEN 1220 ONCE_REWRITE_TAC[REAL_ADD_COMM] THEN 1221 REWRITE_TAC[GSYM MODU_POW2] THEN CONV_TAC SYM_CONV THEN 1222 MATCH_MP_TAC REAL_DIV_REFL THEN 1223 ASM_REWRITE_TAC[MODU_POW2, GSYM COMPLEX_0_THM], 1224 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC POW_2_SQRT THEN 1225 MATCH_MP_TAC REAL_LE_DIV THEN ASM_REWRITE_TAC[MODU_POS] 1226 ] 1227 ], 1228 REWRITE_TAC[SIN_PERIODIC,SIN_NEG, REAL_NEG_EQ] THEN 1229 Q.SUBGOAL_THEN 1230 `sin (acs (RE z / modu z)) = sqrt (1 - cos (acs (RE z / modu z)) pow 2)` 1231 ASSUME_TAC 1232 THENL [ 1233 MATCH_MP_TAC SIN_COS_SQ THEN 1234 MATCH_MP_TAC RE_DIV_MODU_ACS_BOUNDS THEN 1235 ASM_REWRITE_TAC[], 1236 ASM_REWRITE_TAC[] THEN 1237 FIRST_ASSUM (fn th => REWRITE_TAC [MATCH_MP RE_DIV_MODU_ACS_COS th]) THEN 1238 `1 - (RE z / modu z) pow 2 = (IM z / modu z) pow 2` 1239 by (REWRITE_TAC[REAL_EQ_SUB_RADD, REAL_POW_DIV, REAL_DIV_ADD] THEN 1240 ONCE_REWRITE_TAC[REAL_ADD_COMM] THEN 1241 REWRITE_TAC[GSYM MODU_POW2] THEN CONV_TAC SYM_CONV THEN 1242 MATCH_MP_TAC REAL_DIV_REFL THEN 1243 ASM_REWRITE_TAC[MODU_POW2, GSYM COMPLEX_0_THM]) THEN 1244 ASM_REWRITE_TAC[] THEN 1245 ONCE_REWRITE_TAC[GSYM REAL_POW2_ABS] THEN 1246 ONCE_REWRITE_TAC[GSYM ABS_NEG] THEN 1247 REWRITE_TAC[REAL_POW2_ABS] THEN 1248 MATCH_MP_TAC POW_2_SQRT THEN 1249 REWRITE_TAC[real_div, REAL_NEG_LMUL] THEN 1250 REWRITE_TAC[GSYM real_div] THEN 1251 MATCH_MP_TAC REAL_LE_DIV THEN 1252 PROVE_TAC [MODU_POS, REAL_NOT_LE, REAL_NEG_GT0, REAL_LT_IMP_LE] 1253 ] 1254 ]); 1255 1256val RE_MODU_ARG = store_thm("RE_MODU_ARG", 1257 ``!z:complex. RE z = modu z * cos (arg z)``, 1258 GEN_TAC THEN ASM_CASES_TAC (``z = 0``) THENL 1259 [ASM_REWRITE_TAC[MODU_0] THEN 1260 REWRITE_TAC[complex_of_num,complex_of_real,RE,REAL_MUL_LZERO], 1261 FIRST_ASSUM (fn th => REWRITE_TAC [MATCH_MP ARG_COS th]) THEN 1262 CONV_TAC SYM_CONV THEN 1263 MATCH_MP_TAC REAL_DIV_LMUL THEN 1264 ASM_REWRITE_TAC[GSYM MODU_ZERO] 1265 ]); 1266 1267val IM_MODU_ARG = store_thm("IM_MODU_ARG", 1268 ``!z:complex. IM z = modu z * sin (arg z)``, 1269 GEN_TAC THEN ASM_CASES_TAC (``z = 0``) THENL [ 1270 ASM_REWRITE_TAC[MODU_0] THEN 1271 REWRITE_TAC[complex_of_num,complex_of_real,IM,REAL_MUL_LZERO], 1272 FIRST_ASSUM (fn th => REWRITE_TAC [MATCH_MP ARG_SIN th]) THEN 1273 CONV_TAC SYM_CONV THEN 1274 MATCH_MP_TAC REAL_DIV_LMUL THEN 1275 ASM_REWRITE_TAC[GSYM MODU_ZERO] 1276 ]); 1277 1278val COMPLEX_TRIANGLE = store_thm("COMPLEX_TRIANGLE", 1279 ``!z:complex. modu z * (cos (arg z),sin (arg z)) = z``, 1280 REWRITE_TAC[complex_scalar_lmul, RE, IM, GSYM RE_MODU_ARG, GSYM IM_MODU_ARG]); 1281 1282val COMPLEX_MODU_ARG_EQ = store_thm("COMPLEX_MODU_ARG_EQ", 1283 ``!z:complex w. (z = w) = ((modu z = modu w) /\ (arg z = arg w))``, 1284 REPEAT GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN 1285 ASM_REWRITE_TAC[COMPLEX_RE_IM_EQ,RE_MODU_ARG,IM_MODU_ARG]); 1286 1287val MODU_UNIT = store_thm("MODU_UNIT", 1288 ``!x:real y. modu (cos x,sin x) = 1``, 1289 REWRITE_TAC [modu, RE, IM] THEN ONCE_REWRITE_TAC[REAL_ADD_COMM] 1290 THEN REWRITE_TAC[SIN_CIRCLE, SQRT_1]); 1291 1292val COMPLEX_MUL_ARG = store_thm("COMPLEX_MUL_ARG", 1293 ``!x:real y:real. 1294 (cos x,sin x) * (cos y, sin y) = (cos (x + y),sin (x + y))``, 1295 REWRITE_TAC [complex_mul, RE, IM, SIN_ADD, COS_ADD] THEN 1296 PROVE_TAC [REAL_ADD_COMM]); 1297 1298val COMPLEX_INV_ARG = store_thm("COMPLEX_INV_ARG", 1299 ``!x:real. inv (cos x,sin x) = (cos (-x),sin (-x))``, 1300 REWRITE_TAC [complex_inv, RE, IM] THEN 1301 ONCE_REWRITE_TAC [REAL_ADD_COMM] THEN 1302 REWRITE_TAC[SIN_CIRCLE, real_div, REAL_INV1,REAL_MUL_RID, COS_NEG, SIN_NEG]); 1303 1304val COMPLEX_DIV_ARG = store_thm("COMPLEX_DIV_ARG", 1305 ``!x:real y. 1306 (cos x,sin x) / (cos y, sin y) = (cos(x - y),sin(x - y))``, 1307 REWRITE_TAC[complex_div,COMPLEX_INV_ARG,COMPLEX_MUL_ARG,real_sub]); 1308 1309(*--------------------------------------------------------------------*) 1310(* The operation of nature numbers power of complex numbers *) 1311(*--------------------------------------------------------------------*) 1312 1313val complex_pow = Define 1314`(complex_pow (z:complex) 0 = 1) /\ 1315 (complex_pow (z:complex) (SUC n) = z * (complex_pow z n))`; 1316 1317val _ = overload_on ("pow", Term`$complex_pow`); 1318 1319val COMPLEX_POW_0 = store_thm("COMPLEX_POW_0", 1320 ``!n:num. 0 pow (SUC n) = 0``, 1321 INDUCT_TAC THEN REWRITE_TAC[complex_pow, COMPLEX_MUL_LZERO]); 1322 1323val COMPLEX_POW_NZ = store_thm("COMPLEX_POW_NZ", 1324 ``!z:complex n:num. (z <> 0) ==> (z pow n <> 0)``, 1325 REPEAT GEN_TAC THEN DISCH_TAC THEN 1326 SPEC_TAC((``n:num``),(``n:num``)) THEN INDUCT_TAC THEN 1327 ASM_REWRITE_TAC[complex_pow, COMPLEX_10, COMPLEX_ENTIRE]); 1328 1329val COMPLEX_POWINV = store_thm("COMPLEX_POWINV", 1330 ``!z:complex. 1331 ~(z = 0) ==> !n:num. (inv(z pow n) = (inv z) pow n)``, 1332 GEN_TAC THEN DISCH_TAC THEN INDUCT_TAC THEN 1333 REWRITE_TAC[complex_pow, COMPLEX_INV1] THEN 1334 MP_TAC(SPECL [(``z:complex``), (``z pow n``)] COMPLEX_INV_MUL) THEN 1335 ASM_REWRITE_TAC[] THEN 1336 SUBGOAL_THEN (``~(z pow n = 0)``) ASSUME_TAC THENL 1337 [MATCH_MP_TAC COMPLEX_POW_NZ THEN ASM_REWRITE_TAC[], ALL_TAC] 1338 THEN ASM_REWRITE_TAC[]); 1339 1340val MODU_COMPLEX_POW = store_thm("MODU_COMPLEX_POW", 1341 ``!z:complex n:num. modu (z pow n) = modu z pow n``, 1342 GEN_TAC THEN INDUCT_TAC THEN 1343 ASM_REWRITE_TAC[complex_pow,pow, MODU_1, MODU_MUL]); 1344 1345val COMPLEX_POW_ADD = store_thm("COMPLEX_POW_ADD", 1346 ``!z:complex m:num n. z pow (m + n) = (z pow m) * (z pow n)``, 1347 GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN 1348 ASM_REWRITE_TAC[complex_pow, ADD_CLAUSES, COMPLEX_MUL_RID] THEN 1349 CONV_TAC(AC_CONV(COMPLEX_MUL_ASSOC,COMPLEX_MUL_COMM))); 1350 1351val COMPLEX_POW_1 = store_thm("COMPLEX_POW_1", 1352 ``!z:complex. z pow 1 = z``, 1353 GEN_TAC THEN REWRITE_TAC[num_CONV (``1:num``)] THEN 1354 REWRITE_TAC[complex_pow, COMPLEX_MUL_RID]); 1355 1356val COMPLEX_POW_2 = store_thm("COMPLEX_POW_2", 1357 ``!z:complex. z pow 2 = z * z``, 1358 GEN_TAC THEN REWRITE_TAC[num_CONV ``2:num``] THEN 1359 REWRITE_TAC[complex_pow, COMPLEX_POW_1]); 1360 1361val COMPLEX_POW_ONE = store_thm("COMPLEX_POW_ONE", 1362 ``!n:num. 1 pow n = 1``, 1363 INDUCT_TAC THEN ASM_REWRITE_TAC[complex_pow, COMPLEX_MUL_LID]); 1364 1365val COMPLEX_POW_MUL = store_thm("COMPLEX_POW_MUL", 1366 ``!n:num z:complex w:complex. (z * w) pow n = (z pow n) * (w pow n)``, 1367 INDUCT_TAC THEN REWRITE_TAC[complex_pow, COMPLEX_MUL_LID] THEN 1368 REPEAT GEN_TAC THEN ASM_REWRITE_TAC[] THEN 1369 CONV_TAC(AC_CONV(COMPLEX_MUL_ASSOC,COMPLEX_MUL_COMM))); 1370 1371val COMPLEX_POW_INV = store_thm("COMPLEX_POW_INV", 1372 ``!z:complex n:num. (inv z) pow n = inv (z pow n)``, 1373 Induct_on `n` THEN REWRITE_TAC [complex_pow] THENL 1374 [REWRITE_TAC [COMPLEX_INV1], 1375 GEN_TAC THEN Cases_on `z = 0` THENL 1376 [POP_ASSUM SUBST_ALL_TAC 1377 THEN REWRITE_TAC [COMPLEX_INV_0,COMPLEX_MUL_LZERO], 1378 `~(z pow n = 0)` by PROVE_TAC [COMPLEX_POW_NZ] THEN 1379 IMP_RES_TAC COMPLEX_INV_MUL THEN ASM_REWRITE_TAC []]]); 1380 1381val COMPLEX_POW_DIV = store_thm("COMPLEX_POW_DIV", 1382 ``!z:complex w:complex n:num. (z / w) pow n = (z pow n) / (w pow n)``, 1383 REWRITE_TAC[complex_div, COMPLEX_POW_MUL, COMPLEX_POW_INV]); 1384 1385val COMPLEX_POW_SCALAR_LMUL = store_thm("COMPLEX_POW_L", 1386 ``!n:num k:real z:complex. (k * z) pow n = (k pow n) * (z pow n)``, 1387 INDUCT_TAC THEN 1388 REWRITE_TAC[complex_pow, pow, COMPLEX_SCALAR_LMUL_ONE] THEN 1389 REPEAT GEN_TAC THEN ASM_REWRITE_TAC[] THEN 1390 REWRITE_TAC[COMPLEX_MUL_SCALAR_LMUL2]); 1391 1392val COMPLEX_POW_ZERO = store_thm("COMPLEX_POW_ZERO", 1393 ``!n:num z:complex. (z pow n = 0) ==> (z = 0)``, 1394 INDUCT_TAC THEN GEN_TAC THEN REWRITE_TAC[complex_pow] THEN 1395 REWRITE_TAC[COMPLEX_10, COMPLEX_ENTIRE] THEN 1396 DISCH_THEN(DISJ_CASES_THEN2 ACCEPT_TAC ASSUME_TAC) THEN 1397 FIRST_ASSUM MATCH_MP_TAC THEN FIRST_ASSUM ACCEPT_TAC); 1398 1399val COMPLEX_POW_ZERO_EQ = store_thm("COMPLEX_POW_ZERO_EQ", 1400 ``!n:num z:complex. (z pow (SUC n) = 0) = (z = 0)``, 1401 REPEAT GEN_TAC THEN EQ_TAC THEN 1402 REWRITE_TAC[COMPLEX_POW_ZERO] THEN 1403 DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[COMPLEX_POW_0]); 1404 1405val COMPLEX_POW_POW = store_thm("COMPLEX_POW_POW", 1406 ``!z:complex m:num n:num. (z pow m) pow n = z pow (m * n)``, 1407 GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN 1408 ASM_REWRITE_TAC[complex_pow, MULT_CLAUSES, COMPLEX_POW_ADD]); 1409 1410val DE_MOIVRE_LEMMA = store_thm("DE_MOIVRE_LEMMA", 1411 ``!x:real n:num. (cos x, sin x) pow n = (cos (&n * x), sin(&n * x))``, 1412 GEN_TAC THEN INDUCT_TAC THEN 1413 ASM_REWRITE_TAC [complex_pow, REAL_MUL_LZERO, COS_0, SIN_0, complex_of_num, 1414 complex_of_real, COMPLEX_MUL_ARG] THEN 1415 ONCE_REWRITE_TAC [REAL_ADD_COMM] THEN 1416 REWRITE_TAC[REAL, REAL_ADD_RDISTRIB, REAL_MUL_LID]); 1417 1418val DE_MOIVRE_THM = store_thm("DE_MOIVRE_THM", 1419 ``!z:complex n:num. 1420 (modu z * (cos (arg z),sin (arg z))) pow n = 1421 modu z pow n * (cos (&n * arg z),sin(&n * arg z))``, 1422 REWRITE_TAC[COMPLEX_POW_SCALAR_LMUL, DE_MOIVRE_LEMMA]); 1423 1424(*--------------------------------------------------------------------*) 1425(*Exponential form of complex numbers *) 1426(*--------------------------------------------------------------------*) 1427 1428val complex_exp = new_definition("complex_exp", 1429 ``complex_exp (z:complex) = exp(RE z) * (cos (IM z),sin (IM z))``); 1430 1431val _ = overload_on ("exp", Term`$complex_exp`); 1432 1433val EXP_IMAGINARY = store_thm("EXP_IMAGINARY", 1434 ``!x:real. exp (i * x) = (cos x,sin x)``, 1435 REWRITE_TAC[complex_exp, i, complex_scalar_rmul, RE, IM, REAL_MUL_LZERO, 1436 REAL_MUL_LID, EXP_0, COMPLEX_SCALAR_LMUL_ONE]); 1437 1438val EULER_FORMULE = store_thm("EULER_FORMULE", 1439 ``!z:complex. modu z * exp (i * arg z) = z``, 1440 REWRITE_TAC[complex_exp, i, complex_scalar_rmul, RE, IM, REAL_MUL_LZERO, 1441 REAL_MUL_LID, EXP_0, COMPLEX_SCALAR_LMUL_ONE, COMPLEX_TRIANGLE]); 1442 1443val COMPLEX_EXP_ADD = store_thm("COMPLEX_EXP_ADD", 1444 ``!z:complex w:complex. exp (z + w) = exp z * exp w``, 1445 REWRITE_TAC[complex_exp, COMPLEX_MUL_SCALAR_LMUL2, GSYM EXP_ADD, 1446 COMPLEX_MUL_ARG, complex_add, RE, IM]); 1447 1448val COMPLEX_EXP_NEG = store_thm("COMPLEX_EXP_NEG", 1449 ``!z:complex. exp (-z) = inv (exp z)``, 1450 GEN_TAC THEN 1451 REWRITE_TAC [complex_exp, complex_neg, RE, IM, EXP_NEG, 1452 GSYM COMPLEX_INV_ARG] THEN 1453 CONV_TAC SYM_CONV THEN MATCH_MP_TAC COMPLEX_INV_SCALAR_LMUL THEN 1454 REWRITE_TAC[EXP_NZ, MODU_NZ, MODU_UNIT, REAL_LT_01]); 1455 1456val COMPLEX_EXP_SUB = store_thm("COMPLEX_EXP_SUB", 1457 ``!z:complex w:complex. exp (z - w) = exp z / exp w``, 1458 REWRITE_TAC[complex_sub,COMPLEX_EXP_ADD,COMPLEX_EXP_NEG,complex_div]); 1459 1460val COMPLEX_EXP_N = store_thm("COMPLEX_EXP_N", 1461 ``!z:complex n:num. exp (&n : real * z) = exp z pow n``, 1462 REWRITE_TAC[complex_scalar_lmul] THEN 1463 REWRITE_TAC[complex_exp, RE, IM, EXP_N, GSYM DE_MOIVRE_LEMMA, 1464 COMPLEX_POW_SCALAR_LMUL]); 1465 1466val COMPLEX_EXP_N2 = store_thm("COMPLEX_EXP_N2", 1467 ``!z:complex n:num. exp (&n :complex * z) = exp z pow n``, 1468 REWRITE_TAC[complex_mul, complex_of_num, RE_COMPLEX_OF_REAL, 1469 IM_COMPLEX_OF_REAL, REAL_MUL_LZERO, REAL_ADD_RID,REAL_SUB_RZERO, 1470 GSYM complex_scalar_lmul, COMPLEX_EXP_N]); 1471 1472val COMPLEX_EXP_0 = store_thm("COMPLEX_EXP_0", 1473 ``exp 0c = 1``, 1474 REWRITE_TAC[complex_of_num, complex_of_real, complex_exp, RE, IM, EXP_0, 1475 COS_0, SIN_0, COMPLEX_SCALAR_LMUL_ONE]); 1476 1477val COMPLEX_EXP_NZ = store_thm("COMPLEX_EXP_NZ", 1478 ``!z:complex. exp z <> 0``, 1479 REWRITE_TAC[complex_exp, COMPLEX_SCALAR_LMUL_ENTIRE] THEN 1480 REWRITE_TAC[EXP_NZ, MODU_NZ, MODU_UNIT, REAL_LT_01]); 1481 1482val COMPLEX_EXP_ADD_MUL = store_thm("COMPLEX_EXP_ADD_MUL", 1483 ``!z:complex w:complex. exp (z + w) * exp (-z) = exp w``, 1484 REWRITE_TAC[GSYM COMPLEX_EXP_ADD, GSYM complex_sub, COMPLEX_ADD_SUB]); 1485 1486val COMPLEX_EXP_NEG_MUL = store_thm("COMPLEX_EXP_NEG_MUL", 1487 ``!z:complex. exp z * exp (-z) = 1``, 1488 REWRITE_TAC[GSYM COMPLEX_EXP_ADD, COMPLEX_ADD_RINV, COMPLEX_EXP_0]); 1489 1490val COMPLEX_EXP_NEG_MUL2 = store_thm("COMPLEX_EXP_NEG_MUL2", 1491 ``!z:complex. exp (-z) * exp z = 1``, 1492 ONCE_REWRITE_TAC[COMPLEX_MUL_COMM] THEN 1493 MATCH_ACCEPT_TAC COMPLEX_EXP_NEG_MUL); 1494 1495val _ = export_theory() 1496