--- /dev/null
+(* ========================================================================= *)
+(* *)
+(* Frequent Component Library *)
+(* *)
+(* (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";;
+
+(*-----THIN LENS------------*)
+
+let thin_lens_mat = new_definition
+ `thin_lens_mat R1 R2 (n1:real) (n2:real) =
+ mat2x2 (&1) (&0) (((n2 - n1)/n1) *(&1/R2 - &1/R1)) (&1) `;;
+
+let thin_lens = new_definition
+ `thin_lens R1 R2 n1 n2: optical_system =
+ ([(n1,&0),(spherical R1),transmitted;
+ (n2,&0),(spherical R2),transmitted],n1,&0)`;;
+
+let VALID_OPTICAL_SYSTEM_TAC x =
+ SIMP_TAC[x;is_valid_optical_system;is_valid_optical_component;ALL;
+ is_valid_free_space;is_valid_interface]
+ THEN CONV_TAC REAL_FIELD;;
+
+let VALID_THIN_LENS = prove
+ (`!R1 R2 n1 n2.
+ ~(R1= &0) /\ ~(R2= &0) /\ &0 < n1 /\ &0 < n2 ==>
+ is_valid_optical_system (thin_lens R1 R2 n1 n2)`,
+ VALID_OPTICAL_SYSTEM_TAC thin_lens);;
+
+let THIN_LENS_THIN_LENS_MAT = prove
+ (`!R1 R2 n1 n2.
+ ~(R1 = &0) /\ ~(R2 = &0) /\ &0 < n1 /\ &0 < n2 ==>
+ system_composition (thin_lens R1 R2 n1 n2) = thin_lens_mat R1 R2 n1 n2`,
+ REWRITE_TAC[system_composition;head_index;interface_matrix;free_space_matrix;
+ thin_lens_mat;thin_lens;MAT2X2_MUL;MAT2X2_EQ]
+ THEN CONV_TAC REAL_FIELD);;
+
+let THIN_LENS_MATRIX = prove
+ (`!R1 R2 n1 n2.
+ ~(R1= &0) /\ ~(R2= &0) /\ &0 < n1 /\ &0 < n2 ==>
+ !ray. is_valid_ray_in_system ray (thin_lens R1 R2 n1 n2) ==>
+ let ((y0,theta0),(y1,theta1),rs) = ray in
+ let (y_n,theta_n) = last_single_ray ray in
+ vector [y_n;theta_n] = thin_lens_mat R1 R2 n1 n2 ** vector [y0;theta0]`,
+ SIMP_TAC[GSYM THIN_LENS_THIN_LENS_MAT] THEN REPEAT STRIP_TAC
+ THEN MATCH_MP_TAC SYSTEM_MATRIX THEN ASM_SIMP_TAC[VALID_THIN_LENS]);;
+
+(*------------------THICK LENS---------------------*)
+let thick_lens_mat = new_definition
+ `thick_lens_mat R1 R2 (n1:real) (n2:real) d =
+ mat2x2 (&1 + d*(n1/(n2*R1) - &1/R1)) (d * n1 / n2)
+ (--(((n1 - n2)*(d*(n1-n2) + n2*(R1-R2)))/(n1*n2*R1*R2)))
+ ( &1 + d*(&1/R2 - n1/(n2*R2))) `;;
+
+let thick_lens = new_definition
+ `thick_lens R1 R2 n1 n2 d: optical_system =
+ ([(n1,&0),(spherical R1),transmitted;
+ (n2,d),(spherical R2),transmitted],n1,&0)`;;
+
+
+let VALID_THICK_LENS = prove
+ (`!R1 R2 n1 n2.
+ ~(R1= &0) /\ ~(R2= &0) /\ &0 < n1 /\ &0 < n2 /\ &0 <= d ==>
+ is_valid_optical_system (thick_lens R1 R2 n1 n2 d)`,
+ VALID_OPTICAL_SYSTEM_TAC thick_lens);;
+
+let THICK_LENS_THICK_LENS_MAT = prove
+ (`!R1 R2 n1 n2 d.
+ ~(R1 = &0) /\ ~(R2 = &0) /\ &0 < n1 /\ &0 < n2 /\ &0 <= d ==>
+ system_composition (thick_lens R1 R2 n1 n2 d) = thick_lens_mat R1 R2 n1 n2 d`,
+ REWRITE_TAC[system_composition;head_index;interface_matrix;free_space_matrix;
+ thick_lens_mat;thick_lens;MAT2X2_MUL;MAT2X2_EQ]
+ THEN CONV_TAC REAL_FIELD);;
+
+let THICK_LENS_MATRIX = prove
+ (`!R1 R2 n1 n2.
+ ~(R1= &0) /\ ~(R2= &0) /\ &0 < n1 /\ &0 < n2 /\ &0 <= d ==>
+ !ray. is_valid_ray_in_system ray (thick_lens R1 R2 n1 n2 d) ==>
+ let ((y0,theta0),(y1,theta1),rs) = ray in
+ let (y_n,theta_n) = last_single_ray ray in
+ vector [y_n;theta_n] = thick_lens_mat R1 R2 n1 n2 d ** vector [y0;theta0]`,
+ SIMP_TAC[GSYM THICK_LENS_THICK_LENS_MAT] THEN REPEAT STRIP_TAC
+ THEN MATCH_MP_TAC SYSTEM_MATRIX THEN ASM_SIMP_TAC[VALID_THICK_LENS]);;
+
+(*-----------DIELECTRIC SLAB---------------*)
+
+let slab_mat = new_definition
+ `slab_mat (n1:real) (n2:real) d =
+ mat2x2 (&1) (d*(n1/n2)) (&0) (&1) `;;
+
+let slab = new_definition
+ `slab n1 n2 d: optical_system =
+ ([(n1,&0),(plane),transmitted;
+ (n2,d),(plane),transmitted],n1,&0)`;;
+
+
+let VALID_SLAB = prove
+ (`!n1 n2 d.
+ &0 < n1 /\ &0 < n2 /\ &0 < d ==>
+ is_valid_optical_system (slab n1 n2 d)`,
+ VALID_OPTICAL_SYSTEM_TAC slab);;
+
+let SLAB_SLAB_MAT = prove
+ (` !n1 n2 d.
+ &0 < n1 /\ &0 < n2 /\ &0 < d ==>
+ system_composition (slab n1 n2 d) = (slab_mat n1 n2 d)`,
+ REWRITE_TAC[system_composition;head_index;interface_matrix;free_space_matrix;
+ slab_mat;slab;MAT2X2_MUL;MAT2X2_EQ]
+ THEN CONV_TAC REAL_FIELD);;
+
+let SLAB_MATRIX = prove
+ (`!n1 n2 d.
+ &0 < n1 /\ &0 < n2 /\ &0 < d ==>
+ !ray. is_valid_ray_in_system ray (slab n1 n2 d) ==>
+ let ((y0,theta0),(y1,theta1),rs) = ray in
+ let (y_n,theta_n) = last_single_ray ray in
+ vector [y_n;theta_n] = slab_mat n1 n2 d ** vector [y0;theta0]`,
+ SIMP_TAC[GSYM SLAB_SLAB_MAT] THEN REPEAT STRIP_TAC
+ THEN MATCH_MP_TAC SYSTEM_MATRIX THEN ASM_SIMP_TAC[VALID_SLAB]);;
+
+
--- /dev/null
+(* ========================================================================= *)
+(* *)
+(* 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);;
+
--- /dev/null
+(* ========================================================================= *)
+(* *)
+(* Geometrical Optics Library *)
+(* *)
+(* (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 "Multivariate/make_complex.ml";;
+needs "utils.ml";;
+(* ------------------------------------------------------------------------- *)
+(* Preliminaries *)
+(* ------------------------------------------------------------------------- *)
+
+let LET_PAIR = prove
+ (`!P t. (let x,y = t in P x y) = P (FST t) (SND t)`,
+ ONCE_REWRITE_TAC[GSYM PAIR] THEN PURE_REWRITE_TAC[LET_DEF;LET_END_DEF;FST;SND]
+ THEN REWRITE_TAC[]);;
+
+let ALL_REVERSE = prove
+ (`!l P. ALL P (REVERSE l) = ALL P l`,
+ LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[REVERSE;ALL;ALL_APPEND] THEN ITAUT_TAC);;
+
+let BOUNDED_VECTOR_COMPONENT = prove
+ (`!v:real^N. (?B:real^N. !i. 1 <= i /\ i <= dimindex(:N) ==> v$i <= B$i)
+ <=> (?b. !i. 1 <= i /\ i <= dimindex(:N) ==> v$i <= b)`,
+ REPEAT (STRIP_TAC ORELSE EQ_TAC) THENL [
+ MESON_TAC[REAL_LE_TRANS;REAL_ABS_LE;COMPONENT_LE_INFNORM];
+ EXISTS_TAC `b % vec 1:real^N`
+ THEN ASM_REWRITE_TAC[VEC_COMPONENT;VECTOR_MUL_COMPONENT;REAL_MUL_RID]
+ ]);;
+
+let BOUNDED_MATRIX_BOUNDED_VECTOR_MUL = prove
+ (`!M:num->real^M^N.
+ (?b. !n i j. 1 <= i /\ i <= dimindex(:N) /\ 1 <= j /\ j <= dimindex(:M)
+ ==> abs ((M n)$i$j) <= b)
+ ==> (!v:real^M.
+ ?b. !n i. 1 <= i /\ i <= dimindex(:N) ==> abs ((M n ** v)$i) <= b)`,
+ REPEAT STRIP_TAC
+ THEN SIMP_TAC[MATRIX_VECTOR_MUL_COMPONENT;dot]
+ THEN Pa.EXISTS_TAC "sum (1..dimindex(:M)) (\i. b * abs (v$i))"
+ THEN REPEAT GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC SUM_ABS_LE
+ THEN REWRITE_TAC[FINITE_NUMSEG;IN_NUMSEG;REAL_ABS_MUL]
+ THEN GEN_TAC THEN Pa.ASM_CASES_TAC "v$x = &0"
+ THEN ASM_REWRITE_TAC[REAL_ABS_0;REAL_MUL_RZERO;REAL_LE_REFL]
+ THEN MP_REWRITE_TAC REAL_LE_RMUL_EQ
+ THEN ASM_MESON_TAC[REAL_LT_LE;REAL_ABS_ZERO;REAL_ABS_POS]);;
+
+
+(* ------------------------------------------------------------------------- *)
+(* System formalization *)
+(* ------------------------------------------------------------------------- *)
+
+new_type_abbrev ("free_space",`:real#real`);;
+
+let FORALL_FREE_SPACE_THM = prove
+ (`!P. (!fs:free_space. P fs) <=> !n d. P (n,d)`,
+ REWRITE_TAC[FORALL_PAIR_THM]);;
+
+let EXISTS_FREE_SPACE_THM = prove
+ (`!P. (?fs:free_space. P fs) <=> ?n d. P (n,d)`,
+ REWRITE_TAC[EXISTS_PAIR_THM]);;
+
+let interface_IND,interface_REC = define_type
+ "interface = plane | spherical real";;
+
+let interface_kind_IND,interface_kind_REC = define_type
+ "interface_kind = transmitted | reflected";;
+
+new_type_abbrev("optical_component",`:free_space#interface#interface_kind`);;
+
+let FORALL_OPTICAL_COMPONENT_THM = prove
+ (`!P. (!c:optical_component. P c) <=> !fs i ik. P (fs,i,ik)`,
+ REWRITE_TAC[FORALL_PAIR_THM]);;
+
+let EXISTS_OPTICAL_COMPONENT_THM = prove
+ (`!P. (?c:optical_component. P c) <=> ?fs i ik. P (fs,i,ik)`,
+ REWRITE_TAC[EXISTS_PAIR_THM]);;
+
+new_type_abbrev("optical_system",`:optical_component list#free_space`);;
+
+let FORALL_OPTICAL_SYSTEM_THM = prove
+ (`!P. (!os:optical_system. P os) <=> !cs fs. P (cs,fs)`,
+ REWRITE_TAC[FORALL_PAIR_THM]);;
+
+let is_valid_free_space = define
+ `is_valid_free_space ((n,d):free_space) <=> &0 < n /\ &0 <= d`;;
+
+let is_valid_interface = define
+ `(is_valid_interface (plane) <=> T) /\
+ (is_valid_interface (spherical R) <=> ~(&0 = R))`;;
+
+let is_valid_optical_component = new_definition
+ `is_valid_optical_component (fs,i,ik) <=>
+ is_valid_free_space fs /\ is_valid_interface i`;;
+
+let is_valid_optical_system = new_definition
+ `is_valid_optical_system (cs,fs) <=>
+ ALL is_valid_optical_component cs /\ is_valid_free_space fs`;;
+
+let head_index = define
+ `head_index ([],(n,d)) = n /\
+ head_index (CONS ((n,d),i) cs, (nt,dt)) = n`;;
+
+let HEAD_INDEX_VALID_OPTICAL_SYSTEM = prove
+ (`!os:optical_system. is_valid_optical_system os ==> &0 < head_index os`,
+ REWRITE_TAC[FORALL_OPTICAL_SYSTEM_THM;is_valid_optical_system]
+ THEN MATCH_MP_TAC list_INDUCT
+ THEN SIMP_TAC[FORALL_OPTICAL_COMPONENT_THM;FORALL_FREE_SPACE_THM;
+ head_index;is_valid_free_space;ALL;is_valid_optical_component]);;
+
+let HEAD_INDEX_APPEND = prove
+ (`!cs1:optical_component list cs2 fs a.
+ head_index (APPEND cs1 cs2, fs)
+ = head_index (cs1, (head_index (cs2,fs),a))`,
+ MATCH_MP_TAC list_INDUCT
+ THEN REWRITE_TAC[APPEND;head_index;FORALL_OPTICAL_COMPONENT_THM;
+ FORALL_FREE_SPACE_THM]);;
+
+let HEAD_INDEX_CONS_ALT = prove
+ (`!fs i cs:optical_component list fs'.
+ head_index (CONS (fs,i) cs,fs')
+ = head_index ([]:optical_component list,fs)`,
+ REWRITE_TAC[FORALL_FREE_SPACE_THM;head_index]);;
+
+let HEAD_INDEX_CONS_EQ = prove
+ (`!n1 n2 d1 d2 i1 i2 cs1 cs2 fs1 fs2.
+ head_index (CONS ((n1,d1),i1) cs1,fs1)
+ = head_index (CONS ((n2,d2),i2) cs2,fs2)
+ <=> n1 = n2`,
+ REWRITE_TAC[FORALL_PAIR_THM;head_index;PAIR_EQ]);;
+
+let HEAD_INDEX_CONS_EQ_ALT = prove
+ (`!c1 c2 cs1 cs2 fs1 fs2.
+ c1 = c2 ==> head_index (CONS c1 cs1,fs1) = head_index (CONS c2 cs2,fs2)`,
+ SIMP_TAC[FORALL_PAIR_THM;head_index;PAIR_EQ]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Ray formalization *)
+(* ------------------------------------------------------------------------- *)
+
+new_type_abbrev("single_ray",`:real#real`);;
+
+let FORALL_SINGLE_RAY_THM = prove
+ (`!P. (!sr:single_ray. P sr) <=> !y theta. P (y,theta)`,
+ REWRITE_TAC[FORALL_PAIR_THM]);;
+
+new_type_abbrev("ray",
+ `:single_ray # single_ray # (single_ray # single_ray) list`);;
+
+let FORALL_RAY_THM = prove
+ (`!P. (!r:ray. P r) <=> !sr1 sr2 srs. P (sr1,sr2,srs)`,
+ REWRITE_TAC[FORALL_PAIR_THM]);;
+
+let is_valid_ray_in_free_space = define
+ `is_valid_ray_in_free_space (y0,theta0) (y1,theta1) ((n0,d):free_space) <=>
+ y1 = y0 + d * theta0 /\ theta0 = theta1`;;
+
+let is_valid_ray_at_interface = define
+ `(is_valid_ray_at_interface (y0,theta0) (y1,theta1) n0 n1 plane transmitted
+ <=> y1 = y0 /\ n0 * theta0 = n1 * theta1) /\
+ (is_valid_ray_at_interface (y0,theta0) (y1,theta1) n0 n1 (spherical R)
+ transmitted <=>
+ let phi_i = theta0 + y1 / R and phi_t = theta1 + y1 / R in
+ y1 = y0 /\ n0 * phi_i = n1 * phi_t) /\
+ (is_valid_ray_at_interface (y0,theta0) (y1,theta1) n0 n1 plane reflected <=>
+ y1 = y0 /\ n0 * theta0 = n0 * theta1) /\
+ (is_valid_ray_at_interface (y0,theta0) (y1,theta1) n0 n1 (spherical R)
+ reflected <=>
+ let phi = y1 / R - theta0 in
+ y1 = y0 /\ theta1 = --(theta0 + &2 * phi))`;;
+
+let last_single_ray = define
+ `last_single_ray ((sr1,sr2,[]):ray) = sr2 /\
+ last_single_ray ((sr1,sr2,CONS sr3 t):ray) = SND (LAST (CONS sr3 t))`;;
+
+let fst_single_ray = define
+ `fst_single_ray ((sr1,sr2,rs):ray )= sr1`;;
+
+
+let EXISTS_IS_VALID_RAY_IN_SYSTEM = prove(
+ `?f. !sr1 sr2 h h' fs cs rs i ik y0 theta0 y1 theta1 y2 theta2 y3 theta3 n d n' d'.
+ (f (sr1,sr2,[]) (CONS h cs,fs) <=> F) /\
+ (f (sr1,sr2, CONS h' rs) ([],fs) <=> F) /\
+ (f ((y0,theta0),(y1,theta1), []) ([],(n,d)) <=>
+ is_valid_ray_in_free_space (y0,theta0) (y1,theta1) (n,d)) /\
+ (f ((y0,theta0),(y1,theta1), CONS ((y2,theta2),(y3,theta3)) rs)
+ ((CONS ((n',d'),i,ik) cs),(n,d)) <=>
+ (is_valid_ray_in_free_space (y0,theta0) (y1,theta1) (n',d') /\
+ (is_valid_ray_at_interface (y1,theta1) (y2,theta2) n' (head_index(cs,(n,d))) i ik))
+ /\ f ((y2,theta2),(y3,theta3),rs) (cs,(n,d)))`,
+ SUBGOAL_THEN `!y0 theta0 y1 theta1 n d. ?f1. (f1 ([]:(free_space#interface#interface_kind)list) = is_valid_ray_in_free_space (y0,theta0) (y1,theta1) (n,d)
+ /\ !h t. f1 (CONS h t) = F)` (STRIP_ASSUME_TAC o REWRITE_RULE[SKOLEM_THM])
+ THENL [
+ REPEAT GEN_TAC THEN MATCH_ACCEPT_TAC list_RECURSION;
+ SUBGOAL_THEN
+ `!y2 theta2 self y0 theta0 y1 theta1 (fs:free_space). ?f2. (f2 [] = F /\ !h t.
+ f2 (CONS h t) <=>
+ let (n,d),i,ik = h in
+ is_valid_ray_in_free_space (y0,theta0) (y1,theta1) (n,d) /\
+ is_valid_ray_at_interface (y1,theta1) (y2,theta2) n (head_index(t,fs)) i ik /\
+ self t)`
+ (STRIP_ASSUME_TAC o REWRITE_RULE[SKOLEM_THM])
+ THENL [
+ REPEAT GEN_TAC THEN MATCH_ACCEPT_TAC list_RECURSION;
+ SUBGOAL_THEN
+ `!n:real d:real. ?g. (g [] = (\y0:real theta0:real y1:real theta1:real. f1 y0 theta0 y1 theta1 n d) /\ !h t. g (CONS h t) =
+ \y0:real theta0:real y1:real theta1:real.
+ let (y2,theta2),(y3,theta3) = (h:single_ray#single_ray) in
+ (f2 y2 theta2 (g t y2 theta2 y3 theta3) y0 theta0 y1 theta1 (n,d)):(free_space#interface#interface_kind)list ->bool)`
+ (STRIP_ASSUME_TAC o REWRITE_RULE [SKOLEM_THM])
+ THENL [
+ REPEAT GEN_TAC THEN MATCH_ACCEPT_TAC list_RECURSION;
+ EXISTS_TAC `\(((y0,theta0),(y1,theta1),rs):ray) ((cs,(n,d)):optical_system). (g n d rs y0 theta0 y1 theta1 cs):bool`
+ THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;CONJ_ACI;FORALL_PAIR_THM]
+ ]
+ ]
+ ]);;
+
+let is_valid_ray_in_system = new_specification ["is_valid_ray_in_system"] EXISTS_IS_VALID_RAY_IN_SYSTEM;;
+
+
+(* ------------------------------------------------------------------------- *)
+(* 2x2 Matrices *)
+(* ------------------------------------------------------------------------- *)
+
+let mat_pow = define
+ `mat_pow (M:real^N^N) (0:num) :real^N^N = mat 1 /\
+ mat_pow M (SUC n) = M ** mat_pow M n`;;
+
+overload_interface("pow",`mat_pow:real^N^N->num->real^N^N`);;
+
+let MAT_POW_ALT = prove
+ (`!n M. mat_pow M 0 = mat 1 /\ mat_pow M (SUC n) = mat_pow M n ** M`,
+ REWRITE_TAC[mat_pow] THEN INDUCT_TAC
+ THEN REWRITE_TAC[mat_pow;MATRIX_MUL_LID;MATRIX_MUL_RID]
+ THEN ASM_REWRITE_TAC[GSYM MATRIX_MUL_ASSOC]);;
+
+let mat2x2 = new_definition
+ `mat2x2 A B C D :A^2^2 = vector[ vector[A;B]; vector[C;D] ]`;;
+
+let COMMON_TAC xs =
+ SIMP_TAC (xs @ [mat2x2;CART_EQ;VECTOR_2;DIMINDEX_2;FORALL_2;DOT_2;SUM_2]);;
+
+let MAT2X2_VECTOR_MUL = prove
+ (`!A B C D X Y.
+ mat2x2 A B C D ** vector [X;Y] = vector[A*X+B*Y;C*X+D*Y]`,
+ COMMON_TAC [MATRIX_VECTOR_MUL_COMPONENT]);;
+
+let MAT2X2_VECTOR_MUL_GEN = prove
+ (`!(M:real^2^2) (X:real) (Y:real).
+ M ** vector [X;Y] = vector[(M$1$1)*X+ (M$1$2)*Y;(M$2$1*X)+ (M$2$2)*Y]`,
+ COMMON_TAC [MATRIX_VECTOR_MUL_COMPONENT]);;
+
+let MAT2X2_EQ = prove
+ (`!A B C D P Q R S. mat2x2 A B C D = mat2x2 P Q R S <=>
+ A = P /\ B = Q /\ C = R /\ D = S`,
+ COMMON_TAC [] THEN CONV_TAC TAUT);;
+
+let VECTOR2_EQ = prove
+ (`!x y z t. vector [x;y] :A^2 = vector [z;t] <=> x=z /\ y=t`,
+ COMMON_TAC[]);;
+
+let MAT2X2_MUL = prove
+ (`!A B C D P Q R S.
+ mat2x2 A B C D ** mat2x2 P Q R S =
+ mat2x2 (A*P + B*R) (A*Q + B*S) (C*P + D*R) (C*Q + D*S)`,
+ COMMON_TAC[matrix_mul;MATRIX_VECTOR_MUL_COMPONENT;LAMBDA_BETA]);;
+
+let MAT2X2_MAT1 = prove
+ (`mat2x2 (&1) (&0) (&0) (&1) = mat 1`,
+ COMMON_TAC[mat;LAMBDA_BETA] THEN CONV_TAC NUM_REDUCE_CONV);;
+
+let MAT2X2_LID = prove
+ (`!m:real^2^2. mat2x2 (&1) (&0) (&0) (&1) ** m = m`,
+ REWRITE_TAC[MAT2X2_MAT1;MATRIX_MUL_LID]);;
+
+let MAT2X2_RID = prove
+ (`!m:real^2^2. m ** mat2x2 (&1) (&0) (&0) (&1) = m`,
+ REWRITE_TAC[MAT2X2_MAT1;MATRIX_MUL_RID]);;
+
+let MAT2X2_ID = CONJ MAT2X2_LID MAT2X2_RID;;
+
+let MAT2X2_SCALAR_MUL = prove
+ (`!A B C D k. k %% mat2x2 A B C D = mat2x2 (k*A) (k*B) (k*C) (k*D)`,
+ COMMON_TAC [MATRIX_CMUL_COMPONENT]);;
+
+let MAT2X2_SCALAR_MUL_ASSOC = prove
+ (`!A B C D L M N P k.
+ mat2x2 L M N P ** (k %% mat2x2 A B C D)
+ = k %% (mat2x2 L M N P ** mat2x2 A B C D)`,
+ SIMP_TAC[MAT2X2_SCALAR_MUL;MAT2X2_MUL;MAT2X2_EQ] THEN CONV_TAC REAL_FIELD);;
+
+let MAT2X2_EQ_SCALAR_LMUL = prove
+ (`!A B C D P Q R S. ~(k = &0) ==>
+ (k %% mat2x2 A B C D = k %% mat2x2 P Q R S
+ <=> A = P /\ B = Q /\ C = R /\ D = S)`,
+ COMMON_TAC[MAT2X2_SCALAR_MUL] THEN CONV_TAC REAL_FIELD);;
+
+let MAT2X2_DET = prove
+ (`!A B C D. det (mat2x2 A B C D) = A * D - B * C`,
+ COMMON_TAC[DET_2]);;
+
+let FORALL_MATRIX_2X2 = prove
+ (`!P. (!M:real^2^2. P M) <=> ! a b c d.P (mat2x2 a b c d )`,
+ REWRITE_TAC[FORALL_VECTOR_2;mat2x2] );;
+
+let MAT2X2_VECTOR_MUL_ALT = prove
+ (`!(M:real^2^2) (x:real) y x' y'. (vector[x';y'] = M ** vector[x;y]) =
+ (x' = (M ** vector[x;y])$1 /\ y' = (M ** vector[x;y])$2)`,
+COMMON_TAC [ FORALL_MATRIX_2X2;VECTOR2_EQ;MAT2X2_VECTOR_MUL]);;
+
+
+let MAT2_MUL = prove (
+ ` !(M:real^2^2). M**M = mat2x2((M$1$1 * M$1$1) + (M$1$2 * M$2$1))
+ ((M$1$1 * M$1$2) + (M$1$2 * M$2$2))
+ ((M$2$1 * M$1$1) + (M$2$2 * M$2$1))
+ ((M$2$1 * M$1$2) + (M$2$2 * M$2$2))`,
+ COMMON_TAC[matrix_mul;MATRIX_VECTOR_MUL_COMPONENT;LAMBDA_BETA]);;
+
+
+let MAT_POW_ADD = prove (
+`!(M:real^a^a) m n. (M pow (m + n)) = ((M pow m)**(M pow n))`,
+GEN_TAC THEN INDUCT_TAC THEN
+REWRITE_TAC[mat_pow;ADD_CLAUSES;MATRIX_MUL_LID] THEN
+REWRITE_TAC[mat_pow;ADD_CLAUSES;MATRIX_MUL_LID] THEN
+REWRITE_TAC[GSYM MATRIX_MUL_ASSOC] THEN ASM_SIMP_TAC[]);;
+
+
+let MAT2X2_POW2_POW = prove (
+ ` !N. ((mat2x2 A B C D) pow 2) pow N = (mat2x2 A B C D) pow (2*N)`,
+INDUCT_TAC THEN REWRITE_TAC[mat_pow;MULT_0] THEN
+REWRITE_TAC[mat_pow;ADD1;LEFT_ADD_DISTRIB;MULT_CLAUSES;MAT_POW_ADD] THEN
+POP_ASSUM MP_TAC THEN SIMP_TAC[EQ_SYM_EQ]);;
+
+let MAT2X2_POW2_POW_GEN = prove
+(` !n (M:real^k^k). (M pow 2) pow n = M pow (2*n)`,
+INDUCT_TAC THEN REWRITE_TAC[mat_pow;MULT_0] THEN
+REWRITE_TAC[mat_pow;ADD1;LEFT_ADD_DISTRIB;MULT_CLAUSES;MAT_POW_ADD] THEN
+POP_ASSUM MP_TAC THEN SIMP_TAC[EQ_SYM_EQ]);;
+
+let MAT_POW2 = prove (`
+ !(M:real^a^a). M pow 2 = M**M`,
+REWRITE_TAC[mat_pow;TWO;ONE] THEN
+REWRITE_TAC[GSYM ONE; MATRIX_MUL_RID]);;
+
+let TRACE_MAT2X2 = prove( `!A B C D. trace (mat2x2 A B C D) = A+D`,
+ SIMP_TAC[SUM_2;trace;mat2x2;CART_EQ;DIMINDEX_2;FORALL_2;VECTOR_2]);;
+
+let DET_MAT2X2 = prove( `!A B C D. det (mat2x2 A B C D) = A*D - B*C`,
+ SIMP_TAC[SUM_2;DET_2;mat2x2;CART_EQ;DIMINDEX_2;FORALL_2;VECTOR_2]);;
+
+
+(* ------------------------------------------------------------------------- *)
+(* Matrix formalism *)
+(* ------------------------------------------------------------------------- *)
+
+let free_space_matrix = new_definition
+ `free_space_matrix (n,d) = mat2x2 (&1) d (&0) (&1)`;;
+
+let interface_matrix = define
+ `interface_matrix n0 n1 plane transmitted = mat2x2 (&1) (&0) (&0) (n0/n1) /\
+ interface_matrix n0 n1 (spherical R) transmitted
+ = mat2x2 (&1) (&0) ((n0-n1)/n1 * &1/R) (n0/n1)/\
+ interface_matrix n0 n1 plane reflected = mat2x2 (&1) (&0) (&0) (&1) /\
+ interface_matrix n0 n1 (spherical R) reflected
+ = mat2x2 (&1) (&0) (-- &2/R) (&1)`;;
+
+
+(*-------------------------------------------------------------------------
+---Verification of matrix relationships for free space and interfaces------
+-- ** PI= Plane Interface *** SI = Spherical Interface ** FS = Free Space--
+--------------------------------------------------------------------------*)
+
+let common_prove t = prove (t,
+ SIMP_TAC[free_space_matrix;FORALL_FREE_SPACE_THM;MAT2X2_VECTOR_MUL;VECTOR2_EQ;
+ LET_END_DEF;is_valid_ray_in_free_space;REAL_MUL_LZERO;REAL_MUL_LID;LET_DEF;
+ REAL_ADD_LID;interface_matrix;is_valid_ray_at_interface;REAL_ADD_RID]
+ THEN CONV_TAC REAL_FIELD);;
+
+let FS_MATRIX = common_prove
+ `!fs y0 theta0 y1 theta1.
+ is_valid_free_space fs
+ /\ is_valid_ray_in_free_space (y0,theta0) (y1,theta1) fs
+ ==> vector[y1;theta1] = free_space_matrix fs ** vector[y0;theta0]`;;
+
+let PI_MATRIX_TRANSMITTED = common_prove
+ `!n0 n1 y0 theta0 y1 theta1.
+ is_valid_ray_at_interface (y0,theta0) (y1,theta1) n0 n1 plane transmitted
+ /\ &0 < n0 /\ &0 < n1
+ ==> vector [y1;theta1]
+ = interface_matrix n0 n1 plane transmitted ** vector [y0; theta0]`;;
+
+let PI_MATRIX_REFLECTED = common_prove
+ `!n0 y0 theta0 y1 theta1.
+ is_valid_ray_at_interface (y0,theta0) (y1,theta1) n0 n1 plane reflected
+ /\ &0 < n0 /\ &0 < n1
+ ==> vector [y1;theta1]
+ = interface_matrix n0 n1 plane reflected ** vector [y0;theta0]`;;
+
+let PI_MATRIX = prove
+ (`!ik n0 n1 y0 theta0 y1 theta1.
+ is_valid_ray_at_interface (y0,theta0) (y1,theta1) n0 n1 plane ik
+ /\ &0 < n0 /\ &0 < n1
+ ==> vector [y1;theta1]
+ = interface_matrix n0 n1 plane ik ** vector [y0;theta0]`,
+ MATCH_MP_TAC interface_kind_IND
+ THEN SIMP_TAC[PI_MATRIX_TRANSMITTED;PI_MATRIX_REFLECTED]);;
+
+let SI_MATRIX_TRANSMITTED = common_prove
+ `!n0 n1 y0 theta0 y1 theta1 R.
+ is_valid_interface (spherical R) /\ &0 < n0 /\ &0 < n1
+ /\ is_valid_ray_at_interface (y0,theta0) (y1,theta1) n0 n1 (spherical R)
+ transmitted
+ ==> vector [y1;theta1]
+ = interface_matrix n0 n1 (spherical R) transmitted ** vector [y0;theta0]`;;
+
+let SI_MATRIX_REFLECTED = common_prove
+ `!n0 y0 theta0 y1 theta1 R.
+ is_valid_interface (spherical R) /\ &0 < n0
+ /\ is_valid_ray_at_interface (y0,theta0) (y1,theta1) n0 n1 (spherical R)
+ reflected
+ ==> vector [y1;theta1]
+ = interface_matrix n0 n1 (spherical R) reflected ** vector [y0; theta0]`;;
+
+let SI_MATRIX = prove
+ (`!ik n0 n1 y0 theta0 y1 theta1.
+ is_valid_interface (spherical R)
+ /\ is_valid_ray_at_interface (y0,theta0) (y1,theta1) n0 n1 (spherical R) ik
+ /\ &0 < n0 /\ &0 < n1
+ ==> vector [y1; theta1] = interface_matrix n0 n1 (spherical R) ik ** vector [y0; theta0]`,
+ MATCH_MP_TAC interface_kind_IND
+ THEN SIMP_TAC[SI_MATRIX_TRANSMITTED;SI_MATRIX_REFLECTED ]);;
+
+
+(*-------General Relationship for any Interface i --------------------*)
+
+
+let INTERFACE_MATRIX = prove
+ (`!n0 n1 y0 theta0 y1 theta1 i ik.
+ is_valid_interface i /\ &0 < n0 /\ &0 < n1 /\
+ is_valid_ray_at_interface (y0,theta0) (y1,theta1) n0 n1 i ik
+ ==> vector [y1;theta1] = interface_matrix n0 n1 i ik ** vector [y0;theta0]`,
+ REPEAT (MATCH_MP_TAC interface_IND ORELSE GEN_TAC)
+ THEN MESON_TAC[PI_MATRIX;SI_MATRIX]);;
+
+
+(*-----------------------------------------------*)
+
+let system_composition = define
+ `system_composition ([],fs) = free_space_matrix fs /\
+ system_composition (CONS ((n',d'),i,ik) cs,n,d) =
+ system_composition (cs,n,d)
+ ** interface_matrix n' (head_index (cs,n,d)) i ik
+ ** free_space_matrix (n',d')`;;
+
+let IS_VALID_OPTICAL_SYSTEM_REC = prove
+ (`!fs fs' i ik t.
+ is_valid_optical_system ([],fs) = is_valid_free_space fs /\
+ (is_valid_optical_system (CONS (fs,i,ik) t,fs') <=> is_valid_free_space fs
+ /\ is_valid_interface i /\ is_valid_optical_system (t,fs'))`,
+ REWRITE_TAC[is_valid_optical_system;ALL;is_valid_optical_component]
+ THEN MESON_TAC[]);;
+
+let LAST_SINGLE_RAY_REC = prove
+ (`!sr1 sr2 sr3 sr4 t.
+ last_single_ray (sr1,sr2,[]) = sr2 /\
+ last_single_ray (sr1,sr2,CONS (sr3,sr4) t) = last_single_ray (sr3,sr4,t)`,
+ REPEAT (LIST_INDUCT_TAC ORELSE GEN_TAC)
+ THEN SIMP_TAC[last_single_ray;LAST;NOT_CONS_NIL]);;
+
+let IS_VALID_OPTICAL_SYSTEM_HEAD_INDEX = prove
+ (`!os:optical_system. is_valid_optical_system os ==> &0 < head_index os`,
+ REWRITE_TAC[FORALL_OPTICAL_SYSTEM_THM] THEN MATCH_MP_TAC list_INDUCT
+ THEN SIMP_TAC[FORALL_FREE_SPACE_THM;IS_VALID_OPTICAL_SYSTEM_REC;ALL;
+ is_valid_free_space;head_index;FORALL_OPTICAL_COMPONENT_THM]);;
+
+let SYSTEM_MATRIX = prove
+ (`!sys ray.
+ is_valid_optical_system sys /\ is_valid_ray_in_system ray sys ==>
+ let ((y0,theta0),(y1,theta1),rs) = ray in
+ let (y_n,theta_n) = last_single_ray ray in
+ vector [y_n;theta_n] = system_composition sys ** vector [y0;theta0]`,
+ REWRITE_TAC[FORALL_OPTICAL_SYSTEM_THM;FORALL_RAY_THM]
+ THEN MATCH_MP_TAC list_INDUCT THEN CONJ_TAC
+ THEN REWRITE_TAC[FORALL_SINGLE_RAY_THM;FORALL_OPTICAL_COMPONENT_THM]
+ THENL [ALL_TAC;REPEAT GEN_TAC THEN DISCH_TAC]
+ THEN REPEAT (MATCH_MP_TAC list_INDUCT ORELSE GEN_TAC) THEN CONJ_TAC
+ THEN REWRITE_TAC[IS_VALID_OPTICAL_SYSTEM_REC;is_valid_ray_in_system;ALL;
+ system_composition;head_index]
+ THENL [
+ REWRITE_TAC[last_single_ray;LET_DEF;LET_END_DEF;FS_MATRIX];
+ let lemma = prove(`!P. (!a. P a) <=> !y1 th1 y2 th2. P((y1,th1),y2,th2)`,
+ REWRITE_TAC[FORALL_PAIR_THM]) in
+ REWRITE_TAC[lemma;is_valid_ray_in_system;GSYM MATRIX_VECTOR_MUL_ASSOC;
+ LAST_SINGLE_RAY_REC;is_valid_free_space]
+ THEN REPEAT STRIP_TAC THEN REPEAT LET_TAC
+ THEN ASSUM_LIST (REWRITE_TAC o map (REWRITE_RULE[PAIR_EQ] o GSYM))
+ THEN REPEAT_GTCL IMP_RES_THEN (wrap REWRITE_TAC)
+ (REWRITE_RULE[IMP_CONJ;is_valid_free_space;FORALL_FREE_SPACE_THM]
+ (GSYM FS_MATRIX))
+ THEN IMP_RES_THEN ASSUME_TAC IS_VALID_OPTICAL_SYSTEM_HEAD_INDEX
+ THEN REPEAT_GTCL IMP_RES_THEN (wrap REWRITE_TAC)
+ (REWRITE_RULE[IMP_CONJ] (GSYM INTERFACE_MATRIX))
+ THEN EVERY_ASSUM (REPEAT_GTCL IMP_RES_THEN MP_TAC o REWRITE_RULE[IMP_CONJ])
+ THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF] THEN SIMP_TAC[]
+ ]);;
+
+
--- /dev/null
+(* ========================================================================= *)
+(* *)
+(* Top Level File *)
+(* *)
+(* (c) Copyright, Muhammad Umair Siddique, Vincent Aravantinos, 2012 *)
+(* Hardware Verification Group, *)
+(* Concordia University *)
+(* *)
+(* Contact: <muh_sidd@ece.concordia.ca> *)
+(* *)
+(* Last update: July 2014 *)
+(* *)
+(* ========================================================================= *)
+
+(*--------------------------------------------------------------------------*)
+(*--------------It will load all the files in the development---------------*)
+(*--------------------------------------------------------------------------*)
+
+(*needs "utils.ml";;*)
+needs "geometrical_optics.ml";;
+needs "component_library.ml";;
+needs "resonator.ml";;
+needs "z_resonator.ml";;
+needs "fp_resonator.ml";;
+
+
+
+(*-----------------------------------------------------------------------*)
+(*-----------------------TEST--------------------------------------------*)
+(*-----------------------------------------------------------------------*)
+(*-----------------------------------------------------------------------
+ Type in
+
+ > RESONATOR_MATRIX
+
+ you should get the following output--
+
+ |- !n res.
+ system_composition (unfold_resonator res n) =
+ system_composition (unfold_resonator res 1) pow n
+
+
+Moreover, If the last theorem is following:
+
+val ( STABLE_FP ) : thm =
+ |- !R d n.
+ ~(R = &0) /\ &0 < d / R /\ d / R < &2 /\ &0 < n /\ &0 < d
+ ==> is_stable_resonator (fp_cavity R d n)
+- : unit = ()
+
+It means everything is loaded correctly :)
+
+
+NOTE: This development needs "Multivariate" analysis libraries
+of HOL Light. It takes 3 hrs :( on my laptop. On my lab server
+it takes one hour or so. In any case it take a while to load
+depending upon the machine.
+
+--------------------------------------------------------------------------*)
+
+
--- /dev/null
+needs "main.ml";;\r
--- /dev/null
+(* ========================================================================= *)\r
+(* *)\r
+(* Optical Resoantors *)\r
+(* *)\r
+(* (c) Copyright, Muhammad Umair Siddique, Vincent Aravantinos, 2012 *)\r
+(* Hardware Verification Group, *)\r
+(* Concordia University *)\r
+(* *)\r
+(* Contact: <muh_sidd@ece.concordia.ca>, <vincent@ece.concordia.ca> *)\r
+(* *)\r
+(* Last update: Feb 16, 2012 *)\r
+(* *)\r
+(* ========================================================================= *)\r
+\r
+\r
+needs "geometrical_optics.ml";;\r
+\r
+\r
+\r
+(* ------------------------------------------------------------------------- *)\r
+(* Resonators Formalization *)\r
+(* ------------------------------------------------------------------------- *)\r
+\r
+new_type_abbrev("resonator",\r
+ `:interface # optical_component list # free_space # interface`);;\r
+\r
+let FORALL_RESONATOR_THM = prove\r
+ (`!P. (!res:resonator. P res) <=> !i1 cs fs i2. P (i1,cs,fs,i2)`,\r
+ REWRITE_TAC[FORALL_PAIR_THM]);;\r
+\r
+\r
+(* Shifts the free spaces in a list of optical components from right to left.\r
+ * Takes an additional free space parameter to insert in place of the ``hole''\r
+ * remainining on the right.\r
+ * Returns an additional free space corresponding to the leftmost free space\r
+ * that is ``thrown away'' by the shifting.\r
+ *)\r
+\r
+let optical_components_shift = define\r
+ `optical_components_shift [] fs' = [], fs' /\\r
+ optical_components_shift (CONS (fs,i) cs) fs' =\r
+ let cs',fs'' = optical_components_shift cs fs' in\r
+ CONS (fs'',i) cs', fs`;;\r
+\r
+let OPTICAL_COMPONENTS_SHIFT_THROWN_IN = prove\r
+ (`!cs:optical_component list fs.\r
+ let cs',fs'' = optical_components_shift cs fs in\r
+ cs = [] \/ ?i cs''. cs = CONS (fs'',i) cs''`,\r
+ MATCH_MP_TAC list_INDUCT\r
+ THEN REWRITE_TAC[optical_components_shift;FORALL_OPTICAL_COMPONENT_THM;\r
+ LET_PAIR]\r
+ THEN MESON_TAC[]);;\r
+\r
+let VALID_OPTICAL_COMPONENTS_SHIFT = prove\r
+ (`!cs:optical_component list fs.\r
+ ALL is_valid_optical_component cs /\ is_valid_free_space fs ==>\r
+ let cs',fs' = optical_components_shift cs fs in\r
+ ALL is_valid_optical_component cs' /\ is_valid_free_space fs'`,\r
+ MATCH_MP_TAC list_INDUCT THEN\r
+ SIMP_TAC[ALL;optical_components_shift;LET_PAIR;\r
+ FORALL_OPTICAL_COMPONENT_THM;is_valid_optical_component]);;\r
+\r
+let round_trip = new_definition\r
+ `round_trip ((i1,cs,fs,i2) : resonator) =\r
+ APPEND cs (CONS (fs,i2,reflected) (\r
+ let cs',fs1 = optical_components_shift cs fs in\r
+ REVERSE (CONS (fs1,i1,reflected) cs')))`;;\r
+\r
+let ROUND_TRIP_NIL = prove\r
+ (`!i1 fs i2. round_trip (i1,[],fs,i2) = [fs,i2,reflected;fs,i1,reflected]`,\r
+ REWRITE_TAC[round_trip;APPEND;optical_components_shift;LET_DEF;\r
+ LET_END_DEF;REVERSE]);;\r
+\r
+let HEAD_INDEX_ROUND_TRIP = prove\r
+ (`!i1 cs fs i2.\r
+ head_index (round_trip (i1,cs,fs,i2),fs) = head_index (cs,fs)`,\r
+ GEN_TAC THEN MATCH_MP_TAC list_INDUCT\r
+ THEN REWRITE_TAC[round_trip;APPEND;head_index;FORALL_FREE_SPACE_THM;\r
+ FORALL_OPTICAL_COMPONENT_THM]);;\r
+\r
+let LIST_POW = define\r
+ `LIST_POW l 0 = [] /\\r
+ LIST_POW l (SUC n) = APPEND l (LIST_POW l n)`;;\r
+\r
+let ALL_LIST_POW = prove\r
+ (`!n l P. ALL P (LIST_POW l n) <=> n = 0 \/ ALL P l`,\r
+ INDUCT_TAC THEN ASM_REWRITE_TAC[LIST_POW;ALL;ALL_APPEND;NOT_SUC]\r
+ THEN ITAUT_TAC);;\r
+\r
+let SYSTEM_COMPOSITION_APPEND = prove\r
+ (`!cs1 cs2 fs.\r
+ system_composition (APPEND cs1 cs2,fs)\r
+ = system_composition (cs2,fs)\r
+ ** system_composition (cs1,head_index (cs2,fs),&0)`,\r
+ MATCH_MP_TAC list_INDUCT\r
+ THEN SIMP_TAC[free_space_matrix;MAT2X2_ID;FORALL_OPTICAL_COMPONENT_THM;APPEND;\r
+ FORALL_FREE_SPACE_THM;system_composition;GSYM HEAD_INDEX_APPEND;\r
+ MATRIX_MUL_ASSOC]);;\r
+\r
+let is_valid_resonator = new_definition\r
+ `is_valid_resonator ((i1,cs,fs,i2):resonator) <=>\r
+ is_valid_interface i1 /\ ALL is_valid_optical_component cs /\\r
+ is_valid_free_space fs /\ is_valid_interface i2`;;\r
+\r
+(*------- Generates a resonator unfolded n times ------- *)\r
+\r
+let unfold_resonator = define\r
+ `unfold_resonator (i1,cs,fs,i2) n =\r
+ LIST_POW (round_trip (i1,cs,fs,i2)) n, (head_index (cs,fs),&0)`;;\r
+\r
+\r
+let VALID_UNFOLD_RESONATOR = prove\r
+ (`!res. is_valid_resonator res ==>\r
+ !n. is_valid_optical_system (unfold_resonator res n)`,\r
+ REWRITE_TAC[FORALL_RESONATOR_THM;is_valid_resonator]\r
+ THEN REPEAT (INDUCT_TAC ORELSE STRIP_TAC)\r
+ THEN REWRITE_TAC [FORALL_OPTICAL_SYSTEM_THM;is_valid_optical_system;\r
+ unfold_resonator;LIST_POW;ALL;ALL_APPEND;is_valid_free_space;REAL_LE_REFL]\r
+ THEN MP_REWRITE_TAC HEAD_INDEX_VALID_OPTICAL_SYSTEM\r
+ THEN ASM_SIMP_TAC[is_valid_optical_system;ALL_LIST_POW;round_trip;ALL_APPEND;\r
+ TAUT `A /\ (B \/ A) <=> A`;ALL;is_valid_optical_component;LET_PAIR;\r
+ ALL_REVERSE;REWRITE_RULE[LET_PAIR] VALID_OPTICAL_COMPONENTS_SHIFT]);;\r
+\r
+let RESONATOR_MATRIX = prove\r
+ (`!n res.\r
+ system_composition (unfold_resonator res n)\r
+ = system_composition (unfold_resonator res 1) pow n`,\r
+ INDUCT_TAC THEN REWRITE_TAC[FORALL_RESONATOR_THM]\r
+ THENL [\r
+ REWRITE_TAC[unfold_resonator;mat_pow;system_composition;free_space_matrix;\r
+ MAT2X2_MAT1;LIST_POW];\r
+ POP_ASSUM (fun x -> REWRITE_TAC[GSYM x;MAT_POW_ALT])\r
+ THEN REWRITE_TAC[unfold_resonator;LIST_POW;ONE;APPEND_NIL;\r
+ SYSTEM_COMPOSITION_APPEND]\r
+ THEN REPEAT GEN_TAC\r
+ THEN STRUCT_CASES_TAC (Pa.SPEC "n" num_CASES)\r
+ THEN REWRITE_TAC[LIST_POW;head_index]\r
+ THEN Pa.PARSE_IN_CONTEXT (STRUCT_CASES_TAC o C ISPEC list_CASES) "cs"\r
+ THEN REWRITE_TAC[ROUND_TRIP_NIL;APPEND;HEAD_INDEX_CONS_ALT]\r
+ THEN REWRITE_TAC[round_trip;APPEND]\r
+ THEN (REPEAT (REWRITE_TAC[PAIR_EQ] THEN\r
+ (MATCH_MP_TAC HEAD_INDEX_CONS_EQ_ALT ORELSE AP_TERM_TAC)))\r
+ ]);;\r
+\r
+\r
+(* ------------------------------------------------------------------------- *)\r
+(* Stability analysis *)\r
+(* ------------------------------------------------------------------------- *)\r
+\r
+let is_stable_resonator = new_definition\r
+ `is_stable_resonator (res:resonator) <=>\r
+ !r. ?y theta.\r
+ !n. is_valid_ray_in_system r (unfold_resonator res n) ==>\r
+ let y',theta' = last_single_ray r in\r
+ abs y' <= y /\ abs theta' <= theta`;;\r
+\r
+\r
+let REAL_REDUCE_TAC = CONV_TAC (DEPTH_CONV (CHANGED_CONV REAL_POLY_CONV));;\r
+\r
+let SYLVESTER_THEOREM = prove\r
+ (`!A B C D . \r
+ det (mat2x2 A B C D) = &1 /\ -- &1 < (A + D) / &2 /\ (A + D) / &2 < &1 ==>\r
+ let theta = acs ((A + D) / &2) in\r
+ !N.\r
+ (mat2x2 A B C D) pow N = \r
+ (&1 / sin theta) %% (mat2x2\r
+ (A * sin (&N * theta) - sin((&N - &1) * theta))\r
+ (B * sin (&N * theta)) (C * sin (&N * theta))\r
+ (D * sin (&N*theta) - sin ((&N - &1)* theta)))`,\r
+ REWRITE_TAC[MAT2X2_DET;LET_DEF;LET_END_DEF]\r
+ THEN REPEAT (INDUCT_TAC ORELSE STRIP_TAC) THEN REPEAT (POP_ASSUM MP_TAC)\r
+ THEN SIMP_TAC[mat_pow;MAT2X2_MUL;MAT2X2_SCALAR_MUL;MAT2X2_EQ;\r
+ GSYM REAL_OF_NUM_SUC;GSYM MAT2X2_MAT1]\r
+ THEN ONCE_REWRITE_TAC[GSYM REAL_SUB_0] THEN REAL_REDUCE_TAC\r
+ THEN SIMP_TAC[SIN_0;GSYM REAL_NEG_MINUS1;SIN_NEG;SIN_ADD;COS_NEG]\r
+ THEN REAL_REDUCE_TAC THEN SIMP_TAC[REAL_MUL_LINV;SIN_ACS_NZ]\r
+ THEN SIMP_TAC[REAL_LT_IMP_LE;COS_ACS;SIN_ACS] THEN REAL_REDUCE_TAC\r
+ THEN SIMP_TAC\r
+ [REAL_ARITH `x + -- &1 * y + z = t <=> x = t + y - z`;\r
+ REAL_ARITH `-- &1 * x * y * z = --(x * y) * z`]\r
+ THEN CONV_TAC REAL_FIELD);;\r
+\r
+\r
+let SYLVESTER_THEOREM_ALT = prove (` ! (N:num) (A:real) B C D . theta = acs((A + D)/ &2) /\ \r
+ (det (mat2x2 A B C D) = &1) /\ -- &1 <((A + D)/ &2) /\ \r
+ ((A + D)/ &2) < &1 ==> ((mat2x2 A B C D) pow N = \r
+ (&1/sin(theta)) %% (mat2x2 (A*sin(&N*theta)- \r
+ sin((&N - (&1))* theta)) (B*sin(&N*theta)) \r
+ (C*sin(&N*theta)) (D*sin(&N*theta)- sin((&N - (&1))* theta)))) `,\r
+ SUBGOAL_THEN` !A B C D.\r
+ det (mat2x2 A B C D) = &1 /\\r
+ -- &1 < (A + D) / &2 /\\r
+ (A + D) / &2 < &1\r
+ ==> (let theta = acs ((A + D) / &2) in\r
+ !N. mat2x2 A B C D pow N =\r
+ &1 / sin theta %%\r
+ mat2x2 (A * sin (&N * theta) - sin ((&N - &1) * theta))\r
+ (B * sin (&N * theta))\r
+ (C * sin (&N * theta))\r
+ (D * sin (&N * theta) - sin ((&N - &1) * theta))) ` ASSUME_TAC THENL[SIMP_TAC[SYLVESTER_THEOREM];ALL_TAC] THEN POP_ASSUM MP_TAC THEN\r
+LET_TAC THEN ASM_SIMP_TAC[]);;\r
+\r
+\r
+let STABILITY_LEMMA = prove(`\r
+! A B C D xi thetai. det (mat2x2 A B C D) = &1 /\\r
+ -- &1 < (A + D) / &2 /\ (A + D) / &2 < &1 ==>\r
+ ?(Y:real^2). !n. abs ((mat2x2 A B C D pow n ** vector [xi; thetai])$1) <= Y$1 /\\r
+ abs ((mat2x2 A B C D pow n ** vector [xi; thetai])$2) <= Y$2`,\r
+\r
+REPEAT STRIP_TAC THEN \r
+EXISTS_TAC(`vector[ ((abs (&1 / sin (acs ((A + D) / &2))) * abs xi)* &1 + (abs (&1 / sin (acs ((A + D) / &2))) * abs A * abs xi)*abs (&1)) \r
+ + (abs (&1 / sin (acs ((A + D) / &2))) * abs B * abs thetai)* (&1) ;\r
+(abs (&1 / sin (acs ((A + D) / &2))) * abs C * abs xi)* abs(&1) + \r
+((abs (&1 / sin (acs ((A + D) / &2))) * abs thetai)* abs(&1) + (abs (&1 / sin (acs ((A + D) / &2))) * abs D * abs thetai)* abs(&1))]:real^2`) THEN \r
+GEN_TAC THEN SUBGOAL_THEN `!N. mat2x2 A B C D pow N =\r
+ &1 / sin (acs ((A + D) / &2)) %%\r
+ mat2x2 (A * sin (&N * (acs ((A + D) / &2))) - sin ((&N - &1) * (acs ((A + D) / &2))))\r
+ (B * sin (&N * (acs ((A + D) / &2))))\r
+ (C * sin (&N * (acs ((A + D) / &2))))\r
+ (D * sin (&N * (acs ((A + D) / &2))) - sin ((&N - &1) * (acs ((A + D) / &2)))) ` ASSUME_TAC\r
+THENL[GEN_TAC THEN MATCH_MP_TAC SYLVESTER_THEOREM_ALT THEN \r
+ASM_SIMP_TAC[];ALL_TAC] THEN \r
+ONCE_ASM_REWRITE_TAC[] THEN\r
+CONJ_TAC \r
+\r
+THENL[\r
+\r
+SIMP_TAC[ MAT2X2_VECTOR_MUL; MAT2X2_SCALAR_MUL;VECTOR_2] THEN\r
+MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC(` abs\r
+ ((&1 / sin (acs ((A + D) / &2)) * (A * sin (&n * (acs ((A + D) / &2))) - sin ((&n - &1) * (acs ((A + D) / &2))))) *\r
+ xi) +\r
+ abs((&1 / sin (acs ((A + D) / &2)) * B * sin (&n * (acs ((A + D) / &2)))) * thetai)`) THEN \r
+SIMP_TAC[REAL_ABS_TRIANGLE] THEN MATCH_MP_TAC REAL_LE_ADD2 THEN \r
+CONJ_TAC THENL[\r
+SIMP_TAC[REAL_SUB_LDISTRIB;REAL_SUB_RDISTRIB] THEN \r
+SUBGOAL_THEN ` abs\r
+ ((&1 / sin (acs ((A + D) / &2)) * A * sin (&n * (acs ((A + D) / &2)))) * xi -\r
+ (&1 / sin (acs ((A + D) / &2)) * sin (&n * (acs ((A + D) / &2)) - &1 * (acs ((A + D) / &2)))) * xi) = \r
+abs\r
+ ((&1 / sin (acs ((A + D) / &2)) * A * xi) * sin (&n * (acs ((A + D) / &2))) -\r
+ (((&1 / sin (acs ((A + D) / &2))) *xi)* sin (&n * (acs ((A + D) / &2)) - &1 * (acs ((A + D) / &2)))))` ASSUME_TAC THENL[\r
+REAL_ARITH_TAC; ALL_TAC] THEN \r
+ONCE_ASM_REWRITE_TAC[] THEN\r
+SIMP_TAC[REAL_FIELD `!(a:real) b. (b - a)= (--a + b)`] THEN \r
+MATCH_MP_TAC REAL_LE_TRANS THEN \r
+EXISTS_TAC(` abs\r
+ (--((&1 / sin (acs ((A + D) / &2)) * xi) * sin (--(&1 * (acs ((A + D) / &2))) + &n * (acs ((A + D) / &2))))) +\r
+ abs( (&1 / sin (acs ((A + D) / &2)) * A * xi) * sin (&n * (acs ((A + D) / &2)))) `) THEN \r
+SIMP_TAC[REAL_ABS_TRIANGLE] THEN \r
+SIMP_TAC[REAL_ABS_NEG;REAL_ABS_MUL] THEN \r
+MATCH_MP_TAC REAL_LE_ADD2 THEN \r
+\r
+CONJ_TAC THENL[\r
+MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS] THEN\r
+\r
+CONJ_TAC THENL[\r
+SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN\r
+MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] THEN\r
+\r
+SIMP_TAC[REAL_LE_LT;SIN_BOUND];ALL_TAC] THEN \r
+\r
+MATCH_MP_TAC REAL_LE_MUL2 THEN \r
+CONJ_TAC THENL[\r
+\r
+SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN \r
+MATCH_MP_TAC REAL_LE_MUL2 THEN \r
+SIMP_TAC[REAL_ABS_POS] THEN \r
+\r
+CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT]; ALL_TAC] THEN\r
+CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT]; ALL_TAC] THEN \r
+\r
+SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN \r
+MATCH_MP_TAC REAL_LE_MUL2 THEN \r
+SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] THEN \r
+\r
+SIMP_TAC[REAL_ABS_POS;REAL_ABS_1;SIN_BOUND] THEN \r
+SIMP_TAC[REAL_LE_LT]; ALL_TAC] THEN \r
+\r
+SUBGOAL_THEN `abs ((&1 / sin (acs ((A + D) / &2)) * B * sin (&n * (acs ((A + D) / &2)))) * thetai)= abs ((&1 / sin (acs ((A + D) / &2)) * B *thetai)* sin (&n * (acs ((A + D) / &2)))) ` ASSUME_TAC \r
+THENL [REAL_ARITH_TAC;ALL_TAC] THEN \r
+ONCE_ASM_REWRITE_TAC[] THEN SIMP_TAC[REAL_ABS_MUL] THEN \r
+\r
+MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS] THEN CONJ_TAC THENL[\r
+SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN \r
+MATCH_MP_TAC REAL_LE_MUL2 THEN \r
+SIMP_TAC[REAL_ABS_POS]\r
+THEN CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN \r
+ CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN \r
+SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN \r
+MATCH_MP_TAC REAL_LE_MUL2 THEN \r
+SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] THEN \r
+\r
+SIMP_TAC[SIN_BOUND] THEN SIMP_TAC[REAL_LE_LT]; ALL_TAC] THEN \r
+\r
+\r
+SIMP_TAC[ MAT2X2_VECTOR_MUL; MAT2X2_SCALAR_MUL;VECTOR_2] \r
+ THEN MATCH_MP_TAC REAL_LE_TRANS THEN \r
+ EXISTS_TAC(` abs\r
+ ((&1 / sin (acs ((A + D) / &2)) * C * sin (&n * (acs ((A + D) / &2)))) * xi) +\r
+ abs((&1 / sin (acs ((A + D) / &2)) * (D * sin (&n * (acs ((A + D) / &2))) - sin ((&n - &1) * (acs ((A + D) / &2))))) *\r
+ thetai) `) THEN SIMP_TAC[REAL_ABS_TRIANGLE] THEN \r
+MATCH_MP_TAC REAL_LE_ADD2 THEN \r
+CONJ_TAC THENL[SUBGOAL_THEN `abs ((&1 / sin (acs ((A + D) / &2)) * C * sin (&n * (acs ((A + D) / &2)))) * xi) = abs ((&1 / sin (acs ((A + D) / &2)) * C * xi)* sin (&n * (acs ((A + D) / &2)))) ` ASSUME_TAC \r
+THENL[REAL_ARITH_TAC;ALL_TAC] THEN ONCE_ASM_REWRITE_TAC[] THEN \r
+SIMP_TAC[REAL_ABS_MUL] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN \r
+SIMP_TAC[REAL_ABS_POS;SIN_BOUND;REAL_ABS_1] THEN \r
+CONJ_TAC THENL[\r
+SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN \r
+MATCH_MP_TAC REAL_LE_MUL2 THEN \r
+SIMP_TAC[REAL_ABS_POS] THEN CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC]\r
+THEN CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC]\r
+THEN SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN \r
+MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] \r
+THEN SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN \r
+\r
+SIMP_TAC[REAL_SUB_LDISTRIB;REAL_SUB_RDISTRIB] THEN \r
+SUBGOAL_THEN `abs\r
+ ((&1 / sin (acs ((A + D) / &2)) * D * sin (&n * (acs ((A + D) / &2)))) * thetai -\r
+ (&1 / sin (acs ((A + D) / &2)) * sin (&n * (acs ((A + D) / &2)) - &1 * (acs ((A + D) / &2)))) * thetai) = \r
+abs\r
+ ((&1 / sin (acs ((A + D) / &2)) * D * thetai )*sin (&n * (acs ((A + D) / &2))) -\r
+ (&1 / sin (acs ((A + D) / &2)) * thetai) * sin (&n * (acs ((A + D) / &2)) - &1 * (acs ((A + D) / &2)))) ` ASSUME_TAC THENL[\r
+REAL_ARITH_TAC;ALL_TAC] THEN ONCE_ASM_REWRITE_TAC[] THEN \r
+SIMP_TAC[REAL_FIELD `!(a:real) b. (b - a)= (--a + b)`] THEN \r
+MATCH_MP_TAC REAL_LE_TRANS THEN \r
+EXISTS_TAC(` abs\r
+ (--((&1 / sin (acs ((A + D) / &2)) * thetai) * sin (--(&1 * (acs ((A + D) / &2))) + &n * (acs ((A + D) / &2))))) +\r
+ abs( (&1 / sin (acs ((A + D) / &2)) * D * thetai) * sin (&n * (acs ((A + D) / &2)))) `)\r
+THEN SIMP_TAC[REAL_ABS_TRIANGLE] THEN SIMP_TAC[REAL_ABS_NEG;REAL_ABS_MUL]\r
+THEN MATCH_MP_TAC REAL_LE_ADD2 THEN \r
+CONJ_TAC THENL[MATCH_MP_TAC REAL_LE_MUL2 THEN \r
+SIMP_TAC[REAL_ABS_POS;REAL_ABS_1;SIN_BOUND] THEN \r
+CONJ_TAC THENL[ SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN\r
+MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] THEN\r
+SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN \r
+MATCH_MP_TAC REAL_LE_MUL2 THEN \r
+SIMP_TAC[REAL_ABS_POS;REAL_ABS_1;SIN_BOUND] THEN \r
+CONJ_TAC THENL[SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b`] THEN \r
+MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS] THEN\r
+CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN \r
+CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN \r
+SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN \r
+MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] THEN\r
+SIMP_TAC[REAL_LE_LT]);;\r
+\r
+\r
+let STABILITY_LEMMA_GENERAL = prove(`! (M:real^2^2) xi thetai. det (M) = &1 /\\r
+ -- &1 < (M$1$1 + M$2$2) / &2 /\ (M$1$1 + M$2$2) / &2 < &1 ==>\r
+ ?(Y:real^2). !n. abs ((M pow n ** vector [xi; thetai])$1) <= Y$1 /\\r
+ abs ((M pow n ** vector [xi; thetai])$2) <= Y$2`,\r
+ REWRITE_TAC[FORALL_MATRIX_2X2] THEN REPEAT STRIP_TAC THEN \r
+MATCH_MP_TAC STABILITY_LEMMA THEN REPEAT(POP_ASSUM MP_TAC) THEN \r
+SIMP_TAC [mat2x2;CART_EQ;VECTOR_2;DIMINDEX_2;FORALL_2;DOT_2;SUM_2]);;\r
+\r
+\r
+let STABILITY_THEOREM = prove (`\r
+ !res. is_valid_resonator res /\\r
+ (!n. let M = system_composition (unfold_resonator res 1) in\r
+ (det M = &1) /\ -- &1 < (M$1$1 + M$2$2) / &2 /\ (M$1$1 + M$2$2) / &2 < &1)\r
+ ==> is_stable_resonator res`,\r
+\r
+GEN_TAC THEN REPEAT (LET_TAC) THEN REPEAT STRIP_TAC THEN \r
+REPEAT STRIP_TAC THEN REWRITE_TAC[is_stable_resonator] THEN GEN_TAC THEN \r
+SUBGOAL_THEN ` (?Y:real^2. !n. abs ((M pow n ** vector [FST(fst_single_ray r);SND(fst_single_ray r) ])$1) \r
+<= Y$1 /\ abs (((M:real^2^2) pow n ** vector [FST(fst_single_ray r);SND(fst_single_ray r) ])$2) <= Y$2)`\r
+ASSUME_TAC THENL[MP_REWRITE_TAC STABILITY_LEMMA_GENERAL THEN ASM_SIMP_TAC[];ALL_TAC] THEN \r
+POP_ASSUM MP_TAC THEN STRIP_TAC THEN \r
+EXISTS_TAC(`((Y:real^2)$1):real`) THEN EXISTS_TAC(`((Y:real^2)$2):real`) THEN \r
+REPEAT STRIP_TAC THEN LET_TAC THEN \r
+SUBGOAL_THEN `(let (xi,thetai),(y1,theta1),rs = r in\r
+ let y',theta' = last_single_ray r in\r
+ vector [y'; theta'] =\r
+ system_composition ((unfold_resonator res n):optical_system) **\r
+ vector [xi; thetai])` ASSUME_TAC THENL[MATCH_MP_TAC SYSTEM_MATRIX THEN \r
+ASM_SIMP_TAC[ VALID_UNFOLD_RESONATOR ]; ALL_TAC] THEN POP_ASSUM MP_TAC THEN \r
+ONCE_REWRITE_TAC[ MAT2X2_VECTOR_MUL_ALT] THEN ONCE_REWRITE_TAC[RESONATOR_MATRIX] THEN \r
+ONCE_ASM_REWRITE_TAC[] THEN LET_TAC THEN LET_TAC THEN \r
+DISCH_TAC THEN ONCE_ASM_REWRITE_TAC[] THEN REPEAT(POP_ASSUM MP_TAC) THEN \r
+REWRITE_TAC[fst_single_ray;FST;SND] THEN SIMP_TAC[]);;\r
+\r
+(*-----------------Stability theorem for the symmetric resonators ------------------*)\r
+\r
+\r
+let STABILITY_LEMMA_SYM = prove (` ! A B C D xi thetai. det (mat2x2 A B C D) = &1 /\\r
+ -- &1 < (A + D) / &2 /\ (A + D) / &2 < &1 ==>\r
+ ?(Y:real^2). !n. abs (((mat2x2 A B C D pow 2)pow n ** vector [xi; thetai])$1) <= Y$1 /\\r
+ abs (((mat2x2 A B C D pow 2) pow n ** vector [xi; thetai])$2) <= Y$2`,\r
+\r
+REWRITE_TAC[MAT2X2_POW2_POW] THEN \r
+REPEAT STRIP_TAC THEN \r
+EXISTS_TAC(`vector[ ((abs (&1 / sin (acs ((A + D) / &2))) * abs xi)* &1 + (abs (&1 / sin (acs ((A + D) / &2))) * abs A * abs xi)*abs (&1)) \r
+ + (abs (&1 / sin (acs ((A + D) / &2))) * abs B * abs thetai)* (&1) ;\r
+(abs (&1 / sin (acs ((A + D) / &2))) * abs C * abs xi)* abs(&1) + \r
+((abs (&1 / sin (acs ((A + D) / &2))) * abs thetai)* abs(&1) + (abs (&1 / sin (acs ((A + D) / &2))) * abs D * abs thetai)* abs(&1))]:real^2`) THEN \r
+GEN_TAC THEN SUBGOAL_THEN `!N. mat2x2 A B C D pow (2*N) =\r
+ &1 / sin (acs ((A + D) / &2)) %%\r
+ mat2x2 (A * sin (&(2*N) * (acs ((A + D) / &2))) - sin ((&(2*N) - &1) * (acs ((A + D) / &2))))\r
+ (B * sin (&(2*N) * (acs ((A + D) / &2))))\r
+ (C * sin (&(2*N) * (acs ((A + D) / &2))))\r
+ (D * sin (&(2*N) * (acs ((A + D) / &2))) - sin ((&(2*N) - &1) * (acs ((A + D) / &2)))) ` ASSUME_TAC\r
+THENL[GEN_TAC THEN MATCH_MP_TAC SYLVESTER_THEOREM_ALT THEN \r
+ASM_SIMP_TAC[];ALL_TAC] THEN \r
+ONCE_ASM_REWRITE_TAC[] THEN CONJ_TAC \r
+THENL[SIMP_TAC[ MAT2X2_VECTOR_MUL; MAT2X2_SCALAR_MUL;VECTOR_2] THEN\r
+MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC(` abs\r
+ ((&1 / sin (acs ((A + D) / &2)) * (A * sin (&(2*n) * (acs ((A + D) / &2))) - sin ((&(2*n) - &1) * (acs ((A + D) / &2))))) *\r
+ xi) +\r
+ abs((&1 / sin (acs ((A + D) / &2)) * B * sin (&(2*n) * (acs ((A + D) / &2)))) * thetai)`) THEN \r
+SIMP_TAC[REAL_ABS_TRIANGLE] THEN MATCH_MP_TAC REAL_LE_ADD2 THEN \r
+CONJ_TAC THENL[\r
+SIMP_TAC[REAL_SUB_LDISTRIB;REAL_SUB_RDISTRIB] THEN \r
+SUBGOAL_THEN ` abs\r
+ ((&1 / sin (acs ((A + D) / &2)) * A * sin (&(2*n) * (acs ((A + D) / &2)))) * xi -\r
+ (&1 / sin (acs ((A + D) / &2)) * sin (&(2*n) * (acs ((A + D) / &2)) - &1 * (acs ((A + D) / &2)))) * xi) = \r
+abs\r
+ ((&1 / sin (acs ((A + D) / &2)) * A * xi) * sin (&(2*n) * (acs ((A + D) / &2))) -\r
+ (((&1 / sin (acs ((A + D) / &2))) *xi)* sin (&(2*n) * (acs ((A + D) / &2)) - &1 * (acs ((A + D) / &2)))))` ASSUME_TAC THENL[\r
+REAL_ARITH_TAC; ALL_TAC] THEN \r
+ONCE_ASM_REWRITE_TAC[] THEN\r
+SIMP_TAC[REAL_FIELD `!(a:real) b. (b - a)= (--a + b)`] THEN \r
+MATCH_MP_TAC REAL_LE_TRANS THEN \r
+EXISTS_TAC(` abs\r
+ (--((&1 / sin (acs ((A + D) / &2)) * xi) * sin (--(&1 * (acs ((A + D) / &2))) + &(2*n) * (acs ((A + D) / &2))))) +\r
+ abs( (&1 / sin (acs ((A + D) / &2)) * A * xi) * sin (&(2*n) * (acs ((A + D) / &2)))) `) THEN \r
+SIMP_TAC[REAL_ABS_TRIANGLE] THEN \r
+SIMP_TAC[REAL_ABS_NEG;REAL_ABS_MUL] THEN \r
+MATCH_MP_TAC REAL_LE_ADD2 THEN \r
+\r
+CONJ_TAC THENL[\r
+MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS] THEN\r
+\r
+CONJ_TAC THENL[\r
+SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN\r
+MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] THEN\r
+\r
+SIMP_TAC[REAL_LE_LT;SIN_BOUND];ALL_TAC] THEN \r
+\r
+MATCH_MP_TAC REAL_LE_MUL2 THEN \r
+CONJ_TAC THENL[\r
+\r
+SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN \r
+MATCH_MP_TAC REAL_LE_MUL2 THEN \r
+SIMP_TAC[REAL_ABS_POS] THEN \r
+\r
+CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT]; ALL_TAC] THEN\r
+CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT]; ALL_TAC] THEN \r
+\r
+SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN \r
+MATCH_MP_TAC REAL_LE_MUL2 THEN \r
+SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] THEN \r
+\r
+SIMP_TAC[REAL_ABS_POS;REAL_ABS_1;SIN_BOUND] THEN \r
+SIMP_TAC[REAL_LE_LT]; ALL_TAC] THEN \r
+\r
+SUBGOAL_THEN `abs ((&1 / sin (acs ((A + D) / &2)) * B * sin (&(2*n) * (acs ((A + D) / &2)))) * thetai)= abs ((&1 / sin (acs ((A + D) / &2)) * B *thetai)* sin (&(2*n) * (acs ((A + D) / &2)))) ` ASSUME_TAC \r
+THENL [REAL_ARITH_TAC;ALL_TAC] THEN \r
+ONCE_ASM_REWRITE_TAC[] THEN SIMP_TAC[REAL_ABS_MUL] THEN \r
+\r
+MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS] THEN CONJ_TAC THENL[\r
+SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN \r
+MATCH_MP_TAC REAL_LE_MUL2 THEN \r
+SIMP_TAC[REAL_ABS_POS]\r
+THEN CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN \r
+ CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN \r
+SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN \r
+MATCH_MP_TAC REAL_LE_MUL2 THEN \r
+SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] THEN \r
+\r
+SIMP_TAC[SIN_BOUND] THEN SIMP_TAC[REAL_LE_LT]; ALL_TAC] THEN \r
+\r
+\r
+SIMP_TAC[ MAT2X2_VECTOR_MUL; MAT2X2_SCALAR_MUL;VECTOR_2] \r
+ THEN MATCH_MP_TAC REAL_LE_TRANS THEN \r
+ EXISTS_TAC(` abs\r
+ ((&1 / sin (acs ((A + D) / &2)) * C * sin (&(2*n) * (acs ((A + D) / &2)))) * xi) +\r
+ abs((&1 / sin (acs ((A + D) / &2)) * (D * sin (&(2*n) * (acs ((A + D) / &2))) - sin ((&(2*n) - &1) * (acs ((A + D) / &2))))) *\r
+ thetai) `) THEN SIMP_TAC[REAL_ABS_TRIANGLE] THEN \r
+MATCH_MP_TAC REAL_LE_ADD2 THEN \r
+CONJ_TAC THENL[SUBGOAL_THEN `abs ((&1 / sin (acs ((A + D) / &2)) * C * sin (&(2*n) * (acs ((A + D) / &2)))) * xi) = abs ((&1 / sin (acs ((A + D) / &2)) * C * xi)* sin (&(2*n) * (acs ((A + D) / &2)))) ` ASSUME_TAC \r
+THENL[REAL_ARITH_TAC;ALL_TAC] THEN ONCE_ASM_REWRITE_TAC[] THEN \r
+SIMP_TAC[REAL_ABS_MUL] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN \r
+SIMP_TAC[REAL_ABS_POS;SIN_BOUND;REAL_ABS_1] THEN \r
+CONJ_TAC THENL[\r
+SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN \r
+MATCH_MP_TAC REAL_LE_MUL2 THEN \r
+SIMP_TAC[REAL_ABS_POS] THEN CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC]\r
+THEN CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC]\r
+THEN SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN \r
+MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] \r
+THEN SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN \r
+\r
+SIMP_TAC[REAL_SUB_LDISTRIB;REAL_SUB_RDISTRIB] THEN \r
+SUBGOAL_THEN `abs\r
+ ((&1 / sin (acs ((A + D) / &2)) * D * sin (&(2*n) * (acs ((A + D) / &2)))) * thetai -\r
+ (&1 / sin (acs ((A + D) / &2)) * sin (&(2*n) * (acs ((A + D) / &2)) - &1 * (acs ((A + D) / &2)))) * thetai) = \r
+abs\r
+ ((&1 / sin (acs ((A + D) / &2)) * D * thetai )*sin (&(2*n) * (acs ((A + D) / &2))) -\r
+ (&1 / sin (acs ((A + D) / &2)) * thetai) * sin (&(2*n) * (acs ((A + D) / &2)) - &1 * (acs ((A + D) / &2)))) ` ASSUME_TAC THENL[\r
+REAL_ARITH_TAC;ALL_TAC] THEN ONCE_ASM_REWRITE_TAC[] THEN \r
+SIMP_TAC[REAL_FIELD `!(a:real) b. (b - a)= (--a + b)`] THEN \r
+MATCH_MP_TAC REAL_LE_TRANS THEN \r
+EXISTS_TAC(` abs\r
+ (--((&1 / sin (acs ((A + D) / &2)) * thetai) * sin (--(&1 * (acs ((A + D) / &2))) + &(2*n) * (acs ((A + D) / &2))))) +\r
+ abs( (&1 / sin (acs ((A + D) / &2)) * D * thetai) * sin (&(2*n) * (acs ((A + D) / &2)))) `)\r
+THEN SIMP_TAC[REAL_ABS_TRIANGLE] THEN SIMP_TAC[REAL_ABS_NEG;REAL_ABS_MUL]\r
+THEN MATCH_MP_TAC REAL_LE_ADD2 THEN \r
+CONJ_TAC THENL[MATCH_MP_TAC REAL_LE_MUL2 THEN \r
+SIMP_TAC[REAL_ABS_POS;REAL_ABS_1;SIN_BOUND] THEN \r
+CONJ_TAC THENL[ SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN\r
+MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] THEN\r
+SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN \r
+MATCH_MP_TAC REAL_LE_MUL2 THEN \r
+SIMP_TAC[REAL_ABS_POS;REAL_ABS_1;SIN_BOUND] THEN \r
+CONJ_TAC THENL[SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b`] THEN \r
+MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS] THEN\r
+CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN \r
+CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN \r
+SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN \r
+MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] THEN\r
+SIMP_TAC[REAL_LE_LT]);;\r
+\r
+let STABILITY_LEMMA_GENERAL_SYM = prove(`! (M:real^2^2) xi thetai. det (M) = &1 /\\r
+ -- &1 < (M$1$1 + M$2$2) / &2 /\ (M$1$1 + M$2$2) / &2 < &1 ==>\r
+ ?(Y:real^2). !n. abs (((M pow 2) pow n ** vector [xi; thetai])$1) <= Y$1 /\\r
+ abs (((M pow 2) pow n ** vector [xi; thetai])$2) <= Y$2`,\r
+ REWRITE_TAC[FORALL_MATRIX_2X2] THEN REPEAT STRIP_TAC THEN \r
+MATCH_MP_TAC STABILITY_LEMMA_SYM THEN REPEAT(POP_ASSUM MP_TAC) THEN \r
+SIMP_TAC [mat2x2;CART_EQ;VECTOR_2;DIMINDEX_2;FORALL_2;DOT_2;SUM_2]);;\r
+\r
+let STABILITY_THEOREM_SYM = prove (\r
+ `!res. is_valid_resonator res /\\r
+ ((M:real^2^2) pow 2 = system_composition (unfold_resonator res 1)) /\\r
+ (det (M:real^2^2) = &1) /\ -- &1 < (M$1$1 + M$2$2) / &2 /\ (M$1$1 + M$2$2) / &2 < &1\r
+ ==> is_stable_resonator res`,\r
+\r
+GEN_TAC THEN ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN \r
+POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN \r
+REPEAT STRIP_TAC THEN REWRITE_TAC[is_stable_resonator] THEN \r
+GEN_TAC THEN \r
+SUBGOAL_THEN ` (?Y:real^2. !n. abs (((M pow 2) pow n ** vector [FST(fst_single_ray r);SND(fst_single_ray r) ])$1) <= Y$1 /\\r
+ abs ((((M:real^2^2) pow 2 ) pow n ** vector [FST(fst_single_ray r);SND(fst_single_ray r) ])$2) <= Y$2) ` ASSUME_TAC THENL[ \r
+MP_REWRITE_TAC STABILITY_LEMMA_GENERAL_SYM THEN ASM_SIMP_TAC[]; ALL_TAC] THEN \r
+POP_ASSUM MP_TAC THEN STRIP_TAC THEN EXISTS_TAC(`((Y:real^2)$1):real`) THEN \r
+EXISTS_TAC(`((Y:real^2)$2):real`) THEN REPEAT STRIP_TAC THEN \r
+LET_TAC THEN SUBGOAL_THEN `(let (xi,thetai),(y1,theta1),rs = r in\r
+ let y',theta' = last_single_ray r in\r
+ vector [y'; theta'] =\r
+ system_composition ((unfold_resonator res n):optical_system) **\r
+ vector [xi; thetai])` ASSUME_TAC THENL[ \r
+MATCH_MP_TAC SYSTEM_MATRIX THEN ASM_SIMP_TAC[ VALID_UNFOLD_RESONATOR];ALL_TAC] THEN \r
+POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[MAT2X2_VECTOR_MUL_ALT] THEN \r
+ONCE_REWRITE_TAC[RESONATOR_MATRIX] THEN ONCE_ASM_REWRITE_TAC[] THEN LET_TAC THEN \r
+LET_TAC THEN DISCH_TAC THEN ONCE_ASM_REWRITE_TAC[] THEN REPEAT(POP_ASSUM MP_TAC) THEN \r
+REWRITE_TAC[fst_single_ray;FST;SND] THEN SIMP_TAC[]);;\r
+\r
+ \r
--- /dev/null
+module Pa :
+ sig
+ val CONTEXT_TAC : ((string * pretype) list -> tactic) -> tactic
+ val PARSE_IN_CONTEXT : (term -> tactic) -> (string -> tactic)
+ val EXISTS_TAC : string -> tactic
+ val SUBGOAL_THEN : string -> thm_tactic -> tactic
+ val SUBGOAL_TAC : string -> string -> tactic list -> tactic
+ val ASM_CASES_TAC : string -> tactic
+ val BOOL_CASES_TAC : string -> tactic
+ val SPEC_TAC : string * string -> tactic
+ val SPEC : string -> thm -> thm
+ val SPECL : string list -> thm -> thm
+ val GEN : string -> thm -> thm
+ val GENL : string list -> thm -> thm
+ val X_GEN_TAC : string -> tactic
+ val REAL_ARITH : string -> thm
+ val REAL_FIELD : string -> thm
+ val REAL_RING : string -> thm
+ val ARITH_RULE : string -> thm
+ val NUM_RING : string -> thm
+ val INT_ARITH : string -> thm
+ val call_with_interface : (unit -> 'a) -> (term -> 'b) -> string -> 'b
+ end
+ =
+ struct
+ let parse_preterm = fst o parse_preterm o lex o explode
+
+ let CONTEXT_TAC ttac (asms,c as g) =
+ let vs = frees c @ freesl (map (concl o snd) asms) in
+ ttac (map (fun x -> name_of x,pretype_of_type(type_of x)) vs) g
+
+ let PARSE_IN_CONTEXT ttac s =
+ CONTEXT_TAC (fun env ->
+ ttac (term_of_preterm (retypecheck env (parse_preterm s))))
+
+ let type_of_forall = type_of o fst o dest_forall
+
+ let force_type ?(env=[]) s ty =
+ let pty = pretype_of_type ty in
+ term_of_preterm (retypecheck env (Typing(parse_preterm s,pty)))
+
+ let BOOL_CONTEXT_TAC ttac s =
+ CONTEXT_TAC (fun env -> ttac (force_type ~env s bool_ty))
+
+ let SUBGOAL_THEN s ttac = BOOL_CONTEXT_TAC (C SUBGOAL_THEN ttac) s
+ let SUBGOAL_TAC l s tacs = BOOL_CONTEXT_TAC (C (SUBGOAL_TAC l) tacs) s
+
+ let ASM_CASES_TAC = BOOL_CONTEXT_TAC ASM_CASES_TAC
+ let BOOL_CASES_TAC = BOOL_CONTEXT_TAC BOOL_CASES_TAC
+
+ let EXISTS_TAC s (_,c as g) =
+ CONTEXT_TAC (fun env ->
+ EXISTS_TAC (force_type ~env s (type_of (fst (dest_exists c))))) g
+
+ let SPEC_TAC (u,x) =
+ PARSE_IN_CONTEXT (fun u' -> SPEC_TAC (u',force_type x (type_of u'))) u
+
+ let SPEC s th = SPEC (force_type s (type_of_forall (concl th))) th
+
+ let SPECL tms th =
+ try rev_itlist SPEC tms th with Failure _ -> failwith "SPECL"
+
+ let GEN s th =
+ GEN (try find ((=) s o name_of) (frees (concl th)) with _ -> parse_term s)
+ th
+
+ let GENL = itlist GEN
+
+ let X_GEN_TAC s (_,c as g) = X_GEN_TAC (force_type s (type_of_forall c)) g
+
+ let call_with_interface p f s =
+ let i = !the_interface in
+ p ();
+ let res = f (parse_term s) in
+ the_interface := i;
+ res
+
+ let [REAL_ARITH;REAL_FIELD;REAL_RING] =
+ map (call_with_interface prioritize_real) [REAL_ARITH;REAL_FIELD;REAL_RING]
+ let [ARITH_RULE;NUM_RING] =
+ map (call_with_interface prioritize_num) [ARITH_RULE;NUM_RING]
+ let INT_ARITH = call_with_interface prioritize_int INT_ARITH
+ end;;
+
+module Pa =
+ struct
+ include Pa
+ let COMPLEX_FIELD = call_with_interface prioritize_complex COMPLEX_FIELD;;
+ let SIMPLE_COMPLEX_ARITH =
+ call_with_interface prioritize_complex SIMPLE_COMPLEX_ARITH;
+ end;;
+
+let MP_REWRITE_TAC th (_,c as g) =
+ let [th] = mk_rewrites true th [] in
+ let PART_MATCH = PART_MATCH (lhs o snd o strip_forall o snd o dest_imp) th in
+ let th = ref TRUTH in
+ ignore (find_term (fun t -> try th := PART_MATCH t; true with _ -> false) c);
+ (SUBGOAL_THEN (lhand (concl !th)) (fun x ->
+ REWRITE_TAC[MP !th x] THEN STRIP_ASSUME_TAC x)) g;;
+
+let CASES_REWRITE_TAC th (_,c as g) =
+ let [th] = mk_rewrites true th [] in
+ let PART_MATCH = PART_MATCH (lhs o snd o strip_forall o snd o dest_imp) th in
+ let th = ref TRUTH in
+ ignore (find_term (fun t -> try th := PART_MATCH t; true with _ -> false) c);
+ (ASM_CASES_TAC (lhand (concl !th)) THENL [
+ POP_ASSUM (fun x -> REWRITE_TAC[MP !th x] THEN ASSUME_TAC x);
+ POP_ASSUM (ASSUME_TAC o REWRITE_RULE[NOT_CLAUSES])]) g;;
+
+let wrap f x = f [x];;
+
+let CONJS xs = end_itlist CONJ xs;;
+
+let rec simp_horn_conv =
+ let is_atomic (x,y) = if x = [] then y else failwith "" in
+ let rec tl = function [] -> [] | _::xs -> xs in
+ fun l ->
+ let fixpoint = ref true in
+ let l' =
+ rev_itlist (fun (hs,cs) (dones,todos) ->
+ let atomics = flat (mapfilter is_atomic (dones@todos)) in
+ let f = filter (not o C mem atomics) in
+ let hs' = f hs and cs' = f cs in
+ if not (hs' = hs) or not (cs' = cs) then fixpoint := false;
+ if (cs' = [] && cs <> [])
+ then (dones,tl todos)
+ else ((hs',cs')::dones),tl todos)
+ l ([],tl l)
+ in
+ if !fixpoint then l else simp_horn_conv (fst l');;
+
+let horns_of_term =
+ let strip_conj = binops `(/\)` in
+ fun t -> map (fun t ->
+ try
+ let h,c = dest_imp t in
+ strip_conj h,strip_conj c
+ with _ -> [],[t]) (strip_conj t);;
+
+let term_of_horns =
+ let term_of_horn = function
+ |[],cs -> list_mk_conj cs
+ |_,[] -> (print_endline "ici";`T`)
+ |hs,cs -> mk_imp (list_mk_conj hs,list_mk_conj cs)
+ in
+ list_mk_conj o map term_of_horn;;
+
+let SIMP_HORN_CONV t =
+ TAUT (mk_eq (t,((term_of_horns o simp_horn_conv o horns_of_term) t)));;
+
+let SIMP_HORN_TAC =
+ REWRITE_TAC[IMP_IMP]
+ THEN CONV_TAC (TOP_DEPTH_CONV (CHANGED_CONV SIMP_HORN_CONV));;
+
+let HINT_EXISTS_TAC =
+ let strip_conj = binops `/\` in
+ let P = `P:bool` in
+ fun (hs,c as g) ->
+ let hs = map snd hs in
+ let vars = flat (map thm_frees hs) in
+ let vs,c' = strip_exists c in
+ let cs = strip_conj c' in
+ let hyp_match c h = term_match (subtract vars vs) c (concl h), h in
+ let (_,fosubs,_),h = tryfind (fun c -> tryfind (hyp_match c) hs) cs in
+ let ts,vs' = unzip fosubs in
+ let vs'' = subtract vs vs' in
+ let th = MESON[] (mk_eq(list_mk_exists(vs,P),list_mk_exists(vs'@vs'',P))) in
+ (REWRITE_TAC [th] THEN MAP_EVERY EXISTS_TAC ts THEN REWRITE_TAC [h]) g;;
+
+let rec fixpoint f x =
+ let y = f x in
+ if y = x then y else fixpoint f y;;
+
+let GIMP_IMP =
+ GEN_ALL o REWRITE_RULE[IMP_IMP;GSYM CONJ_ASSOC] o DISCH_ALL o fixpoint
+ (UNDISCH_ALL o SPEC_ALL);;
+
--- /dev/null
+(* ========================================================================= *)
+(* *)
+(* 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))`]);;
+
+
git://colo12-c703.uibk.ac.at / Ray193/.git / commitdiff