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

--------------------------------------------------------------------------*)