(* ========================================================================= *)
(*                                                                           *)
(*                        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]);;