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