Email Gateway (Aug 18 2022 at 16:47): Email Gateway (Aug 18 2022 at 16:47):From: Jesus Aransay <jesus-maria.aransay@unirioja.es>
Dear all,
I was trying to define a (recursive) function over sets. One of the
premises in my setting is that sets are finite. The function should
behave as follows:
function remove :: "'b set => 'b set => 'b set"
where
remove_Nil: "remove A {} = A"
| remove_Cons: "remove A (insert x B) = (if _ then remove whatever B
else remove whatever' B)"
The function is decreasing in the size of the second argument (which
has a finite cardinal), but I do not know if there is some chance to
define "remove" by means of "fun", "function" or some other recursive
mechanism. What kind of induction rule is then obtained for that
recursive definition (something similar to finite.induct)?
Thanks in advance for any help,
Jesus
Email Gateway (Aug 18 2022 at 16:47):From: Tobias Nipkow <nipkow@in.tum.de>
You cannot define such a function with any of the recursive function
definition facilities because it would have to terminate for all sets,
not just the finite ones. Which it doesn't. The standard solution is
outlined in the TPHOLs 2005 paper by Larry and me. You find the
necessary combinators (fold and fold_image) in theory Finite_Set.
Thank you for your non-lexical email.
Tobias
Jesus Aransay schrieb:
Last updated: Apr 19 2024 at 12:27 UTC