1 (*-------------------------------------------------------------------------*)
6 This file defines the theorems for the UNLESS definition.
8 Author: (c) Copyright 1989-2008 by Flemming Andersen
10 Last Update: December 30, 2007
12 (*-------------------------------------------------------------------------*)
15 (*-------------------------------------------------------------------------*)
16 (* The definition of UNLESS is based on the definition:
18 p UNLESS q in Pr = <!s in Pr: {p /\ ~q} s {p \/ q}>
20 where p and q are state dependent first order logic predicates or all
21 s in the program Pr are conditionally enabled statements transforming
22 a state into a new state.
24 To define UNLESS as a relation UNLESS_STMT to be satisfied for a finite
25 number of program statements, we define the UNLESS_STMT to be fulfilled as
26 a separate HOARE tripple relation between pre- or post predicates to be
27 satisfied for state transitions. The pre- or post predicates of the
28 UNLESS_STMT relation must be satisfiable for all states possible in the
29 finite state space of the program.
34 let UNLESS_STMT = new_infix_definition
35 ("UNLESS_STMT", "<=>",
36 `UNLESS_STMT (p:'a->bool) q st =
37 \s:'a. (p s /\ ~q s) ==> (p (st s) \/ q (st s))`, TL_FIX);;
40 Since a program is defined as a set (list) of statements, we
41 recursively define the UNLESS relation itself using the UNLESS_STMT
42 relation to be satisfied for every statement in the program.
44 As the bottom of the recursion we choose the empty program always to be
45 satisfied. For every statement in the program the UNLESS_STMT relation
46 must be satisfied in all possible states.
50 (`(!p q. UNLESS p q [] <=> T) /\
51 (!p q. UNLESS p q (CONS (st:'a->'a) Pr) <=>
52 ((!s:'a. (p UNLESS_STMT q) st s) /\ (UNLESS p q Pr)))`);;
53 let UNLESS = new_recursive_definition list_RECURSION UNLESS_term;;
54 parse_as_infix ( "UNLESS", (TL_FIX, "right") );;
56 let STABLE_STMT = new_infix_definition
57 ("STABLE_STMT", "<=>",
58 `STABLE_STMT (p:'a->bool) st = \s:'a. p s ==> p (st s)`, TL_FIX);;
61 * The state predicate STABLE is a special case of UNLESS.
63 * stable p in Pr = p unless false in Pr
65 let STABLE = new_infix_definition
66 ("STABLE", "<=>", `STABLE (p:'a->bool) Pr = (p UNLESS False) Pr`, TL_FIX);;
69 * The state predicate INVARIANT is a special case of UNLESS too.
70 * However invariant is dependent of a program /\* its initial state.
72 * invariant P in (initial condition, Pr) =
73 * (initial condition ==> p) /\ (p stable in Pr)
75 let INVARIANT = new_infix_definition
77 `INVARIANT p (p0, Pr) = ((!s:'a. p0 s ==> p s) /\ (p STABLE Pr))`, TL_FIX);;
79 (************************************************************************
81 * Lemmas used in the UNLESS Theory *
83 ************************************************************************)
86 let p = `p:'a->bool`;;
87 let q = `q:'a->bool`;;
88 let r = `r:'a->bool`;;
89 let P = `P:num->'a->bool`;;
91 let IMP_IMP_CONJIMP_lemma = TAC_PROOF
93 (`!p q ps qs p' q' p's q's.
94 (p /\ ~q ==> ps \/ qs) ==> (p' /\ ~q' ==> p's \/ q's) ==>
95 (p /\ p' /\ (~p \/ ~q') /\ (~p' \/ ~q) /\ (~q \/ ~q') ==>
96 ps /\ p's \/ ps /\ q's \/ p's /\ qs \/ qs /\ q's)`)),
97 REPEAT STRIP_TAC THEN RES_TAC THEN ASM_REWRITE_TAC []);;
99 let NOT_NOT_OR_lemma = TAC_PROOF
101 (`!t1 t2 t3. t1 \/ t2 \/ t3 <=> ~(~t1 /\ ~t2) \/ t3`)),
102 REWRITE_TAC [NOT_CLAUSES; DE_MORGAN_THM; (SYM (SPEC_ALL DISJ_ASSOC))]);;
104 let CONJ_IMPLY_THM = TAC_PROOF
107 ((p \/ p') /\ (p \/ ~q') /\ (p' \/ ~q) /\ (~q \/ ~q')) =
108 ((p /\ ~q) \/ (p' /\ ~q'))`)),
111 REPEAT STRIP_TAC THEN REPEAT (ASM_REWRITE_TAC []));;
113 (************************************************************************
115 * Theorems about UNLESS_STMT *
117 ************************************************************************)
120 * The reflexivity theorem:
122 * p unless_stmt P in Prog
124 let UNLESS_STMT_thm0 = prove_thm
126 `!p st (s:'a). (p UNLESS_STMT p)st s`,
127 REPEAT STRIP_TAC THEN
128 REWRITE_TAC [UNLESS_STMT] THEN
129 REWRITE_TAC [BETA_CONV (`(\s:'a. p s /\ ~(p s) ==> p (st s))s`)] THEN
130 REPEAT STRIP_TAC THEN
135 * p unless_stmt Q in stmt, q ==> r
136 * ------------------------------
137 * p unless_stmt r in stmt
140 let UNLESS_STMT_thm1 = prove_thm
142 `!(p:'a->bool) q r st.
143 ((!s. (p UNLESS_STMT q) st s) /\ (!s. (q s) ==> (r s))) ==>
144 (!s. (p UNLESS_STMT r) st s)`,
146 REWRITE_TAC [UNLESS_STMT] THEN
147 REPEAT STRIP_TAC THEN
148 ASSUME_TAC (REWRITE_RULE [ASSUME `~r (s:'a)`]
149 ( CONTRAPOS (SPEC `s:'a` (ASSUME `!s:'a. q s ==> r s`)))) THEN
150 STRIP_ASSUME_TAC (REWRITE_RULE [ASSUME `(p:'a->bool) s`; ASSUME `~q (s:'a)`]
151 (SPEC `s:'a` (ASSUME `!s:'a. p s /\ ~q s ==> p (st s) \/ q (st s)`))) THEN
152 ASM_REWRITE_TAC [] THEN
153 STRIP_ASSUME_TAC (REWRITE_RULE [ASSUME `(q:'a->bool) ((st:'a->'a) s)`]
154 (SPEC `(st:'a->'a) s` (ASSUME `!s:'a. q s ==> r s`))) THEN
155 ASM_REWRITE_TAC []);;
159 p unless_stmt Q in st, p' unless_stmt q' in st
160 ------------------------------------------------
161 p\/p' unless_stmt q\/q' in st
163 let UNLESS_STMT_thm2 = prove_thm
165 `!p q p' q' (st:'a->'a).
166 ((!s. (p UNLESS_STMT q) st s) /\ (!s. (p' UNLESS_STMT q') st s)) ==>
167 (!s. ((p \/* p') UNLESS_STMT (q \/* q')) st s)`,
168 REWRITE_TAC [UNLESS_STMT;OR_def] THEN
169 CONV_TAC (DEPTH_CONV BETA_CONV) THEN
170 REWRITE_TAC [GEN_ALL (SYM (SPEC_ALL CONJ_ASSOC));
171 (SYM (SPEC_ALL DISJ_ASSOC)); NOT_CLAUSES; DE_MORGAN_THM] THEN
172 (REPEAT STRIP_TAC THEN RES_TAC THEN ASM_REWRITE_TAC []));;
176 p unless_stmt Q in stmt, p' unless_stmt q' in stmt
177 ------------------------------------------------------------------
178 (p /\ p') unless_stmt (p /\ q') \/ (p' /\ q) \/ (q /\ q') in stmt
180 let UNLESS_STMT_thm3 = prove_thm
182 `!p q p' q' (st:'a->'a).
183 ((!s. (p UNLESS_STMT q) st s) /\ (!s. (p' UNLESS_STMT q') st s)) ==>
184 (!s. ((p /\* p') UNLESS_STMT
185 (((p /\* q') \/* (p' /\* q)) \/* (q /\* q'))) st s)`,
186 PURE_REWRITE_TAC [UNLESS_STMT;AND_def;OR_def] THEN
187 CONV_TAC (DEPTH_CONV BETA_CONV) THEN
188 REWRITE_TAC [GEN_ALL (SYM (SPEC_ALL CONJ_ASSOC));
189 (SYM (SPEC_ALL DISJ_ASSOC)); NOT_CLAUSES; DE_MORGAN_THM] THEN
190 STRIP_TAC THEN STRIP_TAC THEN STRIP_TAC THEN STRIP_TAC THEN STRIP_TAC THEN
191 DISCH_TAC THEN STRIP_TAC THEN DISCH_TAC THEN
192 ASSUME_TAC (CONJUNCT1 (ASSUME
193 (`(!s. p s /\ ~q s ==> p ((st:'a->'a) s) \/ q (st s)) /\
194 (!s. p' s /\ ~q' s ==> p'((st:'a->'a) s) \/ q'(st s))`))) THEN
195 ASSUME_TAC (CONJUNCT2 (ASSUME
196 (`(!s. p s /\ ~q s ==> p ((st:'a->'a) s) \/ q (st s)) /\
197 (!s. p' s /\ ~q' s ==> p'((st:'a->'a) s) \/ q'(st s))`))) THEN
198 STRIP_ASSUME_TAC (SPEC_ALL (ASSUME
199 (`(!s. p s /\ ~q s ==> p ((st:'a->'a) s) \/ q (st s))`))) THEN
200 STRIP_ASSUME_TAC (SPEC_ALL (ASSUME
201 (`(!s. p' s /\ ~q' s ==> p'((st:'a->'a) s) \/ q'(st s))`))) THEN
202 ASSUME_TAC (UNDISCH_ALL
203 (SPEC (`(q':'a->bool) ((st:'a->'a) s)`)
204 (SPEC (`(p':'a->bool) ((st:'a->'a) s)`)
205 (SPEC (`(q':'a->bool) s`)
206 (SPEC (`(p':'a->bool) s`)
207 (SPEC (`(q:'a->bool) ((st:'a->'a) s)`)
208 (SPEC (`(p:'a->bool) ((st:'a->'a) s)`)
209 (SPEC (`(q:'a->bool) s`)
210 (SPEC (`(p:'a->bool) s`)
211 IMP_IMP_CONJIMP_lemma))))))))) THEN
212 ASM_REWRITE_TAC []);;
216 p unless_stmt Q in stmt, p' unless_stmt q' in stmt
217 ------------------------------------------------------------------
218 (p \/ p') unless_stmt (~p /\ q') \/ (~p' /\ q) \/ (q /\ q') in stmt
220 let UNLESS_STMT_thm4 = prove_thm
222 `!p q p' q' (st:'a->'a).
223 ((!s. (p UNLESS_STMT q) st s) /\ (!s. (p' UNLESS_STMT q') st s)) ==>
224 (!s. ((p \/* p') UNLESS_STMT
225 ((((Not p) /\* q') \/* ((Not p') /\* q)) \/* (q /\* q')))
228 PURE_REWRITE_TAC [UNLESS_STMT;AND_def;OR_def;NOT_def1] THEN
231 let UNLESS_STMT_thm5_lemma1 = TAC_PROOF
233 `!p q r. (p ==> q) ==> (p \/ r ==> q \/ r)`),
234 REPEAT STRIP_TAC THENL
235 [RES_TAC THEN ASM_REWRITE_TAC []
236 ;ASM_REWRITE_TAC []]);;
238 let UNLESS_STMT_thm5_lemma2 = TAC_PROOF
240 `!(P:num->('a->bool)) q s. ((?n. P n s) \/ q s) = (?n. P n s \/ q s)`),
241 REPEAT GEN_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL
242 [ EXISTS_TAC (`n:num`) THEN
244 ; EXISTS_TAC (`n:num`) THEN
247 EXISTS_TAC (`n:num`) THEN
253 let UNLESS_STMT_thm5 = prove_thm
255 `!(P:num->('a->bool)) q st.
256 (!m. (!s. ((P m) UNLESS_STMT q)st s)) ==>
257 (!s. ((\s. ?n. P n s) UNLESS_STMT q)st s)`,
259 REWRITE_TAC [UNLESS_STMT] THEN
261 REPEAT STRIP_TAC THEN
262 REWRITE_TAC [UNLESS_STMT_thm5_lemma2] THEN
263 EXISTS_TAC (`n:num`) THEN
265 ASM_REWRITE_TAC []);;
267 let UNLESS_STMT_thm6 = prove_thm
269 `!(p:'a->bool) q r (st:'a->'a).
270 (!s. (p UNLESS_STMT q) st s) ==>
271 (!s. ((p \/* r) UNLESS_STMT (q \/* r)) st s)`,
273 REWRITE_TAC [UNLESS_STMT; OR_def] THEN
277 Theorems about UNLESS
281 The reflexivity theorem:
285 let UNLESS_thm1 = prove_thm
287 `!(p:'a->bool) Pr. (p UNLESS p) Pr`,
290 PURE_REWRITE_TAC [UNLESS] THEN
291 ASM_REWRITE_TAC [] THEN
292 PURE_REWRITE_TAC [UNLESS_STMT] THEN
293 CONV_TAC (DEPTH_CONV BETA_CONV) THEN
294 REPEAT STRIP_TAC THEN
298 * The anti reflexivity theorem:
300 * p unless ~p in Prog
302 let UNLESS_thm2 = prove_thm
304 (`!(p:'a->bool) Pr. (p UNLESS (Not p)) Pr`),
307 PURE_REWRITE_TAC [UNLESS] THEN
308 ASM_REWRITE_TAC [] THEN
309 PURE_REWRITE_TAC [UNLESS_STMT;NOT_def1] THEN
310 CONV_TAC (DEPTH_CONV BETA_CONV) THEN
311 REPEAT STRIP_TAC THEN
312 REWRITE_TAC [EXCLUDED_MIDDLE]);;
315 The unless implies theorem:
316 p unless q in Pr, q ==> r
317 ---------------------------
320 let UNLESS_thm3 = prove_thm
322 `!(p:'a->bool) q r Pr.
323 (((p UNLESS q) Pr) /\ (!s. (q s) ==> (r s))) ==> ((p UNLESS r) Pr)`,
324 GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN
326 REWRITE_TAC [UNLESS] THEN
328 ASM_REWRITE_TAC [] THEN
330 ASM_REWRITE_TAC [] THEN
331 IMP_RES_TAC UNLESS_STMT_thm1);;
335 p unless q in Pr, p' unless q' in Pr
336 -----------------------------------------------------------
337 (p /\ p') unless (p /\ q') \/ (p' /\ q) \/ (q /\ q') in Pr
339 let UNLESS_thm4 = prove_thm
341 `!(p:'a->bool) q p' q' Pr.
342 (((p UNLESS q) Pr) /\ ((p' UNLESS q') Pr)) ==>
344 (((p /\* q') \/* (p' /\* q)) \/* (q /\* q'))) Pr)`,
345 GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN
347 REWRITE_TAC [UNLESS] THEN
349 ASM_REWRITE_TAC [] THEN
351 ASM_REWRITE_TAC [] THEN
352 IMP_RES_TAC UNLESS_STMT_thm3);;
356 p unless q in Pr, p' unless q' in Pr
357 -------------------------------------------------------------
358 (p \/ p') unless (~p /\ q') \/ (~p' /\ q) \/ (q /\ q') in Pr
360 let UNLESS_thm5 = prove_thm
362 `!(p:'a->bool) q p' q' Pr.
363 (((p UNLESS q) Pr) /\ ((p' UNLESS q') Pr))
366 ((((Not p) /\* q') \/* ((Not p') /\* q)) \/* (q /\* q'))) Pr)`,
367 GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN
369 REWRITE_TAC [UNLESS] THEN
371 ASM_REWRITE_TAC [] THEN
373 ASM_REWRITE_TAC [] THEN
374 IMP_RES_TAC UNLESS_STMT_thm4);;
377 Simple Conjunction Theorem:
378 p unless q in Pr, p' unless q' in Pr
379 -------------------------------------------
380 (p /\ p') unless (q \/ q') in Pr
382 let UNLESS_thm6 = prove_thm
384 `!(p:'a->bool) q p' q' Pr.
385 (((p UNLESS q) Pr) /\ ((p' UNLESS q') Pr)) ==>
386 (((p /\* p') UNLESS (q \/* q')) Pr)`,
387 REPEAT STRIP_TAC THEN
388 ASSUME_TAC (UNDISCH_ALL (SPECL
389 [(`((p:'a->bool) UNLESS q)Pr`);
390 (`((p':'a->bool) UNLESS q')Pr`)]
392 ASSUME_TAC (UNDISCH_ALL (SPEC_ALL UNLESS_thm4)) THEN
393 ASSUME_TAC (SPECL [(`p:'a->bool`); (`q:'a->bool`);
394 (`p':'a->bool`); (`q':'a->bool`)]
395 IMPLY_WEAK_lemma1) THEN
396 ASSUME_TAC (UNDISCH_ALL (SPECL
397 [(`(((p:'a->bool) /\* p') UNLESS
398 (((p /\* q') \/* (p' /\* q)) \/* (q /\* q')))Pr`);
399 (`!s. ((((p:'a->bool) /\* q') \/* (p' /\* q)) \/* (q /\* q'))s ==>
402 ASM_REWRITE_TAC [UNDISCH_ALL (SPECL
403 [(`(p:'a->bool) /\* p'`);
404 (`((((p:'a->bool) /\* q') \/* (p' /\* q)) \/* (q /\* q'))`);
405 (`(q:'a->bool) \/* q'`); (`Pr:('a->'a)list`)]
409 Simple Disjunction Theorem:
410 p unless Q in Pr, p' unless q' in Pr
411 ---------------------------------------
412 (p \/ p') unless (q \/ q') in Pr
414 let UNLESS_thm7 = prove_thm
416 `!(p:'a->bool) q p' q' Pr.
417 (((p UNLESS q) Pr) /\ ((p' UNLESS q') Pr)) ==>
418 (((p \/* p') UNLESS (q \/* q')) Pr)`,
419 REPEAT STRIP_TAC THEN
420 ASSUME_TAC (UNDISCH_ALL (SPECL
421 [(`((p:'a->bool) UNLESS q)Pr`); (`((p':'a->bool) UNLESS q')Pr`)]
423 ASSUME_TAC (UNDISCH_ALL (SPEC_ALL UNLESS_thm5)) THEN
424 ASSUME_TAC (SPECL [(`p:'a->bool`); (`q:'a->bool`);
425 (`p':'a->bool`); (`q':'a->bool`)]
426 IMPLY_WEAK_lemma2) THEN
427 ASSUME_TAC (UNDISCH_ALL (SPECL
428 [(`(((p:'a->bool) \/* p') UNLESS
429 ((((Not p) /\* q') \/* ((Not p') /\* q)) \/* (q /\* q')))
431 (`!s. ((((Not (p:'a->bool)) /\* q') \/* ((Not p') /\* q)) \/*
432 (q /\* q'))s ==> (q \/* q')s`)]
434 STRIP_ASSUME_TAC (UNDISCH_ALL (SPECL
435 [`(p:'a->bool) \/* p'`;
436 `(((Not (p:'a->bool)) /\* q') \/* ((Not p') /\* q)) \/* (q /\* q')`;
437 `(q:'a->bool) \/* q'`;
442 Cancellation Theorem:
443 p unless Q in Pr, q unless r in Pr
444 ------------------------------------
445 (p \/ q) unless r in Pr
447 let UNLESS_thm8 = prove_thm
449 `!(p:'a->bool) q r Pr.
450 (((p UNLESS q) Pr) /\ ((q UNLESS r) Pr)) ==>
451 (((p \/* q) UNLESS r) Pr)`,
452 REPEAT STRIP_TAC THEN
453 ASSUME_TAC (UNDISCH_ALL (SPECL
454 [`((p:'a->bool) UNLESS q)Pr`; `((q:'a->bool) UNLESS r)Pr`]
456 ASSUME_TAC (UNDISCH_ALL (SPEC_ALL (SPECL
457 [(`p:'a->bool`); (`q:'a->bool`);
458 (`q:'a->bool`); (`r:'a->bool`)]
461 [(`p:'a->bool`); (`q:'a->bool`); (`r:'a->bool`)]
462 IMPLY_WEAK_lemma3) THEN
463 ASSUME_TAC (UNDISCH_ALL (SPECL
464 [(`(((p:'a->bool) \/* q) UNLESS
465 ((((Not p) /\* r) \/* ((Not q) /\* q)) \/* (q /\* r))) Pr`);
466 (`!s:'a. ((((Not p) /\* r) \/* ((Not q) /\* q)) \/*
467 (q /\* r))s ==> r s`)]
469 STRIP_ASSUME_TAC (UNDISCH_ALL (SPEC_ALL (SPECL
470 [(`((p:'a->bool) \/* q)`);
471 (`((((Not (p:'a->bool)) /\* r) \/* ((Not q) /\* q)) \/*
479 let UNLESS_cor1 = prove_thm
481 `!(p:'a->bool) q Pr. (!s. p s ==> q s) ==> ((p UNLESS q) Pr)`,
482 REPEAT STRIP_TAC THEN
483 ASSUME_TAC (SPEC_ALL UNLESS_thm1) THEN
484 ASSUME_TAC (UNDISCH_ALL (SPECL
485 [`((p:'a->bool) UNLESS p)Pr`; `!s:'a. p s ==> q s`]
487 ASM_REWRITE_TAC [UNDISCH_ALL (SPECL
488 [(`p:'a->bool`); (`p:'a->bool`); (`q:'a->bool`);
489 (`Pr:('a->'a)list`)] UNLESS_thm3)]);;
491 let UNLESS_cor2 = prove_thm
493 (`!(p:'a->bool) q Pr. (!s. (Not p)s ==> q s) ==> ((p UNLESS q) Pr)`),
494 REPEAT STRIP_TAC THEN
495 ASSUME_TAC (SPEC_ALL UNLESS_thm2) THEN
496 ASSUME_TAC (UNDISCH_ALL (SPECL
497 [(`((p:'a->bool) UNLESS (Not p))Pr`);
498 (`!s:'a. (Not p) s ==> q s`)]
500 ASM_REWRITE_TAC [UNDISCH_ALL (SPECL
501 [(`p:'a->bool`); (`Not (p:'a->bool)`);
502 (`q:'a->bool`); (`Pr:('a->'a)list`)]
505 let UNLESS_cor3a = TAC_PROOF
507 (`!(p:'a->bool) q r Pr.
508 (p UNLESS (q \/* r)) Pr ==>
509 ((p /\* (Not q)) UNLESS (q \/* r)) Pr`)),
511 ASSUME_TAC (SPECL [(`Not (q:'a->bool)`);
512 (`Pr:('a->'a)list`)] UNLESS_thm2) THEN
513 UNDISCH_TAC (`((Not (q:'a->bool)) UNLESS (Not(Not q)))Pr`) THEN
514 REWRITE_TAC [NOT_NOT_lemma] THEN
515 REPEAT STRIP_TAC THEN
516 ASSUME_TAC (UNDISCH_ALL (SPECL
517 [(`((p:'a->bool) UNLESS (q \/* r))Pr`);
518 (`((Not (q:'a->bool)) UNLESS q)Pr`)]
520 ASSUME_TAC (UNDISCH_ALL (SPECL
521 [(`p:'a->bool`); (`((q:'a->bool) \/* r)`);
522 (`(Not (q:'a->bool))`); (`q:'a->bool`); (`Pr:('a->'a)list`)]
524 UNDISCH_TAC (`(((p:'a->bool) /\* (Not q)) UNLESS
525 ((q \/* r) \/* q))Pr`) THEN
526 PURE_ONCE_REWRITE_TAC
527 [SPECL [(`(q:'a->bool) \/* r`);
528 (`q:'a->bool`)] OR_COMM_lemma] THEN
529 REWRITE_TAC [GEN_ALL (SYM (SPEC_ALL OR_ASSOC_lemma))] THEN
530 REWRITE_TAC [OR_OR_lemma]);;
532 let UNLESS_cor3b = TAC_PROOF
534 (`!(p:'a->bool) q r Pr.
535 ((p /\* (Not q)) UNLESS (q \/* r)) Pr ==> (p UNLESS (q \/* r)) Pr`)),
536 REPEAT STRIP_TAC THEN
537 ASSUME_TAC (SPECL [(`(p:'a->bool) /\* q`);
538 (`Pr:('a->'a)list`)] UNLESS_thm1) THEN
539 ASSUME_TAC (SPECL [(`p:'a->bool`); (`q:'a->bool`)]
540 AND_IMPLY_WEAK_lemma) THEN
541 ASSUME_TAC (UNDISCH_ALL (SPECL
542 [(`(((p:'a->bool) /\* q) UNLESS (p /\* q))Pr`);
543 (`!s:'a. (p /\* q)s ==> q s`)]
545 ASSUME_TAC (UNDISCH_ALL (SPECL
546 [(`(p:'a->bool) /\* q`); (`(p:'a->bool) /\* q`);
547 (`q:'a->bool`); (`Pr:('a->'a)list`)]
549 ASSUME_TAC (UNDISCH_ALL (SPECL
550 [(`(((p:'a->bool) /\* (Not q)) UNLESS (q \/* r))Pr`);
551 (`(((p:'a->bool) /\* q) UNLESS q)Pr`)]
553 ASSUME_TAC (UNDISCH_ALL (SPECL
554 [(`((p:'a->bool) /\* (Not q))`); (`((q:'a->bool) \/* r)`);
555 (`((p:'a->bool) /\* q)`); (`q:'a->bool`); (`Pr:('a->'a)list`)]
558 (`((((p:'a->bool) /\* (Not q)) \/* (p /\* q)) UNLESS
559 ((q \/* r) \/* q))Pr`) THEN
560 REWRITE_TAC [AND_COMPL_OR_lemma] THEN
561 ONCE_REWRITE_TAC [OR_COMM_lemma] THEN
562 REWRITE_TAC [GEN_ALL (SYM (SPEC_ALL (OR_ASSOC_lemma)))] THEN
563 REWRITE_TAC [OR_OR_lemma] THEN
565 ONCE_REWRITE_TAC [OR_COMM_lemma] THEN
566 ASM_REWRITE_TAC []);;
568 let UNLESS_cor3 = prove_thm
570 (`!(p:'a->bool) q r Pr.
571 ((p /\* (Not q)) UNLESS (q \/* r)) Pr = (p UNLESS (q \/* r)) Pr`),
572 REWRITE_TAC [IMP_ANTISYM_RULE
573 (SPEC_ALL UNLESS_cor3b) (SPEC_ALL UNLESS_cor3a)]);;
575 let UNLESS_cor4 = prove_thm
577 (`!(p:'a->bool) q r Pr.
578 ((p \/* q) UNLESS r) Pr ==> (p UNLESS (q \/* r)) Pr`),
579 REPEAT STRIP_TAC THEN
580 ASSUME_TAC (SPEC_ALL ((SPEC (`Not (q:'a->bool)`) UNLESS_thm2))) THEN
581 UNDISCH_TAC (`((Not (q:'a->bool)) UNLESS (Not(Not q)))Pr`) THEN
582 REWRITE_TAC [NOT_NOT_lemma] THEN
584 ASSUME_TAC (UNDISCH_ALL (SPEC_ALL (SPECL
585 [(`(((p:'a->bool) \/* q) UNLESS r)Pr`);
586 (`((Not (q:'a->bool)) UNLESS q)Pr`)]
587 AND_INTRO_THM))) THEN
588 ASSUME_TAC (UNDISCH_ALL (SPEC_ALL (SPECL
589 [(`((p:'a->bool) \/* q)`); (`r:'a->bool`);
590 (`(Not (q:'a->bool))`); (`q:'a->bool`)]
592 UNDISCH_TAC (`((((p:'a->bool) \/* q) /\* (Not q)) UNLESS
594 REWRITE_TAC [OR_NOT_AND_lemma] THEN
595 PURE_ONCE_REWRITE_TAC [SPECL [(`r:'a->bool`); (`q:'a->bool`)]
597 REWRITE_TAC [UNLESS_cor3] THEN
599 PURE_ONCE_REWRITE_TAC [SPECL [(`r:'a->bool`); (`q:'a->bool`)]
601 ASM_REWRITE_TAC []);;
603 let UNLESS_cor5 = prove_thm
605 (`!(p:'a->bool) Pr. (p UNLESS True) Pr`),
607 ASSUME_TAC (SPEC_ALL UNLESS_thm1) THEN
608 ASSUME_TAC (SPEC_ALL UNLESS_thm2) THEN
609 ASSUME_TAC (UNDISCH_ALL (SPECL
610 [(`((p:'a->bool) UNLESS p)Pr`);
611 (`((p:'a->bool) UNLESS (Not p))Pr`)]
613 ASSUME_TAC (UNDISCH_ALL (SPEC_ALL (SPECL
614 [(`p:'a->bool`); (`p:'a->bool`);
615 (`p:'a->bool`); (`(Not (p:'a->bool))`)]
617 UNDISCH_TAC (`(((p:'a->bool) /\* p) UNLESS (p \/* (Not p)))Pr`) THEN
618 REWRITE_TAC [AND_AND_lemma;P_OR_NOT_P_lemma]);;
620 let UNLESS_cor6 = prove_thm
622 (`!(p:'a->bool) Pr. (True UNLESS p) Pr`),
624 ASSUME_TAC (SPEC_ALL UNLESS_thm1) THEN
625 ASSUME_TAC (SPEC_ALL (SPEC (`(Not (p:'a->bool))`) UNLESS_thm2)) THEN
626 UNDISCH_TAC (`((Not (p:'a->bool)) UNLESS (Not(Not p)))Pr`) THEN
627 REWRITE_TAC [NOT_NOT_lemma] THEN
629 ASSUME_TAC (UNDISCH_ALL (SPECL
630 [(`((Not (p:'a->bool)) UNLESS p)Pr`);
631 (`((p:'a->bool) UNLESS p)Pr`)]
633 ASSUME_TAC (UNDISCH_ALL (SPEC_ALL (SPECL
634 [(`(Not (p:'a->bool))`); (`p:'a->bool`);
635 (`p:'a->bool`); (`p:'a->bool`)]
637 UNDISCH_TAC (`(((Not (p:'a->bool)) \/* p) UNLESS (p \/* p))Pr`) THEN
638 PURE_ONCE_REWRITE_TAC [OR_COMM_lemma] THEN
639 REWRITE_TAC [OR_OR_lemma;P_OR_NOT_P_lemma]);;
641 let UNLESS_cor7 = prove_thm
643 (`!(p:'a->bool) Pr. (False UNLESS p) Pr`),
645 ASSUME_TAC (SPEC_ALL UNLESS_thm1) THEN
646 ASSUME_TAC (SPEC_ALL (SPEC (`(Not (p:'a->bool))`) UNLESS_thm2)) THEN
647 UNDISCH_TAC (`((Not (p:'a->bool)) UNLESS (Not(Not p)))Pr`) THEN
648 REWRITE_TAC [NOT_NOT_lemma] THEN
650 ASSUME_TAC (UNDISCH_ALL (SPECL
651 [(`((Not (p:'a->bool)) UNLESS p)Pr`);
652 (`((p:'a->bool) UNLESS p)Pr`)]
654 ASSUME_TAC (UNDISCH_ALL (SPEC_ALL (SPECL
655 [(`(Not (p:'a->bool))`); (`p:'a->bool`);
656 (`p:'a->bool`); (`p:'a->bool`)]
658 UNDISCH_TAC (`(((Not (p:'a->bool)) /\* p) UNLESS (p \/* p))Pr`) THEN
659 PURE_ONCE_REWRITE_TAC [AND_COMM_lemma] THEN
660 REWRITE_TAC [OR_OR_lemma;P_AND_NOT_P_lemma]);;
662 let HeJiFeng_lemma1 = TAC_PROOF
664 (`!(p:'a->bool) q p'.
665 (!s. p s /\ ~q s) ==> (!s. p' s) ==> (!s. p s \/ q s) ==>
666 (!s. p s /\ ~q s ==> p' s /\ ~q s)`)),
667 REPEAT STRIP_TAC THEN RES_TAC THEN ASM_REWRITE_TAC []);;
669 let HeJiFeng_lemma2 = TAC_PROOF
671 (`!(p:'a->bool) q p'.
672 (!s. p s /\ ~q s) ==> (!s. p' s) ==> (!s. p s \/ q s) ==>
673 (!s. p' s /\ ~q s ==> p s /\ ~q s)`)),
674 REPEAT STRIP_TAC THEN RES_TAC THEN ASM_REWRITE_TAC []);;
676 let HeJiFeng_lemma = TAC_PROOF
678 (`!(p:'a->bool) q p'.
679 (!s. p s /\ ~q s) ==> (!s. p' s) ==> (!s. p s \/ q s) ==>
680 (!s. p s /\ ~q s <=> p' s /\ ~q s)`)),
681 REPEAT STRIP_TAC THEN
682 REWRITE_TAC [IMP_ANTISYM_RULE
683 (SPEC_ALL (UNDISCH (UNDISCH (UNDISCH (SPEC_ALL HeJiFeng_lemma1)))))
684 (SPEC_ALL (UNDISCH (UNDISCH (UNDISCH (SPEC_ALL HeJiFeng_lemma2)))))]);;
686 let HeJiFeng_lemma_f = MK_ABS (UNDISCH_ALL (SPEC_ALL HeJiFeng_lemma));;
688 let UNLESS_cor8 = prove_thm
690 (`!(p:'a->bool) q p' Pr.
691 (!s. p s /\ ~q s) ==> (!s. p' s) ==> (!s. p s \/ q s)
692 ==> (((p /\* (Not q)) UNLESS q) Pr =
693 ((p' /\* (Not q)) UNLESS q) Pr)`),
694 REPEAT STRIP_TAC THEN
695 REWRITE_TAC [AND_def;OR_def;NOT_def1] THEN
696 CONV_TAC (DEPTH_CONV BETA_CONV) THEN
697 REWRITE_TAC [HeJiFeng_lemma_f]);;
700 Corollary of generalized cancellation
702 let UNLESS_cor9 = prove_thm
704 (`!(p:'a->bool) q p' q' r r' Pr.
705 ((p \/* p') UNLESS (q \/* r)) Pr /\ ((q \/* q') UNLESS (p \/* r')) Pr ==>
706 ((p \/* p' \/* q \/* q') UNLESS ((p /\* q) \/* r \/* r')) Pr`),
707 REPEAT GEN_TAC THEN DISCH_TAC THEN
708 ASSUME_TAC (UNDISCH_ALL (SPECL
709 [(`((p:'a->bool) \/* p')`); (`((q:'a->bool) \/* r)`);
710 (`((q:'a->bool) \/* q')`); (`((p:'a->bool) \/* r')`);
714 [(`p:'a->bool`); (`q:'a->bool`);
715 (`p':'a->bool`); (`q':'a->bool`);
716 (`r:'a->bool`); (`r':'a->bool`)] IMPLY_WEAK_lemma4) THEN
717 ASSUME_TAC (UNDISCH_ALL (SPECL
718 [(`((((p:'a->bool) \/* p') \/* (q \/* q')) UNLESS
719 ((((Not(p \/* p')) /\* (p \/* r')) \/*
720 ((Not(q \/* q')) /\* (q \/* r))) \/*
721 ((q \/* r) /\* (p \/* r')))) Pr`);
722 (`!s:'a. ((((Not(p \/* p')) /\* (p \/* r')) \/*
723 ((Not(q \/* q')) /\* (q \/* r))) \/*
724 ((q \/* r) /\* (p \/* r'))) s ==>
725 ((p /\* q) \/* (r \/* r'))s`)]
727 STRIP_ASSUME_TAC (UNDISCH_ALL (SPEC_ALL (SPECL
728 [(`(((p:'a->bool) \/* p') \/* (q \/* q'))`);
729 (`((((Not((p:'a->bool) \/* p')) /\* (p \/* r')) \/*
730 ((Not(q \/* q')) /\* (q \/* r))) \/*
731 ((q \/* r) /\* (p \/* r')))`);
732 (`(((p:'a->bool) /\* q) \/* (r \/* r'))`)]
734 UNDISCH_TAC (`((((p:'a->bool) \/* p') \/* (q \/* q')) UNLESS
735 ((p /\* q) \/* (r \/* r')))Pr`) THEN
736 REWRITE_TAC [OR_ASSOC_lemma]);;
738 let UNLESS_cor10 = prove_thm
740 (`!(p:'a->bool) q Pr. (p \/* q) STABLE Pr ==> (p UNLESS q) Pr`),
742 REWRITE_TAC [STABLE] THEN
744 STRIP_ASSUME_TAC (UNDISCH_ALL (SPECL
745 [(`p:'a->bool`); (`q:'a->bool`);
746 (`False:'a->bool`); (`Pr:('a->'a)list`)]
748 UNDISCH_TAC (`((p:'a->bool) UNLESS (q \/* False))Pr`) THEN
749 REWRITE_TAC [OR_False_lemma]);;
752 let UNLESS_cor11 = prove_thm
754 (`!(p:'a->bool) Pr. (!s. (Not p)s) ==> p STABLE Pr`),
756 REWRITE_TAC [STABLE] THEN
758 REWRITE_TAC [UNLESS] THEN
761 ASM_REWRITE_TAC [] THEN
763 REWRITE_TAC [UNLESS_STMT; FALSE_def] THEN
764 STRIP_ASSUME_TAC (REWRITE_RULE [NOT_def1]
765 (SPEC `s:'a` (ASSUME `!s:'a. Not (p:'a->bool) s`))) THEN
769 let UNLESS_cor12 = prove_thm
771 (`!(p:'a->bool) Pr. (!s. (Not p)s) ==> (Not p) STABLE Pr`),
773 REWRITE_TAC [STABLE] THEN
775 REWRITE_TAC [UNLESS] THEN
778 ASM_REWRITE_TAC [UNLESS_STMT]);;
780 let UNLESS_cor13 = prove_thm
782 (`!(p:'a->bool) q Pr.
783 (p UNLESS q) Pr /\ (q UNLESS p) Pr /\ (!s. Not (p /\* q) s) ==>
784 (p \/* q) STABLE Pr`),
785 REPEAT STRIP_TAC THEN
786 ASSUME_TAC (UNDISCH_ALL (SPECL
787 [(`((p:'a->bool) /\* q)`);
788 (`Pr:('a->'a)list`)] UNLESS_cor11)) THEN
789 UNDISCH_TAC (`((p:'a->bool) /\* q) STABLE Pr`) THEN
790 REWRITE_TAC [STABLE] THEN
792 ASSUME_TAC (UNDISCH_ALL (SPECL
793 [(`((p:'a->bool) UNLESS q)Pr`); (`((q:'a->bool) UNLESS p)Pr`)]
795 ASSUME_TAC (UNDISCH_ALL (SPECL
796 [(`(p:'a->bool)`); (`(q:'a->bool)`);
797 (`(q:'a->bool)`); (`(p:'a->bool)`); (`Pr:('a->'a)list`)]
799 UNDISCH_TAC (`(((p:'a->bool) \/* q) UNLESS
800 ((((Not p) /\* p) \/* ((Not q) /\* q)) \/* (q /\* p))
802 PURE_ONCE_REWRITE_TAC [AND_COMM_lemma] THEN
803 REWRITE_TAC [P_AND_NOT_P_lemma;OR_False_lemma] THEN
804 PURE_ONCE_REWRITE_TAC [OR_COMM_lemma] THEN
805 REWRITE_TAC [OR_False_lemma] THEN
807 ASSUME_TAC (UNDISCH_ALL (SPECL
808 [(`(((q:'a->bool) \/* p) UNLESS (p /\* q))Pr`);
809 (`(((p:'a->bool) /\* q) UNLESS False)Pr`)]
811 ASSUME_TAC (UNDISCH_ALL (SPECL
812 [(`((q:'a->bool) \/* p)`); (`((p:'a->bool) /\* q)`);
813 (`False:'a->bool`); (`Pr:('a->'a)list`)]
816 (`((((q:'a->bool) \/* p) \/* (p /\* q)) UNLESS False)Pr`) THEN
817 REWRITE_TAC [OR_AND_DISTR_lemma] THEN
818 REWRITE_TAC [OR_ASSOC_lemma;OR_OR_lemma] THEN
819 PURE_ONCE_REWRITE_TAC [OR_COMM_lemma] THEN
820 REWRITE_TAC [OR_ASSOC_lemma;OR_OR_lemma;AND_AND_lemma]);;
822 let UNLESS_cor14 = prove_thm
824 (`!(p:'a->bool) q Pr. (p UNLESS (Not q)) Pr /\ q STABLE Pr ==>
825 (p UNLESS (p /\* (Not q))) Pr`),
826 REWRITE_TAC [STABLE] THEN
827 REPEAT GEN_TAC THEN DISCH_TAC THEN
828 ASSUME_TAC (UNDISCH_ALL (SPECL
829 [(`p:'a->bool`); (`Not (q:'a->bool)`);
830 (`q:'a->bool`); (`False:'a->bool`); (`Pr:('a->'a)list`)]
832 UNDISCH_TAC (`(((p:'a->bool) /\* q) UNLESS
833 (((p /\* False) \/* (q /\* (Not q))) \/*
834 ((Not q) /\* False)))Pr`) THEN
835 REWRITE_TAC [AND_False_lemma;P_AND_NOT_P_lemma;OR_False_lemma] THEN
838 [(`(p:'a->bool) /\* (Not q)`);
839 (`Pr:('a->'a)list`)] UNLESS_thm1) THEN
840 ASSUME_TAC (UNDISCH_ALL (SPECL
841 [(`(((p:'a->bool) /\* q) UNLESS False)Pr`);
842 (`(((p:'a->bool) /\* (Not q)) UNLESS (p /\* (Not q)))Pr`)]
844 ASSUME_TAC (UNDISCH_ALL (SPECL
845 [(`(p:'a->bool) /\* q`); (`False:'a->bool`);
846 (`(p:'a->bool) /\* (Not q)`); (`(p:'a->bool) /\* (Not q)`);
849 UNDISCH_TAC (`((((p:'a->bool) /\* q) \/* (p /\* (Not q))) UNLESS
850 ((((Not(p /\* q)) /\* (p /\* (Not q))) \/*
851 ((Not(p /\* (Not q))) /\* False)) \/*
852 (False /\* (p /\* (Not q)))))Pr`) THEN
853 REWRITE_TAC [AND_False_lemma;OR_False_lemma] THEN
854 ONCE_REWRITE_TAC [OR_COMM_lemma] THEN
855 REWRITE_TAC [AND_COMPL_OR_lemma] THEN
856 ONCE_REWRITE_TAC [AND_COMM_lemma] THEN
857 REWRITE_TAC [AND_False_lemma] THEN
858 ONCE_REWRITE_TAC [OR_COMM_lemma] THEN
859 REWRITE_TAC [OR_False_lemma] THEN
860 REWRITE_TAC [NOT_AND_OR_NOT_lemma] THEN
861 REWRITE_TAC [AND_OR_DISTR_lemma] THEN
862 REWRITE_TAC [AND_ASSOC_lemma] THEN
863 REWRITE_TAC [AND_AND_lemma] THEN
864 ONCE_REWRITE_TAC [AND_AND_COMM_lemma] THEN
865 REWRITE_TAC [GEN_ALL (SYM (SPEC_ALL AND_ASSOC_lemma))] THEN
866 REWRITE_TAC [P_AND_NOT_P_lemma] THEN
867 ONCE_REWRITE_TAC [AND_COMM_OR_lemma] THEN
868 REWRITE_TAC [AND_False_lemma] THEN
869 ONCE_REWRITE_TAC [OR_COMM_lemma] THEN
870 REWRITE_TAC [OR_False_lemma] THEN
872 ONCE_REWRITE_TAC [AND_COMM_lemma] THEN
873 ASM_REWRITE_TAC []);;
875 let UNLESS_cor15_lem1 = TAC_PROOF
877 (`!p q. p /\ (~p \/ ~q) <=> p /\ ~q`)),
880 REPEAT STRIP_TAC THEN
881 (RES_TAC THEN ASM_REWRITE_TAC []));;
883 let UNLESS_cor15_lem2 = TAC_PROOF
885 (`!p q. p \/ (p /\ q) <=> p`)),
888 REPEAT STRIP_TAC THEN
889 ASM_REWRITE_TAC []);;
891 let UNLESS_cor15_lem3 = TAC_PROOF
893 (`!P Q. (!(i:num). (P i) /\ (Q i)) <=> ((!i. P i) /\ (!i. Q i))`)),
896 REPEAT STRIP_TAC THEN
897 ASM_REWRITE_TAC []);;
900 MESON_TAC is powerful, but I should change this proof to not use
901 MESON_TAC as a detailed proof will better show why the UNLESS_STMT
904 let UNLESS_STMT_cor15 = prove_thm
905 ("UNLESS_STMT_cor15",
906 `!(P:num->('a->bool)) Q st.
907 (!i s. (P i UNLESS_STMT P i /\* Q i) st s) ==>
908 (!s. ((!*) P UNLESS_STMT (!*) P /\* (?*) Q) st s)`,
910 REWRITE_TAC [FORALL_def; EXISTS_def; UNLESS_STMT; AND_def] THEN
911 CONV_TAC (DEPTH_CONV BETA_CONV) THEN
914 let UNLESS_cor15 = prove_thm
916 `!(P:num->('a->bool)) Q Pr.
917 (!i. ((P i) UNLESS ((P i) /\* (Q i))) Pr) ==>
918 (((!*) P) UNLESS (((!*) P) /\* ((?*) Q))) Pr`,
919 GEN_TAC THEN GEN_TAC THEN
921 REWRITE_TAC [UNLESS] THEN
924 ASM_REWRITE_TAC [] THEN
925 STRIP_ASSUME_TAC (REWRITE_RULE [UNLESS_cor15_lem3] (ASSUME
926 `!i:num. (!s:'a. (P i UNLESS_STMT P i /\* Q i) h s) /\
927 (P i UNLESS P i /\* Q i) t`)) THEN
929 ASM_REWRITE_TAC [] THEN
930 IMP_RES_TAC UNLESS_STMT_cor15);;
932 let UNLESS_cor16 = prove_thm
934 `!(P:num->('a->bool)) Q Pr.
935 (!i. ((P i) UNLESS (Q i))Pr) ==>
936 (!i. ((/<=\* P i) UNLESS (\<=/* Q i))Pr)`,
941 ASM_REWRITE_TAC [AND_LE_N_def;OR_LE_N_def]
943 REWRITE_TAC [AND_LE_N_def;OR_LE_N_def] THEN
944 ASSUME_TAC (SPEC (`SUC i`) (ASSUME
945 (`!i. (((P:num->('a->bool)) i) UNLESS (Q i))Pr`))) THEN
946 STRIP_ASSUME_TAC (UNDISCH_ALL (hd (IMP_CANON (SPECL
947 [(`/<=\* (P:num->('a->bool)) i`);
948 (`\<=/* (Q:num->('a->bool)) i`);
949 (`(P:num->('a->bool))(SUC i)`); (`(Q:num->('a->bool))(SUC i)`);
954 let UNLESS_cor17 = prove_thm
956 (`!(P:num->('a->bool)) q Pr.
957 (!i. ((P i) UNLESS q)Pr) ==> (!i. ((/<=\* P i) UNLESS q)Pr)`),
962 ASM_REWRITE_TAC [AND_LE_N_def;OR_LE_N_def]
964 REWRITE_TAC [AND_LE_N_def;OR_LE_N_def] THEN
965 ASSUME_TAC (SPEC (`SUC i`) (ASSUME
966 (`!i. (((P:num->('a->bool)) i) UNLESS q)Pr`))) THEN
967 ASSUME_TAC (UNDISCH_ALL (hd (IMP_CANON (SPECL
968 [(`/<=\* (P:num->('a->bool)) i`); (`q:'a->bool`);
969 (`(P:num->('a->bool))(SUC i)`);
970 (`q:'a->bool`); (`Pr:('a->'a)list`)]
973 REWRITE_TAC [OR_OR_lemma]
977 MESON_TAC is powerful, but I should change this proof to not use
978 MESON_TAC as a detailed proof will better show why the UNLESS_STMT
981 let UNLESS_STMT_cor18 = prove_thm
982 ("UNLESS_STMT_cor18",
983 `!(P:num->('a->bool)) Q st.
984 (!i s. ((P i) UNLESS_STMT q) st s) ==>
985 (!s. (((?*) P) UNLESS_STMT q) st s)`,
987 REWRITE_TAC [FORALL_def; EXISTS_def; UNLESS_STMT; AND_def] THEN
988 CONV_TAC (DEPTH_CONV BETA_CONV) THEN
991 let UNLESS_cor18 = prove_thm
993 (`!(P:num->('a->bool)) q Pr.
994 (!m. ((P m) UNLESS q) Pr) ==> (((?*) P) UNLESS q) Pr`),
995 GEN_TAC THEN GEN_TAC THEN
997 REWRITE_TAC [UNLESS] THEN
999 ASM_REWRITE_TAC [] THEN
1000 STRIP_ASSUME_TAC (REWRITE_RULE [UNLESS_cor15_lem3] (ASSUME
1001 `!m:num. (!s:'a. (P m UNLESS_STMT q) h s) /\ (P m UNLESS q) t`)) THEN
1003 ASM_REWRITE_TAC [] THEN
1004 IMP_RES_TAC UNLESS_STMT_cor18);;
1006 let UNLESS_cor19 = prove_thm
1008 (`!Pr. (False:'a->bool) STABLE Pr`),
1010 REWRITE_TAC [STABLE] THEN
1011 REWRITE_TAC [UNLESS_thm1]);;
1013 let UNLESS_cor20 = prove_thm
1015 (`!(p:'a->bool) q Pr.
1016 (p STABLE Pr) /\ (q STABLE Pr) ==> ((p /\* q) STABLE Pr)`),
1018 REWRITE_TAC [STABLE] THEN
1019 ACCEPT_TAC (REWRITE_RULE [AND_False_lemma;OR_False_lemma] (SPECL
1020 [(`p:'a->bool`); (`False:'a->bool`);
1021 (`q:'a->bool`); (`False:'a->bool`);
1022 (`Pr:('a->'a)list`)] UNLESS_thm4)));;
1024 let UNLESS_cor21 = prove_thm
1026 (`!(p:'a->bool) q Pr.
1027 (p STABLE Pr) /\ (q STABLE Pr) ==> ((p \/* q) STABLE Pr)`),
1029 REWRITE_TAC [STABLE] THEN
1030 ACCEPT_TAC (REWRITE_RULE [AND_False_lemma;OR_False_lemma] (SPECL
1031 [(`p:'a->bool`); (`False:'a->bool`);
1032 (`q:'a->bool`); (`False:'a->bool`);
1033 (`Pr:('a->'a)list`)] UNLESS_thm7)));;
1035 let UNLESS_cor22 = prove_thm
1037 (`!(p:'a->bool) q r Pr.
1038 (p UNLESS q) Pr /\ (r STABLE Pr) ==>
1039 ((p /\* r) UNLESS (q /\* r))Pr`),
1041 REWRITE_TAC [STABLE] THEN
1042 ACCEPT_TAC (REWRITE_RULE [OR_False_lemma] (ONCE_REWRITE_RULE [OR_COMM_lemma]
1043 (ONCE_REWRITE_RULE [OR_AND_COMM_lemma]
1044 (REWRITE_RULE [AND_False_lemma;OR_False_lemma] (SPECL
1045 [(`p:'a->bool`); (`q:'a->bool`);
1046 (`r:'a->bool`); (`False:'a->bool`);
1047 (`Pr:('a->'a)list`)] UNLESS_thm4))))));;
1049 let UNLESS_cor23 = prove_thm
1051 (`!(p:'a->bool) q r Pr.
1052 ((p UNLESS q) Pr) ==> ((p \/* r) UNLESS (q \/* r)) Pr`),
1053 GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN
1054 LIST_INDUCT_TAC THEN
1055 REWRITE_TAC [UNLESS] THEN
1058 ASM_REWRITE_TAC [] THEN
1059 IMP_RES_TAC UNLESS_STMT_thm6 THEN
1060 ASM_REWRITE_TAC []);;