(* ========================================================================= *)
(* File Name: Reaction_Schemes.ml		                             *)
(*---------------------------------------------------------------------------*)
(* Description: Formal Verification of Reaction Schemes                      *)
(*                                                                           *)
(*                                                                           *)
(*     (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              *)
(*---------------------------------------------------------------------------*)


(*===========================================================================*)
(*             Properties of Reaction Kinetics Based Modeling                *)
(*===========================================================================*)


(*===========================================================================*)
(*                           Reaction Scheme 01                              *)
(*---------------------------------------------------------------------------*)
(*                  The Irreverible Consecutive Reactions                    *)
(*===========================================================================*)

let rea_sch_01 = new_definition`
   rea_sch_01 A B C k1 k2 t = 
  [(irreversible, ([(1,A t); (0,B t); (0,C t)], [(0,A t); (1,B t); (0,C t)], (k1,&0)));
   (irreversible, ([(0,A t); (1,B t); (0,C t)], [(0,A t); (0,B t); (1,C t)], (k2,&0)))
  ]`;;


g `! A B C k1 k2 t. 
      ((entities_deriv_vec [A;B;C] t):real^3) =
       vector [real_derivative A t; real_derivative B t; real_derivative C t]`;;

e (KINETIC_SIMP []);;

let ENTITIES_DERIVATIVE_VEC = top_thm();;


g `!A B C k1 k2 t. 
    transp((st_matrix (rea_sch_01 A B C k1 k2 t)):real^3^2) = 
       vector [vector [&0 - &1; &0 - &0]; 
               vector [&1 - &0; &0 - &1]; 
	       vector [&0 - &0; &1 - &0]]`;;

e (KINETIC_SIMP [rea_sch_01; TRANSP_2X3_MAT_LEMMA]);;

let ST_MATRIX_REA_SCH_01 = top_thm();;


g `!A B C k1 k2 t.
    flux (rea_sch_01 A B C k1 k2 t) = 
       vector [k1 * A t; k2 * B t]`;;

e (KINETIC_SIMP [rea_sch_01]);;

let FLUX_VECTOR_REA_SCH_01 = top_thm();;


g `! A B C t k1 k2. 
     (&0 < k1) /\ (&0 < k2) /\ ~((k2 - k1) = &0) /\
     (A (&0) = A0) /\ (B (&0) = &0) /\ (C (&0) = &0) /\
     (!t. A t = A0 * exp (--k1 * t)) /\
     (!t. B t = A0 * ((k1 / (k2 - k1)) * (exp (--k1 * t) - exp (--k2 * t)))) /\
     (!t. C t = A0 * (&1 - ((k2 / (k2 - k1)) * (exp (--k1 * t))) - 
                           ((k1 / (k1 - k2)) * (exp (--k2 * t))))) 
               ==>
    (real_derivative (\t. A t) t = (-- k1 * A t)) /\
    (real_derivative (\t. B t) t = (k1 * A t - k2 * B t)) /\
    (real_derivative (\t. C t) t = (k2 * B t)) `;;

e (SIMP_TAC []);;
e (REPEAT STRIP_TAC);;
e (MATCH_MP_TAC HAS_REAL_DERIVATIVE_DERIVATIVE);;
e (REAL_DIFF_TAC);;
e (REAL_ARITH_TAC);;

e (MATCH_MP_TAC HAS_REAL_DERIVATIVE_DERIVATIVE);;
e (REAL_DIFF_TAC);;
e (REWRITE_TAC [REAL_SUB_LDISTRIB]);;
e (SUBGOAL_THEN `A0 * k1 / (k2 - k1) * (--k1 * &1) * exp (--k1 * t) = k1 * A0 * exp (--k1 * t) -
 (k2 * A0 * k1 / (k2 - k1) * exp (--k1 * t))` ASSUME_TAC);;
      e (REWRITE_TAC [real_div]);;
      e (ONCE_REWRITE_TAC [REAL_MUL_ASSOC]);;
      e (ONCE_REWRITE_TAC [GSYM REAL_SUB_RDISTRIB]);;
      e (ONCE_REWRITE_TAC [REAL_MUL_ASSOC]);;
      e (ONCE_REWRITE_TAC [GSYM REAL_SUB_RDISTRIB]);;
      e (REWRITE_TAC [REAL_EQ_MUL_RCANCEL]);;
      e (DISJ1_TAC);;
      e (SUBGOAL_THEN `k1 * A0 - ((k2:real * A0) * k1) * inv (k2 - k1) 
                = k1 * A0 * (k2 - k1) * inv (k2 - k1)  - ((k2 * A0) * k1) * inv (k2 - k1)` ASSUME_TAC);;
            e (SUBGOAL_THEN `(k2 - k1) * inv (k2 - k1) = &1` ASSUME_TAC);;
	          e (MATCH_MP_TAC REAL_MUL_RINV);;
		  e (ASM_SIMP_TAC []);;

      e (ASM_REWRITE_TAC []);;
      e (REAL_ARITH_TAC);;

      e (ONCE_REWRITE_TAC [REAL_MUL_ASSOC]);;
      e (ASM_REWRITE_TAC []);;
      e (POP_ASSUM (K ALL_TAC));;
      e (ONCE_REWRITE_TAC [REAL_MUL_ASSOC]);;
      e (ONCE_REWRITE_TAC [REAL_MUL_ASSOC]);;
      e (ONCE_REWRITE_TAC [GSYM REAL_SUB_RDISTRIB]);;
      e (REAL_ARITH_TAC);;

      e (ASM_REWRITE_TAC []);;
      e (REAL_ARITH_TAC);;

e (MATCH_MP_TAC HAS_REAL_DERIVATIVE_DERIVATIVE);;
e (REAL_DIFF_TAC);;
e (REWRITE_TAC [REAL_SUB_LDISTRIB]);;
e (SUBGOAL_THEN `A0 * &0 -  A0 * k2 / (k2 - k1) * (--k1 * &1) * exp (--k1 * t) = 
                           A0 * k2 * k1 / (k2 - k1) * exp (--k1 * t)` ASSUME_TAC);;
      e (REAL_ARITH_TAC);;

e (ASM_REWRITE_TAC []);;
e (POP_ASSUM (K ALL_TAC));;
e (SUBGOAL_THEN `A0 * k1 / (k1 - k2) * (--k2 * &1) * exp (--k2 * t) = 
                           k2 * A0 * k1 / (k2 - k1) * exp (--k2 * t)` ASSUME_TAC);;

      e (SUBGOAL_THEN `(k1 - k2:real) = --(k2 - k1)` ASSUME_TAC);;
            e (REWRITE_TAC [REAL_EQ_SUB_RADD]);;
            e (ONCE_REWRITE_TAC [REAL_ADD_SYM]);;
            e (ONCE_REWRITE_TAC [REAL_ARITH `!a:real b. a + --b = a - b`]);;
            e (REAL_ARITH_TAC);;

      e (ASM_REWRITE_TAC []);;
      e (POP_ASSUM (K ALL_TAC));;
      e (SUBGOAL_THEN `(((A0 * k1:real / --(k2 - k1)) * --k2) * &1) 
                               = k2 * A0 * k1 / (k2 - k1)` ASSUME_TAC);;
            e (REWRITE_TAC [real_div]);;
	    e (REWRITE_TAC [REAL_INV_NEG]);;   
            e (REAL_ARITH_TAC);;

      e (ASM_REWRITE_TAC [REAL_MUL_ASSOC]);;
      e (ASM_REWRITE_TAC []);;
      e (REAL_ARITH_TAC);;

let ODE_SOL_REA_SCH_01_LEMMA = top_thm();;


g `! A B C t k1 k2. 
     (&0 < k1) /\ (&0 < k2) /\ ~(k2 = k1) /\
     (A (&0) = A0) /\ (B (&0) = &0) /\ (C (&0) = &0) /\
     (!t. A t = A0 * exp (--k1 * t)) /\
     (!t. B t = A0 * ((k1 / (k2 - k1)) * (exp (--k1 * t) - exp (--k2 * t)))) /\
     (!t. C t = A0 * (&1 - ((k2 / (k2 - k1)) * (exp (--k1 * t))) - 
                           ((k1 / (k1 - k2)) * (exp (--k2 * t))))) 
               ==>
      ((entities_deriv_vec [A;B;C] t):real^3) =
        transp((st_matrix (rea_sch_01 A B C k1 k2 t)):real^3^2) ** 
                  flux (rea_sch_01 A B C k1 k2 t)`;;

e (REWRITE_TAC [ENTITIES_DERIVATIVE_VEC]);;
e (REWRITE_TAC [ST_MATRIX_REA_SCH_01]);;
e (REWRITE_TAC [FLUX_VECTOR_REA_SCH_01]);;
e (REPEAT STRIP_TAC);;
e (REWRITE_TAC [REAL_ARITH `(&0 - &1) = --(&1)`]);;
e (REWRITE_TAC [REAL_ARITH `(&1 - &0) = &1`]);;
e (REWRITE_TAC [REAL_ARITH `(&0 - &0) = &0`]);;
e (REWRITE_TAC [MAT3X2_VECTOR_MUL]);;
e (REWRITE_TAC [REAL_ARITH `!x. &0 * x = &0`]);;
e (REWRITE_TAC [REAL_ARITH `!x. -- &1 * x = -- x`]);;
e (REWRITE_TAC [REAL_ARITH `!x. &1 * x = x`]);;
e (REWRITE_TAC [REAL_NEG_LMUL]);;
e (REWRITE_TAC [REAL_ARITH `!x y z w:real. x * w + --y * z = x * w - y * z`]);;
e (REWRITE_TAC [REAL_ARITH `!x. &0 + x = x`]);;
e (REWRITE_TAC [REAL_ARITH `!x. x + &0 = x`]);;
e (ONCE_REWRITE_TAC [DERIV_ABST]);;
e (REWRITE_TAC [VECTOR3_EQ]);;
e (MATCH_MP_TAC ODE_SOL_REA_SCH_01_LEMMA);;
e (ASM_REWRITE_TAC []);;
e (ASM_REAL_ARITH_TAC);;

let ODE_SOL_REA_SCH_01 = top_thm ();;

(*===========================================================================*)
(*                            Reaction Scheme 02                             *)
(*---------------------------------------------------------------------------*)
(*     The Consecutive Reactions with the Second Step being Reversible       *)
(*===========================================================================*)

let rea_sch_02 = new_definition`
   rea_sch_02 A B C k1 k2 k3 t = 
  [(irreversible, ([(1,A t); (0,B t); (0,C t)], [(0,A t); (1,B t); (0,C t)], (k1,&0))) ;
   (reversible, ([(0,A t); (1,B t); (0,C t)], [(0,A t); (0,B t); (1,C t)], (k2,k3)))
  ]`;;


g `!A B C k1 k2 k3 t. 
    transp((st_matrix (rea_sch_02 A B C k1 k2 k3 t)):real^3^2) = 
       vector [vector [&0 - &1; &0 - &0]; 
               vector [&1 - &0; &0 - &1]; 
	       vector [&0 - &0; &1 - &0]]`;;

e (KINETIC_SIMP [rea_sch_02; TRANSP_2X3_MAT_LEMMA]);;

let ST_MATRIX_REA_SCH_02 = top_thm();;


g `flux (rea_sch_02 A B C k1 k2 k3 t) = 
     vector [k1 * A t; k2 * B t - k3 * C t]`;;

e (KINETIC_SIMP [rea_sch_02]);;

let FLUX_VECTOR_REA_SCH_02 = top_thm();;


g `! A B C t k1 k2 k3. 
     (&0 < k1) /\ (&0 < k2) /\ (&0 < k3) /\
     (A (&0) = A0) /\ (B (&0) = &0) /\ (C (&0) = &0) /\
     (r1 = k1) /\ (r2 = k2 + k3) /\ ~(r1 = r2) /\
     (!t. A t = A0 * exp (--k1 * t)) /\
     (!t. B t = k1 * A0 * ( (k3 / (r1 * r2) ) 
       + (((r2 - k3) / (r2 * (r1 - r2))) * exp (--r2 * t))    
         + (((k3 - r1) / (r1 * (r1 - r2))) * exp (--r1 * t) ) ) ) /\
     (!t. C t =   k1 * k2 * A0 * ( ((&1) / (r1 * r2) ) 
       + (((&1) / (r1 * (r1 - r2))) * exp (--r1 * t))    
         - (((&1) / (r2 * (r1 - r2))) * exp (--r2 * t) ) )) 
               ==>
    (real_derivative (\t. A t) t = (-- k1 * A t)) /\
    (real_derivative (\t. B t) t = (k1 * A t - (k2 * B t - k3 * C t))) /\
    (real_derivative (\t. C t) t = (k2 * B t - k3 * C t)) `;;

e (SIMP_TAC []);;
e (REPEAT STRIP_TAC);;
e (MATCH_MP_TAC HAS_REAL_DERIVATIVE_DERIVATIVE);;
e (REAL_DIFF_TAC);;
e (REAL_ARITH_TAC);;

e (MATCH_MP_TAC HAS_REAL_DERIVATIVE_DERIVATIVE);;
e (REAL_DIFF_TAC);;

e (UNDISCH_TAC `r1 = k1:real`);;
e (UNDISCH_TAC `r2 = k2 + k3:real`);;
e (ONCE_REWRITE_TAC [EQ_SYM_EQ]);;
e (SIMP_TAC []);;
e (REPEAT DISCH_TAC);;
e (ONCE_REWRITE_TAC [EQ_SYM_EQ]);;
e (SUBGOAL_THEN `r1 * A0 * (&0 +
  (r2 - k3) / (r2 * (r1 - r2)) * (--r2 * &1) * exp (--r2 * t) +
  (k3 - r1) / (r1 * (r1 - r2)) * (--r1 * &1) * exp (--r1 * t)) =
r1 * A0 * ((r1 - k3) / (r1 - r2) * exp (--r1 * t) -
  k2 / (r1 - r2) * exp (--r2 * t))` ASSUME_TAC);;
e (UNDISCH_TAC `k2 + k3 = r2:real`);;
e (ONCE_REWRITE_TAC [EQ_SYM_EQ]);;
e (SIMP_TAC []);;
e (DISCH_TAC);;
e (REWRITE_TAC [REAL_EQ_MUL_LCANCEL]);;
e (REPEAT DISJ2_TAC);;
e (REWRITE_TAC [REAL_ARITH `((k2 + k3) - k3) = k2:real`]);;
e (POP_ASSUM MP_TAC);;
e (ONCE_REWRITE_TAC [EQ_SYM_EQ]);;
e (SIMP_TAC []);;
e (DISCH_TAC);;
e (SUBGOAL_THEN `(k3 - r1) / (r1 * (r1 - r2)) * (--r1 * &1) * exp (--r1 * t) = 
  		     (r1 - k3) / (r1 - r2) * exp (--r1 * t)` ASSUME_TAC);;
      e (REWRITE_TAC [REAL_MUL_ASSOC]);;
      e (REWRITE_TAC [REAL_EQ_MUL_RCANCEL]);;
      e (DISJ1_TAC);;
      e (REWRITE_TAC [real_div]);;
      e (REWRITE_TAC [REAL_INV_MUL]);;
      e (REWRITE_TAC [REAL_ARITH `(((k3 - r1:real) * inv r1 * inv (r1 - r2)) * --r1) * &1
      		     		 = (r1 * inv r1) * ((r1 - k3) * inv (r1 - r2))`]);;
      e (SUBGOAL_THEN `(r1 * inv r1) = &1` ASSUME_TAC);;
            e (MATCH_MP_TAC REAL_MUL_RINV);;
	    e (UNDISCH_TAC `k1 = r1:real`);;
	    e (ONCE_REWRITE_TAC [EQ_SYM_EQ]);;
	    e (SIMP_TAC []);;
	    e (DISCH_TAC);;
	    e (REWRITE_TAC [REAL_NOT_EQ]);;
      	    e (DISJ1_TAC);;
	    e (ASM_REWRITE_TAC []);;

      e (ASM_REWRITE_TAC []);;
      e (CONV_TAC REAL_FIELD);;

e (ASM_REWRITE_TAC []);;
e (SUBGOAL_THEN `k2 / (r2 * (r1 - r2)) * (--r2 * &1) * exp (--r2 * t) = 
  		     -- k2 / (r1 - r2) * exp (--r2 * t)` ASSUME_TAC);;
      e (REWRITE_TAC [REAL_MUL_ASSOC]);;
      e (REWRITE_TAC [REAL_EQ_MUL_RCANCEL]);;
      e (DISJ1_TAC);;
      e (REWRITE_TAC [real_div]);;
      e (REWRITE_TAC [REAL_INV_MUL]);;
      e (REWRITE_TAC [REAL_ARITH `(((k2:real) * inv r2 * inv (r1 - r2)) * --r2) * &1
      		     		 = -- (r2 * inv r2) * (k2 * inv (r1 - r2))`]);;
      e (SUBGOAL_THEN `(r2 * inv r2) = &1` ASSUME_TAC);;
            e (MATCH_MP_TAC REAL_MUL_RINV);;
	    e (UNDISCH_TAC `k2 + k3 = r2:real`);;
	    e (ONCE_REWRITE_TAC [EQ_SYM_EQ]);;
	    e (SIMP_TAC []);;
	    e (DISCH_TAC);;
	    e (REWRITE_TAC [REAL_NOT_EQ]);;
      	    e (DISJ1_TAC);;
	    e (ASM_REAL_ARITH_TAC);;

      e (ASM_REWRITE_TAC []);;
      e (CONV_TAC REAL_FIELD);;

e (ASM_REWRITE_TAC []);;
e (CONV_TAC REAL_FIELD);;

e (ASM_REWRITE_TAC []);;
e (POP_ASSUM (K ALL_TAC));;
e (ONCE_REWRITE_TAC [EQ_SYM_EQ]);;
e (REWRITE_TAC [REAL_ARITH `r1 * A0 * exp (--r1 * t) -
 (k2 *
  r1 *
  A0 *
  (k3 / (r1 * r2) +
   (r2 - k3) / (r2 * (r1 - r2)) * exp (--r2 * t) +
   (k3 - r1) / (r1 * (r1 - r2)) * exp (--r1 * t)) -
  k3 *
  r1 *
  k2 *
  A0 *
  (&1 / (r1 * r2) +
   &1 / (r1 * (r1 - r2)) * exp (--r1 * t) -
   &1 / (r2 * (r1 - r2)) * exp (--r2 * t))) = (r1 * A0 * ((&1 - (k2 * (k3 - r1)) / (r1 * (r1 - r2)) +
    (k3 * k2) / (r1 * (r1 - r2)) ) * exp (--r1 * t) -
   ((k2 * (r2 - k3)) / (r2 * (r1 - r2)) +
   (k3 * k2) / (r2 * (r1 - r2))) * exp (--r2 * t)))`]);;
e (REWRITE_TAC [REAL_EQ_MUL_LCANCEL]);;
e (REPEAT DISJ2_TAC);;
e (SUBGOAL_THEN `((k2 * (r2 - k3)) / (r2 * (r1 - r2)) + (k3 * k2) / (r2 * (r1 - r2)))
 * exp (--r2 * t) = k2 / (r1 - r2) * exp (--r2 * t)` ASSUME_TAC);;
      e (REWRITE_TAC [real_div]);;
      e (REWRITE_TAC [REAL_INV_MUL]);;
      e (REWRITE_TAC [REAL_EQ_MUL_RCANCEL]);;
      e (DISJ1_TAC);;
      e (REWRITE_TAC [REAL_MUL_ASSOC]);;
      e (REWRITE_TAC [GSYM REAL_ADD_RDISTRIB]);;
      e (REWRITE_TAC [REAL_EQ_MUL_RCANCEL]);;
      e (DISJ1_TAC);;
      e (REWRITE_TAC [REAL_ARITH `(k2 * (r2 - k3) + k3:real * k2) = (k2 * r2)`]);;
      e (REWRITE_TAC [GSYM REAL_MUL_ASSOC]);;
      e (SUBGOAL_THEN `(r2 * inv r2) = &1` ASSUME_TAC);;
            e (MATCH_MP_TAC REAL_MUL_RINV);;
	    e (UNDISCH_TAC `k2 + k3 = r2:real`);;
	    e (ONCE_REWRITE_TAC [EQ_SYM_EQ]);;
	    e (SIMP_TAC []);;
	    e (DISCH_TAC);;
	    e (REWRITE_TAC [REAL_NOT_EQ]);;
      	    e (DISJ1_TAC);;
	    e (ASM_REAL_ARITH_TAC);;

      e (ASM_REWRITE_TAC []);;
      e (CONV_TAC REAL_FIELD);;

e (ASM_REWRITE_TAC []);;
e (POP_ASSUM (K ALL_TAC));;
e (SUBGOAL_THEN `(&1 - (k2 * (k3 - r1)) / (r1 * (r1 - r2)) + (k3 * k2) / (r1 * (r1 - r2))) *
 exp (--r1 * t) = (r1 - k3) / (r1 - r2) * exp (--r1 * t)` ASSUME_TAC);;
      e (REWRITE_TAC [real_div]);;
      e (REWRITE_TAC [REAL_INV_MUL]);;
      e (REWRITE_TAC [REAL_EQ_MUL_RCANCEL]);;
      e (DISJ1_TAC);;
      e (SUBGOAL_THEN `&1 = (r1 * inv (r1)) * (r1 - r2) * inv (r1 -r2) ` ASSUME_TAC);;
            e (SUBGOAL_THEN `r1 * inv r1 = &1` ASSUME_TAC);;
                  e (MATCH_MP_TAC REAL_MUL_RINV);;
	    	  e (UNDISCH_TAC `k1 = r1:real`);;
	    	  e (ONCE_REWRITE_TAC [EQ_SYM_EQ]);;
	    	  e (SIMP_TAC []);;
	    	  e (DISCH_TAC);;
	    	  e (REWRITE_TAC [REAL_NOT_EQ]);;
      	    	  e (DISJ1_TAC);;
	    	  e (ASM_REAL_ARITH_TAC);;

            e (ASM_REWRITE_TAC []);;
            e (SUBGOAL_THEN `(r1 - r2) * inv (r1 - r2) = &1` ASSUME_TAC);;
                  e (MATCH_MP_TAC REAL_MUL_RINV);;
	    	  e (ASM_REAL_ARITH_TAC);;

            e (ASM_REWRITE_TAC []);;

      e (CONV_TAC REAL_FIELD);;
      e (ASM_REWRITE_TAC []);;
      e (POP_ASSUM (K ALL_TAC));;
      e (REWRITE_TAC [REAL_MUL_ASSOC]);;
      e (REWRITE_TAC [GSYM REAL_SUB_RDISTRIB]);;
      e (REWRITE_TAC [GSYM REAL_ADD_RDISTRIB]);;
      e (REWRITE_TAC [REAL_EQ_MUL_RCANCEL]);;
      e (DISJ1_TAC);;
      e (SUBGOAL_THEN `r1 * inv r1 = &1` ASSUME_TAC);;
            e (MATCH_MP_TAC REAL_MUL_RINV);;
	    e (UNDISCH_TAC `k1 = r1:real`);;
	    e (ONCE_REWRITE_TAC [EQ_SYM_EQ]);;
	    e (SIMP_TAC []);;
	    e (DISCH_TAC);;
	    e (REWRITE_TAC [REAL_NOT_EQ]);;
      	    e (DISJ1_TAC);;
	    e (ASM_REAL_ARITH_TAC);;

      e (ASM_REWRITE_TAC []);;
      e (REWRITE_TAC [REAL_ARITH `(&1 * (r1 - r2) - (k2 * (k3 - r1)) * inv r1 + (k3 * k2) * inv r1) = 
      		     		 (r1 - r2) + k2 * r1 * inv r1`]);;
      e (ASM_REWRITE_TAC []);;
      e (ASM_REAL_ARITH_TAC);;

e (ASM_REWRITE_TAC []);;

e (MATCH_MP_TAC HAS_REAL_DERIVATIVE_DERIVATIVE);;
e (REAL_DIFF_TAC);;
e (SUBGOAL_THEN `(k1 * k2 * A0 * (&0 +
  &1 / (r1 * (r1 - r2)) * (--r1 * &1) * exp (--r1 * t) -
    &1 / (r2 * (r1 - r2)) * (--r2 * &1) * exp (--r2 * t))) = 
      ( k1 * k2 * A0 * ((&1 / (r1 - r2)) * exp (--r2 * t) 
        - (&1 / (r1 - r2)) * exp (--r1 * t)) )` ASSUME_TAC);;
      e (REWRITE_TAC [real_div]);;
      e (REWRITE_TAC [REAL_EQ_MUL_LCANCEL]);;
      e (DISJ2_TAC);;
      e (DISJ2_TAC);;
      e (DISJ2_TAC);;
      e (REWRITE_TAC [REAL_INV_MUL]);;
      e (SUBGOAL_THEN `!x:real. (&1 * inv x * inv (r1 - r2)) * (--x * &1) * exp (--x * t) 
                 =  (&1 * inv x * x * inv (r1 - r2)) * (-- (&1)) * exp (--x * t)` ASSUME_TAC);;
            e (REAL_ARITH_TAC);;

      e (POP_ASSUM MP_TAC);;
      e (SIMP_TAC []);;
      e (DISCH_TAC);;
      e (POP_ASSUM (K ALL_TAC));;
      e (ONCE_REWRITE_TAC [REAL_MUL_ASSOC]);;
      e (ONCE_REWRITE_TAC [REAL_MUL_ASSOC]);;
      e (REWRITE_TAC [REAL_ARITH `!x. (&1 * inv x) = inv x`]);;
      e (ONCE_REWRITE_TAC [REAL_MUL_ASSOC]);;
      e (SUBGOAL_THEN `(inv r1 * r1) = &1` ASSUME_TAC);;
            e (MATCH_MP_TAC REAL_MUL_LINV);;
	    e (REWRITE_TAC [REAL_NOT_EQ]);;
	    e (DISJ2_TAC);;
	    e (ASM_REWRITE_TAC []);;

      e (POP_ASSUM MP_TAC);;
      e (SIMP_TAC []);;
      e (DISCH_TAC);;
      e (POP_ASSUM (K ALL_TAC));;
      e (SUBGOAL_THEN `(inv r2 * r2) = &1` ASSUME_TAC);;
            e (MATCH_MP_TAC REAL_MUL_LINV);;
	    e (REWRITE_TAC [REAL_NOT_EQ]);;
	    e (DISJ2_TAC);;
      	    e (ASM_REAL_ARITH_TAC);;

      e (POP_ASSUM MP_TAC);;
      e (SIMP_TAC []);;
      e (DISCH_TAC);;
      e (POP_ASSUM (K ALL_TAC));;
      e (REAL_ARITH_TAC);;

e (POP_ASSUM MP_TAC);;
e (ONCE_REWRITE_TAC [EQ_SYM_EQ]);;
e (UNDISCH_TAC `r1 = k1:real`);;
e (UNDISCH_TAC `r2 = k2 + k3:real`);;
e (ONCE_REWRITE_TAC [EQ_SYM_EQ]);;
e (SIMP_TAC []);;
e (REPEAT DISCH_TAC);;
e (POP_ASSUM (K ALL_TAC));;
e (ONCE_REWRITE_TAC [EQ_SYM_EQ]);;
e (REWRITE_TAC [REAL_ARITH `(k2 * r1 * A0 *
 (k3 / (r1 * r2) + (r2 - k3) / (r2 * (r1 - r2)) * exp (--r2 * t) +
  (k3 - r1) / (r1 * (r1 - r2)) * exp (--r1 * t)) -
 k3 * r1 * k2 * A0 *
 (&1 / (r1 * r2) +
  &1 / (r1 * (r1 - r2)) * exp (--r1 * t) -
  &1 / (r2 * (r1 - r2)) * exp (--r2 * t))) = (r1 * k2 * A0 * ( (k3 / (r1 * r2) +
  (r2 - k3) / (r2 * (r1 - r2)) * exp (--r2 * t) +
  (k3 - r1) / (r1 * (r1 - r2)) * exp (--r1 * t)) -
 k3 * (&1 / (r1 * r2) +
  &1 / (r1 * (r1 - r2)) * exp (--r1 * t) -
  &1 / (r2 * (r1 - r2)) * exp (--r2 * t)) ))`]);;
e (REWRITE_TAC [REAL_EQ_MUL_LCANCEL]);;
e (REPEAT DISJ2_TAC);;
e (REWRITE_TAC [REAL_ARITH `!a:real b c d. a * (b + c - d) = a * b + a * c - a * d`]);;
e (REWRITE_TAC [REAL_ARITH `!a:real b c d. a - (b + c - d) = a - b - c + d`]);;
e (REWRITE_TAC [REAL_ARITH `!a:real b c d. a * &1 / b = a / b`]);;
e (REWRITE_TAC [REAL_ARITH `!a:real b c d e. (a + b + c) - a - d + e = b + e + c - d`]);;
e (REWRITE_TAC [real_div]);;
e (ONCE_REWRITE_TAC [REAL_MUL_ASSOC]);;
e (ONCE_REWRITE_TAC [GSYM REAL_SUB_RDISTRIB]);;
e (SUBGOAL_THEN `((k3 - r1) * inv (r1 * (r1 - r2)) - k3 * &1 * inv (r1 * (r1 - r2))) *
 exp (--r1 * t) = -- ((&1 * inv (r1 - r2)) * exp (--r1 * t))` ASSUME_TAC);;
      e (REWRITE_TAC [GSYM REAL_MUL_LNEG]);;
      e (REWRITE_TAC [REAL_EQ_MUL_RCANCEL]);;
      e (DISJ1_TAC);;
      e (REWRITE_TAC [REAL_INV_MUL]);;
      e (REWRITE_TAC [REAL_MUL_ASSOC]);;
      e (ONCE_REWRITE_TAC [GSYM REAL_SUB_RDISTRIB]);;
      e (REWRITE_TAC [REAL_EQ_MUL_RCANCEL]);;
      e (DISJ1_TAC);;
      e (ONCE_REWRITE_TAC [GSYM REAL_SUB_RDISTRIB]);;
      e (REWRITE_TAC [REAL_ARITH `(k3 - r1 - k3 * &1) = -- r1`]);;
      e (REWRITE_TAC [REAL_MUL_LNEG]);;
      e (SUBGOAL_THEN `(r1 * inv r1) = &1` ASSUME_TAC);;
            e (MATCH_MP_TAC REAL_MUL_RINV);;
	    e (POP_ASSUM MP_TAC);;
	    e (ONCE_REWRITE_TAC [EQ_SYM_EQ]);;
	    e (SIMP_TAC []);;
	    e (DISCH_TAC);;
	    e (REWRITE_TAC [REAL_NOT_EQ]);;
      	    e (DISJ1_TAC);;
	    e (ASM_REWRITE_TAC []);;

      e (ASM_REWRITE_TAC []);;

e (ASM_REWRITE_TAC []);;
e (POP_ASSUM (K ALL_TAC));;
e (REWRITE_TAC [REAL_ARITH `!a:real b c. a + b + (--c) = a + b - c`]);;
e (REWRITE_TAC [REAL_EQ_SUB_LADD]);;
e (REWRITE_TAC [REAL_ARITH `!a:real b c. (a + b - c) + c = a + b`]);;
e (REWRITE_TAC [GSYM REAL_ADD_RDISTRIB]);;
e (REWRITE_TAC [REAL_INV_MUL]);;
e (REWRITE_TAC [REAL_MUL_ASSOC]);;
e (REWRITE_TAC [GSYM REAL_ADD_RDISTRIB]);;
e (REWRITE_TAC [REAL_MUL_ASSOC]);;
e (REWRITE_TAC [REAL_EQ_MUL_RCANCEL]);;
e (REPEAT DISJ1_TAC);;
e (REWRITE_TAC [REAL_ARITH `(r2 - k3 + k3 * &1) = r2`]);;
e (MATCH_MP_TAC REAL_MUL_RINV);;
e (UNDISCH_TAC `k2 + k3 = r2:real`);;
e (ONCE_REWRITE_TAC [EQ_SYM_EQ]);;
e (SIMP_TAC []);;
e (DISCH_TAC);;
e (REWRITE_TAC [REAL_NOT_EQ]);;
e (DISJ1_TAC);;
e (ASM_REAL_ARITH_TAC);;

let ODE_SOL_REA_SCH_02_LEMMA = top_thm ();;


g `! A B C t k1 k2 k3. 
     (&0 < k1) /\ (&0 < k2) /\ (&0 < k3) /\
     (A (&0) = A0) /\ (B (&0) = &0) /\ (C (&0) = &0) /\
     (r1 = k1) /\ (r2 = k2 + k3) /\ ~(r1 = r2) /\
     (!t. A t = A0 * exp (--k1 * t)) /\
     (!t. B t = k1 * A0 * ( (k3 / (r1 * r2) ) 
       + (((r2 - k3) / (r2 * (r1 - r2))) * exp (--r2 * t))    
         + (((k3 - r1) / (r1 * (r1 - r2))) * exp (--r1 * t) ) ) ) /\
     (!t. C t =   k1 * k2 * A0 * ( ((&1) / (r1 * r2) ) 
       + (((&1) / (r1 * (r1 - r2))) * exp (--r1 * t))    
         - (((&1) / (r2 * (r1 - r2))) * exp (--r2 * t) ) )) 
               ==>
      ((entities_deriv_vec [A;B;C] t):real^3) =
        transp((st_matrix (rea_sch_02 A B C k1 k2 k3 t)):real^3^2) ** 
                  flux (rea_sch_02 A B C k1 k2 k3 t)`;;

e (REWRITE_TAC [ENTITIES_DERIVATIVE_VEC]);;
e (REWRITE_TAC [ST_MATRIX_REA_SCH_02]);;
e (REWRITE_TAC [FLUX_VECTOR_REA_SCH_02]);;
e (REPEAT STRIP_TAC);;
e (REWRITE_TAC [REAL_ARITH `(&0 - &1) = --(&1)`]);;
e (REWRITE_TAC [REAL_ARITH `(&1 - &0) = &1`]);;
e (REWRITE_TAC [REAL_ARITH `(&0 - &0) = &0`]);;
e (REWRITE_TAC [MAT3X2_VECTOR_MUL]);;
e (REWRITE_TAC [REAL_ARITH `!x. &0 * x = &0`]);;
e (REWRITE_TAC [REAL_ARITH `!x. -- &1 * x = -- x`]);;
e (REWRITE_TAC [REAL_ARITH `!x. &1 * x = x`]);;
e (REWRITE_TAC [REAL_NEG_LMUL]);;
e (REWRITE_TAC [REAL_ARITH `!x. &0 + x = x`]);;
e (REWRITE_TAC [REAL_ARITH `!x. x + &0 = x`]);;
e (REWRITE_TAC [REAL_ARITH `!x y z:real. x + -- (y - z) = x - (y - z)`]);;
e (ONCE_REWRITE_TAC [DERIV_ABST]);;
e (REWRITE_TAC [VECTOR3_EQ]);;
e (MATCH_MP_TAC ODE_SOL_REA_SCH_02_LEMMA);;
e (ASM_REWRITE_TAC []);;

let ODE_SOL_REA_SCH_02 = top_thm ();;

(*===========================================================================*)
(*                           Reaction Scheme 03                              *)
(*---------------------------------------------------------------------------*)
(*    The Consecutive Reactions with First Step as a Reversible Reaction     *)
(*===========================================================================*)

let rea_sch_03 = new_definition`
   rea_sch_03 A B C k1 k2 k3 t = 
  [(reversible, ([(1,A t); (0,B t); (0,C t)], [(0,A t); (1,B t); (0,C t)], (k1,k2))) ;
   (irreversible, ([(0,A t); (1,B t); (0,C t)], [(0,A t); (0,B t); (1,C t)], (k3,&0)))]`;;


g `!A B C k1 k2 k3 t. 
    transp((st_matrix (rea_sch_03 A B C k1 k2 k3 t)):real^3^2) = 
       vector [vector [&0 - &1; &0 - &0]; 
               vector [&1 - &0; &0 - &1]; 
	       vector [&0 - &0; &1 - &0]]`;;

e (KINETIC_SIMP [rea_sch_03; TRANSP_2X3_MAT_LEMMA]);;

let ST_MATRIX_REA_SCH_03 = top_thm();;


g `flux (rea_sch_03 A B C k1 k2 k3 t) = 
      vector [k1 * A t - k2 * B t; k3 * B t]`;;

e (KINETIC_SIMP [rea_sch_03]);;

let FLUX_VECTOR_REA_SCH_03 = top_thm();;


g `! A B C t k1 k2 k3. 
     (&0 < k1) /\ (&0 < k2) /\ (&0 < k3) /\
     (A (&0) = A0) /\ (B (&0) = &0) /\ (C (&0) = &0) /\
     (r1 * r2 = k1 * k3) /\ (r1 + r2 = k1 + k2 + k3) /\ 
     ~(r1 = &0) /\ ~(r2 = &0) /\ ~(r1 = r2) /\
     (!t. A t = (A0 / (r2 - r1)) * 
     ( (k2 + k3 - r1) * exp (--r1 * t) - (k2 + k3 - r2) * exp (--r2 * t) ) ) /\
     (!t. B t = ((A0 * k1) / (r2 - r1)) * (exp (--r1 * t) - exp (--r2 * t)  ) ) /\
     (!t. C t =  A0 * (&1 + (k1 * k3) / (r1 * (r1 - r2)) * exp (--r1 * t) 
               + (k1 * k3) / (r2 * (r2 - r1)) * exp (--r2 * t)) )
               ==>
    (real_derivative (\t. A t) t = (-- k1 * A t + k2 * B t)) /\
    (real_derivative (\t. B t) t = (k1 * A t - k2 * B t - k3 * B t)) /\
    (real_derivative (\t. C t) t = (k3 * B t))`;;

e (SIMP_TAC []);;
e (REPEAT STRIP_TAC);;
e (MATCH_MP_TAC HAS_REAL_DERIVATIVE_DERIVATIVE);;
e (REAL_DIFF_TAC);;
e (SUBGOAL_THEN `A0 / (r2 - r1) *
 ((k2 + k3 - r1) * (--r1 * &1) * exp (--r1 * t) -
  (k2 + k3 - r2) * (--r2 * &1) * exp (--r2 * t)) = A0 / (r2 - r1) *
 ((r2 * (r1 - k1)) * exp (--r2 * t) -
  (r1 * (r2 - k1)) * exp (--r1 * t))` ASSUME_TAC);;
      e (REWRITE_TAC [real_div]);;
      e (REWRITE_TAC [REAL_EQ_MUL_LCANCEL]);;
      e (DISJ2_TAC);;
      e (SUBGOAL_THEN `(k2 + k3 - r1) * (--r1 * &1) * exp (--r1 * t) 
                        = -- (r1 * (r2 - k1)) * exp (--r1 * t)` ASSUME_TAC);;
	    e (REWRITE_TAC [REAL_MUL_ASSOC]);;
	    e (REWRITE_TAC [REAL_EQ_MUL_RCANCEL]);;
	    e (DISJ1_TAC);;
	    e (SUBGOAL_THEN `k2 + k3 = r1 + r2 - k1:real` ASSUME_TAC);;
	          e (ASM_REAL_ARITH_TAC);;

	    e (POP_ASSUM MP_TAC);;
      	    e (CONV_TAC REAL_FIELD);;

      e (ASM_REWRITE_TAC []);;
      e (POP_ASSUM (K ALL_TAC));;
      e (SUBGOAL_THEN `(k2 + k3 - r2) * (--r2 * &1) * exp (--r2 * t) 
                    = -- (r2 * (r1 - k1)) * exp (--r2 * t)` ASSUME_TAC);;
	    e (REWRITE_TAC [REAL_MUL_ASSOC]);;
	    e (REWRITE_TAC [REAL_EQ_MUL_RCANCEL]);;
	    e (DISJ1_TAC);;
	    e (SUBGOAL_THEN `k2 + k3 = r1 + r2 - k1:real` ASSUME_TAC);;
	          e (ASM_REAL_ARITH_TAC);;

	    e (POP_ASSUM MP_TAC);;
      	    e (CONV_TAC REAL_FIELD);;

      e (ASM_REWRITE_TAC []);;
      e (CONV_TAC REAL_FIELD);;

      e (ASM_REWRITE_TAC []);;
      e (POP_ASSUM (K ALL_TAC));;
      e (ONCE_REWRITE_TAC [EQ_SYM_EQ]);;
      e (REWRITE_TAC [REAL_ARITH `(--k1 *
 A0 / (r2 - r1) *
 ((k2 + k3 - r1) * exp (--r1 * t) - (k2 + k3 - r2) * exp (--r2 * t)) +
 k2 * (A0 * k1) / (r2 - r1) * (exp (--r1 * t) - exp (--r2 * t)) ) = 
 A0 / (r2 - r1) * 
 ( k1 * (k3 - r2) * exp (--r2 * t) - k1 * (k3 - r1) * exp (--r1 * t) )`]);;
      e (REWRITE_TAC [real_div]);;
      e (REWRITE_TAC [REAL_EQ_MUL_LCANCEL]);;
      e (DISJ2_TAC);;
      e (REWRITE_TAC [REAL_MUL_ASSOC]);;
      e (REWRITE_TAC [REAL_SUB_LDISTRIB]);;
      e (UNDISCH_TAC `r1 * r2 = k1:real * k3`);;
      e (ONCE_REWRITE_TAC [EQ_SYM_EQ]);;
      e (CONV_TAC REAL_FIELD);;

e (MATCH_MP_TAC HAS_REAL_DERIVATIVE_DERIVATIVE);;
e (REAL_DIFF_TAC);;
e (CONV_TAC REAL_FIELD);;

e (MATCH_MP_TAC HAS_REAL_DERIVATIVE_DERIVATIVE);;
e (REAL_DIFF_TAC);;
e (REWRITE_TAC [REAL_ARITH `!x. &0 + x = x`]);;
e (ONCE_REWRITE_TAC [REAL_ADD_LDISTRIB]);;
e (ONCE_REWRITE_TAC [REAL_MUL_ASSOC]);;
e (ONCE_REWRITE_TAC [REAL_MUL_ASSOC]);;
e (REWRITE_TAC [real_div]);;
e (REWRITE_TAC [REAL_INV_MUL]);;
e (ONCE_REWRITE_TAC [REAL_SUB_LDISTRIB]);;
e (SUBGOAL_THEN `((A0 * (k1 * k3) * inv r1 * inv (r1 - r2)) * --r1 * &1) * exp (--r1 * t) =
                  (k3 * (A0 * k1) * inv (r2 - r1)) * exp (--r1 * t)` ASSUME_TAC);;
      e (REWRITE_TAC [REAL_EQ_MUL_RCANCEL]);;
      e (DISJ1_TAC);;
      e (ONCE_REWRITE_TAC [REAL_ARITH `( (A0 * (k1 * k3) * inv r1 * inv (r1 - r2)) * --r1 * &1
   = ((r1 * inv r1) * k3 * (A0 * k1) * -- inv (r1 - r2)) )`]);;
      e (REWRITE_TAC [GSYM REAL_INV_NEG]);;
      e (ONCE_REWRITE_TAC [REAL_ARITH `--(r1 - r2) = (r2:real - r1)`]);;
      e (SUBGOAL_THEN `(r1 * inv r1) = &1` ASSUME_TAC);;
            e (MATCH_MP_TAC REAL_MUL_RINV);;
	    e (ASM_REWRITE_TAC []);;

      e (ASM_REWRITE_TAC []);;
      e (REAL_ARITH_TAC);;

e (ASM_REWRITE_TAC []);;
e (SUBGOAL_THEN `((A0 * (k1 * k3) * inv r2 * inv (r2 - r1)) * --r2 * &1) * exp (--r2 * t)
          = -- (k3 * (A0 * k1) * inv (r2 - r1)) * exp (--r2 * t)` ASSUME_TAC);;
      e (ONCE_REWRITE_TAC [REAL_MUL_ASSOC]);;
      e (REWRITE_TAC [REAL_EQ_MUL_RCANCEL]);;
      e (DISJ1_TAC);;
      e (REWRITE_TAC [REAL_ARITH `((A0 * (k1 * k3) * inv r2 * inv (r2 - r1)) * --r2) * &1 = 
                      -- (((r2 * inv r2) * inv (r2 - r1)) * A0 * (k1 * k3))`]);;
      e (SUBGOAL_THEN `(r2 * inv r2) = &1` ASSUME_TAC);;
            e (MATCH_MP_TAC REAL_MUL_RINV);;
	    e (ASM_REWRITE_TAC []);;

      e (ASM_REWRITE_TAC []);;
      e (REAL_ARITH_TAC);;

e (ASM_REWRITE_TAC []);;
e (CONV_TAC REAL_FIELD);;

let ODE_SOL_REA_SCH_03_LEMMA = top_thm ();;


g `! A B C t k1 k2 k3. 
     (&0 < k1) /\ (&0 < k2) /\ (&0 < k3) /\
     (A (&0) = A0) /\ (B (&0) = &0) /\ (C (&0) = &0) /\
     (r1 * r2 = k1 * k3) /\ (r1 + r2 = k1 + k2 + k3) /\ 
     ~(r1 = &0) /\ ~(r2 = &0) /\ ~(r1 = r2) /\
     (!t. A t = (A0 / (r2 - r1)) * 
     ( (k2 + k3 - r1) * exp (--r1 * t) - (k2 + k3 - r2) * exp (--r2 * t) ) ) /\
     (!t. B t = ((A0 * k1) / (r2 - r1)) * (exp (--r1 * t) - exp (--r2 * t)  ) ) /\
     (!t. C t =  A0 * (&1 + (k1 * k3) / (r1 * (r1 - r2)) * exp (--r1 * t) 
               + (k1 * k3) / (r2 * (r2 - r1)) * exp (--r2 * t)) )
               ==>
      ((entities_deriv_vec [A;B;C] t):real^3) =
        transp((st_matrix (rea_sch_03 A B C k1 k2 k3 t)):real^3^2) ** 
                  flux (rea_sch_03 A B C k1 k2 k3 t)`;;

e (REWRITE_TAC [ENTITIES_DERIVATIVE_VEC]);;
e (REWRITE_TAC [ST_MATRIX_REA_SCH_03]);;
e (REWRITE_TAC [FLUX_VECTOR_REA_SCH_03]);;
e (REPEAT STRIP_TAC);;
e (REWRITE_TAC [REAL_ARITH `(&0 - &1) = --(&1)`]);;
e (REWRITE_TAC [REAL_ARITH `(&1 - &0) = &1`]);;
e (REWRITE_TAC [REAL_ARITH `(&0 - &0) = &0`]);;
e (REWRITE_TAC [MAT3X2_VECTOR_MUL]);;
e (REWRITE_TAC [REAL_ARITH `!x. &0 * x = &0`]);;
e (REWRITE_TAC [REAL_ARITH `!x. -- &1 * x = -- x`]);;
e (REWRITE_TAC [REAL_ARITH `!x. &1 * x = x`]);;
e (REWRITE_TAC [REAL_NEG_LMUL]);;
e (REWRITE_TAC [REAL_ARITH `!x. &0 + x = x`]);;
e (REWRITE_TAC [REAL_ARITH `!x. x + &0 = x`]);;
e (REWRITE_TAC [GSYM REAL_NEG_LMUL]);;
e (REWRITE_TAC [REAL_ARITH `!x y:real. (-- (x - y) ) = (-- x + y)`]);;
e (REWRITE_TAC [REAL_ARITH `!x y z:real. ((x - y) + -- z) = (x - y - z)`]);;
e (REWRITE_TAC [REAL_NEG_LMUL]);;
e (ONCE_REWRITE_TAC [DERIV_ABST]);;
e (REWRITE_TAC [VECTOR3_EQ]);;
e (MATCH_MP_TAC ODE_SOL_REA_SCH_03_LEMMA);;
e (ASM_REWRITE_TAC []);;

let ODE_SOL_REA_SCH_03 = top_thm ();;

(*===========================================================================*)
(*                            Reaction Scheme 04                             *)
(*---------------------------------------------------------------------------*)
(*               The Consecutive Reactions with a Reversible Step            *)
(*===========================================================================*)

let rea_sch_04 = new_definition`
   rea_sch_04 A B C k1 k2 k3 t = 
  [(reversible,([(1,A t); (0,B t); (0,C t)], [(0,A t); (1,B t); (0,C t)], (k1,k2)));
   (irreversible,([(1,A t); (0,B t); (0,C t)], [(0,A t); (0,B t); (1,C t)], (k3,&0)))]`;;


g `!A B C k1 k2 k3 t. 
    transp((st_matrix (rea_sch_04 A B C k1 k2 k3 t)):real^3^2) = 
       vector [vector [&0 - &1; &0 - &1]; 
               vector [&1 - &0; &0 - &0]; 
	       vector [&0 - &0; &1 - &0]]`;;

e (KINETIC_SIMP [rea_sch_04; TRANSP_2X3_MAT_LEMMA]);;

let ST_MATRIX_REA_SCH_04 = top_thm();;


g `flux (rea_sch_04 A B C k1 k2 k3 t) = 
      vector [k1 * A t - k2 * B t; k3 * A t]`;;

e (KINETIC_SIMP [rea_sch_04]);;

let FLUX_VECTOR_REA_SCH_04 = top_thm();;


g `! A B C t k1 k2 k3. 
     (&0 < k1) /\ (&0 < k2) /\ (&0 < k3) /\
     (A (&0) = A0) /\ (B (&0) = &0) /\ (C (&0) = &0) /\
     (r1 * r2 = k2 * k3) /\ (r1 + r2 = k1 + k2 + k3) /\ 
     ~(r1 = &0) /\ ~(r2 = &0) /\ ~(r1 = r2) /\
     (!t. A t =  A0 * ((k2 - r1) / (r2 - r1) * exp (--r1 * t) 
               - (k2 - r2) / (r2 - r1) * exp (--r2 * t)) ) /\
     (!t. B t = ( k1 * A0) / (r2 - r1) * (exp (--r1 * t) - exp (--r2 * t)  ) ) /\
     (!t. C t =  A0 * (&1 + (k3 * (k2 - r1)) / (r1 * (r1 - r2)) * exp (--r1 * t) 
               + (k3 * (k2 - r2)) / (r2 * (r2 - r1)) * exp (--r2 * t)) )
               ==>
    (real_derivative (\t. A t) t = (-- k1 * A t + k2 * B t - k3 * A t)) /\
    (real_derivative (\t. B t) t = (k1 * A t - k2 * B t)) /\
    (real_derivative (\t. C t) t = (k3 * A t))`;;

e (SIMP_TAC []);;
e (REPEAT STRIP_TAC);;
e (MATCH_MP_TAC HAS_REAL_DERIVATIVE_DERIVATIVE);;
e (REAL_DIFF_TAC);;

e (ONCE_REWRITE_TAC [REAL_SUB_LDISTRIB]);;
e (ONCE_REWRITE_TAC [REAL_SUB_LDISTRIB]);;
e (REWRITE_TAC [REAL_ARITH `!a b c:real. a - (b - c) = a - b + c`]);;
e (ONCE_REWRITE_TAC [EQ_SYM_EQ]);;
e (SUBGOAL_THEN `( --k1 * A0 * (k2 - r1) / (r2 - r1) * exp (--r1 * t) 
     +  k2 * (k1 * A0) / (r2 - r1) * exp (--r1 * t)
     - k3 * A0 * (k2 - r1) / (r2 - r1) * exp (--r1 * t)) =
     A0 * (k2 - r1) / (r2 - r1) * (--r1 * &1) * exp (--r1 * t)` ASSUME_TAC);;
      e (REWRITE_TAC [real_div]);;
      e (REWRITE_TAC [REAL_MUL_ASSOC]);;
      e (REWRITE_TAC [REAL_ARITH `!a b c d:real. (a * d + b * d - c * d) = ((a + b - c) * d) `]);;
      e (REWRITE_TAC [REAL_EQ_MUL_RCANCEL]);;
      e (DISJ1_TAC);;
      e (REWRITE_TAC [REAL_ARITH `(((A0 * (k2 - r1)) * inv (r2 - r1)) * --r1) * &1 =
                              ((A0 * (k2 - r1)) * --r1 * inv (r2 - r1))`]);;
      e (REWRITE_TAC [REAL_MUL_ASSOC]);;
      e (REWRITE_TAC [REAL_EQ_MUL_RCANCEL]);;
      e (DISJ1_TAC);;
      e (REWRITE_TAC [REAL_ARITH ` ((--k1 * A0) * (k2 - r1) + (k2 * k1) * A0 - (k3 * A0) * (k2 - r1)) 
           = (A0 * (r1 * (k1 + k3) - (k2:real) * k3))`]);;
      e (REWRITE_TAC [GSYM REAL_MUL_ASSOC]);;
      e (REWRITE_TAC [REAL_EQ_MUL_LCANCEL]);;
      e (DISJ2_TAC);;
      e (UNDISCH_TAC `r1 * r2:real = k2 * k3`);;
      e (UNDISCH_TAC `r1 + r2 = k1 + (k2:real) + k3`);;
      e (CONV_TAC REAL_FIELD);;

e (REWRITE_TAC [REAL_ARITH `(--k1 * A0 * (k2 - r1) / (r2 - r1) * exp (--r1 * t) -
 --k1 * A0 * (k2 - r2) / (r2 - r1) * exp (--r2 * t) +
 k2 * (k1 * A0) / (r2 - r1) * exp (--r1 * t) -
 k2 * (k1 * A0) / (r2 - r1) * exp (--r2 * t) -
 k3 * A0 * (k2 - r1) / (r2 - r1) * exp (--r1 * t) +
 k3 * A0 * (k2 - r2) / (r2 - r1) * exp (--r2 * t)) = ((--k1 * A0 * (k2 - r1) / (r2 - r1) * exp (--r1 * t) +
      k2 * (k1 * A0) / (r2 - r1) * exp (--r1 * t) -
      k3 * A0 * (k2 - r1) / (r2 - r1) * exp (--r1 * t)) 
      + k1 * A0 * (k2 - r2) / (r2 - r1) * exp (--r2 * t)
      - k2 * (k1 * A0) / (r2 - r1) * exp (--r2 * t)
      + k3 * A0 * (k2 - r2) / (r2 - r1:real) * exp (--r2 * t))`]);;

e (ASM_SIMP_TAC []);;
e (POP_ASSUM (K ALL_TAC));;
e (SUBGOAL_THEN `k1 * A0 * (k2 - r2) / (r2 - r1) * exp (--r2 * t) -
 k2 * (k1 * A0) / (r2 - r1) * exp (--r2 * t) +
 k3 * A0 * (k2 - r2) / (r2 - r1) * exp (--r2 * t) = 
 A0 * (k2 - r2) / (r2 - r1) * (r2 * &1) * exp (--r2 * t)` ASSUME_TAC);;
      e (REWRITE_TAC [real_div]);;
      e (REWRITE_TAC [REAL_MUL_ASSOC]);;
      e (REWRITE_TAC [REAL_ARITH `!a b c d:real. (a * d - b * d + c * d) = ((a - b + c) * d) `]);;
      e (REWRITE_TAC [REAL_EQ_MUL_RCANCEL]);;
      e (DISJ1_TAC);;
      e (REWRITE_TAC [REAL_ARITH `(((A0 * (k2 - r2)) * inv (r2 - r1)) * r2) * &1 =
                              ((A0 * (k2 - r2)) * r2 * inv (r2 - r1))`]);;
      e (REWRITE_TAC [REAL_MUL_ASSOC]);;
      e (REWRITE_TAC [REAL_EQ_MUL_RCANCEL]);;
      e (DISJ1_TAC);;
      e (REWRITE_TAC [REAL_ARITH ` ((k1 * A0) * (k2 - r2) - (k2 * k1) * A0 + (k3 * A0) * (k2 - r2)) 
           = (A0 * (-- r2 * (k1 + k3) + (k2:real) * k3))`]);;
      e (REWRITE_TAC [GSYM REAL_MUL_ASSOC]);;
      e (REWRITE_TAC [REAL_EQ_MUL_LCANCEL]);;
      e (DISJ2_TAC);;
      e (UNDISCH_TAC `r1 * r2:real = k2 * k3`);;
      e (UNDISCH_TAC `r1 + r2 = k1 + (k2:real) + k3`);;
      e (CONV_TAC REAL_FIELD);;

e (ASM_REWRITE_TAC []);;
e (CONV_TAC REAL_FIELD);;

e (MATCH_MP_TAC HAS_REAL_DERIVATIVE_DERIVATIVE);;
e (REAL_DIFF_TAC);;

e (CONV_TAC REAL_FIELD);;

e (MATCH_MP_TAC HAS_REAL_DERIVATIVE_DERIVATIVE);;
e (REAL_DIFF_TAC);;
e (REWRITE_TAC [REAL_ARITH `!x. &0 + x = x`]);;
e (ONCE_REWRITE_TAC [REAL_ARITH `!x:real y z. x * y * z = y * x * z`]);;
e (REWRITE_TAC [REAL_EQ_MUL_LCANCEL]);;
e (DISJ2_TAC);;
e (ONCE_REWRITE_TAC [REAL_SUB_LDISTRIB]);;
e (ONCE_REWRITE_TAC [REAL_MUL_ASSOC]);;
e (SUBGOAL_THEN `((--r1 * &1) * (k3 * k2 - k3 * r1) / (r1 * r1 - r1 * r2)) * exp (--r1 * t)
         = (k3 * (k2 - r1) / (r2 - r1)) * exp (--r1 * t)` ASSUME_TAC);;
      e (REWRITE_TAC [REAL_EQ_MUL_RCANCEL]);;
      e (DISJ1_TAC);;
      e (ONCE_REWRITE_TAC [GSYM REAL_SUB_LDISTRIB]);;
      e (REWRITE_TAC [real_div]);;
      e (REWRITE_TAC [REAL_INV_MUL]);;
      e (REWRITE_TAC [REAL_ARITH `(--r1 * &1) * (k3 * (k2 - r1)) * inv r1 * inv (r1 - r2)
      		     		 = ( (r1 * inv r1) * k3 * (k2 - r1) * -- inv (r1 - r2) )`]);;
      e (REWRITE_TAC [GSYM REAL_INV_NEG]);;
      e (ONCE_REWRITE_TAC [REAL_ARITH `--(r1 - r2) = (r2:real - r1)`]);;
      e (SUBGOAL_THEN `(r1 * inv r1) = &1` ASSUME_TAC);;
            e (MATCH_MP_TAC REAL_MUL_RINV);;
	    e (ASM_REWRITE_TAC []);;

      e (ASM_REWRITE_TAC []);;
      e (REAL_ARITH_TAC);;

e (ASM_REWRITE_TAC []);;
e (POP_ASSUM (K ALL_TAC));;
e (SUBGOAL_THEN `((--r2 * &1) * (k3 * k2 - k3 * r2) / (r2 * r2 - r2 * r1)) * exp (--r2 * t)
                 = -- (k3 * (k2 - r2) / (r2 - r1)) * exp (--r2 * t)` ASSUME_TAC);;
      e (REWRITE_TAC [REAL_EQ_MUL_RCANCEL]);;
      e (DISJ1_TAC);;
      e (ONCE_REWRITE_TAC [GSYM REAL_SUB_LDISTRIB]);;
      e (REWRITE_TAC [real_div]);;
      e (REWRITE_TAC [REAL_INV_MUL]);;
      e (REWRITE_TAC [REAL_ARITH `(--r2 * &1) * (k3 * (k2 - r2)) * inv r2 * inv (r2 - r1)
      		     		 = -- ( (r2 * inv r2) * k3 * (k2 - r2) * inv (r2 - r1) )`]);;
      e (REWRITE_TAC [REAL_EQ_NEG2]);;
      e (SUBGOAL_THEN `(r2 * inv r2) = &1` ASSUME_TAC);;
            e (MATCH_MP_TAC REAL_MUL_RINV);;
	    e (ASM_REWRITE_TAC []);;

      e (ASM_REWRITE_TAC []);;
      e (REAL_ARITH_TAC);;

e (ASM_REWRITE_TAC []);;
e (CONV_TAC REAL_FIELD);;

let ODE_SOL_REA_SCH_04_LEMMA = top_thm ();;


g `! A B C t k1 k2 k3. 
     (&0 < k1) /\ (&0 < k2) /\ (&0 < k3) /\
     (A (&0) = A0) /\ (B (&0) = &0) /\ (C (&0) = &0) /\
     (r1 * r2 = k2 * k3) /\ (r1 + r2 = k1 + k2 + k3) /\ 
     ~(r1 = &0) /\ ~(r2 = &0) /\ ~(r1 = r2) /\
     (!t. A t =  A0 * ((k2 - r1) / (r2 - r1) * exp (--r1 * t) 
               - (k2 - r2) / (r2 - r1) * exp (--r2 * t)) ) /\
     (!t. B t = ( k1 * A0) / (r2 - r1) * (exp (--r1 * t) - exp (--r2 * t)  ) ) /\
     (!t. C t =  A0 * (&1 + (k3 * (k2 - r1)) / (r1 * (r1 - r2)) * exp (--r1 * t) 
               + (k3 * (k2 - r2)) / (r2 * (r2 - r1)) * exp (--r2 * t)) )
               ==>
      ((entities_deriv_vec [A;B;C] t):real^3) =
        transp((st_matrix (rea_sch_04 A B C k1 k2 k3 t)):real^3^2) ** 
                  flux (rea_sch_04 A B C k1 k2 k3 t)`;;

e (REWRITE_TAC [ENTITIES_DERIVATIVE_VEC]);;
e (REWRITE_TAC [ST_MATRIX_REA_SCH_04]);;
e (REWRITE_TAC [FLUX_VECTOR_REA_SCH_04]);;
e (REPEAT STRIP_TAC);;
e (REWRITE_TAC [REAL_ARITH `(&0 - &1) = --(&1)`]);;
e (REWRITE_TAC [REAL_ARITH `(&1 - &0) = &1`]);;
e (REWRITE_TAC [REAL_ARITH `(&0 - &0) = &0`]);;
e (REWRITE_TAC [MAT3X2_VECTOR_MUL]);;
e (REWRITE_TAC [REAL_ARITH `!x. &0 * x = &0`]);;
e (REWRITE_TAC [REAL_ARITH `!x. -- &1 * x = -- x`]);;
e (REWRITE_TAC [REAL_ARITH `!x. &1 * x = x`]);;
e (REWRITE_TAC [REAL_NEG_LMUL]);;
e (REWRITE_TAC [REAL_ARITH `!x. &0 + x = x`]);;
e (REWRITE_TAC [REAL_ARITH `!x. x + &0 = x`]);;
e (REWRITE_TAC [GSYM REAL_NEG_LMUL]);;
e (REWRITE_TAC [REAL_ARITH `!x y z:real. (-- (x - y) + -- z) = (-- x + y - z)`]);;
e (ONCE_REWRITE_TAC [DERIV_ABST]);;
e (REWRITE_TAC [VECTOR3_EQ]);;
e (REWRITE_TAC [REAL_NEG_LMUL]);;
e (MATCH_MP_TAC ODE_SOL_REA_SCH_04_LEMMA);;
e (ASM_REWRITE_TAC []);;

let ODE_SOL_REA_SCH_04 = top_thm ();;

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