z_resonator.ml

   1 (* ========================================================================= *)
   2 (*                                                                           *)
   3 (*                        Z-Shaped Resonator                                 *)
   4 (*                                                                           *)
   5 (*        (c) Copyright, Muhammad Umair Siddique, Vincent Aravantinos, 2012  *)
   6 (*                       Hardware Verification Group,                        *)
   7 (*                       Concordia University                                *)
   8 (*                                                                           *)
   9 (*     Contact: <muh_sidd@ece.concordia.ca>, <vincent@ece.concordia.ca>      *)
  10 (*                                                                           *)
  11 (* Last update: Feb 16, 2012                                                 *)
  12 (*                                                                           *)
  13 (* ========================================================================= *)
  14
  15
  16
  17 needs "geometrical_optics.ml";;
  18 needs "resonator.ml";;
  19
  20
  21
  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],
  26        (n,d1),(plane))`;;
  27
  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))
  32           (&4*(d2-R) /(R * R))
  33           ((R * R - &4 * d1 * R - &2 * d2 * R + &4 * d1 * d2)/ (R * R))  `;;
  34
  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);;
  39
  40
  41 let Z_CAVITY_STABILITY_LEMMA = prove (
  42 `!R n d1 d2.
  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`,
  46
  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);;
  53
  54
  55 (*------------Stability_Analysis-------------*)
  56
  57
  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)`,
  60
  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
  74
  75 CONJ_TAC THENL[
  76
  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  `];
  89 ALL_TAC] THEN
  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 `];
 107 ALL_TAC] THEN
 108
 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  `];
 118 ALL_TAC] THEN
 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))`]);;
 123
 124