Hi Chun,
learning Holyhammer is also on my TODO list.
One minor trick. I often look at the theory signature instead of the
Script-file. So I read "relationTheory.sig". For the theories comming
with HOL, the signature is available in the HTML help. For my own
theories, I just open the "*Theory.sig" file.
https://hol-theorem-prover.org/kananaskis-10-helpdocs/help/src-sml/htmlsigs/relationTheory.html#LinearOrder-val
Best
Thomas
On 07.04.2017 13:07, Chun Tian (binghe) wrote:
> 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 <tho...@tuerk-brechen.de
> <mailto:tho...@tuerk-brechen.de>> 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 <tho...@tuerk-brechen.de
>> <mailto:tho...@tuerk-brechen.de>> 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 list
>>> hol-info@lists.sourceforge.net
>>> <mailto:hol-info@lists.sourceforge.net>
>>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>> <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 hol-info@lists.sourceforge.net
>> <mailto:hol-info@lists.sourceforge.net>
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>> <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
>> hol-info@lists.sourceforge.net
>> <mailto:hol-info@lists.sourceforge.net>
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>> <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 hol-info@lists.sourceforge.net
> <mailto:hol-info@lists.sourceforge.net>
> https://lists.sourceforge.net/lists/listinfo/hol-info
> <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
> hol-info@lists.sourceforge.net
> 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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
