<div dir="ltr">So thanks a lot in advance.<div> </div><div>It would be nice to see all of them got included.</div><div> </div><div>Cheers</div><div>Robert</div></div><div class="gmail_extra"> <div class="gmail_quote">On 8 June 2015 at 20:46, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com" target="_blank">joe@gilith.com</a>> wrote: <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Robert, Your question on hol-info boils down to the following: is every theorem in the standard theory library included from <a href="http://basics.ml" target="_blank">basics.ml</a> to <a href="http://realax.ml" target="_blank">realax.ml</a>? And I think right now the answer is no, but I'll work on fixing that. Cheers, Joe On Mon, Jun 8, 2015 at 10:30 AM, Robert White <div class="HOEnZb"><div class="h5"><<a href="mailto:ai.robert.wangshuai@gmail.com">ai.robert.wangshuai@gmail.com</a>> wrote: > Hi Joe, > > Thanks. That's what I need for now. > > Regards, > Robert > > On 8 June 2015 at 19:12, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> wrote: >> >> Hi Robert, >> >> This is every theorem th from <a href="http://basics.ml" target="_blank">basics.ml</a> to <a href="http://realax.ml" target="_blank">realax.ml</a> 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 >> <<a href="mailto:ai.robert.wangshuai@gmail.com">ai.robert.wangshuai@gmail.com</a>> wrote: >> > Hello again. >> > >> > One more question: >> > >> > These are the thms exported as a result of loading <a href="http://hol.ml" target="_blank">hol.ml</a>? >> > >> > So am I right to say that these are the thms from <a href="http://basics.ml" target="_blank">basics.ml</a> to <a href="http://relax.ml" target="_blank">relax.ml</a> >> > (according to the order in <a href="http://hol.ml" target="_blank">hol.ml</a>)? >> > >> > Thanks. >> > >> > Regards, >> > Robert >> > >> > >> > On 8 June 2015 at 18:47, Robert White <<a href="mailto:ai.robert.wangshuai@gmail.com">ai.robert.wangshuai@gmail.com</a>> >> > 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 <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> wrote: >> >>> >> >>> Hi Robert, >> >>> >> >>> If you do a pull I've added a function that will list every exported >> >>> theorem, so you can do: >> >>> >> >>> #use "<a href="http://hol.ml" target="_blank">hol.ml</a>";; >> >>> 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 >> >>> <<a href="mailto:ai.robert.wangshuai@gmail.com">ai.robert.wangshuai@gmail.com</a>> 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 <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> 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 "<a href="http://hol.ml" target="_blank">hol.ml</a>";; >> >>> >> >> >>> >> It would be possible to reload articles from the standard theory >> >>> >> into >> >>> >> HOL Light with some changes to <a href="http://import.ml" target="_blank">import.ml</a>, 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 >> >>> >> <<a href="mailto:ai.robert.wangshuai@gmail.com">ai.robert.wangshuai@gmail.com</a>> 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 <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> 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: >> >>> >> >> >> >>> >> >> <a href="http://opentheory.gilith.com/packages/" target="_blank">http://opentheory.gilith.com/packages/</a> >> >>> >> >> >> >>> >> >> Cheers, >> >>> >> >> >> >>> >> >> Joe >> >>> >> >> >> >>> >> >> On Mon, Jun 8, 2015 at 4:34 AM, Robert White >> >>> >> >> <<a href="mailto:ai.robert.wangshuai@gmail.com">ai.robert.wangshuai@gmail.com</a>> wrote: >> >>> >> >> > Dear Joe, >> >>> >> >> > >> >>> >> >> > Hello. I have the following errors: >> >>> >> >> > >> >>> >> >> > # extend_the_interpretation >> >>> >> >> > "opentheory/theories/list/<a href="http://list.int" target="_blank">list.int</a>";; >> >>> >> >> > 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/<a href="http://bool.int" target="_blank">bool.int</a>";; >> >>> >> >> > Exception: >> >>> >> >> > Sys_error "opentheory/theories/bool/<a href="http://bool.int" target="_blank">bool.int</a>: No such file or >> >>> >> >> > directory". >> >>> >> >> > >> >>> >> >> > # extend_the_interpretation >> >>> >> >> > "opentheory/theories/bool/<a href="http://bool.int" target="_blank">bool.int</a>";; >> >>> >> >> > Exception: >> >>> >> >> > Sys_error "opentheory/theories/bool/<a href="http://bool.int" target="_blank">bool.int</a>: 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 <a href="mailto:shuai.wang@student.uva.nl">shuai.wang@student.uva.nl</a>] >> >>> >> >> > >> >>> >> > >> >>> >> > >> >>> >> > >> >>> >> > >> >>> >> > -- >> >>> >> > >> >>> >> > Regards, >> >>> >> > Robert White (Shuai Wang) >> >>> >> > INRIA Deducteam >> >>> >> > [Moving to ILLC of UvA from this Sep. ] >> >>> >> > [New email address will be <a href="mailto:shuai.wang@student.uva.nl">shuai.wang@student.uva.nl</a>] >> >>> >> > >> >>> > >> >>> > >> >>> > >> >>> > >> >>> > -- >> >>> > >> >>> > Regards, >> >>> > Robert White (Shuai Wang) >> >>> > INRIA Deducteam >> >>> > [Moving to ILLC of UvA from this Sep. ] >> >>> > [New email address will be <a href="mailto:shuai.wang@student.uva.nl">shuai.wang@student.uva.nl</a>] >> >>> > >> >> >> >> >> >> >> >> >> >> -- >> >> >> >> Regards, >> >> Robert White (Shuai Wang) >> >> INRIA Deducteam >> >> [Moving to ILLC of UvA from this Sep. ] >> >> [New email address will be <a href="mailto:shuai.wang@student.uva.nl">shuai.wang@student.uva.nl</a>] >> >> >> > >> > >> > >> > -- >> > >> > Regards, >> > Robert White (Shuai Wang) >> > INRIA Deducteam >> > [Moving to ILLC of UvA from this Sep. ] >> > [New email address will be <a href="mailto:shuai.wang@student.uva.nl">shuai.wang@student.uva.nl</a>] >> > > > > > > -- > > Regards, > Robert White (Shuai Wang) > INRIA Deducteam > [Moving to ILLC of UvA from this Sep. ] > [New email address will be <a href="mailto:shuai.wang@student.uva.nl">shuai.wang@student.uva.nl</a>] > </div></div></blockquote></div> <div> </div>-- <div class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div> </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> </div></div></div></div></div></div></div></div></div></div></div> </div>