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 \\") "_setle" :: [set, set] => o ("(_/ \\ _)" [50, 51] 50) "_setless" :: [set, set] => o ("op \\") "_setless" :: [set, set] => o ("(_/ \\ _)" [50, 51] 50) "op Int" :: [set, set] => set (infixl "\\" 70) "op Un" :: [set, set] => set (infixl "\\" 65) "op :" :: ['a, set] => o ("op \\") "op :" :: ['a, set] => o ("(_/ \\ _)" [50, 51] 50) "op ~:" :: ['a, set] => o ("op \\") "op ~:" :: ['a, set] => o ("(_/ \\ _)" [50, 51] 50) "UN " :: [idts, o] => o ("(3\\ _./ _)" 10) "INT " :: [idts, o] => o ("(3\\ _./ _)" 10) "@UNION1" :: [pttrn, set] => set ("(3\\ _./ _)" 10) "@INTER1" :: [pttrn, set] => set ("(3\\ _./ _)" 10) "@UNION" :: [pttrn, set, set] => set ("(3\\ _\\_./ _)" 10) "@INTER" :: [pttrn, set, set] => set ("(3\\ _\\_./ _)" 10) "_Ball" :: [pttrn, set, o] => o ("(3\\ _\\_./ _)" [0, 0, 10] 10) "_Bex" :: [pttrn, set, o] => o ("(3\\ _\\_./ _)" [0, 0, 10] 10) translations "op \\" => "op <= :: [_ set, _ set] => o" (* "op \\" => "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