primitive_rules.ml

   1 (* ========================================================================= *)\r
   2 (*               Formalization of Electromagnetic Optics                     *)\r
   3 (*                                                                           *)\r
   4 (*            (c) Copyright, Sanaz Khan Afshar & Vincent Aravantinos 2011-14 *)\r
   5 (*                           Hardware Verification Group,                    *)\r
   6 (*                           Concordia University                            *)\r
   7 (*                                                                           *)\r
   8 (*                Contact:   <s_khanaf@encs.concordia.ca>                    *)\r
   9 (*                           <vincent@encs.concordia.ca>                     *)\r
  10 (*                                                                           *)\r
  11 (* This file deals with the non-trivial theorems called "primitive rules".   *)\r
  12 (* ========================================================================= *)\r
  13 \r
  14 \r
  15 let WAVE_ORTHOGONALITY = prove\r
  16   (`!emf. is_plane_wave emf ==> corthogonal (h_of_wave emf) (e_of_wave emf)`,\r
  17   REWRITE_TAC[IS_PLANE_WAVE;is_valid_emf;plane_wave;emf_at_point_mul;e_of_emf;\r
  18     h_of_emf;LET_DEF;LET_END_DEF]\r
  19   THEN REPEAT STRIP_TAC THEN REPLICATE_TAC 2 (POP_ASSUM (K ALL_TAC))\r
  20   THEN POP_ASSUM (fun x -> RULE_ASSUM_TAC (ONCE_REWRITE_RULE[x]))\r
  21   THEN RULE_ASSUM_TAC (REWRITE_RULE[BETA_THM;LET_DEF;LET_END_DEF])\r
  22   THEN REPEAT (POP_ASSUM MP_TAC)\r
  23   THEN SIMP_TAC[corthogonal;CDOT3;CVECTOR_MUL_COMPONENT;CNJ_MUL;\r
  24     SIMPLE_COMPLEX_ARITH `(x*y)*cnj z*t=(x*cnj z)*(y*t):complex`;\r
  25     GSYM COMPLEX_ADD_LDISTRIB;COMPLEX_ENTIRE;CEXP_NZ;CNJ_EQ_0]);;\r
  26 \r
  27 let NON_NULL_LEMMA = prove\r
  28   (`!emf v. ~(v = vec 0) /\ non_null_wave emf ==>\r
  29     let v_ccross = (ccross) (vector_to_cvector v) in\r
  30     ~(v_ccross (e_of_wave emf) = cvector_zero)\r
  31     \/ ~(v_ccross (h_of_wave emf) = cvector_zero)`,\r
  32   REPEAT GEN_TAC THEN CONV_TAC (DEPTH_CONV let_CONV)\r
  33   THEN ASM_CASES_TAC `vector_to_cvector v ccross e_of_wave emf = cvector_zero`\r
  34   THEN ASM_REWRITE_TAC[non_null_wave]\r
  35   THEN RULE_ASSUM_TAC (REWRITE_RULE[CCROSS_COLLINEAR_CVECTORS])\r
  36   THEN ASSUME_CONSEQUENCES (REWRITE_RULE[IMP_CONJ]\r
  37     CORTHOGONAL_COLLINEAR_CVECTORS)\r
  38   THEN REPEAT STRIP_TAC\r
  39   THEN SUBGOAL_THEN `~(vector_to_cvector (v:real^3) = cvector_zero)` ASSUME_TAC\r
  40   THENL ON_FIRST_GOAL \r
  41     (REWRITE_TAC[CART_EQ3;CVECTOR_ZERO_COMPONENT;VECTOR_TO_CVECTOR_COMPONENT;\r
  42       CX_INJ]\r
  43     THEN RULE_ASSUM_TAC (REWRITE_RULE[CART_EQ;VEC_COMPONENT;DIMINDEX_3;FORALL_3])\r
  44     THEN ASM_REWRITE_TAC[])\r
  45   THEN SUBGOAL_THEN\r
  46     `?a . ~(a=Cx(&0)) /\ vector_to_cvector v = a % e_of_wave emf` STRIP_ASSUME_TAC\r
  47   THENL ON_FIRST_GOAL (ASM_MESON_TAC[NON_NULL_COLLINEARS;COLLINEAR_CVECTORS_SYM])\r
  48   THEN ASSUME_CONSEQUENCES WAVE_ORTHOGONALITY\r
  49   THEN POP_ASSUM MP_TAC\r
  50   THEN POP_ASSUM (fun x ->\r
  51     RULE_ASSUM_TAC (REWRITE_RULE[x;CCROSS_LMUL;CVECTOR_MUL_EQ_0]))\r
  52   THEN POP_ASSUM (fun x ->\r
  53     RULE_ASSUM_TAC (REWRITE_RULE[x;CCROSS_COLLINEAR_CVECTORS]))\r
  54   THEN ASM_MESON_TAC[CORTHOGONAL_COLLINEAR_CVECTORS;CORTHOGONAL_SYM]);;\r
  55 \r
  56 let NON_NULL_LEMMA_PASTECART = prove\r
  57   (`!emf v. ~(v = vec 0) /\ non_null_wave emf ==>\r
  58     let v_ccross = (ccross) (vector_to_cvector v) in\r
  59     ~(pastecart (v_ccross (e_of_wave emf)) (v_ccross (h_of_wave emf)) =\r
  60       cvector_zero)`,\r
  61   REWRITE_TAC[PASTECART_EQ_CVECTOR_ZERO;DE_MORGAN_THM;NON_NULL_LEMMA]);;\r
  62 \r
  63 let BOUNDARY_CONDITIONS_FOR_PLANE_WAVES = prove\r
  64   (`!i emf_i emf_r emf_t.\r
  65     is_plane_wave_at_interface i emf_i emf_r emf_t ==>\r
  66     let p = plane_of_interface i in\r
  67     !n. is_normal_to_plane n p ==>\r
  68     let n_ccross = (ccross) (vector_to_cvector n) in\r
  69     !pt. pt IN p ==> !t.\r
  70       let plane_component = \f_of_wave emf. cexp (--ii * Cx((k_of_wave emf) dot\r
  71         pt - w_of_wave emf*t)) % n_ccross (f_of_wave emf) in\r
  72       plane_component e_of_wave emf_i + plane_component e_of_wave emf_r\r
  73         = plane_component e_of_wave emf_t\r
  74       /\ plane_component h_of_wave emf_i + plane_component h_of_wave emf_r\r
  75         = plane_component h_of_wave emf_t`,\r
  76   REWRITE_TAC[FORALL_INTERFACE_THM;plane_of_interface;LET_DEF;LET_END_DEF;\r
  77     is_plane_wave_at_interface;non_null_wave;IS_PLANE_WAVE;plane_wave;\r
  78     emf_at_point_mul;e_of_emf;h_of_emf;LET_DEF;LET_END_DEF;map_triple;o_DEF]\r
  79   THEN REPEAT STRIP_TAC\r
  80   THEN POP_ASSUM (fun x -> FIRST_X_ASSUM (fun y -> MP_TAC (MATCH_MP y x)))\r
  81   THEN ASM (GEN_REWRITE_TAC (RATOR_CONV o DEPTH_CONV)) []\r
  82   THEN REWRITE_TAC[boundary_conditions;emf_add;e_of_emf;h_of_emf;LET_DEF;\r
  83     LET_END_DEF;CCROSS_RADD;CCROSS_RMUL]\r
  84   THEN DISCH_THEN (C ASM_CSQ_THEN STRIP_ASSUME_TAC) THEN ASM_REWRITE_TAC[]);;\r
  85 \r
  86 (* We combine the E and H field as one complex^6 vector. \r
  87  * Convenient for some proofs. *)\r
  88 let PASTECART_BOUNDARY_CONDITIONS_FOR_PLANE_WAVES = prove\r
  89   (`!i emf_i emf_r emf_t. is_plane_wave_at_interface i emf_i emf_r emf_t ==>\r
  90   let p = plane_of_interface i in\r
  91   !n. is_normal_to_plane n p ==>\r
  92   let n_ccross = (ccross) (vector_to_cvector n) in\r
  93         !pt. pt IN p ==> !t.\r
  94     let plane_component = \emf.\r
  95       cexp (--ii * Cx((k_of_wave emf) dot pt - w_of_wave emf*t)) % pastecart\r
  96         (n_ccross (e_of_wave emf)) (n_ccross (h_of_wave emf)) in\r
  97     plane_component emf_i + plane_component emf_r = plane_component emf_t`,\r
  98     REWRITE_TAC[LET_DEF;LET_END_DEF] THEN REPEAT STRIP_TAC\r
  99     THEN ASM_CSQ_THEN (REWRITE_RULE[LET_DEF;LET_END_DEF]\r
 100       BOUNDARY_CONDITIONS_FOR_PLANE_WAVES) (C ASM_CSQ_THEN (C ASM_CSQ_THEN\r
 101         (MP_TAC o SPEC_ALL)))\r
 102     THEN PASTECART_TAC[GSYM PASTECART_CVECTOR_MUL;PASTECART_CVECTOR_ADD]);;\r
 103 \r
 104 let EXISTS_NORMAL_OF_PLANE_INTERFACE = prove\r
 105   (`!i emf_i emf_r emf_t. is_plane_wave_at_interface i emf_i emf_r emf_t ==>\r
 106     ?n. is_normal_to_plane n (plane_of_interface i)`,\r
 107   REWRITE_TAC[FORALL_INTERFACE_THM;LET_DEF;LET_END_DEF;\r
 108     is_plane_wave_at_interface;is_valid_interface;plane_of_interface]\r
 109   THEN MESON_TAC[EXISTS_NORMAL_OF_PLANE]);;\r
 110 \r
 111 let FREQUENCY_CONSERVATION = prove\r
 112   (`!i emf_i emf_r emf_t. is_plane_wave_at_interface i emf_i emf_r emf_t ==>\r
 113   (non_null_wave emf_r ==> w_of_wave emf_r = w_of_wave emf_i)\r
 114   /\ (non_null_wave emf_t ==> w_of_wave emf_t = w_of_wave emf_i)`,\r
 115   REWRITE_TAC[FORALL_INTERFACE_THM] THEN REPEAT STRIP_TAC\r
 116   THEN ASM_CSQ_THEN EXISTS_NORMAL_OF_PLANE_INTERFACE STRIP_ASSUME_TAC\r
 117   THEN SUBGOAL_THEN `~(n' = vec 0:real^3) /\ plane (p:plane)`\r
 118     STRIP_ASSUME_TAC THEN\r
 119   TRY (RULE_ASSUM_TAC (REWRITE_RULE[is_plane_wave_at_interface;LET_DEF;\r
 120     LET_END_DEF;is_valid_interface;is_normal_to_plane])\r
 121     THEN ASM_REWRITE_TAC[] THEN NO_TAC)\r
 122   THEN ASM_CSQ_THEN PLANE_NON_EMPTY (STRIP_ASSUME_TAC o REWRITE_RULE[GSYM\r
 123     MEMBER_NOT_EMPTY])\r
 124   THEN ASM_CSQ_THEN (REWRITE_RULE[LET_DEF;LET_END_DEF]\r
 125     PASTECART_BOUNDARY_CONDITIONS_FOR_PLANE_WAVES) (C ASM_CSQ_THEN ASSUME_TAC)\r
 126   THEN RULE_ASSUM_TAC (REWRITE_RULE[plane_of_interface;LET_DEF;LET_END_DEF])\r
 127   THEN POP_ASSUM (C ASM_CSQ_THEN MP_TAC)\r
 128   THEN REWRITE_TAC[CX_SUB;CX_MUL;SIMPLE_COMPLEX_ARITH\r
 129     `--ii*(x-y*z) = (ii*y)*z+ --ii*x`;CEXP_ADD;GSYM CVECTOR_MUL_ASSOC]\r
 130   THEN ONCE_REWRITE_TAC[MESON[COMPLEX_EQ_MUL_LCANCEL;II_NZ;CX_INJ]\r
 131     `x=y <=> ii * Cx x = ii * Cx y`]\r
 132   THENL\r
 133     (let APPLY_FREQ_EQ_TAC x =\r
 134       DISCH_THEN (MP_TAC o MATCH_MP (REWRITE_RULE[MESON[]\r
 135         `(A /\ B /\ C ==> D) <=> (C ==> A ==> B ==> D)`] x)) in\r
 136     map APPLY_FREQ_EQ_TAC [ VEC_WAVE_SUM_EQ_WEAK2; VEC_WAVE_SUM_EQ_WEAK1])\r
 137   THEN ANTS_TAC\r
 138   THEN\r
 139   let APPLY_NON_NULL_LEMMA = REWRITE_TAC[CVECTOR_MUL_EQ_0;CEXP_NZ]\r
 140     THEN MATCH_MP_TAC (CONV_RULE (DEPTH_CONV let_CONV) NON_NULL_LEMMA_PASTECART) in\r
 141   REPEAT (ANTS_TAC ORELSE APPLY_NON_NULL_LEMMA)\r
 142   THEN ASM_MESON_TAC[is_plane_wave_at_interface]);;\r
 143 \r
 144 let IS_PLANE_WAVE_AT_INTERFACE_THMS =\r
 145   [is_plane_wave_at_interface;LET_DEF;LET_END_DEF;map_triple;o_DEF;\r
 146     is_valid_interface];;\r
 147 \r
 148 let K_PLANE_PROJECTION_CONSERVATION = prove\r
 149   (`!i emf_i emf_r emf_t. is_plane_wave_at_interface i emf_i emf_r emf_t ==>\r
 150     let n = unit (normal_of_interface i) in\r
 151     (non_null_wave emf_r ==>\r
 152       projection_on_hyperplane (k_of_wave emf_r) n =\r
 153         projection_on_hyperplane (k_of_wave emf_i) n)\r
 154     /\ (non_null_wave emf_t ==>\r
 155       projection_on_hyperplane (k_of_wave emf_t) n =\r
 156         projection_on_hyperplane (k_of_wave emf_i) n)`,\r
 157     REWRITE_TAC[FORALL_INTERFACE_THM] THEN REPEAT GEN_TAC\r
 158     THEN DISCH_THEN (DISTRIB [MP_TAC; LABEL_TAC "*" o MATCH_MP\r
 159       PASTECART_BOUNDARY_CONDITIONS_FOR_PLANE_WAVES])\r
 160     THEN REWRITE_TAC([normal_of_interface] @ IS_PLANE_WAVE_AT_INTERFACE_THMS)\r
 161     THEN REPEAT STRIP_TAC\r
 162     THEN REMOVE_THEN "*" (C ASM_CSQ_THEN ASSUME_TAC o\r
 163       REWRITE_RULE[LET_DEF;LET_END_DEF;plane_of_interface])\r
 164     THEN ASM_CSQ_THEN FORALL_PLANE_THM_2 STRIP_ASSUME_TAC\r
 165     THEN POP_ASSUM (RULE_ASSUM_TAC o SINGLE REWRITE_RULE)\r
 166     THEN FIRST_ASSUM (STRIP_ASSUME_TAC o CONV_RULE\r
 167       (REWR_CONV is_normal_to_plane))\r
 168     THEN ASM_SIMP_TAC[UNIT_THM;PROJECTION_ON_HYPERPLANE_THM]\r
 169     THEN ASM_CSQ_THEN PLANE_DECOMP_DOT (C ASM_CSQ_THEN (C\r
 170       ASM_CSQ_THEN ASSUME_TAC))\r
 171     THEN MAP_EVERY (fun x -> REWRITE_TAC[VECTOR_ARITH x]\r
 172       THEN ASSUM_LIST (GEN_REWRITE_TAC (RATOR_CONV o ONCE_DEPTH_CONV)))\r
 173       [`a-b=c-d <=> a=c+b-d:real^N`;`a=c+b-d <=> c=a-b+d:real^N`]\r
 174     THEN REWRITE_TAC[VECTOR_ARITH `a+b+c=(d+e+f)-f+c <=> a+b=d+e:real^N`]\r
 175     THEN ASM_CSQ_THEN BASIS_NON_NULL (fun x -> FIRST_ASSUM\r
 176       (STRIP_ASSUME_TAC o REWRITE_RULE[IN_INSERT;IN_SING;\r
 177       MESON[] `(!x. x=a \/ x=b ==> p x) <=> p a /\ p b`;UNIT_EQ_ZERO]\r
 178       o MATCH_MP x o CONJUNCT1 o CONV_RULE\r
 179         (REWR_CONV is_orthogonal_plane_basis)))\r
 180     THEN ASM_SIMP_TAC[UNIT_UNIT] THEN MK_COMB_TAC\r
 181     THENL [AP_TERM_TAC;ALL_TAC;AP_TERM_TAC;ALL_TAC]\r
 182     THEN AP_THM_TAC THEN AP_TERM_TAC \r
 183     THEN ONCE_REWRITE_TAC[MESON[COMPLEX_EQ_MUL_LCANCEL;II_NZ;CX_INJ;\r
 184       COMPLEX_NEG_EQ_0] `x=y <=> --ii * Cx x = --ii * Cx y`]\r
 185     THEN RULE_ASSUM_TAC (REWRITE_RULE[\r
 186       VECTOR_ARITH `x dot (y+a%z+b%t) = x dot y+(x dot z)*a+(x dot t)*b`;\r
 187       SIMPLE_COMPLEX_ARITH `--ii * Cx ((a+b*b'+c*c')-d) = (--ii * Cx b)\r
 188         * Cx b' + (--ii * Cx c) * Cx c' + --ii * Cx a + ii * Cx d`;\r
 189       CEXP_ADD])\r
 190     THENL (map (fun f -> FIRST_X_ASSUM (ASSUME_TAC o f)) [\r
 191       funpow 2 (SPEC `&0` o ONCE_REWRITE_RULE[SWAP_FORALL_THM]);\r
 192       SPEC `&0` o ONCE_REWRITE_RULE[SWAP_FORALL_THM] o SPEC `&0`;\r
 193       funpow 2 (SPEC `&0` o ONCE_REWRITE_RULE[SWAP_FORALL_THM]);\r
 194       SPEC `&0` o ONCE_REWRITE_RULE[SWAP_FORALL_THM] o SPEC `&0`;\r
 195     ])\r
 196     THEN RULE_ASSUM_TAC (REWRITE_RULE[COMPLEX_MUL_RZERO;CEXP_0;COMPLEX_MUL_RID;\r
 197       REAL_MUL_RZERO;GSYM CVECTOR_MUL_ASSOC;CVECTOR_MUL_ID])\r
 198     THENL\r
 199     (let lemma = MESON[] `(!x y z t u v. p x y z t v u ==> q x y z /\ r t v u)\r
 200       ==> (!x y z t u v. p x y z t v u ==> q x y z)` in\r
 201     let APPLY_FREQ_EQ_TAC x =\r
 202       POP_ASSUM (DISTRIB [ASSUME_TAC;MP_TAC o MATCH_MP (REWRITE_RULE[MESON[]\r
 203         `(A /\ B /\ C ==> D) <=> (C ==> A ==> B ==> D)`](MATCH_MP lemma x))])\r
 204     in\r
 205     map APPLY_FREQ_EQ_TAC [VEC_WAVE_SUM_EQ_WEAK2;VEC_WAVE_SUM_EQ_WEAK2;\r
 206       VEC_WAVE_SUM_EQ_WEAK1;VEC_WAVE_SUM_EQ_WEAK1])\r
 207     THEN ANTS_TAC\r
 208     THEN\r
 209       let APPLY_NON_NULL_LEMMA =\r
 210         REWRITE_TAC[CVECTOR_MUL_EQ_0;CEXP_NZ]\r
 211         THEN MATCH_MP_TAC (CONV_RULE (DEPTH_CONV let_CONV)\r
 212           NON_NULL_LEMMA_PASTECART)\r
 213       in\r
 214       REPEAT (ANTS_TAC ORELSE APPLY_NON_NULL_LEMMA)\r
 215     THEN ASM_REWRITE_TAC[]);;\r
 216 \r
 217 let LAW_OF_REFLECTION = prove\r
 218   (`!i emf_i emf_r emf_t. is_plane_wave_at_interface i emf_i emf_r emf_t ==>\r
 219     let n = unit (normal_of_interface i) in\r
 220     non_null_wave emf_r ==>\r
 221       symetric_vectors_wrt (--(k_of_wave emf_r)) (k_of_wave emf_i) n`,\r
 222     REWRITE_TAC[FORALL_INTERFACE_THM;LET_DEFs] THEN REPEAT STRIP_TAC\r
 223     THEN ASM_CSQ_THEN (REWRITE_RULE[LET_DEFs] K_PLANE_PROJECTION_CONSERVATION)\r
 224       (C ASM_CSQ_THEN MP_TAC o CONJUNCT1)\r
 225     THEN ASM_CSQ_THEN (MESON[is_plane_wave_at_interface]\r
 226       `is_plane_wave_at_interface i emf_i emf_r emf_t ==> is_valid_interface i`)\r
 227       (DISTRIB [ASSUME_TAC; STRIP_ASSUME_TAC o\r
 228         REWRITE_RULE[LET_DEFs;is_valid_interface]])\r
 229     THEN ASM_SIMP_TAC[normal_of_interface;LET_DEFs;\r
 230       PROJECTION_ON_HYPERPLANE_THM;symetric_vectors_wrt;\r
 231       NORMAL_OF_INTERFACE_NON_NULL;UNIT_THM;UNIT_EQ_ZERO]\r
 232     THEN DISCH_TAC\r
 233     THEN SUBGOAL_THEN `!x:real^3. orthogonal (x - (x dot unit n) % unit n) ((x\r
 234       dot unit n) % unit n)` ASSUME_TAC\r
 235     THENL ON_FIRST_GOAL (ASM_MESON_TAC [ORTHOGONAL_RUNIT;ORTHOGONAL_CLAUSES;\r
 236         SUB_UNIT_NORMAL_IS_ORTHOGONAL_TO_NORMAL])\r
 237     THEN FIRST_ASSUM (REPEAT_TCL STRIP_THM_THEN (fun x ->\r
 238       if contains_sub_term_name "k_of_wave" (concl x) then ASSUME_TAC x\r
 239       else ALL_TAC)\r
 240       o REWRITE_RULE[LET_DEFs;map_triple;o_DEF] o CONV_RULE (REWR_CONV\r
 241         is_plane_wave_at_interface))\r
 242     THEN REPLICATE_TAC 3 (POP_ASSUM (K ALL_TAC))\r
 243     THEN POP_ASSUM (fun _ -> POP_ASSUM (fun x -> POP_ASSUM (fun y -> MP_TAC\r
 244       (REWRITE_RULE[NORM_EQ] (TRANS x (GSYM y))))))\r
 245     THEN FIRST_ASSUM (ASSUME_TAC o SPEC `k_of_wave emf`)\r
 246     THEN ASM_CSQ_THEN ORTHOGONAL_SQR_NORM (SINGLE REWRITE_TAC)\r
 247     THEN ASM_REWRITE_TAC[REAL_EQ_ADD_LCANCEL;DOT_LMUL;DOT_RMUL;DOT_SQUARE_NORM]\r
 248     THEN SUBGOAL_TAC "" `~(n = vec 0 :real^3)` \r
 249       [ASM_MESON_TAC[is_normal_to_plane]]\r
 250     THEN ASM_SIMP_TAC[UNIT_THM;REAL_POW_2;REAL_MUL_RID]\r
 251     THEN REWRITE_TAC[GSYM REAL_POW_2;GSYM REAL_EQ_SQUARE_ABS;real_abs]\r
 252     THEN REPEAT COND_CASES_TAC THEN RULE_ASSUM_TAC (REWRITE_RULE \r
 253       [real_ge;REWRITE_RULE[real_lt;MESON[] `(~p <=> ~q) <=> (p <=> q)`]\r
 254       DOT_RUNIT_LT0])\r
 255     THENL [\r
 256       FIRST_X_ASSUM (fun x -> FIRST_X_ASSUM (ASSUME_TAC \r
 257         o ONCE_REWRITE_RULE[GSYM DOT_RUNIT_EQ0] o GSYM\r
 258         o CONV_RULE (REWR_CONV REAL_LE_ANTISYM) o CONJ x))\r
 259       THEN ASM_REWRITE_TAC[DOT_LNEG;REAL_NEG_0;REAL_MUL_RZERO;VECTOR_MUL_LZERO;\r
 260         VECTOR_ARITH `--x+y=vec 0 <=> x=y`]\r
 261       THEN DISCH_THEN (RULE_ASSUM_TAC o SINGLE REWRITE_RULE o GSYM)\r
 262       THEN POP_ASSUM (RULE_ASSUM_TAC o SINGLE REWRITE_RULE)\r
 263       THEN RULE_ASSUM_TAC (REWRITE_RULE[VECTOR_MUL_LZERO;VECTOR_SUB_RZERO])\r
 264       THEN ASM_REWRITE_TAC[];\r
 265       ASM_MESON_TAC[REAL_ARITH `x > &0 ==> &0 <= x`];\r
 266       DISCH_THEN (ASSUME_TAC o GSYM)\r
 267       THEN FIRST_X_ASSUM (fun x -> ignore (term_match [] `x-y=z-t` (concl x));\r
 268         MP_TAC x)\r
 269       THEN POP_ASSUM (fun x -> REWRITE_TAC(x::[VECTOR_MUL_LNEG;DOT_LNEG;\r
 270         REAL_MUL_RNEG;VECTOR_ARITH `x-y=z- --y <=> --x+z = --(&2%y)`;\r
 271         VECTOR_MUL_ASSOC]));\r
 272       ASM_MESON_TAC[REAL_ARITH `x > &0 ==> &0 <= x`];\r
 273     ]);;\r
 274 \r
 275 let PLANE_OF_INCIDENCE_LAW = prove\r
 276   (`!i emf_i emf_r emf_t.\r
 277     is_plane_wave_at_interface i emf_i emf_r emf_t /\ non_null_wave emf_r\r
 278     /\ non_null_wave emf_t ==>\r
 279     coplanar {vec 0, k_of_wave emf_i, k_of_wave emf_r, k_of_wave emf_t,\r
 280       normal_of_interface i}`,\r
 281   REWRITE_TAC[FORALL_INTERFACE_THM;LET_DEFs;normal_of_interface]\r
 282   THEN REPEAT STRIP_TAC\r
 283   THEN REWRITE_TAC[coplanar] THEN REPEAT STRIP_TAC\r
 284   THEN MAP_EVERY EXISTS_TAC [`vec 0:real^3`;`k_of_wave emf_i`;`unit n:real^3`]\r
 285   THEN ASM_CSQ_THEN (MESON[is_plane_wave_at_interface]\r
 286     `is_plane_wave_at_interface i emf_i emf_r emf_t ==> is_valid_interface i`)\r
 287     (DISTRIB [ASSUME_TAC; STRIP_ASSUME_TAC o\r
 288       REWRITE_RULE[LET_DEFs;is_valid_interface]])\r
 289   THEN ASM_CSQ_THEN (REWRITE_RULE[LET_DEFs] K_PLANE_PROJECTION_CONSERVATION)\r
 290     (DISTRIB (map ((o) (C ASM_CSQ_THEN ASSUME_TAC)) [CONJUNCT1;CONJUNCT2]))\r
 291   THEN REWRITE_TAC[INSERT_SUBSET;SING_SUBSET] THEN REPEAT CONJ_TAC\r
 292   THENL \r
 293   let IN_SET_TAC = MATCH_MP_TAC HULL_INC THEN SET_TAC[] in\r
 294   let COMBINATION_TAC =\r
 295     POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC \r
 296     THEN ASM_SIMP_TAC[AFFINE_HULL_3_ZERO;IN_ELIM_THM;UNIV;normal_of_interface;\r
 297       LET_DEFs;PROJECTION_ON_HYPERPLANE_THM;symetric_vectors_wrt;\r
 298       NORMAL_OF_INTERFACE_NON_NULL;UNIT_THM;UNIT_EQ_ZERO;\r
 299       VECTOR_ARITH `x-a%y=z-b%y <=> x= &1%z+(a-b)%y`]\r
 300     THEN MESON_TAC[]\r
 301   in\r
 302   [ IN_SET_TAC; IN_SET_TAC; COMBINATION_TAC; COMBINATION_TAC;\r
 303     REWRITE_TAC[AFFINE_HULL_3_ZERO;IN_ELIM_THM;UNIV]\r
 304     THEN MAP_EVERY EXISTS_TAC [`&0`;`norm (n:real^3)`]\r
 305     THEN REWRITE_TAC[VECTOR_MUL_LZERO;VECTOR_ADD_LID]\r
 306     THEN MATCH_MP_TAC UNIT_INTRO THEN ASM_MESON_TAC[is_normal_to_plane]]);;\r
 307 \r
 308 let SNELL_LAW = prove\r
 309   (`!i emf_i emf_r emf_t.\r
 310     is_plane_wave_at_interface i emf_i emf_r emf_t /\ non_null_wave emf_t ==>\r
 311     let theta = \emf. vector_angle (k_of_wave emf) (normal_of_interface i) in\r
 312     n1_of_interface i * sin (theta emf_i) =\r
 313       n2_of_interface i * sin (theta emf_t)`,\r
 314   REWRITE_TAC[FORALL_INTERFACE_THM;LET_DEFs;n1_of_interface;n2_of_interface;\r
 315     normal_of_interface]\r
 316   THEN REPEAT STRIP_TAC\r
 317   THEN FIRST_ASSUM (STRIP_ASSUME_TAC o REWRITE_RULE[LET_DEFs;map_triple;o_DEF;\r
 318     is_valid_interface;IS_PLANE_WAVE;non_null_wave]\r
 319     o CONV_RULE (REWR_CONV is_plane_wave_at_interface))\r
 320   THEN SUBGOAL_TAC ""\r
 321     `~(k_of_wave emf_i = vec 0) /\ ~(k_of_wave emf_t = vec 0)` \r
 322     [ASM_REWRITE_TAC[]]\r
 323   THEN SUBGOAL_TAC "" `~(n = vec 0:real^3)` [ASM_MESON_TAC[is_normal_to_plane]]\r
 324   THEN ASSUM_LIST (SIMP_TAC o (@) [REWRITE_RULE[DE_MORGAN_THM;\r
 325     MESON[] `(p\/q==>r) <=> (p==>r) /\ (q==>r)`] (CONV_RULE (DEPTH_CONV\r
 326       COND_ELIM_CONV) vector_angle)]\r
 327     o filter (fun x -> not (contains_sub_term_name "norm" (concl x))))\r
 328   THEN SUBGOAL_THEN\r
 329     `(k_of_wave emf_i dot unit n) / (k0*n1) =\r
 330       (k_of_wave emf_i dot n) / (norm (k_of_wave emf_i) * norm n)\r
 331     /\ (k_of_wave emf_t dot unit n) / (k0*n2) =\r
 332       (k_of_wave emf_t dot n) / (norm (k_of_wave emf_t) * norm n)`\r
 333     ASSUME_TAC\r
 334   THENL ON_FIRST_GOAL (ASM_REWRITE_TAC[unit;DOT_RMUL;real_div;\r
 335     REAL_ARITH `(x*y)*z=y*(z*x):real`;REAL_INV_MUL])\r
 336   THEN SIMP_TAC[REWRITE_RULE[REAL_ABS_BOUNDS] NORM_CAUCHY_SCHWARZ_DIV;SIN_ACS;\r
 337     GSYM REAL_EQ_SQUARE_ABS]\r
 338   THEN ASM_CSQ_THEN (REWRITE_RULE[LET_DEFs] K_PLANE_PROJECTION_CONSERVATION) \r
 339     (C ASM_CSQ_THEN MP_TAC o CONJUNCT2)\r
 340   THEN ASM_SIMP_TAC[normal_of_interface;LET_DEFs;PROJECTION_ON_HYPERPLANE_THM;\r
 341     NORMAL_OF_INTERFACE_NON_NULL;UNIT_THM;UNIT_EQ_ZERO]\r
 342   THEN DISCH_THEN (MP_TAC o MATCH_MP (MESON[] `x=y ==> x dot x = y dot y`))\r
 343   THEN SUBGOAL_THEN `!x:real^3. orthogonal (x - (x dot unit n) % unit n) ((x\r
 344     dot unit n) % unit n)` ASSUME_TAC\r
 345   THENL ON_FIRST_GOAL (ASM_MESON_TAC[ORTHOGONAL_RUNIT;ORTHOGONAL_CLAUSES;\r
 346     SUB_UNIT_NORMAL_IS_ORTHOGONAL_TO_NORMAL])\r
 347   THEN ASM_SIMP_TAC[REWRITE_RULE[REAL_ARITH `x=y+z <=> y=x-z:real`] \r
 348     ORTHOGONAL_SQR_NORM;DOT_SQUARE_NORM;NORM_MUL;UNIT_THM;REAL_MUL_RID;\r
 349     REAL_POW2_ABS]\r
 350   THEN SUBGOAL_TAC "" `~(k0*n2 = &0) /\ ~(k0*n1 = &0)`\r
 351     [ASM_MESON_TAC[NORM_EQ_0]]\r
 352   THEN SUBGOAL_THEN `&0 < inv(k0*n1)` ASSUME_TAC\r
 353   THENL ON_FIRST_GOAL (ASM_REWRITE_TAC[REAL_LT_INV_EQ;REAL_LT_LE]\r
 354     THEN ASM_MESON_TAC[NORM_POS_LE])\r
 355   THEN SUBGOAL_THEN `~((k0*n2) pow 2 = &0) /\ ~(inv ((k0 * n2) pow 2) = &0)`\r
 356     STRIP_ASSUME_TAC\r
 357   THENL ON_FIRST_GOAL (REWRITE_TAC[REAL_POW_EQ_0;REAL_INV_EQ_0]\r
 358     THEN ASM_ARITH_TAC)\r
 359   THEN POP_ASSUM (fun x -> DISCH_THEN (MP_TAC o\r
 360     ONCE_REWRITE_RULE [REWRITE_RULE[x] (GENL [`x:real`;`y:real`] (SPECL\r
 361       [`x:real`;`y:real`;`inv ((k0 * n2:real) pow 2)`] (GSYM\r
 362       REAL_EQ_MUL_RCANCEL)))]))\r
 363   THEN ASM_SIMP_TAC[REAL_SUB_RDISTRIB;REAL_MUL_RINV;GSYM real_div;\r
 364     GSYM REAL_POW_DIV;REAL_DIV_REFL;REAL_POW_ONE]\r
 365   THEN DISCH_THEN (K ALL_TAC)\r
 366   THEN MATCH_MP_TAC (MESON[SQRT_MUL;POW_2_SQRT;REAL_LE_POW_2]\r
 367     `!x y. &0 <= x /\ &0 <= y /\ &0 <= z /\ &0 <= t /\ sqrt(x pow 2 * y) =\r
 368       sqrt(z pow 2*t) ==> x * sqrt y = z * sqrt t`)\r
 369   THEN REPEAT CONJ_TAC THENL [\r
 370     ASM_REAL_ARITH_TAC;\r
 371     REWRITE_TAC[REAL_SUB_LE;ABS_SQUARE_LE_1]\r
 372     THEN ASM_MESON_TAC[NORM_CAUCHY_SCHWARZ_DIV];\r
 373     ASM_REAL_ARITH_TAC;\r
 374     REWRITE_TAC[REAL_POW_DIV;REAL_ARITH `x/y-z/y=(x-z)/y:real`]\r
 375     THEN MATCH_MP_TAC REAL_LE_DIV THEN CONJ_TAC THENL [\r
 376       REWRITE_TAC[REAL_SUB_LE] THEN MATCH_MP_TAC REAL_POW_LE2 THEN CONJ_TAC\r
 377       THENL [\r
 378         REWRITE_TAC[unit;DOT_RMUL] THEN MATCH_MP_TAC REAL_LE_MUL\r
 379         THEN REWRITE_TAC[REAL_LE_INV_EQ;NORM_POS_LE] THEN ASM_ARITH_TAC;\r
 380         FIRST_ASSUM (SINGLE ONCE_REWRITE_TAC o REWRITE_RULE[GSYM real_div]\r
 381           o MATCH_MP (GSYM REAL_LE_RMUL_EQ))\r
 382         THEN ASM_SIMP_TAC[REAL_DIV_REFL]\r
 383         THEN ASM_MESON_TAC[REWRITE_RULE[REAL_ABS_BOUNDS] \r
 384           NORM_CAUCHY_SCHWARZ_DIV]\r
 385       ];\r
 386       MATCH_ACCEPT_TAC REAL_LE_POW_2;\r
 387     ];\r
 388     AP_TERM_TAC THEN SUBGOAL_TAC "" `~(k0 = &0) /\ ~(n1 = &0) /\ ~(n2 = &0)`\r
 389       [ASM_MESON_TAC[REAL_MUL_LZERO;REAL_MUL_RZERO]]\r
 390     THEN ASM_SIMP_TAC[real_div;REAL_INV_MUL;\r
 391       REAL_ARITH `(x*y)*inv x*inv z=(x*inv x)*y*inv z:real`;REAL_MUL_RINV;\r
 392       REAL_MUL_LID;REAL_SUB_LDISTRIB;REAL_MUL_RID]\r
 393     THEN ASM_SIMP_TAC[GSYM REAL_POW_MUL;\r
 394       REAL_ARITH `x*y*inv x=(x*inv x)*y:real`;\r
 395       REAL_ARITH `x*y*(inv z*inv x)*t=(x*inv x)*y*inv z*t:real`;\r
 396       REAL_ARITH `x*y*inv z*inv x=(x*inv x)*y*inv z:real`;\r
 397       REAL_MUL_RINV;REAL_MUL_LID;REAL_INV_MUL]\r
 398     THEN REWRITE_TAC[REAL_ARITH `x*inv y*inv z=(inv z*x)*inv y:real`;\r
 399       GSYM DOT_RMUL;unit]\r
 400   ]);;\r
 401 \r
 402 let phase_shift_at_plane = new_definition\r
 403   `phase_shift_at_plane p n emf =\r
 404     k_of_wave emf dot (@a. a % unit n IN p) % unit n`;;\r
 405 \r
 406 let PLANE_WAVE_WITH_PHASE_SHIFT_AT_PLANE = prove\r
 407   (`!emf. is_plane_wave emf ==> !p. plane p ==> !n. is_normal_to_plane n p ==>\r
 408   !r. r IN p ==> !t.\r
 409   emf r t = cexp (--ii * Cx(projection_on_hyperplane (k_of_wave emf) (unit n)\r
 410     dot r - w_of_wave emf * t + phase_shift_at_plane p n emf))\r
 411     % eh_of_wave emf`,\r
 412   let tmp = DISCH_ALL (GSYM (UNDISCH (ISPECL [`k_of_wave emf`;`unit n:real^3`]\r
 413     PROJECTION_ON_HYPERPLANE_DECOMPOS))) in\r
 414   let tmp' = UNDISCH_ALL (IMP_TRANS (SPEC `n:real^3` (UNDISCH (SPEC `p:plane`\r
 415     NORMAL_OF_PLANE_NON_NULL))) (IMP_TRANS (ISPEC `n:real^3` UNIT_THM) tmp)) in\r
 416   REWRITE_TAC[LET_DEF;LET_END_DEF;IS_PLANE_WAVE;plane_wave]\r
 417   THEN REPEAT STRIP_TAC\r
 418   THEN FIRST_ASSUM (let thm = MESON[] `f=g ==> g x y=z ==> f x y=z` in\r
 419     fun x -> MATCH_MP_TAC (MATCH_MP thm x))\r
 420   THEN REWRITE_TAC[emf_at_point_mul;PAIR_EQ;FUN_EQ_THM;eh_of_wave;e_of_emf;\r
 421     h_of_emf;LET_DEF;LET_END_DEF]\r
 422   THEN REPEAT (FIRST[CONJ_TAC;AP_THM_TAC;AP_TERM_TAC;GEN_TAC])\r
 423   THEN REWRITE_TAC[REAL_ARITH `x-y=(z-y)+t <=> x=t+z:real`]\r
 424   THEN GEN_REWRITE_TAC (RATOR_CONV o ONCE_DEPTH_CONV) \r
 425     [ONCE_REWRITE_RULE[VECTOR_ADD_SYM] tmp']\r
 426   THEN REWRITE_TAC[DOT_LADD;REAL_EQ_ADD_RCANCEL;phase_shift_at_plane]\r
 427   THEN ABBREV_TAC `a = @a. a % unit n IN (p:plane)`\r
 428   THEN GEN_REWRITE_TAC (RATOR_CONV o ONCE_DEPTH_CONV) \r
 429     [VECTOR_ARITH `v dot r = v dot (r - a % unit n + a % unit n:real^3)`]\r
 430   THEN REWRITE_TAC[DOT_RADD;DOT_RMUL;DOT_LMUL;REAL_ADD_LDISTRIB]\r
 431   THEN ASM_REWRITE_TAC[MATCH_MP (UNIT_DOT_UNIT_SELF)\r
 432     (STRIP_RULE NORMAL_OF_PLANE_NON_NULL);REAL_ARITH `x+y*z* &1=z*y <=> x= &0`]\r
 433   THEN REWRITE_TAC[REAL_ENTIRE;GSYM orthogonal;ORTHOGONAL_LUNIT] THEN DISJ2_TAC\r
 434   THEN ONCE_REWRITE_TAC[ORTHOGONAL_SYM]\r
 435   THEN MATCH_MP_TAC (GENL [`pt1:point`;`pt2:point`] \r
 436     (REWRITE_RULE[GSYM IMP_CONJ] (DISCH_ALL (STRIP_RULE \r
 437       NORMAL_OF_PLANE_IS_ORTHOGONAL_TO_SEGMENT))))\r
 438   THEN ASM_REWRITE_TAC[]\r
 439   THEN EXPAND_TAC "a" THEN SELECT_ELIM_TAC\r
 440   THEN ASM_SIMP_TAC[EXISTS_MULTIPLE_OF_NORMAL_IN_PLANE]);;\r
 441 \r
 442 let PLANE_WAVE_WITH_PHASE_SHIFT_AT_INTERFACE = prove\r
 443   (`!emf. is_plane_wave emf ==> !i. is_valid_interface i ==> !r.\r
 444   r IN plane_of_interface i ==> !t.\r
 445   let n = normal_of_interface i in\r
 446   emf r t = cexp (--ii * Cx(projection_on_hyperplane (k_of_wave emf) (unit n)\r
 447     dot r - w_of_wave emf * t + phase_shift_at_plane (plane_of_interface i) n emf))\r
 448     % eh_of_wave emf`,\r
 449   REWRITE_TAC[LET_DEFs] THEN REPEAT STRIP_TAC THEN ASM_CSQ_THEN \r
 450     IS_VALID_INTERFACE_IS_NORMAL_TO_PLANE ASSUME_TAC\r
 451   THEN ASM_CSQ_THEN IS_VALID_INTERFACE_PLANE ASSUME_TAC\r
 452   THEN ASM_CSQS_THEN PLANE_WAVE_WITH_PHASE_SHIFT_AT_PLANE ASSUME_TAC\r
 453   THEN ASM_REWRITE_TAC[]);;\r
 454 \r
 455 let magnitude_shifted_at_plane = new_definition\r
 456   `magnitude_shifted_at_plane p n emf =\r
 457     cexp (--ii * Cx(phase_shift_at_plane p n emf)) % eh_of_wave emf`;;\r
 458 \r
 459 let E_PRESERVED_IN_TE_MODE = prove\r
 460   (`!i emf_i emf_r emf_t.\r
 461     is_plane_wave_at_interface i emf_i emf_r emf_t /\ non_null_wave emf_r\r
 462     /\ non_null_wave emf_t /\ TE_mode i emf_i emf_r emf_t ==>\r
 463     let magnitude =\r
 464       \emf. FST (magnitude_shifted_at_plane (plane_of_interface i)\r
 465         (normal_of_interface i) emf) cdot (vector_to_cvector (TE_mode_axis\r
 466           i emf_i emf_r emf_t))\r
 467     in\r
 468     magnitude emf_r + magnitude emf_i = magnitude emf_t`,\r
 469   REWRITE_TAC[FORALL_INTERFACE_THM;LET_DEFs;plane_of_interface;\r
 470     normal_of_interface] THEN REPEAT STRIP_TAC\r
 471   THEN ASM_CSQ_THEN (GEQ_IMP is_plane_wave_at_interface) (STRIP_ASSUME_TAC o\r
 472     REWRITE_RULE[LET_DEFs])\r
 473   THEN FIRST_ASSUM (let tmp = MESON[non_null_wave] `!emf. non_null_wave emf\r
 474     ==> is_plane_wave emf` in ASSUME_TAC o MATCH_MP tmp)\r
 475   THEN ASM_CSQ_THEN (GEN_ALL (MATCH_MP EQ_IMP (SPEC_ALL is_valid_interface)))\r
 476     (STRIP_ASSUME_TAC o REWRITE_RULE[LET_DEFs])\r
 477   THEN ASM_CSQ_THEN PLANE_NON_EMPTY (STRIP_ASSUME_TAC o\r
 478     REWRITE_RULE[GSYM MEMBER_NOT_EMPTY])\r
 479   THEN FIRST_ASSUM (fun x -> FIRST_X_ASSUM (C ASM_CSQ_THEN (MP_TAC o\r
 480     REWRITE_RULE[LET_DEFs] o GEN_REWRITE_RULE (RATOR_CONV o ONCE_DEPTH_CONV)\r
 481     [e_of_emf] o CONJUNCT1 o SPEC `&0`) o REWRITE_RULE[boundary_conditions;\r
 482     emf_add;LET_DEFs] o C MATCH_MP x))\r
 483   THEN ASSUM_LIST (MAP_EVERY (C ASM_CSQS_THEN (SINGLE REWRITE_TAC o CONJUNCT1\r
 484     o SPEC `&0` o REWRITE_RULE[emf_at_point_mul;eh_of_wave;FST;SND;EMF_EQ]))\r
 485     o mapfilter (REWRITE_RULE[FORALL_INTERFACE_THM;LET_DEFs;plane_of_interface;\r
 486       normal_of_interface;]\r
 487     o MATCH_MP PLANE_WAVE_WITH_PHASE_SHIFT_AT_INTERFACE))\r
 488   THEN ASM_CSQ_THEN (REWRITE_RULE[LET_DEFs] K_PLANE_PROJECTION_CONSERVATION)\r
 489     (CONJUNCTS_THEN (C ASM_CSQ_THEN (SINGLE REWRITE_TAC o \r
 490       SIMP_RULE[normal_of_interface;LET_DEFs])))\r
 491   THEN REWRITE_TAC[REAL_ARITH `x - y * &0 = x`;CX_ADD;COMPLEX_ADD_LDISTRIB;\r
 492     CEXP_ADD;GSYM CVECTOR_MUL_ASSOC;GSYM CVECTOR_ADD_LDISTRIB;\r
 493     CCROSS_RMUL;CVECTOR_MUL_LCANCEL;CEXP_NZ;magnitude_shifted_at_plane;\r
 494     eh_of_wave;emf_at_point_mul;GSYM CDOT_LADD]\r
 495   THEN ASM_CSQS_THEN (REWRITE_RULE[IMP_CONJ;LET_DEFs] TE_MODE_PLANEWAVE_PROJ)\r
 496     (GEN_REWRITE_TAC (RATOR_CONV o ONCE_DEPTH_CONV) o CONJUNCTS)\r
 497   THEN REWRITE_TAC[CCROSS_RADD;CCROSS_RMUL;CVECTOR_MUL_ASSOC;\r
 498     GSYM CVECTOR_ADD_RDISTRIB;CVECTOR_MUL_RCANCEL;CCROSS_COLLINEAR_CVECTORS;\r
 499     GSYM CDOT_LMUL;GSYM CDOT_LADD;COLLINEAR_CVECTORS_VECTOR_TO_CVECTOR]\r
 500   THEN FIRST_X_ASSUM (STRIP_ASSUME_TAC o REWRITE_RULE[is_mode_axis;\r
 501     normal_of_interface;LET_DEFs] o MATCH_MP (GEQ_IMP TE_MODE_THM))\r
 502   THEN FIRST_ASSUM (ASSUME_TAC o REWRITE_RULE[NORM_EQ_0] o MATCH_MP \r
 503     (REAL_ARITH `!x. x= &1 ==> ~(x= &0)`))\r
 504   THEN FIRST_X_ASSUM (STRIP_ASSUME_TAC o MATCH_MP (GEQ_IMP is_normal_to_plane))\r
 505   THEN ASM_CSQS_THEN (ONCE_REWRITE_RULE[ORTHOGONAL_SYM] (REWRITE_RULE[IMP_CONJ]\r
 506     ORTHOGONAL_NON_COLLINEAR)) (SINGLE REWRITE_TAC)\r
 507   THEN REWRITE_TAC[CVECTOR_ADD_SYM]);;\r
 508 \r
 509 let H_CROSS_Z_WRT_E_IN_TE_MODE = prove\r
 510   (`!i emf_i emf_r emf_t.\r
 511     is_plane_wave_at_interface i emf_i emf_r emf_t\r
 512     /\ TE_mode i emf_i emf_r emf_t ==>\r
 513     let p = plane_of_interface i in\r
 514     let n = normal_of_interface i in\r
 515     let h_cross_z_wrt_e =\r
 516       \emf. (h_of_wave emf) ccross (vector_to_cvector n) =\r
 517         Cx ((n dot k_of_wave emf) / (eta0 * k0)) % e_of_wave emf\r
 518     in\r
 519     h_cross_z_wrt_e emf_i /\ h_cross_z_wrt_e emf_r /\ h_cross_z_wrt_e emf_t`,\r
 520   SIMP_TAC[FORALL_INTERFACE_THM;LET_DEFs;is_plane_wave_at_interface;\r
 521     plane_of_interface;non_null_wave;normal_of_interface]\r
 522   THEN REPEAT STRIP_TAC THEN ASM_CSQS_THEN (REWRITE_RULE[LET_DEFs;IMP_CONJ]\r
 523     TE_MODE_PLANEWAVE_PROJ) (SINGLE ONCE_REWRITE_TAC)\r
 524   THEN REWRITE_TAC[CCROSS_LMUL;CCROSS_LREAL;CDOT_RREAL;CVECTOR_ADD_RDISTRIB;\r
 525     GSYM CVECTOR_MUL_ASSOC;GSYM VECTOR_TO_CVECTOR_MUL;\r
 526     CVECTOR_IM_VECTOR_TO_CVECTOR_RE_IM;CVECTOR_RE_VECTOR_TO_CVECTOR_RE_IM;\r
 527     CCROSS_LADD;CVECTOR_ADD_LDISTRIB]\r
 528   THEN REWRITE_TAC[REWRITE_RULE[VECTOR_ARITH `--x = y <=> x = --y :real^N`] \r
 529     (ONCE_REWRITE_RULE[CROSS_SKEW] CROSS_LAGRANGE);\r
 530       CVECTOR_RE_VECTOR_TO_CVECTOR;\r
 531       CVECTOR_IM_VECTOR_TO_CVECTOR;DOT_LZERO;VECTOR_MUL_LZERO;VECTOR_SUB_RZERO;\r
 532       VECTOR_NEG_0;VECTOR_TO_CVECTOR_ZERO;CVECTOR_MUL_RZERO;CVECTOR_ADD_ID;\r
 533       DOT_RMUL]\r
 534   THEN ASM_CSQ_THEN TE_MODE_AXIS_ORTHOGONAL_N\r
 535     (SINGLE REWRITE_TAC o REWRITE_RULE[orthogonal;normal_of_interface;LET_DEFs]\r
 536       o ONCE_REWRITE_RULE[ORTHOGONAL_SYM])\r
 537   THEN REWRITE_TAC[REAL_MUL_RZERO;VECTOR_MUL_LZERO;VECTOR_ARITH\r
 538     `--(vec 0 - x) = x`;VECTOR_NEG_0;VECTOR_TO_CVECTOR_ZERO;CVECTOR_MUL_RZERO;\r
 539     CVECTOR_ADD_ID]\r
 540   THEN REWRITE_TAC[MESON[CVECTOR_MUL_ASSOC;COMPLEX_MUL_SYM]\r
 541     `a % ii % v = ii % a % v:complex^N`;GSYM VECTOR_TO_CVECTOR_MUL;CVECTOR_EQ;\r
 542     CVECTOR_RE_VECTOR_TO_CVECTOR_RE_IM;CVECTOR_IM_VECTOR_TO_CVECTOR_RE_IM;\r
 543     VECTOR_MUL_ASSOC]\r
 544   THEN CONJ_TAC THEN REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC)\r
 545   THEN REAL_ARITH_TAC);;\r
 546 \r
 547 let NON_PROJECTED_E_RELATION_IN_TE_MODE = prove\r
 548   (`!i emf_i emf_r emf_t.\r
 549     is_plane_wave_at_interface i emf_i emf_r emf_t /\ non_null_wave emf_r\r
 550     /\ non_null_wave emf_t /\ TE_mode i emf_i emf_r emf_t ==>\r
 551     let magnitude =\r
 552       \emf. FST (magnitude_shifted_at_plane (plane_of_interface i)\r
 553         (normal_of_interface i) emf) cdot (vector_to_cvector (TE_mode_axis i\r
 554           emf_i emf_r emf_t))\r
 555     in\r
 556     let n = unit (normal_of_interface i) in\r
 557     Cx (n dot k_of_wave emf_i) * (magnitude emf_i - magnitude emf_r) =\r
 558       Cx (n dot k_of_wave emf_t) * magnitude emf_t`,\r
 559   REWRITE_TAC[FORALL_INTERFACE_THM;LET_DEFs;normal_of_interface;\r
 560     plane_of_interface] THEN REPEAT STRIP_TAC \r
 561   THEN ASM_CSQ_THEN (GEQ_IMP is_plane_wave_at_interface) (STRIP_ASSUME_TAC o\r
 562     REWRITE_RULE[LET_DEFs])\r
 563   THEN FIRST_ASSUM (let tmp = MESON[non_null_wave] `!emf. non_null_wave emf\r
 564     ==> is_plane_wave emf` in ASSUME_TAC o MATCH_MP tmp)\r
 565   THEN ASM_CSQ_THEN (GEN_ALL (MATCH_MP EQ_IMP (SPEC_ALL is_valid_interface)))\r
 566     (STRIP_ASSUME_TAC o REWRITE_RULE[LET_DEFs])\r
 567   THEN ASM_CSQ_THEN PLANE_NON_EMPTY (STRIP_ASSUME_TAC \r
 568     o REWRITE_RULE[GSYM MEMBER_NOT_EMPTY])\r
 569   THEN FIRST_ASSUM (fun x -> FIRST_X_ASSUM (C ASM_CSQ_THEN (MP_TAC o\r
 570     REWRITE_RULE[LET_DEFs]\r
 571     o GEN_REWRITE_RULE (RATOR_CONV o ONCE_DEPTH_CONV) [h_of_emf] \r
 572     o CONJUNCT2 o SPEC `&0`) \r
 573     o REWRITE_RULE[boundary_conditions;emf_add;LET_DEFs] o C MATCH_MP x))\r
 574   THEN ASSUM_LIST (MAP_EVERY (C ASM_CSQS_THEN (SINGLE REWRITE_TAC o CONJUNCT2\r
 575     o SPEC `&0` o REWRITE_RULE[emf_at_point_mul;eh_of_wave;FST;SND;EMF_EQ]))\r
 576     o mapfilter (REWRITE_RULE[FORALL_INTERFACE_THM;LET_DEFs;plane_of_interface;\r
 577       normal_of_interface;]\r
 578     o MATCH_MP PLANE_WAVE_WITH_PHASE_SHIFT_AT_INTERFACE))\r
 579   THEN ASM_CSQ_THEN (REWRITE_RULE[LET_DEFs] K_PLANE_PROJECTION_CONSERVATION)\r
 580     (CONJUNCTS_THEN (C ASM_CSQ_THEN (SINGLE REWRITE_TAC\r
 581       o SIMP_RULE[normal_of_interface;LET_DEFs])))\r
 582   THEN REWRITE_TAC[REAL_ARITH `x - y * &0 = x`;CX_ADD;COMPLEX_ADD_LDISTRIB;\r
 583     CEXP_ADD;GSYM CVECTOR_MUL_ASSOC;GSYM CVECTOR_ADD_LDISTRIB;\r
 584     CCROSS_RMUL;CVECTOR_MUL_LCANCEL;CEXP_NZ;magnitude_shifted_at_plane;\r
 585     eh_of_wave;emf_at_point_mul;GSYM CDOT_LADD;CCROSS_RADD]\r
 586   THEN ASM_CSQS_THEN (REWRITE_RULE[IMP_CONJ;CVECTOR_ARITH\r
 587     `--x=a%y <=> x = (--a)%y:complex^N`] (ONCE_REWRITE_RULE[CCROSS_SKEW]\r
 588     (REWRITE_RULE[LET_DEFs] H_CROSS_Z_WRT_E_IN_TE_MODE)))\r
 589     (SINGLE REWRITE_TAC \r
 590       o REWRITE_RULE[LET_DEFs;plane_of_interface;normal_of_interface])\r
 591   THEN REWRITE_TAC[GSYM CX_NEG;real_div;REAL_NEG_LMUL;GSYM DOT_RNEG]\r
 592   THEN FIRST_ASSUM (ASSUME_TAC o ONCE_REWRITE_RULE[DOT_SYM]\r
 593     o REWRITE_RULE[DOT_RUNIT_EQ] o MATCH_MP SYMETRIC_VECTORS_PROJECTION_ON_AXIS\r
 594     o MATCH_MP UNIT_THM o CONJUNCT1 o MATCH_MP (GEQ_IMP is_normal_to_plane))\r
 595   THEN ASM_CSQS_THEN (SIMP_RULE[LET_DEFs] LAW_OF_REFLECTION) (fun x -> \r
 596     POP_ASSUM (SINGLE REWRITE_TAC o C MATCH_MP (REWRITE_RULE\r
 597       [normal_of_interface;LET_DEFs] x)))\r
 598   THEN REWRITE_TAC[CX_MUL;DOT_RNEG;CX_NEG;COMPLEX_MUL_LNEG;CVECTOR_ARITH\r
 599     `a%(--(u*v))%x+c%(u*v)%y = d%(--(u'*v))%z\r
 600     <=> v%u%(a%x-c%y) = v%u'%d%z:complex^N`]\r
 601   THEN REWRITE_TAC[CVECTOR_MUL_LCANCEL;CX_INJ;REAL_INV_EQ_0;REAL_ENTIRE;\r
 602     MATCH_MP REAL_LT_IMP_NZ eta0;MATCH_MP REAL_LT_IMP_NZ k0]\r
 603   THEN REWRITE_TAC[unit;DOT_LMUL;CX_MUL;GSYM COMPLEX_MUL_ASSOC;\r
 604     COMPLEX_EQ_MUL_LCANCEL;CX_INJ;REAL_ENTIRE;REAL_INV_EQ_0;NORM_EQ_0]\r
 605   THEN ASM_CSQS_THEN NORMAL_OF_PLANE_NON_NULL (SINGLE REWRITE_TAC)\r
 606   THEN ASM_CSQS_THEN (REWRITE_RULE[IMP_CONJ;LET_DEFs] TE_MODE_PLANEWAVE_PROJ)\r
 607     (GEN_REWRITE_TAC (RATOR_CONV o ONCE_DEPTH_CONV) o CONJUNCTS)\r
 608   THEN REWRITE_TAC[CVECTOR_MUL_ASSOC;GSYM CVECTOR_SUB_RDISTRIB;\r
 609     CVECTOR_MUL_RCANCEL;VECTOR_TO_CVECTOR_ZERO_EQ;GSYM NORM_EQ_0]\r
 610   THEN FIRST_ASSUM (SINGLE REWRITE_TAC o MATCH_MP (REWRITE_RULE[is_mode_axis]\r
 611     (GEQ_IMP TE_MODE_THM)))\r
 612   THEN SIMP_TAC[REAL_ARITH `~(&1 = &0)`;CDOT_LMUL;COMPLEX_MUL_ASSOC]);;\r
 613 \r
 614 let COMPLEX_MUL_LINV2 = prove\r
 615   (`!x y. ~(x=Cx(&0)) ==> inv x * (x * y) = y`,\r
 616   SIMP_TAC[COMPLEX_MUL_ASSOC;COMPLEX_MUL_LINV;COMPLEX_MUL_LID]);;\r
 617 \r
 618 let COMPLEX_BALANCE_MUL_DIV = prove\r
 619   (`!x y z. ~(x=Cx(&0)) ==> (x*y=z <=> y=z/x)`,\r
 620  REPEAT STRIP_TAC THEN EQ_TAC THENL [\r
 621    DISCH_THEN (fun x -> ASM_SIMP_TAC[GSYM x;complex_div;SIMPLE_COMPLEX_ARITH\r
 622    `(x*y)*inv x=(x*inv x)*y:complex`;COMPLEX_MUL_RINV;COMPLEX_MUL_LID]);\r
 623    DISCH_THEN (fun x -> ASM_SIMP_TAC[x;COMPLEX_DIV_LMUL]);\r
 624  ]);;\r
 625 \r
 626 \r
 627 let FRESNEL_REFLECTION_TE_MODE = prove\r
 628   (`!i emf_i emf_r emf_t.\r
 629   is_plane_wave_at_interface i emf_i emf_r emf_t /\ non_null_wave emf_r\r
 630   /\ non_null_wave emf_t /\ TE_mode i emf_i emf_r emf_t ==>\r
 631   let magnitude =\r
 632     \emf. FST (magnitude_shifted_at_plane (plane_of_interface i)\r
 633       (normal_of_interface i) emf) cdot (vector_to_cvector (TE_mode_axis i\r
 634         emf_i emf_r emf_t))\r
 635   in\r
 636   let theta = \emf. Cx(vector_angle (k_of_wave emf) (normal_of_interface i)) in\r
 637   let n1 = Cx(n1_of_interface i) in\r
 638   let n2 = Cx(n2_of_interface i) in\r
 639   magnitude emf_r = (n1 * ccos (theta emf_i) - n2 * ccos (theta emf_t)) / (n1 *\r
 640     ccos (theta emf_i) + n2 * ccos (theta emf_t)) * magnitude emf_i`,\r
 641   REPEAT STRIP_TAC THEN ASM_CSQS_THEN (REWRITE_RULE[IMP_CONJ]\r
 642     NON_PROJECTED_E_RELATION_IN_TE_MODE) MP_TAC\r
 643   THEN ASM_CSQS_THEN (REWRITE_RULE[IMP_CONJ] E_PRESERVED_IN_TE_MODE) (MP_TAC o\r
 644     GSYM)\r
 645   THEN LET_TAC THEN REWRITE_TAC[LET_DEFs] \r
 646   THEN DISCH_THEN (fun x -> REWRITE_TAC[x;SIMPLE_COMPLEX_ARITH\r
 647     `x*(y-z)=t*(z+y) <=> (x+t)*z=(x-t)*y:complex`])\r
 648   THEN DISCH_THEN (MP_TAC o MATCH_MP (MATCH_MP (MESON[]\r
 649     `(!x y z. p x ==> (q x y z <=> r x y z)) ==> !x y z. q x y z ==> p x\r
 650     ==> r x y z`) COMPLEX_BALANCE_MUL_DIV))\r
 651   THEN ANTS_TAC THENL [\r
 652     REWRITE_TAC[GSYM CX_ADD;CX_INJ] THEN MATCH_MP_TAC REAL_POS_NZ\r
 653     THEN MATCH_MP_TAC REAL_LTE_ADD THEN REWRITE_TAC[DOT_LUNIT_POS;DOT_LUNIT_GE0]\r
 654     THEN ONCE_REWRITE_TAC[DOT_SYM] THEN REPEAT (POP_ASSUM MP_TAC)\r
 655     THEN SPEC_TAC (`i:interface`,`i:interface`)\r
 656     THEN SIMP_TAC[FORALL_INTERFACE_THM;is_plane_wave_at_interface;\r
 657       normal_of_interface;map_triple;LET_DEFs;real_ge;real_gt];\r
 658     SIMP_TAC[SIMPLE_COMPLEX_ARITH `(x*y)/z = (x/z)*y`]\r
 659     THEN DISCH_THEN (K ALL_TAC) THEN AP_THM_TAC THEN AP_TERM_TAC \r
 660     THEN REWRITE_TAC[GSYM CX_ADD;GSYM CX_SUB;GSYM CX_COS;GSYM CX_MUL;\r
 661       GSYM CX_DIV;CX_INJ]\r
 662     THEN REPEAT (POP_ASSUM MP_TAC) THEN SPEC_TAC (`i:interface`,`i:interface`)\r
 663     THEN REWRITE_TAC[FORALL_INTERFACE_THM;normal_of_interface;\r
 664       plane_of_interface;LET_DEFs;n1_of_interface;n2_of_interface]\r
 665     THEN REPEAT STRIP_TAC\r
 666     THEN ASM_CSQ_THEN (GEQ_IMP is_plane_wave_at_interface) (STRIP_ASSUME_TAC\r
 667       o REWRITE_RULE[is_valid_interface;is_normal_to_plane;LET_DEFs;\r
 668         map_triple])\r
 669     THEN ASM_REWRITE_TAC[GSYM NORM_EQ_0]\r
 670     THEN ASM_SIMP_TAC [GEN_ALL (DISCH_ALL (GSYM (MATCH_MP REAL_LT_IMP_NE\r
 671       (UNDISCH_ALL (SPEC_ALL (MATCH_MP (REWRITE_RULE[IMP_CONJ] REAL_LT_MUL)\r
 672         k0))))))]\r
 673     THEN GEN_REWRITE_TAC (RATOR_CONV o ONCE_DEPTH_CONV) [VECTOR_ANGLE]\r
 674     THEN ASM_SIMP_TAC[UNIT_THM;REAL_MUL_LID]\r
 675     THEN REWRITE_TAC[GSYM REAL_MUL_ASSOC;GSYM REAL_ADD_LDISTRIB;\r
 676       GSYM REAL_SUB_LDISTRIB;real_div;REAL_INV_MUL]\r
 677     THEN REWRITE_TAC[REAL_ARITH `x*y*inv x*z=(x*inv x)*y*z:real`;\r
 678       MATCH_MP REAL_MUL_RINV (GSYM (MATCH_MP REAL_LT_IMP_NE k0));REAL_MUL_LID]\r
 679     THEN ASM_SIMP_TAC[unit;VECTOR_ANGLE_LMUL;REAL_INV_EQ_0;NORM_EQ_0;\r
 680       REAL_LE_INV_EQ;NORM_POS_LE;VECTOR_ANGLE_SYM]]);;\r
 681 \r
 682 let FRESNEL_TRANSMISSION_TE_MODE = prove\r
 683   (`!i emf_i emf_r emf_t.\r
 684     is_plane_wave_at_interface i emf_i emf_r emf_t /\ non_null_wave emf_r \r
 685     /\ non_null_wave emf_t /\ TE_mode i emf_i emf_r emf_t ==>\r
 686     let magnitude =\r
 687       \emf. FST (magnitude_shifted_at_plane (plane_of_interface i) \r
 688         (normal_of_interface i) emf) cdot (vector_to_cvector (TE_mode_axis i\r
 689           emf_i emf_r emf_t))\r
 690     in\r
 691     let theta =\r
 692       \emf. Cx(vector_angle (k_of_wave emf) (normal_of_interface i))\r
 693     in\r
 694     let n1 = Cx(n1_of_interface i) in\r
 695     let n2 = Cx(n2_of_interface i) in\r
 696     magnitude emf_t = Cx(&2) * n1 * ccos (theta emf_i) / (n1 * ccos\r
 697       (theta emf_i) + n2 * ccos (theta emf_t)) * magnitude emf_i`,\r
 698   REPEAT STRIP_TAC THEN ASM_CSQS_THEN (REWRITE_RULE[IMP_CONJ] \r
 699     E_PRESERVED_IN_TE_MODE) (MP_TAC o GSYM)\r
 700   THEN ASM_CSQS_THEN (REWRITE_RULE[IMP_CONJ] \r
 701     NON_PROJECTED_E_RELATION_IN_TE_MODE) MP_TAC THEN LET_TAC\r
 702     THEN REWRITE_TAC[LET_DEFs] \r
 703   THEN REWRITE_TAC[SIMPLE_COMPLEX_ARITH `x*(y-z)=t*u <=> x*z=x*y-t*u:complex`]\r
 704   THEN DISCH_THEN (MP_TAC o MATCH_MP (MATCH_MP (MESON[]\r
 705     `(!x y z. p x ==> (q x y z <=> r x y z)) ==> !x y z. q x y z ==> p x\r
 706       ==> r x y z`) COMPLEX_BALANCE_MUL_DIV))\r
 707   THEN MATCH_MP_TAC (MESON[] `p/\(p==>q==>r==>s) ==> ((p==>q)==>r==>s)`)\r
 708   THEN CONJ_TAC THENL [\r
 709     REWRITE_TAC[CX_INJ] THEN MATCH_MP_TAC REAL_POS_NZ\r
 710     THEN REWRITE_TAC[DOT_LUNIT_POS;DOT_LUNIT_GE0]\r
 711     THEN ONCE_REWRITE_TAC[DOT_SYM] THEN REPEAT (POP_ASSUM MP_TAC)\r
 712     THEN SPEC_TAC (`i:interface`,`i:interface`)\r
 713     THEN SIMP_TAC[FORALL_INTERFACE_THM;is_plane_wave_at_interface;\r
 714       normal_of_interface;map_triple;LET_DEFs;real_gt];\r
 715     DISCH_TAC THEN DISCH_THEN (fun x -> ASM_SIMP_TAC[x;SIMPLE_COMPLEX_ARITH\r
 716       `t = (x*i-y*t)/x+i <=> (y/x+Cx(&1))*t = (x/x+Cx(&1))*i:complex`;\r
 717       COMPLEX_DIV_REFL;SIMPLE_COMPLEX_ARITH `Cx(&1)+Cx(&1)=Cx(&2)`])\r
 718     THEN ASM_CSQ_THEN COMPLEX_DIV_REFL (SINGLE REWRITE_TAC o GSYM)\r
 719     THEN REWRITE_TAC[GSYM CX_ADD;GSYM CX_DIV;real_div;GSYM REAL_ADD_RDISTRIB]\r
 720     THEN DISCH_THEN (MP_TAC o MATCH_MP (MATCH_MP (MESON[]\r
 721       `(!x y z. p x ==> (q x y z <=> r x y z)) ==> (!x y z. q x y z ==> p x \r
 722         ==> r x y z)`) COMPLEX_BALANCE_MUL_DIV))\r
 723     THEN ANTS_TAC THENL [\r
 724       ASM_REWRITE_TAC[CX_MUL;CX_INV;COMPLEX_ENTIRE;COMPLEX_INV_EQ_0] \r
 725       THEN REWRITE_TAC[CX_INJ] THEN MATCH_MP_TAC REAL_POS_NZ \r
 726       THEN MATCH_MP_TAC REAL_LET_ADD\r
 727       THEN REWRITE_TAC[DOT_LUNIT_POS;DOT_LUNIT_GE0]\r
 728       THEN ONCE_REWRITE_TAC[DOT_SYM] THEN REPEAT (POP_ASSUM MP_TAC)\r
 729       THEN SPEC_TAC (`i:interface`,`i:interface`)\r
 730       THEN SIMP_TAC[FORALL_INTERFACE_THM;is_plane_wave_at_interface;\r
 731         normal_of_interface;map_triple;LET_DEFs;real_ge;real_gt];\r
 732       SIMP_TAC[SIMPLE_COMPLEX_ARITH `(x*y)/z = x/z*y:complex`;GSYM CX_DIV;\r
 733         real_div;REAL_INV_MUL;REAL_INV_INV] THEN DISCH_THEN (K ALL_TAC)\r
 734       THEN REWRITE_TAC[GSYM CX_MUL;GSYM CX_COS;GSYM CX_ADD;GSYM CX_DIV;\r
 735         COMPLEX_MUL_ASSOC;CX_INJ]\r
 736       THEN AP_THM_TAC THEN AP_TERM_TAC\r
 737       THEN REWRITE_TAC[CX_INJ;REAL_ARITH `&2*x = (&2*y)*z <=> x=y*z`]\r
 738       THEN REPEAT (POP_ASSUM MP_TAC) THEN SPEC_TAC (`i:interface`,`i:interface`)\r
 739       THEN REWRITE_TAC[FORALL_INTERFACE_THM;normal_of_interface;\r
 740         plane_of_interface;LET_DEFs;n1_of_interface;n2_of_interface]\r
 741       THEN REPEAT STRIP_TAC\r
 742       THEN ASM_CSQ_THEN (GEQ_IMP is_plane_wave_at_interface) (STRIP_ASSUME_TAC\r
 743         o REWRITE_RULE[is_valid_interface;is_normal_to_plane;LET_DEFs;map_triple])\r
 744       THEN GEN_REWRITE_TAC (RATOR_CONV o ONCE_DEPTH_CONV) [VECTOR_ANGLE]\r
 745       THEN ASM_SIMP_TAC[UNIT_THM;REAL_MUL_LID]\r
 746       THEN REWRITE_TAC[GSYM REAL_MUL_ASSOC;GSYM REAL_ADD_LDISTRIB;\r
 747         GSYM REAL_SUB_LDISTRIB;real_div;REAL_INV_MUL]\r
 748       THEN REWRITE_TAC[REAL_ARITH `inv x*y*x*z=(x*inv x)*y*z:real`;\r
 749         MATCH_MP REAL_MUL_RINV (GSYM (MATCH_MP REAL_LT_IMP_NE k0));\r
 750           REAL_MUL_LID]\r
 751       THEN ASM_SIMP_TAC[unit;VECTOR_ANGLE_LMUL;REAL_INV_EQ_0;NORM_EQ_0;\r
 752         REAL_LE_INV_EQ;NORM_POS_LE]\r
 753       THEN GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [VECTOR_ANGLE_SYM]\r
 754       THEN REAL_ARITH_TAC]]);;\r