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
>>> listhol-info@lists.sourceforge.nethttps://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
>> listhol-info@lists.sourceforge.nethttps://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
> listhol-info@lists.sourceforge.nethttps://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
