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
```

Thanks a lot in advance for your help!

Maybe `Finite_Set.fold`

?

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)"
```

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
```

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.

Kevin Kappelmann said:

Maybe

`Finite_Set.fold`

?

Thank you for the pointer!

Last updated: Dec 07 2023 at 20:16 UTC