src/relation/relationScript.sml

62 (* The TC and RTC suffixes are tighter than function application.  This
71    `TC (R:'a->'a->bool) a b =
78                    term_name = "TC" }
79 val _ = Unicode.unicode_version {u = Unicode.UChar.sup_plus, tmnm = "TC"}
83 val _ = OpenTheoryMap.OpenTheory_const_name {const={Thy="relation",Name="TC"},name=(["Relation"],"transitiveClosure")}
108   ``EQC (R:'a->'a->bool) = RC (TC (SC R))``);
122  `!R:'a->'a->bool. transitive(TC R)`,
136   ``!R. (!x (y:'a). R x y ==> TC R x y) /\
137         (!x y z. TC R x y /\ TC R y z ==> TC R x z)``,
250 `!R x (y:'a). R x y ==> TC R x y`,
318    ==> !u v. (TC R) u v ==> P u v`,
323    ``!R x y. tc R x y = TC R x y``),
331    ``!R x y. tc R x y = TC R x y``),
354           val (TC, R, u', v') = case strip_comb ant of
355               (TC, [R, u', v']) => (TC, R, u', v')
357           val _ = assert (equal "TC") (fst (dest_const TC))
371           (!x y z. P x y /\ P y z /\ TC R x y /\ TC R y z ==> P x z) ==>
372           (!u v. TC R u v ==> P u v /\ TC R u v)``,
379           (!x y z. P x y /\ P y z /\ TC R x y /\ TC R y z ==> P x z) ==>
380           (!u v. TC R u v ==> P u v)``,
385           (!x y z. R x y /\ P y z /\ TC R y z ==> P x z) ==>
386           (!u v. TC R u v ==> P u v /\ TC R u v)``,
392           (!x y z. P x y /\ TC R x y /\ R y z ==> P x z) ==>
393           (!u v. TC R u v ==> P u v /\ TC R u v)``,
400           (!x y z. R x y /\ P y z /\ TC R y z ==> P x z) ==>
401           (!u v. TC R u v ==> P u v)``,
406           (!x y z. P x y /\ TC R x y /\ R y z ==> P x z) ==>
407           (!u v. TC R u v ==> P u v)``,
411   but only for particular cases of x or y in TC R x y *)
425     !a. TC R a b ==> Q a`,
426   tc_ind_alt_tacs TC_INDUCT_LEFT1 `\x y. if y = b then Q x else TC R x y`) ;
430     !b. TC R a b ==> Q b`,
431   tc_ind_alt_tacs TC_INDUCT_RIGHT1 `\x y. if x = a then Q y else TC R x y`) ;
436     !x y. TC R x y ==> TC R (f x) (f y)``,
442   ``(!x y. P x /\ R x y ==> P y) ==> (!x y. P x /\ TC R x y ==> P y)``,
444   Q_TAC SUFF_TAC `!x y. TC R x y ==> P x ==> P y` THEN1 METIS_TAC [] THEN
449   ``(!x y. R x y ==> (f x = f y)) ==> (!x y. TC R x y ==> (f x = f y))``,
456     (!x y. TC R x y ==> Q (f x) (f y))``,
469   ``!R (x:'a) y. TC R x y ==> RTC R x y``,
474   ``!R (x:'a) y. RTC R x y ==> RC R x y \/ TC R x y``,
484   ``!R:'a->'a->bool. (RC (TC R) = RTC R) /\ (TC (RC R) = RTC R)``,
559   ``!R x y z. R x y /\ RTC R y z ==> TC R x z``,
561   Q_TAC SUFF_TAC `!y z. RTC R y z ==> !x. R x y ==> TC R x z` THEN1
569   ``!R x z. TC R x z = ?y. (R x y /\ RTC R y z)``,
571   Q_TAC SUFF_TAC `!x z. TC R x z ==> ?y. R x y /\ RTC R y z` THEN1
589   ``!R. transitive R ==> (TC R = R)``,
608   ``!R:'a->'a->bool.  TC (TC R) = TC R``,
615         (TC (RC R) = RC (TC R))``,
621   ``!R. symmetric R ==> symmetric (TC R)``,
630   ``!R. reflexive R ==> reflexive (TC R)``,
686   `!R x z. TC R x z ==> R x z \/ ?y:'a. R x y /\ TC R y z`,
693   ``TC R x z <=> R x z \/ ?y:'a. R x y /\ TC R y z``,
699     `!R x z. TC R x z ==> R x z \/ ?y:'a. TC R x y /\ R y z`,
706   ``TC R x z <=> R x z \/ ?y:'a. TC R x y /\ R y z``,
711   ``(!x y. R x y ==> Q x y) ==> TC R x y ==> TC Q x y``,
730   Q.PAT_X_ASSUM `TC _ x y` MP_TAC THEN
752   Q.SUBGOAL_THEN `symmetric (TC (SC R))` ASSUME_TAC THEN1
780 `!R. (EQC (RC R) = EQC R) /\ (EQC (SC R) = EQC R) /\ (EQC (TC R) = EQC R)`,
1032 `!R:'a->'a->bool. WF R ==> WF(TC R)`,
1036        Q.EXISTS_TAC`\m:'a. ?a z. B a /\ TC R a m /\ TC R m z /\ B z`
1041   Q.X_GEN_TAC`m` THEN STRIP_TAC THEN Q.UNDISCH_TAC`TC R (a:'a) m`
1060   ``WF R ==> TC R x y ==> x <> y``,
1068   STRIP_TAC THEN Q_TAC SUFF_TAC `TC R a a` THEN1 METIS_TAC [WF_noloops] THEN
1254  *    \p. R p x => the_fun (TC R) (\f v. M (f%R,v) v) x p | Arb
1267      \x. M (RESTRICT (the_fun (TC R) (\f v. M (RESTRICT f R v) v) x) R x) x`);
1360  * Unrolling works for any R M and x, hence it works for "TC R" and
1368      (Q.SPECL[`TC R`,`\f v. M (RESTRICT f R v) v`,`x`] the_fun_unroll));
1375  `!(f:'a->'b) R w. RESTRICT (RESTRICT f (TC R) w) R w = RESTRICT f R w`,
1401   THEN MAP_EVERY Q.EXISTS_TAC [`TC R`, `\f v. M (RESTRICT f R v) v`, `x`, `y`]
1619   ``!R. inv (TC R) = TC (inv R)``,
1636         (RC (inv R) = inv (RC R)) /\ (TC (inv R) = inv (TC R)) /\
2008   ``IDEM TC``,
2243   ``!R. diamond R ==> diamond (TC R)``,
2246         `!x y. TC R x y ==> !z. TC R x z ==> ?u. TC R y u /\ TC R z u` THEN1
2250     `!x y. TC R x y ==> !z. R x z ==> ?u. TC R y u /\ TC R z u`
2258   ``RTC R = TC (RC R)``,
2274   `WF (TC (inv R))` by PROVE_TAC [WF_TC, SN_def] THEN
2287   `TC R x y1 /\ TC R x z1` by PROVE_TAC [TC_RULES] THEN
2290   `TC R x x0` by PROVE_TAC [EXTEND_RTC_TC] THEN