1 (* ========================================================================= *)
3 (* Z-Shaped Resonator *)
5 (* (c) Copyright, Muhammad Umair Siddique, Vincent Aravantinos, 2012 *)
6 (* Hardware Verification Group, *)
7 (* Concordia University *)
9 (* Contact: <muh_sidd@ece.concordia.ca>, <vincent@ece.concordia.ca> *)
11 (* Last update: Feb 16, 2012 *)
13 (* ========================================================================= *)
17 needs "geometrical_optics.ml";;
18 needs "resonator.ml";;
22 (*--------------------------Z Cavity Modeling----------------------------*)
23 let z_cavity = new_definition
24 `z_cavity R d1 d2 n: resonator =
25 ((plane), [(n,d1),(spherical R),reflected;(n,d2),(spherical R),reflected],
28 let z_cavity_mat_half = new_definition
29 `z_cavity_mat_half R (n:real) d1 d2 =
30 mat2x2 ((R * R - &4 * d1 * R - &2 * d2 * R + &4 * d1 * d2)/ (R * R))
31 ((&4*d2*d1*d1 - &4*R*d1*d1 + &2*R*R*d1 - &4*d2*R*d1 + d2*R*R)/(R*R))
33 ((R * R - &4 * d1 * R - &2 * d2 * R + &4 * d1 * d2)/ (R * R)) `;;
35 let VALID_Z_CAVITY = prove
36 (`!R n. ~(R= &0) /\ &0 < n /\ &0 <= d1 /\ &0 <= d2 ==>
37 is_valid_resonator (z_cavity R d1 d2 n)`,
38 VALID_RESONATOR_TAC z_cavity);;
41 let Z_CAVITY_STABILITY_LEMMA = prove (
43 ~(R= &0) /\ &0 < n /\ &0 <= d1 /\ &0 <= d2 ==>
44 system_composition (unfold_resonator (z_cavity R d1 d2 n) 1) =
45 (z_cavity_mat_half R (n:real) d1 d2) pow 2`,
47 REWRITE_TAC[MAT_POW2;z_cavity_mat_half;unfold_resonator; system_composition;
48 z_cavity;unfold_resonator;LIST_POW;ONE;fp_cavity;round_trip;APPEND;
49 optical_components_shift;LET_DEF;LET_END_DEF;REVERSE;
50 interface_matrix;head_index;free_space_matrix] THEN SIMP_TAC[GSYM ONE; GSYM MATRIX_MUL_ASSOC]
51 THEN SIMP_TAC[ MAT2X2_MUL;REAL_MUL_RZERO;REAL_MUL_LZERO;REAL_ADD_LID;REAL_ADD_RID;REAL_MUL_LID;REAL_MUL_RID ] THEN SIMP_TAC[MAT2X2_EQ ] THEN
52 CONV_TAC REAL_FIELD);;
55 (*------------Stability_Analysis-------------*)
58 let STABLE_Z_CAVITY = prove(`!d1 d2 R n. ~(R = &0)/\ &0 < n /\ &0 < d1 /\ &0 < d2 /\ (&2 * d1 + d2) pow 2 / (&2 * d1) < d2 /\
59 (&2*d1*d2)/ (&2*d1 + d2) < R ==> is_stable_resonator (z_cavity R d1 d2 n)`,
61 REPEAT STRIP_TAC THEN MP_REWRITE_TAC STABILITY_THEOREM_SYM THEN
62 EXISTS_TAC(`(z_cavity_mat_half R n d1 d2):real^2^2`) THEN
63 CONJ_TAC THENL[MP_REWRITE_TAC VALID_Z_CAVITY THEN
64 ASM_SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN
65 CONJ_TAC THENL[MP_REWRITE_TAC Z_CAVITY_STABILITY_LEMMA THEN
66 ASM_SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN
67 REWRITE_TAC[z_cavity_mat_half;DET_MAT2X2] THEN
68 REWRITE_TAC[mat2x2;VECTOR_2] THEN
69 CONJ_TAC THENL[ REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC REAL_FIELD;ALL_TAC]
70 THEN SIMP_TAC[REAL_FIELD`!a. a + a = &2*a`; REAL_FIELD `!a b. (&2*(a)/b)/ &2 = a/b`] THEN ASM_SIMP_TAC[ REAL_FIELD `!R a b c d . ~(R = &0) ==> (a - b - c + d)/(R*R) =
71 (a/(R*R) - b/(R*R) - c/(R*R) + d/(R*R))`;
72 REAL_FIELD ` !a. ~(a = &0)==> (a*a)/(a*a) = &1 `;
73 REAL_FIELD `! a b z. ~(z = &0) ==> (a*b*z)/(z*z) = (a*b)/z `] THEN
77 SUBGOAL_THEN `(-- &1 < &1 - (&4 * d1) / R - (&2 * d2) / R + (&4 * d1 * d2) / (R * R)) = (&2 + (&4 * d1 * d2) / (R * R) > (&4 * d1) / R + (&2 * d2) / R)` ASSUME_TAC THENL[REAL_ARITH_TAC;ALL_TAC] THEN ONCE_ASM_REWRITE_TAC[] THEN
78 ASM_SIMP_TAC[REAL_FIELD `!a b c. ~(a = &0) ==> b/a + c/a = (b+c)/a `] THEN
79 SUBGOAL_THEN `&2 + (&4 * d1 * d2) / (R * R) > (&4 * d1 + &2 * d2) / R <=>
80 &1 + (&2 * d1 * d2) / (R * R) > (&2* d1 + d2) / R` ASSUME_TAC THENL[
81 REAL_ARITH_TAC;ALL_TAC] THEN ONCE_ASM_REWRITE_TAC[] THEN
82 ONCE_SIMP_TAC[REAL_FIELD `! a b. a:real > b <=> b < a`] THEN
83 ONCE_SIMP_TAC[REAL_FIELD `! a b. (b < a) = (b + &0 < a) `] THEN
84 MATCH_MP_TAC REAL_LT_ADD2 THEN CONJ_TAC THENL[
85 SUBGOAL_THEN `&0 < R ` ASSUME_TAC THENL[MATCH_MP_TAC REAL_LT_TRANS THEN
86 EXISTS_TAC(`(&2 * d1 * d2) / (&2 * d1 + d2) `) THEN ASM_SIMP_TAC[] THEN
87 MATCH_MP_TAC REAL_LT_DIV THEN CONJ_TAC THENL[
88 MATCH_MP_TAC REAL_LT_MUL THEN ASM_SIMP_TAC[REAL_LT_MUL;REAL_FIELD `&0 < &2 `];
90 ASM_SIMP_TAC[REAL_LT_MUL;REAL_FIELD `!a b. &0 < a /\ &0 < b ==> &0 < &2*a + b ` ];
91 ALL_TAC] THEN ASM_SIMP_TAC[REAL_LT_LDIV_EQ;REAL_MUL_LID] THEN
92 MATCH_MP_TAC REAL_LT_TRANS THEN EXISTS_TAC(`(&2 * d1 * d2) / (&2 * d1 + d2) `) THEN
93 ASM_SIMP_TAC[] THEN ASM_SIMP_TAC[REAL_LT_RDIV_EQ;REAL_FIELD `!a b. &0 < a /\ &0 < b ==> &0 < &2*a + b `;REAL_MUL_ASSOC ] THEN
94 SUBGOAL_THEN `(&2 * d1 + d2) * (&2 * d1 + d2) < (&2 * d1) * d2 <=>
95 ((&2 * d1 + d2) * (&2 * d1 + d2)) /(&2 * d1) < d2` ASSUME_TAC THENL[
96 REWRITE_TAC[EQ_SYM_EQ;REAL_MUL_SYM] THEN MATCH_MP_TAC REAL_LT_LDIV_EQ THEN
97 ASM_SIMP_TAC[REAL_FIELD `!a . &0 < a ==> &0 < a* &2` ];ALL_TAC] THEN
98 ONCE_ASM_REWRITE_TAC[] THEN ASM_SIMP_TAC[GSYM REAL_POW_2 ];ALL_TAC] THEN
99 MATCH_MP_TAC REAL_LT_DIV THEN CONJ_TAC THENL[ MATCH_MP_TAC REAL_LT_MUL THEN
100 ASM_SIMP_TAC[REAL_LT_MUL;REAL_FIELD `&0 < &2 `];ALL_TAC] THEN
101 ASM_SIMP_TAC[GSYM REAL_POW_2] THEN MATCH_MP_TAC REAL_POW_LT THEN
102 MATCH_MP_TAC REAL_LT_TRANS THEN EXISTS_TAC(`(&2 * d1 * d2) / (&2 * d1 + d2) `) THEN
103 ASM_SIMP_TAC[] THEN MATCH_MP_TAC REAL_LT_DIV THEN
104 CONJ_TAC THENL[ MATCH_MP_TAC REAL_LT_MUL THEN
105 ASM_SIMP_TAC[REAL_LT_MUL;REAL_FIELD `&0 < &2 `];ALL_TAC]THEN
106 ASM_SIMP_TAC[REAL_LT_MUL;REAL_FIELD `!a b. &0 < a /\ &0 < b ==> &0 < &2*a + b `];
109 SIMP_TAC[REAL_FIELD ` !a:real b c d. a - b -c + d < a <=> d < b + c `] THEN
110 ASM_SIMP_TAC[REAL_FIELD `!a b c. ~(a = &0) ==> b/a + c/a = (b+c)/a `] THEN
111 SUBGOAL_THEN `(&4 * d1 * d2) / (R * R) < (&4 * d1 + &2 * d2) / R <=>
112 ((&4 * d1 * d2) / R)/ R < (&4 * d1 + &2 * d2) / R ` ASSUME_TAC THENL[
113 SIMP_TAC[real_div; GSYM REAL_MUL_ASSOC] THEN SIMP_TAC[GSYM REAL_INV_MUL];ALL_TAC] THEN
114 ONCE_ASM_REWRITE_TAC[] THEN SUBGOAL_THEN `&0 < R ` ASSUME_TAC THENL[MATCH_MP_TAC REAL_LT_TRANS THEN
115 EXISTS_TAC(`(&2 * d1 * d2) / (&2 * d1 + d2) `) THEN ASM_SIMP_TAC[] THEN
116 MATCH_MP_TAC REAL_LT_DIV THEN CONJ_TAC THENL[
117 MATCH_MP_TAC REAL_LT_MUL THEN ASM_SIMP_TAC[REAL_LT_MUL;REAL_FIELD `&0 < &2 `];
119 ASM_SIMP_TAC[REAL_LT_MUL;REAL_FIELD `!a b. &0 < a /\ &0 < b ==> &0 < &2*a + b ` ];
120 ALL_TAC] THEN ASM_SIMP_TAC[REAL_LT_DIV2_EQ ] THEN ASM_SIMP_TAC[REAL_LT_LDIV_EQ;REAL_MUL_SYM ]
121 THEN ASM_SIMP_TAC[GSYM REAL_LT_LDIV_EQ; REAL_FIELD `! d1 d2. &0 < d1 /\ &0 < d2 ==> &0 < (d1 * &4 + d2 * &2) `] THEN SUBGOAL_THEN `(&4 * d1 * d2) / (d1 * &4 + d2 * &2) = &2*(&2 * d1 * d2) / (&2*(d1 * &2 + d2 * &1)) ` ASSUME_TAC THENL[REAL_ARITH_TAC;ALL_TAC] THEN
122 ONCE_ASM_REWRITE_TAC[] THEN ASM_SIMP_TAC[REAL_FIELD `&2 * (&2 * d1 * d2) / (&2 * (d1 * &2 + d2 * &1)) =(&2 * d1 * d2) / ((&2*d1 + d2))`]);;