Temporal_LogicScript.sml
1(*
2 app load ["tautLib", "numLib", "pairLib", "schneiderUtils"];
3*)
4Theory Temporal_Logic
5Ancestors
6 num prim_rec arithmetic pair
7Libs
8 numLib pairLib Rsyntax schneiderUtils tautLib
9
10
11val _ = ParseExtras.temp_loose_equality()
12
13fun TAC_PROOF(g,t) = Tactical.TAC_PROOF(g,t) handle e => Raise e;
14
15val _ = Rewrite.add_implicit_rewrites pairLib.pair_rws;
16
17
18
19(* ************************************************************ *)
20(* Definitions via Hardware-Formulae *)
21(* ************************************************************ *)
22
23
24val NEXT = new_definition("NEXT", “NEXT P = \t. P(SUC t):bool”);
25
26val ALWAYS = new_definition("ALWAYS", “ALWAYS P t0 = !t:num.P(t+t0)”);
27
28val EVENTUAL = new_definition("EVENTUAL", “EVENTUAL P t0 = ?t:num.P(t+t0)”);
29
30val WATCH = new_infixr_definition("WATCH",
31 “$WATCH q b t0 =
32 !t. (q t0 = F) /\ (q (SUC (t+t0)) = (q (t+t0) \/ b (t+t0)))”,200);
33
34val UPTO = new_definition("UPTO",
35 “UPTO(t0,t1,a) =
36 !t2. t0<=t2 /\ t2<t1 ==> a t2”);
37
38val WHEN = new_infixr_definition("WHEN",
39 “$WHEN a b t0 =
40 ?q. (q WATCH b) t0
41 /\ !t.(q(t+t0) \/ (b(t+t0) ==> a(t+t0)))”,200);
42
43val UNTIL = new_infixr_definition("UNTIL",
44 “$UNTIL a b t0 =
45 ?q. (q WATCH b) t0
46 /\ !t.(q (t+t0) \/ b(t+t0) \/ a(t+t0)) ”,200);
47
48val BEFORE = new_infixr_definition("BEFORE",
49 “$BEFORE a b t0 =
50 ?q. (q WATCH b) t0
51 /\ ((?t.~q(t+t0) /\ ~b(t+t0) /\ a(t+t0))
52 \/ !t.~b(t+t0)) ”,200);
53
54val SWHEN = new_infixr_definition("SWHEN",
55 “$SWHEN a b t0 =
56 ?q. (q WATCH b) t0
57 /\ ?t.~q(t+t0) /\ b(t+t0) /\ a(t+t0)”,200);
58
59val SUNTIL = new_infixr_definition("SUNTIL",
60 “$SUNTIL a b t0 =
61 ?q. (q WATCH b) t0
62 /\ (!t.q (t+t0) \/ b(t+t0) \/ a(t+t0))
63 /\ (?t. b(t+t0))”,200);
64
65val SBEFORE = new_infixr_definition("SBEFORE",
66 “$SBEFORE a b t0 =
67 ?q. (q WATCH b) t0
68 /\ (?t.~q(t+t0) /\ ~b(t+t0) /\ a(t+t0))”,200);
69
70
71(* %%%%%% use "lemmata.sml"; %%%%%%%%%% *)
72
73(* ************************************************************ *)
74(* General Lemmata *)
75(* ************************************************************ *)
76
77val WATCH_EXISTS = TAC_PROOF(([],“!b.!t0.?q. (q WATCH b) t0”),
78 let val lem1 = INST_TYPE[alpha |-> bool] num_Axiom_old
79 val lem2 = SPECL [“F”,“\z t. z \/ b(t:num)”] lem1
80 val lem3 = EXISTENCE (BETA_RULE lem2)
81 val lem4 = BETA_RULE(SPEC “\t.b(t+t0):bool” (GEN “b:num->bool” lem3))
82 in PURE_REWRITE_TAC[WATCH] THEN REPEAT GEN_TAC
83 THEN ASSUME_TAC lem4 THEN LEFT_EXISTS_TAC
84 THEN EXISTS_TAC “\t.fn1(t-t0):bool”
85 THEN BETA_TAC THEN REWRITE_TAC[]
86 THEN ASM_REWRITE_TAC[SYM(SPEC_ALL(CONJUNCT2 ADD)),SUB_EQUAL_0,ADD_SUB]
87 end)
88
89
90
91val WELL_ORDER = TAC_PROOF(
92 ([],“(?n.P n) = (?m.P m /\ !n. n<m ==> ~P n)”),
93 EQ_TAC THENL[REWRITE_TAC[WOP],
94 STRIP_TAC THEN EXISTS_TAC “m:num”
95 THEN ASM_REWRITE_TAC[]])
96
97
98val WELL_ORDER_UNIQUE = TAC_PROOF(
99 ([],“!m2 m1 P.
100 (P m1 /\ !n. n<m1 ==> ~P n) /\
101 (P m2 /\ !n. n<m2 ==> ~P n) ==> (m1 = m2)”),
102 REPEAT GEN_TAC THEN STRIP_TAC
103 THEN DISJ_CASES_TAC(SPECL[“m1:num”,“m2:num”]LESS_LESS_CASES)
104 THENL[ASM_REWRITE_TAC[],POP_ASSUM DISJ_CASES_TAC THEN RES_TAC])
105
106
107
108Theorem DELTA_CASES:
109 (?d. (!t. t<d ==> ~b(t+t0)) /\ b(d+t0)) \/ !d. ~b(d+t0)
110Proof
111 SUBST1_TAC (SYM(NOT_EXISTS_CONV “~?d.b(d+t0)”))
112 THEN ONCE_REWRITE_TAC[BETA_RULE(SPEC “\t.b(t+t0):bool” (GEN_ALL WELL_ORDER))]
113 THEN RIGHT_DISJ_TAC
114 THEN ONCE_REWRITE_TAC[CONJ_COMM]
115 THEN ASM_REWRITE_TAC[]
116QED
117
118
119
120(* ************************************************************ *)
121(* Implicational Forms *)
122(* ************************************************************ *)
123
124val WHEN_IMP = TAC_PROOF(
125 ([],“(a WHEN b) t0 = !q. (q WATCH b) t0 ==>
126 !t.(q(t+t0) \/ (b(t+t0) ==> a(t+t0)))”),
127 REWRITE_TAC[WHEN,WATCH] THEN EQ_TAC THEN REPEAT STRIP_TAC
128 THENL[MY_MP_TAC “!t. q'(t+t0):bool = q(t+t0)”
129 THENL[INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES],
130 DISCH_TAC THEN ASM_REWRITE_TAC[]],
131 ASSUME_TAC(SPEC_ALL WATCH_EXISTS)
132 THEN LEFT_EXISTS_TAC
133 THEN RULE_ASSUM_TAC(REWRITE_RULE[WATCH])
134 THEN EXISTS_TAC“q:num->bool”
135 THEN LEFT_NO_FORALL_TAC 1 “q:num->bool”
136 THEN ASM_REWRITE_TAC[] THEN RES_TAC])
137
138
139val UNTIL_IMP = TAC_PROOF(
140 ([],“(a UNTIL b) t0 = !q. (q WATCH b) t0 ==>
141 !t.(q(t+t0) \/ b(t+t0) \/ a(t+t0))”),
142 REWRITE_TAC[UNTIL,WATCH] THEN EQ_TAC THEN REPEAT STRIP_TAC
143 THENL[MY_MP_TAC “!t. q'(t+t0):bool = q(t+t0)”
144 THENL[INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES],
145 DISCH_TAC THEN ASM_REWRITE_TAC[]],
146 ASSUME_TAC(SPEC_ALL WATCH_EXISTS)
147 THEN LEFT_EXISTS_TAC
148 THEN RULE_ASSUM_TAC(REWRITE_RULE[WATCH])
149 THEN EXISTS_TAC“q:num->bool”
150 THEN LEFT_NO_FORALL_TAC 1 “q:num->bool”
151 THEN ASM_REWRITE_TAC[] THEN RES_TAC])
152
153
154
155val BEFORE_IMP = TAC_PROOF(
156 ([],“(a BEFORE b) t0 =
157 !q. (q WATCH b) t0 ==>
158 ((?t.~q(t+t0)/\~b(t+t0)/\a(t+t0)) \/ (!t.~b(t+t0)))”),
159 REWRITE_TAC[BEFORE,WATCH] THEN EQ_TAC THEN REPEAT STRIP_TAC
160 THENL[
161 MY_MP_TAC “!t. q'(t+t0):bool = q(t+t0)”
162 THENL[
163 INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES],
164 DISCH_TAC THEN ASM_REWRITE_TAC[]]
165 THEN DISJ1_TAC THEN EXISTS_TAC “t:num”
166 THEN ASM_REWRITE_TAC[],
167 ASM_REWRITE_TAC[],
168 ASSUME_TAC(SPEC_ALL WATCH_EXISTS)
169 THEN LEFT_EXISTS_TAC
170 THEN RULE_ASSUM_TAC(REWRITE_RULE[WATCH])
171 THEN EXISTS_TAC“q:num->bool”
172 THEN LEFT_NO_FORALL_TAC 1 “q:num->bool”
173 THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[]])
174
175
176
177val SWHEN_IMP = TAC_PROOF(
178 ([],“(a SWHEN b) t0 =
179 !q. (q WATCH b) t0 ==>
180 ?t.~q(t+t0) /\ b(t+t0) /\ a(t+t0)”),
181 REWRITE_TAC[SWHEN,WATCH] THEN EQ_TAC THEN REPEAT STRIP_TAC
182 THENL[
183 MY_MP_TAC “!t. q'(t+t0):bool = q(t+t0)”
184 THENL[
185 INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES],
186 DISCH_TAC]
187 THEN EXISTS_TAC“t:num” THEN ASM_REWRITE_TAC[],
188 ASSUME_TAC(SPEC_ALL WATCH_EXISTS)
189 THEN LEFT_EXISTS_TAC
190 THEN RULE_ASSUM_TAC(REWRITE_RULE[WATCH])
191 THEN EXISTS_TAC“q:num->bool”
192 THEN LEFT_NO_FORALL_TAC 1 “q:num->bool”
193 THEN RES_TAC THEN ASM_REWRITE_TAC[]
194 THEN EXISTS_TAC“t:num” THEN ASM_REWRITE_TAC[]])
195
196
197val SUNTIL_IMP = TAC_PROOF(
198 ([],“(a SUNTIL b) t0 =
199 !q. (q WATCH b) t0 ==>
200 (!t.q(t+t0) \/ b(t+t0) \/ a(t+t0))
201 /\ ?t. b(t+t0)”),
202 REWRITE_TAC[SUNTIL,WATCH] THEN BETA_TAC
203 THEN EQ_TAC THEN REPEAT STRIP_TAC THEN RES_TAC
204 THEN ASM_REWRITE_TAC[]
205 THENL[
206 MY_MP_TAC “!t. q'(t+t0):bool = q(t+t0)”
207 THENL[
208 INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES],
209 DISCH_TAC THEN ASM_REWRITE_TAC[]],
210 EXISTS_TAC“t:num” THEN ASM_REWRITE_TAC[],
211 ASSUME_TAC(SPEC_ALL WATCH_EXISTS)
212 THEN LEFT_EXISTS_TAC
213 THEN RULE_ASSUM_TAC(REWRITE_RULE[WATCH])
214 THEN EXISTS_TAC“q:num->bool”
215 THEN LEFT_NO_FORALL_TAC 1 “q:num->bool”
216 THEN RES_TAC THEN ASM_REWRITE_TAC[]
217 THEN EXISTS_TAC“t:num” THEN ASM_REWRITE_TAC[]])
218
219
220val SBEFORE_IMP = TAC_PROOF(
221 ([],“(a SBEFORE b) t0 =
222 !q. (q WATCH b) t0 ==>
223 (?t.~q(t+t0)/\~b(t+t0)/\a(t+t0))”),
224 REWRITE_TAC[SBEFORE,WATCH] THEN BETA_TAC
225 THEN EQ_TAC THEN REPEAT STRIP_TAC THEN RES_TAC
226 THEN ASM_REWRITE_TAC[]
227 THENL[
228 MY_MP_TAC “!t. q'(t+t0):bool = q(t+t0)”
229 THENL[
230 INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES],
231 DISCH_TAC]
232 THEN EXISTS_TAC “t:num” THEN ASM_REWRITE_TAC[],
233 ASSUME_TAC(SPEC_ALL WATCH_EXISTS)
234 THEN LEFT_EXISTS_TAC
235 THEN RULE_ASSUM_TAC(REWRITE_RULE[WATCH])
236 THEN EXISTS_TAC“q:num->bool”
237 THEN LEFT_NO_FORALL_TAC 1 “q:num->bool”
238 THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[]]);
239
240
241
242(* ************************************************************ *)
243(* Signal Theorems *)
244(* ************************************************************ *)
245
246
247val ALWAYS_SIGNAL = TAC_PROOF(
248 ([],“ALWAYS a t0 = (!t. a(t+t0))”),
249 REWRITE_TAC[ALWAYS])
250
251
252val EVENTUAL_SIGNAL = TAC_PROOF(
253 ([],“EVENTUAL a t0 = (?t. a(t+t0))”),
254 REWRITE_TAC[EVENTUAL])
255
256
257
258
259Theorem WATCH_SIGNAL:
260 (q WATCH b) t0 <=>
261 ((!t. ~b(t+t0)) ==> (!t. ~q(t+t0))) /\
262 (!d. b(d+t0) /\ (!t. t<d ==> ~b(t+t0)) ==>
263 (!t. t<=d ==> ~q(t+t0)) /\ (!t. q(SUC(t+(d+t0)))))
264Proof
265 PURE_REWRITE_TAC[WATCH]
266 THEN RIGHT_LEMMA_DISJ_CASES_TAC DELTA_CASES THEN ASM_REWRITE_TAC[]
267 THENL[ALL_TAC,
268 EQ_TAC THEN DISCH_TAC
269 THENL[
270 INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES],
271 ASM_REWRITE_TAC[] THEN GEN_TAC THEN CONJ_TAC
272 THENL[LEFT_FORALL_TAC “0”,LEFT_FORALL_TAC “SUC t”]
273 THEN UNDISCH_HD_TAC THEN REWRITE_TAC[ADD_CLAUSES]]]
274 THEN EQ_TAC THEN STRIP_TAC
275 THENL[
276 GEN_TAC THEN STRIP_TAC THEN LEFT_CONJ_TAC
277 THENL[
278 INDUCT_TAC THEN ASM_REWRITE_TAC[ZERO_LESS_EQ,ADD_CLAUSES]
279 THEN DISCH_TAC THEN IMP_RES_TAC OR_LESS
280 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ
281 THEN RES_TAC THEN ASM_REWRITE_TAC[],
282 INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES]
283 THEN SUBST1_TAC(EQT_ELIM(ARITH_CONV“SUC(t+(d'+t0))=SUC(t+d')+t0”))
284 THEN ASM_REWRITE_TAC[ADD_CLAUSES,SYM(SPEC_ALL ADD_ASSOC)]],
285 ALL_TAC]
286 THEN RES_TAC THEN POP_NO_TAC 2 THEN POP_NO_TAC 2
287 THEN GEN_TAC THEN CONJ_TAC
288 THENL[LEFT_NO_FORALL_TAC 1 “0” THEN UNDISCH_HD_TAC
289 THEN REWRITE_TAC[ADD_CLAUSES,ZERO_LESS_EQ],
290 ALL_TAC]
291 THEN DISJ_CASES_TAC (SPECL[“d:num”,“t:num”]LESS_LESS_CASES)
292 THENL[POP_ASSUM(SUBST1_TAC o SYM) THEN LEFT_FORALL_TAC “0”
293 THEN RULE_ASSUM_TAC(REWRITE_RULE[ADD_CLAUSES])
294 THEN ASM_REWRITE_TAC[],
295 ALL_TAC]
296 THEN POP_ASSUM DISJ_CASES_TAC
297 THENL[IMP_RES_TAC LESS_ADD_1 THEN POP_ASSUM SUBST1_TAC
298 THEN SUBST1_TAC(EQT_ELIM(ARITH_CONV“(d+(p+1))+t0=SUC(p+(d+t0))”))
299 THEN ASM_REWRITE_TAC[]
300 THEN LEFT_NO_FORALL_TAC 1 “SUC p” THEN UNDISCH_HD_TAC
301 THEN REWRITE_TAC[ADD_CLAUSES],
302 IMP_RES_TAC LESS_IMP_LESS_OR_EQ THEN IMP_RES_TAC LESS_OR
303 THEN RES_TAC THEN UNDISCH_NO_TAC 2
304 THEN ASM_REWRITE_TAC[ADD_CLAUSES]]
305QED
306
307
308
309val WHEN_SIGNAL = prove(
310 “(a WHEN b) t0 =
311 !delta.((!t. t<delta ==> ~b(t+t0)) /\ b(delta+t0) ==> a(delta+t0))”,
312 PURE_REWRITE_TAC[WHEN,WATCH_SIGNAL]
313 >> RIGHT_LEMMA_DISJ_CASES_TAC DELTA_CASES >> ASM_REWRITE_TAC[]
314 THENL[ALL_TAC, EXISTS_TAC“\t:num.F” >> BETA_TAC >> REWRITE_TAC[]]
315 >> EQ_TAC >> STRIP_TAC
316 THENL[
317 GEN_TAC >> LEFT_NO_FORALL_TAC 1 “delta:num”
318 >> STRIP_TAC >> RES_TAC
319 >> LEFT_NO_FORALL_TAC 5 “delta:num”
320 >> LEFT_NO_FORALL_TAC 2 “delta:num”
321 >> RULE_ASSUM_TAC (REWRITE_RULE[LESS_EQ_REFL])
322 >> POP_ASSUM (fn x=> RULE_ASSUM_TAC (REWRITE_RULE[x]))
323 >> UNDISCH_HD_TAC >> ASM_REWRITE_TAC[],
324 ASSUME_TAC (SPEC_ALL(REWRITE_RULE[WATCH_SIGNAL]WATCH_EXISTS))
325 >> LEFT_EXISTS_TAC >> EXISTS_TAC “q:num->bool”
326 >> UNDISCH_HD_TAC >> ASM_REWRITE_TAC[] >> STRIP_TAC
327 >> ASM_REWRITE_TAC[]
328 >> LEFT_FORALL_TAC “d:num” >> RES_TAC >> POP_NO_TAC 3
329 >> POP_NO_TAC 3
330 >> GEN_TAC >> DISJ_CASES_TAC (SPECL[“t:num”,“d:num”]LESS_LESS_CASES)
331 THENL[POP_ASSUM SUBST1_TAC >> ASM_REWRITE_TAC[],
332 POP_ASSUM DISJ_CASES_TAC]
333 THENL[IMP_RES_TAC LESS_IMP_LESS_OR_EQ,
334 IMP_RES_TAC LESS_ADD_1 >> POP_ASSUM SUBST1_TAC
335 >> SUBST1_TAC(EQT_ELIM(ARITH_CONV“(d+(p+1))+t0 = (SUC(p+(d+t0)))”))]
336 >> RES_TAC >> ASM_REWRITE_TAC[]])
337
338
339
340
341val UNTIL_SIGNAL = TAC_PROOF(
342 ([],“(a UNTIL b) t0 =
343 (((!t. ~b(t+t0)) ==> (!t. a(t+t0))) /\
344 (!d. (!t.t<d ==> ~b(t+t0)) /\ b(d+t0) ==> (!t. t<d ==> a(t+t0))))”),
345 PURE_REWRITE_TAC[UNTIL,WATCH_SIGNAL,ALWAYS]
346 >> RIGHT_LEMMA_DISJ_CASES_TAC DELTA_CASES >> ASM_REWRITE_TAC[]
347 THENL[ALL_TAC,
348 EQ_TAC >> STRIP_TAC
349 THENL[UNDISCH_HD_TAC >> ASM_REWRITE_TAC[],
350 EXISTS_TAC “\t:num.F” >> BETA_TAC
351 >> ASM_REWRITE_TAC[]]]
352 >> EQ_TAC >> STRIP_TAC
353 THENL[
354 GEN_TAC >> STRIP_TAC
355 >> LEFT_NO_FORALL_TAC 3 “d':num” >> RES_TAC
356 >> POP_NO_TAC 2
357 >> GEN_TAC >> DISCH_TAC
358 >> IMP_RES_TAC LESS_IMP_LESS_OR_EQ >> RES_TAC
359 >> LEFT_NO_FORALL_TAC 8 “t:num”
360 >> UNDISCH_HD_TAC >> ASM_REWRITE_TAC[],
361 ASSUME_TAC (SPEC_ALL(REWRITE_RULE[WATCH_SIGNAL]WATCH_EXISTS))
362 >> LEFT_EXISTS_TAC >> EXISTS_TAC “q:num->bool”
363 >> UNDISCH_HD_TAC >> ASM_REWRITE_TAC[] >> STRIP_TAC
364 >> ASM_REWRITE_TAC[]
365 >> LEFT_FORALL_TAC “d:num” >> RES_TAC >> POP_NO_TAC 3 >> POP_NO_TAC 3
366 >> GEN_TAC >> DISJ_CASES_TAC (SPECL[“t:num”,“d:num”]LESS_LESS_CASES)
367 THENL[POP_ASSUM SUBST1_TAC >> ASM_REWRITE_TAC[],POP_ASSUM DISJ_CASES_TAC]
368 THENL[IMP_RES_TAC LESS_IMP_LESS_OR_EQ,
369 IMP_RES_TAC LESS_ADD_1 >> POP_ASSUM SUBST1_TAC
370 >> SUBST1_TAC(EQT_ELIM(ARITH_CONV“(d+(p+1))+t0 = (SUC(p+(d+t0)))”))]
371 >> RES_TAC >> ASM_REWRITE_TAC[]])
372
373
374
375val BEFORE_SIGNAL = TAC_PROOF(
376 ([],“(a BEFORE b) t0
377 = !delta.
378 ((!t. t<delta ==> ~b(t+t0)) /\ b(delta+t0))
379 ==> ?t. t<delta /\ a(t+t0)”),
380 REWRITE_TAC[BEFORE,WATCH] THEN EQ_TAC THEN REPEAT STRIP_TAC
381 THENL[
382 EXISTS_TAC “t:num” THEN ASM_REWRITE_TAC[]
383 THEN MY_MP_TAC “!t.q(SUC((t+delta)+t0)):bool”
384 THENL[
385 INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES]
386 THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES]
387 THEN STRIP_TAC THEN ASM_REWRITE_TAC[],
388 DISCH_TAC]
389 THEN DISJ_CASES_TAC(SPECL[“t:num”,“delta:num”]LESS_CASES)
390 THEN ASM_REWRITE_TAC[] THEN UNDISCH_HD_TAC
391 THEN REWRITE_TAC[LESS_OR_EQ] THEN STRIP_TAC
392 THENL[
393 IMP_RES_TAC LESS_ADD_1 THEN LEFT_NO_FORALL_TAC 2 “p:num”
394 THEN UNDISCH_HD_TAC THEN IMP_RES_TAC(EQT_ELIM(ARITH_CONV
395 “(t=delta+(p+1)) ==> (SUC((p+delta)+t0) = t+t0)”))
396 THEN POP_ASSUM REWRITE1_TAC THEN ASM_REWRITE_TAC[],
397 UNDISCH_NO_TAC 2 THEN ASM_REWRITE_TAC[]],
398 UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[],
399 ASSUME_TAC(SPEC_ALL(REWRITE_RULE[WATCH]WATCH_EXISTS))
400 THEN LEFT_EXISTS_TAC THEN EXISTS_TAC“q:num->bool”
401 THEN ASM_REWRITE_TAC[] THEN DISJ_CASES_TAC DELTA_CASES
402 THEN ASM_REWRITE_TAC[] THEN DISJ1_TAC THEN LEFT_EXISTS_TAC
403 THEN LEFT_NO_FORALL_TAC 2 “d:num” THEN UNDISCH_HD_TAC
404 THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN EXISTS_TAC “t:num”
405 THEN RES_TAC THEN ASM_REWRITE_TAC[]
406 THEN MY_MP_TAC “!t. t<d ==> ~q(t+t0)”
407 THENL[
408 INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES]
409 THEN DISCH_TAC THEN IMP_RES_TAC(EQT_ELIM(ARITH_CONV
410 “(SUC t < d) ==> t < d”))
411 THEN RES_TAC THEN ASM_REWRITE_TAC[],
412 DISCH_TAC]
413 THEN POP_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]]);
414
415val SWHEN_SIGNAL = TAC_PROOF(
416 ([],“(a SWHEN b) t0 =
417 ?delta. (!t. t<delta ==> ~b(t+t0)) /\ b(delta+t0) /\ a(delta+t0)”),
418 REWRITE_TAC[SWHEN] THEN EQ_TAC THEN STRIP_TAC
419 THENL[
420 RULE_ASSUM_TAC(REWRITE_RULE[WATCH_SIGNAL])
421 THEN UNDISCH_NO_TAC 3 THEN DISJ_CASES_TAC DELTA_CASES
422 THEN RES_TAC THEN LEFT_EXISTS_TAC
423 THEN STRIP_TAC THEN LEFT_FORALL_TAC “d:num”
424 THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
425 THEN MY_MP_TAC “d=(t:num)”
426 THENL[
427 DISJ_CASES_TAC(SPECL[“t:num”,“d:num”]LESS_CASES)
428 THEN RES_TAC THEN UNDISCH_HD_TAC THEN REWRITE_TAC[LESS_OR_EQ]
429 THEN STRIP_TAC THEN IMP_RES_TAC LESS_ADD_1 THEN UNDISCH_NO_TAC 8
430 THEN POP_ASSUM SUBST1_TAC
431 THEN SUBST1_TAC(EQT_ELIM(ARITH_CONV“(d+(p+1))+t0 = SUC(p+(d+t0))”))
432 THEN ASM_REWRITE_TAC[],
433 DISCH_TAC]
434 THEN POP_ASSUM(fn x=> RULE_ASSUM_TAC(REWRITE_RULE[SYM x]))
435 THEN EXISTS_TAC“d:num” THEN ASM_REWRITE_TAC[],
436 ASSUME_TAC(SPEC_ALL WATCH_EXISTS) THEN LEFT_EXISTS_TAC
437 THEN EXISTS_TAC “q:num->bool” THEN ASM_REWRITE_TAC[]
438 THEN EXISTS_TAC“delta:num” THEN ASM_REWRITE_TAC[]
439 THEN RULE_ASSUM_TAC(REWRITE_RULE[WATCH_SIGNAL])
440 THEN UNDISCH_HD_TAC THEN STRIP_TAC
441 THEN LEFT_FORALL_TAC “delta:num” THEN UNDISCH_HD_TAC
442 THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
443 THEN POP_NO_ASSUM 1 MATCH_MP_TAC
444 THEN CONV_TAC ARITH_CONV])
445
446
447
448
449Theorem SUNTIL_SIGNAL:
450 (a SUNTIL b) t0 =
451 ?delta. (!t. t<delta ==> a(t+t0) /\~b(t+t0)) /\ b(delta+t0)
452Proof
453 REWRITE_TAC[SUNTIL] >> EQ_TAC >> STRIP_TAC
454 THENL[
455 RULE_ASSUM_TAC(REWRITE_RULE[WATCH_SIGNAL])
456 >> UNDISCH_NO_TAC 2 >> DISJ_CASES_TAC DELTA_CASES
457 THENL[LEFT_EXISTS_TAC, UNDISCH_NO_TAC 1 >> ASM_REWRITE_TAC[]]
458 >> STRIP_TAC >> LEFT_FORALL_TAC “d:num”
459 >> UNDISCH_HD_TAC >> ASM_REWRITE_TAC[] >> DISCH_TAC
460 >> EXISTS_TAC “d:num” >> ASM_REWRITE_TAC[]
461 >> GEN_TAC >> STRIP_TAC
462 >> IMP_RES_TAC(EQT_ELIM(ARITH_CONV“x<y==>x<=y”))
463 >> RES_TAC >> LEFT_NO_FORALL_TAC 8 “t':num”
464 >> UNDISCH_HD_TAC >> ASM_REWRITE_TAC[] ,
465 ASSUME_TAC(SPEC_ALL WATCH_EXISTS) >> LEFT_EXISTS_TAC
466 >> EXISTS_TAC “q:num->bool” >> ASM_REWRITE_TAC[]
467 >> CONJ_TAC
468 THENL[ALL_TAC, EXISTS_TAC“delta:num” >> ASM_REWRITE_TAC[]]
469 >> UNDISCH_NO_TAC 2 >> REWRITE_TAC[IMP_CONJ_THM]
470 >> CONV_TAC(DEPTH_CONV FORALL_AND_CONV) >> STRIP_TAC
471 >> RULE_ASSUM_TAC(REWRITE_RULE[WATCH_SIGNAL])
472 >> UNDISCH_NO_TAC 2 >> STRIP_TAC
473 >> LEFT_FORALL_TAC “delta:num” >> UNDISCH_HD_TAC
474 >> ASM_REWRITE_TAC[] >> STRIP_TAC >> GEN_TAC
475 >> DISJ_CASES_TAC(SPECL[“t:num”,“delta:num”]LESS_CASES)
476 THENL[RES_TAC >> ASM_REWRITE_TAC[],ALL_TAC]
477 >> UNDISCH_HD_TAC >> REWRITE_TAC[LESS_OR_EQ] >> STRIP_TAC
478 THENL[ALL_TAC,POP_ASSUM(SUBST1_TAC o SYM) >> ASM_REWRITE_TAC[]]
479 >> IMP_RES_TAC LESS_ADD_1 >> POP_ASSUM SUBST1_TAC >> DISJ1_TAC
480 >> SUBST1_TAC(EQT_ELIM(ARITH_CONV“(delta+(p+1))+t0 = SUC(p+(delta+t0))”))
481 >> ASM_REWRITE_TAC[]]
482QED
483
484val SBEFORE_SIGNAL = TAC_PROOF(
485 ([],“(a SBEFORE b) t0
486 = ?delta.
487 a(delta+t0) /\
488 (!t. t<=delta ==> ~b(t+t0))”),
489 REWRITE_TAC[SBEFORE,WATCH] THEN EQ_TAC THEN REPEAT STRIP_TAC
490 THENL[
491 EXISTS_TAC “t:num” THEN ASM_REWRITE_TAC[]
492 THEN MY_MP_TAC “!t. b(t+t0) ==> !x. q(SUC(x+(t+t0)))”
493 THENL[
494 GEN_TAC THEN DISCH_TAC
495 THEN INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES]
496 THEN LEFT_NO_FORALL_TAC 5 “SUC(x+t')”
497 THEN UNDISCH_HD_TAC
498 THEN SUBST1_TAC(EQT_ELIM(ARITH_CONV
499 “ SUC(x+t')+t0 = SUC(x+(t'+t0))”))
500 THEN ASM_TAC 0 REWRITE1_TAC
501 THEN STRIP_TAC,
502 DISCH_TAC]
503 THEN GEN_TAC THEN DISCH_TAC
504 THEN IMP_RES_TAC LESS_EQUAL_ADD
505 THEN UNDISCH_NO_TAC 4 THEN UNDISCH_NO_TAC 4
506 THEN POP_ASSUM SUBST1_TAC
507 THEN SPEC_TAC(“p:num”,“p:num”)
508 THEN INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES]
509 THEN UNDISCH_HD_TAC THEN TAUT_TAC,
510 ASSUME_TAC(SPEC_ALL(REWRITE_RULE[WATCH]WATCH_EXISTS))
511 THEN LEFT_EXISTS_TAC THEN EXISTS_TAC “q:num->bool”
512 THEN ASM_REWRITE_TAC[]
513 THEN EXISTS_TAC “delta:num” THEN ASM_REWRITE_TAC[]
514 THEN CONJ_TAC
515 THENL[
516 MY_MP_TAC “!t. t<=delta ==> ~q(t+t0)”
517 THENL[
518 INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES]
519 THEN DISCH_TAC
520 THEN IMP_RES_TAC(EQT_ELIM(ARITH_CONV
521 “ SUC t <= delta ==> t<=delta”))
522 THEN RES_TAC THEN ASM_REWRITE_TAC[],
523 DISCH_TAC]
524 THEN POP_ASSUM MATCH_MP_TAC THEN CONV_TAC ARITH_CONV,
525 POP_NO_ASSUM 1 MATCH_MP_TAC THEN CONV_TAC ARITH_CONV
526 ]])
527
528
529
530
531(* ************************************************************ *)
532(* Expressiveness of WHEN *)
533(* ************************************************************ *)
534
535val ALWAYS_AS_WHEN = TAC_PROOF(
536 ([],“ALWAYS a = ((\t.F) WHEN (\t. ~a t))”),
537 CONV_TAC (X_FUN_EQ_CONV “t0:num”) THEN GEN_TAC
538 THEN PURE_REWRITE_TAC[ALWAYS,WHEN,WATCH] THEN BETA_TAC
539 THEN REWRITE_TAC[] THEN EQ_TAC THEN STRIP_TAC
540 THENL[
541 ASSUME_TAC(SPECL[“\t:num.F”,“t0:num”] WATCH_EXISTS)
542 THEN LEFT_EXISTS_TAC THEN RULE_ASSUM_TAC (REWRITE_RULE[WATCH])
543 THEN EXISTS_TAC“q:num->bool” THEN ASM_REWRITE_TAC[],
544 MY_MP_TAC“!t. ~q(t+t0)”
545 THENL[
546 INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES]
547 THEN LEFT_NO_FORALL_TAC 1 “t:num”
548 THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[],
549 DISCH_TAC THEN UNDISCH_NO_TAC 1
550 THEN ASM_REWRITE_TAC[]]])
551
552val EVENTUAL_AS_WHEN = TAC_PROOF(
553 ([],“EVENTUAL a = \t. ~((\t.F) WHEN a) t”),
554 ASSUME_TAC(SPEC“\t:num.~a t”(GEN“a:num->bool”ALWAYS_AS_WHEN))
555 THEN UNDISCH_HD_TAC THEN BETA_TAC THEN REWRITE_TAC[]
556 THEN CONV_TAC(DEPTH_CONV ETA_CONV) THEN DISCH_TAC
557 THEN POP_ASSUM (SUBST1_TAC o SYM)
558 THEN CONV_TAC FUN_EQ_CONV THEN GEN_TAC
559 THEN REWRITE_TAC[EVENTUAL,ALWAYS]
560 THEN BETA_TAC THEN CONV_TAC(DEPTH_CONV NOT_FORALL_CONV)
561 THEN REWRITE_TAC[])
562
563val UNTIL_AS_WHEN = TAC_PROOF(
564 ([],“(a UNTIL b) = (b WHEN (\t. a t ==> b t))”),
565 CONV_TAC (X_FUN_EQ_CONV “t0:num”) >> GEN_TAC
566 >> PURE_REWRITE_TAC[UNTIL, WHEN,WATCH]
567 >> BETA_TAC >> EQ_TAC >> STRIP_TAC
568 THENL[
569 ASSUME_TAC(SPECL[“\t:num. a t ==> b t”,“t0:num”]WATCH_EXISTS)
570 >> LEFT_EXISTS_TAC >> RULE_ASSUM_TAC (BETA_RULE o REWRITE_RULE[WATCH])
571 >> EXISTS_TAC“q':num->bool” >> ASM_REWRITE_TAC[],
572 ASSUME_TAC(SPEC_ALL WATCH_EXISTS)
573 >> LEFT_EXISTS_TAC >> RULE_ASSUM_TAC (REWRITE_RULE[WATCH])
574 >> EXISTS_TAC“q':num->bool” >> ASM_REWRITE_TAC[]]
575 >> (MY_MP_TAC “!t. q(t+t0):bool = q'(t+t0)” THENL[
576 INDUCT_TAC >> ASM_REWRITE_TAC[ADD_CLAUSES]
577 >> LEFT_NO_FORALL_TAC 2 “t:num”
578 >> UNDISCH_HD_TAC >> ASM_REWRITE_TAC[] >> TAUT_TAC,
579 DISCH_TAC
580 >> POP_ASSUM (fn x=> REWRITE_TAC[x] >> RULE_ASSUM_TAC(REWRITE_RULE[x]))
581 >> GEN_TAC >> LEFT_NO_FORALL_TAC 1 “t:num”
582 >> UNDISCH_HD_TAC >> TAUT_TAC]));
583
584
585
586Theorem BEFORE_AS_WHEN:
587 a BEFORE b = (\t. ~b t) WHEN (\t.a t \/ b t)
588Proof
589 CONV_TAC(X_FUN_EQ_CONV “t0:num”) THEN GEN_TAC
590 THEN REWRITE_TAC[BEFORE_SIGNAL,WHEN_SIGNAL] THEN BETA_TAC
591 THEN MY_MP_TAC “!delta.
592 (!t. t<delta ==> ~a(t+t0) /\ ~b(t+t0))
593 <=>
594 (!t. t<delta ==> ~a(t+t0)) /\
595 (!t. t<delta ==> ~b(t+t0))”
596 THENL[GEN_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THEN RES_TAC,
597 DISCH_TAC]
598 THEN REWRITE_TAC[DE_MORGAN_THM] THEN POP_ASSUM REWRITE1_TAC
599 THEN EQ_TAC THEN REPEAT STRIP_TAC
600 THENL[
601 LEFT_NO_FORALL_TAC 4 “delta:num”
602 THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[]
603 THEN CONV_TAC NOT_EXISTS_CONV THEN GEN_TAC
604 THEN REWRITE_TAC[DECIDE “~(a/\b) <=> a==>~b”]
605 THEN DISCH_TAC THEN RES_TAC,
606 LEFT_NO_FORALL_TAC 3 “delta:num”
607 THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[]
608 THEN STRIP_TAC THEN RES_TAC,
609 LEFT_NO_FORALL_TAC 2 “delta:num”
610 THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[]
611 THEN CONV_TAC(DEPTH_CONV NOT_FORALL_CONV)
612 THEN REWRITE_TAC[DECIDE “~(a==>b) <=> a/\~b”]]
613QED
614
615
616
617val SWHEN_AS_WHEN = TAC_PROOF(
618 ([],“(a SWHEN b) = \t0. (a WHEN b) t0 /\ EVENTUAL b t0”),
619 CONV_TAC(X_FUN_EQ_CONV“t0:num”) THEN BETA_TAC THEN GEN_TAC
620 THEN REWRITE_TAC[SWHEN_SIGNAL,WHEN_SIGNAL,EVENTUAL]
621 THEN EQ_TAC THEN REPEAT STRIP_TAC
622 THENL[
623 MY_MP_TAC “delta=(delta':num)”
624 THENL[
625 DISJ_CASES_TAC(SPECL[“delta':num”,“delta:num”]LESS_CASES)
626 THENL[RES_TAC,ALL_TAC]
627 THEN UNDISCH_HD_TAC THEN REWRITE_TAC[LESS_OR_EQ] THEN STRIP_TAC
628 THEN RES_TAC,
629 DISCH_TAC]
630 THEN POP_ASSUM(SUBST1_TAC o SYM) THEN ASM_REWRITE_TAC[],
631 EXISTS_TAC“delta:num” THEN ASM_REWRITE_TAC[],
632 DISJ_CASES_TAC DELTA_CASES THEN RES_TAC
633 THEN LEFT_NO_EXISTS_TAC 1 THEN LEFT_NO_FORALL_TAC 3 “d:num”
634 THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
635 THEN EXISTS_TAC “d:num” THEN ASM_REWRITE_TAC[]])
636
637
638val SWHEN_AS_NOT_WHEN =
639 let
640 val NOT_WHEN = TAC_PROOF(
641 ([],“~((a WHEN b)t0) = ((\t.~a t) SWHEN b) t0”),
642 REWRITE_TAC[WHEN_SIGNAL,SWHEN_SIGNAL] THEN BETA_TAC
643 THEN CONV_TAC(DEPTH_CONV NOT_FORALL_CONV)
644 THEN REWRITE_TAC[DECIDE “~(a==>b) = a/\~b”]
645 THEN EQ_TAC THEN REPEAT STRIP_TAC THEN RES_TAC
646 THEN EXISTS_TAC“delta:num” THEN ASM_REWRITE_TAC[])
647 val thm1 = BETA_RULE(SPEC“\t:num.~a t”(GEN“a:num->bool”NOT_WHEN))
648 val thm2 = SYM(REWRITE_RULE[]thm1)
649 val thm3 = (CONV_RULE(DEPTH_CONV ETA_CONV)) thm2
650 in thm3
651 end
652
653
654val SUNTIL_AS_WHEN = TAC_PROOF(
655 ([],“(a SUNTIL b) = \t. (b WHEN (\t. a t ==> b t)) t /\ EVENTUAL b t”),
656 REWRITE_TAC[SYM UNTIL_AS_WHEN]
657 THEN CONV_TAC(X_FUN_EQ_CONV“t0:num”) THEN BETA_TAC THEN GEN_TAC
658 THEN REWRITE_TAC[SUNTIL_SIGNAL,UNTIL_SIGNAL,EVENTUAL]
659 THEN EQ_TAC THEN REPEAT STRIP_TAC
660 THENL[
661 RES_TAC,
662 MY_MP_TAC “delta=(d:num)”
663 THENL[
664 DISJ_CASES_TAC(SPECL[“d:num”,“delta:num”]LESS_CASES)
665 THENL[RES_TAC,ALL_TAC]
666 THEN UNDISCH_HD_TAC THEN REWRITE_TAC[LESS_OR_EQ] THEN STRIP_TAC
667 THEN RES_TAC,
668 DISCH_TAC]
669 THEN POP_ASSUM(fn x=> RULE_ASSUM_TAC(REWRITE_RULE[SYM x]))
670 THEN RES_TAC,
671 EXISTS_TAC“delta:num” THEN ASM_REWRITE_TAC[],
672 DISJ_CASES_TAC DELTA_CASES THEN RES_TAC
673 THEN LEFT_NO_EXISTS_TAC 1 THEN LEFT_NO_FORALL_TAC 3 “d:num”
674 THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
675 THEN EXISTS_TAC “d:num” THEN ASM_REWRITE_TAC[]
676 THEN GEN_TAC THEN DISCH_TAC THEN RES_TAC
677 THEN ASM_REWRITE_TAC[]])
678
679
680
681val SBEFORE_AS_WHEN = prove(
682 “a SBEFORE b = \t0. ((\t.~b t) WHEN (\t.a t \/ b t)) t0 /\ EVENTUAL a t0”,
683 REWRITE_TAC[SYM BEFORE_AS_WHEN]
684 THEN CONV_TAC(X_FUN_EQ_CONV “t0:num”) THEN GEN_TAC THEN BETA_TAC
685 THEN REWRITE_TAC[SBEFORE,BEFORE,EVENTUAL] THEN EQ_TAC
686 THEN REPEAT STRIP_TAC
687 THENL[
688 EXISTS_TAC “q:num->bool” THEN ASM_REWRITE_TAC[]
689 THEN DISJ1_TAC THEN EXISTS_TAC “t:num”
690 THEN ASM_REWRITE_TAC[],
691 EXISTS_TAC “t:num” THEN ASM_REWRITE_TAC[],
692 EXISTS_TAC “q:num->bool” THEN ASM_REWRITE_TAC[]
693 THEN EXISTS_TAC “t:num” THEN ASM_REWRITE_TAC[],
694 EXISTS_TAC “q:num->bool” THEN ASM_REWRITE_TAC[]
695 THEN EXISTS_TAC “t:num” THEN ASM_REWRITE_TAC[]
696 THEN UNDISCH_NO_TAC 2 THEN ASM_REWRITE_TAC[WATCH_SIGNAL]
697 THEN DISCH_TAC THEN ASM_REWRITE_TAC[]]);
698
699
700
701
702
703val BEFORE_AS_WHEN_UNTIL = TAC_PROOF(
704 ([],“(a BEFORE b) = \t. ((\t.~b t) UNTIL a) t /\ ((\t.~b t) WHEN a) t”),
705 CONV_TAC(X_FUN_EQ_CONV “t0:num”) THEN GEN_TAC
706 THEN REWRITE_TAC[BEFORE_SIGNAL,UNTIL_SIGNAL,WHEN_SIGNAL]
707 THEN BETA_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC
708 THENL[
709 UNDISCH_NO_TAC 2 THEN ASM_REWRITE_TAC[]
710 THEN IMP_RES_TAC(BETA_RULE(ISPEC“\t.b(t+t0):bool”WOP))
711 THEN CONV_TAC NOT_FORALL_CONV THEN EXISTS_TAC “n:num”
712 THEN ASM_REWRITE_TAC[],
713 DISJ_CASES_TAC DELTA_CASES THENL[ALL_TAC,RES_TAC]
714 THEN LEFT_EXISTS_TAC THEN LEFT_NO_FORALL_TAC 5 “d':num”
715 THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[]
716 THEN CONV_TAC NOT_EXISTS_CONV THEN GEN_TAC
717 THEN REWRITE_TAC[DECIDE “~(a/\b) = a==>~b”]
718 THEN DISCH_TAC THEN ASM_TAC 5 MATCH_MP_TAC
719 THEN MY_MP_TAC “d'<=d”
720 THENL[
721 DISJ_CASES_TAC(SPECL[“d:num”,“d':num”]LESS_CASES)
722 THEN ASM_REWRITE_TAC[] THEN IMP_RES_TAC LESS_TRANS
723 THEN RES_TAC,
724 DISCH_TAC]
725 THEN IMP_RES_TAC(EQT_ELIM(ARITH_CONV“x<y /\ y<=z ==> x<z”)),
726 DISJ_CASES_TAC DELTA_CASES THENL[ALL_TAC,RES_TAC] THEN LEFT_EXISTS_TAC
727 THEN LEFT_NO_FORALL_TAC 4 “d:num”
728 THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[]
729 THEN CONV_TAC NOT_EXISTS_CONV THEN GEN_TAC
730 THEN REWRITE_TAC[DECIDE “~(a/\b) = a==>~b”]
731 THEN DISCH_TAC THEN ASM_TAC 4 MATCH_MP_TAC
732 THEN MY_MP_TAC “d<=delta”
733 THENL[
734 DISJ_CASES_TAC(SPECL[“delta:num”,“d:num”]LESS_CASES)
735 THEN ASM_REWRITE_TAC[] THEN IMP_RES_TAC LESS_TRANS
736 THEN RES_TAC,
737 DISCH_TAC]
738 THEN IMP_RES_TAC(EQT_ELIM(ARITH_CONV“x<y /\ y<=z ==> x<z”)),
739 DISJ_CASES_TAC(SPEC“a:num->bool”(GEN“b:num->bool”DELTA_CASES))
740 THENL[ALL_TAC,RES_TAC] THEN LEFT_EXISTS_TAC
741 THEN LEFT_NO_FORALL_TAC 3 “d:num” THEN UNDISCH_HD_TAC
742 THEN LEFT_NO_FORALL_TAC 3 “d:num” THEN UNDISCH_HD_TAC
743 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN DISCH_TAC
744 THEN MY_MP_TAC “d<delta”
745 THENL[
746 DISJ_CASES_TAC(SPECL[“d:num”,“delta:num”]LESS_CASES)
747 THEN ASM_REWRITE_TAC[] THEN UNDISCH_HD_TAC
748 THEN REWRITE_TAC[LESS_OR_EQ] THEN STRIP_TAC THEN RES_TAC
749 THEN UNDISCH_NO_TAC 4 THEN ASM_REWRITE_TAC[],
750 DISCH_TAC]
751 THEN EXISTS_TAC “d:num” THEN ASM_REWRITE_TAC[]])
752
753
754
755val BEFORE_HW = TAC_PROOF(
756 ([],“(a BEFORE b) t0 = ?q. (q WATCH a) t0 /\ !t. q(t+t0)\/ ~b(t+t0)”),
757 REWRITE_TAC[BEFORE_AS_WHEN_UNTIL,WHEN,UNTIL] THEN BETA_TAC
758 THEN EQ_TAC THEN REPEAT STRIP_TAC
759 THEN EXISTS_TAC “q:num->bool” THEN ASM_REWRITE_TAC[]
760 THENL[
761 ALL_TAC,
762 GEN_TAC THEN REWRITE_TAC[DECIDE “(a\/b) = ~a==>b”]
763 THEN DISCH_TAC THEN LEFT_NO_FORALL_TAC 1 “t':num”
764 THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
765 THEN ASM_REWRITE_TAC[],
766 GEN_TAC THEN REWRITE_TAC[DECIDE “(a\/b) = ~a==>b”]
767 THEN DISCH_TAC THEN LEFT_NO_FORALL_TAC 1 “t':num”
768 THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
769 THEN ASM_REWRITE_TAC[]]
770 THEN RULE_ASSUM_TAC(REWRITE_RULE[WATCH])
771 THEN MY_MP_TAC“!t. q(t+t0):bool = q'(t+t0)”
772 THENL[INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES],DISCH_TAC]
773 THEN POP_ASSUM (fn x=> RULE_ASSUM_TAC(REWRITE_RULE[SYM(SPEC_ALL x)]))
774 THEN GEN_TAC THEN LEFT_NO_FORALL_TAC 2 “t:num”
775 THEN UNDISCH_HD_TAC THEN LEFT_NO_FORALL_TAC 0 “t:num”
776 THEN UNDISCH_HD_TAC THEN TAUT_TAC)
777
778(* ************************************************************ *)
779(* Expressiveness of UNTIL *)
780(* ************************************************************ *)
781
782val ALWAYS_AS_UNTIL = TAC_PROOF(
783 ([],“(ALWAYS a) = (a UNTIL (\t.F))”),
784 CONV_TAC (X_FUN_EQ_CONV “t0:num”) THEN GEN_TAC
785 THEN PURE_REWRITE_TAC[UNTIL_AS_WHEN] THEN BETA_TAC
786 THEN REWRITE_TAC[ALWAYS_AS_WHEN])
787
788val EVENTUAL_AS_UNTIL = TAC_PROOF(
789 ([],“(EVENTUAL a) = \t. ~((\t.~a t) UNTIL (\t.F)) t”),
790 ASSUME_TAC(SPEC“\t:num.~a t”(GEN“a:num->bool”ALWAYS_AS_UNTIL))
791 THEN UNDISCH_HD_TAC THEN BETA_TAC THEN REWRITE_TAC[]
792 THEN CONV_TAC(DEPTH_CONV ETA_CONV) THEN DISCH_TAC
793 THEN POP_ASSUM (SUBST1_TAC o SYM)
794 THEN CONV_TAC FUN_EQ_CONV THEN GEN_TAC
795 THEN REWRITE_TAC[EVENTUAL,ALWAYS]
796 THEN BETA_TAC THEN CONV_TAC(DEPTH_CONV NOT_FORALL_CONV)
797 THEN REWRITE_TAC[])
798
799
800val WHEN_AS_UNTIL = TAC_PROOF(
801 ([],“(a WHEN b) = ((\t.~b t) UNTIL (\t.a t /\ b t))”),
802 CONV_TAC (X_FUN_EQ_CONV “t0:num”) THEN GEN_TAC
803 THEN PURE_REWRITE_TAC[UNTIL_AS_WHEN] THEN BETA_TAC
804 THEN REWRITE_TAC[DECIDE “(~b==> a/\b) = b”]
805 THEN PURE_REWRITE_TAC[WHEN_SIGNAL]
806 THEN BETA_TAC THEN EQ_TAC THEN STRIP_TAC
807 THEN GEN_TAC THEN STRIP_TAC THEN RES_TAC THEN ASM_REWRITE_TAC[])
808
809
810val BEFORE_AS_UNTIL = TAC_PROOF(
811 ([],“(a BEFORE b) = \t0. ~((\t.~a t) UNTIL b) t0 \/ ALWAYS (\t.~b t) t0”),
812 CONV_TAC (X_FUN_EQ_CONV “t0:num”) THEN GEN_TAC
813 THEN REWRITE_TAC[BEFORE_IMP,UNTIL,ALWAYS]
814 THEN BETA_TAC THEN CONV_TAC(DEPTH_CONV NOT_EXISTS_CONV)
815 THEN REWRITE_TAC[DECIDE “(a==>b) = (~a\/b)”]
816 THEN REWRITE_TAC[DE_MORGAN_THM]
817 THEN CONV_TAC(DEPTH_CONV LEFT_OR_FORALL_CONV)
818 THEN CONV_TAC(DEPTH_CONV NOT_FORALL_CONV)
819 THEN REWRITE_TAC[DE_MORGAN_THM]
820 THEN REWRITE_TAC[DECIDE “(a\/b)\/c = a\/b\/c”])
821
822
823
824
825val SWHEN_AS_UNTIL = TAC_PROOF(
826 ([],“(a SWHEN b) = \t.((\t.~b t) UNTIL (\t.a t /\ b t)) t /\
827 EVENTUAL b t”),
828 CONV_TAC FUN_EQ_CONV THEN BETA_TAC
829 THEN REWRITE_TAC[SWHEN_AS_WHEN,WHEN_AS_UNTIL]
830 THEN BETA_TAC THEN REWRITE_TAC[])
831
832
833
834
835
836val SUNTIL_AS_UNTIL = TAC_PROOF(
837 ([],“(a SUNTIL b) = \t0. (a UNTIL b) t0 /\ EVENTUAL b t0”),
838 CONV_TAC(X_FUN_EQ_CONV“t0:num”) THEN BETA_TAC THEN GEN_TAC
839 THEN REWRITE_TAC[SUNTIL_SIGNAL,UNTIL_SIGNAL,EVENTUAL]
840 THEN EQ_TAC THEN REPEAT STRIP_TAC
841 THENL[
842 RES_TAC,
843 MY_MP_TAC “delta=(d:num)”
844 THENL[
845 DISJ_CASES_TAC(SPECL[“d:num”,“delta:num”]LESS_CASES)
846 THENL[RES_TAC,ALL_TAC]
847 THEN UNDISCH_HD_TAC THEN REWRITE_TAC[LESS_OR_EQ] THEN STRIP_TAC
848 THEN RES_TAC,
849 DISCH_TAC]
850 THEN POP_ASSUM(fn x=> RULE_ASSUM_TAC(REWRITE_RULE[SYM x]))
851 THEN RES_TAC,
852 EXISTS_TAC“delta:num” THEN ASM_REWRITE_TAC[],
853 DISJ_CASES_TAC DELTA_CASES THEN RES_TAC
854 THEN LEFT_NO_EXISTS_TAC 1 THEN LEFT_NO_FORALL_TAC 3 “d:num”
855 THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
856 THEN EXISTS_TAC “d:num” THEN ASM_REWRITE_TAC[]
857 THEN GEN_TAC THEN DISCH_TAC THEN RES_TAC
858 THEN ASM_REWRITE_TAC[]])
859
860
861
862
863val SBEFORE_AS_UNTIL = TAC_PROOF(
864 ([],“(a SBEFORE b) = \t0. ~((\t.~a t) UNTIL b) t0 ”),
865 CONV_TAC (X_FUN_EQ_CONV “t0:num”) THEN GEN_TAC
866 THEN REWRITE_TAC[SBEFORE,UNTIL_IMP]
867 THEN BETA_TAC THEN CONV_TAC(DEPTH_CONV NOT_FORALL_CONV)
868 THEN REWRITE_TAC[DECIDE “~(a==>b) = a/\~b”]
869 THEN CONV_TAC(DEPTH_CONV NOT_FORALL_CONV)
870 THEN REWRITE_TAC[DE_MORGAN_THM])
871
872(* ************************************************************ *)
873(* Expressiveness of BEFORE *)
874(* ************************************************************ *)
875
876
877val EVENTUAL_AS_BEFORE = TAC_PROOF(
878 ([],“EVENTUAL b = \t0. ~((\t.F) BEFORE b) t0”),
879 CONV_TAC(X_FUN_EQ_CONV“t0:num”) THEN BETA_TAC THEN GEN_TAC
880 THEN REWRITE_TAC[BEFORE_SIGNAL,EVENTUAL] THEN BETA_TAC
881 THEN CONV_TAC(DEPTH_CONV NOT_FORALL_CONV)
882 THEN REWRITE_TAC[] THEN EQ_TAC THEN REPEAT STRIP_TAC
883 THENL[
884 DISJ_CASES_TAC DELTA_CASES THEN RES_TAC
885 THEN ASM_REWRITE_TAC[],
886 EXISTS_TAC“delta:num” THEN ASM_REWRITE_TAC[]])
887
888
889val ALWAYS_AS_BEFORE = TAC_PROOF(
890 ([],“ALWAYS b = (\t.F) BEFORE (\t.~b t)”),
891 let val thm1 = GEN_ALL EVENTUAL_AS_BEFORE
892 val thm2 = SPEC“\t:num.~b t”thm1
893 val thm3 = (CONV_RULE(X_FUN_EQ_CONV“t0:num”)) thm2
894 val thm4 = SPEC_ALL(BETA_RULE thm3)
895 in
896 CONV_TAC(X_FUN_EQ_CONV“t0:num”) THEN GEN_TAC
897 THEN ONCE_REWRITE_TAC[DECIDE “(a=b) = (~a= ~b)”]
898 THEN REWRITE_TAC[SYM thm4,ALWAYS,EVENTUAL] THEN BETA_TAC
899 THEN CONV_TAC(DEPTH_CONV NOT_FORALL_CONV)
900 THEN REWRITE_TAC[]
901 end)
902
903
904val UNTIL_AS_BEFORE = TAC_PROOF(
905 ([],“(a UNTIL b) = \t0. ~((\t.~a t) BEFORE b) t0 \/ ALWAYS a t0”),
906 CONV_TAC(X_FUN_EQ_CONV“t0:num”) THEN BETA_TAC THEN GEN_TAC
907 THEN REWRITE_TAC[UNTIL_SIGNAL,BEFORE_SIGNAL,ALWAYS] THEN BETA_TAC
908 THEN CONV_TAC(DEPTH_CONV NOT_FORALL_CONV)
909 THEN REWRITE_TAC[DE_MORGAN_THM,DECIDE “~(a==>b) = a/\~b”]
910 THEN CONV_TAC(DEPTH_CONV NOT_EXISTS_CONV)
911 THEN REWRITE_TAC[DECIDE “~(a/\~b) = a==>b”]
912 THEN EQ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]
913 THENL[
914 DISJ_CASES_TAC DELTA_CASES
915 THENL[
916 LEFT_EXISTS_TAC THEN LEFT_NO_FORALL_TAC 1 “d:num”
917 THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
918 THEN DISJ1_TAC THEN EXISTS_TAC “d:num”
919 THEN ASM_REWRITE_TAC[],
920 UNDISCH_NO_TAC 2 THEN ASM_REWRITE_TAC[]],
921 UNDISCH_NO_TAC 2 THEN ASM_REWRITE_TAC[],
922 MY_MP_TAC“(d:num)=delta”
923 THENL[
924 DISJ_CASES_TAC(SPECL[“delta:num”,“d:num”]LESS_CASES)
925 THENL[RES_TAC,ALL_TAC]
926 THEN UNDISCH_HD_TAC THEN REWRITE_TAC[LESS_OR_EQ] THEN STRIP_TAC
927 THEN RES_TAC,
928 DISCH_TAC]
929 THEN POP_ASSUM (fn x=> RULE_ASSUM_TAC(REWRITE_RULE[x]))
930 THEN RES_TAC])
931
932
933val WHEN_AS_BEFORE =
934 let
935 val thm1 = GEN_ALL UNTIL_AS_BEFORE
936 val thm2 = SPECL[“\t:num. a t /\ b t”,“\t:num. ~b t”]thm1
937 val thm3 = REWRITE_RULE[SYM WHEN_AS_UNTIL]thm2
938 val thm4 = REWRITE_RULE[](BETA_RULE thm3)
939 val thm5 = (CONV_RULE(DEPTH_CONV ETA_CONV)) thm4
940 in thm5
941 end
942
943
944val SWHEN_AS_BEFORE = TAC_PROOF(
945 ([],“a SWHEN b = \t0.~(b BEFORE (\t. a t /\ b t)) t0”),
946 CONV_TAC(X_FUN_EQ_CONV“t0:num”) THEN BETA_TAC THEN GEN_TAC
947 THEN REWRITE_TAC[SWHEN_AS_WHEN,WHEN_AS_BEFORE,ALWAYS,EVENTUAL]
948 THEN BETA_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]
949 THEN RES_TAC THEN UNDISCH_HD_TAC THEN REWRITE_TAC[BEFORE_IMP]
950 THEN CONV_TAC(DEPTH_CONV NOT_FORALL_CONV) THEN BETA_TAC
951 THEN REWRITE_TAC[DECIDE “~(a==>b) = a/\~b”]
952 THEN REWRITE_TAC[DE_MORGAN_THM]
953 THEN CONV_TAC(DEPTH_CONV NOT_FORALL_CONV)
954 THEN CONV_TAC(DEPTH_CONV NOT_EXISTS_CONV)
955 THEN REWRITE_TAC[DE_MORGAN_THM]
956 THEN REPEAT STRIP_TAC THEN EXISTS_TAC“t:num”
957 THEN ASM_REWRITE_TAC[])
958
959
960
961val SUNTIL_AS_BEFORE = TAC_PROOF(
962 ([],“(a SUNTIL b) = \t0. ~((\t.~a t) BEFORE b) t0”),
963 CONV_TAC(X_FUN_EQ_CONV“t0:num”) THEN BETA_TAC THEN GEN_TAC
964 THEN REWRITE_TAC[SUNTIL_AS_UNTIL,UNTIL_AS_BEFORE,ALWAYS,EVENTUAL]
965 THEN BETA_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]
966 THEN RES_TAC
967 THENL[
968 UNDISCH_HD_TAC THEN REWRITE_TAC[BEFORE]
969 THEN BETA_TAC THEN ASM_REWRITE_TAC[]
970 THEN CONV_TAC(DEPTH_CONV NOT_EXISTS_CONV)
971 THEN REWRITE_TAC[DE_MORGAN_THM] THEN GEN_TAC THEN DISJ2_TAC
972 THEN CONV_TAC(DEPTH_CONV NOT_FORALL_CONV)
973 THEN EXISTS_TAC“t:num” THEN ASM_REWRITE_TAC[],
974 UNDISCH_HD_TAC THEN REWRITE_TAC[BEFORE_IMP]
975 THEN CONV_TAC(DEPTH_CONV NOT_FORALL_CONV) THEN BETA_TAC
976 THEN REWRITE_TAC[DECIDE “~(a==>b) = a/\~b”]
977 THEN REWRITE_TAC[DE_MORGAN_THM]
978 THEN CONV_TAC(DEPTH_CONV NOT_FORALL_CONV)
979 THEN CONV_TAC(DEPTH_CONV NOT_EXISTS_CONV)
980 THEN REWRITE_TAC[DE_MORGAN_THM]
981 THEN REPEAT STRIP_TAC THEN EXISTS_TAC“t:num”
982 THEN ASM_REWRITE_TAC[]])
983
984
985
986
987val SBEFORE_AS_BEFORE = TAC_PROOF(
988 ([],“(a SBEFORE b) = \t0.(a BEFORE b) t0 /\ EVENTUAL a t0”),
989 CONV_TAC(X_FUN_EQ_CONV“t0:num”) THEN BETA_TAC THEN GEN_TAC
990 THEN REWRITE_TAC[SBEFORE,BEFORE,EVENTUAL] THEN EQ_TAC
991 THEN REPEAT STRIP_TAC
992 THENL[
993 EXISTS_TAC “q:num->bool” THEN ASM_REWRITE_TAC[]
994 THEN DISJ1_TAC THEN EXISTS_TAC “t:num”
995 THEN ASM_REWRITE_TAC[],
996 EXISTS_TAC “t:num” THEN ASM_REWRITE_TAC[],
997 EXISTS_TAC “q:num->bool” THEN ASM_REWRITE_TAC[]
998 THEN EXISTS_TAC “t:num” THEN ASM_REWRITE_TAC[],
999 EXISTS_TAC “q:num->bool” THEN ASM_REWRITE_TAC[]
1000 THEN EXISTS_TAC “t:num” THEN ASM_REWRITE_TAC[]
1001 THEN UNDISCH_NO_TAC 2 THEN ASM_REWRITE_TAC[WATCH_SIGNAL]
1002 THEN DISCH_TAC THEN ASM_REWRITE_TAC[]])
1003
1004(* ************************************************************ *)
1005(* Expressiveness of SWHEN *)
1006(* ************************************************************ *)
1007
1008
1009val WHEN_SWHEN_LEMMA = TAC_PROOF(
1010 ([],“if (!t1.?t2.b(t2+t1))
1011 then (!t0. (a WHEN b) t0 = (a SWHEN b) t0)
1012 else ?t1.!t2. (a WHEN b)(t2+t1) /\ ~(a SWHEN b)(t2+t1)”),
1013 REWRITE_TAC[SWHEN_SIGNAL,WHEN_SIGNAL]
1014 THEN ASM_CASES_TAC“!t1.?t2.b(t2+t1)” THEN ASM_TAC 0 REWRITE1_TAC
1015 THENL[
1016 GEN_TAC THEN EQ_TAC THEN STRIP_TAC
1017 THENL[
1018 DISJ_CASES_TAC DELTA_CASES
1019 THENL[
1020 ALL_TAC,
1021 LEFT_NO_FORALL_TAC 2 “t0:num” THEN UNDISCH_HD_TAC
1022 THEN ASM_TAC 0 REWRITE1_TAC]
1023 THEN UNDISCH_HD_TAC THEN STRIP_TAC
1024 THEN RES_TAC THEN POP_NO_TAC 3 THEN EXISTS_TAC “d:num”
1025 THEN ASM_REWRITE_TAC[],
1026 REPEAT STRIP_TAC
1027 THEN MY_MP_TAC “delta'=(delta:num)”
1028 THENL[
1029 DISJ_CASES_TAC(SPECL[“delta:num”,“delta':num”]LESS_CASES)
1030 THENL[RES_TAC,ALL_TAC]
1031 THEN UNDISCH_HD_TAC THEN REWRITE_TAC[LESS_OR_EQ] THEN STRIP_TAC
1032 THEN RES_TAC,
1033 DISCH_TAC]
1034 THEN ASM_REWRITE_TAC[]],
1035 RULE_ASSUM_TAC(CONV_RULE(DEPTH_CONV NOT_FORALL_CONV))
1036 THEN RULE_ASSUM_TAC(CONV_RULE(DEPTH_CONV NOT_EXISTS_CONV))
1037 THEN LEFT_EXISTS_TAC THEN EXISTS_TAC “t1:num”
1038 THEN CONV_TAC(DEPTH_CONV NOT_EXISTS_CONV)
1039 THEN REPEAT STRIP_TAC
1040 THENL[UNDISCH_NO_TAC 0,UNDISCH_NO_TAC 1]
1041 THEN ASM_REWRITE_TAC[ADD_ASSOC]])
1042
1043
1044val EVENTUAL_AS_SWHEN = TAC_PROOF(
1045 ([],“EVENTUAL a = (\t.T) SWHEN a”),
1046 CONV_TAC (X_FUN_EQ_CONV “t0:num”) THEN GEN_TAC
1047 THEN REWRITE_TAC[SWHEN_SIGNAL,EVENTUAL_SIGNAL] THEN BETA_TAC
1048 THEN EQ_TAC THEN REPEAT STRIP_TAC THEN RES_TAC
1049 THENL[
1050 DISJ_CASES_TAC(SPEC“a:num->bool”(GEN“b:num->bool” DELTA_CASES))
1051 THENL[ALL_TAC, UNDISCH_NO_TAC 1 THEN ASM_REWRITE_TAC[]]
1052 THEN LEFT_EXISTS_TAC THEN EXISTS_TAC “d:num”
1053 THEN ASM_REWRITE_TAC[],
1054 EXISTS_TAC “delta:num” THEN ASM_REWRITE_TAC[]])
1055
1056
1057val ALWAYS_AS_SWHEN = TAC_PROOF(
1058 ([],“ALWAYS a = \t. ~((\t.T) SWHEN (\t.~a t)) t”),
1059 ASSUME_TAC(SPEC“\t:num.~a t”(GEN“a:num->bool”EVENTUAL_AS_SWHEN))
1060 THEN UNDISCH_HD_TAC THEN BETA_TAC THEN REWRITE_TAC[]
1061 THEN DISCH_TAC THEN POP_ASSUM (SUBST1_TAC o SYM)
1062 THEN CONV_TAC FUN_EQ_CONV THEN GEN_TAC
1063 THEN REWRITE_TAC[EVENTUAL,ALWAYS]
1064 THEN BETA_TAC THEN CONV_TAC(DEPTH_CONV NOT_EXISTS_CONV)
1065 THEN REWRITE_TAC[])
1066
1067
1068val WHEN_AS_SWHEN = TAC_PROOF(
1069 ([],“a WHEN b = \t. (a SWHEN b) t \/ ALWAYS (\t.~b t) t”),
1070 CONV_TAC (X_FUN_EQ_CONV “t0:num”) THEN GEN_TAC
1071 THEN REWRITE_TAC[SWHEN_SIGNAL,WHEN_SIGNAL,ALWAYS] THEN BETA_TAC
1072 THEN EQ_TAC THEN REPEAT STRIP_TAC THEN RES_TAC
1073 THENL[
1074 DISJ_CASES_TAC DELTA_CASES THEN ASM_REWRITE_TAC[]
1075 THEN LEFT_EXISTS_TAC THEN LEFT_NO_FORALL_TAC 1 “d:num”
1076 THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
1077 THEN DISJ1_TAC THEN EXISTS_TAC “d:num” THEN ASM_REWRITE_TAC[],
1078 MY_MP_TAC “delta=(delta':num)”
1079 THENL[
1080 DISJ_CASES_TAC(SPECL[“delta':num”,“delta:num”]LESS_CASES)
1081 THENL[RES_TAC,ALL_TAC]
1082 THEN UNDISCH_HD_TAC THEN REWRITE_TAC[LESS_OR_EQ] THEN STRIP_TAC
1083 THEN RES_TAC,
1084 DISCH_TAC]
1085 THEN POP_ASSUM (SUBST1_TAC o SYM) THEN ASM_REWRITE_TAC[]])
1086
1087
1088val WHEN_AS_NOT_SWHEN = TAC_PROOF(
1089 ([],“((a WHEN b)t0) = ~((\t.~a t) SWHEN b) t0”),
1090 REWRITE_TAC[WHEN_SIGNAL,SWHEN_SIGNAL] THEN BETA_TAC
1091 THEN CONV_TAC(DEPTH_CONV NOT_EXISTS_CONV)
1092 THEN REWRITE_TAC[DECIDE “~(a/\b/\~x) = a/\b==>x”])
1093
1094
1095val BEFORE_AS_SWHEN = TAC_PROOF(
1096 ([],“a BEFORE b =
1097 \t0. ((\t.~b t) SWHEN (\t. a t \/ b t)) t0 \/ ALWAYS (\t. ~a t /\ ~b t) t0”),
1098 CONV_TAC (X_FUN_EQ_CONV “t0:num”) THEN GEN_TAC
1099 THEN REWRITE_TAC[BEFORE_AS_WHEN,SWHEN_AS_WHEN,EVENTUAL,ALWAYS,WHEN_SIGNAL]
1100 THEN BETA_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC
1101 THEN RES_TAC THEN ASM_REWRITE_TAC[] THEN UNDISCH_HD_TAC
1102 THEN REWRITE_TAC[DECIDE “a/\(x\/b) ==> ~b = b ==> ~a”]
1103 THEN CONV_TAC(DEPTH_CONV NOT_FORALL_CONV)
1104 THEN REWRITE_TAC[DECIDE “~(a==>~b) = b /\ a”]
1105 THEN STRIP_TAC
1106 THEN DISJ_CASES_TAC DELTA_CASES
1107 THENL[
1108 LEFT_EXISTS_TAC THEN DISJ1_TAC THEN EXISTS_TAC“d:num”
1109 THEN ASM_REWRITE_TAC[],
1110 UNDISCH_NO_TAC 1 THEN ASM_REWRITE_TAC[]
1111 THEN MY_MP_TAC“~(?t.a(t+t0)) = !t.~a(t+t0)”
1112 THENL[CONV_TAC(DEPTH_CONV NOT_EXISTS_CONV) THEN REWRITE_TAC[],DISCH_TAC]
1113 THEN POP_ASSUM (SUBST1_TAC o SYM)
1114 THEN REWRITE_TAC[DECIDE “a\/~a”]])
1115
1116
1117val BEFORE_AS_NOT_SWHEN = TAC_PROOF(
1118 ([],“a BEFORE b = \t0. ~(b SWHEN (\t. a t \/ b t)) t0”),
1119 CONV_TAC (X_FUN_EQ_CONV “t0:num”) THEN GEN_TAC
1120 THEN REWRITE_TAC[BEFORE_AS_WHEN,WHEN_AS_NOT_SWHEN]
1121 THEN BETA_TAC THEN REWRITE_TAC[]
1122 THEN CONV_TAC(DEPTH_CONV ETA_CONV)
1123 THEN REWRITE_TAC[])
1124
1125
1126
1127val SUNTIL_AS_SWHEN = TAC_PROOF(
1128 ([],“a SUNTIL b = b SWHEN (\t. a t ==> b t)”),
1129 REWRITE_TAC[SUNTIL_AS_UNTIL,SWHEN_AS_WHEN,UNTIL_AS_WHEN,EVENTUAL,WHEN_SIGNAL]
1130 THEN CONV_TAC FUN_EQ_CONV THEN BETA_TAC THEN X_GEN_TAC “t0:num”
1131 THEN EQ_TAC THEN REPEAT STRIP_TAC THEN RES_TAC THEN ASM_REWRITE_TAC[]
1132 THENL[EXISTS_TAC “t:num” THEN ASM_REWRITE_TAC[], ALL_TAC]
1133 THEN DISJ_CASES_TAC(BETA_RULE
1134 (SPEC“\t:num.a t==>b t”(GEN“b:num->bool”DELTA_CASES)))
1135 THENL[
1136 LEFT_EXISTS_TAC THEN LEFT_NO_FORALL_TAC 3 “d:num”
1137 THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
1138 THEN EXISTS_TAC“d:num” THEN ASM_REWRITE_TAC[],
1139 UNDISCH_HD_TAC
1140 THEN REWRITE_TAC[DECIDE “~(a==>b) = a/\~b”]
1141 THEN DISCH_TAC THEN UNDISCH_NO_TAC 1 THEN ASM_REWRITE_TAC[]])
1142
1143
1144
1145val UNTIL_AS_SWHEN = TAC_PROOF(
1146 ([],“a UNTIL b = \t. (b SWHEN (\t. a t ==> b t)) t \/ ALWAYS a t”),
1147 CONV_TAC (X_FUN_EQ_CONV “t0:num”) THEN GEN_TAC
1148 THEN REWRITE_TAC[SYM SUNTIL_AS_SWHEN,SUNTIL_AS_UNTIL] THEN BETA_TAC
1149 THEN REWRITE_TAC[EVENTUAL,ALWAYS]
1150 THEN EQ_TAC THEN REPEAT STRIP_TAC THEN RES_TAC
1151 THENL[ALL_TAC,ASM_REWRITE_TAC[UNTIL,WATCH_EXISTS]]
1152 THEN ASM_REWRITE_TAC[] THEN RULE_ASSUM_TAC(REWRITE_RULE[UNTIL_SIGNAL])
1153 THEN UNDISCH_HD_TAC THEN STRIP_TAC
1154 THEN DISJ_CASES_TAC DELTA_CASES THEN RES_TAC
1155 THEN ASM_REWRITE_TAC[] THEN DISJ1_TAC THEN LEFT_EXISTS_TAC
1156 THEN EXISTS_TAC“d:num” THEN ASM_REWRITE_TAC[])
1157
1158
1159
1160
1161
1162val SBEFORE_AS_SWHEN = TAC_PROOF(
1163 ([],“a SBEFORE b = ((\t. ~b t) SWHEN (\t.a t \/ b t))”),
1164 CONV_TAC(X_FUN_EQ_CONV “t0:num”) THEN GEN_TAC
1165 THEN REWRITE_TAC[SBEFORE_AS_BEFORE,BEFORE_AS_WHEN,SWHEN_AS_WHEN]
1166 THEN BETA_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]
1167 THENL[
1168 UNDISCH_HD_TAC THEN REWRITE_TAC[EVENTUAL]
1169 THEN BETA_TAC THEN STRIP_TAC
1170 THEN EXISTS_TAC“t:num” THEN ASM_REWRITE_TAC[],
1171 ALL_TAC]
1172 THEN UNDISCH_ALL_TAC THEN REWRITE_TAC[WHEN_SIGNAL,EVENTUAL]
1173 THEN BETA_TAC THEN STRIP_TAC THEN DISCH_TAC
1174 THEN ASSUME_TAC (BETA_RULE(SPEC“\t.a(t+t0)\/b(t+t0)”WOP))
1175 THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[]
1176 THEN STRIP_TAC
1177 THENL[ EXISTS_TAC“n:num” THEN ASM_REWRITE_TAC[], ALL_TAC]
1178 THEN LEFT_NO_FORALL_TAC 3 “n:num”
1179 THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[])
1180
1181
1182
1183(* ************************************************************ *)
1184(* Expressiveness of SUNTIL *)
1185(* ************************************************************ *)
1186
1187
1188val EVENTUAL_AS_SUNTIL = TAC_PROOF(
1189 ([],“EVENTUAL a = (\t.T) SUNTIL a”),
1190 REWRITE_TAC[SUNTIL_AS_UNTIL,UNTIL_SIGNAL]
1191 THEN CONV_TAC(DEPTH_CONV ETA_CONV) THEN REWRITE_TAC[])
1192
1193val ALWAYS_AS_SUNTIL = TAC_PROOF(
1194 ([],“ALWAYS a = \t. ~((\t.T) SUNTIL (\t.~a t)) t”),
1195 ASSUME_TAC(SPEC“\t:num.~a t”
1196 (GEN“a:num->bool”EVENTUAL_AS_SUNTIL))
1197 THEN UNDISCH_HD_TAC THEN BETA_TAC THEN REWRITE_TAC[]
1198 THEN DISCH_TAC THEN POP_ASSUM (SUBST1_TAC o SYM)
1199 THEN CONV_TAC FUN_EQ_CONV THEN GEN_TAC
1200 THEN REWRITE_TAC[EVENTUAL,ALWAYS]
1201 THEN BETA_TAC THEN CONV_TAC(DEPTH_CONV NOT_EXISTS_CONV)
1202 THEN REWRITE_TAC[])
1203
1204
1205val UNTIL_AS_SUNTIL = TAC_PROOF(
1206 ([],“a UNTIL b = \t. (a SUNTIL b) t \/ ALWAYS a t”),
1207 CONV_TAC (X_FUN_EQ_CONV “t0:num”) THEN GEN_TAC
1208 THEN REWRITE_TAC[SUNTIL_SIGNAL,UNTIL_SIGNAL,ALWAYS_SIGNAL] THEN BETA_TAC
1209 THEN EQ_TAC THEN REPEAT STRIP_TAC THEN RES_TAC THEN ASM_REWRITE_TAC[]
1210 THENL[
1211 DISJ_CASES_TAC DELTA_CASES
1212 THENL[
1213 LEFT_EXISTS_TAC THEN LEFT_NO_FORALL_TAC 1 “d:num”
1214 THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
1215 THEN DISJ1_TAC THEN EXISTS_TAC “d:num”
1216 THEN ASM_REWRITE_TAC[] THEN GEN_TAC THEN DISCH_TAC THEN RES_TAC
1217 THEN ASM_REWRITE_TAC[],
1218 DISJ2_TAC THEN POP_NO_ASSUM 2 MATCH_MP_TAC
1219 THEN ASM_REWRITE_TAC[]],
1220 MY_MP_TAC “delta=(d:num)”
1221 THENL[
1222 DISJ_CASES_TAC(SPECL[“d:num”,“delta:num”]LESS_CASES)
1223 THENL[RES_TAC,ALL_TAC]
1224 THEN UNDISCH_HD_TAC THEN REWRITE_TAC[LESS_OR_EQ] THEN STRIP_TAC
1225 THEN RES_TAC,
1226 DISCH_TAC]
1227 THEN UNDISCH_NO_TAC 6 THEN POP_ASSUM SUBST1_TAC THEN DISCH_TAC
1228 THEN RES_TAC])
1229
1230
1231val SWHEN_AS_SUNTIL = TAC_PROOF(
1232 ([],“a SWHEN b = (\t. ~b t) SUNTIL (\t. a t /\ b t)”),
1233 REWRITE_TAC[SUNTIL_AS_SWHEN] THEN BETA_TAC
1234 THEN REWRITE_TAC[DECIDE “(~b ==> a /\ b) = b”]
1235 THEN CONV_TAC FUN_EQ_CONV THEN BETA_TAC THEN REWRITE_TAC[SWHEN_SIGNAL]
1236 THEN GEN_TAC THEN BETA_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC
1237 THEN EXISTS_TAC “delta:num” THEN ASM_REWRITE_TAC[])
1238
1239val WHEN_AS_SUNTIL = prove(
1240 “a WHEN b =
1241 \t. ((\t. ~b t) SUNTIL (\t. a t /\ b t)) t \/ ALWAYS (\t. ~b t) t”,
1242 REWRITE_TAC[SYM SWHEN_AS_SUNTIL,WHEN_AS_SWHEN])
1243
1244
1245val BEFORE_AS_SUNTIL = TAC_PROOF(
1246 ([],“a BEFORE b = \t. ~((\t. ~a t) SUNTIL b) t”),
1247 CONV_TAC (X_FUN_EQ_CONV “t0:num”) THEN GEN_TAC
1248 THEN REWRITE_TAC[SUNTIL_AS_UNTIL,BEFORE_AS_UNTIL]
1249 THEN REWRITE_TAC[DE_MORGAN_THM,ALWAYS,EVENTUAL] THEN BETA_TAC
1250 THEN REWRITE_TAC[DE_MORGAN_THM] THEN CONV_TAC(DEPTH_CONV NOT_EXISTS_CONV)
1251 THEN TAUT_TAC)
1252
1253
1254val SBEFORE_AS_SUNTIL = TAC_PROOF(
1255 ([],“a SBEFORE b = \t0. ~((\t. ~a t) SUNTIL b) t0 /\ EVENTUAL a t0”),
1256 CONV_TAC (X_FUN_EQ_CONV “t0:num”) THEN GEN_TAC
1257 THEN REWRITE_TAC[SBEFORE_AS_BEFORE,BEFORE_AS_SUNTIL]
1258 THEN BETA_TAC THEN TAUT_TAC)
1259
1260
1261(* ************************************************************ *)
1262(* Expressiveness of SBEFORE *)
1263(* ************************************************************ *)
1264
1265val EVENTUAL_AS_SBEFORE = TAC_PROOF(
1266 ([],“EVENTUAL b = (b SBEFORE (\t.F))”),
1267 CONV_TAC(X_FUN_EQ_CONV“t0:num”) THEN BETA_TAC THEN GEN_TAC
1268 THEN ONCE_REWRITE_TAC[DECIDE “(a=b) = (~a= ~b)”]
1269 THEN REWRITE_TAC[SBEFORE_AS_UNTIL] THEN BETA_TAC
1270 THEN REWRITE_TAC[SYM ALWAYS_AS_UNTIL]
1271 THEN REWRITE_TAC[ALWAYS,EVENTUAL] THEN BETA_TAC
1272 THEN CONV_TAC(DEPTH_CONV(NOT_EXISTS_CONV))
1273 THEN REWRITE_TAC[])
1274
1275
1276val ALWAYS_AS_SBEFORE = TAC_PROOF(
1277 ([],“ALWAYS b = \t0. ~((\t.~b t) SBEFORE(\t.F)) t0”),
1278 CONV_TAC(X_FUN_EQ_CONV“t0:num”) THEN GEN_TAC THEN BETA_TAC
1279 THEN ONCE_REWRITE_TAC[DECIDE “(a=b) = (~a= ~b)”]
1280 THEN REWRITE_TAC[SBEFORE_AS_UNTIL] THEN BETA_TAC
1281 THEN REWRITE_TAC[SYM ALWAYS_AS_UNTIL]
1282 THEN CONV_TAC(DEPTH_CONV ETA_CONV)
1283 THEN REWRITE_TAC[])
1284
1285
1286
1287val WHEN_AS_SBEFORE = prove(
1288 “(a WHEN b) = \t0. (b SBEFORE (\t. ~a t /\ b t)) t0 \/ ALWAYS(\t. ~b t) t0”,
1289 CONV_TAC(X_FUN_EQ_CONV“t0:num”) >> GEN_TAC >> BETA_TAC
1290 >> ONCE_REWRITE_TAC[DECIDE “(a=b) = (~a= ~b)”]
1291 >> ASSUME_TAC (REWRITE_RULE[](BETA_RULE
1292 (SPEC“\t:num.~a t”(GEN“a:num->bool”SWHEN_AS_NOT_WHEN))))
1293 >> UNDISCH_HD_TAC >> CONV_TAC(DEPTH_CONV ETA_CONV)
1294 >> DISCH_TAC >> POP_ASSUM (SUBST1_TAC o SYM)
1295 >> REWRITE_TAC[SBEFORE_AS_WHEN] >> BETA_TAC
1296 >> REWRITE_TAC[DE_MORGAN_THM]
1297 >> REWRITE_TAC[DECIDE “(b\/a/\b) = b”]
1298 >> CONV_TAC(DEPTH_CONV ETA_CONV)
1299 >> ASSUME_TAC
1300 (REWRITE_RULE[](
1301 BETA_RULE
1302 (SPEC“\t:num. ~a t /\b t”(GEN“a:num->bool”SWHEN_AS_NOT_WHEN))))
1303 >> UNDISCH_HD_TAC >> CONV_TAC(DEPTH_CONV ETA_CONV)
1304 >> REWRITE_TAC[DE_MORGAN_THM]
1305 >> DISCH_TAC >> POP_ASSUM (SUBST1_TAC o SYM)
1306 >> MY_MP_TAC “~(ALWAYS (\t. ~(b t)) t0) = EVENTUAL b t0”
1307 THENL[
1308 REWRITE_TAC[EVENTUAL,ALWAYS]
1309 >> CONV_TAC(DEPTH_CONV NOT_FORALL_CONV)
1310 >> BETA_TAC >> REWRITE_TAC[],
1311 DISCH_TAC]
1312 >> POP_ASSUM SUBST1_TAC
1313 >> REWRITE_TAC[DECIDE “(b\/~a)/\a = b/\a”]
1314 >> REWRITE_TAC[SWHEN_AS_WHEN] >> BETA_TAC
1315 >> REWRITE_TAC[DECIDE “(a/\b)/\b = a/\b”]
1316 >> MATCH_MP_TAC (DECIDE “(a=c) ==> (a/\b = c/\b)”)
1317 >> REWRITE_TAC[WHEN_SIGNAL] >> BETA_TAC
1318 >> EQ_TAC >> REPEAT STRIP_TAC >> ASM_REWRITE_TAC[]
1319 >> LEFT_NO_FORALL_TAC 3 “delta:num”
1320 >> UNDISCH_HD_TAC >> ASM_REWRITE_TAC[])
1321
1322
1323val UNTIL_AS_SBEFORE = TAC_PROOF(
1324 ([],“a UNTIL b = \t0.~((\t.~a t) SBEFORE b) t0”),
1325 CONV_TAC(X_FUN_EQ_CONV“t0:num”) THEN GEN_TAC THEN BETA_TAC
1326 THEN ONCE_REWRITE_TAC[DECIDE “(a=b) = (~a= ~b)”]
1327 THEN ASSUME_TAC (REWRITE_RULE[](BETA_RULE
1328 (SPEC“\t:num.~a t”(GEN“a:num->bool”SBEFORE_AS_UNTIL))))
1329 THEN POP_ASSUM REWRITE1_TAC
1330 THEN BETA_TAC THEN CONV_TAC(DEPTH_CONV ETA_CONV)
1331 THEN REWRITE_TAC[])
1332
1333
1334
1335val BEFORE_AS_SBEFORE = TAC_PROOF(
1336 ([],“a BEFORE b = \t0. (a SBEFORE b) t0 \/ ALWAYS (\t.~b t) t0”),
1337 CONV_TAC(X_FUN_EQ_CONV“t0:num”) THEN GEN_TAC THEN BETA_TAC
1338 THEN REWRITE_TAC[BEFORE_AS_SUNTIL,SBEFORE_AS_SUNTIL]
1339 THEN BETA_TAC THEN REWRITE_TAC[SUNTIL_SIGNAL,EVENTUAL,ALWAYS]
1340 THEN BETA_TAC THEN CONV_TAC(DEPTH_CONV NOT_EXISTS_CONV)
1341 THEN REWRITE_TAC[DECIDE “~(a/\b) = a ==> ~b”]
1342 THEN EQ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[]
1343 THEN REWRITE_TAC[DECIDE “a\/b = ~a ==> b”]
1344 THEN CONV_TAC(DEPTH_CONV NOT_EXISTS_CONV)
1345 THEN DISCH_TAC THEN POP_ASSUM (fn x=> RULE_ASSUM_TAC(REWRITE_RULE[x]))
1346 THEN MATCH_MP_TAC
1347 (BETA_RULE(SPEC“\t.~b(t+t0)” COMPLETE_INDUCTION))
1348
1349 THEN ASM_REWRITE_TAC[]);
1350
1351
1352
1353val SWHEN_AS_SBEFORE = TAC_PROOF(
1354 ([],“(a SWHEN b) = (b SBEFORE (\t.~a t/\b t))”),
1355 CONV_TAC(X_FUN_EQ_CONV“t0:num”) THEN GEN_TAC THEN BETA_TAC
1356 THEN REWRITE_TAC[SWHEN_AS_WHEN,SBEFORE_AS_WHEN]
1357 THEN BETA_TAC
1358 THEN REWRITE_TAC[DECIDE “b\/~a/\b= b”]
1359 THEN CONV_TAC(DEPTH_CONV ETA_CONV)
1360 THEN MATCH_MP_TAC (DECIDE “(a=c) ==> (a/\b = c/\b)”)
1361 THEN REWRITE_TAC[WHEN_SIGNAL] THEN BETA_TAC
1362 THEN EQ_TAC THEN REPEAT STRIP_TAC
1363 THENL[
1364 LEFT_NO_FORALL_TAC 3 “delta:num”
1365 THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[],
1366 LEFT_NO_FORALL_TAC 2 “delta:num”
1367 THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[]])
1368
1369
1370
1371val SUNTIL_AS_SBEFORE = TAC_PROOF(
1372 ([],“(a SUNTIL b) = \t0. ~((\t.~a t) SBEFORE b) t0 /\ EVENTUAL b t0”),
1373 let val thm1 = GEN“a:num->bool” SBEFORE_AS_UNTIL
1374 val thm2 = BETA_RULE(SPEC“\t:num.~a t”thm1)
1375 val thm3 = (CONV_RULE(DEPTH_CONV ETA_CONV))(REWRITE_RULE[]thm2)
1376 in
1377 SUBST1_TAC thm3 THEN CONV_TAC(X_FUN_EQ_CONV“t0:num”)
1378 THEN BETA_TAC THEN GEN_TAC THEN REWRITE_TAC[DE_MORGAN_THM]
1379 THEN REWRITE_TAC[SUNTIL_AS_UNTIL] THEN BETA_TAC THEN REWRITE_TAC[]
1380 end)
1381
1382
1383
1384(* ************************************************************ *)
1385(* Homomorphism of the NEXT operator *)
1386(* ************************************************************ *)
1387
1388
1389val NOT_NEXT = TAC_PROOF(
1390 ([],“!P. NEXT (\t.~P t) = \t. ~NEXT P t”),
1391 GEN_TAC THEN REWRITE_TAC[NEXT] THEN BETA_TAC THEN REWRITE_TAC[])
1392
1393val AND_NEXT = TAC_PROOF(
1394 ([],“!Q P. NEXT (\t.P t /\ Q t) = \t. NEXT P t /\ NEXT Q t”),
1395 REPEAT GEN_TAC THEN REWRITE_TAC[NEXT]
1396 THEN BETA_TAC THEN REWRITE_TAC[])
1397
1398val OR_NEXT = TAC_PROOF(
1399 ([],“!Q P. NEXT (\t.P t \/ Q t) = \t. NEXT P t \/ NEXT Q t”),
1400 REPEAT GEN_TAC THEN REWRITE_TAC[NEXT]
1401 THEN BETA_TAC THEN REWRITE_TAC[])
1402
1403val IMP_NEXT = TAC_PROOF(
1404 ([],“!Q P. NEXT (\t.P t ==> Q t) = \t. NEXT P t ==> NEXT Q t”),
1405 REPEAT GEN_TAC THEN REWRITE_TAC[NEXT]
1406 THEN BETA_TAC THEN REWRITE_TAC[])
1407
1408val EQUIV_NEXT = TAC_PROOF(
1409 ([],“!Q P. NEXT (\t.P t = Q t) = \t. NEXT P t = NEXT Q t”),
1410 REPEAT GEN_TAC THEN REWRITE_TAC[NEXT]
1411 THEN BETA_TAC THEN REWRITE_TAC[])
1412
1413
1414val ALWAYS_NEXT = TAC_PROOF(
1415 ([],“!a. NEXT (ALWAYS a) = ALWAYS(NEXT a)”),
1416 GEN_TAC THEN REWRITE_TAC[NEXT,ALWAYS]
1417 THEN CONV_TAC (X_FUN_EQ_CONV “t0:num”)
1418 THEN BETA_TAC
1419 THEN REWRITE_TAC[ALWAYS] THEN BETA_TAC
1420 THEN REWRITE_TAC[ADD_CLAUSES])
1421
1422
1423val EVENTUAL_NEXT = TAC_PROOF(
1424 ([],“!a. NEXT (EVENTUAL a) = EVENTUAL(NEXT a)”),
1425 GEN_TAC THEN REWRITE_TAC[NEXT,EVENTUAL]
1426 THEN CONV_TAC (X_FUN_EQ_CONV “t0:num”)
1427 THEN BETA_TAC
1428 THEN REWRITE_TAC[EVENTUAL] THEN BETA_TAC
1429 THEN REWRITE_TAC[ADD_CLAUSES])
1430
1431val WHEN_NEXT = TAC_PROOF(
1432 ([],“!a b.(NEXT (a WHEN b)) = (NEXT a) WHEN (NEXT b)”),
1433 REPEAT GEN_TAC
1434 THEN CONV_TAC (X_FUN_EQ_CONV “t0:num”) THEN GEN_TAC
1435 THEN REWRITE_TAC[NEXT,WHEN,WATCH] THEN BETA_TAC
1436 THEN REWRITE_TAC[ADD_CLAUSES]
1437 THEN EQ_TAC THEN STRIP_TAC
1438 THENL[EXISTS_TAC “\t.q(SUC t):bool”,
1439 EXISTS_TAC “\t.q(PRE t):bool”]
1440 THEN BETA_TAC
1441 THEN ASM_REWRITE_TAC[PRE])
1442
1443
1444val UNTIL_NEXT = TAC_PROOF(
1445 ([],“!a b.(NEXT (a UNTIL b)) = (NEXT a) UNTIL (NEXT b)”),
1446 REPEAT GEN_TAC
1447 THEN CONV_TAC (X_FUN_EQ_CONV “t0:num”) THEN GEN_TAC
1448 THEN REWRITE_TAC[NEXT,UNTIL,WATCH] THEN BETA_TAC
1449 THEN REWRITE_TAC[ADD_CLAUSES]
1450 THEN EQ_TAC THEN STRIP_TAC
1451 THENL[EXISTS_TAC “\t.q(SUC t):bool”,
1452 EXISTS_TAC “\t.q(PRE t):bool”]
1453 THEN BETA_TAC
1454 THEN ASM_REWRITE_TAC[PRE])
1455
1456val BEFORE_NEXT = TAC_PROOF(
1457 ([],“!a b.(NEXT (a BEFORE b)) = (NEXT a) BEFORE (NEXT b)”),
1458 REPEAT GEN_TAC
1459 THEN CONV_TAC (X_FUN_EQ_CONV “t0:num”) THEN GEN_TAC
1460 THEN REWRITE_TAC[BEFORE_AS_WHEN,WHEN_NEXT,NOT_NEXT,OR_NEXT])
1461
1462val SWHEN_NEXT = TAC_PROOF(
1463 ([],“!a b.(NEXT (a SWHEN b)) = (NEXT a) SWHEN (NEXT b)”),
1464 REWRITE_TAC[SWHEN_AS_WHEN,AND_NEXT,EVENTUAL_NEXT,WHEN_NEXT])
1465
1466val SUNTIL_NEXT = TAC_PROOF(
1467 ([],“!a b.(NEXT (a SUNTIL b)) = (NEXT a) SUNTIL (NEXT b)”),
1468 REWRITE_TAC[SUNTIL_AS_UNTIL,AND_NEXT,EVENTUAL_NEXT,UNTIL_NEXT])
1469
1470val SBEFORE_NEXT = TAC_PROOF(
1471 ([],“!a b.(NEXT (a SBEFORE b)) = (NEXT a) SBEFORE (NEXT b)”),
1472 REPEAT GEN_TAC
1473 THEN CONV_TAC (X_FUN_EQ_CONV “t0:num”) THEN GEN_TAC
1474 THEN REWRITE_TAC[SBEFORE_AS_BEFORE,AND_NEXT,BEFORE_NEXT,EVENTUAL_NEXT])
1475
1476
1477(* ************************************************************ *)
1478(* Recursion Theorems *)
1479(* ************************************************************ *)
1480
1481
1482val NEXT2 = prove(``NEXT P x = P (SUC x)``,
1483 REWRITE_TAC [NEXT] THEN BETA_TAC THEN REWRITE_TAC []);
1484
1485
1486val ALWAYS_REC = TAC_PROOF(
1487 ([],“ALWAYS P t0 = (P t0 /\ NEXT (ALWAYS P) t0)”),
1488 REWRITE_TAC [NEXT2,ALWAYS] THEN
1489 REWRITE_TAC[ADD_CLAUSES]
1490 THEN EQ_TAC THEN REPEAT STRIP_TAC
1491 THENL[
1492 LEFT_FORALL_TAC “0” THEN UNDISCH_HD_TAC
1493 THEN REWRITE_TAC[ADD_CLAUSES],
1494 LEFT_FORALL_TAC “SUC t” THEN UNDISCH_HD_TAC
1495 THEN REWRITE_TAC[ADD_CLAUSES],
1496 SPEC_TAC(“t:num”,“t:num”) THEN INDUCT_TAC
1497 THEN ASM_REWRITE_TAC[ADD_CLAUSES]])
1498
1499
1500val EVENTUAL_ALWAYS_THM = TAC_PROOF(
1501 ([],“EVENTUAL P = \t.~ALWAYS (\t.~P t) t”),
1502 CONV_TAC (X_FUN_EQ_CONV “t0:num”) THEN GEN_TAC
1503 THEN REWRITE_TAC[EVENTUAL,ALWAYS] THEN BETA_TAC
1504 THEN CONV_TAC(DEPTH_CONV NOT_FORALL_CONV)
1505 THEN REWRITE_TAC[])
1506
1507
1508
1509val EVENTUAL_REC = TAC_PROOF(
1510 ([],“EVENTUAL P t0 = (P t0 \/ NEXT (EVENTUAL P) t0)”),
1511 PURE_ONCE_REWRITE_TAC[TAC_PROOF(([],“(a=b) = (~a= ~b)”),
1512 BOOL_CASES_TAC “a:bool” THEN REWRITE_TAC[])]
1513 THEN REWRITE_TAC[DE_MORGAN_THM,EVENTUAL_ALWAYS_THM]
1514 THEN BETA_TAC
1515 THEN SUBST1_TAC(SPECL[“t0:num”,“(\t:num.~P t)”](GEN_ALL ALWAYS_REC))
1516 THEN BETA_TAC THEN BETA_TAC
1517 THEN SUBST1_TAC(SPEC“ALWAYS (\t. ~(P t))”NOT_NEXT)
1518 THEN BETA_TAC THEN REWRITE_TAC[])
1519
1520
1521val WATCH_REC = TAC_PROOF(
1522 ([],“(q WATCH b) t0 =
1523 ~q t0 /\ (if b t0 then (NEXT (ALWAYS q) t0)
1524 else (NEXT (q WATCH b) t0))”),
1525 PURE_REWRITE_TAC[WATCH,NEXT,ALWAYS]
1526 THEN BETA_TAC THEN EQ_TAC THEN STRIP_TAC
1527 THENL[
1528 ASM_REWRITE_TAC[] THEN COND_CASES_TAC
1529 THENL[
1530 REWRITE_TAC[ADD_CLAUSES] THEN INDUCT_TAC
1531 THEN ASM_REWRITE_TAC[] THEN ASM_REWRITE_TAC[ADD_CLAUSES],
1532 REWRITE_TAC[EQT_ELIM(ARITH_CONV“SUC(t'+SUC t0) = SUC((SUC t')+t0)”)]
1533 THEN ASM_REWRITE_TAC[ADD_CLAUSES]
1534 THEN LEFT_NO_FORALL_TAC 1 “0”
1535 THEN RULE_ASSUM_TAC (REWRITE_RULE[ADD_CLAUSES])
1536 THEN ASM_REWRITE_TAC[]],
1537 ASM_REWRITE_TAC[]
1538 THEN RULE_ASSUM_TAC (REWRITE_RULE[EQT_ELIM
1539 (ARITH_CONV“SUC(t'+SUC t0) = SUC((SUC t')+t0)”)])
1540 THEN DISJ_CASES_TAC (SPEC“(b:num->bool) t0” BOOL_CASES_AX)
1541 THEN POP_ASSUM (fn x=> RULE_ASSUM_TAC (REWRITE_RULE[x])
1542 THEN REWRITE_TAC[x] THEN ASSUME_TAC x)
1543 THENL[
1544 RULE_ASSUM_TAC(REWRITE_RULE[ADD_CLAUSES])
1545 THEN INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES]
1546 THEN POP_ASSUM (SUBST1_TAC o SYM) THEN ASM_REWRITE_TAC[],
1547 INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES]]])
1548
1549
1550val WHEN_REC = TAC_PROOF(
1551 ([],“(a WHEN b) t0 = if b t0 then a t0 else NEXT (a WHEN b) t0”),
1552 PURE_REWRITE_TAC[NEXT2,WHEN_SIGNAL] THEN BETA_TAC
1553 THEN DISJ_CASES_TAC(SPEC“(b:num->bool) t0” BOOL_CASES_AX)
1554 THEN ASM_REWRITE_TAC[]
1555 THENL[
1556 EQ_TAC THEN STRIP_TAC
1557 THENL[
1558 LEFT_FORALL_TAC “0”
1559 THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[NOT_LESS_0,ADD_CLAUSES],
1560 GEN_TAC THEN STRIP_TAC
1561 THEN RULE_ASSUM_TAC((CONV_RULE(ONCE_DEPTH_CONV CONTRAPOS_CONV))
1562 handle _=>(fn x=> x))
1563 THEN LEFT_NO_FORALL_TAC 1 “0”
1564 THEN UNDISCH_HD_TAC
1565 THEN ASM_REWRITE_TAC[ADD_CLAUSES]
1566 THEN REWRITE_TAC[NOT_LESS,LESS_EQ_0]
1567 THEN DISCH_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES]],
1568 REWRITE_TAC[ADD_CLAUSES]
1569 THEN EQ_TAC THEN STRIP_TAC
1570 THENL[
1571 GEN_TAC THEN LEFT_FORALL_TAC “SUC delta”
1572 THEN STRIP_TAC
1573 THEN RULE_ASSUM_TAC(REWRITE_RULE[ADD_CLAUSES])
1574 THEN POP_NO_ASSUM 2 MATCH_MP_TAC
1575 THEN ASM_REWRITE_TAC[] THEN INDUCT_TAC
1576 THEN ASM_REWRITE_TAC[ADD_CLAUSES,LESS_MONO_EQ],
1577 INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES,NOT_LESS_0]
1578 THEN LEFT_NO_FORALL_TAC 1 “delta:num”
1579 THEN STRIP_TAC THEN POP_NO_ASSUM 2 MATCH_MP_TAC
1580 THEN ASM_REWRITE_TAC[]
1581 THEN GEN_TAC THEN LEFT_NO_FORALL_TAC 1 “SUC t”
1582 THEN UNDISCH_HD_TAC THEN REWRITE_TAC[LESS_MONO_EQ,ADD_CLAUSES]]])
1583
1584
1585
1586val UNTIL_REC = TAC_PROOF(
1587 ([],“(a UNTIL b) t0 = (~b t0 ==> a t0 /\ NEXT (a UNTIL b) t0)”),
1588 PURE_REWRITE_TAC[UNTIL_AS_WHEN,NEXT]
1589 THEN SUBST1_TAC(SPECL[“t0:num”,“\t:num. a t ==> b t”,“b:num->bool”]
1590 (GEN_ALL WHEN_REC))
1591 THEN REWRITE_TAC[NEXT] THEN BETA_TAC
1592 THEN MAP_EVERY BOOL_CASES_TAC [“(b:num->bool) t0”,“(a:num->bool) t0”]
1593 THEN REWRITE_TAC[])
1594
1595
1596val BEFORE_REC = TAC_PROOF(
1597 ([],“(a BEFORE b) t0 = ~b t0 /\ (a t0 \/ NEXT (a BEFORE b) t0)”),
1598 REWRITE_TAC[BEFORE_AS_WHEN_UNTIL]
1599 THEN CONV_TAC(RATOR_CONV(REWRITE_CONV[WHEN_REC,UNTIL_REC]))
1600 THEN BETA_TAC THEN REWRITE_TAC[AND_NEXT] THEN BETA_TAC
1601 THEN TAUT_TAC)
1602
1603
1604val SWHEN_REC = TAC_PROOF(
1605 ([],“(a SWHEN b) t0 = (if (b t0) then (a t0) else (NEXT (a SWHEN b) t0))”),
1606 REWRITE_TAC[SWHEN_AS_WHEN,AND_NEXT]
1607 THEN CONV_TAC(RATOR_CONV(REWRITE_CONV[WHEN_REC,EVENTUAL_REC]))
1608 THEN BETA_TAC THEN TAUT_TAC)
1609
1610
1611val SUNTIL_REC = TAC_PROOF(
1612 ([],“(a SUNTIL b) t0 = ~(b t0) ==> a t0 /\ NEXT (a SUNTIL b) t0”),
1613 REWRITE_TAC[SUNTIL_AS_UNTIL,AND_NEXT]
1614 THEN CONV_TAC(RATOR_CONV(REWRITE_CONV[UNTIL_REC,EVENTUAL_REC]))
1615 THEN BETA_TAC THEN TAUT_TAC)
1616
1617
1618val SBEFORE_REC = TAC_PROOF(
1619 ([],“(a SBEFORE b) t0 = ~b t0 /\ (a t0 \/ NEXT (a SBEFORE b) t0)”),
1620 REWRITE_TAC[SBEFORE_AS_SWHEN,AND_NEXT]
1621 THEN CONV_TAC(RATOR_CONV(REWRITE_CONV[SWHEN_REC,EVENTUAL_REC]))
1622 THEN BETA_TAC THEN TAUT_TAC)
1623
1624
1625(*---------------------------------------------------------------------------
1626 Useful simplifications
1627 ---------------------------------------------------------------------------*)
1628
1629val WHEN_SIMP = TAC_PROOF(
1630 ([],“ ( ((\t.F) WHEN b) = ALWAYS(\t.~b t)) /\
1631 ( ((\t.T) WHEN b) = \t.T) /\
1632 ( (a WHEN (\t.F)) = \t.T) /\
1633 ( (a WHEN (\t.T)) = \t. a t) /\
1634 ( (a WHEN a) = \t.T)”),
1635 CONV_TAC(DEPTH_CONV(X_FUN_EQ_CONV“t0:num”))
1636 THEN REWRITE_TAC[WHEN_SIGNAL,ALWAYS]
1637 THEN BETA_TAC THEN REWRITE_TAC[DE_MORGAN_THM]
1638 THEN CONV_TAC(DEPTH_CONV NOT_FORALL_CONV)
1639 THEN REWRITE_TAC[DECIDE “~(a==>~b) = a/\b”]
1640 THEN MY_MP_TAC “!delta.(!t.~(t<delta)) = (delta=0)”
1641 THENL[
1642 GEN_TAC THEN REWRITE_TAC[NOT_LESS] THEN EQ_TAC THEN REPEAT STRIP_TAC
1643 THEN ASM_REWRITE_TAC[] THENL[LEFT_FORALL_TAC “0”,ALL_TAC]
1644 THEN UNDISCH_HD_TAC THEN CONV_TAC ARITH_CONV,
1645 DISCH_TAC]
1646 THEN POP_ASSUM REWRITE1_TAC
1647 THEN REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC
1648 THENL[
1649 UNDISCH_NO_TAC 1 THEN REWRITE_TAC[]
1650 THEN DISJ_CASES_TAC DELTA_CASES THEN RES_TAC
1651 THEN LEFT_EXISTS_TAC
1652 THEN CONV_TAC(DEPTH_CONV NOT_FORALL_CONV)
1653 THEN REWRITE_TAC[DE_MORGAN_THM] THEN EXISTS_TAC“d:num”
1654 THEN ASM_REWRITE_TAC[] THEN CONV_TAC(DEPTH_CONV NOT_EXISTS_CONV)
1655 THEN ASM_REWRITE_TAC[DECIDE “~(a/\b) = a==>~b”],
1656 ASM_REWRITE_TAC[],
1657 LEFT_FORALL_TAC “0” THEN UNDISCH_HD_TAC
1658 THEN REWRITE_TAC[ADD_CLAUSES],
1659 ASM_REWRITE_TAC[ADD_CLAUSES]])
1660
1661
1662
1663
1664val UNTIL_SIMP = TAC_PROOF(
1665 ([],“ ( ((\t.F) UNTIL b) = \t.b t) /\
1666 ( ((\t.T) UNTIL b) = \t.T) /\
1667 ( (a UNTIL (\t.F)) = ALWAYS a) /\
1668 ( (a UNTIL (\t.T)) = \t. T) /\
1669 ( (a UNTIL a) = \t.a t)”),
1670 CONV_TAC(DEPTH_CONV(X_FUN_EQ_CONV“t0:num”))
1671 THEN REWRITE_TAC[UNTIL_AS_WHEN,WHEN_SIMP] THEN BETA_TAC
1672 THEN CONV_TAC(DEPTH_CONV ETA_CONV)
1673 THEN REWRITE_TAC[WHEN_SIMP]
1674 THEN CONV_TAC(DEPTH_CONV ETA_CONV)
1675 THEN REWRITE_TAC[])
1676
1677
1678
1679
1680
1681val BEFORE_SIMP = TAC_PROOF(
1682 ([],“ ( ((\t.F) BEFORE b) = ALWAYS (\t.~b t)) /\
1683 ( ((\t.T) BEFORE b) = \t.~ b t) /\
1684 ( (a BEFORE (\t.F)) = \t. T) /\
1685 ( (a BEFORE (\t.T)) = \t. F) /\
1686 ( (a BEFORE a) = ALWAYS (\t.~a t))”),
1687 CONV_TAC(DEPTH_CONV(X_FUN_EQ_CONV“t0:num”))
1688 THEN REWRITE_TAC[BEFORE_AS_WHEN,WHEN_SIMP] THEN BETA_TAC
1689 THEN REWRITE_TAC[WHEN_SIGNAL,ALWAYS] THEN BETA_TAC
1690 THEN REWRITE_TAC[DECIDE “(a/\b==>~b) = a==>~b”]
1691 THEN REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THEN RES_TAC
1692 THENL[
1693 DISJ_CASES_TAC DELTA_CASES THEN RES_TAC
1694 THEN LEFT_EXISTS_TAC THEN LEFT_NO_FORALL_TAC 2 “d:num”
1695 THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[],
1696 DISJ_CASES_TAC(SPEC“a:num->bool”(GEN“b:num->bool”DELTA_CASES))
1697 THEN RES_TAC THEN LEFT_EXISTS_TAC THEN LEFT_NO_FORALL_TAC 2 “d:num”
1698 THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[]])
1699
1700
1701
1702
1703
1704val SWHEN_SIMP = TAC_PROOF(
1705 ([],“ ( ((\t.F) SWHEN b) = \t.F) /\
1706 ( ((\t.T) SWHEN b) = EVENTUAL b) /\
1707 ( (a SWHEN (\t.F)) = \t.F) /\
1708 ( (a SWHEN (\t.T)) = \t. a t) /\
1709 ( (a SWHEN a) = EVENTUAL a)”),
1710 CONV_TAC(DEPTH_CONV(X_FUN_EQ_CONV“t0:num”))
1711 THEN REWRITE_TAC[SWHEN_AS_WHEN,WHEN_SIMP] THEN BETA_TAC
1712 THEN REWRITE_TAC[EVENTUAL,ALWAYS] THEN BETA_TAC
1713 THEN REWRITE_TAC[DE_MORGAN_THM]
1714 THEN CONV_TAC(DEPTH_CONV NOT_FORALL_CONV)
1715 THEN REWRITE_TAC[DECIDE “b\/~b”])
1716
1717
1718
1719
1720val SUNTIL_SIMP = TAC_PROOF(
1721 ([],“ ( ((\t.F) SUNTIL b) = \t.b t) /\
1722 ( ((\t.T) SUNTIL b) = EVENTUAL b) /\
1723 ( (a SUNTIL (\t.F)) = \t.F) /\
1724 ( (a SUNTIL (\t.T)) = \t.T) /\
1725 ( (a SUNTIL a) = \t. a t)”),
1726 CONV_TAC(DEPTH_CONV(X_FUN_EQ_CONV“t0:num”))
1727 THEN REWRITE_TAC[SUNTIL_AS_UNTIL,UNTIL_SIMP] THEN BETA_TAC
1728 THEN REWRITE_TAC[EVENTUAL,ALWAYS] THEN BETA_TAC
1729 THEN MY_MP_TAC“!b.(!t0. b t0 /\ (?t. b(t+t0)) = b t0)”
1730 THENL[
1731 REPEAT GEN_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC
1732 THEN ASM_REWRITE_TAC[] THEN EXISTS_TAC“0”
1733 THEN ASM_REWRITE_TAC[ADD_CLAUSES],
1734 DISCH_TAC]
1735 THEN ASM_REWRITE_TAC[])
1736
1737
1738
1739
1740val SBEFORE_SIMP = TAC_PROOF(
1741 ([],“ ( ((\t.F) SBEFORE b) = \t.F) /\
1742 ( ((\t.T) SBEFORE b) = \t.~b t) /\
1743 ( (a SBEFORE (\t.F)) = EVENTUAL a) /\
1744 ( (a SBEFORE (\t.T)) = \t.F) /\
1745 ( (a SBEFORE a) = \t.F)”),
1746 CONV_TAC(DEPTH_CONV(X_FUN_EQ_CONV“t0:num”))
1747 THEN REWRITE_TAC[SBEFORE_AS_BEFORE,BEFORE_SIMP] THEN BETA_TAC
1748 THEN REWRITE_TAC[EVENTUAL,ALWAYS] THEN BETA_TAC
1749 THEN REWRITE_TAC[DE_MORGAN_THM]
1750 THEN CONV_TAC(DEPTH_CONV NOT_FORALL_CONV)
1751 THEN REWRITE_TAC[DECIDE “b\/~b”])
1752
1753
1754
1755
1756
1757val WHEN_EVENT = TAC_PROOF(
1758 ([],“a WHEN b = (\t.a t /\ b t) WHEN b”),
1759 CONV_TAC(X_FUN_EQ_CONV“t0:num”) THEN GEN_TAC
1760 THEN REWRITE_TAC[WHEN,WATCH] THEN BETA_TAC THEN EQ_TAC
1761 THEN REPEAT STRIP_TAC THEN EXISTS_TAC“q:num->bool”
1762 THEN ASM_REWRITE_TAC[] THEN GEN_TAC
1763 THEN LEFT_FORALL_TAC“t:num” THEN UNDISCH_HD_TAC
1764 THEN TAUT_TAC)
1765
1766val UNTIL_EVENT = TAC_PROOF(
1767 ([],“a UNTIL b = (\t.a t /\ ~b t) UNTIL b”),
1768 CONV_TAC(X_FUN_EQ_CONV“t0:num”) THEN GEN_TAC
1769 THEN REWRITE_TAC[UNTIL,WATCH] THEN BETA_TAC THEN EQ_TAC
1770 THEN REPEAT STRIP_TAC THEN EXISTS_TAC“q:num->bool”
1771 THEN ASM_REWRITE_TAC[] THEN GEN_TAC
1772 THEN LEFT_FORALL_TAC“t:num” THEN UNDISCH_HD_TAC
1773 THEN TAUT_TAC)
1774
1775val BEFORE_EVENT = TAC_PROOF(
1776 ([],“a BEFORE b = (\t.a t /\ ~b t) BEFORE b”),
1777 CONV_TAC(X_FUN_EQ_CONV“t0:num”) THEN GEN_TAC
1778 THEN REWRITE_TAC[BEFORE,WATCH] THEN BETA_TAC THEN EQ_TAC
1779 THEN REPEAT STRIP_TAC THEN EXISTS_TAC“q:num->bool”
1780 THEN ASM_REWRITE_TAC[] THEN DISJ1_TAC
1781 THEN EXISTS_TAC“t:num” THEN ASM_REWRITE_TAC[])
1782
1783
1784
1785val SWHEN_EVENT = TAC_PROOF(
1786 ([],“a SWHEN b = (\t.a t /\ b t) SWHEN b”),
1787 CONV_TAC(X_FUN_EQ_CONV“t0:num”) THEN GEN_TAC
1788 THEN REWRITE_TAC[SWHEN,WATCH] THEN BETA_TAC THEN EQ_TAC
1789 THEN REPEAT STRIP_TAC THEN EXISTS_TAC“q:num->bool”
1790 THEN ASM_REWRITE_TAC[]
1791 THEN EXISTS_TAC“t:num” THEN ASM_REWRITE_TAC[])
1792
1793val SUNTIL_EVENT = TAC_PROOF(
1794 ([],“a SUNTIL b = (\t.a t /\ ~b t) SUNTIL b”),
1795 CONV_TAC(X_FUN_EQ_CONV“t0:num”) THEN GEN_TAC
1796 THEN REWRITE_TAC[SUNTIL,WATCH] THEN BETA_TAC THEN EQ_TAC
1797 THEN REPEAT STRIP_TAC THEN EXISTS_TAC“q:num->bool”
1798 THEN ASM_REWRITE_TAC[] THEN CONJ_TAC
1799 THENL[
1800 ASM_REWRITE_TAC[DECIDE “q\/b\/a/\~b=q\/b\/a”],
1801 EXISTS_TAC“t:num” THEN ASM_REWRITE_TAC[],
1802 UNDISCH_NO_TAC 1 THEN
1803 REWRITE_TAC[DECIDE “q\/b\/a/\~b=q\/b\/a”],
1804 EXISTS_TAC“t:num” THEN ASM_REWRITE_TAC[]])
1805
1806
1807val SBEFORE_EVENT = TAC_PROOF(
1808 ([],“a SBEFORE b = (\t.a t /\ ~b t) SBEFORE b”),
1809 CONV_TAC(X_FUN_EQ_CONV“t0:num”) THEN GEN_TAC
1810 THEN REWRITE_TAC[SBEFORE,WATCH] THEN BETA_TAC THEN EQ_TAC
1811 THEN REPEAT STRIP_TAC THEN EXISTS_TAC“q:num->bool”
1812 THEN ASM_REWRITE_TAC[] THEN EXISTS_TAC“t:num”
1813 THEN ASM_REWRITE_TAC[])
1814
1815
1816
1817val IMMEDIATE_EVENT = TAC_PROOF(
1818 ([],“b t0 ==>
1819 (!a. (a WHEN b) t0 = a t0) /\
1820 (!a. (a UNTIL b) t0 = T) /\
1821 (!a. (a BEFORE b) t0 = F) /\
1822 (!a. (a SWHEN b) t0 = a t0) /\
1823 (!a. (a SUNTIL b) t0 = T) /\
1824 (!a. (a SBEFORE b) t0 = F)”),
1825 DISCH_TAC
1826 THEN ASM_REWRITE_TAC[WHEN_REC,UNTIL_REC,BEFORE_REC]
1827 THEN ASM_REWRITE_TAC[SWHEN_REC,SUNTIL_REC,SBEFORE_REC])
1828
1829
1830val NO_EVENT = TAC_PROOF(
1831 ([],“ALWAYS(\t.~b t) t0 ==>
1832 (!a. (a WHEN b) t0 = T) /\
1833 (!a. (a UNTIL b) t0 = ALWAYS a t0) /\
1834 (!a. (a BEFORE b) t0 = T) /\
1835 (!a. (a SWHEN b) t0 = F) /\
1836 (!a. (a SUNTIL b) t0 = F) /\
1837 (!a. (a SBEFORE b) t0 = EVENTUAL a t0)”),
1838 REWRITE_TAC[ALWAYS,EVENTUAL] THEN BETA_TAC THEN DISCH_TAC
1839 THEN ASM_REWRITE_TAC[WHEN_SIGNAL,UNTIL_SIGNAL,BEFORE_SIGNAL]
1840 THEN ASM_REWRITE_TAC[SWHEN_SIGNAL,SUNTIL_SIGNAL,SBEFORE_SIGNAL])
1841
1842
1843val SOME_EVENT = TAC_PROOF(
1844 ([],“ (EVENTUAL b t0 = (!a. (a WHEN b) t0 = (a SWHEN b) t0)) /\
1845 (EVENTUAL b t0 = (!a. (a UNTIL b) t0 = (a SUNTIL b) t0)) /\
1846 (EVENTUAL b t0 = (!a. (a BEFORE b) t0 = (a SBEFORE b) t0))”),
1847 REPEAT STRIP_TAC >> EQ_TAC >> REPEAT STRIP_TAC
1848 >> REWRITE_TAC[SWHEN_AS_WHEN,SUNTIL_AS_UNTIL,BEFORE_AS_SBEFORE]
1849 >> BETA_TAC >> ASM_REWRITE_TAC[]
1850 >> (MATCH_MP_TAC (DECIDE “~b ==> (a\/b=a)”) ORELSE ALL_TAC)
1851 THENL[
1852 LEFT_FORALL_TAC “\t:num.T”,
1853 LEFT_FORALL_TAC “\t:num.T”,
1854 ALL_TAC,
1855 LEFT_FORALL_TAC “\t:num.F”]
1856 >> UNDISCH_HD_TAC
1857 >> REWRITE_TAC[WHEN_SIMP,SWHEN_SIMP,UNTIL_SIMP,SUNTIL_SIMP]
1858 >> REWRITE_TAC[BEFORE_SIMP,SBEFORE_SIMP,ALWAYS,EVENTUAL]
1859 >> BETA_TAC >> CONV_TAC(DEPTH_CONV NOT_FORALL_CONV)
1860 >> REWRITE_TAC[])
1861
1862
1863
1864val MORE_EVENT = TAC_PROOF(
1865 ([],“ ((a WHEN b) = (\t. a t /\ b t) WHEN b) /\
1866 ((a UNTIL b) = (\t. a t /\ ~b t) UNTIL b) /\
1867 ((a BEFORE b) = (\t. a t /\ ~b t) BEFORE b) /\
1868 ((a SWHEN b) = (\t. a t /\ b t) SWHEN b) /\
1869 ((a SUNTIL b) = (\t. a t /\ ~b t) SUNTIL b) /\
1870 ((a SBEFORE b) = (\t. a t /\ ~b t) SBEFORE b)”),
1871 CONV_TAC(DEPTH_CONV FUN_EQ_CONV)
1872 THEN REWRITE_TAC[WHEN_SIGNAL,SWHEN_SIGNAL,
1873 UNTIL_SIGNAL,SUNTIL_SIGNAL,
1874 BEFORE_SIGNAL,SBEFORE_SIGNAL]
1875 THEN BETA_TAC THEN REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC
1876 THEN RES_TAC THEN ASM_REWRITE_TAC[]
1877 THENL[
1878 EXISTS_TAC“t:num” THEN ASM_REWRITE_TAC[] THEN RES_TAC,
1879 EXISTS_TAC“t:num” THEN ASM_REWRITE_TAC[],
1880 EXISTS_TAC“delta:num” THEN ASM_REWRITE_TAC[],
1881 EXISTS_TAC“delta:num” THEN ASM_REWRITE_TAC[],
1882 EXISTS_TAC“delta:num” THEN ASM_REWRITE_TAC[]
1883 THEN REPEAT STRIP_TAC THEN RES_TAC,
1884 EXISTS_TAC“delta:num” THEN ASM_REWRITE_TAC[]
1885 THEN REPEAT STRIP_TAC THEN RES_TAC,
1886 EXISTS_TAC“delta:num” THEN ASM_REWRITE_TAC[]
1887 THEN POP_ASSUM MATCH_MP_TAC THEN REWRITE_TAC[LESS_EQ_REFL],
1888 EXISTS_TAC“delta:num” THEN ASM_REWRITE_TAC[]])
1889
1890
1891
1892(*---------------------------------------------------------------------------
1893 Fixpoint theorems.
1894 ---------------------------------------------------------------------------*)
1895
1896val WHEN_FIX = prove(
1897 “(y = \t:num. if b t then a t else y(t+1)) =
1898 ((y = a WHEN b) \/ (y = a SWHEN b))”,
1899 EQ_TAC >> REPEAT STRIP_TAC
1900 THENL[
1901 ALL_TAC,
1902 POP_ASSUM SUBST1_TAC >> CONV_TAC FUN_EQ_CONV >> BETA_TAC >> GEN_TAC
1903 >> CONV_TAC(RATOR_CONV(REWRITE_CONV[WHEN_REC]))
1904 >> REWRITE_TAC[NEXT] >> BETA_TAC >> REWRITE_TAC[ADD1],
1905 POP_ASSUM SUBST1_TAC >> CONV_TAC FUN_EQ_CONV >> BETA_TAC >> GEN_TAC
1906 >> CONV_TAC(RATOR_CONV(REWRITE_CONV[SWHEN_REC]))
1907 >> REWRITE_TAC[NEXT] >> BETA_TAC >> REWRITE_TAC[ADD1]]
1908 (* ----------------------------------------------------------------- *)
1909 >> MY_MP_TAC “!y. (y = (\t. if b t then a t else y(t+1)))
1910 ==> !t0. (!t.~b(t+t0)) ==> (!t. y(t+t0):bool = y t0)”
1911 (* ----------------------------------------------------------------- *)
1912 THENL[
1913 GEN_TAC >> DISCH_TAC >> GEN_TAC >> DISCH_TAC
1914 >> INDUCT_TAC >> REWRITE_TAC[ADD_CLAUSES]
1915 >> POP_ASSUM(SUBST1_TAC o SYM)
1916 >> POP_NO_ASSUM 1 (fn x=> CONV_TAC(RAND_CONV(ONCE_REWRITE_CONV[x])))
1917 >> BETA_TAC >> ASM_REWRITE_TAC[ADD1],
1918 DISCH_TAC]
1919 (* ----------------------------------------------------------------- *)
1920 >> MY_MP_TAC “!y. (y = (\t. if b t then a t else y(t+1)))
1921 ==> ( !delta t0. (!t. t<delta ==> ~b(t+t0))
1922 ==> (!t. t<delta ==> (y(t+t0):bool = y t0)))”
1923 (* ----------------------------------------------------------------- *)
1924 THENL[
1925 GEN_TAC >> DISCH_TAC >> REPEAT GEN_TAC >> DISCH_TAC
1926 >> INDUCT_TAC >> REWRITE_TAC[ADD_CLAUSES] >> DISCH_TAC
1927 >> IMP_RES_TAC(EQT_ELIM(ARITH_CONV“SUC d <delta ==> d<delta”))
1928 >> RES_TAC
1929 >> POP_NO_ASSUM 10 (fn x=> CONV_TAC(RAND_CONV(ONCE_REWRITE_CONV[SYM x])))
1930 >> POP_NO_ASSUM 14 (fn x=> CONV_TAC(RAND_CONV(ONCE_REWRITE_CONV[x])))
1931 >> BETA_TAC >> ASM_REWRITE_TAC[ADD1],
1932 DISCH_TAC]
1933 (* ----------------------------------------------------------------- *)
1934 >> MY_MP_TAC
1935 “!y. (y = (\t. if b t then a t else y(t+1)))
1936 ==>
1937 !delta t0. b(delta+t0) ==> (y(delta+t0):bool = a(delta+t0))”
1938 (* ----------------------------------------------------------------- *)
1939 THENL[
1940 GEN_TAC >> DISCH_TAC >> REPEAT STRIP_TAC
1941 >> POP_NO_ASSUM 1 (fn x=> CONV_TAC(RATOR_CONV(ONCE_REWRITE_CONV[x])))
1942 >> BETA_TAC >> ASM_REWRITE_TAC[],
1943 DISCH_TAC]
1944 (* ----------------------------------------------------------------- *)
1945 >> MY_MP_TAC “!y. (y = (\t. if b t then a t else y(t+1)))
1946 ==> !t0. (?d.b(d+t0)) ==> (y t0 = (a WHEN b) t0)”
1947 (* ----------------------------------------------------------------- *)
1948 THENL[
1949 REPEAT STRIP_TAC
1950 >> IMP_RES_TAC(BETA_RULE(ISPEC“\d.b(d+t0):bool”WOP))
1951 >> REWRITE_TAC[WHEN_SIGNAL] >> EQ_TAC >> REPEAT STRIP_TAC
1952 THENL[
1953 MY_MP_TAC “n=(delta:num)”
1954 THENL[
1955 DISJ_CASES_TAC(SPECL[“delta:num”,“n:num”]LESS_CASES)
1956 THENL[RES_TAC,ALL_TAC]
1957 >> UNDISCH_HD_TAC >> REWRITE_TAC[LESS_OR_EQ] >> STRIP_TAC
1958 >> RES_TAC,
1959 DISCH_TAC]
1960 >> POP_ASSUM (SUBST1_TAC o SYM) >> POP_NO_TAC 0 >> POP_NO_TAC 0
1961 >> POP_NO_TAC 8 >> RES_TAC
1962 >> POP_NO_ASSUM 11 (SUBST1_TAC o SYM)
1963 >> DISJ_CASES_TAC(EQT_ELIM(ARITH_CONV“(n=0)\/(0<n)”))
1964 THENL[
1965 POP_ASSUM REWRITE1_TAC >> REWRITE_TAC[ADD_CLAUSES]
1966 >> POP_NO_ASSUM 11 REWRITE1_TAC,
1967 ALL_TAC]
1968 >> IMP_RES_TAC LESS_ADD_1
1969 >> IMP_RES_TAC(EQT_ELIM(ARITH_CONV“(d=0+(p+1))==>(p<d)”))
1970 >> RES_TAC >> UNDISCH_NO_TAC 4
1971 >> POP_NO_ASSUM 22 (fn x=> CONV_TAC(RATOR_CONV(ONCE_REWRITE_CONV[x])))
1972 >> BETA_TAC >> ASM_TAC 2 REWRITE1_TAC
1973 >> IMP_RES_TAC(EQT_ELIM(ARITH_CONV“(d=0+(p+1))==>((p+t0)+1 = d+t0)”))
1974 >> ASM_TAC 0 REWRITE1_TAC,
1975 LEFT_FORALL_TAC “n:num” >> UNDISCH_HD_TAC
1976 >> ASM_TAC 1 REWRITE1_TAC >> ASM_TAC 0 REWRITE1_TAC
1977 >> POP_NO_TAC 7 >> POP_NO_TAC 6 >> RES_TAC
1978 >> POP_NO_ASSUM 8 (SUBST1_TAC o SYM)
1979 >> DISJ_CASES_TAC(EQT_ELIM(ARITH_CONV“(n=0)\/(0<n)”))
1980 THENL[
1981 POP_ASSUM REWRITE1_TAC >> REWRITE_TAC[ADD_CLAUSES],
1982 ALL_TAC]
1983 >> IMP_RES_TAC LESS_ADD_1
1984 >> IMP_RES_TAC(EQT_ELIM(ARITH_CONV“(d=0+(p+1))==>(p<d)”))
1985 >> RES_TAC >> POP_NO_ASSUM 4 (SUBST1_TAC o SYM)
1986 >> POP_NO_ASSUM 22 (fn x=> CONV_TAC(RAND_CONV(ONCE_REWRITE_CONV[x])))
1987 >> BETA_TAC >> ASM_TAC 2 REWRITE1_TAC
1988 >> IMP_RES_TAC(EQT_ELIM(ARITH_CONV“(d=0+(p+1))==>((p+t0)+1 = d+t0)”))
1989 >> ASM_TAC 0 REWRITE1_TAC],
1990 DISCH_TAC]
1991 >> CONV_TAC(DEPTH_CONV FUN_EQ_CONV)
1992 >> ASSUME_TAC WHEN_SWHEN_LEMMA >> UNDISCH_HD_TAC
1993 >> ASM_CASES_TAC“!t1.?t2.b(t2+t1)” >> ASM_TAC 0 REWRITE1_TAC
1994 THENL[
1995 (* ----------------------------------------------------------------- *)
1996 (* first case : !t1.?t2.b(t2+t1) *)
1997 (* ----------------------------------------------------------------- *)
1998 DISCH_TAC >> ASM_TAC 0 (REWRITE1_TAC o SYM o SPEC_ALL)
1999 >> REWRITE_TAC[WHEN_SIGNAL] >> BETA_TAC
2000 >> X_GEN_TAC “t0:num” >> EQ_TAC
2001 >> REPEAT STRIP_TAC
2002 THENL[
2003 RES_TAC >> POP_NO_ASSUM 8 (SUBST1_TAC o SYM)
2004 >> DISJ_CASES_TAC(EQT_ELIM(ARITH_CONV“(delta=0)\/(0<delta)”))
2005 THENL[
2006 POP_ASSUM REWRITE1_TAC >> REWRITE_TAC[ADD_CLAUSES]
2007 >> ASM_TAC 11 REWRITE1_TAC,
2008 ALL_TAC]
2009 >> IMP_RES_TAC LESS_ADD_1
2010 >> IMP_RES_TAC(EQT_ELIM(ARITH_CONV“(d=0+(p+1))==>(p<d)”))
2011 >> RES_TAC >> UNDISCH_NO_TAC 5
2012 >> POP_NO_ASSUM 26 (fn x=> CONV_TAC(RATOR_CONV(ONCE_REWRITE_CONV[x])))
2013 >> BETA_TAC >> ASM_TAC 3 REWRITE1_TAC
2014 >> IMP_RES_TAC(EQT_ELIM(ARITH_CONV“(d=0+(p+1))==>((p+t0)+1 = d+t0)”))
2015 >> ASM_TAC 0 REWRITE1_TAC,
2016 LEFT_NO_FORALL_TAC 2 “t0:num” >> LEFT_EXISTS_TAC
2017 >> IMP_RES_TAC(BETA_RULE(ISPEC“\t2.b(t2+t0):bool”WOP))
2018 >> LEFT_NO_FORALL_TAC 3 “n:num” >> UNDISCH_HD_TAC
2019 >> ASM_TAC 0 REWRITE1_TAC >> ASM_TAC 1 REWRITE1_TAC
2020 >> POP_NO_TAC 2 >> RES_TAC
2021 >> POP_NO_ASSUM 8 (SUBST1_TAC o SYM)
2022 >> DISJ_CASES_TAC(EQT_ELIM(ARITH_CONV“(n=0)\/(0<n)”))
2023 THENL[
2024 POP_ASSUM REWRITE1_TAC >> REWRITE_TAC[ADD_CLAUSES],
2025 ALL_TAC]
2026 >> IMP_RES_TAC LESS_ADD_1
2027 >> IMP_RES_TAC(EQT_ELIM(ARITH_CONV“(d=0+(p+1))==>(p<d)”))
2028 >> RES_TAC >> POP_NO_ASSUM 4 (SUBST1_TAC o SYM)
2029 >> POP_NO_ASSUM 29 (fn x=> CONV_TAC(RAND_CONV(ONCE_REWRITE_CONV[x])))
2030 >> BETA_TAC >> ASM_TAC 2 REWRITE1_TAC
2031 >> IMP_RES_TAC(EQT_ELIM(ARITH_CONV“(d=0+(p+1))==>((p+t0)+1 = d+t0)”))
2032 >> ASM_TAC 0 REWRITE1_TAC],
2033 ALL_TAC]
2034 (* ----------------------------------------------------------------- *)
2035 (* second case : ?t1.!t2.~b(t2+t1) *)
2036 (* ----------------------------------------------------------------- *)
2037 >> UNDISCH_HD_TAC >> CONV_TAC(DEPTH_CONV NOT_FORALL_CONV)
2038 >> CONV_TAC(DEPTH_CONV NOT_EXISTS_CONV) >> DISCH_TAC
2039 >> LEFT_EXISTS_TAC >> DISCH_TAC >> LEFT_EXISTS_TAC
2040 >> IMP_RES_TAC(BETA_RULE(ISPEC“\t1.!t2.~b(t2+t1)”WOP))
2041 >> POP_NO_TAC 3 >> UNDISCH_HD_TAC
2042 >> CONV_TAC(DEPTH_CONV NOT_FORALL_CONV)
2043 >> REWRITE_TAC[] >> DISCH_TAC
2044 (* ----------------------------------------------------------------- *)
2045 >> MY_MP_TAC“!y. (y = (\t. if b t then a t else y(t+1)))
2046 ==> !m. m<n ==> (y m = (a WHEN b) m)”
2047 (* ----------------------------------------------------------------- *)
2048 THENL[
2049 REPEAT STRIP_TAC >> POP_NO_TAC 9 >> RES_TAC,
2050 DISCH_TAC]
2051 (* ----------------------------------------------------------------- *)
2052 >> MY_MP_TAC“!y:num->bool. (y = (\t. if b t then a t else y(t+1)))
2053 ==> !m. y(m+n) = y n”
2054 (* ----------------------------------------------------------------- *)
2055 THENL[
2056 GEN_TAC >> DISCH_TAC >> POP_NO_TAC 9 >> RES_TAC,
2057 DISCH_TAC]
2058 (* ----------------------------------------------------------------- *)
2059 >> MY_MP_TAC“!m. m<n ==> (y m = (a WHEN b) m)”
2060 (* ----------------------------------------------------------------- *)
2061 THENL[
2062 POP_NO_ASSUM 1 MATCH_MP_TAC >> POP_NO_ASSUM 8 (REWRITE1_TAC o SYM),
2063 DISCH_TAC]
2064 (* ----------------------------------------------------------------- *)
2065 >> MY_MP_TAC“!m. m<n ==> ((a SWHEN b) m = (a WHEN b) m)”
2066 (* ----------------------------------------------------------------- *)
2067 THENL[
2068 POP_NO_ASSUM 2 MATCH_MP_TAC >> CONV_TAC FUN_EQ_CONV >> GEN_TAC
2069 >> CONV_TAC(RATOR_CONV(REWRITE_CONV[SWHEN_REC]))
2070 >> REWRITE_TAC[NEXT] >> BETA_TAC >> REWRITE_TAC[ADD1],
2071 DISCH_TAC]
2072 >> ASM_CASES_TAC “(y:num->bool) n”
2073 THENL[
2074 DISJ1_TAC >> GEN_TAC
2075 >> DISJ_CASES_TAC(SPECL[“n':num”,“n:num”] LESS_CASES)
2076 THENL[RES_TAC,ALL_TAC]
2077 >> IMP_RES_TAC LESS_EQUAL_ADD
2078 >> POP_ASSUM SUBST1_TAC >> POP_NO_TAC 0
2079 >> ONCE_REWRITE_TAC[ADD_SYM] >> RES_TAC
2080 >> ASM_TAC 12 REWRITE1_TAC
2081 >> ASM_REWRITE_TAC[WHEN_SIGNAL,ADD_ASSOC],
2082 DISJ2_TAC >> GEN_TAC
2083 >> DISJ_CASES_TAC(SPECL[“n':num”,“n:num”] LESS_CASES)
2084 THENL[
2085 RES_TAC >> ASM_TAC 12 REWRITE1_TAC >> ASM_TAC 15 REWRITE1_TAC,
2086 ALL_TAC]
2087 >> IMP_RES_TAC LESS_EQUAL_ADD
2088 >> POP_ASSUM SUBST1_TAC >> POP_NO_TAC 0
2089 >> ONCE_REWRITE_TAC[ADD_SYM] >> RES_TAC
2090 >> ASM_TAC 13 REWRITE1_TAC >> ASM_TAC 14 REWRITE1_TAC
2091 >> ASM_REWRITE_TAC[SWHEN_SIGNAL,ADD_ASSOC]])
2092
2093
2094
2095val UNTIL_FIX =
2096 let val th1 = SPEC“z:num->bool”(GEN“a:num->bool”WHEN_FIX)
2097 val th2 = GENL[“b:num->bool”,“z:num->bool”]th1
2098 val th3 = SPECL[“\t:num.a t ==> b t”,“b:num->bool”]th2
2099 val th4 = REWRITE_RULE[SYM UNTIL_AS_WHEN,SYM SUNTIL_AS_SWHEN] th3
2100 val th5 = BETA_RULE th4
2101 val rwt = prove(“(if (a==>b) then b else y) = (~b ==> a /\ y)”,TAUT_TAC)
2102 val th6 = REWRITE_RULE[rwt] th5
2103 in
2104 th6
2105 end
2106
2107
2108
2109val ALWAYS_FIX =
2110 let val th1 = BETA_RULE(SPEC“\t:num.F”(GEN“a:num->bool”WHEN_FIX))
2111 val th2 = BETA_RULE(SPEC“\t:num.~a t”(GEN“b:num->bool”th1))
2112 val th3 = REWRITE_RULE[SYM ALWAYS_AS_WHEN] th2
2113 val th4 = REWRITE_RULE[prove(“(if ~a then F else y) = a/\y”,TAUT_TAC)]
2114 th3
2115 val th5 = TAC_PROOF(
2116 ([],“(\t.F) SWHEN (\t.~a t) = \t.F”),
2117 CONV_TAC FUN_EQ_CONV THEN BETA_TAC
2118 THEN REWRITE_TAC[SWHEN_SIGNAL])
2119 val th6 = REWRITE_RULE[th5] th4
2120 in
2121 th6
2122 end
2123
2124
2125
2126
2127val EVENTUAL_FIX = TAC_PROOF(
2128 ([],“(y = \t. a t \/ y(t+1)) = (y = EVENTUAL a) \/ (y = (\t. T))”),
2129 let val th1 = SPECL[“\t:num.~y t”,“\t:num.~a t”](GEN_ALL ALWAYS_FIX)
2130 val th2 = BETA_RULE(CONV_RULE(DEPTH_CONV FUN_EQ_CONV) th1)
2131 in
2132 CONV_TAC(DEPTH_CONV FUN_EQ_CONV) THEN BETA_TAC
2133 THEN ONCE_REWRITE_TAC[
2134 DECIDE “(y (n:num)=b) = (~y n = ~b)”]
2135 THEN REWRITE_TAC[DE_MORGAN_THM,
2136 TAC_PROOF(([],“EVENTUAL a = \t.~ALWAYS (\t.~a t) t”),
2137 CONV_TAC FUN_EQ_CONV THEN REWRITE_TAC[ALWAYS,EVENTUAL]
2138 THEN BETA_TAC THEN CONV_TAC(DEPTH_CONV NOT_FORALL_CONV)
2139 THEN REWRITE_TAC[])]
2140 THEN BETA_TAC THEN REWRITE_TAC[th2]
2141 end)
2142
2143
2144
2145val BEFORE_FIX = TAC_PROOF(
2146 ([],“!y.
2147 (y = (\t. ~(b t) /\ (a t \/ y (t + 1)))) =
2148 (y = a BEFORE b) \/ (y = a SBEFORE b)”),
2149 REWRITE_TAC[BEFORE_AS_WHEN,SBEFORE_AS_SWHEN]
2150 THEN ASSUME_TAC (Q.GEN `y`
2151 (Q.INST [(`a` |-> `\t:num.~b t`),
2152 (`b` |-> `\t:num. a t \/ b t`)] WHEN_FIX))
2153 THEN GEN_TAC THEN UNDISCH_HD_TAC THEN BETA_TAC
2154 THEN DISCH_TAC THEN POP_ASSUM (REWRITE1_TAC o SYM o SPEC_ALL)
2155 THEN REWRITE_TAC[prove(“(if (a\/b) then ~b else y) = ~b/\(a\/y)”,
2156 TAUT_TAC)])
2157
2158
2159(* ************************************************************ *)
2160(* Invariant Theorems of the Operators *)
2161(* ************************************************************ *)
2162
2163(* -------------------------------------------- *)
2164(* Proving the invariant theorem of WHEN *)
2165(* -------------------------------------------- *)
2166
2167
2168val WHEN_INVARIANT = TAC_PROOF(
2169 ([],“(a WHEN b) t0 =
2170 ?J.J t0 /\
2171 (!t. ~(b (t + t0)) /\ J (t + t0) ==> J (SUC (t + t0))) /\
2172 (!d. b (d + t0) /\ J (d + t0) ==> a (d + t0))”),
2173 EQ_TAC THENL[
2174 REWRITE_TAC[WHEN,WATCH] >> REPEAT STRIP_TAC
2175 >> EXISTS_TAC “a WHEN b” >> BETA_TAC
2176 >> REPEAT CONJ_TAC
2177 THENL[
2178 ALL_TAC,
2179 GEN_TAC >> SUBST1_TAC(SPEC“t+t0”(GEN“t0:num”WHEN_REC))
2180 >> REWRITE_TAC[NEXT] >> BETA_TAC
2181 >> REPEAT STRIP_TAC >> UNDISCH_HD_TAC >> ASM_REWRITE_TAC[],
2182 REWRITE_TAC[WHEN_SIGNAL] >> REPEAT STRIP_TAC
2183 >> LEFT_FORALL_TAC “0”
2184 >> UNDISCH_HD_TAC >> ASM_REWRITE_TAC[NOT_LESS_0,ADD_CLAUSES]]
2185 >> REWRITE_TAC[WHEN] >> ASSUME_TAC (SPEC_ALL WATCH_EXISTS)
2186 >> LEFT_EXISTS_TAC >> EXISTS_TAC “q':num->bool”
2187 >> UNDISCH_HD_TAC >> ASM_REWRITE_TAC[WATCH] >> STRIP_TAC
2188 >> MY_MP_TAC“!t.q'(t+t0):bool = q(t+t0)”
2189 THENL[INDUCT_TAC >> ASM_REWRITE_TAC[ADD_CLAUSES],ALL_TAC]
2190 >> DISCH_TAC >> ASM_REWRITE_TAC[],
2191 REPEAT STRIP_TAC >> PURE_REWRITE_TAC[WHEN]
2192 >> ASSUME_TAC (SPEC_ALL(REWRITE_RULE[WATCH]WATCH_EXISTS))
2193 >> LEFT_EXISTS_TAC >> EXISTS_TAC “q:num->bool” >> ASM_REWRITE_TAC[WATCH]
2194 >> DISJ_CASES_TAC DELTA_CASES
2195 THENL[ALL_TAC,UNDISCH_NO_TAC 1 >> PURE_REWRITE_TAC[WATCH_SIGNAL]
2196 >> ASM_REWRITE_TAC[]]
2197 >> LEFT_EXISTS_TAC >> UNDISCH_HD_TAC >> STRIP_TAC >> GEN_TAC
2198 >> DISJ_CASES_TAC (SPECL [“t:num”,“d:num”] LESS_LESS_CASES)
2199 THENL[MY_MP_TAC “!t. t<=d ==> J(t+t0)”
2200 THENL[INDUCT_TAC THENL[ASM_REWRITE_TAC[ADD_CLAUSES],ALL_TAC]
2201 >> REWRITE_TAC[SYM(SPEC_ALL LESS_EQ)]
2202 >> DISCH_TAC >> IMP_RES_TAC LESS_IMP_LESS_OR_EQ
2203 >> RES_TAC >> RES_TAC
2204 >> UNDISCH_HD_TAC >> ASM_REWRITE_TAC[ADD_CLAUSES],
2205 DISCH_TAC >> LEFT_FORALL_TAC “d:num”
2206 >> RULE_ASSUM_TAC(REWRITE_RULE[LESS_EQ_REFL])
2207 >> RES_TAC >> ASM_REWRITE_TAC[]],
2208 POP_ASSUM DISJ_CASES_TAC THENL[RES_TAC >> ASM_REWRITE_TAC[],ALL_TAC]
2209 >> UNDISCH_HD_TAC >> REWRITE_TAC[LESS_EQ] >> DISCH_TAC
2210 >> IMP_RES_TAC LESS_EQUAL_ADD >> POP_ASSUM SUBST1_TAC
2211 >> DISJ1_TAC >> ASSUME_TAC(SPEC_ALL WATCH_SIGNAL)
2212 >> UNDISCH_HD_TAC >> ASM_REWRITE_TAC[WATCH] >> STRIP_TAC
2213 >> RES_TAC >> LEFT_NO_FORALL_TAC 2 “p:num”
2214 >> UNDISCH_HD_TAC
2215 >> REWRITE_TAC[(EQT_ELIM(ARITH_CONV“(SUC d+p)+t0 = SUC(p+(d+t0))”))]]])
2216
2217
2218
2219val UNTIL_INVARIANT =
2220 let
2221 val t0 = “t0:num”
2222 val a = “b:num->bool”
2223 val b = “\t:num. a t ==> b t”
2224 val lemma1 = BETA_RULE(SPECL[t0,b,a](GEN_ALL WHEN_INVARIANT))
2225 val lemma2 = X_FUN_EQ_CONV t0 (concl UNTIL_AS_WHEN)
2226 val lemma3 = EQ_MP lemma2 UNTIL_AS_WHEN
2227 val lemma4 = REWRITE_RULE[lemma1] lemma3
2228 val t1 = #conj2(dest_conj(#Body(dest_exists(rhs(concl(SPEC_ALL lemma4))))))
2229 val {Rand=t2,Rator=fa} = dest_comb(#conj2(dest_conj t1))
2230 val lemma5 = AP_TERM fa (ALPHA_CONV “t:num” t2)
2231 val lemma6 = ONCE_REWRITE_RULE[lemma5] lemma4
2232 val lemma7 = CONV_RULE(DEPTH_CONV AND_FORALL_CONV) lemma6
2233 val lemma8 = TAC_PROOF(
2234 ([],“((~(a==>b) /\ j ==> J) /\
2235 ( (a==>b) /\ j ==> b) )
2236 = (j /\ ~b ==> (a /\ J))”),
2237 TAUT_TAC)
2238 in
2239 REWRITE_RULE[lemma8]lemma7
2240 end
2241
2242
2243
2244val BEFORE_INVARIANT = TAC_PROOF(
2245 ([],“(a BEFORE b) t0 =
2246 ?J.
2247 J t0 /\
2248 (!t. J(t+t0) /\ ~a(t+t0) ==> J(SUC(t+t0))) /\
2249 (!d. J(d+t0) ==> ~b(d+t0))”),
2250 REWRITE_TAC[BEFORE_AS_WHEN,WHEN_INVARIANT] THEN BETA_TAC
2251 THEN REWRITE_TAC[DECIDE “(a\/b)/\J==> ~b = J==>~b”]
2252 THEN EQ_TAC THEN REPEAT STRIP_TAC THEN EXISTS_TAC“J:num->bool”
2253 THEN ASM_REWRITE_TAC[] THEN GEN_TAC
2254 THEN LEFT_FORALL_TAC“t:num” THEN UNDISCH_HD_TAC
2255 THEN LEFT_FORALL_TAC“t:num” THEN UNDISCH_HD_TAC
2256 THEN TAUT_TAC)
2257
2258
2259val ALWAYS_INVARIANT = TAC_PROOF(
2260 ([],“ALWAYS a t0 = ?J. J t0 /\ (!t. J(t+t0) ==> a(t+t0)/\J(t+(t0+1)))”),
2261 REWRITE_TAC[ALWAYS_AS_UNTIL,UNTIL_INVARIANT,ONE,ADD_CLAUSES])
2262
2263
2264
2265val EVENTUAL_INVARIANT = TAC_PROOF(
2266 ([],“EVENTUAL b t0 =
2267 ?J.
2268 (0<J t0) /\
2269 (!t. (J(SUC(t+t0)) < J(t+t0)) \/ (J(SUC(t+t0))=0)) /\
2270 (!t. (0<J(t+t0)) /\ (J(SUC(t+t0))=0) ==> b(t+t0))”),
2271 REWRITE_TAC[EVENTUAL] >> EQ_TAC >> REPEAT STRIP_TAC
2272 THENL[
2273 EXISTS_TAC “\x:num.SUC(t+t0)-x”
2274 >> BETA_TAC >> REPEAT STRIP_TAC
2275 THENL[
2276 CONV_TAC ARITH_CONV,
2277 CONV_TAC ARITH_CONV,
2278 IMP_RES_TAC(EQT_ELIM(ARITH_CONV
2279 “(SUC(t+t0)-SUC(t'+t0)=0) ==> (t<=t')”))
2280 >> IMP_RES_TAC(EQT_ELIM(ARITH_CONV
2281 “(0<SUC(t+t0)-(t'+t0)) ==> (t'<=t)”))
2282 >> IMP_RES_TAC(EQT_ELIM(ARITH_CONV
2283 “(t<=t')/\(t'<=t)==>(t'=t)”))
2284 >> POP_ASSUM SUBST1_TAC >> ASM_TAC 5 REWRITE1_TAC],
2285 ALL_TAC]
2286 >> MY_MP_TAC “!n t0 J.
2287 (!t. J(SUC(t+t0))<J(t+t0) \/ (J(SUC(t+t0))=0))
2288 ==>
2289 ((J t0 <= n) ==> (J(n+t0)=0))”
2290 THENL[
2291 INDUCT_TAC >> REWRITE_TAC[ADD_CLAUSES] >> REPEAT STRIP_TAC
2292 THENL[
2293 RULE_ASSUM_TAC(REWRITE_RULE[LESS_EQ_0]) >> ASM_REWRITE_TAC[ADD_CLAUSES],
2294 REPEAT STRIP_TAC >> LEFT_NO_FORALL_TAC 2 “t0':num”
2295 >> LEFT_FORALL_TAC“\x.J'(SUC x):num”
2296 >> RULE_ASSUM_TAC BETA_RULE
2297 >> RULE_ASSUM_TAC(REWRITE_RULE[
2298 DECIDE “a==>(b==>c)= a/\b==>c”])
2299 >> POP_ASSUM MATCH_MP_TAC >> CONJ_TAC
2300 THENL[
2301 GEN_TAC >> LEFT_NO_FORALL_TAC 1 “SUC t”
2302 >> UNDISCH_HD_TAC >> REWRITE_TAC[ADD_CLAUSES],
2303 LEFT_NO_FORALL_TAC 1 “0” >> UNDISCH_HD_TAC
2304 >> REWRITE_TAC[ADD_CLAUSES] >> STRIP_TAC
2305 >> ASM_REWRITE_TAC[] THENL[ALL_TAC,CONV_TAC ARITH_CONV]
2306 >> IMP_RES_TAC(EQT_ELIM(ARITH_CONV
2307 “!m n p. m<n /\ n<=p ==> m<p”))
2308 >> UNDISCH_NO_TAC 1 >> CONV_TAC ARITH_CONV]],
2309 DISCH_TAC
2310 ] >>
2311 LEFT_FORALL_TAC “(J:num->num) t0”
2312 >> LEFT_FORALL_TAC “t0:num”
2313 >> LEFT_FORALL_TAC “J:num->num”
2314 >> UNDISCH_HD_TAC >> ASM_REWRITE_TAC[LESS_EQ_REFL]
2315 >> DISCH_TAC
2316 >> IMP_RES_TAC(BETA_RULE(ISPEC“\t.J(t+t0)=0”WOP))
2317 >> DISJ_CASES_TAC(SPEC“n:num”num_CASES)
2318 THENL[
2319 UNDISCH_NO_TAC 2 >> ASM_REWRITE_TAC[ADD_CLAUSES]
2320 >> IMP_RES_TAC(EQT_ELIM(ARITH_CONV“0<x ==> ~(x=0)”))
2321 >> ASM_REWRITE_TAC[],
2322 LEFT_EXISTS_TAC >> LEFT_NO_FORALL_TAC 4 “n':num”
2323 >> EXISTS_TAC“n':num” >> POP_ASSUM MATCH_MP_TAC
2324 >> LEFT_NO_FORALL_TAC 1 “n':num”
2325 >> UNDISCH_HD_TAC >> ASM_REWRITE_TAC[LESS_SUC_REFL,
2326 EQT_ELIM(ARITH_CONV“~(x=0) = (0<x)”)]
2327 >> DISCH_TAC >> POP_ASSUM REWRITE1_TAC
2328 >> UNDISCH_NO_TAC 1 >> ASM_REWRITE_TAC[ADD_CLAUSES]])
2329
2330
2331
2332
2333
2334
2335val SWHEN_INVARIANT = TAC_PROOF(
2336 ([],“(a SWHEN b) t0 =
2337 (?J1.J1 t0 /\
2338 (!t. ~b(t+t0) /\ J1(t+t0) ==> J1(SUC(t+t0))) /\
2339 (!d. b(d+t0) /\ J1(d+t0) ==> a(d+t0))) /\
2340 (?J2.
2341 0 < J2 t0 /\
2342 (!t. J2(SUC(t+t0))<J2(t+t0) \/ (J2(SUC(t+t0))=0)) /\
2343 (!t. 0<J2(t+t0) /\ (J2(SUC(t+t0))=0) ==> b(t+t0)))”),
2344 REWRITE_TAC[SWHEN_AS_WHEN,WHEN_INVARIANT,EVENTUAL_INVARIANT]
2345 THEN BETA_TAC THEN REWRITE_TAC[])
2346
2347
2348
2349
2350val SUNTIL_INVARIANT = TAC_PROOF(
2351 ([],“(a SUNTIL b) t0 =
2352 (?J1.J1 t0 /\
2353 (!t. J1(t+t0) /\ ~b(t+t0) ==> a(t+t0) /\ J1(SUC(t+t0)))) /\
2354 (?J2.
2355 0 < J2 t0 /\
2356 (!t. J2(SUC(t+t0))<J2(t+t0) \/ (J2(SUC(t+t0))=0)) /\
2357 (!t. 0<J2(t+t0) /\ (J2(SUC(t+t0))=0) ==> b(t+t0)))”),
2358 REWRITE_TAC[SUNTIL_AS_UNTIL,UNTIL_INVARIANT,EVENTUAL_INVARIANT]
2359 THEN BETA_TAC THEN REWRITE_TAC[])
2360
2361
2362
2363val SBEFORE_INVARIANT = TAC_PROOF(
2364 ([],“(a SBEFORE b) t0 =
2365 (?J1. J1 t0 /\
2366 (!t.J1(t+t0) /\ ~a(t+t0) ==> J1(SUC(t+t0))) /\
2367 (!d.J1(d+t0) ==> ~b(d+t0))) /\
2368 (?J2.
2369 0 < J2 t0 /\
2370 (!t. J2(SUC(t+t0))<J2(t+t0) \/ (J2(SUC(t+t0))=0)) /\
2371 (!t. 0<J2(t+t0) /\ (J2(SUC(t+t0))=0) ==> a(t+t0)))”),
2372 REWRITE_TAC[SBEFORE_AS_BEFORE,BEFORE_INVARIANT,EVENTUAL_INVARIANT]
2373 THEN BETA_TAC THEN REWRITE_TAC[])
2374
2375
2376
2377
2378(* ************************************************************************* *)
2379(* Negations of temporal expressions *)
2380(* ************************************************************************* *)
2381
2382val NOT_ALWAYS = TAC_PROOF(
2383 ([],“~(ALWAYS a t0) = EVENTUAL (\t.~a t) t0”),
2384 REWRITE_TAC[ALWAYS,EVENTUAL] THEN BETA_TAC
2385 THEN CONV_TAC(DEPTH_CONV NOT_FORALL_CONV)
2386 THEN REWRITE_TAC[])
2387
2388
2389val NOT_EVENTUAL = TAC_PROOF(
2390 ([],“~(EVENTUAL a t0) = ALWAYS (\t.~a t) t0”),
2391 REWRITE_TAC[ALWAYS,EVENTUAL] THEN BETA_TAC
2392 THEN CONV_TAC(DEPTH_CONV NOT_EXISTS_CONV)
2393 THEN REWRITE_TAC[])
2394
2395
2396val NOT_WHEN = TAC_PROOF(
2397 ([],“~((a WHEN b)t0) = ((\t.~a t) SWHEN b) t0”),
2398 REWRITE_TAC[WHEN_SIGNAL,SWHEN_SIGNAL] THEN BETA_TAC
2399 THEN CONV_TAC(DEPTH_CONV NOT_FORALL_CONV)
2400 THEN REWRITE_TAC[DECIDE “~(a==>b) = a/\~b”]
2401 THEN EQ_TAC THEN REPEAT STRIP_TAC THEN RES_TAC
2402 THEN EXISTS_TAC“delta:num” THEN ASM_REWRITE_TAC[])
2403
2404
2405val NOT_UNTIL = TAC_PROOF(
2406 ([],“~((a UNTIL b)t0) = ((\t.~a t) SBEFORE b) t0”),
2407 REWRITE_TAC[UNTIL_AS_SBEFORE] THEN BETA_TAC
2408 THEN REWRITE_TAC[])
2409
2410
2411
2412val NOT_BEFORE = TAC_PROOF(
2413 ([],“~((a BEFORE b)t0) = ((\t.~a t) SUNTIL b) t0”),
2414 REWRITE_TAC[BEFORE_AS_SUNTIL] THEN BETA_TAC
2415 THEN REWRITE_TAC[])
2416
2417
2418val NOT_SWHEN =
2419 let
2420 val thm1 = BETA_RULE(SPEC“\t:num.~a t”(GEN“a:num->bool”NOT_WHEN))
2421 val thm2 = SYM(REWRITE_RULE[]thm1)
2422 val thm3 = (CONV_RULE(DEPTH_CONV ETA_CONV)) thm2
2423 val thm4 = ONCE_REWRITE_RULE[prove(“(a= ~b) = (~a=b)”,TAUT_TAC)] thm3
2424 in thm4
2425 end
2426
2427
2428val NOT_SUNTIL = TAC_PROOF(
2429 ([],“~((a SUNTIL b)t0) = ((\t.~a t) BEFORE b) t0”),
2430 REWRITE_TAC[SUNTIL_AS_BEFORE] THEN BETA_TAC
2431 THEN REWRITE_TAC[DE_MORGAN_THM,NOT_ALWAYS])
2432
2433
2434
2435
2436val NOT_SBEFORE = TAC_PROOF(
2437 ([],“~((a SBEFORE b)t0) = ((\t.~a t) UNTIL b) t0”),
2438 REWRITE_TAC[SBEFORE_AS_UNTIL] THEN BETA_TAC
2439 THEN REWRITE_TAC[])
2440
2441
2442(* ************************************************************ *)
2443(* IDEMPOTENCY THEOREMS *)
2444(* ************************************************************ *)
2445
2446
2447val ALWAYS_IDEM = TAC_PROOF(
2448 ([],“ALWAYS a = ALWAYS (ALWAYS a)”),
2449 CONV_TAC (X_FUN_EQ_CONV“t0:num”) THEN GEN_TAC
2450 THEN REWRITE_TAC[ALWAYS_SIGNAL]
2451 THEN EQ_TAC THEN REPEAT STRIP_TAC
2452 THENL[
2453 LEFT_FORALL_TAC “t' + t”THEN UNDISCH_HD_TAC
2454 THEN REWRITE_TAC[ADD_ASSOC],
2455 LEFT_FORALL_TAC “t:num” THEN LEFT_FORALL_TAC “0”
2456 THEN UNDISCH_HD_TAC THEN REWRITE_TAC[ADD_CLAUSES]])
2457
2458
2459
2460val EVENTUAL_IDEM = TAC_PROOF(
2461 ([],“EVENTUAL a = EVENTUAL (EVENTUAL a)”),
2462 CONV_TAC (X_FUN_EQ_CONV“t0:num”) THEN GEN_TAC
2463 THEN REWRITE_TAC[EVENTUAL_SIGNAL]
2464 THEN EQ_TAC THEN STRIP_TAC
2465 THENL[
2466 EXISTS_TAC“t:num” THEN EXISTS_TAC“0”
2467 THEN ASM_REWRITE_TAC[ADD_CLAUSES],
2468 EXISTS_TAC“t'+t”THEN UNDISCH_HD_TAC
2469 THEN REWRITE_TAC[ADD_ASSOC]])
2470
2471
2472
2473val WHEN_IDEM = TAC_PROOF(
2474 ([],“(a WHEN b) = ((a WHEN b) WHEN b)”),
2475 CONV_TAC (X_FUN_EQ_CONV“t0:num”) THEN GEN_TAC
2476 THEN REWRITE_TAC[WHEN_SIGNAL] THEN EQ_TAC THEN REPEAT STRIP_TAC
2477 THENL[
2478 LEFT_NO_FORALL_TAC 4 “delta'+delta”
2479 THEN RULE_ASSUM_TAC(REWRITE_RULE[SYM(SPEC_ALL ADD_ASSOC)])
2480 THEN POP_ASSUM MATCH_MP_TAC
2481 THEN ASM_REWRITE_TAC[]
2482 THEN DISJ_CASES_TAC(SPEC“delta':num” num_CASES)
2483 THEN ASM_REWRITE_TAC[ADD_CLAUSES]
2484 THEN LEFT_EXISTS_TAC
2485 THEN POP_ASSUM (fn x=> SUBST1_TAC x THEN RULE_ASSUM_TAC(SUBS[x]))
2486 THEN LEFT_NO_FORALL_TAC 1 “0”
2487 THEN UNDISCH_HD_TAC
2488 THEN ASM_REWRITE_TAC[LESS_0,ADD_CLAUSES],
2489 LEFT_NO_FORALL_TAC 2 “delta:num” THEN UNDISCH_HD_TAC
2490 THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC
2491 THEN LEFT_FORALL_TAC“0” THEN RULE_ASSUM_TAC(REWRITE_RULE[ADD_CLAUSES])
2492 THEN POP_ASSUM MATCH_MP_TAC
2493 THEN ASM_REWRITE_TAC[NOT_LESS_0]])
2494
2495
2496
2497val UNTIL_IDEM = TAC_PROOF(
2498 ([],“(a UNTIL b) = ((a UNTIL b) UNTIL b)”),
2499 CONV_TAC (X_FUN_EQ_CONV“t0:num”) THEN GEN_TAC
2500 THEN REWRITE_TAC[UNTIL_SIGNAL]
2501 THEN RIGHT_LEMMA_DISJ_CASES_TAC DELTA_CASES
2502 THEN ASM_REWRITE_TAC[ADD_ASSOC]
2503 THENL[
2504 EQ_TAC THEN REPEAT STRIP_TAC,
2505 EQ_TAC THEN REPEAT STRIP_TAC
2506 THENL[
2507 LEFT_FORALL_TAC “t'+t”,
2508 LEFT_FORALL_TAC “t:num” THEN LEFT_FORALL_TAC “0”]
2509 THEN UNDISCH_HD_TAC THEN REWRITE_TAC[ADD_CLAUSES]]
2510 THENL[
2511 IMP_RES_TAC LESS_ADD
2512 THEN POP_ASSUM (fn x=> RULE_ASSUM_TAC(SUBS[SYM x]))
2513 THEN LEFT_FORALL_TAC“p:num”
2514 THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[ADD_ASSOC],
2515 LEFT_NO_FORALL_TAC 6 “d':num” THEN UNDISCH_HD_TAC
2516 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
2517 THEN MY_MP_TAC“d'=d''+t”
2518 THENL[ALL_TAC,
2519 DISCH_TAC THEN POP_ASSUM(fn x=> RULE_ASSUM_TAC(SUBS[x]))
2520 THEN LEFT_FORALL_TAC“t'+t” THEN UNDISCH_HD_TAC
2521 THEN ASM_REWRITE_TAC[LESS_MONO_ADD_EQ,ADD_ASSOC]]
2522 THEN DISJ_CASES_TAC (SPECL[“d':num”,“d''+t”]LESS_LESS_CASES)
2523 THENL[ASM_REWRITE_TAC[], POP_ASSUM DISJ_CASES_TAC]
2524 THENL[
2525 ASM_TAC 5 (fn x=> ASSUME_TAC(MATCH_MP LESS_IMP_LESS_OR_EQ x))
2526 THEN ASM_TAC 0 (fn x=> ASSUME_TAC(MATCH_MP SUB_ADD x))
2527 THEN UNDISCH_NO_TAC 2
2528 THEN ASM_TAC 0 (fn x=> SUBST1_TAC(SYM x))
2529 THEN REWRITE_TAC[LESS_MONO_ADD_EQ]
2530 THEN DISCH_TAC THEN POP_NO_ASSUM 6 IMP_RES_TAC
2531 THEN UNDISCH_NO_TAC 1 THEN ASM_REWRITE_TAC[ADD_ASSOC],
2532 POP_NO_ASSUM 7 IMP_RES_TAC
2533 THEN UNDISCH_NO_TAC 5 THEN ASM_REWRITE_TAC[ADD_ASSOC]],
2534 LEFT_NO_FORALL_TAC 3 “d':num”
2535 THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
2536 THEN LEFT_FORALL_TAC “t:num”
2537 THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
2538 THEN LEFT_FORALL_TAC “d'-t”
2539 THEN ASM_TAC 2 (fn x=> ASSUME_TAC(MATCH_MP LESS_IMP_LESS_OR_EQ x))
2540 THEN ASM_TAC 0 (fn x=> ASSUME_TAC(MATCH_MP SUB_ADD x))
2541 THEN UNDISCH_NO_TAC 2
2542 THEN ONCE_REWRITE_TAC[SYM(SPECL[“t'':num”,
2543 “d' - t”,“t:num”]LESS_MONO_ADD_EQ)]
2544 THEN ASM_REWRITE_TAC[ADD_ASSOC] THEN DISCH_TAC
2545 THEN LEFT_FORALL_TAC “0”
2546 THEN RULE_ASSUM_TAC(REWRITE_RULE[ADD_CLAUSES])
2547 THEN RES_TAC])
2548
2549
2550
2551val SWHEN_IDEM = TAC_PROOF(
2552 ([],“(a SWHEN b) = ((a SWHEN b) SWHEN b)”),
2553 CONV_TAC (X_FUN_EQ_CONV“t0:num”) THEN GEN_TAC
2554 THEN REWRITE_TAC[SWHEN_SIGNAL] THEN EQ_TAC THEN REPEAT STRIP_TAC
2555 THENL[
2556 EXISTS_TAC “delta:num” THEN ASM_REWRITE_TAC[]
2557 THEN EXISTS_TAC “0” THEN ASM_REWRITE_TAC[ADD_CLAUSES]
2558 THEN REWRITE_TAC[EQT_ELIM(ARITH_CONV“~(t<0)”)],
2559 MY_MP_TAC “delta' = 0”
2560 THENL[
2561 DISJ_CASES_TAC(SPEC“delta':num”num_CASES)
2562 THEN ASM_REWRITE_TAC[] THEN LEFT_EXISTS_TAC
2563 THEN LEFT_NO_FORALL_TAC 3 “0” THEN UNDISCH_HD_TAC
2564 THEN POP_ASSUM SUBST1_TAC
2565 THEN ASM_REWRITE_TAC[ADD_CLAUSES,LESS_0],
2566 DISCH_TAC]
2567 THEN EXISTS_TAC “delta:num” THEN ASM_REWRITE_TAC[ADD_CLAUSES]
2568 THEN UNDISCH_NO_TAC 1 THEN ASM_REWRITE_TAC[ADD_CLAUSES]])
2569
2570
2571
2572val SUNTIL_IDEM = TAC_PROOF(
2573 ([],“(a SUNTIL b) = ((a SUNTIL b) SUNTIL b)”),
2574 CONV_TAC (X_FUN_EQ_CONV“t0:num”) THEN GEN_TAC
2575 THEN REWRITE_TAC[SUNTIL_SIGNAL] THEN EQ_TAC THEN REPEAT STRIP_TAC
2576 THENL[
2577 EXISTS_TAC “delta:num” THEN ASM_REWRITE_TAC[]
2578 THEN GEN_TAC THEN DISCH_TAC THEN IMP_RES_TAC LESS_ADD
2579 THEN RES_TAC THEN ASM_REWRITE_TAC[]
2580 THEN EXISTS_TAC “p:num” THEN ASM_REWRITE_TAC[ADD_ASSOC]
2581 THEN GEN_TAC THEN DISCH_TAC THEN POP_NO_ASSUM 6 MATCH_MP_TAC
2582 THEN UNDISCH_NO_TAC 3 THEN UNDISCH_NO_TAC 0
2583 THEN CONV_TAC ARITH_CONV,
2584 ALL_TAC]
2585 THEN DISJ_CASES_TAC(SPEC“delta:num”num_CASES)
2586 THENL[
2587 EXISTS_TAC “0”
2588 THEN REWRITE_TAC[EQT_ELIM(ARITH_CONV“~(t<0)”)]
2589 THEN UNDISCH_NO_TAC 1 THEN ASM_REWRITE_TAC[ADD_CLAUSES],
2590 ALL_TAC]
2591 THEN LEFT_EXISTS_TAC THEN POP_ASSUM (fn x=> RULE_ASSUM_TAC(REWRITE_RULE[x]))
2592 THEN LEFT_NO_FORALL_TAC 1 “0” THEN UNDISCH_HD_TAC
2593 THEN REWRITE_TAC[LESS_0,ADD_CLAUSES] THEN STRIP_TAC
2594 THEN EXISTS_TAC “delta:num” THEN ASM_REWRITE_TAC[])
2595
2596
2597
2598
2599val BEFORE_IDEM = TAC_PROOF(
2600 ([],“(a BEFORE b) = ((a BEFORE b) BEFORE b)”),
2601 CONV_TAC(X_FUN_EQ_CONV“t0:num”) THEN BETA_TAC THEN GEN_TAC
2602 THEN ONCE_REWRITE_TAC[DECIDE “(a=b) = (~a= ~b)”]
2603 THEN REWRITE_TAC[NOT_BEFORE]
2604 THEN CONV_TAC(DEPTH_CONV ETA_CONV)
2605 THEN REWRITE_TAC[SYM SUNTIL_IDEM])
2606
2607
2608
2609val SBEFORE_IDEM = TAC_PROOF(
2610 ([],“(a SBEFORE b) = ((a SBEFORE b) SBEFORE b)”),
2611 CONV_TAC(X_FUN_EQ_CONV“t0:num”) THEN BETA_TAC THEN GEN_TAC
2612 THEN ONCE_REWRITE_TAC[DECIDE “(a=b) = (~a= ~b)”]
2613 THEN REWRITE_TAC[NOT_SBEFORE]
2614 THEN CONV_TAC(DEPTH_CONV ETA_CONV)
2615 THEN REWRITE_TAC[SYM UNTIL_IDEM])
2616
2617
2618
2619(* ************************************************************ *)
2620(* Signal Theorems for Translation to LinOrd *)
2621(* ************************************************************ *)
2622
2623
2624
2625val SUNTIL_LINORD = TAC_PROOF(
2626 ([],“(a SUNTIL b) t0 = ?t1. (t0<=t1) /\ b t1 /\ UPTO(t0,t1,a)”),
2627 REWRITE_TAC[SUNTIL_SIGNAL,UPTO] THEN EQ_TAC
2628 THENL[
2629 STRIP_TAC
2630 THEN EXISTS_TAC“delta+t0” THEN ASM_REWRITE_TAC[]
2631 THEN REPEAT STRIP_TAC THENL[CONV_TAC ARITH_CONV,ALL_TAC]
2632 THEN IMP_RES_TAC LESS_EQUAL_ADD
2633 THEN LEFT_NO_FORALL_TAC 4 “p:num”
2634 THEN IMP_RES_TAC(EQT_ELIM(ARITH_CONV
2635 “(t2=t0+p) /\ (t2<delta+t0) ==> p<delta”))
2636 THEN RES_TAC THEN UNDISCH_NO_TAC 1
2637 THEN ONCE_REWRITE_TAC[ADD_SYM]
2638 THEN ASM_REWRITE_TAC[],
2639 DISCH_TAC
2640 THEN ASSUME_TAC(BETA_RULE(SPEC
2641 “\t1.t0<=t1 /\ b t1 /\ (!t2. t0<=t2 /\ t2<t1 ==> a t2)”WOP))
2642 THEN UNDISCH_HD_TAC THEN POP_ASSUM REWRITE1_TAC
2643 THEN REPEAT STRIP_TAC
2644 THEN IMP_RES_TAC LESS_EQUAL_ADD THEN EXISTS_TAC“p:num”
2645 THEN REPEAT STRIP_TAC
2646 THENL[
2647 POP_NO_ASSUM 3 MATCH_MP_TAC
2648 THEN UNDISCH_HD_TAC THEN UNDISCH_HD_TAC
2649 THEN CONV_TAC ARITH_CONV,
2650 LEFT_NO_FORALL_TAC 3 “t+t0”
2651 THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[]
2652 THEN IMP_RES_TAC(EQT_ELIM(ARITH_CONV“t<p ==> t+t0<t0+p”))
2653 THEN POP_ASSUM REWRITE1_TAC
2654 THEN REWRITE_TAC[EQT_ELIM(ARITH_CONV“t0<=t+t0”)]
2655 THEN REPEAT STRIP_TAC THEN POP_NO_ASSUM 5 MATCH_MP_TAC
2656 THEN ASM_REWRITE_TAC[] THEN UNDISCH_HD_TAC
2657 THEN UNDISCH_NO_TAC 2 THEN CONV_TAC ARITH_CONV,
2658 ONCE_REWRITE_TAC[ADD_SYM] THEN POP_ASSUM (SUBST1_TAC o SYM)
2659 THEN ASM_REWRITE_TAC[]
2660 ]
2661 ]);
2662
2663
2664val SWHEN_LINORD = prove(
2665 “(a SWHEN b) t0 = ?t1. (t0<=t1) /\ a t1 /\ b t1 /\ UPTO(t0,t1,(\t.~b t))”,
2666 REWRITE_TAC[SWHEN_SIGNAL,UPTO] THEN BETA_TAC THEN EQ_TAC
2667 THENL[
2668 STRIP_TAC
2669 THEN EXISTS_TAC“delta+t0” THEN ASM_REWRITE_TAC[]
2670 THEN REPEAT STRIP_TAC THENL[CONV_TAC ARITH_CONV,ALL_TAC]
2671 THEN IMP_RES_TAC LESS_EQUAL_ADD
2672 THEN LEFT_NO_FORALL_TAC 6 “p:num”
2673 THEN UNDISCH_NO_TAC 2 THEN ASM_REWRITE_TAC[]
2674 THEN ONCE_REWRITE_TAC[ADD_SYM]
2675 THEN POP_ASSUM MATCH_MP_TAC
2676 THEN UNDISCH_NO_TAC 1 THEN ASM_REWRITE_TAC[]
2677 THEN CONV_TAC ARITH_CONV,
2678 DISCH_TAC
2679 THEN ASSUME_TAC(BETA_RULE(SPEC
2680 “\t1.t0<=t1 /\ a t1 /\ b t1 /\
2681 (!t2. t0<=t2 /\ t2<t1 ==> ~b t2)”WOP))
2682 THEN UNDISCH_HD_TAC THEN POP_ASSUM REWRITE1_TAC
2683 THEN REPEAT STRIP_TAC
2684 THEN IMP_RES_TAC LESS_EQUAL_ADD THEN EXISTS_TAC“p:num”
2685 THEN REPEAT STRIP_TAC
2686 THENL[
2687 UNDISCH_HD_TAC THEN REWRITE_TAC[]
2688 THEN POP_NO_ASSUM 3 MATCH_MP_TAC
2689 THEN UNDISCH_HD_TAC THEN UNDISCH_HD_TAC
2690 THEN CONV_TAC ARITH_CONV,
2691 ONCE_REWRITE_TAC[ADD_SYM] THEN POP_ASSUM (SUBST1_TAC o SYM)
2692 THEN ASM_REWRITE_TAC[],
2693 ONCE_REWRITE_TAC[ADD_SYM] THEN POP_ASSUM (SUBST1_TAC o SYM)
2694 THEN ASM_REWRITE_TAC[]
2695 ]
2696 ]);
2697
2698
2699
2700
2701val SBEFORE_LINORD = prove(
2702 “(a SBEFORE b) t0 = ?t1. (t0<=t1) /\ a t1 /\ ~b t1 /\ UPTO(t0,t1,(\t.~b t))”,
2703 REWRITE_TAC[SBEFORE_SIGNAL,UPTO] THEN BETA_TAC THEN EQ_TAC
2704 THENL[
2705 STRIP_TAC
2706 THEN EXISTS_TAC“delta+t0” THEN ASM_REWRITE_TAC[]
2707 THEN REPEAT STRIP_TAC
2708 THENL[
2709 CONV_TAC ARITH_CONV,
2710 LEFT_NO_FORALL_TAC 1 “delta:num”
2711 THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[LESS_EQ_REFL],
2712 UNDISCH_HD_TAC THEN IMP_RES_TAC LESS_EQUAL_ADD
2713 THEN ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[ADD_SYM]
2714 THEN POP_NO_ASSUM 3 MATCH_MP_TAC
2715 THEN UNDISCH_HD_TAC THEN UNDISCH_HD_TAC
2716 THEN CONV_TAC ARITH_CONV],
2717 DISCH_TAC
2718 THEN ASSUME_TAC(BETA_RULE(SPEC
2719 “\t1.t0<=t1 /\ a t1 /\ ~b t1 /\
2720 (!t2. t0<=t2 /\ t2<t1 ==> ~b t2)”WOP))
2721 THEN UNDISCH_HD_TAC THEN POP_ASSUM REWRITE1_TAC
2722 THEN REPEAT STRIP_TAC
2723 THEN IMP_RES_TAC LESS_EQUAL_ADD THEN EXISTS_TAC“p:num”
2724 THEN REPEAT STRIP_TAC
2725 THENL[
2726 ONCE_REWRITE_TAC[ADD_SYM] THEN POP_ASSUM (SUBST1_TAC o SYM)
2727 THEN ASM_REWRITE_TAC[],
2728 LEFT_NO_FORALL_TAC 4 “t+t0”
2729 THEN UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[]
2730 THEN REWRITE_TAC[EQT_ELIM(ARITH_CONV“t0<=t+t0”)]
2731 THEN UNDISCH_NO_TAC 1 THEN REWRITE_TAC[LESS_OR_EQ]
2732 THEN STRIP_TAC
2733 THENL[UNDISCH_HD_TAC THEN CONV_TAC ARITH_CONV,ALL_TAC]
2734 THEN POP_ASSUM (fn x => RULE_ASSUM_TAC(REWRITE_RULE[x]))
2735 THEN UNDISCH_HD_TAC THEN ONCE_REWRITE_TAC[ADD_SYM]
2736 THEN POP_ASSUM (SUBST1_TAC o SYM)
2737 THEN ASM_REWRITE_TAC[]
2738 ]
2739 ]);
2740
2741
2742
2743
2744val UNTIL_LINORD = prove(
2745 “(a UNTIL b) t0 = !t1. (t0<=t1) /\ ~b t1 /\ UPTO(t0,t1,(\t.~b t)) ==> a t1”,
2746 ONCE_REWRITE_TAC[DECIDE “(a=b) = (~a= ~b)”]
2747 THEN REWRITE_TAC[NOT_UNTIL,SBEFORE_LINORD]
2748 THEN BETA_TAC THEN CONV_TAC(DEPTH_CONV NOT_FORALL_CONV)
2749 THEN REWRITE_TAC[DECIDE “~(a==>b) = (a/\~b)”]
2750 THEN EQ_TAC THEN REPEAT STRIP_TAC
2751 THENL[
2752 EXISTS_TAC“t1:num” THEN ASM_REWRITE_TAC[],
2753 EXISTS_TAC“t1:num” THEN ASM_REWRITE_TAC[]]
2754 );
2755
2756
2757
2758
2759
2760val WHEN_LINORD = prove(
2761 “(a WHEN b) t0 = !t1. (t0<=t1) /\ b t1 /\ UPTO(t0,t1,(\t.~b t)) ==> a t1”,
2762 ONCE_REWRITE_TAC[DECIDE “(a=b) = (~a= ~b)”]
2763 THEN REWRITE_TAC[NOT_WHEN,SWHEN_LINORD]
2764 THEN BETA_TAC THEN CONV_TAC(DEPTH_CONV NOT_FORALL_CONV)
2765 THEN REWRITE_TAC[DECIDE “~(a==>b) = (a/\~b)”]
2766 THEN EQ_TAC THEN REPEAT STRIP_TAC
2767 THENL[
2768 EXISTS_TAC“t1:num” THEN ASM_REWRITE_TAC[],
2769 EXISTS_TAC“t1:num” THEN ASM_REWRITE_TAC[]]
2770 );
2771
2772
2773
2774
2775
2776val BEFORE_LINORD = TAC_PROOF(
2777 ([],“(a BEFORE b) t0 = !t1. (t0<=t1) /\ UPTO(t0,t1,(\t.~a t)) ==> ~b t1”),
2778 ONCE_REWRITE_TAC[DECIDE “(a=b) = (~a= ~b)”]
2779 THEN REWRITE_TAC[NOT_BEFORE,SUNTIL_LINORD]
2780 THEN BETA_TAC THEN CONV_TAC(DEPTH_CONV NOT_FORALL_CONV)
2781 THEN REWRITE_TAC[DECIDE “~(a==>b) = (a/\~b)”]
2782 THEN EQ_TAC THEN REPEAT STRIP_TAC
2783 THENL[
2784 EXISTS_TAC“t1:num” THEN ASM_REWRITE_TAC[],
2785 EXISTS_TAC“t1:num” THEN ASM_REWRITE_TAC[]]
2786 );
2787
2788
2789
2790val ALWAYS_LINORD = TAC_PROOF(
2791 ([],“(ALWAYS a) t0 = !t1. (t0<=t1) ==> a t1”),
2792 REWRITE_TAC[ALWAYS_AS_UNTIL,UNTIL_LINORD,UPTO]
2793 );
2794
2795
2796
2797val EVENTUAL_LINORD = TAC_PROOF(
2798 ([],“(EVENTUAL a) t0 = ?t1. (t0<=t1) /\ a t1”),
2799 REWRITE_TAC[EVENTUAL_AS_SUNTIL,SUNTIL_LINORD,UPTO]
2800 );
2801
2802
2803val NEXT_LINORD = TAC_PROOF(
2804 ([],“(NEXT a) t0 = ?t1. t0<t1 /\ (!t3. t0<t3 ==> t1<=t3) /\ a t1”),
2805 REWRITE_TAC[NEXT] THEN BETA_TAC
2806 THEN EQ_TAC THEN REPEAT STRIP_TAC
2807 THENL[
2808 EXISTS_TAC“SUC t0” THEN ASM_REWRITE_TAC[]
2809 THEN CONV_TAC ARITH_CONV,
2810 MY_MP_TAC “t1 = SUC t0”
2811 THENL[
2812 DISJ_CASES_TAC(EQT_ELIM(ARITH_CONV
2813 “(t1<SUC t0) \/ (t1=SUC t0) \/ (SUC t0<t1)”))
2814 THENL[ALL_TAC,POP_ASSUM DISJ_CASES_TAC]
2815 THENL[
2816 UNDISCH_NO_TAC 3 THEN UNDISCH_NO_TAC 0
2817 THEN CONV_TAC ARITH_CONV,
2818 POP_ASSUM REWRITE1_TAC,
2819 LEFT_NO_FORALL_TAC 2 “SUC t0” THEN UNDISCH_HD_TAC
2820 THEN REWRITE_TAC[EQT_ELIM(ARITH_CONV“t0<SUC t0”)]
2821 THEN UNDISCH_HD_TAC THEN UNDISCH_NO_TAC 1
2822 THEN CONV_TAC ARITH_CONV],
2823 DISCH_TAC]
2824 THEN POP_ASSUM (SUBST1_TAC o SYM)
2825 THEN ASM_REWRITE_TAC[]
2826 ]);
2827
2828
2829(* ************************************************************ *)
2830(* Saving the most interesting theorems *)
2831(* ************************************************************ *)
2832
2833(* ----------------- from file lemmata.sml ------------------ *)
2834val _ = save_thm("WATCH_EXISTS",WATCH_EXISTS);
2835val _ = save_thm("WELL_ORDER",WELL_ORDER);
2836val _ = save_thm("WELL_ORDER_UNIQUE",WELL_ORDER_UNIQUE);
2837
2838(* ----------------- from file hw_imp.sml ------------------ *)
2839val _ = save_thm("WHEN_IMP",WHEN_IMP);
2840val _ = save_thm("UNTIL_IMP",UNTIL_IMP);
2841val _ = save_thm("BEFORE_IMP",BEFORE_IMP);
2842val _ = save_thm("SWHEN_IMP",SWHEN_IMP);
2843val _ = save_thm("SUNTIL_IMP",SUNTIL_IMP);
2844val _ = save_thm("SBEFORE_IMP",SBEFORE_IMP);
2845
2846(* ----------------- from file signal.sml ------------------ *)
2847val _ = save_thm("ALWAYS_SIGNAL",ALWAYS_SIGNAL);
2848val _ = save_thm("EVENTUAL_SIGNAL",EVENTUAL_SIGNAL);
2849val _ = save_thm("WHEN_SIGNAL",WHEN_SIGNAL);
2850val _ = save_thm("UNTIL_SIGNAL",UNTIL_SIGNAL);
2851val _ = save_thm("BEFORE_SIGNAL",BEFORE_SIGNAL);
2852val _ = save_thm("SWHEN_SIGNAL",SWHEN_SIGNAL);
2853val _ = save_thm("SBEFORE_SIGNAL",SBEFORE_SIGNAL);
2854
2855(* ----------------- from file temp2linord.sml ---------------- *)
2856val _ = save_thm("NEXT_LINORD",NEXT_LINORD);
2857val _ = save_thm("ALWAYS_LINORD",ALWAYS_LINORD);
2858val _ = save_thm("EVENTUAL_LINORD",EVENTUAL_LINORD);
2859val _ = save_thm("SUNTIL_LINORD",SUNTIL_LINORD);
2860val _ = save_thm("UNTIL_LINORD",UNTIL_LINORD);
2861val _ = save_thm("SBEFORE_LINORD",SBEFORE_LINORD);
2862val _ = save_thm("BEFORE_LINORD",BEFORE_LINORD);
2863val _ = save_thm("SWHEN_LINORD",SWHEN_LINORD);
2864val _ = save_thm("WHEN_LINORD",WHEN_LINORD);
2865
2866(* ----------------- from file when_expressive.sml ------------------ *)
2867val _ = save_thm("ALWAYS_AS_WHEN",ALWAYS_AS_WHEN);
2868val _ = save_thm("EVENTUAL_AS_WHEN",EVENTUAL_AS_WHEN);
2869val _ = save_thm("UNTIL_AS_WHEN",UNTIL_AS_WHEN);
2870val _ = save_thm("SWHEN_AS_WHEN",SWHEN_AS_WHEN);
2871val _ = save_thm("SWHEN_AS_NOT_WHEN",SWHEN_AS_NOT_WHEN);
2872val _ = save_thm("SUNTIL_AS_WHEN",SUNTIL_AS_WHEN);
2873val _ = save_thm("SBEFORE_AS_WHEN",SBEFORE_AS_WHEN);
2874val _ = save_thm("BEFORE_AS_WHEN_UNTIL",BEFORE_AS_WHEN_UNTIL);
2875val _ = save_thm("BEFORE_HW",BEFORE_HW);
2876
2877(* ----------------- from file until_expressive.sml ------------------ *)
2878val _ = save_thm("ALWAYS_AS_UNTIL",ALWAYS_AS_UNTIL);
2879val _ = save_thm("EVENTUAL_AS_UNTIL",EVENTUAL_AS_UNTIL);
2880val _ = save_thm("WHEN_AS_UNTIL",WHEN_AS_UNTIL);
2881val _ = save_thm("BEFORE_AS_UNTIL",BEFORE_AS_UNTIL);
2882val _ = save_thm("SWHEN_AS_UNTIL",SWHEN_AS_UNTIL);
2883val _ = save_thm("SUNTIL_AS_UNTIL",SUNTIL_AS_UNTIL);
2884val _ = save_thm("SBEFORE_AS_UNTIL",SBEFORE_AS_UNTIL);
2885
2886(* ----------------- from file before_expressive.sml ------------------ *)
2887val _ = save_thm("ALWAYS_AS_BEFORE",ALWAYS_AS_BEFORE);
2888val _ = save_thm("EVENTUAL_AS_BEFORE",EVENTUAL_AS_BEFORE);
2889val _ = save_thm("WHEN_AS_BEFORE",WHEN_AS_BEFORE);
2890val _ = save_thm("UNTIL_AS_BEFORE",UNTIL_AS_BEFORE);
2891val _ = save_thm("SWHEN_AS_BEFORE",SWHEN_AS_BEFORE);
2892val _ = save_thm("SUNTIL_AS_BEFORE",SUNTIL_AS_BEFORE);
2893val _ = save_thm("SBEFORE_AS_BEFORE",SBEFORE_AS_BEFORE);
2894
2895(* ----------------- from file swhen_expressive.sml ------------------ *)
2896val _ = save_thm("WHEN_SWHEN_LEMMA",WHEN_SWHEN_LEMMA);
2897
2898val _ = save_thm("ALWAYS_AS_SWHEN",ALWAYS_AS_SWHEN);
2899val _ = save_thm("EVENTUAL_AS_SWHEN",EVENTUAL_AS_SWHEN);
2900val _ = save_thm("WHEN_AS_SWHEN",WHEN_AS_SWHEN);
2901val _ = save_thm("WHEN_AS_NOT_SWHEN",WHEN_AS_NOT_SWHEN);
2902val _ = save_thm("UNTIL_AS_SWHEN",UNTIL_AS_SWHEN);
2903val _ = save_thm("BEFORE_AS_SWHEN",BEFORE_AS_SWHEN);
2904val _ = save_thm("BEFORE_AS_NOT_SWHEN",BEFORE_AS_NOT_SWHEN);
2905val _ = save_thm("SUNTIL_AS_SWHEN",SUNTIL_AS_SWHEN);
2906val _ = save_thm("SBEFORE_AS_SWHEN",SBEFORE_AS_SWHEN);
2907
2908(* ----------------- from file suntil_expressive.sml ------------------ *)
2909val _ = save_thm("ALWAYS_AS_SUNTIL",ALWAYS_AS_SUNTIL);
2910val _ = save_thm("EVENTUAL_AS_SUNTIL",EVENTUAL_AS_SUNTIL);
2911val _ = save_thm("WHEN_AS_SUNTIL",WHEN_AS_SUNTIL);
2912val _ = save_thm("UNTIL_AS_SUNTIL",UNTIL_AS_SUNTIL);
2913val _ = save_thm("BEFORE_AS_SUNTIL",BEFORE_AS_SUNTIL);
2914val _ = save_thm("SWHEN_AS_SUNTIL",SWHEN_AS_SUNTIL);
2915val _ = save_thm("SBEFORE_AS_SUNTIL",SBEFORE_AS_SUNTIL);
2916
2917(* ----------------- from file sbefore_expressive.sml ------------------ *)
2918val _ = save_thm("ALWAYS_AS_SBEFORE",ALWAYS_AS_SBEFORE);
2919val _ = save_thm("EVENTUAL_AS_SBEFORE",EVENTUAL_AS_SBEFORE);
2920val _ = save_thm("WHEN_AS_SBEFORE",WHEN_AS_SBEFORE);
2921val _ = save_thm("UNTIL_AS_SBEFORE",UNTIL_AS_SBEFORE);
2922val _ = save_thm("SWHEN_AS_SBEFORE",SWHEN_AS_SBEFORE);
2923val _ = save_thm("SUNTIL_AS_SBEFORE",SUNTIL_AS_SBEFORE);
2924val _ = save_thm("BEFORE_AS_SBEFORE",BEFORE_AS_SBEFORE);
2925
2926(* ----------------- from file simplify.sml ------------------ *)
2927val _ = save_thm("WHEN_SIMP",WHEN_SIMP);
2928val _ = save_thm("UNTIL_SIMP",UNTIL_SIMP);
2929val _ = save_thm("BEFORE_SIMP",BEFORE_SIMP);
2930val _ = save_thm("SWHEN_SIMP",SWHEN_SIMP);
2931val _ = save_thm("SUNTIL_SIMP",SUNTIL_SIMP);
2932val _ = save_thm("SBEFORE_SIMP",SBEFORE_SIMP);
2933val _ = save_thm("WHEN_EVENT",WHEN_EVENT);
2934val _ = save_thm("UNTIL_EVENT",UNTIL_EVENT);
2935val _ = save_thm("BEFORE_EVENT",BEFORE_EVENT);
2936val _ = save_thm("SWHEN_EVENT",SWHEN_EVENT);
2937val _ = save_thm("SUNTIL_EVENT",SUNTIL_EVENT);
2938val _ = save_thm("SBEFORE_EVENT",SBEFORE_EVENT);
2939val _ = save_thm("IMMEDIATE_EVENT",IMMEDIATE_EVENT);
2940val _ = save_thm("NO_EVENT",NO_EVENT);
2941val _ = save_thm("SOME_EVENT",SOME_EVENT);
2942val _ = save_thm("MORE_EVENT",MORE_EVENT);
2943
2944(* ----------------- from file next_homo.sml ------------------ *)
2945val _ = save_thm("NOT_NEXT",NOT_NEXT);
2946val _ = save_thm("AND_NEXT",AND_NEXT);
2947val _ = save_thm("OR_NEXT",OR_NEXT);
2948val _ = save_thm("IMP_NEXT",IMP_NEXT);
2949val _ = save_thm("EQUIV_NEXT",EQUIV_NEXT);
2950val _ = save_thm("ALWAYS_NEXT",ALWAYS_NEXT);
2951val _ = save_thm("EVENTUAL_NEXT",EVENTUAL_NEXT);
2952val _ = save_thm("WHEN_NEXT",WHEN_NEXT);
2953val _ = save_thm("UNTIL_NEXT",UNTIL_NEXT);
2954val _ = save_thm("BEFORE_NEXT",BEFORE_NEXT);
2955val _ = save_thm("SWHEN_NEXT",SWHEN_NEXT);
2956val _ = save_thm("SUNTIL_NEXT",SUNTIL_NEXT);
2957val _ = save_thm("SBEFORE_NEXT",SBEFORE_NEXT);
2958
2959(* ----------------- from file recursion.sml ------------------ *)
2960val _ = save_thm("ALWAYS_REC",ALWAYS_REC);
2961val _ = save_thm("EVENTUAL_REC",EVENTUAL_REC);
2962val _ = save_thm("WATCH_REC",WATCH_REC);
2963val _ = save_thm("WHEN_REC",WHEN_REC);
2964val _ = save_thm("UNTIL_REC",UNTIL_REC);
2965val _ = save_thm("BEFORE_REC",BEFORE_REC);
2966val _ = save_thm("SWHEN_REC",SWHEN_REC);
2967val _ = save_thm("SUNTIL_REC",SUNTIL_REC);
2968val _ = save_thm("SBEFORE_REC",SBEFORE_REC);
2969
2970(* ----------------- from file fixpoints.sml ------------------ *)
2971val _ = save_thm("ALWAYS_FIX",ALWAYS_FIX);
2972val _ = save_thm("EVENTUAL_FIX",EVENTUAL_FIX);
2973val _ = save_thm("WHEN_FIX",WHEN_FIX);
2974val _ = save_thm("UNTIL_FIX",UNTIL_FIX);
2975val _ = save_thm("BEFORE_FIX",BEFORE_FIX);
2976
2977(* ----------------- from file invariant.sml ------------------ *)
2978val _ = save_thm("WHEN_INVARIANT",WHEN_INVARIANT);
2979val _ = save_thm("UNTIL_INVARIANT",UNTIL_INVARIANT);
2980val _ = save_thm("BEFORE_INVARIANT",BEFORE_INVARIANT);
2981val _ = save_thm("ALWAYS_INVARIANT",ALWAYS_INVARIANT);
2982val _ = save_thm("EVENTUAL_INVARIANT",EVENTUAL_INVARIANT);
2983val _ = save_thm("SWHEN_INVARIANT",SWHEN_INVARIANT);
2984val _ = save_thm("SUNTIL_INVARIANT",SUNTIL_INVARIANT);
2985val _ = save_thm("SBEFORE_INVARIANT",SBEFORE_INVARIANT);
2986
2987(* ----------------- from file idem.sml ------------------ *)
2988val _ = save_thm("ALWAYS_IDEM",ALWAYS_IDEM);
2989val _ = save_thm("EVENTUAL_IDEM",EVENTUAL_IDEM);
2990val _ = save_thm("WHEN_IDEM",WHEN_IDEM);
2991val _ = save_thm("UNTIL_IDEM",UNTIL_IDEM);
2992val _ = save_thm("BEFORE_IDEM",BEFORE_IDEM);
2993val _ = save_thm("SWHEN_IDEM",SWHEN_IDEM);
2994val _ = save_thm("SUNTIL_IDEM",SUNTIL_IDEM);
2995val _ = save_thm("SBEFORE_IDEM",SBEFORE_IDEM);
2996
2997(* ----------------- from file negation.sml ------------------ *)
2998val _ = save_thm("NOT_ALWAYS",NOT_ALWAYS);
2999val _ = save_thm("NOT_EVENTUAL",NOT_EVENTUAL);
3000val _ = save_thm("NOT_WHEN",NOT_WHEN);
3001val _ = save_thm("NOT_UNTIL",NOT_UNTIL);
3002val _ = save_thm("NOT_BEFORE",NOT_BEFORE);
3003val _ = save_thm("NOT_SWHEN",NOT_SWHEN);
3004val _ = save_thm("NOT_SUNTIL",NOT_SUNTIL);
3005val _ = save_thm("NOT_SBEFORE",NOT_SBEFORE);
3006
3007
3008(* html_theory "-"; *)