Hi,
1) They are the same. You can easily proof with induction (see below).
2) Yes you can prove it. You would also do it via some kind of induction
proof. However there is no need, since it is already present in the
relationTheory as RTC_INDUCT_RIGHT1.
Cheers
Thomas
open relationTheory
val (RTC1_rules, RTC1_ind, RTC1_cases) = Hol_reln `
(!x. RTC1 R x x) /\
(!x y z. R x y /\ RTC1 R y z ==> RTC1 R x z)`;
val (RTC2_rules, RTC2_ind, RTC2_cases) = Hol_reln `
(!x. RTC2 R x x) /\
(!x y z. RTC2 R x y /\ R y z ==> RTC2 R x z)`;
val RTC1_ALT_DEF = prove (``RTC1 = RTC``,
`!R. (!x y. RTC1 R x y ==> RTC R x y) /\
(!x y. RTC R x y ==> RTC1 R x y)` suffices_by (
SIMP_TAC std_ss [FUN_EQ_THM] THEN METIS_TAC[FUN_EQ_THM])
THEN
GEN_TAC THEN CONJ_TAC THENL [
Induct_on `RTC1` THEN
METIS_TAC [RTC_RULES],
MATCH_MP_TAC RTC_INDUCT THEN
METIS_TAC[RTC1_rules]
]);
val RTC2_ALT_DEF = prove (``RTC2 = RTC``,
`!R. (!x y. RTC2 R x y ==> RTC R x y) /\
(!x y. RTC R x y ==> RTC2 R x y)` suffices_by (
SIMP_TAC std_ss [FUN_EQ_THM] THEN METIS_TAC[FUN_EQ_THM])
THEN
GEN_TAC THEN CONJ_TAC THENL [
Induct_on `RTC2` THEN
METIS_TAC [RTC_RULES_RIGHT1],
MATCH_MP_TAC RTC_INDUCT_RIGHT1 THEN
METIS_TAC[RTC2_rules]
]);
On 07.04.2017 11:49, Chun Tian (binghe) wrote:
> Hi,
>
> If I try to define RTC manually (like those in HOL tutorial, chapter
> 6, page 74):
>
> val (RTC1_rules, RTC1_ind, RTC1_cases) = Hol_reln `
> (!x. RTC1 R x x) /\
> (!x y z. R x y /\ RTC1 R y z ==> RTC1 R x z)`;
>
> It seems that (maybe) I can also define the "same" relation with a
> different transitive rule:
>
> val (RTC2_rules, RTC2_ind, RTC2_cases) = Hol_reln `
> (!x. RTC2 R x x) /\
> (!x y z. RTC2 R x y /\ R y z ==> RTC2 R x z)`;
>
> Here are some observations:
>
> 1. If I directly use the RTC definition from HOL's relationTheory,
> above two transitive rules are both true, easily provable by theorems
> RTC_CASES1 and RTC_CASES2 (relationTheory):
>
> > RTC_CASES1;
> val it =
> |- ∀R x y. R^* x y ⇔ (x = y) ∨ ∃u. R x u ∧ R^* u y:
> thm
> > RTC_CASES2;
> val it =
> |- ∀R x y. R^* x y ⇔ (x = y) ∨ ∃u. R^* x u ∧ R u y:
> thm
>
> 2. The theorem RTC1_ind (generated by Hol_reln) is the same as
> theorem RTC_INDUCT (relationTheory):
>
> val RTC1_ind =
> |- ∀R RTC1'.
> (∀x. RTC1' x x) ∧ (∀x y z. R x y ∧ RTC1' y z ⇒ RTC1' x z) ⇒
> ∀a0 a1. RTC1 R a0 a1 ⇒ RTC1' a0 a1:
> thm
>
> > RTC_INDUCT;
> val it =
> |- ∀R P.
> (∀x. P x x) ∧ (∀x y z. R x y ∧ P y z ⇒ P x z) ⇒
> ∀x y. R^* x y ⇒ P x y:
> thm
>
> Now my questions are:
>
> 1. Given any R, are the two relations (RTC1 R) and (RTC2 R) really the
> same? i.e. is ``!R x y. RTC1 R x y = RTC2 R x y`` a theorem? (and if
> so, how to prove it?)
>
> 2. (If the answer of last question is yes) Is it possible to prove the
> following theorem RTC_INDUCT2 in relationTheory? (which looks like
> RTC2_ind generated in above definition)
>
> val RTC_INDUCT2 = store_thm(
> "RTC_INDUCT2",
> ``!R P. (!x. P x x) /\ (!x y z. P x y /\ R y z ==> P x z) ==>
> (!x (y:'a). RTC R x y ==> P x y)``,
> cheat);
>
> (and the corresponding RTC_STRONG_INDUCT2).
>
> 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
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
