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