1(*****************************************************************************) 2(* Definitions from LRM B.3 "Syntactic sugaring" *) 3(*****************************************************************************) 4 5(*****************************************************************************) 6(* START BOILERPLATE *) 7(*****************************************************************************) 8 9(* 10quietdec := true; 11loadPath := "../official-semantics" :: !loadPath; 12map load ["intLib","stringLib","stringTheory","SyntaxTheory"]; 13open intLib stringLib stringTheory SyntaxTheory; 14val _ = intLib.deprecate_int(); 15quietdec := false; 16*) 17 18(****************************************************************************** 19* Boilerplate needed for compilation 20******************************************************************************) 21open HolKernel Parse boolLib bossLib; 22 23(****************************************************************************** 24* Open theories 25******************************************************************************) 26open intLib stringLib stringTheory SyntaxTheory; 27 28(****************************************************************************** 29* Set default parsing to natural numbers rather than integers 30******************************************************************************) 31val _ = intLib.deprecate_int(); 32 33(*****************************************************************************) 34(* END BOILERPLATE *) 35(*****************************************************************************) 36 37(****************************************************************************** 38* Start a new theory called SyntacticSugarTheory 39******************************************************************************) 40val _ = new_theory "SyntacticSugar"; 41 42(****************************************************************************** 43* Ensure term_of_int has correct type 44* (i.e. not int/1 -> term) 45******************************************************************************) 46val term_of_int = numLib.term_of_int; 47 48(****************************************************************************** 49* pureDefine doesn't export definitions to theCompset (for EVAL). 50******************************************************************************) 51val pureDefine = with_flag (computeLib.auto_import_definitions, false) Define; 52 53(****************************************************************************** 54* Additional boolean operators 55******************************************************************************) 56 57(****************************************************************************** 58* Definition of disjunction 59******************************************************************************) 60 61val B_OR_def = 62 pureDefine `B_OR(b1,b2) = B_NOT(B_AND(B_NOT b1, B_NOT b2))`; 63 64(****************************************************************************** 65* Definition of implication 66******************************************************************************) 67 68val B_IMP_def = 69 pureDefine `B_IMP(b1,b2) = B_OR(B_NOT b1, b2)`; 70 71(****************************************************************************** 72* Definition of logical equivalence 73******************************************************************************) 74 75val B_IFF_def = 76 pureDefine `B_IFF(b1,b2) = B_AND(B_IMP(b1, b2),B_IMP(b2, b1))`; 77 78(****************************************************************************** 79* Definition of truth 80******************************************************************************) 81 82val B_TRUE_def = 83 pureDefine `B_TRUE = B_OR(B_PROP ARB, B_NOT(B_PROP ARB))`; 84 85(****************************************************************************** 86* Definition of falsity 87******************************************************************************) 88 89val B_FALSE_def = 90 pureDefine `B_FALSE = B_NOT B_TRUE`; 91 92(****************************************************************************** 93* Additional SERE operators 94******************************************************************************) 95 96(****************************************************************************** 97* SERE versions of T and F 98******************************************************************************) 99 100val S_TRUE_def = Define `S_TRUE = S_BOOL B_TRUE` 101and S_FALSE_def = Define `S_FALSE = S_BOOL B_FALSE`; 102 103(****************************************************************************** 104* {r1} & {r2} = {{r1} && {r2;T[*]}} | {{r1;T[*]} && {r2}} 105******************************************************************************) 106val S_FLEX_AND_def = 107 Define 108 `S_FLEX_AND(r1,r2) = 109 S_OR 110 (S_AND(r1,S_CAT(r2, S_REPEAT S_TRUE)), 111 S_AND(S_CAT(r1,S_REPEAT S_TRUE), r2))`; 112 113(****************************************************************************** 114* | F[*] if i = 0 115* r[*i] = < 116* | r;r;...;r (i times) otherwise 117******************************************************************************) 118val S_REPEAT_ITER_def = 119 Define 120 `S_REPEAT_ITER r i = 121 if i=0 then S_REPEAT(S_BOOL B_FALSE) 122 else if i=1 then r else S_CAT(r, S_REPEAT_ITER r (i-1))`; 123 124(****************************************************************************** 125* RANGE_ITER(i, j) op f = (f i) op (f(i+1)) op ... op (f j) 126******************************************************************************) 127 128(****************************************************************************** 129* RANGE_ITER_AUX op f i n = (f i) op (f(i+1)) op ... op (f n) 130******************************************************************************) 131val RANGE_ITER_AUX_def = 132 Define 133 `(RANGE_ITER_AUX op f i 0 = f i) 134 /\ 135 (RANGE_ITER_AUX op f i (SUC n) = op(f i, RANGE_ITER_AUX op f (i+1) n))`; 136 137(****************************************************************************** 138* Prove if-then-else form needed by computeLib 139******************************************************************************) 140val RANGE_ITER_AUX = 141 prove 142 (``RANGE_ITER_AUX op f i n = 143 if n=0 then f i 144 else op(f i, RANGE_ITER_AUX op f (i+1) (n-1))``, 145 Cases_on `n` THEN RW_TAC arith_ss [RANGE_ITER_AUX_def]); 146 147val _ = computeLib.add_funs[RANGE_ITER_AUX]; 148 149val RANGE_ITER_def = 150 Define `RANGE_ITER(i, j) op f = RANGE_ITER_AUX op f i (j-i)`; 151 152(****************************************************************************** 153* S_RANGE_REPEAT(r, (i,j)) = r[*i..j] = {r[*i]} | {r[*(i+1)]} | ... | {r[*j]} 154******************************************************************************) 155val S_RANGE_REPEAT_def = 156 Define 157 `(S_RANGE_REPEAT(r, (i, SOME j)) = RANGE_ITER(i, j) S_OR (S_REPEAT_ITER r)) 158 /\ 159 (S_RANGE_REPEAT(r, (i, NONE)) = S_CAT(S_REPEAT_ITER r i, S_REPEAT r))`; 160 161(****************************************************************************** 162* r[+] = r;r[*] 163******************************************************************************) 164val S_NON_ZERO_REPEAT_def = 165 Define `S_NON_ZERO_REPEAT r = S_CAT(r, S_REPEAT r)`; 166 167(****************************************************************************** 168* b[=i] = {!b[*];b}[*i];!b[*] 169******************************************************************************) 170val S_EQ_REPEAT_ITER_def = 171 Define 172 `S_EQ_REPEAT_ITER b i = 173 S_CAT 174 (S_REPEAT_ITER (S_CAT(S_REPEAT(S_BOOL(B_NOT b)),S_BOOL b)) i, 175 S_REPEAT(S_BOOL(B_NOT b)))`; 176 177(****************************************************************************** 178* S_RANGE_EQ_REPEAT(b, (i,j)) = 179* b[=i..j] = {b[=i]} | {b[*=i+1)]} | ... | {b[=j]} 180******************************************************************************) 181val S_RANGE_EQ_REPEAT_def = 182 Define 183 `(S_RANGE_EQ_REPEAT(b, (i, SOME j)) = 184 RANGE_ITER(i, j) S_OR (S_EQ_REPEAT_ITER b)) 185 /\ 186 (S_RANGE_EQ_REPEAT(b, (i, NONE)) = 187 S_CAT(S_EQ_REPEAT_ITER b i, S_REPEAT S_TRUE))`; 188 189(****************************************************************************** 190* b[->i] = {!b[*];b}[*i] 191******************************************************************************) 192val S_GOTO_REPEAT_ITER_def = 193 Define 194 `S_GOTO_REPEAT_ITER b = 195 S_REPEAT_ITER (S_CAT(S_REPEAT(S_BOOL(B_NOT b)),S_BOOL b))`; 196 197(****************************************************************************** 198* S_RANGE_GOTO_REPEAT(b, (i,j)) = 199* b[=i..j] = {b[=i]} | {b[*=i+1)]} | ... | {b[=j]} 200******************************************************************************) 201val S_RANGE_GOTO_REPEAT_def = 202 Define 203 `(S_RANGE_GOTO_REPEAT(b, (i, SOME j)) = 204 RANGE_ITER(i, j) S_OR (S_GOTO_REPEAT_ITER b)) 205 /\ 206 (S_RANGE_GOTO_REPEAT(b, (i, NONE)) = S_GOTO_REPEAT_ITER b i)`; 207 208(****************************************************************************** 209* Formula disjunction: f1 \/ f2 210******************************************************************************) 211val F_OR_def = 212 Define 213 `F_OR(f1,f2) = F_NOT(F_AND(F_NOT f1, F_NOT f2))`; 214 215(****************************************************************************** 216* Formula implication: f1 --> f2 217******************************************************************************) 218val F_IMPLIES_def = 219 Define 220 `F_IMPLIES(f1,f2) = F_OR(F_NOT f1, f2)`; 221 222(****************************************************************************** 223* Formula implication: f1 --> f2 224* (alternative definition to match ML datatype) 225******************************************************************************) 226val F_IMP_def = 227 Define 228 `F_IMP = F_IMPLIES`; 229 230(****************************************************************************** 231* Formula equivalence: f1 <--> f2 232******************************************************************************) 233val F_IFF_def = 234 Define 235 `F_IFF(f1,f2) = F_AND(F_IMPLIES(f1, f2), F_IMPLIES(f2, f1))`; 236 237(****************************************************************************** 238* Weak next: X f 239******************************************************************************) 240val F_WEAK_X_def = 241 Define 242 `F_WEAK_X f = F_NOT(F_NEXT(F_NOT f))`; 243 244(****************************************************************************** 245* Eventually: F f 246******************************************************************************) 247val F_F_def = 248 Define 249 `F_F f = F_UNTIL(F_BOOL B_TRUE, f)`; 250 251(****************************************************************************** 252* Always: G f 253******************************************************************************) 254val F_G_def = 255 Define 256 `F_G f = F_NOT(F_F(F_NOT f))`; 257 258(****************************************************************************** 259* Weak until: [f1 W f2] 260******************************************************************************) 261val F_W_def = 262 Define 263 `F_W(f1,f2) = F_OR(F_UNTIL(f1,f2), F_G f1)`; 264 265(****************************************************************************** 266* always f 267******************************************************************************) 268val F_ALWAYS_def = 269 Define 270 `F_ALWAYS = F_G`; 271 272(****************************************************************************** 273* never f 274******************************************************************************) 275val F_NEVER_def = 276 Define 277 `F_NEVER f = F_G(F_NOT f)`; 278 279(****************************************************************************** 280* Strong next: next! f 281******************************************************************************) 282val F_STRONG_NEXT_def = 283 Define 284 `F_STRONG_NEXT f = F_NEXT f`; 285 286(****************************************************************************** 287* Weak next: next f 288******************************************************************************) 289val F_WEAK_NEXT_def = 290 Define 291 `F_WEAK_NEXT = F_WEAK_X`; 292 293(****************************************************************************** 294* eventually! f 295******************************************************************************) 296val F_STRONG_EVENTUALLY_def = 297 Define 298 `F_STRONG_EVENTUALLY = F_F`; 299 300(****************************************************************************** 301* f1 until! f2 302******************************************************************************) 303val F_STRONG_UNTIL_def = 304 Define 305 `F_STRONG_UNTIL = F_UNTIL`; 306 307(****************************************************************************** 308* f1 until f2 309******************************************************************************) 310val F_WEAK_UNTIL_def = 311 Define 312 `F_WEAK_UNTIL = F_W`; 313 314(****************************************************************************** 315* f1 until!_ f2 316******************************************************************************) 317val F_STRONG_UNTIL_INC_def = 318 Define 319 `F_STRONG_UNTIL_INC(f1,f2) = F_UNTIL(f1, F_AND(f1,f2))`; 320 321(****************************************************************************** 322* f1 until_ f2 323******************************************************************************) 324val F_WEAK_UNTIL_INC_def = 325 Define 326 `F_WEAK_UNTIL_INC(f1,f2) = F_W(f1, F_AND(f1,f2))`; 327 328(****************************************************************************** 329* f1 before! f2 330******************************************************************************) 331val F_STRONG_BEFORE_def = 332 Define 333 `F_STRONG_BEFORE(f1,f2) = F_UNTIL(F_NOT f2, F_AND(f1, F_NOT f2))`; 334 335(****************************************************************************** 336* f1 before f2 337******************************************************************************) 338val F_WEAK_BEFORE_def = 339 Define 340 `F_WEAK_BEFORE(f1,f2) = F_W(F_NOT f2, F_AND(f1, F_NOT f2))`; 341 342(****************************************************************************** 343* f1 before!_ f2 344******************************************************************************) 345val F_STRONG_BEFORE_INC_def = 346 Define 347 `F_STRONG_BEFORE_INC(f1,f2) = F_UNTIL(F_NOT f2, f1)`; 348 349(****************************************************************************** 350* f1 before_ f2 351******************************************************************************) 352val F_WEAK_BEFORE_INC_def = 353 Define 354 `F_WEAK_BEFORE_INC(f1,f2) = F_W(F_NOT f2, f1)`; 355 356(****************************************************************************** 357* | f if i = 0 358* X![i]f = < 359* | X! X! ... X! (i times) otherwise 360******************************************************************************) 361val F_NUM_STRONG_X_def = 362 Define 363 `F_NUM_STRONG_X(i,f) = FUNPOW F_NEXT i f`; 364 365(****************************************************************************** 366* | f if i = 0 367* X[i]f = < 368* | X X ... X (i times) otherwise 369* 370* Note double-negation redundancy: 371* EVAL ``F_NUM_WEAK_X(2,f)``; 372* > val it = 373* |- F_NUM_WEAK_X (2,f) = 374* F_NOT (F_NEXT (F_NOT (F_NOT (F_NEXT (F_NOT f))))) : thm 375* 376******************************************************************************) 377val F_NUM_WEAK_X_def = 378 Define 379 `F_NUM_WEAK_X(i,f) = FUNPOW F_WEAK_X i f`; 380 381(****************************************************************************** 382* next![i] f = X! [i] f 383******************************************************************************) 384val F_NUM_STRONG_NEXT_def = 385 Define 386 `F_NUM_STRONG_NEXT = F_NUM_STRONG_X`; 387 388(****************************************************************************** 389* next[i] f = X [i] f 390******************************************************************************) 391val F_NUM_WEAK_NEXT_def = 392 Define 393 `F_NUM_WEAK_NEXT = F_NUM_WEAK_X`; 394 395(****************************************************************************** 396* next_a![i..j]f = X![i]f /\ ... /\ X![j]f 397******************************************************************************) 398val F_NUM_STRONG_NEXT_A_def = 399 Define 400 `F_NUM_STRONG_NEXT_A((i, SOME j),f) = 401 RANGE_ITER (i,j) $F_AND (\n. F_NUM_STRONG_X(n,f))`; 402 403(****************************************************************************** 404* next_a[i..j]f = X[i]f /\ ... /\ X[j]f 405******************************************************************************) 406val F_NUM_WEAK_NEXT_A_def = 407 Define 408 `F_NUM_WEAK_NEXT_A((i, SOME j),f) = 409 RANGE_ITER (i,j) $F_AND (\n. F_NUM_WEAK_X(n,f))`; 410 411(****************************************************************************** 412* next_e![i..j]f = X![i]f \/ ... \/ X![j]f 413******************************************************************************) 414val F_NUM_STRONG_NEXT_E_def = 415 Define 416 `F_NUM_STRONG_NEXT_E((i, SOME j),f) = 417 RANGE_ITER (i,j) $F_OR (\n. F_NUM_STRONG_X(n,f))`; 418 419(****************************************************************************** 420* next_e[i..j]f = X[i]f \/ ... \/ X[j]f 421******************************************************************************) 422val F_NUM_WEAK_NEXT_E_def = 423 Define 424 `F_NUM_WEAK_NEXT_E((i, SOME j),f) = 425 RANGE_ITER (i,j) $F_OR (\n. F_NUM_WEAK_X(n,f))`; 426 427(****************************************************************************** 428* next_event!(b)(f) = [!b U (b & f)] 429******************************************************************************) 430val F_STRONG_NEXT_EVENT_def = 431 Define 432 `F_STRONG_NEXT_EVENT(b,f) = 433 F_UNTIL(F_BOOL(B_NOT b), F_AND(F_BOOL b, f))`; 434 435(****************************************************************************** 436* next_event(b)(f) = [!b W (b & f)] 437******************************************************************************) 438val F_WEAK_NEXT_EVENT_def = 439 Define 440 `F_WEAK_NEXT_EVENT(b,f) = 441 F_W(F_BOOL(B_NOT b), F_AND(F_BOOL b, f))`; 442 443(****************************************************************************** 444* next_event!(b)[k](f) = next_event! 445* (b) 446* (X! next_event!(b) ... (X! next_event!(b)(f)) ... ) 447* |---------------- k-1 times ----------------| 448******************************************************************************) 449val F_NUM_STRONG_NEXT_EVENT_def = 450 Define 451 `F_NUM_STRONG_NEXT_EVENT(b,k,f) = 452 F_STRONG_NEXT_EVENT 453 (b, FUNPOW (\f. F_NEXT(F_STRONG_NEXT_EVENT(b,f))) (k-1) f)`; 454 455(****************************************************************************** 456* next_event(b)[k](f) = next_event 457* (b) 458* (X next_event(b) ... (X next_event(b)(f)) ... ) 459* |-------------- k-1 times --------------| 460******************************************************************************) 461val F_NUM_WEAK_NEXT_EVENT_def = 462 Define 463 `F_NUM_WEAK_NEXT_EVENT(b,k,f) = 464 F_WEAK_NEXT_EVENT 465 (b, FUNPOW (\f. F_NEXT(F_WEAK_NEXT_EVENT(b,f))) (k-1) f)`; 466 467(****************************************************************************** 468* next_event_a!(b)[k..l](f) = 469* next_event! (b) [k] (f) /\ ... /\ next_event! (b) [l] (f) 470******************************************************************************) 471val F_NUM_STRONG_NEXT_EVENT_A_def = 472 Define 473 `F_NUM_STRONG_NEXT_EVENT_A(b,(k,SOME l),f) = 474 RANGE_ITER (k,l) $F_AND (\n. F_NUM_STRONG_NEXT_EVENT(b,n,f))`; 475 476(****************************************************************************** 477* next_event_a(b)[k..l](f) = 478* next_event (b) [k] (f) /\ ... /\ next_event (b) [l] (f) 479******************************************************************************) 480val F_NUM_WEAK_NEXT_EVENT_A_def = 481 Define 482 `F_NUM_WEAK_NEXT_EVENT_A(b,(k,SOME l),f) = 483 RANGE_ITER (k,l) $F_AND (\n. F_NUM_WEAK_NEXT_EVENT(b,n,f))`; 484 485(****************************************************************************** 486* next_event_e!(b)[k..l](f) = 487* next_event! (b) [k] (f) \/ ... \/ next_event! (b) [l] (f) 488******************************************************************************) 489val F_NUM_STRONG_NEXT_EVENT_E_def = 490 Define 491 `F_NUM_STRONG_NEXT_EVENT_E(b,(k,SOME l),f) = 492 RANGE_ITER (k,l) $F_OR (\n. F_NUM_STRONG_NEXT_EVENT(b,n,f))`; 493 494(****************************************************************************** 495* next_event_a(b)[k..l](f) = 496* next_event (b) [k] (f) \/ ... \/ next_event (b) [l] (f) 497******************************************************************************) 498val F_NUM_WEAK_NEXT_EVENT_E_def = 499 Define 500 `F_NUM_WEAK_NEXT_EVENT_E(b,(k,SOME l),f) = 501 RANGE_ITER (k,l) $F_OR (\n. F_NUM_WEAK_NEXT_EVENT(b,n,f))`; 502 503(****************************************************************************** 504* {r1} |=> {r2}! = {r1} |-> {T;r2}! 505******************************************************************************) 506val F_SKIP_STRONG_IMP_def = 507 Define 508 `F_SKIP_STRONG_IMP(r1,r2) = F_STRONG_IMP(r1, S_CAT(S_TRUE, r2))`; 509 510(****************************************************************************** 511* {r1} |=> {r2} = {r1} |-> {T;r2} 512******************************************************************************) 513val F_SKIP_WEAK_IMP_def = 514 Define 515 `F_SKIP_WEAK_IMP(r1,r2) = F_WEAK_IMP(r1, S_CAT(S_TRUE, r2))`; 516 517(****************************************************************************** 518* always{r} = {T[*]} |-> {r} 519******************************************************************************) 520val F_SERE_ALWAYS_def = 521 Define 522 `F_SERE_ALWAYS r = F_WEAK_IMP(S_REPEAT S_TRUE, r)`; 523 524(****************************************************************************** 525* never{r} = {T[*];r} |-> {F} 526******************************************************************************) 527val F_SERE_NEVER_def = 528 Define 529 `F_SERE_NEVER r = F_WEAK_IMP(S_CAT(S_REPEAT S_TRUE, r), S_FALSE) `; 530 531(****************************************************************************** 532* eventually! {r} = {T} |-> {T[*];r}! 533******************************************************************************) 534val F_SERE_STRONG_EVENTUALLY_def = 535 Define 536 `F_SERE_STRONG_EVENTUALLY r = 537 F_STRONG_IMP(S_TRUE, S_CAT(S_REPEAT S_TRUE, r))`; 538 539(****************************************************************************** 540* within!(r1,b){r2} = {r1} |-> {r2&&b[=0];b}! 541******************************************************************************) 542val F_STRONG_WITHIN_def = 543 Define 544 `F_STRONG_WITHIN (r1,b,r2) = 545 F_STRONG_IMP(r1, S_CAT(S_AND(r2, S_EQ_REPEAT_ITER b 0), S_BOOL b))`; 546 547(****************************************************************************** 548* within(r1,b){r2} = {r1} |-> {r2&&b[=0];b} 549******************************************************************************) 550val F_WEAK_WITHIN_def = 551 Define 552 `F_WEAK_WITHIN (r1,b,r2) = 553 F_WEAK_IMP(r1, S_CAT(S_AND(r2, S_EQ_REPEAT_ITER b 0), S_BOOL b))`; 554 555(****************************************************************************** 556* within!_(r1,b){r2} = {r1} |-> {r2&&{b[=0];b}}! 557******************************************************************************) 558val F_STRONG_WITHIN_INC_def = 559 Define 560 `F_STRONG_WITHIN_INC (r1,b,r2) = 561 F_STRONG_IMP(r1, S_AND(r2, S_CAT(S_EQ_REPEAT_ITER b 0, S_BOOL b)))`; 562 563(****************************************************************************** 564* within_(r1,b){r2} = {r1} |-> {r2&&{b[=0];b}} 565******************************************************************************) 566val F_WEAK_WITHIN_INC_def = 567 Define 568 `F_WEAK_WITHIN_INC (r1,b,r2) = 569 F_WEAK_IMP(r1, S_AND(r2, S_CAT(S_EQ_REPEAT_ITER b 0, S_BOOL b)))`; 570 571(****************************************************************************** 572* within(r1,b){r2} = {r1} |-> {r2&&b[=0];b} 573******************************************************************************) 574val F_WEAK_WITHIN_def = 575 Define 576 `F_WEAK_WITHIN (r1,b,r2) = 577 F_WEAK_IMP(r1, S_CAT(S_AND(r2, S_EQ_REPEAT_ITER b 0), S_BOOL b))`; 578 579(****************************************************************************** 580* whilenot!(b){r} = within!(T,b){r} 581******************************************************************************) 582val F_STRONG_WHILENOT_def = 583 Define 584 `F_STRONG_WHILENOT (b,r) = F_STRONG_WITHIN(S_TRUE,b,r)`; 585 586(****************************************************************************** 587* whilenot(b){r} = within(T,b){r} 588******************************************************************************) 589val F_WEAK_WHILENOT_def = 590 Define 591 `F_WEAK_WHILENOT (b,r) = F_WEAK_WITHIN(S_TRUE,b,r)`; 592 593(****************************************************************************** 594* whilenot!_(b){r} = within!_(T,b){r} 595******************************************************************************) 596val F_STRONG_WHILENOT_INC_def = 597 Define 598 `F_STRONG_WHILENOT_INC (b,r) = F_STRONG_WITHIN_INC(S_TRUE,b,r)`; 599 600(****************************************************************************** 601* whilenot_(b){r} = within_(T,b){r} 602******************************************************************************) 603val F_WEAK_WHILENOT_INC_def = 604 Define 605 `F_WEAK_WHILENOT_INC (b,r) = F_WEAK_WITHIN_INC(S_TRUE,b,r)`; 606 607(****************************************************************************** 608* Define weak clocking: f@clk = !(!f)@clk) 609******************************************************************************) 610val F_WEAK_CLOCK_def = 611 Define 612 `F_WEAK_CLOCK(f,clk) = F_NOT(F_STRONG_CLOCK(F_NOT f, clk))`; 613 614val _ = export_theory(); 615