set.why 1.62 KB
Newer Older
1

2
theory Set
3
4
5
6
7
8
9

  type 'a t 

  logic mem('a, 'a t)

  logic empty : 'a t

10
11
12
  logic is_empty(s : 'a t) = forall x : 'a. not mem(x, s)

  axiom Empty_def1 : is_empty(empty : 'a t)
13
14
15
16
17
18
19

  logic add('a, 'a t) : 'a t

  axiom Add_def1 : 
    forall x, y : 'a. forall s : 'a t.
    mem(x, add(y, s)) <-> (x = y or mem(x, s))

20
21
22
23
24
25
  logic remove('a, 'a t) : 'a t

  axiom Remove_def1 :
    forall x, y : 'a. forall s : 'a t.
    mem(x, remove(y, s)) <-> (x <> y and mem(x, s))

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
  logic union('a t, 'a t) : 'a t

  axiom Union_def1 : 
    forall s1, s2 : 'a t. forall x : 'a.
    mem(x, union(s1, s2)) <-> (mem(x, s1) or mem(x, s2))

  logic inter('a t, 'a t) : 'a t

  axiom Inter_def1 : 
    forall s1, s2 : 'a t. forall x : 'a.
    mem(x, inter(s1, s2)) <-> (mem(x, s1) and mem(x, s2))

  logic diff('a t, 'a t) : 'a t

  axiom Diff_def1 : 
    forall s1, s2 : 'a t. forall x : 'a.
    mem(x, diff(s1, s2)) <-> (mem(x, s1) and not mem(x, s2))

  logic equal(s1 : 'a t, s2 : 'a t) = forall x : 'a. mem(x, s1) <-> mem(x, s2)

  logic subset(s1 : 'a t, s2 : 'a t) = forall x : 'a. mem(x, s1) -> mem(x, s2)

end

(* finite sets *)
theory Fset
  use import int.Int
53
  clone export Set
54
55
  
  logic cardinal('a t) : int
56
57
58

  axiom Cardinal_nonneg : forall s : 'a t. cardinal(s) >= 0

59
  axiom Cardinal_empty : cardinal(empty : 'a t) = 0
60
61
62
63
64
65
66
67
68
69
70
71

  axiom Cardinal_add : 
    forall x : 'a. forall s : 'a t. 
    not mem(x, s) -> cardinal(add(x, s)) = 1 + cardinal(s)

  axiom Cardinal_remove : 
    forall x : 'a. forall s : 'a t. 
    mem(x, s) -> cardinal(s) = 1 + cardinal(remove(x, s))

  axiom Cardinal_subset :
    forall s1, s2 : 'a t. subset(s1, s2) -> cardinal(s1) <= cardinal(s2)

72
73
end