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