Can I define an "inductive" function on finite sets?

Question

I am working with a finite set of elements and I need to define a recursive operation on them. Think something of the form

  "fx {} = []" 
| "fx (insert x X) = (if finite X then (if x ∈ X then fx X else x#(fx X)) else [])"
  apply blast
  apply simp
  apply simp
  apply simp

This is an oversimplification of my goal, however, if I am able to define fx in this specific way, the rest will flow better. I know there is another way to get from a set to a list, and please understand that's not what I am trying to do. In the end, I process the element x in a certain way, and add it (in a special way) to the processed set X.

Technically this definition should terminate, however I am unable to prove the last step of the termination (I cannot even fathom where to start).

Thus, I have 2 questions:

(1) is there a better way to define this kind of recursive function? my definition is always on finite sets and I can rewrite it like

function fx :: "'a fset ⇒ 'a list" where 
  "fx {||} =  []" 
| "fx (finsert x X) = (if x |∈| X then fx X else x#(fx X))"

I still end up with the last goal of termination being

 ⋀x X xa Xa.
       finsert x X = finsert xa Xa ⟹
       (if x |∈| X then fx_sumC X else x # fx_sumC X) =
       (if xa |∈| Xa then fx_sumC Xa else xa # fx_sumC Xa)

(2) Assuming this is the best way, how di I go about proving that last goal?

I have the nagging feeling that I am missing a crucial piece of information. However, after digging myself in and out of a lot of rabbit holes, I am at my wits ends. Any suggestions on how to approach this would be much appreciated.

P.S. Eventually, the recursive function above will be used to prove lemmas of the form "X ⊆ Y ⟶ fx x ∩ fx Y = fx (X∩Y)". Yes, I know that is incorrect with this current version of fx; fx will eventually become something of the form fx :: "'a fset ⇒ 'a set".

Answer 1

This is not going to work because that would not be a well-defined function. There is no "first" element of a set, so you cannot pattern match on insert. Generally, pattern matching only works for free constructors, i.e. families of injective functions with disjoint images, such as Nil and Cons on lists or 0 and Suc for nat.

For example, {1,2} = insert 1 (insert 2 {}) = insert 2 (insert 1 {}) = {2, 1}. So what should your function return here? [1,2] or [2,1]?

For functions where the order of traversal provably does not matter (e.g. taking the sum of all elements) you can use Finite_Set.fold, but it seems like in your case this is not so, so that doesn't work.

There are some options though:

1. It is easy to show that if A is a finite set then there exists a list xs such that distinct xs and set xs = A. See the theorem finite_distinct_list. This way, you can obtain such a list in a proof.

2. If your set has a linear order defined on it (i.e. its element type is of the sort linorder), there is a unique sorted list for that set. You can get this e.g. with the function sorted_list_of_set :: 'a :: linorder set ⇒ 'a list.

3. You can also more generally define a function that gives you a list that contains all the elements of a given finite set exactly once, e.g. like this:

    definition list_of_set :: "'a set ⇒ 'a list" where
      "list_of_set A = (if finite A then SOME xs. distinct xs ∧ set xs = A else [])"
    
    lemma list_of_set:
      assumes "finite A"
      shows   "set (list_of_set A) = A" "distinct (list_of_set A)"
    proof -
      from assms have "∃xs. set xs = A ∧ distinct xs"
        by (rule finite_distinct_list)
      from someI_ex[OF this] show "set (list_of_set A) = A" "distinct (list_of_set A)"
        using assms by (auto simp: list_of_set_def)
    qed

Or, a bit more directly, with the little-known specification command:

consts list_of_set :: "'a set ⇒ 'a list"

specification (list_of_set)
  list_of_set: "finite A ⟹ set (list_of_set A) = A ∧ distinct (list_of_set A)"
  using finite_distinct_list by metis+

Just note that the function thus defined will not be executable and there is no way to know what order the elements will be in. I.e. you will not be able to show e.g. list_of_set {1,2,3::nat} = [1, 2, 3]. Still having such a function may at times be convenient in proofs.

Which of these options works best depends on your specific use case, I suppose.