(* ========================================================================= *) (* *) (* Optical Resoantors *) (* *) (* (c) Copyright, Muhammad Umair Siddique, Vincent Aravantinos, 2012 *) (* Hardware Verification Group, *) (* Concordia University *) (* *) (* Contact: , *) (* *) (* Last update: Feb 16, 2012 *) (* *) (* ========================================================================= *) needs "geometrical_optics.ml";; (* ------------------------------------------------------------------------- *) (* Resonators Formalization *) (* ------------------------------------------------------------------------- *) new_type_abbrev("resonator", `:interface # optical_component list # free_space # interface`);; let FORALL_RESONATOR_THM = prove (`!P. (!res:resonator. P res) <=> !i1 cs fs i2. P (i1,cs,fs,i2)`, REWRITE_TAC[FORALL_PAIR_THM]);; (* Shifts the free spaces in a list of optical components from right to left. * Takes an additional free space parameter to insert in place of the ``hole'' * remainining on the right. * Returns an additional free space corresponding to the leftmost free space * that is ``thrown away'' by the shifting. *) let optical_components_shift = define `optical_components_shift [] fs' = [], fs' /\ optical_components_shift (CONS (fs,i) cs) fs' = let cs',fs'' = optical_components_shift cs fs' in CONS (fs'',i) cs', fs`;; let OPTICAL_COMPONENTS_SHIFT_THROWN_IN = prove (`!cs:optical_component list fs. let cs',fs'' = optical_components_shift cs fs in cs = [] \/ ?i cs''. cs = CONS (fs'',i) cs''`, MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[optical_components_shift;FORALL_OPTICAL_COMPONENT_THM; LET_PAIR] THEN MESON_TAC[]);; let VALID_OPTICAL_COMPONENTS_SHIFT = prove (`!cs:optical_component list fs. ALL is_valid_optical_component cs /\ is_valid_free_space fs ==> let cs',fs' = optical_components_shift cs fs in ALL is_valid_optical_component cs' /\ is_valid_free_space fs'`, MATCH_MP_TAC list_INDUCT THEN SIMP_TAC[ALL;optical_components_shift;LET_PAIR; FORALL_OPTICAL_COMPONENT_THM;is_valid_optical_component]);; let round_trip = new_definition `round_trip ((i1,cs,fs,i2) : resonator) = APPEND cs (CONS (fs,i2,reflected) ( let cs',fs1 = optical_components_shift cs fs in REVERSE (CONS (fs1,i1,reflected) cs')))`;; let ROUND_TRIP_NIL = prove (`!i1 fs i2. round_trip (i1,[],fs,i2) = [fs,i2,reflected;fs,i1,reflected]`, REWRITE_TAC[round_trip;APPEND;optical_components_shift;LET_DEF; LET_END_DEF;REVERSE]);; let HEAD_INDEX_ROUND_TRIP = prove (`!i1 cs fs i2. head_index (round_trip (i1,cs,fs,i2),fs) = head_index (cs,fs)`, GEN_TAC THEN MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[round_trip;APPEND;head_index;FORALL_FREE_SPACE_THM; FORALL_OPTICAL_COMPONENT_THM]);; let LIST_POW = define `LIST_POW l 0 = [] /\ LIST_POW l (SUC n) = APPEND l (LIST_POW l n)`;; let ALL_LIST_POW = prove (`!n l P. ALL P (LIST_POW l n) <=> n = 0 \/ ALL P l`, INDUCT_TAC THEN ASM_REWRITE_TAC[LIST_POW;ALL;ALL_APPEND;NOT_SUC] THEN ITAUT_TAC);; let SYSTEM_COMPOSITION_APPEND = prove (`!cs1 cs2 fs. system_composition (APPEND cs1 cs2,fs) = system_composition (cs2,fs) ** system_composition (cs1,head_index (cs2,fs),&0)`, MATCH_MP_TAC list_INDUCT THEN SIMP_TAC[free_space_matrix;MAT2X2_ID;FORALL_OPTICAL_COMPONENT_THM;APPEND; FORALL_FREE_SPACE_THM;system_composition;GSYM HEAD_INDEX_APPEND; MATRIX_MUL_ASSOC]);; let is_valid_resonator = new_definition `is_valid_resonator ((i1,cs,fs,i2):resonator) <=> is_valid_interface i1 /\ ALL is_valid_optical_component cs /\ is_valid_free_space fs /\ is_valid_interface i2`;; (*------- Generates a resonator unfolded n times ------- *) let unfold_resonator = define `unfold_resonator (i1,cs,fs,i2) n = LIST_POW (round_trip (i1,cs,fs,i2)) n, (head_index (cs,fs),&0)`;; let VALID_UNFOLD_RESONATOR = prove (`!res. is_valid_resonator res ==> !n. is_valid_optical_system (unfold_resonator res n)`, REWRITE_TAC[FORALL_RESONATOR_THM;is_valid_resonator] THEN REPEAT (INDUCT_TAC ORELSE STRIP_TAC) THEN REWRITE_TAC [FORALL_OPTICAL_SYSTEM_THM;is_valid_optical_system; unfold_resonator;LIST_POW;ALL;ALL_APPEND;is_valid_free_space;REAL_LE_REFL] THEN MP_REWRITE_TAC HEAD_INDEX_VALID_OPTICAL_SYSTEM THEN ASM_SIMP_TAC[is_valid_optical_system;ALL_LIST_POW;round_trip;ALL_APPEND; TAUT `A /\ (B \/ A) <=> A`;ALL;is_valid_optical_component;LET_PAIR; ALL_REVERSE;REWRITE_RULE[LET_PAIR] VALID_OPTICAL_COMPONENTS_SHIFT]);; let RESONATOR_MATRIX = prove (`!n res. system_composition (unfold_resonator res n) = system_composition (unfold_resonator res 1) pow n`, INDUCT_TAC THEN REWRITE_TAC[FORALL_RESONATOR_THM] THENL [ REWRITE_TAC[unfold_resonator;mat_pow;system_composition;free_space_matrix; MAT2X2_MAT1;LIST_POW]; POP_ASSUM (fun x -> REWRITE_TAC[GSYM x;MAT_POW_ALT]) THEN REWRITE_TAC[unfold_resonator;LIST_POW;ONE;APPEND_NIL; SYSTEM_COMPOSITION_APPEND] THEN REPEAT GEN_TAC THEN STRUCT_CASES_TAC (Pa.SPEC "n" num_CASES) THEN REWRITE_TAC[LIST_POW;head_index] THEN Pa.PARSE_IN_CONTEXT (STRUCT_CASES_TAC o C ISPEC list_CASES) "cs" THEN REWRITE_TAC[ROUND_TRIP_NIL;APPEND;HEAD_INDEX_CONS_ALT] THEN REWRITE_TAC[round_trip;APPEND] THEN (REPEAT (REWRITE_TAC[PAIR_EQ] THEN (MATCH_MP_TAC HEAD_INDEX_CONS_EQ_ALT ORELSE AP_TERM_TAC))) ]);; (* ------------------------------------------------------------------------- *) (* Stability analysis *) (* ------------------------------------------------------------------------- *) let is_stable_resonator = new_definition `is_stable_resonator (res:resonator) <=> !r. ?y theta. !n. is_valid_ray_in_system r (unfold_resonator res n) ==> let y',theta' = last_single_ray r in abs y' <= y /\ abs theta' <= theta`;; let REAL_REDUCE_TAC = CONV_TAC (DEPTH_CONV (CHANGED_CONV REAL_POLY_CONV));; let SYLVESTER_THEOREM = prove (`!A B C D . det (mat2x2 A B C D) = &1 /\ -- &1 < (A + D) / &2 /\ (A + D) / &2 < &1 ==> let theta = acs ((A + D) / &2) in !N. (mat2x2 A B C D) pow N = (&1 / sin theta) %% (mat2x2 (A * sin (&N * theta) - sin((&N - &1) * theta)) (B * sin (&N * theta)) (C * sin (&N * theta)) (D * sin (&N*theta) - sin ((&N - &1)* theta)))`, REWRITE_TAC[MAT2X2_DET;LET_DEF;LET_END_DEF] THEN REPEAT (INDUCT_TAC ORELSE STRIP_TAC) THEN REPEAT (POP_ASSUM MP_TAC) THEN SIMP_TAC[mat_pow;MAT2X2_MUL;MAT2X2_SCALAR_MUL;MAT2X2_EQ; GSYM REAL_OF_NUM_SUC;GSYM MAT2X2_MAT1] THEN ONCE_REWRITE_TAC[GSYM REAL_SUB_0] THEN REAL_REDUCE_TAC THEN SIMP_TAC[SIN_0;GSYM REAL_NEG_MINUS1;SIN_NEG;SIN_ADD;COS_NEG] THEN REAL_REDUCE_TAC THEN SIMP_TAC[REAL_MUL_LINV;SIN_ACS_NZ] THEN SIMP_TAC[REAL_LT_IMP_LE;COS_ACS;SIN_ACS] THEN REAL_REDUCE_TAC THEN SIMP_TAC [REAL_ARITH `x + -- &1 * y + z = t <=> x = t + y - z`; REAL_ARITH `-- &1 * x * y * z = --(x * y) * z`] THEN CONV_TAC REAL_FIELD);; let SYLVESTER_THEOREM_ALT = prove (` ! (N:num) (A:real) B C D . theta = acs((A + D)/ &2) /\ (det (mat2x2 A B C D) = &1) /\ -- &1 <((A + D)/ &2) /\ ((A + D)/ &2) < &1 ==> ((mat2x2 A B C D) pow N = (&1/sin(theta)) %% (mat2x2 (A*sin(&N*theta)- sin((&N - (&1))* theta)) (B*sin(&N*theta)) (C*sin(&N*theta)) (D*sin(&N*theta)- sin((&N - (&1))* theta)))) `, SUBGOAL_THEN` !A B C D. det (mat2x2 A B C D) = &1 /\ -- &1 < (A + D) / &2 /\ (A + D) / &2 < &1 ==> (let theta = acs ((A + D) / &2) in !N. mat2x2 A B C D pow N = &1 / sin theta %% mat2x2 (A * sin (&N * theta) - sin ((&N - &1) * theta)) (B * sin (&N * theta)) (C * sin (&N * theta)) (D * sin (&N * theta) - sin ((&N - &1) * theta))) ` ASSUME_TAC THENL[SIMP_TAC[SYLVESTER_THEOREM];ALL_TAC] THEN POP_ASSUM MP_TAC THEN LET_TAC THEN ASM_SIMP_TAC[]);; let STABILITY_LEMMA = prove(` ! A B C D xi thetai. det (mat2x2 A B C D) = &1 /\ -- &1 < (A + D) / &2 /\ (A + D) / &2 < &1 ==> ?(Y:real^2). !n. abs ((mat2x2 A B C D pow n ** vector [xi; thetai])$1) <= Y$1 /\ abs ((mat2x2 A B C D pow n ** vector [xi; thetai])$2) <= Y$2`, REPEAT STRIP_TAC THEN EXISTS_TAC(`vector[ ((abs (&1 / sin (acs ((A + D) / &2))) * abs xi)* &1 + (abs (&1 / sin (acs ((A + D) / &2))) * abs A * abs xi)*abs (&1)) + (abs (&1 / sin (acs ((A + D) / &2))) * abs B * abs thetai)* (&1) ; (abs (&1 / sin (acs ((A + D) / &2))) * abs C * abs xi)* abs(&1) + ((abs (&1 / sin (acs ((A + D) / &2))) * abs thetai)* abs(&1) + (abs (&1 / sin (acs ((A + D) / &2))) * abs D * abs thetai)* abs(&1))]:real^2`) THEN GEN_TAC THEN SUBGOAL_THEN `!N. mat2x2 A B C D pow N = &1 / sin (acs ((A + D) / &2)) %% mat2x2 (A * sin (&N * (acs ((A + D) / &2))) - sin ((&N - &1) * (acs ((A + D) / &2)))) (B * sin (&N * (acs ((A + D) / &2)))) (C * sin (&N * (acs ((A + D) / &2)))) (D * sin (&N * (acs ((A + D) / &2))) - sin ((&N - &1) * (acs ((A + D) / &2)))) ` ASSUME_TAC THENL[GEN_TAC THEN MATCH_MP_TAC SYLVESTER_THEOREM_ALT THEN ASM_SIMP_TAC[];ALL_TAC] THEN ONCE_ASM_REWRITE_TAC[] THEN CONJ_TAC THENL[ SIMP_TAC[ MAT2X2_VECTOR_MUL; MAT2X2_SCALAR_MUL;VECTOR_2] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC(` abs ((&1 / sin (acs ((A + D) / &2)) * (A * sin (&n * (acs ((A + D) / &2))) - sin ((&n - &1) * (acs ((A + D) / &2))))) * xi) + abs((&1 / sin (acs ((A + D) / &2)) * B * sin (&n * (acs ((A + D) / &2)))) * thetai)`) THEN SIMP_TAC[REAL_ABS_TRIANGLE] THEN MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC THENL[ SIMP_TAC[REAL_SUB_LDISTRIB;REAL_SUB_RDISTRIB] THEN SUBGOAL_THEN ` abs ((&1 / sin (acs ((A + D) / &2)) * A * sin (&n * (acs ((A + D) / &2)))) * xi - (&1 / sin (acs ((A + D) / &2)) * sin (&n * (acs ((A + D) / &2)) - &1 * (acs ((A + D) / &2)))) * xi) = abs ((&1 / sin (acs ((A + D) / &2)) * A * xi) * sin (&n * (acs ((A + D) / &2))) - (((&1 / sin (acs ((A + D) / &2))) *xi)* sin (&n * (acs ((A + D) / &2)) - &1 * (acs ((A + D) / &2)))))` ASSUME_TAC THENL[ REAL_ARITH_TAC; ALL_TAC] THEN ONCE_ASM_REWRITE_TAC[] THEN SIMP_TAC[REAL_FIELD `!(a:real) b. (b - a)= (--a + b)`] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC(` abs (--((&1 / sin (acs ((A + D) / &2)) * xi) * sin (--(&1 * (acs ((A + D) / &2))) + &n * (acs ((A + D) / &2))))) + abs( (&1 / sin (acs ((A + D) / &2)) * A * xi) * sin (&n * (acs ((A + D) / &2)))) `) THEN SIMP_TAC[REAL_ABS_TRIANGLE] THEN SIMP_TAC[REAL_ABS_NEG;REAL_ABS_MUL] THEN MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC THENL[ MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS] THEN CONJ_TAC THENL[ SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] THEN SIMP_TAC[REAL_LE_LT;SIN_BOUND];ALL_TAC] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN CONJ_TAC THENL[ SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS] THEN CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT]; ALL_TAC] THEN CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT]; ALL_TAC] THEN SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] THEN SIMP_TAC[REAL_ABS_POS;REAL_ABS_1;SIN_BOUND] THEN SIMP_TAC[REAL_LE_LT]; ALL_TAC] THEN SUBGOAL_THEN `abs ((&1 / sin (acs ((A + D) / &2)) * B * sin (&n * (acs ((A + D) / &2)))) * thetai)= abs ((&1 / sin (acs ((A + D) / &2)) * B *thetai)* sin (&n * (acs ((A + D) / &2)))) ` ASSUME_TAC THENL [REAL_ARITH_TAC;ALL_TAC] THEN ONCE_ASM_REWRITE_TAC[] THEN SIMP_TAC[REAL_ABS_MUL] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS] THEN CONJ_TAC THENL[ SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS] THEN CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] THEN SIMP_TAC[SIN_BOUND] THEN SIMP_TAC[REAL_LE_LT]; ALL_TAC] THEN SIMP_TAC[ MAT2X2_VECTOR_MUL; MAT2X2_SCALAR_MUL;VECTOR_2] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC(` abs ((&1 / sin (acs ((A + D) / &2)) * C * sin (&n * (acs ((A + D) / &2)))) * xi) + abs((&1 / sin (acs ((A + D) / &2)) * (D * sin (&n * (acs ((A + D) / &2))) - sin ((&n - &1) * (acs ((A + D) / &2))))) * thetai) `) THEN SIMP_TAC[REAL_ABS_TRIANGLE] THEN MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC THENL[SUBGOAL_THEN `abs ((&1 / sin (acs ((A + D) / &2)) * C * sin (&n * (acs ((A + D) / &2)))) * xi) = abs ((&1 / sin (acs ((A + D) / &2)) * C * xi)* sin (&n * (acs ((A + D) / &2)))) ` ASSUME_TAC THENL[REAL_ARITH_TAC;ALL_TAC] THEN ONCE_ASM_REWRITE_TAC[] THEN SIMP_TAC[REAL_ABS_MUL] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS;SIN_BOUND;REAL_ABS_1] THEN CONJ_TAC THENL[ SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS] THEN CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] THEN SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN SIMP_TAC[REAL_SUB_LDISTRIB;REAL_SUB_RDISTRIB] THEN SUBGOAL_THEN `abs ((&1 / sin (acs ((A + D) / &2)) * D * sin (&n * (acs ((A + D) / &2)))) * thetai - (&1 / sin (acs ((A + D) / &2)) * sin (&n * (acs ((A + D) / &2)) - &1 * (acs ((A + D) / &2)))) * thetai) = abs ((&1 / sin (acs ((A + D) / &2)) * D * thetai )*sin (&n * (acs ((A + D) / &2))) - (&1 / sin (acs ((A + D) / &2)) * thetai) * sin (&n * (acs ((A + D) / &2)) - &1 * (acs ((A + D) / &2)))) ` ASSUME_TAC THENL[ REAL_ARITH_TAC;ALL_TAC] THEN ONCE_ASM_REWRITE_TAC[] THEN SIMP_TAC[REAL_FIELD `!(a:real) b. (b - a)= (--a + b)`] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC(` abs (--((&1 / sin (acs ((A + D) / &2)) * thetai) * sin (--(&1 * (acs ((A + D) / &2))) + &n * (acs ((A + D) / &2))))) + abs( (&1 / sin (acs ((A + D) / &2)) * D * thetai) * sin (&n * (acs ((A + D) / &2)))) `) THEN SIMP_TAC[REAL_ABS_TRIANGLE] THEN SIMP_TAC[REAL_ABS_NEG;REAL_ABS_MUL] THEN MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC THENL[MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS;REAL_ABS_1;SIN_BOUND] THEN CONJ_TAC THENL[ SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] THEN SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS;REAL_ABS_1;SIN_BOUND] THEN CONJ_TAC THENL[SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b`] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS] THEN CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] THEN SIMP_TAC[REAL_LE_LT]);; let STABILITY_LEMMA_GENERAL = prove(`! (M:real^2^2) xi thetai. det (M) = &1 /\ -- &1 < (M$1$1 + M$2$2) / &2 /\ (M$1$1 + M$2$2) / &2 < &1 ==> ?(Y:real^2). !n. abs ((M pow n ** vector [xi; thetai])$1) <= Y$1 /\ abs ((M pow n ** vector [xi; thetai])$2) <= Y$2`, REWRITE_TAC[FORALL_MATRIX_2X2] THEN REPEAT STRIP_TAC THEN MATCH_MP_TAC STABILITY_LEMMA THEN REPEAT(POP_ASSUM MP_TAC) THEN SIMP_TAC [mat2x2;CART_EQ;VECTOR_2;DIMINDEX_2;FORALL_2;DOT_2;SUM_2]);; let STABILITY_THEOREM = prove (` !res. is_valid_resonator res /\ (!n. let M = system_composition (unfold_resonator res 1) in (det M = &1) /\ -- &1 < (M$1$1 + M$2$2) / &2 /\ (M$1$1 + M$2$2) / &2 < &1) ==> is_stable_resonator res`, GEN_TAC THEN REPEAT (LET_TAC) THEN REPEAT STRIP_TAC THEN REPEAT STRIP_TAC THEN REWRITE_TAC[is_stable_resonator] THEN GEN_TAC THEN SUBGOAL_THEN ` (?Y:real^2. !n. abs ((M pow n ** vector [FST(fst_single_ray r);SND(fst_single_ray r) ])$1) <= Y$1 /\ abs (((M:real^2^2) pow n ** vector [FST(fst_single_ray r);SND(fst_single_ray r) ])$2) <= Y$2)` ASSUME_TAC THENL[MP_REWRITE_TAC STABILITY_LEMMA_GENERAL THEN ASM_SIMP_TAC[];ALL_TAC] THEN POP_ASSUM MP_TAC THEN STRIP_TAC THEN EXISTS_TAC(`((Y:real^2)$1):real`) THEN EXISTS_TAC(`((Y:real^2)$2):real`) THEN REPEAT STRIP_TAC THEN LET_TAC THEN SUBGOAL_THEN `(let (xi,thetai),(y1,theta1),rs = r in let y',theta' = last_single_ray r in vector [y'; theta'] = system_composition ((unfold_resonator res n):optical_system) ** vector [xi; thetai])` ASSUME_TAC THENL[MATCH_MP_TAC SYSTEM_MATRIX THEN ASM_SIMP_TAC[ VALID_UNFOLD_RESONATOR ]; ALL_TAC] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[ MAT2X2_VECTOR_MUL_ALT] THEN ONCE_REWRITE_TAC[RESONATOR_MATRIX] THEN ONCE_ASM_REWRITE_TAC[] THEN LET_TAC THEN LET_TAC THEN DISCH_TAC THEN ONCE_ASM_REWRITE_TAC[] THEN REPEAT(POP_ASSUM MP_TAC) THEN REWRITE_TAC[fst_single_ray;FST;SND] THEN SIMP_TAC[]);; (*-----------------Stability theorem for the symmetric resonators ------------------*) let STABILITY_LEMMA_SYM = prove (` ! A B C D xi thetai. det (mat2x2 A B C D) = &1 /\ -- &1 < (A + D) / &2 /\ (A + D) / &2 < &1 ==> ?(Y:real^2). !n. abs (((mat2x2 A B C D pow 2)pow n ** vector [xi; thetai])$1) <= Y$1 /\ abs (((mat2x2 A B C D pow 2) pow n ** vector [xi; thetai])$2) <= Y$2`, REWRITE_TAC[MAT2X2_POW2_POW] THEN REPEAT STRIP_TAC THEN EXISTS_TAC(`vector[ ((abs (&1 / sin (acs ((A + D) / &2))) * abs xi)* &1 + (abs (&1 / sin (acs ((A + D) / &2))) * abs A * abs xi)*abs (&1)) + (abs (&1 / sin (acs ((A + D) / &2))) * abs B * abs thetai)* (&1) ; (abs (&1 / sin (acs ((A + D) / &2))) * abs C * abs xi)* abs(&1) + ((abs (&1 / sin (acs ((A + D) / &2))) * abs thetai)* abs(&1) + (abs (&1 / sin (acs ((A + D) / &2))) * abs D * abs thetai)* abs(&1))]:real^2`) THEN GEN_TAC THEN SUBGOAL_THEN `!N. mat2x2 A B C D pow (2*N) = &1 / sin (acs ((A + D) / &2)) %% mat2x2 (A * sin (&(2*N) * (acs ((A + D) / &2))) - sin ((&(2*N) - &1) * (acs ((A + D) / &2)))) (B * sin (&(2*N) * (acs ((A + D) / &2)))) (C * sin (&(2*N) * (acs ((A + D) / &2)))) (D * sin (&(2*N) * (acs ((A + D) / &2))) - sin ((&(2*N) - &1) * (acs ((A + D) / &2)))) ` ASSUME_TAC THENL[GEN_TAC THEN MATCH_MP_TAC SYLVESTER_THEOREM_ALT THEN ASM_SIMP_TAC[];ALL_TAC] THEN ONCE_ASM_REWRITE_TAC[] THEN CONJ_TAC THENL[SIMP_TAC[ MAT2X2_VECTOR_MUL; MAT2X2_SCALAR_MUL;VECTOR_2] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC(` abs ((&1 / sin (acs ((A + D) / &2)) * (A * sin (&(2*n) * (acs ((A + D) / &2))) - sin ((&(2*n) - &1) * (acs ((A + D) / &2))))) * xi) + abs((&1 / sin (acs ((A + D) / &2)) * B * sin (&(2*n) * (acs ((A + D) / &2)))) * thetai)`) THEN SIMP_TAC[REAL_ABS_TRIANGLE] THEN MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC THENL[ SIMP_TAC[REAL_SUB_LDISTRIB;REAL_SUB_RDISTRIB] THEN SUBGOAL_THEN ` abs ((&1 / sin (acs ((A + D) / &2)) * A * sin (&(2*n) * (acs ((A + D) / &2)))) * xi - (&1 / sin (acs ((A + D) / &2)) * sin (&(2*n) * (acs ((A + D) / &2)) - &1 * (acs ((A + D) / &2)))) * xi) = abs ((&1 / sin (acs ((A + D) / &2)) * A * xi) * sin (&(2*n) * (acs ((A + D) / &2))) - (((&1 / sin (acs ((A + D) / &2))) *xi)* sin (&(2*n) * (acs ((A + D) / &2)) - &1 * (acs ((A + D) / &2)))))` ASSUME_TAC THENL[ REAL_ARITH_TAC; ALL_TAC] THEN ONCE_ASM_REWRITE_TAC[] THEN SIMP_TAC[REAL_FIELD `!(a:real) b. (b - a)= (--a + b)`] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC(` abs (--((&1 / sin (acs ((A + D) / &2)) * xi) * sin (--(&1 * (acs ((A + D) / &2))) + &(2*n) * (acs ((A + D) / &2))))) + abs( (&1 / sin (acs ((A + D) / &2)) * A * xi) * sin (&(2*n) * (acs ((A + D) / &2)))) `) THEN SIMP_TAC[REAL_ABS_TRIANGLE] THEN SIMP_TAC[REAL_ABS_NEG;REAL_ABS_MUL] THEN MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC THENL[ MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS] THEN CONJ_TAC THENL[ SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] THEN SIMP_TAC[REAL_LE_LT;SIN_BOUND];ALL_TAC] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN CONJ_TAC THENL[ SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS] THEN CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT]; ALL_TAC] THEN CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT]; ALL_TAC] THEN SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] THEN SIMP_TAC[REAL_ABS_POS;REAL_ABS_1;SIN_BOUND] THEN SIMP_TAC[REAL_LE_LT]; ALL_TAC] THEN SUBGOAL_THEN `abs ((&1 / sin (acs ((A + D) / &2)) * B * sin (&(2*n) * (acs ((A + D) / &2)))) * thetai)= abs ((&1 / sin (acs ((A + D) / &2)) * B *thetai)* sin (&(2*n) * (acs ((A + D) / &2)))) ` ASSUME_TAC THENL [REAL_ARITH_TAC;ALL_TAC] THEN ONCE_ASM_REWRITE_TAC[] THEN SIMP_TAC[REAL_ABS_MUL] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS] THEN CONJ_TAC THENL[ SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS] THEN CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] THEN SIMP_TAC[SIN_BOUND] THEN SIMP_TAC[REAL_LE_LT]; ALL_TAC] THEN SIMP_TAC[ MAT2X2_VECTOR_MUL; MAT2X2_SCALAR_MUL;VECTOR_2] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC(` abs ((&1 / sin (acs ((A + D) / &2)) * C * sin (&(2*n) * (acs ((A + D) / &2)))) * xi) + abs((&1 / sin (acs ((A + D) / &2)) * (D * sin (&(2*n) * (acs ((A + D) / &2))) - sin ((&(2*n) - &1) * (acs ((A + D) / &2))))) * thetai) `) THEN SIMP_TAC[REAL_ABS_TRIANGLE] THEN MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC THENL[SUBGOAL_THEN `abs ((&1 / sin (acs ((A + D) / &2)) * C * sin (&(2*n) * (acs ((A + D) / &2)))) * xi) = abs ((&1 / sin (acs ((A + D) / &2)) * C * xi)* sin (&(2*n) * (acs ((A + D) / &2)))) ` ASSUME_TAC THENL[REAL_ARITH_TAC;ALL_TAC] THEN ONCE_ASM_REWRITE_TAC[] THEN SIMP_TAC[REAL_ABS_MUL] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS;SIN_BOUND;REAL_ABS_1] THEN CONJ_TAC THENL[ SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS] THEN CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] THEN SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN SIMP_TAC[REAL_SUB_LDISTRIB;REAL_SUB_RDISTRIB] THEN SUBGOAL_THEN `abs ((&1 / sin (acs ((A + D) / &2)) * D * sin (&(2*n) * (acs ((A + D) / &2)))) * thetai - (&1 / sin (acs ((A + D) / &2)) * sin (&(2*n) * (acs ((A + D) / &2)) - &1 * (acs ((A + D) / &2)))) * thetai) = abs ((&1 / sin (acs ((A + D) / &2)) * D * thetai )*sin (&(2*n) * (acs ((A + D) / &2))) - (&1 / sin (acs ((A + D) / &2)) * thetai) * sin (&(2*n) * (acs ((A + D) / &2)) - &1 * (acs ((A + D) / &2)))) ` ASSUME_TAC THENL[ REAL_ARITH_TAC;ALL_TAC] THEN ONCE_ASM_REWRITE_TAC[] THEN SIMP_TAC[REAL_FIELD `!(a:real) b. (b - a)= (--a + b)`] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC(` abs (--((&1 / sin (acs ((A + D) / &2)) * thetai) * sin (--(&1 * (acs ((A + D) / &2))) + &(2*n) * (acs ((A + D) / &2))))) + abs( (&1 / sin (acs ((A + D) / &2)) * D * thetai) * sin (&(2*n) * (acs ((A + D) / &2)))) `) THEN SIMP_TAC[REAL_ABS_TRIANGLE] THEN SIMP_TAC[REAL_ABS_NEG;REAL_ABS_MUL] THEN MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC THENL[MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS;REAL_ABS_1;SIN_BOUND] THEN CONJ_TAC THENL[ SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] THEN SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS;REAL_ABS_1;SIN_BOUND] THEN CONJ_TAC THENL[SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b`] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS] THEN CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] THEN SIMP_TAC[REAL_LE_LT]);; let STABILITY_LEMMA_GENERAL_SYM = prove(`! (M:real^2^2) xi thetai. det (M) = &1 /\ -- &1 < (M$1$1 + M$2$2) / &2 /\ (M$1$1 + M$2$2) / &2 < &1 ==> ?(Y:real^2). !n. abs (((M pow 2) pow n ** vector [xi; thetai])$1) <= Y$1 /\ abs (((M pow 2) pow n ** vector [xi; thetai])$2) <= Y$2`, REWRITE_TAC[FORALL_MATRIX_2X2] THEN REPEAT STRIP_TAC THEN MATCH_MP_TAC STABILITY_LEMMA_SYM THEN REPEAT(POP_ASSUM MP_TAC) THEN SIMP_TAC [mat2x2;CART_EQ;VECTOR_2;DIMINDEX_2;FORALL_2;DOT_2;SUM_2]);; let STABILITY_THEOREM_SYM = prove ( `!res. is_valid_resonator res /\ ((M:real^2^2) pow 2 = system_composition (unfold_resonator res 1)) /\ (det (M:real^2^2) = &1) /\ -- &1 < (M$1$1 + M$2$2) / &2 /\ (M$1$1 + M$2$2) / &2 < &1 ==> is_stable_resonator res`, GEN_TAC THEN ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN REPEAT STRIP_TAC THEN REWRITE_TAC[is_stable_resonator] THEN GEN_TAC THEN SUBGOAL_THEN ` (?Y:real^2. !n. abs (((M pow 2) pow n ** vector [FST(fst_single_ray r);SND(fst_single_ray r) ])$1) <= Y$1 /\ abs ((((M:real^2^2) pow 2 ) pow n ** vector [FST(fst_single_ray r);SND(fst_single_ray r) ])$2) <= Y$2) ` ASSUME_TAC THENL[ MP_REWRITE_TAC STABILITY_LEMMA_GENERAL_SYM THEN ASM_SIMP_TAC[]; ALL_TAC] THEN POP_ASSUM MP_TAC THEN STRIP_TAC THEN EXISTS_TAC(`((Y:real^2)$1):real`) THEN EXISTS_TAC(`((Y:real^2)$2):real`) THEN REPEAT STRIP_TAC THEN LET_TAC THEN SUBGOAL_THEN `(let (xi,thetai),(y1,theta1),rs = r in let y',theta' = last_single_ray r in vector [y'; theta'] = system_composition ((unfold_resonator res n):optical_system) ** vector [xi; thetai])` ASSUME_TAC THENL[ MATCH_MP_TAC SYSTEM_MATRIX THEN ASM_SIMP_TAC[ VALID_UNFOLD_RESONATOR];ALL_TAC] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[MAT2X2_VECTOR_MUL_ALT] THEN ONCE_REWRITE_TAC[RESONATOR_MATRIX] THEN ONCE_ASM_REWRITE_TAC[] THEN LET_TAC THEN LET_TAC THEN DISCH_TAC THEN ONCE_ASM_REWRITE_TAC[] THEN REPEAT(POP_ASSUM MP_TAC) THEN REWRITE_TAC[fst_single_ray;FST;SND] THEN SIMP_TAC[]);;