src/real/complexScript.sml

946 val conj = new_definition
947      ("conj", ``conj (z:complex) = (RE z, -IM z)``);
950   ``!x:real. conj (complex_of_real x) = complex_of_real x``,
951   REWRITE_TAC[complex_of_real,conj, RE,IM, REAL_NEG_0]);
954   ``!n:num. conj (complex_of_num n) = complex_of_num n``,
958   ``!z:complex w:complex. conj (z + w) = conj z + conj w``,
959   REWRITE_TAC [conj,complex_add,RE,IM,REAL_NEG_ADD]);
962   ``!z:complex. conj (-z) = -conj z ``,
963   REWRITE_TAC [complex_neg, conj,RE,IM]);
966   ``!z:complex w:complex. conj (z - w) = conj z - conj w``,
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,
975   ``!z: complex. conj (inv z) = inv (conj z)``,
976   RW_TAC real_ss [conj, complex_inv, RE, IM, POW_2, real_div]);
979   ``!z:complex w. conj (z / w) = conj z / conj w``,
983   ``!k:real z:complex. conj (k * z) = k * conj z``,
984   REWRITE_TAC [conj,complex_scalar_lmul, RE,IM,REAL_MUL_RNEG]);
987   ``!z:complex. conj (conj z) = z``,
988   REWRITE_TAC[conj, RE,IM,REAL_NEGNEG]);
991   ``!z:complex w:complex. (conj z = w) = (z = conj w)``,
992   REWRITE_TAC [conj, COMPLEX_RE_IM_EQ, RE, IM, REAL_NEG_EQ]);
995   ``!z:complex w:complex. (conj z = conj w) = (z = w)``,
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,
1007          conj z * z = complex_of_real ((RE z) pow 2 + (IM z) pow 2)``,
1011   ``conj 0 = 0``,
1047   ``!z:complex. z * conj z = complex_of_real ((modu z) pow 2)``,
1051   ``!z:complex. conj z * z = complex_of_real ((modu z) pow 2)``,
1065   ``!z:complex. modu (conj z) = modu z ``,
1066   REWRITE_TAC[modu, conj,RE,IM,POW_2,REAL_NEG_MUL2]);