(* ========================================================================= *)
(*                                                                           *)
(*                        Fabry Perot Resonator                              *)
(*                                                                           *)
(*        (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";;
needs "resonator.ml";;

let VALID_RESONATOR_TAC x =
  SIMP_TAC[x;is_valid_resonator;is_valid_optical_component;ALL;
    is_valid_free_space;is_valid_interface]
  THEN CONV_TAC REAL_FIELD;;


let fp_mat_half = new_definition 
  `fp_mat_half R d = mat2x2 (&1)  (d) (--(&2/R)) (&1 - (&2*d)/R) `;;
let fp_cavity = new_definition
  `fp_cavity R d n :resonator =
    ((spherical R),[],(n,d),(spherical R)) `;;

let VALID_FP_CAVITY = 
prove
  (`!R d n.
    ~(R= &0) /\ &0 < d /\ &0 < n  ==>
    is_valid_resonator (fp_cavity R d n)`,

    VALID_RESONATOR_TAC fp_cavity);;

let TRACE_FP = 
prove 
(`!R d.  ~(R= &0) /\ &0 < d ==> trace (fp_mat_half R d) = &2 - &2*d/R`,

SIMP_TAC[TRACE_MAT2X2;fp_mat_half] THEN  CONV_TAC REAL_FIELD);;
                 
let STABLE_FP = 
prove
(`!R d n.  ~(R= &0) /\ &0 < d/R /\ d/R < &2 /\  &0 < n /\ &0 < d   ==> 
                              is_stable_resonator (fp_cavity R d n)`,

REPEAT STRIP_TAC THEN MP_REWRITE_TAC STABILITY_THEOREM_SYM THEN 
EXISTS_TAC(`(fp_mat_half R d):real^2^2`) THEN 
REWRITE_TAC[MAT_POW2;fp_mat_half] THEN CONJ_TAC THENL[
ASM_SIMP_TAC[VALID_FP_CAVITY ];ALL_TAC] THEN CONJ_TAC THENL[
REWRITE_TAC[system_composition;unfold_resonator;LIST_POW;ONE;fp_cavity;
round_trip;APPEND;optical_components_shift;LET_DEF;LET_END_DEF;REVERSE;
interface_matrix;head_index;free_space_matrix] THEN
REPEAT(POP_ASSUM MP_TAC) THEN REWRITE_TAC[GSYM ONE] 
THEN SIMP_TAC[GSYM MATRIX_MUL_ASSOC] 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 CONV_TAC REAL_FIELD; ALL_TAC] THEN 
REPEAT(POP_ASSUM MP_TAC) THEN 
REWRITE_TAC[DET_MAT2X2] THEN REWRITE_TAC[mat2x2;VECTOR_2] THEN
CONV_TAC REAL_FIELD);;