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";
54val _ = ParseExtras.temp_loose_equality()
55
56(******************************************************************************
57* pureDefine doesn't export definitions to theCompset (for EVAL).
58******************************************************************************)
59val pureDefine = with_flag (computeLib.auto_import_definitions, false) Define;
60
61(******************************************************************************
62* B_SEM l b means "l |= b" where l is a letter, i.e. l : 'prop -> bool
63******************************************************************************)
64val B_SEM_def =
65 Define
66  `(B_SEM l (B_PROP(p:'prop)) = p IN l)
67   /\
68   (B_SEM l (B_NOT b)         = ~(B_SEM l b))
69   /\
70   (B_SEM l (B_AND(b1,b2))    = B_SEM l b1 /\ B_SEM l b2)`;
71
72val B_SEM =
73 store_thm
74  ("B_SEM",
75   ``(B_SEM l (B_PROP p)     = p IN l)
76     /\
77     (B_SEM l B_TRUE         = T)
78     /\
79     (B_SEM l B_FALSE        = F)
80     /\
81     (B_SEM l (B_NOT b)      = ~(B_SEM l b))
82     /\
83     (B_SEM l (B_AND(b1,b2)) = B_SEM l b1 /\ B_SEM l b2)
84     /\
85     (B_SEM l (B_OR(b1,b2)) = B_SEM l b1 \/ B_SEM l b2)``,
86   RW_TAC std_ss [B_SEM_def,B_OR_def,B_TRUE_def,B_FALSE_def]
87    THEN PROVE_TAC[]);
88
89(******************************************************************************
90* Unclocked "SEM 1" semantics of SEREs.
91* US_SEM w r means "w is in the language of r" in the unclocked semantics
92* where w is a word, i.e. a list of letters: w : ('prop -> bool)list
93******************************************************************************)
94val US_SEM_def =
95 pureDefine
96  `(US_SEM w (S_BOOL b) = (LENGTH w = 1) /\ B_SEM (ELEM w 0) b)
97   /\
98   (US_SEM w (S_CAT(r1,r2)) =
99     ?w1 w2. (w = w1 <> w2) /\ US_SEM w1 r1 /\ US_SEM w2 r2)
100   /\
101   (US_SEM w (S_FUSION(r1,r2)) =
102     ?w1 w2 l. (w = w1 <> [l] <> w2) /\
103               US_SEM (w1<>[l]) r1 /\ US_SEM ([l]<>w2) r2)
104   /\
105   (US_SEM w (S_OR(r1,r2)) =
106     US_SEM w r1 \/ US_SEM w r2)
107   /\
108   (US_SEM w (S_AND(r1,r2)) =
109     US_SEM w r1 /\ US_SEM w r2)
110   /\
111   (US_SEM w (S_REPEAT r) =
112     ?wlist. (w = CONCAT wlist) /\ EVERY (\w. US_SEM w r) wlist)`;
113
114(******************************************************************************
115* Original unclocked "SEM 1" semantics of Sugar formulas
116* UF_SEM w f means "w |= f"  in the unclocked semantics
117* where w is a finite or infinite word i.e. w : ('prop -> bool)path
118******************************************************************************)
119val OLD_UF_SEM_def =
120 Define
121   `(OLD_UF_SEM w (F_BOOL b) =
122      B_SEM (ELEM w 0) b)
123    /\
124    (OLD_UF_SEM w (F_NOT f) =
125      ~(OLD_UF_SEM w f))
126    /\
127    (OLD_UF_SEM w (F_AND(f1,f2)) =
128      OLD_UF_SEM w f1 /\ OLD_UF_SEM w f2)
129    /\
130    (OLD_UF_SEM w (F_NEXT f) =
131      LENGTH w > 1 /\ OLD_UF_SEM (RESTN w 1) f)
132    /\
133    (OLD_UF_SEM w (F_UNTIL(f1,f2)) =
134      ?k :: (0 to LENGTH w).
135        OLD_UF_SEM (RESTN w k) f2 /\ !j :: (0 to k). OLD_UF_SEM (RESTN w j) f1)
136    /\
137    (OLD_UF_SEM w (F_SUFFIX_IMP(r,f)) =
138      !j :: (0 to LENGTH w).
139        US_SEM (SEL w (0,j)) r ==> OLD_UF_SEM (RESTN w j) f)
140    /\
141    (OLD_UF_SEM w (F_STRONG_IMP(r1,r2)) =
142      !j :: (0 to LENGTH w).
143        US_SEM (SEL w (0,j)) r1
144        ==>
145        ?k :: (j to LENGTH w). US_SEM (SEL w (j,k)) r2)
146    /\
147    (OLD_UF_SEM w (F_WEAK_IMP(r1,r2)) =
148      !j :: (0 to LENGTH w).
149        US_SEM (SEL w (0,j)) r1
150        ==>
151        ((?k :: (j to LENGTH w). US_SEM (SEL w (j,k)) r2)
152         \/
153         (!k :: (j to LENGTH w). ?w'. US_SEM (SEL w (j,k) <> w') r2)))
154    /\
155    (OLD_UF_SEM w (F_ABORT (f,b)) =
156      OLD_UF_SEM w f
157      \/
158      OLD_UF_SEM w (F_BOOL b)
159      \/
160      ?j :: (1 to LENGTH w).
161        ?w'. OLD_UF_SEM (RESTN w j) (F_BOOL b)
162             /\
163             OLD_UF_SEM (CAT(SEL w (0,j-1),w')) f)`;
164
165(******************************************************************************
166* Unclocked "SEM 1" semantics of Sugar formulas
167* with additional |w|>0 for boolean formulas
168* UF_SEM w f means "w |= f"  in the unclocked semantics
169* where w is a finite or infinite word i.e. w : ('prop -> bool)path
170******************************************************************************)
171val UF_SEM_def =
172 Define
173   `(UF_SEM w (F_BOOL b) =
174      LENGTH w > 0 /\ B_SEM (ELEM w 0) b)
175    /\
176    (UF_SEM w (F_NOT f) =
177      ~(UF_SEM w f))
178    /\
179    (UF_SEM w (F_AND(f1,f2)) =
180      UF_SEM w f1 /\ UF_SEM w f2)
181    /\
182    (UF_SEM w (F_NEXT f) =
183      LENGTH w > 1 /\ UF_SEM (RESTN w 1) f)
184    /\
185    (UF_SEM w (F_UNTIL(f1,f2)) =
186      ?k :: (0 to LENGTH w).
187        UF_SEM (RESTN w k) f2 /\ !j :: (0 to k). UF_SEM (RESTN w j) f1)
188    /\
189    (UF_SEM w (F_SUFFIX_IMP(r,f)) =
190      !j :: (0 to LENGTH w).
191        US_SEM (SEL w (0,j)) r ==> UF_SEM (RESTN w j) f)
192    /\
193    (UF_SEM w (F_STRONG_IMP(r1,r2)) =
194      !j :: (0 to LENGTH w).
195        US_SEM (SEL w (0,j)) r1
196        ==>
197        ?k :: (j to LENGTH w). US_SEM (SEL w (j,k)) r2)
198    /\
199    (UF_SEM w (F_WEAK_IMP(r1,r2)) =
200      !j :: (0 to LENGTH w).
201        US_SEM (SEL w (0,j)) r1
202        ==>
203        ((?k :: (j to LENGTH w). US_SEM (SEL w (j,k)) r2)
204         \/
205         (!k :: (j to LENGTH w). ?w'. US_SEM (SEL w (j,k) <> w') r2)))
206    /\
207    (UF_SEM w (F_ABORT (f,b)) =
208      UF_SEM w f
209      \/
210      UF_SEM w (F_BOOL b)
211      \/
212      ?j :: (1 to LENGTH w).
213        ?w'. UF_SEM (RESTN w j) (F_BOOL b)
214             /\
215             UF_SEM (CAT(SEL w (0,j-1),w')) f)`;
216
217(******************************************************************************
218* PATH M p is true iff p is a path with respect to transition relation M.R
219******************************************************************************)
220val PATH_def = Define `PATH M p s = IS_INFINITE p /\ (ELEM p 0 = s) /\ (!n. M.R(ELEM p n, ELEM p (n+1)))`;
221
222(******************************************************************************
223* O_SEM M s f means "M, s |= f"
224******************************************************************************)
225val O_SEM_def =
226 Define
227  `(O_SEM M (O_BOOL b) s = B_SEM (M.L s) b)
228   /\
229   (O_SEM M (O_NOT f) s = ~(O_SEM M f s))
230   /\
231   (O_SEM M (O_AND(f1,f2)) s = O_SEM M f1 s /\ O_SEM M f2 s)
232   /\
233   (O_SEM M (O_EX f) s =
234     ?p. PATH M p s /\ O_SEM M f (ELEM p 1))
235   /\
236   (O_SEM M (O_EU(f1,f2)) s =
237     ?p. PATH M p s /\
238         ?k :: (0 to LENGTH p). O_SEM M f2 (ELEM p k) /\ !j. j < k ==> O_SEM M f1 (ELEM p j))
239   /\
240   (O_SEM M (O_EG f) s =
241     ?p. PATH M p s /\ !j :: (0 to LENGTH p). O_SEM M f (ELEM p j))`;
242
243val _ = export_theory();
244