fp_resonator.ml

   1 (* ========================================================================= *)
   2 (*                                                                           *)
   3 (*                        Fabry Perot 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 needs "geometrical_optics.ml";;
  17 needs "resonator.ml";;
  18
  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;;
  23
  24
  25 let fp_mat_half = new_definition
  26   `fp_mat_half R d = mat2x2 (&1)  (d) (--(&2/R)) (&1 - (&2*d)/R) `;;
  27
  28 let fp_cavity = new_definition
  29   `fp_cavity R d n :resonator =
  30     ((spherical R),[],(n,d),(spherical R)) `;;
  31
  32
  33 let VALID_FP_CAVITY = prove
  34   (`!R d n.
  35     ~(R= &0) /\ &0 < d /\ &0 < n  ==>
  36     is_valid_resonator (fp_cavity R d n)`,
  37     VALID_RESONATOR_TAC fp_cavity);;
  38
  39
  40 let TRACE_FP = prove
  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);;
  43
  44 let STABLE_FP =  prove
  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);;
  62