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