component_library.ml

   1 (* ========================================================================= *)
   2 (*                                                                           *)
   3 (*                        Frequent Component Library                         *)
   4 (*                                                                           *)
   5 (*        (c) Copyright, Muhammad Umair Siddique, Vincent Aravantinos, 2012  *)
   6 (*                       Hardware Verification Group,                        *)
   7 (*                       Concordia University                                *)
   8 (*                                                                           *)
   9 (*     Contact: <muh_sidd@ece.concordia.ca>, <vincent@ece.concordia.ca>      *)
  10 (*                                                                           *)
  11 (* Last update: Feb 16, 2012                                                 *)
  12 (*                                                                           *)
  13 (* ========================================================================= *)
  14
  15 needs "geometrical_optics.ml";;
  16
  17 (*-----THIN LENS------------*)
  18
  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) `;;
  22
  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)`;;
  27
  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;;
  32
  33 let VALID_THIN_LENS = prove
  34   (`!R1 R2 n1 n2.
  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);;
  38
  39 let THIN_LENS_THIN_LENS_MAT = prove
  40   (`!R1 R2 n1 n2.
  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);;
  46
  47 let THIN_LENS_MATRIX = prove
  48   (`!R1 R2 n1 n2.
  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]);;
  56
  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)))   `;;
  63
  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)`;;
  68
  69
  70 let VALID_THICK_LENS = prove
  71   (`!R1 R2 n1 n2.
  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);;
  75
  76 let THICK_LENS_THICK_LENS_MAT = prove
  77   (`!R1 R2 n1 n2 d.
  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);;
  83
  84 let THICK_LENS_MATRIX = prove
  85   (`!R1 R2 n1 n2.
  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]);;
  93
  94 (*-----------DIELECTRIC SLAB---------------*)
  95
  96 let slab_mat = new_definition
  97   `slab_mat (n1:real) (n2:real) d =
  98      mat2x2 (&1) (d*(n1/n2)) (&0) (&1) `;;
  99
 100 let slab = new_definition
 101   `slab n1 n2 d: optical_system =
 102     ([(n1,&0),(plane),transmitted;
 103       (n2,d),(plane),transmitted],n1,&0)`;;
 104
 105
 106 let VALID_SLAB = prove
 107   (`!n1 n2 d.
 108     &0 < n1 /\ &0 < n2 /\   &0 < d ==>
 109       is_valid_optical_system (slab n1 n2 d)`,
 110   VALID_OPTICAL_SYSTEM_TAC slab);;
 111
 112 let SLAB_SLAB_MAT = prove
 113   (` !n1 n2 d.
 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);;
 119
 120 let SLAB_MATRIX = prove
 121   (`!n1 n2 d.
 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]);;
 129
 130