(* ========================================================================= *)
(*                                                                           *)
(*                        Z-Shaped 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";;



(*--------------------------Z Cavity Modeling----------------------------*)
let z_cavity = new_definition
  `z_cavity R d1 d2 n: resonator = 
       ((plane), [(n,d1),(spherical R),reflected;(n,d2),(spherical R),reflected],
       (n,d1),(plane))`;;
let z_cavity_mat_half = new_definition 
   `z_cavity_mat_half  R (n:real) d1 d2 = 
   mat2x2 ((R * R - &4 * d1 * R - &2 * d2 * R + &4 * d1 * d2)/ (R * R))   
          ((&4*d2*d1*d1 - &4*R*d1*d1 + &2*R*R*d1 - &4*d2*R*d1 + d2*R*R)/(R*R))  
          (&4*(d2-R) /(R * R))
          ((R * R - &4 * d1 * R - &2 * d2 * R + &4 * d1 * d2)/ (R * R))  `;;
let VALID_Z_CAVITY = 
prove
  (`!R n. ~(R= &0) /\  &0 < n /\ &0 <= d1 /\ &0 <= d2  ==>
      is_valid_resonator (z_cavity R d1 d2 n)`,

  VALID_RESONATOR_TAC z_cavity);;

let Z_CAVITY_STABILITY_LEMMA = 
prove (
`!R n d1 d2.
     ~(R= &0) /\  &0 < n /\ &0 <= d1 /\ &0 <= d2 ==> 
system_composition (unfold_resonator  (z_cavity R d1 d2 n) 1) = 
(z_cavity_mat_half  R (n:real) d1 d2) pow 2`,


REWRITE_TAC[MAT_POW2;z_cavity_mat_half;unfold_resonator; system_composition;
z_cavity;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 SIMP_TAC[GSYM ONE; 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);;

(*------------Stability_Analysis-------------*)


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 /\ 
     (&2*d1*d2)/ (&2*d1 + d2) < R   ==> is_stable_resonator (z_cavity R d1 d2 n)`,


REPEAT STRIP_TAC THEN MP_REWRITE_TAC STABILITY_THEOREM_SYM THEN 
EXISTS_TAC(`(z_cavity_mat_half R n d1 d2):real^2^2`) THEN 
CONJ_TAC THENL[MP_REWRITE_TAC VALID_Z_CAVITY THEN 
ASM_SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN 
CONJ_TAC THENL[MP_REWRITE_TAC Z_CAVITY_STABILITY_LEMMA THEN 
ASM_SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN 
REWRITE_TAC[z_cavity_mat_half;DET_MAT2X2] THEN 
REWRITE_TAC[mat2x2;VECTOR_2] THEN 
CONJ_TAC THENL[ REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC REAL_FIELD;ALL_TAC]
 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) =
 (a/(R*R) - b/(R*R) -  c/(R*R) + d/(R*R))`;
  REAL_FIELD ` !a. ~(a = &0)==> (a*a)/(a*a) = &1 `; 
  REAL_FIELD `! a b z. ~(z = &0) ==> (a*b*z)/(z*z) = (a*b)/z `] THEN 

CONJ_TAC THENL[

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 
ASM_SIMP_TAC[REAL_FIELD `!a b c.  ~(a = &0) ==> b/a + c/a = (b+c)/a `] THEN 
SUBGOAL_THEN `&2 + (&4 * d1 * d2) / (R * R) > (&4 * d1 + &2 * d2) / R <=> 
 &1 + (&2 * d1 * d2) / (R * R) > (&2* d1 + d2) / R` ASSUME_TAC THENL[
REAL_ARITH_TAC;ALL_TAC] THEN ONCE_ASM_REWRITE_TAC[] THEN 
ONCE_SIMP_TAC[REAL_FIELD `! a b. a:real > b <=> b < a`] THEN
ONCE_SIMP_TAC[REAL_FIELD `! a b. (b < a) = (b + &0 < a) `] THEN
MATCH_MP_TAC REAL_LT_ADD2 THEN CONJ_TAC THENL[
SUBGOAL_THEN `&0  < R ` ASSUME_TAC  THENL[MATCH_MP_TAC REAL_LT_TRANS THEN 
EXISTS_TAC(`(&2 * d1 * d2) / (&2 * d1 + d2) `) THEN ASM_SIMP_TAC[] THEN
MATCH_MP_TAC REAL_LT_DIV THEN CONJ_TAC THENL[
MATCH_MP_TAC REAL_LT_MUL THEN  ASM_SIMP_TAC[REAL_LT_MUL;REAL_FIELD `&0 < &2  `];
ALL_TAC] THEN
ASM_SIMP_TAC[REAL_LT_MUL;REAL_FIELD `!a b. &0 < a /\ &0 < b ==> &0 < &2*a + b ` ];
ALL_TAC] THEN  ASM_SIMP_TAC[REAL_LT_LDIV_EQ;REAL_MUL_LID] THEN
MATCH_MP_TAC REAL_LT_TRANS THEN EXISTS_TAC(`(&2 * d1 * d2) / (&2 * d1 + d2) `) THEN
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
SUBGOAL_THEN `(&2 * d1 + d2) * (&2 * d1 + d2) < (&2 * d1) * d2  <=> 
                ((&2 * d1 + d2) * (&2 * d1 + d2)) /(&2 * d1) < d2` ASSUME_TAC THENL[
REWRITE_TAC[EQ_SYM_EQ;REAL_MUL_SYM] THEN MATCH_MP_TAC REAL_LT_LDIV_EQ THEN
ASM_SIMP_TAC[REAL_FIELD `!a . &0 < a  ==> &0 < a* &2` ];ALL_TAC] THEN  
ONCE_ASM_REWRITE_TAC[] THEN  ASM_SIMP_TAC[GSYM REAL_POW_2 ];ALL_TAC] THEN
MATCH_MP_TAC REAL_LT_DIV THEN CONJ_TAC THENL[ MATCH_MP_TAC REAL_LT_MUL THEN 
ASM_SIMP_TAC[REAL_LT_MUL;REAL_FIELD `&0 < &2  `];ALL_TAC] THEN 
ASM_SIMP_TAC[GSYM REAL_POW_2] THEN  MATCH_MP_TAC REAL_POW_LT THEN
MATCH_MP_TAC REAL_LT_TRANS THEN EXISTS_TAC(`(&2 * d1 * d2) / (&2 * d1 + d2) `) THEN 
ASM_SIMP_TAC[] THEN MATCH_MP_TAC REAL_LT_DIV THEN
CONJ_TAC THENL[ MATCH_MP_TAC REAL_LT_MUL THEN 
ASM_SIMP_TAC[REAL_LT_MUL;REAL_FIELD `&0 < &2  `];ALL_TAC]THEN 
ASM_SIMP_TAC[REAL_LT_MUL;REAL_FIELD `!a b. &0 < a /\ &0 < b ==> &0 < &2*a + b `];
ALL_TAC] THEN 

SIMP_TAC[REAL_FIELD ` !a:real b c d. a - b -c + d < a <=> d < b + c `] THEN
ASM_SIMP_TAC[REAL_FIELD `!a b c.  ~(a = &0) ==> b/a + c/a = (b+c)/a `] THEN 
SUBGOAL_THEN `(&4 * d1 * d2) / (R * R) < (&4 * d1 + &2 * d2) / R <=> 
               ((&4 * d1 * d2) / R)/ R < (&4 * d1 + &2 * d2) / R ` ASSUME_TAC THENL[
SIMP_TAC[real_div; GSYM REAL_MUL_ASSOC] THEN SIMP_TAC[GSYM REAL_INV_MUL];ALL_TAC] THEN 
ONCE_ASM_REWRITE_TAC[] THEN SUBGOAL_THEN `&0  < R ` ASSUME_TAC THENL[MATCH_MP_TAC REAL_LT_TRANS THEN 
EXISTS_TAC(`(&2 * d1 * d2) / (&2 * d1 + d2) `) THEN ASM_SIMP_TAC[] THEN
MATCH_MP_TAC REAL_LT_DIV THEN CONJ_TAC THENL[
MATCH_MP_TAC REAL_LT_MUL THEN  ASM_SIMP_TAC[REAL_LT_MUL;REAL_FIELD `&0 < &2  `];
ALL_TAC] THEN
ASM_SIMP_TAC[REAL_LT_MUL;REAL_FIELD `!a b. &0 < a /\ &0 < b ==> &0 < &2*a + b ` ];
ALL_TAC] THEN  ASM_SIMP_TAC[REAL_LT_DIV2_EQ ] THEN ASM_SIMP_TAC[REAL_LT_LDIV_EQ;REAL_MUL_SYM ]
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
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))`]);;