1 (* ========================================================================= *)
3 (* Frequent Component Library *)
5 (* (c) Copyright, Muhammad Umair Siddique, Vincent Aravantinos, 2012 *)
6 (* Hardware Verification Group, *)
7 (* Concordia University *)
9 (* Contact: <muh_sidd@ece.concordia.ca>, <vincent@ece.concordia.ca> *)
11 (* Last update: Feb 16, 2012 *)
13 (* ========================================================================= *)
15 needs "geometrical_optics.ml";;
17 (*-----THIN LENS------------*)
19 let thin_lens_mat = new_definition
20 `thin_lens_mat R1 R2 (n1:real) (n2:real) =
21 mat2x2 (&1) (&0) (((n2 - n1)/n1) *(&1/R2 - &1/R1)) (&1) `;;
23 let thin_lens = new_definition
24 `thin_lens R1 R2 n1 n2: optical_system =
25 ([(n1,&0),(spherical R1),transmitted;
26 (n2,&0),(spherical R2),transmitted],n1,&0)`;;
28 let VALID_OPTICAL_SYSTEM_TAC x =
29 SIMP_TAC[x;is_valid_optical_system;is_valid_optical_component;ALL;
30 is_valid_free_space;is_valid_interface]
31 THEN CONV_TAC REAL_FIELD;;
33 let VALID_THIN_LENS = prove
35 ~(R1= &0) /\ ~(R2= &0) /\ &0 < n1 /\ &0 < n2 ==>
36 is_valid_optical_system (thin_lens R1 R2 n1 n2)`,
37 VALID_OPTICAL_SYSTEM_TAC thin_lens);;
39 let THIN_LENS_THIN_LENS_MAT = prove
41 ~(R1 = &0) /\ ~(R2 = &0) /\ &0 < n1 /\ &0 < n2 ==>
42 system_composition (thin_lens R1 R2 n1 n2) = thin_lens_mat R1 R2 n1 n2`,
43 REWRITE_TAC[system_composition;head_index;interface_matrix;free_space_matrix;
44 thin_lens_mat;thin_lens;MAT2X2_MUL;MAT2X2_EQ]
45 THEN CONV_TAC REAL_FIELD);;
47 let THIN_LENS_MATRIX = prove
49 ~(R1= &0) /\ ~(R2= &0) /\ &0 < n1 /\ &0 < n2 ==>
50 !ray. is_valid_ray_in_system ray (thin_lens R1 R2 n1 n2) ==>
51 let ((y0,theta0),(y1,theta1),rs) = ray in
52 let (y_n,theta_n) = last_single_ray ray in
53 vector [y_n;theta_n] = thin_lens_mat R1 R2 n1 n2 ** vector [y0;theta0]`,
54 SIMP_TAC[GSYM THIN_LENS_THIN_LENS_MAT] THEN REPEAT STRIP_TAC
55 THEN MATCH_MP_TAC SYSTEM_MATRIX THEN ASM_SIMP_TAC[VALID_THIN_LENS]);;
57 (*------------------THICK LENS---------------------*)
58 let thick_lens_mat = new_definition
59 `thick_lens_mat R1 R2 (n1:real) (n2:real) d =
60 mat2x2 (&1 + d*(n1/(n2*R1) - &1/R1)) (d * n1 / n2)
61 (--(((n1 - n2)*(d*(n1-n2) + n2*(R1-R2)))/(n1*n2*R1*R2)))
62 ( &1 + d*(&1/R2 - n1/(n2*R2))) `;;
64 let thick_lens = new_definition
65 `thick_lens R1 R2 n1 n2 d: optical_system =
66 ([(n1,&0),(spherical R1),transmitted;
67 (n2,d),(spherical R2),transmitted],n1,&0)`;;
70 let VALID_THICK_LENS = prove
72 ~(R1= &0) /\ ~(R2= &0) /\ &0 < n1 /\ &0 < n2 /\ &0 <= d ==>
73 is_valid_optical_system (thick_lens R1 R2 n1 n2 d)`,
74 VALID_OPTICAL_SYSTEM_TAC thick_lens);;
76 let THICK_LENS_THICK_LENS_MAT = prove
78 ~(R1 = &0) /\ ~(R2 = &0) /\ &0 < n1 /\ &0 < n2 /\ &0 <= d ==>
79 system_composition (thick_lens R1 R2 n1 n2 d) = thick_lens_mat R1 R2 n1 n2 d`,
80 REWRITE_TAC[system_composition;head_index;interface_matrix;free_space_matrix;
81 thick_lens_mat;thick_lens;MAT2X2_MUL;MAT2X2_EQ]
82 THEN CONV_TAC REAL_FIELD);;
84 let THICK_LENS_MATRIX = prove
86 ~(R1= &0) /\ ~(R2= &0) /\ &0 < n1 /\ &0 < n2 /\ &0 <= d ==>
87 !ray. is_valid_ray_in_system ray (thick_lens R1 R2 n1 n2 d) ==>
88 let ((y0,theta0),(y1,theta1),rs) = ray in
89 let (y_n,theta_n) = last_single_ray ray in
90 vector [y_n;theta_n] = thick_lens_mat R1 R2 n1 n2 d ** vector [y0;theta0]`,
91 SIMP_TAC[GSYM THICK_LENS_THICK_LENS_MAT] THEN REPEAT STRIP_TAC
92 THEN MATCH_MP_TAC SYSTEM_MATRIX THEN ASM_SIMP_TAC[VALID_THICK_LENS]);;
94 (*-----------DIELECTRIC SLAB---------------*)
96 let slab_mat = new_definition
97 `slab_mat (n1:real) (n2:real) d =
98 mat2x2 (&1) (d*(n1/n2)) (&0) (&1) `;;
100 let slab = new_definition
101 `slab n1 n2 d: optical_system =
102 ([(n1,&0),(plane),transmitted;
103 (n2,d),(plane),transmitted],n1,&0)`;;
106 let VALID_SLAB = prove
108 &0 < n1 /\ &0 < n2 /\ &0 < d ==>
109 is_valid_optical_system (slab n1 n2 d)`,
110 VALID_OPTICAL_SYSTEM_TAC slab);;
112 let SLAB_SLAB_MAT = prove
114 &0 < n1 /\ &0 < n2 /\ &0 < d ==>
115 system_composition (slab n1 n2 d) = (slab_mat n1 n2 d)`,
116 REWRITE_TAC[system_composition;head_index;interface_matrix;free_space_matrix;
117 slab_mat;slab;MAT2X2_MUL;MAT2X2_EQ]
118 THEN CONV_TAC REAL_FIELD);;
120 let SLAB_MATRIX = prove
122 &0 < n1 /\ &0 < n2 /\ &0 < d ==>
123 !ray. is_valid_ray_in_system ray (slab n1 n2 d) ==>
124 let ((y0,theta0),(y1,theta1),rs) = ray in
125 let (y_n,theta_n) = last_single_ray ray in
126 vector [y_n;theta_n] = slab_mat n1 n2 d ** vector [y0;theta0]`,
127 SIMP_TAC[GSYM SLAB_SLAB_MAT] THEN REPEAT STRIP_TAC
128 THEN MATCH_MP_TAC SYSTEM_MATRIX THEN ASM_SIMP_TAC[VALID_SLAB]);;