Thanks again, this is really convenient.
Actually a large piece of my time was spent on reading HOL's
relationScript.sml and other scripts that I needed, I try to find useful
theorems by their name (otherwise I couldn't know RTC_CASES*, RTC_INDUCT,
RTC_SINGLE, etc.), but maybe the scripts are too long, I don't know how to
I missed RTC_INDUCT_RIGHT1, etc.)
I hope one day I could learn to use the Holyhammer ...
Regards,
Chun
On 7 April 2017 at 12:57, Thomas Tuerk <[email protected]> wrote:
> Hi Chun,
>
> by the way. I always find DB.match and DB.find very helpful. You can for
> example try
>
> DB.print_match [] ``RTC``
> DB.print_match [] ``RTC _ x x``
> DB.print_find "RTC"
> to find interesting theorems about RTC.
>
> Cheers
>
> Thomas
>
>
> On 07.04.2017 12:51, Chun Tian (binghe) wrote:
>
> Hi Thomas,
>
> Thank you very much!! Obviously I didn't know those RTC_ALT* and
> RTC_RIGHT* series of theorems before. Now I can prove something new:)
>
> Best regards,
>
> Chun
>
>
> On 7 April 2017 at 12:08, Thomas Tuerk <[email protected]> wrote:
>
>> 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
>> [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
>
> --
> ---
> 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
> [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
>
>
--
---
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
