# Theory Lem_set_extra

theory Lem_set_extra
imports Lem_sorting Lem_set
```chapter ‹Generated by Lem from ‹set_extra.lem›.›

theory "Lem_set_extra"

imports
Main
"Lem_bool"
"Lem_basic_classes"
"Lem_maybe"
"Lem_function"
"Lem_num"
"Lem_list"
"Lem_sorting"
"Lem_set"

begin

― ‹‹****************************************************************************››
― ‹‹ A library for sets                                                         ››
― ‹‹                                                                            ››
― ‹‹ It mainly follows the Haskell Set-library                                  ››
― ‹‹****************************************************************************››

― ‹‹ ========================================================================== ››
― ‹‹ ========================================================================== ››

― ‹‹open import Bool Basic_classes Maybe Function Num List Sorting Set››

― ‹‹ ----------------------------››
― ‹‹ set choose (be careful !)   ››
― ‹‹ --------------------------- ››

― ‹‹val choose : forall 'a. SetType 'a => set 'a -> 'a››

― ‹‹ ------------------------ ››
― ‹‹ chooseAndSplit           ››
― ‹‹ ------------------------ ››
― ‹‹ The idea here is to provide a simple primitive that Lem code can use
* to perform its own custom searches within the set -- likely using a
* search criterion related to the element ordering, but not necessarily).
* For example, sometimes we don't necessarily want to search for a specific
* element, but want to search for elements greater than or less than some other.
* Someties we'd like to use "split" but don't know a good value to "split" at.
* This function lets the set implementation decide that value.
*
* The contract of chooseAndSplit is simply to select an element nondeterministically
* and return that element, together with the subsets of elements less than and
* greater than it. In this way, we can recursively traverse the set with any
* search criterion, and we avoid baking in the tree representation (although that
* is the obvious choice).
››
― ‹‹val chooseAndSplit : forall 'a. SetType 'a, Ord 'a => set 'a -> maybe (set 'a * 'a * set 'a)››
definition chooseAndSplit  :: " 'a Ord_class ⇒ 'a set ⇒('a set*'a*'a set)option "  where
" chooseAndSplit dict_Basic_classes_Ord_a s = (
if s = {} then
None
else
(let element  = (set_choose s) in
(let (lt, gt) = (Lem_set.split
dict_Basic_classes_Ord_a element s) in
Some (lt, element, gt))))"

― ‹‹ ----------------------------››
― ‹‹ universal set               ››
― ‹‹ --------------------------- ››

― ‹‹val universal : forall 'a. SetType 'a => set 'a››

― ‹‹ ----------------------------››
― ‹‹ toList                      ››
― ‹‹ --------------------------- ››

― ‹‹val toList        : forall 'a. SetType 'a => set 'a -> list 'a››

― ‹‹ ----------------------------››
― ‹‹ toOrderedList               ››
― ‹‹ --------------------------- ››

― ‹‹ "toOrderedList" returns a sorted list. Therefore the result is (given a suitable order) deterministic.
Therefore, it is much preferred to "toList". However, it still is only defined for finite sets. So, please
use carefully and consider using set-operations instead of translating sets to lists, performing list manipulations
and then transforming back to sets. ››

― ‹‹val toOrderedListBy : forall 'a. ('a -> 'a -> bool) -> set 'a -> list 'a››

― ‹‹val toOrderedList : forall 'a. SetType 'a, Ord 'a => set 'a -> list 'a››

― ‹‹ ----------------------- ››
― ‹‹ compare                 ››
― ‹‹ ----------------------- ››

― ‹‹val setCompareBy: forall 'a. ('a -> 'a -> ordering) -> set 'a -> set 'a -> ordering››
definition setCompareBy  :: "('a ⇒ 'a ⇒ ordering)⇒ 'a set ⇒ 'a set ⇒ ordering "  where
" setCompareBy cmp ss ts = (
(let ss' = (ordered_list_of_set (λ x y .  cmp x y = LT) ss) in
(let ts' = (ordered_list_of_set (λ x y .  cmp x y = LT) ts) in
lexicographicCompareBy cmp ss' ts')))"

― ‹‹val setCompare : forall 'a. SetType 'a, Ord 'a => set 'a -> set 'a -> ordering››
definition setCompare  :: " 'a Ord_class ⇒ 'a set ⇒ 'a set ⇒ ordering "  where
" setCompare dict_Basic_classes_Ord_a = ( setCompareBy
(compare_method   dict_Basic_classes_Ord_a) )"

― ‹‹ ----------------------------››
― ‹‹ unbounded fixed point       ››
― ‹‹ --------------------------- ››

― ‹‹ Is NOT supported by the coq backend! ››
― ‹‹val leastFixedPointUnbounded : forall 'a. SetType 'a => (set 'a -> set 'a) -> set 'a -> set 'a››
― ‹‹let rec leastFixedPointUnbounded f x=
let fx = f x in
if fx subset x then x
else leastFixedPointUnbounded f (fx union x)››
end
```