Hi Michael, Thanks, I’ll see if I can directly use something from pathTheory.
Regards,
Chun
> Il giorno 23 ott 2017, alle ore 02:23, michael.norr...@data61.csiro.au ha
> scritto:
>
> I’m afraid I can’t now remember if someone has already pointed this out, but
> I think you probably should use the theory of “paths” for this sort of thing.
>
> See the description in the DESCRIPTION manual, and the theory itself in
> src/path
>
> Michael
>
> From: "Chun Tian (binghe)" <binghe.l...@gmail.com>
> Date: Thursday, 5 October 2017 at 23:35
> To: hol-info <hol-info@lists.sourceforge.net>
> Subject: [Hol-info] LRTC (Reflexive Transitive Closure with a List)
>
> 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)
>
signature.asc
Description: Message signed with OpenPGP using GPGMail
------------------------------------------------------------------------------ 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
