(* ========================================================================= *)
(* *)
(* Optical Resoantors *)
(* *)
(* (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";;
(* ------------------------------------------------------------------------- *)
(* Resonators Formalization *)
(* ------------------------------------------------------------------------- *)
new_type_abbrev("resonator",
`:interface # optical_component list # free_space # interface`);;
let FORALL_RESONATOR_THM = prove
(`!P. (!res:resonator. P res) <=> !i1 cs fs i2. P (i1,cs,fs,i2)`,
(* Shifts the free spaces in a list of optical components from right to left.
* Takes an additional free space parameter to insert in place of the ``hole''
* remainining on the right.
* Returns an additional free space corresponding to the leftmost free space
* that is ``thrown away'' by the shifting.
*)
let optical_components_shift = define
`optical_components_shift [] fs' = [], fs' /\
optical_components_shift (CONS (fs,i) cs) fs' =
let cs',fs'' = optical_components_shift cs fs' in
CONS (fs'',i) cs', fs`;;
let OPTICAL_COMPONENTS_SHIFT_THROWN_IN = prove
(`!cs:optical_component list fs.
let cs',fs'' = optical_components_shift cs fs in
cs = [] \/ ?i cs''. cs = CONS (fs'',i) cs''`,
let VALID_OPTICAL_COMPONENTS_SHIFT = prove
(`!cs:optical_component list fs.
ALL is_valid_optical_component cs /\ is_valid_free_space fs ==>
let cs',fs' = optical_components_shift cs fs in
ALL is_valid_optical_component cs' /\ is_valid_free_space fs'`,
let round_trip = new_definition
`round_trip ((i1,cs,fs,i2) : resonator) =
APPEND cs (CONS (fs,i2,reflected) (
let cs',fs1 = optical_components_shift cs fs in
REVERSE (CONS (fs1,i1,reflected) cs')))`;;
let ROUND_TRIP_NIL = prove
(`!i1 fs i2. round_trip (i1,[],fs,i2) = [fs,i2,reflected;fs,i1,reflected]`,
let SYSTEM_COMPOSITION_APPEND = prove
(`!cs1 cs2 fs.
system_composition (APPEND cs1 cs2,fs)
= system_composition (cs2,fs)
** system_composition (cs1,head_index (cs2,fs),&0)`,
let is_valid_resonator = new_definition
`is_valid_resonator ((i1,cs,fs,i2):resonator) <=>
is_valid_interface i1 /\ ALL is_valid_optical_component cs /\
is_valid_free_space fs /\ is_valid_interface i2`;;
(*------- Generates a resonator unfolded n times ------- *)
let unfold_resonator = define
`unfold_resonator (i1,cs,fs,i2) n =
LIST_POW (round_trip (i1,cs,fs,i2)) n, (head_index (cs,fs),&0)`;;
let RESONATOR_MATRIX = prove
(`!n res.
system_composition (unfold_resonator res n)
= system_composition (unfold_resonator res 1) pow n`,
(* ------------------------------------------------------------------------- *)
(* Stability analysis *)
(* ------------------------------------------------------------------------- *)
let is_stable_resonator = new_definition
`is_stable_resonator (res:resonator) <=>
!r. ?y theta.
!n. is_valid_ray_in_system r (unfold_resonator res n) ==>
let y',theta' = last_single_ray r in
abs y' <= y /\ abs theta' <= theta`;;
let REAL_REDUCE_TAC = CONV_TAC (DEPTH_CONV (CHANGED_CONV REAL_POLY_CONV));;
let SYLVESTER_THEOREM = prove
(`!A B C D .
det (mat2x2 A B C D) = &1 /\ -- &1 < (A + D) / &2 /\ (A + D) / &2 < &1 ==>
let theta = acs ((A + D) / &2) in
!N.
(mat2x2 A B C D) pow N =
(&1 / sin theta) %% (mat2x2
(A * sin (&N * theta) - sin((&N - &1) * theta))
(B * sin (&N * theta)) (C * sin (&N * theta))
(D * sin (&N*theta) - sin ((&N - &1)* theta)))`,
let SYLVESTER_THEOREM_ALT = prove (` ! (N:num) (A:real) B C D . theta = acs((A + D)/ &2) /\
(det (mat2x2 A B C D) = &1) /\ -- &1 <((A + D)/ &2) /\
((A + D)/ &2) < &1 ==> ((mat2x2 A B C D) pow N =
(&1/sin(theta)) %% (mat2x2 (A*sin(&N*theta)-
sin((&N - (&1))* theta)) (B*sin(&N*theta))
(C*sin(&N*theta)) (D*sin(&N*theta)- sin((&N - (&1))* theta)))) `,
let STABILITY_THEOREM = prove (`
!res. is_valid_resonator res /\
(!n. let M = system_composition (unfold_resonator res 1) in
(det M = &1) /\ -- &1 < (M$1$1 + M$2$2) / &2 /\ (M$1$1 + M$2$2) / &2 < &1)
==> is_stable_resonator res`,
theta'] =
system_composition ((unfold_resonator res n):optical_system) **
vector [xi; thetai])` ASSUME_TAC THENL[MATCH_MP_TAC SYSTEM_MATRIX THEN
ASM_SIMP_TAC[ VALID_UNFOLD_RESONATOR ]; ALL_TAC] THEN POP_ASSUM MP_TAC THEN
ONCE_REWRITE_TAC[ MAT2X2_VECTOR_MUL_ALT] THEN ONCE_REWRITE_TAC[RESONATOR_MATRIX] THEN
ONCE_ASM_REWRITE_TAC[] THEN LET_TAC THEN LET_TAC THEN
DISCH_TAC THEN ONCE_ASM_REWRITE_TAC[] THEN REPEAT(POP_ASSUM MP_TAC) THEN
REWRITE_TAC[fst_single_ray;FST;SND] THEN SIMP_TAC[]);;
(*-----------------Stability theorem for the symmetric resonators ------------------*)
let STABILITY_THEOREM_SYM = prove (
`!res. is_valid_resonator res /\
((M:real^2^2) pow 2 = system_composition (unfold_resonator res 1)) /\
(det (M:real^2^2) = &1) /\ -- &1 < (M$1$1 + M$2$2) / &2 /\ (M$1$1 + M$2$2) / &2 < &1
==> is_stable_resonator res`,
theta'] =
system_composition ((unfold_resonator res n):optical_system) **
vector [xi; thetai])` ASSUME_TAC THENL[
MATCH_MP_TAC SYSTEM_MATRIX THEN ASM_SIMP_TAC[ VALID_UNFOLD_RESONATOR];ALL_TAC] THEN
POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[MAT2X2_VECTOR_MUL_ALT] THEN
ONCE_REWRITE_TAC[RESONATOR_MATRIX] THEN ONCE_ASM_REWRITE_TAC[] THEN LET_TAC THEN
LET_TAC THEN DISCH_TAC THEN ONCE_ASM_REWRITE_TAC[] THEN REPEAT(POP_ASSUM MP_TAC) THEN
REWRITE_TAC[fst_single_ray;FST;SND] THEN SIMP_TAC[]);;