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







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