Ah ... thank you very much!
Chun
> Il giorno 07 apr 2017, alle ore 16:43, Konrad Slind <konrad.sl...@gmail.com>
> ha scritto:
>
> To print theory "foo" as html :
>
> DB.html_theory "foo";
>
> Konrad.
>
>
>> On Fri, Apr 7, 2017 at 6:50 AM, Chun Tian (binghe) <binghe.l...@gmail.com>
>> wrote:
>> yes, I know these signature files, I use them too (when the proofs do not
>> interest me), but I found that, in signatures, all theorems and definitions
>> are sorted in lexicographic order, which is sometimes very different from
>> the source scripts. But the source scripts well preserved the relationships
>> (and dependences) between theorems, i.e. later theorems were proved by
>> previous theorems, they're kind of very useful information to me.
>>
>> By the way, is it possible to generate HTML files from any theory signature?
>> I know how to use EmitTeX.print_theories_as_tex_doc() to print my theory
>> into PDF finally. But I find HOL's HTML outputs beautiful and compat, I
>> would like have the same for my own theories ... (sorry for bring this last
>> question to you, today ^_^)
>>
>> Regards,
>>
>> Chun
>>
>>> On 7 April 2017 at 13:17, Thomas Tuerk <tho...@tuerk-brechen.de> wrote:
>>> 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> 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> 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
>>>>>>>> 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
>>>>>>
>>>>>> --
>>>>>> ---
>>>>>> 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
>>>>
>>>> --
>>>> ---
>>>> 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
>>>
>>
>>
>>
>> --
>> 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
