Hi,
In listTheory there's a concept called "LRC":
(* ----------------------------------------------------------------------
LRC
Where NRC has the number of steps in a transitive path,
LRC has a list of the elements in the path (excluding the rightmost)
---------------------------------------------------------------------- *)
val LRC_def = Define`
(LRC R [] x y = (x = y)) /\
(LRC R (h::t) x y =
(x = h) /\ ?z. R x z /\ LRC R t z y)`;
But I think a more useful similar concept should be a Reflexive Transitive
Closure which is able to remember all the transition labels in a relation R
(of type 'a -> 'b -> 'a -> bool), that is:
val LRTC_DEF = new_definition ("LRTC_DEF",
``LRTC (R :'a -> 'b -> 'a -> bool) a l b =
!P. (!x. P x [] x) /\
(!x h y t z. R x h y /\ P y t z ==> P x (h :: t) z) ==> P a l
b``);
For example, if we have a relation R and things like P --a--> Q, Q --b-->
R, the resulting closure (LRTC R) can be used to describe P --[a;b]--> R.
Following a similar path with RTC in relationTheory, I can prove the
following basic theorems:
[LRTC0_NO_TRANS] Theorem
|- ∀R x y. LRTC R x [] y ⇔ (x = y)
[LRTC_CASES1] Theorem
|- ∀R x l y.
LRTC R x l y ⇔
if NULL l then x = y else ∃u. R x (HD l) u ∧ LRTC R u (TL l) y
[LRTC_CASES2] Theorem
|- ∀R x l y.
LRTC R x l y ⇔
if NULL l then x = y
else ∃u. LRTC R x (FRONT l) u ∧ R u (LAST l) y
[LRTC_CASES_LRTC_TWICE] Theorem
|- ∀R x l y.
LRTC R x l y ⇔
∃u l1 l2. LRTC R x l1 u ∧ LRTC R u l2 y ∧ (l = l1 ⧺ l2)
[LRTC_INDUCT] Theorem
|- ∀R P.
(∀x. P x [] x) ∧
(∀x h y t z. R x h y ∧ P y t z ⇒ P x (h::t) z) ⇒
∀x l y. LRTC R x l y ⇒ P x l y
[LRTC_LRTC] Theorem
|- ∀R x m y. LRTC R x m y ⇒ ∀n z. LRTC R y n z ⇒ LRTC R x (m ⧺ n) z
[LRTC_REFL] Theorem
|- ∀R. LRTC R x [] x
[LRTC_RULES] Theorem
|- ∀R.
(∀x. LRTC R x [] x) ∧
∀x h y t z. R x h y ∧ LRTC R y t z ⇒ LRTC R x (h::t) z
[LRTC_SINGLE] Theorem
|- ∀R x t y. R x t y ⇒ LRTC R x [t] y
[LRTC_STRONG_INDUCT] Theorem
|- ∀R P.
(∀x. P x [] x) ∧
(∀x h y t z. R x h y ∧ LRTC R y t z ∧ P y t z ⇒ P x (h::t) z) ⇒
∀x l y. LRTC R x l y ⇒ P x l y
[LRTC_TRANS] Theorem
|- ∀R x m y n z. LRTC R x m y ∧ LRTC R y n z ⇒ LRTC R x (m ⧺ n) z
Is this something general enough for putting into, say, rich_listTheory?
(or has anyone already done a similar development?)
Regards,
--
Chun Tian (binghe)
University of Bologna (Italy)
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
