set.why 4.97 KB
Newer Older
1

2
theory Set
3

4
  type set 'a
5

6
  (* membership *)
Andrei Paskevich's avatar
Andrei Paskevich committed
7
  predicate mem 'a (set 'a)
8

9
10
11
12
13
14
15
16
17
18
19
20
21
  (* equality *)
  predicate (==) (s1 s2: set 'a) = forall x : 'a. mem x s1 <-> mem x s2

  axiom extensionality:
    forall s1 s2: set 'a. s1 == s2 -> s1 = s2

  (* inclusion *)
  predicate subset (s1 s2: set 'a) = forall x : 'a. mem x s1 -> mem x s2

  lemma subset_trans:
    forall s1 s2 s3: set 'a. subset s1 s2 -> subset s2 s3 -> subset s1 s3

  (* empty set *)
22
  constant empty : set 'a
23

24
  predicate is_empty (s: set 'a) = forall x: 'a. not (mem x s)
25

26
  axiom empty_def1: is_empty (empty : set 'a)
27

28
  (* addition *)
Andrei Paskevich's avatar
Andrei Paskevich committed
29
  function add 'a (set 'a) : set 'a
30

31
32
  axiom add_def1:
    forall x y: 'a. forall s: set 'a.
Andrei Paskevich's avatar
Andrei Paskevich committed
33
    mem x (add y s) <-> x = y \/ mem x s
34

35
36
37
  function singleton (x: 'a) : set 'a = add x empty

  (* removal *)
Andrei Paskevich's avatar
Andrei Paskevich committed
38
  function remove 'a (set 'a) : set 'a
39

40
41
  axiom remove_def1:
    forall x y : 'a, s : set 'a.
Andrei Paskevich's avatar
Andrei Paskevich committed
42
    mem x (remove y s) <-> x <> y /\ mem x s
43

44
45
46
47
  lemma subset_remove:
    forall x: 'a, s: set 'a. subset (remove x s) s

  (* union *)
Andrei Paskevich's avatar
Andrei Paskevich committed
48
  function union (set 'a) (set 'a) : set 'a
49

50
51
  axiom union_def1:
    forall s1 s2: set 'a, x: 'a.
Andrei Paskevich's avatar
Andrei Paskevich committed
52
    mem x (union s1 s2) <-> mem x s1 \/ mem x s2
53

54
  (* intersection *)
Andrei Paskevich's avatar
Andrei Paskevich committed
55
  function inter (set 'a) (set 'a) : set 'a
56

57
58
  axiom inter_def1:
    forall s1 s2: set 'a, x: 'a.
Andrei Paskevich's avatar
Andrei Paskevich committed
59
    mem x (inter s1 s2) <-> mem x s1 /\ mem x s2
60

61
  (* difference *)
Andrei Paskevich's avatar
Andrei Paskevich committed
62
  function diff (set 'a) (set 'a) : set 'a
63

64
65
66
  axiom diff_def1:
    forall s1 s2: set 'a, x: 'a.
    mem x (diff s1 s2) <-> mem x s1 /\ not (mem x s2)
67

68
69
  lemma subset_diff:
    forall s1 s2: set 'a. subset (diff s1 s2) s1
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
  (* the set of all x of type 'a *)
  constant all: set 'a

  axiom all_def: forall x: 'a. mem x all

end

theory SetComprehension

  use export Set
  use HighOrd as HO

  (* { x | p x } *)
  function comprehension (p: HO.pred 'a) : set 'a

  axiom comprehension_def:
    forall p: HO.pred 'a.
    forall x: 'a. mem x (comprehension p) <-> p x

  (* { x | x in U and p(x) *)
  function filter (p: HO.pred 'a) (u: set 'a) : set 'a =
    comprehension (\ x: 'a. p x /\ mem x u)

  (* { f x | x in U } *)
  function map (f: HO.func 'a 'b) (u: set 'a) : set 'b =
    comprehension (\ y: 'b. exists x: 'a. mem x u /\ y = f x)

  lemma map_def:
    forall f: HO.func 'a 'b, u: set 'a.
    forall x: 'a. mem x u -> mem (f x) (map f u)

102
103
104
105
106
end

(* finite sets *)
theory Fset
  use import int.Int
107
  clone export Set
108

Andrei Paskevich's avatar
Andrei Paskevich committed
109
  function cardinal (set 'a) : int
110

111
  axiom cardinal_nonneg: forall s: set 'a. cardinal s >= 0
112

113
114
  axiom cardinal_empty:
    forall s: set 'a. cardinal s = 0 <-> is_empty s
115

116
  axiom cardinal_add:
117
    forall x : 'a. forall s : set 'a.
118
    not (mem x s) -> cardinal (add x s) = 1 + cardinal s
119

120
  axiom cardinal_remove:
121
    forall x : 'a. forall s : set 'a.
122
    mem x s -> cardinal s = 1 + cardinal (remove x s)
123

124
  axiom cardinal_subset:
125
    forall s1 s2 : set 'a. subset s1 s2 -> cardinal s1 <= cardinal s2
126

127
128
end

129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
(* finite sets of integers *)
theory Fsetint

  use export int.Int
  use export Fset

  function min_elt (set int) : int

  axiom min_elt_def1:
    forall s: set int. not (is_empty s) -> mem (min_elt s) s
  axiom min_elt_def2:
    forall s: set int. not (is_empty s) ->
    forall x: int. mem x s -> min_elt s <= x

  function max_elt (set int) : int

  axiom max_elt_def1:
    forall s: set int. not (is_empty s) -> mem (max_elt s) s
  axiom max_elt_def2:
    forall s: set int. not (is_empty s) ->
    forall x: int. mem x s -> x <= max_elt s

  (* the set {0,1,...,n-1} *)
  function below int : set int

  axiom below_def: forall x n: int. mem x (below n) <-> 0 <= x < n

156
157
158
  lemma cardinal_below:
    forall n: int. cardinal (below n) = if n >= 0 then n else 0

159
160
end

MARCHE Claude's avatar
MARCHE Claude committed
161
theory FsetExt
162

MARCHE Claude's avatar
MARCHE Claude committed
163
164
  use export Fset

165
  axiom ext: forall s1 s2 : set 'a.
MARCHE Claude's avatar
MARCHE Claude committed
166
167
168
169
    s1 = s2 <-> (forall x : 'a. mem x s1 <-> mem x s2)

end

170
171
theory SetMap
  use import map.Map
François Bobot's avatar
François Bobot committed
172
173
  use import bool.Bool

174
  type set 'a = map 'a bool
François Bobot's avatar
François Bobot committed
175

Andrei Paskevich's avatar
Andrei Paskevich committed
176
  predicate mem (x:'a) (s:set 'a) = s[x] = True
François Bobot's avatar
François Bobot committed
177

178
  constant empty : set 'a = const False
François Bobot's avatar
François Bobot committed
179

180
  predicate is_empty (s : set 'a) = forall x : 'a. not (mem x s)
François Bobot's avatar
François Bobot committed
181

182
  goal Empty_def1 : is_empty(empty : set 'a)
François Bobot's avatar
François Bobot committed
183

Andrei Paskevich's avatar
Andrei Paskevich committed
184
  function add (x:'a) (s:set 'a) : set 'a = s[x <- True]
François Bobot's avatar
François Bobot committed
185

Andrei Paskevich's avatar
Andrei Paskevich committed
186
  function remove (x:'a) (s:set 'a) : set 'a =  s[x <- False]
François Bobot's avatar
François Bobot committed
187

Andrei Paskevich's avatar
Andrei Paskevich committed
188
  function union (set 'a) (set 'a) : set 'a
François Bobot's avatar
François Bobot committed
189
190

  axiom Union_def :
191
192
    forall s1 s2 : set 'a. forall x : 'a.
    (union s1 s2)[x] = orb s1[x] s2[x]
François Bobot's avatar
François Bobot committed
193

Andrei Paskevich's avatar
Andrei Paskevich committed
194
  function inter (set 'a) (set 'a) : set 'a
François Bobot's avatar
François Bobot committed
195
196

  axiom Inter_def :
197
198
    forall s1 s2 : set 'a. forall x : 'a.
    (inter s1 s2)[x] = andb s1[x] s2[x]
François Bobot's avatar
François Bobot committed
199

Andrei Paskevich's avatar
Andrei Paskevich committed
200
  function diff (set 'a) (set 'a) : set 'a
François Bobot's avatar
François Bobot committed
201
202

  axiom Diff_def1 :
203
    forall s1 s2 : set 'a. forall x : 'a.
204
    (diff s1 s2)[x] = andb s1[x] (notb s2[x])
François Bobot's avatar
François Bobot committed
205

Andrei Paskevich's avatar
Andrei Paskevich committed
206
  predicate equal(s1 s2 : set 'a) = forall x : 'a. s1[x] = s2[x]
François Bobot's avatar
François Bobot committed
207

208
  axiom Equal_is_eq : forall s1 s2 : set 'a. equal s1 s2 -> s1 = s2
François Bobot's avatar
François Bobot committed
209

Andrei Paskevich's avatar
Andrei Paskevich committed
210
  predicate subset(s1 s2 : set 'a) = forall x : 'a. mem x s1 -> mem x s2
François Bobot's avatar
François Bobot committed
211

Andrei Paskevich's avatar
Andrei Paskevich committed
212
  function complement (set 'a) : set 'a
François Bobot's avatar
François Bobot committed
213
214

  axiom Complement_def :
215
216
    forall s : set 'a. forall x : 'a.
    (complement s)[x] = notb s[x]
François Bobot's avatar
François Bobot committed
217

218
219
220
221
end


(*
222
Local Variables:
223
compile-command: "make -C .. theories/set"
224
End:
225
*)