*To*: Yucy <yucy0405 at 163.com>*Subject*: Re: [isabelle] promble of "add a number to every element of set"*From*: Peter Lammich <peter.lammich at uni-muenster.de>*Date*: Thu, 30 Oct 2008 10:34:27 +0100*Cc*: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <33487971.259671225273272434.JavaMail.coremail@bj163app48.163.com>*References*: <33487971.259671225273272434.JavaMail.coremail@bj163app48.163.com>*User-agent*: Thunderbird 2.0.0.14 (X11/20080421)

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.

Regards, Peter

**References**:

- Previous by Date: Re: [isabelle] promble of "add a number to every element of set"
- Next by Date: [isabelle] [Deadline extension] MACIS 2008
- Previous by Thread: Re: [isabelle] promble of "add a number to every element of set"
- Next by Thread: [isabelle] Symposium on Automatic Program Verification - last call for papers
- Cl-isabelle-users October 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list