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