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