<div dir="ltr">Hi Rob,<div><br></div><div class="gmail_extra"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">
<div style="word-wrap:break-word"><div><div>Many thanks for that. I have now defined a set fold operation like the one in the repo and I can import the whole base package conservatively without any devious tricks in one go using the article file that your perl magic generates.</div>
</div></div></blockquote><div><br></div><div>That is excellent news.</div><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">
<div style="word-wrap:break-word"><div><div>I have just one outstanding concern: there are no theorems in the sum package and only one in the real package (and the only operators it uses are <= and sup. There don’t seem to be any uses of real or sum in the other packages in the repo, so I haven’t really been able to test that I have got the mappings right for these packages. Any suggestions would be welcome.</div>
</div></div></blockquote><div><br></div><div>Hmm... do you have any suggestions for theorems about sum types that I could prove in a sum-thm package to help here? Does ProofPower contain any such theorems?</div><div><br></div>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><div style="word-wrap:break-word"><div><div>I am trying with some success to load the other packages in the repo. In each case, I constructed an article for each package XYZ in the 35 package other than those included in the base package with the command:</div>
<div><br></div><div>   opentheory info —article -o XYZ.art XYZ.</div></div></div></blockquote><div><br></div><div>That looks like a good thing to do, although you might also want to know the theories that XYZ depends on, either by looking at the requires: meta-data in XYZ.thy or by using the command</div>
<div><br></div><div>opentheory info --requires XYZ<br></div><div><br></div><div>This will tell you the intended load-order of theories.</div><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">
<div style="word-wrap:break-word"><div><div>The package modular seems to expect a constant called Number.Modular.modulus to be defined, but nothing defines it, so modular won’t load. The package word seems to expect a constant called “Data.Word.width” but nothing defines it. byte will load, but the word10, word12 and word16 packages won’t, apparently because they are trying to redefine a constant called Number.Modular.equivalent.</div>
</div></div></blockquote><div><br></div><div>modular is an example of a parameterized theory, which expects its parameter symbols to be bound to symbols having the required properties. For each parameterized theory I have uploaded a witness theory that shows that these parameters can be satisfied, where the parameter symbols are defined in the witness theory. For example:</div>
<div><br></div><div>$ opentheory install modular-witness<br></div><div><div>installed package modular-witness-1.3</div><div>$ opentheory info --theory modular-witness</div><div>3 external type operators: -> bool natural</div>
<div>9 external constants: = ! /\ ==> ~ F T suc zero</div><div>8 satisfied assumptions: hidden</div><div>1 defined constant: modulus</div><div>1 theorem:</div><div>  |- ~(modulus = 0)</div></div><div><br></div><div>The parameter symbols show up as defined symbols in the witness theory (i.e., the constant modulus), and the required properties show up as theorems (i.e., modulus is non-zero).</div>
<div><br></div><div>word is another parameterized theory that instantiates modular, as can be seen in its theory source file:</div><div><br></div><div><a href="http://opentheory.gilith.com/opentheory/packages/word-def-1.64/word-def.thy">http://opentheory.gilith.com/opentheory/packages/word-def-1.64/word-def.thy</a><br>
</div><div><br></div><div>The concrete word theories (e.g., byte, word16, etc) then instantiate the word theory with different word sizes, for example:<br></div><div><br></div><div><a href="http://opentheory.gilith.com/opentheory/packages/byte-def-1.73/byte-def.thy">http://opentheory.gilith.com/opentheory/packages/byte-def-1.73/byte-def.thy</a><br>
</div><div><a href="http://opentheory.gilith.com/opentheory/packages/word16-def-1.73/word16-def.thy">http://opentheory.gilith.com/opentheory/packages/word16-def-1.73/word16-def.thy</a><br></div><div><br></div><div>The upshot is that you'll be able to read in these concrete theories just fine, but trying to read multiple of them will fail because they will define internal symbols carried over from modular and word (e.g., Number.Modular.equivalent) with the same name but different definitions. I'm not sure what to do about this, but let me continue this in the other thread about multiple definitions.</div>
<div><br></div><div>Cheers,</div><div><br></div><div>Joe</div><div><br></div></div></div></div>