1open HolKernel Parse boolLib bossLib; 2 3(* 4quietdec := true; 5val hol_dir = concat Globals.HOLDIR "/"; 6val home_dir = (concat hol_dir "examples/temporal_deep/"); 7loadPath := (concat home_dir "src/deep_embeddings") :: 8 (concat home_dir "src/tools") :: 9 !loadPath; 10 11map load 12 ["metisLib", "rltlTheory", "full_ltlTheory", "prop_logicTheory", 13 "pred_setTheory"]; 14*) 15 16open rltlTheory full_ltlTheory prop_logicTheory pred_setTheory; 17open Sanity; 18 19(* 20show_assums := false; 21show_assums := true; 22show_types := true; 23show_types := false; 24quietdec := false; 25*) 26 27 28val _ = new_theory "rltl_to_ltl"; 29 30 31val RLTL_TO_LTL_def = 32 Define 33 `(RLTL_TO_LTL a r (RLTL_PROP b)= 34 LTL_PROP(P_OR(a, P_AND(b, P_NOT r)))) 35 /\ 36 (RLTL_TO_LTL a r (RLTL_NOT f)= 37 LTL_NOT(RLTL_TO_LTL r a f)) 38 /\ 39 (RLTL_TO_LTL a r (RLTL_AND(f1,f2)) = 40 LTL_AND(RLTL_TO_LTL a r f1, RLTL_TO_LTL a r f2)) 41 /\ 42 (RLTL_TO_LTL a r (RLTL_NEXT f)= 43 LTL_OR(LTL_PROP a, LTL_AND(LTL_NEXT(RLTL_TO_LTL a r f), LTL_NOT(LTL_PROP r)))) 44 /\ 45 (RLTL_TO_LTL a r (RLTL_SUNTIL(f1, f2))= 46 LTL_SUNTIL(RLTL_TO_LTL a r f1, RLTL_TO_LTL a r f2)) 47 /\ 48 (RLTL_TO_LTL a r (RLTL_ACCEPT (f, b)) = 49 RLTL_TO_LTL (P_OR(a, P_AND(b, P_NOT(r)))) r f)`; 50 51 52 53val RLTL_TO_LTL_REWRITES = 54 store_thm 55 ("RLTL_TO_LTL_REWRITES", 56 ``!a r f1 f2. 57 (RLTL_TO_LTL a r (RLTL_OR(f1,f2)) = LTL_OR(RLTL_TO_LTL a r f1, RLTL_TO_LTL a r f2)) /\ 58 (RLTL_TO_LTL a r (RLTL_IMPL(f1,f2)) = LTL_IMPL(RLTL_TO_LTL r a f1, RLTL_TO_LTL a r f2)) /\ 59 (RLTL_TO_LTL a r (RLTL_BEFORE(f1,f2)) = LTL_BEFORE(RLTL_TO_LTL a r f1, RLTL_TO_LTL r a f2)) /\ 60 (RLTL_TO_LTL a r (RLTL_SBEFORE(f1,f2)) = LTL_SBEFORE(RLTL_TO_LTL a r f1, RLTL_TO_LTL r a f2))``, 61 62 EVAL_TAC THEN PROVE_TAC[]); 63 64val LTL_USED_VARS___RLTL_TO_LTL = 65 store_thm 66 ("LTL_USED_VARS___RLTL_TO_LTL", 67 ``!f a r. LTL_USED_VARS (RLTL_TO_LTL a r f) = (RLTL_USED_VARS f UNION P_USED_VARS a UNION P_USED_VARS r)``, 68 69 INDUCT_THEN rltl_induct ASSUME_TAC THEN REPEAT STRIP_TAC THENL [ 70 SIMP_TAC std_ss [RLTL_TO_LTL_def, LTL_USED_VARS_EVAL, P_USED_VARS_EVAL, RLTL_USED_VARS_def, EXTENSION, 71 IN_UNION] THEN 72 PROVE_TAC[], 73 74 ASM_SIMP_TAC std_ss [RLTL_TO_LTL_def, LTL_USED_VARS_def, 75 RLTL_USED_VARS_def] THEN 76 SIMP_TAC std_ss [EXTENSION, IN_UNION] THEN 77 PROVE_TAC[], 78 79 80 ASM_SIMP_TAC std_ss [RLTL_TO_LTL_def, LTL_USED_VARS_def, 81 RLTL_USED_VARS_def] THEN 82 SIMP_TAC std_ss [EXTENSION, IN_UNION] THEN 83 PROVE_TAC[], 84 85 ASM_SIMP_TAC std_ss [RLTL_TO_LTL_def, LTL_USED_VARS_def, 86 RLTL_USED_VARS_def, LTL_OR_def] THEN 87 SIMP_TAC std_ss [EXTENSION, IN_UNION] THEN 88 PROVE_TAC[], 89 90 ASM_SIMP_TAC std_ss [RLTL_TO_LTL_def, LTL_USED_VARS_def, 91 RLTL_USED_VARS_def] THEN 92 SIMP_TAC std_ss [EXTENSION, IN_UNION] THEN 93 PROVE_TAC[], 94 95 ASM_SIMP_TAC std_ss [RLTL_TO_LTL_def, LTL_USED_VARS_def, 96 RLTL_USED_VARS_def, P_USED_VARS_EVAL] THEN 97 SIMP_TAC std_ss [EXTENSION, IN_UNION] THEN 98 PROVE_TAC[] 99 ]); 100 101 102 103val RLTL_TO_LTL_THM = 104 store_thm 105 ("RLTL_TO_LTL_THM", 106 ``!f v a r t. (RLTL_SEM_TIME t v a r f = LTL_SEM_TIME t v (RLTL_TO_LTL a r f))``, 107 108 INDUCT_THEN rltl_induct ASSUME_TAC THEN REPEAT STRIP_TAC THEN 109 SIMP_TAC std_ss [LTL_SEM_THM, RLTL_SEM_THM, RLTL_TO_LTL_def, P_SEM_THM] THEN METIS_TAC[]); 110 111 112val RLTL_TO_LTL_THM___KS_SEM = 113 store_thm 114 ("RLTL_TO_LTL_THM___KS_SEM", 115 ``!f k. (RLTL_KS_SEM k f = LTL_KS_SEM k (RLTL_TO_LTL P_FALSE P_FALSE f))``, 116 117 SIMP_TAC std_ss [RLTL_KS_SEM_def, LTL_KS_SEM_def, RLTL_SEM_def, LTL_SEM_def, 118 RLTL_TO_LTL_THM]); 119 120 121val FUTURE_LTL_TO_RLTL_def = 122 Define 123 `(FUTURE_LTL_TO_RLTL (LTL_PROP b) = (RLTL_PROP b)) /\ 124 (FUTURE_LTL_TO_RLTL (LTL_NOT f) = (RLTL_NOT (FUTURE_LTL_TO_RLTL f))) /\ 125 (FUTURE_LTL_TO_RLTL (LTL_AND(f1,f2)) = (RLTL_AND(FUTURE_LTL_TO_RLTL f1, FUTURE_LTL_TO_RLTL f2))) /\ 126 (FUTURE_LTL_TO_RLTL (LTL_NEXT f) = (RLTL_NEXT (FUTURE_LTL_TO_RLTL f))) /\ 127 (FUTURE_LTL_TO_RLTL (LTL_SUNTIL(f1,f2)) = (RLTL_SUNTIL(FUTURE_LTL_TO_RLTL f1, FUTURE_LTL_TO_RLTL f2)))`; 128 129 130val FUTURE_LTL_TO_RLTL_THM = 131 store_thm 132 ("FUTURE_LTL_TO_RLTL_THM", 133 ``!f v t. ((IS_FUTURE_LTL f) ==> (LTL_SEM_TIME t v f = RLTL_SEM_TIME t v P_FALSE P_FALSE (FUTURE_LTL_TO_RLTL f)))``, 134 135 INDUCT_THEN ltl_induct ASSUME_TAC THEN REPEAT STRIP_TAC THEN 136 FULL_SIMP_TAC std_ss [LTL_SEM_THM, RLTL_SEM_THM, FUTURE_LTL_TO_RLTL_def, P_SEM_THM, IS_FUTURE_LTL_def]); 137 138 139val IS_RLTL_LTL_THM = 140 store_thm 141 ("IS_RLTL_LTL_THM", 142 143 ``!f a r. (IS_RLTL_G f = IS_LTL_G (RLTL_TO_LTL a r f)) /\ 144 (IS_RLTL_F f = IS_LTL_F (RLTL_TO_LTL a r f)) /\ 145 (IS_RLTL_GF f = IS_LTL_GF (RLTL_TO_LTL a r f)) /\ 146 (IS_RLTL_FG f = IS_LTL_FG (RLTL_TO_LTL a r f)) /\ 147 (IS_RLTL_PREFIX f = IS_LTL_PREFIX (RLTL_TO_LTL a r f)) /\ 148 (IS_RLTL_STREET f = IS_LTL_STREET (RLTL_TO_LTL a r f))``, 149 150 INDUCT_THEN rltl_induct STRIP_ASSUME_TAC THEN 151 REWRITE_TAC[IS_RLTL_THM, IS_LTL_THM, RLTL_TO_LTL_def, LTL_OR_def] THEN 152 ASM_REWRITE_TAC[] THEN 153 METIS_TAC[]); 154 155 156val IS_LTL_RLTL_THM = 157 store_thm 158 ("IS_LTL_RLTL_THM", 159 160 ``!f. (IS_FUTURE_LTL f) ==> 161 ((IS_LTL_G f = IS_RLTL_G (FUTURE_LTL_TO_RLTL f)) /\ 162 (IS_LTL_F f = IS_RLTL_F (FUTURE_LTL_TO_RLTL f)) /\ 163 (IS_LTL_GF f = IS_RLTL_GF (FUTURE_LTL_TO_RLTL f)) /\ 164 (IS_LTL_FG f = IS_RLTL_FG (FUTURE_LTL_TO_RLTL f)) /\ 165 (IS_LTL_PREFIX f = IS_RLTL_PREFIX (FUTURE_LTL_TO_RLTL f)) /\ 166 (IS_LTL_STREET f = IS_RLTL_STREET (FUTURE_LTL_TO_RLTL f)))``, 167 168 INDUCT_THEN ltl_induct STRIP_ASSUME_TAC THEN 169 FULL_SIMP_TAC std_ss[IS_RLTL_THM, IS_LTL_THM, IS_FUTURE_LTL_def, FUTURE_LTL_TO_RLTL_def, LTL_OR_def]); 170 171 172val _ = export_theory(); 173