Hi everyone, I want to define and use a set of functions to map elements from set X to set Y but I got trouble about using it.

For example, we have two sets as follows:

```
definition X :: "nat set"
where "X = {1, 2}"
definition Y :: "nat set"
where "Y = {3, 4}"
```

`alpha`

is the function map an element of X to an element of Y and `alphaSet`

is the set of `alpha`

. For instance,

```
alphaSet = {(1,3), (2,4)} or {(1,4), (2,3)} or ...
If alphaSet = {(1,3), (2,4)} then
alpha 1 = 3
alpha 2 = 4
```

Thus, I defined `alpha`

and `alphaSet`

as follows:

```
definition alpha :: "nat ⇒ nat" where
"alpha x = (if x ∈ X then (SOME y. y ∈ Y) else 0)"
definition alphaSet :: "(nat ⇒ nat) set " where
"alphaSet = {f. (∀x ∈ X.(f x) ∈ Y)}"
```

My problem is that how can I generate the values of `alphaSet`

(i.e. how to get the set of function)? I tried

```
value "∀x ∈ X. alpha x". ------- error
lemma test1: "(x ∈ X) ∧ (alpha ∈ alphaSet) ⟹ ((alpha x) ∈ Y)"
```

but the result is `Failed to finish proof`

. Could anyone help me, please? Thank you very much.

value does not work for an obvious reason: It does not type. You are probably looking for `value "alpha ` X"`

, which does not work either, because of the SOME. There is no way Isabelle can evaluate this expression, it is not constructive.

About test1: I don't believe that it is out of the reach of someone who has done the Isabelle part of the Concrete Semantics.

(and the lemma is correct)

A constructive way for alpha can involve `sorted_list_of_set`

to convert a set to a list and build the mapping explicitly.

About test1: I don't believe that it is out of the reach of someone who has done the Isabelle part of the Concrete Semantics.

Yes, I've just done it. I forgot to unfold the definitions of X, Y, alpha, and alphaSet.

A constructive way for alpha can involve

`sorted_list_of_set`

to convert a set to a list and build the mapping explicitly.

Thank you for your suggestion. I'll try it.

The question is probably if you really need to have an explicit mapping. There should be a theorem somewhere that states that there is an injection between two sets of the same cardinality.

Mathias Fleury said:

The question is probably if you really need to have an explicit mapping. There should be a theorem somewhere that states that there is an injection between two sets of the same cardinality.

Yes, actually, I need that: for each `x ∈ X`

, create a set Y_x. For example,

```
X = {0, 1}
x ∈ X
x = 0: create Y_0 = {3,4,5}
x = 1: create Y_1 = {6,7}
```

Mathias Fleury said:

The question is probably if you really need to have an explicit mapping. There should be a theorem somewhere that states that there is an injection between two sets of the same cardinality.

Hi Mathias, I got a problem defining a set of functions. I defined `alphaSet`

(a set of `alpha`

function) as follows:

```
definition SyncExport :: "nat set" (* Export*)
where "SyncExport = {1, 2}"
definition SyncElemExport :: "nat set" (*element Export*)
where "SyncElemExport = {1, 2}"
definition TypeSync :: "nat set" (*port types*)
where "TypeSync = {1, 2}"
definition IncSync :: "nat set set" (*port instances of each port type TypeSync*)
where "IncSync = {{5,6}, {7,8,9}}"
definition mapin :: "nat ⇒ nat set" where (*mapin 1 = {5,6}; mapin 2 = {7,8,9}*)
"mapin pt = (if pt ∈ TypeSync then (SOME pIn. pIn ∈ IncSync) else {})"
definition alphaSet :: "(nat ⇒ nat) set " where (*set of functions alpha*)
"alphaSet = {f. ∀x∈TypeSync. (f x) ∈ (mapin x)}"
definition alpha :: "nat ⇒ nat" where (*alpha 1= 5 or alpha 1 = 6*)
"alpha pt = (if pt ∈ TypeSync then (SOME y. y ∈ (mapin pt)) else 0)"
```

Then, I test the cardinality of `TypeSync`

and `IncSync`

. They are equal.

```
value "card TypeSync"
value "card IncSync"
```

But when I want to show the value of the below predicate:

```
value "(∀t∈TypeSync.∀alp∈alphaSet.(P t (alp t)))"
```

It caused the error:

```
Wellsortedness error
(in code equation alphaSet ≡ {f. ∀x∈TypeSync. f x ∈ mapin x},
with dependency "Pure.dummy_pattern" -> "alphaSet"):
Type nat ⇒ nat not of sort enum
No type arity nat :: enum
```

As I understand, this error is from the infinite set but I defined `TypeSync`

and `IncSync`

are finite sets. Do you have any suggestions?

- This is
*not*an explicit construction (you cannot use SOME for that!) and`mapin`

cannot be calculated - The error message hints that
`alphaSet`

cannot be calculated. Without code setup, it requires enumerating constructing all functions`f`

and then filtering them.

In the `mapin`

, I want that from the `i element`

of set A, we take the corresponding element in the set B.

I read the `set`

library in Isabelle but they just provide operators `insert`

or `empty`

