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

```Yucy wrote:
```
``` 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
```
```Try the image-function (syntax is _ ` _), defined in Set.thy.

e.g. try

"(op + 1) ` A" (equal to: "(%x. x+1) ` A" )

which is the set A, where every element gets added one to it.

```
Your approach might work for finite sets, but will definitely not for infinite sets.
```

Regards,
Peter

```

• References:

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