(* ========================================================================= *) (* File Name: No_Reaction.ml *) (*---------------------------------------------------------------------------*) (* Description: Formal Verification of Zsyntax Properties *) (* *) (* *) (* (c) Author : Adnan Rashid *) (* Co-Author : Sohaib Ahmad *) (* Co-Author : Dr. Osman Hasan *) (* SYSTEM ANALYSIS & VERIFICATION (SAVe) LAB *) (* National University of Sciences and Technology (NUST), PAKISTAN *) (* NOTE: This Script is written in HOL Light *) (* *) (* ========================================================================= *) (* ==========================================================================*) (* Theorems List *) (*---------------------------------------------------------------------------*) (* EVF_GEN_THM; *) (* RECUR1_GEN_THM; *) (* RECUR2_GEN_THM; *) (* RECUR_DED_GEN_THM; *) (* Z_NOMATCH_THM; *) (* This file needs Formalization.ml to be uploaded first *) (* This file needs Supporting_Theorems.ml to be uploaded first *) (* This file needs Delete_Theorems.ml to be uploaded first *) (* This file needs z_Delete_Theorems.ml to be uploaded first *) (*---------------------------------------------------------------------------*) (*---------------------------------------------------------------------------*) (* z_EVF_NO_MATCH_THM *) (*---------------------------------------------------------------------------*) g `!p e l x y. ~NULL e /\ ~NULL l /\ (x < LENGTH l) /\ (y < LENGTH l) /\ (p < LENGTH e) /\ (!a. (MEM a e) ==> ~(MEM (FST a) [HD l])) ==> (zsyn_EVF (l:(((A)list) list)) (e:((((A)list) # ((A)list) list) list)) p x y = (F,TL l))`;; e (SIMP_TAC [MEM; GSYM LENGTH_NOT_NULL]);; e (INDUCT_TAC);; e (REPEAT STRIP_TAC);; e (REWRITE_TAC [zsyn_EVF; HD; TL; EL]);; e (SUBGOAL_THEN `MEM (HD e) (e:(((A)list) # ((A)list) list) list)` ASSUME_TAC);; e (SIMP_TAC [MEM_EXISTS_EL]);; e (EXISTS_TAC `0`);; e (ASM_MESON_TAC [EL]);; e (ASM_MESON_TAC []);; e (REPEAT STRIP_TAC);; e (REWRITE_TAC [zsyn_EVF; HD; TL; EL]);; e (SUBGOAL_THEN `MEM (EL p (TL e)) (e:((((A)list) # ((A)list) list) list))` ASSUME_TAC);; e (SIMP_TAC [MEM_EXISTS_EL]);; e (EXISTS_TAC `SUC p`);; e (ASM_MESON_TAC [EL]);; e (COND_CASES_TAC);; e (ASM_MESON_TAC []);; e (UNDISCH_TAC `!(e:((((A)list) # ((A)list) list) list)) (l:(((A)list) list)) x y. 0 < LENGTH e /\ 0 < LENGTH l /\ x < LENGTH l /\ y < LENGTH l /\ p < LENGTH e /\ (!a. MEM a e ==> ~(FST a = HD l)) ==> zsyn_EVF l e p x y = F,TL l`);; e (DISCH_THEN (MP_TAC o SPEC `(e:((((A)list) # ((A)list) list) list))`));; e (DISCH_THEN (MP_TAC o SPEC `(l:(((A)list) list))`));; e (DISCH_THEN (MP_TAC o SPEC `x:num`));; e (DISCH_THEN (MP_TAC o SPEC `y:num`));; e (ASM_SIMP_TAC []);; e (SUBGOAL_THEN `p < LENGTH (e:((((A)list) # ((A)list) list) list))` ASSUME_TAC);; e (MATCH_MP_TAC LT_TRANS);; e (EXISTS_TAC `SUC p`);; e (ASM_SIMP_TAC []);; e (ARITH_TAC);; e (ASM_REWRITE_TAC []);; let EVF_GEN_THM = top_thm ();; (*---------------------------------------------------------------------------*) (* z_RECUR1_NO_MATCH_THM *) (*---------------------------------------------------------------------------*) g `!y e l x. ~NULL e /\ ~NULL l /\ (x < LENGTH l) /\ (y < LENGTH l) /\ (!a y. (MEM a e) /\ (y < LENGTH l) ==> ~(MEM (FST a) [HD (zsyn_conjun_intro l x y)])) ==> (zsyn_recurs1 (l:(((A)list) list)) (e:((((A)list) # ((A)list) list) list)) x y = (F,l))`;; e (REWRITE_TAC [zsyn_conjun_intro; HD; MEM]);; e (INDUCT_TAC);; e (REPEAT STRIP_TAC);; e (REWRITE_TAC [zsyn_recurs1]);; e (REWRITE_TAC [zsyn_conjun_intro]);; e (SUBGOAL_THEN `zsyn_EVF (CONS (FLAT [EL x l; EL 0 l]) (l:(((A)list) list))) (e:((((A)list) # ((A)list) list) list)) (LENGTH e - 1) (x:num) 0 = (F, TL (CONS (FLAT [EL x l; EL 0 l]) l))` ASSUME_TAC);; e (MATCH_MP_TAC EVF_GEN_THM);; e (ASM_SIMP_TAC [NULL; LENGTH; MEM; HD; LENGTH_NOT_NULL]);; e (CONJ_TAC);; e (ASM_ARITH_TAC);; e (REWRITE_TAC [GSYM REAL_OF_NUM_LT]);; e (SUBGOAL_THEN `&(LENGTH (e:((((A)list) # ((A)list) list) list)) - 1) = &(LENGTH e) - &1` ASSUME_TAC);; e (ONCE_REWRITE_TAC [EQ_SYM_EQ]);; e (MATCH_MP_TAC REAL_OF_NUM_SUB);; e (UNDISCH_TAC `~NULL (e:((((A)list) # ((A)list) list) list))`);; e (REWRITE_TAC [GSYM LENGTH_NOT_NULL]);; e (ARITH_TAC);; e (ASM_REWRITE_TAC []);; e (POP_ASSUM (K ALL_TAC));; e (REWRITE_TAC [REAL_ARITH `(&m - &1 < &m) = (&0 < &1)`]);; e (REAL_ARITH_TAC);; e (ASM_REWRITE_TAC []);; e (REWRITE_TAC [TL]);; e (REPEAT STRIP_TAC);; e (REWRITE_TAC [zsyn_recurs1]);; e (REWRITE_TAC [zsyn_conjun_intro]);; e (SUBGOAL_THEN `zsyn_EVF (CONS (FLAT [EL x l; EL (SUC y) l]) (l:(((A)list) list))) (e:((((A)list) # ((A)list) list) list)) (LENGTH e - 1) (x:num) ((SUC y)) = (F, TL (CONS (FLAT [EL x l; EL (SUC y) l]) l))` ASSUME_TAC);; e (MATCH_MP_TAC EVF_GEN_THM);; e (ASM_SIMP_TAC [NULL; LENGTH; MEM; HD; LENGTH_NOT_NULL]);; e (CONJ_TAC);; e (ASM_ARITH_TAC);; e (CONJ_TAC);; e (ASM_ARITH_TAC);; e (REWRITE_TAC [GSYM REAL_OF_NUM_LT]);; e (SUBGOAL_THEN `&(LENGTH (e:((((A)list) # ((A)list) list) list)) - 1) = &(LENGTH e) - &1` ASSUME_TAC);; e (ONCE_REWRITE_TAC [EQ_SYM_EQ]);; e (MATCH_MP_TAC REAL_OF_NUM_SUB);; e (UNDISCH_TAC `~NULL (e:((((A)list) # ((A)list) list) list))`);; e (REWRITE_TAC [GSYM LENGTH_NOT_NULL]);; e (ARITH_TAC);; e (ASM_REWRITE_TAC []);; e (POP_ASSUM (K ALL_TAC));; e (REWRITE_TAC [REAL_ARITH `(&m - &1 < &m) = (&0 < &1)`]);; e (REAL_ARITH_TAC);; e (ASM_REWRITE_TAC []);; e (UNDISCH_TAC `!(e:((((A)list) # ((A)list) list) list)) (l:(((A)list) list)) x. ~NULL e /\ ~NULL l /\ x < LENGTH l /\ y < LENGTH l /\ (!a y. MEM a e /\ y < LENGTH l ==> ~(FST a = FLAT [EL x l; EL y l])) ==> zsyn_recurs1 l e x y = F,l`);; e (DISCH_THEN (MP_TAC o SPEC `(e:((((A)list) # ((A)list) list) list))`));; e (DISCH_THEN (MP_TAC o SPEC `(l:(((A)list) list))`));; e (DISCH_THEN (MP_TAC o SPEC `x:num`));; e (ASM_SIMP_TAC []);; e (SUBGOAL_THEN `y < LENGTH (l:(((A)list) list))` ASSUME_TAC);; e (MATCH_MP_TAC LT_TRANS);; e (EXISTS_TAC `SUC y`);; e (ASM_SIMP_TAC []);; e (ARITH_TAC);; e (ASM_REWRITE_TAC []);; let RECUR1_GEN_THM = top_thm ();; (*---------------------------------------------------------------------------*) (* RECUR2_NO_MATCH_THM *) (*---------------------------------------------------------------------------*) g `!x e l y. ~NULL e /\ ~NULL l /\ (x < LENGTH l) /\ (y < LENGTH l) /\ (!a x y. (MEM a e) /\ (x < LENGTH l) /\ (y < LENGTH l) ==> ~(MEM (FST a) [HD (zsyn_conjun_intro l x y)])) ==> (zsyn_recurs2 (l:(((A)list) list)) (e:((((A)list) # ((A)list) list) list)) x y = (F,l))`;; e (INDUCT_TAC);; e (REWRITE_TAC [zsyn_conjun_intro; HD; MEM]);; e (REPEAT STRIP_TAC);; e (REWRITE_TAC [zsyn_recurs2]);; e (SUBGOAL_THEN `(zsyn_recurs1 (l:(((A)list) list)) (e:((((A)list) # ((A)list) list) list)) 0 (y:num) = (F, l))` ASSUME_TAC);; e (MATCH_MP_TAC RECUR1_GEN_THM);; e (ASM_SIMP_TAC [zsyn_conjun_intro; HD; MEM]);; e (ASM_REWRITE_TAC []);; e (POP_ASSUM MP_TAC);; e (SIMP_TAC [zsyn_conjun_intro; LENGTH; MEM; HD]);; e (REPEAT STRIP_TAC);; e (REWRITE_TAC [zsyn_recurs2]);; e (SUBGOAL_THEN `(zsyn_recurs1 (l:(((A)list) list)) (e:((((A)list) # ((A)list) list) list)) (SUC x) (y:num) = (F, l))` ASSUME_TAC);; e (MATCH_MP_TAC RECUR1_GEN_THM);; e (ASM_SIMP_TAC [zsyn_conjun_intro; HD; MEM]);; e (ASM_SIMP_TAC []);; e (UNDISCH_TAC `!(e:((((A)list) # ((A)list) list) list)) (l:(((A)list) list)) y. ~NULL e /\ ~NULL l /\ x < LENGTH l /\ y < LENGTH l /\ (!a x y. MEM a e /\ x < LENGTH l /\ y < LENGTH l ==> ~(FST a = FLAT [EL x l; EL y l])) ==> zsyn_recurs2 l e x y = F,l`);; e (DISCH_THEN (MP_TAC o SPEC `(e:((((A)list) # ((A)list) list) list))`));; e (DISCH_THEN (MP_TAC o SPEC `(l:(((A)list) list))`));; e (DISCH_THEN (MP_TAC o SPEC `LENGTH (l:(((A)list) list)) - 1`));; e (ASM_SIMP_TAC []);; e (SUBGOAL_THEN `x < LENGTH (l:(((A)list) list))` ASSUME_TAC);; e (MATCH_MP_TAC LT_TRANS);; e (EXISTS_TAC `SUC x`);; e (ASM_SIMP_TAC []);; e (ARITH_TAC);; e (ASM_REWRITE_TAC []);; e (SUBGOAL_THEN `LENGTH (l:(((A)list) list)) - 1 < LENGTH l` ASSUME_TAC);; e (REWRITE_TAC [GSYM REAL_OF_NUM_LT]);; e (SUBGOAL_THEN `&(LENGTH (l:(((A)list) list)) - 1) = &(LENGTH l) - &1` ASSUME_TAC);; e (ONCE_REWRITE_TAC [EQ_SYM_EQ]);; e (MATCH_MP_TAC REAL_OF_NUM_SUB);; e (UNDISCH_TAC `~NULL (l:(((A)list) list))`);; e (REWRITE_TAC [GSYM LENGTH_NOT_NULL]);; e (ARITH_TAC);; e (ASM_REWRITE_TAC []);; e (POP_ASSUM (K ALL_TAC));; e (REWRITE_TAC [REAL_ARITH `(&m - &1 < &m) = (&0 < &1)`]);; e (REAL_ARITH_TAC);; e (ASM_REWRITE_TAC []);; let RECUR2_GEN_THM = top_thm ();; (*---------------------------------------------------------------------------*) (* Z_DEDUCTION_RECUR_NO_MATCH_THM *) (*---------------------------------------------------------------------------*) g `!le e l x y. ~NULL e /\ ~NULL l /\ (x < LENGTH l) /\ (y < LENGTH l) /\ (le <= LENGTH e)/\ (!a x y. (MEM a e) /\ (x < LENGTH l) /\ (y < LENGTH l) ==> ~(MEM (FST a) [HD (zsyn_conjun_intro l x y)])) ==> (zsyn_deduct_recurs (l:(((A)list) list)) (e:((((A)list) # ((A)list) list) list)) x y le = (T,l))`;; e (INDUCT_TAC);; e (REWRITE_TAC [zsyn_conjun_intro; HD; MEM]);; e (REPEAT STRIP_TAC);; e (REWRITE_TAC [zsyn_deduct_recurs]);; e (REWRITE_TAC [zsyn_deduct_recurs]);; e (REPEAT STRIP_TAC);; e (SUBGOAL_THEN `(zsyn_recurs2 (l:(((A)list) list)) (e:((((A)list) # ((A)list) list) list)) x (y:num) = (F, l))` ASSUME_TAC);; e (MATCH_MP_TAC RECUR2_GEN_THM);; e (ASM_SIMP_TAC [zsyn_conjun_intro; HD; MEM]);; e (ASM_REWRITE_TAC []);; e (SUBGOAL_THEN `(zsyn_recurs2 (l:(((A)list) list)) (e:((((A)list) # ((A)list) list) list)) (LENGTH l - 1) (LENGTH l - 1) = (F, l))` ASSUME_TAC);; e (MATCH_MP_TAC RECUR2_GEN_THM);; e (ASM_SIMP_TAC [zsyn_conjun_intro; HD; MEM]);; e (SUBGOAL_THEN `LENGTH (l:(((A)list) list)) - 1 < LENGTH l` ASSUME_TAC);; e (REWRITE_TAC [GSYM REAL_OF_NUM_LT]);; e (SUBGOAL_THEN `&(LENGTH (l:(((A)list) list)) - 1) = &(LENGTH l) - &1` ASSUME_TAC);; e (ONCE_REWRITE_TAC [EQ_SYM_EQ]);; e (MATCH_MP_TAC REAL_OF_NUM_SUB);; e (UNDISCH_TAC `~NULL (l:(((A)list) list))`);; e (REWRITE_TAC [GSYM LENGTH_NOT_NULL]);; e (ARITH_TAC);; e (ASM_REWRITE_TAC []);; e (POP_ASSUM (K ALL_TAC));; e (REWRITE_TAC [REAL_ARITH `(&m - &1 < &m) = (&0 < &1)`]);; e (REAL_ARITH_TAC);; e (ASM_REWRITE_TAC []);; e (ASM_REWRITE_TAC []);; let RECUR_DED_GEN_THM = top_thm ();; (*---------------------------------------------------------------------------*) (* z_DEDUCTION_NO_MATCH_THM *) (*---------------------------------------------------------------------------*) g `!e l. ~NULL e /\ ~NULL l /\ (!a x y. (MEM a e) /\ (x < LENGTH l) /\ (y < LENGTH l) ==> ~(MEM (FST a) [HD (zsyn_conjun_intro l x y)])) ==> (zsyn_deduct (l:(((A)list) list)) (e:((((A)list) # ((A)list) list) list)) = l)`;; e (REPEAT GEN_TAC);; e (SIMP_TAC [zsyn_conjun_intro; HD; MEM]);; e (REWRITE_TAC [zsyn_deduct]);; e (REPEAT STRIP_TAC);; e (SUBGOAL_THEN `(zsyn_deduct_recurs (l:(((A)list) list)) (e:((((A)list) # ((A)list) list) list)) (LENGTH l - 1) (LENGTH l - 1) (LENGTH e)) = (T,l)` ASSUME_TAC);; e (MATCH_MP_TAC RECUR_DED_GEN_THM);; e (ASM_SIMP_TAC [zsyn_conjun_intro; HD; MEM; LENGTH_NOT_NULL]);; e (CONJ_TAC);; e (SUBGOAL_THEN `LENGTH (l:(((A)list) list)) - 1 < LENGTH l` ASSUME_TAC);; e (REWRITE_TAC [GSYM REAL_OF_NUM_LT]);; e (SUBGOAL_THEN `&(LENGTH (l:(((A)list) list)) - 1) = &(LENGTH l) - &1` ASSUME_TAC);; e (ONCE_REWRITE_TAC [EQ_SYM_EQ]);; e (MATCH_MP_TAC REAL_OF_NUM_SUB);; e (UNDISCH_TAC `~NULL (l:(((A)list) list))`);; e (REWRITE_TAC [GSYM LENGTH_NOT_NULL]);; e (ARITH_TAC);; e (ASM_REWRITE_TAC []);; e (POP_ASSUM (K ALL_TAC));; e (REWRITE_TAC [REAL_ARITH `(&m - &1 < &m) = (&0 < &1)`]);; e (REAL_ARITH_TAC);; e (ASM_REWRITE_TAC []);; e (CONJ_TAC);; e (SUBGOAL_THEN `LENGTH (l:(((A)list) list)) - 1 < LENGTH l` ASSUME_TAC);; e (REWRITE_TAC [GSYM REAL_OF_NUM_LT]);; e (SUBGOAL_THEN `&(LENGTH (l:(((A)list) list)) - 1) = &(LENGTH l) - &1` ASSUME_TAC);; e (ONCE_REWRITE_TAC [EQ_SYM_EQ]);; e (MATCH_MP_TAC REAL_OF_NUM_SUB);; e (UNDISCH_TAC `~NULL (l:(((A)list) list))`);; e (REWRITE_TAC [GSYM LENGTH_NOT_NULL]);; e (ARITH_TAC);; e (ASM_REWRITE_TAC []);; e (POP_ASSUM (K ALL_TAC));; e (REWRITE_TAC [REAL_ARITH `(&m - &1 < &m) = (&0 < &1)`]);; e (REAL_ARITH_TAC);; e (ASM_REWRITE_TAC []);; e (ARITH_TAC);; e (ASM_REWRITE_TAC []);; let Z_NOMATCH_THM = top_thm ();; (*--------------------------------END_OF_FILE--------------------------------*)