opaque union Set<T>
fun rep<T>(S:Set<T>) {
switch S {
case char_fun(f) {
f
}
}
}
fun set_of_pred<T>(f:(fn T -> bool)) {
char_fun(f)
}
fun empty_set<T>() {
∅
}
fun single<V>(x:V) {
char_fun(fun y:V { x = y })
}
fun operator ∪<E>(P:Set<E>, Q:Set<E>) {
char_fun(fun x:E { (rep(P)(x) or rep(Q)(x)) })
}
fun operator ∩<T>(P:Set<T>, Q:Set<T>) {
char_fun(fun x:T { (rep(P)(x) and rep(Q)(x)) })
}
fun operator ∈<T>(x:T, S:Set<T>) {
rep(S)(x)
}
fun operator ⊆<T>(P:Set<T>, Q:Set<T>) {
(all x:T. (if x ∈ P then x ∈ Q))
}
single_member: (all T:type. (all x:T. x ∈ single(x)))
single_equal: (all T:type. (all x:T, y:T. (if y ∈ single(x) then x = y)))
single_equal_equal: (all T:type. (all x:T, y:T. (y ∈ single(x)) = (x = y)))
single_pred: (all T:type. (all x:T. set_of_pred(fun y:T { x = y }) = single(x)))
empty_no_members: (all T:type. (all x:T. not (x ∈ empty_set())))
rep_char_fun: (all T:type, f:(fn T -> bool). rep(char_fun(f)) = f)
rep_set_of_pred: (all T:type, f:(fn T -> bool). rep(set_of_pred(f)) = f)
set_of_pred_equal_fwd: (all T:type, f:(fn T -> bool), g:(fn T -> bool). (if set_of_pred(f) = set_of_pred(g) then f = g))
set_of_pred_equal_bkwd: (all T:type, f:(fn T -> bool), g:(fn T -> bool). (if f = g then set_of_pred(f) = set_of_pred(g)))
set_of_pred_equal: (all T:type, f:(fn T -> bool), g:(fn T -> bool). ((set_of_pred(f) = set_of_pred(g)) ⇔ (f = g)))
member_set_of_pred: (all T:type, x:T, f:(fn T -> bool). (if x ∈ set_of_pred(f) then f(x)))
union_set_of_pred: (all T:type, f:(fn T -> bool), g:(fn T -> bool). set_of_pred(f) ∪ set_of_pred(g) = set_of_pred(fun x { (f(x) or g(x)) }))
union_member: (all T:type. (all x:T, A:Set<T>, B:Set<T>. (if (x ∈ A or x ∈ B) then x ∈ A ∪ B)))
member_union: (all T:type. (all x:T, A:Set<T>, B:Set<T>. (if x ∈ A ∪ B then (x ∈ A or x ∈ B))))
member_union_equal: (all T:type. (all x:T, A:Set<T>, B:Set<T>. (x ∈ A ∪ B) = (x ∈ A or x ∈ B)))
union_empty: (all T:type. (all A:Set<T>. A ∪ empty_set() = A))
empty_union: (all T:type. (all A:Set<T>. @empty_set<T>() ∪ A = A))
union_sym: (all T:type. (all A:Set<T>, B:Set<T>. A ∪ B = B ∪ A))
union_assoc: (all T:type. (all A:Set<T>, B:Set<T>, C:Set<T>. (A ∪ B) ∪ C = A ∪ (B ∪ C)))
in_left_union: (all T:type. (all B:Set<T>. (all x:T, A:Set<T>. (if x ∈ A then x ∈ A ∪ B))))
in_right_union: (all T:type. (all A:Set<T>. (all x:T, B:Set<T>. (if x ∈ B then x ∈ A ∪ B))))
subset_equal: (all T:type. (all A:Set<T>, B:Set<T>. (if (A ⊆ B and B ⊆ A) then A = B)))
member_equal: (all T:type, A:Set<T>, B:Set<T>. (if (all x:T. ((x ∈ A) ⇔ (x ∈ B))) then A = B))