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