/
sets.thy
119 lines (89 loc) · 2.75 KB
/
sets.thy
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
Definition Space :=
thy
Parameter s : Set.
end.
(* ***** Lists ***** *)
Definition List(S : Space) :=
thy
Parameter s : Set.
Parameter nil : s.
Parameter cons : S.s -> s -> s.
(* Induction principle for ts gives us "fold". *)
Axiom induction:
forall M : thy Parameter p : s -> Prop. end,
M.p nil ->
(forall x : S.s, forall lst : s, (M.p lst -> M.p (cons x lst))) ->
(forall lst : s, M.p lst).
end.
Parameter ListMaker : [S : Space] -> List S.
Definition Hyperspace(S : Space) :=
thy
Parameter s : Set.
Parameter elm : S.s -> s -> Prop.
Definition carrier (u : s) := {x : S.s | elm x u}.
end.
(* ***** Finite sets ***** *)
Definition Finite(S : Space) :=
thy
include Hyperspace(S).
Parameter emptySet : s.
Parameter add : S.s -> s -> s.
Axiom elm_emptySet:
forall x : S.s, not (elm x emptySet).
Axiom elm_add:
forall x : S.s, forall u : s,
(elm x u <-> u = add x u).
Axiom add_idempotent:
forall x : S.s, forall u : s, add x (add x u) = add x u.
Axiom add_commutative:
forall x y : S.s, forall u : s, add x (add y u) = add y (add x u).
Axiom induction:
forall M : thy Parameter p : s -> Prop. end,
M.p emptySet ->
(forall x : S.s, forall u : s, (M.p u -> M.p (add x u))) ->
(forall u : s, M.p u).
end.
(* ***** Multisets ***** *)
Require Number.
Definition Multi (I : Number.Integer) (S : Space) :=
thy
Parameter s : Set.
Parameter count : S.s -> s -> I.integer.
Definition carrier (u : s) := {p : S.s * I.integer | count (p.0) u = p.1}.
Parameter emptySet : s.
Parameter add : S.s -> s -> s.
Axiom count_emptySet:
forall x : S.s, count x emptySet = I.zero.
Axiom count_add:
forall x : S.s, forall u : s,
count x (add x u) = I.add1 (count x u).
Axiom add_commutative:
forall x y : S.s, forall u : s, add x (add y u) = add y (add x u).
Axiom induction:
forall M : thy Parameter p : s -> Prop. end,
M.p emptySet ->
(forall x : S.s, forall u : s, (M.p u -> M.p (add x u))) ->
(forall u : s, M.p u).
end.
(* ***** Countable sets ***** *)
Definition Countable :=
fun (I : Number.Integer) =>
fun (S : Space) =>
thy
include Hyperspace(S).
Parameter emptySet : s.
Parameter add : S.s -> s -> s.
Axiom emptySet_empty:
forall x : S.s, not (elm x emptySet).
Axiom elm_add:
forall x : S.s, forall u : s, (elm x u <-> u = add x u).
Axiom add_idempotent:
forall x : S.s, forall u : s,
add x (add x u) = add x u.
Axiom add_commutative:
forall x y : S.s, forall u : s,
add x (add y u) = add y (add x u).
Axiom countable:
forall u : s, exists e : I.nat -> [`skip] + [`enum : S.s],
forall x : carrier u, exists n : I.nat, `enum (x :< S.s) = e n.
end.