frequency_equalities.ml

   1 (* ========================================================================= *)\r
   2 (*               Formalization of Electromagnetic Optics                     *)\r
   3 (*                                                                           *)\r
   4 (*            (c) Copyright, Sanaz Khan Afshar & Vincent Aravantinos 2011-13 *)\r
   5 (*                           Hardware Verification Group,                    *)\r
   6 (*                           Concordia University                            *)\r
   7 (*                                                                           *)\r
   8 (*                Contact:   <s_khanaf@encs.concordia.ca>                    *)\r
   9 (*                           <vincent@encs.concordia.ca>                     *)\r
  10 (*                                                                           *)\r
  11 (* Proving that (!x. A*e^(iax)+B*e^(ibx)=C*e^(icx)) ==> a=b=c /\ A+B=C       *)\r
  12 (* Several versions of this result are proved that are useful in proofs.     *)\r
  13 (* ========================================================================= *)\r
  14 \r
  15 \r
  16 \r
  17 (** DERIVATION OF FUNCTIONS WITH REAL ARGUMENTS AND COMPLEX VALUES\r
  18  *\r
  19  * The proof of the lemma requires derivation of functions whose argument is \r
  20  * real but whose value is complex. The theoretical background to do this in\r
  21  * HOL-Light is already present in the library, but the automation is not well\r
  22  * developped. In addition, we need several intermediate results which are\r
  23  * available only for complex derivations or only for general derivation, etc.\r
  24  * Hence we need a bit of work before getting the results we want.\r
  25  *)\r
  26 \r
  27 let REAL_CMUL_TO_VECTOR_MUL = prove\r
  28   (`!a x. a * Cx x = x % a`,\r
  29   REWRITE_TAC[complex_mul;RE_DEF;IM_DEF;CX_DEF;complex;CART_EQ;DIMINDEX_2;\r
  30     FORALL_2;VECTOR_2;VECTOR_MUL_COMPONENT] THEN SIMPLE_COMPLEX_ARITH_TAC);;\r
  31 \r
  32 let LINEAR_REAL_CMUL = prove\r
  33   (`!a. linear (\x. a * Cx (drop x))`,\r
  34   REWRITE_TAC[REAL_CMUL_TO_VECTOR_MUL;linear;drop;VECTOR_ADD_COMPONENT;\r
  35     VECTOR_MUL_COMPONENT]\r
  36   THEN VECTOR_ARITH_TAC);;\r
  37 \r
  38 let HAS_VECTOR_DERIVATIVE_REAL_CMUL = prove\r
  39   (`!a x. ((\x. a * Cx (drop x)) has_vector_derivative a) (at x)`,\r
  40   SIMP_TAC[has_vector_derivative;GSYM REAL_CMUL_TO_VECTOR_MUL;\r
  41     HAS_DERIVATIVE_LINEAR;LINEAR_REAL_CMUL]);;\r
  42 \r
  43 let HAS_COMPLEX_DERIVATIVE_MUL_CEXP = prove\r
  44   (`!a z. ((\z. a * cexp z) has_complex_derivative (a * cexp z)) (at z)`,\r
  45   REPEAT GEN_TAC THEN COMPLEX_DIFF_TAC THEN SIMPLE_COMPLEX_ARITH_TAC);;\r
  46 \r
  47 let HAS_VECTOR_DERIVATIVE_CEXP = prove\r
  48   (`!A a x. ((\x. A * cexp(a * Cx(drop x))) has_vector_derivative (A * a *\r
  49     cexp (a * Cx(drop x)))) (at x)`,\r
  50   REWRITE_TAC[has_vector_derivative; GSYM (REWRITE_CONV[o_DEF] \r
  51     `(\x. A * cexp x) o (\x. a * Cx(drop x))`); GSYM REAL_CMUL_TO_VECTOR_MUL]\r
  52   THEN SUBGOAL_THEN\r
  53     `!A a x. (\x'. (A * a * cexp (a * Cx (drop x))) * Cx (drop x')) = (\x'. A *\r
  54       cexp(a * Cx(drop x)) * x') o (\x. a * Cx(drop x))` (SINGLE REWRITE_TAC)\r
  55   THENL ON_FIRST_GOAL (REWRITE_TAC[o_DEF;FUN_EQ_THM]\r
  56     THEN SIMPLE_COMPLEX_ARITH_TAC)\r
  57   THEN REPEAT GEN_TAC THEN MATCH_MP_TAC DIFF_CHAIN_AT THEN CONJ_TAC \r
  58   THENL [\r
  59     REWRITE_TAC[REAL_CMUL_TO_VECTOR_MUL;GSYM has_vector_derivative]\r
  60     THEN REWRITE_TAC[GSYM REAL_CMUL_TO_VECTOR_MUL;\r
  61       HAS_VECTOR_DERIVATIVE_REAL_CMUL];\r
  62     REWRITE_TAC[] THEN MATCH_ACCEPT_TAC (REWRITE_RULE[has_complex_derivative;\r
  63       GSYM COMPLEX_MUL_ASSOC] HAS_COMPLEX_DERIVATIVE_MUL_CEXP);\r
  64   ]);;\r
  65 \r
  66 let HAS_VECTOR_DERIVATIVE_SUM_CEXP = prove\r
  67   (`!A B a b x. ((\x. A * cexp(a * Cx(drop x)) + B * cexp(b * Cx(drop x)))\r
  68     has_vector_derivative (A * a * cexp (a * Cx(drop x)) + B * b * cexp (b *\r
  69       Cx(drop x)))) (at x)`,\r
  70   REPEAT GEN_TAC THEN MATCH_MP_TAC HAS_VECTOR_DERIVATIVE_ADD THEN CONJ_TAC\r
  71   THEN MATCH_ACCEPT_TAC HAS_VECTOR_DERIVATIVE_CEXP);;\r
  72 \r
  73 \r
  74 (** MAIN RESULT *)\r
  75 \r
  76 let WAVE_SUM_EQ_CORE = prove \r
  77   (`!a b c A B C. ~(A = Cx(&0)) /\ ~(B = Cx(&0)) /\ ~(C = Cx(&0))\r
  78   /\ (!x. A * cexp (a * Cx x) + B * cexp (b * Cx x) = C * cexp (c * Cx x))\r
  79   ==> a = b /\ b = c /\ A + B = C`,\r
  80   REPEAT GEN_TAC THEN STRIP_TAC\r
  81   THEN SUBGOAL_THEN\r
  82     `!x. a * A * cexp (a*Cx x) + b * B * cexp (b*Cx x) = c * C * cexp (c*Cx x)`\r
  83     ASSUME_TAC\r
  84         THENL ON_FIRST_GOAL \r
  85     (REWRITE_TAC[FORALL_DROP] THEN GEN_TAC \r
  86     THEN MATCH_MP_TAC VECTOR_DERIVATIVE_UNIQUE_AT\r
  87     THEN MAP_EVERY EXISTS_TAC [`\x. C * cexp (c * Cx(drop x))`;`x:real^1`]\r
  88     THEN REWRITE_TAC\r
  89       [MESON[COMPLEX_MUL_AC] `!A a. a * A * cexp x = A * a * cexp x`]\r
  90     THEN CONJ_TAC THEN TRY (MATCH_ACCEPT_TAC HAS_VECTOR_DERIVATIVE_CEXP)\r
  91     THEN POP_ASSUM (fun x -> REWRITE_TAC[GSYM x]) \r
  92     THEN MATCH_ACCEPT_TAC HAS_VECTOR_DERIVATIVE_SUM_CEXP)\r
  93   THEN SUBGOAL_THEN `!x. a pow 2 * A * cexp (a*Cx x) + b\r
  94     pow 2 * B * cexp (b*Cx x) = c pow 2 * C * cexp (c*Cx x)` ASSUME_TAC\r
  95   THENL ON_FIRST_GOAL \r
  96     (REWRITE_TAC[FORALL_DROP] THEN GEN_TAC \r
  97     THEN MATCH_MP_TAC VECTOR_DERIVATIVE_UNIQUE_AT\r
  98     THEN MAP_EVERY EXISTS_TAC [`\x.(C * c) * cexp (c * Cx(drop x))`;`x:real^1`]\r
  99     THEN REWRITE_TAC[COMPLEX_POW_2]\r
 100     THEN REWRITE_TAC\r
 101       [MESON[COMPLEX_MUL_AC] `!A a. (a*a) * A * cexp x = (A*a)*a*cexp x`]\r
 102     THEN CONJ_TAC THEN TRY (MATCH_ACCEPT_TAC HAS_VECTOR_DERIVATIVE_CEXP)\r
 103     THEN\r
 104       let assoc_on_cexp =\r
 105         MESON[COMPLEX_MUL_AC] `!C c. (C*c) * cexp x = c*C*cexp x`\r
 106       in\r
 107       REWRITE_TAC[assoc_on_cexp]\r
 108     THEN POP_ASSUM (fun x -> REWRITE_TAC[GSYM x; GSYM assoc_on_cexp])\r
 109     THEN REWRITE_TAC\r
 110       [MESON[COMPLEX_MUL_AC] `!A a. (a*A*a) * cexp x = (A*a)*a*cexp x`]\r
 111     THEN MATCH_ACCEPT_TAC HAS_VECTOR_DERIVATIVE_SUM_CEXP)\r
 112   THEN RULE_ASSUM_TAC (try_or_id (REWRITE_RULE[COMPLEX_MUL_RZERO;\r
 113     COMPLEX_ADD_RID;CEXP_0;COMPLEX_MUL_RID] o SPEC `&0`))\r
 114   THEN SUBGOAL_THEN\r
 115     `(a*A+b*B) pow 2 = a pow 2 * A pow 2 + b pow 2 * B pow 2 + Cx(&2)*a*b*A*B`\r
 116     MP_TAC\r
 117   THENL ON_FIRST_GOAL\r
 118     (REWRITE_TAC[COMPLEX_POW_2] THEN SIMPLE_COMPLEX_ARITH_TAC)\r
 119   THEN SUBGOAL_THEN\r
 120     `(a*A+b*B) pow 2 = a pow 2 * A pow 2 + b pow 2 * B pow 2 + a pow 2 * A *\r
 121       B + b pow 2 * A * B :complex` \r
 122     (SINGLE REWRITE_TAC)\r
 123   THENL ON_FIRST_GOAL \r
 124     (GEN_REWRITE_TAC (RATOR_CONV o ONCE_DEPTH_CONV) [COMPLEX_POW_2]\r
 125     THEN ASM\r
 126       (GEN_REWRITE_TAC (RATOR_CONV o RAND_CONV o RATOR_CONV o DEPTH_CONV)) []\r
 127     THEN FIND_ASSUM (SINGLE REWRITE_TAC o GSYM) `A+B=C:complex`\r
 128     THEN FIND_ASSUM (SINGLE REWRITE_TAC) `a * A + b * B = c * C:complex`\r
 129     THEN SUBGOAL_TAC "" `(c * (A + B)) * c * C = (A+B) * c pow 2 * C:complex`\r
 130       [REWRITE_TAC[COMPLEX_POW_2] THEN SIMPLE_COMPLEX_ARITH_TAC]\r
 131     THEN POP_ASSUM (SINGLE REWRITE_TAC)\r
 132     THEN FIND_ASSUM (SINGLE REWRITE_TAC o GSYM)\r
 133       (`a pow 2 * A + b pow 2 * B = c pow 2 * C:complex`)\r
 134     THEN REWRITE_TAC[COMPLEX_POW_2] THEN SIMPLE_COMPLEX_ARITH_TAC)\r
 135   THEN REWRITE_TAC[COMPLEX_EQ_ADD_LCANCEL]\r
 136   THEN SUBGOAL_THEN `a pow 2 * A * B + b pow 2 * A * B = Cx (&2) * a * b * A *\r
 137     B <=> (a-b) pow 2 * A * B = Cx(&0)` (SINGLE REWRITE_TAC)\r
 138   THENL ON_FIRST_GOAL\r
 139     (REWRITE_TAC[COMPLEX_POW_2] THEN SIMPLE_COMPLEX_ARITH_TAC)\r
 140   THEN REWRITE_TAC[COMPLEX_ENTIRE]\r
 141   THEN RULE_ASSUM_TAC (SINGLE PURE_REWRITE_RULE (TAUT `~p <=> (p<=>F)`))\r
 142   THEN ASM_REWRITE_TAC[COMPLEX_POW_2;COMPLEX_ENTIRE;COMPLEX_SUB_0]\r
 143   THEN DISCH_THEN (fun x -> REWRITE_ASSUMPTIONS[x;GSYM COMPLEX_ADD_LDISTRIB]\r
 144     THEN REWRITE_TAC[x])\r
 145   THEN POP_ASSUM (K ALL_TAC) THEN POP_ASSUM MP_TAC\r
 146   THEN ASM_REWRITE_TAC[COMPLEX_EQ_MUL_RCANCEL]);;\r
 147 \r
 148 \r
 149 (** WEAKER RESULTS\r
 150  * - with only two exponentials (WAVE_SUM_EQ_SINGLE)\r
 151  * - with B possibly equal to zero (WAVE_SUM_EQ_WEAK1)\r
 152  * - with C possibly equal to zero (WAVE_SUM_EQ_WEAK2)\r
 153  *)\r
 154 let WAVE_SUM_EQ_SINGLE = prove \r
 155   (`!a b A B.\r
 156     ~(A = Cx(&0)) /\ (!x. A * cexp (a * Cx x) = B * cexp (b * Cx x))\r
 157     ==> a = b /\ A = B`,\r
 158   REPEAT GEN_TAC THEN STRIP_TAC THEN SUBGOAL_THEN `~(B = Cx(&0))` ASSUME_TAC\r
 159   THENL ON_FIRST_GOAL (POP_ASSUM (fun x -> ASM_REWRITE_TAC[REWRITE_RULE\r
 160     [COMPLEX_MUL_RZERO;CEXP_0;COMPLEX_MUL_RID] (SPEC `&0` (GSYM x))]))\r
 161   THEN SUBGOAL_THEN\r
 162     `!x. A * cexp (a * Cx x) + A * cexp (a * Cx x) \r
 163       = (Cx(&2)*B) * cexp (b * Cx x)` \r
 164     ASSUME_TAC\r
 165   THENL ON_FIRST_GOAL (GEN_TAC THEN POP_ASSUM (K ALL_TAC)\r
 166     THEN POP_ASSUM (MP_TAC o SPEC_ALL) THEN SIMPLE_COMPLEX_ARITH_TAC)\r
 167   THEN SUBGOAL_THEN `~(Cx(&2)*B=Cx(&0))` ASSUME_TAC \r
 168   THENL ON_FIRST_GOAL\r
 169     (POP_ASSUM (K ALL_TAC) THEN POP_ASSUM MP_TAC THEN SIMPLE_COMPLEX_ARITH_TAC)\r
 170   THEN ASM_MESON_TAC\r
 171     [WAVE_SUM_EQ_CORE;SIMPLE_COMPLEX_ARITH `A + A = Cx(&2) * B <=> A = B`]);;\r
 172 \r
 173 let WAVE_SUM_EQ_WEAK1 = prove \r
 174   (`!a b c A B C.\r
 175     ~(A = Cx(&0)) /\ ~(C = Cx(&0))\r
 176     /\ (!x. A * cexp (a * Cx x) + B * cexp (b * Cx x) = C * cexp (c * Cx x)) \r
 177     ==> a = c /\ A + B = C`,\r
 178   REPEAT GEN_TAC THEN ASM_CASES_TAC `B = Cx(&0)` THENL [\r
 179     ASM_REWRITE_TAC[COMPLEX_MUL_LZERO;COMPLEX_ADD_RID]\r
 180     THEN MESON_TAC[WAVE_SUM_EQ_SINGLE];\r
 181     REPEAT STRIP_TAC\r
 182     THENL ON_FIRST_GOAL (MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `b:complex`)\r
 183     THEN ASM_MESON_TAC[WAVE_SUM_EQ_CORE];\r
 184   ]);;\r
 185 \r
 186 let WAVE_SUM_EQ_WEAK2 = prove \r
 187   (`!a b c A B C.\r
 188     ~(A = Cx(&0)) /\ ~(B = Cx(&0)) \r
 189     /\ (!x. A * cexp (a * Cx x) + B * cexp (b * Cx x) = C * cexp (c * Cx x)) \r
 190     ==> a = b /\ A + B = C`,\r
 191   REPEAT GEN_TAC THEN ASM_CASES_TAC `C = Cx(&0)` THENL [\r
 192     ASM_REWRITE_TAC[COMPLEX_MUL_LZERO;COMPLEX_LNEG_UNIQ;COMPLEX_NEG_LMUL]\r
 193     THEN MESON_TAC[WAVE_SUM_EQ_SINGLE;COMPLEX_NEG_EQ_0];\r
 194     ASM_MESON_TAC[WAVE_SUM_EQ_CORE];\r
 195   ]);;\r
 196 \r
 197 \r
 198 (** VECTORIAL VERSIONS OF THE ABOVE THEOREMS **)\r
 199 let VEC_WAVE_SUM_EQ_CORE = prove\r
 200   (`!a b c A B C:complex^N.\r
 201     ~(A = cvector_zero) /\ ~(B = cvector_zero) /\ ~(C = cvector_zero)\r
 202     /\ (!x. cexp (a * Cx x) % A + cexp (b * Cx x) % B = cexp (c * Cx x) % C)\r
 203     ==> a = b /\ b = c /\ A + B = C`,\r
 204   REWRITE_TAC[CVECTOR_NON_ZERO;IMP_CONJ;\r
 205     MESON[] `(a ==> b/\c/\d) <=> (a==>b/\c) /\ (b/\c==>a==>d)`]\r
 206   THEN REPEAT GEN_TAC \r
 207   THEN MAP_EVERY (DISCH_THEN o X_CHOOSE_TAC) [`i:num`;`j:num`;`k:num`]\r
 208   THEN CONJ_TAC\r
 209   THENL ON_FIRST_GOAL (MAP_EVERY ASM_CASES_TAC [`i=(j:num)`;`j=(k:num)`])\r
 210   THENL\r
 211     let cexp_SYM = SIMPLE_COMPLEX_ARITH `cexp x * y = y * cexp x` in\r
 212     let PROJECT_ON t =\r
 213       MAP_ANTECEDENT (SPEC t o ONCE_REWRITE_RULE[SWAP_FORALL_THM] o\r
 214         ONCE_REWRITE_RULE[CART_EQ])\r
 215       THEN ASM_REWRITE_TAC[CVECTOR_MUL_COMPONENT;CVECTOR_ADD_COMPONENT;cexp_SYM]\r
 216     in\r
 217     let CONJ1_FIRST = MESON[] `(a ==> b/\c) <=> ((a==>b)/\(b==>a==>c))` in\r
 218     [\r
 219       PROJECT_ON `i:num` THEN ASM_MESON_TAC[WAVE_SUM_EQ_CORE];\r
 220       REWRITE_TAC[CONJ1_FIRST] THEN CONJ_TAC\r
 221       THENL [\r
 222         PROJECT_ON `i:num` THEN ASM_MESON_TAC[WAVE_SUM_EQ_WEAK2];\r
 223         DISCH_THEN (fun x -> REWRITE_TAC[x;GSYM CVECTOR_ADD_LDISTRIB])\r
 224         THEN PROJECT_ON `k:num` THEN ASM_MESON_TAC[WAVE_SUM_EQ_SINGLE];\r
 225       ];\r
 226       REWRITE_TAC[MESON[] `(a ==> b/\c) <=> ((a==>c)/\(c==>a==>b))`]\r
 227       THEN CONJ_TAC\r
 228       THENL [\r
 229         PROJECT_ON `j:num` THEN ONCE_REWRITE_TAC[COMPLEX_ADD_SYM]\r
 230         THEN ASM_MESON_TAC[WAVE_SUM_EQ_WEAK1];\r
 231         DISCH_THEN (fun x -> \r
 232           REWRITE_TAC[x;CVECTOR_ARITH `!x:complex^N. x +y=z <=> x=z-y`;\r
 233           GSYM CVECTOR_SUB_LDISTRIB])\r
 234         THEN PROJECT_ON `i:num` THEN ASM_MESON_TAC[WAVE_SUM_EQ_SINGLE];\r
 235       ];\r
 236       ASM_CASES_TAC `(C:complex^N)$i = Cx(&0)`\r
 237       THENL [\r
 238         REWRITE_TAC[CONJ1_FIRST] THEN CONJ_TAC\r
 239         THENL [\r
 240           PROJECT_ON `i:num`\r
 241           THEN REWRITE_TAC[COMPLEX_MUL_LZERO;COMPLEX_LNEG_UNIQ;\r
 242             COMPLEX_NEG_LMUL]\r
 243           THEN ASM_MESON_TAC[WAVE_SUM_EQ_SINGLE];\r
 244           DISCH_THEN (fun x -> REWRITE_TAC[x;GSYM CVECTOR_ADD_LDISTRIB])\r
 245           THEN PROJECT_ON `k:num` THEN ASM_MESON_TAC[WAVE_SUM_EQ_SINGLE];\r
 246         ];\r
 247         ONCE_REWRITE_TAC[MESON[] `a=b/\b=c <=> a=c /\ (a=b/\b=c)`]\r
 248         THEN REWRITE_TAC\r
 249           [MESON[] `(a==>b/\c/\d) <=> (a==>b) /\ (b==>a==>c/\d)`]\r
 250         THEN CONJ_TAC\r
 251         THENL [\r
 252           PROJECT_ON `i:num` THEN ASM_MESON_TAC[WAVE_SUM_EQ_WEAK1];\r
 253           DISCH_THEN (fun x ->\r
 254             REWRITE_TAC[x;CVECTOR_ARITH `!x:complex^N. x +y=z <=> y=z-x`;\r
 255               GSYM CVECTOR_SUB_LDISTRIB])\r
 256           THEN PROJECT_ON `j:num` THEN ASM_MESON_TAC[WAVE_SUM_EQ_SINGLE]\r
 257         ];\r
 258       ];\r
 259       REPLICATE_TAC 2 (DISCH_THEN (SINGLE REWRITE_TAC))\r
 260       THEN REWRITE_TAC\r
 261         [CVECTOR_ARITH `x % X + x % Y = x % Z <=> x % (X+Y-Z) = cvector_zero`;\r
 262           CVECTOR_MUL_EQ_0;CEXP_NZ]\r
 263       THEN CVECTOR_ARITH_TAC\r
 264     ]);;\r
 265 \r
 266 let VEC_WAVE_SUM_EQ_SINGLE = prove \r
 267   (`!a b A B:complex^N.\r
 268     ~(A = cvector_zero) /\ (!x. cexp (a * Cx x) % A = cexp (b * Cx x) % B) \r
 269     ==> a = b /\ A = B`,\r
 270   REPEAT GEN_TAC THEN STRIP_TAC\r
 271   THEN SUBGOAL_THEN `~(B:complex^N = cvector_zero)` ASSUME_TAC\r
 272   THENL ON_FIRST_GOAL (POP_ASSUM (fun x -> ASM_REWRITE_TAC[\r
 273     REWRITE_RULE[COMPLEX_MUL_RZERO;CEXP_0;CVECTOR_MUL_ID]\r
 274       (SPEC `&0` (GSYM x))]))\r
 275   THEN SUBGOAL_THEN\r
 276     `!x. cexp (a * Cx x) % (A:complex^N) + cexp (a * Cx x) % A\r
 277       = cexp (b * Cx x) % (Cx(&2) % B)` \r
 278     ASSUME_TAC\r
 279   THENL ON_FIRST_GOAL (GEN_TAC THEN POP_ASSUM (K ALL_TAC)\r
 280     THEN POP_ASSUM (MP_TAC o SPEC_ALL) THEN CVECTOR_ARITH_TAC)\r
 281   THEN SUBGOAL_THEN `~(Cx(&2) % (B:complex^N) = cvector_zero)` ASSUME_TAC\r
 282   THENL ON_FIRST_GOAL (POP_ASSUM (K ALL_TAC) THEN POP_ASSUM MP_TAC\r
 283   THEN REWRITE_TAC[CVECTOR_MUL_EQ_0;SIMPLE_COMPLEX_ARITH `~(Cx(&2) = Cx(&0))`])\r
 284   THEN ASM_MESON_TAC\r
 285     [VEC_WAVE_SUM_EQ_CORE;CVECTOR_ARITH `A + A = Cx(&2) % B <=> A = B`]);;\r
 286 \r
 287 let VEC_WAVE_SUM_EQ_WEAK1 = prove \r
 288   (`!a b c A B C:complex^N.\r
 289     ~(A = cvector_zero) /\ ~(C = cvector_zero)\r
 290     /\ (!x. cexp (a * Cx x) % A + cexp (b * Cx x) % B = cexp (c * Cx x) % C) \r
 291     ==> a = c /\ A + B = C`,\r
 292   REPEAT GEN_TAC THEN ASM_CASES_TAC `(B:complex^N) = cvector_zero` THENL [\r
 293     ASM_REWRITE_TAC[CVECTOR_MUL_RZERO;CVECTOR_ADD_ID]\r
 294     THEN MESON_TAC[VEC_WAVE_SUM_EQ_SINGLE];\r
 295     REPEAT STRIP_TAC\r
 296     THENL ON_FIRST_GOAL (MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `b:complex`)\r
 297     THEN ASM_MESON_TAC[VEC_WAVE_SUM_EQ_CORE];\r
 298   ]);;\r
 299 \r
 300 let VEC_WAVE_SUM_EQ_WEAK2 = prove \r
 301   (`!a b c A B C:complex^N.\r
 302     ~(A = cvector_zero) /\ ~(B = cvector_zero)\r
 303     /\ (!x. cexp (a * Cx x) % A + cexp (b * Cx x) % B = cexp (c * Cx x) % C) \r
 304     ==> a = b /\ A + B = C`,\r
 305   REPEAT GEN_TAC THEN ASM_CASES_TAC `(C:complex^N) = cvector_zero` \r
 306   THENL [\r
 307     ASM_REWRITE_TAC[CVECTOR_MUL_RZERO;\r
 308       CVECTOR_ARITH `x+y = cvector_zero <=> x= --y`;GSYM CVECTOR_MUL_RNEG]\r
 309     THEN MESON_TAC[VEC_WAVE_SUM_EQ_SINGLE];\r
 310     ASM_MESON_TAC[VEC_WAVE_SUM_EQ_CORE];\r
 311   ]);;\r