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"; 65 66(****************************************************************************** 67* Clocked semantics of SEREs 68* S_SEM w c r means "w is in the language of r in context of clock c" 69******************************************************************************) 70val S_SEM_def = 71 Define 72 `(S_SEM w c (S_BOOL b) = 73 LENGTH w >= 1 74 /\ 75 (!i :: (0 to (LENGTH w - 1)). B_SEM (ELEM w i) (B_NOT c)) 76 /\ 77 B_SEM (ELEM w (LENGTH w - 1)) (B_AND(c,b))) 78 /\ 79 (S_SEM w c (S_CAT(r1,r2)) = 80 ?w1 w2. (w = w1 <> w2) /\ S_SEM w1 c r1 /\ S_SEM w2 c r2) 81 /\ 82 (S_SEM w c (S_FUSION(r1,r2)) = 83 ?w1 w2 l. (w = w1 <> [l] <> w2) /\ 84 S_SEM (w1<>[l]) c r1 /\ S_SEM ([l]<>w2) c r2) 85 /\ 86 (S_SEM w c (S_OR(r1,r2)) = 87 S_SEM w c r1 \/ S_SEM w c r2) 88 /\ 89 (S_SEM w c (S_AND(r1,r2)) = 90 S_SEM w c r1 /\ S_SEM w c r2) 91 /\ 92 (S_SEM w c (S_REPEAT r) = 93 ?wlist. (w = CONCAT wlist) /\ EVERY (\w. S_SEM w c r) wlist) 94 /\ 95 (S_SEM w c (S_CLOCK(r,c1)) = 96 ?i :: (0 to LENGTH w). 97 US_SEM (SEL w (0,i)) (S_CAT(S_REPEAT(S_BOOL(B_NOT c1)),S_BOOL c1)) 98 /\ 99 S_SEM (RESTN w i) c1 r)`; 100 101(****************************************************************************** 102* Original clocked "SEM 1" semantics of Sugar formulas, partly unfolded 103* (see commented out stuff) to avoid need for TFL hacks to prove termination. 104******************************************************************************) 105val OLD_F_SEM_def = 106 Define 107 `(OLD_F_SEM w c (F_BOOL b) = B_SEM (ELEM w 0) b) 108 /\ 109 (OLD_F_SEM w c (F_NOT f) = 110 ~(OLD_F_SEM w c f)) 111 /\ 112 (OLD_F_SEM w c (F_AND(f1,f2)) = 113 OLD_F_SEM w c f1 /\ OLD_F_SEM w c f2) 114 /\ 115 (OLD_F_SEM w c (F_NEXT f) = 116 ?i :: (1 to LENGTH w). 117 S_SEM (SEL w (1,i)) B_TRUE (S_CAT(S_REPEAT(S_BOOL(B_NOT c)),S_BOOL c)) 118 /\ 119 OLD_F_SEM (RESTN w i) c f) 120 /\ 121 (OLD_F_SEM w c (F_UNTIL(f1,f2)) = 122 ?k :: (0 to LENGTH w). 123(* OLD_F_SEM (RESTN w k) B_TRUE (F_BOOL c) /\ *) 124 B_SEM (ELEM w k) c /\ 125 OLD_F_SEM (RESTN w k) c f2 /\ 126 !j :: (0 to k). 127(* OLD_F_SEM (RESTN w j) B_TRUE (F_BOOL c) ==> OLD_F_SEM (RESTN w j) c f1) *) 128 B_SEM (ELEM w j) c ==> OLD_F_SEM (RESTN w j) c f1) 129 /\ 130 (OLD_F_SEM w c (F_SUFFIX_IMP(r,f)) = 131 !i :: (0 to LENGTH w). 132 S_SEM (SEL w (0,i)) c r 133 ==> 134 ?j :: (i to LENGTH w). 135 S_SEM (SEL w (i,j)) B_TRUE (S_CAT(S_REPEAT(S_BOOL(B_NOT c)),S_BOOL c)) 136 /\ 137 OLD_F_SEM (RESTN w j) c f) 138 /\ 139 (OLD_F_SEM w c (F_STRONG_IMP(r1,r2)) = 140 !i :: (0 to LENGTH w). 141 S_SEM (SEL w (0,i)) c r1 142 ==> 143 ?j :: (i to LENGTH w). S_SEM (SEL w (i,j)) c r2) 144 /\ 145 (OLD_F_SEM w c (F_WEAK_IMP(r1,r2)) = 146 !i :: (0 to LENGTH w). 147 S_SEM (SEL w (0,i)) c r1 148 ==> 149 ((?j :: (i to LENGTH w). S_SEM (SEL w (i,j)) c r2) 150 \/ 151 (!j :: (i to LENGTH w). ?w'. S_SEM (SEL w (i,j) <> w') c r2))) 152 /\ 153 (OLD_F_SEM w c (F_ABORT (f,b)) = 154 OLD_F_SEM w c f 155 \/ 156(* OLD_F_SEM w c (F_BOOL b) *) 157 B_SEM (ELEM w 0) b 158 \/ 159 ?i :: (1 to LENGTH w). 160(* ?w'. OLD_F_SEM (RESTN w i) B_TRUE (F_BOOL(B_AND(c,b))) *) 161 ?w'. B_SEM (ELEM w i) (B_AND(c,b)) 162 /\ 163 OLD_F_SEM (CAT(SEL w (0,i-1),w')) c f) 164 /\ 165 (OLD_F_SEM w c (F_STRONG_CLOCK(f,c1)) = 166 ?i :: (0 to LENGTH w). 167 S_SEM (SEL w (0,i)) B_TRUE (S_CAT(S_REPEAT(S_BOOL(B_NOT c1)),S_BOOL c1)) 168 /\ 169 OLD_F_SEM (RESTN w i) c1 f)`; 170 171(****************************************************************************** 172* Derivation of "golden" form of clocked "SEM 1" semantics of Sugar formulas 173******************************************************************************) 174val OLD_F_SEM = 175 store_thm 176 ("OLD_F_SEM", 177 ``(OLD_F_SEM w c (F_BOOL b) = B_SEM (ELEM w 0) b) 178 /\ 179 (OLD_F_SEM w c (F_NOT f) = 180 ~(OLD_F_SEM w c f)) 181 /\ 182 (OLD_F_SEM w c (F_AND(f1,f2)) = 183 OLD_F_SEM w c f1 /\ OLD_F_SEM w c f2) 184 /\ 185 (OLD_F_SEM w c (F_NEXT f) = 186 ?i :: (1 to LENGTH w). 187 S_SEM (SEL w (1,i)) B_TRUE (S_CAT(S_REPEAT(S_BOOL(B_NOT c)),S_BOOL c)) 188 /\ 189 OLD_F_SEM (RESTN w i) c f) 190 /\ 191 (OLD_F_SEM w c (F_UNTIL(f1,f2)) = 192 ?k :: (0 to LENGTH w). 193 OLD_F_SEM (RESTN w k) B_TRUE (F_BOOL c) /\ 194 OLD_F_SEM (RESTN w k) c f2 /\ 195 !j :: (0 to k). 196 OLD_F_SEM (RESTN w j) B_TRUE (F_BOOL c) ==> OLD_F_SEM (RESTN w j) c f1) 197 /\ 198 (OLD_F_SEM w c (F_SUFFIX_IMP(r,f)) = 199 !i :: (0 to LENGTH w). 200 S_SEM (SEL w (0,i)) c r 201 ==> 202 ?j :: (i to LENGTH w). 203 S_SEM (SEL w (i,j)) B_TRUE (S_CAT(S_REPEAT(S_BOOL(B_NOT c)),S_BOOL c)) 204 /\ 205 OLD_F_SEM (RESTN w j) c f) 206 /\ 207 (OLD_F_SEM w c (F_STRONG_IMP(r1,r2)) = 208 !i :: (0 to LENGTH w). 209 S_SEM (SEL w (0,i)) c r1 210 ==> 211 ?j :: (i to LENGTH w). S_SEM (SEL w (i,j)) c r2) 212 /\ 213 (OLD_F_SEM w c (F_WEAK_IMP(r1,r2)) = 214 !i :: (0 to LENGTH w). 215 S_SEM (SEL w (0,i)) c r1 216 ==> 217 ((?j :: (i to LENGTH w). S_SEM (SEL w (i,j)) c r2) 218 \/ 219 (!j :: (i to LENGTH w). ?w'. S_SEM (SEL w (i,j) <> w') c r2))) 220 /\ 221 (OLD_F_SEM w c (F_ABORT (f,b)) = 222 OLD_F_SEM w c f 223 \/ 224 OLD_F_SEM w c (F_BOOL b) 225 \/ 226 ?i :: (1 to LENGTH w). 227 ?w'. OLD_F_SEM (RESTN w i) B_TRUE (F_BOOL(B_AND(c,b))) 228 /\ 229 OLD_F_SEM (CAT(SEL w (0,i-1),w')) c f) 230 /\ 231 (OLD_F_SEM w c (F_STRONG_CLOCK(f,c1)) = 232 ?i :: (0 to LENGTH w). 233 S_SEM (SEL w (0,i)) B_TRUE (S_CAT(S_REPEAT(S_BOOL(B_NOT c1)),S_BOOL c1)) 234 /\ 235 OLD_F_SEM (RESTN w i) c1 f)``, 236 RW_TAC arith_ss [OLD_F_SEM_def,ELEM_RESTN,B_SEM_def]); 237 238(****************************************************************************** 239* Clocked "SEM 1" semantics of Sugar formulas, partly unfolded 240* with additional |w|>0 for boolean formulas 241* (see commented out stuff) to avoid need for TFL hacks to prove termination. 242******************************************************************************) 243val F_SEM_def = 244 Define 245 `(F_SEM w c (F_BOOL b) = 246 LENGTH w > 0 /\ B_SEM (ELEM w 0) b) 247 /\ 248 (F_SEM w c (F_NOT f) = 249 ~(F_SEM w c f)) 250 /\ 251 (F_SEM w c (F_AND(f1,f2)) = 252 F_SEM w c f1 /\ F_SEM w c f2) 253 /\ 254 (F_SEM w c (F_NEXT f) = 255 ?i :: (1 to LENGTH w). 256 S_SEM (SEL w (1,i)) B_TRUE (S_CAT(S_REPEAT(S_BOOL(B_NOT c)),S_BOOL c)) 257 /\ 258 F_SEM (RESTN w i) c f) 259 /\ 260 (F_SEM w c (F_UNTIL(f1,f2)) = 261 ?k :: (0 to LENGTH w). 262(* F_SEM (RESTN w k) B_TRUE (F_BOOL c) /\ *) 263 B_SEM (ELEM w k) c /\ 264 F_SEM (RESTN w k) c f2 /\ 265 !j :: (0 to k). 266(* F_SEM (RESTN w j) B_TRUE (F_BOOL c) ==> F_SEM (RESTN w j) c f1) *) 267 B_SEM (ELEM w j) c ==> F_SEM (RESTN w j) c f1) 268 /\ 269 (F_SEM w c (F_SUFFIX_IMP(r,f)) = 270 !i :: (0 to LENGTH w). 271 S_SEM (SEL w (0,i)) c r 272 ==> 273 ?j :: (i to LENGTH w). 274 S_SEM (SEL w (i,j)) B_TRUE (S_CAT(S_REPEAT(S_BOOL(B_NOT c)),S_BOOL c)) 275 /\ 276 F_SEM (RESTN w j) c f) 277 /\ 278 (F_SEM w c (F_STRONG_IMP(r1,r2)) = 279 !i :: (0 to LENGTH w). 280 S_SEM (SEL w (0,i)) c r1 281 ==> 282 ?j :: (i to LENGTH w). S_SEM (SEL w (i,j)) c r2) 283 /\ 284 (F_SEM w c (F_WEAK_IMP(r1,r2)) = 285 !i :: (0 to LENGTH w). 286 S_SEM (SEL w (0,i)) c r1 287 ==> 288 ((?j :: (i to LENGTH w). S_SEM (SEL w (i,j)) c r2) 289 \/ 290 (!j :: (i to LENGTH w). ?w'. S_SEM (SEL w (i,j) <> w') c r2))) 291 /\ 292 (F_SEM w c (F_ABORT (f,b)) = 293 F_SEM w c f 294 \/ 295(* F_SEM w c (F_BOOL b) *) 296 LENGTH w > 0 /\ B_SEM (ELEM w 0) b 297 \/ 298 ?i :: (1 to LENGTH w). 299(* ?w'. F_SEM (RESTN w i) B_TRUE (F_BOOL(B_AND(c,b))) *) 300 ?w'. B_SEM (ELEM w i) (B_AND(c,b)) 301 /\ 302 F_SEM (CAT(SEL w (0,i-1),w')) c f) 303 /\ 304 (F_SEM w c (F_STRONG_CLOCK(f,c1)) = 305 ?i :: (0 to LENGTH w). 306 S_SEM (SEL w (0,i)) B_TRUE (S_CAT(S_REPEAT(S_BOOL(B_NOT c1)),S_BOOL c1)) 307 /\ 308 F_SEM (RESTN w i) c1 f)`; 309 310(****************************************************************************** 311* Derivation of "golden" form of clocked "SEM 1" semantics of Sugar formulas 312******************************************************************************) 313val F_SEM = 314 store_thm 315 ("F_SEM", 316 ``(F_SEM w c (F_BOOL b) = 317 LENGTH w > 0 /\ B_SEM (ELEM w 0) b) 318 /\ 319 (F_SEM w c (F_NOT f) = 320 ~(F_SEM w c f)) 321 /\ 322 (F_SEM w c (F_AND(f1,f2)) = 323 F_SEM w c f1 /\ F_SEM w c f2) 324 /\ 325 (F_SEM w c (F_NEXT f) = 326 ?i :: (1 to LENGTH w). 327 S_SEM (SEL w (1,i)) B_TRUE (S_CAT(S_REPEAT(S_BOOL(B_NOT c)),S_BOOL c)) 328 /\ 329 F_SEM (RESTN w i) c f) 330 /\ 331 (F_SEM w c (F_UNTIL(f1,f2)) = 332 ?k :: (0 to LENGTH w). 333 F_SEM (RESTN w k) B_TRUE (F_BOOL c) /\ 334 F_SEM (RESTN w k) c f2 /\ 335 !j :: (0 to k). 336 F_SEM (RESTN w j) B_TRUE (F_BOOL c) ==> F_SEM (RESTN w j) c f1) 337 /\ 338 (F_SEM w c (F_SUFFIX_IMP(r,f)) = 339 !i :: (0 to LENGTH w). 340 S_SEM (SEL w (0,i)) c r 341 ==> 342 ?j :: (i to LENGTH w). 343 S_SEM (SEL w (i,j)) B_TRUE (S_CAT(S_REPEAT(S_BOOL(B_NOT c)),S_BOOL c)) 344 /\ 345 F_SEM (RESTN w j) c f) 346 /\ 347 (F_SEM w c (F_STRONG_IMP(r1,r2)) = 348 !i :: (0 to LENGTH w). 349 S_SEM (SEL w (0,i)) c r1 350 ==> 351 ?j :: (i to LENGTH w). S_SEM (SEL w (i,j)) c r2) 352 /\ 353 (F_SEM w c (F_WEAK_IMP(r1,r2)) = 354 !i :: (0 to LENGTH w). 355 S_SEM (SEL w (0,i)) c r1 356 ==> 357 ((?j :: (i to LENGTH w). S_SEM (SEL w (i,j)) c r2) 358 \/ 359 (!j :: (i to LENGTH w). ?w'. S_SEM (SEL w (i,j) <> w') c r2))) 360 /\ 361 (F_SEM w c (F_ABORT (f,b)) = 362 F_SEM w c f 363 \/ 364 F_SEM w c (F_BOOL b) 365 \/ 366 ?i :: (1 to LENGTH w). 367 ?w'. F_SEM (RESTN w i) B_TRUE (F_BOOL(B_AND(c,b))) 368 /\ 369 F_SEM (CAT(SEL w (0,i-1),w')) c f) 370 /\ 371 (F_SEM w c (F_STRONG_CLOCK(f,c1)) = 372 ?i :: (0 to LENGTH w). 373 S_SEM (SEL w (0,i)) B_TRUE (S_CAT(S_REPEAT(S_BOOL(B_NOT c1)),S_BOOL c1)) 374 /\ 375 F_SEM (RESTN w i) c1 f)``, 376 RW_TAC arith_ss [F_SEM_def,ELEM_RESTN,B_SEM_def] 377 THEN Cases_on `w` 378 THEN RW_TAC (arith_ss ++ resq_SS) 379 [GT_xnum_num_def,num_to_def,xnum_to_def,RESTN_FINITE,LENGTH_def, 380 LENGTH_RESTN_INFINITE] 381 THEN EQ_TAC 382 THEN RW_TAC arith_ss [] 383 THEN RW_TAC arith_ss [] 384 THENL 385 [Q.EXISTS_TAC `k` 386 THEN RW_TAC arith_ss [FinitePSLPathTheory.LENGTH_RESTN], 387 Q.EXISTS_TAC `k` 388 THEN RW_TAC arith_ss [FinitePSLPathTheory.LENGTH_RESTN], 389 REPEAT DISJ2_TAC 390 THEN Q.EXISTS_TAC `i` 391 THEN RW_TAC arith_ss [FinitePSLPathTheory.LENGTH_RESTN] 392 THEN PROVE_TAC[], 393 REPEAT DISJ2_TAC 394 THEN Q.EXISTS_TAC `i` 395 THEN RW_TAC arith_ss [FinitePSLPathTheory.LENGTH_RESTN] 396 THEN PROVE_TAC[]]); 397 398val _ = export_theory(); 399