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

   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"
    "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!

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