## Stream: Beginner Questions

### Topic: Un-indexed sum of finite set of numbers

#### Chengsong Tan (May 23 2023 at 11:46):

Hi community,

I am looking for ways to represent functions (maps) on a finite domain and be able to count certain entries in that map easily.
Say I want to express a system which has two blocks which can be in different states. Such a system can be expressed by a function which we call `block_map`.

``````datatype BlockID = Block1 | Block2
datatype MESI_State = Modified| Exclusive| Shared| Invalid

type_synonym block_map = "BlockID ⇒ MESI_State"
``````

It is clear that `block_map` is defined on a finite domain.
Now if we define a function that count the number of blocks that are in a `Shared` state, it would look like the following:

``````fun count_sharers :: "block_map ⇒ nat"
where "count_sharers f = finite_sum ((λstate. case state of Shared ⇒ (1::nat) | _ ⇒ 0) ` (f ` (UNIV::BlockID set)))"
``````

It is not sure how the function `finite_sum` which sums all numbers in a finite set should be defined.
A search in the FiniteSet theory entry did not give anything useful.
An alternative is to define the datatype of a `BlockID` which takes a natural number parameter, and then doing an indexed sum over the blocks. The natural number parameter needs to be restricted to a finite subset of nat to make the sum finite:

``````datatype BlockIDSet2 = nat{.. < 2}
datatype BlockID2 = Block2 BlockIDSet2

type_synonym block_map2 = "BlockID2 ⇒ MESI_State"

fun count_sharers2 :: "block_map2 ⇒ nat"
where "count_sharers2 f = (∑i::nat=0..<2.  (λstate. case state of Shared ⇒ (1::nat) | _ ⇒ 0) (f (Block2 i))   )"
``````

Again I am not sure how to make this finite restriction on datatypes work for Isabelle.

A MWE code snippet:

``````theory mweFiniteSum imports
Main
begin

datatype BlockID = Block1 | Block2

datatype MESI_State = Modified| Exclusive| Shared| Invalid

type_synonym block_map = "BlockID ⇒ MESI_State"

fun count_sharers :: "block_map ⇒ nat"
where "count_sharers f = finite_sum ((λstate. case state of Shared ⇒ (1::nat) | _ ⇒ 0) ` (f ` (UNIV::BlockID set)))"

datatype BlockIDSet2 = nat{.. < 2}
datatype BlockID2 = Block2 BlockIDSet2

type_synonym block_map2 = "BlockID2 ⇒ MESI_State"

fun count_sharers2 :: "block_map2 ⇒ nat"
where "count_sharers2 f = (∑i::nat=0..<2.  (λstate. case state of Shared ⇒ (1::nat) | _ ⇒ 0) (f (Block2 i))   )"

end
``````

#### Kevin Kappelmann (May 24 2023 at 14:31):

Maybe `Finite_Set.fold`?

#### Mathias Fleury (May 24 2023 at 14:36):

Or summing over the set directly:

``````fun count_sharers :: "block_map ⇒ nat"
where "count_sharers f = (∑i ∈ (UNIV::BlockID set). if f i = Shared then 1 else 0)"
``````

#### Mathias Fleury (May 24 2023 at 14:38):

Remark that infinite sets are not really a problem, the sum just becomes empty

``````thm Groups_Big.comm_monoid_add_class.sum.infinite
infinite ?A ⟹ sum ?g ?A = 0
``````

#### Chengsong Tan (May 26 2023 at 10:24):

Mathias Fleury said:

Or summing over the set directly:

``````fun count_sharers :: "block_map ⇒ nat"
where "count_sharers f = (∑i ∈ (UNIV::BlockID set). if f i = Shared then 1 else 0)"
``````

Thank you! That works. I forgot to emphasise that I wanted to generate executable code. But this works perfectly regardless.

#### Chengsong Tan (May 26 2023 at 10:24):

Kevin Kappelmann said:

Maybe `Finite_Set.fold`?

Thank you for the pointer!

Last updated: Dec 07 2023 at 20:16 UTC