1 2(*****************************************************************************) 3(* Create "ClockedSemanticsTheory" for clocked "SEM 1" and semantics *) 4(* F_SEM w c f means "w |=c= f" in the clocked semantics *) 5(* where w is a finite or infinite word i.e. w : ('prop -> bool)path *) 6(* and c is a boolean expression, i.e. c : *) 7(* *) 8(* Created Fri Dec 27 04:18:32 GMT 2002 *) 9(*****************************************************************************) 10 11(*****************************************************************************) 12(* START BOILERPLATE *) 13(*****************************************************************************) 14 15(****************************************************************************** 16* Load theory of paths and additional definitions of functions on lists 17* (commented out for compilation) 18******************************************************************************) 19(* 20quietdec := true; 21app load 22 ["bossLib", "SyntaxTheory", "PSLPathTheory", "KripkeTheory", 23 "UnclockedSemanticsTheory", "rich_listTheory", "intLib","res_quanLib"]; 24open SyntaxTheory PSLPathTheory KripkeTheory 25 UnclockedSemanticsTheory (* Needed for S_SEM w c (S_CLOCK(r,c1)) *) 26 listTheory rich_listTheory; 27val _ = intLib.deprecate_int(); 28quietdec := false; 29*) 30 31(****************************************************************************** 32* Boilerplate needed for compilation 33******************************************************************************) 34open HolKernel Parse boolLib bossLib; 35 36(****************************************************************************** 37* Open theories of paths and lists 38******************************************************************************) 39open SyntaxTheory PSLPathTheory KripkeTheory 40 UnclockedSemanticsTheory (* Needed for S_SEM w c (S_CLOCK(r,c1)) *) 41 listTheory rich_listTheory res_quanLib; 42 43(****************************************************************************** 44* Set default parsing to natural numbers rather than integers 45******************************************************************************) 46val _ = intLib.deprecate_int(); 47 48(*****************************************************************************) 49(* END BOILERPLATE *) 50(*****************************************************************************) 51 52(****************************************************************************** 53* A simpset fragment to rewrite away quantifiers restricted with :: (a to b) 54******************************************************************************) 55val resq_SS = 56 simpLib.merge_ss 57 [res_quanTools.resq_SS, 58 rewrites 59 [num_to_def,xnum_to_def,IN_DEF,num_to_def,xnum_to_def,LENGTH_def]]; 60 61(****************************************************************************** 62* Start a new theory called ClockedSemantics 63******************************************************************************) 64val _ = new_theory "ClockedSemantics"; 65val _ = ParseExtras.temp_loose_equality() 66 67(****************************************************************************** 68* Clocked semantics of SEREs 69* S_SEM w c r means "w is in the language of r in context of clock c" 70******************************************************************************) 71val S_SEM_def = 72 Define 73 `(S_SEM w c (S_BOOL b) = 74 LENGTH w >= 1 75 /\ 76 (!i :: (0 to (LENGTH w - 1)). B_SEM (ELEM w i) (B_NOT c)) 77 /\ 78 B_SEM (ELEM w (LENGTH w - 1)) (B_AND(c,b))) 79 /\ 80 (S_SEM w c (S_CAT(r1,r2)) = 81 ?w1 w2. (w = w1 <> w2) /\ S_SEM w1 c r1 /\ S_SEM w2 c r2) 82 /\ 83 (S_SEM w c (S_FUSION(r1,r2)) = 84 ?w1 w2 l. (w = w1 <> [l] <> w2) /\ 85 S_SEM (w1<>[l]) c r1 /\ S_SEM ([l]<>w2) c r2) 86 /\ 87 (S_SEM w c (S_OR(r1,r2)) = 88 S_SEM w c r1 \/ S_SEM w c r2) 89 /\ 90 (S_SEM w c (S_AND(r1,r2)) = 91 S_SEM w c r1 /\ S_SEM w c r2) 92 /\ 93 (S_SEM w c (S_REPEAT r) = 94 ?wlist. (w = CONCAT wlist) /\ EVERY (\w. S_SEM w c r) wlist) 95 /\ 96 (S_SEM w c (S_CLOCK(r,c1)) = 97 ?i :: (0 to LENGTH w). 98 US_SEM (SEL w (0,i)) (S_CAT(S_REPEAT(S_BOOL(B_NOT c1)),S_BOOL c1)) 99 /\ 100 S_SEM (RESTN w i) c1 r)`; 101 102(****************************************************************************** 103* Original clocked "SEM 1" semantics of Sugar formulas, partly unfolded 104* (see commented out stuff) to avoid need for TFL hacks to prove termination. 105******************************************************************************) 106val OLD_F_SEM_def = 107 Define 108 `(OLD_F_SEM w c (F_BOOL b) = B_SEM (ELEM w 0) b) 109 /\ 110 (OLD_F_SEM w c (F_NOT f) = 111 ~(OLD_F_SEM w c f)) 112 /\ 113 (OLD_F_SEM w c (F_AND(f1,f2)) = 114 OLD_F_SEM w c f1 /\ OLD_F_SEM w c f2) 115 /\ 116 (OLD_F_SEM w c (F_NEXT f) = 117 ?i :: (1 to LENGTH w). 118 S_SEM (SEL w (1,i)) B_TRUE (S_CAT(S_REPEAT(S_BOOL(B_NOT c)),S_BOOL c)) 119 /\ 120 OLD_F_SEM (RESTN w i) c f) 121 /\ 122 (OLD_F_SEM w c (F_UNTIL(f1,f2)) = 123 ?k :: (0 to LENGTH w). 124(* OLD_F_SEM (RESTN w k) B_TRUE (F_BOOL c) /\ *) 125 B_SEM (ELEM w k) c /\ 126 OLD_F_SEM (RESTN w k) c f2 /\ 127 !j :: (0 to k). 128(* OLD_F_SEM (RESTN w j) B_TRUE (F_BOOL c) ==> OLD_F_SEM (RESTN w j) c f1) *) 129 B_SEM (ELEM w j) c ==> OLD_F_SEM (RESTN w j) c f1) 130 /\ 131 (OLD_F_SEM w c (F_SUFFIX_IMP(r,f)) = 132 !i :: (0 to LENGTH w). 133 S_SEM (SEL w (0,i)) c r 134 ==> 135 ?j :: (i to LENGTH w). 136 S_SEM (SEL w (i,j)) B_TRUE (S_CAT(S_REPEAT(S_BOOL(B_NOT c)),S_BOOL c)) 137 /\ 138 OLD_F_SEM (RESTN w j) c f) 139 /\ 140 (OLD_F_SEM w c (F_STRONG_IMP(r1,r2)) = 141 !i :: (0 to LENGTH w). 142 S_SEM (SEL w (0,i)) c r1 143 ==> 144 ?j :: (i to LENGTH w). S_SEM (SEL w (i,j)) c r2) 145 /\ 146 (OLD_F_SEM w c (F_WEAK_IMP(r1,r2)) = 147 !i :: (0 to LENGTH w). 148 S_SEM (SEL w (0,i)) c r1 149 ==> 150 ((?j :: (i to LENGTH w). S_SEM (SEL w (i,j)) c r2) 151 \/ 152 (!j :: (i to LENGTH w). ?w'. S_SEM (SEL w (i,j) <> w') c r2))) 153 /\ 154 (OLD_F_SEM w c (F_ABORT (f,b)) = 155 OLD_F_SEM w c f 156 \/ 157(* OLD_F_SEM w c (F_BOOL b) *) 158 B_SEM (ELEM w 0) b 159 \/ 160 ?i :: (1 to LENGTH w). 161(* ?w'. OLD_F_SEM (RESTN w i) B_TRUE (F_BOOL(B_AND(c,b))) *) 162 ?w'. B_SEM (ELEM w i) (B_AND(c,b)) 163 /\ 164 OLD_F_SEM (CAT(SEL w (0,i-1),w')) c f) 165 /\ 166 (OLD_F_SEM w c (F_STRONG_CLOCK(f,c1)) = 167 ?i :: (0 to LENGTH w). 168 S_SEM (SEL w (0,i)) B_TRUE (S_CAT(S_REPEAT(S_BOOL(B_NOT c1)),S_BOOL c1)) 169 /\ 170 OLD_F_SEM (RESTN w i) c1 f)`; 171 172(****************************************************************************** 173* Derivation of "golden" form of clocked "SEM 1" semantics of Sugar formulas 174******************************************************************************) 175val OLD_F_SEM = 176 store_thm 177 ("OLD_F_SEM", 178 ``(OLD_F_SEM w c (F_BOOL b) = B_SEM (ELEM w 0) b) 179 /\ 180 (OLD_F_SEM w c (F_NOT f) = 181 ~(OLD_F_SEM w c f)) 182 /\ 183 (OLD_F_SEM w c (F_AND(f1,f2)) = 184 OLD_F_SEM w c f1 /\ OLD_F_SEM w c f2) 185 /\ 186 (OLD_F_SEM w c (F_NEXT f) = 187 ?i :: (1 to LENGTH w). 188 S_SEM (SEL w (1,i)) B_TRUE (S_CAT(S_REPEAT(S_BOOL(B_NOT c)),S_BOOL c)) 189 /\ 190 OLD_F_SEM (RESTN w i) c f) 191 /\ 192 (OLD_F_SEM w c (F_UNTIL(f1,f2)) = 193 ?k :: (0 to LENGTH w). 194 OLD_F_SEM (RESTN w k) B_TRUE (F_BOOL c) /\ 195 OLD_F_SEM (RESTN w k) c f2 /\ 196 !j :: (0 to k). 197 OLD_F_SEM (RESTN w j) B_TRUE (F_BOOL c) ==> OLD_F_SEM (RESTN w j) c f1) 198 /\ 199 (OLD_F_SEM w c (F_SUFFIX_IMP(r,f)) = 200 !i :: (0 to LENGTH w). 201 S_SEM (SEL w (0,i)) c r 202 ==> 203 ?j :: (i to LENGTH w). 204 S_SEM (SEL w (i,j)) B_TRUE (S_CAT(S_REPEAT(S_BOOL(B_NOT c)),S_BOOL c)) 205 /\ 206 OLD_F_SEM (RESTN w j) c f) 207 /\ 208 (OLD_F_SEM w c (F_STRONG_IMP(r1,r2)) = 209 !i :: (0 to LENGTH w). 210 S_SEM (SEL w (0,i)) c r1 211 ==> 212 ?j :: (i to LENGTH w). S_SEM (SEL w (i,j)) c r2) 213 /\ 214 (OLD_F_SEM w c (F_WEAK_IMP(r1,r2)) = 215 !i :: (0 to LENGTH w). 216 S_SEM (SEL w (0,i)) c r1 217 ==> 218 ((?j :: (i to LENGTH w). S_SEM (SEL w (i,j)) c r2) 219 \/ 220 (!j :: (i to LENGTH w). ?w'. S_SEM (SEL w (i,j) <> w') c r2))) 221 /\ 222 (OLD_F_SEM w c (F_ABORT (f,b)) = 223 OLD_F_SEM w c f 224 \/ 225 OLD_F_SEM w c (F_BOOL b) 226 \/ 227 ?i :: (1 to LENGTH w). 228 ?w'. OLD_F_SEM (RESTN w i) B_TRUE (F_BOOL(B_AND(c,b))) 229 /\ 230 OLD_F_SEM (CAT(SEL w (0,i-1),w')) c f) 231 /\ 232 (OLD_F_SEM w c (F_STRONG_CLOCK(f,c1)) = 233 ?i :: (0 to LENGTH w). 234 S_SEM (SEL w (0,i)) B_TRUE (S_CAT(S_REPEAT(S_BOOL(B_NOT c1)),S_BOOL c1)) 235 /\ 236 OLD_F_SEM (RESTN w i) c1 f)``, 237 RW_TAC arith_ss [OLD_F_SEM_def,ELEM_RESTN,B_SEM_def]); 238 239(****************************************************************************** 240* Clocked "SEM 1" semantics of Sugar formulas, partly unfolded 241* with additional |w|>0 for boolean formulas 242* (see commented out stuff) to avoid need for TFL hacks to prove termination. 243******************************************************************************) 244val F_SEM_def = 245 Define 246 `(F_SEM w c (F_BOOL b) = 247 LENGTH w > 0 /\ B_SEM (ELEM w 0) b) 248 /\ 249 (F_SEM w c (F_NOT f) = 250 ~(F_SEM w c f)) 251 /\ 252 (F_SEM w c (F_AND(f1,f2)) = 253 F_SEM w c f1 /\ F_SEM w c f2) 254 /\ 255 (F_SEM w c (F_NEXT f) = 256 ?i :: (1 to LENGTH w). 257 S_SEM (SEL w (1,i)) B_TRUE (S_CAT(S_REPEAT(S_BOOL(B_NOT c)),S_BOOL c)) 258 /\ 259 F_SEM (RESTN w i) c f) 260 /\ 261 (F_SEM w c (F_UNTIL(f1,f2)) = 262 ?k :: (0 to LENGTH w). 263(* F_SEM (RESTN w k) B_TRUE (F_BOOL c) /\ *) 264 B_SEM (ELEM w k) c /\ 265 F_SEM (RESTN w k) c f2 /\ 266 !j :: (0 to k). 267(* F_SEM (RESTN w j) B_TRUE (F_BOOL c) ==> F_SEM (RESTN w j) c f1) *) 268 B_SEM (ELEM w j) c ==> F_SEM (RESTN w j) c f1) 269 /\ 270 (F_SEM w c (F_SUFFIX_IMP(r,f)) = 271 !i :: (0 to LENGTH w). 272 S_SEM (SEL w (0,i)) c r 273 ==> 274 ?j :: (i to LENGTH w). 275 S_SEM (SEL w (i,j)) B_TRUE (S_CAT(S_REPEAT(S_BOOL(B_NOT c)),S_BOOL c)) 276 /\ 277 F_SEM (RESTN w j) c f) 278 /\ 279 (F_SEM w c (F_STRONG_IMP(r1,r2)) = 280 !i :: (0 to LENGTH w). 281 S_SEM (SEL w (0,i)) c r1 282 ==> 283 ?j :: (i to LENGTH w). S_SEM (SEL w (i,j)) c r2) 284 /\ 285 (F_SEM w c (F_WEAK_IMP(r1,r2)) = 286 !i :: (0 to LENGTH w). 287 S_SEM (SEL w (0,i)) c r1 288 ==> 289 ((?j :: (i to LENGTH w). S_SEM (SEL w (i,j)) c r2) 290 \/ 291 (!j :: (i to LENGTH w). ?w'. S_SEM (SEL w (i,j) <> w') c r2))) 292 /\ 293 (F_SEM w c (F_ABORT (f,b)) = 294 F_SEM w c f 295 \/ 296(* F_SEM w c (F_BOOL b) *) 297 LENGTH w > 0 /\ B_SEM (ELEM w 0) b 298 \/ 299 ?i :: (1 to LENGTH w). 300(* ?w'. F_SEM (RESTN w i) B_TRUE (F_BOOL(B_AND(c,b))) *) 301 ?w'. B_SEM (ELEM w i) (B_AND(c,b)) 302 /\ 303 F_SEM (CAT(SEL w (0,i-1),w')) c f) 304 /\ 305 (F_SEM w c (F_STRONG_CLOCK(f,c1)) = 306 ?i :: (0 to LENGTH w). 307 S_SEM (SEL w (0,i)) B_TRUE (S_CAT(S_REPEAT(S_BOOL(B_NOT c1)),S_BOOL c1)) 308 /\ 309 F_SEM (RESTN w i) c1 f)`; 310 311(****************************************************************************** 312* Derivation of "golden" form of clocked "SEM 1" semantics of Sugar formulas 313******************************************************************************) 314val F_SEM = 315 store_thm 316 ("F_SEM", 317 ``(F_SEM w c (F_BOOL b) = 318 LENGTH w > 0 /\ B_SEM (ELEM w 0) b) 319 /\ 320 (F_SEM w c (F_NOT f) = 321 ~(F_SEM w c f)) 322 /\ 323 (F_SEM w c (F_AND(f1,f2)) = 324 F_SEM w c f1 /\ F_SEM w c f2) 325 /\ 326 (F_SEM w c (F_NEXT f) = 327 ?i :: (1 to LENGTH w). 328 S_SEM (SEL w (1,i)) B_TRUE (S_CAT(S_REPEAT(S_BOOL(B_NOT c)),S_BOOL c)) 329 /\ 330 F_SEM (RESTN w i) c f) 331 /\ 332 (F_SEM w c (F_UNTIL(f1,f2)) = 333 ?k :: (0 to LENGTH w). 334 F_SEM (RESTN w k) B_TRUE (F_BOOL c) /\ 335 F_SEM (RESTN w k) c f2 /\ 336 !j :: (0 to k). 337 F_SEM (RESTN w j) B_TRUE (F_BOOL c) ==> F_SEM (RESTN w j) c f1) 338 /\ 339 (F_SEM w c (F_SUFFIX_IMP(r,f)) = 340 !i :: (0 to LENGTH w). 341 S_SEM (SEL w (0,i)) c r 342 ==> 343 ?j :: (i to LENGTH w). 344 S_SEM (SEL w (i,j)) B_TRUE (S_CAT(S_REPEAT(S_BOOL(B_NOT c)),S_BOOL c)) 345 /\ 346 F_SEM (RESTN w j) c f) 347 /\ 348 (F_SEM w c (F_STRONG_IMP(r1,r2)) = 349 !i :: (0 to LENGTH w). 350 S_SEM (SEL w (0,i)) c r1 351 ==> 352 ?j :: (i to LENGTH w). S_SEM (SEL w (i,j)) c r2) 353 /\ 354 (F_SEM w c (F_WEAK_IMP(r1,r2)) = 355 !i :: (0 to LENGTH w). 356 S_SEM (SEL w (0,i)) c r1 357 ==> 358 ((?j :: (i to LENGTH w). S_SEM (SEL w (i,j)) c r2) 359 \/ 360 (!j :: (i to LENGTH w). ?w'. S_SEM (SEL w (i,j) <> w') c r2))) 361 /\ 362 (F_SEM w c (F_ABORT (f,b)) = 363 F_SEM w c f 364 \/ 365 F_SEM w c (F_BOOL b) 366 \/ 367 ?i :: (1 to LENGTH w). 368 ?w'. F_SEM (RESTN w i) B_TRUE (F_BOOL(B_AND(c,b))) 369 /\ 370 F_SEM (CAT(SEL w (0,i-1),w')) c f) 371 /\ 372 (F_SEM w c (F_STRONG_CLOCK(f,c1)) = 373 ?i :: (0 to LENGTH w). 374 S_SEM (SEL w (0,i)) B_TRUE (S_CAT(S_REPEAT(S_BOOL(B_NOT c1)),S_BOOL c1)) 375 /\ 376 F_SEM (RESTN w i) c1 f)``, 377 RW_TAC arith_ss [F_SEM_def,ELEM_RESTN,B_SEM_def] 378 THEN Cases_on `w` 379 THEN RW_TAC (arith_ss ++ resq_SS) 380 [GT_xnum_num_def,num_to_def,xnum_to_def,RESTN_FINITE,LENGTH_def, 381 LENGTH_RESTN_INFINITE] 382 THEN EQ_TAC 383 THEN RW_TAC arith_ss [] 384 THEN RW_TAC arith_ss [] 385 THENL 386 [Q.EXISTS_TAC `k` 387 THEN RW_TAC arith_ss [FinitePSLPathTheory.LENGTH_RESTN], 388 Q.EXISTS_TAC `k` 389 THEN RW_TAC arith_ss [FinitePSLPathTheory.LENGTH_RESTN], 390 REPEAT DISJ2_TAC 391 THEN Q.EXISTS_TAC `i` 392 THEN RW_TAC arith_ss [FinitePSLPathTheory.LENGTH_RESTN] 393 THEN PROVE_TAC[], 394 REPEAT DISJ2_TAC 395 THEN Q.EXISTS_TAC `i` 396 THEN RW_TAC arith_ss [FinitePSLPathTheory.LENGTH_RESTN] 397 THEN PROVE_TAC[]]); 398 399val _ = export_theory(); 400