em_model.ml

   1
   2 (* Upadted for the latest version of HOL Light (JULY 2014) *)
   3 (* ========================================================================= *)\r
   4 (*               Formalization of Electromagnetic Optics                     *)\r
   5 (*                                                                           *)\r
   6 (*            (c) Copyright, Sanaz Khan Afshar & Vincent Aravantinos 2011-13 *)\r
   7 (*                           Hardware Verification Group,                    *)\r
   8 (*                           Concordia University                            *)\r
   9 (*                                                                           *)\r
  10 (*                Contact:   <s_khanaf@encs.concordia.ca>                    *)\r
  11 (*                           <vincent@encs.concordia.ca>                     *)\r
  12 (*                                                                           *)\r
  13 (* This file deals with the definition and basic theorems about the          *)\r
  14 (* electromagnetic model.                                                    *)\r
  15 (* ========================================================================= *)\r
  16 \r
  17 new_type_abbrev("time",`:real`);;\r
  18 \r
  19 (********************************)\r
  20 (* Electromagnetic fields       *)\r
  21 (********************************)\r
  22 \r
  23 new_type_abbrev("single_field",`:point -> time -> complex^3`);;\r
  24 new_type_abbrev("emf", `:point -> time -> complex^3 # complex^3`);;\r
  25 \r
  26 let e_of_emf = new_definition\r
  27   `e_of_emf (emf:emf) : single_field = \r t. let (e,h) = emf r t in e`;;\r
  28 let h_of_emf = new_definition\r
  29   `h_of_emf (emf:emf) : single_field = \r t. let (e,h) = emf r t in h`;;\r
  30 let is_valid_emf = new_definition\r
  31   `is_valid_emf emf\r
  32     <=> !r t. corthogonal (h_of_emf emf r t) (e_of_emf emf r t)`;;\r
  33 \r
  34 let EMF_EQ = prove\r
  35   (`!emf:emf r t e h. emf r t = e,h\r
  36     <=> e_of_emf emf r t = e /\ h_of_emf emf r t = h`,\r
  37   REPEAT STRIP_TAC THEN EQ_TAC\r
  38   THEN SIMP_TAC[e_of_emf;h_of_emf;LET_DEFs;PAIR_EQ;LAMBDA_PAIR]\r
  39   THEN MESON_TAC[PAIR]);;\r
  40 \r
  41 let emf_at_point_mul = new_definition\r
  42   `emf_at_point_mul (f:complex) (emf:complex^3#complex^3) :complex^3#complex^3\r
  43     = (f % FST emf, f % SND emf)`;;\r
  44 \r
  45 overload_interface("%",\r
  46   `emf_at_point_mul :complex->complex^3#complex^3->complex^3#complex^3`);;\r
  47 \r
  48 let emf_add = new_definition\r
  49   `emf_add (emf1:emf) (emf2:emf) :emf = \r t.\r
  50     (e_of_emf emf1 r t + e_of_emf emf2 r t,\r
  51       h_of_emf emf1 r t + h_of_emf emf2 r t)`;;\r
  52 \r
  53 overload_interface("+",`emf_add :emf->emf->emf`);;\r
  54  \r
  55 \r
  56 (********************************)\r
  57 (* Plane waves                  *)\r
  58 (********************************)\r
  59 \r
  60 let plane_wave = new_definition\r
  61   `plane_wave k w e h : emf = \r t. cexp (--ii * Cx(k dot r - w*t)) % (e,h)`;;\r
  62 \r
  63 let is_plane_wave = new_definition\r
  64   `is_plane_wave emf <=>\r
  65     is_valid_emf emf /\ ?k w e h.\r
  66       &0 < w /\ ~(k = vec 0) /\ emf = plane_wave k w e h\r
  67       /\ corthogonal e (vector_to_cvector k)\r
  68       /\ corthogonal h (vector_to_cvector k)`;;\r
  69 \r
  70 let k_of_wave = new_definition\r
  71   `k_of_wave emf = @k. ?w e h . &0 < w /\ ~(k = vec 0)\r
  72     /\ emf = plane_wave k w e h\r
  73     /\ corthogonal e (vector_to_cvector k)\r
  74     /\ corthogonal h (vector_to_cvector k)`;;\r
  75 \r
  76 let w_of_wave = new_definition\r
  77   `w_of_wave emf = @w. ?e h . &0 < w /\ emf = plane_wave (k_of_wave emf) w e h\r
  78     /\ corthogonal e (vector_to_cvector (k_of_wave emf))\r
  79     /\ corthogonal h (vector_to_cvector (k_of_wave emf))`;;\r
  80 \r
  81 let e_of_wave = new_definition\r
  82   `e_of_wave emf = @e. ?h . emf = plane_wave (k_of_wave emf) (w_of_wave emf) e h\r
  83     /\ corthogonal e (vector_to_cvector (k_of_wave emf))\r
  84     /\ corthogonal h (vector_to_cvector (k_of_wave emf))`;;\r
  85 \r
  86 let h_of_wave = new_definition\r
  87   `h_of_wave emf = @h.\r
  88     emf = plane_wave (k_of_wave emf) (w_of_wave emf) (e_of_wave emf) h\r
  89     /\ corthogonal (e_of_wave emf) (vector_to_cvector (k_of_wave emf)) \r
  90     /\ corthogonal h (vector_to_cvector (k_of_wave emf))`;;\r
  91 \r
  92 let eh_of_wave = new_definition\r
  93   `eh_of_wave emf = (e_of_wave emf,h_of_wave emf)`;;\r
  94 \r
  95 let scalar_of_wave = new_definition\r
  96   `scalar_of_wave emf =\r
  97     \r t. cexp (--ii * Cx(k_of_wave emf dot r - w_of_wave emf * t))`;;\r
  98 \r
  99 let IS_PLANE_WAVE = prove\r
 100   (`!emf. is_plane_wave emf <=>\r
 101     is_valid_emf emf /\ &0 < w_of_wave emf /\ ~(k_of_wave emf = vec 0)\r
 102     /\ emf = plane_wave (k_of_wave emf) (w_of_wave emf) (e_of_wave emf)\r
 103       (h_of_wave emf)\r
 104     /\ corthogonal (e_of_wave emf) (vector_to_cvector (k_of_wave emf))\r
 105     /\ corthogonal (h_of_wave emf) (vector_to_cvector (k_of_wave emf))`,\r
 106   let COMMON_TAC x =\r
 107     GEN_TAC THEN EQ_TAC THEN REWRITE_TAC[is_plane_wave;x] THEN MESON_TAC[]\r
 108   in\r
 109   let lemma1 = prove\r
 110     (`!emf. is_plane_wave emf <=> is_valid_emf emf /\ ?w e h . &0 < w\r
 111       /\ ~(k_of_wave emf = vec 0) /\ emf = plane_wave (k_of_wave emf) w e h\r
 112       /\ corthogonal e (vector_to_cvector (k_of_wave emf))\r
 113       /\ corthogonal h (vector_to_cvector (k_of_wave emf))`,\r
 114     COMMON_TAC k_of_wave)\r
 115   in\r
 116   let lemma2 = prove\r
 117     (`!emf. is_plane_wave emf <=>\r
 118       is_valid_emf emf /\ ?e h . &0 < w_of_wave emf /\ ~(k_of_wave emf = vec 0)\r
 119       /\ emf = plane_wave (k_of_wave emf) (w_of_wave emf) e h\r
 120       /\ corthogonal e (vector_to_cvector (k_of_wave emf))\r
 121       /\ corthogonal h (vector_to_cvector (k_of_wave emf))`,\r
 122     REWRITE_TAC[lemma1] THEN COMMON_TAC w_of_wave)\r
 123   in\r
 124   let lemma3 = prove\r
 125     (`!emf. is_plane_wave emf <=>\r
 126       is_valid_emf emf /\ ?h . &0 < w_of_wave emf /\ ~(k_of_wave emf = vec 0) /\\r
 127       emf = plane_wave (k_of_wave emf) (w_of_wave emf) (e_of_wave emf) h\r
 128       /\ corthogonal (e_of_wave emf) (vector_to_cvector (k_of_wave emf))\r
 129       /\ corthogonal h (vector_to_cvector (k_of_wave emf))`,\r
 130     REWRITE_TAC[lemma2] THEN COMMON_TAC e_of_wave)\r
 131   in\r
 132   REWRITE_TAC[lemma3] THEN COMMON_TAC h_of_wave);;\r
 133 \r
 134 let EH_OF_EMF_PLANE_WAVE = prove\r
 135   (`!k w e h.\r
 136     (e_of_emf (plane_wave k w e h) = \r t. cexp (--ii * Cx(k dot r - w*t)) % e )\r
 137     /\ h_of_emf (plane_wave k w e h) = \r t.\r
 138       cexp (--ii * Cx(k dot r - w*t)) % h`,\r
 139   REWRITE_TAC[e_of_emf;h_of_emf;plane_wave;emf_at_point_mul;LET_DEFs]);;\r
 140 \r
 141 let non_null_wave = new_definition\r
 142   `non_null_wave emf <=>\r
 143     is_plane_wave emf /\ ~(e_of_wave emf = cvector_zero)\r
 144     /\ ~(h_of_wave emf = cvector_zero)`;;\r
 145 \r
 146 \r
 147 (***********************************)\r
 148 (* Plane interface between mediums *)\r
 149 (***********************************)\r
 150 \r
 151  (* A medium is characterized by its refractive index *)\r
 152 new_type_abbrev("medium", `:real`);;\r
 153 \r
 154 (* The real^3 vector is a normal to the plane. It is needed in order to fix an\r
 155  * orientation so that we can clearly say on which side is medium 1 or 2 \r
 156  * respectively. *)\r
 157 new_type_abbrev("interface",`:medium # medium # plane # real^3`);;\r
 158 \r
 159 let FORALL_INTERFACE_THM = prove\r
 160   (`!P. (!(i:interface). P i) <=> (!n1 n2 p n. P (n1,n2,p,n))`,\r
 161   MESON_TAC[PAIR_SURJECTIVE]);;\r
 162 \r
 163 let is_valid_interface = new_definition\r
 164   `is_valid_interface (i:interface) <=>\r
 165     let (n1,n2,p,n) = i in\r
 166     &0 < n1 /\ &0 < n2 /\ plane p /\ is_normal_to_plane n p`;;\r
 167 \r
 168 let plane_of_interface = new_definition\r
 169   `plane_of_interface (i:interface) = let (n1,n2,p,n) = i in p`;;\r
 170 let normal_of_interface = new_definition\r
 171   `normal_of_interface (i:interface) = let (n1,n2,p,n) = i in n`;;\r
 172 let n1_of_interface = new_definition\r
 173   `n1_of_interface (i:interface) = let (n1,n2,p,n) = i in n1`;;\r
 174 let n2_of_interface = new_definition\r
 175   `n2_of_interface (i:interface) = let (n1,n2,p,n) = i in n2`;;\r
 176 \r
 177 (* Helpers *)\r
 178 let IS_VALID_INTERFACE_IS_NORMAL_TO_PLANE = prove\r
 179   (`!i. is_valid_interface i ==>\r
 180     is_normal_to_plane (normal_of_interface i) (plane_of_interface i)`,\r
 181   SIMP_TAC[FORALL_INTERFACE_THM;is_valid_interface;LET_DEFs;\r
 182     normal_of_interface;plane_of_interface]);;\r
 183 \r
 184 let NORMAL_OF_INTERFACE_NON_NULL = prove\r
 185   (`!i. is_valid_interface i ==> ~(normal_of_interface i = vec 0)`,\r
 186   SIMP_TAC[FORALL_INTERFACE_THM;is_valid_interface;is_normal_to_plane;\r
 187     normal_of_interface;LET_DEFs]);;\r
 188 let IS_VALID_INTERFACE_PLANE = prove\r
 189   (`!i. is_valid_interface i ==> plane (plane_of_interface i)`,\r
 190   SIMP_TAC[FORALL_INTERFACE_THM;is_valid_interface;plane_of_interface;\r
 191     LET_DEFs]);;\r
 192 \r
 193 (* [p] is the point where continuity holds; [n] is the normal to the tangent\r
 194  * plane at that point. *)\r
 195 \r
 196 let boundary_conditions = new_definition\r
 197   `boundary_conditions emf1 emf2 p r t <=>\r
 198     !n. is_normal_to_plane n p ==>\r
 199     let n_ccross = (ccross) (vector_to_cvector n) in\r
 200     n_ccross (e_of_emf emf1 r t) = n_ccross (e_of_emf emf2 r t)\r
 201     /\ n_ccross (h_of_emf emf1 r t) = n_ccross (h_of_emf emf2 r t)`;;\r
 202 \r
 203 let eta0 = new_specification ["eta0"] \r
 204   (EXISTS (`?x. &0 < x`,`&1`) (REAL_ARITH `&0 < &1`));;\r
 205 let k0 = new_specification ["k0"] \r
 206   (EXISTS (`?x. &0 < x`,`&1`) (REAL_ARITH `&0 < &1`));;\r
 207 \r
 208 let is_plane_wave_at_interface = new_definition\r
 209   `is_plane_wave_at_interface i emf_i emf_r emf_t <=>\r
 210     is_valid_interface i /\ non_null_wave emf_i /\ is_plane_wave emf_r\r
 211     /\ is_plane_wave emf_t\r
 212     /\ let (n1,n2,p,n) = i in\r
 213       (!pt. pt IN p ==> !t. boundary_conditions (emf_i + emf_r) emf_t p pt t) /\\r
 214       (let (k_i,k_r,k_t) = map_triple k_of_wave (emf_i, emf_r, emf_t) in\r
 215       (k_i dot n > &0 /\ k_r dot n <= &0 /\ k_t dot n >= &0) /\\r
 216       norm k_i = k0 * n1 /\ norm k_r = k0 * n1 /\ norm k_t = k0 * n2) /\\r
 217       let emf_in_medium = \emf n.\r
 218         h_of_wave emf = Cx(&1 / (eta0 * k0)) %\r
 219           (vector_to_cvector (k_of_wave emf) ccross (e_of_wave emf))\r
 220       in\r
 221       emf_in_medium emf_i n1 /\ emf_in_medium emf_r n1\r
 222       /\ emf_in_medium emf_t n2`;;\r
 223 \r
 224 let IS_PLANE_WAVE_AT_INTERFACE_MAGNITUDES_RELATION = prove(\r
 225   `!i emf_i emf_r emf_t. is_plane_wave_at_interface i emf_i emf_r emf_t ==>\r
 226         let (n1,n2,p,n) = i in\r
 227         let (e_i,e_r,e_t) = map_triple (norm o e_of_wave) (emf_i,emf_r,emf_t) in\r
 228         let (h_i,h_r,h_t) = map_triple (norm o h_of_wave) (emf_i,emf_r,emf_t) in\r
 229         h_i = e_i * n1_of_interface i / eta0\r
 230   /\ h_r = e_r * n1_of_interface i / eta0\r
 231   /\ h_t = e_t * n2_of_interface i / eta0`,\r
 232   SIMP_TAC[FORALL_INTERFACE_THM;LET_DEFs;map_triple;o_DEF;n1_of_interface;\r
 233     n2_of_interface;is_plane_wave_at_interface;GSYM CCROSS_LMUL;\r
 234     GSYM VECTOR_TO_CVECTOR_MUL;CCROSS_LREAL;CNORM_NORM_2;\r
 235     REWRITE_RULE[REAL_ARITH `x+y=z <=> x=z-y:real`] NORM_CROSS_DOT;non_null_wave;\r
 236     REAL_ARITH `(x-y)+(z-t)=(x+z)-(y+t):real`;REAL_POW_MUL;\r
 237     GSYM REAL_ADD_LDISTRIB;IS_PLANE_WAVE;CORTHOGONAL_REAL_CLAUSES;DOT_LMUL]\r
 238   THEN ONCE_REWRITE_TAC[ORTHOGONAL_SYM] THEN SIMP_TAC[orthogonal;REAL_POW_2;\r
 239     REAL_MUL_RZERO;REAL_ADD_RID;REAL_SUB_RZERO]\r
 240   THEN SIMP_TAC[GSYM REAL_POW_2;REAL_LE_POW_2;MESON[REAL_LE_ADD;REAL_LE_POW_2]\r
 241     `!x y. &0 <= x pow 2 + y pow 2`;SQRT_MUL;CX_MUL]\r
 242   THEN REWRITE_TAC[GSYM CNORM_NORM_2;VECTOR_TO_CVECTOR_CVECTOR_RE_IM]
 243 (*   THEN SIMP_TAC[NORM_POS_LE;POW_2_SQRT;NORM_MUL;real_div;REAL_MUL_LID] *)\r
 244   THEN SIMP_TAC[NORM_POS_LE;SQRT_POW_2;NORM_MUL;real_div;REAL_MUL_LID]\r
 245   THEN REWRITE_TAC[MESON[REAL_LT_IMP_LE;REAL_ABS_REFL;REAL_LE_INV;REAL_LE_MUL;\r
 246     eta0;k0] `abs (inv (eta0 * k0)) = inv (eta0 * k0)`]\r
 247   THEN REWRITE_TAC[REAL_INV_MUL;REAL_ARITH `(x*y)*z*t=x*(y*z)*t:real`;MATCH_MP\r
 248     REAL_MUL_LINV (GSYM (MATCH_MP REAL_LT_IMP_NE k0));REAL_MUL_LID]\r
 249   THEN REWRITE_TAC[COMPLEX_MUL_SYM;REAL_MUL_SYM]);;\r
 250 \r
 251 (* Helpers *)\r
 252 let IS_PLANE_WAVE_AT_INTERFACE_BOUNDARY_CONDITIONS = prove\r
 253   (`!i emf_i emf_r emf_t.\r
 254     is_plane_wave_at_interface i emf_i emf_r emf_t ==>\r
 255     !pt. pt IN (plane_of_interface i) ==> !t.\r
 256       boundary_conditions (emf_i + emf_r) emf_t (plane_of_interface i) pt t`,\r
 257   SIMP_TAC[FORALL_INTERFACE_THM;is_plane_wave_at_interface;plane_of_interface;\r
 258     LET_DEFs]);;\r
 259 \r
 260 let IS_PLANE_WAVE_AT_INTERFACE_IS_NORMAL_TO_PLANE = prove\r
 261   (`!i emf_i emf_r emf_t. is_plane_wave_at_interface i emf_i emf_r emf_t ==>\r
 262     is_normal_to_plane (normal_of_interface i) (plane_of_interface i)`,\r
 263   SIMP_TAC[is_plane_wave_at_interface;IS_VALID_INTERFACE_IS_NORMAL_TO_PLANE]);;\r
 264 \r
 265 let IS_PLANE_WAVE_AT_INTERFACE_PLANE = prove\r
 266   (`!i emf_i emf_r emf_t. is_plane_wave_at_interface i emf_i emf_r emf_t ==>\r
 267     plane (plane_of_interface i)`,\r
 268   SIMP_TAC[is_plane_wave_at_interface;IS_VALID_INTERFACE_PLANE]);;\r
 269 \r
 270 let IS_PLANE_WAVE_AT_INTERFACE_NON_NULL_NORMAL = prove\r
 271   (`!i emf_i emf_r emf_t. is_plane_wave_at_interface i emf_i emf_r emf_t ==>\r
 272     ~(normal_of_interface i = vec 0)`,\r
 273   SIMP_TAC[FORALL_INTERFACE_THM;is_plane_wave_at_interface;is_valid_interface;\r
 274     normal_of_interface;is_normal_to_plane;LET_DEFs]);;\r
 275 \r
 276 \r
 277 (***********************************)\r
 278 (* TE and TM modes                 *)\r
 279 (***********************************)\r
 280 \r
 281 let is_mode_axis = new_definition\r
 282   `is_mode_axis field (i:interface) emf_i emf_r emf_t v <=>\r
 283     orthogonal v (normal_of_interface i) /\ norm v = &1 /\ !r t.\r
 284     collinear_cvectors (field emf_i r t) (vector_to_cvector v)\r
 285     /\ collinear_cvectors (field emf_r r t) (vector_to_cvector v)\r
 286     /\ collinear_cvectors (field emf_t r t) (vector_to_cvector v)`;;\r
 287 \r
 288 let transverse_mode = new_definition\r
 289   `transverse_mode field (i:interface) emf_i emf_r emf_t <=>\r
 290     ?v. is_mode_axis field (i:interface) emf_i emf_r emf_t v`;;\r
 291 \r
 292 let TE_mode = new_definition `TE_mode = transverse_mode e_of_emf`;;\r
 293 let TM_mode = new_definition `TM_mode = transverse_mode h_of_emf`;;\r
 294 \r
 295 let mode_axis = new_definition `mode_axis field i emf_i emf_r emf_t =\r
 296   @v. is_mode_axis field i emf_i emf_r emf_t v`;;\r
 297 \r
 298 let TE_mode_axis = new_definition `TE_mode_axis = mode_axis e_of_emf`;;\r
 299 let TM_mode_axis = new_definition `TM_mode_axis = mode_axis h_of_emf`;;\r
 300 \r
 301 let TRANSVERSE_MODE_THM = prove\r
 302   (`!field i emf_i emf_r emf_t. transverse_mode field i emf_i emf_r emf_t <=>\r
 303     is_mode_axis field i emf_i emf_r emf_t (mode_axis field i emf_i emf_r emf_t)`,\r
 304   REWRITE_TAC[transverse_mode;mode_axis] THEN SELECT_ELIM_TAC\r
 305   THEN REWRITE_TAC[]);;\r
 306 \r
 307 let TE_MODE_THM = prove\r
 308   (`!i emf_i emf_r emf_t. TE_mode i emf_i emf_r emf_t <=>\r
 309     is_mode_axis e_of_emf i emf_i emf_r emf_t\r
 310       (TE_mode_axis i emf_i emf_r emf_t)`,\r
 311   REWRITE_TAC[TE_mode;TE_mode_axis;TRANSVERSE_MODE_THM]);;\r
 312 \r
 313 let TM_MODE_THM = prove\r
 314   (`!i emf_i emf_r emf_t. TM_mode i emf_i emf_r emf_t <=>\r
 315     is_mode_axis h_of_emf i emf_i emf_r emf_t \r
 316       (TM_mode_axis i emf_i emf_r emf_t)`,\r
 317   REWRITE_TAC[TM_mode;TM_mode_axis;TRANSVERSE_MODE_THM]);;\r
 318 \r
 319 let MODE_AXIS_ORTHOGONAL_N = prove\r
 320   (`!field i emf_i emf_r emf_t. transverse_mode field i emf_i emf_r emf_t ==>\r
 321     orthogonal (mode_axis field i emf_i emf_r emf_t) (normal_of_interface i)`,\r
 322   SIMP_TAC[TRANSVERSE_MODE_THM;is_mode_axis]);;\r
 323 \r
 324 let TE_MODE_AXIS_ORTHOGONAL_N = prove\r
 325   (`!i emf_i emf_r emf_t. TE_mode i emf_i emf_r emf_t ==>\r
 326     orthogonal (TE_mode_axis i emf_i emf_r emf_t) (normal_of_interface i)`,\r
 327   REWRITE_TAC[TE_mode;TE_mode_axis;MODE_AXIS_ORTHOGONAL_N]);;\r
 328 \r
 329 let TM_MODE_AXIS_ORTHOGONAL_N = prove\r
 330   (`!i emf_i emf_r emf_t. TM_mode i emf_i emf_r emf_t ==>\r
 331     orthogonal (TM_mode_axis i emf_i emf_r emf_t) (normal_of_interface i)`,\r
 332   REWRITE_TAC[TM_mode;TM_mode_axis;MODE_AXIS_ORTHOGONAL_N]);;\r
 333 \r
 334 let TRANSVERSE_MODE_PROJ = prove\r
 335   (`!field i emf_i emf_r emf_t. transverse_mode field i emf_i emf_r emf_t ==>\r
 336     !r t. let x = vector_to_cvector (mode_axis field i emf_i emf_r emf_t) in\r
 337     field emf_i r t = (field emf_i r t cdot x) % x\r
 338     /\ field emf_r r t = (field emf_r r t cdot x) % x\r
 339     /\ field emf_t r t = (field emf_t r t cdot x) % x`,\r
 340   REWRITE_TAC[TRANSVERSE_MODE_THM;is_mode_axis;LET_DEFs] THEN REPEAT STRIP_TAC\r
 341   THEN POP_ASSUM (STRIP_ASSUME_TAC o SPEC_ALL)\r
 342   THEN FIRST_ASSUM (ASSUME_TAC o REWRITE_RULE[NORM_EQ_0;GSYM \r
 343     VECTOR_TO_CVECTOR_ZERO_EQ] o MATCH_MP\r
 344     (REAL_ARITH `!x. x= &1 ==> ~(x= &0)`))\r
 345   THEN ASM_SIMP_TAC[COLLINEAR_RUNITREAL]);;\r
 346 \r
 347 let TE_MODE_PROJ = prove\r
 348   (`!i emf_i emf_r emf_t. TE_mode i emf_i emf_r emf_t ==> !r t.\r
 349     let x = vector_to_cvector (TE_mode_axis i emf_i emf_r emf_t) in\r
 350     e_of_emf emf_i r t = (e_of_emf emf_i r t cdot x) % x \r
 351     /\ e_of_emf emf_r r t = (e_of_emf emf_r r t cdot x) % x \r
 352     /\ e_of_emf emf_t r t = (e_of_emf emf_t r t cdot x) % x`,\r
 353   REWRITE_TAC[TE_mode;TE_mode_axis;TRANSVERSE_MODE_PROJ]);;\r
 354 \r
 355 let TM_MODE_PROJ = prove\r
 356   (`!i emf_i emf_r emf_t. TM_mode i emf_i emf_r emf_t ==> !r t.\r
 357     let x = vector_to_cvector (TM_mode_axis i emf_i emf_r emf_t) in\r
 358     h_of_emf emf_i r t = (h_of_emf emf_i r t cdot x) % x \r
 359     /\ h_of_emf emf_r r t = (h_of_emf emf_r r t cdot x) % x \r
 360     /\ h_of_emf emf_t r t = (h_of_emf emf_t r t cdot x) % x`,\r
 361   REWRITE_TAC[TM_mode;TM_mode_axis;TRANSVERSE_MODE_PROJ]);;\r
 362 \r
 363 let TE_MODE_PLANEWAVE_PROJ = prove\r
 364   (`!i emf_i emf_r emf_t. TE_mode i emf_i emf_r emf_t /\ is_plane_wave emf_i\r
 365     /\ is_plane_wave emf_r /\ is_plane_wave emf_t ==>\r
 366     let x = vector_to_cvector (TE_mode_axis i emf_i emf_r emf_t) in\r
 367     e_of_wave emf_i = (e_of_wave emf_i cdot x) % x\r
 368     /\ e_of_wave emf_r = (e_of_wave emf_r cdot x) % x\r
 369     /\ e_of_wave emf_t = (e_of_wave emf_t cdot x) % x`,\r
 370   REWRITE_TAC[IS_PLANE_WAVE] THEN REPEAT STRIP_TAC \r
 371   THEN ASM_CSQ_THEN TE_MODE_PROJ (MP_TAC o REWRITE_RULE[LET_DEFs])\r
 372   THEN ASSUM_LIST (REWRITE_TAC o mapfilter (REWRITE_RULE[EH_OF_EMF_PLANE_WAVE]\r
 373     o MATCH_MP (MESON[] `x=y ==> e_of_emf x = e_of_emf y`)))\r
 374   THEN REWRITE_TAC[CDOT_LMUL;GSYM CVECTOR_MUL_ASSOC;CVECTOR_MUL_LCANCEL;\r
 375     CEXP_NZ;LET_DEFs]);;\r
 376 \r
 377 let TM_MODE_PLANEWAVE_PROJ = prove\r
 378   (`!i emf_i emf_r emf_t. TM_mode i emf_i emf_r emf_t /\ is_plane_wave emf_i\r
 379     /\ is_plane_wave emf_r /\ is_plane_wave emf_t ==>\r
 380     let x = vector_to_cvector (TM_mode_axis i emf_i emf_r emf_t) in\r
 381   h_of_wave emf_i = (h_of_wave emf_i cdot x) % x\r
 382   /\ h_of_wave emf_r = (h_of_wave emf_r cdot x) % x\r
 383   /\ h_of_wave emf_t = (h_of_wave emf_t cdot x) % x`,\r
 384   REWRITE_TAC[IS_PLANE_WAVE] THEN REPEAT STRIP_TAC\r
 385   THEN ASM_CSQ_THEN TM_MODE_PROJ (MP_TAC o REWRITE_RULE[LET_DEFs])\r
 386   THEN ASSUM_LIST (REWRITE_TAC o mapfilter (REWRITE_RULE[EH_OF_EMF_PLANE_WAVE]\r
 387     o MATCH_MP (MESON[] `x=y ==> h_of_emf x = h_of_emf y`)))\r
 388   THEN REWRITE_TAC[CDOT_LMUL;GSYM CVECTOR_MUL_ASSOC;CVECTOR_MUL_LCANCEL;CEXP_NZ;\r
 389     LET_DEFs]);;\r
 390
 391