***********************************************************************************************************************
**********************************************Running Examples*********************************************************
***********************************************************************************************************************

Example 1 : TPHOL2009 [1]

call_mathematica "tan ((&5 / (&10 pow  4)) * kappa) =((sqrt  ((((((&2 * pi) * (&10 pow  4)) pow  2) * ((&3 / &2) pow  2)) - (kappa pow  2)) -   ((((&2 * pi) * (&10 pow  4)) pow  2) * ((&145 / &100) pow  2)))+ sqrt ((((((&2 * pi) * (&10 pow  4)) pow  2) * ((&3 / &2) pow  2)) - (kappa pow  2)) - ((((&2 * pi) * (&10 pow  4)) pow  2) * ((&14 / &10) pow  2)))) / ((kappa * (&1 - ((sqrt  ((((((&2 * pi) * (&10 pow  4)) pow  2) * ((&3 / &2) pow  2)) - (kappa pow  2)) -   ((((&2 * pi) * (&10 pow  4)) pow  2) * ((&145 / &100) pow  2)))* sqrt ((((((&2 * pi) * (&10 pow  4)) pow  2) * ((&3 / &2) pow  2)) - (kappa pow  2)) - ((((&2 * pi) * (&10 pow  4)) pow  2) * ((&14 / &10) pow  2))))/ (kappa pow  2))))))" "FindRoot";;


************************************************************************************************************************
************************************************************************************************************************

DoForm Example [2] : 

Before running this example load cvector.ml in the HOL Light session. 
 
Type : 
  needs "Multivariate/make_complex.ml";;
  needs "cvector.ml" ;; [3]

Then type:

call_mathematica "(((vector [(Cx (&1)); (Cx (&0)); (Cx (&0))]) ccross ((vector [(Cx (&0));(a * (cexp ((-- ii) * (Cx ((k0 * n1) * (&0 * (cos thetai) + z * (sin thetai)) + (omega * t)))))); (Cx (&0))]) +   (vector [(Cx (&0)); ((((Cx(((n2 * (cos thetai)) - (n1 * (cos (asn (n1 /  (n2 * (sin thetai))))))) / ((n2 * (cos thetai)) + (n1 * (cos (asn (n1 / (n2 * (sin thetai)))))) ) )) * a) * (cexp ((--ii) * (Cx ((k0 * n1) * (&0 * (cos thetai) + z * (sin thetai)) + (omega * t))))))) ;   (Cx (&0))]))) = ((vector [(Cx (&1)); (Cx (&0)); (Cx (&0))]) ccross (vector  [(Cx (&0)); ((Cx (((&2 * (n2 * (cos thetai))) / ((n2 * (cos thetai)) + (n1 * (cos (asn (n1 / (n2 * (sin thetai)))))) ) ) )) * (a * (cexp ((-- ii) * (Cx ((k0 * n1) * (&0 * (cos thetai) + z * (sin thetai)) + (omega * t)))))) ) ; (Cx (&0))]))) and ((vector [(Cx (&1)); (Cx (&0)); (Cx (&0))]) ccross ((vector  [(((a * Cx (n1 / eta0)) * (ccos (Cx thetai))) *  (cexp ((-- ii) * (Cx ((k0 * n1) * (&0 * (cos thetai) + z * (sin thetai)) + (omega * t))))));  (Cx (&0)); (((-- a) * Cx (n1 / eta0)) * (csin (Cx thetai) *  (cexp ((-- ii) * (Cx ((k0 * n1) * (&0 * (cos thetai) + z * (sin thetai)) + (omega * t)))))))]) +   (vector [(( (Cx(((n2 * (cos thetai)) - (n1 * (cos (asn (n1 /  (n2 * (sin thetai))))))) / ((n2 * (cos thetai)) + (n1 * (cos (asn (n1 / (n2 * (sin thetai)))))) ) ))  * (((-- a) * Cx (n1 / eta0)) * (ccos (Cx thetai)))) *  (cexp ((-- ii) * (Cx ((k0 * n1) * (&0 * (cos thetai) + z * (sin thetai)) + (omega * t)))))); (Cx (&0)); (( (Cx(((n2 * (cos thetai)) - (n1 * (cos (asn (n1 /  (n2 * (sin thetai))))))) / ((n2 * (cos thetai)) + (n1 * (cos (asn (n1 / (n2 * (sin thetai)))))) ) ))  *    (((-- a) * Cx (n1 / eta0)) * (csin (Cx thetai)))) *  (cexp ((-- ii) * (Cx ((k0 * n1) * (&0 * (cos thetai) + z * (sin thetai)) + (omega * t))))))])) =  (vector [(Cx (&1)); (Cx (&0)); (Cx (&0))]) ccross (vector [(( (Cx(((&2 * n2) * (cos (asn (n1 /  (n2 * (sin thetai)))))) / ((n2 * (cos thetai)) + (n1 * (cos (asn (n1 / (n2 * (sin thetai)))))) ) ))  *    ((a * Cx (n2 / eta0)) * (ccos (Cx thetai)))) *  ( cexp ((-- ii) * (Cx ((k0 * n1) * (&0 * (cos  thetai) + z * (sin thetai)) + (omega * t))))));  (Cx (&0)); (( (Cx(((&2 * n2) * (sin thetai)) / ((n2 * (cos thetai)) + (n1 * (cos (asn (n1 / (n2 * (sin thetai)))))) ) ))  *    (((-- a) * Cx (n1 / eta0)) * (ccos (Cx thetai)))) *  ( cexp ((-- ii) * (Cx ((k0 * n1) * (&0 * (cos thetai) + z * (sin thetai)) + (omega * t))))))]) )" "FullSimplify";;

