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