*To*: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*Subject*: [isabelle] promble of "add a number to every element of set"*From*: Yucy <yucy0405 at 163.com>*Date*: Wed, 29 Oct 2008 17:41:12 +0800 (CST)

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

**Follow-Ups**:**Re: [isabelle] promble of "add a number to every element of set"***From:*Andreas Lochbihler

**Re: [isabelle] promble of "add a number to every element of set"***From:*Peter Lammich

- Previous by Date: Re: [isabelle] promble with "Min_Un theorem"
- Next by Date: [isabelle] Symposium on Automatic Program Verification - last call for papers
- Previous by Thread: Re: [isabelle] promble with "Min_Un theorem"
- 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