(* ========================================================================= *)
(* File Name: CSC.ml	       	                                     *)
(*---------------------------------------------------------------------------*)
(* Description: Formal Verification of Tumor Growth Model                    *)
(*                                                                           *)
(*                                                                           *)
(*     (c) Author :  Adnan Rashid*			                     *)
(*      Co-Author :  Umair Siddique**					     *)
(*                                                                           *)
(* 	   *System Analyis & Verification (SAVe) LAB                  	     *)
(*          School of Electrical Engineering and Computer Sciences           *)
(*          National University of Sciences and Technology (NUST)            *)
(*                     Islamabad, Pakistan                                   *)
(*                                                                	     *)
(*        **Hardware Verification Group                                      *)
(*          Department of Electrical and Computer Engineering                *)
(*                Concordia University, Montreal, Canada                     *)
(*                                                                           *)
(*     Contact: *<adnan.rashid@seecs.edu.pk>,                                *)
(*              ** <muh_sidd@ece.concordia.ca>                               *)
(*                                                                           *)
(* NOTE: This Script is written in HOL Light		               	     *)
(*                                                                           *)
(* ========================================================================= *)

(* ==========================================================================*)
(*	    This file needs Formalization.ml to be uploaded first   	     *)
(*	    This file needs Supporting_Theorems.ml to be uploaded first      *)
(*	    This file needs Simplifiers.ml to be uploaded first              *)
(*---------------------------------------------------------------------------*)


(*===========================================================================*)
(*                               CASE STUDY                                  *)
(*---------------------------------------------------------------------------*)
(*          Time Evolution of Tumor Growth based on Cancer Stem Cells        *)
(*===========================================================================*)

let tumor_growth_rk_model =  new_definition`
    tumor_growth_rk_model CSC P M k1 k2 k3 t = 
  [(irreversible, ([(1,CSC t); (0,P t); (0,M t)],
                   [(1,CSC t); (1,P t); (0,M t)], (k1,&0)));
   (irreversible, ([(1,CSC t); (0,P t); (0,M t)],
                   [(0,CSC t); (0,P t); (1,M t)], (k2,&0)));
   (irreversible, ([(0,CSC t); (1,P t); (0,M t)],
                   [(0,CSC t); (0,P t); (1,M t)], (k3,&0))) ]`;;


g `!k1 k2 k3 CSC P M t. 
    st_matrix (tumor_growth_rk_model CSC P M k1 k2 k3 t) = 
       vector
          [vector [&0; &1; &0];  
  	   vector [-- &1; &0; &1]; 
  	   vector [&0; -- &1; &1]]`;;

e (KINETIC_SIMP [tumor_growth_rk_model]);;
e (SIMP_TAC [REAL_FIELD `&0 - &0 = &0`;
             REAL_FIELD `!(a:real). &0 - a = --a`; 
             REAL_FIELD `!(a:real). a - &0 = a`;
             REAL_FIELD `a - a = &0`]);;

let ST_MATRIX_CSC_GROWTH = top_thm ();;


g `!k1 k2 k3 CSC P M t.
    flux (tumor_growth_rk_model CSC P M k1 k2 k3 t) = 
        vector
         [k1 * CSC t; k2 * CSC t; k3 * P t]`;;

e (KINETIC_SIMP [tumor_growth_rk_model]);;

let FLUX_VECTOR_CSC_GROWTH = top_thm ();;


(*===========================================================================*)
(*                         Main Lemma and  Theorem                           *)
(*===========================================================================*)

g `!k1 k2 k3 t.
    ~((k3 - k2) = &0) 
       ==>
    real_derivative
 (\t. ((k3 - k2 - k1) * exp (--k3 * t) + k1 * exp (--k2 * t)) / (k3 - k2))
 t =
 k1 * exp (--k2 * t) -
 &1 *
 k3 *
 ((k3 - k2 - k1) * exp (--k3 * t) + k1 * exp (--k2 * t)) / (k3 - k2)`;;

e (REPEAT STRIP_TAC);;
e (MATCH_MP_TAC HAS_REAL_DERIVATIVE_DERIVATIVE);;
e (REAL_DIFF_TAC);;
e (POP_ASSUM MP_TAC);;
e (CONV_TAC REAL_FIELD);;

let TGM_LEMMA_RK = top_thm();;


g `!k1 k2 k3 CSC P M t.
       ~(k3 -k2 = &0) /\
       (!t. CSC t = exp ((-- k2) * t)) /\
       (!t. P t =  ((k3 - k2 - k1) * exp ((-- k3) * t) + k1 * exp ((-- k2) * t)) / (k3 - k2)) /\
       (real_derivative M t = k2 * CSC t + k3 * P t) ==>
       ((entities_deriv_vec [CSC; P; M] t):real^3) =
         transp ((st_matrix 
          (tumor_growth_rk_model CSC P M k1 k2 k3 t)):real^3^3) ** 
           flux (tumor_growth_rk_model CSC P M k1 k2 k3 t)`;;

e (REPEAT STRIP_TAC);;
e (KINETIC_SIMP [tumor_growth_rk_model; ST_MATRIX_CSC_GROWTH]);;
e (SIMP_TAC [TRANSP_3X3_MAT_LEMMA; FLUX_VECTOR_CSC_GROWTH; ST_MATRIX_CSC_GROWTH; MATRIX_VEXTOR_3X3]);;
e (SIMP_TAC [REAL_MUL_LID; REAL_MUL_LZERO; REAL_MUL_RZERO; REAL_ADD_RID; REAL_ADD_LID]);;
e (COMMON_TAC [VECTOR_3; DIMINDEX_3; FORALL_3]);;
e (SIMP_TAC [REAL_FIELD `!k. -- &1 * k = --k`; REAL_FIELD ` ! a b. (a:real) + --b = a - b`; REAL_FIELD `(!k. -- (k * (b:real)) = --k * b)`; REAL_FIELD `! a b c. (a:real) + -- b * c = a - b * c`]);;
e (CONJ_TAC);;
      e (ONCE_REWRITE_TAC [DERIV_ABST]);;
      e (ONCE_ASM_REWRITE_TAC []);;
      e (MATCH_MP_TAC HAS_REAL_DERIVATIVE_DERIVATIVE);;
      e (REAL_DIFF_TAC);;
      e (CONV_TAC REAL_FIELD);;

      e (CONJ_TAC);;
      r (1);;
      e (ASM_SIMP_TAC []);;

            e (ONCE_REWRITE_TAC [DERIV_ABST]);;
	    e (ONCE_ASM_REWRITE_TAC []);;
            e (ASM_MESON_TAC [TGM_LEMMA_RK]);;

let TUMOR_GROWTH_SOLUTION_RK = top_thm();;

(*===================================End=====================================*)