relationScript.sml
1(*---------------------------------------------------------------------------*
2 * A theory about relations, taken as functions of type 'a->'a->bool. *
3 * We treat various kinds of closure (reflexive, transitive, r&t) *
4 * and wellfoundedness to start. A few other notions, like inverse image, *
5 * are also defined. *
6 *---------------------------------------------------------------------------*)
7Theory relation[bare]
8Ancestors
9 (* mention satTheory to work around dependency-analysis flaw in Holmake;
10 satTheory is a dependency of BasicProvers, but without explicit mention
11 here, Holmake will not rebuild relationTheory when satTheory changes. *)
12 combin sat[qualified]
13Libs
14 HolKernel Parse boolLib BasicProvers QLib tautLib mesonLib
15 metisLib simpLib boolSimps
16
17(*---------------------------------------------------------------------------*)
18(* Basic properties of relations. *)
19(*---------------------------------------------------------------------------*)
20
21val transitive_def =
22Q.new_definition
23("transitive_def",
24 `transitive (R:'a->'a->bool) = !x y z. R x y /\ R y z ==> R x z`);
25val _ = OpenTheoryMap.OpenTheory_const_name
26 {const={Thy="relation",Name="transitive"},
27 name=(["Relation"],"transitive")}
28
29val reflexive_def = new_definition(
30 "reflexive_def",
31 ``reflexive (R:'a->'a->bool) = !x. R x x``);
32val _ = OpenTheoryMap.OpenTheory_const_name
33 {const={Thy="relation",Name="reflexive"},
34 name=(["Relation"],"reflexive")}
35
36val irreflexive_def = new_definition(
37 "irreflexive_def",
38 ``irreflexive (R:'a->'a->bool) = !x. ~R x x``);
39val _ = OpenTheoryMap.OpenTheory_const_name
40 {const={Thy="relation",Name="irreflexive"},
41 name=(["Relation"],"irreflexive")}
42
43val symmetric_def = new_definition(
44 "symmetric_def",
45 ``symmetric (R:'a->'a->bool) = !x y. R x y = R y x``);
46
47val antisymmetric_def = new_definition(
48 "antisymmetric_def",
49 ``antisymmetric (R:'a->'a->bool) = !x y. R x y /\ R y x ==> (x = y)``);
50
51val equivalence_def = new_definition(
52 "equivalence_def",
53 “equivalence (R:'a->'a->bool) <=> reflexive R /\ symmetric R /\ transitive R”
54);
55
56val total_def = new_definition(
57 "total_def",
58 ``total (R:'a->'a->bool) = !x y. R x y \/ R y x``);
59
60val trichotomous = new_definition(
61 "trichotomous",
62 ``trichotomous (R:'a->'a->bool) = !a b. R a b \/ R b a \/ (a = b)``);
63
64(*---------------------------------------------------------------------------*)
65(* Closures *)
66(*---------------------------------------------------------------------------*)
67
68(* The TC and RTC suffixes are tighter than function application. This
69 means that
70 inv R^+
71 is the inverse of the transitive closure, and you need parentheses to
72 write the transitive closure of the inverse:
73 (inv R)^+
74*)
75val TC_DEF = Q.new_definition
76 ("TC_DEF",
77 `TC (R:'a->'a->bool) a b =
78 !P.(!x y. R x y ==> P x y) /\
79 (!x y z. P x y /\ P y z ==> P x z) ==> P a b`);
80val _ = add_rule { fixity = Suffix 2100,
81 block_style = (AroundEachPhrase, (Portable.CONSISTENT,0)),
82 paren_style = ParoundPrec,
83 pp_elements = [TOK "^+"],
84 term_name = "TC" }
85val _ = Unicode.unicode_version {u = Unicode.UChar.sup_plus, tmnm = "TC"}
86val _ = TeX_notation {hol = Unicode.UChar.sup_plus,
87 TeX = ("\\HOLTokenSupPlus{}", 1)}
88val _ = TeX_notation {hol = "^+", TeX = ("\\HOLTokenSupPlus{}", 1)}
89val _ = OpenTheoryMap.OpenTheory_const_name
90 {const={Thy="relation",Name="TC"},
91 name=(["Relation"],"transitiveClosure")}
92
93
94Inductive RTC:
95 (!x. RTC R x x)
96 /\
97 (!x y z. R x y /\ RTC R y z ==> RTC R x z)
98End
99val _ = add_rule { fixity = Suffix 2100,
100 block_style = (AroundEachPhrase, (Portable.CONSISTENT,0)),
101 paren_style = ParoundPrec,
102 pp_elements = [TOK "^*"],
103 term_name = "RTC" }
104val _ = Unicode.unicode_version {u = UTF8.chr 0xA673, tmnm = "RTC"}
105val _ = TeX_notation {hol = UTF8.chr 0xA673, TeX = ("\\HOLTokenSupStar{}", 1)}
106val _ = TeX_notation {hol = "^*", TeX = ("\\HOLTokenSupStar{}", 1)}
107
108val RC_DEF = new_definition(
109 "RC_DEF",
110 ``RC (R:'a->'a->bool) x y <=> (x = y) \/ R x y``);
111
112val SC_DEF = new_definition(
113 "SC_DEF",
114 ``SC (R:'a->'a->bool) x y <=> R x y \/ R y x``);
115
116val EQC_DEF = new_definition(
117 "EQC_DEF",
118 ``EQC (R:'a->'a->bool) = RC (TC (SC R))``);
119val _ = add_rule { fixity = Suffix 2100,
120 block_style = (AroundEachPhrase, (Portable.CONSISTENT,0)),
121 paren_style = ParoundPrec,
122 pp_elements = [TOK "^="],
123 term_name = "EQC" }
124
125
126Theorem SC_SYMMETRIC:
127 !R. symmetric (SC R)
128Proof
129 REWRITE_TAC [symmetric_def, SC_DEF] THEN MESON_TAC []
130QED
131
132Theorem TC_TRANSITIVE[simp]:
133 !R:'a->'a->bool. transitive(TC R)
134Proof
135 REWRITE_TAC[transitive_def,TC_DEF]
136 THEN REPEAT STRIP_TAC
137 THEN RES_TAC THEN ASM_MESON_TAC[]
138QED
139
140Theorem RTC_INDUCT:
141 !R P. (!x. P x x) /\ (!x y z. R x y /\ P y z ==> P x z) ==>
142 (!x (y:'a). RTC R x y ==> P x y)
143Proof
144 MESON_TAC [RTC_ind] (* differs only in choice of induction variable "P" *)
145QED
146
147Theorem TC_RULES:
148 !R. (!x (y:'a). R x y ==> TC R x y) /\
149 (!x y z. TC R x y /\ TC R y z ==> TC R x z)
150Proof
151 REWRITE_TAC [TC_DEF] THEN REPEAT STRIP_TAC THENL [
152 ASM_MESON_TAC [],
153 FIRST_ASSUM MATCH_MP_TAC THEN RES_TAC THEN ASM_MESON_TAC []
154 ]
155QED
156
157Theorem RTC_RULES = RTC_rules;
158Theorem RTC_REFL[simp]:
159 RTC R x x
160Proof REWRITE_TAC [RTC_RULES]
161QED
162
163Theorem RTC_SINGLE[simp]:
164 !R x y. R x y ==> RTC R x y
165Proof
166 PROVE_TAC [RTC_RULES]
167QED
168
169Theorem RTC_STRONG_INDUCT[rule_induction]:
170 !R P. (!x. P x x) /\ (!x y z. R x y /\ RTC R y z /\ P y z ==> P x z) ==>
171 (!x (y:'a). RTC R x y ==> P x y)
172Proof
173 ASM_MESON_TAC [RTC_strongind]
174QED
175
176Theorem RTC_RTC:
177 !R (x:'a) y. RTC R x y ==> !z. RTC R y z ==> RTC R x z
178Proof
179 GEN_TAC THEN HO_MATCH_MP_TAC RTC_STRONG_INDUCT THEN MESON_TAC [RTC_RULES]
180QED
181
182Theorem RTC_TRANSITIVE[simp]: !R:'a->'a->bool. transitive (RTC R)
183Proof REWRITE_TAC [transitive_def] THEN MESON_TAC [RTC_RTC]
184QED
185Theorem transitive_RTC = RTC_TRANSITIVE
186
187Theorem RTC_TRANS:
188 R^* x y /\ R^* y z ==> R^* x z
189Proof
190 METIS_TAC[RTC_TRANSITIVE, transitive_def]
191QED
192
193Theorem RTC_REFLEXIVE[simp]: !R:'a->'a->bool. reflexive (RTC R)
194Proof MESON_TAC [reflexive_def, RTC_RULES]
195QED
196Theorem reflexive_RTC = RTC_REFLEXIVE
197
198Theorem RTC_BRACKETS_RTC_EQN:
199 (!x y. R1 x y ==> R2 x y) /\ (!x y. R2 x y ==> RTC R1 x y) ==>
200 (RTC R2 = RTC R1)
201Proof
202 strip_tac >> SIMP_TAC bool_ss [FUN_EQ_THM, EQ_IMP_THM, FORALL_AND_THM] >>
203 conj_tac >> Induct_on ‘RTC’ >> simp_tac (srw_ss()) [] >>
204 METIS_TAC[RTC_RTC, RTC_RULES]
205QED
206
207Theorem RC_REFLEXIVE[simp]:
208 !R:'a->'a->bool. reflexive (RC R)
209Proof MESON_TAC [reflexive_def, RC_DEF]
210QED
211Theorem reflexive_RC = RC_REFLEXIVE
212
213Theorem RC_REFL[simp]:
214 RC R x x
215Proof
216 MESON_TAC [RC_DEF]
217QED
218
219Theorem RC_lifts_monotonicities:
220 (!x y. R x y ==> R (f x) (f y)) ==> !x y. RC R x y ==> RC R (f x) (f y)
221Proof METIS_TAC [RC_DEF]
222QED
223
224Theorem RC_MONOTONE[mono]: (!x y. R x y ==> Q x y) ==> RC R x y ==> RC Q x y
225Proof
226 STRIP_TAC THEN REWRITE_TAC [RC_DEF] THEN STRIP_TAC THEN
227 ASM_REWRITE_TAC [] THEN RES_TAC THEN ASM_REWRITE_TAC []
228QED
229
230Theorem RC_lifts_invariants:
231 (!x y. P x /\ R x y ==> P y) ==> (!x y. P x /\ RC R x y ==> P y)
232Proof METIS_TAC [RC_DEF]
233QED
234
235Theorem RC_lifts_equalities:
236 (!x y. R x y ==> (f x = f y)) ==> (!x y. RC R x y ==> (f x = f y))
237Proof METIS_TAC [RC_DEF]
238QED
239
240Theorem SC_lifts_monotonicities:
241 (!x y. R x y ==> R (f x) (f y)) ==> !x y. SC R x y ==> SC R (f x) (f y)
242Proof
243 METIS_TAC [SC_DEF]
244QED
245
246Theorem SC_lifts_equalities:
247 (!x y. R x y ==> (f x = f y)) ==> !x y. SC R x y ==> (f x = f y)
248Proof
249 METIS_TAC [SC_DEF]
250QED
251
252Theorem SC_MONOTONE[mono]:
253 (!x:'a y. R x y ==> Q x y) ==> SC R x y ==> SC Q x y
254Proof
255 STRIP_TAC THEN REWRITE_TAC [SC_DEF] THEN STRIP_TAC THEN RES_TAC THEN
256 ASM_REWRITE_TAC []
257QED
258
259Theorem symmetric_RC[simp]:
260 !R. symmetric (RC R) = symmetric R
261Proof
262 REWRITE_TAC [symmetric_def, RC_DEF] THEN
263 REPEAT (STRIP_TAC ORELSE EQ_TAC) THEN ASM_MESON_TAC []
264QED
265
266Theorem antisymmetric_RC[simp]:
267 !R. antisymmetric (RC R) = antisymmetric R
268Proof
269 SRW_TAC [][antisymmetric_def, RC_DEF] THEN PROVE_TAC []
270QED
271
272Theorem transitive_RC:
273 !R. transitive R ==> transitive (RC R)
274Proof
275 SRW_TAC [][transitive_def, RC_DEF] THEN PROVE_TAC []
276QED
277
278Theorem TC_SUBSET:
279 !R x (y:'a). R x y ==> TC R x y
280Proof
281REWRITE_TAC[TC_DEF] THEN MESON_TAC[]
282QED
283
284Theorem RTC_SUBSET:
285 !R (x:'a) y. R x y ==> RTC R x y
286Proof
287 MESON_TAC [RTC_RULES]
288QED
289
290Theorem RC_SUBSET:
291 !R (x:'a) y. R x y ==> RC R x y
292Proof
293 MESON_TAC [RC_DEF]
294QED
295
296Theorem RC_RTC:
297 !R (x:'a) y. RC R x y ==> RTC R x y
298Proof
299 MESON_TAC [RC_DEF, RTC_RULES]
300QED
301
302val tc = ``tc : ('a -> 'a -> bool) -> ('a -> 'a -> bool)``
303val tc_left_asm =
304 ``tc = \R a b. !P. (!x y. R x y ==> P x y) /\
305 (!x y z. R x y /\ P y z ==> P x z) ==>
306 P a b``;
307val tc_right_asm =
308 ``tc = \R a b. !P. (!x y. R x y ==> P x y) /\
309 (!x y z. P x y /\ R y z ==> P x z) ==>
310 P a b``;
311
312Theorem tc_left_rules0[local]:
313 ^tc_left_asm ==> (!x y. R x y ==> tc R x y) /\
314 (!x y z. R x y /\ tc R y z ==> tc R x z)
315Proof
316 STRIP_TAC THEN ASM_REWRITE_TAC [] THEN BETA_TAC THEN MESON_TAC []
317QED
318val tc_left_rules = UNDISCH tc_left_rules0
319
320val tc_right_rules = UNDISCH (prove(
321 ``^tc_right_asm ==> (!x y. R x y ==> tc R x y) /\
322 (!x y z. tc R x y /\ R y z ==> tc R x z)``,
323 STRIP_TAC THEN ASM_REWRITE_TAC [] THEN BETA_TAC THEN MESON_TAC []));
324
325val tc_left_ind = TAC_PROOF(
326 ([tc_left_asm],
327 ``!R P. (!x y. R x y ==> P x y) /\
328 (!x y z. R x y /\ P y z ==> P x z) ==>
329 (!x y. tc R x y ==> P x y)``),
330 ASM_REWRITE_TAC [] THEN BETA_TAC THEN MESON_TAC []);
331
332val tc_right_ind = TAC_PROOF(
333 ([tc_right_asm],
334 ``!R P. (!x y. R x y ==> P x y) /\
335 (!x y z. P x y /\ R y z ==> P x z) ==>
336 (!x y. tc R x y ==> P x y)``),
337 ASM_REWRITE_TAC [] THEN BETA_TAC THEN MESON_TAC []);
338
339val tc_left_twice = TAC_PROOF(
340 ([tc_left_asm],
341 ``!R x y. ^tc R x y ==> !z. tc R y z ==> tc R x z``),
342 GEN_TAC THEN
343 HO_MATCH_MP_TAC tc_left_ind THEN MESON_TAC [tc_left_rules]);
344val tc_right_twice = TAC_PROOF(
345 ([tc_right_asm],
346 ``!R x y. ^tc R x y ==> !z. tc R z x ==> tc R z y``),
347 GEN_TAC THEN HO_MATCH_MP_TAC tc_right_ind THEN MESON_TAC [tc_right_rules]);
348
349
350Theorem TC_INDUCT:
351 !(R:'a->'a->bool) P.
352 (!x y. R x y ==> P x y) /\
353 (!x y z. P x y /\ P y z ==> P x z)
354 ==> !u v. (TC R) u v ==> P u v
355Proof
356REWRITE_TAC[TC_DEF] THEN MESON_TAC[]
357QED
358
359val tc_left_TC = TAC_PROOF(
360 ([tc_left_asm],
361 ``!R x y. tc R x y = TC R x y``),
362 GEN_TAC THEN
363 SIMP_TAC bool_ss [FORALL_AND_THM, EQ_IMP_THM] THEN CONJ_TAC THENL [
364 HO_MATCH_MP_TAC tc_left_ind THEN MESON_TAC [TC_RULES],
365 HO_MATCH_MP_TAC TC_INDUCT THEN MESON_TAC [tc_left_twice, tc_left_rules]
366 ]);
367val tc_right_TC = TAC_PROOF(
368 ([tc_right_asm],
369 ``!R x y. tc R x y = TC R x y``),
370 GEN_TAC THEN
371 SIMP_TAC bool_ss [FORALL_AND_THM, EQ_IMP_THM] THEN CONJ_TAC THENL [
372 HO_MATCH_MP_TAC tc_right_ind THEN MESON_TAC [TC_RULES],
373 HO_MATCH_MP_TAC TC_INDUCT THEN MESON_TAC [tc_right_twice, tc_right_rules]
374 ]);
375
376val tc_left_exists = SIMP_PROVE bool_ss [] ``?tc. ^tc_left_asm``;
377val tc_right_exists = SIMP_PROVE bool_ss [] ``?tc. ^tc_right_asm``;
378
379Theorem TC_INDUCT_LEFT1 =
380 CHOOSE(tc, tc_left_exists) (REWRITE_RULE [tc_left_TC] tc_left_ind);
381Theorem TC_INDUCT_RIGHT1 =
382 CHOOSE(tc, tc_right_exists) (REWRITE_RULE [tc_right_TC] tc_right_ind);
383
384val TC_INDUCT_TAC =
385 let val tc_thm = TC_INDUCT
386 fun tac (asl,w) =
387 let val (u,Body) = dest_forall w
388 val (v,Body) = dest_forall Body
389 val (ant,conseq) = dest_imp Body
390 val (TC, R, u', v') = case strip_comb ant of
391 (TC, [R, u', v']) => (TC, R, u', v')
392 | _ => raise Match
393 val _ = assert (equal "TC") (fst (dest_const TC))
394 val _ = assert (aconv u) u'
395 val _ = assert (aconv v) v'
396 val P = list_mk_abs([u,v], conseq)
397 val tc_thm' = BETA_RULE(ISPEC P (ISPEC R tc_thm))
398 in MATCH_MP_TAC tc_thm' (asl,w)
399 end
400 handle _ => raise mk_HOL_ERR "<top-level>" "TC_INDUCT_TAC"
401 "Unanticipated term structure"
402 in tac
403 end;
404
405Theorem TC_STRONG_INDUCT0[local]:
406 !R P. (!x y. R x y ==> P x y) /\
407 (!x y z. P x y /\ P y z /\ TC R x y /\ TC R y z ==> P x z) ==>
408 (!u v. TC R u v ==> P u v /\ TC R u v)
409Proof
410 REPEAT GEN_TAC THEN STRIP_TAC THEN TC_INDUCT_TAC THEN
411 ASM_MESON_TAC [TC_RULES]
412QED
413
414Theorem TC_STRONG_INDUCT[rule_induction]:
415 !R P. (!x y. R x y ==> P x y) /\
416 (!x y z. P x y /\ P y z /\ TC R x y /\ TC R y z ==> P x z) ==>
417 (!u v. TC R u v ==> P u v)
418Proof REPEAT STRIP_TAC THEN IMP_RES_TAC TC_STRONG_INDUCT0
419QED
420
421Theorem TC_STRONG_INDUCT_LEFT1_0[local]:
422 !R P. (!x y. R x y ==> P x y) /\
423 (!x y z. R x y /\ P y z /\ TC R y z ==> P x z) ==>
424 (!u v. TC R u v ==> P u v /\ TC R u v)
425Proof
426 REPEAT GEN_TAC THEN STRIP_TAC THEN HO_MATCH_MP_TAC TC_INDUCT_LEFT1 THEN
427 ASM_MESON_TAC [TC_RULES]
428QED
429
430Theorem TC_STRONG_INDUCT_RIGHT1_0[local]:
431 !R P. (!x y. R x y ==> P x y) /\
432 (!x y z. P x y /\ TC R x y /\ R y z ==> P x z) ==>
433 (!u v. TC R u v ==> P u v /\ TC R u v)
434Proof
435 REPEAT GEN_TAC THEN STRIP_TAC THEN HO_MATCH_MP_TAC TC_INDUCT_RIGHT1 THEN
436 ASM_MESON_TAC [TC_RULES]
437QED
438
439Theorem TC_STRONG_INDUCT_LEFT1:
440 !R P. (!x y. R x y ==> P x y) /\
441 (!x y z. R x y /\ P y z /\ TC R y z ==> P x z) ==>
442 (!u v. TC R u v ==> P u v)
443Proof
444 REPEAT STRIP_TAC THEN IMP_RES_TAC TC_STRONG_INDUCT_LEFT1_0
445QED
446Theorem TC_STRONG_INDUCT_RIGHT1:
447 !R P. (!x y. R x y ==> P x y) /\
448 (!x y z. P x y /\ TC R x y /\ R y z ==> P x z) ==>
449 (!u v. TC R u v ==> P u v)
450Proof
451 REPEAT STRIP_TAC THEN IMP_RES_TAC TC_STRONG_INDUCT_RIGHT1_0
452QED
453
454(* can get inductive principles for properties which do not hold generally
455 but only for particular cases of x or y in TC R x y *)
456
457fun tc_ind_alt_tacs tc_ind_thm tq =
458 REPEAT STRIP_TAC THEN
459 POP_ASSUM (ASSUME_TAC o Ho_Rewrite.REWRITE_RULE [BETA_THM]
460 o Q.SPEC tq o GEN_ALL o MATCH_MP (REORDER_ANTS rev tc_ind_thm)) THEN
461 VALIDATE (POP_ASSUM (ACCEPT_TAC o UNDISCH)) THEN
462 POP_ASSUM (K ALL_TAC) THEN REPEAT STRIP_TAC THEN
463 TRY COND_CASES_TAC THEN
464 FULL_SIMP_TAC bool_ss [TC_SUBSET] THEN
465 RES_TAC THEN IMP_RES_TAC TC_RULES ;
466
467Theorem TC_INDUCT_ALT_LEFT:
468 !R Q. (!x. R x b ==> Q x) /\ (!x y. R x y /\ Q y ==> Q x) ==>
469 !a. TC R a b ==> Q a
470Proof
471 tc_ind_alt_tacs TC_INDUCT_LEFT1 `\x y. if y = b then Q x else TC R x y`
472QED
473
474Theorem TC_INDUCT_ALT_RIGHT:
475 !R Q. (!y. R a y ==> Q y) /\ (!x y. Q x /\ R x y ==> Q y) ==>
476 !b. TC R a b ==> Q b
477Proof
478 tc_ind_alt_tacs TC_INDUCT_RIGHT1 `\x y. if x = a then Q y else TC R x y`
479QED
480
481Theorem TC_lifts_monotonicities:
482 (!x y. R x y ==> R (f x) (f y)) ==>
483 !x y. TC R x y ==> TC R (f x) (f y)
484Proof
485 STRIP_TAC THEN HO_MATCH_MP_TAC TC_INDUCT THEN
486 METIS_TAC [TC_RULES]
487QED
488
489Theorem TC_lifts_invariants:
490 (!x y. P x /\ R x y ==> P y) ==> (!x y. P x /\ TC R x y ==> P y)
491Proof
492 STRIP_TAC THEN
493 Q_TAC SUFF_TAC `!x y. TC R x y ==> P x ==> P y` THEN1 METIS_TAC [] THEN
494 HO_MATCH_MP_TAC TC_INDUCT THEN METIS_TAC []
495QED
496
497Theorem TC_lifts_equalities:
498 (!x y. R x y ==> (f x = f y)) ==> (!x y. TC R x y ==> (f x = f y))
499Proof
500 STRIP_TAC THEN HO_MATCH_MP_TAC TC_INDUCT THEN METIS_TAC []
501QED
502
503(* generalisation of above results *)
504Theorem TC_lifts_transitive_relations:
505 (!x y. R x y ==> Q (f x) (f y)) /\ transitive Q ==>
506 (!x y. TC R x y ==> Q (f x) (f y))
507Proof
508 STRIP_TAC THEN HO_MATCH_MP_TAC TC_INDUCT THEN METIS_TAC [transitive_def]
509QED
510
511Theorem TC_implies_one_step:
512 !x y . R^+ x y /\ x <> y ==> ?z. R x z /\ x <> z
513Proof
514REWRITE_TAC [GSYM AND_IMP_INTRO] THEN
515HO_MATCH_MP_TAC TC_INDUCT THEN
516SRW_TAC [SatisfySimps.SATISFY_ss][] THEN
517PROVE_TAC []
518QED
519
520Theorem TC_RTC:
521 !R (x:'a) y. TC R x y ==> RTC R x y
522Proof
523 GEN_TAC THEN TC_INDUCT_TAC THEN MESON_TAC [RTC_RULES, RTC_RTC]
524QED
525
526Theorem RTC_TC_RC:
527 !R (x:'a) y. RTC R x y ==> RC R x y \/ TC R x y
528Proof
529 GEN_TAC THEN HO_MATCH_MP_TAC RTC_STRONG_INDUCT THEN
530 REPEAT STRIP_TAC THENL [
531 REWRITE_TAC [RC_DEF],
532 FULL_SIMP_TAC bool_ss [RC_DEF] THEN ASM_MESON_TAC [TC_RULES],
533 ASM_MESON_TAC [TC_RULES]
534 ]
535QED
536
537Theorem TC_RC_EQNS:
538 !R:'a->'a->bool. (RC (TC R) = RTC R) /\ (TC (RC R) = RTC R)
539Proof
540 REPEAT STRIP_TAC THEN
541 CONV_TAC (Q.X_FUN_EQ_CONV `u`) THEN GEN_TAC THEN
542 CONV_TAC (Q.X_FUN_EQ_CONV `v`) THEN GEN_TAC THEN
543 EQ_TAC THENL [
544 REWRITE_TAC [RC_DEF] THEN MESON_TAC [TC_RTC, RTC_RULES],
545 Q.ID_SPEC_TAC `v` THEN Q.ID_SPEC_TAC `u` THEN
546 HO_MATCH_MP_TAC RTC_STRONG_INDUCT THEN
547 SIMP_TAC bool_ss [RC_DEF] THEN MESON_TAC [TC_RULES],
548 Q.ID_SPEC_TAC `v` THEN Q.ID_SPEC_TAC `u` THEN
549 HO_MATCH_MP_TAC TC_INDUCT THEN MESON_TAC [RC_RTC, RTC_RTC],
550 Q.ID_SPEC_TAC `v` THEN Q.ID_SPEC_TAC `u` THEN
551 HO_MATCH_MP_TAC RTC_INDUCT THEN MESON_TAC [TC_RULES, RC_DEF]
552 ]
553QED
554
555Theorem TC_LEFT1_I:
556 !x y z. R x y /\ TC R y z ==> TC R x z
557Proof
558 METIS_TAC[TC_RULES]
559QED
560
561Theorem TC_RIGHT1_I:
562 !x y z. TC R x y /\ R y z ==> TC R x z
563Proof
564 METIS_TAC[TC_RULES]
565QED
566
567(* can get inductive principles for properties which do not hold generally
568 but only for particular cases of x or y in RTC R x y *)
569
570Theorem RTC_ALT_DEF:
571 !R a b. RTC R a b <=> !Q. Q b /\ (!x y. R x y /\ Q y ==> Q x) ==> Q a
572Proof
573 REWRITE_TAC [EQ_IMP_THM] THEN CONV_TAC (REDEPTH_CONV FORALL_AND_CONV) THEN
574 CONJ_TAC THEN1 (GEN_TAC THEN Induct_on `RTC` THEN METIS_TAC[]) THEN
575 REPEAT GEN_TAC THEN
576 DISCH_THEN (Q.SPEC_THEN `\z. RTC R z b` (MATCH_MP_TAC o BETA_RULE)) THEN
577 METIS_TAC[RTC_RULES]
578QED
579
580Theorem RTC_ALT_INDUCT:
581 !R Q b. Q b /\ (!x y. R x y /\ Q y ==> Q x) ==> !x. RTC R x b ==> Q x
582Proof
583 REWRITE_TAC [RTC_ALT_DEF] THEN REPEAT STRIP_TAC THEN RES_TAC
584QED
585
586Theorem RTC_ALT_RIGHT_DEF:
587 !R a b. RTC R a b = !Q. Q a /\ (!y z. Q y /\ R y z ==> Q z) ==> Q b
588Proof
589 REWRITE_TAC [RTC_ALT_DEF] THEN REPEAT (STRIP_TAC ORELSE EQ_TAC) THEN
590 FIRST_X_ASSUM (ASSUME_TAC o Q.SPEC `$~ o Q`) THEN
591 REV_FULL_SIMP_TAC bool_ss [combinTheory.o_THM] THEN RES_TAC
592QED
593
594Theorem RTC_ALT_RIGHT_INDUCT:
595 !R Q a. Q a /\ (!y z. Q y /\ R y z ==> Q z) ==> !z. RTC R a z ==> Q z
596Proof
597 REWRITE_TAC [RTC_ALT_RIGHT_DEF] THEN REPEAT STRIP_TAC THEN RES_TAC
598QED
599
600Theorem RTC_INDUCT_RIGHT1:
601 !R P. (!x. P x x) /\
602 (!x y z. P x y /\ R y z ==> P x z) ==>
603 (!x y. RTC R x y ==> P x y)
604Proof
605 REPEAT STRIP_TAC THEN
606 FIRST_X_ASSUM (irule o MATCH_MP (REORDER_ANTS rev RTC_ALT_RIGHT_INDUCT)) THEN
607 ASM_REWRITE_TAC []
608QED
609
610Theorem RTC_RULES_RIGHT1:
611 !R. (!x. RTC R x x) /\ (!x y z. RTC R x y /\ R y z ==> RTC R x z)
612Proof
613 REWRITE_TAC [RTC_ALT_RIGHT_DEF] THEN
614 REPEAT STRIP_TAC THEN RES_TAC THEN RES_TAC
615QED
616
617Theorem RTC_STRONG_INDUCT_RIGHT1:
618 !R P. (!x. P x x) /\
619 (!x y z. P x y /\ RTC R x y /\ R y z ==> P x z) ==>
620 (!x y. RTC R x y ==> P x y)
621Proof
622 REPEAT STRIP_TAC THEN
623 Q_TAC SUFF_TAC `P x y /\ RTC R x y` THEN1 MESON_TAC [] THEN
624 Q.UNDISCH_THEN `RTC R x y` MP_TAC THEN
625 MAP_EVERY Q.ID_SPEC_TAC [`y`, `x`] THEN
626 HO_MATCH_MP_TAC RTC_INDUCT_RIGHT1 THEN
627 ASM_MESON_TAC [RTC_RULES_RIGHT1]
628QED
629
630
631Theorem EXTEND_RTC_TC:
632 !R x y z. R x y /\ RTC R y z ==> TC R x z
633Proof
634 GEN_TAC THEN
635 Q_TAC SUFF_TAC `!y z. RTC R y z ==> !x. R x y ==> TC R x z` THEN1
636 MESON_TAC [] THEN
637 HO_MATCH_MP_TAC RTC_INDUCT THEN
638 MESON_TAC [TC_RULES]
639QED
640
641
642Theorem EXTEND_RTC_TC_EQN:
643 !R x z. TC R x z = ?y. (R x y /\ RTC R y z)
644Proof
645 GEN_TAC THEN
646 Q_TAC SUFF_TAC `!x z. TC R x z ==> ?y. R x y /\ RTC R y z` THEN1
647 MESON_TAC [EXTEND_RTC_TC] THEN
648 HO_MATCH_MP_TAC TC_INDUCT THEN
649 PROVE_TAC[RTC_RULES, RTC_TRANSITIVE, transitive_def,
650 RTC_RULES_RIGHT1]
651QED
652
653Theorem EXTEND_RTC_TC_RIGHT1:
654 !R x y z. RTC R x y /\ R y z ==> TC R x z
655Proof
656 GEN_TAC THEN
657 Q_TAC SUFF_TAC `!x y. RTC R x y ==> !z. R y z ==> TC R x z` THEN1
658 MESON_TAC [] THEN
659 HO_MATCH_MP_TAC RTC_INDUCT_RIGHT1 THEN
660 MESON_TAC [TC_RULES]
661QED
662
663Theorem EXTEND_RTC_TC_RIGHT1_EQN:
664 !R x z. TC R x z = ?y. (RTC R x y /\ R y z)
665Proof
666 GEN_TAC THEN
667 Q_TAC SUFF_TAC `!x z. TC R x z ==> ?y. RTC R x y /\ R y z` THEN1
668 MESON_TAC [EXTEND_RTC_TC_RIGHT1] THEN
669 HO_MATCH_MP_TAC TC_INDUCT_RIGHT1 THEN
670 PROVE_TAC[RTC_RULES, RTC_TRANSITIVE, transitive_def,
671 RTC_RULES_RIGHT1]
672QED
673
674Theorem reflexive_RC_identity:
675 !R. reflexive R ==> (RC R = R)
676Proof
677 SIMP_TAC bool_ss [reflexive_def, RC_DEF, FUN_EQ_THM] THEN MESON_TAC []
678QED
679
680Theorem symmetric_SC_identity:
681 !R. symmetric R ==> (SC R = R)
682Proof
683 SIMP_TAC bool_ss [symmetric_def, SC_DEF, FUN_EQ_THM]
684QED
685
686Theorem transitive_TC_identity:
687 !R. transitive R ==> (TC R = R)
688Proof
689 SIMP_TAC bool_ss [transitive_def, FUN_EQ_THM, EQ_IMP_THM, FORALL_AND_THM,
690 TC_RULES] THEN GEN_TAC THEN STRIP_TAC THEN
691 HO_MATCH_MP_TAC TC_INDUCT THEN ASM_MESON_TAC []
692QED
693
694Theorem RC_IDEM[simp]:
695 !R:'a->'a->bool. RC (RC R) = RC R
696Proof
697 SIMP_TAC bool_ss [RC_REFLEXIVE, reflexive_RC_identity]
698QED
699
700Theorem SC_IDEM[simp]:
701 !R:'a->'a->bool. SC (SC R) = SC R
702Proof
703 SIMP_TAC bool_ss [SC_SYMMETRIC, symmetric_SC_identity]
704QED
705
706Theorem TC_IDEM[simp]:
707 !R:'a->'a->bool. TC (TC R) = TC R
708Proof
709 SIMP_TAC bool_ss [TC_TRANSITIVE, transitive_TC_identity]
710QED
711
712Theorem RC_MOVES_OUT:
713 !R. (SC (RC R) = RC (SC R)) /\ (RC (RC R) = RC R) /\
714 (TC (RC R) = RC (TC R))
715Proof
716 REWRITE_TAC [TC_RC_EQNS, RC_IDEM] THEN
717 SIMP_TAC bool_ss [SC_DEF, RC_DEF, FUN_EQ_THM] THEN MESON_TAC []
718QED
719
720Theorem symmetric_TC:
721 !R. symmetric R ==> symmetric (TC R)
722Proof
723 REWRITE_TAC [symmetric_def] THEN GEN_TAC THEN STRIP_TAC THEN
724 SIMP_TAC bool_ss [EQ_IMP_THM, FORALL_AND_THM] THEN CONJ_TAC THENL [
725 HO_MATCH_MP_TAC TC_INDUCT,
726 CONV_TAC SWAP_VARS_CONV THEN HO_MATCH_MP_TAC TC_INDUCT
727 ] THEN ASM_MESON_TAC [TC_RULES]
728QED
729
730Theorem reflexive_TC:
731 !R. reflexive R ==> reflexive (TC R)
732Proof
733 PROVE_TAC [reflexive_def,TC_SUBSET]
734QED
735
736Theorem EQC_EQUIVALENCE[simp]:
737 !R. equivalence (EQC R)
738Proof
739 REWRITE_TAC [equivalence_def, EQC_DEF, RC_REFLEXIVE, symmetric_RC] THEN
740 MESON_TAC [symmetric_TC, TC_RC_EQNS, TC_TRANSITIVE, SC_SYMMETRIC]
741QED
742
743Theorem EQC_IDEM[simp]:
744 !R:'a->'a->bool. EQC(EQC R) = EQC R
745Proof
746 SIMP_TAC bool_ss [EQC_DEF, RC_MOVES_OUT, symmetric_SC_identity,
747 symmetric_TC, SC_SYMMETRIC, TC_IDEM]
748QED
749
750
751Theorem RTC_IDEM[simp]:
752 !R:'a->'a->bool. RTC (RTC R) = RTC R
753Proof
754 SIMP_TAC bool_ss [GSYM TC_RC_EQNS, RC_MOVES_OUT, TC_IDEM]
755QED
756
757Theorem RTC_CASES1:
758 !R (x:'a) y. RTC R x y <=> (x = y) \/ ?u. R x u /\ RTC R u y
759Proof
760 SIMP_TAC bool_ss [EQ_IMP_THM, FORALL_AND_THM] THEN CONJ_TAC THENL [
761 GEN_TAC THEN HO_MATCH_MP_TAC RTC_INDUCT THEN MESON_TAC [RTC_RULES],
762 MESON_TAC [RTC_RULES]
763 ]
764QED
765
766Theorem RTC_CASES_TC:
767 !R x y. R^* x y <=> (x = y) \/ R^+ x y
768Proof
769 METIS_TAC [EXTEND_RTC_TC_EQN, RTC_CASES1]
770QED
771
772Theorem RTC_CASES2:
773 !R (x:'a) y. RTC R x y <=> (x = y) \/ ?u. RTC R x u /\ R u y
774Proof
775 SIMP_TAC bool_ss [EQ_IMP_THM, FORALL_AND_THM] THEN CONJ_TAC THENL [
776 GEN_TAC THEN HO_MATCH_MP_TAC RTC_INDUCT THEN MESON_TAC [RTC_RULES],
777 MESON_TAC [RTC_RULES, RTC_SUBSET, RTC_RTC]
778 ]
779QED
780
781Theorem RTC_CASES_RTC_TWICE:
782 !R (x:'a) y. RTC R x y <=> ?u. RTC R x u /\ RTC R u y
783Proof
784 SIMP_TAC bool_ss [EQ_IMP_THM, FORALL_AND_THM] THEN CONJ_TAC THENL [
785 GEN_TAC THEN HO_MATCH_MP_TAC RTC_INDUCT THEN MESON_TAC [RTC_RULES],
786 MESON_TAC [RTC_RULES, RTC_SUBSET, RTC_RTC]
787 ]
788QED
789
790Theorem TC_CASES1_E:
791 !R x z. TC R x z ==> R x z \/ ?y:'a. R x y /\ TC R y z
792Proof
793GEN_TAC
794 THEN TC_INDUCT_TAC
795 THEN MESON_TAC [REWRITE_RULE[transitive_def] TC_TRANSITIVE, TC_SUBSET]
796QED
797
798Theorem TC_CASES1:
799 TC R x z <=> R x z \/ ?y:'a. R x y /\ TC R y z
800Proof
801 MESON_TAC[TC_RULES, TC_CASES1_E]
802QED
803
804Theorem TC_CASES2_E:
805 !R x z. TC R x z ==> R x z \/ ?y:'a. TC R x y /\ R y z
806Proof
807GEN_TAC
808 THEN TC_INDUCT_TAC
809 THEN MESON_TAC [REWRITE_RULE[transitive_def] TC_TRANSITIVE, TC_SUBSET]
810QED
811
812Theorem TC_CASES2:
813 TC R x z <=> R x z \/ ?y:'a. TC R x y /\ R y z
814Proof
815 MESON_TAC [TC_RULES, TC_CASES2_E]
816QED
817
818Theorem TC_MONOTONE[mono]:
819 (!x y. R x y ==> Q x y) ==> TC R x y ==> TC Q x y
820Proof
821 REPEAT GEN_TAC THEN STRIP_TAC THEN MAP_EVERY Q.ID_SPEC_TAC [`y`, `x`] THEN
822 TC_INDUCT_TAC THEN ASM_MESON_TAC [TC_RULES]
823QED
824
825Theorem RTC_MONOTONE[mono]:
826 (!x y. R x y ==> Q x y) ==> RTC R x y ==> RTC Q x y
827Proof
828 REPEAT GEN_TAC THEN STRIP_TAC THEN MAP_EVERY Q.ID_SPEC_TAC [`y`, `x`] THEN
829 HO_MATCH_MP_TAC RTC_INDUCT THEN ASM_MESON_TAC [RTC_RULES]
830QED
831
832Theorem EQC_INDUCTION:
833 !R P. (!x y. R x y ==> P x y) /\
834 (!x. P x x) /\
835 (!x y. P x y ==> P y x) /\
836 (!x y z. P x y /\ P y z ==> P x z) ==>
837 (!x y. EQC R x y ==> P x y)
838Proof
839 REWRITE_TAC [EQC_DEF] THEN REPEAT STRIP_TAC THEN
840 FULL_SIMP_TAC bool_ss [RC_DEF] THEN
841 Q.PAT_X_ASSUM `TC _ x y` MP_TAC THEN
842 MAP_EVERY Q.ID_SPEC_TAC [`y`, `x`] THEN
843 HO_MATCH_MP_TAC TC_INDUCT THEN REWRITE_TAC [SC_DEF] THEN
844 ASM_MESON_TAC []
845QED
846
847Theorem EQC_REFL[simp]:
848 !R x. EQC R x x
849Proof
850 SRW_TAC [][EQC_DEF, RC_DEF]
851QED
852
853Theorem EQC_R:
854 !R x y. R x y ==> EQC R x y
855Proof
856 SRW_TAC [][EQC_DEF, RC_DEF] THEN
857 DISJ2_TAC THEN MATCH_MP_TAC TC_SUBSET THEN
858 SRW_TAC [][SC_DEF]
859QED
860
861Theorem EQC_SYM:
862 !R x y. EQC R x y ==> EQC R y x
863Proof
864 SRW_TAC [][EQC_DEF, RC_DEF] THEN
865 Q.SUBGOAL_THEN `symmetric (TC (SC R))` ASSUME_TAC THEN1
866 SRW_TAC [][SC_SYMMETRIC, symmetric_TC] THEN
867 PROVE_TAC [symmetric_def]
868QED
869
870Theorem EQC_TRANS:
871 !R x y z. EQC R x y /\ EQC R y z ==> EQC R x z
872Proof
873 REPEAT GEN_TAC THEN
874 Q_TAC SUFF_TAC `transitive (EQC R)` THEN1 PROVE_TAC [transitive_def] THEN
875 SRW_TAC [][EQC_DEF, transitive_RC, TC_TRANSITIVE]
876QED
877
878Theorem transitive_EQC:
879 transitive (EQC R)
880Proof
881PROVE_TAC [transitive_def,EQC_TRANS]
882QED
883
884Theorem symmetric_EQC:
885 symmetric (EQC R)
886Proof
887PROVE_TAC [symmetric_def,EQC_SYM]
888QED
889
890Theorem reflexive_EQC:
891 reflexive (EQC R)
892Proof
893PROVE_TAC [reflexive_def,EQC_REFL]
894QED
895
896Theorem EQC_MOVES_IN[simp]:
897 !R. (EQC (RC R) = EQC R) /\ (EQC (SC R) = EQC R) /\ (EQC (TC R) = EQC R)
898Proof
899 SRW_TAC [][EQC_DEF,RC_MOVES_OUT,SC_IDEM] THEN
900 AP_TERM_TAC THEN
901 SRW_TAC [][FUN_EQ_THM] THEN
902 REVERSE EQ_TAC THEN
903 MAP_EVERY Q.ID_SPEC_TAC [`x'`,`x`] THEN
904 HO_MATCH_MP_TAC TC_INDUCT THEN1 (SRW_TAC [][SC_DEF] THEN
905 PROVE_TAC [TC_RULES,SC_DEF]) THEN
906 REVERSE (SRW_TAC [][SC_DEF]) THEN1
907 PROVE_TAC [TC_RULES,SC_DEF] THEN
908 Q.MATCH_ASSUM_RENAME_TAC `R^+ a b` THEN
909 POP_ASSUM MP_TAC THEN
910 MAP_EVERY Q.ID_SPEC_TAC [`b`,`a`] THEN
911 HO_MATCH_MP_TAC TC_INDUCT THEN
912 SRW_TAC [][SC_DEF] THEN
913 PROVE_TAC [TC_RULES,SC_DEF]
914QED
915
916Theorem STRONG_EQC_INDUCTION[rule_induction]:
917 !R P. (!x y. R x y ==> P x y) /\
918 (!x. P x x) /\
919 (!x y. EQC R x y /\ P x y ==> P y x) /\
920 (!x y z. P x y /\ P y z /\ EQC R x y /\ EQC R y z ==> P x z)
921 ==>
922 !x y. EQC R x y ==> P x y
923Proof
924 REPEAT GEN_TAC THEN STRIP_TAC THEN
925 Q_TAC SUFF_TAC `!x y. EQC R x y ==> EQC R x y /\ P x y`
926 THEN1 PROVE_TAC [] THEN
927 HO_MATCH_MP_TAC EQC_INDUCTION THEN
928 PROVE_TAC [EQC_R, EQC_REFL, EQC_SYM, EQC_TRANS]
929QED
930
931Theorem ALT_equivalence:
932 !R. equivalence R = !x y. R x y = (R x = R y)
933Proof
934 REWRITE_TAC [equivalence_def, reflexive_def, symmetric_def,
935 transitive_def, FUN_EQ_THM, EQ_IMP_THM] THEN
936 MESON_TAC []
937QED
938
939Theorem EQC_MONOTONE[mono]:
940 (!x y. R x y ==> R' x y) ==> EQC R x y ==> EQC R' x y
941Proof
942 STRIP_TAC THEN MAP_EVERY Q.ID_SPEC_TAC [`y`, `x`] THEN
943 HO_MATCH_MP_TAC STRONG_EQC_INDUCTION THEN
944 METIS_TAC [EQC_R, EQC_TRANS, EQC_SYM, EQC_REFL]
945QED
946
947Theorem RTC_EQC:
948 !x y. RTC R x y ==> EQC R x y
949Proof
950 HO_MATCH_MP_TAC RTC_INDUCT THEN METIS_TAC [EQC_R, EQC_REFL, EQC_TRANS]
951QED
952
953Theorem RTC_lifts_monotonicities:
954 (!x y. R x y ==> R (f x) (f y)) ==>
955 !x y. R^* x y ==> R^* (f x) (f y)
956Proof
957 STRIP_TAC THEN HO_MATCH_MP_TAC RTC_INDUCT THEN SRW_TAC [][] THEN
958 METIS_TAC [RTC_RULES]
959QED
960
961Theorem RTC_lifts_reflexive_transitive_relations:
962 (!x y. R x y ==> Q (f x) (f y)) /\ reflexive Q /\ transitive Q ==>
963 !x y. R^* x y ==> Q (f x) (f y)
964Proof
965 STRIP_TAC THEN
966 HO_MATCH_MP_TAC RTC_INDUCT THEN
967 FULL_SIMP_TAC bool_ss [reflexive_def,transitive_def] THEN
968 METIS_TAC []
969QED
970
971Theorem RTC_lifts_equalities:
972 (!x y. R x y ==> (f x = f y)) ==> !x y. R^* x y ==> (f x = f y)
973Proof
974 STRIP_TAC THEN
975 HO_MATCH_MP_TAC RTC_lifts_reflexive_transitive_relations THEN
976 ASM_SIMP_TAC bool_ss [reflexive_def,transitive_def]
977QED
978
979Theorem RTC_lifts_invariants:
980 (!x y. P x /\ R x y ==> P y) ==> !x y. P x /\ R^* x y ==> P y
981Proof
982 STRIP_TAC THEN
983 REWRITE_TAC [Once CONJ_COMM] THEN
984 REWRITE_TAC [GSYM AND_IMP_INTRO] THEN
985 HO_MATCH_MP_TAC RTC_INDUCT THEN
986 METIS_TAC []
987QED
988
989(*---------------------------------------------------------------------------*
990 * Wellfounded relations. Wellfoundedness: Every non-empty set has an *
991 * R-minimal element. Applications of wellfoundedness to specific types *
992 * (numbers, lists, etc.) can be found in the respective theories. *
993 *---------------------------------------------------------------------------*)
994
995val WF_DEF =
996Q.new_definition
997 ("WF_DEF", `WF R = !B. (?w:'a. B w) ==> ?min. B min /\ !b. R b min ==> ~B b`);
998val _ = OpenTheoryMap.OpenTheory_const_name
999 {const={Thy="relation",Name="WF"},name=(["Relation"],"wellFounded")}
1000
1001(*---------------------------------------------------------------------------*)
1002(* Misc. proof tools, from pre-automation days. *)
1003(*---------------------------------------------------------------------------*)
1004
1005val USE_TAC = IMP_RES_THEN(fn th => ONCE_REWRITE_TAC[th]);
1006
1007val NNF_CONV =
1008 let val DE_MORGAN = REWRITE_CONV
1009 [TAUT `~(x==>y) = (x /\ ~y)`,
1010 TAUT `~x \/ y <=> (x ==> y)`,DE_MORGAN_THM]
1011 val QUANT_CONV = NOT_EXISTS_CONV ORELSEC NOT_FORALL_CONV
1012 in REDEPTH_CONV (QUANT_CONV ORELSEC CHANGED_CONV DE_MORGAN)
1013 end;
1014
1015val NNF_TAC = CONV_TAC NNF_CONV;
1016
1017
1018(*---------------------------------------------------------------------------*
1019 * *
1020 * WELL FOUNDED INDUCTION *
1021 * *
1022 * Proof: For RAA, assume there's a z s.t. ~P z. By wellfoundedness, *
1023 * there's a minimal object w s.t. ~P w. (P holds of all objects "less" *
1024 * than w.) By the other assumption, i.e., *
1025 * *
1026 * !x. (!y. R y x ==> P y) ==> P x, *
1027 * *
1028 * P w holds, QEA. *
1029 * *
1030 *---------------------------------------------------------------------------*)
1031
1032Theorem WF_INDUCTION_THM:
1033 !(R:'a->'a->bool).
1034 WF R ==> !P. (!x. (!y. R y x ==> P y) ==> P x) ==> !x. P x
1035Proof
1036GEN_TAC THEN REWRITE_TAC[WF_DEF]
1037 THEN DISCH_THEN (fn th => GEN_TAC THEN (MP_TAC (Q.SPEC `\x:'a. ~P x` th)))
1038 THEN BETA_TAC THEN REWRITE_TAC[] THEN STRIP_TAC THEN CONV_TAC CONTRAPOS_CONV
1039 THEN NNF_TAC THEN STRIP_TAC THEN RES_TAC
1040 THEN Q.EXISTS_TAC`min` THEN ASM_REWRITE_TAC[]
1041QED
1042
1043
1044Theorem INDUCTION_WF_THM:
1045 !R:'a->'a->bool.
1046 (!P. (!x. (!y. R y x ==> P y) ==> P x) ==> !x. P x) ==> WF R
1047Proof
1048GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[WF_DEF] THEN GEN_TAC THEN
1049 CONV_TAC CONTRAPOS_CONV THEN NNF_TAC THEN
1050 DISCH_THEN (fn th => POP_ASSUM (MATCH_MP_TAC o BETA_RULE o Q.SPEC`\w. ~B w`)
1051 THEN ASSUME_TAC th) THEN GEN_TAC THEN
1052 CONV_TAC CONTRAPOS_CONV THEN NNF_TAC
1053 THEN POP_ASSUM MATCH_ACCEPT_TAC
1054QED
1055
1056Theorem WF_EQ_INDUCTION_THM:
1057 !R:'a->'a->bool.
1058 WF R = !P. (!x. (!y. R y x ==> P y) ==> P x) ==> !x. P x
1059Proof
1060GEN_TAC THEN EQ_TAC THEN STRIP_TAC THENL
1061 [IMP_RES_TAC WF_INDUCTION_THM, IMP_RES_TAC INDUCTION_WF_THM]
1062QED
1063
1064
1065(*---------------------------------------------------------------------------
1066 * A tactic for doing wellfounded induction. Lifted and adapted from
1067 * John Harrison's definition of WO_INDUCT_TAC in the wellordering library.
1068 *---------------------------------------------------------------------------*)
1069
1070val _ = Parse.hide "C";
1071
1072val WF_INDUCT_TAC =
1073 let val wf_thm0 = CONV_RULE (ONCE_DEPTH_CONV ETA_CONV)
1074 (REWRITE_RULE [TAUT`A==>B==>C <=> A/\B==>C`]
1075 (CONV_RULE (ONCE_DEPTH_CONV RIGHT_IMP_FORALL_CONV)
1076 WF_INDUCTION_THM))
1077 val [R,P] = fst(strip_forall(concl wf_thm0))
1078 val wf_thm1 = GENL [P,R](SPEC_ALL wf_thm0)
1079 fun tac (asl,w) =
1080 let val (Rator,Rand) = dest_comb w
1081 val _ = assert (equal "!") (fst (dest_const Rator))
1082 val thi = ISPEC Rand wf_thm1
1083 fun eqRand t = Term.compare(Rand,t) = EQUAL
1084 val thf = CONV_RULE(ONCE_DEPTH_CONV
1085 (BETA_CONV o assert (eqRand o rator))) thi
1086 in MATCH_MP_TAC thf (asl,w)
1087 end
1088 handle _ => raise mk_HOL_ERR "" "WF_INDUCT_TAC"
1089 "Unanticipated term structure"
1090 in tac
1091 end;
1092
1093
1094Theorem ex_lem[local]:
1095 !x. (?y. y = x) /\ ?y. x=y
1096Proof
1097GEN_TAC THEN CONJ_TAC THEN Q.EXISTS_TAC`x` THEN REFL_TAC
1098QED
1099
1100Theorem WF_NOT_REFL:
1101 !R x y. WF R ==> R x y ==> ~(x=y)
1102Proof
1103REWRITE_TAC[WF_DEF]
1104 THEN REPEAT GEN_TAC
1105 THEN DISCH_THEN (MP_TAC o Q.SPEC`\x. x=y`)
1106 THEN BETA_TAC THEN REWRITE_TAC[ex_lem]
1107 THEN STRIP_TAC
1108 THEN Q.UNDISCH_THEN `min=y` SUBST_ALL_TAC
1109 THEN DISCH_TAC THEN RES_TAC
1110QED
1111
1112(* delete this or the previous if we abbreviate irreflexive *)
1113Theorem WF_irreflexive:
1114 WF R ==> irreflexive R
1115Proof
1116 METIS_TAC [WF_NOT_REFL, irreflexive_def]
1117QED
1118
1119(*---------------------------------------------------------------------------
1120 * Some combinators for wellfounded relations.
1121 *---------------------------------------------------------------------------*)
1122
1123(*---------------------------------------------------------------------------
1124 * The empty relation is wellfounded.
1125 *---------------------------------------------------------------------------*)
1126
1127val EMPTY_REL_DEF =
1128Q.new_definition
1129 ("EMPTY_REL_DEF[simp]", `EMPTY_REL (x:'a) (y:'a) = F`);
1130Overload REMPTY = ``EMPTY_REL``
1131val _ = Unicode.unicode_version {u = UnicodeChars.emptyset ^ UnicodeChars.sub_r,
1132 tmnm = "EMPTY_REL"}
1133
1134
1135Theorem WF_EMPTY_REL:
1136 WF (EMPTY_REL:'a->'a->bool)
1137Proof
1138REWRITE_TAC[EMPTY_REL_DEF,WF_DEF]
1139QED
1140
1141
1142(*---------------------------------------------------------------------------
1143 * Subset: if R is a WF relation and P is a subrelation of R, then
1144 * P is a wellfounded relation.
1145 *---------------------------------------------------------------------------*)
1146
1147Theorem WF_SUBSET:
1148 !(R:'a->'a->bool) P.
1149 WF R /\ (!x y. P x y ==> R x y) ==> WF P
1150Proof
1151REWRITE_TAC[WF_DEF]
1152 THEN REPEAT STRIP_TAC
1153 THEN RES_TAC
1154 THEN Q.EXISTS_TAC`min`
1155 THEN ASM_REWRITE_TAC[]
1156 THEN GEN_TAC
1157 THEN DISCH_TAC
1158 THEN REPEAT RES_TAC
1159QED
1160
1161
1162(*---------------------------------------------------------------------------
1163 * The transitive closure of a wellfounded relation is wellfounded.
1164 * I got the clue about the witness from Peter Johnstone's book:
1165 * "Notes on Logic and Set Theory". An alternative proof that Bernhard
1166 * Schaetz showed me uses well-founded induction then case analysis. In that
1167 * approach, the IH must be quantified over all sets, so that we can
1168 * specialize it later to an extension of B.
1169 *---------------------------------------------------------------------------*)
1170
1171Theorem WF_TC:
1172 !R:'a->'a->bool. WF R ==> WF(TC R)
1173Proof
1174GEN_TAC THEN CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[WF_DEF]
1175 THEN NNF_TAC THEN DISCH_THEN (Q.X_CHOOSE_THEN `B` MP_TAC)
1176 THEN DISCH_THEN (fn th =>
1177 Q.EXISTS_TAC`\m:'a. ?a z. B a /\ TC R a m /\ TC R m z /\ B z`
1178 THEN BETA_TAC THEN CONJ_TAC THEN STRIP_ASSUME_TAC th)
1179 THENL
1180 [RES_TAC THEN RES_TAC THEN MAP_EVERY Q.EXISTS_TAC[`b`, `b'`, `w`]
1181 THEN ASM_REWRITE_TAC[],
1182 Q.X_GEN_TAC`m` THEN STRIP_TAC THEN Q.UNDISCH_TAC`TC R (a:'a) m`
1183 THEN DISCH_THEN(fn th => STRIP_ASSUME_TAC
1184 (CONJ th (MATCH_MP TC_CASES2_E th)))
1185 THENL
1186 [ Q.EXISTS_TAC`a` THEN ASM_REWRITE_TAC[] THEN RES_TAC
1187 THEN MAP_EVERY Q.EXISTS_TAC [`b'`, `z`] THEN ASM_REWRITE_TAC[],
1188 Q.EXISTS_TAC`y` THEN ASM_REWRITE_TAC[]
1189 THEN MAP_EVERY Q.EXISTS_TAC[`a`,`z`] THEN ASM_REWRITE_TAC[]
1190 THEN IMP_RES_TAC TC_SUBSET]
1191 THEN
1192 IMP_RES_TAC(REWRITE_RULE[transitive_def] TC_TRANSITIVE)]
1193QED
1194
1195Theorem WF_TC_EQN:
1196 WF (R^+) <=> WF R
1197Proof
1198 METIS_TAC [WF_TC, TC_SUBSET, WF_SUBSET]
1199QED
1200
1201Theorem WF_noloops:
1202 WF R ==> TC R x y ==> x <> y
1203Proof
1204 METIS_TAC [WF_NOT_REFL, WF_TC_EQN]
1205QED
1206
1207Theorem WF_antisymmetric:
1208 WF R ==> antisymmetric R
1209Proof
1210 REWRITE_TAC [antisymmetric_def] THEN STRIP_TAC THEN
1211 MAP_EVERY Q.X_GEN_TAC [`a`, `b`] THEN
1212 STRIP_TAC THEN Q_TAC SUFF_TAC `TC R a a` THEN1 METIS_TAC [WF_noloops] THEN
1213 METIS_TAC [TC_RULES]
1214QED
1215
1216(*---------------------------------------------------------------------------
1217 * If `f x` remains unchanged in relation `R'` and `f x` always satisfy `P`,
1218 * and there is a mapping `g` such that `R' x y ==> R (f x) (g x) (g y)`, then
1219 * to prove `WF R'`, it is sufficient to prove that `P (f x) ==> WF (R (f x))`.
1220 *---------------------------------------------------------------------------*)
1221Theorem WF_PULL:
1222 !P f R g R'.
1223 (!x. P (f x) ==> WF (R (f x))) /\
1224 (!x y. R' x y ==> P (f x) /\ f x = f y /\ R (f x) (g x) (g y)) ==>
1225 WF R'
1226Proof
1227 rw_tac(srw_ss())[WF_DEF] >>
1228 Cases_on `?w'. P (f w') /\ B w'`
1229 >- (
1230 POP_ASSUM STRIP_ASSUME_TAC >>
1231 FIRST_X_ASSUM drule >>
1232 Q.PAT_X_ASSUM `B w` (K ALL_TAC) >>
1233 DISCH_THEN $ Q.SPEC_THEN
1234 `\x. ?y. x = g y /\ B y /\ P (f y) /\ f y = f w'`
1235 (ASSUME_TAC o SIMP_RULE bool_ss [PULL_EXISTS]) >>
1236 FIRST_X_ASSUM (dxrule_then dxrule) >>
1237 METIS_TAC[]) >>
1238 METIS_TAC[]
1239QED
1240
1241(*---------------------------------------------------------------------------
1242 * Inverse image theorem: mapping into a wellfounded relation gives a
1243 * derived well founded relation. A "size" mapping, like "length" for
1244 * lists is such a relation.
1245 *
1246 * Proof.
1247 * f is total and maps from one n.e. set (Alpha) into another (Beta which is
1248 * "\y. ?x:'a. Alpha x /\ (f x = y)"). Since the latter is n.e.
1249 * and has a wellfounded relation R on it, it has an R-minimal element
1250 * (call it "min"). There exists an x:'a s.t. f x = min. Such an x is an
1251 * R1-minimal element of Alpha (R1 is our derived ordering.) Why is x
1252 * R1-minimal in Alpha? Well, if there was a y:'a s.t. R1 y x, then f y
1253 * would not be in Beta (being less than f x, i.e., min). If f y wasn't in
1254 * Beta, then y couldn't be in Alpha.
1255 *---------------------------------------------------------------------------*)
1256
1257val inv_image_def =
1258Q.new_definition
1259("inv_image_def",
1260 `inv_image R (f:'a->'b) = \x y. R (f x) (f y):bool`);
1261
1262Theorem inv_image_thm[simp] =
1263 SIMP_RULE bool_ss [FUN_EQ_THM] inv_image_def
1264
1265Theorem WF_inv_image:
1266 !R (f:'a->'b). WF R ==> WF (inv_image R f)
1267Proof
1268REPEAT GEN_TAC
1269 THEN REWRITE_TAC[inv_image_def,WF_DEF] THEN BETA_TAC
1270 THEN DISCH_THEN (fn th => Q.X_GEN_TAC`Alpha` THEN STRIP_TAC THEN MP_TAC th)
1271 THEN Q.SUBGOAL_THEN`?w:'b. (\y. ?x:'a. Alpha x /\ (f x = y)) w` MP_TAC
1272 THENL
1273 [ BETA_TAC
1274 THEN MAP_EVERY Q.EXISTS_TAC[`f(w:'a)`,`w`]
1275 THEN ASM_REWRITE_TAC[],
1276 DISCH_THEN (fn th => DISCH_THEN (MP_TAC o C MATCH_MP th)) THEN BETA_TAC
1277 THEN NNF_TAC
1278 THEN REPEAT STRIP_TAC
1279 THEN Q.EXISTS_TAC`x`
1280 THEN ASM_REWRITE_TAC[]
1281 THEN GEN_TAC
1282 THEN DISCH_THEN (ANTE_RES_THEN (MP_TAC o Q.SPEC`b`))
1283 THEN REWRITE_TAC[]]
1284QED
1285
1286Theorem total_inv_image[simp]:
1287 !R f. total R ==> total (inv_image R f)
1288Proof
1289 SRW_TAC[][total_def, inv_image_def]
1290QED
1291
1292Theorem reflexive_inv_image[simp]:
1293 !R f. reflexive R ==> reflexive (inv_image R f)
1294Proof
1295 SRW_TAC[][reflexive_def, inv_image_def]
1296QED
1297
1298Theorem symmetric_inv_image[simp]:
1299 !R f. symmetric R ==> symmetric (inv_image R f)
1300Proof
1301 SRW_TAC[][symmetric_def, inv_image_def]
1302QED
1303
1304Theorem transitive_inv_image[simp]:
1305 !R f. transitive R ==> transitive (inv_image R f)
1306Proof
1307 SRW_TAC[][transitive_def, inv_image_def] THEN METIS_TAC[]
1308QED
1309
1310(*---------------------------------------------------------------------------
1311 * Now the WF recursion theorem. Based on Tobias Nipkow's Isabelle development
1312 * of wellfounded recursion, which itself is a generalization of Mike
1313 * Gordon's HOL development of the primitive recursion theorem.
1314 *---------------------------------------------------------------------------*)
1315
1316(* NOTE: Now RESTRICT is based on the new combinTheory.RESTRICTION
1317
1318 :('a -> 'b) -> ('a -> 'a -> bool) -> 'a -> 'a -> 'b
1319 *)
1320val RESTRICT = new_definition
1321 ("RESTRICT", “RESTRICT (f :'a->'b) R (x :'a) = RESTRICTION (\y. R y x) f”);
1322
1323(* The old definition of RESTRICT now becomes a theorem *)
1324Theorem RESTRICT_DEF :
1325 !(f :'a->'b) R x. RESTRICT f R x = \y. if R y x then f y else ARB
1326Proof
1327 SRW_TAC[][RESTRICT, FUN_EQ_THM, RESTRICTION, IN_DEF]
1328QED
1329
1330(*---------------------------------------------------------------------------
1331 * Obvious, but crucially useful. Unary case. Handling the n-ary case might
1332 * be messy!
1333 *---------------------------------------------------------------------------*)
1334
1335Theorem RESTRICT_LEMMA:
1336 !(f:'a->'b) R (y:'a) (z:'a).
1337 R y z ==> (RESTRICT f R z y = f y)
1338Proof
1339REWRITE_TAC [RESTRICT_DEF] THEN BETA_TAC THEN REPEAT GEN_TAC THEN STRIP_TAC
1340THEN ASM_REWRITE_TAC[]
1341QED
1342
1343
1344(*---------------------------------------------------------------------------
1345 * Two restricted functions are equal just when they are equal on each
1346 * element of their domain.
1347 *---------------------------------------------------------------------------*)
1348
1349Theorem CUTS_EQ[local]:
1350 !R f g (x:'a).
1351 (RESTRICT f R x = RESTRICT g R x)
1352 = !y:'a. R y x ==> (f y:'b = g y)
1353Proof
1354REPEAT GEN_TAC THEN REWRITE_TAC[RESTRICT_DEF]
1355 THEN CONV_TAC (DEPTH_CONV FUN_EQ_CONV) THEN BETA_TAC THEN EQ_TAC
1356 THENL
1357 [ CONV_TAC RIGHT_IMP_FORALL_CONV THEN GEN_TAC
1358 THEN DISCH_THEN (MP_TAC o Q.SPEC`y`) THEN COND_CASES_TAC THEN REWRITE_TAC[],
1359 DISCH_TAC THEN GEN_TAC THEN COND_CASES_TAC THEN RES_TAC
1360 THEN ASM_REWRITE_TAC[]]
1361QED
1362
1363
1364val EXPOSE_CUTS_TAC =
1365 BETA_TAC THEN AP_THM_TAC THEN AP_TERM_TAC
1366 THEN REWRITE_TAC[CUTS_EQ]
1367 THEN REPEAT STRIP_TAC;
1368
1369
1370(*---------------------------------------------------------------------------
1371 * The set of approximations to the function being defined, restricted to
1372 * being R-parents of x. This has the consequence (approx_ext):
1373 *
1374 * approx R M x f = !w. f w = ((R w x) => (M (RESTRICT f R w w) | (@v. T))
1375 *
1376 *---------------------------------------------------------------------------*)
1377
1378val approx_def =
1379Q.new_definition
1380 ("approx_def",
1381 `approx R M x (f:'a->'b) = (f = RESTRICT (\y. M (RESTRICT f R y) y) R x)`);
1382
1383(* This could, in fact, be the definition. *)
1384val approx_ext =
1385BETA_RULE(ONCE_REWRITE_RULE[RESTRICT_DEF]
1386 (CONV_RULE (ONCE_DEPTH_CONV (Q.X_FUN_EQ_CONV`w`)) approx_def));
1387
1388val approx_SELECT0 =
1389 Q.GEN`g` (Q.SPEC`g`
1390 (BETA_RULE(Q.ISPEC `\f:'a->'b. approx R M x f` boolTheory.SELECT_AX)));
1391
1392val approx_SELECT1 = CONV_RULE FORALL_IMP_CONV approx_SELECT0;
1393
1394
1395(*---------------------------------------------------------------------------
1396 * Choose an approximation for R and M at x. Thus it is a
1397 * kind of "lookup" function, associating partial functions with arguments.
1398 * One can easily prove
1399 * (?g. approx R M x g) ==>
1400 * (!w. the_fun R M x w = ((R w x) => (M (RESTRICT (the_fun R M x) R w) w)
1401 * | (@v. T)))
1402 *---------------------------------------------------------------------------*)
1403
1404val the_fun_def =
1405Q.new_definition
1406("the_fun_def",
1407 `the_fun R M x = @f:'a->'b. approx R M x f`);
1408
1409val approx_the_fun0 = ONCE_REWRITE_RULE [GSYM the_fun_def] approx_SELECT0;
1410val approx_the_fun1 = ONCE_REWRITE_RULE [GSYM the_fun_def] approx_SELECT1;
1411val approx_the_fun2 = SUBS [Q.SPECL[`R`,`M`,`x`,`the_fun R M x`] approx_ext]
1412 approx_the_fun1;
1413
1414Theorem the_fun_rw1[local]:
1415 (?g:'a->'b. approx R M x g)
1416 ==>
1417 !w. R w x
1418 ==>
1419 (the_fun R M x w = M (RESTRICT (the_fun R M x) R w) w)
1420Proof
1421 DISCH_THEN (MP_TAC o MP approx_the_fun2) THEN
1422 DISCH_THEN (fn th => GEN_TAC THEN MP_TAC (SPEC_ALL th))
1423 THEN COND_CASES_TAC
1424 THEN ASM_REWRITE_TAC[]
1425QED
1426
1427Theorem the_fun_rw2[local]:
1428 (?g:'a->'b. approx R M x g) ==> !w. ~R w x ==> (the_fun R M x w = ARB)
1429Proof
1430 DISCH_THEN (MP_TAC o MP approx_the_fun2) THEN
1431 DISCH_THEN (fn th => GEN_TAC THEN MP_TAC (SPEC_ALL th))
1432 THEN COND_CASES_TAC
1433 THEN ASM_REWRITE_TAC[]
1434QED
1435
1436(*---------------------------------------------------------------------------
1437 * Define a recursion operator for wellfounded relations. This takes the
1438 * (canonical) function obeying the recursion for all R-ancestors of x:
1439 *
1440 * \p. R p x => the_fun (TC R) (\f v. M (f%R,v) v) x p | Arb
1441 *
1442 * as the function made available for M to use, along with x. Notice that the
1443 * function unrolls properly for each R-ancestor, but only gets applied
1444 * "parentwise", i.e., you can't apply it to any old ancestor, just to a
1445 * parent. This holds recursively, which is what the theorem we eventually
1446 * prove is all about.
1447 *---------------------------------------------------------------------------*)
1448
1449val WFREC_DEF =
1450Q.new_definition
1451("WFREC_DEF",
1452 `WFREC R (M:('a->'b) -> ('a->'b)) =
1453 \x. M (RESTRICT (the_fun (TC R) (\f v. M (RESTRICT f R v) v) x) R x) x`);
1454
1455
1456(*---------------------------------------------------------------------------
1457 * Two approximations agree on their common domain.
1458 *---------------------------------------------------------------------------*)
1459
1460Theorem APPROX_EQUAL_BELOW[local]:
1461 !R M f g u v.
1462 WF R /\ transitive R /\
1463 approx R M u f /\ approx R M v g
1464 ==> !x:'a. R x u ==> R x v
1465 ==> (f x:'b = g x)
1466Proof
1467REWRITE_TAC[approx_ext] THEN REPEAT GEN_TAC THEN STRIP_TAC
1468 THEN WF_INDUCT_TAC THEN Q.EXISTS_TAC`R`
1469 THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC
1470 THEN REPEAT COND_CASES_TAC THEN RES_TAC
1471 THEN EXPOSE_CUTS_TAC
1472 THEN ASM_REWRITE_TAC[]
1473 THEN RULE_ASSUM_TAC (REWRITE_RULE[TAUT`A==>B==>C==>D <=> A/\B/\C==>D`,
1474 transitive_def])
1475 THEN FIRST_ASSUM MATCH_MP_TAC
1476 THEN RES_TAC THEN ASM_REWRITE_TAC[]
1477QED
1478
1479Theorem AGREE_BELOW[local] =
1480 REWRITE_RULE[TAUT`A==>B==>C==>D <=> B/\C/\A==>D`]
1481 (CONV_RULE (DEPTH_CONV RIGHT_IMP_FORALL_CONV) APPROX_EQUAL_BELOW);
1482
1483
1484(*---------------------------------------------------------------------------
1485 * A specialization of AGREE_BELOW
1486 *---------------------------------------------------------------------------*)
1487
1488Theorem RESTRICT_FUN_EQ[local]:
1489 !R M f (g:'a->'b) u v.
1490 WF R /\
1491 transitive R /\
1492 approx R M u f /\
1493 approx R M v g /\
1494 R v u
1495 ==> (RESTRICT f R v = g)
1496Proof
1497REWRITE_TAC[RESTRICT_DEF,transitive_def] THEN REPEAT STRIP_TAC
1498 THEN CONV_TAC (Q.X_FUN_EQ_CONV`w`) THEN BETA_TAC THEN GEN_TAC
1499 THEN COND_CASES_TAC (* on R w v *)
1500 THENL [ MATCH_MP_TAC AGREE_BELOW THEN REPEAT ID_EX_TAC
1501 THEN RES_TAC THEN ASM_REWRITE_TAC[transitive_def],
1502 Q.UNDISCH_TAC`approx R M v (g:'a->'b)`
1503 THEN DISCH_THEN(fn th =>
1504 ASM_REWRITE_TAC[REWRITE_RULE[approx_ext]th])]
1505QED
1506
1507
1508(*---------------------------------------------------------------------------
1509 * Every x has an approximation. This is the crucial theorem.
1510 *---------------------------------------------------------------------------*)
1511
1512Theorem EXISTS_LEMMA[local]:
1513 !R M. WF R /\ transitive R ==> !x. ?f:'a->'b. approx R M x f
1514Proof
1515REPEAT GEN_TAC >> STRIP_TAC
1516 >> WF_INDUCT_TAC
1517 >> Q.EXISTS_TAC`R` >> ASM_REWRITE_TAC[] >> GEN_TAC
1518 >> DISCH_THEN (* Adjust IH by applying Choice *)
1519 (ASSUME_TAC o Q.GEN`y` o Q.DISCH`R (y:'a) (x:'a)`
1520 o (fn th => REWRITE_RULE[GSYM the_fun_def] th)
1521 o SELECT_RULE o UNDISCH o Q.ID_SPEC)
1522 >> Q.EXISTS_TAC`\p. if R p x then M (the_fun R M p) p else ARB` (* witness *)
1523 >> REWRITE_TAC[approx_ext] >> BETA_TAC >> GEN_TAC
1524 >> COND_CASES_TAC
1525 >> ASM_REWRITE_TAC[]
1526 >> EXPOSE_CUTS_TAC
1527 >> RES_THEN (SUBST1_TAC o REWRITE_RULE[approx_def]) (* use IH *)
1528 >> REWRITE_TAC[CUTS_EQ]
1529 >> Q.X_GEN_TAC`v` >> BETA_TAC >> DISCH_TAC
1530 >> RULE_ASSUM_TAC(REWRITE_RULE[transitive_def]) >> RES_TAC
1531 >> ASM_REWRITE_TAC[]
1532 >> EXPOSE_CUTS_TAC
1533 >> MATCH_MP_TAC RESTRICT_FUN_EQ
1534 >> MAP_EVERY Q.EXISTS_TAC[`M`,`w`]
1535 >> ASM_REWRITE_TAC[transitive_def]
1536 >> RES_TAC
1537QED
1538
1539
1540Theorem the_fun_unroll[local]:
1541 !R M x (w:'a).
1542 WF R /\ transitive R
1543 ==> R w x
1544 ==> (the_fun R M x w:'b = M (RESTRICT (the_fun R M x) R w) w)
1545Proof
1546REPEAT GEN_TAC THEN DISCH_TAC
1547 THEN Q.ID_SPEC_TAC`w`
1548 THEN MATCH_MP_TAC the_fun_rw1
1549 THEN MATCH_MP_TAC EXISTS_LEMMA
1550 THEN POP_ASSUM ACCEPT_TAC
1551QED
1552
1553(*---------------------------------------------------------------------------
1554 * Unrolling works for any R M and x, hence it works for "TC R" and
1555 * "\f v. M (f % R,v) v".
1556 *---------------------------------------------------------------------------*)
1557
1558val the_fun_TC0 =
1559 BETA_RULE
1560 (REWRITE_RULE[MATCH_MP WF_TC (Q.ASSUME`WF (R:'a->'a->bool)`),
1561 TC_TRANSITIVE]
1562 (Q.SPECL[`TC R`,`\f v. M (RESTRICT f R v) v`,`x`] the_fun_unroll));
1563
1564
1565(*---------------------------------------------------------------------------
1566 * There's a rewrite rule that simplifies this mess.
1567 *---------------------------------------------------------------------------*)
1568Theorem TC_RESTRICT_LEMMA[local]:
1569 !(f:'a->'b) R w. RESTRICT (RESTRICT f (TC R) w) R w = RESTRICT f R w
1570Proof
1571REPEAT GEN_TAC
1572 THEN REWRITE_TAC[RESTRICT_DEF]
1573 THEN CONV_TAC (Q.X_FUN_EQ_CONV`p`)
1574 THEN BETA_TAC THEN GEN_TAC
1575 THEN COND_CASES_TAC
1576 THENL [IMP_RES_TAC TC_SUBSET, ALL_TAC]
1577 THEN ASM_REWRITE_TAC[]
1578QED
1579
1580val the_fun_TC = REWRITE_RULE[TC_RESTRICT_LEMMA] the_fun_TC0;
1581
1582
1583(*---------------------------------------------------------------------------
1584 * WFREC R M behaves as a fixpoint operator should.
1585 *---------------------------------------------------------------------------*)
1586
1587Theorem WFREC_THM:
1588 !R. !M:('a -> 'b) -> ('a -> 'b).
1589 WF R ==> !x. WFREC R M x = M (RESTRICT (WFREC R M) R x) x
1590Proof
1591REPEAT STRIP_TAC THEN REWRITE_TAC[WFREC_DEF]
1592 THEN EXPOSE_CUTS_TAC THEN BETA_TAC
1593 THEN IMP_RES_TAC TC_SUBSET
1594 THEN USE_TAC the_fun_TC
1595 THEN EXPOSE_CUTS_TAC
1596 THEN MATCH_MP_TAC AGREE_BELOW
1597 THEN MAP_EVERY Q.EXISTS_TAC [`TC R`, `\f v. M (RESTRICT f R v) v`, `x`, `y`]
1598 THEN IMP_RES_TAC WF_TC
1599 THEN ASSUME_TAC(SPEC_ALL TC_TRANSITIVE)
1600 THEN IMP_RES_TAC TC_SUBSET THEN POP_ASSUM (K ALL_TAC)
1601 THEN ASM_REWRITE_TAC[]
1602 THEN REPEAT CONJ_TAC
1603 THENL [ RULE_ASSUM_TAC(REWRITE_RULE[transitive_def]) THEN RES_TAC,
1604 ALL_TAC,ALL_TAC]
1605 THEN MATCH_MP_TAC approx_the_fun1
1606 THEN MATCH_MP_TAC EXISTS_LEMMA
1607 THEN ASM_REWRITE_TAC[]
1608QED
1609
1610
1611(*---------------------------------------------------------------------------*
1612 * This is what is used by TFL. *
1613 *---------------------------------------------------------------------------*)
1614
1615Theorem WFREC_COROLLARY:
1616 !M R (f:'a->'b).
1617 (f = WFREC R M) ==> WF R ==> !x. f x = M (RESTRICT f R x) x
1618Proof
1619REPEAT GEN_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[WFREC_THM]
1620QED
1621
1622
1623(*---------------------------------------------------------------------------*
1624 * The usual phrasing of the wellfounded recursion theorem. *
1625 *---------------------------------------------------------------------------*)
1626
1627Theorem WF_RECURSION_THM:
1628 !R. WF R ==> !M. ?!f:'a->'b. !x. f x = M (RESTRICT f R x) x
1629Proof
1630GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN CONV_TAC EXISTS_UNIQUE_CONV
1631THEN CONJ_TAC THENL
1632[Q.EXISTS_TAC`WFREC R M` THEN MATCH_MP_TAC WFREC_THM THEN POP_ASSUM ACCEPT_TAC,
1633 REPEAT STRIP_TAC THEN CONV_TAC (Q.X_FUN_EQ_CONV`w`) THEN WF_INDUCT_TAC
1634 THEN Q.EXISTS_TAC`R` THEN CONJ_TAC THENL
1635 [ FIRST_ASSUM ACCEPT_TAC,
1636 GEN_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN AP_THM_TAC THEN
1637 AP_TERM_TAC THEN REWRITE_TAC[CUTS_EQ] THEN GEN_TAC THEN
1638 FIRST_ASSUM MATCH_ACCEPT_TAC]]
1639QED
1640
1641
1642(*---------------------------------------------------------------------------*)
1643(* The wellfounded part of a relation. Defined inductively. *)
1644(*---------------------------------------------------------------------------*)
1645
1646val WFP_DEF = Q.new_definition
1647 ("WFP_DEF",
1648 `WFP R a = !P. (!x. (!y. R y x ==> P y) ==> P x) ==> P a`);
1649
1650Theorem WFP_RULES:
1651 !R x. (!y. R y x ==> WFP R y) ==> WFP R x
1652Proof
1653 REWRITE_TAC [WFP_DEF] THEN MESON_TAC []
1654QED
1655
1656Theorem WFP_INDUCT:
1657 !R P. (!x. (!y. R y x ==> P y) ==> P x) ==> !x. WFP R x ==> P x
1658Proof
1659 REWRITE_TAC [WFP_DEF] THEN MESON_TAC []
1660QED
1661
1662Theorem WFP_CASES:
1663 !R x. WFP R x = !y. R y x ==> WFP R y
1664Proof
1665 REPEAT STRIP_TAC THEN EQ_TAC
1666 THENL [Q.ID_SPEC_TAC `x` THEN HO_MATCH_MP_TAC WFP_INDUCT, ALL_TAC]
1667 THEN MESON_TAC [WFP_RULES]
1668QED
1669
1670(* ------------------------------------------------------------------------- *)
1671(* Wellfounded part induction, strong version. *)
1672(* ------------------------------------------------------------------------- *)
1673
1674Theorem WFP_STRONG_INDUCT:
1675 !R. (!x. WFP R x /\ (!y. R y x ==> P y) ==> P x)
1676 ==>
1677 !x. WFP R x ==> P x
1678Proof
1679 REPEAT GEN_TAC THEN STRIP_TAC
1680 THEN ONCE_REWRITE_TAC[TAUT `a ==> b <=> a ==> a /\ b`]
1681 THEN HO_MATCH_MP_TAC WFP_INDUCT THEN ASM_MESON_TAC[WFP_RULES]
1682QED
1683
1684
1685(* ------------------------------------------------------------------------- *)
1686(* A relation is wellfounded iff WFP is the whole universe. *)
1687(* ------------------------------------------------------------------------- *)
1688
1689Theorem WF_EQ_WFP:
1690 !R. WF R = !x. WFP R x
1691Proof
1692 GEN_TAC THEN EQ_TAC THENL
1693 [REWRITE_TAC [WF_EQ_INDUCTION_THM] THEN MESON_TAC [WFP_RULES],
1694 DISCH_TAC THEN MATCH_MP_TAC (SPEC_ALL INDUCTION_WF_THM)
1695 THEN GEN_TAC THEN MP_TAC (SPEC_ALL WFP_STRONG_INDUCT)
1696 THEN ASM_REWRITE_TAC []]
1697QED
1698
1699(*---------------------------------------------------------------------------*)
1700(* A formalization of some of the results in *)
1701(* *)
1702(* "Inductive Invariants for Nested Recursion", *)
1703(* Sava Krsti\'{c} and John Matthews, *)
1704(* TPHOLs 2003, LNCS vol. 2758, pp. 253-269. *)
1705(* *)
1706(*---------------------------------------------------------------------------*)
1707
1708
1709(*---------------------------------------------------------------------------*)
1710(* Definition. P is an "inductive invariant" of the functional M with *)
1711(* respect to the wellfounded relation R. *)
1712(*---------------------------------------------------------------------------*)
1713
1714val INDUCTIVE_INVARIANT_DEF =
1715 Q.new_definition
1716 ("INDUCTIVE_INVARIANT_DEF",
1717 `INDUCTIVE_INVARIANT R P M =
1718 !f x. (!y. R y x ==> P y (f y)) ==> P x (M f x)`);
1719
1720(*---------------------------------------------------------------------------*)
1721(* Definition. P is an inductive invariant of the functional M on set D with *)
1722(* respect to the wellfounded relation R. *)
1723(*---------------------------------------------------------------------------*)
1724
1725val INDUCTIVE_INVARIANT_ON_DEF =
1726 Q.new_definition
1727 ("INDUCTIVE_INVARIANT_ON_DEF",
1728 `INDUCTIVE_INVARIANT_ON R D P M =
1729 !f x. D x /\ (!y. D y ==> R y x ==> P y (f y)) ==> P x (M f x)`);
1730
1731(*---------------------------------------------------------------------------*)
1732(* The key theorem, corresponding to theorem 1 of the paper. *)
1733(*---------------------------------------------------------------------------*)
1734
1735Theorem INDUCTIVE_INVARIANT_WFREC:
1736 !R P M. WF R /\ INDUCTIVE_INVARIANT R P M ==> !x. P x (WFREC R M x)
1737Proof
1738 REPEAT GEN_TAC THEN STRIP_TAC
1739 THEN IMP_RES_THEN HO_MATCH_MP_TAC WF_INDUCTION_THM
1740 THEN FULL_SIMP_TAC bool_ss [INDUCTIVE_INVARIANT_DEF]
1741 THEN METIS_TAC [WFREC_THM,RESTRICT_DEF]
1742QED
1743
1744Theorem TFL_INDUCTIVE_INVARIANT_WFREC:
1745 !f R P M x. (f = WFREC R M) /\ WF R /\ INDUCTIVE_INVARIANT R P M ==> P x (f x)
1746Proof PROVE_TAC [INDUCTIVE_INVARIANT_WFREC]
1747QED
1748
1749val lem =
1750 INDUCTIVE_INVARIANT_WFREC |> Q.SPEC ‘R’ |> Q.SPEC ‘\x y. D x ==> P x y’
1751 |> REWRITE_RULE[INDUCTIVE_INVARIANT_DEF]
1752 |> BETA_RULE
1753
1754Theorem INDUCTIVE_INVARIANT_ON_WFREC:
1755 !R P M D x. WF R /\ INDUCTIVE_INVARIANT_ON R D P M /\ D x ==>
1756 P x (WFREC R M x)
1757Proof
1758 SIMP_TAC bool_ss [INDUCTIVE_INVARIANT_ON_DEF] THEN PROVE_TAC [lem]
1759QED
1760
1761
1762Theorem TFL_INDUCTIVE_INVARIANT_ON_WFREC:
1763 !f R D P M x.
1764 f = WFREC R M /\ WF R /\ INDUCTIVE_INVARIANT_ON R D P M /\ D x ==>
1765 P x (f x)
1766Proof PROVE_TAC [INDUCTIVE_INVARIANT_ON_WFREC]
1767QED
1768
1769local val lem =
1770 GEN_ALL
1771 (REWRITE_RULE []
1772 (BETA_RULE
1773 (Q.INST [`P` |-> `\a b. (M (WFREC R M) a = b) /\
1774 (WFREC R M a = b) /\ P a b`]
1775 (SPEC_ALL INDUCTIVE_INVARIANT_ON_WFREC))))
1776in
1777val IND_FIXPOINT_ON_LEMMA = Q.prove
1778(`!R D M P x.
1779 WF R /\ D x /\
1780 (!f x. D x /\ (!y. D y /\ R y x ==> P y (WFREC R M y) /\ (f y = WFREC R M y))
1781 ==> P x (WFREC R M x) /\ (M f x = WFREC R M x))
1782 ==>
1783 (M (WFREC R M) x = WFREC R M x) /\ P x (WFREC R M x)`,
1784 REPEAT GEN_TAC THEN STRIP_TAC
1785 THEN MATCH_MP_TAC lem
1786 THEN ID_EX_TAC
1787 THEN ASM_REWRITE_TAC [INDUCTIVE_INVARIANT_ON_DEF]
1788 THEN METIS_TAC [])
1789end;
1790
1791(*---------------------------------------------------------------------------*)
1792(* End of Krstic/Matthews results *)
1793(*---------------------------------------------------------------------------*)
1794
1795
1796(* ----------------------------------------------------------------------
1797 inverting a relation
1798 ---------------------------------------------------------------------- *)
1799
1800val inv_DEF = new_definition(
1801 "inv_DEF[simp]",
1802 ``inv (R:'a->'b->bool) x y = R y x``);
1803(* superscript suffix T, for "transpose" *)
1804val _ = add_rule { block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)),
1805 fixity = Suffix 2100,
1806 paren_style = ParoundPrec,
1807 pp_elements = [TOK (UTF8.chr 0x1D40)],
1808 term_name = "relinv"}
1809Overload relinv = ``inv``
1810val _ = TeX_notation { hol = (UTF8.chr 0x1D40),
1811 TeX = ("\\HOLTokenRInverse{}", 1) }
1812
1813Theorem inv_inv[simp]:
1814 !R. inv (inv R) = R
1815Proof SIMP_TAC bool_ss [FUN_EQ_THM, inv_DEF]
1816QED
1817
1818Theorem inv_RC:
1819 !R. inv (RC R) = RC (inv R)
1820Proof
1821 SIMP_TAC bool_ss [RC_DEF, inv_DEF, FUN_EQ_THM] THEN MESON_TAC []
1822QED
1823
1824Theorem inv_SC[simp]:
1825 !R. (inv (SC R) = SC R) /\ (SC (inv R) = SC R)
1826Proof
1827 SIMP_TAC bool_ss [inv_DEF, SC_DEF, FUN_EQ_THM] THEN MESON_TAC []
1828QED
1829
1830Theorem inv_TC:
1831 !R. inv (TC R) = TC (inv R)
1832Proof
1833 GEN_TAC THEN SIMP_TAC bool_ss [FUN_EQ_THM, inv_DEF, EQ_IMP_THM,
1834 FORALL_AND_THM] THEN
1835 CONJ_TAC THENL [
1836 CONV_TAC SWAP_VARS_CONV,
1837 ALL_TAC
1838 ] THEN HO_MATCH_MP_TAC TC_INDUCT THEN
1839 MESON_TAC [inv_DEF, TC_RULES]
1840QED
1841
1842Theorem inv_EQC[simp]:
1843 !R. (inv (EQC R) = EQC R) /\ (EQC (inv R) = EQC R)
1844Proof
1845 SIMP_TAC bool_ss [EQC_DEF, inv_TC, inv_SC, inv_RC]
1846QED
1847
1848Theorem inv_MOVES_OUT:
1849 !R. (inv (inv R) = R) /\ (SC (inv R) = SC R) /\
1850 (RC (inv R) = inv (RC R)) /\ (TC (inv R) = inv (TC R)) /\
1851 (RTC (inv R) = inv (RTC R)) /\ (EQC (inv R) = EQC R)
1852Proof
1853 SIMP_TAC bool_ss [GSYM TC_RC_EQNS, EQC_DEF, inv_TC, inv_SC, inv_inv, inv_RC]
1854QED
1855
1856Theorem reflexive_inv[simp]:
1857 !R. reflexive (inv R) = reflexive R
1858Proof SIMP_TAC bool_ss [inv_DEF, reflexive_def]
1859QED
1860
1861Theorem irreflexive_inv[simp]:
1862 !R. irreflexive (inv R) = irreflexive R
1863Proof
1864 SRW_TAC [][irreflexive_def, inv_DEF]
1865QED
1866
1867Theorem symmetric_inv[simp]:
1868 !R. symmetric (inv R) = symmetric R
1869Proof
1870 SIMP_TAC bool_ss [inv_DEF, symmetric_def] THEN MESON_TAC []
1871QED
1872
1873Theorem antisymmetric_inv[simp]:
1874 !R. antisymmetric (inv R) = antisymmetric R
1875Proof
1876 SRW_TAC [][antisymmetric_def, inv_DEF] THEN PROVE_TAC []
1877QED
1878
1879Theorem transitive_inv[simp]:
1880 !R. transitive (inv R) = transitive R
1881Proof
1882 SIMP_TAC bool_ss [inv_DEF, transitive_def] THEN MESON_TAC []
1883QED
1884
1885Theorem symmetric_inv_identity:
1886 !R. symmetric R ==> (inv R = R)
1887Proof
1888 SIMP_TAC bool_ss [inv_DEF, symmetric_def, FUN_EQ_THM]
1889QED
1890
1891Theorem equivalence_inv_identity:
1892 !R. equivalence R ==> (inv R = R)
1893Proof
1894 SIMP_TAC bool_ss [equivalence_def, symmetric_inv_identity]
1895QED
1896
1897(* ----------------------------------------------------------------------
1898 properties of relations, and set-like operations on relations from
1899 Lockwood Morris
1900 ---------------------------------------------------------------------- *)
1901
1902(* ----------------------------------------------------------------------
1903 Involutions (functions whose square is the identity)
1904 ---------------------------------------------------------------------- *)
1905
1906
1907val INVOL_DEF = new_definition(
1908 "INVOL_DEF",
1909 ``INVOL (f:'z->'z) = (f o f = I)``);
1910
1911Theorem INVOL:
1912 !f:'z->'z. INVOL f = (!x. f (f x) = x)
1913Proof
1914 SRW_TAC [] [FUN_EQ_THM, INVOL_DEF]
1915QED
1916
1917Theorem INVOL_ONE_ONE:
1918 !f:'z->'z. INVOL f ==> (!a b. (f a = f b) = (a = b))
1919Proof
1920 PROVE_TAC [INVOL]
1921QED
1922
1923Theorem INVOL_ONE_ENO:
1924 !f:'z->'z. INVOL f ==> (!a b. (f a = b) = (a = f b))
1925Proof
1926 PROVE_TAC [INVOL]
1927QED
1928
1929(* logical negation is an involution. *)
1930Theorem NOT_INVOL:
1931 INVOL (~)
1932Proof
1933 REWRITE_TAC [INVOL, NOT_CLAUSES]
1934QED
1935
1936(* ----------------------------------------------------------------------
1937 Idempotent functions are those where f o f = f
1938 ---------------------------------------------------------------------- *)
1939
1940val IDEM_DEF = new_definition(
1941 "IDEM_DEF",
1942 ``IDEM (f:'z->'z) = (f o f = f)``);
1943
1944Theorem IDEM:
1945 !f:'z->'z. IDEM f = (!x. f (f x) = f x)
1946Proof
1947 SRW_TAC [][IDEM_DEF, FUN_EQ_THM]
1948QED
1949
1950(* set up Id as a synonym for equality... *)
1951Overload Id = “(=)”
1952
1953(* but prefer = as the printing form when with two arguments *)
1954Overload "=" = “(=)”
1955
1956(* code below even sets things up so that Id is preferred printing form when
1957 an equality term does not have two arguments. It causes grief in
1958 parsing though - another project for the future maybe.
1959val _ = remove_termtok {term_name = "=", tok = "="}
1960val _ = add_rule { block_style = (AroundEachPhrase, (PP.CONSISTENT, 2)),
1961 fixity = Infix(NONASSOC, 100),
1962 paren_style = OnlyIfNecessary,
1963 pp_elements = [HardSpace 1, TOK "=", BreakSpace(1,0)],
1964 term_name = "Id"}
1965*)
1966
1967(* inv is an involution, which we know from theorem inv_inv above *)
1968Theorem inv_INVOL:
1969 INVOL inv
1970Proof
1971 REWRITE_TAC [INVOL, inv_inv]
1972QED
1973
1974(* ----------------------------------------------------------------------
1975 composition of two relations, written O (Isabelle/HOL notation)
1976 ---------------------------------------------------------------------- *)
1977
1978(* This way 'round by analogy with function composition, where the
1979 second argument to composition acts on the "input" first. This is also
1980 consistent with the way this constant is defined in Isabelle/HOL. *)
1981val O_DEF = new_definition(
1982 "O_DEF",
1983 ``(O) R1 R2 (x:'g) (z:'k) = ?y:'h. R2 x y /\ R1 y z``);
1984val _ = set_fixity "O" (Infixr 800)
1985val _ = Unicode.unicode_version {u = UTF8.chr 0x2218 ^ UnicodeChars.sub_r,
1986 tmnm = "O"}
1987val _ = TeX_notation { hol = UTF8.chr 0x2218 ^ UnicodeChars.sub_r,
1988 TeX = ("\\HOLTokenRCompose{}", 1) }
1989
1990Theorem inv_O:
1991 !R R'. inv (R O R') = inv R' O inv R
1992Proof
1993 SRW_TAC [][FUN_EQ_THM, O_DEF, inv_DEF] THEN PROVE_TAC []
1994QED
1995
1996(* ----------------------------------------------------------------------
1997 relational inclusion, analog of SUBSET
1998 ---------------------------------------------------------------------- *)
1999
2000val RSUBSET = new_definition(
2001 "RSUBSET",
2002 ``(RSUBSET) R1 R2 = !x y. R1 x y ==> R2 x y``);
2003val _ = set_fixity "RSUBSET" (Infix(NONASSOC, 450));
2004val _ = OpenTheoryMap.OpenTheory_const_name
2005 {const={Thy="relation",Name="RSUBSET"},
2006 name=(["Relation"],"subrelation")}
2007val _ = Unicode.unicode_version {u = UnicodeChars.subset ^ UnicodeChars.sub_r,
2008 tmnm = "RSUBSET"}
2009val _ = TeX_notation { hol = UnicodeChars.subset ^ UnicodeChars.sub_r,
2010 TeX = ("\\HOLTokenRSubset{}", 1) }
2011
2012Theorem irreflexive_RSUBSET:
2013 !R1 R2. irreflexive R2 /\ R1 RSUBSET R2 ==> irreflexive R1
2014Proof
2015 SRW_TAC [][irreflexive_def, RSUBSET] THEN PROVE_TAC []
2016QED
2017
2018(* ----------------------------------------------------------------------
2019 relational union
2020 ---------------------------------------------------------------------- *)
2021
2022val RUNION = new_definition(
2023 "RUNION",
2024 ``(RUNION) R1 R2 x y <=> R1 x y \/ R2 x y``);
2025val _ = set_fixity "RUNION" (Infixl 500)
2026val _ = OpenTheoryMap.OpenTheory_const_name
2027 {const={Thy="relation",Name="RUNION"},name=(["Relation"],"union")}
2028
2029Theorem RUNION_COMM:
2030 R1 RUNION R2 = R2 RUNION R1
2031Proof
2032 SRW_TAC [][RUNION, FUN_EQ_THM] THEN PROVE_TAC []
2033QED
2034
2035Theorem RUNION_ASSOC:
2036 R1 RUNION (R2 RUNION R3) = (R1 RUNION R2) RUNION R3
2037Proof
2038 SRW_TAC [][RUNION, FUN_EQ_THM] THEN PROVE_TAC []
2039QED
2040
2041val _ = Unicode.unicode_version {u = UnicodeChars.union ^ UnicodeChars.sub_r,
2042 tmnm = "RUNION"}
2043val _ = TeX_notation { hol = UnicodeChars.union ^ UnicodeChars.sub_r,
2044 TeX = ("\\HOLTokenRUnion{}", 1) }
2045
2046(* ----------------------------------------------------------------------
2047 relational intersection
2048 ---------------------------------------------------------------------- *)
2049
2050val RINTER = new_definition(
2051 "RINTER",
2052 ``(RINTER) R1 R2 x y <=> R1 x y /\ R2 x y``);
2053val _ = set_fixity "RINTER" (Infixl 600)
2054val _ = OpenTheoryMap.OpenTheory_const_name
2055 {const={Thy="relation",Name="RINTER"},name=(["Relation"],"intersect")}
2056val _ = Unicode.unicode_version {u = UnicodeChars.inter ^ UnicodeChars.sub_r,
2057 tmnm = "RINTER"}
2058val _ = TeX_notation { hol = UnicodeChars.inter ^ UnicodeChars.sub_r,
2059 TeX = ("\\HOLTokenRInter{}", 1) }
2060
2061Theorem RINTER_COMM:
2062 R1 RINTER R2 = R2 RINTER R1
2063Proof
2064 SRW_TAC [][RINTER, FUN_EQ_THM] THEN PROVE_TAC []
2065QED
2066
2067Theorem RINTER_ASSOC:
2068 R1 RINTER (R2 RINTER R3) = (R1 RINTER R2) RINTER R3
2069Proof
2070 SRW_TAC [][RINTER, FUN_EQ_THM] THEN PROVE_TAC []
2071QED
2072
2073Theorem antisymmetric_RINTER[simp]:
2074 (antisymmetric R1 ==> antisymmetric (R1 RINTER R2)) /\
2075 (antisymmetric R2 ==> antisymmetric (R1 RINTER R2))
2076Proof
2077 SRW_TAC [][antisymmetric_def,RINTER]
2078QED
2079
2080Theorem transitive_RINTER[simp]:
2081 transitive R1 /\ transitive R2 ==> transitive (R1 RINTER R2)
2082Proof
2083 SRW_TAC [SatisfySimps.SATISFY_ss][transitive_def,RINTER]
2084QED
2085
2086Theorem RTC_RINTER:
2087 !R1 R2 x y. RTC (R1 RINTER R2) x y ==> ((RTC R1) RINTER (RTC R2)) x y
2088Proof
2089 ntac 2 gen_tac >>
2090 match_mp_tac RTC_INDUCT >>
2091 asm_simp_tac(srw_ss())[RINTER] >>
2092 METIS_TAC[RTC_CASES1]
2093QED
2094
2095(* ----------------------------------------------------------------------
2096 relational complement
2097 ---------------------------------------------------------------------- *)
2098
2099val RCOMPL = new_definition(
2100 "RCOMPL",
2101 ``RCOMPL R x y = ~R x y``);
2102
2103(* ----------------------------------------------------------------------
2104 theorems about reflexive, symmetric and transitive predicates in
2105 terms of particular relational-subsets
2106 ---------------------------------------------------------------------- *)
2107
2108Theorem reflexive_Id_RSUBSET:
2109 !R. reflexive R = (Id RSUBSET R)
2110Proof
2111 SRW_TAC [][RSUBSET, reflexive_def]
2112QED
2113
2114Theorem symmetric_inv_RSUBSET:
2115 symmetric R = (inv R RSUBSET R)
2116Proof
2117 SRW_TAC [][symmetric_def, inv_DEF, RSUBSET] THEN PROVE_TAC []
2118QED
2119
2120Theorem transitive_O_RSUBSET:
2121 transitive R = (R O R RSUBSET R)
2122Proof
2123 SRW_TAC [][transitive_def, O_DEF, RSUBSET] THEN PROVE_TAC []
2124QED
2125
2126(* ----------------------------------------------------------------------
2127 various sorts of orders
2128 ---------------------------------------------------------------------- *)
2129
2130val PreOrder = new_definition(
2131 "PreOrder",
2132 ``PreOrder R <=> reflexive R /\ transitive R``);
2133
2134(* The following definition follows Rob Arthan's idea of staying mum,
2135 for the most general notion of (partial) order, about whether the
2136 relation is to be reflexive, irreflexive, or something in
2137 between. *)
2138
2139val Order = new_definition(
2140 "Order",
2141 ``Order (Z:'g->'g->bool) <=> antisymmetric Z /\ transitive Z``);
2142
2143val WeakOrder = new_definition(
2144 "WeakOrder",
2145 ``WeakOrder (Z:'g->'g->bool) <=>
2146 reflexive Z /\ antisymmetric Z /\ transitive Z``);
2147
2148val StrongOrder = new_definition(
2149 "StrongOrder",
2150 ``StrongOrder (Z:'g->'g->bool) <=> irreflexive Z /\ transitive Z``);
2151
2152Theorem irrefl_trans_implies_antisym:
2153 !R. irreflexive R /\ transitive R ==> antisymmetric R
2154Proof
2155 SRW_TAC [][antisymmetric_def, transitive_def, irreflexive_def] THEN
2156 METIS_TAC []
2157QED
2158
2159Theorem StrongOrd_Ord:
2160 !R. StrongOrder R ==> Order R
2161Proof
2162 SRW_TAC [][StrongOrder, Order, irrefl_trans_implies_antisym]
2163QED
2164
2165Theorem WeakOrd_Ord:
2166 !R. WeakOrder R ==> Order R
2167Proof
2168 SRW_TAC [][WeakOrder, Order]
2169QED
2170
2171Theorem WeakOrder_EQ:
2172 !R. WeakOrder R ==> !y z. (y = z) <=> R y z /\ R z y
2173Proof
2174 SRW_TAC [][WeakOrder, reflexive_def, antisymmetric_def] THEN PROVE_TAC []
2175QED
2176
2177Theorem RSUBSET_ANTISYM:
2178 !R1 R2. R1 RSUBSET R2 /\ R2 RSUBSET R1 ==> (R1 = R2)
2179Proof
2180 SRW_TAC [][RSUBSET, FUN_EQ_THM] THEN PROVE_TAC []
2181QED
2182
2183Theorem RSUBSET_antisymmetric:
2184 antisymmetric (RSUBSET)
2185Proof
2186 REWRITE_TAC [antisymmetric_def, RSUBSET_ANTISYM]
2187QED
2188
2189Theorem RSUBSET_WeakOrder:
2190 WeakOrder (RSUBSET)
2191Proof
2192 SRW_TAC [][WeakOrder, reflexive_def, antisymmetric_def, transitive_def,
2193 RSUBSET, FUN_EQ_THM] THEN
2194 PROVE_TAC []
2195QED
2196
2197Theorem EqIsBothRSUBSET =
2198 MATCH_MP WeakOrder_EQ RSUBSET_WeakOrder
2199(* |- !y z. (y = z) = y RSUBSET z /\ z RSUBSET y *)
2200
2201(* ----------------------------------------------------------------------
2202 STRORD makes an order strict (or "strong")
2203 ---------------------------------------------------------------------- *)
2204
2205val STRORD = new_definition(
2206 "STRORD",
2207 ``STRORD R a b <=> R a b /\ ~(a = b)``);
2208
2209Theorem STRORD_AND_NOT_Id:
2210 STRORD R = R RINTER (RCOMPL Id)
2211Proof
2212 SRW_TAC [][STRORD, RINTER, RCOMPL, FUN_EQ_THM]
2213QED
2214
2215(* the corresponding "UNSTRORD", which makes an order weak is just RC *)
2216
2217Theorem RC_OR_Id:
2218 RC R = R RUNION Id
2219Proof
2220 SRW_TAC [][RC_DEF, RUNION, FUN_EQ_THM] THEN PROVE_TAC []
2221QED
2222
2223Theorem RC_Weak:
2224 Order R = WeakOrder (RC R)
2225Proof
2226 SRW_TAC [][Order, WeakOrder, EQ_IMP_THM, transitive_RC] THEN
2227 FULL_SIMP_TAC (srw_ss()) [transitive_def, RC_DEF, antisymmetric_def] THEN
2228 PROVE_TAC []
2229QED
2230
2231Theorem STRORD_Strong:
2232 !R. Order R = StrongOrder (STRORD R)
2233Proof
2234 SRW_TAC [][Order, StrongOrder, STRORD, antisymmetric_def, transitive_def,
2235 irreflexive_def] THEN PROVE_TAC []
2236QED
2237
2238Theorem STRORD_RC:
2239 !R. StrongOrder R ==> (STRORD (RC R) = R)
2240Proof
2241 SRW_TAC [][StrongOrder, STRORD, RC_DEF, irreflexive_def, antisymmetric_def,
2242 transitive_def, FUN_EQ_THM] THEN PROVE_TAC []
2243QED
2244
2245Theorem RC_STRORD:
2246 !R. WeakOrder R ==> (RC (STRORD R) = R)
2247Proof
2248 SRW_TAC [][WeakOrder, STRORD, RC_DEF, reflexive_def, antisymmetric_def,
2249 transitive_def, FUN_EQ_THM] THEN PROVE_TAC []
2250QED
2251
2252Theorem IDEM_STRORD:
2253 IDEM STRORD
2254Proof
2255 SRW_TAC [][STRORD, IDEM, FUN_EQ_THM] THEN PROVE_TAC []
2256QED
2257
2258Theorem IDEM_RC:
2259 IDEM RC
2260Proof
2261 SRW_TAC [][IDEM, RC_IDEM]
2262QED
2263
2264Theorem IDEM_SC:
2265 IDEM SC
2266Proof
2267 SRW_TAC [][IDEM, SC_IDEM]
2268QED
2269
2270Theorem IDEM_TC:
2271 IDEM TC
2272Proof
2273 SRW_TAC [][IDEM, TC_IDEM]
2274QED
2275
2276Theorem IDEM_RTC:
2277 IDEM RTC
2278Proof
2279 SRW_TAC [][IDEM, RTC_IDEM]
2280QED
2281
2282Theorem trichotomous_STRORD[simp]:
2283 trichotomous (STRORD R) <=> trichotomous R
2284Proof
2285 SRW_TAC [][STRORD, trichotomous] THEN METIS_TAC[]
2286QED
2287
2288Theorem trichotomous_RC[simp]:
2289 trichotomous (RC R) <=> trichotomous R
2290Proof
2291 SRW_TAC [][RC_DEF, trichotomous] THEN METIS_TAC[]
2292QED
2293
2294(* ----------------------------------------------------------------------
2295 We may define notions of linear (i.e., total) order, but in the
2296 absence of numbers I don't see much to prove about them.
2297 ---------------------------------------------------------------------- *)
2298
2299val LinearOrder = new_definition(
2300 "LinearOrder",
2301 ``LinearOrder (R:'a->'a->bool) <=> Order R /\ trichotomous R``);
2302
2303val StrongLinearOrder = new_definition(
2304 "StrongLinearOrder",
2305 ``StrongLinearOrder (R:'a->'a->bool) <=> StrongOrder R /\ trichotomous R``);
2306
2307val WeakLinearOrder = new_definition(
2308 "WeakLinearOrder",
2309 ``WeakLinearOrder (R:'a->'a->bool) <=> WeakOrder R /\ trichotomous R``);
2310
2311Theorem WeakLinearOrder_dichotomy:
2312 !R:'a->'a->bool. WeakLinearOrder R <=>
2313 WeakOrder R /\ (!a b. R a b \/ R b a)
2314Proof
2315 SRW_TAC [][WeakLinearOrder, trichotomous] THEN
2316 PROVE_TAC [WeakOrder_EQ]
2317QED
2318
2319(* ----------------------------------------------------------------------
2320 other stuff (inspired by Isabelle's Relation theory)
2321 ---------------------------------------------------------------------- *)
2322
2323val diag_def = new_definition(
2324 "diag_def",
2325 ``diag A x y <=> (x = y) /\ x IN A``);
2326
2327(* properties of O *)
2328
2329Theorem O_ASSOC:
2330 R1 O (R2 O R3) = (R1 O R2) O R3
2331Proof
2332 SRW_TAC [][O_DEF, FUN_EQ_THM] THEN PROVE_TAC []
2333QED
2334
2335Theorem Id_O[simp]:
2336 Id O R = R
2337Proof
2338 SRW_TAC [][O_DEF, FUN_EQ_THM]
2339QED
2340
2341Theorem O_Id[simp]:
2342 R O Id = R
2343Proof
2344 SRW_TAC [][O_DEF, FUN_EQ_THM]
2345QED
2346
2347Theorem O_MONO:
2348 R1 RSUBSET R2 /\ S1 RSUBSET S2 ==> (R1 O S1) RSUBSET (R2 O S2)
2349Proof
2350 SRW_TAC [][RSUBSET, O_DEF] THEN PROVE_TAC []
2351QED
2352
2353Theorem inv_Id:
2354 inv Id = Id
2355Proof
2356 SRW_TAC [][FUN_EQ_THM, inv_DEF, EQ_SYM_EQ]
2357QED
2358
2359Theorem inv_diag:
2360 inv (diag A) = diag A
2361Proof
2362 SRW_TAC [][FUN_EQ_THM, inv_DEF, diag_def] THEN PROVE_TAC []
2363QED
2364
2365(* domain of a relation *)
2366(* if I just had UNIONs and the like around, I could prove great things like
2367 RDOM (R RUNION R') = RDOM R UNION RDOM R'
2368 I can still prove x IN RDOM (R1 RUNION R2) = x IN RDOM R1 \/ x IN RDOM R2
2369 though.
2370*)
2371val RDOM_DEF = new_definition(
2372 "RDOM_DEF",
2373 ``RDOM R x = ?y. R x y``);
2374
2375Theorem IN_RDOM:
2376 x IN RDOM R <=> ?y. R x y
2377Proof
2378 SRW_TAC [][RDOM_DEF, IN_DEF]
2379QED
2380
2381(* range of a relation *)
2382val RRANGE_DEF = new_definition(
2383 "RRANGE",
2384 ``RRANGE R y = ?x. R x y``);
2385
2386Theorem IN_RRANGE:
2387 y IN RRANGE R <=> ?x. R x y
2388Proof
2389 SRW_TAC [][RRANGE_DEF, IN_DEF]
2390QED
2391
2392Theorem IN_RDOM_RUNION:
2393 x IN RDOM (R1 RUNION R2) <=> x IN RDOM R1 \/ x IN RDOM R2
2394Proof
2395 SIMP_TAC (srw_ss()) [RDOM_DEF, RUNION, boolTheory.IN_DEF, EXISTS_OR_THM]
2396QED
2397
2398(* top and bottom elements of RSUBSET lattice *)
2399val RUNIV = new_definition(
2400 "RUNIV[simp]",
2401 ``RUNIV x y = T``);
2402val _ = OpenTheoryMap.OpenTheory_const_name
2403 {const={Thy="relation",Name="RUNIV"},name=(["Relation"],"universe")}
2404val _ = Unicode.unicode_version {
2405 u = UnicodeChars.universal_set ^ UnicodeChars.sub_r,
2406 tmnm = "RUNIV"}
2407
2408
2409Theorem RUNIV_SUBSET[simp]:
2410 (RUNIV RSUBSET R <=> (R = RUNIV)) /\
2411 (R RSUBSET RUNIV)
2412Proof
2413 SRW_TAC [][RSUBSET, FUN_EQ_THM]
2414QED
2415
2416Theorem REMPTY_SUBSET[simp]:
2417 REMPTY RSUBSET R /\
2418 (R RSUBSET REMPTY <=> (R = REMPTY))
2419Proof
2420 SRW_TAC [][RSUBSET, FUN_EQ_THM]
2421QED
2422
2423(* ----------------------------------------------------------------------
2424 Restrictions on relations
2425
2426 In theory there are 3 flavours of restriction, each taking a relation
2427 and a set.
2428
2429 1. restricting the domain of a relation (perhaps the most natural,
2430 gets to be RRESTRICT below)
2431 2. restricting the range of a relation
2432 3. restricting both, forcing the relation to be 'a -> 'a -> bool
2433
2434 In addition, it might be nice to have notation for removal of just
2435 one element in each flavour, which can be expressed as restriction
2436 to the complement of the singleton set containing that element.
2437
2438 ---------------------------------------------------------------------- *)
2439
2440val RRESTRICT_DEF = new_definition(
2441 "RRESTRICT_DEF[simp]",
2442 ``RRESTRICT R s (x:'a) (y:'b) <=> R x y /\ x IN s``);
2443
2444Theorem IN_RDOM_RRESTRICT[simp]:
2445 x IN RDOM (RRESTRICT (R:'a -> 'b -> bool) s) <=> x IN RDOM R /\ x IN s
2446Proof
2447 SIMP_TAC bool_ss [boolTheory.IN_DEF, RDOM_DEF, RRESTRICT_DEF] THEN
2448 METIS_TAC[]
2449QED
2450
2451val RDOM_DELETE_DEF = new_definition(
2452 "RDOM_DELETE_DEF[simp]",
2453 ``RDOM_DELETE R x u v <=> R u v /\ u <> x``);
2454
2455(* this syntax is compatible (easily confused) with that for finite maps *)
2456val _ = set_fixity "\\\\" (Infixl 600)
2457Overload "\\\\" = “RDOM_DELETE”
2458
2459Theorem IN_RDOM_DELETE[simp]:
2460 x IN RDOM (R \\ k) <=> x IN RDOM R /\ x <> k
2461Proof
2462 SIMP_TAC bool_ss [boolTheory.IN_DEF, RDOM_DEF, RDOM_DELETE_DEF] THEN
2463 METIS_TAC[]
2464QED
2465
2466
2467
2468
2469(*===========================================================================*)
2470(* Some notions from Term Rewriting Systems, leading to simple results about *)
2471(* things like confluence and normalisation *)
2472(*===========================================================================*)
2473
2474val diamond_def = new_definition(
2475 "diamond_def",
2476 ``diamond (R:'a->'a->bool) = !x y z. R x y /\ R x z ==> ?u. R y u /\ R z u``)
2477
2478val rcdiamond_def = new_definition( (* reflexive closure half diamond *)
2479 "rcdiamond_def",
2480 ``rcdiamond (R:'a->'a->bool) =
2481 !x y z. R x y /\ R x z ==> ?u. RC R y u /\ RC R z u``);
2482
2483val CR_def = new_definition( (* Church-Rosser *)
2484 "CR_def",
2485 ``CR R = diamond (RTC R)``);
2486
2487val WCR_def = new_definition( (* weakly Church-Rosser *)
2488 "WCR_def",
2489 ``WCR R = !x y z. R x y /\ R x z ==> ?u. RTC R y u /\ RTC R z u``);
2490
2491val SN_def = new_definition( (* strongly normalising *)
2492 "SN_def",
2493 ``SN R = WF (inv R)``);
2494
2495val nf_def = new_definition( (* normal-form *)
2496 "nf_def",
2497 ``nf R x = !y. ~R x y``)
2498
2499(* results *)
2500
2501(* that proving rcdiamond R is equivalent to establishing diamond (RC R) *)
2502Theorem rcdiamond_diamond:
2503 !R. rcdiamond R = diamond (RC R)
2504Proof
2505 SRW_TAC [][rcdiamond_def, diamond_def, RC_DEF] THEN
2506 METIS_TAC []
2507QED(* PROVE_TAC can't cope with this *)
2508
2509Theorem diamond_RC_diamond:
2510 !R. diamond R ==> diamond (RC R)
2511Proof
2512 SRW_TAC [][diamond_def, RC_DEF] THEN METIS_TAC []
2513QED
2514
2515Theorem diamond_TC_diamond:
2516 !R. diamond R ==> diamond (TC R)
2517Proof
2518 REWRITE_TAC [diamond_def] THEN GEN_TAC THEN STRIP_TAC THEN
2519 Q_TAC SUFF_TAC
2520 `!x y. TC R x y ==> !z. TC R x z ==> ?u. TC R y u /\ TC R z u` THEN1
2521 METIS_TAC [] THEN
2522 HO_MATCH_MP_TAC TC_INDUCT_LEFT1 THEN
2523 Q.SUBGOAL_THEN
2524 `!x y. TC R x y ==> !z. R x z ==> ?u. TC R y u /\ TC R z u`
2525 ASSUME_TAC
2526 THENL [
2527 HO_MATCH_MP_TAC TC_INDUCT_LEFT1 THEN PROVE_TAC [TC_RULES],
2528 ALL_TAC (* METIS_TAC very slow in comparison on line above *)
2529 ] THEN PROVE_TAC [TC_RULES]
2530QED
2531
2532Theorem RTC_eq_TCRC[local]:
2533 RTC R = TC (RC R)
2534Proof
2535 REWRITE_TAC [TC_RC_EQNS]
2536QED
2537
2538Theorem establish_CR:
2539 !R. (rcdiamond R ==> CR R) /\ (diamond R ==> CR R)
2540Proof
2541 REWRITE_TAC [CR_def, RTC_eq_TCRC] THEN
2542 PROVE_TAC [diamond_RC_diamond, rcdiamond_diamond, diamond_TC_diamond]
2543QED
2544
2545fun (g by tac) =
2546 Q.SUBGOAL_THEN g STRIP_ASSUME_TAC THEN1 tac
2547
2548Theorem Newmans_lemma:
2549 !R. WCR R /\ SN R ==> CR R
2550Proof
2551 REPEAT STRIP_TAC THEN
2552 `WF (TC (inv R))` by PROVE_TAC [WF_TC, SN_def] THEN
2553 REWRITE_TAC [CR_def, diamond_def] THEN
2554 POP_ASSUM (HO_MATCH_MP_TAC o MATCH_MP WF_INDUCTION_THM) THEN
2555 SRW_TAC [][inv_MOVES_OUT, inv_DEF] THEN
2556 `(x = y) \/ ?y1. R x y1 /\ RTC R y1 y` by PROVE_TAC [RTC_CASES1] THENL [
2557 SRW_TAC [][] THEN PROVE_TAC [RTC_RULES],
2558 ALL_TAC
2559 ] THEN
2560 `(x = z) \/ ?z1. R x z1 /\ RTC R z1 z` by PROVE_TAC [RTC_CASES1] THENL [
2561 SRW_TAC [][] THEN PROVE_TAC [RTC_RULES],
2562 ALL_TAC
2563 ] THEN
2564 `?x0. RTC R y1 x0 /\ RTC R z1 x0` by PROVE_TAC [WCR_def] THEN
2565 `TC R x y1 /\ TC R x z1` by PROVE_TAC [TC_RULES] THEN
2566 `?y2. RTC R y y2 /\ RTC R x0 y2` by PROVE_TAC [] THEN
2567 `?z2. RTC R z z2 /\ RTC R x0 z2` by PROVE_TAC [] THEN
2568 `TC R x x0` by PROVE_TAC [EXTEND_RTC_TC] THEN
2569 PROVE_TAC [RTC_RTC]
2570QED
2571
2572Theorem RUNION_RTC_MONOTONE :
2573 !R1 x y. RTC R1 x y ==> !R2. RTC (R1 RUNION R2) x y
2574Proof
2575 GEN_TAC THEN HO_MATCH_MP_TAC RTC_INDUCT THEN
2576 PROVE_TAC [RTC_RULES, RUNION]
2577QED
2578
2579Theorem RTC_RUNION :
2580 !R1 R2. RTC (RTC R1 RUNION RTC R2) = RTC (R1 RUNION R2)
2581Proof
2582 REPEAT GEN_TAC THEN
2583 Q_TAC SUFF_TAC
2584 `(!x y. RTC (RTC R1 RUNION RTC R2) x y ==> RTC (R1 RUNION R2) x y) /\
2585 (!x y. RTC (R1 RUNION R2) x y ==> RTC (RTC R1 RUNION RTC R2) x y)` THEN1
2586 (SIMP_TAC (srw_ss()) [FUN_EQ_THM, EQ_IMP_THM, FORALL_AND_THM] THEN
2587 PROVE_TAC []) THEN CONJ_TAC
2588 THEN HO_MATCH_MP_TAC RTC_INDUCT THENL [
2589 CONJ_TAC THENL [
2590 PROVE_TAC [RTC_RULES],
2591 MAP_EVERY Q.X_GEN_TAC [`x`,`y`,`z`] THEN REPEAT STRIP_TAC THEN
2592 `RTC R1 x y \/ RTC R2 x y` by PROVE_TAC [RUNION] THEN
2593 PROVE_TAC [RUNION_RTC_MONOTONE, RTC_RTC, RUNION_COMM]
2594 ],
2595 CONJ_TAC THENL [
2596 PROVE_TAC [RTC_RULES],
2597 MAP_EVERY Q.X_GEN_TAC [`x`,`y`,`z`] THEN REPEAT STRIP_TAC THEN
2598 `R1 x y \/ R2 x y` by PROVE_TAC [RUNION] THEN
2599 PROVE_TAC [RTC_RULES, RUNION]
2600 ]
2601 ]
2602QED
2603
2604(* ‘RINSERT’ inserts one more element into an existing relation *)
2605val RINSERT = new_definition ("RINSERT",
2606 “RINSERT R a b = \x y. R x y \/ (x = a /\ y = b)”);
2607
2608Theorem RINSERT_IDEM :
2609 !R a b. (RINSERT R a b) a b
2610Proof
2611 SRW_TAC [] [RINSERT]
2612QED
2613
2614Theorem RSUBSET_RINSERT :
2615 !R a b. R RSUBSET (RINSERT R a b)
2616Proof
2617 SRW_TAC [] [RSUBSET, RINSERT]
2618QED