Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Generic Lemma about Sums of Powers divided by ...


view this post on Zulip Email Gateway (Apr 28 2021 at 14:24):

From: Florian Märkl <isabelle-users@florianmaerkl.de>
Hello,

in my current project I have to reason about right bit shifts, among other things.
In particular I needed to prove the following (simplified) equalities:

X >> 1
= (x_0 * 2^0 + x_1 * 2^1 + x_2 * 2^2 + …) div 2
= x_1 * 2^0 + x_2 * 2^1 + …

where x_0, … are the individual bits of X. The first = is pretty much the definition already given in the word library, but the second turned out to be a bit trickier.
I formulated this problem of „integer-dividing a sum of powers by their base“ to get a representation without a division inside of it as more generic lemmas saying

(∑n∈A. b ^ f n) div b = (∑n∈Set.filter (λn. f n ≠ 0) A. b ^ (f n - 1))

with a few preconditions. I have attached the theory containing this in isolation.
Since it appears to be a little too generic to not already be formalized somewhere, I wonder if maybe this is either something that already exists in some form and I just have not found it yet or if it should be added to the AFP or distribution.
It kind of reminds me of polynomial division, only that here the base is a known constant rather than some variable x.

Cheers
Florian
PowerSum.thy


Last updated: Dec 08 2021 at 08:24 UTC