Email Gateway (Aug 18 2022 at 12:34): Email Gateway (Aug 18 2022 at 12:34):From: Yucy <yucy0405@163.com>
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
Email Gateway (Aug 18 2022 at 12:35):From: Peter Lammich <peter.lammich@uni-muenster.de>
Yucy wrote:
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
Email Gateway (Aug 18 2022 at 12:35):From: Andreas Lochbihler <lochbihl@ipd.info.uni-karlsruhe.de>
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:
Last updated: May 03 2024 at 01:09 UTC