1 (* ========================================================================= *)
\r
2 (* Formalization of Electromagnetic Optics *)
\r
4 (* (c) Copyright, Sanaz Khan Afshar & Vincent Aravantinos 2011-14 *)
\r
5 (* Hardware Verification Group, *)
\r
6 (* Concordia University *)
\r
8 (* Contact: <s_khanaf@encs.concordia.ca> *)
\r
9 (* <vincent@encs.concordia.ca> *)
\r
11 (* This file deals with the non-trivial theorems called "primitive rules". *)
\r
12 (* ========================================================================= *)
\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
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
43 THEN RULE_ASSUM_TAC (REWRITE_RULE[CART_EQ;VEC_COMPONENT;DIMINDEX_3;FORALL_3])
\r
44 THEN ASM_REWRITE_TAC[])
\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
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
61 REWRITE_TAC[PASTECART_EQ_CVECTOR_ZERO;DE_MORGAN_THM;NON_NULL_LEMMA]);;
\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
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
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
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
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
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
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
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
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
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
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
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
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
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
214 REPEAT (ANTS_TAC ORELSE APPLY_NON_NULL_LEMMA)
\r
215 THEN ASM_REWRITE_TAC[]);;
\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
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
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
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
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
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
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
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
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
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
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
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
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
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
386 MATCH_ACCEPT_TAC REAL_LE_POW_2;
\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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
544 THEN CONJ_TAC THEN REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC)
\r
545 THEN REAL_ARITH_TAC);;
\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
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
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
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
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
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
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
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
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
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
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
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
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
692 \emf. Cx(vector_angle (k_of_wave emf) (normal_of_interface i))
\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
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