1
2(*****************************************************************************)
3(* Create "UnclockedSugarSemanticsTheory" containing unclocked "SEM 1"       *)
4(* semantics of the basic language.                                          *)
5(*                                                                           *)
6(* Created Wed Dec 25 23:02:12 GMT 2002                                      *)
7(*****************************************************************************)
8
9(*****************************************************************************)
10(* START BOILERPLATE                                                         *)
11(*****************************************************************************)
12
13(******************************************************************************
14* Load theory of finite and infinite sequences and additional definitions of
15functions on lists (commented out for compilation)
16******************************************************************************)
17(*
18quietdec := true;
19map load
20 ["SyntaxTheory", "SyntacticSugarTheory", "PSLPathTheory", "KripkeTheory",
21  "rich_listTheory", "intLib"];
22
23open SyntaxTheory SyntacticSugarTheory
24     PSLPathTheory KripkeTheory listTheory rich_listTheory intLib;
25
26val _ = intLib.deprecate_int();
27quietdec := false;
28*)
29
30(******************************************************************************
31* Boilerplate needed for compilation
32******************************************************************************)
33open HolKernel Parse boolLib bossLib;
34
35(******************************************************************************
36* Open theories of sequences and lists
37******************************************************************************)
38open SyntaxTheory SyntacticSugarTheory PSLPathTheory KripkeTheory
39     listTheory rich_listTheory intLib;
40
41(******************************************************************************
42* Set default parsing to natural numbers rather than integers
43******************************************************************************)
44val _ = intLib.deprecate_int();
45
46(*****************************************************************************)
47(* END BOILERPLATE                                                           *)
48(*****************************************************************************)
49
50(******************************************************************************
51* Start a new theory called UnclockedSugarSemantics
52******************************************************************************)
53val _ = new_theory "UnclockedSemantics";
54
55(******************************************************************************
56* pureDefine doesn't export definitions to theCompset (for EVAL).
57******************************************************************************)
58val pureDefine = with_flag (computeLib.auto_import_definitions, false) Define;
59
60(******************************************************************************
61* B_SEM l b means "l |= b" where l is a letter, i.e. l : 'prop -> bool
62******************************************************************************)
63val B_SEM_def =
64 Define
65  `(B_SEM l (B_PROP(p:'prop)) = p IN l)
66   /\
67   (B_SEM l (B_NOT b)         = ~(B_SEM l b))
68   /\
69   (B_SEM l (B_AND(b1,b2))    = B_SEM l b1 /\ B_SEM l b2)`;
70
71val B_SEM =
72 store_thm
73  ("B_SEM",
74   ``(B_SEM l (B_PROP p)     = p IN l)
75     /\
76     (B_SEM l B_TRUE         = T)
77     /\
78     (B_SEM l B_FALSE        = F)
79     /\
80     (B_SEM l (B_NOT b)      = ~(B_SEM l b))
81     /\
82     (B_SEM l (B_AND(b1,b2)) = B_SEM l b1 /\ B_SEM l b2)
83     /\
84     (B_SEM l (B_OR(b1,b2)) = B_SEM l b1 \/ B_SEM l b2)``,
85   RW_TAC std_ss [B_SEM_def,B_OR_def,B_TRUE_def,B_FALSE_def]
86    THEN PROVE_TAC[]);
87
88(******************************************************************************
89* Unclocked "SEM 1" semantics of SEREs.
90* US_SEM w r means "w is in the language of r" in the unclocked semantics
91* where w is a word, i.e. a list of letters: w : ('prop -> bool)list
92******************************************************************************)
93val US_SEM_def =
94 pureDefine
95  `(US_SEM w (S_BOOL b) = (LENGTH w = 1) /\ B_SEM (ELEM w 0) b)
96   /\
97   (US_SEM w (S_CAT(r1,r2)) =
98     ?w1 w2. (w = w1 <> w2) /\ US_SEM w1 r1 /\ US_SEM w2 r2)
99   /\
100   (US_SEM w (S_FUSION(r1,r2)) =
101     ?w1 w2 l. (w = w1 <> [l] <> w2) /\
102               US_SEM (w1<>[l]) r1 /\ US_SEM ([l]<>w2) r2)
103   /\
104   (US_SEM w (S_OR(r1,r2)) =
105     US_SEM w r1 \/ US_SEM w r2)
106   /\
107   (US_SEM w (S_AND(r1,r2)) =
108     US_SEM w r1 /\ US_SEM w r2)
109   /\
110   (US_SEM w (S_REPEAT r) =
111     ?wlist. (w = CONCAT wlist) /\ EVERY (\w. US_SEM w r) wlist)`;
112
113(******************************************************************************
114* Original unclocked "SEM 1" semantics of Sugar formulas
115* UF_SEM w f means "w |= f"  in the unclocked semantics
116* where w is a finite or infinite word i.e. w : ('prop -> bool)path
117******************************************************************************)
118val OLD_UF_SEM_def =
119 Define
120   `(OLD_UF_SEM w (F_BOOL b) =
121      B_SEM (ELEM w 0) b)
122    /\
123    (OLD_UF_SEM w (F_NOT f) =
124      ~(OLD_UF_SEM w f))
125    /\
126    (OLD_UF_SEM w (F_AND(f1,f2)) =
127      OLD_UF_SEM w f1 /\ OLD_UF_SEM w f2)
128    /\
129    (OLD_UF_SEM w (F_NEXT f) =
130      LENGTH w > 1 /\ OLD_UF_SEM (RESTN w 1) f)
131    /\
132    (OLD_UF_SEM w (F_UNTIL(f1,f2)) =
133      ?k :: (0 to LENGTH w).
134        OLD_UF_SEM (RESTN w k) f2 /\ !j :: (0 to k). OLD_UF_SEM (RESTN w j) f1)
135    /\
136    (OLD_UF_SEM w (F_SUFFIX_IMP(r,f)) =
137      !j :: (0 to LENGTH w).
138        US_SEM (SEL w (0,j)) r ==> OLD_UF_SEM (RESTN w j) f)
139    /\
140    (OLD_UF_SEM w (F_STRONG_IMP(r1,r2)) =
141      !j :: (0 to LENGTH w).
142        US_SEM (SEL w (0,j)) r1
143        ==>
144        ?k :: (j to LENGTH w). US_SEM (SEL w (j,k)) r2)
145    /\
146    (OLD_UF_SEM w (F_WEAK_IMP(r1,r2)) =
147      !j :: (0 to LENGTH w).
148        US_SEM (SEL w (0,j)) r1
149        ==>
150        ((?k :: (j to LENGTH w). US_SEM (SEL w (j,k)) r2)
151         \/
152         (!k :: (j to LENGTH w). ?w'. US_SEM (SEL w (j,k) <> w') r2)))
153    /\
154    (OLD_UF_SEM w (F_ABORT (f,b)) =
155      OLD_UF_SEM w f
156      \/
157      OLD_UF_SEM w (F_BOOL b)
158      \/
159      ?j :: (1 to LENGTH w).
160        ?w'. OLD_UF_SEM (RESTN w j) (F_BOOL b)
161             /\
162             OLD_UF_SEM (CAT(SEL w (0,j-1),w')) f)`;
163
164(******************************************************************************
165* Unclocked "SEM 1" semantics of Sugar formulas
166* with additional |w|>0 for boolean formulas
167* UF_SEM w f means "w |= f"  in the unclocked semantics
168* where w is a finite or infinite word i.e. w : ('prop -> bool)path
169******************************************************************************)
170val UF_SEM_def =
171 Define
172   `(UF_SEM w (F_BOOL b) =
173      LENGTH w > 0 /\ B_SEM (ELEM w 0) b)
174    /\
175    (UF_SEM w (F_NOT f) =
176      ~(UF_SEM w f))
177    /\
178    (UF_SEM w (F_AND(f1,f2)) =
179      UF_SEM w f1 /\ UF_SEM w f2)
180    /\
181    (UF_SEM w (F_NEXT f) =
182      LENGTH w > 1 /\ UF_SEM (RESTN w 1) f)
183    /\
184    (UF_SEM w (F_UNTIL(f1,f2)) =
185      ?k :: (0 to LENGTH w).
186        UF_SEM (RESTN w k) f2 /\ !j :: (0 to k). UF_SEM (RESTN w j) f1)
187    /\
188    (UF_SEM w (F_SUFFIX_IMP(r,f)) =
189      !j :: (0 to LENGTH w).
190        US_SEM (SEL w (0,j)) r ==> UF_SEM (RESTN w j) f)
191    /\
192    (UF_SEM w (F_STRONG_IMP(r1,r2)) =
193      !j :: (0 to LENGTH w).
194        US_SEM (SEL w (0,j)) r1
195        ==>
196        ?k :: (j to LENGTH w). US_SEM (SEL w (j,k)) r2)
197    /\
198    (UF_SEM w (F_WEAK_IMP(r1,r2)) =
199      !j :: (0 to LENGTH w).
200        US_SEM (SEL w (0,j)) r1
201        ==>
202        ((?k :: (j to LENGTH w). US_SEM (SEL w (j,k)) r2)
203         \/
204         (!k :: (j to LENGTH w). ?w'. US_SEM (SEL w (j,k) <> w') r2)))
205    /\
206    (UF_SEM w (F_ABORT (f,b)) =
207      UF_SEM w f
208      \/
209      UF_SEM w (F_BOOL b)
210      \/
211      ?j :: (1 to LENGTH w).
212        ?w'. UF_SEM (RESTN w j) (F_BOOL b)
213             /\
214             UF_SEM (CAT(SEL w (0,j-1),w')) f)`;
215
216(******************************************************************************
217* PATH M p is true iff p is a path with respect to transition relation M.R
218******************************************************************************)
219val PATH_def = Define `PATH M p s = IS_INFINITE p /\ (ELEM p 0 = s) /\ (!n. M.R(ELEM p n, ELEM p (n+1)))`;
220
221(******************************************************************************
222* O_SEM M s f means "M, s |= f"
223******************************************************************************)
224val O_SEM_def =
225 Define
226  `(O_SEM M (O_BOOL b) s = B_SEM (M.L s) b)
227   /\
228   (O_SEM M (O_NOT f) s = ~(O_SEM M f s))
229   /\
230   (O_SEM M (O_AND(f1,f2)) s = O_SEM M f1 s /\ O_SEM M f2 s)
231   /\
232   (O_SEM M (O_EX f) s =
233     ?p. PATH M p s /\ O_SEM M f (ELEM p 1))
234   /\
235   (O_SEM M (O_EU(f1,f2)) s =
236     ?p. PATH M p s /\
237         ?k :: (0 to LENGTH p). O_SEM M f2 (ELEM p k) /\ !j. j < k ==> O_SEM M f1 (ELEM p j))
238   /\
239   (O_SEM M (O_EG f) s =
240     ?p. PATH M p s /\ !j :: (0 to LENGTH p). O_SEM M f (ELEM p j))`;
241
242val _ = export_theory();
243
244