1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
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 (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()
|
