Merge branch 'sail2' into mappings

1 files changed, 118 insertions, 0 deletions

diff --git a/snapshots/hol4/lem/hol-lib/lem_set_extraScript.sml b/snapshots/hol4/lem/hol-lib/lem_set_extraScript.sml
new file mode 100644
index 00000000..5409a408
--- /dev/null
+++ b/snapshots/hol4/lem/hol-lib/lem_set_extraScript.sml
@@ -0,0 +1,118 @@
+(*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.maybe (set 'a * 'a * set 'a)*)
+val _ = Define `
+ ((chooseAndSplit:'a lem_basic_classes$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 -> Basic_classes.ordering) -> set 'a -> set 'a -> Basic_classes.ordering*)
+val _ = Define `
+ ((setCompareBy:('a -> 'a -> lem_basic_classes$ordering) -> 'a set -> 'a set -> lem_basic_classes$ordering) cmp ss ts=  
+ (let ss' = (ARB (\ x y .  cmp x y = LT) ss) in
+  let ts' = (ARB (\ x y .  cmp x y = LT) ts) in
+    lexicographic_compare cmp ss' ts'))`;
+
+
+(*val setCompare : forall 'a. SetType 'a, Ord 'a => set 'a -> set 'a -> Basic_classes.ordering*)
+val _ = Define `
+ ((setCompare:'a lem_basic_classes$Ord_class -> 'a set -> 'a set -> lem_basic_classes$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()
+