***********************************************************************************************************************
***********************************************************************************************************************

Other Examples: 

****************Mathematica functions "FullSimplify" and "Simplify"***************************************************

Differentiation:  
call_mathematica "diff ((sin x + x - (cos x) + (x pow 2)), x)" "FullSimplify";;  

Definite Integrale:
call_mathematica "int ((x pow 2 + x - &1), x)" "Simplify";; 

Bounded Integrale:
call_mathematica "real_integral (real_interval [&1,&10]) (\x. (x + &1))" "FullSimplify";;

Eigenvectors computation of matrix 2x2: 
call_mathematica "eigenvect (mat2x2 a b c d)" "Simplify";;

Eigenvalues computation of matrix 2x2:
call_mathematica "eigenval (mat2x2 a  b  c  d )" "Simplify";;

Relational operators: 
call_mathematica "(x pow 2) + x + &1 > (x pow 2) + x + &2 " "Simplify";;

Finite summation: 
call_mathematica "sigma ((&1 + x), x, &1 , &10)" "FullSimplify";;

call_mathematica "eigen_pair (mat2x2 a b c d) (x,a)" "FullSimplify";;
*****************************Mathematica function "Solve"*********************************************************

Solve equation: 
call_mathematica "x pow 2 - &1 = &0" "Solve";;


*****************************Mathematica function "Factor"*********************************************************

Factorization: 	
call_mathematica "x pow 3 + &2 * (x pow 2) + x " "Factor";;

*******************************************************************************************************************
*******************************************************************************************************************

Matrix examples : 
Before running these examples type in the HOL Light session: 

  needs "Multivariate/make_complex.ml";; 

Multiplication matrix-vector: 
call_mathematica "(mat4x4 a b c d l f h j k l m n p q r s) ** vector[x;y;z;t]" "FullSimplify";;
call_mathematica "(mat3x3 a b c d l f h j k) ** vector[x;y;z]" "FullSimplify";;
call_mathematica "(mat2x2 a b c d ) ** vector[x;y]" "FullSimplify";;

Multiplication scalar-vector: 
call_mathematica "&5 % (vector[a;b;c;d]) " "FullSimplify";;
call_mathematica "&6 % (vector[a;b;c]) " "FullSimplify";;
call_mathematica "&10 % (vector[a;b]) " "FullSimplify";;

Matrix addition:
call_mathematica "(mat4x4 a b c d l f h j k l m n p q r s) + (mat4x4 a b c d l f h j k l m n p q r s) " "FullSimplify";;
call_mathematica "(mat3x3 a b c d l f h j k) + (mat3x3 a b c d l f h j k) " "FullSimplify";;
call_mathematica "(mat2x2 a b c d ) + (mat2x2 a b c d ) " "FullSimplify";;

Eigen_pai:
call_mathematica "eigen_pair (mat2x2 a b c d) (x,a)" "FullSimplify";;

Inverse :
call_mathematica "inverse (mat3x3 a b c d l f h j k )" "FullSimplify";;
call_mathematica "inverse (mat2x2 a b c d)" "FullSimplify";;

Determinant: 
call_mathematica "det (mat3x3 a b c d l f h j k)" "FullSimplify";;
call_mathematica "det (mat2x2 a b c d )" "FullSimplify";;

MatrixPower:
call_mathematica " (mat4x4 a b c d l f h j k l m n p q r s) pow 2" "FullSimplify";;
call_mathematica " (mat3x3 a b c d l f h j k) pow 4" "FullSimplify";;
call_mathematica " (mat2x2 a b c d ) pow 6" "FullSimplify";;





**************************************************************************************************************************
**************************************************************************************************************************


References: 

[1] O. Hasan, S.K. Afshar, and S. Tahar: Formal Analysis of Optical Waveguides in HOL S. Berghofer et al. (Eds.), Theorem Proving in Higher-Order Logics, Lecture Notes in Computer Science 5674, Springer Verlag, 2009, pp. 228-243. [Proc. International Conference on Theorem Proving in Higher-Order Logics (TPHOLs'09), Munich, Germany, August 2009.]

[2] S. K. Afshar, U. Siddique, M. Y. Mahmoud, V. Aravantinos, O. Seddiki, O. Hasan, and S. Tahar: Formal Analysi of  Optical Systems [In Mathematics in Computer Science, 10 (1), Springer, 2014].

[3] A HOL-Light Library for Vectors of Complex Numbers, https://hvg.ece.concordia.ca/code/hol-light/complex-vectors/.