1
2(*****************************************************************************)
3(* Create "UnclockedSemanticsTheory" containing unclocked  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;
17loadPath                                  (* Add path to loadPath            *)
18 :=
19 "../../path" :: !loadPath;
20map load
21 ["SyntaxTheory","PSLPathTheory","ModelTheory"];
22quietdec := false;
23*)
24
25(******************************************************************************
26* Boilerplate needed for compilation
27******************************************************************************)
28open HolKernel Parse boolLib bossLib;
29
30(******************************************************************************
31* Open theories of sequences and lists
32******************************************************************************)
33open SyntaxTheory PSLPathTheory ModelTheory;
34
35(*****************************************************************************)
36(* END BOILERPLATE                                                           *)
37(*****************************************************************************)
38
39(******************************************************************************
40* Start a new theory called UnclockedSemantics
41******************************************************************************)
42val _ = new_theory "UnclockedSemantics";
43
44(******************************************************************************
45* pureDefine doesn't export definitions to theCompset (for EVAL).
46******************************************************************************)
47val pureDefine = with_flag (computeLib.auto_import_definitions, false) Define;
48
49(* Moved to ModelScript.sml
50(******************************************************************************
51* A letter is either TOP, or BOTTOM
52* or a set of atomic propositions repersenting a state
53******************************************************************************)
54val letter_def =
55 Hol_datatype
56  `letter = TOP | BOTTOM | STATE of ('prop -> bool)`;
57*)
58
59(******************************************************************************
60* B_SEM l b means "l ||= b" where l is a letter
61******************************************************************************)
62val B_SEM_def =
63 Define
64  `(B_SEM TOP b = T)
65   /\
66   (B_SEM BOTTOM b = F)
67   /\
68   (B_SEM (STATE s) (B_PROP(p:'prop)) = p IN s)
69   /\
70   (B_SEM (STATE s) B_TRUE = T)
71   /\
72   (B_SEM (STATE s) B_FALSE = F)
73   /\
74   (B_SEM (STATE s) (B_NOT b) = ~(B_SEM (STATE s) b))
75   /\
76   (B_SEM (STATE s) (B_AND(b1,b2)) = B_SEM (STATE s) b1 /\ B_SEM (STATE s) b2)`;
77
78(******************************************************************************
79* Unclocked semantics of SEREs.
80* US_SEM v r means "v is in the language of r" in the unclocked semantics
81* where v is a finite word, i.e. a list of letters: v :  ('a letter)list.
82* US_SEM_def is a simple structural recursion for easy definition
83* (see clause for ``US_SEM v (S_REPEAT r)``).
84* Theorem US_SEM gives version corresponding to LRM Version 1.1.
85******************************************************************************)
86val US_SEM_def =
87 pureDefine
88  `(US_SEM v (S_BOOL b) = (LENGTH v = 1) /\ B_SEM (ELEM v 0) b)
89   /\
90   (US_SEM v (S_CAT(r1,r2)) =
91     ?v1 v2. (v = v1 <> v2) /\ US_SEM v1 r1 /\ US_SEM v2 r2)
92   /\
93   (US_SEM v (S_FUSION(r1,r2)) =
94     ?v1 v2 l. (v = v1 <> [l] <> v2) /\
95               US_SEM (v1<>[l]) r1 /\ US_SEM ([l]<>v2) r2)
96   /\
97   (US_SEM v (S_OR(r1,r2)) =
98     US_SEM v r1 \/ US_SEM v r2)
99   /\
100   (US_SEM v (S_AND(r1,r2)) =
101     US_SEM v r1 /\ US_SEM v r2)
102   /\
103   (US_SEM v S_EMPTY =
104     (v = []))
105   /\
106   (US_SEM v (S_REPEAT r) =
107     ?vlist. (v = CONCAT vlist) /\ EVERY (\v. US_SEM v r) vlist)`;
108
109(* Lemma for deriving theorem US_SEM below *)
110val US_SEM_REPEAT =
111 store_thm
112  ("US_SEM_REPEAT",
113   ``US_SEM v (S_REPEAT r) =
114      US_SEM v S_EMPTY \/
115      ?v1 v2.
116       ~(v=[]) /\ (v = v1 <> v2) /\ US_SEM v1 r /\ US_SEM v2 (S_REPEAT r)``,
117    Induct_on `v`
118     THEN RW_TAC std_ss [US_SEM_def]
119     THENL
120      [Q.EXISTS_TAC `[]`
121        THEN RW_TAC list_ss [FinitePSLPathTheory.CONCAT_def],
122       EQ_TAC
123        THEN RW_TAC list_ss []
124        THENL
125         [Cases_on `vlist`
126           THEN FULL_SIMP_TAC list_ss [FinitePSLPathTheory.CONCAT_def]
127           THEN Q.EXISTS_TAC `h'` THEN Q.EXISTS_TAC `CONCAT t`
128           THEN PROVE_TAC[],
129          Q.EXISTS_TAC `v1::vlist`
130           THEN RW_TAC list_ss [FinitePSLPathTheory.CONCAT_def]]]);
131
132(******************************************************************************
133* Unclocked semantics of SEREs.
134* US_SEM v r means "v is in the language of r" in the unclocked semantics
135* where v is a finite word, i.e. a list of letters: v :  ('a letter)list.
136* US_SEM_def is a simple structural recursion for easy definition
137* (see clause for ``US_SEM v (S_REPEAT r)``).
138* Theorem US_SEM gives version corresponding to LRM Version 1.1.
139******************************************************************************)
140val US_SEM =
141 store_thm
142  ("US_SEM",
143   ``(US_SEM v (S_BOOL b) = (LENGTH v = 1) /\ B_SEM (ELEM v 0) b)
144     /\
145     (US_SEM v (S_CAT(r1,r2)) =
146       ?v1 v2. (v = v1 <> v2) /\ US_SEM v1 r1 /\ US_SEM v2 r2)
147     /\
148     (US_SEM v (S_FUSION(r1,r2)) =
149       ?v1 v2 l. (v = v1 <> [l] <> v2) /\
150                 US_SEM (v1<>[l]) r1 /\ US_SEM ([l]<>v2) r2)
151     /\
152     (US_SEM v (S_OR(r1,r2)) =
153       US_SEM v r1 \/ US_SEM v r2)
154     /\
155     (US_SEM v (S_AND(r1,r2)) =
156       US_SEM v r1 /\ US_SEM v r2)
157     /\
158     (US_SEM v S_EMPTY =
159       (v = []))
160     /\
161     (US_SEM v (S_REPEAT r) =
162       US_SEM v S_EMPTY \/
163        ?v1 v2.
164         ~(v=[]) /\ (v = v1 <> v2) /\ US_SEM v1 r /\ US_SEM v2 (S_REPEAT r))``,
165   RW_TAC std_ss [US_SEM_def, GSYM US_SEM_REPEAT]);
166
167(******************************************************************************
168* Complement a path
169******************************************************************************)
170val COMPLEMENT_LETTER_def =
171 Define
172  `(COMPLEMENT_LETTER TOP      = BOTTOM) /\
173   (COMPLEMENT_LETTER BOTTOM   = TOP)    /\
174   (COMPLEMENT_LETTER(STATE s) = STATE s)`;
175
176(******************************************************************************
177* Complement a path
178******************************************************************************)
179val COMPLEMENT_def =
180 Define
181  `(COMPLEMENT(FINITE p)   = FINITE(MAP COMPLEMENT_LETTER p)) /\
182   (COMPLEMENT(INFINITE f) = INFINITE(COMPLEMENT_LETTER o f))`;
183
184(******************************************************************************
185* \top^\omega
186******************************************************************************)
187val TOP_OMEGA_def =
188 Define `TOP_OMEGA = INFINITE(\n. TOP)`;
189
190(******************************************************************************
191* LESS m is predicate to test if a number is less than m
192* LESS : num -> num -> bool
193* LESSX m is predicate to test if a number is less than extended number m
194* LESSX : xnum -> num -> bool
195* Now defined in PSLPathTheory
196******************************************************************************)
197
198(******************************************************************************
199* UF_SEM v f means "v |= f"  in the unclocked semantics
200* where v is a finite or infinite word i.e. v : ('prop -> bool)path
201* UF_SEM_def is unfolded version for easy definition.
202* Theorem UF_SEM gives version corresponding to LRM v1.1
203******************************************************************************)
204val UF_SEM_def =
205 Define
206   `(UF_SEM v (F_NOT f) =
207      ~(UF_SEM (COMPLEMENT v) f))
208    /\
209    (UF_SEM v (F_AND(f1,f2)) =
210      UF_SEM v f1 /\ UF_SEM v f2)
211    /\
212    (UF_SEM v (F_STRONG_BOOL b) =
213      (LENGTH v > 0) /\ B_SEM (ELEM v 0) b)
214    /\
215    (UF_SEM v (F_WEAK_BOOL b) =
216      (LENGTH v = XNUM 0) \/ B_SEM (ELEM v 0) b)
217    /\
218    (UF_SEM v (F_STRONG_SERE r) =
219      ?j :: (LESS(LENGTH v)). US_SEM (SEL v (0,j)) r)
220(*
221    /\
222    (UF_SEM v (F_WEAK_SERE r) =
223      !j :: (LESS(LENGTH v)).
224       UF_SEM (CAT(SEL v (0,j),TOP_OMEGA)) (F_STRONG_SERE r))
225*)
226    /\
227    (UF_SEM v (F_WEAK_SERE r) =
228      !j :: (LESS(LENGTH v)).
229        ?k :: (LESS(LENGTH(CAT(SEL v (0,j),TOP_OMEGA)))).
230          US_SEM (SEL(CAT(SEL v (0,j),TOP_OMEGA)) (0,k)) r)
231    /\
232    (UF_SEM v (F_NEXT f) =
233      LENGTH v > 1 /\ UF_SEM (RESTN v 1) f)
234    /\
235    (UF_SEM v (F_UNTIL(f1,f2)) =
236      ?k :: (LESS(LENGTH v)).
237        UF_SEM (RESTN v k) f2 /\ !j :: (LESS k). UF_SEM (RESTN v j) f1)
238    /\
239(* Contains j=0 bug spotted by Thomas Turk
240     (UF_SEM v (F_ABORT (f,b)) =
241       UF_SEM v f
242       \/
243       ?j :: (LESS(LENGTH v)).
244          B_SEM (ELEM v j) b /\ UF_SEM (CAT(SEL v (0,j-1),TOP_OMEGA)) f)
245*)
246    (UF_SEM v (F_ABORT (f,b)) =
247      UF_SEM v f
248      \/
249      ?j :: (LESS(LENGTH v)).
250        B_SEM (ELEM v j) b
251        /\
252        if j=0 then UF_SEM TOP_OMEGA f
253               else UF_SEM (CAT(SEL v (0,j-1),TOP_OMEGA)) f)
254    /\
255    (UF_SEM v (F_SUFFIX_IMP(r,f)) =
256      !j :: (LESS(LENGTH v)).
257        US_SEM (SEL (COMPLEMENT v) (0,j)) r ==> UF_SEM (RESTN v j) f)`;
258
259(******************************************************************************
260* UF_SEM v f means "v |= f"  in the unclocked semantics
261* where v is a finite or infinite word i.e. v : ('prop -> bool)path
262* UF_SEM_def is unfolded version for easy definition.
263* Theorem UF_SEM gives version corresponding to LRM v1.1
264******************************************************************************)
265val UF_SEM =
266 store_thm
267  ("UF_SEM",
268   ``(UF_SEM v (F_NOT f) =
269       ~(UF_SEM (COMPLEMENT v) f))
270     /\
271     (UF_SEM v (F_AND(f1,f2)) =
272       UF_SEM v f1 /\ UF_SEM v f2)
273     /\
274     (UF_SEM v (F_STRONG_BOOL b) =
275       (LENGTH v > 0) /\ B_SEM (ELEM v 0) b)
276     /\
277     (UF_SEM v (F_WEAK_BOOL b) =
278       (LENGTH v = XNUM 0) \/ B_SEM (ELEM v 0) b)
279     /\
280     (UF_SEM v (F_STRONG_SERE r) =
281       ?j :: (LESS(LENGTH v)). US_SEM (SEL v (0,j)) r)
282     /\
283     (UF_SEM v (F_WEAK_SERE r) =
284       !j :: (LESS(LENGTH v)).
285        UF_SEM (CAT(SEL v (0,j),TOP_OMEGA)) (F_STRONG_SERE r))
286(*
287     /\
288     (UF_SEM v (F_WEAK_SERE r) =
289       !j :: (LESS(LENGTH v)).
290         ?k :: (LESS(LENGTH(CAT(SEL v (0,j),TOP_OMEGA)))).
291           US_SEM (SEL(CAT(SEL v (0,j),TOP_OMEGA)) (0,k)) r)
292*)
293     /\
294     (UF_SEM v (F_NEXT f) =
295       LENGTH v > 1 /\ UF_SEM (RESTN v 1) f)
296     /\
297     (UF_SEM v (F_UNTIL(f1,f2)) =
298       ?k :: (LESS(LENGTH v)).
299         UF_SEM (RESTN v k) f2 /\ !j :: (LESS k). UF_SEM (RESTN v j) f1)
300     /\
301(* Contains j=0 bug spotted by Thomas Turk
302     (UF_SEM v (F_ABORT (f,b)) =
303       UF_SEM v f
304       \/
305       ?j :: (LESS(LENGTH v)).
306          B_SEM (ELEM v j) b /\ UF_SEM (CAT(SEL v (0,j-1),TOP_OMEGA)) f)
307*)
308    (UF_SEM v (F_ABORT (f,b)) =
309      UF_SEM v f
310      \/
311      ?j :: (LESS(LENGTH v)).
312        B_SEM (ELEM v j) b
313        /\
314        if j=0 then UF_SEM TOP_OMEGA f
315               else UF_SEM (CAT(SEL v (0,j-1),TOP_OMEGA)) f)
316     /\
317     (UF_SEM v (F_SUFFIX_IMP(r,f)) =
318       !j :: (LESS(LENGTH v)).
319         US_SEM (SEL (COMPLEMENT v) (0,j)) r ==> UF_SEM (RESTN v j) f)``,
320   RW_TAC std_ss [UF_SEM_def]);
321
322(*****************************************************************************)
323(* Map a function over a path (used to define Lhat -- see LRM B.2.2)         *)
324(*****************************************************************************)
325val MAP_PATH_def =
326 Define
327  `(MAP_PATH g (FINITE l) = FINITE(MAP g l))
328   /\
329   (MAP_PATH g (INFINITE f) = INFINITE(\n. g(f n)))`;
330
331(******************************************************************************
332* UF_VALID M f means "Lhat(pi) |= f" for all computations pi of M
333******************************************************************************)
334val UF_VALID_def = (* from UnclockedSemanticsScript.sml *)
335 Define
336  `UF_VALID M f =
337    !v::(COMPUTATION M). UF_SEM (MAP_PATH (\s. STATE(M.L s)) v) f`;
338
339(******************************************************************************
340* PATH M s is true of p iff p is a computation path of M
341* (now defined in ModelTheory)
342******************************************************************************)
343
344(******************************************************************************
345* O_SEM M s f means "M, s |= f"
346******************************************************************************)
347val O_SEM_def =
348 Define
349  `(O_SEM M (O_BOOL b) s = B_SEM (STATE(M.L s)) b)
350   /\
351   (O_SEM M (O_NOT f) s = ~(O_SEM M f s))
352   /\
353   (O_SEM M (O_AND(f1,f2)) s = O_SEM M f1 s /\ O_SEM M f2 s)
354   /\
355   (O_SEM M (O_EX f) s =
356     ?p :: PATH M s.
357       (LENGTH p > 1) /\ (ELEM p 0 = s) /\ O_SEM M f (ELEM p 1))
358   /\
359   (O_SEM M (O_EU(f1,f2)) s =
360     ?p :: PATH M s.
361       ?k :: (LESS(LENGTH p)).
362         (ELEM p 0 = s)        /\
363         O_SEM M f2 (ELEM p k) /\
364         !j. j < k ==> O_SEM M f1 (ELEM p j))
365   /\
366   (O_SEM M (O_EG f) s =
367     ?p :: PATH M s.
368       (ELEM p 0 = s) /\ !j :: (LESS(LENGTH p)). O_SEM M f (ELEM p j))`;
369
370(******************************************************************************
371* O_VALID M f means "M, s |= f" for all initial states s
372******************************************************************************)
373val O_VALID_def =
374 Define
375  `O_VALID M f = !s::(M.S0). O_SEM M f s`;
376
377val _ = export_theory();
378
379