Re: [isabelle] Question about finite sets

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.

Jesus Aransay schrieb:
> 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

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.