1 (* ========================================================================= *)
3 (* Fabry Perot 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 (* ========================================================================= *)
16 needs "geometrical_optics.ml";;
17 needs "resonator.ml";;
19 let VALID_RESONATOR_TAC x =
20 SIMP_TAC[x;is_valid_resonator;is_valid_optical_component;ALL;
21 is_valid_free_space;is_valid_interface]
22 THEN CONV_TAC REAL_FIELD;;
25 let fp_mat_half = new_definition
26 `fp_mat_half R d = mat2x2 (&1) (d) (--(&2/R)) (&1 - (&2*d)/R) `;;
28 let fp_cavity = new_definition
29 `fp_cavity R d n :resonator =
30 ((spherical R),[],(n,d),(spherical R)) `;;
33 let VALID_FP_CAVITY = prove
35 ~(R= &0) /\ &0 < d /\ &0 < n ==>
36 is_valid_resonator (fp_cavity R d n)`,
37 VALID_RESONATOR_TAC fp_cavity);;
41 (`!R d. ~(R= &0) /\ &0 < d ==> trace (fp_mat_half R d) = &2 - &2*d/R`,
42 SIMP_TAC[TRACE_MAT2X2;fp_mat_half] THEN CONV_TAC REAL_FIELD);;
45 (`!R d n. ~(R= &0) /\ &0 < d/R /\ d/R < &2 /\ &0 < n /\ &0 < d ==>
46 is_stable_resonator (fp_cavity R d n)`,
47 REPEAT STRIP_TAC THEN MP_REWRITE_TAC STABILITY_THEOREM_SYM THEN
48 EXISTS_TAC(`(fp_mat_half R d):real^2^2`) THEN
49 REWRITE_TAC[MAT_POW2;fp_mat_half] THEN CONJ_TAC THENL[
50 ASM_SIMP_TAC[VALID_FP_CAVITY ];ALL_TAC] THEN CONJ_TAC THENL[
51 REWRITE_TAC[system_composition;unfold_resonator;LIST_POW;ONE;fp_cavity;
52 round_trip;APPEND;optical_components_shift;LET_DEF;LET_END_DEF;REVERSE;
53 interface_matrix;head_index;free_space_matrix] THEN
54 REPEAT(POP_ASSUM MP_TAC) THEN REWRITE_TAC[GSYM ONE]
55 THEN SIMP_TAC[GSYM MATRIX_MUL_ASSOC] THEN
56 SIMP_TAC[ MAT2X2_MUL;REAL_MUL_RZERO;REAL_MUL_LZERO;REAL_ADD_LID;REAL_ADD_RID;
57 REAL_MUL_LID;REAL_MUL_RID ] THEN
58 SIMP_TAC[MAT2X2_EQ ] THEN CONV_TAC REAL_FIELD; ALL_TAC] THEN
59 REPEAT(POP_ASSUM MP_TAC) THEN
60 REWRITE_TAC[DET_MAT2X2] THEN REWRITE_TAC[mat2x2;VECTOR_2] THEN
61 CONV_TAC REAL_FIELD);;