(* ========================================================================= *)
(*                                                                           *)
(*                        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`,
(*------------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))`]);;