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.

Your function f is then:

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






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