(* ========================================================================= *)
(*                                                                           *)
(*                        Optical Resoantors                                 *)
(*                                                                           *)
(*        (c) Copyright, Muhammad Umair Siddique, Vincent Aravantinos, 2012  *)
(*                       Hardware Verification Group,                        *)
(*                       Concordia University                                *)
(*                                                                           *)
(*     Contact: <muh_sidd@ece.concordia.ca>, <vincent@ece.concordia.ca>      *)
(*                                                                           *)
(* 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'`,
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]`,
let HEAD_INDEX_ROUND_TRIP = 
prove (`!i1 cs fs i2. head_index (round_trip (i1,cs,fs,i2),fs) = head_index (cs,fs)`,
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)`,
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)`,
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[]);;