(* ============================================================== *) (* *) (* Formalization of Macroscopic Models *) (* *) (* (c) Copyright, Muhammad Umair* *) (* Adnan Rashid** *) (* *) (* *Research Center for Modeling and Simulation (RCMS) *) (* National University of Sciences and Technology (NUST) *) (* Islamabad, Pakistan *) (* *) (* **School of Electrical Engineering and Computer Sciences *) (* National University of Sciences and Technology (NUST) *) (* Islamabad, Pakistan *) (* *) (* Contact: * *) (* **, *) (* *) (* ============================================================== *) needs "Multivariate/real.ml";; (*============================================================*) (* Start of the Time_space Model for Occupancy *) (*============================================================*) (* =========================================================*) (* ....................... DESCRIPTION .................... Macroscopic model of a transportation system with spatial region, temporal region, lengths and velocities of the vehicles will be of this form: ((xv, tv, xh, th) , (lng_spd_v, lng_spd_h)) xv = Starting and ending points of the length of the spatial region of type (real # real) tv = Starting and ending points of the width of the spatial region of type (real # real) xh = Starting and ending points of the length of the temporal region of type (real # real) th = Starting and ending points of the width of the temporal region of type (real # real) lng_spd_v = List containing lengths and velocities of the vehicles in the spatial region of type (real # real)list lng_spd_h = List containing lengths and velocities of the vehicles in the temporal region of type (real # real)list ...............................end..........................*) (* =========================================================*) (*==========================================================*) (* Start of the Formalization *) (*==========================================================*) new_type_abbrev ( "ts_macro_trffic_flow", `:(((real#real) # (real#real) # (real#real) # (real#real)) # ((real#real)list # (real#real)list))` );; let differ = new_definition `differ (x_t_rec:real#real) = SND (x_t_rec) - FST (x_t_rec)`;; (*==========================================================*) (* Formalization of the Relative Occupancy *) (*==========================================================*) let occ_list = new_recursive_definition list_RECURSION `(occ_list [] = []) /\ (occ_list (CONS h t) = (CONS (FST (h:real#real) / SND (h:real#real)) (occ_list t)))`;; let occ_sum = new_definition `occ_sum (L:(real#real) list) = sum (1..LENGTH L) (\i. (EL (i - 1) (occ_list L)))`;; let rel_occ_s2 = new_definition `rel_occ_s2 (((xv, tv, xh, th) , (lng_spd_v, lng_spd_h)):ts_macro_trffic_flow) = ( (occ_sum lng_spd_h) / (differ th)) `;; (*----------------------------------------------------------*) let l_list = new_recursive_definition list_RECURSION `(l_list [] = []) /\ (l_list (CONS h t) = (CONS ( FST (h:real#real)) (l_list t)))`;; let sum_l_list = new_definition `sum_l_list (L:(real#real) list) = sum(1..LENGTH L) (\i. EL (i - 1) (l_list L))`;; let rel_occ_s1 = new_definition `rel_occ_s1 (((xv, tv, xh, th) , (lng_spd_v, lng_spd_h)):ts_macro_trffic_flow) = ( (sum_l_list lng_spd_v) / (differ xv)) `;; (*==========================================================*) (* Formalization of the flow rate *) (*==========================================================*) let v_list = new_recursive_definition list_RECURSION `(v_list [] = []) /\ (v_list (CONS h t) = (CONS ( SND (h:real#real)) (v_list t)))`;; let sum_v_list = new_definition `sum_v_list (L:(real#real) list) = sum(1..LENGTH L) (\i. EL (i - 1) (v_list L))`;; let no_veh = new_definition `no_veh (L:(real#real) list) = LENGTH (L)`;; let flow_rate_s2 = new_definition `flow_rate_s2 (((xv, tv, xh, th) , (lng_spd_v, lng_spd_h)):ts_macro_trffic_flow) = (((&(no_veh lng_spd_h)) * (differ xh)) / ((differ th) * (differ xh))) `;; let flow_rate_s1 = new_definition `flow_rate_s1 (((xv, tv, xh, th) , (lng_spd_v, lng_spd_h)):ts_macro_trffic_flow) = ((sum_v_list lng_spd_v) / (differ xv)) `;; (*==========================================================*) (* Formalization of the density *) (*==========================================================*) let v_inv_list = new_recursive_definition list_RECURSION `(v_inv_list [] = []) /\ (v_inv_list (CONS h t) = (CONS (&1 / SND (h:real#real)) (v_inv_list t)))`;; let sum_v_inv = new_definition `sum_v_inv (L:(real#real) list) = sum(1..LENGTH L) (\i. EL (i - 1) (v_inv_list L))`;; let density_s1 = new_definition `density_s1 (((xv, tv, xh, th) , (lng_spd_v, lng_spd_h)):ts_macro_trffic_flow) = (((&(no_veh lng_spd_v)) * (differ tv)) / ((differ xv) * (differ tv))) `;; let density_s2 = new_definition `density_s2 (((xv, tv, xh, th) , (lng_spd_v, lng_spd_h)):ts_macro_trffic_flow) = ((sum_v_inv lng_spd_h) / (differ th) ) `;; (*==========================================================*) (* Formalization of the mean speed *) (*==========================================================*) let mean_speed_s1 = new_definition `mean_speed_s1 (((xv, tv, xh, th) , (lng_spd_v, lng_spd_h)):ts_macro_trffic_flow) = (flow_rate_s1 (((xv, tv, xh, th) , (lng_spd_v, lng_spd_h)):ts_macro_trffic_flow) / (density_s1 (((xv, tv, xh, th) , (lng_spd_v, lng_spd_h)):ts_macro_trffic_flow)) ) `;; let mean_speed_s2 = new_definition `mean_speed_s2 (((xv, tv, xh, th) , (lng_spd_v, lng_spd_h)):ts_macro_trffic_flow) = (flow_rate_s2 (((xv, tv, xh, th) , (lng_spd_v, lng_spd_h)):ts_macro_trffic_flow) / (density_s2 (((xv, tv, xh, th) , (lng_spd_v, lng_spd_h)):ts_macro_trffic_flow)) ) `;; (*==========================================================*) (* Some Supporting Theorems *) (*==========================================================*) (*----------------------------------------------*) (* REAL_RMUL_EQ *) (*----------------------------------------------*) g `!x y:real z. (&0 < z) ==> ((x * z = y * z) = (x = y))`;; e (REPEAT STRIP_TAC);; e (EQ_TAC);; e (POP_ASSUM MP_TAC);; e (SIMPLE_COMPLEX_ARITH_TAC);; e (POP_ASSUM MP_TAC);; e (SIMPLE_COMPLEX_ARITH_TAC);; let REAL_RMUL_EQ = top_thm ();; (*----------------------------------------------*) (* NULL_EQ *) (*----------------------------------------------*) g `!l. NULL l = (l = [])`;; e (LIST_INDUCT_TAC);; e (REWRITE_TAC [NULL]);; e (REWRITE_TAC [NULL]);; e (REWRITE_TAC [NOT_CONS_NIL]);; let NULL_EQ = top_thm ();; (*----------------------------------------------*) (* LENGTH_NOT_NULL *) (*----------------------------------------------*) g `!l. 0 < LENGTH l <=> ~NULL l`;; e (LIST_INDUCT_TAC);; e (SIMP_TAC []);; e (EQ_TAC);; e (REWRITE_TAC [LENGTH]);; e (ARITH_TAC);; e (REWRITE_TAC [NULL]);; e (REWRITE_TAC [NULL]);; e (REWRITE_TAC [LENGTH]);; e (REWRITE_TAC [LT_0]);; let LENGTH_NOT_NULL = top_thm ();; (*----------------------------------------------*) (* LENGTH_EQ_LIST *) (*----------------------------------------------*) g `! (L:(real#real) list). LENGTH L = LENGTH (l_list L)`;; e (LIST_INDUCT_TAC);; e (REWRITE_TAC [l_list]);; e (SIMP_TAC [LENGTH]);; e (REWRITE_TAC [l_list]);; e (SIMP_TAC [LENGTH]);; e (REWRITE_TAC [ADD1]);; e (ASM_REWRITE_TAC []);; let LENGTH_EQ_LIST = top_thm ();; (*==========================================================*) (* Theorem 01 *) (*==========================================================*) (*----------------------------------------------*) (* LEMMA_THM1 *) (*----------------------------------------------*) g `!c (L:real list). ~(NULL L) /\ (!i. (EL i L) = (c:real)) ==> (sum (1..LENGTH L) (\i. EL (i - 1) L) = &(LENGTH L) * c)`;; e (GEN_TAC);; e (LIST_INDUCT_TAC);; e (STRIP_TAC);; e (POP_ASSUM (K ALL_TAC));; e (POP_ASSUM MP_TAC);; e (REWRITE_TAC [NULL]);; e (REPEAT STRIP_TAC);; e (ASM_REWRITE_TAC []);; e (REWRITE_TAC [LENGTH]);; e (SUBGOAL_THEN `(!i. EL i t = (c:real))` ASSUME_TAC);; e (REPEAT STRIP_TAC);; e (POP_ASSUM MP_TAC);; e (DISCH_THEN (MP_TAC o SPEC `SUC i`));; e (REWRITE_TAC [EL]);; e (REWRITE_TAC [TL]);; e (UNDISCH_TAC `~NULL t /\ (!i. EL i t = c) ==> sum (0..LENGTH t) (\i. EL i t) = &(LENGTH t) * c`);; e (ASM_REWRITE_TAC []);; e (ASM_CASES_TAC `NULL (t:real list)`);; e (POP_ASSUM MP_TAC);; e (REWRITE_TAC [NULL_EQ]);; e (DISCH_TAC);; e (ASM_REWRITE_TAC []);; e (REWRITE_TAC [LENGTH]);; e (REWRITE_TAC [ADD1]);; e (SUBGOAL_THEN `0 + 1 = 1` ASSUME_TAC);; e (ARITH_TAC);; e (ASM_REWRITE_TAC []);; e (REWRITE_TAC [SUM_1]);; e (REAL_ARITH_TAC);; e (UNDISCH_TAC `~NULL t /\ (!i. EL i t = c) ==> sum (1..LENGTH t) (\i. EL (i - 1) t) = &(LENGTH t) * c`);; e (ASM_REWRITE_TAC []);; e (DISCH_TAC);; e (REWRITE_TAC [SUM_CLAUSES_NUMSEG]);; e (COND_CASES_TAC);; e (REWRITE_TAC [ADD1]);; e (REWRITE_TAC [GSYM REAL_OF_NUM_ADD]);; e (REWRITE_TAC [REAL_ADD_RDISTRIB]);; e (REWRITE_TAC [REAL_ARITH `&1 * c = c`]);; e (ASM_REWRITE_TAC [REAL_LE_RADD]);; e (POP_ASSUM MP_TAC);; e (REWRITE_TAC [NOT_LE]);; e (UNDISCH_TAC `~NULL (t:real list)`);; e (REWRITE_TAC [GSYM LENGTH_NOT_NULL]);; e (ARITH_TAC);; let LEMMA_THM1 = top_thm ();; (*----------------------------------------------*) (* REL_OCC_DEN_REL_S1 *) (*----------------------------------------------*) g `! xv tv xh th lng_spd_v lng_spd_h c. ~(NULL lng_spd_v) /\ (&0 < SND xv - FST xv) /\ (&0 < SND tv - FST tv) /\ (!i. (EL i (l_list lng_spd_v)) = c) ==> rel_occ_s1 (((xv,tv,xh,th),lng_spd_v,lng_spd_h):ts_macro_trffic_flow) = c * density_s1 ((xv,tv,xh,th),lng_spd_v,lng_spd_h)`;; e (REWRITE_TAC [rel_occ_s1; density_s1]);; e (REWRITE_TAC [sum_l_list; no_veh; differ]);; e (REPEAT STRIP_TAC);; e (REWRITE_TAC [real_div]);; e (REWRITE_TAC [REAL_INV_MUL]);; e (SUBGOAL_THEN `((SND tv:real - FST tv) * inv (SND xv - FST xv) * inv (SND tv - FST tv)) = inv (SND xv - FST xv)` ASSUME_TAC);; e (REWRITE_TAC [REAL_ARITH `!x y. ((x:real) * y * inv (x)) = ((x * inv x) * y)`]);; e (SUBGOAL_THEN `((SND tv - FST tv) * inv (SND tv - FST tv)) = &1` ASSUME_TAC);; e (MATCH_MP_TAC REAL_MUL_RINV);; e (REWRITE_TAC [REAL_NOT_EQ]);; e (DISJ2_TAC);; e (ASM_REAL_ARITH_TAC);; e (ASM_REWRITE_TAC []);; e (REAL_ARITH_TAC);; e (POP_ASSUM MP_TAC);; e (SIMP_TAC [GSYM REAL_MUL_ASSOC]);; e (DISCH_TAC);; e (POP_ASSUM (K ALL_TAC));; e (SIMP_TAC [REAL_MUL_ASSOC]);; e (REWRITE_TAC [REAL_EQ_MUL_RCANCEL]);; e (DISJ1_TAC);; e (ONCE_REWRITE_TAC [REAL_MUL_SYM]);; e (REWRITE_TAC [LENGTH_EQ_LIST]);; e (MATCH_MP_TAC LEMMA_THM1);; e (ASM_REWRITE_TAC []);; e (REWRITE_TAC [GSYM LENGTH_NOT_NULL]);; e (REWRITE_TAC [GSYM LENGTH_EQ_LIST]);; e (REWRITE_TAC [LENGTH_NOT_NULL]);; e (ASM_REWRITE_TAC []);; let REL_OCC_DEN_REL_S1 = top_thm ();; (*==========================================================*) (* Theorem 02 *) (*==========================================================*) (*----------------------------------------------*) (* LEMMA1_THM2 *) (*----------------------------------------------*) g `!c L n. ~(NULL L) /\ (!i. FST (EL i L) = c) /\ (1 <= n) /\ (n <= LENGTH L) ==> (EL (n - 1) (occ_list L) = c * EL (n - 1) (v_inv_list L))`;; e (GEN_TAC);; e (LIST_INDUCT_TAC);; e (REWRITE_TAC [NULL]);; e (INDUCT_TAC);; e (REPEAT STRIP_TAC);; e (ASM_ARITH_TAC);; e (REPEAT STRIP_TAC);; e (UNDISCH_TAC `1 <= SUC n`);; e (REWRITE_TAC [LE]);; e (REPEAT STRIP_TAC);; e (POP_ASSUM MP_TAC);; e (ONCE_REWRITE_TAC [EQ_SYM_EQ]);; e (SIMP_TAC []);; e (DISCH_TAC);; e (SUBGOAL_THEN `1 - 1 = 0` ASSUME_TAC);; e (ARITH_TAC);; e (ASM_REWRITE_TAC []);; e (REWRITE_TAC [occ_list; v_inv_list]);; e (REWRITE_TAC [EL]);; e (REWRITE_TAC [HD]);; e (UNDISCH_TAC `!i. FST (EL i (CONS h (t:(real#real) list))) = c`);; e (DISCH_THEN (MP_TAC o SPEC `0`));; e (REWRITE_TAC [EL]);; e (REWRITE_TAC [HD]);; e (DISCH_TAC);; e (ASM_REWRITE_TAC []);; e (REAL_ARITH_TAC);; e (SUBGOAL_THEN `(SUC n - 1) = (SUC (n - 1))` ASSUME_TAC);; e (ASM_ARITH_TAC);; e (ASM_REWRITE_TAC []);; e (REWRITE_TAC [occ_list; v_inv_list]);; e (REWRITE_TAC [EL]);; e (REWRITE_TAC [TL]);; e (ASM_CASES_TAC `NULL (t:(real#real) list)`);; e (POP_ASSUM MP_TAC);; e (REWRITE_TAC [NULL_EQ]);; e (DISCH_TAC);; e (ASM_REWRITE_TAC []);; e (REWRITE_TAC [occ_list; v_inv_list]);; e (UNDISCH_TAC `SUC n <= LENGTH (CONS h (t:(real#real) list))`);; e (REWRITE_TAC [LENGTH]);; e (REWRITE_TAC [LE_SUC]);; e (ASM_REWRITE_TAC []);; e (REWRITE_TAC [LENGTH]);; e (UNDISCH_TAC `1 <= n`);; e (ARITH_TAC);; e (UNDISCH_TAC `!n. ~NULL t /\ (!i. FST (EL i (t:(real#real) list)) = c) /\ 1 <= n /\ n <= LENGTH t ==> EL (n - 1) (occ_list t) = c * EL (n - 1) (v_inv_list t)`);; e (DISCH_THEN (MP_TAC o SPEC `n:num`));; e (ASM_REWRITE_TAC []);; e (SUBGOAL_THEN `(!i. FST (EL i (t:(real#real) list)) = c)` ASSUME_TAC);; e (STRIP_TAC);; e (UNDISCH_TAC `!i. FST (EL i (CONS h (t:(real#real) list))) = c`);; e (DISCH_THEN (MP_TAC o SPEC `SUC (i:num)`));; e (REWRITE_TAC [EL]);; e (REWRITE_TAC [TL]);; e (SIMP_TAC []);; e (ASM_REWRITE_TAC []);; e (UNDISCH_TAC `SUC n <= LENGTH (CONS h (t:(real#real) list))`);; e (REWRITE_TAC [LENGTH; LE_SUC]);; e (SIMP_TAC []);; let LEMMA1_THM2 = top_thm ();; (*----------------------------------------------*) (* LEMMA2_THM2 *) (*----------------------------------------------*) g `!c L. ~(NULL L) /\ (!i. FST (EL i L) = c) ==> (sum (1..LENGTH L) (\i. EL (i - 1) (occ_list L)) = sum (1..LENGTH L) (\x. c * EL (x - 1) (v_inv_list L)))`;; e (REPEAT STRIP_TAC);; e (MATCH_MP_TAC SUM_EQ_NUMSEG);; e (REPEAT STRIP_TAC);; e (SIMP_TAC []);; e (MATCH_MP_TAC LEMMA1_THM2);; e (ASM_SIMP_TAC []);; let LEMMA2_THM2 = top_thm ();; (*----------------------------------------------*) (* REL_OCC_DEN_REL_S2 *) (*----------------------------------------------*) g `!xv tv xh th lng_spd_v lng_spd_h c. ~(NULL lng_spd_h) /\ (&0 < SND th - FST th) /\ (&0 < SND xh - FST xh) /\ (!i. FST (EL i lng_spd_h) = c) ==> rel_occ_s2 (((xv,tv,xh,th),lng_spd_v,lng_spd_h):ts_macro_trffic_flow) = c * density_s2 ((xv,tv,xh,th),lng_spd_v,lng_spd_h)`;; e (REWRITE_TAC [rel_occ_s2; density_s2]);; e (REWRITE_TAC [occ_sum; sum_v_inv; differ]);; e (REPEAT STRIP_TAC);; e (REWRITE_TAC [real_div]);; e (SIMP_TAC [REAL_MUL_ASSOC]);; e (REWRITE_TAC [REAL_EQ_MUL_RCANCEL]);; e (DISJ1_TAC);; e (REWRITE_TAC [GSYM SUM_LMUL]);; e (MATCH_MP_TAC LEMMA2_THM2);; e (ASM_SIMP_TAC []);; let REL_OCC_DEN_REL_S2 = top_thm ();; (*==========================================================*) (*==========================================================*) (* Application to German Freeway *) (*==========================================================*) (*==========================================================*) (* Theorem 04 *) (*==========================================================*) let german_freeway_lane_1 = new_definition ` german_freeway_lane_1 xv tv xh th L11v V11v L12v V12v L11h V11h L12h V12h = ((xv, tv, xh, th), ([(L11v, V11v); (L12v, V12v)], [(L11h, V11h); (L12h, V12h)]))`;; let german_freeway_lane_2 = new_definition ` german_freeway_lane_2 xv tv xh th L21v V21v L22v V22v L23v V23v L21h V21h L22h V22h L23h V23h = ((xv, tv, xh, th), ([(L21v, V21v); (L22v, V22v); (L23v, V23v)], [(L21h, V21h); (L22h, V22h); (L23h, V23h)]))`;; let german_freeway_lane_3 = new_definition ` german_freeway_lane_3 xv tv xh th L31v V31v L32v V32v L33v V33v L34v V34v L31h V31h L32h V32h L33h V33h L34h V34h = ((xv, tv, xh, th), ([(L31v, V31v); (L32v, V32v); (L33v, V33v); (L34v, V34v)], [(L31h, V31h); (L32h, V32h); (L33h, V33h); (L34h, V34h)]))`;; (*==========================================================*) (* First Property *) (*==========================================================*) (* LANE_AVERAGED_TRFFIC_FLOW *) (*==========================================================*) g `!xv tv xh th L11v V11v L12v V12v L11h V11h L12h V12h L21v V21v L22v V22v L23v V23v L21h V21h L22h V22h L23h V23h L31v V31v L32v V32v L33v V33v L34v V34v L31h V31h L32h V32h L33h V33h L34h V34h. (&0 < SND xh - FST xh) /\ (&0 < SND th - FST th) /\ (L = 3) ==> sum(1..L) (\i. EL (i - 1) [ ((flow_rate_s2 (german_freeway_lane_1 xv tv xh th L11v V11v L12v V12v L11h V11h L12h V12h)) / &L) ; ((flow_rate_s2 (german_freeway_lane_2 xv tv xh th L21v V21v L22v V22v L23v V23v L21h V21h L22h V22h L23h V23h):real ) / &L); ((flow_rate_s2 (german_freeway_lane_3 xv tv xh th L31v V31v L32v V32v L33v V33v L34v V34v L31h V31h L32h V32h L33h V33h L34h V34h)) / &L) ]) = (&9 / (&L * (SND th - FST th)))`;; e (REPEAT STRIP_TAC);; e (REWRITE_TAC [german_freeway_lane_1; german_freeway_lane_2; german_freeway_lane_3]);; e (REWRITE_TAC [flow_rate_s2]);; e (REWRITE_TAC [no_veh]);; e (REWRITE_TAC [differ]);; e (REWRITE_TAC [LENGTH]);; e (REWRITE_TAC [real_div]);; e (REWRITE_TAC [REAL_INV_MUL]);; e (SIMP_TAC [GSYM REAL_MUL_ASSOC]);; e (SUBGOAL_THEN `((SND xh - FST xh) * inv (SND th - FST th) * inv (SND xh - FST xh) * inv (&L)) = ((SND xh - FST xh) * inv (SND th - FST th) * inv (SND xh - FST xh)) * inv (&L)` ASSUME_TAC);; e (REAL_ARITH_TAC);; e (ASM_SIMP_TAC []);; e (POP_ASSUM (K ALL_TAC));; e (SUBGOAL_THEN `((SND xh:real - FST xh) * inv (SND th - FST th) * inv (SND xh - FST xh)) = inv (SND th - FST th)` ASSUME_TAC);; e (REWRITE_TAC [REAL_ARITH `!x y. ((x:real) * y * inv (x)) = ((x * inv x) * y)`]);; e (SUBGOAL_THEN `((SND xh - FST xh) * inv (SND xh - FST xh)) = &1` ASSUME_TAC);; e (MATCH_MP_TAC REAL_MUL_RINV);; e (REWRITE_TAC [REAL_NOT_EQ]);; e (DISJ2_TAC);; e (ASM_REAL_ARITH_TAC);; e (ASM_REWRITE_TAC []);; e (REAL_ARITH_TAC);; e (ASM_SIMP_TAC []);; e (POP_ASSUM (K ALL_TAC));; e (REWRITE_TAC [GSYM ONE]);; e (REWRITE_TAC [GSYM TWO]);; e (REWRITE_TAC [ADD1]);; e (REWRITE_TAC [GSYM REAL_OF_NUM_ADD]);; e (REWRITE_TAC [REAL_ARITH `(&2 + &1) = &3`]);; e (REWRITE_TAC [REAL_ARITH `(&3 + &1) = &4`]);; e (REWRITE_TAC [SUM_3]);; e (SUBGOAL_THEN `((1 - 1) = 0) /\ ((2 - 1) = 1) /\ ((3 - 1) = 2)` ASSUME_TAC);; e (ARITH_TAC);; e (ASM_SIMP_TAC []);; e (POP_ASSUM (K ALL_TAC));; e (REWRITE_TAC [EL]);; e (REWRITE_TAC [HD]);; e (REWRITE_TAC [ONE; TWO]);; e (REWRITE_TAC [EL]);; e (REWRITE_TAC [HD; TL]);; e (REWRITE_TAC [GSYM ONE; GSYM TWO]);; e (REAL_ARITH_TAC);; let LANE_AVERAGED_TRFFIC_FLOW = top_thm ();; (*==========================================================*) (*----------------------------------------------*) (* SUM_4 *) (*----------------------------------------------*) let SUM_4 = prove (`!t. sum(1..4) t = t(1) + t(2) + t(3) + t(4)`, REWRITE_TAC[num_CONV `4`; num_CONV `3`; num_CONV `2`; SUM_CLAUSES_NUMSEG] THEN REWRITE_TAC[SUM_SING_NUMSEG; ARITH; REAL_ADD_ASSOC]);; (*==========================================================*) (* Second Property *) (*==========================================================*) (* LANE_AVE_MEAN_SPEED *) (*==========================================================*) g `! xv tv xh th L11v V11v L12v V12v L11h V11h L12h V12h L21v V21v L22v V22v L23v V23v L21h V21h L22h V22h L23h V23h L31v V31v L32v V32v L33v V33v L34v V34v L31h V31h L32h V32h L33h V33h L34h V34h. (&0 < SND xh - FST xh) /\ (&0 < SND th - FST th) /\ (L = 3) ==> sum(1..L) (\i. EL (i - 1) [ (( ( (&1 / &L) * (flow_rate_s2 (german_freeway_lane_1 xv tv xh th L11v V11v L12v V12v L11h V11h L12h V12h)) ) * (mean_speed_s2 (german_freeway_lane_1 xv tv xh th L11v V11v L12v V12v L11h V11h L12h V12h))) / ( sum(1..L) (\i. EL (i - 1) [ ((flow_rate_s2 (german_freeway_lane_1 xv tv xh th L11v V11v L12v V12v L11h V11h L12h V12h)) / &L) ; ((flow_rate_s2 (german_freeway_lane_2 xv tv xh th L21v V21v L22v V22v L23v V23v L21h V21h L22h V22h L23h V23h):real ) / &L); ((flow_rate_s2 (german_freeway_lane_3 xv tv xh th L31v V31v L32v V32v L33v V33v L34v V34v L31h V31h L32h V32h L33h V33h L34h V34h)) / &L) ]) ) ) ; (( ( (&1 / &L) * (flow_rate_s2 (german_freeway_lane_2 xv tv xh th L21v V21v L22v V22v L23v V23v L21h V21h L22h V22h L23h V23h):real) ) * (mean_speed_s2 (german_freeway_lane_2 xv tv xh th L21v V21v L22v V22v L23v V23v L21h V21h L22h V22h L23h V23h))) / ( sum(1..L) (\i. EL (i - 1) [ ((flow_rate_s2 (german_freeway_lane_1 xv tv xh th L11v V11v L12v V12v L11h V11h L12h V12h)) / &L) ; ((flow_rate_s2 (german_freeway_lane_2 xv tv xh th L21v V21v L22v V22v L23v V23v L21h V21h L22h V22h L23h V23h):real ) / &L); ((flow_rate_s2 (german_freeway_lane_3 xv tv xh th L31v V31v L32v V32v L33v V33v L34v V34v L31h V31h L32h V32h L33h V33h L34h V34h)) / &L) ]) ) ); (( ( (&1 / &L) * (flow_rate_s2 (german_freeway_lane_3 xv tv xh th L31v V31v L32v V32v L33v V33v L34v V34v L31h V31h L32h V32h L33h V33h L34h V34h)) ) * (mean_speed_s2 (german_freeway_lane_3 xv tv xh th L31v V31v L32v V32v L33v V33v L34v V34v L31h V31h L32h V32h L33h V33h L34h V34h))) / ( sum(1..L) (\i. EL (i - 1) [ ((flow_rate_s2 (german_freeway_lane_1 xv tv xh th L11v V11v L12v V12v L11h V11h L12h V12h)) / &L) ; ((flow_rate_s2 (german_freeway_lane_2 xv tv xh th L21v V21v L22v V22v L23v V23v L21h V21h L22h V22h L23h V23h):real ) / &L); ((flow_rate_s2 (german_freeway_lane_3 xv tv xh th L31v V31v L32v V32v L33v V33v L34v V34v L31h V31h L32h V32h L33h V33h L34h V34h)) / &L) ])) ) ]) = ( &4 * inv (&9) * inv (inv V11h + inv V12h) + inv (inv V21h + inv V22h + inv V23h) + ( &16 * inv (&9)) * inv (inv V31h + inv V32h + inv V33h + inv V34h) )`;; e (REPEAT STRIP_TAC);; e (ASM_SIMP_TAC [LANE_AVERAGED_TRFFIC_FLOW]);; e (REWRITE_TAC [GSYM REAL_MUL_ASSOC]);; e (REWRITE_TAC [german_freeway_lane_1; german_freeway_lane_2; german_freeway_lane_3]);; e (REWRITE_TAC [flow_rate_s2; mean_speed_s2]);; e (REWRITE_TAC [no_veh]);; e (REWRITE_TAC [differ]);; e (REWRITE_TAC [density_s2]);; e (REWRITE_TAC [LENGTH]);; e (REWRITE_TAC [real_div]);; e (REWRITE_TAC [REAL_INV_MUL]);; e (SIMP_TAC [GSYM REAL_MUL_ASSOC]);; e (SUBGOAL_THEN `!(i:num). ((SND xh:real - FST xh) * inv (SND th - FST th) * inv (SND xh - FST xh)) = inv (SND th - FST th)` ASSUME_TAC);; e (GEN_TAC);; e (REWRITE_TAC [REAL_ARITH `!x y. ((x:real) * y * inv (x)) = ((x * inv x) * y)`]);; e (SUBGOAL_THEN `((SND xh - FST xh) * inv (SND xh - FST xh)) = &1` ASSUME_TAC);; e (MATCH_MP_TAC REAL_MUL_RINV);; e (REWRITE_TAC [REAL_NOT_EQ]);; e (DISJ2_TAC);; e (ASM_REAL_ARITH_TAC);; e (ASM_REWRITE_TAC []);; e (REAL_ARITH_TAC);; e (ASM_SIMP_TAC []);; e (POP_ASSUM (K ALL_TAC));; e (REWRITE_TAC [sum_v_inv]);; e (REWRITE_TAC [LENGTH]);; e (REWRITE_TAC [differ]);; e (REWRITE_TAC [ADD1]);; e (REWRITE_TAC [GSYM REAL_OF_NUM_ADD]);; e (REWRITE_TAC [v_inv_list]);; e (REWRITE_TAC [real_div]);; e (REWRITE_TAC [REAL_ARITH `(((&0 + &1) + &1)) = &2`]);; e (REWRITE_TAC [REAL_ARITH `(&2 + &1) = &3`]);; e (REWRITE_TAC [REAL_ARITH `(&3 + &1) = &4`]);; e (SUBGOAL_THEN `(((0 + 1) + 1) = 2) /\ ((((0 + 1) + 1) + 1) = 3) /\ (((((0 + 1) + 1) + 1) + 1) = 4)` ASSUME_TAC);; e (ARITH_TAC);; e (ASM_SIMP_TAC []);; e (POP_ASSUM (K ALL_TAC));; e (REWRITE_TAC [REAL_ARITH `!x. &1 * x = x`]);; e (REWRITE_TAC [SUM_3]);; e (SUBGOAL_THEN `((1 - 1) = 0) /\ ((2 - 1) = 1) /\ ((3 - 1) = 2)` ASSUME_TAC);; e (ARITH_TAC);; e (ASM_SIMP_TAC []);; e (POP_ASSUM (K ALL_TAC));; e (REWRITE_TAC [EL]);; e (REWRITE_TAC [HD]);; e (REWRITE_TAC [SUM_2]);; e (SUBGOAL_THEN `((1 - 1) = 0) /\ ((2 - 1) = 1) /\ ((3 - 1) = 2)` ASSUME_TAC);; e (ARITH_TAC);; e (ASM_SIMP_TAC []);; e (POP_ASSUM (K ALL_TAC));; e (REWRITE_TAC [EL]);; e (REWRITE_TAC [HD]);; e (ONCE_REWRITE_TAC [ONE]);; e (REWRITE_TAC [EL]);; e (REWRITE_TAC [TWO]);; e (REWRITE_TAC [EL]);; e (REWRITE_TAC [TL]);; e (REWRITE_TAC [HD]);; e (ONCE_REWRITE_TAC [ONE]);; e (REWRITE_TAC [EL]);; e (REWRITE_TAC [TL]);; e (REWRITE_TAC [HD]);; e (REWRITE_TAC [GSYM ONE]);; e (REWRITE_TAC [GSYM TWO]);; e (REWRITE_TAC [REAL_INV_INV]);; e (SUBGOAL_THEN `( &2 * (SND xh - FST xh) * inv (SND th - FST th) * inv (SND xh - FST xh) * &2 * (SND xh - FST xh) * inv (SND th - FST th) * inv (SND xh - FST xh) * inv (inv V11h + inv V12h) * (SND th - FST th) * inv (&9) * &3 * (SND th - FST th)) = ((&12) * ((SND xh - FST xh) * inv (SND xh - FST xh)) * ((SND xh - FST xh) * inv (SND xh - FST xh)) * ((SND th - FST th) * inv (SND th - FST th)) * ((SND th - FST th) * inv (SND th - FST th)) * inv (&9) * inv (inv V11h + inv V12h) )` ASSUME_TAC);; e (REAL_ARITH_TAC);; e (ASM_REWRITE_TAC []);; e (POP_ASSUM (K ALL_TAC));; e (SUBGOAL_THEN `((SND xh - FST xh) * inv (SND xh - FST xh)) = &1` ASSUME_TAC);; e (MATCH_MP_TAC REAL_MUL_RINV);; e (REWRITE_TAC [REAL_NOT_EQ]);; e (DISJ2_TAC);; e (ASM_REAL_ARITH_TAC);; e (ASM_REWRITE_TAC []);; e (POP_ASSUM (K ALL_TAC));; e (SUBGOAL_THEN `((SND th - FST th) * inv (SND th - FST th)) = &1` ASSUME_TAC);; e (MATCH_MP_TAC REAL_MUL_RINV);; e (REWRITE_TAC [REAL_NOT_EQ]);; e (DISJ2_TAC);; e (ASM_REAL_ARITH_TAC);; e (ASM_REWRITE_TAC []);; e (POP_ASSUM (K ALL_TAC));; e (SUBGOAL_THEN `(&3 * (SND xh - FST xh) * inv (SND th - FST th) * inv (SND xh - FST xh) * &3 * (SND xh - FST xh) * inv (SND th - FST th) * inv (SND xh - FST xh) * inv (inv V21h + inv V22h + inv V23h) * (SND th - FST th) * inv (&9) * &3 * (SND th - FST th) ) = ((&3 * &3 * &3 * inv (&9)) * ((SND xh - FST xh) * inv (SND xh - FST xh)) * ((SND xh - FST xh) * inv (SND xh - FST xh)) * ((SND th - FST th) * inv (SND th - FST th)) * ((SND th - FST th) * inv (SND th - FST th)) * inv (inv V21h + inv V22h + inv V23h) )` ASSUME_TAC);; e (REAL_ARITH_TAC);; e (ASM_REWRITE_TAC []);; e (POP_ASSUM (K ALL_TAC));; e (SUBGOAL_THEN `((SND xh - FST xh) * inv (SND xh - FST xh)) = &1` ASSUME_TAC);; e (MATCH_MP_TAC REAL_MUL_RINV);; e (REWRITE_TAC [REAL_NOT_EQ]);; e (DISJ2_TAC);; e (ASM_REAL_ARITH_TAC);; e (ASM_REWRITE_TAC []);; e (POP_ASSUM (K ALL_TAC));; e (SUBGOAL_THEN `((SND th - FST th) * inv (SND th - FST th)) = &1` ASSUME_TAC);; e (MATCH_MP_TAC REAL_MUL_RINV);; e (REWRITE_TAC [REAL_NOT_EQ]);; e (DISJ2_TAC);; e (ASM_REAL_ARITH_TAC);; e (ASM_REWRITE_TAC []);; e (POP_ASSUM (K ALL_TAC));; e (REWRITE_TAC [SUM_4]);; e (SUBGOAL_THEN `((1 - 1) = 0) /\ ((2 - 1) = 1) /\ ((3 - 1) = 2) /\ ((4 - 1) = 3)` ASSUME_TAC);; e (ARITH_TAC);; e (ASM_SIMP_TAC []);; e (POP_ASSUM (K ALL_TAC));; e (REWRITE_TAC [EL]);; e (REWRITE_TAC [HD]);; e (ONCE_REWRITE_TAC [ONE]);; e (REWRITE_TAC [EL]);; e (REWRITE_TAC [TL]);; e (REWRITE_TAC [HD]);; e (REWRITE_TAC [TWO]);; e (REWRITE_TAC [EL]);; e (ONCE_REWRITE_TAC [ONE]);; e (REWRITE_TAC [EL]);; e (REWRITE_TAC [TL]);; e (REWRITE_TAC [HD]);; e (ONCE_REWRITE_TAC [GSYM ONE]);; e (REWRITE_TAC [REAL_ARITH `(&12 * &1 * &1 * &1 * &1 * inv (&9) * inv (inv V11h + inv V12h)) = ( &12 * inv (&9) * inv (inv V11h + inv V12h) )`]);; e (REWRITE_TAC [REAL_ARITH `((&3 * &3 * &3 * inv (&9)) * &1 * &1 * &1 * &1 * inv (inv V21h + inv V22h + inv V23h) ) = ( (&3 * &3 * &3 * inv (&9)) * inv (inv V21h + inv V22h + inv V23h) )`]);; e (SUBGOAL_THEN `3 = (2 + 1)` ASSUME_TAC);; e (ARITH_TAC);; e (ASM_SIMP_TAC []);; e (REWRITE_TAC [GSYM ADD1]);; e (REWRITE_TAC [EL]);; e (REWRITE_TAC [TL]);; e (REWRITE_TAC [TWO]);; e (REWRITE_TAC [EL]);; e (ONCE_REWRITE_TAC [ONE]);; e (REWRITE_TAC [EL]);; e (REWRITE_TAC [TL]);; e (REWRITE_TAC [ADD1]);; e (REWRITE_TAC [HD]);; e (SUBGOAL_THEN `(((((0 + 1) + 1) + 1)) = 3)` ASSUME_TAC);; e (ARITH_TAC);; e (ASM_SIMP_TAC []);; e (SUBGOAL_THEN `((2 + 1) = 3)` ASSUME_TAC);; e (ARITH_TAC);; e (ONCE_ASM_REWRITE_TAC []);; e (SUBGOAL_THEN `(&4 * (SND xh - FST xh) * inv (SND th - FST th) * inv (SND xh - FST xh) * &4 * (SND xh - FST xh) * inv (SND th - FST th) * inv (SND xh - FST xh) * inv (inv V31h + inv V32h + inv V33h + inv V34h) * (SND th - FST th) * inv (&9) * &3 * (SND th - FST th)) = ( (&4 * &4 * &3 * inv (&9)) * ((SND xh - FST xh) * inv (SND xh - FST xh)) * ((SND xh - FST xh) * inv (SND xh - FST xh)) * ((SND th - FST th) * inv (SND th - FST th)) * ((SND th - FST th) * inv (SND th - FST th)) * inv (inv V31h + inv V32h + inv V33h + inv V34h) )` ASSUME_TAC);; e (REAL_ARITH_TAC);; e (ONCE_ASM_REWRITE_TAC []);; e (POP_ASSUM (K ALL_TAC));; e (SUBGOAL_THEN `((SND xh - FST xh) * inv (SND xh - FST xh)) = &1` ASSUME_TAC);; e (MATCH_MP_TAC REAL_MUL_RINV);; e (REWRITE_TAC [REAL_NOT_EQ]);; e (DISJ2_TAC);; e (ASM_REAL_ARITH_TAC);; e (ONCE_ASM_REWRITE_TAC []);; e (POP_ASSUM (K ALL_TAC));; e (SUBGOAL_THEN `((SND th - FST th) * inv (SND th - FST th)) = &1` ASSUME_TAC);; e (MATCH_MP_TAC REAL_MUL_RINV);; e (REWRITE_TAC [REAL_NOT_EQ]);; e (DISJ2_TAC);; e (ASM_REAL_ARITH_TAC);; e (ONCE_ASM_REWRITE_TAC []);; e (POP_ASSUM (K ALL_TAC));; e (REWRITE_TAC [REAL_ARITH `!x. &1 * x = x`]);; e (ONCE_ASM_REWRITE_TAC []);; e (ONCE_ASM_REWRITE_TAC []);; e (POP_ASSUM MP_TAC);; e (POP_ASSUM (K ALL_TAC));; e (POP_ASSUM (K ALL_TAC));; e (SIMP_TAC []);; e (DISCH_TAC);; e (POP_ASSUM (K ALL_TAC));; e (SUBGOAL_THEN `((inv (&3) * &12 * inv (&9)) = &4 * inv (&9)) /\ (inv (&3) * (&3 * &3 * &3 * inv (&9)) = &1) /\ ((inv (&3) * (&4 * &4 * &3 * inv (&9))) = &16 * inv (&9))` ASSUME_TAC);; e (CONV_TAC REAL_FIELD);; e (ASM_REAL_ARITH_TAC);; let LANE_AVE_MEAN_SPEED = top_thm ();; (*============================================================*) (* End of the Occupancy Verification *) (*============================================================*) (*============================================================*) (*============================================================*) (*============================================================*) (*============================================================*) (* Start of the Shockwave Analysis Formalization *) (*============================================================*) (* =========================================================*) (* ....................... DESCRIPTION .................... Macroscopic model of a transportation system with flow (q), density (k) and speed ( spd = q / k ) in one region, shockwave speed (sw), denisty range in the whole area of observation (sw_d) for the shockwave analysis will be of this form: ((((q, k), spd)list, (t1, t2)), (ind_n, ind_m))list, (k1, k2) q = Flow rate of vehicles at one point in a region region of type (real) k = Density of vehicles at one point in a region region of type (real) spd = Average speed of vehicles at one point in a region region of type (real) t1 = Time point at which shockwave starts in time space diagram of type (real) t2 = Time point at which shockwave ends in time space diagram of type (real) ind_m = Starting point of a shockwave from a list of points in the regions associated with t1 of type (num) ind_n = Ending point of a shockwave from a list of points in the regions associated with t2 of type (num) k1 = Density associated with the first region in the area of consideration of type (real) k2 = Density associated with the last region in the area of consideration of type (real) ...............................end..........................*) (* =========================================================*) (*==========================================================*) (* Start of the Formalization *) (*==========================================================*) new_type_abbrev ( "ptrgn", `:((real#real) # (real))` );; new_type_abbrev ( "sw" , `:((((ptrgn)list)#(real#real))#(num#num))` );; new_type_abbrev ( "sw_d", `:(((sw)list)#(real#real))` );; (*==========================================================*) (* Indices and time points from the list of points ---*) (*==========================================================*) let pt_list = new_definition `pt_list (p:sw) = (FST(FST p)) `;; let time = new_definition `time (p:sw) = SND(SND(FST p)) - FST(SND(FST p)) `;; let ind_m = new_definition `ind_m (p:sw) = FST(SND p) `;; let ind_n = new_definition `ind_n (p:sw) = SND(SND p) `;; (*==========================================================*) (*--- q, k, shock_wv and spd at each interval point --*) (*==========================================================*) let flow_rate = new_definition `flow_rate (t:ptrgn) =(FST(FST(t)))`;; let density = new_definition `density (t:ptrgn) = (SND(FST(t)))`;; let shock_wv = new_definition `shock_wv (t:ptrgn) = (SND(t))`;; let spd = new_definition `spd (t:ptrgn) = (flow_rate (t)) / (density (t)) `;; (*------------------------------------------------------------------------- Number of vehicles crossing line (n) from area (n-1) during time period t is ----------------------------------------------------------------------------*) let n_crossing = new_definition `n_crossing (p:sw) (n:num) = (( flow_rate (EL n ( pt_list p) ) / density (EL n ( pt_list p) ) - shock_wv (EL n ( pt_list p) )) * density (EL n ( pt_list p) )) * (time p) `;; (*=================================================================*) (*--- Some Lemmas for the formalization of Shockwave analysis --*) (*=================================================================*) (*---------------------------------------------------------*) (* lemma not_equal *) (*---------------------------------------------------------*) g `!(x:real) (y:real). ~(x = y) ==> ~((x - y) = &0) `;; e(REAL_ARITH_TAC);; let NOT_EQUAL = top_thm ();; (*--------------------------------------------------*) (* lemma INV_NOT_ZERO *) (*--------------------------------------------------*) g `! (y:real) . ~(y = &0) ==> ~( inv(y) = &0) `;; e(REWRITE_TAC [REAL_NOT_EQ]);; e(REPEAT STRIP_TAC);; e(DISJ1_TAC);; e(POP_ASSUM MP_TAC);; e(REWRITE_TAC [GSYM REAL_NEG_GT0]);; e(REWRITE_TAC [GSYM REAL_INV_NEG]);; e(REWRITE_TAC [REAL_LT_INV]);; e(DISJ2_TAC);; e(POP_ASSUM MP_TAC);; e(REWRITE_TAC [REAL_LT_INV]);; let INV_NOT_ZERO = top_thm ();; (*--------------------------------------------------*) (* lemma RAT_LEMMA_Z *) (*--------------------------------------------------*) g `!(x1:real) (x2:real) (y1:real) (y2:real) . ~((y1:real) = &0) /\ ~((y2:real) = &0) ==> (x1 / y1 = x2 / y2 <=> x1 * y2 = x2 * y1)`;; e(REPEAT STRIP_TAC);; e(REWRITE_TAC [real_div]);; e(EQ_TAC);; (*----------------------------*) e(DISCH_TAC);; e(SUBGOAL_THEN ` (x1:real) * (y2:real) = (x2:real) * (y1:real) <=> (x1 * y2) * (inv (y1)) = (x2 * y1) * (inv (y1) ) ` ASSUME_TAC);; e(EQ_TAC);; e(DISCH_TAC);; e(ONCE_ASM_REWRITE_TAC []);; e(ARITH_TAC);; e(SUBGOAL_THEN ` ~(inv (y1:real) = &0)` ASSUME_TAC);; e(MATCH_MP_TAC INV_NOT_ZERO);; e(ASM_SIMP_TAC []);; e(DISCH_TAC);; e(MATCH_MP_TAC REAL_EQ_RCANCEL_IMP);; e(EXISTS_TAC `inv (y1:real)`);; e(ASM_SIMP_TAC []);; e(ASM_SIMP_TAC []);; e(REWRITE_TAC [GSYM REAL_MUL_ASSOC]);; e(REWRITE_TAC [REAL_ARITH ` (A:real) * (C) * inv(B) = ((A:real) * inv(B)) * C`]);; e(ONCE_ASM_REWRITE_TAC []);; e(REWRITE_TAC [GSYM REAL_MUL_ASSOC]);; e(ASM_SIMP_TAC[REAL_MUL_LINV]);; (*----------------------------*) e(DISCH_TAC);; e(SUBGOAL_THEN ` (x1:real) * inv (y1:real) = (x2:real) * inv (y2:real) <=> x1 * inv y1 * y2 = x2 * (inv y2) * y2 `ASSUME_TAC);; e(EQ_TAC);; e(DISCH_TAC);; e(REWRITE_TAC [ REAL_MUL_ASSOC]);; e(ONCE_ASM_REWRITE_TAC []);; e(ARITH_TAC);; e(DISCH_TAC);; e(MATCH_MP_TAC REAL_EQ_RCANCEL_IMP);; e(EXISTS_TAC `(y2:real)`);; e(ASM_SIMP_TAC [GSYM REAL_MUL_ASSOC]);; e(ONCE_ASM_REWRITE_TAC []);; e(ASM_SIMP_TAC[REAL_MUL_LINV]);; e(ASM_SIMP_TAC[REAL_MUL_RID]);; e(REWRITE_TAC [REAL_ARITH ` (A:real) * inv(B) * (C) = (A * C) * inv(B) `]);; e(ONCE_ASM_REWRITE_TAC []);; e(ASM_SIMP_TAC[GSYM REAL_MUL_ASSOC]);; e(ASM_SIMP_TAC[REAL_MUL_RINV]);; e(ARITH_TAC);; let RAT_LEMMA_Z = top_thm ();; (*==================================================================*) (*=================================================================*) (* End of Lemmas for the formalization of Shockwave analysis *) (*=================================================================*) (*==================================================================*) (* Theorem 03 *) (*==================================================================*) (*------------------------------------------------------------------*) (*==========%%%%% Shock_wave_Speed Verification %%%%%=============*) (*------------------------------------------------------------------*) g `!(p:sw) . n_crossing p (ind_n p) = n_crossing p (ind_m p) /\ &0 <(time p) /\ ~ ( density ((EL (ind_n p) ( pt_list p))) = density ((EL (ind_m p) ( pt_list p)))) /\ ~( density ((EL (ind_n p) ( pt_list p))) = &0) /\ ~( density ((EL (ind_m p) ( pt_list p))) = &0) /\ shock_wv (EL (ind_m p) ( pt_list p)) = shock_wv (EL (ind_n p) ( pt_list p)) ==>( shock_wv (EL (ind_n p) ( pt_list p))) = ( flow_rate ((EL (ind_n p) ( pt_list p))) - flow_rate ((EL (ind_m p) ( pt_list p)))) / ( density ((EL (ind_n p) ( pt_list p))) - density ( (EL (ind_m p) ( pt_list p)) )) `;; e(REPEAT STRIP_TAC);; e(SUBGOAL_THEN ` ~(&1 = &0)` ASSUME_TAC);; e (ARITH_TAC);; e(SUBGOAL_THEN ` (shock_wv (EL (ind_n p) (pt_list p)) = shock_wv (EL (ind_n p) (pt_list p)) / &1)` ASSUME_TAC);; e (ARITH_TAC);; e (ONCE_ASM_REWRITE_TAC []);; e (POP_ASSUM (K ALL_TAC));; e(SUBGOAL_THEN ` ~( (density (EL (ind_n p) (pt_list p)) - density (EL (ind_m p) (pt_list p))) = &0) ` ASSUME_TAC);; e(REWRITE_TAC [REAL_SUB_LT]);; e(MATCH_MP_TAC NOT_EQUAL);; e (ASM_SIMP_TAC []);; e(ASM_SIMP_TAC [RAT_LEMMA_Z; REAL_MUL_RID]);; e (POP_ASSUM (K ALL_TAC));; e(REWRITE_TAC [REAL_SUB_LDISTRIB]);; e(SUBGOAL_THEN ` (((shock_wv (EL (ind_n p) (pt_list p)) ) * density ( (EL (ind_n p) (pt_list p)) ) ) - ((shock_wv (EL (ind_n p) (pt_list p)) ) * density ( (EL (ind_m p) (pt_list p)) ) ) = flow_rate (EL (ind_n p) (pt_list p)) - flow_rate (EL (ind_m p) (pt_list p)) ) = (flow_rate (EL (ind_n p) (pt_list p)) - ((shock_wv (EL (ind_n p) (pt_list p)) ) * density (EL (ind_n p) (pt_list p))) = flow_rate ( (EL (ind_m p) (pt_list p))) - ((shock_wv (EL (ind_n p) (pt_list p)) ) * density (EL (ind_m p) (pt_list p))) ) ` ASSUME_TAC);; e(EQ_TAC);; e(REAL_ARITH_TAC);; e(REAL_ARITH_TAC);; e(ONCE_ASM_REWRITE_TAC[]);; e(POP_ASSUM (K ALL_TAC));; e(SUBGOAL_THEN ` (flow_rate (EL (ind_n p) (pt_list p)) = spd (EL (ind_n p) (pt_list p)) * density (EL (ind_n p) (pt_list p)))/\ (flow_rate (EL (ind_m p) (pt_list p)) = spd (EL (ind_m p) (pt_list p)) * density (EL (ind_m p) (pt_list p))) ` ASSUME_TAC);; e(REWRITE_TAC [spd]);; e(REWRITE_TAC [real_div]);; e(REWRITE_TAC [GSYM REAL_MUL_ASSOC]);; e(ASM_SIMP_TAC [REAL_MUL_LINV]);; e(ARITH_TAC);; (*----------------------------------------------*) e(ASM_SIMP_TAC[]);; e(POP_ASSUM (K ALL_TAC));; e(POP_ASSUM (K ALL_TAC));; e(REWRITE_TAC [GSYM REAL_SUB_RDISTRIB]);; e(SUBGOAL_THEN ` ~(time p = &0) ` ASSUME_TAC);; e(REWRITE_TAC [REAL_NOT_EQ]);; e(ASM_SIMP_TAC[]);; e(SUBGOAL_THEN ` ( (spd (EL (ind_n p) (pt_list p)) - shock_wv (EL (ind_n p) (pt_list p))) * density (EL (ind_n p) (pt_list p)) = (spd (EL (ind_m p) (pt_list p)) - shock_wv (EL (ind_n p) (pt_list p))) * density (EL (ind_m p) (pt_list p)) ) = ( ((spd (EL (ind_n p) (pt_list p)) - shock_wv (EL (ind_n p) (pt_list p))) * density (EL (ind_n p) (pt_list p))) * time p = ((spd (EL (ind_m p) (pt_list p)) - shock_wv (EL (ind_n p) (pt_list p))) * density (EL (ind_m p) (pt_list p))) * time p )` ASSUME_TAC);; e(ONCE_ASM_REWRITE_TAC[]);; e(EQ_TAC);; e(DISCH_TAC);; e(ONCE_ASM_REWRITE_TAC[]);; e(ARITH_TAC);; e(DISCH_TAC);; e(MATCH_MP_TAC REAL_EQ_RCANCEL_IMP);; e(EXISTS_TAC `( time p )`);; e(ASM_SIMP_TAC[]);; e(ASM_SIMP_TAC[]);; e(POP_ASSUM (K ALL_TAC));; e(POP_ASSUM (K ALL_TAC));; e(REWRITE_TAC [spd]);; (*******************************************************) e(SUBGOAL_THEN ` ((flow_rate ((EL (ind_m p) (pt_list p))) / density ( (EL (ind_m p) (pt_list p))) - shock_wv (EL (ind_n p) (pt_list p))) * density ( (EL (ind_m p) (pt_list p)))) * time p = ((flow_rate ((EL (ind_m p) (pt_list p))) / density ( (EL (ind_m p) (pt_list p))) - shock_wv (EL (ind_m p) (pt_list p))) * density ( (EL (ind_m p) (pt_list p)))) * time p ` ASSUME_TAC);; e(ASM_REWRITE_TAC[]);; e (UNDISCH_TAC ` shock_wv (EL (ind_m p) (pt_list p)) = shock_wv (EL (ind_n p) (pt_list p))`);; e(DISCH_TAC);; e(POP_ASSUM (K ALL_TAC));; e (ASM_REWRITE_TAC []);; e(POP_ASSUM (K ALL_TAC));; e(REWRITE_TAC [GSYM n_crossing]);; e (ASM_REWRITE_TAC []);; let n_sw = top_thm();; (*______list of no of vehicles from Shock wave _____*) let sw_list = new_recursive_definition list_RECURSION `(sw_list []= []) /\ (sw_list (CONS h t) = CONS ((shock_wv (EL (ind_n (h:sw)) (pt_list (h:sw)))) * time (h:sw)) (sw_list t))`;; (*________Sum function for S/W __________*) let sum_sw = new_definition `sum_sw (L:(sw list)) = sum (1..(LENGTH L) ) (\i. (EL (i - 1) (sw_list L)))`;; (****=========================================****) (*===================================================================*) (* Application to a general Highway *) (*===================================================================*) (*-------------------------------------------------------------------*) (* No. of vehicles/Queue_size with sw:data_points via S/W analysis *) (*-------------------------------------------------------------------*) (*--------------------------Queue_size in a _Region----------------------*) let sw_rgn = new_definition `sw_rgn (r:sw_d) = --( ((shock_wv (EL (ind_n ( HD (FST(r)) )) (pt_list ( (HD (FST(r))) )))) * time (HD (FST(r))) ) - sum_sw (TL (FST(r)))) * ( SND(SND(r)) - FST(SND(r)) ) `;; let sw_rgn_list = new_recursive_definition list_RECURSION `(sw_rgn_list [] = []) /\ (sw_rgn_list (CONS h t) = CONS (sw_rgn (h:sw_d)) (sw_rgn_list t))`;; let sum_sw_rgn = new_definition `sum_sw_rgn (L:(sw_d list)) = sum (1..LENGTH L) (\i. (EL (i - 1) (sw_rgn_list L)))`;; (*-----------------------------------------------------------------------*) (*-------------------------------------------------------------------*) (* No. of vehicles/Queue_size with sw:data_points via I/O analysis *) (*-------------------------------------------------------------------*) let n_io = new_definition (*__No of vehicles in queue via i/o __*) `n_io (p:sw) = (flow_rate (EL (ind_m p) (pt_list p)) - flow_rate (EL (ind_n p) (pt_list p))) * (time p) `;; (*__ List of no of vehicles via I/O ___*) let io_list = new_recursive_definition list_RECURSION `(io_list [] = []) /\ (io_list (CONS h t) = CONS (n_io (h:sw)) (io_list t))`;; (*__ sum function via I/O ___*) let sum_io = new_definition `sum_io (L:sw list) = sum (1..LENGTH L) (\i. (EL (i - 1) (io_list L)))`;; (*=============================================================*) (* Theorem 05 *) (*---------------------THM_ARRIVAL_IO--------------------------*) (*=============================================================*) g `!(vw:real) (vw2:real) (qc:real) (qa:real) (ka2:real) (ka:real) (t1:real) (t:real). sum_io ([ ([(qa ,ka ), vw ; (qc, kc), vw ], (&0, t1)), 0, 1 ; ([(qa2,ka2), vw2 ; (qc, kc), vw2], (t1, t)), 0, 1 ]:(sw list)) = (qa - qc) * t1 + (qa2 - qc) * (t - t1) `;; e(REPEAT STRIP_TAC);; e(REWRITE_TAC [ sum_io; LENGTH]);; e(REWRITE_TAC [io_list; n_io]);; e(REWRITE_TAC [flow_rate; pt_list]);; e(REWRITE_TAC [time; ind_m; ind_n]);; e(REWRITE_TAC [GSYM ONE; GSYM TWO]);; e(REWRITE_TAC [SUM_2]);; e (SUBGOAL_THEN `((1 - 1) = 0) /\ ((2 - 1) = 1) ` ASSUME_TAC);; e (ARITH_TAC);; e (ASM_SIMP_TAC []);; e (POP_ASSUM (K ALL_TAC));; e(REWRITE_TAC [ ONE; EL; TL; HD]);; e(REWRITE_TAC [REAL_SUB_RZERO]);; let THM_ARRIVAL_IO = top_thm();; (*=============================================================*) (* Theorem 07 *) (*-------------------THM_PROPAGATION_IO------------------------*) (*=============================================================*) g `!(vw:real) (vw2:real) (qc:real) (qa:real) (ka2:real) (ka:real) (t1:real) (t:real). sum_io ([ ([(qa ,ka ), vw ; (qc, kc), vw], (&0, t1)), 0, 1 ; ([(qa ,ka ), vp ; (qr, kr), vp], (t1, t )), 0, 1 ]:(sw list)) = (qa - qc) * t1 + (qa - qr) * (t - t1) `;; e(REPEAT STRIP_TAC);; e(REWRITE_TAC [ sum_io; LENGTH]);; e(REWRITE_TAC [io_list; n_io]);; e(REWRITE_TAC [flow_rate; pt_list]);; e(REWRITE_TAC [time; ind_m; ind_n]);; e(REWRITE_TAC [GSYM ONE; GSYM TWO]);; e(REWRITE_TAC [SUM_2]);; e (SUBGOAL_THEN `((1 - 1) = 0) /\ ((2 - 1) = 1) ` ASSUME_TAC);; e (ARITH_TAC);; e (ASM_SIMP_TAC []);; e (POP_ASSUM (K ALL_TAC));; e(REWRITE_TAC [ ONE; EL; TL; HD]);; e(REWRITE_TAC [REAL_SUB_RZERO]);; let THM_PROPAGATION_IO = top_thm();; (*=============================================================*) (* Theorem 09 *) (*---------------------THM_DISSIPATION_IO----------------------*) (*=============================================================*) g `!(vw:real) (vw2:real) (qc:real) (qa:real) (ka2:real) (ka:real) (t1:real) (t:real). sum_io ([ ([(qa ,ka), vw ; (qc, kc), vw], (&0, t1)), 0, 1; ([(qa ,ka), vr ; (qr, kr), vr], (t1, t2)), 0, 1; ([(qa ,ka), vr ; (qr, kr), vr], (t2, t )), 0, 1 ]:(sw list)) = (qa - qc) * t1 + (qa - qr) * (t2 - t1) + (qa - qr) * (t - t2) `;; e(REPEAT STRIP_TAC);; e(REWRITE_TAC [ sum_io; LENGTH]);; e(REWRITE_TAC [io_list; n_io]);; e(REWRITE_TAC [flow_rate; pt_list]);; e(REWRITE_TAC [time; ind_m; ind_n]);; e(REWRITE_TAC [REAL_SUB_RZERO]);; e(REWRITE_TAC [ADD1; ADD]);; e (SUBGOAL_THEN `((1 + 1) = 2) /\ ((1 + 1) + 1 = 3) ` ASSUME_TAC);; e (ARITH_TAC);; e (ASM_SIMP_TAC []);; e (POP_ASSUM (K ALL_TAC));; e(REWRITE_TAC [SUM_3]);; e (SUBGOAL_THEN `((1 - 1) =0) /\ ((2 - 1) = 1) /\ ((3 - 1) = 2) ` ASSUME_TAC);; e (ARITH_TAC);; e (ASM_SIMP_TAC []);; e (POP_ASSUM (K ALL_TAC));; e(REWRITE_TAC [ TWO; ONE; EL; TL; HD]);; let THM_DISSIPATION_IO = top_thm();; (*==========================================================================*) (* Theorem 06 *) (* THM_ARRIVAL (The number of vehicles for change in arrival) *) (*==========================================================================*) g `!(vw:real) (vw2:real) (qc:real) (qa:real) (qa2:real) (ka2:real) (ka:real) (kc:real) (t1:real) (t:real). ~(ka = kc) /\ ~(ka2 = kc) /\ ~(kc = &0) /\ ~(ka2 = &0) /\ ~(ka = &0) /\ (!(p:sw). n_crossing p (ind_n p) = n_crossing p (ind_m p)) /\ (!(p:sw). shock_wv (EL (ind_m p) (pt_list p)) = shock_wv (EL (ind_n p) (pt_list p))) /\ (!(p:sw). &0 < time p ) ==> sum_sw_rgn ([ [ ([(qa ,ka ), vw ; (qc, kc), vw ], (&0, t1)), (0, 1) ], ka , kc ; [ ([((qa2 ,ka2), vw2) ; (qc, kc), vw2], (t1, t)), (0, 1) ], ka2, kc]:((sw_d)list)) = (qa - qc) * t1 + (qa2 - qc) * (t - t1) `;; e(REPEAT STRIP_TAC);; e(REWRITE_TAC [ sum_sw_rgn; LENGTH]);; e(REWRITE_TAC [sw_rgn_list; sw_rgn; sw_list; sum_sw]);; e(REWRITE_TAC [ HD]);; (****====================================****) e(REWRITE_TAC [ ONE; EL; TL; HD]);; e(REWRITE_TAC [LENGTH; GSYM ADD1]);; e(REWRITE_TAC [ sw_list]);; e(REWRITE_TAC [GSYM ONE; GSYM TWO]);; e (SUBGOAL_THEN ` (sum (1..0) (\i. EL (i - 1) []) = &0) ` ASSUME_TAC);; e (SIMP_TAC [SUM_CLAUSES_NUMSEG]);; e(ARITH_TAC);; e (ASM_SIMP_TAC[]);; e (POP_ASSUM (K ALL_TAC));; e(REWRITE_TAC [SUM_1; SUM_2]);; e (SUBGOAL_THEN `((1 - 1) = 0) /\ ((2 - 1) = 1) ` ASSUME_TAC);; e (ARITH_TAC);; e (ASM_SIMP_TAC []);; e (POP_ASSUM (K ALL_TAC));; e(REWRITE_TAC [ ONE; EL; TL; HD]);; e(REWRITE_TAC [GSYM ONE]);; e(REWRITE_TAC [REAL_SUB_RZERO; time]);; (****===============1st subgoal start=================****) e (SUBGOAL_THEN ` shock_wv (EL (ind_n (([(qa2,ka2),vw2; (qc,kc),vw2],t1,t),0,1)) (pt_list (([(qa2,ka2),vw2; (qc,kc),vw2],t1,t),0,1))) = ( flow_rate (EL (ind_n (([(qa2,ka2),vw2; (qc,kc),vw2],t1,t),0,1)) (pt_list (([(qa2,ka2),vw2; (qc,kc),vw2],t1,t),0,1))) - flow_rate (EL (ind_m (([(qa2,ka2),vw2; (qc,kc),vw2],t1,t),0,1)) (pt_list (([(qa2,ka2),vw2; (qc,kc),vw2],t1,t),0,1))) )/ ( density (EL (ind_n (([(qa2,ka2),vw2; (qc,kc),vw2],t1,t),0,1)) (pt_list (([(qa2,ka2),vw2; (qc,kc),vw2],t1,t),0,1))) - density (EL (ind_m (([(qa2,ka2),vw2; (qc,kc),vw2],t1,t),0,1)) (pt_list (([(qa2,ka2),vw2; (qc,kc),vw2],t1,t),0,1))) ) ` ASSUME_TAC);; (**---------------------------------------------------***) e(MATCH_MP_TAC n_sw);; e(REPEAT CONJ_TAC);; e (ASM_SIMP_TAC []);; e (ASM_SIMP_TAC []);; e(REWRITE_TAC [pt_list ]);; e(REWRITE_TAC [ ind_n; ind_m ;ONE; EL; TL; HD]);; e(REWRITE_TAC [density ]);; (****============================================****) e(ASM_SIMP_TAC [REAL_SUB_LT; GSYM real_gt ]);; e(REWRITE_TAC [pt_list ]);; e(REWRITE_TAC [ ind_n; ind_m ;ONE; EL; TL; HD]);; e(REWRITE_TAC [density ]);; e (ASM_SIMP_TAC []);; e(REWRITE_TAC [pt_list ]);; e(REWRITE_TAC [ ind_n; ind_m ;ONE; EL; TL; HD]);; e(REWRITE_TAC [density ]);; e (ASM_SIMP_TAC []);; e (ASM_SIMP_TAC []);; (****============= 1st subgoal ENDED ========****) e (ASM_SIMP_TAC []);; e (POP_ASSUM (K ALL_TAC));; (****=======================2nd subgoal start===============****) e (SUBGOAL_THEN ` shock_wv (EL (ind_n (([(qa,ka),vw; (qc,kc),vw],&0,t1),0,1)) (pt_list (([(qa,ka),vw; (qc,kc),vw],&0,t1),0,1))) = ( flow_rate (EL (ind_n (([(qa,ka),vw; (qc,kc),vw],&0,t1),0,1)) (pt_list (([(qa,ka),vw; (qc,kc),vw],&0,t1),0,1))) - flow_rate (EL (ind_m (([(qa,ka),vw; (qc,kc),vw],&0,t1),0,1)) (pt_list (([(qa,ka),vw; (qc,kc),vw],&0,t1),0,1))) )/ ( density (EL (ind_n (([(qa,ka),vw; (qc,kc),vw],&0,t1),0,1)) (pt_list (([(qa,ka),vw; (qc,kc),vw],&0,t1),0,1))) - density (EL (ind_m (([(qa,ka),vw; (qc,kc),vw],&0,t1),0,1)) (pt_list (([(qa,ka),vw; (qc,kc),vw],&0,t1),0,1))) ) ` ASSUME_TAC);; (**--------------------------------------***) e(MATCH_MP_TAC n_sw);; e(REPEAT CONJ_TAC);; e (ASM_SIMP_TAC []);; e (ASM_SIMP_TAC []);; e(REWRITE_TAC [pt_list ]);; e(REWRITE_TAC [ ind_n; ind_m ;ONE; EL; TL; HD]);; e(REWRITE_TAC [density ]);; (****=========================================****) e(ASM_SIMP_TAC [REAL_SUB_LT; GSYM real_gt ]);; e(REWRITE_TAC [pt_list ]);; e(REWRITE_TAC [ ind_n; ind_m ;ONE; EL; TL; HD]);; e(REWRITE_TAC [density ]);; e (ASM_SIMP_TAC []);; e(REWRITE_TAC [pt_list ]);; e(REWRITE_TAC [ ind_n; ind_m ;ONE; EL; TL; HD]);; e(REWRITE_TAC [density ]);; e (ASM_SIMP_TAC []);; e (ASM_SIMP_TAC []);; (****=======================2nd subgoal ended===============****) e (ASM_SIMP_TAC []);; e (POP_ASSUM (K ALL_TAC));; e(REWRITE_TAC [pt_list ]);; e(REWRITE_TAC [ ind_n; ind_m ;ONE; EL; TL; HD]);; e(REWRITE_TAC [flow_rate; density ]);; e(REWRITE_TAC [real_div]);; e(REWRITE_TAC [REAL_NEG_LMUL]);; e(REWRITE_TAC [REAL_NEG_SUB]);; e(REWRITE_TAC [GSYM REAL_MUL_ASSOC]);; e(REWRITE_TAC [REAL_ARITH ` (A:real) * inv(B) * (C:real) * B = (A:real) * ( inv(B) * B) * C`]);; e (SUBGOAL_THEN ` ~(kc - ka = &0) /\ ~(kc - ka2 = &0) ` ASSUME_TAC);; e(CONJ_TAC);; e(MATCH_MP_TAC NOT_EQUAL);; e (ASM_SIMP_TAC []);; e(MATCH_MP_TAC NOT_EQUAL);; e (ASM_SIMP_TAC []);; e(ASM_SIMP_TAC[REAL_MUL_LINV]);; e(ONCE_REWRITE_TAC [REAL_MUL_LID]);; e(ARITH_TAC);; let THM_ARRIVAL = top_thm();; (*==================================================================================*) (* Theorem 08 *) (* THM_PROPAGATION (The Queue Size with shockwave analysis *) (* for a change in Discharging (Propagation)) *) (*==================================================================================*) g `!(vp:real) (vw:real) (qa:real) (qc:real) (qr:real) (ka:real) (kc:real) (kr:real) (t1:real) (t:real). ~(ka = kc) /\ ~(kc = kr) /\ ~(ka = &0) /\ ~(kc = &0) /\ ~(kr = &0) /\ (!(p:sw). n_crossing p (ind_n p) = n_crossing p (ind_m p)) /\ (!(p:sw). shock_wv (EL (ind_m p) (pt_list p)) = shock_wv (EL (ind_n p) (pt_list p))) /\ (!(p:sw). &0 < time p) ==> sum_sw_rgn ([ [( [(qc ,kc ), vp ; (qr, kr), vp], (t1, t)), (0, 1)],ka , kr; [ ([((qa ,ka), vw) ; (qc, kc), vw], (&0, t)), (0, 1); ([((qc ,kc), vp) ; (qr, kr), vp], (t1, t)), (0, 1) ], ka, kc ]:((sw_d)list)) = (qa - qc) * t1 + (qa - qr) * (t - t1) `;; e(REPEAT STRIP_TAC);; e(REWRITE_TAC [ sum_sw_rgn; LENGTH]);; e(REWRITE_TAC [sw_rgn_list; sw_rgn; sw_list; sum_sw]);; e(REWRITE_TAC [ HD]);; (****====================================================================****) e(REWRITE_TAC [ ONE; EL; TL; HD]);; e(REWRITE_TAC [LENGTH; GSYM ADD1]);; e(REWRITE_TAC [ sw_list]);; e(REWRITE_TAC [GSYM ONE; GSYM TWO]);; e (SUBGOAL_THEN ` (sum (1..0) (\i. EL (i - 1) []) = &0) ` ASSUME_TAC);; e (SIMP_TAC [SUM_CLAUSES_NUMSEG]);; e(ARITH_TAC);; e (ASM_SIMP_TAC[]);; e (POP_ASSUM (K ALL_TAC));; e(REWRITE_TAC [SUM_1; SUM_2]);; e (SUBGOAL_THEN `((1 - 1) = 0) /\ ((2 - 1) = 1) ` ASSUME_TAC);; e (ARITH_TAC);; e (ASM_SIMP_TAC []);; e (POP_ASSUM (K ALL_TAC));; e(REWRITE_TAC [ ONE; EL; TL; HD]);; e(REWRITE_TAC [GSYM ONE]);; e(REWRITE_TAC [REAL_SUB_RZERO; time]);; (****=======================1st subgoal start for vw==============****) e (SUBGOAL_THEN ` shock_wv (EL (ind_n (([(qa,ka),vw; (qc,kc),vw],&0,t),0,1)) (pt_list (([(qa,ka),vw; (qc,kc),vw],&0,t),0,1))) = (flow_rate (EL (ind_n (([(qa,ka),vw; (qc,kc),vw],&0,t),0,1)) (pt_list (([(qa,ka),vw; (qc,kc),vw],&0,t),0,1))) - flow_rate (EL (ind_m (([(qa,ka),vw; (qc,kc),vw],&0,t),0,1)) (pt_list (([(qa,ka),vw; (qc,kc),vw],&0,t),0,1)))) / (density (EL (ind_n (([(qa,ka),vw; (qc,kc),vw],&0,t),0,1)) (pt_list (([(qa,ka),vw; (qc,kc),vw],&0,t),0,1))) - density (EL (ind_m (([(qa,ka),vw; (qc,kc),vw],&0,t),0,1)) (pt_list (([(qa,ka),vw; (qc,kc),vw],&0,t),0,1)))) ` ASSUME_TAC);; (**--------------------------------------***) e(MATCH_MP_TAC n_sw);; e(REPEAT CONJ_TAC);; e (ASM_SIMP_TAC []);; e (ASM_SIMP_TAC []);; e(REWRITE_TAC [pt_list ]);; e(REWRITE_TAC [ ind_n; ind_m ;ONE; EL; TL; HD]);; e(REWRITE_TAC [density ]);; (****=========================================****) e(ASM_SIMP_TAC [REAL_SUB_LT; GSYM real_gt ]);; e(REWRITE_TAC [pt_list ]);; e(REWRITE_TAC [ ind_n; ind_m ;ONE; EL; TL; HD]);; e(REWRITE_TAC [density ]);; e (ASM_SIMP_TAC []);; e(REWRITE_TAC [pt_list ]);; e(REWRITE_TAC [ ind_n; ind_m ;ONE; EL; TL; HD]);; e(REWRITE_TAC [density ]);; e (ASM_SIMP_TAC []);; e (ASM_SIMP_TAC []);; (****===================1st subgoal ENDED===============****) e (ASM_SIMP_TAC []);; e (POP_ASSUM (K ALL_TAC));; (****=================2nd subgoal start for vp===============****) e (SUBGOAL_THEN ` shock_wv (EL (ind_n (([(qc,kc),vp; (qr,kr),vp],t1,t),0,1)) (pt_list (([(qc,kc),vp; (qr,kr),vp],t1,t),0,1))) = (flow_rate (EL (ind_n (([(qc,kc),vp; (qr,kr),vp],t1,t),0,1)) (pt_list (([(qc,kc),vp; (qr,kr),vp],t1,t),0,1))) - flow_rate (EL (ind_m (([(qc,kc),vp; (qr,kr),vp],t1,t),0,1)) (pt_list (([(qc,kc),vp; (qr,kr),vp],t1,t),0,1))) )/ (density (EL (ind_n (([(qc,kc),vp; (qr,kr),vp],t1,t),0,1)) (pt_list (([(qc,kc),vp; (qr,kr),vp],t1,t),0,1))) -density (EL (ind_m (([(qc,kc),vp; (qr,kr),vp],t1,t),0,1)) (pt_list (([(qc,kc),vp; (qr,kr),vp],t1,t),0,1))) ) ` ASSUME_TAC);; (**--------------------------------------***) e(MATCH_MP_TAC n_sw);; e(REPEAT CONJ_TAC);; e (ASM_SIMP_TAC []);; e (ASM_SIMP_TAC []);; e(REWRITE_TAC [pt_list ]);; e(REWRITE_TAC [ ind_n; ind_m ;ONE; EL; TL; HD]);; e(REWRITE_TAC [density ]);; (****=========================================****) e(ASM_SIMP_TAC [REAL_SUB_LT; GSYM real_gt ]);; e(REWRITE_TAC [pt_list ]);; e(REWRITE_TAC [ ind_n; ind_m ;ONE; EL; TL; HD]);; e(REWRITE_TAC [density ]);; e (ASM_SIMP_TAC []);; e(REWRITE_TAC [pt_list ]);; e(REWRITE_TAC [ ind_n; ind_m ;ONE; EL; TL; HD]);; e(REWRITE_TAC [density ]);; e (ASM_SIMP_TAC []);; e (ASM_SIMP_TAC []);; (****=======================2nd subgoal ended===============****) e (ASM_SIMP_TAC []);; e (POP_ASSUM (K ALL_TAC));; e(REWRITE_TAC [pt_list ]);; e(REWRITE_TAC [ ind_n; ind_m ;ONE; EL; TL; HD]);; e(REWRITE_TAC [flow_rate; density ]);; (*------APPLYING THEOREM NOT EQUAL-----------------------*) e (SUBGOAL_THEN ` ~(kc - ka = &0) /\ ~(kr - kc = &0) ` ASSUME_TAC);; e(CONJ_TAC);; e(MATCH_MP_TAC NOT_EQUAL);; e (ASM_SIMP_TAC []);; e(MATCH_MP_TAC NOT_EQUAL);; e (ASM_SIMP_TAC []);; (*------Applied THEOREM NOT EQUAL-----------------------*) e(REWRITE_TAC [real_div]);; e(REWRITE_TAC [REAL_NEG_LMUL]);; e(REWRITE_TAC [REAL_NEG_SUB]);; e(REWRITE_TAC [GSYM REAL_MUL_ASSOC]);; (*=================================================*) e(REWRITE_TAC [REAL_SUB_RDISTRIB]);; e(REWRITE_TAC [GSYM REAL_MUL_ASSOC]);; e(REWRITE_TAC [REAL_ARITH ` (A:real) * inv(B) * (C:real) * B = (A:real) * ( inv(B) * B) * C`]);; e(ASM_SIMP_TAC[REAL_MUL_LINV]);; (*------------------------------------*) e(ONCE_REWRITE_TAC [REAL_MUL_LID]);; e(REWRITE_TAC [REAL_ADD_RID]);; e(REWRITE_TAC [GSYM REAL_SUB_RDISTRIB]);; e(REWRITE_TAC [GSYM REAL_MUL_ASSOC]);; e(SUBGOAL_THEN ` (qc - qr) * inv (kr - kc) * ((t:real) - (t1:real)) * (kr - ka) + (qr - qc) * inv (kr - kc) * (t - t1) * (kc - ka) - (qc - qa) * t = ((qc - qr) * inv (kr - kc) * (kr - ka) * (t - t1) - (qc - qr) * inv (kr - kc) * (kc - ka) * (t - t1) - (qc - qa) * t) ` ASSUME_TAC);; e(REAL_ARITH_TAC);; e (ASM_REWRITE_TAC []);; e (POP_ASSUM (K ALL_TAC));; e (REWRITE_TAC [REAL_ARITH ` (A:real) * inv(B) * (C:real) * D = (A * inv B * D) * C `]);; e(REWRITE_TAC [GSYM REAL_SUB_LDISTRIB]);; e(REWRITE_TAC [REAL_ARITH ` (A:real) - (B:real) - ((C:real) - B) = A:real - C:real`]);; e(REWRITE_TAC [GSYM REAL_MUL_ASSOC]);; e(REWRITE_TAC [REAL_ARITH ` (A:real) * inv(B) * (C:real) * B = (A:real) * ( inv(B) * B) * C`]);; e(ASM_SIMP_TAC[REAL_MUL_LINV]);; e(ONCE_REWRITE_TAC [REAL_MUL_LID]);; e(REWRITE_TAC [REAL_SUB_RDISTRIB]);; e(REWRITE_TAC [REAL_SUB_LDISTRIB]);; e(REAL_ARITH_TAC);; let THM_PROPAGATION = top_thm();; (*==================================================================================*) (* Theorem 10 *) (* THM_DISSIPATION (The Queue Size with shockwave analysis *) (* for a change in Discharging (Dissipation)) *) (*==================================================================================*) g `!(vp:real) (vw:real) (vr:real) (qa:real) (qc:real) (qr:real) (ka:real) (kc:real) (kr:real) (t1:real) (t2:real) (t:real). ~(ka = kc) /\ ~(kc = kr) /\ ~(ka = kr) /\ ~(ka = &0) /\ ~(kc = &0) /\ ~(kr = &0) /\ (!(p:sw). n_crossing p (ind_n p) = n_crossing p (ind_m p)) /\ (!(p:sw). shock_wv (EL (ind_m p) (pt_list p)) = shock_wv (EL (ind_n p) (pt_list p))) /\ (!(p:sw). &0 < time p ) /\(sw_rgn ( [([(qa ,ka ), vw ; (qc, kc), vw], (&0, t2)), (0, 1)],ka , kr) = sum_sw_rgn ([ [([(qc ,kc ), vp ; (qr, kr), vp], (t1, t2)), (0, 1)],ka , kr; [ ([((qa ,ka), vw) ; (qc, kc), vw], (&0, t2)), (0, 1); ([((qc ,kc), vp) ; (qr, kr), vp], (t1, t2)), (0, 1)], ka, kc ]:((sw_d)list)) ) ==> sum_sw_rgn ([ [( [( qa ,ka ), vw ; (qc, kc), vw], (&0, t2)), (0, 1)],ka, kr; [( [((qa ,ka), vr) ; (qr, kr), vr], (t2 , t)), (0, 1)], ka, kr ]:((sw_d)list)) = (qa - qc) * t1 + (qa - qr) * (t2 - t1) + (qa - qr) * (t - t2) `;; e(REPEAT STRIP_TAC);; e(REWRITE_TAC [ sum_sw_rgn; LENGTH; sw_rgn_list]);; e(REWRITE_TAC [ ONE; EL; TL; HD]);; e(REWRITE_TAC [LENGTH; GSYM ADD1]);; e(REWRITE_TAC [ sw_list]);; e(REWRITE_TAC [GSYM ONE; GSYM TWO]);; e (SUBGOAL_THEN ` (sum (1..0) (\i. EL (i - 1) []) = &0) ` ASSUME_TAC);; e (SIMP_TAC [SUM_CLAUSES_NUMSEG]);; e(ARITH_TAC);; e (ASM_SIMP_TAC[]);; e (POP_ASSUM (K ALL_TAC));; e(REWRITE_TAC [SUM_1; SUM_2]);; e (SUBGOAL_THEN `((1 - 1) = 0) /\ ((2 - 1) = 1) ` ASSUME_TAC);; e (ARITH_TAC);; e (ASM_SIMP_TAC []);; e (POP_ASSUM (K ALL_TAC));; e(REWRITE_TAC [ ONE; EL; TL; HD]);; e(REWRITE_TAC [GSYM ONE]);; (*=========================*) e(SUBGOAL_THEN ` !qa:real qr:real qc:real ka:real kr:real kc:real t2:real t1:real t:real. ~(ka = kc) /\ ~(kc = kr) /\ ~(ka = &0) /\ ~(kc = &0) /\ ~(kr = &0) /\ (!p. n_crossing p (ind_n p) = n_crossing p (ind_m p)) /\ (!p. shock_wv (EL (ind_m p) (pt_list p)) = shock_wv (EL (ind_n p) (pt_list p))) /\ (!p. (&0 < time p) ) ==> sum_sw_rgn [ [([(qc,kc),vp; (qr,kr),vp],t1,t2),0,1],ka,kr; [([(qa,ka),vw; (qc,kc),vw],&0, t2),0, 1; ([(qc,kc),vp; (qr,kr),vp],t1, t2),0, 1], ka, kc] = (qa - qc) * t1 + (qa - qr) * (t2 - t1) ` ASSUME_TAC);; e(REPEAT STRIP_TAC);; e(MATCH_MP_TAC THM_PROPAGATION);; e(ASM_SIMP_TAC[]);; (*-------------------------------------------*) e(ASM_SIMP_TAC[]);; e (POP_ASSUM (K ALL_TAC));; (***---HAVE APPLIED THEOREM PROPAGATION3---***) (***-----------------------------------------------------***) e(REWRITE_TAC [sw_rgn; sw_list; sum_sw]);; e(REWRITE_TAC [ ONE; EL; TL; HD]);; e(REWRITE_TAC [LENGTH; GSYM ADD1]);; e(REWRITE_TAC [ sw_list]);; e(REWRITE_TAC [GSYM ONE]);; e (SUBGOAL_THEN ` (sum (1..0) (\i. EL (i - 1) []) = &0) ` ASSUME_TAC);; e (SIMP_TAC [SUM_CLAUSES_NUMSEG]);; e(ARITH_TAC);; e (ASM_SIMP_TAC[]);; e (POP_ASSUM (K ALL_TAC));; (*----------------------------------------*) e(REWRITE_TAC [REAL_SUB_RZERO; time]);; (****================= subgoal start for vr ==============****) e (SUBGOAL_THEN ` shock_wv (EL (ind_n (([(qa,ka),vr; (qr,kr),vr],t2,t),0,1)) (pt_list (([(qa,ka),vr; (qr,kr),vr],t2,t),0,1))) = (flow_rate (EL (ind_n (([(qa,ka),vr; (qr,kr),vr],t2,t),0,1)) (pt_list (([(qa,ka),vr; (qr,kr),vr],t2,t),0,1))) - flow_rate (EL (ind_m (([(qa,ka),vr; (qr,kr),vr],t2,t),0,1)) (pt_list (([(qa,ka),vr; (qr,kr),vr],t2,t),0,1))) )/ (density (EL (ind_n (([(qa,ka),vr; (qr,kr),vr],t2,t),0,1)) (pt_list (([(qa,ka),vr; (qr,kr),vr],t2,t),0,1))) - density (EL (ind_m (([(qa,ka),vr; (qr,kr),vr],t2,t),0,1)) (pt_list (([(qa,ka),vr; (qr,kr),vr],t2,t),0,1))) ) ` ASSUME_TAC);; (**--------------------------------------***) e(MATCH_MP_TAC n_sw);; e(REPEAT CONJ_TAC);; e (ASM_SIMP_TAC []);; e (ASM_SIMP_TAC []);; e(REWRITE_TAC [pt_list ]);; e(REWRITE_TAC [ ind_n; ind_m ;ONE; EL; TL; HD]);; e(REWRITE_TAC [density ]);; (****=========================================****) e(ASM_SIMP_TAC [REAL_SUB_LT; GSYM real_gt ]);; e(REWRITE_TAC [pt_list ]);; e(REWRITE_TAC [ ind_n; ind_m ;ONE; EL; TL; HD]);; e(REWRITE_TAC [density ]);; e (ASM_SIMP_TAC []);; e(REWRITE_TAC [pt_list ]);; e(REWRITE_TAC [ ind_n; ind_m ;ONE; EL; TL; HD]);; e(REWRITE_TAC [density ]);; e (ASM_SIMP_TAC []);; e (ASM_SIMP_TAC []);; (****================subgoal ENDED===============****) e (ASM_SIMP_TAC []);; e (POP_ASSUM (K ALL_TAC));; e(REWRITE_TAC [pt_list ]);; e(REWRITE_TAC [ ind_n; ind_m ;ONE; EL; TL; HD]);; e(REWRITE_TAC [flow_rate; density ]);; (*------APPLYING THEOREM NOT EQUAL-----------------------*) e (SUBGOAL_THEN `~(kr - ka = &0) ` ASSUME_TAC);; e(MATCH_MP_TAC NOT_EQUAL);; e (ASM_SIMP_TAC []);; (*------APPLYING THEOREM NOT EQUAL-----------------------*) e(REWRITE_TAC [real_div]);; e(REWRITE_TAC [GSYM REAL_MUL_ASSOC]);; e(REWRITE_TAC [REAL_NEG_LMUL]);; e(REWRITE_TAC [REAL_NEG_SUB]);; e(REWRITE_TAC [GSYM REAL_MUL_ASSOC]);; e(REWRITE_TAC [REAL_ARITH ` (A:real) * inv(B) * (C:real) * B = (A:real) * ( inv(B) * B) * C`]);; e(ASM_SIMP_TAC[REAL_MUL_LINV]);; e(ONCE_REWRITE_TAC [REAL_MUL_LID]);; e(REWRITE_TAC [REAL_SUB_RDISTRIB]);; e(REWRITE_TAC [REAL_SUB_LDISTRIB]);; e(REAL_ARITH_TAC);; let THM_DISSIPATION = top_thm();; (*-----------------------------------------*) (*============================================================*) (* End of the Shockwave Analysis Formalization *) (*============================================================*)