set.why

theory Set

  type set 'a

  (* membership *)
  predicate mem 'a (set 'a)

  (* 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 *)
  constant empty : set 'a

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

  axiom empty_def1: is_empty (empty : set 'a)

  (* addition *)
  function add 'a (set 'a) : set 'a

  axiom add_def1:
    forall x y: 'a. forall s: set 'a.
    mem x (add y s) <-> x = y \/ mem x s

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

  (* removal *)
  function remove 'a (set 'a) : set 'a

  axiom remove_def1:
    forall x y : 'a, s : set 'a.
    mem x (remove y s) <-> x <> y /\ mem x s

  lemma subset_remove:
    forall x: 'a, s: set 'a. subset (remove x s) s

  (* union *)
  function union (set 'a) (set 'a) : set 'a

  axiom union_def1:
    forall s1 s2: set 'a, x: 'a.
    mem x (union s1 s2) <-> mem x s1 \/ mem x s2

  (* intersection *)
  function inter (set 'a) (set 'a) : set 'a

  axiom inter_def1:
    forall s1 s2: set 'a, x: 'a.
    mem x (inter s1 s2) <-> mem x s1 /\ mem x s2

  (* difference *)
  function diff (set 'a) (set 'a) : set 'a

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

  lemma subset_diff:
    forall s1 s2: set 'a. subset (diff s1 s2) s1

  (* 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)

end

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

  function cardinal (set 'a) : int

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

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

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

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

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

end

(* 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

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

end

theory FsetExt

  use export Fset

  axiom ext: forall s1 s2 : set 'a.
    s1 = s2 <-> (forall x : 'a. mem x s1 <-> mem x s2)

end

theory SetMap
  use import map.Map
  use import bool.Bool

  type set 'a = map 'a bool

  predicate mem (x:'a) (s:set 'a) = s[x] = True

  constant empty : set 'a = const False

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

  goal Empty_def1 : is_empty(empty : set 'a)

  function add (x:'a) (s:set 'a) : set 'a = s[x <- True]

  function remove (x:'a) (s:set 'a) : set 'a =  s[x <- False]

  function union (set 'a) (set 'a) : set 'a

  axiom Union_def :
    forall s1 s2 : set 'a. forall x : 'a.
    (union s1 s2)[x] = orb s1[x] s2[x]

  function inter (set 'a) (set 'a) : set 'a

  axiom Inter_def :
    forall s1 s2 : set 'a. forall x : 'a.
    (inter s1 s2)[x] = andb s1[x] s2[x]

  function diff (set 'a) (set 'a) : set 'a

  axiom Diff_def1 :
    forall s1 s2 : set 'a. forall x : 'a.
    (diff s1 s2)[x] = andb s1[x] (notb s2[x])

  predicate equal(s1 s2 : set 'a) = forall x : 'a. s1[x] = s2[x]

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

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

  function complement (set 'a) : set 'a

  axiom Complement_def :
    forall s : set 'a. forall x : 'a.
    (complement s)[x] = notb s[x]

end


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