resonator.ml

   1 (* ========================================================================= *)\r
   2 (*                                                                           *)\r
   3 (*                        Optical Resoantors                                 *)\r
   4 (*                                                                           *)\r
   5 (*        (c) Copyright, Muhammad Umair Siddique, Vincent Aravantinos, 2012  *)\r
   6 (*                       Hardware Verification Group,                        *)\r
   7 (*                       Concordia University                                *)\r
   8 (*                                                                           *)\r
   9 (*     Contact: <muh_sidd@ece.concordia.ca>, <vincent@ece.concordia.ca>      *)\r
  10 (*                                                                           *)\r
  11 (* Last update: Feb 16, 2012                                                 *)\r
  12 (*                                                                           *)\r
  13 (* ========================================================================= *)\r
  14 \r
  15 \r
  16 needs "geometrical_optics.ml";;\r
  17 \r
  18 \r
  19 \r
  20 (* ------------------------------------------------------------------------- *)\r
  21 (* Resonators  Formalization                                                 *)\r
  22 (* ------------------------------------------------------------------------- *)\r
  23 \r
  24 new_type_abbrev("resonator",\r
  25   `:interface # optical_component list # free_space # interface`);;\r
  26 \r
  27 let FORALL_RESONATOR_THM = prove\r
  28   (`!P. (!res:resonator. P res) <=> !i1 cs fs i2. P (i1,cs,fs,i2)`,\r
  29   REWRITE_TAC[FORALL_PAIR_THM]);;\r
  30 \r
  31 \r
  32 (* Shifts the free spaces in a list of optical components from right to left.\r
  33  * Takes an additional free space parameter to insert in place of the ``hole''\r
  34  * remainining on the right.\r
  35  * Returns an additional free space corresponding to the leftmost free space\r
  36  * that is ``thrown away'' by the shifting.\r
  37  *)\r
  38 \r
  39 let optical_components_shift = define\r
  40  `optical_components_shift [] fs' = [], fs' /\\r
  41   optical_components_shift (CONS (fs,i) cs) fs' =\r
  42     let cs',fs'' = optical_components_shift cs fs' in\r
  43     CONS (fs'',i) cs', fs`;;\r
  44 \r
  45 let OPTICAL_COMPONENTS_SHIFT_THROWN_IN = prove\r
  46   (`!cs:optical_component list fs.\r
  47     let cs',fs'' = optical_components_shift cs fs in\r
  48     cs = [] \/ ?i cs''. cs = CONS (fs'',i) cs''`,\r
  49   MATCH_MP_TAC list_INDUCT\r
  50   THEN REWRITE_TAC[optical_components_shift;FORALL_OPTICAL_COMPONENT_THM;\r
  51     LET_PAIR]\r
  52   THEN MESON_TAC[]);;\r
  53 \r
  54 let VALID_OPTICAL_COMPONENTS_SHIFT = prove\r
  55   (`!cs:optical_component list fs.\r
  56     ALL is_valid_optical_component cs /\ is_valid_free_space fs ==>\r
  57       let cs',fs' = optical_components_shift cs fs in\r
  58       ALL is_valid_optical_component cs' /\ is_valid_free_space fs'`,\r
  59   MATCH_MP_TAC list_INDUCT THEN\r
  60   SIMP_TAC[ALL;optical_components_shift;LET_PAIR;\r
  61     FORALL_OPTICAL_COMPONENT_THM;is_valid_optical_component]);;\r
  62 \r
  63 let round_trip = new_definition\r
  64   `round_trip ((i1,cs,fs,i2) : resonator) =\r
  65      APPEND cs (CONS (fs,i2,reflected) (\r
  66        let cs',fs1 = optical_components_shift cs fs in\r
  67        REVERSE (CONS (fs1,i1,reflected) cs')))`;;\r
  68 \r
  69 let ROUND_TRIP_NIL = prove\r
  70   (`!i1 fs i2. round_trip (i1,[],fs,i2) = [fs,i2,reflected;fs,i1,reflected]`,\r
  71   REWRITE_TAC[round_trip;APPEND;optical_components_shift;LET_DEF;\r
  72     LET_END_DEF;REVERSE]);;\r
  73 \r
  74 let HEAD_INDEX_ROUND_TRIP = prove\r
  75   (`!i1 cs fs i2.\r
  76     head_index (round_trip (i1,cs,fs,i2),fs) = head_index (cs,fs)`,\r
  77     GEN_TAC THEN MATCH_MP_TAC list_INDUCT\r
  78     THEN REWRITE_TAC[round_trip;APPEND;head_index;FORALL_FREE_SPACE_THM;\r
  79       FORALL_OPTICAL_COMPONENT_THM]);;\r
  80 \r
  81 let LIST_POW = define\r
  82   `LIST_POW l 0 = [] /\\r
  83   LIST_POW l (SUC n) = APPEND l (LIST_POW l n)`;;\r
  84 \r
  85 let ALL_LIST_POW = prove\r
  86   (`!n l P. ALL P (LIST_POW l n) <=> n = 0 \/ ALL P l`,\r
  87   INDUCT_TAC THEN ASM_REWRITE_TAC[LIST_POW;ALL;ALL_APPEND;NOT_SUC]\r
  88   THEN ITAUT_TAC);;\r
  89 \r
  90 let SYSTEM_COMPOSITION_APPEND = prove\r
  91   (`!cs1 cs2 fs.\r
  92       system_composition (APPEND cs1 cs2,fs)\r
  93         = system_composition (cs2,fs)\r
  94           ** system_composition (cs1,head_index (cs2,fs),&0)`,\r
  95   MATCH_MP_TAC list_INDUCT\r
  96   THEN SIMP_TAC[free_space_matrix;MAT2X2_ID;FORALL_OPTICAL_COMPONENT_THM;APPEND;\r
  97     FORALL_FREE_SPACE_THM;system_composition;GSYM HEAD_INDEX_APPEND;\r
  98     MATRIX_MUL_ASSOC]);;\r
  99 \r
 100 let is_valid_resonator = new_definition\r
 101   `is_valid_resonator ((i1,cs,fs,i2):resonator) <=>\r
 102     is_valid_interface i1 /\ ALL is_valid_optical_component cs /\\r
 103     is_valid_free_space fs /\ is_valid_interface i2`;;\r
 104 \r
 105 (*------- Generates a resonator unfolded n times ------- *)\r
 106 \r
 107 let unfold_resonator = define\r
 108   `unfold_resonator (i1,cs,fs,i2) n =\r
 109     LIST_POW (round_trip (i1,cs,fs,i2)) n, (head_index (cs,fs),&0)`;;\r
 110 \r
 111 \r
 112 let VALID_UNFOLD_RESONATOR = prove\r
 113   (`!res. is_valid_resonator res ==>\r
 114       !n. is_valid_optical_system (unfold_resonator res n)`,\r
 115   REWRITE_TAC[FORALL_RESONATOR_THM;is_valid_resonator]\r
 116   THEN REPEAT (INDUCT_TAC ORELSE STRIP_TAC)\r
 117   THEN REWRITE_TAC [FORALL_OPTICAL_SYSTEM_THM;is_valid_optical_system;\r
 118     unfold_resonator;LIST_POW;ALL;ALL_APPEND;is_valid_free_space;REAL_LE_REFL]\r
 119   THEN MP_REWRITE_TAC HEAD_INDEX_VALID_OPTICAL_SYSTEM\r
 120   THEN ASM_SIMP_TAC[is_valid_optical_system;ALL_LIST_POW;round_trip;ALL_APPEND;\r
 121     TAUT `A /\ (B \/ A) <=> A`;ALL;is_valid_optical_component;LET_PAIR;\r
 122     ALL_REVERSE;REWRITE_RULE[LET_PAIR] VALID_OPTICAL_COMPONENTS_SHIFT]);;\r
 123 \r
 124 let RESONATOR_MATRIX = prove\r
 125   (`!n res.\r
 126     system_composition (unfold_resonator res n)\r
 127     = system_composition (unfold_resonator res 1) pow n`,\r
 128   INDUCT_TAC THEN REWRITE_TAC[FORALL_RESONATOR_THM]\r
 129   THENL [\r
 130     REWRITE_TAC[unfold_resonator;mat_pow;system_composition;free_space_matrix;\r
 131       MAT2X2_MAT1;LIST_POW];\r
 132     POP_ASSUM (fun x -> REWRITE_TAC[GSYM x;MAT_POW_ALT])\r
 133     THEN REWRITE_TAC[unfold_resonator;LIST_POW;ONE;APPEND_NIL;\r
 134       SYSTEM_COMPOSITION_APPEND]\r
 135     THEN REPEAT GEN_TAC\r
 136     THEN STRUCT_CASES_TAC (Pa.SPEC "n" num_CASES)\r
 137     THEN REWRITE_TAC[LIST_POW;head_index]\r
 138     THEN Pa.PARSE_IN_CONTEXT (STRUCT_CASES_TAC o C ISPEC list_CASES) "cs"\r
 139     THEN REWRITE_TAC[ROUND_TRIP_NIL;APPEND;HEAD_INDEX_CONS_ALT]\r
 140     THEN REWRITE_TAC[round_trip;APPEND]\r
 141     THEN (REPEAT (REWRITE_TAC[PAIR_EQ] THEN\r
 142       (MATCH_MP_TAC HEAD_INDEX_CONS_EQ_ALT ORELSE AP_TERM_TAC)))\r
 143   ]);;\r
 144 \r
 145 \r
 146 (* ------------------------------------------------------------------------- *)\r
 147 (* Stability analysis                                                        *)\r
 148 (* ------------------------------------------------------------------------- *)\r
 149 \r
 150 let is_stable_resonator = new_definition\r
 151   `is_stable_resonator (res:resonator) <=>\r
 152     !r. ?y theta.\r
 153       !n. is_valid_ray_in_system r (unfold_resonator res n) ==>\r
 154         let y',theta' = last_single_ray r in\r
 155         abs y' <= y /\ abs theta' <= theta`;;\r
 156 \r
 157 \r
 158 let REAL_REDUCE_TAC = CONV_TAC (DEPTH_CONV (CHANGED_CONV REAL_POLY_CONV));;\r
 159 \r
 160 let SYLVESTER_THEOREM = prove\r
 161   (`!A B C D . \r
 162     det (mat2x2 A B C D) = &1 /\ -- &1 < (A + D) / &2 /\ (A + D) / &2 < &1 ==>\r
 163       let theta = acs ((A + D) / &2) in\r
 164       !N.\r
 165         (mat2x2 A B C D) pow N  = \r
 166           (&1 / sin theta) %% (mat2x2\r
 167             (A * sin (&N * theta) - sin((&N - &1) * theta))\r
 168             (B * sin (&N * theta)) (C * sin (&N * theta))\r
 169             (D * sin (&N*theta) - sin ((&N - &1)* theta)))`,\r
 170   REWRITE_TAC[MAT2X2_DET;LET_DEF;LET_END_DEF]\r
 171   THEN REPEAT (INDUCT_TAC ORELSE STRIP_TAC) THEN REPEAT (POP_ASSUM MP_TAC)\r
 172   THEN SIMP_TAC[mat_pow;MAT2X2_MUL;MAT2X2_SCALAR_MUL;MAT2X2_EQ;\r
 173     GSYM REAL_OF_NUM_SUC;GSYM MAT2X2_MAT1]\r
 174   THEN ONCE_REWRITE_TAC[GSYM REAL_SUB_0] THEN REAL_REDUCE_TAC\r
 175   THEN SIMP_TAC[SIN_0;GSYM REAL_NEG_MINUS1;SIN_NEG;SIN_ADD;COS_NEG]\r
 176   THEN REAL_REDUCE_TAC THEN SIMP_TAC[REAL_MUL_LINV;SIN_ACS_NZ]\r
 177   THEN SIMP_TAC[REAL_LT_IMP_LE;COS_ACS;SIN_ACS] THEN REAL_REDUCE_TAC\r
 178   THEN SIMP_TAC\r
 179     [REAL_ARITH `x + -- &1 * y + z = t <=> x = t + y - z`;\r
 180     REAL_ARITH `-- &1 * x * y * z = --(x * y) * z`]\r
 181   THEN CONV_TAC REAL_FIELD);;\r
 182 \r
 183 \r
 184 let SYLVESTER_THEOREM_ALT = prove (` ! (N:num) (A:real) B C D . theta = acs((A + D)/ &2) /\ \r
 185   (det (mat2x2 A B C D)  = &1) /\ -- &1 <((A + D)/ &2) /\ \r
 186   ((A + D)/ &2) < &1  ==> ((mat2x2 A B C D) pow N  = \r
 187   (&1/sin(theta)) %% (mat2x2  (A*sin(&N*theta)- \r
 188   sin((&N - (&1))* theta))  (B*sin(&N*theta)) \r
 189   (C*sin(&N*theta))  (D*sin(&N*theta)-  sin((&N - (&1))* theta)))) `,\r
 190  SUBGOAL_THEN` !A B C D.\r
 191          det (mat2x2 A B C D) = &1 /\\r
 192          -- &1 < (A + D) / &2 /\\r
 193          (A + D) / &2 < &1\r
 194          ==> (let theta = acs ((A + D) / &2) in\r
 195               !N. mat2x2 A B C D pow N =\r
 196                   &1 / sin theta %%\r
 197                   mat2x2 (A * sin (&N * theta) - sin ((&N - &1) * theta))\r
 198                   (B * sin (&N * theta))\r
 199                   (C * sin (&N * theta))\r
 200                   (D * sin (&N * theta) - sin ((&N - &1) * theta))) ` ASSUME_TAC THENL[SIMP_TAC[SYLVESTER_THEOREM];ALL_TAC] THEN POP_ASSUM MP_TAC THEN\r
 201 LET_TAC THEN ASM_SIMP_TAC[]);;\r
 202 \r
 203 \r
 204 let STABILITY_LEMMA = prove(`\r
 205 ! A B C D xi thetai. det (mat2x2 A B C D) = &1 /\\r
 206            -- &1 < (A + D) / &2 /\ (A + D) / &2 < &1 ==>\r
 207      ?(Y:real^2). !n. abs ((mat2x2 A B C D pow n ** vector [xi; thetai])$1) <= Y$1 /\\r
 208              abs ((mat2x2 A B C D pow n ** vector [xi; thetai])$2) <= Y$2`,\r
 209 \r
 210 REPEAT STRIP_TAC THEN \r
 211 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)) \r
 212  + (abs (&1 / sin (acs ((A + D) / &2))) * abs B * abs thetai)* (&1) ;\r
 213 (abs (&1 / sin (acs ((A + D) / &2))) * abs C * abs xi)* abs(&1) + \r
 214 ((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 \r
 215 GEN_TAC THEN  SUBGOAL_THEN `!N. mat2x2 A B C D pow N =\r
 216              &1 / sin (acs ((A + D) / &2)) %%\r
 217              mat2x2 (A * sin (&N * (acs ((A + D) / &2))) - sin ((&N - &1) * (acs ((A + D) / &2))))\r
 218              (B * sin (&N * (acs ((A + D) / &2))))\r
 219              (C * sin (&N * (acs ((A + D) / &2))))\r
 220              (D * sin (&N * (acs ((A + D) / &2))) - sin ((&N - &1) * (acs ((A + D) / &2)))) ` ASSUME_TAC\r
 221 THENL[GEN_TAC THEN MATCH_MP_TAC SYLVESTER_THEOREM_ALT THEN \r
 222 ASM_SIMP_TAC[];ALL_TAC] THEN \r
 223 ONCE_ASM_REWRITE_TAC[] THEN\r
 224 CONJ_TAC \r
 225 \r
 226 THENL[\r
 227 \r
 228 SIMP_TAC[ MAT2X2_VECTOR_MUL; MAT2X2_SCALAR_MUL;VECTOR_2] THEN\r
 229 MATCH_MP_TAC REAL_LE_TRANS THEN  EXISTS_TAC(` abs\r
 230      ((&1 / sin (acs ((A + D) / &2)) * (A * sin (&n * (acs ((A + D) / &2))) - sin ((&n - &1) * (acs ((A + D) / &2))))) *\r
 231       xi) +\r
 232       abs((&1 / sin (acs ((A + D) / &2)) * B * sin (&n * (acs ((A + D) / &2)))) * thetai)`) THEN \r
 233 SIMP_TAC[REAL_ABS_TRIANGLE] THEN MATCH_MP_TAC REAL_LE_ADD2 THEN \r
 234 CONJ_TAC THENL[\r
 235 SIMP_TAC[REAL_SUB_LDISTRIB;REAL_SUB_RDISTRIB] THEN \r
 236 SUBGOAL_THEN ` abs\r
 237  ((&1 / sin (acs ((A + D) / &2)) * A * sin (&n * (acs ((A + D) / &2)))) * xi -\r
 238   (&1 / sin (acs ((A + D) / &2)) * sin (&n * (acs ((A + D) / &2)) - &1 * (acs ((A + D) / &2)))) * xi) = \r
 239 abs\r
 240  ((&1 / sin (acs ((A + D) / &2)) * A * xi) * sin (&n * (acs ((A + D) / &2))) -\r
 241   (((&1 / sin (acs ((A + D) / &2))) *xi)* sin (&n * (acs ((A + D) / &2)) - &1 * (acs ((A + D) / &2)))))` ASSUME_TAC THENL[\r
 242 REAL_ARITH_TAC; ALL_TAC] THEN \r
 243 ONCE_ASM_REWRITE_TAC[] THEN\r
 244 SIMP_TAC[REAL_FIELD `!(a:real) b. (b - a)= (--a + b)`] THEN \r
 245 MATCH_MP_TAC REAL_LE_TRANS THEN \r
 246 EXISTS_TAC(` abs\r
 247      (--((&1 / sin (acs ((A + D) / &2)) * xi) * sin (--(&1 * (acs ((A + D) / &2))) + &n * (acs ((A + D) / &2))))) +\r
 248      abs( (&1 / sin (acs ((A + D) / &2)) * A * xi) * sin (&n * (acs ((A + D) / &2)))) `) THEN \r
 249 SIMP_TAC[REAL_ABS_TRIANGLE] THEN \r
 250 SIMP_TAC[REAL_ABS_NEG;REAL_ABS_MUL] THEN \r
 251 MATCH_MP_TAC REAL_LE_ADD2 THEN \r
 252 \r
 253 CONJ_TAC THENL[\r
 254 MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS] THEN\r
 255 \r
 256 CONJ_TAC THENL[\r
 257 SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b  `] THEN\r
 258 MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] THEN\r
 259 \r
 260 SIMP_TAC[REAL_LE_LT;SIN_BOUND];ALL_TAC] THEN \r
 261 \r
 262 MATCH_MP_TAC REAL_LE_MUL2 THEN \r
 263 CONJ_TAC THENL[\r
 264 \r
 265 SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b  `] THEN \r
 266 MATCH_MP_TAC REAL_LE_MUL2 THEN \r
 267 SIMP_TAC[REAL_ABS_POS] THEN \r
 268 \r
 269 CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT]; ALL_TAC] THEN\r
 270 CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT]; ALL_TAC] THEN \r
 271 \r
 272 SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b  `] THEN \r
 273 MATCH_MP_TAC REAL_LE_MUL2 THEN \r
 274 SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] THEN \r
 275 \r
 276 SIMP_TAC[REAL_ABS_POS;REAL_ABS_1;SIN_BOUND] THEN \r
 277 SIMP_TAC[REAL_LE_LT]; ALL_TAC] THEN \r
 278 \r
 279 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 \r
 280 THENL [REAL_ARITH_TAC;ALL_TAC] THEN \r
 281 ONCE_ASM_REWRITE_TAC[] THEN SIMP_TAC[REAL_ABS_MUL] THEN \r
 282 \r
 283 MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS] THEN CONJ_TAC THENL[\r
 284 SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b  `] THEN \r
 285 MATCH_MP_TAC REAL_LE_MUL2 THEN \r
 286 SIMP_TAC[REAL_ABS_POS]\r
 287 THEN CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN \r
 288  CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN \r
 289 SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b  `] THEN \r
 290 MATCH_MP_TAC REAL_LE_MUL2  THEN \r
 291 SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] THEN \r
 292 \r
 293 SIMP_TAC[SIN_BOUND] THEN  SIMP_TAC[REAL_LE_LT]; ALL_TAC] THEN \r
 294 \r
 295 \r
 296 SIMP_TAC[ MAT2X2_VECTOR_MUL; MAT2X2_SCALAR_MUL;VECTOR_2] \r
 297  THEN MATCH_MP_TAC REAL_LE_TRANS THEN \r
 298  EXISTS_TAC(` abs\r
 299      ((&1 / sin (acs ((A + D) / &2)) * C * sin (&n * (acs ((A + D) / &2)))) * xi) +\r
 300       abs((&1 / sin (acs ((A + D) / &2)) * (D * sin (&n * (acs ((A + D) / &2))) - sin ((&n - &1) * (acs ((A + D) / &2))))) *\r
 301       thetai) `) THEN SIMP_TAC[REAL_ABS_TRIANGLE] THEN \r
 302 MATCH_MP_TAC REAL_LE_ADD2 THEN \r
 303 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 \r
 304 THENL[REAL_ARITH_TAC;ALL_TAC] THEN ONCE_ASM_REWRITE_TAC[] THEN \r
 305 SIMP_TAC[REAL_ABS_MUL] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN \r
 306 SIMP_TAC[REAL_ABS_POS;SIN_BOUND;REAL_ABS_1] THEN \r
 307 CONJ_TAC THENL[\r
 308 SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN \r
 309 MATCH_MP_TAC REAL_LE_MUL2 THEN \r
 310 SIMP_TAC[REAL_ABS_POS] THEN CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC]\r
 311 THEN CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC]\r
 312 THEN SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b  `] THEN \r
 313 MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] \r
 314 THEN SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN \r
 315 \r
 316 SIMP_TAC[REAL_SUB_LDISTRIB;REAL_SUB_RDISTRIB] THEN \r
 317 SUBGOAL_THEN `abs\r
 318  ((&1 / sin (acs ((A + D) / &2)) * D * sin (&n * (acs ((A + D) / &2)))) * thetai -\r
 319   (&1 / sin (acs ((A + D) / &2)) * sin (&n * (acs ((A + D) / &2)) - &1 * (acs ((A + D) / &2)))) * thetai)  = \r
 320 abs\r
 321  ((&1 / sin (acs ((A + D) / &2)) * D * thetai )*sin (&n * (acs ((A + D) / &2))) -\r
 322   (&1 / sin (acs ((A + D) / &2)) * thetai) * sin (&n * (acs ((A + D) / &2)) - &1 * (acs ((A + D) / &2))))  ` ASSUME_TAC THENL[\r
 323 REAL_ARITH_TAC;ALL_TAC] THEN ONCE_ASM_REWRITE_TAC[] THEN \r
 324 SIMP_TAC[REAL_FIELD `!(a:real) b. (b - a)= (--a + b)`] THEN \r
 325 MATCH_MP_TAC REAL_LE_TRANS THEN \r
 326 EXISTS_TAC(`  abs\r
 327      (--((&1 / sin (acs ((A + D) / &2)) * thetai) * sin (--(&1 * (acs ((A + D) / &2))) + &n * (acs ((A + D) / &2))))) +\r
 328      abs( (&1 / sin (acs ((A + D) / &2)) * D * thetai) * sin (&n * (acs ((A + D) / &2)))) `)\r
 329 THEN SIMP_TAC[REAL_ABS_TRIANGLE] THEN SIMP_TAC[REAL_ABS_NEG;REAL_ABS_MUL]\r
 330 THEN MATCH_MP_TAC REAL_LE_ADD2 THEN \r
 331 CONJ_TAC THENL[MATCH_MP_TAC REAL_LE_MUL2 THEN \r
 332 SIMP_TAC[REAL_ABS_POS;REAL_ABS_1;SIN_BOUND] THEN \r
 333 CONJ_TAC THENL[ SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b  `] THEN\r
 334 MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] THEN\r
 335 SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN \r
 336 MATCH_MP_TAC REAL_LE_MUL2 THEN \r
 337 SIMP_TAC[REAL_ABS_POS;REAL_ABS_1;SIN_BOUND] THEN \r
 338 CONJ_TAC THENL[SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b`] THEN \r
 339 MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS] THEN\r
 340 CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN \r
 341 CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN \r
 342 SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b  `] THEN \r
 343 MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] THEN\r
 344 SIMP_TAC[REAL_LE_LT]);;\r
 345 \r
 346 \r
 347 let STABILITY_LEMMA_GENERAL = prove(`! (M:real^2^2) xi thetai. det (M) = &1 /\\r
 348            -- &1 < (M$1$1 + M$2$2) / &2 /\ (M$1$1 + M$2$2) / &2 < &1 ==>\r
 349  ?(Y:real^2). !n. abs ((M pow n ** vector [xi; thetai])$1) <= Y$1 /\\r
 350              abs ((M pow n ** vector [xi; thetai])$2) <= Y$2`,\r
 351  REWRITE_TAC[FORALL_MATRIX_2X2] THEN REPEAT STRIP_TAC THEN \r
 352 MATCH_MP_TAC  STABILITY_LEMMA THEN REPEAT(POP_ASSUM MP_TAC) THEN \r
 353 SIMP_TAC [mat2x2;CART_EQ;VECTOR_2;DIMINDEX_2;FORALL_2;DOT_2;SUM_2]);;\r
 354 \r
 355 \r
 356 let STABILITY_THEOREM = prove (`\r
 357    !res. is_valid_resonator res /\\r
 358         (!n. let M = system_composition (unfold_resonator res 1) in\r
 359         (det M = &1) /\ -- &1 < (M$1$1 + M$2$2) / &2 /\ (M$1$1 + M$2$2) / &2 < &1)\r
 360           ==> is_stable_resonator res`,\r
 361 \r
 362 GEN_TAC THEN REPEAT (LET_TAC) THEN REPEAT STRIP_TAC THEN \r
 363 REPEAT STRIP_TAC THEN REWRITE_TAC[is_stable_resonator] THEN GEN_TAC THEN \r
 364 SUBGOAL_THEN ` (?Y:real^2. !n. abs ((M pow n ** vector [FST(fst_single_ray r);SND(fst_single_ray r) ])$1) \r
 365 <= Y$1 /\ abs (((M:real^2^2) pow n ** vector [FST(fst_single_ray r);SND(fst_single_ray r) ])$2) <= Y$2)`\r
 366 ASSUME_TAC THENL[MP_REWRITE_TAC STABILITY_LEMMA_GENERAL THEN ASM_SIMP_TAC[];ALL_TAC] THEN \r
 367 POP_ASSUM MP_TAC THEN STRIP_TAC THEN \r
 368 EXISTS_TAC(`((Y:real^2)$1):real`) THEN EXISTS_TAC(`((Y:real^2)$2):real`) THEN \r
 369 REPEAT STRIP_TAC THEN LET_TAC THEN \r
 370 SUBGOAL_THEN `(let (xi,thetai),(y1,theta1),rs = r in\r
 371               let y',theta' = last_single_ray r in\r
 372               vector [y'; theta'] =\r
 373               system_composition ((unfold_resonator res n):optical_system) **\r
 374               vector [xi; thetai])` ASSUME_TAC THENL[MATCH_MP_TAC SYSTEM_MATRIX THEN \r
 375 ASM_SIMP_TAC[ VALID_UNFOLD_RESONATOR ]; ALL_TAC] THEN POP_ASSUM MP_TAC THEN \r
 376 ONCE_REWRITE_TAC[ MAT2X2_VECTOR_MUL_ALT] THEN ONCE_REWRITE_TAC[RESONATOR_MATRIX] THEN \r
 377 ONCE_ASM_REWRITE_TAC[] THEN LET_TAC THEN LET_TAC THEN \r
 378 DISCH_TAC THEN ONCE_ASM_REWRITE_TAC[] THEN REPEAT(POP_ASSUM MP_TAC) THEN \r
 379 REWRITE_TAC[fst_single_ray;FST;SND] THEN SIMP_TAC[]);;\r
 380 \r
 381 (*-----------------Stability theorem for the symmetric resonators ------------------*)\r
 382 \r
 383 \r
 384 let STABILITY_LEMMA_SYM = prove (` ! A B C D xi thetai. det (mat2x2 A B C D) = &1 /\\r
 385            -- &1 < (A + D) / &2 /\ (A + D) / &2 < &1 ==>\r
 386      ?(Y:real^2). !n. abs (((mat2x2 A B C D pow 2)pow n ** vector [xi; thetai])$1) <= Y$1 /\\r
 387              abs (((mat2x2 A B C D pow 2) pow n ** vector [xi; thetai])$2) <= Y$2`,\r
 388 \r
 389 REWRITE_TAC[MAT2X2_POW2_POW] THEN \r
 390 REPEAT STRIP_TAC THEN \r
 391 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)) \r
 392  + (abs (&1 / sin (acs ((A + D) / &2))) * abs B * abs thetai)* (&1) ;\r
 393 (abs (&1 / sin (acs ((A + D) / &2))) * abs C * abs xi)* abs(&1) + \r
 394 ((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 \r
 395 GEN_TAC THEN  SUBGOAL_THEN `!N. mat2x2 A B C D pow (2*N) =\r
 396              &1 / sin (acs ((A + D) / &2)) %%\r
 397              mat2x2 (A * sin (&(2*N) * (acs ((A + D) / &2))) - sin ((&(2*N) - &1) * (acs ((A + D) / &2))))\r
 398              (B * sin (&(2*N) * (acs ((A + D) / &2))))\r
 399              (C * sin (&(2*N) * (acs ((A + D) / &2))))\r
 400              (D * sin (&(2*N) * (acs ((A + D) / &2))) - sin ((&(2*N) - &1) * (acs ((A + D) / &2)))) ` ASSUME_TAC\r
 401 THENL[GEN_TAC THEN MATCH_MP_TAC SYLVESTER_THEOREM_ALT THEN \r
 402 ASM_SIMP_TAC[];ALL_TAC] THEN \r
 403 ONCE_ASM_REWRITE_TAC[] THEN CONJ_TAC \r
 404 THENL[SIMP_TAC[ MAT2X2_VECTOR_MUL; MAT2X2_SCALAR_MUL;VECTOR_2] THEN\r
 405 MATCH_MP_TAC REAL_LE_TRANS THEN  EXISTS_TAC(` abs\r
 406      ((&1 / sin (acs ((A + D) / &2)) * (A * sin (&(2*n) * (acs ((A + D) / &2))) - sin ((&(2*n) - &1) * (acs ((A + D) / &2))))) *\r
 407       xi) +\r
 408       abs((&1 / sin (acs ((A + D) / &2)) * B * sin (&(2*n) * (acs ((A + D) / &2)))) * thetai)`) THEN \r
 409 SIMP_TAC[REAL_ABS_TRIANGLE] THEN MATCH_MP_TAC REAL_LE_ADD2 THEN \r
 410 CONJ_TAC THENL[\r
 411 SIMP_TAC[REAL_SUB_LDISTRIB;REAL_SUB_RDISTRIB] THEN \r
 412 SUBGOAL_THEN ` abs\r
 413  ((&1 / sin (acs ((A + D) / &2)) * A * sin (&(2*n) * (acs ((A + D) / &2)))) * xi -\r
 414   (&1 / sin (acs ((A + D) / &2)) * sin (&(2*n) * (acs ((A + D) / &2)) - &1 * (acs ((A + D) / &2)))) * xi) = \r
 415 abs\r
 416  ((&1 / sin (acs ((A + D) / &2)) * A * xi) * sin (&(2*n) * (acs ((A + D) / &2))) -\r
 417   (((&1 / sin (acs ((A + D) / &2))) *xi)* sin (&(2*n) * (acs ((A + D) / &2)) - &1 * (acs ((A + D) / &2)))))` ASSUME_TAC THENL[\r
 418 REAL_ARITH_TAC; ALL_TAC] THEN \r
 419 ONCE_ASM_REWRITE_TAC[] THEN\r
 420 SIMP_TAC[REAL_FIELD `!(a:real) b. (b - a)= (--a + b)`] THEN \r
 421 MATCH_MP_TAC REAL_LE_TRANS THEN \r
 422 EXISTS_TAC(` abs\r
 423      (--((&1 / sin (acs ((A + D) / &2)) * xi) * sin (--(&1 * (acs ((A + D) / &2))) + &(2*n) * (acs ((A + D) / &2))))) +\r
 424      abs( (&1 / sin (acs ((A + D) / &2)) * A * xi) * sin (&(2*n) * (acs ((A + D) / &2)))) `) THEN \r
 425 SIMP_TAC[REAL_ABS_TRIANGLE] THEN \r
 426 SIMP_TAC[REAL_ABS_NEG;REAL_ABS_MUL] THEN \r
 427 MATCH_MP_TAC REAL_LE_ADD2 THEN \r
 428 \r
 429 CONJ_TAC THENL[\r
 430 MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS] THEN\r
 431 \r
 432 CONJ_TAC THENL[\r
 433 SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b  `] THEN\r
 434 MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] THEN\r
 435 \r
 436 SIMP_TAC[REAL_LE_LT;SIN_BOUND];ALL_TAC] THEN \r
 437 \r
 438 MATCH_MP_TAC REAL_LE_MUL2 THEN \r
 439 CONJ_TAC THENL[\r
 440 \r
 441 SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b  `] THEN \r
 442 MATCH_MP_TAC REAL_LE_MUL2 THEN \r
 443 SIMP_TAC[REAL_ABS_POS] THEN \r
 444 \r
 445 CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT]; ALL_TAC] THEN\r
 446 CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT]; ALL_TAC] THEN \r
 447 \r
 448 SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b  `] THEN \r
 449 MATCH_MP_TAC REAL_LE_MUL2 THEN \r
 450 SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] THEN \r
 451 \r
 452 SIMP_TAC[REAL_ABS_POS;REAL_ABS_1;SIN_BOUND] THEN \r
 453 SIMP_TAC[REAL_LE_LT]; ALL_TAC] THEN \r
 454 \r
 455 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 \r
 456 THENL [REAL_ARITH_TAC;ALL_TAC] THEN \r
 457 ONCE_ASM_REWRITE_TAC[] THEN SIMP_TAC[REAL_ABS_MUL] THEN \r
 458 \r
 459 MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS] THEN CONJ_TAC THENL[\r
 460 SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b  `] THEN \r
 461 MATCH_MP_TAC REAL_LE_MUL2 THEN \r
 462 SIMP_TAC[REAL_ABS_POS]\r
 463 THEN CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN \r
 464  CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN \r
 465 SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b  `] THEN \r
 466 MATCH_MP_TAC REAL_LE_MUL2  THEN \r
 467 SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] THEN \r
 468 \r
 469 SIMP_TAC[SIN_BOUND] THEN  SIMP_TAC[REAL_LE_LT]; ALL_TAC] THEN \r
 470 \r
 471 \r
 472 SIMP_TAC[ MAT2X2_VECTOR_MUL; MAT2X2_SCALAR_MUL;VECTOR_2] \r
 473  THEN MATCH_MP_TAC REAL_LE_TRANS THEN \r
 474  EXISTS_TAC(` abs\r
 475      ((&1 / sin (acs ((A + D) / &2)) * C * sin (&(2*n) * (acs ((A + D) / &2)))) * xi) +\r
 476       abs((&1 / sin (acs ((A + D) / &2)) * (D * sin (&(2*n) * (acs ((A + D) / &2))) - sin ((&(2*n) - &1) * (acs ((A + D) / &2))))) *\r
 477       thetai) `) THEN SIMP_TAC[REAL_ABS_TRIANGLE] THEN \r
 478 MATCH_MP_TAC REAL_LE_ADD2 THEN \r
 479 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 \r
 480 THENL[REAL_ARITH_TAC;ALL_TAC] THEN ONCE_ASM_REWRITE_TAC[] THEN \r
 481 SIMP_TAC[REAL_ABS_MUL] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN \r
 482 SIMP_TAC[REAL_ABS_POS;SIN_BOUND;REAL_ABS_1] THEN \r
 483 CONJ_TAC THENL[\r
 484 SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN \r
 485 MATCH_MP_TAC REAL_LE_MUL2 THEN \r
 486 SIMP_TAC[REAL_ABS_POS] THEN CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC]\r
 487 THEN CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC]\r
 488 THEN SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b  `] THEN \r
 489 MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] \r
 490 THEN SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN \r
 491 \r
 492 SIMP_TAC[REAL_SUB_LDISTRIB;REAL_SUB_RDISTRIB] THEN \r
 493 SUBGOAL_THEN `abs\r
 494  ((&1 / sin (acs ((A + D) / &2)) * D * sin (&(2*n) * (acs ((A + D) / &2)))) * thetai -\r
 495   (&1 / sin (acs ((A + D) / &2)) * sin (&(2*n) * (acs ((A + D) / &2)) - &1 * (acs ((A + D) / &2)))) * thetai)  = \r
 496 abs\r
 497  ((&1 / sin (acs ((A + D) / &2)) * D * thetai )*sin (&(2*n) * (acs ((A + D) / &2))) -\r
 498   (&1 / sin (acs ((A + D) / &2)) * thetai) * sin (&(2*n) * (acs ((A + D) / &2)) - &1 * (acs ((A + D) / &2))))  ` ASSUME_TAC THENL[\r
 499 REAL_ARITH_TAC;ALL_TAC] THEN ONCE_ASM_REWRITE_TAC[] THEN \r
 500 SIMP_TAC[REAL_FIELD `!(a:real) b. (b - a)= (--a + b)`] THEN \r
 501 MATCH_MP_TAC REAL_LE_TRANS THEN \r
 502 EXISTS_TAC(`  abs\r
 503      (--((&1 / sin (acs ((A + D) / &2)) * thetai) * sin (--(&1 * (acs ((A + D) / &2))) + &(2*n) * (acs ((A + D) / &2))))) +\r
 504      abs( (&1 / sin (acs ((A + D) / &2)) * D * thetai) * sin (&(2*n) * (acs ((A + D) / &2)))) `)\r
 505 THEN SIMP_TAC[REAL_ABS_TRIANGLE] THEN SIMP_TAC[REAL_ABS_NEG;REAL_ABS_MUL]\r
 506 THEN MATCH_MP_TAC REAL_LE_ADD2 THEN \r
 507 CONJ_TAC THENL[MATCH_MP_TAC REAL_LE_MUL2 THEN \r
 508 SIMP_TAC[REAL_ABS_POS;REAL_ABS_1;SIN_BOUND] THEN \r
 509 CONJ_TAC THENL[ SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b  `] THEN\r
 510 MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] THEN\r
 511 SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN \r
 512 MATCH_MP_TAC REAL_LE_MUL2 THEN \r
 513 SIMP_TAC[REAL_ABS_POS;REAL_ABS_1;SIN_BOUND] THEN \r
 514 CONJ_TAC THENL[SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b`] THEN \r
 515 MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS] THEN\r
 516 CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN \r
 517 CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN \r
 518 SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b  `] THEN \r
 519 MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] THEN\r
 520 SIMP_TAC[REAL_LE_LT]);;\r
 521 \r
 522 let STABILITY_LEMMA_GENERAL_SYM = prove(`! (M:real^2^2) xi thetai. det (M) = &1 /\\r
 523            -- &1 < (M$1$1 + M$2$2) / &2 /\ (M$1$1 + M$2$2) / &2 < &1 ==>\r
 524  ?(Y:real^2). !n. abs (((M pow 2) pow n ** vector [xi; thetai])$1) <= Y$1 /\\r
 525              abs (((M pow 2)  pow n ** vector [xi; thetai])$2) <= Y$2`,\r
 526  REWRITE_TAC[FORALL_MATRIX_2X2] THEN REPEAT STRIP_TAC THEN \r
 527 MATCH_MP_TAC  STABILITY_LEMMA_SYM THEN REPEAT(POP_ASSUM MP_TAC) THEN \r
 528 SIMP_TAC [mat2x2;CART_EQ;VECTOR_2;DIMINDEX_2;FORALL_2;DOT_2;SUM_2]);;\r
 529 \r
 530 let STABILITY_THEOREM_SYM = prove (\r
 531   `!res. is_valid_resonator res /\\r
 532         ((M:real^2^2) pow 2 = system_composition (unfold_resonator res 1)) /\\r
 533         (det (M:real^2^2) = &1) /\ -- &1 < (M$1$1 + M$2$2) / &2 /\ (M$1$1 + M$2$2) / &2 < &1\r
 534           ==> is_stable_resonator res`,\r
 535 \r
 536 GEN_TAC THEN ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN \r
 537 POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN \r
 538 REPEAT STRIP_TAC THEN REWRITE_TAC[is_stable_resonator] THEN \r
 539 GEN_TAC THEN \r
 540 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 /\\r
 541                       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[ \r
 542 MP_REWRITE_TAC STABILITY_LEMMA_GENERAL_SYM THEN ASM_SIMP_TAC[]; ALL_TAC] THEN \r
 543 POP_ASSUM MP_TAC THEN STRIP_TAC THEN EXISTS_TAC(`((Y:real^2)$1):real`) THEN \r
 544 EXISTS_TAC(`((Y:real^2)$2):real`) THEN REPEAT STRIP_TAC THEN \r
 545 LET_TAC THEN SUBGOAL_THEN `(let (xi,thetai),(y1,theta1),rs = r in\r
 546               let y',theta' = last_single_ray r in\r
 547               vector [y'; theta'] =\r
 548               system_composition ((unfold_resonator res n):optical_system) **\r
 549               vector [xi; thetai])` ASSUME_TAC THENL[ \r
 550 MATCH_MP_TAC SYSTEM_MATRIX THEN ASM_SIMP_TAC[ VALID_UNFOLD_RESONATOR];ALL_TAC] THEN \r
 551 POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[MAT2X2_VECTOR_MUL_ALT] THEN \r
 552 ONCE_REWRITE_TAC[RESONATOR_MATRIX] THEN ONCE_ASM_REWRITE_TAC[] THEN LET_TAC THEN \r
 553 LET_TAC THEN DISCH_TAC THEN ONCE_ASM_REWRITE_TAC[] THEN REPEAT(POP_ASSUM MP_TAC) THEN \r
 554 REWRITE_TAC[fst_single_ray;FST;SND] THEN SIMP_TAC[]);;\r
 555 \r
 556  \r