cvectors.ml

   1 (* Upadted for the latest version of HOL Light (JULY 2014) *)
   2
   3 (* ========================================================================= *)\r
   4 (* A library for vectors of complex numbers.                                 *)\r
   5 (* Much inspired from HOL-Light real vector library <"vectors.ml">.          *)\r
   6 (*                                                                           *)\r
   7 (*            (c) Copyright, Sanaz Khan Afshar & Vincent Aravantinos 2011-13 *)\r
   8 (*                           Hardware Verification Group,                    *)\r
   9 (*                           Concordia University                            *)\r
  10 (*                                                                           *)\r
  11 (*                Contact:   <s_khanaf@encs.concordia.ca>                    *)\r
  12 (*                           <vincent@encs.concordia.ca>                     *)\r
  13 (*                                                                           *)\r
  14 (* Acknowledgements:                                                         *)\r
  15 (* - Harsh Singhal: n-dimensional dot product, utility theorems              *)\r
  16 (*                                                                           *)\r
  17 (* Last update: July 2013                                                    *)\r
  18 (*                                                                           *)\r
  19 (* ========================================================================= *)\r
  20 \r
  21 \r
  22 (* ========================================================================= *)\r
  23 (* ADDITIONS TO THE BASE LIBRARY                                             *)\r
  24 (* ========================================================================= *)\r
  25 \r
  26   (* ----------------------------------------------------------------------- *)\r
  27   (* Additional tacticals                                                    *)\r
  28   (* ----------------------------------------------------------------------- *)\r
  29 \r
  30 \r
  31 let SINGLE f x = f [x];;\r
  32 \r
  33 let distrib fs x = map (fun f -> f x) fs;;\r
  34 \r
  35 let DISTRIB ttacs x = EVERY (distrib ttacs x);;\r
  36 \r
  37 let REWRITE_TACS = MAP_EVERY (SINGLE REWRITE_TAC);;\r
  38 \r
  39 let GCONJUNCTS thm = map GEN_ALL (CONJUNCTS (SPEC_ALL thm));;\r
  40 \r
  41   (* ----------------------------------------------------------------------- *)\r
  42   (* Additions to the vectors library                                        *)\r
  43   (* ----------------------------------------------------------------------- *)\r
  44 \r
  45 let COMPONENT_LE_NORM_ALT = prove\r
  46   (`!x:real^N i. 1 <= i /\ i <= dimindex (:N) ==> x$i <= norm x`,\r
  47   MESON_TAC [REAL_ABS_LE;COMPONENT_LE_NORM;REAL_LE_TRANS]);;\r
  48 \r
  49   (* ----------------------------------------------------------------------- *)\r
  50   (* Additions to the library of complex numbers                             *)\r
  51   (* ----------------------------------------------------------------------- *)\r
  52 \r
  53 (* Lemmas *)\r
  54 let RE_IM_NORM = prove\r
  55   (`!x. Re x <= norm x /\ Im x <= norm x /\ abs(Re x) <= norm x\r
  56   /\ abs(Im x) <= norm x`,\r
  57   REWRITE_TAC[RE_DEF;IM_DEF] THEN GEN_TAC THEN REPEAT CONJ_TAC\r
  58   THEN ((MATCH_MP_TAC COMPONENT_LE_NORM_ALT\r
  59   THEN REWRITE_TAC[DIMINDEX_2] THEN ARITH_TAC) ORELSE SIMP_TAC [COMPONENT_LE_NORM]));;\r
  60 \r
  61 let [RE_NORM;IM_NORM;ABS_RE_NORM;ABS_IM_NORM] = GCONJUNCTS RE_IM_NORM;;\r
  62 \r
  63 let NORM_RE = prove\r
  64   (`!x. &0 <= norm x + Re x /\ &0 <= norm x - Re x`, \r
  65   GEN_TAC THEN MP_TAC (SPEC_ALL ABS_RE_NORM) THEN REAL_ARITH_TAC);;\r
  66 \r
  67 let [NORM_RE_ADD;NORM_RE_SUB] = GCONJUNCTS NORM_RE;;\r
  68 \r
  69 let NORM2_ADD_REAL = prove\r
  70   (`!x y.\r
  71     real x /\ real y ==> norm (x + ii * y) pow 2 = norm x pow 2 + norm y pow 2`,\r
  72   SIMP_TAC[real;complex_norm;RE_ADD;IM_ADD;RE_MUL_II;IM_MUL_II;REAL_NEG_0;\r
  73     REAL_ADD_LID;REAL_ADD_RID;REAL_POW_ZERO;ARITH_RULE `~(2=0)`;REAL_LE_POW_2;\r
  74     SQRT_POW_2;REAL_LE_ADD]);;\r
  75 \r
  76 let COMPLEX_EQ_RCANCEL_IMP = GEN_ALL (MATCH_MP (MESON []\r
  77   `(p <=> r \/ q) ==> (p /\ ~r ==> q) `) (SPEC_ALL COMPLEX_EQ_MUL_RCANCEL));;\r
  78 \r
  79 let COMPLEX_BALANCE_DIV_MUL = prove\r
  80   (`!x y z t. ~(z=Cx(&0)) ==> (x = y/z * t <=> x*z = y * t)`,\r
  81   REPEAT STRIP_TAC THEN POP_ASSUM (fun x ->\r
  82     ASSUME_TAC (REWRITE_RULE[x] (SPEC_ALL COMPLEX_EQ_MUL_RCANCEL))\r
  83     THEN ASSUME_TAC (REWRITE_RULE[x] (SPECL [`x:complex`;`z:complex`]\r
  84     COMPLEX_DIV_RMUL)))\r
  85   THEN SUBGOAL_THEN `x=y/z*t <=> x*z=(y/z*t)*z:complex` (SINGLE REWRITE_TAC)\r
  86   THENL [ASM_REWRITE_TAC[];\r
  87     REWRITE_TAC[SIMPLE_COMPLEX_ARITH `(y/z*t)*z=(y/z*z)*t:complex`]\r
  88   THEN ASM_REWRITE_TAC[]]);;\r
  89 \r
  90 let CSQRT_MUL_LCX_LT = prove\r
  91   (`!x y. &0 < x ==> csqrt(Cx x * y) = Cx(sqrt x) * csqrt y`,\r
  92   REWRITE_TAC[csqrt;complex_mul;IM;RE;IM_CX;REAL_MUL_LZERO;REAL_ADD_RID;RE_CX;\r
  93     REAL_SUB_RZERO]\r
  94   THEN REPEAT STRIP_TAC THEN REPEAT COND_CASES_TAC\r
  95   THEN FIRST_ASSUM (ASSUME_TAC o MATCH_MP REAL_LT_IMP_LE)\r
  96   THEN ASM_SIMP_TAC[IM;RE;REAL_MUL_RZERO;SQRT_MUL]\r
  97   THENL [\r
  98     REPEAT (POP_ASSUM MP_TAC) THEN REWRITE_TAC[REAL_ENTIRE;REAL_MUL_POS_LE]\r
  99     THEN REPEAT STRIP_TAC\r
 100     THEN ASM_REWRITE_TAC[SQRT_0;REAL_MUL_LZERO;REAL_MUL_RZERO];\r
 101     REPEAT (POP_ASSUM MP_TAC) THEN SIMP_TAC [REAL_ENTIRE]\r
 102     THEN MESON_TAC [REAL_LT_IMP_NZ];\r
 103     ASM_MESON_TAC [REAL_LE_MUL_EQ;REAL_ARITH `~(&0 <= y) = &0 > y`];\r
 104     SIMP_TAC [REAL_NEG_RMUL] THEN REPEAT (POP_ASSUM MP_TAC)\r
 105     THEN SIMP_TAC [REAL_ARITH `~(&0 <= y) = y < &0`]\r
 106     THEN SIMP_TAC [GSYM REAL_NEG_GT0] THEN MESON_TAC[REAL_LT_IMP_LE;SQRT_MUL];\r
 107     REPEAT (POP_ASSUM MP_TAC) THEN SIMP_TAC [REAL_ENTIRE]\r
 108     THEN MESON_TAC [REAL_LT_IMP_NZ];\r
 109     REPEAT (POP_ASSUM MP_TAC) THEN SIMP_TAC [REAL_ENTIRE]\r
 110     THEN SIMP_TAC [DE_MORGAN_THM];\r
 111     REPEAT (POP_ASSUM MP_TAC) THEN SIMP_TAC [REAL_ENTIRE]\r
 112     THEN SIMP_TAC [DE_MORGAN_THM]; ALL_TAC] THENL [\r
 113       SIMP_TAC [REAL_NEG_0;SQRT_0;REAL_MUL_RZERO];\r
 114       ASM_MESON_TAC[REAL_ARITH `~(x<y /\ ~(x <=y))`];\r
 115       ASM_MESON_TAC[REAL_ARITH `~(x<y /\ y<x)`];\r
 116       ALL_TAC]\r
 117     THEN REWRITE_TAC[GSYM (REWRITE_RULE[CX_DEF;complex_mul;RE;IM;\r
 118       REAL_MUL_LZERO;REAL_ADD_RID;REAL_SUB_RZERO] COMPLEX_CMUL)]\r
 119     THEN SIMP_TAC [NORM_MUL] THEN POP_ASSUM MP_TAC\r
 120     THEN ASM_SIMP_TAC [GSYM REAL_ABS_REFL] THEN DISCH_TAC\r
 121     THEN SIMP_TAC [REAL_ABS_MUL]\r
 122     THEN ASM_SIMP_TAC [GSYM REAL_ABS_REFL]\r
 123     THEN SIMP_TAC [GSYM REAL_ADD_LDISTRIB; GSYM REAL_SUB_LDISTRIB]\r
 124     THEN SUBGOAL_THEN `(x*Im y) / (x*abs(Im y)) = Im y / abs(Im y)` ASSUME_TAC\r
 125     THENL [\r
 126       SIMP_TAC [real_div] THEN SIMP_TAC [REAL_INV_MUL]\r
 127       THEN SIMP_TAC [GSYM REAL_MUL_ASSOC] THEN ONCE_REWRITE_TAC[REAL_MUL_AC]\r
 128       THEN SUBGOAL_THEN `Im y * x * inv x * inv (abs(Im y)) =\r
 129         Im y * (x * inv x) * inv (abs (Im y)) ` ASSUME_TAC\r
 130         THENL [SIMP_TAC [REAL_MUL_AC]; ALL_TAC]\r
 131       THEN ASM_SIMP_TAC[REAL_MUL_RINV;REAL_LT_IMP_NZ]\r
 132       THEN SIMP_TAC [REAL_MUL_LID] THEN SIMP_TAC [REAL_MUL_AC];\r
 133       ALL_TAC]\r
 134     THEN ASM_SIMP_TAC[]\r
 135     THEN SUBGOAL_THEN `sqrt x * Im y / abs(Im y) * sqrt ((norm y-Re y) / &2) =\r
 136       Im y / abs (Im y) * sqrt x * sqrt ((norm y - Re y) / &2)` ASSUME_TAC\r
 137     THENL [SIMP_TAC [REAL_MUL_AC]; ALL_TAC] THEN ASM_SIMP_TAC[]\r
 138     THEN SUBGOAL_THEN `sqrt ((x * (norm y - Re y)) / &2) =\r
 139       sqrt (x * (norm y - Re y)) / sqrt (&2)` ASSUME_TAC\r
 140     THENL [\r
 141       SIMP_TAC[SQRT_DIV] THEN CONJ_TAC THENL [\r
 142         ASM_SIMP_TAC[REAL_LE_MUL_EQ;REAL_LT_IMP_LE] THEN SIMP_TAC[NORM_RE_SUB];\r
 143         REAL_ARITH_TAC];\r
 144       ALL_TAC]\r
 145     THEN ASM_SIMP_TAC[] THEN SUBGOAL_THEN `sqrt ((norm y - Re y) / &2) =\r
 146       sqrt (norm y - Re y) / sqrt (&2)` ASSUME_TAC\r
 147     THENL [\r
 148       SIMP_TAC[SQRT_DIV] THEN CONJ_TAC\r
 149       THENL [SIMP_TAC [NORM_RE_SUB]; REAL_ARITH_TAC];\r
 150       ALL_TAC ]\r
 151     THEN ASM_SIMP_TAC[]\r
 152     THEN SUBGOAL_THEN `sqrt ((x * (norm y + Re y)) / &2) =\r
 153       sqrt (x * (norm y + Re y)) / sqrt (&2)` ASSUME_TAC\r
 154     THENL [\r
 155       SIMP_TAC[SQRT_DIV] THEN CONJ_TAC\r
 156       THENL [\r
 157         ASM_SIMP_TAC [REAL_LE_MUL_EQ;REAL_LT_IMP_LE]\r
 158         THEN SIMP_TAC[NORM_RE_ADD];\r
 159         REAL_ARITH_TAC];\r
 160       ALL_TAC]\r
 161     THEN SUBGOAL_THEN `sqrt ((norm y + Re y) / &2) =\r
 162       sqrt (norm y + Re y) / sqrt (&2)` ASSUME_TAC\r
 163     THENL [\r
 164       SIMP_TAC[SQRT_DIV] THEN CONJ_TAC\r
 165       THENL [SIMP_TAC[NORM_RE_ADD]; REAL_ARITH_TAC];\r
 166       ALL_TAC]\r
 167     THEN ASM_SIMP_TAC[] THEN SUBGOAL_THEN `&0 <= x` ASSUME_TAC\r
 168     THENL [ ASM_SIMP_TAC [REAL_LT_IMP_LE]; ALL_TAC ]\r
 169     THEN SIMP_TAC[COMPLEX_EQ] THEN SIMP_TAC[RE;IM] THEN CONJ_TAC\r
 170     THENL [\r
 171       SUBGOAL_THEN `sqrt x * sqrt (norm y + Re y) / sqrt (&2) =\r
 172         (sqrt x * sqrt (norm y + Re y)) / sqrt (&2)` ASSUME_TAC\r
 173       THENL [REAL_ARITH_TAC; ALL_TAC]\r
 174       THEN ASM_MESON_TAC [SQRT_MUL;NORM_RE_ADD];\r
 175       SUBGOAL_THEN `Im y/abs(Im y) * sqrt x * sqrt (norm y-Re y) / sqrt(&2) =\r
 176         Im y/abs (Im y) * (sqrt x * sqrt (norm y - Re y))/sqrt(&2)` ASSUME_TAC\r
 177       THENL [REAL_ARITH_TAC; ALL_TAC]\r
 178       THEN ASM_MESON_TAC[SQRT_MUL;NORM_RE_SUB]]);;\r
 179 \r
 180 let CSQRT_MUL_LCX = prove\r
 181   (`!x y. &0 <= x ==> csqrt(Cx x * y) = Cx(sqrt x) * csqrt y`,\r
 182   REWRITE_TAC[REAL_LE_LT] THEN REPEAT STRIP_TAC\r
 183   THEN ASM_SIMP_TAC[CSQRT_MUL_LCX_LT] THEN EXPAND_TAC "x"\r
 184   THEN REWRITE_TAC[COMPLEX_MUL_LZERO;SQRT_0;CSQRT_0]);;\r
 185 \r
 186 let REAL_ADD_POW_2 = prove\r
 187   (`!x y:real. (x+y) pow 2 = x pow 2 + y pow 2 + &2 * x * y`,\r
 188   REAL_ARITH_TAC);;\r
 189 \r
 190 let COMPLEX_ADD_POW_2 = prove\r
 191   (`!x y:complex. (x+y) pow 2 = x pow 2 + y pow 2 + Cx(&2) * x * y`,\r
 192   REWRITE_TAC[COMPLEX_POW_2] THEN SIMPLE_COMPLEX_ARITH_TAC);;\r
 193
 194
 195 \r
 196 (* ----------------------------------------------------------------------- *)\r
 197 (* Additions to the topology library                                       *)\r
 198 (* ----------------------------------------------------------------------- *)\r
 199
 200  prioritize_vector ();;
 201 \r
 202 (* Lemmas *)\r
 203 let FINITE_INTER_ENUM = prove\r
 204   (`!s n. FINITE(s INTER (0..n))`,\r
 205   MESON_TAC[FINITE_INTER;FINITE_NUMSEG]);;\r
 206 \r
 207 let NORM_PASTECART_GE1 = prove\r
 208   (`!x y. norm x <= norm (pastecart x y)`,\r
 209   MESON_TAC[FSTCART_PASTECART;NORM_FSTCART]);;\r
 210 \r
 211 let NORM_PASTECART_GE2 = prove\r
 212   (`!x y. norm y <= norm (pastecart x y)`,\r
 213   MESON_TAC[SNDCART_PASTECART;NORM_SNDCART]);;\r
 214 \r
 215 let LIM_PASTECART_EQ = prove\r
 216   (`!net a b f:A->real^M g:A->real^N. (f --> a) net /\ (g --> b) net\r
 217     <=> ((\x. pastecart (f x) (g x)) --> pastecart a b) net`,\r
 218   REWRITE_TAC[MESON[] `(a <=> b) <=> (a ==> b) /\ (b ==> a)`;LIM_PASTECART;LIM;\r
 219     MESON[]`(p\/q ==> (p \/ r) /\ (p \/ s)) <=> (~p /\ q ==> r /\ s)`;dist;\r
 220     PASTECART_SUB] \r
 221   THEN ASM_MESON_TAC[REAL_LET_TRANS;NORM_PASTECART_GE1;NORM_PASTECART_GE2]);;\r
 222 \r
 223 let SUMS_PASTECART = prove\r
 224   (`!s f1:num->real^N f2:num->real^M l1 l2. (f1 sums l1) s /\ (f2 sums l2) s\r
 225     <=> ((\x. pastecart (f1 x) (f2 x)) sums (pastecart l1 l2)) s`,\r
 226   SIMP_TAC[sums;FINITE_INTER_ENUM;GSYM PASTECART_VSUM;LIM_PASTECART_EQ]);;\r
 227 \r
 228 let LINEAR_SUMS = prove(\r
 229   `!s f l g. linear g ==> ((f sums l) s ==> ((g o f) sums (g l)) s)`,\r
 230   SIMP_TAC[sums;FINITE_INTER_ENUM;GSYM LINEAR_VSUM;\r
 231     REWRITE_RULE[o_DEF;CONTINUOUS_AT_SEQUENTIALLY] LINEAR_CONTINUOUS_AT]);; \r
 232 \r
 233   (* ----------------------------------------------------------------------- *)\r
 234   (* Embedding of reals in complex numbers                                   *)\r
 235   (* ----------------------------------------------------------------------- *)\r
 236 \r
 237 let real_of_complex = new_definition `real_of_complex c = @r. c = Cx r`;;\r
 238 \r
 239 let REAL_OF_COMPLEX = prove\r
 240   (`!c. real c ==> Cx(real_of_complex c) = c`,\r
 241   MESON_TAC[REAL;real_of_complex]);;\r
 242 \r
 243 let REAL_OF_COMPLEX_RE = prove\r
 244   (`!c. real c ==> real_of_complex c = Re c`,\r
 245   MESON_TAC[RE_CX;REAL_OF_COMPLEX]);;\r
 246 \r
 247 let REAL_OF_COMPLEX_CX = prove\r
 248   (`!r. real_of_complex (Cx r) = r`,\r
 249   SIMP_TAC[REAL_CX;REAL_OF_COMPLEX_RE;RE_CX]);;\r
 250 \r
 251 let REAL_OF_COMPLEX_NORM = prove\r
 252   (`!c. real c ==> norm c = abs (real_of_complex c)`,\r
 253   MESON_TAC[REAL_NORM;REAL_OF_COMPLEX_RE]);;\r
 254 \r
 255 let REAL_OF_COMPLEX_ADD = prove\r
 256   (`!x y. real x /\ real y\r
 257     ==> real_of_complex (x+y) = real_of_complex x + real_of_complex y`,\r
 258   MESON_TAC[REAL_ADD;REAL_OF_COMPLEX_RE;RE_ADD]);;\r
 259 \r
 260 let REAL_MUL = prove\r
 261   (`!x y. real x /\ real y ==> real (x*y)`,\r
 262   REWRITE_TAC[real] THEN SIMPLE_COMPLEX_ARITH_TAC);;\r
 263 \r
 264 let REAL_OF_COMPLEX_MUL = prove(\r
 265   `!x y. real x /\ real y\r
 266     ==> real_of_complex (x*y) = real_of_complex x * real_of_complex y`,\r
 267   MESON_TAC[REAL_MUL;REAL_OF_COMPLEX;CX_MUL;REAL_OF_COMPLEX_CX]);;\r
 268 \r
 269 let REAL_OF_COMPLEX_0 = prove(\r
 270   `!x. real x ==> (real_of_complex x = &0 <=> x = Cx(&0))`,\r
 271   REWRITE_TAC[REAL_EXISTS] THEN REPEAT STRIP_TAC\r
 272   THEN ASM_SIMP_TAC[REAL_OF_COMPLEX_CX;CX_INJ]);;\r
 273 \r
 274 let REAL_COMPLEX_ADD_CNJ = prove(\r
 275   `!x. real(cnj x + x) /\ real(x + cnj x)`,\r
 276   REWRITE_TAC[COMPLEX_ADD_CNJ;REAL_CX]);;\r
 277 \r
 278 (* TODO\r
 279  *let RE_EQ_NORM = prove(`!x. Re x = norm x <=> real x /\ &0 <= real_of_complex x`,\r
 280  *)\r
 281 \r
 282   (* ----------------------------------------------------------------------- *)\r
 283   (* Additions to the vectors library                                        *)\r
 284   (* ----------------------------------------------------------------------- *)\r
 285 \r
 286 let vector_const = new_definition\r
 287   `vector_const (k:A) :A^N = lambda i. k`;;\r
 288 let vector_map = new_definition\r
 289   `vector_map (f:A->B) (v:A^N) :B^N = lambda i. f(v$i)`;;\r
 290 let vector_map2 = new_definition\r
 291   `vector_map2 (f:A->B->C) (v1:A^N) (v2:B^N) :C^N =\r
 292     lambda i. f (v1$i) (v2$i)`;;\r
 293 let vector_map3 = new_definition\r
 294   `vector_map3 (f:A->B->C->D) (v1:A^N) (v2:B^N) (v3:C^N) :D^N =\r
 295     lambda i. f (v1$i) (v2$i) (v3$i)`;;\r
 296 \r
 297 let FINITE_INDEX_INRANGE_2 = prove\r
 298  (`!i. ?k. 1 <= k /\ k <= dimindex(:N) /\ (!x:A^N. x$i = x$k)\r
 299   /\ (!x:B^N. x$i = x$k) /\ (!x:C^N. x$i = x$k) /\ (!x:D^N. x$i = x$k)`,\r
 300   REWRITE_TAC[finite_index] THEN MESON_TAC[FINITE_INDEX_WORKS]);;\r
 301 \r
 302 let COMPONENT_TAC x =\r
 303   REPEAT GEN_TAC THEN CHOOSE_TAC (SPEC_ALL FINITE_INDEX_INRANGE_2)\r
 304   THEN ASM_SIMP_TAC[x;LAMBDA_BETA];;\r
 305 \r
 306 let VECTOR_CONST_COMPONENT = prove\r
 307   (`!i k. ((vector_const k):A^N)$i = k`,\r
 308   COMPONENT_TAC vector_const);;\r
 309 let VECTOR_MAP_COMPONENT = prove\r
 310   (`!i f:A->B v:A^N. (vector_map f v)$i = f (v$i)`,\r
 311   COMPONENT_TAC vector_map);;\r
 312 let VECTOR_MAP2_COMPONENT = prove\r
 313   (`!i f:A->B->C v1:A^N v2. (vector_map2 f v1 v2)$i = f (v1$i) (v2$i)`,\r
 314   COMPONENT_TAC vector_map2);;\r
 315 let VECTOR_MAP3_COMPONENT = prove(\r
 316   `!i f:A->B->C->D v1:A^N v2 v3. (vector_map3 f v1 v2 v3)$i =\r
 317     f (v1$i) (v2$i) (v3$i)`,\r
 318     COMPONENT_TAC vector_map3);;\r
 319 \r
 320 let COMMON_TAC =\r
 321   REWRITE_TAC[vector_const;vector_map;vector_map2;vector_map3]\r
 322   THEN ONCE_REWRITE_TAC[CART_EQ] THEN SIMP_TAC[LAMBDA_BETA;o_DEF];;\r
 323 \r
 324 let VECTOR_MAP_VECTOR_CONST = prove\r
 325   (`!f:A->B k. vector_map f ((vector_const k):A^N) = vector_const (f k)`,\r
 326   COMMON_TAC);;\r
 327 \r
 328 let VECTOR_MAP_VECTOR_MAP = prove\r
 329   (`!f:A->B g:C->A v:C^N.\r
 330     vector_map f (vector_map g v) = vector_map (f o g) v`,\r
 331   COMMON_TAC);;\r
 332 \r
 333 let VECTOR_MAP_VECTOR_MAP2 = prove\r
 334   (`!f:A->B g:C->D->A u v:D^N.\r
 335     vector_map f (vector_map2 g u v) = vector_map2 (\x y. f (g x y)) u v`,\r
 336   COMMON_TAC);;\r
 337 \r
 338 let VECTOR_MAP2_LVECTOR_CONST = prove\r
 339   (`!f:A->B->C k v:B^N.\r
 340     vector_map2 f (vector_const k) v = vector_map (f k) v`,\r
 341   COMMON_TAC);;\r
 342 \r
 343 let VECTOR_MAP2_RVECTOR_CONST = prove\r
 344   (`!f:A->B->C k v:A^N.\r
 345     vector_map2 f v (vector_const k) = vector_map (\x. f x k) v`,\r
 346   COMMON_TAC);;\r
 347 \r
 348 let VECTOR_MAP2_LVECTOR_MAP = prove\r
 349   (`!f:A->B->C g:D->A v1 v2:B^N.\r
 350     vector_map2 f (vector_map g v1) v2 = vector_map2 (f o g) v1 v2`,\r
 351   COMMON_TAC);;\r
 352 \r
 353 let VECTOR_MAP2_RVECTOR_MAP = prove\r
 354   (`!f:A->B->C g:D->B v1 v2:D^N.\r
 355     vector_map2 f v1 (vector_map g v2) = vector_map2 (\x y. f x (g y)) v1 v2`,\r
 356   COMMON_TAC);;\r
 357 \r
 358 let VECTOR_MAP2_LVECTOR_MAP2 = prove\r
 359   (`!f:A->B->C g:D->E->A v1 v2 v3:B^N.\r
 360     vector_map2 f (vector_map2 g v1 v2) v3 =\r
 361       vector_map3 (\x y. f (g x y)) v1 v2 v3`,\r
 362   COMMON_TAC);;\r
 363 \r
 364 let VECTOR_MAP2_RVECTOR_MAP2 = prove(\r
 365   `!f:A->B->C g:D->E->B v1 v2 v3:E^N.\r
 366     vector_map2 f v1 (vector_map2 g v2 v3) =\r
 367       vector_map3 (\x y z. f x (g y z)) v1 v2 v3`,\r
 368   COMMON_TAC);;\r
 369 \r
 370 let VECTOR_MAP_SIMP_TAC = REWRITE_TAC[\r
 371     VECTOR_MAP_VECTOR_CONST;VECTOR_MAP2_LVECTOR_CONST;\r
 372     VECTOR_MAP2_RVECTOR_CONST;VECTOR_MAP_VECTOR_MAP;VECTOR_MAP2_RVECTOR_MAP;\r
 373     VECTOR_MAP2_LVECTOR_MAP;VECTOR_MAP2_RVECTOR_MAP2;VECTOR_MAP2_LVECTOR_MAP2;\r
 374     VECTOR_MAP_VECTOR_MAP2];;\r
 375 \r
 376 let VECTOR_MAP_PROPERTY_TAC fs prop =\r
 377   REWRITE_TAC fs THEN VECTOR_MAP_SIMP_TAC THEN ONCE_REWRITE_TAC[CART_EQ]\r
 378   THEN REWRITE_TAC[VECTOR_MAP_COMPONENT;VECTOR_MAP2_COMPONENT;\r
 379     VECTOR_MAP3_COMPONENT;VECTOR_CONST_COMPONENT;o_DEF;prop];;\r
 380 \r
 381 let VECTOR_MAP_PROPERTY thm f prop =\r
 382   prove(thm,VECTOR_MAP_PROPERTY_TAC f prop);;\r
 383 \r
 384 let COMPLEX_VECTOR_MAP = prove\r
 385   (`!f:complex->complex g. f = vector_map g \r
 386     <=> !z. f z = complex (g (Re z), g (Im z))`,\r
 387   REWRITE_TAC[vector_map;FUN_EQ_THM;complex] THEN REPEAT (GEN_TAC ORELSE EQ_TAC)\r
 388   THEN ASM_SIMP_TAC[CART_EQ;DIMINDEX_2;FORALL_2;LAMBDA_BETA;VECTOR_2;RE_DEF;IM_DEF]);;\r
 389 \r
 390 let COMPLEX_NEG_IS_A_MAP = prove\r
 391   (`(--):complex->complex = vector_map ((--):real->real)`,\r
 392   REWRITE_TAC[COMPLEX_VECTOR_MAP;complex_neg]);;\r
 393 \r
 394 let VECTOR_NEG_IS_A_MAP = prove\r
 395   (`(--):real^N->real^N = vector_map ((--):real->real)`,\r
 396   REWRITE_TAC[FUN_EQ_THM;CART_EQ;VECTOR_NEG_COMPONENT;VECTOR_MAP_COMPONENT]);;\r
 397 \r
 398 let VECTOR_MAP_VECTOR_MAP_ALT = prove\r
 399   (`!f:A^N->B^N g:C^N->A^N f' g'. f = vector_map f' /\ g = vector_map g' ==>\r
 400     f o g = vector_map (f' o g')`,\r
 401   SIMP_TAC[o_DEF;FUN_EQ_THM;VECTOR_MAP_VECTOR_MAP]);;\r
 402 \r
 403 let COMPLEX_VECTOR_MAP2 = prove\r
 404   (`!f:complex->complex->complex g. f = vector_map2 g <=>\r
 405     !z1 z2. f z1 z2 = complex (g (Re z1) (Re z2), g (Im z1) (Im z2))`,\r
 406   REWRITE_TAC[vector_map2;FUN_EQ_THM;complex]\r
 407   THEN REPEAT (GEN_TAC ORELSE EQ_TAC)\r
 408   THEN ASM_SIMP_TAC[CART_EQ;DIMINDEX_2;FORALL_2;LAMBDA_BETA;VECTOR_2;RE_DEF;\r
 409     IM_DEF]);;\r
 410 \r
 411 let VECTOR_MAP2_RVECTOR_MAP_ALT = prove(\r
 412   `!f:complex->complex->complex g:complex->complex f' g'.\r
 413     f = vector_map2 f' /\ g = vector_map g'\r
 414       ==> (\x y. f x (g y)) = vector_map2 (\x y. f' x (g' y))`,\r
 415   SIMP_TAC[FUN_EQ_THM;VECTOR_MAP2_RVECTOR_MAP]);;\r
 416 \r
 417 let COMPLEX_ADD_IS_A_MAP = prove\r
 418   (`(+):complex->complex->complex = vector_map2 ((+):real->real->real)`,\r
 419   REWRITE_TAC[COMPLEX_VECTOR_MAP2;complex_add]);;\r
 420 \r
 421 let VECTOR_ADD_IS_A_MAP = prove\r
 422   (`(+):real^N->real^N->real^N = vector_map2 ((+):real->real->real)`,\r
 423   REWRITE_TAC[FUN_EQ_THM;CART_EQ;VECTOR_ADD_COMPONENT;VECTOR_MAP2_COMPONENT]);;\r
 424 \r
 425 let COMPLEX_SUB_IS_A_MAP = prove\r
 426   (`(-):complex->complex->complex = vector_map2 ((-):real->real->real)`, \r
 427   ONCE_REWRITE_TAC[prove(`(-) = \x y:complex. x-y`,REWRITE_TAC[FUN_EQ_THM])]\r
 428   THEN ONCE_REWRITE_TAC[prove(`(-) = \x y:real. x-y`,REWRITE_TAC[FUN_EQ_THM])]\r
 429   THEN REWRITE_TAC[complex_sub;real_sub]\r
 430   THEN MATCH_MP_TAC VECTOR_MAP2_RVECTOR_MAP_ALT\r
 431   THEN REWRITE_TAC[COMPLEX_NEG_IS_A_MAP;COMPLEX_ADD_IS_A_MAP]);;\r
 432 \r
 433 let VECTOR_SUB_IS_A_MAP = prove\r
 434   (`(-):real^N->real^N->real^N = vector_map2 ((-):real->real->real)`,\r
 435   REWRITE_TAC[FUN_EQ_THM;CART_EQ;VECTOR_SUB_COMPONENT;VECTOR_MAP2_COMPONENT]);;\r
 436 \r
 437 let COMMON_TAC x = \r
 438   SIMP_TAC[CART_EQ;pastecart;x;LAMBDA_BETA] THEN REPEAT STRIP_TAC\r
 439   THEN REPEAT COND_CASES_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[]\r
 440   THEN SUBGOAL_THEN `1<= i-dimindex(:N) /\ i-dimindex(:N) <= dimindex(:M)`\r
 441     ASSUME_TAC\r
 442   THEN ASM_SIMP_TAC[LAMBDA_BETA]\r
 443   THEN REPEAT (POP_ASSUM (MP_TAC o REWRITE_RULE[DIMINDEX_FINITE_SUM]))\r
 444   THEN ARITH_TAC;;\r
 445 \r
 446 let PASTECART_VECTOR_MAP = prove\r
 447   (`!f:A->B x:A^N y:A^M.\r
 448     pastecart (vector_map f x) (vector_map f y) =\r
 449       vector_map f (pastecart x y)`,\r
 450     COMMON_TAC vector_map);;\r
 451 \r
 452 let PASTECART_VECTOR_MAP2 = prove\r
 453   (`!f:A->B->C x1:A^N x2 y1:A^M y2.\r
 454     pastecart (vector_map2 f x1 x2) (vector_map2 f y1 y2)\r
 455       = vector_map2 f (pastecart x1 y1) (pastecart x2 y2)`,\r
 456   COMMON_TAC vector_map2);;\r
 457 \r
 458 let vector_zip = new_definition\r
 459   `vector_zip (v1:A^N) (v2:B^N) : (A#B)^N = lambda i. (v1$i,v2$i)`;;\r
 460 \r
 461 let VECTOR_ZIP_COMPONENT = prove\r
 462   (`!i v1:A^N v2:B^N. (vector_zip v1 v2)$i = (v1$i,v2$i)`,\r
 463   REPEAT GEN_TAC THEN CHOOSE_TAC (INST_TYPE [`:A#B`,`:C`] (SPEC_ALL\r
 464     FINITE_INDEX_INRANGE_2)) THEN ASM_SIMP_TAC[vector_zip;LAMBDA_BETA]);;\r
 465 \r
 466 let vector_unzip = new_definition\r
 467   `vector_unzip (v:(A#B)^N):(A^N)#(B^N) = vector_map FST v,vector_map SND v`;;\r
 468 \r
 469 let VECTOR_UNZIP_COMPONENT = prove\r
 470   (`!i v:(A#B)^N. (FST (vector_unzip v))$i = FST (v$i)\r
 471     /\ (SND (vector_unzip v))$i = SND (v$i)`,\r
 472   REWRITE_TAC[vector_unzip;VECTOR_MAP_COMPONENT]);;\r
 473 \r
 474 let VECTOR_MAP2_AS_VECTOR_MAP = prove\r
 475   (`!f:A->B->C v1:A^N v2:B^N.\r
 476     vector_map2 f v1 v2 = vector_map (UNCURRY f) (vector_zip v1 v2)`,\r
 477   REWRITE_TAC[CART_EQ;VECTOR_MAP2_COMPONENT;VECTOR_MAP_COMPONENT;\r
 478     VECTOR_ZIP_COMPONENT;UNCURRY_DEF]);;\r
 479 \r
 480 \r
 481 \r
 482 (* ========================================================================= *)\r
 483 (* BASIC ARITHMETIC                                                          *)\r
 484 (* ========================================================================= *)\r
 485 \r
 486 make_overloadable "%" `:A-> B-> B`;; \r
 487 \r
 488 let prioritize_cvector () =\r
 489   overload_interface("--",`(cvector_neg):complex^N->complex^N`);\r
 490   overload_interface("+",`(cvector_add):complex^N->complex^N->complex^N`);\r
 491   overload_interface("-",`(cvector_sub):complex^N->complex^N->complex^N`);\r
 492   overload_interface("%",`(cvector_mul):complex->complex^N->complex^N`);;\r
 493 \r
 494 let cvector_zero = new_definition\r
 495   `cvector_zero:complex^N = vector_const (Cx(&0))`;;\r
 496 \r
 497 let cvector_neg = new_definition\r
 498   `cvector_neg :complex^N->complex^N = vector_map (--)`;;\r
 499 \r
 500 let cvector_add = new_definition\r
 501   `cvector_add :complex^N->complex^N->complex^N = vector_map2 (+)`;;\r
 502 \r
 503 let cvector_sub = new_definition\r
 504   `cvector_sub :complex^N->complex^N->complex^N = vector_map2 (-)`;;\r
 505 \r
 506 let cvector_mul = new_definition\r
 507   `(cvector_mul:complex->complex^N->complex^N) a = vector_map (( * ) a)`;;\r
 508 \r
 509 overload_interface("%",`(%):real->real^N->real^N`);;\r
 510 prioritize_cvector ();;\r
 511 \r
 512 let CVECTOR_ZERO_COMPONENT = prove\r
 513   (`!i. (cvector_zero:complex^N)$i = Cx(&0)`,\r
 514   REWRITE_TAC[cvector_zero;VECTOR_CONST_COMPONENT]);;\r
 515 \r
 516 let CVECTOR_NON_ZERO = prove\r
 517   (`!x:complex^N. ~(x=cvector_zero)\r
 518     <=> ?i. 1 <= i /\ i <= dimindex(:N) /\ ~(x$i = Cx(&0))`,\r
 519   GEN_TAC THEN GEN_REWRITE_TAC (RATOR_CONV o ONCE_DEPTH_CONV) [CART_EQ]\r
 520   THEN REWRITE_TAC[CVECTOR_ZERO_COMPONENT] THEN MESON_TAC[]);;\r
 521 \r
 522 let CVECTOR_ADD_COMPONENT = prove\r
 523   (`!X Y:complex^N i. ((X + Y)$i = X$i + Y$i)`,\r
 524   REWRITE_TAC[cvector_add;VECTOR_MAP2_COMPONENT]);;\r
 525 \r
 526 let CVECTOR_SUB_COMPONENT = prove \r
 527   (`!X:complex^N Y i. ((X - Y)$i = X$i - Y$i)`,\r
 528   REWRITE_TAC[cvector_sub;VECTOR_MAP2_COMPONENT]);;\r
 529 \r
 530 let CVECTOR_NEG_COMPONENT = prove\r
 531   (`!X:complex^N i. ((--X)$i = --(X$i))`,\r
 532   REWRITE_TAC[cvector_neg;VECTOR_MAP_COMPONENT]);;\r
 533 \r
 534 let CVECTOR_MUL_COMPONENT = prove\r
 535   (`!c:complex X:complex^N i. ((c % X)$i = c * X$i)`,\r
 536   REWRITE_TAC[cvector_mul;VECTOR_MAP_COMPONENT]);;\r
 537 \r
 538 (* Simple generic tactic adapted from VECTOR_ARITH_TAC *)\r
 539 let CVECTOR_ARITH_TAC =\r
 540   let RENAMED_LAMBDA_BETA th =\r
 541     if fst(dest_fun_ty(type_of(funpow 3 rand (concl th)))) = aty\r
 542     then INST_TYPE [aty,bty; bty,aty] LAMBDA_BETA else LAMBDA_BETA \r
 543   in\r
 544   POP_ASSUM_LIST(K ALL_TAC) THEN\r
 545   REPEAT(GEN_TAC ORELSE CONJ_TAC ORELSE DISCH_TAC ORELSE EQ_TAC) THEN\r
 546   REPEAT(POP_ASSUM MP_TAC) THEN REWRITE_TAC[IMP_IMP; GSYM CONJ_ASSOC] THEN\r
 547   GEN_REWRITE_TAC ONCE_DEPTH_CONV [CART_EQ] THEN\r
 548   REWRITE_TAC[AND_FORALL_THM] THEN TRY EQ_TAC THEN\r
 549   TRY(MATCH_MP_TAC MONO_FORALL) THEN GEN_TAC THEN\r
 550   REWRITE_TAC[TAUT `(a ==> b) /\ (a ==> c) <=> a ==> b /\ c`;\r
 551               TAUT `(a ==> b) \/ (a ==> c) <=> a ==> b \/ c`] THEN\r
 552   TRY(MATCH_MP_TAC(TAUT `(a ==> b ==> c) ==> (a ==> b) ==> (a ==> c)`)) THEN\r
 553   REWRITE_TAC[cvector_zero;cvector_add; cvector_sub; cvector_neg; cvector_mul; vector_map;vector_map2;vector_const] THEN\r
 554   DISCH_THEN(fun th -> REWRITE_TAC[MATCH_MP(RENAMED_LAMBDA_BETA th) th]) THEN\r
 555   SIMPLE_COMPLEX_ARITH_TAC;;\r
 556 \r
 557 let CVECTOR_ARITH tm = prove(tm,CVECTOR_ARITH_TAC);;\r
 558 \r
 559 (* ========================================================================= *)\r
 560 (*  VECTOR SPACE AXIOMS AND ADDITIONAL BASIC RESULTS                         *)\r
 561 (* ========================================================================= *)\r
 562 \r
 563 let CVECTOR_MAP_PROPERTY thm =\r
 564   VECTOR_MAP_PROPERTY thm [cvector_zero;cvector_add;cvector_sub;cvector_neg;\r
 565     cvector_mul];;\r
 566 \r
 567 let CVECTOR_ADD_SYM = CVECTOR_MAP_PROPERTY\r
 568   `!x y:complex^N. x + y = y + x`\r
 569   COMPLEX_ADD_SYM;;\r
 570 \r
 571 let CVECTOR_ADD_ASSOC = CVECTOR_MAP_PROPERTY\r
 572   `!x y z:complex^N. x + (y + z) = (x + y) + z`\r
 573   COMPLEX_ADD_ASSOC;;\r
 574 \r
 575 let CVECTOR_ADD_ID = CVECTOR_MAP_PROPERTY\r
 576   `!x:complex^N. x + cvector_zero = x /\ cvector_zero + x = x`\r
 577   (CONJ COMPLEX_ADD_RID COMPLEX_ADD_LID);;\r
 578 \r
 579 let [CVECTOR_ADD_RID;CVECTOR_ADD_LID] = GCONJUNCTS CVECTOR_ADD_ID;;\r
 580 \r
 581 let CVECTOR_ADD_INV = CVECTOR_MAP_PROPERTY\r
 582   `!x:complex^N. x + -- x = cvector_zero /\ --x + x = cvector_zero`\r
 583   (CONJ COMPLEX_ADD_RINV COMPLEX_ADD_LINV);;\r
 584 \r
 585 let CVECTOR_MUL_ASSOC = CVECTOR_MAP_PROPERTY\r
 586   `!a b x:complex^N. a % (b % x) = (a * b) % x`\r
 587   COMPLEX_MUL_ASSOC;;\r
 588 \r
 589 let CVECTOR_SUB_LDISTRIB = CVECTOR_MAP_PROPERTY\r
 590   `!c x y:complex^N. c % (x - y) = c % x - c % y`\r
 591   COMPLEX_SUB_LDISTRIB;;\r
 592 \r
 593 let CVECTOR_SCALAR_RDIST = CVECTOR_MAP_PROPERTY\r
 594   `!a b x:complex^N. (a + b) % x = a % x + b % x`\r
 595   COMPLEX_ADD_RDISTRIB;;\r
 596 \r
 597 let CVECTOR_MUL_ID = CVECTOR_MAP_PROPERTY\r
 598   `!x:complex^N. Cx(&1) % x = x`\r
 599   COMPLEX_MUL_LID;;\r
 600 \r
 601 let CVECTOR_SUB_REFL = CVECTOR_MAP_PROPERTY\r
 602   `!x:complex^N. x - x = cvector_zero`\r
 603   COMPLEX_SUB_REFL;;\r
 604 \r
 605 let CVECTOR_SUB_RADD = CVECTOR_MAP_PROPERTY\r
 606   `!x y:complex^N. x - (x + y) = --y`\r
 607   COMPLEX_ADD_SUB2;;\r
 608 \r
 609 let CVECTOR_NEG_SUB = CVECTOR_MAP_PROPERTY\r
 610   `!x y:complex^N. --(x - y) = y - x`\r
 611   COMPLEX_NEG_SUB;;\r
 612 \r
 613 let CVECTOR_SUB_EQ = CVECTOR_MAP_PROPERTY\r
 614   `!x y:complex^N. (x - y = cvector_zero) <=> (x = y)`\r
 615   COMPLEX_SUB_0;;\r
 616 \r
 617 let CVECTOR_MUL_LZERO = CVECTOR_MAP_PROPERTY\r
 618   `!x. Cx(&0) % x = cvector_zero`\r
 619   COMPLEX_MUL_LZERO;;\r
 620 \r
 621 let CVECTOR_SUB_ADD = CVECTOR_MAP_PROPERTY\r
 622   `!x y:complex^N. (x - y) + y = x`\r
 623   COMPLEX_SUB_ADD;;\r
 624 \r
 625 let CVECTOR_SUB_ADD2 = CVECTOR_MAP_PROPERTY\r
 626   `!x y:complex^N. y + (x - y) = x`\r
 627   COMPLEX_SUB_ADD2;;\r
 628 \r
 629 let CVECTOR_ADD_LDISTRIB = CVECTOR_MAP_PROPERTY\r
 630   `!c x y:complex^N. c % (x + y) = c % x + c % y`\r
 631   COMPLEX_ADD_LDISTRIB;;\r
 632 \r
 633 let CVECTOR_ADD_RDISTRIB = CVECTOR_MAP_PROPERTY\r
 634   `!a b x:complex^N. (a + b) % x = a % x + b % x`\r
 635   COMPLEX_ADD_RDISTRIB;;\r
 636 \r
 637 let CVECTOR_SUB_RDISTRIB = CVECTOR_MAP_PROPERTY\r
 638   `!a b x:complex^N. (a - b) % x = a % x - b % x`\r
 639   COMPLEX_SUB_RDISTRIB;;\r
 640 \r
 641 let CVECTOR_ADD_SUB = CVECTOR_MAP_PROPERTY\r
 642   `!x y:complex^N. (x + y:complex^N) - x = y`\r
 643   COMPLEX_ADD_SUB;;\r
 644 \r
 645 let CVECTOR_EQ_ADDR = CVECTOR_MAP_PROPERTY\r
 646   `!x y:complex^N. (x + y = x) <=> (y = cvector_zero)`\r
 647   COMPLEX_EQ_ADD_LCANCEL_0;;\r
 648 \r
 649 let CVECTOR_SUB = CVECTOR_MAP_PROPERTY\r
 650   `!x y:complex^N. x - y = x + --(y:complex^N)`\r
 651   complex_sub;;\r
 652 \r
 653 let CVECTOR_SUB_RZERO = CVECTOR_MAP_PROPERTY\r
 654   `!x:complex^N. x - cvector_zero = x`\r
 655   COMPLEX_SUB_RZERO;;\r
 656 \r
 657 let CVECTOR_MUL_RZERO = CVECTOR_MAP_PROPERTY\r
 658   `!c:complex. c % cvector_zero = cvector_zero`\r
 659   COMPLEX_MUL_RZERO;;\r
 660 \r
 661 let CVECTOR_MUL_LZERO = CVECTOR_MAP_PROPERTY\r
 662   `!x:complex^N. Cx(&0) % x = cvector_zero`\r
 663   COMPLEX_MUL_LZERO;;\r
 664 \r
 665 let CVECTOR_MUL_EQ_0 = prove\r
 666   (`!a:complex x:complex^N.\r
 667     (a % x = cvector_zero <=> a = Cx(&0) \/ x = cvector_zero)`,\r
 668   REPEAT STRIP_TAC THEN EQ_TAC THENL [\r
 669     ASM_CASES_TAC `a=Cx(&0)` THENL [\r
 670       ASM_REWRITE_TAC[];\r
 671       GEN_REWRITE_TAC (RATOR_CONV o DEPTH_CONV) [CART_EQ]\r
 672       THEN ASM_REWRITE_TAC[CVECTOR_MUL_COMPONENT;CVECTOR_ZERO_COMPONENT;\r
 673         COMPLEX_ENTIRE]\r
 674       THEN GEN_REWRITE_TAC (RAND_CONV o DEPTH_CONV) [CART_EQ]\r
 675       THEN REWRITE_TAC[CVECTOR_ZERO_COMPONENT];\r
 676     ];\r
 677     REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[CVECTOR_MUL_RZERO;CVECTOR_MUL_LZERO];\r
 678   ]);;\r
 679 \r
 680 let CVECTOR_NEG_MINUS1 = CVECTOR_MAP_PROPERTY\r
 681   `!x:complex^N. --x = (--(Cx(&1))) % x`\r
 682   (GSYM COMPLEX_NEG_MINUS1);;\r
 683 \r
 684 let CVECTOR_SUB_LZERO = CVECTOR_MAP_PROPERTY\r
 685   `!x:complex^N. cvector_zero - x = --x`\r
 686   COMPLEX_SUB_LZERO;;\r
 687 \r
 688 let CVECTOR_NEG_NEG = CVECTOR_MAP_PROPERTY\r
 689   `!x:complex^N. --(--(x:complex^N)) = x`\r
 690   COMPLEX_NEG_NEG;;\r
 691 \r
 692 let CVECTOR_MUL_LNEG = CVECTOR_MAP_PROPERTY\r
 693   `!c x:complex^N. --c % x = --(c % x)`\r
 694   COMPLEX_MUL_LNEG;;\r
 695 \r
 696 let CVECTOR_MUL_RNEG = CVECTOR_MAP_PROPERTY\r
 697   `!c x:complex^N. c % --x = --(c % x)`\r
 698   COMPLEX_MUL_RNEG;;\r
 699 \r
 700 let CVECTOR_NEG_0 = CVECTOR_MAP_PROPERTY\r
 701   `--cvector_zero = cvector_zero`\r
 702   COMPLEX_NEG_0;;\r
 703 \r
 704 let CVECTOR_NEG_EQ_0 = CVECTOR_MAP_PROPERTY\r
 705   `!x:complex^N. --x = cvector_zero <=> x = cvector_zero`\r
 706   COMPLEX_NEG_EQ_0;;\r
 707 \r
 708 let CVECTOR_ADD_AC = prove\r
 709   (`!x y z:complex^N.\r
 710     (x + y = y + x) /\ ((x + y) + z = x + y + z) /\ (x + y + z = y + x + z)`,\r
 711   MESON_TAC[CVECTOR_ADD_SYM;CVECTOR_ADD_ASSOC]);;\r
 712 \r
 713 let CVECTOR_MUL_LCANCEL = prove\r
 714   (`!a x y:complex^N. a % x = a % y <=> a = Cx(&0) \/ x = y`,\r
 715   MESON_TAC[CVECTOR_MUL_EQ_0;CVECTOR_SUB_LDISTRIB;CVECTOR_SUB_EQ]);;\r
 716 \r
 717 let CVECTOR_MUL_RCANCEL = prove\r
 718   (`!a b x:complex^N. a % x = b % x <=> a = b \/ x = cvector_zero`,\r
 719   MESON_TAC[CVECTOR_MUL_EQ_0;CVECTOR_SUB_RDISTRIB;COMPLEX_SUB_0;CVECTOR_SUB_EQ]);;\r
 720 \r
 721 \r
 722 (* ========================================================================= *)\r
 723 (* LINEARITY                                                                 *)\r
 724 (* ========================================================================= *)\r
 725 \r
 726 let clinear = new_definition\r
 727   `clinear (f:complex^M->complex^N)\r
 728     <=> (!x y. f(x + y) = f(x) + f(y)) /\ (!c x. f(c % x) = c % f(x))`;;\r
 729 \r
 730 let COMMON_TAC additional_thms =\r
 731   SIMP_TAC[clinear] THEN REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[CART_EQ]\r
 732   THEN SIMP_TAC(CVECTOR_ADD_COMPONENT::CVECTOR_MUL_COMPONENT::additional_thms)\r
 733   THEN SIMPLE_COMPLEX_ARITH_TAC;;\r
 734 \r
 735 let CLINEAR_COMPOSE_CMUL = prove\r
 736  (`!f:complex^M->complex^N c. clinear f ==> clinear (\x. c % f x)`,\r
 737  COMMON_TAC[]);;\r
 738 \r
 739 let CLINEAR_COMPOSE_NEG = prove\r
 740  (`!f:complex^M->complex^N. clinear f ==> clinear (\x. --(f x))`,\r
 741  COMMON_TAC[CVECTOR_NEG_COMPONENT]);;\r
 742 \r
 743 let CLINEAR_COMPOSE_ADD = prove\r
 744  (`!f:complex^M->complex^N g. clinear f /\ clinear g ==> clinear (\x. f x + g x)`,\r
 745  COMMON_TAC[]);;\r
 746 \r
 747 let CLINEAR_COMPOSE_SUB = prove\r
 748  (`!f:complex^M->complex^N g. clinear f /\ clinear g ==> clinear (\x. f x - g x)`,\r
 749  COMMON_TAC[CVECTOR_SUB_COMPONENT]);;\r
 750 \r
 751 let CLINEAR_COMPOSE = prove\r
 752  (`!f:complex^M->complex^N g. clinear f /\ clinear g ==> clinear (g o f)`,\r
 753  SIMP_TAC[clinear;o_THM]);;\r
 754 \r
 755 let CLINEAR_ID = prove\r
 756  (`clinear (\x:complex^N. x)`,\r
 757  REWRITE_TAC[clinear]);;\r
 758 \r
 759 let CLINEAR_I = prove\r
 760  (`clinear (I:complex^N->complex^N)`,\r
 761   REWRITE_TAC[I_DEF;CLINEAR_ID]);;\r
 762 \r
 763 let CLINEAR_ZERO = prove\r
 764  (`clinear ((\x. cvector_zero):complex^M->complex^N)`,\r
 765  COMMON_TAC[CVECTOR_ZERO_COMPONENT]);;\r
 766 \r
 767 let CLINEAR_NEGATION = prove\r
 768  (`clinear ((--):complex^N->complex^N)`,\r
 769  COMMON_TAC[CVECTOR_NEG_COMPONENT]);;\r
 770 \r
 771 let CLINEAR_VMUL_COMPONENT = prove\r
 772  (`!f:complex^M->complex^N v:complex^P k.\r
 773      clinear f /\ 1 <= k /\ k <= dimindex(:N) ==> clinear (\x. (f x)$k % v)`,\r
 774  COMMON_TAC[]);;\r
 775 \r
 776 let CLINEAR_0 = prove\r
 777  (`!f:complex^M->complex^N. clinear f ==> (f cvector_zero = cvector_zero)`,\r
 778   MESON_TAC[CVECTOR_MUL_LZERO;clinear]);;\r
 779 \r
 780 let CLINEAR_CMUL = prove\r
 781  (`!f:complex^M->complex^N c x. clinear f ==> (f (c % x) = c % f x)`,\r
 782   SIMP_TAC[clinear]);;\r
 783 \r
 784 let CLINEAR_NEG = prove\r
 785  (`!f:complex^M->complex^N x. clinear f ==> (f (--x) = --(f x))`,\r
 786   ONCE_REWRITE_TAC[CVECTOR_NEG_MINUS1] THEN SIMP_TAC[CLINEAR_CMUL]);;\r
 787 \r
 788 let CLINEAR_ADD = prove\r
 789  (`!f:complex^M->complex^N x y. clinear f ==> (f (x + y) = f x + f y)`,\r
 790   SIMP_TAC[clinear]);;\r
 791 \r
 792 let CLINEAR_SUB = prove\r
 793  (`!f:complex^M->complex^N x y. clinear f ==> (f(x - y) = f x - f y)`,\r
 794   SIMP_TAC[CVECTOR_SUB;CLINEAR_ADD;CLINEAR_NEG]);;\r
 795 \r
 796 let CLINEAR_INJECTIVE_0 = prove\r
 797  (`!f:complex^M->complex^N.\r
 798   clinear f\r
 799    ==> ((!x y. f x = f y ==> x = y)\r
 800     <=> (!x. f x = cvector_zero ==> x = cvector_zero))`,\r
 801   ONCE_REWRITE_TAC[GSYM CVECTOR_SUB_EQ] \r
 802   THEN SIMP_TAC[CVECTOR_SUB_RZERO;GSYM CLINEAR_SUB]\r
 803   THEN MESON_TAC[CVECTOR_SUB_RZERO]);;\r
 804 \r
 805 \r
 806 \r
 807 (* ========================================================================= *)\r
 808 (* PASTING COMPLEX VECTORS                                                   *)\r
 809 (* ========================================================================= *)\r
 810 \r
 811 let CLINEAR_FSTCART_SNDCART = prove\r
 812   (`clinear fstcart /\ clinear sndcart`,\r
 813   SIMP_TAC[clinear;fstcart;sndcart;CART_EQ;LAMBDA_BETA;CVECTOR_ADD_COMPONENT;\r
 814     CVECTOR_MUL_COMPONENT; DIMINDEX_FINITE_SUM;\r
 815     ARITH_RULE `x <= a ==> x <= a + b:num`;\r
 816     ARITH_RULE `x <= b ==> x + a <= a + b:num`]);;\r
 817 \r
 818 let FSTCART_CLINEAR = CONJUNCT1 CLINEAR_FSTCART_SNDCART;;\r
 819 let SNDCART_CLINEAR = CONJUNCT2 CLINEAR_FSTCART_SNDCART;;\r
 820 \r
 821 let FSTCART_SNDCART_CVECTOR_ZERO = prove\r
 822   (`fstcart cvector_zero = cvector_zero /\ sndcart cvector_zero = cvector_zero`,\r
 823   SIMP_TAC[CVECTOR_ZERO_COMPONENT;fstcart;sndcart;LAMBDA_BETA;CART_EQ;\r
 824     DIMINDEX_FINITE_SUM;ARITH_RULE `x <= a ==> x <= a + b:num`;\r
 825     ARITH_RULE `x <= b ==> x + a <= a + b:num`]);;\r
 826 \r
 827 let FSTCART_CVECTOR_ZERO = CONJUNCT1 FSTCART_SNDCART_CVECTOR_ZERO;;\r
 828 let SNDCART_CVECTOR_ZERO = CONJUNCT2 FSTCART_SNDCART_CVECTOR_ZERO;;\r
 829 \r
 830 let FSTCART_SNDCART_CVECTOR_ADD = prove\r
 831  (`!x:complex^(M,N)finite_sum y.\r
 832   fstcart(x + y) = fstcart(x) + fstcart(y) \r
 833   /\ sndcart(x + y) = sndcart(x) + sndcart(y)`,\r
 834   REWRITE_TAC[REWRITE_RULE[clinear] CLINEAR_FSTCART_SNDCART]);;\r
 835 \r
 836 let FSTCART_SNDCART_CVECTOR_MUL = prove\r
 837   (`!x:complex^(M,N)finite_sum c.\r
 838   fstcart(c % x) = c % fstcart(x) /\ sndcart(c % x) = c % sndcart(x)`,\r
 839   REWRITE_TAC[REWRITE_RULE[clinear] CLINEAR_FSTCART_SNDCART]);;\r
 840 \r
 841 let PASTECART_TAC xs =\r
 842   REWRITE_TAC(PASTECART_EQ::FSTCART_PASTECART::SNDCART_PASTECART::xs);;\r
 843 \r
 844 let PASTECART_CVECTOR_ZERO = prove\r
 845   (`pastecart (cvector_zero:complex^N) (cvector_zero:complex^M) = cvector_zero`,\r
 846   PASTECART_TAC[FSTCART_SNDCART_CVECTOR_ZERO]);;\r
 847 \r
 848 let PASTECART_EQ_CVECTOR_ZERO = prove\r
 849   (`!x:complex^N y:complex^M.\r
 850     pastecart x y = cvector_zero <=> x = cvector_zero /\ y = cvector_zero`,\r
 851   PASTECART_TAC [FSTCART_SNDCART_CVECTOR_ZERO]);;\r
 852 \r
 853 let PASTECART_CVECTOR_ADD = prove\r
 854   (`!x1 y2 x2:complex^N y2:complex^M.\r
 855   pastecart x1 y1 + pastecart x2 y2 = pastecart (x1 + x2) (y1 + y2)`,\r
 856   PASTECART_TAC [FSTCART_SNDCART_CVECTOR_ADD]);;\r
 857 \r
 858 let PASTECART_CVECTOR_MUL = prove\r
 859   (`!x1 x2 c:complex.\r
 860   pastecart (c % x1) (c % y1) = c % pastecart x1 y1`, PASTECART_TAC [FSTCART_SNDCART_CVECTOR_MUL]);;\r
 861 \r
 862 \r
 863 (* ========================================================================= *)\r
 864 (* REAL AND IMAGINARY VECTORS                                                *)\r
 865 (* ========================================================================= *)\r
 866 \r
 867 let cvector_re = new_definition\r
 868   `cvector_re :complex^N -> real^N = vector_map Re`;;\r
 869 let cvector_im = new_definition\r
 870   `cvector_im :complex^N -> real^N = vector_map Im`;;\r
 871 let vector_to_cvector = new_definition\r
 872   `vector_to_cvector :real^N -> complex^N = vector_map Cx`;;\r
 873 \r
 874 let CVECTOR_RE_COMPONENT = prove\r
 875   (`!x:complex^N i. (cvector_re x)$i = Re (x$i)`,\r
 876   REWRITE_TAC[cvector_re;VECTOR_MAP_COMPONENT]);;\r
 877 let CVECTOR_IM_COMPONENT = prove\r
 878   (`!x:complex^N i. (cvector_im x)$i = Im (x$i)`,\r
 879   REWRITE_TAC[cvector_im;VECTOR_MAP_COMPONENT]);;\r
 880 let VECTOR_TO_CVECTOR_COMPONENT = prove\r
 881   (`!x:real^N i. (vector_to_cvector x)$i = Cx(x$i)`,\r
 882   REWRITE_TAC[vector_to_cvector;VECTOR_MAP_COMPONENT]);;\r
 883 \r
 884 let VECTOR_TO_CVECTOR_ZERO = prove\r
 885   (`vector_to_cvector (vec 0) = cvector_zero:complex^N`,\r
 886   ONCE_REWRITE_TAC[CART_EQ]\r
 887   THEN REWRITE_TAC[VECTOR_TO_CVECTOR_COMPONENT;CVECTOR_ZERO_COMPONENT;\r
 888     VEC_COMPONENT]);;\r
 889 \r
 890 let VECTOR_TO_CVECTOR_ZERO_EQ = prove\r
 891   (`!x:real^N. vector_to_cvector x = cvector_zero <=> x = vec 0`,\r
 892   GEN_TAC THEN EQ_TAC THEN SIMP_TAC[VECTOR_TO_CVECTOR_ZERO]\r
 893   THEN ONCE_REWRITE_TAC[CART_EQ]\r
 894   THEN SIMP_TAC[VECTOR_TO_CVECTOR_COMPONENT;CVECTOR_ZERO_COMPONENT;\r
 895     VEC_COMPONENT;CX_INJ]);;\r
 896 \r
 897 let CVECTOR_ZERO_VEC0 = prove\r
 898   (`!x:complex^N. x = cvector_zero <=> cvector_re x = vec 0 /\ cvector_im x = vec 0`,\r
 899   ONCE_REWRITE_TAC[CART_EQ]\r
 900   THEN REWRITE_TAC[CVECTOR_ZERO_COMPONENT;CVECTOR_RE_COMPONENT;\r
 901     CVECTOR_IM_COMPONENT;VEC_COMPONENT;COMPLEX_EQ;RE_CX;IM_CX]\r
 902   THEN MESON_TAC[]);;\r
 903 \r
 904 let VECTOR_TO_CVECTOR_MUL = prove\r
 905   (`!a x:real^N. vector_to_cvector (a % x) = Cx a % vector_to_cvector x`,\r
 906   ONCE_REWRITE_TAC[CART_EQ] THEN REWRITE_TAC[VECTOR_TO_CVECTOR_COMPONENT;CVECTOR_MUL_COMPONENT;VECTOR_MUL_COMPONENT;CX_MUL]);;\r
 907 \r
 908 let CVECTOR_EQ = prove\r
 909   (`!x:complex^N y z.\r
 910     x = vector_to_cvector y + ii % vector_to_cvector z\r
 911     <=> cvector_re x = y /\ cvector_im x = z`,\r
 912   ONCE_REWRITE_TAC[CART_EQ]\r
 913   THEN REWRITE_TAC[CVECTOR_ADD_COMPONENT;CVECTOR_MUL_COMPONENT;\r
 914     CVECTOR_RE_COMPONENT;CVECTOR_IM_COMPONENT;VECTOR_TO_CVECTOR_COMPONENT]\r
 915   THEN REWRITE_TAC[COMPLEX_EQ;RE_CX;IM_CX;RE_ADD;IM_ADD;RE_MUL_II;REAL_NEG_0;\r
 916     REAL_ADD_RID;REAL_ADD_LID;IM_MUL_II] THEN MESON_TAC[]);;\r
 917 \r
 918 let CVECTOR_RE_VECTOR_TO_CVECTOR = prove\r
 919   (`!x:real^N. cvector_re (vector_to_cvector x) = x`,\r
 920   ONCE_REWRITE_TAC[CART_EQ]\r
 921   THEN REWRITE_TAC[CVECTOR_RE_COMPONENT;VECTOR_TO_CVECTOR_COMPONENT;RE_CX]);;\r
 922 \r
 923 let CVECTOR_IM_VECTOR_TO_CVECTOR = prove\r
 924   (`!x:real^N. cvector_im (vector_to_cvector x) = vec 0`,\r
 925   ONCE_REWRITE_TAC[CART_EQ]\r
 926   THEN REWRITE_TAC[CVECTOR_IM_COMPONENT;VECTOR_TO_CVECTOR_COMPONENT;IM_CX;\r
 927     VEC_COMPONENT]);;\r
 928 \r
 929 let CVECTOR_IM_VECTOR_TO_CVECTOR_IM = prove\r
 930   (`!x:real^N. cvector_im (ii % vector_to_cvector x) = x`,\r
 931   ONCE_REWRITE_TAC[CART_EQ]\r
 932   THEN REWRITE_TAC[CVECTOR_IM_COMPONENT;VECTOR_TO_CVECTOR_COMPONENT;IM_CX;\r
 933     VEC_COMPONENT;CVECTOR_MUL_COMPONENT;IM_MUL_II;RE_CX]);;\r
 934 \r
 935 let VECTOR_TO_CVECTOR_CVECTOR_RE_IM = prove\r
 936   (`!x:complex^N.\r
 937     vector_to_cvector (cvector_re x) + ii % vector_to_cvector (cvector_im x)\r
 938       = x`,\r
 939   GEN_TAC THEN MATCH_MP_TAC EQ_SYM THEN REWRITE_TAC[CVECTOR_EQ]);;\r
 940 \r
 941 let CVECTOR_IM_VECTOR_TO_CVECTOR_RE_IM = prove\r
 942   (`!x y:real^N. cvector_im (vector_to_cvector x + ii % vector_to_cvector y) = y`,\r
 943   ONCE_REWRITE_TAC[CART_EQ]\r
 944   THEN REWRITE_TAC[CVECTOR_IM_COMPONENT;CVECTOR_ADD_COMPONENT;\r
 945     CVECTOR_MUL_COMPONENT;VECTOR_TO_CVECTOR_COMPONENT;IM_ADD;IM_CX;IM_MUL_II;\r
 946     RE_CX;REAL_ADD_LID]);;\r
 947 \r
 948 let CVECTOR_RE_VECTOR_TO_CVECTOR_RE_IM = prove\r
 949   (`!x y:real^N. cvector_re (vector_to_cvector x + ii % vector_to_cvector y)= x`,\r
 950   ONCE_REWRITE_TAC[CART_EQ]\r
 951   THEN REWRITE_TAC[CVECTOR_RE_COMPONENT;CVECTOR_ADD_COMPONENT;\r
 952     CVECTOR_MUL_COMPONENT;RE_ADD;VECTOR_TO_CVECTOR_COMPONENT;RE_CX;RE_MUL_CX;\r
 953     RE_II;REAL_MUL_LZERO;REAL_ADD_RID]);;\r
 954 \r
 955 let CVECTOR_RE_ADD = prove\r
 956   (`!x y:complex^N. cvector_re (x+y) = cvector_re x + cvector_re y`,\r
 957   ONCE_REWRITE_TAC[CART_EQ] THEN REWRITE_TAC[CVECTOR_RE_COMPONENT;\r
 958     VECTOR_ADD_COMPONENT;CVECTOR_ADD_COMPONENT;RE_ADD]);;\r
 959 \r
 960 let CVECTOR_IM_ADD = prove\r
 961   (`!x y:complex^N. cvector_im (x+y) = cvector_im x + cvector_im y`,\r
 962   ONCE_REWRITE_TAC[CART_EQ]\r
 963   THEN REWRITE_TAC[CVECTOR_IM_COMPONENT;VECTOR_ADD_COMPONENT;\r
 964     CVECTOR_ADD_COMPONENT;IM_ADD]);;\r
 965 \r
 966 let CVECTOR_RE_MUL = prove\r
 967   (`!a x:complex^N. cvector_re (Cx a % x) = a % cvector_re x`,\r
 968   ONCE_REWRITE_TAC[CART_EQ]\r
 969   THEN REWRITE_TAC[CVECTOR_RE_COMPONENT;VECTOR_MUL_COMPONENT;\r
 970     CVECTOR_MUL_COMPONENT;RE_MUL_CX]);;\r
 971 \r
 972 let CVECTOR_IM_MUL = prove\r
 973   (`!a x:complex^N. cvector_im (Cx a % x) = a % cvector_im x`,\r
 974   ONCE_REWRITE_TAC[CART_EQ]\r
 975   THEN REWRITE_TAC[CVECTOR_IM_COMPONENT;VECTOR_MUL_COMPONENT;\r
 976     CVECTOR_MUL_COMPONENT;IM_MUL_CX]);;\r
 977 \r
 978 let CVECTOR_RE_VECTOR_MAP = prove\r
 979   (`!f v:A^N. cvector_re (vector_map f v) = vector_map (Re o f) v`,\r
 980   REWRITE_TAC[cvector_re;VECTOR_MAP_VECTOR_MAP]);;\r
 981 \r
 982 let CVECTOR_IM_VECTOR_MAP = prove\r
 983   (`!f v:A^N. cvector_im (vector_map f v) = vector_map (Im o f) v`,\r
 984   REWRITE_TAC[cvector_im;VECTOR_MAP_VECTOR_MAP]);;\r
 985 \r
 986 let VECTOR_MAP_CVECTOR_RE = prove\r
 987   (`!f:real->A v:complex^N.\r
 988     vector_map f (cvector_re v) = vector_map (f o Re) v`,\r
 989   REWRITE_TAC[cvector_re;VECTOR_MAP_VECTOR_MAP]);;\r
 990 \r
 991 let VECTOR_MAP_CVECTOR_IM = prove\r
 992   (`!f:real->A v:complex^N.\r
 993     vector_map f (cvector_im v) = vector_map (f o Im) v`,\r
 994   REWRITE_TAC[cvector_im;VECTOR_MAP_VECTOR_MAP]);;\r
 995 \r
 996 let CVECTOR_RE_VECTOR_MAP2 = prove\r
 997   (`!f v1:A^N v2:B^N.\r
 998     cvector_re (vector_map2 f v1 v2) = vector_map2 (\x y. Re (f x y)) v1 v2`,\r
 999   REWRITE_TAC[cvector_re;VECTOR_MAP_VECTOR_MAP2]);;\r
1000 \r
1001 let CVECTOR_IM_VECTOR_MAP2 = prove\r
1002   (`!f v1:A^N v2:B^N.\r
1003     cvector_im (vector_map2 f v1 v2) = vector_map2 (\x y. Im (f x y)) v1 v2`,\r
1004   REWRITE_TAC[cvector_im;VECTOR_MAP_VECTOR_MAP2]);;\r
1005 \r
1006 \r
1007 (* ========================================================================= *)\r
1008 (* FLATTENING COMPLEX VECTORS INTO REAL VECTORS                              *)\r
1009 (*                                                                           *)\r
1010 (* Note:                                                                     *)\r
1011 (* Theoretically, the following could be defined more generally for matrices *)\r
1012 (* instead of complex vectors, but this would require a "finite_prod" type   *)\r
1013 (* constructor, which is not available right now, and which, at first sight, *)\r
1014 (* would probably require dependent types.                                   *)\r
1015 (* ========================================================================= *)\r
1016 \r
1017 let cvector_flatten = new_definition\r
1018   `cvector_flatten (v:complex^N) :real^(N,N) finite_sum =\r
1019     pastecart (cvector_re v) (cvector_im v)`;;\r
1020 \r
1021 let FLATTEN_RE_IM_COMPONENT = prove\r
1022   (`!v:complex^N i.\r
1023   1 <= i /\ i <= 2 * dimindex(:N)\r
1024     ==> (cvector_flatten v)$i =\r
1025       if i <= dimindex(:N)\r
1026       then (cvector_re v)$i\r
1027       else (cvector_im v)$(i-dimindex(:N))`,\r
1028   SIMP_TAC[MULT_2;GSYM DIMINDEX_FINITE_SUM;cvector_flatten;pastecart;\r
1029     LAMBDA_BETA]);;\r
1030 \r
1031 let complex_vector = new_definition\r
1032   `complex_vector (v1,v2) :complex^N\r
1033     = vector_map2 (\x y. Cx x + ii * Cx y) v1 v2`;;\r
1034 \r
1035 let COMPLEX_VECTOR_TRANSPOSE = prove(\r
1036   `!v1 v2:real^N.\r
1037   complex_vector (v1,v2) = vector_to_cvector v1 + ii % vector_to_cvector v2`,\r
1038   ONCE_REWRITE_TAC[CART_EQ]\r
1039   THEN SIMP_TAC[complex_vector;CVECTOR_ADD_COMPONENT;CVECTOR_MUL_COMPONENT;\r
1040     VECTOR_TO_CVECTOR_COMPONENT;VECTOR_MAP2_COMPONENT]);;\r
1041 \r
1042 let cvector_unflatten = new_definition\r
1043   `cvector_unflatten (v:real^(N,N) finite_sum) :complex^N\r
1044     = complex_vector (fstcart v, sndcart v)`;;\r
1045 \r
1046 let UNFLATTEN_FLATTEN = prove\r
1047   (`cvector_unflatten o cvector_flatten = I :complex^N -> complex^N`,\r
1048   REWRITE_TAC[FUN_EQ_THM;o_DEF;I_DEF;cvector_flatten;cvector_unflatten;\r
1049     FSTCART_PASTECART;SNDCART_PASTECART;COMPLEX_VECTOR_TRANSPOSE;\r
1050     VECTOR_TO_CVECTOR_CVECTOR_RE_IM]);;\r
1051 \r
1052 let FLATTEN_UNFLATTEN = prove\r
1053   (`cvector_flatten o cvector_unflatten =\r
1054     I :real^(N,N) finite_sum -> real^(N,N) finite_sum`,\r
1055   REWRITE_TAC[FUN_EQ_THM;o_DEF;I_DEF;cvector_flatten;cvector_unflatten;\r
1056     PASTECART_FST_SND;COMPLEX_VECTOR_TRANSPOSE;\r
1057     CVECTOR_RE_VECTOR_TO_CVECTOR_RE_IM;CVECTOR_IM_VECTOR_TO_CVECTOR_RE_IM]);;\r
1058 \r
1059 let FLATTEN_CLINEAR = prove\r
1060   (`!f:complex^N->complex^M.\r
1061     clinear f ==> linear (cvector_flatten o f o cvector_unflatten)`,\r
1062   REWRITE_TAC[clinear;linear;cvector_flatten;cvector_unflatten;o_DEF;\r
1063     FSTCART_ADD;SNDCART_ADD;PASTECART_ADD;complex_vector;GSYM PASTECART_CMUL]\r
1064   THEN REPEAT STRIP_TAC THEN REPEAT (AP_TERM_TAC ORELSE MK_COMB_TAC)\r
1065   THEN REWRITE_TAC(map GSYM [CVECTOR_RE_ADD;CVECTOR_IM_ADD;CVECTOR_RE_MUL;\r
1066     CVECTOR_IM_MUL])\r
1067   THEN AP_TERM_TAC THEN ASSUM_LIST (REWRITE_TAC o map GSYM) \r
1068   THEN AP_TERM_TAC THEN ONCE_REWRITE_TAC[CART_EQ]\r
1069   THEN SIMP_TAC[VECTOR_MAP2_COMPONENT;VECTOR_ADD_COMPONENT;\r
1070     CVECTOR_ADD_COMPONENT;CX_ADD;VECTOR_MUL_COMPONENT;CVECTOR_MUL_COMPONENT;\r
1071     FSTCART_CMUL;SNDCART_CMUL;CX_MUL]\r
1072   THEN SIMPLE_COMPLEX_ARITH_TAC);;\r
1073 \r
1074 let FLATTEN_MAP = prove\r
1075   (`!f g.\r
1076     f = vector_map g\r
1077       ==> !x:complex^N.\r
1078         cvector_flatten (vector_map f x) = vector_map g (cvector_flatten x)`,\r
1079   SIMP_TAC[cvector_flatten;CVECTOR_RE_VECTOR_MAP;CVECTOR_IM_VECTOR_MAP;\r
1080     GSYM PASTECART_VECTOR_MAP;VECTOR_MAP_CVECTOR_RE;VECTOR_MAP_CVECTOR_IM;\r
1081     o_DEF;IM_DEF;RE_DEF;VECTOR_MAP_COMPONENT]);;\r
1082 \r
1083 let FLATTEN_NEG = prove\r
1084   (`!x:complex^N. cvector_flatten (--x) = --(cvector_flatten x)`,\r
1085   REWRITE_TAC[cvector_neg;MATCH_MP FLATTEN_MAP COMPLEX_NEG_IS_A_MAP]\r
1086   THEN REWRITE_TAC[VECTOR_NEG_IS_A_MAP]);;\r
1087 \r
1088 let CVECTOR_NEG_ALT = prove\r
1089   (`!x:complex^N. --x = cvector_unflatten (--(cvector_flatten x))`,\r
1090   REWRITE_TAC[GSYM FLATTEN_NEG;\r
1091     REWRITE_RULE[o_DEF;FUN_EQ_THM;I_DEF] UNFLATTEN_FLATTEN]);;\r
1092 \r
1093 let FLATTEN_MAP2 = prove(\r
1094   `!f g.\r
1095     f = vector_map2 g ==>\r
1096       !x y:complex^N.\r
1097         cvector_flatten (vector_map2 f x y) =\r
1098           vector_map2 g (cvector_flatten x) (cvector_flatten y)`,\r
1099   SIMP_TAC[cvector_flatten;CVECTOR_RE_VECTOR_MAP2;CVECTOR_IM_VECTOR_MAP2;\r
1100     CVECTOR_RE_VECTOR_MAP2;GSYM PASTECART_VECTOR_MAP2]\r
1101   THEN REWRITE_TAC[cvector_re;cvector_im;VECTOR_MAP2_LVECTOR_MAP;\r
1102     VECTOR_MAP2_RVECTOR_MAP]\r
1103   THEN REPEAT MK_COMB_TAC\r
1104   THEN REWRITE_TAC[FUN_EQ_THM;IM_DEF;RE_DEF;VECTOR_MAP2_COMPONENT;o_DEF]);;\r
1105 \r
1106 let FLATTEN_ADD = prove\r
1107   (`!x y:complex^N.\r
1108     cvector_flatten (x+y) = cvector_flatten x + cvector_flatten y`,\r
1109   REWRITE_TAC[cvector_add;MATCH_MP FLATTEN_MAP2 COMPLEX_ADD_IS_A_MAP]\r
1110   THEN REWRITE_TAC[VECTOR_ADD_IS_A_MAP]);;\r
1111 \r
1112 let CVECTOR_ADD_ALT = prove\r
1113   (`!x y:complex^N.\r
1114     x+y = cvector_unflatten (cvector_flatten x + cvector_flatten y)`,\r
1115   REWRITE_TAC[GSYM FLATTEN_ADD;\r
1116     REWRITE_RULE[o_DEF;FUN_EQ_THM;I_DEF] UNFLATTEN_FLATTEN]);;\r
1117 \r
1118 let FLATTEN_SUB = prove\r
1119   (`!x y:complex^N. cvector_flatten (x-y) = cvector_flatten x - cvector_flatten y`,\r
1120   REWRITE_TAC[cvector_sub;MATCH_MP FLATTEN_MAP2 COMPLEX_SUB_IS_A_MAP]\r
1121   THEN REWRITE_TAC[VECTOR_SUB_IS_A_MAP]);;\r
1122 \r
1123 let CVECTOR_SUB_ALT = prove\r
1124   (`!x y:complex^N. x-y = cvector_unflatten (cvector_flatten x - cvector_flatten y)`,\r
1125   REWRITE_TAC[GSYM FLATTEN_SUB;\r
1126     REWRITE_RULE[o_DEF;FUN_EQ_THM;I_DEF] UNFLATTEN_FLATTEN]);;\r
1127 \r
1128 \r
1129 (* ========================================================================= *)\r
1130 (* CONJUGATE VECTOR.                                                         *)\r
1131 (* ========================================================================= *)\r
1132 \r
1133 let cvector_cnj = new_definition\r
1134   `cvector_cnj : complex^N->complex^N = vector_map cnj`;;\r
1135 \r
1136 let CVECTOR_MAP_PROPERTY thm =\r
1137   VECTOR_MAP_PROPERTY thm [cvector_zero;cvector_add;cvector_sub;cvector_neg;\r
1138   cvector_mul;cvector_cnj;cvector_re;cvector_im];;\r
1139 \r
1140 let CVECTOR_CNJ_ADD = CVECTOR_MAP_PROPERTY\r
1141   `!x y:complex^N. cvector_cnj (x+y) = cvector_cnj x + cvector_cnj y`\r
1142   CNJ_ADD;;\r
1143 \r
1144 let CVECTOR_CNJ_SUB = CVECTOR_MAP_PROPERTY\r
1145   `!x y:complex^N. cvector_cnj (x-y) = cvector_cnj x - cvector_cnj y`\r
1146   CNJ_SUB;;\r
1147 \r
1148 let CVECTOR_CNJ_NEG = CVECTOR_MAP_PROPERTY\r
1149   `!x:complex^N. cvector_cnj (--x) = --(cvector_cnj x)`\r
1150   CNJ_NEG;;\r
1151 \r
1152 let CVECTOR_RE_CNJ = CVECTOR_MAP_PROPERTY\r
1153   `!x:complex^N. cvector_re (cvector_cnj x) = cvector_re x`\r
1154   RE_CNJ;;\r
1155 \r
1156 let CVECTOR_IM_CNJ = prove\r
1157   (`!x:complex^N. cvector_im (cvector_cnj x) = --(cvector_im x)`,\r
1158   VECTOR_MAP_PROPERTY_TAC[cvector_im;cvector_cnj;VECTOR_NEG_IS_A_MAP] IM_CNJ);;\r
1159 \r
1160 let CVECTOR_CNJ_CNJ = CVECTOR_MAP_PROPERTY\r
1161   `!x:complex^N. cvector_cnj (cvector_cnj x) = x`\r
1162   CNJ_CNJ;;\r
1163 \r
1164 \r
1165 (* ========================================================================= *)\r
1166 (* CROSS PRODUCTS IN COMPLEX^3.                                              *)\r
1167 (* ========================================================================= *)\r
1168 \r
1169 prioritize_vector();;\r
1170 \r
1171 parse_as_infix("ccross",(20,"right"));;\r
1172 \r
1173 let ccross = new_definition\r
1174   `((ccross):complex^3 -> complex^3 -> complex^3) x y = vector [\r
1175     x$2 * y$3 - x$3 * y$2;\r
1176     x$3 * y$1 - x$1 * y$3;\r
1177     x$1 * y$2 - x$2 * y$1\r
1178   ]`;; \r
1179 \r
1180 let CCROSS_COMPONENT = prove \r
1181   (`!x y:complex^3.\r
1182   (x ccross y)$1 = x$2 * y$3 - x$3 * y$2\r
1183   /\ (x ccross y)$2 = x$3 * y$1 - x$1 * y$3\r
1184   /\ (x ccross y)$3 = x$1 * y$2 - x$2 * y$1`,\r
1185   REWRITE_TAC[ccross;VECTOR_3]);;\r
1186 \r
1187 (* simple handy instantiation of CART_EQ for dimension 3*)\r
1188 let CART_EQ3 = prove\r
1189   (`!x y:complex^3. x = y <=> x$1 = y$1 /\ x$2 = y$2 /\ x$3 = y$3`,\r
1190   GEN_REWRITE_TAC (PATH_CONV "rbrblr") [CART_EQ]\r
1191   THEN REWRITE_TAC[DIMINDEX_3;FORALL_3]);;\r
1192 \r
1193 let CCROSS_TAC lemmas =\r
1194   REWRITE_TAC(CART_EQ3::CCROSS_COMPONENT::lemmas)\r
1195   THEN SIMPLE_COMPLEX_ARITH_TAC;;\r
1196 \r
1197 let CCROSS_LZERO = prove \r
1198   (`!x:complex^3. cvector_zero ccross x = cvector_zero`,\r
1199   CCROSS_TAC[CVECTOR_ZERO_COMPONENT]);;\r
1200 \r
1201 let CCROSS_RZERO = prove \r
1202   (`!x:complex^3. x ccross cvector_zero = cvector_zero`,\r
1203   CCROSS_TAC[CVECTOR_ZERO_COMPONENT]);;\r
1204 \r
1205 let CCROSS_SKEW = prove \r
1206   (`!x y:complex^3. (x ccross y) = --(y ccross x)`,\r
1207   CCROSS_TAC[CVECTOR_NEG_COMPONENT]);;\r
1208 \r
1209 let CCROSS_REFL = prove \r
1210   (`!x:complex^3. x ccross x = cvector_zero`,\r
1211   CCROSS_TAC[CVECTOR_ZERO_COMPONENT]);;\r
1212 \r
1213 let CCROSS_LADD = prove\r
1214   (`!x y z:complex^3. (x + y) ccross z = (x ccross z) + (y ccross z)`,\r
1215   CCROSS_TAC[CVECTOR_ADD_COMPONENT]);;\r
1216 \r
1217 let CCROSS_RADD = prove \r
1218   (`!x y z:complex^3. x ccross(y + z) = (x ccross y) + (x ccross z)`,\r
1219   CCROSS_TAC[CVECTOR_ADD_COMPONENT]);;\r
1220 \r
1221 let CCROSS_LMUL = prove \r
1222   (`!c x y:complex^3. (c % x) ccross y = c % (x ccross y)`,\r
1223   CCROSS_TAC[CVECTOR_MUL_COMPONENT]);;\r
1224 \r
1225 let CCROSS_RMUL = prove \r
1226   (`!c x y:complex^3. x ccross (c % y) = c % (x ccross y)`,\r
1227   CCROSS_TAC[CVECTOR_MUL_COMPONENT]);;\r
1228 \r
1229 let CCROSS_LNEG = prove \r
1230   (`!x y:complex^3. (--x) ccross y = --(x ccross y)`,\r
1231   CCROSS_TAC[CVECTOR_NEG_COMPONENT]);;\r
1232 \r
1233 let CCROSS_RNEG = prove \r
1234   (`!x y:complex^3. x ccross (--y) = --(x ccross y)`,\r
1235   CCROSS_TAC[CVECTOR_NEG_COMPONENT]);;\r
1236 \r
1237 let CCROSS_JACOBI = prove\r
1238  (`!(x:complex^3) y z.\r
1239     x ccross (y ccross z) + y ccross (z ccross x) + z ccross (x ccross y) =\r
1240       cvector_zero`,\r
1241   REWRITE_TAC[CART_EQ3]\r
1242   THEN REWRITE_TAC[CVECTOR_ADD_COMPONENT;CCROSS_COMPONENT;\r
1243     CVECTOR_ZERO_COMPONENT] THEN SIMPLE_COMPLEX_ARITH_TAC);;\r
1244 \r
1245 \r
1246 (* ========================================================================= *)\r
1247 (* DOT PRODUCTS IN COMPLEX^N                                                 *)\r
1248 (*                                                                           *)\r
1249 (* Only difference with the real case:                                       *)\r
1250 (* we take the conjugate of the 2nd argument                                 *)\r
1251 (* ========================================================================= *)\r
1252 \r
1253 prioritize_complex();;\r
1254 \r
1255 parse_as_infix("cdot",(20,"right"));;\r
1256 \r
1257 let cdot = new_definition\r
1258   `(cdot) (x:complex^N) (y:complex^N) =\r
1259     vsum (1..dimindex(:N)) (\i. x$i * cnj(y$i))`;;\r
1260 \r
1261 (* The dot product is symmetric MODULO the conjugate *)\r
1262 let CDOT_SYM = prove\r
1263   (`!x:complex^N y. x cdot y = cnj (y cdot x)`,\r
1264   REWRITE_TAC[cdot]\r
1265   THEN REWRITE_TAC[MATCH_MP (SPEC_ALL CNJ_VSUM) (SPEC `dimindex (:N)` (GEN_ALL\r
1266     (CONJUNCT1 (SPEC_ALL (REWRITE_RULE[HAS_SIZE] HAS_SIZE_NUMSEG_1)))))]\r
1267   THEN REWRITE_TAC[CNJ_MUL;CNJ_CNJ;COMPLEX_MUL_SYM]);;\r
1268 \r
1269 let REAL_CDOT_SELF = prove\r
1270   (`!x:complex^N. real(x cdot x)`,\r
1271   REWRITE_TAC[REAL_CNJ;GSYM CDOT_SYM]);;\r
1272 \r
1273 (* The following theorems are usual axioms of the hermitian dot product, they are proved later on.\r
1274  * let CDOT_SELF_POS = prove(`!x:complex^N. &0 <= real_of_complex (x cdot x)`, ...\r
1275  * let CDOT_EQ_0 = prove(`!x:complex^N. x cdot x = Cx(&0) <=> x = cvector_zero`\r
1276  *)\r
1277 \r
1278 let CDOT_LADD = prove\r
1279   (`!x:complex^N y z. (x + y) cdot z = (x cdot z) + (y cdot z)`,\r
1280   REWRITE_TAC[cdot]\r
1281   THEN REWRITE_TAC[MATCH_MP (GSYM VSUM_ADD) (SPEC `dimindex (:N)` (GEN_ALL\r
1282     (CONJUNCT1 (SPEC_ALL (REWRITE_RULE[HAS_SIZE] HAS_SIZE_NUMSEG_1)))))]\r
1283   THEN REPEAT GEN_TAC THEN MATCH_MP_TAC VSUM_EQ THEN GEN_TAC THEN DISCH_TAC\r
1284   THEN REWRITE_TAC[FUN_EQ_THM]\r
1285   THEN REWRITE_TAC[SPECL [`(x:real^2^N)$(x':num)`;`(y:real^2^N)$(x':num)`;\r
1286     `cnj ((z:real^2^N)$(x':num))`] (GSYM COMPLEX_ADD_RDISTRIB)]\r
1287   THEN REWRITE_TAC[CVECTOR_ADD_COMPONENT]);;\r
1288 \r
1289 let CDOT_RADD = prove\r
1290   (`!x:complex^N y z. x cdot (y + z) = (x cdot y) + (x cdot z)`,\r
1291   REWRITE_TAC[cdot]\r
1292   THEN REWRITE_TAC[MATCH_MP (GSYM VSUM_ADD) (SPEC `dimindex (:N)` (GEN_ALL\r
1293     (CONJUNCT1 (SPEC_ALL (REWRITE_RULE[HAS_SIZE] HAS_SIZE_NUMSEG_1)))))]\r
1294   THEN REPEAT GEN_TAC THEN MATCH_MP_TAC VSUM_EQ THEN GEN_TAC THEN DISCH_TAC\r
1295   THEN REWRITE_TAC[FUN_EQ_THM]\r
1296   THEN REWRITE_TAC[SPECL [`(x:real^2^N)$(x':num)`; `cnj((y:real^2^N)$(x':num))`;\r
1297   `cnj ((z:real^2^N)$(x':num))`] (GSYM COMPLEX_ADD_LDISTRIB)]\r
1298   THEN REWRITE_TAC[CNJ_ADD; CVECTOR_ADD_COMPONENT]);;\r
1299 \r
1300 let CDOT_LSUB = prove\r
1301   (`!x:complex^N y z. (x - y) cdot z = (x cdot z) - (y cdot z)`,\r
1302   REWRITE_TAC[cdot]\r
1303   THEN REWRITE_TAC[MATCH_MP (GSYM VSUM_SUB) (SPEC `dimindex (:N)` (GEN_ALL\r
1304     (CONJUNCT1 (SPEC_ALL (REWRITE_RULE[HAS_SIZE] HAS_SIZE_NUMSEG_1)))))]\r
1305   THEN REPEAT GEN_TAC THEN MATCH_MP_TAC VSUM_EQ THEN GEN_TAC THEN DISCH_TAC\r
1306   THEN REWRITE_TAC[FUN_EQ_THM]\r
1307   THEN REWRITE_TAC[SPECL [`(x:real^2^N)$(x':num)`; `(y:real^2^N)$(x':num)`;\r
1308     `cnj ((z:real^2^N)$(x':num))`] (GSYM COMPLEX_SUB_RDISTRIB)]\r
1309   THEN REWRITE_TAC[CVECTOR_SUB_COMPONENT]);;\r
1310 \r
1311 let CDOT_RSUB = prove\r
1312   (`!x:complex^N y z. x cdot (y - z) = (x cdot y) - (x cdot z)`,\r
1313   REWRITE_TAC[cdot]\r
1314   THEN REWRITE_TAC[MATCH_MP (GSYM VSUM_SUB) (SPEC `dimindex (:N)` (GEN_ALL\r
1315     (CONJUNCT1 (SPEC_ALL (REWRITE_RULE[HAS_SIZE] HAS_SIZE_NUMSEG_1)))))]\r
1316   THEN REPEAT GEN_TAC THEN MATCH_MP_TAC VSUM_EQ THEN GEN_TAC THEN DISCH_TAC\r
1317   THEN REWRITE_TAC[FUN_EQ_THM]\r
1318   THEN REWRITE_TAC[SPECL [`(x:real^2^N)$(x':num)`; `cnj((y:real^2^N)$(x':num))`;\r
1319     `cnj ((z:real^2^N)$(x':num))`] (GSYM COMPLEX_SUB_LDISTRIB)]\r
1320   THEN REWRITE_TAC[CNJ_SUB; CVECTOR_SUB_COMPONENT]);;\r
1321 \r
1322 let CDOT_LMUL = prove\r
1323   (`!c:complex x:complex^N y. (c % x) cdot y = c * (x cdot y)`,\r
1324   REWRITE_TAC[cdot]\r
1325   THEN REWRITE_TAC[MATCH_MP (GSYM VSUM_COMPLEX_LMUL) (SPEC `dimindex (:N)`\r
1326     (GEN_ALL (CONJUNCT1 (SPEC_ALL (REWRITE_RULE[HAS_SIZE]\r
1327     HAS_SIZE_NUMSEG_1)))))]\r
1328   THEN REWRITE_TAC[CVECTOR_MUL_COMPONENT; GSYM COMPLEX_MUL_ASSOC]);;\r
1329 \r
1330 let CDOT_RMUL = prove\r
1331   (`!c:complex x:complex^N x y. x cdot (c % y) = cnj c * (x cdot y)`,\r
1332   REWRITE_TAC[cdot]\r
1333   THEN REWRITE_TAC[MATCH_MP (GSYM VSUM_COMPLEX_LMUL) (SPEC `dimindex (:N)`\r
1334     (GEN_ALL (CONJUNCT1 (SPEC_ALL (REWRITE_RULE[HAS_SIZE]\r
1335     HAS_SIZE_NUMSEG_1)))))]\r
1336   THEN REWRITE_TAC[CVECTOR_MUL_COMPONENT; CNJ_MUL; COMPLEX_MUL_AC]);;\r
1337 \r
1338 let CDOT_LNEG = prove\r
1339   (`!x:complex^N y. (--x) cdot y = --(x cdot y)`,\r
1340   REWRITE_TAC[cdot] THEN ONCE_REWRITE_TAC[COMPLEX_NEG_MINUS1]\r
1341   THEN REWRITE_TAC[MATCH_MP (GSYM VSUM_COMPLEX_LMUL) (SPEC `dimindex (:N)`\r
1342     (GEN_ALL (CONJUNCT1 (SPEC_ALL (REWRITE_RULE[HAS_SIZE]\r
1343     HAS_SIZE_NUMSEG_1)))))]\r
1344   THEN REWRITE_TAC[CVECTOR_NEG_COMPONENT] THEN ONCE_REWRITE_TAC[GSYM\r
1345     COMPLEX_NEG_MINUS1] THEN REWRITE_TAC[COMPLEX_NEG_LMUL]);;\r
1346 \r
1347 let CDOT_RNEG = prove\r
1348   (`!x:complex^N y. x cdot (--y) = --(x cdot y)`,\r
1349   REWRITE_TAC[cdot] THEN ONCE_REWRITE_TAC[COMPLEX_NEG_MINUS1]\r
1350   THEN REWRITE_TAC[MATCH_MP (GSYM VSUM_COMPLEX_LMUL) (SPEC `dimindex (:N)`\r
1351     (GEN_ALL (CONJUNCT1 (SPEC_ALL (REWRITE_RULE[HAS_SIZE]\r
1352     HAS_SIZE_NUMSEG_1)))))]\r
1353   THEN ONCE_REWRITE_TAC[GSYM COMPLEX_NEG_MINUS1]\r
1354   THEN REWRITE_TAC[CVECTOR_NEG_COMPONENT; CNJ_NEG; COMPLEX_NEG_RMUL]);;\r
1355 \r
1356 let CDOT_LZERO = prove\r
1357   (`!x:complex^N. cvector_zero cdot x = Cx (&0)`,\r
1358   REWRITE_TAC[cdot] THEN REWRITE_TAC[CVECTOR_ZERO_COMPONENT]\r
1359   THEN REWRITE_TAC[COMPLEX_MUL_LZERO; GSYM COMPLEX_VEC_0; VSUM_0]);;\r
1360 \r
1361 let CNJ_ZERO = prove(\r
1362   `cnj (Cx(&0)) = Cx(&0)`,\r
1363   REWRITE_TAC[cnj;RE_CX;IM_CX;CX_DEF;REAL_NEG_0]);;\r
1364 \r
1365 let CDOT_RZERO = prove(\r
1366   `!x:complex^N. x cdot cvector_zero = Cx (&0)`,\r
1367   REWRITE_TAC[cdot] THEN REWRITE_TAC[CVECTOR_ZERO_COMPONENT]\r
1368   THEN REWRITE_TAC[CNJ_ZERO]\r
1369   THEN REWRITE_TAC[COMPLEX_MUL_RZERO;GSYM COMPLEX_VEC_0;VSUM_0]);;\r
1370 \r
1371 (* Cauchy Schwarz inequality: proved later on \r
1372  * let CDOT_CAUCHY_SCHWARZ = prove (`!x y:complex^N. norm (x cdot y) pow 2 <= cnorm2 x * cnorm2 y`,\r
1373  * let CDOT_CAUCHY_SCHWARZ_EQUAL = prove(`!x y:complex^N. norm (x cdot y) pow 2 = cnorm2 x * cnorm2 y <=> collinear_cvectors x y`,\r
1374 *)\r
1375 \r
1376 let CDOT3 = prove\r
1377   (`!x y:complex^3.\r
1378     x cdot y = (x$1 * cnj (y$1) + x$2 * cnj (y$2) + x$3 * cnj (y$3))`,\r
1379   REWRITE_TAC[cdot] THEN SIMP_TAC [DIMINDEX_3] THEN REWRITE_TAC[VSUM_3]);;\r
1380 \r
1381 let ADD_CDOT_SYM = prove(\r
1382   `!x y:complex^N. x cdot y + y cdot x = Cx(&2 * Re(x cdot y))`,\r
1383   MESON_TAC[CDOT_SYM;COMPLEX_ADD_CNJ]);;\r
1384 \r
1385 \r
1386 (* ========================================================================= *)\r
1387 (* RELATION WITH REAL DOT AND CROSS PRODUCTS                                 *)\r
1388 (* ========================================================================= *)\r
1389 \r
1390 let CCROSS_LREAL = prove\r
1391   (`!r c.\r
1392     (vector_to_cvector r) ccross c =\r
1393       vector_to_cvector (r cross (cvector_re c)) \r
1394       + ii % (vector_to_cvector (r cross (cvector_im c)))`,\r
1395   REWRITE_TAC[CART_EQ3;CVECTOR_ADD_COMPONENT;CVECTOR_MUL_COMPONENT;\r
1396     VECTOR_TO_CVECTOR_COMPONENT;CCROSS_COMPONENT;CROSS_COMPONENTS;\r
1397     CVECTOR_RE_COMPONENT;CVECTOR_IM_COMPONENT;complex_mul;RE_CX;IM_CX;CX_DEF;\r
1398     complex_sub;complex_neg;complex_add;RE;IM;RE_II;IM_II]\r
1399   THEN REPEAT STRIP_TAC THEN AP_TERM_TAC THEN REWRITE_TAC[PAIR_EQ]\r
1400   THEN ARITH_TAC);;\r
1401 \r
1402 let CCROSS_RREAL = prove\r
1403   (`!r c.\r
1404     c ccross (vector_to_cvector r) =\r
1405       vector_to_cvector ((cvector_re c) cross r)\r
1406       + ii % (vector_to_cvector ((cvector_im c) cross r))`,\r
1407   REWRITE_TAC[CART_EQ3;CVECTOR_ADD_COMPONENT;CVECTOR_MUL_COMPONENT;\r
1408     VECTOR_TO_CVECTOR_COMPONENT;CCROSS_COMPONENT;CROSS_COMPONENTS;\r
1409     CVECTOR_RE_COMPONENT;CVECTOR_IM_COMPONENT;complex_mul;RE_CX;IM_CX;CX_DEF;\r
1410     complex_sub;complex_neg;complex_add;RE;IM;RE_II;IM_II]\r
1411   THEN REPEAT STRIP_TAC THEN AP_TERM_TAC THEN REWRITE_TAC[PAIR_EQ]\r
1412   THEN ARITH_TAC);;\r
1413 \r
1414 let CDOT_LREAL = prove\r
1415   (`!r c.\r
1416     (vector_to_cvector r) cdot c =\r
1417       Cx (r dot (cvector_re c)) - ii * Cx (r dot (cvector_im c))`,\r
1418   REWRITE_TAC[cdot; dot; VECTOR_TO_CVECTOR_COMPONENT;CVECTOR_RE_COMPONENT;\r
1419     CVECTOR_IM_COMPONENT] THEN REPEAT GEN_TAC\r
1420   THEN GEN_REWRITE_TAC (RATOR_CONV o ONCE_DEPTH_CONV) [COMPLEX_EXPAND]\r
1421   THEN REWRITE_TAC[MATCH_MP RE_VSUM (SPEC `dimindex (:N)` (GEN_ALL (CONJUNCT1\r
1422     (SPEC_ALL (REWRITE_RULE[HAS_SIZE] HAS_SIZE_NUMSEG_1)))))]\r
1423   THEN REWRITE_TAC[MATCH_MP (IM_VSUM) (SPEC `dimindex (:N)` (GEN_ALL\r
1424     (CONJUNCT1 (SPEC_ALL (REWRITE_RULE[HAS_SIZE]\r
1425       HAS_SIZE_NUMSEG_1)))))]\r
1426   THEN REWRITE_TAC[RE_MUL_CX;RE_CNJ;IM_MUL_CX;IM_CNJ]\r
1427   THEN REWRITE_TAC[COMPLEX_POLY_NEG_CLAUSES] THEN REWRITE_TAC[COMPLEX_MUL_AC]\r
1428   THEN REWRITE_TAC[COMPLEX_MUL_ASSOC] THEN REWRITE_TAC[GSYM CX_MUL]\r
1429   THEN REWRITE_TAC[GSYM SUM_LMUL]\r
1430   THEN REWRITE_TAC[GSYM REAL_NEG_MINUS1;GSYM REAL_MUL_RNEG]);;\r
1431 \r
1432 let CDOT_RREAL = prove\r
1433   (`!r c.\r
1434     c cdot (vector_to_cvector r) = \r
1435       Cx ((cvector_re c) dot r) + ii * Cx ((cvector_im c) dot r)`,\r
1436   REWRITE_TAC[cdot; dot; VECTOR_TO_CVECTOR_COMPONENT;CVECTOR_RE_COMPONENT;\r
1437     CVECTOR_IM_COMPONENT]\r
1438   THEN REPEAT GEN_TAC\r
1439   THEN GEN_REWRITE_TAC (RATOR_CONV o ONCE_DEPTH_CONV) [COMPLEX_EXPAND]\r
1440   THEN REWRITE_TAC[MATCH_MP RE_VSUM (SPEC `dimindex (:N)` (GEN_ALL (CONJUNCT1\r
1441     (SPEC_ALL (REWRITE_RULE[HAS_SIZE] HAS_SIZE_NUMSEG_1)))))]\r
1442   THEN REWRITE_TAC[MATCH_MP IM_VSUM (SPEC `dimindex (:N)` (GEN_ALL (CONJUNCT1\r
1443     (SPEC_ALL (REWRITE_RULE[HAS_SIZE] HAS_SIZE_NUMSEG_1)))))]\r
1444   THEN REWRITE_TAC[CNJ_CX]\r
1445   THEN REWRITE_TAC[RE_MUL_CX;RE_CNJ;IM_MUL_CX;IM_CNJ]);;\r
1446 \r
1447 \r
1448 (* ========================================================================= *)\r
1449 (* NORM, UNIT VECTORS.                                                       *)\r
1450 (* ========================================================================= *)\r
1451 \r
1452 let cnorm2 = new_definition\r
1453   `cnorm2 (v:complex^N) = real_of_complex (v cdot v)`;;\r
1454 \r
1455 let CX_CNORM2 = prove\r
1456   (`!v:complex^N. Cx(cnorm2 v) = v cdot v`,\r
1457   SIMP_TAC[cnorm2;REAL_CDOT_SELF;REAL_OF_COMPLEX]);;\r
1458 \r
1459 let CNORM2_CVECTOR_ZERO = prove\r
1460   (`cnorm2 (cvector_zero:complex^N) = &0`,\r
1461   REWRITE_TAC[cnorm2;CDOT_RZERO;REAL_OF_COMPLEX_CX]);;\r
1462 \r
1463 let CNORM2_MODULUS = prove\r
1464   (`!x:complex^N. cnorm2 x = (vector_map norm x) dot (vector_map norm x)`,\r
1465   REWRITE_TAC[cnorm2;cdot;COMPLEX_MUL_CNJ;COMPLEX_POW_2;GSYM CX_MUL;\r
1466     VSUM_CX_NUMSEG;dot;VECTOR_MAP_COMPONENT;REAL_OF_COMPLEX_CX]);;\r
1467 \r
1468 let CNORM2_EQ_0 = prove\r
1469   (`!x:complex^N. cnorm2 x = &0 <=> x = cvector_zero`,\r
1470   REWRITE_TAC[CNORM2_MODULUS;CX_INJ;DOT_EQ_0] THEN GEN_TAC\r
1471   THEN GEN_REWRITE_TAC (RATOR_CONV o DEPTH_CONV) [CART_EQ]\r
1472   THEN REWRITE_TAC[VEC_COMPONENT;VECTOR_MAP_COMPONENT;COMPLEX_NORM_ZERO]\r
1473   THEN GEN_REWRITE_TAC (RAND_CONV o DEPTH_CONV) [CART_EQ]\r
1474   THEN REWRITE_TAC[CVECTOR_ZERO_COMPONENT]);;\r
1475 \r
1476 let CDOT_EQ_0 = prove\r
1477   (`!x:complex^N. x cdot x = Cx(&0) <=> x = cvector_zero`,\r
1478   SIMP_TAC[TAUT `(p<=>q) <=> ((p==>q) /\ (q==>p))`;CDOT_LZERO]\r
1479   THEN GEN_TAC THEN DISCH_THEN (MP_TAC o MATCH_MP (MESON[REAL_OF_COMPLEX_CX]\r
1480     `x = Cx y ==> real_of_complex x = y`))\r
1481   THEN REWRITE_TAC[GSYM cnorm2;CNORM2_EQ_0]);;\r
1482 \r
1483 let CNORM2_POS = prove\r
1484   (`!x:complex^N. &0 <= cnorm2 x`, REWRITE_TAC[CNORM2_MODULUS;DOT_POS_LE]);;\r
1485 \r
1486 let CDOT_SELF_POS = prove\r
1487   (`!x:complex^N. &0 <= real_of_complex (x cdot x)`,\r
1488   REWRITE_TAC[GSYM cnorm2;CNORM2_POS]);;\r
1489 \r
1490 let CNORM2_MUL = prove\r
1491   (`!a x:complex^N. cnorm2 (a % x) = (norm a) pow 2 * cnorm2 x`,\r
1492   SIMP_TAC[cnorm2;CDOT_LMUL;CDOT_RMUL;\r
1493     SIMPLE_COMPLEX_ARITH `x * cnj x * y = (x * cnj x) * y`;COMPLEX_MUL_CNJ;\r
1494     REAL_OF_COMPLEX_CX;REAL_OF_COMPLEX_MUL;REAL_CX;REAL_CDOT_SELF;\r
1495     GSYM CX_POW]);;\r
1496 \r
1497 let CNORM2_NORM2_2 = prove\r
1498   (`!x y:real^N.\r
1499     cnorm2 (vector_to_cvector x + ii % vector_to_cvector y) =\r
1500       norm x pow 2 + norm y pow 2`,\r
1501   REWRITE_TAC[cnorm2;vector_norm;cdot;CVECTOR_ADD_COMPONENT;\r
1502     CVECTOR_MUL_COMPONENT;VECTOR_TO_CVECTOR_COMPONENT;CNJ_ADD;CNJ_CX;CNJ_MUL;\r
1503     CNJ_II;COMPLEX_ADD_RDISTRIB;COMPLEX_ADD_LDISTRIB;\r
1504     SIMPLE_COMPLEX_ARITH\r
1505       `(x*x+x*(--ii)*y)+(ii*y)*x+(ii*y)*(--ii)*y = x*x-(ii*ii)*y*y`]\r
1506   THEN REWRITE_TAC[GSYM COMPLEX_POW_2;COMPLEX_POW_II_2;\r
1507     SIMPLE_COMPLEX_ARITH `x-(--Cx(&1))*y = x+y`]\r
1508   THEN SIMP_TAC[MESON[CARD_NUMSEG_1;HAS_SIZE_NUMSEG_1;FINITE_HAS_SIZE]\r
1509     `FINITE (1..dimindex(:N))`;VSUM_ADD;GSYM CX_POW;VSUM_CX;GSYM dot;\r
1510     REAL_POW_2;GSYM dot]\r
1511   THEN SIMP_TAC[GSYM CX_ADD;REAL_OF_COMPLEX_CX;GSYM REAL_POW_2;DOT_POS_LE;\r
1512     SQRT_POW_2]);;\r
1513 \r
1514 let CNORM2_NORM2 = prove\r
1515   (`!v:complex^N.\r
1516     cnorm2 v = norm (cvector_re v) pow 2 + norm (cvector_im v) pow 2`,\r
1517   GEN_TAC THEN GEN_REWRITE_TAC (RATOR_CONV o ONCE_DEPTH_CONV) [GSYM\r
1518     VECTOR_TO_CVECTOR_CVECTOR_RE_IM] THEN REWRITE_TAC[CNORM2_NORM2_2]);;\r
1519 \r
1520 let CNORM2_ALT = prove\r
1521   (`!x:complex^N. cnorm2 x = norm (x cdot x)`,\r
1522   SIMP_TAC[cnorm2;REAL_OF_COMPLEX_NORM;REAL_CDOT_SELF;EQ_SYM_EQ;REAL_ABS_REFL;\r
1523     REWRITE_RULE[cnorm2] CNORM2_POS]);;\r
1524 \r
1525 let CNORM2_SUB = prove\r
1526   (`!x y:complex^N. cnorm2 (x-y) = cnorm2 (y-x)`,\r
1527   REWRITE_TAC[cnorm2;CDOT_LSUB;CDOT_RSUB] THEN REPEAT GEN_TAC THEN AP_TERM_TAC\r
1528   THEN SIMPLE_COMPLEX_ARITH_TAC);;\r
1529 \r
1530 let CNORM2_VECTOR_TO_CVECTOR = prove\r
1531   (`!x:real^N. cnorm2 (vector_to_cvector x) = norm x pow 2`,\r
1532   REWRITE_TAC[CNORM2_ALT;CDOT_RREAL;CVECTOR_RE_VECTOR_TO_CVECTOR;\r
1533     CVECTOR_IM_VECTOR_TO_CVECTOR;DOT_LZERO;COMPLEX_MUL_RZERO;COMPLEX_ADD_RID;\r
1534     DOT_SQUARE_NORM;CX_POW;COMPLEX_NORM_POW;COMPLEX_NORM_CX;REAL_POW2_ABS]);;\r
1535 \r
1536 let cnorm = new_definition\r
1537   `cnorm :complex^N->real = sqrt o cnorm2`;;\r
1538 \r
1539 overload_interface ("norm",`cnorm:complex^N->real`);;\r
1540 \r
1541 let CNORM_CVECTOR_ZERO = prove\r
1542   (`norm (cvector_zero:complex^N) = &0`,\r
1543   REWRITE_TAC[cnorm;CNORM2_CVECTOR_ZERO;o_DEF;SQRT_0]);;\r
1544 \r
1545 let CNORM_POW_2 = prove\r
1546   (`!x:complex^N. norm x pow 2 = cnorm2 x`, \r
1547   SIMP_TAC[cnorm;o_DEF;SQRT_POW_2;CNORM2_POS]);;\r
1548 \r
1549 let CNORM_NORM_2 = prove\r
1550   (`!x y:real^N.\r
1551     norm (vector_to_cvector x + ii % vector_to_cvector y) =\r
1552       sqrt(norm x pow 2 + norm y pow 2)`,\r
1553   REWRITE_TAC[cnorm;o_DEF;CNORM2_NORM2_2]);;\r
1554 \r
1555 let CNORM_NORM = prove(\r
1556   `!v:complex^N.\r
1557     norm v = sqrt(norm (cvector_re v) pow 2 + norm (cvector_im v) pow 2)`,\r
1558   GEN_TAC THEN GEN_REWRITE_TAC (RATOR_CONV o ONCE_DEPTH_CONV) [GSYM\r
1559     VECTOR_TO_CVECTOR_CVECTOR_RE_IM] THEN REWRITE_TAC[CNORM_NORM_2]);;\r
1560 \r
1561 let CNORM_MUL = prove\r
1562   (`!a x:complex^N. norm (a % x) = norm a * norm x`,\r
1563   SIMP_TAC[cnorm;o_DEF;CNORM2_MUL;REAL_LE_POW_2;SQRT_MUL;CNORM2_POS;\r
1564     NORM_POS_LE;POW_2_SQRT]);;\r
1565 \r
1566 let CNORM_EQ_0 = prove\r
1567   (`!x:complex^N. norm x = &0 <=> x = cvector_zero`,\r
1568   SIMP_TAC[cnorm;o_DEF;SQRT_EQ_0;CNORM2_POS;CNORM2_EQ_0]);;\r
1569 \r
1570 let CNORM_POS = prove\r
1571   (`!x:complex^N. &0 <= norm x`,\r
1572   SIMP_TAC[cnorm;o_DEF;SQRT_POS_LE;CNORM2_POS]);;\r
1573 \r
1574 let CNORM_SUB = prove\r
1575   (`!x y:complex^N. norm (x-y) = norm (y-x)`,\r
1576   REWRITE_TAC[cnorm;o_DEF;CNORM2_SUB]);;\r
1577 \r
1578 let CNORM_VECTOR_TO_CVECTOR = prove\r
1579   (`!x:real^N. norm (vector_to_cvector x) = norm x`,\r
1580   SIMP_TAC[cnorm;o_DEF;CNORM2_VECTOR_TO_CVECTOR;POW_2_SQRT;NORM_POS_LE]);;\r
1581 \r
1582 let CNORM_BASIS = prove\r
1583   (`!k. 1 <= k /\ k <= dimindex(:N)\r
1584     ==> norm (vector_to_cvector (basis k :real^N)) = &1`,\r
1585   SIMP_TAC[NORM_BASIS;CNORM_VECTOR_TO_CVECTOR]);;\r
1586 \r
1587 let CNORM_BASIS_1 = prove\r
1588  (`norm(basis 1:real^N) = &1`,\r
1589   SIMP_TAC[NORM_BASIS_1;CNORM_VECTOR_TO_CVECTOR]);;\r
1590 \r
1591 let CVECTOR_CHOOSE_SIZE = prove\r
1592   (`!c. &0 <= c ==> ?x:complex^N. norm(x) = c`,\r
1593   MESON_TAC[VECTOR_CHOOSE_SIZE;CNORM_VECTOR_TO_CVECTOR]);;\r
1594 \r
1595 (* Triangle inequality. Proved later on using Cauchy Schwarz inequality.\r
1596  * let CNORM_TRIANGLE = prove(`!x y:complex^N. norm (x+y) <= norm x + norm y`, ...\r
1597  *)\r
1598 \r
1599 let cunit = new_definition\r
1600   `cunit (X:complex^N) = inv(Cx(norm X))% X`;;\r
1601 \r
1602 let CUNIT_CVECTOR_ZERO = prove\r
1603   (`cunit cvector_zero = cvector_zero:complex^N`, \r
1604   REWRITE_TAC[cunit;CNORM_CVECTOR_ZERO;COMPLEX_INV_0;CVECTOR_MUL_LZERO]);;\r
1605 \r
1606 let CDOT_CUNIT_MUL_CUNIT = prove\r
1607   (`!x:complex^N. (cunit x cdot x) % cunit x = x`,\r
1608   GEN_TAC THEN ASM_CASES_TAC `x = cvector_zero:complex^N`\r
1609   THEN ASM_REWRITE_TAC[CUNIT_CVECTOR_ZERO;CDOT_LZERO;CVECTOR_MUL_LZERO]\r
1610   THEN SIMP_TAC[cunit;CVECTOR_MUL_ASSOC;CDOT_LMUL;\r
1611     SIMPLE_COMPLEX_ARITH `(x*y)*x=(x*x)*y`;GSYM COMPLEX_INV_MUL;GSYM CX_MUL;\r
1612     GSYM REAL_POW_2;cnorm;o_DEF;CNORM2_POS;SQRT_POW_2]\r
1613   THEN ASM_SIMP_TAC[cnorm2;REAL_OF_COMPLEX;REAL_CDOT_SELF;CDOT_EQ_0;\r
1614     CNORM2_CVECTOR_ZERO;CVECTOR_MUL_RZERO;CNORM2_EQ_0;COMPLEX_MUL_LINV;\r
1615     CVECTOR_MUL_ID]);;\r
1616 \r
1617 \r
1618 (* ========================================================================= *)\r
1619 (* COLLINEARITY                                                              *)\r
1620 (* ========================================================================= *)\r
1621 \r
1622 (* Definition of collinearity between complex vectors.\r
1623  * Note: This is different from collinearity between points (which is the one defined in HOL-Light library)\r
1624  *)\r
1625 let collinear_cvectors = new_definition\r
1626   `collinear_cvectors x (y:complex^N) <=> ?a. y = a % x \/ x = a % y`;;\r
1627 \r
1628 let COLLINEAR_CVECTORS_SYM = prove\r
1629   (`!x y:complex^N. collinear_cvectors x y <=> collinear_cvectors y x`,\r
1630   REWRITE_TAC[collinear_cvectors] THEN MESON_TAC[]);;\r
1631 \r
1632 let COLLINEAR_CVECTORS_0 = prove\r
1633   (`!x:complex^N. collinear_cvectors x cvector_zero`,\r
1634   REWRITE_TAC[collinear_cvectors] THEN GEN_TAC THEN EXISTS_TAC `Cx(&0)`\r
1635   THEN REWRITE_TAC[CVECTOR_MUL_LZERO]);;\r
1636 \r
1637 let NON_NULL_COLLINEARS = prove\r
1638   (`!x y:complex^N.\r
1639     collinear_cvectors x y /\ ~(x=cvector_zero) /\ ~(y=cvector_zero)\r
1640       ==> ?a. ~(a=Cx(&0)) /\ y = a % x`,\r
1641   REWRITE_TAC[collinear_cvectors] THEN REPEAT STRIP_TAC THENL [\r
1642     ASM_MESON_TAC[CVECTOR_MUL_LZERO];\r
1643     SUBGOAL_THEN `~(a=Cx(&0))` ASSUME_TAC THENL [\r
1644       ASM_MESON_TAC[CVECTOR_MUL_LZERO];\r
1645       EXISTS_TAC `inv a :complex`\r
1646       THEN ASM_REWRITE_TAC[COMPLEX_INV_EQ_0;CVECTOR_MUL_ASSOC]\r
1647       THEN ASM_SIMP_TAC[COMPLEX_MUL_LINV;CVECTOR_MUL_ID]]]);;\r
1648 \r
1649 let COLLINEAR_LNONNULL = prove(\r
1650   `!x y:complex^N.\r
1651     collinear_cvectors x y /\ ~(x=cvector_zero) ==> ?a. y = a % x`,\r
1652   REPEAT STRIP_TAC THEN ASM_CASES_TAC `y=cvector_zero:complex^N` THENL [\r
1653     ASM_REWRITE_TAC[] THEN EXISTS_TAC `Cx(&0)`\r
1654     THEN ASM_MESON_TAC[CVECTOR_MUL_LZERO];\r
1655     ASM_MESON_TAC[NON_NULL_COLLINEARS] ]);;\r
1656 \r
1657 let COLLINEAR_RNONNULL = prove(\r
1658   `!x y:complex^N.\r
1659     collinear_cvectors x y /\ ~(y=cvector_zero) ==> ?a. x = a % y`,\r
1660   MESON_TAC[COLLINEAR_LNONNULL;COLLINEAR_CVECTORS_SYM]);;\r
1661 \r
1662 let COLLINEAR_RUNITREAL = prove(\r
1663   `!x y:real^N.\r
1664     collinear_cvectors x (vector_to_cvector y) /\ norm y = &1\r
1665       ==> x = (x cdot (vector_to_cvector y)) % vector_to_cvector y`,\r
1666   REPEAT STRIP_TAC\r
1667   THEN POP_ASSUM (DISTRIB [ASSUME_TAC; ASSUME_TAC o REWRITE_RULE[NORM_EQ_0;\r
1668     GSYM VECTOR_TO_CVECTOR_ZERO_EQ] o MATCH_MP\r
1669       (REAL_ARITH `!x. x= &1 ==> ~(x= &0)`)])\r
1670   THEN FIRST_X_ASSUM (fun x -> FIRST_X_ASSUM (fun y ->\r
1671     CHOOSE_THEN (SINGLE ONCE_REWRITE_TAC) (MATCH_MP COLLINEAR_RNONNULL\r
1672       (CONJ y x))))\r
1673   THEN REWRITE_TAC[CDOT_LMUL;CDOT_LREAL;CVECTOR_RE_VECTOR_TO_CVECTOR;\r
1674     CVECTOR_IM_VECTOR_TO_CVECTOR;DOT_RZERO;COMPLEX_MUL_RZERO;COMPLEX_SUB_RZERO]\r
1675   THEN POP_ASSUM ((fun x ->\r
1676     REWRITE_TAC[x;COMPLEX_MUL_RID]) o REWRITE_RULE[NORM_EQ_1]));;\r
1677 \r
1678 let CCROSS_COLLINEAR_CVECTORS = prove\r
1679   (`!x y:complex^3. x ccross y = cvector_zero <=> collinear_cvectors x y`,\r
1680   REWRITE_TAC[ccross;collinear_cvectors;CART_EQ3;VECTOR_3;\r
1681     CVECTOR_ZERO_COMPONENT;COMPLEX_SUB_0;CVECTOR_MUL_COMPONENT]\r
1682   THEN REPEAT GEN_TAC THEN EQ_TAC\r
1683   THENL [\r
1684     REPEAT (POP_ASSUM MP_TAC) THEN ASM_CASES_TAC `(x:complex^3)$1 = Cx(&0)`\r
1685     THENL [\r
1686       ASM_CASES_TAC `(x:complex^3)$2 = Cx(&0)` THENL [\r
1687         ASM_CASES_TAC `(x:complex^3)$3 = Cx(&0)` THENL [\r
1688           REPEAT DISCH_TAC THEN EXISTS_TAC `Cx(&0)`\r
1689           THEN ASM_REWRITE_TAC[COMPLEX_POLY_CLAUSES];\r
1690           REPEAT STRIP_TAC THEN EXISTS_TAC `(y:complex^3)$3/(x:complex^3)$3`\r
1691           THEN ASM_SIMP_TAC[COMPLEX_BALANCE_DIV_MUL]\r
1692           THEN ASM_MESON_TAC[COMPLEX_MUL_AC];];\r
1693         REPEAT STRIP_TAC THEN EXISTS_TAC `(y:complex^3)$2/(x:complex^3)$2`\r
1694         THEN ASM_SIMP_TAC[COMPLEX_BALANCE_DIV_MUL]\r
1695         THEN ASM_MESON_TAC[COMPLEX_MUL_AC]; ];\r
1696       REPEAT STRIP_TAC THEN EXISTS_TAC `(y:complex^3)$1/(x:complex^3)$1`\r
1697       THEN ASM_SIMP_TAC[COMPLEX_BALANCE_DIV_MUL]\r
1698       THEN ASM_MESON_TAC[COMPLEX_MUL_AC];];\r
1699       SIMPLE_COMPLEX_ARITH_TAC ]);;\r
1700 \r
1701 let CVECTOR_MUL_INV = prove\r
1702   (`!a x y:complex^N. ~(a = Cx(&0)) /\ x = a % y ==> y = inv a % x`,\r
1703   REPEAT STRIP_TAC THEN ASM_SIMP_TAC[CVECTOR_MUL_ASSOC;\r
1704     MESON[] `(p\/q) <=> (~p ==> q)`;COMPLEX_MUL_LINV;CVECTOR_MUL_ID]);;\r
1705 \r
1706 let CVECTOR_MUL_INV2 = prove\r
1707   (`!a x y:complex^N. ~(x = cvector_zero) /\ x = a % y ==> y = inv a % x`,\r
1708   REPEAT STRIP_TAC THEN ASM_CASES_TAC `a=Cx(&0)`\r
1709   THEN ASM_MESON_TAC[CVECTOR_MUL_LZERO;CVECTOR_MUL_INV]);;\r
1710 \r
1711 \r
1712 \r
1713 let COLLINEAR_CVECTORS_VECTOR_TO_CVECTOR = prove(\r
1714   `!x y:real^N.\r
1715     collinear_cvectors (vector_to_cvector x) (vector_to_cvector y)\r
1716       <=> collinear {vec 0,x,y}`,\r
1717   REWRITE_TAC[COLLINEAR_LEMMA_ALT;collinear_cvectors]\r
1718   THEN REPEAT (STRIP_TAC ORELSE EQ_TAC) THENL [\r
1719     POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[CART_EQ]\r
1720     THEN REWRITE_TAC[CVECTOR_MUL_COMPONENT;VECTOR_TO_CVECTOR_COMPONENT;\r
1721       VECTOR_MUL_COMPONENT;COMPLEX_EQ;RE_CX;RE_MUL_CX]\r
1722     THEN REPEAT STRIP_TAC THEN DISJ2_TAC THEN EXISTS_TAC `Re a`\r
1723     THEN ASM_SIMP_TAC[];\r
1724     REWRITE_TAC[MESON[]`(p\/q) <=> (~p ==> q)`]\r
1725     THEN REWRITE_TAC[GSYM VECTOR_TO_CVECTOR_ZERO_EQ]\r
1726     THEN DISCH_TAC\r
1727     THEN SUBGOAL_TAC "" `vector_to_cvector (y:real^N) =\r
1728       inv a % vector_to_cvector x` [ASM_MESON_TAC[CVECTOR_MUL_INV2]]\r
1729     THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[CART_EQ]\r
1730     THEN REWRITE_TAC[CVECTOR_MUL_COMPONENT;VECTOR_TO_CVECTOR_COMPONENT;\r
1731       VECTOR_MUL_COMPONENT;COMPLEX_EQ;RE_CX;RE_MUL_CX]\r
1732     THEN REPEAT STRIP_TAC THEN EXISTS_TAC `Re(inv a)` THEN ASM_SIMP_TAC[];\r
1733     EXISTS_TAC `Cx(&0)` THEN ASM_REWRITE_TAC[VECTOR_TO_CVECTOR_ZERO;\r
1734       CVECTOR_MUL_LZERO];\r
1735     ASM_REWRITE_TAC[VECTOR_TO_CVECTOR_MUL] THEN EXISTS_TAC `Cx c`\r
1736     THEN REWRITE_TAC[];\r
1737   ]);;\r
1738 \r
1739 \r
1740 (* ========================================================================= *)\r
1741 (* ORTHOGONALITY                                                             *)\r
1742 (* ========================================================================= *)\r
1743 \r
1744 let corthogonal = new_definition\r
1745   `corthogonal (x:complex^N) y <=> x cdot y = Cx(&0)`;;\r
1746 \r
1747 let CORTHOGONAL_SYM = prove(\r
1748   `!x y:complex^N. corthogonal x y <=> corthogonal y x`,\r
1749   MESON_TAC[corthogonal;CDOT_SYM;CNJ_ZERO]);;\r
1750 \r
1751 let CORTHOGONAL_0 = prove(\r
1752   `!x:complex^N. corthogonal cvector_zero x /\ corthogonal x cvector_zero`,\r
1753   REWRITE_TAC[corthogonal;CDOT_LZERO;CDOT_RZERO]);;\r
1754 \r
1755 let [CORTHOGONAL_LZERO;CORTHOGONAL_RZERO] = GCONJUNCTS CORTHOGONAL_0;;\r
1756 \r
1757 let CORTHOGONAL_COLLINEAR_CVECTORS = prove\r
1758   (`!x y:complex^N.\r
1759     collinear_cvectors x y /\ ~(x=cvector_zero) /\ ~(y=cvector_zero)\r
1760       ==> ~(corthogonal x y)`,\r
1761   REWRITE_TAC[collinear_cvectors;corthogonal] THEN REPEAT STRIP_TAC\r
1762   THEN POP_ASSUM MP_TAC\r
1763   THEN ASM_REWRITE_TAC[CDOT_RMUL;CDOT_LMUL;COMPLEX_ENTIRE;GSYM cnorm2;\r
1764     CDOT_EQ_0;CNJ_EQ_0]\r
1765   THEN ASM_MESON_TAC[CVECTOR_MUL_LZERO]);;\r
1766  \r
1767 let CORTHOGONAL_MUL_CLAUSES = prove\r
1768   (`!x y a.\r
1769     (corthogonal x y ==> corthogonal x (a%y))\r
1770     /\ (corthogonal x y \/ a = Cx(&0) <=> corthogonal x (a%y))\r
1771     /\ (corthogonal x y ==> corthogonal (a%x) y)\r
1772     /\ (corthogonal x y \/ a = Cx(&0) <=> corthogonal (a%x) y)`,\r
1773   SIMP_TAC[corthogonal;CDOT_RMUL;CDOT_LMUL;COMPLEX_ENTIRE;CNJ_EQ_0]\r
1774   THEN MESON_TAC[]);;\r
1775 \r
1776 let [CORTHOGONAL_RMUL;CORTHOGONAL_RMUL_EQ;CORTHOGONAL_LMUL;\r
1777   CORTHOGONAL_LMUL_EQ] = GCONJUNCTS CORTHOGONAL_MUL_CLAUSES;;\r
1778 \r
1779 let CORTHOGONAL_LRMUL_CLAUSES = prove \r
1780   (`!x y a b.\r
1781     (corthogonal x y ==> corthogonal (a%x) (b%y))\r
1782     /\ (corthogonal x y \/ a = Cx(&0) \/ b = Cx(&0)\r
1783       <=> corthogonal (a%x) (b%y))`,\r
1784   MESON_TAC[CORTHOGONAL_MUL_CLAUSES]);;\r
1785 \r
1786 let [CORTHOGONAL_LRMUL;CORTHOGONAL_LRMUL_EQ] =\r
1787   GCONJUNCTS CORTHOGONAL_LRMUL_CLAUSES;;\r
1788 \r
1789 let CORTHOGONAL_REAL_CLAUSES = prove\r
1790   (`!r c.\r
1791     (corthogonal c (vector_to_cvector r)\r
1792       <=> orthogonal (cvector_re c) r /\ orthogonal (cvector_im c) r)\r
1793     /\ (corthogonal (vector_to_cvector r) c\r
1794       <=> orthogonal r (cvector_re c) /\ orthogonal r (cvector_im c))`,\r
1795   REWRITE_TAC[corthogonal;orthogonal;CDOT_LREAL;CDOT_RREAL;COMPLEX_SUB_0;\r
1796     COMPLEX_EQ;RE_CX;IM_CX;RE_SUB;IM_SUB;RE_ADD;IM_ADD]\r
1797   THEN REWRITE_TAC[RE_DEF;CX_DEF;IM_DEF;complex;complex_mul;VECTOR_2;ii]\r
1798   THEN CONV_TAC REAL_FIELD);;\r
1799 \r
1800 let [CORTHOGONAL_RREAL;CORTHOGONAL_LREAL] =\r
1801   GCONJUNCTS CORTHOGONAL_REAL_CLAUSES;;\r
1802 \r
1803 let CORTHOGONAL_UNIT = prove\r
1804   (`!x y:complex^N.\r
1805     (corthogonal x (cunit y) <=> corthogonal x y)\r
1806     /\ (corthogonal (cunit x) y <=> corthogonal x y)`,\r
1807   REWRITE_TAC[cunit;GSYM CORTHOGONAL_MUL_CLAUSES;COMPLEX_INV_EQ_0;CX_INJ;\r
1808     CNORM_EQ_0]\r
1809   THEN MESON_TAC[CORTHOGONAL_0]);;\r
1810 \r
1811 let [CORTHOGONAL_RUNIT;CORTHOGONAL_LUNIT] = GCONJUNCTS CORTHOGONAL_UNIT;;\r
1812 \r
1813 let CORTHOGONAL_PROJECTION = prove(\r
1814   `!x y:complex^N. corthogonal (x - (x cdot cunit y) % cunit y) y`,\r
1815   REPEAT GEN_TAC THEN ASM_CASES_TAC `y=cvector_zero:complex^N`\r
1816   THEN ASM_REWRITE_TAC[corthogonal;CDOT_RZERO]\r
1817   THEN REWRITE_TAC[CDOT_LSUB;cunit;CVECTOR_MUL_ASSOC;GSYM cnorm2;CDOT_LMUL;\r
1818     CDOT_RMUL;REWRITE_RULE[REAL_CNJ] (MATCH_MP REAL_INV (SPEC_ALL REAL_CX))]\r
1819   THEN REWRITE_TAC[COMPLEX_MUL_AC;GSYM COMPLEX_INV_MUL;GSYM COMPLEX_POW_2;\r
1820     cnorm;o_DEF;CSQRT]\r
1821   THEN SIMP_TAC[CNORM2_POS;CX_SQRT;cnorm2;REAL_CDOT_SELF;REAL_OF_COMPLEX;CSQRT]\r
1822   THEN ASM_SIMP_TAC[CDOT_EQ_0;COMPLEX_MUL_RINV;COMPLEX_MUL_RID;\r
1823     COMPLEX_SUB_REFL]);;\r
1824 \r
1825 let CDOT_PYTHAGOREAN = prove\r
1826   (`!x y:complex^N. corthogonal x y ==> cnorm2 (x+y) = cnorm2 x + cnorm2 y`,\r
1827   SIMP_TAC[corthogonal;cnorm2;CDOT_LADD;CDOT_RADD;COMPLEX_ADD_RID;\r
1828     COMPLEX_ADD_LID;REAL_OF_COMPLEX_ADD;REAL_CDOT_SELF;\r
1829     MESON[CDOT_SYM;CNJ_ZERO] `x cdot y = Cx (&0) ==> y cdot x = Cx(&0)`]);;\r
1830 \r
1831 let CDOT_CAUCHY_SCHWARZ_POW_2 = prove\r
1832   (`!x y:complex^N. norm (x cdot y) pow 2 <= cnorm2 x * cnorm2 y`,\r
1833   REPEAT GEN_TAC THEN ASM_CASES_TAC `y = cvector_zero:complex^N`\r
1834   THEN ASM_REWRITE_TAC[CNORM2_CVECTOR_ZERO;CDOT_RZERO;COMPLEX_NORM_0;\r
1835     REAL_POW_2;REAL_MUL_RZERO;REAL_OF_COMPLEX_CX;REAL_LE_REFL]\r
1836   THEN ONCE_REWRITE_TAC[MATCH_MP (MESON[CVECTOR_SUB_ADD] \r
1837     `(!x:complex^N y. p (x - f x y) y)\r
1838       ==> cnorm2 x * z = cnorm2 (x - f x y + f x y) * z`) CORTHOGONAL_PROJECTION]\r
1839   THEN MATCH_MP_TAC (GEN_ALL (MATCH_MP (MESON[] `(!x y. P x y ==> f x y = (g x y:real))\r
1840     ==> P x y /\ a <= g x y * b ==> a <= f x y * b`) CDOT_PYTHAGOREAN))\r
1841   THEN REWRITE_TAC[GSYM CORTHOGONAL_MUL_CLAUSES;CORTHOGONAL_RUNIT;\r
1842     CORTHOGONAL_PROJECTION]\r
1843   THEN SIMP_TAC[cnorm2;GSYM REAL_OF_COMPLEX_ADD;REAL_CDOT_SELF;REAL_ADD;\r
1844     GSYM REAL_OF_COMPLEX_MUL]\r
1845   THEN REWRITE_TACS[cunit;CDOT_RMUL;CVECTOR_MUL_ASSOC;REWRITE_RULE[REAL_CNJ]\r
1846     (MATCH_MP REAL_INV (SPEC_ALL REAL_CX));COMPLEX_MUL_AC;GSYM COMPLEX_INV_MUL;\r
1847     GSYM COMPLEX_POW_2;cnorm;o_DEF;CSQRT;COMPLEX_ADD_LDISTRIB;cnorm2;CDOT_RMUL;\r
1848     CNJ_MUL;CDOT_LMUL;GSYM cnorm2;\r
1849     REWRITE_RULE[REAL_CNJ] (MATCH_MP REAL_INV (SPEC_ALL REAL_CX))]\r
1850   THEN SIMP_TAC[CX_SQRT;CNORM2_POS;CSQRT;CX_CNORM2]\r
1851   THEN REWRITE_TAC[SIMPLE_COMPLEX_ARITH\r
1852     `x * ((y * inv x) * x) * (z * inv x') * inv x'\r
1853     = (y * z) * (x * inv x) * (x * inv x' * inv x'):complex`]\r
1854   THEN ASM_SIMP_TAC[CDOT_EQ_0;COMPLEX_MUL_RINV;COMPLEX_MUL_LID;COMPLEX_MUL_CNJ;\r
1855     GSYM COMPLEX_INV_MUL]\r
1856   THEN ONCE_REWRITE_TAC[\r
1857     GSYM (MATCH_MP REAL_OF_COMPLEX (SPEC_ALL REAL_CDOT_SELF))]\r
1858   THEN SIMP_TAC[GSYM cnorm2;GSYM CX_SQRT;CNORM2_POS;GSYM CX_MUL;\r
1859     GSYM COMPLEX_POW_2;GSYM CX_POW;SQRT_POW_2;GSYM CX_INV]\r
1860   THEN ASM_SIMP_TAC[REAL_MUL_RINV;CNORM2_EQ_0;REAL_MUL_RID;GSYM CX_ADD;\r
1861     REAL_OF_COMPLEX_CX;GSYM REAL_POW_2;REAL_LE_ADDL;REAL_LE_MUL;CNORM2_POS]);;\r
1862 \r
1863 let CDOT_CAUCHY_SCHWARZ = prove \r
1864   (`!x y:complex^N. norm (x cdot y) <= norm x * norm y`,\r
1865   REPEAT GEN_TAC THEN MATCH_MP_TAC (REWRITE_RULE[REAL_LE_SQUARE_ABS]\r
1866     (REAL_ARITH `&0 <= x /\ &0 <= y /\ abs x <= abs y ==> x <= y`))\r
1867   THEN SIMP_TAC[NORM_POS_LE;CNORM_POS;REAL_LE_MUL;REAL_POW_MUL;CNORM_POW_2;\r
1868     CDOT_CAUCHY_SCHWARZ_POW_2]);;\r
1869 \r
1870 let CDOT_CAUCHY_SCHWARZ_POW_2_EQUAL = prove\r
1871   (`!x y:complex^N.\r
1872     norm (x cdot y) pow 2 = cnorm2 x * cnorm2 y <=> collinear_cvectors x y`,\r
1873   REPEAT GEN_TAC THEN ASM_CASES_TAC `y = cvector_zero:complex^N`\r
1874   THEN ASM_REWRITE_TAC[CNORM2_CVECTOR_ZERO;CDOT_RZERO;COMPLEX_NORM_0;\r
1875     REAL_POW_2;REAL_MUL_RZERO;REAL_OF_COMPLEX_CX;COLLINEAR_CVECTORS_0]\r
1876   THEN EQ_TAC THENL [\r
1877     ONCE_REWRITE_TAC[MATCH_MP (MESON[CVECTOR_SUB_ADD] \r
1878       `(!x:complex^N y. p (x - f x y) y) ==>\r
1879       cnorm2 x * z = cnorm2 (x - f x y + f x y) * z`) CORTHOGONAL_PROJECTION]\r
1880     THEN MATCH_MP_TAC (GEN_ALL (MATCH_MP (MESON[]\r
1881       `(!x y. P x y ==> g x y = (f x y:real)) ==>\r
1882         P x y /\ (a = f x y * z ==> R) ==> (a = g x y * z ==> R)`)\r
1883       CDOT_PYTHAGOREAN))\r
1884     THEN REWRITE_TAC[GSYM CORTHOGONAL_MUL_CLAUSES;CORTHOGONAL_RUNIT;\r
1885       CORTHOGONAL_PROJECTION]\r
1886     THEN SIMP_TAC[cnorm2;GSYM REAL_OF_COMPLEX_ADD;REAL_CDOT_SELF;REAL_ADD;\r
1887       GSYM REAL_OF_COMPLEX_MUL]\r
1888     THEN REWRITE_TACS[cunit;CDOT_RMUL;CVECTOR_MUL_ASSOC;REWRITE_RULE[REAL_CNJ]\r
1889       (MATCH_MP REAL_INV (SPEC_ALL REAL_CX));COMPLEX_MUL_AC;\r
1890       GSYM COMPLEX_INV_MUL;GSYM COMPLEX_POW_2;cnorm;o_DEF;CSQRT;\r
1891       COMPLEX_ADD_LDISTRIB;cnorm2;CDOT_RMUL;CNJ_MUL;CDOT_LMUL;GSYM cnorm2;\r
1892       REWRITE_RULE[REAL_CNJ] (MATCH_MP REAL_INV (SPEC_ALL REAL_CX))]\r
1893     THEN SIMP_TAC[CX_SQRT;CNORM2_POS;CSQRT;CX_CNORM2]\r
1894     THEN REWRITE_TAC[SIMPLE_COMPLEX_ARITH\r
1895       `x * ((y * inv x) * x) * (z * inv x') * inv x' =\r
1896         (y * z) * (x * inv x) * (x * inv x' * inv x'):complex`]\r
1897     THEN ONCE_REWRITE_TAC[GSYM (MATCH_MP REAL_OF_COMPLEX\r
1898       (SPEC_ALL REAL_CDOT_SELF))]\r
1899     THEN SIMP_TAC[GSYM cnorm2;GSYM CX_SQRT;CNORM2_POS;GSYM CX_MUL;\r
1900       GSYM COMPLEX_POW_2;GSYM CX_POW;SQRT_POW_2;GSYM CX_INV;REAL_POW_INV]\r
1901     THEN ASM_SIMP_TAC[REAL_MUL_RINV;CNORM2_EQ_0;REAL_MUL_RID;GSYM CX_ADD;\r
1902       REAL_OF_COMPLEX_CX;GSYM REAL_POW_2;REAL_LE_ADDL;REAL_LE_MUL;CNORM2_POS;\r
1903       GSYM CX_POW;REAL_POW_ONE;COMPLEX_MUL_RID;COMPLEX_MUL_CNJ;\r
1904       REAL_ARITH `x = y + x <=> y = &0`;REAL_ENTIRE;CNORM2_EQ_0;\r
1905       CVECTOR_SUB_EQ;collinear_cvectors]\r
1906     THEN MESON_TAC[];\r
1907     REWRITE_TAC[collinear_cvectors] THEN REPEAT STRIP_TAC\r
1908     THEN ASM_REWRITE_TAC[cnorm2;CDOT_LMUL;CDOT_RMUL;COMPLEX_NORM_MUL;\r
1909       COMPLEX_MUL_ASSOC]\r
1910     THEN SIMP_TAC[COMPLEX_MUL_CNJ;GSYM cnorm2;COMPLEX_NORM_CNJ;GSYM CX_POW;\r
1911       REAL_OF_COMPLEX_MUL;REAL_CX;REAL_CDOT_SELF;REAL_OF_COMPLEX_CX;\r
1912       GSYM CNORM2_ALT]\r
1913     THEN SIMPLE_COMPLEX_ARITH_TAC\r
1914   ]);;\r
1915 \r
1916 let CDOT_CAUCHY_SCHWARZ_EQUAL = prove\r
1917   (`!x y:complex^N.\r
1918   norm (x cdot y) = norm x * norm y <=> collinear_cvectors x y`,\r
1919   ONCE_REWRITE_TAC[REWRITE_RULE[REAL_EQ_SQUARE_ABS] (REAL_ARITH\r
1920     `x=y <=> abs x = abs y /\ (&0 <= x /\ &0 <= y \/ x < &0 /\ y < &0)`)]\r
1921   THEN SIMP_TAC[NORM_POS_LE;CNORM_POS;REAL_LE_MUL;REAL_POW_MUL;CNORM_POW_2;\r
1922     CDOT_CAUCHY_SCHWARZ_POW_2_EQUAL]);;\r
1923 \r
1924 let CNORM_TRIANGLE = prove\r
1925   (`!x y:complex^N. norm (x+y) <= norm x + norm y`,\r
1926   REPEAT GEN_TAC THEN MATCH_MP_TAC (REWRITE_RULE[REAL_LE_SQUARE_ABS]\r
1927     (REAL_ARITH `abs x <= abs y /\ &0 <= x /\ &0 <= y ==> x <= y`))\r
1928   THEN SIMP_TAC[CNORM_POS;REAL_LE_ADD;REAL_ADD_POW_2;CNORM_POW_2;cnorm2;\r
1929     CDOT_LADD;CDOT_RADD;SIMPLE_COMPLEX_ARITH `(x+y)+z+t = x+(y+z)+t:complex`;\r
1930     ADD_CDOT_SYM;REAL_OF_COMPLEX_ADD;REAL_CDOT_SELF;REAL_CX;REAL_ADD;\r
1931     REAL_OF_COMPLEX_CX;REAL_ARITH `x+ &2*y+z<=x+z+ &2*t <=> y<=t:real`]\r
1932   THEN MESON_TAC[CDOT_CAUCHY_SCHWARZ;RE_NORM;REAL_LE_TRANS]);;\r
1933 \r
1934 let REAL_ABS_SUB_CNORM = prove\r
1935   (`!x y:complex^N. abs (norm x - norm y) <= norm (x-y)`,\r
1936   let lemma =\r
1937     REWRITE_RULE[CVECTOR_SUB_ADD2;REAL_ARITH `x<=y+z <=> x-y<=z:real`]\r
1938       (SPECL [`x:complex^N`;`y-x:complex^N`] CNORM_TRIANGLE)\r
1939   in\r
1940   REPEAT GEN_TAC\r
1941   THEN MATCH_MP_TAC (MATCH_MP (MESON[]\r
1942     `(!x y. P x y <=> Q x y) ==> Q x y ==> P x y`) REAL_ABS_BOUNDS)\r
1943   THEN ONCE_REWRITE_TAC[REAL_ARITH `--x <= y <=>  --y <= x`]\r
1944   THEN REWRITE_TAC[REAL_NEG_SUB]\r
1945   THEN REWRITE_TAC[lemma;ONCE_REWRITE_RULE[CNORM_SUB] lemma]);;\r
1946 \r
1947 (* ========================================================================= *)\r
1948 (* VSUM                                                                      *)\r
1949 (* ========================================================================= *)\r
1950 \r
1951 let cvsum = new_definition\r
1952   `(cvsum:(A->bool)->(A->complex^N)->complex^N) s f = lambda i. vsum s (\x. (f x)$i)`;;\r
1953 \r
1954 \r
1955 (* ========================================================================= *)\r
1956 (* INFINITE SUM                                                              *)\r
1957 (* ========================================================================= *)\r
1958 \r
1959 let csummable = new_definition\r
1960   `csummable (s:num->bool) (f:num->complex^N)\r
1961     <=> summable s (cvector_re o f) /\ summable s (cvector_im o f)`;;\r
1962 \r
1963 let cinfsum = new_definition\r
1964   `cinfsum (s:num->bool) (f:num->complex^N) :complex^N\r
1965     = vector_to_cvector (infsum s (\x. cvector_re (f x)))\r
1966       + ii % vector_to_cvector (infsum s (\x.cvector_im (f x)))`;;\r
1967 \r
1968 let CSUMMABLE_FLATTEN_CVECTOR = prove\r
1969   (`!s (f:num->complex^N). csummable s f <=> summable s (cvector_flatten o f)`,\r
1970   REWRITE_TAC[csummable;summable;cvector_flatten;o_DEF]\r
1971   THEN REPEAT (STRIP_TAC ORELSE EQ_TAC)\r
1972   THENL [\r
1973     EXISTS_TAC `pastecart (l:real^N) (l':real^N)`\r
1974     THEN ASM_SIMP_TAC[GSYM SUMS_PASTECART];\r
1975     EXISTS_TAC `fstcart (l:real^(N,N) finite_sum)`\r
1976     THEN MATCH_MP_TAC (GEN_ALL (MATCH_MP (TAUT `(p /\ q <=> r) ==> (r ==> p)`)\r
1977       (INST_TYPE [`:N`,`:M`] (SPEC_ALL SUMS_PASTECART))))\r
1978     THEN EXISTS_TAC `(cvector_im o f) :num->real^N`\r
1979     THEN EXISTS_TAC `sndcart (l:real^(N,N) finite_sum)`\r
1980     THEN ASM_REWRITE_TAC[ETA_AX;o_DEF;PASTECART_FST_SND];\r
1981     EXISTS_TAC `sndcart (l:real^(N,N) finite_sum)`\r
1982     THEN MATCH_MP_TAC (GEN_ALL (MATCH_MP (TAUT `(p /\ q <=> r) ==> (r ==> q)`)\r
1983       (INST_TYPE [`:N`,`:M`] (SPEC_ALL SUMS_PASTECART))))\r
1984     THEN EXISTS_TAC `(cvector_re o f) :num->real^N`\r
1985     THEN EXISTS_TAC `fstcart (l:real^(N,N) finite_sum)`\r
1986     THEN ASM_REWRITE_TAC[ETA_AX;o_DEF;PASTECART_FST_SND];\r
1987   ]);;\r
1988 \r
1989 let FLATTEN_CINFSUM = prove\r
1990   (`!s f.\r
1991     csummable s f ==>\r
1992       ((cinfsum s f):complex^N) =\r
1993         cvector_unflatten (infsum s (cvector_flatten o f))`,\r
1994   SIMP_TAC[cinfsum;cvector_unflatten;COMPLEX_VECTOR_TRANSPOSE;LINEAR_FSTCART;\r
1995     LINEAR_SNDCART;CSUMMABLE_FLATTEN_CVECTOR;GSYM INFSUM_LINEAR;o_DEF;\r
1996     cvector_flatten;FSTCART_PASTECART;SNDCART_PASTECART]);;\r
1997 \r
1998 let CSUMMABLE_LINEAR = prove\r
1999   (`!f h:complex^N->complex^M s.\r
2000     csummable s f /\ clinear h ==> csummable s (h o f)`,\r
2001   REWRITE_TAC[CSUMMABLE_FLATTEN_CVECTOR] THEN REPEAT STRIP_TAC\r
2002   THEN POP_ASSUM (ASSUME_TAC o MATCH_MP FLATTEN_CLINEAR)\r
2003   THEN SUBGOAL_THEN\r
2004     `cvector_flatten o (h:complex^N -> complex^M) o (f:num -> complex^N) =\r
2005     \n. (cvector_flatten o h o cvector_unflatten) (cvector_flatten (f n))`\r
2006     (SINGLE REWRITE_TAC)\r
2007   THENL [\r
2008     REWRITE_TAC[o_DEF;FUN_EQ_THM] THEN GEN_TAC THEN REPEAT AP_TERM_TAC\r
2009     THEN REWRITE_TAC[REWRITE_RULE[o_DEF;I_DEF;FUN_EQ_THM] UNFLATTEN_FLATTEN];\r
2010     MATCH_MP_TAC SUMMABLE_LINEAR THEN ASM_SIMP_TAC[GSYM o_DEF]\r
2011   ]);;\r
2012 \r
2013 let CINFSUM_LINEAR = prove\r
2014   (`!f (h:complex^M->complex^N) s.\r
2015     csummable s f /\ clinear h ==> cinfsum s (h o f) = h (cinfsum s f)`,\r
2016   REPEAT GEN_TAC\r
2017   THEN DISCH_THEN (fun x -> MP_TAC (CONJ (MATCH_MP CSUMMABLE_LINEAR x) x))\r
2018   THEN SIMP_TAC[FLATTEN_CINFSUM;CSUMMABLE_FLATTEN_CVECTOR]\r
2019   THEN REPEAT STRIP_TAC THEN POP_ASSUM (ASSUME_TAC o MATCH_MP FLATTEN_CLINEAR)\r
2020   THEN SUBGOAL_THEN\r
2021     `cvector_flatten o (h:complex^M->complex^N) o (f:num->complex^M) =\r
2022     \n. (cvector_flatten o h o cvector_unflatten) ((cvector_flatten o f) n)`\r
2023     (SINGLE REWRITE_TAC)\r
2024   THENL [\r
2025     REWRITE_TAC[o_DEF;FUN_EQ_THM] THEN GEN_TAC THEN REPEAT AP_TERM_TAC\r
2026     THEN REWRITE_TAC[REWRITE_RULE[o_DEF;I_DEF;FUN_EQ_THM] UNFLATTEN_FLATTEN];\r
2027     FIRST_ASSUM (fun x -> FIRST_ASSUM (fun y -> REWRITE_TAC[MATCH_MP\r
2028       (MATCH_MP (REWRITE_RULE[IMP_CONJ] INFSUM_LINEAR) x) y]))\r
2029     THEN REWRITE_TAC[o_DEF;REWRITE_RULE[o_DEF;I_DEF;FUN_EQ_THM]\r
2030       UNFLATTEN_FLATTEN]\r
2031   ]);;\r
2032