# Re: [isabelle] promble of "add a number to every element of set"

```Hello Yucy,

```
you can change a set by applying a modifying function (like "add i") to every element using the image function from Set.thy.
```

definition f
where "f i A = (op + i) ` A"

You can then prove the lemmas
"f i {} = {}""
"f i (insert a A) = insert (i + a) (f i A)"
separately.

```
Recursion over sets is not easy at all, but there is the fold function in Finite_Set, which only works properly for finite sets.
```
Andreas

Yucy schrieb:
```
``` Hello,
In order to add a integer number "x" to every elements of a "int set A", I  don't find a direct operation about it in the file "HOL/Set.thy". Hence, I try to define a function which can excute this operation, but i don't known how to proof the completeness and termination of this function. My function is given as follow:
```
function f:: "int \<Rightarrow> int set \<Rightarrow> int set" where "f i {} = {}" |
```    "f i (insert a A) = {i+a}\<union>(f i A)"

Maybe there are some simple methods which can implement this operation, I need your help! thanks for your attention!
yucy
```
```

```

• References:

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.