(* ========================================================================= *) (* File Name: Tumor_growth.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: *, *) (* ** *) (* *) (* 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 *) (*---------------------------------------------------------------------------*) (* Tumor Growth based on Cancer Stem Cells *) (*===========================================================================*) let cancer_stem_cell = new_definition` cancer_stem_cell CSC P D M k1 k2 k3 k4 k5 k6 k7 k8 t = [(irreversible, ([(1,CSC t); (0,P t); (0,D t); (0,M t)], [(2,CSC t); (0,P t); (0,D t); (0,M t)], (k1,&0))); (irreversible, ([(1,CSC t); (0,P t); (0,D t); (0,M t)], [(1,CSC t); (1,P t); (0,D t); (0,M t)], (k2,&0))); (irreversible, ([(1,CSC t); (0,P t); (0,D t); (0,M t)], [(0,CSC t); (2,P t); (0,D t); (0,M t)], (k3,&0))); (irreversible, ([(0,CSC t); (1,P t); (0,D t); (0,M t)], [(0,CSC t); (2,P t); (0,D t); (0,M t)], (k4,&0))); (irreversible, ([(0,CSC t); (1,P t); (0,D t); (0,M t)], [(0,CSC t); (0,P t); (2,D t); (0,M t)], (k5,&0))); (irreversible, ([(1,CSC t); (0,P t); (0,D t); (0,M t)], [(0,CSC t); (0,P t); (0,D t); (1,M t)], (k6,&0))); (irreversible, ([(0,CSC t); (1,P t); (0,D t); (0,M t)], [(0,CSC t); (0,P t); (0,D t); (1,M t)], (k7,&0))); (irreversible, ([(0,CSC t); (0,P t); (1,D t); (0,M t)], [(0,CSC t); (0,P t); (0,D t); (1,M t)], (k8,&0))) ]`;; g `!k1 k2 k3 k4 k5 k6 k7 CSC P D M t k8. st_matrix (cancer_stem_cell CSC P D M k1 k2 k3 k4 k5 k6 k7 k8 t) = vector [vector [&1; &0; &0; &0]; vector [&0; &1; &0; &0]; vector [-- &1; &2; &0; &0]; vector [&0; &1; &0; &0]; vector [&0; -- &1; &2; &0]; vector [-- &1; &0; &0; &1]; vector [&0; -- &1; &0; &1]; vector [&0; &0; -- &1; &1]]`;; e (KINETIC_SIMP [cancer_stem_cell]);; e (SIMP_TAC [REAL_FIELD `&0 - &0 = &0`; REAL_FIELD `!(a:real). &0 - a = --a`; REAL_FIELD `!(a:real). a - &0 = a`; REAL_FIELD ` &2 - &1 = &1 /\ a - a = &0`]);; let ST_MATRIX_CSC = top_thm ();; g `!k1 k2 k3 k4 k5 k6 k7 CSC P D M t k8. flux (cancer_stem_cell CSC P D M k1 k2 k3 k4 k5 k6 k7 k8 t) = vector [k1 * CSC t; k2 * CSC t; k3 * CSC t; k4 * P t; k5 * P t; k6 * CSC t; k7 * P t; k8 * D t]`;; e (KINETIC_SIMP [cancer_stem_cell]);; let FLUX_VECTOR_CSC = top_thm ();; (*===========================================================================*) (* Main Lemma and Theorem *) (*===========================================================================*) g `!k1 k2 k3 k4 k5 k6 k7 k8 t. ~(((--k1 + k3 + k4 - k5 + k6 - k7)* (--k1 + k3 + k6 - k8) * (--k4 + k5 + k7 - k8)) = &0) /\ ~((k1 - k3 - k4 + k5 - k6 + k7) = &0) ==> real_derivative (\t. (&2 * exp(--k8 * t) * (k2 + &2* k3) * k5 * ((-- &1 + exp ((k4 - k5 - k7 + k8) * t)) * k1 + k3 + k4 - k5 + k6 - k7 + exp ((k1 - k3 - k6 + k8) * t) * (-- k4 + k5 + k7 - k8) + exp ((k4 - k5 - k7 + k8) * t) * (--k3 - k6 + k8))) / ((--k1 + k3 + k4 - k5 + k6 - k7) * (--k1 + k3 + k6 - k8) * (--k4 + k5 + k7 - k8))) t = &2 * k5 * ((exp ((k1 - k3 - k6) *t) - exp ((k4 - k5 - k7) * t)) * (k2 + &2* k3)) / (k1 - k3 - k4 + k5 - k6 + k7) - k8 * (&2 * exp(--k8 * t) * (k2 + &2* k3) * k5 * ((-- &1 + exp ((k4 - k5 - k7 + k8) * t)) * k1 + k3 + k4 - k5 + k6 - k7 + exp ((k1 - k3 - k6 + k8) * t) * (-- k4 + k5 + k7 - k8) + exp ((k4 - k5 - k7 + k8) * t) * (--k3 - k6 + k8))) / ((--k1 + k3 + k4 - k5 + k6 - k7) * (--k1 + k3 + k6 - k8) * (--k4 + k5 + k7 - k8))`;; e (REPEAT STRIP_TAC);; e (MATCH_MP_TAC HAS_REAL_DERIVATIVE_DERIVATIVE);; e (REAL_DIFF_TAC);; e (SIMP_TAC [REAL_ADD_LID; REAL_FIELD ` &0 - a = --a`; REAL_ADD_RID; REAL_MUL_RID]);; e (ASM_SIMP_TAC [REAL_FIELD ` ! a b c d g h k. ~(d = &0) /\ ~(k = &0) ==> a * b * c / d - g * ( h / k) = (a * b * c * k - g * h * d) / (d * k)`]);; e (ASM_SIMP_TAC [REAL_FIELD `! a b c (d:real). ~(b = &0 ) /\ ~(d = &0) ==> ((a / b) = (c / (d * b))) = (a * d = c ) `; REAL_FIELD ` ((k1 - k3 - k4 + k5 - k6 + k7) * (--k1 + k3 + k4 - k5 + k6 - k7) * (--k1 + k3 + k6 - k8) * (--k4 + k5 + k7 - k8)) = ((k1 - k3 - k4 + k5 - k6 + k7) * ( (--k1 + k3 + k4 - k5 + k6 - k7) * (--k1 + k3 + k6 - k8) * (--k4 + k5 + k7 - k8)))`]);; e (SIMP_TAC [REAL_FIELD `! a b c. a * (b * c) = a * b * c`]);; e (SIMP_TAC [REAL_FIELD ` (&2 * (exp (--k8 * t) * (k2 + &2 * k3) * k5 * (((k4 - k5 - k7 + k8) * exp ((k4 - k5 - k7 + k8) * t)) * k1 + ((k1 - k3 - k6 + k8) * exp ((k1 - k3 - k6 + k8) * t)) * (--k4 + k5 + k7 - k8) + ((k4 - k5 - k7 + k8) * exp ((k4 - k5 - k7 + k8) * t)) * (--k3 - k6 + k8)) + (--k8 * exp (--k8 * t)) * (k2 + &2 * k3) * k5 * ((-- &1 + exp ((k4 - k5 - k7 + k8) * t)) * k1 + k3 + k4 - k5 + k6 - k7 + exp ((k1 - k3 - k6 + k8) * t) * (--k4 + k5 + k7 - k8) + exp ((k4 - k5 - k7 + k8) * t) * (--k3 - k6 + k8)))) * (k1 - k3 - k4 + k5 - k6 + k7) = ((&2 * exp (--k8 * t) * (k2 + &2 * k3) * k5 * (((k4 - k5 - k7 + k8) * exp ((k4 - k5 - k7 + k8) * t)) * k1 + ((k1 - k3 - k6 + k8) * exp ((k1 - k3 - k6 + k8) * t)) * (--k4 + k5 + k7 - k8) + ((k4 - k5 - k7 + k8) * exp ((k4 - k5 - k7 + k8) * t)) * (--k3 - k6 + k8)) - &2 * (k8 * exp (--k8 * t)) * (k2 + &2 * k3) * k5 * ((-- &1 + exp ((k4 - k5 - k7 + k8) * t)) * k1 + k3 + k4 - k5 + k6 - k7 + exp ((k1 - k3 - k6 + k8) * t) * (--k4 + k5 + k7 - k8) + exp ((k4 - k5 - k7 + k8) * t) * (--k3 - k6 + k8)))) * (k1 - k3 - k4 + k5 - k6 + k7)`]);; e (SIMP_TAC [REAL_FIELD ` (&2 * exp (--k8 * t) * (k2 + &2 * k3) * k5 * (((k4 - k5 - k7 + k8) * exp ((k4 - k5 - k7 + k8) * t)) * k1 + ((k1 - k3 - k6 + k8) * exp ((k1 - k3 - k6 + k8) * t)) * (--k4 + k5 + k7 - k8) + ((k4 - k5 - k7 + k8) * exp ((k4 - k5 - k7 + k8) * t)) * (--k3 - k6 + k8)) - &2 * (k8 * exp (--k8 * t)) * (k2 + &2 * k3) * k5 * ((-- &1 + exp ((k4 - k5 - k7 + k8) * t)) * k1 + k3 + k4 - k5 + k6 - k7 + exp ((k1 - k3 - k6 + k8) * t) * (--k4 + k5 + k7 - k8) + exp ((k4 - k5 - k7 + k8) * t) * (--k3 - k6 + k8))) * (k1 - k3 - k4 + k5 - k6 + k7) = &2 * exp (--k8 * t) * (k2 + &2 * k3) * k5 * (((k4 - k5 - k7 + k8) * exp ((k4 - k5 - k7 + k8) * t)) * k1 + ((k1 - k3 - k6 + k8) * exp ((k1 - k3 - k6 + k8) * t)) * (--k4 + k5 + k7 - k8) + ((k4 - k5 - k7 + k8) * exp ((k4 - k5 - k7 + k8) * t)) * (--k3 - k6 + k8))* (k1 - k3 - k4 + k5 - k6 + k7) - &2 * (k8 * exp (--k8 * t)) * (k2 + &2 * k3) * k5 * ((-- &1 + exp ((k4 - k5 - k7 + k8) * t)) * k1 + k3 + k4 - k5 + k6 - k7 + exp ((k1 - k3 - k6 + k8) * t) * (--k4 + k5 + k7 - k8) + exp ((k4 - k5 - k7 + k8) * t) * (--k3 - k6 + k8)) * (k1 - k3 - k4 + k5 - k6 + k7) `]);; e (SIMP_TAC [REAL_FIELD `&2 * (k8 * exp (--k8 * t)) * (k2 + &2 * k3) * k5 * ((-- &1 + exp ((k4 - k5 - k7 + k8) * t)) * k1 + k3 + k4 - k5 + k6 - k7 + exp ((k1 - k3 - k6 + k8) * t) * (--k4 + k5 + k7 - k8) + exp ((k4 - k5 - k7 + k8) * t) * (--k3 - k6 + k8)) * (k1 - k3 - k4 + k5 - k6 + k7) = k8 * (&2 * exp (--k8 * t) * (k2 + &2 * k3) * k5 * ((-- &1 + exp ((k4 - k5 - k7 + k8) * t)) * k1 + k3 + k4 - k5 + k6 - k7 + exp ((k1 - k3 - k6 + k8) * t) * (--k4 + k5 + k7 - k8) + exp ((k4 - k5 - k7 + k8) * t) * (--k3 - k6 + k8))) * (k1 - k3 - k4 + k5 - k6 + k7)`]);; e (SIMP_TAC [REAL_FIELD `!(a:real) b c. a - b = c - b <=> a = c`]);; e (SIMP_TAC [REAL_FIELD ` &2 * exp (--k8 * t) * (k2 + &2 * k3) * k5 * (((k4 - k5 - k7 + k8) * exp ((k4 - k5 - k7 + k8) * t)) * k1 + ((k1 - k3 - k6 + k8) * exp ((k1 - k3 - k6 + k8) * t)) * (--k4 + k5 + k7 - k8) + ((k4 - k5 - k7 + k8) * exp ((k4 - k5 - k7 + k8) * t)) * (--k3 - k6 + k8)) * (k1 - k3 - k4 + k5 - k6 + k7) = &2 * exp (--k8 * t) * (k2 + &2 * k3) * k5 * (((k4 - k5 - k7 + k8) * exp ((k4 - k5 - k7 + k8) * t)) * (k1 - k3 - k6 + k8) + ((k1 - k3 - k6 + k8) * exp ((k1 - k3 - k6 + k8) * t)) * (--k4 + k5 + k7 - k8) ) * (k1 - k3 - k4 + k5 - k6 + k7)`]);; e (SIMP_TAC [REAL_FIELD `(((k4:real) - k5 - k7 + k8) * t) = ((k4 - k5 - k7)*t + k8 * t)`]);; e (SIMP_TAC [REAL_EXP_ADD]);; e (SIMP_TAC [REAL_FIELD `((k4 - k5 - k7) * exp ((k4 - k5 - k7) * t) * exp (k8 * t) + k8 * exp ((k4 - k5 - k7) * t) * exp (k8 * t)) = ((k4 - k5 - k7) * exp ((k4 - k5 - k7) * t) + k8 * exp ((k4 - k5 - k7) * t)) * exp (k8 * t)`; REAL_FIELD `((k1 - k3 - k6) * exp ((k1 - k3 - k6) * t) * exp (k8 * t) + k8 * exp ((k1 - k3 - k6) * t) * exp (k8 * t)) = ((k1 - k3 - k6) * exp ((k1 - k3 - k6) * t) + k8 * exp ((k1 - k3 - k6) * t)) * exp (k8 * t)`] );; e (SIMP_TAC [REAL_FIELD `((((k4 - k5 - k7) * exp ((k4 - k5 - k7) * t) + k8 * exp ((k4 - k5 - k7) * t)) * exp (k8 * t)) * (k1 - k3 - k6 + k8) + (((k1 - k3 - k6) * exp ((k1 - k3 - k6) * t) + k8 * exp ((k1 - k3 - k6) * t)) * exp (k8 * t)) * (--k4 + k5 + k7 - k8)) = ((((k4 - k5 - k7) * exp ((k4 - k5 - k7) * t) + k8 * exp ((k4 - k5 - k7) * t))) * (k1 - k3 - k6 + k8) + (((k1 - k3 - k6) * exp ((k1 - k3 - k6) * t) + k8 * exp ((k1 - k3 - k6) * t))) * (--k4 + k5 + k7 - k8)) * exp (k8 * t)`]);; e (SIMP_TAC [REAL_FIELD `&2 * exp (--k8 * t) * (k2 + &2 * k3) * k5 * ((((k4 - k5 - k7) * exp ((k4 - k5 - k7) * t) + k8 * exp ((k4 - k5 - k7) * t)) * (k1 - k3 - k6 + k8) + ((k1 - k3 - k6) * exp ((k1 - k3 - k6) * t) + k8 * exp ((k1 - k3 - k6) * t)) * (--k4 + k5 + k7 - k8)) * exp (k8 * t)) * (k1 - k3 - k4 + k5 - k6 + k7) = &2 * (exp (--k8 * t) * exp (k8 * t)) * (k2 + &2 * k3) * k5 * ((((k4 - k5 - k7) * exp ((k4 - k5 - k7) * t) + k8 * exp ((k4 - k5 - k7) * t)) * (k1 - k3 - k6 + k8) + ((k1 - k3 - k6) * exp ((k1 - k3 - k6) * t) + k8 * exp ((k1 - k3 - k6) * t)) * (--k4 + k5 + k7 - k8)) * (k1 - k3 - k4 + k5 - k6 + k7))`]);; e (SIMP_TAC [REAL_EXP_NEG; REAL_FIELD ` --(k8:real) * t = --(k8 * t)`]);; e (SIMP_TAC [REAL_MUL_LINV;REAL_EXP_NZ]);; e (CONV_TAC REAL_FIELD);; let TGM_LEMMA = top_thm();; (*---------------------------------------------------------------------------*) g `!k1 k2 k3 k4 k5 k6 k7 CSC P D M t k8. ~((--k1 + k3 + k4 - k5 + k6 - k7) * (--k1 + k3 + k6 - k8) * (--k4 + k5 + k7 - k8) = &0) /\ ~(k1 - k3 - k4 + k5 - k6 + k7 = &0) /\ (!t. CSC t = exp ((k1 - k3 - k6)*t)) /\ (!t. P t = ((exp ((k1 - k3 - k6) * t) - exp ((k4 - k5 - k7) * t)) * (k2 + &2 * k3)) / (k1 - k3 - k4 + k5 - k6 + k7)) /\ (!t. D t = (&2 * exp (--k8 * t) * (k2 + &2 * k3) * k5 * ((-- &1 + exp ((k4 - k5 - k7 + k8) * t)) * k1 + k3 + k4 - k5 + k6 - k7 + exp ((k1 - k3 - k6 + k8) * t) * (--k4 + k5 + k7 - k8) + exp ((k4 - k5 - k7 + k8) * t) * (--k3 - k6 + k8))) / ((--k1 + k3 + k4 - k5 + k6 - k7) * (--k1 + k3 + k6 - k8) * (--k4 + k5 + k7 - k8))) /\ (real_derivative M t = k6 * CSC t + k7 * P t + k8 * D t) ==> ((entities_deriv_vec [CSC;P;D;M] t):real^4) = transp ((st_matrix (cancer_stem_cell CSC P D M k1 k2 k3 k4 k5 k6 k7 k8 t)):real^4^8) ** flux (cancer_stem_cell CSC P D M k1 k2 k3 k4 k5 k6 k7 k8 t)`;; e (REPEAT STRIP_TAC);; e (KINETIC_SIMP [cancer_stem_cell; ST_MATRIX_CSC]);; e (SIMP_TAC [TRANSP_8X3_MAT_LEMMA; FLUX_VECTOR_CSC; ST_MATRIX_CSC; MATRIX_VEXTOR_8X4]);; e (SIMP_TAC [REAL_MUL_LID; REAL_MUL_LZERO; REAL_MUL_RZERO; REAL_ADD_RID; REAL_ADD_LID]);; e (COMMON_TAC [VECTOR_8; VECTOR_4; DIMINDEX_8; DIMINDEX_4; FORALL_4]);; e (SIMP_TAC [REAL_FIELD `!k. -- &1 * k = --k`; REAL_FIELD ` ! a b. (a:real) + --b = a - b`; REAL_FIELD `! a b c. (a:real) + --(b * c) = a - b * c`]);; e (SIMP_TAC [REAL_FIELD `(k1:real) * CSC t + --(k3 * CSC t) - k6 * CSC t = k1 * CSC t - (k3 * CSC t) - k6 * CSC t`; REAL_FIELD ` (k2:real) * CSC t + &2 * k3 * CSC t + k4 * P t + --(k5 * P t) - k7 * P t = (k2 + &2 * k3) * CSC t + (k4 - k5 - k7) * P t`]);; e (SIMP_TAC [REAL_FIELD `(k1:real) * CSC t - k3 * CSC t - k6 * CSC t = (k1 - k3 - k6) * CSC t`]);; 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);; e (ONCE_REWRITE_TAC [DERIV_ABST]);; e (ONCE_ASM_REWRITE_TAC []);; e (MATCH_MP_TAC HAS_REAL_DERIVATIVE_DERIVATIVE);; e (REAL_DIFF_TAC);; e (UNDISCH_TAC `~(k1 - k3 - k4 + k5 - k6 + k7 = &0)`);; e (CONV_TAC REAL_FIELD);; e (CONJ_TAC);; e (ONCE_REWRITE_TAC [DERIV_ABST]);; e (ONCE_ASM_REWRITE_TAC []);; e (ASM_MESON_TAC [TGM_LEMMA]);; e (ASM_SIMP_TAC []);; let TUMOR_GROWTH_SOLUTION = top_thm();; (*===================================End=====================================*)