1
2(*****************************************************************************)
3(* Create "Clockedsugarsemanticstheory" containing clocked  semantics        *)
4(* of PSL Version 1.1.                                                       *)
5(*****************************************************************************)
6
7(*****************************************************************************)
8(* START BOILERPLATE                                                         *)
9(*****************************************************************************)
10
11(******************************************************************************
12* Load theory of syntax, paths and models
13* (commented out for compilation)
14******************************************************************************)
15(*
16quietdec := true;
17map load
18 ["SyntaxTheory","UnclockedSemanticsTheory"];
19open SyntaxTheory PSLPathTheory ModelTheory UnclockedSemanticsTheory;
20quietdec := false;
21*)
22
23(******************************************************************************
24* Boilerplate needed for compilation
25******************************************************************************)
26open HolKernel Parse boolLib bossLib;
27
28(******************************************************************************
29* Open theories of sequences and lists
30******************************************************************************)
31open SyntaxTheory PSLPathTheory ModelTheory UnclockedSemanticsTheory;
32
33(*****************************************************************************)
34(* END BOILERPLATE                                                           *)
35(*****************************************************************************)
36
37(******************************************************************************
38* Start a new theory called ClockedSemantics
39******************************************************************************)
40val _ = new_theory "ClockedSemantics";
41val _ = ParseExtras.temp_loose_equality()
42
43(******************************************************************************
44* pureDefine doesn't export definitions to theCompset (for EVAL).
45******************************************************************************)
46val pureDefine = with_flag (computeLib.auto_import_definitions, false) Define;
47
48(******************************************************************************
49* CLOCK_TICK v c formalises "v is a clock tick of c"
50******************************************************************************)
51val CLOCK_TICK_def =
52 Define
53  `CLOCK_TICK v c =
54    LENGTH v > 0                    /\
55    B_SEM (ELEM v (LENGTH v - 1)) c /\
56    !i :: LESS(LENGTH v - 1). B_SEM (ELEM v i) (B_NOT c)`;
57
58(******************************************************************************
59* Clocked semantics of SEREs.
60* S_SEM v r means "v is in the language of r" in the clocked semantics
61* where v is a finite word, i.e. a list of letters: v :  ('a letter)list.
62* S_SEM_def is a simple structural recursion for easy definition
63* (see clause for ``S_SEM v (S_REPEAT r)``).
64* Theorem S_SEM gives LRM v1.1 version.
65******************************************************************************)
66val S_SEM_def =
67 pureDefine
68  `(S_SEM v c (S_BOOL b) = CLOCK_TICK v c /\ B_SEM (ELEM v (LENGTH v - 1)) b)
69   /\
70   (S_SEM v c (S_CAT(r1,r2)) =
71     ?v1 v2. (v = v1 <> v2) /\ S_SEM v1 c r1 /\ S_SEM v2 c r2)
72   /\
73   (S_SEM v c (S_FUSION(r1,r2)) =
74     ?v1 v2 l. (v = v1 <> [l] <> v2) /\
75               S_SEM (v1<>[l]) c r1 /\ S_SEM ([l]<>v2) c r2)
76   /\
77   (S_SEM v c (S_OR(r1,r2)) =
78     S_SEM v c r1 \/ S_SEM v c r2)
79   /\
80   (S_SEM v c (S_AND(r1,r2)) =
81     S_SEM v c r1 /\ S_SEM v c r2)
82   /\
83   (S_SEM v c S_EMPTY =
84     (v = []))
85   /\
86   (S_SEM v c (S_REPEAT r) =
87     ?vlist. (v = CONCAT vlist) /\ EVERY (\v. S_SEM v c r) vlist)
88   /\
89   (S_SEM v c (S_CLOCK(r,c1)) =
90       S_SEM v c1 r)`;
91
92(* Lemma for deriving theorem S_SEM below *)
93val S_SEM_REPEAT =
94 store_thm
95  ("S_SEM_REPEAT",
96   ``S_SEM v c (S_REPEAT r) =
97      S_SEM v c S_EMPTY \/
98      ?v1 v2.
99       ~(v=[]) /\ (v = v1 <> v2) /\ S_SEM v1 c r /\ S_SEM v2 c (S_REPEAT r)``,
100    Induct_on `v`
101     THEN RW_TAC std_ss [S_SEM_def]
102     THENL
103      [Q.EXISTS_TAC `[]`
104        THEN RW_TAC list_ss [FinitePSLPathTheory.CONCAT_def],
105       EQ_TAC
106        THEN RW_TAC list_ss []
107        THENL
108         [Cases_on `vlist`
109           THEN FULL_SIMP_TAC list_ss [FinitePSLPathTheory.CONCAT_def]
110           THEN Q.EXISTS_TAC `h'` THEN Q.EXISTS_TAC `CONCAT t`
111           THEN PROVE_TAC[],
112          Q.EXISTS_TAC `v1::vlist`
113           THEN RW_TAC list_ss [FinitePSLPathTheory.CONCAT_def]]]);
114
115
116(******************************************************************************
117* Clocked semantics of SEREs.
118* S_SEM v r means "v is in the language of r" in the clocked semantics: v |=c r
119* where v is a finite word, i.e. a list of letters: v :  ('a letter)list.
120* S_SEM_def is a simple structural recursion for easy definition
121* (see clause for ``S_SEM v (S_REPEAT r)``).
122* Theorem S_SEM gives LRM v1.1 version.
123******************************************************************************)
124val S_SEM =
125 store_thm
126  ("S_SEM",
127   ``(S_SEM v c (S_BOOL b) = CLOCK_TICK v c /\ B_SEM (ELEM v (LENGTH v - 1)) b)
128     /\
129     (S_SEM v c (S_CAT(r1,r2)) =
130       ?v1 v2. (v = v1 <> v2) /\ S_SEM v1 c r1 /\ S_SEM v2 c r2)
131     /\
132     (S_SEM v c (S_FUSION(r1,r2)) =
133       ?v1 v2 l. (v = v1 <> [l] <> v2) /\
134                 S_SEM (v1<>[l]) c r1 /\ S_SEM ([l]<>v2) c r2)
135     /\
136     (S_SEM v c (S_OR(r1,r2)) =
137       S_SEM v c r1 \/ S_SEM v c r2)
138     /\
139     (S_SEM v c (S_AND(r1,r2)) =
140       S_SEM v c r1 /\ S_SEM v c r2)
141     /\
142     (S_SEM v c S_EMPTY =
143       (v = []))
144     /\
145     (S_SEM v c (S_REPEAT r) =
146       S_SEM v c S_EMPTY \/
147        ?v1 v2.
148         ~(v=[]) /\ (v = v1 <> v2) /\ S_SEM v1 c r /\ S_SEM v2 c (S_REPEAT r))
149     /\
150     (S_SEM v c (S_CLOCK(r,c1)) =
151         S_SEM v c1 r)``,
152   RW_TAC std_ss [S_SEM_def, GSYM S_SEM_REPEAT]);
153
154
155(******************************************************************************
156* F_SEM v c f means "v |=c f"  in the clocked semantics
157* where v is a finite or infinite word i.e. v : ('prop letter)path
158* F_SEM_def is unfolded version for easy definition.
159* Theorem F_SEM gives version corresponding to LRM v1.1
160******************************************************************************)
161val F_SEM_def =
162 Define
163   `(F_SEM v c (F_NOT f) =
164      ~(F_SEM (COMPLEMENT v) c f))
165    /\
166    (F_SEM v c (F_AND(f1,f2)) =
167      F_SEM v c f1 /\ F_SEM v c f2)
168    /\
169    (F_SEM v c (F_STRONG_BOOL b) =
170      ?j :: LESS(LENGTH v). CLOCK_TICK (SEL v (0,j)) c /\ B_SEM (ELEM v j) b)
171    /\
172    (F_SEM v c (F_WEAK_BOOL b) =
173      !j :: LESS(LENGTH v).
174        CLOCK_TICK (SEL (COMPLEMENT v) (0,j)) c ==> B_SEM (ELEM v j) b)
175    /\
176    (F_SEM v c (F_STRONG_SERE r) =
177      ?j :: LESS(LENGTH v). S_SEM (SEL v (0,j)) c r)
178(*
179    /\
180    (F_SEM v c (F_WEAK_SERE r) =
181      !j :: LESS(LENGTH v).
182       F_SEM (CAT(SEL v (0,j),TOP_OMEGA)) c (F_STRONG_SERE r))
183*)
184    /\
185    (F_SEM v c (F_WEAK_SERE r) =
186      !j :: LESS(LENGTH v).
187        ?k :: LESS(LENGTH(CAT(SEL v (0,j),TOP_OMEGA))).
188          S_SEM (SEL(CAT(SEL v (0,j),TOP_OMEGA)) (0,k)) c r)
189    /\
190    (F_SEM v c (F_NEXT f) =
191      ?j k :: LESS(LENGTH v).
192        j < k                        /\
193        CLOCK_TICK (SEL v (0,j)) c   /\
194        CLOCK_TICK (SEL v (j+1,k)) c /\
195        F_SEM (RESTN v k) c f)
196    /\
197    (F_SEM v c (F_UNTIL(f1,f2)) =
198      ?k :: LESS(LENGTH v).
199        B_SEM (ELEM v k) c /\
200        F_SEM (RESTN v k) c f2 /\
201        !j :: LESS k. B_SEM (ELEM (COMPLEMENT v) j) c ==> F_SEM (RESTN v j) c f1)
202    /\
203(* Contains j=0 bug spoteed by Thomas Turk
204    (F_SEM v c (F_ABORT (f,b)) =
205      F_SEM v c f
206      \/
207      ?j :: LESS(LENGTH v).
208         B_SEM (ELEM v j) b /\ F_SEM (CAT(SEL v (0,j-1),TOP_OMEGA)) c f)
209*)
210    (F_SEM v c (F_ABORT (f,b)) =
211      F_SEM v c f
212      \/
213      ?j :: LESS(LENGTH v).
214         B_SEM (ELEM v j) b
215         /\
216         if j=0 then F_SEM TOP_OMEGA c f
217                else F_SEM (CAT(SEL v (0,j-1),TOP_OMEGA)) c f)
218    /\
219    (F_SEM v c (F_CLOCK(f,c1)) =
220      F_SEM v c1 f)
221    /\
222    (F_SEM v c (F_SUFFIX_IMP(r,f)) =
223      !j :: LESS(LENGTH v).
224        S_SEM (SEL (COMPLEMENT v) (0,j)) c r ==> F_SEM (RESTN v j) c f)`;
225
226(******************************************************************************
227* F_SEM v c f means "v |=c f"  in the clocked semantics
228* where v is a finite or infinite word i.e. v : ('prop letter)path
229* F_SEM_def is unfolded version for easy definition.
230* Theorem F_SEM gives version corresponding to LRM v1.1
231******************************************************************************)
232val F_SEM =
233 store_thm
234  ("F_SEM",
235   ``(F_SEM v c (F_NOT f) =
236       ~(F_SEM (COMPLEMENT v) c f))
237     /\
238     (F_SEM v c (F_AND(f1,f2)) =
239       F_SEM v c f1 /\ F_SEM v c f2)
240     /\
241     (F_SEM v c (F_STRONG_BOOL b) =
242       ?j :: LESS(LENGTH v). CLOCK_TICK (SEL v (0,j)) c /\ B_SEM (ELEM v j) b)
243     /\
244     (F_SEM v c (F_WEAK_BOOL b) =
245       !j :: LESS(LENGTH v).
246         CLOCK_TICK (SEL (COMPLEMENT v) (0,j)) c ==> B_SEM (ELEM v j) b)
247     /\
248     (F_SEM v c (F_STRONG_SERE r) =
249       ?j :: LESS(LENGTH v). S_SEM (SEL v (0,j)) c r)
250     /\
251     (F_SEM v c (F_WEAK_SERE r) =
252       !j :: LESS(LENGTH v).
253        F_SEM (CAT(SEL v (0,j),TOP_OMEGA)) c (F_STRONG_SERE r))
254(*
255     /\
256     (F_SEM v c (F_WEAK_SERE r) =
257       !j :: LESS(LENGTH v).
258         ?k :: LESS(LENGTH(CAT(SEL v (0,j),TOP_OMEGA))).
259           S_SEM (SEL(CAT(SEL v (0,j),TOP_OMEGA)) (0,k)) c r)
260*)
261     /\
262     (F_SEM v c (F_NEXT f) =
263       ?j k :: LESS(LENGTH v).
264         j < k                        /\
265         CLOCK_TICK (SEL v (0,j)) c   /\
266         CLOCK_TICK (SEL v (j+1,k)) c /\
267         F_SEM (RESTN v k) c f)
268     /\
269     (F_SEM v c (F_UNTIL(f1,f2)) =
270       ?k :: LESS(LENGTH v).
271         B_SEM (ELEM v k) c /\
272         F_SEM (RESTN v k) c f2 /\
273         !j :: LESS k. B_SEM (ELEM (COMPLEMENT v) j) c ==> F_SEM (RESTN v j) c f1)
274     /\
275(* Contains j=0 bug spoteed by Thomas Turk
276    (F_SEM v c (F_ABORT (f,b)) =
277      F_SEM v c f
278      \/
279      ?j :: LESS(LENGTH v).
280         B_SEM (ELEM v j) b /\ F_SEM (CAT(SEL v (0,j-1),TOP_OMEGA)) c f)
281*)
282    (F_SEM v c (F_ABORT (f,b)) =
283      F_SEM v c f
284      \/
285      ?j :: LESS(LENGTH v).
286         B_SEM (ELEM v j) b
287         /\
288         if j=0 then F_SEM TOP_OMEGA c f
289                else F_SEM (CAT(SEL v (0,j-1),TOP_OMEGA)) c f)
290     /\
291     (F_SEM v c (F_CLOCK(f,c1)) =
292       F_SEM v c1 f)
293     /\
294     (F_SEM v c (F_SUFFIX_IMP(r,f)) =
295       !j :: LESS(LENGTH v).
296         S_SEM (SEL (COMPLEMENT v) (0,j)) c r ==> F_SEM (RESTN v j) c f)``,
297   RW_TAC std_ss [F_SEM_def]);
298
299val _ = export_theory();
300