Update from HH
[Emf193/.git] / 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