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