[opentheory-users] Error in importing

[Joe Leslie-Hurd]

Hi Robert,

This is every theorem th from basics.ml to realax.ml for which there was a call

export_thm th;;

which means that the theorem is part of the standard theory library.

Cheers,

Joe

On Mon, Jun 8, 2015 at 9:50 AM, Robert White
<ai.robert.wangshuai at gmail.com> wrote:
> Hello again.
>
> One more question:
>
> These are the thms exported as a result of loading hol.ml?
>
> So am I right to say that these are the thms from basics.ml to relax.ml
> (according to the order in hol.ml)?
>
> Thanks.
>
> Regards,
> Robert
>
>
> On 8 June 2015 at 18:47, Robert White <ai.robert.wangshuai at gmail.com> wrote:
>>
>> Dear Joe,
>>
>> Thanks very much!
>>
>> It is really helpful.
>>
>> Thanks a lot for your help :)
>>
>> Regards,
>> Robert
>>
>> On 8 June 2015 at 18:13, Joe Leslie-Hurd <joe at gilith.com> wrote:
>>>
>>> Hi Robert,
>>>
>>> If you do a pull I've added a function that will list every exported
>>> theorem, so you can do:
>>>
>>> #use "hol.ml";;
>>> Export.list_the_exported_thms ();;
>>>
>>> Please let me know if that gives you what you need.
>>>
>>> Cheers,
>>>
>>> Joe
>>>
>>> On Mon, Jun 8, 2015 at 8:50 AM, Robert White
>>> <ai.robert.wangshuai at gmail.com> wrote:
>>> > Dear Joe,
>>> >
>>> > I need to do some checking and proofs of these proofs. so Logically
>>> > using
>>> > these proofs directly is a good thing but I can't find a "list" I can
>>> > simply
>>> > use. So I was trying to load from the .art files.
>>> >
>>> > Do you know if there is any way to get a list of these thms? If so then
>>> > the
>>> > problem is solved.
>>> >
>>> > Thanks
>>> > Robert
>>> >
>>> >
>>> >
>>> > On 8 June 2015 at 17:45, Joe Leslie-Hurd <joe at gilith.com> wrote:
>>> >>
>>> >> Hi Robert,
>>> >>
>>> >> Did you have a specific reason for wanting to load the standard theory
>>> >> library into HOL Light? You could regard this as already being loaded
>>> >> when you execute
>>> >>
>>> >> #use "hol.ml";;
>>> >>
>>> >> It would be possible to reload articles from the standard theory into
>>> >> HOL Light with some changes to import.ml, but right now I can't see a
>>> >> use-case for it.
>>> >>
>>> >> Cheers,
>>> >>
>>> >> Joe
>>> >>
>>> >> On Mon, Jun 8, 2015 at 8:35 AM, Robert White
>>> >> <ai.robert.wangshuai at gmail.com> wrote:
>>> >> > Dear Joe,
>>> >> >
>>> >> > Okay, looks I have no way to load the others for now then.
>>> >> > I will just play with these three first.
>>> >> >
>>> >> > Thanks again for your advice.
>>> >> >
>>> >> > Regards,
>>> >> > Rob
>>> >> >
>>> >> > On 8 June 2015 at 17:27, Joe Leslie-Hurd <joe at gilith.com> wrote:
>>> >> >>
>>> >> >> Hi Robert,
>>> >> >>
>>> >> >> The theories that are causing you errors are part of the standard
>>> >> >> theory library:
>>> >> >>
>>> >> >> $ opentheory list 'Includes base'
>>> >> >> bool-1.36
>>> >> >> function-1.55
>>> >> >> list-1.103
>>> >> >> natural-1.104
>>> >> >> option-1.72
>>> >> >> pair-1.27
>>> >> >> real-1.61
>>> >> >> relation-1.60
>>> >> >> set-1.71
>>> >> >> sum-1.61
>>> >> >> unit-1.20
>>> >> >>
>>> >> >> Since HOL Light already implements the standard theory library,
>>> >> >> trying
>>> >> >> to reload it will generate errors about defining symbols, as you
>>> >> >> have
>>> >> >> experienced.
>>> >> >>
>>> >> >> My advice is to focus on theories that are not part of the standard
>>> >> >> theory library, the easiest to obtain being those on the OpenTheory
>>> >> >> repo:
>>> >> >>
>>> >> >> http://opentheory.gilith.com/packages/
>>> >> >>
>>> >> >> Cheers,
>>> >> >>
>>> >> >> Joe
>>> >> >>
>>> >> >> On Mon, Jun 8, 2015 at 4:34 AM, Robert White
>>> >> >> <ai.robert.wangshuai at gmail.com> wrote:
>>> >> >> > Dear Joe,
>>> >> >> >
>>> >> >> > Hello. I have the following errors:
>>> >> >> >
>>> >> >> > # extend_the_interpretation
>>> >> >> > "opentheory/theories/list/list.int";;
>>> >> >> > val it : unit = ()
>>> >> >> > # let all= import_article "opentheory/articles/list.art";;
>>> >> >> > Exception:
>>> >> >> > Failure
>>> >> >> >  "in article opentheory/articles/list.art at line 467:
>>> >> >> > defineConst\nstack =
>>> >> >> > [Term; \"HOLLight.NUMSUM\"; Term; Term; Term; Var; Term; Var;
>>> >> >> > Term;
>>> >> >> > Var;
>>> >> >> > Term; Var; [[\"HOLLight.NUMLEFT\"; Var]]; Term; Var; Var; Var;
>>> >> >> > Var;
>>> >> >> > \"HOLLight.INJP\"; \"HOLLight.ZBOT\"; Term; Term; Term; Var;
>>> >> >> > Term;
>>> >> >> > Term;
>>> >> >> > Var; Term; Var; \"HOLLight.ZRECSPACE\"; [\"A\"];
>>> >> >> > \"HOLLight._dest_rec\";
>>> >> >> > \"HOLLight._mk_rec\"; \"HOLLight.recspace\"; \"a1\"; Var;
>>> >> >> > [\"A\"];
>>> >> >> > \"HOLLight._dest_list\"; \"HOLLight._mk_list\";
>>> >> >> > \"Data.List.list\";
>>> >> >> > TypeOp<fun>; \"NULL\"; \"Data.List.null\"; Var; [];
>>> >> >> > Thm]\nnew_constant:
>>> >> >> > constant NUMSUM has already been declared".
>>> >> >> >
>>> >> >> > # let all= import_article "opentheory/articles/sum.art";;
>>> >> >> > Exception:
>>> >> >> > Failure
>>> >> >> >  "in article opentheory/articles/sum.art at line 499:
>>> >> >> > defineConst\nstack
>>> >> >> > =
>>> >> >> > [Term; \"HOLLight.NUMSUM\"; Term; Term; Term; Var; Term; Var;
>>> >> >> > Term;
>>> >> >> > Var;
>>> >> >> > Term; Var; [[\"HOLLight.NUMLEFT\"; Var]]; Term; Var; Var; Var;
>>> >> >> > Var;
>>> >> >> > \"HOLLight.INJP\"; \"HOLLight.ZBOT\"; Term; Term; Term; Var;
>>> >> >> > Term;
>>> >> >> > Term;
>>> >> >> > Var; Term; Var; \"HOLLight.ZRECSPACE\"; [\"A\"];
>>> >> >> > \"HOLLight._dest_rec\";
>>> >> >> > \"HOLLight._mk_rec\"; \"HOLLight.recspace\"; Type; TypeOp<fun>;
>>> >> >> > \"_15483\";
>>> >> >> > Var; Var; \"HOLLight.CONSTR\"; Var; [\"A\"; \"B\"];
>>> >> >> > \"HOLLight._dest_sum\";
>>> >> >> > \"HOLLight._mk_sum\"; \"Data.Sum.+\"; TypeOp<fun>; \"ISL\";
>>> >> >> > \"Data.Sum.isLeft\"; Var; []; Var; Thm; Thm]\nnew_constant:
>>> >> >> > constant
>>> >> >> > NUMSUM
>>> >> >> > has already been declared".
>>> >> >> >
>>> >> >> >
>>> >> >> > # extend_the_interpretation
>>> >> >> > "opentheory/theories/bool/bool.int";;
>>> >> >> > Exception:
>>> >> >> > Sys_error "opentheory/theories/bool/bool.int: No such file or
>>> >> >> > directory".
>>> >> >> >
>>> >> >> > # extend_the_interpretation
>>> >> >> > "opentheory/theories/bool/bool.int";;
>>> >> >> > Exception:
>>> >> >> > Sys_error "opentheory/theories/bool/bool.int: No such file or
>>> >> >> > directory".
>>> >> >> > # let all= import_article "opentheory/articles/bool.art";;
>>> >> >> > Exception:
>>> >> >> > Failure
>>> >> >> >  "in article opentheory/articles/bool.art at line 89:
>>> >> >> > defineConst\nstack
>>> >> >> > =
>>> >> >> > [Term; \"Data.Bool.T\"; Thm]\nnew_constant: constant T has
>>> >> >> > already
>>> >> >> > been
>>> >> >> > declared".
>>> >> >> >
>>> >> >> >
>>> >> >> >
>>> >> >> > # let all= import_article "opentheory/articles/real.art";;
>>> >> >> > Exception:
>>> >> >> > Failure
>>> >> >> >  "in article opentheory/articles/real.art at line 283:
>>> >> >> > defineConst\nstack =
>>> >> >> > [Term; \"HOLLight.is_nadd\"; [[]; [[Var; Term]]]; [[]; [[Var;
>>> >> >> > Term]]];
>>> >> >> > [];
>>> >> >> > \"HOLLight.dest_nadd\"; \"HOLLight.mk_nadd\"; \"HOLLight.nadd\";
>>> >> >> > TypeOp<fun>; \"s\"; []; \"HOLLight.dest_hreal\";
>>> >> >> > \"HOLLight.mk_hreal\";
>>> >> >> > \"HOLLight.hreal\"; TypeOp<prod>; TypeOp<fun>; TypeOp<fun>;
>>> >> >> > Const<!>]\nnew_constant: constant is_nadd has already been
>>> >> >> > declared".
>>> >> >> >
>>> >> >> >
>>> >> >> > # let all= import_article "opentheory/articles/option.art";;
>>> >> >> > Exception:
>>> >> >> > Failure
>>> >> >> >  "in article opentheory/articles/option.art at line 478:
>>> >> >> > defineConst\nstack
>>> >> >> > = [Term; \"HOLLight.NUMSUM\"; Term; Term; Term; Var; Term; Var;
>>> >> >> > Term;
>>> >> >> > Var;
>>> >> >> > Term; Var; [[\"HOLLight.NUMLEFT\"; Var]]; Term; Var; Var; Var;
>>> >> >> > Var;
>>> >> >> > \"HOLLight.INJP\"; \"HOLLight.ZBOT\"; Term; Term; Term; Var;
>>> >> >> > Term;
>>> >> >> > Term;
>>> >> >> > Var; Term; Var; \"HOLLight.ZRECSPACE\"; [\"A\"];
>>> >> >> > \"HOLLight._dest_rec\";
>>> >> >> > \"HOLLight._mk_rec\"; \"HOLLight.recspace\"; Type; TypeOp<fun>;
>>> >> >> > \"_15483\";
>>> >> >> > Var; Var; \"HOLLight.CONSTR\"; Var; [\"A\"];
>>> >> >> > \"HOLLight._dest_option\";
>>> >> >> > \"HOLLight._mk_option\"; \"Data.Option.option\"; TypeOp<fun>;
>>> >> >> > \"is_none\";
>>> >> >> > \"Data.Option.isNone\"; Var; []; Thm]\nnew_constant: constant
>>> >> >> > NUMSUM
>>> >> >> > has
>>> >> >> > already been declared".
>>> >> >> >
>>> >> >> >
>>> >> >> >
>>> >> >> > So far I have only the three ones you showed in previous email
>>> >> >> > working.
>>> >> >> > :
>>> >> >> > "natural-divides.art", "stream.art" and "natural-prime.art"
>>> >> >> >
>>> >> >> > I wonder how I should load the rest.
>>> >> >> >
>>> >> >> > Thanks a lot.
>>> >> >> > --
>>> >> >> >
>>> >> >> > Regards,
>>> >> >> > Robert White (Shuai Wang)
>>> >> >> > INRIA Deducteam
>>> >> >> > [Moving to ILLC of UvA from this Sep. ]
>>> >> >> > [New email address will be shuai.wang at student.uva.nl]
>>> >> >> >
>>> >> >
>>> >> >
>>> >> >
>>> >> >
>>> >> > --
>>> >> >
>>> >> > Regards,
>>> >> > Robert White (Shuai Wang)
>>> >> > INRIA Deducteam
>>> >> > [Moving to ILLC of UvA from this Sep. ]
>>> >> > [New email address will be shuai.wang at student.uva.nl]
>>> >> >
>>> >
>>> >
>>> >
>>> >
>>> > --
>>> >
>>> > Regards,
>>> > Robert White (Shuai Wang)
>>> > INRIA Deducteam
>>> > [Moving to ILLC of UvA from this Sep. ]
>>> > [New email address will be shuai.wang at student.uva.nl]
>>> >
>>
>>
>>
>>
>> --
>>
>> Regards,
>> Robert White (Shuai Wang)
>> INRIA Deducteam
>> [Moving to ILLC of UvA from this Sep. ]
>> [New email address will be shuai.wang at student.uva.nl]
>>
>
>
>
> --
>
> Regards,
> Robert White (Shuai Wang)
> INRIA Deducteam
> [Moving to ILLC of UvA from this Sep. ]
> [New email address will be shuai.wang at student.uva.nl]
>