Theory Lem_set_extra

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                                  ››
― ‹‹****************************************************************************››

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

― ‹‹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