#line 123 "/home/travis/build/felix-lang/felix/src/packages/algebra.fdoc"
// note: eq is not necessarily required for a membership test
// for example: string member of regexp doesn't require
// string equality
// Set need not be finite (example regexp again)
// A list is a set, despite the duplications
class Set[c,t] {
fun mem (elt:t, container:c):bool => elt $$\in$$ container;
virtual fun $$\in$$ : t * c-> bool;
fun $$\owns$$ (container:c, elt:t) => elt $$\in$$ container;
fun $$\ni$$ (container:c, elt:t) => elt $$\in$$ container;
fun $$\notin$$ (elt:t, container:c) => not (elt $$\in$$ container);

fun $$\cup$$[c2 with Set[c2,t]]
(x:c, y:c2) =>
{ e : t | e $$\in$$ x or e $$\in$$ y }
;

fun $$\cap$$[c2 with Set[c2,t]]
(x:c, y:c2) =>
{ e : t | e $$\in$$ x and e $$\in$$ y }
;

fun $$\setminus$$[c2 with Set[c2,t]]
(x:c, y:c2) =>
{ e : t | e $$\in$$ x and e $$\notin$$ y }
;
}

#line 176 "/home/travis/build/felix-lang/felix/src/packages/algebra.fdoc"
interface set_form[T] { has_elt: T -> bool; }

instance[T] Set[set_form[T], T] {
fun $$\in$$ (elt:T, s:set_form[T]) => s.has_elt elt;
}
open[T] Set[set_form[T],T];

// INVERSE image of a set under a function
// For a function f: t -> t2, an element e
// is in a restriction of the domain t if its
// image in t2 is in the specified set.
fun invimg[t,c2,t2 with Set[c2,t2]]
(f:t->t2, x:c2) : set_form[t] =>
{ e : t | (f e) $$\in$$ x }
;

#line 199 "/home/travis/build/felix-lang/felix/src/packages/algebra.fdoc"

fun $$\times$$[U,V] (x:set_form[U],y:set_form[V]) =>
{ u,v : U * V | u $$\in$$ x and v $$\in$$ y }
;

fun $$\otimes$$[U,V] (x:set_form[U],y:set_form[V]) =>
{ u,v : U * V | u $$\in$$ x and v $$\in$$ y }
;

fun $$\otimes$$[U,V,W] (head:set_form[U], tail:set_form[V*W]) =>
{ u,v,w : U * V * W | u $$\in$$ head and (v,w) $$\in$$ tail }
;

fun $$\otimes$$[NH,OH,OT] (head:set_form[NH], tail:set_form[OH**OT]) =>
{ h,,(oh,,ot) : NH ** (OH ** OT) | h $$\in$$ head and (oh,,ot) $$\in$$ tail }
;