(*Generated by Lem from set_extra.lem.*)
open HolKernel Parse boolLib bossLib;
open lem_boolTheory lem_basic_classesTheory lem_maybeTheory lem_functionTheory lem_numTheory lem_listTheory lem_sortingTheory lem_setTheory;

val _ = numLib.prefer_num();



val _ = new_theory "lem_set_extra"

(******************************************************************************)
(* 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)*)
val _ = Define `
 ((chooseAndSplit:'a Ord_class -> 'a set ->('a set#'a#'a set)option)dict_Basic_classes_Ord_a s=
   (if s = EMPTY then
    NONE
  else
    let element1  = (CHOICE s) in
    let (lt, gt) = (lem_set$SET_SPLIT 
  dict_Basic_classes_Ord_a element1 s) in
      SOME (lt, element1, 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*)
val _ = Define `
 ((setCompareBy:('a -> 'a -> ordering) -> 'a set -> 'a set -> ordering) cmp ss ts=
   (let ss' = (ARB (\ x y .  cmp x y = LESS) ss) in
  let ts' = (ARB (\ x y .  cmp x y = LESS) ts) in
    lexicographic_compare cmp ss' ts'))`;


(*val setCompare : forall 'a. SetType 'a, Ord 'a => set 'a -> set 'a -> ordering*)
val _ = Define `
 ((setCompare:'a Ord_class -> 'a set -> 'a set -> ordering)dict_Basic_classes_Ord_a=  (setCompareBy  
  dict_Basic_classes_Ord_a.compare_method))`;


(* ----------------------------*)
(* unbounded fixed point       *)
(* --------------------------- *)

(* Is NOT supported by the coq backend! *)
(*val leastFixedPointUnbounded : forall 'a. SetType 'a => (set 'a -> set 'a) -> set 'a -> set 'a*)
 val leastFixedPointUnbounded_defn = Hol_defn "leastFixedPointUnbounded" `
 ((leastFixedPointUnbounded:('a set -> 'a set) -> 'a set -> 'a set) f x=
    (let fx = (f x) in
   if fx SUBSET x then x
   else leastFixedPointUnbounded f (fx UNION x)))`;

val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn leastFixedPointUnbounded_defn;
val _ = export_theory()