[opentheory-users] Error in importing

[Joe Leslie-Hurd]

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