Ok, I can work within integers for awhile! I was trying to use the general form of the geometric progression that may involve fractions, but I can explore whole numbers more first. I see the "induction_thm" won't work with R anyway since it has the base case as 0 and SML would expect 0.0 there for domain R (at least that is what I am seeing so far in trying to open_theory R and apply the thm).
I am trying wrk074 however open_theory "fincomb" fails so I need to find out how to load that as pre-requisite. On Fri, Nov 1, 2019 at 9:00 AM <proofpower-requ...@lemma-one.com> wrote: > Send Proofpower mailing list submissions to > proofpower@lemma-one.com > > To subscribe or unsubscribe via the World Wide Web, visit > http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com > or, via email, send a message with subject or body 'help' to > proofpower-requ...@lemma-one.com > > You can reach the person managing the list at > proofpower-ow...@lemma-one.com > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of Proofpower digest..." > > > Today's Topics: > > 1. Re: (EXTERNAL) Re: ProofPower and Discrete Math > (Roger Bishop Jones) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Thu, 31 Oct 2019 22:25:43 +0000 > From: Roger Bishop Jones <r...@rbjones.com> > To: David Topham <dtop...@ohlone.edu>, proofpower@lemma-one.com > Subject: Re: [ProofPower] (EXTERNAL) Re: ProofPower and Discrete Math > Message-ID: <e068cf45-46c0-f9f1-8aeb-fc5f64656...@rbjones.com> > Content-Type: text/plain; charset="utf-8"; Format="flowed" > > David, > > On 31/10/2019 19:14, David Topham wrote: > > Thank you Roger, that is very helpful.? I found I had to add this line > > to make it work: > > > > (open_theory "cs113" handle _ => (open_theory "hol"; new_theory > "cs113")); > > > > But then my next problem is to work on geometric progressions which > > require real numbers > > > > When I use R->R > > > > I get error message > > > > "type constructor or abbreviation for R not in scope." > > > > I wonder if hol is enough for using R? Or will I need to change or add > > to the ancestor theory I am inheriting from? > You could try the theory "?", which is not an ancestor of HOL. > You are making quite a big leap in complexity, going from arithmetic to > analysis, so things will get harder. > > You can have geometric progressions over the natural numbers, so if the > result you? are looking for actually works in that context, you might be > best to try it there first. > > If not you might benefit from working in one of the theories in > maths_egs, depending on how much analysis you need. > You would need to look at what is available (you can see the listings at > lemma-one.com if you want to check before installing maths_egs) and > decide what is the best context for your work. > see: http://www.lemma-one.com/ProofPower/examples/examples.html > > Even if you stick to the natural numbers, maths_egs has something for > you, the theory "numbers" in wrk074. > > Roger > > -------------- next part -------------- > An HTML attachment was scrubbed... > URL: < > http://lemma-one.com/pipermail/proofpower_lemma-one.com/attachments/20191031/826466b6/attachment-0001.html > > > > ------------------------------ > > Subject: Digest Footer > > _______________________________________________ > Proofpower mailing list > Proofpower@lemma-one.com > http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com > > > ------------------------------ > > End of Proofpower Digest, Vol 119, Issue 1 > ****************************************** >
_______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
