Re: [Hol-info] Questions about RTC (reflexive transitive closure)

Ah ... thank you very much! Chun > Il giorno 07 apr 2017, alle ore 16:43, Konrad Slind > 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) >>

Re: [Hol-info] Questions about RTC (reflexive transitive closure)

To print theory "foo" as html : DB.html_theory "foo"; Konrad. On Fri, Apr 7, 2017 at 6:50 AM, Chun Tian (binghe) 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

Re: [Hol-info] Questions about RTC (reflexive transitive closure)

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

Re: [Hol-info] Questions about RTC (reflexive transitive closure)

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

Re: [Hol-info] Questions about RTC (reflexive transitive closure)

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

Re: [Hol-info] Questions about RTC (reflexive transitive closure)

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, > >

Re: [Hol-info] Questions about RTC (reflexive transitive closure)

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 wrote: > Hi, > > 1) They are the same. You can easily proof

Re: [Hol-info] Questions about RTC (reflexive transitive closure)

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