I'm trying to lead an inductive proof over a finite set, and I found the `Finite_Set.finite_induct`

lemma which seems to be what I want (though I may in future need to induct over the elements in a specified linear order, but not yet). But I can't figure out how to start the proof, other than just `proof (rule finite_induct)`

, but it feels like there should be a more idiomatic way of using it?

I assume that you just forgot to add the `finite S`

fact to the context:

```
using `finite S`
proof (induct rule: finite_induct)
```

Oh, yeap, that was it. Thanks!

Is there a way to fold over elements in a finite set (with `Finite_Set.fold`

or something similar) in a specified linear order? (And then that'll constrain the `finite_induct`

proof as well I assume..)

Though I guess at that point I might as well just use a list, but it'd be unhandy with the rest of my definitions & lemmas..

why would you want to do that?

Yeah good question, guess that's a bad idea then.

A set is by definitions unordered. If you need an order, then you don't have a set anymore…

IIRC, there is a `sorted_list_of_list`

or something like that to convert a set to an ordered list

Yeah there is `List.sorted_list_of_set :: 'a set => 'a list`

, but it takes no linear order as an argument, so I don't know how to call that..

`'a`

is assumed to have a linear order

Ah, hm, guess I'll finally have to dive into locales then

but why do you need an order? For non-determinism, I would use an inductive predicate

You can also always just "obtain" a list using the theorem `finite_list`

. If you need this top-level for whatever reason (i.e. outside an Isar proof), you can use `SOME`

in combination with that theorem (`SOME xs. set xs = A`

). None of this is executable, of course (while `sorted_list_of_set`

) ist.

I would, however, generally avoid working with lists instead of finite sets unless you have a good reason for doing so.

I am working with an existing framework which gives me a set of elected alternatives E, and for each alternative I want to do something. And the order in which I draw those candidates *may* affect the outcome, but I am not sure.

If you are not sure and don't care, use an inductive predicate to express a nondetirministic fold…

Oh sorry I had somehow missed your message yesterday.

`Library/Multiset_Permutations`

also has `permutations_of_set`

which gives you all the lists that are a permutation of a given finite set `A`

How would I use an inductive predicate to express some fold then? Right now I'm trying to define a `function`

which computes my result (pattern matching on `{}`

and `insert x xs`

), but to be honest I have no clue what I'm doing.

`finite`

is already an inductive predicate, so maybe that could be reused.

```
function draw :: "'a set ⇒ 'a list" where
"draw {} = []" |
"finite (insert x xs) ⟹ draw (insert x xs) = x # draw xs"
```

This is just a minimal example, something roughly like this is what I had in mind. (yes I know it's probably terribly wrong, please don't laugh :P)

that is the whole point of the discussion: this is not possible.

You cannot do that.

The definition is not well defined

What you can define is a fold-like predicate:

```
inductive fold_set :: ‹_ ⇒ 'b ⇒ 'a set ⇒ bool›
for f :: ‹'b ⇒ 'a ⇒ 'b›
where
"fold_set f dflt {}" |
"fold_set f a S ⟹ fold_set f (f a b) (insert b S)"
```

`dflt`

must be a meaningfull constant in you case or another parameter

This is available as `Finite_Set.fold_graph`

ah, I did not know about that predicate. Thanks

If your operation is commutative, i.e. the result doesn't depend on the order used (and you can prove it), then there's `Finite_Set.fold`

which uses `THE`

on `fold_graph`

I gave up on this last time, but the issue has come up again, and I'm at my wit's end to be honest. I have a set `A`

, and a subset `S`

of A. And I have a linear order `linord`

on A. How do I get `S`

transformed into a list according to the linear order? I know there is `List.sorted_list_of_set`

, but it uses Locales and I have no time to dig into that for something this (seemingly) simple, sorry..

Is the linear order on the type or or just the set `S`

?

Just on `A`

(and S is a subset).

can you use `SOME xs. set xs = A`

?

If it is on the set, then you are out of luck currently without resorting to `Types-To-Sets`

. I have already relativised the `folding`

locale to sets but the changes will be in the next release at the earliest.

I have something like that in the AFP: https://www.isa-afp.org/browser_info/current/AFP/Comparison_Sort_Lower_Bound/Linorder_Relations.html

`sorted_wrt_list_of_set`

It uses its own notation of "linear order", but that should be easy to adapt.

Looks like `linorder_on`

is equivalent to `linear_order_on`

Looks like what I need then! I never used AFP before, is there a canonical way of importing theories from AFP? It also seems to depend on List_Index which is AFP-only as well by the looks of it

The easiest way is to download the AFP, include it as a component (that's explained on the website) and then you can import it by writing `Comparison_Sort_Lower_Bound.Linorder_Relations`

.

You can also try just copying out whatever parts of the theory you need (no need to cite me or anything).

Last updated: Aug 10 2022 at 19:17 UTC