NSet = FOL +

types
    i
  set = i


arities 

    i::term


consts

  "0"     :: i                 ("0")
  "1"     :: i                 ("1")
  "{}"    :: set               ("{}")
  insert  :: [i, set] => set
  "op :"  :: [i, set] => o     ("(_/ : _)" [50, 51] 50)
  "<="    :: [set, set] => o   (infixl 50)
  Collect :: [i => o] => set
  
  INTER,
  UNION   :: [set, i => set] => set
  Minus   :: [set, set] => set (infixl 65)
  Int     :: [set, set] => set (infixl 70)
  Un      :: [set, set] => set (infixl 65)
  Compl   :: set => set
  Pow     :: set => set
  UNIV    :: set

  Ball,
  Bex     :: [set, i => o] => o


syntax

  "op :"     :: [i,set] => o                ("op :")
  "op ~:"    :: [i,set] => o                ("(_/ ~: _)" [50, 51] 50)
  "op ~:"    :: [i,set] => o                ("op ~:")
  "@Collect" :: [pttrn, o] => set           ("(1{_./ _})")
  "@Finset"  :: args => set                 ("{(_)}") 
  "@INTER"   :: [pttrn, set, set] => set    ("(3INT _:_./ _)" 10)
  "@UNION"   :: [pttrn, set, set] => set    ("(3UN _:_./ _)" 10)
  "*Ball"    :: [pttrn, set, o] => o        ("(3ALL _:_./ _)" [0, 0, 10] 10)
  "*Bex"     :: [pttrn, set, o] => o        ("(3EX _:_./ _)" [0, 0, 10] 10)


translations		

  "UNIV"        == "Compl({})"
  "x ~: y"      == "~ (x : y)"
  "{x, xs}"     == "insert(x, {xs})"
  "{x}"         == "insert(x, {})"  
  "{x. P}"       == "Collect(%x. P)"
  "INT x:A. B"  == "INTER(A, (%x. B))"
  "UN x:A. B"   == "UNION(A, (%x. B))"
  "ALL x:A. P"  == "Ball(A, (%x. P))"
  "EX x:A. P"   == "Bex(A, (%x. P))"


rules

  ext       "A = B <-> (ALL x. x:A <-> x:B)"
  Collect   "(t : { x. P(x) }) <-> (P(t))"

syntax ("" output)
  "_setle"      :: [set, set] => o           ("op <=")
  "_setle"      :: [set, set] => o           ("(_/ <= _)" [50, 51] 50)
  "_setless"    :: [set, set] => o           ("op <")
  "_setless"    :: [set, set] => o           ("(_/ < _)" [50, 51] 50)

syntax (symbols)
  "_setle"      :: [set, set] => o           ("op \\<subseteq>")
  "_setle"      :: [set, set] => o           ("(_/ \\<subseteq> _)" [50, 51] 50)
  "_setless"    :: [set, set] => o           ("op \\<subset>")
  "_setless"    :: [set, set] => o           ("(_/ \\<subset> _)" [50, 51] 50)
  "op Int"      :: [set, set] => set         (infixl "\\<inter>" 70)
  "op Un"       :: [set, set] => set         (infixl "\\<union>" 65)
  "op :"        :: ['a, set] => o               ("op \\<in>")
  "op :"        :: ['a, set] => o               ("(_/ \\<in> _)" [50, 51] 50)
  "op ~:"       :: ['a, set] => o               ("op \\<notin>")
  "op ~:"       :: ['a, set] => o               ("(_/ \\<notin> _)" [50, 51] 50)
  "UN "         :: [idts, o] => o               ("(3\\<Union> _./ _)" 10)
  "INT "        :: [idts, o] => o               ("(3\\<Inter> _./ _)" 10)
  "@UNION1"     :: [pttrn, set] => set          ("(3\\<Union> _./ _)" 10)
  "@INTER1"     :: [pttrn, set] => set          ("(3\\<Inter> _./ _)" 10)
  "@UNION"      :: [pttrn, set, set] => set  ("(3\\<Union> _\\<in>_./ _)" 10)
  "@INTER"      :: [pttrn, set, set] => set  ("(3\\<Inter> _\\<in>_./ _)" 10)
  "_Ball"       :: [pttrn, set, o] => o      ("(3\\<forall> _\\<in>_./ _)" [0, 0, 10] 10)
  "_Bex"        :: [pttrn, set, o] => o      ("(3\\<exists> _\\<in>_./ _)" [0, 0, 10] 10)

translations
  "op \\<subseteq>" => "op <= :: [_ set, _ set] => o"
(*  "op \\<subset>" => "op <  :: [_ set, _ set] => o"*)


defs

  subset_def "A <= B        == ALL x. x:A --> x:B"
  empty_def  "{}            == {x. False}"
  Minus_def  "A Minus B     == {x. x : A & x ~: B}"
  Un_def     "A Un B        == {x. x : A | x : B}"
  Int_def    "A Int B       == {x. x : A & x : B}"
  Ball_def   "Ball(A, P)    == (ALL x. x:A --> P(x))"
  Bex_def    "Bex(A, P)     == (EX x. x:A & P(x))"
  Compl_def  "Compl(A)      == {x. ~x:A}"
  INTER_def  "INTER(A, B)   == {y. ALL x:A. y:B(x)}"
  UNION_def  "UNION(A, B)   == {y. EX  x:A. y:B(x)}"
  insert_def "insert(a, B)  == {x. x=a} Un B"
  Pow_def    "Pow(A)        == {B. B <= A}"

end
