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
119
120
121
|
chapter \<open>Generated by Lem from set_extra.lem.\<close>
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 \<Rightarrow> 'a set \<Rightarrow>('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 \<Rightarrow> 'a \<Rightarrow> ordering)\<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> ordering " where
" setCompareBy cmp ss ts = (
(let ss' = (ordered_list_of_set (\<lambda> x y . cmp x y = LT) ss) in
(let ts' = (ordered_list_of_set (\<lambda> 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 \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> 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
|
