Converting a set to a list in Isabelle

isabelle

Solution

By searching for `"'a set" "'a list"` in the Find Constants tab of Isabelle/jEdit's Query panel I stumbled upon

sorted_list_of_set :: "'a set ⇒ 'a list"

from theory `List`. However, this constant requires `'a` to be in class `linorder`, i.e., it applies only to sets over linearly ordered elements. Moreover, as mentioned in my comment, it only works for finite sets. There is also a warning directly above the definition of `sorted_list_of_set` which I repeat here for completeness:

This function maps (finite) linearly ordered sets to sorted lists. Warning: in most cases it is not a good idea to convert from sets to lists but one should convert in the other direction (via @{const set}).

Problem

Original source