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