From 34ad47d63939a9c5fd96cc54ae90d49115b54a9f Mon Sep 17 00:00:00 2001 From: Cezary Kaliszyk Date: Sun, 24 Aug 2014 15:21:06 +0200 Subject: [PATCH] Update from HH --- component_library.ml | 130 ++++++++++++ fp_resonator.ml | 62 ++++++ geometrical_optics.ml | 516 +++++++++++++++++++++++++++++++++++++++++++++ main.ml | 61 ++++++ make.ml | 1 + resonator.ml | 556 +++++++++++++++++++++++++++++++++++++++++++++++++ utils.ml | 177 ++++++++++++++++ z_resonator.ml | 124 +++++++++++ 8 files changed, 1627 insertions(+), 0 deletions(-) create mode 100644 component_library.ml create mode 100644 fp_resonator.ml create mode 100644 geometrical_optics.ml create mode 100644 main.ml create mode 100644 make.ml create mode 100644 resonator.ml create mode 100644 utils.ml create mode 100644 z_resonator.ml diff --git a/component_library.ml b/component_library.ml new file mode 100644 index 0000000..e39bd5f --- /dev/null +++ b/component_library.ml @@ -0,0 +1,130 @@ +(* ========================================================================= *) +(* *) +(* Frequent Component Library *) +(* *) +(* (c) Copyright, Muhammad Umair Siddique, Vincent Aravantinos, 2012 *) +(* Hardware Verification Group, *) +(* Concordia University *) +(* *) +(* Contact: , *) +(* *) +(* 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]);; + + diff --git a/fp_resonator.ml b/fp_resonator.ml new file mode 100644 index 0000000..77becd8 --- /dev/null +++ b/fp_resonator.ml @@ -0,0 +1,62 @@ +(* ========================================================================= *) +(* *) +(* Fabry Perot Resonator *) +(* *) +(* (c) Copyright, Muhammad Umair Siddique, Vincent Aravantinos, 2012 *) +(* Hardware Verification Group, *) +(* Concordia University *) +(* *) +(* Contact: , *) +(* *) +(* 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);; + diff --git a/geometrical_optics.ml b/geometrical_optics.ml new file mode 100644 index 0000000..72fe307 --- /dev/null +++ b/geometrical_optics.ml @@ -0,0 +1,516 @@ +(* ========================================================================= *) +(* *) +(* Geometrical Optics Library *) +(* *) +(* (c) Copyright, Muhammad Umair Siddique, Vincent Aravantinos, 2012 *) +(* Hardware Verification Group, *) +(* Concordia University *) +(* *) +(* Contact: , *) +(* *) +(* 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[] + ]);; + + diff --git a/main.ml b/main.ml new file mode 100644 index 0000000..8ee0bec --- /dev/null +++ b/main.ml @@ -0,0 +1,61 @@ +(* ========================================================================= *) +(* *) +(* Top Level File *) +(* *) +(* (c) Copyright, Muhammad Umair Siddique, Vincent Aravantinos, 2012 *) +(* Hardware Verification Group, *) +(* Concordia University *) +(* *) +(* Contact: *) +(* *) +(* 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. + +--------------------------------------------------------------------------*) + + diff --git a/make.ml b/make.ml new file mode 100644 index 0000000..fcdca26 --- /dev/null +++ b/make.ml @@ -0,0 +1 @@ +needs "main.ml";; diff --git a/resonator.ml b/resonator.ml new file mode 100644 index 0000000..3319014 --- /dev/null +++ b/resonator.ml @@ -0,0 +1,556 @@ +(* ========================================================================= *) +(* *) +(* Optical Resoantors *) +(* *) +(* (c) Copyright, Muhammad Umair Siddique, Vincent Aravantinos, 2012 *) +(* Hardware Verification Group, *) +(* Concordia University *) +(* *) +(* Contact: , *) +(* *) +(* 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)`, + REWRITE_TAC[FORALL_PAIR_THM]);; + + +(* 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''`, + MATCH_MP_TAC list_INDUCT + THEN REWRITE_TAC[optical_components_shift;FORALL_OPTICAL_COMPONENT_THM; + LET_PAIR] + THEN MESON_TAC[]);; + +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'`, + MATCH_MP_TAC list_INDUCT THEN + SIMP_TAC[ALL;optical_components_shift;LET_PAIR; + FORALL_OPTICAL_COMPONENT_THM;is_valid_optical_component]);; + +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]`, + REWRITE_TAC[round_trip;APPEND;optical_components_shift;LET_DEF; + LET_END_DEF;REVERSE]);; + +let HEAD_INDEX_ROUND_TRIP = prove + (`!i1 cs fs i2. + head_index (round_trip (i1,cs,fs,i2),fs) = head_index (cs,fs)`, + GEN_TAC THEN MATCH_MP_TAC list_INDUCT + THEN REWRITE_TAC[round_trip;APPEND;head_index;FORALL_FREE_SPACE_THM; + FORALL_OPTICAL_COMPONENT_THM]);; + +let LIST_POW = define + `LIST_POW l 0 = [] /\ + LIST_POW l (SUC n) = APPEND l (LIST_POW l n)`;; + +let ALL_LIST_POW = prove + (`!n l P. ALL P (LIST_POW l n) <=> n = 0 \/ ALL P l`, + INDUCT_TAC THEN ASM_REWRITE_TAC[LIST_POW;ALL;ALL_APPEND;NOT_SUC] + THEN ITAUT_TAC);; + +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)`, + MATCH_MP_TAC list_INDUCT + THEN SIMP_TAC[free_space_matrix;MAT2X2_ID;FORALL_OPTICAL_COMPONENT_THM;APPEND; + FORALL_FREE_SPACE_THM;system_composition;GSYM HEAD_INDEX_APPEND; + MATRIX_MUL_ASSOC]);; + +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 VALID_UNFOLD_RESONATOR = prove + (`!res. is_valid_resonator res ==> + !n. is_valid_optical_system (unfold_resonator res n)`, + REWRITE_TAC[FORALL_RESONATOR_THM;is_valid_resonator] + THEN REPEAT (INDUCT_TAC ORELSE STRIP_TAC) + THEN REWRITE_TAC [FORALL_OPTICAL_SYSTEM_THM;is_valid_optical_system; + unfold_resonator;LIST_POW;ALL;ALL_APPEND;is_valid_free_space;REAL_LE_REFL] + THEN MP_REWRITE_TAC HEAD_INDEX_VALID_OPTICAL_SYSTEM + THEN ASM_SIMP_TAC[is_valid_optical_system;ALL_LIST_POW;round_trip;ALL_APPEND; + TAUT `A /\ (B \/ A) <=> A`;ALL;is_valid_optical_component;LET_PAIR; + ALL_REVERSE;REWRITE_RULE[LET_PAIR] VALID_OPTICAL_COMPONENTS_SHIFT]);; + +let RESONATOR_MATRIX = prove + (`!n res. + system_composition (unfold_resonator res n) + = system_composition (unfold_resonator res 1) pow n`, + INDUCT_TAC THEN REWRITE_TAC[FORALL_RESONATOR_THM] + THENL [ + REWRITE_TAC[unfold_resonator;mat_pow;system_composition;free_space_matrix; + MAT2X2_MAT1;LIST_POW]; + POP_ASSUM (fun x -> REWRITE_TAC[GSYM x;MAT_POW_ALT]) + THEN REWRITE_TAC[unfold_resonator;LIST_POW;ONE;APPEND_NIL; + SYSTEM_COMPOSITION_APPEND] + THEN REPEAT GEN_TAC + THEN STRUCT_CASES_TAC (Pa.SPEC "n" num_CASES) + THEN REWRITE_TAC[LIST_POW;head_index] + THEN Pa.PARSE_IN_CONTEXT (STRUCT_CASES_TAC o C ISPEC list_CASES) "cs" + THEN REWRITE_TAC[ROUND_TRIP_NIL;APPEND;HEAD_INDEX_CONS_ALT] + THEN REWRITE_TAC[round_trip;APPEND] + THEN (REPEAT (REWRITE_TAC[PAIR_EQ] THEN + (MATCH_MP_TAC HEAD_INDEX_CONS_EQ_ALT ORELSE AP_TERM_TAC))) + ]);; + + +(* ------------------------------------------------------------------------- *) +(* 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)))`, + REWRITE_TAC[MAT2X2_DET;LET_DEF;LET_END_DEF] + THEN REPEAT (INDUCT_TAC ORELSE STRIP_TAC) THEN REPEAT (POP_ASSUM MP_TAC) + THEN SIMP_TAC[mat_pow;MAT2X2_MUL;MAT2X2_SCALAR_MUL;MAT2X2_EQ; + GSYM REAL_OF_NUM_SUC;GSYM MAT2X2_MAT1] + THEN ONCE_REWRITE_TAC[GSYM REAL_SUB_0] THEN REAL_REDUCE_TAC + THEN SIMP_TAC[SIN_0;GSYM REAL_NEG_MINUS1;SIN_NEG;SIN_ADD;COS_NEG] + THEN REAL_REDUCE_TAC THEN SIMP_TAC[REAL_MUL_LINV;SIN_ACS_NZ] + THEN SIMP_TAC[REAL_LT_IMP_LE;COS_ACS;SIN_ACS] THEN REAL_REDUCE_TAC + THEN SIMP_TAC + [REAL_ARITH `x + -- &1 * y + z = t <=> x = t + y - z`; + REAL_ARITH `-- &1 * x * y * z = --(x * y) * z`] + THEN CONV_TAC REAL_FIELD);; + + +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)))) `, + SUBGOAL_THEN` !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))) ` ASSUME_TAC THENL[SIMP_TAC[SYLVESTER_THEOREM];ALL_TAC] THEN POP_ASSUM MP_TAC THEN +LET_TAC THEN ASM_SIMP_TAC[]);; + + +let STABILITY_LEMMA = prove(` +! A B C D xi thetai. det (mat2x2 A B C D) = &1 /\ + -- &1 < (A + D) / &2 /\ (A + D) / &2 < &1 ==> + ?(Y:real^2). !n. abs ((mat2x2 A B C D pow n ** vector [xi; thetai])$1) <= Y$1 /\ + abs ((mat2x2 A B C D pow n ** vector [xi; thetai])$2) <= Y$2`, + +REPEAT STRIP_TAC THEN +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)) + + (abs (&1 / sin (acs ((A + D) / &2))) * abs B * abs thetai)* (&1) ; +(abs (&1 / sin (acs ((A + D) / &2))) * abs C * abs xi)* abs(&1) + +((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 +GEN_TAC THEN SUBGOAL_THEN `!N. mat2x2 A B C D pow N = + &1 / sin (acs ((A + D) / &2)) %% + mat2x2 (A * sin (&N * (acs ((A + D) / &2))) - sin ((&N - &1) * (acs ((A + D) / &2)))) + (B * sin (&N * (acs ((A + D) / &2)))) + (C * sin (&N * (acs ((A + D) / &2)))) + (D * sin (&N * (acs ((A + D) / &2))) - sin ((&N - &1) * (acs ((A + D) / &2)))) ` ASSUME_TAC +THENL[GEN_TAC THEN MATCH_MP_TAC SYLVESTER_THEOREM_ALT THEN +ASM_SIMP_TAC[];ALL_TAC] THEN +ONCE_ASM_REWRITE_TAC[] THEN +CONJ_TAC + +THENL[ + +SIMP_TAC[ MAT2X2_VECTOR_MUL; MAT2X2_SCALAR_MUL;VECTOR_2] THEN +MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC(` abs + ((&1 / sin (acs ((A + D) / &2)) * (A * sin (&n * (acs ((A + D) / &2))) - sin ((&n - &1) * (acs ((A + D) / &2))))) * + xi) + + abs((&1 / sin (acs ((A + D) / &2)) * B * sin (&n * (acs ((A + D) / &2)))) * thetai)`) THEN +SIMP_TAC[REAL_ABS_TRIANGLE] THEN MATCH_MP_TAC REAL_LE_ADD2 THEN +CONJ_TAC THENL[ +SIMP_TAC[REAL_SUB_LDISTRIB;REAL_SUB_RDISTRIB] THEN +SUBGOAL_THEN ` abs + ((&1 / sin (acs ((A + D) / &2)) * A * sin (&n * (acs ((A + D) / &2)))) * xi - + (&1 / sin (acs ((A + D) / &2)) * sin (&n * (acs ((A + D) / &2)) - &1 * (acs ((A + D) / &2)))) * xi) = +abs + ((&1 / sin (acs ((A + D) / &2)) * A * xi) * sin (&n * (acs ((A + D) / &2))) - + (((&1 / sin (acs ((A + D) / &2))) *xi)* sin (&n * (acs ((A + D) / &2)) - &1 * (acs ((A + D) / &2)))))` ASSUME_TAC THENL[ +REAL_ARITH_TAC; ALL_TAC] THEN +ONCE_ASM_REWRITE_TAC[] THEN +SIMP_TAC[REAL_FIELD `!(a:real) b. (b - a)= (--a + b)`] THEN +MATCH_MP_TAC REAL_LE_TRANS THEN +EXISTS_TAC(` abs + (--((&1 / sin (acs ((A + D) / &2)) * xi) * sin (--(&1 * (acs ((A + D) / &2))) + &n * (acs ((A + D) / &2))))) + + abs( (&1 / sin (acs ((A + D) / &2)) * A * xi) * sin (&n * (acs ((A + D) / &2)))) `) THEN +SIMP_TAC[REAL_ABS_TRIANGLE] THEN +SIMP_TAC[REAL_ABS_NEG;REAL_ABS_MUL] THEN +MATCH_MP_TAC REAL_LE_ADD2 THEN + +CONJ_TAC THENL[ +MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS] THEN + +CONJ_TAC THENL[ +SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN +MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] THEN + +SIMP_TAC[REAL_LE_LT;SIN_BOUND];ALL_TAC] THEN + +MATCH_MP_TAC REAL_LE_MUL2 THEN +CONJ_TAC THENL[ + +SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN +MATCH_MP_TAC REAL_LE_MUL2 THEN +SIMP_TAC[REAL_ABS_POS] THEN + +CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT]; ALL_TAC] THEN +CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT]; ALL_TAC] THEN + +SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN +MATCH_MP_TAC REAL_LE_MUL2 THEN +SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] THEN + +SIMP_TAC[REAL_ABS_POS;REAL_ABS_1;SIN_BOUND] THEN +SIMP_TAC[REAL_LE_LT]; ALL_TAC] THEN + +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 +THENL [REAL_ARITH_TAC;ALL_TAC] THEN +ONCE_ASM_REWRITE_TAC[] THEN SIMP_TAC[REAL_ABS_MUL] THEN + +MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS] THEN CONJ_TAC THENL[ +SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN +MATCH_MP_TAC REAL_LE_MUL2 THEN +SIMP_TAC[REAL_ABS_POS] +THEN CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN + CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN +SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN +MATCH_MP_TAC REAL_LE_MUL2 THEN +SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] THEN + +SIMP_TAC[SIN_BOUND] THEN SIMP_TAC[REAL_LE_LT]; ALL_TAC] THEN + + +SIMP_TAC[ MAT2X2_VECTOR_MUL; MAT2X2_SCALAR_MUL;VECTOR_2] + THEN MATCH_MP_TAC REAL_LE_TRANS THEN + EXISTS_TAC(` abs + ((&1 / sin (acs ((A + D) / &2)) * C * sin (&n * (acs ((A + D) / &2)))) * xi) + + abs((&1 / sin (acs ((A + D) / &2)) * (D * sin (&n * (acs ((A + D) / &2))) - sin ((&n - &1) * (acs ((A + D) / &2))))) * + thetai) `) THEN SIMP_TAC[REAL_ABS_TRIANGLE] THEN +MATCH_MP_TAC REAL_LE_ADD2 THEN +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 +THENL[REAL_ARITH_TAC;ALL_TAC] THEN ONCE_ASM_REWRITE_TAC[] THEN +SIMP_TAC[REAL_ABS_MUL] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN +SIMP_TAC[REAL_ABS_POS;SIN_BOUND;REAL_ABS_1] THEN +CONJ_TAC THENL[ +SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN +MATCH_MP_TAC REAL_LE_MUL2 THEN +SIMP_TAC[REAL_ABS_POS] THEN CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC] +THEN CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC] +THEN SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN +MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] +THEN SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN + +SIMP_TAC[REAL_SUB_LDISTRIB;REAL_SUB_RDISTRIB] THEN +SUBGOAL_THEN `abs + ((&1 / sin (acs ((A + D) / &2)) * D * sin (&n * (acs ((A + D) / &2)))) * thetai - + (&1 / sin (acs ((A + D) / &2)) * sin (&n * (acs ((A + D) / &2)) - &1 * (acs ((A + D) / &2)))) * thetai) = +abs + ((&1 / sin (acs ((A + D) / &2)) * D * thetai )*sin (&n * (acs ((A + D) / &2))) - + (&1 / sin (acs ((A + D) / &2)) * thetai) * sin (&n * (acs ((A + D) / &2)) - &1 * (acs ((A + D) / &2)))) ` ASSUME_TAC THENL[ +REAL_ARITH_TAC;ALL_TAC] THEN ONCE_ASM_REWRITE_TAC[] THEN +SIMP_TAC[REAL_FIELD `!(a:real) b. (b - a)= (--a + b)`] THEN +MATCH_MP_TAC REAL_LE_TRANS THEN +EXISTS_TAC(` abs + (--((&1 / sin (acs ((A + D) / &2)) * thetai) * sin (--(&1 * (acs ((A + D) / &2))) + &n * (acs ((A + D) / &2))))) + + abs( (&1 / sin (acs ((A + D) / &2)) * D * thetai) * sin (&n * (acs ((A + D) / &2)))) `) +THEN SIMP_TAC[REAL_ABS_TRIANGLE] THEN SIMP_TAC[REAL_ABS_NEG;REAL_ABS_MUL] +THEN MATCH_MP_TAC REAL_LE_ADD2 THEN +CONJ_TAC THENL[MATCH_MP_TAC REAL_LE_MUL2 THEN +SIMP_TAC[REAL_ABS_POS;REAL_ABS_1;SIN_BOUND] THEN +CONJ_TAC THENL[ SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN +MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] THEN +SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN +MATCH_MP_TAC REAL_LE_MUL2 THEN +SIMP_TAC[REAL_ABS_POS;REAL_ABS_1;SIN_BOUND] THEN +CONJ_TAC THENL[SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b`] THEN +MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS] THEN +CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN +CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN +SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN +MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] THEN +SIMP_TAC[REAL_LE_LT]);; + + +let STABILITY_LEMMA_GENERAL = prove(`! (M:real^2^2) xi thetai. det (M) = &1 /\ + -- &1 < (M$1$1 + M$2$2) / &2 /\ (M$1$1 + M$2$2) / &2 < &1 ==> + ?(Y:real^2). !n. abs ((M pow n ** vector [xi; thetai])$1) <= Y$1 /\ + abs ((M pow n ** vector [xi; thetai])$2) <= Y$2`, + REWRITE_TAC[FORALL_MATRIX_2X2] THEN REPEAT STRIP_TAC THEN +MATCH_MP_TAC STABILITY_LEMMA THEN REPEAT(POP_ASSUM MP_TAC) THEN +SIMP_TAC [mat2x2;CART_EQ;VECTOR_2;DIMINDEX_2;FORALL_2;DOT_2;SUM_2]);; + + +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`, + +GEN_TAC THEN REPEAT (LET_TAC) THEN REPEAT STRIP_TAC THEN +REPEAT STRIP_TAC THEN REWRITE_TAC[is_stable_resonator] THEN GEN_TAC THEN +SUBGOAL_THEN ` (?Y:real^2. !n. abs ((M pow n ** vector [FST(fst_single_ray r);SND(fst_single_ray r) ])$1) +<= Y$1 /\ abs (((M:real^2^2) pow n ** vector [FST(fst_single_ray r);SND(fst_single_ray r) ])$2) <= Y$2)` +ASSUME_TAC THENL[MP_REWRITE_TAC STABILITY_LEMMA_GENERAL THEN ASM_SIMP_TAC[];ALL_TAC] THEN +POP_ASSUM MP_TAC THEN STRIP_TAC THEN +EXISTS_TAC(`((Y:real^2)$1):real`) THEN EXISTS_TAC(`((Y:real^2)$2):real`) THEN +REPEAT STRIP_TAC THEN LET_TAC THEN +SUBGOAL_THEN `(let (xi,thetai),(y1,theta1),rs = r in + let y',theta' = last_single_ray r in + vector [y'; 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_LEMMA_SYM = prove (` ! A B C D xi thetai. det (mat2x2 A B C D) = &1 /\ + -- &1 < (A + D) / &2 /\ (A + D) / &2 < &1 ==> + ?(Y:real^2). !n. abs (((mat2x2 A B C D pow 2)pow n ** vector [xi; thetai])$1) <= Y$1 /\ + abs (((mat2x2 A B C D pow 2) pow n ** vector [xi; thetai])$2) <= Y$2`, + +REWRITE_TAC[MAT2X2_POW2_POW] THEN +REPEAT STRIP_TAC THEN +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)) + + (abs (&1 / sin (acs ((A + D) / &2))) * abs B * abs thetai)* (&1) ; +(abs (&1 / sin (acs ((A + D) / &2))) * abs C * abs xi)* abs(&1) + +((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 +GEN_TAC THEN SUBGOAL_THEN `!N. mat2x2 A B C D pow (2*N) = + &1 / sin (acs ((A + D) / &2)) %% + mat2x2 (A * sin (&(2*N) * (acs ((A + D) / &2))) - sin ((&(2*N) - &1) * (acs ((A + D) / &2)))) + (B * sin (&(2*N) * (acs ((A + D) / &2)))) + (C * sin (&(2*N) * (acs ((A + D) / &2)))) + (D * sin (&(2*N) * (acs ((A + D) / &2))) - sin ((&(2*N) - &1) * (acs ((A + D) / &2)))) ` ASSUME_TAC +THENL[GEN_TAC THEN MATCH_MP_TAC SYLVESTER_THEOREM_ALT THEN +ASM_SIMP_TAC[];ALL_TAC] THEN +ONCE_ASM_REWRITE_TAC[] THEN CONJ_TAC +THENL[SIMP_TAC[ MAT2X2_VECTOR_MUL; MAT2X2_SCALAR_MUL;VECTOR_2] THEN +MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC(` abs + ((&1 / sin (acs ((A + D) / &2)) * (A * sin (&(2*n) * (acs ((A + D) / &2))) - sin ((&(2*n) - &1) * (acs ((A + D) / &2))))) * + xi) + + abs((&1 / sin (acs ((A + D) / &2)) * B * sin (&(2*n) * (acs ((A + D) / &2)))) * thetai)`) THEN +SIMP_TAC[REAL_ABS_TRIANGLE] THEN MATCH_MP_TAC REAL_LE_ADD2 THEN +CONJ_TAC THENL[ +SIMP_TAC[REAL_SUB_LDISTRIB;REAL_SUB_RDISTRIB] THEN +SUBGOAL_THEN ` abs + ((&1 / sin (acs ((A + D) / &2)) * A * sin (&(2*n) * (acs ((A + D) / &2)))) * xi - + (&1 / sin (acs ((A + D) / &2)) * sin (&(2*n) * (acs ((A + D) / &2)) - &1 * (acs ((A + D) / &2)))) * xi) = +abs + ((&1 / sin (acs ((A + D) / &2)) * A * xi) * sin (&(2*n) * (acs ((A + D) / &2))) - + (((&1 / sin (acs ((A + D) / &2))) *xi)* sin (&(2*n) * (acs ((A + D) / &2)) - &1 * (acs ((A + D) / &2)))))` ASSUME_TAC THENL[ +REAL_ARITH_TAC; ALL_TAC] THEN +ONCE_ASM_REWRITE_TAC[] THEN +SIMP_TAC[REAL_FIELD `!(a:real) b. (b - a)= (--a + b)`] THEN +MATCH_MP_TAC REAL_LE_TRANS THEN +EXISTS_TAC(` abs + (--((&1 / sin (acs ((A + D) / &2)) * xi) * sin (--(&1 * (acs ((A + D) / &2))) + &(2*n) * (acs ((A + D) / &2))))) + + abs( (&1 / sin (acs ((A + D) / &2)) * A * xi) * sin (&(2*n) * (acs ((A + D) / &2)))) `) THEN +SIMP_TAC[REAL_ABS_TRIANGLE] THEN +SIMP_TAC[REAL_ABS_NEG;REAL_ABS_MUL] THEN +MATCH_MP_TAC REAL_LE_ADD2 THEN + +CONJ_TAC THENL[ +MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS] THEN + +CONJ_TAC THENL[ +SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN +MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] THEN + +SIMP_TAC[REAL_LE_LT;SIN_BOUND];ALL_TAC] THEN + +MATCH_MP_TAC REAL_LE_MUL2 THEN +CONJ_TAC THENL[ + +SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN +MATCH_MP_TAC REAL_LE_MUL2 THEN +SIMP_TAC[REAL_ABS_POS] THEN + +CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT]; ALL_TAC] THEN +CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT]; ALL_TAC] THEN + +SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN +MATCH_MP_TAC REAL_LE_MUL2 THEN +SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] THEN + +SIMP_TAC[REAL_ABS_POS;REAL_ABS_1;SIN_BOUND] THEN +SIMP_TAC[REAL_LE_LT]; ALL_TAC] THEN + +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 +THENL [REAL_ARITH_TAC;ALL_TAC] THEN +ONCE_ASM_REWRITE_TAC[] THEN SIMP_TAC[REAL_ABS_MUL] THEN + +MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS] THEN CONJ_TAC THENL[ +SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN +MATCH_MP_TAC REAL_LE_MUL2 THEN +SIMP_TAC[REAL_ABS_POS] +THEN CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN + CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN +SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN +MATCH_MP_TAC REAL_LE_MUL2 THEN +SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] THEN + +SIMP_TAC[SIN_BOUND] THEN SIMP_TAC[REAL_LE_LT]; ALL_TAC] THEN + + +SIMP_TAC[ MAT2X2_VECTOR_MUL; MAT2X2_SCALAR_MUL;VECTOR_2] + THEN MATCH_MP_TAC REAL_LE_TRANS THEN + EXISTS_TAC(` abs + ((&1 / sin (acs ((A + D) / &2)) * C * sin (&(2*n) * (acs ((A + D) / &2)))) * xi) + + abs((&1 / sin (acs ((A + D) / &2)) * (D * sin (&(2*n) * (acs ((A + D) / &2))) - sin ((&(2*n) - &1) * (acs ((A + D) / &2))))) * + thetai) `) THEN SIMP_TAC[REAL_ABS_TRIANGLE] THEN +MATCH_MP_TAC REAL_LE_ADD2 THEN +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 +THENL[REAL_ARITH_TAC;ALL_TAC] THEN ONCE_ASM_REWRITE_TAC[] THEN +SIMP_TAC[REAL_ABS_MUL] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN +SIMP_TAC[REAL_ABS_POS;SIN_BOUND;REAL_ABS_1] THEN +CONJ_TAC THENL[ +SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN +MATCH_MP_TAC REAL_LE_MUL2 THEN +SIMP_TAC[REAL_ABS_POS] THEN CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC] +THEN CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC] +THEN SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN +MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] +THEN SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN + +SIMP_TAC[REAL_SUB_LDISTRIB;REAL_SUB_RDISTRIB] THEN +SUBGOAL_THEN `abs + ((&1 / sin (acs ((A + D) / &2)) * D * sin (&(2*n) * (acs ((A + D) / &2)))) * thetai - + (&1 / sin (acs ((A + D) / &2)) * sin (&(2*n) * (acs ((A + D) / &2)) - &1 * (acs ((A + D) / &2)))) * thetai) = +abs + ((&1 / sin (acs ((A + D) / &2)) * D * thetai )*sin (&(2*n) * (acs ((A + D) / &2))) - + (&1 / sin (acs ((A + D) / &2)) * thetai) * sin (&(2*n) * (acs ((A + D) / &2)) - &1 * (acs ((A + D) / &2)))) ` ASSUME_TAC THENL[ +REAL_ARITH_TAC;ALL_TAC] THEN ONCE_ASM_REWRITE_TAC[] THEN +SIMP_TAC[REAL_FIELD `!(a:real) b. (b - a)= (--a + b)`] THEN +MATCH_MP_TAC REAL_LE_TRANS THEN +EXISTS_TAC(` abs + (--((&1 / sin (acs ((A + D) / &2)) * thetai) * sin (--(&1 * (acs ((A + D) / &2))) + &(2*n) * (acs ((A + D) / &2))))) + + abs( (&1 / sin (acs ((A + D) / &2)) * D * thetai) * sin (&(2*n) * (acs ((A + D) / &2)))) `) +THEN SIMP_TAC[REAL_ABS_TRIANGLE] THEN SIMP_TAC[REAL_ABS_NEG;REAL_ABS_MUL] +THEN MATCH_MP_TAC REAL_LE_ADD2 THEN +CONJ_TAC THENL[MATCH_MP_TAC REAL_LE_MUL2 THEN +SIMP_TAC[REAL_ABS_POS;REAL_ABS_1;SIN_BOUND] THEN +CONJ_TAC THENL[ SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN +MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] THEN +SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN +MATCH_MP_TAC REAL_LE_MUL2 THEN +SIMP_TAC[REAL_ABS_POS;REAL_ABS_1;SIN_BOUND] THEN +CONJ_TAC THENL[SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b`] THEN +MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS] THEN +CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN +CONJ_TAC THENL[SIMP_TAC[REAL_LE_LT];ALL_TAC] THEN +SIMP_TAC[ REAL_FIELD`! a b. &0 <= a*b <=> &0 * &0 <= a*b `] THEN +MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS;REAL_LE_LT];ALL_TAC] THEN +SIMP_TAC[REAL_LE_LT]);; + +let STABILITY_LEMMA_GENERAL_SYM = prove(`! (M:real^2^2) xi thetai. det (M) = &1 /\ + -- &1 < (M$1$1 + M$2$2) / &2 /\ (M$1$1 + M$2$2) / &2 < &1 ==> + ?(Y:real^2). !n. abs (((M pow 2) pow n ** vector [xi; thetai])$1) <= Y$1 /\ + abs (((M pow 2) pow n ** vector [xi; thetai])$2) <= Y$2`, + REWRITE_TAC[FORALL_MATRIX_2X2] THEN REPEAT STRIP_TAC THEN +MATCH_MP_TAC STABILITY_LEMMA_SYM THEN REPEAT(POP_ASSUM MP_TAC) THEN +SIMP_TAC [mat2x2;CART_EQ;VECTOR_2;DIMINDEX_2;FORALL_2;DOT_2;SUM_2]);; + +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`, + +GEN_TAC THEN ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN +POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN +REPEAT STRIP_TAC THEN REWRITE_TAC[is_stable_resonator] THEN +GEN_TAC THEN +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 /\ + 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[ +MP_REWRITE_TAC STABILITY_LEMMA_GENERAL_SYM THEN ASM_SIMP_TAC[]; ALL_TAC] THEN +POP_ASSUM MP_TAC THEN STRIP_TAC THEN EXISTS_TAC(`((Y:real^2)$1):real`) THEN +EXISTS_TAC(`((Y:real^2)$2):real`) THEN REPEAT STRIP_TAC THEN +LET_TAC THEN SUBGOAL_THEN `(let (xi,thetai),(y1,theta1),rs = r in + let y',theta' = last_single_ray r in + vector [y'; 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[]);; + + diff --git a/utils.ml b/utils.ml new file mode 100644 index 0000000..5bad5fa --- /dev/null +++ b/utils.ml @@ -0,0 +1,177 @@ +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);; + diff --git a/z_resonator.ml b/z_resonator.ml new file mode 100644 index 0000000..430eec4 --- /dev/null +++ b/z_resonator.ml @@ -0,0 +1,124 @@ +(* ========================================================================= *) +(* *) +(* Z-Shaped Resonator *) +(* *) +(* (c) Copyright, Muhammad Umair Siddique, Vincent Aravantinos, 2012 *) +(* Hardware Verification Group, *) +(* Concordia University *) +(* *) +(* Contact: , *) +(* *) +(* 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))`]);; + + -- 1.7.1