*To*: Yucy <yucy0405 at 163.com>*Subject*: Re: [isabelle] promble of "add a number to every element of set"*From*: Andreas Lochbihler <lochbihl at ipd.info.uni-karlsruhe.de>*Date*: Thu, 30 Oct 2008 10:22:26 +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.17 (X11/20080925)

Hello Yucy,

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.

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

**References**:

- Previous by Date: [isabelle] interpretations and lambda terms
- Next by Date: Re: [isabelle] promble of "add a number to every element of set"
- Previous by Thread: [isabelle] promble of "add a number to every element of set"
- Next by Thread: Re: [isabelle] promble of "add a number to every element of set"
- 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