<html><head><meta http-equiv="Content-Type" content="text/html charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;">Joe,<div><br></div><div><br><div><div>On 27 Mar 2014, at 18:04, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><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>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></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>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></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></div></div></div></blockquote><div><br></div></div>I didn’t have any to hand. The following are analogous to some of the theorems you have about pairs.</div><div><br></div><div>⊢ ∀ p⦁ (∀ x⦁ p x) ⇔ (∀ a⦁ p (InL a)) ∧ (∀ b⦁ p (InR b))<br>⊢ ∀ p⦁ (∀ a⦁ p a) ⇔ (∀ x⦁ p (OutL x))<br>⊢ ∀ p⦁ (∀ b⦁ p b) ⇔ (∀ x⦁ p (OutR x))</div><div><br></div><div>I can send you an article that proves these if you like (but the proofs are so easy, it is probably more trouble than it is worth).</div><div><br></div><div>I will have a think about how you might populate real-thm.</div><div><br></div><div>Regards,</div><div><br></div><div>Rob.</div></body></html>