. Is there any chance to make an explicit mapping between two sets' elements?

By definition there is *no order* of elements of sets, but:

Mathias Fleury said:

A constructive way for alpha can involve

`sorted_list_of_set`

to convert a set to a list and build the mapping explicitly.

allows you to build a list containing the same elements (if the set is finite). Then there is an order on the elements.

Along that line (don't name the function `t`

in your development!):

```
fun t where
‹t (x # xs) (y # ys) = (t xs ys) (x := y)› |
‹t _ _ = (λx. 0)›
definition explicit_mapping :: ‹nat set ⇒ nat set ⇒ (nat ⇒ nat)› where
‹explicit_mapping xs ys = t (sorted_list_of_set xs) (sorted_list_of_set ys)›
value ‹explicit_mapping {1, 2, 3} {4, 5, 6}›
```

And here a completely random lemma:

```
lemma t_maps_to_existing:
‹length xs = length ys ⟹ x ∈ set xs ⟹ (t xs ys) x ∈ set ys›
by (induction xs ys rule: list_induct2) auto
(*why is that not in the library?*)
lemma length_sorted_list_of_set[simp]:
‹finite xs ⟹ length (sorted_list_of_set xs) = card xs›
by (metis distinct_card distinct_sorted_list_of_set set_sorted_list_of_set)
lemma
‹finite xs ⟹ finite ys ⟹ card xs = card ys ⟹ x ∈ xs ⟹ explicit_mapping xs ys x ∈ ys›
using t_maps_to_existing[of ‹sorted_list_of_set xs› ‹sorted_list_of_set ys› x]
by (auto simp: explicit_mapping_def)
```

But again: do you need to build the mapping explicitly or is it sufficient for you to show that one exists?

In the latter case, you can use the function `finite_same_card_bij`

.

Mathias Fleury said:

In the latter case, you can use the function

`finite_same_card_bij`

.

Thank you for your comment. This command

```
value ‹explicit_mapping {1, 2, 3} {4, 5, 6}›
```

returns

```
"_"
:: "nat ⇒ nat"
```

not

```
(1=>4), (2=>5), (3=>6)
```

I think the result should be the latter right?

In the latter case, you can use the function

`finite_same_card_bij`

.

You mean that I can use it when proving lemmas and theorems not defining the mapping, right? Besides, defining the mapping using `SOME`

is incorrect. I should change the definition, right?

I am convinced you can change the definitions to change `explicit_mapping`

from a function (like it is now) to whatever you want.

```
You mean that I can use it when proving lemmas and theorems not defining the mapping, right? Besides, defining the mapping using SOME is incorrect. I should change the definition, right?
```

No, using SOME means you cannot compute it, so `value`

cannot work. If you don't need the concrete mapping and don't need value, you can use some.

So, I keep my definition as follows:

```
definition PType :: "nat set" (*port types*)
where "PType = {1, 2}"
definition PIns :: "nat set set" (*port instances of each port type PType*)
where "PIns = {{5,6}, {7,8,9}}"
definition mapin :: "nat ⇒ nat set" where (*mapin 1 = {5,6}; mapin 2 = {7,8,9}*)
"mapin pt = (if pt ∈ PType then (SOME pIn. pIn ∈ PIns) else {})"
definition alphaSet :: "(nat ⇒ nat) set " where (*set of functions alpha*)
"alphaSet = {f. ∀x∈PType. (f x) ∈ (mapin x)}"
```

Then, I create a lemma using `finite_same_card_bij`

but it unprovable (it stayed in proving forever)

```
lemma test31: "(∀t∈PType.(∀alp∈alphaSet.(P t (alp t) ⟶ (∀l1∈(mapin t)-{alp t}.¬P t l1))))
⟹ (∀t∈PType.(∃alp∈alphaSet.∀l1∈(mapin t)-{alp t}. ¬P t l1))"
unfolding PType_def mapin_def PIns_def alpha_def alphaSet_def
using finite_same_card_bij
apply blast
done
```

In Math, it should be equal because

```
(P 2 7 ⟶ ¬P 2 8 ∧ ¬P 2 9) ∧ (P 2 8 ⟶ ¬P 2 7 ∧ ¬P 2 9) ∧ (P 2 9 ⟶ ¬P 2 8 ∧ ¬P 2 7)
⟷ (¬P 2 8 ∧ ¬P 2 9)∨(¬P 2 7 ∧ ¬P 2 9)∨(¬P 2 8 ∧ ¬P 2 7)
```

You misunderstand what `SOME`

means. It is an arbitrary choice. Unless that choice is unique, you _cannot say anything_ about its value. In particular `mapin 1 = {5, 6}`

might be true but might also be false.

You are in exactly one of those cases:

```
mapin 1 = {5, 6} and mapin 2 = {7, 8, 9}
or mapin 1 = {5, 6} and mapin 2 = {5, 6}
or mapin 1 = {7, 8, 9} and mapin 2 = {5, 6}
or mapin 1 = {7, 8, 9} and mapin 2 = {7, 8, 9}
```

YOU HAVE NO WAY TO KNOW WHICH OF THOSE CASES IS TRUE.

Last updated: Feb 27 2024 at 08:17 UTC