[opentheory-users] article reader for HOL4

[Ramana Kumar]

On Sun, Jan 9, 2011 at 8:43 PM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
> On Sun, Jan 9, 2011 at 7:08 PM, Joe Hurd <joe at gilith.com> wrote:
>> Hi Ramana,
>>
>> Thanks for implementing this: HOL4 is now the first theorem prover
>> with an article reader!
>>
>> I'd like to try it out: how do I run it?
>
> At this stage it's going to break on anything interesting you try it on...
> But the basic method would be:
>
> Build the latest svn version of HOL4
>
> In a HOL4 session, do:
>
> val input = (* article file, e.g. TextIO.openIn("/path/to/file.art") *)
> val asms = (* net of theorems the article depends on, you can use
> Opentheory.thmsFromList ls to create this from a list of HOL4 theorems *)
> val consts = (* dictionary of constants the article depends on, keyed by their
> name, and represented by functions (hol_type -> term).
> You can use Opentheory.constsFromList ls,
> e.g. constsFromList [("=",fn ty => Term.mk_const("=",ty))] *)
> val types = (* dictionary of types the article depends on, keyed by their
> names, and represented by functions (hol_type list -> hol-type).
> You can use Opentheory.typesFromList ls,
> e.g. typesFromList [("->",fn ls => Type.mk_type("fun",ls))] *)
> val thms = Opentheory.read_article input {thms=asms,consts=consts,types=types}
>
> If all goes well, thms should be bound to a list of theorems proved by
> the article.

I'm starting to discover that this design may be quite broken...
articles can depend on assumption expressed using constants and types
defined by the article - how am I supposed to pass those in as
theorems to read_article? For example the bool-1.0 package has an
axiom |- !t. (\x. t x) = t, which is provable in HOL using HOL's
definition of !, but the package wants that theorem for it's own
version of ! that it defines itself...

I think I must have fundamentally misunderstood how articles are
supposed to be used. I guess instead of actually defining new
constants while reading an article, one should just pass in constants
that you want to act like the ones the article is going to define, and
pass in theorems you already know about them for the article's
axioms..?

What's the difference between an assumption and an axiom?
opentheory info --summary gives lists of input type operators, input
constants, assumptions, defined constants, axioms, and theorems.
My new understanding of how to deal with these is as follows:
input type operators: existing type operators
input constants: existing constants
assumptions: unknown? actually these are probably just theorems about
the input constants, which can be supplied
defined constants: existing constants that you want the article to
provide you more theorems about
axioms: theorems you need to supply about the defined constants
theorems: theorems you get by reading the article

Does this make sense?
I will try reworking my reader to act like this...

>
>>
>> Cheers,
>>
>> Joe
>>
>> On Sun, Jan 9, 2011 at 5:43 AM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
>>> I have added a preliminary version of an article reader to HOL4
>>> (hol.sf.net, svn r8839)
>>>
>>> Which other proof assistants have readers, by the way? Is there a list
>>> somewhere?
>>>
>>> On Sat, Jan 8, 2011 at 5:54 PM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
>>>> Does anyone know if there's an article reader for HOL4?
>>>> Or, in fact, which theorem provers have article readers, and where can
>>>> they be found?
>>>> I'm thinking if there is none for HOL4 I should write it, and then put
>>>> it with the HOL4 sources - or should it come with the opentheory?
>>>>
>>>
>>> _______________________________________________
>>> opentheory-users mailing list
>>> opentheory-users at gilith.com
>>> http://www.gilith.com/opentheory/mailing-list
>>>
>>
>> _______________________________________________
>> opentheory-users mailing list
>> opentheory-users at gilith.com
>> http://www.gilith.com/opentheory/mailing-list
>>
>