Re: [Hol-info] LRTC (Reflexive Transitive Closure with a List)

2017-10-23 Thread Chun Tian 
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

Re: [Hol-info] LRTC (Reflexive Transitive Closure with a List)

2017-10-22 Thread Michael.Norrish 
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)

--
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

[Hol-info] LRTC (Reflexive Transitive Closure with a List)

2017-10-05 Thread Chun Tian (binghe) 
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