1(* -*- Mode: holscript; -*- ***************************************************) 2(* *) 3(* Translation from Reset Linear Temporal Logic (RLTL) to LTL *) 4(* *) 5(******************************************************************************) 6 7open HolKernel Parse boolLib bossLib; 8 9open rltlTheory full_ltlTheory prop_logicTheory pred_setTheory; 10 11open Sanity; 12 13val _ = new_theory "rltl_to_ltl"; 14 15val RLTL_TO_LTL_def = Define (* see [1, p.35] *) 16 `(RLTL_TO_LTL a r (RLTL_PROP b) = LTL_PROP(P_OR(a, P_AND(b, P_NOT r)))) /\ 17 (RLTL_TO_LTL a r (RLTL_NOT f) = LTL_NOT(RLTL_TO_LTL r a f)) /\ 18 (RLTL_TO_LTL a r (RLTL_AND(f1,f2)) = 19 LTL_AND(RLTL_TO_LTL a r f1, RLTL_TO_LTL a r f2)) /\ 20 (RLTL_TO_LTL a r (RLTL_NEXT f) = 21 LTL_OR(LTL_PROP a, LTL_AND(LTL_NEXT(RLTL_TO_LTL a r f), LTL_NOT(LTL_PROP r)))) /\ 22 (RLTL_TO_LTL a r (RLTL_SUNTIL(f1, f2)) = 23 LTL_SUNTIL(RLTL_TO_LTL a r f1, RLTL_TO_LTL a r f2)) /\ 24 (RLTL_TO_LTL a r (RLTL_ACCEPT (f, b)) = 25 RLTL_TO_LTL (P_OR(a, P_AND(b, P_NOT(r)))) r f)`; 26 27Theorem RLTL_TO_LTL_REWRITES : 28 !a r f1 f2. 29 (RLTL_TO_LTL a r (RLTL_OR(f1,f2)) = LTL_OR(RLTL_TO_LTL a r f1, RLTL_TO_LTL a r f2)) /\ 30 (RLTL_TO_LTL a r (RLTL_IMPL(f1,f2)) = LTL_IMPL(RLTL_TO_LTL r a f1, RLTL_TO_LTL a r f2)) /\ 31 (RLTL_TO_LTL a r (RLTL_BEFORE(f1,f2)) = LTL_BEFORE(RLTL_TO_LTL a r f1, RLTL_TO_LTL r a f2)) /\ 32 (RLTL_TO_LTL a r (RLTL_SBEFORE(f1,f2)) = LTL_SBEFORE(RLTL_TO_LTL a r f1, RLTL_TO_LTL r a f2)) 33Proof 34 EVAL_TAC THEN PROVE_TAC[] 35QED 36 37Theorem LTL_USED_VARS___RLTL_TO_LTL : 38 !f a r. LTL_USED_VARS (RLTL_TO_LTL a r f) = 39 (RLTL_USED_VARS f) UNION (P_USED_VARS a) UNION (P_USED_VARS r) 40Proof 41 INDUCT_THEN rltl_induct ASSUME_TAC 42 >> rpt STRIP_TAC 43 >| [ SIMP_TAC std_ss [RLTL_TO_LTL_def, LTL_USED_VARS_EVAL, P_USED_VARS_EVAL, 44 RLTL_USED_VARS_def, EXTENSION, IN_UNION] THEN 45 PROVE_TAC[], 46 47 ASM_SIMP_TAC std_ss [RLTL_TO_LTL_def, LTL_USED_VARS_def, 48 RLTL_USED_VARS_def] THEN 49 SIMP_TAC std_ss [EXTENSION, IN_UNION] THEN 50 PROVE_TAC[], 51 52 53 ASM_SIMP_TAC std_ss [RLTL_TO_LTL_def, LTL_USED_VARS_def, 54 RLTL_USED_VARS_def] THEN 55 SIMP_TAC std_ss [EXTENSION, IN_UNION] THEN 56 PROVE_TAC[], 57 58 ASM_SIMP_TAC std_ss [RLTL_TO_LTL_def, LTL_USED_VARS_def, 59 RLTL_USED_VARS_def, LTL_OR_def] THEN 60 SIMP_TAC std_ss [EXTENSION, IN_UNION] THEN 61 PROVE_TAC[], 62 63 ASM_SIMP_TAC std_ss [RLTL_TO_LTL_def, LTL_USED_VARS_def, 64 RLTL_USED_VARS_def] THEN 65 SIMP_TAC std_ss [EXTENSION, IN_UNION] THEN 66 PROVE_TAC[], 67 68 ASM_SIMP_TAC std_ss [RLTL_TO_LTL_def, LTL_USED_VARS_def, 69 RLTL_USED_VARS_def, P_USED_VARS_EVAL] THEN 70 SIMP_TAC std_ss [EXTENSION, IN_UNION] THEN 71 PROVE_TAC[] ] 72QED 73 74Theorem RLTL_TO_LTL_THM : 75 !f v a r t. RLTL_SEM_TIME t v a r f = LTL_SEM_TIME t v (RLTL_TO_LTL a r f) 76Proof 77 INDUCT_THEN rltl_induct ASSUME_TAC 78 >> rpt STRIP_TAC 79 >> SIMP_TAC std_ss [LTL_SEM_THM, RLTL_SEM_THM, RLTL_TO_LTL_def, P_SEM_THM] 80 >> METIS_TAC [] 81QED 82 83Theorem RLTL_TO_LTL_THM___KS_SEM : 84 !f k. (RLTL_KS_SEM k f = LTL_KS_SEM k (RLTL_TO_LTL P_FALSE P_FALSE f)) 85Proof 86 SIMP_TAC std_ss [RLTL_KS_SEM_def, LTL_KS_SEM_def, RLTL_SEM_def, LTL_SEM_def, 87 RLTL_TO_LTL_THM] 88QED 89 90val FUTURE_LTL_TO_RLTL_def = Define 91 `(FUTURE_LTL_TO_RLTL (LTL_PROP b) = (RLTL_PROP b)) /\ 92 (FUTURE_LTL_TO_RLTL (LTL_NOT f) = (RLTL_NOT (FUTURE_LTL_TO_RLTL f))) /\ 93 (FUTURE_LTL_TO_RLTL (LTL_AND(f1,f2)) = 94 (RLTL_AND(FUTURE_LTL_TO_RLTL f1, FUTURE_LTL_TO_RLTL f2))) /\ 95 (FUTURE_LTL_TO_RLTL (LTL_NEXT f) = (RLTL_NEXT (FUTURE_LTL_TO_RLTL f))) /\ 96 (FUTURE_LTL_TO_RLTL (LTL_SUNTIL(f1,f2)) = 97 (RLTL_SUNTIL(FUTURE_LTL_TO_RLTL f1, FUTURE_LTL_TO_RLTL f2)))`; 98 99Theorem FUTURE_LTL_TO_RLTL_THM : 100 !f v t. IS_FUTURE_LTL f ==> 101 (LTL_SEM_TIME t v f = RLTL_SEM_TIME t v P_FALSE P_FALSE (FUTURE_LTL_TO_RLTL f)) 102Proof 103 INDUCT_THEN ltl_induct ASSUME_TAC 104 >> REPEAT STRIP_TAC 105 >> FULL_SIMP_TAC std_ss [LTL_SEM_THM, RLTL_SEM_THM, FUTURE_LTL_TO_RLTL_def, 106 P_SEM_THM, IS_FUTURE_LTL_def] 107QED 108 109Theorem IS_RLTL_LTL_THM : 110 !f a r. (IS_RLTL_G f = IS_LTL_G (RLTL_TO_LTL a r f)) /\ 111 (IS_RLTL_F f = IS_LTL_F (RLTL_TO_LTL a r f)) /\ 112 (IS_RLTL_GF f = IS_LTL_GF (RLTL_TO_LTL a r f)) /\ 113 (IS_RLTL_FG f = IS_LTL_FG (RLTL_TO_LTL a r f)) /\ 114 (IS_RLTL_PREFIX f = IS_LTL_PREFIX (RLTL_TO_LTL a r f)) /\ 115 (IS_RLTL_STREET f = IS_LTL_STREET (RLTL_TO_LTL a r f)) 116Proof 117 INDUCT_THEN rltl_induct STRIP_ASSUME_TAC 118 >> REWRITE_TAC [IS_RLTL_THM, IS_LTL_THM, RLTL_TO_LTL_def, LTL_OR_def] 119 >> ASM_REWRITE_TAC [] 120 >> METIS_TAC [] 121QED 122 123Theorem IS_LTL_RLTL_THM : 124 !f. IS_FUTURE_LTL f ==> 125 (IS_LTL_G f = IS_RLTL_G (FUTURE_LTL_TO_RLTL f)) /\ 126 (IS_LTL_F f = IS_RLTL_F (FUTURE_LTL_TO_RLTL f)) /\ 127 (IS_LTL_GF f = IS_RLTL_GF (FUTURE_LTL_TO_RLTL f)) /\ 128 (IS_LTL_FG f = IS_RLTL_FG (FUTURE_LTL_TO_RLTL f)) /\ 129 (IS_LTL_PREFIX f = IS_RLTL_PREFIX (FUTURE_LTL_TO_RLTL f)) /\ 130 (IS_LTL_STREET f = IS_RLTL_STREET (FUTURE_LTL_TO_RLTL f)) 131Proof 132 INDUCT_THEN ltl_induct STRIP_ASSUME_TAC 133 >> FULL_SIMP_TAC std_ss [IS_RLTL_THM, IS_LTL_THM, IS_FUTURE_LTL_def, 134 FUTURE_LTL_TO_RLTL_def, LTL_OR_def] 135QED 136 137val _ = export_theory(); 138 139(* References: 140 141 [1] Tuerk, T., Schneider, K.: A hierarchy for Accellera's property specification language, (2005). 142 *) 143