Re: [ProofPower] Proofpower Digest, Vol 119, Issue 1

[Rob Arthan]

David,

> On 1 Nov 2019, at 16:13, David Topham  wrote:
> 
> 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.

As an aside from what Roger has been trying to help with, you may also like to 
look at the treatment of sequences and series in the document wrk066.doc in the 
mathematical case studies that deals with some basic analysis. Sequences are 
modelled as functions ℕ → ℝ. The following function is defined to convert a 
sequence s into the series comprising the sequence of partial sums s_0 + s_1 + 
… + s_n.

ⓈHOLCONST
│ ⦏Sigma⦎ : (ℕ → ℝ) → (ℕ → ℝ)
├──
│   (∀s⦁ Sigma s 0 = ℕℝ 0)
│ ∧ (∀s n⦁ Sigma s (n+1) = Sigma s n + s n)
■

In a similar vein, a function that maps a sequence of coefficients to the 
corresponding power series is defined as follows:

ⓈHOLCONST
│ ⦏PowerSeries⦎ : (ℕ → ℝ) → (ℕ → ℝ → ℝ)
├──
│ ∀s n⦁ PowerSeries s n = PolyEval (s To n)
■

where s To n is the list comprising the first n elements of the sequence s and 
PolyEval maps a list of coefficients to the corresponding polynomial function:

ⓈHOLCONST
│ ⦏PolyEval⦎ : ℝ LIST → (ℝ → ℝ)
├──
│   (∀x⦁ PolyEval [] x = ℕℝ 0)
│∧  (∀c l x⦁ PolyEval (Cons c l) x = c + x * PolyEval l x)
■

When you are reasoning about these things, you can do induction over the index 
of a sequence, because that’s a natural number. The theory includes the usual 
results on geometric series:

:) geometric_sum_thm;
val it = ⊢ ∀ n x⦁ ¬ x = 1. ⇒ Sigma (휆 m⦁ x ^ m) (n + 1) = (1. - x ^ (n + 1)) / 
(1. - x): THM

:) geometric_series_thm;
val it = ⊢ ∀ x⦁ ~ 1. < x ∧ x < 1. ⇒ (휆 n⦁ PowerSeries (휆 m⦁ 1.) n x) -> 1. / 
(1. - x): THM

Regards,

Rob





___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] Proofpower Digest, Vol 119, Issue 1

[David Topham]

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  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 +
> From: Roger Bishop Jones 
> To: David Topham , proofpower@lemma-one.com
> Subject: Re: [ProofPower] (EXTERNAL) Re:  ProofPower and Discrete Math
> Message-ID: 
> 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