Email Gateway (Aug 18 2022 at 12:37): Email Gateway (Aug 18 2022 at 12:37):From: Andreas Lochbihler <lochbihl@ipd.info.uni-karlsruhe.de>
Hi all,
I am looking for some way of defining a function recursively over finite
sets.
For a datatype t, the datatype package automatically generates a
recursion operator t_rec with which primitive-recursively functions over
that datatype can be defined. For finite sets, I haven't found
anything similar. The only thing I have found is the fold combinator in
Finite_Set of type "('a => 'a => 'a) => ('b => 'a) => 'a => 'b set =>
'a" where "fold f g z A" is f folded over the (multiset) image of A
under g with initial value z.
But I would rather like to have some function finite_rec :: "('b set =>
'b => 'a => 'a) => 'a => 'b set => 'a" that satisfies
"finite_rec f z {} = z" and
"[| finite A; ~ (x : A) |]
==> finite f z (insert x A) = f A x (finite_rec f A z)"
for all "well-formed" functions f.
Is there already something there that I can use like finite_rec or can
finite_rec be somehow defined using existing fold?
Best,
Andreas
Email Gateway (Aug 18 2022 at 12:37):From: Alexander Krauss <krauss@in.tum.de>
Hi Andreas,
Hmmm... How would you specify well-formed? It seems this is not easy...
As far as I know, Finite_Set.fold is all we have at the moment.
Alex
Email Gateway (Aug 18 2022 at 12:37):From: Tobias Nipkow <nipkow@in.tum.de>
If f does not take the remaining set A as an argument, then you can
define such a recursion operator completelty along the same lines as the
fold operator currently provided. It will require f to be
left-commutative: f a (f b c) = f b (f a c). See the TPHOLs 2005 paper
by Larry and me for more details. In fact, such an operator would be
welcome.
If the same development could be generalized to your f I am not sure.
Tobias
Andreas Lochbihler wrote:
Last updated: May 03 2024 at 04:19 UTC